# HG changeset patch # User nipkow # Date 764512594 -3600 # Node ID 5ef75ff3baeb943719758274193c27dc47348a27 # Parent e1f6cd9f682ed59f1a84776a28602984d176ddff Franz fragen diff -r e1f6cd9f682e -r 5ef75ff3baeb src/HOLCF/Cfun2.ML --- 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 => [ diff -r e1f6cd9f682e -r 5ef75ff3baeb src/HOLCF/Dnat.ML --- 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< 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 -*) diff -r e1f6cd9f682e -r 5ef75ff3baeb src/HOLCF/Fix.ML --- 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), diff -r e1f6cd9f682e -r 5ef75ff3baeb src/HOLCF/Porder.ML --- 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 => diff -r e1f6cd9f682e -r 5ef75ff3baeb src/HOLCF/Porder.thy --- 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< x = y" - (* witness antisym_less_void *) - -trans_less "[|x< x<bool = less_void" - (* class definitions *) is_ub "S <| x == ! y.y:S --> y< (x< C(i) = C(j)" diff -r e1f6cd9f682e -r 5ef75ff3baeb src/HOLCF/ROOT.ML --- 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; diff -r e1f6cd9f682e -r 5ef75ff3baeb src/HOLCF/Stream.ML --- 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) + ]); + + diff -r e1f6cd9f682e -r 5ef75ff3baeb src/HOLCF/Stream2.thy --- 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 diff -r e1f6cd9f682e -r 5ef75ff3baeb src/HOLCF/cfun2.ML --- 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 => [ diff -r e1f6cd9f682e -r 5ef75ff3baeb src/HOLCF/dnat.ML --- 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< 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 -*) diff -r e1f6cd9f682e -r 5ef75ff3baeb src/HOLCF/ex/Coind.ML --- 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), diff -r e1f6cd9f682e -r 5ef75ff3baeb src/HOLCF/ex/ROOT.ML --- 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"; diff -r e1f6cd9f682e -r 5ef75ff3baeb src/HOLCF/ex/coind.ML --- 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), diff -r e1f6cd9f682e -r 5ef75ff3baeb src/HOLCF/fix.ML --- 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), diff -r e1f6cd9f682e -r 5ef75ff3baeb src/HOLCF/porder.ML --- 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 => diff -r e1f6cd9f682e -r 5ef75ff3baeb src/HOLCF/porder.thy --- 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< x = y" - (* witness antisym_less_void *) - -trans_less "[|x< x<bool = less_void" - (* class definitions *) is_ub "S <| x == ! y.y:S --> y< (x< C(i) = C(j)" diff -r e1f6cd9f682e -r 5ef75ff3baeb src/HOLCF/stream.ML --- 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) + ]); + + diff -r e1f6cd9f682e -r 5ef75ff3baeb src/HOLCF/stream2.thy --- 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