src/HOLCF/Cfun1.ML
author slotosch
Sun May 25 11:07:52 1997 +0200 (1997-05-25)
changeset 3323 194ae2e0c193
parent 2838 2e908f29bc3d
child 5291 5706f0ef1d43
permissions -rw-r--r--
eliminated the constant less by the introduction of the axclass sq_ord
added explicit type ::'a::po in the following theorems:
minimal2UU,antisym_less_inverse,box_less,not_less2not_eq,monofun_pair
and dist_eqI (in domain-package)
added instances
instance fun :: (term,sq_ord)sq_ord
instance "->" :: (term,sq_ord)sq_ord
instance "**" :: (sq_ord,sq_ord)sq_ord
instance "*" :: (sq_ord,sq_ord)sq_ord
instance "++" :: (pcpo,pcpo)sq_ord
instance u :: (sq_ord)sq_ord
instance lift :: (term)sq_ord
instance discr :: (term)sq_ord
     1 (*  Title:      HOLCF/Cfun1.ML
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Lemmas for Cfun1.thy 
     7 *)
     8 
     9 open Cfun1;
    10 
    11 (* ------------------------------------------------------------------------ *)
    12 (* derive old type definition rules for fabs & fapp                         *)
    13 (* fapp and fabs should be replaced by Rep_Cfun anf Abs_Cfun in future      *)
    14 (* ------------------------------------------------------------------------ *)
    15 qed_goalw "Rep_Cfun" thy [fapp_def] "fapp fo : CFun"
    16 (fn prems =>
    17         [
    18         (rtac Rep_CFun 1)
    19         ]);
    20 
    21 qed_goalw "Rep_Cfun_inverse" thy [fapp_def,fabs_def] "fabs (fapp fo) = fo"
    22 (fn prems =>
    23         [
    24         (rtac Rep_CFun_inverse 1)
    25         ]);
    26 
    27 qed_goalw "Abs_Cfun_inverse" thy [fapp_def,fabs_def] "f:CFun==>fapp(fabs f)=f"
    28 (fn prems =>
    29         [
    30 	(cut_facts_tac prems 1),
    31         (etac Abs_CFun_inverse 1)
    32         ]);
    33 
    34 (* ------------------------------------------------------------------------ *)
    35 (* less_cfun is a partial order on type 'a -> 'b                            *)
    36 (* ------------------------------------------------------------------------ *)
    37 
    38 qed_goalw "refl_less_cfun" thy [less_cfun_def] "(f::'a->'b) << f"
    39 (fn prems =>
    40         [
    41         (rtac refl_less 1)
    42         ]);
    43 
    44 qed_goalw "antisym_less_cfun" thy [less_cfun_def] 
    45         "[|(f1::'a->'b) << f2; f2 << f1|] ==> f1 = f2"
    46 (fn prems =>
    47         [
    48         (cut_facts_tac prems 1),
    49         (rtac injD 1),
    50         (rtac antisym_less 2),
    51         (atac 3),
    52         (atac 2),
    53         (rtac inj_inverseI 1),
    54         (rtac Rep_Cfun_inverse 1)
    55         ]);
    56 
    57 qed_goalw "trans_less_cfun" thy [less_cfun_def] 
    58         "[|(f1::'a->'b) << f2; f2 << f3|] ==> f1 << f3"
    59 (fn prems =>
    60         [
    61         (cut_facts_tac prems 1),
    62         (etac trans_less 1),
    63         (atac 1)
    64         ]);
    65 
    66 (* ------------------------------------------------------------------------ *)
    67 (* lemmas about application of continuous functions                         *)
    68 (* ------------------------------------------------------------------------ *)
    69 
    70 qed_goal "cfun_cong" thy 
    71          "[| f=g; x=y |] ==> f`x = g`y"
    72 (fn prems =>
    73         [
    74         (cut_facts_tac prems 1),
    75         (fast_tac HOL_cs 1)
    76         ]);
    77 
    78 qed_goal "cfun_fun_cong" thy "f=g ==> f`x = g`x"
    79 (fn prems =>
    80         [
    81         (cut_facts_tac prems 1),
    82         (etac cfun_cong 1),
    83         (rtac refl 1)
    84         ]);
    85 
    86 qed_goal "cfun_arg_cong" thy "x=y ==> f`x = f`y"
    87 (fn prems =>
    88         [
    89         (cut_facts_tac prems 1),
    90         (rtac cfun_cong 1),
    91         (rtac refl 1),
    92         (atac 1)
    93         ]);
    94 
    95 
    96 (* ------------------------------------------------------------------------ *)
    97 (* additional lemma about the isomorphism between -> and Cfun               *)
    98 (* ------------------------------------------------------------------------ *)
    99 
   100 qed_goal "Abs_Cfun_inverse2" thy "cont f ==> fapp (fabs f) = f"
   101 (fn prems =>
   102         [
   103         (cut_facts_tac prems 1),
   104         (rtac Abs_Cfun_inverse 1),
   105         (rewtac CFun_def),
   106         (etac (mem_Collect_eq RS ssubst) 1)
   107         ]);
   108 
   109 (* ------------------------------------------------------------------------ *)
   110 (* simplification of application                                            *)
   111 (* ------------------------------------------------------------------------ *)
   112 
   113 qed_goal "Cfunapp2" thy "cont f ==> (fabs f)`x = f x"
   114 (fn prems =>
   115         [
   116         (cut_facts_tac prems 1),
   117         (etac (Abs_Cfun_inverse2 RS fun_cong) 1)
   118         ]);
   119 
   120 (* ------------------------------------------------------------------------ *)
   121 (* beta - equality for continuous functions                                 *)
   122 (* ------------------------------------------------------------------------ *)
   123 
   124 qed_goal "beta_cfun" thy 
   125         "cont(c1) ==> (LAM x .c1 x)`u = c1 u"
   126 (fn prems =>
   127         [
   128         (cut_facts_tac prems 1),
   129         (rtac Cfunapp2 1),
   130         (atac 1)
   131         ]);