259 THEN prune_params_tac |
259 THEN prune_params_tac |
260 (*Mutual recursion: collapse references to Part(D,h)*) |
260 (*Mutual recursion: collapse references to Part(D,h)*) |
261 THEN (PRIMITIVE (fold_rule part_rec_defs)); |
261 THEN (PRIMITIVE (fold_rule part_rec_defs)); |
262 |
262 |
263 (*Elimination*) |
263 (*Elimination*) |
264 val elim = rule_by_tactic basic_elim_tac |
264 val elim = rule_by_tactic (ProofContext.init thy1) basic_elim_tac |
265 (unfold RS Ind_Syntax.equals_CollectD) |
265 (unfold RS Ind_Syntax.equals_CollectD) |
266 |
266 |
267 (*Applies freeness of the given constructors, which *must* be unfolded by |
267 (*Applies freeness of the given constructors, which *must* be unfolded by |
268 the given defs. Cannot simply use the local con_defs because |
268 the given defs. Cannot simply use the local con_defs because |
269 con_defs=[] for inference systems. |
269 con_defs=[] for inference systems. |
270 Proposition A should have the form t:Si where Si is an inductive set*) |
270 Proposition A should have the form t:Si where Si is an inductive set*) |
271 fun make_cases ctxt A = |
271 fun make_cases ctxt A = |
272 rule_by_tactic |
272 rule_by_tactic ctxt |
273 (basic_elim_tac THEN ALLGOALS (asm_full_simp_tac (simpset_of ctxt)) THEN basic_elim_tac) |
273 (basic_elim_tac THEN ALLGOALS (asm_full_simp_tac (simpset_of ctxt)) THEN basic_elim_tac) |
274 (Thm.assume A RS elim) |
274 (Thm.assume A RS elim) |
275 |> Drule.export_without_context_open; |
275 |> Drule.export_without_context_open; |
276 |
276 |
277 fun induction_rules raw_induct thy = |
277 fun induction_rules raw_induct thy = |