--- a/src/HOLCF/FOCUS/Stream_adm.thy Thu Nov 03 00:43:11 2005 +0100
+++ b/src/HOLCF/FOCUS/Stream_adm.thy Thu Nov 03 00:43:50 2005 +0100
@@ -13,13 +13,13 @@
stream_monoP :: "(('a stream) set \<Rightarrow> ('a stream) set) \<Rightarrow> bool"
"stream_monoP F \<equiv> \<exists>Q i. \<forall>P s. Fin i \<le> #s \<longrightarrow>
- (s \<in> F P) = (stream_take i\<cdot>s \<in> Q \<and> iterate i rt s \<in> P)"
+ (s \<in> F P) = (stream_take i\<cdot>s \<in> Q \<and> iterate i\<cdot>rt\<cdot>s \<in> P)"
stream_antiP :: "(('a stream) set \<Rightarrow> ('a stream) set) \<Rightarrow> bool"
"stream_antiP F \<equiv> \<forall>P x. \<exists>Q i.
(#x < Fin i \<longrightarrow> (\<forall>y. x \<sqsubseteq> y \<longrightarrow> y \<in> F P \<longrightarrow> x \<in> F P)) \<and>
(Fin i <= #x \<longrightarrow> (\<forall>y. x \<sqsubseteq> y \<longrightarrow>
- (y \<in> F P) = (stream_take i\<cdot>y \<in> Q \<and> iterate i rt y \<in> P)))"
+ (y \<in> F P) = (stream_take i\<cdot>y \<in> Q \<and> iterate i\<cdot>rt\<cdot>y \<in> P)))"
antitonP :: "'a set => bool"
"antitonP P \<equiv> \<forall>x y. x \<sqsubseteq> y \<longrightarrow> y\<in>P \<longrightarrow> x\<in>P"
--- a/src/HOLCF/domain/axioms.ML Thu Nov 03 00:43:11 2005 +0100
+++ b/src/HOLCF/domain/axioms.ML Thu Nov 03 00:43:50 2005 +0100
@@ -83,7 +83,7 @@
val reach_ax = ("reach", mk_trp(cproj (%%:fixN`%%(comp_dname^"_copy")) eqs n
`%x_name === %:x_name));
val take_def = ("take_def",%%:(dname^"_take") == mk_lam("n",cproj'
- (%%:iterateN $ Bound 0 $ %%:(comp_dname^"_copy") $ UU) eqs n));
+ (%%:iterateN $ Bound 0 ` %%:(comp_dname^"_copy") ` UU) eqs n));
val finite_def = ("finite_def",%%:(dname^"_finite") == mk_lam(x_name,
mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
--- a/src/HOLCF/ex/Fix2.ML Thu Nov 03 00:43:11 2005 +0100
+++ b/src/HOLCF/ex/Fix2.ML Thu Nov 03 00:43:50 2005 +0100
@@ -13,7 +13,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/Hoare.ML Thu Nov 03 00:43:11 2005 +0100
+++ b/src/HOLCF/ex/Hoare.ML Thu Nov 03 00:43:50 2005 +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);
@@ -84,16 +84,16 @@
(** --------- 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 (induct_tac "k" 1);
by (Simp_tac 1);
by (Simp_tac 1);
by (strip_tac 1);
-by (res_inst_tac [("s","p$(iterate n g x)")] trans 1);
+by (res_inst_tac [("s","p$(iterate n$g$x)")] trans 1);
by (rtac trans 1);
by (rtac (p_def3 RS sym) 2);
-by (res_inst_tac [("s","TT"),("t","b1$(iterate n g x)")] ssubst 1);
+by (res_inst_tac [("s","TT"),("t","b1$(iterate n$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 (induct_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 n g x)")] trans 1);
+by (res_inst_tac [("s","q$(iterate n$g$x)")] trans 1);
by (rtac trans 1);
by (rtac (q_def3 RS sym) 2);
-by (res_inst_tac [("s","TT"),("t","b1$(iterate n g x)")] ssubst 1);
+by (res_inst_tac [("s","TT"),("t","b1$(iterate n$g$x)")] ssubst 1);
by (fast_tac HOL_cs 1);
by (simp_tac HOLCF_ss 1);
by (etac mp 1);
@@ -123,7 +123,7 @@
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));
@@ -134,9 +134,9 @@
*)
-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,8 +166,8 @@
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 \
+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);
@@ -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,7 +265,7 @@
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);
@@ -282,7 +282,7 @@
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) );
(*
@@ -291,9 +291,9 @@
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,8 +316,8 @@
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 \
+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);
@@ -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);
@@ -366,9 +366,9 @@
by (rtac refl 1);
qed "hoare_lemma23";
-(* ------------ EX k. b1~(iterate k g x) ~= TT ==> q o p = q ----- *)
+(* ------------ 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/Loop.ML Thu Nov 03 00:43:11 2005 +0100
+++ b/src/HOLCF/ex/Loop.ML Thu Nov 03 00:43:50 2005 +0100
@@ -28,7 +28,7 @@
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 (induct_tac "k" 1);
by (simp_tac HOLCF_ss 1);
by (rtac allI 1);
@@ -54,7 +54,7 @@
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);
+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";
@@ -64,8 +64,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);
@@ -76,34 +76,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)";
+\ ==> iterate k$(step$b$g)$x ~=UU --> INV (iterate k$(step$b$g)$x)";
by (induct_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 n (step$b$g) x)")] trE 1);
+by (res_inst_tac [("p","b$(iterate n$(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 n) (step$b$g) x"),
- ("t","g$(iterate n (step$b$g) x)")] ssubst 1);
+by (res_inst_tac [("s","iterate (Suc n)$(step$b$g)$x"),
+ ("t","g$(iterate n$(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 (induct_tac "k" 1);
by (Simp_tac 1);
by (strip_tac 1);
@@ -117,8 +117,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);
@@ -127,10 +127,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);
@@ -140,12 +140,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";
@@ -158,7 +158,7 @@
"[| (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 (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);
--- a/src/HOLCF/ex/Stream.thy Thu Nov 03 00:43:11 2005 +0100
+++ b/src/HOLCF/ex/Stream.thy Thu Nov 03 00:43:50 2005 +0100
@@ -37,7 +37,7 @@
constr_sconc' :: "nat => 'a stream => 'a stream => 'a stream"
defs
- i_rt_def: "i_rt == %i s. iterate i rt s"
+ i_rt_def: "i_rt == %i s. iterate i$rt$s"
i_th_def: "i_th == %i s. ft$(i_rt i s)"
sconc_def: "s1 ooo s2 == case #s1 of
@@ -136,8 +136,8 @@
lemma surjectiv_scons: "(ft$s)&&(rt$s)=s"
by (rule stream.casedist [of s], auto)
-lemma monofun_rt_mult: "x << s ==> iterate i rt x << iterate i rt s"
-by (insert monofun_iterate2 [of i "rt"], simp add: monofun_def, auto)
+lemma monofun_rt_mult: "x << s ==> iterate i$rt$x << iterate i$rt$s"
+by (rule monofun_cfun_arg)
@@ -152,7 +152,7 @@
lemma stream_reach2: "(LUB i. stream_take i$s) = s"
apply (insert stream.reach [of s], erule subst) back
apply (simp add: fix_def2 stream.take_def)
-apply (insert contlub_cfun_fun [of "%i. iterate i stream_copy UU" s,THEN sym])
+apply (insert contlub_cfun_fun [of "%i. iterate i$stream_copy$UU" s,THEN sym])
by (simp add: chain_iterate)
lemma chain_stream_take: "chain (%i. stream_take i$s)"
@@ -470,10 +470,10 @@
apply (drule slen_mono_lemma, auto)
by (simp add: slen_def)
-lemma iterate_lemma: "F$(iterate n F x) = iterate n F (F$x)"
+lemma iterate_lemma: "F$(iterate n$F$x) = iterate n$F$(F$x)"
by (insert iterate_Suc2 [of n F x], auto)
-lemma slen_rt_mult [rule_format]: "!x. Fin (i + j) <= #x --> Fin j <= #(iterate i rt x)"
+lemma slen_rt_mult [rule_format]: "!x. Fin (i + j) <= #x --> Fin j <= #(iterate i$rt$x)"
apply (induct_tac i, auto)
apply (case_tac "x=UU", auto)
apply (simp add: inat_defs)
@@ -970,11 +970,8 @@
"chain Y ==> (LUB i. x ooo Y i) = (x ooo (LUB i. Y i))"
apply (case_tac "#x=Infty")
apply (simp add: sconc_def)
- prefer 2
- apply (drule finite_lub_sconc,auto simp add: slen_infinite)
-apply (simp add: slen_def)
-apply (insert lub_const [of x] unique_lub [of _ x _])
-by (auto simp add: lub)
+apply (drule finite_lub_sconc,auto simp add: slen_infinite)
+done
lemma contlub_sconc: "contlub (%y. x ooo y)"
by (rule contlubI, insert contlub_sconc_lemma [of _ x], simp)