src/ZF/simpdata.ML
author wenzelm
Fri Oct 10 18:23:31 1997 +0200 (1997-10-10 ago)
changeset 3840 e0baea4d485a
parent 3425 fc4ca570d185
child 3859 810fccb1ebe4
permissions -rw-r--r--
fixed dots;
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@3425
    11
local
paulson@3425
    12
  (*For proving rewrite rules*)
paulson@3425
    13
  fun prover s = (prove_goal ZF.thy s (fn _ => [Blast_tac 1]));
paulson@3425
    14
paulson@3425
    15
in
clasohm@0
    16
paulson@3425
    17
val ball_simps = map prover
paulson@3425
    18
    ["(ALL x:A. P(x) | Q)   <-> ((ALL x:A. P(x)) | Q)",
paulson@3425
    19
     "(ALL x:A. P | Q(x))   <-> (P | (ALL x:A. Q(x)))",
paulson@3425
    20
     "(ALL x:A. P --> Q(x)) <-> (P --> (ALL x:A. Q(x)))",
paulson@3425
    21
     "(ALL x:A. P(x) --> Q) <-> ((EX x:A. P(x)) --> Q)",
paulson@3425
    22
     "(ALL x:0.P(x)) <-> True",
wenzelm@3840
    23
     "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i. P(x))",
wenzelm@3840
    24
     "(ALL x:cons(a,B).P(x)) <-> P(a) & (ALL x:B. P(x))",
paulson@2482
    25
     "(ALL x:RepFun(A,f). P(x)) <-> (ALL y:A. P(f(y)))",
paulson@2482
    26
     "(ALL x:Union(A).P(x)) <-> (ALL y:A. ALL x:y. P(x))",
paulson@2482
    27
     "(ALL x:Collect(A,Q).P(x)) <-> (ALL x:A. Q(x) --> P(x))"];
paulson@2482
    28
paulson@3425
    29
val ball_conj_distrib = 
paulson@3425
    30
    prover "(ALL x:A. P(x) & Q(x)) <-> ((ALL x:A. P(x)) & (ALL x:A. Q(x)))";
paulson@3425
    31
paulson@3425
    32
val bex_simps = map prover
paulson@3425
    33
    ["(EX x:A. P(x) & Q) <-> ((EX x:A. P(x)) & Q)",
paulson@3425
    34
     "(EX x:A. P & Q(x)) <-> (P & (EX x:A. Q(x)))",
paulson@3425
    35
     "(EX x:0.P(x)) <-> False",
wenzelm@3840
    36
     "(EX x:succ(i).P(x)) <-> P(i) | (EX x:i. P(x))",
wenzelm@3840
    37
     "(EX x:cons(a,B).P(x)) <-> P(a) | (EX x:B. P(x))",
paulson@2482
    38
     "(EX x:RepFun(A,f). P(x)) <-> (EX y:A. P(f(y)))",
paulson@2482
    39
     "(EX x:Union(A).P(x)) <-> (EX y:A. EX x:y.  P(x))",
paulson@2482
    40
     "(EX x:Collect(A,Q).P(x)) <-> (EX x:A. Q(x) & P(x))"];
paulson@2482
    41
paulson@3425
    42
val bex_disj_distrib = 
paulson@3425
    43
    prover "(EX x:A. P(x) | Q(x)) <-> ((EX x:A. P(x)) | (EX x:A. Q(x)))";
paulson@3425
    44
paulson@3425
    45
val Rep_simps = map prover
paulson@3425
    46
    ["{x:0. P(x)} = 0",
paulson@3425
    47
     "{x:A. False} = 0",
paulson@3425
    48
     "{x:A. True} = A",
paulson@3425
    49
     "RepFun(0,f) = 0",
paulson@3425
    50
     "RepFun(succ(i),f) = cons(f(i), RepFun(i,f))",
paulson@3425
    51
     "RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))"]
clasohm@0
    52
paulson@3425
    53
val misc_simps = map prover
paulson@3425
    54
    ["0 Un A = A",  "A Un 0 = A",
paulson@3425
    55
     "0 Int A = 0", "A Int 0 = 0",
paulson@3425
    56
     "0-A = 0",     "A-0 = A",
paulson@3425
    57
     "Union(0) = 0",
paulson@3425
    58
     "Union(cons(b,A)) = b Un Union(A)",
paulson@3425
    59
     "Inter({b}) = b"]
clasohm@0
    60
paulson@3425
    61
end;
paulson@3425
    62
paulson@3425
    63
Addsimps (ball_simps @ bex_simps @ Rep_simps @ misc_simps);
paulson@3425
    64
clasohm@0
    65
clasohm@0
    66
(** New version of mk_rew_rules **)
clasohm@0
    67
clasohm@0
    68
(*Should False yield False<->True, or should it solve goals some other way?*)
clasohm@0
    69
lcp@1036
    70
(*Analyse a theorem to atomic rewrite rules*)
lcp@1036
    71
fun atomize (conn_pairs, mem_pairs) th = 
lcp@1036
    72
  let fun tryrules pairs t =
clasohm@1461
    73
          case head_of t of
clasohm@1461
    74
              Const(a,_) => 
clasohm@1461
    75
                (case assoc(pairs,a) of
clasohm@1461
    76
                     Some rls => flat (map (atomize (conn_pairs, mem_pairs))
clasohm@1461
    77
                                       ([th] RL rls))
clasohm@1461
    78
                   | None     => [th])
clasohm@1461
    79
            | _ => [th]
lcp@1036
    80
  in case concl_of th of 
clasohm@1461
    81
         Const("Trueprop",_) $ P => 
clasohm@1461
    82
            (case P of
clasohm@1461
    83
                 Const("op :",_) $ a $ b => tryrules mem_pairs b
clasohm@1461
    84
               | Const("True",_)         => []
clasohm@1461
    85
               | Const("False",_)        => []
clasohm@1461
    86
               | A => tryrules conn_pairs A)
lcp@1036
    87
       | _                       => [th]
lcp@1036
    88
  end;
lcp@1036
    89
clasohm@0
    90
(*Analyse a rigid formula*)
lcp@1036
    91
val ZF_conn_pairs =
clasohm@1461
    92
  [("Ball",     [bspec]), 
clasohm@1461
    93
   ("All",      [spec]),
clasohm@1461
    94
   ("op -->",   [mp]),
clasohm@1461
    95
   ("op &",     [conjunct1,conjunct2])];
clasohm@0
    96
clasohm@0
    97
(*Analyse a:b, where b is rigid*)
lcp@1036
    98
val ZF_mem_pairs = 
clasohm@1461
    99
  [("Collect",  [CollectD1,CollectD2]),
clasohm@1461
   100
   ("op -",     [DiffD1,DiffD2]),
clasohm@1461
   101
   ("op Int",   [IntD1,IntD2])];
clasohm@0
   102
lcp@1036
   103
val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
lcp@1036
   104
paulson@2469
   105
simpset := !simpset setmksimps (map mk_meta_eq o ZF_atomize o gen_all);
paulson@2469
   106
paulson@2469
   107
val ZF_ss = !simpset;