Theory Ext_pre_choice

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

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

theory Ext_pre_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_pre_choice_domT ***)

lemma Ext_pre_choice_domT: 
  "{t. t = []t | 
       (EX a s. t = [Ev a]t @t s & s :t [[Pf a]]T ev & a : X) } : domT"
apply (simp add: domT_def HC_T1_def)
apply (rule conjI)
apply (rule_tac x="[]t" in exI, simp)

apply (simp add: prefix_closed_def)
apply (intro allI impI)
apply (elim conjE exE)

apply (erule disjE, simp)    (* []t *)

apply (elim conjE exE, simp)
apply (erule disjE, simp)    (* None --> contradict *)
apply (erule disjE, simp)    (* []t *)

apply (elim conjE exE, simp)
apply (rule_tac x="a" in exI)
apply (rule_tac x="v'" in exI, simp)
apply (rule memT_prefix_closed)
by (simp_all)

(*** Ext_pre_choice_memT ***)

lemma Ext_pre_choice_memT: 
  "(t :t [[? :X -> Pf ]]T ev) = 
   (t = []t | (EX a s. t = [Ev a]t @t s & s :t [[Pf a]]T ev & a : X))"
apply (simp add: evalT_def)
by (simp add: memT_def Abs_domT_inverse Ext_pre_choice_domT[simplified memT_def])

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

(*** Ext_pre_choice_domF ***)

lemma Ext_pre_choice_domF: 
  "{f. (EX Y. f = ([]t,Y) & Ev`X Int Y = {}) |
       (EX a s Y. f = ([Ev a]t @t s, Y) & (s,Y) :f [[Pf a]]F ev & a : X) } : domF"
apply (simp add: domF_def HC_F2_def)
apply (intro allI impI)
apply (elim conjE disjE, force)

apply (elim conjE exE, simp)
apply (rule_tac x="a" in exI)
apply (rule_tac x="sa" in exI, simp)
apply (rule memF_F2, simp_all)
done

(*** Ext_pre_choice_memT ***)

lemma Ext_pre_choice_memF: 
  "(f :f [[? :X -> Pf]]F ev) = 
   ((EX Y.     f = ([]t,Y) & Ev`X Int Y = {}) |
    (EX a s Y. f = ([Ev a]t @t s, Y) & (s,Y) :f [[Pf a]]F ev & a : X))"
apply (simp add: evalF_def)
by (simp add: memF_def Abs_domF_inverse Ext_pre_choice_domF[simplified memF_def])

lemmas Ext_pre_choice_mem = Ext_pre_choice_memT Ext_pre_choice_memF

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

(* T2 *)

lemma Ext_pre_choice_T2 :
  "ALL a. ([[Pf a]]T ev, [[Pf a]]F ev) : domSF
     ==> HC_T2 ([[? :X -> Pf]]T ev, [[? :X -> Pf]]F ev)"
apply (simp add: HC_T2_def Ext_pre_choice_mem)
apply (intro allI impI)
apply (elim conjE exE, simp)
apply (rule_tac x="a" in exI)
apply (rule_tac x="sa" in exI, simp)

apply (drule_tac x="a" in spec)
apply (simp add: domSF_def HC_T2_def)
apply (elim conjE)
apply (drule_tac x="sa" in spec)
by (force)

(* F3 *)

lemma Ext_pre_choice_F3 :
  "ALL a. ([[Pf a]]T ev, [[Pf a]]F ev) : domSF
     ==> HC_F3 ([[? :X -> Pf]]T ev, [[? :X -> Pf]]F ev)"
apply (simp add: HC_F3_def Ext_pre_choice_mem)
apply (intro allI impI)

apply (elim conjE disjE, simp)

(* s = []t *)
apply (case_tac "EX a. Ev a :Ev ` X Int (Xa Un Y)")  (* show contradiction" *)
 apply (elim conjE exE)
 apply (drule_tac x="Ev a" in spec)
 apply (drule mp)
  apply (simp)                      (* show "Ev a : Y" *)
  apply (elim conjE disjE)
  apply (fast)                      (* contradict *)
  apply (simp)

 apply (drule_tac x="a" in spec)
 apply (drule_tac x="a" in spec)
 apply (simp)
 apply (drule_tac x="s" in spec)
 apply (simp)
 apply (fast)                      (* contradict *)
apply (fast)                       (* Ev ` X Int (Xa Un Y) = {} *)

(* s ~= []t *)
apply (elim conjE exE, simp)
apply (rule_tac x="a" in exI)
apply (rule_tac x="sa" in exI)
apply (simp)

apply (drule_tac x="a" in spec)
apply (simp add: domSF_def HC_F3_def)
apply (elim conjE)
apply (drule_tac x="sa" in spec)
apply (drule_tac x="Xa" in spec)
apply (drule_tac x="Y" in spec)
apply (simp)

apply (drule mp)
 apply (intro allI impI)
 apply (drule_tac x="aa" in spec, simp)
 apply (drule_tac x="a" in spec)
 apply (drule_tac x="sa @t [aa]t" in spec, simp)
by (simp)

(* T3_F4 *)

lemma Ext_pre_choice_T3_F4 : 
  "ALL a. ([[Pf a]]T ev, [[Pf a]]F ev) : domSF
     ==> HC_T3_F4 ([[? :X -> Pf]]T ev, [[? :X -> Pf]]F ev)"
apply (simp add: HC_T3_F4_def Ext_pre_choice_mem)
apply (intro allI impI)
apply (elim conjE exE)
apply (insert trace_nil_or_Tick_or_Ev)
apply (drule_tac x="s" in spec)
apply (simp add: not_None)

apply (erule disjE, simp)   (* s = []t --> contradict *)
apply (erule disjE, simp)   (* s = [Tick]t --> contradict *)

apply (elim conjE exE)      (* s = [Ev aa]t @t sb *)
apply (simp add: not_None)

apply (drule_tac x="a" in spec)
apply (simp add: domSF_iff HC_T3_F4_def)
apply (elim conjE exE)
apply (drule_tac x="sb" in spec)
by (simp)

(*** Ext_pre_choice_domSF ***)

lemma Ext_pre_choice_domSF : 
  "ALL a. ([[Pf a]]T ev, [[Pf a]]F ev) : domSF
     ==> ([[? :X -> Pf]]T ev, [[? :X -> Pf]]F ev) : domSF"
apply (simp (no_asm) add: domSF_iff)
apply (simp add: Ext_pre_choice_T2)
apply (simp add: Ext_pre_choice_F3)
apply (simp add: Ext_pre_choice_T3_F4)
done

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

(*** T ***)

lemma Ext_pre_choice_evalT_mono:
  "ALL a:X. [[Pf a]]T ev1 <= [[Qf a]]T ev2
    ==> [[? :X -> Pf]]T ev1 <= [[? :X -> Qf]]T ev2"
apply (simp add: subsetT_iff)
apply (intro allI impI)
apply (simp add: Ext_pre_choice_memT)
apply (erule disjE, simp)

apply (elim conjE exE)
apply (drule_tac x="a" in bspec, simp)
apply (drule_tac x="s" in spec, simp)
apply (rule_tac x="a" in exI)
apply (rule_tac x="s" in exI)
by (simp)

(*** F ***)

lemma Ext_pre_choice_evalF_mono:
  "ALL a:X. [[Pf a]]F ev1 <= [[Qf a]]F ev2 
    ==> [[? :X -> Pf]]F ev1 <= [[? :X -> Qf]]F ev2"
apply (simp add: subsetF_iff)
apply (intro allI impI)
apply (simp add: Ext_pre_choice_memF)
apply (erule disjE, simp)

apply (elim conjE exE)
apply (drule_tac x="a" in bspec, simp)
apply (drule_tac x="sa" in spec)
apply (drule_tac x="Xa" in spec)
apply (simp)
apply (rule_tac x="a" in exI)
apply (rule_tac x="sa" in exI)
by (simp)

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

declare disj_not1   [simp]
declare not_None_eq [simp]

end

lemma Ext_pre_choice_domT: 

  {t. t = []t ∨ (∃a s. t = [Ev a]t @t s ∧ s :t [[Pf a]]T ev ∧ a ∈ X)} ∈ domT

lemma Ext_pre_choice_memT: 

  (t :t [[? :X -> Pf]]T ev) =
  (t = []t ∨ (∃a s. t = [Ev a]t @t s ∧ s :t [[Pf a]]T ev ∧ a ∈ X))

lemma Ext_pre_choice_domF: 

  {f. (∃Y. f = ([]t, Y) ∧ Ev ` X ∩ Y = {}) ∨
      (∃a s Y. f = ([Ev a]t @t s, Y) ∧ (s, Y) :f [[Pf a]]F ev ∧ a ∈ X)}
  ∈ domF

