added 'ultimately';
authorwenzelm
Sun Mar 26 22:31:11 2000 +0200 (2000-03-26)
changeset 8588b7c3f264f8ac
parent 8587 49069dfedb1e
child 8589 a24f7e5ee7ef
added 'ultimately';
src/Pure/Isar/calculation.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/isar_thy.ML
     1.1 --- a/src/Pure/Isar/calculation.ML	Sun Mar 26 22:29:33 2000 +0200
     1.2 +++ b/src/Pure/Isar/calculation.ML	Sun Mar 26 22:31:11 2000 +0200
     1.3 @@ -16,6 +16,7 @@
     1.4    val also: thm list option -> (thm list -> unit) -> Proof.state -> Proof.state Seq.seq
     1.5    val finally: thm list option -> (thm list -> unit) -> Proof.state -> Proof.state Seq.seq
     1.6    val moreover: (thm list -> unit) -> Proof.state -> Proof.state
     1.7 +  val ultimately: (thm list -> unit) -> Proof.state -> Proof.state
     1.8    val setup: (theory -> theory) list
     1.9  end;
    1.10  
    1.11 @@ -104,22 +105,29 @@
    1.12  
    1.13  (** proof commands **)
    1.14  
    1.15 -(* maintain calculation *)
    1.16 +(* maintain calculation register *)
    1.17  
    1.18  val calculationN = "calculation";
    1.19  
    1.20 -fun maintain_calculation calc state =
    1.21 -  state
    1.22 -  |> put_calculation calc
    1.23 -  |> Proof.simple_have_thms calculationN calc
    1.24 -  |> Proof.reset_facts;
    1.25 +fun maintain_calculation false calc state =
    1.26 +      state
    1.27 +      |> put_calculation calc
    1.28 +      |> Proof.simple_have_thms calculationN calc
    1.29 +      |> Proof.reset_facts
    1.30 +  | maintain_calculation true calc state =
    1.31 +      state
    1.32 +      |> reset_calculation
    1.33 +      |> Proof.reset_thms calculationN
    1.34 +      |> Proof.simple_have_thms "" calc
    1.35 +      |> Proof.chain;
    1.36  
    1.37  
    1.38  (* 'also' and 'finally' *)
    1.39  
    1.40 +fun err_if state b msg = if b then raise Proof.STATE (msg, state) else ();
    1.41 +
    1.42  fun calculate final opt_rules print state =
    1.43    let
    1.44 -    fun err_if b msg = if b then raise Proof.STATE (msg, state) else ();
    1.45      val facts = Proof.the_facts state;
    1.46  
    1.47      val eq_prop = op aconv o pairself (#prop o Thm.rep_thm);
    1.48 @@ -140,30 +148,33 @@
    1.49          None => (true, Seq.single facts)
    1.50        | Some thms => (false, Seq.filter (differ thms) (combine thms)))
    1.51    in
    1.52 -    err_if (initial andalso final) "No calculation yet";
    1.53 -    err_if (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
    1.54 -    calculations |> Seq.map (fn calc =>
    1.55 -      (print calc;
    1.56 -        (if final then
    1.57 -          state
    1.58 -          |> reset_calculation
    1.59 -          |> Proof.reset_thms calculationN
    1.60 -          |> Proof.simple_have_thms "" calc
    1.61 -          |> Proof.chain
    1.62 -        else
    1.63 -          state
    1.64 -          |> maintain_calculation calc)))
    1.65 +    err_if state (initial andalso final) "No calculation yet";
    1.66 +    err_if state (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
    1.67 +    calculations |> Seq.map (fn calc => (print calc; state |> maintain_calculation final calc))
    1.68    end;
    1.69  
    1.70  fun also print = calculate false print;
    1.71  fun finally print = calculate true print;
    1.72  
    1.73  
    1.74 -(* 'moreover' *)
    1.75 +(* 'moreover' and 'ultimately' *)
    1.76  
    1.77 -fun moreover print state =
    1.78 -  let val calc = if_none (get_calculation state) [] @ Proof.the_facts state
    1.79 -  in print calc; state |> maintain_calculation calc end;
    1.80 +fun collect final print state =
    1.81 +  let
    1.82 +    val facts = Proof.the_facts state;
    1.83 +    val (initial, thms) =
    1.84 +      (case get_calculation state of
    1.85 +        None => (true, [])
    1.86 +      | Some thms => (false, thms));
    1.87 +    val calc = thms @ facts;
    1.88 +  in
    1.89 +    err_if state (initial andalso final) "No calculation yet";
    1.90 +    print calc;
    1.91 +    state |> maintain_calculation final calc
    1.92 +  end;
    1.93 +
    1.94 +fun moreover print = collect false print;
    1.95 +fun ultimately print = collect true print;
    1.96  
    1.97  
    1.98  
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Sun Mar 26 22:29:33 2000 +0200
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Mar 26 22:31:11 2000 +0200
     2.3 @@ -425,6 +425,10 @@
     2.4    OuterSyntax.command "moreover" "augment calculation by current facts" K.prf_decl
     2.5      (P.marg_comment >> IsarThy.moreover);
     2.6  
     2.7 +val ultimatelyP =
     2.8 +  OuterSyntax.command "ultimately" "augment calculation by current facts, exhibit result"
     2.9 +    K.prf_chain (P.marg_comment >> IsarThy.ultimately);
    2.10 +
    2.11  
    2.12  (* proof navigation *)
    2.13  
    2.14 @@ -642,8 +646,8 @@
    2.15    defP, fixP, letP, caseP, thenP, fromP, withP, noteP, beginP, endP,
    2.16    nextP, qedP, terminal_proofP, immediate_proofP, default_proofP,
    2.17    skip_proofP, forget_proofP, deferP, preferP, applyP, apply_endP,
    2.18 -  proofP, alsoP, finallyP, moreoverP, backP, cannot_undoP,
    2.19 -  clear_undosP, redoP, undos_proofP, undoP, killP,
    2.20 +  proofP, alsoP, finallyP, moreoverP, ultimatelyP, backP,
    2.21 +  cannot_undoP, clear_undosP, redoP, undos_proofP, undoP, killP,
    2.22    (*diagnostic commands*)
    2.23    pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
    2.24    print_syntaxP, print_theoremsP, print_attributesP, print_methodsP,
     3.1 --- a/src/Pure/Isar/isar_thy.ML	Sun Mar 26 22:29:33 2000 +0200
     3.2 +++ b/src/Pure/Isar/isar_thy.ML	Sun Mar 26 22:31:11 2000 +0200
     3.3 @@ -144,6 +144,7 @@
     3.4    val finally_i: (thm list * Comment.interest) option * Comment.text
     3.5      -> Toplevel.transition -> Toplevel.transition
     3.6    val moreover: Comment.text -> Toplevel.transition -> Toplevel.transition
     3.7 +  val ultimately: Comment.text -> Toplevel.transition -> Toplevel.transition
     3.8    val parse_ast_translation: string -> theory -> theory
     3.9    val parse_translation: string -> theory -> theory
    3.10    val print_translation: string -> theory -> theory
    3.11 @@ -456,6 +457,7 @@
    3.12  fun finally x = proof''' (ProofHistory.applys o gen_calc get_thmss Calculation.finally x);
    3.13  fun finally_i x = proof''' (ProofHistory.applys o gen_calc get_thmss_i Calculation.finally x);
    3.14  fun moreover comment = proof''' (ProofHistory.apply o Calculation.moreover);
    3.15 +fun ultimately comment = proof''' (ProofHistory.apply o Calculation.ultimately);
    3.16  
    3.17  end;
    3.18