# HG changeset patch
# User wenzelm
# Date 1148842383 -7200
# Node ID 86f21beabafc9b979d36beae6680fcef83f4d30b
# Parent  f65265d714261ff13ba70b3a6b3906c5e112fb62
removed legacy ML scripts;

diff -r f65265d71426 -r 86f21beabafc src/HOLCF/IsaMakefile
--- a/src/HOLCF/IsaMakefile	Sun May 28 19:54:20 2006 +0200
+++ b/src/HOLCF/IsaMakefile	Sun May 28 20:53:03 2006 +0200
@@ -52,11 +52,9 @@
 
 HOLCF-ex: HOLCF $(LOG)/HOLCF-ex.gz
 
-$(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF ex/Dagstuhl.ML ex/Dagstuhl.thy \
-  ex/Dnat.thy ex/Fix2.ML ex/Fix2.thy ex/Focus_ex.ML \
-  ex/Focus_ex.thy ex/Hoare.ML ex/Hoare.thy ex/Loop.ML ex/Loop.thy \
-  ex/ROOT.ML ex/Fixrec_ex.thy \
-  ../HOL/Library/Nat_Infinity.thy 
+$(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF ex/Dagstuhl.thy \
+  ex/Dnat.thy ex/Fix2.thy ex/Focus_ex.thy ex/Hoare.thy ex/Loop.thy \
+  ex/ROOT.ML ex/Fixrec_ex.thy ../HOL/Library/Nat_Infinity.thy
 	@$(ISATOOL) usedir $(OUT)/HOLCF ex
 
 
diff -r f65265d71426 -r 86f21beabafc src/HOLCF/ex/Dagstuhl.ML
--- a/src/HOLCF/ex/Dagstuhl.ML	Sun May 28 19:54:20 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,67 +0,0 @@
-(* $Id$ *)
-
-val YS_def2  = fix_prover2 (the_context ())  YS_def  "YS = y && YS";
-val YYS_def2 = fix_prover2 (the_context ()) YYS_def "YYS = y && y && YYS";
-
-
-val prems = goal (the_context ()) "YYS << y && YYS";
-by (rtac (YYS_def RS def_fix_ind) 1);
-by (Simp_tac 1);
-by (Simp_tac 1);
-by (Simp_tac 1);
-by (rtac monofun_cfun_arg 1);
-by (rtac monofun_cfun_arg 1);
-by (atac 1);
-val lemma3 = result();
-
-val prems = goal (the_context ()) "y && YYS << YYS";
-by (stac YYS_def2 1);
-back();
-by (rtac monofun_cfun_arg 1);
-by (rtac lemma3 1);
-val lemma4=result();
-
-(* val  lemma5 = lemma3 RS (lemma4 RS antisym_less) *)
-
-val prems = goal (the_context ()) "y && YYS = YYS";
-by (rtac antisym_less 1);
-by (rtac lemma4 1);
-by (rtac lemma3 1);
-val lemma5=result();
-
-val prems = goal (the_context ()) "YS = YYS";
-by (resolve_tac (thms "stream.take_lemmas") 1);
-by (induct_tac "n" 1);
-by (simp_tac (simpset() addsimps (thms "stream.rews")) 1);
-by (stac YS_def2 1);
-by (stac YYS_def2 1);
-by (asm_simp_tac (simpset() addsimps (thms "stream.rews")) 1);
-by (rtac (lemma5 RS sym RS subst) 1);
-by (rtac refl 1);
-val wir_moel=result();
-
-(* ------------------------------------------------------------------------ *)
-(* Zweite L"osung: Bernhard M"oller                                         *)
-(* statt Beweis von  wir_moel "uber take_lemma beidseitige Inclusion        *)
-(* verwendet lemma5                                                         *)
-(* ------------------------------------------------------------------------ *)
-
-val prems = goal (the_context ()) "YYS << YS";
-by (rewtac YYS_def);
-by (rtac fix_least 1);
-by (stac beta_cfun 1);
-by (cont_tacR 1);
-by (simp_tac (simpset() addsimps [YS_def2 RS sym]) 1);
-val lemma6=result();
-
-val prems = goal (the_context ()) "YS << YYS";
-by (rtac (YS_def RS def_fix_ind) 1);
-by (Simp_tac 1);
-by (Simp_tac 1);
-by (Simp_tac 1);
-by (stac (lemma5 RS sym) 1);
-by (etac monofun_cfun_arg 1);
-val lemma7 = result();
-
-val  wir_moel = lemma6 RS (lemma7 RS antisym_less);
-
diff -r f65265d71426 -r 86f21beabafc src/HOLCF/ex/Dagstuhl.thy
--- a/src/HOLCF/ex/Dagstuhl.thy	Sun May 28 19:54:20 2006 +0200
+++ b/src/HOLCF/ex/Dagstuhl.thy	Sun May 28 20:53:03 2006 +0200
@@ -13,7 +13,80 @@
   YYS :: "'a stream"
   "YYS == fix$(LAM z. y && y && z)"
 
-ML {* use_legacy_bindings (the_context ()) *}
+lemma YS_def2: "YS = y && YS"
+  apply (rule trans)
+  apply (rule fix_eq2)
+  apply (rule YS_def)
+  apply (rule beta_cfun)
+  apply simp
+  done
+
+lemma YYS_def2: "YYS = y && y && YYS"
+  apply (rule trans)
+  apply (rule fix_eq2)
+  apply (rule YYS_def)
+  apply (rule beta_cfun)
+  apply simp
+  done
+
+
+lemma lemma3: "YYS << y && YYS"
+  apply (rule YYS_def [THEN def_fix_ind])
+  apply simp_all
+  apply (rule monofun_cfun_arg)
+  apply (rule monofun_cfun_arg)
+  apply assumption
+  done
+
+lemma lemma4: "y && YYS << YYS"
+  apply (subst YYS_def2)
+  back
+  apply (rule monofun_cfun_arg)
+  apply (rule lemma3)
+  done
+
+lemma lemma5: "y && YYS = YYS"
+  apply (rule antisym_less)
+  apply (rule lemma4)
+  apply (rule lemma3)
+  done
+
+lemma wir_moel: "YS = YYS"
+  apply (rule stream.take_lemmas)
+  apply (induct_tac n)
+  apply (simp (no_asm) add: stream.rews)
+  apply (subst YS_def2)
+  apply (subst YYS_def2)
+  apply (simp add: stream.rews)
+  apply (rule lemma5 [symmetric, THEN subst])
+  apply (rule refl)
+  done
+
+(* ------------------------------------------------------------------------ *)
+(* Zweite L"osung: Bernhard Möller                                          *)
+(* statt Beweis von  wir_moel "uber take_lemma beidseitige Inclusion        *)
+(* verwendet lemma5                                                         *)
+(* ------------------------------------------------------------------------ *)
+
+lemma lemma6: "YYS << YS"
+  apply (unfold YYS_def)
+  apply (rule fix_least)
+  apply (subst beta_cfun)
+  apply (tactic "cont_tacR 1")
+  apply (simp add: YS_def2 [symmetric])
+  done
+
+lemma lemma7: "YS << YYS"
+  apply (rule YS_def [THEN def_fix_ind])
+  apply simp_all
+  apply (subst lemma5 [symmetric])
+  apply (erule monofun_cfun_arg)
+  done
+
+lemma wir_moel': "YS = YYS"
+  apply (rule antisym_less)
+  apply (rule lemma7)
+  apply (rule lemma6)
+  done
 
 end
-
diff -r f65265d71426 -r 86f21beabafc src/HOLCF/ex/Fix2.ML
--- a/src/HOLCF/ex/Fix2.ML	Sun May 28 19:54:20 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-(*  Title:      HOLCF/ex/Fix2.ML
-    ID:         $Id$
-    Author:     Franz Regensburger
-*)
-
-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";
-
-
-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 f65265d71426 -r 86f21beabafc src/HOLCF/ex/Fix2.thy
--- a/src/HOLCF/ex/Fix2.thy	Sun May 28 19:54:20 2006 +0200
+++ b/src/HOLCF/ex/Fix2.thy	Sun May 28 20:53:03 2006 +0200
@@ -17,6 +17,19 @@
   gix1_def: "F$(gix$F) = gix$F"
   gix2_def: "F$y=y ==> gix$F << y"
 
-ML {* use_legacy_bindings (the_context ()) *}
+
+lemma lemma1: "fix = gix"
+apply (rule ext_cfun)
+apply (rule antisym_less)
+apply (rule fix_least)
+apply (rule gix1_def)
+apply (rule gix2_def)
+apply (rule fix_eq [symmetric])
+done
+
+lemma lemma2: "gix$F=lub(range(%i. iterate i$F$UU))"
+apply (rule lemma1 [THEN subst])
+apply (rule fix_def2)
+done
 
 end
diff -r f65265d71426 -r 86f21beabafc src/HOLCF/ex/Focus_ex.ML
--- a/src/HOLCF/ex/Focus_ex.ML	Sun May 28 19:54:20 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,142 +0,0 @@
-
-(* $Id$ *)
-
-(* first some logical trading *)
-
-val prems = goal (the_context ())
-"is_g(g) = \ 
-\ (? 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 (the_context ())
-"(? 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)))";
-by (rtac iffI 1);
-by (etac exE 1);
-by (res_inst_tac [("x","f")] exI 1);
-by (REPEAT (etac conjE 1));
-by (etac conjI 1);
-by (strip_tac 1);
-by (etac allE 1);
-by (etac exE 1);
-by (res_inst_tac [("x","z")] exI 1);
-by (REPEAT (etac conjE 1));
-by (rtac conjI 1);
-by (rtac conjI 2);
-by (atac 3);
-by (dtac sym 1);
-by (asm_simp_tac HOLCF_ss 1);
-by (dtac sym 1);
-by (asm_simp_tac HOLCF_ss 1);
-by (etac exE 1);
-by (res_inst_tac [("x","f")] exI 1);
-by (REPEAT (etac conjE 1));
-by (etac conjI 1);
-by (strip_tac 1);
-by (etac allE 1);
-by (etac exE 1);
-by (res_inst_tac [("x","z")] exI 1);
-by (REPEAT (etac conjE 1));
-by (rtac conjI 1);
-by (atac 2);
-by (rtac trans 1);
-by (rtac (surjective_pairing_Cprod2) 2);
-by (etac subst 1);
-by (etac subst 1);
-by (rtac refl 1);
-val lemma2 = result();
-
-(* direction def_g(g) --> is_g(g) *)
-
-val prems = goal (the_context ()) "def_g(g) --> is_g(g)";
-by (simp_tac (HOL_ss addsimps [def_g,lemma1, lemma2]) 1);
-by (rtac impI 1);
-by (etac exE 1);
-by (res_inst_tac [("x","f")] exI 1);
-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 (rtac conjI 1);
- by (asm_simp_tac HOLCF_ss 1);
- by (rtac trans 1);
-  by (rtac surjective_pairing_Cprod2 2);
- by (rtac cfun_arg_cong 1);
- by (rtac trans 1);
-  by (rtac fix_eq 1);
- by (Simp_tac 1);
-by (strip_tac 1);
-by (rtac fix_least 1);
-by (Simp_tac 1);
-by (etac exE 1);
-by (dtac sym 1);
-back();
-by (asm_simp_tac HOLCF_ss 1);
-val lemma3 = result();
-
-(* direction is_g(g) --> def_g(g) *)
-val prems = goal (the_context ()) "is_g(g) --> def_g(g)";
-by (simp_tac (HOL_ss delsimps (ex_simps @ all_simps)
-                     addsimps [lemma1,lemma2,def_g]) 1);
-by (rtac impI 1);
-by (etac exE 1);
-by (res_inst_tac [("x","f")] exI 1);
-by (REPEAT (etac conjE 1));
-by (etac conjI 1);
-by (rtac ext_cfun 1);
-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 (asm_simp_tac HOLCF_ss 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 (fast_tac HOL_cs 1);
-by (rtac trans 1);
-by (rtac (surjective_pairing_Cprod2 RS sym) 1);
-by (etac cfun_arg_cong 1);
-by (strip_tac 1);
-by (REPEAT (etac allE 1));
-by (etac mp 1);
-by (etac sym 1);
-val lemma4 = result();
-
-(* now we assemble the result *)
-
-val prems = goal (the_context ()) "def_g = is_g";
-by (rtac ext 1);
-by (rtac iffI 1);
-by (etac (lemma3 RS mp) 1);
-by (etac (lemma4 RS mp) 1);
-val loopback_eq = result();
-
-val prems = goal (the_context ()) 
-"(? f.\
-\ is_f(f::'b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream))\
-\ -->\
-\ (? g. def_g(g::'b stream -> 'c stream ))";
-by (simp_tac (HOL_ss addsimps [def_g]) 1);
-val L2 = result();
-
-val prems = goal (the_context ()) 
-"(? f.\
-\ is_f(f::'b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream))\
-\ -->\
-\ (? g. is_g(g::'b stream -> 'c stream ))";
-by (rtac (loopback_eq RS subst) 1);
-by (rtac L2 1);
-val conservative_loopback = result();
diff -r f65265d71426 -r 86f21beabafc src/HOLCF/ex/Focus_ex.thy
--- a/src/HOLCF/ex/Focus_ex.thy	Sun May 28 19:54:20 2006 +0200
+++ b/src/HOLCF/ex/Focus_ex.thy	Sun May 28 20:53:03 2006 +0200
@@ -136,6 +136,142 @@
                         is_f f  &
                         g = (LAM x. cfst$(f$<x,fix$(LAM  k. csnd$(f$<x,k>))>)))"
 
-ML {* use_legacy_bindings (the_context ()) *}
+
+(* first some logical trading *)
+
+lemma lemma1:
+"is_g(g) =
+  (? f. is_f(f) &  (!x.(? z. <g$x,z> = f$<x,z> &
+                   (! w y. <y,w> = f$<x,w>  --> z << w))))"
+apply (simp add: is_g is_net_g)
+apply fast
+done
+
+lemma lemma2:
+"(? 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)))"
+apply (rule iffI)
+apply (erule exE)
+apply (rule_tac x = "f" in exI)
+apply (erule conjE)+
+apply (erule conjI)
+apply (intro strip)
+apply (erule allE)
+apply (erule exE)
+apply (rule_tac x = "z" in exI)
+apply (erule conjE)+
+apply (rule conjI)
+apply (rule_tac [2] conjI)
+prefer 3 apply (assumption)
+apply (drule sym)
+apply (tactic "asm_simp_tac HOLCF_ss 1")
+apply (drule sym)
+apply (tactic "asm_simp_tac HOLCF_ss 1")
+apply (erule exE)
+apply (rule_tac x = "f" in exI)
+apply (erule conjE)+
+apply (erule conjI)
+apply (intro strip)
+apply (erule allE)
+apply (erule exE)
+apply (rule_tac x = "z" in exI)
+apply (erule conjE)+
+apply (rule conjI)
+prefer 2 apply (assumption)
+apply (rule trans)
+apply (rule_tac [2] surjective_pairing_Cprod2)
+apply (erule subst)
+apply (erule subst)
+apply (rule refl)
+done
+
+lemma lemma3: "def_g(g) --> is_g(g)"
+apply (tactic {* simp_tac (HOL_ss addsimps [thm "def_g", thm "lemma1", thm "lemma2"]) 1 *})
+apply (rule impI)
+apply (erule exE)
+apply (rule_tac x = "f" in exI)
+apply (erule conjE)+
+apply (erule conjI)
+apply (intro strip)
+apply (rule_tac x = "fix$ (LAM k. csnd$ (f$<x,k>))" in exI)
+apply (rule conjI)
+ apply (tactic "asm_simp_tac HOLCF_ss 1")
+ apply (rule trans)
+  apply (rule_tac [2] surjective_pairing_Cprod2)
+ apply (rule cfun_arg_cong)
+ apply (rule trans)
+  apply (rule fix_eq)
+ apply (simp (no_asm))
+apply (intro strip)
+apply (rule fix_least)
+apply (simp (no_asm))
+apply (erule exE)
+apply (drule sym)
+back
+apply simp
+done
+
+lemma lemma4: "is_g(g) --> def_g(g)"
+apply (tactic {* simp_tac (HOL_ss delsimps (thms "ex_simps" @ thms "all_simps")
+  addsimps [thm "lemma1", thm "lemma2", thm "def_g"]) 1 *})
+apply (rule impI)
+apply (erule exE)
+apply (rule_tac x = "f" in exI)
+apply (erule conjE)+
+apply (erule conjI)
+apply (rule ext_cfun)
+apply (erule_tac x = "x" in allE)
+apply (erule exE)
+apply (erule conjE)+
+apply (subgoal_tac "fix$ (LAM k. csnd$ (f$<x, k>)) = z")
+ apply simp
+apply (subgoal_tac "! w y. f$<x, w> = <y, w> --> z << w")
+apply (rule sym)
+apply (rule fix_eqI)
+apply simp
+apply (rule allI)
+apply (tactic "simp_tac HOLCF_ss 1")
+apply (intro strip)
+apply (subgoal_tac "f$<x, za> = <cfst$ (f$<x,za>) ,za>")
+apply fast
+apply (rule trans)
+apply (rule surjective_pairing_Cprod2 [symmetric])
+apply (erule cfun_arg_cong)
+apply (intro strip)
+apply (erule allE)+
+apply (erule mp)
+apply (erule sym)
+done
+
+(* now we assemble the result *)
+
+lemma loopback_eq: "def_g = is_g"
+apply (rule ext)
+apply (rule iffI)
+apply (erule lemma3 [THEN mp])
+apply (erule lemma4 [THEN mp])
+done
+
+lemma L2:
+"(? f.
+  is_f(f::'b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream))
+  -->
+  (? g. def_g(g::'b stream -> 'c stream ))"
+apply (simp add: def_g)
+done
+
+theorem conservative_loopback:
+"(? f.
+  is_f(f::'b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream))
+  -->
+  (? g. is_g(g::'b stream -> 'c stream ))"
+apply (rule loopback_eq [THEN subst])
+apply (rule L2)
+done
 
 end
diff -r f65265d71426 -r 86f21beabafc src/HOLCF/ex/Hoare.ML
--- a/src/HOLCF/ex/Hoare.ML	Sun May 28 19:54:20 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,412 +0,0 @@
-(*  Title:      HOLCF/ex/hoare.ML
-    ID:         $Id$
-    Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
-*)
-
-(* --------- pure HOLCF logic, some little lemmas ------ *)
-
-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";
-
-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";
-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";
-by (hyp_subst_tac 1);
-by (rtac hoare_lemma2 1);
-by (etac exE 1);
-by (etac LeastI 1);
-qed "hoare_lemma5";
-
-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";
-
-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 (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";
-
-
-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 ----- *)
-
-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";
-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";
-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 (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 (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";
-
-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 (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 (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 (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
-
-*)
-
-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);
-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";
-
-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);
-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  (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";
-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 Rep_CFun_strict1 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";
-
-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) ------- *)
-
-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 Rep_CFun_strict1 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";
-
-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";
-
-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 Rep_CFun_strict1 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";
-
-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";
-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) ------- *)
-
-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
-*)
-
-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);
-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";
-
-
-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);
-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";
-
-(* ------- (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";
-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";
-
-(* ------------  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";
-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 ------ *)
-
-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";
diff -r f65265d71426 -r 86f21beabafc src/HOLCF/ex/Hoare.thy
--- a/src/HOLCF/ex/Hoare.thy	Sun May 28 19:54:20 2006 +0200
+++ b/src/HOLCF/ex/Hoare.thy	Sun May 28 20:53:03 2006 +0200
@@ -38,6 +38,407 @@
   q_def:  "q == fix$(LAM f. LAM x.
                  If b1$x orelse b2$x then f$(g$x) else x fi)"
 
-ML {* use_legacy_bindings (the_context ()) *}
+
+(* --------- pure HOLCF logic, some little lemmas ------ *)
+
+lemma hoare_lemma2: "b~=TT ==> b=FF | b=UU"
+apply (rule Exh_tr [THEN disjE])
+apply blast+
+done
+
+lemma hoare_lemma3: " (ALL k. b1$(iterate k$g$x) = TT) | (EX k. b1$(iterate k$g$x)~=TT)"
+apply blast
+done
+
+lemma hoare_lemma4: "(EX k. b1$(iterate k$g$x) ~= TT) ==>  
+  EX k. b1$(iterate k$g$x) = FF | b1$(iterate k$g$x) = UU"
+apply (erule exE)
+apply (rule exI)
+apply (rule hoare_lemma2)
+apply assumption
+done
+
+lemma hoare_lemma5: "[|(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"
+apply hypsubst
+apply (rule hoare_lemma2)
+apply (erule exE)
+apply (erule LeastI)
+done
+
+lemma hoare_lemma6: "b=UU ==> b~=TT"
+apply hypsubst
+apply (rule dist_eq_tr)
+done
+
+lemma hoare_lemma7: "b=FF ==> b~=TT"
+apply hypsubst
+apply (rule dist_eq_tr)
+done
+
+lemma hoare_lemma8: "[|(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"
+apply hypsubst
+apply (erule exE)
+apply (intro strip)
+apply (rule_tac p = "b1$ (iterate m$g$x) " in trE)
+prefer 2 apply (assumption)
+apply (rule le_less_trans [THEN less_irrefl])
+prefer 2 apply (assumption)
+apply (rule Least_le)
+apply (erule hoare_lemma6)
+apply (rule le_less_trans [THEN less_irrefl])
+prefer 2 apply (assumption)
+apply (rule Least_le)
+apply (erule hoare_lemma7)
+done
+
+
+lemma hoare_lemma28: "f$(y::'a)=(UU::tr) ==> f$UU = UU"
+apply (erule flat_codom [THEN disjE])
+apply auto
+done
+
+
+(* ----- access to definitions ----- *)
+
+lemma p_def3: "p$x = If b1$x then p$(g$x) else x fi"
+apply (rule trans)
+apply (rule p_def [THEN fix_eq3])
+apply simp
+done
+
+lemma q_def3: "q$x = If b1$x orelse b2$x then q$(g$x) else x fi"
+apply (rule trans)
+apply (rule q_def [THEN fix_eq3])
+apply simp
+done
+
+(** --------- proofs about iterations of p and q ---------- **)
+
+lemma hoare_lemma9: "(ALL m. m< Suc k --> b1$(iterate m$g$x)=TT) --> 
+   p$(iterate k$g$x)=p$x"
+apply (induct_tac k)
+apply (simp (no_asm))
+apply (simp (no_asm))
+apply (intro strip)
+apply (rule_tac s = "p$ (iterate n$g$x) " in trans)
+apply (rule trans)
+apply (rule_tac [2] p_def3 [symmetric])
+apply (rule_tac s = "TT" and t = "b1$ (iterate n$g$x) " in ssubst)
+apply (rule mp)
+apply (erule spec)
+apply (simp (no_asm) add: less_Suc_eq)
+apply simp
+apply (erule mp)
+apply (intro strip)
+apply (rule mp)
+apply (erule spec)
+apply (erule less_trans)
+apply simp
+done
+
+lemma hoare_lemma24: "(ALL m. m< Suc k --> b1$(iterate m$g$x)=TT) -->  
+  q$(iterate k$g$x)=q$x"
+apply (induct_tac k)
+apply (simp (no_asm))
+apply (simp (no_asm) add: less_Suc_eq)
+apply (intro strip)
+apply (rule_tac s = "q$ (iterate n$g$x) " in trans)
+apply (rule trans)
+apply (rule_tac [2] q_def3 [symmetric])
+apply (rule_tac s = "TT" and t = "b1$ (iterate n$g$x) " in ssubst)
+apply blast
+apply simp
+apply (erule mp)
+apply (intro strip)
+apply (fast dest!: less_Suc_eq [THEN iffD1])
+done
+
+(* -------- results about p for case (EX k. b1$(iterate k$g$x)~=TT) ------- *)
+
+thm hoare_lemma8 [THEN hoare_lemma9 [THEN mp], standard, no_vars]
+
+lemma hoare_lemma10:
+  "EX k. b1$(iterate k$g$x) ~= TT
+    ==> Suc k = (LEAST n. b1$(iterate n$g$x) ~= TT) ==> p$(iterate k$g$x) = p$x"
+  by (rule hoare_lemma8 [THEN hoare_lemma9 [THEN mp]])
+
+lemma hoare_lemma11: "(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"
+apply (case_tac "k")
+apply hypsubst
+apply (simp (no_asm))
+apply (intro strip)
+apply (erule conjE)
+apply (rule trans)
+apply (rule p_def3)
+apply simp
+apply hypsubst
+apply (intro strip)
+apply (erule conjE)
+apply (rule trans)
+apply (erule hoare_lemma10 [symmetric])
+apply assumption
+apply (rule trans)
+apply (rule p_def3)
+apply (rule_tac s = "TT" and t = "b1$ (iterate nat$g$x) " in ssubst)
+apply (rule hoare_lemma8 [THEN spec, THEN mp])
+apply assumption
+apply assumption
+apply (simp (no_asm))
+apply (tactic "simp_tac HOLCF_ss 1")
+apply (rule trans)
+apply (rule p_def3)
+apply (simp (no_asm) del: iterate_Suc add: iterate_Suc [symmetric])
+apply (erule_tac s = "FF" in ssubst)
+apply simp
+done
+
+lemma hoare_lemma12: "(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"
+apply (case_tac "k")
+apply hypsubst
+apply (simp (no_asm))
+apply (intro strip)
+apply (erule conjE)
+apply (rule trans)
+apply (rule p_def3)
+apply simp
+apply hypsubst
+apply (simp (no_asm))
+apply (intro strip)
+apply (erule conjE)
+apply (rule trans)
+apply (rule hoare_lemma10 [symmetric])
+apply assumption
+apply assumption
+apply (rule trans)
+apply (rule p_def3)
+apply (rule_tac s = "TT" and t = "b1$ (iterate nat$g$x) " in ssubst)
+apply (rule hoare_lemma8 [THEN spec, THEN mp])
+apply assumption
+apply assumption
+apply (simp (no_asm))
+apply (tactic "asm_simp_tac HOLCF_ss 1")
+apply (rule trans)
+apply (rule p_def3)
+apply simp
+done
+
+(* -------- results about p for case  (ALL k. b1$(iterate k$g$x)=TT) ------- *)
+
+lemma fernpass_lemma: "(ALL k. b1$(iterate k$g$x)=TT) ==> ALL k. p$(iterate k$g$x) = UU"
+apply (rule p_def [THEN def_fix_ind])
+apply (rule adm_all)
+apply (rule allI)
+apply (rule adm_eq)
+apply (tactic "cont_tacR 1")
+apply (rule allI)
+apply (subst Rep_CFun_strict1)
+apply (rule refl)
+apply (simp (no_asm))
+apply (rule allI)
+apply (rule_tac s = "TT" and t = "b1$ (iterate k$g$x) " in ssubst)
+apply (erule spec)
+apply (tactic "asm_simp_tac HOLCF_ss 1")
+apply (rule iterate_Suc [THEN subst])
+apply (erule spec)
+done
+
+lemma hoare_lemma16: "(ALL k. b1$(iterate k$g$x)=TT) ==> p$x = UU"
+apply (rule_tac F1 = "g" and t = "x" in iterate_0 [THEN subst])
+apply (erule fernpass_lemma [THEN spec])
+done
+
+(* -------- results about q for case  (ALL k. b1$(iterate k$g$x)=TT) ------- *)
+
+lemma hoare_lemma17: "(ALL k. b1$(iterate k$g$x)=TT) ==> ALL k. q$(iterate k$g$x) = UU"
+apply (rule q_def [THEN def_fix_ind])
+apply (rule adm_all)
+apply (rule allI)
+apply (rule adm_eq)
+apply (tactic "cont_tacR 1")
+apply (rule allI)
+apply (subst Rep_CFun_strict1)
+apply (rule refl)
+apply (rule allI)
+apply (simp (no_asm))
+apply (rule_tac s = "TT" and t = "b1$ (iterate k$g$x) " in ssubst)
+apply (erule spec)
+apply (tactic "asm_simp_tac HOLCF_ss 1")
+apply (rule iterate_Suc [THEN subst])
+apply (erule spec)
+done
+
+lemma hoare_lemma18: "(ALL k. b1$(iterate k$g$x)=TT) ==> q$x = UU"
+apply (rule_tac F1 = "g" and t = "x" in iterate_0 [THEN subst])
+apply (erule hoare_lemma17 [THEN spec])
+done
+
+lemma hoare_lemma19:
+  "(ALL k. (b1::'a->tr)$(iterate k$g$x)=TT) ==> b1$(UU::'a) = UU | (ALL y. b1$(y::'a)=TT)"
+apply (rule flat_codom)
+apply (rule_tac t = "x1" in iterate_0 [THEN subst])
+apply (erule spec)
+done
+
+lemma hoare_lemma20: "(ALL y. b1$(y::'a)=TT) ==> ALL k. q$(iterate k$g$(x::'a)) = UU"
+apply (rule q_def [THEN def_fix_ind])
+apply (rule adm_all)
+apply (rule allI)
+apply (rule adm_eq)
+apply (tactic "cont_tacR 1")
+apply (rule allI)
+apply (subst Rep_CFun_strict1)
+apply (rule refl)
+apply (rule allI)
+apply (simp (no_asm))
+apply (rule_tac s = "TT" and t = "b1$ (iterate k$g$ (x::'a))" in ssubst)
+apply (erule spec)
+apply (tactic "asm_simp_tac HOLCF_ss 1")
+apply (rule iterate_Suc [THEN subst])
+apply (erule spec)
+done
+
+lemma hoare_lemma21: "(ALL y. b1$(y::'a)=TT) ==> q$(x::'a) = UU"
+apply (rule_tac F1 = "g" and t = "x" in iterate_0 [THEN subst])
+apply (erule hoare_lemma20 [THEN spec])
+done
+
+lemma hoare_lemma22: "b1$(UU::'a)=UU ==> q$(UU::'a) = UU"
+apply (subst q_def3)
+apply simp
+done
+
+(* -------- results about q for case (EX k. b1$(iterate k$g$x) ~= TT) ------- *)
+
+lemma hoare_lemma25: "EX k. b1$(iterate k$g$x) ~= TT
+  ==> Suc k = (LEAST n. b1$(iterate n$g$x) ~= TT) ==> q$(iterate k$g$x) = q$x"
+  by (rule hoare_lemma8 [THEN hoare_lemma24 [THEN mp]])
+
+lemma hoare_lemma26: "(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)"
+apply (case_tac "k")
+apply hypsubst
+apply (intro strip)
+apply (simp (no_asm))
+apply hypsubst
+apply (intro strip)
+apply (erule conjE)
+apply (rule trans)
+apply (rule hoare_lemma25 [symmetric])
+apply assumption
+apply assumption
+apply (rule trans)
+apply (rule q_def3)
+apply (rule_tac s = "TT" and t = "b1$ (iterate nat$g$x) " in ssubst)
+apply (rule hoare_lemma8 [THEN spec, THEN mp])
+apply assumption
+apply assumption
+apply (simp (no_asm))
+apply (simp (no_asm))
+done
+
+
+lemma hoare_lemma27: "(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"
+apply (case_tac "k")
+apply hypsubst
+apply (simp (no_asm))
+apply (intro strip)
+apply (erule conjE)
+apply (subst q_def3)
+apply (tactic "asm_simp_tac HOLCF_ss 1")
+apply hypsubst
+apply (simp (no_asm))
+apply (intro strip)
+apply (erule conjE)
+apply (rule trans)
+apply (rule hoare_lemma25 [symmetric])
+apply assumption
+apply assumption
+apply (rule trans)
+apply (rule q_def3)
+apply (rule_tac s = "TT" and t = "b1$ (iterate nat$g$x) " in ssubst)
+apply (rule hoare_lemma8 [THEN spec, THEN mp])
+apply assumption
+apply assumption
+apply (simp (no_asm))
+apply (tactic "asm_simp_tac HOLCF_ss 1")
+apply (rule trans)
+apply (rule q_def3)
+apply (tactic "asm_simp_tac HOLCF_ss 1")
+done
+
+(* ------- (ALL k. b1$(iterate k$g$x)=TT) ==> q o p = q   ----- *)
+
+lemma hoare_lemma23: "(ALL k. b1$(iterate k$g$x)=TT) ==> q$(p$x) = q$x"
+apply (subst hoare_lemma16)
+apply assumption
+apply (rule hoare_lemma19 [THEN disjE])
+apply assumption
+apply (simplesubst hoare_lemma18)
+apply assumption
+apply (simplesubst hoare_lemma22)
+apply assumption
+apply (rule refl)
+apply (simplesubst hoare_lemma21)
+apply assumption
+apply (simplesubst hoare_lemma21)
+apply assumption
+apply (rule refl)
+done
+
+(* ------------  EX k. b1~(iterate k$g$x) ~= TT ==> q o p = q   ----- *)
+
+lemma hoare_lemma29: "EX k. b1$(iterate k$g$x) ~= TT ==> q$(p$x) = q$x"
+apply (rule hoare_lemma5 [THEN disjE])
+apply assumption
+apply (rule refl)
+apply (subst hoare_lemma11 [THEN mp])
+apply assumption
+apply (rule conjI)
+apply (rule refl)
+apply assumption
+apply (rule hoare_lemma26 [THEN mp, THEN subst])
+apply assumption
+apply (rule conjI)
+apply (rule refl)
+apply assumption
+apply (rule refl)
+apply (subst hoare_lemma12 [THEN mp])
+apply assumption
+apply (rule conjI)
+apply (rule refl)
+apply assumption
+apply (subst hoare_lemma22)
+apply (subst hoare_lemma28)
+apply assumption
+apply (rule refl)
+apply (rule sym)
+apply (subst hoare_lemma27 [THEN mp])
+apply assumption
+apply (rule conjI)
+apply (rule refl)
+apply assumption
+apply (rule refl)
+done
+
+(* ------ the main proof q o p = q ------ *)
+
+theorem hoare_main: "q oo p = q"
+apply (rule ext_cfun)
+apply (subst cfcomp2)
+apply (rule hoare_lemma3 [THEN disjE])
+apply (erule hoare_lemma23)
+apply (erule hoare_lemma29)
+done
 
 end
diff -r f65265d71426 -r 86f21beabafc src/HOLCF/ex/Loop.ML
--- a/src/HOLCF/ex/Loop.ML	Sun May 28 19:54:20 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,187 +0,0 @@
-(*  Title:      HOLCF/ex/Loop.ML
-    ID:         $Id$
-    Author:     Franz Regensburger
-
-Theory for a loop primitive like while
-*)
-
-(* ------------------------------------------------------------------------- *)
-(* access to definitions                                                     *)
-(* ------------------------------------------------------------------------- *)
-
-
-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)";
-by (Simp_tac 1);
-qed "while_def2";
-
-
-(* ------------------------------------------------------------------------- *)
-(* rekursive properties of while                                             *)
-(* ------------------------------------------------------------------------- *)
-
-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)";
-by (induct_tac "k" 1);
-by (simp_tac HOLCF_ss 1);
-by (rtac allI 1);
-by (rtac trans 1);
-by (stac while_unfold 1);
-by (rtac refl 2);
-by (stac iterate_Suc2 1);
-by (rtac trans 1);
-by (etac spec 2);
-by (stac step_def2 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 (etac (flat_codom RS disjE) 1);
-by (atac 1);
-by (etac spec 1);
-by (simp_tac HOLCF_ss 1);
-by (asm_simp_tac HOLCF_ss 1);
-by (asm_simp_tac HOLCF_ss 1);
-by (stac while_unfold 1);
-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);
-by (rtac (while_unfold2 RS spec) 1);
-by (Simp_tac 1);
-qed "while_unfold3";
-
-
-(* ------------------------------------------------------------------------- *)
-(* 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";
-by (Simp_tac 1);
-by (rtac trans 1);
-by (rtac step_def2 1);
-by (asm_simp_tac HOLCF_ss 1);
-by (etac exE 1);
-by (etac (flat_codom RS disjE) 1);
-by (asm_simp_tac HOLCF_ss 1);
-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";
-
-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)";
-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 (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 (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";
-by (induct_tac "k" 1);
-by (Simp_tac 1);
-by (strip_tac 1);
-by (stac while_unfold 1);
-by (asm_simp_tac HOLCF_ss 1);
-by (rtac allI 1);
-by (stac iterate_Suc2 1);
-by (strip_tac 1);
-by (rtac trans 1);
-by (rtac while_unfold3 1);
-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";
-by (stac while_def2 1);
-by (rtac fix_ind 1);
-by (rtac (allI RS adm_all) 1);
-by (rtac adm_eq 1);
-by (cont_tacR 1);
-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 (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 (etac spec 2);
-by (rtac cfun_arg_cong 1);
-by (rtac trans 1);
-by (rtac (iterate_Suc RS sym) 2);
-by (asm_simp_tac (HOLCF_ss addsimps [step_def2]) 1);
-by (Blast_tac 1);
-qed_spec_mp "loop_lemma5";
-
-
-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";
-by (blast_tac (claset() addIs [loop_lemma6]) 1);
-qed "loop_lemma7";
-
-
-(* ------------------------------------------------------------------------- *)
-(* an invariant rule for loops                                               *)
-(* ------------------------------------------------------------------------- *)
-
-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);
-by (etac loop_lemma7 1);
-by (stac (loop_lemma4) 1);
-by (atac 1);
-by (dtac spec 1 THEN etac mp 1);
-by (rtac conjI 1);
-by (atac 2);
-by (rtac (loop_lemma3) 1);
-by (assume_tac 1);
-by (blast_tac (claset() addIs [loop_lemma6]) 1);
-by (assume_tac 1);
-by (rotate_tac ~1 1);
-by (asm_full_simp_tac (simpset() addsimps [loop_lemma4]) 1);
-qed "loop_inv2";
-
-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)";
-by (rtac loop_inv2 1);
-by (rtac (premP RS premI) 3);
-by (rtac premW 3);
-by (blast_tac (claset() addIs [premTT]) 1);
-by (blast_tac (claset() addIs [premFF]) 1);
-qed "loop_inv";
diff -r f65265d71426 -r 86f21beabafc src/HOLCF/ex/Loop.thy
--- a/src/HOLCF/ex/Loop.thy	Sun May 28 19:54:20 2006 +0200
+++ b/src/HOLCF/ex/Loop.thy	Sun May 28 20:53:03 2006 +0200
@@ -12,11 +12,196 @@
 constdefs
   step  :: "('a -> tr)->('a -> 'a)->'a->'a"
   "step == (LAM b g x. If b$x then g$x else x fi)"
+
   while :: "('a -> tr)->('a -> 'a)->'a->'a"
   "while == (LAM b g. fix$(LAM f x.
     If b$x then f$(g$x) else x fi))"
 
-ML {* use_legacy_bindings (the_context ()) *}
+(* ------------------------------------------------------------------------- *)
+(* access to definitions                                                     *)
+(* ------------------------------------------------------------------------- *)
+
+
+lemma step_def2: "step$b$g$x = If b$x then g$x else x fi"
+apply (unfold step_def)
+apply simp
+done
+
+lemma while_def2: "while$b$g = fix$(LAM f x. If b$x then f$(g$x) else x fi)"
+apply (unfold while_def)
+apply simp
+done
+
+
+(* ------------------------------------------------------------------------- *)
+(* rekursive properties of while                                             *)
+(* ------------------------------------------------------------------------- *)
+
+lemma while_unfold: "while$b$g$x = If b$x then while$b$g$(g$x) else x fi"
+apply (rule trans)
+apply (rule while_def2 [THEN fix_eq5])
+apply simp
+done
+
+lemma while_unfold2: "ALL x. while$b$g$x = while$b$g$(iterate k$(step$b$g)$x)"
+apply (induct_tac k)
+apply simp
+apply (rule allI)
+apply (rule trans)
+apply (subst while_unfold)
+apply (rule_tac [2] refl)
+apply (subst iterate_Suc2)
+apply (rule trans)
+apply (erule_tac [2] spec)
+apply (subst step_def2)
+apply (rule_tac p = "b$x" in trE)
+apply simp
+apply (subst while_unfold)
+apply (rule_tac s = "UU" and t = "b$UU" in ssubst)
+apply (erule flat_codom [THEN disjE])
+apply assumption
+apply (erule spec)
+apply simp
+apply simp
+apply simp
+apply (subst while_unfold)
+apply simp
+done
+
+lemma while_unfold3: "while$b$g$x = while$b$g$(step$b$g$x)"
+apply (rule_tac s = "while$b$g$ (iterate (Suc 0) $ (step$b$g) $x) " in trans)
+apply (rule while_unfold2 [THEN spec])
+apply simp
+done
+
+
+(* ------------------------------------------------------------------------- *)
+(* properties of while and iterations                                        *)
+(* ------------------------------------------------------------------------- *)
+
+lemma loop_lemma1: "[| EX y. b$y=FF; iterate k$(step$b$g)$x = UU |]
+     ==>iterate(Suc k)$(step$b$g)$x=UU"
+apply (simp (no_asm))
+apply (rule trans)
+apply (rule step_def2)
+apply simp
+apply (erule exE)
+apply (erule flat_codom [THEN disjE])
+apply simp_all
+done
+
+lemma loop_lemma2: "[|EX y. b$y=FF;iterate (Suc k)$(step$b$g)$x ~=UU |]==>
+      iterate k$(step$b$g)$x ~=UU"
+apply (blast intro: loop_lemma1)
+done
+
+lemma loop_lemma3 [rule_format (no_asm)]:
+  "[| 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)"
+apply (induct_tac "k")
+apply (simp (no_asm_simp))
+apply (intro strip)
+apply (simp (no_asm) add: step_def2)
+apply (rule_tac p = "b$ (iterate n$ (step$b$g) $x) " in trE)
+apply (erule notE)
+apply (tactic {* asm_simp_tac (HOLCF_ss addsimps [thm "step_def2"]) 1 *})
+apply (tactic "asm_simp_tac HOLCF_ss 1")
+apply (rule mp)
+apply (erule spec)
+apply (tactic {* asm_simp_tac (HOLCF_ss delsimps [thm "iterate_Suc"]
+  addsimps [thm "loop_lemma2"]) 1 *})
+apply (rule_tac s = "iterate (Suc n) $ (step$b$g) $x"
+  and t = "g$ (iterate n$ (step$b$g) $x) " in ssubst)
+prefer 2 apply (assumption)
+apply (simp add: step_def2)
+apply (simp del: iterate_Suc add: loop_lemma2)
+done
+
+lemma loop_lemma4 [rule_format]:
+  "ALL x. b$(iterate k$(step$b$g)$x)=FF --> while$b$g$x= iterate k$(step$b$g)$x"
+apply (induct_tac k)
+apply (simp (no_asm))
+apply (intro strip)
+apply (simplesubst while_unfold)
+apply simp
+apply (rule allI)
+apply (simplesubst iterate_Suc2)
+apply (intro strip)
+apply (rule trans)
+apply (rule while_unfold3)
+apply simp
+done
+
+lemma loop_lemma5 [rule_format (no_asm)]:
+  "ALL k. b$(iterate k$(step$b$g)$x) ~= FF ==>
+    ALL m. while$b$g$(iterate m$(step$b$g)$x)=UU"
+apply (simplesubst while_def2)
+apply (rule fix_ind)
+apply (rule allI [THEN adm_all])
+apply (rule adm_eq)
+apply (tactic "cont_tacR 1")
+apply (simp (no_asm))
+apply (rule allI)
+apply (simp (no_asm))
+apply (rule_tac p = "b$ (iterate m$ (step$b$g) $x) " in trE)
+apply (simp (no_asm_simp))
+apply (simp (no_asm_simp))
+apply (rule_tac s = "xa$ (iterate (Suc m) $ (step$b$g) $x) " in trans)
+apply (erule_tac [2] spec)
+apply (rule cfun_arg_cong)
+apply (rule trans)
+apply (rule_tac [2] iterate_Suc [symmetric])
+apply (simp add: step_def2)
+apply blast
+done
+
+lemma loop_lemma6: "ALL k. b$(iterate k$(step$b$g)$x) ~= FF ==> while$b$g$x=UU"
+apply (rule_tac t = "x" in iterate_0 [THEN subst])
+apply (erule loop_lemma5)
+done
+
+lemma loop_lemma7: "while$b$g$x ~= UU ==> EX k. b$(iterate k$(step$b$g)$x) = FF"
+apply (blast intro: loop_lemma6)
+done
+
+
+(* ------------------------------------------------------------------------- *)
+(* an invariant rule for loops                                               *)
+(* ------------------------------------------------------------------------- *)
+
+lemma loop_inv2:
+"[| (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)"
+apply (rule_tac P = "%k. b$ (iterate k$ (step$b$g) $x) =FF" in exE)
+apply (erule loop_lemma7)
+apply (simplesubst loop_lemma4)
+apply assumption
+apply (drule spec, erule mp)
+apply (rule conjI)
+prefer 2 apply (assumption)
+apply (rule loop_lemma3)
+apply assumption
+apply (blast intro: loop_lemma6)
+apply assumption
+apply (rotate_tac -1)
+apply (simp add: loop_lemma4)
+done
+
+lemma loop_inv:
+  assumes premP: "P(x)"
+    and premI: "!!y. P y ==> INV y"
+    and premTT: "!!y. [| INV y; b$y=TT; g$y~=UU|] ==> INV (g$y)"
+    and premFF: "!!y. [| INV y; b$y=FF|] ==> Q y"
+    and premW: "while$b$g$x ~= UU"
+  shows "Q (while$b$g$x)"
+apply (rule loop_inv2)
+apply (rule_tac [3] premP [THEN premI])
+apply (rule_tac [3] premW)
+apply (blast intro: premTT)
+apply (blast intro: premFF)
+done
 
 end