src/HOLCF/Cfun1.ML
changeset 2640 ee4dfce170a0
parent 2033 639de962ded4
child 2838 2e908f29bc3d
     1.1 --- a/src/HOLCF/Cfun1.ML	Sat Feb 15 18:24:05 1997 +0100
     1.2 +++ b/src/HOLCF/Cfun1.ML	Mon Feb 17 10:57:11 1997 +0100
     1.3 @@ -1,37 +1,48 @@
     1.4 -(*  Title:      HOLCF/cfun1.ML
     1.5 +(*  Title:      HOLCF/Cfun1.ML
     1.6      ID:         $Id$
     1.7      Author:     Franz Regensburger
     1.8      Copyright   1993 Technische Universitaet Muenchen
     1.9  
    1.10 -Lemmas for cfun1.thy 
    1.11 +Lemmas for Cfun1.thy 
    1.12  *)
    1.13  
    1.14  open Cfun1;
    1.15  
    1.16  (* ------------------------------------------------------------------------ *)
    1.17 -(* A non-emptyness result for Cfun                                          *)
    1.18 +(* derive old type definition rules for fabs & fapp                         *)
    1.19 +(* fapp and fabs should be replaced by Rep_Cfun anf Abs_Cfun in future      *)
    1.20  (* ------------------------------------------------------------------------ *)
    1.21 -
    1.22 -qed_goalw "CfunI" Cfun1.thy [Cfun_def] "(% x.x):Cfun"
    1.23 - (fn prems =>
    1.24 +qed_goalw "Rep_Cfun" thy [fapp_def] "fapp fo : CFun"
    1.25 +(fn prems =>
    1.26          [
    1.27 -        (stac mem_Collect_eq 1),
    1.28 -        (rtac cont_id 1)
    1.29 +        (rtac Rep_CFun 1)
    1.30          ]);
    1.31  
    1.32 +qed_goalw "Rep_Cfun_inverse" thy [fapp_def,fabs_def] "fabs (fapp fo) = fo"
    1.33 +(fn prems =>
    1.34 +        [
    1.35 +        (rtac Rep_CFun_inverse 1)
    1.36 +        ]);
    1.37 +
    1.38 +qed_goalw "Abs_Cfun_inverse" thy [fapp_def,fabs_def] "f:CFun==>fapp(fabs f)=f"
    1.39 +(fn prems =>
    1.40 +        [
    1.41 +	(cut_facts_tac prems 1),
    1.42 +        (etac Abs_CFun_inverse 1)
    1.43 +        ]);
    1.44  
    1.45  (* ------------------------------------------------------------------------ *)
    1.46  (* less_cfun is a partial order on type 'a -> 'b                            *)
    1.47  (* ------------------------------------------------------------------------ *)
    1.48  
    1.49 -qed_goalw "refl_less_cfun" Cfun1.thy [less_cfun_def] "less_cfun f f"
    1.50 +qed_goalw "refl_less_cfun" thy [less_cfun_def] "less(f::'a::pcpo->'b::pcpo) f"
    1.51  (fn prems =>
    1.52          [
    1.53          (rtac refl_less 1)
    1.54          ]);
    1.55  
    1.56 -qed_goalw "antisym_less_cfun" Cfun1.thy [less_cfun_def] 
    1.57 -        "[|less_cfun f1 f2; less_cfun f2 f1|] ==> f1 = f2"
    1.58 +qed_goalw "antisym_less_cfun" thy [less_cfun_def] 
    1.59 +        "[|less (f1::'a::pcpo->'b::pcpo) f2; less f2 f1|] ==> f1 = f2"
    1.60  (fn prems =>
    1.61          [
    1.62          (cut_facts_tac prems 1),
    1.63 @@ -43,8 +54,8 @@
    1.64          (rtac Rep_Cfun_inverse 1)
    1.65          ]);
    1.66  
    1.67 -qed_goalw "trans_less_cfun" Cfun1.thy [less_cfun_def] 
    1.68 -        "[|less_cfun f1 f2; less_cfun f2 f3|] ==> less_cfun f1 f3"
    1.69 +qed_goalw "trans_less_cfun" thy [less_cfun_def] 
    1.70 +        "[|less (f1::'a::pcpo->'b::pcpo) f2; less f2 f3|] ==> less f1 f3"
    1.71  (fn prems =>
    1.72          [
    1.73          (cut_facts_tac prems 1),
    1.74 @@ -56,7 +67,7 @@
    1.75  (* lemmas about application of continuous functions                         *)
    1.76  (* ------------------------------------------------------------------------ *)
    1.77  
    1.78 -qed_goal "cfun_cong" Cfun1.thy 
    1.79 +qed_goal "cfun_cong" thy 
    1.80           "[| f=g; x=y |] ==> f`x = g`y"
    1.81  (fn prems =>
    1.82          [
    1.83 @@ -64,7 +75,7 @@
    1.84          (fast_tac HOL_cs 1)
    1.85          ]);
    1.86  
    1.87 -qed_goal "cfun_fun_cong" Cfun1.thy "f=g ==> f`x = g`x"
    1.88 +qed_goal "cfun_fun_cong" thy "f=g ==> f`x = g`x"
    1.89  (fn prems =>
    1.90          [
    1.91          (cut_facts_tac prems 1),
    1.92 @@ -72,7 +83,7 @@
    1.93          (rtac refl 1)
    1.94          ]);
    1.95  
    1.96 -qed_goal "cfun_arg_cong" Cfun1.thy "x=y ==> f`x = f`y"
    1.97 +qed_goal "cfun_arg_cong" thy "x=y ==> f`x = f`y"
    1.98  (fn prems =>
    1.99          [
   1.100          (cut_facts_tac prems 1),
   1.101 @@ -86,12 +97,12 @@
   1.102  (* additional lemma about the isomorphism between -> and Cfun               *)
   1.103  (* ------------------------------------------------------------------------ *)
   1.104  
   1.105 -qed_goal "Abs_Cfun_inverse2" Cfun1.thy "cont(f) ==> fapp(fabs(f)) = f"
   1.106 +qed_goal "Abs_Cfun_inverse2" thy "cont f ==> fapp (fabs f) = f"
   1.107  (fn prems =>
   1.108          [
   1.109          (cut_facts_tac prems 1),
   1.110          (rtac Abs_Cfun_inverse 1),
   1.111 -        (rewtac Cfun_def),
   1.112 +        (rewtac CFun_def),
   1.113          (etac (mem_Collect_eq RS ssubst) 1)
   1.114          ]);
   1.115  
   1.116 @@ -99,8 +110,7 @@
   1.117  (* simplification of application                                            *)
   1.118  (* ------------------------------------------------------------------------ *)
   1.119  
   1.120 -qed_goal "Cfunapp2" Cfun1.thy 
   1.121 -        "cont(f) ==> (fabs f)`x = f x"
   1.122 +qed_goal "Cfunapp2" thy "cont f ==> (fabs f)`x = f x"
   1.123  (fn prems =>
   1.124          [
   1.125          (cut_facts_tac prems 1),
   1.126 @@ -111,7 +121,7 @@
   1.127  (* beta - equality for continuous functions                                 *)
   1.128  (* ------------------------------------------------------------------------ *)
   1.129  
   1.130 -qed_goal "beta_cfun" Cfun1.thy 
   1.131 +qed_goal "beta_cfun" thy 
   1.132          "cont(c1) ==> (LAM x .c1 x)`u = c1 u"
   1.133  (fn prems =>
   1.134          [