--- 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
--- 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;
--- 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;
--- 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