1(*  Title:      HOL/Types_To_Sets/unoverload_def.ML
2    Author:     Fabian Immler, CMU
3
4Define unoverloaded constants from overloaded definitions.
5*)
6
7structure Unoverload_Def = struct
8
9fun unoverload_def name_opt thm thy =
10  let
11    val ctxt = Proof_Context.init_global thy
12    val thm_abs = Local_Defs.abs_def_rule ctxt thm
13      |> Conv.fconv_rule (Conv.top_conv
14        (K (Conv.try_conv (Conv.rewrs_conv
15              (Named_Theorems.get ctxt @{named_theorems unoverload_def})))) ctxt)
16    val (lhs, rhs) = thm_abs
17      |> Thm.cprop_of
18      |> Thm.dest_equals
19    val c = lhs |> Thm.term_of |> Term.dest_Const
20    val binding_with =
21      case name_opt of NONE =>
22        Binding.qualify_name true
23          (Binding.name (Binding.name_of (Binding.qualified_name (#1 c))))
24          "with"
25      | SOME name => name
26
27    val tvars = Term.add_tvars (Thm.term_of rhs) [] |> map fst
28
29    val thm_with = Thm.reflexive rhs
30      |> Unoverload_Type.unoverload_type (Context.Proof ctxt) (tvars)
31
32    val rhs_with' = thm_with |> Thm.cconcl_of |> Thm.dest_equals |> #2 |> Thm.term_of
33    val vars = Term.add_vars rhs_with' []
34    val rhs_abs = fold (Var #> Term.lambda) vars rhs_with'
35
36    val ([rhs_abs'], ctxt') = Variable.importT_terms [rhs_abs] ctxt
37    val (with_const, thy') = Sign.declare_const_global
38      ((binding_with, Term.fastype_of rhs_abs'), NoSyn)
39      thy
40    val ([with_def], thy'') = Global_Theory.add_defs false
41      [((Binding.suffix_name "_def" binding_with,
42      Logic.mk_equals (with_const, rhs_abs')), [])] thy'
43
44    val with_var_def =
45      fold_rev
46        (fn (x, _) => fn thm =>
47          let
48            val ty = Thm.concl_of thm |> Logic.dest_equals |> #2 |>
49              fastype_of |> dest_funT |> #1
50          in
51            Thm.combination thm
52              (Thm.reflexive (Thm.var (x, Thm.ctyp_of (Proof_Context.init_global thy'') ty)))
53          end)
54        (vars)
55        (with_def)
56
57    val thm_with = ([thm_abs, Thm.symmetric with_var_def] MRS @{thm Pure.transitive})
58    val thy''' =
59      Global_Theory.add_thm
60        ((binding_with, thm_with), [Named_Theorems.add @{named_theorems "unoverload_def"}]) thy''
61      |> #2
62  in thy''' end
63
64fun unoverload_def1_cmd (name_opt, facts) thy =
65  let
66    val [thm] = Attrib.eval_thms (Proof_Context.init_global thy) [facts]
67  in unoverload_def name_opt thm thy end
68
69val _ =
70  Outer_Syntax.local_theory \<^command_keyword>\<open>unoverload_definition\<close>
71    "definition of unoverloaded constants"
72    (Parse.and_list (Scan.option (Parse.binding --| \<^keyword>\<open>:\<close>) -- Parse.thm) >>
73      (fn things => Local_Theory.raw_theory (fold unoverload_def1_cmd things))
74    )
75
76end