author | wenzelm |
Sun, 26 Mar 2000 22:31:11 +0200 | |
changeset 8588 | b7c3f264f8ac |
parent 8562 | ce0e2b8e8844 |
child 8634 | 3f34637cb9c0 |
permissions | -rw-r--r-- |
6778 | 1 |
(* Title: Pure/Isar/calculation.ML |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
4 |
||
5 |
Support for calculational proofs. |
|
6 |
*) |
|
7 |
||
8 |
signature CALCULATION = |
|
9 |
sig |
|
10 |
val print_global_rules: theory -> unit |
|
11 |
val print_local_rules: Proof.context -> unit |
|
12 |
val trans_add_global: theory attribute |
|
13 |
val trans_del_global: theory attribute |
|
14 |
val trans_add_local: Proof.context attribute |
|
15 |
val trans_del_local: Proof.context attribute |
|
7414 | 16 |
val also: thm list option -> (thm list -> unit) -> Proof.state -> Proof.state Seq.seq |
17 |
val finally: thm list option -> (thm list -> unit) -> Proof.state -> Proof.state Seq.seq |
|
8562 | 18 |
val moreover: (thm list -> unit) -> Proof.state -> Proof.state |
8588 | 19 |
val ultimately: (thm list -> unit) -> Proof.state -> Proof.state |
6778 | 20 |
val setup: (theory -> theory) list |
21 |
end; |
|
22 |
||
23 |
structure Calculation: CALCULATION = |
|
24 |
struct |
|
25 |
||
26 |
(** global and local calculation data **) |
|
27 |
||
8300 | 28 |
(* theory data kind 'Isar/calculation' *) |
6778 | 29 |
|
8300 | 30 |
fun print_rules rs = Pretty.writeln (Pretty.big_list "calculation rules:" |
31 |
(map Display.pretty_thm (NetRules.rules rs))); |
|
6778 | 32 |
|
33 |
structure GlobalCalculationArgs = |
|
34 |
struct |
|
35 |
val name = "Isar/calculation"; |
|
8300 | 36 |
type T = thm NetRules.T |
6778 | 37 |
|
8300 | 38 |
val empty = NetRules.init_elim; |
6778 | 39 |
val copy = I; |
40 |
val prep_ext = I; |
|
8300 | 41 |
val merge = NetRules.merge; |
6778 | 42 |
fun print _ = print_rules; |
43 |
end; |
|
44 |
||
45 |
structure GlobalCalculation = TheoryDataFun(GlobalCalculationArgs); |
|
46 |
val print_global_rules = GlobalCalculation.print; |
|
47 |
||
48 |
||
49 |
(* proof data kind 'Isar/calculation' *) |
|
50 |
||
51 |
structure LocalCalculationArgs = |
|
52 |
struct |
|
53 |
val name = "Isar/calculation"; |
|
8300 | 54 |
type T = thm NetRules.T * (thm list * int) option; |
6778 | 55 |
|
56 |
fun init thy = (GlobalCalculation.get thy, None); |
|
8300 | 57 |
fun print _ (rs, _) = print_rules rs; |
6778 | 58 |
end; |
59 |
||
60 |
structure LocalCalculation = ProofDataFun(LocalCalculationArgs); |
|
6787 | 61 |
val get_local_rules = #1 o LocalCalculation.get_st; |
6778 | 62 |
val print_local_rules = LocalCalculation.print; |
63 |
||
64 |
||
65 |
(* access calculation *) |
|
66 |
||
67 |
fun get_calculation state = |
|
6787 | 68 |
(case #2 (LocalCalculation.get_st state) of |
6778 | 69 |
None => None |
7414 | 70 |
| Some (thms, lev) => if lev = Proof.level state then Some thms else None); |
6778 | 71 |
|
7414 | 72 |
fun put_calculation thms state = |
73 |
LocalCalculation.put_st (get_local_rules state, Some (thms, Proof.level state)) state; |
|
6778 | 74 |
|
6787 | 75 |
fun reset_calculation state = |
76 |
LocalCalculation.put_st (get_local_rules state, None) state; |
|
77 |
||
6778 | 78 |
|
79 |
||
80 |
(** attributes **) |
|
81 |
||
82 |
(* trans add/del *) |
|
83 |
||
84 |
fun mk_att f g (x, thm) = (f (g thm) x, thm); |
|
85 |
||
8300 | 86 |
val trans_add_global = mk_att GlobalCalculation.map NetRules.insert; |
87 |
val trans_del_global = mk_att GlobalCalculation.map NetRules.delete; |
|
88 |
val trans_add_local = mk_att LocalCalculation.map (Library.apfst o NetRules.insert); |
|
89 |
val trans_del_local = mk_att LocalCalculation.map (Library.apfst o NetRules.delete); |
|
6778 | 90 |
|
91 |
||
92 |
(* concrete syntax *) |
|
93 |
||
94 |
val transN = "trans"; |
|
95 |
val addN = "add"; |
|
96 |
val delN = "del"; |
|
97 |
||
98 |
fun trans_att add del = |
|
99 |
Attrib.syntax (Scan.lift (Args.$$$ addN >> K add || Args.$$$ delN >> K del || Scan.succeed add)); |
|
100 |
||
101 |
val trans_attr = |
|
102 |
(trans_att trans_add_global trans_del_global, trans_att trans_add_local trans_del_local); |
|
103 |
||
104 |
||
6787 | 105 |
|
6778 | 106 |
(** proof commands **) |
107 |
||
8588 | 108 |
(* maintain calculation register *) |
8562 | 109 |
|
6778 | 110 |
val calculationN = "calculation"; |
111 |
||
8588 | 112 |
fun maintain_calculation false calc state = |
113 |
state |
|
114 |
|> put_calculation calc |
|
115 |
|> Proof.simple_have_thms calculationN calc |
|
116 |
|> Proof.reset_facts |
|
117 |
| maintain_calculation true calc state = |
|
118 |
state |
|
119 |
|> reset_calculation |
|
120 |
|> Proof.reset_thms calculationN |
|
121 |
|> Proof.simple_have_thms "" calc |
|
122 |
|> Proof.chain; |
|
8562 | 123 |
|
124 |
||
125 |
(* 'also' and 'finally' *) |
|
126 |
||
8588 | 127 |
fun err_if state b msg = if b then raise Proof.STATE (msg, state) else (); |
128 |
||
6877 | 129 |
fun calculate final opt_rules print state = |
6778 | 130 |
let |
7414 | 131 |
val facts = Proof.the_facts state; |
132 |
||
7554
30327f9f6b4a
differ: compare actual props only (hyps may changed due to trivial steps involving assumptions);
wenzelm
parents:
7475
diff
changeset
|
133 |
val eq_prop = op aconv o pairself (#prop o Thm.rep_thm); |
30327f9f6b4a
differ: compare actual props only (hyps may changed due to trivial steps involving assumptions);
wenzelm
parents:
7475
diff
changeset
|
134 |
fun differ thms thms' = not (Library.equal_lists eq_prop (thms, thms')); |
8300 | 135 |
|
7414 | 136 |
fun combine thms = |
8300 | 137 |
let |
138 |
val ths = thms @ facts; |
|
139 |
val rs = NetRules.inserts (if_none opt_rules []) (get_local_rules state); |
|
140 |
val rules = |
|
141 |
(case ths of [] => NetRules.rules rs |
|
142 |
| th :: _ => NetRules.may_unify rs (Logic.strip_assums_concl (#prop (Thm.rep_thm th)))); |
|
143 |
val ruleq = Seq.of_list rules; |
|
144 |
in Seq.map Library.single (Seq.flat (Seq.map (Method.multi_resolve ths) ruleq)) end; |
|
7414 | 145 |
|
6903 | 146 |
val (initial, calculations) = |
6778 | 147 |
(case get_calculation state of |
7414 | 148 |
None => (true, Seq.single facts) |
149 |
| Some thms => (false, Seq.filter (differ thms) (combine thms))) |
|
6778 | 150 |
in |
8588 | 151 |
err_if state (initial andalso final) "No calculation yet"; |
152 |
err_if state (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given"; |
|
153 |
calculations |> Seq.map (fn calc => (print calc; state |> maintain_calculation final calc)) |
|
6778 | 154 |
end; |
155 |
||
6782 | 156 |
fun also print = calculate false print; |
157 |
fun finally print = calculate true print; |
|
6778 | 158 |
|
159 |
||
8588 | 160 |
(* 'moreover' and 'ultimately' *) |
8562 | 161 |
|
8588 | 162 |
fun collect final print state = |
163 |
let |
|
164 |
val facts = Proof.the_facts state; |
|
165 |
val (initial, thms) = |
|
166 |
(case get_calculation state of |
|
167 |
None => (true, []) |
|
168 |
| Some thms => (false, thms)); |
|
169 |
val calc = thms @ facts; |
|
170 |
in |
|
171 |
err_if state (initial andalso final) "No calculation yet"; |
|
172 |
print calc; |
|
173 |
state |> maintain_calculation final calc |
|
174 |
end; |
|
175 |
||
176 |
fun moreover print = collect false print; |
|
177 |
fun ultimately print = collect true print; |
|
8562 | 178 |
|
179 |
||
6778 | 180 |
|
181 |
(** theory setup **) |
|
182 |
||
183 |
val setup = [GlobalCalculation.init, LocalCalculation.init, |
|
8461 | 184 |
Attrib.add_attributes [(transN, trans_attr, "declare transitivity rule")]]; |
6778 | 185 |
|
186 |
||
187 |
end; |