equal
deleted
inserted
replaced
245 |
245 |
246 local |
246 local |
247 |
247 |
248 fun err_in_rule ctxt name t msg = |
248 fun err_in_rule ctxt name t msg = |
249 error (cat_lines ["Ill-formed introduction rule " ^ quote name, |
249 error (cat_lines ["Ill-formed introduction rule " ^ quote name, |
250 ProofContext.string_of_term ctxt t, msg]); |
250 Syntax.string_of_term ctxt t, msg]); |
251 |
251 |
252 fun err_in_prem ctxt name t p msg = |
252 fun err_in_prem ctxt name t p msg = |
253 error (cat_lines ["Ill-formed premise", ProofContext.string_of_term ctxt p, |
253 error (cat_lines ["Ill-formed premise", Syntax.string_of_term ctxt p, |
254 "in introduction rule " ^ quote name, ProofContext.string_of_term ctxt t, msg]); |
254 "in introduction rule " ^ quote name, Syntax.string_of_term ctxt t, msg]); |
255 |
255 |
256 val bad_concl = "Conclusion of introduction rule must be an inductive predicate"; |
256 val bad_concl = "Conclusion of introduction rule must be an inductive predicate"; |
257 |
257 |
258 val bad_ind_occ = "Inductive predicate occurs in argument of inductive predicate"; |
258 val bad_ind_occ = "Inductive predicate occurs in argument of inductive predicate"; |
259 |
259 |
273 val aprems = map (atomize_term (ProofContext.theory_of ctxt)) prems; |
273 val aprems = map (atomize_term (ProofContext.theory_of ctxt)) prems; |
274 val arule = list_all_free (params', Logic.list_implies (aprems, concl)); |
274 val arule = list_all_free (params', Logic.list_implies (aprems, concl)); |
275 |
275 |
276 fun check_ind err t = case dest_predicate cs params t of |
276 fun check_ind err t = case dest_predicate cs params t of |
277 NONE => err (bad_app ^ |
277 NONE => err (bad_app ^ |
278 commas (map (ProofContext.string_of_term ctxt) params)) |
278 commas (map (Syntax.string_of_term ctxt) params)) |
279 | SOME (_, _, ys, _) => |
279 | SOME (_, _, ys, _) => |
280 if exists (fn c => exists (fn t => Logic.occs (c, t)) ys) cs |
280 if exists (fn c => exists (fn t => Logic.occs (c, t)) ys) cs |
281 then err bad_ind_occ else (); |
281 then err bad_ind_occ else (); |
282 |
282 |
283 fun check_prem' prem t = |
283 fun check_prem' prem t = |
429 val thy = ProofContext.theory_of ctxt; |
429 val thy = ProofContext.theory_of ctxt; |
430 val ss = Simplifier.local_simpset_of ctxt; |
430 val ss = Simplifier.local_simpset_of ctxt; |
431 |
431 |
432 fun err msg = |
432 fun err msg = |
433 error (Pretty.string_of (Pretty.block |
433 error (Pretty.string_of (Pretty.block |
434 [Pretty.str msg, Pretty.fbrk, ProofContext.pretty_term ctxt prop])); |
434 [Pretty.str msg, Pretty.fbrk, Syntax.pretty_term ctxt prop])); |
435 |
435 |
436 val elims = Induct.find_casesP ctxt prop; |
436 val elims = Induct.find_casesP ctxt prop; |
437 |
437 |
438 val cprop = Thm.cterm_of thy prop; |
438 val cprop = Thm.cterm_of thy prop; |
439 val tac = ALLGOALS (simp_case_tac ss) THEN prune_params_tac; |
439 val tac = ALLGOALS (simp_case_tac ss) THEN prune_params_tac; |