1(*  Title:      ZF/simpdata.ML
2    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3    Copyright   1991  University of Cambridge
4
5Rewriting for ZF set theory: specialized extraction of rewrites from theorems.
6*)
7
8(*** New version of mk_rew_rules ***)
9
10(*Should False yield False<->True, or should it solve goals some other way?*)
11
12(*Analyse a theorem to atomic rewrite rules*)
13fun atomize (conn_pairs, mem_pairs) th =
14  let fun tryrules pairs t =
15          case head_of t of
16              Const(a,_) =>
17                (case AList.lookup (op =) pairs a of
18                     SOME rls => maps (atomize (conn_pairs, mem_pairs)) ([th] RL rls)
19                   | NONE => [th])
20            | _ => [th]
21  in case Thm.concl_of th of
22         Const(\<^const_name>\<open>Trueprop\<close>,_) $ P =>
23            (case P of
24                 Const(\<^const_name>\<open>mem\<close>,_) $ a $ b => tryrules mem_pairs b
25               | Const(\<^const_name>\<open>True\<close>,_)         => []
26               | Const(\<^const_name>\<open>False\<close>,_)        => []
27               | A => tryrules conn_pairs A)
28       | _                       => [th]
29  end;
30
31(*Analyse a rigid formula*)
32val ZF_conn_pairs =
33  [(\<^const_name>\<open>Ball\<close>, [@{thm bspec}]),
34   (\<^const_name>\<open>All\<close>, [@{thm spec}]),
35   (\<^const_name>\<open>imp\<close>, [@{thm mp}]),
36   (\<^const_name>\<open>conj\<close>, [@{thm conjunct1}, @{thm conjunct2}])];
37
38(*Analyse a:b, where b is rigid*)
39val ZF_mem_pairs =
40  [(\<^const_name>\<open>Collect\<close>, [@{thm CollectD1}, @{thm CollectD2}]),
41   (\<^const_name>\<open>Diff\<close>, [@{thm DiffD1}, @{thm DiffD2}]),
42   (\<^const_name>\<open>Int\<close>, [@{thm IntD1}, @{thm IntD2}])];
43
44val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
45
46