--- a/src/HOL/HOLCF/IOA/CompoExecs.thy Mon Jul 25 14:02:29 2016 +0200
+++ b/src/HOL/HOLCF/IOA/CompoExecs.thy Mon Jul 25 21:50:04 2016 +0200
@@ -12,23 +12,23 @@
where "ProjA2 = Map (\<lambda>x. (fst x, fst (snd x)))"
definition ProjA :: "('a, 's \<times> 't) execution \<Rightarrow> ('a, 's) execution"
- where "ProjA ex = (fst (fst ex), ProjA2 $ (snd ex))"
+ where "ProjA ex = (fst (fst ex), ProjA2 \<cdot> (snd ex))"
definition ProjB2 :: "('a, 's \<times> 't) pairs \<rightarrow> ('a, 't) pairs"
where "ProjB2 = Map (\<lambda>x. (fst x, snd (snd x)))"
definition ProjB :: "('a, 's \<times> 't) execution \<Rightarrow> ('a, 't) execution"
- where "ProjB ex = (snd (fst ex), ProjB2 $ (snd ex))"
+ where "ProjB ex = (snd (fst ex), ProjB2 \<cdot> (snd ex))"
definition Filter_ex2 :: "'a signature \<Rightarrow> ('a, 's) pairs \<rightarrow> ('a, 's) pairs"
where "Filter_ex2 sig = Filter (\<lambda>x. fst x \<in> actions sig)"
definition Filter_ex :: "'a signature \<Rightarrow> ('a, 's) execution \<Rightarrow> ('a, 's) execution"
- where "Filter_ex sig ex = (fst ex, Filter_ex2 sig $ (snd ex))"
+ where "Filter_ex sig ex = (fst ex, Filter_ex2 sig \<cdot> (snd ex))"
definition stutter2 :: "'a signature \<Rightarrow> ('a, 's) pairs \<rightarrow> ('s \<Rightarrow> tr)"
where "stutter2 sig =
- (fix $
+ (fix \<cdot>
(LAM h ex.
(\<lambda>s.
case ex of
@@ -37,10 +37,10 @@
(flift1
(\<lambda>p.
(If Def (fst p \<notin> actions sig) then Def (s = snd p) else TT)
- andalso (h$xs) (snd p)) $ x))))"
+ andalso (h\<cdot>xs) (snd p)) \<cdot> x))))"
definition stutter :: "'a signature \<Rightarrow> ('a, 's) execution \<Rightarrow> bool"
- where "stutter sig ex \<longleftrightarrow> (stutter2 sig $ (snd ex)) (fst ex) \<noteq> FF"
+ where "stutter sig ex \<longleftrightarrow> (stutter2 sig \<cdot> (snd ex)) (fst ex) \<noteq> FF"
definition par_execs ::
"('a, 's) execution_module \<Rightarrow> ('a, 't) execution_module \<Rightarrow> ('a, 's \<times> 't) execution_module"
@@ -64,41 +64,41 @@
subsection \<open>\<open>ProjA2\<close>\<close>
-lemma ProjA2_UU: "ProjA2 $ UU = UU"
+lemma ProjA2_UU: "ProjA2 \<cdot> UU = UU"
by (simp add: ProjA2_def)
-lemma ProjA2_nil: "ProjA2 $ nil = nil"
+lemma ProjA2_nil: "ProjA2 \<cdot> nil = nil"
by (simp add: ProjA2_def)
-lemma ProjA2_cons: "ProjA2 $ ((a, t) \<leadsto> xs) = (a, fst t) \<leadsto> ProjA2 $ xs"
+lemma ProjA2_cons: "ProjA2 \<cdot> ((a, t) \<leadsto> xs) = (a, fst t) \<leadsto> ProjA2 \<cdot> xs"
by (simp add: ProjA2_def)
subsection \<open>\<open>ProjB2\<close>\<close>
-lemma ProjB2_UU: "ProjB2 $ UU = UU"
+lemma ProjB2_UU: "ProjB2 \<cdot> UU = UU"
by (simp add: ProjB2_def)
-lemma ProjB2_nil: "ProjB2 $ nil = nil"
+lemma ProjB2_nil: "ProjB2 \<cdot> nil = nil"
by (simp add: ProjB2_def)
-lemma ProjB2_cons: "ProjB2 $ ((a, t) \<leadsto> xs) = (a, snd t) \<leadsto> ProjB2 $ xs"
+lemma ProjB2_cons: "ProjB2 \<cdot> ((a, t) \<leadsto> xs) = (a, snd t) \<leadsto> ProjB2 \<cdot> xs"
by (simp add: ProjB2_def)
subsection \<open>\<open>Filter_ex2\<close>\<close>
-lemma Filter_ex2_UU: "Filter_ex2 sig $ UU = UU"
+lemma Filter_ex2_UU: "Filter_ex2 sig \<cdot> UU = UU"
by (simp add: Filter_ex2_def)
-lemma Filter_ex2_nil: "Filter_ex2 sig $ nil = nil"
+lemma Filter_ex2_nil: "Filter_ex2 sig \<cdot> nil = nil"
by (simp add: Filter_ex2_def)
lemma Filter_ex2_cons:
- "Filter_ex2 sig $ (at \<leadsto> xs) =
+ "Filter_ex2 sig \<cdot> (at \<leadsto> xs) =
(if fst at \<in> actions sig
- then at \<leadsto> (Filter_ex2 sig $ xs)
- else Filter_ex2 sig $ xs)"
+ then at \<leadsto> (Filter_ex2 sig \<cdot> xs)
+ else Filter_ex2 sig \<cdot> xs)"
by (simp add: Filter_ex2_def)
@@ -114,7 +114,7 @@
(flift1
(\<lambda>p.
(If Def (fst p \<notin> actions sig) then Def (s= snd p) else TT)
- andalso (stutter2 sig$xs) (snd p)) $ x)))"
+ andalso (stutter2 sig\<cdot>xs) (snd p)) \<cdot> x)))"
apply (rule trans)
apply (rule fix_eq2)
apply (simp only: stutter2_def)
@@ -122,20 +122,20 @@
apply (simp add: flift1_def)
done
-lemma stutter2_UU: "(stutter2 sig $ UU) s = UU"
+lemma stutter2_UU: "(stutter2 sig \<cdot> UU) s = UU"
apply (subst stutter2_unfold)
apply simp
done
-lemma stutter2_nil: "(stutter2 sig $ nil) s = TT"
+lemma stutter2_nil: "(stutter2 sig \<cdot> nil) s = TT"
apply (subst stutter2_unfold)
apply simp
done
lemma stutter2_cons:
- "(stutter2 sig $ (at \<leadsto> xs)) s =
+ "(stutter2 sig \<cdot> (at \<leadsto> xs)) s =
((if fst at \<notin> actions sig then Def (s = snd at) else TT)
- andalso (stutter2 sig $ xs) (snd at))"
+ andalso (stutter2 sig \<cdot> xs) (snd at))"
apply (rule trans)
apply (subst stutter2_unfold)
apply (simp add: Consq_def flift1_def If_and_if)
@@ -172,8 +172,8 @@
lemma lemma_1_1a:
\<comment> \<open>\<open>is_ex_fr\<close> propagates from \<open>A \<parallel> B\<close> to projections \<open>A\<close> and \<open>B\<close>\<close>
"\<forall>s. is_exec_frag (A \<parallel> B) (s, xs) \<longrightarrow>
- is_exec_frag A (fst s, Filter_ex2 (asig_of A) $ (ProjA2 $ xs)) \<and>
- is_exec_frag B (snd s, Filter_ex2 (asig_of B) $ (ProjB2 $ xs))"
+ is_exec_frag A (fst s, Filter_ex2 (asig_of A) \<cdot> (ProjA2 \<cdot> xs)) \<and>
+ is_exec_frag B (snd s, Filter_ex2 (asig_of B) \<cdot> (ProjB2 \<cdot> xs))"
apply (pair_induct xs simp: is_exec_frag_def)
text \<open>main case\<close>
apply (auto simp add: trans_of_defs2)
@@ -182,8 +182,8 @@
lemma lemma_1_1b:
\<comment> \<open>\<open>is_ex_fr (A \<parallel> B)\<close> implies stuttering on projections\<close>
"\<forall>s. is_exec_frag (A \<parallel> B) (s, xs) \<longrightarrow>
- stutter (asig_of A) (fst s, ProjA2 $ xs) \<and>
- stutter (asig_of B) (snd s, ProjB2 $ xs)"
+ stutter (asig_of A) (fst s, ProjA2 \<cdot> xs) \<and>
+ stutter (asig_of B) (snd s, ProjB2 \<cdot> xs)"
apply (pair_induct xs simp: stutter_def is_exec_frag_def)
text \<open>main case\<close>
apply (auto simp add: trans_of_defs2)
@@ -201,10 +201,10 @@
lemma lemma_1_2:
\<comment> \<open>\<open>ex A\<close>, \<open>exB\<close>, stuttering and forall \<open>a \<in> A \<parallel> B\<close> implies \<open>ex (A \<parallel> B)\<close>\<close>
"\<forall>s.
- is_exec_frag A (fst s, Filter_ex2 (asig_of A) $ (ProjA2 $ xs)) \<and>
- is_exec_frag B (snd s, Filter_ex2 (asig_of B) $ (ProjB2 $ xs)) \<and>
- stutter (asig_of A) (fst s, ProjA2 $ xs) \<and>
- stutter (asig_of B) (snd s, ProjB2 $ xs) \<and>
+ is_exec_frag A (fst s, Filter_ex2 (asig_of A) \<cdot> (ProjA2 \<cdot> xs)) \<and>
+ is_exec_frag B (snd s, Filter_ex2 (asig_of B) \<cdot> (ProjB2 \<cdot> xs)) \<and>
+ stutter (asig_of A) (fst s, ProjA2 \<cdot> xs) \<and>
+ stutter (asig_of B) (snd s, ProjB2 \<cdot> xs) \<and>
Forall (\<lambda>x. fst x \<in> act (A \<parallel> B)) xs \<longrightarrow>
is_exec_frag (A \<parallel> B) (s, xs)"
apply (pair_induct xs simp: Forall_def sforall_def is_exec_frag_def stutter_def)