1(*  Title:      HOL/Types_To_Sets/internalize_sort.ML
2    Author:     Ond��ej Kun��ar, TU M��nchen
3
4A derived rule (by using Thm.unconstrainT) that internalizes
5type class annotations.
6*)
7
8
9(*
10                     \<phi>['a::{c_1, ..., c_n} / 'a]
11---------------------------------------------------------------------
12  class.c_1 ops_1 \<Longrightarrow> ... \<Longrightarrow> class.c_n ops_n \<Longrightarrow> \<phi>['a::type / 'a]
13
14where class.c is the locale predicate associated with type class c and
15ops are operations associated with type class c. For example:
16If c = semigroup_add, then ops = op-, op+, 0, uminus.
17If c = finite, then ops = TYPE('a::type).
18*)
19
20signature INTERNALIZE_SORT =
21sig
22  val internalize_sort:  ctyp -> thm -> typ * thm
23  val internalize_sort_attr: typ -> attribute
24end;
25
26structure Internalize_Sort : INTERNALIZE_SORT =
27struct
28
29fun internalize_sort ctvar thm =
30  let
31    val thy = Thm.theory_of_thm thm;
32    val tvar = Thm.typ_of ctvar;
33
34    val (ucontext, _) = Logic.unconstrainT [] (Thm.prop_of thm);
35
36    fun is_proper_class thy = can (Axclass.get_info thy); (* trick by FH *)
37    fun reduce_to_non_proper_sort (TVar (name, sort)) =
38        TVar (name, Sign.minimize_sort thy (filter_out (is_proper_class thy) (Sign.complete_sort thy sort)))
39      | reduce_to_non_proper_sort _ = error "not supported";
40
41    val data = map #1 (#outer_constraints ucontext) ~~ #constraints ucontext;
42
43    val new_tvar = get_first (fn (tvar', ((ren_tvar, _), _)) => if tvar = tvar'
44      then SOME (reduce_to_non_proper_sort ren_tvar) else NONE) data
45      |> the_default tvar;
46
47    fun localify class = Class.rules thy class |> snd |> Thm.transfer thy;
48
49    fun discharge_of_class tvar class = Thm.of_class (Thm.global_ctyp_of thy tvar, class);
50
51    val rules = map (fn (tvar', ((ren_tvar, class), _)) => if tvar = tvar'
52      then (if Class.is_class thy class then localify class else discharge_of_class ren_tvar class)
53      else discharge_of_class ren_tvar class) data;
54  in
55    (new_tvar, (Thm.unconstrainT (Thm.strip_shyps thm) OF rules) |> Drule.zero_var_indexes)
56  end;
57
58val tvar = Args.context -- Args.typ >> (fn (_, v as TFree _) => Logic.varifyT_global v
59  | (ctxt, t) => error ("Not a type variable: " ^ Syntax.string_of_typ ctxt t));
60
61fun internalize_sort_attr tvar =
62  Thm.rule_attribute [] (fn context => fn thm =>
63    (snd (internalize_sort (Thm.ctyp_of (Context.proof_of context) tvar) thm)));
64
65val _ = Context.>> (Context.map_theory (Attrib.setup \<^binding>\<open>internalize_sort\<close>
66  (tvar >> internalize_sort_attr) "internalize a sort"));
67
68end;
69