src/Pure/more_thm.ML

--- a/src/Pure/more_thm.ML	Fri Oct 23 16:09:06 2015 +0200
+++ b/src/Pure/more_thm.ML	Fri Oct 23 17:17:11 2015 +0200
@@ -48,7 +48,6 @@
   val equiv_thm: theory -> thm * thm -> bool
   val class_triv: theory -> class -> thm
   val of_sort: ctyp * sort -> thm list
-  val check_shyps: Proof.context -> sort list -> thm -> thm
   val is_dummy: thm -> bool
   val plain_prop_of: thm -> term
   val add_thm: thm -> thm list -> thm list
@@ -63,6 +62,9 @@
   val restore_hyps: Proof.context -> Proof.context -> Proof.context
   val undeclared_hyps: Context.generic -> thm -> term list
   val check_hyps: Context.generic -> thm -> thm
+  val declare_term_sorts: term -> Proof.context -> Proof.context
+  val check_shyps: Proof.context -> thm -> thm
+  val weaken_sorts': Proof.context -> cterm -> cterm
   val elim_implies: thm -> thm -> thm
   val forall_intr_name: string * cterm -> thm -> thm
   val forall_elim_var: int -> thm -> thm
@@ -229,16 +231,6 @@
 
 fun of_sort (T, S) = map (fn c => Thm.of_class (T, c)) S;
 
-fun check_shyps ctxt sorts raw_th =
-  let
-    val th = Thm.strip_shyps raw_th;
-    val pending = Sorts.subtract sorts (Thm.extra_shyps th);
-  in
-    if null pending then th
-    else error (Pretty.string_of (Pretty.block (Pretty.str "Pending sort hypotheses:" ::
-      Pretty.brk 1 :: Pretty.commas (map (Syntax.pretty_sort ctxt) pending))))
-  end;
-
 
 (* misc operations *)
 
@@ -274,22 +266,33 @@
 
 
 
-(** declared hyps **)
+(** declared hyps and sort hyps **)
 
 structure Hyps = Proof_Data
 (
-  type T = Termtab.set * bool;
-  fun init _ : T = (Termtab.empty, true);
+  type T = {checked_hyps: bool, hyps: Termtab.set, shyps: sort Ord_List.T};
+  fun init _ : T = {checked_hyps = true, hyps = Termtab.empty, shyps = []};
 );
 
-fun declare_hyps raw_ct ctxt =
-  let val ct = Thm.transfer_cterm (Proof_Context.theory_of ctxt) raw_ct
-  in (Hyps.map o apfst) (Termtab.update (Thm.term_of ct, ())) ctxt end;
+fun map_hyps f = Hyps.map (fn {checked_hyps, hyps, shyps} =>
+  let val (checked_hyps', hyps', shyps') = f (checked_hyps, hyps, shyps)
+  in {checked_hyps = checked_hyps', hyps = hyps', shyps = shyps'} end);
+
+
+(* hyps *)
+
+fun declare_hyps raw_ct ctxt = ctxt |> map_hyps (fn (checked_hyps, hyps, shyps) =>
+  let
+    val ct = Thm.transfer_cterm (Proof_Context.theory_of ctxt) raw_ct;
+    val hyps' = Termtab.update (Thm.term_of ct, ()) hyps;
+  in (checked_hyps, hyps', shyps) end);
 
 fun assume_hyps ct ctxt = (Thm.assume ct, declare_hyps ct ctxt);
 
-val unchecked_hyps = (Hyps.map o apsnd) (K false);
-fun restore_hyps ctxt = (Hyps.map o apsnd) (K (#2 (Hyps.get ctxt)));
+val unchecked_hyps = map_hyps (fn (_, hyps, shyps) => (false, hyps, shyps));
+
+fun restore_hyps ctxt =
+  map_hyps (fn (_, hyps, shyps) => (#checked_hyps (Hyps.get ctxt), hyps, shyps));
 
 fun undeclared_hyps context th =
   Thm.hyps_of th
@@ -298,8 +301,8 @@
       Context.Theory _ => K false
     | Context.Proof ctxt =>
         (case Hyps.get ctxt of
-          (_, false) => K true
-        | (hyps, _) => Termtab.defined hyps));
+          {checked_hyps = false, ...} => K true
+        | {hyps, ...} => Termtab.defined hyps));
 
 fun check_hyps context th =
   (case undeclared_hyps context th of
@@ -309,6 +312,25 @@
         (map (Pretty.item o single o Syntax.pretty_term (Syntax.init_pretty context)) undeclared))));
 
 
+(* shyps *)
+
+fun declare_term_sorts t =
+  map_hyps (fn (checked_hyps, hyps, shyps) =>
+    (checked_hyps, hyps, Sorts.insert_term t shyps));
+
+fun check_shyps ctxt raw_th =
+  let
+    val th = Thm.strip_shyps raw_th;
+    val pending = Sorts.subtract (#shyps (Hyps.get ctxt)) (Thm.extra_shyps th);
+  in
+    if null pending then th
+    else error (Pretty.string_of (Pretty.block (Pretty.str "Pending sort hypotheses:" ::
+      Pretty.brk 1 :: Pretty.commas (map (Syntax.pretty_sort ctxt) pending))))
+  end;
+
+val weaken_sorts' = Thm.weaken_sorts o #shyps o Hyps.get;
+
+
 
 (** basic derived rules **)