src/HOLCF/Cfun1.ML
author wenzelm
Sat Nov 03 01:41:26 2001 +0100 (2001-11-03)
changeset 12030 46d57d0290a2
parent 10834 a7897aebbffc
child 14981 e73f8140af78
permissions -rw-r--r--
GPLed;
slotosch@2640
     1
(*  Title:      HOLCF/Cfun1.ML
nipkow@243
     2
    ID:         $Id$
clasohm@1461
     3
    Author:     Franz Regensburger
wenzelm@12030
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
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@9248
    13
Goal "Rep_CFun fo : CFun";
paulson@9245
    14
by (rtac Rep_CFun 1);
paulson@9245
    15
qed "Rep_Cfun";
nipkow@243
    16
paulson@9248
    17
Goal "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@9248
    21
Goal "f:CFun==>Rep_CFun(Abs_CFun f)=f";
paulson@9245
    22
by (etac Abs_CFun_inverse 1);
paulson@9245
    23
qed "Abs_Cfun_inverse";
nipkow@243
    24
nipkow@243
    25
(* ------------------------------------------------------------------------ *)
nipkow@243
    26
(* less_cfun is a partial order on type 'a -> 'b                            *)
nipkow@243
    27
(* ------------------------------------------------------------------------ *)
nipkow@243
    28
paulson@9248
    29
Goalw [less_cfun_def] "(f::'a->'b) << f";
paulson@9245
    30
by (rtac refl_less 1);
paulson@9245
    31
qed "refl_less_cfun";
nipkow@243
    32
paulson@9248
    33
Goalw [less_cfun_def] 
paulson@9245
    34
        "[|(f1::'a->'b) << f2; f2 << f1|] ==> f1 = f2";
paulson@9245
    35
by (rtac injD 1);
paulson@9245
    36
by (rtac antisym_less 2);
paulson@9245
    37
by (atac 3);
paulson@9245
    38
by (atac 2);
paulson@9245
    39
by (rtac inj_inverseI 1);
paulson@9245
    40
by (rtac Rep_Cfun_inverse 1);
paulson@9245
    41
qed "antisym_less_cfun";
nipkow@243
    42
paulson@9248
    43
Goalw [less_cfun_def] 
paulson@9245
    44
        "[|(f1::'a->'b) << f2; f2 << f3|] ==> f1 << f3";
paulson@9245
    45
by (etac trans_less 1);
paulson@9245
    46
by (atac 1);
paulson@9245
    47
qed "trans_less_cfun";
nipkow@243
    48
nipkow@243
    49
(* ------------------------------------------------------------------------ *)
nipkow@243
    50
(* lemmas about application of continuous functions                         *)
nipkow@243
    51
(* ------------------------------------------------------------------------ *)
nipkow@243
    52
nipkow@10834
    53
Goal "[| f=g; x=y |] ==> f$x = g$y";
paulson@9248
    54
by (Asm_simp_tac 1);
paulson@9245
    55
qed "cfun_cong";
nipkow@243
    56
nipkow@10834
    57
Goal "f=g ==> f$x = g$x";
paulson@9248
    58
by (Asm_simp_tac 1);
paulson@9245
    59
qed "cfun_fun_cong";
nipkow@243
    60
nipkow@10834
    61
Goal "x=y ==> f$x = f$y";
paulson@9248
    62
by (Asm_simp_tac 1);
paulson@9245
    63
qed "cfun_arg_cong";
nipkow@243
    64
nipkow@243
    65
nipkow@243
    66
(* ------------------------------------------------------------------------ *)
nipkow@243
    67
(* additional lemma about the isomorphism between -> and Cfun               *)
nipkow@243
    68
(* ------------------------------------------------------------------------ *)
nipkow@243
    69
paulson@9248
    70
Goal "cont f ==> Rep_CFun (Abs_CFun f) = f";
paulson@9245
    71
by (rtac Abs_Cfun_inverse 1);
paulson@9245
    72
by (rewtac CFun_def);
paulson@9245
    73
by (etac (mem_Collect_eq RS ssubst) 1);
paulson@9245
    74
qed "Abs_Cfun_inverse2";
nipkow@243
    75
nipkow@243
    76
(* ------------------------------------------------------------------------ *)
nipkow@243
    77
(* simplification of application                                            *)
nipkow@243
    78
(* ------------------------------------------------------------------------ *)
nipkow@243
    79
nipkow@10834
    80
Goal "cont f ==> (Abs_CFun f)$x = f x";
paulson@9245
    81
by (etac (Abs_Cfun_inverse2 RS fun_cong) 1);
paulson@9245
    82
qed "Cfunapp2";
nipkow@243
    83
nipkow@243
    84
(* ------------------------------------------------------------------------ *)
nipkow@243
    85
(* beta - equality for continuous functions                                 *)
nipkow@243
    86
(* ------------------------------------------------------------------------ *)
nipkow@243
    87
nipkow@10834
    88
Goal "cont(c1) ==> (LAM x .c1 x)$u = c1 u";
paulson@9245
    89
by (rtac Cfunapp2 1);
paulson@9245
    90
by (atac 1);
paulson@9245
    91
qed "beta_cfun";