src/HOLCF/Cfun1.ML
author slotosch
Wed Aug 12 12:17:20 1998 +0200 (1998-08-12)
changeset 5291 5706f0ef1d43
parent 3323 194ae2e0c193
child 9245 428385c4bc50
permissions -rw-r--r--
eliminated fabs,fapp.
changed all theorem names and functions into Rep_CFun, Abs_CFun
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
slotosch@2640
     6
Lemmas for Cfun1.thy 
nipkow@243
     7
*)
nipkow@243
     8
nipkow@243
     9
open Cfun1;
nipkow@243
    10
nipkow@243
    11
(* ------------------------------------------------------------------------ *)
slotosch@5291
    12
(* derive old type definition rules for Abs_CFun & Rep_CFun                         *)
slotosch@5291
    13
(* Rep_CFun and Abs_CFun should be replaced by Rep_Cfun anf Abs_Cfun in future      *)
nipkow@243
    14
(* ------------------------------------------------------------------------ *)
slotosch@5291
    15
qed_goal "Rep_Cfun" thy "Rep_CFun fo : CFun"
slotosch@2640
    16
(fn prems =>
clasohm@1461
    17
        [
slotosch@2640
    18
        (rtac Rep_CFun 1)
clasohm@1461
    19
        ]);
nipkow@243
    20
slotosch@5291
    21
qed_goal "Rep_Cfun_inverse" thy "Abs_CFun (Rep_CFun fo) = fo"
slotosch@2640
    22
(fn prems =>
slotosch@2640
    23
        [
slotosch@2640
    24
        (rtac Rep_CFun_inverse 1)
slotosch@2640
    25
        ]);
slotosch@2640
    26
slotosch@5291
    27
qed_goal "Abs_Cfun_inverse" thy "f:CFun==>Rep_CFun(Abs_CFun f)=f"
slotosch@2640
    28
(fn prems =>
slotosch@2640
    29
        [
slotosch@2640
    30
	(cut_facts_tac prems 1),
slotosch@2640
    31
        (etac Abs_CFun_inverse 1)
slotosch@2640
    32
        ]);
nipkow@243
    33
nipkow@243
    34
(* ------------------------------------------------------------------------ *)
nipkow@243
    35
(* less_cfun is a partial order on type 'a -> 'b                            *)
nipkow@243
    36
(* ------------------------------------------------------------------------ *)
nipkow@243
    37
slotosch@3323
    38
qed_goalw "refl_less_cfun" thy [less_cfun_def] "(f::'a->'b) << f"
nipkow@243
    39
(fn prems =>
clasohm@1461
    40
        [
clasohm@1461
    41
        (rtac refl_less 1)
clasohm@1461
    42
        ]);
nipkow@243
    43
slotosch@2640
    44
qed_goalw "antisym_less_cfun" thy [less_cfun_def] 
slotosch@3323
    45
        "[|(f1::'a->'b) << f2; f2 << f1|] ==> f1 = f2"
nipkow@243
    46
(fn prems =>
clasohm@1461
    47
        [
clasohm@1461
    48
        (cut_facts_tac prems 1),
clasohm@1461
    49
        (rtac injD 1),
clasohm@1461
    50
        (rtac antisym_less 2),
clasohm@1461
    51
        (atac 3),
clasohm@1461
    52
        (atac 2),
clasohm@1461
    53
        (rtac inj_inverseI 1),
clasohm@1461
    54
        (rtac Rep_Cfun_inverse 1)
clasohm@1461
    55
        ]);
nipkow@243
    56
slotosch@2640
    57
qed_goalw "trans_less_cfun" thy [less_cfun_def] 
slotosch@3323
    58
        "[|(f1::'a->'b) << f2; f2 << f3|] ==> f1 << f3"
nipkow@243
    59
(fn prems =>
clasohm@1461
    60
        [
clasohm@1461
    61
        (cut_facts_tac prems 1),
clasohm@1461
    62
        (etac trans_less 1),
clasohm@1461
    63
        (atac 1)
clasohm@1461
    64
        ]);
