261 val pat = [@{term "Ball (Respects (R1 ===> R2)) P"}]; |
261 val pat = [@{term "Ball (Respects (R1 ===> R2)) P"}]; |
262 val thy = ProofContext.theory_of ctxt |
262 val thy = ProofContext.theory_of ctxt |
263 val simproc = Simplifier.simproc_i thy "" pat (K (ball_simproc rel_eqvs)) |
263 val simproc = Simplifier.simproc_i thy "" pat (K (ball_simproc rel_eqvs)) |
264 in |
264 in |
265 (ObjectLogic.full_atomize_tac) THEN' |
265 (ObjectLogic.full_atomize_tac) THEN' |
266 (simp_tac (((Simplifier.context ctxt empty_ss) addsimps subs) addsimprocs [simproc])) |
266 (simp_tac (((Simplifier.context ctxt empty_ss) addsimps subs) addsimprocs [simproc])) THEN' |
267 THEN' |
|
268 REPEAT_ALL_NEW (FIRST' [ |
267 REPEAT_ALL_NEW (FIRST' [ |
269 (rtac @{thm RIGHT_RES_FORALL_REGULAR}), |
268 (rtac @{thm RIGHT_RES_FORALL_REGULAR}), |
270 (rtac @{thm LEFT_RES_EXISTS_REGULAR}), |
269 (rtac @{thm LEFT_RES_EXISTS_REGULAR}), |
271 (rtac @{thm left_ball_regular} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])), |
270 (rtac @{thm left_ball_regular} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])), |
272 (rtac @{thm right_bex_regular} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])), |
271 (rtac @{thm right_bex_regular} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])), |
273 (rtac @{thm ball_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])), |
272 (rtac @{thm ball_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])), |
274 (rtac @{thm bex_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])), |
273 (rtac @{thm bex_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])), |
275 (resolve_tac (Inductive.get_monos ctxt)), |
274 (resolve_tac (Inductive.get_monos ctxt)), |
276 rtac @{thm move_forall}, |
275 rtac @{thm move_forall}, |
277 rtac @{thm move_exists} |
276 rtac @{thm move_exists}, |
|
277 (simp_tac (((Simplifier.context ctxt empty_ss) addsimps subs) addsimprocs [simproc])) |
278 ]) |
278 ]) |
279 end |
279 end |
280 *} |
280 *} |
281 |
281 |
282 |
282 |
298 \<Longrightarrow> P3 (LAM A x M) (LAM A' x' M')\<rbrakk> |
298 \<Longrightarrow> P3 (LAM A x M) (LAM A' x' M')\<rbrakk> |
299 \<Longrightarrow> ((x1 :: KIND) = x2 \<longrightarrow> P1 x1 x2) \<and> |
299 \<Longrightarrow> ((x1 :: KIND) = x2 \<longrightarrow> P1 x1 x2) \<and> |
300 ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)" |
300 ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)" |
301 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
301 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
302 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
302 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
303 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
304 |
|
305 apply(rule LEFT_RES_FORALL_REGULAR) |
|
306 apply(tactic {* (simp_tac ((Simplifier.context @{context} empty_ss) addsimps (subs1))) 1 *}) |
|
307 apply(atomize (full)) |
|
308 apply(rule RIGHT_RES_FORALL_REGULAR) |
|
309 apply(rule RIGHT_RES_FORALL_REGULAR) |
|
310 apply(rule RIGHT_RES_FORALL_REGULAR) |
|
311 apply(rule test) |
|
312 defer |
|
313 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+ |
|
314 apply(rule test) |
|
315 defer |
|
316 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+ |
|
317 apply(rule move_quant) |
|
318 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+ |
|
319 apply(rule move_quant) |
|
320 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+ |
|
321 apply(rule move_quant) |
|
322 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+ |
|
323 apply(rule test) |
|
324 defer |
|
325 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+ |
|
326 |
|
327 |
|
328 thm test[OF mp] |
|
329 |
|
330 |
|
331 prefer 2 |
303 prefer 2 |
332 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+ |
304 apply(tactic {* r_mk_comb_tac' @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
333 apply(thin_tac "Respects (akind ===> akind ===> op =) x") |
305 apply (tactic {* clean_tac @{context} quot defs reps_same absrep 1 *}) |
334 apply(thin_tac "Respects (aty ===> aty ===> op =) xa") |
|
335 apply(thin_tac "Respects (atrm ===> atrm ===> op =) xb") |
|
336 apply (simp add: Ball_def IN_RESPECTS Respects_def) |
|
337 apply (metis COMBK_def al_refl(3)) |
|
338 |
|
339 apply(rule LEFT_RES_FORALL_REGULAR) |
|
340 apply(rule conjI) |
|
341 prefer 2 |
|
342 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+ |
|
343 using al_refl |
|
344 apply(simp add: Respects_def) |
|
345 |
|
346 |
|
347 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
348 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
349 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
350 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
351 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
352 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
353 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
354 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
355 apply (simp add: Ball_def IN_RESPECTS Respects_def) |
|
356 apply (metis COMBK_def al_refl(3)) |
|
357 |
|
358 apply(rule impI) apply(assumption) |
|
359 apply(rule Set.imp_mono) |
|
360 apply(rule impI) apply(assumption) |
|
361 apply(rule Set.imp_mono) |
|
362 apply(rule impI) apply(assumption) |
|
363 apply(rule Set.imp_mono) |
|
364 apply(rule impI) apply(assumption) |
|
365 apply(rule Set.imp_mono) |
|
366 apply(rule impI) apply(assumption) |
|
367 apply(rule Set.imp_mono) |
|
368 apply(rule impI) apply(assumption) |
|
369 apply(rule Set.imp_mono) |
|
370 apply(rule impI) apply(assumption) |
|
371 apply(rule Set.imp_mono) |
|
372 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
373 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
374 apply (simp add: Ball_def IN_RESPECTS Respects_def) |
|
375 apply (metis COMBK_def al_refl(3)) |
|
376 apply(rule Set.imp_mono) |
|
377 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
378 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
379 apply (simp add: Ball_def IN_RESPECTS Respects_def) |
|
380 apply (metis COMBK_def al_refl(3)) |
|
381 apply(rule Set.imp_mono) |
|
382 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
383 apply(rule move_quant) |
|
384 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
385 apply(rule move_quant) |
|
386 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
387 apply(rule move_quant) |
|
388 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
389 apply (simp add: Ball_def IN_RESPECTS Respects_def) |
|
390 apply (metis COMBK_def al_refl(3)) |
|
391 apply(rule impI) apply(assumption) |
|
392 |
306 |
393 ML {* |
307 ML {* |
394 val rty_qty_rel = |
308 val rty_qty_rel = |
395 [(@{typ kind}, (@{typ KIND}, @{term akind})), |
309 [(@{typ kind}, (@{typ KIND}, @{term akind})), |
396 (@{typ ty}, (@{typ TY}, @{term aty})), |
310 (@{typ ty}, (@{typ TY}, @{term aty})), |