src/HOL/Import/HOLLightCompat.thy
changeset 19064 bf19cc5a7899
parent 17322 781abf7011e6
child 35416 d8d7d1b785af
equal deleted inserted replaced
19063:049c010c8fb7 19064:bf19cc5a7899
    89   "NUMERAL_BIT0 n \<equiv> n + n"
    89   "NUMERAL_BIT0 n \<equiv> n + n"
    90 
    90 
    91 lemma NUMERAL_BIT1_altdef: "NUMERAL_BIT1 n = Suc (n + n)"
    91 lemma NUMERAL_BIT1_altdef: "NUMERAL_BIT1 n = Suc (n + n)"
    92   by (simp add: NUMERAL_BIT1_def)
    92   by (simp add: NUMERAL_BIT1_def)
    93 
    93 
       
    94 consts
       
    95   sumlift :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> (('a + 'b) \<Rightarrow> 'c)"
    94 
    96 
       
    97 primrec
       
    98   "sumlift f g (Inl a) = f a"
       
    99   "sumlift f g (Inr b) = g b"
       
   100   
       
   101 lemma sum_Recursion: "\<exists> f. (\<forall> a. f (Inl a) = Inl' a) \<and> (\<forall> b. f (Inr b) = Inr' b)"
       
   102   apply (rule exI[where x="sumlift Inl' Inr'"])
       
   103   apply auto
       
   104   done
    95 
   105 
    96 end
   106 end