src/HOL/Sum_Type.thy
changeset 49948 744934b818c7
parent 49834 b27bbb021df1
child 53010 ec5e6f69bd65
     1.1 --- a/src/HOL/Sum_Type.thy	Sat Oct 20 09:09:37 2012 +0200
     1.2 +++ b/src/HOL/Sum_Type.thy	Sat Oct 20 09:12:16 2012 +0200
     1.3 @@ -209,8 +209,19 @@
     1.4    show "u \<in> UNIV <+> UNIV \<longleftrightarrow> u \<in> UNIV" by (cases u) auto
     1.5  qed
     1.6  
     1.7 +lemma UNIV_sum:
     1.8 +  "UNIV = Inl ` UNIV \<union> Inr ` UNIV"
     1.9 +proof -
    1.10 +  { fix x :: "'a + 'b"
    1.11 +    assume "x \<notin> range Inr"
    1.12 +    then have "x \<in> range Inl"
    1.13 +    by (cases x) simp_all
    1.14 +  } then show ?thesis by auto
    1.15 +qed
    1.16 +
    1.17  hide_const (open) Suml Sumr Projl Projr
    1.18  
    1.19  hide_const (open) sum
    1.20  
    1.21  end
    1.22 +