File ‹simpdata.ML›
fun atomize (conn_pairs, mem_pairs) th =
let fun tryrules pairs t =
case head_of t of
Const(a,_) =>
(case AList.lookup (op =) pairs a of
SOME rls => maps (atomize (conn_pairs, mem_pairs)) ([th] RL rls)
| NONE => [th])
| _ => [th]
in case Thm.concl_of th of
\<^Const_>‹Trueprop for P› =>
(case P of
\<^Const_>‹mem for a b› => tryrules mem_pairs b
| \<^Const_>‹True› => []
| \<^Const_>‹False› => []
| A => tryrules conn_pairs A)
| _ => [th]
end;
val ZF_conn_pairs =
[(\<^const_name>‹Ball›, [@{thm bspec}]),
(\<^const_name>‹All›, [@{thm spec}]),
(\<^const_name>‹imp›, [@{thm mp}]),
(\<^const_name>‹conj›, [@{thm conjunct1}, @{thm conjunct2}])];
val ZF_mem_pairs =
[(\<^const_name>‹Collect›, [@{thm CollectD1}, @{thm CollectD2}]),
(\<^const_name>‹Diff›, [@{thm DiffD1}, @{thm DiffD2}]),
(\<^const_name>‹Int›, [@{thm IntD1}, @{thm IntD2}])];
val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);