nipkow@243: (* Title: HOLCF/cfun2.thy nipkow@243: ID: $Id$ nipkow@243: 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: nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: (* access to less_cfun in class po *) nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: clasohm@892: qed_goal "less_cfun" Cfun2.thy "( f1 << f2 ) = (fapp(f1) << fapp(f2))" nipkow@243: (fn prems => nipkow@243: [ nipkow@243: (rtac (inst_cfun_po RS ssubst) 1), nipkow@243: (fold_goals_tac [less_cfun_def]), nipkow@243: (rtac refl 1) nipkow@243: ]); nipkow@243: nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: (* Type 'a ->'b is pointed *) nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: clasohm@892: qed_goalw "minimal_cfun" Cfun2.thy [UU_cfun_def] "UU_cfun << f" nipkow@243: (fn prems => nipkow@243: [ nipkow@243: (rtac (less_cfun RS ssubst) 1), nipkow@243: (rtac (Abs_Cfun_inverse2 RS ssubst) 1), regensbu@1168: (rtac cont_const 1), nipkow@243: (fold_goals_tac [UU_fun_def]), nipkow@243: (rtac minimal_fun 1) nipkow@243: ]); nipkow@243: nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: (* fapp yields continuous functions in 'a => 'b *) nipkow@243: (* this is continuity of fapp in its 'second' argument *) regensbu@1168: (* cont_fapp2 ==> monofun_fapp2 & contlub_fapp2 *) nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: regensbu@1168: qed_goal "cont_fapp2" Cfun2.thy "cont(fapp(fo))" nipkow@243: (fn prems => nipkow@243: [ regensbu@1168: (res_inst_tac [("P","cont")] CollectD 1), nipkow@243: (fold_goals_tac [Cfun_def]), nipkow@243: (rtac Rep_Cfun 1) nipkow@243: ]); nipkow@243: regensbu@1168: val monofun_fapp2 = cont_fapp2 RS cont2mono; nipkow@243: (* monofun(fapp(?fo1)) *) nipkow@243: nipkow@243: regensbu@1168: val contlub_fapp2 = cont_fapp2 RS cont2contlub; nipkow@243: (* contlub(fapp(?fo1)) *) nipkow@243: nipkow@243: (* ------------------------------------------------------------------------ *) regensbu@1168: (* expanded thms cont_fapp2, contlub_fapp2 *) regensbu@1168: (* looks nice with mixfix syntac *) nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: regensbu@1168: val cont_cfun_arg = (cont_fapp2 RS contE RS spec RS mp); regensbu@1168: (* is_chain(?x1) ==> range (%i. ?fo3`(?x1 i)) <<| ?fo3`(lub (range ?x1)) *) nipkow@243: nipkow@243: val contlub_cfun_arg = (contlub_fapp2 RS contlubE RS spec RS mp); regensbu@1168: (* is_chain(?x1) ==> ?fo4`(lub (range ?x1)) = lub (range (%i. ?fo4`(?x1 i))) *) nipkow@243: nipkow@243: nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: (* fapp is monotone in its 'first' argument *) nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: clasohm@892: qed_goalw "monofun_fapp1" Cfun2.thy [monofun] "monofun(fapp)" nipkow@243: (fn prems => nipkow@243: [ nipkow@243: (strip_tac 1), nipkow@243: (etac (less_cfun RS subst) 1) nipkow@243: ]); nipkow@243: nipkow@243: nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: (* monotonicity of application fapp in mixfix syntax [_]_ *) nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: regensbu@1168: qed_goal "monofun_cfun_fun" Cfun2.thy "f1 << f2 ==> f1`x << f2`x" nipkow@243: (fn prems => nipkow@243: [ nipkow@243: (cut_facts_tac prems 1), nipkow@243: (res_inst_tac [("x","x")] spec 1), nipkow@243: (rtac (less_fun RS subst) 1), nipkow@243: (etac (monofun_fapp1 RS monofunE RS spec RS spec RS mp) 1) nipkow@243: ]); nipkow@243: nipkow@243: nipkow@243: val monofun_cfun_arg = (monofun_fapp2 RS monofunE RS spec RS spec RS mp); regensbu@1168: (* ?x2 << ?x1 ==> ?fo5`?x2 << ?fo5`?x1 *) nipkow@243: nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: (* monotonicity of fapp in both arguments in mixfix syntax [_]_ *) nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: clasohm@892: qed_goal "monofun_cfun" Cfun2.thy regensbu@1168: "[|f1< f1`x1 << f2`x2" nipkow@243: (fn prems => nipkow@243: [ nipkow@243: (cut_facts_tac prems 1), nipkow@243: (rtac trans_less 1), nipkow@243: (etac monofun_cfun_arg 1), nipkow@243: (etac monofun_cfun_fun 1) nipkow@243: ]); nipkow@243: nipkow@243: nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: (* ch2ch - rules for the type 'a -> 'b *) nipkow@243: (* use MF2 lemmas from Cont.ML *) nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: clasohm@892: qed_goal "ch2ch_fappR" Cfun2.thy regensbu@1168: "is_chain(Y) ==> is_chain(%i. f`(Y i))" nipkow@243: (fn prems => nipkow@243: [ nipkow@243: (cut_facts_tac prems 1), nipkow@243: (etac (monofun_fapp2 RS ch2ch_MF2R) 1) nipkow@243: ]); nipkow@243: nipkow@243: nipkow@243: val ch2ch_fappL = (monofun_fapp1 RS ch2ch_MF2L); regensbu@1168: (* is_chain(?F) ==> is_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: clasohm@892: qed_goal "lub_cfun_mono" Cfun2.thy regensbu@1168: "is_chain(F) ==> monofun(% x.lub(range(% j.(F j)`x)))" nipkow@243: (fn prems => nipkow@243: [ nipkow@243: (cut_facts_tac prems 1), nipkow@243: (rtac lub_MF2_mono 1), nipkow@243: (rtac monofun_fapp1 1), nipkow@243: (rtac (monofun_fapp2 RS allI) 1), nipkow@243: (atac 1) nipkow@243: ]); 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: clasohm@892: qed_goal "ex_lubcfun" Cfun2.thy nipkow@243: "[| is_chain(F); is_chain(Y) |] ==>\ regensbu@1168: \ lub(range(%j. lub(range(%i. F(j)`(Y i))))) =\ regensbu@1168: \ lub(range(%i. lub(range(%j. F(j)`(Y i)))))" nipkow@243: (fn prems => nipkow@243: [ nipkow@243: (cut_facts_tac prems 1), nipkow@243: (rtac ex_lubMF2 1), nipkow@243: (rtac monofun_fapp1 1), nipkow@243: (rtac (monofun_fapp2 RS allI) 1), nipkow@243: (atac 1), nipkow@243: (atac 1) nipkow@243: ]); nipkow@243: nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: (* the lub of a chain of cont. functions is continuous *) nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: regensbu@1168: qed_goal "cont_lubcfun" Cfun2.thy regensbu@1168: "is_chain(F) ==> cont(% x.lub(range(% j.F(j)`x)))" nipkow@243: (fn prems => nipkow@243: [ nipkow@243: (cut_facts_tac prems 1), regensbu@1168: (rtac monocontlub2cont 1), nipkow@243: (etac lub_cfun_mono 1), nipkow@243: (rtac contlubI 1), nipkow@243: (strip_tac 1), nipkow@243: (rtac (contlub_cfun_arg RS ext RS ssubst) 1), nipkow@243: (atac 1), nipkow@243: (etac ex_lubcfun 1), nipkow@243: (atac 1) nipkow@243: ]); nipkow@243: nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: (* type 'a -> 'b is chain complete *) nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: clasohm@892: qed_goal "lub_cfun" Cfun2.thy regensbu@1168: "is_chain(CCF) ==> range(CCF) <<| (LAM x.lub(range(% i.CCF(i)`x)))" nipkow@243: (fn prems => nipkow@243: [ nipkow@243: (cut_facts_tac prems 1), nipkow@243: (rtac is_lubI 1), nipkow@243: (rtac conjI 1), nipkow@243: (rtac ub_rangeI 1), nipkow@243: (rtac allI 1), nipkow@243: (rtac (less_cfun RS ssubst) 1), nipkow@243: (rtac (Abs_Cfun_inverse2 RS ssubst) 1), regensbu@1168: (etac cont_lubcfun 1), nipkow@243: (rtac (lub_fun RS is_lubE RS conjunct1 RS ub_rangeE RS spec) 1), nipkow@243: (etac (monofun_fapp1 RS ch2ch_monofun) 1), nipkow@243: (strip_tac 1), nipkow@243: (rtac (less_cfun RS ssubst) 1), nipkow@243: (rtac (Abs_Cfun_inverse2 RS ssubst) 1), regensbu@1168: (etac cont_lubcfun 1), nipkow@243: (rtac (lub_fun RS is_lubE RS conjunct2 RS spec RS mp) 1), nipkow@243: (etac (monofun_fapp1 RS ch2ch_monofun) 1), nipkow@243: (etac (monofun_fapp1 RS ub2ub_monofun) 1) nipkow@243: ]); nipkow@243: nipkow@243: val thelub_cfun = (lub_cfun RS thelubI); nipkow@243: (* regensbu@1168: is_chain(?CCF1) ==> lub (range ?CCF1) = (LAM x. lub (range (%i. ?CCF1 i`x))) nipkow@243: *) nipkow@243: clasohm@892: qed_goal "cpo_cfun" Cfun2.thy nipkow@243: "is_chain(CCF::nat=>('a::pcpo->'b::pcpo)) ==> ? x. range(CCF) <<| x" nipkow@243: (fn prems => nipkow@243: [ nipkow@243: (cut_facts_tac prems 1), nipkow@243: (rtac exI 1), nipkow@243: (etac lub_cfun 1) nipkow@243: ]); 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 => nipkow@243: [ nipkow@243: (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1), nipkow@243: (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1), nipkow@243: (res_inst_tac [("f","fabs")] arg_cong 1), nipkow@243: (rtac ext 1), nipkow@243: (resolve_tac prems 1) nipkow@243: ]); nipkow@243: nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: (* Monotonicity of fabs *) nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: clasohm@892: qed_goal "semi_monofun_fabs" Cfun2.thy regensbu@1168: "[|cont(f);cont(g);f<fabs(f)< nipkow@243: [ nipkow@243: (rtac (less_cfun RS iffD2) 1), nipkow@243: (rtac (Abs_Cfun_inverse2 RS ssubst) 1), nipkow@243: (resolve_tac prems 1), nipkow@243: (rtac (Abs_Cfun_inverse2 RS ssubst) 1), nipkow@243: (resolve_tac prems 1), nipkow@243: (resolve_tac prems 1) nipkow@243: ]); nipkow@243: nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: (* Extenionality wrt. << in 'a -> 'b *) nipkow@243: (* ------------------------------------------------------------------------ *) nipkow@243: regensbu@1168: qed_goal "less_cfun2" Cfun2.thy "(!!x. f`x << g`x) ==> f << g" nipkow@243: (fn prems => nipkow@243: [ nipkow@243: (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1), nipkow@243: (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1), nipkow@243: (rtac semi_monofun_fabs 1), regensbu@1168: (rtac cont_fapp2 1), regensbu@1168: (rtac cont_fapp2 1), nipkow@243: (rtac (less_fun RS iffD2) 1), nipkow@243: (rtac allI 1), nipkow@243: (resolve_tac prems 1) nipkow@243: ]); nipkow@243: nipkow@243: