src/HOL/Sum_Type.thy
changeset 29183 f1648e009dc1
parent 29025 8c8859c0d734
child 31080 21ffc770ebc0
     1.1 --- a/src/HOL/Sum_Type.thy	Sat Dec 27 17:35:01 2008 +0100
     1.2 +++ b/src/HOL/Sum_Type.thy	Sat Dec 27 17:49:15 2008 +0100
     1.3 @@ -120,29 +120,6 @@
     1.4  by (blast dest!: Inr_inject)
     1.5  
     1.6  
     1.7 -subsection {* Projections *}
     1.8 -
     1.9 -definition 
    1.10 -  "sum_case f g x =
    1.11 -  (if (\<exists>!y. x = Inl y) 
    1.12 -  then f (THE y. x = Inl y) 
    1.13 -  else g (THE y. x = Inr y))"
    1.14 -definition "Projl x = sum_case id undefined x"
    1.15 -definition "Projr x = sum_case undefined id x"
    1.16 -
    1.17 -lemma sum_cases[simp]: 
    1.18 -  "sum_case f g (Inl x) = f x"
    1.19 -  "sum_case f g (Inr y) = g y"
    1.20 -  unfolding sum_case_def
    1.21 -  by auto
    1.22 -
    1.23 -lemma Projl_Inl[simp]: "Projl (Inl x) = x"
    1.24 -  unfolding Projl_def by simp
    1.25 -
    1.26 -lemma Projr_Inr[simp]: "Projr (Inr x) = x"
    1.27 -  unfolding Projr_def by simp
    1.28 -
    1.29 -
    1.30  subsection{*The Disjoint Sum of Sets*}
    1.31  
    1.32  (** Introduction rules for the injections **)