src/HOL/equalities.ML
changeset 2513 d708d8cdc8e8
parent 2512 0231e4f467f2
child 2519 761e3094e32f
     1.1 --- a/src/HOL/equalities.ML	Fri Jan 17 10:09:46 1997 +0100
     1.2 +++ b/src/HOL/equalities.ML	Fri Jan 17 11:09:19 1997 +0100
     1.3 @@ -564,9 +564,44 @@
     1.4                   "(INT x. A x - B)   = ((INT x.A x) - B)",
     1.5                   "(INT x. A - B x)   = (A - (UN x.B x))"];
     1.6  
     1.7 -(*Analogous laws for bounded Unions and Intersections are conditional
     1.8 +val UN_simps = map prover 
     1.9 +                ["(UN x:C. A x Int B)  = ((UN x:C.A x) Int B)",
    1.10 +                 "(UN x:C. A Int B x)  = (A Int (UN x:C.B x))",
    1.11 +                 "(UN x:C. A x - B)    = ((UN x:C.A x) - B)",
    1.12 +                 "(UN x:C. A - B x)    = (A - (INT x:C.B x))"];
    1.13 +
    1.14 +val INT_simps = map prover
    1.15 +                ["(INT x:C. insert a (B x)) = insert a (INT x:C. B x)",
    1.16 +                 "(INT x:C. A x Un B)  = ((INT x:C.A x) Un B)",
    1.17 +                 "(INT x:C. A Un B x)  = (A Un (INT x:C.B x))"];
    1.18 +
    1.19 +(*The missing laws for bounded Unions and Intersections are conditional
    1.20    on the index set's being non-empty.  Thus they are probably NOT worth 
    1.21    adding as default rewrites.*)
    1.22 +
    1.23 +val ball_simps = map prover
    1.24 +    ["(ALL x:A. P x | Q) = ((ALL x:A. P x) | Q)",
    1.25 +     "(ALL x:A. P | Q x) = (P | (ALL x:A. Q x))",
    1.26 +     "(ALL x:{}. P x) = True",
    1.27 +     "(ALL x:insert a B. P x) = (P(a) & (ALL x:B. P x))",
    1.28 +     "(ALL x:Union(A). P x) = (ALL y:A. ALL x:y. P x)",
    1.29 +     "(ALL x:Collect Q. P x) = (ALL x. Q x --> P x)"];
    1.30 +
    1.31 +val ball_conj_distrib = 
    1.32 +    prover "(ALL x:A. P x & Q x) = ((ALL x:A. P x) & (ALL x:A. Q x))";
    1.33 +
    1.34 +val bex_simps = map prover
    1.35 +    ["(EX x:A. P x & Q) = ((EX x:A. P x) & Q)",
    1.36 +     "(EX x:A. P & Q x) = (P & (EX x:A. Q x))",
    1.37 +     "(EX x:{}. P x) = False",
    1.38 +     "(EX x:insert a B. P x) = (P(a) | (EX x:B. P x))",
    1.39 +     "(EX x:Union(A). P x) = (EX y:A. EX x:y.  P x)",
    1.40 +     "(EX x:Collect Q. P x) = (EX x. Q x & P x)"];
    1.41 +
    1.42 +val bex_conj_distrib = 
    1.43 +    prover "(EX x:A. P x | Q x) = ((EX x:A. P x) | (EX x:A. Q x))";
    1.44 +
    1.45  end;
    1.46  
    1.47 -Addsimps (UN1_simps @ INT1_simps);
    1.48 +Addsimps (UN1_simps @ INT1_simps @ UN_simps @ INT_simps @ 
    1.49 +	  ball_simps @ bex_simps);