1.1 --- a/src/Pure/Isar/calculation.ML	Fri May 21 21:28:31 2010 +0200
     1.2 +++ b/src/Pure/Isar/calculation.ML	Fri May 21 22:08:13 2010 +0200
     1.3 @@ -14,7 +14,8 @@
     1.4    val sym_del: attribute
     1.5    val symmetric: attribute
     1.6    val also: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
     1.7 -  val also_cmd: (Facts.ref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
     1.8 +  val also_cmd: (Facts.ref * Attrib.src list) list option ->
     1.9 +    bool -> Proof.state -> Proof.state Seq.seq
    1.10    val finally: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
    1.11    val finally_cmd: (Facts.ref * Attrib.src list) list option -> bool ->
    1.12      Proof.state -> Proof.state Seq.seq
    1.13 @@ -27,7 +28,7 @@
    1.14  
    1.15  (** calculation data **)
    1.16  
    1.17 -structure CalculationData = Generic_Data
    1.18 +structure Data = Generic_Data
    1.19  (
    1.20    type T = (thm Item_Net.T * thm list) * (thm list * int) option;
    1.21    val empty = ((Thm.elim_rules, []), NONE);
    1.22 @@ -37,7 +38,7 @@
    1.23  );
    1.24  
    1.25  fun print_rules ctxt =
    1.26 -  let val ((trans, sym), _) = CalculationData.get (Context.Proof ctxt) in
    1.27 +  let val ((trans, sym), _) = Data.get (Context.Proof ctxt) in
    1.28      [Pretty.big_list "transitivity rules:"
    1.29          (map (Display.pretty_thm ctxt) (Item_Net.content trans)),
    1.30        Pretty.big_list "symmetry rules:" (map (Display.pretty_thm ctxt) sym)]
    1.31 @@ -48,7 +49,7 @@
    1.32  (* access calculation *)
    1.33  
    1.34  fun get_calculation state =
    1.35 -  (case #2 (CalculationData.get (Context.Proof (Proof.context_of state))) of
    1.36 +  (case #2 (Data.get (Context.Proof (Proof.context_of state))) of
    1.37      NONE => NONE
    1.38    | SOME (thms, lev) => if lev = Proof.level state then SOME thms else NONE);
    1.39  
    1.40 @@ -56,7 +57,7 @@
    1.41  
    1.42  fun put_calculation calc =
    1.43    `Proof.level #-> (fn lev => Proof.map_context (Context.proof_map
    1.44 -     (CalculationData.map (apsnd (K (Option.map (rpair lev) calc))))))
    1.45 +     (Data.map (apsnd (K (Option.map (rpair lev) calc))))))
    1.46    #> Proof.put_thms false (calculationN, calc);
    1.47  
    1.48  
    1.49 @@ -65,22 +66,22 @@
    1.50  
    1.51  (* add/del rules *)
    1.52  
    1.53 -val trans_add = Thm.declaration_attribute (CalculationData.map o apfst o apfst o Item_Net.update);
    1.54 -val trans_del = Thm.declaration_attribute (CalculationData.map o apfst o apfst o Item_Net.remove);
    1.55 +val trans_add = Thm.declaration_attribute (Data.map o apfst o apfst o Item_Net.update);
    1.56 +val trans_del = Thm.declaration_attribute (Data.map o apfst o apfst o Item_Net.remove);
    1.57  
    1.58  val sym_add =
    1.59 -  Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.add_thm)
    1.60 +  Thm.declaration_attribute (Data.map o apfst o apsnd o Thm.add_thm)
    1.61    #> Context_Rules.elim_query NONE;
    1.62  
    1.63  val sym_del =
    1.64 -  Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.del_thm)
    1.65 +  Thm.declaration_attribute (Data.map o apfst o apsnd o Thm.del_thm)
    1.66    #> Context_Rules.rule_del;
    1.67  
    1.68  
    1.69  (* symmetric *)
    1.70  
    1.71  val symmetric = Thm.rule_attribute (fn x => fn th =>
    1.72 -  (case Seq.chop 2 (Drule.multi_resolves [th] (#2 (#1 (CalculationData.get x)))) of
    1.73 +  (case Seq.chop 2 (Drule.multi_resolves [th] (#2 (#1 (Data.get x)))) of
    1.74      ([th'], _) => Drule.zero_var_indexes th'
    1.75    | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
    1.76    | _ => raise THM ("symmetric: multiple unifiers", 1, [th])));
    1.77 @@ -103,28 +104,31 @@
    1.78  
    1.79  (** proof commands **)
    1.80  
    1.81 -fun err_if b msg = if b then error msg else ();
    1.82 -
    1.83  fun assert_sane final =
    1.84    if final then Proof.assert_forward else Proof.assert_forward_or_chain;
    1.85  
    1.86 -fun maintain_calculation false calc = put_calculation (SOME calc)
    1.87 -  | maintain_calculation true calc = put_calculation NONE #> Proof.chain_facts calc;
    1.88 -
    1.89 -fun print_calculation false _ _ = ()
    1.90 -  | print_calculation true ctxt calc = Pretty.writeln
    1.91 -      (ProofContext.pretty_fact ctxt (ProofContext.full_name ctxt (Binding.name calculationN), calc));
    1.92 +fun maintain_calculation int final calc state =
    1.93 +  let
    1.94 +    val state' = put_calculation (SOME calc) state;
    1.95 +    val ctxt' = Proof.context_of state';
    1.96 +    val _ =
    1.97 +      if int then
    1.98 +        Pretty.writeln
    1.99 +          (ProofContext.pretty_fact ctxt'
   1.100 +            (ProofContext.full_name ctxt' (Binding.name calculationN), calc))
   1.101 +      else ();
   1.102 +  in state' |> final ? (put_calculation NONE #> Proof.chain_facts calc) end;
   1.103  
   1.104  
   1.105  (* also and finally *)
   1.106  
   1.107 -val get_rules = #1 o CalculationData.get o Context.Proof o Proof.context_of;
   1.108 +val get_rules = #1 o Data.get o Context.Proof o Proof.context_of;
   1.109  
   1.110  fun calculate prep_rules final raw_rules int state =
   1.111    let
   1.112      val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of;
   1.113      val eq_prop = op aconv o pairself (Envir.beta_eta_contract o strip_assums_concl);
   1.114 -    fun projection ths th = Library.exists (Library.curry eq_prop th) ths;
   1.115 +    fun projection ths th = exists (curry eq_prop th) ths;
   1.116  
   1.117      val opt_rules = Option.map (prep_rules state) raw_rules;
   1.118      fun combine ths =
   1.119 @@ -141,11 +145,12 @@
   1.120        (case get_calculation state of
   1.121          NONE => (true, Seq.single facts)
   1.122        | SOME calc => (false, Seq.map single (combine (calc @ facts))));
   1.123 +
   1.124 +    val _ = initial andalso final andalso error "No calculation yet";
   1.125 +    val _ = initial andalso is_some opt_rules andalso
   1.126 +      error "Initial calculation -- no rules to be given";
   1.127    in
   1.128 -    err_if (initial andalso final) "No calculation yet";
   1.129 -    err_if (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
   1.130 -    calculations |> Seq.map (fn calc => (print_calculation int (Proof.context_of state) calc;
   1.131 -        state |> maintain_calculation final calc))
   1.132 +    calculations |> Seq.map (fn calc => maintain_calculation int final calc state)
   1.133    end;
   1.134  
   1.135  val also = calculate (K I) false;
   1.136 @@ -164,11 +169,8 @@
   1.137          NONE => (true, [])
   1.138        | SOME thms => (false, thms));
   1.139      val calc = thms @ facts;
   1.140 -  in
   1.141 -    err_if (initial andalso final) "No calculation yet";
   1.142 -    print_calculation int (Proof.context_of state) calc;
   1.143 -    state |> maintain_calculation final calc
   1.144 -  end;
   1.145 +    val _ = initial andalso final andalso error "No calculation yet";
   1.146 +  in maintain_calculation int final calc state end;
   1.147  
   1.148  val moreover = collect false;
   1.149  val ultimately = collect true;