69689
|
1 |
(* Title: HOL/Types_To_Sets/unoverload_def.ML
|
|
2 |
Author: Fabian Immler, CMU
|
|
3 |
|
|
4 |
Define unoverloaded constants from overloaded definitions.
|
|
5 |
*)
|
|
6 |
|
|
7 |
structure Unoverload_Def = struct
|
|
8 |
|
|
9 |
fun 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 |
|
|
64 |
fun 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 |
|
|
69 |
val _ =
|
|
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 |
|
|
76 |
end |