# HG changeset patch # User wenzelm # Date 1451507721 -3600 # Node ID 89291b5d0ede5c7e3e385787a2f110467363bd9a # Parent b66d2ca1f907d1337e3429c9f91a46d582aadd1c more symbols; diff -r b66d2ca1f907 -r 89291b5d0ede src/HOL/HOLCF/IOA/ABP/Correctness.thy --- a/src/HOL/HOLCF/IOA/ABP/Correctness.thy Wed Dec 30 21:23:38 2015 +0100 +++ b/src/HOL/HOLCF/IOA/ABP/Correctness.thy Wed Dec 30 21:35:21 2015 +0100 @@ -28,11 +28,11 @@ definition system_ioa :: "('m action, bool * 'm impl_state)ioa" where - "system_ioa = (env_ioa || impl_ioa)" + "system_ioa = (env_ioa \ impl_ioa)" definition system_fin_ioa :: "('m action, bool * 'm impl_state)ioa" where - "system_fin_ioa = (env_ioa || impl_fin_ioa)" + "system_fin_ioa = (env_ioa \ impl_fin_ioa)" axiomatization where @@ -231,7 +231,7 @@ srch_fin_ioa_def rsch_fin_ioa_def rsch_ioa_def sender_trans_def receiver_trans_def set_lemmas -lemma compat_rec: "compatible receiver_ioa (srch_ioa || rsch_ioa)" +lemma compat_rec: "compatible receiver_ioa (srch_ioa \ rsch_ioa)" apply (simp del: del_simps add: compatible_def asig_of_par asig_comp_def actions_def Int_def) apply simp @@ -241,7 +241,7 @@ done text {* 5 proofs totally the same as before *} -lemma compat_rec_fin: "compatible receiver_ioa (srch_fin_ioa || rsch_fin_ioa)" +lemma compat_rec_fin: "compatible receiver_ioa (srch_fin_ioa \ rsch_fin_ioa)" apply (simp del: del_simps add: compatible_def asig_of_par asig_comp_def actions_def Int_def) apply simp @@ -251,7 +251,7 @@ done lemma compat_sen: "compatible sender_ioa - (receiver_ioa || srch_ioa || rsch_ioa)" + (receiver_ioa \ srch_ioa \ rsch_ioa)" apply (simp del: del_simps add: compatible_def asig_of_par asig_comp_def actions_def Int_def) apply simp @@ -261,7 +261,7 @@ done lemma compat_sen_fin: "compatible sender_ioa - (receiver_ioa || srch_fin_ioa || rsch_fin_ioa)" + (receiver_ioa \ srch_fin_ioa \ rsch_fin_ioa)" apply (simp del: del_simps add: compatible_def asig_of_par asig_comp_def actions_def Int_def) apply simp @@ -271,7 +271,7 @@ done lemma compat_env: "compatible env_ioa - (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)" + (sender_ioa \ receiver_ioa \ srch_ioa \ rsch_ioa)" apply (simp del: del_simps add: compatible_def asig_of_par asig_comp_def actions_def Int_def) apply simp @@ -281,7 +281,7 @@ done lemma compat_env_fin: "compatible env_ioa - (sender_ioa || receiver_ioa || srch_fin_ioa || rsch_fin_ioa)" + (sender_ioa \ receiver_ioa \ srch_fin_ioa \ rsch_fin_ioa)" apply (simp del: del_simps add: compatible_def asig_of_par asig_comp_def actions_def Int_def) apply simp diff -r b66d2ca1f907 -r 89291b5d0ede src/HOL/HOLCF/IOA/ABP/Impl.thy --- a/src/HOL/HOLCF/IOA/ABP/Impl.thy Wed Dec 30 21:23:38 2015 +0100 +++ b/src/HOL/HOLCF/IOA/ABP/Impl.thy Wed Dec 30 21:35:21 2015 +0100 @@ -14,7 +14,7 @@ definition impl_ioa :: "('m action, 'm impl_state)ioa" where - "impl_ioa = (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)" + "impl_ioa = (sender_ioa \ receiver_ioa \ srch_ioa \ rsch_ioa)" definition sen :: "'m impl_state => 'm sender_state" where diff -r b66d2ca1f907 -r 89291b5d0ede src/HOL/HOLCF/IOA/ABP/Impl_finite.thy --- a/src/HOL/HOLCF/IOA/ABP/Impl_finite.thy Wed Dec 30 21:23:38 2015 +0100 +++ b/src/HOL/HOLCF/IOA/ABP/Impl_finite.thy Wed Dec 30 21:35:21 2015 +0100 @@ -15,7 +15,7 @@ definition impl_fin_ioa :: "('m action, 'm impl_fin_state)ioa" where - "impl_fin_ioa = (sender_ioa || receiver_ioa || srch_fin_ioa || + "impl_fin_ioa = (sender_ioa \ receiver_ioa \ srch_fin_ioa \ rsch_fin_ioa)" definition diff -r b66d2ca1f907 -r 89291b5d0ede src/HOL/HOLCF/IOA/NTP/Impl.thy --- a/src/HOL/HOLCF/IOA/NTP/Impl.thy Wed Dec 30 21:23:38 2015 +0100 +++ b/src/HOL/HOLCF/IOA/NTP/Impl.thy Wed Dec 30 21:35:21 2015 +0100 @@ -15,7 +15,7 @@ definition impl_ioa :: "('m action, 'm impl_state)ioa" where - impl_def: "impl_ioa == (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)" + impl_def: "impl_ioa == (sender_ioa \ receiver_ioa \ srch_ioa \ rsch_ioa)" definition sen :: "'m impl_state => 'm sender_state" where "sen = fst" definition rec :: "'m impl_state => 'm receiver_state" where "rec = fst o snd" diff -r b66d2ca1f907 -r 89291b5d0ede src/HOL/HOLCF/IOA/ex/TrivEx.thy --- a/src/HOL/HOLCF/IOA/ex/TrivEx.thy Wed Dec 30 21:23:38 2015 +0100 +++ b/src/HOL/HOLCF/IOA/ex/TrivEx.thy Wed Dec 30 21:35:21 2015 +0100 @@ -45,7 +45,7 @@ "h_abs n = (n~=0)" axiomatization where - MC_result: "validIOA A_ioa (<>[] <%(b,a,c). b>)" + MC_result: "validIOA A_ioa (\\<%(b,a,c). b>)" lemma h_abs_is_abstraction: "is_abstraction h_abs C_ioa A_ioa" @@ -61,7 +61,7 @@ apply (simp add: h_abs_def) done -lemma TrivEx_abstraction: "validIOA C_ioa (<>[] <%(n,a,m). n~=0>)" +lemma TrivEx_abstraction: "validIOA C_ioa (\\<%(n,a,m). n~=0>)" apply (rule AbsRuleT1) apply (rule h_abs_is_abstraction) apply (rule MC_result) diff -r b66d2ca1f907 -r 89291b5d0ede src/HOL/HOLCF/IOA/ex/TrivEx2.thy --- a/src/HOL/HOLCF/IOA/ex/TrivEx2.thy Wed Dec 30 21:23:38 2015 +0100 +++ b/src/HOL/HOLCF/IOA/ex/TrivEx2.thy Wed Dec 30 21:35:21 2015 +0100 @@ -51,7 +51,7 @@ "h_abs n = (n~=0)" axiomatization where - MC_result: "validLIOA (A_ioa,WF A_ioa {INC}) (<>[] <%(b,a,c). b>)" + MC_result: "validLIOA (A_ioa,WF A_ioa {INC}) (\\<%(b,a,c). b>)" lemma h_abs_is_abstraction: @@ -90,7 +90,7 @@ lemma TrivEx2_abstraction: - "validLIOA C_live_ioa (<>[] <%(n,a,m). n~=0>)" + "validLIOA C_live_ioa (\\<%(n,a,m). n~=0>)" apply (unfold C_live_ioa_def) apply (rule AbsRuleT2) apply (rule h_abs_is_liveabstraction) diff -r b66d2ca1f907 -r 89291b5d0ede src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy --- a/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy Wed Dec 30 21:23:38 2015 +0100 +++ b/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy Wed Dec 30 21:35:21 2015 +0100 @@ -58,7 +58,7 @@ (* analog to the proved thm strength_Box - proof skipped as trivial *) weak_Box: "temp_weakening P Q h - ==> temp_weakening ([] P) ([] Q) h" + ==> temp_weakening (\P) (\Q) h" axiomatization where (* analog to the proved thm strength_Next - proof skipped as trivial *) @@ -412,7 +412,7 @@ lemma strength_Box: "[| temp_strengthening P Q h |] - ==> temp_strengthening ([] P) ([] Q) h" + ==> temp_strengthening (\P) (\Q) h" apply (unfold temp_strengthening_def state_strengthening_def temp_sat_def satisfies_def Box_def) apply clarify apply (frule ex2seq_tsuffix) @@ -526,7 +526,7 @@ lemma strength_Diamond: "[| temp_strengthening P Q h |] - ==> temp_strengthening (<> P) (<> Q) h" + ==> temp_strengthening (\P) (\Q) h" apply (unfold Diamond_def) apply (rule strength_NOT) apply (rule weak_Box) @@ -536,7 +536,7 @@ lemma strength_Leadsto: "[| temp_weakening P1 P2 h; temp_strengthening Q1 Q2 h |] - ==> temp_strengthening (P1 ~> Q1) (P2 ~> Q2) h" + ==> temp_strengthening (P1 \ Q1) (P2 \ Q2) h" apply (unfold Leadsto_def) apply (rule strength_Box) apply (erule strength_IMPLIES) @@ -548,7 +548,7 @@ lemma weak_Diamond: "[| temp_weakening P Q h |] - ==> temp_weakening (<> P) (<> Q) h" + ==> temp_weakening (\P) (\Q) h" apply (unfold Diamond_def) apply (rule weak_NOT) apply (rule strength_Box) @@ -558,7 +558,7 @@ lemma weak_Leadsto: "[| temp_strengthening P1 P2 h; temp_weakening Q1 Q2 h |] - ==> temp_weakening (P1 ~> Q1) (P2 ~> Q2) h" + ==> temp_weakening (P1 \ Q1) (P2 \ Q2) h" apply (unfold Leadsto_def) apply (rule weak_Box) apply (erule weak_IMPLIES) diff -r b66d2ca1f907 -r 89291b5d0ede src/HOL/HOLCF/IOA/meta_theory/Automata.thy --- a/src/HOL/HOLCF/IOA/meta_theory/Automata.thy Wed Dec 30 21:23:38 2015 +0100 +++ b/src/HOL/HOLCF/IOA/meta_theory/Automata.thy Wed Dec 30 21:35:21 2015 +0100 @@ -57,7 +57,7 @@ (* binary composition of action signatures and automata *) asig_comp ::"['a signature, 'a signature] => 'a signature" compatible ::"[('a,'s)ioa, ('a,'t)ioa] => bool" - par ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa" (infixr "||" 10) + par ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa" (infixr "\" 10) (* hiding and restricting *) hide_asig :: "['a signature, 'a set] => 'a signature" @@ -69,9 +69,6 @@ rename_set :: "'a set => ('c => 'a option) => 'c set" rename :: "('a, 'b)ioa => ('c => 'a option) => ('c,'b)ioa" -notation (xsymbols) - par (infixr "\" 10) - inductive reachable :: "('a, 's) ioa => 's => bool" @@ -145,7 +142,7 @@ (internals(a1) Un internals(a2))))" par_def: - "(A || B) == + "(A \ B) == (asig_comp (asig_of A) (asig_of B), {pr. fst(pr):starts_of(A) & snd(pr):starts_of(B)}, {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) @@ -266,12 +263,12 @@ done lemma starts_of_par: -"starts_of(A || B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}" +"starts_of(A \ B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}" apply (simp add: par_def ioa_projections) done lemma trans_of_par: -"trans_of(A || B) = {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) +"trans_of(A \ B) = {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) in (a:act A | a:act B) & (if a:act A then (fst(s),a,fst(t)):trans_of(A) @@ -293,38 +290,38 @@ apply blast done -lemma asig_of_par: "asig_of(A || B) = asig_comp (asig_of A) (asig_of B)" +lemma asig_of_par: "asig_of(A \ B) = asig_comp (asig_of A) (asig_of B)" apply (simp add: par_def ioa_projections) done -lemma externals_of_par: "ext (A1||A2) = +lemma externals_of_par: "ext (A1\A2) = (ext A1) Un (ext A2)" apply (simp add: externals_def asig_of_par asig_comp_def asig_inputs_def asig_outputs_def Un_def set_diff_eq) apply blast done -lemma actions_of_par: "act (A1||A2) = +lemma actions_of_par: "act (A1\A2) = (act A1) Un (act A2)" apply (simp add: actions_def asig_of_par asig_comp_def asig_inputs_def asig_outputs_def asig_internals_def Un_def set_diff_eq) apply blast done -lemma inputs_of_par: "inp (A1||A2) = +lemma inputs_of_par: "inp (A1\A2) = ((inp A1) Un (inp A2)) - ((out A1) Un (out A2))" apply (simp add: actions_def asig_of_par asig_comp_def asig_inputs_def asig_outputs_def Un_def set_diff_eq) done -lemma outputs_of_par: "out (A1||A2) = +lemma outputs_of_par: "out (A1\A2) = (out A1) Un (out A2)" apply (simp add: actions_def asig_of_par asig_comp_def asig_outputs_def Un_def set_diff_eq) done -lemma internals_of_par: "int (A1||A2) = +lemma internals_of_par: "int (A1\A2) = (int A1) Un (int A2)" apply (simp add: actions_def asig_of_par asig_comp_def asig_inputs_def asig_outputs_def asig_internals_def Un_def set_diff_eq) @@ -379,7 +376,7 @@ apply blast done -(* needed for propagation of input_enabledness from A,B to A||B *) +(* needed for propagation of input_enabledness from A,B to A\B *) lemma inpAAactB_is_inpBoroutB: "[| compatible A B; a:inp A ;a:act B|] ==> a : inp B | a: out B" apply (unfold asig_outputs_def asig_internals_def actions_def asig_inputs_def @@ -396,7 +393,7 @@ 2. inputs_of_par: outputs are no longer inputs of par. This is important here *) lemma input_enabled_par: "[| compatible A B; input_enabled A; input_enabled B|] - ==> input_enabled (A||B)" + ==> input_enabled (A\B)" apply (unfold input_enabled_def) apply (simp add: Let_def inputs_of_par trans_of_par) apply (tactic "safe_tac (Context.raw_transfer @{theory} @{theory_context Fun})") @@ -544,49 +541,49 @@ done -subsection "trans_of(A||B)" +subsection "trans_of(A\B)" -lemma trans_A_proj: "[|(s,a,t):trans_of (A||B); a:act A|] +lemma trans_A_proj: "[|(s,a,t):trans_of (A\B); a:act A|] ==> (fst s,a,fst t):trans_of A" apply (simp add: Let_def par_def trans_of_def) done -lemma trans_B_proj: "[|(s,a,t):trans_of (A||B); a:act B|] +lemma trans_B_proj: "[|(s,a,t):trans_of (A\B); a:act B|] ==> (snd s,a,snd t):trans_of B" apply (simp add: Let_def par_def trans_of_def) done -lemma trans_A_proj2: "[|(s,a,t):trans_of (A||B); a~:act A|] +lemma trans_A_proj2: "[|(s,a,t):trans_of (A\B); a~:act A|] ==> fst s = fst t" apply (simp add: Let_def par_def trans_of_def) done -lemma trans_B_proj2: "[|(s,a,t):trans_of (A||B); a~:act B|] +lemma trans_B_proj2: "[|(s,a,t):trans_of (A\B); a~:act B|] ==> snd s = snd t" apply (simp add: Let_def par_def trans_of_def) done -lemma trans_AB_proj: "(s,a,t):trans_of (A||B) +lemma trans_AB_proj: "(s,a,t):trans_of (A\B) ==> a :act A | a :act B" apply (simp add: Let_def par_def trans_of_def) done lemma trans_AB: "[|a:act A;a:act B; (fst s,a,fst t):trans_of A;(snd s,a,snd t):trans_of B|] - ==> (s,a,t):trans_of (A||B)" + ==> (s,a,t):trans_of (A\B)" apply (simp add: Let_def par_def trans_of_def) done lemma trans_A_notB: "[|a:act A;a~:act B; (fst s,a,fst t):trans_of A;snd s=snd t|] - ==> (s,a,t):trans_of (A||B)" + ==> (s,a,t):trans_of (A\B)" apply (simp add: Let_def par_def trans_of_def) done lemma trans_notA_B: "[|a~:act A;a:act B; (snd s,a,snd t):trans_of B;fst s=fst t|] - ==> (s,a,t):trans_of (A||B)" + ==> (s,a,t):trans_of (A\B)" apply (simp add: Let_def par_def trans_of_def) done @@ -595,7 +592,7 @@ lemma trans_of_par4: -"((s,a,t) : trans_of(A || B || C || D)) = +"((s,a,t) : trans_of(A \ B \ C \ D)) = ((a:actions(asig_of(A)) | a:actions(asig_of(B)) | a:actions(asig_of(C)) | a:actions(asig_of(D))) & (if a:actions(asig_of(A)) then (fst(s),a,fst(t)):trans_of(A) @@ -614,8 +611,8 @@ subsection "proof obligation generator for IOA requirements" -(* without assumptions on A and B because is_trans_of is also incorporated in ||def *) -lemma is_trans_of_par: "is_trans_of (A||B)" +(* without assumptions on A and B because is_trans_of is also incorporated in \def *) +lemma is_trans_of_par: "is_trans_of (A\B)" apply (unfold is_trans_of_def) apply (simp add: Let_def actions_of_par trans_of_par) done @@ -635,7 +632,7 @@ done lemma is_asig_of_par: "[| is_asig_of A; is_asig_of B; compatible A B|] - ==> is_asig_of (A||B)" + ==> is_asig_of (A\B)" apply (simp add: is_asig_of_def asig_of_par asig_comp_def compatible_def asig_internals_def asig_outputs_def asig_inputs_def actions_def is_asig_def) apply (simp add: asig_of_def) @@ -663,7 +660,7 @@ lemma compatible_par: -"[|compatible A B; compatible A C |]==> compatible A (B||C)" +"[|compatible A B; compatible A C |]==> compatible A (B\C)" apply (unfold compatible_def) apply (simp add: internals_of_par outputs_of_par actions_of_par) apply auto @@ -671,7 +668,7 @@ (* better derive by previous one and compat_commute *) lemma compatible_par2: -"[|compatible A C; compatible B C |]==> compatible (A||B) C" +"[|compatible A C; compatible B C |]==> compatible (A\B) C" apply (unfold compatible_def) apply (simp add: internals_of_par outputs_of_par actions_of_par) apply auto diff -r b66d2ca1f907 -r 89291b5d0ede src/HOL/HOLCF/IOA/meta_theory/CompoExecs.thy --- a/src/HOL/HOLCF/IOA/meta_theory/CompoExecs.thy Wed Dec 30 21:23:38 2015 +0100 +++ b/src/HOL/HOLCF/IOA/meta_theory/CompoExecs.thy Wed Dec 30 21:35:21 2015 +0100 @@ -208,10 +208,10 @@ (* --------------------------------------------------------------------- *) -(* Lemma_1_1a : is_ex_fr propagates from A||B to Projections A and B *) +(* Lemma_1_1a : is_ex_fr propagates from A\B to Projections A and B *) (* --------------------------------------------------------------------- *) -lemma lemma_1_1a: "!s. is_exec_frag (A||B) (s,xs) +lemma lemma_1_1a: "!s. is_exec_frag (A\B) (s,xs) --> is_exec_frag A (fst s, Filter_ex2 (asig_of A)$(ProjA2$xs)) & is_exec_frag B (snd s, Filter_ex2 (asig_of B)$(ProjB2$xs))" @@ -222,10 +222,10 @@ (* --------------------------------------------------------------------- *) -(* Lemma_1_1b : is_ex_fr (A||B) implies stuttering on Projections *) +(* Lemma_1_1b : is_ex_fr (A\B) implies stuttering on Projections *) (* --------------------------------------------------------------------- *) -lemma lemma_1_1b: "!s. is_exec_frag (A||B) (s,xs) +lemma lemma_1_1b: "!s. is_exec_frag (A\B) (s,xs) --> stutter (asig_of A) (fst s,ProjA2$xs) & stutter (asig_of B) (snd s,ProjB2$xs)" @@ -237,11 +237,11 @@ (* --------------------------------------------------------------------- *) -(* Lemma_1_1c : Executions of A||B have only A- or B-actions *) +(* Lemma_1_1c : Executions of A\B have only A- or B-actions *) (* --------------------------------------------------------------------- *) -lemma lemma_1_1c: "!s. (is_exec_frag (A||B) (s,xs) - --> Forall (%x. fst x:act (A||B)) xs)" +lemma lemma_1_1c: "!s. (is_exec_frag (A\B) (s,xs) + --> Forall (%x. fst x:act (A\B)) xs)" apply (tactic {* pair_induct_tac @{context} "xs" [@{thm Forall_def}, @{thm sforall_def}, @{thm is_exec_frag_def}] 1 *}) @@ -252,7 +252,7 @@ (* ----------------------------------------------------------------------- *) -(* Lemma_1_2 : ex A, exB, stuttering and forall a:A|B implies ex (A||B) *) +(* Lemma_1_2 : ex A, exB, stuttering and forall a:A|B implies ex (A\B) *) (* ----------------------------------------------------------------------- *) lemma lemma_1_2: @@ -260,8 +260,8 @@ is_exec_frag B (snd s,Filter_ex2 (asig_of B)$(ProjB2$xs)) & stutter (asig_of A) (fst s,(ProjA2$xs)) & stutter (asig_of B) (snd s,(ProjB2$xs)) & - Forall (%x. fst x:act (A||B)) xs - --> is_exec_frag (A||B) (s,xs)" + Forall (%x. fst x:act (A\B)) xs + --> is_exec_frag (A\B) (s,xs)" apply (tactic {* pair_induct_tac @{context} "xs" [@{thm Forall_def}, @{thm sforall_def}, @{thm is_exec_frag_def}, @{thm stutter_def}] 1 *}) @@ -272,11 +272,11 @@ subsection {* COMPOSITIONALITY on EXECUTION Level -- Main Theorem *} lemma compositionality_ex: -"(ex:executions(A||B)) = +"(ex:executions(A\B)) = (Filter_ex (asig_of A) (ProjA ex) : executions A & Filter_ex (asig_of B) (ProjB ex) : executions B & stutter (asig_of A) (ProjA ex) & stutter (asig_of B) (ProjB ex) & - Forall (%x. fst x:act (A||B)) (snd ex))" + Forall (%x. fst x:act (A\B)) (snd ex))" apply (simp (no_asm) add: executions_def ProjB_def Filter_ex_def ProjA_def starts_of_par) apply (tactic {* pair_tac @{context} "ex" 1 *}) @@ -293,7 +293,7 @@ subsection {* COMPOSITIONALITY on EXECUTION Level -- for Modules *} lemma compositionality_ex_modules: - "Execs (A||B) = par_execs (Execs A) (Execs B)" + "Execs (A\B) = par_execs (Execs A) (Execs B)" apply (unfold Execs_def par_execs_def) apply (simp add: asig_of_par) apply (rule set_eqI) diff -r b66d2ca1f907 -r 89291b5d0ede src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy --- a/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy Wed Dec 30 21:23:38 2015 +0100 +++ b/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy Wed Dec 30 21:35:21 2015 +0100 @@ -220,15 +220,15 @@ (* --------------------------------------------------------------------- *) -(* Schedules of A||B have only A- or B-actions *) +(* Schedules of A\B have only A- or B-actions *) (* --------------------------------------------------------------------- *) (* very similar to lemma_1_1c, but it is not checking if every action element of an ex is in A or B, but after projecting it onto the action schedule. Of course, this is the same proposition, but we cannot change this one, when then rather lemma_1_1c *) -lemma sch_actions_in_AorB: "!s. is_exec_frag (A||B) (s,xs) - --> Forall (%x. x:act (A||B)) (filter_act$xs)" +lemma sch_actions_in_AorB: "!s. is_exec_frag (A\B) (s,xs) + --> Forall (%x. x:act (A\B)) (filter_act$xs)" apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}, @{thm Forall_def}, @{thm sforall_def}] 1 *}) @@ -246,7 +246,7 @@ --------------------------------------------------------------------------- *) lemma Mapfst_mkex_is_sch: "! exA exB s t. - Forall (%x. x:act (A||B)) sch & + Forall (%x. x:act (A\B)) sch & Filter (%a. a:act A)$sch << filter_act$exA & Filter (%a. a:act B)$sch << filter_act$exB --> filter_act$(snd (mkex A B sch (s,exA) (t,exB))) = sch" @@ -324,14 +324,14 @@ --------------------------------------------------------------------------- *) lemma stutterA_mkex: "! exA exB s t. - Forall (%x. x:act (A||B)) sch & + Forall (%x. x:act (A\B)) sch & Filter (%a. a:act A)$sch << filter_act$exA & Filter (%a. a:act B)$sch << filter_act$exB --> stutter (asig_of A) (s,ProjA2$(snd (mkex A B sch (s,exA) (t,exB))))" by (mkex_induct sch exA exB) lemma stutter_mkex_on_A: "[| - Forall (%x. x:act (A||B)) sch ; + Forall (%x. x:act (A\B)) sch ; Filter (%a. a:act A)$sch << filter_act$(snd exA) ; Filter (%a. a:act B)$sch << filter_act$(snd exB) |] ==> stutter (asig_of A) (ProjA (mkex A B sch exA exB))" @@ -351,7 +351,7 @@ --------------------------------------------------------------------------- *) lemma stutterB_mkex: "! exA exB s t. - Forall (%x. x:act (A||B)) sch & + Forall (%x. x:act (A\B)) sch & Filter (%a. a:act A)$sch << filter_act$exA & Filter (%a. a:act B)$sch << filter_act$exB --> stutter (asig_of B) (t,ProjB2$(snd (mkex A B sch (s,exA) (t,exB))))" @@ -359,7 +359,7 @@ lemma stutter_mkex_on_B: "[| - Forall (%x. x:act (A||B)) sch ; + Forall (%x. x:act (A\B)) sch ; Filter (%a. a:act A)$sch << filter_act$(snd exA) ; Filter (%a. a:act B)$sch << filter_act$(snd exB) |] ==> stutter (asig_of B) (ProjB (mkex A B sch exA exB))" @@ -380,7 +380,7 @@ --------------------------------------------------------------------------- *) lemma filter_mkex_is_exA_tmp: "! exA exB s t. - Forall (%x. x:act (A||B)) sch & + Forall (%x. x:act (A\B)) sch & Filter (%a. a:act A)$sch << filter_act$exA & Filter (%a. a:act B)$sch << filter_act$exB --> Filter_ex2 (asig_of A)$(ProjA2$(snd (mkex A B sch (s,exA) (t,exB)))) = @@ -416,7 +416,7 @@ lemma filter_mkex_is_exA: "!!sch exA exB. - [| Forall (%a. a:act (A||B)) sch ; + [| Forall (%a. a:act (A\B)) sch ; Filter (%a. a:act A)$sch = filter_act$(snd exA) ; Filter (%a. a:act B)$sch = filter_act$(snd exB) |] ==> Filter_ex (asig_of A) (ProjA (mkex A B sch exA exB)) = exA" @@ -440,7 +440,7 @@ --------------------------------------------------------------------------- *) lemma filter_mkex_is_exB_tmp: "! exA exB s t. - Forall (%x. x:act (A||B)) sch & + Forall (%x. x:act (A\B)) sch & Filter (%a. a:act A)$sch << filter_act$exA & Filter (%a. a:act B)$sch << filter_act$exB --> Filter_ex2 (asig_of B)$(ProjB2$(snd (mkex A B sch (s,exA) (t,exB)))) = @@ -457,7 +457,7 @@ lemma filter_mkex_is_exB: "!!sch exA exB. - [| Forall (%a. a:act (A||B)) sch ; + [| Forall (%a. a:act (A\B)) sch ; Filter (%a. a:act A)$sch = filter_act$(snd exA) ; Filter (%a. a:act B)$sch = filter_act$(snd exB) |] ==> Filter_ex (asig_of B) (ProjB (mkex A B sch exA exB)) = exB" @@ -478,10 +478,10 @@ lemma mkex_actions_in_AorB: "!s t exA exB. - Forall (%x. x : act (A || B)) sch & + Forall (%x. x : act (A \ B)) sch & Filter (%a. a:act A)$sch << filter_act$exA & Filter (%a. a:act B)$sch << filter_act$exB - --> Forall (%x. fst x : act (A ||B)) + --> Forall (%x. fst x : act (A \B)) (snd (mkex A B sch (s,exA) (t,exB)))" by (mkex_induct sch exA exB) @@ -492,10 +492,10 @@ (* ------------------------------------------------------------------ *) lemma compositionality_sch: -"(sch : schedules (A||B)) = +"(sch : schedules (A\B)) = (Filter (%a. a:act A)$sch : schedules A & Filter (%a. a:act B)$sch : schedules B & - Forall (%x. x:act (A||B)) sch)" + Forall (%x. x:act (A\B)) sch)" apply (simp (no_asm) add: schedules_def has_schedule_def) apply auto (* ==> *) @@ -514,7 +514,7 @@ (* <== *) -(* mkex is exactly the construction of exA||B out of exA, exB, and the oracle sch, +(* mkex is exactly the construction of exA\B out of exA, exB, and the oracle sch, we need here *) apply (rename_tac exA exB) apply (rule_tac x = "mkex A B sch exA exB" in bexI) @@ -535,7 +535,7 @@ subsection {* COMPOSITIONALITY on SCHEDULE Level -- for Modules *} lemma compositionality_sch_modules: - "Scheds (A||B) = par_scheds (Scheds A) (Scheds B)" + "Scheds (A\B) = par_scheds (Scheds A) (Scheds B)" apply (unfold Scheds_def par_scheds_def) apply (simp add: asig_of_par) diff -r b66d2ca1f907 -r 89291b5d0ede src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy --- a/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy Wed Dec 30 21:23:38 2015 +0100 +++ b/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy Wed Dec 30 21:35:21 2015 +0100 @@ -199,8 +199,8 @@ lemma ForallAorB_mksch [rule_format]: "!!A B. compatible A B ==> - ! schA schB. Forall (%x. x:act (A||B)) tr - --> Forall (%x. x:act (A||B)) (mksch A B$tr$schA$schB)" + ! schA schB. Forall (%x. x:act (A\B)) tr + --> Forall (%x. x:act (A\B)) (mksch A B$tr$schA$schB)" apply (tactic {* Seq_induct_tac @{context} "tr" [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *}) apply auto @@ -253,7 +253,7 @@ ! x y. Forall (%x. x:act A) x & Forall (%x. x:act B) y & Filter (%a. a:ext A)$x = Filter (%a. a:act A)$tr & Filter (%a. a:ext B)$y = Filter (%a. a:act B)$tr & - Forall (%x. x:ext (A||B)) tr + Forall (%x. x:ext (A\B)) tr --> Finite (mksch A B$tr$x$y)" apply (erule Seq_Finite_ind) @@ -409,10 +409,10 @@ "!! A B. [| compatible A B; compatible B A; is_asig(asig_of A); is_asig(asig_of B) |] ==> ! schA schB. Forall (%x. x:act A) schA & Forall (%x. x:act B) schB & - Forall (%x. x:ext (A||B)) tr & + Forall (%x. x:ext (A\B)) tr & Filter (%a. a:act A)$tr << Filter (%a. a:ext A)$schA & Filter (%a. a:act B)$tr << Filter (%a. a:ext B)$schB - --> Filter (%a. a:ext (A||B))$(mksch A B$tr$schA$schB) = tr" + --> Filter (%a. a:ext (A\B))$(mksch A B$tr$schA$schB) = tr" apply (tactic {* Seq_induct_tac @{context} "tr" [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *}) @@ -463,7 +463,7 @@ lemma FilterAmksch_is_schA: "!! A B. [| compatible A B; compatible B A; is_asig(asig_of A); is_asig(asig_of B) |] ==> - Forall (%x. x:ext (A||B)) tr & + Forall (%x. x:ext (A\B)) tr & Forall (%x. x:act A) schA & Forall (%x. x:act B) schB & Filter (%a. a:ext A)$schA = Filter (%a. a:act A)$tr & Filter (%a. a:ext B)$schB = Filter (%a. a:act B)$tr & @@ -683,7 +683,7 @@ lemma FilterBmksch_is_schB: "!! A B. [| compatible A B; compatible B A; is_asig(asig_of A); is_asig(asig_of B) |] ==> - Forall (%x. x:ext (A||B)) tr & + Forall (%x. x:ext (A\B)) tr & Forall (%x. x:act A) schA & Forall (%x. x:act B) schB & Filter (%a. a:ext A)$schA = Filter (%a. a:act A)$tr & Filter (%a. a:ext B)$schB = Filter (%a. a:act B)$tr & @@ -900,10 +900,10 @@ lemma compositionality_tr: "!! A B. [| is_trans_of A; is_trans_of B; compatible A B; compatible B A; is_asig(asig_of A); is_asig(asig_of B)|] - ==> (tr: traces(A||B)) = + ==> (tr: traces(A\B)) = (Filter (%a. a:act A)$tr : traces A & Filter (%a. a:act B)$tr : traces B & - Forall (%x. x:ext(A||B)) tr)" + Forall (%x. x:ext(A\B)) tr)" apply (simp (no_asm) add: traces_def has_trace_def) apply auto @@ -919,7 +919,7 @@ prefer 2 apply (simp add: compositionality_sch) apply (simp add: compatibility_consequence2 externals_of_par ext1_ext2_is_not_act2) -(* Traces of A||B have only external actions from A or B *) +(* Traces of A\B have only external actions from A or B *) apply (rule ForallPFilterP) (* <== *) @@ -938,7 +938,7 @@ apply assumption apply (rename_tac h1 h2 schA schB) -(* mksch is exactly the construction of trA||B out of schA, schB, and the oracle tr, +(* mksch is exactly the construction of trA\B out of schA, schB, and the oracle tr, we need here *) apply (rule_tac x = "mksch A B$tr$schA$schB" in bexI) @@ -961,7 +961,7 @@ "!! A B. [| is_trans_of A; is_trans_of B; compatible A B; compatible B A; is_asig(asig_of A); is_asig(asig_of B)|] - ==> Traces (A||B) = par_traces (Traces A) (Traces B)" + ==> Traces (A\B) = par_traces (Traces A) (Traces B)" apply (unfold Traces_def par_traces_def) apply (simp add: asig_of_par) diff -r b66d2ca1f907 -r 89291b5d0ede src/HOL/HOLCF/IOA/meta_theory/Compositionality.thy --- a/src/HOL/HOLCF/IOA/meta_theory/Compositionality.thy Wed Dec 30 21:23:38 2015 +0100 +++ b/src/HOL/HOLCF/IOA/meta_theory/Compositionality.thy Wed Dec 30 21:35:21 2015 +0100 @@ -23,7 +23,7 @@ done -(* the next two theorems are only necessary, as there is no theorem ext (A||B) = ext (B||A) *) +(* the next two theorems are only necessary, as there is no theorem ext (A\B) = ext (B\A) *) lemma compatibility_consequence4: "[|eA --> A ; eB & ~eA --> ~A|] ==> (eB | eA) --> A=eA" apply auto @@ -46,7 +46,7 @@ compatible A1 B1; compatible A2 B2; A1 =<| A2; B1 =<| B2 |] - ==> (A1 || B1) =<| (A2 || B2)" + ==> (A1 \ B1) =<| (A2 \ B2)" apply (simp add: is_asig_of_def) apply (frule_tac A1 = "A1" in compat_commute [THEN iffD1]) apply (frule_tac A1 = "A2" in compat_commute [THEN iffD1]) diff -r b66d2ca1f907 -r 89291b5d0ede src/HOL/HOLCF/IOA/meta_theory/Deadlock.thy --- a/src/HOL/HOLCF/IOA/meta_theory/Deadlock.thy Wed Dec 30 21:23:38 2015 +0100 +++ b/src/HOL/HOLCF/IOA/meta_theory/Deadlock.thy Wed Dec 30 21:35:21 2015 +0100 @@ -55,12 +55,12 @@ *} declare split_if [split del] -lemma IOA_deadlock_free: "[| a : local A; Finite sch; sch : schedules (A||B); +lemma IOA_deadlock_free: "[| a : local A; Finite sch; sch : schedules (A\B); Filter (%x. x:act A)$(sch @@ a>>nil) : schedules A; compatible A B; input_enabled B |] - ==> (sch @@ a>>nil) : schedules (A||B)" + ==> (sch @@ a>>nil) : schedules (A\B)" apply (simp add: compositionality_sch locals_def) apply (rule conjI) -(* a : act (A||B) *) +(* a : act (A\B) *) prefer 2 apply (simp add: actions_of_par) apply (blast dest: int_is_act out_is_act) diff -r b66d2ca1f907 -r 89291b5d0ede src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy --- a/src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy Wed Dec 30 21:23:38 2015 +0100 +++ b/src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy Wed Dec 30 21:35:21 2015 +0100 @@ -19,10 +19,10 @@ definition WF :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp" where - "WF A acts = (<> [] <%(s,a,t) . Enabled A acts s> .--> [] <> )" + "WF A acts = (\\<%(s,a,t) . Enabled A acts s> .--> \\)" definition SF :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp" where - "SF A acts = ([] <> <%(s,a,t) . Enabled A acts s> .--> [] <> )" + "SF A acts = (\\<%(s,a,t) . Enabled A acts s> .--> \\)" definition liveexecutions :: "('a,'s)live_ioa => ('a,'s)execution set" where diff -r b66d2ca1f907 -r 89291b5d0ede src/HOL/HOLCF/IOA/meta_theory/TL.thy --- a/src/HOL/HOLCF/IOA/meta_theory/TL.thy Wed Dec 30 21:23:38 2015 +0100 +++ b/src/HOL/HOLCF/IOA/meta_theory/TL.thy Wed Dec 30 21:35:21 2015 +0100 @@ -22,17 +22,12 @@ unlift :: "'a lift => 'a" -Init ::"'a predicate => 'a temporal" ("<_>" [0] 1000) +Init :: "'a predicate => 'a temporal" ("<_>" [0] 1000) -Box ::"'a temporal => 'a temporal" ("[] (_)" [80] 80) -Diamond ::"'a temporal => 'a temporal" ("<> (_)" [80] 80) -Next ::"'a temporal => 'a temporal" -Leadsto ::"'a temporal => 'a temporal => 'a temporal" (infixr "~>" 22) - -notation (xsymbols) - Box ("\ (_)" [80] 80) and - Diamond ("\ (_)" [80] 80) and - Leadsto (infixr "\" 22) +Box :: "'a temporal => 'a temporal" ("\ (_)" [80] 80) +Diamond :: "'a temporal => 'a temporal" ("\ (_)" [80] 80) +Next :: "'a temporal => 'a temporal" +Leadsto :: "'a temporal => 'a temporal => 'a temporal" (infixr "\" 22) defs @@ -50,37 +45,37 @@ "tsuffix s2 s == s2 ~= nil & s2 ~= UU & suffix s2 s" Box_def: - "([] P) s == ! s2. tsuffix s2 s --> P s2" + "(\P) s == ! s2. tsuffix s2 s --> P s2" Next_def: "(Next P) s == if (TL$s=UU | TL$s=nil) then (P s) else P (TL$s)" Diamond_def: - "<> P == .~ ([] (.~ P))" + "\P == .~ (\(.~ P))" Leadsto_def: - "P ~> Q == ([] (P .--> (<> Q)))" + "P \ Q == (\(P .--> (\Q)))" validT_def: "validT P == ! s. s~=UU & s~=nil --> (s |= P)" -lemma simple: "[] <> (.~ P) = (.~ <> [] P)" +lemma simple: "\\(.~ P) = (.~ \\P)" apply (rule ext) apply (simp add: Diamond_def NOT_def Box_def) done -lemma Boxnil: "nil |= [] P" +lemma Boxnil: "nil |= \P" apply (simp add: satisfies_def Box_def tsuffix_def suffix_def nil_is_Conc) done -lemma Diamondnil: "~(nil |= <> P)" +lemma Diamondnil: "~(nil |= \P)" apply (simp add: Diamond_def satisfies_def NOT_def) apply (cut_tac Boxnil) apply (simp add: satisfies_def) done -lemma Diamond_def2: "(<> F) s = (? s2. tsuffix s2 s & F s2)" +lemma Diamond_def2: "(\F) s = (? s2. tsuffix s2 s & F s2)" apply (simp add: Diamond_def NOT_def Box_def) done @@ -94,7 +89,7 @@ apply auto done -lemma reflT: "s~=UU & s~=nil --> (s |= [] F .--> F)" +lemma reflT: "s~=UU & s~=nil --> (s |= \F .--> F)" apply (simp add: satisfies_def IMPLIES_def Box_def) apply (rule impI)+ apply (erule_tac x = "s" in allE) @@ -110,7 +105,7 @@ apply (simp (no_asm) add: Conc_assoc) done -lemma transT: "s |= [] F .--> [] [] F" +lemma transT: "s |= \F .--> \\F" apply (simp (no_asm) add: satisfies_def IMPLIES_def Box_def tsuffix_def) apply auto apply (drule suffix_trans) @@ -120,14 +115,14 @@ done -lemma normalT: "s |= [] (F .--> G) .--> [] F .--> [] G" +lemma normalT: "s |= \(F .--> G) .--> \F .--> \G" apply (simp (no_asm) add: satisfies_def IMPLIES_def Box_def) done subsection "TLA Rules by Lamport" -lemma STL1a: "validT P ==> validT ([] P)" +lemma STL1a: "validT P ==> validT (\P)" apply (simp add: validT_def satisfies_def Box_def tsuffix_def) done @@ -135,13 +130,13 @@ apply (simp add: valid_def validT_def satisfies_def Init_def) done -lemma STL1: "valid P ==> validT ([] (Init P))" +lemma STL1: "valid P ==> validT (\(Init P))" apply (rule STL1a) apply (erule STL1b) done (* Note that unlift and HD is not at all used !!! *) -lemma STL4: "valid (P .--> Q) ==> validT ([] (Init P) .--> [] (Init Q))" +lemma STL4: "valid (P .--> Q) ==> validT (\(Init P) .--> \(Init Q))" apply (simp add: valid_def validT_def satisfies_def IMPLIES_def Box_def Init_def) done @@ -161,13 +156,13 @@ declare split_if [split del] lemma LTL1: - "s~=UU & s~=nil --> (s |= [] F .--> (F .& (Next ([] F))))" + "s~=UU & s~=nil --> (s |= \F .--> (F .& (Next (\F))))" apply (unfold Next_def satisfies_def NOT_def IMPLIES_def AND_def Box_def) apply auto -(* []F .--> F *) +(* \F .--> F *) apply (erule_tac x = "s" in allE) apply (simp add: tsuffix_def suffix_refl) -(* []F .--> Next [] F *) +(* \F .--> Next \F *) apply (simp split add: split_if) apply auto apply (drule tsuffix_TL2)