src/ZF/simpdata.ML
author paulson
Mon Jan 21 14:47:55 2002 +0100 (2002-01-21)
changeset 12825 f1f7964ed05c
parent 12725 7ede865e1fe5
child 13462 56610e2ba220
permissions -rw-r--r--
new simprules and classical rules
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@12199
     9
(*** New version of mk_rew_rules ***)
clasohm@0
    10
clasohm@0
    11
(*Should False yield False<->True, or should it solve goals some other way?*)
clasohm@0
    12
lcp@1036
    13
(*Analyse a theorem to atomic rewrite rules*)
lcp@1036
    14
fun atomize (conn_pairs, mem_pairs) th = 
lcp@1036
    15
  let fun tryrules pairs t =
clasohm@1461
    16
          case head_of t of
clasohm@1461
    17
              Const(a,_) => 
clasohm@1461
    18
                (case assoc(pairs,a) of
clasohm@1461
    19
                     Some rls => flat (map (atomize (conn_pairs, mem_pairs))
clasohm@1461
    20
                                       ([th] RL rls))
clasohm@1461
    21
                   | None     => [th])
clasohm@1461
    22
            | _ => [th]
lcp@1036
    23
  in case concl_of th of 
clasohm@1461
    24
         Const("Trueprop",_) $ P => 
clasohm@1461
    25
            (case P of
clasohm@1461
    26
                 Const("op :",_) $ a $ b => tryrules mem_pairs b
clasohm@1461
    27
               | Const("True",_)         => []
clasohm@1461
    28
               | Const("False",_)        => []
clasohm@1461
    29
               | A => tryrules conn_pairs A)
lcp@1036
    30
       | _                       => [th]
lcp@1036
    31
  end;
lcp@1036
    32
clasohm@0
    33
(*Analyse a rigid formula*)
lcp@1036
    34
val ZF_conn_pairs =
clasohm@1461
    35
  [("Ball",     [bspec]), 
clasohm@1461
    36
   ("All",      [spec]),
clasohm@1461
    37
   ("op -->",   [mp]),
clasohm@1461
    38
   ("op &",     [conjunct1,conjunct2])];
clasohm@0
    39
clasohm@0
    40
(*Analyse a:b, where b is rigid*)
lcp@1036
    41
val ZF_mem_pairs = 
clasohm@1461
    42
  [("Collect",  [CollectD1,CollectD2]),
clasohm@1461
    43
   ("op -",     [DiffD1,DiffD2]),
clasohm@1461
    44
   ("op Int",   [IntD1,IntD2])];
clasohm@0
    45
lcp@1036
    46
val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
lcp@1036
    47
wenzelm@12209
    48
simpset_ref() :=
wenzelm@12725
    49
  simpset() setmksimps (map mk_eq o ZF_atomize o gen_all)
wenzelm@12209
    50
  addcongs [if_weak_cong]
wenzelm@12209
    51
  addsplits [split_if]