lemma Ext_pre_choice_memF: 

  (f :f [[? :X -> Pf]]F ev) =
  ((∃Y. f = ([]t, Y) ∧ Ev ` X ∩ Y = {}) ∨
   (∃a s Y. f = ([Ev a]t @t s, Y) ∧ (s, Y) :f [[Pf a]]F ev ∧ a ∈ X))

lemmas Ext_pre_choice_mem: 

  (t :t [[? :X -> Pf]]T ev) =
  (t = []t ∨ (∃a s. t = [Ev a]t @t s ∧ s :t [[Pf a]]T ev ∧ a ∈ X))
  (f :f [[? :X -> Pf]]F ev) =
  ((∃Y. f = ([]t, Y) ∧ Ev ` X ∩ Y = {}) ∨
   (∃a s Y. f = ([Ev a]t @t s, Y) ∧ (s, Y) :f [[Pf a]]F ev ∧ a ∈ X))

lemma Ext_pre_choice_T2: 

  ∀a. ([[Pf a]]T ev, [[Pf a]]F ev) ∈ domSF
  ==> HC_T2 ([[? :X -> Pf]]T ev, [[? :X -> Pf]]F ev)

lemma Ext_pre_choice_F3: 

  ∀a. ([[Pf a]]T ev, [[Pf a]]F ev) ∈ domSF
  ==> HC_F3 ([[? :X -> Pf]]T ev, [[? :X -> Pf]]F ev)

lemma Ext_pre_choice_T3_F4: 

  ∀a. ([[Pf a]]T ev, [[Pf a]]F ev) ∈ domSF
  ==> HC_T3_F4 ([[? :X -> Pf]]T ev, [[? :X -> Pf]]F ev)

lemma Ext_pre_choice_domSF: 

  ∀a. ([[Pf a]]T ev, [[Pf a]]F ev) ∈ domSF
  ==> ([[? :X -> Pf]]T ev, [[? :X -> Pf]]F ev) ∈ domSF

lemma Ext_pre_choice_evalT_mono: 

  ∀a∈X. [[Pf a]]T ev1 ≤ [[Qf a]]T ev2
  ==> [[? :X -> Pf]]T ev1 ≤ [[? :X -> Qf]]T ev2

lemma Ext_pre_choice_evalF_mono: 

  ∀a∈X. [[Pf a]]F ev1 ≤ [[Qf a]]F ev2
  ==> [[? :X -> Pf]]F ev1 ≤ [[? :X -> Qf]]F ev2