1.1 --- a/src/HOLCF/Cfun2.ML Sat Feb 15 18:24:05 1997 +0100
1.2 +++ b/src/HOLCF/Cfun2.ML Mon Feb 17 10:57:11 1997 +0100
1.3 @@ -8,43 +8,57 @@
1.4
1.5 open Cfun2;
1.6
1.7 +(* for compatibility with old HOLCF-Version *)
1.8 +qed_goal "inst_cfun_po" thy "(op <<)=(%f1 f2.fapp f1 << fapp f2)"
1.9 + (fn prems =>
1.10 + [
1.11 + (fold_goals_tac [po_def,less_cfun_def]),
1.12 + (rtac refl 1)
1.13 + ]);
1.14 +
1.15 (* ------------------------------------------------------------------------ *)
1.16 (* access to less_cfun in class po *)
1.17 (* ------------------------------------------------------------------------ *)
1.18
1.19 -qed_goal "less_cfun" Cfun2.thy "( f1 << f2 ) = (fapp(f1) << fapp(f2))"
1.20 +qed_goal "less_cfun" thy "( f1 << f2 ) = (fapp(f1) << fapp(f2))"
1.21 (fn prems =>
1.22 [
1.23 - (stac inst_cfun_po 1),
1.24 - (fold_goals_tac [less_cfun_def]),
1.25 - (rtac refl 1)
1.26 + (simp_tac (!simpset addsimps [inst_cfun_po]) 1)
1.27 ]);
1.28
1.29 (* ------------------------------------------------------------------------ *)
1.30 (* Type 'a ->'b is pointed *)
1.31 (* ------------------------------------------------------------------------ *)
1.32
1.33 -qed_goalw "minimal_cfun" Cfun2.thy [UU_cfun_def] "UU_cfun << f"
1.34 +qed_goal "minimal_cfun" thy "fabs(% x.UU) << f"
1.35 (fn prems =>
1.36 [
1.37 (stac less_cfun 1),
1.38 (stac Abs_Cfun_inverse2 1),
1.39 (rtac cont_const 1),
1.40 - (fold_goals_tac [UU_fun_def]),
1.41 (rtac minimal_fun 1)
1.42 ]);
1.43
1.44 +bind_thm ("UU_cfun_def",minimal_cfun RS minimal2UU RS sym);
1.45 +
1.46 +qed_goal "least_cfun" thy "? x::'a->'b.!y.x<<y"
1.47 +(fn prems =>
1.48 + [
1.49 + (res_inst_tac [("x","fabs(% x.UU)")] exI 1),
1.50 + (rtac (minimal_cfun RS allI) 1)
1.51 + ]);
1.52 +
1.53 (* ------------------------------------------------------------------------ *)
1.54 (* fapp yields continuous functions in 'a => 'b *)
1.55 (* this is continuity of fapp in its 'second' argument *)
1.56 (* cont_fapp2 ==> monofun_fapp2 & contlub_fapp2 *)
1.57 (* ------------------------------------------------------------------------ *)
1.58
1.59 -qed_goal "cont_fapp2" Cfun2.thy "cont(fapp(fo))"
1.60 +qed_goal "cont_fapp2" thy "cont(fapp(fo))"
1.61 (fn prems =>
1.62 [
1.63 (res_inst_tac [("P","cont")] CollectD 1),
1.64 - (fold_goals_tac [Cfun_def]),
1.65 + (fold_goals_tac [CFun_def]),
1.66 (rtac Rep_Cfun 1)
1.67 ]);
1.68
1.69 @@ -71,7 +85,7 @@
1.70 (* fapp is monotone in its 'first' argument *)
1.71 (* ------------------------------------------------------------------------ *)
1.72
1.73 -qed_goalw "monofun_fapp1" Cfun2.thy [monofun] "monofun(fapp)"
1.74 +qed_goalw "monofun_fapp1" thy [monofun] "monofun(fapp)"
1.75 (fn prems =>
1.76 [
1.77 (strip_tac 1),
1.78 @@ -83,7 +97,7 @@
1.79 (* monotonicity of application fapp in mixfix syntax [_]_ *)
1.80 (* ------------------------------------------------------------------------ *)
1.81
1.82 -qed_goal "monofun_cfun_fun" Cfun2.thy "f1 << f2 ==> f1`x << f2`x"
1.83 +qed_goal "monofun_cfun_fun" thy "f1 << f2 ==> f1`x << f2`x"
1.84 (fn prems =>
1.85 [
1.86 (cut_facts_tac prems 1),
1.87 @@ -100,7 +114,7 @@
1.88 (* monotonicity of fapp in both arguments in mixfix syntax [_]_ *)
1.89 (* ------------------------------------------------------------------------ *)
1.90
1.91 -qed_goal "monofun_cfun" Cfun2.thy
1.92 +qed_goal "monofun_cfun" thy
1.93 "[|f1<<f2;x1<<x2|] ==> f1`x1 << f2`x2"
1.94 (fn prems =>
1.95 [
1.96 @@ -111,7 +125,7 @@
1.97 ]);
1.98
1.99
1.100 -qed_goal "strictI" Cfun2.thy "f`x = UU ==> f`UU = UU" (fn prems => [
1.101 +qed_goal "strictI" thy "f`x = UU ==> f`UU = UU" (fn prems => [
1.102 cut_facts_tac prems 1,
1.103 rtac (eq_UU_iff RS iffD2) 1,
1.104 etac subst 1,
1.105 @@ -123,7 +137,7 @@
1.106 (* use MF2 lemmas from Cont.ML *)
1.107 (* ------------------------------------------------------------------------ *)
1.108
1.109 -qed_goal "ch2ch_fappR" Cfun2.thy
1.110 +qed_goal "ch2ch_fappR" thy
1.111 "is_chain(Y) ==> is_chain(%i. f`(Y i))"
1.112 (fn prems =>
1.113 [
1.114 @@ -141,7 +155,7 @@
1.115 (* use MF2 lemmas from Cont.ML *)
1.116 (* ------------------------------------------------------------------------ *)
1.117
1.118 -qed_goal "lub_cfun_mono" Cfun2.thy
1.119 +qed_goal "lub_cfun_mono" thy
1.120 "is_chain(F) ==> monofun(% x.lub(range(% j.(F j)`x)))"
1.121 (fn prems =>
1.122 [
1.123 @@ -157,7 +171,7 @@
1.124 (* use MF2 lemmas from Cont.ML *)
1.125 (* ------------------------------------------------------------------------ *)
1.126
1.127 -qed_goal "ex_lubcfun" Cfun2.thy
1.128 +qed_goal "ex_lubcfun" thy
1.129 "[| is_chain(F); is_chain(Y) |] ==>\
1.130 \ lub(range(%j. lub(range(%i. F(j)`(Y i))))) =\
1.131 \ lub(range(%i. lub(range(%j. F(j)`(Y i)))))"
1.132 @@ -175,7 +189,7 @@
1.133 (* the lub of a chain of cont. functions is continuous *)
1.134 (* ------------------------------------------------------------------------ *)
1.135
1.136 -qed_goal "cont_lubcfun" Cfun2.thy
1.137 +qed_goal "cont_lubcfun" thy
1.138 "is_chain(F) ==> cont(% x.lub(range(% j.F(j)`x)))"
1.139 (fn prems =>
1.140 [
1.141 @@ -194,7 +208,7 @@
1.142 (* type 'a -> 'b is chain complete *)
1.143 (* ------------------------------------------------------------------------ *)
1.144
1.145 -qed_goal "lub_cfun" Cfun2.thy
1.146 +qed_goal "lub_cfun" thy
1.147 "is_chain(CCF) ==> range(CCF) <<| (LAM x.lub(range(% i.CCF(i)`x)))"
1.148 (fn prems =>
1.149 [
1.150 @@ -222,7 +236,7 @@
1.151 is_chain(?CCF1) ==> lub (range ?CCF1) = (LAM x. lub (range (%i. ?CCF1 i`x)))
1.152 *)
1.153
1.154 -qed_goal "cpo_cfun" Cfun2.thy
1.155 +qed_goal "cpo_cfun" thy
1.156 "is_chain(CCF::nat=>('a::pcpo->'b::pcpo)) ==> ? x. range(CCF) <<| x"
1.157 (fn prems =>
1.158 [
1.159 @@ -250,7 +264,7 @@
1.160 (* Monotonicity of fabs *)
1.161 (* ------------------------------------------------------------------------ *)
1.162
1.163 -qed_goal "semi_monofun_fabs" Cfun2.thy
1.164 +qed_goal "semi_monofun_fabs" thy
1.165 "[|cont(f);cont(g);f<<g|]==>fabs(f)<<fabs(g)"
1.166 (fn prems =>
1.167 [
1.168 @@ -266,7 +280,7 @@
1.169 (* Extenionality wrt. << in 'a -> 'b *)
1.170 (* ------------------------------------------------------------------------ *)
1.171
1.172 -qed_goal "less_cfun2" Cfun2.thy "(!!x. f`x << g`x) ==> f << g"
1.173 +qed_goal "less_cfun2" thy "(!!x. f`x << g`x) ==> f << g"
1.174 (fn prems =>
1.175 [
1.176 (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),