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;
     1 (*  Title:      HOLCF/fun2.ML
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Lemmas for fun2.thy 
     7 *)
     8 
     9 open Fun2;
    10 
    11 (* for compatibility with old HOLCF-Version *)
    12 qed_goal "inst_fun_po" thy "(op <<)=(%f g.!x. f x << g x)"
    13  (fn prems => 
    14         [
    15 	(fold_goals_tac [less_fun_def]),
    16 	(rtac refl 1)
    17         ]);
    18 
    19 (* ------------------------------------------------------------------------ *)
    20 (* Type 'a::term => 'b::pcpo is pointed                                     *)
    21 (* ------------------------------------------------------------------------ *)
    22 
    23 qed_goal "minimal_fun" thy "(%z. UU) << x"
    24 (fn prems =>
    25         [
    26         (simp_tac (simpset() addsimps [inst_fun_po,minimal]) 1)
    27         ]);
    28 
    29 bind_thm ("UU_fun_def",minimal_fun RS minimal2UU RS sym);
    30 
    31 qed_goal "least_fun" thy "? x::'a=>'b::pcpo.!y. x<<y"
    32 (fn prems =>
    33         [
    34         (res_inst_tac [("x","(%z. UU)")] exI 1),
    35         (rtac (minimal_fun RS allI) 1)
    36         ]);
    37 
    38 (* ------------------------------------------------------------------------ *)
    39 (* make the symbol << accessible for type fun                               *)
    40 (* ------------------------------------------------------------------------ *)
    41 
    42 qed_goal "less_fun" thy "(f1 << f2) = (! x. f1(x) << f2(x))"
    43 (fn prems =>
    44         [
    45         (stac inst_fun_po 1),
    46         (fold_goals_tac [less_fun_def]),
    47         (rtac refl 1)
    48         ]);
    49 
    50 (* ------------------------------------------------------------------------ *)
    51 (* chains of functions yield chains in the po range                         *)
    52 (* ------------------------------------------------------------------------ *)
    53 
    54 qed_goal "ch2ch_fun" thy 
    55         "chain(S::nat=>('a=>'b::po)) ==> chain(% i. S(i)(x))"
    56 (fn prems =>
    57         [
    58         (cut_facts_tac prems 1),
    59         (rewtac chain),
    60         (rtac allI 1),
    61         (rtac spec 1),
    62         (rtac (less_fun RS subst) 1),
    63         (etac allE 1),
    64         (atac 1)
    65         ]);
    66 
    67 (* ------------------------------------------------------------------------ *)
    68 (* upper bounds of function chains yield upper bound in the po range        *)
    69 (* ------------------------------------------------------------------------ *)
    70 
    71 qed_goal "ub2ub_fun" Fun2.thy 
    72    " range(S::nat=>('a::term => 'b::po)) <| u ==> range(%i. S i x) <| u(x)"
    73 (fn prems =>
    74         [
    75         (cut_facts_tac prems 1),
    76         (rtac ub_rangeI 1),
    77         (rtac allI 1),
    78         (rtac allE 1),
    79         (rtac (less_fun RS subst) 1),
    80         (etac (ub_rangeE RS spec) 1),
    81         (atac 1)
    82         ]);
    83 
    84 (* ------------------------------------------------------------------------ *)
    85 (* Type 'a::term => 'b::pcpo is chain complete                              *)
    86 (* ------------------------------------------------------------------------ *)
    87 
    88 qed_goal "lub_fun"  Fun2.thy
    89         "chain(S::nat=>('a::term => 'b::cpo)) ==> \
    90 \        range(S) <<| (% x. lub(range(% i. S(i)(x))))"
    91 (fn prems =>
    92         [
    93         (cut_facts_tac prems 1),
    94         (rtac is_lubI 1),
    95         (rtac conjI 1),
    96         (rtac ub_rangeI 1),
    97         (rtac allI 1),
    98         (stac less_fun 1),
    99         (rtac allI 1),
   100         (rtac is_ub_thelub 1),
   101         (etac ch2ch_fun 1),
   102         (strip_tac 1),
   103         (stac less_fun 1),
   104         (rtac allI 1),
   105         (rtac is_lub_thelub 1),
   106         (etac ch2ch_fun 1),
   107         (etac ub2ub_fun 1)
   108         ]);
   109 
   110 bind_thm ("thelub_fun", lub_fun RS thelubI);
   111 (* chain ?S1 ==> lub (range ?S1) = (%x. lub (range (%i. ?S1 i x))) *)
   112 
   113 qed_goal "cpo_fun"  Fun2.thy
   114         "chain(S::nat=>('a::term => 'b::cpo)) ==> ? x. range(S) <<| x"
   115 (fn prems =>
   116         [
   117         (cut_facts_tac prems 1),
   118         (rtac exI 1),
   119         (etac lub_fun 1)
   120         ]);