16 val assert_bottom: bool -> state -> state |
16 val assert_bottom: bool -> state -> state |
17 val context_of: state -> context |
17 val context_of: state -> context |
18 val theory_of: state -> theory |
18 val theory_of: state -> theory |
19 val map_context: (context -> context) -> state -> state |
19 val map_context: (context -> context) -> state -> state |
20 val add_binds_i: (indexname * term option) list -> state -> state |
20 val add_binds_i: (indexname * term option) list -> state -> state |
21 val put_thms: bool -> string * thm list option -> state -> state |
21 val put_thms: string * thm list option -> state -> state |
22 val put_thms_internal: string * thm list option -> state -> state |
|
23 val the_facts: state -> thm list |
22 val the_facts: state -> thm list |
24 val the_fact: state -> thm |
23 val the_fact: state -> thm |
25 val put_facts: thm list option -> state -> state |
24 val put_facts: thm list option -> state -> state |
26 val assert_forward: state -> state |
25 val assert_forward: state -> state |
27 val assert_chain: state -> state |
26 val assert_chain: state -> state |
88 (theory -> 'a -> attribute) -> |
87 (theory -> 'a -> attribute) -> |
89 (context * 'b list -> context * (term list list * (context -> context))) -> |
88 (context * 'b list -> context * (term list list * (context -> context))) -> |
90 string -> Method.text option -> (thm list list -> state -> state Seq.seq) -> |
89 string -> Method.text option -> (thm list list -> state -> state Seq.seq) -> |
91 ((string * 'a list) * 'b) list -> state -> state |
90 ((string * 'a list) * 'b) list -> state -> state |
92 val local_qed: Method.text option * bool -> state -> state Seq.seq |
91 val local_qed: Method.text option * bool -> state -> state Seq.seq |
93 val theorem: string -> Method.text option -> (thm list list -> context -> context) -> |
92 val theorem: Method.text option -> (thm list list -> context -> context) -> |
94 (string * string list) list list -> context -> state |
93 (string * string list) list list -> context -> state |
95 val theorem_i: string -> Method.text option -> (thm list list -> context -> context) -> |
94 val theorem_i: Method.text option -> (thm list list -> context -> context) -> |
96 (term * term list) list list -> context -> state |
95 (term * term list) list list -> context -> state |
97 val global_qed: Method.text option * bool -> state -> context |
96 val global_qed: Method.text option * bool -> state -> context |
98 val local_terminal_proof: Method.text * Method.text option -> state -> state Seq.seq |
97 val local_terminal_proof: Method.text * Method.text option -> state -> state Seq.seq |
99 val local_default_proof: state -> state Seq.seq |
98 val local_default_proof: state -> state Seq.seq |
100 val local_immediate_proof: state -> state Seq.seq |
99 val local_immediate_proof: state -> state Seq.seq |
192 |
191 |
193 fun map_context_result f state = |
192 fun map_context_result f state = |
194 f (context_of state) ||> (fn ctxt => map_context (K ctxt) state); |
193 f (context_of state) ||> (fn ctxt => map_context (K ctxt) state); |
195 |
194 |
196 val add_binds_i = map_context o ProofContext.add_binds_i; |
195 val add_binds_i = map_context o ProofContext.add_binds_i; |
197 val put_thms = map_context oo ProofContext.put_thms; |
196 val put_thms = map_context o ProofContext.put_thms; |
198 val put_thms_internal = map_context o ProofContext.put_thms_internal; |
|
199 |
197 |
200 |
198 |
201 (* facts *) |
199 (* facts *) |
202 |
200 |
203 val get_facts = #facts o current; |
201 val get_facts = #facts o current; |
210 (case the_facts state of [thm] => thm |
208 (case the_facts state of [thm] => thm |
211 | _ => error "Single theorem expected"); |
209 | _ => error "Single theorem expected"); |
212 |
210 |
213 fun put_facts facts = |
211 fun put_facts facts = |
214 map_current (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) #> |
212 map_current (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) #> |
215 put_thms_internal (AutoBind.thisN, facts); |
213 put_thms (AutoBind.thisN, facts); |
216 |
214 |
217 fun these_factss more_facts (named_factss, state) = |
215 fun these_factss more_facts (named_factss, state) = |
218 (named_factss, state |> put_facts (SOME (maps snd named_factss @ more_facts))); |
216 (named_factss, state |> put_facts (SOME (maps snd named_factss @ more_facts))); |
219 |
217 |
220 fun export_facts inner outer = |
218 fun export_facts inner outer = |
332 |
330 |
333 fun description strs = |
331 fun description strs = |
334 (case filter_out (equal "") strs of [] => "" |
332 (case filter_out (equal "") strs of [] => "" |
335 | strs' => enclose " (" ")" (commas strs')); |
333 | strs' => enclose " (" ")" (commas strs')); |
336 |
334 |
337 fun prt_goal (SOME (ctxt, (i, {statement = (kind, _), using, goal, before_qed, after_qed}))) = |
335 fun prt_goal (SOME (ctxt, (i, {using, goal, before_qed, after_qed, ...}))) = |
338 pretty_facts "using " ctxt |
336 pretty_facts "using " ctxt |
339 (if mode <> Backward orelse null using then NONE else SOME using) @ |
337 (if mode <> Backward orelse null using then NONE else SOME using) @ |
340 [Pretty.str ("goal" ^ description [kind, levels_up (i div 2), |
338 [Pretty.str ("goal" ^ |
341 subgoals (Thm.nprems_of goal)] ^ ":")] @ |
339 description [levels_up (i div 2), subgoals (Thm.nprems_of goal)] ^ ":")] @ |
342 pretty_goals_local ctxt bg (true, ! show_main_goal) (! Display.goals_limit) goal |
340 pretty_goals_local ctxt bg (true, ! show_main_goal) (! Display.goals_limit) goal |
343 | prt_goal NONE = []; |
341 | prt_goal NONE = []; |
344 |
342 |
345 val prt_ctxt = |
343 val prt_ctxt = |
346 if ! verbose orelse mode = Forward then ProofContext.pretty_context context |
344 if ! verbose orelse mode = Forward then ProofContext.pretty_context context |
595 ||> opt_chain |
593 ||> opt_chain |
596 |> opt_result; |
594 |> opt_result; |
597 |
595 |
598 in |
596 in |
599 |
597 |
600 val note_thmss = gen_thmss ProofContext.note_thmss (K []) I #2 Attrib.attribute; |
598 val note_thmss = gen_thmss (ProofContext.note_thmss "") (K []) I #2 Attrib.attribute; |
601 val note_thmss_i = gen_thmss ProofContext.note_thmss_i (K []) I #2 (K I); |
599 val note_thmss_i = gen_thmss (ProofContext.note_thmss_i "") (K []) I #2 (K I); |
602 |
600 |
603 val from_thmss = |
601 val from_thmss = |
604 gen_thmss ProofContext.note_thmss (K []) chain #2 Attrib.attribute o no_binding; |
602 gen_thmss (ProofContext.note_thmss "") (K []) chain #2 Attrib.attribute o no_binding; |
605 val from_thmss_i = gen_thmss ProofContext.note_thmss_i (K []) chain #2 (K I) o no_binding; |
603 val from_thmss_i = gen_thmss (ProofContext.note_thmss_i "") (K []) chain #2 (K I) o no_binding; |
606 |
604 |
607 val with_thmss = |
605 val with_thmss = |
608 gen_thmss ProofContext.note_thmss the_facts chain #2 Attrib.attribute o no_binding; |
606 gen_thmss (ProofContext.note_thmss "") the_facts chain #2 Attrib.attribute o no_binding; |
609 val with_thmss_i = gen_thmss ProofContext.note_thmss_i the_facts chain #2 (K I) o no_binding; |
607 val with_thmss_i = gen_thmss (ProofContext.note_thmss_i "") the_facts chain #2 (K I) o no_binding; |
610 |
608 |
611 val local_results = |
609 val local_results = |
612 gen_thmss ProofContext.note_thmss_i (K []) I I (K I) o map (apsnd Thm.simple_fact); |
610 gen_thmss (ProofContext.note_thmss_i "") (K []) I I (K I) o map (apsnd Thm.simple_fact); |
613 |
611 |
614 fun get_thmss state srcs = the_facts (note_thmss [(("", []), srcs)] state); |
612 fun get_thmss state srcs = the_facts (note_thmss [(("", []), srcs)] state); |
615 fun simple_note_thms name thms = note_thmss_i [((name, []), [(thms, [])])]; |
613 fun simple_note_thms name thms = note_thmss_i [((name, []), [(thms, [])])]; |
616 |
614 |
617 end; |
615 end; |
622 local |
620 local |
623 |
621 |
624 fun gen_using f g note prep_atts args state = |
622 fun gen_using f g note prep_atts args state = |
625 state |
623 state |
626 |> assert_backward |
624 |> assert_backward |
627 |> map_context_result (note (Attrib.map_facts (prep_atts (theory_of state)) (no_binding args))) |
625 |> map_context_result |
|
626 (note "" (Attrib.map_facts (prep_atts (theory_of state)) (no_binding args))) |
628 |> (fn (named_facts, state') => |
627 |> (fn (named_facts, state') => |
629 state' |> map_goal I (fn (statement, using, goal, before_qed, after_qed) => |
628 state' |> map_goal I (fn (statement, using, goal, before_qed, after_qed) => |
630 let |
629 let |
631 val ctxt = context_of state'; |
630 val ctxt = context_of state'; |
632 val ths = maps snd named_facts; |
631 val ths = maps snd named_facts; |
832 Seq.maps (generic_qed #-> (fn ((after_qed, _), results) => after_qed results)); |
831 Seq.maps (generic_qed #-> (fn ((after_qed, _), results) => after_qed results)); |
833 |
832 |
834 |
833 |
835 (* global goals *) |
834 (* global goals *) |
836 |
835 |
837 fun global_goal prepp kind before_qed after_qed propp ctxt = |
836 fun global_goal prepp before_qed after_qed propp ctxt = |
838 init ctxt |
837 init ctxt |
839 |> generic_goal (prepp #> ProofContext.auto_fixes) kind |
838 |> generic_goal (prepp #> ProofContext.auto_fixes) "" |
840 before_qed (K Seq.single, after_qed) propp; |
839 before_qed (K Seq.single, after_qed) propp; |
841 |
840 |
842 val theorem = global_goal ProofContext.bind_propp_schematic; |
841 val theorem = global_goal ProofContext.bind_propp_schematic; |
843 val theorem_i = global_goal ProofContext.bind_propp_schematic_i; |
842 val theorem_i = global_goal ProofContext.bind_propp_schematic_i; |
844 |
843 |