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