396 |> Datatype_Aux.split_conj_thm |
396 |> Datatype_Aux.split_conj_thm |
397 |> map (fn th => zero_var_indexes (th RS mp)) |
397 |> map (fn th => zero_var_indexes (th RS mp)) |
398 end |
398 end |
399 |
399 |
400 |
400 |
|
401 |
401 (** transitivity proof for alphas **) |
402 (** transitivity proof for alphas **) |
402 |
403 |
|
404 fun ecases_tac cases = |
|
405 Subgoal.FOCUS (fn {prems, ...} => |
|
406 HEADGOAL (resolve_tac cases THEN' rtac (List.last prems))) |
|
407 |
|
408 fun aatac pred_names = |
|
409 SUBPROOF (fn {prems, context, ...} => |
|
410 HEADGOAL (resolve_tac (map (transform_prem1 context pred_names) prems))) |
|
411 |
|
412 val perm_inst_tac = |
|
413 Subgoal.FOCUS (fn {params, ...} => |
|
414 let |
|
415 val (p, q) = pairself snd (last2 params) |
|
416 val pq_inst = foldl1 (uncurry Thm.capply) [@{cterm "plus::perm => perm => perm"}, p, q] |
|
417 val exi_inst = Drule.instantiate' [SOME (@{ctyp "perm"})] [NONE, SOME pq_inst] @{thm exI} |
|
418 in |
|
419 HEADGOAL (rtac exi_inst) |
|
420 end) |
|
421 |
|
422 fun non_trivial_cases_tac pred_names intros ctxt = |
|
423 let |
|
424 val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def prod_rel.simps} |
|
425 in |
|
426 resolve_tac intros |
|
427 THEN_ALL_NEW (asm_simp_tac HOL_basic_ss THEN' |
|
428 TRY o EVERY' |
|
429 [ etac @{thm exE}, |
|
430 etac @{thm exE}, |
|
431 perm_inst_tac ctxt, |
|
432 resolve_tac @{thms alpha_trans_eqvt}, |
|
433 atac, |
|
434 aatac pred_names ctxt, |
|
435 Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl}, |
|
436 asm_full_simp_tac (HOL_ss addsimps prod_simps) ]) |
|
437 end |
|
438 |
403 fun prove_trans_tac pred_names raw_dt_thms intros induct cases ctxt = |
439 fun prove_trans_tac pred_names raw_dt_thms intros induct cases ctxt = |
404 let |
440 let |
405 val _ = ("induct\n" ^ Syntax.string_of_term ctxt (prop_of induct)) |
441 fun all_cases ctxt = |
406 |
442 asm_full_simp_tac (HOL_basic_ss addsimps raw_dt_thms) |
407 val tac1 = asm_full_simp_tac (HOL_basic_ss addsimps raw_dt_thms) |
443 THEN' TRY o non_trivial_cases_tac pred_names intros ctxt |
408 fun tac i = (EVERY' [rtac @{thm allI}, rtac @{thm impI}, rotate_tac ~1, |
444 in |
409 etac (nth cases i) THEN_ALL_NEW tac1]) i |
445 HEADGOAL (rtac induct THEN_ALL_NEW |
410 in |
446 EVERY' [ rtac @{thm allI}, rtac @{thm impI}, |
411 HEADGOAL (rtac induct THEN_ALL_NEW tac) |
447 ecases_tac cases ctxt THEN_ALL_NEW all_cases ctxt ]) |
412 end |
448 end |
413 |
449 |
414 fun prep_trans_goal alpha_trm ((arg1, arg2), arg_ty) = |
450 xfun prep_trans_goal alpha_trm ((arg1, arg2), arg_ty) = |
415 let |
451 let |
416 val lhs = alpha_trm $ arg1 $ arg2 |
452 val lhs = alpha_trm $ arg1 $ arg2 |
417 val mid = alpha_trm $ arg2 $ (Bound 0) |
453 val mid = alpha_trm $ arg2 $ (Bound 0) |
418 val rhs = alpha_trm $ arg1 $ (Bound 0) |
454 val rhs = alpha_trm $ arg1 $ (Bound 0) |
419 in |
455 in |
420 HOLogic.mk_imp (lhs, |
456 HOLogic.mk_imp (lhs, |
421 HOLogic.all_const arg_ty $ Abs ("z", arg_ty, |
457 HOLogic.all_const arg_ty $ Abs ("z", arg_ty, |
422 HOLogic.mk_imp (mid, rhs))) |
458 HOLogic.mk_imp (mid, rhs))) |
423 end |
459 end |
|
460 |
|
461 val norm = @{lemma "A --> (!x. B x --> C x) ==> (!!x. [|A; B x|] ==> C x)" by simp} |
424 |
462 |
425 fun raw_prove_trans alpha_trms raw_dt_thms alpha_intros alpha_induct alpha_cases ctxt = |
463 fun raw_prove_trans alpha_trms raw_dt_thms alpha_intros alpha_induct alpha_cases ctxt = |
426 let |
464 let |
427 val alpha_names = map (fst o dest_Const) alpha_trms |
465 val alpha_names = map (fst o dest_Const) alpha_trms |
428 val arg_tys = |
466 val arg_tys = |