added lemmas
authornipkow
Sat May 08 19:29:12 2010 +0200 (2010-05-08)
changeset 36755d1b498f2f50b
parent 36754 5ce217fc769a
child 36757 21443c2858a7
added lemmas
src/HOL/SetInterval.thy
     1.1 --- a/src/HOL/SetInterval.thy	Sat May 08 17:15:50 2010 +0200
     1.2 +++ b/src/HOL/SetInterval.thy	Sat May 08 19:29:12 2010 +0200
     1.3 @@ -562,6 +562,38 @@
     1.4  
     1.5  subsubsection {* Proving Inclusions and Equalities between Unions *}
     1.6  
     1.7 +lemma UN_le_eq_Un0:
     1.8 +  "(\<Union>i\<le>n::nat. M i) = (\<Union>i\<in>{1..n}. M i) \<union> M 0" (is "?A = ?B")
     1.9 +proof
    1.10 +  show "?A <= ?B"
    1.11 +  proof
    1.12 +    fix x assume "x : ?A"
    1.13 +    then obtain i where i: "i\<le>n" "x : M i" by auto
    1.14 +    show "x : ?B"
    1.15 +    proof(cases i)
    1.16 +      case 0 with i show ?thesis by simp
    1.17 +    next
    1.18 +      case (Suc j) with i show ?thesis by auto
    1.19 +    qed
    1.20 +  qed
    1.21 +next
    1.22 +  show "?B <= ?A" by auto
    1.23 +qed
    1.24 +
    1.25 +lemma UN_le_add_shift:
    1.26 +  "(\<Union>i\<le>n::nat. M(i+k)) = (\<Union>i\<in>{k..n+k}. M i)" (is "?A = ?B")
    1.27 +proof
    1.28 +  show "?A <= ?B" by fastsimp
    1.29 +next
    1.30 +  show "?B <= ?A"
    1.31 +  proof
    1.32 +    fix x assume "x : ?B"
    1.33 +    then obtain i where i: "i : {k..n+k}" "x : M(i)" by auto
    1.34 +    hence "i-k\<le>n & x : M((i-k)+k)" by auto
    1.35 +    thus "x : ?A" by blast
    1.36 +  qed
    1.37 +qed
    1.38 +
    1.39  lemma UN_UN_finite_eq: "(\<Union>n::nat. \<Union>i\<in>{0..<n}. A i) = (\<Union>n. A n)"
    1.40    by (auto simp add: atLeast0LessThan) 
    1.41