# HG changeset patch # User nipkow # Date 979050990 -3600 # Node ID f4745d77e620ce749abbb573b147de11ee0e0258 # Parent a7897aebbffc6ba75e5f9a688b7b6bdb0fa4da8e ` -> $ diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IMP/Denotational.ML --- a/src/HOLCF/IMP/Denotational.ML Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/IMP/Denotational.ML Tue Jan 09 15:36:30 2001 +0100 @@ -6,7 +6,7 @@ Equivalence of Denotational Semantics in HOLCF and Evaluation Semantics in HOL *) -Goalw [dlift_def] "dlift f`(Def x) = f`(Discr x)"; +Goalw [dlift_def] "dlift f$(Def x) = f$(Discr x)"; by (Simp_tac 1); qed "dlift_Def"; Addsimps [dlift_Def]; @@ -17,18 +17,18 @@ AddIffs [cont_dlift]; Goalw [dlift_def] - "(dlift f`l = Def y) = (? x. l = Def x & f`(Discr x) = Def y)"; + "(dlift f$l = Def y) = (? x. l = Def x & f$(Discr x) = Def y)"; by (simp_tac (simpset() addsplits [Lift1.lift.split]) 1); qed "dlift_is_Def"; Addsimps [dlift_is_Def]; -Goal " -c-> t ==> D c`(Discr s) = (Def t)"; +Goal " -c-> t ==> D c$(Discr s) = (Def t)"; by (etac evalc.induct 1); by (ALLGOALS Asm_simp_tac); by (ALLGOALS (stac fix_eq THEN' Asm_full_simp_tac)); qed_spec_mp "eval_implies_D"; -Goal "!s t. D c`(Discr s) = (Def t) --> -c-> t"; +Goal "!s t. D c$(Discr s) = (Def t) --> -c-> t"; by (induct_tac "c" 1); by (Force_tac 1); by (Force_tac 1); @@ -46,6 +46,6 @@ qed_spec_mp "D_implies_eval"; -Goal "(D c`(Discr s) = (Def t)) = ( -c-> t)"; +Goal "(D c$(Discr s) = (Def t)) = ( -c-> t)"; by (fast_tac (claset() addSEs [D_implies_eval,eval_implies_D]) 1); qed "D_is_eval"; diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IMP/Denotational.thy --- a/src/HOLCF/IMP/Denotational.thy Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/IMP/Denotational.thy Tue Jan 09 15:36:30 2001 +0100 @@ -10,7 +10,7 @@ constdefs dlift :: "(('a::term) discr -> 'b::pcpo) => ('a lift -> 'b)" - "dlift f == (LAM x. case x of Undef => UU | Def(y) => f`(Discr y))" + "dlift f == (LAM x. case x of Undef => UU | Def(y) => f$(Discr y))" consts D :: "com => state discr -> state lift" @@ -19,9 +19,9 @@ "D(X :== a) = (LAM s. Def((undiscr s)[X ::= a(undiscr s)]))" "D(c0 ; c1) = (dlift(D c1) oo (D c0))" "D(IF b THEN c1 ELSE c2) = - (LAM s. if b(undiscr s) then (D c1)`s else (D c2)`s)" + (LAM s. if b(undiscr s) then (D c1)$s else (D c2)$s)" "D(WHILE b DO c) = - fix`(LAM w s. if b(undiscr s) then (dlift w)`((D c)`s) + fix$(LAM w s. if b(undiscr s) then (dlift w)$((D c)$s) else Def(undiscr s))" end diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IMP/HoareEx.thy --- a/src/HOLCF/IMP/HoareEx.thy Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/IMP/HoareEx.thy Tue Jan 09 15:36:30 2001 +0100 @@ -13,6 +13,6 @@ types assn = state => bool constdefs hoare_valid :: [assn,com,assn] => bool ("|= {(1_)}/ (_)/ {(1_)}" 50) - "|= {A} c {B} == !s t. A s & D c `(Discr s) = Def t --> B t" + "|= {A} c {B} == !s t. A s & D c $(Discr s) = Def t --> B t" end diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/Abstraction.ML --- a/src/HOLCF/IOA/meta_theory/Abstraction.ML Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.ML Tue Jan 09 15:36:30 2001 +0100 @@ -181,7 +181,7 @@ that is to special Map Lemma *) Goalw [cex_abs_def,mk_trace_def,filter_act_def] "ext C = ext A \ -\ ==> mk_trace C`xs = mk_trace A`(snd (cex_abs f (s,xs)))"; +\ ==> mk_trace C$xs = mk_trace A$(snd (cex_abs f (s,xs)))"; by (Asm_full_simp_tac 1); by (pair_induct_tac "xs" [] 1); qed"traces_coincide_abs"; @@ -383,11 +383,11 @@ (* FIX: NAch Sequence.ML bringen *) -Goal "(Map f`s = nil) = (s=nil)"; +Goal "(Map f$s = nil) = (s=nil)"; by (Seq_case_simp_tac "s" 1); qed"Mapnil"; -Goal "(Map f`s = UU) = (s=UU)"; +Goal "(Map f$s = UU) = (s=UU)"; by (Seq_case_simp_tac "s" 1); qed"MapUU"; @@ -400,7 +400,7 @@ by Auto_tac; by (asm_full_simp_tac (simpset() addsimps [Mapnil])1); by (asm_full_simp_tac (simpset() addsimps [MapUU])1); -by (res_inst_tac [("x","Map (%(s,a,t). (h s,a, h t))`s1")] exI 1); +by (res_inst_tac [("x","Map (%(s,a,t). (h s,a, h t))$s1")] exI 1); by (asm_full_simp_tac (simpset() addsimps [Map2Finite,MapConc])1); qed"cex_absSeq_tsuffix"; @@ -433,7 +433,7 @@ (* ------------------ Next ----------------------------*) Goal -"(TL`(ex2seq (cex_abs h ex))=UU) = (TL`(ex2seq ex)=UU)"; +"(TL$(ex2seq (cex_abs h ex))=UU) = (TL$(ex2seq ex)=UU)"; by (pair_tac "ex" 1); by (Seq_case_simp_tac "y" 1); by (pair_tac "a" 1); @@ -442,7 +442,7 @@ qed"TL_ex2seq_UU"; Goal -"(TL`(ex2seq (cex_abs h ex))=nil) = (TL`(ex2seq ex)=nil)"; +"(TL$(ex2seq (cex_abs h ex))=nil) = (TL$(ex2seq ex)=nil)"; by (pair_tac "ex" 1); by (Seq_case_simp_tac "y" 1); by (pair_tac "a" 1); @@ -451,7 +451,7 @@ qed"TL_ex2seq_nil"; (* FIX: put to Sequence Lemmas *) -Goal "Map f`(TL`s) = TL`(Map f`s)"; +Goal "Map f$(TL$s) = TL$(Map f$s)"; by (Seq_induct_tac "s" [] 1); qed"MapTL"; @@ -459,13 +459,13 @@ properties carry over *) Goalw [cex_absSeq_def] -"cex_absSeq h (TL`s) = (TL`(cex_absSeq h s))"; +"cex_absSeq h (TL$s) = (TL$(cex_absSeq h s))"; by (simp_tac (simpset() addsimps [MapTL]) 1); qed"cex_absSeq_TL"; (* important property of ex2seq: can be shiftet, as defined "pointwise" *) -Goal "[| (snd ex)~=UU ; (snd ex)~=nil |] ==> (? ex'. TL`(ex2seq ex) = ex2seq ex')"; +Goal "[| (snd ex)~=UU ; (snd ex)~=nil |] ==> (? ex'. TL$(ex2seq ex) = ex2seq ex')"; by (pair_tac "ex" 1); by (Seq_case_simp_tac "y" 1); by (pair_tac "a" 1); @@ -473,7 +473,7 @@ qed"TLex2seq"; -Goal "(TL`(ex2seq ex)~=nil) = ((snd ex)~=nil & (snd ex)~=UU)"; +Goal "(TL$(ex2seq ex)~=nil) = ((snd ex)~=nil & (snd ex)~=UU)"; by (pair_tac "ex" 1); by (Seq_case_simp_tac "y" 1); by (pair_tac "a" 1); diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/Abstraction.thy --- a/src/HOLCF/IOA/meta_theory/Abstraction.thy Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy Tue Jan 09 15:36:30 2001 +0100 @@ -43,11 +43,11 @@ temp_weakening (snd AM) (snd CL) h" cex_abs_def - "cex_abs f ex == (f (fst ex), Map (%(a,t). (a,f t))`(snd ex))" + "cex_abs f ex == (f (fst ex), Map (%(a,t). (a,f t))$(snd ex))" (* equals cex_abs on Sequneces -- after ex2seq application -- *) cex_absSeq_def - "cex_absSeq f == % s. Map (%(s,a,t). (f s,a,f t))`s" + "cex_absSeq f == % s. Map (%(s,a,t). (f s,a,f t))$s" weakeningIOA_def "weakeningIOA A C h == ! ex. ex : executions C --> cex_abs h ex : executions A" diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/CompoExecs.ML --- a/src/HOLCF/IOA/meta_theory/CompoExecs.ML Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/IOA/meta_theory/CompoExecs.ML Tue Jan 09 15:36:30 2001 +0100 @@ -20,15 +20,15 @@ (* ---------------------------------------------------------------- *) -Goal "ProjA2`UU = UU"; +Goal "ProjA2$UU = UU"; by (simp_tac (simpset() addsimps [ProjA2_def]) 1); qed"ProjA2_UU"; -Goal "ProjA2`nil = nil"; +Goal "ProjA2$nil = nil"; by (simp_tac (simpset() addsimps [ProjA2_def]) 1); qed"ProjA2_nil"; -Goal "ProjA2`((a,t)>>xs) = (a,fst t) >> ProjA2`xs"; +Goal "ProjA2$((a,t)>>xs) = (a,fst t) >> ProjA2$xs"; by (simp_tac (simpset() addsimps [ProjA2_def]) 1); qed"ProjA2_cons"; @@ -38,15 +38,15 @@ (* ---------------------------------------------------------------- *) -Goal "ProjB2`UU = UU"; +Goal "ProjB2$UU = UU"; by (simp_tac (simpset() addsimps [ProjB2_def]) 1); qed"ProjB2_UU"; -Goal "ProjB2`nil = nil"; +Goal "ProjB2$nil = nil"; by (simp_tac (simpset() addsimps [ProjB2_def]) 1); qed"ProjB2_nil"; -Goal "ProjB2`((a,t)>>xs) = (a,snd t) >> ProjB2`xs"; +Goal "ProjB2$((a,t)>>xs) = (a,snd t) >> ProjB2$xs"; by (simp_tac (simpset() addsimps [ProjB2_def]) 1); qed"ProjB2_cons"; @@ -57,18 +57,18 @@ (* ---------------------------------------------------------------- *) -Goal "Filter_ex2 sig`UU=UU"; +Goal "Filter_ex2 sig$UU=UU"; by (simp_tac (simpset() addsimps [Filter_ex2_def]) 1); qed"Filter_ex2_UU"; -Goal "Filter_ex2 sig`nil=nil"; +Goal "Filter_ex2 sig$nil=nil"; by (simp_tac (simpset() addsimps [Filter_ex2_def]) 1); qed"Filter_ex2_nil"; -Goal "Filter_ex2 sig`(at >> xs) = \ +Goal "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 (asm_full_simp_tac (simpset() addsimps [Filter_ex2_def]) 1); qed"Filter_ex2_cons"; @@ -85,8 +85,8 @@ \ (%p.(If Def ((fst p)~:actions sig) \ \ then Def (s=(snd p)) \ \ else TT fi) \ -\ andalso (stutter2 sig`xs) (snd p)) \ -\ `x) \ +\ andalso (stutter2 sig$xs) (snd p)) \ +\ $x) \ \ ))"; by (rtac trans 1); by (rtac fix_eq2 1); @@ -95,19 +95,19 @@ by (simp_tac (simpset() addsimps [flift1_def]) 1); qed"stutter2_unfold"; -Goal "(stutter2 sig`UU) s=UU"; +Goal "(stutter2 sig$UU) s=UU"; by (stac stutter2_unfold 1); by (Simp_tac 1); qed"stutter2_UU"; -Goal "(stutter2 sig`nil) s = TT"; +Goal "(stutter2 sig$nil) s = TT"; by (stac stutter2_unfold 1); by (Simp_tac 1); qed"stutter2_nil"; -Goal "(stutter2 sig`(at>>xs)) s = \ +Goal "(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))"; by (rtac trans 1); by (stac stutter2_unfold 1); by (asm_full_simp_tac (simpset() addsimps [Consq_def,flift1_def,If_and_if]) 1); @@ -159,8 +159,8 @@ (* --------------------------------------------------------------------- *) Goal "!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))"; by (pair_induct_tac "xs" [is_exec_frag_def] 1); (* main case *) @@ -175,8 +175,8 @@ (* --------------------------------------------------------------------- *) Goal "!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)"; by (pair_induct_tac "xs" [stutter_def,is_exec_frag_def] 1); (* main case *) @@ -205,10 +205,10 @@ (* ----------------------------------------------------------------------- *) Goal -"!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)) & \ +"!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)) & \ \ Forall (%x. fst x:act (A||B)) xs \ \ --> is_exec_frag (A||B) (s,xs)"; diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/CompoExecs.thy --- a/src/HOLCF/IOA/meta_theory/CompoExecs.thy Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/IOA/meta_theory/CompoExecs.thy Tue Jan 09 15:36:30 2001 +0100 @@ -27,10 +27,10 @@ ProjA_def - "ProjA ex == (fst (fst ex), ProjA2`(snd ex))" + "ProjA ex == (fst (fst ex), ProjA2$(snd ex))" ProjB_def - "ProjB ex == (snd (fst ex), ProjB2`(snd ex))" + "ProjB ex == (snd (fst ex), ProjB2$(snd ex))" ProjA2_def @@ -41,24 +41,24 @@ Filter_ex_def - "Filter_ex sig ex == (fst ex,Filter_ex2 sig`(snd ex))" + "Filter_ex sig ex == (fst ex,Filter_ex2 sig$(snd ex))" Filter_ex2_def "Filter_ex2 sig == Filter (%x. fst x:actions sig)" stutter_def - "stutter sig ex == ((stutter2 sig`(snd ex)) (fst ex) ~= FF)" + "stutter sig ex == ((stutter2 sig$(snd ex)) (fst ex) ~= FF)" stutter2_def - "stutter2 sig ==(fix`(LAM h ex. (%s. case ex of + "stutter2 sig ==(fix$(LAM h ex. (%s. case ex of nil => TT | x##xs => (flift1 (%p.(If Def ((fst p)~:actions sig) then Def (s=(snd p)) else TT fi) - andalso (h`xs) (snd p)) - `x) + andalso (h$xs) (snd p)) + $x) )))" par_execs_def diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/CompoScheds.ML --- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML Tue Jan 09 15:36:30 2001 +0100 @@ -30,25 +30,25 @@ \ | Def y => \ \ (if y:act A then \ \ (if y:act B then \ -\ (case HD`exA of \ +\ (case HD$exA of \ \ Undef => UU \ -\ | Def a => (case HD`exB of \ +\ | Def a => (case HD$exB of \ \ Undef => 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 \ \ Undef => 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 \ +\ (case HD$exB of \ \ Undef => 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 \ \ ) \ @@ -56,38 +56,38 @@ \ )))"); -Goal "(mkex2 A B`UU`exA`exB) s t = UU"; +Goal "(mkex2 A B$UU$exA$exB) s t = UU"; by (stac mkex2_unfold 1); by (Simp_tac 1); qed"mkex2_UU"; -Goal "(mkex2 A B`nil`exA`exB) s t= nil"; +Goal "(mkex2 A B$nil$exA$exB) s t= nil"; by (stac mkex2_unfold 1); by (Simp_tac 1); qed"mkex2_nil"; -Goal "[| 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"; +Goal "[| 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"; by (rtac trans 1); by (stac mkex2_unfold 1); by (asm_full_simp_tac (simpset() addsimps [Consq_def,If_and_if]) 1); by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1); qed"mkex2_cons_1"; -Goal "[| 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)"; +Goal "[| 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)"; by (rtac trans 1); by (stac mkex2_unfold 1); by (asm_full_simp_tac (simpset() addsimps [Consq_def,If_and_if]) 1); by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1); qed"mkex2_cons_2"; -Goal "[| x:act A; x:act B; HD`exA=Def a;HD`exB=Def b|] \ -\ ==> (mkex2 A B`(x>>sch)`exA`exB) s t = \ +Goal "[| 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)"; +\ (mkex2 A B$sch$(TL$exA)$(TL$exB)) (snd a) (snd b)"; by (rtac trans 1); by (stac mkex2_unfold 1); by (asm_full_simp_tac (simpset() addsimps [Consq_def,If_and_if]) 1); @@ -156,8 +156,8 @@ (* --------------------------------------------------------------------- *) Goalw [filter_act_def,Filter_ex2_def] - "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)"; by (simp_tac (simpset() addsimps [MapFilter,o_def]) 1); qed"lemma_2_1a"; @@ -168,8 +168,8 @@ (* --------------------------------------------------------------------- *) Goal - "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_tac "xs" [] 1); qed"lemma_2_1b"; @@ -184,7 +184,7 @@ is the same proposition, but we cannot change this one, when then rather lemma_1_1c *) Goal "!s. is_exec_frag (A||B) (s,xs) \ -\ --> Forall (%x. x:act (A||B)) (filter_act`xs)"; +\ --> Forall (%x. x:act (A||B)) (filter_act$xs)"; by (pair_induct_tac "xs" [is_exec_frag_def,Forall_def,sforall_def] 1); (* main case *) @@ -205,9 +205,9 @@ Goal "! 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"; by (Seq_induct_tac "sch" [Filter_def,Forall_def,sforall_def,mkex_def] 1); @@ -268,9 +268,9 @@ Goal "! 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_tac "sch" "exA" "exB"); @@ -279,8 +279,8 @@ Goal "[| \ \ 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))"; by (cut_facts_tac [stutterA_mkex] 1); @@ -299,9 +299,9 @@ Goal "! 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_tac "sch" "exA" "exB"); @@ -310,8 +310,8 @@ Goal "[| \ \ 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))"; by (cut_facts_tac [stutterB_mkex] 1); @@ -325,40 +325,40 @@ (*--------------------------------------------------------------------------- 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 --------------------------------------------------------------------------- *) Goal "! 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_tac "sch" "exB" "exA"); qed"filter_mkex_is_exA_tmp"; (*--------------------------------------------------------------------------- - zip`(proj1`y)`(proj2`y) = y (using the lift operations) + zip$(proj1$y)$(proj2$y) = y (using the lift operations) lemma for admissibility problems --------------------------------------------------------------------------- *) -Goal "Zip`(Map fst`y)`(Map snd`y) = y"; +Goal "Zip$(Map fst$y)$(Map snd$y) = y"; by (Seq_induct_tac "y" [] 1); qed"Zip_Map_fst_snd"; (*--------------------------------------------------------------------------- - 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 --------------------------------------------------------------------------- *) Goal "!! sch ex. \ -\ 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)"; by (asm_full_simp_tac (simpset() addsimps [filter_act_def]) 1); by (rtac (Zip_Map_fst_snd RS sym) 1); qed"trick_against_eq_in_ass"; @@ -371,8 +371,8 @@ Goal "!!sch exA 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 A) (ProjA (mkex A B sch exA exB)) = exA"; by (asm_full_simp_tac (simpset() addsimps [ProjA_def,Filter_ex_def]) 1); by (pair_tac "exA" 1); @@ -388,7 +388,7 @@ (*--------------------------------------------------------------------------- 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 --------------------------------------------------------------------------- *) @@ -396,10 +396,10 @@ Goal "! 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_tac "sch" "exA" "exB"); @@ -415,8 +415,8 @@ Goal "!!sch exA 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"; by (asm_full_simp_tac (simpset() addsimps [ProjB_def,Filter_ex_def]) 1); by (pair_tac "exA" 1); @@ -436,8 +436,8 @@ Goal "!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)))"; @@ -453,8 +453,8 @@ Goal "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)"; by (simp_tac (simpset() addsimps [schedules_def, has_schedule_def]) 1); diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/CompoScheds.thy --- a/src/HOLCF/IOA/meta_theory/CompoScheds.thy Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy Tue Jan 09 15:36:30 2001 +0100 @@ -26,10 +26,10 @@ mkex_def "mkex A B sch exA exB == ((fst exA,fst exB), - (mkex2 A B`sch`(snd exA)`(snd exB)) (fst exA) (fst exB))" + (mkex2 A B$sch$(snd exA)$(snd exB)) (fst exA) (fst exB))" mkex2_def - "mkex2 A B == (fix`(LAM h sch exA exB. (%s t. case sch of + "mkex2 A B == (fix$(LAM h sch exA exB. (%s t. case sch of nil => nil | x##xs => (case x of @@ -37,25 +37,25 @@ | Def y => (if y:act A then (if y:act B then - (case HD`exA of + (case HD$exA of Undef => UU - | Def a => (case HD`exB of + | Def a => (case HD$exB of Undef => 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 Undef => 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 + (case HD$exB of Undef => 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 ) @@ -67,8 +67,8 @@ let schA = fst SchedsA; sigA = snd SchedsA; schB = fst SchedsB; sigB = snd SchedsB in - ( {sch. Filter (%a. a:actions sigA)`sch : schA} - Int {sch. Filter (%a. a:actions sigB)`sch : schB} + ( {sch. Filter (%a. a:actions sigA)$sch : schA} + Int {sch. Filter (%a. a:actions sigB)$sch : schB} Int {sch. Forall (%x. x:(actions sigA Un actions sigB)) sch}, asig_comp sigA sigB)" diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/CompoTraces.ML --- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML Tue Jan 09 15:36:30 2001 +0100 @@ -24,24 +24,24 @@ \ | 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 \ @@ -50,21 +50,21 @@ \ ))"); -Goal "mksch A B`UU`schA`schB = UU"; +Goal "mksch A B$UU$schA$schB = UU"; by (stac mksch_unfold 1); by (Simp_tac 1); qed"mksch_UU"; -Goal "mksch A B`nil`schA`schB = nil"; +Goal "mksch A B$nil$schA$schB = nil"; by (stac mksch_unfold 1); by (Simp_tac 1); qed"mksch_nil"; Goal "[|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))"; by (rtac trans 1); by (stac mksch_unfold 1); by (asm_full_simp_tac (simpset() addsimps [Consq_def,If_and_if]) 1); @@ -72,9 +72,9 @@ qed"mksch_cons1"; Goal "[|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)) \ \ ))"; by (rtac trans 1); by (stac mksch_unfold 1); @@ -83,11 +83,11 @@ qed"mksch_cons2"; Goal "[|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)))) \ \ )"; by (rtac trans 1); by (stac mksch_unfold 1); @@ -148,7 +148,7 @@ Goal "!!A B. 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)"; by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1); by (safe_tac set_cs); by (asm_full_simp_tac (simpset() addsimps [actions_of_par]) 1); @@ -175,7 +175,7 @@ Goal "!!A B. 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))"; by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1); by (safe_tac set_cs); @@ -186,7 +186,7 @@ Goal "!!A B. 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))"; by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1); by (safe_tac set_cs); @@ -201,10 +201,10 @@ Goal "[| 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 &\ +\ 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)"; +\ --> Finite (mksch A B$tr$x$y)"; by (etac Seq_Finite_ind 1); by (Asm_full_simp_tac 1); @@ -222,10 +222,10 @@ [not_ext_is_int_or_not_act,FiniteConc]) 1); (* now for conclusion IH applicable, but assumptions have to be transformed *) by (dres_inst_tac [("x","x"), - ("g","Filter (%a. a:act A)`s")] subst_lemma2 1); + ("g","Filter (%a. a:act A)$s")] subst_lemma2 1); by (assume_tac 1); by (dres_inst_tac [("x","y"), - ("g","Filter (%a. a:act B)`s")] subst_lemma2 1); + ("g","Filter (%a. a:act B)$s")] subst_lemma2 1); by (assume_tac 1); (* IH *) by (asm_full_simp_tac (simpset() @@ -240,7 +240,7 @@ [not_ext_is_int_or_not_act,FiniteConc]) 1); (* now for conclusion IH applicable, but assumptions have to be transformed *) by (dres_inst_tac [("x","y"), - ("g","Filter (%a. a:act B)`s")] subst_lemma2 1); + ("g","Filter (%a. a:act B)$s")] subst_lemma2 1); by (assume_tac 1); (* IH *) by (asm_full_simp_tac (simpset() @@ -255,7 +255,7 @@ [not_ext_is_int_or_not_act,FiniteConc]) 1); (* now for conclusion IH applicable, but assumptions have to be transformed *) by (dres_inst_tac [("x","x"), - ("g","Filter (%a. a:act A)`s")] subst_lemma2 1); + ("g","Filter (%a. a:act A)$s")] subst_lemma2 1); by (assume_tac 1); (* IH *) by (asm_full_simp_tac (simpset() @@ -274,11 +274,11 @@ Goal " [| 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) \ -\ --> (? y1 y2. (mksch A B`(bs @@ z)`x`y) = (y1 @@ (mksch A B`z`x`y2)) & \ +\ 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)) & \ \ 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)"; by (forw_inst_tac [("A1","A")] (compat_commute RS iffD1) 1); by (etac Seq_Finite_ind 1); by (REPEAT (rtac allI 1)); @@ -297,12 +297,12 @@ by (REPEAT (etac conjE 1)); (* transform assumption f eB y = f B (s@z) *) by (dres_inst_tac [("x","y"), - ("g","Filter (%a. a:act B)`(s@@z)")] subst_lemma2 1); + ("g","Filter (%a. a:act B)$(s@@z)")] subst_lemma2 1); by (assume_tac 1); Addsimps [FilterConc]; by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act]) 1); (* apply IH *) -by (eres_inst_tac [("x","TL`(Dropwhile (%a. a:int B)`y)")] allE 1); +by (eres_inst_tac [("x","TL$(Dropwhile (%a. a:int B)$y)")] allE 1); by (asm_full_simp_tac (simpset() addsimps [ForallTL,ForallDropwhile])1); by (REPEAT (etac exE 1)); by (REPEAT (etac conjE 1)); @@ -311,7 +311,7 @@ by (rotate_tac ~2 1); by (Asm_full_simp_tac 1); (* instantiate y1a and y2a *) -by (res_inst_tac [("x","Takewhile (%a. a:int B)`y @@ a>>y1")] exI 1); +by (res_inst_tac [("x","Takewhile (%a. a:int B)$y @@ a>>y1")] exI 1); by (res_inst_tac [("x","y2")] exI 1); (* elminate all obligations up to two depending on Conc_assoc *) by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ, intA_is_not_actB, @@ -328,11 +328,11 @@ Goal " [| Finite as; 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) as &\ -\ Filter (%a. a:ext A)`x = Filter (%a. a:act A)`(as @@ z) \ -\ --> (? x1 x2. (mksch A B`(as @@ z)`x`y) = (x1 @@ (mksch A B`z`x2`y)) & \ +\ Filter (%a. a:ext A)$x = Filter (%a. a:act A)$(as @@ z) \ +\ --> (? x1 x2. (mksch A B$(as @@ 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 = as)"; +\ Filter (%a. a:ext A)$x1 = as)"; by (forw_inst_tac [("A1","A")] (compat_commute RS iffD1) 1); by (etac Seq_Finite_ind 1); by (REPEAT (rtac allI 1)); @@ -351,12 +351,12 @@ by (REPEAT (etac conjE 1)); (* transform assumption f eA x = f A (s@z) *) by (dres_inst_tac [("x","x"), - ("g","Filter (%a. a:act A)`(s@@z)")] subst_lemma2 1); + ("g","Filter (%a. a:act A)$(s@@z)")] subst_lemma2 1); by (assume_tac 1); Addsimps [FilterConc]; by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act]) 1); (* apply IH *) -by (eres_inst_tac [("x","TL`(Dropwhile (%a. a:int A)`x)")] allE 1); +by (eres_inst_tac [("x","TL$(Dropwhile (%a. a:int A)$x)")] allE 1); by (asm_full_simp_tac (simpset() addsimps [ForallTL,ForallDropwhile])1); by (REPEAT (etac exE 1)); by (REPEAT (etac conjE 1)); @@ -365,7 +365,7 @@ by (rotate_tac ~2 1); by (Asm_full_simp_tac 1); (* instantiate y1a and y2a *) -by (res_inst_tac [("x","Takewhile (%a. a:int A)`x @@ a>>x1")] exI 1); +by (res_inst_tac [("x","Takewhile (%a. a:int A)$x @@ a>>x1")] exI 1); by (res_inst_tac [("x","x2")] exI 1); (* elminate all obligations up to two depending on Conc_assoc *) by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ, intA_is_not_actB, @@ -380,7 +380,7 @@ Goal "Finite y ==> ! z tr. Forall (%a.a:ext (A||B)) tr & \ -\ y = z @@ mksch A B`tr`a`b\ +\ y = z @@ mksch A B$tr$a$b\ \ --> Finite tr"; by (etac Seq_Finite_ind 1); by Auto_tac; @@ -422,7 +422,7 @@ by (rotate_tac ~2 2); by (rotate_tac ~2 3); by (asm_full_simp_tac (HOL_basic_ss addsimps [mksch_cons3]) 2); -by (eres_inst_tac [("x","sb@@Takewhile (%a. a: int A)`a @@ Takewhile (%a. a:int B)`b@@(aaa>>nil)")] allE 2); +by (eres_inst_tac [("x","sb@@Takewhile (%a. a: int A)$a @@ Takewhile (%a. a:int B)$b@@(aaa>>nil)")] allE 2); by (eres_inst_tac [("x","sa")] allE 2); by (asm_full_simp_tac (simpset() addsimps [Conc_assoc])2); @@ -455,7 +455,7 @@ qed"FiniteConcUU"; finiteR_mksch - "Finite (mksch A B`tr`x`y) --> Finite tr" + "Finite (mksch A B$tr$x$y) --> Finite tr" *) @@ -470,9 +470,9 @@ \ is_asig(asig_of A); is_asig(asig_of B) |] ==> \ \ ! schA schB. 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"; by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1); @@ -546,10 +546,10 @@ \ is_asig(asig_of A); is_asig(asig_of B) |] ==> \ \ 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"; by (res_inst_tac [("Q","%x. x:act B & x~:act A"),("x","tr")] take_lemma_less_induct 1); by (REPEAT (etac conjE 1)); @@ -600,7 +600,7 @@ (* eliminate the B-only prefix *) -by (subgoal_tac "(Filter (%a. a :act A)`y1) = nil" 1); +by (subgoal_tac "(Filter (%a. a :act A)$y1) = nil" 1); by (etac ForallQFilterPnil 2); by (assume_tac 2); by (Fast_tac 2); @@ -613,7 +613,7 @@ by (rotate_tac ~2 1); by (Asm_full_simp_tac 1); -by (subgoal_tac "Filter (%a. a:act A & a:ext B)`y1=nil" 1); +by (subgoal_tac "Filter (%a. a:act A & a:ext B)$y1=nil" 1); by (rotate_tac ~1 1); by (Asm_full_simp_tac 1); (* eliminate introduced subgoal 2 *) @@ -651,7 +651,7 @@ by (asm_full_simp_tac (simpset() addsimps [ext_and_act]) 1); (* assumption schA *) by (dres_inst_tac [("x","schA"), - ("g","Filter (%a. a:act A)`s2")] subst_lemma2 1); + ("g","Filter (%a. a:act A)$s2")] subst_lemma2 1); by (assume_tac 1); by (Asm_full_simp_tac 1); (* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *) @@ -680,10 +680,10 @@ \ is_asig(asig_of A); is_asig(asig_of B) |] ==> \ \ 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"; by (strip_tac 1); by (resolve_tac seq.take_lemmas 1); @@ -756,7 +756,7 @@ (* eliminate the B-only prefix *) -by (subgoal_tac "(Filter (%a. a :act A)`y1) = nil" 1); +by (subgoal_tac "(Filter (%a. a :act A)$y1) = nil" 1); by (etac ForallQFilterPnil 2); by (assume_tac 2); by (Fast_tac 2); @@ -769,7 +769,7 @@ by (rotate_tac ~2 1); by (Asm_full_simp_tac 1); -by (subgoal_tac "Filter (%a. a:act A & a:ext B)`y1=nil" 1); +by (subgoal_tac "Filter (%a. a:act A & a:ext B)$y1=nil" 1); by (rotate_tac ~1 1); by (Asm_full_simp_tac 1); (* eliminate introduced subgoal 2 *) @@ -808,7 +808,7 @@ by (REPEAT (etac conjE 1)); (* assumption schA *) by (dres_inst_tac [("x","schA"), - ("g","Filter (%a. a:act A)`rs")] subst_lemma2 1); + ("g","Filter (%a. a:act A)$rs")] subst_lemma2 1); by (assume_tac 1); by (asm_full_simp_tac (simpset() addsimps [int_is_not_ext]) 1); (* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *) @@ -828,7 +828,7 @@ by (rotate_tac ~2 1); by (Asm_full_simp_tac 1); -by (subgoal_tac "Filter (%a. a:act A & a:ext B)`y1=nil" 1); +by (subgoal_tac "Filter (%a. a:act A & a:ext B)$y1=nil" 1); by (rotate_tac ~1 1); by (Asm_full_simp_tac 1); (* eliminate introduced subgoal 2 *) @@ -860,7 +860,7 @@ by (REPEAT (etac conjE 1)); (* assumption schA *) by (dres_inst_tac [("x","schA"), - ("g","Filter (%a. a:act A)`rs")] subst_lemma2 1); + ("g","Filter (%a. a:act A)$rs")] subst_lemma2 1); by (assume_tac 1); by (asm_full_simp_tac (simpset() addsimps [int_is_not_ext]) 1); @@ -878,7 +878,7 @@ (* assumption schB *) by (dres_inst_tac [("x","y2"), - ("g","Filter (%a. a:act B)`rs")] subst_lemma2 1); + ("g","Filter (%a. a:act B)$rs")] subst_lemma2 1); by (assume_tac 1); by (asm_full_simp_tac (simpset() addsimps [intA_is_not_actB,int_is_not_ext]) 1); @@ -920,10 +920,10 @@ \ is_asig(asig_of A); is_asig(asig_of B) |] ==> \ \ 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"; by (strip_tac 1); by (resolve_tac seq.take_lemmas 1); @@ -998,7 +998,7 @@ (* eliminate the A-only prefix *) -by (subgoal_tac "(Filter (%a. a :act B)`x1) = nil" 1); +by (subgoal_tac "(Filter (%a. a :act B)$x1) = nil" 1); by (etac ForallQFilterPnil 2); by (assume_tac 2); by (Fast_tac 2); @@ -1011,7 +1011,7 @@ by (rotate_tac ~2 1); by (Asm_full_simp_tac 1); -by (subgoal_tac "Filter (%a. a:act B & a:ext A)`x1=nil" 1); +by (subgoal_tac "Filter (%a. a:act B & a:ext A)$x1=nil" 1); by (rotate_tac ~1 1); by (Asm_full_simp_tac 1); (* eliminate introduced subgoal 2 *) @@ -1050,7 +1050,7 @@ by (REPEAT (etac conjE 1)); (* assumption schB *) by (dres_inst_tac [("x","schB"), - ("g","Filter (%a. a:act B)`rs")] subst_lemma2 1); + ("g","Filter (%a. a:act B)$rs")] subst_lemma2 1); by (assume_tac 1); by (asm_full_simp_tac (simpset() addsimps [int_is_not_ext]) 1); (* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *) @@ -1070,7 +1070,7 @@ by (rotate_tac ~2 1); by (Asm_full_simp_tac 1); -by (subgoal_tac "Filter (%a. a:act B & a:ext A)`x1=nil" 1); +by (subgoal_tac "Filter (%a. a:act B & a:ext A)$x1=nil" 1); by (rotate_tac ~1 1); by (Asm_full_simp_tac 1); (* eliminate introduced subgoal 2 *) @@ -1102,7 +1102,7 @@ by (REPEAT (etac conjE 1)); (* assumption schA *) by (dres_inst_tac [("x","schB"), - ("g","Filter (%a. a:act B)`rs")] subst_lemma2 1); + ("g","Filter (%a. a:act B)$rs")] subst_lemma2 1); by (assume_tac 1); by (asm_full_simp_tac (simpset() addsimps [int_is_not_ext]) 1); @@ -1120,7 +1120,7 @@ (* assumption schA *) by (dres_inst_tac [("x","x2"), - ("g","Filter (%a. a:act A)`rs")] subst_lemma2 1); + ("g","Filter (%a. a:act A)$rs")] subst_lemma2 1); by (assume_tac 1); by (asm_full_simp_tac (simpset() addsimps [intA_is_not_actB,int_is_not_ext]) 1); @@ -1158,8 +1158,8 @@ "!! A B. [| 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)"; by (simp_tac (simpset() addsimps [traces_def,has_trace_def]) 1); @@ -1167,12 +1167,12 @@ (* ==> *) (* There is a schedule of A *) -by (res_inst_tac [("x","Filter (%a. a:act A)`sch")] bexI 1); +by (res_inst_tac [("x","Filter (%a. a:act A)$sch")] bexI 1); by (asm_full_simp_tac (simpset() addsimps [compositionality_sch]) 2); by (asm_full_simp_tac (simpset() addsimps [compatibility_consequence1, externals_of_par,ext1_ext2_is_not_act1]) 1); (* There is a schedule of B *) -by (res_inst_tac [("x","Filter (%a. a:act B)`sch")] bexI 1); +by (res_inst_tac [("x","Filter (%a. a:act B)$sch")] bexI 1); by (asm_full_simp_tac (simpset() addsimps [compositionality_sch]) 2); by (asm_full_simp_tac (simpset() addsimps [compatibility_consequence2, externals_of_par,ext1_ext2_is_not_act2]) 1); @@ -1197,7 +1197,7 @@ ren "h1 h2 schA schB" 1; (* mksch is exactly the construction of trA||B out of schA, schB, and the oracle tr, we need here *) -by (res_inst_tac [("x","mksch A B`tr`schA`schB")] bexI 1); +by (res_inst_tac [("x","mksch A B$tr$schA$schB")] bexI 1); (* External actions of mksch are just the oracle *) by (asm_full_simp_tac (simpset() addsimps [FilterA_mksch_is_tr RS spec RS spec RS mp]) 1); diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/CompoTraces.thy --- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy Tue Jan 09 15:36:30 2001 +0100 @@ -17,7 +17,7 @@ defs mksch_def - "mksch A B == (fix`(LAM h tr schA schB. case tr of + "mksch A B == (fix$(LAM h tr schA schB. case tr of nil => nil | x##xs => (case x of @@ -25,24 +25,24 @@ | 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 @@ -56,8 +56,8 @@ let trA = fst TracesA; sigA = snd TracesA; trB = fst TracesB; sigB = snd TracesB in - ( {tr. Filter (%a. a:actions sigA)`tr : trA} - Int {tr. Filter (%a. a:actions sigB)`tr : trB} + ( {tr. Filter (%a. a:actions sigA)$tr : trA} + Int {tr. Filter (%a. a:actions sigB)$tr : trB} Int {tr. Forall (%x. x:(externals sigA Un externals sigB)) tr}, asig_comp sigA sigB)" @@ -65,7 +65,7 @@ finiteR_mksch - "Finite (mksch A B`tr`x`y) --> Finite tr" + "Finite (mksch A B$tr$x$y) --> Finite tr" diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/Compositionality.ML --- a/src/HOLCF/IOA/meta_theory/Compositionality.ML Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/IOA/meta_theory/Compositionality.ML Tue Jan 09 15:36:30 2001 +0100 @@ -15,9 +15,9 @@ Goal "!! A B. [| 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"; by (rtac ForallPFilterQR 1); -(* i.e.: [| (! x. P x --> (Q x = R x)) ; Forall P tr |] ==> Filter Q`tr = Filter R`tr *) +(* i.e.: [| (! x. P x --> (Q x = R x)) ; Forall P tr |] ==> Filter Q$tr = Filter R$tr *) by (assume_tac 2); by (rtac compatibility_consequence3 1); by (REPEAT (asm_full_simp_tac (simpset() @@ -32,7 +32,7 @@ qed"compatibility_consequence4"; Goal "[| 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"; by (rtac ForallPFilterQR 1); by (assume_tac 2); by (rtac compatibility_consequence4 1); diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/Deadlock.ML --- a/src/HOLCF/IOA/meta_theory/Deadlock.ML Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/IOA/meta_theory/Deadlock.ML Tue Jan 09 15:36:30 2001 +0100 @@ -10,8 +10,8 @@ input actions may always be added to a schedule **********************************************************************************) -Goal "[| 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"; +Goal "[| 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"; by (asm_full_simp_tac (simpset() addsimps [schedules_def,has_schedule_def]) 1); by (safe_tac set_cs); by (ftac inp_is_act 1); @@ -21,7 +21,7 @@ by (subgoal_tac "Finite ex" 1); by (asm_full_simp_tac (simpset() addsimps [filter_act_def]) 2); by (rtac (Map2Finite RS iffD1) 2); -by (res_inst_tac [("t","Map fst`ex")] subst 2); +by (res_inst_tac [("t","Map fst$ex")] subst 2); by (assume_tac 2); by (etac FiniteFilter 2); (* subgoal 1 *) @@ -52,7 +52,7 @@ **********************************************************************************) Delsplits [split_if]; Goal "[| 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 |] \ +\ Filter (%x. x:act A)$(sch @@ a>>nil) : schedules A; compatible A B; input_enabled B |] \ \ ==> (sch @@ a>>nil) : schedules (A||B)"; by (asm_full_simp_tac (simpset() addsimps [compositionality_sch,locals_def]) 1); diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/LiveIOA.thy --- a/src/HOLCF/IOA/meta_theory/LiveIOA.thy Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/IOA/meta_theory/LiveIOA.thy Tue Jan 09 15:36:30 2001 +0100 @@ -45,7 +45,7 @@ "liveexecutions AP == {exec. exec : executions (fst AP) & (exec |== (snd AP))}" livetraces_def - "livetraces AP == {mk_trace (fst AP)`(snd ex) | ex. ex:liveexecutions AP}" + "livetraces AP == {mk_trace (fst AP)$(snd ex) | ex. ex:liveexecutions AP}" live_implements_def "live_implements CL AM == (inp (fst CL) = inp (fst AM)) & diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/RefCorrectness.ML --- a/src/HOLCF/IOA/meta_theory/RefCorrectness.ML Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.ML Tue Jan 09 15:36:30 2001 +0100 @@ -21,8 +21,8 @@ Goal "corresp_exC A f = (LAM ex. (%s. case ex of \ \ nil => nil \ \ | x##xs => (flift1 (%pr. (@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) ))"; by (rtac trans 1); by (rtac fix_eq2 1); by (rtac corresp_exC_def 1); @@ -30,19 +30,19 @@ by (simp_tac (simpset() addsimps [flift1_def]) 1); qed"corresp_exC_unfold"; -Goal "(corresp_exC A f`UU) s=UU"; +Goal "(corresp_exC A f$UU) s=UU"; by (stac corresp_exC_unfold 1); by (Simp_tac 1); qed"corresp_exC_UU"; -Goal "(corresp_exC A f`nil) s = nil"; +Goal "(corresp_exC A f$nil) s = nil"; by (stac corresp_exC_unfold 1); by (Simp_tac 1); qed"corresp_exC_nil"; -Goal "(corresp_exC A f`(at>>xs)) s = \ +Goal "(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))"; +\ @@ ((corresp_exC A f$xs) (snd at))"; by (rtac trans 1); by (stac corresp_exC_unfold 1); by (asm_full_simp_tac (simpset() addsimps [Consq_def,flift1_def]) 1); @@ -98,7 +98,7 @@ Goal "[|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))) = \ +\ mk_trace A$((@x. move A x (f s) a (f t))) = \ \ (if a:ext A then a>>nil else nil)"; by (cut_inst_tac [] move_is_move 1); @@ -119,7 +119,7 @@ (* --------------------------------------------------- *) -Goal "mk_trace C`(ex1 @@ ex2)= (mk_trace C`ex1) @@ (mk_trace C`ex2)"; +Goal "mk_trace C$(ex1 @@ ex2)= (mk_trace C$ex1) @@ (mk_trace C$ex2)"; by (simp_tac (simpset() addsimps [mk_trace_def,filter_act_def, FilterConc,MapConc]) 1); qed"mk_traceConc"; @@ -133,7 +133,7 @@ Goalw [corresp_ex_def] "[|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)))"; by (pair_induct_tac "xs" [is_exec_frag_def] 1); (* cons case *) diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/RefCorrectness.thy --- a/src/HOLCF/IOA/meta_theory/RefCorrectness.thy Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.thy Tue Jan 09 15:36:30 2001 +0100 @@ -20,15 +20,15 @@ defs corresp_ex_def - "corresp_ex A f ex == (f (fst ex),(corresp_exC A f`(snd ex)) (fst ex))" + "corresp_ex A f ex == (f (fst ex),(corresp_exC A f$(snd ex)) (fst ex))" corresp_exC_def - "corresp_exC A f == (fix`(LAM h ex. (%s. case ex of + "corresp_exC A f == (fix$(LAM h ex. (%s. case ex of nil => nil | x##xs => (flift1 (%pr. (@cex. move A cex (f s) (fst pr) (f (snd pr))) - @@ ((h`xs) (snd pr))) - `x) )))" + @@ ((h$xs) (snd pr))) + $x) )))" is_fair_ref_map_def "is_fair_ref_map f C A == diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/RefMappings.thy --- a/src/HOLCF/IOA/meta_theory/RefMappings.thy Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/IOA/meta_theory/RefMappings.thy Tue Jan 09 15:36:30 2001 +0100 @@ -24,7 +24,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))" is_ref_map_def "is_ref_map f C A == diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/Seq.ML --- a/src/HOLCF/IOA/meta_theory/Seq.ML Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/IOA/meta_theory/Seq.ML Tue Jan 09 15:36:30 2001 +0100 @@ -34,20 +34,20 @@ bind_thm ("smap_unfold", fix_prover2 thy smap_def "smap = (LAM f tr. case tr of \ \ nil => nil \ - \ | x##xs => f`x ## smap`f`xs)"); + \ | x##xs => f$x ## smap$f$xs)"); -Goal "smap`f`nil=nil"; +Goal "smap$f$nil=nil"; by (stac smap_unfold 1); by (Simp_tac 1); qed"smap_nil"; -Goal "smap`f`UU=UU"; +Goal "smap$f$UU=UU"; by (stac smap_unfold 1); by (Simp_tac 1); qed"smap_UU"; Goal -"[|x~=UU|] ==> smap`f`(x##xs)= (f`x)##smap`f`xs"; +"[|x~=UU|] ==> smap$f$(x##xs)= (f$x)##smap$f$xs"; by (rtac trans 1); by (stac smap_unfold 1); by (Asm_full_simp_tac 1); @@ -61,21 +61,21 @@ bind_thm ("sfilter_unfold", fix_prover2 thy sfilter_def "sfilter = (LAM P tr. case tr of \ \ nil => nil \ - \ | x##xs => If P`x then x##(sfilter`P`xs) else sfilter`P`xs fi)"); + \ | x##xs => If P$x then x##(sfilter$P$xs) else sfilter$P$xs fi)"); -Goal "sfilter`P`nil=nil"; +Goal "sfilter$P$nil=nil"; by (stac sfilter_unfold 1); by (Simp_tac 1); qed"sfilter_nil"; -Goal "sfilter`P`UU=UU"; +Goal "sfilter$P$UU=UU"; by (stac sfilter_unfold 1); by (Simp_tac 1); qed"sfilter_UU"; Goal -"x~=UU ==> sfilter`P`(x##xs)= \ -\ (If P`x then x##(sfilter`P`xs) else sfilter`P`xs fi)"; +"x~=UU ==> sfilter$P$(x##xs)= \ +\ (If P$x then x##(sfilter$P$xs) else sfilter$P$xs fi)"; by (rtac trans 1); by (stac sfilter_unfold 1); by (Asm_full_simp_tac 1); @@ -89,20 +89,20 @@ bind_thm ("sforall2_unfold", fix_prover2 thy sforall2_def "sforall2 = (LAM P tr. case tr of \ \ nil => TT \ - \ | x##xs => (P`x andalso sforall2`P`xs))"); + \ | x##xs => (P$x andalso sforall2$P$xs))"); -Goal "sforall2`P`nil=TT"; +Goal "sforall2$P$nil=TT"; by (stac sforall2_unfold 1); by (Simp_tac 1); qed"sforall2_nil"; -Goal "sforall2`P`UU=UU"; +Goal "sforall2$P$UU=UU"; by (stac sforall2_unfold 1); by (Simp_tac 1); qed"sforall2_UU"; Goal -"x~=UU ==> sforall2`P`(x##xs)= ((P`x) andalso sforall2`P`xs)"; +"x~=UU ==> sforall2$P$(x##xs)= ((P$x) andalso sforall2$P$xs)"; by (rtac trans 1); by (stac sforall2_unfold 1); by (Asm_full_simp_tac 1); @@ -118,21 +118,21 @@ bind_thm ("stakewhile_unfold", fix_prover2 thy stakewhile_def "stakewhile = (LAM P tr. case tr of \ \ nil => nil \ - \ | x##xs => (If P`x then x##(stakewhile`P`xs) else nil fi))"); + \ | x##xs => (If P$x then x##(stakewhile$P$xs) else nil fi))"); -Goal "stakewhile`P`nil=nil"; +Goal "stakewhile$P$nil=nil"; by (stac stakewhile_unfold 1); by (Simp_tac 1); qed"stakewhile_nil"; -Goal "stakewhile`P`UU=UU"; +Goal "stakewhile$P$UU=UU"; by (stac stakewhile_unfold 1); by (Simp_tac 1); qed"stakewhile_UU"; Goal -"x~=UU ==> stakewhile`P`(x##xs) = \ -\ (If P`x then x##(stakewhile`P`xs) else nil fi)"; +"x~=UU ==> stakewhile$P$(x##xs) = \ +\ (If P$x then x##(stakewhile$P$xs) else nil fi)"; by (rtac trans 1); by (stac stakewhile_unfold 1); by (Asm_full_simp_tac 1); @@ -147,21 +147,21 @@ bind_thm ("sdropwhile_unfold", fix_prover2 thy sdropwhile_def "sdropwhile = (LAM P tr. case tr of \ \ nil => nil \ - \ | x##xs => (If P`x then sdropwhile`P`xs else tr fi))"); + \ | x##xs => (If P$x then sdropwhile$P$xs else tr fi))"); -Goal "sdropwhile`P`nil=nil"; +Goal "sdropwhile$P$nil=nil"; by (stac sdropwhile_unfold 1); by (Simp_tac 1); qed"sdropwhile_nil"; -Goal "sdropwhile`P`UU=UU"; +Goal "sdropwhile$P$UU=UU"; by (stac sdropwhile_unfold 1); by (Simp_tac 1); qed"sdropwhile_UU"; Goal -"x~=UU ==> sdropwhile`P`(x##xs) = \ -\ (If P`x then sdropwhile`P`xs else x##xs fi)"; +"x~=UU ==> sdropwhile$P$(x##xs) = \ +\ (If P$x then sdropwhile$P$xs else x##xs fi)"; by (rtac trans 1); by (stac sdropwhile_unfold 1); by (Asm_full_simp_tac 1); @@ -177,21 +177,21 @@ bind_thm ("slast_unfold", fix_prover2 thy slast_def "slast = (LAM tr. case tr of \ \ nil => UU \ - \ | x##xs => (If is_nil`xs then x else slast`xs fi))"); + \ | x##xs => (If is_nil$xs then x else slast$xs fi))"); -Goal "slast`nil=UU"; +Goal "slast$nil=UU"; by (stac slast_unfold 1); by (Simp_tac 1); qed"slast_nil"; -Goal "slast`UU=UU"; +Goal "slast$UU=UU"; by (stac slast_unfold 1); by (Simp_tac 1); qed"slast_UU"; Goal -"x~=UU ==> slast`(x##xs)= (If is_nil`xs then x else slast`xs fi)"; +"x~=UU ==> slast$(x##xs)= (If is_nil$xs then x else slast$xs fi)"; by (rtac trans 1); by (stac slast_unfold 1); by (Asm_full_simp_tac 1); @@ -237,19 +237,19 @@ bind_thm ("sflat_unfold", fix_prover2 thy sflat_def "sflat = (LAM tr. case tr of \ \ nil => nil \ - \ | x##xs => x @@ sflat`xs)"); + \ | x##xs => x @@ sflat$xs)"); -Goal "sflat`nil=nil"; +Goal "sflat$nil=nil"; by (stac sflat_unfold 1); by (Simp_tac 1); qed"sflat_nil"; -Goal "sflat`UU=UU"; +Goal "sflat$UU=UU"; by (stac sflat_unfold 1); by (Simp_tac 1); qed"sflat_UU"; -Goal "sflat`(x##xs)= x@@(sflat`xs)"; +Goal "sflat$(x##xs)= x@@(sflat$xs)"; by (rtac trans 1); by (stac sflat_unfold 1); by (Asm_full_simp_tac 1); @@ -269,32 +269,32 @@ \ nil => nil \ \ | x##xs => (case t2 of \ \ nil => UU \ -\ | y##ys => ##(szip`xs`ys)))"); +\ | y##ys => ##(szip$xs$ys)))"); -Goal "szip`nil`y=nil"; +Goal "szip$nil$y=nil"; by (stac szip_unfold 1); by (Simp_tac 1); qed"szip_nil"; -Goal "szip`UU`y=UU"; +Goal "szip$UU$y=UU"; by (stac szip_unfold 1); by (Simp_tac 1); qed"szip_UU1"; -Goal "x~=nil ==> szip`x`UU=UU"; +Goal "x~=nil ==> szip$x$UU=UU"; by (stac szip_unfold 1); by (Asm_full_simp_tac 1); by (res_inst_tac [("x","x")] seq.casedist 1); by (REPEAT (Asm_full_simp_tac 1)); qed"szip_UU2"; -Goal "x~=UU ==> szip`(x##xs)`nil=UU"; +Goal "x~=UU ==> szip$(x##xs)$nil=UU"; by (rtac trans 1); by (stac szip_unfold 1); by (REPEAT (Asm_full_simp_tac 1)); qed"szip_cons_nil"; -Goal "[| x~=UU; y~=UU|] ==> szip`(x##xs)`(y##ys) = ##szip`xs`ys"; +Goal "[| x~=UU; y~=UU|] ==> szip$(x##xs)$(y##ys) = ##szip$xs$ys"; by (rtac trans 1); by (stac szip_unfold 1); by (REPEAT (Asm_full_simp_tac 1)); @@ -348,7 +348,7 @@ Addsimps [if_and_sconc]; -Goal "sfilter`P`(x @@ y) = (sfilter`P`x @@ sfilter`P`y)"; +Goal "sfilter$P$(x @@ y) = (sfilter$P$x @@ sfilter$P$y)"; by (res_inst_tac[("x","x")] seq.ind 1); (* adm *) @@ -360,7 +360,7 @@ by (asm_full_simp_tac (simpset() setloop split_If_tac) 1); qed"sfiltersconc"; -Goal "sforall P (stakewhile`P`x)"; +Goal "sforall P (stakewhile$P$x)"; by (simp_tac (simpset() addsimps [sforall_def]) 1); by (res_inst_tac[("x","x")] seq.ind 1); (* adm *) @@ -372,7 +372,7 @@ by (asm_full_simp_tac (simpset() setloop split_If_tac) 1); qed"sforallPstakewhileP"; -Goal "sforall P (sfilter`P`x)"; +Goal "sforall P (sfilter$P$x)"; by (simp_tac (simpset() addsimps [sforall_def]) 1); by (res_inst_tac[("x","x")] seq.ind 1); (* adm *) @@ -438,7 +438,7 @@ qed_goalw "seq_finite_ind_lemma" thy [seq.finite_def] -"(!!n. P(seq_take n`s)) ==> seq_finite(s) -->P(s)" +"(!!n. P(seq_take n$s)) ==> seq_finite(s) -->P(s)" (fn prems => [ (strip_tac 1), diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/Seq.thy --- a/src/HOLCF/IOA/meta_theory/Seq.thy Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/IOA/meta_theory/Seq.thy Tue Jan 09 15:36:30 2001 +0100 @@ -36,7 +36,7 @@ "Finite" :: "'a seq => bool" translations - "xs @@ ys" == "sconc`xs`ys" + "xs @@ ys" == "sconc$xs$ys" "Finite x" == "x:sfinite" "~(Finite x)" =="x~:sfinite" @@ -47,63 +47,63 @@ (* f not possible at lhs, as "pattern matching" only for % x arguments, f cannot be written at rhs in front, as fix_eq3 does not apply later *) smap_def - "smap == (fix`(LAM h f tr. case tr of + "smap == (fix$(LAM h f tr. case tr of nil => nil - | x##xs => f`x ## h`f`xs))" + | x##xs => f$x ## h$f$xs))" sfilter_def - "sfilter == (fix`(LAM h P t. case t of + "sfilter == (fix$(LAM h P t. case t of nil => nil - | x##xs => If P`x - then x##(h`P`xs) - else h`P`xs + | x##xs => If P$x + then x##(h$P$xs) + else h$P$xs fi))" sforall_def - "sforall P t == (sforall2`P`t ~=FF)" + "sforall P t == (sforall2$P$t ~=FF)" sforall2_def - "sforall2 == (fix`(LAM h P t. case t of + "sforall2 == (fix$(LAM h P t. case t of nil => TT - | x##xs => P`x andalso h`P`xs))" + | x##xs => P$x andalso h$P$xs))" sconc_def - "sconc == (fix`(LAM h t1 t2. case t1 of + "sconc == (fix$(LAM h t1 t2. case t1 of nil => t2 - | x##xs => x##(h`xs`t2)))" + | x##xs => x##(h$xs$t2)))" slast_def - "slast == (fix`(LAM h t. case t of + "slast == (fix$(LAM h t. case t of nil => UU - | x##xs => (If is_nil`xs + | x##xs => (If is_nil$xs then x - else h`xs fi)))" + else h$xs fi)))" stakewhile_def - "stakewhile == (fix`(LAM h P t. case t of + "stakewhile == (fix$(LAM h P t. case t of nil => nil - | x##xs => If P`x - then x##(h`P`xs) + | x##xs => If P$x + then x##(h$P$xs) else nil fi))" sdropwhile_def - "sdropwhile == (fix`(LAM h P t. case t of + "sdropwhile == (fix$(LAM h P t. case t of nil => nil - | x##xs => If P`x - then h`P`xs + | x##xs => If P$x + then h$P$xs else t fi))" sflat_def - "sflat == (fix`(LAM h t. case t of + "sflat == (fix$(LAM h t. case t of nil => nil - | x##xs => x @@ (h`xs)))" + | x##xs => x @@ (h$xs)))" szip_def - "szip == (fix`(LAM h t1 t2. case t1 of + "szip == (fix$(LAM h t1 t2. case t1 of nil => nil | x##xs => (case t2 of nil => UU - | y##ys => ##(h`xs`ys))))" + | y##ys => ##(h$xs$ys))))" Partial_def "Partial x == (seq_finite x) & ~(Finite x)" diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/Sequence.ML --- a/src/HOLCF/IOA/meta_theory/Sequence.ML Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/IOA/meta_theory/Sequence.ML Tue Jan 09 15:36:30 2001 +0100 @@ -18,15 +18,15 @@ (* Map *) (* ---------------------------------------------------------------- *) -Goal "Map f`UU =UU"; +Goal "Map f$UU =UU"; by (simp_tac (simpset() addsimps [Map_def]) 1); qed"Map_UU"; -Goal "Map f`nil =nil"; +Goal "Map f$nil =nil"; by (simp_tac (simpset() addsimps [Map_def]) 1); qed"Map_nil"; -Goal "Map f`(x>>xs)=(f x) >> Map f`xs"; +Goal "Map f$(x>>xs)=(f x) >> Map f$xs"; by (simp_tac (simpset() addsimps [Map_def, Consq_def,flift2_def]) 1); qed"Map_cons"; @@ -34,15 +34,15 @@ (* Filter *) (* ---------------------------------------------------------------- *) -Goal "Filter P`UU =UU"; +Goal "Filter P$UU =UU"; by (simp_tac (simpset() addsimps [Filter_def]) 1); qed"Filter_UU"; -Goal "Filter P`nil =nil"; +Goal "Filter P$nil =nil"; by (simp_tac (simpset() addsimps [Filter_def]) 1); qed"Filter_nil"; -Goal "Filter P`(x>>xs)= (if P x then x>>(Filter P`xs) else Filter P`xs)"; +Goal "Filter P$(x>>xs)= (if P x then x>>(Filter P$xs) else Filter P$xs)"; by (simp_tac (simpset() addsimps [Filter_def, Consq_def,flift2_def,If_and_if]) 1); qed"Filter_cons"; @@ -76,15 +76,15 @@ (* Takewhile *) (* ---------------------------------------------------------------- *) -Goal "Takewhile P`UU =UU"; +Goal "Takewhile P$UU =UU"; by (simp_tac (simpset() addsimps [Takewhile_def]) 1); qed"Takewhile_UU"; -Goal "Takewhile P`nil =nil"; +Goal "Takewhile P$nil =nil"; by (simp_tac (simpset() addsimps [Takewhile_def]) 1); qed"Takewhile_nil"; -Goal "Takewhile P`(x>>xs)= (if P x then x>>(Takewhile P`xs) else nil)"; +Goal "Takewhile P$(x>>xs)= (if P x then x>>(Takewhile P$xs) else nil)"; by (simp_tac (simpset() addsimps [Takewhile_def, Consq_def,flift2_def,If_and_if]) 1); qed"Takewhile_cons"; @@ -92,15 +92,15 @@ (* Dropwhile *) (* ---------------------------------------------------------------- *) -Goal "Dropwhile P`UU =UU"; +Goal "Dropwhile P$UU =UU"; by (simp_tac (simpset() addsimps [Dropwhile_def]) 1); qed"Dropwhile_UU"; -Goal "Dropwhile P`nil =nil"; +Goal "Dropwhile P$nil =nil"; by (simp_tac (simpset() addsimps [Dropwhile_def]) 1); qed"Dropwhile_nil"; -Goal "Dropwhile P`(x>>xs)= (if P x then Dropwhile P`xs else x>>xs)"; +Goal "Dropwhile P$(x>>xs)= (if P x then Dropwhile P$xs else x>>xs)"; by (simp_tac (simpset() addsimps [Dropwhile_def, Consq_def,flift2_def,If_and_if]) 1); qed"Dropwhile_cons"; @@ -109,15 +109,15 @@ (* ---------------------------------------------------------------- *) -Goal "Last`UU =UU"; +Goal "Last$UU =UU"; by (simp_tac (simpset() addsimps [Last_def]) 1); qed"Last_UU"; -Goal "Last`nil =UU"; +Goal "Last$nil =UU"; by (simp_tac (simpset() addsimps [Last_def]) 1); qed"Last_nil"; -Goal "Last`(x>>xs)= (if xs=nil then Def x else Last`xs)"; +Goal "Last$(x>>xs)= (if xs=nil then Def x else Last$xs)"; by (simp_tac (simpset() addsimps [Last_def, Consq_def]) 1); by (res_inst_tac [("x","xs")] seq.casedist 1); by (Asm_simp_tac 1); @@ -129,15 +129,15 @@ (* Flat *) (* ---------------------------------------------------------------- *) -Goal "Flat`UU =UU"; +Goal "Flat$UU =UU"; by (simp_tac (simpset() addsimps [Flat_def]) 1); qed"Flat_UU"; -Goal "Flat`nil =nil"; +Goal "Flat$nil =nil"; by (simp_tac (simpset() addsimps [Flat_def]) 1); qed"Flat_nil"; -Goal "Flat`(x##xs)= x @@ (Flat`xs)"; +Goal "Flat$(x##xs)= x @@ (Flat$xs)"; by (simp_tac (simpset() addsimps [Flat_def, Consq_def]) 1); qed"Flat_cons"; @@ -154,7 +154,7 @@ \ Undef => UU \ \ | Def a => (case y of \ \ Undef => UU \ -\ | Def b => Def (a,b)##(Zip`xs`ys)))))"; +\ | Def b => Def (a,b)##(Zip$xs$ys)))))"; by (rtac trans 1); by (rtac fix_eq2 1); by (rtac Zip_def 1); @@ -162,29 +162,29 @@ by (Simp_tac 1); qed"Zip_unfold"; -Goal "Zip`UU`y =UU"; +Goal "Zip$UU$y =UU"; by (stac Zip_unfold 1); by (Simp_tac 1); qed"Zip_UU1"; -Goal "x~=nil ==> Zip`x`UU =UU"; +Goal "x~=nil ==> Zip$x$UU =UU"; by (stac Zip_unfold 1); by (Simp_tac 1); by (res_inst_tac [("x","x")] seq.casedist 1); by (REPEAT (Asm_full_simp_tac 1)); qed"Zip_UU2"; -Goal "Zip`nil`y =nil"; +Goal "Zip$nil$y =nil"; by (stac Zip_unfold 1); by (Simp_tac 1); qed"Zip_nil"; -Goal "Zip`(x>>xs)`nil= UU"; +Goal "Zip$(x>>xs)$nil= UU"; by (stac Zip_unfold 1); by (simp_tac (simpset() addsimps [Consq_def]) 1); qed"Zip_cons_nil"; -Goal "Zip`(x>>xs)`(y>>ys)= (x,y) >> Zip`xs`ys"; +Goal "Zip$(x>>xs)$(y>>ys)= (x,y) >> Zip$xs$ys"; by (rtac trans 1); by (stac Zip_unfold 1); by (Simp_tac 1); @@ -298,7 +298,7 @@ by (etac monofun_cfun_arg 1); qed"Cons_inject_less_eq"; -Goal "seq_take (Suc n)`(a>>x) = a>> (seq_take n`x)"; +Goal "seq_take (Suc n)$(a>>x) = a>> (seq_take n$x)"; by (simp_tac (simpset() addsimps [Consq_def]) 1); qed"seq_take_Cons"; @@ -365,11 +365,11 @@ section "HD,TL"; -Goal "HD`(x>>y) = Def x"; +Goal "HD$(x>>y) = Def x"; by (simp_tac (simpset() addsimps [Consq_def]) 1); qed"HD_Cons"; -Goal "TL`(x>>y) = y"; +Goal "TL$(x>>y) = y"; by (simp_tac (simpset() addsimps [Consq_def]) 1); qed"TL_Cons"; @@ -415,11 +415,11 @@ Addsimps [FiniteConc]; -Goal "Finite s ==> Finite (Map f`s)"; +Goal "Finite s ==> Finite (Map f$s)"; by (Seq_Finite_induct_tac 1); qed"FiniteMap1"; -Goal "Finite s ==> ! t. (s = Map f`t) --> Finite t"; +Goal "Finite s ==> ! t. (s = Map f$t) --> Finite t"; by (Seq_Finite_induct_tac 1); by (strip_tac 1); by (Seq_case_simp_tac "t" 1); @@ -430,7 +430,7 @@ by (Asm_full_simp_tac 1); qed"FiniteMap2"; -Goal "Finite (Map f`s) = Finite s"; +Goal "Finite (Map f$s) = Finite s"; by Auto_tac; by (etac (FiniteMap2 RS spec RS mp) 1); by (rtac refl 1); @@ -438,7 +438,7 @@ qed"Map2Finite"; -Goal "Finite s ==> Finite (Filter P`s)"; +Goal "Finite s ==> Finite (Filter P$s)"; by (Seq_Finite_induct_tac 1); qed"FiniteFilter"; @@ -519,11 +519,11 @@ section "Last"; -Goal "Finite s ==> s~=nil --> Last`s~=UU"; +Goal "Finite s ==> s~=nil --> Last$s~=UU"; by (Seq_Finite_induct_tac 1); qed"Finite_Last1"; -Goal "Finite s ==> Last`s=UU --> s=nil"; +Goal "Finite s ==> Last$s=UU --> s=nil"; by (Seq_Finite_induct_tac 1); by (fast_tac HOL_cs 1); qed"Finite_Last2"; @@ -535,11 +535,11 @@ section "Filter, Conc"; -Goal "Filter P`(Filter Q`s) = Filter (%x. P x & Q x)`s"; +Goal "Filter P$(Filter Q$s) = Filter (%x. P x & Q x)$s"; by (Seq_induct_tac "s" [Filter_def] 1); qed"FilterPQ"; -Goal "Filter P`(x @@ y) = (Filter P`x @@ Filter P`y)"; +Goal "Filter P$(x @@ y) = (Filter P$x @@ Filter P$y)"; by (simp_tac (simpset() addsimps [Filter_def,sfiltersconc]) 1); qed"FilterConc"; @@ -547,24 +547,24 @@ section "Map"; -Goal "Map f`(Map g`s) = Map (f o g)`s"; +Goal "Map f$(Map g$s) = Map (f o g)$s"; by (Seq_induct_tac "s" [] 1); qed"MapMap"; -Goal "Map f`(x@@y) = (Map f`x) @@ (Map f`y)"; +Goal "Map f$(x@@y) = (Map f$x) @@ (Map f$y)"; by (Seq_induct_tac "x" [] 1); qed"MapConc"; -Goal "Filter P`(Map f`x) = Map f`(Filter (P o f)`x)"; +Goal "Filter P$(Map f$x) = Map f$(Filter (P o f)$x)"; by (Seq_induct_tac "x" [] 1); qed"MapFilter"; -Goal "nil = (Map f`s) --> s= nil"; +Goal "nil = (Map f$s) --> s= nil"; by (Seq_case_simp_tac "s" 1); qed"nilMap"; -Goal "Forall P (Map f`s) = Forall (P o f) s"; +Goal "Forall P (Map f$s) = Forall (P o f) s"; by (Seq_induct_tac "s" [Forall_def,sforall_def] 1); qed"ForallMap"; @@ -593,13 +593,13 @@ Addsimps [Forall_Conc]; -Goal "Forall P s --> Forall P (TL`s)"; +Goal "Forall P s --> Forall P (TL$s)"; by (Seq_induct_tac "s" [Forall_def,sforall_def] 1); qed"ForallTL1"; bind_thm ("ForallTL",ForallTL1 RS mp); -Goal "Forall P s --> Forall P (Dropwhile Q`s)"; +Goal "Forall P s --> Forall P (Dropwhile Q$s)"; by (Seq_induct_tac "s" [Forall_def,sforall_def] 1); qed"ForallDropwhile1"; @@ -624,7 +624,7 @@ qed"Forall_postfixclosed"; -Goal "((! x. P x --> (Q x = R x)) & Forall P tr) --> Filter Q`tr = Filter R`tr"; +Goal "((! x. P x --> (Q x = R x)) & Forall P tr) --> Filter Q$tr = Filter R$tr"; by (Seq_induct_tac "tr" [Forall_def,sforall_def] 1); qed"ForallPFilterQR1"; @@ -636,12 +636,12 @@ section "Forall, Filter"; -Goal "Forall P (Filter P`x)"; +Goal "Forall P (Filter P$x)"; by (simp_tac (simpset() addsimps [Filter_def,Forall_def,forallPsfilterP]) 1); qed"ForallPFilterP"; (* holds also in other direction, then equal to forallPfilterP *) -Goal "Forall P x --> Filter P`x = x"; +Goal "Forall P x --> Filter P$x = x"; by (Seq_induct_tac "x" [Forall_def,sforall_def,Filter_def] 1); qed"ForallPFilterPid1"; @@ -650,7 +650,7 @@ (* holds also in other direction *) Goal "!! ys . Finite ys ==> \ -\ Forall (%x. ~P x) ys --> Filter P`ys = nil "; +\ Forall (%x. ~P x) ys --> Filter P$ys = nil "; by (Seq_Finite_induct_tac 1); qed"ForallnPFilterPnil1"; @@ -659,7 +659,7 @@ (* holds also in other direction *) Goal "~Finite ys & Forall (%x. ~P x) ys \ -\ --> Filter P`ys = UU "; +\ --> Filter P$ys = UU "; by (Seq_induct_tac "ys" [Forall_def,sforall_def] 1); qed"ForallnPFilterPUU1"; @@ -668,7 +668,7 @@ (* inverse of ForallnPFilterPnil *) -Goal "!! ys . Filter P`ys = nil --> \ +Goal "!! ys . Filter P$ys = nil --> \ \ (Forall (%x. ~P x) ys & Finite ys)"; by (res_inst_tac[("x","ys")] Seq_induct 1); (* adm *) @@ -685,15 +685,15 @@ (* inverse of ForallnPFilterPUU. proved by 2 lemmas because of adm problems *) -Goal "Finite ys ==> Filter P`ys ~= UU"; +Goal "Finite ys ==> Filter P$ys ~= UU"; by (Seq_Finite_induct_tac 1); qed"FilterUU_nFinite_lemma1"; -Goal "~ Forall (%x. ~P x) ys --> Filter P`ys ~= UU"; +Goal "~ Forall (%x. ~P x) ys --> Filter P$ys ~= UU"; by (Seq_induct_tac "ys" [Forall_def,sforall_def] 1); qed"FilterUU_nFinite_lemma2"; -Goal "Filter P`ys = UU ==> \ +Goal "Filter P$ys = UU ==> \ \ (Forall (%x. ~P x) ys & ~Finite ys)"; by (rtac conjI 1); by (cut_inst_tac [] (FilterUU_nFinite_lemma2 RS mp COMP rev_contrapos) 1); @@ -703,14 +703,14 @@ Goal "!! Q P.[| Forall Q ys; Finite ys; !!x. Q x ==> ~P x|] \ -\ ==> Filter P`ys = nil"; +\ ==> Filter P$ys = nil"; by (etac ForallnPFilterPnil 1); by (etac ForallPForallQ 1); by Auto_tac; qed"ForallQFilterPnil"; Goal "!! Q P. [| ~Finite ys; Forall Q ys; !!x. Q x ==> ~P x|] \ -\ ==> Filter P`ys = UU "; +\ ==> Filter P$ys = UU "; by (etac ForallnPFilterPUU 1); by (etac ForallPForallQ 1); by Auto_tac; @@ -723,20 +723,20 @@ section "Takewhile, Forall, Filter"; -Goal "Forall P (Takewhile P`x)"; +Goal "Forall P (Takewhile P$x)"; by (simp_tac (simpset() addsimps [Forall_def,Takewhile_def,sforallPstakewhileP]) 1); qed"ForallPTakewhileP"; -Goal"!! P. [| !!x. Q x==> P x |] ==> Forall P (Takewhile Q`x)"; +Goal"!! P. [| !!x. Q x==> P x |] ==> Forall P (Takewhile Q$x)"; by (rtac ForallPForallQ 1); by (rtac ForallPTakewhileP 1); by Auto_tac; qed"ForallPTakewhileQ"; -Goal "!! Q P.[| Finite (Takewhile Q`ys); !!x. Q x ==> ~P x |] \ -\ ==> Filter P`(Takewhile Q`ys) = nil"; +Goal "!! Q P.[| Finite (Takewhile Q$ys); !!x. Q x ==> ~P x |] \ +\ ==> Filter P$(Takewhile Q$ys) = nil"; by (etac ForallnPFilterPnil 1); by (rtac ForallPForallQ 1); by (rtac ForallPTakewhileP 1); @@ -744,7 +744,7 @@ qed"FilterPTakewhileQnil"; Goal "!! Q P. [| !!x. Q x ==> P x |] ==> \ -\ Filter P`(Takewhile Q`ys) = (Takewhile Q`ys)"; +\ Filter P$(Takewhile Q$ys) = (Takewhile Q$ys)"; by (rtac ForallPFilterPid 1); by (rtac ForallPForallQ 1); by (rtac ForallPTakewhileP 1); @@ -754,28 +754,28 @@ Addsimps [ForallPTakewhileP,ForallPTakewhileQ, FilterPTakewhileQnil,FilterPTakewhileQid]; -Goal "Takewhile P`(Takewhile P`s) = Takewhile P`s"; +Goal "Takewhile P$(Takewhile P$s) = Takewhile P$s"; by (Seq_induct_tac "s" [Forall_def,sforall_def] 1); qed"Takewhile_idempotent"; -Goal "Forall P s --> Takewhile (%x. Q x | (~P x))`s = Takewhile Q`s"; +Goal "Forall P s --> Takewhile (%x. Q x | (~P x))$s = Takewhile Q$s"; by (Seq_induct_tac "s" [Forall_def,sforall_def] 1); qed"ForallPTakewhileQnP"; -Goal "Forall P s --> Dropwhile (%x. Q x | (~P x))`s = Dropwhile Q`s"; +Goal "Forall P s --> Dropwhile (%x. Q x | (~P x))$s = Dropwhile Q$s"; by (Seq_induct_tac "s" [Forall_def,sforall_def] 1); qed"ForallPDropwhileQnP"; Addsimps [ForallPTakewhileQnP RS mp, ForallPDropwhileQnP RS mp]; -Goal "Forall P s --> Takewhile P`(s @@ t) = s @@ (Takewhile P`t)"; +Goal "Forall P s --> Takewhile P$(s @@ t) = s @@ (Takewhile P$t)"; by (Seq_induct_tac "s" [Forall_def,sforall_def] 1); qed"TakewhileConc1"; bind_thm("TakewhileConc",TakewhileConc1 RS mp); -Goal "Finite s ==> Forall P s --> Dropwhile P`(s @@ t) = Dropwhile P`t"; +Goal "Finite s ==> Forall P s --> Dropwhile P$(s @@ t) = Dropwhile P$t"; by (Seq_Finite_induct_tac 1); qed"DropwhileConc1"; @@ -788,9 +788,9 @@ section "coinductive characterizations of Filter"; -Goal "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"; +Goal "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 *) @@ -804,16 +804,16 @@ by (Asm_full_simp_tac 1); qed"divide_Seq_lemma"; -Goal "(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"; +Goal "(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"; by (rtac (divide_Seq_lemma RS mp) 1); by (dres_inst_tac [("fo","HD"),("xa","x>>xs")] monofun_cfun_arg 1); by (Asm_full_simp_tac 1); qed"divide_Seq"; -Goal "~Forall P y --> (? x. HD`(Filter (%a. ~P a)`y) = Def x)"; +Goal "~Forall P y --> (? x. HD$(Filter (%a. ~P a)$y) = Def x)"; (* Pay attention: is only admissible with chain-finite package to be added to adm test *) by (Seq_induct_tac "y" [Forall_def,sforall_def] 1); @@ -821,8 +821,8 @@ Goal "~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)"; by (dtac (nForall_HDFilter RS mp) 1); by (safe_tac set_cs); by (res_inst_tac [("x","x")] exI 1); @@ -846,15 +846,15 @@ section "take_lemma"; -Goal "(!n. seq_take n`x = seq_take n`x') = (x = x')"; +Goal "(!n. seq_take n$x = seq_take n$x') = (x = x')"; by (rtac iffI 1); by (resolve_tac seq.take_lemmas 1); by Auto_tac; qed"seq_take_lemma"; Goal -" ! 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)))"; by (Seq_induct_tac "x" [] 1); by (strip_tac 1); by (case_tac "n" 1); @@ -864,8 +864,8 @@ qed"take_reduction1"; -Goal "!! 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))"; +Goal "!! 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))"; by (auto_tac (claset() addSIs [take_reduction1 RS spec RS mp],simpset())); qed"take_reduction"; @@ -875,8 +875,8 @@ ------------------------------------------------------------------ *) Goal -" ! 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)))"; by (Seq_induct_tac "x" [] 1); by (strip_tac 1); by (case_tac "n" 1); @@ -886,14 +886,14 @@ qed"take_reduction_less1"; -Goal "!! 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))"; +Goal "!! 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))"; by (auto_tac (claset() addSIs [take_reduction_less1 RS spec RS mp],simpset())); qed"take_reduction_less"; val prems = goalw thy [seq.take_def] -"(!! n. seq_take n`s1 << seq_take n`s2) ==> s1< s1< (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)) |] \ +\ ==> ! n. seq_take n$(f (s1 @@ y>>s2)) \ +\ = seq_take n$(g (s1 @@ y>>s2)) |] \ \ ==> A x --> (f x)=(g x)"; by (case_tac "Forall Q x" 1); by (auto_tac (claset() addSDs [divide_Seq3],simpset())); @@ -951,10 +951,10 @@ Goal "!! 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);\ +\ !! 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)) |] \ +\ ==> seq_take (Suc n)$(f (s1 @@ y>>s2)) \ +\ = seq_take (Suc n)$(g (s1 @@ y>>s2)) |] \ \ ==> A x --> (f x)=(g x)"; by (rtac impI 1); by (resolve_tac seq.take_lemmas 1); @@ -973,10 +973,10 @@ Goal "!! 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);\ +\ !! 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)) |] \ +\ ==> seq_take n$(f (s1 @@ y>>s2)) \ +\ = seq_take n$(g (s1 @@ y>>s2)) |] \ \ ==> A x --> (f x)=(g x)"; by (rtac impI 1); by (resolve_tac seq.take_lemmas 1); @@ -1025,10 +1025,10 @@ Goal "!! Q. [|!! s h1 h2. [| Forall Q s; A s h1 h2|] ==> (f s h1 h2) = (g s h1 h2) ; \ -\ !! s1 s2 y n. [| ! t h1 h2 m. m < n --> (A t h1 h2) --> seq_take m`(f t h1 h2) = seq_take m`(g t h1 h2);\ +\ !! s1 s2 y n. [| ! t h1 h2 m. m < n --> (A t h1 h2) --> seq_take m$(f t h1 h2) = seq_take m$(g t h1 h2);\ \ Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) h1 h2|] \ -\ ==> seq_take n`(f (s1 @@ y>>s2) h1 h2) \ -\ = seq_take n`(g (s1 @@ y>>s2) h1 h2) |] \ +\ ==> seq_take n$(f (s1 @@ y>>s2) h1 h2) \ +\ = seq_take n$(g (s1 @@ y>>s2) h1 h2) |] \ \ ==> ! h1 h2. (A x h1 h2) --> (f x h1 h2)=(g x h1 h2)"; by (strip_tac 1); by (resolve_tac seq.take_lemmas 1); @@ -1049,14 +1049,14 @@ Goal "!! Q. [|!! s. Forall Q s ==> P ((f s) = (g s)) ; \ -\ !! s1 s2 y n. [| ! t m. m < n --> P (seq_take m`(f t) = seq_take m`(g t));\ +\ !! s1 s2 y n. [| ! t m. m < n --> P (seq_take m$(f t) = seq_take m$(g t));\ \ Forall Q s1; Finite s1; ~ Q y|] \ -\ ==> P (seq_take n`(f (s1 @@ y>>s2)) \ -\ = seq_take n`(g (s1 @@ y>>s2))) |] \ +\ ==> P (seq_take n$(f (s1 @@ y>>s2)) \ +\ = seq_take n$(g (s1 @@ y>>s2))) |] \ \ ==> P ((f x)=(g x))"; by (res_inst_tac [("t","f x = g x"), - ("s","!n. seq_take n`(f x) = seq_take n`(g x)")] subst 1); + ("s","!n. seq_take n$(f x) = seq_take n$(g x)")] subst 1); by (rtac seq_take_lemma 1); wie ziehe ich n durch P, d.h. evtl. ns in P muessen umbenannt werden..... @@ -1079,10 +1079,10 @@ Goal "!! 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);\ +\ !! 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)) |] \ +\ ==> seq_take (Suc n)$(f (y>>s)) \ +\ = seq_take (Suc n)$(g (y>>s)) |] \ \ ==> A x --> (f x)=(g x)"; by (rtac impI 1); by (resolve_tac seq.take_lemmas 1); @@ -1111,26 +1111,26 @@ (* In general: How to do this case without the same adm problems as for the entire proof ? *) Goal "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"; by (Seq_induct_tac "s" [Forall_def,sforall_def] 1); qed"Filter_lemma1"; Goal "Finite s ==> \ \ (Forall (%x. (~P x) | (~ Q x)) s \ -\ --> Filter P`(Filter Q`s) = nil)"; +\ --> Filter P$(Filter Q$s) = nil)"; by (Seq_Finite_induct_tac 1); qed"Filter_lemma2"; Goal "Finite s ==> \ \ Forall (%x. (~P x) | (~ Q x)) s \ -\ --> Filter (%x. P x & Q x)`s = nil"; +\ --> Filter (%x. P x & Q x)$s = nil"; by (Seq_Finite_induct_tac 1); qed"Filter_lemma3"; -Goal "Filter P`(Filter Q`s) = Filter (%x. P x & Q x)`s"; +Goal "Filter P$(Filter Q$s) = Filter (%x. P x & Q x)$s"; by (res_inst_tac [("A1","%x. True") ,("Q1","%x.~(P x & Q x)"),("x1","s")] (take_lemma_induct RS mp) 1); @@ -1149,7 +1149,7 @@ -Goal "Map f`(x@@y) = (Map f`x) @@ (Map f`y)"; +Goal "Map f$(x@@y) = (Map f$x) @@ (Map f$y)"; by (res_inst_tac [("A1","%x. True"), ("x1","x")] (take_lemma_in_eq_out RS mp) 1); by Auto_tac; diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/Sequence.thy --- a/src/HOLCF/IOA/meta_theory/Sequence.thy Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Tue Jan 09 15:36:30 2001 +0100 @@ -42,7 +42,7 @@ translations - "a>>s" == "Consq a`s" + "a>>s" == "Consq a$s" "[x, xs!]" == "x>>[xs!]" "[x!]" == "x>>nil" "[x, xs?]" == "x>>[xs?]" @@ -53,22 +53,22 @@ Consq_def "Consq a == LAM s. Def a ## s" -Filter_def "Filter P == sfilter`(flift2 P)" +Filter_def "Filter P == sfilter$(flift2 P)" -Map_def "Map f == smap`(flift2 f)" +Map_def "Map f == smap$(flift2 f)" Forall_def "Forall P == sforall (flift2 P)" Last_def "Last == slast" -Dropwhile_def "Dropwhile P == sdropwhile`(flift2 P)" +Dropwhile_def "Dropwhile P == sdropwhile$(flift2 P)" -Takewhile_def "Takewhile P == stakewhile`(flift2 P)" +Takewhile_def "Takewhile P == stakewhile$(flift2 P)" Flat_def "Flat == sflat" Zip_def - "Zip == (fix`(LAM h t1 t2. case t1 of + "Zip == (fix$(LAM h t1 t2. case t1 of nil => nil | x##xs => (case t2 of nil => UU @@ -76,13 +76,13 @@ Undef => UU | Def a => (case y of Undef => UU - | Def b => Def (a,b)##(h`xs`ys))))))" + | Def b => Def (a,b)##(h$xs$ys))))))" -Filter2_def "Filter2 P == (fix`(LAM h t. case t of +Filter2_def "Filter2 P == (fix$(LAM h t. case t of nil => nil | x##xs => (case x of Undef => UU | Def y => (if P y - then x##(h`xs) - else h`xs))))" + then x##(h$xs) + else h$xs))))" rules diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/ShortExecutions.ML --- a/src/HOLCF/IOA/meta_theory/ShortExecutions.ML Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.ML Tue Jan 09 15:36:30 2001 +0100 @@ -29,24 +29,24 @@ \ | x##xs => \ \ (case x of\ \ Undef => UU\ -\ | Def y => (Takewhile (%a.~ P a)`s)\ -\ @@ (y>>(oraclebuild P`(TL`(Dropwhile (%a.~ P a)`s))`xs))\ +\ | Def y => (Takewhile (%a.~ P a)$s)\ +\ @@ (y>>(oraclebuild P$(TL$(Dropwhile (%a.~ P a)$s))$xs))\ \ )\ \ )"); -Goal "oraclebuild P`sch`UU = UU"; +Goal "oraclebuild P$sch$UU = UU"; by (stac oraclebuild_unfold 1); by (Simp_tac 1); qed"oraclebuild_UU"; -Goal "oraclebuild P`sch`nil = nil"; +Goal "oraclebuild P$sch$nil = nil"; by (stac oraclebuild_unfold 1); by (Simp_tac 1); qed"oraclebuild_nil"; -Goal "oraclebuild P`s`(x>>t) = \ -\ (Takewhile (%a.~ P a)`s) \ -\ @@ (x>>(oraclebuild P`(TL`(Dropwhile (%a.~ P a)`s))`t))"; +Goal "oraclebuild P$s$(x>>t) = \ +\ (Takewhile (%a.~ P a)$s) \ +\ @@ (x>>(oraclebuild P$(TL$(Dropwhile (%a.~ P a)$s))$t))"; by (rtac trans 1); by (stac oraclebuild_unfold 1); by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1); @@ -63,7 +63,7 @@ Goalw [Cut_def] "[| Forall (%a.~ P a) s; Finite s|] \ \ ==> Cut P s =nil"; -by (subgoal_tac "Filter P`s = nil" 1); +by (subgoal_tac "Filter P$s = nil" 1); by (asm_simp_tac (simpset() addsimps [oraclebuild_nil]) 1); by (rtac ForallQFilterPnil 1); by (REPEAT (atac 1)); @@ -72,7 +72,7 @@ Goalw [Cut_def] "[| Forall (%a.~ P a) s; ~Finite s|] \ \ ==> Cut P s =UU"; -by (subgoal_tac "Filter P`s= UU" 1); +by (subgoal_tac "Filter P$s= UU" 1); by (asm_simp_tac (simpset() addsimps [oraclebuild_UU]) 1); by (rtac ForallQFilterPUU 1); by (REPEAT (atac 1)); @@ -93,7 +93,7 @@ (* ---------------------------------------------------------------- *) -Goal "Filter P`s = Filter P`(Cut P s)"; +Goal "Filter P$s = Filter P$(Cut P s)"; by (res_inst_tac [("A1","%x. True") ,("Q1","%x.~ P x"), ("x1","s")] @@ -128,7 +128,7 @@ qed"Cut_idemp"; -Goal "Map f`(Cut (P o f) s) = Cut P (Map f`s)"; +Goal "Map f$(Cut (P o f) s) = Cut P (Map f$s)"; by (res_inst_tac [("A1","%x. True") ,("Q1","%x.~ P (f x)"), ("x1","s")] @@ -200,13 +200,13 @@ Goalw [schedules_def,has_schedule_def] - "[|sch : schedules A ; tr = Filter (%a. a:ext A)`sch|] \ + "[|sch : schedules A ; tr = Filter (%a. a:ext A)$sch|] \ \ ==> ? sch. sch : schedules A & \ -\ tr = Filter (%a. a:ext A)`sch &\ +\ tr = Filter (%a. a:ext A)$sch &\ \ LastActExtsch A sch"; by (safe_tac set_cs); -by (res_inst_tac [("x","filter_act`(Cut (%a. fst a:ext A) (snd ex))")] exI 1); +by (res_inst_tac [("x","filter_act$(Cut (%a. fst a:ext A) (snd ex))")] exI 1); by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1); by (pair_tac "ex" 1); by (safe_tac set_cs); @@ -220,7 +220,7 @@ (* Subgoal 2: Lemma: Filter P s = Filter P (Cut P s) *) by (simp_tac (simpset() addsimps [filter_act_def]) 1); -by (subgoal_tac "Map fst`(Cut (%a. fst a: ext A) y)= Cut (%a. a:ext A) (Map fst`y)" 1); +by (subgoal_tac "Map fst$(Cut (%a. fst a: ext A) y)= Cut (%a. a:ext A) (Map fst$y)" 1); by (rtac (rewrite_rule [o_def] MapCut) 2); by (asm_full_simp_tac (simpset() addsimps [FilterCut RS sym]) 1); @@ -228,7 +228,7 @@ (* Subgoal 3: Lemma: Cut idempotent *) by (simp_tac (simpset() addsimps [LastActExtsch_def,filter_act_def]) 1); -by (subgoal_tac "Map fst`(Cut (%a. fst a: ext A) y)= Cut (%a. a:ext A) (Map fst`y)" 1); +by (subgoal_tac "Map fst$(Cut (%a. fst a: ext A) y)= Cut (%a. a:ext A) (Map fst$y)" 1); by (rtac (rewrite_rule [o_def] MapCut) 2); by (asm_full_simp_tac (simpset() addsimps [Cut_idemp]) 1); qed"exists_LastActExtsch"; @@ -239,7 +239,7 @@ (* ---------------------------------------------------------------- *) Goalw [LastActExtsch_def] - "[| LastActExtsch A sch; Filter (%x. x:ext A)`sch = nil |] \ + "[| LastActExtsch A sch; Filter (%x. x:ext A)$sch = nil |] \ \ ==> sch=nil"; by (dtac FilternPnilForallP 1); by (etac conjE 1); @@ -249,7 +249,7 @@ qed"LastActExtimplnil"; Goalw [LastActExtsch_def] - "[| LastActExtsch A sch; Filter (%x. x:ext A)`sch = UU |] \ + "[| LastActExtsch A sch; Filter (%x. x:ext A)$sch = UU |] \ \ ==> sch=UU"; by (dtac FilternPUUForallP 1); by (etac conjE 1); diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/ShortExecutions.thy --- a/src/HOLCF/IOA/meta_theory/ShortExecutions.thy Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.thy Tue Jan 09 15:36:30 2001 +0100 @@ -28,19 +28,19 @@ "LastActExtsch A sch == (Cut (%x. x: ext A) sch = sch)" (* LastActExtex_def - "LastActExtex A ex == LastActExtsch A (filter_act`ex)" *) + "LastActExtex A ex == LastActExtsch A (filter_act$ex)" *) Cut_def - "Cut P s == oraclebuild P`s`(Filter P`s)" + "Cut P s == oraclebuild P$s$(Filter P$s)" oraclebuild_def - "oraclebuild P == (fix`(LAM h s t. case t of + "oraclebuild P == (fix$(LAM h s t. case t of nil => nil | x##xs => (case x of Undef => UU - | Def y => (Takewhile (%x.~P x)`s) - @@ (y>>(h`(TL`(Dropwhile (%x.~ P x)`s))`xs)) + | Def y => (Takewhile (%x.~P x)$s) + @@ (y>>(h$(TL$(Dropwhile (%x.~ P x)$s))$xs)) ) ))" @@ -53,7 +53,7 @@ "Finite s ==> (? y. s = Cut P s @@ y)" LastActExtsmall1 - "LastActExtsch A sch ==> LastActExtsch A (TL`(Dropwhile P`sch))" + "LastActExtsch A sch ==> LastActExtsch A (TL$(Dropwhile P$sch))" LastActExtsmall2 "[| Finite sch1; LastActExtsch A (sch1 @@ sch2) |] ==> LastActExtsch A sch2" diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/SimCorrectness.ML --- a/src/HOLCF/IOA/meta_theory/SimCorrectness.ML Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.ML Tue Jan 09 15:36:30 2001 +0100 @@ -24,8 +24,8 @@ \ T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t' \ \ in \ \ (@cex. move A cex s a T') \ -\ @@ ((corresp_ex_simC A R `xs) T')) \ -\ `x) ))"; +\ @@ ((corresp_ex_simC A R $xs) T')) \ +\ $x) ))"; by (rtac trans 1); by (rtac fix_eq2 1); by (rtac corresp_ex_simC_def 1); @@ -33,21 +33,21 @@ by (simp_tac (simpset() addsimps [flift1_def]) 1); qed"corresp_ex_simC_unfold"; -Goal "(corresp_ex_simC A R`UU) s=UU"; +Goal "(corresp_ex_simC A R$UU) s=UU"; by (stac corresp_ex_simC_unfold 1); by (Simp_tac 1); qed"corresp_ex_simC_UU"; -Goal "(corresp_ex_simC A R`nil) s = nil"; +Goal "(corresp_ex_simC A R$nil) s = nil"; by (stac corresp_ex_simC_unfold 1); by (Simp_tac 1); qed"corresp_ex_simC_nil"; -Goal "(corresp_ex_simC A R`((a,t)>>xs)) s = \ +Goal "(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') \ -\ @@ ((corresp_ex_simC A R`xs) T'))"; +\ @@ ((corresp_ex_simC A R$xs) T'))"; by (rtac trans 1); by (stac corresp_ex_simC_unfold 1); by (asm_full_simp_tac (simpset() addsimps [Consq_def,flift1_def]) 1); @@ -128,7 +128,7 @@ Goal "[|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')) = \ +\ mk_trace A$((@x. move A x s' a T')) = \ \ (if a:ext A then a>>nil else nil)"; by (cut_inst_tac [] move_is_move_sim 1); by (REPEAT (assume_tac 1)); @@ -160,7 +160,7 @@ Goal "[|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')"; by (pair_induct_tac "ex" [is_exec_frag_def] 1); (* cons case *) @@ -190,7 +190,7 @@ Goal "[| 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')"; by (Asm_full_simp_tac 1); by (pair_induct_tac "ex" [is_exec_frag_def] 1); diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/SimCorrectness.thy --- a/src/HOLCF/IOA/meta_theory/SimCorrectness.thy Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.thy Tue Jan 09 15:36:30 2001 +0100 @@ -23,17 +23,17 @@ corresp_ex_sim_def "corresp_ex_sim A R ex == let S'= (@s'.(fst ex,s'):R & s': starts_of A) in - (S',(corresp_ex_simC A R`(snd ex)) S')" + (S',(corresp_ex_simC A R$(snd ex)) S')" corresp_ex_simC_def - "corresp_ex_simC A R == (fix`(LAM h ex. (%s. case ex of + "corresp_ex_simC A R == (fix$(LAM h ex. (%s. case ex of nil => nil | x##xs => (flift1 (%pr. let a = (fst pr); t = (snd pr); T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t' in (@cex. move A cex s a T') - @@ ((h`xs) T')) - `x) )))" + @@ ((h$xs) T')) + $x) )))" end \ No newline at end of file diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/Simulations.ML --- a/src/HOLCF/IOA/meta_theory/Simulations.ML Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/IOA/meta_theory/Simulations.ML Tue Jan 09 15:36:30 2001 +0100 @@ -19,7 +19,7 @@ Goalw [Image_def] -"(R```{x} Int S ~= {}) = (? y. (x,y):R & y:S)"; +"(R``{x} Int S ~= {}) = (? y. (x,y):R & y:S)"; by (simp_tac (simpset() addsimps [Int_non_empty]) 1); qed"Sim_start_convert"; diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/Simulations.thy --- a/src/HOLCF/IOA/meta_theory/Simulations.thy Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/IOA/meta_theory/Simulations.thy Tue Jan 09 15:36:30 2001 +0100 @@ -23,7 +23,7 @@ is_simulation_def "is_simulation R C A == - (!s:starts_of C. R```{s} Int starts_of A ~= {}) & + (!s:starts_of C. R``{s} Int starts_of A ~= {}) & (!s s' t a. reachable C s & s -a--C-> t & (s,s') : R @@ -31,7 +31,7 @@ is_backward_simulation_def "is_backward_simulation R C A == - (!s:starts_of C. R```{s} <= starts_of A) & + (!s:starts_of C. R``{s} <= starts_of A) & (!s t t' a. reachable C s & s -a--C-> t & (t,t') : R diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/TL.ML --- a/src/HOLCF/IOA/meta_theory/TL.ML Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/IOA/meta_theory/TL.ML Tue Jan 09 15:36:30 2001 +0100 @@ -106,7 +106,7 @@ Goalw [tsuffix_def,suffix_def] -"s~=UU & s~=nil --> tsuffix s2 (TL`s) --> tsuffix s2 s"; +"s~=UU & s~=nil --> tsuffix s2 (TL$s) --> tsuffix s2 s"; by Auto_tac; by (Seq_case_simp_tac "s" 1); by (res_inst_tac [("x","a>>s1")] exI 1); diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/TL.thy --- a/src/HOLCF/IOA/meta_theory/TL.thy Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/IOA/meta_theory/TL.thy Tue Jan 09 15:36:30 2001 +0100 @@ -50,7 +50,7 @@ (* this means that for nil and UU the effect is unpredictable *) Init_def - "Init P s == (P (unlift (HD`s)))" + "Init P s == (P (unlift (HD$s)))" suffix_def "suffix s2 s == ? s1. (Finite s1 & s = s1 @@ s2)" @@ -62,7 +62,7 @@ "([] P) s == ! s2. tsuffix s2 s --> P s2" Next_def - "(Next P) s == if (TL`s=UU | TL`s=nil) then (P s) else P (TL`s)" + "(Next P) s == if (TL$s=UU | TL$s=nil) then (P s) else P (TL$s)" Diamond_def "<> P == .~ ([] (.~ P))" diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/TLS.ML --- a/src/HOLCF/IOA/meta_theory/TLS.ML Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/IOA/meta_theory/TLS.ML Tue Jan 09 15:36:30 2001 +0100 @@ -20,8 +20,8 @@ Goal "ex2seqC = (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) \ +\ (s,Some (fst pr), snd pr)>> (ex2seqC$xs) (snd pr)) \ +\ $x) \ \ ))"; by (rtac trans 1); by (rtac fix_eq2 1); @@ -30,18 +30,18 @@ by (simp_tac (simpset() addsimps [flift1_def]) 1); qed"ex2seqC_unfold"; -Goal "(ex2seqC `UU) s=UU"; +Goal "(ex2seqC $UU) s=UU"; by (stac ex2seqC_unfold 1); by (Simp_tac 1); qed"ex2seqC_UU"; -Goal "(ex2seqC `nil) s = (s,None,s)>>nil"; +Goal "(ex2seqC $nil) s = (s,None,s)>>nil"; by (stac ex2seqC_unfold 1); by (Simp_tac 1); qed"ex2seqC_nil"; -Goal "(ex2seqC `((a,t)>>xs)) s = \ -\ (s,Some a,t)>> ((ex2seqC`xs) t)"; +Goal "(ex2seqC $((a,t)>>xs)) s = \ +\ (s,Some a,t)>> ((ex2seqC$xs) t)"; by (rtac trans 1); by (stac ex2seqC_unfold 1); by (asm_full_simp_tac (simpset() addsimps [Consq_def,flift1_def]) 1); diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/TLS.thy --- a/src/HOLCF/IOA/meta_theory/TLS.thy Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/IOA/meta_theory/TLS.thy Tue Jan 09 15:36:30 2001 +0100 @@ -60,14 +60,14 @@ "xt2 P tr == P (fst (snd tr))" ex2seq_def - "ex2seq ex == ((ex2seqC `(mkfin (snd ex))) (fst ex))" + "ex2seq ex == ((ex2seqC $(mkfin (snd ex))) (fst ex))" ex2seqC_def - "ex2seqC == (fix`(LAM h ex. (%s. case ex of + "ex2seqC == (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) + (s,Some (fst pr), snd pr)>> (h$xs) (snd pr)) + $x) )))" validTE_def diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/Traces.ML --- a/src/HOLCF/IOA/meta_theory/Traces.ML Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/IOA/meta_theory/Traces.ML Tue Jan 09 15:36:30 2001 +0100 @@ -26,15 +26,15 @@ (* ---------------------------------------------------------------- *) -Goal "filter_act`UU = UU"; +Goal "filter_act$UU = UU"; by (simp_tac (simpset() addsimps [filter_act_def]) 1); qed"filter_act_UU"; -Goal "filter_act`nil = nil"; +Goal "filter_act$nil = nil"; by (simp_tac (simpset() addsimps [filter_act_def]) 1); qed"filter_act_nil"; -Goal "filter_act`(x>>xs) = (fst x) >> filter_act`xs"; +Goal "filter_act$(x>>xs) = (fst x) >> filter_act$xs"; by (simp_tac (simpset() addsimps [filter_act_def]) 1); qed"filter_act_cons"; @@ -45,18 +45,18 @@ (* mk_trace *) (* ---------------------------------------------------------------- *) -Goal "mk_trace A`UU=UU"; +Goal "mk_trace A$UU=UU"; by (simp_tac (simpset() addsimps [mk_trace_def]) 1); qed"mk_trace_UU"; -Goal "mk_trace A`nil=nil"; +Goal "mk_trace A$nil=nil"; by (simp_tac (simpset() addsimps [mk_trace_def]) 1); qed"mk_trace_nil"; -Goal "mk_trace A`(at >> xs) = \ +Goal "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 (asm_full_simp_tac (simpset() addsimps [mk_trace_def]) 1); qed"mk_trace_cons"; @@ -71,8 +71,8 @@ Goal "is_exec_fragC A = (LAM ex. (%s. case ex of \ \ nil => TT \ \ | x##xs => (flift1 \ -\ (%p. Def ((s,p):trans_of A) andalso (is_exec_fragC A`xs) (snd p)) \ -\ `x) \ +\ (%p. Def ((s,p):trans_of A) andalso (is_exec_fragC A$xs) (snd p)) \ +\ $x) \ \ ))"; by (rtac trans 1); by (rtac fix_eq2 1); @@ -81,19 +81,19 @@ by (simp_tac (simpset() addsimps [flift1_def]) 1); qed"is_exec_fragC_unfold"; -Goal "(is_exec_fragC A`UU) s=UU"; +Goal "(is_exec_fragC A$UU) s=UU"; by (stac is_exec_fragC_unfold 1); by (Simp_tac 1); qed"is_exec_fragC_UU"; -Goal "(is_exec_fragC A`nil) s = TT"; +Goal "(is_exec_fragC A$nil) s = TT"; by (stac is_exec_fragC_unfold 1); by (Simp_tac 1); qed"is_exec_fragC_nil"; -Goal "(is_exec_fragC A`(pr>>xs)) s = \ +Goal "(is_exec_fragC A$(pr>>xs)) s = \ \ (Def ((s,pr):trans_of A) \ -\ andalso (is_exec_fragC A`xs)(snd pr))"; +\ andalso (is_exec_fragC A$xs)(snd pr))"; by (rtac trans 1); by (stac is_exec_fragC_unfold 1); by (asm_full_simp_tac (simpset() addsimps [Consq_def,flift1_def]) 1); @@ -163,7 +163,7 @@ take the detour of schedules *) Goalw [executions_def,mk_trace_def,has_trace_def,schedules_def,has_schedule_def] -"has_trace A b = (? ex:executions A. b = mk_trace A`(snd ex))"; +"has_trace A b = (? ex:executions A. b = mk_trace A$(snd ex))"; by (safe_tac set_cs); (* 1 *) @@ -173,7 +173,7 @@ by (Simp_tac 1); by (Asm_simp_tac 1); (* 2 *) -by (res_inst_tac[("x","filter_act`(snd ex)")] bexI 1); +by (res_inst_tac[("x","filter_act$(snd ex)")] bexI 1); by (stac beta_cfun 1); by (cont_tacR 1); by (Simp_tac 1); @@ -195,7 +195,7 @@ Goal "!! A. is_trans_of A ==> \ -\ ! s. is_exec_frag A (s,xs) --> Forall (%a. a:act A) (filter_act`xs)"; +\ ! s. is_exec_frag A (s,xs) --> Forall (%a. a:act A) (filter_act$xs)"; by (pair_induct_tac "xs" [is_exec_frag_def,Forall_def,sforall_def] 1); (* main case *) @@ -206,7 +206,7 @@ Goal "!! A.[| is_trans_of A; x:executions A |] ==> \ -\ Forall (%a. a:act A) (filter_act`(snd x))"; +\ Forall (%a. a:act A) (filter_act$(snd x))"; by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1); by (pair_tac "x" 1); diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/Traces.thy --- a/src/HOLCF/IOA/meta_theory/Traces.thy Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/IOA/meta_theory/Traces.thy Tue Jan 09 15:36:30 2001 +0100 @@ -74,15 +74,15 @@ is_exec_frag_def - "is_exec_frag A ex == ((is_exec_fragC A`(snd ex)) (fst ex) ~= FF)" + "is_exec_frag A ex == ((is_exec_fragC A$(snd ex)) (fst ex) ~= FF)" is_exec_fragC_def - "is_exec_fragC A ==(fix`(LAM h ex. (%s. case ex of + "is_exec_fragC A ==(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) + (%p. Def ((s,p):trans_of A) andalso (h$xs) (snd p)) + $x) )))" @@ -100,7 +100,7 @@ has_schedule_def "has_schedule ioa sch == - (? ex:executions ioa. sch = filter_act`(snd ex))" + (? ex:executions ioa. sch = filter_act$(snd ex))" schedules_def "schedules ioa == {sch. has_schedule ioa sch}" @@ -110,7 +110,7 @@ has_trace_def "has_trace ioa tr == - (? sch:schedules ioa. tr = Filter (%a. a:ext(ioa))`sch)" + (? sch:schedules ioa. tr = Filter (%a. a:ext(ioa))$sch)" traces_def "traces ioa == {tr. has_trace ioa tr}" @@ -118,18 +118,18 @@ mk_trace_def "mk_trace ioa == LAM tr. - Filter (%a. a:ext(ioa))`(filter_act`tr)" + Filter (%a. a:ext(ioa))$(filter_act$tr)" (* ------------------- Fair Traces ------------------------------ *) laststate_def - "laststate ex == case Last`(snd ex) of + "laststate ex == case Last$(snd ex) of Undef => fst ex | Def at => snd at" inf_often_def - "inf_often P s == Infinite (Filter P`s)" + "inf_often P s == Infinite (Filter P$s)" (* filtering P yields a finite or partial sequence *) fin_often_def @@ -166,7 +166,7 @@ "fairexecutions A == {ex. ex:executions A & fair_ex A ex}" fairtraces_def - "fairtraces A == {mk_trace A`(snd ex) | ex. ex:fairexecutions A}" + "fairtraces A == {mk_trace A$(snd ex) | ex. ex:fairexecutions A}" (* ------------------- Implementation ------------------------------ *) diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/domain/theorems.ML --- a/src/HOLCF/domain/theorems.ML Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/domain/theorems.ML Tue Jan 09 15:36:30 2001 +0100 @@ -451,7 +451,7 @@ asm_simp_tac take_ss 1 :: map (fn arg => case_UU_tac (prems@con_rews) 1 ( - nth_elem(rec_of arg,dnames)^"_take n`"^vname arg)) + nth_elem(rec_of arg,dnames)^"_take n$"^vname arg)) (filter is_nonlazy_rec args) @ [ resolve_tac prems 1] @ map (K (atac 1)) (nonlazy args) @ diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/ex/Dagstuhl.thy --- a/src/HOLCF/ex/Dagstuhl.thy Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/ex/Dagstuhl.thy Tue Jan 09 15:36:30 2001 +0100 @@ -10,8 +10,8 @@ defs -YS_def "YS == fix`(LAM x. y && x)" -YYS_def "YYS == fix`(LAM z. y && y && z)" +YS_def "YS == fix$(LAM x. y && x)" +YYS_def "YYS == fix$(LAM z. y && y && z)" end diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/ex/Dnat.ML --- a/src/HOLCF/ex/Dnat.ML Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/ex/Dnat.ML Tue Jan 09 15:36:30 2001 +0100 @@ -13,23 +13,23 @@ bind_thm ("iterator_def2", fix_prover2 Dnat.thy iterator_def "iterator = (LAM n f x. case n of dzero => x | \ -\ dsucc`m => f`(iterator`m`f`x))"); +\ dsucc$m => f$(iterator$m$f$x))"); (* ------------------------------------------------------------------------- *) (* recursive properties *) (* ------------------------------------------------------------------------- *) -Goal "iterator`UU`f`x = UU"; +Goal "iterator$UU$f$x = UU"; by (stac iterator_def2 1); by (simp_tac (HOLCF_ss addsimps dnat.rews) 1); qed "iterator1"; -Goal "iterator`dzero`f`x = x"; +Goal "iterator$dzero$f$x = x"; by (stac iterator_def2 1); by (simp_tac (HOLCF_ss addsimps dnat.rews) 1); qed "iterator2"; -Goal "n~=UU ==> iterator`(dsucc`n)`f`x = f`(iterator`n`f`x)"; +Goal "n~=UU ==> iterator$(dsucc$n)$f$x = f$(iterator$n$f$x)"; by (rtac trans 1); by (stac iterator_def2 1); by (asm_simp_tac (HOLCF_ss addsimps dnat.rews) 1); diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/ex/Dnat.thy --- a/src/HOLCF/ex/Dnat.thy Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/ex/Dnat.thy Tue Jan 09 15:36:30 2001 +0100 @@ -13,7 +13,7 @@ constdefs iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a" - "iterator == fix`(LAM h n f x . case n of dzero => x - | dsucc`m => f`(h`m`f`x))" + "iterator == fix$(LAM h n f x . case n of dzero => x + | dsucc$m => f$(h$m$f$x))" end diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/ex/Fix2.ML --- a/src/HOLCF/ex/Fix2.ML Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/ex/Fix2.ML Tue Jan 09 15:36:30 2001 +0100 @@ -14,7 +14,7 @@ qed "lemma1"; -Goal "gix`F=lub(range(%i. iterate i F UU))"; +Goal "gix$F=lub(range(%i. iterate i F UU))"; by (rtac (lemma1 RS subst) 1); by (rtac fix_def2 1); qed "lemma2"; diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/ex/Fix2.thy --- a/src/HOLCF/ex/Fix2.thy Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/ex/Fix2.thy Tue Jan 09 15:36:30 2001 +0100 @@ -16,7 +16,7 @@ rules -gix1_def "F`(gix`F) = gix`F" -gix2_def "F`y=y ==> gix`F << y" +gix1_def "F$(gix$F) = gix$F" +gix2_def "F$y=y ==> gix$F << y" end diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/ex/Focus_ex.ML --- a/src/HOLCF/ex/Focus_ex.ML Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/ex/Focus_ex.ML Tue Jan 09 15:36:30 2001 +0100 @@ -4,20 +4,20 @@ val prems = goal Focus_ex.thy "is_g(g) = \ -\ (? f. is_f(f) & (!x.(? z. = f` & \ -\ (! w y. = f` --> z << w))))"; +\ (? f. is_f(f) & (!x.(? z. = f$ & \ +\ (! w y. = f$ --> z << w))))"; by (simp_tac (HOL_ss addsimps [is_g,is_net_g]) 1); by (fast_tac HOL_cs 1); val lemma1 = result(); val prems = goal Focus_ex.thy -"(? f. is_f(f) & (!x. (? z. = f` & \ -\ (!w y. = f` --> z << w)))) \ +"(? f. is_f(f) & (!x. (? z. = f$ & \ +\ (!w y. = f$ --> z << w)))) \ \ = \ \ (? f. is_f(f) & (!x. ? z.\ -\ g`x = cfst`(f`) & \ -\ z = csnd`(f`) & \ -\ (! w y. = f` --> z << w)))"; +\ g$x = cfst$(f$) & \ +\ z = csnd$(f$) & \ +\ (! w y. = f$ --> z << w)))"; by (rtac iffI 1); by (etac exE 1); by (res_inst_tac [("x","f")] exI 1); @@ -63,7 +63,7 @@ by (REPEAT (etac conjE 1)); by (etac conjI 1); by (strip_tac 1); -by (res_inst_tac [("x","fix`(LAM k. csnd`(f`))")] exI 1); +by (res_inst_tac [("x","fix$(LAM k. csnd$(f$))")] exI 1); by (rtac conjI 1); by (asm_simp_tac HOLCF_ss 1); by (rtac trans 1); @@ -94,16 +94,16 @@ by (eres_inst_tac [("x","x")] allE 1); by (etac exE 1); by (REPEAT (etac conjE 1)); -by (subgoal_tac "fix`(LAM k. csnd`(f`)) = z" 1); +by (subgoal_tac "fix$(LAM k. csnd$(f$)) = z" 1); by (asm_simp_tac HOLCF_ss 1); -by (subgoal_tac "! w y. f` = --> z << w" 1); +by (subgoal_tac "! w y. f$ = --> z << w" 1); by (rtac sym 1); by (rtac fix_eqI 1); by (asm_simp_tac HOLCF_ss 1); by (rtac allI 1); by (simp_tac HOLCF_ss 1); by (strip_tac 1); -by (subgoal_tac "f` = ),za>" 1); +by (subgoal_tac "f$ = ),za>" 1); by (fast_tac HOL_cs 1); by (rtac trans 1); by (rtac (surjective_pairing_Cprod2 RS sym) 1); diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/ex/Focus_ex.thy --- a/src/HOLCF/ex/Focus_ex.thy Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/ex/Focus_ex.thy Tue Jan 09 15:36:30 2001 +0100 @@ -30,7 +30,7 @@ input channel x:'b output channel y:'c is network - = f` + = f$ end network end g @@ -47,7 +47,7 @@ 'c stream * ('b,'c) tc stream) => bool is_f f = !i1 i2 o1 o2. - f` = --> Rf(i1,i2,o1,o2) + f$ = --> Rf(i1,i2,o1,o2) Specification of agent g is translated to predicate is_g which uses predicate is_net_g @@ -56,13 +56,13 @@ 'b stream => 'c stream => bool is_net_g f x y = - ? z. = f` & - !oy hz. = f` --> z << hz + ? z. = f$ & + !oy hz. = f$ --> z << hz is_g :: ('b stream -> 'c stream) => bool -is_g g = ? f. is_f f & (!x y. g`x = y --> is_net_g f x y +is_g g = ? f. is_f f & (!x y. g$x = y --> is_net_g f x y Third step: (show conservativity) ----------- @@ -84,7 +84,7 @@ def_g g = (? f. is_f f & - g = (LAM x. cfst`(f`))>)) ) + g = (LAM x. cfst$(f$))>)) ) Now we prove: @@ -118,19 +118,19 @@ defs is_f "is_f f == (!i1 i2 o1 o2. - f` = --> Rf(i1,i2,o1,o2))" + f$ = --> Rf(i1,i2,o1,o2))" is_net_g "is_net_g f x y == (? z. - = f` & - (!oy hz. = f` --> z << hz))" + = f$ & + (!oy hz. = f$ --> z << hz))" is_g "is_g g == (? f. is_f f & - (!x y. g`x = y --> is_net_g f x y))" + (!x y. g$x = y --> is_net_g f x y))" def_g "def_g g == (? f. is_f f & - g = (LAM x. cfst`(f`))>)))" + g = (LAM x. cfst$(f$))>)))" end diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/ex/Hoare.ML --- a/src/HOLCF/ex/Hoare.ML Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/ex/Hoare.ML Tue Jan 09 15:36:30 2001 +0100 @@ -14,21 +14,21 @@ by (fast_tac HOL_cs 1); qed "hoare_lemma2"; -Goal " (ALL k. b1`(iterate k g x) = TT) | (EX k. b1`(iterate k g x)~=TT)"; +Goal " (ALL k. b1$(iterate k g x) = TT) | (EX k. b1$(iterate k g x)~=TT)"; by (fast_tac HOL_cs 1); qed "hoare_lemma3"; -Goal "(EX k. b1`(iterate k g x) ~= TT) ==> \ -\ EX k. b1`(iterate k g x) = FF | b1`(iterate k g x) = UU"; +Goal "(EX k. b1$(iterate k g x) ~= TT) ==> \ +\ EX k. b1$(iterate k g x) = FF | b1$(iterate k g x) = UU"; by (etac exE 1); by (rtac exI 1); by (rtac hoare_lemma2 1); by (atac 1); qed "hoare_lemma4"; -Goal "[|(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"; +Goal "[|(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"; by (hyp_subst_tac 1); by (rtac hoare_lemma2 1); by (etac exE 1); @@ -45,13 +45,13 @@ by (resolve_tac dist_eq_tr 1); qed "hoare_lemma7"; -Goal "[|(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"; +Goal "[|(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"; by (hyp_subst_tac 1); by (etac exE 1); by (strip_tac 1); -by (res_inst_tac [("p","b1`(iterate m g x)")] trE 1); +by (res_inst_tac [("p","b1$(iterate m g x)")] trE 1); by (atac 2); by (rtac (le_less_trans RS less_irrefl) 1); by (atac 2); @@ -64,7 +64,7 @@ qed "hoare_lemma8"; -Goal "f`(y::'a)=(UU::tr) ==> f`UU = UU"; +Goal "f$(y::'a)=(UU::tr) ==> f$UU = UU"; by (etac (flat_codom RS disjE) 1); by Auto_tac; qed "hoare_lemma28"; @@ -72,28 +72,28 @@ (* ----- access to definitions ----- *) -Goal "p`x = If b1`x then p`(g`x) else x fi"; +Goal "p$x = If b1$x then p$(g$x) else x fi"; by (fix_tac3 p_def 1); by (Simp_tac 1); qed "p_def3"; -Goal "q`x = If b1`x orelse b2`x then q`(g`x) else x fi"; +Goal "q$x = If b1$x orelse b2$x then q$(g$x) else x fi"; by (fix_tac3 q_def 1); by (Simp_tac 1); qed "q_def3"; (** --------- proves about iterations of p and q ---------- **) -Goal "(ALL m. m< Suc k --> b1`(iterate m g x)=TT) -->\ -\ p`(iterate k g x)=p`x"; +Goal "(ALL m. m< Suc k --> b1$(iterate m g x)=TT) -->\ +\ p$(iterate k g x)=p$x"; by (nat_ind_tac "k" 1); by (Simp_tac 1); by (Simp_tac 1); by (strip_tac 1); -by (res_inst_tac [("s","p`(iterate k g x)")] trans 1); +by (res_inst_tac [("s","p$(iterate k g x)")] trans 1); by (rtac trans 1); by (rtac (p_def3 RS sym) 2); -by (res_inst_tac [("s","TT"),("t","b1`(iterate k g x)")] ssubst 1); +by (res_inst_tac [("s","TT"),("t","b1$(iterate k g x)")] ssubst 1); by (rtac mp 1); by (etac spec 1); by (simp_tac (simpset() addsimps [less_Suc_eq]) 1); @@ -106,16 +106,16 @@ by (Simp_tac 1); qed "hoare_lemma9"; -Goal "(ALL m. m< Suc k --> b1`(iterate m g x)=TT) --> \ -\ q`(iterate k g x)=q`x"; +Goal "(ALL m. m< Suc k --> b1$(iterate m g x)=TT) --> \ +\ q$(iterate k g x)=q$x"; by (nat_ind_tac "k" 1); by (Simp_tac 1); by (simp_tac (simpset() addsimps [less_Suc_eq]) 1); by (strip_tac 1); -by (res_inst_tac [("s","q`(iterate k g x)")] trans 1); +by (res_inst_tac [("s","q$(iterate k g x)")] trans 1); by (rtac trans 1); by (rtac (q_def3 RS sym) 2); -by (res_inst_tac [("s","TT"),("t","b1`(iterate k g x)")] ssubst 1); +by (res_inst_tac [("s","TT"),("t","b1$(iterate k g x)")] ssubst 1); by (fast_tac HOL_cs 1); by (simp_tac HOLCF_ss 1); by (etac mp 1); @@ -123,20 +123,20 @@ by (fast_tac (HOL_cs addSDs [less_Suc_eq RS iffD1]) 1); qed "hoare_lemma24"; -(* -------- results about p for case (EX k. b1`(iterate k g x)~=TT) ------- *) +(* -------- results about p for case (EX k. b1$(iterate k g x)~=TT) ------- *) val hoare_lemma10 = (hoare_lemma8 RS (hoare_lemma9 RS mp)); (* -val hoare_lemma10 = "[| EX k. b1`(iterate k g ?x1) ~= TT; - Suc ?k3 = Least(%n. b1`(iterate n g ?x1) ~= TT) |] ==> - p`(iterate ?k3 g ?x1) = p`?x1" : thm +val hoare_lemma10 = "[| EX k. b1$(iterate k g ?x1) ~= TT; + Suc ?k3 = Least(%n. b1$(iterate n g ?x1) ~= TT) |] ==> + p$(iterate ?k3 g ?x1) = p$?x1" : thm *) -Goal "(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"; +Goal "(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"; by (case_tac "k" 1); by (hyp_subst_tac 1); by (Simp_tac 1); @@ -153,7 +153,7 @@ by (atac 1); by (rtac trans 1); by (rtac p_def3 1); -by (res_inst_tac [("s","TT"),("t","b1`(iterate nat g x)")] ssubst 1); +by (res_inst_tac [("s","TT"),("t","b1$(iterate nat g x)")] ssubst 1); by (rtac (hoare_lemma8 RS spec RS mp) 1); by (atac 1); by (atac 1); @@ -166,9 +166,9 @@ by (simp_tac HOLCF_ss 1); qed "hoare_lemma11"; -Goal "(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"; +Goal "(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"; by (case_tac "k" 1); by (hyp_subst_tac 1); by (Simp_tac 1); @@ -187,7 +187,7 @@ by (atac 1); by (rtac trans 1); by (rtac p_def3 1); -by (res_inst_tac [("s","TT"),("t","b1`(iterate nat g x)")] ssubst 1); +by (res_inst_tac [("s","TT"),("t","b1$(iterate nat g x)")] ssubst 1); by (rtac (hoare_lemma8 RS spec RS mp) 1); by (atac 1); by (atac 1); @@ -198,9 +198,9 @@ by (asm_simp_tac HOLCF_ss 1); qed "hoare_lemma12"; -(* -------- results about p for case (ALL k. b1`(iterate k g x)=TT) ------- *) +(* -------- results about p for case (ALL k. b1$(iterate k g x)=TT) ------- *) -Goal "(ALL k. b1`(iterate k g x)=TT) ==> ALL k. p`(iterate k g x) = UU"; +Goal "(ALL k. b1$(iterate k g x)=TT) ==> ALL k. p$(iterate k g x) = UU"; by (rtac (p_def RS def_fix_ind) 1); by (rtac adm_all 1); by (rtac allI 1); @@ -211,21 +211,21 @@ by (rtac refl 1); by (Simp_tac 1); by (rtac allI 1); -by (res_inst_tac [("s","TT"),("t","b1`(iterate k g x)")] ssubst 1); +by (res_inst_tac [("s","TT"),("t","b1$(iterate k g x)")] ssubst 1); by (etac spec 1); by (asm_simp_tac HOLCF_ss 1); by (rtac (iterate_Suc RS subst) 1); by (etac spec 1); qed "fernpass_lemma"; -Goal "(ALL k. b1`(iterate k g x)=TT) ==> p`x = UU"; +Goal "(ALL k. b1$(iterate k g x)=TT) ==> p$x = UU"; by (res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1); by (etac (fernpass_lemma RS spec) 1); qed "hoare_lemma16"; -(* -------- results about q for case (ALL k. b1`(iterate k g x)=TT) ------- *) +(* -------- results about q for case (ALL k. b1$(iterate k g x)=TT) ------- *) -Goal "(ALL k. b1`(iterate k g x)=TT) ==> ALL k. q`(iterate k g x) = UU"; +Goal "(ALL k. b1$(iterate k g x)=TT) ==> ALL k. q$(iterate k g x) = UU"; by (rtac (q_def RS def_fix_ind) 1); by (rtac adm_all 1); by (rtac allI 1); @@ -236,25 +236,25 @@ by (rtac refl 1); by (rtac allI 1); by (Simp_tac 1); -by (res_inst_tac [("s","TT"),("t","b1`(iterate k g x)")] ssubst 1); +by (res_inst_tac [("s","TT"),("t","b1$(iterate k g x)")] ssubst 1); by (etac spec 1); by (asm_simp_tac HOLCF_ss 1); by (rtac (iterate_Suc RS subst) 1); by (etac spec 1); qed "hoare_lemma17"; -Goal "(ALL k. b1`(iterate k g x)=TT) ==> q`x = UU"; +Goal "(ALL k. b1$(iterate k g x)=TT) ==> q$x = UU"; by (res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1); by (etac (hoare_lemma17 RS spec) 1); qed "hoare_lemma18"; -Goal "(ALL k. (b1::'a->tr)`(iterate k g x)=TT) ==> b1`(UU::'a) = UU | (ALL y. b1`(y::'a)=TT)"; +Goal "(ALL k. (b1::'a->tr)$(iterate k g x)=TT) ==> b1$(UU::'a) = UU | (ALL y. b1$(y::'a)=TT)"; by (rtac (flat_codom) 1); by (res_inst_tac [("t","x1")] (iterate_0 RS subst) 1); by (etac spec 1); qed "hoare_lemma19"; -Goal "(ALL y. b1`(y::'a)=TT) ==> ALL k. q`(iterate k g (x::'a)) = UU"; +Goal "(ALL y. b1$(y::'a)=TT) ==> ALL k. q$(iterate k g (x::'a)) = UU"; by (rtac (q_def RS def_fix_ind) 1); by (rtac adm_all 1); by (rtac allI 1); @@ -265,35 +265,35 @@ by (rtac refl 1); by (rtac allI 1); by (Simp_tac 1); -by (res_inst_tac [("s","TT"),("t","b1`(iterate k g (x::'a))")] ssubst 1); +by (res_inst_tac [("s","TT"),("t","b1$(iterate k g (x::'a))")] ssubst 1); by (etac spec 1); by (asm_simp_tac HOLCF_ss 1); by (rtac (iterate_Suc RS subst) 1); by (etac spec 1); qed "hoare_lemma20"; -Goal "(ALL y. b1`(y::'a)=TT) ==> q`(x::'a) = UU"; +Goal "(ALL y. b1$(y::'a)=TT) ==> q$(x::'a) = UU"; by (res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1); by (etac (hoare_lemma20 RS spec) 1); qed "hoare_lemma21"; -Goal "b1`(UU::'a)=UU ==> q`(UU::'a) = UU"; +Goal "b1$(UU::'a)=UU ==> q$(UU::'a) = UU"; by (stac q_def3 1); by (asm_simp_tac HOLCF_ss 1); qed "hoare_lemma22"; -(* -------- results about q for case (EX k. b1`(iterate k g x) ~= TT) ------- *) +(* -------- results about q for case (EX k. b1$(iterate k g x) ~= TT) ------- *) val hoare_lemma25 = (hoare_lemma8 RS (hoare_lemma24 RS mp) ); (* -val hoare_lemma25 = "[| EX k. b1`(iterate k g ?x1) ~= TT; - Suc ?k3 = Least(%n. b1`(iterate n g ?x1) ~= TT) |] ==> - q`(iterate ?k3 g ?x1) = q`?x1" : thm +val hoare_lemma25 = "[| EX k. b1$(iterate k g ?x1) ~= TT; + Suc ?k3 = Least(%n. b1$(iterate n g ?x1) ~= TT) |] ==> + q$(iterate ?k3 g ?x1) = q$?x1" : thm *) -Goal "(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)"; +Goal "(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)"; by (case_tac "k" 1); by (hyp_subst_tac 1); by (strip_tac 1); @@ -307,7 +307,7 @@ by (atac 1); by (rtac trans 1); by (rtac q_def3 1); -by (res_inst_tac [("s","TT"),("t","b1`(iterate nat g x)")] ssubst 1); +by (res_inst_tac [("s","TT"),("t","b1$(iterate nat g x)")] ssubst 1); by (rtac (hoare_lemma8 RS spec RS mp) 1); by (atac 1); by (atac 1); @@ -316,9 +316,9 @@ qed "hoare_lemma26"; -Goal "(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"; +Goal "(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"; by (case_tac "k" 1); by (hyp_subst_tac 1); by (Simp_tac 1); @@ -336,7 +336,7 @@ by (atac 1); by (rtac trans 1); by (rtac q_def3 1); -by (res_inst_tac [("s","TT"),("t","b1`(iterate nat g x)")] ssubst 1); +by (res_inst_tac [("s","TT"),("t","b1$(iterate nat g x)")] ssubst 1); by (rtac (hoare_lemma8 RS spec RS mp) 1); by (atac 1); by (atac 1); @@ -347,9 +347,9 @@ by (asm_simp_tac HOLCF_ss 1); qed "hoare_lemma27"; -(* ------- (ALL k. b1`(iterate k g x)=TT) ==> q o p = q ----- *) +(* ------- (ALL k. b1$(iterate k g x)=TT) ==> q o p = q ----- *) -Goal "(ALL k. b1`(iterate k g x)=TT) ==> q`(p`x) = q`x"; +Goal "(ALL k. b1$(iterate k g x)=TT) ==> q$(p$x) = q$x"; by (stac hoare_lemma16 1); by (atac 1); by (rtac (hoare_lemma19 RS disjE) 1); @@ -368,7 +368,7 @@ (* ------------ EX k. b1~(iterate k g x) ~= TT ==> q o p = q ----- *) -Goal "EX k. b1`(iterate k g x) ~= TT ==> q`(p`x) = q`x"; +Goal "EX k. b1$(iterate k g x) ~= TT ==> q$(p$x) = q$x"; by (rtac (hoare_lemma5 RS disjE) 1); by (atac 1); by (rtac refl 1); diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/ex/Hoare.thy --- a/src/HOLCF/ex/Hoare.thy Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/ex/Hoare.thy Tue Jan 09 15:36:30 2001 +0100 @@ -32,11 +32,11 @@ defs - p_def "p == fix`(LAM f. LAM x. - If b1`x then f`(g`x) else x fi)" + p_def "p == fix$(LAM f. LAM x. + If b1$x then f$(g$x) else x fi)" - q_def "q == fix`(LAM f. LAM x. - If b1`x orelse b2`x then f`(g`x) else x fi)" + q_def "q == fix$(LAM f. LAM x. + If b1$x orelse b2$x then f$(g$x) else x fi)" end diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/ex/Loop.ML --- a/src/HOLCF/ex/Loop.ML Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/ex/Loop.ML Tue Jan 09 15:36:30 2001 +0100 @@ -11,11 +11,11 @@ (* ------------------------------------------------------------------------- *) -Goalw [step_def] "step`b`g`x = If b`x then g`x else x fi"; +Goalw [step_def] "step$b$g$x = If b$x then g$x else x fi"; by (Simp_tac 1); qed "step_def2"; -Goalw [while_def] "while`b`g = fix`(LAM f x. If b`x then f`(g`x) else x fi)"; +Goalw [while_def] "while$b$g = fix$(LAM f x. If b$x then f$(g$x) else x fi)"; by (Simp_tac 1); qed "while_def2"; @@ -24,12 +24,12 @@ (* rekursive properties of while *) (* ------------------------------------------------------------------------- *) -Goal "while`b`g`x = If b`x then while`b`g`(g`x) else x fi"; +Goal "while$b$g$x = If b$x then while$b$g$(g$x) else x fi"; by (fix_tac5 while_def2 1); by (Simp_tac 1); qed "while_unfold"; -Goal "ALL x. while`b`g`x = while`b`g`(iterate k (step`b`g) x)"; +Goal "ALL x. while$b$g$x = while$b$g$(iterate k (step$b$g) x)"; by (nat_ind_tac "k" 1); by (simp_tac HOLCF_ss 1); by (rtac allI 1); @@ -40,10 +40,10 @@ by (rtac trans 1); by (etac spec 2); by (stac step_def2 1); -by (res_inst_tac [("p","b`x")] trE 1); +by (res_inst_tac [("p","b$x")] trE 1); by (asm_simp_tac HOLCF_ss 1); by (stac while_unfold 1); -by (res_inst_tac [("s","UU"),("t","b`UU")]ssubst 1); +by (res_inst_tac [("s","UU"),("t","b$UU")]ssubst 1); by (etac (flat_codom RS disjE) 1); by (atac 1); by (etac spec 1); @@ -54,8 +54,8 @@ by (asm_simp_tac HOLCF_ss 1); qed "while_unfold2"; -Goal "while`b`g`x = while`b`g`(step`b`g`x)"; -by (res_inst_tac [("s", "while`b`g`(iterate (Suc 0) (step`b`g) x)")] trans 1); +Goal "while$b$g$x = while$b$g$(step$b$g$x)"; +by (res_inst_tac [("s", "while$b$g$(iterate (Suc 0) (step$b$g) x)")] trans 1); by (rtac (while_unfold2 RS spec) 1); by (Simp_tac 1); qed "while_unfold3"; @@ -65,8 +65,8 @@ (* properties of while and iterations *) (* ------------------------------------------------------------------------- *) -Goal "[| EX y. b`y=FF; iterate k (step`b`g) x = UU |] \ -\ ==>iterate(Suc k) (step`b`g) x=UU"; +Goal "[| EX y. b$y=FF; iterate k (step$b$g) x = UU |] \ +\ ==>iterate(Suc k) (step$b$g) x=UU"; by (Simp_tac 1); by (rtac trans 1); by (rtac step_def2 1); @@ -77,34 +77,34 @@ by (asm_simp_tac HOLCF_ss 1); qed "loop_lemma1"; -Goal "[|EX y. b`y=FF;iterate (Suc k) (step`b`g) x ~=UU |]==>\ -\ iterate k (step`b`g) x ~=UU"; +Goal "[|EX y. b$y=FF;iterate (Suc k) (step$b$g) x ~=UU |]==>\ +\ iterate k (step$b$g) x ~=UU"; by (blast_tac (claset() addIs [loop_lemma1]) 1); qed "loop_lemma2"; -Goal "[| 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)"; +Goal "[| 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)"; by (nat_ind_tac "k" 1); by (Asm_simp_tac 1); by (strip_tac 1); by (simp_tac (simpset() addsimps [step_def2]) 1); -by (res_inst_tac [("p","b`(iterate k (step`b`g) x)")] trE 1); +by (res_inst_tac [("p","b$(iterate k (step$b$g) x)")] trE 1); by (etac notE 1); by (asm_simp_tac (HOLCF_ss addsimps [step_def2] ) 1); by (asm_simp_tac HOLCF_ss 1); by (rtac mp 1); by (etac spec 1); by (asm_simp_tac (HOLCF_ss delsimps [iterate_Suc] addsimps [loop_lemma2] ) 1); -by (res_inst_tac [("s","iterate (Suc k) (step`b`g) x"), - ("t","g`(iterate k (step`b`g) x)")] ssubst 1); +by (res_inst_tac [("s","iterate (Suc k) (step$b$g) x"), + ("t","g$(iterate k (step$b$g) x)")] ssubst 1); by (atac 2); by (asm_simp_tac (HOLCF_ss addsimps [step_def2] ) 1); by (asm_simp_tac (HOLCF_ss delsimps [iterate_Suc] addsimps [loop_lemma2] ) 1); qed_spec_mp "loop_lemma3"; -Goal "ALL x. b`(iterate k (step`b`g) x)=FF --> while`b`g`x= iterate k (step`b`g) x"; +Goal "ALL x. b$(iterate k (step$b$g) x)=FF --> while$b$g$x= iterate k (step$b$g) x"; by (nat_ind_tac "k" 1); by (Simp_tac 1); by (strip_tac 1); @@ -118,8 +118,8 @@ by (Asm_simp_tac 1); qed_spec_mp "loop_lemma4"; -Goal "ALL k. b`(iterate k (step`b`g) x) ~= FF ==>\ -\ ALL m. while`b`g`(iterate m (step`b`g) x)=UU"; +Goal "ALL k. b$(iterate k (step$b$g) x) ~= FF ==>\ +\ ALL m. while$b$g$(iterate m (step$b$g) x)=UU"; by (stac while_def2 1); by (rtac fix_ind 1); by (rtac (allI RS adm_all) 1); @@ -128,10 +128,10 @@ by (Simp_tac 1); by (rtac allI 1); by (Simp_tac 1); -by (res_inst_tac [("p","b`(iterate m (step`b`g) x)")] trE 1); +by (res_inst_tac [("p","b$(iterate m (step$b$g) x)")] trE 1); by (Asm_simp_tac 1); by (Asm_simp_tac 1); -by (res_inst_tac [("s","xa`(iterate (Suc m) (step`b`g) x)")] trans 1); +by (res_inst_tac [("s","xa$(iterate (Suc m) (step$b$g) x)")] trans 1); by (etac spec 2); by (rtac cfun_arg_cong 1); by (rtac trans 1); @@ -141,12 +141,12 @@ qed_spec_mp "loop_lemma5"; -Goal "ALL k. b`(iterate k (step`b`g) x) ~= FF ==> while`b`g`x=UU"; +Goal "ALL k. b$(iterate k (step$b$g) x) ~= FF ==> while$b$g$x=UU"; by (res_inst_tac [("t","x")] (iterate_0 RS subst) 1); by (etac (loop_lemma5) 1); qed "loop_lemma6"; -Goal "while`b`g`x ~= UU ==> EX k. b`(iterate k (step`b`g) x) = FF"; +Goal "while$b$g$x ~= UU ==> EX k. b$(iterate k (step$b$g) x) = FF"; by (blast_tac (claset() addIs [loop_lemma6]) 1); qed "loop_lemma7"; @@ -156,10 +156,10 @@ (* ------------------------------------------------------------------------- *) Goal -"[| (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)"; -by (res_inst_tac [("P","%k. b`(iterate k (step`b`g) x)=FF")] exE 1); +"[| (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)"; +by (res_inst_tac [("P","%k. b$(iterate k (step$b$g) x)=FF")] exE 1); by (etac loop_lemma7 1); by (stac (loop_lemma4) 1); by (atac 1); @@ -177,9 +177,9 @@ val [premP,premI,premTT,premFF,premW] = Goal "[| P(x); \ \ !!y. P y ==> INV y;\ -\ !!y. [| INV y; b`y=TT; g`y~=UU|] ==> INV (g`y);\ -\ !!y. [| INV y; b`y=FF|] ==> Q y;\ -\ while`b`g`x ~= UU |] ==> Q (while`b`g`x)"; +\ !!y. [| INV y; b$y=TT; g$y~=UU|] ==> INV (g$y);\ +\ !!y. [| INV y; b$y=FF|] ==> Q y;\ +\ while$b$g$x ~= UU |] ==> Q (while$b$g$x)"; by (rtac loop_inv2 1); by (rtac (premP RS premI) 3); by (rtac premW 3); diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/ex/Loop.thy --- a/src/HOLCF/ex/Loop.thy Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/ex/Loop.thy Tue Jan 09 15:36:30 2001 +0100 @@ -14,9 +14,9 @@ defs - step_def "step == (LAM b g x. If b`x then g`x else x fi)" - while_def "while == (LAM b g. fix`(LAM f x. - If b`x then f`(g`x) else x fi))" + step_def "step == (LAM b g x. If b$x then g$x else x fi)" + while_def "while == (LAM b g. fix$(LAM f x. + If b$x then f$(g$x) else x fi))" end diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/ex/Stream.ML --- a/src/HOLCF/ex/Stream.ML Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/ex/Stream.ML Tue Jan 09 15:36:30 2001 +0100 @@ -74,7 +74,7 @@ section "stream_when"; -Goal "stream_when`UU`s=UU"; +Goal "stream_when$UU$s=UU"; by (stream_case_tac "s" 1); by (ALLGOALS(asm_simp_tac (simpset() addsimps [strict_Rep_CFun1]))); qed "stream_when_strictf"; @@ -87,23 +87,23 @@ section "ft & rt"; (* -Goal "ft`s=UU --> s=UU"; +Goal "ft$s=UU --> s=UU"; by (stream_case_tac "s" 1); by (REPEAT (asm_simp_tac (simpset() addsimps stream.rews) 1)); qed "stream_ft_lemma1"; *) -Goal "s~=UU ==> ft`s~=UU"; +Goal "s~=UU ==> ft$s~=UU"; by (stream_case_tac "s" 1); by (Blast_tac 1); by (asm_simp_tac (simpset() addsimps stream.rews) 1); qed "ft_defin"; -Goal "rt`s~=UU ==> s~=UU"; +Goal "rt$s~=UU ==> s~=UU"; by Auto_tac; qed "rt_strict_rev"; -Goal "(ft`s)&&(rt`s)=s"; +Goal "(ft$s)&&(rt$s)=s"; by (stream_case_tac "s" 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps stream.rews))); qed "surjectiv_scons"; @@ -127,16 +127,16 @@ section "stream_take"; -Goal "(LUB i. stream_take i`s) = s"; -by (subgoal_tac "(LUB i. stream_take i`s) = fix`stream_copy`s" 1); +Goal "(LUB i. stream_take i$s) = s"; +by (subgoal_tac "(LUB i. stream_take i$s) = fix$stream_copy$s" 1); by (simp_tac (simpset() addsimps [fix_def2, stream.take_def, contlub_cfun_fun, chain_iterate]) 2); by (asm_full_simp_tac (simpset() addsimps [stream.reach]) 1); qed "stream_reach2"; -Goal "chain (%i. stream_take i`s)"; +Goal "chain (%i. stream_take i$s)"; by (rtac chainI 1); -by (subgoal_tac "ALL i s. stream_take i`s << stream_take (Suc i)`s" 1); +by (subgoal_tac "ALL i s. stream_take i$s << stream_take (Suc i)$s" 1); by (Fast_tac 1); by (rtac allI 1); by (induct_tac "ia" 1); @@ -149,9 +149,9 @@ Goalw [stream.take_def] - "stream_take n`x = x ==> stream_take (Suc n)`x = x"; + "stream_take n$x = x ==> stream_take (Suc n)$x = x"; by (rtac antisym_less 1); -by (subgoal_tac "iterate (Suc n) stream_copy UU`x << fix`stream_copy`x" 1); +by (subgoal_tac "iterate (Suc n) stream_copy UU$x << fix$stream_copy$x" 1); by (asm_full_simp_tac (simpset() addsimps [stream.reach]) 1); by (rtac monofun_cfun_fun 1); by (stac fix_def2 1); @@ -163,7 +163,7 @@ (* Goal - "ALL s2. stream_take n`s2 = s2 --> stream_take (Suc n)`s2=s2"; + "ALL s2. stream_take n$s2 = s2 --> stream_take (Suc n)$s2=s2"; by (induct_tac "n" 1); by (simp_tac (simpset() addsimps stream_rews) 1); by (strip_tac 1); @@ -174,7 +174,7 @@ by (asm_simp_tac (simpset() addsimps stream_rews) 1); by (asm_simp_tac (simpset() addsimps stream_rews) 1); by (strip_tac 1 ); -by (subgoal_tac "stream_take n1`xs = xs" 1); +by (subgoal_tac "stream_take n1$xs = xs" 1); by (rtac ((hd stream_inject) RS conjunct2) 2); by (atac 4); by (atac 2); @@ -185,7 +185,7 @@ *) Goal - "ALL x xs. x~=UU --> stream_take n`(x && xs) = x && xs --> stream_take n`xs=xs"; + "ALL x xs. x~=UU --> stream_take n$(x && xs) = x && xs --> stream_take n$xs=xs"; by (induct_tac "n" 1); by (Asm_simp_tac 1); by (strip_tac 1); @@ -201,7 +201,7 @@ qed_spec_mp "stream_take_lemma3"; Goal - "ALL x xs. stream_take n`xs=xs --> stream_take (Suc n)`(x && xs) = x && xs"; + "ALL x xs. stream_take n$xs=xs --> stream_take (Suc n)$(x && xs) = x && xs"; by (induct_tac "n" 1); by Auto_tac; qed_spec_mp "stream_take_lemma4"; @@ -232,7 +232,7 @@ "[| 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)"; +\ |] ==> !s. P (stream_take n$s)"; by (res_inst_tac [("n","n")] nat_induct2 1); by (asm_simp_tac (simpset() addsimps [major]) 1); by (rtac allI 1); @@ -275,7 +275,7 @@ Goalw [stream.bisim_def] -"!s1 s2. R s1 s2 --> ft`s1 = ft`s2 & R (rt`s1) (rt`s2) ==> stream_bisim R"; +"!s1 s2. R s1 s2 --> ft$s1 = ft$s2 & R (rt$s1) (rt$s2) ==> stream_bisim R"; by (strip_tac 1); by (etac allE 1); by (etac allE 1); @@ -288,21 +288,21 @@ by (rtac disjI2 1); by (rtac disjE 1); by (etac (de_Morgan_conj RS subst) 1); -by (res_inst_tac [("x","ft`x")] exI 1); -by (res_inst_tac [("x","rt`x")] exI 1); -by (res_inst_tac [("x","rt`x'")] exI 1); +by (res_inst_tac [("x","ft$x")] exI 1); +by (res_inst_tac [("x","rt$x")] exI 1); +by (res_inst_tac [("x","rt$x'")] exI 1); by (rtac conjI 1); by (etac ft_defin 1); by (asm_simp_tac (simpset() addsimps stream.rews addsimps [surjectiv_scons]) 1); -by (eres_inst_tac [("s","ft`x"),("t","ft`x'")] subst 1); +by (eres_inst_tac [("s","ft$x"),("t","ft$x'")] subst 1); by (simp_tac (simpset() addsimps stream.rews addsimps [surjectiv_scons]) 1); -by (res_inst_tac [("x","ft`x'")] exI 1); -by (res_inst_tac [("x","rt`x")] exI 1); -by (res_inst_tac [("x","rt`x'")] exI 1); +by (res_inst_tac [("x","ft$x'")] exI 1); +by (res_inst_tac [("x","rt$x")] exI 1); +by (res_inst_tac [("x","rt$x'")] exI 1); by (rtac conjI 1); by (etac ft_defin 1); by (asm_simp_tac (simpset() addsimps stream.rews addsimps [surjectiv_scons]) 1); -by (res_inst_tac [("s","ft`x"),("t","ft`x'")] ssubst 1); +by (res_inst_tac [("s","ft$x"),("t","ft$x'")] ssubst 1); by (etac sym 1); by (simp_tac (simpset() addsimps stream.rews addsimps [surjectiv_scons]) 1); qed "stream_coind_lemma2"; @@ -332,7 +332,7 @@ by (blast_tac (claset() addIs [stream_take_lemma3]) 1); qed "stream_finite_lemma2"; -Goal "stream_finite (rt`s) = stream_finite s"; +Goal "stream_finite (rt$s) = stream_finite s"; by (stream_case_tac "s" 1); by (simp_tac (simpset() addsimps [stream_finite_UU]) 1); by (Asm_simp_tac 1); diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/ex/loeckx.ML --- a/src/HOLCF/ex/loeckx.ML Tue Jan 09 15:32:27 2001 +0100 +++ b/src/HOLCF/ex/loeckx.ML Tue Jan 09 15:36:30 2001 +0100 @@ -19,16 +19,16 @@ Since we already proved the theorem val cont_lubcfun = prove_goal Cfun2.thy - "chain ?F ==> cont (%x. lub (range (%j. ?F j`x)))" + "chain ?F ==> cont (%x. lub (range (%j. ?F j$x)))" it suffices to prove: -Ifix = (%f.lub (range (%j. (LAM f. iterate j f UU)`f))) +Ifix = (%f.lub (range (%j. (LAM f. iterate j f UU)$f))) and -cont (%f.lub (range (%j. (LAM f. iterate j f UU)`f))) +cont (%f.lub (range (%j. (LAM f. iterate j f UU)$f))) Note that if we use the term @@ -40,15 +40,15 @@ Goal "cont(Ifix)"; by (res_inst_tac - [("t","Ifix"),("s","(%f. lub(range(%j.(LAM f. iterate j f UU)`f)))")] + [("t","Ifix"),("s","(%f. lub(range(%j.(LAM f. iterate j f UU)$f)))")] ssubst 1); by (rtac ext 1); by (rewtac Ifix_def ); by (subgoal_tac - "range(% i. iterate i f UU) = range(%j.(LAM f. iterate j f UU)`f)" 1); + "range(% i. iterate i f UU) = range(%j.(LAM f. iterate j f UU)$f)" 1); by (etac arg_cong 1); by (subgoal_tac - "(% i. iterate i f UU) = (%j.(LAM f. iterate j f UU)`f)" 1); + "(% i. iterate i f UU) = (%j.(LAM f. iterate j f UU)$f)" 1); by (etac arg_cong 1); by (rtac ext 1); by (stac beta_cfun 1); @@ -70,19 +70,19 @@ (* the proof in little steps *) -Goal "(% i. iterate i f UU) = (%j.(LAM f. iterate j f UU)`f)"; +Goal "(% i. iterate i f UU) = (%j.(LAM f. iterate j f UU)$f)"; by (rtac ext 1); by (simp_tac (simpset() addsimps [beta_cfun, cont2cont_CF1L, cont_iterate]) 1); qed "fix_lemma1"; -Goal "Ifix = (%f. lub(range(%j.(LAM f. iterate j f UU)`f)))"; +Goal "Ifix = (%f. lub(range(%j.(LAM f. iterate j f UU)$f)))"; by (rtac ext 1); by (simp_tac (simpset() addsimps [Ifix_def, fix_lemma1]) 1); qed "fix_lemma2"; (* - cont_lubcfun; -val it = "chain ?F ==> cont (%x. lub (range (%j. ?F j`x)))" : thm +val it = "chain ?F ==> cont (%x. lub (range (%j. ?F j$x)))" : thm *)