author | wenzelm |
Sat, 01 Apr 2000 20:13:33 +0200 | |
changeset 8652 | 39a695b0b1d7 |
parent 8649 | dc496bb0638f |
child 8807 | 0046be1769f9 |
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 trans_attr = |
|
8634 | 95 |
(Attrib.add_del_args trans_add_global trans_del_global, |
96 |
Attrib.add_del_args trans_add_local trans_del_local); |
|
6778 | 97 |
|
98 |
||
6787 | 99 |
|
6778 | 100 |
(** proof commands **) |
101 |
||
8588 | 102 |
(* maintain calculation register *) |
8562 | 103 |
|
6778 | 104 |
val calculationN = "calculation"; |
105 |
||
8588 | 106 |
fun maintain_calculation false calc state = |
107 |
state |
|
108 |
|> put_calculation calc |
|
109 |
|> Proof.simple_have_thms calculationN calc |
|
110 |
|> Proof.reset_facts |
|
111 |
| maintain_calculation true calc state = |
|
112 |
state |
|
113 |
|> reset_calculation |
|
114 |
|> Proof.reset_thms calculationN |
|
115 |
|> Proof.simple_have_thms "" calc |
|
116 |
|> Proof.chain; |
|
8562 | 117 |
|
118 |
||
119 |
(* 'also' and 'finally' *) |
|
120 |
||
8588 | 121 |
fun err_if state b msg = if b then raise Proof.STATE (msg, state) else (); |
122 |
||
6877 | 123 |
fun calculate final opt_rules print state = |
6778 | 124 |
let |
7414 | 125 |
val facts = Proof.the_facts state; |
126 |
||
7554
30327f9f6b4a
differ: compare actual props only (hyps may changed due to trivial steps involving assumptions);
wenzelm
parents:
7475
diff
changeset
|
127 |
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
|
128 |
fun differ thms thms' = not (Library.equal_lists eq_prop (thms, thms')); |
8300 | 129 |
|
7414 | 130 |
fun combine thms = |
8300 | 131 |
let |
132 |
val ths = thms @ facts; |
|
8649 | 133 |
val rs = get_local_rules state; |
8300 | 134 |
val rules = |
135 |
(case ths of [] => NetRules.rules rs |
|
136 |
| th :: _ => NetRules.may_unify rs (Logic.strip_assums_concl (#prop (Thm.rep_thm th)))); |
|
8649 | 137 |
val ruleq = Seq.of_list (if_none opt_rules [] @ rules); |
8300 | 138 |
in Seq.map Library.single (Seq.flat (Seq.map (Method.multi_resolve ths) ruleq)) end; |
7414 | 139 |
|
6903 | 140 |
val (initial, calculations) = |
6778 | 141 |
(case get_calculation state of |
7414 | 142 |
None => (true, Seq.single facts) |
143 |
| Some thms => (false, Seq.filter (differ thms) (combine thms))) |
|
6778 | 144 |
in |
8588 | 145 |
err_if state (initial andalso final) "No calculation yet"; |
146 |
err_if state (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given"; |
|
147 |
calculations |> Seq.map (fn calc => (print calc; state |> maintain_calculation final calc)) |
|
6778 | 148 |
end; |
149 |
||
6782 | 150 |
fun also print = calculate false print; |
151 |
fun finally print = calculate true print; |
|
6778 | 152 |
|
153 |
||
8588 | 154 |
(* 'moreover' and 'ultimately' *) |
8562 | 155 |
|
8588 | 156 |
fun collect final print state = |
157 |
let |
|
158 |
val facts = Proof.the_facts state; |
|
159 |
val (initial, thms) = |
|
160 |
(case get_calculation state of |
|
161 |
None => (true, []) |
|
162 |
| Some thms => (false, thms)); |
|
163 |
val calc = thms @ facts; |
|
164 |
in |
|
165 |
err_if state (initial andalso final) "No calculation yet"; |
|
166 |
print calc; |
|
167 |
state |> maintain_calculation final calc |
|
168 |
end; |
|
169 |
||
170 |
fun moreover print = collect false print; |
|
171 |
fun ultimately print = collect true print; |
|
8562 | 172 |
|
173 |
||
6778 | 174 |
|
175 |
(** theory setup **) |
|
176 |
||
177 |
val setup = [GlobalCalculation.init, LocalCalculation.init, |
|
8634 | 178 |
Attrib.add_attributes [("trans", trans_attr, "declare transitivity rule")]]; |
6778 | 179 |
|
180 |
||
181 |
end; |