src/HOLCF/Fun2.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 4721 c8a8482a8124
child 9245 428385c4bc50
permissions -rw-r--r--
made tutorial first;
clasohm@1461
     1
(*  Title:      HOLCF/fun2.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 fun2.thy 
nipkow@243
     7
*)
nipkow@243
     8
nipkow@243
     9
open Fun2;
nipkow@243
    10
slotosch@2640
    11
(* for compatibility with old HOLCF-Version *)
wenzelm@3842
    12
qed_goal "inst_fun_po" thy "(op <<)=(%f g.!x. f x << g x)"
slotosch@2640
    13
 (fn prems => 
slotosch@2640
    14
        [
slotosch@3323
    15
	(fold_goals_tac [less_fun_def]),
slotosch@2640
    16
	(rtac refl 1)
slotosch@2640
    17
        ]);
slotosch@2640
    18
nipkow@243
    19
(* ------------------------------------------------------------------------ *)
nipkow@243
    20
(* Type 'a::term => 'b::pcpo is pointed                                     *)
nipkow@243
    21
(* ------------------------------------------------------------------------ *)
nipkow@243
    22
wenzelm@3842
    23
qed_goal "minimal_fun" thy "(%z. UU) << x"
nipkow@243
    24
(fn prems =>
clasohm@1461
    25
        [
wenzelm@4098
    26
        (simp_tac (simpset() addsimps [inst_fun_po,minimal]) 1)
slotosch@2640
    27
        ]);
slotosch@2640
    28
slotosch@2640
    29
bind_thm ("UU_fun_def",minimal_fun RS minimal2UU RS sym);
slotosch@2640
    30
wenzelm@3842
    31
qed_goal "least_fun" thy "? x::'a=>'b::pcpo.!y. x<<y"
slotosch@2640
    32
(fn prems =>
slotosch@2640
    33
        [
wenzelm@3842
    34
        (res_inst_tac [("x","(%z. UU)")] exI 1),
slotosch@2640
    35
        (rtac (minimal_fun RS allI) 1)
clasohm@1461
    36
        ]);
nipkow@243
    37
nipkow@243
    38
(* ------------------------------------------------------------------------ *)
nipkow@243
    39
(* make the symbol << accessible for type fun                               *)
nipkow@243
    40
(* ------------------------------------------------------------------------ *)
nipkow@243
    41
slotosch@2640
    42
qed_goal "less_fun" thy "(f1 << f2) = (! x. f1(x) << f2(x))"
nipkow@243
    43
(fn prems =>
clasohm@1461
    44
        [
paulson@2033
    45
        (stac inst_fun_po 1),
clasohm@1461
    46
        (fold_goals_tac [less_fun_def]),
clasohm@1461
    47
        (rtac refl 1)
clasohm@1461
    48
        ]);
nipkow@243
    49
nipkow@243
    50
(* ------------------------------------------------------------------------ *)
nipkow@243
    51
(* chains of functions yield chains in the po range                         *)
nipkow@243
    52
(* ------------------------------------------------------------------------ *)
nipkow@243
    53
slotosch@2640
    54
qed_goal "ch2ch_fun" thy 
oheimb@4721
    55
        "chain(S::nat=>('a=>'b::po)) ==> chain(% i. S(i)(x))"
nipkow@243
    56
(fn prems =>
clasohm@1461
    57
        [
clasohm@1461
    58
        (cut_facts_tac prems 1),
oheimb@4721
    59
        (rewtac chain),
clasohm@1461
    60
        (rtac allI 1),
clasohm@1461
    61
        (rtac spec 1),
clasohm@1461
    62
        (rtac (less_fun RS subst) 1),
clasohm@1461
    63
        (etac allE 1),
clasohm@1461
    64
        (atac 1)
clasohm@1461
    65
        ]);
nipkow@243
    66
nipkow@243
    67
(* ------------------------------------------------------------------------ *)
nipkow@243
    68
(* upper bounds of function chains yield upper bound in the po range        *)
nipkow@243
    69
(* ------------------------------------------------------------------------ *)
nipkow@243
    70
clasohm@892
    71
qed_goal "ub2ub_fun" Fun2.thy 
regensbu@1168
    72
   " range(S::nat=>('a::term => 'b::po)) <| u ==> range(%i. S i x) <| u(x)"
nipkow@243
    73
(fn prems =>
clasohm@1461
    74
        [
clasohm@1461
    75
        (cut_facts_tac prems 1),
clasohm@1461
    76
        (rtac ub_rangeI 1),
clasohm@1461
    77
        (rtac allI 1),
clasohm@1461
    78
        (rtac allE 1),
clasohm@1461
    79
        (rtac (less_fun RS subst) 1),
clasohm@1461
    80
        (etac (ub_rangeE RS spec) 1),
clasohm@1461
    81
        (atac 1)
clasohm@1461
    82
        ]);
nipkow@243
    83
nipkow@243
    84
(* ------------------------------------------------------------------------ *)
nipkow@243
    85
(* Type 'a::term => 'b::pcpo is chain complete                              *)
nipkow@243
    86
(* ------------------------------------------------------------------------ *)
nipkow@243
    87
clasohm@892
    88
qed_goal "lub_fun"  Fun2.thy
oheimb@4721
    89
        "chain(S::nat=>('a::term => 'b::cpo)) ==> \
wenzelm@3842
    90
\        range(S) <<| (% x. lub(range(% i. S(i)(x))))"
nipkow@243
    91
(fn prems =>
clasohm@1461
    92
        [
clasohm@1461
    93
        (cut_facts_tac prems 1),
clasohm@1461
    94
        (rtac is_lubI 1),
clasohm@1461
    95
        (rtac conjI 1),
clasohm@1461
    96
        (rtac ub_rangeI 1),
clasohm@1461
    97
        (rtac allI 1),
paulson@2033
    98
        (stac less_fun 1),
clasohm@1461
    99
        (rtac allI 1),
clasohm@1461
   100
        (rtac is_ub_thelub 1),
clasohm@1461
   101
        (etac ch2ch_fun 1),
clasohm@1461
   102
        (strip_tac 1),
paulson@2033
   103
        (stac less_fun 1),
clasohm@1461
   104
        (rtac allI 1),
clasohm@1461
   105
        (rtac is_lub_thelub 1),
clasohm@1461
   106
        (etac ch2ch_fun 1),
clasohm@1461
   107
        (etac ub2ub_fun 1)
clasohm@1461
   108
        ]);
nipkow@243
   109
oheimb@1779
   110
bind_thm ("thelub_fun", lub_fun RS thelubI);
oheimb@4721
   111
(* chain ?S1 ==> lub (range ?S1) = (%x. lub (range (%i. ?S1 i x))) *)
nipkow@243
   112
clasohm@892
   113
qed_goal "cpo_fun"  Fun2.thy
oheimb@4721
   114
        "chain(S::nat=>('a::term => 'b::cpo)) ==> ? x. range(S) <<| x"
nipkow@243
   115
(fn prems =>
clasohm@1461
   116
        [
clasohm@1461
   117
        (cut_facts_tac prems 1),
clasohm@1461
   118
        (rtac exI 1),
clasohm@1461
   119
        (etac lub_fun 1)
clasohm@1461
   120
        ]);