1 (* Title: HOLCF/lift2.ML |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 Lemmas for lift2.thy |
|
7 *) |
|
8 |
|
9 open Lift2; |
|
10 |
|
11 (* -------------------------------------------------------------------------*) |
|
12 (* type ('a)u is pointed *) |
|
13 (* ------------------------------------------------------------------------ *) |
|
14 |
|
15 qed_goal "minimal_lift" Lift2.thy "UU_lift << z" |
|
16 (fn prems => |
|
17 [ |
|
18 (stac inst_lift_po 1), |
|
19 (rtac less_lift1a 1) |
|
20 ]); |
|
21 |
|
22 (* -------------------------------------------------------------------------*) |
|
23 (* access to less_lift in class po *) |
|
24 (* ------------------------------------------------------------------------ *) |
|
25 |
|
26 qed_goal "less_lift2b" Lift2.thy "~ Iup(x) << UU_lift" |
|
27 (fn prems => |
|
28 [ |
|
29 (stac inst_lift_po 1), |
|
30 (rtac less_lift1b 1) |
|
31 ]); |
|
32 |
|
33 qed_goal "less_lift2c" Lift2.thy "(Iup(x)<<Iup(y)) = (x<<y)" |
|
34 (fn prems => |
|
35 [ |
|
36 (stac inst_lift_po 1), |
|
37 (rtac less_lift1c 1) |
|
38 ]); |
|
39 |
|
40 (* ------------------------------------------------------------------------ *) |
|
41 (* Iup and Ilift are monotone *) |
|
42 (* ------------------------------------------------------------------------ *) |
|
43 |
|
44 qed_goalw "monofun_Iup" Lift2.thy [monofun] "monofun(Iup)" |
|
45 (fn prems => |
|
46 [ |
|
47 (strip_tac 1), |
|
48 (etac (less_lift2c RS iffD2) 1) |
|
49 ]); |
|
50 |
|
51 qed_goalw "monofun_Ilift1" Lift2.thy [monofun] "monofun(Ilift)" |
|
52 (fn prems => |
|
53 [ |
|
54 (strip_tac 1), |
|
55 (rtac (less_fun RS iffD2) 1), |
|
56 (strip_tac 1), |
|
57 (res_inst_tac [("p","xa")] liftE 1), |
|
58 (asm_simp_tac Lift0_ss 1), |
|
59 (asm_simp_tac Lift0_ss 1), |
|
60 (etac monofun_cfun_fun 1) |
|
61 ]); |
|
62 |
|
63 qed_goalw "monofun_Ilift2" Lift2.thy [monofun] "monofun(Ilift(f))" |
|
64 (fn prems => |
|
65 [ |
|
66 (strip_tac 1), |
|
67 (res_inst_tac [("p","x")] liftE 1), |
|
68 (asm_simp_tac Lift0_ss 1), |
|
69 (asm_simp_tac Lift0_ss 1), |
|
70 (res_inst_tac [("p","y")] liftE 1), |
|
71 (hyp_subst_tac 1), |
|
72 (rtac notE 1), |
|
73 (rtac less_lift2b 1), |
|
74 (atac 1), |
|
75 (asm_simp_tac Lift0_ss 1), |
|
76 (rtac monofun_cfun_arg 1), |
|
77 (hyp_subst_tac 1), |
|
78 (etac (less_lift2c RS iffD1) 1) |
|
79 ]); |
|
80 |
|
81 (* ------------------------------------------------------------------------ *) |
|
82 (* Some kind of surjectivity lemma *) |
|
83 (* ------------------------------------------------------------------------ *) |
|
84 |
|
85 |
|
86 qed_goal "lift_lemma1" Lift2.thy "z=Iup(x) ==> Iup(Ilift(LAM x.x)(z)) = z" |
|
87 (fn prems => |
|
88 [ |
|
89 (cut_facts_tac prems 1), |
|
90 (asm_simp_tac Lift0_ss 1) |
|
91 ]); |
|
92 |
|
93 (* ------------------------------------------------------------------------ *) |
|
94 (* ('a)u is a cpo *) |
|
95 (* ------------------------------------------------------------------------ *) |
|
96 |
|
97 qed_goal "lub_lift1a" Lift2.thy |
|
98 "[|is_chain(Y);? i x.Y(i)=Iup(x)|] ==>\ |
|
99 \ range(Y) <<| Iup(lub(range(%i.(Ilift (LAM x.x) (Y(i))))))" |
|
100 (fn prems => |
|
101 [ |
|
102 (cut_facts_tac prems 1), |
|
103 (rtac is_lubI 1), |
|
104 (rtac conjI 1), |
|
105 (rtac ub_rangeI 1), |
|
106 (rtac allI 1), |
|
107 (res_inst_tac [("p","Y(i)")] liftE 1), |
|
108 (res_inst_tac [("s","UU_lift"),("t","Y(i)")] subst 1), |
|
109 (etac sym 1), |
|
110 (rtac minimal_lift 1), |
|
111 (res_inst_tac [("t","Y(i)")] (lift_lemma1 RS subst) 1), |
|
112 (atac 1), |
|
113 (rtac (less_lift2c RS iffD2) 1), |
|
114 (rtac is_ub_thelub 1), |
|
115 (etac (monofun_Ilift2 RS ch2ch_monofun) 1), |
|
116 (strip_tac 1), |
|
117 (res_inst_tac [("p","u")] liftE 1), |
|
118 (etac exE 1), |
|
119 (etac exE 1), |
|
120 (res_inst_tac [("P","Y(i)<<UU_lift")] notE 1), |
|
121 (res_inst_tac [("s","Iup(x)"),("t","Y(i)")] ssubst 1), |
|
122 (atac 1), |
|
123 (rtac less_lift2b 1), |
|
124 (hyp_subst_tac 1), |
|
125 (etac (ub_rangeE RS spec) 1), |
|
126 (res_inst_tac [("t","u")] (lift_lemma1 RS subst) 1), |
|
127 (atac 1), |
|
128 (rtac (less_lift2c RS iffD2) 1), |
|
129 (rtac is_lub_thelub 1), |
|
130 (etac (monofun_Ilift2 RS ch2ch_monofun) 1), |
|
131 (etac (monofun_Ilift2 RS ub2ub_monofun) 1) |
|
132 ]); |
|
133 |
|
134 qed_goal "lub_lift1b" Lift2.thy |
|
135 "[|is_chain(Y);!i x. Y(i)~=Iup(x)|] ==>\ |
|
136 \ range(Y) <<| UU_lift" |
|
137 (fn prems => |
|
138 [ |
|
139 (cut_facts_tac prems 1), |
|
140 (rtac is_lubI 1), |
|
141 (rtac conjI 1), |
|
142 (rtac ub_rangeI 1), |
|
143 (rtac allI 1), |
|
144 (res_inst_tac [("p","Y(i)")] liftE 1), |
|
145 (res_inst_tac [("s","UU_lift"),("t","Y(i)")] ssubst 1), |
|
146 (atac 1), |
|
147 (rtac refl_less 1), |
|
148 (rtac notE 1), |
|
149 (dtac spec 1), |
|
150 (dtac spec 1), |
|
151 (atac 1), |
|
152 (atac 1), |
|
153 (strip_tac 1), |
|
154 (rtac minimal_lift 1) |
|
155 ]); |
|
156 |
|
157 bind_thm ("thelub_lift1a", lub_lift1a RS thelubI); |
|
158 (* |
|
159 [| is_chain ?Y1; ? i x. ?Y1 i = Iup x |] ==> |
|
160 lub (range ?Y1) = Iup (lub (range (%i. Ilift (LAM x. x) (?Y1 i)))) |
|
161 *) |
|
162 |
|
163 bind_thm ("thelub_lift1b", lub_lift1b RS thelubI); |
|
164 (* |
|
165 [| is_chain ?Y1; ! i x. ?Y1 i ~= Iup x |] ==> |
|
166 lub (range ?Y1) = UU_lift |
|
167 *) |
|
168 |
|
169 qed_goal "cpo_lift" Lift2.thy |
|
170 "is_chain(Y::nat=>('a)u) ==> ? x.range(Y) <<|x" |
|
171 (fn prems => |
|
172 [ |
|
173 (cut_facts_tac prems 1), |
|
174 (rtac disjE 1), |
|
175 (rtac exI 2), |
|
176 (etac lub_lift1a 2), |
|
177 (atac 2), |
|
178 (rtac exI 2), |
|
179 (etac lub_lift1b 2), |
|
180 (atac 2), |
|
181 (fast_tac HOL_cs 1) |
|
182 ]); |
|
183 |
|