--- /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)
+ ]);
+
--- /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]]]
+
+
+*)
+
+
--- /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)
+ ]);
+
+
--- /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
+
--- /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)
+ ]);
--- /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
+
--- /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";
--- /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)
+ ]);
+
--- /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]]]
+
+
+*)
+
+
--- /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)
+ ]);
+
+
--- /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
+
--- /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.
+
+
+
+
+
+
+
+
--- /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)
+ ]);
--- /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
+