src/HOL/Integ/NatBin.thy
 changeset 15439 71c0f98e31f1 parent 15251 bb6f072c8d10 child 15440 d0cd75f7a365
equal 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 `
`   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";`
`   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";`