src/HOL/Import/HOLLightCompat.thy
changeset 19064 bf19cc5a7899
parent 17322 781abf7011e6
child 35416 d8d7d1b785af
--- a/src/HOL/Import/HOLLightCompat.thy	Wed Feb 15 21:35:13 2006 +0100
+++ b/src/HOL/Import/HOLLightCompat.thy	Wed Feb 15 23:57:06 2006 +0100
@@ -91,6 +91,16 @@
 lemma NUMERAL_BIT1_altdef: "NUMERAL_BIT1 n = Suc (n + n)"
   by (simp add: NUMERAL_BIT1_def)
 
+consts
+  sumlift :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> (('a + 'b) \<Rightarrow> 'c)"
 
+primrec
+  "sumlift f g (Inl a) = f a"
+  "sumlift f g (Inr b) = g b"
+  
+lemma sum_Recursion: "\<exists> f. (\<forall> a. f (Inl a) = Inl' a) \<and> (\<forall> b. f (Inr b) = Inr' b)"
+  apply (rule exI[where x="sumlift Inl' Inr'"])
+  apply auto
+  done
 
 end