equal
deleted
inserted
replaced
417 apply (simp add: power_0_left) |
417 apply (simp add: power_0_left) |
418 apply (rule nonzero_power_divide) |
418 apply (rule nonzero_power_divide) |
419 apply assumption |
419 apply assumption |
420 done |
420 done |
421 |
421 |
422 class recpower = monoid_mult |
|
423 |
|
424 |
422 |
425 subsection {* Exponentiation for the Natural Numbers *} |
423 subsection {* Exponentiation for the Natural Numbers *} |
426 |
|
427 instance nat :: recpower .. |
|
428 |
424 |
429 lemma nat_one_le_power [simp]: |
425 lemma nat_one_le_power [simp]: |
430 "Suc 0 \<le> i \<Longrightarrow> Suc 0 \<le> i ^ n" |
426 "Suc 0 \<le> i \<Longrightarrow> Suc 0 \<le> i ^ n" |
431 by (rule one_le_power [of i n, unfolded One_nat_def]) |
427 by (rule one_le_power [of i n, unfolded One_nat_def]) |
432 |
428 |