# HG changeset patch # User wenzelm # Date 1469476204 -7200 # Node ID b0d31c7def86ff0fb5978b375978dad1b45c5e22 # Parent 6c2c16fef8f18663b8ed4a44d97c690c456a9df4 more symbols; diff -r 6c2c16fef8f1 -r b0d31c7def86 src/HOL/HOLCF/Cfun.thy --- 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 \some lemmata for functions with flat/chfin domain/range types\ 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)\s = Y n\s" apply (rule allI) apply (subst contlub_cfun_fun) apply assumption diff -r 6c2c16fef8f1 -r b0d31c7def86 src/HOL/HOLCF/FOCUS/Fstreams.thy --- 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\(flift2 f)" definition jth :: "nat => 'a fstream => 'a" where @@ -51,7 +51,7 @@ fsfilter' ("(_'(C')_)" [64,63] 63) -lemma ft_fsingleton[simp]: "ft$() = Def a" +lemma ft_fsingleton[simp]: "ft\() = Def a" by (simp add: fsingleton_def2) lemma slen_fsingleton[simp]: "#() = 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 = \ ==> last s = undefined" +lemma last_infinite[simp]:"#s = \ \ 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 \ k \ enat n = #s \ 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:"\s \ UU; enat (Suc n) = #s\ \ (stream_take n\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)$( ooo s) = ooo stream_take n$s" +lemma fstreams_take_Suc[simp]: "stream_take (Suc n)\( ooo s) = ooo stream_take n\s" by (simp add: fsingleton_def2) -lemma fstreams_not_empty[simp]: " ooo s ~= <>" +lemma fstreams_not_empty[simp]: " ooo s \ <>" by (simp add: fsingleton_def2) -lemma fstreams_not_empty2[simp]: "s ooo ~= <>" +lemma fstreams_not_empty2[simp]: "s ooo \ <>" by (case_tac "s=UU", auto) -lemma fstreams_exhaust: "x = UU | (EX a s. x = ooo s)" +lemma fstreams_exhaust: "x = UU \ (\a s. x = 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 = ooo y ==> P |] ==> P" +lemma fstreams_cases: "\x = UU \ P; \a y. x = ooo y \ P\ \ P" by (insert fstreams_exhaust [of x], auto) -lemma fstreams_exhaust_eq: "(x ~= UU) = (? a y. x = ooo y)" +lemma fstreams_exhaust_eq: "x \ UU \ (\a y. x = 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: "( ooo s = ooo t) = (a=b & s=t)" +lemma fstreams_inject: " ooo s = ooo t \ a = b \ s = t" by (simp add: fsingleton_def2) -lemma fstreams_prefix: " ooo s << t ==> EX tt. t = ooo tt & s << tt" +lemma fstreams_prefix: " ooo s << t \ \tt. t = ooo tt \ s << tt" apply (simp add: fsingleton_def2) apply (insert stream_prefix [of "Def a" s t], auto) done -lemma fstreams_prefix': "x << ooo z = (x = <> | (EX y. x = ooo y & y << z))" +lemma fstreams_prefix': "x << ooo z \ x = <> \ (\y. x = ooo y \ 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$( ooo s) = Def a" +lemma ft_fstreams[simp]: "ft\( ooo s) = Def a" by (simp add: fsingleton_def2) -lemma rt_fstreams[simp]: "rt$( ooo s) = s" +lemma rt_fstreams[simp]: "rt\( ooo s) = s" by (simp add: fsingleton_def2) -lemma ft_eq[simp]: "(ft$s = Def a) = (EX t. s = ooo t)" +lemma ft_eq[simp]: "ft\s = Def a \ (\t. s = ooo t)" apply (cases s, auto) apply (auto simp add: fsingleton_def2) done -lemma surjective_fstreams: "( ooo y = x) = (ft$x = Def d & rt$x = y)" +lemma surjective_fstreams: " ooo y = x \ (ft\x = Def d \ rt\x = y)" by auto -lemma fstreams_mono: " ooo b << ooo c ==> b << c" +lemma fstreams_mono: " ooo b << ooo c \ b << c" by (simp add: fsingleton_def2) -lemma fsmap_UU[simp]: "fsmap f$UU = UU" +lemma fsmap_UU[simp]: "fsmap f\UU = UU" by (simp add: fsmap_def) -lemma fsmap_fsingleton_sconc: "fsmap f$( ooo xs) = <(f x)> ooo (fsmap f$xs)" +lemma fsmap_fsingleton_sconc: "fsmap f\( ooo xs) = <(f x)> ooo (fsmap f\xs)" by (simp add: fsmap_def fsingleton_def2 flift2_def) -lemma fsmap_fsingleton[simp]: "fsmap f$() = <(f x)>" +lemma fsmap_fsingleton[simp]: "fsmap f\() = <(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" + "\s x y. stream_take n\(s::'a fstream) << x \ x << y \ y << s \ x \ y \ stream_take (Suc n)\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) = ooo s |] ==> EX j t. Y j = ooo t" +lemma fstreams_lub_lemma1: "\chain Y; (LUB i. Y i) = ooo s\ \ \j t. Y j = 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) = ooo s |] - ==> (EX j t. Y j = ooo t) & (EX X. chain X & (ALL i. EX j. ooo X i << Y j) & (LUB i. X i) = s)" + "\chain Y; (LUB i. Y i) = ooo s\ + \ (\j t. Y j = ooo t) \ (\X. chain X \ (\i. \j. ooo X i << Y j) \ (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="\n. stream_take n\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" + "\chain Y; (LUB i. Y i) = ((a::'a::flat), b); a \ UU; b \ UU\ + \ \j c d. Y j = (c, d) \ c \ UU \ d \ UU" apply (frule lub_prod, clarsimp) apply (clarsimp simp add: lub_eq_bottom_iff [where Y="\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, ooo ms); (a::'a::flat) ~= UU |] ==> EX j t. Y j = (a, ooo t)" + "\chain Y; (LUB i. Y i) = (a, ooo ms); (a::'a::flat) \ UU\ \ \j t. Y j = (a, 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, ooo ms); (a::'a::flat) ~= UU |] - ==> (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) = ms)" + "\chain Y; (LUB i. Y i) = (a, ooo ms); (a::'a::flat) \ UU\ + \ (\j t. Y j = (a, ooo t)) \ (\X. chain X \ (\i. \j. (a, ooo X i) << Y j) \ (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="\n. stream_take n\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 \ 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) \ fst (Y ja) \ snd (Y j) \ 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" + "\monofun (f::'a::cpo \ 'b::cpo); (\Y. chain Y \ f (lub(range Y)) << (LUB i. f (Y i)))\ \ cont f" apply (erule contI2) apply simp done diff -r 6c2c16fef8f1 -r b0d31c7def86 src/HOL/HOLCF/IMP/HoareEx.thy --- 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. \ -type_synonym assn = "state => bool" +type_synonym assn = "state \ bool" definition - hoare_valid :: "[assn, com, assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) where - "|= {P} c {Q} = (\s t. P s \ D c $(Discr s) = Def t --> Q t)" + hoare_valid :: "[assn, com, assn] \ bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) where + "|= {P} c {Q} = (\s t. P s \ D c\(Discr s) = Def t \ Q t)" lemma WHILE_rule_sound: - "|= {A} c {A} ==> |= {A} WHILE b DO c {\s. A s \ \ bval b s}" + "|= {A} c {A} \ |= {A} WHILE b DO c {\s. A s \ \ bval b s}" apply (unfold hoare_valid_def) apply (simp (no_asm)) apply (rule fix_ind) diff -r 6c2c16fef8f1 -r b0d31c7def86 src/HOL/HOLCF/IOA/Abstraction.thy --- 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 \ 's2) \ ('a, 's1) execution \ ('a, 's2) execution" - where "cex_abs f ex = (f (fst ex), Map (\(a, t). (a, f t)) $ (snd ex))" + where "cex_abs f ex = (f (fst ex), Map (\(a, t). (a, f t)) \ (snd ex))" text \equals cex_abs on Sequences -- after ex2seq application\ definition cex_absSeq :: "('s1 \ 's2) \ ('a option, 's1) transition Seq \ ('a option, 's2)transition Seq" - where "cex_absSeq f = (\s. Map (\(s, a, t). (f s, a, f t)) $ s)" + where "cex_absSeq f = (\s. Map (\(s, a, t). (f s, a, f t)) \ s)" definition is_abstraction :: "('s1 \ 's2) \ ('a, 's1) ioa \ ('a, 's2) ioa \ bool" where "is_abstraction f C A \ @@ -161,7 +161,7 @@ that is to special Map Lemma. \ lemma traces_coincide_abs: - "ext C = ext A \ mk_trace C $ xs = mk_trace A $ (snd (cex_abs f (s, xs)))" + "ext C = ext A \ mk_trace C \ xs = mk_trace A \ (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))\s1" in exI) apply (simp add: Map2Finite MapConc) done @@ -345,7 +345,7 @@ subsubsection \Next\ -lemma TL_ex2seq_UU: "TL $ (ex2seq (cex_abs h ex)) = UU \ TL $ (ex2seq ex) = UU" +lemma TL_ex2seq_UU: "TL \ (ex2seq (cex_abs h ex)) = UU \ TL \ (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 \ TL $ (ex2seq ex) = nil" +lemma TL_ex2seq_nil: "TL \ (ex2seq (cex_abs h ex)) = nil \ TL \ (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 \ s) = TL \ (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 \ UU \ snd ex \ nil \ \ex'. TL$(ex2seq ex) = ex2seq ex'" +lemma TLex2seq: "snd ex \ UU \ snd ex \ nil \ \ex'. TL\(ex2seq ex) = ex2seq ex'" apply (pair ex) apply (Seq_case_simp x2) apply (pair a) apply auto done -lemma ex2seqnilTL: "TL $ (ex2seq ex) \ nil \ snd ex \ nil \ snd ex \ UU" +lemma ex2seqnilTL: "TL \ (ex2seq ex) \ nil \ snd ex \ nil \ snd ex \ UU" apply (pair ex) apply (Seq_case_simp x2) apply (pair a) diff -r 6c2c16fef8f1 -r b0d31c7def86 src/HOL/HOLCF/IOA/CompoExecs.thy --- 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 (\x. (fst x, fst (snd x)))" definition ProjA :: "('a, 's \ 't) execution \ ('a, 's) execution" - where "ProjA ex = (fst (fst ex), ProjA2 $ (snd ex))" + where "ProjA ex = (fst (fst ex), ProjA2 \ (snd ex))" definition ProjB2 :: "('a, 's \ 't) pairs \ ('a, 't) pairs" where "ProjB2 = Map (\x. (fst x, snd (snd x)))" definition ProjB :: "('a, 's \ 't) execution \ ('a, 't) execution" - where "ProjB ex = (snd (fst ex), ProjB2 $ (snd ex))" + where "ProjB ex = (snd (fst ex), ProjB2 \ (snd ex))" definition Filter_ex2 :: "'a signature \ ('a, 's) pairs \ ('a, 's) pairs" where "Filter_ex2 sig = Filter (\x. fst x \ actions sig)" definition Filter_ex :: "'a signature \ ('a, 's) execution \ ('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 \ (snd ex))" definition stutter2 :: "'a signature \ ('a, 's) pairs \ ('s \ tr)" where "stutter2 sig = - (fix $ + (fix \ (LAM h ex. (\s. case ex of @@ -37,10 +37,10 @@ (flift1 (\p. (If Def (fst p \ actions sig) then Def (s = snd p) else TT) - andalso (h$xs) (snd p)) $ x))))" + andalso (h\xs) (snd p)) \ x))))" definition stutter :: "'a signature \ ('a, 's) execution \ bool" - where "stutter sig ex \ (stutter2 sig $ (snd ex)) (fst ex) \ FF" + where "stutter sig ex \ (stutter2 sig \ (snd ex)) (fst ex) \ FF" definition par_execs :: "('a, 's) execution_module \ ('a, 't) execution_module \ ('a, 's \ 't) execution_module" @@ -64,41 +64,41 @@ subsection \\ProjA2\\ -lemma ProjA2_UU: "ProjA2 $ UU = UU" +lemma ProjA2_UU: "ProjA2 \ UU = UU" by (simp add: ProjA2_def) -lemma ProjA2_nil: "ProjA2 $ nil = nil" +lemma ProjA2_nil: "ProjA2 \ nil = nil" by (simp add: ProjA2_def) -lemma ProjA2_cons: "ProjA2 $ ((a, t) \ xs) = (a, fst t) \ ProjA2 $ xs" +lemma ProjA2_cons: "ProjA2 \ ((a, t) \ xs) = (a, fst t) \ ProjA2 \ xs" by (simp add: ProjA2_def) subsection \\ProjB2\\ -lemma ProjB2_UU: "ProjB2 $ UU = UU" +lemma ProjB2_UU: "ProjB2 \ UU = UU" by (simp add: ProjB2_def) -lemma ProjB2_nil: "ProjB2 $ nil = nil" +lemma ProjB2_nil: "ProjB2 \ nil = nil" by (simp add: ProjB2_def) -lemma ProjB2_cons: "ProjB2 $ ((a, t) \ xs) = (a, snd t) \ ProjB2 $ xs" +lemma ProjB2_cons: "ProjB2 \ ((a, t) \ xs) = (a, snd t) \ ProjB2 \ xs" by (simp add: ProjB2_def) subsection \\Filter_ex2\\ -lemma Filter_ex2_UU: "Filter_ex2 sig $ UU = UU" +lemma Filter_ex2_UU: "Filter_ex2 sig \ UU = UU" by (simp add: Filter_ex2_def) -lemma Filter_ex2_nil: "Filter_ex2 sig $ nil = nil" +lemma Filter_ex2_nil: "Filter_ex2 sig \ nil = nil" by (simp add: Filter_ex2_def) lemma Filter_ex2_cons: - "Filter_ex2 sig $ (at \ xs) = + "Filter_ex2 sig \ (at \ xs) = (if fst at \ actions sig - then at \ (Filter_ex2 sig $ xs) - else Filter_ex2 sig $ xs)" + then at \ (Filter_ex2 sig \ xs) + else Filter_ex2 sig \ xs)" by (simp add: Filter_ex2_def) @@ -114,7 +114,7 @@ (flift1 (\p. (If Def (fst p \ actions sig) then Def (s= snd p) else TT) - andalso (stutter2 sig$xs) (snd p)) $ x)))" + andalso (stutter2 sig\xs) (snd p)) \ 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 \ UU) s = UU" apply (subst stutter2_unfold) apply simp done -lemma stutter2_nil: "(stutter2 sig $ nil) s = TT" +lemma stutter2_nil: "(stutter2 sig \ nil) s = TT" apply (subst stutter2_unfold) apply simp done lemma stutter2_cons: - "(stutter2 sig $ (at \ xs)) s = + "(stutter2 sig \ (at \ xs)) s = ((if fst at \ actions sig then Def (s = snd at) else TT) - andalso (stutter2 sig $ xs) (snd at))" + andalso (stutter2 sig \ 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: \ \\is_ex_fr\ propagates from \A \ B\ to projections \A\ and \B\\ "\s. is_exec_frag (A \ B) (s, xs) \ - is_exec_frag A (fst s, Filter_ex2 (asig_of A) $ (ProjA2 $ xs)) \ - is_exec_frag B (snd s, Filter_ex2 (asig_of B) $ (ProjB2 $ xs))" + is_exec_frag A (fst s, Filter_ex2 (asig_of A) \ (ProjA2 \ xs)) \ + is_exec_frag B (snd s, Filter_ex2 (asig_of B) \ (ProjB2 \ xs))" apply (pair_induct xs simp: is_exec_frag_def) text \main case\ apply (auto simp add: trans_of_defs2) @@ -182,8 +182,8 @@ lemma lemma_1_1b: \ \\is_ex_fr (A \ B)\ implies stuttering on projections\ "\s. is_exec_frag (A \ B) (s, xs) \ - stutter (asig_of A) (fst s, ProjA2 $ xs) \ - stutter (asig_of B) (snd s, ProjB2 $ xs)" + stutter (asig_of A) (fst s, ProjA2 \ xs) \ + stutter (asig_of B) (snd s, ProjB2 \ xs)" apply (pair_induct xs simp: stutter_def is_exec_frag_def) text \main case\ apply (auto simp add: trans_of_defs2) @@ -201,10 +201,10 @@ lemma lemma_1_2: \ \\ex A\, \exB\, stuttering and forall \a \ A \ B\ implies \ex (A \ B)\\ "\s. - is_exec_frag A (fst s, Filter_ex2 (asig_of A) $ (ProjA2 $ xs)) \ - is_exec_frag B (snd s, Filter_ex2 (asig_of B) $ (ProjB2 $ xs)) \ - stutter (asig_of A) (fst s, ProjA2 $ xs) \ - stutter (asig_of B) (snd s, ProjB2 $ xs) \ + is_exec_frag A (fst s, Filter_ex2 (asig_of A) \ (ProjA2 \ xs)) \ + is_exec_frag B (snd s, Filter_ex2 (asig_of B) \ (ProjB2 \ xs)) \ + stutter (asig_of A) (fst s, ProjA2 \ xs) \ + stutter (asig_of B) (snd s, ProjB2 \ xs) \ Forall (\x. fst x \ act (A \ B)) xs \ is_exec_frag (A \ B) (s, xs)" apply (pair_induct xs simp: Forall_def sforall_def is_exec_frag_def stutter_def) diff -r 6c2c16fef8f1 -r b0d31c7def86 src/HOL/HOLCF/IOA/CompoScheds.thy --- 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 \ ('a, 't) ioa \ 'a Seq \ ('a, 's) pairs \ ('a, 't) pairs \ ('s \ 't \ ('a, 's \ 't) pairs)" where "mkex2 A B = - (fix $ + (fix \ (LAM h sch exA exB. (\s t. case sch of @@ -22,29 +22,29 @@ | Def y \ (if y \ act A then (if y \ act B then - (case HD $ exA of + (case HD \ exA of UU \ UU | Def a \ - (case HD $ exB of + (case HD \ exB of UU \ UU | Def b \ (y, (snd a, snd b)) \ - (h $ xs $ (TL $ exA) $ (TL $ exB)) (snd a) (snd b))) + (h \ xs \ (TL \ exA) \ (TL \ exB)) (snd a) (snd b))) else - (case HD $ exA of + (case HD \ exA of UU \ UU - | Def a \ (y, (snd a, t)) \ (h $ xs $ (TL $ exA) $ exB) (snd a) t)) + | Def a \ (y, (snd a, t)) \ (h \ xs \ (TL \ exA) \ exB) (snd a) t)) else (if y \ act B then - (case HD $ exB of + (case HD \ exB of UU \ UU - | Def b \ (y, (s, snd b)) \ (h $ xs $ exA $ (TL $ exB)) s (snd b)) + | Def b \ (y, (s, snd b)) \ (h \ xs \ exA \ (TL \ exB)) s (snd b)) else UU))))))" definition mkex :: "('a, 's) ioa \ ('a, 't) ioa \ 'a Seq \ ('a, 's) execution \ ('a, 't) execution \ ('a, 's \ '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 \ sch \ (snd exA) \ (snd exB)) (fst exA) (fst exB))" definition par_scheds :: "'a schedule_module \ 'a schedule_module \ '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} \ - {sch. Filter (%a. a:actions sigB)$sch : schB} \ + ({sch. Filter (%a. a:actions sigA)\sch : schA} \ + {sch. Filter (%a. a:actions sigB)\sch : schB} \ {sch. Forall (%x. x:(actions sigA Un actions sigB)) sch}, asig_comp sigA sigB))" @@ -72,23 +72,23 @@ | Def y \ (if y \ act A then (if y \ act B then - (case HD $ exA of + (case HD \ exA of UU \ UU | Def a \ - (case HD $ exB of + (case HD \ exB of UU \ UU | Def b \ (y, (snd a, snd b)) \ - (mkex2 A B $ xs $ (TL $ exA) $ (TL $ exB)) (snd a) (snd b))) + (mkex2 A B \ xs \ (TL \ exA) \ (TL \ exB)) (snd a) (snd b))) else - (case HD $ exA of + (case HD \ exA of UU \ UU - | Def a \ (y, (snd a, t)) \ (mkex2 A B $ xs $ (TL $ exA) $ exB) (snd a) t)) + | Def a \ (y, (snd a, t)) \ (mkex2 A B \ xs \ (TL \ exA) \ exB) (snd a) t)) else (if y \ act B then - (case HD $ exB of + (case HD \ exB of UU \ UU - | Def b \ (y, (s, snd b)) \ (mkex2 A B $ xs $ exA $ (TL $ exB)) s (snd b)) + | Def b \ (y, (s, snd b)) \ (mkex2 A B \ xs \ exA \ (TL \ 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 \ UU \ exA \ 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 \ nil \ exA \ exB) s t = nil" apply (subst mkex2_unfold) apply simp done lemma mkex2_cons_1: - "x \ act A \ x \ act B \ HD $ exA = Def a \ - (mkex2 A B $ (x \ sch) $ exA $ exB) s t = - (x, snd a,t) \ (mkex2 A B $ sch $ (TL $ exA) $ exB) (snd a) t" + "x \ act A \ x \ act B \ HD \ exA = Def a \ + (mkex2 A B \ (x \ sch) \ exA \ exB) s t = + (x, snd a,t) \ (mkex2 A B \ sch \ (TL \ exA) \ 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 \ act A \ x \ act B \ HD $ exB = Def b \ - (mkex2 A B $ (x \ sch) $ exA $ exB) s t = - (x, s, snd b) \ (mkex2 A B $ sch $ exA $ (TL $ exB)) s (snd b)" + "x \ act A \ x \ act B \ HD \ exB = Def b \ + (mkex2 A B \ (x \ sch) \ exA \ exB) s t = + (x, s, snd b) \ (mkex2 A B \ sch \ exA \ (TL \ 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 \ act A \ x \ act B \ HD $ exA = Def a \ HD $ exB = Def b \ - (mkex2 A B $ (x \ sch) $ exA $ exB) s t = - (x, snd a,snd b) \ (mkex2 A B $ sch $ (TL $ exA) $ (TL $ exB)) (snd a) (snd b)" + "x \ act A \ x \ act B \ HD \ exA = Def a \ HD \ exB = Def b \ + (mkex2 A B \ (x \ sch) \ exA \ exB) s t = + (x, snd a,snd b) \ (mkex2 A B \ sch \ (TL \ exA) \ (TL \ 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: \ \\tfilter ex\ and \filter_act\ are commutative\ - "filter_act $ (Filter_ex2 (asig_of A) $ xs) = - Filter (\a. a \ act A) $ (filter_act $ xs)" + "filter_act \ (Filter_ex2 (asig_of A) \ xs) = + Filter (\a. a \ act A) \ (filter_act \ xs)" apply (unfold filter_act_def Filter_ex2_def) apply (simp add: MapFilter o_def) done lemma lemma_2_1b: \ \State-projections do not affect \filter_act\\ - "filter_act $ (ProjA2 $ xs) = filter_act $ xs \ - filter_act $ (ProjB2 $ xs) = filter_act $ xs" + "filter_act \ (ProjA2 \ xs) = filter_act \ xs \ + filter_act \ (ProjB2 \ xs) = filter_act \ xs" by (pair_induct xs) @@ -213,7 +213,7 @@ \ lemma sch_actions_in_AorB: - "\s. is_exec_frag (A \ B) (s, xs) \ Forall (\x. x \ act (A \ B)) (filter_act $ xs)" + "\s. is_exec_frag (A \ B) (s, xs) \ Forall (\x. x \ act (A \ B)) (filter_act \ xs)" apply (pair_induct xs simp: is_exec_frag_def Forall_def sforall_def) text \main case\ apply auto @@ -231,9 +231,9 @@ lemma Mapfst_mkex_is_sch: "\exA exB s t. Forall (\x. x \ act (A \ B)) sch \ - Filter (\a. a \ act A) $ sch \ filter_act $ exA \ - Filter (\a. a \ act B) $ sch \ filter_act $ exB \ - filter_act $ (snd (mkex A B sch (s, exA) (t, exB))) = sch" + Filter (\a. a \ act A) \ sch \ filter_act \ exA \ + Filter (\a. a \ act B) \ sch \ filter_act \ exB \ + filter_act \ (snd (mkex A B sch (s, exA) (t, exB))) = sch" apply (Seq_induct sch simp: Filter_def Forall_def sforall_def mkex_def) text \main case: splitting into 4 cases according to \a \ A\, \a \ B\\ @@ -303,15 +303,15 @@ lemma stutterA_mkex: "\exA exB s t. Forall (\x. x \ act (A \ B)) sch \ - Filter (\a. a \ act A) $ sch \ filter_act $ exA \ - Filter (\a. a \ act B) $ sch \ filter_act $ exB \ - stutter (asig_of A) (s, ProjA2 $ (snd (mkex A B sch (s, exA) (t, exB))))" + Filter (\a. a \ act A) \ sch \ filter_act \ exA \ + Filter (\a. a \ act B) \ sch \ filter_act \ exB \ + stutter (asig_of A) (s, ProjA2 \ (snd (mkex A B sch (s, exA) (t, exB))))" by (mkex_induct sch exA exB) lemma stutter_mkex_on_A: "Forall (\x. x \ act (A \ B)) sch \ - Filter (\a. a \ act A) $ sch \ filter_act $ (snd exA) \ - Filter (\a. a \ act B) $ sch \ filter_act $ (snd exB) \ + Filter (\a. a \ act A) \ sch \ filter_act \ (snd exA) \ + Filter (\a. a \ act B) \ sch \ filter_act \ (snd exB) \ stutter (asig_of A) (ProjA (mkex A B sch exA exB))" apply (cut_tac stutterA_mkex) apply (simp add: stutter_def ProjA_def mkex_def) @@ -330,16 +330,16 @@ lemma stutterB_mkex: "\exA exB s t. Forall (\x. x \ act (A \ B)) sch \ - Filter (\a. a \ act A) $ sch \ filter_act $ exA \ - Filter (\a. a \ act B) $ sch \ filter_act $ exB \ - stutter (asig_of B) (t, ProjB2 $ (snd (mkex A B sch (s, exA) (t, exB))))" + Filter (\a. a \ act A) \ sch \ filter_act \ exA \ + Filter (\a. a \ act B) \ sch \ filter_act \ exB \ + stutter (asig_of B) (t, ProjB2 \ (snd (mkex A B sch (s, exA) (t, exB))))" by (mkex_induct sch exA exB) lemma stutter_mkex_on_B: "Forall (\x. x \ act (A \ B)) sch \ - Filter (\a. a \ act A) $ sch \ filter_act $ (snd exA) \ - Filter (\a. a \ act B) $ sch \ filter_act $ (snd exB) \ + Filter (\a. a \ act A) \ sch \ filter_act \ (snd exA) \ + Filter (\a. a \ act B) \ sch \ filter_act \ (snd exB) \ stutter (asig_of B) (ProjB (mkex A B sch exA exB))" apply (cut_tac stutterB_mkex) apply (simp add: stutter_def ProjB_def mkex_def) @@ -352,36 +352,36 @@ text \ Filter of \mkex (sch, exA, exB)\ to \A\ after projection onto \A\ is \exA\, - using \zip $ (proj1 $ exA) $ (proj2 $ exA)\ instead of \exA\, + using \zip \ (proj1 \ exA) \ (proj2 \ exA)\ instead of \exA\, because of admissibility problems structural induction. \ lemma filter_mkex_is_exA_tmp: "\exA exB s t. Forall (\x. x \ act (A \ B)) sch \ - Filter (\a. a \ act A) $ sch \ filter_act $ exA \ - Filter (\a. a \ act B) $ sch \ filter_act $ exB \ - Filter_ex2 (asig_of A) $ (ProjA2 $ (snd (mkex A B sch (s, exA) (t, exB)))) = - Zip $ (Filter (\a. a \ act A) $ sch) $ (Map snd $ exA)" + Filter (\a. a \ act A) \ sch \ filter_act \ exA \ + Filter (\a. a \ act B) \ sch \ filter_act \ exB \ + Filter_ex2 (asig_of A) \ (ProjA2 \ (snd (mkex A B sch (s, exA) (t, exB)))) = + Zip \ (Filter (\a. a \ act A) \ sch) \ (Map snd \ exA)" by (mkex_induct sch exB exA) text \ - \zip $ (proj1 $ y) $ (proj2 $ y) = y\ (using the lift operations) + \zip \ (proj1 \ y) \ (proj2 \ y) = y\ (using the lift operations) lemma for admissibility problems \ -lemma Zip_Map_fst_snd: "Zip $ (Map fst $ y) $ (Map snd $ y) = y" +lemma Zip_Map_fst_snd: "Zip \ (Map fst \ y) \ (Map snd \ y) = y" by (Seq_induct y) text \ - \filter A $ sch = proj1 $ ex \ zip $ (filter A $ sch) $ (proj2 $ ex) = ex\ + \filter A \ sch = proj1 \ ex \ zip \ (filter A \ sch) \ (proj2 \ ex) = ex\ lemma for eliminating non admissible equations in assumptions \ lemma trick_against_eq_in_ass: - "Filter (\a. a \ act AB) $ sch = filter_act $ ex \ - ex = Zip $ (Filter (\a. a \ act AB) $ sch) $ (Map snd $ ex)" + "Filter (\a. a \ act AB) \ sch = filter_act \ ex \ + ex = Zip \ (Filter (\a. a \ act AB) \ sch) \ (Map snd \ 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 (\a. a \ act (A \ B)) sch \ - Filter (\a. a \ act A) $ sch = filter_act $ (snd exA) \ - Filter (\a. a \ act B) $ sch = filter_act $ (snd exB) \ + Filter (\a. a \ act A) \ sch = filter_act \ (snd exA) \ + Filter (\a. a \ act B) \ sch = filter_act \ (snd exB) \ Filter_ex (asig_of A) (ProjA (mkex A B sch exA exB)) = exA" apply (simp add: ProjA_def Filter_ex_def) apply (pair exA) @@ -409,17 +409,17 @@ text \ Filter of \mkex (sch, exA, exB)\ to \B\ after projection onto \B\ is \exB\ - using \zip $ (proj1 $ exB) $ (proj2 $ exB)\ instead of \exB\ + using \zip \ (proj1 \ exB) \ (proj2 \ exB)\ instead of \exB\ because of admissibility problems structural induction. \ lemma filter_mkex_is_exB_tmp: "\exA exB s t. Forall (\x. x \ act (A \ B)) sch \ - Filter (\a. a \ act A) $ sch \ filter_act $ exA \ - Filter (\a. a \ act B) $ sch \ filter_act $ exB \ - Filter_ex2 (asig_of B) $ (ProjB2 $ (snd (mkex A B sch (s, exA) (t, exB)))) = - Zip $ (Filter (\a. a \ act B) $ sch) $ (Map snd $ exB)" + Filter (\a. a \ act A) \ sch \ filter_act \ exA \ + Filter (\a. a \ act B) \ sch \ filter_act \ exB \ + Filter_ex2 (asig_of B) \ (ProjB2 \ (snd (mkex A B sch (s, exA) (t, exB)))) = + Zip \ (Filter (\a. a \ act B) \ sch) \ (Map snd \ 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 (\a. a \ act (A \ B)) sch \ - Filter (\a. a \ act A) $ sch = filter_act $ (snd exA) \ - Filter (\a. a \ act B) $ sch = filter_act $ (snd exB) \ + Filter (\a. a \ act A) \ sch = filter_act \ (snd exA) \ + Filter (\a. a \ act B) \ sch = filter_act \ (snd exB) \ Filter_ex (asig_of B) (ProjB (mkex A B sch exA exB)) = exB" apply (simp add: ProjB_def Filter_ex_def) apply (pair exA) @@ -448,16 +448,16 @@ \ \\mkex\ has only \A\- or \B\-actions\ "\s t exA exB. Forall (\x. x \ act (A \ B)) sch & - Filter (\a. a \ act A) $ sch \ filter_act $ exA \ - Filter (\a. a \ act B) $ sch \ filter_act $ exB \ + Filter (\a. a \ act A) \ sch \ filter_act \ exA \ + Filter (\a. a \ act B) \ sch \ filter_act \ exB \ Forall (\x. fst x \ act (A \ B)) (snd (mkex A B sch (s, exA) (t, exB)))" by (mkex_induct sch exA exB) theorem compositionality_sch: "sch \ schedules (A \ B) \ - Filter (\a. a \ act A) $ sch \ schedules A \ - Filter (\a. a \ act B) $ sch \ schedules B \ + Filter (\a. a \ act A) \ sch \ schedules A \ + Filter (\a. a \ act B) \ sch \ schedules B \ Forall (\x. x \ act (A \ B)) sch" apply (simp add: schedules_def has_schedule_def) apply auto diff -r 6c2c16fef8f1 -r b0d31c7def86 src/HOL/HOLCF/IOA/CompoTraces.thy --- 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 \ ('a, 't) ioa \ 'a Seq \ 'a Seq \ 'a Seq \ 'a Seq" where "mksch A B = - (fix $ + (fix \ (LAM h tr schA schB. case tr of nil \ nil @@ -21,17 +21,17 @@ | Def y \ (if y \ act A then (if y \ act B then - ((Takewhile (\a. a \ int A) $ schA) @@ - (Takewhile (\a. a \ int B) $ schB) @@ - (y \ (h $ xs $ (TL $ (Dropwhile (\a. a \ int A) $ schA)) - $ (TL $ (Dropwhile (\a. a \ int B) $ schB))))) + ((Takewhile (\a. a \ int A) \ schA) @@ + (Takewhile (\a. a \ int B) \ schB) @@ + (y \ (h \ xs \ (TL \ (Dropwhile (\a. a \ int A) \ schA)) + \ (TL \ (Dropwhile (\a. a \ int B) \ schB))))) else - ((Takewhile (\a. a \ int A) $ schA) @@ - (y \ (h $ xs $ (TL $ (Dropwhile (\a. a \ int A) $ schA)) $ schB)))) + ((Takewhile (\a. a \ int A) \ schA) @@ + (y \ (h \ xs \ (TL \ (Dropwhile (\a. a \ int A) \ schA)) \ schB)))) else (if y \ act B then - ((Takewhile (\a. a \ int B) $ schB) @@ - (y \ (h $ xs $ schA $ (TL $ (Dropwhile (\a. a \ int B) $ schB))))) + ((Takewhile (\a. a \ int B) \ schB) @@ + (y \ (h \ xs \ schA \ (TL \ (Dropwhile (\a. a \ int B) \ schB))))) else UU)))))" definition par_traces :: "'a trace_module \ 'a trace_module \ 'a trace_module" @@ -40,15 +40,15 @@ trA = fst TracesA; sigA = snd TracesA; trB = fst TracesB; sigB = snd TracesB in - ({tr. Filter (\a. a \ actions sigA) $ tr \ trA} \ - {tr. Filter (\a. a \ actions sigB) $ tr \ trB} \ + ({tr. Filter (\a. a \ actions sigA) \ tr \ trA} \ + {tr. Filter (\a. a \ actions sigB) \ tr \ trB} \ {tr. Forall (\x. x \ externals sigA \ externals sigB) tr}, asig_comp sigA sigB))" axiomatization where - finiteR_mksch: "Finite (mksch A B $ tr $ x $ y) \ Finite tr" + finiteR_mksch: "Finite (mksch A B \ tr \ x \ y) \ Finite tr" -lemma finiteR_mksch': "\ Finite tr \ \ Finite (mksch A B $ tr $ x $ y)" +lemma finiteR_mksch': "\ Finite tr \ \ Finite (mksch A B \ tr \ x \ y)" by (blast intro: finiteR_mksch) @@ -68,17 +68,17 @@ | Def y \ (if y \ act A then (if y \ act B then - ((Takewhile (\a. a \ int A) $ schA) @@ - (Takewhile (\a. a \ int B) $ schB) @@ - (y \ (mksch A B $ xs $(TL $ (Dropwhile (\a. a \ int A) $ schA)) - $(TL $ (Dropwhile (\a. a \ int B) $ schB))))) + ((Takewhile (\a. a \ int A) \ schA) @@ + (Takewhile (\a. a \ int B) \ schB) @@ + (y \ (mksch A B \ xs \(TL \ (Dropwhile (\a. a \ int A) \ schA)) + \(TL \ (Dropwhile (\a. a \ int B) \ schB))))) else - ((Takewhile (\a. a \ int A) $ schA) @@ - (y \ (mksch A B $ xs $ (TL $ (Dropwhile (\a. a \ int A) $ schA)) $ schB)))) + ((Takewhile (\a. a \ int A) \ schA) @@ + (y \ (mksch A B \ xs \ (TL \ (Dropwhile (\a. a \ int A) \ schA)) \ schB)))) else (if y \ act B then - ((Takewhile (\a. a \ int B) $ schB) @@ - (y \ (mksch A B $ xs $ schA $ (TL $ (Dropwhile (\a. a \ int B) $ schB))))) + ((Takewhile (\a. a \ int B) \ schB) @@ + (y \ (mksch A B \ xs \ schA \ (TL \ (Dropwhile (\a. a \ int B) \ 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 \ UU \ schA \ 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 \ nil \ schA \ schB = nil" apply (subst mksch_unfold) apply simp done lemma mksch_cons1: "x \ act A \ x \ act B \ - mksch A B $ (x \ tr) $ schA $ schB = - (Takewhile (\a. a \ int A) $ schA) @@ - (x \ (mksch A B $ tr $ (TL $ (Dropwhile (\a. a \ int A) $ schA)) $ schB))" + mksch A B \ (x \ tr) \ schA \ schB = + (Takewhile (\a. a \ int A) \ schA) @@ + (x \ (mksch A B \ tr \ (TL \ (Dropwhile (\a. a \ int A) \ schA)) \ schB))" apply (rule trans) apply (subst mksch_unfold) apply (simp add: Consq_def If_and_if) @@ -110,9 +110,9 @@ lemma mksch_cons2: "x \ act A \ x \ act B \ - mksch A B $ (x \ tr) $ schA $ schB = - (Takewhile (\a. a \ int B) $ schB) @@ - (x \ (mksch A B $ tr $ schA $ (TL $ (Dropwhile (\a. a \ int B) $ schB))))" + mksch A B \ (x \ tr) \ schA \ schB = + (Takewhile (\a. a \ int B) \ schB) @@ + (x \ (mksch A B \ tr \ schA \ (TL \ (Dropwhile (\a. a \ int B) \ schB))))" apply (rule trans) apply (subst mksch_unfold) apply (simp add: Consq_def If_and_if) @@ -121,11 +121,11 @@ lemma mksch_cons3: "x \ act A \ x \ act B \ - mksch A B $ (x \ tr) $ schA $ schB = - (Takewhile (\a. a \ int A) $ schA) @@ - ((Takewhile (\a. a \ int B) $ schB) @@ - (x \ (mksch A B $ tr $ (TL $ (Dropwhile (\a. a \ int A) $ schA)) - $ (TL $ (Dropwhile (\a. a \ int B) $ schB)))))" + mksch A B \ (x \ tr) \ schA \ schB = + (Takewhile (\a. a \ int A) \ schA) @@ + ((Takewhile (\a. a \ int B) \ schB) @@ + (x \ (mksch A B \ tr \ (TL \ (Dropwhile (\a. a \ int A) \ schA)) + \ (TL \ (Dropwhile (\a. a \ int B) \ 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 \ \schA schB. Forall (\x. x \ act (A \ B)) tr \ - Forall (\x. x \ act (A \ B)) (mksch A B $ tr $ schA $ schB)" + Forall (\x. x \ act (A \ B)) (mksch A B \ tr \ schA \ 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 \ \schA schB. Forall (\x. x \ act B \ x \ act A) tr \ - Forall (\x. x \ act B \ x \ act A) (mksch A B $ tr $ schA $ schB)" + Forall (\x. x \ act B \ x \ act A) (mksch A B \ tr \ schA \ 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 \ \schA schB. Forall (\x. x \ act A \ x \ act B) tr \ - Forall (\x. x \ act A \ x \ act B) (mksch A B $ tr $ schA $ schB)" + Forall (\x. x \ act A \ x \ act B) (mksch A B \ tr \ schA \ 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 \ is_asig (asig_of A) \ is_asig (asig_of B) \ \x y. Forall (\x. x \ act A) x \ Forall (\x. x \ act B) y \ - Filter (\a. a \ ext A) $ x = Filter (\a. a \ act A) $ tr \ - Filter (\a. a \ ext B) $ y = Filter (\a. a \ act B) $ tr \ - Forall (\x. x \ ext (A \ B)) tr \ Finite (mksch A B $ tr $ x $ y)" + Filter (\a. a \ ext A) \ x = Filter (\a. a \ act A) \ tr \ + Filter (\a. a \ ext B) \ y = Filter (\a. a \ act B) \ tr \ + Forall (\x. x \ ext (A \ B)) tr \ Finite (mksch A B \ tr \ x \ y)" apply (erule Seq_Finite_ind) apply simp text \main case\ @@ -238,9 +238,9 @@ text \\Finite (tw iA x)\ and \Finite (tw iB y)\\ apply (simp add: not_ext_is_int_or_not_act FiniteConc) text \now for conclusion IH applicable, but assumptions have to be transformed\ - apply (drule_tac x = "x" and g = "Filter (\a. a \ act A) $ s" in subst_lemma2) + apply (drule_tac x = "x" and g = "Filter (\a. a \ act A) \ s" in subst_lemma2) apply assumption - apply (drule_tac x = "y" and g = "Filter (\a. a \ act B) $ s" in subst_lemma2) + apply (drule_tac x = "y" and g = "Filter (\a. a \ act B) \ s" in subst_lemma2) apply assumption text \IH\ apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile) @@ -252,7 +252,7 @@ text \\Finite (tw iB y)\\ apply (simp add: not_ext_is_int_or_not_act FiniteConc) text \now for conclusion IH applicable, but assumptions have to be transformed\ - apply (drule_tac x = "y" and g = "Filter (\a. a \ act B) $ s" in subst_lemma2) + apply (drule_tac x = "y" and g = "Filter (\a. a \ act B) \ s" in subst_lemma2) apply assumption text \IH\ apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile) @@ -264,7 +264,7 @@ text \\Finite (tw iA x)\\ apply (simp add: not_ext_is_int_or_not_act FiniteConc) text \now for conclusion IH applicable, but assumptions have to be transformed\ - apply (drule_tac x = "x" and g = "Filter (\a. a \ act A) $ s" in subst_lemma2) + apply (drule_tac x = "x" and g = "Filter (\a. a \ act A) \ s" in subst_lemma2) apply assumption text \IH\ apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile) @@ -280,12 +280,12 @@ lemma reduceA_mksch1 [rule_format]: "Finite bs \ is_asig (asig_of A) \ is_asig (asig_of B) \ compatible A B \ \y. Forall (\x. x \ act B) y \ Forall (\x. x \ act B \ x \ act A) bs \ - Filter (\a. a \ ext B) $ y = Filter (\a. a \ act B) $ (bs @@ z) \ + Filter (\a. a \ ext B) \ y = Filter (\a. a \ act B) \ (bs @@ z) \ (\y1 y2. - (mksch A B $ (bs @@ z) $ x $ y) = (y1 @@ (mksch A B $ z $ x $ y2)) \ + (mksch A B \ (bs @@ z) \ x \ y) = (y1 @@ (mksch A B \ z \ x \ y2)) \ Forall (\x. x \ act B \ x \ act A) y1 \ Finite y1 \ y = (y1 @@ y2) \ - Filter (\a. a \ ext B) $ y1 = bs)" + Filter (\a. a \ ext B) \ 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 \transform assumption \f eB y = f B (s @ z)\\ - apply (drule_tac x = "y" and g = "Filter (\a. a \ act B) $ (s @@ z) " in subst_lemma2) + apply (drule_tac x = "y" and g = "Filter (\a. a \ act B) \ (s @@ z) " in subst_lemma2) apply assumption apply (simp add: not_ext_is_int_or_not_act FilterConc) text \apply IH\ - apply (erule_tac x = "TL $ (Dropwhile (\a. a \ int B) $ y)" in allE) + apply (erule_tac x = "TL \ (Dropwhile (\a. a \ int B) \ y)" in allE) apply (simp add: ForallTL ForallDropwhile FilterConc) apply (erule exE)+ apply (erule conjE)+ @@ -315,7 +315,7 @@ text \for replacing IH in conclusion\ apply (rotate_tac -2) text \instantiate \y1a\ and \y2a\\ - apply (rule_tac x = "Takewhile (\a. a \ int B) $ y @@ a \ y1" in exI) + apply (rule_tac x = "Takewhile (\a. a \ int B) \ y @@ a \ y1" in exI) apply (rule_tac x = "y2" in exI) text \elminate all obligations up to two depending on \Conc_assoc\\ 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 \ is_asig (asig_of A) \ is_asig (asig_of B) \ compatible A B \ \x. Forall (\x. x \ act A) x \ Forall (\x. x \ act A \ x \ act B) a_s \ - Filter (\a. a \ ext A) $ x = Filter (\a. a \ act A) $ (a_s @@ z) \ + Filter (\a. a \ ext A) \ x = Filter (\a. a \ act A) \ (a_s @@ z) \ (\x1 x2. - (mksch A B $ (a_s @@ z) $ x $ y) = (x1 @@ (mksch A B $ z $ x2 $ y)) \ + (mksch A B \ (a_s @@ z) \ x \ y) = (x1 @@ (mksch A B \ z \ x2 \ y)) \ Forall (\x. x \ act A \ x \ act B) x1 \ Finite x1 \ x = (x1 @@ x2) \ - Filter (\a. a \ ext A) $ x1 = a_s)" + Filter (\a. a \ ext A) \ 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 \transform assumption \f eA x = f A (s @ z)\\ - apply (drule_tac x = "x" and g = "Filter (\a. a \ act A) $ (s @@ z)" in subst_lemma2) + apply (drule_tac x = "x" and g = "Filter (\a. a \ act A) \ (s @@ z)" in subst_lemma2) apply assumption apply (simp add: not_ext_is_int_or_not_act FilterConc) text \apply IH\ - apply (erule_tac x = "TL $ (Dropwhile (\a. a \ int A) $ x)" in allE) + apply (erule_tac x = "TL \ (Dropwhile (\a. a \ int A) \ x)" in allE) apply (simp add: ForallTL ForallDropwhile FilterConc) apply (erule exE)+ apply (erule conjE)+ @@ -362,7 +362,7 @@ text \for replacing IH in conclusion\ apply (rotate_tac -2) text \instantiate \y1a\ and \y2a\\ - apply (rule_tac x = "Takewhile (\a. a \ int A) $ x @@ a \ x1" in exI) + apply (rule_tac x = "Takewhile (\a. a \ int A) \ x @@ a \ x1" in exI) apply (rule_tac x = "x2" in exI) text \eliminate all obligations up to two depending on \Conc_assoc\\ apply (simp add: intA_is_not_actB int_is_act int_is_not_ext FilterConc) @@ -382,9 +382,9 @@ Forall (\x. x \ act A) schA \ Forall (\x. x \ act B) schB \ Forall (\x. x \ ext (A \ B)) tr \ - Filter (\a. a \ act A) $ tr \ Filter (\a. a \ ext A) $ schA \ - Filter (\a. a \ act B) $ tr \ Filter (\a. a \ ext B) $ schB - \ Filter (\a. a \ ext (A \ B)) $ (mksch A B $ tr $ schA $ schB) = tr" + Filter (\a. a \ act A) \ tr \ Filter (\a. a \ ext A) \ schA \ + Filter (\a. a \ act B) \ tr \ Filter (\a. a \ ext B) \ schB + \ Filter (\a. a \ ext (A \ B)) \ (mksch A B \ tr \ schA \ schB) = tr" apply (Seq_induct tr simp: Forall_def sforall_def mksch_def) text \main case\ text \splitting into 4 cases according to \a \ A\, \a \ B\\ @@ -436,10 +436,10 @@ Forall (\x. x \ ext (A \ B)) tr \ Forall (\x. x \ act A) schA \ Forall (\x. x \ act B) schB \ - Filter (\a. a \ ext A) $ schA = Filter (\a. a \ act A) $ tr \ - Filter (\a. a \ ext B) $ schB = Filter (\a. a \ act B) $ tr \ + Filter (\a. a \ ext A) \ schA = Filter (\a. a \ act A) \ tr \ + Filter (\a. a \ ext B) \ schB = Filter (\a. a \ act B) \ tr \ LastActExtsch A schA \ LastActExtsch B schB - \ Filter (\a. a \ act A) $ (mksch A B $ tr $ schA $ schB) = schA" + \ Filter (\a. a \ act A) \ (mksch A B \ tr \ schA \ schB) = schA" apply (intro strip) apply (rule seq.take_lemma) apply (rule mp) @@ -509,7 +509,7 @@ text \eliminate the \B\-only prefix\ - apply (subgoal_tac "(Filter (\a. a \ act A) $ y1) = nil") + apply (subgoal_tac "(Filter (\a. a \ act A) \ 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 (\a. a \ act A \ a \ ext B) $ y1 = nil") + apply (subgoal_tac "Filter (\a. a \ act A \ a \ ext B) \ y1 = nil") apply (rotate_tac -1) apply simp text \eliminate introduced subgoal 2\ @@ -556,7 +556,7 @@ text \assumption \schB\\ apply (simp add: ext_and_act) text \assumption \schA\\ - 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) \ rs" in subst_lemma2) apply assumption apply (simp add: int_is_not_ext) text \assumptions concerning \LastActExtsch\, cannot be rewritten, as \LastActExtsmalli\ are looping\ @@ -574,7 +574,7 @@ apply (rotate_tac -2) apply simp - apply (subgoal_tac "Filter (\a. a \ act A \ a \ ext B) $ y1 = nil") + apply (subgoal_tac "Filter (\a. a \ act A \ a \ ext B) \ y1 = nil") apply (rotate_tac -1) apply simp text \eliminate introduced subgoal 2\ @@ -604,7 +604,7 @@ apply (frule_tac y = "y2" in sym [THEN eq_imp_below, THEN divide_Seq]) apply (erule conjE)+ text \assumption \schA\\ - 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) \rs" in subst_lemma2) apply assumption apply (simp add: int_is_not_ext) @@ -620,7 +620,7 @@ text \now conclusion fulfills induction hypothesis, but assumptions are not all ready\ text \assumption \schB\\ - apply (drule_tac x = "y2" and g = "Filter (\a. a \ act B) $ rs" in subst_lemma2) + apply (drule_tac x = "y2" and g = "Filter (\a. a \ act B) \ rs" in subst_lemma2) apply assumption apply (simp add: intA_is_not_actB int_is_not_ext) @@ -654,10 +654,10 @@ Forall (\x. x \ ext (A \ B)) tr \ Forall (\x. x \ act A) schA \ Forall (\x. x \ act B) schB \ - Filter (\a. a \ ext A) $ schA = Filter (\a. a \ act A) $ tr \ - Filter (\a. a \ ext B) $ schB = Filter (\a. a \ act B) $ tr \ + Filter (\a. a \ ext A) \ schA = Filter (\a. a \ act A) \ tr \ + Filter (\a. a \ ext B) \ schB = Filter (\a. a \ act B) \ tr \ LastActExtsch A schA \ LastActExtsch B schB - \ Filter (\a. a \ act B) $ (mksch A B $ tr $ schA $ schB) = schB" + \ Filter (\a. a \ act B) \ (mksch A B \ tr \ schA \ schB) = schB" apply (intro strip) apply (rule seq.take_lemma) apply (rule mp) @@ -726,7 +726,7 @@ text \eliminate the \A\-only prefix\ - apply (subgoal_tac "(Filter (\a. a \ act B) $ x1) = nil") + apply (subgoal_tac "(Filter (\a. a \ act B) \ 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 (\a. a \ act B \ a \ ext A) $ x1 = nil") + apply (subgoal_tac "Filter (\a. a \ act B \ a \ ext A) \ x1 = nil") apply (rotate_tac -1) apply simp text \eliminate introduced subgoal 2\ @@ -772,7 +772,7 @@ text \assumption \schA\\ apply (simp add: ext_and_act) text \assumption \schB\\ - apply (drule_tac x = "schB" and g = "Filter (\a. a \ act B) $ rs" in subst_lemma2) + apply (drule_tac x = "schB" and g = "Filter (\a. a \ act B) \ rs" in subst_lemma2) apply assumption apply (simp add: int_is_not_ext) text \assumptions concerning \LastActExtsch\, cannot be rewritten, as \LastActExtsmalli\ are looping\ @@ -790,7 +790,7 @@ apply (rotate_tac -2) apply simp - apply (subgoal_tac "Filter (\a. a \ act B \ a \ ext A) $ x1 = nil") + apply (subgoal_tac "Filter (\a. a \ act B \ a \ ext A) \ x1 = nil") apply (rotate_tac -1) apply simp text \eliminate introduced subgoal 2\ @@ -820,7 +820,7 @@ apply (frule_tac y = "x2" in sym [THEN eq_imp_below, THEN divide_Seq]) apply (erule conjE)+ text \assumption \schA\\ - apply (drule_tac x = "schB" and g = "Filter (\a. a \ act B) $ rs" in subst_lemma2) + apply (drule_tac x = "schB" and g = "Filter (\a. a \ act B) \ rs" in subst_lemma2) apply assumption apply (simp add: int_is_not_ext) @@ -836,7 +836,7 @@ text \now conclusion fulfills induction hypothesis, but assumptions are not all ready\ text \assumption \schA\\ - apply (drule_tac x = "x2" and g = "Filter (\a. a \ act A) $ rs" in subst_lemma2) + apply (drule_tac x = "x2" and g = "Filter (\a. a \ act A) \ 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 \ is_trans_of B \ compatible A B \ compatible B A \ is_asig (asig_of A) \ is_asig (asig_of B) \ tr \ traces (A \ B) \ - Filter (\a. a \ act A) $ tr \ traces A \ - Filter (\a. a \ act B) $ tr \ traces B \ + Filter (\a. a \ act A) \ tr \ traces A \ + Filter (\a. a \ act B) \ tr \ traces B \ Forall (\x. x \ ext(A \ B)) tr" apply (simp add: traces_def has_trace_def) apply auto text \\\\\ text \There is a schedule of \A\\ - apply (rule_tac x = "Filter (\a. a \ act A) $ sch" in bexI) + apply (rule_tac x = "Filter (\a. a \ act A) \ sch" in bexI) prefer 2 apply (simp add: compositionality_sch) apply (simp add: compatibility_consequence1 externals_of_par ext1_ext2_is_not_act1) text \There is a schedule of \B\\ - apply (rule_tac x = "Filter (\a. a \ act B) $ sch" in bexI) + apply (rule_tac x = "Filter (\a. a \ act B) \ 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 \\mksch\ is exactly the construction of \trA\B\ out of \schA\, \schB\, and the oracle \tr\, we need here\ - apply (rule_tac x = "mksch A B $ tr $ schA $ schB" in bexI) + apply (rule_tac x = "mksch A B \ tr \ schA \ schB" in bexI) text \External actions of mksch are just the oracle\ apply (simp add: FilterA_mksch_is_tr) diff -r 6c2c16fef8f1 -r b0d31c7def86 src/HOL/HOLCF/IOA/Compositionality.thy --- 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 \ Forall (\a. a \ ext A \ a \ ext B) tr \ - Filter (\a. a \ act A) $ tr = Filter (\a. a \ ext A) $ tr" + Filter (\a. a \ act A) \ tr = Filter (\a. a \ ext A) \ tr" apply (rule ForallPFilterQR) - text \i.e.: \(\x. P x \ (Q x = R x)) \ Forall P tr \ Filter Q $ tr = Filter R $ tr\\ + text \i.e.: \(\x. P x \ (Q x = R x)) \ Forall P tr \ Filter Q \ tr = Filter R \ tr\\ 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 \ Forall (\a. a \ ext B \ a \ ext A) tr \ - Filter (\a. a \ act A) $ tr = Filter (\a. a \ ext A) $ tr" + Filter (\a. a \ act A) \ tr = Filter (\a. a \ ext A) \ tr" apply (rule ForallPFilterQR) prefer 2 apply (assumption) apply (rule compatibility_consequence4) diff -r 6c2c16fef8f1 -r b0d31c7def86 src/HOL/HOLCF/IOA/Deadlock.thy --- 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 \Input actions may always be added to a schedule.\ lemma scheds_input_enabled: - "Filter (\x. x \ act A) $ sch \ schedules A \ a \ inp A \ input_enabled A \ Finite sch - \ Filter (\x. x \ act A) $ sch @@ a \ nil \ schedules A" + "Filter (\x. x \ act A) \ sch \ schedules A \ a \ inp A \ input_enabled A \ Finite sch + \ Filter (\x. x \ act A) \ sch @@ a \ nil \ 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 \ ex" in subst) prefer 2 apply assumption apply (erule_tac [2] FiniteFilter) @@ -60,7 +60,7 @@ assumes "a \ local A" and "Finite sch" and "sch \ schedules (A \ B)" - and "Filter (\x. x \ act A) $ (sch @@ a \ nil) \ schedules A" + and "Filter (\x. x \ act A) \ (sch @@ a \ nil) \ schedules A" and "compatible A B" and "input_enabled B" shows "(sch @@ a \ nil) \ schedules (A \ B)" diff -r 6c2c16fef8f1 -r b0d31c7def86 src/HOL/HOLCF/IOA/LiveIOA.thy --- 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 \ executions (fst AP) \ (exec \ snd AP)}" definition livetraces :: "('a, 's) live_ioa \ 'a trace set" - where "livetraces AP = {mk_trace (fst AP) $ (snd ex) |ex. ex \ liveexecutions AP}" + where "livetraces AP = {mk_trace (fst AP) \ (snd ex) |ex. ex \ liveexecutions AP}" definition live_implements :: "('a, 's1) live_ioa \ ('a, 's2) live_ioa \ bool" where "live_implements CL AM \ diff -r 6c2c16fef8f1 -r b0d31c7def86 src/HOL/HOLCF/IOA/RefCorrectness.thy --- 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 \ ('s1 \ 's2) \ ('a, 's1) pairs \ ('s1 \ ('a, 's2) pairs)" where "corresp_exC A f = - (fix $ + (fix \ (LAM h ex. (\s. case ex of nil \ nil | x ## xs \ flift1 (\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 \ xs) (snd pr))) \ x)))" definition corresp_ex :: "('a, 's2) ioa \ ('s1 \ 's2) \ ('a, 's1) execution \ ('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 \ (snd ex)) (fst ex))" definition is_fair_ref_map :: "('s1 \ 's2) \ ('a, 's1) ioa \ ('a, 's2) ioa \ bool" @@ -82,7 +82,7 @@ | x ## xs \ (flift1 (\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 \ xs) (snd pr))) \ 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 \ 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 \ nil) s = nil" apply (subst corresp_exC_unfold) apply simp done lemma corresp_exC_cons: - "(corresp_exC A f $ (at \ xs)) s = + "(corresp_exC A f \ (at \ 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 \ 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 \ reachable C s \ (s, a, t) \ trans_of C \ - mk_trace A $ ((SOME x. move A x (f s) a (f t))) = + mk_trace A \ ((SOME x. move A x (f s) a (f t))) = (if a \ ext A then a \ nil else nil)" apply (cut_tac move_is_move) defer @@ -172,7 +172,7 @@ text \Lemma 1.1: Distribution of \mk_trace\ and \@@\\ lemma mk_traceConc: - "mk_trace C $ (ex1 @@ ex2) = (mk_trace C $ ex1) @@ (mk_trace C $ ex2)" + "mk_trace C \ (ex1 @@ ex2) = (mk_trace C \ ex1) @@ (mk_trace C \ ex2)" by (simp add: mk_trace_def filter_act_def MapConc) @@ -181,7 +181,7 @@ lemma lemma_1: "is_ref_map f C A \ ext C = ext A \ \s. reachable C s \ is_exec_frag C (s, xs) \ - mk_trace C $ xs = mk_trace A $ (snd (corresp_ex A f (s, xs)))" + mk_trace C \ xs = mk_trace A \ (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) diff -r 6c2c16fef8f1 -r b0d31c7def86 src/HOL/HOLCF/IOA/RefMappings.thy --- 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 \ is_exec_frag ioa (s, ex) \ Finite ex \ laststate (s, ex) = t \ - mk_trace ioa $ ex = (if a \ ext ioa then a \ nil else nil)" + mk_trace ioa \ ex = (if a \ ext ioa then a \ nil else nil)" definition is_ref_map :: "('s1 \ 's2) \ ('a, 's1) ioa \ ('a, 's2) ioa \ bool" where "is_ref_map f C A \ diff -r 6c2c16fef8f1 -r b0d31c7def86 src/HOL/HOLCF/IOA/Seq.thy --- 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 \ 'b) \ 'a seq \ 'b seq" where - smap_nil: "smap $ f $ nil = nil" -| smap_cons: "x \ UU \ smap $ f $ (x ## xs) = (f $ x) ## smap $ f $ xs" + smap_nil: "smap \ f \ nil = nil" +| smap_cons: "x \ UU \ smap \ f \ (x ## xs) = (f \ x) ## smap \ f \ xs" -lemma smap_UU [simp]: "smap $ f $ UU = UU" +lemma smap_UU [simp]: "smap \ f \ UU = UU" by fixrec_simp @@ -43,13 +43,13 @@ fixrec sfilter :: "('a \ tr) \ 'a seq \ 'a seq" where - sfilter_nil: "sfilter $ P $ nil = nil" + sfilter_nil: "sfilter \ P \ nil = nil" | sfilter_cons: "x \ UU \ - sfilter $ P $ (x ## xs) = - (If P $ x then x ## (sfilter $ P $ xs) else sfilter $ P $ xs)" + sfilter \ P \ (x ## xs) = + (If P \ x then x ## (sfilter \ P \ xs) else sfilter \ P \ xs)" -lemma sfilter_UU [simp]: "sfilter $ P $ UU = UU" +lemma sfilter_UU [simp]: "sfilter \ P \ UU = UU" by fixrec_simp @@ -57,24 +57,24 @@ fixrec sforall2 :: "('a \ tr) \ 'a seq \ tr" where - sforall2_nil: "sforall2 $ P $ nil = TT" -| sforall2_cons: "x \ UU \ sforall2 $ P $ (x ## xs) = ((P $ x) andalso sforall2 $ P $ xs)" + sforall2_nil: "sforall2 \ P \ nil = TT" +| sforall2_cons: "x \ UU \ sforall2 \ P \ (x ## xs) = ((P \ x) andalso sforall2 \ P \ xs)" -lemma sforall2_UU [simp]: "sforall2 $ P $ UU = UU" +lemma sforall2_UU [simp]: "sforall2 \ P \ UU = UU" by fixrec_simp -definition "sforall P t = (sforall2 $ P $ t \ FF)" +definition "sforall P t \ sforall2 \ P \ t \ FF" subsubsection \\stakewhile\\ fixrec stakewhile :: "('a \ tr) \ 'a seq \ 'a seq" where - stakewhile_nil: "stakewhile $ P $ nil = nil" + stakewhile_nil: "stakewhile \ P \ nil = nil" | stakewhile_cons: - "x \ UU \ stakewhile $ P $ (x ## xs) = (If P $ x then x ## (stakewhile $ P $ xs) else nil)" + "x \ UU \ stakewhile \ P \ (x ## xs) = (If P \ x then x ## (stakewhile \ P \ xs) else nil)" -lemma stakewhile_UU [simp]: "stakewhile $ P $ UU = UU" +lemma stakewhile_UU [simp]: "stakewhile \ P \ UU = UU" by fixrec_simp @@ -82,11 +82,11 @@ fixrec sdropwhile :: "('a \ tr) \ 'a seq \ 'a seq" where - sdropwhile_nil: "sdropwhile $ P $ nil = nil" + sdropwhile_nil: "sdropwhile \ P \ nil = nil" | sdropwhile_cons: - "x \ UU \ sdropwhile $ P $ (x ## xs) = (If P $ x then sdropwhile $ P $ xs else x ## xs)" + "x \ UU \ sdropwhile \ P \ (x ## xs) = (If P \ x then sdropwhile \ P \ xs else x ## xs)" -lemma sdropwhile_UU [simp]: "sdropwhile $ P $ UU = UU" +lemma sdropwhile_UU [simp]: "sdropwhile \ P \ UU = UU" by fixrec_simp @@ -94,10 +94,10 @@ fixrec slast :: "'a seq \ 'a" where - slast_nil: "slast $ nil = UU" -| slast_cons: "x \ UU \ slast $ (x ## xs) = (If is_nil $ xs then x else slast $ xs)" + slast_nil: "slast \ nil = UU" +| slast_cons: "x \ UU \ slast \ (x ## xs) = (If is_nil \ xs then x else slast \ xs)" -lemma slast_UU [simp]: "slast $ UU = UU" +lemma slast_UU [simp]: "slast \ UU = UU" by fixrec_simp @@ -105,11 +105,11 @@ fixrec sconc :: "'a seq \ 'a seq \ 'a seq" where - sconc_nil: "sconc $ nil $ y = y" -| sconc_cons': "x \ UU \ sconc $ (x ## xs) $ y = x ## (sconc $ xs $ y)" + sconc_nil: "sconc \ nil \ y = y" +| sconc_cons': "x \ UU \ sconc \ (x ## xs) \ y = x ## (sconc \ xs \ y)" -abbreviation sconc_syn :: "'a seq => 'a seq => 'a seq" (infixr "@@" 65) - where "xs @@ ys \ sconc $ xs $ ys" +abbreviation sconc_syn :: "'a seq \ 'a seq \ 'a seq" (infixr "@@" 65) + where "xs @@ ys \ sconc \ xs \ ys" lemma sconc_UU [simp]: "UU @@ y = UU" by fixrec_simp @@ -124,13 +124,13 @@ fixrec sflat :: "'a seq seq \ 'a seq" where - sflat_nil: "sflat $ nil = nil" -| sflat_cons': "x \ UU \ sflat $ (x ## xs) = x @@ (sflat $ xs)" + sflat_nil: "sflat \ nil = nil" +| sflat_cons': "x \ UU \ sflat \ (x ## xs) = x @@ (sflat \ xs)" -lemma sflat_UU [simp]: "sflat $ UU = UU" +lemma sflat_UU [simp]: "sflat \ UU = UU" by fixrec_simp -lemma sflat_cons [simp]: "sflat $ (x ## xs) = x @@ (sflat $ xs)" +lemma sflat_cons [simp]: "sflat \ (x ## xs) = x @@ (sflat \ xs)" by (cases "x = UU") simp_all declare sflat_cons' [simp del] @@ -140,14 +140,14 @@ fixrec szip :: "'a seq \ 'b seq \ ('a \ 'b) seq" where - szip_nil: "szip $ nil $ y = nil" -| szip_cons_nil: "x \ UU \ szip $ (x ## xs) $ nil = UU" -| szip_cons: "x \ UU \ y \ UU \ szip $ (x ## xs) $ (y ## ys) = (x, y) ## szip $ xs $ ys" + szip_nil: "szip \ nil \ y = nil" +| szip_cons_nil: "x \ UU \ szip \ (x ## xs) \ nil = UU" +| szip_cons: "x \ UU \ y \ UU \ szip \ (x ## xs) \ (y ## ys) = (x, y) ## szip \ xs \ ys" -lemma szip_UU1 [simp]: "szip $ UU $ y = UU" +lemma szip_UU1 [simp]: "szip \ UU \ y = UU" by fixrec_simp -lemma szip_UU2 [simp]: "x \ nil \ szip $ x $ UU = UU" +lemma szip_UU2 [simp]: "x \ nil \ szip \ x \ 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 \ P \ (x @@ y) = (sfilter \ P \ x @@ sfilter \ P \ y)" apply (induct x) text \adm\ apply simp @@ -174,13 +174,13 @@ apply simp apply simp text \main case\ - apply (rule_tac p = "P$a" in trE) + apply (rule_tac p = "P\a" in trE) apply simp apply simp apply simp done -lemma sforallPstakewhileP: "sforall P (stakewhile $ P $ x)" +lemma sforallPstakewhileP: "sforall P (stakewhile \ P \ x)" apply (simp add: sforall_def) apply (induct x) text \adm\ @@ -189,13 +189,13 @@ apply simp apply simp text \main case\ - apply (rule_tac p = "P$a" in trE) + apply (rule_tac p = "P\a" in trE) apply simp apply simp apply simp done -lemma forallPsfilterP: "sforall P (sfilter $ P $ x)" +lemma forallPsfilterP: "sforall P (sfilter \ P \ x)" apply (simp add: sforall_def) apply (induct x) text \adm\ @@ -204,7 +204,7 @@ apply simp apply simp text \main case\ - apply (rule_tac p="P$a" in trE) + apply (rule_tac p="P\a" in trE) apply simp apply simp apply simp @@ -260,7 +260,7 @@ text \Extensions to Induction Theorems.\ lemma seq_finite_ind_lemma: - assumes "\n. P (seq_take n $ s)" + assumes "\n. P (seq_take n \ s)" shows "seq_finite s \ P s" apply (unfold seq.finite_def) apply (intro strip) diff -r 6c2c16fef8f1 -r b0d31c7def86 src/HOL/HOLCF/IOA/Sequence.thy --- 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 \ bool) \ 'a Seq \ 'a Seq" - where "Filter P = sfilter $ (flift2 P)" + where "Filter P = sfilter \ (flift2 P)" definition Map :: "('a \ 'b) \ 'a Seq \ 'b Seq" - where "Map f = smap $ (flift2 f)" + where "Map f = smap \ (flift2 f)" definition Forall :: "('a \ bool) \ 'a Seq \ bool" where "Forall P = sforall (flift2 P)" @@ -28,14 +28,14 @@ where "Last = slast" definition Dropwhile :: "('a \ bool) \ 'a Seq \ 'a Seq" - where "Dropwhile P = sdropwhile $ (flift2 P)" + where "Dropwhile P = sdropwhile \ (flift2 P)" definition Takewhile :: "('a \ bool) \ 'a Seq \ 'a Seq" - where "Takewhile P = stakewhile $ (flift2 P)" + where "Takewhile P = stakewhile \ (flift2 P)" definition Zip :: "'a Seq \ 'b Seq \ ('a * 'b) Seq" where "Zip = - (fix $ (LAM h t1 t2. + (fix \ (LAM h t1 t2. case t1 of nil \ nil | x ## xs \ @@ -47,24 +47,24 @@ | Def a \ (case y of UU \ UU - | Def b \ Def (a, b) ## (h $ xs $ ys))))))" + | Def b \ Def (a, b) ## (h \ xs \ ys))))))" definition Flat :: "'a Seq seq \ 'a Seq" where "Flat = sflat" definition Filter2 :: "('a \ bool) \ 'a Seq \ 'a Seq" where "Filter2 P = - (fix $ + (fix \ (LAM h t. case t of nil \ nil | x ## xs \ (case x of UU \ UU - | Def y \ (if P y then x ## (h $ xs) else h $ xs))))" + | Def y \ (if P y then x ## (h \ xs) else h \ xs))))" abbreviation Consq_syn ("(_/\_)" [66, 65] 65) - where "a \ s \ Consq a $ s" + where "a \ s \ Consq a \ s" subsection \List enumeration\ @@ -87,25 +87,25 @@ subsubsection \Map\ -lemma Map_UU: "Map f $ UU = UU" +lemma Map_UU: "Map f \ UU = UU" by (simp add: Map_def) -lemma Map_nil: "Map f $ nil = nil" +lemma Map_nil: "Map f \ nil = nil" by (simp add: Map_def) -lemma Map_cons: "Map f $ (x \ xs) = (f x) \ Map f $ xs" +lemma Map_cons: "Map f \ (x \ xs) = (f x) \ Map f \ xs" by (simp add: Map_def Consq_def flift2_def) subsubsection \Filter\ -lemma Filter_UU: "Filter P $ UU = UU" +lemma Filter_UU: "Filter P \ UU = UU" by (simp add: Filter_def) -lemma Filter_nil: "Filter P $ nil = nil" +lemma Filter_nil: "Filter P \ nil = nil" by (simp add: Filter_def) -lemma Filter_cons: "Filter P $ (x \ xs) = (if P x then x \ (Filter P $ xs) else Filter P $ xs)" +lemma Filter_cons: "Filter P \ (x \ xs) = (if P x then x \ (Filter P \ xs) else Filter P \ xs)" by (simp add: Filter_def Consq_def flift2_def If_and_if) @@ -129,50 +129,50 @@ subsubsection \Takewhile\ -lemma Takewhile_UU: "Takewhile P $ UU = UU" +lemma Takewhile_UU: "Takewhile P \ UU = UU" by (simp add: Takewhile_def) -lemma Takewhile_nil: "Takewhile P $ nil = nil" +lemma Takewhile_nil: "Takewhile P \ nil = nil" by (simp add: Takewhile_def) lemma Takewhile_cons: - "Takewhile P $ (x \ xs) = (if P x then x \ (Takewhile P $ xs) else nil)" + "Takewhile P \ (x \ xs) = (if P x then x \ (Takewhile P \ xs) else nil)" by (simp add: Takewhile_def Consq_def flift2_def If_and_if) subsubsection \DropWhile\ -lemma Dropwhile_UU: "Dropwhile P $ UU = UU" +lemma Dropwhile_UU: "Dropwhile P \ UU = UU" by (simp add: Dropwhile_def) -lemma Dropwhile_nil: "Dropwhile P $ nil = nil" +lemma Dropwhile_nil: "Dropwhile P \ nil = nil" by (simp add: Dropwhile_def) -lemma Dropwhile_cons: "Dropwhile P $ (x \ xs) = (if P x then Dropwhile P $ xs else x \ xs)" +lemma Dropwhile_cons: "Dropwhile P \ (x \ xs) = (if P x then Dropwhile P \ xs else x \ xs)" by (simp add: Dropwhile_def Consq_def flift2_def If_and_if) subsubsection \Last\ -lemma Last_UU: "Last $ UU =UU" +lemma Last_UU: "Last \ UU = UU" by (simp add: Last_def) -lemma Last_nil: "Last $ nil =UU" +lemma Last_nil: "Last \ nil = UU" by (simp add: Last_def) -lemma Last_cons: "Last $ (x \ xs) = (if xs = nil then Def x else Last $ xs)" +lemma Last_cons: "Last \ (x \ xs) = (if xs = nil then Def x else Last \ xs)" by (cases xs) (simp_all add: Last_def Consq_def) subsubsection \Flat\ -lemma Flat_UU: "Flat $ UU = UU" +lemma Flat_UU: "Flat \ UU = UU" by (simp add: Flat_def) -lemma Flat_nil: "Flat $ nil = nil" +lemma Flat_nil: "Flat \ nil = nil" by (simp add: Flat_def) -lemma Flat_cons: "Flat $ (x ## xs) = x @@ (Flat $ xs)" +lemma Flat_cons: "Flat \ (x ## xs) = x @@ (Flat \ xs)" by (simp add: Flat_def Consq_def) @@ -192,7 +192,7 @@ | Def a \ (case y of UU \ UU - | Def b \ Def (a, b) ## (Zip $ xs $ ys)))))" + | Def b \ Def (a, b) ## (Zip \ xs \ 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 \ UU \ y = UU" apply (subst Zip_unfold) apply simp done -lemma Zip_UU2: "x \ nil \ Zip $ x $ UU = UU" +lemma Zip_UU2: "x \ nil \ Zip \ x \ 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 \ nil \ y = nil" apply (subst Zip_unfold) apply simp done -lemma Zip_cons_nil: "Zip $ (x \ xs) $ nil = UU" +lemma Zip_cons_nil: "Zip \ (x \ xs) \ nil = UU" apply (subst Zip_unfold) apply (simp add: Consq_def) done -lemma Zip_cons: "Zip $ (x \ xs) $ (y \ ys) = (x, y) \ Zip $ xs $ ys" +lemma Zip_cons: "Zip \ (x \ xs) \ (y \ ys) = (x, y) \ Zip \ xs \ ys" apply (rule trans) apply (subst Zip_unfold) apply simp @@ -298,7 +298,7 @@ lemma Cons_inject_less_eq: "a \ s \ b \ t \ a = b \ s \ t" by (simp add: Consq_def2) -lemma seq_take_Cons: "seq_take (Suc n) $ (a \ x) = a \ (seq_take n $ x)" +lemma seq_take_Cons: "seq_take (Suc n) \ (a \ x) = a \ (seq_take n \ x)" by (simp add: Consq_def) lemmas [simp] = @@ -345,10 +345,10 @@ subsection \\HD\ and \TL\\ -lemma HD_Cons [simp]: "HD $ (x \ y) = Def x" +lemma HD_Cons [simp]: "HD \ (x \ y) = Def x" by (simp add: Consq_def) -lemma TL_Cons [simp]: "TL $ (x \ y) = y" +lemma TL_Cons [simp]: "TL \ (x \ y) = y" by (simp add: Consq_def) @@ -382,12 +382,12 @@ done -lemma FiniteMap1: "Finite s \ Finite (Map f $ s)" +lemma FiniteMap1: "Finite s \ Finite (Map f \ s)" apply (erule Seq_Finite_ind) apply simp_all done -lemma FiniteMap2: "Finite s \ \t. s = Map f $ t \ Finite t" +lemma FiniteMap2: "Finite s \ \t. s = Map f \ t \ 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 \ s) = Finite s" apply auto apply (erule FiniteMap2 [rule_format]) apply (rule refl) @@ -404,7 +404,7 @@ done -lemma FiniteFilter: "Finite s \ Finite (Filter P $ s)" +lemma FiniteFilter: "Finite s \ Finite (Filter P \ s)" apply (erule Seq_Finite_ind) apply simp_all done @@ -445,37 +445,37 @@ subsection \Last\ -lemma Finite_Last1: "Finite s \ s \ nil \ Last $ s \ UU" +lemma Finite_Last1: "Finite s \ s \ nil \ Last \ s \ UU" by (erule Seq_Finite_ind) simp_all -lemma Finite_Last2: "Finite s \ Last $ s = UU \ s = nil" +lemma Finite_Last2: "Finite s \ Last \ s = UU \ s = nil" by (erule Seq_Finite_ind) auto subsection \Filter, Conc\ -lemma FilterPQ: "Filter P $ (Filter Q $ s) = Filter (\x. P x \ Q x) $ s" +lemma FilterPQ: "Filter P \ (Filter Q \ s) = Filter (\x. P x \ Q x) \ 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 \ (x @@ y) = (Filter P \ x @@ Filter P \ y)" by (simp add: Filter_def sfiltersconc) subsection \Map\ -lemma MapMap: "Map f $ (Map g $ s) = Map (f \ g) $ s" +lemma MapMap: "Map f \ (Map g \ s) = Map (f \ g) \ 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 \ (x @@ y) = (Map f \ x) @@ (Map f \ y)" by (rule_tac x="x" in Seq_induct) simp_all -lemma MapFilter: "Filter P $ (Map f $ x) = Map f $ (Filter (P \ f) $ x)" +lemma MapFilter: "Filter P \ (Map f \ x) = Map f \ (Filter (P \ f) \ x)" by (rule_tac x="x" in Seq_induct) simp_all -lemma nilMap: "nil = (Map f $ s) \ s = nil" +lemma nilMap: "nil = (Map f \ s) \ s = nil" by (rule_tac x="s" in Seq_cases) simp_all -lemma ForallMap: "Forall P (Map f $ s) = Forall (P \ f) s" +lemma ForallMap: "Forall P (Map f \ s) = Forall (P \ 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 \ Forall P (x @@ y) \ Forall P x \ Forall P y" by (erule Seq_Finite_ind) simp_all -lemma ForallTL1: "Forall P s \ Forall P (TL $ s)" +lemma ForallTL1: "Forall P s \ Forall P (TL \ 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 \ Forall P (Dropwhile Q $ s)" +lemma ForallDropwhile1: "Forall P s \ Forall P (Dropwhile Q \ 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: - "(\x. P x \ Q x = R x) \ Forall P tr \ Filter Q $ tr = Filter R $ tr" + "(\x. P x \ Q x = R x) \ Forall P tr \ Filter Q \ tr = Filter R \ tr" apply (rule_tac x="tr" in Seq_induct) apply (simp add: Forall_def sforall_def) apply simp_all @@ -548,11 +548,11 @@ subsection \Forall, Filter\ -lemma ForallPFilterP: "Forall P (Filter P $ x)" +lemma ForallPFilterP: "Forall P (Filter P \ x)" by (simp add: Filter_def Forall_def forallPsfilterP) (*holds also in other direction, then equal to forallPfilterP*) -lemma ForallPFilterPid1: "Forall P x \ Filter P $ x = x" +lemma ForallPFilterPid1: "Forall P x \ Filter P \ 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 \ Forall (\x. \ P x) ys \ Filter P $ ys = nil" +lemma ForallnPFilterPnil1: "Finite ys \ Forall (\x. \ P x) ys \ Filter P \ ys = nil" by (erule Seq_Finite_ind) simp_all lemmas ForallnPFilterPnil = ForallnPFilterPnil1 [THEN mp] (*holds also in other direction*) -lemma ForallnPFilterPUU1: "\ Finite ys \ Forall (\x. \ P x) ys \ Filter P $ ys = UU" +lemma ForallnPFilterPUU1: "\ Finite ys \ Forall (\x. \ P x) ys \ Filter P \ 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 \ Forall (\x. \ P x) ys \ Finite ys" +lemma FilternPnilForallP [rule_format]: "Filter P \ ys = nil \ Forall (\x. \ P x) ys \ Finite ys" apply (rule_tac x="ys" in Seq_induct) text \adm\ apply (simp add: Forall_def sforall_def) @@ -591,13 +591,13 @@ (*inverse of ForallnPFilterPUU*) lemma FilternPUUForallP: - assumes "Filter P $ ys = UU" + assumes "Filter P \ ys = UU" shows "Forall (\x. \ P x) ys \ \ Finite ys" proof show "Forall (\x. \ P x) ys" proof (rule classical) assume "\ ?thesis" - then have "Filter P $ ys \ UU" + then have "Filter P \ ys \ UU" apply (rule rev_mp) apply (induct ys rule: Seq_induct) apply (simp add: Forall_def sforall_def) @@ -608,7 +608,7 @@ show "\ Finite ys" proof assume "Finite ys" - then have "Filter P$ys \ UU" + then have "Filter P\ys \ UU" by (rule Seq_Finite_ind) simp_all with assms show False by contradiction qed @@ -616,13 +616,13 @@ lemma ForallQFilterPnil: - "Forall Q ys \ Finite ys \ (\x. Q x \ \ P x) \ Filter P $ ys = nil" + "Forall Q ys \ Finite ys \ (\x. Q x \ \ P x) \ Filter P \ ys = nil" apply (erule ForallnPFilterPnil) apply (erule ForallPForallQ) apply auto done -lemma ForallQFilterPUU: "\ Finite ys \ Forall Q ys \ (\x. Q x \ \ P x) \ Filter P $ ys = UU" +lemma ForallQFilterPUU: "\ Finite ys \ Forall Q ys \ (\x. Q x \ \ P x) \ Filter P \ ys = UU" apply (erule ForallnPFilterPUU) apply (erule ForallPForallQ) apply auto @@ -631,11 +631,11 @@ subsection \Takewhile, Forall, Filter\ -lemma ForallPTakewhileP [simp]: "Forall P (Takewhile P $ x)" +lemma ForallPTakewhileP [simp]: "Forall P (Takewhile P \ x)" by (simp add: Forall_def Takewhile_def sforallPstakewhileP) -lemma ForallPTakewhileQ [simp]: "(\x. Q x \ P x) \ Forall P (Takewhile Q $ x)" +lemma ForallPTakewhileQ [simp]: "(\x. Q x \ P x) \ Forall P (Takewhile Q \ x)" apply (rule ForallPForallQ) apply (rule ForallPTakewhileP) apply auto @@ -643,7 +643,7 @@ lemma FilterPTakewhileQnil [simp]: - "Finite (Takewhile Q $ ys) \ (\x. Q x \ \ P x) \ Filter P $ (Takewhile Q $ ys) = nil" + "Finite (Takewhile Q \ ys) \ (\x. Q x \ \ P x) \ Filter P \ (Takewhile Q \ ys) = nil" apply (erule ForallnPFilterPnil) apply (rule ForallPForallQ) apply (rule ForallPTakewhileP) @@ -651,7 +651,7 @@ done lemma FilterPTakewhileQid [simp]: - "(\x. Q x \ P x) \ Filter P $ (Takewhile Q $ ys) = Takewhile Q $ ys" + "(\x. Q x \ P x) \ Filter P \ (Takewhile Q \ ys) = Takewhile Q \ 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 \ (Takewhile P \ s) = Takewhile P \ 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 \ Takewhile (\x. Q x \ (\ P x)) $ s = Takewhile Q $ s" + "Forall P s \ Takewhile (\x. Q x \ (\ P x)) \ s = Takewhile Q \ 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 \ Dropwhile (\x. Q x \ (\ P x)) $ s = Dropwhile Q $ s" + "Forall P s \ Dropwhile (\x. Q x \ (\ P x)) \ s = Dropwhile Q \ 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 \ Takewhile P $ (s @@ t) = s @@ (Takewhile P $ t)" +lemma TakewhileConc1: "Forall P s \ Takewhile P \ (s @@ t) = s @@ (Takewhile P \ 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 \ Forall P s \ Dropwhile P $ (s @@ t) = Dropwhile P $ t" +lemma DropwhileConc1: "Finite s \ Forall P s \ Dropwhile P \ (s @@ t) = Dropwhile P \ t" by (erule Seq_Finite_ind) simp_all lemmas DropwhileConc = DropwhileConc1 [THEN mp] @@ -697,9 +697,9 @@ subsection \Coinductive characterizations of Filter\ lemma divide_Seq_lemma: - "HD $ (Filter P $ y) = Def x \ - y = (Takewhile (\x. \ P x) $ y) @@ (x \ TL $ (Dropwhile (\a. \ P a) $ y)) \ - Finite (Takewhile (\x. \ P x) $ y) \ P x" + "HD \ (Filter P \ y) = Def x \ + y = (Takewhile (\x. \ P x) \ y) @@ (x \ TL \ (Dropwhile (\a. \ P a) \ y)) \ + Finite (Takewhile (\x. \ P x) \ y) \ 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 \ xs) \ Filter P $ y \ - y = ((Takewhile (\a. \ P a) $ y) @@ (x \ TL $ (Dropwhile (\a. \ P a) $ y))) \ - Finite (Takewhile (\a. \ P a) $ y) \ P x" +lemma divide_Seq: "(x \ xs) \ Filter P \ y \ + y = ((Takewhile (\a. \ P a) \ y) @@ (x \ TL \ (Dropwhile (\a. \ P a) \ y))) \ + Finite (Takewhile (\a. \ P a) \ y) \ P x" apply (rule divide_Seq_lemma [THEN mp]) apply (drule_tac f="HD" and x="x \ xs" in monofun_cfun_arg) apply simp done -lemma nForall_HDFilter: "\ Forall P y \ (\x. HD $ (Filter (\a. \ P a) $ y) = Def x)" +lemma nForall_HDFilter: "\ Forall P y \ (\x. HD \ (Filter (\a. \ P a) \ 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: "\ Forall P y \ - \x. y = Takewhile P$y @@ (x \ TL $ (Dropwhile P $ y)) \ Finite (Takewhile P $ y) \ \ P x" + \x. y = Takewhile P\y @@ (x \ TL \ (Dropwhile P \ y)) \ Finite (Takewhile P \ y) \ \ P x" apply (drule nForall_HDFilter [THEN mp]) apply safe apply (rule_tac x="x" in exI) @@ -752,15 +752,15 @@ subsection \Take-lemma\ -lemma seq_take_lemma: "(\n. seq_take n $ x = seq_take n $ x') \ x = x'" +lemma seq_take_lemma: "(\n. seq_take n \ x = seq_take n \ x') \ x = x'" apply (rule iffI) apply (rule seq.take_lemma) apply auto done lemma take_reduction1: - "\n. ((\k. k < n \ seq_take k $ y1 = seq_take k $ y2) \ - seq_take n $ (x @@ (t \ y1)) = seq_take n $ (x @@ (t \ y2)))" + "\n. ((\k. k < n \ seq_take k \ y1 = seq_take k \ y2) \ + seq_take n \ (x @@ (t \ y1)) = seq_take n \ (x @@ (t \ 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 \ s = t \ (\k. k < n \ seq_take k $ y1 = seq_take k $ y2) - \ seq_take n $ (x @@ (s \ y1)) = seq_take n $ (y @@ (t \ y2))" + "x = y \ s = t \ (\k. k < n \ seq_take k \ y1 = seq_take k \ y2) + \ seq_take n \ (x @@ (s \ y1)) = seq_take n \ (y @@ (t \ y2))" by (auto intro!: take_reduction1 [rule_format]) @@ -781,8 +781,8 @@ \ lemma take_reduction_less1: - "\n. ((\k. k < n \ seq_take k $ y1 \ seq_take k$y2) \ - seq_take n $ (x @@ (t \ y1)) \ seq_take n $ (x @@ (t \ y2)))" + "\n. ((\k. k < n \ seq_take k \ y1 \ seq_take k\y2) \ + seq_take n \ (x @@ (t \ y1)) \ seq_take n \ (x @@ (t \ 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 \ s = t \ (\k. k < n \ seq_take k $ y1 \ seq_take k $ y2) \ - seq_take n $ (x @@ (s \ y1)) \ seq_take n $ (y @@ (t \ y2))" + "x = y \ s = t \ (\k. k < n \ seq_take k \ y1 \ seq_take k \ y2) \ + seq_take n \ (x @@ (s \ y1)) \ seq_take n \ (y @@ (t \ y2))" by (auto intro!: take_reduction_less1 [rule_format]) lemma take_lemma_less1: - assumes "\n. seq_take n $ s1 \ seq_take n $ s2" + assumes "\n. seq_take n \ s1 \ seq_take n \ s2" shows "s1 \ 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: "(\n. seq_take n $ x \ seq_take n $ x') \ x \ x'" +lemma take_lemma_less: "(\n. seq_take n \ x \ seq_take n \ x') \ x \ x'" apply (rule iffI) apply (rule take_lemma_less1) apply auto @@ -828,7 +828,7 @@ lemma take_lemma_principle2: assumes "\s. Forall Q s \ A s \ f s = g s" and "\s1 s2 y. Forall Q s1 \ Finite s1 \ \ Q y \ A (s1 @@ y \ s2) \ - \n. seq_take n $ (f (s1 @@ y \ s2)) = seq_take n $ (g (s1 @@ y \ s2))" + \n. seq_take n \ (f (s1 @@ y \ s2)) = seq_take n \ (g (s1 @@ y \ s2))" shows "A x \ f x = g x" using assms apply (cases "Forall Q x") @@ -852,10 +852,10 @@ lemma take_lemma_induct: assumes "\s. Forall Q s \ A s \ f s = g s" and "\s1 s2 y n. - \t. A t \ seq_take n $ (f t) = seq_take n $ (g t) \ + \t. A t \ seq_take n \ (f t) = seq_take n \ (g t) \ Forall Q s1 \ Finite s1 \ \ Q y \ A (s1 @@ y \ s2) \ - seq_take (Suc n) $ (f (s1 @@ y \ s2)) = - seq_take (Suc n) $ (g (s1 @@ y \ s2))" + seq_take (Suc n) \ (f (s1 @@ y \ s2)) = + seq_take (Suc n) \ (g (s1 @@ y \ s2))" shows "A x \ f x = g x" apply (insert assms) apply (rule impI) @@ -875,10 +875,10 @@ lemma take_lemma_less_induct: assumes "\s. Forall Q s \ A s \ f s = g s" and "\s1 s2 y n. - \t m. m < n \ A t \ seq_take m $ (f t) = seq_take m $ (g t) \ + \t m. m < n \ A t \ seq_take m \ (f t) = seq_take m \ (g t) \ Forall Q s1 \ Finite s1 \ \ Q y \ A (s1 @@ y \ s2) \ - seq_take n $ (f (s1 @@ y \ s2)) = - seq_take n $ (g (s1 @@ y \ s2))" + seq_take n \ (f (s1 @@ y \ s2)) = + seq_take n \ (g (s1 @@ y \ s2))" shows "A x \ f x = g x" apply (insert assms) apply (rule impI) @@ -899,9 +899,9 @@ assumes "A UU \ f UU = g UU" and "A nil \ f nil = g nil" and "\s y n. - \t. A t \ seq_take n $ (f t) = seq_take n $ (g t) \ A (y \ s) \ - seq_take (Suc n) $ (f (y \ s)) = - seq_take (Suc n) $ (g (y \ s))" + \t. A t \ seq_take n \ (f t) = seq_take n \ (g t) \ A (y \ s) \ + seq_take (Suc n) \ (f (y \ s)) = + seq_take (Suc n) \ (g (y \ s))" shows "A x \ f x = g x" apply (insert assms) apply (rule impI) @@ -928,21 +928,21 @@ as for the entire proof?*) lemma Filter_lemma1: "Forall (\x. \ (P x \ Q x)) s \ - Filter P $ (Filter Q $ s) = Filter (\x. P x \ Q x) $ s" + Filter P \ (Filter Q \ s) = Filter (\x. P x \ Q x) \ 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 \ - Forall (\x. \ P x \ \ Q x) s \ Filter P $ (Filter Q $ s) = nil" + Forall (\x. \ P x \ \ Q x) s \ Filter P \ (Filter Q \ s) = nil" by (erule Seq_Finite_ind) simp_all lemma Filter_lemma3: "Finite s \ - Forall (\x. \ P x \ \ Q x) s \ Filter (\x. P x \ Q x) $ s = nil" + Forall (\x. \ P x \ \ Q x) s \ Filter (\x. P x \ Q x) \ s = nil" by (erule Seq_Finite_ind) simp_all -lemma FilterPQ_takelemma: "Filter P $ (Filter Q $ s) = Filter (\x. P x \ Q x) $ s" +lemma FilterPQ_takelemma: "Filter P \ (Filter Q \ s) = Filter (\x. P x \ Q x) \ s" apply (rule_tac A1="\x. True" and Q1="\x. \ (P x \ Q x)" and x1="s" in take_lemma_induct [THEN mp]) (*better support for A = \x. True*) @@ -956,7 +956,7 @@ subsubsection \Alternative Proof of \MapConc\\ -lemma MapConc_takelemma: "Map f $ (x @@ y) = (Map f $ x) @@ (Map f $ y)" +lemma MapConc_takelemma: "Map f \ (x @@ y) = (Map f \ x) @@ (Map f \ y)" apply (rule_tac A1="\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))\ -lemma Mapnil: "Map f $ s = nil \ s = nil" +lemma Mapnil: "Map f \ s = nil \ s = nil" by (Seq_case_simp s) -lemma MapUU: "Map f $ s = UU \ s = UU" +lemma MapUU: "Map f \ s = UU \ s = UU" by (Seq_case_simp s) -lemma MapTL: "Map f $ (TL $ s) = TL $ (Map f $ s)" +lemma MapTL: "Map f \ (TL \ s) = TL \ (Map f \ s)" by (Seq_induct s) end diff -r 6c2c16fef8f1 -r b0d31c7def86 src/HOL/HOLCF/IOA/ShortExecutions.thy --- 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 \ bool) \ 'a Seq \ 'a Seq \ 'a Seq" where "oraclebuild P = - (fix $ + (fix \ (LAM h s t. case t of nil \ nil @@ -23,11 +23,11 @@ (case x of UU \ UU | Def y \ - (Takewhile (\x. \ P x) $ s) @@ - (y \ (h $ (TL $ (Dropwhile (\x. \ P x) $ s)) $ xs)))))" + (Takewhile (\x. \ P x) \ s) @@ + (y \ (h \ (TL \ (Dropwhile (\x. \ P x) \ s)) \ xs)))))" definition Cut :: "('a \ bool) \ 'a Seq \ 'a Seq" - where "Cut P s = oraclebuild P $ s $ (Filter P $ s)" + where "Cut P s = oraclebuild P \ s \ (Filter P \ s)" definition LastActExtsch :: "('a,'s) ioa \ 'a Seq \ bool" where "LastActExtsch A sch \ Cut (\x. x \ ext A) sch = sch" @@ -36,7 +36,7 @@ Cut_prefixcl_Finite: "Finite s \ \y. s = Cut P s @@ y" axiomatization where - LastActExtsmall1: "LastActExtsch A sch \ LastActExtsch A (TL $ (Dropwhile P $ sch))" + LastActExtsmall1: "LastActExtsch A sch \ LastActExtsch A (TL \ (Dropwhile P \ sch))" axiomatization where LastActExtsmall2: "Finite sch1 \ LastActExtsch A (sch1 @@ sch2) \ LastActExtsch A sch2" @@ -60,8 +60,8 @@ (case x of UU \ UU | Def y \ - (Takewhile (\a. \ P a) $ s) @@ - (y \ (oraclebuild P $ (TL $ (Dropwhile (\a. \ P a) $ s)) $ xs))))" + (Takewhile (\a. \ P a) \ s) @@ + (y \ (oraclebuild P \ (TL \ (Dropwhile (\a. \ P a) \ s)) \ 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 \ sch \ UU = UU" apply (subst oraclebuild_unfold) apply simp done -lemma oraclebuild_nil: "oraclebuild P $ sch $ nil = nil" +lemma oraclebuild_nil: "oraclebuild P \ sch \ nil = nil" apply (subst oraclebuild_unfold) apply simp done lemma oraclebuild_cons: - "oraclebuild P $ s $ (x \ t) = - (Takewhile (\a. \ P a) $ s) @@ - (x \ (oraclebuild P $ (TL $ (Dropwhile (\a. \ P a) $ s)) $ t))" + "oraclebuild P \ s \ (x \ t) = + (Takewhile (\a. \ P a) \ s) @@ + (x \ (oraclebuild P \ (TL \ (Dropwhile (\a. \ P a) \ s)) \ t))" apply (rule trans) apply (subst oraclebuild_unfold) apply (simp add: Consq_def) @@ -94,7 +94,7 @@ lemma Cut_nil: "Forall (\a. \ P a) s \ Finite s \ Cut P s = nil" apply (unfold Cut_def) - apply (subgoal_tac "Filter P $ s = nil") + apply (subgoal_tac "Filter P \ s = nil") apply (simp add: oraclebuild_nil) apply (rule ForallQFilterPnil) apply assumption+ @@ -102,7 +102,7 @@ lemma Cut_UU: "Forall (\a. \ P a) s \ \ Finite s \ Cut P s = UU" apply (unfold Cut_def) - apply (subgoal_tac "Filter P $ s = UU") + apply (subgoal_tac "Filter P \ s = UU") apply (simp add: oraclebuild_UU) apply (rule ForallQFilterPUU) apply assumption+ @@ -118,7 +118,7 @@ subsection \Cut lemmas for main theorem\ -lemma FilterCut: "Filter P $ s = Filter P $ (Cut P s)" +lemma FilterCut: "Filter P \ s = Filter P \ (Cut P s)" apply (rule_tac A1 = "\x. True" and Q1 = "\x. \ 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 \ f) s) = Cut P (Map f$s)" +lemma MapCut: "Map f\(Cut (P \ f) s) = Cut P (Map f\s)" apply (rule_tac A1 = "\x. True" and Q1 = "\x. \ P (f x) " and x1 = "s" in take_lemma_less_induct [THEN mp]) prefer 3 @@ -206,11 +206,11 @@ subsection \Main Cut Theorem\ lemma exists_LastActExtsch: - "sch \ schedules A \ tr = Filter (\a. a \ ext A) $ sch \ - \sch. sch \ schedules A \ tr = Filter (\a. a \ ext A) $ sch \ LastActExtsch A sch" + "sch \ schedules A \ tr = Filter (\a. a \ ext A) \ sch \ + \sch. sch \ schedules A \ tr = Filter (\a. a \ ext A) \ sch \ LastActExtsch A sch" apply (unfold schedules_def has_schedule_def [abs_def]) apply auto - apply (rule_tac x = "filter_act $ (Cut (\a. fst a \ ext A) (snd ex))" in exI) + apply (rule_tac x = "filter_act \ (Cut (\a. fst a \ ext A) (snd ex))" in exI) apply (simp add: executions_def) apply (pair ex) apply auto @@ -222,13 +222,13 @@ text \Subgoal 2: Lemma: \Filter P s = Filter P (Cut P s)\\ apply (simp add: filter_act_def) - apply (subgoal_tac "Map fst $ (Cut (\a. fst a \ ext A) x2) = Cut (\a. a \ ext A) (Map fst $ x2)") + apply (subgoal_tac "Map fst \ (Cut (\a. fst a \ ext A) x2) = Cut (\a. a \ ext A) (Map fst \ x2)") apply (rule_tac [2] MapCut [unfolded o_def]) apply (simp add: FilterCut [symmetric]) text \Subgoal 3: Lemma: \Cut\ idempotent\ apply (simp add: LastActExtsch_def filter_act_def) - apply (subgoal_tac "Map fst $ (Cut (\a. fst a \ ext A) x2) = Cut (\a. a \ ext A) (Map fst $ x2)") + apply (subgoal_tac "Map fst \ (Cut (\a. fst a \ ext A) x2) = Cut (\a. a \ ext A) (Map fst \ x2)") apply (rule_tac [2] MapCut [unfolded o_def]) apply (simp add: Cut_idemp) done @@ -236,7 +236,7 @@ subsection \Further Cut lemmas\ -lemma LastActExtimplnil: "LastActExtsch A sch \ Filter (\x. x \ ext A) $ sch = nil \ sch = nil" +lemma LastActExtimplnil: "LastActExtsch A sch \ Filter (\x. x \ ext A) \ sch = nil \ sch = nil" apply (unfold LastActExtsch_def) apply (drule FilternPnilForallP) apply (erule conjE) @@ -245,7 +245,7 @@ apply simp done -lemma LastActExtimplUU: "LastActExtsch A sch \ Filter (\x. x \ ext A) $ sch = UU \ sch = UU" +lemma LastActExtimplUU: "LastActExtsch A sch \ Filter (\x. x \ ext A) \ sch = UU \ sch = UU" apply (unfold LastActExtsch_def) apply (drule FilternPUUForallP) apply (erule conjE) diff -r 6c2c16fef8f1 -r b0d31c7def86 src/HOL/HOLCF/IOA/SimCorrectness.thy --- 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 \ ('s1 \ 's2) set \ ('a, 's1) pairs \ ('s2 \ ('a, 's2) pairs)" where "corresp_ex_simC A R = - (fix $ (LAM h ex. (\s. case ex of + (fix \ (LAM h ex. (\s. case ex of nil \ nil | x ## xs \ (flift1 @@ -21,13 +21,13 @@ a = fst pr; t = snd pr; T' = SOME t'. \ex1. (t, t') \ R \ 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 \ xs) T')) \ x))))" definition corresp_ex_sim :: "('a, 's2) ioa \ ('s1 \ 's2) set \ ('a, 's1) execution \ ('a, 's2) execution" where "corresp_ex_sim A R ex \ let S' = SOME s'. (fst ex, s') \ R \ s' \ starts_of A - in (S', (corresp_ex_simC A R $ (snd ex)) S')" + in (S', (corresp_ex_simC A R \ (snd ex)) S')" subsection \\corresp_ex_sim\\ @@ -43,7 +43,7 @@ a = fst pr; t = snd pr; T' = SOME t'. \ex1. (t, t') \ R \ 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 \ xs) T')) \ 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 \ 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 \ 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) \ xs)) s = + "(corresp_ex_simC A R \ ((a, t) \ xs)) s = (let T' = SOME t'. \ex1. (t, t') \ R \ 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 \ 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 \ reachable C s \ s \a\C\ t \ (s, s') \ R \ let T' = SOME t'. \ex1. (t, t') \ R \ move A ex1 s' a t' - in mk_trace A $ (SOME x. move A x s' a T') = (if a \ ext A then a \ nil else nil)" + in mk_trace A \ (SOME x. move A x s' a T') = (if a \ ext A then a \ 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 \ ext C = ext A \ \s s'. reachable C s \ is_exec_frag C (s, ex) \ (s, s') \ R \ - mk_trace C $ ex = mk_trace A $ ((corresp_ex_simC A R $ ex) s')" + mk_trace C \ ex = mk_trace A \ ((corresp_ex_simC A R \ ex) s')" supply if_split [split del] apply (pair_induct ex simp: is_exec_frag_def) text \cons case\ @@ -181,7 +181,7 @@ lemma correspsim_is_execution [rule_format]: "is_simulation R C A \ \s s'. reachable C s \ is_exec_frag C (s, ex) \ (s, s') \ R - \ is_exec_frag A (s', (corresp_ex_simC A R $ ex) s')" + \ is_exec_frag A (s', (corresp_ex_simC A R \ ex) s')" apply (pair_induct ex simp: is_exec_frag_def) text \main case\ apply auto diff -r 6c2c16fef8f1 -r b0d31c7def86 src/HOL/HOLCF/IOA/TL.thy --- 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 \ y)" definition Init :: "'a predicate \ 'a temporal" ("\_\" [0] 1000) - where "Init P s = P (unlift (HD $ s))" + where "Init P s = P (unlift (HD \ s))" \ \this means that for \nil\ and \UU\ the effect is unpredictable\ definition Next :: "'a temporal \ 'a temporal" ("\(_)" [80] 80) - where "(\P) s \ (if TL $ s = UU \ TL $ s = nil then P s else P (TL $ s))" + where "(\P) s \ (if TL \ s = UU \ TL \ s = nil then P s else P (TL \ s))" definition suffix :: "'a Seq \ 'a Seq \ bool" where "suffix s2 s \ (\s1. Finite s1 \ s = s1 @@ s2)" @@ -110,7 +110,7 @@ subsection \LTL Axioms by Manna/Pnueli\ -lemma tsuffix_TL [rule_format]: "s \ UU \ s \ nil \ tsuffix s2 (TL $ s) \ tsuffix s2 s" +lemma tsuffix_TL [rule_format]: "s \ UU \ s \ nil \ tsuffix s2 (TL \ s) \ tsuffix s2 s" apply (unfold tsuffix_def suffix_def) apply auto apply (Seq_case_simp s) diff -r 6c2c16fef8f1 -r b0d31c7def86 src/HOL/HOLCF/IOA/TLS.thy --- 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 \ ('s \ ('a option, 's) transition Seq)" where "ex2seqC = - (fix $ (LAM h ex. (\s. case ex of + (fix \ (LAM h ex. (\s. case ex of nil \ (s, None, s) \ nil - | x ## xs \ (flift1 (\pr. (s, Some (fst pr), snd pr) \ (h $ xs) (snd pr)) $ x))))" + | x ## xs \ (flift1 (\pr. (s, Some (fst pr), snd pr) \ (h \ xs) (snd pr)) \ x))))" definition ex2seq :: "('a, 's) execution \ ('a option, 's) transition Seq" - where "ex2seq ex = (ex2seqC $ (mkfin (snd ex))) (fst ex)" + where "ex2seq ex = (ex2seqC \ (mkfin (snd ex))) (fst ex)" definition temp_sat :: "('a, 's) execution \ ('a, 's) ioa_temp \ bool" (infixr "\" 22) where "(ex \ P) \ ((ex2seq ex) \ P)" @@ -83,7 +83,7 @@ (LAM ex. (\s. case ex of nil \ (s, None, s) \ nil | x ## xs \ - (flift1 (\pr. (s, Some (fst pr), snd pr) \ (ex2seqC $ xs) (snd pr)) $ x)))" + (flift1 (\pr. (s, Some (fst pr), snd pr) \ (ex2seqC \ xs) (snd pr)) \ 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 \ UU) s = UU" apply (subst ex2seqC_unfold) apply simp done -lemma ex2seqC_nil [simp]: "(ex2seqC $ nil) s = (s, None, s) \ nil" +lemma ex2seqC_nil [simp]: "(ex2seqC \ nil) s = (s, None, s) \ nil" apply (subst ex2seqC_unfold) apply simp done -lemma ex2seqC_cons [simp]: "(ex2seqC $ ((a, t) \ xs)) s = (s, Some a,t ) \ (ex2seqC $ xs) t" +lemma ex2seqC_cons [simp]: "(ex2seqC \ ((a, t) \ xs)) s = (s, Some a,t ) \ (ex2seqC \ xs) t" apply (rule trans) apply (subst ex2seqC_unfold) apply (simp add: Consq_def flift1_def) diff -r 6c2c16fef8f1 -r b0d31c7def86 src/HOL/HOLCF/IOA/Traces.thy --- 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 \ ('a, 's) pairs \ 's \ tr" where "is_exec_fragC A = - (fix $ + (fix \ (LAM h ex. (\s. case ex of nil \ TT - | x ## xs \ flift1 (\p. Def ((s, p) \ trans_of A) andalso (h $ xs) (snd p)) $ x)))" + | x ## xs \ flift1 (\p. Def ((s, p) \ trans_of A) andalso (h \ xs) (snd p)) \ x)))" definition is_exec_frag :: "('a, 's) ioa \ ('a, 's) execution \ bool" - where "is_exec_frag A ex \ (is_exec_fragC A $ (snd ex)) (fst ex) \ FF" + where "is_exec_frag A ex \ (is_exec_fragC A \ (snd ex)) (fst ex) \ FF" definition executions :: "('a, 's) ioa \ ('a, 's) execution set" where "executions ioa = {e. fst e \ starts_of ioa \ is_exec_frag ioa e}" @@ -42,7 +42,7 @@ where "filter_act = Map fst" definition has_schedule :: "('a, 's) ioa \ 'a trace \ bool" - where "has_schedule ioa sch \ (\ex \ executions ioa. sch = filter_act $ (snd ex))" + where "has_schedule ioa sch \ (\ex \ executions ioa. sch = filter_act \ (snd ex))" definition schedules :: "('a, 's) ioa \ 'a trace set" where "schedules ioa = {sch. has_schedule ioa sch}" @@ -51,26 +51,26 @@ subsection \Traces\ definition has_trace :: "('a, 's) ioa \ 'a trace \ bool" - where "has_trace ioa tr \ (\sch \ schedules ioa. tr = Filter (\a. a \ ext ioa) $ sch)" + where "has_trace ioa tr \ (\sch \ schedules ioa. tr = Filter (\a. a \ ext ioa) \ sch)" definition traces :: "('a, 's) ioa \ 'a trace set" where "traces ioa \ {tr. has_trace ioa tr}" definition mk_trace :: "('a, 's) ioa \ ('a, 's) pairs \ 'a trace" - where "mk_trace ioa = (LAM tr. Filter (\a. a \ ext ioa) $ (filter_act $ tr))" + where "mk_trace ioa = (LAM tr. Filter (\a. a \ ext ioa) \ (filter_act \ tr))" subsection \Fair Traces\ definition laststate :: "('a, 's) execution \ 's" where "laststate ex = - (case Last $ (snd ex) of + (case Last \ (snd ex) of UU \ fst ex | Def at \ snd at)" text \A predicate holds infinitely (finitely) often in a sequence.\ definition inf_often :: "('a \ bool) \ 'a Seq \ bool" - where "inf_often P s \ Infinite (Filter P $ s)" + where "inf_often P s \ Infinite (Filter P \ s)" text \Filtering \P\ yields a finite or partial sequence.\ definition fin_often :: "('a \ bool) \ 'a Seq \ bool" @@ -122,7 +122,7 @@ where "fairexecutions A = {ex. ex \ executions A \ fair_ex A ex}" definition fairtraces :: "('a, 's) ioa \ 'a trace set" - where "fairtraces A = {mk_trace A $ (snd ex) | ex. ex \ fairexecutions A}" + where "fairtraces A = {mk_trace A \ (snd ex) | ex. ex \ fairexecutions A}" subsection \Implementation\ @@ -167,13 +167,13 @@ subsubsection \\filter_act\\ -lemma filter_act_UU: "filter_act $ UU = UU" +lemma filter_act_UU: "filter_act \ UU = UU" by (simp add: filter_act_def) -lemma filter_act_nil: "filter_act $ nil = nil" +lemma filter_act_nil: "filter_act \ nil = nil" by (simp add: filter_act_def) -lemma filter_act_cons: "filter_act $ (x \ xs) = fst x \ filter_act $ xs" +lemma filter_act_cons: "filter_act \ (x \ xs) = fst x \ filter_act \ 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 \\mk_trace\\ -lemma mk_trace_UU: "mk_trace A $ UU = UU" +lemma mk_trace_UU: "mk_trace A \ UU = UU" by (simp add: mk_trace_def) -lemma mk_trace_nil: "mk_trace A $ nil = nil" +lemma mk_trace_nil: "mk_trace A \ nil = nil" by (simp add: mk_trace_def) lemma mk_trace_cons: - "mk_trace A $ (at \ xs) = + "mk_trace A \ (at \ xs) = (if fst at \ ext A - then fst at \ mk_trace A $ xs - else mk_trace A $ xs)" + then fst at \ mk_trace A \ xs + else mk_trace A \ 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 \ TT | x ## xs \ - (flift1 (\p. Def ((s, p) \ trans_of A) andalso (is_exec_fragC A$xs) (snd p)) $ x)))" + (flift1 (\p. Def ((s, p) \ trans_of A) andalso (is_exec_fragC A\xs) (snd p)) \ 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 \ 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 \ nil) s = TT" apply (subst is_exec_fragC_unfold) apply simp done lemma is_exec_fragC_cons: - "(is_exec_fragC A $ (pr \ xs)) s = - (Def ((s, pr) \ trans_of A) andalso (is_exec_fragC A $ xs) (snd pr))" + "(is_exec_fragC A \ (pr \ xs)) s = + (Def ((s, pr) \ trans_of A) andalso (is_exec_fragC A \ 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 \ (\ex \ executions A. b = mk_trace A $ (snd ex))" +lemma has_trace_def2: "has_trace A b \ (\ex \ executions A. b = mk_trace A \ (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 @@ \ lemma execfrag_in_sig: - "is_trans_of A \ \s. is_exec_frag A (s, xs) \ Forall (\a. a \ act A) (filter_act $ xs)" + "is_trans_of A \ \s. is_exec_frag A (s, xs) \ Forall (\a. a \ act A) (filter_act \ xs)" apply (pair_induct xs simp: is_exec_frag_def Forall_def sforall_def) text \main case\ apply (auto simp add: is_trans_of_def) done lemma exec_in_sig: - "is_trans_of A \ x \ executions A \ Forall (\a. a \ act A) (filter_act $ (snd x))" + "is_trans_of A \ x \ executions A \ Forall (\a. a \ act A) (filter_act \ (snd x))" apply (simp add: executions_def) apply (pair x) apply (rule execfrag_in_sig [THEN spec, THEN mp]) diff -r 6c2c16fef8f1 -r b0d31c7def86 src/HOL/HOLCF/Library/Stream.thy --- 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 \ 'a stream \ 'a stream" where (* chops the first i elements *) + "i_rt = (\i s. iterate i\rt\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 \ 'a stream \ 'a" where (* the i-th element *) + "i_th = (\i s. ft\(i_rt i s))" definition - sconc :: "'a stream => 'a stream => 'a stream" (infixr "ooo" 65) where + sconc :: "'a stream \ 'a stream \ 'a stream" (infixr "ooo" 65) where "s1 ooo s2 = (case #s1 of - enat n \ (SOME s. (stream_take n$s=s1) & (i_rt n s = s2)) + enat n \ (SOME s. (stream_take n\s = s1) \ (i_rt n s = s2)) | \ \ s1)" -primrec constr_sconc' :: "nat => 'a stream => 'a stream => 'a stream" +primrec constr_sconc' :: "nat \ 'a stream \ 'a stream \ '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\s1 && constr_sconc' n (rt\s1) s2" definition - constr_sconc :: "'a stream => 'a stream => 'a stream" where (* constructive *) + constr_sconc :: "'a stream \ 'a stream \ 'a stream" where (* constructive *) "constr_sconc s1 s2 = (case #s1 of enat n \ constr_sconc' n s1 s2 | \ \ 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: "\a && x = UU; a \ UU\ \ R" by simp -lemma stream_exhaust_eq: "(x ~= UU) = (EX a y. a ~= UU & x = a && y)" +lemma stream_exhaust_eq: "x \ UU \ (\a y. a \ UU \ 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 \ UU \ \a a_s. x = a && a_s \ a \ 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" + "\a && s \ t; a \ UU\ \ \b tt. t = b && tt \ b \ UU \ s \ 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 \ UU \ x \ b && z = + (x = UU \ (\a y. x = a && y \ a \ UU \ a \ b \ y \ z))" by (cases x, auto) (* -lemma stream_prefix1: "[| x< x&&xs << y&&ys" -by (insert stream_prefix' [of y "x&&xs" ys],force) +lemma stream_prefix1: "\x \ y; xs \ ys\ \ x && xs \ 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) + "\x && xs \ y && ys; (x::'a::flat) \ UU\ \ x = y \ xs \ 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\UU\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 \ UU \ ft\s \ UU" by simp -lemma rt_strict_rev: "rt$s~=UU ==> s~=UU" +lemma rt_strict_rev: "rt\s \ UU \ s \ UU" by auto -lemma surjectiv_scons: "(ft$s)&&(rt$s)=s" +lemma surjectiv_scons: "(ft\s) && (rt\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 \ s \ iterate i\rt\x \ iterate i\rt\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\s) = s" by (rule stream.reach) -lemma chain_stream_take: "chain (%i. stream_take i$s)" +lemma chain_stream_take: "chain (\i. stream_take i\s)" by simp -lemma stream_take_prefix [simp]: "stream_take n$s << s" +lemma stream_take_prefix [simp]: "stream_take n\s \ 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" + "\x. stream_take n\x = x \ stream_take (Suc n)\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" + "\x xs. x \ UU \ stream_take n\(x && xs) = x && xs \ stream_take n\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" + "\x xs. stream_take n\xs = xs \ stream_take (Suc n)\(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" + "\s. stream_take n\(stream_take n\s) = stream_take n\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" + "\s. stream_take n\(stream_take (Suc n)\s) = stream_take n\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)\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) (* 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)\s1 \ stream_take (Suc n)\s2 \ + stream_take n\s1 \ stream_take n\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" + "\k\n. stream_take n\s1 \ stream_take n\s2 \ stream_take k\s1 \ stream_take k\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 \ n \ stream_take k\s1 \ stream_take n\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 \ s2 \ stream_take n\s1 \ stream_take n\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\s \ s" +apply (subgoal_tac "s=(LUB n. stream_take n\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\(stream_take n\s) \ stream_take k\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" + "\stream_finite x; P UU; \a s. \a \ UU; P s\ \ P (a && s)\ \ 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)" + "\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)" 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" +"\ 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" 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: "\s1 s2. R s1 s2 \ ft\s1 = ft\s2 \ R (rt\s1) (rt\s2) \ 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: "\ stream_finite s \ s \ 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 \ 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: "\x \ UU; stream_finite (x && xs)\ \ 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\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< stream_finite t" +lemma stream_finite_less: "stream_finite s \ \t. t \ s \ 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\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 (\x. \ 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]: "#\ = 0" by (simp add: slen_def stream.finite_def zero_enat_def Least_equality) -lemma slen_scons [simp]: "x ~= \ ==> #(x&&xs) = eSuc (#xs)" +lemma slen_scons [simp]: "x \ \ \ #(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 = \)" by (cases x) auto -lemma slen_scons_eq: "(enat (Suc n) < #x) = (? a y. x = a && y & a ~= \ & enat n < #y)" +lemma slen_scons_eq: "(enat (Suc n) < #x) = (? a y. x = a && y \ a \ \ \ 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 ~= \ & #y = n)" +lemma slen_eSuc: "#x = eSuc n \ (\a y. x = a && y \ a \ \ \ #y = n)" by (cases x) auto -lemma slen_stream_take_finite [simp]: "#(stream_take n$s) ~= \" +lemma slen_stream_take_finite [simp]: "#(stream_take n\s) \ \" by (simp add: slen_def) -lemma slen_scons_eq_rev: "(#x < enat (Suc (Suc n))) = (!a y. x ~= a && y | a = \ | #y < enat (Suc n))" +lemma slen_scons_eq_rev: "#x < enat (Suc (Suc n)) \ (\a y. x \ a && y \ a = \ \ #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" + "\s. stream_take n\s \ s \ #(stream_take n\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\(stream_take n\s) = stream_take n\s" +apply (case_tac "stream_take n\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\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\(stream_take (Suc n)\s) = + stream_take n\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\s = stream_take n\(stream_take n\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\x ~= x)" +lemma slen_take_eq: "\x. enat n < #x \ stream_take n\x \ 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\x = x)" +lemma slen_take_eq_rev: "#x \ enat n \ stream_take n\x = x" by (simp add: linorder_not_less [symmetric] slen_take_eq) -lemma slen_take_lemma1: "#x = enat n ==> stream_take n\x = x" +lemma slen_take_lemma1: "#x = enat n \ stream_take n\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 \ #s1 \ #(rt\s2) \ #(rt\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\s) \ enat n" +apply (case_tac "stream_take n\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\x) = enat i" +lemma slen_take_lemma2: "\x. \ stream_finite x \ #(stream_take i\x) = enat i" apply (simp add: stream.finite_def, auto) apply (simp add: slen_take_lemma4) done -lemma slen_infinite: "stream_finite x = (#x ~= \)" +lemma slen_infinite: "stream_finite x \ #x \ \" 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 \ \t. s \ t \ #s \ #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 \ t \ #s \ #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\(iterate n\F\x) = iterate n\F\(F\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]: "\x. enat (i + j) \ #x \ enat j \ #(iterate i\rt\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\x = stream_take n\y" + "\(x::'a::flat stream) y. enat n \ #x \ x \ y \ stream_take n\x = stream_take n\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 \ \s. #(s::'a::flat stream) = #t \ s \ t \ 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: "\stream_finite t; s \ t; s \ (t::'a::flat stream)\ \ #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)\s \ s \ + stream_take n\s \ stream_take (Suc n)\s" apply auto -apply (subgoal_tac "stream_take n$s ~=s") +apply (subgoal_tac "stream_take n\s \ 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 = (\ f t. case t of x&&xs \ f$x && smap$f$xs)" +lemma smap_unfold: "smap = (\ f t. case t of x && xs \ f\x && smap\f\xs)" by (insert smap_def [where 'a='a and 'b='b, THEN eq_reflection, THEN fix_eq2], auto) lemma smap_empty [simp]: "smap\f\\ = \" by (subst smap_unfold, simp) -lemma smap_scons [simp]: "x~=\ ==> smap\f\(x&&xs) = (f\x)&&(smap\f\xs)" +lemma smap_scons [simp]: "x \ \ \ smap\f\(x && xs) = (f\x) && (smap\f\xs)" by (subst smap_unfold, force) @@ -548,7 +545,7 @@ by (subst sfilter_unfold, force) lemma sfilter_scons [simp]: - "x ~= \ ==> sfilter\f\(x && xs) = + "x \ \ \ sfilter\f\(x && xs) = If f\x then x && sfilter\f\xs else sfilter\f\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 \ UU \ 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\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\(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 \ 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) \ #x \ enat j \ #(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 \ #s1 \ #(i_rt n s2) \ #(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]: "\s. i_rt n (stream_take n\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 \ stream_take n\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\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 \ 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: "\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" 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 "\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 |] ==> +"\enat sl = #x; n \ sl; #(stream_take n\x) = enat t; #(i_rt n x) = enat j\ \ 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" + "\s. i_th n (stream_take (Suc n)\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)\s)" +apply (insert surjectiv_scons [of "i_rt n (stream_take (Suc n)\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 \ i_rt n (stream_take (Suc n)\s1) = i_rt n (stream_take (Suc n)\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 |] ==> +"\k \ n; stream_take (Suc n)\s1 << stream_take (Suc n)\s2\ \ 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)\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" 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" +"\stream_take n\s1 << stream_take n\s2; i_rt n s1 << i_rt n s2\ \ 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\s1 << stream_take 0\s2 \ 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 \ + (stream_take n\s1 << stream_take n\s2 \ 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" + "\stream_take n\s1 = stream_take n\s2; i_rt n s1 = i_rt n s2\ \ 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 \ UU \ a && s \ UU" by auto -lemma singleton_sconc [rule_format, simp]: "x~=UU --> (x && UU) ooo y = x && y" +lemma singleton_sconc [rule_format, simp]: "x \ UU \ (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)" + "\k y. #x = enat k \ (\w. stream_take k\w = x \ 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 \ 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 \ stream_take n\(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 \ UU \ (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 \ UU \ ft\(x ooo y) = ft\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' \ 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 \ x = UU \ 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 \ UU \ rt\(s ooo x) = rt\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" + "\x y. enat n < #x \ 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]: "\s. stream_take n\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)\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 i_th_stream_take_eq: -"!!n. ALL n. i_th n s1 = i_th n s2 ==> stream_take n$s1 = stream_take n$s2" + "\n. \n. i_th n s1 = i_th n s2 \ stream_take n\s1 = stream_take n\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)\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 (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]: "\n. i_th n s1 = i_th n s2 \ 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) = \; enat n = #x |] ==> #y = \" -apply (case_tac "#y ~= \",auto) + "\#(x ooo y) = \; enat n = #x\ \ #y = \" +apply (case_tac "#y \ \",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=\ ==> #(x ooo y) = \" +lemma slen_sconc_infinite1: "#x=\ \ #(x ooo y) = \" by (simp add: sconc_def) -lemma slen_sconc_infinite2: "#y=\ ==> #(x ooo y) = \" +lemma slen_sconc_infinite2: "#y=\ \ #(x ooo y) = \" 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~=\ & #y~=\) = (#(x ooo y)~=\)" +lemma sconc_finite: "#x \ \ \ #y \ \ \ #(x ooo y) \ \" 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: "\enat n = #x; enat k = #(x ooo y)\ \ n \ 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: "\enat n = #x; enat m = #y\ \ #(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 \ \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\s1 = stream_take nat\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 \ chain (\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 \ chain (\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 \ (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 \ stream_finite x \ (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 \ (LUB i. x ooo Y i) = (x ooo (LUB i. Y i))" apply (case_tac "#x=\") 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 (\y. x ooo y)" by (simp add: monofun_def sconc_mono) diff -r 6c2c16fef8f1 -r b0d31c7def86 src/HOL/HOLCF/ex/Dagstuhl.thy --- 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\(LAM x. y && x)" definition YYS :: "'a stream" where - "YYS = fix$(LAM z. y && y && z)" + "YYS = fix\(LAM z. y && y && z)" lemma YS_def2: "YS = y && YS" apply (rule trans) diff -r 6c2c16fef8f1 -r b0d31c7def86 src/HOL/HOLCF/ex/Dnat.thy --- 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 \ ('a \ 'a) \ 'a \ 'a" where + "iterator = fix\(LAM h n f x. + case n of dzero \ x + | dsucc\m \ f\(h\m\f\x))" text \ \medskip Expand fixed point properties. \ 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 \ x | dsucc\m \ f\(iterator\m\f\x))" apply (rule trans) apply (rule fix_eq2) apply (rule iterator_def [THEN eq_reflection]) @@ -31,17 +31,17 @@ text \\medskip Recursive properties.\ -lemma iterator1: "iterator $ UU $ f $ x = UU" +lemma iterator1: "iterator\UU\f\x = UU" apply (subst iterator_def2) apply simp done -lemma iterator2: "iterator $ dzero $ f $ x = x" +lemma iterator2: "iterator\dzero\f\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 \ UU \ iterator\(dsucc\n)\f\x = f\(iterator\n\f\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< x=UU | x=y" +lemma dnat_flat: "\x y::dnat. x \ y \ x = UU \ 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 "\y. dnat \ y \ dnat = UU \ dnat = y") apply simp apply (simp (no_asm_simp)) apply (drule_tac x="dnata" in spec) diff -r 6c2c16fef8f1 -r b0d31c7def86 src/HOL/HOLCF/ex/Fix2.thy --- 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 \ 'a) \'a" where + gix1_def: "F\(gix\F) = gix\F" and + gix2_def: "F\y = y \ gix\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\F = lub (range (\i. iterate i\F\UU))" apply (rule lemma1 [THEN subst]) apply (rule fix_def2) done diff -r 6c2c16fef8f1 -r b0d31c7def86 src/HOL/HOLCF/ex/Focus_ex.thy --- 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) \ 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 \ '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))" 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 \ '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))" 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 \ 'c stream) \ bool" where + "is_g g \ (\f. is_f f \ (\x y. g\x = y \ 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 \ 'c stream) => bool" where + "def_g g \ (\f. is_f f \ g = (LAM x. fst (f\(x, fix\(LAM k. snd (f\(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 \ + (\f. is_f(f) \ (\x.(\z. (g\x,z) = f\(x,z) \ (\w y. (y, w) = f\(x, w) \ 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)))" + "(\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)))" 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 \ is_g g" apply (tactic \simp_tac (put_simpset HOL_ss @{context} addsimps [@{thm def_g_def}, @{thm lemma1}, @{thm lemma2}]) 1\) 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\(LAM k. snd (f\(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 \ def_g g" apply (tactic \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\) @@ -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\(LAM k. snd (f\(x, k))) = z") apply simp -apply (subgoal_tac "! w y. f$(x, w) = (y, w) --> z << w") +apply (subgoal_tac "\w y. f\(x, w) = (y, w) \ z << w") apply (rule fix_eqI) apply simp -apply (subgoal_tac "f$(x, za) = (fst (f$(x,za)) ,za)") +apply (subgoal_tac "f\(x, za) = (fst (f\(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 ))" + "(\f. is_f (f::'b stream * ('b,'c) tc stream \ 'c stream * ('b,'c) tc stream)) \ + (\g. def_g (g::'b stream \ '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 ))" + "(\f. is_f (f::'b stream * ('b,'c) tc stream \ 'c stream * ('b,'c) tc stream)) \ + (\g. is_g (g::'b stream \ 'c stream))" apply (rule loopback_eq [THEN subst]) apply (rule L2) done diff -r 6c2c16fef8f1 -r b0d31c7def86 src/HOL/HOLCF/ex/Hoare.thy --- 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 \ tr" and + b2 :: "'a \ tr" and + g :: "'a \ 'a" definition - p :: "'a -> 'a" where - "p = fix$(LAM f. LAM x. If b1$x then f$(g$x) else x)" + p :: "'a \ 'a" where + "p = fix\(LAM f. LAM x. If b1\x then f\(g\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 \ 'a" where + "q = fix\(LAM f. LAM x. If b1\x orelse b2\x then f\(g\x) else x)" (* --------- pure HOLCF logic, some little lemmas ------ *) -lemma hoare_lemma2: "b~=TT ==> b=FF | b=UU" +lemma hoare_lemma2: "b \ TT \ b = FF \ 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: "(\k. b1\(iterate k\g\x) = TT) \ (\k. b1\(iterate k\g\x) \ 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: "(\k. b1\(iterate k\g\x) \ TT) \ + \k. b1\(iterate k\g\x) = FF \ b1\(iterate k\g\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: "\(\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" 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 \ b \ TT" apply hypsubst apply (rule dist_eq_tr) done -lemma hoare_lemma7: "b=FF ==> b~=TT" +lemma hoare_lemma7: "b = FF \ b \ 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: "\(\k. b1\(iterate k\g\x) \ TT); + k = Least (\n. b1\(iterate n\g\x) \ TT)\ \ + \m. m < k \ b1\(iterate m\g\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\(iterate m\g\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\(y::'a) = (UU::tr) \ f\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\x = If b1\x then p\(g\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\x = If b1\x orelse b2\x then q\(g\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: "(\m. m < Suc k \ b1\(iterate m\g\x) = TT) \ + p\(iterate k\g\x) = p\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\(iterate n\g\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\(iterate n\g\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: "(\m. m < Suc k \ b1\(iterate m\g\x) = TT) \ + q\(iterate k\g\x) = q\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\(iterate n\g\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\(iterate n\g\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 (\k. b1\(iterate k\g\x) \ 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" + "\k. b1\(iterate k\g\x) \ TT + \ Suc k = (LEAST n. b1\(iterate n\g\x) \ TT) \ p\(iterate k\g\x) = p\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: "(\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" 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\(iterate nat\g\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: "(\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" 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\(iterate nat\g\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 (\k. b1\(iterate k\g\x) = TT) ------- *) -lemma fernpass_lemma: "(ALL k. b1$(iterate k$g$x)=TT) ==> ALL k. p$(iterate k$g$x) = UU" +lemma fernpass_lemma: "(\k. b1\(iterate k\g\x) = TT) \ \k. p\(iterate k\g\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\(iterate k\g\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: "(\k. b1\(iterate k\g\x) = TT) \ p\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 (\k. b1\(iterate k\g\x) = TT) ------- *) -lemma hoare_lemma17: "(ALL k. b1$(iterate k$g$x)=TT) ==> ALL k. q$(iterate k$g$x) = UU" +lemma hoare_lemma17: "(\k. b1\(iterate k\g\x) = TT) \ \k. q\(iterate k\g\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\(iterate k\g\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: "(\k. b1\(iterate k\g\x) = TT) \ q\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)" + "(\k. (b1::'a\tr)\(iterate k\g\x) = TT) \ b1\(UU::'a) = UU \ (\y. b1\(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: "(\y. b1\(y::'a) = TT) \ \k. q\(iterate k\g\(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\(iterate k\g\(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: "(\y. b1\(y::'a) = TT) \ q\(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\(UU::'a) = UU \ q\(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 (\k. b1\(iterate k\g\x) \ 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: "\k. b1\(iterate k\g\x) \ TT + \ Suc k = (LEAST n. b1\(iterate n\g\x) \ TT) \ q\(iterate k\g\x) = q\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: "(\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)" 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\(iterate nat\g\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: "(\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" 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\(iterate nat\g\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 ----- *) +(* ------- (\k. b1\(iterate k\g\x) = TT) \ q \ p = q ----- *) -lemma hoare_lemma23: "(ALL k. b1$(iterate k$g$x)=TT) ==> q$(p$x) = q$x" +lemma hoare_lemma23: "(\k. b1\(iterate k\g\x) = TT) \ q\(p\x) = q\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 ----- *) +(* ------------ \k. b1\(iterate k\g\x) \ TT \ q \ p = q ----- *) -lemma hoare_lemma29: "EX k. b1$(iterate k$g$x) ~= TT ==> q$(p$x) = q$x" +lemma hoare_lemma29: "\k. b1\(iterate k\g\x) \ TT \ q\(p\x) = q\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 \ p = q ------ *) theorem hoare_main: "q oo p = q" apply (rule cfun_eqI) diff -r 6c2c16fef8f1 -r b0d31c7def86 src/HOL/HOLCF/ex/Loop.thy --- 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 \ tr) \ ('a \ 'a) \ 'a \ 'a" where + "step = (LAM b g x. If b\x then g\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 \ tr) \ ('a \ 'a) \ 'a \ 'a" where + "while = (LAM b g. fix\(LAM f x. If b\x then f\(g\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\b\g\x = If b\x then g\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\b\g = fix\(LAM f x. If b\x then f\(g\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\b\g\x = If b\x then while\b\g\(g\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: "\x. while\b\g\x = while\b\g\(iterate k\(step\b\g)\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\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\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\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) 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: "\EX y. b\y = FF; iterate k\(step\b\g)\x = UU\ + \ iterate(Suc k)\(step\b\g)\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: "\\y. b\y = FF; iterate (Suc k)\(step\b\g)\x \ UU\ \ + iterate k\(step\b\g)\x \ 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)" + "\\x. INV x \ b\x = TT \ g\x \ UU \ INV (g\x); + \y. b\y = FF; INV x\ + \ iterate k\(step\b\g)\x \ UU \ INV (iterate k\(step\b\g)\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\(iterate n\(step\b\g)\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)\(step\b\g)\x" + and t = "g\(iterate n\(step\b\g)\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" + "\x. b\(iterate k\(step\b\g)\x) = FF \ while\b\g\x = iterate k\(step\b\g)\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" + "\k. b\(iterate k\(step\b\g)\x) \ FF \ + \m. while\b\g\(iterate m\(step\b\g)\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\(iterate m\(step\b\g)\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\(iterate (Suc m)\(step\b\g)\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: "\k. b\(iterate k\(step\b\g)\x) \ FF \ while\b\g\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\b\g\x \ UU \ \k. b\(iterate k\(step\b\g)\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) +"\(\y. INV y \ b\y = TT \ g\y \ UU \ INV (g\y)); + (\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) 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: "\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)" apply (rule loop_inv2) apply (rule_tac [3] premP [THEN premI]) apply (rule_tac [3] premW) @@ -197,4 +197,3 @@ done end -