Theory Ext_choice

Up to index of Isabelle/HOL/HOL-Complex/CSP-Prover

theory Ext_choice = CSP_semantics: 
           (*-------------------------------------------*
            |                CSP-Prover                 |
            |               December 2004               |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory Ext_choice = CSP_semantics:

(*  The following simplification rules are deleted in this theory file *)
(*  because they unexpectly rewrite UnionT and InterT.                 *)
(*                  disj_not1: (~ P | Q) = (P --> Q)                   *)

declare disj_not1 [simp del]

(*  The following simplification is sometimes unexpected.              *)
(*                                                                     *)
(*             not_None_eq: (x ~= None) = (EX y. x = Some y)           *)

declare not_None_eq [simp del]

(*********************************************************
                        Dom_T
 *********************************************************)

(*** Ext_choice_memT ***)

lemma Ext_choice_memT: 
  "(t :t [[P [+] Q]]T ev) = (t :t [[P]]T ev | t :t [[Q]]T ev)"
by (simp add: evalT_def memT_UnT)

(*********************************************************
                        Dom_F
 *********************************************************)

(*** Ext_choice_domF ***)

lemma Ext_choice_domF: 
  "{f. (EX   X. f = ([]t,X) & f :f [[P]]F ev IntF [[Q]]F ev) |
       (EX s X. f = (s,X)   & f :f [[P]]F ev UnF  [[Q]]F ev & 
                s ~= []t) |
       (EX   X. f = ([]t,X) & [Tick]t :t [[P]]T ev UnT [[Q]]T ev &
                X <= Evset)} : domF"
apply (simp add: domF_def HC_F2_def)
apply (intro allI impI)
apply (elim conjE disjE)

(* part1 *)
apply (simp add: memF_IntF)
apply (rule disjI1)
apply (rule conjI)
apply (rule memF_F2, simp_all)
apply (rule memF_F2, simp_all)

(* part2 *)
apply (simp add: memF_UnF)
apply (erule disjE)
apply (rule disjI1)
apply (rule memF_F2, simp_all)
apply (rule disjI2)
apply (rule memF_F2, simp_all)

(* part3 *)
apply (fast)
done

(*** Ext_choice_memT ***)

lemma Ext_choice_memF: 
  "(f :f [[P [+] Q]]F ev) =
   ((EX   X. f = ([]t,X) & f :f [[P]]F ev IntF [[Q]]F ev) |
    (EX s X. f = (s,X)   & f :f [[P]]F ev UnF  [[Q]]F ev & s ~= []t) |
    (EX   X. f = ([]t,X) & [Tick]t :t [[P]]T ev UnT [[Q]]T ev & X <= Evset))"
apply (simp only: evalF_def)
apply (simp only: memF_def Abs_domF_inverse Ext_choice_domF[simplified memF_def])
by (simp)

lemmas Ext_choice_mem = Ext_choice_memT Ext_choice_memF

(*******************************
             domSF
 *******************************)

(* T2 *)

lemma Ext_choice_T2 :
  "[| ([[P]]T ev, [[P]]F ev) : domSF ; ([[Q]]T ev, [[Q]]F ev) : domSF |]
     ==> HC_T2 ([[P [+] Q]]T ev, [[P [+] Q]]F ev)"
apply (simp add: HC_T2_def Ext_choice_mem)
apply (intro allI impI)
apply (elim conjE exE)
apply (simp add: memF_UnF)

apply (simp add: domSF_def HC_T2_def)
apply (elim conjE)
apply (drule_tac x="s" in spec)
apply (drule_tac x="s" in spec)
by (fast)

(* F3 *)

lemma Ext_choice_F3 :
  "[| ([[P]]T ev, [[P]]F ev) : domSF ; ([[Q]]T ev, [[Q]]F ev) : domSF |]
     ==> HC_F3 ([[P [+] Q]]T ev, [[P [+] Q]]F ev)"
apply (simp add: HC_F3_def Ext_choice_mem)
apply (intro allI impI)

apply (elim conjE disjE)

(* part1 *)
apply (simp add: memF_IntF)
apply (simp add: domSF_def HC_F3_def)

(* part2 *)
apply (simp add: memF_UnF)
apply (simp add: domSF_def HC_F3_def)
apply (force)

(* part3 *)
apply (simp add: memT_UnT memF_IntF)
apply (case_tac "Tick ~: Y")
 apply (simp add: Evset_def)
 apply (force)

 (* Tick : Y *)
 apply (drule_tac x="Tick" in spec)
 apply (simp)
done

(* T3_F4 *)

lemma Ext_choice_T3_F4 : 
  "[| ([[P]]T ev, [[P]]F ev) : domSF ; ([[Q]]T ev, [[Q]]F ev) : domSF |]
     ==> HC_T3_F4 ([[P [+] Q]]T ev, [[P [+] Q]]F ev)"
apply (simp add: HC_T3_F4_def Ext_choice_mem)
apply (intro allI impI)
apply (elim conjE exE)

apply (simp add: domSF_iff HC_T3_F4_def)
apply (elim conjE)
apply (drule_tac x="s" in spec)
apply (drule_tac x="s" in spec)
apply (simp add: memF_UnF memT_UnT)
by (auto)

(*** Ext_choice_domSF ***)

lemma Ext_choice_domSF : 
  "[| ([[P]]T ev, [[P]]F ev) : domSF ; ([[Q]]T ev, [[Q]]F ev) : domSF |]
     ==> ([[P [+] Q]]T ev, [[P [+] Q]]F ev) : domSF"