nipkow@243
    65
nipkow@243
    66
(* ------------------------------------------------------------------------ *)
nipkow@243
    67
(* lemmas about application of continuous functions                         *)
nipkow@243
    68
(* ------------------------------------------------------------------------ *)
nipkow@243
    69
slotosch@2640
    70
qed_goal "cfun_cong" thy 
clasohm@1461
    71
         "[| f=g; x=y |] ==> f`x = g`y"
nipkow@243
    72
(fn prems =>
clasohm@1461
    73
        [
clasohm@1461
    74
        (cut_facts_tac prems 1),
clasohm@1461
    75
        (fast_tac HOL_cs 1)
clasohm@1461
    76
        ]);
nipkow@243
    77
slotosch@2640
    78
qed_goal "cfun_fun_cong" thy "f=g ==> f`x = g`x"
nipkow@243
    79
(fn prems =>
clasohm@1461
    80
        [
clasohm@1461
    81
        (cut_facts_tac prems 1),
clasohm@1461
    82
        (etac cfun_cong 1),
clasohm@1461
    83
        (rtac refl 1)
clasohm@1461
    84
        ]);
nipkow@243
    85
slotosch@2640
    86
qed_goal "cfun_arg_cong" thy "x=y ==> f`x = f`y"
nipkow@243
    87
(fn prems =>
clasohm@1461
    88
        [
clasohm@1461
    89
        (cut_facts_tac prems 1),
clasohm@1461
    90
        (rtac cfun_cong 1),
clasohm@1461
    91
        (rtac refl 1),
clasohm@1461
    92
        (atac 1)
clasohm@1461
    93
        ]);
nipkow@243
    94
nipkow@243
    95
nipkow@243
    96
(* ------------------------------------------------------------------------ *)
nipkow@243
    97
(* additional lemma about the isomorphism between -> and Cfun               *)
nipkow@243
    98
(* ------------------------------------------------------------------------ *)
nipkow@243
    99
slotosch@5291
   100
qed_goal "Abs_Cfun_inverse2" thy "cont f ==> Rep_CFun (Abs_CFun f) = f"
nipkow@243
   101
(fn prems =>
clasohm@1461
   102
        [
clasohm@1461
   103
        (cut_facts_tac prems 1),
clasohm@1461
   104
        (rtac Abs_Cfun_inverse 1),
slotosch@2640
   105
        (rewtac CFun_def),
clasohm@1461
   106
        (etac (mem_Collect_eq RS ssubst) 1)
clasohm@1461
   107
        ]);
nipkow@243
   108
nipkow@243
   109
(* ------------------------------------------------------------------------ *)
nipkow@243
   110
(* simplification of application                                            *)
nipkow@243
   111
(* ------------------------------------------------------------------------ *)
nipkow@243
   112
slotosch@5291
   113
qed_goal "Cfunapp2" thy "cont f ==> (Abs_CFun f)`x = f x"
nipkow@243
   114
(fn prems =>
clasohm@1461
   115
        [
clasohm@1461
   116
        (cut_facts_tac prems 1),
clasohm@1461
   117
        (etac (Abs_Cfun_inverse2 RS fun_cong) 1)
clasohm@1461
   118
        ]);
nipkow@243
   119
nipkow@243
   120
(* ------------------------------------------------------------------------ *)
nipkow@243
   121
(* beta - equality for continuous functions                                 *)
nipkow@243
   122
(* ------------------------------------------------------------------------ *)
nipkow@243
   123
slotosch@2640
   124
qed_goal "beta_cfun" thy 
clasohm@1461
   125
        "cont(c1) ==> (LAM x .c1 x)`u = c1 u"
nipkow@243
   126
(fn prems =>
clasohm@1461
   127
        [
clasohm@1461
   128
        (cut_facts_tac prems 1),
clasohm@1461
   129
        (rtac Cfunapp2 1),
clasohm@1461
   130
        (atac 1)
clasohm@1461
   131
        ]);