src/HOL/Types_To_Sets/unoverload_type.ML
changeset 68428 46beee72fb66
child 68429 38961724a017
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Types_To_Sets/unoverload_type.ML	Tue Jun 12 16:21:52 2018 +0200
     1.3 @@ -0,0 +1,56 @@
     1.4 +(*  Title:      HOL/Types_To_Sets/unoverload_type.ML
     1.5 +    Author:     Fabian Immler, TU M√ľnchen
     1.6 +
     1.7 +Internalize sorts and unoverload parameters of a type variable.
     1.8 +*)
     1.9 +
    1.10 +signature UNOVERLOAD_TYPE =
    1.11 +sig
    1.12 +  val unoverload_type: Context.generic -> string -> thm -> thm
    1.13 +  val unoverload_type_attr: string -> attribute
    1.14 +end;
    1.15 +
    1.16 +structure Unoverload_Type : UNOVERLOAD_TYPE =
    1.17 +struct
    1.18 +
    1.19 +fun those [] = []
    1.20 +  | those (NONE::xs) = those xs
    1.21 +  | those (SOME x::xs) = x::those xs
    1.22 +
    1.23 +fun params_of_sort context sort =
    1.24 +  let
    1.25 +    val algebra = Sign.classes_of (Context.theory_of context)
    1.26 +    val params = List.concat (map (Sorts.super_classes algebra) sort) |>
    1.27 +      map (try (Axclass.get_info (Context.theory_of context))) |>
    1.28 +      those |>
    1.29 +      map #params |>
    1.30 +      List.concat
    1.31 +  in params end
    1.32 +
    1.33 +fun unoverload_type context s thm =
    1.34 +  let
    1.35 +    val tvars = Term.add_tvars (Thm.prop_of thm) []
    1.36 +    val thy = Context.theory_of context
    1.37 +  in
    1.38 +  case find_first (fn ((n,_), _) => n = s) tvars of NONE =>
    1.39 +    raise THM ("unoverload_internalize_deps: type variable ("^s^") not in theorem", 0, [thm])
    1.40 +  | SOME (x as (_, sort)) =>
    1.41 +    let
    1.42 +      val (tvar, thm') = Internalize_Sort.internalize_sort (Thm.global_ctyp_of thy (TVar x)) thm
    1.43 +      val consts = params_of_sort context sort |>
    1.44 +        map (apsnd (map_type_tfree (fn ("'a", _) =>  tvar | x => TFree x)))
    1.45 +    in
    1.46 +      fold (fn c => Unoverloading.unoverload (Thm.global_cterm_of thy (Const c))) consts thm'
    1.47 +    end
    1.48 +  end
    1.49 +
    1.50 +val tyN = (Args.context -- Args.typ) >>
    1.51 +  (fn (_, TFree (n, _)) => n
    1.52 +  | (ctxt, t) => error ("Not a type variable: " ^ Syntax.string_of_typ ctxt t))
    1.53 +
    1.54 +fun unoverload_type_attr n = Thm.rule_attribute [] (fn context => unoverload_type context n)
    1.55 +
    1.56 +val _ = Context.>> (Context.map_theory (Attrib.setup @{binding unoverload_type}
    1.57 +  (tyN >> unoverload_type_attr) "internalize a sort"))
    1.58 +
    1.59 +end
    1.60 \ No newline at end of file