src/HOL/Library/Types_To_Sets/internalize_sort.ML
changeset 64551 79e9587dbcca
parent 64550 3e20defb1e3c
child 64552 7aa3c52f27aa
     1.1 --- a/src/HOL/Library/Types_To_Sets/internalize_sort.ML	Thu Dec 08 15:11:20 2016 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,68 +0,0 @@
     1.4 -(*  Title:      internalize_sort.ML
     1.5 -    Author:     Ondřej Kunčar, TU München
     1.6 -
     1.7 -    Implements a derived rule (by using Thm.unconstrainT) that internalizes
     1.8 -    type class annotations.
     1.9 -*)
    1.10 -
    1.11 -
    1.12 -(*
    1.13 -                     \<phi>['a::{c_1, ..., c_n} / 'a]
    1.14 ----------------------------------------------------------------------
    1.15 -  class.c_1 ops_1 \<Longrightarrow> ... \<Longrightarrow> class.c_n ops_n \<Longrightarrow> \<phi>['a::type / 'a]
    1.16 -
    1.17 -where class.c is the locale predicate associated with type class c and
    1.18 -ops are operations associated with type class c. For example:
    1.19 -If c = semigroup_add, then ops = op-, op+, 0, uminus.
    1.20 -If c = finite, then ops = TYPE('a::type).
    1.21 -*)
    1.22 -
    1.23 -signature INTERNALIZE_SORT =
    1.24 -sig
    1.25 -  val internalize_sort:  ctyp -> thm -> typ * thm
    1.26 -  val internalize_sort_attr: typ -> attribute
    1.27 -end;
    1.28 -
    1.29 -structure Internalize_Sort : INTERNALIZE_SORT =
    1.30 -struct
    1.31 -
    1.32 -fun internalize_sort ctvar thm =
    1.33 -  let
    1.34 -    val thy = Thm.theory_of_thm thm;
    1.35 -    val tvar = Thm.typ_of ctvar;
    1.36 -    
    1.37 -    val ((_, assms, classes),_) = Logic.unconstrainT [] (Thm.prop_of thm);
    1.38 -
    1.39 -    fun is_proper_class thy = can (Axclass.get_info thy); (* trick by FH *)
    1.40 -    fun reduce_to_non_proper_sort (TVar (name, sort)) = 
    1.41 -        TVar (name, Sign.minimize_sort thy (filter_out (is_proper_class thy) (Sign.complete_sort thy sort)))
    1.42 -      | reduce_to_non_proper_sort _ = error "not supported";
    1.43 -
    1.44 -    val data = (map fst classes) ~~ assms;
    1.45 -    
    1.46 -    val new_tvar = get_first (fn (tvar', ((ren_tvar, _), _)) => if tvar = tvar' 
    1.47 -      then SOME (reduce_to_non_proper_sort ren_tvar) else NONE) data
    1.48 -      |> the_default tvar;
    1.49 -
    1.50 -    fun localify class = Class.rules thy class |> snd |> Thm.transfer thy;
    1.51 -
    1.52 -    fun discharge_of_class tvar class = Thm.of_class (Thm.global_ctyp_of thy tvar, class);
    1.53 -
    1.54 -    val rules = map (fn (tvar', ((ren_tvar, class), _)) => if tvar = tvar' 
    1.55 -      then (if Class.is_class thy class then localify class else discharge_of_class ren_tvar class)
    1.56 -      else discharge_of_class ren_tvar class) data;
    1.57 -  in
    1.58 -    (new_tvar, (Thm.unconstrainT (Thm.strip_shyps thm) OF rules) |> Drule.zero_var_indexes)
    1.59 -  end;
    1.60 -
    1.61 -val tvar = Args.context -- Args.typ >> (fn (_, v as TFree _) => Logic.varifyT_global v 
    1.62 -  | (ctxt, t) => error ("Not a type variable: " ^ Syntax.string_of_typ ctxt t));
    1.63 -
    1.64 -fun internalize_sort_attr tvar = 
    1.65 -  Thm.rule_attribute [] (fn context => fn thm => 
    1.66 -    (snd (internalize_sort (Thm.ctyp_of (Context.proof_of context) tvar) thm)));
    1.67 -
    1.68 -val _ = Context.>> (Context.map_theory (Attrib.setup @{binding internalize_sort} 
    1.69 -  (tvar >> internalize_sort_attr) "internalize a sort"));
    1.70 -
    1.71 -end;
    1.72 \ No newline at end of file