equal
deleted
inserted
replaced
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)" |