# HG changeset patch
# User wenzelm
# Date 921839040 -3600
# Node ID 2daaf2943c7916fde11f025c46dc2f6f319a1778
# Parent  86e9d24f4238b3db869d7e7e9d6d1274f7b15c38
common qed and end of proofs;

diff -r 86e9d24f4238 -r 2daaf2943c79 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Mar 18 16:44:53 1999 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Fri Mar 19 11:24:00 1999 +0100
@@ -33,7 +33,7 @@
 
 (*end current theory / sub-proof / excursion*)
 val endP =
-  OuterSyntax.command "end" "end current theory / sub-proof / excursion"
+  OuterSyntax.command "end" "end current block / theory / excursion"
     (Scan.succeed (Toplevel.print o Toplevel.exit o Toplevel.proof IsarThy.end_block));
 
 val contextP =
@@ -308,42 +308,45 @@
 
 (* end proof *)
 
-val qedP =
-  OuterSyntax.command "qed" "conclude proof"
-    (Scan.succeed (Toplevel.proof_to_theory IsarThy.qed));
+val kill_proofP =
+  OuterSyntax.improper_command "kill" "abort current proof"
+    (Scan.succeed (Toplevel.print o Toplevel.proof_to_theory IsarThy.kill_proof));
 
 val qed_withP =
   OuterSyntax.improper_command "qed_with" "conclude proof, may patch name and attributes"
-    (Scan.option name -- Scan.option attribs >> (Toplevel.proof_to_theory o IsarThy.qed_with));
+    (Scan.option name -- Scan.option attribs -- Scan.option method
+      >> (uncurry IsarThy.global_qed_with));
+
+val qedP =
+  OuterSyntax.command "qed" "conclude (sub-)proof"
+    (Scan.option method >> IsarThy.qed);
 
-val kill_proofP =
-  OuterSyntax.improper_command "kill" "abort current proof"
-    (Scan.succeed (Toplevel.print o Toplevel.proof_to_theory IsarThy.kill_proof));
+val terminal_proofP =
+  OuterSyntax.command "by" "terminal backward proof"
+    (method >> (Toplevel.print oo IsarThy.terminal_proof));
+
+val immediate_proofP =
+  OuterSyntax.command "." "immediate proof"
+    (Scan.succeed (Toplevel.print o IsarThy.immediate_proof));
+
+val default_proofP =
+  OuterSyntax.command ".." "default proof"
+    (Scan.succeed (Toplevel.print o IsarThy.default_proof));
 
 
 (* proof steps *)
 
-fun gen_stepP meth int name cmt f =
-  OuterSyntax.parser int name cmt
-    (meth >> (fn txt => Toplevel.print o Toplevel.proof (f txt)));
-
-val stepP = gen_stepP method;
-
-val refineP = stepP true "refine" "unstructured backward proof step, ignoring facts" IsarThy.tac;
-val then_refineP =
-  stepP true "then_refine" "unstructured backward proof step, using facts" IsarThy.then_tac;
-
+val refineP =
+  OuterSyntax.improper_command "refine" "unstructured backward proof step, ignoring facts"
+    (method >> (Toplevel.print oo (Toplevel.proof o IsarThy.tac)));
 
-val proofP = gen_stepP (Scan.option method) false "proof" "backward proof" IsarThy.proof;
-val terminal_proofP = stepP false "by" "terminal backward proof" IsarThy.terminal_proof;
+val then_refineP =
+  OuterSyntax.improper_command "then_refine" "unstructured backward proof step, using facts"
+    (method >> (Toplevel.print oo (Toplevel.proof o IsarThy.then_tac)));
 
-val immediate_proofP =
-  OuterSyntax.command "." "immediate proof"
-    (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.immediate_proof));
-
-val default_proofP =
-  OuterSyntax.command ".." "default proof"
-    (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.default_proof));
+val proofP =
+  OuterSyntax.command "proof" "backward proof"
+    (Scan.option method >> (Toplevel.print oo (Toplevel.proof o IsarThy.proof)));
 
 
 (* proof history *)
@@ -507,10 +510,10 @@
   print_ast_translationP, token_translationP, oracleP,
   (*proof commands*)
   theoremP, lemmaP, showP, haveP, assumeP, fixP, letP, thenP, fromP,
-  factsP, beginP, nextP, qedP, qed_withP, kill_proofP, refineP,
-  then_refineP, proofP, terminal_proofP, immediate_proofP,
-  default_proofP, clear_undoP, undoP, redoP, undosP, redosP, backP,
-  prevP, upP, topP,
+  factsP, beginP, nextP, kill_proofP, qed_withP, qedP,
+  terminal_proofP, immediate_proofP, default_proofP, refineP,
+  then_refineP, proofP, clear_undoP, undoP, redoP, undosP, redosP,
+  backP, prevP, upP, topP,
   (*diagnostic commands*)
   print_commandsP, print_theoryP, print_syntaxP, print_attributesP,
   print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,
