src/ZF/simpdata.ML
 author haftmann Mon Sep 12 18:20:32 2005 +0200 (2005-09-12 ago) changeset 17325 d9d50222808e parent 17002 fb9261990ffe child 17876 b9c92f384109 permissions -rw-r--r--
introduced new-style AList operations
1 (*  Title:      ZF/simpdata
2     ID:         \$Id\$
3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
4     Copyright   1991  University of Cambridge
6 Rewriting for ZF set theory: specialized extraction of rewrites from theorems
7 *)
9 (*** New version of mk_rew_rules ***)
11 (*Should False yield False<->True, or should it solve goals some other way?*)
13 (*Analyse a theorem to atomic rewrite rules*)
14 fun atomize (conn_pairs, mem_pairs) th =
15   let fun tryrules pairs t =
16           case head_of t of
17               Const(a,_) =>
18                 (case AList.lookup (op =) pairs a of
19                      SOME rls => List.concat (map (atomize (conn_pairs, mem_pairs))
20                                        ([th] RL rls))
21                    | NONE     => [th])
22             | _ => [th]
23   in case concl_of th of
24          Const("Trueprop",_) \$ P =>
25             (case P of
26                  Const("op :",_) \$ a \$ b => tryrules mem_pairs b
27                | Const("True",_)         => []
28                | Const("False",_)        => []
29                | A => tryrules conn_pairs A)
30        | _                       => [th]
31   end;
33 (*Analyse a rigid formula*)
34 val ZF_conn_pairs =
35   [("Ball",     [bspec]),
36    ("All",      [spec]),
37    ("op -->",   [mp]),
38    ("op &",     [conjunct1,conjunct2])];
40 (*Analyse a:b, where b is rigid*)
41 val ZF_mem_pairs =
42   [("Collect",  [CollectD1,CollectD2]),
43    ("op -",     [DiffD1,DiffD2]),
44    ("op Int",   [IntD1,IntD2])];
46 val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
48 val type_solver =
49   mk_solver "types" (fn prems => TCSET' (fn tcset => type_solver_tac tcset prems));
51 simpset_ref() :=
52   simpset() setmksimps (map mk_eq o ZF_atomize o gen_all)
54   setSolver type_solver;
56 local
58 fun prove_bex_tac ss = unfold_tac ss [Bex_def] THEN Quantifier1.prove_one_point_ex_tac;
59 val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
61 fun prove_ball_tac ss = unfold_tac ss [Ball_def] THEN Quantifier1.prove_one_point_all_tac;
62 val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
64 in
66 val defBEX_regroup = Simplifier.simproc (the_context ())
67   "defined BEX" ["EX x:A. P(x) & Q(x)"] rearrange_bex;
69 val defBALL_regroup = Simplifier.simproc (the_context ())
70   "defined BALL" ["ALL x:A. P(x) --> Q(x)"] rearrange_ball;
72 end;
74 Addsimprocs [defBALL_regroup, defBEX_regroup];
77 val ZF_ss = simpset();