# HG changeset patch
# User wenzelm
# Date 1564418679 -7200
# Node ID 52435af442a66890ff9f0ba818376e7d032987d9
# Parent  4abd07cd034f41750c269ce3b3c66bd306cd6284# Parent  03cfef16ddb4551080f8d546fa65a7a92cbb177d
merged

diff -r 4abd07cd034f -r 52435af442a6 src/HOL/Types_To_Sets/internalize_sort.ML
--- a/src/HOL/Types_To_Sets/internalize_sort.ML	Mon Jul 29 16:26:06 2019 +0200
+++ b/src/HOL/Types_To_Sets/internalize_sort.ML	Mon Jul 29 18:44:39 2019 +0200
@@ -31,14 +31,14 @@
     val thy = Thm.theory_of_thm thm;
     val tvar = Thm.typ_of ctvar;
 
-    val ((_, assms, classes),_) = Logic.unconstrainT [] (Thm.prop_of thm);
+    val (ucontext, _) = Logic.unconstrainT [] (Thm.prop_of thm);
 
     fun is_proper_class thy = can (Axclass.get_info thy); (* trick by FH *)
     fun reduce_to_non_proper_sort (TVar (name, sort)) =
         TVar (name, Sign.minimize_sort thy (filter_out (is_proper_class thy) (Sign.complete_sort thy sort)))
       | reduce_to_non_proper_sort _ = error "not supported";
 
