48 val export_thm: context -> thm -> thm |
48 val export_thm: context -> thm -> thm |
49 val match_bind: (string list * string) list -> state -> state |
49 val match_bind: (string list * string) list -> state -> state |
50 val match_bind_i: (term list * term) list -> state -> state |
50 val match_bind_i: (term list * term) list -> state -> state |
51 val let_bind: (string list * string) list -> state -> state |
51 val let_bind: (string list * string) list -> state -> state |
52 val let_bind_i: (term list * term) list -> state -> state |
52 val let_bind_i: (term list * term) list -> state -> state |
53 val have_thmss: thm list -> string -> context attribute list -> |
|
54 (thm list * context attribute list) list -> state -> state |
|
55 val simple_have_thms: string -> thm list -> state -> state |
53 val simple_have_thms: string -> thm list -> state -> state |
|
54 val have_thmss: ((string * context attribute list) * |
|
55 (thm list * context attribute list) list) list -> state -> state |
|
56 val with_thmss: ((string * context attribute list) * |
|
57 (thm list * context attribute list) list) list -> state -> state |
56 val fix: (string list * string option) list -> state -> state |
58 val fix: (string list * string option) list -> state -> state |
57 val fix_i: (string list * typ option) list -> state -> state |
59 val fix_i: (string list * typ option) list -> state -> state |
58 val assm: (int -> tactic) * (int -> tactic) |
60 val assm: (int -> tactic) * (int -> tactic) |
59 -> (string * context attribute list * (string * (string list * string list)) list) list |
61 -> (string * context attribute list * (string * (string list * string list)) list) list |
60 -> state -> state |
62 -> state -> state |
216 |> map_current (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) |
218 |> map_current (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) |
217 |> (case facts of None => reset_thms thisN | Some ths => put_thms (thisN, ths)); |
219 |> (case facts of None => reset_thms thisN | Some ths => put_thms (thisN, ths)); |
218 |
220 |
219 val reset_facts = put_facts None; |
221 val reset_facts = put_facts None; |
220 |
222 |
221 fun have_facts (name, facts) state = |
223 fun these_factss (state, named_factss) = |
222 state |
224 state |
223 |> put_facts (Some facts) |
225 |> put_thmss named_factss |
224 |> put_thms (name, facts); |
226 |> put_facts (Some (flat (map #2 named_factss))); |
225 |
|
226 fun these_facts (state, ths) = have_facts ths state; |
|
227 |
227 |
228 |
228 |
229 (* goal *) |
229 (* goal *) |
230 |
230 |
231 fun find_goal i (state as State (Node {goal = Some goal, ...}, _)) = (context_of state, (i, goal)) |
231 fun find_goal i (state as State (Node {goal = Some goal, ...}, _)) = (context_of state, (i, goal)) |
266 val enter_backward = put_mode Backward; |
266 val enter_backward = put_mode Backward; |
267 |
267 |
268 fun assert_mode pred state = |
268 fun assert_mode pred state = |
269 let val mode = get_mode state in |
269 let val mode = get_mode state in |
270 if pred mode then state |
270 if pred mode then state |
271 else raise STATE ("Illegal application of proof command in " ^ mode_name mode ^ " mode", state) |
271 else raise STATE ("Illegal application of proof command in " ^ quote (mode_name mode) ^ " mode", state) |
272 end; |
272 end; |
273 |
273 |
274 fun is_chain state = get_mode state = ForwardChain; |
274 fun is_chain state = get_mode state = ForwardChain; |
275 val assert_forward = assert_mode (equal Forward); |
275 val assert_forward = assert_mode (equal Forward); |
276 val assert_forward_or_chain = assert_mode (equal Forward orf equal ForwardChain); |
276 val assert_forward_or_chain = assert_mode (equal Forward orf equal ForwardChain); |
464 val match_bind_i = gen_bind (ProofContext.match_bind_i false); |
464 val match_bind_i = gen_bind (ProofContext.match_bind_i false); |
465 val let_bind = gen_bind (ProofContext.match_bind true); |
465 val let_bind = gen_bind (ProofContext.match_bind true); |
466 val let_bind_i = gen_bind (ProofContext.match_bind_i true); |
466 val let_bind_i = gen_bind (ProofContext.match_bind_i true); |
467 |
467 |
468 |
468 |
469 (* have_thmss *) |
469 (* have_thmss etc. *) |
470 |
470 |
471 fun have_thmss ths name atts ths_atts state = |
471 fun have_thmss args state = |
472 state |
472 state |
473 |> assert_forward |
473 |> assert_forward |
474 |> map_context_result (ProofContext.have_thmss ths name atts ths_atts) |
474 |> map_context_result (ProofContext.have_thmss args) |
475 |> these_facts; |
475 |> these_factss; |
476 |
476 |
477 fun simple_have_thms name thms = have_thmss [] name [] [(thms, [])]; |
477 fun simple_have_thms name thms = have_thmss [((name, []), [(thms, [])])]; |
|
478 |
|
479 fun with_thmss args state = |
|
480 let val state' = state |> have_thmss args |
|
481 in state' |> simple_have_thms "" (the_facts state' @ the_facts state) end; |
478 |
482 |
479 |
483 |
480 (* fix *) |
484 (* fix *) |
481 |
485 |
482 fun gen_fix f xs state = |
486 fun gen_fix f xs state = |
496 fun gen_assume f tac args state = |
500 fun gen_assume f tac args state = |
497 state |
501 state |
498 |> assert_forward |
502 |> assert_forward |
499 |> map_context_result (f tac args) |
503 |> map_context_result (f tac args) |
500 |> (fn (st, (factss, prems)) => |
504 |> (fn (st, (factss, prems)) => |
501 foldl these_facts (st, factss) |
505 these_factss (st, factss) |
502 |> put_thms ("prems", prems) |
506 |> put_thms ("prems", prems)); |
503 |> put_facts (Some (flat (map #2 factss)))); |
|
504 |
507 |
505 val hard_asm_tac = Tactic.etac Drule.triv_goal; |
508 val hard_asm_tac = Tactic.etac Drule.triv_goal; |
506 val soft_asm_tac = Tactic.rtac Drule.triv_goal |
509 val soft_asm_tac = Tactic.rtac Drule.triv_goal |
507 THEN' Tactic.rtac asm_rl; (* FIXME hack to norm goal *) |
510 THEN' Tactic.rtac asm_rl; (* FIXME hack to norm goal *) |
508 |
511 |
639 | _ => err_malformed "finish_local" state); |
642 | _ => err_malformed "finish_local" state); |
640 in |
643 in |
641 print_result {kind = kind_name kind, name = name, thm = result}; |
644 print_result {kind = kind_name kind, name = name, thm = result}; |
642 outer_state |
645 outer_state |
643 |> auto_bind_facts name [ProofContext.generalize goal_ctxt outer_ctxt t] |
646 |> auto_bind_facts name [ProofContext.generalize goal_ctxt outer_ctxt t] |
644 |> have_thmss [] name atts [Thm.no_attributes |
647 |> have_thmss [((name, atts), [Thm.no_attributes |
645 [#1 (ProofContext.export_wrt goal_ctxt (Some outer_ctxt)) result]] |
648 [#1 (ProofContext.export_wrt goal_ctxt (Some outer_ctxt)) result]])] |
646 |> opt_solve |
649 |> opt_solve |
647 |> (Seq.flat o Seq.map after_qed) |
650 |> (Seq.flat o Seq.map after_qed) |
648 end; |
651 end; |
649 |
652 |
650 fun local_qed finalize print state = |
653 fun local_qed finalize print state = |