author  wenzelm 
Sun, 25 Oct 2009 19:19:29 +0100  
changeset 33168  853493e5d5d4 
parent 33159  369da293bbd4 
child 33173  b8ca12f6681a 
permissions  rwrr 
1526  1 
(* Title: Pure/theory.ML 
2 
Author: Lawrence C Paulson and Markus Wenzel 

3 

28290  4 
Logical theory content: axioms, definitions, and begin/end wrappers. 
1526  5 
*) 
16291  6 

26668
65023d4fd226
removed obsolete SIGN_THEORY  no name aliases in structure Theory;
wenzelm
parents:
26631
diff
changeset

7 
signature THEORY = 
3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

8 
sig 
16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

9 
val eq_thy: theory * theory > bool 
3996  10 
val subthy: theory * theory > bool 
24666  11 
val assert_super: theory > theory > theory 
22684  12 
val parents_of: theory > theory list 
13 
val ancestors_of: theory > theory list 

24666  14 
val check_thy: theory > theory_ref 
15 
val deref: theory_ref > theory 

16 
val merge: theory * theory > theory 

17 
val merge_refs: theory_ref * theory_ref > theory_ref 

18 
val merge_list: theory list > theory 

16495  19 
val checkpoint: theory > theory 
20 
val copy: theory > theory 

24666  21 
val requires: theory > string > string > unit 
33095
bbd52d2f8696
renamed NameSpace to Name_Space  also to emphasize its subtle change in semantics;
wenzelm
parents:
33092
diff
changeset

22 
val axiom_space: theory > Name_Space.T 
22684  23 
val axiom_table: theory > term Symtab.table 
16339  24 
val axioms_of: theory > (string * term) list 
25 
val all_axioms_of: theory > (string * term) list 

24666  26 
val defs_of: theory > Defs.T 
27 
val at_begin: (theory > theory option) > theory > theory 

28 
val at_end: (theory > theory option) > theory > theory 

29 
val begin_theory: string > theory list > theory 

30 
val end_theory: theory > theory 

29581  31 
val add_axioms_i: (binding * term) list > theory > theory 
30337
eb189f7e43a1
Theory.add_axioms/add_defs: replaced old bstring by binding;
wenzelm
parents:
30218
diff
changeset

32 
val add_axioms: (binding * string) list > theory > theory 
19708
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

33 
val add_deps: string > string * typ > (string * typ) list > theory > theory 
29581  34 
val add_defs_i: bool > bool > (binding * term) list > theory > theory 
30337
eb189f7e43a1
Theory.add_axioms/add_defs: replaced old bstring by binding;
wenzelm
parents:
30218
diff
changeset

35 
val add_defs: bool > bool > (binding * string) list > theory > theory 
29581  36 
val add_finals_i: bool > term list > theory > theory 
16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

37 
val add_finals: bool > string list > theory > theory 
29581  38 
val specify_const: Properties.T > (binding * typ) * mixfix > theory > term * theory 
16495  39 
end 
1526  40 

24666  41 
structure Theory: THEORY = 
16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

42 
struct 
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

43 

19708
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

44 

24666  45 
(** theory context operations **) 
16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

46 

82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

47 
val eq_thy = Context.eq_thy; 
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

48 
val subthy = Context.subthy; 
1526  49 

24626
85eceef2edc7
introduced generic concepts for theory interpretators
haftmann
parents:
24199
diff
changeset

50 
fun assert_super thy1 thy2 = 
85eceef2edc7
introduced generic concepts for theory interpretators
haftmann
parents:
24199
diff
changeset

51 
if subthy (thy1, thy2) then thy2 
85eceef2edc7
introduced generic concepts for theory interpretators
haftmann
parents:
24199
diff
changeset

52 
else raise THEORY ("Not a super theory", [thy1, thy2]); 
85eceef2edc7
introduced generic concepts for theory interpretators
haftmann
parents:
24199
diff
changeset

53 

16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

54 
val parents_of = Context.parents_of; 
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

55 
val ancestors_of = Context.ancestors_of; 
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

56 

24137
8d7896398147
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23655
diff
changeset

57 
val check_thy = Context.check_thy; 
16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

58 
val deref = Context.deref; 
24666  59 

16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

60 
val merge = Context.merge; 
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

61 
val merge_refs = Context.merge_refs; 
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

62 

23600  63 
fun merge_list [] = raise THEORY ("Empty merge of theories", []) 
21608  64 
 merge_list (thy :: thys) = Library.foldl merge (thy, thys); 