diff -r 86e9d24f4238 -r 2daaf2943c79 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Thu Mar 18 16:44:53 1999 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Fri Mar 19 11:24:00 1999 +0100
@@ -61,20 +61,18 @@
   val begin_block: ProofHistory.T -> ProofHistory.T
   val next_block: ProofHistory.T -> ProofHistory.T
   val end_block: ProofHistory.T -> ProofHistory.T
-  val qed_with: bstring option * Args.src list option -> ProofHistory.T -> theory
-  val qed_with_i: bstring option * theory attribute list option -> ProofHistory.T -> theory
-  val qed: ProofHistory.T -> theory
-  val kill_proof: ProofHistory.T -> theory
   val tac: Method.text -> ProofHistory.T -> ProofHistory.T
-  val tac_i: (Proof.context -> Proof.method) -> ProofHistory.T -> ProofHistory.T
   val then_tac: Method.text -> ProofHistory.T -> ProofHistory.T
-  val then_tac_i: (Proof.context -> Proof.method) -> ProofHistory.T -> ProofHistory.T
   val proof: Method.text option -> ProofHistory.T -> ProofHistory.T
-  val proof_i: (Proof.context -> Proof.method) option -> ProofHistory.T -> ProofHistory.T
-  val terminal_proof: Method.text -> ProofHistory.T -> ProofHistory.T
-  val terminal_proof_i: (Proof.context -> Proof.method) -> ProofHistory.T -> ProofHistory.T
-  val immediate_proof: ProofHistory.T -> ProofHistory.T
-  val default_proof: ProofHistory.T -> ProofHistory.T
+  val kill_proof: ProofHistory.T -> theory
+  val global_qed_with: bstring option * Args.src list option -> Method.text option
+    -> Toplevel.transition -> Toplevel.transition
+  val global_qed_with_i: bstring option * theory attribute list option -> Method.text option
+    -> Toplevel.transition -> Toplevel.transition
+  val qed: Method.text option -> Toplevel.transition -> Toplevel.transition
+  val terminal_proof: Method.text -> Toplevel.transition -> Toplevel.transition
+  val immediate_proof: Toplevel.transition -> Toplevel.transition
+  val default_proof: Toplevel.transition -> Toplevel.transition
   val use_mltext: string -> theory option -> theory option
   val use_mltext_theory: string -> theory -> theory
   val use_setup: string -> theory -> theory
@@ -201,46 +199,63 @@
 val have_i = local_statement_i true Proof.have_i;
 
 
