# HG changeset patch
# User immler
# Date 1528813312 -7200
# Node ID 46beee72fb66065283acc9efcf06c4ecffd59a30
# Parent  f75d765a281f0f949d6ff16c3b7a91c1760a137f
a derived rule combining unoverload and internalize_sort

diff -r f75d765a281f -r 46beee72fb66 src/HOL/Types_To_Sets/Examples/T2_Spaces.thy
--- a/src/HOL/Types_To_Sets/Examples/T2_Spaces.thy	Tue Jun 12 11:18:35 2018 +0100
+++ b/src/HOL/Types_To_Sets/Examples/T2_Spaces.thy	Tue Jun 12 16:21:52 2018 +0200
@@ -120,6 +120,9 @@
      for the original relativization algorithm.\<close>
 thm dictionary_second_step
 
+text \<open>Alternative construction using \<open>unoverload_type\<close>
+  (This does not require fiddling with \<open>Sign.add_const_constraint\<close>).\<close>
+lemmas dictionary_second_step' = dictionary_first_step[unoverload_type 'a]
 
 text\<open>This is the set-based variant of the theorem compact_imp_closed.\<close>
 lemma compact_imp_closed_set_based:
diff -r f75d765a281f -r 46beee72fb66 src/HOL/Types_To_Sets/Types_To_Sets.thy
--- a/src/HOL/Types_To_Sets/Types_To_Sets.thy	Tue Jun 12 11:18:35 2018 +0100
+++ b/src/HOL/Types_To_Sets/Types_To_Sets.thy	Tue Jun 12 16:21:52 2018 +0200
@@ -24,4 +24,8 @@
 text\<open>The following file implements a derived rule that internalizes type class annotations.\<close>
 ML_file "internalize_sort.ML"
 
+text\<open>The following file provides some automation to unoverload and internalize the parameters o
+  the sort constraints of a type variable.\<close>
+ML_file \<open>unoverload_type.ML\<close>
+
 end
diff -r f75d765a281f -r 46beee72fb66 src/HOL/Types_To_Sets/unoverload_type.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Types_To_Sets/unoverload_type.ML	Tue Jun 12 16:21:52 2018 +0200
@@ -0,0 +1,56 @@
+(*  Title:      HOL/Types_To_Sets/unoverload_type.ML
+    Author:     Fabian Immler, TU München
+
+Internalize sorts and unoverload parameters of a type variable.
+*)
+
+signature UNOVERLOAD_TYPE =
+sig
+  val unoverload_type: Context.generic -> string -> thm -> thm
+  val unoverload_type_attr: string -> attribute
+end;
+
+structure Unoverload_Type : UNOVERLOAD_TYPE =
+struct
+
+fun those [] = []
+  | those (NONE::xs) = those xs
+  | those (SOME x::xs) = x::those xs
+
+fun params_of_sort context sort =
+  let
+    val algebra = Sign.classes_of (Context.theory_of context)
+    val params = List.concat (map (Sorts.super_classes algebra) sort) |>
+      map (try (Axclass.get_info (Context.theory_of context))) |>
+      those |>
+      map #params |>
+      List.concat
+  in params end
+
+fun unoverload_type context s thm =
+  let
+    val tvars = Term.add_tvars (Thm.prop_of thm) []
+    val thy = Context.theory_of context
+  in
+  case find_first (fn ((n,_), _) => n = s) tvars of NONE =>
+    raise THM ("unoverload_internalize_deps: type variable ("^s^") not in theorem", 0, [thm])
+  | SOME (x as (_, sort)) =>
+    let
+      val (tvar, thm') = Internalize_Sort.internalize_sort (Thm.global_ctyp_of thy (TVar x)) thm
+      val consts = params_of_sort context sort |>
+        map (apsnd (map_type_tfree (fn ("'a", _) =>  tvar | x => TFree x)))
+    in
+      fold (fn c => Unoverloading.unoverload (Thm.global_cterm_of thy (Const c))) consts thm'
+    end
+  end
+
+val tyN = (Args.context -- Args.typ) >>
+  (fn (_, TFree (n, _)) => n
+  | (ctxt, t) => error ("Not a type variable: " ^ Syntax.string_of_typ ctxt t))
+
+fun unoverload_type_attr n = Thm.rule_attribute [] (fn context => unoverload_type context n)
+
+val _ = Context.>> (Context.map_theory (Attrib.setup @{binding unoverload_type}
+  (tyN >> unoverload_type_attr) "internalize a sort"))
+
+end
\ No newline at end of file