vdash: a formal math wiki
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:

Email:
Coming Soon!

Creative Commons License This page by Cameron Freer is licensed under a Creative Commons Attribution 3.0 License.