src/HOLCF/Cfun1.ML
author paulson
Tue Jul 04 15:58:11 2000 +0200 (2000-07-04)
changeset 9245 428385c4bc50
parent 5291 5706f0ef1d43
child 9248 e1dee89de037
permissions -rw-r--r--
removed most batch-style proofs
     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 val prems = goal thy "Rep_CFun fo : CFun";
    14 by (rtac Rep_CFun 1);
    15 qed "Rep_Cfun";
    16 
    17 val prems = goal thy "Abs_CFun (Rep_CFun fo) = fo";
    18 by (rtac Rep_CFun_inverse 1);
    19 qed "Rep_Cfun_inverse";
    20 
    21 val prems = goal thy "f:CFun==>Rep_CFun(Abs_CFun f)=f";
    22 by (cut_facts_tac prems 1);
    23 by (etac Abs_CFun_inverse 1);
    24 qed "Abs_Cfun_inverse";
    25 
    26 (* ------------------------------------------------------------------------ *)
    27 (* less_cfun is a partial order on type 'a -> 'b                            *)
    28 (* ------------------------------------------------------------------------ *)
    29 
    30 val prems = goalw thy [less_cfun_def] "(f::'a->'b) << f";
    31 by (rtac refl_less 1);
    32 qed "refl_less_cfun";
    33 
    34 val prems = goalw thy [less_cfun_def] 
    35         "[|(f1::'a->'b) << f2; f2 << f1|] ==> f1 = f2";
    36 by (cut_facts_tac prems 1);
    37 by (rtac injD 1);
    38 by (rtac antisym_less 2);
    39 by (atac 3);
    40 by (atac 2);
    41 by (rtac inj_inverseI 1);
    42 by (rtac Rep_Cfun_inverse 1);
    43 qed "antisym_less_cfun";
    44 
    45 val prems = goalw thy [less_cfun_def] 
    46         "[|(f1::'a->'b) << f2; f2 << f3|] ==> f1 << f3";
    47 by (cut_facts_tac prems 1);
    48 by (etac trans_less 1);
    49 by (atac 1);
    50 qed "trans_less_cfun";
    51 
    52 (* ------------------------------------------------------------------------ *)
    53 (* lemmas about application of continuous functions                         *)
    54 (* ------------------------------------------------------------------------ *)
    55 
    56 val prems = goal thy 
    57          "[| f=g; x=y |] ==> f`x = g`y";
    58 by (cut_facts_tac prems 1);
    59 by (fast_tac HOL_cs 1);
    60 qed "cfun_cong";
    61 
    62 val prems = goal thy "f=g ==> f`x = g`x";
    63 by (cut_facts_tac prems 1);
    64 by (etac cfun_cong 1);
    65 by (rtac refl 1);
    66 qed "cfun_fun_cong";
    67 
    68 val prems = goal thy "x=y ==> f`x = f`y";
    69 by (cut_facts_tac prems 1);
    70 by (rtac cfun_cong 1);
    71 by (rtac refl 1);
    72 by (atac 1);
    73 qed "cfun_arg_cong";
    74 
    75 
    76 (* ------------------------------------------------------------------------ *)
    77 (* additional lemma about the isomorphism between -> and Cfun               *)
    78 (* ------------------------------------------------------------------------ *)
    79 
    80 val prems = goal thy "cont f ==> Rep_CFun (Abs_CFun f) = f";
    81 by (cut_facts_tac prems 1);
    82 by (rtac Abs_Cfun_inverse 1);
    83 by (rewtac CFun_def);
    84 by (etac (mem_Collect_eq RS ssubst) 1);
    85 qed "Abs_Cfun_inverse2";
    86 
    87 (* ------------------------------------------------------------------------ *)
    88 (* simplification of application                                            *)
    89 (* ------------------------------------------------------------------------ *)
    90 
    91 val prems = goal thy "cont f ==> (Abs_CFun f)`x = f x";
    92 by (cut_facts_tac prems 1);
    93 by (etac (Abs_Cfun_inverse2 RS fun_cong) 1);
    94 qed "Cfunapp2";
    95 
    96 (* ------------------------------------------------------------------------ *)
    97 (* beta - equality for continuous functions                                 *)
    98 (* ------------------------------------------------------------------------ *)
    99 
   100 val prems = goal thy 
   101         "cont(c1) ==> (LAM x .c1 x)`u = c1 u";
   102 by (cut_facts_tac prems 1);
   103 by (rtac Cfunapp2 1);
   104 by (atac 1);
   105 qed "beta_cfun";