wenzelm@6778
|
1 |
(* Title: Pure/Isar/calculation.ML
|
wenzelm@6778
|
2 |
ID: $Id$
|
wenzelm@6778
|
3 |
Author: Markus Wenzel, TU Muenchen
|
wenzelm@6778
|
4 |
|
wenzelm@6778
|
5 |
Support for calculational proofs.
|
wenzelm@6778
|
6 |
*)
|
wenzelm@6778
|
7 |
|
wenzelm@6778
|
8 |
signature CALCULATION =
|
wenzelm@6778
|
9 |
sig
|
wenzelm@6778
|
10 |
val print_global_rules: theory -> unit
|
wenzelm@6778
|
11 |
val print_local_rules: Proof.context -> unit
|
wenzelm@6778
|
12 |
val trans_add_global: theory attribute
|
wenzelm@6778
|
13 |
val trans_del_global: theory attribute
|
wenzelm@6778
|
14 |
val trans_add_local: Proof.context attribute
|
wenzelm@6778
|
15 |
val trans_del_local: Proof.context attribute
|
wenzelm@12379
|
16 |
val sym_add_global: theory attribute
|
wenzelm@12379
|
17 |
val sym_del_global: theory attribute
|
wenzelm@12379
|
18 |
val sym_add_local: Proof.context attribute
|
wenzelm@12379
|
19 |
val sym_del_local: Proof.context attribute
|
wenzelm@12379
|
20 |
val symmetric_global: theory attribute
|
wenzelm@12379
|
21 |
val symmetric_local: Proof.context attribute
|
wenzelm@12055
|
22 |
val also: thm list option -> (Proof.context -> thm list -> unit)
|
wenzelm@12055
|
23 |
-> Proof.state -> Proof.state Seq.seq
|
wenzelm@12055
|
24 |
val finally: thm list option -> (Proof.context -> thm list -> unit)
|
wenzelm@12055
|
25 |
-> Proof.state -> Proof.state Seq.seq
|
wenzelm@12055
|
26 |
val moreover: (Proof.context -> thm list -> unit) -> Proof.state -> Proof.state
|
wenzelm@12055
|
27 |
val ultimately: (Proof.context -> thm list -> unit) -> Proof.state -> Proof.state
|
wenzelm@6778
|
28 |
end;
|
wenzelm@6778
|
29 |
|
wenzelm@6778
|
30 |
structure Calculation: CALCULATION =
|
wenzelm@6778
|
31 |
struct
|
wenzelm@6778
|
32 |
|
wenzelm@6778
|
33 |
(** global and local calculation data **)
|
wenzelm@6778
|
34 |
|
wenzelm@8300
|
35 |
(* theory data kind 'Isar/calculation' *)
|
wenzelm@6778
|
36 |
|
wenzelm@12379
|
37 |
fun print_rules prt x (trans, sym) =
|
wenzelm@12379
|
38 |
[Pretty.big_list "transitivity rules:" (map (prt x) (NetRules.rules trans)),
|
wenzelm@12379
|
39 |
Pretty.big_list "symmetry rules:" (map (prt x) sym)]
|
wenzelm@12379
|
40 |
|> Pretty.chunks |> Pretty.writeln;
|
wenzelm@6778
|
41 |
|
wenzelm@6778
|
42 |
structure GlobalCalculationArgs =
|
wenzelm@6778
|
43 |
struct
|
wenzelm@6778
|
44 |
val name = "Isar/calculation";
|
wenzelm@12379
|
45 |
type T = thm NetRules.T * thm list
|
wenzelm@6778
|
46 |
|
wenzelm@12379
|
47 |
val empty = (NetRules.elim, []);
|
wenzelm@6778
|
48 |
val copy = I;
|
wenzelm@6778
|
49 |
val prep_ext = I;
|
wenzelm@12379
|
50 |
fun merge ((trans1, sym1), (trans2, sym2)) =
|
wenzelm@12379
|
51 |
(NetRules.merge (trans1, trans2), Drule.merge_rules (sym1, sym2));
|
wenzelm@12055
|
52 |
val print = print_rules Display.pretty_thm_sg;
|
wenzelm@6778
|
53 |
end;
|
wenzelm@6778
|
54 |
|
wenzelm@6778
|
55 |
structure GlobalCalculation = TheoryDataFun(GlobalCalculationArgs);
|
wenzelm@15801
|
56 |
val _ = Context.add_setup [GlobalCalculation.init];
|
wenzelm@6778
|
57 |
val print_global_rules = GlobalCalculation.print;
|
wenzelm@6778
|
58 |
|
wenzelm@6778
|
59 |
|
wenzelm@6778
|
60 |
(* proof data kind 'Isar/calculation' *)
|
wenzelm@6778
|
61 |
|
wenzelm@6778
|
62 |
structure LocalCalculationArgs =
|
wenzelm@6778
|
63 |
struct
|
wenzelm@6778
|
64 |
val name = "Isar/calculation";
|
wenzelm@12379
|
65 |
type T = (thm NetRules.T * thm list) * (thm list * int) option;
|
wenzelm@6778
|
66 |
|
skalberg@15531
|
67 |
fun init thy = (GlobalCalculation.get thy, NONE);
|
wenzelm@12055
|
68 |
fun print ctxt (rs, _) = print_rules ProofContext.pretty_thm ctxt rs;
|
wenzelm@6778
|
69 |
end;
|
wenzelm@6778
|
70 |
|
wenzelm@6778
|
71 |
structure LocalCalculation = ProofDataFun(LocalCalculationArgs);
|
wenzelm@15801
|
72 |
val _ = Context.add_setup [LocalCalculation.init];
|
wenzelm@13371
|
73 |
val get_local_rules = #1 o LocalCalculation.get o Proof.context_of;
|
wenzelm@6778
|
74 |
val print_local_rules = LocalCalculation.print;
|
wenzelm@6778
|
75 |
|
wenzelm@6778
|
76 |
|
wenzelm@6778
|
77 |
(* access calculation *)
|
wenzelm@6778
|
78 |
|
wenzelm@6778
|
79 |
fun get_calculation state =
|
wenzelm@13371
|
80 |
(case #2 (LocalCalculation.get (Proof.context_of state)) of
|
skalberg@15531
|
81 |
NONE => NONE
|
skalberg@15531
|
82 |
| SOME (thms, lev) => if lev = Proof.level state then SOME thms else NONE);
|
wenzelm@6778
|
83 |
|
wenzelm@7414
|
84 |
fun put_calculation thms state =
|
wenzelm@13371
|
85 |
Proof.map_context
|
skalberg@15531
|
86 |
(LocalCalculation.put (get_local_rules state, SOME (thms, Proof.level state))) state;
|
wenzelm@6778
|
87 |
|
wenzelm@6787
|
88 |
fun reset_calculation state =
|
skalberg@15531
|
89 |
Proof.map_context (LocalCalculation.put (get_local_rules state, NONE)) state;
|
wenzelm@6787
|
90 |
|
wenzelm@6778
|
91 |
|
wenzelm@6778
|
92 |
|
wenzelm@6778
|
93 |
(** attributes **)
|
wenzelm@6778
|
94 |
|
wenzelm@12379
|
95 |
(* add/del rules *)
|
wenzelm@6778
|
96 |
|
wenzelm@12379
|
97 |
fun global_att f (x, thm) = (GlobalCalculation.map (f thm) x, thm);
|
wenzelm@12379
|
98 |
fun local_att f (x, thm) = (LocalCalculation.map (apfst (f thm)) x, thm);
|
wenzelm@6778
|
99 |
|
wenzelm@12379
|
100 |
val trans_add_global = global_att (apfst o NetRules.insert);
|
wenzelm@12379
|
101 |
val trans_del_global = global_att (apfst o NetRules.delete);
|
wenzelm@12379
|
102 |
val trans_add_local = local_att (apfst o NetRules.insert);
|
wenzelm@12379
|
103 |
val trans_del_local = local_att (apfst o NetRules.delete);
|
wenzelm@12379
|
104 |
|
skalberg@15531
|
105 |
val sym_add_global = global_att (apsnd o Drule.add_rule) o ContextRules.elim_query_global NONE;
|
wenzelm@12402
|
106 |
val sym_del_global = global_att (apsnd o Drule.del_rule) o ContextRules.rule_del_global;
|
skalberg@15531
|
107 |
val sym_add_local = local_att (apsnd o Drule.add_rule) o ContextRules.elim_query_local NONE;
|
wenzelm@12402
|
108 |
val sym_del_local = local_att (apsnd o Drule.del_rule) o ContextRules.rule_del_local;
|
wenzelm@12379
|
109 |
|
wenzelm@12379
|
110 |
|
wenzelm@12379
|
111 |
(* symmetry *)
|
wenzelm@12379
|
112 |
|
wenzelm@12379
|
113 |
fun gen_symmetric get_sym = Drule.rule_attribute (fn x => fn th =>
|
wenzelm@12379
|
114 |
(case Seq.chop (2, Method.multi_resolves [th] (get_sym x)) of
|
wenzelm@12379
|
115 |
([th'], _) => th'
|
wenzelm@12379
|
116 |
| ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
|
wenzelm@12379
|
117 |
| _ => raise THM ("symmetric: multiple unifiers", 1, [th])));
|
wenzelm@12379
|
118 |
|
wenzelm@12379
|
119 |
val symmetric_global = gen_symmetric (#2 o GlobalCalculation.get);
|
wenzelm@12379
|
120 |
val symmetric_local = gen_symmetric (#2 o #1 o LocalCalculation.get);
|
wenzelm@6778
|
121 |
|
wenzelm@6778
|
122 |
|
wenzelm@6778
|
123 |
(* concrete syntax *)
|
wenzelm@6778
|
124 |
|
wenzelm@6778
|
125 |
val trans_attr =
|
wenzelm@8634
|
126 |
(Attrib.add_del_args trans_add_global trans_del_global,
|
wenzelm@8634
|
127 |
Attrib.add_del_args trans_add_local trans_del_local);
|
wenzelm@6778
|
128 |
|
wenzelm@12379
|
129 |
val sym_attr =
|
wenzelm@12379
|
130 |
(Attrib.add_del_args sym_add_global sym_del_global,
|
wenzelm@12379
|
131 |
Attrib.add_del_args sym_add_local sym_del_local);
|
wenzelm@12379
|
132 |
|
wenzelm@15801
|
133 |
val _ = Context.add_setup
|
wenzelm@15801
|
134 |
[Attrib.add_attributes
|
wenzelm@15801
|
135 |
[("trans", trans_attr, "declaration of transitivity rule"),
|
wenzelm@15801
|
136 |
("sym", sym_attr, "declaration of symmetry rule"),
|
wenzelm@15801
|
137 |
("symmetric", (Attrib.no_args symmetric_global, Attrib.no_args symmetric_local),
|
wenzelm@15801
|
138 |
"resolution with symmetry rule")],
|
wenzelm@15801
|
139 |
#1 o PureThy.add_thms
|
wenzelm@15801
|
140 |
[(("", transitive_thm), [trans_add_global]),
|
wenzelm@15801
|
141 |
(("", symmetric_thm), [sym_add_global])]];
|
wenzelm@15801
|
142 |
|
wenzelm@6778
|
143 |
|
wenzelm@6787
|
144 |
|
wenzelm@6778
|
145 |
(** proof commands **)
|
wenzelm@6778
|
146 |
|
wenzelm@14555
|
147 |
fun assert_sane final =
|
wenzelm@14555
|
148 |
if final then Proof.assert_forward else Proof.assert_forward_or_chain;
|
wenzelm@14555
|
149 |
|
wenzelm@14555
|
150 |
|
wenzelm@8588
|
151 |
(* maintain calculation register *)
|
wenzelm@8562
|
152 |
|
wenzelm@6778
|
153 |
val calculationN = "calculation";
|
wenzelm@6778
|
154 |
|
wenzelm@8588
|
155 |
fun maintain_calculation false calc state =
|
wenzelm@8588
|
156 |
state
|
wenzelm@8588
|
157 |
|> put_calculation calc
|
wenzelm@14555
|
158 |
|> Proof.put_thms (calculationN, calc)
|
wenzelm@8588
|
159 |
| maintain_calculation true calc state =
|
wenzelm@8588
|
160 |
state
|
wenzelm@8588
|
161 |
|> reset_calculation
|
wenzelm@8588
|
162 |
|> Proof.reset_thms calculationN
|
wenzelm@14564
|
163 |
|> Proof.simple_note_thms "" calc
|
wenzelm@8588
|
164 |
|> Proof.chain;
|
wenzelm@8562
|
165 |
|
wenzelm@8562
|
166 |
|
wenzelm@8562
|
167 |
(* 'also' and 'finally' *)
|
wenzelm@8562
|
168 |
|
wenzelm@8588
|
169 |
fun err_if state b msg = if b then raise Proof.STATE (msg, state) else ();
|
wenzelm@8588
|
170 |
|
wenzelm@6877
|
171 |
fun calculate final opt_rules print state =
|
wenzelm@6778
|
172 |
let
|
wenzelm@12805
|
173 |
val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of;
|
wenzelm@9322
|
174 |
val eq_prop = op aconv o pairself (Pattern.eta_contract o strip_assums_concl);
|
wenzelm@11097
|
175 |
fun projection ths th = Library.exists (Library.curry eq_prop th) ths;
|
wenzelm@8300
|
176 |
|
wenzelm@11097
|
177 |
fun combine ths =
|
skalberg@15531
|
178 |
(case opt_rules of SOME rules => rules
|
skalberg@15531
|
179 |
| NONE =>
|
wenzelm@12379
|
180 |
(case ths of [] => NetRules.rules (#1 (get_local_rules state))
|
wenzelm@12379
|
181 |
| th :: _ => NetRules.retrieve (#1 (get_local_rules state)) (strip_assums_concl th)))
|
wenzelm@11097
|
182 |
|> Seq.of_list |> Seq.map (Method.multi_resolve ths) |> Seq.flat
|
wenzelm@11097
|
183 |
|> Seq.filter (not o projection ths);
|
wenzelm@7414
|
184 |
|
wenzelm@14555
|
185 |
val facts = Proof.the_facts (assert_sane final state);
|
wenzelm@6903
|
186 |
val (initial, calculations) =
|
wenzelm@6778
|
187 |
(case get_calculation state of
|
skalberg@15531
|
188 |
NONE => (true, Seq.single facts)
|
skalberg@15531
|
189 |
| SOME calc => (false, Seq.map single (combine (calc @ facts))));
|
wenzelm@6778
|
190 |
in
|
wenzelm@8588
|
191 |
err_if state (initial andalso final) "No calculation yet";
|
wenzelm@15973
|
192 |
err_if state (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
|
wenzelm@12055
|
193 |
calculations |> Seq.map (fn calc => (print (Proof.context_of state) calc;
|
wenzelm@12055
|
194 |
state |> maintain_calculation final calc))
|
wenzelm@6778
|
195 |
end;
|
wenzelm@6778
|
196 |
|
wenzelm@6782
|
197 |
fun also print = calculate false print;
|
wenzelm@6782
|
198 |
fun finally print = calculate true print;
|
wenzelm@6778
|
199 |
|
wenzelm@6778
|
200 |
|
wenzelm@8588
|
201 |
(* 'moreover' and 'ultimately' *)
|
wenzelm@8562
|
202 |
|
wenzelm@8588
|
203 |
fun collect final print state =
|
wenzelm@8588
|
204 |
let
|
wenzelm@14555
|
205 |
val facts = Proof.the_facts (assert_sane final state);
|
wenzelm@8588
|
206 |
val (initial, thms) =
|
wenzelm@8588
|
207 |
(case get_calculation state of
|
skalberg@15531
|
208 |
NONE => (true, [])
|
skalberg@15531
|
209 |
| SOME thms => (false, thms));
|
wenzelm@8588
|
210 |
val calc = thms @ facts;
|
wenzelm@8588
|
211 |
in
|
wenzelm@8588
|
212 |
err_if state (initial andalso final) "No calculation yet";
|
wenzelm@12055
|
213 |
print (Proof.context_of state) calc;
|
wenzelm@8588
|
214 |
state |> maintain_calculation final calc
|
wenzelm@8588
|
215 |
end;
|
wenzelm@8588
|
216 |
|
wenzelm@8588
|
217 |
fun moreover print = collect false print;
|
wenzelm@8588
|
218 |
fun ultimately print = collect true print;
|
wenzelm@8562
|
219 |
|
wenzelm@8562
|
220 |
|
wenzelm@6778
|
221 |
end;
|