handling type classes without parameters
authorhaftmann
Tue Feb 03 21:26:21 2009 +0100 (2009-02-03)
changeset 2979708ef36ed2f8a
parent 29796 a342da8ddf39
child 29798 6df726203e39
handling type classes without parameters
NEWS
src/HOL/Finite_Set.thy
src/HOL/Library/Countable.thy
src/HOL/Library/Enum.thy
src/HOL/Typedef.thy
src/Pure/Isar/class.ML
src/Pure/Isar/expression.ML
     1.1 --- a/NEWS	Tue Feb 03 19:48:06 2009 +0100
     1.2 +++ b/NEWS	Tue Feb 03 21:26:21 2009 +0100
     1.3 @@ -193,6 +193,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Auxiliary class "itself" has disappeared -- classes without any parameter
     1.8 +are treated as expected by the 'class' command.
     1.9 +
    1.10  * Theory "Reflection" now resides in HOL/Library.  Common reflection examples
    1.11  (Cooper, MIR, Ferrack) now in distinct session directory HOL/Reflection.
    1.12  
     2.1 --- a/src/HOL/Finite_Set.thy	Tue Feb 03 19:48:06 2009 +0100
     2.2 +++ b/src/HOL/Finite_Set.thy	Tue Feb 03 21:26:21 2009 +0100
     2.3 @@ -383,7 +383,7 @@
     2.4  subsection {* Class @{text finite}  *}
     2.5  
     2.6  setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
     2.7 -class finite = itself +
     2.8 +class finite =
     2.9    assumes finite_UNIV: "finite (UNIV \<Colon> 'a set)"
    2.10  setup {* Sign.parent_path *}
    2.11  hide const finite
     3.1 --- a/src/HOL/Library/Countable.thy	Tue Feb 03 19:48:06 2009 +0100
     3.2 +++ b/src/HOL/Library/Countable.thy	Tue Feb 03 21:26:21 2009 +0100
     3.3 @@ -10,7 +10,7 @@
     3.4  
     3.5  subsection {* The class of countable types *}
     3.6  
     3.7 -class countable = itself +
     3.8 +class countable =
     3.9    assumes ex_inj: "\<exists>to_nat \<Colon> 'a \<Rightarrow> nat. inj to_nat"
    3.10  
    3.11  lemma countable_classI:
     4.1 --- a/src/HOL/Library/Enum.thy	Tue Feb 03 19:48:06 2009 +0100
     4.2 +++ b/src/HOL/Library/Enum.thy	Tue Feb 03 21:26:21 2009 +0100
     4.3 @@ -11,14 +11,14 @@
     4.4  
     4.5  subsection {* Class @{text enum} *}
     4.6  
     4.7 -class enum = itself +
     4.8 +class enum =
     4.9    fixes enum :: "'a list"
    4.10    assumes UNIV_enum [code]: "UNIV = set enum"
    4.11      and enum_distinct: "distinct enum"
    4.12  begin
    4.13  
    4.14 -lemma finite_enum: "finite (UNIV \<Colon> 'a set)"
    4.15 -  unfolding UNIV_enum ..
    4.16 +subclass finite proof
    4.17 +qed (simp add: UNIV_enum)
    4.18  
    4.19  lemma enum_all: "set enum = UNIV" unfolding UNIV_enum ..
    4.20  
     5.1 --- a/src/HOL/Typedef.thy	Tue Feb 03 19:48:06 2009 +0100
     5.2 +++ b/src/HOL/Typedef.thy	Tue Feb 03 21:26:21 2009 +0100
     5.3 @@ -119,52 +119,4 @@
     5.4  use "Tools/typecopy_package.ML" setup TypecopyPackage.setup
     5.5  use "Tools/typedef_codegen.ML" setup TypedefCodegen.setup
     5.6  
     5.7 -
     5.8 -text {* This class is just a workaround for classes without parameters;
     5.9 -  it shall disappear as soon as possible. *}
    5.10 -
    5.11 -class itself = 
    5.12 -  fixes itself :: "'a itself"
    5.13 -
    5.14 -setup {*
    5.15 -let fun add_itself tyco thy =
    5.16 -  let
    5.17 -    val vs = Name.names Name.context "'a"
    5.18 -      (replicate (Sign.arity_number thy tyco) @{sort type});
    5.19 -    val ty = Type (tyco, map TFree vs);
    5.20 -    val lhs = Const (@{const_name itself}, Term.itselfT ty);
    5.21 -    val rhs = Logic.mk_type ty;
    5.22 -    val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
    5.23 -  in
    5.24 -    thy
    5.25 -    |> TheoryTarget.instantiation ([tyco], vs, @{sort itself})
    5.26 -    |> `(fn lthy => Syntax.check_term lthy eq)
    5.27 -    |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
    5.28 -    |> snd
    5.29 -    |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
    5.30 -    |> LocalTheory.exit_global
    5.31 -  end
    5.32 -in TypedefPackage.interpretation add_itself end
    5.33 -*}
    5.34 -
    5.35 -instantiation bool :: itself
    5.36 -begin
    5.37 -
    5.38 -definition "itself = TYPE(bool)"
    5.39 -
    5.40 -instance ..
    5.41 -
    5.42  end
    5.43 -
    5.44 -instantiation "fun" :: ("type", "type") itself
    5.45 -begin
    5.46 -
    5.47 -definition "itself = TYPE('a \<Rightarrow> 'b)"
    5.48 -
    5.49 -instance ..
    5.50 -
    5.51 -end
    5.52 -
    5.53 -hide (open) const itself
    5.54 -
    5.55 -end
     6.1 --- a/src/Pure/Isar/class.ML	Tue Feb 03 19:48:06 2009 +0100
     6.2 +++ b/src/Pure/Isar/class.ML	Tue Feb 03 21:26:21 2009 +0100
     6.3 @@ -41,9 +41,16 @@
     6.4        (Const o apsnd (map_atyps (K aT))) param_map;
     6.5      val const_morph = Element.inst_morphism thy
     6.6        (Symtab.empty, Symtab.make param_map_inst);
     6.7 -    val (([props], [(_, inst_morph)], export_morph), _) = empty_ctxt
     6.8 +    val typ_morph = Element.inst_morphism thy
     6.9 +      (Symtab.empty |> Symtab.update (Name.aT, TFree (Name.aT, [class])), Symtab.empty);
    6.10 +    val (([raw_props], [(_, raw_inst_morph)], export_morph), _) = empty_ctxt
    6.11        |> Expression.cert_goal_expression ([(class, (("", false),
    6.12             Expression.Named param_map_const))], []);
    6.13 +    val (props, inst_morph) = if null param_map
    6.14 +      then (raw_props |> map (Morphism.term typ_morph),
    6.15 +        raw_inst_morph $> typ_morph)
    6.16 +      else (raw_props, raw_inst_morph); (*FIXME proper handling in
    6.17 +        locale.ML / expression.ML would be desirable*)
    6.18  
    6.19      (* witness for canonical interpretation *)
    6.20      val prop = try the_single props;
    6.21 @@ -162,7 +169,7 @@
    6.22        |> Sign.minimize_sort thy;
    6.23      val _ = case filter_out (is_class thy) sups
    6.24       of [] => ()
    6.25 -      | no_classes => error ("No proper classes: " ^ commas (map quote no_classes));
    6.26 +      | no_classes => error ("No (proper) classes: " ^ commas (map quote no_classes));
    6.27            val supparams = (map o apsnd) (snd o snd) (these_params thy sups);
    6.28      val supparam_names = map fst supparams;
    6.29      val _ = if has_duplicates (op =) supparam_names
     7.1 --- a/src/Pure/Isar/expression.ML	Tue Feb 03 19:48:06 2009 +0100
     7.2 +++ b/src/Pure/Isar/expression.ML	Tue Feb 03 21:26:21 2009 +0100
     7.3 @@ -100,7 +100,7 @@
     7.4        (* FIXME: cannot compare bindings for equality. *)
     7.5  
     7.6      fun params_loc loc =
     7.7 -          (Locale.params_of thy loc |> map (fn (p, _, mx) => (p, mx)), loc);
     7.8 +      (Locale.params_of thy loc |> map (fn (p, _, mx) => (p, mx)), loc);
     7.9      fun params_inst (expr as (loc, (prfx, Positional insts))) =
    7.10            let
    7.11              val (ps, loc') = params_loc loc;
    7.12 @@ -150,14 +150,14 @@
    7.13  
    7.14  local
    7.15  
    7.16 -fun prep_inst parse_term ctxt parms (Positional insts) =
    7.17 +fun prep_inst prep_term ctxt parms (Positional insts) =
    7.18        (insts ~~ parms) |> map (fn
    7.19 -        (NONE, p) => Free (p, the (Variable.default_type ctxt p)) |
    7.20 -        (SOME t, _) => parse_term ctxt t)
    7.21 -  | prep_inst parse_term ctxt parms (Named insts) =
    7.22 +        (NONE, p) => Free (p, dummyT) |
    7.23 +        (SOME t, _) => prep_term ctxt t)
    7.24 +  | prep_inst prep_term ctxt parms (Named insts) =
    7.25        parms |> map (fn p => case AList.lookup (op =) insts p of
    7.26 -        SOME t => parse_term ctxt t |
    7.27 -        NONE => Free (p, the (Variable.default_type ctxt p)));
    7.28 +        SOME t => prep_term ctxt t |
    7.29 +        NONE => Free (p, dummyT));
    7.30  
    7.31  in
    7.32  
    7.33 @@ -350,19 +350,19 @@
    7.34  
    7.35  local
    7.36  
    7.37 -fun prep_full_context_statement parse_typ parse_prop prep_vars_elem parse_inst prep_vars_inst prep_expr
    7.38 +fun prep_full_context_statement parse_typ parse_prop prep_vars_elem prep_inst prep_vars_inst prep_expr
    7.39      strict do_close raw_import init_body raw_elems raw_concl ctxt1 =
    7.40    let
    7.41      val thy = ProofContext.theory_of ctxt1;
    7.42  
    7.43      val (raw_insts, fixed) = parameters_of thy strict (apfst (prep_expr thy) raw_import);
    7.44  
    7.45 -    fun prep_inst (loc, (prfx, inst)) (i, insts, ctxt) =
    7.46 +    fun prep_insts (loc, (prfx, inst)) (i, insts, ctxt) =
    7.47        let
    7.48          val (parm_names, parm_types) = Locale.params_of thy loc |>
    7.49            map_split (fn (b, SOME T, _) => (Binding.base_name b, T))
    7.50              (*FIXME return value of Locale.params_of has strange type*)
    7.51 -        val inst' = parse_inst ctxt parm_names inst;
    7.52 +        val inst' = prep_inst ctxt parm_names inst;
    7.53          val parm_types' = map (TypeInfer.paramify_vars o
    7.54            Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT) parm_types;
    7.55          val inst'' = map2 TypeInfer.constrain parm_types' inst';
    7.56 @@ -387,7 +387,7 @@
    7.57  
    7.58      val fors = prep_vars_inst fixed ctxt1 |> fst;
    7.59      val ctxt2 = ctxt1 |> ProofContext.add_fixes_i fors |> snd;
    7.60 -    val (_, insts', ctxt3) = fold prep_inst raw_insts (0, [], ctxt2);
    7.61 +    val (_, insts', ctxt3) = fold prep_insts raw_insts (0, [], ctxt2);
    7.62      val ctxt4 = init_body ctxt3;
    7.63      val (elems, ctxt5) = fold (prep_elem insts') raw_elems ([], ctxt4);
    7.64      val (insts, elems', concl, ctxt6) =