-
Notifications
You must be signed in to change notification settings - Fork 1
/
Def_Const.thy
30 lines (22 loc) · 1.06 KB
/
Def_Const.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
section \<open> Defining Declared Constants \<close>
theory Def_Const
imports Main
keywords "def_consts" :: "thy_defn"
begin
text \<open> Add a simple command to define previously declared polymorphic constants. This is
particularly useful for handling given sets in Z. \<close>
ML \<open>
structure Def_Const =
struct
fun def_const (n, v) thy =
let val Const (pn, typ) = Proof_Context.read_const {proper = false, strict = false} (Named_Target.theory_init thy) n
val ctx = Overloading.overloading [(n, (pn, dummyT), false)] thy
val pt = Syntax.check_term ctx (Type.constraint typ (Syntax.parse_term ctx v))
in (Local_Theory.exit_global o snd o Local_Theory.define (((Binding.name n), NoSyn), ((Binding.name (n ^ "_def"), [Attrib.check_src @{context} (Token.make_src ("code", Position.none) [])]), pt))) ctx
end
val def_consts = fold def_const
end;
Outer_Syntax.command @{command_keyword def_consts} "define a declared constant"
(Scan.repeat1 ((Parse.name --| @{keyword "="}) -- Parse.term) >> (Toplevel.theory o Def_Const.def_consts));
\<close>
end