# HG changeset patch
# User nipkow
# Date 881222759 -3600
# Node ID 6f2986464280b66be6857ef5f02f8cc7891e5878
# Parent  aa22fcb46a5d2d04bdd615d4f06b44bc1d205f6e
Simplified proofs.

diff -r aa22fcb46a5d -r 6f2986464280 src/HOL/Hoare/Arith2.ML
--- 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];
diff -r aa22fcb46a5d -r 6f2986464280 src/HOL/Hoare/Arith2.thy
--- 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
diff -r aa22fcb46a5d -r 6f2986464280 src/HOL/Hoare/Examples.ML
--- 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";