58 (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> |
58 (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> |
59 (binding * string option * mixfix) list -> |
59 (binding * string option * mixfix) list -> |
60 bool -> local_theory -> (string * thm list) list * local_theory |
60 bool -> local_theory -> (string * thm list) list * local_theory |
61 val theorem: string -> Method.text option -> |
61 val theorem: string -> Method.text option -> |
62 (thm list list -> local_theory -> local_theory) -> Attrib.binding -> |
62 (thm list list -> local_theory -> local_theory) -> Attrib.binding -> |
63 Element.context_i list -> Element.statement_i -> |
63 string list -> Element.context_i list -> Element.statement_i -> |
64 bool -> local_theory -> Proof.state |
64 bool -> local_theory -> Proof.state |
65 val theorem_cmd: string -> Method.text option -> |
65 val theorem_cmd: string -> Method.text option -> |
66 (thm list list -> local_theory -> local_theory) -> Attrib.binding -> |
66 (thm list list -> local_theory -> local_theory) -> Attrib.binding -> |
67 Element.context list -> Element.statement -> |
67 (xstring * Position.T) list -> Element.context list -> Element.statement -> |
68 bool -> local_theory -> Proof.state |
68 bool -> local_theory -> Proof.state |
69 val schematic_theorem: string -> Method.text option -> |
69 val schematic_theorem: string -> Method.text option -> |
70 (thm list list -> local_theory -> local_theory) -> Attrib.binding -> |
70 (thm list list -> local_theory -> local_theory) -> Attrib.binding -> |
71 Element.context_i list -> Element.statement_i -> |
71 string list -> Element.context_i list -> Element.statement_i -> |
72 bool -> local_theory -> Proof.state |
72 bool -> local_theory -> Proof.state |
73 val schematic_theorem_cmd: string -> Method.text option -> |
73 val schematic_theorem_cmd: string -> Method.text option -> |
74 (thm list list -> local_theory -> local_theory) -> Attrib.binding -> |
74 (thm list list -> local_theory -> local_theory) -> Attrib.binding -> |
75 Element.context list -> Element.statement -> |
75 (xstring * Position.T) list -> Element.context list -> Element.statement -> |
76 bool -> local_theory -> Proof.state |
76 bool -> local_theory -> Proof.state |
77 val add_theorem_hook: (bool -> Proof.state -> Proof.state) -> Context.generic -> Context.generic |
77 val add_theorem_hook: (bool -> Proof.state -> Proof.state) -> Context.generic -> Context.generic |
78 end; |
78 end; |
79 |
79 |
80 structure Specification: SPECIFICATION = |
80 structure Specification: SPECIFICATION = |
376 val empty = []; |
376 val empty = []; |
377 val extend = I; |
377 val extend = I; |
378 fun merge data : T = Library.merge (eq_snd op =) data; |
378 fun merge data : T = Library.merge (eq_snd op =) data; |
379 ); |
379 ); |
380 |
380 |
381 fun gen_theorem schematic prep_att prep_stmt |
381 fun gen_theorem schematic prep_bundle prep_att prep_stmt |
382 kind before_qed after_qed (name, raw_atts) raw_elems raw_concl int lthy = |
382 kind before_qed after_qed (name, raw_atts) raw_includes raw_elems raw_concl int lthy = |
383 let |
383 let |
384 val _ = Local_Theory.assert lthy; |
384 val _ = Local_Theory.assert lthy; |
385 val thy = Proof_Context.theory_of lthy; |
385 val thy = Proof_Context.theory_of lthy; |
386 |
386 |
387 val attrib = prep_att thy; |
387 val attrib = prep_att thy; |
|
388 |
388 val elems = raw_elems |> map (Element.map_ctxt_attrib attrib); |
389 val elems = raw_elems |> map (Element.map_ctxt_attrib attrib); |
389 val ((more_atts, prems, stmt, facts), goal_ctxt) = |
390 val ((more_atts, prems, stmt, facts), goal_ctxt) = lthy |
390 prep_statement attrib prep_stmt elems raw_concl lthy; |
391 |> Bundle.includes (map (prep_bundle lthy) raw_includes) |
|
392 |> prep_statement attrib prep_stmt elems raw_concl; |
391 val atts = more_atts @ map attrib raw_atts; |
393 val atts = more_atts @ map attrib raw_atts; |
392 |
394 |
393 fun after_qed' results goal_ctxt' = |
395 fun after_qed' results goal_ctxt' = |
394 let |
396 let |
395 val results' = burrow (map Goal.norm_result o Proof_Context.export goal_ctxt' lthy) results; |
397 val results' = burrow (map Goal.norm_result o Proof_Context.export goal_ctxt' lthy) results; |
419 |> fold_rev (fn (f, _) => f int) (Theorem_Hook.get (Context.Proof goal_ctxt)) |
421 |> fold_rev (fn (f, _) => f int) (Theorem_Hook.get (Context.Proof goal_ctxt)) |
420 end; |
422 end; |
421 |
423 |
422 in |
424 in |
423 |
425 |
424 val theorem' = gen_theorem false (K I) Expression.cert_statement; |
426 val theorem = gen_theorem false (K I) (K I) Expression.cert_statement; |
425 fun theorem a b c d e f = theorem' a b c d e f; |
427 val theorem_cmd = |
426 val theorem_cmd = gen_theorem false Attrib.intern_src Expression.read_statement; |
428 gen_theorem false Bundle.check Attrib.intern_src Expression.read_statement; |
427 |
429 |
428 val schematic_theorem = gen_theorem true (K I) Expression.cert_statement; |
430 val schematic_theorem = gen_theorem true (K I) (K I) Expression.cert_statement; |
429 val schematic_theorem_cmd = gen_theorem true Attrib.intern_src Expression.read_statement; |
431 val schematic_theorem_cmd = |
|
432 gen_theorem true Bundle.check Attrib.intern_src Expression.read_statement; |
430 |
433 |
431 fun add_theorem_hook f = Theorem_Hook.map (cons (f, stamp ())); |
434 fun add_theorem_hook f = Theorem_Hook.map (cons (f, stamp ())); |
432 |
435 |
433 end; |
436 end; |
434 |
437 |