# HG changeset patch # User wenzelm # Date 959188190 -7200 # Node ID 916966f689076d3a8514a55fd9741d4b5cc06b5a # Parent d46b36785c70d41a4f23f7df8e58ed8947115132 added "done" proof; diff -r d46b36785c70 -r 916966f68907 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Wed May 24 19:09:36 2000 +0200 +++ b/src/Pure/Isar/isar_syn.ML Wed May 24 19:09:50 2000 +0200 @@ -371,13 +371,17 @@ (P.method -- P.interest -- Scan.option (P.method -- P.interest) -- P.marg_comment >> IsarThy.terminal_proof); +val default_proofP = + OuterSyntax.command ".." "default proof" K.qed + (P.marg_comment >> IsarThy.default_proof); + val immediate_proofP = OuterSyntax.command "." "immediate proof" K.qed (P.marg_comment >> IsarThy.immediate_proof); -val default_proofP = - OuterSyntax.command ".." "default proof" K.qed - (P.marg_comment >> IsarThy.default_proof); +val done_proofP = + OuterSyntax.command "done" "done proof" K.qed + (P.marg_comment >> IsarThy.done_proof); val skip_proofP = OuterSyntax.improper_command "sorry" "skip proof (quick-and-dirty mode only!)" K.qed @@ -648,9 +652,9 @@ (*proof commands*) theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, presumeP, defP, fixP, letP, caseP, thenP, fromP, withP, noteP, beginP, endP, - nextP, qedP, terminal_proofP, immediate_proofP, default_proofP, - skip_proofP, forget_proofP, deferP, preferP, applyP, apply_endP, - proofP, alsoP, finallyP, moreoverP, ultimatelyP, backP, + nextP, qedP, terminal_proofP, default_proofP, immediate_proofP, + done_proofP, skip_proofP, forget_proofP, deferP, preferP, applyP, + apply_endP, proofP, alsoP, finallyP, moreoverP, ultimatelyP, backP, cannot_undoP, clear_undosP, redoP, undos_proofP, undoP, killP, (*diagnostic commands*) pretty_setmarginP, print_commandsP, print_contextP, print_theoryP, diff -r d46b36785c70 -r 916966f68907 src/Pure/Isar/isar_thy.ML --- a/src/Pure/Isar/isar_thy.ML Wed May 24 19:09:36 2000 +0200 +++ b/src/Pure/Isar/isar_thy.ML Wed May 24 19:09:50 2000 +0200 @@ -135,8 +135,9 @@ -> Toplevel.transition -> Toplevel.transition val terminal_proof: ((Method.text * Comment.interest) * (Method.text * Comment.interest) option) * Comment.text -> Toplevel.transition -> Toplevel.transition + val default_proof: Comment.text -> Toplevel.transition -> Toplevel.transition val immediate_proof: Comment.text -> Toplevel.transition -> Toplevel.transition - val default_proof: Comment.text -> Toplevel.transition -> Toplevel.transition + val done_proof: Comment.text -> Toplevel.transition -> Toplevel.transition val skip_proof: Comment.text -> Toplevel.transition -> Toplevel.transition val forget_proof: Comment.text -> Toplevel.transition -> Toplevel.transition val get_thmss: (string * Args.src list) list -> Proof.state -> thm list @@ -438,16 +439,17 @@ (* local endings *) val local_qed = - proof'' o (ProofHistory.applys oo Method.local_qed) o apsome Comment.ignore_interest; + proof'' o (ProofHistory.applys oo Method.local_qed true) o apsome Comment.ignore_interest; fun ignore_interests (x, y) = (Comment.ignore_interest x, apsome Comment.ignore_interest y); val local_terminal_proof = proof'' o (ProofHistory.applys oo Method.local_terminal_proof) o ignore_interests; +val local_default_proof = proof'' (ProofHistory.applys o Method.local_default_proof); val local_immediate_proof = proof'' (ProofHistory.applys o Method.local_immediate_proof); -val local_default_proof = proof'' (ProofHistory.applys o Method.local_default_proof); val local_skip_proof = proof'' (ProofHistory.applys o SkipProof.local_skip_proof); +val local_done_proof = proof'' (ProofHistory.applys o Method.local_done_proof); (* global endings *) @@ -459,19 +461,21 @@ val (thy, res as {kind, name, thm}) = finish state; in print_result res; Context.setmp (Some thy) (Present.result kind name) thm; thy end); -val global_qed = global_result o Method.global_qed o apsome Comment.ignore_interest; +val global_qed = global_result o Method.global_qed true o apsome Comment.ignore_interest; val global_terminal_proof = global_result o Method.global_terminal_proof o ignore_interests; +val global_default_proof = global_result Method.global_default_proof; val global_immediate_proof = global_result Method.global_immediate_proof; -val global_default_proof = global_result Method.global_default_proof; val global_skip_proof = global_result SkipProof.global_skip_proof; +val global_done_proof = global_result Method.global_done_proof; (* common endings *) fun qed (meth, comment) = local_qed meth o global_qed meth; fun terminal_proof (meths, comment) = local_terminal_proof meths o global_terminal_proof meths; +fun default_proof comment = local_default_proof o global_default_proof; fun immediate_proof comment = local_immediate_proof o global_immediate_proof; -fun default_proof comment = local_default_proof o global_default_proof; +fun done_proof comment = local_done_proof o global_done_proof; fun skip_proof comment = local_skip_proof o global_skip_proof; fun forget_proof comment = Toplevel.proof_to_theory (Proof.theory_of o ProofHistory.current); diff -r d46b36785c70 -r 916966f68907 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Wed May 24 19:09:36 2000 +0200 +++ b/src/Pure/Isar/method.ML Wed May 24 19:09:50 2000 +0200 @@ -86,21 +86,25 @@ val refine: text -> Proof.state -> Proof.state Seq.seq val refine_end: text -> Proof.state -> Proof.state Seq.seq val proof: text option -> Proof.state -> Proof.state Seq.seq - val local_qed: text option + val local_qed: bool -> text option -> ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit) -> Proof.state -> Proof.state Seq.seq val local_terminal_proof: text * text option -> ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit) -> Proof.state -> Proof.state Seq.seq - val local_immediate_proof: ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit) - -> Proof.state -> Proof.state Seq.seq val local_default_proof: ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit) -> Proof.state -> Proof.state Seq.seq - val global_qed: text option -> Proof.state -> theory * {kind: string, name: string, thm: thm} + val local_immediate_proof: ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit) + -> Proof.state -> Proof.state Seq.seq + val local_done_proof: ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit) + -> Proof.state -> Proof.state Seq.seq + val global_qed: bool -> text option + -> Proof.state -> theory * {kind: string, name: string, thm: thm} val global_terminal_proof: text * text option -> Proof.state -> theory * {kind: string, name: string, thm: thm} + val global_default_proof: Proof.state -> theory * {kind: string, name: string, thm: thm} val global_immediate_proof: Proof.state -> theory * {kind: string, name: string, thm: thm} - val global_default_proof: Proof.state -> theory * {kind: string, name: string, thm: thm} + val global_done_proof: Proof.state -> theory * {kind: string, name: string, thm: thm} val setup: (theory -> theory) list end; @@ -202,7 +206,7 @@ val METHOD = Proof.method; val METHOD_CASES = Proof.method_cases; -fun METHOD0 tac = METHOD (fn [] => tac | _ => error "Method may not be used with facts"); +fun METHOD0 tac = METHOD (fn [] => tac | _ => error "Cannot handle current facts"); (* primitive *) @@ -536,11 +540,13 @@ val default_text = Source (Args.src (("default", []), Position.none)); val this_text = Basic (K this); - -fun finish ctxt = METHOD (K (FILTER Thm.no_prems (ALLGOALS (assm_tac ctxt) THEN flexflex_tac))); +val done_text = Basic (K (METHOD0 all_tac)); -fun finish_text None = Basic finish - | finish_text (Some txt) = Then [txt, Basic finish]; +fun close_text asm = Basic (fn ctxt => METHOD (K + (FILTER Thm.no_prems ((if asm then ALLGOALS (assm_tac ctxt) else all_tac) THEN flexflex_tac)))); + +fun finish_text asm None = close_text asm + | finish_text asm (Some txt) = Then [txt, close_text asm]; fun proof opt_text state = state @@ -549,31 +555,34 @@ |> Seq.map (Proof.goal_facts (K [])) |> Seq.map Proof.enter_forward; -fun local_qed opt_text = Proof.local_qed (refine (finish_text opt_text)); -fun local_terminal_proof (text, opt_text) pr = Seq.THEN (proof (Some text), local_qed opt_text pr); +fun local_qed asm opt_text = Proof.local_qed (refine (finish_text asm opt_text)); +fun local_terminal_proof (text, opt_text) pr = + Seq.THEN (proof (Some text), local_qed true opt_text pr); +val local_default_proof = local_terminal_proof (default_text, None); val local_immediate_proof = local_terminal_proof (this_text, None); -val local_default_proof = local_terminal_proof (default_text, None); +fun local_done_proof pr = Seq.THEN (proof (Some done_text), local_qed false None pr); -fun global_qeds opt_text = Proof.global_qed (refine (finish_text opt_text)); +fun global_qeds asm opt_text = Proof.global_qed (refine (finish_text asm opt_text)); -fun global_qed opt_text state = +fun global_qed asm opt_text state = state - |> global_qeds opt_text + |> global_qeds asm opt_text |> Proof.check_result "Failed to finish proof" state |> Seq.hd; -fun global_terminal_proof (text, opt_text) state = +fun global_term_proof asm (text, opt_text) state = state |> proof (Some text) |> Proof.check_result "Terminal proof method failed" state - |> (Seq.flat o Seq.map (global_qeds opt_text)) + |> (Seq.flat o Seq.map (global_qeds asm opt_text)) |> Proof.check_result "Failed to finish proof (after successful terminal method)" state |> Seq.hd; -val global_immediate_proof = global_terminal_proof (this_text, None); +val global_terminal_proof = global_term_proof true; val global_default_proof = global_terminal_proof (default_text, None); - +val global_immediate_proof = global_terminal_proof (this_text, None); +val global_done_proof = global_term_proof false (done_text, None); (** theory setup **)