65 

16495  66 
val checkpoint = Context.checkpoint_thy; 
67 
val copy = Context.copy_thy; 

68 

24666  69 
fun requires thy name what = 
29092  70 
if exists (fn thy' => Context.theory_name thy' = name) (thy :: ancestors_of thy) then () 
24666  71 
else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what); 
72 

73 

74 

25059  75 
(** datatype thy **) 
24666  76 

77 
type wrapper = (theory > theory option) * stamp; 

78 

79 
fun apply_wrappers (wrappers: wrapper list) = 

25059  80 
perhaps (perhaps_loop (perhaps_apply (map fst wrappers))); 
24666  81 

82 
datatype thy = Thy of 

33095
bbd52d2f8696
renamed NameSpace to Name_Space  also to emphasize its subtle change in semantics;
wenzelm
parents:
33092
diff
changeset

83 
{axioms: term Name_Space.table, 
24666  84 
defs: Defs.T, 
85 
wrappers: wrapper list * wrapper list}; 

86 

28290  87 
fun make_thy (axioms, defs, wrappers) = Thy {axioms = axioms, defs = defs, wrappers = wrappers}; 
24666  88 

89 
structure ThyData = TheoryDataFun 

90 
( 

91 
type T = thy; 

33159  92 
val empty_axioms = Name_Space.empty_table "axiom" : term Name_Space.table; 
33096  93 
val empty = make_thy (empty_axioms, Defs.empty, ([], [])); 
24666  94 
val copy = I; 
95 

33096  96 
fun extend (Thy {axioms = _, defs, wrappers}) = make_thy (empty_axioms, defs, wrappers); 
24666  97 

98 
fun merge pp (thy1, thy2) = 

99 
let 

28290  100 
val Thy {axioms = _, defs = defs1, wrappers = (bgs1, ens1)} = thy1; 
101 
val Thy {axioms = _, defs = defs2, wrappers = (bgs2, ens2)} = thy2; 

24666  102 

33096  103 
val axioms' = empty_axioms; 
24666  104 
val defs' = Defs.merge pp (defs1, defs2); 
105 
val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2); 

106 
val ens' = Library.merge (eq_snd op =) (ens1, ens2); 

28290  107 
in make_thy (axioms', defs', (bgs', ens')) end; 
24666  108 
); 
109 

110 
fun rep_theory thy = ThyData.get thy > (fn Thy args => args); 

111 

28290  112 
fun map_thy f = ThyData.map (fn (Thy {axioms, defs, wrappers}) => 
113 
make_thy (f (axioms, defs, wrappers))); 

24666  114 

115 

28290  116 
fun map_axioms f = map_thy (fn (axioms, defs, wrappers) => (f axioms, defs, wrappers)); 
117 
fun map_defs f = map_thy (fn (axioms, defs, wrappers) => (axioms, f defs, wrappers)); 

118 
fun map_wrappers f = map_thy (fn (axioms, defs, wrappers) => (axioms, defs, f wrappers)); 

24666  119 

120 

121 
(* basic operations *) 

122 

123 
val axiom_space = #1 o #axioms o rep_theory; 

124 
val axiom_table = #2 o #axioms o rep_theory; 

125 

126 
val axioms_of = Symtab.dest o #2 o #axioms o rep_theory; 

127 
fun all_axioms_of thy = maps axioms_of (thy :: ancestors_of thy); 

128 

129 
val defs_of = #defs o rep_theory; 

130 

131 

132 
(* begin/end theory *) 

133 

134 
val begin_wrappers = rev o #1 o #wrappers o rep_theory; 

135 
val end_wrappers = rev o #2 o #wrappers o rep_theory; 

136 

137 
fun at_begin f = map_wrappers (apfst (cons (f, stamp ()))); 

138 
fun at_end f = map_wrappers (apsnd (cons (f, stamp ()))); 

139 

140 
fun begin_theory name imports = 

141 
let 

26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26668
diff
changeset

142 
val thy = Context.begin_thy Syntax.pp_global name imports; 
24666  143 
val wrappers = begin_wrappers thy; 
33168  144 
in 
145 
thy 

146 
> Sign.local_path 

147 
> Sign.map_naming (Name_Space.set_theory_name name) 

148 
> apply_wrappers wrappers 

149 
end; 

24666  150 

151 
fun end_theory thy = 

