added "done" proof;
authorwenzelm
Wed May 24 19:09:50 2000 +0200 (2000-05-24)
changeset 8966916966f68907
parent 8965 d46b36785c70
child 8967 00f18476ac15
added "done" proof;
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/isar_thy.ML
src/Pure/Isar/method.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Wed May 24 19:09:36 2000 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed May 24 19:09:50 2000 +0200
     1.3 @@ -371,13 +371,17 @@
     1.4      (P.method -- P.interest -- Scan.option (P.method -- P.interest)
     1.5        -- P.marg_comment >> IsarThy.terminal_proof);
     1.6  
     1.7 +val default_proofP =
     1.8 +  OuterSyntax.command ".." "default proof" K.qed
     1.9 +    (P.marg_comment >> IsarThy.default_proof);
    1.10 +
    1.11  val immediate_proofP =
    1.12    OuterSyntax.command "." "immediate proof" K.qed
    1.13      (P.marg_comment >> IsarThy.immediate_proof);
    1.14  
    1.15 -val default_proofP =
    1.16 -  OuterSyntax.command ".." "default proof" K.qed
    1.17 -    (P.marg_comment >> IsarThy.default_proof);
    1.18 +val done_proofP =
    1.19 +  OuterSyntax.command "done" "done proof" K.qed
    1.20 +    (P.marg_comment >> IsarThy.done_proof);
    1.21  
    1.22  val skip_proofP =
    1.23    OuterSyntax.improper_command "sorry" "skip proof (quick-and-dirty mode only!)" K.qed
    1.24 @@ -648,9 +652,9 @@
    1.25    (*proof commands*)
    1.26    theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, presumeP,
    1.27    defP, fixP, letP, caseP, thenP, fromP, withP, noteP, beginP, endP,
    1.28 -  nextP, qedP, terminal_proofP, immediate_proofP, default_proofP,
    1.29 -  skip_proofP, forget_proofP, deferP, preferP, applyP, apply_endP,
    1.30 -  proofP, alsoP, finallyP, moreoverP, ultimatelyP, backP,
    1.31 +  nextP, qedP, terminal_proofP, default_proofP, immediate_proofP,
    1.32 +  done_proofP, skip_proofP, forget_proofP, deferP, preferP, applyP,
    1.33 +  apply_endP, proofP, alsoP, finallyP, moreoverP, ultimatelyP, backP,
    1.34    cannot_undoP, clear_undosP, redoP, undos_proofP, undoP, killP,
    1.35    (*diagnostic commands*)
    1.36    pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
     2.1 --- a/src/Pure/Isar/isar_thy.ML	Wed May 24 19:09:36 2000 +0200
     2.2 +++ b/src/Pure/Isar/isar_thy.ML	Wed May 24 19:09:50 2000 +0200
     2.3 @@ -135,8 +135,9 @@
     2.4      -> Toplevel.transition -> Toplevel.transition
     2.5    val terminal_proof: ((Method.text * Comment.interest) * (Method.text * Comment.interest) option)
     2.6      * Comment.text -> Toplevel.transition -> Toplevel.transition
     2.7 +  val default_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
     2.8    val immediate_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
     2.9 -  val default_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
    2.10 +  val done_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
    2.11    val skip_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
    2.12    val forget_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
    2.13    val get_thmss: (string * Args.src list) list -> Proof.state -> thm list
    2.14 @@ -438,16 +439,17 @@
    2.15  (* local endings *)
    2.16  
    2.17  val local_qed =
    2.18 -  proof'' o (ProofHistory.applys oo Method.local_qed) o apsome Comment.ignore_interest;
    2.19 +  proof'' o (ProofHistory.applys oo Method.local_qed true) o apsome Comment.ignore_interest;
    2.20  
    2.21  fun ignore_interests (x, y) = (Comment.ignore_interest x, apsome Comment.ignore_interest y);
    2.22  
    2.23  val local_terminal_proof =
    2.24    proof'' o (ProofHistory.applys oo Method.local_terminal_proof) o ignore_interests;
    2.25  
    2.26 +val local_default_proof = proof'' (ProofHistory.applys o Method.local_default_proof);
    2.27  val local_immediate_proof = proof'' (ProofHistory.applys o Method.local_immediate_proof);
    2.28 -val local_default_proof = proof'' (ProofHistory.applys o Method.local_default_proof);
    2.29  val local_skip_proof = proof'' (ProofHistory.applys o SkipProof.local_skip_proof);
    2.30 +val local_done_proof = proof'' (ProofHistory.applys o Method.local_done_proof);
    2.31  
    2.32  
    2.33  (* global endings *)
    2.34 @@ -459,19 +461,21 @@
    2.35      val (thy, res as {kind, name, thm}) = finish state;
    2.36    in print_result res; Context.setmp (Some thy) (Present.result kind name) thm; thy end);
    2.37  
    2.38 -val global_qed = global_result o Method.global_qed o apsome Comment.ignore_interest;
    2.39 +val global_qed = global_result o Method.global_qed true o apsome Comment.ignore_interest;
    2.40  val global_terminal_proof = global_result o Method.global_terminal_proof o ignore_interests;
    2.41 +val global_default_proof = global_result Method.global_default_proof;
    2.42  val global_immediate_proof = global_result Method.global_immediate_proof;
    2.43 -val global_default_proof = global_result Method.global_default_proof;
    2.44  val global_skip_proof = global_result SkipProof.global_skip_proof;
    2.45 +val global_done_proof = global_result Method.global_done_proof;
    2.46  
    2.47  
    2.48  (* common endings *)
    2.49  
    2.50  fun qed (meth, comment) = local_qed meth o global_qed meth;
    2.51  fun terminal_proof (meths, comment) = local_terminal_proof meths o global_terminal_proof meths;
    2.52 +fun default_proof comment = local_default_proof o global_default_proof;
    2.53  fun immediate_proof comment = local_immediate_proof o global_immediate_proof;
    2.54 -fun default_proof comment = local_default_proof o global_default_proof;
    2.55 +fun done_proof comment = local_done_proof o global_done_proof;
    2.56  fun skip_proof comment = local_skip_proof o global_skip_proof;
    2.57  
    2.58  fun forget_proof comment = Toplevel.proof_to_theory (Proof.theory_of o ProofHistory.current);
     3.1 --- a/src/Pure/Isar/method.ML	Wed May 24 19:09:36 2000 +0200
     3.2 +++ b/src/Pure/Isar/method.ML	Wed May 24 19:09:50 2000 +0200
     3.3 @@ -86,21 +86,25 @@
     3.4    val refine: text -> Proof.state -> Proof.state Seq.seq
     3.5    val refine_end: text -> Proof.state -> Proof.state Seq.seq
     3.6    val proof: text option -> Proof.state -> Proof.state Seq.seq
     3.7 -  val local_qed: text option
     3.8 +  val local_qed: bool -> text option
     3.9      -> ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
    3.10      -> Proof.state -> Proof.state Seq.seq
    3.11    val local_terminal_proof: text * text option
    3.12      -> ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
    3.13      -> Proof.state -> Proof.state Seq.seq
    3.14 -  val local_immediate_proof: ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
    3.15 -    -> Proof.state -> Proof.state Seq.seq
    3.16    val local_default_proof: ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
    3.17      -> Proof.state -> Proof.state Seq.seq
    3.18 -  val global_qed: text option -> Proof.state -> theory * {kind: string, name: string, thm: thm}
    3.19 +  val local_immediate_proof: ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
    3.20 +    -> Proof.state -> Proof.state Seq.seq
    3.21 +  val local_done_proof: ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
    3.22 +    -> Proof.state -> Proof.state Seq.seq
    3.23 +  val global_qed: bool -> text option
    3.24 +    -> Proof.state -> theory * {kind: string, name: string, thm: thm}
    3.25    val global_terminal_proof: text * text option
    3.26      -> Proof.state -> theory * {kind: string, name: string, thm: thm}
    3.27 +  val global_default_proof: Proof.state -> theory * {kind: string, name: string, thm: thm}
    3.28    val global_immediate_proof: Proof.state -> theory * {kind: string, name: string, thm: thm}
    3.29 -  val global_default_proof: Proof.state -> theory * {kind: string, name: string, thm: thm}
    3.30 +  val global_done_proof: Proof.state -> theory * {kind: string, name: string, thm: thm}
    3.31    val setup: (theory -> theory) list
    3.32  end;
    3.33  
    3.34 @@ -202,7 +206,7 @@
    3.35  val METHOD = Proof.method;
    3.36  val METHOD_CASES = Proof.method_cases;
    3.37  
    3.38 -fun METHOD0 tac = METHOD (fn [] => tac | _ => error "Method may not be used with facts");
    3.39 +fun METHOD0 tac = METHOD (fn [] => tac | _ => error "Cannot handle current facts");
    3.40  
    3.41  
    3.42  (* primitive *)
    3.43 @@ -536,11 +540,13 @@
    3.44  
    3.45  val default_text = Source (Args.src (("default", []), Position.none));
    3.46  val this_text = Basic (K this);
    3.47 -
    3.48 -fun finish ctxt = METHOD (K (FILTER Thm.no_prems (ALLGOALS (assm_tac ctxt) THEN flexflex_tac)));
    3.49 +val done_text = Basic (K (METHOD0 all_tac));
    3.50  
    3.51 -fun finish_text None = Basic finish
    3.52 -  | finish_text (Some txt) = Then [txt, Basic finish];
    3.53 +fun close_text asm = Basic (fn ctxt => METHOD (K
    3.54 +  (FILTER Thm.no_prems ((if asm then ALLGOALS (assm_tac ctxt) else all_tac) THEN flexflex_tac))));
    3.55 +
    3.56 +fun finish_text asm None = close_text asm
    3.57 +  | finish_text asm (Some txt) = Then [txt, close_text asm];
    3.58  
    3.59  fun proof opt_text state =
    3.60    state
    3.61 @@ -549,31 +555,34 @@
    3.62    |> Seq.map (Proof.goal_facts (K []))
    3.63    |> Seq.map Proof.enter_forward;
    3.64  
    3.65 -fun local_qed opt_text = Proof.local_qed (refine (finish_text opt_text));
    3.66 -fun local_terminal_proof (text, opt_text) pr = Seq.THEN (proof (Some text), local_qed opt_text pr);
    3.67 +fun local_qed asm opt_text = Proof.local_qed (refine (finish_text asm opt_text));
    3.68 +fun local_terminal_proof (text, opt_text) pr =
    3.69 +  Seq.THEN (proof (Some text), local_qed true opt_text pr);
    3.70 +val local_default_proof = local_terminal_proof (default_text, None);
    3.71  val local_immediate_proof = local_terminal_proof (this_text, None);
    3.72 -val local_default_proof = local_terminal_proof (default_text, None);
    3.73 +fun local_done_proof pr = Seq.THEN (proof (Some done_text), local_qed false None pr);
    3.74  
    3.75  
    3.76 -fun global_qeds opt_text = Proof.global_qed (refine (finish_text opt_text));
    3.77 +fun global_qeds asm opt_text = Proof.global_qed (refine (finish_text asm opt_text));
    3.78  
    3.79 -fun global_qed opt_text state =
    3.80 +fun global_qed asm opt_text state =
    3.81    state
    3.82 -  |> global_qeds opt_text
    3.83 +  |> global_qeds asm opt_text
    3.84    |> Proof.check_result "Failed to finish proof" state
    3.85    |> Seq.hd;
    3.86  
    3.87 -fun global_terminal_proof (text, opt_text) state =
    3.88 +fun global_term_proof asm (text, opt_text) state =
    3.89    state
    3.90    |> proof (Some text)
    3.91    |> Proof.check_result "Terminal proof method failed" state
    3.92 -  |> (Seq.flat o Seq.map (global_qeds opt_text))
    3.93 +  |> (Seq.flat o Seq.map (global_qeds asm opt_text))
    3.94    |> Proof.check_result "Failed to finish proof (after successful terminal method)" state
    3.95    |> Seq.hd;
    3.96  
    3.97 -val global_immediate_proof = global_terminal_proof (this_text, None);
    3.98 +val global_terminal_proof = global_term_proof true;
    3.99  val global_default_proof = global_terminal_proof (default_text, None);
   3.100 -
   3.101 +val global_immediate_proof = global_terminal_proof (this_text, None);
   3.102 +val global_done_proof = global_term_proof false (done_text, None);
   3.103  
   3.104  
   3.105  (** theory setup **)