author paulson Fri Mar 14 10:30:15 2003 +0100 (2003-03-14) changeset 13860 b681a3cb0beb parent 13859 adf68d9e5dec child 13861 0c18f31d901a
new UN/INT simprules
 src/HOL/Set.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Set.thy	Thu Mar 13 18:54:38 2003 +0100
1.2 +++ b/src/HOL/Set.thy	Fri Mar 14 10:30:15 2003 +0100
1.3 @@ -1657,7 +1657,8 @@
1.4    by rules
1.5
1.6
1.7 -text {* \medskip Miniscoping: pushing in big Unions and Intersections. *}
1.8 +text {* \medskip Miniscoping: pushing in quantifiers and big Unions
1.9 +           and Intersections. *}
1.10
1.11  lemma UN_simps [simp]:
1.12    "!!a B C. (UN x:C. insert a (B x)) = (if C={} then {} else insert a (UN x:C. B x))"
1.13 @@ -1722,6 +1723,35 @@
1.14    by blast
1.15
1.16
1.17 +text {* \medskip Maxiscoping: pulling out big Unions and Intersections. *}
1.18 +
1.19 +lemma UN_extend_simps:
1.20 +  "!!a B C. insert a (UN x:C. B x) = (if C={} then {a} else (UN x:C. insert a (B x)))"
1.21 +  "!!A B C. (UN x:C. A x) Un B    = (if C={} then B else (UN x:C. A x Un B))"
1.22 +  "!!A B C. A Un (UN x:C. B x)   = (if C={} then A else (UN x:C. A Un B x))"
1.23 +  "!!A B C. ((UN x:C. A x) Int B) = (UN x:C. A x Int B)"
1.24 +  "!!A B C. (A Int (UN x:C. B x)) = (UN x:C. A Int B x)"
1.25 +  "!!A B C. ((UN x:C. A x) - B) = (UN x:C. A x - B)"
1.26 +  "!!A B C. (A - (INT x:C. B x)) = (UN x:C. A - B x)"
1.27 +  "!!A B. (UN y:A. UN x:y. B x) = (UN x: Union A. B x)"
1.28 +  "!!A B C. (UN  x:A. UN z: B(x). C z) = (UN z: UNION A B. C z)"
1.29 +  "!!A B f. (UN a:A. B (f a)) = (UN x:f`A. B x)"
1.30 +  by auto
1.31 +
1.32 +lemma INT_extend_simps:
1.33 +  "!!A B C. (INT x:C. A x) Int B = (if C={} then B else (INT x:C. A x Int B))"
1.34 +  "!!A B C. A Int (INT x:C. B x) = (if C={} then A else (INT x:C. A Int B x))"
1.35 +  "!!A B C. (INT x:C. A x) - B   = (if C={} then UNIV-B else (INT x:C. A x - B))"
1.36 +  "!!A B C. A - (UN x:C. B x)   = (if C={} then A else (INT x:C. A - B x))"
1.37 +  "!!a B C. insert a (INT x:C. B x) = (INT x:C. insert a (B x))"
1.38 +  "!!A B C. ((INT x:C. A x) Un B)  = (INT x:C. A x Un B)"
1.39 +  "!!A B C. A Un (INT x:C. B x)  = (INT x:C. A Un B x)"
1.40 +  "!!A B. (INT y:A. INT x:y. B x) = (INT x: Union A. B x)"
1.41 +  "!!A B C. (INT x:A. INT z: B(x). C z) = (INT z: UNION A B. C z)"
1.42 +  "!!A B f. (INT a:A. B (f a))    = (INT x:f`A. B x)"
1.43 +  by auto
1.44 +
1.45 +
1.46  subsubsection {* Monotonicity of various operations *}
1.47
1.48  lemma image_mono: "A \<subseteq> B ==> f`A \<subseteq> f`B"
```