src/ZF/simpdata.ML
author paulson
Tue Jan 07 12:37:07 1997 +0100 (1997-01-07 ago)
changeset 2482 87383dd9f4b5
parent 2469 b50b8c0eec01
child 2496 40efb87985b5
permissions -rw-r--r--
Default rewrite rules for quantification over Collect(A,P)
clasohm@0
     1
(*  Title:      ZF/simpdata
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1991  University of Cambridge
clasohm@0
     5
paulson@2469
     6
Rewriting for ZF set theory: specialized extraction of rewrites from theorems
clasohm@0
     7
*)
clasohm@0
     8
paulson@2469
     9
(** Rewriting **)
clasohm@0
    10
paulson@2469
    11
(*For proving rewrite rules*)
paulson@2469
    12
fun prove_fun s = 
paulson@2469
    13
    (writeln s;  prove_goal thy s
paulson@2469
    14
       (fn prems => [ (cut_facts_tac prems 1), 
paulson@2469
    15
                      (fast_tac (!claset addSIs [equalityI]) 1) ]));
clasohm@0
    16
paulson@2469
    17
(*Are all these really suitable?*)
paulson@2482
    18
val ball_simps = map prove_fun
paulson@2482
    19
    ["(ALL x:0.P(x)) <-> True",
paulson@2482
    20
     "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i.P(x))",
paulson@2482
    21
     "(ALL x:cons(a,B).P(x)) <-> P(a) & (ALL x:B.P(x))",
paulson@2482
    22
     "(ALL x:RepFun(A,f). P(x)) <-> (ALL y:A. P(f(y)))",
paulson@2482
    23
     "(ALL x:Union(A).P(x)) <-> (ALL y:A. ALL x:y. P(x))",
paulson@2482
    24
     "(ALL x:Collect(A,Q).P(x)) <-> (ALL x:A. Q(x) --> P(x))"];
paulson@2482
    25
paulson@2482
    26
val bex_simps = map prove_fun
paulson@2482
    27
    ["(EX x:0.P(x)) <-> False",
paulson@2482
    28
     "(EX x:succ(i).P(x)) <-> P(i) | (EX x:i.P(x))",
paulson@2482
    29
     "(EX x:cons(a,B).P(x)) <-> P(a) | (EX x:B.P(x))",
paulson@2482
    30
     "(EX x:RepFun(A,f). P(x)) <-> (EX y:A. P(f(y)))",
paulson@2482
    31
     "(EX x:Union(A).P(x)) <-> (EX y:A. EX x:y.  P(x))",
paulson@2482
    32
     "(EX x:Collect(A,Q).P(x)) <-> (EX x:A. Q(x) & P(x))"];
paulson@2482
    33
paulson@2482
    34
Addsimps (ball_simps @ bex_simps);
clasohm@0
    35
paulson@2469
    36
Addsimps (map prove_fun
paulson@2469
    37
	  ["{x:0. P(x)} = 0",
paulson@2469
    38
	   "{x:A. False} = 0",
paulson@2469
    39
	   "{x:A. True} = A",
paulson@2469
    40
	   "RepFun(0,f) = 0",
paulson@2469
    41
	   "RepFun(succ(i),f) = cons(f(i), RepFun(i,f))",
paulson@2469
    42
	   "RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))"]);
clasohm@0
    43
paulson@2469
    44
Addsimps (map prove_fun
paulson@2469
    45
	  ["0 Un A = A",  "A Un 0 = A",
paulson@2469
    46
	   "0 Int A = 0", "A Int 0 = 0",
paulson@2469
    47
	   "0-A = 0",     "A-0 = A",
paulson@2469
    48
	   "Union(0) = 0",
paulson@2469
    49
	   "Union(cons(b,A)) = b Un Union(A)",
paulson@2469
    50
	   "Inter({b}) = b"]);
clasohm@0
    51
clasohm@0
    52
(** New version of mk_rew_rules **)
clasohm@0
    53
clasohm@0
    54
(*Should False yield False<->True, or should it solve goals some other way?*)
clasohm@0
    55
lcp@1036
    56
(*Analyse a theorem to atomic rewrite rules*)
lcp@1036
    57
fun atomize (conn_pairs, mem_pairs) th = 
lcp@1036
    58
  let fun tryrules pairs t =
clasohm@1461
    59
          case head_of t of
clasohm@1461
    60
              Const(a,_) => 
clasohm@1461
    61
                (case assoc(pairs,a) of
clasohm@1461
    62
                     Some rls => flat (map (atomize (conn_pairs, mem_pairs))
clasohm@1461
    63
                                       ([th] RL rls))
clasohm@1461
    64
                   | None     => [th])
clasohm@1461
    65
            | _ => [th]
lcp@1036
    66
  in case concl_of th of 
clasohm@1461
    67
         Const("Trueprop",_) $ P => 
clasohm@1461
    68
            (case P of
clasohm@1461
    69
                 Const("op :",_) $ a $ b => tryrules mem_pairs b
clasohm@1461
    70
               | Const("True",_)         => []
clasohm@1461
    71
               | Const("False",_)        => []
clasohm@1461
    72
               | A => tryrules conn_pairs A)
lcp@1036
    73
       | _                       => [th]
lcp@1036
    74
  end;
lcp@1036
    75
clasohm@0
    76
(*Analyse a rigid formula*)
lcp@1036
    77
val ZF_conn_pairs =
clasohm@1461
    78
  [("Ball",     [bspec]), 
clasohm@1461
    79
   ("All",      [spec]),
clasohm@1461
    80
   ("op -->",   [mp]),
clasohm@1461
    81
   ("op &",     [conjunct1,conjunct2])];
clasohm@0
    82
clasohm@0
    83
(*Analyse a:b, where b is rigid*)
lcp@1036
    84
val ZF_mem_pairs = 
clasohm@1461
    85
  [("Collect",  [CollectD1,CollectD2]),
clasohm@1461
    86
   ("op -",     [DiffD1,DiffD2]),
clasohm@1461
    87
   ("op Int",   [IntD1,IntD2])];
clasohm@0
    88
lcp@1036
    89
val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
lcp@1036
    90
paulson@2469
    91
simpset := !simpset setmksimps (map mk_meta_eq o ZF_atomize o gen_all);
paulson@2469
    92
paulson@2469
    93
val ZF_ss = !simpset;