# HG changeset patch
# User huffman
# Date 1130975030 -3600
# Node ID 43000d7a017cd4c6d9b33d7ee883f177c9f914bc
# Parent  a92b7c5133de40fc79153f652ce1b3e64448d12e
changed iterate to a continuous type

diff -r a92b7c5133de -r 43000d7a017c src/HOLCF/FOCUS/Stream_adm.thy
--- 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"
diff -r a92b7c5133de -r 43000d7a017c src/HOLCF/domain/axioms.ML
--- 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)));
 
diff -r a92b7c5133de -r 43000d7a017c src/HOLCF/ex/Fix2.ML
--- 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";
diff -r a92b7c5133de -r 43000d7a017c src/HOLCF/ex/Hoare.ML
--- 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);
diff -r a92b7c5133de -r 43000d7a017c src/HOLCF/ex/Loop.ML
--- 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);
diff -r a92b7c5133de -r 43000d7a017c src/HOLCF/ex/Stream.thy
--- 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)