src/ZF/simpdata.ML
author nipkow
Tue Sep 21 19:11:07 1999 +0200 (1999-09-21)
changeset 7570 a9391550eea1
parent 6153 bff90585cce5
child 9570 e16e168984e1
permissions -rw-r--r--
Mod because of new solver interface.
     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 (mk_solver "types" Type_solver_tac);
   111 
   112 val ZF_ss = simpset();