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
slotosch@2640
     1
(*  Title:      HOLCF/Cfun1.ML
nipkow@243
     2
    ID:         $Id$
clasohm@1461
     3
    Author:     Franz Regensburger
nipkow@243
     4
    Copyright   1993 Technische Universitaet Muenchen
nipkow@243
     5
paulson@9245
     6
The type ->  of continuous functions.
nipkow@243
     7
*)
nipkow@243
     8
nipkow@243
     9
(* ------------------------------------------------------------------------ *)
slotosch@5291
    10
(* derive old type definition rules for Abs_CFun & Rep_CFun                         *)
slotosch@5291
    11
(* Rep_CFun and Abs_CFun should be replaced by Rep_Cfun anf Abs_Cfun in future      *)
nipkow@243
    12
(* ------------------------------------------------------------------------ *)
paulson@9245
    13
val prems = goal thy "Rep_CFun fo : CFun";
paulson@9245
    14
by (rtac Rep_CFun 1);
paulson@9245
    15
qed "Rep_Cfun";
nipkow@243
    16
paulson@9245
    17
val prems = goal thy "Abs_CFun (Rep_CFun fo) = fo";
paulson@9245
    18
by (rtac Rep_CFun_inverse 1);
paulson@9245
    19
qed "Rep_Cfun_inverse";
slotosch@2640
    20
paulson@9245
    21
val prems = goal thy "f:CFun==>Rep_CFun(Abs_CFun f)=f";
paulson@9245
    22
by (cut_facts_tac prems 1);
paulson@9245
    23
by (etac Abs_CFun_inverse 1);
paulson@9245
    24
qed "Abs_Cfun_inverse";
nipkow@243
    25
nipkow@243
    26
(* ------------------------------------------------------------------------ *)
nipkow@243
    27
(* less_cfun is a partial order on type 'a -> 'b                            *)
nipkow@243
    28
(* ------------------------------------------------------------------------ *)
nipkow@243
    29
paulson@9245
    30
val prems = goalw thy [less_cfun_def] "(f::'a->'b) << f";
paulson@9245
    31
by (rtac refl_less 1);
paulson@9245
    32
qed "refl_less_cfun";
nipkow@243
    33
paulson@9245
    34
val prems = goalw thy [less_cfun_def] 
paulson@9245
    35
        "[|(f1::'a->'b) << f2; f2 << f1|] ==> f1 = f2";
paulson@9245
    36
by (cut_facts_tac prems 1);
paulson@9245
    37
by (rtac injD 1);
paulson@9245
    38
by (rtac antisym_less 2);
paulson@9245
    39
by (atac 3);
paulson@9245
    40
by (atac 2);
paulson@9245
    41
by (rtac inj_inverseI 1);
paulson@9245
    42
by (rtac Rep_Cfun_inverse 1);
paulson@9245
    43
qed "antisym_less_cfun";
nipkow@243
    44
paulson@9245
    45
val prems = goalw thy [less_cfun_def] 
paulson@9245
    46
        "[|(f1::'a->'b) << f2; f2 << f3|] ==> f1 << f3";
paulson@9245
    47
by (cut_facts_tac prems 1);
paulson@9245
    48
by (etac trans_less 1);
paulson@9245
    49
by (atac 1);
paulson@9245
    50
qed "trans_less_cfun";
nipkow@243
    51
nipkow@243
    52
(* ------------------------------------------------------------------------ *)
nipkow@243
    53
(* lemmas about application of continuous functions                         *)
nipkow@243
    54
(* ------------------------------------------------------------------------ *)
nipkow@243
    55
paulson@9245
    56
val prems = goal thy 
paulson@9245
    57
         "[| f=g; x=y |] ==> f`x = g`y";
paulson@9245
    58
by (cut_facts_tac prems 1);
paulson@9245
    59
by (fast_tac HOL_cs 1);
paulson@9245
    60
qed "cfun_cong";
nipkow@243
    61
paulson@9245
    62
val prems = goal thy "f=g ==> f`x = g`x";
paulson@9245
    63
by (cut_facts_tac prems 1);
paulson@9245
    64
by (etac cfun_cong 1);
paulson@9245
    65
by (rtac refl 1);
paulson@9245
    66
qed "cfun_fun_cong";
nipkow@243
    67
paulson@9245
    68
val prems = goal thy "x=y ==> f`x = f`y";
paulson@9245
    69
by (cut_facts_tac prems 1);
paulson@9245
    70
by (rtac cfun_cong 1);
paulson@9245
    71
by (rtac refl 1);
paulson@9245
    72
by (atac 1);
paulson@9245
    73
qed "cfun_arg_cong";
nipkow@243
    74
nipkow@243
    75
nipkow@243
    76
(* ------------------------------------------------------------------------ *)
nipkow@243
    77
(* additional lemma about the isomorphism between -> and Cfun               *)
nipkow@243
    78
(* ------------------------------------------------------------------------ *)
nipkow@243
    79
paulson@9245
    80
val prems = goal thy "cont f ==> Rep_CFun (Abs_CFun f) = f";
paulson@9245
    81
by (cut_facts_tac prems 1);
paulson@9245
    82
by (rtac Abs_Cfun_inverse 1);
paulson@9245
    83
by (rewtac CFun_def);
paulson@9245
    84
by (etac (mem_Collect_eq RS ssubst) 1);
paulson@9245
    85
qed "Abs_Cfun_inverse2";
nipkow@243
    86
nipkow@243
    87
(* ------------------------------------------------------------------------ *)
nipkow@243
    88
(* simplification of application                                            *)
nipkow@243
    89
(* ------------------------------------------------------------------------ *)
nipkow@243
    90
paulson@9245
    91
val prems = goal thy "cont f ==> (Abs_CFun f)`x = f x";
paulson@9245
    92
by (cut_facts_tac prems 1);
paulson@9245
    93
by (etac (Abs_Cfun_inverse2 RS fun_cong) 1);
paulson@9245
    94
qed "Cfunapp2";
nipkow@243
    95
nipkow@243
    96
(* ------------------------------------------------------------------------ *)
nipkow@243
    97
(* beta - equality for continuous functions                                 *)
nipkow@243
    98
(* ------------------------------------------------------------------------ *)
nipkow@243
    99
paulson@9245
   100
val prems = goal thy 
paulson@9245
   101
        "cont(c1) ==> (LAM x .c1 x)`u = c1 u";
paulson@9245
   102
by (cut_facts_tac prems 1);
paulson@9245
   103
by (rtac Cfunapp2 1);
paulson@9245
   104
by (atac 1);
paulson@9245
   105
qed "beta_cfun";