clasohm@1461: (* Title: HOLCF/cfun2.thy nipkow@243: ID: $Id$ clasohm@1461: Author: Franz Regensburger nipkow@243: Copyright 1993 Technische Universitaet Muenchen nipkow@243: nipkow@243: Lemmas for cfun2.thy nipkow@243: *) nipkow@243: nipkow@243: open Cfun2; nipkow@243: slotosch@2640: (* for compatibility with old HOLCF-Version *) slotosch@5291: qed_goal "inst_cfun_po" thy "(op <<)=(%f1 f2. Rep_CFun f1 << Rep_CFun f2)" slotosch@2640: (fn prems => slotosch@2640: [ slotosch@3323: (fold_goals_tac [less_cfun_def]), slotosch@2640: (rtac refl 1) slotosch@2640: ]); slotosch@2640: nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: (* access to less_cfun in class po *) nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: slotosch@5291: qed_goal "less_cfun" thy "( f1 << f2 ) = (Rep_CFun(f1) << Rep_CFun(f2))" nipkow@243: (fn prems => clasohm@1461: [ wenzelm@4098: (simp_tac (simpset() addsimps [inst_cfun_po]) 1) clasohm@1461: ]); nipkow@243: nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: (* Type 'a ->'b is pointed *) nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: slotosch@5291: qed_goal "minimal_cfun" thy "Abs_CFun(% x. UU) << f" nipkow@243: (fn prems => clasohm@1461: [ paulson@2033: (stac less_cfun 1), paulson@2033: (stac Abs_Cfun_inverse2 1), clasohm@1461: (rtac cont_const 1), clasohm@1461: (rtac minimal_fun 1) clasohm@1461: ]); nipkow@243: slotosch@2640: bind_thm ("UU_cfun_def",minimal_cfun RS minimal2UU RS sym); slotosch@2640: wenzelm@3842: qed_goal "least_cfun" thy "? x::'a->'b::pcpo.!y. x< slotosch@2640: [ slotosch@5291: (res_inst_tac [("x","Abs_CFun(% x. UU)")] exI 1), slotosch@2640: (rtac (minimal_cfun RS allI) 1) slotosch@2640: ]); slotosch@2640: nipkow@243: (* ------------------------------------------------------------------------ *) slotosch@5291: (* Rep_CFun yields continuous functions in 'a => 'b *) slotosch@5291: (* this is continuity of Rep_CFun in its 'second' argument *) slotosch@5291: (* cont_Rep_CFun2 ==> monofun_Rep_CFun2 & contlub_Rep_CFun2 *) nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: slotosch@5291: qed_goal "cont_Rep_CFun2" thy "cont(Rep_CFun(fo))" nipkow@243: (fn prems => clasohm@1461: [ clasohm@1461: (res_inst_tac [("P","cont")] CollectD 1), slotosch@2640: (fold_goals_tac [CFun_def]), clasohm@1461: (rtac Rep_Cfun 1) clasohm@1461: ]); nipkow@243: slotosch@5291: bind_thm ("monofun_Rep_CFun2", cont_Rep_CFun2 RS cont2mono); slotosch@5291: (* monofun(Rep_CFun(?fo1)) *) nipkow@243: nipkow@243: slotosch@5291: bind_thm ("contlub_Rep_CFun2", cont_Rep_CFun2 RS cont2contlub); slotosch@5291: (* contlub(Rep_CFun(?fo1)) *) nipkow@243: nipkow@243: (* ------------------------------------------------------------------------ *) slotosch@5291: (* expanded thms cont_Rep_CFun2, contlub_Rep_CFun2 *) regensbu@1168: (* looks nice with mixfix syntac *) nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: slotosch@5291: bind_thm ("cont_cfun_arg", (cont_Rep_CFun2 RS contE RS spec RS mp)); oheimb@4721: (* chain(?x1) ==> range (%i. ?fo3`(?x1 i)) <<| ?fo3`(lub (range ?x1)) *) nipkow@243: slotosch@5291: bind_thm ("contlub_cfun_arg", (contlub_Rep_CFun2 RS contlubE RS spec RS mp)); oheimb@4721: (* chain(?x1) ==> ?fo4`(lub (range ?x1)) = lub (range (%i. ?fo4`(?x1 i))) *) nipkow@243: nipkow@243: nipkow@243: (* ------------------------------------------------------------------------ *) slotosch@5291: (* Rep_CFun is monotone in its 'first' argument *) nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: slotosch@5291: qed_goalw "monofun_Rep_CFun1" thy [monofun] "monofun(Rep_CFun)" nipkow@243: (fn prems => clasohm@1461: [ clasohm@1461: (strip_tac 1), clasohm@1461: (etac (less_cfun RS subst) 1) clasohm@1461: ]); nipkow@243: nipkow@243: nipkow@243: (* ------------------------------------------------------------------------ *) slotosch@5291: (* monotonicity of application Rep_CFun in mixfix syntax [_]_ *) nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: slotosch@2640: qed_goal "monofun_cfun_fun" thy "f1 << f2 ==> f1`x << f2`x" nipkow@243: (fn prems => clasohm@1461: [ clasohm@1461: (cut_facts_tac prems 1), clasohm@1461: (res_inst_tac [("x","x")] spec 1), clasohm@1461: (rtac (less_fun RS subst) 1), slotosch@5291: (etac (monofun_Rep_CFun1 RS monofunE RS spec RS spec RS mp) 1) clasohm@1461: ]); nipkow@243: nipkow@243: slotosch@5291: bind_thm ("monofun_cfun_arg", monofun_Rep_CFun2 RS monofunE RS spec RS spec RS mp); regensbu@1168: (* ?x2 << ?x1 ==> ?fo5`?x2 << ?fo5`?x1 *) nipkow@243: nipkow@243: (* ------------------------------------------------------------------------ *) slotosch@5291: (* monotonicity of Rep_CFun in both arguments in mixfix syntax [_]_ *) nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: slotosch@2640: qed_goal "monofun_cfun" thy clasohm@1461: "[|f1< f1`x1 << f2`x2" nipkow@243: (fn prems => clasohm@1461: [ clasohm@1461: (cut_facts_tac prems 1), clasohm@1461: (rtac trans_less 1), clasohm@1461: (etac monofun_cfun_arg 1), clasohm@1461: (etac monofun_cfun_fun 1) clasohm@1461: ]); nipkow@243: nipkow@243: slotosch@2640: qed_goal "strictI" thy "f`x = UU ==> f`UU = UU" (fn prems => [ paulson@2033: cut_facts_tac prems 1, paulson@2033: rtac (eq_UU_iff RS iffD2) 1, paulson@2033: etac subst 1, paulson@2033: rtac (minimal RS monofun_cfun_arg) 1]); oheimb@1989: oheimb@1989: nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: (* ch2ch - rules for the type 'a -> 'b *) nipkow@243: (* use MF2 lemmas from Cont.ML *) nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: slotosch@5291: qed_goal "ch2ch_Rep_CFunR" thy oheimb@4721: "chain(Y) ==> chain(%i. f`(Y i))" nipkow@243: (fn prems => clasohm@1461: [ clasohm@1461: (cut_facts_tac prems 1), slotosch@5291: (etac (monofun_Rep_CFun2 RS ch2ch_MF2R) 1) clasohm@1461: ]); nipkow@243: nipkow@243: slotosch@5291: bind_thm ("ch2ch_Rep_CFunL", monofun_Rep_CFun1 RS ch2ch_MF2L); oheimb@4721: (* chain(?F) ==> chain (%i. ?F i`?x) *) nipkow@243: nipkow@243: nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: (* the lub of a chain of continous functions is monotone *) nipkow@243: (* use MF2 lemmas from Cont.ML *) nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: slotosch@2640: qed_goal "lub_cfun_mono" thy oheimb@4721: "chain(F) ==> monofun(% x. lub(range(% j.(F j)`x)))" nipkow@243: (fn prems => clasohm@1461: [ clasohm@1461: (cut_facts_tac prems 1), clasohm@1461: (rtac lub_MF2_mono 1), slotosch@5291: (rtac monofun_Rep_CFun1 1), slotosch@5291: (rtac (monofun_Rep_CFun2 RS allI) 1), clasohm@1461: (atac 1) clasohm@1461: ]); nipkow@243: nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: (* a lemma about the exchange of lubs for type 'a -> 'b *) nipkow@243: (* use MF2 lemmas from Cont.ML *) nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: slotosch@2640: qed_goal "ex_lubcfun" thy oheimb@4721: "[| chain(F); chain(Y) |] ==>\ clasohm@1461: \ lub(range(%j. lub(range(%i. F(j)`(Y i))))) =\ clasohm@1461: \ lub(range(%i. lub(range(%j. F(j)`(Y i)))))" nipkow@243: (fn prems => clasohm@1461: [ clasohm@1461: (cut_facts_tac prems 1), clasohm@1461: (rtac ex_lubMF2 1), slotosch@5291: (rtac monofun_Rep_CFun1 1), slotosch@5291: (rtac (monofun_Rep_CFun2 RS allI) 1), clasohm@1461: (atac 1), clasohm@1461: (atac 1) clasohm@1461: ]); nipkow@243: nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: (* the lub of a chain of cont. functions is continuous *) nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: slotosch@2640: qed_goal "cont_lubcfun" thy oheimb@4721: "chain(F) ==> cont(% x. lub(range(% j. F(j)`x)))" nipkow@243: (fn prems => clasohm@1461: [ clasohm@1461: (cut_facts_tac prems 1), clasohm@1461: (rtac monocontlub2cont 1), clasohm@1461: (etac lub_cfun_mono 1), clasohm@1461: (rtac contlubI 1), clasohm@1461: (strip_tac 1), paulson@2033: (stac (contlub_cfun_arg RS ext) 1), clasohm@1461: (atac 1), clasohm@1461: (etac ex_lubcfun 1), clasohm@1461: (atac 1) clasohm@1461: ]); nipkow@243: nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: (* type 'a -> 'b is chain complete *) nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: slotosch@2640: qed_goal "lub_cfun" thy oheimb@4721: "chain(CCF) ==> range(CCF) <<| (LAM x. lub(range(% i. CCF(i)`x)))" nipkow@243: (fn prems => clasohm@1461: [ clasohm@1461: (cut_facts_tac prems 1), clasohm@1461: (rtac is_lubI 1), clasohm@1461: (rtac conjI 1), clasohm@1461: (rtac ub_rangeI 1), clasohm@1461: (rtac allI 1), paulson@2033: (stac less_cfun 1), paulson@2033: (stac Abs_Cfun_inverse2 1), clasohm@1461: (etac cont_lubcfun 1), clasohm@1461: (rtac (lub_fun RS is_lubE RS conjunct1 RS ub_rangeE RS spec) 1), slotosch@5291: (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1), clasohm@1461: (strip_tac 1), paulson@2033: (stac less_cfun 1), paulson@2033: (stac Abs_Cfun_inverse2 1), clasohm@1461: (etac cont_lubcfun 1), clasohm@1461: (rtac (lub_fun RS is_lubE RS conjunct2 RS spec RS mp) 1), slotosch@5291: (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1), slotosch@5291: (etac (monofun_Rep_CFun1 RS ub2ub_monofun) 1) clasohm@1461: ]); nipkow@243: oheimb@1779: bind_thm ("thelub_cfun", lub_cfun RS thelubI); nipkow@243: (* oheimb@4721: chain(?CCF1) ==> lub (range ?CCF1) = (LAM x. lub (range (%i. ?CCF1 i`x))) nipkow@243: *) nipkow@243: slotosch@2640: qed_goal "cpo_cfun" thy oheimb@4721: "chain(CCF::nat=>('a->'b)) ==> ? x. range(CCF) <<| x" nipkow@243: (fn prems => clasohm@1461: [ clasohm@1461: (cut_facts_tac prems 1), clasohm@1461: (rtac exI 1), clasohm@1461: (etac lub_cfun 1) clasohm@1461: ]); nipkow@243: nipkow@243: nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: (* Extensionality in 'a -> 'b *) nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: regensbu@1168: qed_goal "ext_cfun" Cfun1.thy "(!!x. f`x = g`x) ==> f = g" nipkow@243: (fn prems => clasohm@1461: [ clasohm@1461: (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1), clasohm@1461: (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1), slotosch@5291: (res_inst_tac [("f","Abs_CFun")] arg_cong 1), clasohm@1461: (rtac ext 1), clasohm@1461: (resolve_tac prems 1) clasohm@1461: ]); nipkow@243: nipkow@243: (* ------------------------------------------------------------------------ *) slotosch@5291: (* Monotonicity of Abs_CFun *) nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: slotosch@5291: qed_goal "semi_monofun_Abs_CFun" thy slotosch@5291: "[|cont(f);cont(g);f<Abs_CFun(f)< clasohm@1461: [ clasohm@1461: (rtac (less_cfun RS iffD2) 1), paulson@2033: (stac Abs_Cfun_inverse2 1), clasohm@1461: (resolve_tac prems 1), paulson@2033: (stac Abs_Cfun_inverse2 1), clasohm@1461: (resolve_tac prems 1), clasohm@1461: (resolve_tac prems 1) clasohm@1461: ]); nipkow@243: nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: (* Extenionality wrt. << in 'a -> 'b *) nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: slotosch@2640: qed_goal "less_cfun2" thy "(!!x. f`x << g`x) ==> f << g" nipkow@243: (fn prems => clasohm@1461: [ clasohm@1461: (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1), clasohm@1461: (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1), slotosch@5291: (rtac semi_monofun_Abs_CFun 1), slotosch@5291: (rtac cont_Rep_CFun2 1), slotosch@5291: (rtac cont_Rep_CFun2 1), clasohm@1461: (rtac (less_fun RS iffD2) 1), clasohm@1461: (rtac allI 1), clasohm@1461: (resolve_tac prems 1) clasohm@1461: ]); nipkow@243: nipkow@243: