246 apply (metis COMBK_def al_refl(3)) |
246 apply (metis COMBK_def al_refl(3)) |
247 *) |
247 *) |
248 |
248 |
249 lemma move_quant: "((\<forall>y. \<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>y. \<forall>x. B x y)) \<Longrightarrow> ((\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y))" |
249 lemma move_quant: "((\<forall>y. \<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>y. \<forall>x. B x y)) \<Longrightarrow> ((\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y))" |
250 by auto |
250 by auto |
|
251 |
|
252 lemma [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>P" |
|
253 apply(auto) |
|
254 done |
|
255 |
|
256 lemma test: |
|
257 fixes P Q::"'a \<Rightarrow> bool" |
|
258 and x::"'a" |
|
259 assumes a: "REFL R2" |
|
260 and b: "\<And>f. Q (f x) \<longrightarrow> P (f x)" |
|
261 shows "(Ball (Respects (R1 ===> R2)) (\<lambda>f. Q (f x)) \<longrightarrow> All (\<lambda>f. P (f x)))" |
|
262 apply(rule impI) |
|
263 apply(rule allI) |
|
264 apply(drule_tac x="\<lambda>y. f x" in bspec) |
|
265 apply(simp add: Respects_def IN_RESPECTS) |
|
266 apply(rule impI) |
|
267 using a |
|
268 apply(simp add: REFL_def) |
|
269 using b |
|
270 apply(simp) |
|
271 done |
251 |
272 |
252 lemma "\<lbrakk>P1 TYP TYP; \<And>A A' K K' x. \<lbrakk>(A::TY) = A'; P2 A A'; (K::KIND) = K'; P1 K K'\<rbrakk> \<Longrightarrow> P1 (KPI A x K) (KPI A' x K'); |
273 lemma "\<lbrakk>P1 TYP TYP; \<And>A A' K K' x. \<lbrakk>(A::TY) = A'; P2 A A'; (K::KIND) = K'; P1 K K'\<rbrakk> \<Longrightarrow> P1 (KPI A x K) (KPI A' x K'); |
253 \<And>A A' K x x' K'. |
274 \<And>A A' K x x' K'. |
254 \<lbrakk>(A ::TY) = A'; P2 A A'; (K :: KIND) = ([(x, x')] \<bullet> K'); P1 K ([(x, x')] \<bullet> K'); x \<notin> FV_ty A'; x \<notin> FV_kind K' - {x'}\<rbrakk> |
275 \<lbrakk>(A ::TY) = A'; P2 A A'; (K :: KIND) = ([(x, x')] \<bullet> K'); P1 K ([(x, x')] \<bullet> K'); x \<notin> FV_ty A'; x \<notin> FV_kind K' - {x'}\<rbrakk> |
255 \<Longrightarrow> P1 (KPI A x K) (KPI A' x' K'); |
276 \<Longrightarrow> P1 (KPI A x K) (KPI A' x' K'); |
271 apply(tactic {* (simp_tac ((Simplifier.context @{context} empty_ss) addsimps (subs1))) 1 *}) |
292 apply(tactic {* (simp_tac ((Simplifier.context @{context} empty_ss) addsimps (subs1))) 1 *}) |
272 apply(atomize (full)) |
293 apply(atomize (full)) |
273 apply(rule RIGHT_RES_FORALL_REGULAR) |
294 apply(rule RIGHT_RES_FORALL_REGULAR) |
274 apply(rule RIGHT_RES_FORALL_REGULAR) |
295 apply(rule RIGHT_RES_FORALL_REGULAR) |
275 apply(rule RIGHT_RES_FORALL_REGULAR) |
296 apply(rule RIGHT_RES_FORALL_REGULAR) |
276 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
297 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+ |
277 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
298 apply(rule test) |
278 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
299 defer |
279 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
300 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+ |
280 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
301 apply(rule test) |
281 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
302 defer |
282 apply(rule Set.imp_mono) |
303 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+ |
|
304 apply(rule move_quant) |
|
305 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+ |
|
306 apply(rule move_quant) |
|
307 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+ |
|
308 apply(rule move_quant) |
|
309 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+ |
|
310 apply(rule test) |
|
311 defer |
|
312 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+ |
|
313 |
|
314 |
|
315 thm test[OF mp] |
|
316 |
|
317 |
|
318 prefer 2 |
|
319 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+ |
|
320 apply(thin_tac "Respects (akind ===> akind ===> op =) x") |
|
321 apply(thin_tac "Respects (aty ===> aty ===> op =) xa") |
|
322 apply(thin_tac "Respects (atrm ===> atrm ===> op =) xb") |
|
323 apply (simp add: Ball_def IN_RESPECTS Respects_def) |
|
324 apply (metis COMBK_def al_refl(3)) |
|
325 |
|
326 apply(rule LEFT_RES_FORALL_REGULAR) |
|
327 apply(rule conjI) |
|
328 prefer 2 |
|
329 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+ |
|
330 using al_refl |
|
331 apply(simp add: Respects_def) |
|
332 |
|
333 |
|
334 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
335 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
336 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
337 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
338 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
339 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
340 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
341 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
342 apply (simp add: Ball_def IN_RESPECTS Respects_def) |
|
343 apply (metis COMBK_def al_refl(3)) |
|
344 |
283 apply(rule impI) apply(assumption) |
345 apply(rule impI) apply(assumption) |
284 apply(rule Set.imp_mono) |
346 apply(rule Set.imp_mono) |
285 apply(rule impI) apply(assumption) |
347 apply(rule impI) apply(assumption) |
286 apply(rule Set.imp_mono) |
348 apply(rule Set.imp_mono) |
287 apply(rule impI) apply(assumption) |
349 apply(rule impI) apply(assumption) |