# HG changeset patch
# User berghofe
# Date 1034252281 -7200
# Node ID c41e88151b54198f261546839caa9b10fe674cf9
# Parent  99a593b49b04c4252719b369658ce466790cd068
Added functions Suml and Sumr which are useful for constructing
datatypes involving function types.

diff -r 99a593b49b04 -r c41e88151b54 src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Wed Oct 09 11:07:13 2002 +0200
+++ b/src/HOL/Datatype.thy	Thu Oct 10 14:18:01 2002 +0200
@@ -8,13 +8,6 @@
 
 theory Datatype = Datatype_Universe:
 
-subsection {* Finishing the datatype package setup *}
-
-text {* Belongs to theory @{text Datatype_Universe}; hides popular names. *}
-hide const Node Atom Leaf Numb Lim Funs Split Case
-hide type node item
-
-
 subsection {* Representing primitive types *}
 
 rep_datatype bool
@@ -70,6 +63,26 @@
     done
 qed
 
+constdefs
+  Suml :: "('a => 'c) => 'a + 'b => 'c"
+  "Suml == (%f. sum_case f arbitrary)"
+
+  Sumr :: "('b => 'c) => 'a + 'b => 'c"
+  "Sumr == sum_case arbitrary"
+
+lemma Suml_inject: "Suml f = Suml g ==> f = g"
+  by (unfold Suml_def) (erule sum_case_inject)
+
+lemma Sumr_inject: "Sumr f = Sumr g ==> f = g"
+  by (unfold Sumr_def) (erule sum_case_inject)
+
+
+subsection {* Finishing the datatype package setup *}
+
+text {* Belongs to theory @{text Datatype_Universe}; hides popular names. *}
+hide const Node Atom Leaf Numb Lim Split Case Suml Sumr
+hide type node item
+
 
 subsection {* Further cases/induct rules for tuples *}