wenzelm@6778: (*  Title:      Pure/Isar/calculation.ML
wenzelm@6778:     ID:         $Id$
wenzelm@6778:     Author:     Markus Wenzel, TU Muenchen
wenzelm@6778: 
wenzelm@17350: Generic calculational proofs.
wenzelm@6778: *)
wenzelm@6778: 
wenzelm@6778: signature CALCULATION =
wenzelm@6778: sig
wenzelm@21506:   val print_rules: Proof.context -> unit
wenzelm@16571:   val get_calculation: Proof.state -> thm list option
wenzelm@18728:   val trans_add: attribute
wenzelm@18728:   val trans_del: attribute
wenzelm@18728:   val sym_add: attribute
wenzelm@18728:   val sym_del: attribute
wenzelm@18728:   val symmetric: attribute
wenzelm@17350:   val also: (thmref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
wenzelm@17350:   val also_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
wenzelm@22573:   val finally_: (thmref * Attrib.src list) list option -> bool ->
wenzelm@22573:     Proof.state -> Proof.state Seq.seq
wenzelm@17350:   val finally_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
wenzelm@17350:   val moreover: bool -> Proof.state -> Proof.state
wenzelm@17350:   val ultimately: bool -> Proof.state -> Proof.state
wenzelm@6778: end;
wenzelm@6778: 
wenzelm@6778: structure Calculation: CALCULATION =
wenzelm@6778: struct
wenzelm@6778: 
wenzelm@18637: (** calculation data **)
wenzelm@6778: 
wenzelm@18637: structure CalculationData = GenericDataFun
wenzelm@18637: (
wenzelm@12379:   type T = (thm NetRules.T * thm list) * (thm list * int) option;
wenzelm@18637:   val empty = ((NetRules.elim, []), NONE);
wenzelm@18637:   val extend = I;
wenzelm@6778: 
wenzelm@18637:   fun merge _ (((trans1, sym1), _), ((trans2, sym2), _)) =
wenzelm@18637:     ((NetRules.merge (trans1, trans2), Drule.merge_rules (sym1, sym2)), NONE);
wenzelm@18637: );
wenzelm@18637: 
wenzelm@22846: fun print_rules ctxt =
wenzelm@22846:   let val ((trans, sym), _) = CalculationData.get (Context.Proof ctxt) in
wenzelm@22846:     [Pretty.big_list "transitivity rules:"
wenzelm@22846:         (map (ProofContext.pretty_thm ctxt) (NetRules.rules trans)),
wenzelm@22846:       Pretty.big_list "symmetry rules:" (map (ProofContext.pretty_thm ctxt) sym)]
wenzelm@22846:     |> Pretty.chunks |> Pretty.writeln
wenzelm@22846:   end;
wenzelm@6778: 
wenzelm@6778: 
wenzelm@6778: (* access calculation *)
wenzelm@6778: 
wenzelm@6778: fun get_calculation state =
wenzelm@18637:   (case #2 (CalculationData.get (Context.Proof (Proof.context_of state))) of
skalberg@15531:     NONE => NONE
skalberg@15531:   | SOME (thms, lev) => if lev = Proof.level state then SOME thms else NONE);
wenzelm@6778: 
wenzelm@17350: val calculationN = "calculation";
wenzelm@6778: 
wenzelm@17350: fun put_calculation calc =
wenzelm@18728:   `Proof.level #-> (fn lev => Proof.map_context (Context.proof_map
wenzelm@18728:      (CalculationData.map (apsnd (K (Option.map (rpair lev) calc))))))
wenzelm@21445:   #> Proof.put_thms (calculationN, calc);
wenzelm@6778: 
wenzelm@6778: 
wenzelm@18637: 
wenzelm@6778: (** attributes **)
wenzelm@6778: 
wenzelm@12379: (* add/del rules *)
wenzelm@12379: 
wenzelm@18728: val trans_add = Thm.declaration_attribute (CalculationData.map o apfst o apfst o NetRules.insert);
wenzelm@18728: val trans_del = Thm.declaration_attribute (CalculationData.map o apfst o apfst o NetRules.delete);
wenzelm@6778: 
wenzelm@18637: val sym_add =
wenzelm@18728:   Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Drule.add_rule)
wenzelm@18637:   #> ContextRules.elim_query NONE;
wenzelm@18637: val sym_del =
wenzelm@18728:   Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Drule.del_rule)
wenzelm@18637:   #> ContextRules.rule_del;
wenzelm@12379: 
wenzelm@12379: 
wenzelm@18637: (* symmetric *)
wenzelm@12379: 
wenzelm@18728: val symmetric = Thm.rule_attribute (fn x => fn th =>
wenzelm@19861:   (case Seq.chop 2 (Drule.multi_resolves [th] (#2 (#1 (CalculationData.get x)))) of
wenzelm@20898:     ([th'], _) => Drule.zero_var_indexes th'
wenzelm@12379:   | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
wenzelm@12379:   | _ => raise THM ("symmetric: multiple unifiers", 1, [th])));
wenzelm@12379: 
wenzelm@6778: 
wenzelm@6778: (* concrete syntax *)
wenzelm@6778: 
wenzelm@18637: val trans_att = Attrib.add_del_args trans_add trans_del;
wenzelm@18637: val sym_att = Attrib.add_del_args sym_add sym_del;
wenzelm@12379: 
wenzelm@15801: val _ = Context.add_setup
wenzelm@18708:  (Attrib.add_attributes
wenzelm@18728:    [("trans", trans_att, "declaration of transitivity rule"),
wenzelm@18728:     ("sym", sym_att, "declaration of symmetry rule"),
wenzelm@18728:     ("symmetric", Attrib.no_args symmetric, "resolution with symmetry rule")] #>
wenzelm@18708:   PureThy.add_thms
wenzelm@18728:    [(("", transitive_thm), [trans_add]),
wenzelm@18728:     (("", symmetric_thm), [sym_add])] #> snd);
wenzelm@15801: 
wenzelm@6778: 
wenzelm@6787: 
wenzelm@6778: (** proof commands **)
wenzelm@6778: 
wenzelm@18678: fun err_if b msg = if b then error msg else ();
wenzelm@17350: 
wenzelm@14555: fun assert_sane final =
wenzelm@14555:   if final then Proof.assert_forward else Proof.assert_forward_or_chain;
wenzelm@14555: 
wenzelm@17350: fun maintain_calculation false calc = put_calculation (SOME calc)
wenzelm@17350:   | maintain_calculation true calc = put_calculation NONE #> Proof.chain_facts calc;
wenzelm@6778: 
wenzelm@17350: fun print_calculation false _ _ = ()
wenzelm@17350:   | print_calculation true ctxt calc =
wenzelm@17350:       Pretty.writeln (ProofContext.pretty_fact ctxt (calculationN, calc));
wenzelm@8562: 
wenzelm@8562: 
wenzelm@17350: (* also and finally *)
wenzelm@8562: 
wenzelm@18637: val get_rules = #1 o CalculationData.get o Context.Proof o Proof.context_of;
wenzelm@18637: 
wenzelm@17350: fun calculate prep_rules final raw_rules int state =
wenzelm@6778:   let
wenzelm@12805:     val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of;
wenzelm@18947:     val eq_prop = op aconv o pairself (Envir.beta_eta_contract o strip_assums_concl);
wenzelm@11097:     fun projection ths th = Library.exists (Library.curry eq_prop th) ths;
wenzelm@8300: 
wenzelm@17350:     val opt_rules = Option.map (prep_rules state) raw_rules;
wenzelm@11097:     fun combine ths =
skalberg@15531:       (case opt_rules of SOME rules => rules
skalberg@15531:       | NONE =>
wenzelm@18637:           (case ths of [] => NetRules.rules (#1 (get_rules state))
wenzelm@18637:           | th :: _ => NetRules.retrieve (#1 (get_rules state)) (strip_assums_concl th)))
wenzelm@18223:       |> Seq.of_list |> Seq.maps (Drule.multi_resolve ths)
wenzelm@11097:       |> Seq.filter (not o projection ths);
wenzelm@7414: 
wenzelm@14555:     val facts = Proof.the_facts (assert_sane final state);
wenzelm@6903:     val (initial, calculations) =
wenzelm@6778:       (case get_calculation state of
skalberg@15531:         NONE => (true, Seq.single facts)
skalberg@15531:       | SOME calc => (false, Seq.map single (combine (calc @ facts))));
wenzelm@6778:   in
wenzelm@18678:     err_if (initial andalso final) "No calculation yet";
wenzelm@18678:     err_if (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
wenzelm@17350:     calculations |> Seq.map (fn calc => (print_calculation int (Proof.context_of state) calc;
wenzelm@12055:         state |> maintain_calculation final calc))
wenzelm@6778:   end;
wenzelm@6778: 
wenzelm@17350: val also = calculate Proof.get_thmss false;
wenzelm@17350: val also_i = calculate (K I) false;
wenzelm@22573: val finally_ = calculate Proof.get_thmss true;
wenzelm@17350: val finally_i = calculate (K I) true;
wenzelm@6778: 
wenzelm@6778: 
wenzelm@17350: (* moreover and ultimately *)
wenzelm@8562: 
wenzelm@17350: fun collect final int state =
wenzelm@8588:   let
wenzelm@14555:     val facts = Proof.the_facts (assert_sane final state);
wenzelm@8588:     val (initial, thms) =
wenzelm@8588:       (case get_calculation state of
skalberg@15531:         NONE => (true, [])
skalberg@15531:       | SOME thms => (false, thms));
wenzelm@8588:     val calc = thms @ facts;
wenzelm@8588:   in
wenzelm@18678:     err_if (initial andalso final) "No calculation yet";
wenzelm@17350:     print_calculation int (Proof.context_of state) calc;
wenzelm@8588:     state |> maintain_calculation final calc
wenzelm@8588:   end;
wenzelm@8588: 
wenzelm@17350: val moreover = collect false;
wenzelm@17350: val ultimately = collect true;
wenzelm@8562: 
wenzelm@6778: end;