author | paulson |
Thu, 26 Sep 1996 12:47:47 +0200 | |
changeset 2031 | 03a843f0f447 |
parent 2022 | 9d47e2962edd |
child 2036 | 62ff902eeffc |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/simpdata.ML |
923 | 2 |
ID: $Id$ |
1465 | 3 |
Author: Tobias Nipkow |
923 | 4 |
Copyright 1991 University of Cambridge |
5 |
||
6 |
Instantiation of the generic simplifier |
|
7 |
*) |
|
8 |
||
1984 | 9 |
section "Simplifier"; |
10 |
||
923 | 11 |
open Simplifier; |
12 |
||
1922 | 13 |
(*** Integration of simplifier with classical reasoner ***) |
14 |
||
15 |
(*Add a simpset to a classical set!*) |
|
16 |
infix 4 addss; |
|
17 |
fun cs addss ss = cs addbefore asm_full_simp_tac ss 1; |
|
18 |
||
19 |
fun Addss ss = (claset := !claset addbefore asm_full_simp_tac ss 1); |
|
20 |
||
1968
daa97cc96feb
Beefed-up auto-tactic: now repeatedly simplifies if needed
paulson
parents:
1948
diff
changeset
|
21 |
(*Designed to be idempotent, except if best_tac instantiates variables |
daa97cc96feb
Beefed-up auto-tactic: now repeatedly simplifies if needed
paulson
parents:
1948
diff
changeset
|
22 |
in some of the subgoals*) |
1922 | 23 |
fun auto_tac (cs,ss) = |
24 |
ALLGOALS (asm_full_simp_tac ss) THEN |
|
1968
daa97cc96feb
Beefed-up auto-tactic: now repeatedly simplifies if needed
paulson
parents:
1948
diff
changeset
|
25 |
REPEAT (safe_tac cs THEN ALLGOALS (asm_full_simp_tac ss)) THEN |
1922 | 26 |
REPEAT (FIRSTGOAL (best_tac (cs addss ss))); |
27 |
||
28 |
fun Auto_tac() = auto_tac (!claset, !simpset); |
|
29 |
||
30 |
fun auto() = by (Auto_tac()); |
|
31 |
||
32 |
||
1984 | 33 |
(*** Addition of rules to simpsets and clasets simultaneously ***) |
34 |
||
35 |
(*Takes UNCONDITIONAL theorems of the form A<->B to |
|
2031 | 36 |
the Safe Intr rule B==>A and |
37 |
the Safe Destruct rule A==>B. |
|
1984 | 38 |
Also ~A goes to the Safe Elim rule A ==> ?R |
39 |
Failing other cases, A is added as a Safe Intr rule*) |
|
40 |
local |
|
41 |
val iff_const = HOLogic.eq_const HOLogic.boolT; |
|
42 |
||
43 |
fun addIff th = |
|
44 |
(case HOLogic.dest_Trueprop (#prop(rep_thm th)) of |
|
2031 | 45 |
(Const("not",_) $ A) => |
46 |
AddSEs [zero_var_indexes (th RS notE)] |
|
47 |
| (con $ _ $ _) => |
|
48 |
if con=iff_const |
|
49 |
then (AddSIs [zero_var_indexes (th RS iffD2)]; |
|
50 |
AddSDs [zero_var_indexes (th RS iffD1)]) |
|
51 |
else AddSIs [th] |
|
52 |
| _ => AddSIs [th]; |
|
1984 | 53 |
Addsimps [th]) |
54 |
handle _ => error ("AddIffs: theorem must be unconditional\n" ^ |
|
2031 | 55 |
string_of_thm th) |
1984 | 56 |
|
57 |
fun delIff th = |
|
58 |
(case HOLogic.dest_Trueprop (#prop(rep_thm th)) of |
|
2031 | 59 |
(Const("not",_) $ A) => |
60 |
Delrules [zero_var_indexes (th RS notE)] |
|
61 |
| (con $ _ $ _) => |
|
62 |
if con=iff_const |
|
63 |
then Delrules [zero_var_indexes (th RS iffD2), |
|
64 |
zero_var_indexes (th RS iffD1)] |
|
65 |
else Delrules [th] |
|
66 |
| _ => Delrules [th]; |
|
1984 | 67 |
Delsimps [th]) |
68 |
handle _ => warning("DelIffs: ignoring conditional theorem\n" ^ |
|
2031 | 69 |
string_of_thm th) |
1984 | 70 |
in |
71 |
val AddIffs = seq addIff |
|
72 |
val DelIffs = seq delIff |
|
73 |
end; |
|
74 |
||
75 |
||
923 | 76 |
local |
77 |
||
1922 | 78 |
fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]); |
923 | 79 |
|
1922 | 80 |
val P_imp_P_iff_True = prover "P --> (P = True)" RS mp; |
81 |
val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection; |
|
923 | 82 |
|
1922 | 83 |
val not_P_imp_P_iff_F = prover "~P --> (P = False)" RS mp; |
84 |
val not_P_imp_P_eq_False = not_P_imp_P_iff_F RS eq_reflection; |
|
923 | 85 |
|
1922 | 86 |
fun atomize pairs = |
87 |
let fun atoms th = |
|
2031 | 88 |
(case concl_of th of |
89 |
Const("Trueprop",_) $ p => |
|
90 |
(case head_of p of |
|
91 |
Const(a,_) => |
|
92 |
(case assoc(pairs,a) of |
|
93 |
Some(rls) => flat (map atoms ([th] RL rls)) |
|
94 |
| None => [th]) |
|
95 |
| _ => [th]) |
|
96 |
| _ => [th]) |
|
1922 | 97 |
in atoms end; |
923 | 98 |
|
1922 | 99 |
fun mk_meta_eq r = case concl_of r of |
2031 | 100 |
Const("==",_)$_$_ => r |
1922 | 101 |
| _$(Const("op =",_)$_$_) => r RS eq_reflection |
102 |
| _$(Const("not",_)$_) => r RS not_P_imp_P_eq_False |
|
103 |
| _ => r RS P_imp_P_eq_True; |
|
104 |
(* last 2 lines requires all formulae to be of the from Trueprop(.) *) |
|
923 | 105 |
|
1922 | 106 |
fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th; |
923 | 107 |
|
1922 | 108 |
val simp_thms = map prover |
109 |
[ "(x=x) = True", |
|
110 |
"(~True) = False", "(~False) = True", "(~ ~ P) = P", |
|
111 |
"(~P) ~= P", "P ~= (~P)", "(P ~= Q) = (P = (~Q))", |
|
112 |
"(True=P) = P", "(P=True) = P", |
|
113 |
"(True --> P) = P", "(False --> P) = True", |
|
114 |
"(P --> True) = True", "(P --> P) = True", |
|
115 |
"(P --> False) = (~P)", "(P --> ~P) = (~P)", |
|
116 |
"(P & True) = P", "(True & P) = P", |
|
117 |
"(P & False) = False", "(False & P) = False", "(P & P) = P", |
|
118 |
"(P | True) = True", "(True | P) = True", |
|
119 |
"(P | False) = P", "(False | P) = P", "(P | P) = P", |
|
1948
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
120 |
"((~P) = (~Q)) = (P=Q)", |
1922 | 121 |
"(!x.P) = P", "(? x.P) = P", "? x. x=t", |
122 |
"(? x. x=t & P(x)) = P(t)", "(! x. x=t --> P(x)) = P(t)" ]; |
|
923 | 123 |
|
124 |
in |
|
125 |
||
126 |
val meta_eq_to_obj_eq = prove_goal HOL.thy "x==y ==> x=y" |
|
127 |
(fn [prem] => [rewtac prem, rtac refl 1]); |
|
128 |
||
129 |
val eq_sym_conv = prover "(x=y) = (y=x)"; |
|
130 |
||
131 |
val conj_assoc = prover "((P&Q)&R) = (P&(Q&R))"; |
|
132 |
||
1922 | 133 |
val disj_assoc = prover "((P|Q)|R) = (P|(Q|R))"; |
134 |
||
135 |
val imp_disj = prover "(P|Q --> R) = ((P-->R)&(Q-->R))"; |
|
136 |
||
1948
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
137 |
(*Avoids duplication of subgoals after expand_if, when the true and false |
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
138 |
cases boil down to the same thing.*) |
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
139 |
val cases_simp = prover "((P --> Q) & (~P --> Q)) = Q"; |
1922 | 140 |
|
965 | 141 |
val if_True = prove_goalw HOL.thy [if_def] "(if True then x else y) = x" |
923 | 142 |
(fn _=>[fast_tac (HOL_cs addIs [select_equality]) 1]); |
143 |
||
965 | 144 |
val if_False = prove_goalw HOL.thy [if_def] "(if False then x else y) = y" |
923 | 145 |
(fn _=>[fast_tac (HOL_cs addIs [select_equality]) 1]); |
146 |
||
965 | 147 |
val if_P = prove_goal HOL.thy "P ==> (if P then x else y) = x" |
923 | 148 |
(fn [prem] => [ stac (prem RS eqTrueI) 1, rtac if_True 1 ]); |
149 |
||
965 | 150 |
val if_not_P = prove_goal HOL.thy "~P ==> (if P then x else y) = y" |
923 | 151 |
(fn [prem] => [ stac (prem RS not_P_imp_P_iff_F) 1, rtac if_False 1 ]); |
152 |
||
153 |
val expand_if = prove_goal HOL.thy |
|
965 | 154 |
"P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))" |
923 | 155 |
(fn _=> [ (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1), |
2031 | 156 |
stac if_P 2, |
157 |
stac if_not_P 1, |
|
1465 | 158 |
REPEAT(fast_tac HOL_cs 1) ]); |
923 | 159 |
|
965 | 160 |
val if_bool_eq = prove_goal HOL.thy |
161 |
"(if P then Q else R) = ((P-->Q) & (~P-->R))" |
|
162 |
(fn _ => [rtac expand_if 1]); |
|
923 | 163 |
|
988 | 164 |
(*Add congruence rules for = (instead of ==) *) |
165 |
infix 4 addcongs; |
|
923 | 166 |
fun ss addcongs congs = ss addeqcongs (congs RL [eq_reflection]); |
167 |
||
1264 | 168 |
fun Addcongs congs = (simpset := !simpset addcongs congs); |
169 |
||
923 | 170 |
val mksimps_pairs = |
171 |
[("op -->", [mp]), ("op &", [conjunct1,conjunct2]), |
|
172 |
("All", [spec]), ("True", []), ("False", []), |
|
965 | 173 |
("If", [if_bool_eq RS iffD1])]; |
923 | 174 |
|
175 |
fun mksimps pairs = map mk_meta_eq o atomize pairs o gen_all; |
|
176 |
||
1922 | 177 |
val imp_cong = impI RSN |
178 |
(2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))" |
|
179 |
(fn _=> [fast_tac HOL_cs 1]) RS mp RS mp); |
|
180 |
||
181 |
val o_apply = prove_goalw HOL.thy [o_def] "(f o g)(x) = f(g(x))" |
|
182 |
(fn _ => [rtac refl 1]); |
|
183 |
||
1948
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
184 |
(*Miniscoping: pushing in existential quantifiers*) |
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
185 |
val ex_simps = map prover |
2031 | 186 |
["(EX x. P x & Q) = ((EX x.P x) & Q)", |
187 |
"(EX x. P & Q x) = (P & (EX x.Q x))", |
|
188 |
"(EX x. P x | Q) = ((EX x.P x) | Q)", |
|
189 |
"(EX x. P | Q x) = (P | (EX x.Q x))", |
|
190 |
"(EX x. P x --> Q) = ((ALL x.P x) --> Q)", |
|
191 |
"(EX x. P --> Q x) = (P --> (EX x.Q x))"]; |
|
1948
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
192 |
|
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
193 |
(*Miniscoping: pushing in universal quantifiers*) |
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
194 |
val all_simps = map prover |
2031 | 195 |
["(ALL x. P x & Q) = ((ALL x.P x) & Q)", |
196 |
"(ALL x. P & Q x) = (P & (ALL x.Q x))", |
|
197 |
"(ALL x. P x | Q) = ((ALL x.P x) | Q)", |
|
198 |
"(ALL x. P | Q x) = (P | (ALL x.Q x))", |
|
199 |
"(ALL x. P x --> Q) = ((EX x.P x) --> Q)", |
|
200 |
"(ALL x. P --> Q x) = (P --> (ALL x.Q x))"]; |
|
1948
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
201 |
|
923 | 202 |
val HOL_ss = empty_ss |
203 |
setmksimps (mksimps mksimps_pairs) |
|
204 |
setsolver (fn prems => resolve_tac (TrueI::refl::prems) ORELSE' atac |
|
205 |
ORELSE' etac FalseE) |
|
206 |
setsubgoaler asm_simp_tac |
|
1948
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
207 |
addsimps ([if_True, if_False, o_apply, imp_disj, conj_assoc, disj_assoc, |
2031 | 208 |
cases_simp] |
1948
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
209 |
@ ex_simps @ all_simps @ simp_thms) |
923 | 210 |
addcongs [imp_cong]; |
211 |
||
1922 | 212 |
|
213 |
(*In general it seems wrong to add distributive laws by default: they |
|
1948
78e5bfcbc1e9
Added miniscoping to the simplifier: quantifiers are now pushed in
paulson
parents:
1922
diff
changeset
|
214 |
might cause exponential blow-up. But imp_disj has been in for a while |
1922 | 215 |
and cannot be removed without affecting existing proofs. Moreover, |
216 |
rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the |
|
217 |
grounds that it allows simplification of R in the two cases.*) |
|
218 |
||
219 |
||
941 | 220 |
local val mktac = mk_case_split_tac (meta_eq_to_obj_eq RS iffD2) |
221 |
in |
|
222 |
fun split_tac splits = mktac (map mk_meta_eq splits) |
|
223 |
end; |
|
224 |
||
1722 | 225 |
local val mktac = mk_case_split_inside_tac (meta_eq_to_obj_eq RS iffD2) |
226 |
in |
|
227 |
fun split_inside_tac splits = mktac (map mk_meta_eq splits) |
|
228 |
end; |
|
229 |
||
923 | 230 |
|
2022 | 231 |
(* elimination of existential quantifiers in assumptions *) |
923 | 232 |
|
233 |
val ex_all_equiv = |
|
234 |
let val lemma1 = prove_goal HOL.thy |
|
235 |
"(? x. P(x) ==> PROP Q) ==> (!!x. P(x) ==> PROP Q)" |
|
236 |
(fn prems => [resolve_tac prems 1, etac exI 1]); |
|
237 |
val lemma2 = prove_goalw HOL.thy [Ex_def] |
|
238 |
"(!!x. P(x) ==> PROP Q) ==> (? x. P(x) ==> PROP Q)" |
|
239 |
(fn prems => [REPEAT(resolve_tac prems 1)]) |
|
240 |
in equal_intr lemma1 lemma2 end; |
|
241 |
||
242 |
(* '&' congruence rule: not included by default! |
|
243 |
May slow rewrite proofs down by as much as 50% *) |
|
244 |
||
2022 | 245 |
val conj_cong = |
246 |
let val th = prove_goal HOL.thy |
|
247 |
"(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))" |
|
2031 | 248 |
(fn _=> [fast_tac HOL_cs 1]) |
2022 | 249 |
in standard (impI RSN (2, th RS mp RS mp)) end; |
923 | 250 |
|
2022 | 251 |
val rev_conj_cong = |
252 |
let val th = prove_goal HOL.thy |
|
253 |
"(Q=Q')--> (Q'--> (P=P'))--> ((P&Q) = (P'&Q'))" |
|
2031 | 254 |
(fn _=> [fast_tac HOL_cs 1]) |
2022 | 255 |
in standard (impI RSN (2, th RS mp RS mp)) end; |
256 |
||
257 |
(* '|' congruence rule: not included by default! *) |
|
258 |
||
259 |
val disj_cong = |
|
260 |
let val th = prove_goal HOL.thy |
|
261 |
"(P=P')--> (~P'--> (Q=Q'))--> ((P|Q) = (P'|Q'))" |
|
2031 | 262 |
(fn _=> [fast_tac HOL_cs 1]) |
2022 | 263 |
in standard (impI RSN (2, th RS mp RS mp)) end; |
1548 | 264 |
|
923 | 265 |
(** 'if' congruence rules: neither included by default! *) |
266 |
||
267 |
(*Simplifies x assuming c and y assuming ~c*) |
|
268 |
val if_cong = prove_goal HOL.thy |
|
965 | 269 |
"[| b=c; c ==> x=u; ~c ==> y=v |] ==>\ |
270 |
\ (if b then x else y) = (if c then u else v)" |
|
923 | 271 |
(fn rew::prems => |
272 |
[stac rew 1, stac expand_if 1, stac expand_if 1, |
|
273 |
fast_tac (HOL_cs addDs prems) 1]); |
|
274 |
||
275 |
(*Prevents simplification of x and y: much faster*) |
|
276 |
val if_weak_cong = prove_goal HOL.thy |
|
965 | 277 |
"b=c ==> (if b then x else y) = (if c then x else y)" |
923 | 278 |
(fn [prem] => [rtac (prem RS arg_cong) 1]); |
279 |
||
280 |
(*Prevents simplification of t: much faster*) |
|
281 |
val let_weak_cong = prove_goal HOL.thy |
|
282 |
"a = b ==> (let x=a in t(x)) = (let x=b in t(x))" |
|
283 |
(fn [prem] => [rtac (prem RS arg_cong) 1]); |
|
284 |
||
285 |
end; |
|
286 |
||
287 |
fun prove nm thm = qed_goal nm HOL.thy thm (fn _ => [fast_tac HOL_cs 1]); |
|
288 |
||
289 |
prove "conj_commute" "(P&Q) = (Q&P)"; |
|
290 |
prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))"; |
|
291 |
val conj_comms = [conj_commute, conj_left_commute]; |
|
292 |
||
1922 | 293 |
prove "disj_commute" "(P|Q) = (Q|P)"; |
294 |
prove "disj_left_commute" "(P|(Q|R)) = (Q|(P|R))"; |
|
295 |
val disj_comms = [disj_commute, disj_left_commute]; |
|
296 |
||
923 | 297 |
prove "conj_disj_distribL" "(P&(Q|R)) = (P&Q | P&R)"; |
298 |
prove "conj_disj_distribR" "((P|Q)&R) = (P&R | Q&R)"; |
|
1485
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1465
diff
changeset
|
299 |
|
1892 | 300 |
prove "disj_conj_distribL" "(P|(Q&R)) = ((P|Q) & (P|R))"; |
301 |
prove "disj_conj_distribR" "((P&Q)|R) = ((P|R) & (Q|R))"; |
|
302 |
||
303 |
prove "imp_conj_distrib" "(P --> (Q&R)) = ((P-->Q) & (P-->R))"; |
|
1922 | 304 |
prove "imp_conj" "((P&Q)-->R) = (P --> (Q --> R))"; |
1892 | 305 |
|
1485
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1465
diff
changeset
|
306 |
prove "de_Morgan_disj" "(~(P | Q)) = (~P & ~Q)"; |
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1465
diff
changeset
|
307 |
prove "de_Morgan_conj" "(~(P & Q)) = (~P | ~Q)"; |
1922 | 308 |
prove "not_iff" "(P~=Q) = (P = (~Q))"; |
1485
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1465
diff
changeset
|
309 |
|
1660 | 310 |
prove "not_all" "(~ (! x.P(x))) = (? x.~P(x))"; |
1922 | 311 |
prove "imp_all" "((! x. P x) --> Q) = (? x. P x --> Q)"; |
1660 | 312 |
prove "not_ex" "(~ (? x.P(x))) = (! x.~P(x))"; |
1922 | 313 |
prove "imp_ex" "((? x. P x) --> Q) = (! x. P x --> Q)"; |
1660 | 314 |
|
1655 | 315 |
prove "ex_disj_distrib" "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))"; |
316 |
prove "all_conj_distrib" "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))"; |
|
317 |
||
1758 | 318 |
|
1655 | 319 |
qed_goal "if_cancel" HOL.thy "(if c then x else x) = x" |
320 |
(fn _ => [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]); |
|
321 |
||
322 |
qed_goal "if_distrib" HOL.thy |
|
323 |
"f(if c then x else y) = (if c then f x else f y)" |
|
324 |
(fn _ => [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]); |
|
325 |
||
1874 | 326 |
qed_goalw "o_assoc" HOL.thy [o_def] "f o (g o h) = (f o g o h)" |
1655 | 327 |
(fn _=>[rtac ext 1, rtac refl 1]); |
1984 | 328 |
|
329 |
||
330 |
||
331 |
||
332 |
(*** Install simpsets and datatypes in theory structure ***) |
|
333 |
||
334 |
simpset := HOL_ss; |
|
335 |
||
336 |
exception SS_DATA of simpset; |
|
337 |
||
338 |
let fun merge [] = SS_DATA empty_ss |
|
339 |
| merge ss = let val ss = map (fn SS_DATA x => x) ss; |
|
340 |
in SS_DATA (foldl merge_ss (hd ss, tl ss)) end; |
|
341 |
||
342 |
fun put (SS_DATA ss) = simpset := ss; |
|
343 |
||
344 |
fun get () = SS_DATA (!simpset); |
|
345 |
in add_thydata "HOL" |
|
346 |
("simpset", ThyMethods {merge = merge, put = put, get = get}) |
|
347 |
end; |
|
348 |
||
349 |
type dtype_info = {case_const:term, case_rewrites:thm list, |
|
350 |
constructors:term list, nchotomy:thm, case_cong:thm}; |
|
351 |
||
352 |
exception DT_DATA of (string * dtype_info) list; |
|
353 |
val datatypes = ref [] : (string * dtype_info) list ref; |
|
354 |
||
355 |
let fun merge [] = DT_DATA [] |
|
356 |
| merge ds = |
|
357 |
let val ds = map (fn DT_DATA x => x) ds; |
|
358 |
in DT_DATA (foldl (gen_union eq_fst) (hd ds, tl ds)) end; |
|
359 |
||
360 |
fun put (DT_DATA ds) = datatypes := ds; |
|
361 |
||
362 |
fun get () = DT_DATA (!datatypes); |
|
363 |
in add_thydata "HOL" |
|
364 |
("datatypes", ThyMethods {merge = merge, put = put, get = get}) |
|
365 |
end; |
|
366 |
||
367 |
||
368 |
add_thy_reader_file "thy_data.ML"; |