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