New lemmas for gcd example

--- a/src/HOL/Arith.ML	Fri Jun 14 12:21:02 1996 +0200
+++ b/src/HOL/Arith.ML	Fri Jun 14 12:22:42 1996 +0200
@@ -140,6 +140,14 @@
 
 Addsimps [mult_0_right,mult_Suc_right];
 
+goal Arith.thy "1 * n = n";
+by (Asm_simp_tac 1);
+qed "mult_1";
+
+goal Arith.thy "n * 1 = n";
+by (Asm_simp_tac 1);
+qed "mult_1_right";
+
 (*Commutative law for multiplication*)
 qed_goal "mult_commute" Arith.thy "m * n = n * (m::nat)"
  (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
@@ -153,11 +161,10 @@
  (fn _ => [nat_ind_tac "m" 1,
            ALLGOALS(asm_simp_tac (!simpset addsimps add_ac))]);
 
-Addsimps [add_mult_distrib,add_mult_distrib2];
-
 (*Associative law for multiplication*)
 qed_goal "mult_assoc" Arith.thy "(m * n) * k = m * ((n * k)::nat)"
-  (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
+  (fn _ => [nat_ind_tac "m" 1, 
+	    ALLGOALS (asm_simp_tac (!simpset addsimps [add_mult_distrib]))]);
 
 qed_goal "mult_left_commute" Arith.thy "x*(y*z) = y*((x*z)::nat)"
  (fn _ => [rtac trans 1, rtac mult_commute 1, rtac trans 1,
@@ -540,6 +547,14 @@
 by (ALLGOALS Asm_simp_tac);
 qed "zero_less_mult_iff";
 
+goal Arith.thy "(m*n = 1) = (m=1 & n=1)";
+by (nat_ind_tac "m" 1);
+by (Simp_tac 1);
+by (nat_ind_tac "n" 1);
+by (Simp_tac 1);
+by (fast_tac (!claset addss !simpset) 1);
+qed "mult_eq_1_iff";
+
 (*Cancellation law for division*)
 goal Arith.thy "!!k. [| 0<n; 0<k |] ==> (k*m) div (k*n) = m div n";
 by (res_inst_tac [("n","m")] less_induct 1);
@@ -568,3 +583,15 @@
 qed "mult_mod_distrib";
 
 
+(** Lemma for gcd **)
+
+goal Arith.thy "!!m n. m = m*n ==> n=1 | m=0";
+by (dtac sym 1);
+by (rtac disjCI 1);
+by (rtac nat_less_cases 1 THEN assume_tac 2);
+by (fast_tac (!claset addss !simpset) 1);
+by (fast_tac (!claset addDs [mult_less_mono2] 
+                      addss (!simpset addsimps [zero_less_eq RS sym])) 1);
+qed "mult_eq_self_implies_10";
+
+