src/Pure/Isar/calculation.ML

more robust toplevel_error reporting (NB: Context.proof_of on a stale theory crashes ungracefully);

(*  Title:      Pure/Isar/calculation.ML
    Author:     Markus Wenzel, TU Muenchen

Generic calculational proofs.
*)

signature CALCULATION =
sig
  val print_rules: Proof.context -> unit
  val get_calculation: Proof.state -> thm list option
  val trans_add: attribute
  val trans_del: attribute
  val sym_add: attribute
  val sym_del: attribute
  val symmetric: attribute
  val also: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
  val also_cmd: (Facts.ref * Attrib.src list) list option ->
    bool -> Proof.state -> Proof.state Seq.seq
  val finally: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
  val finally_cmd: (Facts.ref * Attrib.src list) list option -> bool ->
    Proof.state -> Proof.state Seq.seq
  val moreover: bool -> Proof.state -> Proof.state
  val ultimately: bool -> Proof.state -> Proof.state
end;

structure Calculation: CALCULATION =
struct

(** calculation data **)

structure Data = Generic_Data
(
  type T = (thm Item_Net.T * thm list) * (thm list * int) option;
  val empty = ((Thm.elim_rules, []), NONE);
  val extend = I;
  fun merge (((trans1, sym1), _), ((trans2, sym2), _)) =
    ((Item_Net.merge (trans1, trans2), Thm.merge_thms (sym1, sym2)), NONE);
);

val get_rules = #1 o Data.get o Context.Proof;

fun print_rules ctxt =
  let val (trans, sym) = get_rules ctxt in
    [Pretty.big_list "transitivity rules:"
        (map (Display.pretty_thm ctxt) (Item_Net.content trans)),
      Pretty.big_list "symmetry rules:" (map (Display.pretty_thm ctxt) sym)]
    |> Pretty.chunks |> Pretty.writeln
  end;


(* access calculation *)

fun get_calculation state =
  (case #2 (Data.get (Context.Proof (Proof.context_of state))) of
    NONE => NONE
  | SOME (thms, lev) => if lev = Proof.level state then SOME thms else NONE);

val calculationN = "calculation";

fun put_calculation calc =
  `Proof.level #-> (fn lev => Proof.map_context (Context.proof_map
     (Data.map (apsnd (K (Option.map (rpair lev) calc))))))
  #> Proof.put_thms false (calculationN, calc);



(** attributes **)

(* add/del rules *)

val trans_add = Thm.declaration_attribute (Data.map o apfst o apfst o Item_Net.update);
val trans_del = Thm.declaration_attribute (Data.map o apfst o apfst o Item_Net.remove);

val sym_add =
  Thm.declaration_attribute (Data.map o apfst o apsnd o Thm.add_thm)
  #> Context_Rules.elim_query NONE;

val sym_del =
  Thm.declaration_attribute (Data.map o apfst o apsnd o Thm.del_thm)
  #> Context_Rules.rule_del;


(* symmetric *)

val symmetric = Thm.rule_attribute (fn x => fn th =>
  (case Seq.chop 2 (Drule.multi_resolves [th] (#2 (#1 (Data.get x)))) of
    ([th'], _) => Drule.zero_var_indexes th'
  | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
  | _ => raise THM ("symmetric: multiple unifiers", 1, [th])));


(* concrete syntax *)

val _ = Context.>> (Context.map_theory
 (Attrib.setup (Binding.name "trans") (Attrib.add_del trans_add trans_del)
    "declaration of transitivity rule" #>
  Attrib.setup (Binding.name "sym") (Attrib.add_del sym_add sym_del)
    "declaration of symmetry rule" #>
  Attrib.setup (Binding.name "symmetric") (Scan.succeed symmetric)
    "resolution with symmetry rule" #>
  Global_Theory.add_thms
   [((Binding.empty, transitive_thm), [trans_add]),
    ((Binding.empty, symmetric_thm), [sym_add])] #> snd));



(** proof commands **)

fun assert_sane final =
  if final then Proof.assert_forward else Proof.assert_forward_or_chain;

fun maintain_calculation int final calc state =
  let
    val state' = put_calculation (SOME calc) state;
    val ctxt' = Proof.context_of state';
    val _ =
      if int then
        Pretty.writeln
          (Proof_Context.pretty_fact ctxt'
            (Proof_Context.full_name ctxt' (Binding.name calculationN), calc))
      else ();
  in state' |> final ? (put_calculation NONE #> Proof.chain_facts calc) end;


(* also and finally *)

fun calculate prep_rules final raw_rules int state =
  let
    val ctxt = Proof.context_of state;

    val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of;
    val eq_prop = op aconv o pairself (Envir.beta_eta_contract o strip_assums_concl);
    fun projection ths th = exists (curry eq_prop th) ths;

    val opt_rules = Option.map (prep_rules ctxt) raw_rules;
    fun combine ths =
      (case opt_rules of SOME rules => rules
      | NONE =>
          (case ths of
            [] => Item_Net.content (#1 (get_rules ctxt))
          | th :: _ => Item_Net.retrieve (#1 (get_rules ctxt)) (strip_assums_concl th)))
      |> Seq.of_list |> Seq.maps (Drule.multi_resolve ths)
      |> Seq.filter (not o projection ths);

    val facts = Proof.the_facts (assert_sane final state);
    val (initial, calculations) =
      (case get_calculation state of
        NONE => (true, Seq.single facts)
      | SOME calc => (false, Seq.map single (combine (calc @ facts))));

    val _ = initial andalso final andalso error "No calculation yet";
    val _ = initial andalso is_some opt_rules andalso
      error "Initial calculation -- no rules to be given";
  in
    calculations |> Seq.map (fn calc => maintain_calculation int final calc state)
  end;

val also = calculate (K I) false;
val also_cmd = calculate Attrib.eval_thms false;
val finally = calculate (K I) true;
val finally_cmd = calculate Attrib.eval_thms true;


(* moreover and ultimately *)

fun collect final int state =
  let
    val facts = Proof.the_facts (assert_sane final state);
    val (initial, thms) =
      (case get_calculation state of
        NONE => (true, [])
      | SOME thms => (false, thms));
    val calc = thms @ facts;
    val _ = initial andalso final andalso error "No calculation yet";
  in maintain_calculation int final calc state end;

val moreover = collect false;
val ultimately = collect true;

end;