--- a/NEWS Tue Feb 03 19:48:06 2009 +0100
+++ b/NEWS Tue Feb 03 21:26:21 2009 +0100
@@ -193,6 +193,9 @@
*** HOL ***
+* Auxiliary class "itself" has disappeared -- classes without any parameter
+are treated as expected by the 'class' command.
+
* Theory "Reflection" now resides in HOL/Library. Common reflection examples
(Cooper, MIR, Ferrack) now in distinct session directory HOL/Reflection.
--- a/src/HOL/Finite_Set.thy Tue Feb 03 19:48:06 2009 +0100
+++ b/src/HOL/Finite_Set.thy Tue Feb 03 21:26:21 2009 +0100
@@ -383,7 +383,7 @@
subsection {* Class @{text finite} *}
setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
-class finite = itself +
+class finite =
assumes finite_UNIV: "finite (UNIV \<Colon> 'a set)"
setup {* Sign.parent_path *}
hide const finite
--- a/src/HOL/Library/Countable.thy Tue Feb 03 19:48:06 2009 +0100
+++ b/src/HOL/Library/Countable.thy Tue Feb 03 21:26:21 2009 +0100
@@ -10,7 +10,7 @@
subsection {* The class of countable types *}
-class countable = itself +
+class countable =
assumes ex_inj: "\<exists>to_nat \<Colon> 'a \<Rightarrow> nat. inj to_nat"
lemma countable_classI:
--- a/src/HOL/Library/Enum.thy Tue Feb 03 19:48:06 2009 +0100
+++ b/src/HOL/Library/Enum.thy Tue Feb 03 21:26:21 2009 +0100
@@ -11,14 +11,14 @@
subsection {* Class @{text enum} *}
-class enum = itself +
+class enum =
fixes enum :: "'a list"
assumes UNIV_enum [code]: "UNIV = set enum"
and enum_distinct: "distinct enum"
begin
-lemma finite_enum: "finite (UNIV \<Colon> 'a set)"
- unfolding UNIV_enum ..
+subclass finite proof
+qed (simp add: UNIV_enum)
lemma enum_all: "set enum = UNIV" unfolding UNIV_enum ..
--- a/src/HOL/Typedef.thy Tue Feb 03 19:48:06 2009 +0100
+++ b/src/HOL/Typedef.thy Tue Feb 03 21:26:21 2009 +0100
@@ -119,52 +119,4 @@
use "Tools/typecopy_package.ML" setup TypecopyPackage.setup
use "Tools/typedef_codegen.ML" setup TypedefCodegen.setup
-
-text {* This class is just a workaround for classes without parameters;
- it shall disappear as soon as possible. *}
-
-class itself =
- fixes itself :: "'a itself"
-
-setup {*
-let fun add_itself tyco thy =
- let
- val vs = Name.names Name.context "'a"
- (replicate (Sign.arity_number thy tyco) @{sort type});
- val ty = Type (tyco, map TFree vs);
- val lhs = Const (@{const_name itself}, Term.itselfT ty);
- val rhs = Logic.mk_type ty;
- val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
- in
- thy
- |> TheoryTarget.instantiation ([tyco], vs, @{sort itself})
- |> `(fn lthy => Syntax.check_term lthy eq)
- |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
- |> snd
- |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
- |> LocalTheory.exit_global
- end
-in TypedefPackage.interpretation add_itself end
-*}
-
-instantiation bool :: itself
-begin
-
-definition "itself = TYPE(bool)"
-
-instance ..
-
end
-
-instantiation "fun" :: ("type", "type") itself
-begin
-
-definition "itself = TYPE('a \<Rightarrow> 'b)"
-
-instance ..
-
-end
-
-hide (open) const itself
-
-end
--- a/src/Pure/Isar/class.ML Tue Feb 03 19:48:06 2009 +0100
+++ b/src/Pure/Isar/class.ML Tue Feb 03 21:26:21 2009 +0100
@@ -41,9 +41,16 @@
(Const o apsnd (map_atyps (K aT))) param_map;
val const_morph = Element.inst_morphism thy
(Symtab.empty, Symtab.make param_map_inst);
- val (([props], [(_, inst_morph)], export_morph), _) = empty_ctxt
+ val typ_morph = Element.inst_morphism thy
+ (Symtab.empty |> Symtab.update (Name.aT, TFree (Name.aT, [class])), Symtab.empty);
+ val (([raw_props], [(_, raw_inst_morph)], export_morph), _) = empty_ctxt
|> Expression.cert_goal_expression ([(class, (("", false),
Expression.Named param_map_const))], []);
+ val (props, inst_morph) = if null param_map
+ then (raw_props |> map (Morphism.term typ_morph),
+ raw_inst_morph $> typ_morph)
+ else (raw_props, raw_inst_morph); (*FIXME proper handling in
+ locale.ML / expression.ML would be desirable*)
(* witness for canonical interpretation *)
val prop = try the_single props;
@@ -162,7 +169,7 @@
|> Sign.minimize_sort thy;
val _ = case filter_out (is_class thy) sups
of [] => ()
- | no_classes => error ("No proper classes: " ^ commas (map quote no_classes));
+ | no_classes => error ("No (proper) classes: " ^ commas (map quote no_classes));
val supparams = (map o apsnd) (snd o snd) (these_params thy sups);
val supparam_names = map fst supparams;
val _ = if has_duplicates (op =) supparam_names
--- a/src/Pure/Isar/expression.ML Tue Feb 03 19:48:06 2009 +0100
+++ b/src/Pure/Isar/expression.ML Tue Feb 03 21:26:21 2009 +0100
@@ -100,7 +100,7 @@
(* FIXME: cannot compare bindings for equality. *)
fun params_loc loc =
- (Locale.params_of thy loc |> map (fn (p, _, mx) => (p, mx)), loc);
+ (Locale.params_of thy loc |> map (fn (p, _, mx) => (p, mx)), loc);
fun params_inst (expr as (loc, (prfx, Positional insts))) =
let
val (ps, loc') = params_loc loc;
@@ -150,14 +150,14 @@
local
-fun prep_inst parse_term ctxt parms (Positional insts) =
+fun prep_inst prep_term ctxt parms (Positional insts) =
(insts ~~ parms) |> map (fn
- (NONE, p) => Free (p, the (Variable.default_type ctxt p)) |
- (SOME t, _) => parse_term ctxt t)
- | prep_inst parse_term ctxt parms (Named insts) =
+ (NONE, p) => Free (p, dummyT) |
+ (SOME t, _) => prep_term ctxt t)
+ | prep_inst prep_term ctxt parms (Named insts) =
parms |> map (fn p => case AList.lookup (op =) insts p of
- SOME t => parse_term ctxt t |
- NONE => Free (p, the (Variable.default_type ctxt p)));
+ SOME t => prep_term ctxt t |
+ NONE => Free (p, dummyT));
in
@@ -350,19 +350,19 @@
local
-fun prep_full_context_statement parse_typ parse_prop prep_vars_elem parse_inst prep_vars_inst prep_expr
+fun prep_full_context_statement parse_typ parse_prop prep_vars_elem prep_inst prep_vars_inst prep_expr
strict do_close raw_import init_body raw_elems raw_concl ctxt1 =
let
val thy = ProofContext.theory_of ctxt1;
val (raw_insts, fixed) = parameters_of thy strict (apfst (prep_expr thy) raw_import);
- fun prep_inst (loc, (prfx, inst)) (i, insts, ctxt) =
+ fun prep_insts (loc, (prfx, inst)) (i, insts, ctxt) =
let
val (parm_names, parm_types) = Locale.params_of thy loc |>
map_split (fn (b, SOME T, _) => (Binding.base_name b, T))
(*FIXME return value of Locale.params_of has strange type*)
- val inst' = parse_inst ctxt parm_names inst;
+ val inst' = prep_inst ctxt parm_names inst;
val parm_types' = map (TypeInfer.paramify_vars o
Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT) parm_types;
val inst'' = map2 TypeInfer.constrain parm_types' inst';
@@ -387,7 +387,7 @@
val fors = prep_vars_inst fixed ctxt1 |> fst;
val ctxt2 = ctxt1 |> ProofContext.add_fixes_i fors |> snd;
- val (_, insts', ctxt3) = fold prep_inst raw_insts (0, [], ctxt2);
+ val (_, insts', ctxt3) = fold prep_insts raw_insts (0, [], ctxt2);
val ctxt4 = init_body ctxt3;
val (elems, ctxt5) = fold (prep_elem insts') raw_elems ([], ctxt4);
val (insts, elems', concl, ctxt6) =