152 
thy > apply_wrappers (end_wrappers thy) > Context.finish_thy; 

153 

16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

154 

3996  155 

24666  156 
(** add axioms **) 
3814  157 

1526  158 
(* prepare axioms *) 
159 

29581  160 
fun cert_axm thy (b, raw_tm) = 
1526  161 
let 
32789
d89327de0b3c
removed redundant Sign.certify_prop, use Sign.cert_prop instead;
wenzelm
parents:
30466
diff
changeset

162 
val t = Sign.cert_prop thy raw_tm 
2979  163 
handle TYPE (msg, _, _) => error msg 
16291  164 
 TERM (msg, _) => error msg; 
1526  165 
in 
9537  166 
Term.no_dummy_patterns t handle TERM (msg, _) => error msg; 
29581  167 
(b, Sign.no_vars (Syntax.pp_global thy) t) 
9629  168 
end; 
1526  169 

30337
eb189f7e43a1
Theory.add_axioms/add_defs: replaced old bstring by binding;
wenzelm
parents:
30218
diff
changeset

170 
fun read_axm thy (b, str) = 
eb189f7e43a1
Theory.add_axioms/add_defs: replaced old bstring by binding;
wenzelm
parents:
30218
diff
changeset

171 
cert_axm thy (b, Syntax.read_prop_global thy str) handle ERROR msg => 
33092
c859019d3ac5
eliminated separate stamp  NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents:
32966
diff
changeset

172 
cat_error msg ("The error(s) above occurred in axiom " ^ quote (Binding.str_of b)); 
1526  173 

174 

16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

175 
(* add_axioms(_i) *) 
1526  176 

16291  177 
local 
178 

16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

