theorem "( a :: int )
dvd b ==> a ^ n dvd
b ^ n" proof - assume
"a dvd b" show "a ^ n
dvd b ^ n" proof
( induct n ) show
"a^0 dvd b^0" proof
- have "a^0 = 1" by ( rule power_0 ) moreover
have "( 1 dvd b ^ 0 )" by ( rule zdvd_1_left)
ultimately show ?thesis by simp qed next
fix n assume "a ^ n dvd b ^ n" show "a ^ Suc
n dvd b ^ Suc n" proof - from prems
have "a * a ^ n dvd b * b ^ n" by ( intro
zdvd_zmult_mono ) moreover have "a ^ Suc n
= a * a^n" by ( rule
power_Suc ) moreover
have "b ^ Suc n =
b * b^n" by (rule
power_Suc) ultimately
show ?thesis by simp
qed qed qed
|
|
Background
Slides
Contact
For more information, email freer@mit.edu
or subscribe to the
google groups mailing list:
|
