src/HOLCF/fun2.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 243 c22b85994e17
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 (* ------------------------------------------------------------------------ *)
    12 (* Type 'a::term => 'b::pcpo is pointed                                     *)
    13 (* ------------------------------------------------------------------------ *)
    14 
    15 val minimal_fun = prove_goalw  Fun2.thy [UU_fun_def] "UU_fun << f"
    16 (fn prems =>
    17 	[
    18 	(rtac (inst_fun_po RS ssubst) 1),
    19 	(rewrite_goals_tac [less_fun_def]),
    20 	(fast_tac (HOL_cs addSIs [minimal]) 1)
    21 	]);
    22 
    23 (* ------------------------------------------------------------------------ *)
    24 (* make the symbol << accessible for type fun                               *)
    25 (* ------------------------------------------------------------------------ *)
    26 
    27 val less_fun = prove_goal  Fun2.thy  "(f1 << f2) = (! x. f1(x) << f2(x))"
    28 (fn prems =>
    29 	[
    30 	(rtac (inst_fun_po RS ssubst) 1),
    31 	(fold_goals_tac [less_fun_def]),
    32 	(rtac refl 1)
    33 	]);
    34 
    35 (* ------------------------------------------------------------------------ *)
    36 (* chains of functions yield chains in the po range                         *)
    37 (* ------------------------------------------------------------------------ *)
    38 
    39 val ch2ch_fun = prove_goal  Fun2.thy 
    40 	"is_chain(S::nat=>('a::term => 'b::po)) ==> is_chain(% i.S(i)(x))"
    41 (fn prems =>
    42 	[
    43 	(cut_facts_tac prems 1),
    44 	(rewrite_goals_tac [is_chain]),
    45 	(rtac allI 1),
    46 	(rtac spec 1),
    47 	(rtac (less_fun RS subst) 1),
    48 	(etac allE 1),
    49 	(atac 1)
    50 	]);
    51 
    52 (* ------------------------------------------------------------------------ *)
    53 (* upper bounds of function chains yield upper bound in the po range        *)
    54 (* ------------------------------------------------------------------------ *)
    55 
    56 val ub2ub_fun = prove_goal Fun2.thy 
    57    " range(S::nat=>('a::term => 'b::po)) <| u ==> range(%i. S(i,x)) <| u(x)"
    58 (fn prems =>
    59 	[
    60 	(cut_facts_tac prems 1),
    61 	(rtac ub_rangeI 1),
    62 	(rtac allI 1),
    63 	(rtac allE 1),
    64 	(rtac (less_fun RS subst) 1),
    65 	(etac (ub_rangeE RS spec) 1),
    66 	(atac 1)
    67 	]);
    68 
    69 (* ------------------------------------------------------------------------ *)
    70 (* Type 'a::term => 'b::pcpo is chain complete                              *)
    71 (* ------------------------------------------------------------------------ *)
    72 
    73 val lub_fun = prove_goal  Fun2.thy
    74 	"is_chain(S::nat=>('a::term => 'b::pcpo)) ==> \
    75 \        range(S) <<| (% x.lub(range(% i.S(i)(x))))"
    76 (fn prems =>
    77 	[
    78 	(cut_facts_tac prems 1),
    79 	(rtac is_lubI 1),
    80 	(rtac conjI 1),
    81 	(rtac ub_rangeI 1),
    82 	(rtac allI 1),
    83 	(rtac (less_fun RS ssubst) 1),
    84 	(rtac allI 1),
    85 	(rtac is_ub_thelub 1),
    86 	(etac ch2ch_fun 1),
    87 	(strip_tac 1),
    88 	(rtac (less_fun RS ssubst) 1),
    89 	(rtac allI 1),
    90 	(rtac is_lub_thelub 1),
    91 	(etac ch2ch_fun 1),
    92 	(etac ub2ub_fun 1)
    93 	]);
    94 
    95 val thelub_fun = (lub_fun RS thelubI);
    96 (* is_chain(?S1) ==> lub(range(?S1)) = (%x. lub(range(%i. ?S1(i,x)))) *)
    97 
    98 val cpo_fun = prove_goal  Fun2.thy
    99 	"is_chain(S::nat=>('a::term => 'b::pcpo)) ==> ? x. range(S) <<| x"
   100 (fn prems =>
   101 	[
   102 	(cut_facts_tac prems 1),
   103 	(rtac exI 1),
   104 	(etac lub_fun 1)
   105 	]);
   106