# HG changeset patch # User sandnerr # Date 850155071 -3600 # Node ID b4a1e3306aa0b253a50ad4c0215eda959bd7012f # Parent 7405e3cac88ae04c2cab12c82d9aafed5f874ba6 added theorems diff -r 7405e3cac88a -r b4a1e3306aa0 src/HOLCF/Cont.ML --- a/src/HOLCF/Cont.ML Mon Dec 09 19:07:26 1996 +0100 +++ b/src/HOLCF/Cont.ML Mon Dec 09 19:11:11 1996 +0100 @@ -167,6 +167,28 @@ ]); (* ------------------------------------------------------------------------ *) +(* monotone functions map finite chains to finite chains *) +(* ------------------------------------------------------------------------ *) + +qed_goalw "monofun_finch2finch" Cont.thy [finite_chain_def] + "[| monofun f; finite_chain Y |] ==> finite_chain (%n. f (Y n))" +(fn prems => + [ + cut_facts_tac prems 1, + safe_tac HOL_cs, + fast_tac (HOL_cs addSEs [ch2ch_monofun]) 1, + fast_tac (HOL_cs addss (HOL_ss addsimps [max_in_chain_def])) 1 + ]); + +(* ------------------------------------------------------------------------ *) +(* The same holds for continuous functions *) +(* ------------------------------------------------------------------------ *) + +bind_thm ("cont_finch2finch", cont2mono RS monofun_finch2finch); +(* [| cont ?f; finite_chain ?Y |] ==> finite_chain (%n. ?f (?Y n)) *) + + +(* ------------------------------------------------------------------------ *) (* The following results are about a curried function that is monotone *) (* in both arguments *) (* ------------------------------------------------------------------------ *) diff -r 7405e3cac88a -r b4a1e3306aa0 src/HOLCF/Fix.ML --- a/src/HOLCF/Fix.ML Mon Dec 09 19:07:26 1996 +0100 +++ b/src/HOLCF/Fix.ML Mon Dec 09 19:11:11 1996 +0100 @@ -230,7 +230,6 @@ (etac (monofun_iterate RS monofunE RS spec RS spec RS mp) 1) ]); - (* ------------------------------------------------------------------------ *) (* since iterate is not monotone in its first argument, special lemmas must *) (* be derived for lubs in this argument *) @@ -589,6 +588,19 @@ bind_thm ("adm_flat", flat_imp_chain_finite RS adm_chain_finite); (* flat(?x::?'a) ==> adm(?P::?'a => bool) *) +(* ------------------------------------------------------------------------ *) +(* some properties of flat *) +(* ------------------------------------------------------------------------ *) + +qed_goalw "flatdom2monofun" Fix.thy [flat_def] + "[| flat(x::'a::pcpo); f UU = UU |] ==> monofun (f::'a=>'b::pcpo)" +(fn prems => + [ + cut_facts_tac prems 1, + fast_tac ((HOL_cs addss !simpset) addSIs [monofunI]) 1 + ]); + + qed_goalw "flat_void" Fix.thy [flat_def] "flat(UU::void)" (fn prems => [ @@ -602,6 +614,78 @@ (cut_facts_tac prems 1), (fast_tac (HOL_cs addIs [refl_less]) 1)]); + +(* ------------------------------------------------------------------------ *) +(* some lemmata for functions with flat/chain_finite domain/range types *) +(* ------------------------------------------------------------------------ *) + +qed_goal "chfin2finch" Fix.thy + "[| is_chain (Y::nat=>'a); chain_finite (x::'a) |] ==> finite_chain Y" +(fn prems => + [ + cut_facts_tac prems 1, + fast_tac (HOL_cs addss + (!simpset addsimps [chain_finite_def,finite_chain_def])) 1 + ]); + +qed_goal "chfindom_monofun2cont" Fix.thy + "[| chain_finite(x::'a::pcpo); monofun f |] ==> cont (f::'a=>'b::pcpo)" +(fn prems => + [ + cut_facts_tac prems 1, + rtac monocontlub2cont 1, + atac 1, + rtac contlubI 1, + strip_tac 1, + dtac (chfin2finch COMP swap_prems_rl) 1, + atac 1, + rtac antisym_less 1, + fast_tac ((HOL_cs addIs [is_ub_thelub,ch2ch_monofun]) + addss (HOL_ss addsimps [finite_chain_def,maxinch_is_thelub])) 1, + dtac (monofun_finch2finch COMP swap_prems_rl) 1, + atac 1, + fast_tac ((HOL_cs + addIs [is_ub_thelub,(monofunE RS spec RS spec RS mp)]) + addss (HOL_ss addsimps [finite_chain_def,maxinch_is_thelub])) 1 + ]); + +bind_thm("flatdom_monofun2cont",flat_imp_chain_finite RS chfindom_monofun2cont); +(* [| flat ?x; monofun ?f |] ==> cont ?f *) + +qed_goal "flatdom_strict2cont" Fix.thy + "[| flat(x::'a::pcpo); f UU = UU |] ==> cont (f::'a=>'b::pcpo)" +(fn prems => + [ + cut_facts_tac prems 1, + fast_tac ((HOL_cs addSIs [flatdom2monofun, + flat_imp_chain_finite RS chfindom_monofun2cont])) 1 + ]); + +qed_goal "chfin_fappR" Fix.thy + "[| is_chain (Y::nat => 'a->'b); chain_finite(x::'b) |] ==> \ +\ !s. ? n. lub(range(Y))`s = Y n`s" +(fn prems => + [ + cut_facts_tac prems 1, + rtac allI 1, + rtac (contlub_cfun_fun RS ssubst) 1, + atac 1, + fast_tac (HOL_cs addSIs [thelubI,lub_finch2,chfin2finch,ch2ch_fappL])1 + ]); + +qed_goalw "adm_chfindom" Fix.thy [adm_def] + "chain_finite (x::'b) ==> adm (%(u::'a->'b). P(u`s))" (fn prems => [ + cut_facts_tac prems 1, + strip_tac 1, + dtac chfin_fappR 1, + atac 1, + eres_inst_tac [("x","s")] allE 1, + fast_tac (HOL_cs addss !simpset) 1]); + +bind_thm("adm_flatdom",flat_imp_chain_finite RS adm_chfindom); +(* flat ?x ==> adm (%u. ?P (u`?s)) *) + + (* ------------------------------------------------------------------------ *) (* lemmata for improved admissibility introdution rule *) (* ------------------------------------------------------------------------ *) diff -r 7405e3cac88a -r b4a1e3306aa0 src/HOLCF/Pcpo.ML --- a/src/HOLCF/Pcpo.ML Mon Dec 09 19:07:26 1996 +0100 +++ b/src/HOLCF/Pcpo.ML Mon Dec 09 19:11:11 1996 +0100 @@ -33,6 +33,20 @@ bind_thm ("is_lub_thelub", cpo RS lubI RS is_lub_lub); (* [| is_chain(?S5); range(?S5) <| ?x1 |] ==> lub(range(?S5)) << ?x1 *) +qed_goal "maxinch_is_thelub" Pcpo.thy "is_chain Y ==> \ +\ max_in_chain i Y = (lub(range(Y)) = ((Y i)::'a::pcpo))" +(fn prems => + [ + cut_facts_tac prems 1, + rtac iffI 1, + fast_tac (HOL_cs addSIs [thelubI,lub_finch1]) 1, + rewtac max_in_chain_def, + safe_tac (HOL_cs addSIs [antisym_less]), + fast_tac (HOL_cs addSEs [chain_mono3]) 1, + dtac sym 1, + fast_tac ((HOL_cs addSEs [is_ub_thelub]) addss !simpset) 1 + ]); + (* ------------------------------------------------------------------------ *) (* the << relation between two chains is preserved by their lubs *)