179 
fun gen_add_axioms prep_axm raw_axms thy = thy > map_axioms (fn axioms => 
1526  180 
let 
29581  181 
val axms = map (apsnd Logic.varify o prep_axm thy) raw_axms; 
33095
bbd52d2f8696
renamed NameSpace to Name_Space  also to emphasize its subtle change in semantics;
wenzelm
parents:
33092
diff
changeset

182 
val axioms' = fold (#2 oo Name_Space.define true (Sign.naming_of thy)) axms axioms; 
16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

183 
in axioms' end); 
1526  184 

16291  185 
in 
186 

29581  187 
val add_axioms_i = gen_add_axioms cert_axm; 
16291  188 
val add_axioms = gen_add_axioms read_axm; 
189 

190 
end; 

1526  191 

192 

3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

193 

e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

194 
(** add constant definitions **) 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

195 

19708
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

196 
(* dependencies *) 
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

197 

a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

198 
fun dependencies thy unchecked is_def name lhs rhs = 
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

199 
let 
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26668
diff
changeset

200 
val pp = Syntax.pp_global thy; 
19708
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

201 
val consts = Sign.consts_of thy; 
19727  202 
fun prep const = 
203 
let val Const (c, T) = Sign.no_vars pp (Const const) 

26631
d6b6c74a8bcf
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25059
diff
changeset

204 
in (c, Consts.typargs consts (c, Logic.varifyT T)) end; 
19708
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

205 

a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

206 
val lhs_vars = Term.add_tfreesT (#2 lhs) []; 
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

207 
val rhs_extras = fold (#2 #> Term.fold_atyps (fn TFree v => 
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

208 
if member (op =) lhs_vars v then I else insert (op =) v  _ => I)) rhs []; 
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

209 
val _ = 
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

210 
if null rhs_extras then () 
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

211 
else error ("Specification depends on extra type variables: " ^ 
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

212 
commas_quote (map (Pretty.string_of_typ pp o TFree) rhs_extras) ^ 
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

213 
"\nThe error(s) above occurred in " ^ quote name); 
24199  214 
in Defs.define pp unchecked is_def name (prep lhs) (map prep rhs) end; 
19708
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

215 

a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

216 
fun add_deps a raw_lhs raw_rhs thy = 
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

217 
let 
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

218 
val lhs :: rhs = map (dest_Const o Sign.cert_term thy o Const) (raw_lhs :: raw_rhs); 
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

219 
val name = if a = "" then (#1 lhs ^ " axiom") else a; 
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

220 
in thy > map_defs (dependencies thy false false name lhs rhs) end; 
17706  221 

28112
691993ef6abe
simplified specify_const: canonical args, global deps;
wenzelm
parents:
28017
diff
changeset

222 
fun specify_const tags decl thy = 
25017  223 
let val (t as Const const, thy') = Sign.declare_const tags decl thy 
28112
691993ef6abe
simplified specify_const: canonical args, global deps;
wenzelm
parents:
28017
diff
changeset

224 
in (t, add_deps "" const [] thy') end; 
25017  225 

17706  226 

16944  227 
(* check_overloading *) 
9280  228 

16944  229 
fun check_overloading thy overloaded (c, T) = 
16291  230 
let 
24763  231 
val declT = Sign.the_const_constraint thy c 
232 
handle TYPE (msg, _, _) => error msg; 

19806  233 
val T' = Logic.varifyT T; 
16944  234 

235 
fun message txt = 

236 
[Pretty.block [Pretty.str "Specification of constant ", 

26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26668
diff
changeset

237 
Pretty.str c, Pretty.str " ::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ_global thy T)], 
16944  238 
Pretty.str txt] > Pretty.chunks > Pretty.string_of; 
16291  239 
in 
16944  240 
if Sign.typ_instance thy (declT, T') then () 
241 
else if Type.raw_instance (declT, T') then 

32966
5b21661fe618
indicate CRITICAL nature of various setmp combinators;
wenzelm
parents:
32789
diff
changeset

242 
error (setmp_CRITICAL show_sorts true 
16944  243 
message "imposes additional sort constraints on the constant declaration") 
244 
else if overloaded then () 

245 
else warning (message "is strictly less general than the declared type"); 

246 
(c, T) 

9280  247 
end; 
248 

3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

249 

16291  250 
(* check_def *) 
251 

29581  252 
fun check_def thy unchecked overloaded (b, tm) defs = 
16291  253 
let 
24981
4ec3f95190bf
dest/cert_def: replaced Pretty.pp by explicit Proof.context;
wenzelm
parents:
24966
diff
changeset

254 
val ctxt = ProofContext.init thy; 
29581  255 
val name = Sign.full_name thy b; 
24981
4ec3f95190bf
dest/cert_def: replaced Pretty.pp by explicit Proof.context;
wenzelm
parents:
24966
diff
changeset

256 
val (lhs_const, rhs) = Sign.cert_def ctxt tm; 
16944  257 
val rhs_consts = fold_aterms (fn Const const => insert (op =) const  _ => I) rhs []; 
18943  258 
val _ = check_overloading thy overloaded lhs_const; 
19708
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

259 
in defs > dependencies thy unchecked true name lhs_const rhs_consts end 
18678  260 
handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block 
30218  261 
[Pretty.str ("The error(s) above occurred in definition " ^ quote (Binding.str_of b) ^ ":"), 
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26668
diff
changeset

262 
Pretty.fbrk, Pretty.quote (Syntax.pretty_term_global thy tm)])); 
3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

263 

e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

264 

16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

265 
(* add_defs(_i) *) 
3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

266 

16291  267 
local 
9320  268 

19630  269 
fun gen_add_defs prep_axm unchecked overloaded raw_axms thy = 
16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

270 
let val axms = map (prep_axm thy) raw_axms in 
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

271 
thy 
19630  272 
> map_defs (fold (check_def thy unchecked overloaded) axms) 
9320  273 
> add_axioms_i axms 
3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

274 
end; 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

275 

16291  276 
in 
277 

278 
val add_defs_i = gen_add_defs cert_axm; 

279 
val add_defs = gen_add_defs read_axm; 

280 

281 
end; 

3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

282 

e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

283 

16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

284 
(* add_finals(_i) *) 
14223
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

285 

16291  286 
local 
287 

17706  288 
fun gen_add_finals prep_term overloaded args thy = 
14223
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

289 
let 
17706  290 
fun const_of (Const const) = const 
291 
 const_of (Free _) = error "Attempt to finalize variable (or undeclared constant)" 

292 
 const_of _ = error "Attempt to finalize nonconstant term"; 

19708
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

293 
fun specify (c, T) = dependencies thy false false (c ^ " axiom") (c, T) []; 
24708  294 
val finalize = specify o check_overloading thy overloaded o const_of o 
295 
Sign.cert_term thy o prep_term thy; 

17706  296 
in thy > map_defs (fold finalize args) end; 
16291  297 

14223
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

298 
in 
16291  299 

29581  300 
val add_finals_i = gen_add_finals (K I); 
24708  301 
val add_finals = gen_add_finals Syntax.read_term_global; 
16291  302 

14223
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

303 
end; 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

304 

1526  305 
end; 