--- a/NEWS Tue Apr 27 11:17:50 2010 -0700
+++ b/NEWS Tue Apr 27 22:23:12 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/HOL/Nominal/nominal_datatype.ML Tue Apr 27 11:17:50 2010 -0700
+++ b/src/HOL/Nominal/nominal_datatype.ML Tue Apr 27 22:23:12 2010 +0200
@@ -215,7 +215,7 @@
fun inter_sort thy S S' = Type.inter_sort (Sign.tsig_of thy) (S, S');
fun augment_sort_typ thy S =
- let val S = Sign.certify_sort thy S
+ let val S = Sign.minimize_sort thy (Sign.certify_sort thy S)
in map_type_tfree (fn (s, S') => TFree (s,
if member (op = o apsnd fst) sorts s then inter_sort thy S S' else S'))
end;
@@ -449,7 +449,7 @@
at_inst RS (pt_inst RS pt_perm_compose) RS sym,
at_inst RS (pt_inst RS pt_perm_compose_rev) RS sym]
end))
- val sort = Sign.certify_sort thy (cp_class :: pt_class);
+ val sort = Sign.minimize_sort thy (Sign.certify_sort thy (cp_class :: pt_class));
val thms = split_conj_thm (Goal.prove_global thy [] []
(augment_sort thy sort
(HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
@@ -654,8 +654,8 @@
perm_def), name), tvs), perm_closed) => fn thy =>
let
val pt_class = pt_class_of thy atom;
- val sort = Sign.certify_sort thy
- (pt_class :: map (cp_class_of thy atom) (remove (op =) atom dt_atoms))
+ val sort = Sign.minimize_sort thy (Sign.certify_sort thy
+ (pt_class :: map (cp_class_of thy atom) (remove (op =) atom dt_atoms)))
in AxClass.prove_arity
(Sign.intern_type thy name,
map (inter_sort thy sort o snd) tvs, [pt_class])
@@ -678,10 +678,10 @@
fun cp_instance (atom1, perm_closed_thms1) (atom2, perm_closed_thms2) thy =
let
val cp_class = cp_class_of thy atom1 atom2;
- val sort = Sign.certify_sort thy
+ val sort = Sign.minimize_sort thy (Sign.certify_sort thy
(pt_class_of thy atom1 :: map (cp_class_of thy atom1) (remove (op =) atom1 dt_atoms) @
(if atom1 = atom2 then [cp_class_of thy atom1 atom1] else
- pt_class_of thy atom2 :: map (cp_class_of thy atom2) (remove (op =) atom2 dt_atoms)));
+ pt_class_of thy atom2 :: map (cp_class_of thy atom2) (remove (op =) atom2 dt_atoms))));
val cp1' = cp_inst_of thy atom1 atom2 RS cp1
in fold (fn ((((((Abs_inverse, Rep),
perm_def), name), tvs), perm_closed1), perm_closed2) => fn thy =>
@@ -1131,7 +1131,7 @@
fold (fn (atom, ths) => fn thy =>
let
val class = fs_class_of thy atom;
- val sort = Sign.certify_sort thy (class :: pt_cp_sort)
+ val sort = Sign.minimize_sort thy (Sign.certify_sort thy (class :: pt_cp_sort));
in fold (fn Type (s, Ts) => AxClass.prove_arity
(s, map (inter_sort thy sort o snd o dest_TFree) Ts, [class])
(Class.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy
@@ -1142,7 +1142,7 @@
val pnames = if length descr'' = 1 then ["P"]
else map (fn i => "P" ^ string_of_int i) (1 upto length descr'');
val ind_sort = if null dt_atomTs then HOLogic.typeS
- else Sign.certify_sort thy9 (map (fs_class_of thy9) dt_atoms);
+ else Sign.minimize_sort thy9 (Sign.certify_sort thy9 (map (fs_class_of thy9) dt_atoms));
val fsT = TFree ("'n", ind_sort);
val fsT' = TFree ("'n", HOLogic.typeS);
@@ -1423,7 +1423,7 @@
val (rec_result_Ts', rec_fn_Ts') = Datatype_Prop.make_primrec_Ts descr' sorts used;
val rec_sort = if null dt_atomTs then HOLogic.typeS else
- Sign.certify_sort thy10 pt_cp_sort;
+ Sign.minimize_sort thy10 (Sign.certify_sort thy10 pt_cp_sort);
val rec_result_Ts = map (fn TFree (s, _) => TFree (s, rec_sort)) rec_result_Ts';
val rec_fn_Ts = map (typ_subst_atomic (rec_result_Ts' ~~ rec_result_Ts)) rec_fn_Ts';
--- a/src/HOL/Nominal/nominal_inductive.ML Tue Apr 27 11:17:50 2010 -0700
+++ b/src/HOL/Nominal/nominal_inductive.ML Tue Apr 27 22:23:12 2010 +0200
@@ -198,8 +198,8 @@
val atomTs = distinct op = (maps (map snd o #2) prems);
val ind_sort = if null atomTs then HOLogic.typeS
- else Sign.certify_sort thy (map (fn T => Sign.intern_class thy
- ("fs_" ^ Long_Name.base_name (fst (dest_Type T)))) atomTs);
+ else Sign.minimize_sort thy (Sign.certify_sort thy (map (fn T => Sign.intern_class thy
+ ("fs_" ^ Long_Name.base_name (fst (dest_Type T)))) atomTs));
val ([fs_ctxt_tyname], _) = Name.variants ["'n"] (Variable.names_of ctxt');
val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt';
val fsT = TFree (fs_ctxt_tyname, ind_sort);
--- a/src/HOL/Nominal/nominal_inductive2.ML Tue Apr 27 11:17:50 2010 -0700
+++ b/src/HOL/Nominal/nominal_inductive2.ML Tue Apr 27 22:23:12 2010 +0200
@@ -223,8 +223,8 @@
val atomTs = distinct op = (maps (map snd o #2) prems);
val atoms = map (fst o dest_Type) atomTs;
val ind_sort = if null atomTs then HOLogic.typeS
- else Sign.certify_sort thy (map (fn a => Sign.intern_class thy
- ("fs_" ^ Long_Name.base_name a)) atoms);
+ else Sign.minimize_sort thy (Sign.certify_sort thy (map (fn a => Sign.intern_class thy
+ ("fs_" ^ Long_Name.base_name a)) atoms));
val ([fs_ctxt_tyname], _) = Name.variants ["'n"] (Variable.names_of ctxt');
val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt';
val fsT = TFree (fs_ctxt_tyname, ind_sort);
--- a/src/Pure/Isar/proof_context.ML Tue Apr 27 11:17:50 2010 -0700
+++ b/src/Pure/Isar/proof_context.ML Tue Apr 27 22:23:12 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/axclass.ML Tue Apr 27 11:17:50 2010 -0700
+++ b/src/Pure/axclass.ML Tue Apr 27 22:23:12 2010 +0200
@@ -7,35 +7,35 @@
signature AX_CLASS =
sig
- val define_class: binding * class list -> string list ->
- (Thm.binding * term list) list -> theory -> class * theory
+ type info = {def: thm, intro: thm, axioms: thm list, params: (string * typ) list}
+ val get_info: theory -> class -> info
+ val class_of_param: theory -> string -> class option
+ val instance_name: string * class -> string
+ val thynames_of_arity: theory -> class * string -> string list
+ val param_of_inst: theory -> string * string -> string
+ val inst_of_param: theory -> string -> (string * string) option
+ val unoverload: theory -> thm -> thm
+ val overload: theory -> thm -> thm
+ val unoverload_conv: theory -> conv
+ val overload_conv: theory -> conv
+ val lookup_inst_param: Consts.T -> ((string * string) * 'a) list -> string * typ -> 'a option
+ val unoverload_const: theory -> string * typ -> string
+ val cert_classrel: theory -> class * class -> class * class
+ val read_classrel: theory -> xstring * xstring -> class * class
+ val declare_overloaded: string * typ -> theory -> term * theory
+ val define_overloaded: binding -> string * term -> theory -> thm * theory
val add_classrel: thm -> theory -> theory
val add_arity: thm -> theory -> theory
val prove_classrel: class * class -> tactic -> theory -> theory
val prove_arity: string * sort list * sort -> tactic -> theory -> theory
- type info = {def: thm, intro: thm, axioms: thm list, params: (string * typ) list}
- val get_info: theory -> class -> info
- val class_of_param: theory -> string -> class option
- val cert_classrel: theory -> class * class -> class * class
- val read_classrel: theory -> xstring * xstring -> class * class
+ val define_class: binding * class list -> string list ->
+ (Thm.binding * term list) list -> theory -> class * theory
val axiomatize_class: binding * class list -> theory -> theory
val axiomatize_class_cmd: binding * xstring list -> theory -> theory
val axiomatize_classrel: (class * class) list -> theory -> theory
val axiomatize_classrel_cmd: (xstring * xstring) list -> theory -> theory
val axiomatize_arity: arity -> theory -> theory
val axiomatize_arity_cmd: xstring * string list * string -> theory -> theory
- val instance_name: string * class -> string
- val declare_overloaded: string * typ -> theory -> term * theory
- val define_overloaded: binding -> string * term -> theory -> thm * theory
- val unoverload: theory -> thm -> thm
- val overload: theory -> thm -> thm
- val unoverload_conv: theory -> conv
- val overload_conv: theory -> conv
- val unoverload_const: theory -> string * typ -> string
- val lookup_inst_param: Consts.T -> ((string * string) * 'a) list -> string * typ -> 'a option
- val param_of_inst: theory -> string * string -> string
- val inst_of_param: theory -> string -> (string * string) option
- val thynames_of_arity: theory -> class * string -> string list
end;
structure AxClass: AX_CLASS =
@@ -445,7 +445,6 @@
|> maps (these o Option.map #params o try (get_info thy))
|> filter_out (fn (const, _) => can (get_inst_param thy) (const, t))
|> (map o apsnd o map_atyps) (K T);
- val _ = map (Sign.certify_sort thy) Ss = Ss orelse err ();
val th' = th
|> Drule.instantiate' std_vars []
|> Thm.unconstrain_allTs;
--- a/src/Pure/sorts.ML Tue Apr 27 11:17:50 2010 -0700
+++ b/src/Pure/sorts.ML Tue Apr 27 22:23:12 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);