author | wenzelm |
Fri, 21 May 2010 22:08:13 +0200 | |
changeset 37047 | 4a95a50d0ec4 |
parent 36323 | 655e2d74de3a |
child 38332 | 6551e310e7cb |
permissions | -rw-r--r-- |
6778 | 1 |
(* Title: Pure/Isar/calculation.ML |
2 |
Author: Markus Wenzel, TU Muenchen |
|
3 |
||
17350
26cd3756377a
more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset
|
4 |
Generic calculational proofs. |
6778 | 5 |
*) |
6 |
||
7 |
signature CALCULATION = |
|
8 |
sig |
|
21506 | 9 |
val print_rules: Proof.context -> unit |
16571 | 10 |
val get_calculation: Proof.state -> thm list option |
18728 | 11 |
val trans_add: attribute |
12 |
val trans_del: attribute |
|
13 |
val sym_add: attribute |
|
14 |
val sym_del: attribute |
|
15 |
val symmetric: attribute |
|
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
33519
diff
changeset
|
16 |
val also: thm list option -> bool -> Proof.state -> Proof.state Seq.seq |
37047
4a95a50d0ec4
print calculation result in the context where the fact is actually defined -- proper externing;
wenzelm
parents:
36323
diff
changeset
|
17 |
val also_cmd: (Facts.ref * Attrib.src list) list option -> |
4a95a50d0ec4
print calculation result in the context where the fact is actually defined -- proper externing;
wenzelm
parents:
36323
diff
changeset
|
18 |
bool -> Proof.state -> Proof.state Seq.seq |
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
33519
diff
changeset
|
19 |
val finally: thm list option -> bool -> Proof.state -> Proof.state Seq.seq |
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
33519
diff
changeset
|
20 |
val finally_cmd: (Facts.ref * Attrib.src list) list option -> bool -> |
22573 | 21 |
Proof.state -> Proof.state Seq.seq |
17350
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 |
|
37047
4a95a50d0ec4
print calculation result in the context where the fact is actually defined -- proper externing;
wenzelm
parents:
36323
diff
changeset
|
31 |
structure Data = Generic_Data |
18637 | 32 |
( |
30560 | 33 |
type T = (thm Item_Net.T * thm list) * (thm list * int) option; |
34 |
val empty = ((Thm.elim_rules, []), NONE); |
|
18637 | 35 |
val extend = I; |
33519 | 36 |
fun merge (((trans1, sym1), _), ((trans2, sym2), _)) = |
30560 | 37 |
((Item_Net.merge (trans1, trans2), Thm.merge_thms (sym1, sym2)), NONE); |
18637 | 38 |
); |
39 |
||
22846 | 40 |
fun print_rules ctxt = |
37047
4a95a50d0ec4
print calculation result in the context where the fact is actually defined -- proper externing;
wenzelm
parents:
36323
diff
changeset
|
41 |
let val ((trans, sym), _) = Data.get (Context.Proof ctxt) in |
22846 | 42 |
[Pretty.big_list "transitivity rules:" |
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
30560
diff
changeset
|
43 |
(map (Display.pretty_thm ctxt) (Item_Net.content trans)), |
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
30560
diff
changeset
|
44 |
Pretty.big_list "symmetry rules:" (map (Display.pretty_thm ctxt) sym)] |
22846 | 45 |
|> Pretty.chunks |> Pretty.writeln |
46 |
end; |
|
6778 | 47 |
|
48 |
||
49 |
(* access calculation *) |
|
50 |
||
51 |
fun get_calculation state = |
|
37047
4a95a50d0ec4
print calculation result in the context where the fact is actually defined -- proper externing;
wenzelm
parents:
36323
diff
changeset
|
52 |
(case #2 (Data.get (Context.Proof (Proof.context_of state))) of |
15531 | 53 |
NONE => NONE |
54 |
| SOME (thms, lev) => if lev = Proof.level state then SOME thms else NONE); |
|
6778 | 55 |
|
17350
26cd3756377a
more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset
|
56 |
val calculationN = "calculation"; |
6778 | 57 |
|
17350
26cd3756377a
more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset
|
58 |
fun put_calculation calc = |
18728 | 59 |
`Proof.level #-> (fn lev => Proof.map_context (Context.proof_map |
37047
4a95a50d0ec4
print calculation result in the context where the fact is actually defined -- proper externing;
wenzelm
parents:
36323
diff
changeset
|
60 |
(Data.map (apsnd (K (Option.map (rpair lev) calc)))))) |
26252 | 61 |
#> Proof.put_thms false (calculationN, calc); |
6778 | 62 |
|
63 |
||
18637 | 64 |
|
6778 | 65 |
(** attributes **) |
66 |
||
12379 | 67 |
(* add/del rules *) |
68 |
||
37047
4a95a50d0ec4
print calculation result in the context where the fact is actually defined -- proper externing;
wenzelm
parents:
36323
diff
changeset
|
69 |
val trans_add = Thm.declaration_attribute (Data.map o apfst o apfst o Item_Net.update); |
4a95a50d0ec4
print calculation result in the context where the fact is actually defined -- proper externing;
wenzelm
parents:
36323
diff
changeset
|
70 |
val trans_del = Thm.declaration_attribute (Data.map o apfst o apfst o Item_Net.remove); |
6778 | 71 |
|
18637 | 72 |
val sym_add = |
37047
4a95a50d0ec4
print calculation result in the context where the fact is actually defined -- proper externing;
wenzelm
parents:
36323
diff
changeset
|
73 |
Thm.declaration_attribute (Data.map o apfst o apsnd o Thm.add_thm) |
33369 | 74 |
#> Context_Rules.elim_query NONE; |
75 |
||
18637 | 76 |
val sym_del = |
37047
4a95a50d0ec4
print calculation result in the context where the fact is actually defined -- proper externing;
wenzelm
parents:
36323
diff
changeset
|
77 |
Thm.declaration_attribute (Data.map o apfst o apsnd o Thm.del_thm) |
33369 | 78 |
#> Context_Rules.rule_del; |
12379 | 79 |
|
80 |
||
18637 | 81 |
(* symmetric *) |
12379 | 82 |
|
18728 | 83 |
val symmetric = Thm.rule_attribute (fn x => fn th => |
37047
4a95a50d0ec4
print calculation result in the context where the fact is actually defined -- proper externing;
wenzelm
parents:
36323
diff
changeset
|
84 |
(case Seq.chop 2 (Drule.multi_resolves [th] (#2 (#1 (Data.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 |
||
26463 | 92 |
val _ = Context.>> (Context.map_theory |
30528 | 93 |
(Attrib.setup (Binding.name "trans") (Attrib.add_del trans_add trans_del) |
94 |
"declaration of transitivity rule" #> |
|
95 |
Attrib.setup (Binding.name "sym") (Attrib.add_del sym_add sym_del) |
|
96 |
"declaration of symmetry rule" #> |
|
97 |
Attrib.setup (Binding.name "symmetric") (Scan.succeed symmetric) |
|
98 |
"resolution with symmetry rule" #> |
|
18708 | 99 |
PureThy.add_thms |
29579 | 100 |
[((Binding.empty, transitive_thm), [trans_add]), |
101 |
((Binding.empty, symmetric_thm), [sym_add])] #> snd)); |
|
15801 | 102 |
|
6778 | 103 |
|
6787 | 104 |
|
6778 | 105 |
(** proof commands **) |
106 |
||
14555
341908d6c792
'also'/'moreover': do not interfere with current facts, allow in chain mode;
wenzelm
parents:
14549
diff
changeset
|
107 |
fun assert_sane final = |
341908d6c792
'also'/'moreover': do not interfere with current facts, allow in chain mode;
wenzelm
parents:
14549
diff
changeset
|
108 |
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
|
109 |
|
37047
4a95a50d0ec4
print calculation result in the context where the fact is actually defined -- proper externing;
wenzelm
parents:
36323
diff
changeset
|
110 |
fun maintain_calculation int final calc state = |
4a95a50d0ec4
print calculation result in the context where the fact is actually defined -- proper externing;
wenzelm
parents:
36323
diff
changeset
|
111 |
let |
4a95a50d0ec4
print calculation result in the context where the fact is actually defined -- proper externing;
wenzelm
parents:
36323
diff
changeset
|
112 |
val state' = put_calculation (SOME calc) state; |
4a95a50d0ec4
print calculation result in the context where the fact is actually defined -- proper externing;
wenzelm
parents:
36323
diff
changeset
|
113 |
val ctxt' = Proof.context_of state'; |
4a95a50d0ec4
print calculation result in the context where the fact is actually defined -- proper externing;
wenzelm
parents:
36323
diff
changeset
|
114 |
val _ = |
4a95a50d0ec4
print calculation result in the context where the fact is actually defined -- proper externing;
wenzelm
parents:
36323
diff
changeset
|
115 |
if int then |
4a95a50d0ec4
print calculation result in the context where the fact is actually defined -- proper externing;
wenzelm
parents:
36323
diff
changeset
|
116 |
Pretty.writeln |
4a95a50d0ec4
print calculation result in the context where the fact is actually defined -- proper externing;
wenzelm
parents:
36323
diff
changeset
|
117 |
(ProofContext.pretty_fact ctxt' |
4a95a50d0ec4
print calculation result in the context where the fact is actually defined -- proper externing;
wenzelm
parents:
36323
diff
changeset
|
118 |
(ProofContext.full_name ctxt' (Binding.name calculationN), calc)) |
4a95a50d0ec4
print calculation result in the context where the fact is actually defined -- proper externing;
wenzelm
parents:
36323
diff
changeset
|
119 |
else (); |
4a95a50d0ec4
print calculation result in the context where the fact is actually defined -- proper externing;
wenzelm
parents:
36323
diff
changeset
|
120 |
in state' |> final ? (put_calculation NONE #> Proof.chain_facts calc) end; |
8562 | 121 |
|
122 |
||
17350
26cd3756377a
more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset
|
123 |
(* also and finally *) |
8562 | 124 |
|
37047
4a95a50d0ec4
print calculation result in the context where the fact is actually defined -- proper externing;
wenzelm
parents:
36323
diff
changeset
|
125 |
val get_rules = #1 o Data.get o Context.Proof o Proof.context_of; |
18637 | 126 |
|
17350
26cd3756377a
more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset
|
127 |
fun calculate prep_rules final raw_rules int state = |
6778 | 128 |
let |
12805 | 129 |
val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of; |
18947 | 130 |
val eq_prop = op aconv o pairself (Envir.beta_eta_contract o strip_assums_concl); |
37047
4a95a50d0ec4
print calculation result in the context where the fact is actually defined -- proper externing;
wenzelm
parents:
36323
diff
changeset
|
131 |
fun projection ths th = exists (curry eq_prop th) ths; |
8300 | 132 |
|
17350
26cd3756377a
more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset
|
133 |
val opt_rules = Option.map (prep_rules state) raw_rules; |
11097 | 134 |
fun combine ths = |
15531 | 135 |
(case opt_rules of SOME rules => rules |
136 |
| NONE => |
|
33373 | 137 |
(case ths of |
138 |
[] => Item_Net.content (#1 (get_rules state)) |
|
30560 | 139 |
| th :: _ => Item_Net.retrieve (#1 (get_rules state)) (strip_assums_concl th))) |
18223 | 140 |
|> Seq.of_list |> Seq.maps (Drule.multi_resolve ths) |
11097 | 141 |
|> Seq.filter (not o projection ths); |
7414 | 142 |
|
14555
341908d6c792
'also'/'moreover': do not interfere with current facts, allow in chain mode;
wenzelm
parents:
14549
diff
changeset
|
143 |
val facts = Proof.the_facts (assert_sane final state); |
6903 | 144 |
val (initial, calculations) = |
6778 | 145 |
(case get_calculation state of |
15531 | 146 |
NONE => (true, Seq.single facts) |
147 |
| SOME calc => (false, Seq.map single (combine (calc @ facts)))); |
|
37047
4a95a50d0ec4
print calculation result in the context where the fact is actually defined -- proper externing;
wenzelm
parents:
36323
diff
changeset
|
148 |
|
4a95a50d0ec4
print calculation result in the context where the fact is actually defined -- proper externing;
wenzelm
parents:
36323
diff
changeset
|
149 |
val _ = initial andalso final andalso error "No calculation yet"; |
4a95a50d0ec4
print calculation result in the context where the fact is actually defined -- proper externing;
wenzelm
parents:
36323
diff
changeset
|
150 |
val _ = initial andalso is_some opt_rules andalso |
4a95a50d0ec4
print calculation result in the context where the fact is actually defined -- proper externing;
wenzelm
parents:
36323
diff
changeset
|
151 |
error "Initial calculation -- no rules to be given"; |
6778 | 152 |
in |
37047
4a95a50d0ec4
print calculation result in the context where the fact is actually defined -- proper externing;
wenzelm
parents:
36323
diff
changeset
|
153 |
calculations |> Seq.map (fn calc => maintain_calculation int final calc state) |
6778 | 154 |
end; |
155 |
||
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
33519
diff
changeset
|
156 |
val also = calculate (K I) false; |
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
33519
diff
changeset
|
157 |
val also_cmd = calculate Proof.get_thmss_cmd false; |
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
33519
diff
changeset
|
158 |
val finally = calculate (K I) true; |
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
33519
diff
changeset
|
159 |
val finally_cmd = calculate Proof.get_thmss_cmd true; |
6778 | 160 |
|
161 |
||
17350
26cd3756377a
more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset
|
162 |
(* moreover and ultimately *) |
8562 | 163 |
|
17350
26cd3756377a
more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset
|
164 |
fun collect final int state = |
8588 | 165 |
let |
14555
341908d6c792
'also'/'moreover': do not interfere with current facts, allow in chain mode;
wenzelm
parents:
14549
diff
changeset
|
166 |
val facts = Proof.the_facts (assert_sane final state); |
8588 | 167 |
val (initial, thms) = |
168 |
(case get_calculation state of |
|
15531 | 169 |
NONE => (true, []) |
170 |
| SOME thms => (false, thms)); |
|
8588 | 171 |
val calc = thms @ facts; |
37047
4a95a50d0ec4
print calculation result in the context where the fact is actually defined -- proper externing;
wenzelm
parents:
36323
diff
changeset
|
172 |
val _ = initial andalso final andalso error "No calculation yet"; |
4a95a50d0ec4
print calculation result in the context where the fact is actually defined -- proper externing;
wenzelm
parents:
36323
diff
changeset
|
173 |
in maintain_calculation int final calc state end; |
8588 | 174 |
|
17350
26cd3756377a
more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset
|
175 |
val moreover = collect false; |
26cd3756377a
more self-contained proof elements (material from isar_thy.ML);
wenzelm
parents:
16571
diff
changeset
|
176 |
val ultimately = collect true; |
8562 | 177 |
|
6778 | 178 |
end; |