170 |
170 |
171 val prm' = (prems' MRS prm) |
171 val prm' = (prems' MRS prm) |
172 |> flag ? (all_elims [p]) |
172 |> flag ? (all_elims [p]) |
173 |> flag ? (eqvt_srule context) |
173 |> flag ? (eqvt_srule context) |
174 in |
174 in |
175 asm_full_simp_tac (HOL_ss addsimps (prm' :: @{thms induct_forall_def})) 1 |
175 asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps (prm' :: @{thms induct_forall_def})) 1 |
176 end) ctxt |
176 end) ctxt |
177 |
177 |
178 fun non_binder_tac prem intr_cvars Ps ctxt = |
178 fun non_binder_tac prem intr_cvars Ps ctxt = |
179 Subgoal.SUBPROOF (fn {context, params, prems, ...} => |
179 Subgoal.SUBPROOF (fn {context, params, prems, ...} => |
180 let |
180 let |
213 val fresh_goal = mk_exists ("q", @{typ perm}) (HOLogic.mk_conj (conj1, conj2)) |
213 val fresh_goal = mk_exists ("q", @{typ perm}) (HOLogic.mk_conj (conj1, conj2)) |
214 |> HOLogic.mk_Trueprop |
214 |> HOLogic.mk_Trueprop |
215 |
215 |
216 val ss = @{thms finite_supp supp_Pair finite_Un permute_finite} @ |
216 val ss = @{thms finite_supp supp_Pair finite_Un permute_finite} @ |
217 @{thms fresh_star_Pair fresh_star_permute_iff} |
217 @{thms fresh_star_Pair fresh_star_permute_iff} |
218 val simp = asm_full_simp_tac (HOL_ss addsimps ss) |
218 val simp = asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps ss) |
219 in |
219 in |
220 Goal.prove ctxt [] [] fresh_goal |
220 Goal.prove ctxt [] [] fresh_goal |
221 (K (HEADGOAL (rtac @{thm at_set_avoiding2} |
221 (K (HEADGOAL (rtac @{thm at_set_avoiding2} |
222 THEN_ALL_NEW EVERY' [cut_facts_tac user_thm, REPEAT o etac @{thm conjE}, simp]))) |
222 THEN_ALL_NEW EVERY' [cut_facts_tac user_thm, REPEAT o etac @{thm conjE}, simp]))) |
223 end |
223 end |
239 |
239 |
240 val avoid_trm' = subst_free (param_trms ~~ prm_trms) avoid_trm |
240 val avoid_trm' = subst_free (param_trms ~~ prm_trms) avoid_trm |
241 val concl_args' = map (subst_free (param_trms ~~ prm_trms)) concl_args |
241 val concl_args' = map (subst_free (param_trms ~~ prm_trms)) concl_args |
242 |
242 |
243 val user_thm' = map (cterm_instantiate (intr_cvars ~~ prms)) user_thm |
243 val user_thm' = map (cterm_instantiate (intr_cvars ~~ prms)) user_thm |
244 |> map (full_simplify (HOL_ss addsimps (@{thm fresh_star_Pair}::prems))) |
244 |> map (full_simplify (put_simpset HOL_ss ctxt addsimps (@{thm fresh_star_Pair}::prems))) |
245 |
245 |
246 val fthm = fresh_thm ctxt user_thm' (term_of p) (term_of c) concl_args' avoid_trm' |
246 val fthm = fresh_thm ctxt user_thm' (term_of p) (term_of c) concl_args' avoid_trm' |
247 |
247 |
248 val (([(_, q)], fprop :: fresh_eqs), ctxt') = Obtain.result |
248 val (([(_, q)], fprop :: fresh_eqs), ctxt') = Obtain.result |
249 (K (EVERY1 [etac @{thm exE}, |
249 (K (EVERY1 [etac @{thm exE}, |
250 full_simp_tac (HOL_basic_ss addsimps @{thms supp_Pair fresh_star_Un}), |
250 full_simp_tac (put_simpset HOL_basic_ss ctxt |
|
251 addsimps @{thms supp_Pair fresh_star_Un}), |
251 REPEAT o etac @{thm conjE}, |
252 REPEAT o etac @{thm conjE}, |
252 dtac fresh_star_plus, |
253 dtac fresh_star_plus, |
253 REPEAT o dtac supp_perm_eq'])) [fthm] ctxt |
254 REPEAT o dtac supp_perm_eq'])) [fthm] ctxt |
254 |
255 |
255 val expand_conv = Conv.try_conv (Conv.rewrs_conv fresh_eqs) |
256 val expand_conv = Conv.try_conv (Conv.rewrs_conv fresh_eqs) |
260 val prem' = prem |
261 val prem' = prem |
261 |> cterm_instantiate (intr_cvars ~~ qp_prms) |
262 |> cterm_instantiate (intr_cvars ~~ qp_prms) |
262 |> eqvt_srule ctxt |
263 |> eqvt_srule ctxt |
263 |
264 |
264 val fprop' = eqvt_srule ctxt' fprop |
265 val fprop' = eqvt_srule ctxt' fprop |
265 val tac_fresh = simp_tac (HOL_basic_ss addsimps [fprop']) |
266 val tac_fresh = simp_tac (put_simpset HOL_basic_ss ctxt' addsimps [fprop']) |
266 |
267 |
267 (* for inductive-premises*) |
268 (* for inductive-premises*) |
268 fun tac1 prm = helper_tac true prm (mk_cplus q p) ctxt' |
269 fun tac1 prm = helper_tac true prm (mk_cplus q p) ctxt' |
269 |
270 |
270 (* for non-inductive premises *) |
271 (* for non-inductive premises *) |
368 val strong_ind_thms = Goal.prove ctxt [] ind_prems' ind_concl' |
369 val strong_ind_thms = Goal.prove ctxt [] ind_prems' ind_concl' |
369 (prove_sinduct_tac raw_induct user_thms Ps avoids avoid_trms intr_cvars param_trms intr_concls_args) |
370 (prove_sinduct_tac raw_induct user_thms Ps avoids avoid_trms intr_cvars param_trms intr_concls_args) |
370 |> singleton (Proof_Context.export ctxt ctxt_outside) |
371 |> singleton (Proof_Context.export ctxt ctxt_outside) |
371 |> Datatype_Aux.split_conj_thm |
372 |> Datatype_Aux.split_conj_thm |
372 |> map (fn thm => thm RS normalise) |
373 |> map (fn thm => thm RS normalise) |
373 |> map (asm_full_simplify (HOL_basic_ss addsimps @{thms permute_zero induct_rulify})) |
374 |> map (asm_full_simplify (put_simpset HOL_basic_ss ctxt |
|
375 addsimps @{thms permute_zero induct_rulify})) |
374 |> map (Drule.rotate_prems (length ind_prems')) |
376 |> map (Drule.rotate_prems (length ind_prems')) |
375 |> map zero_var_indexes |
377 |> map zero_var_indexes |
376 |
378 |
377 val qualified_thm_name = pred_names |
379 val qualified_thm_name = pred_names |
378 |> map Long_Name.base_name |
380 |> map Long_Name.base_name |