--- a/src/Pure/more_thm.ML Fri Jan 10 17:44:41 2014 +0100
+++ b/src/Pure/more_thm.ML Fri Jan 10 21:37:28 2014 +0100
@@ -52,6 +52,9 @@
val full_rules: thm Item_Net.T
val intro_rules: thm Item_Net.T
val elim_rules: thm Item_Net.T
+ val declare_hyps: cterm -> Proof.context -> Proof.context
+ val assume_hyps: cterm -> Proof.context -> thm * Proof.context
+ val check_hyps: Proof.context -> thm -> thm
val elim_implies: thm -> thm -> thm
val forall_elim_var: int -> thm -> thm
val forall_elim_vars: int -> thm -> thm
@@ -259,6 +262,30 @@
+(** declared hyps **)
+
+structure Hyps = Proof_Data
+(
+ type T = Termtab.set;
+ fun init _ : T = Termtab.empty;
+);
+
+fun declare_hyps ct ctxt =
+ if Theory.subthy (theory_of_cterm ct, Proof_Context.theory_of ctxt) then
+ Hyps.map (Termtab.update (term_of ct, ())) ctxt
+ else raise CTERM ("assume_hyps: bad background theory", [ct]);
+
+fun assume_hyps ct ctxt = (Thm.assume ct, declare_hyps ct ctxt);
+
+fun check_hyps ctxt th =
+ let
+ val undeclared = filter_out (Termtab.defined (Hyps.get ctxt)) (Thm.hyps_of th);
+ val _ = null undeclared orelse
+ error ("Undeclared hypotheses:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) undeclared));
+ in th end;
+
+
+
(** basic derived rules **)
(*Elimination of implication