src/HOLCF/Cfun1.ML
author nipkow
Tue Jan 09 15:32:27 2001 +0100 (2001-01-09)
changeset 10834 a7897aebbffc
parent 9248 e1dee89de037
child 12030 46d57d0290a2
permissions -rw-r--r--
*** empty log message ***
     1 (*  Title:      HOLCF/Cfun1.ML
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 The type ->  of continuous functions.
     7 *)
     8 
     9 (* ------------------------------------------------------------------------ *)
    10 (* derive old type definition rules for Abs_CFun & Rep_CFun                         *)
    11 (* Rep_CFun and Abs_CFun should be replaced by Rep_Cfun anf Abs_Cfun in future      *)
    12 (* ------------------------------------------------------------------------ *)
    13 Goal "Rep_CFun fo : CFun";
    14 by (rtac Rep_CFun 1);
    15 qed "Rep_Cfun";
    16 
    17 Goal "Abs_CFun (Rep_CFun fo) = fo";
    18 by (rtac Rep_CFun_inverse 1);
    19 qed "Rep_Cfun_inverse";
    20 
    21 Goal "f:CFun==>Rep_CFun(Abs_CFun f)=f";
    22 by (etac Abs_CFun_inverse 1);
    23 qed "Abs_Cfun_inverse";
    24 
    25 (* ------------------------------------------------------------------------ *)
    26 (* less_cfun is a partial order on type 'a -> 'b                            *)
    27 (* ------------------------------------------------------------------------ *)
    28 
    29 Goalw [less_cfun_def] "(f::'a->'b) << f";
    30 by (rtac refl_less 1);
    31 qed "refl_less_cfun";
    32 
    33 Goalw [less_cfun_def] 
    34         "[|(f1::'a->'b) << f2; f2 << f1|] ==> f1 = f2";
    35 by (rtac injD 1);
    36 by (rtac antisym_less 2);
    37 by (atac 3);
    38 by (atac 2);
    39 by (rtac inj_inverseI 1);
    40 by (rtac Rep_Cfun_inverse 1);
    41 qed "antisym_less_cfun";
    42 
    43 Goalw [less_cfun_def] 
    44         "[|(f1::'a->'b) << f2; f2 << f3|] ==> f1 << f3";
    45 by (etac trans_less 1);
    46 by (atac 1);
    47 qed "trans_less_cfun";
    48 
    49 (* ------------------------------------------------------------------------ *)
    50 (* lemmas about application of continuous functions                         *)
    51 (* ------------------------------------------------------------------------ *)
    52 
    53 Goal "[| f=g; x=y |] ==> f$x = g$y";
    54 by (Asm_simp_tac 1);
    55 qed "cfun_cong";
    56 
    57 Goal "f=g ==> f$x = g$x";
    58 by (Asm_simp_tac 1);
    59 qed "cfun_fun_cong";
    60 
    61 Goal "x=y ==> f$x = f$y";
    62 by (Asm_simp_tac 1);
    63 qed "cfun_arg_cong";
    64 
    65 
    66 (* ------------------------------------------------------------------------ *)
    67 (* additional lemma about the isomorphism between -> and Cfun               *)
    68 (* ------------------------------------------------------------------------ *)
    69 
    70 Goal "cont f ==> Rep_CFun (Abs_CFun f) = f";
    71 by (rtac Abs_Cfun_inverse 1);
    72 by (rewtac CFun_def);
    73 by (etac (mem_Collect_eq RS ssubst) 1);
    74 qed "Abs_Cfun_inverse2";
    75 
    76 (* ------------------------------------------------------------------------ *)
    77 (* simplification of application                                            *)
    78 (* ------------------------------------------------------------------------ *)
    79 
    80 Goal "cont f ==> (Abs_CFun f)$x = f x";
    81 by (etac (Abs_Cfun_inverse2 RS fun_cong) 1);
    82 qed "Cfunapp2";
    83 
    84 (* ------------------------------------------------------------------------ *)
    85 (* beta - equality for continuous functions                                 *)
    86 (* ------------------------------------------------------------------------ *)
    87 
    88 Goal "cont(c1) ==> (LAM x .c1 x)$u = c1 u";
    89 by (rtac Cfunapp2 1);
    90 by (atac 1);
    91 qed "beta_cfun";