|
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 |
|