246 |
246 |
247 val all_alpha_names = map (fn (a, ty) => ((Binding.name a, ty), NoSyn)) |
247 val all_alpha_names = map (fn (a, ty) => ((Binding.name a, ty), NoSyn)) |
248 (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys) |
248 (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys) |
249 val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros) |
249 val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros) |
250 |
250 |
251 val (alpha_info, lthy') = Inductive.add_inductive_i |
251 val (alpha_info, lthy') = lthy |
|
252 |> Inductive.add_inductive_i |
252 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
253 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
253 coind = false, no_elim = false, no_ind = false, skip_mono = false} |
254 coind = false, no_elim = false, no_ind = false, skip_mono = false} |
254 all_alpha_names [] all_alpha_intros [] lthy |
255 all_alpha_names [] all_alpha_intros [] |
255 |
256 |
256 val all_alpha_trms_loc = #preds alpha_info; |
257 val all_alpha_trms_loc = #preds alpha_info; |
257 val alpha_raw_induct_loc = #raw_induct alpha_info; |
258 val alpha_raw_induct_loc = #raw_induct alpha_info; |
258 val alpha_intros_loc = #intrs alpha_info; |
259 val alpha_intros_loc = #intrs alpha_info; |
259 val alpha_cases_loc = #elims alpha_info; |
260 val alpha_cases_loc = #elims alpha_info; |
260 val phi = Proof_Context.export_morphism lthy' lthy; |
261 val phi = |
|
262 Proof_Context.export_morphism lthy' |
|
263 (Proof_Context.transfer (Proof_Context.theory_of lthy') lthy); |
261 |
264 |
262 val all_alpha_trms = all_alpha_trms_loc |
265 val all_alpha_trms = all_alpha_trms_loc |
263 |> map (Morphism.term phi) |
266 |> map (Morphism.term phi) |
264 |> map Type.legacy_freeze |
267 |> map Type.legacy_freeze |
265 val alpha_raw_induct = Morphism.thm phi alpha_raw_induct_loc |
268 val alpha_raw_induct = Morphism.thm phi alpha_raw_induct_loc |
311 |> foldr1 HOLogic.mk_conj |
314 |> foldr1 HOLogic.mk_conj |
312 |> HOLogic.mk_Trueprop |
315 |> HOLogic.mk_Trueprop |
313 |
316 |
314 fun tac ctxt = |
317 fun tac ctxt = |
315 HEADGOAL |
318 HEADGOAL |
316 (DETERM o (rtac induct_thm) |
319 (DETERM o (resolve_tac ctxt [induct_thm]) |
317 THEN_ALL_NEW |
320 THEN_ALL_NEW |
318 (REPEAT_ALL_NEW (FIRST' [resolve_tac ctxt @{thms TrueI conjI}, cases_tac ctxt]))) |
321 (REPEAT_ALL_NEW (FIRST' [resolve_tac ctxt @{thms TrueI conjI}, cases_tac ctxt]))) |
319 in |
322 in |
320 Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context) |
323 Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context) |
321 |> singleton (Proof_Context.export ctxt' ctxt) |
324 |> singleton (Proof_Context.export ctxt' ctxt) |
358 |> foldr1 HOLogic.mk_conj |
361 |> foldr1 HOLogic.mk_conj |
359 |> HOLogic.mk_Trueprop |
362 |> HOLogic.mk_Trueprop |
360 |
363 |
361 fun tac ctxt = |
364 fun tac ctxt = |
362 HEADGOAL |
365 HEADGOAL |
363 (DETERM o (rtac alpha_induct_thm) |
366 (DETERM o (resolve_tac ctxt [alpha_induct_thm]) |
364 THEN_ALL_NEW FIRST' [rtac @{thm TrueI}, cases_tac ctxt]) |
367 THEN_ALL_NEW FIRST' [resolve_tac ctxt @{thms TrueI}, cases_tac ctxt]) |
365 in |
368 in |
366 Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context) |
369 Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context) |
367 |> singleton (Proof_Context.export ctxt' ctxt) |
370 |> singleton (Proof_Context.export ctxt' ctxt) |
368 |> Old_Datatype_Aux.split_conj_thm |
371 |> Old_Datatype_Aux.split_conj_thm |
369 |> map (fn th => th RS mp) |
372 |> map (fn th => th RS mp) |
390 |> HOLogic.mk_not |
393 |> HOLogic.mk_not |
391 |> HOLogic.mk_Trueprop |
394 |> HOLogic.mk_Trueprop |
392 end |
395 end |
393 |
396 |
394 fun distinct_tac ctxt cases_thms distinct_thms = |
397 fun distinct_tac ctxt cases_thms distinct_thms = |
395 rtac notI THEN' eresolve_tac ctxt cases_thms |
398 resolve_tac ctxt [notI] THEN' eresolve_tac ctxt cases_thms |
396 THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps distinct_thms) |
399 THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps distinct_thms) |
397 |
400 |
398 fun raw_prove_alpha_distincts ctxt alpha_result raw_dt_info = |
401 fun raw_prove_alpha_distincts ctxt alpha_result raw_dt_info = |
399 let |
402 let |
400 val AlphaResult {alpha_names, alpha_cases, ...} = alpha_result |
403 val AlphaResult {alpha_names, alpha_cases, ...} = alpha_result |
425 @{term "Trueprop"} $ (_ $ Const _ $ Const _) => thm RS @{thm eqTrueI} |
428 @{term "Trueprop"} $ (_ $ Const _ $ Const _) => thm RS @{thm eqTrueI} |
426 | _ => thm |
429 | _ => thm |
427 |
430 |
428 fun alpha_eq_iff_tac ctxt dist_inj intros elims = |
431 fun alpha_eq_iff_tac ctxt dist_inj intros elims = |
429 SOLVED' (asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps intros)) ORELSE' |
432 SOLVED' (asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps intros)) ORELSE' |
430 (rtac @{thm iffI} THEN' |
433 (resolve_tac ctxt @{thms iffI} THEN' |
431 RANGE [eresolve_tac ctxt elims THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps dist_inj), |
434 RANGE [eresolve_tac ctxt elims THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps dist_inj), |
432 asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps intros)]) |
435 asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps intros)]) |
433 |
436 |
434 fun mk_alpha_eq_iff_goal thm = |
437 fun mk_alpha_eq_iff_goal thm = |
435 let |
438 let |
463 |
466 |
464 fun cases_tac intros ctxt = |
467 fun cases_tac intros ctxt = |
465 let |
468 let |
466 val prod_simps = @{thms split_conv prod_alpha_def rel_prod_conv} |
469 val prod_simps = @{thms split_conv prod_alpha_def rel_prod_conv} |
467 |
470 |
468 val unbound_tac = REPEAT o (etac @{thm conjE}) THEN' assume_tac ctxt |
471 val unbound_tac = REPEAT o (eresolve_tac ctxt @{thms conjE}) THEN' assume_tac ctxt |
469 |
472 |
470 val bound_tac = |
473 val bound_tac = |
471 EVERY' [ rtac exi_zero, |
474 EVERY' [ resolve_tac ctxt [exi_zero], |
472 resolve_tac ctxt @{thms alpha_refl}, |
475 resolve_tac ctxt @{thms alpha_refl}, |
473 asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps) ] |
476 asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps) ] |
474 in |
477 in |
475 resolve_tac ctxt intros THEN_ALL_NEW FIRST' [rtac @{thm refl}, unbound_tac, bound_tac] |
478 resolve_tac ctxt intros THEN_ALL_NEW |
|
479 FIRST' [resolve_tac ctxt @{thms refl}, unbound_tac, bound_tac] |
476 end |
480 end |
477 |
481 |
478 fun raw_prove_refl ctxt alpha_result raw_dt_induct = |
482 fun raw_prove_refl ctxt alpha_result raw_dt_induct = |
479 let |
483 let |
480 val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_bn_tys, alpha_intros, ...} = |
484 val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_bn_tys, alpha_intros, ...} = |
496 |
500 |
497 (* for premises that contain binders *) |
501 (* for premises that contain binders *) |
498 fun prem_bound_tac pred_names alpha_eqvt ctxt = |
502 fun prem_bound_tac pred_names alpha_eqvt ctxt = |
499 let |
503 let |
500 fun trans_prem_tac pred_names ctxt = |
504 fun trans_prem_tac pred_names ctxt = |
501 SUBPROOF (fn {prems, context, ...} => |
505 SUBPROOF (fn {prems, context = ctxt', ...} => |
502 let |
506 let |
503 val prems' = map (transform_prem1 context pred_names) prems |
507 val prems' = map (transform_prem1 ctxt' pred_names) prems |
504 in |
508 in |
505 resolve_tac ctxt prems' 1 |
509 resolve_tac ctxt' prems' 1 |
506 end) ctxt |
510 end) ctxt |
507 val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def rel_prod_conv alphas} |
511 val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def rel_prod_conv alphas} |
508 in |
512 in |
509 EVERY' |
513 EVERY' |
510 [ etac exi_neg, |
514 [ eresolve_tac ctxt [exi_neg], |
511 resolve_tac ctxt @{thms alpha_sym_eqvt}, |
515 resolve_tac ctxt @{thms alpha_sym_eqvt}, |
512 asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps), |
516 asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps), |
513 eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' rtac @{thm refl}, |
517 eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' |
|
518 resolve_tac ctxt @{thms refl}, |
514 trans_prem_tac pred_names ctxt] |
519 trans_prem_tac pred_names ctxt] |
515 end |
520 end |
516 |
521 |
517 fun raw_prove_sym ctxt alpha_result alpha_eqvt = |
522 fun raw_prove_sym ctxt alpha_result alpha_eqvt = |
518 let |
523 let |
525 val props = map (fn t => fn (x, y) => t $ y $ x) alpha_trms |
530 val props = map (fn t => fn (x, y) => t $ y $ x) alpha_trms |
526 |
531 |
527 fun tac ctxt = |
532 fun tac ctxt = |
528 resolve_tac ctxt alpha_intros THEN_ALL_NEW |
533 resolve_tac ctxt alpha_intros THEN_ALL_NEW |
529 FIRST' [assume_tac ctxt, |
534 FIRST' [assume_tac ctxt, |
530 rtac @{thm sym} THEN' assume_tac ctxt, |
535 resolve_tac ctxt @{thms sym} THEN' assume_tac ctxt, |
531 prem_bound_tac alpha_names alpha_eqvt ctxt] |
536 prem_bound_tac alpha_names alpha_eqvt ctxt] |
532 in |
537 in |
533 alpha_prove alpha_trms (alpha_trms ~~ props) alpha_raw_induct tac ctxt |
538 alpha_prove alpha_trms (alpha_trms ~~ props) alpha_raw_induct tac ctxt |
534 end |
539 end |
535 |
540 |
537 (** transitivity proof for alphas **) |
542 (** transitivity proof for alphas **) |
538 |
543 |
539 (* applies cases rules and resolves them with the last premise *) |
544 (* applies cases rules and resolves them with the last premise *) |
540 fun ecases_tac cases = |
545 fun ecases_tac cases = |
541 Subgoal.FOCUS (fn {context = ctxt, prems, ...} => |
546 Subgoal.FOCUS (fn {context = ctxt, prems, ...} => |
542 HEADGOAL (resolve_tac ctxt cases THEN' rtac (List.last prems))) |
547 HEADGOAL (resolve_tac ctxt cases THEN' resolve_tac ctxt [List.last prems])) |
543 |
548 |
544 fun aatac pred_names = |
549 fun aatac pred_names = |
545 SUBPROOF (fn {context = ctxt, prems, ...} => |
550 SUBPROOF (fn {context = ctxt, prems, ...} => |
546 HEADGOAL (resolve_tac ctxt (map (transform_prem1 ctxt pred_names) prems))) |
551 HEADGOAL (resolve_tac ctxt (map (transform_prem1 ctxt pred_names) prems))) |
547 |
552 |
548 (* instantiates exI with the permutation p + q *) |
553 (* instantiates exI with the permutation p + q *) |
549 val perm_inst_tac = |
554 val perm_inst_tac = |
550 Subgoal.FOCUS (fn {params, ...} => |
555 Subgoal.FOCUS (fn {context = ctxt, params, ...} => |
551 let |
556 let |
552 val (p, q) = apply2 snd (last2 params) |
557 val (p, q) = apply2 snd (last2 params) |
553 val pq_inst = foldl1 (uncurry Thm.apply) [@{cterm "plus::perm => perm => perm"}, p, q] |
558 val pq_inst = foldl1 (uncurry Thm.apply) [@{cterm "plus::perm => perm => perm"}, p, q] |
554 val exi_inst = Drule.instantiate' [SOME (@{ctyp "perm"})] [NONE, SOME pq_inst] @{thm exI} |
559 val exi_inst = Thm.instantiate' [SOME (@{ctyp "perm"})] [NONE, SOME pq_inst] @{thm exI} |
555 in |
560 in |
556 HEADGOAL (rtac exi_inst) |
561 HEADGOAL (resolve_tac ctxt [exi_inst]) |
557 end) |
562 end) |
558 |
563 |
559 fun non_trivial_cases_tac pred_names intros alpha_eqvt ctxt = |
564 fun non_trivial_cases_tac pred_names intros alpha_eqvt ctxt = |
560 let |
565 let |
561 val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def rel_prod_conv} |
566 val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def rel_prod_conv} |
562 in |
567 in |
563 resolve_tac ctxt intros |
568 resolve_tac ctxt intros |
564 THEN_ALL_NEW (asm_simp_tac (put_simpset HOL_basic_ss ctxt) THEN' |
569 THEN_ALL_NEW (asm_simp_tac (put_simpset HOL_basic_ss ctxt) THEN' |
565 TRY o EVERY' (* if binders are present *) |
570 TRY o EVERY' (* if binders are present *) |
566 [ etac @{thm exE}, |
571 [ eresolve_tac ctxt @{thms exE}, |
567 etac @{thm exE}, |
572 eresolve_tac ctxt @{thms exE}, |
568 perm_inst_tac ctxt, |
573 perm_inst_tac ctxt, |
569 resolve_tac ctxt @{thms alpha_trans_eqvt}, |
574 resolve_tac ctxt @{thms alpha_trans_eqvt}, |
570 assume_tac ctxt, |
575 assume_tac ctxt, |
571 aatac pred_names ctxt, |
576 aatac pred_names ctxt, |
572 eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' rtac @{thm refl}, |
577 eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' |
|
578 resolve_tac ctxt @{thms refl}, |
573 asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps) ]) |
579 asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps) ]) |
574 end |
580 end |
575 |
581 |
576 fun prove_trans_tac alpha_result raw_dt_thms alpha_eqvt ctxt = |
582 fun prove_trans_tac alpha_result raw_dt_thms alpha_eqvt ctxt = |
577 let |
583 let |
580 |
586 |
581 fun all_cases ctxt = |
587 fun all_cases ctxt = |
582 asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps raw_dt_thms) |
588 asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps raw_dt_thms) |
583 THEN' TRY o non_trivial_cases_tac alpha_names alpha_intros alpha_eqvt ctxt |
589 THEN' TRY o non_trivial_cases_tac alpha_names alpha_intros alpha_eqvt ctxt |
584 in |
590 in |
585 EVERY' [ rtac @{thm allI}, rtac @{thm impI}, |
591 EVERY' [ resolve_tac ctxt @{thms allI}, |
586 ecases_tac alpha_cases ctxt THEN_ALL_NEW all_cases ctxt ] |
592 resolve_tac ctxt @{thms impI}, |
|
593 ecases_tac alpha_cases ctxt THEN_ALL_NEW all_cases ctxt ] |
587 end |
594 end |
588 |
595 |
589 fun prep_trans_goal alpha_trm (arg1, arg2) = |
596 fun prep_trans_goal alpha_trm (arg1, arg2) = |
590 let |
597 let |
591 val arg_ty = fastype_of arg1 |
598 val arg_ty = fastype_of arg1 |
631 |
638 |
632 fun prep_goal t = |
639 fun prep_goal t = |
633 HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t) |
640 HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t) |
634 in |
641 in |
635 Goal.prove_common ctxt NONE [] [] (map prep_goal (alpha_trms @ alpha_bn_trms)) |
642 Goal.prove_common ctxt NONE [] [] (map prep_goal (alpha_trms @ alpha_bn_trms)) |
636 (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (rtac @{thm equivpI} THEN' |
643 (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (resolve_tac ctxt @{thms equivpI} THEN' |
637 RANGE [resolve_tac ctxt refl', resolve_tac ctxt symm', resolve_tac ctxt trans'])))) |
644 RANGE [resolve_tac ctxt refl', resolve_tac ctxt symm', resolve_tac ctxt trans'])))) |
638 |> chop (length alpha_trms) |
645 |> chop (length alpha_trms) |
639 end |
646 end |
640 |
647 |
641 |
648 |
642 (* proves that alpha_raw implies alpha_bn *) |
649 (* proves that alpha_raw implies alpha_bn *) |
643 |
650 |
644 fun raw_prove_bn_imp_tac alpha_result ctxt = |
651 fun raw_prove_bn_imp_tac alpha_result ctxt = |
645 SUBPROOF (fn {prems, context, ...} => |
652 SUBPROOF (fn {prems, context = ctxt', ...} => |
646 let |
653 let |
647 val AlphaResult {alpha_names, alpha_intros, ...} = alpha_result |
654 val AlphaResult {alpha_names, alpha_intros, ...} = alpha_result |
648 |
655 |
649 val prems' = flat (map Old_Datatype_Aux.split_conj_thm prems) |
656 val prems' = flat (map Old_Datatype_Aux.split_conj_thm prems) |
650 val prems'' = map (transform_prem1 context alpha_names) prems' |
657 val prems'' = map (transform_prem1 ctxt' alpha_names) prems' |
651 in |
658 in |
652 HEADGOAL |
659 HEADGOAL |
653 (REPEAT_ALL_NEW |
660 (REPEAT_ALL_NEW |
654 (FIRST' [ rtac @{thm TrueI}, |
661 (FIRST' [ resolve_tac ctxt' @{thms TrueI}, |
655 rtac @{thm conjI}, |
662 resolve_tac ctxt' @{thms conjI}, |
656 resolve_tac ctxt prems', |
663 resolve_tac ctxt' prems', |
657 resolve_tac ctxt prems'', |
664 resolve_tac ctxt' prems'', |
658 resolve_tac ctxt alpha_intros ])) |
665 resolve_tac ctxt' alpha_intros ])) |
659 end) ctxt |
666 end) ctxt |
660 |
667 |
661 |
668 |
662 fun raw_prove_bn_imp ctxt alpha_result = |
669 fun raw_prove_bn_imp ctxt alpha_result = |
663 let |
670 let |
726 prod_fv.simps fresh_star_zero permute_zero prod.case} @ simps |
733 prod_fv.simps fresh_star_zero permute_zero prod.case} @ simps |
727 in |
734 in |
728 asm_full_simp_tac pre_simpset |
735 asm_full_simp_tac pre_simpset |
729 THEN' REPEAT o (resolve_tac ctxt @{thms allI impI}) |
736 THEN' REPEAT o (resolve_tac ctxt @{thms allI impI}) |
730 THEN' resolve_tac ctxt alpha_intros |
737 THEN' resolve_tac ctxt alpha_intros |
731 THEN_ALL_NEW (TRY o (rtac exi_zero) THEN' asm_full_simp_tac post_simpset) |
738 THEN_ALL_NEW (TRY o (resolve_tac ctxt [exi_zero]) THEN' asm_full_simp_tac post_simpset) |
732 end |
739 end |
733 |
740 |
734 fun raw_constrs_rsp ctxt alpha_result constrs simps = |
741 fun raw_constrs_rsp ctxt alpha_result constrs simps = |
735 let |
742 let |
736 val AlphaResult {alpha_trms, alpha_tys, alpha_intros, ...} = alpha_result |
743 val AlphaResult {alpha_trms, alpha_tys, alpha_intros, ...} = alpha_result |
794 |
801 |
795 val perm_bn_rsp = @{lemma "(!x y p. R x y --> R (f p x) (f p y)) ==> (op= ===> R ===> R) f f" |
802 val perm_bn_rsp = @{lemma "(!x y p. R x y --> R (f p x) (f p y)) ==> (op= ===> R ===> R) f f" |
796 by (simp add: rel_fun_def)} |
803 by (simp add: rel_fun_def)} |
797 |
804 |
798 fun raw_prove_perm_bn_tac alpha_result simps ctxt = |
805 fun raw_prove_perm_bn_tac alpha_result simps ctxt = |
799 SUBPROOF (fn {prems, context, ...} => |
806 SUBPROOF (fn {prems, context = ctxt', ...} => |
800 let |
807 let |
801 val AlphaResult {alpha_names, alpha_bn_names, alpha_intros, ...} = alpha_result |
808 val AlphaResult {alpha_names, alpha_bn_names, alpha_intros, ...} = alpha_result |
802 val prems' = flat (map Old_Datatype_Aux.split_conj_thm prems) |
809 val prems' = flat (map Old_Datatype_Aux.split_conj_thm prems) |
803 val prems'' = map (transform_prem1 context (alpha_names @ alpha_bn_names)) prems' |
810 val prems'' = map (transform_prem1 ctxt' (alpha_names @ alpha_bn_names)) prems' |
804 in |
811 in |
805 HEADGOAL |
812 HEADGOAL |
806 (simp_tac (put_simpset HOL_basic_ss ctxt addsimps (simps @ prems')) |
813 (simp_tac (put_simpset HOL_basic_ss ctxt' addsimps (simps @ prems')) |
807 THEN' TRY o REPEAT_ALL_NEW |
814 THEN' TRY o REPEAT_ALL_NEW |
808 (FIRST' [ rtac @{thm TrueI}, |
815 (FIRST' [ resolve_tac ctxt' @{thms TrueI}, |
809 rtac @{thm conjI}, |
816 resolve_tac ctxt' @{thms conjI}, |
810 rtac @{thm refl}, |
817 resolve_tac ctxt' @{thms refl}, |
811 resolve_tac ctxt prems', |
818 resolve_tac ctxt' prems', |
812 resolve_tac ctxt prems'', |
819 resolve_tac ctxt' prems'', |
813 resolve_tac ctxt alpha_intros ])) |
820 resolve_tac ctxt' alpha_intros ])) |
814 end) ctxt |
821 end) ctxt |
815 |
822 |
816 fun raw_perm_bn_rsp ctxt alpha_result perm_bns simps = |
823 fun raw_perm_bn_rsp ctxt alpha_result perm_bns simps = |
817 let |
824 let |
818 val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_bn_tys, alpha_raw_induct, ...} = |
825 val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_bn_tys, alpha_raw_induct, ...} = |