equal
deleted
inserted
replaced
228 |> HOLogic.mk_Trueprop |
228 |> HOLogic.mk_Trueprop |
229 |
229 |
230 val tac = |
230 val tac = |
231 EVERY' [ rtac @{thm supports_finite}, |
231 EVERY' [ rtac @{thm supports_finite}, |
232 resolve_tac qsupports_thms, |
232 resolve_tac qsupports_thms, |
233 asm_simp_tac (put_simpset HOL_ss ctxt |
233 asm_simp_tac (put_simpset HOL_ss ctxt' |
234 addsimps @{thms finite_supp supp_Pair finite_Un}) ] |
234 addsimps @{thms finite_supp supp_Pair finite_Un}) ] |
235 in |
235 in |
236 Goal.prove ctxt' [] [] goals |
236 Goal.prove ctxt' [] [] goals |
237 (K (HEADGOAL (rtac qinduct THEN_ALL_NEW tac))) |
237 (K (HEADGOAL (rtac qinduct THEN_ALL_NEW tac))) |
238 |> singleton (Proof_Context.export ctxt' ctxt) |
238 |> singleton (Proof_Context.export ctxt' ctxt) |
570 (fn ctxt' => EVERY1 [etac exE, |
570 (fn ctxt' => EVERY1 [etac exE, |
571 full_simp_tac (put_simpset HOL_basic_ss ctxt' addsimps ss), |
571 full_simp_tac (put_simpset HOL_basic_ss ctxt' addsimps ss), |
572 REPEAT o (etac @{thm conjE})]) [fthm] ctxt |
572 REPEAT o (etac @{thm conjE})]) [fthm] ctxt |
573 |
573 |
574 val abs_eq_thms = flat |
574 val abs_eq_thms = flat |
575 (map (abs_eq_thm ctxt fprops (term_of fperm) parms bn_eqvt permute_bns) bclauses) |
575 (map (abs_eq_thm ctxt' fprops (term_of fperm) parms bn_eqvt permute_bns) bclauses) |
576 |
576 |
577 val ((_, eqs), ctxt'') = Obtain.result |
577 val ((_, eqs), ctxt'') = Obtain.result |
578 (fn ctxt'' => EVERY1 |
578 (fn ctxt'' => EVERY1 |
579 [ REPEAT o (etac @{thm exE}), |
579 [ REPEAT o (etac @{thm exE}), |
580 REPEAT o (etac @{thm conjE}), |
580 REPEAT o (etac @{thm conjE}), |
583 addsimps @{thms set_append set.simps})]) abs_eq_thms ctxt' |
583 addsimps @{thms set_append set.simps})]) abs_eq_thms ctxt' |
584 |
584 |
585 val (abs_eqs, peqs) = split_filter is_abs_eq eqs |
585 val (abs_eqs, peqs) = split_filter is_abs_eq eqs |
586 |
586 |
587 val fprops' = |
587 val fprops' = |
588 map (eqvt_rule ctxt (eqvt_strict_config addpres permute_bns)) fprops |
588 map (eqvt_rule ctxt'' (eqvt_strict_config addpres permute_bns)) fprops |
589 @ map (eqvt_rule ctxt (eqvt_strict_config addpres bn_eqvt)) fprops |
589 @ map (eqvt_rule ctxt'' (eqvt_strict_config addpres bn_eqvt)) fprops |
590 |
590 |
591 (* for freshness conditions *) |
591 (* for freshness conditions *) |
592 val tac1 = SOLVED' (EVERY' |
592 val tac1 = SOLVED' (EVERY' |
593 [ simp_tac (put_simpset HOL_basic_ss ctxt'' addsimps peqs), |
593 [ simp_tac (put_simpset HOL_basic_ss ctxt'' addsimps peqs), |
594 rewrite_goal_tac ctxt'' (@{thms fresh_star_Un[THEN eq_reflection]}), |
594 rewrite_goal_tac ctxt'' (@{thms fresh_star_Un[THEN eq_reflection]}), |
734 in |
734 in |
735 rtac thm' 1 |
735 rtac thm' 1 |
736 end) ctxt |
736 end) ctxt |
737 THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_basic_ss ctxt) |
737 THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_basic_ss ctxt) |
738 |
738 |
739 (* FIXME proper goal context *) |
739 fun size_simp_tac ctxt = |
740 val size_simp_tac = |
740 simp_tac (put_simpset size_ss ctxt addsimps (@{thms comp_def snd_conv} @ size_thms)) |
741 simp_tac (put_simpset size_ss lthy'' addsimps (@{thms comp_def snd_conv} @ size_thms)) |
|
742 in |
741 in |
743 Goal.prove_multi lthy'' [] prems' concls |
742 Goal.prove_multi lthy'' [] prems' concls |
744 (fn {prems, context} => |
743 (fn {prems, context = ctxt} => |
745 Induction_Schema.induction_schema_tac context prems |
744 Induction_Schema.induction_schema_tac ctxt prems |
746 THEN RANGE (map (pat_tac context) exhausts) 1 |
745 THEN RANGE (map (pat_tac ctxt) exhausts) 1 |
747 THEN prove_termination_ind context 1 |
746 THEN prove_termination_ind ctxt 1 |
748 THEN ALLGOALS size_simp_tac) |
747 THEN ALLGOALS (size_simp_tac ctxt)) |
749 |> Proof_Context.export lthy'' lthy |
748 |> Proof_Context.export lthy'' lthy |
750 end |
749 end |
751 |
750 |
752 |
751 |
753 end (* structure *) |
752 end (* structure *) |