# HG changeset patch
# User paulson
# Date 962883340 -7200
# Node ID 35aab1c9c08cea859cb3de8eb8c7c2c6b5b861d7
# Parent  051592f4236aedfa11e783a03005bcf27becac0b
removal of batch style, and tidying

diff -r 051592f4236a -r 35aab1c9c08c src/HOLCF/ex/Dnat.ML
--- a/src/HOLCF/ex/Dnat.ML	Thu Jul 06 13:28:36 2000 +0200
+++ b/src/HOLCF/ex/Dnat.ML	Thu Jul 06 13:35:40 2000 +0200
@@ -19,57 +19,49 @@
 (* recursive  properties                                                     *)
 (* ------------------------------------------------------------------------- *)
 
-qed_goal "iterator1" Dnat.thy "iterator`UU`f`x = UU"
- (fn prems =>
-	[
-	(stac iterator_def2 1),
-	(simp_tac (HOLCF_ss addsimps dnat.rews) 1)
-	]);
+Goal "iterator`UU`f`x = UU";
+by (stac iterator_def2 1);
+by (simp_tac (HOLCF_ss addsimps dnat.rews) 1);
+qed "iterator1";
 
-qed_goal "iterator2" Dnat.thy "iterator`dzero`f`x = x"
- (fn prems =>
-	[
-	(stac iterator_def2 1),
-	(simp_tac (HOLCF_ss addsimps dnat.rews) 1)
-	]);
+Goal "iterator`dzero`f`x = x";
+by (stac iterator_def2 1);
+by (simp_tac (HOLCF_ss addsimps dnat.rews) 1);
+qed "iterator2";
 
-qed_goal "iterator3" Dnat.thy 
-"n~=UU ==> iterator`(dsucc`n)`f`x = f`(iterator`n`f`x)"
- (fn prems =>
-	[
-	(cut_facts_tac prems 1),
-	(rtac trans 1),
-	(stac iterator_def2 1),
-	(asm_simp_tac (HOLCF_ss addsimps dnat.rews) 1),
-	(rtac refl 1)
-	]);
+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);
+by (rtac refl 1);
+qed "iterator3";
 
 val iterator_rews = 
 	[iterator1, iterator2, iterator3];
 
-val dnat_flat = prove_goal Dnat.thy "!x y::dnat. x<<y --> x=UU | x=y" 
-(fn _ => [
-	(rtac allI 1),
-	(res_inst_tac [("x","x")] dnat.ind 1),
-	(fast_tac HOL_cs 1),
-	(rtac allI 1),
-	(res_inst_tac [("x","y")] dnat.casedist 1),
-	(fast_tac (HOL_cs addSIs [UU_I]) 1),
-	(Asm_simp_tac 1),
-	(asm_simp_tac (simpset() addsimps dnat.dist_les) 1),
-	(rtac allI 1),
-	(res_inst_tac [("x","y")] dnat.casedist 1),
-	(fast_tac (HOL_cs addSIs [UU_I]) 1),
-	(asm_simp_tac (simpset() addsimps dnat.dist_les) 1),
-	(asm_simp_tac (simpset() addsimps dnat.rews) 1),
-	(strip_tac 1),
-	(subgoal_tac "d<<da" 1),
-	(etac allE 1),
-	(dtac mp 1),
-	(atac 1),
-	(etac disjE 1),
-	(contr_tac 1),
-	(Asm_simp_tac 1),
-	(resolve_tac  dnat.inverts 1),
-	(REPEAT (atac 1))]);
+Goal "ALL x y::dnat. x<<y --> x=UU | x=y";
+by (rtac allI 1);
+by (res_inst_tac [("x","x")] dnat.ind 1);
+by (fast_tac HOL_cs 1);
+by (rtac allI 1);
+by (res_inst_tac [("x","y")] dnat.casedist 1);
+by (fast_tac (HOL_cs addSIs [UU_I]) 1);
+by (Asm_simp_tac 1);
+by (asm_simp_tac (simpset() addsimps dnat.dist_les) 1);
+by (rtac allI 1);
+by (res_inst_tac [("x","y")] dnat.casedist 1);
+by (fast_tac (HOL_cs addSIs [UU_I]) 1);
+by (asm_simp_tac (simpset() addsimps dnat.dist_les) 1);
+by (asm_simp_tac (simpset() addsimps dnat.rews) 1);
+by (strip_tac 1);
+by (subgoal_tac "d<<da" 1);
+by (etac allE 1);
+by (dtac mp 1);
+by (atac 1);
+by (etac disjE 1);
+by (contr_tac 1);
+by (Asm_simp_tac 1);
+by (resolve_tac  dnat.inverts 1);
+by (REPEAT (atac 1));
+qed "dnat_flat";
 
