# HG changeset patch
# User nipkow
# Date 758997626 -3600
# Node ID 929fc2c63bd0f71bc0b80658436102b8b75ec760
# Parent  c22b85994e179702a041ddfcd7211bae3df1d459
HOLCF examples

diff -r c22b85994e17 -r 929fc2c63bd0 src/HOLCF/ex/Coind.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/Coind.ML	Wed Jan 19 17:40:26 1994 +0100
@@ -0,0 +1,140 @@
+(*  Title: 	HOLCF/coind.ML
+    ID:         $Id$
+    Author: 	Franz Regensburger
+    Copyright   1993 Technische Universitaet Muenchen
+*)
+
+open Coind;
+
+(* ------------------------------------------------------------------------- *)
+(* expand fixed point properties                                             *)
+(* ------------------------------------------------------------------------- *)
+
+
+val nats_def2 = fix_prover Coind.thy nats_def 
+	"nats = scons[dzero][smap[dsucc][nats]]";
+
+val from_def2 = fix_prover Coind.thy from_def 
+	"from = (LAM n.scons[n][from[dsucc[n]]])";
+
+
+
+(* ------------------------------------------------------------------------- *)
+(* recursive  properties                                                     *)
+(* ------------------------------------------------------------------------- *)
+
+
+val from = prove_goal Coind.thy "from[n] = scons[n][from[dsucc[n]]]"
+ (fn prems =>
+	[
+	(rtac trans 1),
+	(rtac (from_def2 RS ssubst) 1),
+	(simp_tac HOLCF_ss  1),
+	(rtac refl 1)
+	]);
+
+
+val from1 = prove_goal Coind.thy "from[UU] = UU"
+ (fn prems =>
+	[
+	(rtac trans 1),
+	(rtac (from RS ssubst) 1),
+	(resolve_tac  stream_constrdef 1),
+	(rtac refl 1)
+	]);
+
+val coind_rews = 
+	[iterator1, iterator2, iterator3, smap1, smap2,from1];
+
+
+(* ------------------------------------------------------------------------- *)
+(* the example                                                               *)
+(* prove:        nats = from[dzero]                                          *)
+(* ------------------------------------------------------------------------- *)
+
+
+val coind_lemma1 = prove_goal Coind.thy "iterator[n][smap[dsucc]][nats] =\
+\		 scons[n][iterator[dsucc[n]][smap[dsucc]][nats]]"
+ (fn prems =>
+	[
+	(res_inst_tac [("s","n")] dnat_ind2 1),
+	(simp_tac (HOLCF_ss addsimps (coind_rews @ stream_rews)) 1),
+	(simp_tac (HOLCF_ss addsimps (coind_rews @ stream_rews)) 1),
+	(rtac trans 1),
+	(rtac nats_def2 1),
+	(simp_tac (HOLCF_ss addsimps (coind_rews @ dnat_rews)) 1),
+	(rtac trans 1),
+	(etac iterator3 1),
+	(rtac trans 1),
+	(asm_simp_tac HOLCF_ss 1),
+	(rtac trans 1),
+	(etac smap2 1),
+	(rtac cfun_arg_cong 1),
+	(asm_simp_tac (HOLCF_ss addsimps ([iterator3 RS sym] @ dnat_rews)) 1)
+	]);
+
+
+val nats_eq_from = prove_goal Coind.thy "nats = from[dzero]"
+ (fn prems =>
+	[
+	(res_inst_tac [("R",
+"% p q.? n. p = iterator[n][smap[dsucc]][nats] & q = from[n]")] stream_coind 1),
+	(res_inst_tac [("x","dzero")] exI 2),
+	(asm_simp_tac (HOLCF_ss addsimps coind_rews) 2),
+	(rewrite_goals_tac [stream_bisim_def]),
+	(strip_tac 1),
+	(etac exE 1),
+	(res_inst_tac [("Q","n=UU")] classical2 1),
+	(rtac disjI1 1),
+	(asm_simp_tac (HOLCF_ss addsimps coind_rews) 1),
+	(rtac disjI2 1),
+	(etac conjE 1),
+	(hyp_subst_tac 1),
+	(hyp_subst_tac 1),
+	(res_inst_tac [("x","n")] exI 1),
+	(res_inst_tac [("x","iterator[dsucc[n]][smap[dsucc]][nats]")] exI 1),
+	(res_inst_tac [("x","from[dsucc[n]]")] exI 1),
+	(etac conjI 1),
+	(rtac conjI 1),
+	(rtac coind_lemma1 1),
+	(rtac conjI 1),
+	(rtac from 1),
+	(res_inst_tac [("x","dsucc[n]")] exI 1),
+	(fast_tac HOL_cs 1)
+	]);
+
+(* another proof using stream_coind_lemma2 *)
+
+val nats_eq_from = prove_goal Coind.thy "nats = from[dzero]"
+ (fn prems =>
+	[
+	(res_inst_tac [("R","% p q.? n. p = \
+\	iterator[n][smap[dsucc]][nats] & q = from[n]")] stream_coind 1),
+	(rtac stream_coind_lemma2 1),
+	(strip_tac 1),
+	(etac exE 1),
+	(res_inst_tac [("Q","n=UU")] classical2 1),
+	(asm_simp_tac (HOLCF_ss addsimps coind_rews) 1),
+	(res_inst_tac [("x","UU::dnat")] exI 1),
+	(simp_tac (HOLCF_ss addsimps coind_rews addsimps stream_rews) 1),
+	(etac conjE 1),
+	(hyp_subst_tac 1),
+	(hyp_subst_tac 1),
+	(rtac conjI 1),
+	(rtac (coind_lemma1 RS ssubst) 1),
+	(rtac (from RS ssubst) 1),
+	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+	(res_inst_tac [("x","dsucc[n]")] exI 1),
+	(rtac conjI 1),
+	(rtac trans 1),
+	(rtac (coind_lemma1 RS ssubst) 1),
+	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+	(rtac refl 1),
+	(rtac trans 1),
+	(rtac (from RS ssubst) 1),
+	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+	(rtac refl 1),
+	(res_inst_tac [("x","dzero")] exI 1),
+	(asm_simp_tac (HOLCF_ss addsimps coind_rews) 1)
+	]);
+
diff -r c22b85994e17 -r 929fc2c63bd0 src/HOLCF/ex/Coind.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/Coind.thy	Wed Jan 19 17:40:26 1994 +0100
@@ -0,0 +1,37 @@
+(*  Title: 	HOLCF/coind.thy
+    ID:         $Id$
+    Author: 	Franz Regensburger
+    Copyright   1993 Technische Universitaet Muenchen
+
+Example for co-induction on streams
+*)
+
+Coind = Stream2 +
+
+
+consts
+
+nats		:: "dnat stream"
+from		:: "dnat -> dnat stream"
+
+rules
+
+nats_def	"nats = fix[LAM h.scons[dzero][smap[dsucc][h]]]"
+
+from_def	"from = fix[LAM h n.scons[n][h[dsucc[n]]]]"
+
+end
+
+(*
+
+		smap[f][UU] = UU
+      x~=UU --> smap[f][scons[x][xs]] = scons[f[x]][smap[f][xs]]
+
+		nats = scons[dzero][smap[dsucc][nats]]
+
+		from[n] = scons[n][from[dsucc[n]]]
+
+
+*)
+
+
diff -r c22b85994e17 -r 929fc2c63bd0 src/HOLCF/ex/Hoare.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/Hoare.ML	Wed Jan 19 17:40:26 1994 +0100
@@ -0,0 +1,540 @@
+(*  Title:	HOLCF/ex/hoare.ML
+    ID:         $Id$
+    Author: 	Franz Regensburger
+    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)
+	]);
+
+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)
+	]);
+
+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)
+	]);
+
+val hoare_lemma5 = prove_goal HOLCF.thy 
+"[|(? k.~ b1[iterate(k,g,x)]=TT);\
+\   k=theleast(%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 theleast1 1)
+	]);
+
+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)
+	]);
+
+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);\
+\   k=theleast(%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_anti_refl) 1),
+	(atac 2),
+	(rtac theleast2 1),
+	(etac hoare_lemma6 1),
+	(rtac (le_less_trans RS less_anti_refl) 1),
+	(atac 2),
+	(rtac theleast2 1),
+	(etac hoare_lemma7 1)
+	]);
+
+val hoare_lemma28 = prove_goal HOLCF.thy 
+"b1[y::'a]=UU::tr ==> b1[UU] = UU"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(etac (flat_tr RS flat_codom RS disjE) 1),
+	(atac 1),
+	(etac spec 1)
+	]);
+
+
+(* ----- access to definitions ----- *)
+
+val p_def2 = prove_goalw Hoare.thy [p_def]
+"p = fix[LAM f x. If b1[x] then f[g[x]] else x fi]"
+ (fn prems =>
+	[
+	(rtac refl 1)
+	]);
+
+val q_def2 = prove_goalw Hoare.thy [q_def]
+"q = fix[LAM f x. If b1[x] orelse b2[x] then \
+\     f[g[x]] else x fi]"
+ (fn prems =>
+	[
+	(rtac refl 1)
+	]);
+
+
+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 HOLCF_ss 1)
+	]);
+
+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 HOLCF_ss 1)
+	]);
+
+(** --------- 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 iterate_ss 1),
+	(simp_tac iterate_ss 1),
+	(strip_tac 1),
+	(res_inst_tac [("s","p[iterate(k1,g,x)]")] trans 1),
+	(rtac trans 1),
+	(rtac (p_def3 RS sym) 2),
+	(res_inst_tac [("s","TT"),("t","b1[iterate(k1,g,x)]")] ssubst 1),
+	(rtac mp 1),
+	(etac spec 1),
+	(simp_tac nat_ss 1),
+	(simp_tac HOLCF_ss 1),
+	(etac mp 1),
+	(strip_tac 1),
+	(rtac mp 1),
+	(etac spec 1),
+	(etac less_trans 1),
+	(simp_tac nat_ss 1)
+	]);
+
+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 iterate_ss 1),
+	(simp_tac iterate_ss 1),
+	(strip_tac 1),
+	(res_inst_tac [("s","q[iterate(k1,g,x)]")] trans 1),
+	(rtac trans 1),
+	(rtac (q_def3 RS sym) 2),
+	(res_inst_tac [("s","TT"),("t","b1[iterate(k1,g,x)]")] ssubst 1),
+	(rtac mp 1),
+	(etac spec 1),
+	(simp_tac nat_ss 1),
+	(simp_tac HOLCF_ss 1),
+	(etac mp 1),
+	(strip_tac 1),
+	(rtac mp 1),
+	(etac spec 1),
+	(etac less_trans 1),
+	(simp_tac nat_ss 1)
+	]);
+
+(* -------- results about p for case (? k.~ b1[iterate(k,g,x)]=TT) ------- *)
+
+
+val hoare_lemma10 = (hoare_lemma8 RS (hoare_lemma9 RS mp));
+(* 
+[| ? k. ~ b1[iterate(k,g,?x1)] = TT;
+   Suc(?k3) = theleast(%n. ~ b1[iterate(n,g,?x1)] = TT) |] ==>
+p[iterate(?k3,g,?x1)] = p[?x1]
+*)
+
+val hoare_lemma11 = prove_goal Hoare.thy 
+"(? n.b1[iterate(n,g,x)]~=TT) ==>\
+\ k=theleast(%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),
+	(res_inst_tac [("n","k")] natE 1),
+	(hyp_subst_tac 1),
+	(simp_tac iterate_ss 1),
+	(strip_tac 1),
+	(etac conjE 1),
+	(rtac trans 1),
+	(rtac p_def3 1),
+	(asm_simp_tac HOLCF_ss  1),
+	(eres_inst_tac [("s","0"),("t","theleast(%n. b1[iterate(n, g, x)] ~= TT)")]
+	subst 1),
+	(simp_tac iterate_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(xa,g,x)]")] ssubst 1),
+	(rtac (hoare_lemma8 RS spec RS mp) 1),
+	(atac 1),
+	(atac 1),
+	(simp_tac nat_ss 1),
+	(simp_tac HOLCF_ss 1),
+	(rtac trans 1),
+	(rtac p_def3 1),
+	(simp_tac (HOLCF_ss addsimps [iterate_Suc RS sym]) 1),
+	(eres_inst_tac [("s","FF")]	ssubst 1),
+	(simp_tac HOLCF_ss 1)
+	]);
+
+val hoare_lemma12 = prove_goal Hoare.thy 
+"(? n.~ b1[iterate(n,g,x)]=TT) ==>\
+\ k=theleast(%n.~ b1[iterate(n,g,x)]=TT) & b1[iterate(k,g,x)]=UU \
+\ --> p[x] = UU"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(res_inst_tac [("n","k")] natE 1),
+	(hyp_subst_tac 1),
+	(simp_tac iterate_ss 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 iterate_ss 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(xa,g,x)]")] ssubst 1),
+	(rtac (hoare_lemma8 RS spec RS mp) 1),
+	(atac 1),
+	(atac 1),
+	(simp_tac nat_ss 1),
+	(asm_simp_tac HOLCF_ss  1),
+	(rtac trans 1),
+	(rtac p_def3 1),
+	(asm_simp_tac HOLCF_ss  1)
+	]);
+
+(* -------- results about p for case  (! 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_def2 RS ssubst) 1),
+	(rtac fix_ind 1),
+	(rtac adm_all 1),
+	(rtac allI 1),
+	(rtac adm_eq 1),
+	(contX_tacR 1),
+	(rtac allI 1),
+	(rtac (strict_fapp1 RS ssubst) 1),
+	(rtac refl 1),
+	(simp_tac iterate_ss 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)
+	]);
+
+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) ------- *)
+
+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_def2 RS ssubst) 1),
+	(rtac fix_ind 1),
+	(rtac adm_all 1),
+	(rtac allI 1),
+	(rtac adm_eq 1),
+	(contX_tacR 1),
+	(rtac allI 1),
+	(rtac (strict_fapp1 RS ssubst) 1),
+	(rtac refl 1),
+	(rtac allI 1),
+	(simp_tac iterate_ss 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)
+	]);
+
+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)
+	]);
+
+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_tr RS flat_codom) 1),
+	(res_inst_tac [("t","x1")] (iterate_0 RS subst) 1),
+	(etac spec 1)
+	]);
+
+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_def2 RS ssubst) 1),
+	(rtac fix_ind 1),
+	(rtac adm_all 1),
+	(rtac allI 1),
+	(rtac adm_eq 1),
+	(contX_tacR 1),
+	(rtac allI 1),
+	(rtac (strict_fapp1 RS ssubst) 1),
+	(rtac refl 1),
+	(rtac allI 1),
+	(simp_tac iterate_ss 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)
+	]);
+
+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)
+	]);
+
+val hoare_lemma22 = prove_goal Hoare.thy 
+"b1[UU::'a]=UU ==> q[UU::'a] = UU"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(rtac (q_def3 RS ssubst) 1),
+	(asm_simp_tac HOLCF_ss  1)
+	]);
+
+(* -------- results about q for case (? k.~ b1[iterate(k,g,x)]=TT) ------- *)
+
+val hoare_lemma25 = (hoare_lemma8 RS (hoare_lemma24 RS mp) );
+(* 
+[| ? k. ~ ?b1.1[iterate(k,?g1,?x1)] = TT;
+   Suc(?k3) = theleast(%n. ~ ?b1.1[iterate(n,?g1,?x1)] = TT) |] ==>
+q[iterate(?k3,?g1,?x1)] = q[?x1]
+*)
+
+val hoare_lemma26 = prove_goal Hoare.thy 
+"(? n.~ b1[iterate(n,g,x)]=TT) ==>\
+\ k=theleast(%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),
+	(res_inst_tac [("n","k")] natE 1),
+	(hyp_subst_tac 1),
+	(strip_tac 1),
+	(simp_tac iterate_ss 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(xa,g,x)]")] ssubst 1),
+	(rtac (hoare_lemma8 RS spec RS mp) 1),
+	(atac 1),
+	(atac 1),
+	(simp_tac nat_ss 1),
+	(simp_tac (HOLCF_ss addsimps [iterate_Suc]) 1)
+	]);
+
+
+val hoare_lemma27 = prove_goal Hoare.thy 
+"(? n.~ b1[iterate(n,g,x)]=TT) ==>\
+\ k=theleast(%n.~ b1[iterate(n,g,x)]=TT) & b1[iterate(k,g,x)]=UU \
+\ --> q[x] = UU"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(res_inst_tac [("n","k")] natE 1),
+	(hyp_subst_tac 1),
+	(simp_tac iterate_ss 1),
+	(strip_tac 1),
+	(etac conjE 1),
+	(rtac (q_def3 RS ssubst) 1),
+	(asm_simp_tac HOLCF_ss  1),
+	(hyp_subst_tac 1),
+	(simp_tac iterate_ss 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(xa,g,x)]")] ssubst 1),
+	(rtac (hoare_lemma8 RS spec RS mp) 1),
+	(atac 1),
+	(atac 1),
+	(simp_tac nat_ss 1),
+	(asm_simp_tac HOLCF_ss 1),
+	(rtac trans 1),
+	(rtac q_def3 1),
+	(asm_simp_tac HOLCF_ss  1)
+	]);
+
+(* ------- (! 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),
+	(rtac (hoare_lemma16 RS ssubst) 1),
+	(atac 1),
+	(rtac (hoare_lemma19 RS disjE) 1),
+	(atac 1),
+	(rtac (hoare_lemma18 RS ssubst) 1),
+	(atac 1),
+	(rtac (hoare_lemma22 RS ssubst) 1),
+	(atac 1),
+	(rtac refl 1),
+	(rtac (hoare_lemma21 RS ssubst) 1),
+	(atac 1),
+	(rtac (hoare_lemma21 RS ssubst) 1),
+	(atac 1),
+	(rtac refl 1)
+	]);
+
+(* ------------  ? 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),
+	(rtac (hoare_lemma11 RS mp RS ssubst) 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),
+	(rtac (hoare_lemma12 RS mp RS ssubst) 1),
+	(atac 1),
+	(rtac conjI 1),
+	(rtac refl 1),
+	(atac 1),
+	(rtac (hoare_lemma22 RS ssubst) 1),
+	(rtac (hoare_lemma28 RS ssubst) 1),
+	(atac 1),
+	(rtac refl 1),
+	(rtac sym 1),
+	(rtac (hoare_lemma27 RS mp RS ssubst) 1),
+	(atac 1),
+	(rtac conjI 1),
+	(rtac refl 1),
+	(atac 1),
+	(rtac refl 1)
+	]);
+
+(* ------ the main prove q o p = q ------ *)
+
+val hoare_main = prove_goal Hoare.thy "q oo p = q"
+ (fn prems =>
+	[
+	(rtac ext_cfun 1),
+	(rtac (cfcomp2 RS ssubst) 1),
+	(rtac (hoare_lemma3 RS disjE) 1),
+	(etac hoare_lemma23 1),
+	(etac hoare_lemma29 1)
+	]);
+
+
diff -r c22b85994e17 -r 929fc2c63bd0 src/HOLCF/ex/Hoare.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/Hoare.thy	Wed Jan 19 17:40:26 1994 +0100
@@ -0,0 +1,43 @@
+(*  Title:	HOLCF/ex/hoare.thy
+    ID:         $Id$
+    Author: 	Franz Regensburger
+    Copyright	1993 Technische Universitaet Muenchen
+
+Theory for an example by C.A.R. Hoare 
+
+p x = if b1(x) 
+         then p(g(x))
+         else x fi
+
+q x = if b1(x) orelse b2(x) 
+         then q (g(x))
+         else x fi
+
+Prove: for all b1 b2 g . 
+            q o p  = q 
+
+In order to get a nice notation we fix the functions b1,b2 and g in the
+signature of this example
+
+*)
+
+Hoare = Tr2 +
+
+consts
+	b1:: "'a -> tr"
+	b2:: "'a -> tr"
+	 g:: "'a -> 'a"
+	p :: "'a -> 'a"
+	q :: "'a -> 'a"
+
+rules
+
+  p_def  "p == fix[LAM f. LAM x.\
+\                 If b1[x] then f[g[x]] else x fi]"
+
+  q_def  "q == fix[LAM f. LAM x.\
+\                 If b1[x] orelse b2[x] then f[g[x]] else x fi]"
+
+
+end
+ 
diff -r c22b85994e17 -r 929fc2c63bd0 src/HOLCF/ex/Loop.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/Loop.ML	Wed Jan 19 17:40:26 1994 +0100
@@ -0,0 +1,282 @@
+(*  Title:	HOLCF/ex/loop.ML
+    ID:         $Id$
+    Author: 	Franz Regensburger
+    Copyright	1993 Technische Universitaet Muenchen
+
+Lemmas for theory loop.thy
+*)
+
+open Loop;
+
+(* --------------------------------------------------------------------------- *)
+(* access to definitions                                                       *)
+(* --------------------------------------------------------------------------- *)
+
+val step_def2 = prove_goalw Loop.thy [step_def]
+"step[b][g][x] = If b[x] then g[x] else x fi"
+ (fn prems =>
+	[
+	(simp_tac Cfun_ss 1)
+	]);
+
+val while_def2 = prove_goalw Loop.thy [while_def]
+"while[b][g] = fix[LAM f x. If b[x] then f[g[x]] else x fi]"
+ (fn prems =>
+	[
+	(simp_tac Cfun_ss 1)
+	]);
+
+
+(* ------------------------------------------------------------------------- *)
+(* rekursive properties of while                                             *)
+(* ------------------------------------------------------------------------- *)
+
+val while_unfold = prove_goal Loop.thy 
+"while[b][g][x] = If b[x] then while[b][g][g[x]] else x fi"
+ (fn prems =>
+	[
+	(fix_tac5  while_def2 1),
+	(simp_tac Cfun_ss 1)
+	]);
+
+val while_unfold2 = prove_goal Loop.thy 
+	"!x.while[b][g][x] = while[b][g][iterate(k,step[b][g],x)]"
+ (fn prems =>
+	[
+	(nat_ind_tac "k" 1),
+	(simp_tac (HOLCF_ss addsimps [iterate_0,iterate_Suc]) 1),
+	(rtac allI 1),
+	(rtac trans 1),
+	(rtac (while_unfold RS ssubst) 1),
+	(rtac refl 2),
+	(rtac (iterate_Suc2 RS ssubst) 1),
+	(rtac trans 1),
+	(etac spec 2),
+	(rtac (step_def2 RS ssubst) 1),
+	(res_inst_tac [("p","b[x]")] trE 1),
+	(asm_simp_tac HOLCF_ss 1),
+	(rtac (while_unfold RS ssubst) 1),
+	(res_inst_tac [("s","UU"),("t","b[UU]")] ssubst 1),
+	(etac (flat_tr RS flat_codom RS disjE) 1),
+	(atac 1),
+	(etac spec 1),
+	(simp_tac HOLCF_ss 1),
+	(asm_simp_tac HOLCF_ss 1),
+	(asm_simp_tac HOLCF_ss 1),
+	(rtac (while_unfold RS ssubst) 1),
+	(asm_simp_tac HOLCF_ss 1)
+	]);
+
+val while_unfold3 = prove_goal Loop.thy 
+	"while[b][g][x] = while[b][g][step[b][g][x]]"
+ (fn prems =>
+	[
+	(res_inst_tac [("s","while[b][g][iterate(Suc(0),step[b][g],x)]")] trans 1),
+	(rtac (while_unfold2 RS spec) 1),
+	(simp_tac iterate_ss 1)
+	]);
+
+
+(* --------------------------------------------------------------------------- *)
+(* properties of while and iterations                                          *)
+(* --------------------------------------------------------------------------- *)
+
+val loop_lemma1 = prove_goal Loop.thy
+"[|? y.b[y]=FF; iterate(k,step[b][g],x)=UU|]==>iterate(Suc(k),step[b][g],x)=UU"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(simp_tac iterate_ss 1),
+	(rtac trans 1),
+	(rtac step_def2 1),
+	(asm_simp_tac HOLCF_ss 1),
+	(etac exE 1),
+	(etac (flat_tr RS flat_codom RS disjE) 1),
+	(asm_simp_tac HOLCF_ss 1),
+	(asm_simp_tac HOLCF_ss 1)
+	]);
+
+val loop_lemma2 = prove_goal Loop.thy
+"[|? y.b[y]=FF;~iterate(Suc(k),step[b][g],x)=UU |]==>\
+\~iterate(k,step[b][g],x)=UU"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(rtac contrapos 1),
+	(etac  loop_lemma1 2),
+	(atac 1),
+	(atac 1)
+	]);
+
+val loop_lemma3 = prove_goal Loop.thy
+"[|!x. INV(x) & b[x]=TT & ~g[x]=UU --> INV(g[x]);\
+\? y.b[y]=FF; INV(x)|] ==>\
+\~iterate(k,step[b][g],x)=UU --> INV(iterate(k,step[b][g],x))"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(nat_ind_tac "k" 1),
+	(asm_simp_tac iterate_ss 1),
+	(strip_tac 1),
+	(simp_tac (iterate_ss addsimps [step_def2]) 1),
+	(res_inst_tac [("p","b[iterate(k1, step[b][g], x)]")] trE 1),
+	(etac notE 1),
+	(asm_simp_tac (HOLCF_ss addsimps [step_def2,iterate_Suc] ) 1),
+	(asm_simp_tac HOLCF_ss  1),
+	(rtac mp 1),
+	(etac spec  1),
+	(asm_simp_tac (HOLCF_ss addsimps [loop_lemma2] ) 1),
+	(res_inst_tac [("s","iterate(Suc(k1), step[b][g], x)"),
+		("t","g[iterate(k1, step[b][g], x)]")] ssubst 1),
+	(atac 2),
+	(asm_simp_tac (HOLCF_ss addsimps [iterate_Suc,step_def2] ) 1),
+	(asm_simp_tac (HOLCF_ss addsimps [loop_lemma2] ) 1)
+	]);
+
+
+val loop_lemma4 = prove_goal Loop.thy
+"!x. b[iterate(k,step[b][g],x)]=FF --> while[b][g][x]=iterate(k,step[b][g],x)"
+ (fn prems =>
+	[
+	(nat_ind_tac "k" 1),
+	(simp_tac iterate_ss 1),
+	(strip_tac 1),
+	(rtac (while_unfold RS ssubst) 1),
+	(asm_simp_tac HOLCF_ss  1),
+	(rtac allI 1),
+	(rtac (iterate_Suc2 RS ssubst) 1),
+	(strip_tac 1),
+	(rtac trans 1),
+	(rtac while_unfold3 1),
+	(asm_simp_tac HOLCF_ss  1)
+	]);
+
+val loop_lemma5 = prove_goal Loop.thy
+"!k. ~b[iterate(k,step[b][g],x)]=FF ==>\
+\ !m. while[b][g][iterate(m,step[b][g],x)]=UU"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(rtac (while_def2 RS ssubst) 1),
+	(rtac fix_ind 1),
+	(rtac (allI RS adm_all) 1),
+	(rtac adm_eq 1),
+	(contX_tacR 1),
+	(simp_tac HOLCF_ss  1),
+	(rtac allI 1),
+	(simp_tac HOLCF_ss  1),
+	(res_inst_tac [("p","b[iterate(m, step[b][g],x)]")] trE 1),
+	(asm_simp_tac HOLCF_ss  1),
+	(asm_simp_tac HOLCF_ss  1),
+	(res_inst_tac [("s","xa[iterate(Suc(m), step[b][g], x)]")] trans 1),
+	(etac spec 2),
+	(rtac cfun_arg_cong 1),
+	(rtac trans 1),
+	(rtac (iterate_Suc RS sym) 2),
+	(asm_simp_tac (HOLCF_ss addsimps [step_def2]) 1),
+	(dtac spec 1),
+	(contr_tac 1)
+	]);
+
+
+val loop_lemma6 = prove_goal Loop.thy
+"!k. ~b[iterate(k,step[b][g],x)]=FF ==> while[b][g][x]=UU"
+ (fn prems =>
+	[
+	(res_inst_tac [("t","x")] (iterate_0 RS subst) 1),
+	(rtac (loop_lemma5 RS spec) 1),
+	(resolve_tac prems 1)
+	]);
+
+val loop_lemma7 = prove_goal Loop.thy
+"~while[b][g][x]=UU ==> ? k. b[iterate(k,step[b][g],x)]=FF"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(etac swap 1),
+	(rtac loop_lemma6 1),
+	(fast_tac HOL_cs 1)
+	]);
+
+val loop_lemma8 = prove_goal Loop.thy
+"~while[b][g][x]=UU ==> ? y. b[y]=FF"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(dtac loop_lemma7 1),
+	(fast_tac HOL_cs 1)
+	]);
+
+
+(* --------------------------------------------------------------------------- *)
+(* an invariant rule for loops                                                 *)
+(* --------------------------------------------------------------------------- *)
+
+val loop_inv2 = prove_goal Loop.thy
+"[| (!y. INV(y) & b[y]=TT & ~g[y]=UU --> INV(g[y]));\
+\   (!y. INV(y) & b[y]=FF --> Q(y));\
+\   INV(x); ~while[b][g][x]=UU |] ==> Q(while[b][g][x])"
+ (fn prems =>
+	[
+	(res_inst_tac [("P","%k.b[iterate(k,step[b][g],x)]=FF")] exE 1),
+	(rtac loop_lemma7 1),
+	(resolve_tac prems 1),
+	(rtac ((loop_lemma4 RS spec RS mp) RS ssubst) 1),
+	(atac 1),
+	(rtac (nth_elem (1,prems) RS spec RS mp) 1),
+	(rtac conjI 1),
+	(atac 2),
+	(rtac (loop_lemma3 RS mp) 1),
+	(resolve_tac prems 1),
+	(rtac loop_lemma8 1),
+	(resolve_tac prems 1),
+	(resolve_tac prems 1),
+	(rtac classical3 1),
+	(resolve_tac prems 1),
+	(etac box_equals 1),
+	(rtac (loop_lemma4 RS spec RS mp RS sym) 1),
+	(atac 1),
+	(rtac refl 1)
+	]);
+
+val loop_inv3 = prove_goal Loop.thy
+"[| !!y.[| INV(y); b[y]=TT; ~g[y]=UU|] ==> INV(g[y]);\
+\   !!y.[| INV(y); b[y]=FF|]==> Q(y);\
+\   INV(x); ~while[b][g][x]=UU |] ==> Q(while[b][g][x])"
+ (fn prems =>
+	[
+	(rtac loop_inv2 1),
+	(rtac allI 1),
+	(rtac impI 1),
+	(resolve_tac prems 1),
+	(fast_tac HOL_cs 1),
+	(fast_tac HOL_cs 1),
+	(fast_tac HOL_cs 1),
+	(rtac allI 1),
+	(rtac impI 1),
+	(resolve_tac prems 1),
+	(fast_tac HOL_cs 1),
+	(fast_tac HOL_cs 1),
+	(resolve_tac prems 1),
+	(resolve_tac prems 1)
+	]);
+
+val loop_inv = prove_goal Loop.thy
+"[| 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])"
+ (fn prems =>
+	[
+	(rtac loop_inv3 1),
+	(eresolve_tac prems 1),
+	(atac 1),
+	(atac 1),
+	(resolve_tac prems 1),
+	(atac 1),
+	(atac 1),
+	(resolve_tac prems 1),
+	(resolve_tac prems 1),
+	(resolve_tac prems 1)
+	]);
diff -r c22b85994e17 -r 929fc2c63bd0 src/HOLCF/ex/Loop.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/Loop.thy	Wed Jan 19 17:40:26 1994 +0100
@@ -0,0 +1,24 @@
+(*  Title:	HOLCF/ex/loop.thy
+    ID:         $Id$
+    Author: 	Franz Regensburger
+    Copyright	1993 Technische Universitaet Muenchen
+
+Theory for a loop primitive like while
+*)
+
+Loop = Tr2 +
+
+consts
+
+	step  :: "('a -> tr)->('a -> 'a)->'a->'a"
+	while :: "('a -> tr)->('a -> 'a)->'a->'a"
+
+rules
+
+  step_def	"step == (LAM b g x. If b[x] then g[x] else x fi)"
+  while_def	"while == (LAM b g. fix[LAM f x.\
+\                 If b[x] then f[g[x]] else x fi])"
+
+
+end
+ 
diff -r c22b85994e17 -r 929fc2c63bd0 src/HOLCF/ex/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/ROOT.ML	Wed Jan 19 17:40:26 1994 +0100
@@ -0,0 +1,16 @@
+(*  Title:  	HOLCF/ex/ROOT
+    ID:         $Id$
+    Author: 	Tobias Nipkow
+    Copyright   1994 TU Muenchen
+
+Executes all examples for HOLCF. 
+*)
+
+HOLCF_build_completed;    (*Cause examples to fail if HOLCF did*)
+
+writeln"Root file for HOLCF examples";
+proof_timing := true;
+time_use_thy "ex/Coind";
+time_use_thy "ex/Hoare";
+time_use_thy "ex/Loop";
+maketest     "END: Root file for HOLCF examples";
diff -r c22b85994e17 -r 929fc2c63bd0 src/HOLCF/ex/coind.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/coind.ML	Wed Jan 19 17:40:26 1994 +0100
@@ -0,0 +1,140 @@
+(*  Title: 	HOLCF/coind.ML
+    ID:         $Id$
+    Author: 	Franz Regensburger
+    Copyright   1993 Technische Universitaet Muenchen
+*)
+
+open Coind;
+
+(* ------------------------------------------------------------------------- *)
+(* expand fixed point properties                                             *)
+(* ------------------------------------------------------------------------- *)
+
+
+val nats_def2 = fix_prover Coind.thy nats_def 
+	"nats = scons[dzero][smap[dsucc][nats]]";
+
+val from_def2 = fix_prover Coind.thy from_def 
+	"from = (LAM n.scons[n][from[dsucc[n]]])";
+
+
+
+(* ------------------------------------------------------------------------- *)
+(* recursive  properties                                                     *)
+(* ------------------------------------------------------------------------- *)
+
+
+val from = prove_goal Coind.thy "from[n] = scons[n][from[dsucc[n]]]"
+ (fn prems =>
+	[
+	(rtac trans 1),
+	(rtac (from_def2 RS ssubst) 1),
+	(simp_tac HOLCF_ss  1),
+	(rtac refl 1)
+	]);
+
+
+val from1 = prove_goal Coind.thy "from[UU] = UU"
+ (fn prems =>
+	[
+	(rtac trans 1),
+	(rtac (from RS ssubst) 1),
+	(resolve_tac  stream_constrdef 1),
+	(rtac refl 1)
+	]);
+
+val coind_rews = 
+	[iterator1, iterator2, iterator3, smap1, smap2,from1];
+
+
+(* ------------------------------------------------------------------------- *)
+(* the example                                                               *)
+(* prove:        nats = from[dzero]                                          *)
+(* ------------------------------------------------------------------------- *)
+
+
+val coind_lemma1 = prove_goal Coind.thy "iterator[n][smap[dsucc]][nats] =\
+\		 scons[n][iterator[dsucc[n]][smap[dsucc]][nats]]"
+ (fn prems =>
+	[
+	(res_inst_tac [("s","n")] dnat_ind2 1),
+	(simp_tac (HOLCF_ss addsimps (coind_rews @ stream_rews)) 1),
+	(simp_tac (HOLCF_ss addsimps (coind_rews @ stream_rews)) 1),
+	(rtac trans 1),
+	(rtac nats_def2 1),
+	(simp_tac (HOLCF_ss addsimps (coind_rews @ dnat_rews)) 1),
+	(rtac trans 1),
+	(etac iterator3 1),
+	(rtac trans 1),
+	(asm_simp_tac HOLCF_ss 1),
+	(rtac trans 1),
+	(etac smap2 1),
+	(rtac cfun_arg_cong 1),
+	(asm_simp_tac (HOLCF_ss addsimps ([iterator3 RS sym] @ dnat_rews)) 1)
+	]);
+
+
+val nats_eq_from = prove_goal Coind.thy "nats = from[dzero]"
+ (fn prems =>
+	[
+	(res_inst_tac [("R",
+"% p q.? n. p = iterator[n][smap[dsucc]][nats] & q = from[n]")] stream_coind 1),
+	(res_inst_tac [("x","dzero")] exI 2),
+	(asm_simp_tac (HOLCF_ss addsimps coind_rews) 2),
+	(rewrite_goals_tac [stream_bisim_def]),
+	(strip_tac 1),
+	(etac exE 1),
+	(res_inst_tac [("Q","n=UU")] classical2 1),
+	(rtac disjI1 1),
+	(asm_simp_tac (HOLCF_ss addsimps coind_rews) 1),
+	(rtac disjI2 1),
+	(etac conjE 1),
+	(hyp_subst_tac 1),
+	(hyp_subst_tac 1),
+	(res_inst_tac [("x","n")] exI 1),
+	(res_inst_tac [("x","iterator[dsucc[n]][smap[dsucc]][nats]")] exI 1),
+	(res_inst_tac [("x","from[dsucc[n]]")] exI 1),
+	(etac conjI 1),
+	(rtac conjI 1),
+	(rtac coind_lemma1 1),
+	(rtac conjI 1),
+	(rtac from 1),
+	(res_inst_tac [("x","dsucc[n]")] exI 1),
+	(fast_tac HOL_cs 1)
+	]);
+
+(* another proof using stream_coind_lemma2 *)
+
+val nats_eq_from = prove_goal Coind.thy "nats = from[dzero]"
+ (fn prems =>
+	[
+	(res_inst_tac [("R","% p q.? n. p = \
+\	iterator[n][smap[dsucc]][nats] & q = from[n]")] stream_coind 1),
+	(rtac stream_coind_lemma2 1),
+	(strip_tac 1),
+	(etac exE 1),
+	(res_inst_tac [("Q","n=UU")] classical2 1),
+	(asm_simp_tac (HOLCF_ss addsimps coind_rews) 1),
+	(res_inst_tac [("x","UU::dnat")] exI 1),
+	(simp_tac (HOLCF_ss addsimps coind_rews addsimps stream_rews) 1),
+	(etac conjE 1),
+	(hyp_subst_tac 1),
+	(hyp_subst_tac 1),
+	(rtac conjI 1),
+	(rtac (coind_lemma1 RS ssubst) 1),
+	(rtac (from RS ssubst) 1),
+	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+	(res_inst_tac [("x","dsucc[n]")] exI 1),
+	(rtac conjI 1),
+	(rtac trans 1),
+	(rtac (coind_lemma1 RS ssubst) 1),
+	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+	(rtac refl 1),
+	(rtac trans 1),
+	(rtac (from RS ssubst) 1),
+	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+	(rtac refl 1),
+	(res_inst_tac [("x","dzero")] exI 1),
+	(asm_simp_tac (HOLCF_ss addsimps coind_rews) 1)
+	]);
+
diff -r c22b85994e17 -r 929fc2c63bd0 src/HOLCF/ex/coind.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/coind.thy	Wed Jan 19 17:40:26 1994 +0100
@@ -0,0 +1,37 @@
+(*  Title: 	HOLCF/coind.thy
+    ID:         $Id$
+    Author: 	Franz Regensburger
+    Copyright   1993 Technische Universitaet Muenchen
+
+Example for co-induction on streams
+*)
+
+Coind = Stream2 +
+
+
+consts
+
+nats		:: "dnat stream"
+from		:: "dnat -> dnat stream"
+
+rules
+
+nats_def	"nats = fix[LAM h.scons[dzero][smap[dsucc][h]]]"
+
+from_def	"from = fix[LAM h n.scons[n][h[dsucc[n]]]]"
+
+end
+
+(*
+
+		smap[f][UU] = UU
+      x~=UU --> smap[f][scons[x][xs]] = scons[f[x]][smap[f][xs]]
+
+		nats = scons[dzero][smap[dsucc][nats]]
+
+		from[n] = scons[n][from[dsucc[n]]]
+
+
+*)
+
+
diff -r c22b85994e17 -r 929fc2c63bd0 src/HOLCF/ex/hoare.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/hoare.ML	Wed Jan 19 17:40:26 1994 +0100
@@ -0,0 +1,540 @@
+(*  Title:	HOLCF/ex/hoare.ML
+    ID:         $Id$
+    Author: 	Franz Regensburger
+    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)
+	]);
+
+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)
+	]);
+
+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)
+	]);
+
+val hoare_lemma5 = prove_goal HOLCF.thy 
+"[|(? k.~ b1[iterate(k,g,x)]=TT);\
+\   k=theleast(%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 theleast1 1)
+	]);
+
+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)
+	]);
+
+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);\
+\   k=theleast(%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_anti_refl) 1),
+	(atac 2),
+	(rtac theleast2 1),
+	(etac hoare_lemma6 1),
+	(rtac (le_less_trans RS less_anti_refl) 1),
+	(atac 2),
+	(rtac theleast2 1),
+	(etac hoare_lemma7 1)
+	]);
+
+val hoare_lemma28 = prove_goal HOLCF.thy 
+"b1[y::'a]=UU::tr ==> b1[UU] = UU"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(etac (flat_tr RS flat_codom RS disjE) 1),
+	(atac 1),
+	(etac spec 1)
+	]);
+
+
+(* ----- access to definitions ----- *)
+
+val p_def2 = prove_goalw Hoare.thy [p_def]
+"p = fix[LAM f x. If b1[x] then f[g[x]] else x fi]"
+ (fn prems =>
+	[
+	(rtac refl 1)
+	]);
+
+val q_def2 = prove_goalw Hoare.thy [q_def]
+"q = fix[LAM f x. If b1[x] orelse b2[x] then \
+\     f[g[x]] else x fi]"
+ (fn prems =>
+	[
+	(rtac refl 1)
+	]);
+
+
+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 HOLCF_ss 1)
+	]);
+
+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 HOLCF_ss 1)
+	]);
+
+(** --------- 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 iterate_ss 1),
+	(simp_tac iterate_ss 1),
+	(strip_tac 1),
+	(res_inst_tac [("s","p[iterate(k1,g,x)]")] trans 1),
+	(rtac trans 1),
+	(rtac (p_def3 RS sym) 2),
+	(res_inst_tac [("s","TT"),("t","b1[iterate(k1,g,x)]")] ssubst 1),
+	(rtac mp 1),
+	(etac spec 1),
+	(simp_tac nat_ss 1),
+	(simp_tac HOLCF_ss 1),
+	(etac mp 1),
+	(strip_tac 1),
+	(rtac mp 1),
+	(etac spec 1),
+	(etac less_trans 1),
+	(simp_tac nat_ss 1)
+	]);
+
+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 iterate_ss 1),
+	(simp_tac iterate_ss 1),
+	(strip_tac 1),
+	(res_inst_tac [("s","q[iterate(k1,g,x)]")] trans 1),
+	(rtac trans 1),
+	(rtac (q_def3 RS sym) 2),
+	(res_inst_tac [("s","TT"),("t","b1[iterate(k1,g,x)]")] ssubst 1),
+	(rtac mp 1),
+	(etac spec 1),
+	(simp_tac nat_ss 1),
+	(simp_tac HOLCF_ss 1),
+	(etac mp 1),
+	(strip_tac 1),
+	(rtac mp 1),
+	(etac spec 1),
+	(etac less_trans 1),
+	(simp_tac nat_ss 1)
+	]);
+
+(* -------- results about p for case (? k.~ b1[iterate(k,g,x)]=TT) ------- *)
+
+
+val hoare_lemma10 = (hoare_lemma8 RS (hoare_lemma9 RS mp));
+(* 
+[| ? k. ~ b1[iterate(k,g,?x1)] = TT;
+   Suc(?k3) = theleast(%n. ~ b1[iterate(n,g,?x1)] = TT) |] ==>
+p[iterate(?k3,g,?x1)] = p[?x1]
+*)
+
+val hoare_lemma11 = prove_goal Hoare.thy 
+"(? n.b1[iterate(n,g,x)]~=TT) ==>\
+\ k=theleast(%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),
+	(res_inst_tac [("n","k")] natE 1),
+	(hyp_subst_tac 1),
+	(simp_tac iterate_ss 1),
+	(strip_tac 1),
+	(etac conjE 1),
+	(rtac trans 1),
+	(rtac p_def3 1),
+	(asm_simp_tac HOLCF_ss  1),
+	(eres_inst_tac [("s","0"),("t","theleast(%n. b1[iterate(n, g, x)] ~= TT)")]
+	subst 1),
+	(simp_tac iterate_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(xa,g,x)]")] ssubst 1),
+	(rtac (hoare_lemma8 RS spec RS mp) 1),
+	(atac 1),
+	(atac 1),
+	(simp_tac nat_ss 1),
+	(simp_tac HOLCF_ss 1),
+	(rtac trans 1),
+	(rtac p_def3 1),
+	(simp_tac (HOLCF_ss addsimps [iterate_Suc RS sym]) 1),
+	(eres_inst_tac [("s","FF")]	ssubst 1),
+	(simp_tac HOLCF_ss 1)
+	]);
+
+val hoare_lemma12 = prove_goal Hoare.thy 
+"(? n.~ b1[iterate(n,g,x)]=TT) ==>\
+\ k=theleast(%n.~ b1[iterate(n,g,x)]=TT) & b1[iterate(k,g,x)]=UU \
+\ --> p[x] = UU"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(res_inst_tac [("n","k")] natE 1),
+	(hyp_subst_tac 1),
+	(simp_tac iterate_ss 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 iterate_ss 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(xa,g,x)]")] ssubst 1),
+	(rtac (hoare_lemma8 RS spec RS mp) 1),
+	(atac 1),
+	(atac 1),
+	(simp_tac nat_ss 1),
+	(asm_simp_tac HOLCF_ss  1),
+	(rtac trans 1),
+	(rtac p_def3 1),
+	(asm_simp_tac HOLCF_ss  1)
+	]);
+
+(* -------- results about p for case  (! 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_def2 RS ssubst) 1),
+	(rtac fix_ind 1),
+	(rtac adm_all 1),
+	(rtac allI 1),
+	(rtac adm_eq 1),
+	(contX_tacR 1),
+	(rtac allI 1),
+	(rtac (strict_fapp1 RS ssubst) 1),
+	(rtac refl 1),
+	(simp_tac iterate_ss 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)
+	]);
+
+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) ------- *)
+
+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_def2 RS ssubst) 1),
+	(rtac fix_ind 1),
+	(rtac adm_all 1),
+	(rtac allI 1),
+	(rtac adm_eq 1),
+	(contX_tacR 1),
+	(rtac allI 1),
+	(rtac (strict_fapp1 RS ssubst) 1),
+	(rtac refl 1),
+	(rtac allI 1),
+	(simp_tac iterate_ss 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)
+	]);
+
+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)
+	]);
+
+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_tr RS flat_codom) 1),
+	(res_inst_tac [("t","x1")] (iterate_0 RS subst) 1),
+	(etac spec 1)
+	]);
+
+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_def2 RS ssubst) 1),
+	(rtac fix_ind 1),
+	(rtac adm_all 1),
+	(rtac allI 1),
+	(rtac adm_eq 1),
+	(contX_tacR 1),
+	(rtac allI 1),
+	(rtac (strict_fapp1 RS ssubst) 1),
+	(rtac refl 1),
+	(rtac allI 1),
+	(simp_tac iterate_ss 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)
+	]);
+
+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)
+	]);
+
+val hoare_lemma22 = prove_goal Hoare.thy 
+"b1[UU::'a]=UU ==> q[UU::'a] = UU"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(rtac (q_def3 RS ssubst) 1),
+	(asm_simp_tac HOLCF_ss  1)
+	]);
+
+(* -------- results about q for case (? k.~ b1[iterate(k,g,x)]=TT) ------- *)
+
+val hoare_lemma25 = (hoare_lemma8 RS (hoare_lemma24 RS mp) );
+(* 
+[| ? k. ~ ?b1.1[iterate(k,?g1,?x1)] = TT;
+   Suc(?k3) = theleast(%n. ~ ?b1.1[iterate(n,?g1,?x1)] = TT) |] ==>
+q[iterate(?k3,?g1,?x1)] = q[?x1]
+*)
+
+val hoare_lemma26 = prove_goal Hoare.thy 
+"(? n.~ b1[iterate(n,g,x)]=TT) ==>\
+\ k=theleast(%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),
+	(res_inst_tac [("n","k")] natE 1),
+	(hyp_subst_tac 1),
+	(strip_tac 1),
+	(simp_tac iterate_ss 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(xa,g,x)]")] ssubst 1),
+	(rtac (hoare_lemma8 RS spec RS mp) 1),
+	(atac 1),
+	(atac 1),
+	(simp_tac nat_ss 1),
+	(simp_tac (HOLCF_ss addsimps [iterate_Suc]) 1)
+	]);
+
+
+val hoare_lemma27 = prove_goal Hoare.thy 
+"(? n.~ b1[iterate(n,g,x)]=TT) ==>\
+\ k=theleast(%n.~ b1[iterate(n,g,x)]=TT) & b1[iterate(k,g,x)]=UU \
+\ --> q[x] = UU"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(res_inst_tac [("n","k")] natE 1),
+	(hyp_subst_tac 1),
+	(simp_tac iterate_ss 1),
+	(strip_tac 1),
+	(etac conjE 1),
+	(rtac (q_def3 RS ssubst) 1),
+	(asm_simp_tac HOLCF_ss  1),
+	(hyp_subst_tac 1),
+	(simp_tac iterate_ss 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(xa,g,x)]")] ssubst 1),
+	(rtac (hoare_lemma8 RS spec RS mp) 1),
+	(atac 1),
+	(atac 1),
+	(simp_tac nat_ss 1),
+	(asm_simp_tac HOLCF_ss 1),
+	(rtac trans 1),
+	(rtac q_def3 1),
+	(asm_simp_tac HOLCF_ss  1)
+	]);
+
+(* ------- (! 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),
+	(rtac (hoare_lemma16 RS ssubst) 1),
+	(atac 1),
+	(rtac (hoare_lemma19 RS disjE) 1),
+	(atac 1),
+	(rtac (hoare_lemma18 RS ssubst) 1),
+	(atac 1),
+	(rtac (hoare_lemma22 RS ssubst) 1),
+	(atac 1),
+	(rtac refl 1),
+	(rtac (hoare_lemma21 RS ssubst) 1),
+	(atac 1),
+	(rtac (hoare_lemma21 RS ssubst) 1),
+	(atac 1),
+	(rtac refl 1)
+	]);
+
+(* ------------  ? 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),
+	(rtac (hoare_lemma11 RS mp RS ssubst) 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),
+	(rtac (hoare_lemma12 RS mp RS ssubst) 1),
+	(atac 1),
+	(rtac conjI 1),
+	(rtac refl 1),
+	(atac 1),
+	(rtac (hoare_lemma22 RS ssubst) 1),
+	(rtac (hoare_lemma28 RS ssubst) 1),
+	(atac 1),
+	(rtac refl 1),
+	(rtac sym 1),
+	(rtac (hoare_lemma27 RS mp RS ssubst) 1),
+	(atac 1),
+	(rtac conjI 1),
+	(rtac refl 1),
+	(atac 1),
+	(rtac refl 1)
+	]);
+
+(* ------ the main prove q o p = q ------ *)
+
+val hoare_main = prove_goal Hoare.thy "q oo p = q"
+ (fn prems =>
+	[
+	(rtac ext_cfun 1),
+	(rtac (cfcomp2 RS ssubst) 1),
+	(rtac (hoare_lemma3 RS disjE) 1),
+	(etac hoare_lemma23 1),
+	(etac hoare_lemma29 1)
+	]);
+
+
diff -r c22b85994e17 -r 929fc2c63bd0 src/HOLCF/ex/hoare.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/hoare.thy	Wed Jan 19 17:40:26 1994 +0100
@@ -0,0 +1,43 @@
+(*  Title:	HOLCF/ex/hoare.thy
+    ID:         $Id$
+    Author: 	Franz Regensburger
+    Copyright	1993 Technische Universitaet Muenchen
+
+Theory for an example by C.A.R. Hoare 
+
+p x = if b1(x) 
+         then p(g(x))
+         else x fi
+
+q x = if b1(x) orelse b2(x) 
+         then q (g(x))
+         else x fi
+
+Prove: for all b1 b2 g . 
+            q o p  = q 
+
+In order to get a nice notation we fix the functions b1,b2 and g in the
+signature of this example
+
+*)
+
+Hoare = Tr2 +
+
+consts
+	b1:: "'a -> tr"
+	b2:: "'a -> tr"
+	 g:: "'a -> 'a"
+	p :: "'a -> 'a"
+	q :: "'a -> 'a"
+
+rules
+
+  p_def  "p == fix[LAM f. LAM x.\
+\                 If b1[x] then f[g[x]] else x fi]"
+
+  q_def  "q == fix[LAM f. LAM x.\
+\                 If b1[x] orelse b2[x] then f[g[x]] else x fi]"
+
+
+end
+ 
diff -r c22b85994e17 -r 929fc2c63bd0 src/HOLCF/ex/hoare.txt
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/hoare.txt	Wed Jan 19 17:40:26 1994 +0100
@@ -0,0 +1,97 @@
+Proves about loops and tail-recursive functions
+===============================================
+
+Problem A
+
+P = while B1       do S od
+Q = while B1 or B2 do S od
+
+Prove P;Q = Q    (provided B1, B2 have no side effects)
+
+------
+
+Looking at the denotational semantics of while, we get
+
+Problem B
+
+[|B1|]:State->Bool
+[|B2|]:State->Bool
+[|S |]:State->State
+f     :State->State
+
+p = fix LAM f.LAM x. if [| B1 |] x                  then f([| S |] x) else x fi
+q = fix LAM f.LAM x. if [| B1 |] x orelse [|b2 |] x then f([| S |] x) else x fi
+
+Prove q o p = q          rsp.       ALL x.q(p(x))=q(x)
+
+Remark: 1. Bool is the three-valued domain {UU,FF,TT} since tests B1 and B2 may
+           not terminate.
+        2. orelse is the sequential or like in ML
+
+----------
+
+If we abstract over the structure of stores we get
+
+Problem C
+
+b1:'a -> Bool
+b2:'a -> Bool
+g :'a ->'a
+h :'a ->'a
+
+p = fix LAM h.LAM x. if b1(x)              then h(g(x)) else x fi
+q = fix LAM h.LAM x. if b1(x) orelse b2(x) then h(g(x)) else x fi
+
+where g is an abstraction of [| S |]
+
+Prove q o p = q 
+
+Remark: there are no restrictions wrt. definedness or strictness for any of 
+        the involved functions.
+
+----------
+
+In a functional programming language the problem reads as follows:
+
+p(x) = if b1(x) 
+         then p(g(x))
+         else x fi
+
+q(x) = if b1(x) orelse b2(x) 
+         then q(g(x))
+         else x fi
+
+
+Prove:  q o p = q
+
+
+-------------
+
+In you like to test the problem in ML (bad guy) you have to introduce 
+formal parameters for b1,b2 and g.
+
+fun p b1 g x = if b1(x) 
+         then p b1 g (g(x))
+         else x;
+
+
+fun q b1 b2 g x = if b1(x) orelse b2(x) 
+         then q b1 b2 g (g(x))
+         else x;
+
+Prove: for all b1 b2 g . 
+            (q b1 b2 g) o (p b1 g) = (q b1 b2 g)
+
+===========
+
+It took 4 person-days to formulate and prove the problem C in the
+Isabelle logic HOLCF. The formalisation was done by conservative extension and
+all proof principles where derived from pure HOLCF.
+
+
+    
+
+
+
+
+
diff -r c22b85994e17 -r 929fc2c63bd0 src/HOLCF/ex/loop.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/loop.ML	Wed Jan 19 17:40:26 1994 +0100
@@ -0,0 +1,282 @@
+(*  Title:	HOLCF/ex/loop.ML
+    ID:         $Id$
+    Author: 	Franz Regensburger
+    Copyright	1993 Technische Universitaet Muenchen
+
+Lemmas for theory loop.thy
+*)
+
+open Loop;
+
+(* --------------------------------------------------------------------------- *)
+(* access to definitions                                                       *)
+(* --------------------------------------------------------------------------- *)
+
+val step_def2 = prove_goalw Loop.thy [step_def]
+"step[b][g][x] = If b[x] then g[x] else x fi"
+ (fn prems =>
+	[
+	(simp_tac Cfun_ss 1)
+	]);
+
+val while_def2 = prove_goalw Loop.thy [while_def]
+"while[b][g] = fix[LAM f x. If b[x] then f[g[x]] else x fi]"
+ (fn prems =>
+	[
+	(simp_tac Cfun_ss 1)
+	]);
+
+
+(* ------------------------------------------------------------------------- *)
+(* rekursive properties of while                                             *)
+(* ------------------------------------------------------------------------- *)
+
+val while_unfold = prove_goal Loop.thy 
+"while[b][g][x] = If b[x] then while[b][g][g[x]] else x fi"
+ (fn prems =>
+	[
+	(fix_tac5  while_def2 1),
+	(simp_tac Cfun_ss 1)
+	]);
+
+val while_unfold2 = prove_goal Loop.thy 
+	"!x.while[b][g][x] = while[b][g][iterate(k,step[b][g],x)]"
+ (fn prems =>
+	[
+	(nat_ind_tac "k" 1),
+	(simp_tac (HOLCF_ss addsimps [iterate_0,iterate_Suc]) 1),
+	(rtac allI 1),
+	(rtac trans 1),
+	(rtac (while_unfold RS ssubst) 1),
+	(rtac refl 2),
+	(rtac (iterate_Suc2 RS ssubst) 1),
+	(rtac trans 1),
+	(etac spec 2),
+	(rtac (step_def2 RS ssubst) 1),
+	(res_inst_tac [("p","b[x]")] trE 1),
+	(asm_simp_tac HOLCF_ss 1),
+	(rtac (while_unfold RS ssubst) 1),
+	(res_inst_tac [("s","UU"),("t","b[UU]")] ssubst 1),
+	(etac (flat_tr RS flat_codom RS disjE) 1),
+	(atac 1),
+	(etac spec 1),
+	(simp_tac HOLCF_ss 1),
+	(asm_simp_tac HOLCF_ss 1),
+	(asm_simp_tac HOLCF_ss 1),
+	(rtac (while_unfold RS ssubst) 1),
+	(asm_simp_tac HOLCF_ss 1)
+	]);
+
+val while_unfold3 = prove_goal Loop.thy 
+	"while[b][g][x] = while[b][g][step[b][g][x]]"
+ (fn prems =>
+	[
+	(res_inst_tac [("s","while[b][g][iterate(Suc(0),step[b][g],x)]")] trans 1),
+	(rtac (while_unfold2 RS spec) 1),
+	(simp_tac iterate_ss 1)
+	]);
+
+
+(* --------------------------------------------------------------------------- *)
+(* properties of while and iterations                                          *)
+(* --------------------------------------------------------------------------- *)
+
+val loop_lemma1 = prove_goal Loop.thy
+"[|? y.b[y]=FF; iterate(k,step[b][g],x)=UU|]==>iterate(Suc(k),step[b][g],x)=UU"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(simp_tac iterate_ss 1),
+	(rtac trans 1),
+	(rtac step_def2 1),
+	(asm_simp_tac HOLCF_ss 1),
+	(etac exE 1),
+	(etac (flat_tr RS flat_codom RS disjE) 1),
+	(asm_simp_tac HOLCF_ss 1),
+	(asm_simp_tac HOLCF_ss 1)
+	]);
+
+val loop_lemma2 = prove_goal Loop.thy
+"[|? y.b[y]=FF;~iterate(Suc(k),step[b][g],x)=UU |]==>\
+\~iterate(k,step[b][g],x)=UU"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(rtac contrapos 1),
+	(etac  loop_lemma1 2),
+	(atac 1),
+	(atac 1)
+	]);
+
+val loop_lemma3 = prove_goal Loop.thy
+"[|!x. INV(x) & b[x]=TT & ~g[x]=UU --> INV(g[x]);\
+\? y.b[y]=FF; INV(x)|] ==>\
+\~iterate(k,step[b][g],x)=UU --> INV(iterate(k,step[b][g],x))"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(nat_ind_tac "k" 1),
+	(asm_simp_tac iterate_ss 1),
+	(strip_tac 1),
+	(simp_tac (iterate_ss addsimps [step_def2]) 1),
+	(res_inst_tac [("p","b[iterate(k1, step[b][g], x)]")] trE 1),
+	(etac notE 1),
+	(asm_simp_tac (HOLCF_ss addsimps [step_def2,iterate_Suc] ) 1),
+	(asm_simp_tac HOLCF_ss  1),
+	(rtac mp 1),
+	(etac spec  1),
+	(asm_simp_tac (HOLCF_ss addsimps [loop_lemma2] ) 1),
+	(res_inst_tac [("s","iterate(Suc(k1), step[b][g], x)"),
+		("t","g[iterate(k1, step[b][g], x)]")] ssubst 1),
+	(atac 2),
+	(asm_simp_tac (HOLCF_ss addsimps [iterate_Suc,step_def2] ) 1),
+	(asm_simp_tac (HOLCF_ss addsimps [loop_lemma2] ) 1)
+	]);
+
+
+val loop_lemma4 = prove_goal Loop.thy
+"!x. b[iterate(k,step[b][g],x)]=FF --> while[b][g][x]=iterate(k,step[b][g],x)"
+ (fn prems =>
+	[
+	(nat_ind_tac "k" 1),
+	(simp_tac iterate_ss 1),
+	(strip_tac 1),
+	(rtac (while_unfold RS ssubst) 1),
+	(asm_simp_tac HOLCF_ss  1),
+	(rtac allI 1),
+	(rtac (iterate_Suc2 RS ssubst) 1),
+	(strip_tac 1),
+	(rtac trans 1),
+	(rtac while_unfold3 1),
+	(asm_simp_tac HOLCF_ss  1)
+	]);
+
+val loop_lemma5 = prove_goal Loop.thy
+"!k. ~b[iterate(k,step[b][g],x)]=FF ==>\
+\ !m. while[b][g][iterate(m,step[b][g],x)]=UU"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(rtac (while_def2 RS ssubst) 1),
+	(rtac fix_ind 1),
+	(rtac (allI RS adm_all) 1),
+	(rtac adm_eq 1),
+	(contX_tacR 1),
+	(simp_tac HOLCF_ss  1),
+	(rtac allI 1),
+	(simp_tac HOLCF_ss  1),
+	(res_inst_tac [("p","b[iterate(m, step[b][g],x)]")] trE 1),
+	(asm_simp_tac HOLCF_ss  1),
+	(asm_simp_tac HOLCF_ss  1),
+	(res_inst_tac [("s","xa[iterate(Suc(m), step[b][g], x)]")] trans 1),
+	(etac spec 2),
+	(rtac cfun_arg_cong 1),
+	(rtac trans 1),
+	(rtac (iterate_Suc RS sym) 2),
+	(asm_simp_tac (HOLCF_ss addsimps [step_def2]) 1),
+	(dtac spec 1),
+	(contr_tac 1)
+	]);
+
+
+val loop_lemma6 = prove_goal Loop.thy
+"!k. ~b[iterate(k,step[b][g],x)]=FF ==> while[b][g][x]=UU"
+ (fn prems =>
+	[
+	(res_inst_tac [("t","x")] (iterate_0 RS subst) 1),
+	(rtac (loop_lemma5 RS spec) 1),
+	(resolve_tac prems 1)
+	]);
+
+val loop_lemma7 = prove_goal Loop.thy
+"~while[b][g][x]=UU ==> ? k. b[iterate(k,step[b][g],x)]=FF"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(etac swap 1),
+	(rtac loop_lemma6 1),
+	(fast_tac HOL_cs 1)
+	]);
+
+val loop_lemma8 = prove_goal Loop.thy
+"~while[b][g][x]=UU ==> ? y. b[y]=FF"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(dtac loop_lemma7 1),
+	(fast_tac HOL_cs 1)
+	]);
+
+
+(* --------------------------------------------------------------------------- *)
+(* an invariant rule for loops                                                 *)
+(* --------------------------------------------------------------------------- *)
+
+val loop_inv2 = prove_goal Loop.thy
+"[| (!y. INV(y) & b[y]=TT & ~g[y]=UU --> INV(g[y]));\
+\   (!y. INV(y) & b[y]=FF --> Q(y));\
+\   INV(x); ~while[b][g][x]=UU |] ==> Q(while[b][g][x])"
+ (fn prems =>
+	[
+	(res_inst_tac [("P","%k.b[iterate(k,step[b][g],x)]=FF")] exE 1),
+	(rtac loop_lemma7 1),
+	(resolve_tac prems 1),
+	(rtac ((loop_lemma4 RS spec RS mp) RS ssubst) 1),
+	(atac 1),
+	(rtac (nth_elem (1,prems) RS spec RS mp) 1),
+	(rtac conjI 1),
+	(atac 2),
+	(rtac (loop_lemma3 RS mp) 1),
+	(resolve_tac prems 1),
+	(rtac loop_lemma8 1),
+	(resolve_tac prems 1),
+	(resolve_tac prems 1),
+	(rtac classical3 1),
+	(resolve_tac prems 1),
+	(etac box_equals 1),
+	(rtac (loop_lemma4 RS spec RS mp RS sym) 1),
+	(atac 1),
+	(rtac refl 1)
+	]);
+
+val loop_inv3 = prove_goal Loop.thy
+"[| !!y.[| INV(y); b[y]=TT; ~g[y]=UU|] ==> INV(g[y]);\
+\   !!y.[| INV(y); b[y]=FF|]==> Q(y);\
+\   INV(x); ~while[b][g][x]=UU |] ==> Q(while[b][g][x])"
+ (fn prems =>
+	[
+	(rtac loop_inv2 1),
+	(rtac allI 1),
+	(rtac impI 1),
+	(resolve_tac prems 1),
+	(fast_tac HOL_cs 1),
+	(fast_tac HOL_cs 1),
+	(fast_tac HOL_cs 1),
+	(rtac allI 1),
+	(rtac impI 1),
+	(resolve_tac prems 1),
+	(fast_tac HOL_cs 1),
+	(fast_tac HOL_cs 1),
+	(resolve_tac prems 1),
+	(resolve_tac prems 1)
+	]);
+
+val loop_inv = prove_goal Loop.thy
+"[| 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])"
+ (fn prems =>
+	[
+	(rtac loop_inv3 1),
+	(eresolve_tac prems 1),
+	(atac 1),
+	(atac 1),
+	(resolve_tac prems 1),
+	(atac 1),
+	(atac 1),
+	(resolve_tac prems 1),
+	(resolve_tac prems 1),
+	(resolve_tac prems 1)
+	]);
diff -r c22b85994e17 -r 929fc2c63bd0 src/HOLCF/ex/loop.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/loop.thy	Wed Jan 19 17:40:26 1994 +0100
@@ -0,0 +1,24 @@
+(*  Title:	HOLCF/ex/loop.thy
+    ID:         $Id$
+    Author: 	Franz Regensburger
+    Copyright	1993 Technische Universitaet Muenchen
+
+Theory for a loop primitive like while
+*)
+
+Loop = Tr2 +
+
+consts
+
+	step  :: "('a -> tr)->('a -> 'a)->'a->'a"
+	while :: "('a -> tr)->('a -> 'a)->'a->'a"
+
+rules
+
+  step_def	"step == (LAM b g x. If b[x] then g[x] else x fi)"
+  while_def	"while == (LAM b g. fix[LAM f x.\
+\                 If b[x] then f[g[x]] else x fi])"
+
+
+end
+