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;