diff -r 051592f4236a -r 35aab1c9c08c src/HOLCF/ex/Fix2.ML
--- a/src/HOLCF/ex/Fix2.ML	Thu Jul 06 13:28:36 2000 +0200
+++ b/src/HOLCF/ex/Fix2.ML	Thu Jul 06 13:35:40 2000 +0200
@@ -4,25 +4,19 @@
     Copyright   1995 Technische Universitaet Muenchen
 *)
 
-open Fix2;
-
-val lemma1 = prove_goal Fix2.thy "fix = gix"
- (fn prems =>
-        [
-        (rtac ext_cfun 1),
-        (rtac antisym_less 1),
-        (rtac fix_least 1),
-        (rtac gix1_def 1),
-        (rtac gix2_def 1),
-        (rtac (fix_eq RS sym) 1)
-        ]);
+Goal "fix = gix";
+by (rtac ext_cfun 1);
+by (rtac antisym_less 1);
+by (rtac fix_least 1);
+by (rtac gix1_def 1);
+by (rtac gix2_def 1);
+by (rtac (fix_eq RS sym) 1);
+qed "lemma1";
 
 
-val lemma2 = prove_goal Fix2.thy "gix`F=lub(range(%i. iterate i F UU))"
- (fn prems =>
-        [
-        (rtac (lemma1 RS subst) 1),
-        (rtac fix_def2 1)
-        ]);
+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 051592f4236a -r 35aab1c9c08c src/HOLCF/ex/Hoare.ML
--- a/src/HOLCF/ex/Hoare.ML	Thu Jul 06 13:28:36 2000 +0200
+++ b/src/HOLCF/ex/Hoare.ML	Thu Jul 06 13:35:40 2000 +0200
@@ -4,512 +4,411 @@
     Copyright   1993 Technische Universitaet Muenchen
 *)
 
-open Hoare;
-
 (* --------- pure HOLCF logic, some little lemmas ------ *)
 
-val hoare_lemma2 = prove_goal HOLCF.thy "b~=TT ==> b=FF | b=UU"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (rtac (Exh_tr RS disjE) 1),
-        (fast_tac HOL_cs 1),
-        (etac disjE 1),
-        (contr_tac 1),
-        (fast_tac HOL_cs 1)
-        ]);
+Goal "b~=TT ==> b=FF | b=UU";
+by (rtac (Exh_tr RS disjE) 1);
+by (fast_tac HOL_cs 1);
+by (etac disjE 1);
+by (contr_tac 1);
+by (fast_tac HOL_cs 1);
+qed "hoare_lemma2";
 
-val hoare_lemma3 = prove_goal HOLCF.thy 
-" (!k. b1`(iterate k g x) = TT) | (? k. b1`(iterate k g x)~=TT)"
- (fn prems =>
-        [
-        (fast_tac HOL_cs 1)
-        ]);
+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";
 
-val hoare_lemma4 = prove_goal HOLCF.thy 
-"(? k. b1`(iterate k g x) ~= TT) ==> \
-\ ? k. b1`(iterate k g x) = FF | b1`(iterate k g x) = UU"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (etac exE 1),
-        (rtac exI 1),
-        (rtac hoare_lemma2 1),
-        (atac 1)
-        ]);
+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";
 
