1 (* Title: Pure/Isar/calculation.ML
3 Author: Markus Wenzel, TU Muenchen
5 Generic calculational proofs.
8 signature CALCULATION =
10 val print_rules: Context.generic -> unit
11 val get_calculation: Proof.state -> thm list option
12 val trans_add: Context.generic attribute
13 val trans_del: Context.generic attribute
14 val sym_add: Context.generic attribute
15 val sym_del: Context.generic attribute
16 val symmetric: Context.generic attribute
17 val also: (thmref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
18 val also_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
19 val finally: (thmref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
20 val finally_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
21 val moreover: bool -> Proof.state -> Proof.state
22 val ultimately: bool -> Proof.state -> Proof.state
25 structure Calculation: CALCULATION =
28 (** calculation data **)
30 structure CalculationData = GenericDataFun
32 val name = "Isar/calculation";
33 type T = (thm NetRules.T * thm list) * (thm list * int) option;
34 val empty = ((NetRules.elim, []), NONE);
37 fun merge _ (((trans1, sym1), _), ((trans2, sym2), _)) =
38 ((NetRules.merge (trans1, trans2), Drule.merge_rules (sym1, sym2)), NONE);
40 fun print generic ((trans, sym), _) =
41 let val ctxt = Context.proof_of generic in
42 [Pretty.big_list "transitivity rules:"
43 (map (ProofContext.pretty_thm ctxt) (NetRules.rules trans)),
44 Pretty.big_list "symmetry rules:" (map (ProofContext.pretty_thm ctxt) sym)]
45 |> Pretty.chunks |> Pretty.writeln
49 val _ = Context.add_setup [CalculationData.init];
50 val print_rules = CalculationData.print;
53 (* access calculation *)
55 fun get_calculation state =
56 (case #2 (CalculationData.get (Context.Proof (Proof.context_of state))) of
58 | SOME (thms, lev) => if lev = Proof.level state then SOME thms else NONE);
60 val calculationN = "calculation";
62 fun put_calculation calc =
63 `Proof.level #-> (fn lev =>
64 Proof.map_context (Context.the_proof o
65 CalculationData.map (apsnd (K (Option.map (rpair lev) calc))) o Context.Proof))
66 #> Proof.put_thms (calculationN, calc);
74 val trans_add = Attrib.declaration (CalculationData.map o apfst o apfst o NetRules.insert);
75 val trans_del = Attrib.declaration (CalculationData.map o apfst o apfst o NetRules.delete);
78 Attrib.declaration (CalculationData.map o apfst o apsnd o Drule.add_rule)
79 #> ContextRules.elim_query NONE;
81 Attrib.declaration (CalculationData.map o apfst o apsnd o Drule.del_rule)
82 #> ContextRules.rule_del;
87 val symmetric = Attrib.rule (fn x => fn th =>
88 (case Seq.chop (2, Drule.multi_resolves [th] (#2 (#1 (CalculationData.get x)))) of
90 | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
91 | _ => raise THM ("symmetric: multiple unifiers", 1, [th])));
96 val trans_att = Attrib.add_del_args trans_add trans_del;
97 val sym_att = Attrib.add_del_args sym_add sym_del;
99 val _ = Context.add_setup
100 [Attrib.add_attributes
101 [("trans", Attrib.common trans_att, "declaration of transitivity rule"),
102 ("sym", Attrib.common sym_att, "declaration of symmetry rule"),
103 ("symmetric", Attrib.common (Attrib.no_args symmetric), "resolution with symmetry rule")],
104 snd o PureThy.add_thms
105 [(("", transitive_thm), [Attrib.theory trans_add]),
106 (("", symmetric_thm), [Attrib.theory sym_add])]];
110 (** proof commands **)
112 fun err_if state b msg = if b then raise Proof.STATE (msg, state) else ();
114 fun assert_sane final =
115 if final then Proof.assert_forward else Proof.assert_forward_or_chain;
117 fun maintain_calculation false calc = put_calculation (SOME calc)
118 | maintain_calculation true calc = put_calculation NONE #> Proof.chain_facts calc;
120 fun print_calculation false _ _ = ()
121 | print_calculation true ctxt calc =
122 Pretty.writeln (ProofContext.pretty_fact ctxt (calculationN, calc));
125 (* also and finally *)
127 val get_rules = #1 o CalculationData.get o Context.Proof o Proof.context_of;
129 fun calculate prep_rules final raw_rules int state =
131 val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of;
132 val eq_prop = op aconv o pairself (Pattern.eta_contract o strip_assums_concl);
133 fun projection ths th = Library.exists (Library.curry eq_prop th) ths;
135 val opt_rules = Option.map (prep_rules state) raw_rules;
137 (case opt_rules of SOME rules => rules
139 (case ths of [] => NetRules.rules (#1 (get_rules state))
140 | th :: _ => NetRules.retrieve (#1 (get_rules state)) (strip_assums_concl th)))
141 |> Seq.of_list |> Seq.maps (Drule.multi_resolve ths)
142 |> Seq.filter (not o projection ths);
144 val facts = Proof.the_facts (assert_sane final state);
145 val (initial, calculations) =
146 (case get_calculation state of
147 NONE => (true, Seq.single facts)
148 | SOME calc => (false, Seq.map single (combine (calc @ facts))));
150 err_if state (initial andalso final) "No calculation yet";
151 err_if state (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
152 calculations |> Seq.map (fn calc => (print_calculation int (Proof.context_of state) calc;
153 state |> maintain_calculation final calc))
156 val also = calculate Proof.get_thmss false;
157 val also_i = calculate (K I) false;
158 val finally = calculate Proof.get_thmss true;
159 val finally_i = calculate (K I) true;
162 (* moreover and ultimately *)
164 fun collect final int state =
166 val facts = Proof.the_facts (assert_sane final state);
167 val (initial, thms) =
168 (case get_calculation state of
170 | SOME thms => (false, thms));
171 val calc = thms @ facts;
173 err_if state (initial andalso final) "No calculation yet";
174 print_calculation int (Proof.context_of state) calc;
175 state |> maintain_calculation final calc
178 val moreover = collect false;
179 val ultimately = collect true;