| changeset 33633 | 9f7280e0c231 |
| parent 30235 | 58d147683393 |
| child 33959 | 2afc55e8ed27 |
--- a/src/HOL/Datatype.thy Thu Nov 12 15:48:44 2009 +0100 +++ b/src/HOL/Datatype.thy Thu Nov 12 15:49:01 2009 +0100 @@ -562,6 +562,14 @@ Sumr :: "('b => 'c) => 'a + 'b => 'c" "Sumr == sum_case undefined" +lemma [code]: + "Suml f (Inl x) = f x" + by (simp add: Suml_def) + +lemma [code]: + "Sumr f (Inr x) = f x" + by (simp add: Sumr_def) + lemma Suml_inject: "Suml f = Suml g ==> f = g" by (unfold Suml_def) (erule sum_case_inject)