-val hoare_lemma5 = prove_goal HOLCF.thy 
-"[|(? k. b1`(iterate k g x) ~= TT);\
+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"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (hyp_subst_tac 1),
-        (rtac hoare_lemma2 1),
-        (etac exE 1),
-        (etac LeastI 1)
-        ]);
+\ 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);
+by (etac LeastI 1);
+qed "hoare_lemma5";
 
-val hoare_lemma6 = prove_goal HOLCF.thy "b=UU ==> b~=TT"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (hyp_subst_tac 1),
-        (resolve_tac dist_eq_tr 1)
-        ]);
+Goal "b=UU ==> b~=TT";
+by (hyp_subst_tac 1);
+by (resolve_tac dist_eq_tr 1);
+qed "hoare_lemma6";
+
+Goal "b=FF ==> b~=TT";
+by (hyp_subst_tac 1);
+by (resolve_tac dist_eq_tr 1);
+qed "hoare_lemma7";
 
-val hoare_lemma7 = prove_goal HOLCF.thy "b=FF ==> b~=TT"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (hyp_subst_tac 1),
-        (resolve_tac dist_eq_tr 1)
-        ]);
-
-val hoare_lemma8 = prove_goal HOLCF.thy 
-"[|(? k. b1`(iterate k g x) ~= TT);\
+Goal "[|(EX k. b1`(iterate k g x) ~= TT);\
 \   k=Least(%n. b1`(iterate n g x) ~= TT)|] ==> \
-\ !m. m < k --> b1`(iterate m g x)=TT"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (hyp_subst_tac 1),
-        (etac exE 1),
-        (strip_tac 1),
-        (res_inst_tac [("p","b1`(iterate m g x)")] trE 1),
-        (atac 2),
-        (rtac (le_less_trans RS less_irrefl) 1),
-        (atac 2),
-        (rtac Least_le 1),
-        (etac hoare_lemma6 1),
-        (rtac (le_less_trans RS less_irrefl) 1),
-        (atac 2),
-        (rtac Least_le 1),
-        (etac hoare_lemma7 1)
-        ]);
+\ 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 (atac 2);
+by (rtac (le_less_trans RS less_irrefl) 1);
+by (atac 2);
+by (rtac Least_le 1);
+by (etac hoare_lemma6 1);
+by (rtac (le_less_trans RS less_irrefl) 1);
+by (atac 2);
+by (rtac Least_le 1);
+by (etac hoare_lemma7 1);
+qed "hoare_lemma8";
 
 
-val hoare_lemma28 = prove_goal HOLCF.thy 
-"b1`(y::'a)=(UU::tr) ==> b1`UU = UU"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (etac (flat_codom RS disjE) 1),
-        (atac 1),
-        (etac spec 1)
-        ]);
+Goal "f`(y::'a)=(UU::tr) ==> f`UU = UU";
+by (etac (flat_codom RS disjE) 1);
+by Auto_tac;  
+qed "hoare_lemma28";
 
 
 (* ----- access to definitions ----- *)
 
-val p_def3 = prove_goal Hoare.thy 
-"p`x = If b1`x then p`(g`x) else x fi"
- (fn prems =>
-        [
-        (fix_tac3 p_def 1),
-        (Simp_tac 1)
-        ]);
+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";
 
-val q_def3 = prove_goal Hoare.thy 
-"q`x = If b1`x orelse b2`x then q`(g`x) else x fi"
- (fn prems =>
-        [
-        (fix_tac3 q_def 1),
-        (Simp_tac 1)
-        ]);
+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 ---------- **)
 
