31 val plain_prop_of: thm -> term |
31 val plain_prop_of: thm -> term |
32 val fold_terms: (term -> 'a -> 'a) -> thm -> 'a -> 'a |
32 val fold_terms: (term -> 'a -> 'a) -> thm -> 'a -> 'a |
33 val add_thm: thm -> thm list -> thm list |
33 val add_thm: thm -> thm list -> thm list |
34 val del_thm: thm -> thm list -> thm list |
34 val del_thm: thm -> thm list -> thm list |
35 val merge_thms: thm list * thm list -> thm list |
35 val merge_thms: thm list * thm list -> thm list |
|
36 val elim_implies: thm -> thm -> thm |
|
37 val forall_elim_var: int -> thm -> thm |
|
38 val forall_elim_vars: int -> thm -> thm |
|
39 val unvarify: thm -> thm |
|
40 val close_derivation: thm -> thm |
|
41 val add_axiom: term list -> bstring * term -> theory -> thm * theory |
|
42 val add_def: bool -> bool -> bstring * term -> theory -> thm * theory |
|
43 val rule_attribute: (Context.generic -> thm -> thm) -> attribute |
|
44 val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute |
|
45 val theory_attributes: attribute list -> theory * thm -> theory * thm |
|
46 val proof_attributes: attribute list -> Proof.context * thm -> Proof.context * thm |
|
47 val no_attributes: 'a -> 'a * 'b list |
|
48 val simple_fact: 'a -> ('a * 'b list) list |
|
49 val tag_rule: Markup.property -> thm -> thm |
|
50 val untag_rule: string -> thm -> thm |
|
51 val tag: Markup.property -> attribute |
|
52 val untag: string -> attribute |
|
53 val position_of: thm -> Position.T |
|
54 val default_position: Position.T -> thm -> thm |
|
55 val default_position_of: thm -> thm -> thm |
|
56 val has_name_hint: thm -> bool |
|
57 val get_name_hint: thm -> string |
|
58 val put_name_hint: string -> thm -> thm |
|
59 val get_group: thm -> string option |
|
60 val put_group: string -> thm -> thm |
|
61 val group: string -> attribute |
36 val axiomK: string |
62 val axiomK: string |
37 val assumptionK: string |
63 val assumptionK: string |
38 val definitionK: string |
64 val definitionK: string |
39 val theoremK: string |
65 val theoremK: string |
40 val lemmaK: string |
66 val lemmaK: string |
41 val corollaryK: string |
67 val corollaryK: string |
42 val internalK: string |
68 val internalK: string |
43 val rule_attribute: (Context.generic -> thm -> thm) -> attribute |
69 val has_kind: thm -> bool |
44 val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute |
70 val get_kind: thm -> string |
45 val theory_attributes: attribute list -> theory * thm -> theory * thm |
71 val kind_rule: string -> thm -> thm |
46 val proof_attributes: attribute list -> Proof.context * thm -> Proof.context * thm |
72 val kind: string -> attribute |
47 val no_attributes: 'a -> 'a * 'b list |
73 val kind_internal: attribute |
48 val simple_fact: 'a -> ('a * 'b list) list |
74 val has_internal: Markup.property list -> bool |
49 val elim_implies: thm -> thm -> thm |
75 val is_internal: thm -> bool |
50 val forall_elim_var: int -> thm -> thm |
|
51 val forall_elim_vars: int -> thm -> thm |
|
52 val unvarify: thm -> thm |
|
53 val close_derivation: thm -> thm |
|
54 val add_axiom: term list -> bstring * term -> theory -> thm * theory |
|
55 val add_def: bool -> bool -> bstring * term -> theory -> thm * theory |
|
56 end; |
76 end; |
57 |
77 |
58 structure Thm: THM = |
78 structure Thm: THM = |
59 struct |
79 struct |
60 |
80 |
173 val del_thm = remove eq_thm_prop; |
193 val del_thm = remove eq_thm_prop; |
174 val merge_thms = merge eq_thm_prop; |
194 val merge_thms = merge eq_thm_prop; |
175 |
195 |
176 |
196 |
177 |
197 |
178 (** theorem kinds **) |
|
179 |
|
180 val axiomK = "axiom"; |
|
181 val assumptionK = "assumption"; |
|
182 val definitionK = "definition"; |
|
183 val theoremK = "theorem"; |
|
184 val lemmaK = "lemma"; |
|
185 val corollaryK = "corollary"; |
|
186 val internalK = Markup.internalK; |
|
187 |
|
188 |
|
189 |
|
190 (** attributes **) |
|
191 |
|
192 fun rule_attribute f (x, th) = (x, f x th); |
|
193 fun declaration_attribute f (x, th) = (f th x, th); |
|
194 |
|
195 fun apply_attributes mk dest = |
|
196 let |
|
197 fun app [] = I |
|
198 | app ((f: attribute) :: fs) = fn (x, th) => f (mk x, th) |>> dest |> app fs; |
|
199 in app end; |
|
200 |
|
201 val theory_attributes = apply_attributes Context.Theory Context.the_theory; |
|
202 val proof_attributes = apply_attributes Context.Proof Context.the_proof; |
|
203 |
|
204 fun no_attributes x = (x, []); |
|
205 fun simple_fact x = [(x, [])]; |
|
206 |
|
207 |
|
208 |
|
209 (** basic derived rules **) |
198 (** basic derived rules **) |
210 |
199 |
211 (*Elimination of implication |
200 (*Elimination of implication |
212 A A ==> B |
201 A A ==> B |
213 ------------ |
202 ------------ |
294 val thy' = Theory.add_defs_i unchecked overloaded [(name, prop')] thy; |
283 val thy' = Theory.add_defs_i unchecked overloaded [(name, prop')] thy; |
295 val axm' = Thm.get_axiom_i thy' (Sign.full_name thy' name); |
284 val axm' = Thm.get_axiom_i thy' (Sign.full_name thy' name); |
296 val thm = unvarify (Thm.instantiate (recover_sorts, []) axm'); |
285 val thm = unvarify (Thm.instantiate (recover_sorts, []) axm'); |
297 in (thm, thy') end; |
286 in (thm, thy') end; |
298 |
287 |
|
288 |
|
289 |
|
290 (** attributes **) |
|
291 |
|
292 fun rule_attribute f (x, th) = (x, f x th); |
|
293 fun declaration_attribute f (x, th) = (f th x, th); |
|
294 |
|
295 fun apply_attributes mk dest = |
|
296 let |
|
297 fun app [] = I |
|
298 | app ((f: attribute) :: fs) = fn (x, th) => f (mk x, th) |>> dest |> app fs; |
|
299 in app end; |
|
300 |
|
301 val theory_attributes = apply_attributes Context.Theory Context.the_theory; |
|
302 val proof_attributes = apply_attributes Context.Proof Context.the_proof; |
|
303 |
|
304 fun no_attributes x = (x, []); |
|
305 fun simple_fact x = [(x, [])]; |
|
306 |
|
307 |
|
308 |
|
309 (*** theorem tags ***) |
|
310 |
|
311 (* add / delete tags *) |
|
312 |
|
313 fun tag_rule tg = Thm.map_tags (insert (op =) tg); |
|
314 fun untag_rule s = Thm.map_tags (filter_out (fn (s', _) => s = s')); |
|
315 |
|
316 fun tag tg x = rule_attribute (K (tag_rule tg)) x; |
|
317 fun untag s x = rule_attribute (K (untag_rule s)) x; |
|
318 |
|
319 |
|
320 (* position *) |
|
321 |
|
322 val position_of = Position.of_properties o Thm.get_tags; |
|
323 |
|
324 fun default_position pos = Thm.map_tags (Position.default_properties pos); |
|
325 val default_position_of = default_position o position_of; |
|
326 |
|
327 |
|
328 (* unofficial theorem names *) |
|
329 |
|
330 fun the_name_hint thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.nameN); |
|
331 |
|
332 val has_name_hint = can the_name_hint; |
|
333 val get_name_hint = the_default "??.unknown" o try the_name_hint; |
|
334 |
|
335 fun put_name_hint name = untag_rule Markup.nameN #> tag_rule (Markup.nameN, name); |
|
336 |
|
337 |
|
338 (* theorem groups *) |
|
339 |
|
340 fun get_group thm = AList.lookup (op =) (Thm.get_tags thm) Markup.groupN; |
|
341 |
|
342 fun put_group name = |
|
343 if name = "" then I else Thm.map_tags (AList.update (op =) (Markup.groupN, name)); |
|
344 |
|
345 fun group name = rule_attribute (K (put_group name)); |
|
346 |
|
347 |
|
348 (* theorem kinds *) |
|
349 |
|
350 val axiomK = "axiom"; |
|
351 val assumptionK = "assumption"; |
|
352 val definitionK = "definition"; |
|
353 val theoremK = "theorem"; |
|
354 val lemmaK = "lemma"; |
|
355 val corollaryK = "corollary"; |
|
356 val internalK = Markup.internalK; |
|
357 |
|
358 fun the_kind thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.kindN); |
|
359 |
|
360 val has_kind = can the_kind; |
|
361 val get_kind = the_default "" o try the_kind; |
|
362 |
|
363 fun kind_rule k = tag_rule (Markup.kindN, k) o untag_rule Markup.kindN; |
|
364 fun kind k x = if k = "" then x else rule_attribute (K (kind_rule k)) x; |
|
365 fun kind_internal x = kind internalK x; |
|
366 fun has_internal tags = exists (fn tg => tg = (Markup.kindN, internalK)) tags; |
|
367 val is_internal = has_internal o Thm.get_tags; |
|
368 |
|
369 |
299 open Thm; |
370 open Thm; |
300 |
371 |
301 end; |
372 end; |
302 |
373 |
303 val op aconvc = Thm.aconvc; |
374 val op aconvc = Thm.aconvc; |