# HG changeset patch # User haftmann # Date 1233692781 -3600 # Node ID 08ef36ed2f8ad624a3c01cf4f25dc6fc37371201 # Parent a342da8ddf3986ca639fdef9a389d1fd3f1e98af handling type classes without parameters diff -r a342da8ddf39 -r 08ef36ed2f8a NEWS --- 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. diff -r a342da8ddf39 -r 08ef36ed2f8a src/HOL/Finite_Set.thy --- 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 \ 'a set)" setup {* Sign.parent_path *} hide const finite diff -r a342da8ddf39 -r 08ef36ed2f8a src/HOL/Library/Countable.thy --- 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: "\to_nat \ 'a \ nat. inj to_nat" lemma countable_classI: diff -r a342da8ddf39 -r 08ef36ed2f8a src/HOL/Library/Enum.thy --- 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 \ 'a set)" - unfolding UNIV_enum .. +subclass finite proof +qed (simp add: UNIV_enum) lemma enum_all: "set enum = UNIV" unfolding UNIV_enum .. diff -r a342da8ddf39 -r 08ef36ed2f8a src/HOL/Typedef.thy --- 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 \ 'b)" - -instance .. - -end - -hide (open) const itself - -end diff -r a342da8ddf39 -r 08ef36ed2f8a src/Pure/Isar/class.ML --- 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 diff -r a342da8ddf39 -r 08ef36ed2f8a src/Pure/Isar/expression.ML --- 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) =