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