-val hoare_lemma9 = prove_goal Hoare.thy 
-"(! m. m< Suc k --> b1`(iterate m g x)=TT) -->\
-\  p`(iterate k g x)=p`x"
- (fn prems =>
-        [
-        (nat_ind_tac "k" 1),
-        (Simp_tac 1),
-        (Simp_tac 1),
-        (strip_tac 1),
-        (res_inst_tac [("s","p`(iterate k g x)")] trans 1),
-        (rtac trans 1),
-        (rtac (p_def3 RS sym) 2),
-        (res_inst_tac [("s","TT"),("t","b1`(iterate k g x)")] ssubst 1),
-        (rtac mp 1),
-        (etac spec 1),
-        (simp_tac (simpset() addsimps [less_Suc_eq]) 1),
-        (simp_tac HOLCF_ss 1),
-        (etac mp 1),
-        (strip_tac 1),
-        (rtac mp 1),
-        (etac spec 1),
-        (etac less_trans 1),
-        (Simp_tac 1)
-        ]);
+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 (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 (rtac mp 1);
+by (etac spec 1);
+by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
+by (simp_tac HOLCF_ss 1);
+by (etac mp 1);
+by (strip_tac 1);
+by (rtac mp 1);
+by (etac spec 1);
+by (etac less_trans 1);
+by (Simp_tac 1);
+qed "hoare_lemma9";
 
-val hoare_lemma24 = prove_goal Hoare.thy 
-"(! m. m< Suc k --> b1`(iterate m g x)=TT) --> \
-\ q`(iterate k g x)=q`x"
- (fn prems =>
-        [
-        (nat_ind_tac "k" 1),
-        (Simp_tac 1),
-(simp_tac (simpset() addsimps [less_Suc_eq]) 1),
-        (strip_tac 1),
-        (res_inst_tac [("s","q`(iterate k g x)")] trans 1),
-        (rtac trans 1),
-        (rtac (q_def3 RS sym) 2),
-        (res_inst_tac [("s","TT"),("t","b1`(iterate k g x)")] ssubst 1),
-        (fast_tac HOL_cs 1),
-        (simp_tac HOLCF_ss 1),
-        (etac mp 1),
-        (strip_tac 1),
-        (fast_tac (HOL_cs addSDs [less_Suc_eq RS iffD1]) 1)]);
+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 (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 (fast_tac HOL_cs 1);
+by (simp_tac HOLCF_ss 1);
+by (etac mp 1);
+by (strip_tac 1);
+by (fast_tac (HOL_cs addSDs [less_Suc_eq RS iffD1]) 1);
+qed "hoare_lemma24";
 
-(* -------- results about p for case (? 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 = "[| ? k. b1`(iterate k g ?x1) ~= TT;
+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_lemma11 = prove_goal Hoare.thy 
-"(? n. b1`(iterate n g x) ~= TT) ==>\
+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"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (case_tac "k" 1),
-        (hyp_subst_tac 1),
-        (Simp_tac 1),
-        (strip_tac 1),
-        (etac conjE 1),
-        (rtac trans 1),
-        (rtac p_def3 1),
-        (asm_simp_tac HOLCF_ss 1),
-        (hyp_subst_tac 1),
-        (strip_tac 1),
-        (etac conjE 1),
-        (rtac trans 1),
-        (etac (hoare_lemma10 RS sym) 1),
-        (atac 1),
-        (rtac trans 1),
-        (rtac p_def3 1),
-        (res_inst_tac [("s","TT"),("t","b1`(iterate nat g x)")] ssubst 1),
-        (rtac (hoare_lemma8 RS spec RS mp) 1),
-        (atac 1),
-        (atac 1),
-        (Simp_tac 1),
-        (simp_tac HOLCF_ss 1),
-        (rtac trans 1),
-        (rtac p_def3 1),
-        (simp_tac (simpset() delsimps [iterate_Suc]
-                            addsimps [iterate_Suc RS sym]) 1),
-        (eres_inst_tac [("s","FF")] ssubst 1),
-        (simp_tac HOLCF_ss 1)
-        ]);
+\ --> p`x = iterate k g x";
+by (case_tac "k" 1);
+by (hyp_subst_tac 1);
+by (Simp_tac 1);
+by (strip_tac 1);
+by (etac conjE 1);
+by (rtac trans 1);
+by (rtac p_def3 1);
+by (asm_simp_tac HOLCF_ss 1);
+by (hyp_subst_tac 1);
+by (strip_tac 1);
+by (etac conjE 1);
+by (rtac trans 1);
+by (etac (hoare_lemma10 RS sym) 1);
+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 (rtac (hoare_lemma8 RS spec RS mp) 1);
+by (atac 1);
+by (atac 1);
+by (Simp_tac 1);
+by (simp_tac HOLCF_ss 1);
+by (rtac trans 1);
+by (rtac p_def3 1);
+by (simp_tac (simpset() delsimps [iterate_Suc] addsimps [iterate_Suc RS sym]) 1);
+by (eres_inst_tac [("s","FF")] ssubst 1);
+by (simp_tac HOLCF_ss 1);
+qed "hoare_lemma11";
 
-val hoare_lemma12 = prove_goal Hoare.thy 
-"(? n. b1`(iterate n g x) ~= TT) ==>\
+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"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (case_tac "k" 1),
-        (hyp_subst_tac 1),
-        (Simp_tac 1),
-        (strip_tac 1),
-        (etac conjE 1),
-        (rtac trans 1),
-        (rtac p_def3 1),
-        (asm_simp_tac HOLCF_ss 1),
-        (hyp_subst_tac 1),
-        (Simp_tac 1),
-        (strip_tac 1),
-        (etac conjE 1),
-        (rtac trans 1),
-        (rtac (hoare_lemma10 RS sym) 1),
-        (atac 1),
-        (atac 1),
-        (rtac trans 1),
-        (rtac p_def3 1),
-        (res_inst_tac [("s","TT"),("t","b1`(iterate nat g x)")] ssubst 1),
-        (rtac (hoare_lemma8 RS spec RS mp) 1),
-        (atac 1),
-        (atac 1),
-        (Simp_tac 1),
-        (asm_simp_tac HOLCF_ss 1),
-        (rtac trans 1),
-        (rtac p_def3 1),
-        (asm_simp_tac HOLCF_ss 1)
-        ]);
+\ --> p`x = UU";
+by (case_tac "k" 1);
+by (hyp_subst_tac 1);
+by (Simp_tac 1);
+by (strip_tac 1);
+by (etac conjE 1);
+by (rtac trans 1);
+by (rtac p_def3 1);
+by (asm_simp_tac HOLCF_ss 1);
+by (hyp_subst_tac 1);
+by (Simp_tac 1);
+by (strip_tac 1);
+by (etac conjE 1);
+by (rtac trans 1);
+by (rtac (hoare_lemma10 RS sym) 1);
+by (atac 1);
+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 (rtac (hoare_lemma8 RS spec RS mp) 1);
+by (atac 1);
+by (atac 1);
+by (Simp_tac 1);
+by (asm_simp_tac HOLCF_ss 1);
+by (rtac trans 1);
+by (rtac p_def3 1);
+by (asm_simp_tac HOLCF_ss 1);
+qed "hoare_lemma12";
 
-(* -------- results about p for case  (! k. b1`(iterate k g x)=TT) ------- *)
+(* -------- results about p for case  (ALL k. b1`(iterate k g x)=TT) ------- *)
 
-val fernpass_lemma = prove_goal Hoare.thy 
-"(! k. b1`(iterate k g x)=TT) ==> !k. p`(iterate k g x) = UU"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (rtac (p_def RS def_fix_ind) 1),
-        (rtac adm_all 1),
-        (rtac allI 1),
-        (rtac adm_eq 1),
-        (cont_tacR 1),
-        (rtac allI 1),
-        (stac strict_Rep_CFun1 1),
-        (rtac refl 1),
-        (Simp_tac 1),
-        (rtac allI 1),
-        (res_inst_tac [("s","TT"),("t","b1`(iterate k g x)")] ssubst 1),
-        (etac spec 1),
-        (asm_simp_tac HOLCF_ss 1),
-        (rtac (iterate_Suc RS subst) 1),
-        (etac spec 1)
-        ]);
+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);
+by (rtac adm_eq 1);
+by (cont_tacR 1);
+by (rtac allI 1);
+by (stac strict_Rep_CFun1 1);
+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 (etac spec 1);
+by (asm_simp_tac HOLCF_ss 1);
+by (rtac (iterate_Suc RS subst) 1);
+by (etac spec 1);
+qed "fernpass_lemma";
 
