--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Cfun2.ML Wed Jan 19 17:35:01 1994 +0100
@@ -0,0 +1,276 @@
+(* Title: HOLCF/cfun2.thy
+ ID: $Id$
+ Author: Franz Regensburger
+ Copyright 1993 Technische Universitaet Muenchen
+
+Lemmas for cfun2.thy
+*)
+
+open Cfun2;
+
+(* ------------------------------------------------------------------------ *)
+(* access to less_cfun in class po *)
+(* ------------------------------------------------------------------------ *)
+
+val less_cfun = prove_goal Cfun2.thy "( f1 << f2 ) = (fapp(f1) << fapp(f2))"
+(fn prems =>
+ [
+ (rtac (inst_cfun_po RS ssubst) 1),
+ (fold_goals_tac [less_cfun_def]),
+ (rtac refl 1)
+ ]);
+
+(* ------------------------------------------------------------------------ *)
+(* Type 'a ->'b is pointed *)
+(* ------------------------------------------------------------------------ *)
+
+val minimal_cfun = prove_goalw Cfun2.thy [UU_cfun_def] "UU_cfun << f"
+(fn prems =>
+ [
+ (rtac (less_cfun RS ssubst) 1),
+ (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
+ (rtac contX_const 1),
+ (fold_goals_tac [UU_fun_def]),
+ (rtac minimal_fun 1)
+ ]);
+
+(* ------------------------------------------------------------------------ *)
+(* fapp yields continuous functions in 'a => 'b *)
+(* this is continuity of fapp in its 'second' argument *)
+(* contX_fapp2 ==> monofun_fapp2 & contlub_fapp2 *)
+(* ------------------------------------------------------------------------ *)
+
+val contX_fapp2 = prove_goal Cfun2.thy "contX(fapp(fo))"
+(fn prems =>
+ [
+ (res_inst_tac [("P","contX")] CollectD 1),
+ (fold_goals_tac [Cfun_def]),
+ (rtac Rep_Cfun 1)
+ ]);
+
+val monofun_fapp2 = contX_fapp2 RS contX2mono;
+(* monofun(fapp(?fo1)) *)
+
+
+val contlub_fapp2 = contX_fapp2 RS contX2contlub;
+(* contlub(fapp(?fo1)) *)
+
+(* ------------------------------------------------------------------------ *)
+(* expanded thms contX_fapp2, contlub_fapp2 *)
+(* looks nice with mixfix syntac _[_] *)
+(* ------------------------------------------------------------------------ *)
+
+val contX_cfun_arg = (contX_fapp2 RS contXE RS spec RS mp);
+(* is_chain(?x1) ==> range(%i. ?fo3[?x1(i)]) <<| ?fo3[lub(range(?x1))] *)
+
+val contlub_cfun_arg = (contlub_fapp2 RS contlubE RS spec RS mp);
+(* is_chain(?x1) ==> ?fo4[lub(range(?x1))] = lub(range(%i. ?fo4[?x1(i)])) *)
+
+
+
+(* ------------------------------------------------------------------------ *)
+(* fapp is monotone in its 'first' argument *)
+(* ------------------------------------------------------------------------ *)
+
+val monofun_fapp1 = prove_goalw Cfun2.thy [monofun] "monofun(fapp)"
+(fn prems =>
+ [
+ (strip_tac 1),
+ (etac (less_cfun RS subst) 1)
+ ]);
+
+
+(* ------------------------------------------------------------------------ *)
+(* monotonicity of application fapp in mixfix syntax [_]_ *)
+(* ------------------------------------------------------------------------ *)
+
+val monofun_cfun_fun = prove_goal Cfun2.thy "f1 << f2 ==> f1[x] << f2[x]"
+(fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (res_inst_tac [("x","x")] spec 1),
+ (rtac (less_fun RS subst) 1),
+ (etac (monofun_fapp1 RS monofunE RS spec RS spec RS mp) 1)
+ ]);
+
+
+val monofun_cfun_arg = (monofun_fapp2 RS monofunE RS spec RS spec RS mp);
+(* ?x2 << ?x1 ==> ?fo5[?x2] << ?fo5[?x1] *)
+
+(* ------------------------------------------------------------------------ *)
+(* monotonicity of fapp in both arguments in mixfix syntax [_]_ *)
+(* ------------------------------------------------------------------------ *)
+
+val monofun_cfun = prove_goal Cfun2.thy
+ "[|f1<<f2;x1<<x2|] ==> f1[x1] << f2[x2]"
+(fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (rtac trans_less 1),
+ (etac monofun_cfun_arg 1),
+ (etac monofun_cfun_fun 1)
+ ]);
+
+
+(* ------------------------------------------------------------------------ *)
+(* ch2ch - rules for the type 'a -> 'b *)
+(* use MF2 lemmas from Cont.ML *)
+(* ------------------------------------------------------------------------ *)
+
+val ch2ch_fappR = prove_goal Cfun2.thy
+ "is_chain(Y) ==> is_chain(%i. f[Y(i)])"
+(fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (etac (monofun_fapp2 RS ch2ch_MF2R) 1)
+ ]);
+
+
+val ch2ch_fappL = (monofun_fapp1 RS ch2ch_MF2L);
+(* is_chain(?F) ==> is_chain(%i. ?F(i)[?x]) *)
+
+
+(* ------------------------------------------------------------------------ *)
+(* the lub of a chain of continous functions is monotone *)
+(* use MF2 lemmas from Cont.ML *)
+(* ------------------------------------------------------------------------ *)
+
+val lub_cfun_mono = prove_goal Cfun2.thy
+ "is_chain(F) ==> monofun(% x.lub(range(% j.F(j)[x])))"
+(fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (rtac lub_MF2_mono 1),
+ (rtac monofun_fapp1 1),
+ (rtac (monofun_fapp2 RS allI) 1),
+ (atac 1)
+ ]);
+
+(* ------------------------------------------------------------------------ *)
+(* a lemma about the exchange of lubs for type 'a -> 'b *)
+(* use MF2 lemmas from Cont.ML *)
+(* ------------------------------------------------------------------------ *)
+
+val ex_lubcfun = prove_goal Cfun2.thy
+ "[| is_chain(F); is_chain(Y) |] ==>\
+\ lub(range(%j. lub(range(%i. F(j)[Y(i)])))) =\
+\ lub(range(%i. lub(range(%j. F(j)[Y(i)]))))"
+(fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (rtac ex_lubMF2 1),
+ (rtac monofun_fapp1 1),
+ (rtac (monofun_fapp2 RS allI) 1),
+ (atac 1),
+ (atac 1)
+ ]);
+
+(* ------------------------------------------------------------------------ *)
+(* the lub of a chain of cont. functions is continuous *)
+(* ------------------------------------------------------------------------ *)
+
+val contX_lubcfun = prove_goal Cfun2.thy
+ "is_chain(F) ==> contX(% x.lub(range(% j.F(j)[x])))"
+(fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (rtac monocontlub2contX 1),
+ (etac lub_cfun_mono 1),
+ (rtac contlubI 1),
+ (strip_tac 1),
+ (rtac (contlub_cfun_arg RS ext RS ssubst) 1),
+ (atac 1),
+ (etac ex_lubcfun 1),
+ (atac 1)
+ ]);
+
+(* ------------------------------------------------------------------------ *)
+(* type 'a -> 'b is chain complete *)
+(* ------------------------------------------------------------------------ *)
+
+val lub_cfun = prove_goal Cfun2.thy
+ "is_chain(CCF) ==> range(CCF) <<| fabs(% x.lub(range(% i.CCF(i)[x])))"
+(fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (rtac is_lubI 1),
+ (rtac conjI 1),
+ (rtac ub_rangeI 1),
+ (rtac allI 1),
+ (rtac (less_cfun RS ssubst) 1),
+ (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
+ (etac contX_lubcfun 1),
+ (rtac (lub_fun RS is_lubE RS conjunct1 RS ub_rangeE RS spec) 1),
+ (etac (monofun_fapp1 RS ch2ch_monofun) 1),
+ (strip_tac 1),
+ (rtac (less_cfun RS ssubst) 1),
+ (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
+ (etac contX_lubcfun 1),
+ (rtac (lub_fun RS is_lubE RS conjunct2 RS spec RS mp) 1),
+ (etac (monofun_fapp1 RS ch2ch_monofun) 1),
+ (etac (monofun_fapp1 RS ub2ub_monofun) 1)
+ ]);
+
+val thelub_cfun = (lub_cfun RS thelubI);
+(*
+is_chain(?CCF1) ==> lub(range(?CCF1)) = fabs(%x. lub(range(%i. ?CCF1(i)[x])))
+*)
+
+val cpo_fun = prove_goal Cfun2.thy
+ "is_chain(CCF::nat=>('a::pcpo->'b::pcpo)) ==> ? x. range(CCF) <<| x"
+(fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (rtac exI 1),
+ (etac lub_cfun 1)
+ ]);
+
+
+(* ------------------------------------------------------------------------ *)
+(* Extensionality in 'a -> 'b *)
+(* ------------------------------------------------------------------------ *)
+
+val ext_cfun = prove_goal Cfun1.thy "(!!x. f[x] = g[x]) ==> f = g"
+ (fn prems =>
+ [
+ (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),
+ (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1),
+ (res_inst_tac [("f","fabs")] arg_cong 1),
+ (rtac ext 1),
+ (resolve_tac prems 1)
+ ]);
+
+(* ------------------------------------------------------------------------ *)
+(* Monotonicity of fabs *)
+(* ------------------------------------------------------------------------ *)
+
+val semi_monofun_fabs = prove_goal Cfun2.thy
+ "[|contX(f);contX(g);f<<g|]==>fabs(f)<<fabs(g)"
+ (fn prems =>
+ [
+ (rtac (less_cfun RS iffD2) 1),
+ (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
+ (resolve_tac prems 1),
+ (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
+ (resolve_tac prems 1),
+ (resolve_tac prems 1)
+ ]);
+
+(* ------------------------------------------------------------------------ *)
+(* Extenionality wrt. << in 'a -> 'b *)
+(* ------------------------------------------------------------------------ *)
+
+val less_cfun2 = prove_goal Cfun2.thy "(!!x. f[x] << g[x]) ==> f << g"
+ (fn prems =>
+ [
+ (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),
+ (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1),
+ (rtac semi_monofun_fabs 1),
+ (rtac contX_fapp2 1),
+ (rtac contX_fapp2 1),
+ (rtac (less_fun RS iffD2) 1),
+ (rtac allI 1),
+ (resolve_tac prems 1)
+ ]);
+
+