explicit code lemmas produce nices code
authorhaftmann
Thu Nov 12 15:49:01 2009 +0100 (2009-11-12)
changeset 336339f7280e0c231
parent 33632 6ea8a4cce9e7
child 33634 df25bf15a248
explicit code lemmas produce nices code
src/HOL/Datatype.thy
     1.1 --- a/src/HOL/Datatype.thy	Thu Nov 12 15:48:44 2009 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Thu Nov 12 15:49:01 2009 +0100
     1.3 @@ -562,6 +562,14 @@
     1.4    Sumr :: "('b => 'c) => 'a + 'b => 'c"
     1.5    "Sumr == sum_case undefined"
     1.6  
     1.7 +lemma [code]:
     1.8 +  "Suml f (Inl x) = f x"
     1.9 +  by (simp add: Suml_def)
    1.10 +
    1.11 +lemma [code]:
    1.12 +  "Sumr f (Inr x) = f x"
    1.13 +  by (simp add: Sumr_def)
    1.14 +
    1.15  lemma Suml_inject: "Suml f = Suml g ==> f = g"
    1.16    by (unfold Suml_def) (erule sum_case_inject)
    1.17