--- 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,s> -c-> t ==> D c`(Discr s) = (Def t)";
+Goal "<c,s> -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,s> -c-> t";
+Goal "!s t. D c$(Discr s) = (Def t) --> <c,s> -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,s> -c-> t)";
+Goal "(D c$(Discr s) = (Def t)) = (<c,s> -c-> t)";
by (fast_tac (claset() addSEs [D_implies_eval,eval_implies_D]) 1);
qed "D_is_eval";
--- 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
--- 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
--- 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);
--- 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"
--- 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)";
--- 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
--- 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);
--- 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)"
--- 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);
--- 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"
--- 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);
--- 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);
--- 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)) &
--- 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 *)
--- 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 ==
--- 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 ==
--- 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 => <x,y>##(szip`xs`ys)))");
+\ | y##ys => <x,y>##(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) = <x,y>##szip`xs`ys";
+Goal "[| x~=UU; y~=UU|] ==> szip$(x##xs)$(y##ys) = <x,y>##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),
--- 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 => <x,y>##(h`xs`ys))))"
+ | y##ys => <x,y>##(h$xs$ys))))"
Partial_def
"Partial x == (seq_finite x) & ~(Finite x)"
--- 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<n ==> 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<n ==> 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<n ==> 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<n ==> 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<<s2";
+"(!! n. seq_take n$s1 << seq_take n$s2) ==> s1<<s2";
by (res_inst_tac [("t","s1")] (seq.reach RS subst) 1);
by (res_inst_tac [("t","s2")] (seq.reach RS subst) 1);
@@ -910,7 +910,7 @@
qed"take_lemma_less1";
-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 (rtac take_lemma_less1 1);
by Auto_tac;
@@ -931,8 +931,8 @@
Goal "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \
\ !! s1 s2 y. [| Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2)|] \
-\ ==> ! n. seq_take n`(f (s1 @@ y>>s2)) \
-\ = seq_take n`(g (s1 @@ y>>s2)) |] \
+\ ==> ! 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;
--- 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
--- 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);
--- 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"
--- 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);
--- 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
--- 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";
--- 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
--- 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);
--- 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))"
--- 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);
--- 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
--- 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);
--- 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 ------------------------------ *)
--- 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) @
--- 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
--- 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);
--- 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
--- 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";
--- 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
--- 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. <g`x,z> = f`<x,z> & \
-\ (! w y. <y,w> = f`<x,w> --> z << w))))";
+\ (? f. is_f(f) & (!x.(? z. <g$x,z> = f$<x,z> & \
+\ (! w y. <y,w> = f$<x,w> --> z << w))))";
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. <g`x,z> = f`<x,z> & \
-\ (!w y. <y,w> = f`<x,w> --> z << w)))) \
+"(? f. is_f(f) & (!x. (? z. <g$x,z> = f$<x,z> & \
+\ (!w y. <y,w> = f$<x,w> --> z << w)))) \
\ = \
\ (? f. is_f(f) & (!x. ? z.\
-\ g`x = cfst`(f`<x,z>) & \
-\ z = csnd`(f`<x,z>) & \
-\ (! w y. <y,w> = f`<x,w> --> z << w)))";
+\ g$x = cfst$(f$<x,z>) & \
+\ z = csnd$(f$<x,z>) & \
+\ (! w y. <y,w> = f$<x,w> --> 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`<x,k>))")] exI 1);
+by (res_inst_tac [("x","fix$(LAM k. csnd$(f$<x,k>))")] 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`<x, k>)) = z" 1);
+by (subgoal_tac "fix$(LAM k. csnd$(f$<x, k>)) = z" 1);
by (asm_simp_tac HOLCF_ss 1);
-by (subgoal_tac "! w y. f`<x, w> = <y, w> --> z << w" 1);
+by (subgoal_tac "! w y. f$<x, w> = <y, w> --> 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`<x, za> = <cfst`(f`<x,za>),za>" 1);
+by (subgoal_tac "f$<x, za> = <cfst$(f$<x,za>),za>" 1);
by (fast_tac HOL_cs 1);
by (rtac trans 1);
by (rtac (surjective_pairing_Cprod2 RS sym) 1);
--- 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
- <y,z> = f`<x,z>
+ <y,z> = f$<x,z>
end network
end g
@@ -47,7 +47,7 @@
'c stream * ('b,'c) tc stream) => bool
is_f f = !i1 i2 o1 o2.
- f`<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2)
+ f$<i1,i2> = <o1,o2> --> 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. <y,z> = f`<x,z> &
- !oy hz. <oy,hz> = f`<x,hz> --> z << hz
+ ? z. <y,z> = f$<x,z> &
+ !oy hz. <oy,hz> = f$<x,hz> --> 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`<x,fix`(LAM k.csnd`(f`<x,k>))>)) )
+ g = (LAM x. cfst$(f$<x,fix$(LAM k.csnd$(f$<x,k>))>)) )
Now we prove:
@@ -118,19 +118,19 @@
defs
is_f "is_f f == (!i1 i2 o1 o2.
- f`<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2))"
+ f$<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2))"
is_net_g "is_net_g f x y == (? z.
- <y,z> = f`<x,z> &
- (!oy hz. <oy,hz> = f`<x,hz> --> z << hz))"
+ <y,z> = f$<x,z> &
+ (!oy hz. <oy,hz> = f$<x,hz> --> 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`<x,fix`(LAM k. csnd`(f`<x,k>))>)))"
+ g = (LAM x. cfst$(f$<x,fix$(LAM k. csnd$(f$<x,k>))>)))"
end
--- 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);
--- 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
--- 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);
--- 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
--- 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);
--- 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
*)