37 (* ------------------------------------------------------------------------ *) |
37 (* ------------------------------------------------------------------------ *) |
38 (* the << relation between two chains is preserved by their lubs *) |
38 (* the << relation between two chains is preserved by their lubs *) |
39 (* ------------------------------------------------------------------------ *) |
39 (* ------------------------------------------------------------------------ *) |
40 |
40 |
41 qed_goal "lub_mono" Pcpo.thy |
41 qed_goal "lub_mono" Pcpo.thy |
42 "[|is_chain(C1::(nat=>'a::pcpo));is_chain(C2); ! k. C1(k) << C2(k)|]\ |
42 "[|is_chain(C1::(nat=>'a::pcpo));is_chain(C2); ! k. C1(k) << C2(k)|]\ |
43 \ ==> lub(range(C1)) << lub(range(C2))" |
43 \ ==> lub(range(C1)) << lub(range(C2))" |
44 (fn prems => |
44 (fn prems => |
45 [ |
45 [ |
46 (cut_facts_tac prems 1), |
46 (cut_facts_tac prems 1), |
47 (etac is_lub_thelub 1), |
47 (etac is_lub_thelub 1), |
48 (rtac ub_rangeI 1), |
48 (rtac ub_rangeI 1), |
49 (rtac allI 1), |
49 (rtac allI 1), |
50 (rtac trans_less 1), |
50 (rtac trans_less 1), |
51 (etac spec 1), |
51 (etac spec 1), |
52 (etac is_ub_thelub 1) |
52 (etac is_ub_thelub 1) |
53 ]); |
53 ]); |
54 |
54 |
55 (* ------------------------------------------------------------------------ *) |
55 (* ------------------------------------------------------------------------ *) |
56 (* the = relation between two chains is preserved by their lubs *) |
56 (* the = relation between two chains is preserved by their lubs *) |
57 (* ------------------------------------------------------------------------ *) |
57 (* ------------------------------------------------------------------------ *) |
58 |
58 |
59 qed_goal "lub_equal" Pcpo.thy |
59 qed_goal "lub_equal" Pcpo.thy |
60 "[| is_chain(C1::(nat=>'a::pcpo));is_chain(C2);!k.C1(k)=C2(k)|]\ |
60 "[| is_chain(C1::(nat=>'a::pcpo));is_chain(C2);!k.C1(k)=C2(k)|]\ |
61 \ ==> lub(range(C1))=lub(range(C2))" |
61 \ ==> lub(range(C1))=lub(range(C2))" |
62 (fn prems => |
62 (fn prems => |
63 [ |
63 [ |
64 (cut_facts_tac prems 1), |
64 (cut_facts_tac prems 1), |
65 (rtac antisym_less 1), |
65 (rtac antisym_less 1), |
66 (rtac lub_mono 1), |
66 (rtac lub_mono 1), |
67 (atac 1), |
67 (atac 1), |
68 (atac 1), |
68 (atac 1), |
69 (strip_tac 1), |
69 (strip_tac 1), |
70 (rtac (antisym_less_inverse RS conjunct1) 1), |
70 (rtac (antisym_less_inverse RS conjunct1) 1), |
71 (etac spec 1), |
71 (etac spec 1), |
72 (rtac lub_mono 1), |
72 (rtac lub_mono 1), |
73 (atac 1), |
73 (atac 1), |
74 (atac 1), |
74 (atac 1), |
75 (strip_tac 1), |
75 (strip_tac 1), |
76 (rtac (antisym_less_inverse RS conjunct2) 1), |
76 (rtac (antisym_less_inverse RS conjunct2) 1), |
77 (etac spec 1) |
77 (etac spec 1) |
78 ]); |
78 ]); |
79 |
79 |
80 (* ------------------------------------------------------------------------ *) |
80 (* ------------------------------------------------------------------------ *) |
81 (* more results about mono and = of lubs of chains *) |
81 (* more results about mono and = of lubs of chains *) |
82 (* ------------------------------------------------------------------------ *) |
82 (* ------------------------------------------------------------------------ *) |
83 |
83 |
84 qed_goal "lub_mono2" Pcpo.thy |
84 qed_goal "lub_mono2" Pcpo.thy |
85 "[|? j.!i. j<i --> X(i::nat)=Y(i);is_chain(X::nat=>'a::pcpo);is_chain(Y)|]\ |
85 "[|? j.!i. j<i --> X(i::nat)=Y(i);is_chain(X::nat=>'a::pcpo);is_chain(Y)|]\ |
86 \ ==> lub(range(X))<<lub(range(Y))" |
86 \ ==> lub(range(X))<<lub(range(Y))" |
87 (fn prems => |
87 (fn prems => |
88 [ |
88 [ |
89 (rtac exE 1), |
89 (rtac exE 1), |
90 (resolve_tac prems 1), |
90 (resolve_tac prems 1), |
91 (rtac is_lub_thelub 1), |
91 (rtac is_lub_thelub 1), |
92 (resolve_tac prems 1), |
92 (resolve_tac prems 1), |
93 (rtac ub_rangeI 1), |
93 (rtac ub_rangeI 1), |
94 (strip_tac 1), |
94 (strip_tac 1), |
95 (res_inst_tac [("Q","x<i")] classical2 1), |
95 (res_inst_tac [("Q","x<i")] classical2 1), |
96 (res_inst_tac [("s","Y(i)"),("t","X(i)")] subst 1), |
96 (res_inst_tac [("s","Y(i)"),("t","X(i)")] subst 1), |
97 (rtac sym 1), |
97 (rtac sym 1), |
98 (fast_tac HOL_cs 1), |
98 (fast_tac HOL_cs 1), |
99 (rtac is_ub_thelub 1), |
99 (rtac is_ub_thelub 1), |
100 (resolve_tac prems 1), |
100 (resolve_tac prems 1), |
101 (res_inst_tac [("y","X(Suc(x))")] trans_less 1), |
101 (res_inst_tac [("y","X(Suc(x))")] trans_less 1), |
102 (rtac (chain_mono RS mp) 1), |
102 (rtac (chain_mono RS mp) 1), |
103 (resolve_tac prems 1), |
103 (resolve_tac prems 1), |
104 (rtac (not_less_eq RS subst) 1), |
104 (rtac (not_less_eq RS subst) 1), |
105 (atac 1), |
105 (atac 1), |
106 (res_inst_tac [("s","Y(Suc(x))"),("t","X(Suc(x))")] subst 1), |
106 (res_inst_tac [("s","Y(Suc(x))"),("t","X(Suc(x))")] subst 1), |
107 (rtac sym 1), |
107 (rtac sym 1), |
108 (Asm_simp_tac 1), |
108 (Asm_simp_tac 1), |
109 (rtac is_ub_thelub 1), |
109 (rtac is_ub_thelub 1), |
110 (resolve_tac prems 1) |
110 (resolve_tac prems 1) |
111 ]); |
111 ]); |
112 |
112 |
113 qed_goal "lub_equal2" Pcpo.thy |
113 qed_goal "lub_equal2" Pcpo.thy |
114 "[|? j.!i. j<i --> X(i)=Y(i);is_chain(X::nat=>'a::pcpo);is_chain(Y)|]\ |
114 "[|? j.!i. j<i --> X(i)=Y(i);is_chain(X::nat=>'a::pcpo);is_chain(Y)|]\ |
115 \ ==> lub(range(X))=lub(range(Y))" |
115 \ ==> lub(range(X))=lub(range(Y))" |
116 (fn prems => |
116 (fn prems => |
117 [ |
117 [ |
118 (rtac antisym_less 1), |
118 (rtac antisym_less 1), |
119 (rtac lub_mono2 1), |
119 (rtac lub_mono2 1), |
120 (REPEAT (resolve_tac prems 1)), |
120 (REPEAT (resolve_tac prems 1)), |
121 (cut_facts_tac prems 1), |
121 (cut_facts_tac prems 1), |
122 (rtac lub_mono2 1), |
122 (rtac lub_mono2 1), |
123 (safe_tac HOL_cs), |
123 (safe_tac HOL_cs), |
124 (step_tac HOL_cs 1), |
124 (step_tac HOL_cs 1), |
125 (safe_tac HOL_cs), |
125 (safe_tac HOL_cs), |
126 (rtac sym 1), |
126 (rtac sym 1), |
127 (fast_tac HOL_cs 1) |
127 (fast_tac HOL_cs 1) |
128 ]); |
128 ]); |
129 |
129 |
130 qed_goal "lub_mono3" Pcpo.thy "[|is_chain(Y::nat=>'a::pcpo);is_chain(X);\ |
130 qed_goal "lub_mono3" Pcpo.thy "[|is_chain(Y::nat=>'a::pcpo);is_chain(X);\ |
131 \! i. ? j. Y(i)<< X(j)|]==> lub(range(Y))<<lub(range(X))" |
131 \! i. ? j. Y(i)<< X(j)|]==> lub(range(Y))<<lub(range(X))" |
132 (fn prems => |
132 (fn prems => |
133 [ |
133 [ |
134 (cut_facts_tac prems 1), |
134 (cut_facts_tac prems 1), |
135 (rtac is_lub_thelub 1), |
135 (rtac is_lub_thelub 1), |
136 (atac 1), |
136 (atac 1), |
137 (rtac ub_rangeI 1), |
137 (rtac ub_rangeI 1), |
138 (strip_tac 1), |
138 (strip_tac 1), |
139 (etac allE 1), |
139 (etac allE 1), |
140 (etac exE 1), |
140 (etac exE 1), |
141 (rtac trans_less 1), |
141 (rtac trans_less 1), |
142 (rtac is_ub_thelub 2), |
142 (rtac is_ub_thelub 2), |
143 (atac 2), |
143 (atac 2), |
144 (atac 1) |
144 (atac 1) |
145 ]); |
145 ]); |
146 |
146 |
147 (* ------------------------------------------------------------------------ *) |
147 (* ------------------------------------------------------------------------ *) |
148 (* usefull lemmas about UU *) |
148 (* usefull lemmas about UU *) |
149 (* ------------------------------------------------------------------------ *) |
149 (* ------------------------------------------------------------------------ *) |
150 |
150 |
151 qed_goal "eq_UU_iff" Pcpo.thy "(x=UU)=(x<<UU)" |
151 qed_goal "eq_UU_iff" Pcpo.thy "(x=UU)=(x<<UU)" |
152 (fn prems => |
152 (fn prems => |
153 [ |
153 [ |
154 (rtac iffI 1), |
154 (rtac iffI 1), |
155 (hyp_subst_tac 1), |
155 (hyp_subst_tac 1), |
156 (rtac refl_less 1), |
156 (rtac refl_less 1), |
157 (rtac antisym_less 1), |
157 (rtac antisym_less 1), |
158 (atac 1), |
158 (atac 1), |
159 (rtac minimal 1) |
159 (rtac minimal 1) |
160 ]); |
160 ]); |
161 |
161 |
162 qed_goal "UU_I" Pcpo.thy "x << UU ==> x = UU" |
162 qed_goal "UU_I" Pcpo.thy "x << UU ==> x = UU" |
163 (fn prems => |
163 (fn prems => |
164 [ |
164 [ |
165 (rtac (eq_UU_iff RS ssubst) 1), |
165 (rtac (eq_UU_iff RS ssubst) 1), |
166 (resolve_tac prems 1) |
166 (resolve_tac prems 1) |
167 ]); |
167 ]); |
168 |
168 |
169 qed_goal "not_less2not_eq" Pcpo.thy "~x<<y ==> ~x=y" |
169 qed_goal "not_less2not_eq" Pcpo.thy "~x<<y ==> ~x=y" |
170 (fn prems => |
170 (fn prems => |
171 [ |
171 [ |
172 (cut_facts_tac prems 1), |
172 (cut_facts_tac prems 1), |
173 (rtac classical3 1), |
173 (rtac classical3 1), |
174 (atac 1), |
174 (atac 1), |
175 (hyp_subst_tac 1), |
175 (hyp_subst_tac 1), |
176 (rtac refl_less 1) |
176 (rtac refl_less 1) |
177 ]); |
177 ]); |
178 |
178 |
179 qed_goal "chain_UU_I" Pcpo.thy |
179 qed_goal "chain_UU_I" Pcpo.thy |
180 "[|is_chain(Y);lub(range(Y))=UU|] ==> ! i.Y(i)=UU" |
180 "[|is_chain(Y);lub(range(Y))=UU|] ==> ! i.Y(i)=UU" |
181 (fn prems => |
181 (fn prems => |
182 [ |
182 [ |
183 (cut_facts_tac prems 1), |
183 (cut_facts_tac prems 1), |
184 (rtac allI 1), |
184 (rtac allI 1), |
185 (rtac antisym_less 1), |
185 (rtac antisym_less 1), |
186 (rtac minimal 2), |
186 (rtac minimal 2), |
187 (etac subst 1), |
187 (etac subst 1), |
188 (etac is_ub_thelub 1) |
188 (etac is_ub_thelub 1) |
189 ]); |
189 ]); |
190 |
190 |
191 |
191 |
192 qed_goal "chain_UU_I_inverse" Pcpo.thy |
192 qed_goal "chain_UU_I_inverse" Pcpo.thy |
193 "!i.Y(i::nat)=UU ==> lub(range(Y::(nat=>'a::pcpo)))=UU" |
193 "!i.Y(i::nat)=UU ==> lub(range(Y::(nat=>'a::pcpo)))=UU" |
194 (fn prems => |
194 (fn prems => |
195 [ |
195 [ |
196 (cut_facts_tac prems 1), |
196 (cut_facts_tac prems 1), |
197 (rtac lub_chain_maxelem 1), |
197 (rtac lub_chain_maxelem 1), |
198 (rtac exI 1), |
198 (rtac exI 1), |
199 (etac spec 1), |
199 (etac spec 1), |
200 (rtac allI 1), |
200 (rtac allI 1), |
201 (rtac (antisym_less_inverse RS conjunct1) 1), |
201 (rtac (antisym_less_inverse RS conjunct1) 1), |
202 (etac spec 1) |
202 (etac spec 1) |
203 ]); |
203 ]); |
204 |
204 |
205 qed_goal "chain_UU_I_inverse2" Pcpo.thy |
205 qed_goal "chain_UU_I_inverse2" Pcpo.thy |
206 "~lub(range(Y::(nat=>'a::pcpo)))=UU ==> ? i.~ Y(i)=UU" |
206 "~lub(range(Y::(nat=>'a::pcpo)))=UU ==> ? i.~ Y(i)=UU" |
207 (fn prems => |
207 (fn prems => |
208 [ |
208 [ |
209 (cut_facts_tac prems 1), |
209 (cut_facts_tac prems 1), |
210 (rtac (notall2ex RS iffD1) 1), |
210 (rtac (notall2ex RS iffD1) 1), |
211 (rtac swap 1), |
211 (rtac swap 1), |
212 (rtac chain_UU_I_inverse 2), |
212 (rtac chain_UU_I_inverse 2), |
213 (etac notnotD 2), |
213 (etac notnotD 2), |
214 (atac 1) |
214 (atac 1) |
215 ]); |
215 ]); |
216 |
216 |
217 |
217 |
218 qed_goal "notUU_I" Pcpo.thy "[| x<<y; ~x=UU |] ==> ~y=UU" |
218 qed_goal "notUU_I" Pcpo.thy "[| x<<y; ~x=UU |] ==> ~y=UU" |
219 (fn prems => |
219 (fn prems => |
220 [ |
220 [ |
221 (cut_facts_tac prems 1), |
221 (cut_facts_tac prems 1), |
222 (etac contrapos 1), |
222 (etac contrapos 1), |
223 (rtac UU_I 1), |
223 (rtac UU_I 1), |
224 (hyp_subst_tac 1), |
224 (hyp_subst_tac 1), |
225 (atac 1) |
225 (atac 1) |
226 ]); |
226 ]); |
227 |
227 |
228 |
228 |
229 qed_goal "chain_mono2" Pcpo.thy |
229 qed_goal "chain_mono2" Pcpo.thy |
230 "[|? j.~Y(j)=UU;is_chain(Y::nat=>'a::pcpo)|]\ |
230 "[|? j.~Y(j)=UU;is_chain(Y::nat=>'a::pcpo)|]\ |
231 \ ==> ? j.!i.j<i-->~Y(i)=UU" |
231 \ ==> ? j.!i.j<i-->~Y(i)=UU" |
232 (fn prems => |
232 (fn prems => |
233 [ |
233 [ |
234 (cut_facts_tac prems 1), |
234 (cut_facts_tac prems 1), |
235 (safe_tac HOL_cs), |
235 (safe_tac HOL_cs), |
236 (step_tac HOL_cs 1), |
236 (step_tac HOL_cs 1), |
237 (strip_tac 1), |
237 (strip_tac 1), |
238 (rtac notUU_I 1), |
238 (rtac notUU_I 1), |
239 (atac 2), |
239 (atac 2), |
240 (etac (chain_mono RS mp) 1), |
240 (etac (chain_mono RS mp) 1), |
241 (atac 1) |
241 (atac 1) |
242 ]); |
242 ]); |
243 |
243 |
244 |
244 |
245 |
245 |
246 |
246 |
247 (* ------------------------------------------------------------------------ *) |
247 (* ------------------------------------------------------------------------ *) |
248 (* uniqueness in void *) |
248 (* uniqueness in void *) |
249 (* ------------------------------------------------------------------------ *) |
249 (* ------------------------------------------------------------------------ *) |
250 |
250 |
251 qed_goal "unique_void2" Pcpo.thy "(x::void)=UU" |
251 qed_goal "unique_void2" Pcpo.thy "(x::void)=UU" |
252 (fn prems => |
252 (fn prems => |
253 [ |
253 [ |
254 (rtac (inst_void_pcpo RS ssubst) 1), |
254 (rtac (inst_void_pcpo RS ssubst) 1), |
255 (rtac (Rep_Void_inverse RS subst) 1), |
255 (rtac (Rep_Void_inverse RS subst) 1), |
256 (rtac (Rep_Void_inverse RS subst) 1), |
256 (rtac (Rep_Void_inverse RS subst) 1), |
257 (rtac arg_cong 1), |
257 (rtac arg_cong 1), |
258 (rtac box_equals 1), |
258 (rtac box_equals 1), |
259 (rtac refl 1), |
259 (rtac refl 1), |
260 (rtac (unique_void RS sym) 1), |
260 (rtac (unique_void RS sym) 1), |
261 (rtac (unique_void RS sym) 1) |
261 (rtac (unique_void RS sym) 1) |
262 ]); |
262 ]); |
263 |
263 |
264 |
264 |