src/HOLCF/Cfun2.ML
changeset 243 c22b85994e17
child 297 5ef75ff3baeb
--- /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)
+	]);
+
+