author | wenzelm |
Thu, 07 Aug 2008 19:21:41 +0200 | |
changeset 27779 | 4569003b8813 |
parent 26463 | 9283b4185fdf |
child 28210 | c164d1892553 |
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 |
|
21506 | 10 |
val print_rules: Proof.context -> unit |
16571 | 11 |
val get_calculation: Proof.state -> thm list option |
18728 | 12 |
val trans_add: attribute |
13 |
val trans_del: attribute |
|
14 |
val sym_add: attribute |
|
15 |
val sym_del: attribute |
|
16 |
val symmetric: attribute |
|
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26252
diff
changeset
|
17 |
val also: (Facts.ref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq |
17350
26cd3756377a
more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset
|
18 |
val also_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq |
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26252
diff
changeset
|
19 |
val finally_: (Facts.ref * Attrib.src list) list option -> bool -> |
22573 | 20 |
Proof.state -> Proof.state Seq.seq |
17350
26cd3756377a
more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset
|
21 |
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
|
22 |
val moreover: bool -> Proof.state -> Proof.state |
26cd3756377a
more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset
|
23 |
val ultimately: bool -> Proof.state -> Proof.state |
6778 | 24 |
end; |
25 |
||
26 |
structure Calculation: CALCULATION = |
|
27 |
struct |
|
28 |
||
18637 | 29 |
(** calculation data **) |
6778 | 30 |
|
18637 | 31 |
structure CalculationData = GenericDataFun |
32 |
( |
|
12379 | 33 |
type T = (thm NetRules.T * thm list) * (thm list * int) option; |
18637 | 34 |
val empty = ((NetRules.elim, []), NONE); |
35 |
val extend = I; |
|
6778 | 36 |
|
18637 | 37 |
fun merge _ (((trans1, sym1), _), ((trans2, sym2), _)) = |
24039
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
22846
diff
changeset
|
38 |
((NetRules.merge (trans1, trans2), Thm.merge_thms (sym1, sym2)), NONE); |
18637 | 39 |
); |
40 |
||
22846 | 41 |
fun print_rules ctxt = |
42 |
let val ((trans, sym), _) = CalculationData.get (Context.Proof ctxt) in |
|
43 |
[Pretty.big_list "transitivity rules:" |
|
44 |
(map (ProofContext.pretty_thm ctxt) (NetRules.rules trans)), |
|
45 |
Pretty.big_list "symmetry rules:" (map (ProofContext.pretty_thm ctxt) sym)] |
|
46 |
|> Pretty.chunks |> Pretty.writeln |
|
47 |
end; |
|
6778 | 48 |
|
49 |
||
50 |
(* access calculation *) |
|
51 |
||
52 |
fun get_calculation state = |
|
18637 | 53 |
(case #2 (CalculationData.get (Context.Proof (Proof.context_of state))) of |
15531 | 54 |
NONE => NONE |
55 |
| SOME (thms, lev) => if lev = Proof.level state then SOME thms else NONE); |
|
6778 | 56 |
|
17350
26cd3756377a
more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset
|
57 |
val calculationN = "calculation"; |
6778 | 58 |
|
17350
26cd3756377a
more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset
|
59 |
fun put_calculation calc = |
18728 | 60 |
`Proof.level #-> (fn lev => Proof.map_context (Context.proof_map |
61 |
(CalculationData.map (apsnd (K (Option.map (rpair lev) calc)))))) |
|
26252 | 62 |
#> Proof.put_thms false (calculationN, calc); |
6778 | 63 |
|
64 |
||
18637 | 65 |
|
6778 | 66 |
(** attributes **) |
67 |
||
12379 | 68 |
(* add/del rules *) |
69 |
||
18728 | 70 |
val trans_add = Thm.declaration_attribute (CalculationData.map o apfst o apfst o NetRules.insert); |
71 |
val trans_del = Thm.declaration_attribute (CalculationData.map o apfst o apfst o NetRules.delete); |
|
6778 | 72 |
|
18637 | 73 |
val sym_add = |
24039
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
22846
diff
changeset
|
74 |
Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.add_thm) |
18637 | 75 |
#> ContextRules.elim_query NONE; |
76 |
val sym_del = |
|
24039
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
22846
diff
changeset
|
77 |
Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.del_thm) |
18637 | 78 |
#> ContextRules.rule_del; |
12379 | 79 |
|
80 |
||
18637 | 81 |
(* symmetric *) |
12379 | 82 |
|
18728 | 83 |
val symmetric = Thm.rule_attribute (fn x => fn th => |
19861 | 84 |
(case Seq.chop 2 (Drule.multi_resolves [th] (#2 (#1 (CalculationData.get x)))) of |
20898 | 85 |
([th'], _) => Drule.zero_var_indexes th' |
12379 | 86 |
| ([], _) => raise THM ("symmetric: no unifiers", 1, [th]) |
87 |
| _ => raise THM ("symmetric: multiple unifiers", 1, [th]))); |
|
88 |
||
6778 | 89 |
|
90 |
(* concrete syntax *) |
|
91 |
||
18637 | 92 |
val trans_att = Attrib.add_del_args trans_add trans_del; |
93 |
val sym_att = Attrib.add_del_args sym_add sym_del; |
|
12379 | 94 |
|
26463 | 95 |
val _ = Context.>> (Context.map_theory |
18708 | 96 |
(Attrib.add_attributes |
18728 | 97 |
[("trans", trans_att, "declaration of transitivity rule"), |
98 |
("sym", sym_att, "declaration of symmetry rule"), |
|
99 |
("symmetric", Attrib.no_args symmetric, "resolution with symmetry rule")] #> |
|
18708 | 100 |
PureThy.add_thms |
18728 | 101 |
[(("", transitive_thm), [trans_add]), |
26463 | 102 |
(("", symmetric_thm), [sym_add])] #> snd)); |
15801 | 103 |
|
6778 | 104 |
|
6787 | 105 |
|
6778 | 106 |
(** proof commands **) |
107 |
||
18678 | 108 |
fun err_if b msg = if b then error msg else (); |
17350
26cd3756377a
more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset
|
109 |
|
14555
341908d6c792
'also'/'moreover': do not interfere with current facts, allow in chain mode;
wenzelm
parents:
14549
diff
changeset
|
110 |
fun assert_sane final = |
341908d6c792
'also'/'moreover': do not interfere with current facts, allow in chain mode;
wenzelm
parents:
14549
diff
changeset
|
111 |
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
|
112 |
|
17350
26cd3756377a
more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset
|
113 |
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
|
114 |
| maintain_calculation true calc = put_calculation NONE #> Proof.chain_facts calc; |
6778 | 115 |
|
17350
26cd3756377a
more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset
|
116 |
fun print_calculation false _ _ = () |
26cd3756377a
more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset
|
117 |
| print_calculation true ctxt calc = |
26cd3756377a
more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset
|
118 |
Pretty.writeln (ProofContext.pretty_fact ctxt (calculationN, calc)); |
8562 | 119 |
|
120 |
||
17350
26cd3756377a
more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset
|
121 |
(* also and finally *) |
8562 | 122 |
|
18637 | 123 |
val get_rules = #1 o CalculationData.get o Context.Proof o Proof.context_of; |
124 |
||
17350
26cd3756377a
more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset
|
125 |
fun calculate prep_rules final raw_rules int state = |
6778 | 126 |
let |
12805 | 127 |
val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of; |
18947 | 128 |
val eq_prop = op aconv o pairself (Envir.beta_eta_contract o strip_assums_concl); |
11097 | 129 |
fun projection ths th = Library.exists (Library.curry eq_prop th) ths; |
8300 | 130 |
|
17350
26cd3756377a
more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset
|
131 |
val opt_rules = Option.map (prep_rules state) raw_rules; |
11097 | 132 |
fun combine ths = |
15531 | 133 |
(case opt_rules of SOME rules => rules |
134 |
| NONE => |
|
18637 | 135 |
(case ths of [] => NetRules.rules (#1 (get_rules state)) |
136 |
| th :: _ => NetRules.retrieve (#1 (get_rules state)) (strip_assums_concl th))) |
|
18223 | 137 |
|> Seq.of_list |> Seq.maps (Drule.multi_resolve ths) |
11097 | 138 |
|> Seq.filter (not o projection ths); |
7414 | 139 |
|
14555
341908d6c792
'also'/'moreover': do not interfere with current facts, allow in chain mode;
wenzelm
parents:
14549
diff
changeset
|
140 |
val facts = Proof.the_facts (assert_sane final state); |
6903 | 141 |
val (initial, calculations) = |
6778 | 142 |
(case get_calculation state of |
15531 | 143 |
NONE => (true, Seq.single facts) |
144 |
| SOME calc => (false, Seq.map single (combine (calc @ facts)))); |
|
6778 | 145 |
in |
18678 | 146 |
err_if (initial andalso final) "No calculation yet"; |
147 |
err_if (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
|
148 |
calculations |> Seq.map (fn calc => (print_calculation int (Proof.context_of state) calc; |
12055 | 149 |
state |> maintain_calculation final calc)) |
6778 | 150 |
end; |
151 |
||
17350
26cd3756377a
more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset
|
152 |
val also = calculate Proof.get_thmss false; |
26cd3756377a
more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset
|
153 |
val also_i = calculate (K I) false; |
22573 | 154 |
val finally_ = calculate Proof.get_thmss true; |
17350
26cd3756377a
more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset
|
155 |
val finally_i = calculate (K I) true; |
6778 | 156 |
|
157 |
||
17350
26cd3756377a
more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset
|
158 |
(* moreover and ultimately *) |
8562 | 159 |
|
17350
26cd3756377a
more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset
|
160 |
fun collect final int state = |
8588 | 161 |
let |
14555
341908d6c792
'also'/'moreover': do not interfere with current facts, allow in chain mode;
wenzelm
parents:
14549
diff
changeset
|
162 |
val facts = Proof.the_facts (assert_sane final state); |
8588 | 163 |
val (initial, thms) = |
164 |
(case get_calculation state of |
|
15531 | 165 |
NONE => (true, []) |
166 |
| SOME thms => (false, thms)); |
|
8588 | 167 |
val calc = thms @ facts; |
168 |
in |
|
18678 | 169 |
err_if (initial andalso final) "No calculation yet"; |
17350
26cd3756377a
more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset
|
170 |
print_calculation int (Proof.context_of state) calc; |
8588 | 171 |
state |> maintain_calculation final calc |
172 |
end; |
|
173 |
||
17350
26cd3756377a
more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset
|
174 |
val moreover = collect false; |
26cd3756377a
more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset
|
175 |
val ultimately = collect true; |
8562 | 176 |
|
6778 | 177 |
end; |