src/HOLCF/Cfun2.ML
changeset 2640 ee4dfce170a0
parent 2033 639de962ded4
child 2838 2e908f29bc3d
     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),