# HG changeset patch # User wenzelm # Date 933883733 -7200 # Node ID a329a37ed91aef4e97e2f78bf4c1f18b18ab68ca # Parent 8263d0b50e120c07712cd855868037d8c8164f05 local goals: after_qed; diff -r 8263d0b50e12 -r a329a37ed91a src/Pure/Isar/isar_thy.ML --- a/src/Pure/Isar/isar_thy.ML Wed Aug 04 18:20:24 1999 +0200 +++ b/src/Pure/Isar/isar_thy.ML Thu Aug 05 22:08:53 1999 +0200 @@ -295,14 +295,14 @@ val presume_i = local_statement_i Proof.presume_i I o Comment.ignore; val local_def = local_statement LocalDefs.def I o Comment.ignore; val local_def_i = local_statement LocalDefs.def_i I o Comment.ignore; -val show = local_statement Proof.show I o Comment.ignore; -val show_i = local_statement_i Proof.show_i I o Comment.ignore; -val have = local_statement Proof.have I o Comment.ignore; -val have_i = local_statement_i Proof.have_i I o Comment.ignore; -val thus = local_statement Proof.show Proof.chain o Comment.ignore; -val thus_i = local_statement_i Proof.show_i Proof.chain o Comment.ignore; -val hence = local_statement Proof.have Proof.chain o Comment.ignore; -val hence_i = local_statement_i Proof.have_i Proof.chain o Comment.ignore; +val show = local_statement (Proof.show Seq.single) I o Comment.ignore; +val show_i = local_statement_i (Proof.show_i Seq.single) I o Comment.ignore; +val have = local_statement (Proof.have Seq.single) I o Comment.ignore; +val have_i = local_statement_i (Proof.have_i Seq.single) I o Comment.ignore; +val thus = local_statement (Proof.show Seq.single) Proof.chain o Comment.ignore; +val thus_i = local_statement_i (Proof.show_i Seq.single) Proof.chain o Comment.ignore; +val hence = local_statement (Proof.have Seq.single) Proof.chain o Comment.ignore; +val hence_i = local_statement_i (Proof.have_i Seq.single) Proof.chain o Comment.ignore; (* blocks *) diff -r 8263d0b50e12 -r a329a37ed91a src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Wed Aug 04 18:20:24 1999 +0200 +++ b/src/Pure/Isar/proof.ML Thu Aug 05 22:08:53 1999 +0200 @@ -17,6 +17,7 @@ val sign_of: state -> Sign.sg val the_facts: state -> thm list val the_fact: state -> thm + val get_goal: state -> thm list * thm val goal_facts: (state -> thm list) -> state -> state val use_facts: state -> state val reset_facts: state -> state @@ -64,14 +65,14 @@ val chain: state -> state val export_chain: state -> state Seq.seq val from_facts: thm list -> state -> state - val show: string -> context attribute list -> string * (string list * string list) - -> state -> state - val show_i: string -> context attribute list -> term * (term list * term list) - -> state -> state - val have: string -> context attribute list -> string * (string list * string list) - -> state -> state - val have_i: string -> context attribute list -> term * (term list * term list) - -> state -> state + val show: (state -> state Seq.seq) -> string -> context attribute list + -> string * (string list * string list) -> state -> state + val show_i: (state -> state Seq.seq) -> string -> context attribute list + -> term * (term list * term list) -> state -> state + val have: (state -> state Seq.seq) -> string -> context attribute list + -> string * (string list * string list) -> state -> state + val have_i: (state -> state Seq.seq) -> string -> context attribute list + -> term * (term list * term list) -> state -> state val at_bottom: state -> bool val local_qed: (state -> state Seq.seq) -> ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit) -> state -> state Seq.seq @@ -125,25 +126,23 @@ (fn Forward => "state" | ForwardChain => "chain" | Backward => "prove"); -(* type node *) - -type node = - {context: context, - facts: thm list option, - mode: mode, - goal: goal option}; - -fun make_node (context, facts, mode, goal) = - {context = context, facts = facts, mode = mode, goal = goal}: node; - - (* datatype state *) -datatype state = +datatype node = + Node of + {context: context, + facts: thm list option, + mode: mode, + goal: (goal * (state -> state Seq.seq)) option} +and state = State of node * (*current*) node list; (*parents wrt. block structure*) +fun make_node (context, facts, mode, goal) = + Node {context = context, facts = facts, mode = mode, goal = goal}; + + exception STATE of string * state; fun err_malformed name state = @@ -155,7 +154,7 @@ | Some s_sq => Seq.cons s_sq); -fun map_current f (State ({context, facts, mode, goal}, nodes)) = +fun map_current f (State (Node {context, facts, mode, goal}, nodes)) = State (make_node (f (context, facts, mode, goal)), nodes); fun init_state thy = @@ -167,13 +166,13 @@ (* context *) -fun context_of (State ({context, ...}, _)) = context; +fun context_of (State (Node {context, ...}, _)) = context; val theory_of = ProofContext.theory_of o context_of; val sign_of = ProofContext.sign_of o context_of; fun map_context f = map_current (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal)); -fun map_context_result f (state as State ({context, facts, mode, goal}, nodes)) = +fun map_context_result f (state as State (Node {context, facts, mode, goal}, nodes)) = let val (context', result) = f context in (State (make_node (context', facts, mode, goal), nodes), result) end; @@ -190,7 +189,7 @@ (* facts *) -fun the_facts (State ({facts = Some facts, ...}, _)) = facts +fun the_facts (State (Node {facts = Some facts, ...}, _)) = facts | the_facts state = raise STATE ("No current facts available", state); fun the_fact state = @@ -199,7 +198,7 @@ | _ => raise STATE ("Single fact expected", state)); fun assert_facts state = (the_facts state; state); -fun get_facts (State ({facts, ...}, _)) = facts; +fun get_facts (State (Node {facts, ...}, _)) = facts; fun put_facts facts state = state @@ -218,14 +217,18 @@ (* goal *) -fun find_goal i (state as State ({goal = Some goal, ...}, _)) = (context_of state, (i, goal)) - | find_goal i (State ({goal = None, ...}, node :: nodes)) = +fun find_goal i (state as State (Node {goal = Some goal, ...}, _)) = (context_of state, (i, goal)) + | find_goal i (State (Node {goal = None, ...}, node :: nodes)) = find_goal (i + 1) (State (node, nodes)) | find_goal _ (state as State (_, [])) = err_malformed "find_goal" state; +fun get_goal state = + let val (_, (_, ((_, goal), _))) = find_goal 0 state + in goal end; + fun put_goal goal = map_current (fn (ctxt, facts, mode, _) => (ctxt, facts, mode, goal)); -fun map_goal f (State ({context, facts, mode, goal = Some goal}, nodes)) = +fun map_goal f (State (Node {context, facts, mode, goal = Some goal}, nodes)) = State (make_node (context, facts, mode, Some (f goal)), nodes) | map_goal f (State (nd, node :: nodes)) = let val State (node', nodes') = map_goal f (State (node, nodes)) @@ -234,7 +237,7 @@ fun goal_facts get state = state - |> map_goal (fn (result, (_, thm)) => (result, (get state, thm))); + |> map_goal (fn ((result, (_, thm)), f) => ((result, (get state, thm)), f)); fun use_facts state = state @@ -244,7 +247,7 @@ (* mode *) -fun get_mode (State ({mode, ...}, _)) = mode; +fun get_mode (State (Node {mode, ...}, _)) = mode; fun put_mode mode = map_current (fn (ctxt, facts, _, goal) => (ctxt, facts, mode, goal)); val enter_forward = put_mode Forward; @@ -292,7 +295,7 @@ | print_facts s (Some ths) = Pretty.writeln (Pretty.big_list (s ^ " facts:") (map pretty_thm ths)); -fun print_state (state as State ({context, facts, mode, goal = _}, nodes)) = +fun print_state (state as State (Node {context, facts, mode, goal = _}, nodes)) = let val ref (_, _, begin_goal) = Goals.current_goals_markers; @@ -300,7 +303,7 @@ | levels_up 1 = " (1 level up)" | levels_up i = " (" ^ string_of_int i ^ " levels up)"; - fun print_goal (_, (i, ((kind, name, _), (goal_facts, thm)))) = + fun print_goal (_, (i, (((kind, name, _), (goal_facts, thm)), _))) = (print_facts "Using" (if null goal_facts then None else Some goal_facts); writeln (kind_name kind ^ " " ^ quote name ^ levels_up (i div 2) ^ ":"); Locale.print_goals_marker begin_goal (! goals_limit) thm); @@ -335,15 +338,15 @@ if Sign.subsig (sg, sign_of state) then state else raise STATE ("Bad signature of result: " ^ Sign.str_of_sg sg, state); -fun refine meth_fun (state as State ({context, ...}, _)) = +fun refine meth_fun state = let - val Method meth = meth_fun context; - val (_, (_, (result, (facts, thm)))) = find_goal 0 state; + val Method meth = meth_fun (context_of state); + val (_, (_, ((result, (facts, thm)), f))) = find_goal 0 state; fun refn thm' = state |> check_sign (Thm.sign_of_thm thm') - |> map_goal (K (result, (facts, thm'))); + |> map_goal (K ((result, (facts, thm')), f)); in Seq.map refn (meth facts thm) end; @@ -403,12 +406,12 @@ fun export_goal print_rule raw_rule inner state = let - val (outer, (_, (result, (facts, thm)))) = find_goal 0 state; + val (outer, (_, ((result, (facts, thm)), f))) = find_goal 0 state; val (exp, tacs) = export_wrt inner (Some outer); val rule = exp raw_rule; val _ = print_rule rule; val thmq = FIRSTGOAL (Tactic.rtac rule THEN' RANGE (map #1 tacs)) thm; - in Seq.map (fn th => map_goal (K (result, (facts, th))) state) thmq end; + in Seq.map (fn th => map_goal (K ((result, (facts, th)), f)) state) thmq end; fun export_thm inner thm = @@ -573,7 +576,7 @@ (* setup goals *) -fun setup_goal opt_block prepp kind name atts raw_propp state = +fun setup_goal opt_block prepp kind after_qed name atts raw_propp state = let val (state', prop) = state @@ -589,7 +592,7 @@ val goal = foldr cut_asm (casms, Drule.mk_triv_goal cprop); in state' - |> put_goal (Some ((kind atts, (PureThy.default_name name), prop), ([], goal))) + |> put_goal (Some (((kind atts, (PureThy.default_name name), prop), ([], goal)), after_qed)) |> auto_bind_goal prop |> (if is_chain state then use_facts else reset_facts) |> new_block @@ -599,7 +602,7 @@ (*global goals*) fun global_goal prep kind name atts x thy = - setup_goal I prep kind name atts x (init_state thy); + setup_goal I prep kind Seq.single name atts x (init_state thy); val theorem = global_goal ProofContext.bind_propp Theorem; val theorem_i = global_goal ProofContext.bind_propp_i Theorem; @@ -608,8 +611,8 @@ (*local goals*) -fun local_goal prep kind name atts x = - setup_goal open_block prep kind name atts x; +fun local_goal prep kind f name atts x = + setup_goal open_block prep kind f name atts x; val show = local_goal ProofContext.bind_propp Goal; val show_i = local_goal ProofContext.bind_propp_i Goal; @@ -622,12 +625,12 @@ (* current goal *) -fun current_goal (State ({context, goal = Some goal, ...}, _)) = (context, goal) +fun current_goal (State (Node {context, goal = Some goal, ...}, _)) = (context, goal) | current_goal state = raise STATE ("No current goal!", state); -fun assert_current_goal true (state as State ({goal = None, ...}, _)) = +fun assert_current_goal true (state as State (Node {goal = None, ...}, _)) = raise STATE ("No goal in this block!", state) - | assert_current_goal false (state as State ({goal = Some _, ...}, _)) = + | assert_current_goal false (state as State (Node {goal = Some _, ...}, _)) = raise STATE ("Goal present in this block!", state) | assert_current_goal _ state = state; @@ -652,7 +655,7 @@ fun finish_local (print_result, print_rule) state = let - val (ctxt, ((kind, name, t), (_, raw_thm))) = current_goal state; + val (ctxt, (((kind, name, t), (_, raw_thm)), after_qed)) = current_goal state; val result = prep_result state t raw_thm; val (atts, opt_solve) = (case kind of @@ -666,6 +669,7 @@ |> auto_bind_facts name [t] |> have_thmss [] name atts [Thm.no_attributes [result]] |> opt_solve + |> (Seq.flat o Seq.map after_qed) end; fun local_qed finalize print state = @@ -679,7 +683,7 @@ fun finish_global state = let - val (_, ((kind, name, t), (_, raw_thm))) = current_goal state; + val (_, (((kind, name, t), (_, raw_thm)), _)) = current_goal state; (*ignores after_qed!*) val result = final_result state (prep_result state t raw_thm); val atts =