-val hoare_lemma16 = prove_goal Hoare.thy 
-"(! k. b1`(iterate k g x)=TT) ==> p`x = UU"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1),
-        (etac (fernpass_lemma RS spec) 1)
-        ]);
-
-(* -------- results about q for case  (! k. b1`(iterate k g x)=TT) ------- *)
+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";
 
-val hoare_lemma17 = prove_goal Hoare.thy 
-"(! k. b1`(iterate k g x)=TT) ==> !k. q`(iterate k g x) = UU"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (rtac (q_def RS def_fix_ind) 1),
-        (rtac adm_all 1),
-        (rtac allI 1),
-        (rtac adm_eq 1),
-        (cont_tacR 1),
-        (rtac allI 1),
-        (stac strict_Rep_CFun1 1),
-        (rtac refl 1),
-        (rtac allI 1),
-        (Simp_tac 1),
-        (res_inst_tac [("s","TT"),("t","b1`(iterate k g x)")] ssubst 1),
-        (etac spec 1),
-        (asm_simp_tac HOLCF_ss 1),
-        (rtac (iterate_Suc RS subst) 1),
-        (etac spec 1)
-        ]);
+(* -------- results about q for case  (ALL k. b1`(iterate k g x)=TT) ------- *)
 
-val hoare_lemma18 = prove_goal Hoare.thy 
-"(! k. b1`(iterate k g x)=TT) ==> q`x = UU"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1),
-        (etac (hoare_lemma17 RS spec) 1)
-        ]);
+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);
+by (rtac adm_eq 1);
+by (cont_tacR 1);
+by (rtac allI 1);
+by (stac strict_Rep_CFun1 1);
+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 (etac spec 1);
+by (asm_simp_tac HOLCF_ss 1);
+by (rtac (iterate_Suc RS subst) 1);
+by (etac spec 1);
+qed "hoare_lemma17";
 
-val hoare_lemma19 = prove_goal Hoare.thy 
-"(!k. (b1::'a->tr)`(iterate k g x)=TT) ==> b1`(UU::'a) = UU | (!y. b1`(y::'a)=TT)"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (rtac (flat_codom) 1),
-        (res_inst_tac [("t","x1")] (iterate_0 RS subst) 1),
-        (etac spec 1)
-        ]);
+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)";
+by (rtac (flat_codom) 1);
+by (res_inst_tac [("t","x1")] (iterate_0 RS subst) 1);
+by (etac spec 1);
+qed "hoare_lemma19";
 
