new UN/INT simprules
authorpaulson
Fri Mar 14 10:30:15 2003 +0100 (2003-03-14)
changeset 13860b681a3cb0beb
parent 13859 adf68d9e5dec
child 13861 0c18f31d901a
new UN/INT simprules
src/HOL/Set.thy
     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"