more self-contained proof elements (material from isar_thy.ML);
authorwenzelm
Tue Sep 13 22:19:34 2005 +0200 (2005-09-13 ago)
changeset 1735026cd3756377a
parent 17349 03fafcdfdfa7
child 17351 f7f2f56fcc28
more self-contained proof elements (material from isar_thy.ML);
tuned;
src/Pure/Isar/calculation.ML
     1.1 --- a/src/Pure/Isar/calculation.ML	Tue Sep 13 22:19:33 2005 +0200
     1.2 +++ b/src/Pure/Isar/calculation.ML	Tue Sep 13 22:19:34 2005 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      ID:         $Id$
     1.5      Author:     Markus Wenzel, TU Muenchen
     1.6  
     1.7 -Support for calculational proofs.
     1.8 +Generic calculational proofs.
     1.9  *)
    1.10  
    1.11  signature CALCULATION =
    1.12 @@ -20,12 +20,13 @@
    1.13    val sym_del_local: Proof.context attribute
    1.14    val symmetric_global: theory attribute
    1.15    val symmetric_local: Proof.context attribute
    1.16 -  val also: thm list option -> (Proof.context -> thm list -> unit)
    1.17 -    -> Proof.state -> Proof.state Seq.seq
    1.18 -  val finally: thm list option -> (Proof.context -> thm list -> unit)
    1.19 -    -> Proof.state -> Proof.state Seq.seq
    1.20 -  val moreover: (Proof.context -> thm list -> unit) -> Proof.state -> Proof.state
    1.21 -  val ultimately: (Proof.context -> thm list -> unit) -> Proof.state -> Proof.state
    1.22 +  val also: (thmref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
    1.23 +  val also_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
    1.24 +  val finally: (thmref * Attrib.src list) list option -> bool ->
    1.25 +    Proof.state -> Proof.state Seq.seq
    1.26 +  val finally_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
    1.27 +  val moreover: bool -> Proof.state -> Proof.state
    1.28 +  val ultimately: bool -> Proof.state -> Proof.state
    1.29  end;
    1.30  
    1.31  structure Calculation: CALCULATION =
    1.32 @@ -80,13 +81,12 @@
    1.33      NONE => NONE
    1.34    | SOME (thms, lev) => if lev = Proof.level state then SOME thms else NONE);
    1.35  
    1.36 -fun put_calculation thms state =
    1.37 -  Proof.map_context
    1.38 -    (LocalCalculation.put (get_local_rules state, SOME (thms, Proof.level state))) state;
    1.39 +val calculationN = "calculation";
    1.40  
    1.41 -fun reset_calculation state =
    1.42 -  Proof.map_context (LocalCalculation.put (get_local_rules state, NONE)) state;
    1.43 -
    1.44 +fun put_calculation calc =
    1.45 +  `Proof.level #-> (fn lev => Proof.map_context
    1.46 +    (LocalCalculation.map (apsnd (K (Option.map (rpair lev) calc)))))
    1.47 +  #> Proof.put_thms (calculationN, calc);
    1.48  
    1.49  
    1.50  (** attributes **)
    1.51 @@ -143,42 +143,37 @@
    1.52  
    1.53  (** proof commands **)
    1.54  
    1.55 +fun err_if state b msg = if b then raise Proof.STATE (msg, state) else ();
    1.56 +
    1.57  fun assert_sane final =
    1.58    if final then Proof.assert_forward else Proof.assert_forward_or_chain;
    1.59  
    1.60 -
    1.61 -(* maintain calculation register *)
    1.62 -
    1.63 -val calculationN = "calculation";
    1.64 +fun maintain_calculation false calc = put_calculation (SOME calc)
    1.65 +  | maintain_calculation true calc = put_calculation NONE #> Proof.chain_facts calc;
    1.66  
    1.67 -fun maintain_calculation false calc state =
    1.68 -      state
    1.69 -      |> put_calculation calc
    1.70 -      |> Proof.put_thms (calculationN, calc)
    1.71 -  | maintain_calculation true calc state =
    1.72 -      state
    1.73 -      |> reset_calculation
    1.74 -      |> Proof.reset_thms calculationN
    1.75 -      |> Proof.simple_note_thms "" calc
    1.76 -      |> Proof.chain;
    1.77 +fun print_calculation false _ _ = ()
    1.78 +  | print_calculation true ctxt calc =
    1.79 +      Pretty.writeln (Pretty.big_list "calculation:" (map (ProofContext.pretty_thm ctxt) calc));
    1.80 +(* FIXME 
    1.81 +      Pretty.writeln (ProofContext.pretty_fact ctxt (calculationN, calc));
    1.82 +*)
    1.83  
    1.84  
    1.85 -(* 'also' and 'finally' *)
    1.86 +(* also and finally *)
    1.87  
    1.88 -fun err_if state b msg = if b then raise Proof.STATE (msg, state) else ();
    1.89 -
    1.90 -fun calculate final opt_rules print state =
    1.91 +fun calculate prep_rules final raw_rules int state =
    1.92    let
    1.93      val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of;
    1.94      val eq_prop = op aconv o pairself (Pattern.eta_contract o strip_assums_concl);
    1.95      fun projection ths th = Library.exists (Library.curry eq_prop th) ths;
    1.96  
    1.97 +    val opt_rules = Option.map (prep_rules state) raw_rules;
    1.98      fun combine ths =
    1.99        (case opt_rules of SOME rules => rules
   1.100        | NONE =>
   1.101            (case ths of [] => NetRules.rules (#1 (get_local_rules state))
   1.102            | th :: _ => NetRules.retrieve (#1 (get_local_rules state)) (strip_assums_concl th)))
   1.103 -      |> Seq.of_list |> Seq.map (Method.multi_resolve ths) |> Seq.flat
   1.104 +      |> Seq.of_list |> Seq.maps (Method.multi_resolve ths)
   1.105        |> Seq.filter (not o projection ths);
   1.106  
   1.107      val facts = Proof.the_facts (assert_sane final state);
   1.108 @@ -189,17 +184,19 @@
   1.109    in
   1.110      err_if state (initial andalso final) "No calculation yet";
   1.111      err_if state (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
   1.112 -    calculations |> Seq.map (fn calc => (print (Proof.context_of state) calc;
   1.113 +    calculations |> Seq.map (fn calc => (print_calculation int (Proof.context_of state) calc;
   1.114          state |> maintain_calculation final calc))
   1.115    end;
   1.116  
   1.117 -fun also print = calculate false print;
   1.118 -fun finally print = calculate true print;
   1.119 +val also = calculate Proof.get_thmss false;
   1.120 +val also_i = calculate (K I) false;
   1.121 +val finally = calculate Proof.get_thmss true;
   1.122 +val finally_i = calculate (K I) true;
   1.123  
   1.124  
   1.125 -(* 'moreover' and 'ultimately' *)
   1.126 +(* moreover and ultimately *)
   1.127  
   1.128 -fun collect final print state =
   1.129 +fun collect final int state =
   1.130    let
   1.131      val facts = Proof.the_facts (assert_sane final state);
   1.132      val (initial, thms) =
   1.133 @@ -209,12 +206,11 @@
   1.134      val calc = thms @ facts;
   1.135    in
   1.136      err_if state (initial andalso final) "No calculation yet";
   1.137 -    print (Proof.context_of state) calc;
   1.138 +    print_calculation int (Proof.context_of state) calc;
   1.139      state |> maintain_calculation final calc
   1.140    end;
   1.141  
   1.142 -fun moreover print = collect false print;
   1.143 -fun ultimately print = collect true print;
   1.144 -
   1.145 +val moreover = collect false;
   1.146 +val ultimately = collect true;
   1.147  
   1.148  end;