# HG changeset patch
# User wenzelm
# Date 1272976739 -7200
# Node ID 2fd4e2c766366b47817634c23688358969fdf2c6
# Parent  e6bb250402b51153d496f9da436d5da2f2c4794d
proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
* present type variables are only compared wrt. first component (the atomic type), not the duplicated sort;
* extra sorts are grounded towards fixed 'a, potentially with different sorts (the original version with Name.names could cause name clashes with other present variables, too, but this should not be a problem);
* deriv_rule_unconditional ensures that proof terms are always maintained independently of the "proofs" flag -- this improves robustness and preserves basic PThm proofs required for extraction attributes, e.g. in theory HOL/Extraction;

diff -r e6bb250402b5 -r 2fd4e2c76636 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Tue May 04 12:30:15 2010 +0200
+++ b/src/Pure/proofterm.ML	Tue May 04 14:38:59 2010 +0200
@@ -108,6 +108,8 @@
   val combination: term -> term -> term -> term -> typ -> proof -> proof -> proof
   val equal_intr: term -> term -> proof -> proof -> proof
   val equal_elim: term -> term -> proof -> proof -> proof
+  val strip_shyps_proof: Sorts.algebra -> (typ * sort) list -> (typ * sort) list ->
+    sort list -> proof -> proof
   val axm_proof: string -> term -> proof
   val oracle_proof: string -> term -> oracle * proof
   val promise_proof: theory -> serial -> term -> proof
@@ -884,6 +886,22 @@
   equal_elim_axm %> remove_types A %> remove_types B %% prf1 %% prf2;
 
 
+(**** sort hypotheses ****)
+
+fun strip_shyps_proof algebra present witnessed extra_sorts prf =
+  let
+    fun get S2 (T, S1) = if Sorts.sort_le algebra (S1, S2) then SOME T else NONE;
+    val extra = map (fn S => (TFree (Name.aT, S), S)) extra_sorts;
+    val replacements = present @ extra @ witnessed;
+    fun replace T =
+      if exists (fn (T', _) => T' = T) present then raise Same.SAME
+      else
+        (case get_first (get (Type.sort_of_atyp T)) replacements of
+          SOME T' => T'
+        | NONE => raise Fail "strip_shyps_proof: bad type variable in proof term");
+  in Same.commit (map_proof_types_same (Term_Subst.map_atypsT_same replace)) prf end;
+
+
 (***** axioms and theorems *****)
 
 val proofs = Unsynchronized.ref 2;
diff -r e6bb250402b5 -r 2fd4e2c76636 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue May 04 12:30:15 2010 +0200
+++ b/src/Pure/thm.ML	Tue May 04 14:38:59 2010 +0200
@@ -512,6 +512,9 @@
 fun deriv_rule1 f = deriv_rule2 (K f) empty_deriv;
 fun deriv_rule0 prf = deriv_rule1 I (make_deriv [] [] [] prf);
 
+fun deriv_rule_unconditional f (Deriv {promises, body = PBody {oracles, thms, proof}}) =
+  make_deriv promises oracles thms (f proof);
+
 
 (* fulfilled proofs *)
 
@@ -1204,14 +1207,17 @@
   | strip_shyps (thm as Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) =
       let
         val thy = Theory.deref thy_ref;
-        val present = (fold_terms o fold_types o fold_atyps_sorts) (insert (eq_snd op =)) thm [];
+        val algebra = Sign.classes_of thy;
+
+        val present = (fold_terms o fold_types o fold_atyps_sorts) (insert (eq_fst op =)) thm [];
         val extra = fold (Sorts.remove_sort o #2) present shyps;
         val witnessed = Sign.witness_sorts thy present extra;
         val extra' = fold (Sorts.remove_sort o #2) witnessed extra
-          |> Sorts.minimal_sorts (Sign.classes_of thy);
+          |> Sorts.minimal_sorts algebra;
         val shyps' = fold (Sorts.insert_sort o #2) present extra';
       in
-        Thm (der, {thy_ref = Theory.check_thy thy, tags = tags, maxidx = maxidx,
+        Thm (deriv_rule_unconditional (Pt.strip_shyps_proof algebra present witnessed extra') der,
+         {thy_ref = Theory.check_thy thy, tags = tags, maxidx = maxidx,
           shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop})
       end;
 
diff -r e6bb250402b5 -r 2fd4e2c76636 src/Pure/type.ML
--- a/src/Pure/type.ML	Tue May 04 12:30:15 2010 +0200
+++ b/src/Pure/type.ML	Tue May 04 14:38:59 2010 +0200
@@ -53,6 +53,7 @@
   val arity_sorts: Pretty.pp -> tsig -> string -> sort -> sort list
 
   (*special treatment of type vars*)
+  val sort_of_atyp: typ -> sort
   val strip_sorts: typ -> typ
   val no_tvars: typ -> typ
   val varify_global: (string * sort) list -> term -> ((string * sort) * indexname) list * term
@@ -271,6 +272,13 @@
 
 (** special treatment of type vars **)
 
+(* sort_of_atyp *)
+
+fun sort_of_atyp (TFree (_, S)) = S
+  | sort_of_atyp (TVar (_, S)) = S
+  | sort_of_atyp T = raise TYPE ("sort_of_atyp", [T], []);
+
+
 (* strip_sorts *)
 
 fun strip_sorts (Type (a, Ts)) = Type (a, map strip_sorts Ts)