-(* end proof *)
-
-fun gen_qed_with prep_att (alt_name, raw_atts) prf =
-  let
-    val state = ProofHistory.current prf;
-    val thy = Proof.theory_of state;
-    val alt_atts = apsome (map (prep_att thy)) raw_atts;
-    val (thy', (kind, name, thm)) = Method.qed alt_name alt_atts state;
-
-    val prt_result = Pretty.block
-      [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, Display.pretty_thm thm];
-  in Pretty.writeln prt_result; thy end;
-
-val qed_with = gen_qed_with Attrib.global_attribute;
-val qed_with_i = gen_qed_with (K I);
-
-val qed = qed_with (None, None);
-
-val kill_proof = Proof.theory_of o ProofHistory.current;
-
-
 (* blocks *)
 
 val begin_block = ProofHistory.apply_open Proof.begin_block;
 val next_block = ProofHistory.apply Proof.next_block;
+val end_block = ProofHistory.apply_close Proof.end_block;
 
 
 (* backward steps *)
 
 val tac = ProofHistory.applys o Method.tac;
-val tac_i = tac o Method.Basic;
 val then_tac = ProofHistory.applys o Method.then_tac;
-val then_tac_i = then_tac o Method.Basic;
 val proof = ProofHistory.applys o Method.proof;
-val proof_i = proof o apsome Method.Basic;
-val end_block = ProofHistory.applys_close Method.end_block;
-val terminal_proof = ProofHistory.applys_close o Method.terminal_proof;
-val terminal_proof_i = terminal_proof o Method.Basic;
-val immediate_proof = ProofHistory.applys_close Method.immediate_proof;
-val default_proof = ProofHistory.applys_close Method.default_proof;
+
+
+(* local endings *)
+
+val local_qed = Toplevel.proof o ProofHistory.applys_close o Method.local_qed;
+val local_terminal_proof = Toplevel.proof o ProofHistory.applys_close o Method.local_terminal_proof;
+val local_immediate_proof = Toplevel.proof (ProofHistory.applys_close Method.local_immediate_proof);
+val local_default_proof = Toplevel.proof (ProofHistory.applys_close Method.local_default_proof);
+
+
+(* global endings *)
+
+val kill_proof = Proof.theory_of o ProofHistory.current;
+
+fun global_result finish = Toplevel.proof_to_theory (fn prf =>
+  let
+    val state = ProofHistory.current prf;
+    val _ = if Proof.at_bottom state then () else raise Toplevel.UNDEF;
+    val (thy, (kind, name, thm)) = finish state;
+
+    val prt_result = Pretty.block
+      [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, Display.pretty_thm thm];
+  in Pretty.writeln prt_result; thy end);
+
+fun gen_global_qed_with prep_att (alt_name, raw_atts) opt_text state =
+  let
+    val thy = Proof.theory_of state;
+    val alt_atts = apsome (map (prep_att thy)) raw_atts;
+  in Method.global_qed alt_name alt_atts opt_text state end;
+
+val global_qed_with = global_result oo gen_global_qed_with Attrib.global_attribute;
+val global_qed_with_i = global_result oo gen_global_qed_with (K I);
+val global_qed = global_qed_with (None, None);
+
+val global_terminal_proof = global_result o Method.global_terminal_proof;
+val global_immediate_proof = global_result Method.global_immediate_proof;
+val global_default_proof = global_result Method.global_default_proof;
+
+
+(* common endings *)
+
+fun qed opt_text = local_qed opt_text o global_qed opt_text;
+fun terminal_proof opt_text = local_terminal_proof opt_text o global_terminal_proof opt_text;
+val immediate_proof = local_immediate_proof o global_immediate_proof;
+val default_proof = local_default_proof o global_default_proof;
 
 
 (* use ML text *)
diff -r 86e9d24f4238 -r 2daaf2943c79 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Thu Mar 18 16:44:53 1999 +0100
+++ b/src/Pure/Isar/method.ML	Fri Mar 19 11:24:00 1999 +0100
@@ -49,17 +49,19 @@
     Try of text |
     Repeat of text |
     Repeat1 of text
-  val dynamic_method: string -> (Proof.context -> Proof.method)
   val refine: text -> Proof.state -> Proof.state Seq.seq
   val tac: text -> Proof.state -> Proof.state Seq.seq
   val then_tac: text -> Proof.state -> Proof.state Seq.seq
   val proof: text option -> Proof.state -> Proof.state Seq.seq
-  val end_block: Proof.state -> Proof.state Seq.seq
-  val terminal_proof: text -> Proof.state -> Proof.state Seq.seq
-  val immediate_proof: Proof.state -> Proof.state Seq.seq
-  val default_proof: Proof.state -> Proof.state Seq.seq
-  val qed: bstring option -> theory attribute list option -> Proof.state
-    -> theory * (string * string * thm)
+  val local_qed: text option -> Proof.state -> Proof.state Seq.seq
+  val local_terminal_proof: text -> Proof.state -> Proof.state Seq.seq
+  val local_immediate_proof: Proof.state -> Proof.state Seq.seq
+  val local_default_proof: Proof.state -> Proof.state Seq.seq
+  val global_qed: bstring option -> theory attribute list option -> text option
+    -> Proof.state -> theory * (string * string * thm)
+  val global_terminal_proof: text -> Proof.state -> theory * (string * string * thm)
+  val global_immediate_proof: Proof.state -> theory * (string * string * thm)
+  val global_default_proof: Proof.state -> theory * (string * string * thm)
   val setup: (theory -> theory) list
 end;
 
@@ -241,12 +243,6 @@
   Repeat1 of text;
 
 
-(* dynamic methods *)
-
-fun dynamic_method name = (fn ctxt =>
-  method (ProofContext.theory_of ctxt) (Args.src ((name, []), Position.none)) ctxt);
-
-
 (* refine *)
 
 fun refine text state =
@@ -262,6 +258,8 @@
       | eval (Repeat1 txt) = Seq.REPEAT1 (eval txt);
   in eval text state end;
 
+fun named_method name = Source (Args.src ((name, []), Position.none));
+
 
 (* unstructured steps *)
 
@@ -276,27 +274,28 @@
   |> refine text;
 
 
-(* proof steps *)
+(* structured proof steps *)
 
-val default_txt = Source (Args.src (("default", []), Position.none));
-val finishN = "finish";
+val default_text = named_method "default";
+val finish_text = named_method "finish";
 
 fun proof opt_text state =
   state
   |> Proof.assert_backward
-  |> refine (if_none opt_text default_txt)
+  |> refine (if_none opt_text default_text)
   |> Seq.map Proof.enter_forward;
 
-
-(* conclusions *)
-
-val end_block = Proof.end_block (dynamic_method finishN);
+fun local_qed opt_text = Proof.local_qed (refine (if_none opt_text finish_text));
+fun local_terminal_proof text = Seq.THEN (proof (Some text), local_qed None);
+val local_immediate_proof = local_terminal_proof (Basic (K same));
+val local_default_proof = local_terminal_proof default_text;
 
-fun terminal_proof text = Seq.THEN (proof (Some text), end_block);
-val immediate_proof = terminal_proof (Basic (K same));
-val default_proof = terminal_proof default_txt;
+fun global_qed alt_name alt_atts opt_text =
+  Proof.global_qed (refine (if_none opt_text finish_text)) alt_name alt_atts;
 
-val qed = Proof.qed (dynamic_method finishN);
+fun global_terminal_proof text = Seq.hd o Seq.map (global_qed None None None) o proof (Some text);
+val global_immediate_proof = global_terminal_proof (Basic (K same));
+val global_default_proof = global_terminal_proof default_text;
 
 
 
diff -r 86e9d24f4238 -r 2daaf2943c79 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Mar 18 16:44:53 1999 +0100
+++ b/src/Pure/Isar/proof.ML	Fri Mar 19 11:24:00 1999 +0100
@@ -55,9 +55,11 @@
   val have_i: string -> context attribute list -> term * term list -> state -> state
   val begin_block: state -> state
   val next_block: state -> state
-  val end_block: (context -> method) -> state -> state Seq.seq
-  val qed: (context -> method) -> bstring option -> theory attribute list option -> state
-    -> theory * (string * string * thm)
+  val end_block: state -> state
+  val at_bottom: state -> bool
+  val local_qed: (state -> state Seq.seq) -> state -> state Seq.seq
+  val global_qed: (state -> state Seq.seq) -> bstring option
+    -> theory attribute list option -> state -> theory * (string * string * thm)
 end;
 
 signature PROOF_PRIVATE =
@@ -555,7 +557,11 @@
 fun current_goal (State ({goal = Some goal, ...}, _)) = goal
   | current_goal state = raise STATE ("No current goal!", state);
 
-fun assert_current_goal state = (current_goal state; state);
+fun assert_current_goal true (state as State ({goal = None, ...}, _)) =
+      raise STATE ("No goal in this block!", state)
+  | assert_current_goal false (state as State ({goal = Some _, ...}, _)) =
+      raise STATE ("Goal present in this block!", state)
+  | assert_current_goal _ state = state;
 
 fun assert_bottom true (state as State (_, _ :: _)) =
       raise STATE ("Not at bottom of proof!", state)
@@ -563,6 +569,8 @@
       raise STATE ("Already at bottom of proof!", state)
   | assert_bottom _ state = state;
 
+val at_bottom = can (assert_bottom true o close_block);
+
 
 (* finish proof *)
 
@@ -571,17 +579,28 @@
     None => raise STATE ("Failed to finish proof", state)
   | Some s_sq => Seq.cons s_sq);
 