apply (simp (no_asm) add: domSF_iff)
apply (simp add: Ext_choice_T2)
apply (simp add: Ext_choice_F3)
apply (simp add: Ext_choice_T3_F4)
done

(*********************************************************
                      mono
 *********************************************************)

(*** T ***)

lemma Ext_choice_evalT_mono:
  "[| [[P1]]T ev1 <= [[P2]]T ev2 ; [[Q1]]T ev1 <= [[Q2]]T ev2 |]
   ==> [[P1 [+] Q1]]T ev1 <= [[P2 [+] Q2]]T ev2"
apply (simp add: subsetT_iff)
apply (intro allI impI)
apply (simp add: Ext_choice_memT)
apply (erule disjE)
by (simp_all)

(*** F ***)

lemma Ext_choice_evalF_mono:
  "[| [[P1]]T ev1 <= [[P2]]T ev2 ; [[Q1]]T ev1 <= [[Q2]]T ev2 ; 
      [[P1]]F ev1 <= [[P2]]F ev2 ; [[Q1]]F ev1 <= [[Q2]]F ev2 |]
   ==> [[P1 [+] Q1]]F ev1 <= [[P2 [+] Q2]]F ev2"
apply (simp add: subsetF_iff)
apply (intro allI impI)
apply (simp add: Ext_choice_memF)

 apply (erule disjE)
 apply (simp add: memF_IntF)
 apply (force)

 apply (erule disjE)
 apply (simp add: memF_UnF)
 apply (force)

 apply (simp add: memT_UnT memF_IntF)
 apply (simp add: subsetT_iff)
 apply (elim conjE disjE)
 apply (auto)
done

(****************** to add them again ******************)

declare disj_not1   [simp]
declare not_None_eq [simp]

end

lemma Ext_choice_memT: 

  (t :t [[P [+] Q]]T ev) = (t :t [[P]]T ev ∨ t :t [[Q]]T ev)

lemma Ext_choice_domF: 

  {f. (∃X. f = ([]t, X) ∧ f :f [[P]]F ev IntF [[Q]]F ev) ∨
      (∃s X. f = (s, X) ∧ f :f [[P]]F ev UnF [[Q]]F ev ∧ s ≠ []t) ∨
      (∃X. f = ([]t, X) ∧ [Tick]t :t [[P]]T ev UnT [[Q]]T ev ∧ X ⊆ Evset)}
  ∈ domF

lemma Ext_choice_memF: 

  (f :f [[P [+] Q]]F ev) =
  ((∃X. f = ([]t, X) ∧ f :f [[P]]F ev IntF [[Q]]F ev) ∨
   (∃s X. f = (s, X) ∧ f :f [[P]]F ev UnF [[Q]]F ev ∧ s ≠ []t) ∨
   (∃X. f = ([]t, X) ∧ [Tick]t :t [[P]]T ev UnT [[Q]]T ev ∧ X ⊆ Evset))

lemmas Ext_choice_mem: 

  (t :t [[P [+] Q]]T ev) = (t :t [[P]]T ev ∨ t :t [[Q]]T ev)
  (f :f [[P [+] Q]]F ev) =
  ((∃X. f = ([]t, X) ∧ f :f [[P]]F ev IntF [[Q]]F ev) ∨
   (∃s X. f = (s, X) ∧ f :f [[P]]F ev UnF [[Q]]F ev ∧ s ≠ []t) ∨
   (∃X. f = ([]t, X) ∧ [Tick]t :t [[P]]T ev UnT [[Q]]T ev ∧ X ⊆ Evset))

lemma Ext_choice_T2: 

  [| ([[P]]T ev, [[P]]F ev) ∈ domSF; ([[Q]]T ev, [[Q]]F ev) ∈ domSF |]
  ==> HC_T2 ([[P [+] Q]]T ev, [[P [+] Q]]F ev)

lemma Ext_choice_F3: 

  [| ([[P]]T ev, [[P]]F ev) ∈ domSF; ([[Q]]T ev, [[Q]]F ev) ∈ domSF |]
  ==> HC_F3 ([[P [+] Q]]T ev, [[P [+] Q]]F ev)

lemma Ext_choice_T3_F4: 

  [| ([[P]]T ev, [[P]]F ev) ∈ domSF; ([[Q]]T ev, [[Q]]F ev) ∈ domSF |]
  ==> HC_T3_F4 ([[P [+] Q]]T ev, [[P [+] Q]]F ev)

lemma Ext_choice_domSF: 

  [| ([[P]]T ev, [[P]]F ev) ∈ domSF; ([[Q]]T ev, [[Q]]F ev) ∈ domSF |]
  ==> ([[P [+] Q]]T ev, [[P [+] Q]]F ev) ∈ domSF

lemma Ext_choice_evalT_mono: 

  [| [[P1]]T ev1 ≤ [[P2]]T ev2; [[Q1]]T ev1 ≤ [[Q2]]T ev2 |]
  ==> [[P1 [+] Q1]]T ev1 ≤ [[P2 [+] Q2]]T ev2

lemma Ext_choice_evalF_mono: 

  [| [[P1]]T ev1 ≤ [[P2]]T ev2; [[Q1]]T ev1 ≤ [[Q2]]T ev2;
     [[P1]]F ev1 ≤ [[P2]]F ev2; [[Q1]]F ev1 ≤ [[Q2]]F ev2 |]
  ==> [[P1 [+] Q1]]F ev1 ≤ [[P2 [+] Q2]]F ev2