src/Pure/Isar/calculation.ML
changeset 8588 b7c3f264f8ac
parent 8562 ce0e2b8e8844
child 8634 3f34637cb9c0
     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