author | wenzelm |
Thu, 07 Oct 1999 12:36:53 +0200 | |
changeset 7775 | 26898fbd19ca |
parent 7600 | 73f91da46230 |
child 8150 | 7021549ef32d |
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 |
|
6778 | 18 |
val setup: (theory -> theory) list |
19 |
end; |
|
20 |
||
21 |
structure Calculation: CALCULATION = |
|
22 |
struct |
|
23 |
||
24 |
||
25 |
(** global and local calculation data **) |
|
26 |
||
27 |
fun print_rules ths = |
|
28 |
Pretty.writeln (Pretty.big_list "calculation rules:" (map Display.pretty_thm ths)); |
|
29 |
||
7414 | 30 |
|
6778 | 31 |
(* theory data kind 'Isar/calculation' *) |
32 |
||
33 |
structure GlobalCalculationArgs = |
|
34 |
struct |
|
35 |
val name = "Isar/calculation"; |
|
36 |
type T = thm list; |
|
37 |
||
38 |
val empty = []; |
|
39 |
val copy = I; |
|
40 |
val prep_ext = I; |
|
41 |
fun merge (ths1, ths2) = Library.generic_merge Thm.eq_thm I I ths1 ths2; |
|
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"; |
|
7414 | 54 |
type T = thm list * (thm list * int) option; |
6778 | 55 |
|
56 |
fun init thy = (GlobalCalculation.get thy, None); |
|
57 |
fun print _ (ths, _) = print_rules ths; |
|
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 |
local |
|
85 |
||
86 |
fun map_rules_global f thy = GlobalCalculation.put (f (GlobalCalculation.get thy)) thy; |
|
87 |
fun map_rules_local f ctxt = LocalCalculation.put (f (LocalCalculation.get ctxt)) ctxt; |
|
88 |
||
89 |
fun add_trans thm rules = Library.gen_ins Thm.eq_thm (thm, rules); |
|
90 |
fun del_trans thm rules = Library.gen_rem Thm.eq_thm (rules, thm); |
|
91 |
||
92 |
fun mk_att f g (x, thm) = (f (g thm) x, thm); |
|
93 |
||
94 |
in |
|
95 |
||
96 |
val trans_add_global = mk_att map_rules_global add_trans; |
|
97 |
val trans_del_global = mk_att map_rules_global del_trans; |
|
98 |
val trans_add_local = mk_att map_rules_local (Library.apfst o add_trans); |
|
99 |
val trans_del_local = mk_att map_rules_local (Library.apfst o del_trans); |
|
100 |
||
101 |
end; |
|
102 |
||
103 |
||
104 |
(* concrete syntax *) |
|
105 |
||
106 |
val transN = "trans"; |
|
107 |
val addN = "add"; |
|
108 |
val delN = "del"; |
|
109 |
||
110 |
fun trans_att add del = |
|
111 |
Attrib.syntax (Scan.lift (Args.$$$ addN >> K add || Args.$$$ delN >> K del || Scan.succeed add)); |
|
112 |
||
113 |
val trans_attr = |
|
114 |
(trans_att trans_add_global trans_del_global, trans_att trans_add_local trans_del_local); |
|
115 |
||
116 |
||
6787 | 117 |
|
6778 | 118 |
(** proof commands **) |
119 |
||
120 |
val calculationN = "calculation"; |
|
121 |
||
6877 | 122 |
fun calculate final opt_rules print state = |
6778 | 123 |
let |
6903 | 124 |
fun err_if b msg = if b then raise Proof.STATE (msg, state) else (); |
7414 | 125 |
val facts = Proof.the_facts state; |
7197 | 126 |
val rules = Seq.of_list (if_none opt_rules [] @ get_local_rules state); |
7414 | 127 |
|
7554
30327f9f6b4a
differ: compare actual props only (hyps may changed due to trivial steps involving assumptions);
wenzelm
parents:
7475
diff
changeset
|
128 |
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
|
129 |
fun differ thms thms' = not (Library.equal_lists eq_prop (thms, thms')); |
7414 | 130 |
fun combine thms = |
131 |
Seq.map Library.single (Seq.flat (Seq.map (Method.multi_resolve (thms @ facts)) rules)); |
|
132 |
||
6903 | 133 |
val (initial, calculations) = |
6778 | 134 |
(case get_calculation state of |
7414 | 135 |
None => (true, Seq.single facts) |
136 |
| Some thms => (false, Seq.filter (differ thms) (combine thms))) |
|
6778 | 137 |
in |
6903 | 138 |
err_if (initial andalso final) "No calculation yet"; |
139 |
err_if (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given"; |
|
6782 | 140 |
calculations |> Seq.map (fn calc => |
141 |
(print calc; |
|
6787 | 142 |
(if final then |
143 |
state |
|
144 |
|> reset_calculation |
|
7600 | 145 |
|> Proof.reset_thms calculationN |
7414 | 146 |
|> Proof.simple_have_thms "" calc |
6787 | 147 |
|> Proof.chain |
148 |
else |
|
149 |
state |
|
150 |
|> put_calculation calc |
|
7414 | 151 |
|> Proof.simple_have_thms calculationN calc |
6787 | 152 |
|> Proof.reset_facts))) |
6778 | 153 |
end; |
154 |
||
6782 | 155 |
fun also print = calculate false print; |
156 |
fun finally print = calculate true print; |
|
6778 | 157 |
|
158 |
||
159 |
||
160 |
(** theory setup **) |
|
161 |
||
162 |
val setup = [GlobalCalculation.init, LocalCalculation.init, |
|
163 |
Attrib.add_attributes [(transN, trans_attr, "transitivity rule")]]; |
|
164 |
||
165 |
||
166 |
end; |