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