wenzelm@12209
    52
  setSolver (mk_solver "types" (fn prems => TCSET' (fn tcset => type_solver_tac tcset prems)));
wenzelm@12209
    53
paulson@2469
    54
paulson@11323
    55
(** Splitting IFs in the assumptions **)
paulson@11323
    56
paulson@11323
    57
Goal "P(if Q then x else y) <-> (~((Q & ~P(x)) | (~Q & ~P(y))))";
paulson@11323
    58
by (Simp_tac 1); 
paulson@11323
    59
qed "split_if_asm";   
paulson@11323
    60
paulson@11323
    61
bind_thms ("if_splits", [split_if, split_if_asm]);
paulson@11323
    62
paulson@12199
    63
paulson@12199
    64
(*** Miniscoping: pushing in big Unions, Intersections, quantifiers, etc. ***)
paulson@12199
    65
paulson@12199
    66
local
paulson@12199
    67
  (*For proving rewrite rules*)
paulson@12199
    68
  fun prover s = (print s;prove_goalw (the_context ()) [Inter_def] s 
paulson@12199
    69
                  (fn _ => [Simp_tac 1, 
paulson@12199
    70
                            ALLGOALS (blast_tac (claset() addSIs[equalityI]))]));
paulson@12199
    71
paulson@12199
    72
in
paulson@12199
    73
paulson@12199
    74
val ball_simps = map prover
paulson@12825
    75
    ["(ALL x:A. P(x) & Q)   <-> (ALL x:A. P(x)) & (A=0 | Q)",
paulson@12825
    76
     "(ALL x:A. P & Q(x))   <-> (A=0 | P) & (ALL x:A. Q(x))",
paulson@12825
    77
     "(ALL x:A. P(x) | Q)   <-> ((ALL x:A. P(x)) | Q)",
paulson@12199
    78
     "(ALL x:A. P | Q(x))   <-> (P | (ALL x:A. Q(x)))",
paulson@12199
    79
     "(ALL x:A. P --> Q(x)) <-> (P --> (ALL x:A. Q(x)))",
paulson@12199
    80
     "(ALL x:A. P(x) --> Q) <-> ((EX x:A. P(x)) --> Q)",
paulson@12199
    81
     "(ALL x:0.P(x)) <-> True",
paulson@12199
    82
     "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i. P(x))",
paulson@12199
    83
     "(ALL x:cons(a,B).P(x)) <-> P(a) & (ALL x:B. P(x))",
paulson@12199
    84
     "(ALL x:RepFun(A,f). P(x)) <-> (ALL y:A. P(f(y)))",
paulson@12199
    85
     "(ALL x:Union(A).P(x)) <-> (ALL y:A. ALL x:y. P(x))",
paulson@12199
    86
     "(ALL x:Collect(A,Q).P(x)) <-> (ALL x:A. Q(x) --> P(x))",
paulson@12199
    87
     "(~(ALL x:A. P(x))) <-> (EX x:A. ~P(x))"];
paulson@12199
    88
paulson@12199
    89
val ball_conj_distrib = 
paulson@12199
    90
    prover "(ALL x:A. P(x) & Q(x)) <-> ((ALL x:A. P(x)) & (ALL x:A. Q(x)))";
paulson@12199
    91
paulson@12199
    92
val bex_simps = map prover
paulson@12199
    93
    ["(EX x:A. P(x) & Q) <-> ((EX x:A. P(x)) & Q)",
paulson@12199
    94
     "(EX x:A. P & Q(x)) <-> (P & (EX x:A. Q(x)))",
paulson@12825
    95
     "(EX x:A. P(x) | Q) <-> (EX x:A. P(x)) | (A~=0 & Q)",
paulson@12825
    96
     "(EX x:A. P | Q(x)) <-> (A~=0 & P) | (EX x:A. Q(x))",
paulson@12825
    97
     "(EX x:A. P --> Q(x)) <-> ((A=0 | P) --> (EX x:A. Q(x)))",
paulson@12825
    98
     "(EX x:A. P(x) --> Q) <-> ((ALL x:A. P(x)) --> (A~=0 & Q))",
paulson@12199
    99
     "(EX x:0.P(x)) <-> False",
paulson@12199
   100
     "(EX x:succ(i).P(x)) <-> P(i) | (EX x:i. P(x))",
paulson@12199
   101
     "(EX x:cons(a,B).P(x)) <-> P(a) | (EX x:B. P(x))",
paulson@12199
   102
     "(EX x:RepFun(A,f). P(x)) <-> (EX y:A. P(f(y)))",
paulson@12199
   103
     "(EX x:Union(A).P(x)) <-> (EX y:A. EX x:y.  P(x))",
paulson@12199
   104
     "(EX x:Collect(A,Q).P(x)) <-> (EX x:A. Q(x) & P(x))",
paulson@12199
   105
     "(~(EX x:A. P(x))) <-> (ALL x:A. ~P(x))"];
paulson@12199
   106
paulson@12199
   107
val bex_disj_distrib = 
paulson@12199
   108
    prover "(EX x:A. P(x) | Q(x)) <-> ((EX x:A. P(x)) | (EX x:A. Q(x)))";
paulson@12199
   109
paulson@12199
   110
val Rep_simps = map prover
paulson@12199
   111
    ["{x. y:0, R(x,y)} = 0",	(*Replace*)
paulson@12199
   112
     "{x:0. P(x)} = 0",		(*Collect*)
paulson@12552
   113
     "{x:A. P} = (if P then A else 0)",
paulson@12199
   114
     "RepFun(0,f) = 0",		(*RepFun*)
paulson@12199
   115
     "RepFun(succ(i),f) = cons(f(i), RepFun(i,f))",
paulson@12199
   116
     "RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))"]
paulson@12199
   117
paulson@12199
   118
val misc_simps = map prover
paulson@12199
   119
    ["0 Un A = A", "A Un 0 = A",
paulson@12199
   120
     "0 Int A = 0", "A Int 0 = 0",
paulson@12199
   121
     "0 - A = 0", "A - 0 = A",
paulson@12199
   122
     "Union(0) = 0",
paulson@12199
   123
     "Union(cons(b,A)) = b Un Union(A)",
paulson@12199
   124
     "Inter({b}) = b"]
paulson@12199
   125
paulson@12199
   126
paulson@12199
   127
val UN_simps = map prover 
paulson@12199
   128
    ["(UN x:C. cons(a, B(x))) = (if C=0 then 0 else cons(a, UN x:C. B(x)))",
paulson@12199
   129
     "(UN x:C. A(x) Un B)   = (if C=0 then 0 else (UN x:C. A(x)) Un B)",
paulson@12199
   130
     "(UN x:C. A Un B(x))   = (if C=0 then 0 else A Un (UN x:C. B(x)))",
paulson@12199
   131
     "(UN x:C. A(x) Int B)  = ((UN x:C. A(x)) Int B)",
paulson@12199
   132
     "(UN x:C. A Int B(x))  = (A Int (UN x:C. B(x)))",
paulson@12199
   133
     "(UN x:C. A(x) - B)    = ((UN x:C. A(x)) - B)",
paulson@12199
   134
     "(UN x:C. A - B(x))    = (if C=0 then 0 else A - (INT x:C. B(x)))",
paulson@12199
   135
     "(UN x: Union(A). B(x)) = (UN y:A. UN x:y. B(x))",
paulson@12199
   136
     "(UN z: (UN x:A. B(x)). C(z)) = (UN  x:A. UN z: B(x). C(z))",
paulson@12199
   137
     "(UN x: RepFun(A,f). B(x))     = (UN a:A. B(f(a)))"];
paulson@12199
   138
paulson@12199
   139
val INT_simps = map prover
paulson@12199
   140
    ["(INT x:C. A(x) Int B) = (INT x:C. A(x)) Int B",
paulson@12199
   141
     "(INT x:C. A Int B(x)) = A Int (INT x:C. B(x))",
paulson@12199
   142
     "(INT x:C. A(x) - B)   = (INT x:C. A(x)) - B",
paulson@12199
   143
     "(INT x:C. A - B(x))   = (if C=0 then 0 else A - (UN x:C. B(x)))",
paulson@12199
   144
     "(INT x:C. cons(a, B(x))) = (if C=0 then 0 else cons(a, INT x:C. B(x)))",
paulson@12199
   145
     "(INT x:C. A(x) Un B)  = (if C=0 then 0 else (INT x:C. A(x)) Un B)",
paulson@12199
   146
     "(INT x:C. A Un B(x))  = (if C=0 then 0 else A Un (INT x:C. B(x)))"];
paulson@12199
   147
paulson@12199
   148
(** The _extend_simps rules are oriented in the opposite direction, to 
paulson@12199
   149
    pull UN and INT outwards. **)
paulson@12199
   150
paulson@12199
   151
val UN_extend_simps = map prover 
paulson@12199
   152
    ["cons(a, UN x:C. B(x)) = (if C=0 then {a} else (UN x:C. cons(a, B(x))))",
paulson@12199
   153
     "(UN x:C. A(x)) Un B   = (if C=0 then B else (UN x:C. A(x) Un B))",
paulson@12199
   154
     "A Un (UN x:C. B(x))   = (if C=0 then A else (UN x:C. A Un B(x)))",
paulson@12199
   155
     "((UN x:C. A(x)) Int B) = (UN x:C. A(x) Int B)",
paulson@12199
   156
     "(A Int (UN x:C. B(x))) = (UN x:C. A Int B(x))",
paulson@12199
   157
     "((UN x:C. A(x)) - B) = (UN x:C. A(x) - B)",
paulson@12199
   158
     "A - (INT x:C. B(x))    = (if C=0 then A else (UN x:C. A - B(x)))",
paulson@12199
   159
     "(UN y:A. UN x:y. B(x)) = (UN x: Union(A). B(x))",
paulson@12199
   160
     "(UN  x:A. UN z: B(x). C(z)) = (UN z: (UN x:A. B(x)). C(z))",
paulson@12199
   161
     "(UN a:A. B(f(a))) = (UN x: RepFun(A,f). B(x))"];
paulson@12199
   162
paulson@12199
   163
val INT_extend_simps = map prover
paulson@12199
   164
    ["(INT x:C. A(x)) Int B = (INT x:C. A(x) Int B)",
paulson@12199
   165
     "A Int (INT x:C. B(x)) = (INT x:C. A Int B(x))",
paulson@12199
   166
     "(INT x:C. A(x)) - B = (INT x:C. A(x) - B)",
paulson@12199
   167
     "A - (UN x:C. B(x))   = (if C=0 then A else (INT x:C. A - B(x)))",
paulson@12199
   168
     "cons(a, INT x:C. B(x)) = (if C=0 then {a} else (INT x:C. cons(a, B(x))))",
paulson@12199
   169
     "(INT x:C. A(x)) Un B  = (if C=0 then B else (INT x:C. A(x) Un B))",
paulson@12199
   170
     "A Un (INT x:C. B(x))  = (if C=0 then A else (INT x:C. A Un B(x)))"];
paulson@12199
   171
paulson@12199
   172
end;
paulson@12199
   173
paulson@12199
   174
bind_thms ("ball_simps", ball_simps);
paulson@12199
   175
bind_thm ("ball_conj_distrib", ball_conj_distrib);
paulson@12199
   176
bind_thms ("bex_simps", bex_simps);
paulson@12199
   177
bind_thm ("bex_disj_distrib", bex_disj_distrib);
paulson@12199
   178
bind_thms ("Rep_simps", Rep_simps);
paulson@12199
   179
bind_thms ("misc_simps", misc_simps);
paulson@12199
   180
paulson@12199
   181
Addsimps (ball_simps @ bex_simps @ Rep_simps @ misc_simps);
paulson@12199
   182
paulson@12199
   183
bind_thms ("UN_simps", UN_simps);
paulson@12199
   184
bind_thms ("INT_simps", INT_simps);
paulson@12199
   185
paulson@12199
   186
Addsimps (UN_simps @ INT_simps);
paulson@12199
   187
paulson@12199
   188
bind_thms ("UN_extend_simps", UN_extend_simps);
paulson@12199
   189
bind_thms ("INT_extend_simps", INT_extend_simps);
paulson@12199
   190
paulson@12199
   191
paulson@11233
   192
(** One-point rule for bounded quantifiers: see HOL/Set.ML **)
paulson@11233
   193
paulson@11233
   194
Goal "(EX x:A. x=a) <-> (a:A)";
paulson@11233
   195
by (Blast_tac 1);
paulson@11233
   196
qed "bex_triv_one_point1";
paulson@11233
   197
paulson@11233
   198
Goal "(EX x:A. a=x) <-> (a:A)";
paulson@11233
   199
by (Blast_tac 1);
paulson@11233
   200
qed "bex_triv_one_point2";
paulson@11233
   201
paulson@11233
   202
Goal "(EX x:A. x=a & P(x)) <-> (a:A & P(a))";
paulson@11233
   203
by (Blast_tac 1);
paulson@11233
   204
qed "bex_one_point1";
paulson@11233
   205
paulson@11233
   206
Goal "(EX x:A. a=x & P(x)) <-> (a:A & P(a))";
wenzelm@12484
   207
by (Blast_tac 1);
paulson@11233
   208
qed "bex_one_point2";
paulson@11233
   209
paulson@11233
   210
Goal "(ALL x:A. x=a --> P(x)) <-> (a:A --> P(a))";
paulson@11233
   211
by (Blast_tac 1);
paulson@11233
   212
qed "ball_one_point1";
paulson@11233
   213
paulson@11233
   214
Goal "(ALL x:A. a=x --> P(x)) <-> (a:A --> P(a))";
paulson@11233
   215
by (Blast_tac 1);
paulson@11233
   216
qed "ball_one_point2";
paulson@11233
   217
paulson@11233
   218
Addsimps [bex_triv_one_point1,bex_triv_one_point2,
paulson@11233
   219
          bex_one_point1,bex_one_point2,
paulson@11233
   220
          ball_one_point1,ball_one_point2];
paulson@11233
   221
paulson@12199
   222
paulson@11233
   223
let
paulson@11233
   224
val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
paulson@11233
   225
    ("EX x:A. P(x) & Q(x)",FOLogic.oT)
paulson@11233
   226
wenzelm@12484
   227
val prove_bex_tac = rewtac Bex_def THEN
paulson@11233
   228
                    Quantifier1.prove_one_point_ex_tac;
paulson@11233
   229
paulson@11233
   230
val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
paulson@11233
   231
paulson@11233
   232
val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
paulson@11233
   233
    ("ALL x:A. P(x) --> Q(x)",FOLogic.oT)
paulson@11233
   234
wenzelm@12484
   235
val prove_ball_tac = rewtac Ball_def THEN 
paulson@11233
   236
                     Quantifier1.prove_one_point_all_tac;
paulson@11233
   237
paulson@11233
   238
val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
paulson@11233
   239
paulson@11233
   240
val defBEX_regroup = mk_simproc "defined BEX" [ex_pattern] rearrange_bex;
paulson@11233
   241
val defBALL_regroup = mk_simproc "defined BALL" [all_pattern] rearrange_ball;
paulson@11233
   242
in
paulson@11233
   243
paulson@11233
   244
Addsimprocs [defBALL_regroup,defBEX_regroup]
paulson@11233
   245
paulson@11233
   246
end;
paulson@11233
   247
paulson@12199
   248
wenzelm@4091
   249
val ZF_ss = simpset();