monotonic sort certification: sorts are no longer minimized at the kernel boundary, only when reading input from the end-user;
--- a/NEWS Tue Apr 27 21:34:22 2010 +0200
+++ b/NEWS Tue Apr 27 21:46:10 2010 +0200
@@ -295,6 +295,14 @@
*** ML ***
+* Sorts.certify_sort and derived "cert" operations for types and terms
+no longer minimize sorts. Thus certification at the boundary of the
+inference kernel becomes invariant under addition of class relations,
+which is an important monotonicity principle. Sorts are now minimized
+in the syntax layer only, at the boundary between the end-user and the
+system. Subtle INCOMPATIBILITY, may have to use Sign.minimize_sort
+explicitly in rare situations.
+
* Antiquotations for basic formal entities:
@{class NAME} -- type class
--- a/src/Pure/Isar/proof_context.ML Tue Apr 27 21:34:22 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML Tue Apr 27 21:46:10 2010 +0200
@@ -610,6 +610,7 @@
fun get_sort ctxt raw_env =
let
+ val thy = theory_of ctxt;
val tsig = tsig_of ctxt;
fun eq ((xi, S), (xi', S')) =
@@ -636,7 +637,7 @@
else error ("Sort constraint " ^ Syntax.string_of_sort ctxt S ^
" inconsistent with default " ^ Syntax.string_of_sort ctxt S' ^
" for type variable " ^ quote (Term.string_of_vname' xi)));
- in get end;
+ in Sign.minimize_sort thy o get end;
fun check_tvar ctxt (xi, S) = (xi, get_sort ctxt [(xi, S)] xi);
fun check_tfree ctxt (x, S) = apfst fst (check_tvar ctxt ((x, ~1), S));
@@ -736,10 +737,11 @@
fun parse_sort ctxt text =
let
+ val thy = theory_of ctxt;
val (syms, pos) = Syntax.parse_token Markup.sort text;
val S = Syntax.standard_parse_sort ctxt (syn_of ctxt) (syms, pos)
handle ERROR msg => cat_error msg ("Failed to parse sort" ^ Position.str_of pos)
- in S end;
+ in Sign.minimize_sort thy S end;
fun parse_typ ctxt text =
let
--- a/src/Pure/sorts.ML Tue Apr 27 21:34:22 2010 +0200
+++ b/src/Pure/sorts.ML Tue Apr 27 21:46:10 2010 +0200
@@ -189,7 +189,7 @@
if can (Graph.get_node (classes_of algebra)) c then c
else raise TYPE ("Undeclared class: " ^ quote c, [], []);
-fun certify_sort classes = minimize_sort classes o map (certify_class classes);
+fun certify_sort classes = map (certify_class classes);