1(*  Title:      HOL/Types_To_Sets/unoverload_type.ML
2    Author:     Fabian Immler, TU M��nchen
3
4Internalize sorts and unoverload parameters of a type variable.
5*)
6
7signature UNOVERLOAD_TYPE =
8sig
9  val unoverload_type: Context.generic -> indexname list -> thm -> thm
10  val unoverload_type_attr: indexname list -> attribute
11end;
12
13structure Unoverload_Type : UNOVERLOAD_TYPE =
14struct
15
16fun params_of_class thy class = try (Axclass.get_info thy #> #params) class |> these
17
18fun params_of_super_classes thy class =
19  class::Sorts.super_classes (Sign.classes_of thy) class |> maps (params_of_class thy)
20
21fun params_of_sort thy sort = maps (params_of_super_classes thy) sort
22
23fun subst_TFree n' ty' ty = map_type_tfree (fn x as (n, _) => if n = n' then ty' else TFree x) ty
24
25fun unoverload_single_type context tvar thm =
26  let
27    val tvars = Term.add_tvars (Thm.prop_of thm) []
28    val thy = Context.theory_of context
29  in
30  case find_first (fn (y, _) => tvar = y) tvars of NONE =>
31    raise TYPE ("unoverload_type: no such type variable in theorem", [TVar (tvar,[])], [])
32  | SOME (x as (_, sort)) =>
33    let
34      val (_, thm') = Internalize_Sort.internalize_sort (Thm.global_ctyp_of thy (TVar x)) thm
35      val prop' =
36        fold (fn _ => Term.dest_comb #> #2)
37          (replicate (Thm.nprems_of thm' - Thm.nprems_of thm) ()) (Thm.prop_of thm')
38      val (tyenv, _) = Pattern.first_order_match thy ((prop', Thm.prop_of thm))
39        (Vartab.empty, Vartab.empty)
40      val tyenv_list = tyenv |> Vartab.dest
41        |> map (fn (x, (s, TVar (x', _))) =>
42          ((x, s), Thm.ctyp_of (Context.proof_of context) (TVar(x', s))))
43      val thm'' = Drule.instantiate_normalize (tyenv_list, []) thm'
44      val varify_const =
45        apsnd (subst_TFree "'a" (TVar (tvar, @{sort type}))) #> Const #> Thm.global_cterm_of thy
46      val consts = params_of_sort thy sort
47        |> map varify_const
48    in
49      fold Unoverloading.unoverload consts thm''
50      |> Raw_Simplifier.norm_hhf (Context.proof_of context)
51    end
52  end
53
54fun unoverload_type context xs = fold (unoverload_single_type context) xs
55
56fun unoverload_type_attr xs = Thm.rule_attribute [] (fn context => unoverload_type context xs)
57
58val _ = Context.>> (Context.map_theory (Attrib.setup \<^binding>\<open>unoverload_type\<close>
59  (Scan.lift (Scan.repeat Args.var) >> unoverload_type_attr)
60    "internalize and unoverload type class parameters"))
61
62end