--- 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 +
--- /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
--- 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
--- /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