src/HOLCF/Cfun1.ML
author clasohm
Tue Jan 30 13:42:57 1996 +0100 (1996-01-30)
changeset 1461 6bcb44e4d6e5
parent 1168 74be52691d62
child 2033 639de962ded4
permissions -rw-r--r--
expanded tabs
     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 (* A non-emptyness result for Cfun                                          *)
    13 (* ------------------------------------------------------------------------ *)
    14 
    15 qed_goalw "CfunI" Cfun1.thy [Cfun_def] "(% x.x):Cfun"
    16  (fn prems =>
    17         [
    18         (rtac (mem_Collect_eq RS ssubst) 1),
    19         (rtac cont_id 1)
    20         ]);
    21 
    22 
    23 (* ------------------------------------------------------------------------ *)
    24 (* less_cfun is a partial order on type 'a -> 'b                            *)
    25 (* ------------------------------------------------------------------------ *)
    26 
    27 qed_goalw "refl_less_cfun" Cfun1.thy [less_cfun_def] "less_cfun f f"
    28 (fn prems =>
    29         [
    30         (rtac refl_less 1)
    31         ]);
    32 
    33 qed_goalw "antisym_less_cfun" Cfun1.thy [less_cfun_def] 
    34         "[|less_cfun f1 f2; less_cfun f2 f1|] ==> f1 = f2"
    35 (fn prems =>
    36         [
    37         (cut_facts_tac prems 1),
    38         (rtac injD 1),
    39         (rtac antisym_less 2),
    40         (atac 3),
    41         (atac 2),
    42         (rtac inj_inverseI 1),
    43         (rtac Rep_Cfun_inverse 1)
    44         ]);
    45 
    46 qed_goalw "trans_less_cfun" Cfun1.thy [less_cfun_def] 
    47         "[|less_cfun f1 f2; less_cfun f2 f3|] ==> less_cfun f1 f3"
    48 (fn prems =>
    49         [
    50         (cut_facts_tac prems 1),
    51         (etac trans_less 1),
    52         (atac 1)
    53         ]);
    54 
    55 (* ------------------------------------------------------------------------ *)
    56 (* lemmas about application of continuous functions                         *)
    57 (* ------------------------------------------------------------------------ *)
    58 
    59 qed_goal "cfun_cong" Cfun1.thy 
    60          "[| f=g; x=y |] ==> f`x = g`y"
    61 (fn prems =>
    62         [
    63         (cut_facts_tac prems 1),
    64         (fast_tac HOL_cs 1)
    65         ]);
    66 
    67 qed_goal "cfun_fun_cong" Cfun1.thy "f=g ==> f`x = g`x"
    68 (fn prems =>
    69         [
    70         (cut_facts_tac prems 1),
    71         (etac cfun_cong 1),
    72         (rtac refl 1)
    73         ]);
    74 
    75 qed_goal "cfun_arg_cong" Cfun1.thy "x=y ==> f`x = f`y"
    76 (fn prems =>
    77         [
    78         (cut_facts_tac prems 1),
    79         (rtac cfun_cong 1),
    80         (rtac refl 1),
    81         (atac 1)
    82         ]);
    83 
    84 
    85 (* ------------------------------------------------------------------------ *)
    86 (* additional lemma about the isomorphism between -> and Cfun               *)
    87 (* ------------------------------------------------------------------------ *)
    88 
    89 qed_goal "Abs_Cfun_inverse2" Cfun1.thy "cont(f) ==> fapp(fabs(f)) = f"
    90 (fn prems =>
    91         [
    92         (cut_facts_tac prems 1),
    93         (rtac Abs_Cfun_inverse 1),
    94         (rewtac Cfun_def),
    95         (etac (mem_Collect_eq RS ssubst) 1)
    96         ]);
    97 
    98 (* ------------------------------------------------------------------------ *)
    99 (* simplification of application                                            *)
   100 (* ------------------------------------------------------------------------ *)
   101 
   102 qed_goal "Cfunapp2" Cfun1.thy 
   103         "cont(f) ==> (fabs f)`x = f x"
   104 (fn prems =>
   105         [
   106         (cut_facts_tac prems 1),
   107         (etac (Abs_Cfun_inverse2 RS fun_cong) 1)
   108         ]);
   109 
   110 (* ------------------------------------------------------------------------ *)
   111 (* beta - equality for continuous functions                                 *)
   112 (* ------------------------------------------------------------------------ *)
   113 
   114 qed_goal "beta_cfun" Cfun1.thy 
   115         "cont(c1) ==> (LAM x .c1 x)`u = c1 u"
   116 (fn prems =>
   117         [
   118         (cut_facts_tac prems 1),
   119         (rtac Cfunapp2 1),
   120         (atac 1)
   121         ]);
   122 
   123 
   124 
   125