merged

--- a/src/Pure/ML-Systems/polyml_common.ML	Fri May 14 23:35:35 2010 +0200
+++ b/src/Pure/ML-Systems/polyml_common.ML	Sat May 15 13:31:25 2010 +0200
@@ -6,7 +6,11 @@
 exception Interrupt = SML90.Interrupt;
 
 use "General/exn.ML";
-use "ML-Systems/single_assignment_polyml.ML";
+
+if List.exists (fn s => s = "SingleAssignment") (PolyML.Compiler.structureNames ())
+then ()
+else use "ML-Systems/single_assignment_polyml.ML";
+
 use "ML-Systems/multithreading.ML";
 use "ML-Systems/time_limit.ML";
 use "ML-Systems/timing.ML";

--- a/src/Pure/axclass.ML	Fri May 14 23:35:35 2010 +0200
+++ b/src/Pure/axclass.ML	Sat May 15 13:31:25 2010 +0200
@@ -196,9 +196,9 @@
 
 fun the_classrel thy (c1, c2) =
   (case Symreltab.lookup (proven_classrels_of thy) (c1, c2) of
-    SOME thm => Thm.transfer thy thm
+    SOME thm => thm
   | NONE => error ("Unproven class relation " ^
-      Syntax.string_of_classrel (ProofContext.init_global thy) [c1, c2]));
+      Syntax.string_of_classrel (ProofContext.init_global thy) [c1, c2]));  (* FIXME stale thy (!?) *)
 
 fun put_trancl_classrel ((c1, c2), th) thy =
   let
@@ -206,7 +206,7 @@
     val classrels = proven_classrels_of thy;
 
     fun reflcl_classrel (c1', c2') =
-      if c1' = c2' then NONE else SOME (the_classrel thy (c1', c2'));
+      if c1' = c2' then NONE else SOME (Thm.transfer thy (the_classrel thy (c1', c2')));
     fun gen_classrel (c1_pred, c2_succ) =
       let
         val th' =
@@ -243,9 +243,9 @@
 
 fun the_arity thy (a, Ss, c) =
   (case AList.lookup (op =) (Symtab.lookup_list (proven_arities_of thy) a) (c, Ss) of
-    SOME (thm, _) => Thm.transfer thy thm
+    SOME (thm, _) => thm
   | NONE => error ("Unproven type arity " ^
-      Syntax.string_of_arity (ProofContext.init_global thy) (a, Ss, [c])));
+      Syntax.string_of_arity (ProofContext.init_global thy) (a, Ss, [c])));  (* FIXME stale thy (!?) *)
 
 fun thynames_of_arity thy (c, a) =
   Symtab.lookup_list (proven_arities_of thy) a
@@ -267,7 +267,7 @@
     val completions = super_class_completions |> map (fn c1 =>
       let
         val th1 =
-          (th RS the_classrel thy (c, c1))
+          (th RS Thm.transfer thy (the_classrel thy (c, c1)))
           |> Drule.instantiate' std_vars []
           |> Thm.close_derivation;
       in ((th1, thy_name), c1) end);

--- a/src/Pure/proofterm.ML	Fri May 14 23:35:35 2010 +0200
+++ b/src/Pure/proofterm.ML	Sat May 15 13:31:25 2010 +0200
@@ -118,11 +118,6 @@
     arity_proof: theory -> string * sort list * class -> proof} -> unit
   val axm_proof: string -> term -> proof
   val oracle_proof: string -> term -> oracle * proof
-  val promise_proof: theory -> serial -> term -> proof
-  val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
-  val thm_proof: theory -> string -> term list -> term ->
-    (serial * proof_body future) list -> proof_body -> pthm * proof
-  val get_name: term list -> term -> proof -> string
 
   (** rewriting on proof terms **)
   val add_prf_rrule: proof * proof -> theory -> theory
@@ -134,6 +129,17 @@
   val rewrite_proof_notypes: (proof * proof) list *
     (typ list -> proof -> (proof * proof) option) list -> proof -> proof
   val rew_proof: theory -> proof -> proof
+
+  val promise_proof: theory -> serial -> term -> proof
+  val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
+  val unconstrain_thm_proofs: bool Unsynchronized.ref
+  val thm_proof: theory -> string -> sort list -> term list -> term ->
+    (serial * proof_body future) list -> proof_body -> pthm * proof
+  val unconstrain_thm_proof: theory -> sort list -> term ->
+    (serial * proof_body future) list -> proof_body -> pthm * proof
+  val get_name: term list -> term -> proof -> string
+  val get_name_unconstrained: sort list -> term list -> term -> proof -> string
+  val guess_name: proof -> string
 end
 
 structure Proofterm : PROOFTERM =
@@ -344,7 +350,7 @@
 fun change_type opTs (PAxm (name, prop, _)) = PAxm (name, prop, opTs)
   | change_type (SOME [T]) (OfClass (_, c)) = OfClass (T, c)
   | change_type opTs (Oracle (name, prop, _)) = Oracle (name, prop, opTs)
