Simplified proofs.
--- a/src/HOL/Hoare/Arith2.ML Thu Dec 04 09:05:39 1997 +0100
+++ b/src/HOL/Hoare/Arith2.ML Thu Dec 04 09:05:59 1997 +0100
@@ -79,22 +79,11 @@
(*** pow ***)
-val [pow_0,pow_Suc] = nat_recs pow_def;
-store_thm("pow_0",pow_0);
-store_thm("pow_Suc",pow_Suc);
-
-goalw thy [pow_def] "m pow (n+k) = m pow n * m pow k";
-by (nat_ind_tac "k" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [mult_left_commute])));
-qed "pow_add_reduce";
-
-goalw thy [pow_def] "m pow n pow k = m pow (n*k)";
-by (nat_ind_tac "k" 1);
-by (ALLGOALS Asm_simp_tac);
-by (fold_goals_tac [pow_def]);
-by (rtac (pow_add_reduce RS sym) 1);
-qed "pow_pow_reduce";
-
-(*** fac ***)
-
-Addsimps(nat_recs fac_def);
+val prems = goal Power.thy "m mod 2 = 0 ==> ((n::nat)*n)^(m div 2) = n^m";
+by (subgoal_tac "n*n=n^2" 1);
+by (etac ssubst 1);
+by (stac (power_mult RS sym) 1);
+by (stac mult_div_cancel 1);
+by (ALLGOALS(simp_tac (simpset() addsimps prems)));
+qed "sq_pow_div2";
+Addsimps [sq_pow_div2];
--- a/src/HOL/Hoare/Arith2.thy Thu Dec 04 09:05:39 1997 +0100
+++ b/src/HOL/Hoare/Arith2.thy Thu Dec 04 09:05:59 1997 +0100
@@ -6,7 +6,7 @@
More arithmetic. Much of this duplicates ex/Primes.
*)
-Arith2 = Divides +
+Arith2 = Power +
constdefs
cd :: [nat, nat, nat] => bool
@@ -15,10 +15,9 @@
gcd :: [nat, nat] => nat
"gcd m n == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
- pow :: [nat, nat] => nat (infixl 75)
- "m pow n == nat_rec (Suc 0) (%u v. m*v) n"
-
- fac :: nat => nat
- "fac m == nat_rec (Suc 0) (%u v.(Suc u)*v) m"
+consts fac :: nat => nat
+primrec fac nat
+"fac 0 = Suc 0"
+"fac(Suc n) = (Suc n)*fac(n)"
end
--- a/src/HOL/Hoare/Examples.ML Thu Dec 04 09:05:39 1997 +0100
+++ b/src/HOL/Hoare/Examples.ML Thu Dec 04 09:05:59 1997 +0100
@@ -52,35 +52,23 @@
" {a=A & b=B} \
\ c:=1; \
\ WHILE b~=0 \
-\ DO {A pow B = c * a pow b} \
+\ DO {A^B = c * a^b} \
\ WHILE b mod 2=0 \
-\ DO {A pow B = c * a pow b} \
+\ DO {A^B = c * a^b} \
\ a:=a*a; \
\ b:=b div 2 \
\ END; \
\ c:=c*a; \
-\ b:=b-1 \
+\ b:=pred b \
\ END \
-\ {c = A pow B}";
+\ {c = A^B}";
by (hoare_tac 1);
-by (simp_tac ((simpset_of Arith.thy) addsimps [pow_0]) 3);
-
-by (subgoal_tac "a*a=a pow 2" 1);
-by (Asm_simp_tac 1);
-by (stac pow_pow_reduce 1);
-
-by (subgoal_tac "(b div 2)*2=b" 1);
-by (subgoal_tac "0<2" 2);
-by (dres_inst_tac [("m","b")] mod_div_equality 2);
-
-by (ALLGOALS(asm_full_simp_tac(simpset() addsimps[pow_0,pow_Suc,mult_assoc])));
-
by (res_inst_tac [("n","b")] natE 1);
by (hyp_subst_tac 1);
by (asm_full_simp_tac (simpset() addsimps [mod_less]) 1);
-by (asm_simp_tac (simpset() addsimps [pow_Suc]) 1);
+by (asm_simp_tac (simpset() addsimps [mult_assoc]) 1);
qed "power_by_mult";