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