# HG changeset patch # User paulson # Date 1047634215 -3600 # Node ID b681a3cb0beb08bfdc2a24c6bd4daf55802e4d5b # Parent adf68d9e5dec8ba3b8c46d80182efe38d9b302a0 new UN/INT simprules diff -r adf68d9e5dec -r b681a3cb0beb src/HOL/Set.thy --- a/src/HOL/Set.thy Thu Mar 13 18:54:38 2003 +0100 +++ b/src/HOL/Set.thy Fri Mar 14 10:30:15 2003 +0100 @@ -1657,7 +1657,8 @@ by rules -text {* \medskip Miniscoping: pushing in big Unions and Intersections. *} +text {* \medskip Miniscoping: pushing in quantifiers and big Unions + and Intersections. *} lemma UN_simps [simp]: "!!a B C. (UN x:C. insert a (B x)) = (if C={} then {} else insert a (UN x:C. B x))" @@ -1722,6 +1723,35 @@ by blast +text {* \medskip Maxiscoping: pulling out big Unions and Intersections. *} + +lemma UN_extend_simps: + "!!a B C. insert a (UN x:C. B x) = (if C={} then {a} else (UN x:C. insert a (B x)))" + "!!A B C. (UN x:C. A x) Un B = (if C={} then B else (UN x:C. A x Un B))" + "!!A B C. A Un (UN x:C. B x) = (if C={} then A else (UN x:C. A Un B x))" + "!!A B C. ((UN x:C. A x) Int B) = (UN x:C. A x Int B)" + "!!A B C. (A Int (UN x:C. B x)) = (UN x:C. A Int B x)" + "!!A B C. ((UN x:C. A x) - B) = (UN x:C. A x - B)" + "!!A B C. (A - (INT x:C. B x)) = (UN x:C. A - B x)" + "!!A B. (UN y:A. UN x:y. B x) = (UN x: Union A. B x)" + "!!A B C. (UN x:A. UN z: B(x). C z) = (UN z: UNION A B. C z)" + "!!A B f. (UN a:A. B (f a)) = (UN x:f`A. B x)" + by auto + +lemma INT_extend_simps: + "!!A B C. (INT x:C. A x) Int B = (if C={} then B else (INT x:C. A x Int B))" + "!!A B C. A Int (INT x:C. B x) = (if C={} then A else (INT x:C. A Int B x))" + "!!A B C. (INT x:C. A x) - B = (if C={} then UNIV-B else (INT x:C. A x - B))" + "!!A B C. A - (UN x:C. B x) = (if C={} then A else (INT x:C. A - B x))" + "!!a B C. insert a (INT x:C. B x) = (INT x:C. insert a (B x))" + "!!A B C. ((INT x:C. A x) Un B) = (INT x:C. A x Un B)" + "!!A B C. A Un (INT x:C. B x) = (INT x:C. A Un B x)" + "!!A B. (INT y:A. INT x:y. B x) = (INT x: Union A. B x)" + "!!A B C. (INT x:A. INT z: B(x). C z) = (INT z: UNION A B. C z)" + "!!A B f. (INT a:A. B (f a)) = (INT x:f`A. B x)" + by auto + + subsubsection {* Monotonicity of various operations *} lemma image_mono: "A \ B ==> f`A \ f`B"