src/ZF/simpdata.ML
author wenzelm
Sat Jan 12 16:37:58 2002 +0100 (2002-01-12 ago)
changeset 12725 7ede865e1fe5
parent 12720 f8a134b9a57f
child 12825 f1f7964ed05c
permissions -rw-r--r--
renamed forall_elim_vars_safe to gen_all;
     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)) | Q)",
    76      "(ALL x:A. P | Q(x))   <-> (P | (ALL x:A. Q(x)))",
    77      "(ALL x:A. P --> Q(x)) <-> (P --> (ALL x:A. Q(x)))",
    78      "(ALL x:A. P(x) --> Q) <-> ((EX x:A. P(x)) --> Q)",
    79      "(ALL x:0.P(x)) <-> True",
    80      "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i. P(x))",
    81      "(ALL x:cons(a,B).P(x)) <-> P(a) & (ALL x:B. P(x))",
    82      "(ALL x:RepFun(A,f). P(x)) <-> (ALL y:A. P(f(y)))",
    83      "(ALL x:Union(A).P(x)) <-> (ALL y:A. ALL x:y. P(x))",
    84      "(ALL x:Collect(A,Q).P(x)) <-> (ALL x:A. Q(x) --> P(x))",
    85      "(~(ALL x:A. P(x))) <-> (EX x:A. ~P(x))"];
    86 
    87 val ball_conj_distrib = 
    88     prover "(ALL x:A. P(x) & Q(x)) <-> ((ALL x:A. P(x)) & (ALL x:A. Q(x)))";
    89 
    90 val bex_simps = map prover
    91     ["(EX x:A. P(x) & Q) <-> ((EX x:A. P(x)) & Q)",
    92      "(EX x:A. P & Q(x)) <-> (P & (EX x:A. Q(x)))",
    93      "(EX x:0.P(x)) <-> False",
    94      "(EX x:succ(i).P(x)) <-> P(i) | (EX x:i. P(x))",
    95      "(EX x:cons(a,B).P(x)) <-> P(a) | (EX x:B. P(x))",
    96      "(EX x:RepFun(A,f). P(x)) <-> (EX y:A. P(f(y)))",
    97      "(EX x:Union(A).P(x)) <-> (EX y:A. EX x:y.  P(x))",
    98      "(EX x:Collect(A,Q).P(x)) <-> (EX x:A. Q(x) & P(x))",
    99      "(~(EX x:A. P(x))) <-> (ALL x:A. ~P(x))"];
   100 
   101 val bex_disj_distrib = 
   102     prover "(EX x:A. P(x) | Q(x)) <-> ((EX x:A. P(x)) | (EX x:A. Q(x)))";
   103 
   104 val Rep_simps = map prover
   105     ["{x. y:0, R(x,y)} = 0",	(*Replace*)
   106      "{x:0. P(x)} = 0",		(*Collect*)
   107      "{x:A. P} = (if P then A else 0)",
   108      "RepFun(0,f) = 0",		(*RepFun*)
   109      "RepFun(succ(i),f) = cons(f(i), RepFun(i,f))",
   110      "RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))"]
   111 
   112 val misc_simps = map prover
   113     ["0 Un A = A", "A Un 0 = A",
   114      "0 Int A = 0", "A Int 0 = 0",
   115      "0 - A = 0", "A - 0 = A",
   116      "Union(0) = 0",
   117      "Union(cons(b,A)) = b Un Union(A)",
   118      "Inter({b}) = b"]
   119 
   120 
   121 val UN_simps = map prover 
   122     ["(UN x:C. cons(a, B(x))) = (if C=0 then 0 else cons(a, UN x:C. B(x)))",
   123      "(UN x:C. A(x) Un B)   = (if C=0 then 0 else (UN x:C. A(x)) Un B)",
   124      "(UN x:C. A Un B(x))   = (if C=0 then 0 else A Un (UN x:C. B(x)))",
   125      "(UN x:C. A(x) Int B)  = ((UN x:C. A(x)) Int B)",
   126      "(UN x:C. A Int B(x))  = (A Int (UN x:C. B(x)))",
   127      "(UN x:C. A(x) - B)    = ((UN x:C. A(x)) - B)",
   128      "(UN x:C. A - B(x))    = (if C=0 then 0 else A - (INT x:C. B(x)))",
   129      "(UN x: Union(A). B(x)) = (UN y:A. UN x:y. B(x))",
   130      "(UN z: (UN x:A. B(x)). C(z)) = (UN  x:A. UN z: B(x). C(z))",
   131      "(UN x: RepFun(A,f). B(x))     = (UN a:A. B(f(a)))"];
   132 
   133 val INT_simps = map prover
   134     ["(INT x:C. A(x) Int B) = (INT x:C. A(x)) Int B",
   135      "(INT x:C. A Int B(x)) = A Int (INT x:C. B(x))",
   136      "(INT x:C. A(x) - B)   = (INT x:C. A(x)) - B",
   137      "(INT x:C. A - B(x))   = (if C=0 then 0 else A - (UN x:C. B(x)))",
   138      "(INT x:C. cons(a, B(x))) = (if C=0 then 0 else cons(a, INT x:C. B(x)))",
   139      "(INT x:C. A(x) Un B)  = (if C=0 then 0 else (INT x:C. A(x)) Un B)",
   140      "(INT x:C. A Un B(x))  = (if C=0 then 0 else A Un (INT x:C. B(x)))"];
   141 
   142 (** The _extend_simps rules are oriented in the opposite direction, to 
   143     pull UN and INT outwards. **)
   144 
   145 val UN_extend_simps = map prover 
   146     ["cons(a, UN x:C. B(x)) = (if C=0 then {a} else (UN x:C. cons(a, B(x))))",
   147      "(UN x:C. A(x)) Un B   = (if C=0 then B else (UN x:C. A(x) Un B))",
   148      "A Un (UN x:C. B(x))   = (if C=0 then A else (UN x:C. A Un B(x)))",
   149      "((UN x:C. A(x)) Int B) = (UN x:C. A(x) Int B)",
   150      "(A Int (UN x:C. B(x))) = (UN x:C. A Int B(x))",
   151      "((UN x:C. A(x)) - B) = (UN x:C. A(x) - B)",
   152      "A - (INT x:C. B(x))    = (if C=0 then A else (UN x:C. A - B(x)))",
   153      "(UN y:A. UN x:y. B(x)) = (UN x: Union(A). B(x))",
   154      "(UN  x:A. UN z: B(x). C(z)) = (UN z: (UN x:A. B(x)). C(z))",
   155      "(UN a:A. B(f(a))) = (UN x: RepFun(A,f). B(x))"];
   156 
   157 val INT_extend_simps = map prover
   158     ["(INT x:C. A(x)) Int B = (INT x:C. A(x) Int B)",
   159      "A Int (INT x:C. B(x)) = (INT x:C. A Int B(x))",
   160      "(INT x:C. A(x)) - B = (INT x:C. A(x) - B)",
   161      "A - (UN x:C. B(x))   = (if C=0 then A else (INT x:C. A - B(x)))",
   162      "cons(a, INT x:C. B(x)) = (if C=0 then {a} else (INT x:C. cons(a, B(x))))",
   163      "(INT x:C. A(x)) Un B  = (if C=0 then B else (INT x:C. A(x) Un B))",
   164      "A Un (INT x:C. B(x))  = (if C=0 then A else (INT x:C. A Un B(x)))"];
   165 
   166 end;
   167 
   168 bind_thms ("ball_simps", ball_simps);
   169 bind_thm ("ball_conj_distrib", ball_conj_distrib);
   170 bind_thms ("bex_simps", bex_simps);
   171 bind_thm ("bex_disj_distrib", bex_disj_distrib);
   172 bind_thms ("Rep_simps", Rep_simps);
   173 bind_thms ("misc_simps", misc_simps);
   174 
   175 Addsimps (ball_simps @ bex_simps @ Rep_simps @ misc_simps);
   176 
   177 bind_thms ("UN_simps", UN_simps);
   178 bind_thms ("INT_simps", INT_simps);
   179 
   180 Addsimps (UN_simps @ INT_simps);
   181 
   182 bind_thms ("UN_extend_simps", UN_extend_simps);
   183 bind_thms ("INT_extend_simps", INT_extend_simps);
   184 
   185 
   186 (** One-point rule for bounded quantifiers: see HOL/Set.ML **)
   187 
   188 Goal "(EX x:A. x=a) <-> (a:A)";
   189 by (Blast_tac 1);
   190 qed "bex_triv_one_point1";
   191 
   192 Goal "(EX x:A. a=x) <-> (a:A)";
   193 by (Blast_tac 1);
   194 qed "bex_triv_one_point2";
   195 
   196 Goal "(EX x:A. x=a & P(x)) <-> (a:A & P(a))";
   197 by (Blast_tac 1);
   198 qed "bex_one_point1";
   199 
   200 Goal "(EX x:A. a=x & P(x)) <-> (a:A & P(a))";
   201 by (Blast_tac 1);
   202 qed "bex_one_point2";
   203 
   204 Goal "(ALL x:A. x=a --> P(x)) <-> (a:A --> P(a))";
   205 by (Blast_tac 1);
   206 qed "ball_one_point1";
   207 
   208 Goal "(ALL x:A. a=x --> P(x)) <-> (a:A --> P(a))";
   209 by (Blast_tac 1);
   210 qed "ball_one_point2";
   211 
   212 Addsimps [bex_triv_one_point1,bex_triv_one_point2,
   213           bex_one_point1,bex_one_point2,
   214           ball_one_point1,ball_one_point2];
   215 
   216 
   217 let
   218 val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
   219     ("EX x:A. P(x) & Q(x)",FOLogic.oT)
   220 
   221 val prove_bex_tac = rewtac Bex_def THEN
   222                     Quantifier1.prove_one_point_ex_tac;
   223 
   224 val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
   225 
   226 val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
   227     ("ALL x:A. P(x) --> Q(x)",FOLogic.oT)
   228 
   229 val prove_ball_tac = rewtac Ball_def THEN 
   230                      Quantifier1.prove_one_point_all_tac;
   231 
   232 val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
   233 
   234 val defBEX_regroup = mk_simproc "defined BEX" [ex_pattern] rearrange_bex;
   235 val defBALL_regroup = mk_simproc "defined BALL" [all_pattern] rearrange_ball;
   236 in
   237 
   238 Addsimprocs [defBALL_regroup,defBEX_regroup]
   239 
   240 end;
   241 
   242 
   243 val ZF_ss = simpset();