src/HOL/Types_To_Sets/unoverload_type.ML
author immler
Fri Jan 18 18:52:27 2019 -0500 (10 months ago)
changeset 69688 33843320448f
parent 69597 ff784d5a5bfb
child 70279 02920bc314ee
permissions -rw-r--r--
restore type variable names in unoverload_type
     1 (*  Title:      HOL/Types_To_Sets/unoverload_type.ML
     2     Author:     Fabian Immler, TU M√ľnchen
     3 
     4 Internalize sorts and unoverload parameters of a type variable.
     5 *)
     6 
     7 signature UNOVERLOAD_TYPE =
     8 sig
     9   val unoverload_type: Context.generic -> indexname list -> thm -> thm
    10   val unoverload_type_attr: indexname list -> attribute
    11 end;
    12 
    13 structure Unoverload_Type : UNOVERLOAD_TYPE =
    14 struct
    15 
    16 fun params_of_class thy class = try (Axclass.get_info thy #> #params) class |> these
    17 
    18 fun params_of_super_classes thy class =
    19   Sorts.super_classes (Sign.classes_of thy) class |> maps (params_of_class thy)
    20 
    21 fun params_of_sort thy sort = maps (params_of_super_classes thy) sort
    22 
    23 fun subst_TFree n' ty' ty = map_type_tfree (fn x as (n, _) => if n = n' then ty' else TFree x) ty
    24 
    25 fun unoverload_single_type context tvar thm =
    26   let
    27     val tvars = Term.add_tvars (Thm.prop_of thm) []
    28     val thy = Context.theory_of context
    29   in
    30   case find_first (fn (y, _) => tvar = y) tvars of NONE =>
    31     raise TYPE ("unoverload_type: no such type variable in theorem", [TVar (tvar,[])], [])
    32   | SOME (x as (_, sort)) =>
    33     let
    34       val (_, thm') = Internalize_Sort.internalize_sort (Thm.global_ctyp_of thy (TVar x)) thm
    35       val prop' =
    36         fold (fn _ => Term.dest_comb #> #2)
    37           (replicate (Thm.nprems_of thm' - Thm.nprems_of thm) ()) (Thm.prop_of thm')
    38       val (tyenv, _) = Pattern.first_order_match thy ((prop', Thm.prop_of thm))
    39         (Vartab.empty, Vartab.empty)
    40       val tyenv_list = tyenv |> Vartab.dest
    41         |> map (fn (x, (s, TVar (x', _))) =>
    42           ((x, s), Thm.ctyp_of (Context.proof_of context) (TVar(x', s))))
    43       val thm'' = Drule.instantiate_normalize (tyenv_list, []) thm'
    44       val varify_const =
    45         apsnd (subst_TFree "'a" (TVar (tvar, @{sort type}))) #> Const #> Thm.global_cterm_of thy
    46       val consts = params_of_sort thy sort
    47         |> map varify_const
    48     in
    49       fold Unoverloading.unoverload consts thm''
    50       |> Raw_Simplifier.norm_hhf (Context.proof_of context)
    51     end
    52   end
    53 
    54 fun unoverload_type context xs = fold (unoverload_single_type context) xs
    55 
    56 fun unoverload_type_attr xs = Thm.rule_attribute [] (fn context => unoverload_type context xs)
    57 
    58 val _ = Context.>> (Context.map_theory (Attrib.setup \<^binding>\<open>unoverload_type\<close>
    59   (Scan.lift (Scan.repeat Args.var) >> unoverload_type_attr)
    60     "internalize and unoverload type class parameters"))
    61 
    62 end