-    val data = (map fst classes) ~~ assms;
+    val data = map #1 (#outer_constraints ucontext) ~~ #constraints ucontext;
 
     val new_tvar = get_first (fn (tvar', ((ren_tvar, _), _)) => if tvar = tvar'
       then SOME (reduce_to_non_proper_sort ren_tvar) else NONE) data
diff -r 4abd07cd034f -r 52435af442a6 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Mon Jul 29 16:26:06 2019 +0200
+++ b/src/Pure/Proof/extraction.ML	Mon Jul 29 18:44:39 2019 +0200
@@ -365,7 +365,7 @@
 fun abs_corr_shyps thy thm vs xs prf =
   let
     val S = Sign.defaultS thy;
-    val ((atyp_map, constraints, _), prop') =
+    val (ucontext, prop') =
       Logic.unconstrainT (Thm.shyps_of thm) (Thm.prop_of thm);
     val atyps = fold_types (fold_atyps (insert (op =))) (Thm.prop_of thm) [];
     val Ts = map_filter (fn ((v, i), _) => if member (op =) vs v then
@@ -374,13 +374,13 @@
     val cs = maps (fn T => map (pair T) S) Ts;
     val constraints' = map Logic.mk_of_class cs;
     fun typ_map T = Type.strip_sorts
-      (map_atyps (fn U => if member (op =) atyps U then atyp_map U else U) T);
+      (map_atyps (fn U => if member (op =) atyps U then (#atyp_map ucontext) U else U) T);
     fun mk_hyp (T, c) = Hyp (Logic.mk_of_class (typ_map T, c));
     val xs' = map (map_types typ_map) xs
   in
     prf |>
     Same.commit (Proofterm.map_proof_same (map_types typ_map) typ_map mk_hyp) |>
-    fold_rev Proofterm.implies_intr_proof' (map snd constraints) |>
+    fold_rev Proofterm.implies_intr_proof' (map snd (#constraints ucontext)) |>
     fold_rev Proofterm.forall_intr_proof' xs' |>
     fold_rev Proofterm.implies_intr_proof' constraints'
   end;
diff -r 4abd07cd034f -r 52435af442a6 src/Pure/Proof/reconstruct.ML
diff -r 4abd07cd034f -r 52435af442a6 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Mon Jul 29 16:26:06 2019 +0200
+++ b/src/Pure/logic.ML	Mon Jul 29 18:44:39 2019 +0200
@@ -56,8 +56,14 @@
   val mk_arities: arity -> term list
   val mk_arity: string * sort list * class -> term
   val dest_arity: term -> string * sort list * class
-  val unconstrainT: sort list -> term ->
-    ((typ -> typ) * ((typ * class) * term) list * (typ * class) list) * term
+  type unconstrain_context =
+   {present_map: (typ * typ) list,
+    constraints_map: (sort * typ) list,
+    atyp_map: typ -> typ,
+    map_atyps: typ -> typ,
+    constraints: ((typ * class) * term) list,
+    outer_constraints: (typ * class) list};
+  val unconstrainT: sort list -> term -> unconstrain_context * term
   val protectC: term
   val protect: term -> term
   val unprotect: term -> term
@@ -339,6 +345,14 @@
 
 (* internalized sort constraints *)
 
+type unconstrain_context =
+ {present_map: (typ * typ) list,
+  constraints_map: (sort * typ) list,
+  atyp_map: typ -> typ,
+  map_atyps: typ -> typ,
+  constraints: ((typ * class) * term) list,
+  outer_constraints: (typ * class) list};
+
 fun unconstrainT shyps prop =
   let
     val present = rev ((fold_types o fold_atyps_sorts) (insert (eq_fst op =)) prop []);
@@ -362,19 +376,25 @@
           | NONE => raise TYPE ("Dangling type variable", [T], [])));
 
     val constraints =
-      maps (fn (_, T as TVar (ai, S)) =>
-        map (fn c => ((T, c), mk_of_class (TVar (ai, []), c))) S)
-        constraints_map;
+      constraints_map |> maps (fn (_, T as TVar (ai, S)) =>
+        map (fn c => ((T, c), mk_of_class (TVar (ai, []), c))) S);
 
     val outer_constraints =
       maps (fn (T, S) => map (pair T) S)
         (present @ map (fn S => (TFree ("'dummy", S), S)) extra);
 
-    val prop' =
-      prop
-      |> (Term.map_types o Term.map_atyps) (Type.strip_sorts o atyp_map)
-      |> curry list_implies (map snd constraints);
-  in ((atyp_map, constraints, outer_constraints), prop') end;
+    val map_atyps = Term.map_atyps (Type.strip_sorts o atyp_map);
+    val ucontext =
+     {present_map = present_map,
+      constraints_map = constraints_map,
+      atyp_map = atyp_map,
+      map_atyps = map_atyps,
+      constraints = constraints,
+      outer_constraints = outer_constraints};
+    val prop' = prop
+      |> Term.map_types map_atyps
+      |> curry list_implies (map #2 constraints);
+  in (ucontext, prop') end;
 
 
 
diff -r 4abd07cd034f -r 52435af442a6 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Mon Jul 29 16:26:06 2019 +0200
+++ b/src/Pure/proofterm.ML	Mon Jul 29 18:44:39 2019 +0200
@@ -54,8 +54,9 @@
   val unions_thms: pthm Ord_List.T list -> pthm Ord_List.T
   val all_oracles_of: proof_body -> oracle Ord_List.T
   val approximate_proof_body: proof -> proof_body
-  val no_proof_body: proof_body
+  val no_proof_body: proof -> proof_body
   val no_thm_proofs: proof -> proof
+  val no_body_proofs: proof -> proof
 
   val encode: proof XML.Encode.T
   val encode_body: proof_body XML.Encode.T
@@ -310,8 +311,8 @@
       proof = prf}
   end;
 
-val no_proof_body = PBody {oracles = [], thms = [], proof = MinProof};
-val no_body = Future.value no_proof_body;
+fun no_proof_body proof = PBody {oracles = [], thms = [], proof = proof};
+val no_body = Future.value (no_proof_body MinProof);
 
 fun no_thm_proofs (PThm (i, (a, _))) = PThm (i, (a, no_body))
   | no_thm_proofs (Abst (x, T, prf)) = Abst (x, T, no_thm_proofs prf)
@@ -320,6 +321,14 @@
   | no_thm_proofs (prf1 %% prf2) = no_thm_proofs prf1 %% no_thm_proofs prf2
   | no_thm_proofs a = a;
 
+fun no_body_proofs (PThm (i, (a, body))) =
+      PThm (i, (a, Future.value (no_proof_body (join_proof body))))
+  | no_body_proofs (Abst (x, T, prf)) = Abst (x, T, no_body_proofs prf)
+  | no_body_proofs (AbsP (x, t, prf)) = AbsP (x, t, no_body_proofs prf)
+  | no_body_proofs (prf % t) = no_body_proofs prf % t
+  | no_body_proofs (prf1 %% prf2) = no_body_proofs prf1 %% no_body_proofs prf2
+  | no_body_proofs a = a;
+
 
 
 (** XML data representation **)
@@ -1670,38 +1679,28 @@
 
 
 
-(** 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 **)
 
 val proof_serial = Counter.make ();
 
 local
 
+fun unconstrainT_prf thy (ucontext: Logic.unconstrain_context) =
+  let
+    fun hyp_map hyp =
+      (case AList.lookup (op =) (#constraints ucontext) 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 ucontext);
+    fun ofclass (ty, c) =
+      let val ty' = Term.map_atyps (#atyp_map ucontext) 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 ucontext)
+  end;
+
 fun export thy i proof =
   if Options.default_bool "export_proofs" then
     Export.export thy (Path.binding0 (Path.make ["proofs", string_of_int i]))
@@ -1719,11 +1718,7 @@
     val prop = Logic.list_implies (hyps, concl);
     val args = prop_args prop;
 
-    val ((atyp_map, constraints, outer_constraints), prop1) = Logic.unconstrainT shyps prop;
-    val args1 =
-      (map o Option.map o Term.map_types o Term.map_atyps)
-        (Type.strip_sorts o atyp_map) args;
-    val argsP = map OfClass outer_constraints @ map Hyp hyps;
+    val (ucontext, prop1) = Logic.unconstrainT shyps prop;
 
     val PBody {oracles = oracles0, thms = thms0, proof = prf} = body;
     val body0 =
@@ -1737,7 +1732,7 @@
     fun new_prf () =
       let
         val i = proof_serial ();
-        val postproc = unconstrainT_body thy (atyp_map, constraints) #> named ? publish i;
+        val postproc = map_proof_of (unconstrainT_prf thy ucontext) #> named ? publish i;
       in (i, fulfill_proof_future thy promises postproc body0) end;
 
     val (i, body') =
@@ -1753,9 +1748,11 @@
 
     val head = PThm (i, ((name, prop1, NONE, open_proof), body'));
     val proof =
-      if unconstrain
-      then proof_combt' (head, args1)
-      else proof_combP (proof_combt' (head, args), argsP);
+      if unconstrain then
+        proof_combt' (head, (map o Option.map o Term.map_types) (#map_atyps ucontext) args)
+      else
+        proof_combP (proof_combt' (head, args),
+          map OfClass (#outer_constraints ucontext) @ map Hyp hyps);
   in (pthm, proof) end;
 
 in