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