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