tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
authorboehmes
Wed Mar 17 19:55:07 2010 +0100 (2010-03-17)
changeset 3581510e723e54076
parent 35814 234eaa508359
child 35824 b766aad9136d
child 35829 c5f54c04a1aa
tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
src/HOL/Divides.thy
src/HOL/Int.thy
src/HOL/Nat_Numeral.thy
     1.1 --- a/src/HOL/Divides.thy	Wed Mar 17 17:23:45 2010 +0100
     1.2 +++ b/src/HOL/Divides.thy	Wed Mar 17 19:55:07 2010 +0100
     1.3 @@ -588,8 +588,16 @@
     1.4    from divmod_nat_rel have divmod_nat_m_n: "divmod_nat_rel m n (m div n, m mod n)" .
     1.5    with assms have m_div_n: "m div n \<ge> 1"
     1.6      by (cases "m div n") (auto simp add: divmod_nat_rel_def)
     1.7 -  from assms divmod_nat_m_n have "divmod_nat_rel (m - n) n (m div n - Suc 0, m mod n)"
     1.8 -    by (cases "m div n") (auto simp add: divmod_nat_rel_def)
     1.9 +  have "divmod_nat_rel (m - n) n (m div n - Suc 0, m mod n)"
    1.10 +  proof -
    1.11 +    from assms have
    1.12 +      "n \<noteq> 0"
    1.13 +      "\<And>k. m = Suc k * n + m mod n ==> m - n = (Suc k - Suc 0) * n + m mod n"
    1.14 +      by simp_all
    1.15 +    then show ?thesis using assms divmod_nat_m_n 
    1.16 +      by (cases "m div n")
    1.17 +         (simp_all only: divmod_nat_rel_def fst_conv snd_conv, simp_all)
    1.18 +  qed
    1.19    with divmod_nat_eq have "divmod_nat (m - n) n = (m div n - Suc 0, m mod n)" by simp
    1.20    moreover from divmod_nat_div_mod have "divmod_nat (m - n) n = ((m - n) div n, (m - n) mod n)" .
    1.21    ultimately have "m div n = Suc ((m - n) div n)"
    1.22 @@ -1122,7 +1130,7 @@
    1.23  
    1.24  lemma mod2_gr_0 [simp]: "0 < (m\<Colon>nat) mod 2 \<longleftrightarrow> m mod 2 = 1"
    1.25  proof -
    1.26 -  { fix n :: nat have  "(n::nat) < 2 \<Longrightarrow> n = 0 \<or> n = 1" by (induct n) simp_all }
    1.27 +  { fix n :: nat have  "(n::nat) < 2 \<Longrightarrow> n = 0 \<or> n = 1" by (cases n) simp_all }
    1.28    moreover have "m mod 2 < 2" by simp
    1.29    ultimately have "m mod 2 = 0 \<or> m mod 2 = 1" .
    1.30    then show ?thesis by auto
    1.31 @@ -1166,8 +1174,11 @@
    1.32  lemma Suc_n_div_2_gt_zero [simp]: "(0::nat) < n ==> 0 < (n + 1) div 2"
    1.33  by (cases n) simp_all
    1.34  
    1.35 -lemma div_2_gt_zero [simp]: "(1::nat) < n ==> 0 < n div 2" 
    1.36 -using Suc_n_div_2_gt_zero [of "n - 1"] by simp
    1.37 +lemma div_2_gt_zero [simp]: assumes A: "(1::nat) < n" shows "0 < n div 2"
    1.38 +proof -
    1.39 +  from A have B: "0 < n - 1" and C: "n - 1 + 1 = n" by simp_all
    1.40 +  from Suc_n_div_2_gt_zero [OF B] C show ?thesis by simp 
    1.41 +qed
    1.42  
    1.43    (* Potential use of algebra : Equality modulo n*)
    1.44  lemma mod_mult_self3 [simp]: "(k*n + m) mod n = m mod (n::nat)"
    1.45 @@ -2092,15 +2103,16 @@
    1.46                    div_pos_pos_trivial)
    1.47  qed
    1.48  
    1.49 -lemma neg_zdiv_mult_2: "a \<le> (0::int) ==> (1 + 2*b) div (2*a) = (b+1) div a"
    1.50 -apply (subgoal_tac " (1 + 2* (-b - 1)) div (2 * (-a)) = (-b - 1) div (-a) ")
    1.51 -apply (rule_tac [2] pos_zdiv_mult_2)
    1.52 -apply (auto simp add: right_diff_distrib)
    1.53 -apply (subgoal_tac " (-1 - (2 * b)) = - (1 + (2 * b))")
    1.54 -apply (simp only: zdiv_zminus_zminus diff_minus minus_add_distrib [symmetric])
    1.55 -apply (simp_all add: algebra_simps)
    1.56 -apply (simp only: ab_diff_minus minus_add_distrib [symmetric] number_of_Min zdiv_zminus_zminus)
    1.57 -done
    1.58 +lemma neg_zdiv_mult_2: 
    1.59 +  assumes A: "a \<le> (0::int)" shows "(1 + 2*b) div (2*a) = (b+1) div a"
    1.60 +proof -
    1.61 +  have R: "1 + - (2 * (b + 1)) = - (1 + 2 * b)" by simp
    1.62 +  have "(1 + 2 * (-b - 1)) div (2 * (-a)) = (-b - 1) div (-a)"
    1.63 +    by (rule pos_zdiv_mult_2, simp add: A)
    1.64 +  thus ?thesis
    1.65 +    by (simp only: R zdiv_zminus_zminus diff_minus
    1.66 +      minus_add_distrib [symmetric] mult_minus_right)
    1.67 +qed
    1.68  
    1.69  lemma zdiv_number_of_Bit0 [simp]:
    1.70       "number_of (Int.Bit0 v) div number_of (Int.Bit0 w) =  
     2.1 --- a/src/HOL/Int.thy	Wed Mar 17 17:23:45 2010 +0100
     2.2 +++ b/src/HOL/Int.thy	Wed Mar 17 19:55:07 2010 +0100
     2.3 @@ -1829,11 +1829,12 @@
     2.4  lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int) | m = -1"
     2.5  by (insert abs_zmult_eq_1 [of m n], arith)
     2.6  
     2.7 -lemma pos_zmult_eq_1_iff: "0 < (m::int) ==> (m * n = 1) = (m = 1 & n = 1)"
     2.8 -apply (auto dest: pos_zmult_eq_1_iff_lemma) 
     2.9 -apply (simp add: mult_commute [of m]) 
    2.10 -apply (frule pos_zmult_eq_1_iff_lemma, auto) 
    2.11 -done
    2.12 +lemma pos_zmult_eq_1_iff:
    2.13 +  assumes "0 < (m::int)" shows "(m * n = 1) = (m = 1 & n = 1)"
    2.14 +proof -
    2.15 +  from assms have "m * n = 1 ==> m = 1" by (auto dest: pos_zmult_eq_1_iff_lemma)
    2.16 +  thus ?thesis by (auto dest: pos_zmult_eq_1_iff_lemma)
    2.17 +qed
    2.18  
    2.19  lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"
    2.20  apply (rule iffI) 
     3.1 --- a/src/HOL/Nat_Numeral.thy	Wed Mar 17 17:23:45 2010 +0100
     3.2 +++ b/src/HOL/Nat_Numeral.thy	Wed Mar 17 19:55:07 2010 +0100
     3.3 @@ -643,8 +643,9 @@
     3.4    fixes z :: "'a::number_ring"
     3.5    shows "z ^ number_of (Int.Bit1 w) = (if (0::int) <= number_of w
     3.6       then (let w = z ^ (number_of w) in z * w * w) else 1)"
     3.7 -apply (auto simp add: Let_def Bit1_def nat_number_of_def number_of_is_id
     3.8 -  mult_assoc nat_add_distrib power_add not_le simp del: nat_number_of)
     3.9 +unfolding Let_def Bit1_def nat_number_of_def number_of_is_id
    3.10 +apply (cases "0 <= w")
    3.11 +apply (simp only: mult_assoc nat_add_distrib power_add, simp)
    3.12  apply (simp add: not_le mult_2 [symmetric] add_assoc)
    3.13  done
    3.14  
    3.15 @@ -673,9 +674,10 @@
    3.16    "number_of (Int.Bit1 w) =
    3.17      (if neg (number_of w :: int) then 0
    3.18       else let n = number_of w in Suc (n + n))"
    3.19 -apply (auto simp add: Let_def Bit1_def nat_number_of_def number_of_is_id neg_def
    3.20 -  nat_add_distrib simp del: nat_number_of)
    3.21 +unfolding Let_def Bit1_def nat_number_of_def number_of_is_id neg_def
    3.22 +apply (cases "w < 0")
    3.23  apply (simp add: mult_2 [symmetric] add_assoc)
    3.24 +apply (simp only: nat_add_distrib, simp)
    3.25  done
    3.26  
    3.27  lemmas nat_number =