src/HOL/Integ/NatBin.thy
changeset 15439 71c0f98e31f1
parent 15251 bb6f072c8d10
child 15440 d0cd75f7a365
equal deleted inserted replaced
15438:dfc7d2a824d6 15439:71c0f98e31f1
   386 lemma power_eq_if: "(p ^ m :: nat) = (if m=0 then 1 else p * (p ^ (m - 1)))"
   386 lemma power_eq_if: "(p ^ m :: nat) = (if m=0 then 1 else p * (p ^ (m - 1)))"
   387 apply (case_tac "m")
   387 apply (case_tac "m")
   388 apply (simp_all add: numerals)
   388 apply (simp_all add: numerals)
   389 done
   389 done
   390 
   390 
   391 lemma diff_less': "[| 0<n; 0<m |] ==> m - n < (m::nat)"
       
   392 by (simp add: diff_less numerals)
       
   393 
       
   394 declare diff_less' [of "number_of v", standard, simp]
       
   395 
       
   396 
   391 
   397 subsection{*Comparisons involving (0::nat) *}
   392 subsection{*Comparisons involving (0::nat) *}
   398 
   393 
   399 text{*Simplification already does @{term "n<0"}, @{term "n\<le>0"} and @{term "0\<le>n"}.*}
   394 text{*Simplification already does @{term "n<0"}, @{term "n\<le>0"} and @{term "0\<le>n"}.*}
   400 
   395 
   762 val Suc_eq_add_numeral_1 = thm"Suc_eq_add_numeral_1";
   757 val Suc_eq_add_numeral_1 = thm"Suc_eq_add_numeral_1";
   763 val Suc_eq_add_numeral_1_left = thm"Suc_eq_add_numeral_1_left";
   758 val Suc_eq_add_numeral_1_left = thm"Suc_eq_add_numeral_1_left";
   764 val add_eq_if = thm"add_eq_if";
   759 val add_eq_if = thm"add_eq_if";
   765 val mult_eq_if = thm"mult_eq_if";
   760 val mult_eq_if = thm"mult_eq_if";
   766 val power_eq_if = thm"power_eq_if";
   761 val power_eq_if = thm"power_eq_if";
   767 val diff_less' = thm"diff_less'";
       
   768 val eq_number_of_0 = thm"eq_number_of_0";
   762 val eq_number_of_0 = thm"eq_number_of_0";
   769 val eq_0_number_of = thm"eq_0_number_of";
   763 val eq_0_number_of = thm"eq_0_number_of";
   770 val less_0_number_of = thm"less_0_number_of";
   764 val less_0_number_of = thm"less_0_number_of";
   771 val neg_imp_number_of_eq_0 = thm"neg_imp_number_of_eq_0";
   765 val neg_imp_number_of_eq_0 = thm"neg_imp_number_of_eq_0";
   772 val eq_number_of_Suc = thm"eq_number_of_Suc";
   766 val eq_number_of_Suc = thm"eq_number_of_Suc";