# HG changeset patch
# User boehmes
# Date 1268852107 -3600
# Node ID 10e723e540760e41575aab8a5e95a25072673a77
# Parent  234eaa50835940d196651f37866b40de4dbf624b
tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)

diff -r 234eaa508359 -r 10e723e54076 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Wed Mar 17 17:23:45 2010 +0100
+++ b/src/HOL/Divides.thy	Wed Mar 17 19:55:07 2010 +0100
@@ -588,8 +588,16 @@
   from divmod_nat_rel have divmod_nat_m_n: "divmod_nat_rel m n (m div n, m mod n)" .
   with assms have m_div_n: "m div n \<ge> 1"
     by (cases "m div n") (auto simp add: divmod_nat_rel_def)
-  from assms divmod_nat_m_n have "divmod_nat_rel (m - n) n (m div n - Suc 0, m mod n)"
-    by (cases "m div n") (auto simp add: divmod_nat_rel_def)
+  have "divmod_nat_rel (m - n) n (m div n - Suc 0, m mod n)"
+  proof -
+    from assms have
+      "n \<noteq> 0"
+      "\<And>k. m = Suc k * n + m mod n ==> m - n = (Suc k - Suc 0) * n + m mod n"
+      by simp_all
+    then show ?thesis using assms divmod_nat_m_n 
+      by (cases "m div n")
+         (simp_all only: divmod_nat_rel_def fst_conv snd_conv, simp_all)
+  qed
   with divmod_nat_eq have "divmod_nat (m - n) n = (m div n - Suc 0, m mod n)" by simp
   moreover from divmod_nat_div_mod have "divmod_nat (m - n) n = ((m - n) div n, (m - n) mod n)" .
   ultimately have "m div n = Suc ((m - n) div n)"
@@ -1122,7 +1130,7 @@
 
 lemma mod2_gr_0 [simp]: "0 < (m\<Colon>nat) mod 2 \<longleftrightarrow> m mod 2 = 1"
 proof -
-  { fix n :: nat have  "(n::nat) < 2 \<Longrightarrow> n = 0 \<or> n = 1" by (induct n) simp_all }
+  { fix n :: nat have  "(n::nat) < 2 \<Longrightarrow> n = 0 \<or> n = 1" by (cases n) simp_all }
   moreover have "m mod 2 < 2" by simp
   ultimately have "m mod 2 = 0 \<or> m mod 2 = 1" .
   then show ?thesis by auto
@@ -1166,8 +1174,11 @@
 lemma Suc_n_div_2_gt_zero [simp]: "(0::nat) < n ==> 0 < (n + 1) div 2"
 by (cases n) simp_all
 
-lemma div_2_gt_zero [simp]: "(1::nat) < n ==> 0 < n div 2" 
-using Suc_n_div_2_gt_zero [of "n - 1"] by simp
+lemma div_2_gt_zero [simp]: assumes A: "(1::nat) < n" shows "0 < n div 2"
+proof -
+  from A have B: "0 < n - 1" and C: "n - 1 + 1 = n" by simp_all
+  from Suc_n_div_2_gt_zero [OF B] C show ?thesis by simp 
+qed
 
   (* Potential use of algebra : Equality modulo n*)
 lemma mod_mult_self3 [simp]: "(k*n + m) mod n = m mod (n::nat)"
@@ -2092,15 +2103,16 @@
                   div_pos_pos_trivial)
 qed
 
-lemma neg_zdiv_mult_2: "a \<le> (0::int) ==> (1 + 2*b) div (2*a) = (b+1) div a"
-apply (subgoal_tac " (1 + 2* (-b - 1)) div (2 * (-a)) = (-b - 1) div (-a) ")
-apply (rule_tac [2] pos_zdiv_mult_2)
-apply (auto simp add: right_diff_distrib)
-apply (subgoal_tac " (-1 - (2 * b)) = - (1 + (2 * b))")
-apply (simp only: zdiv_zminus_zminus diff_minus minus_add_distrib [symmetric])
-apply (simp_all add: algebra_simps)
-apply (simp only: ab_diff_minus minus_add_distrib [symmetric] number_of_Min zdiv_zminus_zminus)
-done
+lemma neg_zdiv_mult_2: 
+  assumes A: "a \<le> (0::int)" shows "(1 + 2*b) div (2*a) = (b+1) div a"
+proof -
+  have R: "1 + - (2 * (b + 1)) = - (1 + 2 * b)" by simp
+  have "(1 + 2 * (-b - 1)) div (2 * (-a)) = (-b - 1) div (-a)"
+    by (rule pos_zdiv_mult_2, simp add: A)
+  thus ?thesis
+    by (simp only: R zdiv_zminus_zminus diff_minus
+      minus_add_distrib [symmetric] mult_minus_right)
+qed
 
 lemma zdiv_number_of_Bit0 [simp]:
      "number_of (Int.Bit0 v) div number_of (Int.Bit0 w) =  
diff -r 234eaa508359 -r 10e723e54076 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Wed Mar 17 17:23:45 2010 +0100
+++ b/src/HOL/Int.thy	Wed Mar 17 19:55:07 2010 +0100
@@ -1829,11 +1829,12 @@
 lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int) | m = -1"
 by (insert abs_zmult_eq_1 [of m n], arith)
 
-lemma pos_zmult_eq_1_iff: "0 < (m::int) ==> (m * n = 1) = (m = 1 & n = 1)"
-apply (auto dest: pos_zmult_eq_1_iff_lemma) 
-apply (simp add: mult_commute [of m]) 
-apply (frule pos_zmult_eq_1_iff_lemma, auto) 
-done
+lemma pos_zmult_eq_1_iff:
+  assumes "0 < (m::int)" shows "(m * n = 1) = (m = 1 & n = 1)"
+proof -
+  from assms have "m * n = 1 ==> m = 1" by (auto dest: pos_zmult_eq_1_iff_lemma)
+  thus ?thesis by (auto dest: pos_zmult_eq_1_iff_lemma)
+qed
 
 lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"
 apply (rule iffI) 
diff -r 234eaa508359 -r 10e723e54076 src/HOL/Nat_Numeral.thy
--- a/src/HOL/Nat_Numeral.thy	Wed Mar 17 17:23:45 2010 +0100
+++ b/src/HOL/Nat_Numeral.thy	Wed Mar 17 19:55:07 2010 +0100
@@ -643,8 +643,9 @@
   fixes z :: "'a::number_ring"
   shows "z ^ number_of (Int.Bit1 w) = (if (0::int) <= number_of w
      then (let w = z ^ (number_of w) in z * w * w) else 1)"
-apply (auto simp add: Let_def Bit1_def nat_number_of_def number_of_is_id
-  mult_assoc nat_add_distrib power_add not_le simp del: nat_number_of)
+unfolding Let_def Bit1_def nat_number_of_def number_of_is_id
+apply (cases "0 <= w")
+apply (simp only: mult_assoc nat_add_distrib power_add, simp)
 apply (simp add: not_le mult_2 [symmetric] add_assoc)
 done
 
@@ -673,9 +674,10 @@
   "number_of (Int.Bit1 w) =
     (if neg (number_of w :: int) then 0
      else let n = number_of w in Suc (n + n))"
-apply (auto simp add: Let_def Bit1_def nat_number_of_def number_of_is_id neg_def
-  nat_add_distrib simp del: nat_number_of)
+unfolding Let_def Bit1_def nat_number_of_def number_of_is_id neg_def
+apply (cases "w < 0")
 apply (simp add: mult_2 [symmetric] add_assoc)
+apply (simp only: nat_add_distrib, simp)
 done
 
 lemmas nat_number =