-  | change_type opTs (Promise _) = error "change_type: unexpected promise"
+  | change_type opTs (Promise _) = raise Fail "change_type: unexpected promise"
   | change_type opTs (PThm (i, ((name, prop, _), body))) =
       PThm (i, ((name, prop, opTs), body))
   | change_type _ prf = prf;
@@ -1071,7 +1077,7 @@
               | Oracle (_, prop, _) => prop
               | Promise (_, prop, _) => prop
               | PThm (_, ((_, prop, _), _)) => prop
-              | _ => error "shrink: proof not in normal form");
+              | _ => raise Fail "shrink: proof not in normal form");
             val vs = vars_of prop;
             val (ts', ts'') = chop (length vs) ts;
             val insts = take (length ts') (map (fst o dest_Var) vs) ~~ ts';
@@ -1348,9 +1354,9 @@
   let
     val _ = prop |> Term.exists_subterm (fn t =>
       (Term.is_Free t orelse Term.is_Var t) andalso
-        error ("promise_proof: illegal variable " ^ Syntax.string_of_term_global thy t));
+        raise Fail ("promise_proof: illegal variable " ^ Syntax.string_of_term_global thy t));
     val _ = prop |> Term.exists_type (Term.exists_subtype
-      (fn TFree (a, _) => error ("promise_proof: illegal type variable " ^ quote a)
+      (fn TFree (a, _) => raise Fail ("promise_proof: illegal type variable " ^ quote a)
         | _ => false));
   in Promise (i, prop, map TVar (Term.add_tvars prop [])) end;
 
@@ -1370,15 +1376,40 @@
     val proof = rewrite_prf fst (rules, K fill :: procs) proof0;
   in PBody {oracles = oracles, thms = thms, proof = proof} end;
 
-fun fulfill_proof_future _ [] body = Future.value body
-  | fulfill_proof_future thy promises body =
+fun fulfill_proof_future _ [] postproc body = Future.value (postproc body)
+  | fulfill_proof_future thy promises postproc body =
       Future.fork_deps (map snd promises) (fn () =>
-        fulfill_norm_proof thy (map (apsnd Future.join) promises) body);
+        postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) body));
+
+
+(***** abstraction over sort constraints *****)
+
+fun unconstrainT_prf thy (atyp_map, constraints) =
+  let
+    fun hyp_map hyp =
+      (case AList.lookup (op =) constraints hyp of
+        SOME t => Hyp t
+      | NONE => raise Fail "unconstrainT_prf: missing constraint");
+
+    val typ = Term_Subst.map_atypsT_same (Type.strip_sorts o atyp_map);
+    fun ofclass (ty, c) =
+      let val ty' = Term.map_atyps atyp_map ty;
+      in the_single (of_sort_proof thy hyp_map (ty', [c])) end;
+  in
+    Same.commit (map_proof_same (Term_Subst.map_types_same typ) typ ofclass)
+    #> fold_rev (implies_intr_proof o snd) constraints
+  end;
+
+fun unconstrainT_body thy constrs (PBody {oracles, thms, proof}) =
+  PBody
+   {oracles = oracles,  (* FIXME merge (!), unconstrain (!?!) *)
+    thms = thms,  (* FIXME merge (!) *)
+    proof = unconstrainT_prf thy constrs proof};
 
 
 (***** theorems *****)
 
-fun thm_proof thy name hyps concl promises body =
+fun prepare_thm_proof do_unconstrain thy name shyps hyps concl promises body =
   let
     val PBody {oracles = oracles0, thms = thms0, proof = prf} = body;
     val prop = Logic.list_implies (hyps, concl);
@@ -1387,24 +1418,48 @@
         if member (op =) nvs ixn then SOME v else NONE) (vars_of prop) @
       map SOME (frees_of prop);
 
+    val (postproc, ofclasses, prop1, args1) =
+      if do_unconstrain then
+        let
+          val ((atyp_map, constraints), prop1) = Logic.unconstrainT shyps prop;
+          val postproc = unconstrainT_body thy (atyp_map, constraints);
+          val args1 =
+            (map o Option.map o Term.map_types o Term.map_atyps)
+              (Type.strip_sorts o atyp_map) args;
+        in (postproc, map (OfClass o fst) constraints, prop1, args1) end
+      else (I, [], prop, args);
+    val argsP = ofclasses @ map Hyp hyps;
+
     val proof0 =
       if ! proofs = 2 then
         #4 (shrink_proof [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf)))
       else MinProof;
     val body0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
 
-    fun new_prf () = (serial (), name, prop, fulfill_proof_future thy promises body0);
-    val (i, name, prop, body') =
+    fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);
+    val (i, body') =
       (case strip_combt (fst (strip_combP prf)) of
         (PThm (i, ((old_name, prop', NONE), body')), args') =>
-          if (old_name = "" orelse old_name = name) andalso prop = prop' andalso args = args'
-          then (i, name, prop, body')
+          if (old_name = "" orelse old_name = name) andalso prop1 = prop' andalso args = args'
+          then (i, body')
           else new_prf ()
       | _ => new_prf ());
-    val head = PThm (i, ((name, prop, NONE), body'));
-  in
-    ((i, (name, prop, body')), proof_combP (proof_combt' (head, args), map Hyp hyps))
-  end;
+    val head = PThm (i, ((name, prop1, NONE), body'));
+  in ((i, (name, prop1, body')), head, args, argsP, args1) end;
+
+val unconstrain_thm_proofs = Unsynchronized.ref false;
+
+fun thm_proof thy name shyps hyps concl promises body =
+  let val (pthm, head, args, argsP, _) =
+    prepare_thm_proof (! unconstrain_thm_proofs) thy name shyps hyps concl promises body
+  in (pthm, proof_combP (proof_combt' (head, args), argsP)) end;
+
+fun unconstrain_thm_proof thy shyps concl promises body =
+  let
+    val (pthm, head, _, _, args) =
+      prepare_thm_proof true thy "" shyps [] concl promises body
+  in (pthm, proof_combt' (head, args)) end;
+
 
 fun get_name hyps prop prf =
   let val prop = Logic.list_implies (hyps, prop) in
@@ -1413,6 +1468,20 @@
     | _ => "")
   end;
 
+fun get_name_unconstrained shyps hyps prop prf =
+  let val (_, prop) = Logic.unconstrainT shyps (Logic.list_implies (hyps, prop)) in
+    (case strip_combt (fst (strip_combP prf)) of
+      (PThm (_, ((name, prop', _), _)), _) => if prop = prop' then name else ""
+    | _ => "")
+  end;
+
+fun guess_name (PThm (_, ((name, _, _), _))) = name
+  | guess_name (prf %% Hyp _) = guess_name prf
+  | guess_name (prf %% OfClass _) = guess_name prf
+  | guess_name (prf % NONE) = guess_name prf
+  | guess_name (prf % SOME (Var _)) = guess_name prf
+  | guess_name _ = "";
+
 end;
 
 structure Basic_Proofterm : BASIC_PROOFTERM = Proofterm;

--- a/src/Pure/thm.ML	Fri May 14 23:35:35 2010 +0200
+++ b/src/Pure/thm.ML	Sat May 15 13:31:25 2010 +0200
@@ -586,17 +586,17 @@
 (* closed derivations with official name *)
 
 fun derivation_name thm =
-  Pt.get_name (hyps_of thm) (prop_of thm) (Pt.proof_of (raw_body thm));
+  Pt.guess_name (Pt.proof_of (raw_body thm));   (* FIXME tmp *)
 
 fun name_derivation name (thm as Thm (der, args)) =
   let
     val Deriv {promises, body} = der;
-    val {thy_ref, hyps, prop, tpairs, ...} = args;
+    val {thy_ref, shyps, hyps, prop, tpairs, ...} = args;
     val _ = null tpairs orelse raise THM ("put_name: unsolved flex-flex constraints", 0, [thm]);
 
     val ps = map (apsnd (Future.map proof_body_of)) promises;
     val thy = Theory.deref thy_ref;
-    val (pthm, proof) = Pt.thm_proof thy name hyps prop ps body;
+    val (pthm, proof) = Pt.thm_proof thy name shyps hyps prop ps body;
     val der' = make_deriv [] [] [pthm] proof;
     val _ = Theory.check_thy thy;
   in Thm (der', args) end;
@@ -1222,24 +1222,30 @@
       end;
 
 (*Internalize sort constraints of type variables*)
-fun unconstrainT (thm as Thm (_, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) =
+fun unconstrainT (thm as Thm (der, args)) =
   let
+    val Deriv {promises, body} = der;
+    val {thy_ref, shyps, hyps, tpairs, prop, ...} = args;
+
     fun err msg = raise THM ("unconstrainT: " ^ msg, 0, [thm]);
-
     val _ = null hyps orelse err "illegal hyps";
     val _ = null tpairs orelse err "unsolved flex-flex constraints";
     val tfrees = rev (Term.add_tfree_names prop []);
     val _ = null tfrees orelse err ("illegal free type variables " ^ commas_quote tfrees);
 
-    val (_, prop') = Logic.unconstrainT shyps prop;
+    val ps = map (apsnd (Future.map proof_body_of)) promises;
+    val thy = Theory.deref thy_ref;
+    val (pthm as (_, (_, prop', _)), proof) = Pt.unconstrain_thm_proof thy shyps prop ps body;
+    val der' = make_deriv [] [] [pthm] proof;
+    val _ = Theory.check_thy thy;
   in
-    Thm (deriv_rule0 (Pt.PAxm ("Pure.unconstrainT", prop, SOME [])),
+    Thm (der',
      {thy_ref = thy_ref,
       tags = [],
       maxidx = maxidx_of_term prop',
       shyps = [[]],  (*potentially redundant*)
-      hyps = hyps,
-      tpairs = tpairs,
+      hyps = [],
+      tpairs = [],
       prop = prop'})
   end;