# HG changeset patch # User wenzelm # Date 1014843234 -3600 # Node ID 92195e8c6208ea8a5c0ba8fff5f6ff21091b74d4 # Parent c9b1838a2cc0566a9e48fcb0506e32d61cefa984 tuned feedback of goal forms; diff -r c9b1838a2cc0 -r 92195e8c6208 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Wed Feb 27 21:53:33 2002 +0100 +++ b/src/Pure/Isar/proof.ML Wed Feb 27 21:53:54 2002 +0100 @@ -95,16 +95,16 @@ -> theory -> state val chain: state -> state val from_facts: thm list -> state -> state - val show: (bool -> state -> state) -> (state -> state Seq.seq) + val show: (bool -> state -> state) -> (state -> state Seq.seq) -> bool -> ((string * context attribute list) * (string * (string list * string list)) list) list -> bool -> state -> state - val show_i: (bool -> state -> state) -> (state -> state Seq.seq) + val show_i: (bool -> state -> state) -> (state -> state Seq.seq) -> bool -> ((string * context attribute list) * (term * (term list * term list)) list) list -> bool -> state -> state - val have: (state -> state Seq.seq) + val have: (state -> state Seq.seq) -> bool -> ((string * context attribute list) * (string * (string list * string list)) list) list -> state -> state - val have_i: (state -> state Seq.seq) + val have_i: (state -> state Seq.seq) -> bool -> ((string * context attribute list) * (term * (term list * term list)) list) list -> state -> state val at_bottom: state -> bool @@ -170,7 +170,7 @@ {context: context, facts: thm list option, mode: mode, - goal: (goal * (state -> state Seq.seq)) option} + goal: (goal * ((state -> state Seq.seq) * bool)) option} and state = State of node * (*current*) @@ -402,13 +402,13 @@ fun gen_refine current_context meth_fun state = let - val (goal_ctxt, (_, ((result, (facts, thm)), f))) = find_goal state; + val (goal_ctxt, (_, ((result, (facts, thm)), x))) = find_goal state; val Method meth = meth_fun (if current_context then context_of state else goal_ctxt); fun refn (thm', cases) = state |> check_sign (Thm.sign_of_thm thm') - |> map_goal (ProofContext.add_cases cases) (K ((result, (facts, thm')), f)); + |> map_goal (ProofContext.add_cases cases) (K ((result, (facts, thm')), x)); in Seq.map refn (meth facts thm) end; in @@ -438,13 +438,13 @@ fun export_goal inner print_rule raw_rule state = let - val (outer, (_, ((result, (facts, thm)), f))) = find_goal state; + val (outer, (_, ((result, (facts, thm)), x))) = find_goal state; val exp_tac = ProofContext.export true inner outer; fun exp_rule rule = let val _ = print_rule outer rule; val thmq = FINDGOAL (refine_tac rule) thm; - in Seq.map (fn th => map_goal I (K ((result, (facts, th)), f)) state) thmq end; + in Seq.map (fn th => map_goal I (K ((result, (facts, th)), x)) state) thmq end; in raw_rule |> exp_tac |> (Seq.flat o Seq.map exp_rule) end; fun export_goals inner print_rule raw_rules = @@ -555,8 +555,8 @@ |> assert_backward |> map_context_result (f (map (pair ("", [])) args)) |> (fn (st, named_facts) => - let val (_, (_, ((result, (facts, thm)), f))) = find_goal st; - in st |> map_goal I (K ((result, (facts @ flat (map snd named_facts), thm)), f)) end); + let val (_, (_, ((result, (facts, thm)), x))) = find_goal st; + in st |> map_goal I (K ((result, (facts @ flat (map snd named_facts), thm)), x)) end); in @@ -655,7 +655,7 @@ val rule_contextN = "rule_context"; -fun setup_goal opt_block prepp autofix kind after_qed names raw_propp state = +fun setup_goal opt_block prepp autofix kind after_qed pr names raw_propp state = let val (state', (propss, gen_binds)) = state @@ -680,7 +680,8 @@ commas (map (ProofContext.string_of_term (context_of state')) vars)); state' |> map_context (autofix props) - |> put_goal (Some (((kind, names, propss), ([], goal)), after_qed o map_context gen_binds)) + |> put_goal (Some (((kind, names, propss), ([], goal)), + (after_qed o map_context gen_binds, pr))) |> map_context (ProofContext.add_cases (if length props = 1 then RuleCases.make true (Thm.sign_of_thm goal, Thm.prop_of goal) [rule_contextN] @@ -706,7 +707,7 @@ |> map_context (K elems_ctxt) |> setup_goal I ProofContext.bind_propp_schematic_i ProofContext.fix_frees (Theorem {kind = kind, theory_spec = (a, map (snd o fst) concl), locale_spec = locale_spec}) - Seq.single (map (fst o fst) concl) propp + Seq.single true (map (fst o fst) concl) propp end; val multi_theorem = global_goal Locale.read_context_statement; @@ -714,14 +715,14 @@ (*local goals*) -fun local_goal' prepp kind (check: bool -> state -> state) f args int state = +fun local_goal' prepp kind (check: bool -> state -> state) f pr args int state = state |> setup_goal open_block prepp (K I) (kind (map (snd o fst) args)) - f (map (fst o fst) args) (map snd args) + f pr (map (fst o fst) args) (map snd args) |> warn_extra_tfrees state |> check int; -fun local_goal prepp kind f args = local_goal' prepp kind (K I) f args false; +fun local_goal prepp kind f pr args = local_goal' prepp kind (K I) f pr args false; val show = local_goal' ProofContext.bind_propp Show; val show_i = local_goal' ProofContext.bind_propp_i Show; @@ -765,7 +766,7 @@ fun finish_local (print_result, print_rule) state = let - val (goal_ctxt, (((kind, names, tss), (_, raw_thm)), after_qed)) = current_goal state; + val (goal_ctxt, (((kind, names, tss), (_, raw_thm)), (after_qed, pr))) = current_goal state; val outer_state = state |> close_block; val outer_ctxt = context_of outer_state; @@ -777,11 +778,13 @@ val (attss, opt_solve) = (case kind of - Show attss => (attss, export_goals goal_ctxt print_rule results) + Show attss => (attss, + export_goals goal_ctxt (if pr then print_rule else (K (K ()))) results) | Have attss => (attss, Seq.single) | _ => err_malformed "finish_local" state); in - print_result goal_ctxt (kind_name (sign_of state) kind, names ~~ Library.unflat tss results); + conditional pr (fn () => print_result goal_ctxt + (kind_name (sign_of state) kind, names ~~ Library.unflat tss results)); outer_state |> auto_bind_facts (ProofContext.generalize goal_ctxt outer_ctxt ts) |> (fn st => Seq.map (fn res =>