src/HOL/Datatype.thy
changeset 27104 791607529f6d
parent 26748 4d51ddd6aa5c
child 27823 52971512d1a2
     1.1 --- a/src/HOL/Datatype.thy	Tue Jun 10 15:30:06 2008 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Tue Jun 10 15:30:33 2008 +0200
     1.3 @@ -533,10 +533,13 @@
     1.4  
     1.5  subsection {* Representing sums *}
     1.6  
     1.7 -rep_datatype sum
     1.8 -  distinct Inl_not_Inr Inr_not_Inl
     1.9 -  inject Inl_eq Inr_eq
    1.10 -  induction sum_induct
    1.11 +rep_datatype (sum) Inl Inr
    1.12 +proof -
    1.13 +  fix P
    1.14 +  fix s :: "'a + 'b"
    1.15 +  assume x: "\<And>x\<Colon>'a. P (Inl x)" and y: "\<And>y\<Colon>'b. P (Inr y)"
    1.16 +  then show "P s" by (auto intro: sumE [of s])
    1.17 +qed simp_all
    1.18  
    1.19  lemma sum_case_KK[simp]: "sum_case (%x. a) (%x. a) = (%x. a)"
    1.20    by (rule ext) (simp split: sum.split)