arith.ML

--- a/arith.ML	Fri Mar 18 20:33:32 1994 +0100
+++ b/arith.ML	Tue Mar 22 08:25:30 1994 +0100
@@ -51,14 +51,20 @@
 val arith_ss = arith_ss addsimps [add_0_right,add_Suc_right];
 
 (*Associative law for addition*)
-val add_assoc = prove_goal Arith.thy "(m + n) + k = m + (n + k)::nat"
+val add_assoc = prove_goal Arith.thy "m + (n + k) = (m + n) + k::nat"
  (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
 
-(*Commutative law for addition.  Must simplify after first induction!
-  Orientation of rewrites is delicate*)  
+(*Commutative law for addition*)  
 val add_commute = prove_goal Arith.thy "m + n = n + m::nat"
  (fn _ =>  [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
 
+val add_right_commute = prove_goal Arith.thy "(x+y)+z=(x+z)+y::nat"
+ (fn _ => [rtac trans 1, rtac add_commute 1, rtac trans 1,
+           rtac add_assoc 1, rtac (add_commute RS arg_cong) 1]);
+
+val add_ac = [add_assoc, add_commute, add_right_commute];
+
+
 (*** Multiplication ***)
 
 (*right annihilation in product*)
@@ -66,13 +72,9 @@
  (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
 
 (*right Sucessor law for multiplication*)
-val mult_Suc_right = prove_goal Arith.thy 
-    "m * Suc(n) = m + (m * n)"
- (fn _ =>
-  [nat_ind_tac "m" 1,
-   ALLGOALS(asm_simp_tac(arith_ss addsimps [add_assoc RS sym])),
-       (*The final goal requires the commutative law for addition*)
-   stac add_commute 1, rtac refl 1]);
+val mult_Suc_right = prove_goal Arith.thy  "m * Suc(n) = m + (m * n)"
+ (fn _ => [nat_ind_tac "m" 1,
+           ALLGOALS(asm_simp_tac (arith_ss addsimps add_ac))]);
 
 val arith_ss = arith_ss addsimps [mult_0_right,mult_Suc_right];
 
@@ -83,13 +85,19 @@
 (*addition distributes over multiplication*)
 val add_mult_distrib = prove_goal Arith.thy "(m + n)*k = (m*k) + (n*k)::nat"
  (fn _ => [nat_ind_tac "m" 1,
-           ALLGOALS(asm_simp_tac(arith_ss addsimps [add_assoc]))]);
+           ALLGOALS(asm_simp_tac (arith_ss addsimps add_ac))]);
+
+val arith_ss = arith_ss addsimps [add_mult_distrib];
 
 (*Associative law for multiplication*)
-val mult_assoc = prove_goal Arith.thy "(m * n) * k = m * (n * k)::nat"
-  (fn _ => [nat_ind_tac "m" 1,
-            ALLGOALS(asm_simp_tac(arith_ss addsimps [add_mult_distrib]))]);
+val mult_assoc = prove_goal Arith.thy "m * (n * k) = (m * n) * k::nat"
+  (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
 
+val mult_right_commute = prove_goal Arith.thy "(x*y)*z=(x*z)*y::nat"
+ (fn _ => [rtac trans 1, rtac mult_commute 1, rtac trans 1,
+           rtac mult_assoc 1, rtac (mult_commute RS arg_cong) 1]);
+
+val mult_ac = [mult_assoc,mult_commute,mult_right_commute];
 
 (*** Difference ***)
 
@@ -97,7 +105,7 @@
  (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
 
 (*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
-val [prem] = goal Arith.thy "[| ~ m<n |] ==> n + (m-n) = m::nat";
+val [prem] = goal Arith.thy "[| ~ m<n |] ==> (m-n)+n = m::nat";
 by (rtac (prem RS rev_mp) 1);
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
 by (ALLGOALS(asm_simp_tac arith_ss));
@@ -153,10 +161,10 @@
 goal Arith.thy "!!m. 0<n ==> (m div n)*n + m mod n = m";
 by (res_inst_tac [("n","m")] less_induct 1);
 by (rename_tac "k" 1);    (*Variable name used in line below*)
-by (res_inst_tac [("Q","k<n")] (excluded_middle RS disjE) 1);
-by (ALLGOALS (asm_simp_tac(arith_ss addsimps
+by (case_tac "k<n" 1);
+by (ALLGOALS (asm_simp_tac(arith_ss addsimps (add_ac @
                        [mod_less, mod_geq, div_less, div_geq,
-	                add_assoc, add_diff_inverse, div_termination])));
+	                add_diff_inverse, div_termination]))));
 val mod_div_equality = result();
 
 
@@ -210,13 +218,13 @@
 
 goal Arith.thy "n <= (m + n)::nat";
 by (nat_ind_tac "m" 1);
-by (ALLGOALS(simp_tac (arith_ss addsimps [le_refl])));
+by (ALLGOALS(simp_tac arith_ss));
 by (etac le_trans 1);
 by (rtac (lessI RS less_imp_le) 1);
 val le_add2 = result();
 
-goal Arith.thy "m <= (m + n)::nat";
-by (stac add_commute 1);
+goal Arith.thy "n <= (n + m)::nat";
+by (simp_tac (arith_ss addsimps add_ac) 1);
 by (rtac le_add2 1);
 val le_add1 = result();
 
@@ -225,6 +233,6 @@
 
 goal Arith.thy "m+k<=n --> m<=n::nat";
 by(nat_ind_tac "k" 1);
-by(ALLGOALS(simp_tac arith_ss));
+by(ALLGOALS(asm_full_simp_tac arith_ss));
 by(fast_tac (HOL_cs addDs [Suc_leD]) 1);
 val plus_leD1 = result() RS mp;