53 val elim_rules: thm Item_Net.T |
53 val elim_rules: thm Item_Net.T |
54 val declare_hyps: cterm -> Proof.context -> Proof.context |
54 val declare_hyps: cterm -> Proof.context -> Proof.context |
55 val assume_hyps: cterm -> Proof.context -> thm * Proof.context |
55 val assume_hyps: cterm -> Proof.context -> thm * Proof.context |
56 val unchecked_hyps: Proof.context -> Proof.context |
56 val unchecked_hyps: Proof.context -> Proof.context |
57 val restore_hyps: Proof.context -> Proof.context -> Proof.context |
57 val restore_hyps: Proof.context -> Proof.context -> Proof.context |
|
58 val undeclared_hyps: Context.generic -> thm -> term list |
58 val check_hyps: Context.generic -> thm -> thm |
59 val check_hyps: Context.generic -> thm -> thm |
59 val elim_implies: thm -> thm -> thm |
60 val elim_implies: thm -> thm -> thm |
60 val forall_elim_var: int -> thm -> thm |
61 val forall_elim_var: int -> thm -> thm |
61 val forall_elim_vars: int -> thm -> thm |
62 val forall_elim_vars: int -> thm -> thm |
62 val certify_inst: theory -> |
63 val certify_inst: theory -> |
279 fun assume_hyps ct ctxt = (Thm.assume ct, declare_hyps ct ctxt); |
280 fun assume_hyps ct ctxt = (Thm.assume ct, declare_hyps ct ctxt); |
280 |
281 |
281 val unchecked_hyps = (Hyps.map o apsnd) (K false); |
282 val unchecked_hyps = (Hyps.map o apsnd) (K false); |
282 fun restore_hyps ctxt = (Hyps.map o apsnd) (K (#2 (Hyps.get ctxt))); |
283 fun restore_hyps ctxt = (Hyps.map o apsnd) (K (#2 (Hyps.get ctxt))); |
283 |
284 |
|
285 fun undeclared_hyps context th = |
|
286 Thm.hyps_of th |
|
287 |> filter_out |
|
288 (case context of |
|
289 Context.Theory _ => K false |
|
290 | Context.Proof ctxt => |
|
291 (case Hyps.get ctxt of |
|
292 (_, false) => K true |
|
293 | (hyps, _) => Termtab.defined hyps)); |
|
294 |
284 fun check_hyps context th = |
295 fun check_hyps context th = |
285 let |
296 (case undeclared_hyps context th of |
286 val declared_hyps = |
297 [] => th |
287 (case context of |
298 | undeclared => |
288 Context.Theory _ => K false |
|
289 | Context.Proof ctxt => |
|
290 (case Hyps.get ctxt of |
|
291 (_, false) => K true |
|
292 | (hyps, _) => Termtab.defined hyps)); |
|
293 val undeclared = filter_out declared_hyps (Thm.hyps_of th); |
|
294 in |
|
295 if null undeclared then th |
|
296 else |
|
297 let |
299 let |
298 val ctxt = Context.cases Syntax.init_pretty_global I context; |
300 val ctxt = Context.cases Syntax.init_pretty_global I context; |
299 in |
301 in |
300 error (Pretty.string_of (Pretty.big_list "Undeclared hyps:" |
302 error (Pretty.string_of (Pretty.big_list "Undeclared hyps:" |
301 (map (Pretty.item o single o Syntax.pretty_term ctxt) undeclared))) |
303 (map (Pretty.item o single o Syntax.pretty_term ctxt) undeclared))) |
302 end |
304 end); |
303 end; |
|
304 |
305 |
305 |
306 |
306 |
307 |
307 (** basic derived rules **) |
308 (** basic derived rules **) |
308 |
309 |