src/ZF/simpdata.ML
 author paulson Wed Jan 27 10:31:31 1999 +0100 (1999-01-27 ago) changeset 6153 bff90585cce5 parent 5553 ae42b36a50c2 child 7570 a9391550eea1 permissions -rw-r--r--
new typechecking solver for the simplifier
```     1 (*  Title:      ZF/simpdata
```
```     2     ID:         \$Id\$
```
```     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     4     Copyright   1991  University of Cambridge
```
```     5
```
```     6 Rewriting for ZF set theory: specialized extraction of rewrites from theorems
```
```     7 *)
```
```     8
```
```     9 (** Rewriting **)
```
```    10
```
```    11 local
```
```    12   (*For proving rewrite rules*)
```
```    13   fun prover s = (prove_goal thy s (fn _ => [Blast_tac 1]));
```
```    14
```
```    15 in
```
```    16
```
```    17 val ball_simps = map prover
```
```    18     ["(ALL x:A. P(x) | Q)   <-> ((ALL x:A. P(x)) | Q)",
```
```    19      "(ALL x:A. P | Q(x))   <-> (P | (ALL x:A. Q(x)))",
```
```    20      "(ALL x:A. P --> Q(x)) <-> (P --> (ALL x:A. Q(x)))",
```
```    21      "(ALL x:A. P(x) --> Q) <-> ((EX x:A. P(x)) --> Q)",
```
```    22      "(ALL x:0.P(x)) <-> True",
```
```    23      "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i. P(x))",
```
```    24      "(ALL x:cons(a,B).P(x)) <-> P(a) & (ALL x:B. P(x))",
```
```    25      "(ALL x:RepFun(A,f). P(x)) <-> (ALL y:A. P(f(y)))",
```
```    26      "(ALL x:Union(A).P(x)) <-> (ALL y:A. ALL x:y. P(x))",
```
```    27      "(ALL x:Collect(A,Q).P(x)) <-> (ALL x:A. Q(x) --> P(x))",
```
```    28      "(~(ALL x:A. P(x))) <-> (EX x:A. ~P(x))"];
```
```    29
```
```    30 val ball_conj_distrib =
```
```    31     prover "(ALL x:A. P(x) & Q(x)) <-> ((ALL x:A. P(x)) & (ALL x:A. Q(x)))";
```
```    32
```
```    33 val bex_simps = map prover
```
```    34     ["(EX x:A. P(x) & Q) <-> ((EX x:A. P(x)) & Q)",
```
```    35      "(EX x:A. P & Q(x)) <-> (P & (EX x:A. Q(x)))",
```
```    36      "(EX x:0.P(x)) <-> False",
```
```    37      "(EX x:succ(i).P(x)) <-> P(i) | (EX x:i. P(x))",
```
```    38      "(EX x:cons(a,B).P(x)) <-> P(a) | (EX x:B. P(x))",
```
```    39      "(EX x:RepFun(A,f). P(x)) <-> (EX y:A. P(f(y)))",
```
```    40      "(EX x:Union(A).P(x)) <-> (EX y:A. EX x:y.  P(x))",
```
```    41      "(EX x:Collect(A,Q).P(x)) <-> (EX x:A. Q(x) & P(x))",
```
```    42      "(~(EX x:A. P(x))) <-> (ALL x:A. ~P(x))"];
```
```    43
```
```    44 val bex_disj_distrib =
```
```    45     prover "(EX x:A. P(x) | Q(x)) <-> ((EX x:A. P(x)) | (EX x:A. Q(x)))";
```
```    46
```
```    47 val Rep_simps = map prover
```
```    48     ["{x. y:0, R(x,y)} = 0",	(*Replace*)
```
```    49      "{x:0. P(x)} = 0",		(*Collect*)
```
```    50      "{x:A. False} = 0",
```
```    51      "{x:A. True} = A",
```
```    52      "RepFun(0,f) = 0",		(*RepFun*)
```
```    53      "RepFun(succ(i),f) = cons(f(i), RepFun(i,f))",
```
```    54      "RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))"]
```
```    55
```
```    56 val misc_simps = map prover
```
```    57     ["0 Un A = A",  "A Un 0 = A",
```
```    58      "0 Int A = 0", "A Int 0 = 0",
```
```    59      "0-A = 0",     "A-0 = A",
```
```    60      "Union(0) = 0",
```
```    61      "Union(cons(b,A)) = b Un Union(A)",
```
```    62      "Inter({b}) = b"]
```
```    63
```
```    64 end;
```
```    65
```
```    66 Addsimps (ball_simps @ bex_simps @ Rep_simps @ misc_simps);
```
```    67
```
```    68
```
```    69 (** New version of mk_rew_rules **)
```
```    70
```
```    71 (*Should False yield False<->True, or should it solve goals some other way?*)
```
```    72
```
```    73 (*Analyse a theorem to atomic rewrite rules*)
```
```    74 fun atomize (conn_pairs, mem_pairs) th =
```
```    75   let fun tryrules pairs t =
```
```    76           case head_of t of
```
```    77               Const(a,_) =>
```
```    78                 (case assoc(pairs,a) of
```
```    79                      Some rls => flat (map (atomize (conn_pairs, mem_pairs))
```
```    80                                        ([th] RL rls))
```
```    81                    | None     => [th])
```
```    82             | _ => [th]
```
```    83   in case concl_of th of
```
```    84          Const("Trueprop",_) \$ P =>
```
```    85             (case P of
```
```    86                  Const("op :",_) \$ a \$ b => tryrules mem_pairs b
```
```    87                | Const("True",_)         => []
```
```    88                | Const("False",_)        => []
```
```    89                | A => tryrules conn_pairs A)
```
```    90        | _                       => [th]
```
```    91   end;
```
```    92
```
```    93 (*Analyse a rigid formula*)
```
```    94 val ZF_conn_pairs =
```
```    95   [("Ball",     [bspec]),
```
```    96    ("All",      [spec]),
```
```    97    ("op -->",   [mp]),
```
```    98    ("op &",     [conjunct1,conjunct2])];
```
```    99
```
```   100 (*Analyse a:b, where b is rigid*)
```
```   101 val ZF_mem_pairs =
```
```   102   [("Collect",  [CollectD1,CollectD2]),
```
```   103    ("op -",     [DiffD1,DiffD2]),
```
```   104    ("op Int",   [IntD1,IntD2])];
```
```   105
```
```   106 val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
```
```   107
```
```   108 simpset_ref() := simpset() setmksimps (map mk_eq o ZF_atomize o gen_all)
```
```   109                            addsplits [split_if]
```
```   110                            setSolver Type_solver_tac;
```
```   111
```
```   112 val ZF_ss = simpset();
```