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.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