--- 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)\<leadsto>ex) = (f s, (a,f t) \<leadsto> (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) \<leadsto>nil" in exI)
apply (simp add: move_def)
done
--- 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)\<leadsto>xs) = (a,fst t) \<leadsto> 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)\<leadsto>xs) = (a,snd t) \<leadsto> 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 \<leadsto> xs) =
(if (fst at:actions sig)
- then at >> (Filter_ex2 sig$xs)
+ then at \<leadsto> (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\<leadsto>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)\<leadsto>ex) =
((a~:actions sig --> (s=t)) & stutter sig (t,ex))"
apply (simp add: stutter_def)
done
--- 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))\<leadsto>
(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))\<leadsto>(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))\<leadsto>(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))\<leadsto>
(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))\<leadsto>(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))\<leadsto>(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\<leadsto>sch)$exA$exB) s t =
+ (x,snd a,t) \<leadsto> (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\<leadsto>sch)$exA$exB) s t =
+ (x,s,snd b) \<leadsto> (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\<leadsto>sch)$exA$exB) s t =
+ (x,snd a,snd b) \<leadsto>
(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\<leadsto>sch) (s,a\<leadsto>exA) (t,exB) =
+ ((s,t), (x,snd a,t) \<leadsto> 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\<leadsto>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\<leadsto>sch) (s,exA) (t,b\<leadsto>exB) =
+ ((s,t), (x,s,snd b) \<leadsto> 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\<leadsto>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\<leadsto>sch) (s,a\<leadsto>exA) (t,b\<leadsto>exB) =
+ ((s,t), (x,snd a,snd b) \<leadsto> 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\<leadsto>exB" and exA = "a\<leadsto>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<<f_act exA
- is used! --> to generate a contradiction using ~a>>ss<< UU(nil), using theorems
+ is used! --> to generate a contradiction using ~a\<leadsto>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\<leadsto>x, exB=b\<leadsto>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 *)
--- 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\<leadsto>(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\<leadsto>(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\<leadsto>(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\<leadsto>(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\<leadsto>(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\<leadsto>(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\<leadsto>tr)$schA$schB =
(Takewhile (%a. a:int A)$schA)
- @@ (x>>(mksch A B$tr$(TL$(Dropwhile (%a. a:int A)$schA))
+ @@ (x\<leadsto>(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\<leadsto>tr)$schA$schB =
(Takewhile (%a. a:int B)$schB)
- @@ (x>>(mksch A B$tr$schA$(TL$(Dropwhile (%a. a:int B)$schB))
+ @@ (x\<leadsto>(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\<leadsto>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\<leadsto>(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 \<leadsto> g; x=(h x) |] ==> (f (h x)) = y \<leadsto> 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\<leadsto>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\<leadsto>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\<leadsto>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\<leadsto>rs) *)
apply (simp add: externals_of_par)
apply (fast intro!: ext_is_act)
--- 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\<leadsto>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) \<leadsto>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\<parallel>B);
- Filter (%x. x:act A)$(sch @@ a>>nil) : schedules A; compatible A B; input_enabled B |]
- ==> (sch @@ a>>nil) : schedules (A\<parallel>B)"
+ Filter (%x. x:act A)$(sch @@ a\<leadsto>nil) : schedules A; compatible A B; input_enabled B |]
+ ==> (sch @@ a\<leadsto>nil) : schedules (A\<parallel>B)"
apply (simp add: compositionality_sch locals_def)
apply (rule conjI)
(* a : act (A\<parallel>B) *)
--- 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\<leadsto>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\<leadsto>nil else nil)"
apply (cut_tac move_is_move)
defer
apply assumption+
--- 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\<leadsto>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) \<leadsto>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') \<leadsto> (a',s'') \<leadsto>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) \<leadsto> (a2,s3) \<leadsto> (a3,s4) \<leadsto>nil" in exI)
apply (simp add: move_def)
done
--- 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 ("(_\<leadsto>_)" [66,65] 65)
+ Consq_syn ("(_/\<leadsto>_)" [66,65] 65) where
+ "a\<leadsto>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\<leadsto>[xs!]"
+ "[x!]" == "x\<leadsto>nil"
+ "[x, xs?]" == "x\<leadsto>[xs?]"
+ "[x?]" == "x\<leadsto>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\<leadsto>xs)=(f x) \<leadsto> 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\<leadsto>xs)= (if P x then x\<leadsto>(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\<leadsto>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\<leadsto>xs) @@ y = x\<leadsto>(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\<leadsto>xs)= (if P x then x\<leadsto>(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\<leadsto>xs)= (if P x then Dropwhile P$xs else x\<leadsto>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\<leadsto>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\<leadsto>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\<leadsto>xs)$(y\<leadsto>ys)= (x,y) \<leadsto> 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\<leadsto>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 \<leadsto> 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 \<leadsto> 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\<leadsto>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\<leadsto>s ~= UU"
apply (subst Consq_def2)
apply simp
done
-lemma Cons_not_less_UU: "~(a>>x) << UU"
+lemma Cons_not_less_UU: "~(a\<leadsto>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\<leadsto>s << nil"
apply (simp add: Consq_def2)
done
-lemma Cons_not_nil: "a>>s ~= nil"
+lemma Cons_not_nil: "a\<leadsto>s ~= nil"
apply (simp add: Consq_def2)
done
-lemma Cons_not_nil2: "nil ~= a>>s"
+lemma Cons_not_nil2: "nil ~= a\<leadsto>s"
apply (simp add: Consq_def2)
done
-lemma Cons_inject_eq: "(a>>s = b>>t) = (a = b & s = t)"
+lemma Cons_inject_eq: "(a\<leadsto>s = b\<leadsto>t) = (a = b & s = t)"
apply (simp only: Consq_def2)
apply (simp add: scons_inject_eq)
done
-lemma Cons_inject_less_eq: "(a>>s<<b>>t) = (a = b & s<<t)"
+lemma Cons_inject_less_eq: "(a\<leadsto>s<<b\<leadsto>t) = (a = b & s<<t)"
apply (simp add: Consq_def2)
done
-lemma seq_take_Cons: "seq_take (Suc n)$(a>>x) = a>> (seq_take n$x)"
+lemma seq_take_Cons: "seq_take (Suc n)$(a\<leadsto>x) = a\<leadsto> (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\<leadsto>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\<leadsto>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\<leadsto>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\<leadsto>y) = Def x"
apply (simp add: Consq_def)
done
-lemma TL_Cons [simp]: "TL$(x>>y) = y"
+lemma TL_Cons [simp]: "TL$(x\<leadsto>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\<leadsto>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 \<leadsto> 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\<leadsto>xs) << Filter P$y
+ ==> y = ((Takewhile (%a. ~ P a)$y) @@ (x \<leadsto> 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\<leadsto>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 \<leadsto> 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\<leadsto>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\<leadsto>y1)) = seq_take n$(x @@ (t\<leadsto>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<n ==> 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\<leadsto>y1)) = seq_take n$(y @@ (t\<leadsto>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\<leadsto>y1)) << seq_take n$(x @@ (t\<leadsto>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<n ==> 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\<leadsto>y1)) << seq_take n$(y @@ (t\<leadsto>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\<leadsto>s2)|]
+ ==> (f (s1 @@ y\<leadsto>s2)) = (g (s1 @@ y\<leadsto>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\<leadsto>s2)|]
+ ==> ! n. seq_take n$(f (s1 @@ y\<leadsto>s2))
+ = seq_take n$(g (s1 @@ y\<leadsto>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\<leadsto>s2) |]
+ ==> seq_take (Suc n)$(f (s1 @@ y\<leadsto>s2))
+ = seq_take (Suc n)$(g (s1 @@ y\<leadsto>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\<leadsto>s2) |]
+ ==> seq_take n$(f (s1 @@ y\<leadsto>s2))
+ = seq_take n$(g (s1 @@ y\<leadsto>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\<leadsto>s) |]
+ ==> seq_take (Suc n)$(f (y\<leadsto>s))
+ = seq_take (Suc n)$(g (y\<leadsto>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\<leadsto>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)
--- 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. \<not>P x)$s)
- @@ (y>>(h$(TL$(Dropwhile (%x. \<not> P x)$s))$xs))
+ @@ (y\<leadsto>(h$(TL$(Dropwhile (%x. \<not> P x)$s))$xs))
)
))"
@@ -65,7 +65,7 @@
(case x of
UU => UU
| Def y => (Takewhile (%a. \<not> P a)$s)
- @@ (y>>(oraclebuild P$(TL$(Dropwhile (%a. \<not> P a)$s))$xs))
+ @@ (y\<leadsto>(oraclebuild P$(TL$(Dropwhile (%a. \<not> 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\<leadsto>t) =
(Takewhile (%a. \<not> P a)$s)
- @@ (x>>(oraclebuild P$(TL$(Dropwhile (%a. \<not> P a)$s))$t))"
+ @@ (x\<leadsto>(oraclebuild P$(TL$(Dropwhile (%a. \<not> 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. \<not> P x) ss; Finite ss|]
- ==> Cut P (ss @@ (t>> rs))
- = ss @@ (t >> Cut P rs)"
+ ==> Cut P (ss @@ (t\<leadsto> rs))
+ = ss @@ (t \<leadsto> Cut P rs)"
apply (unfold Cut_def)
apply (simp add: ForallQFilterPnil oraclebuild_cons TakewhileConc DropwhileConc)
done
--- 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)\<leadsto>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\<leadsto>nil else nil)"
apply (cut_tac move_is_move_sim)
defer
apply assumption+
--- 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\<leadsto>s1" in exI)
apply auto
done
--- 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)\<leadsto>nil
| x##xs => (flift1 (%pr.
- (s,Some (fst pr), snd pr)>> (h$xs) (snd pr))
+ (s,Some (fst pr), snd pr)\<leadsto> (h$xs) (snd pr))
$x)
)))"
@@ -87,7 +87,7 @@
"mkfin nil =nil" and
mkfin_cons:
- "(mkfin (a>>s)) = (a>>(mkfin s))"
+ "(mkfin (a\<leadsto>s)) = (a\<leadsto>(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)\<leadsto>nil
| x##xs => (flift1 (%pr.
- (s,Some (fst pr), snd pr)>> (ex2seqC$xs) (snd pr))
+ (s,Some (fst pr), snd pr)\<leadsto> (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)\<leadsto>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)\<leadsto>xs)) s =
+ (s,Some a,t)\<leadsto> ((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)\<leadsto>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)\<leadsto>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)\<leadsto>ex) = (s,Some a,t) \<leadsto> ex2seq (t, ex)"
apply (simp add: ex2seq_def)
done
--- 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\<leadsto>xs) = (fst x) \<leadsto> 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 \<leadsto> xs) =
(if ((fst at):ext A)
- then (fst at) >> (mk_trace A$xs)
+ then (fst at) \<leadsto> (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\<leadsto>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)\<leadsto>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\<leadsto>ex) = laststate (snd at,ex)"
apply (simp (no_asm) add: laststate_def)
apply (case_tac "ex=nil")
apply (simp (no_asm_simp))