-fun finish_proof bot meth_fun state =
+fun finish_proof bot finalize state =
   state
   |> assert_forward
   |> close_block
   |> assert_bottom bot
-  |> assert_current_goal
-  |> refine meth_fun
+  |> assert_current_goal true
+  |> finalize
   |> check_finished state;
 
 
-(* conclude local proof *)
+(* end_block *)
+
+fun end_block state =
+  state
+  |> assert_forward
+  |> close_block
+  |> assert_current_goal false
+  |> close_block
+  |> fetch_facts state;
+
+
+(* local_qed *)
 
 fun finish_local state =
   let
@@ -599,21 +618,13 @@
     |> opt_solve
   end;
 
-fun end_block meth_fun state =
-  if can assert_current_goal (close_block state) then
-    state
-    |> finish_proof false meth_fun
-    |> (Seq.flat o Seq.map finish_local)
-  else
-    state
-    |> assert_forward
-    |> close_block
-    |> close_block
-    |> fetch_facts state
-    |> Seq.single;
+fun local_qed finalize state =
+  state
+  |> finish_proof false finalize
+  |> (Seq.flat o Seq.map finish_local);
 
 
-(* conclude global proof *)
+(* global_qed *)
 
 fun finish_global alt_name alt_atts state =
   let
@@ -630,9 +641,9 @@
     val (thy', result') = PureThy.store_thm ((name, result), atts) (theory_of state);
   in (thy', (kind_name kind, name, result')) end;
 
-fun qed meth_fun alt_name alt_atts state =
+fun global_qed finalize alt_name alt_atts state =
   state
-  |> finish_proof true meth_fun
+  |> finish_proof true finalize
   |> Seq.hd
   |> finish_global alt_name alt_atts;