src/HOLCF/Cfun1.ML
author kleing
Mon Jun 21 10:25:57 2004 +0200 (2004-06-21)
changeset 14981 e73f8140af78
parent 12030 46d57d0290a2
child 15566 eb3b1a5c304e
permissions -rw-r--r--
Merged in license change from Isabelle2004
slotosch@2640
     1
(*  Title:      HOLCF/Cfun1.ML
nipkow@243
     2
    ID:         $Id$
clasohm@1461
     3
    Author:     Franz Regensburger
nipkow@243
     4
paulson@9245
     5
The type ->  of continuous functions.
nipkow@243
     6
*)
nipkow@243
     7
nipkow@243
     8
(* ------------------------------------------------------------------------ *)
slotosch@5291
     9
(* derive old type definition rules for Abs_CFun & Rep_CFun                         *)
slotosch@5291
    10
(* Rep_CFun and Abs_CFun should be replaced by Rep_Cfun anf Abs_Cfun in future      *)
nipkow@243
    11
(* ------------------------------------------------------------------------ *)
paulson@9248
    12
Goal "Rep_CFun fo : CFun";
paulson@9245
    13
by (rtac Rep_CFun 1);
paulson@9245
    14
qed "Rep_Cfun";
nipkow@243
    15
paulson@9248
    16
Goal "Abs_CFun (Rep_CFun fo) = fo";
paulson@9245
    17
by (rtac Rep_CFun_inverse 1);
paulson@9245
    18
qed "Rep_Cfun_inverse";
slotosch@2640
    19
paulson@9248
    20
Goal "f:CFun==>Rep_CFun(Abs_CFun f)=f";
paulson@9245
    21
by (etac Abs_CFun_inverse 1);
paulson@9245
    22
qed "Abs_Cfun_inverse";
nipkow@243
    23
nipkow@243
    24
(* ------------------------------------------------------------------------ *)
nipkow@243
    25
(* less_cfun is a partial order on type 'a -> 'b                            *)
nipkow@243
    26
(* ------------------------------------------------------------------------ *)
nipkow@243
    27
paulson@9248
    28
Goalw [less_cfun_def] "(f::'a->'b) << f";
paulson@9245
    29
by (rtac refl_less 1);
paulson@9245
    30
qed "refl_less_cfun";
nipkow@243
    31
paulson@9248
    32
Goalw [less_cfun_def] 
paulson@9245
    33
        "[|(f1::'a->'b) << f2; f2 << f1|] ==> f1 = f2";
paulson@9245
    34
by (rtac injD 1);
paulson@9245
    35
by (rtac antisym_less 2);
paulson@9245
    36
by (atac 3);
paulson@9245
    37
by (atac 2);
paulson@9245
    38
by (rtac inj_inverseI 1);
paulson@9245
    39
by (rtac Rep_Cfun_inverse 1);
paulson@9245
    40
qed "antisym_less_cfun";
nipkow@243
    41
paulson@9248
    42
Goalw [less_cfun_def] 
paulson@9245
    43
        "[|(f1::'a->'b) << f2; f2 << f3|] ==> f1 << f3";
paulson@9245
    44
by (etac trans_less 1);
paulson@9245
    45
by (atac 1);
paulson@9245
    46
qed "trans_less_cfun";
nipkow@243
    47
nipkow@243
    48
(* ------------------------------------------------------------------------ *)
nipkow@243
    49
(* lemmas about application of continuous functions                         *)
nipkow@243
    50
(* ------------------------------------------------------------------------ *)
nipkow@243
    51
nipkow@10834
    52
Goal "[| f=g; x=y |] ==> f$x = g$y";
paulson@9248
    53
by (Asm_simp_tac 1);
paulson@9245
    54
qed "cfun_cong";
nipkow@243
    55
nipkow@10834
    56
Goal "f=g ==> f$x = g$x";
paulson@9248
    57
by (Asm_simp_tac 1);
paulson@9245
    58
qed "cfun_fun_cong";
nipkow@243
    59
nipkow@10834
    60
Goal "x=y ==> f$x = f$y";
paulson@9248
    61
by (Asm_simp_tac 1);
paulson@9245
    62
qed "cfun_arg_cong";
nipkow@243
    63
nipkow@243
    64
nipkow@243
    65
(* ------------------------------------------------------------------------ *)
nipkow@243
    66
(* additional lemma about the isomorphism between -> and Cfun               *)
nipkow@243
    67
(* ------------------------------------------------------------------------ *)
nipkow@243
    68
paulson@9248
    69
Goal "cont f ==> Rep_CFun (Abs_CFun f) = f";
paulson@9245
    70
by (rtac Abs_Cfun_inverse 1);
paulson@9245
    71
by (rewtac CFun_def);
paulson@9245
    72
by (etac (mem_Collect_eq RS ssubst) 1);
paulson@9245
    73
qed "Abs_Cfun_inverse2";
nipkow@243
    74
nipkow@243
    75
(* ------------------------------------------------------------------------ *)
nipkow@243
    76
(* simplification of application                                            *)
nipkow@243
    77
(* ------------------------------------------------------------------------ *)
nipkow@243
    78
nipkow@10834
    79
Goal "cont f ==> (Abs_CFun f)$x = f x";
paulson@9245
    80
by (etac (Abs_Cfun_inverse2 RS fun_cong) 1);
paulson@9245
    81
qed "Cfunapp2";
nipkow@243
    82
nipkow@243
    83
(* ------------------------------------------------------------------------ *)
nipkow@243
    84
(* beta - equality for continuous functions                                 *)
nipkow@243
    85
(* ------------------------------------------------------------------------ *)
nipkow@243
    86
nipkow@10834
    87
Goal "cont(c1) ==> (LAM x .c1 x)$u = c1 u";
paulson@9245
    88
by (rtac Cfunapp2 1);
paulson@9245
    89
by (atac 1);
paulson@9245
    90
qed "beta_cfun";