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