--- a/src/HOLCF/Cfun2.ML Thu Mar 24 13:25:12 1994 +0100
+++ b/src/HOLCF/Cfun2.ML Thu Mar 24 13:36:34 1994 +0100
@@ -216,7 +216,7 @@
is_chain(?CCF1) ==> lub(range(?CCF1)) = fabs(%x. lub(range(%i. ?CCF1(i)[x])))
*)
-val cpo_fun = prove_goal Cfun2.thy
+val cpo_cfun = prove_goal Cfun2.thy
"is_chain(CCF::nat=>('a::pcpo->'b::pcpo)) ==> ? x. range(CCF) <<| x"
(fn prems =>
[
--- a/src/HOLCF/Dnat.ML Thu Mar 24 13:25:12 1994 +0100
+++ b/src/HOLCF/Dnat.ML Thu Mar 24 13:36:34 1994 +0100
@@ -171,41 +171,49 @@
(* Distinctness wrt. << and = *)
(* ------------------------------------------------------------------------*)
-fun prover contrfun thm = prove_goal Dnat.thy thm
+val temp = prove_goal Dnat.thy "~dzero << dsucc[n]"
+ (fn prems =>
+ [
+ (res_inst_tac [("P1","TT << FF")] classical3 1),
+ (resolve_tac dist_less_tr 1),
+ (dres_inst_tac [("fo5","is_dzero")] monofun_cfun_arg 1),
+ (etac box_less 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (res_inst_tac [("Q","n=UU")] classical2 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
+ ]);
+
+val dnat_dist_less = [temp];
+
+val temp = prove_goal Dnat.thy "n~=UU ==> ~dsucc[n] << dzero"
(fn prems =>
[
(cut_facts_tac prems 1),
(res_inst_tac [("P1","TT << FF")] classical3 1),
(resolve_tac dist_less_tr 1),
- (dres_inst_tac [("fo5",contrfun)] monofun_cfun_arg 1),
+ (dres_inst_tac [("fo5","is_dsucc")] monofun_cfun_arg 1),
(etac box_less 1),
(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
]);
-val dnat_dist_less =
- [
-prover "is_dzero" "n~=UU ==> ~dzero << dsucc[n]",
-prover "is_dsucc" "n~=UU ==> ~dsucc[n] << dzero"
- ];
+val dnat_dist_less = temp::dnat_dist_less;
-fun prover contrfun thm = prove_goal Dnat.thy thm
+val temp = prove_goal Dnat.thy "dzero ~= dsucc[n]"
(fn prems =>
[
- (cut_facts_tac prems 1),
+ (res_inst_tac [("Q","n=UU")] classical2 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
(res_inst_tac [("P1","TT = FF")] classical3 1),
(resolve_tac dist_eq_tr 1),
- (dres_inst_tac [("f",contrfun)] cfun_arg_cong 1),
+ (dres_inst_tac [("f","is_dzero")] cfun_arg_cong 1),
(etac box_equals 1),
(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
]);
-val dnat_dist_eq =
- [
-prover "is_dzero" "n~=UU ==> dzero ~= dsucc[n]",
-prover "is_dsucc" "n~=UU ==> dsucc[n] ~= dzero"
- ];
+val dnat_dist_eq = [temp, temp RS not_sym];
val dnat_rews = dnat_dist_less @ dnat_dist_eq @ dnat_rews;
@@ -271,39 +279,57 @@
(* ------------------------------------------------------------------------*)
(* Properties dnat_take *)
(* ------------------------------------------------------------------------*)
-
-val dnat_take =
- [
-prove_goalw Dnat.thy [dnat_take_def] "dnat_take(n)[UU]=UU"
+val temp = prove_goalw Dnat.thy [dnat_take_def] "dnat_take(n)[UU]=UU"
(fn prems =>
[
(res_inst_tac [("n","n")] natE 1),
(asm_simp_tac iterate_ss 1),
(asm_simp_tac iterate_ss 1),
(simp_tac (HOLCF_ss addsimps dnat_rews) 1)
- ]),
-prove_goalw Dnat.thy [dnat_take_def] "dnat_take(0)[xs]=UU"
+ ]);
+
+val dnat_take = [temp];
+
+val temp = prove_goalw Dnat.thy [dnat_take_def] "dnat_take(0)[xs]=UU"
(fn prems =>
[
(asm_simp_tac iterate_ss 1)
- ])];
+ ]);
-fun prover thm = prove_goalw Dnat.thy [dnat_take_def] thm
+val dnat_take = temp::dnat_take;
+
+val temp = prove_goalw Dnat.thy [dnat_take_def]
+ "dnat_take(Suc(n))[dzero]=dzero"
(fn prems =>
[
- (cut_facts_tac prems 1),
- (simp_tac iterate_ss 1),
+ (asm_simp_tac iterate_ss 1),
+ (simp_tac (HOLCF_ss addsimps dnat_rews) 1)
+ ]);
+
+val dnat_take = temp::dnat_take;
+
+val temp = prove_goalw Dnat.thy [dnat_take_def]
+ "dnat_take(Suc(n))[dsucc[xs]]=dsucc[dnat_take(n)[xs]]"
+ (fn prems =>
+ [
+ (res_inst_tac [("Q","xs=UU")] classical2 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (asm_simp_tac iterate_ss 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (res_inst_tac [("n","n")] natE 1),
+ (asm_simp_tac iterate_ss 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (asm_simp_tac iterate_ss 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (asm_simp_tac iterate_ss 1),
(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
]);
-val dnat_take = [
-prover "dnat_take(Suc(n))[dzero]=dzero",
-prover "xs~=UU ==> dnat_take(Suc(n))[dsucc[xs]]=dsucc[dnat_take(n)[xs]]"
- ] @ dnat_take;
-
+val dnat_take = temp::dnat_take;
val dnat_rews = dnat_take @ dnat_rews;
+
(* ------------------------------------------------------------------------*)
(* take lemma for dnats *)
(* ------------------------------------------------------------------------*)
@@ -368,6 +394,7 @@
(* structural induction for admissible predicates *)
(* ------------------------------------------------------------------------*)
+(* not needed any longer
val dnat_ind = prove_goal Dnat.thy
"[| adm(P);\
\ P(UU);\
@@ -397,6 +424,79 @@
(eresolve_tac prems 1),
(etac spec 1)
]);
+*)
+
+val dnat_finite_ind = prove_goal Dnat.thy
+"[|P(UU);P(dzero);\
+\ !! s1.[|s1~=UU;P(s1)|] ==> P(dsucc[s1])\
+\ |] ==> !s.P(dnat_take(n)[s])"
+ (fn prems =>
+ [
+ (nat_ind_tac "n" 1),
+ (simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (resolve_tac prems 1),
+ (rtac allI 1),
+ (res_inst_tac [("n","s")] dnatE 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (resolve_tac prems 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (resolve_tac prems 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (res_inst_tac [("Q","dnat_take(n1)[x]=UU")] classical2 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (resolve_tac prems 1),
+ (resolve_tac prems 1),
+ (atac 1),
+ (etac spec 1)
+ ]);
+
+val dnat_all_finite_lemma1 = prove_goal Dnat.thy
+"!s.dnat_take(n)[s]=UU |dnat_take(n)[s]=s"
+ (fn prems =>
+ [
+ (nat_ind_tac "n" 1),
+ (simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (rtac allI 1),
+ (res_inst_tac [("n","s")] dnatE 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (eres_inst_tac [("x","x")] allE 1),
+ (etac disjE 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
+ ]);
+
+val dnat_all_finite_lemma2 = prove_goal Dnat.thy "? n.dnat_take(n)[s]=s"
+ (fn prems =>
+ [
+ (res_inst_tac [("Q","s=UU")] classical2 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (subgoal_tac "(!n.dnat_take(n)[s]=UU) |(? n.dnat_take(n)[s]=s)" 1),
+ (etac disjE 1),
+ (eres_inst_tac [("P","s=UU")] notE 1),
+ (rtac dnat_take_lemma 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (atac 1),
+ (subgoal_tac "!n.!s.dnat_take(n)[s]=UU |dnat_take(n)[s]=s" 1),
+ (fast_tac HOL_cs 1),
+ (rtac allI 1),
+ (rtac dnat_all_finite_lemma1 1)
+ ]);
+
+
+val dnat_ind = prove_goal Dnat.thy
+"[|P(UU);P(dzero);\
+\ !! s1.[|s1~=UU;P(s1)|] ==> P(dsucc[s1])\
+\ |] ==> P(s)"
+ (fn prems =>
+ [
+ (rtac (dnat_all_finite_lemma2 RS exE) 1),
+ (etac subst 1),
+ (rtac (dnat_finite_ind RS spec) 1),
+ (REPEAT (resolve_tac prems 1)),
+ (REPEAT (atac 1))
+ ]);
val dnat_flat = prove_goalw Dnat.thy [flat_def] "flat(dzero)"
@@ -404,12 +504,6 @@
[
(rtac allI 1),
(res_inst_tac [("s","x")] dnat_ind 1),
- (REPEAT (resolve_tac adm_thms 1)),
- (contX_tacR 1),
- (REPEAT (resolve_tac adm_thms 1)),
- (contX_tacR 1),
- (REPEAT (resolve_tac adm_thms 1)),
- (contX_tacR 1),
(fast_tac HOL_cs 1),
(rtac allI 1),
(res_inst_tac [("n","y")] dnatE 1),
@@ -419,53 +513,20 @@
(rtac allI 1),
(res_inst_tac [("n","y")] dnatE 1),
(fast_tac (HOL_cs addSIs [UU_I]) 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_dist_less) 1),
(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
- (hyp_subst_tac 1),
(strip_tac 1),
- (rtac disjI2 1),
- (forward_tac dnat_invert 1),
- (atac 2),
- (atac 1),
+ (subgoal_tac "s1<<xa" 1),
(etac allE 1),
(dtac mp 1),
(atac 1),
(etac disjE 1),
(contr_tac 1),
- (asm_simp_tac HOLCF_ss 1)
+ (asm_simp_tac HOLCF_ss 1),
+ (resolve_tac dnat_invert 1),
+ (REPEAT (atac 1))
]);
-val dnat_ind = prove_goal Dnat.thy
-"[| adm(P);\
-\ P(UU);\
-\ P(dzero);\
-\ !! s1.[|s1~=UU ; P(s1)|] ==> P(dsucc[s1])|] ==> P(s)"
- (fn prems =>
- [
- (rtac (dnat_reach RS subst) 1),
- (res_inst_tac [("x","s")] spec 1),
- (rtac fix_ind 1),
- (rtac adm_all2 1),
- (rtac adm_subst 1),
- (contX_tacR 1),
- (resolve_tac prems 1),
- (simp_tac HOLCF_ss 1),
- (resolve_tac prems 1),
- (strip_tac 1),
- (res_inst_tac [("n","xa")] dnatE 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_copy) 1),
- (resolve_tac prems 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_copy) 1),
- (resolve_tac prems 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_copy) 1),
- (res_inst_tac [("Q","x[xb]=UU")] classical2 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
- (resolve_tac prems 1),
- (eresolve_tac prems 1),
- (etac spec 1)
- ]);
+
-val dnat_ind2 = dnat_flat RS adm_flat RS dnat_ind;
-(* "[| ?P(UU); ?P(dzero);
- !!s1. [| s1 ~= UU; ?P(s1) |] ==> ?P(dsucc[s1]) |] ==> ?P(?s)" : thm
-*)
--- a/src/HOLCF/Fix.ML Thu Mar 24 13:25:12 1994 +0100
+++ b/src/HOLCF/Fix.ML Thu Mar 24 13:36:34 1994 +0100
@@ -387,6 +387,19 @@
(rtac refl 1)
]);
+(* ------------------------------------------------------------------------
+
+given the definition
+
+smap_def
+ "smap = fix[LAM h f s. stream_when[LAM x l.scons[f[x]][h[f][l]]][s]]"
+
+use fix_prover for
+
+val smap_def2 = fix_prover Stream2.thy smap_def
+ "smap = (LAM f s. stream_when[LAM x l.scons[f[x]][smap[f][l]]][s])";
+
+ ------------------------------------------------------------------------ *)
(* ------------------------------------------------------------------------ *)
(* better access to definitions *)
@@ -881,7 +894,7 @@
(rtac iffI 1),
(etac FalseE 2),
(rtac notE 1),
- (etac less_not_sym 1),
+ (etac (less_not_sym RS mp) 1),
(atac 1),
(asm_simp_tac Cfun_ss 1),
(etac (is_chainE RS spec) 1),
@@ -921,7 +934,7 @@
(rtac iffI 1),
(etac FalseE 2),
(rtac notE 1),
- (etac less_not_sym 1),
+ (etac (less_not_sym RS mp) 1),
(atac 1),
(asm_simp_tac nat_ss 1),
(dtac spec 1),
--- a/src/HOLCF/Porder.ML Thu Mar 24 13:25:12 1994 +0100
+++ b/src/HOLCF/Porder.ML Thu Mar 24 13:36:34 1994 +0100
@@ -6,9 +6,9 @@
Lemmas for theory porder.thy
*)
+open Porder0;
open Porder;
-
val box_less = prove_goal Porder.thy
"[| a << b; c << a; b << d|] ==> c << d"
(fn prems =>
--- a/src/HOLCF/Porder.thy Thu Mar 24 13:25:12 1994 +0100
+++ b/src/HOLCF/Porder.thy Thu Mar 24 13:36:34 1994 +0100
@@ -3,25 +3,13 @@
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
-Definition of class porder (partial order)
-
-The prototype theory for this class is void.thy
+Conservative extension of theory Porder0 by constant definitions
*)
-Porder = Void +
-
-(* Introduction of new class. The witness is type void. *)
-
-classes po < term
+Porder = Porder0 +
-(* default type is still term ! *)
-(* void is the prototype in po *)
-
-arities void :: po
-
-consts "<<" :: "['a,'a::po] => bool" (infixl 55)
-
+consts
"<|" :: "['a set,'a::po] => bool" (infixl 55)
"<<|" :: "['a set,'a::po] => bool" (infixl 55)
lub :: "'a set => 'a::po"
@@ -32,21 +20,6 @@
rules
-(* class axioms: justification is theory Void *)
-
-refl_less "x << x"
- (* witness refl_less_void *)
-
-antisym_less "[|x<<y ; y<<x |] ==> x = y"
- (* witness antisym_less_void *)
-
-trans_less "[|x<<y ; y<<z |] ==> x<<z"
- (* witness trans_less_void *)
-
-(* instance of << for the prototype void *)
-
-inst_void_po "(op <<)::[void,void]=>bool = less_void"
-
(* class definitions *)
is_ub "S <| x == ! y.y:S --> y<<x"
@@ -57,11 +30,9 @@
(* Arbitrary chains are total orders *)
is_tord "is_tord(S) == ! x y. x:S & y:S --> (x<<y | y<<x)"
-
(* Here we use countable chains and I prefer to code them as functions! *)
is_chain "is_chain(F) == (! i.F(i) << F(Suc(i)))"
-
(* finite chains, needed for monotony of continouous functions *)
max_in_chain_def "max_in_chain(i,C) == ! j. i <= j --> C(i) = C(j)"
--- a/src/HOLCF/ROOT.ML Thu Mar 24 13:25:12 1994 +0100
+++ b/src/HOLCF/ROOT.ML Thu Mar 24 13:36:34 1994 +0100
@@ -17,7 +17,10 @@
use_thy "Holcfb";
use_thy "Void";
+
+use_thy "Porder0";
use_thy "Porder";
+
use_thy "Pcpo";
use_thy "Fun1";
@@ -61,6 +64,8 @@
use_thy "Dnat2";
use_thy "Stream";
use_thy "Stream2";
+use_thy "Dlist";
+
use "../Pure/install_pp.ML";
print_depth 8;
--- a/src/HOLCF/Stream.ML Thu Mar 24 13:25:12 1994 +0100
+++ b/src/HOLCF/Stream.ML Thu Mar 24 13:36:34 1994 +0100
@@ -229,6 +229,7 @@
val stream_rews = stream_discsel_def @ stream_rews;
+
(* ------------------------------------------------------------------------*)
(* Properties stream_take *)
(* ------------------------------------------------------------------------*)
@@ -265,6 +266,46 @@
val stream_rews = stream_take @ stream_rews;
(* ------------------------------------------------------------------------*)
+(* enhance the simplifier *)
+(* ------------------------------------------------------------------------*)
+
+val stream_copy2 = prove_goal Stream.thy
+ "stream_copy[f][scons[x][xs]]= scons[x][f[xs]]"
+ (fn prems =>
+ [
+ (res_inst_tac [("Q","x=UU")] classical2 1),
+ (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
+ ]);
+
+val shd2 = prove_goal Stream.thy "shd[scons[x][xs]]=x"
+ (fn prems =>
+ [
+ (res_inst_tac [("Q","x=UU")] classical2 1),
+ (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
+ ]);
+
+val stream_take2 = prove_goal Stream.thy
+ "stream_take(Suc(n))[scons[x][xs]]=scons[x][stream_take(n)[xs]]"
+ (fn prems =>
+ [
+ (res_inst_tac [("Q","x=UU")] classical2 1),
+ (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
+ ]);
+
+val stream_rews = [stream_iso_strict RS conjunct1,
+ stream_iso_strict RS conjunct2,
+ hd stream_copy, stream_copy2]
+ @ stream_when
+ @ [hd stream_discsel,shd2] @ (tl (tl stream_discsel))
+ @ stream_constrdef
+ @ stream_discsel_def
+ @ [ stream_take2] @ (tl stream_take);
+
+
+(* ------------------------------------------------------------------------*)
(* take lemma for streams *)
(* ------------------------------------------------------------------------*)
@@ -326,8 +367,49 @@
(* structural induction for admissible predicates *)
(* ------------------------------------------------------------------------*)
+val stream_finite_ind = prove_goal Stream.thy
+"[|P(UU);\
+\ !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
+\ |] ==> !s.P(stream_take(n)[s])"
+ (fn prems =>
+ [
+ (nat_ind_tac "n" 1),
+ (simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (resolve_tac prems 1),
+ (rtac allI 1),
+ (res_inst_tac [("s","s")] streamE 1),
+ (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (resolve_tac prems 1),
+ (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (resolve_tac prems 1),
+ (atac 1),
+ (etac spec 1)
+ ]);
+
+val stream_finite_ind2 = prove_goalw Stream.thy [stream_finite_def]
+"(!!n.P(stream_take(n)[s])) ==> stream_finite(s) -->P(s)"
+ (fn prems =>
+ [
+ (strip_tac 1),
+ (etac exE 1),
+ (etac subst 1),
+ (resolve_tac prems 1)
+ ]);
+
+val stream_finite_ind3 = prove_goal Stream.thy
+"[|P(UU);\
+\ !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
+\ |] ==> stream_finite(s) --> P(s)"
+ (fn prems =>
+ [
+ (rtac stream_finite_ind2 1),
+ (rtac (stream_finite_ind RS spec) 1),
+ (REPEAT (resolve_tac prems 1)),
+ (REPEAT (atac 1))
+ ]);
+
val stream_ind = prove_goal Stream.thy
-"[| adm(P);\
+"[|adm(P);\
\ P(UU);\
\ !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
\ |] ==> P(s)"
@@ -335,21 +417,16 @@
[
(rtac (stream_reach RS subst) 1),
(res_inst_tac [("x","s")] spec 1),
- (rtac fix_ind 1),
- (rtac (allI RS adm_all) 1),
+ (rtac wfix_ind 1),
+ (rtac adm_impl_admw 1),
+ (REPEAT (resolve_tac adm_thms 1)),
(rtac adm_subst 1),
(contX_tacR 1),
(resolve_tac prems 1),
- (simp_tac HOLCF_ss 1),
- (resolve_tac prems 1),
- (strip_tac 1),
- (res_inst_tac [("s","xa")] streamE 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
- (resolve_tac prems 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
- (resolve_tac prems 1),
- (atac 1),
- (etac spec 1)
+ (rtac allI 1),
+ (rtac (rewrite_rule [stream_take_def] stream_finite_ind) 1),
+ (REPEAT (resolve_tac prems 1)),
+ (REPEAT (atac 1))
]);
@@ -403,3 +480,312 @@
]);
+(* ------------------------------------------------------------------------*)
+(* theorems about finite and infinite streams *)
+(* ------------------------------------------------------------------------*)
+
+(* ----------------------------------------------------------------------- *)
+(* 2 lemmas about stream_finite *)
+(* ----------------------------------------------------------------------- *)
+
+val stream_finite_UU = prove_goalw Stream.thy [stream_finite_def]
+ "stream_finite(UU)"
+ (fn prems =>
+ [
+ (rtac exI 1),
+ (simp_tac (HOLCF_ss addsimps stream_rews) 1)
+ ]);
+
+val inf_stream_not_UU = prove_goal Stream.thy "~stream_finite(s) ==> s ~= UU"
+ (fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (etac swap 1),
+ (dtac notnotD 1),
+ (hyp_subst_tac 1),
+ (rtac stream_finite_UU 1)
+ ]);
+
+(* ----------------------------------------------------------------------- *)
+(* a lemma about shd *)
+(* ----------------------------------------------------------------------- *)
+
+val stream_shd_lemma1 = prove_goal Stream.thy "shd[s]=UU --> s=UU"
+ (fn prems =>
+ [
+ (res_inst_tac [("s","s")] streamE 1),
+ (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (hyp_subst_tac 1),
+ (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
+ ]);
+
+
+(* ----------------------------------------------------------------------- *)
+(* lemmas about stream_take *)
+(* ----------------------------------------------------------------------- *)
+
+val stream_take_lemma1 = prove_goal Stream.thy
+ "!x xs.x~=UU --> \
+\ stream_take(Suc(n))[scons[x][xs]] = scons[x][xs] --> stream_take(n)[xs]=xs"
+ (fn prems =>
+ [
+ (rtac allI 1),
+ (rtac allI 1),
+ (rtac impI 1),
+ (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (strip_tac 1),
+ (rtac ((hd stream_inject) RS conjunct2) 1),
+ (atac 1),
+ (atac 1),
+ (atac 1)
+ ]);
+
+
+val stream_take_lemma2 = prove_goal Stream.thy
+ "! s2. stream_take(n)[s2] = s2 --> stream_take(Suc(n))[s2]=s2"
+ (fn prems =>
+ [
+ (nat_ind_tac "n" 1),
+ (simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (strip_tac 1 ),
+ (hyp_subst_tac 1),
+ (simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (rtac allI 1),
+ (res_inst_tac [("s","s2")] streamE 1),
+ (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (strip_tac 1 ),
+ (subgoal_tac "stream_take(n1)[xs] = xs" 1),
+ (rtac ((hd stream_inject) RS conjunct2) 2),
+ (atac 4),
+ (atac 2),
+ (atac 2),
+ (rtac cfun_arg_cong 1),
+ (fast_tac HOL_cs 1)
+ ]);
+
+val stream_take_lemma3 = prove_goal Stream.thy
+ "!x xs.x~=UU --> \
+\ stream_take(n)[scons[x][xs]] = scons[x][xs] --> stream_take(n)[xs]=xs"
+ (fn prems =>
+ [
+ (nat_ind_tac "n" 1),
+ (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (strip_tac 1 ),
+ (res_inst_tac [("P","scons[x][xs]=UU")] notE 1),
+ (eresolve_tac stream_constrdef 1),
+ (etac sym 1),
+ (strip_tac 1 ),
+ (rtac (stream_take_lemma2 RS spec RS mp) 1),
+ (res_inst_tac [("x1.1","x")] ((hd stream_inject) RS conjunct2) 1),
+ (atac 1),
+ (atac 1),
+ (etac (stream_take2 RS subst) 1)
+ ]);
+
+val stream_take_lemma4 = prove_goal Stream.thy
+ "!x xs.\
+\stream_take(n)[xs]=xs --> stream_take(Suc(n))[scons[x][xs]] = scons[x][xs]"
+ (fn prems =>
+ [
+ (nat_ind_tac "n" 1),
+ (simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (simp_tac (HOLCF_ss addsimps stream_rews) 1)
+ ]);
+
+(* ---- *)
+
+val stream_take_lemma5 = prove_goal Stream.thy
+"!s. stream_take(n)[s]=s --> iterate(n,stl,s)=UU"
+ (fn prems =>
+ [
+ (nat_ind_tac "n" 1),
+ (simp_tac iterate_ss 1),
+ (simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (strip_tac 1),
+ (res_inst_tac [("s","s")] streamE 1),
+ (hyp_subst_tac 1),
+ (rtac (iterate_Suc2 RS ssubst) 1),
+ (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (rtac (iterate_Suc2 RS ssubst) 1),
+ (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (etac allE 1),
+ (etac mp 1),
+ (hyp_subst_tac 1),
+ (etac (stream_take_lemma1 RS spec RS spec RS mp RS mp) 1),
+ (atac 1)
+ ]);
+
+val stream_take_lemma6 = prove_goal Stream.thy
+"!s.iterate(n,stl,s)=UU --> stream_take(n)[s]=s"
+ (fn prems =>
+ [
+ (nat_ind_tac "n" 1),
+ (simp_tac iterate_ss 1),
+ (strip_tac 1),
+ (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (rtac allI 1),
+ (res_inst_tac [("s","s")] streamE 1),
+ (hyp_subst_tac 1),
+ (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (hyp_subst_tac 1),
+ (rtac (iterate_Suc2 RS ssubst) 1),
+ (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
+ ]);
+
+val stream_take_lemma7 = prove_goal Stream.thy
+"(iterate(n,stl,s)=UU) = (stream_take(n)[s]=s)"
+ (fn prems =>
+ [
+ (rtac iffI 1),
+ (etac (stream_take_lemma6 RS spec RS mp) 1),
+ (etac (stream_take_lemma5 RS spec RS mp) 1)
+ ]);
+
+
+(* ----------------------------------------------------------------------- *)
+(* lemmas stream_finite *)
+(* ----------------------------------------------------------------------- *)
+
+val stream_finite_lemma1 = prove_goalw Stream.thy [stream_finite_def]
+ "stream_finite(xs) ==> stream_finite(scons[x][xs])"
+ (fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (etac exE 1),
+ (rtac exI 1),
+ (etac (stream_take_lemma4 RS spec RS spec RS mp) 1)
+ ]);
+
+val stream_finite_lemma2 = prove_goalw Stream.thy [stream_finite_def]
+ "[|x~=UU; stream_finite(scons[x][xs])|] ==> stream_finite(xs)"
+ (fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (etac exE 1),
+ (rtac exI 1),
+ (etac (stream_take_lemma3 RS spec RS spec RS mp RS mp) 1),
+ (atac 1)
+ ]);
+
+val stream_finite_lemma3 = prove_goal Stream.thy
+ "x~=UU ==> stream_finite(scons[x][xs]) = stream_finite(xs)"
+ (fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (rtac iffI 1),
+ (etac stream_finite_lemma2 1),
+ (atac 1),
+ (etac stream_finite_lemma1 1)
+ ]);
+
+
+val stream_finite_lemma5 = prove_goalw Stream.thy [stream_finite_def]
+ "(!n. s1 << s2 --> stream_take(n)[s2] = s2 --> stream_finite(s1))\
+\=(s1 << s2 --> stream_finite(s2) --> stream_finite(s1))"
+ (fn prems =>
+ [
+ (rtac iffI 1),
+ (fast_tac HOL_cs 1),
+ (fast_tac HOL_cs 1)
+ ]);
+
+val stream_finite_lemma6 = prove_goal Stream.thy
+ "!s1 s2. s1 << s2 --> stream_take(n)[s2] = s2 --> stream_finite(s1)"
+ (fn prems =>
+ [
+ (nat_ind_tac "n" 1),
+ (simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (strip_tac 1 ),
+ (hyp_subst_tac 1),
+ (dtac UU_I 1),
+ (hyp_subst_tac 1),
+ (rtac stream_finite_UU 1),
+ (rtac allI 1),
+ (rtac allI 1),
+ (res_inst_tac [("s","s1")] streamE 1),
+ (hyp_subst_tac 1),
+ (strip_tac 1 ),
+ (rtac stream_finite_UU 1),
+ (hyp_subst_tac 1),
+ (res_inst_tac [("s","s2")] streamE 1),
+ (hyp_subst_tac 1),
+ (strip_tac 1 ),
+ (dtac UU_I 1),
+ (asm_simp_tac(HOLCF_ss addsimps (stream_rews @ [stream_finite_UU])) 1),
+ (hyp_subst_tac 1),
+ (simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (strip_tac 1 ),
+ (rtac stream_finite_lemma1 1),
+ (subgoal_tac "xs << xsa" 1),
+ (subgoal_tac "stream_take(n1)[xsa] = xsa" 1),
+ (fast_tac HOL_cs 1),
+ (res_inst_tac [("x1.1","xa"),("y1.1","xa")]
+ ((hd stream_inject) RS conjunct2) 1),
+ (atac 1),
+ (atac 1),
+ (atac 1),
+ (res_inst_tac [("x1.1","x"),("y1.1","xa")]
+ ((hd stream_invert) RS conjunct2) 1),
+ (atac 1),
+ (atac 1),
+ (atac 1)
+ ]);
+
+val stream_finite_lemma7 = prove_goal Stream.thy
+"s1 << s2 --> stream_finite(s2) --> stream_finite(s1)"
+ (fn prems =>
+ [
+ (rtac (stream_finite_lemma5 RS iffD1) 1),
+ (rtac allI 1),
+ (rtac (stream_finite_lemma6 RS spec RS spec) 1)
+ ]);
+
+val stream_finite_lemma8 = prove_goalw Stream.thy [stream_finite_def]
+"stream_finite(s) = (? n. iterate(n,stl,s)=UU)"
+ (fn prems =>
+ [
+ (simp_tac (HOL_ss addsimps [stream_take_lemma7]) 1)
+ ]);
+
+
+(* ----------------------------------------------------------------------- *)
+(* admissibility of ~stream_finite *)
+(* ----------------------------------------------------------------------- *)
+
+val adm_not_stream_finite = prove_goalw Stream.thy [adm_def]
+ "adm(%s. ~ stream_finite(s))"
+ (fn prems =>
+ [
+ (strip_tac 1 ),
+ (res_inst_tac [("P1","!i. ~ stream_finite(Y(i))")] classical3 1),
+ (atac 2),
+ (subgoal_tac "!i.stream_finite(Y(i))" 1),
+ (fast_tac HOL_cs 1),
+ (rtac allI 1),
+ (rtac (stream_finite_lemma7 RS mp RS mp) 1),
+ (etac is_ub_thelub 1),
+ (atac 1)
+ ]);
+
+(* ----------------------------------------------------------------------- *)
+(* alternative prove for admissibility of ~stream_finite *)
+(* show that stream_finite(s) = (? n. iterate(n, stl, s) = UU) *)
+(* and prove adm. of ~(? n. iterate(n, stl, s) = UU) *)
+(* proof uses theorems stream_take_lemma5-7; stream_finite_lemma8 *)
+(* ----------------------------------------------------------------------- *)
+
+
+val adm_not_stream_finite2=prove_goal Stream.thy "adm(%s. ~ stream_finite(s))"
+ (fn prems =>
+ [
+ (subgoal_tac "(!s.(~stream_finite(s))=(!n.iterate(n,stl,s)~=UU))" 1),
+ (etac (adm_cong RS iffD2)1),
+ (REPEAT(resolve_tac adm_thms 1)),
+ (rtac contX_iterate2 1),
+ (rtac allI 1),
+ (rtac (stream_finite_lemma8 RS ssubst) 1),
+ (fast_tac HOL_cs 1)
+ ]);
+
+
--- a/src/HOLCF/Stream2.thy Thu Mar 24 13:25:12 1994 +0100
+++ b/src/HOLCF/Stream2.thy Thu Mar 24 13:36:34 1994 +0100
@@ -19,7 +19,7 @@
end
-
+
(*
smap[f][UU] = UU
--- a/src/HOLCF/cfun2.ML Thu Mar 24 13:25:12 1994 +0100
+++ b/src/HOLCF/cfun2.ML Thu Mar 24 13:36:34 1994 +0100
@@ -216,7 +216,7 @@
is_chain(?CCF1) ==> lub(range(?CCF1)) = fabs(%x. lub(range(%i. ?CCF1(i)[x])))
*)
-val cpo_fun = prove_goal Cfun2.thy
+val cpo_cfun = prove_goal Cfun2.thy
"is_chain(CCF::nat=>('a::pcpo->'b::pcpo)) ==> ? x. range(CCF) <<| x"
(fn prems =>
[
--- a/src/HOLCF/dnat.ML Thu Mar 24 13:25:12 1994 +0100
+++ b/src/HOLCF/dnat.ML Thu Mar 24 13:36:34 1994 +0100
@@ -171,41 +171,49 @@
(* Distinctness wrt. << and = *)
(* ------------------------------------------------------------------------*)
-fun prover contrfun thm = prove_goal Dnat.thy thm
+val temp = prove_goal Dnat.thy "~dzero << dsucc[n]"
+ (fn prems =>
+ [
+ (res_inst_tac [("P1","TT << FF")] classical3 1),
+ (resolve_tac dist_less_tr 1),
+ (dres_inst_tac [("fo5","is_dzero")] monofun_cfun_arg 1),
+ (etac box_less 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (res_inst_tac [("Q","n=UU")] classical2 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
+ ]);
+
+val dnat_dist_less = [temp];
+
+val temp = prove_goal Dnat.thy "n~=UU ==> ~dsucc[n] << dzero"
(fn prems =>
[
(cut_facts_tac prems 1),
(res_inst_tac [("P1","TT << FF")] classical3 1),
(resolve_tac dist_less_tr 1),
- (dres_inst_tac [("fo5",contrfun)] monofun_cfun_arg 1),
+ (dres_inst_tac [("fo5","is_dsucc")] monofun_cfun_arg 1),
(etac box_less 1),
(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
]);
-val dnat_dist_less =
- [
-prover "is_dzero" "n~=UU ==> ~dzero << dsucc[n]",
-prover "is_dsucc" "n~=UU ==> ~dsucc[n] << dzero"
- ];
+val dnat_dist_less = temp::dnat_dist_less;
-fun prover contrfun thm = prove_goal Dnat.thy thm
+val temp = prove_goal Dnat.thy "dzero ~= dsucc[n]"
(fn prems =>
[
- (cut_facts_tac prems 1),
+ (res_inst_tac [("Q","n=UU")] classical2 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
(res_inst_tac [("P1","TT = FF")] classical3 1),
(resolve_tac dist_eq_tr 1),
- (dres_inst_tac [("f",contrfun)] cfun_arg_cong 1),
+ (dres_inst_tac [("f","is_dzero")] cfun_arg_cong 1),
(etac box_equals 1),
(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
]);
-val dnat_dist_eq =
- [
-prover "is_dzero" "n~=UU ==> dzero ~= dsucc[n]",
-prover "is_dsucc" "n~=UU ==> dsucc[n] ~= dzero"
- ];
+val dnat_dist_eq = [temp, temp RS not_sym];
val dnat_rews = dnat_dist_less @ dnat_dist_eq @ dnat_rews;
@@ -271,39 +279,57 @@
(* ------------------------------------------------------------------------*)
(* Properties dnat_take *)
(* ------------------------------------------------------------------------*)
-
-val dnat_take =
- [
-prove_goalw Dnat.thy [dnat_take_def] "dnat_take(n)[UU]=UU"
+val temp = prove_goalw Dnat.thy [dnat_take_def] "dnat_take(n)[UU]=UU"
(fn prems =>
[
(res_inst_tac [("n","n")] natE 1),
(asm_simp_tac iterate_ss 1),
(asm_simp_tac iterate_ss 1),
(simp_tac (HOLCF_ss addsimps dnat_rews) 1)
- ]),
-prove_goalw Dnat.thy [dnat_take_def] "dnat_take(0)[xs]=UU"
+ ]);
+
+val dnat_take = [temp];
+
+val temp = prove_goalw Dnat.thy [dnat_take_def] "dnat_take(0)[xs]=UU"
(fn prems =>
[
(asm_simp_tac iterate_ss 1)
- ])];
+ ]);
-fun prover thm = prove_goalw Dnat.thy [dnat_take_def] thm
+val dnat_take = temp::dnat_take;
+
+val temp = prove_goalw Dnat.thy [dnat_take_def]
+ "dnat_take(Suc(n))[dzero]=dzero"
(fn prems =>
[
- (cut_facts_tac prems 1),
- (simp_tac iterate_ss 1),
+ (asm_simp_tac iterate_ss 1),
+ (simp_tac (HOLCF_ss addsimps dnat_rews) 1)
+ ]);
+
+val dnat_take = temp::dnat_take;
+
+val temp = prove_goalw Dnat.thy [dnat_take_def]
+ "dnat_take(Suc(n))[dsucc[xs]]=dsucc[dnat_take(n)[xs]]"
+ (fn prems =>
+ [
+ (res_inst_tac [("Q","xs=UU")] classical2 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (asm_simp_tac iterate_ss 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (res_inst_tac [("n","n")] natE 1),
+ (asm_simp_tac iterate_ss 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (asm_simp_tac iterate_ss 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (asm_simp_tac iterate_ss 1),
(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
]);
-val dnat_take = [
-prover "dnat_take(Suc(n))[dzero]=dzero",
-prover "xs~=UU ==> dnat_take(Suc(n))[dsucc[xs]]=dsucc[dnat_take(n)[xs]]"
- ] @ dnat_take;
-
+val dnat_take = temp::dnat_take;
val dnat_rews = dnat_take @ dnat_rews;
+
(* ------------------------------------------------------------------------*)
(* take lemma for dnats *)
(* ------------------------------------------------------------------------*)
@@ -368,6 +394,7 @@
(* structural induction for admissible predicates *)
(* ------------------------------------------------------------------------*)
+(* not needed any longer
val dnat_ind = prove_goal Dnat.thy
"[| adm(P);\
\ P(UU);\
@@ -397,6 +424,79 @@
(eresolve_tac prems 1),
(etac spec 1)
]);
+*)
+
+val dnat_finite_ind = prove_goal Dnat.thy
+"[|P(UU);P(dzero);\
+\ !! s1.[|s1~=UU;P(s1)|] ==> P(dsucc[s1])\
+\ |] ==> !s.P(dnat_take(n)[s])"
+ (fn prems =>
+ [
+ (nat_ind_tac "n" 1),
+ (simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (resolve_tac prems 1),
+ (rtac allI 1),
+ (res_inst_tac [("n","s")] dnatE 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (resolve_tac prems 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (resolve_tac prems 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (res_inst_tac [("Q","dnat_take(n1)[x]=UU")] classical2 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (resolve_tac prems 1),
+ (resolve_tac prems 1),
+ (atac 1),
+ (etac spec 1)
+ ]);
+
+val dnat_all_finite_lemma1 = prove_goal Dnat.thy
+"!s.dnat_take(n)[s]=UU |dnat_take(n)[s]=s"
+ (fn prems =>
+ [
+ (nat_ind_tac "n" 1),
+ (simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (rtac allI 1),
+ (res_inst_tac [("n","s")] dnatE 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (eres_inst_tac [("x","x")] allE 1),
+ (etac disjE 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
+ ]);
+
+val dnat_all_finite_lemma2 = prove_goal Dnat.thy "? n.dnat_take(n)[s]=s"
+ (fn prems =>
+ [
+ (res_inst_tac [("Q","s=UU")] classical2 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (subgoal_tac "(!n.dnat_take(n)[s]=UU) |(? n.dnat_take(n)[s]=s)" 1),
+ (etac disjE 1),
+ (eres_inst_tac [("P","s=UU")] notE 1),
+ (rtac dnat_take_lemma 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (atac 1),
+ (subgoal_tac "!n.!s.dnat_take(n)[s]=UU |dnat_take(n)[s]=s" 1),
+ (fast_tac HOL_cs 1),
+ (rtac allI 1),
+ (rtac dnat_all_finite_lemma1 1)
+ ]);
+
+
+val dnat_ind = prove_goal Dnat.thy
+"[|P(UU);P(dzero);\
+\ !! s1.[|s1~=UU;P(s1)|] ==> P(dsucc[s1])\
+\ |] ==> P(s)"
+ (fn prems =>
+ [
+ (rtac (dnat_all_finite_lemma2 RS exE) 1),
+ (etac subst 1),
+ (rtac (dnat_finite_ind RS spec) 1),
+ (REPEAT (resolve_tac prems 1)),
+ (REPEAT (atac 1))
+ ]);
val dnat_flat = prove_goalw Dnat.thy [flat_def] "flat(dzero)"
@@ -404,12 +504,6 @@
[
(rtac allI 1),
(res_inst_tac [("s","x")] dnat_ind 1),
- (REPEAT (resolve_tac adm_thms 1)),
- (contX_tacR 1),
- (REPEAT (resolve_tac adm_thms 1)),
- (contX_tacR 1),
- (REPEAT (resolve_tac adm_thms 1)),
- (contX_tacR 1),
(fast_tac HOL_cs 1),
(rtac allI 1),
(res_inst_tac [("n","y")] dnatE 1),
@@ -419,53 +513,20 @@
(rtac allI 1),
(res_inst_tac [("n","y")] dnatE 1),
(fast_tac (HOL_cs addSIs [UU_I]) 1),
+ (asm_simp_tac (HOLCF_ss addsimps dnat_dist_less) 1),
(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
- (hyp_subst_tac 1),
(strip_tac 1),
- (rtac disjI2 1),
- (forward_tac dnat_invert 1),
- (atac 2),
- (atac 1),
+ (subgoal_tac "s1<<xa" 1),
(etac allE 1),
(dtac mp 1),
(atac 1),
(etac disjE 1),
(contr_tac 1),
- (asm_simp_tac HOLCF_ss 1)
+ (asm_simp_tac HOLCF_ss 1),
+ (resolve_tac dnat_invert 1),
+ (REPEAT (atac 1))
]);
-val dnat_ind = prove_goal Dnat.thy
-"[| adm(P);\
-\ P(UU);\
-\ P(dzero);\
-\ !! s1.[|s1~=UU ; P(s1)|] ==> P(dsucc[s1])|] ==> P(s)"
- (fn prems =>
- [
- (rtac (dnat_reach RS subst) 1),
- (res_inst_tac [("x","s")] spec 1),
- (rtac fix_ind 1),
- (rtac adm_all2 1),
- (rtac adm_subst 1),
- (contX_tacR 1),
- (resolve_tac prems 1),
- (simp_tac HOLCF_ss 1),
- (resolve_tac prems 1),
- (strip_tac 1),
- (res_inst_tac [("n","xa")] dnatE 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_copy) 1),
- (resolve_tac prems 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_copy) 1),
- (resolve_tac prems 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_copy) 1),
- (res_inst_tac [("Q","x[xb]=UU")] classical2 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
- (resolve_tac prems 1),
- (eresolve_tac prems 1),
- (etac spec 1)
- ]);
+
-val dnat_ind2 = dnat_flat RS adm_flat RS dnat_ind;
-(* "[| ?P(UU); ?P(dzero);
- !!s1. [| s1 ~= UU; ?P(s1) |] ==> ?P(dsucc[s1]) |] ==> ?P(?s)" : thm
-*)
--- a/src/HOLCF/ex/Coind.ML Thu Mar 24 13:25:12 1994 +0100
+++ b/src/HOLCF/ex/Coind.ML Thu Mar 24 13:36:34 1994 +0100
@@ -57,7 +57,7 @@
\ scons[n][iterator[dsucc[n]][smap[dsucc]][nats]]"
(fn prems =>
[
- (res_inst_tac [("s","n")] dnat_ind2 1),
+ (res_inst_tac [("s","n")] dnat_ind 1),
(simp_tac (HOLCF_ss addsimps (coind_rews @ stream_rews)) 1),
(simp_tac (HOLCF_ss addsimps (coind_rews @ stream_rews)) 1),
(rtac trans 1),
--- a/src/HOLCF/ex/ROOT.ML Thu Mar 24 13:25:12 1994 +0100
+++ b/src/HOLCF/ex/ROOT.ML Thu Mar 24 13:36:34 1994 +0100
@@ -13,4 +13,6 @@
time_use_thy "ex/Coind";
time_use_thy "ex/Hoare";
time_use_thy "ex/Loop";
+time_use_thy "ex/Dagstuhl";
+
maketest "END: Root file for HOLCF examples";
--- a/src/HOLCF/ex/coind.ML Thu Mar 24 13:25:12 1994 +0100
+++ b/src/HOLCF/ex/coind.ML Thu Mar 24 13:36:34 1994 +0100
@@ -57,7 +57,7 @@
\ scons[n][iterator[dsucc[n]][smap[dsucc]][nats]]"
(fn prems =>
[
- (res_inst_tac [("s","n")] dnat_ind2 1),
+ (res_inst_tac [("s","n")] dnat_ind 1),
(simp_tac (HOLCF_ss addsimps (coind_rews @ stream_rews)) 1),
(simp_tac (HOLCF_ss addsimps (coind_rews @ stream_rews)) 1),
(rtac trans 1),
--- a/src/HOLCF/fix.ML Thu Mar 24 13:25:12 1994 +0100
+++ b/src/HOLCF/fix.ML Thu Mar 24 13:36:34 1994 +0100
@@ -387,6 +387,19 @@
(rtac refl 1)
]);
+(* ------------------------------------------------------------------------
+
+given the definition
+
+smap_def
+ "smap = fix[LAM h f s. stream_when[LAM x l.scons[f[x]][h[f][l]]][s]]"
+
+use fix_prover for
+
+val smap_def2 = fix_prover Stream2.thy smap_def
+ "smap = (LAM f s. stream_when[LAM x l.scons[f[x]][smap[f][l]]][s])";
+
+ ------------------------------------------------------------------------ *)
(* ------------------------------------------------------------------------ *)
(* better access to definitions *)
@@ -881,7 +894,7 @@
(rtac iffI 1),
(etac FalseE 2),
(rtac notE 1),
- (etac less_not_sym 1),
+ (etac (less_not_sym RS mp) 1),
(atac 1),
(asm_simp_tac Cfun_ss 1),
(etac (is_chainE RS spec) 1),
@@ -921,7 +934,7 @@
(rtac iffI 1),
(etac FalseE 2),
(rtac notE 1),
- (etac less_not_sym 1),
+ (etac (less_not_sym RS mp) 1),
(atac 1),
(asm_simp_tac nat_ss 1),
(dtac spec 1),
--- a/src/HOLCF/porder.ML Thu Mar 24 13:25:12 1994 +0100
+++ b/src/HOLCF/porder.ML Thu Mar 24 13:36:34 1994 +0100
@@ -6,9 +6,9 @@
Lemmas for theory porder.thy
*)
+open Porder0;
open Porder;
-
val box_less = prove_goal Porder.thy
"[| a << b; c << a; b << d|] ==> c << d"
(fn prems =>
--- a/src/HOLCF/porder.thy Thu Mar 24 13:25:12 1994 +0100
+++ b/src/HOLCF/porder.thy Thu Mar 24 13:36:34 1994 +0100
@@ -3,25 +3,13 @@
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
-Definition of class porder (partial order)
-
-The prototype theory for this class is void.thy
+Conservative extension of theory Porder0 by constant definitions
*)
-Porder = Void +
-
-(* Introduction of new class. The witness is type void. *)
-
-classes po < term
+Porder = Porder0 +
-(* default type is still term ! *)
-(* void is the prototype in po *)
-
-arities void :: po
-
-consts "<<" :: "['a,'a::po] => bool" (infixl 55)
-
+consts
"<|" :: "['a set,'a::po] => bool" (infixl 55)
"<<|" :: "['a set,'a::po] => bool" (infixl 55)
lub :: "'a set => 'a::po"
@@ -32,21 +20,6 @@
rules
-(* class axioms: justification is theory Void *)
-
-refl_less "x << x"
- (* witness refl_less_void *)
-
-antisym_less "[|x<<y ; y<<x |] ==> x = y"
- (* witness antisym_less_void *)
-
-trans_less "[|x<<y ; y<<z |] ==> x<<z"
- (* witness trans_less_void *)
-
-(* instance of << for the prototype void *)
-
-inst_void_po "(op <<)::[void,void]=>bool = less_void"
-
(* class definitions *)
is_ub "S <| x == ! y.y:S --> y<<x"
@@ -57,11 +30,9 @@
(* Arbitrary chains are total orders *)
is_tord "is_tord(S) == ! x y. x:S & y:S --> (x<<y | y<<x)"
-
(* Here we use countable chains and I prefer to code them as functions! *)
is_chain "is_chain(F) == (! i.F(i) << F(Suc(i)))"
-
(* finite chains, needed for monotony of continouous functions *)
max_in_chain_def "max_in_chain(i,C) == ! j. i <= j --> C(i) = C(j)"
--- a/src/HOLCF/stream.ML Thu Mar 24 13:25:12 1994 +0100
+++ b/src/HOLCF/stream.ML Thu Mar 24 13:36:34 1994 +0100
@@ -229,6 +229,7 @@
val stream_rews = stream_discsel_def @ stream_rews;
+
(* ------------------------------------------------------------------------*)
(* Properties stream_take *)
(* ------------------------------------------------------------------------*)
@@ -265,6 +266,46 @@
val stream_rews = stream_take @ stream_rews;
(* ------------------------------------------------------------------------*)
+(* enhance the simplifier *)
+(* ------------------------------------------------------------------------*)
+
+val stream_copy2 = prove_goal Stream.thy
+ "stream_copy[f][scons[x][xs]]= scons[x][f[xs]]"
+ (fn prems =>
+ [
+ (res_inst_tac [("Q","x=UU")] classical2 1),
+ (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
+ ]);
+
+val shd2 = prove_goal Stream.thy "shd[scons[x][xs]]=x"
+ (fn prems =>
+ [
+ (res_inst_tac [("Q","x=UU")] classical2 1),
+ (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
+ ]);
+
+val stream_take2 = prove_goal Stream.thy
+ "stream_take(Suc(n))[scons[x][xs]]=scons[x][stream_take(n)[xs]]"
+ (fn prems =>
+ [
+ (res_inst_tac [("Q","x=UU")] classical2 1),
+ (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
+ ]);
+
+val stream_rews = [stream_iso_strict RS conjunct1,
+ stream_iso_strict RS conjunct2,
+ hd stream_copy, stream_copy2]
+ @ stream_when
+ @ [hd stream_discsel,shd2] @ (tl (tl stream_discsel))
+ @ stream_constrdef
+ @ stream_discsel_def
+ @ [ stream_take2] @ (tl stream_take);
+
+
+(* ------------------------------------------------------------------------*)
(* take lemma for streams *)
(* ------------------------------------------------------------------------*)
@@ -326,8 +367,49 @@
(* structural induction for admissible predicates *)
(* ------------------------------------------------------------------------*)
+val stream_finite_ind = prove_goal Stream.thy
+"[|P(UU);\
+\ !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
+\ |] ==> !s.P(stream_take(n)[s])"
+ (fn prems =>
+ [
+ (nat_ind_tac "n" 1),
+ (simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (resolve_tac prems 1),
+ (rtac allI 1),
+ (res_inst_tac [("s","s")] streamE 1),
+ (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (resolve_tac prems 1),
+ (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (resolve_tac prems 1),
+ (atac 1),
+ (etac spec 1)
+ ]);
+
+val stream_finite_ind2 = prove_goalw Stream.thy [stream_finite_def]
+"(!!n.P(stream_take(n)[s])) ==> stream_finite(s) -->P(s)"
+ (fn prems =>
+ [
+ (strip_tac 1),
+ (etac exE 1),
+ (etac subst 1),
+ (resolve_tac prems 1)
+ ]);
+
+val stream_finite_ind3 = prove_goal Stream.thy
+"[|P(UU);\
+\ !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
+\ |] ==> stream_finite(s) --> P(s)"
+ (fn prems =>
+ [
+ (rtac stream_finite_ind2 1),
+ (rtac (stream_finite_ind RS spec) 1),
+ (REPEAT (resolve_tac prems 1)),
+ (REPEAT (atac 1))
+ ]);
+
val stream_ind = prove_goal Stream.thy
-"[| adm(P);\
+"[|adm(P);\
\ P(UU);\
\ !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
\ |] ==> P(s)"
@@ -335,21 +417,16 @@
[
(rtac (stream_reach RS subst) 1),
(res_inst_tac [("x","s")] spec 1),
- (rtac fix_ind 1),
- (rtac (allI RS adm_all) 1),
+ (rtac wfix_ind 1),
+ (rtac adm_impl_admw 1),
+ (REPEAT (resolve_tac adm_thms 1)),
(rtac adm_subst 1),
(contX_tacR 1),
(resolve_tac prems 1),
- (simp_tac HOLCF_ss 1),
- (resolve_tac prems 1),
- (strip_tac 1),
- (res_inst_tac [("s","xa")] streamE 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
- (resolve_tac prems 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
- (resolve_tac prems 1),
- (atac 1),
- (etac spec 1)
+ (rtac allI 1),
+ (rtac (rewrite_rule [stream_take_def] stream_finite_ind) 1),
+ (REPEAT (resolve_tac prems 1)),
+ (REPEAT (atac 1))
]);
@@ -403,3 +480,312 @@
]);
+(* ------------------------------------------------------------------------*)
+(* theorems about finite and infinite streams *)
+(* ------------------------------------------------------------------------*)
+
+(* ----------------------------------------------------------------------- *)
+(* 2 lemmas about stream_finite *)
+(* ----------------------------------------------------------------------- *)
+
+val stream_finite_UU = prove_goalw Stream.thy [stream_finite_def]
+ "stream_finite(UU)"
+ (fn prems =>
+ [
+ (rtac exI 1),
+ (simp_tac (HOLCF_ss addsimps stream_rews) 1)
+ ]);
+
+val inf_stream_not_UU = prove_goal Stream.thy "~stream_finite(s) ==> s ~= UU"
+ (fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (etac swap 1),
+ (dtac notnotD 1),
+ (hyp_subst_tac 1),
+ (rtac stream_finite_UU 1)
+ ]);
+
+(* ----------------------------------------------------------------------- *)
+(* a lemma about shd *)
+(* ----------------------------------------------------------------------- *)
+
+val stream_shd_lemma1 = prove_goal Stream.thy "shd[s]=UU --> s=UU"
+ (fn prems =>
+ [
+ (res_inst_tac [("s","s")] streamE 1),
+ (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (hyp_subst_tac 1),
+ (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
+ ]);
+
+
+(* ----------------------------------------------------------------------- *)
+(* lemmas about stream_take *)
+(* ----------------------------------------------------------------------- *)
+
+val stream_take_lemma1 = prove_goal Stream.thy
+ "!x xs.x~=UU --> \
+\ stream_take(Suc(n))[scons[x][xs]] = scons[x][xs] --> stream_take(n)[xs]=xs"
+ (fn prems =>
+ [
+ (rtac allI 1),
+ (rtac allI 1),
+ (rtac impI 1),
+ (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (strip_tac 1),
+ (rtac ((hd stream_inject) RS conjunct2) 1),
+ (atac 1),
+ (atac 1),
+ (atac 1)
+ ]);
+
+
+val stream_take_lemma2 = prove_goal Stream.thy
+ "! s2. stream_take(n)[s2] = s2 --> stream_take(Suc(n))[s2]=s2"
+ (fn prems =>
+ [
+ (nat_ind_tac "n" 1),
+ (simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (strip_tac 1 ),
+ (hyp_subst_tac 1),
+ (simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (rtac allI 1),
+ (res_inst_tac [("s","s2")] streamE 1),
+ (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (strip_tac 1 ),
+ (subgoal_tac "stream_take(n1)[xs] = xs" 1),
+ (rtac ((hd stream_inject) RS conjunct2) 2),
+ (atac 4),
+ (atac 2),
+ (atac 2),
+ (rtac cfun_arg_cong 1),
+ (fast_tac HOL_cs 1)
+ ]);
+
+val stream_take_lemma3 = prove_goal Stream.thy
+ "!x xs.x~=UU --> \
+\ stream_take(n)[scons[x][xs]] = scons[x][xs] --> stream_take(n)[xs]=xs"
+ (fn prems =>
+ [
+ (nat_ind_tac "n" 1),
+ (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (strip_tac 1 ),
+ (res_inst_tac [("P","scons[x][xs]=UU")] notE 1),
+ (eresolve_tac stream_constrdef 1),
+ (etac sym 1),
+ (strip_tac 1 ),
+ (rtac (stream_take_lemma2 RS spec RS mp) 1),
+ (res_inst_tac [("x1.1","x")] ((hd stream_inject) RS conjunct2) 1),
+ (atac 1),
+ (atac 1),
+ (etac (stream_take2 RS subst) 1)
+ ]);
+
+val stream_take_lemma4 = prove_goal Stream.thy
+ "!x xs.\
+\stream_take(n)[xs]=xs --> stream_take(Suc(n))[scons[x][xs]] = scons[x][xs]"
+ (fn prems =>
+ [
+ (nat_ind_tac "n" 1),
+ (simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (simp_tac (HOLCF_ss addsimps stream_rews) 1)
+ ]);
+
+(* ---- *)
+
+val stream_take_lemma5 = prove_goal Stream.thy
+"!s. stream_take(n)[s]=s --> iterate(n,stl,s)=UU"
+ (fn prems =>
+ [
+ (nat_ind_tac "n" 1),
+ (simp_tac iterate_ss 1),
+ (simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (strip_tac 1),
+ (res_inst_tac [("s","s")] streamE 1),
+ (hyp_subst_tac 1),
+ (rtac (iterate_Suc2 RS ssubst) 1),
+ (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (rtac (iterate_Suc2 RS ssubst) 1),
+ (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (etac allE 1),
+ (etac mp 1),
+ (hyp_subst_tac 1),
+ (etac (stream_take_lemma1 RS spec RS spec RS mp RS mp) 1),
+ (atac 1)
+ ]);
+
+val stream_take_lemma6 = prove_goal Stream.thy
+"!s.iterate(n,stl,s)=UU --> stream_take(n)[s]=s"
+ (fn prems =>
+ [
+ (nat_ind_tac "n" 1),
+ (simp_tac iterate_ss 1),
+ (strip_tac 1),
+ (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (rtac allI 1),
+ (res_inst_tac [("s","s")] streamE 1),
+ (hyp_subst_tac 1),
+ (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (hyp_subst_tac 1),
+ (rtac (iterate_Suc2 RS ssubst) 1),
+ (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
+ ]);
+
+val stream_take_lemma7 = prove_goal Stream.thy
+"(iterate(n,stl,s)=UU) = (stream_take(n)[s]=s)"
+ (fn prems =>
+ [
+ (rtac iffI 1),
+ (etac (stream_take_lemma6 RS spec RS mp) 1),
+ (etac (stream_take_lemma5 RS spec RS mp) 1)
+ ]);
+
+
+(* ----------------------------------------------------------------------- *)
+(* lemmas stream_finite *)
+(* ----------------------------------------------------------------------- *)
+
+val stream_finite_lemma1 = prove_goalw Stream.thy [stream_finite_def]
+ "stream_finite(xs) ==> stream_finite(scons[x][xs])"
+ (fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (etac exE 1),
+ (rtac exI 1),
+ (etac (stream_take_lemma4 RS spec RS spec RS mp) 1)
+ ]);
+
+val stream_finite_lemma2 = prove_goalw Stream.thy [stream_finite_def]
+ "[|x~=UU; stream_finite(scons[x][xs])|] ==> stream_finite(xs)"
+ (fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (etac exE 1),
+ (rtac exI 1),
+ (etac (stream_take_lemma3 RS spec RS spec RS mp RS mp) 1),
+ (atac 1)
+ ]);
+
+val stream_finite_lemma3 = prove_goal Stream.thy
+ "x~=UU ==> stream_finite(scons[x][xs]) = stream_finite(xs)"
+ (fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (rtac iffI 1),
+ (etac stream_finite_lemma2 1),
+ (atac 1),
+ (etac stream_finite_lemma1 1)
+ ]);
+
+
+val stream_finite_lemma5 = prove_goalw Stream.thy [stream_finite_def]
+ "(!n. s1 << s2 --> stream_take(n)[s2] = s2 --> stream_finite(s1))\
+\=(s1 << s2 --> stream_finite(s2) --> stream_finite(s1))"
+ (fn prems =>
+ [
+ (rtac iffI 1),
+ (fast_tac HOL_cs 1),
+ (fast_tac HOL_cs 1)
+ ]);
+
+val stream_finite_lemma6 = prove_goal Stream.thy
+ "!s1 s2. s1 << s2 --> stream_take(n)[s2] = s2 --> stream_finite(s1)"
+ (fn prems =>
+ [
+ (nat_ind_tac "n" 1),
+ (simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (strip_tac 1 ),
+ (hyp_subst_tac 1),
+ (dtac UU_I 1),
+ (hyp_subst_tac 1),
+ (rtac stream_finite_UU 1),
+ (rtac allI 1),
+ (rtac allI 1),
+ (res_inst_tac [("s","s1")] streamE 1),
+ (hyp_subst_tac 1),
+ (strip_tac 1 ),
+ (rtac stream_finite_UU 1),
+ (hyp_subst_tac 1),
+ (res_inst_tac [("s","s2")] streamE 1),
+ (hyp_subst_tac 1),
+ (strip_tac 1 ),
+ (dtac UU_I 1),
+ (asm_simp_tac(HOLCF_ss addsimps (stream_rews @ [stream_finite_UU])) 1),
+ (hyp_subst_tac 1),
+ (simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (strip_tac 1 ),
+ (rtac stream_finite_lemma1 1),
+ (subgoal_tac "xs << xsa" 1),
+ (subgoal_tac "stream_take(n1)[xsa] = xsa" 1),
+ (fast_tac HOL_cs 1),
+ (res_inst_tac [("x1.1","xa"),("y1.1","xa")]
+ ((hd stream_inject) RS conjunct2) 1),
+ (atac 1),
+ (atac 1),
+ (atac 1),
+ (res_inst_tac [("x1.1","x"),("y1.1","xa")]
+ ((hd stream_invert) RS conjunct2) 1),
+ (atac 1),
+ (atac 1),
+ (atac 1)
+ ]);
+
+val stream_finite_lemma7 = prove_goal Stream.thy
+"s1 << s2 --> stream_finite(s2) --> stream_finite(s1)"
+ (fn prems =>
+ [
+ (rtac (stream_finite_lemma5 RS iffD1) 1),
+ (rtac allI 1),
+ (rtac (stream_finite_lemma6 RS spec RS spec) 1)
+ ]);
+
+val stream_finite_lemma8 = prove_goalw Stream.thy [stream_finite_def]
+"stream_finite(s) = (? n. iterate(n,stl,s)=UU)"
+ (fn prems =>
+ [
+ (simp_tac (HOL_ss addsimps [stream_take_lemma7]) 1)
+ ]);
+
+
+(* ----------------------------------------------------------------------- *)
+(* admissibility of ~stream_finite *)
+(* ----------------------------------------------------------------------- *)
+
+val adm_not_stream_finite = prove_goalw Stream.thy [adm_def]
+ "adm(%s. ~ stream_finite(s))"
+ (fn prems =>
+ [
+ (strip_tac 1 ),
+ (res_inst_tac [("P1","!i. ~ stream_finite(Y(i))")] classical3 1),
+ (atac 2),
+ (subgoal_tac "!i.stream_finite(Y(i))" 1),
+ (fast_tac HOL_cs 1),
+ (rtac allI 1),
+ (rtac (stream_finite_lemma7 RS mp RS mp) 1),
+ (etac is_ub_thelub 1),
+ (atac 1)
+ ]);
+
+(* ----------------------------------------------------------------------- *)
+(* alternative prove for admissibility of ~stream_finite *)
+(* show that stream_finite(s) = (? n. iterate(n, stl, s) = UU) *)
+(* and prove adm. of ~(? n. iterate(n, stl, s) = UU) *)
+(* proof uses theorems stream_take_lemma5-7; stream_finite_lemma8 *)
+(* ----------------------------------------------------------------------- *)
+
+
+val adm_not_stream_finite2=prove_goal Stream.thy "adm(%s. ~ stream_finite(s))"
+ (fn prems =>
+ [
+ (subgoal_tac "(!s.(~stream_finite(s))=(!n.iterate(n,stl,s)~=UU))" 1),
+ (etac (adm_cong RS iffD2)1),
+ (REPEAT(resolve_tac adm_thms 1)),
+ (rtac contX_iterate2 1),
+ (rtac allI 1),
+ (rtac (stream_finite_lemma8 RS ssubst) 1),
+ (fast_tac HOL_cs 1)
+ ]);
+
+
--- a/src/HOLCF/stream2.thy Thu Mar 24 13:25:12 1994 +0100
+++ b/src/HOLCF/stream2.thy Thu Mar 24 13:36:34 1994 +0100
@@ -19,7 +19,7 @@
end
-
+
(*
smap[f][UU] = UU