src/ZF/simpdata.ML
 author paulson Thu Jan 09 10:20:03 1997 +0100 (1997-01-09 ago) changeset 2496 40efb87985b5 parent 2482 87383dd9f4b5 child 2876 02c12d4c8b97 permissions -rw-r--r--
Removal of needless "addIs [equality]", etc.
```     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 (*For proving rewrite rules*)
```
```    12 fun prove_fun s =
```
```    13     (writeln s;  prove_goal thy s
```
```    14        (fn prems => [ (cut_facts_tac prems 1), (Fast_tac 1) ]));
```
```    15
```
```    16 (*Are all these really suitable?*)
```
```    17 val ball_simps = map prove_fun
```
```    18     ["(ALL x:0.P(x)) <-> True",
```
```    19      "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i.P(x))",
```
```    20      "(ALL x:cons(a,B).P(x)) <-> P(a) & (ALL x:B.P(x))",
```
```    21      "(ALL x:RepFun(A,f). P(x)) <-> (ALL y:A. P(f(y)))",
```
```    22      "(ALL x:Union(A).P(x)) <-> (ALL y:A. ALL x:y. P(x))",
```
```    23      "(ALL x:Collect(A,Q).P(x)) <-> (ALL x:A. Q(x) --> P(x))"];
```
```    24
```
```    25 val bex_simps = map prove_fun
```
```    26     ["(EX x:0.P(x)) <-> False",
```
```    27      "(EX x:succ(i).P(x)) <-> P(i) | (EX x:i.P(x))",
```
```    28      "(EX x:cons(a,B).P(x)) <-> P(a) | (EX x:B.P(x))",
```
```    29      "(EX x:RepFun(A,f). P(x)) <-> (EX y:A. P(f(y)))",
```
```    30      "(EX x:Union(A).P(x)) <-> (EX y:A. EX x:y.  P(x))",
```
```    31      "(EX x:Collect(A,Q).P(x)) <-> (EX x:A. Q(x) & P(x))"];
```
```    32
```
```    33 Addsimps (ball_simps @ bex_simps);
```
```    34
```
```    35 Addsimps (map prove_fun
```
```    36 	  ["{x:0. P(x)} = 0",
```
```    37 	   "{x:A. False} = 0",
```
```    38 	   "{x:A. True} = A",
```
```    39 	   "RepFun(0,f) = 0",
```
```    40 	   "RepFun(succ(i),f) = cons(f(i), RepFun(i,f))",
```
```    41 	   "RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))"]);
```
```    42
```
```    43 Addsimps (map prove_fun
```
```    44 	  ["0 Un A = A",  "A Un 0 = A",
```
```    45 	   "0 Int A = 0", "A Int 0 = 0",
```
```    46 	   "0-A = 0",     "A-0 = A",
```
```    47 	   "Union(0) = 0",
```
```    48 	   "Union(cons(b,A)) = b Un Union(A)",
```
```    49 	   "Inter({b}) = b"]);
```
```    50
```
```    51 (** New version of mk_rew_rules **)
```
```    52
```
```    53 (*Should False yield False<->True, or should it solve goals some other way?*)
```
```    54
```
```    55 (*Analyse a theorem to atomic rewrite rules*)
```
```    56 fun atomize (conn_pairs, mem_pairs) th =
```
```    57   let fun tryrules pairs t =
```
```    58           case head_of t of
```
```    59               Const(a,_) =>
```
```    60                 (case assoc(pairs,a) of
```
```    61                      Some rls => flat (map (atomize (conn_pairs, mem_pairs))
```
```    62                                        ([th] RL rls))
```
```    63                    | None     => [th])
```
```    64             | _ => [th]
```
```    65   in case concl_of th of
```
```    66          Const("Trueprop",_) \$ P =>
```
```    67             (case P of
```
```    68                  Const("op :",_) \$ a \$ b => tryrules mem_pairs b
```
```    69                | Const("True",_)         => []
```
```    70                | Const("False",_)        => []
```
```    71                | A => tryrules conn_pairs A)
```
```    72        | _                       => [th]
```
```    73   end;
```
```    74
```
```    75 (*Analyse a rigid formula*)
```
```    76 val ZF_conn_pairs =
```
```    77   [("Ball",     [bspec]),
```
```    78    ("All",      [spec]),
```
```    79    ("op -->",   [mp]),
```
```    80    ("op &",     [conjunct1,conjunct2])];
```
```    81
```
```    82 (*Analyse a:b, where b is rigid*)
```
```    83 val ZF_mem_pairs =
```
```    84   [("Collect",  [CollectD1,CollectD2]),
```
```    85    ("op -",     [DiffD1,DiffD2]),
```
```    86    ("op Int",   [IntD1,IntD2])];
```
```    87
```
```    88 val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
```
```    89
```
```    90 simpset := !simpset setmksimps (map mk_meta_eq o ZF_atomize o gen_all);
```
```    91
```
```    92 val ZF_ss = !simpset;
```