# HG changeset patch # User wenzelm # Date 1451508972 -3600 # Node ID 1f2788fb0b8beff0eefc177ac895b69733367a80 # Parent 8cba509ace9cd38edc630d320e1a5c78afdddc70 more symbols; diff -r 8cba509ace9c -r 1f2788fb0b8b src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy --- a/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy Wed Dec 30 21:52:00 2015 +0100 +++ b/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy Wed Dec 30 21:56:12 2015 +0100 @@ -75,7 +75,7 @@ lemma cex_abs_nil: "cex_abs f (s,nil) = (f s, nil)" by (simp add: cex_abs_def) -lemma cex_abs_cons: "cex_abs f (s,(a,t)>>ex) = (f s, (a,f t) >> (snd (cex_abs f (t,ex))))" +lemma cex_abs_cons: "cex_abs f (s,(a,t)\ex) = (f s, (a,f t) \ (snd (cex_abs f (t,ex))))" by (simp add: cex_abs_def) declare cex_abs_UU [simp] cex_abs_nil [simp] cex_abs_cons [simp] @@ -177,7 +177,7 @@ "is_abstraction h C A ==> is_ref_map h C A" apply (unfold is_abstraction_def is_ref_map_def) apply auto -apply (rule_tac x = "(a,h t) >>nil" in exI) +apply (rule_tac x = "(a,h t) \nil" in exI) apply (simp add: move_def) done diff -r 8cba509ace9c -r 1f2788fb0b8b src/HOL/HOLCF/IOA/meta_theory/CompoExecs.thy --- a/src/HOL/HOLCF/IOA/meta_theory/CompoExecs.thy Wed Dec 30 21:52:00 2015 +0100 +++ b/src/HOL/HOLCF/IOA/meta_theory/CompoExecs.thy Wed Dec 30 21:56:12 2015 +0100 @@ -81,7 +81,7 @@ apply (simp add: ProjA2_def) done -lemma ProjA2_cons: "ProjA2$((a,t)>>xs) = (a,fst t) >> ProjA2$xs" +lemma ProjA2_cons: "ProjA2$((a,t)\xs) = (a,fst t) \ ProjA2$xs" apply (simp add: ProjA2_def) done @@ -99,7 +99,7 @@ apply (simp add: ProjB2_def) done -lemma ProjB2_cons: "ProjB2$((a,t)>>xs) = (a,snd t) >> ProjB2$xs" +lemma ProjB2_cons: "ProjB2$((a,t)\xs) = (a,snd t) \ ProjB2$xs" apply (simp add: ProjB2_def) done @@ -118,9 +118,9 @@ apply (simp add: Filter_ex2_def) done -lemma Filter_ex2_cons: "Filter_ex2 sig$(at >> xs) = +lemma Filter_ex2_cons: "Filter_ex2 sig$(at \ xs) = (if (fst at:actions sig) - then at >> (Filter_ex2 sig$xs) + then at \ (Filter_ex2 sig$xs) else Filter_ex2 sig$xs)" apply (simp add: Filter_ex2_def) @@ -158,7 +158,7 @@ apply simp done -lemma stutter2_cons: "(stutter2 sig$(at>>xs)) s = +lemma stutter2_cons: "(stutter2 sig$(at\xs)) s = ((if (fst at)~:actions sig then Def (s=snd at) else TT) andalso (stutter2 sig$xs) (snd at))" apply (rule trans) @@ -183,7 +183,7 @@ apply (simp add: stutter_def) done -lemma stutter_cons: "stutter sig (s, (a,t)>>ex) = +lemma stutter_cons: "stutter sig (s, (a,t)\ex) = ((a~:actions sig --> (s=t)) & stutter sig (t,ex))" apply (simp add: stutter_def) done diff -r 8cba509ace9c -r 1f2788fb0b8b src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy --- a/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy Wed Dec 30 21:52:00 2015 +0100 +++ b/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy Wed Dec 30 21:56:12 2015 +0100 @@ -25,20 +25,20 @@ | Def a => (case HD$exB of UU => UU | Def b => - (y,(snd a,snd b))>> + (y,(snd a,snd b))\ (h$xs$(TL$exA)$(TL$exB)) (snd a) (snd b))) else (case HD$exA of UU => UU | Def a => - (y,(snd a,t))>>(h$xs$(TL$exA)$exB) (snd a) t) + (y,(snd a,t))\(h$xs$(TL$exA)$exB) (snd a) t) ) else (if y:act B then (case HD$exB of UU => UU | Def b => - (y,(s,snd b))>>(h$xs$exA$(TL$exB)) s (snd b)) + (y,(s,snd b))\(h$xs$exA$(TL$exB)) s (snd b)) else UU ) @@ -81,20 +81,20 @@ | Def a => (case HD$exB of UU => UU | Def b => - (y,(snd a,snd b))>> + (y,(snd a,snd b))\ (mkex2 A B$xs$(TL$exA)$(TL$exB)) (snd a) (snd b))) else (case HD$exA of UU => UU | Def a => - (y,(snd a,t))>>(mkex2 A B$xs$(TL$exA)$exB) (snd a) t) + (y,(snd a,t))\(mkex2 A B$xs$(TL$exA)$exB) (snd a) t) ) else (if y:act B then (case HD$exB of UU => UU | Def b => - (y,(s,snd b))>>(mkex2 A B$xs$exA$(TL$exB)) s (snd b)) + (y,(s,snd b))\(mkex2 A B$xs$exA$(TL$exB)) s (snd b)) else UU ) @@ -118,8 +118,8 @@ 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" + ==> (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) @@ -127,8 +127,8 @@ 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)" + ==> (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) @@ -136,8 +136,8 @@ 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$(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) @@ -160,26 +160,26 @@ done lemma mkex_cons_1: "[| x:act A; x~:act B |] - ==> mkex A B (x>>sch) (s,a>>exA) (t,exB) = - ((s,t), (x,snd a,t) >> snd (mkex A B sch (snd a,exA) (t,exB)))" + ==> mkex A B (x\sch) (s,a\exA) (t,exB) = + ((s,t), (x,snd a,t) \ snd (mkex A B sch (snd a,exA) (t,exB)))" apply (simp (no_asm) add: mkex_def) -apply (cut_tac exA = "a>>exA" in mkex2_cons_1) +apply (cut_tac exA = "a\exA" in mkex2_cons_1) apply auto done lemma mkex_cons_2: "[| x~:act A; x:act B |] - ==> mkex A B (x>>sch) (s,exA) (t,b>>exB) = - ((s,t), (x,s,snd b) >> snd (mkex A B sch (s,exA) (snd b,exB)))" + ==> mkex A B (x\sch) (s,exA) (t,b\exB) = + ((s,t), (x,s,snd b) \ snd (mkex A B sch (s,exA) (snd b,exB)))" apply (simp (no_asm) add: mkex_def) -apply (cut_tac exB = "b>>exB" in mkex2_cons_2) +apply (cut_tac exB = "b\exB" in mkex2_cons_2) apply auto done lemma mkex_cons_3: "[| x:act A; x:act B |] - ==> mkex A B (x>>sch) (s,a>>exA) (t,b>>exB) = - ((s,t), (x,snd a,snd b) >> snd (mkex A B sch (snd a,exA) (snd b,exB)))" + ==> mkex A B (x\sch) (s,a\exA) (t,b\exB) = + ((s,t), (x,snd a,snd b) \ snd (mkex A B sch (snd a,exA) (snd b,exB)))" apply (simp (no_asm) add: mkex_def) -apply (cut_tac exB = "b>>exB" and exA = "a>>exA" in mkex2_cons_3) +apply (cut_tac exB = "b\exB" and exA = "a\exA" in mkex2_cons_3) apply auto done @@ -262,10 +262,10 @@ apply (tactic {* Seq_case_simp_tac @{context} "exA" 1 *}) (* Case exA=UU, Case exA=nil*) (* These UU and nil cases are the only places where the assumption filter A sch< to generate a contradiction using ~a>>ss<< UU(nil), using theorems + is used! --> to generate a contradiction using ~a\ss<< UU(nil), using theorems Cons_not_less_UU and Cons_not_less_nil *) apply (tactic {* Seq_case_simp_tac @{context} "exB" 1 *}) -(* Case exA=a>>x, exB=b>>y *) +(* Case exA=a\x, exB=b\y *) (* here it is important that Seq_case_simp_tac uses no !full!_simp_tac for the cons case, as otherwise mkex_cons_3 would not be rewritten without use of rotate_tac: then tactic would not be generally applicable *) diff -r 8cba509ace9c -r 1f2788fb0b8b src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy --- a/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy Wed Dec 30 21:52:00 2015 +0100 +++ b/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy Wed Dec 30 21:56:12 2015 +0100 @@ -27,20 +27,20 @@ (if y:act B then ((Takewhile (%a. a:int A)$schA) @@ (Takewhile (%a. a:int B)$schB) - @@ (y>>(h$xs + @@ (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 + @@ (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 + @@ (y\(h$xs $schA $(TL$(Dropwhile (%a. a:int B)$schB)) ))) @@ -86,20 +86,20 @@ (if y:act B then ((Takewhile (%a. a:int A)$schA) @@(Takewhile (%a. a:int B)$schB) - @@(y>>(mksch A B$xs + @@(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 + @@ (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 + @@ (y\(mksch A B$xs $schA $(TL$(Dropwhile (%a. a:int B)$schB)) ))) @@ -126,9 +126,9 @@ done lemma mksch_cons1: "[|x:act A;x~:act B|] - ==> mksch A B$(x>>tr)$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)) + @@ (x\(mksch A B$tr$(TL$(Dropwhile (%a. a:int A)$schA)) $schB))" apply (rule trans) apply (subst mksch_unfold) @@ -137,9 +137,9 @@ done lemma mksch_cons2: "[|x~:act A;x:act B|] - ==> mksch A B$(x>>tr)$schA$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)) + @@ (x\(mksch A B$tr$schA$(TL$(Dropwhile (%a. a:int B)$schB)) ))" apply (rule trans) apply (subst mksch_unfold) @@ -148,10 +148,10 @@ done lemma mksch_cons3: "[|x:act A;x:act B|] - ==> mksch A B$(x>>tr)$schA$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)) + @@ (x\(mksch A B$tr$(TL$(Dropwhile (%a. a:int A)$schA)) $(TL$(Dropwhile (%a. a:int B)$schB)))) )" apply (rule trans) @@ -194,7 +194,7 @@ by (erule subst) (* Lemma for substitution of looping assumption in another specific assumption *) -lemma subst_lemma2: "[| (f x) = y >> g; x=(h x) |] ==> (f (h x)) = y >> g" +lemma subst_lemma2: "[| (f x) = y \ g; x=(h x) |] ==> (f (h x)) = y \ g" by (erule subst) lemma ForallAorB_mksch [rule_format]: @@ -345,7 +345,7 @@ (* for replacing IH in conclusion *) apply (rotate_tac -2) (* 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) (* 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) @@ -391,7 +391,7 @@ (* for replacing IH in conclusion *) apply (rotate_tac -2) (* 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) (* 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) @@ -671,7 +671,7 @@ (* case x~:A & x~:B *) (* cannot occur because of assumption: Forall (a:ext A | a:ext B) *) apply (rotate_tac -9) -(* reduce forall assumption from tr to (x>>rs) *) +(* reduce forall assumption from tr to (x\rs) *) apply (simp add: externals_of_par) apply (fast intro!: ext_is_act) @@ -888,7 +888,7 @@ (* case x~:B & x~:A *) (* cannot occur because of assumption: Forall (a:ext A | a:ext B) *) apply (rotate_tac -9) -(* reduce forall assumption from tr to (x>>rs) *) +(* reduce forall assumption from tr to (x\rs) *) apply (simp add: externals_of_par) apply (fast intro!: ext_is_act) diff -r 8cba509ace9c -r 1f2788fb0b8b src/HOL/HOLCF/IOA/meta_theory/Deadlock.thy --- a/src/HOL/HOLCF/IOA/meta_theory/Deadlock.thy Wed Dec 30 21:52:00 2015 +0100 +++ b/src/HOL/HOLCF/IOA/meta_theory/Deadlock.thy Wed Dec 30 21:56:12 2015 +0100 @@ -12,7 +12,7 @@ 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 @@ a\nil : schedules A" apply (simp add: schedules_def has_schedule_def) apply auto apply (frule inp_is_act) @@ -39,7 +39,7 @@ apply (erule_tac x = "u" in allE) apply (erule exE) (* instantiate execution *) -apply (rule_tac x = " (s,ex @@ (a,s2) >>nil) " in exI) +apply (rule_tac x = " (s,ex @@ (a,s2) \nil) " in exI) apply (simp add: filter_act_def MapConc) apply (erule_tac t = "u" in lemma_2_1) apply simp @@ -56,8 +56,8 @@ declare split_if [split del] lemma IOA_deadlock_free: "[| a : local A; Finite sch; sch : schedules (A\B); - Filter (%x. x:act A)$(sch @@ a>>nil) : schedules A; compatible A B; input_enabled B |] - ==> (sch @@ a>>nil) : schedules (A\B)" + Filter (%x. x:act A)$(sch @@ a\nil) : schedules A; compatible A B; input_enabled B |] + ==> (sch @@ a\nil) : schedules (A\B)" apply (simp add: compositionality_sch locals_def) apply (rule conjI) (* a : act (A\B) *) diff -r 8cba509ace9c -r 1f2788fb0b8b src/HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy --- a/src/HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy Wed Dec 30 21:52:00 2015 +0100 +++ b/src/HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy Wed Dec 30 21:56:12 2015 +0100 @@ -87,7 +87,7 @@ apply simp done -lemma corresp_exC_cons: "(corresp_exC A f$(at>>xs)) s = +lemma corresp_exC_cons: "(corresp_exC A f$(at\xs)) s = (@cex. move A cex (f s) (fst at) (f (snd at))) @@ ((corresp_exC A f$xs) (snd at))" apply (rule trans) @@ -145,7 +145,7 @@ lemma move_subprop4: "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==> mk_trace A$((@x. move A x (f s) a (f t))) = - (if a:ext A then a>>nil else nil)" + (if a:ext A then a\nil else nil)" apply (cut_tac move_is_move) defer apply assumption+ diff -r 8cba509ace9c -r 1f2788fb0b8b src/HOL/HOLCF/IOA/meta_theory/RefMappings.thy --- a/src/HOL/HOLCF/IOA/meta_theory/RefMappings.thy Wed Dec 30 21:52:00 2015 +0100 +++ b/src/HOL/HOLCF/IOA/meta_theory/RefMappings.thy Wed Dec 30 21:56:12 2015 +0100 @@ -15,7 +15,7 @@ "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 @@ -40,7 +40,7 @@ lemma transition_is_ex: "s -a--A-> t ==> ? ex. move A ex s a t" -apply (rule_tac x = " (a,t) >>nil" in exI) +apply (rule_tac x = " (a,t) \nil" in exI) apply (simp add: move_def) done @@ -53,7 +53,7 @@ lemma ei_transitions_are_ex: "(s -a--A-> s') & (s' -a'--A-> s'') & (~a':ext A) ==> ? ex. move A ex s a s''" -apply (rule_tac x = " (a,s') >> (a',s'') >>nil" in exI) +apply (rule_tac x = " (a,s') \ (a',s'') \nil" in exI) apply (simp add: move_def) done @@ -61,7 +61,7 @@ lemma eii_transitions_are_ex: "(s1 -a1--A-> s2) & (s2 -a2--A-> s3) & (s3 -a3--A-> s4) & (~a2:ext A) & (~a3:ext A) ==> ? ex. move A ex s1 a1 s4" -apply (rule_tac x = " (a1,s2) >> (a2,s3) >> (a3,s4) >>nil" in exI) +apply (rule_tac x = " (a1,s2) \ (a2,s3) \ (a3,s4) \nil" in exI) apply (simp add: move_def) done diff -r 8cba509ace9c -r 1f2788fb0b8b src/HOL/HOLCF/IOA/meta_theory/Sequence.thy --- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Wed Dec 30 21:52:00 2015 +0100 +++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Wed Dec 30 21:56:12 2015 +0100 @@ -27,11 +27,8 @@ Filter2 ::"('a => bool) => 'a Seq -> 'a Seq" abbreviation - Consq_syn ("(_/>>_)" [66,65] 65) where - "a>>s == Consq a$s" - -notation (xsymbols) - Consq_syn ("(_\_)" [66,65] 65) + Consq_syn ("(_/\_)" [66,65] 65) where + "a\s == Consq a$s" (* list Enumeration *) @@ -39,10 +36,10 @@ "_totlist" :: "args => 'a Seq" ("[(_)!]") "_partlist" :: "args => 'a Seq" ("[(_)?]") translations - "[x, xs!]" == "x>>[xs!]" - "[x!]" == "x>>nil" - "[x, xs?]" == "x>>[xs?]" - "[x?]" == "x>>CONST bottom" + "[x, xs!]" == "x\[xs!]" + "[x!]" == "x\nil" + "[x, xs?]" == "x\[xs?]" + "[x?]" == "x\CONST bottom" defs @@ -92,7 +89,7 @@ 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) @@ -105,7 +102,7 @@ by (simp add: Filter_def) lemma Filter_cons: - "Filter P$(x>>xs)= (if P x then x>>(Filter P$xs) else Filter P$xs)" + "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) @@ -117,13 +114,13 @@ lemma Forall_nil: "Forall P nil" by (simp add: Forall_def sforall_def) -lemma Forall_cons: "Forall P (x>>xs)= (P x & Forall P xs)" +lemma Forall_cons: "Forall P (x\xs)= (P x & Forall P xs)" by (simp add: Forall_def sforall_def Consq_def flift2_def) subsubsection {* Conc *} -lemma Conc_cons: "(x>>xs) @@ y = x>>(xs @@y)" +lemma Conc_cons: "(x\xs) @@ y = x\(xs @@y)" by (simp add: Consq_def) @@ -136,7 +133,7 @@ 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) @@ -149,7 +146,7 @@ by (simp add: Dropwhile_def) lemma Dropwhile_cons: - "Dropwhile P$(x>>xs)= (if P x then Dropwhile P$xs else x>>xs)" + "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) @@ -161,7 +158,7 @@ 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)" apply (simp add: Last_def Consq_def) apply (cases xs) apply simp_all @@ -216,12 +213,12 @@ 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 @@ -252,11 +249,11 @@ section "Cons" -lemma Consq_def2: "a>>s = (Def a)##s" +lemma Consq_def2: "a\s = (Def a)##s" apply (simp add: Consq_def) done -lemma Seq_exhaust: "x = UU | x = nil | (? a s. x = a >> s)" +lemma Seq_exhaust: "x = UU | x = nil | (? a s. x = a \ s)" apply (simp add: Consq_def2) apply (cut_tac seq.nchotomy) apply (fast dest: not_Undef_is_Def [THEN iffD1]) @@ -264,7 +261,7 @@ lemma Seq_cases: -"!!P. [| x = UU ==> P; x = nil ==> P; !!a s. x = a >> s ==> P |] ==> P" +"!!P. [| x = UU ==> P; x = nil ==> P; !!a s. x = a \ s ==> P |] ==> P" apply (cut_tac x="x" in Seq_exhaust) apply (erule disjE) apply simp @@ -278,48 +275,48 @@ fun Seq_case_tac s i = rule_tac x",s)] Seq_cases i THEN hyp_subst_tac i THEN hyp_subst_tac (i+1) THEN hyp_subst_tac (i+2); *) -(* on a>>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *) +(* on a\s only simp_tac, as full_simp_tac is uncomplete and often causes errors *) (* fun Seq_case_simp_tac s i = Seq_case_tac s i THEN Asm_simp_tac (i+2) THEN Asm_full_simp_tac (i+1) THEN Asm_full_simp_tac i; *) -lemma Cons_not_UU: "a>>s ~= UU" +lemma Cons_not_UU: "a\s ~= UU" apply (subst Consq_def2) apply simp done -lemma Cons_not_less_UU: "~(a>>x) << UU" +lemma Cons_not_less_UU: "~(a\x) << UU" apply (rule notI) apply (drule below_antisym) apply simp apply (simp add: Cons_not_UU) done -lemma Cons_not_less_nil: "~a>>s << nil" +lemma Cons_not_less_nil: "~a\s << nil" apply (simp add: Consq_def2) done -lemma Cons_not_nil: "a>>s ~= nil" +lemma Cons_not_nil: "a\s ~= nil" apply (simp add: Consq_def2) done -lemma Cons_not_nil2: "nil ~= a>>s" +lemma Cons_not_nil2: "nil ~= a\s" apply (simp add: Consq_def2) done -lemma Cons_inject_eq: "(a>>s = b>>t) = (a = b & s = t)" +lemma Cons_inject_eq: "(a\s = b\t) = (a = b & s = t)" apply (simp only: Consq_def2) apply (simp add: scons_inject_eq) done -lemma Cons_inject_less_eq: "(a>>s<>t) = (a = b & s<s<t) = (a = b & s<>x) = a>> (seq_take n$x)" +lemma seq_take_Cons: "seq_take (Suc n)$(a\x) = a\ (seq_take n$x)" apply (simp add: Consq_def) done @@ -331,14 +328,14 @@ subsection "induction" lemma Seq_induct: -"!! P. [| adm P; P UU; P nil; !! a s. P s ==> P (a>>s)|] ==> P x" +"!! P. [| adm P; P UU; P nil; !! a s. P s ==> P (a\s)|] ==> P x" apply (erule (2) seq.induct) apply defined apply (simp add: Consq_def) done lemma Seq_FinitePartial_ind: -"!! P.[|P UU;P nil; !! a s. P s ==> P(a>>s) |] +"!! P.[|P UU;P nil; !! a s. P s ==> P(a\s) |] ==> seq_finite x --> P x" apply (erule (1) seq_finite_ind) apply defined @@ -346,7 +343,7 @@ done lemma Seq_Finite_ind: -"!! P.[| Finite x; P nil; !! a s. [| Finite s; P s|] ==> P (a>>s) |] ==> P x" +"!! P.[| Finite x; P nil; !! a s. [| Finite s; P s|] ==> P (a\s) |] ==> P x" apply (erule (1) Finite.induct) apply defined apply (simp add: Consq_def) @@ -379,11 +376,11 @@ subsection "HD,TL" -lemma HD_Cons [simp]: "HD$(x>>y) = Def x" +lemma HD_Cons [simp]: "HD$(x\y) = Def x" apply (simp add: Consq_def) done -lemma TL_Cons [simp]: "TL$(x>>y) = y" +lemma TL_Cons [simp]: "TL$(x\y) = y" apply (simp add: Consq_def) done @@ -391,7 +388,7 @@ subsection "Finite, Partial, Infinite" -lemma Finite_Cons [simp]: "Finite (a>>xs) = Finite xs" +lemma Finite_Cons [simp]: "Finite (a\xs) = Finite xs" apply (simp add: Consq_def2 Finite_cons) done @@ -792,7 +789,7 @@ lemma divide_Seq_lemma: "HD$(Filter P$y) = Def x - --> y = ((Takewhile (%x. ~P x)$y) @@ (x >> TL$(Dropwhile (%a. ~P a)$y))) + --> 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 @@ -808,11 +805,11 @@ apply simp done -lemma divide_Seq: "(x>>xs) << Filter P$y - ==> y = ((Takewhile (%a. ~ P a)$y) @@ (x >> TL$(Dropwhile (%a. ~ P a)$y))) +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 (drule_tac f="HD" and x="x\xs" in monofun_cfun_arg) apply simp done @@ -827,7 +824,7 @@ lemma divide_Seq2: "~Forall P y - ==> ? x. y= (Takewhile P$y @@ (x >> TL$(Dropwhile P$y))) & + ==> ? x. y= (Takewhile P$y @@ (x \ TL$(Dropwhile P$y))) & Finite (Takewhile P$y) & (~ P x)" apply (drule nForall_HDFilter [THEN mp]) apply safe @@ -838,7 +835,7 @@ lemma divide_Seq3: "~Forall P y - ==> ? x bs rs. y= (bs @@ (x>>rs)) & Finite bs & Forall P bs & (~ P x)" + ==> ? x bs rs. y= (bs @@ (x\rs)) & Finite bs & Forall P bs & (~ P x)" apply (drule divide_Seq2) (*Auto_tac no longer proves it*) apply fastforce @@ -860,7 +857,7 @@ 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)))" + --> 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) @@ -873,7 +870,7 @@ lemma take_reduction: "!! n.[| x=y; s=t; !! k. k seq_take k$y1 = seq_take k$y2|] - ==> seq_take n$(x @@ (s>>y1)) = seq_take n$(y @@ (t>>y2))" + ==> seq_take n$(x @@ (s\y1)) = seq_take n$(y @@ (t\y2))" apply (auto intro!: take_reduction1 [rule_format]) done @@ -883,7 +880,7 @@ 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)))" + --> 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) @@ -896,7 +893,7 @@ lemma take_reduction_less: "!! n.[| x=y; s=t;!! k. k seq_take k$y1 << seq_take k$y2|] - ==> seq_take n$(x @@ (s>>y1)) << seq_take n$(y @@ (t>>y2))" + ==> seq_take n$(x @@ (s\y1)) << seq_take n$(y @@ (t\y2))" apply (auto intro!: take_reduction_less1 [rule_format]) done @@ -925,8 +922,8 @@ lemma take_lemma_principle1: "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; - !! s1 s2 y. [| Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2)|] - ==> (f (s1 @@ y>>s2)) = (g (s1 @@ y>>s2)) |] + !! s1 s2 y. [| Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y\s2)|] + ==> (f (s1 @@ y\s2)) = (g (s1 @@ y\s2)) |] ==> A x --> (f x)=(g x)" apply (case_tac "Forall Q x") apply (auto dest!: divide_Seq3) @@ -934,9 +931,9 @@ lemma take_lemma_principle2: "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; - !! 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)) |] + !! 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)) |] ==> A x --> (f x)=(g x)" apply (case_tac "Forall Q x") apply (auto dest!: divide_Seq3) @@ -956,9 +953,9 @@ lemma take_lemma_induct: "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; !! s1 s2 y n. [| ! 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)) |] + 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)) |] ==> A x --> (f x)=(g x)" apply (rule impI) apply (rule seq.take_lemma) @@ -977,9 +974,9 @@ lemma take_lemma_less_induct: "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; !! s1 s2 y n. [| ! 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)) |] + 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)) |] ==> A x --> (f x)=(g x)" apply (rule impI) apply (rule seq.take_lemma) @@ -999,9 +996,9 @@ "!! Q. [| A UU ==> (f UU) = (g UU) ; A nil ==> (f nil) = (g nil) ; !! 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)) |] + A (y\s) |] + ==> seq_take (Suc n)$(f (y\s)) + = seq_take (Suc n)$(g (y\s)) |] ==> A x --> (f x)=(g x)" apply (rule impI) apply (rule seq.take_lemma) @@ -1084,7 +1081,7 @@ Rule_Insts.res_inst_tac ctxt [((("x", 0), Position.none), s)] [] @{thm Seq_cases} i THEN hyp_subst_tac ctxt i THEN hyp_subst_tac ctxt (i+1) THEN hyp_subst_tac ctxt (i+2); -(* on a>>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *) +(* on a\s only simp_tac, as full_simp_tac is uncomplete and often causes errors *) fun Seq_case_simp_tac ctxt s i = Seq_case_tac ctxt s i THEN asm_simp_tac ctxt (i+2) diff -r 8cba509ace9c -r 1f2788fb0b8b src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy --- a/src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy Wed Dec 30 21:52:00 2015 +0100 +++ b/src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy Wed Dec 30 21:56:12 2015 +0100 @@ -21,7 +21,7 @@ (case x of UU => UU | Def y => (Takewhile (%x. \P x)$s) - @@ (y>>(h$(TL$(Dropwhile (%x. \ P x)$s))$xs)) + @@ (y\(h$(TL$(Dropwhile (%x. \ P x)$s))$xs)) ) ))" @@ -65,7 +65,7 @@ (case x of UU => UU | Def y => (Takewhile (%a. \ P a)$s) - @@ (y>>(oraclebuild P$(TL$(Dropwhile (%a. \ P a)$s))$xs)) + @@ (y\(oraclebuild P$(TL$(Dropwhile (%a. \ P a)$s))$xs)) ) )" apply (rule trans) @@ -85,9 +85,9 @@ apply simp done -lemma oraclebuild_cons: "oraclebuild P$s$(x>>t) = +lemma oraclebuild_cons: "oraclebuild P$s$(x\t) = (Takewhile (%a. \ P a)$s) - @@ (x>>(oraclebuild P$(TL$(Dropwhile (%a. \ P a)$s))$t))" + @@ (x\(oraclebuild P$(TL$(Dropwhile (%a. \ P a)$s))$t))" apply (rule trans) apply (subst oraclebuild_unfold) apply (simp add: Consq_def) @@ -119,8 +119,8 @@ lemma Cut_Cons: "[| P t; Forall (%x. \ P x) ss; Finite ss|] - ==> Cut P (ss @@ (t>> rs)) - = ss @@ (t >> Cut P rs)" + ==> Cut P (ss @@ (t\ rs)) + = ss @@ (t \ Cut P rs)" apply (unfold Cut_def) apply (simp add: ForallQFilterPnil oraclebuild_cons TakewhileConc DropwhileConc) done diff -r 8cba509ace9c -r 1f2788fb0b8b src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy --- a/src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy Wed Dec 30 21:52:00 2015 +0100 +++ b/src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy Wed Dec 30 21:56:12 2015 +0100 @@ -56,7 +56,7 @@ apply simp done -lemma corresp_ex_simC_cons: "(corresp_ex_simC A R$((a,t)>>xs)) s = +lemma corresp_ex_simC_cons: "(corresp_ex_simC A R$((a,t)\xs)) s = (let T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t' in (@cex. move A cex s a T') @@ -138,7 +138,7 @@ "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==> let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in mk_trace A$((@x. move A x s' a T')) = - (if a:ext A then a>>nil else nil)" + (if a:ext A then a\nil else nil)" apply (cut_tac move_is_move_sim) defer apply assumption+ diff -r 8cba509ace9c -r 1f2788fb0b8b src/HOL/HOLCF/IOA/meta_theory/TL.thy --- a/src/HOL/HOLCF/IOA/meta_theory/TL.thy Wed Dec 30 21:52:00 2015 +0100 +++ b/src/HOL/HOLCF/IOA/meta_theory/TL.thy Wed Dec 30 21:56:12 2015 +0100 @@ -148,7 +148,7 @@ apply (unfold tsuffix_def suffix_def) apply auto apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *}) -apply (rule_tac x = "a>>s1" in exI) +apply (rule_tac x = "a\s1" in exI) apply auto done diff -r 8cba509ace9c -r 1f2788fb0b8b src/HOL/HOLCF/IOA/meta_theory/TLS.thy --- a/src/HOL/HOLCF/IOA/meta_theory/TLS.thy Wed Dec 30 21:52:00 2015 +0100 +++ b/src/HOL/HOLCF/IOA/meta_theory/TLS.thy Wed Dec 30 21:56:12 2015 +0100 @@ -65,9 +65,9 @@ ex2seqC_def: "ex2seqC == (fix$(LAM h ex. (%s. case ex of - nil => (s,None,s)>>nil + nil => (s,None,s)\nil | x##xs => (flift1 (%pr. - (s,Some (fst pr), snd pr)>> (h$xs) (snd pr)) + (s,Some (fst pr), snd pr)\ (h$xs) (snd pr)) $x) )))" @@ -87,7 +87,7 @@ "mkfin nil =nil" and mkfin_cons: - "(mkfin (a>>s)) = (a>>(mkfin s))" + "(mkfin (a\s)) = (a\(mkfin s))" lemmas [simp del] = HOL.ex_simps HOL.all_simps split_paired_Ex @@ -98,9 +98,9 @@ subsection {* ex2seqC *} lemma ex2seqC_unfold: "ex2seqC = (LAM ex. (%s. case ex of - nil => (s,None,s)>>nil + nil => (s,None,s)\nil | x##xs => (flift1 (%pr. - (s,Some (fst pr), snd pr)>> (ex2seqC$xs) (snd pr)) + (s,Some (fst pr), snd pr)\ (ex2seqC$xs) (snd pr)) $x) ))" apply (rule trans) @@ -115,13 +115,13 @@ apply simp done -lemma ex2seqC_nil: "(ex2seqC $nil) s = (s,None,s)>>nil" +lemma ex2seqC_nil: "(ex2seqC $nil) s = (s,None,s)\nil" apply (subst ex2seqC_unfold) apply simp done -lemma ex2seqC_cons: "(ex2seqC $((a,t)>>xs)) s = - (s,Some a,t)>> ((ex2seqC$xs) t)" +lemma ex2seqC_cons: "(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) @@ -134,15 +134,15 @@ declare mkfin_UU [simp] mkfin_nil [simp] mkfin_cons [simp] -lemma ex2seq_UU: "ex2seq (s, UU) = (s,None,s)>>nil" +lemma ex2seq_UU: "ex2seq (s, UU) = (s,None,s)\nil" apply (simp add: ex2seq_def) done -lemma ex2seq_nil: "ex2seq (s, nil) = (s,None,s)>>nil" +lemma ex2seq_nil: "ex2seq (s, nil) = (s,None,s)\nil" apply (simp add: ex2seq_def) done -lemma ex2seq_cons: "ex2seq (s, (a,t)>>ex) = (s,Some a,t) >> ex2seq (t, ex)" +lemma ex2seq_cons: "ex2seq (s, (a,t)\ex) = (s,Some a,t) \ ex2seq (t, ex)" apply (simp add: ex2seq_def) done diff -r 8cba509ace9c -r 1f2788fb0b8b src/HOL/HOLCF/IOA/meta_theory/Traces.thy --- a/src/HOL/HOLCF/IOA/meta_theory/Traces.thy Wed Dec 30 21:52:00 2015 +0100 +++ b/src/HOL/HOLCF/IOA/meta_theory/Traces.thy Wed Dec 30 21:56:12 2015 +0100 @@ -224,7 +224,7 @@ apply (simp add: filter_act_def) done -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" apply (simp add: filter_act_def) done @@ -243,9 +243,9 @@ apply (simp add: mk_trace_def) done -lemma mk_trace_cons: "mk_trace A$(at >> xs) = +lemma mk_trace_cons: "mk_trace A$(at \ xs) = (if ((fst at):ext A) - then (fst at) >> (mk_trace A$xs) + then (fst at) \ (mk_trace A$xs) else mk_trace A$xs)" apply (simp add: mk_trace_def) @@ -281,7 +281,7 @@ apply simp done -lemma is_exec_fragC_cons: "(is_exec_fragC A$(pr>>xs)) s = +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))" apply (rule trans) @@ -306,7 +306,7 @@ apply (simp add: is_exec_frag_def) done -lemma is_exec_frag_cons: "is_exec_frag A (s, (a,t)>>ex) = +lemma is_exec_frag_cons: "is_exec_frag A (s, (a,t)\ex) = (((s,a,t):trans_of A) & is_exec_frag A (t, ex))" apply (simp add: is_exec_frag_def) @@ -328,7 +328,7 @@ apply (simp add: laststate_def) done -lemma laststate_cons: "!! ex. Finite ex ==> laststate (s,at>>ex) = laststate (snd at,ex)" +lemma laststate_cons: "!! ex. Finite ex ==> laststate (s,at\ex) = laststate (snd at,ex)" apply (simp (no_asm) add: laststate_def) apply (case_tac "ex=nil") apply (simp (no_asm_simp))