src/HOL/Types_To_Sets/internalize_sort.ML
author wenzelm
Mon Dec 12 11:33:14 2016 +0100 (17 months ago)
changeset 64551 79e9587dbcca
permissions -rw-r--r--
proper session HOL-Types_To_Sets;
NEWS;
CONTRIBUTORS;
tuned whitespace;
     1 (*  Title:      HOL/Types_To_Sets/internalize_sort.ML
     2     Author:     Ondřej Kunčar, TU München
     3 
     4 A derived rule (by using Thm.unconstrainT) that internalizes
     5 type 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 
    14 where class.c is the locale predicate associated with type class c and
    15 ops are operations associated with type class c. For example:
    16 If c = semigroup_add, then ops = op-, op+, 0, uminus.
    17 If c = finite, then ops = TYPE('a::type).
    18 *)
    19 
    20 signature INTERNALIZE_SORT =
    21 sig
    22   val internalize_sort:  ctyp -> thm -> typ * thm
    23   val internalize_sort_attr: typ -> attribute
    24 end;
    25 
    26 structure Internalize_Sort : INTERNALIZE_SORT =
    27 struct
    28 
    29 fun internalize_sort ctvar thm =
    30   let
    31     val thy = Thm.theory_of_thm thm;
    32     val tvar = Thm.typ_of ctvar;
    33 
    34     val ((_, assms, classes),_) = 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 fst classes) ~~ assms;
    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 
    58 val 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 
    61 fun 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 
    65 val _ = Context.>> (Context.map_theory (Attrib.setup @{binding internalize_sort}
    66   (tvar >> internalize_sort_attr) "internalize a sort"));
    67 
    68 end;