--- 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 \<parallel> 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 \<parallel> 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 \<parallel> 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 \<parallel> 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 \<parallel> srch_ioa \<parallel> 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 \<parallel> srch_fin_ioa \<parallel> 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 \<parallel> receiver_ioa \<parallel> srch_ioa \<parallel> 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 \<parallel> receiver_ioa \<parallel> srch_fin_ioa \<parallel> rsch_fin_ioa)"
apply (simp del: del_simps
add: compatible_def asig_of_par asig_comp_def actions_def Int_def)
apply simp
--- 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 \<parallel> receiver_ioa \<parallel> srch_ioa \<parallel> rsch_ioa)"
definition
sen :: "'m impl_state => 'm sender_state" where
--- 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 \<parallel> receiver_ioa \<parallel> srch_fin_ioa \<parallel>
rsch_fin_ioa)"
definition
--- 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 \<parallel> receiver_ioa \<parallel> srch_ioa \<parallel> 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"
--- 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 (\<diamond>\<box><%(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 (\<diamond>\<box><%(n,a,m). n~=0>)"
apply (rule AbsRuleT1)
apply (rule h_abs_is_abstraction)
apply (rule MC_result)
--- 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}) (\<diamond>\<box><%(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 (\<diamond>\<box><%(n,a,m). n~=0>)"
apply (unfold C_live_ioa_def)
apply (rule AbsRuleT2)
apply (rule h_abs_is_liveabstraction)
--- 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 (\<box>P) (\<box>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 (\<box>P) (\<box>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 (\<diamond>P) (\<diamond>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 \<leadsto> Q1) (P2 \<leadsto> 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 (\<diamond>P) (\<diamond>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 \<leadsto> Q1) (P2 \<leadsto> Q2) h"
apply (unfold Leadsto_def)
apply (rule weak_Box)
apply (erule weak_IMPLIES)
--- 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 "\<parallel>" 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 "\<parallel>" 10)
-
inductive
reachable :: "('a, 's) ioa => 's => bool"
@@ -145,7 +142,7 @@
(internals(a1) Un internals(a2))))"
par_def:
- "(A || B) ==
+ "(A \<parallel> 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 \<parallel> 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 \<parallel> 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 \<parallel> 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\<parallel>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\<parallel>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\<parallel>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\<parallel>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\<parallel>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\<parallel>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\<parallel>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\<parallel>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\<parallel>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\<parallel>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\<parallel>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\<parallel>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\<parallel>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\<parallel>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\<parallel>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\<parallel>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 \<parallel> B \<parallel> C \<parallel> 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 \<parallel>def *)
+lemma is_trans_of_par: "is_trans_of (A\<parallel>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\<parallel>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\<parallel>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\<parallel>B) C"
apply (unfold compatible_def)
apply (simp add: internals_of_par outputs_of_par actions_of_par)
apply auto
--- 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\<parallel>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\<parallel>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\<parallel>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\<parallel>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\<parallel>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\<parallel>B) (s,xs)
+ --> Forall (%x. fst x:act (A\<parallel>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\<parallel>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\<parallel>B)) xs
+ --> is_exec_frag (A\<parallel>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\<parallel>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\<parallel>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\<parallel>B) = par_execs (Execs A) (Execs B)"
apply (unfold Execs_def par_execs_def)
apply (simp add: asig_of_par)
apply (rule set_eqI)
--- 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\<parallel>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\<parallel>B) (s,xs)
+ --> Forall (%x. x:act (A\<parallel>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\<parallel>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\<parallel>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\<parallel>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\<parallel>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\<parallel>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\<parallel>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\<parallel>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\<parallel>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\<parallel>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 \<parallel> 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 \<parallel>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\<parallel>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\<parallel>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\<parallel>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\<parallel>B) = par_scheds (Scheds A) (Scheds B)"
apply (unfold Scheds_def par_scheds_def)
apply (simp add: asig_of_par)
--- 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\<parallel>B)) tr
+ --> Forall (%x. x:act (A\<parallel>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\<parallel>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\<parallel>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\<parallel>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\<parallel>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\<parallel>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\<parallel>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\<parallel>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\<parallel>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\<parallel>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\<parallel>B) = par_traces (Traces A) (Traces B)"
apply (unfold Traces_def par_traces_def)
apply (simp add: asig_of_par)
--- 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\<parallel>B) = ext (B\<parallel>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 \<parallel> B1) =<| (A2 \<parallel> 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])
--- 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\<parallel>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\<parallel>B)"
apply (simp add: compositionality_sch locals_def)
apply (rule conjI)
-(* a : act (A||B) *)
+(* a : act (A\<parallel>B) *)
prefer 2
apply (simp add: actions_of_par)
apply (blast dest: int_is_act out_is_act)
--- 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> .--> [] <> <xt2 (plift (%a. a : acts))>)"
+ "WF A acts = (\<diamond>\<box><%(s,a,t) . Enabled A acts s> .--> \<box>\<diamond><xt2 (plift (%a. a : acts))>)"
definition
SF :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp" where
- "SF A acts = ([] <> <%(s,a,t) . Enabled A acts s> .--> [] <> <xt2 (plift (%a. a : acts))>)"
+ "SF A acts = (\<box>\<diamond><%(s,a,t) . Enabled A acts s> .--> \<box>\<diamond><xt2 (plift (%a. a : acts))>)"
definition
liveexecutions :: "('a,'s)live_ioa => ('a,'s)execution set" where
--- 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 ("\<box> (_)" [80] 80) and
- Diamond ("\<diamond> (_)" [80] 80) and
- Leadsto (infixr "\<leadsto>" 22)
+Box :: "'a temporal => 'a temporal" ("\<box> (_)" [80] 80)
+Diamond :: "'a temporal => 'a temporal" ("\<diamond> (_)" [80] 80)
+Next :: "'a temporal => 'a temporal"
+Leadsto :: "'a temporal => 'a temporal => 'a temporal" (infixr "\<leadsto>" 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"
+ "(\<box>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))"
+ "\<diamond>P == .~ (\<box>(.~ P))"
Leadsto_def:
- "P ~> Q == ([] (P .--> (<> Q)))"
+ "P \<leadsto> Q == (\<box>(P .--> (\<diamond>Q)))"
validT_def:
"validT P == ! s. s~=UU & s~=nil --> (s |= P)"
-lemma simple: "[] <> (.~ P) = (.~ <> [] P)"
+lemma simple: "\<box>\<diamond>(.~ P) = (.~ \<diamond>\<box>P)"
apply (rule ext)
apply (simp add: Diamond_def NOT_def Box_def)
done
-lemma Boxnil: "nil |= [] P"
+lemma Boxnil: "nil |= \<box>P"
apply (simp add: satisfies_def Box_def tsuffix_def suffix_def nil_is_Conc)
done
-lemma Diamondnil: "~(nil |= <> P)"
+lemma Diamondnil: "~(nil |= \<diamond>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: "(\<diamond>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 |= \<box>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 |= \<box>F .--> \<box>\<box>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 |= \<box>(F .--> G) .--> \<box>F .--> \<box>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 (\<box>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 (\<box>(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 (\<box>(Init P) .--> \<box>(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 |= \<box>F .--> (F .& (Next (\<box>F))))"
apply (unfold Next_def satisfies_def NOT_def IMPLIES_def AND_def Box_def)
apply auto
-(* []F .--> F *)
+(* \<box>F .--> F *)
apply (erule_tac x = "s" in allE)
apply (simp add: tsuffix_def suffix_refl)
-(* []F .--> Next [] F *)
+(* \<box>F .--> Next \<box>F *)
apply (simp split add: split_if)
apply auto
apply (drule tsuffix_TL2)