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