common qed and end of proofs;
authorwenzelm
Fri Mar 19 11:24:00 1999 +0100 (1999-03-19)
changeset 64042daaf2943c79
parent 6403 86e9d24f4238
child 6405 39922bfb7107
common qed and end of proofs;
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/isar_thy.ML
src/Pure/Isar/method.ML
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Mar 18 16:44:53 1999 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Mar 19 11:24:00 1999 +0100
     1.3 @@ -33,7 +33,7 @@
     1.4  
     1.5  (*end current theory / sub-proof / excursion*)
     1.6  val endP =
     1.7 -  OuterSyntax.command "end" "end current theory / sub-proof / excursion"
     1.8 +  OuterSyntax.command "end" "end current block / theory / excursion"
     1.9      (Scan.succeed (Toplevel.print o Toplevel.exit o Toplevel.proof IsarThy.end_block));
    1.10  
    1.11  val contextP =
    1.12 @@ -308,42 +308,45 @@
    1.13  
    1.14  (* end proof *)
    1.15  
    1.16 -val qedP =
    1.17 -  OuterSyntax.command "qed" "conclude proof"
    1.18 -    (Scan.succeed (Toplevel.proof_to_theory IsarThy.qed));
    1.19 +val kill_proofP =
    1.20 +  OuterSyntax.improper_command "kill" "abort current proof"
    1.21 +    (Scan.succeed (Toplevel.print o Toplevel.proof_to_theory IsarThy.kill_proof));
    1.22  
    1.23  val qed_withP =
    1.24    OuterSyntax.improper_command "qed_with" "conclude proof, may patch name and attributes"
    1.25 -    (Scan.option name -- Scan.option attribs >> (Toplevel.proof_to_theory o IsarThy.qed_with));
    1.26 +    (Scan.option name -- Scan.option attribs -- Scan.option method
    1.27 +      >> (uncurry IsarThy.global_qed_with));
    1.28 +
    1.29 +val qedP =
    1.30 +  OuterSyntax.command "qed" "conclude (sub-)proof"
    1.31 +    (Scan.option method >> IsarThy.qed);
    1.32  
    1.33 -val kill_proofP =
    1.34 -  OuterSyntax.improper_command "kill" "abort current proof"
    1.35 -    (Scan.succeed (Toplevel.print o Toplevel.proof_to_theory IsarThy.kill_proof));
    1.36 +val terminal_proofP =
    1.37 +  OuterSyntax.command "by" "terminal backward proof"
    1.38 +    (method >> (Toplevel.print oo IsarThy.terminal_proof));
    1.39 +
    1.40 +val immediate_proofP =
    1.41 +  OuterSyntax.command "." "immediate proof"
    1.42 +    (Scan.succeed (Toplevel.print o IsarThy.immediate_proof));
    1.43 +
    1.44 +val default_proofP =
    1.45 +  OuterSyntax.command ".." "default proof"
    1.46 +    (Scan.succeed (Toplevel.print o IsarThy.default_proof));
    1.47  
    1.48  
    1.49  (* proof steps *)
    1.50  
    1.51 -fun gen_stepP meth int name cmt f =
    1.52 -  OuterSyntax.parser int name cmt
    1.53 -    (meth >> (fn txt => Toplevel.print o Toplevel.proof (f txt)));
    1.54 -
    1.55 -val stepP = gen_stepP method;
    1.56 -
    1.57 -val refineP = stepP true "refine" "unstructured backward proof step, ignoring facts" IsarThy.tac;
    1.58 -val then_refineP =
    1.59 -  stepP true "then_refine" "unstructured backward proof step, using facts" IsarThy.then_tac;
    1.60 -
    1.61 +val refineP =
    1.62 +  OuterSyntax.improper_command "refine" "unstructured backward proof step, ignoring facts"
    1.63 +    (method >> (Toplevel.print oo (Toplevel.proof o IsarThy.tac)));
    1.64  
    1.65 -val proofP = gen_stepP (Scan.option method) false "proof" "backward proof" IsarThy.proof;
    1.66 -val terminal_proofP = stepP false "by" "terminal backward proof" IsarThy.terminal_proof;
    1.67 +val then_refineP =
    1.68 +  OuterSyntax.improper_command "then_refine" "unstructured backward proof step, using facts"
    1.69 +    (method >> (Toplevel.print oo (Toplevel.proof o IsarThy.then_tac)));
    1.70  
    1.71 -val immediate_proofP =
    1.72 -  OuterSyntax.command "." "immediate proof"
    1.73 -    (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.immediate_proof));
    1.74 -
    1.75 -val default_proofP =
    1.76 -  OuterSyntax.command ".." "default proof"
    1.77 -    (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.default_proof));
    1.78 +val proofP =
    1.79 +  OuterSyntax.command "proof" "backward proof"
    1.80 +    (Scan.option method >> (Toplevel.print oo (Toplevel.proof o IsarThy.proof)));
    1.81  
    1.82  
    1.83  (* proof history *)
    1.84 @@ -507,10 +510,10 @@
    1.85    print_ast_translationP, token_translationP, oracleP,
    1.86    (*proof commands*)
    1.87    theoremP, lemmaP, showP, haveP, assumeP, fixP, letP, thenP, fromP,
    1.88 -  factsP, beginP, nextP, qedP, qed_withP, kill_proofP, refineP,
    1.89 -  then_refineP, proofP, terminal_proofP, immediate_proofP,
    1.90 -  default_proofP, clear_undoP, undoP, redoP, undosP, redosP, backP,
    1.91 -  prevP, upP, topP,
    1.92 +  factsP, beginP, nextP, kill_proofP, qed_withP, qedP,
    1.93 +  terminal_proofP, immediate_proofP, default_proofP, refineP,
    1.94 +  then_refineP, proofP, clear_undoP, undoP, redoP, undosP, redosP,
    1.95 +  backP, prevP, upP, topP,
    1.96    (*diagnostic commands*)
    1.97    print_commandsP, print_theoryP, print_syntaxP, print_attributesP,
    1.98    print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,
     2.1 --- a/src/Pure/Isar/isar_thy.ML	Thu Mar 18 16:44:53 1999 +0100
     2.2 +++ b/src/Pure/Isar/isar_thy.ML	Fri Mar 19 11:24:00 1999 +0100
     2.3 @@ -61,20 +61,18 @@
     2.4    val begin_block: ProofHistory.T -> ProofHistory.T
     2.5    val next_block: ProofHistory.T -> ProofHistory.T
     2.6    val end_block: ProofHistory.T -> ProofHistory.T
     2.7 -  val qed_with: bstring option * Args.src list option -> ProofHistory.T -> theory
     2.8 -  val qed_with_i: bstring option * theory attribute list option -> ProofHistory.T -> theory
     2.9 -  val qed: ProofHistory.T -> theory
    2.10 -  val kill_proof: ProofHistory.T -> theory
    2.11    val tac: Method.text -> ProofHistory.T -> ProofHistory.T
    2.12 -  val tac_i: (Proof.context -> Proof.method) -> ProofHistory.T -> ProofHistory.T
    2.13    val then_tac: Method.text -> ProofHistory.T -> ProofHistory.T
    2.14 -  val then_tac_i: (Proof.context -> Proof.method) -> ProofHistory.T -> ProofHistory.T
    2.15    val proof: Method.text option -> ProofHistory.T -> ProofHistory.T
    2.16 -  val proof_i: (Proof.context -> Proof.method) option -> ProofHistory.T -> ProofHistory.T
    2.17 -  val terminal_proof: Method.text -> ProofHistory.T -> ProofHistory.T
    2.18 -  val terminal_proof_i: (Proof.context -> Proof.method) -> ProofHistory.T -> ProofHistory.T
    2.19 -  val immediate_proof: ProofHistory.T -> ProofHistory.T
    2.20 -  val default_proof: ProofHistory.T -> ProofHistory.T
    2.21 +  val kill_proof: ProofHistory.T -> theory
    2.22 +  val global_qed_with: bstring option * Args.src list option -> Method.text option
    2.23 +    -> Toplevel.transition -> Toplevel.transition
    2.24 +  val global_qed_with_i: bstring option * theory attribute list option -> Method.text option
    2.25 +    -> Toplevel.transition -> Toplevel.transition
    2.26 +  val qed: Method.text option -> Toplevel.transition -> Toplevel.transition
    2.27 +  val terminal_proof: Method.text -> Toplevel.transition -> Toplevel.transition
    2.28 +  val immediate_proof: Toplevel.transition -> Toplevel.transition
    2.29 +  val default_proof: Toplevel.transition -> Toplevel.transition
    2.30    val use_mltext: string -> theory option -> theory option
    2.31    val use_mltext_theory: string -> theory -> theory
    2.32    val use_setup: string -> theory -> theory
    2.33 @@ -201,46 +199,63 @@
    2.34  val have_i = local_statement_i true Proof.have_i;
    2.35  
    2.36  
    2.37 -(* end proof *)
    2.38 -
    2.39 -fun gen_qed_with prep_att (alt_name, raw_atts) prf =
    2.40 -  let
    2.41 -    val state = ProofHistory.current prf;
    2.42 -    val thy = Proof.theory_of state;
    2.43 -    val alt_atts = apsome (map (prep_att thy)) raw_atts;
    2.44 -    val (thy', (kind, name, thm)) = Method.qed alt_name alt_atts state;
    2.45 -
    2.46 -    val prt_result = Pretty.block
    2.47 -      [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, Display.pretty_thm thm];
    2.48 -  in Pretty.writeln prt_result; thy end;
    2.49 -
    2.50 -val qed_with = gen_qed_with Attrib.global_attribute;
    2.51 -val qed_with_i = gen_qed_with (K I);
    2.52 -
    2.53 -val qed = qed_with (None, None);
    2.54 -
    2.55 -val kill_proof = Proof.theory_of o ProofHistory.current;
    2.56 -
    2.57 -
    2.58  (* blocks *)
    2.59  
    2.60  val begin_block = ProofHistory.apply_open Proof.begin_block;
    2.61  val next_block = ProofHistory.apply Proof.next_block;
    2.62 +val end_block = ProofHistory.apply_close Proof.end_block;
    2.63  
    2.64  
    2.65  (* backward steps *)
    2.66  
    2.67  val tac = ProofHistory.applys o Method.tac;
    2.68 -val tac_i = tac o Method.Basic;
    2.69  val then_tac = ProofHistory.applys o Method.then_tac;
    2.70 -val then_tac_i = then_tac o Method.Basic;
    2.71  val proof = ProofHistory.applys o Method.proof;
    2.72 -val proof_i = proof o apsome Method.Basic;
    2.73 -val end_block = ProofHistory.applys_close Method.end_block;
    2.74 -val terminal_proof = ProofHistory.applys_close o Method.terminal_proof;
    2.75 -val terminal_proof_i = terminal_proof o Method.Basic;
    2.76 -val immediate_proof = ProofHistory.applys_close Method.immediate_proof;
    2.77 -val default_proof = ProofHistory.applys_close Method.default_proof;
    2.78 +
    2.79 +
    2.80 +(* local endings *)
    2.81 +
    2.82 +val local_qed = Toplevel.proof o ProofHistory.applys_close o Method.local_qed;
    2.83 +val local_terminal_proof = Toplevel.proof o ProofHistory.applys_close o Method.local_terminal_proof;
    2.84 +val local_immediate_proof = Toplevel.proof (ProofHistory.applys_close Method.local_immediate_proof);
    2.85 +val local_default_proof = Toplevel.proof (ProofHistory.applys_close Method.local_default_proof);
    2.86 +
    2.87 +
    2.88 +(* global endings *)
    2.89 +
    2.90 +val kill_proof = Proof.theory_of o ProofHistory.current;
    2.91 +
    2.92 +fun global_result finish = Toplevel.proof_to_theory (fn prf =>
    2.93 +  let
    2.94 +    val state = ProofHistory.current prf;
    2.95 +    val _ = if Proof.at_bottom state then () else raise Toplevel.UNDEF;
    2.96 +    val (thy, (kind, name, thm)) = finish state;
    2.97 +
    2.98 +    val prt_result = Pretty.block
    2.99 +      [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, Display.pretty_thm thm];
   2.100 +  in Pretty.writeln prt_result; thy end);
   2.101 +
   2.102 +fun gen_global_qed_with prep_att (alt_name, raw_atts) opt_text state =
   2.103 +  let
   2.104 +    val thy = Proof.theory_of state;
   2.105 +    val alt_atts = apsome (map (prep_att thy)) raw_atts;
   2.106 +  in Method.global_qed alt_name alt_atts opt_text state end;
   2.107 +
   2.108 +val global_qed_with = global_result oo gen_global_qed_with Attrib.global_attribute;
   2.109 +val global_qed_with_i = global_result oo gen_global_qed_with (K I);
   2.110 +val global_qed = global_qed_with (None, None);
   2.111 +
   2.112 +val global_terminal_proof = global_result o Method.global_terminal_proof;
   2.113 +val global_immediate_proof = global_result Method.global_immediate_proof;
   2.114 +val global_default_proof = global_result Method.global_default_proof;
   2.115 +
   2.116 +
   2.117 +(* common endings *)
   2.118 +
   2.119 +fun qed opt_text = local_qed opt_text o global_qed opt_text;
   2.120 +fun terminal_proof opt_text = local_terminal_proof opt_text o global_terminal_proof opt_text;
   2.121 +val immediate_proof = local_immediate_proof o global_immediate_proof;
   2.122 +val default_proof = local_default_proof o global_default_proof;
   2.123  
   2.124  
   2.125  (* use ML text *)
     3.1 --- a/src/Pure/Isar/method.ML	Thu Mar 18 16:44:53 1999 +0100
     3.2 +++ b/src/Pure/Isar/method.ML	Fri Mar 19 11:24:00 1999 +0100
     3.3 @@ -49,17 +49,19 @@
     3.4      Try of text |
     3.5      Repeat of text |
     3.6      Repeat1 of text
     3.7 -  val dynamic_method: string -> (Proof.context -> Proof.method)
     3.8    val refine: text -> Proof.state -> Proof.state Seq.seq
     3.9    val tac: text -> Proof.state -> Proof.state Seq.seq
    3.10    val then_tac: text -> Proof.state -> Proof.state Seq.seq
    3.11    val proof: text option -> Proof.state -> Proof.state Seq.seq
    3.12 -  val end_block: Proof.state -> Proof.state Seq.seq
    3.13 -  val terminal_proof: text -> Proof.state -> Proof.state Seq.seq
    3.14 -  val immediate_proof: Proof.state -> Proof.state Seq.seq
    3.15 -  val default_proof: Proof.state -> Proof.state Seq.seq
    3.16 -  val qed: bstring option -> theory attribute list option -> Proof.state
    3.17 -    -> theory * (string * string * thm)
    3.18 +  val local_qed: text option -> Proof.state -> Proof.state Seq.seq
    3.19 +  val local_terminal_proof: text -> Proof.state -> Proof.state Seq.seq
    3.20 +  val local_immediate_proof: Proof.state -> Proof.state Seq.seq
    3.21 +  val local_default_proof: Proof.state -> Proof.state Seq.seq
    3.22 +  val global_qed: bstring option -> theory attribute list option -> text option
    3.23 +    -> Proof.state -> theory * (string * string * thm)
    3.24 +  val global_terminal_proof: text -> Proof.state -> theory * (string * string * thm)
    3.25 +  val global_immediate_proof: Proof.state -> theory * (string * string * thm)
    3.26 +  val global_default_proof: Proof.state -> theory * (string * string * thm)
    3.27    val setup: (theory -> theory) list
    3.28  end;
    3.29  
    3.30 @@ -241,12 +243,6 @@
    3.31    Repeat1 of text;
    3.32  
    3.33  
    3.34 -(* dynamic methods *)
    3.35 -
    3.36 -fun dynamic_method name = (fn ctxt =>
    3.37 -  method (ProofContext.theory_of ctxt) (Args.src ((name, []), Position.none)) ctxt);
    3.38 -
    3.39 -
    3.40  (* refine *)
    3.41  
    3.42  fun refine text state =
    3.43 @@ -262,6 +258,8 @@
    3.44        | eval (Repeat1 txt) = Seq.REPEAT1 (eval txt);
    3.45    in eval text state end;
    3.46  
    3.47 +fun named_method name = Source (Args.src ((name, []), Position.none));
    3.48 +
    3.49  
    3.50  (* unstructured steps *)
    3.51  
    3.52 @@ -276,27 +274,28 @@
    3.53    |> refine text;
    3.54  
    3.55  
    3.56 -(* proof steps *)
    3.57 +(* structured proof steps *)
    3.58  
    3.59 -val default_txt = Source (Args.src (("default", []), Position.none));
    3.60 -val finishN = "finish";
    3.61 +val default_text = named_method "default";
    3.62 +val finish_text = named_method "finish";
    3.63  
    3.64  fun proof opt_text state =
    3.65    state
    3.66    |> Proof.assert_backward
    3.67 -  |> refine (if_none opt_text default_txt)
    3.68 +  |> refine (if_none opt_text default_text)
    3.69    |> Seq.map Proof.enter_forward;
    3.70  
    3.71 -
    3.72 -(* conclusions *)
    3.73 -
    3.74 -val end_block = Proof.end_block (dynamic_method finishN);
    3.75 +fun local_qed opt_text = Proof.local_qed (refine (if_none opt_text finish_text));
    3.76 +fun local_terminal_proof text = Seq.THEN (proof (Some text), local_qed None);
    3.77 +val local_immediate_proof = local_terminal_proof (Basic (K same));
    3.78 +val local_default_proof = local_terminal_proof default_text;
    3.79  
    3.80 -fun terminal_proof text = Seq.THEN (proof (Some text), end_block);
    3.81 -val immediate_proof = terminal_proof (Basic (K same));
    3.82 -val default_proof = terminal_proof default_txt;
    3.83 +fun global_qed alt_name alt_atts opt_text =
    3.84 +  Proof.global_qed (refine (if_none opt_text finish_text)) alt_name alt_atts;
    3.85  
    3.86 -val qed = Proof.qed (dynamic_method finishN);
    3.87 +fun global_terminal_proof text = Seq.hd o Seq.map (global_qed None None None) o proof (Some text);
    3.88 +val global_immediate_proof = global_terminal_proof (Basic (K same));
    3.89 +val global_default_proof = global_terminal_proof default_text;
    3.90  
    3.91  
    3.92  
     4.1 --- a/src/Pure/Isar/proof.ML	Thu Mar 18 16:44:53 1999 +0100
     4.2 +++ b/src/Pure/Isar/proof.ML	Fri Mar 19 11:24:00 1999 +0100
     4.3 @@ -55,9 +55,11 @@
     4.4    val have_i: string -> context attribute list -> term * term list -> state -> state
     4.5    val begin_block: state -> state
     4.6    val next_block: state -> state
     4.7 -  val end_block: (context -> method) -> state -> state Seq.seq
     4.8 -  val qed: (context -> method) -> bstring option -> theory attribute list option -> state
     4.9 -    -> theory * (string * string * thm)
    4.10 +  val end_block: state -> state
    4.11 +  val at_bottom: state -> bool
    4.12 +  val local_qed: (state -> state Seq.seq) -> state -> state Seq.seq
    4.13 +  val global_qed: (state -> state Seq.seq) -> bstring option
    4.14 +    -> theory attribute list option -> state -> theory * (string * string * thm)
    4.15  end;
    4.16  
    4.17  signature PROOF_PRIVATE =
    4.18 @@ -555,7 +557,11 @@
    4.19  fun current_goal (State ({goal = Some goal, ...}, _)) = goal
    4.20    | current_goal state = raise STATE ("No current goal!", state);
    4.21  
    4.22 -fun assert_current_goal state = (current_goal state; state);
    4.23 +fun assert_current_goal true (state as State ({goal = None, ...}, _)) =
    4.24 +      raise STATE ("No goal in this block!", state)
    4.25 +  | assert_current_goal false (state as State ({goal = Some _, ...}, _)) =
    4.26 +      raise STATE ("Goal present in this block!", state)
    4.27 +  | assert_current_goal _ state = state;
    4.28  
    4.29  fun assert_bottom true (state as State (_, _ :: _)) =
    4.30        raise STATE ("Not at bottom of proof!", state)
    4.31 @@ -563,6 +569,8 @@
    4.32        raise STATE ("Already at bottom of proof!", state)
    4.33    | assert_bottom _ state = state;
    4.34  
    4.35 +val at_bottom = can (assert_bottom true o close_block);
    4.36 +
    4.37  
    4.38  (* finish proof *)
    4.39  
    4.40 @@ -571,17 +579,28 @@
    4.41      None => raise STATE ("Failed to finish proof", state)
    4.42    | Some s_sq => Seq.cons s_sq);
    4.43  
    4.44 -fun finish_proof bot meth_fun state =
    4.45 +fun finish_proof bot finalize state =
    4.46    state
    4.47    |> assert_forward
    4.48    |> close_block
    4.49    |> assert_bottom bot
    4.50 -  |> assert_current_goal
    4.51 -  |> refine meth_fun
    4.52 +  |> assert_current_goal true
    4.53 +  |> finalize
    4.54    |> check_finished state;
    4.55  
    4.56  
    4.57 -(* conclude local proof *)
    4.58 +(* end_block *)
    4.59 +
    4.60 +fun end_block state =
    4.61 +  state
    4.62 +  |> assert_forward
    4.63 +  |> close_block
    4.64 +  |> assert_current_goal false
    4.65 +  |> close_block
    4.66 +  |> fetch_facts state;
    4.67 +
    4.68 +
    4.69 +(* local_qed *)
    4.70  
    4.71  fun finish_local state =
    4.72    let
    4.73 @@ -599,21 +618,13 @@
    4.74      |> opt_solve
    4.75    end;
    4.76  
    4.77 -fun end_block meth_fun state =
    4.78 -  if can assert_current_goal (close_block state) then
    4.79 -    state
    4.80 -    |> finish_proof false meth_fun
    4.81 -    |> (Seq.flat o Seq.map finish_local)
    4.82 -  else
    4.83 -    state
    4.84 -    |> assert_forward
    4.85 -    |> close_block
    4.86 -    |> close_block
    4.87 -    |> fetch_facts state
    4.88 -    |> Seq.single;
    4.89 +fun local_qed finalize state =
    4.90 +  state
    4.91 +  |> finish_proof false finalize
    4.92 +  |> (Seq.flat o Seq.map finish_local);
    4.93  
    4.94  
    4.95 -(* conclude global proof *)
    4.96 +(* global_qed *)
    4.97  
    4.98  fun finish_global alt_name alt_atts state =
    4.99    let
   4.100 @@ -630,9 +641,9 @@
   4.101      val (thy', result') = PureThy.store_thm ((name, result), atts) (theory_of state);
   4.102    in (thy', (kind_name kind, name, result')) end;
   4.103  
   4.104 -fun qed meth_fun alt_name alt_atts state =
   4.105 +fun global_qed finalize alt_name alt_atts state =
   4.106    state
   4.107 -  |> finish_proof true meth_fun
   4.108 +  |> finish_proof true finalize
   4.109    |> Seq.hd
   4.110    |> finish_global alt_name alt_atts;
   4.111