-val hoare_lemma20 = prove_goal Hoare.thy 
-"(! y. b1`(y::'a)=TT) ==> !k. q`(iterate k g (x::'a)) = UU"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (rtac (q_def RS def_fix_ind) 1),
-        (rtac adm_all 1),
-        (rtac allI 1),
-        (rtac adm_eq 1),
-        (cont_tacR 1),
-        (rtac allI 1),
-        (stac strict_Rep_CFun1 1),
-        (rtac refl 1),
-        (rtac allI 1),
-        (Simp_tac 1),
-        (res_inst_tac [("s","TT"),("t","b1`(iterate k g (x::'a))")] ssubst 1),
-        (etac spec 1),
-        (asm_simp_tac HOLCF_ss 1),
-        (rtac (iterate_Suc RS subst) 1),
-        (etac spec 1)
-        ]);
+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);
+by (rtac adm_eq 1);
+by (cont_tacR 1);
+by (rtac allI 1);
+by (stac strict_Rep_CFun1 1);
+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 (etac spec 1);
+by (asm_simp_tac HOLCF_ss 1);
+by (rtac (iterate_Suc RS subst) 1);
+by (etac spec 1);
+qed "hoare_lemma20";
 
-val hoare_lemma21 = prove_goal Hoare.thy 
-"(! y. b1`(y::'a)=TT) ==> q`(x::'a) = UU"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1),
-        (etac (hoare_lemma20 RS spec) 1)
-        ]);
+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";
 
