# HG changeset patch # User wenzelm # Date 1129327688 -7200 # Node ID f1d298e3376023e144dd0d992e0909ad95a8ed17 # Parent bc4db8cfd92f1d899c669af93916c7b8a208c947 goal statements: before_qed argument; diff -r bc4db8cfd92f -r f1d298e33760 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Sat Oct 15 00:08:07 2005 +0200 +++ b/src/Pure/Isar/proof.ML Sat Oct 15 00:08:08 2005 +0200 @@ -87,14 +87,16 @@ val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) -> (theory -> 'a -> context attribute) -> (context * 'b list -> context * (term list list * (context -> context))) -> - string -> (context * thm list -> thm list list -> state -> state Seq.seq) -> + string -> Method.text option -> + (context * thm list -> thm list list -> state -> state Seq.seq) -> ((string * 'a list) * 'b) list -> state -> state val local_qed: Method.text option * bool -> state -> state Seq.seq val global_goal: (context -> (string * string) * (string * thm list) list -> unit) -> (theory -> 'a -> theory attribute) -> (context * 'b list -> context * (term list list * (context -> context))) -> - string -> (context * thm list -> thm list list -> theory -> theory) -> string option -> - string * 'a list -> ((string * 'a list) * 'b) list -> context -> state + string -> Method.text option -> + (context * thm list -> thm list list -> theory -> theory) -> + string option -> string * 'a list -> ((string * 'a list) * 'b) list -> context -> state val global_qed: Method.text option * bool -> state -> theory * context val local_terminal_proof: Method.text * Method.text option -> state -> state Seq.seq val local_default_proof: state -> state Seq.seq @@ -106,23 +108,29 @@ val global_immediate_proof: state -> theory * context val global_done_proof: state -> theory * context val global_skip_proof: bool -> state -> theory * context - val have: (context * thm list -> thm list list -> state -> state Seq.seq) -> + val have: Method.text option -> + (context * thm list -> thm list list -> state -> state Seq.seq) -> ((string * Attrib.src list) * (string * (string list * string list)) list) list -> bool -> state -> state - val have_i: (context * thm list -> thm list list -> state -> state Seq.seq) -> + val have_i: Method.text option -> + (context * thm list -> thm list list -> state -> state Seq.seq) -> ((string * context attribute list) * (term * (term list * term list)) list) list -> bool -> state -> state - val show: (context * thm list -> thm list list -> state -> state Seq.seq) -> + val show: Method.text option -> + (context * thm list -> thm list list -> state -> state Seq.seq) -> ((string * Attrib.src list) * (string * (string list * string list)) list) list -> bool -> state -> state - val show_i: (context * thm list -> thm list list -> state -> state Seq.seq) -> + val show_i: Method.text option -> + (context * thm list -> thm list list -> state -> state Seq.seq) -> ((string * context attribute list) * (term * (term list * term list)) list) list -> bool -> state -> state - val theorem: string -> (context * thm list -> thm list list -> theory -> theory) -> + val theorem: string -> Method.text option -> + (context * thm list -> thm list list -> theory -> theory) -> string option -> string * Attrib.src list -> ((string * Attrib.src list) * (string * (string list * string list)) list) list -> context -> state - val theorem_i: string -> (context * thm list -> thm list list -> theory -> theory) -> + val theorem_i: string -> Method.text option -> + (context * thm list -> thm list list -> theory -> theory) -> string option -> string * theory attribute list -> ((string * theory attribute list) * (term * (term list * term list)) list) list -> context -> state @@ -154,14 +162,16 @@ {statement: string * term list list, (*goal kind and statement*) using: thm list, (*goal facts*) goal: thm, (*subgoals ==> statement*) + before_qed: Method.text option, after_qed: (* FIXME results only *) (context * thm list -> thm list list -> state -> state Seq.seq) * (context * thm list -> thm list list -> theory -> theory)}; exception STATE of string * state; -fun make_goal (statement, using, goal, after_qed) = - Goal {statement = statement, using = using, goal = goal, after_qed = after_qed}; +fun make_goal (statement, using, goal, before_qed, after_qed) = + Goal {statement = statement, using = using, goal = goal, + before_qed = before_qed, after_qed = after_qed}; fun make_node (context, facts, mode, goal) = Node {context = context, facts = facts, mode = mode, goal = goal}; @@ -205,7 +215,7 @@ map_current (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal)); fun map_context_result f state = - f (context_of state) |> swap ||> (fn ctxt => map_context (K ctxt) state); + f (context_of state) ||> (fn ctxt => map_context (K ctxt) state); val warn_extra_tfrees = map_context o ProofContext.warn_extra_tfrees o context_of; val add_binds_i = map_context o ProofContext.add_binds_i; @@ -282,21 +292,23 @@ fun put_goal goal = map_current (fn (ctxt, using, mode, _) => (ctxt, using, mode, goal)); +val before_qed = #before_qed o #2 o current_goal; + (* nested goal *) fun map_goal f g (State (Node {context, facts, mode, goal = SOME goal}, nodes)) = let - val Goal {statement, using, goal, after_qed} = goal; - val goal' = make_goal (g (statement, using, goal, after_qed)); + val Goal {statement, using, goal, before_qed, after_qed} = goal; + val goal' = make_goal (g (statement, using, goal, before_qed, after_qed)); in State (make_node (f context, facts, mode, SOME goal'), nodes) end | map_goal f g (State (nd, node :: nodes)) = let val State (node', nodes') = map_goal f g (State (node, nodes)) in map_context f (State (nd, node' :: nodes')) end | map_goal _ _ state = state; -fun using_facts using = - map_goal I (fn (statement, _, goal, after_qed) => (statement, using, goal, after_qed)); +fun using_facts using = map_goal I (fn (statement, _, goal, before_qed, after_qed) => + (statement, using, goal, before_qed, after_qed)); local fun find i state = @@ -340,7 +352,7 @@ (case filter_out (equal "") strs of [] => "" | strs' => enclose " (" ")" (commas strs')); - fun prt_goal (SOME (ctxt, (i, {statement = (kind, _), using, goal, after_qed = _}))) = + fun prt_goal (SOME (ctxt, (i, {statement = (kind, _), using, goal, before_qed, after_qed}))) = pretty_facts "using " ctxt (if mode <> Backward orelse null using then NONE else SOME using) @ [Pretty.str ("goal" ^ description [kind, levels_up (i div 2), @@ -389,7 +401,7 @@ fun apply_method current_context meth_fun state = let - val (goal_ctxt, (_, {statement, using, goal, after_qed})) = find_goal state; + val (goal_ctxt, (_, {statement, using, goal, before_qed, after_qed})) = find_goal state; val meth = meth_fun (if current_context then context_of state else goal_ctxt); in Method.apply meth using goal |> Seq.map (fn (goal', meth_cases) => @@ -397,7 +409,7 @@ |> check_theory (Thm.theory_of_thm goal') |> map_goal (ProofContext.add_cases (no_goal_cases goal @ goal_cases goal' @ meth_cases)) - (K (statement, using, goal', after_qed))) + (K (statement, using, goal', before_qed, after_qed))) end; fun apply_text cc text state = @@ -431,14 +443,15 @@ else all_tac)); fun refine_goal print_rule inner raw_rule state = - let val (outer, (_, {statement, using, goal, after_qed})) = find_goal state in + let val (outer, (_, {statement, using, goal, before_qed, after_qed})) = find_goal state in raw_rule |> ProofContext.export true inner outer |> Seq.maps (fn rule => (print_rule outer rule; goal |> FINDGOAL (refine_tac rule) - |> Seq.map (fn goal' => map_goal I (K (statement, using, goal', after_qed)) state))) + |> Seq.map (fn goal' => + map_goal I (K (statement, using, goal', before_qed, after_qed)) state))) end; in @@ -506,9 +519,9 @@ local -fun gen_fix fx args = +fun gen_fix fix_ctxt args = assert_forward - #> map_context (fx args) + #> map_context (fix_ctxt args) #> put_facts NONE; in @@ -634,8 +647,8 @@ state |> assert_backward |> map_context_result (note (Attrib.map_facts (prep_atts (theory_of state)) (no_binding args))) - |-> (fn named_facts => map_goal I (fn (statement, using, goal, after_qed) => - (statement, using @ List.concat (map snd named_facts), goal, after_qed))); + |-> (fn named_facts => map_goal I (fn (statement, using, goal, before_qed, after_qed) => + (statement, using @ List.concat (map snd named_facts), goal, before_qed, after_qed))); in @@ -704,7 +717,7 @@ fun proof opt_text = assert_backward - #> refine (if_none opt_text Method.default_text) + #> refine (the_default Method.default_text opt_text) #> Seq.map (using_facts [] #> enter_forward); fun end_proof bot txt = @@ -713,7 +726,8 @@ #> close_block #> assert_current_goal true #> using_facts [] - #> refine (Method.finish_text txt); + #> `before_qed #-> (refine o the_default Method.succeed_text) + #> Seq.maps (refine (Method.finish_text txt)); (* unstructured refinement *) @@ -756,7 +770,7 @@ | vars => warning ("Goal statement contains unbound schematic variable(s): " ^ commas (map (ProofContext.string_of_term (context_of state) o Var) vars))); -fun generic_goal prepp kind after_qed raw_propp state = +fun generic_goal prepp kind before_qed after_qed raw_propp state = let val thy = theory_of state; val chaining = can assert_chain state; @@ -766,7 +780,7 @@ |> assert_forward_or_chain |> enter_forward |> open_block - |> map_context_result (fn ctxt => prepp (ctxt, raw_propp)); + |> map_context_result (fn ctxt => swap (prepp (ctxt, raw_propp))); val props = List.concat propss; val goal = Drule.mk_triv_goal (Thm.cterm_of thy (Logic.mk_conjunction_list props)); @@ -778,7 +792,7 @@ goal_state |> tap (check_tvars props) |> tap (check_vars props) - |> put_goal (SOME (make_goal ((kind, propss), [], goal, after_qed'))) + |> put_goal (SOME (make_goal ((kind, propss), [], goal, before_qed, after_qed'))) |> map_context (ProofContext.add_cases (AutoBind.cases thy props)) |> map_context (ProofContext.auto_bind_goal props) |> K chaining ? (`the_facts #-> using_facts) @@ -791,7 +805,8 @@ fun generic_qed state = let - val (goal_ctxt, {statement = (_, stmt), using, goal, after_qed}) = current_goal state; + val (goal_ctxt, {statement = (_, stmt), using, goal, before_qed = _, after_qed}) = + current_goal state; val outer_state = state |> close_block; val outer_ctxt = context_of outer_state; @@ -810,7 +825,7 @@ (* local goals *) -fun local_goal print_results prep_att prepp kind after_qed stmt state = +fun local_goal print_results prep_att prepp kind before_qed after_qed stmt state = let val ((names, attss), propp) = prep_names (prep_att (theory_of state)) stmt; @@ -820,7 +835,7 @@ #> after_qed raw_results results; in state - |> generic_goal prepp (kind ^ goal_names NONE "" names) (after_qed', K (K I)) propp + |> generic_goal prepp (kind ^ goal_names NONE "" names) before_qed (after_qed', K (K I)) propp |> warn_extra_tfrees state end; @@ -834,7 +849,7 @@ (* global goals *) fun global_goal print_results prep_att prepp - kind after_qed target (name, raw_atts) stmt ctxt = + kind before_qed after_qed target (name, raw_atts) stmt ctxt = let val thy = ProofContext.theory_of ctxt; val thy_ctxt = ProofContext.init thy; @@ -859,7 +874,7 @@ in init ctxt |> generic_goal (prepp #> ProofContext.auto_fix) (kind ^ goal_names target name names) - (K (K Seq.single), after_qed') propp + before_qed (K (K Seq.single), after_qed') propp end; fun check_result msg state sq = @@ -911,10 +926,10 @@ local -fun gen_have prep_att prepp after_qed stmt int = - local_goal (ProofDisplay.print_results int) prep_att prepp "have" after_qed stmt; +fun gen_have prep_att prepp before_qed after_qed stmt int = + local_goal (ProofDisplay.print_results int) prep_att prepp "have" before_qed after_qed stmt; -fun gen_show prep_att prepp after_qed stmt int state = +fun gen_show prep_att prepp before_qed after_qed stmt int state = let val testing = ref false; val rule = ref (NONE: thm option); @@ -941,7 +956,7 @@ #> Seq.maps (after_qed raw_results results); in state - |> local_goal print_results prep_att prepp "show" after_qed' stmt + |> local_goal print_results prep_att prepp "show" before_qed after_qed' stmt |> K int ? (fn goal_state => (case test_proof goal_state of Result (SOME _) => goal_state @@ -950,8 +965,8 @@ | Exn exn => raise EXCEPTION (exn, fail_msg (context_of goal_state)))) end; -fun gen_theorem prep_att prepp kind after_qed target a = - global_goal ProofDisplay.present_results prep_att prepp kind after_qed target a; +fun gen_theorem prep_att prepp kind before_qed after_qed target a = + global_goal ProofDisplay.present_results prep_att prepp kind before_qed after_qed target a; in