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