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.
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@5325
    13
  fun prover s = (prove_goal 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))",
nipkow@3859
    27
     "(ALL x:Collect(A,Q).P(x)) <-> (ALL x:A. Q(x) --> P(x))",
nipkow@3859
    28
     "(~(ALL x:A. P(x))) <-> (EX x:A. ~P(x))"];
paulson@2482
    29
paulson@3425
    30
val ball_conj_distrib = 
paulson@3425
    31
    prover "(ALL x:A. P(x) & Q(x)) <-> ((ALL x:A. P(x)) & (ALL x:A. Q(x)))";
paulson@3425
    32
paulson@3425
    33
val bex_simps = map prover
paulson@3425
    34
    ["(EX x:A. P(x) & Q) <-> ((EX x:A. P(x)) & Q)",
paulson@3425
    35
     "(EX x:A. P & Q(x)) <-> (P & (EX x:A. Q(x)))",
paulson@3425
    36
     "(EX x:0.P(x)) <-> False",
wenzelm@3840
    37
     "(EX x:succ(i).P(x)) <-> P(i) | (EX x:i. P(x))",
wenzelm@3840
    38
     "(EX x:cons(a,B).P(x)) <-> P(a) | (EX x:B. P(x))",
paulson@2482
    39
     "(EX x:RepFun(A,f). P(x)) <-> (EX y:A. P(f(y)))",
paulson@2482
    40
     "(EX x:Union(A).P(x)) <-> (EX y:A. EX x:y.  P(x))",
nipkow@3859
    41
     "(EX x:Collect(A,Q).P(x)) <-> (EX x:A. Q(x) & P(x))",
nipkow@3859
    42
     "(~(EX x:A. P(x))) <-> (ALL x:A. ~P(x))"];
paulson@2482
    43
paulson@3425
    44
val bex_disj_distrib = 
paulson@3425
    45
    prover "(EX x:A. P(x) | Q(x)) <-> ((EX x:A. P(x)) | (EX x:A. Q(x)))";
paulson@3425
    46
paulson@3425
    47
val Rep_simps = map prover
paulson@5202
    48
    ["{x. y:0, R(x,y)} = 0",	(*Replace*)
paulson@5202
    49
     "{x:0. P(x)} = 0",		(*Collect*)
paulson@3425
    50
     "{x:A. False} = 0",
paulson@3425
    51
     "{x:A. True} = A",
paulson@5202
    52
     "RepFun(0,f) = 0",		(*RepFun*)
paulson@3425
    53
     "RepFun(succ(i),f) = cons(f(i), RepFun(i,f))",
paulson@3425
    54
     "RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))"]
clasohm@0
    55
paulson@3425
    56
val misc_simps = map prover
paulson@3425
    57
    ["0 Un A = A",  "A Un 0 = A",
paulson@3425
    58
     "0 Int A = 0", "A Int 0 = 0",
paulson@3425
    59
     "0-A = 0",     "A-0 = A",
paulson@3425
    60
     "Union(0) = 0",
paulson@3425
    61
     "Union(cons(b,A)) = b Un Union(A)",
paulson@3425
    62
     "Inter({b}) = b"]
clasohm@0
    63
paulson@3425
    64
end;
paulson@3425
    65
paulson@3425
    66
Addsimps (ball_simps @ bex_simps @ Rep_simps @ misc_simps);
paulson@3425
    67
clasohm@0
    68
clasohm@0
    69
(** New version of mk_rew_rules **)
clasohm@0
    70
clasohm@0
    71
(*Should False yield False<->True, or should it solve goals some other way?*)
clasohm@0
    72
lcp@1036
    73
(*Analyse a theorem to atomic rewrite rules*)
lcp@1036
    74
fun atomize (conn_pairs, mem_pairs) th = 
lcp@1036
    75
  let fun tryrules pairs t =
clasohm@1461
    76
          case head_of t of
clasohm@1461
    77
              Const(a,_) => 
clasohm@1461
    78
                (case assoc(pairs,a) of
clasohm@1461
    79
                     Some rls => flat (map (atomize (conn_pairs, mem_pairs))
clasohm@1461
    80
                                       ([th] RL rls))
clasohm@1461
    81
                   | None     => [th])
clasohm@1461
    82
            | _ => [th]
lcp@1036
    83
  in case concl_of th of 
clasohm@1461
    84
         Const("Trueprop",_) $ P => 
clasohm@1461
    85
            (case P of
clasohm@1461
    86
                 Const("op :",_) $ a $ b => tryrules mem_pairs b
clasohm@1461
    87
               | Const("True",_)         => []
clasohm@1461
    88
               | Const("False",_)        => []
clasohm@1461
    89
               | A => tryrules conn_pairs A)
lcp@1036
    90
       | _                       => [th]
lcp@1036
    91
  end;
lcp@1036
    92
clasohm@0
    93
(*Analyse a rigid formula*)
lcp@1036
    94
val ZF_conn_pairs =
clasohm@1461
    95
  [("Ball",     [bspec]), 
clasohm@1461
    96
   ("All",      [spec]),
clasohm@1461
    97
   ("op -->",   [mp]),
clasohm@1461
    98
   ("op &",     [conjunct1,conjunct2])];
clasohm@0
    99
clasohm@0
   100
(*Analyse a:b, where b is rigid*)
lcp@1036
   101
val ZF_mem_pairs = 
clasohm@1461
   102
  [("Collect",  [CollectD1,CollectD2]),
clasohm@1461
   103
   ("op -",     [DiffD1,DiffD2]),
clasohm@1461
   104
   ("op Int",   [IntD1,IntD2])];
clasohm@0
   105
lcp@1036
   106
val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
lcp@1036
   107
oheimb@5553
   108
simpset_ref() := simpset() setmksimps (map mk_eq o ZF_atomize o gen_all)
paulson@6153
   109
                           addsplits [split_if]
nipkow@7570
   110
                           setSolver (mk_solver "types" Type_solver_tac);
paulson@2469
   111
wenzelm@4091
   112
val ZF_ss = simpset();