14 val init_state: theory -> state |
14 val init_state: theory -> state |
15 val context_of: state -> context |
15 val context_of: state -> context |
16 val theory_of: state -> theory |
16 val theory_of: state -> theory |
17 val sign_of: state -> Sign.sg |
17 val sign_of: state -> Sign.sg |
18 val the_facts: state -> thm list |
18 val the_facts: state -> thm list |
19 val the_fact: state -> thm |
|
20 val get_goal: state -> thm list * thm |
19 val get_goal: state -> thm list * thm |
21 val goal_facts: (state -> thm list) -> state -> state |
20 val goal_facts: (state -> thm list) -> state -> state |
22 val use_facts: state -> state |
21 val use_facts: state -> state |
23 val reset_facts: state -> state |
22 val reset_facts: state -> state |
24 val assert_forward: state -> state |
23 val assert_forward: state -> state |
25 val assert_backward: state -> state |
24 val assert_backward: state -> state |
26 val enter_forward: state -> state |
25 val enter_forward: state -> state |
27 val show_hyps: bool ref |
26 val show_hyps: bool ref |
28 val pretty_thm: thm -> Pretty.T |
27 val pretty_thm: thm -> Pretty.T |
|
28 val pretty_thms: thm list -> Pretty.T |
29 val verbose: bool ref |
29 val verbose: bool ref |
30 val print_state: int -> state -> unit |
30 val print_state: int -> state -> unit |
31 val level: state -> int |
31 val level: state -> int |
32 type method |
32 type method |
33 val method: (thm list -> tactic) -> method |
33 val method: (thm list -> tactic) -> method |
38 val match_bind: (string list * string) list -> state -> state |
38 val match_bind: (string list * string) list -> state -> state |
39 val match_bind_i: (term list * term) list -> state -> state |
39 val match_bind_i: (term list * term) list -> state -> state |
40 val have_thmss: thm list -> string -> context attribute list -> |
40 val have_thmss: thm list -> string -> context attribute list -> |
41 (thm list * context attribute list) list -> state -> state |
41 (thm list * context attribute list) list -> state -> state |
42 val simple_have_thms: string -> thm list -> state -> state |
42 val simple_have_thms: string -> thm list -> state -> state |
43 val fix: (string * string option) list -> state -> state |
43 val fix: (string list * string option) list -> state -> state |
44 val fix_i: (string * typ) list -> state -> state |
44 val fix_i: (string list * typ) list -> state -> state |
45 val assm: (int -> tactic) * (int -> tactic) |
45 val assm: (int -> tactic) * (int -> tactic) |
46 -> (string * context attribute list * (string * (string list * string list)) list) list |
46 -> (string * context attribute list * (string * (string list * string list)) list) list |
47 -> state -> state |
47 -> state -> state |
48 val assm_i: (int -> tactic) * (int -> tactic) |
48 val assm_i: (int -> tactic) * (int -> tactic) |
49 -> (string * context attribute list * (term * (term list * term list)) list) list |
49 -> (string * context attribute list * (term * (term list * term list)) list) list |
189 (* facts *) |
189 (* facts *) |
190 |
190 |
191 fun the_facts (State (Node {facts = Some facts, ...}, _)) = facts |
191 fun the_facts (State (Node {facts = Some facts, ...}, _)) = facts |
192 | the_facts state = raise STATE ("No current facts available", state); |
192 | the_facts state = raise STATE ("No current facts available", state); |
193 |
193 |
194 fun the_fact state = |
|
195 (case the_facts state of |
|
196 [fact] => fact |
|
197 | _ => raise STATE ("Single fact expected", state)); |
|
198 |
|
199 fun assert_facts state = (the_facts state; state); |
194 fun assert_facts state = (the_facts state; state); |
200 fun get_facts (State (Node {facts, ...}, _)) = facts; |
195 fun get_facts (State (Node {facts, ...}, _)) = facts; |
201 |
196 |
202 fun put_facts facts state = |
197 fun put_facts facts state = |
203 state |
198 state |
204 |> map_current (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) |
199 |> map_current (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) |
205 |> put_thms ("facts", if_none facts []); |
200 |> put_thms ("this", if_none facts []); |
206 |
201 |
207 val reset_facts = put_facts None; |
202 val reset_facts = put_facts None; |
208 |
203 |
209 fun have_facts (name, facts) state = |
204 fun have_facts (name, facts) state = |
210 state |
205 state |
286 (** print_state **) |
281 (** print_state **) |
287 |
282 |
288 val show_hyps = ProofContext.show_hyps; |
283 val show_hyps = ProofContext.show_hyps; |
289 val pretty_thm = ProofContext.pretty_thm; |
284 val pretty_thm = ProofContext.pretty_thm; |
290 |
285 |
|
286 fun pretty_thms [th] = pretty_thm th |
|
287 | pretty_thms ths = Pretty.block (Pretty.fbreaks (map pretty_thm ths)); |
|
288 |
|
289 |
291 val verbose = ProofContext.verbose; |
290 val verbose = ProofContext.verbose; |
292 |
291 |
293 fun print_facts _ None = () |
292 fun print_facts _ None = () |
294 | print_facts s (Some ths) = |
293 | print_facts s (Some ths) = |
295 Pretty.writeln (Pretty.big_list (s ^ " facts:") (map pretty_thm ths)); |
294 Pretty.writeln (Pretty.big_list (s ^ " facts:") (map pretty_thm ths)); |
301 fun levels_up 0 = "" |
300 fun levels_up 0 = "" |
302 | levels_up 1 = " (1 level up)" |
301 | levels_up 1 = " (1 level up)" |
303 | levels_up i = " (" ^ string_of_int i ^ " levels up)"; |
302 | levels_up i = " (" ^ string_of_int i ^ " levels up)"; |
304 |
303 |
305 fun print_goal (_, (i, (((kind, name, _), (goal_facts, thm)), _))) = |
304 fun print_goal (_, (i, (((kind, name, _), (goal_facts, thm)), _))) = |
306 (print_facts "Using" (if null goal_facts then None else Some goal_facts); |
305 (print_facts "Using" |
|
306 (if mode <> Backward orelse null goal_facts then None else Some goal_facts); |
307 writeln (kind_name kind ^ " " ^ quote name ^ levels_up (i div 2) ^ ":"); |
307 writeln (kind_name kind ^ " " ^ quote name ^ levels_up (i div 2) ^ ":"); |
308 Locale.print_goals_marker begin_goal (! goals_limit) thm); |
308 Locale.print_goals_marker begin_goal (! goals_limit) thm); |
309 |
309 |
310 val ctxt_strings = ProofContext.strings_of_context context; |
310 val ctxt_strings = ProofContext.strings_of_context context; |
311 in |
311 in |
585 let |
585 let |
586 val (state', prop) = |
586 val (state', prop) = |
587 state |
587 state |
588 |> assert_forward_or_chain |
588 |> assert_forward_or_chain |
589 |> enter_forward |
589 |> enter_forward |
590 |> opt_block |
|
591 |> map_context_result (fn c => prepp (c, raw_propp)); |
590 |> map_context_result (fn c => prepp (c, raw_propp)); |
592 val cprop = Thm.cterm_of (sign_of state') prop; |
591 val cprop = Thm.cterm_of (sign_of state') prop; |
593 val casms = map #1 (assumptions state'); |
592 val casms = map #1 (assumptions state'); |
594 |
593 |
595 val revcut_rl = Drule.incr_indexes_wrt [] [] (cprop :: casms) [] Drule.revcut_rl; |
594 val revcut_rl = Drule.incr_indexes_wrt [] [] (cprop :: casms) [] Drule.revcut_rl; |
596 fun cut_asm (casm, thm) = Thm.rotate_rule ~1 1 ((Drule.assume_goal casm COMP revcut_rl) RS thm); |
595 fun cut_asm (casm, thm) = Thm.rotate_rule ~1 1 ((Drule.assume_goal casm COMP revcut_rl) RS thm); |
597 val goal = foldr cut_asm (casms, Drule.mk_triv_goal cprop); |
596 val goal = foldr cut_asm (casms, Drule.mk_triv_goal cprop); |
598 in |
597 in |
599 state' |
598 state' |
|
599 |> opt_block |
600 |> put_goal (Some (((kind atts, (PureThy.default_name name), prop), ([], goal)), after_qed)) |
600 |> put_goal (Some (((kind atts, (PureThy.default_name name), prop), ([], goal)), after_qed)) |
601 |> auto_bind_goal prop |
601 |> auto_bind_goal prop |
602 |> (if is_chain state then use_facts else reset_facts) |
602 |> (if is_chain state then use_facts else reset_facts) |
603 |> new_block |
603 |> new_block |
604 |> enter_backward |
604 |> enter_backward |