# HG changeset patch
# User immler
# Date 1547858884 18000
# Node ID ab5a8a2519b0f4b9acd78709f0110b18c9425b10
# Parent  33843320448f243712faeeb13cc4f4de6e4233cd
automation for unverloading definitions

diff -r 33843320448f -r ab5a8a2519b0 src/HOL/ROOT
--- a/src/HOL/ROOT	Fri Jan 18 18:52:27 2019 -0500
+++ b/src/HOL/ROOT	Fri Jan 18 19:48:04 2019 -0500
@@ -957,6 +957,7 @@
     "Examples/Prerequisites"
     "Examples/Finite"
     "Examples/T2_Spaces"
+    "Examples/Unoverload_Def"
     "Examples/Linear_Algebra_On"
 
 session HOLCF (main timing) in HOLCF = HOL +
diff -r 33843320448f -r ab5a8a2519b0 src/HOL/Types_To_Sets/Examples/Unoverload_Def.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Types_To_Sets/Examples/Unoverload_Def.thy	Fri Jan 18 19:48:04 2019 -0500
@@ -0,0 +1,23 @@
+(*  Title:      HOL/Types_To_Sets/Examples/Unoverload_Def.thy
+    Author:     Fabian Immler, CMU
+*)
+theory Unoverload_Def
+  imports
+    "../Types_To_Sets"
+    Complex_Main
+begin
+
+unoverload_definition closed_def
+  and compact_eq_Heine_Borel
+  and cauchy_filter_def
+  and Cauchy_uniform
+  and nhds_def
+  and complete_uniform
+  and module_def
+  and vector_space_def
+  and module_hom_axioms_def
+  and module_hom_def
+  and VS_linear: Vector_Spaces.linear_def
+  and linear_def
+
+end
\ No newline at end of file
diff -r 33843320448f -r ab5a8a2519b0 src/HOL/Types_To_Sets/Types_To_Sets.thy
--- a/src/HOL/Types_To_Sets/Types_To_Sets.thy	Fri Jan 18 18:52:27 2019 -0500
+++ b/src/HOL/Types_To_Sets/Types_To_Sets.thy	Fri Jan 18 19:48:04 2019 -0500
@@ -11,6 +11,7 @@
 
 theory Types_To_Sets
   imports Main
+  keywords "unoverload_definition" :: thy_decl
 begin
 
 subsection \<open>Rules\<close>
@@ -24,8 +25,13 @@
 text\<open>The following file implements a derived rule that internalizes type class annotations.\<close>
 ML_file \<open>internalize_sort.ML\<close>
 
-text\<open>The following file provides some automation to unoverload and internalize the parameters o
+text\<open>The following file provides some automation to unoverload and internalize the parameters of
   the sort constraints of a type variable.\<close>
 ML_file \<open>unoverload_type.ML\<close>
 
+text \<open>The following file provides automation to define unoverloaded constants from overloaded
+  definitions.\<close>
+named_theorems unoverload_def
+ML_file \<open>unoverload_def.ML\<close>
+
 end
diff -r 33843320448f -r ab5a8a2519b0 src/HOL/Types_To_Sets/unoverload_def.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Types_To_Sets/unoverload_def.ML	Fri Jan 18 19:48:04 2019 -0500
@@ -0,0 +1,76 @@
+(*  Title:      HOL/Types_To_Sets/unoverload_def.ML
+    Author:     Fabian Immler, CMU
+
+Define unoverloaded constants from overloaded definitions.
+*)
+
+structure Unoverload_Def = struct
+
+fun unoverload_def name_opt thm thy =
+  let
+    val ctxt = Proof_Context.init_global thy
+    val thm_abs = Local_Defs.abs_def_rule ctxt thm
+      |> Conv.fconv_rule (Conv.top_conv
+        (K (Conv.try_conv (Conv.rewrs_conv
+              (Named_Theorems.get ctxt @{named_theorems unoverload_def})))) ctxt)
+    val (lhs, rhs) = thm_abs
+      |> Thm.cprop_of
+      |> Thm.dest_equals
+    val c = lhs |> Thm.term_of |> Term.dest_Const
+    val binding_with =
+      case name_opt of NONE =>
+        Binding.qualify_name true
+          (Binding.name (Binding.name_of (Binding.qualified_name (#1 c))))
+          "with"
+      | SOME name => name
+
+    val tvars = Term.add_tvars (Thm.term_of rhs) [] |> map fst
+
+    val thm_with = Thm.reflexive rhs
+      |> Unoverload_Type.unoverload_type (Context.Proof ctxt) (tvars)
+
+    val rhs_with' = thm_with |> Thm.cconcl_of |> Thm.dest_equals |> #2 |> Thm.term_of
+    val vars = Term.add_vars rhs_with' []
+    val rhs_abs = fold (Var #> Term.lambda) vars rhs_with'
+
+    val ([rhs_abs'], ctxt') = Variable.importT_terms [rhs_abs] ctxt
+    val (with_const, thy') = Sign.declare_const_global
+      ((binding_with, Term.fastype_of rhs_abs'), NoSyn)
+      thy
+    val ([with_def], thy'') = Global_Theory.add_defs false
+      [((Binding.suffix_name "_def" binding_with,
+      Logic.mk_equals (with_const, rhs_abs')), [])] thy'
+
+    val with_var_def =
+      fold_rev
+        (fn (x, _) => fn thm =>
+          let
+            val ty = Thm.concl_of thm |> Logic.dest_equals |> #2 |>
+              fastype_of |> dest_funT |> #1
+          in
+            Thm.combination thm
+              (Thm.reflexive (Thm.var (x, Thm.ctyp_of (Proof_Context.init_global thy'') ty)))
+          end)
+        (vars)
+        (with_def)
+
+    val thm_with = ([thm_abs, Thm.symmetric with_var_def] MRS @{thm Pure.transitive})
+    val thy''' =
+      Global_Theory.add_thm
+        ((binding_with, thm_with), [Named_Theorems.add @{named_theorems "unoverload_def"}]) thy''
+      |> #2
+  in thy''' end
+
+fun unoverload_def1_cmd (name_opt, facts) thy =
+  let
+    val [thm] = Attrib.eval_thms (Proof_Context.init_global thy) [facts]
+  in unoverload_def name_opt thm thy end
+
+val _ =
+  Outer_Syntax.local_theory \<^command_keyword>\<open>unoverload_definition\<close>
+    "definition of unoverloaded constants"
+    (Parse.and_list (Scan.option (Parse.binding --| \<^keyword>\<open>:\<close>) -- Parse.thm) >>
+      (fn things => Local_Theory.raw_theory (fold unoverload_def1_cmd things))
+    )
+
+end
\ No newline at end of file