src/HOL/Datatype.thy
changeset 25672 5850301e83c7
parent 25534 d0b74fdd6067
child 25836 f7771e4f7064
equal deleted inserted replaced
25671:5e9d6f77d11a 25672:5850301e83c7
   538 
   538 
   539 rep_datatype sum
   539 rep_datatype sum
   540   distinct Inl_not_Inr Inr_not_Inl
   540   distinct Inl_not_Inr Inr_not_Inl
   541   inject Inl_eq Inr_eq
   541   inject Inl_eq Inr_eq
   542   induction sum_induct
   542   induction sum_induct
   543 
       
   544 lemma size_sum [code func]:
       
   545   "size (x \<Colon> 'a + 'b) = 0" by (cases x) auto
       
   546 
   543 
   547 lemma sum_case_KK[simp]: "sum_case (%x. a) (%x. a) = (%x. a)"
   544 lemma sum_case_KK[simp]: "sum_case (%x. a) (%x. a) = (%x. a)"
   548   by (rule ext) (simp split: sum.split)
   545   by (rule ext) (simp split: sum.split)
   549 
   546 
   550 lemma surjective_sum: "sum_case (%x::'a. f (Inl x)) (%y::'b. f (Inr y)) s = f(s)"
   547 lemma surjective_sum: "sum_case (%x::'a. f (Inl x)) (%y::'b. f (Inr y)) s = f(s)"