-val hoare_lemma22 = prove_goal Hoare.thy 
-"b1`(UU::'a)=UU ==> q`(UU::'a) = UU"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (stac q_def3 1),
-        (asm_simp_tac HOLCF_ss 1)
-        ]);
+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 (? 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 = "[| ? k. b1`(iterate k g ?x1) ~= TT;
+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_lemma26 = prove_goal Hoare.thy 
-"(? n. b1`(iterate n g x)~=TT) ==>\
+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)"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (case_tac "k" 1),
-        (hyp_subst_tac 1),
-        (strip_tac 1),
-        (Simp_tac 1),
-        (hyp_subst_tac 1),
-        (strip_tac 1),
-        (etac conjE 1),
-        (rtac trans 1),
-        (rtac (hoare_lemma25 RS sym) 1),
-        (atac 1),
-        (atac 1),
-        (rtac trans 1),
-        (rtac q_def3 1),
-        (res_inst_tac [("s","TT"),("t","b1`(iterate nat g x)")] ssubst 1),
-        (rtac (hoare_lemma8 RS spec RS mp) 1),
-        (atac 1),
-        (atac 1),
-        (Simp_tac 1),
-        (simp_tac HOLCF_ss 1)
-        ]);
+\ --> q`x = q`(iterate k g x)";
+by (case_tac "k" 1);
+by (hyp_subst_tac 1);
+by (strip_tac 1);
+by (Simp_tac 1);
+by (hyp_subst_tac 1);
+by (strip_tac 1);
+by (etac conjE 1);
+by (rtac trans 1);
+by (rtac (hoare_lemma25 RS sym) 1);
+by (atac 1);
+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 (rtac (hoare_lemma8 RS spec RS mp) 1);
+by (atac 1);
+by (atac 1);
+by (Simp_tac 1);
+by (simp_tac HOLCF_ss 1);
+qed "hoare_lemma26";
 
 
-val hoare_lemma27 = prove_goal Hoare.thy 
-"(? n. b1`(iterate n g x) ~= TT) ==>\
+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"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (case_tac "k" 1),
-        (hyp_subst_tac 1),
-        (Simp_tac 1),
-        (strip_tac 1),
-        (etac conjE 1),
-        (stac q_def3 1),
-        (asm_simp_tac HOLCF_ss 1),
-        (hyp_subst_tac 1),
-        (Simp_tac 1),
-        (strip_tac 1),
-        (etac conjE 1),
-        (rtac trans 1),
-        (rtac (hoare_lemma25 RS sym) 1),
-        (atac 1),
-        (atac 1),
-        (rtac trans 1),
-        (rtac q_def3 1),
-        (res_inst_tac [("s","TT"),("t","b1`(iterate nat g x)")] ssubst 1),
-        (rtac (hoare_lemma8 RS spec RS mp) 1),
-        (atac 1),
-        (atac 1),
-        (Simp_tac 1),
-        (asm_simp_tac HOLCF_ss 1),
-        (rtac trans 1),
-        (rtac q_def3 1),
-        (asm_simp_tac HOLCF_ss 1)
-        ]);
+\ --> q`x = UU";
+by (case_tac "k" 1);
+by (hyp_subst_tac 1);
+by (Simp_tac 1);
+by (strip_tac 1);
+by (etac conjE 1);
+by (stac q_def3 1);
+by (asm_simp_tac HOLCF_ss 1);
+by (hyp_subst_tac 1);
+by (Simp_tac 1);
+by (strip_tac 1);
+by (etac conjE 1);
+by (rtac trans 1);
+by (rtac (hoare_lemma25 RS sym) 1);
+by (atac 1);
+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 (rtac (hoare_lemma8 RS spec RS mp) 1);
+by (atac 1);
+by (atac 1);
+by (Simp_tac 1);
+by (asm_simp_tac HOLCF_ss 1);
+by (rtac trans 1);
+by (rtac q_def3 1);
+by (asm_simp_tac HOLCF_ss 1);
+qed "hoare_lemma27";
 
-(* ------- (! k. b1`(iterate k g x)=TT) ==> q o p = q   ----- *)
+(* ------- (ALL k. b1`(iterate k g x)=TT) ==> q o p = q   ----- *)
 
-val hoare_lemma23 = prove_goal Hoare.thy 
-"(! k. b1`(iterate k g x)=TT) ==> q`(p`x) = q`x"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (stac hoare_lemma16 1),
-        (atac 1),
-        (rtac (hoare_lemma19 RS disjE) 1),
-        (atac 1),
-        (stac hoare_lemma18 1),
-        (atac 1),
-        (stac hoare_lemma22 1),
-        (atac 1),
-        (rtac refl 1),
-        (stac hoare_lemma21 1),
-        (atac 1),
-        (stac hoare_lemma21 1),
-        (atac 1),
-        (rtac refl 1)
-        ]);
+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);
+by (atac 1);
+by (stac hoare_lemma18 1);
+by (atac 1);
+by (stac hoare_lemma22 1);
+by (atac 1);
+by (rtac refl 1);
+by (stac hoare_lemma21 1);
+by (atac 1);
+by (stac hoare_lemma21 1);
+by (atac 1);
+by (rtac refl 1);
+qed "hoare_lemma23";
 
-(* ------------  ? k. b1~(iterate k g x) ~= TT ==> q o p = q   ----- *)
+(* ------------  EX k. b1~(iterate k g x) ~= TT ==> q o p = q   ----- *)
 
-val hoare_lemma29 = prove_goal Hoare.thy 
-"? k. b1`(iterate k g x) ~= TT ==> q`(p`x) = q`x"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (rtac (hoare_lemma5 RS disjE) 1),
-        (atac 1),
-        (rtac refl 1),
-        (stac (hoare_lemma11 RS mp) 1),
-        (atac 1),
-        (rtac conjI 1),
-        (rtac refl 1),
-        (atac 1),
-        (rtac (hoare_lemma26 RS mp RS subst) 1),
-        (atac 1),
-        (rtac conjI 1),
-        (rtac refl 1),
-        (atac 1),
-        (rtac refl 1),
-        (stac (hoare_lemma12 RS mp) 1),
-        (atac 1),
-        (rtac conjI 1),
-        (rtac refl 1),
-        (atac 1),
-        (stac hoare_lemma22 1),
-        (stac hoare_lemma28 1),
-        (atac 1),
-        (rtac refl 1),
-        (rtac sym 1),
-        (stac (hoare_lemma27 RS mp) 1),
-        (atac 1),
-        (rtac conjI 1),
-        (rtac refl 1),
-        (atac 1),
-        (rtac refl 1)
-        ]);
+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);
+by (stac (hoare_lemma11 RS mp) 1);
+by (atac 1);
+by (rtac conjI 1);
+by (rtac refl 1);
+by (atac 1);
+by (rtac (hoare_lemma26 RS mp RS subst) 1);
+by (atac 1);
+by (rtac conjI 1);
+by (rtac refl 1);
+by (atac 1);
+by (rtac refl 1);
+by (stac (hoare_lemma12 RS mp) 1);
+by (atac 1);
+by (rtac conjI 1);
+by (rtac refl 1);
+by (atac 1);
+by (stac hoare_lemma22 1);
+by (stac hoare_lemma28 1);
+by (atac 1);
+by (rtac refl 1);
+by (rtac sym 1);
+by (stac (hoare_lemma27 RS mp) 1);
+by (atac 1);
+by (rtac conjI 1);
+by (rtac refl 1);
+by (atac 1);
+by (rtac refl 1);
+qed "hoare_lemma29";
 
 (* ------ the main prove q o p = q ------ *)
 
-val hoare_main = prove_goal Hoare.thy "q oo p = q"
- (fn prems =>
-        [
-        (rtac ext_cfun 1),
-        (stac cfcomp2 1),
-        (rtac (hoare_lemma3 RS disjE) 1),
-        (etac hoare_lemma23 1),
-        (etac hoare_lemma29 1)
-        ]);
+Goal "q oo p = q";
+by (rtac ext_cfun 1);
+by (stac cfcomp2 1);
+by (rtac (hoare_lemma3 RS disjE) 1);
+by (etac hoare_lemma23 1);
+by (etac hoare_lemma29 1);
+qed "hoare_main";