src/HOL/Types_To_Sets/unoverload_type.ML
author immler
Wed Jun 13 10:52:47 2018 +0200 (17 months ago)
changeset 68438 f04d0e75e439
parent 68437 f9b15e7c12bd
child 69597 ff784d5a5bfb
permissions -rw-r--r--
tuned exception
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@68429
    16
fun internalize_sort' ctvar thm =
immler@68429
    17
  let
immler@68429
    18
    val (_, thm') = Internalize_Sort.internalize_sort ctvar thm
immler@68429
    19
    val class_premise = case Thm.prems_of thm' of t::_=> t | [] =>
immler@68430
    20
      raise THM ("internalize_sort': no premise?", 0, [thm'])
immler@68429
    21
    val class_vars = Term.add_tvars class_premise []
immler@68429
    22
    val tvar = case class_vars of [x] => TVar x | _ =>
immler@68430
    23
      raise TERM ("internalize_sort': not one type class variable.", [class_premise])
immler@68429
    24
  in
immler@68429
    25
    (tvar, thm')
immler@68429
    26
  end
immler@68429
    27
immler@68437
    28
fun params_of_class thy class = try (Axclass.get_info thy #> #params) class |> these
immler@68437
    29
immler@68437
    30
fun params_of_super_classes thy class =
immler@68437
    31
  Sorts.super_classes (Sign.classes_of thy) class |> maps (params_of_class thy)
immler@68437
    32
immler@68437
    33
fun params_of_sort thy sort = maps (params_of_super_classes thy) sort
immler@68437
    34
immler@68437
    35
fun subst_TFree n' ty' ty = map_type_tfree (fn x as (n, _) => if n = n' then ty' else TFree x) ty
immler@68437
    36
immler@68434
    37
fun unoverload_single_type context x thm =
immler@68428
    38
  let
immler@68428
    39
    val tvars = Term.add_tvars (Thm.prop_of thm) []
immler@68428
    40
    val thy = Context.theory_of context
immler@68428
    41
  in
immler@68433
    42
  case find_first (fn (y, _) => x = y) tvars of NONE =>
immler@68438
    43
    raise TYPE ("unoverload_type: no such type variable in theorem", [TVar (x,[])], [])
immler@68428
    44
  | SOME (x as (_, sort)) =>
immler@68428
    45
    let
immler@68429
    46
      val (tvar, thm') = internalize_sort' (Thm.global_ctyp_of thy (TVar x)) thm
immler@68437
    47
      val consts = params_of_sort thy sort
immler@68437
    48
        |> map (apsnd (subst_TFree "'a" tvar) #> Const #> Thm.global_cterm_of thy)
immler@68428
    49
    in
immler@68437
    50
      fold Unoverloading.unoverload consts thm'
immler@68436
    51
      |> Raw_Simplifier.norm_hhf (Context.proof_of context)
immler@68428
    52
    end
immler@68428
    53
  end
immler@68428
    54
immler@68434
    55
fun unoverload_type context xs = fold (unoverload_single_type context) xs
immler@68434
    56
immler@68434
    57
fun unoverload_type_attr xs = Thm.rule_attribute [] (fn context => unoverload_type context xs)
immler@68428
    58
immler@68428
    59
val _ = Context.>> (Context.map_theory (Attrib.setup @{binding unoverload_type}
immler@68435
    60
  (Scan.lift (Scan.repeat Args.var) >> unoverload_type_attr)
immler@68435
    61
    "internalize and unoverload type class parameters"))
immler@68428
    62
immler@68428
    63
end