--- a/src/HOL/HOLCF/Cfun.thy Mon Jul 25 14:02:29 2016 +0200
+++ b/src/HOL/HOLCF/Cfun.thy Mon Jul 25 21:50:04 2016 +0200
@@ -338,7 +338,7 @@
text \<open>some lemmata for functions with flat/chfin domain/range types\<close>
lemma chfin_Rep_cfunR: "chain (Y::nat => 'a::cpo->'b::chfin)
- ==> !s. ? n. (LUB i. Y i)$s = Y n$s"
+ ==> !s. ? n. (LUB i. Y i)\<cdot>s = Y n\<cdot>s"
apply (rule allI)
apply (subst contlub_cfun_fun)
apply assumption
--- a/src/HOL/HOLCF/FOCUS/Fstreams.thy Mon Jul 25 14:02:29 2016 +0200
+++ b/src/HOL/HOLCF/FOCUS/Fstreams.thy Mon Jul 25 21:50:04 2016 +0200
@@ -24,7 +24,7 @@
definition
fsmap :: "('a => 'b) => 'a fstream -> 'b fstream" where
- "fsmap f = smap$(flift2 f)"
+ "fsmap f = smap\<cdot>(flift2 f)"
definition
jth :: "nat => 'a fstream => 'a" where
@@ -51,7 +51,7 @@
fsfilter' ("(_'(C')_)" [64,63] 63)
-lemma ft_fsingleton[simp]: "ft$(<a>) = Def a"
+lemma ft_fsingleton[simp]: "ft\<cdot>(<a>) = Def a"
by (simp add: fsingleton_def2)
lemma slen_fsingleton[simp]: "#(<a>) = enat 1"
@@ -104,16 +104,16 @@
lemma last_UU[simp]:"last UU = undefined"
by (simp add: last_def jth_def enat_defs)
-lemma last_infinite[simp]:"#s = \<infinity> ==> last s = undefined"
+lemma last_infinite[simp]:"#s = \<infinity> \<Longrightarrow> last s = undefined"
by (simp add: last_def)
-lemma jth_slen_lemma1:"n <= k & enat n = #s ==> jth k s = undefined"
+lemma jth_slen_lemma1:"n \<le> k \<and> enat n = #s \<Longrightarrow> jth k s = undefined"
by (simp add: jth_def enat_defs split:enat.splits, auto)
lemma jth_UU[simp]:"jth n UU = undefined"
by (simp add: jth_def)
-lemma ext_last:"[|s ~= UU; enat (Suc n) = #s|] ==> (stream_take n$s) ooo <(last s)> = s"
+lemma ext_last:"\<lbrakk>s \<noteq> UU; enat (Suc n) = #s\<rbrakk> \<Longrightarrow> (stream_take n\<cdot>s) ooo <(last s)> = s"
apply (simp add: last_def)
apply (case_tac "#s", auto)
apply (simp add: fsingleton_def2)
@@ -154,40 +154,40 @@
apply (drule not_Undef_is_Def [THEN iffD1], auto)+
done
-lemma fstreams_take_Suc[simp]: "stream_take (Suc n)$(<a> ooo s) = <a> ooo stream_take n$s"
+lemma fstreams_take_Suc[simp]: "stream_take (Suc n)\<cdot>(<a> ooo s) = <a> ooo stream_take n\<cdot>s"
by (simp add: fsingleton_def2)
-lemma fstreams_not_empty[simp]: "<a> ooo s ~= <>"
+lemma fstreams_not_empty[simp]: "<a> ooo s \<noteq> <>"
by (simp add: fsingleton_def2)
-lemma fstreams_not_empty2[simp]: "s ooo <a> ~= <>"
+lemma fstreams_not_empty2[simp]: "s ooo <a> \<noteq> <>"
by (case_tac "s=UU", auto)
-lemma fstreams_exhaust: "x = UU | (EX a s. x = <a> ooo s)"
+lemma fstreams_exhaust: "x = UU \<or> (\<exists>a s. x = <a> ooo s)"
apply (simp add: fsingleton_def2, auto)
apply (erule contrapos_pp, auto)
apply (drule stream_exhaust_eq [THEN iffD1], auto)
apply (drule not_Undef_is_Def [THEN iffD1], auto)
done
-lemma fstreams_cases: "[| x = UU ==> P; !!a y. x = <a> ooo y ==> P |] ==> P"
+lemma fstreams_cases: "\<lbrakk>x = UU \<Longrightarrow> P; \<And>a y. x = <a> ooo y \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
by (insert fstreams_exhaust [of x], auto)
-lemma fstreams_exhaust_eq: "(x ~= UU) = (? a y. x = <a> ooo y)"
+lemma fstreams_exhaust_eq: "x \<noteq> UU \<longleftrightarrow> (\<exists>a y. x = <a> ooo y)"
apply (simp add: fsingleton_def2, auto)
apply (drule stream_exhaust_eq [THEN iffD1], auto)
apply (drule not_Undef_is_Def [THEN iffD1], auto)
done
-lemma fstreams_inject: "(<a> ooo s = <b> ooo t) = (a=b & s=t)"
+lemma fstreams_inject: "<a> ooo s = <b> ooo t \<longleftrightarrow> a = b \<and> s = t"
by (simp add: fsingleton_def2)
-lemma fstreams_prefix: "<a> ooo s << t ==> EX tt. t = <a> ooo tt & s << tt"
+lemma fstreams_prefix: "<a> ooo s << t \<Longrightarrow> \<exists>tt. t = <a> ooo tt \<and> s << tt"
apply (simp add: fsingleton_def2)
apply (insert stream_prefix [of "Def a" s t], auto)
done
-lemma fstreams_prefix': "x << <a> ooo z = (x = <> | (EX y. x = <a> ooo y & y << z))"
+lemma fstreams_prefix': "x << <a> ooo z \<longleftrightarrow> x = <> \<or> (\<exists>y. x = <a> ooo y \<and> y << z)"
apply (auto, case_tac "x=UU", auto)
apply (drule stream_exhaust_eq [THEN iffD1], auto)
apply (simp add: fsingleton_def2, auto)
@@ -195,35 +195,35 @@
apply (erule sconc_mono)
done
-lemma ft_fstreams[simp]: "ft$(<a> ooo s) = Def a"
+lemma ft_fstreams[simp]: "ft\<cdot>(<a> ooo s) = Def a"
by (simp add: fsingleton_def2)
-lemma rt_fstreams[simp]: "rt$(<a> ooo s) = s"
+lemma rt_fstreams[simp]: "rt\<cdot>(<a> ooo s) = s"
by (simp add: fsingleton_def2)
-lemma ft_eq[simp]: "(ft$s = Def a) = (EX t. s = <a> ooo t)"
+lemma ft_eq[simp]: "ft\<cdot>s = Def a \<longleftrightarrow> (\<exists>t. s = <a> ooo t)"
apply (cases s, auto)
apply (auto simp add: fsingleton_def2)
done
-lemma surjective_fstreams: "(<d> ooo y = x) = (ft$x = Def d & rt$x = y)"
+lemma surjective_fstreams: "<d> ooo y = x \<longleftrightarrow> (ft\<cdot>x = Def d \<and> rt\<cdot>x = y)"
by auto
-lemma fstreams_mono: "<a> ooo b << <a> ooo c ==> b << c"
+lemma fstreams_mono: "<a> ooo b << <a> ooo c \<Longrightarrow> b << c"
by (simp add: fsingleton_def2)
-lemma fsmap_UU[simp]: "fsmap f$UU = UU"
+lemma fsmap_UU[simp]: "fsmap f\<cdot>UU = UU"
by (simp add: fsmap_def)
-lemma fsmap_fsingleton_sconc: "fsmap f$(<x> ooo xs) = <(f x)> ooo (fsmap f$xs)"
+lemma fsmap_fsingleton_sconc: "fsmap f\<cdot>(<x> ooo xs) = <(f x)> ooo (fsmap f\<cdot>xs)"
by (simp add: fsmap_def fsingleton_def2 flift2_def)
-lemma fsmap_fsingleton[simp]: "fsmap f$(<x>) = <(f x)>"
+lemma fsmap_fsingleton[simp]: "fsmap f\<cdot>(<x>) = <(f x)>"
by (simp add: fsmap_def fsingleton_def2 flift2_def)
lemma fstreams_chain_lemma[rule_format]:
- "ALL s x y. stream_take n$(s::'a fstream) << x & x << y & y << s & x ~= y --> stream_take (Suc n)$s << y"
+ "\<forall>s x y. stream_take n\<cdot>(s::'a fstream) << x \<and> x << y \<and> y << s \<and> x \<noteq> y \<longrightarrow> stream_take (Suc n)\<cdot>s << y"
apply (induct_tac n, auto)
apply (case_tac "s=UU", auto)
apply (drule stream_exhaust_eq [THEN iffD1], auto)
@@ -244,7 +244,7 @@
apply (simp add: flat_below_iff)
done
-lemma fstreams_lub_lemma1: "[| chain Y; (LUB i. Y i) = <a> ooo s |] ==> EX j t. Y j = <a> ooo t"
+lemma fstreams_lub_lemma1: "\<lbrakk>chain Y; (LUB i. Y i) = <a> ooo s\<rbrakk> \<Longrightarrow> \<exists>j t. Y j = <a> ooo t"
apply (subgoal_tac "(LUB i. Y i) ~= UU")
apply (frule lub_eq_bottom_iff, auto)
apply (drule_tac x="i" in is_ub_thelub, auto)
@@ -252,10 +252,10 @@
done
lemma fstreams_lub1:
- "[| chain Y; (LUB i. Y i) = <a> ooo s |]
- ==> (EX j t. Y j = <a> ooo t) & (EX X. chain X & (ALL i. EX j. <a> ooo X i << Y j) & (LUB i. X i) = s)"
+ "\<lbrakk>chain Y; (LUB i. Y i) = <a> ooo s\<rbrakk>
+ \<Longrightarrow> (\<exists>j t. Y j = <a> ooo t) \<and> (\<exists>X. chain X \<and> (\<forall>i. \<exists>j. <a> ooo X i << Y j) \<and> (LUB i. X i) = s)"
apply (auto simp add: fstreams_lub_lemma1)
-apply (rule_tac x="%n. stream_take n$s" in exI, auto)
+apply (rule_tac x="\<lambda>n. stream_take n\<cdot>s" in exI, auto)
apply (induct_tac i, auto)
apply (drule fstreams_lub_lemma1, auto)
apply (rule_tac x="j" in exI, auto)
@@ -278,8 +278,8 @@
lemma lub_Pair_not_UU_lemma:
- "[| chain Y; (LUB i. Y i) = ((a::'a::flat), b); a ~= UU; b ~= UU |]
- ==> EX j c d. Y j = (c, d) & c ~= UU & d ~= UU"
+ "\<lbrakk>chain Y; (LUB i. Y i) = ((a::'a::flat), b); a \<noteq> UU; b \<noteq> UU\<rbrakk>
+ \<Longrightarrow> \<exists>j c d. Y j = (c, d) \<and> c \<noteq> UU \<and> d \<noteq> UU"
apply (frule lub_prod, clarsimp)
apply (clarsimp simp add: lub_eq_bottom_iff [where Y="\<lambda>i. fst (Y i)"])
apply (case_tac "Y i", clarsimp)
@@ -298,7 +298,7 @@
done
lemma fstreams_lub_lemma2:
- "[| chain Y; (LUB i. Y i) = (a, <m> ooo ms); (a::'a::flat) ~= UU |] ==> EX j t. Y j = (a, <m> ooo t)"
+ "\<lbrakk>chain Y; (LUB i. Y i) = (a, <m> ooo ms); (a::'a::flat) \<noteq> UU\<rbrakk> \<Longrightarrow> \<exists>j t. Y j = (a, <m> ooo t)"
apply (frule lub_Pair_not_UU_lemma, auto)
apply (drule_tac x="j" in is_ub_thelub, auto)
apply (drule ax_flat, clarsimp)
@@ -306,10 +306,10 @@
done
lemma fstreams_lub2:
- "[| chain Y; (LUB i. Y i) = (a, <m> ooo ms); (a::'a::flat) ~= UU |]
- ==> (EX j t. Y j = (a, <m> ooo t)) & (EX X. chain X & (ALL i. EX j. (a, <m> ooo X i) << Y j) & (LUB i. X i) = ms)"
+ "\<lbrakk>chain Y; (LUB i. Y i) = (a, <m> ooo ms); (a::'a::flat) \<noteq> UU\<rbrakk>
+ \<Longrightarrow> (\<exists>j t. Y j = (a, <m> ooo t)) \<and> (\<exists>X. chain X \<and> (\<forall>i. \<exists>j. (a, <m> ooo X i) << Y j) \<and> (LUB i. X i) = ms)"
apply (auto simp add: fstreams_lub_lemma2)
-apply (rule_tac x="%n. stream_take n$ms" in exI, auto)
+apply (rule_tac x="\<lambda>n. stream_take n\<cdot>ms" in exI, auto)
apply (induct_tac i, auto)
apply (drule fstreams_lub_lemma2, auto)
apply (rule_tac x="j" in exI, auto)
@@ -326,14 +326,14 @@
apply (simp add: ax_flat, auto)
apply (drule fstreams_prefix, auto)+
apply (rule sconc_mono)
-apply (subgoal_tac "tt ~= tta" "tta << ms")
+apply (subgoal_tac "tt \<noteq> tta" "tta << ms")
apply (blast intro: fstreams_chain_lemma)
apply (frule lub_prod, auto)
apply (subgoal_tac "snd (Y ja) << (LUB i. snd (Y i))", clarsimp)
apply (drule fstreams_mono, simp)
apply (rule is_ub_thelub chainI)
apply (simp add: chain_def below_prod_def)
-apply (subgoal_tac "fst (Y j) ~= fst (Y ja) | snd (Y j) ~= snd (Y ja)", simp)
+apply (subgoal_tac "fst (Y j) \<noteq> fst (Y ja) \<or> snd (Y j) \<noteq> snd (Y ja)", simp)
apply (drule ax_flat, simp)+
apply (drule prod_eqI, auto)
apply (simp add: chain_mono)
@@ -342,7 +342,7 @@
lemma cpo_cont_lemma:
- "[| monofun (f::'a::cpo => 'b::cpo); (!Y. chain Y --> f (lub(range Y)) << (LUB i. f (Y i))) |] ==> cont f"
+ "\<lbrakk>monofun (f::'a::cpo \<Rightarrow> 'b::cpo); (\<forall>Y. chain Y \<longrightarrow> f (lub(range Y)) << (LUB i. f (Y i)))\<rbrakk> \<Longrightarrow> cont f"
apply (erule contI2)
apply simp
done
--- a/src/HOL/HOLCF/IMP/HoareEx.thy Mon Jul 25 14:02:29 2016 +0200
+++ b/src/HOL/HOLCF/IMP/HoareEx.thy Mon Jul 25 21:50:04 2016 +0200
@@ -13,14 +13,14 @@
the correctness of the Hoare rule for while-loops.
\<close>
-type_synonym assn = "state => bool"
+type_synonym assn = "state \<Rightarrow> bool"
definition
- hoare_valid :: "[assn, com, assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) where
- "|= {P} c {Q} = (\<forall>s t. P s \<and> D c $(Discr s) = Def t --> Q t)"
+ hoare_valid :: "[assn, com, assn] \<Rightarrow> bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) where
+ "|= {P} c {Q} = (\<forall>s t. P s \<and> D c\<cdot>(Discr s) = Def t \<longrightarrow> Q t)"
lemma WHILE_rule_sound:
- "|= {A} c {A} ==> |= {A} WHILE b DO c {\<lambda>s. A s \<and> \<not> bval b s}"
+ "|= {A} c {A} \<Longrightarrow> |= {A} WHILE b DO c {\<lambda>s. A s \<and> \<not> bval b s}"
apply (unfold hoare_valid_def)
apply (simp (no_asm))
apply (rule fix_ind)
--- a/src/HOL/HOLCF/IOA/Abstraction.thy Mon Jul 25 14:02:29 2016 +0200
+++ b/src/HOL/HOLCF/IOA/Abstraction.thy Mon Jul 25 21:50:04 2016 +0200
@@ -11,12 +11,12 @@
default_sort type
definition cex_abs :: "('s1 \<Rightarrow> 's2) \<Rightarrow> ('a, 's1) execution \<Rightarrow> ('a, 's2) execution"
- where "cex_abs f ex = (f (fst ex), Map (\<lambda>(a, t). (a, f t)) $ (snd ex))"
+ where "cex_abs f ex = (f (fst ex), Map (\<lambda>(a, t). (a, f t)) \<cdot> (snd ex))"
text \<open>equals cex_abs on Sequences -- after ex2seq application\<close>
definition cex_absSeq ::
"('s1 \<Rightarrow> 's2) \<Rightarrow> ('a option, 's1) transition Seq \<Rightarrow> ('a option, 's2)transition Seq"
- where "cex_absSeq f = (\<lambda>s. Map (\<lambda>(s, a, t). (f s, a, f t)) $ s)"
+ where "cex_absSeq f = (\<lambda>s. Map (\<lambda>(s, a, t). (f s, a, f t)) \<cdot> s)"
definition is_abstraction :: "('s1 \<Rightarrow> 's2) \<Rightarrow> ('a, 's1) ioa \<Rightarrow> ('a, 's2) ioa \<Rightarrow> bool"
where "is_abstraction f C A \<longleftrightarrow>
@@ -161,7 +161,7 @@
that is to special Map Lemma.
\<close>
lemma traces_coincide_abs:
- "ext C = ext A \<Longrightarrow> mk_trace C $ xs = mk_trace A $ (snd (cex_abs f (s, xs)))"
+ "ext C = ext A \<Longrightarrow> mk_trace C \<cdot> xs = mk_trace A \<cdot> (snd (cex_abs f (s, xs)))"
apply (unfold cex_abs_def mk_trace_def filter_act_def)
apply simp
apply (pair_induct xs)
@@ -315,7 +315,7 @@
apply auto
apply (simp add: Mapnil)
apply (simp add: MapUU)
- apply (rule_tac x = "Map (% (s,a,t) . (h s,a, h t))$s1" in exI)
+ apply (rule_tac x = "Map (% (s,a,t) . (h s,a, h t))\<cdot>s1" in exI)
apply (simp add: Map2Finite MapConc)
done
@@ -345,7 +345,7 @@
subsubsection \<open>Next\<close>
-lemma TL_ex2seq_UU: "TL $ (ex2seq (cex_abs h ex)) = UU \<longleftrightarrow> TL $ (ex2seq ex) = UU"
+lemma TL_ex2seq_UU: "TL \<cdot> (ex2seq (cex_abs h ex)) = UU \<longleftrightarrow> TL \<cdot> (ex2seq ex) = UU"
apply (pair ex)
apply (Seq_case_simp x2)
apply (pair a)
@@ -353,7 +353,7 @@
apply (pair a)
done
-lemma TL_ex2seq_nil: "TL $ (ex2seq (cex_abs h ex)) = nil \<longleftrightarrow> TL $ (ex2seq ex) = nil"
+lemma TL_ex2seq_nil: "TL \<cdot> (ex2seq (cex_abs h ex)) = nil \<longleftrightarrow> TL \<cdot> (ex2seq ex) = nil"
apply (pair ex)
apply (Seq_case_simp x2)
apply (pair a)
@@ -363,18 +363,18 @@
(*important property of cex_absSeq: As it is a 1to1 correspondence,
properties carry over*)
-lemma cex_absSeq_TL: "cex_absSeq h (TL $ s) = TL $ (cex_absSeq h s)"
+lemma cex_absSeq_TL: "cex_absSeq h (TL \<cdot> s) = TL \<cdot> (cex_absSeq h s)"
by (simp add: MapTL cex_absSeq_def)
(* important property of ex2seq: can be shiftet, as defined "pointwise" *)
-lemma TLex2seq: "snd ex \<noteq> UU \<Longrightarrow> snd ex \<noteq> nil \<Longrightarrow> \<exists>ex'. TL$(ex2seq ex) = ex2seq ex'"
+lemma TLex2seq: "snd ex \<noteq> UU \<Longrightarrow> snd ex \<noteq> nil \<Longrightarrow> \<exists>ex'. TL\<cdot>(ex2seq ex) = ex2seq ex'"
apply (pair ex)
apply (Seq_case_simp x2)
apply (pair a)
apply auto
done
-lemma ex2seqnilTL: "TL $ (ex2seq ex) \<noteq> nil \<longleftrightarrow> snd ex \<noteq> nil \<and> snd ex \<noteq> UU"
+lemma ex2seqnilTL: "TL \<cdot> (ex2seq ex) \<noteq> nil \<longleftrightarrow> snd ex \<noteq> nil \<and> snd ex \<noteq> UU"
apply (pair ex)
apply (Seq_case_simp x2)
apply (pair a)
--- 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)
--- a/src/HOL/HOLCF/IOA/CompoScheds.thy Mon Jul 25 14:02:29 2016 +0200
+++ b/src/HOL/HOLCF/IOA/CompoScheds.thy Mon Jul 25 21:50:04 2016 +0200
@@ -11,7 +11,7 @@
definition mkex2 :: "('a, 's) ioa \<Rightarrow> ('a, 't) ioa \<Rightarrow> 'a Seq \<rightarrow>
('a, 's) pairs \<rightarrow> ('a, 't) pairs \<rightarrow> ('s \<Rightarrow> 't \<Rightarrow> ('a, 's \<times> 't) pairs)"
where "mkex2 A B =
- (fix $
+ (fix \<cdot>
(LAM h sch exA exB.
(\<lambda>s t.
case sch of
@@ -22,29 +22,29 @@
| Def y \<Rightarrow>
(if y \<in> act A then
(if y \<in> act B then
- (case HD $ exA of
+ (case HD \<cdot> exA of
UU \<Rightarrow> UU
| Def a \<Rightarrow>
- (case HD $ exB of
+ (case HD \<cdot> exB of
UU \<Rightarrow> UU
| Def b \<Rightarrow>
(y, (snd a, snd b)) \<leadsto>
- (h $ xs $ (TL $ exA) $ (TL $ exB)) (snd a) (snd b)))
+ (h \<cdot> xs \<cdot> (TL \<cdot> exA) \<cdot> (TL \<cdot> exB)) (snd a) (snd b)))
else
- (case HD $ exA of
+ (case HD \<cdot> exA of
UU \<Rightarrow> UU
- | Def a \<Rightarrow> (y, (snd a, t)) \<leadsto> (h $ xs $ (TL $ exA) $ exB) (snd a) t))
+ | Def a \<Rightarrow> (y, (snd a, t)) \<leadsto> (h \<cdot> xs \<cdot> (TL \<cdot> exA) \<cdot> exB) (snd a) t))
else
(if y \<in> act B then
- (case HD $ exB of
+ (case HD \<cdot> exB of
UU \<Rightarrow> UU
- | Def b \<Rightarrow> (y, (s, snd b)) \<leadsto> (h $ xs $ exA $ (TL $ exB)) s (snd b))
+ | Def b \<Rightarrow> (y, (s, snd b)) \<leadsto> (h \<cdot> xs \<cdot> exA \<cdot> (TL \<cdot> exB)) s (snd b))
else UU))))))"
definition mkex :: "('a, 's) ioa \<Rightarrow> ('a, 't) ioa \<Rightarrow> 'a Seq \<Rightarrow>
('a, 's) execution \<Rightarrow> ('a, 't) execution \<Rightarrow> ('a, 's \<times> 't) execution"
where "mkex A B sch exA exB =
- ((fst exA, fst exB), (mkex2 A B $ sch $ (snd exA) $ (snd exB)) (fst exA) (fst exB))"
+ ((fst exA, fst exB), (mkex2 A B \<cdot> sch \<cdot> (snd exA) \<cdot> (snd exB)) (fst exA) (fst exB))"
definition par_scheds :: "'a schedule_module \<Rightarrow> 'a schedule_module \<Rightarrow> 'a schedule_module"
where "par_scheds SchedsA SchedsB =
@@ -52,8 +52,8 @@
schA = fst SchedsA; sigA = snd SchedsA;
schB = fst SchedsB; sigB = snd SchedsB
in
- ({sch. Filter (%a. a:actions sigA)$sch : schA} \<inter>
- {sch. Filter (%a. a:actions sigB)$sch : schB} \<inter>
+ ({sch. Filter (%a. a:actions sigA)\<cdot>sch : schA} \<inter>
+ {sch. Filter (%a. a:actions sigB)\<cdot>sch : schB} \<inter>
{sch. Forall (%x. x:(actions sigA Un actions sigB)) sch},
asig_comp sigA sigB))"
@@ -72,23 +72,23 @@
| Def y \<Rightarrow>
(if y \<in> act A then
(if y \<in> act B then
- (case HD $ exA of
+ (case HD \<cdot> exA of
UU \<Rightarrow> UU
| Def a \<Rightarrow>
- (case HD $ exB of
+ (case HD \<cdot> exB of
UU \<Rightarrow> UU
| Def b \<Rightarrow>
(y, (snd a, snd b)) \<leadsto>
- (mkex2 A B $ xs $ (TL $ exA) $ (TL $ exB)) (snd a) (snd b)))
+ (mkex2 A B \<cdot> xs \<cdot> (TL \<cdot> exA) \<cdot> (TL \<cdot> exB)) (snd a) (snd b)))
else
- (case HD $ exA of
+ (case HD \<cdot> exA of
UU \<Rightarrow> UU
- | Def a \<Rightarrow> (y, (snd a, t)) \<leadsto> (mkex2 A B $ xs $ (TL $ exA) $ exB) (snd a) t))
+ | Def a \<Rightarrow> (y, (snd a, t)) \<leadsto> (mkex2 A B \<cdot> xs \<cdot> (TL \<cdot> exA) \<cdot> exB) (snd a) t))
else
(if y \<in> act B then
- (case HD $ exB of
+ (case HD \<cdot> exB of
UU \<Rightarrow> UU
- | Def b \<Rightarrow> (y, (s, snd b)) \<leadsto> (mkex2 A B $ xs $ exA $ (TL $ exB)) s (snd b))
+ | Def b \<Rightarrow> (y, (s, snd b)) \<leadsto> (mkex2 A B \<cdot> xs \<cdot> exA \<cdot> (TL \<cdot> exB)) s (snd b))
else UU)))))"
apply (rule trans)
apply (rule fix_eq2)
@@ -97,20 +97,20 @@
apply simp
done
-lemma mkex2_UU: "(mkex2 A B $ UU $ exA $ exB) s t = UU"
+lemma mkex2_UU: "(mkex2 A B \<cdot> UU \<cdot> exA \<cdot> exB) s t = UU"
apply (subst mkex2_unfold)
apply simp
done
-lemma mkex2_nil: "(mkex2 A B $ nil $ exA $ exB) s t = nil"
+lemma mkex2_nil: "(mkex2 A B \<cdot> nil \<cdot> exA \<cdot> exB) s t = nil"
apply (subst mkex2_unfold)
apply simp
done
lemma mkex2_cons_1:
- "x \<in> act A \<Longrightarrow> x \<notin> act B \<Longrightarrow> HD $ exA = Def a \<Longrightarrow>
- (mkex2 A B $ (x \<leadsto> sch) $ exA $ exB) s t =
- (x, snd a,t) \<leadsto> (mkex2 A B $ sch $ (TL $ exA) $ exB) (snd a) t"
+ "x \<in> act A \<Longrightarrow> x \<notin> act B \<Longrightarrow> HD \<cdot> exA = Def a \<Longrightarrow>
+ (mkex2 A B \<cdot> (x \<leadsto> sch) \<cdot> exA \<cdot> exB) s t =
+ (x, snd a,t) \<leadsto> (mkex2 A B \<cdot> sch \<cdot> (TL \<cdot> exA) \<cdot> exB) (snd a) t"
apply (rule trans)
apply (subst mkex2_unfold)
apply (simp add: Consq_def If_and_if)
@@ -118,9 +118,9 @@
done
lemma mkex2_cons_2:
- "x \<notin> act A \<Longrightarrow> x \<in> act B \<Longrightarrow> HD $ exB = Def b \<Longrightarrow>
- (mkex2 A B $ (x \<leadsto> sch) $ exA $ exB) s t =
- (x, s, snd b) \<leadsto> (mkex2 A B $ sch $ exA $ (TL $ exB)) s (snd b)"
+ "x \<notin> act A \<Longrightarrow> x \<in> act B \<Longrightarrow> HD \<cdot> exB = Def b \<Longrightarrow>
+ (mkex2 A B \<cdot> (x \<leadsto> sch) \<cdot> exA \<cdot> exB) s t =
+ (x, s, snd b) \<leadsto> (mkex2 A B \<cdot> sch \<cdot> exA \<cdot> (TL \<cdot> exB)) s (snd b)"
apply (rule trans)
apply (subst mkex2_unfold)
apply (simp add: Consq_def If_and_if)
@@ -128,9 +128,9 @@
done
lemma mkex2_cons_3:
- "x \<in> act A \<Longrightarrow> x \<in> act B \<Longrightarrow> HD $ exA = Def a \<Longrightarrow> HD $ exB = Def b \<Longrightarrow>
- (mkex2 A B $ (x \<leadsto> sch) $ exA $ exB) s t =
- (x, snd a,snd b) \<leadsto> (mkex2 A B $ sch $ (TL $ exA) $ (TL $ exB)) (snd a) (snd b)"
+ "x \<in> act A \<Longrightarrow> x \<in> act B \<Longrightarrow> HD \<cdot> exA = Def a \<Longrightarrow> HD \<cdot> exB = Def b \<Longrightarrow>
+ (mkex2 A B \<cdot> (x \<leadsto> sch) \<cdot> exA \<cdot> exB) s t =
+ (x, snd a,snd b) \<leadsto> (mkex2 A B \<cdot> sch \<cdot> (TL \<cdot> exA) \<cdot> (TL \<cdot> exB)) (snd a) (snd b)"
apply (rule trans)
apply (subst mkex2_unfold)
apply (simp add: Consq_def If_and_if)
@@ -190,16 +190,16 @@
lemma lemma_2_1a:
\<comment> \<open>\<open>tfilter ex\<close> and \<open>filter_act\<close> are commutative\<close>
- "filter_act $ (Filter_ex2 (asig_of A) $ xs) =
- Filter (\<lambda>a. a \<in> act A) $ (filter_act $ xs)"
+ "filter_act \<cdot> (Filter_ex2 (asig_of A) \<cdot> xs) =
+ Filter (\<lambda>a. a \<in> act A) \<cdot> (filter_act \<cdot> xs)"
apply (unfold filter_act_def Filter_ex2_def)
apply (simp add: MapFilter o_def)
done
lemma lemma_2_1b:
\<comment> \<open>State-projections do not affect \<open>filter_act\<close>\<close>
- "filter_act $ (ProjA2 $ xs) = filter_act $ xs \<and>
- filter_act $ (ProjB2 $ xs) = filter_act $ xs"
+ "filter_act \<cdot> (ProjA2 \<cdot> xs) = filter_act \<cdot> xs \<and>
+ filter_act \<cdot> (ProjB2 \<cdot> xs) = filter_act \<cdot> xs"
by (pair_induct xs)
@@ -213,7 +213,7 @@
\<close>
lemma sch_actions_in_AorB:
- "\<forall>s. is_exec_frag (A \<parallel> B) (s, xs) \<longrightarrow> Forall (\<lambda>x. x \<in> act (A \<parallel> B)) (filter_act $ xs)"
+ "\<forall>s. is_exec_frag (A \<parallel> B) (s, xs) \<longrightarrow> Forall (\<lambda>x. x \<in> act (A \<parallel> B)) (filter_act \<cdot> xs)"
apply (pair_induct xs simp: is_exec_frag_def Forall_def sforall_def)
text \<open>main case\<close>
apply auto
@@ -231,9 +231,9 @@
lemma Mapfst_mkex_is_sch:
"\<forall>exA exB s t.
Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<and>
- Filter (\<lambda>a. a \<in> act A) $ sch \<sqsubseteq> filter_act $ exA \<and>
- Filter (\<lambda>a. a \<in> act B) $ sch \<sqsubseteq> filter_act $ exB \<longrightarrow>
- filter_act $ (snd (mkex A B sch (s, exA) (t, exB))) = sch"
+ Filter (\<lambda>a. a \<in> act A) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exA \<and>
+ Filter (\<lambda>a. a \<in> act B) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exB \<longrightarrow>
+ filter_act \<cdot> (snd (mkex A B sch (s, exA) (t, exB))) = sch"
apply (Seq_induct sch simp: Filter_def Forall_def sforall_def mkex_def)
text \<open>main case: splitting into 4 cases according to \<open>a \<in> A\<close>, \<open>a \<in> B\<close>\<close>
@@ -303,15 +303,15 @@
lemma stutterA_mkex:
"\<forall>exA exB s t.
Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<and>
- Filter (\<lambda>a. a \<in> act A) $ sch \<sqsubseteq> filter_act $ exA \<and>
- Filter (\<lambda>a. a \<in> act B) $ sch \<sqsubseteq> filter_act $ exB \<longrightarrow>
- stutter (asig_of A) (s, ProjA2 $ (snd (mkex A B sch (s, exA) (t, exB))))"
+ Filter (\<lambda>a. a \<in> act A) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exA \<and>
+ Filter (\<lambda>a. a \<in> act B) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exB \<longrightarrow>
+ stutter (asig_of A) (s, ProjA2 \<cdot> (snd (mkex A B sch (s, exA) (t, exB))))"
by (mkex_induct sch exA exB)
lemma stutter_mkex_on_A:
"Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<Longrightarrow>
- Filter (\<lambda>a. a \<in> act A) $ sch \<sqsubseteq> filter_act $ (snd exA) \<Longrightarrow>
- Filter (\<lambda>a. a \<in> act B) $ sch \<sqsubseteq> filter_act $ (snd exB) \<Longrightarrow>
+ Filter (\<lambda>a. a \<in> act A) \<cdot> sch \<sqsubseteq> filter_act \<cdot> (snd exA) \<Longrightarrow>
+ Filter (\<lambda>a. a \<in> act B) \<cdot> sch \<sqsubseteq> filter_act \<cdot> (snd exB) \<Longrightarrow>
stutter (asig_of A) (ProjA (mkex A B sch exA exB))"
apply (cut_tac stutterA_mkex)
apply (simp add: stutter_def ProjA_def mkex_def)
@@ -330,16 +330,16 @@
lemma stutterB_mkex:
"\<forall>exA exB s t.
Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<and>
- Filter (\<lambda>a. a \<in> act A) $ sch \<sqsubseteq> filter_act $ exA \<and>
- Filter (\<lambda>a. a \<in> act B) $ sch \<sqsubseteq> filter_act $ exB \<longrightarrow>
- stutter (asig_of B) (t, ProjB2 $ (snd (mkex A B sch (s, exA) (t, exB))))"
+ Filter (\<lambda>a. a \<in> act A) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exA \<and>
+ Filter (\<lambda>a. a \<in> act B) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exB \<longrightarrow>
+ stutter (asig_of B) (t, ProjB2 \<cdot> (snd (mkex A B sch (s, exA) (t, exB))))"
by (mkex_induct sch exA exB)
lemma stutter_mkex_on_B:
"Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<Longrightarrow>
- Filter (\<lambda>a. a \<in> act A) $ sch \<sqsubseteq> filter_act $ (snd exA) \<Longrightarrow>
- Filter (\<lambda>a. a \<in> act B) $ sch \<sqsubseteq> filter_act $ (snd exB) \<Longrightarrow>
+ Filter (\<lambda>a. a \<in> act A) \<cdot> sch \<sqsubseteq> filter_act \<cdot> (snd exA) \<Longrightarrow>
+ Filter (\<lambda>a. a \<in> act B) \<cdot> sch \<sqsubseteq> filter_act \<cdot> (snd exB) \<Longrightarrow>
stutter (asig_of B) (ProjB (mkex A B sch exA exB))"
apply (cut_tac stutterB_mkex)
apply (simp add: stutter_def ProjB_def mkex_def)
@@ -352,36 +352,36 @@
text \<open>
Filter of \<open>mkex (sch, exA, exB)\<close> to \<open>A\<close> after projection onto \<open>A\<close> is \<open>exA\<close>,
- using \<open>zip $ (proj1 $ exA) $ (proj2 $ exA)\<close> instead of \<open>exA\<close>,
+ using \<open>zip \<cdot> (proj1 \<cdot> exA) \<cdot> (proj2 \<cdot> exA)\<close> instead of \<open>exA\<close>,
because of admissibility problems structural induction.
\<close>
lemma filter_mkex_is_exA_tmp:
"\<forall>exA exB s t.
Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<and>
- Filter (\<lambda>a. a \<in> act A) $ sch \<sqsubseteq> filter_act $ exA \<and>
- Filter (\<lambda>a. a \<in> act B) $ sch \<sqsubseteq> filter_act $ exB \<longrightarrow>
- Filter_ex2 (asig_of A) $ (ProjA2 $ (snd (mkex A B sch (s, exA) (t, exB)))) =
- Zip $ (Filter (\<lambda>a. a \<in> act A) $ sch) $ (Map snd $ exA)"
+ Filter (\<lambda>a. a \<in> act A) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exA \<and>
+ Filter (\<lambda>a. a \<in> act B) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exB \<longrightarrow>
+ Filter_ex2 (asig_of A) \<cdot> (ProjA2 \<cdot> (snd (mkex A B sch (s, exA) (t, exB)))) =
+ Zip \<cdot> (Filter (\<lambda>a. a \<in> act A) \<cdot> sch) \<cdot> (Map snd \<cdot> exA)"
by (mkex_induct sch exB exA)
text \<open>
- \<open>zip $ (proj1 $ y) $ (proj2 $ y) = y\<close> (using the lift operations)
+ \<open>zip \<cdot> (proj1 \<cdot> y) \<cdot> (proj2 \<cdot> y) = y\<close> (using the lift operations)
lemma for admissibility problems
\<close>
-lemma Zip_Map_fst_snd: "Zip $ (Map fst $ y) $ (Map snd $ y) = y"
+lemma Zip_Map_fst_snd: "Zip \<cdot> (Map fst \<cdot> y) \<cdot> (Map snd \<cdot> y) = y"
by (Seq_induct y)
text \<open>
- \<open>filter A $ sch = proj1 $ ex \<longrightarrow> zip $ (filter A $ sch) $ (proj2 $ ex) = ex\<close>
+ \<open>filter A \<cdot> sch = proj1 \<cdot> ex \<longrightarrow> zip \<cdot> (filter A \<cdot> sch) \<cdot> (proj2 \<cdot> ex) = ex\<close>
lemma for eliminating non admissible equations in assumptions
\<close>
lemma trick_against_eq_in_ass:
- "Filter (\<lambda>a. a \<in> act AB) $ sch = filter_act $ ex \<Longrightarrow>
- ex = Zip $ (Filter (\<lambda>a. a \<in> act AB) $ sch) $ (Map snd $ ex)"
+ "Filter (\<lambda>a. a \<in> act AB) \<cdot> sch = filter_act \<cdot> ex \<Longrightarrow>
+ ex = Zip \<cdot> (Filter (\<lambda>a. a \<in> act AB) \<cdot> sch) \<cdot> (Map snd \<cdot> ex)"
apply (simp add: filter_act_def)
apply (rule Zip_Map_fst_snd [symmetric])
done
@@ -393,8 +393,8 @@
lemma filter_mkex_is_exA:
"Forall (\<lambda>a. a \<in> act (A \<parallel> B)) sch \<Longrightarrow>
- Filter (\<lambda>a. a \<in> act A) $ sch = filter_act $ (snd exA) \<Longrightarrow>
- Filter (\<lambda>a. a \<in> act B) $ sch = filter_act $ (snd exB) \<Longrightarrow>
+ Filter (\<lambda>a. a \<in> act A) \<cdot> sch = filter_act \<cdot> (snd exA) \<Longrightarrow>
+ Filter (\<lambda>a. a \<in> act B) \<cdot> sch = filter_act \<cdot> (snd exB) \<Longrightarrow>
Filter_ex (asig_of A) (ProjA (mkex A B sch exA exB)) = exA"
apply (simp add: ProjA_def Filter_ex_def)
apply (pair exA)
@@ -409,17 +409,17 @@
text \<open>
Filter of \<open>mkex (sch, exA, exB)\<close> to \<open>B\<close> after projection onto \<open>B\<close> is \<open>exB\<close>
- using \<open>zip $ (proj1 $ exB) $ (proj2 $ exB)\<close> instead of \<open>exB\<close>
+ using \<open>zip \<cdot> (proj1 \<cdot> exB) \<cdot> (proj2 \<cdot> exB)\<close> instead of \<open>exB\<close>
because of admissibility problems structural induction.
\<close>
lemma filter_mkex_is_exB_tmp:
"\<forall>exA exB s t.
Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<and>
- Filter (\<lambda>a. a \<in> act A) $ sch \<sqsubseteq> filter_act $ exA \<and>
- Filter (\<lambda>a. a \<in> act B) $ sch \<sqsubseteq> filter_act $ exB \<longrightarrow>
- Filter_ex2 (asig_of B) $ (ProjB2 $ (snd (mkex A B sch (s, exA) (t, exB)))) =
- Zip $ (Filter (\<lambda>a. a \<in> act B) $ sch) $ (Map snd $ exB)"
+ Filter (\<lambda>a. a \<in> act A) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exA \<and>
+ Filter (\<lambda>a. a \<in> act B) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exB \<longrightarrow>
+ Filter_ex2 (asig_of B) \<cdot> (ProjB2 \<cdot> (snd (mkex A B sch (s, exA) (t, exB)))) =
+ Zip \<cdot> (Filter (\<lambda>a. a \<in> act B) \<cdot> sch) \<cdot> (Map snd \<cdot> exB)"
(*notice necessary change of arguments exA and exB*)
by (mkex_induct sch exA exB)
@@ -430,8 +430,8 @@
lemma filter_mkex_is_exB:
"Forall (\<lambda>a. a \<in> act (A \<parallel> B)) sch \<Longrightarrow>
- Filter (\<lambda>a. a \<in> act A) $ sch = filter_act $ (snd exA) \<Longrightarrow>
- Filter (\<lambda>a. a \<in> act B) $ sch = filter_act $ (snd exB) \<Longrightarrow>
+ Filter (\<lambda>a. a \<in> act A) \<cdot> sch = filter_act \<cdot> (snd exA) \<Longrightarrow>
+ Filter (\<lambda>a. a \<in> act B) \<cdot> sch = filter_act \<cdot> (snd exB) \<Longrightarrow>
Filter_ex (asig_of B) (ProjB (mkex A B sch exA exB)) = exB"
apply (simp add: ProjB_def Filter_ex_def)
apply (pair exA)
@@ -448,16 +448,16 @@
\<comment> \<open>\<open>mkex\<close> has only \<open>A\<close>- or \<open>B\<close>-actions\<close>
"\<forall>s t exA exB.
Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch &
- Filter (\<lambda>a. a \<in> act A) $ sch \<sqsubseteq> filter_act $ exA \<and>
- Filter (\<lambda>a. a \<in> act B) $ sch \<sqsubseteq> filter_act $ exB \<longrightarrow>
+ Filter (\<lambda>a. a \<in> act A) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exA \<and>
+ Filter (\<lambda>a. a \<in> act B) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exB \<longrightarrow>
Forall (\<lambda>x. fst x \<in> act (A \<parallel> B)) (snd (mkex A B sch (s, exA) (t, exB)))"
by (mkex_induct sch exA exB)
theorem compositionality_sch:
"sch \<in> schedules (A \<parallel> B) \<longleftrightarrow>
- Filter (\<lambda>a. a \<in> act A) $ sch \<in> schedules A \<and>
- Filter (\<lambda>a. a \<in> act B) $ sch \<in> schedules B \<and>
+ Filter (\<lambda>a. a \<in> act A) \<cdot> sch \<in> schedules A \<and>
+ Filter (\<lambda>a. a \<in> act B) \<cdot> sch \<in> schedules B \<and>
Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch"
apply (simp add: schedules_def has_schedule_def)
apply auto
--- a/src/HOL/HOLCF/IOA/CompoTraces.thy Mon Jul 25 14:02:29 2016 +0200
+++ b/src/HOL/HOLCF/IOA/CompoTraces.thy Mon Jul 25 21:50:04 2016 +0200
@@ -11,7 +11,7 @@
definition mksch ::
"('a, 's) ioa \<Rightarrow> ('a, 't) ioa \<Rightarrow> 'a Seq \<rightarrow> 'a Seq \<rightarrow> 'a Seq \<rightarrow> 'a Seq"
where "mksch A B =
- (fix $
+ (fix \<cdot>
(LAM h tr schA schB.
case tr of
nil \<Rightarrow> nil
@@ -21,17 +21,17 @@
| Def y \<Rightarrow>
(if y \<in> act A then
(if y \<in> act B then
- ((Takewhile (\<lambda>a. a \<in> int A) $ schA) @@
- (Takewhile (\<lambda>a. a \<in> int B) $ schB) @@
- (y \<leadsto> (h $ xs $ (TL $ (Dropwhile (\<lambda>a. a \<in> int A) $ schA))
- $ (TL $ (Dropwhile (\<lambda>a. a \<in> int B) $ schB)))))
+ ((Takewhile (\<lambda>a. a \<in> int A) \<cdot> schA) @@
+ (Takewhile (\<lambda>a. a \<in> int B) \<cdot> schB) @@
+ (y \<leadsto> (h \<cdot> xs \<cdot> (TL \<cdot> (Dropwhile (\<lambda>a. a \<in> int A) \<cdot> schA))
+ \<cdot> (TL \<cdot> (Dropwhile (\<lambda>a. a \<in> int B) \<cdot> schB)))))
else
- ((Takewhile (\<lambda>a. a \<in> int A) $ schA) @@
- (y \<leadsto> (h $ xs $ (TL $ (Dropwhile (\<lambda>a. a \<in> int A) $ schA)) $ schB))))
+ ((Takewhile (\<lambda>a. a \<in> int A) \<cdot> schA) @@
+ (y \<leadsto> (h \<cdot> xs \<cdot> (TL \<cdot> (Dropwhile (\<lambda>a. a \<in> int A) \<cdot> schA)) \<cdot> schB))))
else
(if y \<in> act B then
- ((Takewhile (\<lambda>a. a \<in> int B) $ schB) @@
- (y \<leadsto> (h $ xs $ schA $ (TL $ (Dropwhile (\<lambda>a. a \<in> int B) $ schB)))))
+ ((Takewhile (\<lambda>a. a \<in> int B) \<cdot> schB) @@
+ (y \<leadsto> (h \<cdot> xs \<cdot> schA \<cdot> (TL \<cdot> (Dropwhile (\<lambda>a. a \<in> int B) \<cdot> schB)))))
else UU)))))"
definition par_traces :: "'a trace_module \<Rightarrow> 'a trace_module \<Rightarrow> 'a trace_module"
@@ -40,15 +40,15 @@
trA = fst TracesA; sigA = snd TracesA;
trB = fst TracesB; sigB = snd TracesB
in
- ({tr. Filter (\<lambda>a. a \<in> actions sigA) $ tr \<in> trA} \<inter>
- {tr. Filter (\<lambda>a. a \<in> actions sigB) $ tr \<in> trB} \<inter>
+ ({tr. Filter (\<lambda>a. a \<in> actions sigA) \<cdot> tr \<in> trA} \<inter>
+ {tr. Filter (\<lambda>a. a \<in> actions sigB) \<cdot> tr \<in> trB} \<inter>
{tr. Forall (\<lambda>x. x \<in> externals sigA \<union> externals sigB) tr},
asig_comp sigA sigB))"
axiomatization where
- finiteR_mksch: "Finite (mksch A B $ tr $ x $ y) \<Longrightarrow> Finite tr"
+ finiteR_mksch: "Finite (mksch A B \<cdot> tr \<cdot> x \<cdot> y) \<Longrightarrow> Finite tr"
-lemma finiteR_mksch': "\<not> Finite tr \<Longrightarrow> \<not> Finite (mksch A B $ tr $ x $ y)"
+lemma finiteR_mksch': "\<not> Finite tr \<Longrightarrow> \<not> Finite (mksch A B \<cdot> tr \<cdot> x \<cdot> y)"
by (blast intro: finiteR_mksch)
@@ -68,17 +68,17 @@
| Def y \<Rightarrow>
(if y \<in> act A then
(if y \<in> act B then
- ((Takewhile (\<lambda>a. a \<in> int A) $ schA) @@
- (Takewhile (\<lambda>a. a \<in> int B) $ schB) @@
- (y \<leadsto> (mksch A B $ xs $(TL $ (Dropwhile (\<lambda>a. a \<in> int A) $ schA))
- $(TL $ (Dropwhile (\<lambda>a. a \<in> int B) $ schB)))))
+ ((Takewhile (\<lambda>a. a \<in> int A) \<cdot> schA) @@
+ (Takewhile (\<lambda>a. a \<in> int B) \<cdot> schB) @@
+ (y \<leadsto> (mksch A B \<cdot> xs \<cdot>(TL \<cdot> (Dropwhile (\<lambda>a. a \<in> int A) \<cdot> schA))
+ \<cdot>(TL \<cdot> (Dropwhile (\<lambda>a. a \<in> int B) \<cdot> schB)))))
else
- ((Takewhile (\<lambda>a. a \<in> int A) $ schA) @@
- (y \<leadsto> (mksch A B $ xs $ (TL $ (Dropwhile (\<lambda>a. a \<in> int A) $ schA)) $ schB))))
+ ((Takewhile (\<lambda>a. a \<in> int A) \<cdot> schA) @@
+ (y \<leadsto> (mksch A B \<cdot> xs \<cdot> (TL \<cdot> (Dropwhile (\<lambda>a. a \<in> int A) \<cdot> schA)) \<cdot> schB))))
else
(if y \<in> act B then
- ((Takewhile (\<lambda>a. a \<in> int B) $ schB) @@
- (y \<leadsto> (mksch A B $ xs $ schA $ (TL $ (Dropwhile (\<lambda>a. a \<in> int B) $ schB)))))
+ ((Takewhile (\<lambda>a. a \<in> int B) \<cdot> schB) @@
+ (y \<leadsto> (mksch A B \<cdot> xs \<cdot> schA \<cdot> (TL \<cdot> (Dropwhile (\<lambda>a. a \<in> int B) \<cdot> schB)))))
else UU))))"
apply (rule trans)
apply (rule fix_eq4)
@@ -87,21 +87,21 @@
apply simp
done
-lemma mksch_UU: "mksch A B $ UU $ schA $ schB = UU"
+lemma mksch_UU: "mksch A B \<cdot> UU \<cdot> schA \<cdot> schB = UU"
apply (subst mksch_unfold)
apply simp
done
-lemma mksch_nil: "mksch A B $ nil $ schA $ schB = nil"
+lemma mksch_nil: "mksch A B \<cdot> nil \<cdot> schA \<cdot> schB = nil"
apply (subst mksch_unfold)
apply simp
done
lemma mksch_cons1:
"x \<in> act A \<Longrightarrow> x \<notin> act B \<Longrightarrow>
- mksch A B $ (x \<leadsto> tr) $ schA $ schB =
- (Takewhile (\<lambda>a. a \<in> int A) $ schA) @@
- (x \<leadsto> (mksch A B $ tr $ (TL $ (Dropwhile (\<lambda>a. a \<in> int A) $ schA)) $ schB))"
+ mksch A B \<cdot> (x \<leadsto> tr) \<cdot> schA \<cdot> schB =
+ (Takewhile (\<lambda>a. a \<in> int A) \<cdot> schA) @@
+ (x \<leadsto> (mksch A B \<cdot> tr \<cdot> (TL \<cdot> (Dropwhile (\<lambda>a. a \<in> int A) \<cdot> schA)) \<cdot> schB))"
apply (rule trans)
apply (subst mksch_unfold)
apply (simp add: Consq_def If_and_if)
@@ -110,9 +110,9 @@
lemma mksch_cons2:
"x \<notin> act A \<Longrightarrow> x \<in> act B \<Longrightarrow>
- mksch A B $ (x \<leadsto> tr) $ schA $ schB =
- (Takewhile (\<lambda>a. a \<in> int B) $ schB) @@
- (x \<leadsto> (mksch A B $ tr $ schA $ (TL $ (Dropwhile (\<lambda>a. a \<in> int B) $ schB))))"
+ mksch A B \<cdot> (x \<leadsto> tr) \<cdot> schA \<cdot> schB =
+ (Takewhile (\<lambda>a. a \<in> int B) \<cdot> schB) @@
+ (x \<leadsto> (mksch A B \<cdot> tr \<cdot> schA \<cdot> (TL \<cdot> (Dropwhile (\<lambda>a. a \<in> int B) \<cdot> schB))))"
apply (rule trans)
apply (subst mksch_unfold)
apply (simp add: Consq_def If_and_if)
@@ -121,11 +121,11 @@
lemma mksch_cons3:
"x \<in> act A \<Longrightarrow> x \<in> act B \<Longrightarrow>
- mksch A B $ (x \<leadsto> tr) $ schA $ schB =
- (Takewhile (\<lambda>a. a \<in> int A) $ schA) @@
- ((Takewhile (\<lambda>a. a \<in> int B) $ schB) @@
- (x \<leadsto> (mksch A B $ tr $ (TL $ (Dropwhile (\<lambda>a. a \<in> int A) $ schA))
- $ (TL $ (Dropwhile (\<lambda>a. a \<in> int B) $ schB)))))"
+ mksch A B \<cdot> (x \<leadsto> tr) \<cdot> schA \<cdot> schB =
+ (Takewhile (\<lambda>a. a \<in> int A) \<cdot> schA) @@
+ ((Takewhile (\<lambda>a. a \<in> int B) \<cdot> schB) @@
+ (x \<leadsto> (mksch A B \<cdot> tr \<cdot> (TL \<cdot> (Dropwhile (\<lambda>a. a \<in> int A) \<cdot> schA))
+ \<cdot> (TL \<cdot> (Dropwhile (\<lambda>a. a \<in> int B) \<cdot> schB)))))"
apply (rule trans)
apply (subst mksch_unfold)
apply (simp add: Consq_def If_and_if)
@@ -169,7 +169,7 @@
lemma ForallAorB_mksch [rule_format]:
"compatible A B \<Longrightarrow>
\<forall>schA schB. Forall (\<lambda>x. x \<in> act (A \<parallel> B)) tr \<longrightarrow>
- Forall (\<lambda>x. x \<in> act (A \<parallel> B)) (mksch A B $ tr $ schA $ schB)"
+ Forall (\<lambda>x. x \<in> act (A \<parallel> B)) (mksch A B \<cdot> tr \<cdot> schA \<cdot> schB)"
apply (Seq_induct tr simp: Forall_def sforall_def mksch_def)
apply auto
apply (simp add: actions_of_par)
@@ -197,7 +197,7 @@
lemma ForallBnAmksch [rule_format]:
"compatible B A \<Longrightarrow>
\<forall>schA schB. Forall (\<lambda>x. x \<in> act B \<and> x \<notin> act A) tr \<longrightarrow>
- Forall (\<lambda>x. x \<in> act B \<and> x \<notin> act A) (mksch A B $ tr $ schA $ schB)"
+ Forall (\<lambda>x. x \<in> act B \<and> x \<notin> act A) (mksch A B \<cdot> tr \<cdot> schA \<cdot> schB)"
apply (Seq_induct tr simp: Forall_def sforall_def mksch_def)
apply auto
apply (rule Forall_Conc_impl [THEN mp])
@@ -207,7 +207,7 @@
lemma ForallAnBmksch [rule_format]:
"compatible A B \<Longrightarrow>
\<forall>schA schB. Forall (\<lambda>x. x \<in> act A \<and> x \<notin> act B) tr \<longrightarrow>
- Forall (\<lambda>x. x \<in> act A \<and> x \<notin> act B) (mksch A B $ tr $ schA $ schB)"
+ Forall (\<lambda>x. x \<in> act A \<and> x \<notin> act B) (mksch A B \<cdot> tr \<cdot> schA \<cdot> schB)"
apply (Seq_induct tr simp: Forall_def sforall_def mksch_def)
apply auto
apply (rule Forall_Conc_impl [THEN mp])
@@ -221,9 +221,9 @@
"Finite tr \<Longrightarrow> is_asig (asig_of A) \<Longrightarrow> is_asig (asig_of B) \<Longrightarrow>
\<forall>x y.
Forall (\<lambda>x. x \<in> act A) x \<and> Forall (\<lambda>x. x \<in> act B) y \<and>
- Filter (\<lambda>a. a \<in> ext A) $ x = Filter (\<lambda>a. a \<in> act A) $ tr \<and>
- Filter (\<lambda>a. a \<in> ext B) $ y = Filter (\<lambda>a. a \<in> act B) $ tr \<and>
- Forall (\<lambda>x. x \<in> ext (A \<parallel> B)) tr \<longrightarrow> Finite (mksch A B $ tr $ x $ y)"
+ Filter (\<lambda>a. a \<in> ext A) \<cdot> x = Filter (\<lambda>a. a \<in> act A) \<cdot> tr \<and>
+ Filter (\<lambda>a. a \<in> ext B) \<cdot> y = Filter (\<lambda>a. a \<in> act B) \<cdot> tr \<and>
+ Forall (\<lambda>x. x \<in> ext (A \<parallel> B)) tr \<longrightarrow> Finite (mksch A B \<cdot> tr \<cdot> x \<cdot> y)"
apply (erule Seq_Finite_ind)
apply simp
text \<open>main case\<close>
@@ -238,9 +238,9 @@
text \<open>\<open>Finite (tw iA x)\<close> and \<open>Finite (tw iB y)\<close>\<close>
apply (simp add: not_ext_is_int_or_not_act FiniteConc)
text \<open>now for conclusion IH applicable, but assumptions have to be transformed\<close>
- apply (drule_tac x = "x" and g = "Filter (\<lambda>a. a \<in> act A) $ s" in subst_lemma2)
+ apply (drule_tac x = "x" and g = "Filter (\<lambda>a. a \<in> act A) \<cdot> s" in subst_lemma2)
apply assumption
- apply (drule_tac x = "y" and g = "Filter (\<lambda>a. a \<in> act B) $ s" in subst_lemma2)
+ apply (drule_tac x = "y" and g = "Filter (\<lambda>a. a \<in> act B) \<cdot> s" in subst_lemma2)
apply assumption
text \<open>IH\<close>
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
@@ -252,7 +252,7 @@
text \<open>\<open>Finite (tw iB y)\<close>\<close>
apply (simp add: not_ext_is_int_or_not_act FiniteConc)
text \<open>now for conclusion IH applicable, but assumptions have to be transformed\<close>
- apply (drule_tac x = "y" and g = "Filter (\<lambda>a. a \<in> act B) $ s" in subst_lemma2)
+ apply (drule_tac x = "y" and g = "Filter (\<lambda>a. a \<in> act B) \<cdot> s" in subst_lemma2)
apply assumption
text \<open>IH\<close>
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
@@ -264,7 +264,7 @@
text \<open>\<open>Finite (tw iA x)\<close>\<close>
apply (simp add: not_ext_is_int_or_not_act FiniteConc)
text \<open>now for conclusion IH applicable, but assumptions have to be transformed\<close>
- apply (drule_tac x = "x" and g = "Filter (\<lambda>a. a \<in> act A) $ s" in subst_lemma2)
+ apply (drule_tac x = "x" and g = "Filter (\<lambda>a. a \<in> act A) \<cdot> s" in subst_lemma2)
apply assumption
text \<open>IH\<close>
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
@@ -280,12 +280,12 @@
lemma reduceA_mksch1 [rule_format]:
"Finite bs \<Longrightarrow> is_asig (asig_of A) \<Longrightarrow> is_asig (asig_of B) \<Longrightarrow> compatible A B \<Longrightarrow>
\<forall>y. Forall (\<lambda>x. x \<in> act B) y \<and> Forall (\<lambda>x. x \<in> act B \<and> x \<notin> act A) bs \<and>
- Filter (\<lambda>a. a \<in> ext B) $ y = Filter (\<lambda>a. a \<in> act B) $ (bs @@ z) \<longrightarrow>
+ Filter (\<lambda>a. a \<in> ext B) \<cdot> y = Filter (\<lambda>a. a \<in> act B) \<cdot> (bs @@ z) \<longrightarrow>
(\<exists>y1 y2.
- (mksch A B $ (bs @@ z) $ x $ y) = (y1 @@ (mksch A B $ z $ x $ y2)) \<and>
+ (mksch A B \<cdot> (bs @@ z) \<cdot> x \<cdot> y) = (y1 @@ (mksch A B \<cdot> z \<cdot> x \<cdot> y2)) \<and>
Forall (\<lambda>x. x \<in> act B \<and> x \<notin> act A) y1 \<and>
Finite y1 \<and> y = (y1 @@ y2) \<and>
- Filter (\<lambda>a. a \<in> ext B) $ y1 = bs)"
+ Filter (\<lambda>a. a \<in> ext B) \<cdot> y1 = bs)"
apply (frule_tac A1 = "A" in compat_commute [THEN iffD1])
apply (erule Seq_Finite_ind)
apply (rule allI)+
@@ -303,11 +303,11 @@
apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
apply (erule conjE)+
text \<open>transform assumption \<open>f eB y = f B (s @ z)\<close>\<close>
- apply (drule_tac x = "y" and g = "Filter (\<lambda>a. a \<in> act B) $ (s @@ z) " in subst_lemma2)
+ apply (drule_tac x = "y" and g = "Filter (\<lambda>a. a \<in> act B) \<cdot> (s @@ z) " in subst_lemma2)
apply assumption
apply (simp add: not_ext_is_int_or_not_act FilterConc)
text \<open>apply IH\<close>
- apply (erule_tac x = "TL $ (Dropwhile (\<lambda>a. a \<in> int B) $ y)" in allE)
+ apply (erule_tac x = "TL \<cdot> (Dropwhile (\<lambda>a. a \<in> int B) \<cdot> y)" in allE)
apply (simp add: ForallTL ForallDropwhile FilterConc)
apply (erule exE)+
apply (erule conjE)+
@@ -315,7 +315,7 @@
text \<open>for replacing IH in conclusion\<close>
apply (rotate_tac -2)
text \<open>instantiate \<open>y1a\<close> and \<open>y2a\<close>\<close>
- apply (rule_tac x = "Takewhile (\<lambda>a. a \<in> int B) $ y @@ a \<leadsto> y1" in exI)
+ apply (rule_tac x = "Takewhile (\<lambda>a. a \<in> int B) \<cdot> y @@ a \<leadsto> y1" in exI)
apply (rule_tac x = "y2" in exI)
text \<open>elminate all obligations up to two depending on \<open>Conc_assoc\<close>\<close>
apply (simp add: intA_is_not_actB int_is_act int_is_not_ext FilterConc)
@@ -327,12 +327,12 @@
lemma reduceB_mksch1 [rule_format]:
"Finite a_s \<Longrightarrow> is_asig (asig_of A) \<Longrightarrow> is_asig (asig_of B) \<Longrightarrow> compatible A B \<Longrightarrow>
\<forall>x. Forall (\<lambda>x. x \<in> act A) x \<and> Forall (\<lambda>x. x \<in> act A \<and> x \<notin> act B) a_s \<and>
- Filter (\<lambda>a. a \<in> ext A) $ x = Filter (\<lambda>a. a \<in> act A) $ (a_s @@ z) \<longrightarrow>
+ Filter (\<lambda>a. a \<in> ext A) \<cdot> x = Filter (\<lambda>a. a \<in> act A) \<cdot> (a_s @@ z) \<longrightarrow>
(\<exists>x1 x2.
- (mksch A B $ (a_s @@ z) $ x $ y) = (x1 @@ (mksch A B $ z $ x2 $ y)) \<and>
+ (mksch A B \<cdot> (a_s @@ z) \<cdot> x \<cdot> y) = (x1 @@ (mksch A B \<cdot> z \<cdot> x2 \<cdot> y)) \<and>
Forall (\<lambda>x. x \<in> act A \<and> x \<notin> act B) x1 \<and>
Finite x1 \<and> x = (x1 @@ x2) \<and>
- Filter (\<lambda>a. a \<in> ext A) $ x1 = a_s)"
+ Filter (\<lambda>a. a \<in> ext A) \<cdot> x1 = a_s)"
apply (frule_tac A1 = "A" in compat_commute [THEN iffD1])
apply (erule Seq_Finite_ind)
apply (rule allI)+
@@ -350,11 +350,11 @@
apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
apply (erule conjE)+
text \<open>transform assumption \<open>f eA x = f A (s @ z)\<close>\<close>
- apply (drule_tac x = "x" and g = "Filter (\<lambda>a. a \<in> act A) $ (s @@ z)" in subst_lemma2)
+ apply (drule_tac x = "x" and g = "Filter (\<lambda>a. a \<in> act A) \<cdot> (s @@ z)" in subst_lemma2)
apply assumption
apply (simp add: not_ext_is_int_or_not_act FilterConc)
text \<open>apply IH\<close>
- apply (erule_tac x = "TL $ (Dropwhile (\<lambda>a. a \<in> int A) $ x)" in allE)
+ apply (erule_tac x = "TL \<cdot> (Dropwhile (\<lambda>a. a \<in> int A) \<cdot> x)" in allE)
apply (simp add: ForallTL ForallDropwhile FilterConc)
apply (erule exE)+
apply (erule conjE)+
@@ -362,7 +362,7 @@
text \<open>for replacing IH in conclusion\<close>
apply (rotate_tac -2)
text \<open>instantiate \<open>y1a\<close> and \<open>y2a\<close>\<close>
- apply (rule_tac x = "Takewhile (\<lambda>a. a \<in> int A) $ x @@ a \<leadsto> x1" in exI)
+ apply (rule_tac x = "Takewhile (\<lambda>a. a \<in> int A) \<cdot> x @@ a \<leadsto> x1" in exI)
apply (rule_tac x = "x2" in exI)
text \<open>eliminate all obligations up to two depending on \<open>Conc_assoc\<close>\<close>
apply (simp add: intA_is_not_actB int_is_act int_is_not_ext FilterConc)
@@ -382,9 +382,9 @@
Forall (\<lambda>x. x \<in> act A) schA \<and>
Forall (\<lambda>x. x \<in> act B) schB \<and>
Forall (\<lambda>x. x \<in> ext (A \<parallel> B)) tr \<and>
- Filter (\<lambda>a. a \<in> act A) $ tr \<sqsubseteq> Filter (\<lambda>a. a \<in> ext A) $ schA \<and>
- Filter (\<lambda>a. a \<in> act B) $ tr \<sqsubseteq> Filter (\<lambda>a. a \<in> ext B) $ schB
- \<longrightarrow> Filter (\<lambda>a. a \<in> ext (A \<parallel> B)) $ (mksch A B $ tr $ schA $ schB) = tr"
+ Filter (\<lambda>a. a \<in> act A) \<cdot> tr \<sqsubseteq> Filter (\<lambda>a. a \<in> ext A) \<cdot> schA \<and>
+ Filter (\<lambda>a. a \<in> act B) \<cdot> tr \<sqsubseteq> Filter (\<lambda>a. a \<in> ext B) \<cdot> schB
+ \<longrightarrow> Filter (\<lambda>a. a \<in> ext (A \<parallel> B)) \<cdot> (mksch A B \<cdot> tr \<cdot> schA \<cdot> schB) = tr"
apply (Seq_induct tr simp: Forall_def sforall_def mksch_def)
text \<open>main case\<close>
text \<open>splitting into 4 cases according to \<open>a \<in> A\<close>, \<open>a \<in> B\<close>\<close>
@@ -436,10 +436,10 @@
Forall (\<lambda>x. x \<in> ext (A \<parallel> B)) tr \<and>
Forall (\<lambda>x. x \<in> act A) schA \<and>
Forall (\<lambda>x. x \<in> act B) schB \<and>
- Filter (\<lambda>a. a \<in> ext A) $ schA = Filter (\<lambda>a. a \<in> act A) $ tr \<and>
- Filter (\<lambda>a. a \<in> ext B) $ schB = Filter (\<lambda>a. a \<in> act B) $ tr \<and>
+ Filter (\<lambda>a. a \<in> ext A) \<cdot> schA = Filter (\<lambda>a. a \<in> act A) \<cdot> tr \<and>
+ Filter (\<lambda>a. a \<in> ext B) \<cdot> schB = Filter (\<lambda>a. a \<in> act B) \<cdot> tr \<and>
LastActExtsch A schA \<and> LastActExtsch B schB
- \<longrightarrow> Filter (\<lambda>a. a \<in> act A) $ (mksch A B $ tr $ schA $ schB) = schA"
+ \<longrightarrow> Filter (\<lambda>a. a \<in> act A) \<cdot> (mksch A B \<cdot> tr \<cdot> schA \<cdot> schB) = schA"
apply (intro strip)
apply (rule seq.take_lemma)
apply (rule mp)
@@ -509,7 +509,7 @@
text \<open>eliminate the \<open>B\<close>-only prefix\<close>
- apply (subgoal_tac "(Filter (\<lambda>a. a \<in> act A) $ y1) = nil")
+ apply (subgoal_tac "(Filter (\<lambda>a. a \<in> act A) \<cdot> y1) = nil")
apply (erule_tac [2] ForallQFilterPnil)
prefer 2 apply assumption
prefer 2 apply fast
@@ -522,7 +522,7 @@
apply (rotate_tac -2)
apply simp
- apply (subgoal_tac "Filter (\<lambda>a. a \<in> act A \<and> a \<in> ext B) $ y1 = nil")
+ apply (subgoal_tac "Filter (\<lambda>a. a \<in> act A \<and> a \<in> ext B) \<cdot> y1 = nil")
apply (rotate_tac -1)
apply simp
text \<open>eliminate introduced subgoal 2\<close>
@@ -556,7 +556,7 @@
text \<open>assumption \<open>schB\<close>\<close>
apply (simp add: ext_and_act)
text \<open>assumption \<open>schA\<close>\<close>
- apply (drule_tac x = "schA" and g = "Filter (\<lambda>a. a \<in> act A) $ rs" in subst_lemma2)
+ apply (drule_tac x = "schA" and g = "Filter (\<lambda>a. a \<in> act A) \<cdot> rs" in subst_lemma2)
apply assumption
apply (simp add: int_is_not_ext)
text \<open>assumptions concerning \<open>LastActExtsch\<close>, cannot be rewritten, as \<open>LastActExtsmalli\<close> are looping\<close>
@@ -574,7 +574,7 @@
apply (rotate_tac -2)
apply simp
- apply (subgoal_tac "Filter (\<lambda>a. a \<in> act A \<and> a \<in> ext B) $ y1 = nil")
+ apply (subgoal_tac "Filter (\<lambda>a. a \<in> act A \<and> a \<in> ext B) \<cdot> y1 = nil")
apply (rotate_tac -1)
apply simp
text \<open>eliminate introduced subgoal 2\<close>
@@ -604,7 +604,7 @@
apply (frule_tac y = "y2" in sym [THEN eq_imp_below, THEN divide_Seq])
apply (erule conjE)+
text \<open>assumption \<open>schA\<close>\<close>
- apply (drule_tac x = "schA" and g = "Filter (%a. a:act A) $rs" in subst_lemma2)
+ apply (drule_tac x = "schA" and g = "Filter (%a. a:act A) \<cdot>rs" in subst_lemma2)
apply assumption
apply (simp add: int_is_not_ext)
@@ -620,7 +620,7 @@
text \<open>now conclusion fulfills induction hypothesis, but assumptions are not all ready\<close>
text \<open>assumption \<open>schB\<close>\<close>
- apply (drule_tac x = "y2" and g = "Filter (\<lambda>a. a \<in> act B) $ rs" in subst_lemma2)
+ apply (drule_tac x = "y2" and g = "Filter (\<lambda>a. a \<in> act B) \<cdot> rs" in subst_lemma2)
apply assumption
apply (simp add: intA_is_not_actB int_is_not_ext)
@@ -654,10 +654,10 @@
Forall (\<lambda>x. x \<in> ext (A \<parallel> B)) tr \<and>
Forall (\<lambda>x. x \<in> act A) schA \<and>
Forall (\<lambda>x. x \<in> act B) schB \<and>
- Filter (\<lambda>a. a \<in> ext A) $ schA = Filter (\<lambda>a. a \<in> act A) $ tr \<and>
- Filter (\<lambda>a. a \<in> ext B) $ schB = Filter (\<lambda>a. a \<in> act B) $ tr \<and>
+ Filter (\<lambda>a. a \<in> ext A) \<cdot> schA = Filter (\<lambda>a. a \<in> act A) \<cdot> tr \<and>
+ Filter (\<lambda>a. a \<in> ext B) \<cdot> schB = Filter (\<lambda>a. a \<in> act B) \<cdot> tr \<and>
LastActExtsch A schA \<and> LastActExtsch B schB
- \<longrightarrow> Filter (\<lambda>a. a \<in> act B) $ (mksch A B $ tr $ schA $ schB) = schB"
+ \<longrightarrow> Filter (\<lambda>a. a \<in> act B) \<cdot> (mksch A B \<cdot> tr \<cdot> schA \<cdot> schB) = schB"
apply (intro strip)
apply (rule seq.take_lemma)
apply (rule mp)
@@ -726,7 +726,7 @@
text \<open>eliminate the \<open>A\<close>-only prefix\<close>
- apply (subgoal_tac "(Filter (\<lambda>a. a \<in> act B) $ x1) = nil")
+ apply (subgoal_tac "(Filter (\<lambda>a. a \<in> act B) \<cdot> x1) = nil")
apply (erule_tac [2] ForallQFilterPnil)
prefer 2 apply (assumption)
prefer 2 apply (fast)
@@ -739,7 +739,7 @@
apply (rotate_tac -2)
apply simp
- apply (subgoal_tac "Filter (\<lambda>a. a \<in> act B \<and> a \<in> ext A) $ x1 = nil")
+ apply (subgoal_tac "Filter (\<lambda>a. a \<in> act B \<and> a \<in> ext A) \<cdot> x1 = nil")
apply (rotate_tac -1)
apply simp
text \<open>eliminate introduced subgoal 2\<close>
@@ -772,7 +772,7 @@
text \<open>assumption \<open>schA\<close>\<close>
apply (simp add: ext_and_act)
text \<open>assumption \<open>schB\<close>\<close>
- apply (drule_tac x = "schB" and g = "Filter (\<lambda>a. a \<in> act B) $ rs" in subst_lemma2)
+ apply (drule_tac x = "schB" and g = "Filter (\<lambda>a. a \<in> act B) \<cdot> rs" in subst_lemma2)
apply assumption
apply (simp add: int_is_not_ext)
text \<open>assumptions concerning \<open>LastActExtsch\<close>, cannot be rewritten, as \<open>LastActExtsmalli\<close> are looping\<close>
@@ -790,7 +790,7 @@
apply (rotate_tac -2)
apply simp
- apply (subgoal_tac "Filter (\<lambda>a. a \<in> act B \<and> a \<in> ext A) $ x1 = nil")
+ apply (subgoal_tac "Filter (\<lambda>a. a \<in> act B \<and> a \<in> ext A) \<cdot> x1 = nil")
apply (rotate_tac -1)
apply simp
text \<open>eliminate introduced subgoal 2\<close>
@@ -820,7 +820,7 @@
apply (frule_tac y = "x2" in sym [THEN eq_imp_below, THEN divide_Seq])
apply (erule conjE)+
text \<open>assumption \<open>schA\<close>\<close>
- apply (drule_tac x = "schB" and g = "Filter (\<lambda>a. a \<in> act B) $ rs" in subst_lemma2)
+ apply (drule_tac x = "schB" and g = "Filter (\<lambda>a. a \<in> act B) \<cdot> rs" in subst_lemma2)
apply assumption
apply (simp add: int_is_not_ext)
@@ -836,7 +836,7 @@
text \<open>now conclusion fulfills induction hypothesis, but assumptions are not all ready\<close>
text \<open>assumption \<open>schA\<close>\<close>
- apply (drule_tac x = "x2" and g = "Filter (\<lambda>a. a \<in> act A) $ rs" in subst_lemma2)
+ apply (drule_tac x = "x2" and g = "Filter (\<lambda>a. a \<in> act A) \<cdot> rs" in subst_lemma2)
apply assumption
apply (simp add: intA_is_not_actB int_is_not_ext)
@@ -869,20 +869,20 @@
"is_trans_of A \<Longrightarrow> is_trans_of B \<Longrightarrow> compatible A B \<Longrightarrow> compatible B A \<Longrightarrow>
is_asig (asig_of A) \<Longrightarrow> is_asig (asig_of B) \<Longrightarrow>
tr \<in> traces (A \<parallel> B) \<longleftrightarrow>
- Filter (\<lambda>a. a \<in> act A) $ tr \<in> traces A \<and>
- Filter (\<lambda>a. a \<in> act B) $ tr \<in> traces B \<and>
+ Filter (\<lambda>a. a \<in> act A) \<cdot> tr \<in> traces A \<and>
+ Filter (\<lambda>a. a \<in> act B) \<cdot> tr \<in> traces B \<and>
Forall (\<lambda>x. x \<in> ext(A \<parallel> B)) tr"
apply (simp add: traces_def has_trace_def)
apply auto
text \<open>\<open>\<Longrightarrow>\<close>\<close>
text \<open>There is a schedule of \<open>A\<close>\<close>
- apply (rule_tac x = "Filter (\<lambda>a. a \<in> act A) $ sch" in bexI)
+ apply (rule_tac x = "Filter (\<lambda>a. a \<in> act A) \<cdot> sch" in bexI)
prefer 2
apply (simp add: compositionality_sch)
apply (simp add: compatibility_consequence1 externals_of_par ext1_ext2_is_not_act1)
text \<open>There is a schedule of \<open>B\<close>\<close>
- apply (rule_tac x = "Filter (\<lambda>a. a \<in> act B) $ sch" in bexI)
+ apply (rule_tac x = "Filter (\<lambda>a. a \<in> act B) \<cdot> sch" in bexI)
prefer 2
apply (simp add: compositionality_sch)
apply (simp add: compatibility_consequence2 externals_of_par ext1_ext2_is_not_act2)
@@ -907,7 +907,7 @@
apply (rename_tac h1 h2 schA schB)
text \<open>\<open>mksch\<close> is exactly the construction of \<open>trA\<parallel>B\<close> out of \<open>schA\<close>, \<open>schB\<close>, and the oracle \<open>tr\<close>,
we need here\<close>
- apply (rule_tac x = "mksch A B $ tr $ schA $ schB" in bexI)
+ apply (rule_tac x = "mksch A B \<cdot> tr \<cdot> schA \<cdot> schB" in bexI)
text \<open>External actions of mksch are just the oracle\<close>
apply (simp add: FilterA_mksch_is_tr)
--- a/src/HOL/HOLCF/IOA/Compositionality.thy Mon Jul 25 14:02:29 2016 +0200
+++ b/src/HOL/HOLCF/IOA/Compositionality.thy Mon Jul 25 21:50:04 2016 +0200
@@ -12,9 +12,9 @@
lemma Filter_actAisFilter_extA:
"compatible A B \<Longrightarrow> Forall (\<lambda>a. a \<in> ext A \<or> a \<in> ext B) tr \<Longrightarrow>
- Filter (\<lambda>a. a \<in> act A) $ tr = Filter (\<lambda>a. a \<in> ext A) $ tr"
+ Filter (\<lambda>a. a \<in> act A) \<cdot> tr = Filter (\<lambda>a. a \<in> ext A) \<cdot> tr"
apply (rule ForallPFilterQR)
- text \<open>i.e.: \<open>(\<forall>x. P x \<longrightarrow> (Q x = R x)) \<Longrightarrow> Forall P tr \<Longrightarrow> Filter Q $ tr = Filter R $ tr\<close>\<close>
+ text \<open>i.e.: \<open>(\<forall>x. P x \<longrightarrow> (Q x = R x)) \<Longrightarrow> Forall P tr \<Longrightarrow> Filter Q \<cdot> tr = Filter R \<cdot> tr\<close>\<close>
prefer 2 apply assumption
apply (rule compatibility_consequence3)
apply (simp_all add: ext_is_act ext1_ext2_is_not_act1)
@@ -31,7 +31,7 @@
lemma Filter_actAisFilter_extA2:
"compatible A B \<Longrightarrow> Forall (\<lambda>a. a \<in> ext B \<or> a \<in> ext A) tr \<Longrightarrow>
- Filter (\<lambda>a. a \<in> act A) $ tr = Filter (\<lambda>a. a \<in> ext A) $ tr"
+ Filter (\<lambda>a. a \<in> act A) \<cdot> tr = Filter (\<lambda>a. a \<in> ext A) \<cdot> tr"
apply (rule ForallPFilterQR)
prefer 2 apply (assumption)
apply (rule compatibility_consequence4)
--- a/src/HOL/HOLCF/IOA/Deadlock.thy Mon Jul 25 14:02:29 2016 +0200
+++ b/src/HOL/HOLCF/IOA/Deadlock.thy Mon Jul 25 21:50:04 2016 +0200
@@ -11,8 +11,8 @@
text \<open>Input actions may always be added to a schedule.\<close>
lemma scheds_input_enabled:
- "Filter (\<lambda>x. x \<in> act A) $ sch \<in> schedules A \<Longrightarrow> a \<in> inp A \<Longrightarrow> input_enabled A \<Longrightarrow> Finite sch
- \<Longrightarrow> Filter (\<lambda>x. x \<in> act A) $ sch @@ a \<leadsto> nil \<in> schedules A"
+ "Filter (\<lambda>x. x \<in> act A) \<cdot> sch \<in> schedules A \<Longrightarrow> a \<in> inp A \<Longrightarrow> input_enabled A \<Longrightarrow> Finite sch
+ \<Longrightarrow> Filter (\<lambda>x. x \<in> act A) \<cdot> sch @@ a \<leadsto> nil \<in> schedules A"
apply (simp add: schedules_def has_schedule_def)
apply auto
apply (frule inp_is_act)
@@ -24,7 +24,7 @@
apply (simp add: filter_act_def)
defer
apply (rule_tac [2] Map2Finite [THEN iffD1])
- apply (rule_tac [2] t = "Map fst $ ex" in subst)
+ apply (rule_tac [2] t = "Map fst \<cdot> ex" in subst)
prefer 2
apply assumption
apply (erule_tac [2] FiniteFilter)
@@ -60,7 +60,7 @@
assumes "a \<in> local A"
and "Finite sch"
and "sch \<in> schedules (A \<parallel> B)"
- and "Filter (\<lambda>x. x \<in> act A) $ (sch @@ a \<leadsto> nil) \<in> schedules A"
+ and "Filter (\<lambda>x. x \<in> act A) \<cdot> (sch @@ a \<leadsto> nil) \<in> schedules A"
and "compatible A B"
and "input_enabled B"
shows "(sch @@ a \<leadsto> nil) \<in> schedules (A \<parallel> B)"
--- a/src/HOL/HOLCF/IOA/LiveIOA.thy Mon Jul 25 14:02:29 2016 +0200
+++ b/src/HOL/HOLCF/IOA/LiveIOA.thy Mon Jul 25 21:50:04 2016 +0200
@@ -25,7 +25,7 @@
where "liveexecutions AP = {exec. exec \<in> executions (fst AP) \<and> (exec \<TTurnstile> snd AP)}"
definition livetraces :: "('a, 's) live_ioa \<Rightarrow> 'a trace set"
- where "livetraces AP = {mk_trace (fst AP) $ (snd ex) |ex. ex \<in> liveexecutions AP}"
+ where "livetraces AP = {mk_trace (fst AP) \<cdot> (snd ex) |ex. ex \<in> liveexecutions AP}"
definition live_implements :: "('a, 's1) live_ioa \<Rightarrow> ('a, 's2) live_ioa \<Rightarrow> bool"
where "live_implements CL AM \<longleftrightarrow>
--- a/src/HOL/HOLCF/IOA/RefCorrectness.thy Mon Jul 25 14:02:29 2016 +0200
+++ b/src/HOL/HOLCF/IOA/RefCorrectness.thy Mon Jul 25 21:50:04 2016 +0200
@@ -11,17 +11,17 @@
definition corresp_exC ::
"('a, 's2) ioa \<Rightarrow> ('s1 \<Rightarrow> 's2) \<Rightarrow> ('a, 's1) pairs \<rightarrow> ('s1 \<Rightarrow> ('a, 's2) pairs)"
where "corresp_exC A f =
- (fix $
+ (fix \<cdot>
(LAM h ex.
(\<lambda>s. case ex of
nil \<Rightarrow> nil
| x ## xs \<Rightarrow>
flift1 (\<lambda>pr.
- (SOME cex. move A cex (f s) (fst pr) (f (snd pr))) @@ ((h $ xs) (snd pr))) $ x)))"
+ (SOME cex. move A cex (f s) (fst pr) (f (snd pr))) @@ ((h \<cdot> xs) (snd pr))) \<cdot> x)))"
definition corresp_ex ::
"('a, 's2) ioa \<Rightarrow> ('s1 \<Rightarrow> 's2) \<Rightarrow> ('a, 's1) execution \<Rightarrow> ('a, 's2) execution"
- where "corresp_ex A f ex = (f (fst ex), (corresp_exC A f $ (snd ex)) (fst ex))"
+ where "corresp_ex A f ex = (f (fst ex), (corresp_exC A f \<cdot> (snd ex)) (fst ex))"
definition is_fair_ref_map ::
"('s1 \<Rightarrow> 's2) \<Rightarrow> ('a, 's1) ioa \<Rightarrow> ('a, 's2) ioa \<Rightarrow> bool"
@@ -82,7 +82,7 @@
| x ## xs \<Rightarrow>
(flift1 (\<lambda>pr.
(SOME cex. move A cex (f s) (fst pr) (f (snd pr))) @@
- ((corresp_exC A f $ xs) (snd pr))) $ x)))"
+ ((corresp_exC A f \<cdot> xs) (snd pr))) \<cdot> x)))"
apply (rule trans)
apply (rule fix_eq2)
apply (simp only: corresp_exC_def)
@@ -90,20 +90,20 @@
apply (simp add: flift1_def)
done
-lemma corresp_exC_UU: "(corresp_exC A f $ UU) s = UU"
+lemma corresp_exC_UU: "(corresp_exC A f \<cdot> UU) s = UU"
apply (subst corresp_exC_unfold)
apply simp
done
-lemma corresp_exC_nil: "(corresp_exC A f $ nil) s = nil"
+lemma corresp_exC_nil: "(corresp_exC A f \<cdot> nil) s = nil"
apply (subst corresp_exC_unfold)
apply simp
done
lemma corresp_exC_cons:
- "(corresp_exC A f $ (at \<leadsto> xs)) s =
+ "(corresp_exC A f \<cdot> (at \<leadsto> xs)) s =
(SOME cex. move A cex (f s) (fst at) (f (snd at))) @@
- ((corresp_exC A f $ xs) (snd at))"
+ ((corresp_exC A f \<cdot> xs) (snd at))"
apply (rule trans)
apply (subst corresp_exC_unfold)
apply (simp add: Consq_def flift1_def)
@@ -156,7 +156,7 @@
lemma move_subprop4:
"is_ref_map f C A \<Longrightarrow> reachable C s \<Longrightarrow> (s, a, t) \<in> trans_of C \<Longrightarrow>
- mk_trace A $ ((SOME x. move A x (f s) a (f t))) =
+ mk_trace A \<cdot> ((SOME x. move A x (f s) a (f t))) =
(if a \<in> ext A then a \<leadsto> nil else nil)"
apply (cut_tac move_is_move)
defer
@@ -172,7 +172,7 @@
text \<open>Lemma 1.1: Distribution of \<open>mk_trace\<close> and \<open>@@\<close>\<close>
lemma mk_traceConc:
- "mk_trace C $ (ex1 @@ ex2) = (mk_trace C $ ex1) @@ (mk_trace C $ ex2)"
+ "mk_trace C \<cdot> (ex1 @@ ex2) = (mk_trace C \<cdot> ex1) @@ (mk_trace C \<cdot> ex2)"
by (simp add: mk_trace_def filter_act_def MapConc)
@@ -181,7 +181,7 @@
lemma lemma_1:
"is_ref_map f C A \<Longrightarrow> ext C = ext A \<Longrightarrow>
\<forall>s. reachable C s \<and> is_exec_frag C (s, xs) \<longrightarrow>
- mk_trace C $ xs = mk_trace A $ (snd (corresp_ex A f (s, xs)))"
+ mk_trace C \<cdot> xs = mk_trace A \<cdot> (snd (corresp_ex A f (s, xs)))"
supply if_split [split del]
apply (unfold corresp_ex_def)
apply (pair_induct xs simp: is_exec_frag_def)
--- a/src/HOL/HOLCF/IOA/RefMappings.thy Mon Jul 25 14:02:29 2016 +0200
+++ b/src/HOL/HOLCF/IOA/RefMappings.thy Mon Jul 25 21:50:04 2016 +0200
@@ -14,7 +14,7 @@
where "move ioa ex s a t \<longleftrightarrow>
is_exec_frag ioa (s, ex) \<and> Finite ex \<and>
laststate (s, ex) = t \<and>
- mk_trace ioa $ ex = (if a \<in> ext ioa then a \<leadsto> nil else nil)"
+ mk_trace ioa \<cdot> ex = (if a \<in> ext ioa then a \<leadsto> nil else nil)"
definition is_ref_map :: "('s1 \<Rightarrow> 's2) \<Rightarrow> ('a, 's1) ioa \<Rightarrow> ('a, 's2) ioa \<Rightarrow> bool"
where "is_ref_map f C A \<longleftrightarrow>
--- a/src/HOL/HOLCF/IOA/Seq.thy Mon Jul 25 14:02:29 2016 +0200
+++ b/src/HOL/HOLCF/IOA/Seq.thy Mon Jul 25 21:50:04 2016 +0200
@@ -32,10 +32,10 @@
fixrec smap :: "('a \<rightarrow> 'b) \<rightarrow> 'a seq \<rightarrow> 'b seq"
where
- smap_nil: "smap $ f $ nil = nil"
-| smap_cons: "x \<noteq> UU \<Longrightarrow> smap $ f $ (x ## xs) = (f $ x) ## smap $ f $ xs"
+ smap_nil: "smap \<cdot> f \<cdot> nil = nil"
+| smap_cons: "x \<noteq> UU \<Longrightarrow> smap \<cdot> f \<cdot> (x ## xs) = (f \<cdot> x) ## smap \<cdot> f \<cdot> xs"
-lemma smap_UU [simp]: "smap $ f $ UU = UU"
+lemma smap_UU [simp]: "smap \<cdot> f \<cdot> UU = UU"
by fixrec_simp
@@ -43,13 +43,13 @@
fixrec sfilter :: "('a \<rightarrow> tr) \<rightarrow> 'a seq \<rightarrow> 'a seq"
where
- sfilter_nil: "sfilter $ P $ nil = nil"
+ sfilter_nil: "sfilter \<cdot> P \<cdot> nil = nil"
| sfilter_cons:
"x \<noteq> UU \<Longrightarrow>
- sfilter $ P $ (x ## xs) =
- (If P $ x then x ## (sfilter $ P $ xs) else sfilter $ P $ xs)"
+ sfilter \<cdot> P \<cdot> (x ## xs) =
+ (If P \<cdot> x then x ## (sfilter \<cdot> P \<cdot> xs) else sfilter \<cdot> P \<cdot> xs)"
-lemma sfilter_UU [simp]: "sfilter $ P $ UU = UU"
+lemma sfilter_UU [simp]: "sfilter \<cdot> P \<cdot> UU = UU"
by fixrec_simp
@@ -57,24 +57,24 @@
fixrec sforall2 :: "('a \<rightarrow> tr) \<rightarrow> 'a seq \<rightarrow> tr"
where
- sforall2_nil: "sforall2 $ P $ nil = TT"
-| sforall2_cons: "x \<noteq> UU \<Longrightarrow> sforall2 $ P $ (x ## xs) = ((P $ x) andalso sforall2 $ P $ xs)"
+ sforall2_nil: "sforall2 \<cdot> P \<cdot> nil = TT"
+| sforall2_cons: "x \<noteq> UU \<Longrightarrow> sforall2 \<cdot> P \<cdot> (x ## xs) = ((P \<cdot> x) andalso sforall2 \<cdot> P \<cdot> xs)"
-lemma sforall2_UU [simp]: "sforall2 $ P $ UU = UU"
+lemma sforall2_UU [simp]: "sforall2 \<cdot> P \<cdot> UU = UU"
by fixrec_simp
-definition "sforall P t = (sforall2 $ P $ t \<noteq> FF)"
+definition "sforall P t \<longleftrightarrow> sforall2 \<cdot> P \<cdot> t \<noteq> FF"
subsubsection \<open>\<open>stakewhile\<close>\<close>
fixrec stakewhile :: "('a \<rightarrow> tr) \<rightarrow> 'a seq \<rightarrow> 'a seq"
where
- stakewhile_nil: "stakewhile $ P $ nil = nil"
+ stakewhile_nil: "stakewhile \<cdot> P \<cdot> nil = nil"
| stakewhile_cons:
- "x \<noteq> UU \<Longrightarrow> stakewhile $ P $ (x ## xs) = (If P $ x then x ## (stakewhile $ P $ xs) else nil)"
+ "x \<noteq> UU \<Longrightarrow> stakewhile \<cdot> P \<cdot> (x ## xs) = (If P \<cdot> x then x ## (stakewhile \<cdot> P \<cdot> xs) else nil)"
-lemma stakewhile_UU [simp]: "stakewhile $ P $ UU = UU"
+lemma stakewhile_UU [simp]: "stakewhile \<cdot> P \<cdot> UU = UU"
by fixrec_simp
@@ -82,11 +82,11 @@
fixrec sdropwhile :: "('a \<rightarrow> tr) \<rightarrow> 'a seq \<rightarrow> 'a seq"
where
- sdropwhile_nil: "sdropwhile $ P $ nil = nil"
+ sdropwhile_nil: "sdropwhile \<cdot> P \<cdot> nil = nil"
| sdropwhile_cons:
- "x \<noteq> UU \<Longrightarrow> sdropwhile $ P $ (x ## xs) = (If P $ x then sdropwhile $ P $ xs else x ## xs)"
+ "x \<noteq> UU \<Longrightarrow> sdropwhile \<cdot> P \<cdot> (x ## xs) = (If P \<cdot> x then sdropwhile \<cdot> P \<cdot> xs else x ## xs)"
-lemma sdropwhile_UU [simp]: "sdropwhile $ P $ UU = UU"
+lemma sdropwhile_UU [simp]: "sdropwhile \<cdot> P \<cdot> UU = UU"
by fixrec_simp
@@ -94,10 +94,10 @@
fixrec slast :: "'a seq \<rightarrow> 'a"
where
- slast_nil: "slast $ nil = UU"
-| slast_cons: "x \<noteq> UU \<Longrightarrow> slast $ (x ## xs) = (If is_nil $ xs then x else slast $ xs)"
+ slast_nil: "slast \<cdot> nil = UU"
+| slast_cons: "x \<noteq> UU \<Longrightarrow> slast \<cdot> (x ## xs) = (If is_nil \<cdot> xs then x else slast \<cdot> xs)"
-lemma slast_UU [simp]: "slast $ UU = UU"
+lemma slast_UU [simp]: "slast \<cdot> UU = UU"
by fixrec_simp
@@ -105,11 +105,11 @@
fixrec sconc :: "'a seq \<rightarrow> 'a seq \<rightarrow> 'a seq"
where
- sconc_nil: "sconc $ nil $ y = y"
-| sconc_cons': "x \<noteq> UU \<Longrightarrow> sconc $ (x ## xs) $ y = x ## (sconc $ xs $ y)"
+ sconc_nil: "sconc \<cdot> nil \<cdot> y = y"
+| sconc_cons': "x \<noteq> UU \<Longrightarrow> sconc \<cdot> (x ## xs) \<cdot> y = x ## (sconc \<cdot> xs \<cdot> y)"
-abbreviation sconc_syn :: "'a seq => 'a seq => 'a seq" (infixr "@@" 65)
- where "xs @@ ys \<equiv> sconc $ xs $ ys"
+abbreviation sconc_syn :: "'a seq \<Rightarrow> 'a seq \<Rightarrow> 'a seq" (infixr "@@" 65)
+ where "xs @@ ys \<equiv> sconc \<cdot> xs \<cdot> ys"
lemma sconc_UU [simp]: "UU @@ y = UU"
by fixrec_simp
@@ -124,13 +124,13 @@
fixrec sflat :: "'a seq seq \<rightarrow> 'a seq"
where
- sflat_nil: "sflat $ nil = nil"
-| sflat_cons': "x \<noteq> UU \<Longrightarrow> sflat $ (x ## xs) = x @@ (sflat $ xs)"
+ sflat_nil: "sflat \<cdot> nil = nil"
+| sflat_cons': "x \<noteq> UU \<Longrightarrow> sflat \<cdot> (x ## xs) = x @@ (sflat \<cdot> xs)"
-lemma sflat_UU [simp]: "sflat $ UU = UU"
+lemma sflat_UU [simp]: "sflat \<cdot> UU = UU"
by fixrec_simp
-lemma sflat_cons [simp]: "sflat $ (x ## xs) = x @@ (sflat $ xs)"
+lemma sflat_cons [simp]: "sflat \<cdot> (x ## xs) = x @@ (sflat \<cdot> xs)"
by (cases "x = UU") simp_all
declare sflat_cons' [simp del]
@@ -140,14 +140,14 @@
fixrec szip :: "'a seq \<rightarrow> 'b seq \<rightarrow> ('a \<times> 'b) seq"
where
- szip_nil: "szip $ nil $ y = nil"
-| szip_cons_nil: "x \<noteq> UU \<Longrightarrow> szip $ (x ## xs) $ nil = UU"
-| szip_cons: "x \<noteq> UU \<Longrightarrow> y \<noteq> UU \<Longrightarrow> szip $ (x ## xs) $ (y ## ys) = (x, y) ## szip $ xs $ ys"
+ szip_nil: "szip \<cdot> nil \<cdot> y = nil"
+| szip_cons_nil: "x \<noteq> UU \<Longrightarrow> szip \<cdot> (x ## xs) \<cdot> nil = UU"
+| szip_cons: "x \<noteq> UU \<Longrightarrow> y \<noteq> UU \<Longrightarrow> szip \<cdot> (x ## xs) \<cdot> (y ## ys) = (x, y) ## szip \<cdot> xs \<cdot> ys"
-lemma szip_UU1 [simp]: "szip $ UU $ y = UU"
+lemma szip_UU1 [simp]: "szip \<cdot> UU \<cdot> y = UU"
by fixrec_simp
-lemma szip_UU2 [simp]: "x \<noteq> nil \<Longrightarrow> szip $ x $ UU = UU"
+lemma szip_UU2 [simp]: "x \<noteq> nil \<Longrightarrow> szip \<cdot> x \<cdot> UU = UU"
by (cases x) (simp_all, fixrec_simp)
@@ -166,7 +166,7 @@
"(if b then tr1 else tr2) @@ tr = (if b then tr1 @@ tr else tr2 @@ tr)"
by simp
-lemma sfiltersconc: "sfilter $ P $ (x @@ y) = (sfilter $ P $ x @@ sfilter $ P $ y)"
+lemma sfiltersconc: "sfilter \<cdot> P \<cdot> (x @@ y) = (sfilter \<cdot> P \<cdot> x @@ sfilter \<cdot> P \<cdot> y)"
apply (induct x)
text \<open>adm\<close>
apply simp
@@ -174,13 +174,13 @@
apply simp
apply simp
text \<open>main case\<close>
- apply (rule_tac p = "P$a" in trE)
+ apply (rule_tac p = "P\<cdot>a" in trE)
apply simp
apply simp
apply simp
done
-lemma sforallPstakewhileP: "sforall P (stakewhile $ P $ x)"
+lemma sforallPstakewhileP: "sforall P (stakewhile \<cdot> P \<cdot> x)"
apply (simp add: sforall_def)
apply (induct x)
text \<open>adm\<close>
@@ -189,13 +189,13 @@
apply simp
apply simp
text \<open>main case\<close>
- apply (rule_tac p = "P$a" in trE)
+ apply (rule_tac p = "P\<cdot>a" in trE)
apply simp
apply simp
apply simp
done
-lemma forallPsfilterP: "sforall P (sfilter $ P $ x)"
+lemma forallPsfilterP: "sforall P (sfilter \<cdot> P \<cdot> x)"
apply (simp add: sforall_def)
apply (induct x)
text \<open>adm\<close>
@@ -204,7 +204,7 @@
apply simp
apply simp
text \<open>main case\<close>
- apply (rule_tac p="P$a" in trE)
+ apply (rule_tac p="P\<cdot>a" in trE)
apply simp
apply simp
apply simp
@@ -260,7 +260,7 @@
text \<open>Extensions to Induction Theorems.\<close>
lemma seq_finite_ind_lemma:
- assumes "\<And>n. P (seq_take n $ s)"
+ assumes "\<And>n. P (seq_take n \<cdot> s)"
shows "seq_finite s \<longrightarrow> P s"
apply (unfold seq.finite_def)
apply (intro strip)
--- a/src/HOL/HOLCF/IOA/Sequence.thy Mon Jul 25 14:02:29 2016 +0200
+++ b/src/HOL/HOLCF/IOA/Sequence.thy Mon Jul 25 21:50:04 2016 +0200
@@ -16,10 +16,10 @@
where "Consq a = (LAM s. Def a ## s)"
definition Filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Seq \<rightarrow> 'a Seq"
- where "Filter P = sfilter $ (flift2 P)"
+ where "Filter P = sfilter \<cdot> (flift2 P)"
definition Map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a Seq \<rightarrow> 'b Seq"
- where "Map f = smap $ (flift2 f)"
+ where "Map f = smap \<cdot> (flift2 f)"
definition Forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Seq \<Rightarrow> bool"
where "Forall P = sforall (flift2 P)"
@@ -28,14 +28,14 @@
where "Last = slast"
definition Dropwhile :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Seq \<rightarrow> 'a Seq"
- where "Dropwhile P = sdropwhile $ (flift2 P)"
+ where "Dropwhile P = sdropwhile \<cdot> (flift2 P)"
definition Takewhile :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Seq \<rightarrow> 'a Seq"
- where "Takewhile P = stakewhile $ (flift2 P)"
+ where "Takewhile P = stakewhile \<cdot> (flift2 P)"
definition Zip :: "'a Seq \<rightarrow> 'b Seq \<rightarrow> ('a * 'b) Seq"
where "Zip =
- (fix $ (LAM h t1 t2.
+ (fix \<cdot> (LAM h t1 t2.
case t1 of
nil \<Rightarrow> nil
| x ## xs \<Rightarrow>
@@ -47,24 +47,24 @@
| Def a \<Rightarrow>
(case y of
UU \<Rightarrow> UU
- | Def b \<Rightarrow> Def (a, b) ## (h $ xs $ ys))))))"
+ | Def b \<Rightarrow> Def (a, b) ## (h \<cdot> xs \<cdot> ys))))))"
definition Flat :: "'a Seq seq \<rightarrow> 'a Seq"
where "Flat = sflat"
definition Filter2 :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Seq \<rightarrow> 'a Seq"
where "Filter2 P =
- (fix $
+ (fix \<cdot>
(LAM h t.
case t of
nil \<Rightarrow> nil
| x ## xs \<Rightarrow>
(case x of
UU \<Rightarrow> UU
- | Def y \<Rightarrow> (if P y then x ## (h $ xs) else h $ xs))))"
+ | Def y \<Rightarrow> (if P y then x ## (h \<cdot> xs) else h \<cdot> xs))))"
abbreviation Consq_syn ("(_/\<leadsto>_)" [66, 65] 65)
- where "a \<leadsto> s \<equiv> Consq a $ s"
+ where "a \<leadsto> s \<equiv> Consq a \<cdot> s"
subsection \<open>List enumeration\<close>
@@ -87,25 +87,25 @@
subsubsection \<open>Map\<close>
-lemma Map_UU: "Map f $ UU = UU"
+lemma Map_UU: "Map f \<cdot> UU = UU"
by (simp add: Map_def)
-lemma Map_nil: "Map f $ nil = nil"
+lemma Map_nil: "Map f \<cdot> nil = nil"
by (simp add: Map_def)
-lemma Map_cons: "Map f $ (x \<leadsto> xs) = (f x) \<leadsto> Map f $ xs"
+lemma Map_cons: "Map f \<cdot> (x \<leadsto> xs) = (f x) \<leadsto> Map f \<cdot> xs"
by (simp add: Map_def Consq_def flift2_def)
subsubsection \<open>Filter\<close>
-lemma Filter_UU: "Filter P $ UU = UU"
+lemma Filter_UU: "Filter P \<cdot> UU = UU"
by (simp add: Filter_def)
-lemma Filter_nil: "Filter P $ nil = nil"
+lemma Filter_nil: "Filter P \<cdot> nil = nil"
by (simp add: Filter_def)
-lemma Filter_cons: "Filter P $ (x \<leadsto> xs) = (if P x then x \<leadsto> (Filter P $ xs) else Filter P $ xs)"
+lemma Filter_cons: "Filter P \<cdot> (x \<leadsto> xs) = (if P x then x \<leadsto> (Filter P \<cdot> xs) else Filter P \<cdot> xs)"
by (simp add: Filter_def Consq_def flift2_def If_and_if)
@@ -129,50 +129,50 @@
subsubsection \<open>Takewhile\<close>
-lemma Takewhile_UU: "Takewhile P $ UU = UU"
+lemma Takewhile_UU: "Takewhile P \<cdot> UU = UU"
by (simp add: Takewhile_def)
-lemma Takewhile_nil: "Takewhile P $ nil = nil"
+lemma Takewhile_nil: "Takewhile P \<cdot> nil = nil"
by (simp add: Takewhile_def)
lemma Takewhile_cons:
- "Takewhile P $ (x \<leadsto> xs) = (if P x then x \<leadsto> (Takewhile P $ xs) else nil)"
+ "Takewhile P \<cdot> (x \<leadsto> xs) = (if P x then x \<leadsto> (Takewhile P \<cdot> xs) else nil)"
by (simp add: Takewhile_def Consq_def flift2_def If_and_if)
subsubsection \<open>DropWhile\<close>
-lemma Dropwhile_UU: "Dropwhile P $ UU = UU"
+lemma Dropwhile_UU: "Dropwhile P \<cdot> UU = UU"
by (simp add: Dropwhile_def)
-lemma Dropwhile_nil: "Dropwhile P $ nil = nil"
+lemma Dropwhile_nil: "Dropwhile P \<cdot> nil = nil"
by (simp add: Dropwhile_def)
-lemma Dropwhile_cons: "Dropwhile P $ (x \<leadsto> xs) = (if P x then Dropwhile P $ xs else x \<leadsto> xs)"
+lemma Dropwhile_cons: "Dropwhile P \<cdot> (x \<leadsto> xs) = (if P x then Dropwhile P \<cdot> xs else x \<leadsto> xs)"
by (simp add: Dropwhile_def Consq_def flift2_def If_and_if)
subsubsection \<open>Last\<close>
-lemma Last_UU: "Last $ UU =UU"
+lemma Last_UU: "Last \<cdot> UU = UU"
by (simp add: Last_def)
-lemma Last_nil: "Last $ nil =UU"
+lemma Last_nil: "Last \<cdot> nil = UU"
by (simp add: Last_def)
-lemma Last_cons: "Last $ (x \<leadsto> xs) = (if xs = nil then Def x else Last $ xs)"
+lemma Last_cons: "Last \<cdot> (x \<leadsto> xs) = (if xs = nil then Def x else Last \<cdot> xs)"
by (cases xs) (simp_all add: Last_def Consq_def)
subsubsection \<open>Flat\<close>
-lemma Flat_UU: "Flat $ UU = UU"
+lemma Flat_UU: "Flat \<cdot> UU = UU"
by (simp add: Flat_def)
-lemma Flat_nil: "Flat $ nil = nil"
+lemma Flat_nil: "Flat \<cdot> nil = nil"
by (simp add: Flat_def)
-lemma Flat_cons: "Flat $ (x ## xs) = x @@ (Flat $ xs)"
+lemma Flat_cons: "Flat \<cdot> (x ## xs) = x @@ (Flat \<cdot> xs)"
by (simp add: Flat_def Consq_def)
@@ -192,7 +192,7 @@
| Def a \<Rightarrow>
(case y of
UU \<Rightarrow> UU
- | Def b \<Rightarrow> Def (a, b) ## (Zip $ xs $ ys)))))"
+ | Def b \<Rightarrow> Def (a, b) ## (Zip \<cdot> xs \<cdot> ys)))))"
apply (rule trans)
apply (rule fix_eq4)
apply (rule Zip_def)
@@ -200,29 +200,29 @@
apply simp
done
-lemma Zip_UU1: "Zip $ UU $ y = UU"
+lemma Zip_UU1: "Zip \<cdot> UU \<cdot> y = UU"
apply (subst Zip_unfold)
apply simp
done
-lemma Zip_UU2: "x \<noteq> nil \<Longrightarrow> Zip $ x $ UU = UU"
+lemma Zip_UU2: "x \<noteq> nil \<Longrightarrow> Zip \<cdot> x \<cdot> UU = UU"
apply (subst Zip_unfold)
apply simp
apply (cases x)
apply simp_all
done
-lemma Zip_nil: "Zip $ nil $ y = nil"
+lemma Zip_nil: "Zip \<cdot> nil \<cdot> y = nil"
apply (subst Zip_unfold)
apply simp
done
-lemma Zip_cons_nil: "Zip $ (x \<leadsto> xs) $ nil = UU"
+lemma Zip_cons_nil: "Zip \<cdot> (x \<leadsto> xs) \<cdot> nil = UU"
apply (subst Zip_unfold)
apply (simp add: Consq_def)
done
-lemma Zip_cons: "Zip $ (x \<leadsto> xs) $ (y \<leadsto> ys) = (x, y) \<leadsto> Zip $ xs $ ys"
+lemma Zip_cons: "Zip \<cdot> (x \<leadsto> xs) \<cdot> (y \<leadsto> ys) = (x, y) \<leadsto> Zip \<cdot> xs \<cdot> ys"
apply (rule trans)
apply (subst Zip_unfold)
apply simp
@@ -298,7 +298,7 @@
lemma Cons_inject_less_eq: "a \<leadsto> s \<sqsubseteq> b \<leadsto> t \<longleftrightarrow> a = b \<and> s \<sqsubseteq> t"
by (simp add: Consq_def2)
-lemma seq_take_Cons: "seq_take (Suc n) $ (a \<leadsto> x) = a \<leadsto> (seq_take n $ x)"
+lemma seq_take_Cons: "seq_take (Suc n) \<cdot> (a \<leadsto> x) = a \<leadsto> (seq_take n \<cdot> x)"
by (simp add: Consq_def)
lemmas [simp] =
@@ -345,10 +345,10 @@
subsection \<open>\<open>HD\<close> and \<open>TL\<close>\<close>
-lemma HD_Cons [simp]: "HD $ (x \<leadsto> y) = Def x"
+lemma HD_Cons [simp]: "HD \<cdot> (x \<leadsto> y) = Def x"
by (simp add: Consq_def)
-lemma TL_Cons [simp]: "TL $ (x \<leadsto> y) = y"
+lemma TL_Cons [simp]: "TL \<cdot> (x \<leadsto> y) = y"
by (simp add: Consq_def)
@@ -382,12 +382,12 @@
done
-lemma FiniteMap1: "Finite s \<Longrightarrow> Finite (Map f $ s)"
+lemma FiniteMap1: "Finite s \<Longrightarrow> Finite (Map f \<cdot> s)"
apply (erule Seq_Finite_ind)
apply simp_all
done
-lemma FiniteMap2: "Finite s \<Longrightarrow> \<forall>t. s = Map f $ t \<longrightarrow> Finite t"
+lemma FiniteMap2: "Finite s \<Longrightarrow> \<forall>t. s = Map f \<cdot> t \<longrightarrow> Finite t"
apply (erule Seq_Finite_ind)
apply (intro strip)
apply (rule_tac x="t" in Seq_cases, simp_all)
@@ -396,7 +396,7 @@
apply (rule_tac x="t" in Seq_cases, simp_all)
done
-lemma Map2Finite: "Finite (Map f $ s) = Finite s"
+lemma Map2Finite: "Finite (Map f \<cdot> s) = Finite s"
apply auto
apply (erule FiniteMap2 [rule_format])
apply (rule refl)
@@ -404,7 +404,7 @@
done
-lemma FiniteFilter: "Finite s \<Longrightarrow> Finite (Filter P $ s)"
+lemma FiniteFilter: "Finite s \<Longrightarrow> Finite (Filter P \<cdot> s)"
apply (erule Seq_Finite_ind)
apply simp_all
done
@@ -445,37 +445,37 @@
subsection \<open>Last\<close>
-lemma Finite_Last1: "Finite s \<Longrightarrow> s \<noteq> nil \<longrightarrow> Last $ s \<noteq> UU"
+lemma Finite_Last1: "Finite s \<Longrightarrow> s \<noteq> nil \<longrightarrow> Last \<cdot> s \<noteq> UU"
by (erule Seq_Finite_ind) simp_all
-lemma Finite_Last2: "Finite s \<Longrightarrow> Last $ s = UU \<longrightarrow> s = nil"
+lemma Finite_Last2: "Finite s \<Longrightarrow> Last \<cdot> s = UU \<longrightarrow> s = nil"
by (erule Seq_Finite_ind) auto
subsection \<open>Filter, Conc\<close>
-lemma FilterPQ: "Filter P $ (Filter Q $ s) = Filter (\<lambda>x. P x \<and> Q x) $ s"
+lemma FilterPQ: "Filter P \<cdot> (Filter Q \<cdot> s) = Filter (\<lambda>x. P x \<and> Q x) \<cdot> s"
by (rule_tac x="s" in Seq_induct) simp_all
-lemma FilterConc: "Filter P $ (x @@ y) = (Filter P $ x @@ Filter P $ y)"
+lemma FilterConc: "Filter P \<cdot> (x @@ y) = (Filter P \<cdot> x @@ Filter P \<cdot> y)"
by (simp add: Filter_def sfiltersconc)
subsection \<open>Map\<close>
-lemma MapMap: "Map f $ (Map g $ s) = Map (f \<circ> g) $ s"
+lemma MapMap: "Map f \<cdot> (Map g \<cdot> s) = Map (f \<circ> g) \<cdot> s"
by (rule_tac x="s" in Seq_induct) simp_all
-lemma MapConc: "Map f $ (x @@ y) = (Map f $ x) @@ (Map f $ y)"
+lemma MapConc: "Map f \<cdot> (x @@ y) = (Map f \<cdot> x) @@ (Map f \<cdot> y)"
by (rule_tac x="x" in Seq_induct) simp_all
-lemma MapFilter: "Filter P $ (Map f $ x) = Map f $ (Filter (P \<circ> f) $ x)"
+lemma MapFilter: "Filter P \<cdot> (Map f \<cdot> x) = Map f \<cdot> (Filter (P \<circ> f) \<cdot> x)"
by (rule_tac x="x" in Seq_induct) simp_all
-lemma nilMap: "nil = (Map f $ s) \<longrightarrow> s = nil"
+lemma nilMap: "nil = (Map f \<cdot> s) \<longrightarrow> s = nil"
by (rule_tac x="s" in Seq_cases) simp_all
-lemma ForallMap: "Forall P (Map f $ s) = Forall (P \<circ> f) s"
+lemma ForallMap: "Forall P (Map f \<cdot> s) = Forall (P \<circ> f) s"
apply (rule_tac x="s" in Seq_induct)
apply (simp add: Forall_def sforall_def)
apply simp_all
@@ -502,7 +502,7 @@
lemma Forall_Conc [simp]: "Finite x \<Longrightarrow> Forall P (x @@ y) \<longleftrightarrow> Forall P x \<and> Forall P y"
by (erule Seq_Finite_ind) simp_all
-lemma ForallTL1: "Forall P s \<longrightarrow> Forall P (TL $ s)"
+lemma ForallTL1: "Forall P s \<longrightarrow> Forall P (TL \<cdot> s)"
apply (rule_tac x="s" in Seq_induct)
apply (simp add: Forall_def sforall_def)
apply simp_all
@@ -510,7 +510,7 @@
lemmas ForallTL = ForallTL1 [THEN mp]
-lemma ForallDropwhile1: "Forall P s \<longrightarrow> Forall P (Dropwhile Q $ s)"
+lemma ForallDropwhile1: "Forall P s \<longrightarrow> Forall P (Dropwhile Q \<cdot> s)"
apply (rule_tac x="s" in Seq_induct)
apply (simp add: Forall_def sforall_def)
apply simp_all
@@ -537,7 +537,7 @@
lemma ForallPFilterQR1:
- "(\<forall>x. P x \<longrightarrow> Q x = R x) \<and> Forall P tr \<longrightarrow> Filter Q $ tr = Filter R $ tr"
+ "(\<forall>x. P x \<longrightarrow> Q x = R x) \<and> Forall P tr \<longrightarrow> Filter Q \<cdot> tr = Filter R \<cdot> tr"
apply (rule_tac x="tr" in Seq_induct)
apply (simp add: Forall_def sforall_def)
apply simp_all
@@ -548,11 +548,11 @@
subsection \<open>Forall, Filter\<close>
-lemma ForallPFilterP: "Forall P (Filter P $ x)"
+lemma ForallPFilterP: "Forall P (Filter P \<cdot> x)"
by (simp add: Filter_def Forall_def forallPsfilterP)
(*holds also in other direction, then equal to forallPfilterP*)
-lemma ForallPFilterPid1: "Forall P x \<longrightarrow> Filter P $ x = x"
+lemma ForallPFilterPid1: "Forall P x \<longrightarrow> Filter P \<cdot> x = x"
apply (rule_tac x="x" in Seq_induct)
apply (simp add: Forall_def sforall_def Filter_def)
apply simp_all
@@ -561,14 +561,14 @@
lemmas ForallPFilterPid = ForallPFilterPid1 [THEN mp]
(*holds also in other direction*)
-lemma ForallnPFilterPnil1: "Finite ys \<Longrightarrow> Forall (\<lambda>x. \<not> P x) ys \<longrightarrow> Filter P $ ys = nil"
+lemma ForallnPFilterPnil1: "Finite ys \<Longrightarrow> Forall (\<lambda>x. \<not> P x) ys \<longrightarrow> Filter P \<cdot> ys = nil"
by (erule Seq_Finite_ind) simp_all
lemmas ForallnPFilterPnil = ForallnPFilterPnil1 [THEN mp]
(*holds also in other direction*)
-lemma ForallnPFilterPUU1: "\<not> Finite ys \<and> Forall (\<lambda>x. \<not> P x) ys \<longrightarrow> Filter P $ ys = UU"
+lemma ForallnPFilterPUU1: "\<not> Finite ys \<and> Forall (\<lambda>x. \<not> P x) ys \<longrightarrow> Filter P \<cdot> ys = UU"
apply (rule_tac x="ys" in Seq_induct)
apply (simp add: Forall_def sforall_def)
apply simp_all
@@ -578,7 +578,7 @@
(*inverse of ForallnPFilterPnil*)
-lemma FilternPnilForallP [rule_format]: "Filter P $ ys = nil \<longrightarrow> Forall (\<lambda>x. \<not> P x) ys \<and> Finite ys"
+lemma FilternPnilForallP [rule_format]: "Filter P \<cdot> ys = nil \<longrightarrow> Forall (\<lambda>x. \<not> P x) ys \<and> Finite ys"
apply (rule_tac x="ys" in Seq_induct)
text \<open>adm\<close>
apply (simp add: Forall_def sforall_def)
@@ -591,13 +591,13 @@
(*inverse of ForallnPFilterPUU*)
lemma FilternPUUForallP:
- assumes "Filter P $ ys = UU"
+ assumes "Filter P \<cdot> ys = UU"
shows "Forall (\<lambda>x. \<not> P x) ys \<and> \<not> Finite ys"
proof
show "Forall (\<lambda>x. \<not> P x) ys"
proof (rule classical)
assume "\<not> ?thesis"
- then have "Filter P $ ys \<noteq> UU"
+ then have "Filter P \<cdot> ys \<noteq> UU"
apply (rule rev_mp)
apply (induct ys rule: Seq_induct)
apply (simp add: Forall_def sforall_def)
@@ -608,7 +608,7 @@
show "\<not> Finite ys"
proof
assume "Finite ys"
- then have "Filter P$ys \<noteq> UU"
+ then have "Filter P\<cdot>ys \<noteq> UU"
by (rule Seq_Finite_ind) simp_all
with assms show False by contradiction
qed
@@ -616,13 +616,13 @@
lemma ForallQFilterPnil:
- "Forall Q ys \<Longrightarrow> Finite ys \<Longrightarrow> (\<And>x. Q x \<Longrightarrow> \<not> P x) \<Longrightarrow> Filter P $ ys = nil"
+ "Forall Q ys \<Longrightarrow> Finite ys \<Longrightarrow> (\<And>x. Q x \<Longrightarrow> \<not> P x) \<Longrightarrow> Filter P \<cdot> ys = nil"
apply (erule ForallnPFilterPnil)
apply (erule ForallPForallQ)
apply auto
done
-lemma ForallQFilterPUU: "\<not> Finite ys \<Longrightarrow> Forall Q ys \<Longrightarrow> (\<And>x. Q x \<Longrightarrow> \<not> P x) \<Longrightarrow> Filter P $ ys = UU"
+lemma ForallQFilterPUU: "\<not> Finite ys \<Longrightarrow> Forall Q ys \<Longrightarrow> (\<And>x. Q x \<Longrightarrow> \<not> P x) \<Longrightarrow> Filter P \<cdot> ys = UU"
apply (erule ForallnPFilterPUU)
apply (erule ForallPForallQ)
apply auto
@@ -631,11 +631,11 @@
subsection \<open>Takewhile, Forall, Filter\<close>
-lemma ForallPTakewhileP [simp]: "Forall P (Takewhile P $ x)"
+lemma ForallPTakewhileP [simp]: "Forall P (Takewhile P \<cdot> x)"
by (simp add: Forall_def Takewhile_def sforallPstakewhileP)
-lemma ForallPTakewhileQ [simp]: "(\<And>x. Q x \<Longrightarrow> P x) \<Longrightarrow> Forall P (Takewhile Q $ x)"
+lemma ForallPTakewhileQ [simp]: "(\<And>x. Q x \<Longrightarrow> P x) \<Longrightarrow> Forall P (Takewhile Q \<cdot> x)"
apply (rule ForallPForallQ)
apply (rule ForallPTakewhileP)
apply auto
@@ -643,7 +643,7 @@
lemma FilterPTakewhileQnil [simp]:
- "Finite (Takewhile Q $ ys) \<Longrightarrow> (\<And>x. Q x \<Longrightarrow> \<not> P x) \<Longrightarrow> Filter P $ (Takewhile Q $ ys) = nil"
+ "Finite (Takewhile Q \<cdot> ys) \<Longrightarrow> (\<And>x. Q x \<Longrightarrow> \<not> P x) \<Longrightarrow> Filter P \<cdot> (Takewhile Q \<cdot> ys) = nil"
apply (erule ForallnPFilterPnil)
apply (rule ForallPForallQ)
apply (rule ForallPTakewhileP)
@@ -651,7 +651,7 @@
done
lemma FilterPTakewhileQid [simp]:
- "(\<And>x. Q x \<Longrightarrow> P x) \<Longrightarrow> Filter P $ (Takewhile Q $ ys) = Takewhile Q $ ys"
+ "(\<And>x. Q x \<Longrightarrow> P x) \<Longrightarrow> Filter P \<cdot> (Takewhile Q \<cdot> ys) = Takewhile Q \<cdot> ys"
apply (rule ForallPFilterPid)
apply (rule ForallPForallQ)
apply (rule ForallPTakewhileP)
@@ -659,28 +659,28 @@
done
-lemma Takewhile_idempotent: "Takewhile P $ (Takewhile P $ s) = Takewhile P $ s"
+lemma Takewhile_idempotent: "Takewhile P \<cdot> (Takewhile P \<cdot> s) = Takewhile P \<cdot> s"
apply (rule_tac x="s" in Seq_induct)
apply (simp add: Forall_def sforall_def)
apply simp_all
done
lemma ForallPTakewhileQnP [simp]:
- "Forall P s \<longrightarrow> Takewhile (\<lambda>x. Q x \<or> (\<not> P x)) $ s = Takewhile Q $ s"
+ "Forall P s \<longrightarrow> Takewhile (\<lambda>x. Q x \<or> (\<not> P x)) \<cdot> s = Takewhile Q \<cdot> s"
apply (rule_tac x="s" in Seq_induct)
apply (simp add: Forall_def sforall_def)
apply simp_all
done
lemma ForallPDropwhileQnP [simp]:
- "Forall P s \<longrightarrow> Dropwhile (\<lambda>x. Q x \<or> (\<not> P x)) $ s = Dropwhile Q $ s"
+ "Forall P s \<longrightarrow> Dropwhile (\<lambda>x. Q x \<or> (\<not> P x)) \<cdot> s = Dropwhile Q \<cdot> s"
apply (rule_tac x="s" in Seq_induct)
apply (simp add: Forall_def sforall_def)
apply simp_all
done
-lemma TakewhileConc1: "Forall P s \<longrightarrow> Takewhile P $ (s @@ t) = s @@ (Takewhile P $ t)"
+lemma TakewhileConc1: "Forall P s \<longrightarrow> Takewhile P \<cdot> (s @@ t) = s @@ (Takewhile P \<cdot> t)"
apply (rule_tac x="s" in Seq_induct)
apply (simp add: Forall_def sforall_def)
apply simp_all
@@ -688,7 +688,7 @@
lemmas TakewhileConc = TakewhileConc1 [THEN mp]
-lemma DropwhileConc1: "Finite s \<Longrightarrow> Forall P s \<longrightarrow> Dropwhile P $ (s @@ t) = Dropwhile P $ t"
+lemma DropwhileConc1: "Finite s \<Longrightarrow> Forall P s \<longrightarrow> Dropwhile P \<cdot> (s @@ t) = Dropwhile P \<cdot> t"
by (erule Seq_Finite_ind) simp_all
lemmas DropwhileConc = DropwhileConc1 [THEN mp]
@@ -697,9 +697,9 @@
subsection \<open>Coinductive characterizations of Filter\<close>
lemma divide_Seq_lemma:
- "HD $ (Filter P $ y) = Def x \<longrightarrow>
- y = (Takewhile (\<lambda>x. \<not> P x) $ y) @@ (x \<leadsto> TL $ (Dropwhile (\<lambda>a. \<not> P a) $ y)) \<and>
- Finite (Takewhile (\<lambda>x. \<not> P x) $ y) \<and> P x"
+ "HD \<cdot> (Filter P \<cdot> y) = Def x \<longrightarrow>
+ y = (Takewhile (\<lambda>x. \<not> P x) \<cdot> y) @@ (x \<leadsto> TL \<cdot> (Dropwhile (\<lambda>a. \<not> P a) \<cdot> y)) \<and>
+ Finite (Takewhile (\<lambda>x. \<not> P x) \<cdot> y) \<and> P x"
(* FIX: pay attention: is only admissible with chain-finite package to be added to
adm test and Finite f x admissibility *)
apply (rule_tac x="y" in Seq_induct)
@@ -713,16 +713,16 @@
apply simp
done
-lemma divide_Seq: "(x \<leadsto> xs) \<sqsubseteq> Filter P $ y \<Longrightarrow>
- y = ((Takewhile (\<lambda>a. \<not> P a) $ y) @@ (x \<leadsto> TL $ (Dropwhile (\<lambda>a. \<not> P a) $ y))) \<and>
- Finite (Takewhile (\<lambda>a. \<not> P a) $ y) \<and> P x"
+lemma divide_Seq: "(x \<leadsto> xs) \<sqsubseteq> Filter P \<cdot> y \<Longrightarrow>
+ y = ((Takewhile (\<lambda>a. \<not> P a) \<cdot> y) @@ (x \<leadsto> TL \<cdot> (Dropwhile (\<lambda>a. \<not> P a) \<cdot> y))) \<and>
+ Finite (Takewhile (\<lambda>a. \<not> P a) \<cdot> y) \<and> P x"
apply (rule divide_Seq_lemma [THEN mp])
apply (drule_tac f="HD" and x="x \<leadsto> xs" in monofun_cfun_arg)
apply simp
done
-lemma nForall_HDFilter: "\<not> Forall P y \<longrightarrow> (\<exists>x. HD $ (Filter (\<lambda>a. \<not> P a) $ y) = Def x)"
+lemma nForall_HDFilter: "\<not> Forall P y \<longrightarrow> (\<exists>x. HD \<cdot> (Filter (\<lambda>a. \<not> P a) \<cdot> y) = Def x)"
unfolding not_Undef_is_Def [symmetric]
apply (induct y rule: Seq_induct)
apply (simp add: Forall_def sforall_def)
@@ -732,7 +732,7 @@
lemma divide_Seq2:
"\<not> Forall P y \<Longrightarrow>
- \<exists>x. y = Takewhile P$y @@ (x \<leadsto> TL $ (Dropwhile P $ y)) \<and> Finite (Takewhile P $ y) \<and> \<not> P x"
+ \<exists>x. y = Takewhile P\<cdot>y @@ (x \<leadsto> TL \<cdot> (Dropwhile P \<cdot> y)) \<and> Finite (Takewhile P \<cdot> y) \<and> \<not> P x"
apply (drule nForall_HDFilter [THEN mp])
apply safe
apply (rule_tac x="x" in exI)
@@ -752,15 +752,15 @@
subsection \<open>Take-lemma\<close>
-lemma seq_take_lemma: "(\<forall>n. seq_take n $ x = seq_take n $ x') \<longleftrightarrow> x = x'"
+lemma seq_take_lemma: "(\<forall>n. seq_take n \<cdot> x = seq_take n \<cdot> x') \<longleftrightarrow> x = x'"
apply (rule iffI)
apply (rule seq.take_lemma)
apply auto
done
lemma take_reduction1:
- "\<forall>n. ((\<forall>k. k < n \<longrightarrow> seq_take k $ y1 = seq_take k $ y2) \<longrightarrow>
- seq_take n $ (x @@ (t \<leadsto> y1)) = seq_take n $ (x @@ (t \<leadsto> y2)))"
+ "\<forall>n. ((\<forall>k. k < n \<longrightarrow> seq_take k \<cdot> y1 = seq_take k \<cdot> y2) \<longrightarrow>
+ seq_take n \<cdot> (x @@ (t \<leadsto> y1)) = seq_take n \<cdot> (x @@ (t \<leadsto> y2)))"
apply (rule_tac x="x" in Seq_induct)
apply simp_all
apply (intro strip)
@@ -771,8 +771,8 @@
done
lemma take_reduction:
- "x = y \<Longrightarrow> s = t \<Longrightarrow> (\<And>k. k < n \<Longrightarrow> seq_take k $ y1 = seq_take k $ y2)
- \<Longrightarrow> seq_take n $ (x @@ (s \<leadsto> y1)) = seq_take n $ (y @@ (t \<leadsto> y2))"
+ "x = y \<Longrightarrow> s = t \<Longrightarrow> (\<And>k. k < n \<Longrightarrow> seq_take k \<cdot> y1 = seq_take k \<cdot> y2)
+ \<Longrightarrow> seq_take n \<cdot> (x @@ (s \<leadsto> y1)) = seq_take n \<cdot> (y @@ (t \<leadsto> y2))"
by (auto intro!: take_reduction1 [rule_format])
@@ -781,8 +781,8 @@
\<close>
lemma take_reduction_less1:
- "\<forall>n. ((\<forall>k. k < n \<longrightarrow> seq_take k $ y1 \<sqsubseteq> seq_take k$y2) \<longrightarrow>
- seq_take n $ (x @@ (t \<leadsto> y1)) \<sqsubseteq> seq_take n $ (x @@ (t \<leadsto> y2)))"
+ "\<forall>n. ((\<forall>k. k < n \<longrightarrow> seq_take k \<cdot> y1 \<sqsubseteq> seq_take k\<cdot>y2) \<longrightarrow>
+ seq_take n \<cdot> (x @@ (t \<leadsto> y1)) \<sqsubseteq> seq_take n \<cdot> (x @@ (t \<leadsto> y2)))"
apply (rule_tac x="x" in Seq_induct)
apply simp_all
apply (intro strip)
@@ -793,12 +793,12 @@
done
lemma take_reduction_less:
- "x = y \<Longrightarrow> s = t \<Longrightarrow> (\<And>k. k < n \<Longrightarrow> seq_take k $ y1 \<sqsubseteq> seq_take k $ y2) \<Longrightarrow>
- seq_take n $ (x @@ (s \<leadsto> y1)) \<sqsubseteq> seq_take n $ (y @@ (t \<leadsto> y2))"
+ "x = y \<Longrightarrow> s = t \<Longrightarrow> (\<And>k. k < n \<Longrightarrow> seq_take k \<cdot> y1 \<sqsubseteq> seq_take k \<cdot> y2) \<Longrightarrow>
+ seq_take n \<cdot> (x @@ (s \<leadsto> y1)) \<sqsubseteq> seq_take n \<cdot> (y @@ (t \<leadsto> y2))"
by (auto intro!: take_reduction_less1 [rule_format])
lemma take_lemma_less1:
- assumes "\<And>n. seq_take n $ s1 \<sqsubseteq> seq_take n $ s2"
+ assumes "\<And>n. seq_take n \<cdot> s1 \<sqsubseteq> seq_take n \<cdot> s2"
shows "s1 \<sqsubseteq> s2"
apply (rule_tac t="s1" in seq.reach [THEN subst])
apply (rule_tac t="s2" in seq.reach [THEN subst])
@@ -808,7 +808,7 @@
apply (rule assms)
done
-lemma take_lemma_less: "(\<forall>n. seq_take n $ x \<sqsubseteq> seq_take n $ x') \<longleftrightarrow> x \<sqsubseteq> x'"
+lemma take_lemma_less: "(\<forall>n. seq_take n \<cdot> x \<sqsubseteq> seq_take n \<cdot> x') \<longleftrightarrow> x \<sqsubseteq> x'"
apply (rule iffI)
apply (rule take_lemma_less1)
apply auto
@@ -828,7 +828,7 @@
lemma take_lemma_principle2:
assumes "\<And>s. Forall Q s \<Longrightarrow> A s \<Longrightarrow> f s = g s"
and "\<And>s1 s2 y. Forall Q s1 \<Longrightarrow> Finite s1 \<Longrightarrow> \<not> Q y \<Longrightarrow> A (s1 @@ y \<leadsto> s2) \<Longrightarrow>
- \<forall>n. seq_take n $ (f (s1 @@ y \<leadsto> s2)) = seq_take n $ (g (s1 @@ y \<leadsto> s2))"
+ \<forall>n. seq_take n \<cdot> (f (s1 @@ y \<leadsto> s2)) = seq_take n \<cdot> (g (s1 @@ y \<leadsto> s2))"
shows "A x \<longrightarrow> f x = g x"
using assms
apply (cases "Forall Q x")
@@ -852,10 +852,10 @@
lemma take_lemma_induct:
assumes "\<And>s. Forall Q s \<Longrightarrow> A s \<Longrightarrow> f s = g s"
and "\<And>s1 s2 y n.
- \<forall>t. A t \<longrightarrow> seq_take n $ (f t) = seq_take n $ (g t) \<Longrightarrow>
+ \<forall>t. A t \<longrightarrow> seq_take n \<cdot> (f t) = seq_take n \<cdot> (g t) \<Longrightarrow>
Forall Q s1 \<Longrightarrow> Finite s1 \<Longrightarrow> \<not> Q y \<Longrightarrow> A (s1 @@ y \<leadsto> s2) \<Longrightarrow>
- seq_take (Suc n) $ (f (s1 @@ y \<leadsto> s2)) =
- seq_take (Suc n) $ (g (s1 @@ y \<leadsto> s2))"
+ seq_take (Suc n) \<cdot> (f (s1 @@ y \<leadsto> s2)) =
+ seq_take (Suc n) \<cdot> (g (s1 @@ y \<leadsto> s2))"
shows "A x \<longrightarrow> f x = g x"
apply (insert assms)
apply (rule impI)
@@ -875,10 +875,10 @@
lemma take_lemma_less_induct:
assumes "\<And>s. Forall Q s \<Longrightarrow> A s \<Longrightarrow> f s = g s"
and "\<And>s1 s2 y n.
- \<forall>t m. m < n \<longrightarrow> A t \<longrightarrow> seq_take m $ (f t) = seq_take m $ (g t) \<Longrightarrow>
+ \<forall>t m. m < n \<longrightarrow> A t \<longrightarrow> seq_take m \<cdot> (f t) = seq_take m \<cdot> (g t) \<Longrightarrow>
Forall Q s1 \<Longrightarrow> Finite s1 \<Longrightarrow> \<not> Q y \<Longrightarrow> A (s1 @@ y \<leadsto> s2) \<Longrightarrow>
- seq_take n $ (f (s1 @@ y \<leadsto> s2)) =
- seq_take n $ (g (s1 @@ y \<leadsto> s2))"
+ seq_take n \<cdot> (f (s1 @@ y \<leadsto> s2)) =
+ seq_take n \<cdot> (g (s1 @@ y \<leadsto> s2))"
shows "A x \<longrightarrow> f x = g x"
apply (insert assms)
apply (rule impI)
@@ -899,9 +899,9 @@
assumes "A UU \<Longrightarrow> f UU = g UU"
and "A nil \<Longrightarrow> f nil = g nil"
and "\<And>s y n.
- \<forall>t. A t \<longrightarrow> seq_take n $ (f t) = seq_take n $ (g t) \<Longrightarrow> A (y \<leadsto> s) \<Longrightarrow>
- seq_take (Suc n) $ (f (y \<leadsto> s)) =
- seq_take (Suc n) $ (g (y \<leadsto> s))"
+ \<forall>t. A t \<longrightarrow> seq_take n \<cdot> (f t) = seq_take n \<cdot> (g t) \<Longrightarrow> A (y \<leadsto> s) \<Longrightarrow>
+ seq_take (Suc n) \<cdot> (f (y \<leadsto> s)) =
+ seq_take (Suc n) \<cdot> (g (y \<leadsto> s))"
shows "A x \<longrightarrow> f x = g x"
apply (insert assms)
apply (rule impI)
@@ -928,21 +928,21 @@
as for the entire proof?*)
lemma Filter_lemma1:
"Forall (\<lambda>x. \<not> (P x \<and> Q x)) s \<longrightarrow>
- Filter P $ (Filter Q $ s) = Filter (\<lambda>x. P x \<and> Q x) $ s"
+ Filter P \<cdot> (Filter Q \<cdot> s) = Filter (\<lambda>x. P x \<and> Q x) \<cdot> s"
apply (rule_tac x="s" in Seq_induct)
apply (simp add: Forall_def sforall_def)
apply simp_all
done
lemma Filter_lemma2: "Finite s \<Longrightarrow>
- Forall (\<lambda>x. \<not> P x \<or> \<not> Q x) s \<longrightarrow> Filter P $ (Filter Q $ s) = nil"
+ Forall (\<lambda>x. \<not> P x \<or> \<not> Q x) s \<longrightarrow> Filter P \<cdot> (Filter Q \<cdot> s) = nil"
by (erule Seq_Finite_ind) simp_all
lemma Filter_lemma3: "Finite s \<Longrightarrow>
- Forall (\<lambda>x. \<not> P x \<or> \<not> Q x) s \<longrightarrow> Filter (\<lambda>x. P x \<and> Q x) $ s = nil"
+ Forall (\<lambda>x. \<not> P x \<or> \<not> Q x) s \<longrightarrow> Filter (\<lambda>x. P x \<and> Q x) \<cdot> s = nil"
by (erule Seq_Finite_ind) simp_all
-lemma FilterPQ_takelemma: "Filter P $ (Filter Q $ s) = Filter (\<lambda>x. P x \<and> Q x) $ s"
+lemma FilterPQ_takelemma: "Filter P \<cdot> (Filter Q \<cdot> s) = Filter (\<lambda>x. P x \<and> Q x) \<cdot> s"
apply (rule_tac A1="\<lambda>x. True" and Q1="\<lambda>x. \<not> (P x \<and> Q x)" and x1="s" in
take_lemma_induct [THEN mp])
(*better support for A = \<lambda>x. True*)
@@ -956,7 +956,7 @@
subsubsection \<open>Alternative Proof of \<open>MapConc\<close>\<close>
-lemma MapConc_takelemma: "Map f $ (x @@ y) = (Map f $ x) @@ (Map f $ y)"
+lemma MapConc_takelemma: "Map f \<cdot> (x @@ y) = (Map f \<cdot> x) @@ (Map f \<cdot> y)"
apply (rule_tac A1="\<lambda>x. True" and x1="x" in take_lemma_in_eq_out [THEN mp])
apply auto
done
@@ -1017,13 +1017,13 @@
Scan.optional ((Scan.lift (Args.$$$ "simp" -- Args.colon) |-- Attrib.thms)) []
>> (fn (s, rws) => fn ctxt => SIMPLE_METHOD' (pair_induct_tac ctxt s rws))\<close>
-lemma Mapnil: "Map f $ s = nil \<longleftrightarrow> s = nil"
+lemma Mapnil: "Map f \<cdot> s = nil \<longleftrightarrow> s = nil"
by (Seq_case_simp s)
-lemma MapUU: "Map f $ s = UU \<longleftrightarrow> s = UU"
+lemma MapUU: "Map f \<cdot> s = UU \<longleftrightarrow> s = UU"
by (Seq_case_simp s)
-lemma MapTL: "Map f $ (TL $ s) = TL $ (Map f $ s)"
+lemma MapTL: "Map f \<cdot> (TL \<cdot> s) = TL \<cdot> (Map f \<cdot> s)"
by (Seq_induct s)
end
--- a/src/HOL/HOLCF/IOA/ShortExecutions.thy Mon Jul 25 14:02:29 2016 +0200
+++ b/src/HOL/HOLCF/IOA/ShortExecutions.thy Mon Jul 25 21:50:04 2016 +0200
@@ -15,7 +15,7 @@
definition oraclebuild :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Seq \<rightarrow> 'a Seq \<rightarrow> 'a Seq"
where "oraclebuild P =
- (fix $
+ (fix \<cdot>
(LAM h s t.
case t of
nil \<Rightarrow> nil
@@ -23,11 +23,11 @@
(case x of
UU \<Rightarrow> UU
| Def y \<Rightarrow>
- (Takewhile (\<lambda>x. \<not> P x) $ s) @@
- (y \<leadsto> (h $ (TL $ (Dropwhile (\<lambda>x. \<not> P x) $ s)) $ xs)))))"
+ (Takewhile (\<lambda>x. \<not> P x) \<cdot> s) @@
+ (y \<leadsto> (h \<cdot> (TL \<cdot> (Dropwhile (\<lambda>x. \<not> P x) \<cdot> s)) \<cdot> xs)))))"
definition Cut :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Seq \<Rightarrow> 'a Seq"
- where "Cut P s = oraclebuild P $ s $ (Filter P $ s)"
+ where "Cut P s = oraclebuild P \<cdot> s \<cdot> (Filter P \<cdot> s)"
definition LastActExtsch :: "('a,'s) ioa \<Rightarrow> 'a Seq \<Rightarrow> bool"
where "LastActExtsch A sch \<longleftrightarrow> Cut (\<lambda>x. x \<in> ext A) sch = sch"
@@ -36,7 +36,7 @@
Cut_prefixcl_Finite: "Finite s \<Longrightarrow> \<exists>y. s = Cut P s @@ y"
axiomatization where
- LastActExtsmall1: "LastActExtsch A sch \<Longrightarrow> LastActExtsch A (TL $ (Dropwhile P $ sch))"
+ LastActExtsmall1: "LastActExtsch A sch \<Longrightarrow> LastActExtsch A (TL \<cdot> (Dropwhile P \<cdot> sch))"
axiomatization where
LastActExtsmall2: "Finite sch1 \<Longrightarrow> LastActExtsch A (sch1 @@ sch2) \<Longrightarrow> LastActExtsch A sch2"
@@ -60,8 +60,8 @@
(case x of
UU \<Rightarrow> UU
| Def y \<Rightarrow>
- (Takewhile (\<lambda>a. \<not> P a) $ s) @@
- (y \<leadsto> (oraclebuild P $ (TL $ (Dropwhile (\<lambda>a. \<not> P a) $ s)) $ xs))))"
+ (Takewhile (\<lambda>a. \<not> P a) \<cdot> s) @@
+ (y \<leadsto> (oraclebuild P \<cdot> (TL \<cdot> (Dropwhile (\<lambda>a. \<not> P a) \<cdot> s)) \<cdot> xs))))"
apply (rule trans)
apply (rule fix_eq2)
apply (simp only: oraclebuild_def)
@@ -69,20 +69,20 @@
apply simp
done
-lemma oraclebuild_UU: "oraclebuild P $ sch $ UU = UU"
+lemma oraclebuild_UU: "oraclebuild P \<cdot> sch \<cdot> UU = UU"
apply (subst oraclebuild_unfold)
apply simp
done
-lemma oraclebuild_nil: "oraclebuild P $ sch $ nil = nil"
+lemma oraclebuild_nil: "oraclebuild P \<cdot> sch \<cdot> nil = nil"
apply (subst oraclebuild_unfold)
apply simp
done
lemma oraclebuild_cons:
- "oraclebuild P $ s $ (x \<leadsto> t) =
- (Takewhile (\<lambda>a. \<not> P a) $ s) @@
- (x \<leadsto> (oraclebuild P $ (TL $ (Dropwhile (\<lambda>a. \<not> P a) $ s)) $ t))"
+ "oraclebuild P \<cdot> s \<cdot> (x \<leadsto> t) =
+ (Takewhile (\<lambda>a. \<not> P a) \<cdot> s) @@
+ (x \<leadsto> (oraclebuild P \<cdot> (TL \<cdot> (Dropwhile (\<lambda>a. \<not> P a) \<cdot> s)) \<cdot> t))"
apply (rule trans)
apply (subst oraclebuild_unfold)
apply (simp add: Consq_def)
@@ -94,7 +94,7 @@
lemma Cut_nil: "Forall (\<lambda>a. \<not> P a) s \<Longrightarrow> Finite s \<Longrightarrow> Cut P s = nil"
apply (unfold Cut_def)
- apply (subgoal_tac "Filter P $ s = nil")
+ apply (subgoal_tac "Filter P \<cdot> s = nil")
apply (simp add: oraclebuild_nil)
apply (rule ForallQFilterPnil)
apply assumption+
@@ -102,7 +102,7 @@
lemma Cut_UU: "Forall (\<lambda>a. \<not> P a) s \<Longrightarrow> \<not> Finite s \<Longrightarrow> Cut P s = UU"
apply (unfold Cut_def)
- apply (subgoal_tac "Filter P $ s = UU")
+ apply (subgoal_tac "Filter P \<cdot> s = UU")
apply (simp add: oraclebuild_UU)
apply (rule ForallQFilterPUU)
apply assumption+
@@ -118,7 +118,7 @@
subsection \<open>Cut lemmas for main theorem\<close>
-lemma FilterCut: "Filter P $ s = Filter P $ (Cut P s)"
+lemma FilterCut: "Filter P \<cdot> s = Filter P \<cdot> (Cut P s)"
apply (rule_tac A1 = "\<lambda>x. True" and Q1 = "\<lambda>x. \<not> P x" and x1 = "s" in take_lemma_induct [THEN mp])
prefer 3
apply fast
@@ -143,7 +143,7 @@
apply auto
done
-lemma MapCut: "Map f$(Cut (P \<circ> f) s) = Cut P (Map f$s)"
+lemma MapCut: "Map f\<cdot>(Cut (P \<circ> f) s) = Cut P (Map f\<cdot>s)"
apply (rule_tac A1 = "\<lambda>x. True" and Q1 = "\<lambda>x. \<not> P (f x) " and x1 = "s" in
take_lemma_less_induct [THEN mp])
prefer 3
@@ -206,11 +206,11 @@
subsection \<open>Main Cut Theorem\<close>
lemma exists_LastActExtsch:
- "sch \<in> schedules A \<Longrightarrow> tr = Filter (\<lambda>a. a \<in> ext A) $ sch \<Longrightarrow>
- \<exists>sch. sch \<in> schedules A \<and> tr = Filter (\<lambda>a. a \<in> ext A) $ sch \<and> LastActExtsch A sch"
+ "sch \<in> schedules A \<Longrightarrow> tr = Filter (\<lambda>a. a \<in> ext A) \<cdot> sch \<Longrightarrow>
+ \<exists>sch. sch \<in> schedules A \<and> tr = Filter (\<lambda>a. a \<in> ext A) \<cdot> sch \<and> LastActExtsch A sch"
apply (unfold schedules_def has_schedule_def [abs_def])
apply auto
- apply (rule_tac x = "filter_act $ (Cut (\<lambda>a. fst a \<in> ext A) (snd ex))" in exI)
+ apply (rule_tac x = "filter_act \<cdot> (Cut (\<lambda>a. fst a \<in> ext A) (snd ex))" in exI)
apply (simp add: executions_def)
apply (pair ex)
apply auto
@@ -222,13 +222,13 @@
text \<open>Subgoal 2: Lemma: \<open>Filter P s = Filter P (Cut P s)\<close>\<close>
apply (simp add: filter_act_def)
- apply (subgoal_tac "Map fst $ (Cut (\<lambda>a. fst a \<in> ext A) x2) = Cut (\<lambda>a. a \<in> ext A) (Map fst $ x2)")
+ apply (subgoal_tac "Map fst \<cdot> (Cut (\<lambda>a. fst a \<in> ext A) x2) = Cut (\<lambda>a. a \<in> ext A) (Map fst \<cdot> x2)")
apply (rule_tac [2] MapCut [unfolded o_def])
apply (simp add: FilterCut [symmetric])
text \<open>Subgoal 3: Lemma: \<open>Cut\<close> idempotent\<close>
apply (simp add: LastActExtsch_def filter_act_def)
- apply (subgoal_tac "Map fst $ (Cut (\<lambda>a. fst a \<in> ext A) x2) = Cut (\<lambda>a. a \<in> ext A) (Map fst $ x2)")
+ apply (subgoal_tac "Map fst \<cdot> (Cut (\<lambda>a. fst a \<in> ext A) x2) = Cut (\<lambda>a. a \<in> ext A) (Map fst \<cdot> x2)")
apply (rule_tac [2] MapCut [unfolded o_def])
apply (simp add: Cut_idemp)
done
@@ -236,7 +236,7 @@
subsection \<open>Further Cut lemmas\<close>
-lemma LastActExtimplnil: "LastActExtsch A sch \<Longrightarrow> Filter (\<lambda>x. x \<in> ext A) $ sch = nil \<Longrightarrow> sch = nil"
+lemma LastActExtimplnil: "LastActExtsch A sch \<Longrightarrow> Filter (\<lambda>x. x \<in> ext A) \<cdot> sch = nil \<Longrightarrow> sch = nil"
apply (unfold LastActExtsch_def)
apply (drule FilternPnilForallP)
apply (erule conjE)
@@ -245,7 +245,7 @@
apply simp
done
-lemma LastActExtimplUU: "LastActExtsch A sch \<Longrightarrow> Filter (\<lambda>x. x \<in> ext A) $ sch = UU \<Longrightarrow> sch = UU"
+lemma LastActExtimplUU: "LastActExtsch A sch \<Longrightarrow> Filter (\<lambda>x. x \<in> ext A) \<cdot> sch = UU \<Longrightarrow> sch = UU"
apply (unfold LastActExtsch_def)
apply (drule FilternPUUForallP)
apply (erule conjE)
--- a/src/HOL/HOLCF/IOA/SimCorrectness.thy Mon Jul 25 14:02:29 2016 +0200
+++ b/src/HOL/HOLCF/IOA/SimCorrectness.thy Mon Jul 25 21:50:04 2016 +0200
@@ -12,7 +12,7 @@
definition corresp_ex_simC ::
"('a, 's2) ioa \<Rightarrow> ('s1 \<times> 's2) set \<Rightarrow> ('a, 's1) pairs \<rightarrow> ('s2 \<Rightarrow> ('a, 's2) pairs)"
where "corresp_ex_simC A R =
- (fix $ (LAM h ex. (\<lambda>s. case ex of
+ (fix \<cdot> (LAM h ex. (\<lambda>s. case ex of
nil \<Rightarrow> nil
| x ## xs \<Rightarrow>
(flift1
@@ -21,13 +21,13 @@
a = fst pr;
t = snd pr;
T' = SOME t'. \<exists>ex1. (t, t') \<in> R \<and> move A ex1 s a t'
- in (SOME cex. move A cex s a T') @@ ((h $ xs) T')) $ x))))"
+ in (SOME cex. move A cex s a T') @@ ((h \<cdot> xs) T')) \<cdot> x))))"
definition corresp_ex_sim ::
"('a, 's2) ioa \<Rightarrow> ('s1 \<times> 's2) set \<Rightarrow> ('a, 's1) execution \<Rightarrow> ('a, 's2) execution"
where "corresp_ex_sim A R ex \<equiv>
let S' = SOME s'. (fst ex, s') \<in> R \<and> s' \<in> starts_of A
- in (S', (corresp_ex_simC A R $ (snd ex)) S')"
+ in (S', (corresp_ex_simC A R \<cdot> (snd ex)) S')"
subsection \<open>\<open>corresp_ex_sim\<close>\<close>
@@ -43,7 +43,7 @@
a = fst pr;
t = snd pr;
T' = SOME t'. \<exists>ex1. (t, t') \<in> R \<and> move A ex1 s a t'
- in (SOME cex. move A cex s a T') @@ ((corresp_ex_simC A R $ xs) T')) $ x)))"
+ in (SOME cex. move A cex s a T') @@ ((corresp_ex_simC A R \<cdot> xs) T')) \<cdot> x)))"
apply (rule trans)
apply (rule fix_eq2)
apply (simp only: corresp_ex_simC_def)
@@ -51,20 +51,20 @@
apply (simp add: flift1_def)
done
-lemma corresp_ex_simC_UU [simp]: "(corresp_ex_simC A R $ UU) s = UU"
+lemma corresp_ex_simC_UU [simp]: "(corresp_ex_simC A R \<cdot> UU) s = UU"
apply (subst corresp_ex_simC_unfold)
apply simp
done
-lemma corresp_ex_simC_nil [simp]: "(corresp_ex_simC A R $ nil) s = nil"
+lemma corresp_ex_simC_nil [simp]: "(corresp_ex_simC A R \<cdot> nil) s = nil"
apply (subst corresp_ex_simC_unfold)
apply simp
done
lemma corresp_ex_simC_cons [simp]:
- "(corresp_ex_simC A R $ ((a, t) \<leadsto> xs)) s =
+ "(corresp_ex_simC A R \<cdot> ((a, t) \<leadsto> xs)) s =
(let T' = SOME t'. \<exists>ex1. (t, t') \<in> R \<and> move A ex1 s a t'
- in (SOME cex. move A cex s a T') @@ ((corresp_ex_simC A R $ xs) T'))"
+ in (SOME cex. move A cex s a T') @@ ((corresp_ex_simC A R \<cdot> xs) T'))"
apply (rule trans)
apply (subst corresp_ex_simC_unfold)
apply (simp add: Consq_def flift1_def)
@@ -134,7 +134,7 @@
lemma move_subprop4_sim:
"is_simulation R C A \<Longrightarrow> reachable C s \<Longrightarrow> s \<midarrow>a\<midarrow>C\<rightarrow> t \<Longrightarrow> (s, s') \<in> R \<Longrightarrow>
let T' = SOME t'. \<exists>ex1. (t, t') \<in> R \<and> move A ex1 s' a t'
- in mk_trace A $ (SOME x. move A x s' a T') = (if a \<in> ext A then a \<leadsto> nil else nil)"
+ in mk_trace A \<cdot> (SOME x. move A x s' a T') = (if a \<in> ext A then a \<leadsto> nil else nil)"
apply (cut_tac move_is_move_sim)
defer
apply assumption+
@@ -161,7 +161,7 @@
lemma traces_coincide_sim [rule_format (no_asm)]:
"is_simulation R C A \<Longrightarrow> ext C = ext A \<Longrightarrow>
\<forall>s s'. reachable C s \<and> is_exec_frag C (s, ex) \<and> (s, s') \<in> R \<longrightarrow>
- mk_trace C $ ex = mk_trace A $ ((corresp_ex_simC A R $ ex) s')"
+ mk_trace C \<cdot> ex = mk_trace A \<cdot> ((corresp_ex_simC A R \<cdot> ex) s')"
supply if_split [split del]
apply (pair_induct ex simp: is_exec_frag_def)
text \<open>cons case\<close>
@@ -181,7 +181,7 @@
lemma correspsim_is_execution [rule_format]:
"is_simulation R C A \<Longrightarrow>
\<forall>s s'. reachable C s \<and> is_exec_frag C (s, ex) \<and> (s, s') \<in> R
- \<longrightarrow> is_exec_frag A (s', (corresp_ex_simC A R $ ex) s')"
+ \<longrightarrow> is_exec_frag A (s', (corresp_ex_simC A R \<cdot> ex) s')"
apply (pair_induct ex simp: is_exec_frag_def)
text \<open>main case\<close>
apply auto
--- a/src/HOL/HOLCF/IOA/TL.thy Mon Jul 25 14:02:29 2016 +0200
+++ b/src/HOL/HOLCF/IOA/TL.thy Mon Jul 25 21:50:04 2016 +0200
@@ -19,11 +19,11 @@
where "unlift x = (case x of Def y \<Rightarrow> y)"
definition Init :: "'a predicate \<Rightarrow> 'a temporal" ("\<langle>_\<rangle>" [0] 1000)
- where "Init P s = P (unlift (HD $ s))"
+ where "Init P s = P (unlift (HD \<cdot> s))"
\<comment> \<open>this means that for \<open>nil\<close> and \<open>UU\<close> the effect is unpredictable\<close>
definition Next :: "'a temporal \<Rightarrow> 'a temporal" ("\<circle>(_)" [80] 80)
- where "(\<circle>P) s \<longleftrightarrow> (if TL $ s = UU \<or> TL $ s = nil then P s else P (TL $ s))"
+ where "(\<circle>P) s \<longleftrightarrow> (if TL \<cdot> s = UU \<or> TL \<cdot> s = nil then P s else P (TL \<cdot> s))"
definition suffix :: "'a Seq \<Rightarrow> 'a Seq \<Rightarrow> bool"
where "suffix s2 s \<longleftrightarrow> (\<exists>s1. Finite s1 \<and> s = s1 @@ s2)"
@@ -110,7 +110,7 @@
subsection \<open>LTL Axioms by Manna/Pnueli\<close>
-lemma tsuffix_TL [rule_format]: "s \<noteq> UU \<and> s \<noteq> nil \<longrightarrow> tsuffix s2 (TL $ s) \<longrightarrow> tsuffix s2 s"
+lemma tsuffix_TL [rule_format]: "s \<noteq> UU \<and> s \<noteq> nil \<longrightarrow> tsuffix s2 (TL \<cdot> s) \<longrightarrow> tsuffix s2 s"
apply (unfold tsuffix_def suffix_def)
apply auto
apply (Seq_case_simp s)
--- a/src/HOL/HOLCF/IOA/TLS.thy Mon Jul 25 14:02:29 2016 +0200
+++ b/src/HOL/HOLCF/IOA/TLS.thy Mon Jul 25 21:50:04 2016 +0200
@@ -35,12 +35,12 @@
definition ex2seqC :: "('a, 's) pairs \<rightarrow> ('s \<Rightarrow> ('a option, 's) transition Seq)"
where "ex2seqC =
- (fix $ (LAM h ex. (\<lambda>s. case ex of
+ (fix \<cdot> (LAM h ex. (\<lambda>s. case ex of
nil \<Rightarrow> (s, None, s) \<leadsto> nil
- | x ## xs \<Rightarrow> (flift1 (\<lambda>pr. (s, Some (fst pr), snd pr) \<leadsto> (h $ xs) (snd pr)) $ x))))"
+ | x ## xs \<Rightarrow> (flift1 (\<lambda>pr. (s, Some (fst pr), snd pr) \<leadsto> (h \<cdot> xs) (snd pr)) \<cdot> x))))"
definition ex2seq :: "('a, 's) execution \<Rightarrow> ('a option, 's) transition Seq"
- where "ex2seq ex = (ex2seqC $ (mkfin (snd ex))) (fst ex)"
+ where "ex2seq ex = (ex2seqC \<cdot> (mkfin (snd ex))) (fst ex)"
definition temp_sat :: "('a, 's) execution \<Rightarrow> ('a, 's) ioa_temp \<Rightarrow> bool" (infixr "\<TTurnstile>" 22)
where "(ex \<TTurnstile> P) \<longleftrightarrow> ((ex2seq ex) \<Turnstile> P)"
@@ -83,7 +83,7 @@
(LAM ex. (\<lambda>s. case ex of
nil \<Rightarrow> (s, None, s) \<leadsto> nil
| x ## xs \<Rightarrow>
- (flift1 (\<lambda>pr. (s, Some (fst pr), snd pr) \<leadsto> (ex2seqC $ xs) (snd pr)) $ x)))"
+ (flift1 (\<lambda>pr. (s, Some (fst pr), snd pr) \<leadsto> (ex2seqC \<cdot> xs) (snd pr)) \<cdot> x)))"
apply (rule trans)
apply (rule fix_eq4)
apply (rule ex2seqC_def)
@@ -91,17 +91,17 @@
apply (simp add: flift1_def)
done
-lemma ex2seqC_UU [simp]: "(ex2seqC $ UU) s = UU"
+lemma ex2seqC_UU [simp]: "(ex2seqC \<cdot> UU) s = UU"
apply (subst ex2seqC_unfold)
apply simp
done
-lemma ex2seqC_nil [simp]: "(ex2seqC $ nil) s = (s, None, s) \<leadsto> nil"
+lemma ex2seqC_nil [simp]: "(ex2seqC \<cdot> nil) s = (s, None, s) \<leadsto> nil"
apply (subst ex2seqC_unfold)
apply simp
done
-lemma ex2seqC_cons [simp]: "(ex2seqC $ ((a, t) \<leadsto> xs)) s = (s, Some a,t ) \<leadsto> (ex2seqC $ xs) t"
+lemma ex2seqC_cons [simp]: "(ex2seqC \<cdot> ((a, t) \<leadsto> xs)) s = (s, Some a,t ) \<leadsto> (ex2seqC \<cdot> xs) t"
apply (rule trans)
apply (subst ex2seqC_unfold)
apply (simp add: Consq_def flift1_def)
--- a/src/HOL/HOLCF/IOA/Traces.thy Mon Jul 25 14:02:29 2016 +0200
+++ b/src/HOL/HOLCF/IOA/Traces.thy Mon Jul 25 21:50:04 2016 +0200
@@ -22,15 +22,15 @@
definition is_exec_fragC :: "('a, 's) ioa \<Rightarrow> ('a, 's) pairs \<rightarrow> 's \<Rightarrow> tr"
where "is_exec_fragC A =
- (fix $
+ (fix \<cdot>
(LAM h ex.
(\<lambda>s.
case ex of
nil \<Rightarrow> TT
- | x ## xs \<Rightarrow> flift1 (\<lambda>p. Def ((s, p) \<in> trans_of A) andalso (h $ xs) (snd p)) $ x)))"
+ | x ## xs \<Rightarrow> flift1 (\<lambda>p. Def ((s, p) \<in> trans_of A) andalso (h \<cdot> xs) (snd p)) \<cdot> x)))"
definition is_exec_frag :: "('a, 's) ioa \<Rightarrow> ('a, 's) execution \<Rightarrow> bool"
- where "is_exec_frag A ex \<longleftrightarrow> (is_exec_fragC A $ (snd ex)) (fst ex) \<noteq> FF"
+ where "is_exec_frag A ex \<longleftrightarrow> (is_exec_fragC A \<cdot> (snd ex)) (fst ex) \<noteq> FF"
definition executions :: "('a, 's) ioa \<Rightarrow> ('a, 's) execution set"
where "executions ioa = {e. fst e \<in> starts_of ioa \<and> is_exec_frag ioa e}"
@@ -42,7 +42,7 @@
where "filter_act = Map fst"
definition has_schedule :: "('a, 's) ioa \<Rightarrow> 'a trace \<Rightarrow> bool"
- where "has_schedule ioa sch \<longleftrightarrow> (\<exists>ex \<in> executions ioa. sch = filter_act $ (snd ex))"
+ where "has_schedule ioa sch \<longleftrightarrow> (\<exists>ex \<in> executions ioa. sch = filter_act \<cdot> (snd ex))"
definition schedules :: "('a, 's) ioa \<Rightarrow> 'a trace set"
where "schedules ioa = {sch. has_schedule ioa sch}"
@@ -51,26 +51,26 @@
subsection \<open>Traces\<close>
definition has_trace :: "('a, 's) ioa \<Rightarrow> 'a trace \<Rightarrow> bool"
- where "has_trace ioa tr \<longleftrightarrow> (\<exists>sch \<in> schedules ioa. tr = Filter (\<lambda>a. a \<in> ext ioa) $ sch)"
+ where "has_trace ioa tr \<longleftrightarrow> (\<exists>sch \<in> schedules ioa. tr = Filter (\<lambda>a. a \<in> ext ioa) \<cdot> sch)"
definition traces :: "('a, 's) ioa \<Rightarrow> 'a trace set"
where "traces ioa \<equiv> {tr. has_trace ioa tr}"
definition mk_trace :: "('a, 's) ioa \<Rightarrow> ('a, 's) pairs \<rightarrow> 'a trace"
- where "mk_trace ioa = (LAM tr. Filter (\<lambda>a. a \<in> ext ioa) $ (filter_act $ tr))"
+ where "mk_trace ioa = (LAM tr. Filter (\<lambda>a. a \<in> ext ioa) \<cdot> (filter_act \<cdot> tr))"
subsection \<open>Fair Traces\<close>
definition laststate :: "('a, 's) execution \<Rightarrow> 's"
where "laststate ex =
- (case Last $ (snd ex) of
+ (case Last \<cdot> (snd ex) of
UU \<Rightarrow> fst ex
| Def at \<Rightarrow> snd at)"
text \<open>A predicate holds infinitely (finitely) often in a sequence.\<close>
definition inf_often :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Seq \<Rightarrow> bool"
- where "inf_often P s \<longleftrightarrow> Infinite (Filter P $ s)"
+ where "inf_often P s \<longleftrightarrow> Infinite (Filter P \<cdot> s)"
text \<open>Filtering \<open>P\<close> yields a finite or partial sequence.\<close>
definition fin_often :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Seq \<Rightarrow> bool"
@@ -122,7 +122,7 @@
where "fairexecutions A = {ex. ex \<in> executions A \<and> fair_ex A ex}"
definition fairtraces :: "('a, 's) ioa \<Rightarrow> 'a trace set"
- where "fairtraces A = {mk_trace A $ (snd ex) | ex. ex \<in> fairexecutions A}"
+ where "fairtraces A = {mk_trace A \<cdot> (snd ex) | ex. ex \<in> fairexecutions A}"
subsection \<open>Implementation\<close>
@@ -167,13 +167,13 @@
subsubsection \<open>\<open>filter_act\<close>\<close>
-lemma filter_act_UU: "filter_act $ UU = UU"
+lemma filter_act_UU: "filter_act \<cdot> UU = UU"
by (simp add: filter_act_def)
-lemma filter_act_nil: "filter_act $ nil = nil"
+lemma filter_act_nil: "filter_act \<cdot> nil = nil"
by (simp add: filter_act_def)
-lemma filter_act_cons: "filter_act $ (x \<leadsto> xs) = fst x \<leadsto> filter_act $ xs"
+lemma filter_act_cons: "filter_act \<cdot> (x \<leadsto> xs) = fst x \<leadsto> filter_act \<cdot> xs"
by (simp add: filter_act_def)
declare filter_act_UU [simp] filter_act_nil [simp] filter_act_cons [simp]
@@ -181,17 +181,17 @@
subsubsection \<open>\<open>mk_trace\<close>\<close>
-lemma mk_trace_UU: "mk_trace A $ UU = UU"
+lemma mk_trace_UU: "mk_trace A \<cdot> UU = UU"
by (simp add: mk_trace_def)
-lemma mk_trace_nil: "mk_trace A $ nil = nil"
+lemma mk_trace_nil: "mk_trace A \<cdot> nil = nil"
by (simp add: mk_trace_def)
lemma mk_trace_cons:
- "mk_trace A $ (at \<leadsto> xs) =
+ "mk_trace A \<cdot> (at \<leadsto> xs) =
(if fst at \<in> ext A
- then fst at \<leadsto> mk_trace A $ xs
- else mk_trace A $ xs)"
+ then fst at \<leadsto> mk_trace A \<cdot> xs
+ else mk_trace A \<cdot> xs)"
by (simp add: mk_trace_def)
declare mk_trace_UU [simp] mk_trace_nil [simp] mk_trace_cons [simp]
@@ -206,7 +206,7 @@
case ex of
nil \<Rightarrow> TT
| x ## xs \<Rightarrow>
- (flift1 (\<lambda>p. Def ((s, p) \<in> trans_of A) andalso (is_exec_fragC A$xs) (snd p)) $ x)))"
+ (flift1 (\<lambda>p. Def ((s, p) \<in> trans_of A) andalso (is_exec_fragC A\<cdot>xs) (snd p)) \<cdot> x)))"
apply (rule trans)
apply (rule fix_eq4)
apply (rule is_exec_fragC_def)
@@ -214,19 +214,19 @@
apply (simp add: flift1_def)
done
-lemma is_exec_fragC_UU: "(is_exec_fragC A $ UU) s = UU"
+lemma is_exec_fragC_UU: "(is_exec_fragC A \<cdot> UU) s = UU"
apply (subst is_exec_fragC_unfold)
apply simp
done
-lemma is_exec_fragC_nil: "(is_exec_fragC A $ nil) s = TT"
+lemma is_exec_fragC_nil: "(is_exec_fragC A \<cdot> nil) s = TT"
apply (subst is_exec_fragC_unfold)
apply simp
done
lemma is_exec_fragC_cons:
- "(is_exec_fragC A $ (pr \<leadsto> xs)) s =
- (Def ((s, pr) \<in> trans_of A) andalso (is_exec_fragC A $ xs) (snd pr))"
+ "(is_exec_fragC A \<cdot> (pr \<leadsto> xs)) s =
+ (Def ((s, pr) \<in> trans_of A) andalso (is_exec_fragC A \<cdot> xs) (snd pr))"
apply (rule trans)
apply (subst is_exec_fragC_unfold)
apply (simp add: Consq_def flift1_def)
@@ -279,7 +279,7 @@
(*alternative definition of has_trace tailored for the refinement proof, as it does not
take the detour of schedules*)
-lemma has_trace_def2: "has_trace A b \<longleftrightarrow> (\<exists>ex \<in> executions A. b = mk_trace A $ (snd ex))"
+lemma has_trace_def2: "has_trace A b \<longleftrightarrow> (\<exists>ex \<in> executions A. b = mk_trace A \<cdot> (snd ex))"
apply (unfold executions_def mk_trace_def has_trace_def schedules_def has_schedule_def [abs_def])
apply auto
done
@@ -296,14 +296,14 @@
\<close>
lemma execfrag_in_sig:
- "is_trans_of A \<Longrightarrow> \<forall>s. is_exec_frag A (s, xs) \<longrightarrow> Forall (\<lambda>a. a \<in> act A) (filter_act $ xs)"
+ "is_trans_of A \<Longrightarrow> \<forall>s. is_exec_frag A (s, xs) \<longrightarrow> Forall (\<lambda>a. a \<in> act A) (filter_act \<cdot> xs)"
apply (pair_induct xs simp: is_exec_frag_def Forall_def sforall_def)
text \<open>main case\<close>
apply (auto simp add: is_trans_of_def)
done
lemma exec_in_sig:
- "is_trans_of A \<Longrightarrow> x \<in> executions A \<Longrightarrow> Forall (\<lambda>a. a \<in> act A) (filter_act $ (snd x))"
+ "is_trans_of A \<Longrightarrow> x \<in> executions A \<Longrightarrow> Forall (\<lambda>a. a \<in> act A) (filter_act \<cdot> (snd x))"
apply (simp add: executions_def)
apply (pair x)
apply (rule execfrag_in_sig [THEN spec, THEN mp])
--- a/src/HOL/HOLCF/Library/Stream.thy Mon Jul 25 14:02:29 2016 +0200
+++ b/src/HOL/HOLCF/Library/Stream.thy Mon Jul 25 21:50:04 2016 +0200
@@ -29,27 +29,26 @@
(* concatenation *)
definition
- i_rt :: "nat => 'a stream => 'a stream" where (* chops the first i elements *)
- "i_rt = (%i s. iterate i$rt$s)"
+ i_rt :: "nat \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where (* chops the first i elements *)
+ "i_rt = (\<lambda>i s. iterate i\<cdot>rt\<cdot>s)"
definition
- i_th :: "nat => 'a stream => 'a" where (* the i-th element *)
- "i_th = (%i s. ft$(i_rt i s))"
+ i_th :: "nat \<Rightarrow> 'a stream \<Rightarrow> 'a" where (* the i-th element *)
+ "i_th = (\<lambda>i s. ft\<cdot>(i_rt i s))"
definition
- sconc :: "'a stream => 'a stream => 'a stream" (infixr "ooo" 65) where
+ sconc :: "'a stream \<Rightarrow> 'a stream \<Rightarrow> 'a stream" (infixr "ooo" 65) where
"s1 ooo s2 = (case #s1 of
- enat n \<Rightarrow> (SOME s. (stream_take n$s=s1) & (i_rt n s = s2))
+ enat n \<Rightarrow> (SOME s. (stream_take n\<cdot>s = s1) \<and> (i_rt n s = s2))
| \<infinity> \<Rightarrow> s1)"
-primrec constr_sconc' :: "nat => 'a stream => 'a stream => 'a stream"
+primrec constr_sconc' :: "nat \<Rightarrow> 'a stream \<Rightarrow> 'a stream \<Rightarrow> 'a stream"
where
constr_sconc'_0: "constr_sconc' 0 s1 s2 = s2"
-| constr_sconc'_Suc: "constr_sconc' (Suc n) s1 s2 = ft$s1 &&
- constr_sconc' n (rt$s1) s2"
+| constr_sconc'_Suc: "constr_sconc' (Suc n) s1 s2 = ft\<cdot>s1 && constr_sconc' n (rt\<cdot>s1) s2"
definition
- constr_sconc :: "'a stream => 'a stream => 'a stream" where (* constructive *)
+ constr_sconc :: "'a stream \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where (* constructive *)
"constr_sconc s1 s2 = (case #s1 of
enat n \<Rightarrow> constr_sconc' n s1 s2
| \<infinity> \<Rightarrow> s1)"
@@ -65,33 +64,33 @@
lemma scons_eq_UU: "(a && s = UU) = (a = UU)"
by simp
-lemma scons_not_empty: "[| a && x = UU; a ~= UU |] ==> R"
+lemma scons_not_empty: "\<lbrakk>a && x = UU; a \<noteq> UU\<rbrakk> \<Longrightarrow> R"
by simp
-lemma stream_exhaust_eq: "(x ~= UU) = (EX a y. a ~= UU & x = a && y)"
+lemma stream_exhaust_eq: "x \<noteq> UU \<longleftrightarrow> (\<exists>a y. a \<noteq> UU \<and> x = a && y)"
by (cases x, auto)
-lemma stream_neq_UU: "x~=UU ==> EX a a_s. x=a&&a_s & a~=UU"
+lemma stream_neq_UU: "x \<noteq> UU \<Longrightarrow> \<exists>a a_s. x = a && a_s \<and> a \<noteq> UU"
by (simp add: stream_exhaust_eq,auto)
lemma stream_prefix:
- "[| a && s << t; a ~= UU |] ==> EX b tt. t = b && tt & b ~= UU & s << tt"
+ "\<lbrakk>a && s \<sqsubseteq> t; a \<noteq> UU\<rbrakk> \<Longrightarrow> \<exists>b tt. t = b && tt \<and> b \<noteq> UU \<and> s \<sqsubseteq> tt"
by (cases t, auto)
lemma stream_prefix':
- "b ~= UU ==> x << b && z =
- (x = UU | (EX a y. x = a && y & a ~= UU & a << b & y << z))"
+ "b \<noteq> UU \<Longrightarrow> x \<sqsubseteq> b && z =
+ (x = UU \<or> (\<exists>a y. x = a && y \<and> a \<noteq> UU \<and> a \<sqsubseteq> b \<and> y \<sqsubseteq> z))"
by (cases x, auto)
(*
-lemma stream_prefix1: "[| x<<y; xs<<ys |] ==> x&&xs << y&&ys"
-by (insert stream_prefix' [of y "x&&xs" ys],force)
+lemma stream_prefix1: "\<lbrakk>x \<sqsubseteq> y; xs \<sqsubseteq> ys\<rbrakk> \<Longrightarrow> x && xs \<sqsubseteq> y && ys"
+by (insert stream_prefix' [of y "x && xs" ys],force)
*)
lemma stream_flat_prefix:
- "[| x && xs << y && ys; (x::'a::flat) ~= UU|] ==> x = y & xs << ys"
-apply (case_tac "y=UU",auto)
+ "\<lbrakk>x && xs \<sqsubseteq> y && ys; (x::'a::flat) \<noteq> UU\<rbrakk> \<Longrightarrow> x = y \<and> xs \<sqsubseteq> ys"
+apply (case_tac "y = UU",auto)
apply (drule ax_flat,simp)
done
@@ -105,7 +104,7 @@
section "stream_case"
-lemma stream_case_strictf: "stream_case$UU$s=UU"
+lemma stream_case_strictf: "stream_case\<cdot>UU\<cdot>s = UU"
by (cases s, auto)
@@ -115,19 +114,19 @@
(* ----------------------------------------------------------------------- *)
-section "ft & rt"
+section "ft and rt"
-lemma ft_defin: "s~=UU ==> ft$s~=UU"
+lemma ft_defin: "s \<noteq> UU \<Longrightarrow> ft\<cdot>s \<noteq> UU"
by simp
-lemma rt_strict_rev: "rt$s~=UU ==> s~=UU"
+lemma rt_strict_rev: "rt\<cdot>s \<noteq> UU \<Longrightarrow> s \<noteq> UU"
by auto
-lemma surjectiv_scons: "(ft$s)&&(rt$s)=s"
+lemma surjectiv_scons: "(ft\<cdot>s) && (rt\<cdot>s) = s"
by (cases s, auto)
-lemma monofun_rt_mult: "x << s ==> iterate i$rt$x << iterate i$rt$s"
+lemma monofun_rt_mult: "x \<sqsubseteq> s \<Longrightarrow> iterate i\<cdot>rt\<cdot>x \<sqsubseteq> iterate i\<cdot>rt\<cdot>s"
by (rule monofun_cfun_arg)
@@ -140,13 +139,13 @@
section "stream_take"
-lemma stream_reach2: "(LUB i. stream_take i$s) = s"
+lemma stream_reach2: "(LUB i. stream_take i\<cdot>s) = s"
by (rule stream.reach)
-lemma chain_stream_take: "chain (%i. stream_take i$s)"
+lemma chain_stream_take: "chain (\<lambda>i. stream_take i\<cdot>s)"
by simp
-lemma stream_take_prefix [simp]: "stream_take n$s << s"
+lemma stream_take_prefix [simp]: "stream_take n\<cdot>s \<sqsubseteq> s"
apply (insert stream_reach2 [of s])
apply (erule subst) back
apply (rule is_ub_thelub)
@@ -154,14 +153,14 @@
done
lemma stream_take_more [rule_format]:
- "ALL x. stream_take n$x = x --> stream_take (Suc n)$x = x"
+ "\<forall>x. stream_take n\<cdot>x = x \<longrightarrow> stream_take (Suc n)\<cdot>x = x"
apply (induct_tac n,auto)
apply (case_tac "x=UU",auto)
apply (drule stream_exhaust_eq [THEN iffD1],auto)
done
lemma stream_take_lemma3 [rule_format]:
- "ALL x xs. x~=UU --> stream_take n$(x && xs) = x && xs --> stream_take n$xs=xs"
+ "\<forall>x xs. x \<noteq> UU \<longrightarrow> stream_take n\<cdot>(x && xs) = x && xs \<longrightarrow> stream_take n\<cdot>xs = xs"
apply (induct_tac n,clarsimp)
(*apply (drule sym, erule scons_not_empty, simp)*)
apply (clarify, rule stream_take_more)
@@ -170,62 +169,60 @@
done
lemma stream_take_lemma4:
- "ALL x xs. stream_take n$xs=xs --> stream_take (Suc n)$(x && xs) = x && xs"
+ "\<forall>x xs. stream_take n\<cdot>xs = xs \<longrightarrow> stream_take (Suc n)\<cdot>(x && xs) = x && xs"
by auto
lemma stream_take_idempotent [rule_format, simp]:
- "ALL s. stream_take n$(stream_take n$s) = stream_take n$s"
+ "\<forall>s. stream_take n\<cdot>(stream_take n\<cdot>s) = stream_take n\<cdot>s"
apply (induct_tac n, auto)
apply (case_tac "s=UU", auto)
apply (drule stream_exhaust_eq [THEN iffD1], auto)
done
lemma stream_take_take_Suc [rule_format, simp]:
- "ALL s. stream_take n$(stream_take (Suc n)$s) =
- stream_take n$s"
+ "\<forall>s. stream_take n\<cdot>(stream_take (Suc n)\<cdot>s) = stream_take n\<cdot>s"
apply (induct_tac n, auto)
apply (case_tac "s=UU", auto)
apply (drule stream_exhaust_eq [THEN iffD1], auto)
done
lemma mono_stream_take_pred:
- "stream_take (Suc n)$s1 << stream_take (Suc n)$s2 ==>
- stream_take n$s1 << stream_take n$s2"
-by (insert monofun_cfun_arg [of "stream_take (Suc n)$s1"
- "stream_take (Suc n)$s2" "stream_take n"], auto)
+ "stream_take (Suc n)\<cdot>s1 \<sqsubseteq> stream_take (Suc n)\<cdot>s2 \<Longrightarrow>
+ stream_take n\<cdot>s1 \<sqsubseteq> stream_take n\<cdot>s2"
+by (insert monofun_cfun_arg [of "stream_take (Suc n)\<cdot>s1"
+ "stream_take (Suc n)\<cdot>s2" "stream_take n"], auto)
(*
lemma mono_stream_take_pred:
- "stream_take (Suc n)$s1 << stream_take (Suc n)$s2 ==>
- stream_take n$s1 << stream_take n$s2"
+ "stream_take (Suc n)\<cdot>s1 \<sqsubseteq> stream_take (Suc n)\<cdot>s2 \<Longrightarrow>
+ stream_take n\<cdot>s1 \<sqsubseteq> stream_take n\<cdot>s2"
by (drule mono_stream_take [of _ _ n],simp)
*)
lemma stream_take_lemma10 [rule_format]:
- "ALL k<=n. stream_take n$s1 << stream_take n$s2
- --> stream_take k$s1 << stream_take k$s2"
+ "\<forall>k\<le>n. stream_take n\<cdot>s1 \<sqsubseteq> stream_take n\<cdot>s2 \<longrightarrow> stream_take k\<cdot>s1 \<sqsubseteq> stream_take k\<cdot>s2"
apply (induct_tac n,simp,clarsimp)
apply (case_tac "k=Suc n",blast)
apply (erule_tac x="k" in allE)
apply (drule mono_stream_take_pred,simp)
done
-lemma stream_take_le_mono : "k<=n ==> stream_take k$s1 << stream_take n$s1"
+lemma stream_take_le_mono : "k \<le> n \<Longrightarrow> stream_take k\<cdot>s1 \<sqsubseteq> stream_take n\<cdot>s1"
apply (insert chain_stream_take [of s1])
apply (drule chain_mono,auto)
done
-lemma mono_stream_take: "s1 << s2 ==> stream_take n$s1 << stream_take n$s2"
+lemma mono_stream_take: "s1 \<sqsubseteq> s2 \<Longrightarrow> stream_take n\<cdot>s1 \<sqsubseteq> stream_take n\<cdot>s2"
by (simp add: monofun_cfun_arg)
(*
-lemma stream_take_prefix [simp]: "stream_take n$s << s"
-apply (subgoal_tac "s=(LUB n. stream_take n$s)")
+lemma stream_take_prefix [simp]: "stream_take n\<cdot>s \<sqsubseteq> s"
+apply (subgoal_tac "s=(LUB n. stream_take n\<cdot>s)")
apply (erule ssubst, rule is_ub_thelub)
apply (simp only: chain_stream_take)
by (simp only: stream_reach2)
*)
-lemma stream_take_take_less:"stream_take k$(stream_take n$s) << stream_take k$s"
+lemma stream_take_take_less:"stream_take k\<cdot>(stream_take n\<cdot>s) \<sqsubseteq> stream_take k\<cdot>s"
by (rule monofun_cfun_arg,auto)
@@ -237,15 +234,15 @@
section "induction"
lemma stream_finite_ind:
- "[| stream_finite x; P UU; !!a s. [| a ~= UU; P s |] ==> P (a && s) |] ==> P x"
+ "\<lbrakk>stream_finite x; P UU; \<And>a s. \<lbrakk>a \<noteq> UU; P s\<rbrakk> \<Longrightarrow> P (a && s)\<rbrakk> \<Longrightarrow> P x"
apply (simp add: stream.finite_def,auto)
apply (erule subst)
apply (drule stream.finite_induct [of P _ x], auto)
done
lemma stream_finite_ind2:
-"[| P UU; !! x. x ~= UU ==> P (x && UU); !! y z s. [| y ~= UU; z ~= UU; P s |] ==> P (y && z && s )|] ==>
- !s. P (stream_take n$s)"
+ "\<lbrakk>P UU; \<And>x. x \<noteq> UU \<Longrightarrow> P (x && UU); \<And>y z s. \<lbrakk>y \<noteq> UU; z \<noteq> UU; P s\<rbrakk> \<Longrightarrow> P (y && z && s)\<rbrakk> \<Longrightarrow>
+ \<forall>s. P (stream_take n\<cdot>s)"
apply (rule nat_less_induct [of _ n],auto)
apply (case_tac n, auto)
apply (case_tac nat, auto)
@@ -258,7 +255,7 @@
done
lemma stream_ind2:
-"[| adm P; P UU; !!a. a ~= UU ==> P (a && UU); !!a b s. [| a ~= UU; b ~= UU; P s |] ==> P (a && b && s) |] ==> P x"
+"\<lbrakk> adm P; P UU; \<And>a. a \<noteq> UU \<Longrightarrow> P (a && UU); \<And>a b s. \<lbrakk>a \<noteq> UU; b \<noteq> UU; P s\<rbrakk> \<Longrightarrow> P (a && b && s)\<rbrakk> \<Longrightarrow> P x"
apply (insert stream.reach [of x],erule subst)
apply (erule admD, rule chain_stream_take)
apply (insert stream_finite_ind2 [of P])
@@ -273,7 +270,7 @@
section "coinduction"
-lemma stream_coind_lemma2: "!s1 s2. R s1 s2 --> ft$s1 = ft$s2 & R (rt$s1) (rt$s2) ==> stream_bisim R"
+lemma stream_coind_lemma2: "\<forall>s1 s2. R s1 s2 \<longrightarrow> ft\<cdot>s1 = ft\<cdot>s2 \<and> R (rt\<cdot>s1) (rt\<cdot>s2) \<Longrightarrow> stream_bisim R"
apply (simp add: stream.bisim_def,clarsimp)
apply (drule spec, drule spec, drule (1) mp)
apply (case_tac "x", simp)
@@ -293,29 +290,29 @@
lemma stream_finite_UU [simp]: "stream_finite UU"
by (simp add: stream.finite_def)
-lemma stream_finite_UU_rev: "~ stream_finite s ==> s ~= UU"
+lemma stream_finite_UU_rev: "\<not> stream_finite s \<Longrightarrow> s \<noteq> UU"
by (auto simp add: stream.finite_def)
-lemma stream_finite_lemma1: "stream_finite xs ==> stream_finite (x && xs)"
+lemma stream_finite_lemma1: "stream_finite xs \<Longrightarrow> stream_finite (x && xs)"
apply (simp add: stream.finite_def,auto)
apply (rule_tac x="Suc n" in exI)
apply (simp add: stream_take_lemma4)
done
-lemma stream_finite_lemma2: "[| x ~= UU; stream_finite (x && xs) |] ==> stream_finite xs"
+lemma stream_finite_lemma2: "\<lbrakk>x \<noteq> UU; stream_finite (x && xs)\<rbrakk> \<Longrightarrow> stream_finite xs"
apply (simp add: stream.finite_def, auto)
apply (rule_tac x="n" in exI)
apply (erule stream_take_lemma3,simp)
done
-lemma stream_finite_rt_eq: "stream_finite (rt$s) = stream_finite s"
+lemma stream_finite_rt_eq: "stream_finite (rt\<cdot>s) = stream_finite s"
apply (cases s, auto)
apply (rule stream_finite_lemma1, simp)
apply (rule stream_finite_lemma2,simp)
apply assumption
done
-lemma stream_finite_less: "stream_finite s ==> !t. t<<s --> stream_finite t"
+lemma stream_finite_less: "stream_finite s \<Longrightarrow> \<forall>t. t \<sqsubseteq> s \<longrightarrow> stream_finite t"
apply (erule stream_finite_ind [of s], auto)
apply (case_tac "t=UU", auto)
apply (drule stream_exhaust_eq [THEN iffD1],auto)
@@ -323,12 +320,12 @@
apply (rule stream_finite_lemma1, simp)
done
-lemma stream_take_finite [simp]: "stream_finite (stream_take n$s)"
+lemma stream_take_finite [simp]: "stream_finite (stream_take n\<cdot>s)"
apply (simp add: stream.finite_def)
apply (rule_tac x="n" in exI,simp)
done
-lemma adm_not_stream_finite: "adm (%x. ~ stream_finite x)"
+lemma adm_not_stream_finite: "adm (\<lambda>x. \<not> stream_finite x)"
apply (rule adm_upward)
apply (erule contrapos_nn)
apply (erule (1) stream_finite_less [rule_format])
@@ -346,7 +343,7 @@
lemma slen_empty [simp]: "#\<bottom> = 0"
by (simp add: slen_def stream.finite_def zero_enat_def Least_equality)
-lemma slen_scons [simp]: "x ~= \<bottom> ==> #(x&&xs) = eSuc (#xs)"
+lemma slen_scons [simp]: "x \<noteq> \<bottom> \<Longrightarrow> #(x && xs) = eSuc (#xs)"
apply (case_tac "stream_finite (x && xs)")
apply (simp add: slen_def, auto)
apply (simp add: stream.finite_def, auto simp add: eSuc_enat)
@@ -364,20 +361,20 @@
lemma slen_empty_eq: "(#x = 0) = (x = \<bottom>)"
by (cases x) auto
-lemma slen_scons_eq: "(enat (Suc n) < #x) = (? a y. x = a && y & a ~= \<bottom> & enat n < #y)"
+lemma slen_scons_eq: "(enat (Suc n) < #x) = (? a y. x = a && y \<and> a \<noteq> \<bottom> \<and> enat n < #y)"
apply (auto, case_tac "x=UU",auto)
apply (drule stream_exhaust_eq [THEN iffD1], auto)
apply (case_tac "#y") apply simp_all
apply (case_tac "#y") apply simp_all
done
-lemma slen_eSuc: "#x = eSuc n --> (? a y. x = a&&y & a ~= \<bottom> & #y = n)"
+lemma slen_eSuc: "#x = eSuc n \<longrightarrow> (\<exists>a y. x = a && y \<and> a \<noteq> \<bottom> \<and> #y = n)"
by (cases x) auto
-lemma slen_stream_take_finite [simp]: "#(stream_take n$s) ~= \<infinity>"
+lemma slen_stream_take_finite [simp]: "#(stream_take n\<cdot>s) \<noteq> \<infinity>"
by (simp add: slen_def)
-lemma slen_scons_eq_rev: "(#x < enat (Suc (Suc n))) = (!a y. x ~= a && y | a = \<bottom> | #y < enat (Suc n))"
+lemma slen_scons_eq_rev: "#x < enat (Suc (Suc n)) \<longleftrightarrow> (\<forall>a y. x \<noteq> a && y \<or> a = \<bottom> \<or> #y < enat (Suc n))"
apply (cases x, auto)
apply (simp add: zero_enat_def)
apply (case_tac "#stream") apply (simp_all add: eSuc_enat)
@@ -385,7 +382,7 @@
done
lemma slen_take_lemma4 [rule_format]:
- "!s. stream_take n$s ~= s --> #(stream_take n$s) = enat n"
+ "\<forall>s. stream_take n\<cdot>s \<noteq> s \<longrightarrow> #(stream_take n\<cdot>s) = enat n"
apply (induct n, auto simp add: enat_0)
apply (case_tac "s=UU", simp)
apply (drule stream_exhaust_eq [THEN iffD1], auto simp add: eSuc_enat)
@@ -393,23 +390,23 @@
(*
lemma stream_take_idempotent [simp]:
- "stream_take n$(stream_take n$s) = stream_take n$s"
-apply (case_tac "stream_take n$s = s")
+ "stream_take n\<cdot>(stream_take n\<cdot>s) = stream_take n\<cdot>s"
+apply (case_tac "stream_take n\<cdot>s = s")
apply (auto,insert slen_take_lemma4 [of n s]);
-by (auto,insert slen_take_lemma1 [of "stream_take n$s" n],simp)
+by (auto,insert slen_take_lemma1 [of "stream_take n\<cdot>s" n],simp)
-lemma stream_take_take_Suc [simp]: "stream_take n$(stream_take (Suc n)$s) =
- stream_take n$s"
+lemma stream_take_take_Suc [simp]: "stream_take n\<cdot>(stream_take (Suc n)\<cdot>s) =
+ stream_take n\<cdot>s"
apply (simp add: po_eq_conv,auto)
apply (simp add: stream_take_take_less)
-apply (subgoal_tac "stream_take n$s = stream_take n$(stream_take n$s)")
+apply (subgoal_tac "stream_take n\<cdot>s = stream_take n\<cdot>(stream_take n\<cdot>s)")
apply (erule ssubst)
apply (rule_tac monofun_cfun_arg)
apply (insert chain_stream_take [of s])
by (simp add: chain_def,simp)
*)
-lemma slen_take_eq: "ALL x. (enat n < #x) = (stream_take n\<cdot>x ~= x)"
+lemma slen_take_eq: "\<forall>x. enat n < #x \<longleftrightarrow> stream_take n\<cdot>x \<noteq> x"
apply (induct_tac n, auto)
apply (simp add: enat_0, clarsimp)
apply (drule not_sym)
@@ -426,38 +423,38 @@
apply simp_all
done
-lemma slen_take_eq_rev: "(#x <= enat n) = (stream_take n\<cdot>x = x)"
+lemma slen_take_eq_rev: "#x \<le> enat n \<longleftrightarrow> stream_take n\<cdot>x = x"
by (simp add: linorder_not_less [symmetric] slen_take_eq)
-lemma slen_take_lemma1: "#x = enat n ==> stream_take n\<cdot>x = x"
+lemma slen_take_lemma1: "#x = enat n \<Longrightarrow> stream_take n\<cdot>x = x"
by (rule slen_take_eq_rev [THEN iffD1], auto)
-lemma slen_rt_mono: "#s2 <= #s1 ==> #(rt$s2) <= #(rt$s1)"
+lemma slen_rt_mono: "#s2 \<le> #s1 \<Longrightarrow> #(rt\<cdot>s2) \<le> #(rt\<cdot>s1)"
apply (cases s1)
apply (cases s2, simp+)+
done
-lemma slen_take_lemma5: "#(stream_take n$s) <= enat n"
-apply (case_tac "stream_take n$s = s")
+lemma slen_take_lemma5: "#(stream_take n\<cdot>s) \<le> enat n"
+apply (case_tac "stream_take n\<cdot>s = s")
apply (simp add: slen_take_eq_rev)
apply (simp add: slen_take_lemma4)
done
-lemma slen_take_lemma2: "!x. ~stream_finite x --> #(stream_take i\<cdot>x) = enat i"
+lemma slen_take_lemma2: "\<forall>x. \<not> stream_finite x \<longrightarrow> #(stream_take i\<cdot>x) = enat i"
apply (simp add: stream.finite_def, auto)
apply (simp add: slen_take_lemma4)
done
-lemma slen_infinite: "stream_finite x = (#x ~= \<infinity>)"
+lemma slen_infinite: "stream_finite x \<longleftrightarrow> #x \<noteq> \<infinity>"
by (simp add: slen_def)
-lemma slen_mono_lemma: "stream_finite s ==> ALL t. s << t --> #s <= #t"
+lemma slen_mono_lemma: "stream_finite s \<Longrightarrow> \<forall>t. s \<sqsubseteq> t \<longrightarrow> #s \<le> #t"
apply (erule stream_finite_ind [of s], auto)
-apply (case_tac "t=UU", auto)
+apply (case_tac "t = UU", auto)
apply (drule stream_exhaust_eq [THEN iffD1], auto)
done
-lemma slen_mono: "s << t ==> #s <= #t"
+lemma slen_mono: "s \<sqsubseteq> t \<Longrightarrow> #s \<le> #t"
apply (case_tac "stream_finite t")
apply (frule stream_finite_less)
apply (erule_tac x="s" in allE, simp)
@@ -465,20 +462,20 @@
apply (simp add: slen_def)
done
-lemma iterate_lemma: "F$(iterate n$F$x) = iterate n$F$(F$x)"
+lemma iterate_lemma: "F\<cdot>(iterate n\<cdot>F\<cdot>x) = iterate n\<cdot>F\<cdot>(F\<cdot>x)"
by (insert iterate_Suc2 [of n F x], auto)
-lemma slen_rt_mult [rule_format]: "!x. enat (i + j) <= #x --> enat j <= #(iterate i$rt$x)"
+lemma slen_rt_mult [rule_format]: "\<forall>x. enat (i + j) \<le> #x \<longrightarrow> enat j \<le> #(iterate i\<cdot>rt\<cdot>x)"
apply (induct i, auto)
-apply (case_tac "x=UU", auto simp add: zero_enat_def)
+apply (case_tac "x = UU", auto simp add: zero_enat_def)
apply (drule stream_exhaust_eq [THEN iffD1], auto)
-apply (erule_tac x="y" in allE, auto)
+apply (erule_tac x = "y" in allE, auto)
apply (simp add: not_le) apply (case_tac "#y") apply (simp_all add: eSuc_enat)
apply (simp add: iterate_lemma)
done
lemma slen_take_lemma3 [rule_format]:
- "!(x::'a::flat stream) y. enat n <= #x --> x << y --> stream_take n\<cdot>x = stream_take n\<cdot>y"
+ "\<forall>(x::'a::flat stream) y. enat n \<le> #x \<longrightarrow> x \<sqsubseteq> y \<longrightarrow> stream_take n\<cdot>x = stream_take n\<cdot>y"
apply (induct_tac n, auto)
apply (case_tac "x=UU", auto)
apply (simp add: zero_enat_def)
@@ -489,20 +486,20 @@
by (drule ax_flat, simp)
lemma slen_strict_mono_lemma:
- "stream_finite t ==> !s. #(s::'a::flat stream) = #t & s << t --> s = t"
+ "stream_finite t \<Longrightarrow> \<forall>s. #(s::'a::flat stream) = #t \<and> s \<sqsubseteq> t \<longrightarrow> s = t"
apply (erule stream_finite_ind, auto)
-apply (case_tac "sa=UU", auto)
+apply (case_tac "sa = UU", auto)
apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
apply (drule ax_flat, simp)
done
-lemma slen_strict_mono: "[|stream_finite t; s ~= t; s << (t::'a::flat stream) |] ==> #s < #t"
+lemma slen_strict_mono: "\<lbrakk>stream_finite t; s \<noteq> t; s \<sqsubseteq> (t::'a::flat stream)\<rbrakk> \<Longrightarrow> #s < #t"
by (auto simp add: slen_mono less_le dest: slen_strict_mono_lemma)
-lemma stream_take_Suc_neq: "stream_take (Suc n)$s ~=s ==>
- stream_take n$s ~= stream_take (Suc n)$s"
+lemma stream_take_Suc_neq: "stream_take (Suc n)\<cdot>s \<noteq> s \<Longrightarrow>
+ stream_take n\<cdot>s \<noteq> stream_take (Suc n)\<cdot>s"
apply auto
-apply (subgoal_tac "stream_take n$s ~=s")
+apply (subgoal_tac "stream_take n\<cdot>s \<noteq> s")
apply (insert slen_take_lemma4 [of n s],auto)
apply (cases s, simp)
apply (simp add: slen_take_lemma4 eSuc_enat)
@@ -515,13 +512,13 @@
section "smap"
-lemma smap_unfold: "smap = (\<Lambda> f t. case t of x&&xs \<Rightarrow> f$x && smap$f$xs)"
+lemma smap_unfold: "smap = (\<Lambda> f t. case t of x && xs \<Rightarrow> f\<cdot>x && smap\<cdot>f\<cdot>xs)"
by (insert smap_def [where 'a='a and 'b='b, THEN eq_reflection, THEN fix_eq2], auto)
lemma smap_empty [simp]: "smap\<cdot>f\<cdot>\<bottom> = \<bottom>"
by (subst smap_unfold, simp)
-lemma smap_scons [simp]: "x~=\<bottom> ==> smap\<cdot>f\<cdot>(x&&xs) = (f\<cdot>x)&&(smap\<cdot>f\<cdot>xs)"
+lemma smap_scons [simp]: "x \<noteq> \<bottom> \<Longrightarrow> smap\<cdot>f\<cdot>(x && xs) = (f\<cdot>x) && (smap\<cdot>f\<cdot>xs)"
by (subst smap_unfold, force)
@@ -548,7 +545,7 @@
by (subst sfilter_unfold, force)
lemma sfilter_scons [simp]:
- "x ~= \<bottom> ==> sfilter\<cdot>f\<cdot>(x && xs) =
+ "x \<noteq> \<bottom> \<Longrightarrow> sfilter\<cdot>f\<cdot>(x && xs) =
If f\<cdot>x then x && sfilter\<cdot>f\<cdot>xs else sfilter\<cdot>f\<cdot>xs"
by (subst sfilter_unfold, force)
@@ -563,39 +560,39 @@
lemma i_rt_0 [simp]: "i_rt 0 s = s"
by (simp add: i_rt_def)
-lemma i_rt_Suc [simp]: "a ~= UU ==> i_rt (Suc n) (a&&s) = i_rt n s"
+lemma i_rt_Suc [simp]: "a \<noteq> UU \<Longrightarrow> i_rt (Suc n) (a&&s) = i_rt n s"
by (simp add: i_rt_def iterate_Suc2 del: iterate_Suc)
-lemma i_rt_Suc_forw: "i_rt (Suc n) s = i_rt n (rt$s)"
+lemma i_rt_Suc_forw: "i_rt (Suc n) s = i_rt n (rt\<cdot>s)"
by (simp only: i_rt_def iterate_Suc2)
-lemma i_rt_Suc_back:"i_rt (Suc n) s = rt$(i_rt n s)"
+lemma i_rt_Suc_back: "i_rt (Suc n) s = rt\<cdot>(i_rt n s)"
by (simp only: i_rt_def,auto)
-lemma i_rt_mono: "x << s ==> i_rt n x << i_rt n s"
+lemma i_rt_mono: "x << s \<Longrightarrow> i_rt n x << i_rt n s"
by (simp add: i_rt_def monofun_rt_mult)
-lemma i_rt_ij_lemma: "enat (i + j) <= #x ==> enat j <= #(i_rt i x)"
+lemma i_rt_ij_lemma: "enat (i + j) \<le> #x \<Longrightarrow> enat j \<le> #(i_rt i x)"
by (simp add: i_rt_def slen_rt_mult)
-lemma slen_i_rt_mono: "#s2 <= #s1 ==> #(i_rt n s2) <= #(i_rt n s1)"
+lemma slen_i_rt_mono: "#s2 \<le> #s1 \<Longrightarrow> #(i_rt n s2) \<le> #(i_rt n s1)"
apply (induct_tac n,auto)
apply (simp add: i_rt_Suc_back)
apply (drule slen_rt_mono,simp)
done
-lemma i_rt_take_lemma1 [rule_format]: "ALL s. i_rt n (stream_take n$s) = UU"
+lemma i_rt_take_lemma1 [rule_format]: "\<forall>s. i_rt n (stream_take n\<cdot>s) = UU"
apply (induct_tac n)
apply (simp add: i_rt_Suc_back,auto)
apply (case_tac "s=UU",auto)
apply (drule stream_exhaust_eq [THEN iffD1],auto)
done
-lemma i_rt_slen: "(i_rt n s = UU) = (stream_take n$s = s)"
+lemma i_rt_slen: "i_rt n s = UU \<longleftrightarrow> stream_take n\<cdot>s = s"
apply auto
apply (insert i_rt_ij_lemma [of n "Suc 0" s])
apply (subgoal_tac "#(i_rt n s)=0")
- apply (case_tac "stream_take n$s = s",simp+)
+ apply (case_tac "stream_take n\<cdot>s = s",simp+)
apply (insert slen_take_eq [rule_format,of n s],simp)
apply (cases "#s") apply (simp_all add: zero_enat_def)
apply (simp add: slen_take_eq)
@@ -604,7 +601,7 @@
apply (simp_all add: zero_enat_def)
done
-lemma i_rt_lemma_slen: "#s=enat n ==> i_rt n s = UU"
+lemma i_rt_lemma_slen: "#s=enat n \<Longrightarrow> i_rt n s = UU"
by (simp add: i_rt_slen slen_take_lemma1)
lemma stream_finite_i_rt [simp]: "stream_finite (i_rt n s) = stream_finite s"
@@ -613,15 +610,15 @@
apply (simp add: i_rt_Suc_back stream_finite_rt_eq)+
done
-lemma take_i_rt_len_lemma: "ALL sl x j t. enat sl = #x & n <= sl &
- #(stream_take n$x) = enat t & #(i_rt n x)= enat j
- --> enat (j + t) = #x"
+lemma take_i_rt_len_lemma: "\<forall>sl x j t. enat sl = #x \<and> n \<le> sl \<and>
+ #(stream_take n\<cdot>x) = enat t \<and> #(i_rt n x) = enat j
+ \<longrightarrow> enat (j + t) = #x"
apply (induct n, auto)
apply (simp add: zero_enat_def)
apply (case_tac "x=UU",auto)
apply (simp add: zero_enat_def)
apply (drule stream_exhaust_eq [THEN iffD1],clarsimp)
-apply (subgoal_tac "EX k. enat k = #y",clarify)
+apply (subgoal_tac "\<exists>k. enat k = #y",clarify)
apply (erule_tac x="k" in allE)
apply (erule_tac x="y" in allE,auto)
apply (erule_tac x="THE p. Suc p = t" in allE,auto)
@@ -634,7 +631,7 @@
done
lemma take_i_rt_len:
-"[| enat sl = #x; n <= sl; #(stream_take n$x) = enat t; #(i_rt n x) = enat j |] ==>
+"\<lbrakk>enat sl = #x; n \<le> sl; #(stream_take n\<cdot>x) = enat t; #(i_rt n x) = enat j\<rbrakk> \<Longrightarrow>
enat (j + t) = #x"
by (blast intro: take_i_rt_len_lemma [rule_format])
@@ -652,7 +649,7 @@
done
lemma i_th_stream_take_Suc [rule_format]:
- "ALL s. i_th n (stream_take (Suc n)$s) = i_th n s"
+ "\<forall>s. i_th n (stream_take (Suc n)\<cdot>s) = i_th n s"
apply (induct_tac n,auto)
apply (simp add: i_th_def)
apply (case_tac "s=UU",auto)
@@ -662,21 +659,21 @@
apply (simp add: i_th_def i_rt_Suc_forw)
done
-lemma i_th_last: "i_th n s && UU = i_rt n (stream_take (Suc n)$s)"
-apply (insert surjectiv_scons [of "i_rt n (stream_take (Suc n)$s)"])
+lemma i_th_last: "i_th n s && UU = i_rt n (stream_take (Suc n)\<cdot>s)"
+apply (insert surjectiv_scons [of "i_rt n (stream_take (Suc n)\<cdot>s)"])
apply (rule i_th_stream_take_Suc [THEN subst])
apply (simp add: i_th_def i_rt_Suc_back [symmetric])
by (simp add: i_rt_take_lemma1)
lemma i_th_last_eq:
-"i_th n s1 = i_th n s2 ==> i_rt n (stream_take (Suc n)$s1) = i_rt n (stream_take (Suc n)$s2)"
+"i_th n s1 = i_th n s2 \<Longrightarrow> i_rt n (stream_take (Suc n)\<cdot>s1) = i_rt n (stream_take (Suc n)\<cdot>s2)"
apply (insert i_th_last [of n s1])
apply (insert i_th_last [of n s2])
apply auto
done
lemma i_th_prefix_lemma:
-"[| k <= n; stream_take (Suc n)$s1 << stream_take (Suc n)$s2 |] ==>
+"\<lbrakk>k \<le> n; stream_take (Suc n)\<cdot>s1 << stream_take (Suc n)\<cdot>s2\<rbrakk> \<Longrightarrow>
i_th k s1 << i_th k s2"
apply (insert i_th_stream_take_Suc [of k s1, THEN sym])
apply (insert i_th_stream_take_Suc [of k s2, THEN sym],auto)
@@ -687,9 +684,9 @@
done
lemma take_i_rt_prefix_lemma1:
- "stream_take (Suc n)$s1 << stream_take (Suc n)$s2 ==>
- i_rt (Suc n) s1 << i_rt (Suc n) s2 ==>
- i_rt n s1 << i_rt n s2 & stream_take n$s1 << stream_take n$s2"
+ "stream_take (Suc n)\<cdot>s1 << stream_take (Suc n)\<cdot>s2 \<Longrightarrow>
+ i_rt (Suc n) s1 << i_rt (Suc n) s2 \<Longrightarrow>
+ i_rt n s1 << i_rt n s2 \<and> stream_take n\<cdot>s1 << stream_take n\<cdot>s2"
apply auto
apply (insert i_th_prefix_lemma [of n n s1 s2])
apply (rule i_th_i_rt_step,auto)
@@ -697,19 +694,18 @@
done
lemma take_i_rt_prefix_lemma:
-"[| stream_take n$s1 << stream_take n$s2; i_rt n s1 << i_rt n s2 |] ==> s1 << s2"
+"\<lbrakk>stream_take n\<cdot>s1 << stream_take n\<cdot>s2; i_rt n s1 << i_rt n s2\<rbrakk> \<Longrightarrow> s1 << s2"
apply (case_tac "n=0",simp)
apply (auto)
-apply (subgoal_tac "stream_take 0$s1 << stream_take 0$s2 &
- i_rt 0 s1 << i_rt 0 s2")
+apply (subgoal_tac "stream_take 0\<cdot>s1 << stream_take 0\<cdot>s2 \<and> i_rt 0 s1 << i_rt 0 s2")
defer 1
apply (rule zero_induct,blast)
apply (blast dest: take_i_rt_prefix_lemma1)
apply simp
done
-lemma streams_prefix_lemma: "(s1 << s2) =
- (stream_take n$s1 << stream_take n$s2 & i_rt n s1 << i_rt n s2)"
+lemma streams_prefix_lemma: "s1 << s2 \<longleftrightarrow>
+ (stream_take n\<cdot>s1 << stream_take n\<cdot>s2 \<and> i_rt n s1 << i_rt n s2)"
apply auto
apply (simp add: monofun_cfun_arg)
apply (simp add: i_rt_mono)
@@ -717,7 +713,7 @@
done
lemma streams_prefix_lemma1:
- "[| stream_take n$s1 = stream_take n$s2; i_rt n s1 = i_rt n s2 |] ==> s1 = s2"
+ "\<lbrakk>stream_take n\<cdot>s1 = stream_take n\<cdot>s2; i_rt n s1 = i_rt n s2\<rbrakk> \<Longrightarrow> s1 = s2"
apply (simp add: po_eq_conv,auto)
apply (insert streams_prefix_lemma)
apply blast+
@@ -731,10 +727,10 @@
lemma UU_sconc [simp]: " UU ooo s = s "
by (simp add: sconc_def zero_enat_def)
-lemma scons_neq_UU: "a~=UU ==> a && s ~=UU"
+lemma scons_neq_UU: "a \<noteq> UU \<Longrightarrow> a && s \<noteq> UU"
by auto
-lemma singleton_sconc [rule_format, simp]: "x~=UU --> (x && UU) ooo y = x && y"
+lemma singleton_sconc [rule_format, simp]: "x \<noteq> UU \<longrightarrow> (x && UU) ooo y = x && y"
apply (simp add: sconc_def zero_enat_def eSuc_def split: enat.splits, auto)
apply (rule someI2_ex,auto)
apply (rule_tac x="x && y" in exI,auto)
@@ -743,7 +739,7 @@
by (drule stream_exhaust_eq [THEN iffD1],auto)
lemma ex_sconc [rule_format]:
- "ALL k y. #x = enat k --> (EX w. stream_take k$w = x & i_rt k w = y)"
+ "\<forall>k y. #x = enat k \<longrightarrow> (\<exists>w. stream_take k\<cdot>w = x \<and> i_rt k w = y)"
apply (case_tac "#x")
apply (rule stream_finite_ind [of x],auto)
apply (simp add: stream.finite_def)
@@ -753,7 +749,7 @@
apply (rule_tac x="a && w" in exI,auto)
done
-lemma rt_sconc1: "enat n = #x ==> i_rt n (x ooo y) = y"
+lemma rt_sconc1: "enat n = #x \<Longrightarrow> i_rt n (x ooo y) = y"
apply (simp add: sconc_def split: enat.splits, arith?,auto)
apply (rule someI2_ex,auto)
apply (drule ex_sconc,simp)
@@ -777,7 +773,7 @@
apply (simp add: sconc_def)
done
-lemma stream_take_sconc [simp]: "enat n = #x ==> stream_take n$(x ooo y) = x"
+lemma stream_take_sconc [simp]: "enat n = #x \<Longrightarrow> stream_take n\<cdot>(x ooo y) = x"
apply (simp add: sconc_def)
apply (cases "#x")
apply auto
@@ -785,7 +781,7 @@
apply (drule ex_sconc,simp)
done
-lemma scons_sconc [rule_format,simp]: "a~=UU --> (a && x) ooo y = a && x ooo y"
+lemma scons_sconc [rule_format,simp]: "a \<noteq> UU \<longrightarrow> (a && x) ooo y = a && x ooo y"
apply (cases "#x",auto)
apply (simp add: sconc_def eSuc_enat)
apply (rule someI2_ex)
@@ -799,7 +795,7 @@
apply (simp add: sconc_def)
done
-lemma ft_sconc: "x ~= UU ==> ft$(x ooo y) = ft$x"
+lemma ft_sconc: "x \<noteq> UU \<Longrightarrow> ft\<cdot>(x ooo y) = ft\<cdot>x"
by (cases x) auto
lemma sconc_assoc: "(x ooo y) ooo z = x ooo y ooo z"
@@ -825,7 +821,7 @@
apply (erule cont_sconc_lemma2)
done
-lemma sconc_mono: "y << y' ==> x ooo y << x ooo y'"
+lemma sconc_mono: "y << y' \<Longrightarrow> x ooo y << x ooo y'"
by (rule cont_sconc [THEN cont2mono, THEN monofunE])
lemma sconc_mono1 [simp]: "x << x ooo y"
@@ -833,7 +829,7 @@
(* ----------------------------------------------------------------------- *)
-lemma empty_sconc [simp]: "(x ooo y = UU) = (x = UU & y = UU)"
+lemma empty_sconc [simp]: "x ooo y = UU \<longleftrightarrow> x = UU \<and> y = UU"
apply (case_tac "#x",auto)
apply (insert sconc_mono1 [of x y])
apply auto
@@ -841,11 +837,11 @@
(* ----------------------------------------------------------------------- *)
-lemma rt_sconc [rule_format, simp]: "s~=UU --> rt$(s ooo x) = rt$s ooo x"
+lemma rt_sconc [rule_format, simp]: "s \<noteq> UU \<longrightarrow> rt\<cdot>(s ooo x) = rt\<cdot>s ooo x"
by (cases s, auto)
lemma i_th_sconc_lemma [rule_format]:
- "ALL x y. enat n < #x --> i_th n (x ooo y) = i_th n x"
+ "\<forall>x y. enat n < #x \<longrightarrow> i_th n (x ooo y) = i_th n x"
apply (induct_tac n, auto)
apply (simp add: enat_0 i_th_def)
apply (simp add: slen_empty_eq ft_sconc)
@@ -861,7 +857,7 @@
(* ----------------------------------------------------------------------- *)
-lemma sconc_lemma [rule_format, simp]: "ALL s. stream_take n$s ooo i_rt n s = s"
+lemma sconc_lemma [rule_format, simp]: "\<forall>s. stream_take n\<cdot>s ooo i_rt n s = s"
apply (induct_tac n,auto)
apply (case_tac "s=UU",auto)
apply (drule stream_exhaust_eq [THEN iffD1],auto)
@@ -871,26 +867,26 @@
subsection "pointwise equality"
(* ----------------------------------------------------------------------- *)
-lemma ex_last_stream_take_scons: "stream_take (Suc n)$s =
- stream_take n$s ooo i_rt n (stream_take (Suc n)$s)"
-by (insert sconc_lemma [of n "stream_take (Suc n)$s"],simp)
+lemma ex_last_stream_take_scons: "stream_take (Suc n)\<cdot>s =
+ stream_take n\<cdot>s ooo i_rt n (stream_take (Suc n)\<cdot>s)"
+by (insert sconc_lemma [of n "stream_take (Suc n)\<cdot>s"],simp)
lemma i_th_stream_take_eq:
-"!!n. ALL n. i_th n s1 = i_th n s2 ==> stream_take n$s1 = stream_take n$s2"
+ "\<And>n. \<forall>n. i_th n s1 = i_th n s2 \<Longrightarrow> stream_take n\<cdot>s1 = stream_take n\<cdot>s2"
apply (induct_tac n,auto)
-apply (subgoal_tac "stream_take (Suc na)$s1 =
- stream_take na$s1 ooo i_rt na (stream_take (Suc na)$s1)")
- apply (subgoal_tac "i_rt na (stream_take (Suc na)$s1) =
- i_rt na (stream_take (Suc na)$s2)")
- apply (subgoal_tac "stream_take (Suc na)$s2 =
- stream_take na$s2 ooo i_rt na (stream_take (Suc na)$s2)")
+apply (subgoal_tac "stream_take (Suc na)\<cdot>s1 =
+ stream_take na\<cdot>s1 ooo i_rt na (stream_take (Suc na)\<cdot>s1)")
+ apply (subgoal_tac "i_rt na (stream_take (Suc na)\<cdot>s1) =
+ i_rt na (stream_take (Suc na)\<cdot>s2)")
+ apply (subgoal_tac "stream_take (Suc na)\<cdot>s2 =
+ stream_take na\<cdot>s2 ooo i_rt na (stream_take (Suc na)\<cdot>s2)")
apply (insert ex_last_stream_take_scons,simp)
apply blast
apply (erule_tac x="na" in allE)
apply (insert i_th_last_eq [of _ s1 s2])
by blast+
-lemma pointwise_eq_lemma[rule_format]: "ALL n. i_th n s1 = i_th n s2 ==> s1 = s2"
+lemma pointwise_eq_lemma[rule_format]: "\<forall>n. i_th n s1 = i_th n s2 \<Longrightarrow> s1 = s2"
by (insert i_th_stream_take_eq [THEN stream.take_lemma],blast)
(* ----------------------------------------------------------------------- *)
@@ -898,17 +894,17 @@
(* ----------------------------------------------------------------------- *)
lemma slen_sconc_finite1:
- "[| #(x ooo y) = \<infinity>; enat n = #x |] ==> #y = \<infinity>"
-apply (case_tac "#y ~= \<infinity>",auto)
+ "\<lbrakk>#(x ooo y) = \<infinity>; enat n = #x\<rbrakk> \<Longrightarrow> #y = \<infinity>"
+apply (case_tac "#y \<noteq> \<infinity>",auto)
apply (drule_tac y=y in rt_sconc1)
apply (insert stream_finite_i_rt [of n "x ooo y"])
apply (simp add: slen_infinite)
done
-lemma slen_sconc_infinite1: "#x=\<infinity> ==> #(x ooo y) = \<infinity>"
+lemma slen_sconc_infinite1: "#x=\<infinity> \<Longrightarrow> #(x ooo y) = \<infinity>"
by (simp add: sconc_def)
-lemma slen_sconc_infinite2: "#y=\<infinity> ==> #(x ooo y) = \<infinity>"
+lemma slen_sconc_infinite2: "#y=\<infinity> \<Longrightarrow> #(x ooo y) = \<infinity>"
apply (case_tac "#x")
apply (simp add: sconc_def)
apply (rule someI2_ex)
@@ -918,7 +914,7 @@
apply (fastforce simp add: slen_infinite,auto)
by (simp add: sconc_def)
-lemma sconc_finite: "(#x~=\<infinity> & #y~=\<infinity>) = (#(x ooo y)~=\<infinity>)"
+lemma sconc_finite: "#x \<noteq> \<infinity> \<and> #y \<noteq> \<infinity> \<longleftrightarrow> #(x ooo y) \<noteq> \<infinity>"
apply auto
apply (metis not_infinity_eq slen_sconc_finite1)
apply (metis not_infinity_eq slen_sconc_infinite1)
@@ -927,7 +923,7 @@
(* ----------------------------------------------------------------------- *)
-lemma slen_sconc_mono3: "[| enat n = #x; enat k = #(x ooo y) |] ==> n <= k"
+lemma slen_sconc_mono3: "\<lbrakk>enat n = #x; enat k = #(x ooo y)\<rbrakk> \<Longrightarrow> n \<le> k"
apply (insert slen_mono [of "x" "x ooo y"])
apply (cases "#x") apply simp_all
apply (cases "#(x ooo y)") apply simp_all
@@ -937,7 +933,7 @@
subsection "finite slen"
(* ----------------------------------------------------------------------- *)
-lemma slen_sconc: "[| enat n = #x; enat m = #y |] ==> #(x ooo y) = enat (n + m)"
+lemma slen_sconc: "\<lbrakk>enat n = #x; enat m = #y\<rbrakk> \<Longrightarrow> #(x ooo y) = enat (n + m)"
apply (case_tac "#(x ooo y)")
apply (frule_tac y=y in rt_sconc1)
apply (insert take_i_rt_len [of "THE j. enat j = #(x ooo y)" "x ooo y" n n m],simp)
@@ -949,9 +945,9 @@
subsection "flat prefix"
(* ----------------------------------------------------------------------- *)
-lemma sconc_prefix: "(s1::'a::flat stream) << s2 ==> EX t. s1 ooo t = s2"
+lemma sconc_prefix: "(s1::'a::flat stream) << s2 \<Longrightarrow> \<exists>t. s1 ooo t = s2"
apply (case_tac "#s1")
- apply (subgoal_tac "stream_take nat$s1 = stream_take nat$s2")
+ apply (subgoal_tac "stream_take nat\<cdot>s1 = stream_take nat\<cdot>s2")
apply (rule_tac x="i_rt nat s2" in exI)
apply (simp add: sconc_def)
apply (rule someI2_ex)
@@ -967,18 +963,18 @@
subsection "continuity"
(* ----------------------------------------------------------------------- *)
-lemma chain_sconc: "chain S ==> chain (%i. (x ooo S i))"
+lemma chain_sconc: "chain S \<Longrightarrow> chain (\<lambda>i. (x ooo S i))"
by (simp add: chain_def,auto simp add: sconc_mono)
-lemma chain_scons: "chain S ==> chain (%i. a && S i)"
+lemma chain_scons: "chain S \<Longrightarrow> chain (\<lambda>i. a && S i)"
apply (simp add: chain_def,auto)
apply (rule monofun_cfun_arg,simp)
done
-lemma contlub_scons_lemma: "chain S ==> (LUB i. a && S i) = a && (LUB i. S i)"
+lemma contlub_scons_lemma: "chain S \<Longrightarrow> (LUB i. a && S i) = a && (LUB i. S i)"
by (rule cont2contlubE [OF cont_Rep_cfun2, symmetric])
-lemma finite_lub_sconc: "chain Y ==> (stream_finite x) ==>
+lemma finite_lub_sconc: "chain Y \<Longrightarrow> stream_finite x \<Longrightarrow>
(LUB i. x ooo Y i) = (x ooo (LUB i. Y i))"
apply (rule stream_finite_ind [of x])
apply (auto)
@@ -987,13 +983,13 @@
done
lemma contlub_sconc_lemma:
- "chain Y ==> (LUB i. x ooo Y i) = (x ooo (LUB i. Y i))"
+ "chain Y \<Longrightarrow> (LUB i. x ooo Y i) = (x ooo (LUB i. Y i))"
apply (case_tac "#x=\<infinity>")
apply (simp add: sconc_def)
apply (drule finite_lub_sconc,auto simp add: slen_infinite)
done
-lemma monofun_sconc: "monofun (%y. x ooo y)"
+lemma monofun_sconc: "monofun (\<lambda>y. x ooo y)"
by (simp add: monofun_def sconc_mono)
--- a/src/HOL/HOLCF/ex/Dagstuhl.thy Mon Jul 25 14:02:29 2016 +0200
+++ b/src/HOL/HOLCF/ex/Dagstuhl.thy Mon Jul 25 21:50:04 2016 +0200
@@ -7,11 +7,11 @@
definition
YS :: "'a stream" where
- "YS = fix$(LAM x. y && x)"
+ "YS = fix\<cdot>(LAM x. y && x)"
definition
YYS :: "'a stream" where
- "YYS = fix$(LAM z. y && y && z)"
+ "YYS = fix\<cdot>(LAM z. y && y && z)"
lemma YS_def2: "YS = y && YS"
apply (rule trans)
--- a/src/HOL/HOLCF/ex/Dnat.thy Mon Jul 25 14:02:29 2016 +0200
+++ b/src/HOL/HOLCF/ex/Dnat.thy Mon Jul 25 21:50:04 2016 +0200
@@ -11,17 +11,17 @@
domain dnat = dzero | dsucc (dpred :: dnat)
definition
- iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a" where
- "iterator = fix $ (LAM h n f x.
- case n of dzero => x
- | dsucc $ m => f $ (h $ m $ f $ x))"
+ iterator :: "dnat \<rightarrow> ('a \<rightarrow> 'a) \<rightarrow> 'a \<rightarrow> 'a" where
+ "iterator = fix\<cdot>(LAM h n f x.
+ case n of dzero \<Rightarrow> x
+ | dsucc\<cdot>m \<Rightarrow> f\<cdot>(h\<cdot>m\<cdot>f\<cdot>x))"
text \<open>
\medskip Expand fixed point properties.
\<close>
lemma iterator_def2:
- "iterator = (LAM n f x. case n of dzero => x | dsucc$m => f$(iterator$m$f$x))"
+ "iterator = (LAM n f x. case n of dzero \<Rightarrow> x | dsucc\<cdot>m \<Rightarrow> f\<cdot>(iterator\<cdot>m\<cdot>f\<cdot>x))"
apply (rule trans)
apply (rule fix_eq2)
apply (rule iterator_def [THEN eq_reflection])
@@ -31,17 +31,17 @@
text \<open>\medskip Recursive properties.\<close>
-lemma iterator1: "iterator $ UU $ f $ x = UU"
+lemma iterator1: "iterator\<cdot>UU\<cdot>f\<cdot>x = UU"
apply (subst iterator_def2)
apply simp
done
-lemma iterator2: "iterator $ dzero $ f $ x = x"
+lemma iterator2: "iterator\<cdot>dzero\<cdot>f\<cdot>x = x"
apply (subst iterator_def2)
apply simp
done
-lemma iterator3: "n ~= UU ==> iterator $ (dsucc $ n) $ f $ x = f $ (iterator $ n $ f $ x)"
+lemma iterator3: "n \<noteq> UU \<Longrightarrow> iterator\<cdot>(dsucc\<cdot>n)\<cdot>f\<cdot>x = f\<cdot>(iterator\<cdot>n\<cdot>f\<cdot>x)"
apply (rule trans)
apply (subst iterator_def2)
apply simp
@@ -50,7 +50,7 @@
lemmas iterator_rews = iterator1 iterator2 iterator3
-lemma dnat_flat: "ALL x y::dnat. x<<y --> x=UU | x=y"
+lemma dnat_flat: "\<forall>x y::dnat. x \<sqsubseteq> y \<longrightarrow> x = UU \<or> x = y"
apply (rule allI)
apply (induct_tac x)
apply fast
@@ -62,7 +62,7 @@
apply (rule allI)
apply (case_tac y)
apply (fast intro!: bottomI)
- apply (thin_tac "ALL y. dnat << y --> dnat = UU | dnat = y")
+ apply (thin_tac "\<forall>y. dnat \<sqsubseteq> y \<longrightarrow> dnat = UU \<or> dnat = y")
apply simp
apply (simp (no_asm_simp))
apply (drule_tac x="dnata" in spec)
--- a/src/HOL/HOLCF/ex/Fix2.thy Mon Jul 25 14:02:29 2016 +0200
+++ b/src/HOL/HOLCF/ex/Fix2.thy Mon Jul 25 21:50:04 2016 +0200
@@ -10,9 +10,9 @@
begin
axiomatization
- gix :: "('a->'a)->'a" where
- gix1_def: "F$(gix$F) = gix$F" and
- gix2_def: "F$y=y ==> gix$F << y"
+ gix :: "('a \<rightarrow> 'a) \<rightarrow>'a" where
+ gix1_def: "F\<cdot>(gix\<cdot>F) = gix\<cdot>F" and
+ gix2_def: "F\<cdot>y = y \<Longrightarrow> gix\<cdot>F << y"
lemma lemma1: "fix = gix"
@@ -24,7 +24,7 @@
apply (rule fix_eq [symmetric])
done
-lemma lemma2: "gix$F=lub(range(%i. iterate i$F$UU))"
+lemma lemma2: "gix\<cdot>F = lub (range (\<lambda>i. iterate i\<cdot>F\<cdot>UU))"
apply (rule lemma1 [THEN subst])
apply (rule fix_def2)
done
--- a/src/HOL/HOLCF/ex/Focus_ex.thy Mon Jul 25 14:02:29 2016 +0200
+++ b/src/HOL/HOLCF/ex/Focus_ex.thy Mon Jul 25 21:50:04 2016 +0200
@@ -107,46 +107,43 @@
instance tc :: (pcpo, pcpo) pcpo by (rule tc_arity)
axiomatization
- Rf :: "('b stream * ('b,'c) tc stream * 'c stream * ('b,'c) tc stream) => bool"
+ Rf :: "('b stream * ('b,'c) tc stream * 'c stream * ('b,'c) tc stream) \<Rightarrow> bool"
definition
- is_f :: "('b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) => bool" where
- "is_f f = (!i1 i2 o1 o2. f$(i1,i2) = (o1,o2) --> Rf(i1,i2,o1,o2))"
+ is_f :: "('b stream * ('b,'c) tc stream \<rightarrow> 'c stream * ('b,'c) tc stream) \<Rightarrow> bool" where
+ "is_f f \<longleftrightarrow> (\<forall>i1 i2 o1 o2. f\<cdot>(i1, i2) = (o1, o2) \<longrightarrow> Rf (i1, i2, o1, o2))"
definition
- is_net_g :: "('b stream *('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) =>
- 'b stream => 'c stream => bool" where
- "is_net_g f x y == (? z.
- (y,z) = f$(x,z) &
- (!oy hz. (oy,hz) = f$(x,hz) --> z << hz))"
+ is_net_g :: "('b stream * ('b,'c) tc stream \<rightarrow> 'c stream * ('b,'c) tc stream) \<Rightarrow>
+ 'b stream \<Rightarrow> 'c stream \<Rightarrow> bool" where
+ "is_net_g f x y \<equiv> (\<exists>z.
+ (y, z) = f\<cdot>(x,z) \<and>
+ (\<forall>oy hz. (oy, hz) = f\<cdot>(x, hz) \<longrightarrow> z << hz))"
definition
- is_g :: "('b stream -> 'c stream) => bool" where
- "is_g g == (? f. is_f f & (!x y. g$x = y --> is_net_g f x y))"
+ is_g :: "('b stream \<rightarrow> 'c stream) \<Rightarrow> bool" where
+ "is_g g \<equiv> (\<exists>f. is_f f \<and> (\<forall>x y. g\<cdot>x = y \<longrightarrow> is_net_g f x y))"
definition
- def_g :: "('b stream -> 'c stream) => bool" where
- "def_g g == (? f. is_f f & g = (LAM x. fst (f$(x,fix$(LAM k. snd (f$(x,k)))))))"
+ def_g :: "('b stream \<rightarrow> 'c stream) => bool" where
+ "def_g g \<equiv> (\<exists>f. is_f f \<and> g = (LAM x. fst (f\<cdot>(x, fix\<cdot>(LAM k. snd (f\<cdot>(x, k)))))))"
(* first some logical trading *)
lemma lemma1:
-"is_g(g) =
- (? f. is_f(f) & (!x.(? z. (g$x,z) = f$(x,z) &
- (! w y. (y,w) = f$(x,w) --> z << w))))"
+ "is_g g \<longleftrightarrow>
+ (\<exists>f. is_f(f) \<and> (\<forall>x.(\<exists>z. (g\<cdot>x,z) = f\<cdot>(x,z) \<and> (\<forall>w y. (y, w) = f\<cdot>(x, w) \<longrightarrow> z << w))))"
apply (simp add: is_g_def is_net_g_def)
apply fast
done
lemma lemma2:
-"(? f. is_f(f) & (!x. (? z. (g$x,z) = f$(x,z) &
- (!w y. (y,w) = f$(x,w) --> z << w))))
- =
- (? f. is_f(f) & (!x. ? z.
- g$x = fst (f$(x,z)) &
- z = snd (f$(x,z)) &
- (! w y. (y,w) = f$(x,w) --> z << w)))"
+ "(\<exists>f. is_f f \<and> (\<forall>x. (\<exists>z. (g\<cdot>x, z) = f\<cdot>(x, z) \<and> (\<forall>w y. (y, w) = f\<cdot>(x,w) \<longrightarrow> z << w)))) \<longleftrightarrow>
+ (\<exists>f. is_f f \<and> (\<forall>x. \<exists>z.
+ g\<cdot>x = fst (f\<cdot>(x, z)) \<and>
+ z = snd (f\<cdot>(x, z)) \<and>
+ (\<forall>w y. (y, w) = f\<cdot>(x, w) \<longrightarrow> z << w)))"
apply (rule iffI)
apply (erule exE)
apply (rule_tac x = "f" in exI)
@@ -180,7 +177,7 @@
apply simp
done
-lemma lemma3: "def_g(g) --> is_g(g)"
+lemma lemma3: "def_g g \<longrightarrow> is_g g"
apply (tactic \<open>simp_tac (put_simpset HOL_ss @{context}
addsimps [@{thm def_g_def}, @{thm lemma1}, @{thm lemma2}]) 1\<close>)
apply (rule impI)
@@ -189,7 +186,7 @@
apply (erule conjE)+
apply (erule conjI)
apply (intro strip)
-apply (rule_tac x = "fix$ (LAM k. snd (f$(x,k)))" in exI)
+apply (rule_tac x = "fix\<cdot>(LAM k. snd (f\<cdot>(x, k)))" in exI)
apply (rule conjI)
apply (simp)
apply (rule prod_eqI, simp, simp)
@@ -205,7 +202,7 @@
apply simp
done
-lemma lemma4: "is_g(g) --> def_g(g)"
+lemma lemma4: "is_g g \<longrightarrow> def_g g"
apply (tactic \<open>simp_tac (put_simpset HOL_ss @{context}
delsimps (@{thms HOL.ex_simps} @ @{thms HOL.all_simps})
addsimps [@{thm lemma1}, @{thm lemma2}, @{thm def_g_def}]) 1\<close>)
@@ -218,12 +215,12 @@
apply (erule_tac x = "x" in allE)
apply (erule exE)
apply (erule conjE)+
-apply (subgoal_tac "fix$ (LAM k. snd (f$(x, k))) = z")
+apply (subgoal_tac "fix\<cdot>(LAM k. snd (f\<cdot>(x, k))) = z")
apply simp
-apply (subgoal_tac "! w y. f$(x, w) = (y, w) --> z << w")
+apply (subgoal_tac "\<forall>w y. f\<cdot>(x, w) = (y, w) \<longrightarrow> z << w")
apply (rule fix_eqI)
apply simp
-apply (subgoal_tac "f$(x, za) = (fst (f$(x,za)) ,za)")
+apply (subgoal_tac "f\<cdot>(x, za) = (fst (f\<cdot>(x, za)), za)")
apply fast
apply (rule prod_eqI, simp, simp)
apply (intro strip)
@@ -242,18 +239,14 @@
done
lemma L2:
-"(? f.
- is_f(f::'b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream))
- -->
- (? g. def_g(g::'b stream -> 'c stream ))"
+ "(\<exists>f. is_f (f::'b stream * ('b,'c) tc stream \<rightarrow> 'c stream * ('b,'c) tc stream)) \<longrightarrow>
+ (\<exists>g. def_g (g::'b stream \<rightarrow> 'c stream))"
apply (simp add: def_g_def)
done
theorem conservative_loopback:
-"(? f.
- is_f(f::'b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream))
- -->
- (? g. is_g(g::'b stream -> 'c stream ))"
+ "(\<exists>f. is_f (f::'b stream * ('b,'c) tc stream \<rightarrow> 'c stream * ('b,'c) tc stream)) \<longrightarrow>
+ (\<exists>g. is_g (g::'b stream \<rightarrow> 'c stream))"
apply (rule loopback_eq [THEN subst])
apply (rule L2)
done
--- a/src/HOL/HOLCF/ex/Hoare.thy Mon Jul 25 14:02:29 2016 +0200
+++ b/src/HOL/HOLCF/ex/Hoare.thy Mon Jul 25 21:50:04 2016 +0200
@@ -24,64 +24,64 @@
begin
axiomatization
- b1 :: "'a -> tr" and
- b2 :: "'a -> tr" and
- g :: "'a -> 'a"
+ b1 :: "'a \<rightarrow> tr" and
+ b2 :: "'a \<rightarrow> tr" and
+ g :: "'a \<rightarrow> 'a"
definition
- p :: "'a -> 'a" where
- "p = fix$(LAM f. LAM x. If b1$x then f$(g$x) else x)"
+ p :: "'a \<rightarrow> 'a" where
+ "p = fix\<cdot>(LAM f. LAM x. If b1\<cdot>x then f\<cdot>(g\<cdot>x) else x)"
definition
- q :: "'a -> 'a" where
- "q = fix$(LAM f. LAM x. If b1$x orelse b2$x then f$(g$x) else x)"
+ q :: "'a \<rightarrow> 'a" where
+ "q = fix\<cdot>(LAM f. LAM x. If b1\<cdot>x orelse b2\<cdot>x then f\<cdot>(g\<cdot>x) else x)"
(* --------- pure HOLCF logic, some little lemmas ------ *)
-lemma hoare_lemma2: "b~=TT ==> b=FF | b=UU"
+lemma hoare_lemma2: "b \<noteq> TT \<Longrightarrow> b = FF \<or> b = UU"
apply (rule Exh_tr [THEN disjE])
apply blast+
done
-lemma hoare_lemma3: " (ALL k. b1$(iterate k$g$x) = TT) | (EX k. b1$(iterate k$g$x)~=TT)"
+lemma hoare_lemma3: "(\<forall>k. b1\<cdot>(iterate k\<cdot>g\<cdot>x) = TT) \<or> (\<exists>k. b1\<cdot>(iterate k\<cdot>g\<cdot>x) \<noteq> TT)"
apply blast
done
-lemma hoare_lemma4: "(EX k. b1$(iterate k$g$x) ~= TT) ==>
- EX k. b1$(iterate k$g$x) = FF | b1$(iterate k$g$x) = UU"
+lemma hoare_lemma4: "(\<exists>k. b1\<cdot>(iterate k\<cdot>g\<cdot>x) \<noteq> TT) \<Longrightarrow>
+ \<exists>k. b1\<cdot>(iterate k\<cdot>g\<cdot>x) = FF \<or> b1\<cdot>(iterate k\<cdot>g\<cdot>x) = UU"
apply (erule exE)
apply (rule exI)
apply (rule hoare_lemma2)
apply assumption
done
-lemma hoare_lemma5: "[|(EX k. b1$(iterate k$g$x) ~= TT);
- k=Least(%n. b1$(iterate n$g$x) ~= TT)|] ==>
- b1$(iterate k$g$x)=FF | b1$(iterate k$g$x)=UU"
+lemma hoare_lemma5: "\<lbrakk>(\<exists>k. b1\<cdot>(iterate k\<cdot>g\<cdot>x) \<noteq> TT);
+ k = Least (\<lambda>n. b1\<cdot>(iterate n\<cdot>g\<cdot>x) \<noteq> TT)\<rbrakk> \<Longrightarrow>
+ b1\<cdot>(iterate k\<cdot>g\<cdot>x) = FF \<or> b1\<cdot>(iterate k\<cdot>g\<cdot>x) = UU"
apply hypsubst
apply (rule hoare_lemma2)
apply (erule exE)
apply (erule LeastI)
done
-lemma hoare_lemma6: "b=UU ==> b~=TT"
+lemma hoare_lemma6: "b = UU \<Longrightarrow> b \<noteq> TT"
apply hypsubst
apply (rule dist_eq_tr)
done
-lemma hoare_lemma7: "b=FF ==> b~=TT"
+lemma hoare_lemma7: "b = FF \<Longrightarrow> b \<noteq> TT"
apply hypsubst
apply (rule dist_eq_tr)
done
-lemma hoare_lemma8: "[|(EX k. b1$(iterate k$g$x) ~= TT);
- k=Least(%n. b1$(iterate n$g$x) ~= TT)|] ==>
- ALL m. m < k --> b1$(iterate m$g$x)=TT"
+lemma hoare_lemma8: "\<lbrakk>(\<exists>k. b1\<cdot>(iterate k\<cdot>g\<cdot>x) \<noteq> TT);
+ k = Least (\<lambda>n. b1\<cdot>(iterate n\<cdot>g\<cdot>x) \<noteq> TT)\<rbrakk> \<Longrightarrow>
+ \<forall>m. m < k \<longrightarrow> b1\<cdot>(iterate m\<cdot>g\<cdot>x) = TT"
apply hypsubst
apply (erule exE)
apply (intro strip)
-apply (rule_tac p = "b1$ (iterate m$g$x) " in trE)
+apply (rule_tac p = "b1\<cdot>(iterate m\<cdot>g\<cdot>x)" in trE)
prefer 2 apply (assumption)
apply (rule le_less_trans [THEN less_irrefl [THEN notE]])
prefer 2 apply (assumption)
@@ -94,19 +94,19 @@
done
-lemma hoare_lemma28: "f$(y::'a)=(UU::tr) ==> f$UU = UU"
+lemma hoare_lemma28: "f\<cdot>(y::'a) = (UU::tr) \<Longrightarrow> f\<cdot>UU = UU"
by (rule strictI)
(* ----- access to definitions ----- *)
-lemma p_def3: "p$x = If b1$x then p$(g$x) else x"
+lemma p_def3: "p\<cdot>x = If b1\<cdot>x then p\<cdot>(g\<cdot>x) else x"
apply (rule trans)
apply (rule p_def [THEN eq_reflection, THEN fix_eq3])
apply simp
done
-lemma q_def3: "q$x = If b1$x orelse b2$x then q$(g$x) else x"
+lemma q_def3: "q\<cdot>x = If b1\<cdot>x orelse b2\<cdot>x then q\<cdot>(g\<cdot>x) else x"
apply (rule trans)
apply (rule q_def [THEN eq_reflection, THEN fix_eq3])
apply simp
@@ -114,16 +114,16 @@
(** --------- proofs about iterations of p and q ---------- **)
-lemma hoare_lemma9: "(ALL m. m< Suc k --> b1$(iterate m$g$x)=TT) -->
- p$(iterate k$g$x)=p$x"
+lemma hoare_lemma9: "(\<forall>m. m < Suc k \<longrightarrow> b1\<cdot>(iterate m\<cdot>g\<cdot>x) = TT) \<longrightarrow>
+ p\<cdot>(iterate k\<cdot>g\<cdot>x) = p\<cdot>x"
apply (induct_tac k)
apply (simp (no_asm))
apply (simp (no_asm))
apply (intro strip)
-apply (rule_tac s = "p$ (iterate n$g$x) " in trans)
+apply (rule_tac s = "p\<cdot>(iterate n\<cdot>g\<cdot>x)" in trans)
apply (rule trans)
apply (rule_tac [2] p_def3 [symmetric])
-apply (rule_tac s = "TT" and t = "b1$ (iterate n$g$x) " in ssubst)
+apply (rule_tac s = "TT" and t = "b1\<cdot>(iterate n\<cdot>g\<cdot>x)" in ssubst)
apply (rule mp)
apply (erule spec)
apply (simp (no_asm) add: less_Suc_eq)
@@ -136,16 +136,16 @@
apply simp
done
-lemma hoare_lemma24: "(ALL m. m< Suc k --> b1$(iterate m$g$x)=TT) -->
- q$(iterate k$g$x)=q$x"
+lemma hoare_lemma24: "(\<forall>m. m < Suc k \<longrightarrow> b1\<cdot>(iterate m\<cdot>g\<cdot>x) = TT) \<longrightarrow>
+ q\<cdot>(iterate k\<cdot>g\<cdot>x) = q\<cdot>x"
apply (induct_tac k)
apply (simp (no_asm))
apply (simp (no_asm) add: less_Suc_eq)
apply (intro strip)
-apply (rule_tac s = "q$ (iterate n$g$x) " in trans)
+apply (rule_tac s = "q\<cdot>(iterate n\<cdot>g\<cdot>x)" in trans)
apply (rule trans)
apply (rule_tac [2] q_def3 [symmetric])
-apply (rule_tac s = "TT" and t = "b1$ (iterate n$g$x) " in ssubst)
+apply (rule_tac s = "TT" and t = "b1\<cdot>(iterate n\<cdot>g\<cdot>x)" in ssubst)
apply blast
apply simp
apply (erule mp)
@@ -153,16 +153,16 @@
apply (fast dest!: less_Suc_eq [THEN iffD1])
done
-(* -------- results about p for case (EX k. b1$(iterate k$g$x)~=TT) ------- *)
+(* -------- results about p for case (\<exists>k. b1\<cdot>(iterate k\<cdot>g\<cdot>x) \<noteq> TT) ------- *)
lemma hoare_lemma10:
- "EX k. b1$(iterate k$g$x) ~= TT
- ==> Suc k = (LEAST n. b1$(iterate n$g$x) ~= TT) ==> p$(iterate k$g$x) = p$x"
+ "\<exists>k. b1\<cdot>(iterate k\<cdot>g\<cdot>x) \<noteq> TT
+ \<Longrightarrow> Suc k = (LEAST n. b1\<cdot>(iterate n\<cdot>g\<cdot>x) \<noteq> TT) \<Longrightarrow> p\<cdot>(iterate k\<cdot>g\<cdot>x) = p\<cdot>x"
by (rule hoare_lemma8 [THEN hoare_lemma9 [THEN mp]])
-lemma hoare_lemma11: "(EX n. b1$(iterate n$g$x) ~= TT) ==>
- k=(LEAST n. b1$(iterate n$g$x) ~= TT) & b1$(iterate k$g$x)=FF
- --> p$x = iterate k$g$x"
+lemma hoare_lemma11: "(\<exists>n. b1\<cdot>(iterate n\<cdot>g\<cdot>x) \<noteq> TT) \<Longrightarrow>
+ k = (LEAST n. b1\<cdot>(iterate n\<cdot>g\<cdot>x) \<noteq> TT) \<and> b1\<cdot>(iterate k\<cdot>g\<cdot>x) = FF
+ \<longrightarrow> p\<cdot>x = iterate k\<cdot>g\<cdot>x"
apply (case_tac "k")
apply hypsubst
apply (simp (no_asm))
@@ -179,7 +179,7 @@
apply assumption
apply (rule trans)
apply (rule p_def3)
-apply (rule_tac s = "TT" and t = "b1$ (iterate nat$g$x) " in ssubst)
+apply (rule_tac s = "TT" and t = "b1\<cdot>(iterate nat\<cdot>g\<cdot>x)" in ssubst)
apply (rule hoare_lemma8 [THEN spec, THEN mp])
apply assumption
apply assumption
@@ -192,9 +192,9 @@
apply simp
done
-lemma hoare_lemma12: "(EX n. b1$(iterate n$g$x) ~= TT) ==>
- k=Least(%n. b1$(iterate n$g$x)~=TT) & b1$(iterate k$g$x)=UU
- --> p$x = UU"
+lemma hoare_lemma12: "(\<exists>n. b1\<cdot>(iterate n\<cdot>g\<cdot>x) \<noteq> TT) \<Longrightarrow>
+ k = Least (\<lambda>n. b1\<cdot>(iterate n\<cdot>g\<cdot>x) \<noteq> TT) \<and> b1\<cdot>(iterate k\<cdot>g\<cdot>x) = UU
+ \<longrightarrow> p\<cdot>x = UU"
apply (case_tac "k")
apply hypsubst
apply (simp (no_asm))
@@ -213,7 +213,7 @@
apply assumption
apply (rule trans)
apply (rule p_def3)
-apply (rule_tac s = "TT" and t = "b1$ (iterate nat$g$x) " in ssubst)
+apply (rule_tac s = "TT" and t = "b1\<cdot>(iterate nat\<cdot>g\<cdot>x)" in ssubst)
apply (rule hoare_lemma8 [THEN spec, THEN mp])
apply assumption
apply assumption
@@ -224,85 +224,85 @@
apply simp
done
-(* -------- results about p for case (ALL k. b1$(iterate k$g$x)=TT) ------- *)
+(* -------- results about p for case (\<forall>k. b1\<cdot>(iterate k\<cdot>g\<cdot>x) = TT) ------- *)
-lemma fernpass_lemma: "(ALL k. b1$(iterate k$g$x)=TT) ==> ALL k. p$(iterate k$g$x) = UU"
+lemma fernpass_lemma: "(\<forall>k. b1\<cdot>(iterate k\<cdot>g\<cdot>x) = TT) \<Longrightarrow> \<forall>k. p\<cdot>(iterate k\<cdot>g\<cdot>x) = UU"
apply (rule p_def [THEN eq_reflection, THEN def_fix_ind])
apply simp
apply simp
apply (simp (no_asm))
apply (rule allI)
-apply (rule_tac s = "TT" and t = "b1$ (iterate k$g$x) " in ssubst)
+apply (rule_tac s = "TT" and t = "b1\<cdot>(iterate k\<cdot>g\<cdot>x)" in ssubst)
apply (erule spec)
apply (simp)
apply (rule iterate_Suc [THEN subst])
apply (erule spec)
done
-lemma hoare_lemma16: "(ALL k. b1$(iterate k$g$x)=TT) ==> p$x = UU"
+lemma hoare_lemma16: "(\<forall>k. b1\<cdot>(iterate k\<cdot>g\<cdot>x) = TT) \<Longrightarrow> p\<cdot>x = UU"
apply (rule_tac F1 = "g" and t = "x" in iterate_0 [THEN subst])
apply (erule fernpass_lemma [THEN spec])
done
-(* -------- results about q for case (ALL k. b1$(iterate k$g$x)=TT) ------- *)
+(* -------- results about q for case (\<forall>k. b1\<cdot>(iterate k\<cdot>g\<cdot>x) = TT) ------- *)
-lemma hoare_lemma17: "(ALL k. b1$(iterate k$g$x)=TT) ==> ALL k. q$(iterate k$g$x) = UU"
+lemma hoare_lemma17: "(\<forall>k. b1\<cdot>(iterate k\<cdot>g\<cdot>x) = TT) \<Longrightarrow> \<forall>k. q\<cdot>(iterate k\<cdot>g\<cdot>x) = UU"
apply (rule q_def [THEN eq_reflection, THEN def_fix_ind])
apply simp
apply simp
apply (rule allI)
apply (simp (no_asm))
-apply (rule_tac s = "TT" and t = "b1$ (iterate k$g$x) " in ssubst)
+apply (rule_tac s = "TT" and t = "b1\<cdot>(iterate k\<cdot>g\<cdot>x)" in ssubst)
apply (erule spec)
apply (simp)
apply (rule iterate_Suc [THEN subst])
apply (erule spec)
done
-lemma hoare_lemma18: "(ALL k. b1$(iterate k$g$x)=TT) ==> q$x = UU"
+lemma hoare_lemma18: "(\<forall>k. b1\<cdot>(iterate k\<cdot>g\<cdot>x) = TT) \<Longrightarrow> q\<cdot>x = UU"
apply (rule_tac F1 = "g" and t = "x" in iterate_0 [THEN subst])
apply (erule hoare_lemma17 [THEN spec])
done
lemma hoare_lemma19:
- "(ALL k. (b1::'a->tr)$(iterate k$g$x)=TT) ==> b1$(UU::'a) = UU | (ALL y. b1$(y::'a)=TT)"
+ "(\<forall>k. (b1::'a\<rightarrow>tr)\<cdot>(iterate k\<cdot>g\<cdot>x) = TT) \<Longrightarrow> b1\<cdot>(UU::'a) = UU \<or> (\<forall>y. b1\<cdot>(y::'a) = TT)"
apply (rule flat_codom)
apply (rule_tac t = "x" in iterate_0 [THEN subst])
apply (erule spec)
done
-lemma hoare_lemma20: "(ALL y. b1$(y::'a)=TT) ==> ALL k. q$(iterate k$g$(x::'a)) = UU"
+lemma hoare_lemma20: "(\<forall>y. b1\<cdot>(y::'a) = TT) \<Longrightarrow> \<forall>k. q\<cdot>(iterate k\<cdot>g\<cdot>(x::'a)) = UU"
apply (rule q_def [THEN eq_reflection, THEN def_fix_ind])
apply simp
apply simp
apply (rule allI)
apply (simp (no_asm))
-apply (rule_tac s = "TT" and t = "b1$ (iterate k$g$ (x::'a))" in ssubst)
+apply (rule_tac s = "TT" and t = "b1\<cdot>(iterate k\<cdot>g\<cdot>(x::'a))" in ssubst)
apply (erule spec)
apply (simp)
apply (rule iterate_Suc [THEN subst])
apply (erule spec)
done
-lemma hoare_lemma21: "(ALL y. b1$(y::'a)=TT) ==> q$(x::'a) = UU"
+lemma hoare_lemma21: "(\<forall>y. b1\<cdot>(y::'a) = TT) \<Longrightarrow> q\<cdot>(x::'a) = UU"
apply (rule_tac F1 = "g" and t = "x" in iterate_0 [THEN subst])
apply (erule hoare_lemma20 [THEN spec])
done
-lemma hoare_lemma22: "b1$(UU::'a)=UU ==> q$(UU::'a) = UU"
+lemma hoare_lemma22: "b1\<cdot>(UU::'a) = UU \<Longrightarrow> q\<cdot>(UU::'a) = UU"
apply (subst q_def3)
apply simp
done
-(* -------- results about q for case (EX k. b1$(iterate k$g$x) ~= TT) ------- *)
+(* -------- results about q for case (\<exists>k. b1\<cdot>(iterate k\<cdot>g\<cdot>x) \<noteq> TT) ------- *)
-lemma hoare_lemma25: "EX k. b1$(iterate k$g$x) ~= TT
- ==> Suc k = (LEAST n. b1$(iterate n$g$x) ~= TT) ==> q$(iterate k$g$x) = q$x"
+lemma hoare_lemma25: "\<exists>k. b1\<cdot>(iterate k\<cdot>g\<cdot>x) \<noteq> TT
+ \<Longrightarrow> Suc k = (LEAST n. b1\<cdot>(iterate n\<cdot>g\<cdot>x) \<noteq> TT) \<Longrightarrow> q\<cdot>(iterate k\<cdot>g\<cdot>x) = q\<cdot>x"
by (rule hoare_lemma8 [THEN hoare_lemma24 [THEN mp]])
-lemma hoare_lemma26: "(EX n. b1$(iterate n$g$x)~=TT) ==>
- k=Least(%n. b1$(iterate n$g$x) ~= TT) & b1$(iterate k$g$x) =FF
- --> q$x = q$(iterate k$g$x)"
+lemma hoare_lemma26: "(\<exists>n. b1\<cdot>(iterate n\<cdot>g\<cdot>x) \<noteq> TT) \<Longrightarrow>
+ k = Least (\<lambda>n. b1\<cdot>(iterate n\<cdot>g\<cdot>x) \<noteq> TT) \<and> b1\<cdot>(iterate k\<cdot>g\<cdot>x) = FF
+ \<longrightarrow> q\<cdot>x = q\<cdot>(iterate k\<cdot>g\<cdot>x)"
apply (case_tac "k")
apply hypsubst
apply (intro strip)
@@ -316,7 +316,7 @@
apply assumption
apply (rule trans)
apply (rule q_def3)
-apply (rule_tac s = "TT" and t = "b1$ (iterate nat$g$x) " in ssubst)
+apply (rule_tac s = "TT" and t = "b1\<cdot>(iterate nat\<cdot>g\<cdot>x)" in ssubst)
apply (rule hoare_lemma8 [THEN spec, THEN mp])
apply assumption
apply assumption
@@ -325,9 +325,9 @@
done
-lemma hoare_lemma27: "(EX n. b1$(iterate n$g$x) ~= TT) ==>
- k=Least(%n. b1$(iterate n$g$x)~=TT) & b1$(iterate k$g$x)=UU
- --> q$x = UU"
+lemma hoare_lemma27: "(\<exists>n. b1\<cdot>(iterate n\<cdot>g\<cdot>x) \<noteq> TT) \<Longrightarrow>
+ k = Least(\<lambda>n. b1\<cdot>(iterate n\<cdot>g\<cdot>x) \<noteq> TT) \<and> b1\<cdot>(iterate k\<cdot>g\<cdot>x) = UU
+ \<longrightarrow> q\<cdot>x = UU"
apply (case_tac "k")
apply hypsubst
apply (simp (no_asm))
@@ -345,7 +345,7 @@
apply assumption
apply (rule trans)
apply (rule q_def3)
-apply (rule_tac s = "TT" and t = "b1$ (iterate nat$g$x) " in ssubst)
+apply (rule_tac s = "TT" and t = "b1\<cdot>(iterate nat\<cdot>g\<cdot>x)" in ssubst)
apply (rule hoare_lemma8 [THEN spec, THEN mp])
apply assumption
apply assumption
@@ -356,9 +356,9 @@
apply (simp)
done
-(* ------- (ALL k. b1$(iterate k$g$x)=TT) ==> q o p = q ----- *)
+(* ------- (\<forall>k. b1\<cdot>(iterate k\<cdot>g\<cdot>x) = TT) \<Longrightarrow> q \<circ> p = q ----- *)
-lemma hoare_lemma23: "(ALL k. b1$(iterate k$g$x)=TT) ==> q$(p$x) = q$x"
+lemma hoare_lemma23: "(\<forall>k. b1\<cdot>(iterate k\<cdot>g\<cdot>x) = TT) \<Longrightarrow> q\<cdot>(p\<cdot>x) = q\<cdot>x"
apply (subst hoare_lemma16)
apply assumption
apply (rule hoare_lemma19 [THEN disjE])
@@ -375,9 +375,9 @@
apply (rule refl)
done
-(* ------------ EX k. b1~(iterate k$g$x) ~= TT ==> q o p = q ----- *)
+(* ------------ \<exists>k. b1\<cdot>(iterate k\<cdot>g\<cdot>x) \<noteq> TT \<Longrightarrow> q \<circ> p = q ----- *)
-lemma hoare_lemma29: "EX k. b1$(iterate k$g$x) ~= TT ==> q$(p$x) = q$x"
+lemma hoare_lemma29: "\<exists>k. b1\<cdot>(iterate k\<cdot>g\<cdot>x) \<noteq> TT \<Longrightarrow> q\<cdot>(p\<cdot>x) = q\<cdot>x"
apply (rule hoare_lemma5 [THEN disjE])
apply assumption
apply (rule refl)
@@ -410,7 +410,7 @@
apply (rule refl)
done
-(* ------ the main proof q o p = q ------ *)
+(* ------ the main proof q \<circ> p = q ------ *)
theorem hoare_main: "q oo p = q"
apply (rule cfun_eqI)
--- a/src/HOL/HOLCF/ex/Loop.thy Mon Jul 25 14:02:29 2016 +0200
+++ b/src/HOL/HOLCF/ex/Loop.thy Mon Jul 25 21:50:04 2016 +0200
@@ -9,24 +9,24 @@
begin
definition
- step :: "('a -> tr)->('a -> 'a)->'a->'a" where
- "step = (LAM b g x. If b$x then g$x else x)"
+ step :: "('a \<rightarrow> tr) \<rightarrow> ('a \<rightarrow> 'a) \<rightarrow> 'a \<rightarrow> 'a" where
+ "step = (LAM b g x. If b\<cdot>x then g\<cdot>x else x)"
definition
- while :: "('a -> tr)->('a -> 'a)->'a->'a" where
- "while = (LAM b g. fix$(LAM f x. If b$x then f$(g$x) else x))"
+ while :: "('a \<rightarrow> tr) \<rightarrow> ('a \<rightarrow> 'a) \<rightarrow> 'a \<rightarrow> 'a" where
+ "while = (LAM b g. fix\<cdot>(LAM f x. If b\<cdot>x then f\<cdot>(g\<cdot>x) else x))"
(* ------------------------------------------------------------------------- *)
(* access to definitions *)
(* ------------------------------------------------------------------------- *)
-lemma step_def2: "step$b$g$x = If b$x then g$x else x"
+lemma step_def2: "step\<cdot>b\<cdot>g\<cdot>x = If b\<cdot>x then g\<cdot>x else x"
apply (unfold step_def)
apply simp
done
-lemma while_def2: "while$b$g = fix$(LAM f x. If b$x then f$(g$x) else x)"
+lemma while_def2: "while\<cdot>b\<cdot>g = fix\<cdot>(LAM f x. If b\<cdot>x then f\<cdot>(g\<cdot>x) else x)"
apply (unfold while_def)
apply simp
done
@@ -36,13 +36,13 @@
(* rekursive properties of while *)
(* ------------------------------------------------------------------------- *)
-lemma while_unfold: "while$b$g$x = If b$x then while$b$g$(g$x) else x"
+lemma while_unfold: "while\<cdot>b\<cdot>g\<cdot>x = If b\<cdot>x then while\<cdot>b\<cdot>g\<cdot>(g\<cdot>x) else x"
apply (rule trans)
apply (rule while_def2 [THEN fix_eq5])
apply simp
done
-lemma while_unfold2: "ALL x. while$b$g$x = while$b$g$(iterate k$(step$b$g)$x)"
+lemma while_unfold2: "\<forall>x. while\<cdot>b\<cdot>g\<cdot>x = while\<cdot>b\<cdot>g\<cdot>(iterate k\<cdot>(step\<cdot>b\<cdot>g)\<cdot>x)"
apply (induct_tac k)
apply simp
apply (rule allI)
@@ -52,10 +52,10 @@
apply (rule trans)
apply (erule_tac [2] spec)
apply (subst step_def2)
-apply (rule_tac p = "b$x" in trE)
+apply (rule_tac p = "b\<cdot>x" in trE)
apply simp
apply (subst while_unfold)
-apply (rule_tac s = "UU" and t = "b$UU" in ssubst)
+apply (rule_tac s = "UU" and t = "b\<cdot>UU" in ssubst)
apply (erule strictI)
apply simp
apply simp
@@ -64,8 +64,8 @@
apply simp
done
-lemma while_unfold3: "while$b$g$x = while$b$g$(step$b$g$x)"
-apply (rule_tac s = "while$b$g$ (iterate (Suc 0) $ (step$b$g) $x) " in trans)
+lemma while_unfold3: "while\<cdot>b\<cdot>g\<cdot>x = while\<cdot>b\<cdot>g\<cdot>(step\<cdot>b\<cdot>g\<cdot>x)"
+apply (rule_tac s = "while\<cdot>b\<cdot>g\<cdot>(iterate (Suc 0)\<cdot>(step\<cdot>b\<cdot>g)\<cdot>x)" in trans)
apply (rule while_unfold2 [THEN spec])
apply simp
done
@@ -75,8 +75,8 @@
(* properties of while and iterations *)
(* ------------------------------------------------------------------------- *)
-lemma loop_lemma1: "[| EX y. b$y=FF; iterate k$(step$b$g)$x = UU |]
- ==>iterate(Suc k)$(step$b$g)$x=UU"
+lemma loop_lemma1: "\<lbrakk>EX y. b\<cdot>y = FF; iterate k\<cdot>(step\<cdot>b\<cdot>g)\<cdot>x = UU\<rbrakk>
+ \<Longrightarrow> iterate(Suc k)\<cdot>(step\<cdot>b\<cdot>g)\<cdot>x = UU"
apply (simp (no_asm))
apply (rule trans)
apply (rule step_def2)
@@ -86,35 +86,35 @@
apply simp_all
done
-lemma loop_lemma2: "[|EX y. b$y=FF;iterate (Suc k)$(step$b$g)$x ~=UU |]==>
- iterate k$(step$b$g)$x ~=UU"
+lemma loop_lemma2: "\<lbrakk>\<exists>y. b\<cdot>y = FF; iterate (Suc k)\<cdot>(step\<cdot>b\<cdot>g)\<cdot>x \<noteq> UU\<rbrakk> \<Longrightarrow>
+ iterate k\<cdot>(step\<cdot>b\<cdot>g)\<cdot>x \<noteq> UU"
apply (blast intro: loop_lemma1)
done
lemma loop_lemma3 [rule_format (no_asm)]:
- "[| ALL x. INV x & b$x=TT & g$x~=UU --> INV (g$x);
- EX y. b$y=FF; INV x |]
- ==> iterate k$(step$b$g)$x ~=UU --> INV (iterate k$(step$b$g)$x)"
+ "\<lbrakk>\<forall>x. INV x \<and> b\<cdot>x = TT \<and> g\<cdot>x \<noteq> UU \<longrightarrow> INV (g\<cdot>x);
+ \<exists>y. b\<cdot>y = FF; INV x\<rbrakk>
+ \<Longrightarrow> iterate k\<cdot>(step\<cdot>b\<cdot>g)\<cdot>x \<noteq> UU \<longrightarrow> INV (iterate k\<cdot>(step\<cdot>b\<cdot>g)\<cdot>x)"
apply (induct_tac "k")
apply (simp (no_asm_simp))
apply (intro strip)
apply (simp (no_asm) add: step_def2)
-apply (rule_tac p = "b$ (iterate n$ (step$b$g) $x) " in trE)
+apply (rule_tac p = "b\<cdot>(iterate n\<cdot>(step\<cdot>b\<cdot>g)\<cdot>x)" in trE)
apply (erule notE)
apply (simp add: step_def2)
apply (simp (no_asm_simp))
apply (rule mp)
apply (erule spec)
apply (simp (no_asm_simp) del: iterate_Suc add: loop_lemma2)
-apply (rule_tac s = "iterate (Suc n) $ (step$b$g) $x"
- and t = "g$ (iterate n$ (step$b$g) $x) " in ssubst)
+apply (rule_tac s = "iterate (Suc n)\<cdot>(step\<cdot>b\<cdot>g)\<cdot>x"
+ and t = "g\<cdot>(iterate n\<cdot>(step\<cdot>b\<cdot>g)\<cdot>x)" in ssubst)
prefer 2 apply (assumption)
apply (simp add: step_def2)
apply (drule (1) loop_lemma2, simp)
done
lemma loop_lemma4 [rule_format]:
- "ALL x. b$(iterate k$(step$b$g)$x)=FF --> while$b$g$x= iterate k$(step$b$g)$x"
+ "\<forall>x. b\<cdot>(iterate k\<cdot>(step\<cdot>b\<cdot>g)\<cdot>x) = FF \<longrightarrow> while\<cdot>b\<cdot>g\<cdot>x = iterate k\<cdot>(step\<cdot>b\<cdot>g)\<cdot>x"
apply (induct_tac k)
apply (simp (no_asm))
apply (intro strip)
@@ -129,18 +129,18 @@
done
lemma loop_lemma5 [rule_format (no_asm)]:
- "ALL k. b$(iterate k$(step$b$g)$x) ~= FF ==>
- ALL m. while$b$g$(iterate m$(step$b$g)$x)=UU"
+ "\<forall>k. b\<cdot>(iterate k\<cdot>(step\<cdot>b\<cdot>g)\<cdot>x) \<noteq> FF \<Longrightarrow>
+ \<forall>m. while\<cdot>b\<cdot>g\<cdot>(iterate m\<cdot>(step\<cdot>b\<cdot>g)\<cdot>x) = UU"
apply (simplesubst while_def2)
apply (rule fix_ind)
apply simp
apply simp
apply (rule allI)
apply (simp (no_asm))
-apply (rule_tac p = "b$ (iterate m$ (step$b$g) $x) " in trE)
+apply (rule_tac p = "b\<cdot>(iterate m\<cdot>(step\<cdot>b\<cdot>g)\<cdot>x)" in trE)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
-apply (rule_tac s = "xa$ (iterate (Suc m) $ (step$b$g) $x) " in trans)
+apply (rule_tac s = "xa\<cdot>(iterate (Suc m)\<cdot>(step\<cdot>b\<cdot>g)\<cdot>x)" in trans)
apply (erule_tac [2] spec)
apply (rule cfun_arg_cong)
apply (rule trans)
@@ -149,12 +149,12 @@
apply blast
done
-lemma loop_lemma6: "ALL k. b$(iterate k$(step$b$g)$x) ~= FF ==> while$b$g$x=UU"
+lemma loop_lemma6: "\<forall>k. b\<cdot>(iterate k\<cdot>(step\<cdot>b\<cdot>g)\<cdot>x) \<noteq> FF \<Longrightarrow> while\<cdot>b\<cdot>g\<cdot>x = UU"
apply (rule_tac t = "x" in iterate_0 [THEN subst])
apply (erule loop_lemma5)
done
-lemma loop_lemma7: "while$b$g$x ~= UU ==> EX k. b$(iterate k$(step$b$g)$x) = FF"
+lemma loop_lemma7: "while\<cdot>b\<cdot>g\<cdot>x \<noteq> UU \<Longrightarrow> \<exists>k. b\<cdot>(iterate k\<cdot>(step\<cdot>b\<cdot>g)\<cdot>x) = FF"
apply (blast intro: loop_lemma6)
done
@@ -164,10 +164,10 @@
(* ------------------------------------------------------------------------- *)
lemma loop_inv2:
-"[| (ALL y. INV y & b$y=TT & g$y ~= UU --> INV (g$y));
- (ALL y. INV y & b$y=FF --> Q y);
- INV x; while$b$g$x~=UU |] ==> Q (while$b$g$x)"
-apply (rule_tac P = "%k. b$ (iterate k$ (step$b$g) $x) =FF" in exE)
+"\<lbrakk>(\<forall>y. INV y \<and> b\<cdot>y = TT \<and> g\<cdot>y \<noteq> UU \<longrightarrow> INV (g\<cdot>y));
+ (\<forall>y. INV y \<and> b\<cdot>y = FF \<longrightarrow> Q y);
+ INV x; while\<cdot>b\<cdot>g\<cdot>x \<noteq> UU\<rbrakk> \<Longrightarrow> Q (while\<cdot>b\<cdot>g\<cdot>x)"
+apply (rule_tac P = "\<lambda>k. b\<cdot>(iterate k\<cdot>(step\<cdot>b\<cdot>g)\<cdot>x) = FF" in exE)
apply (erule loop_lemma7)
apply (simplesubst loop_lemma4)
apply assumption
@@ -184,11 +184,11 @@
lemma loop_inv:
assumes premP: "P(x)"
- and premI: "!!y. P y ==> INV y"
- and premTT: "!!y. [| INV y; b$y=TT; g$y~=UU|] ==> INV (g$y)"
- and premFF: "!!y. [| INV y; b$y=FF|] ==> Q y"
- and premW: "while$b$g$x ~= UU"
- shows "Q (while$b$g$x)"
+ and premI: "\<And>y. P y \<Longrightarrow> INV y"
+ and premTT: "\<And>y. \<lbrakk>INV y; b\<cdot>y = TT; g\<cdot>y \<noteq> UU\<rbrakk> \<Longrightarrow> INV (g\<cdot>y)"
+ and premFF: "\<And>y. \<lbrakk>INV y; b\<cdot>y = FF\<rbrakk> \<Longrightarrow> Q y"
+ and premW: "while\<cdot>b\<cdot>g\<cdot>x \<noteq> UU"
+ shows "Q (while\<cdot>b\<cdot>g\<cdot>x)"
apply (rule loop_inv2)
apply (rule_tac [3] premP [THEN premI])
apply (rule_tac [3] premW)
@@ -197,4 +197,3 @@
done
end
-