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