src/HOL/Old_Number_Theory/Int2.thy
changeset 41541 1fa4725c4656
parent 38159 e9b4835a54ee
child 44766 d4d33a4d7548
     1.1 --- a/src/HOL/Old_Number_Theory/Int2.thy	Thu Jan 13 21:50:13 2011 +0100
     1.2 +++ b/src/HOL/Old_Number_Theory/Int2.thy	Thu Jan 13 23:50:16 2011 +0100
     1.3 @@ -43,38 +43,39 @@
     1.4    apply (force simp del:dvd_mult)
     1.5    done
     1.6  
     1.7 -lemma div_prop1: "[| 0 < z; (x::int) < y * z |] ==> x div z < y"
     1.8 +lemma div_prop1:
     1.9 +  assumes "0 < z" and "(x::int) < y * z"
    1.10 +  shows "x div z < y"
    1.11  proof -
    1.12 -  assume "0 < z" then have modth: "x mod z \<ge> 0" by simp
    1.13 +  from `0 < z` have modth: "x mod z \<ge> 0" by simp
    1.14    have "(x div z) * z \<le> (x div z) * z" by simp
    1.15    then have "(x div z) * z \<le> (x div z) * z + x mod z" using modth by arith 
    1.16    also have "\<dots> = x"
    1.17      by (auto simp add: zmod_zdiv_equality [symmetric] zmult_ac)
    1.18 -  also assume  "x < y * z"
    1.19 +  also note `x < y * z`
    1.20    finally show ?thesis
    1.21 -    by (auto simp add: prems mult_less_cancel_right, insert prems, arith)
    1.22 +    apply (auto simp add: mult_less_cancel_right)
    1.23 +    using assms apply arith
    1.24 +    done
    1.25  qed
    1.26  
    1.27 -lemma div_prop2: "[| 0 < z; (x::int) < (y * z) + z |] ==> x div z \<le> y"
    1.28 +lemma div_prop2:
    1.29 +  assumes "0 < z" and "(x::int) < (y * z) + z"
    1.30 +  shows "x div z \<le> y"
    1.31  proof -
    1.32 -  assume "0 < z" and "x < (y * z) + z"
    1.33 -  then have "x < (y + 1) * z" by (auto simp add: int_distrib)
    1.34 +  from assms have "x < (y + 1) * z" by (auto simp add: int_distrib)
    1.35    then have "x div z < y + 1"
    1.36 -    apply -
    1.37      apply (rule_tac y = "y + 1" in div_prop1)
    1.38 -    apply (auto simp add: prems)
    1.39 +    apply (auto simp add: `0 < z`)
    1.40      done
    1.41    then show ?thesis by auto
    1.42  qed
    1.43  
    1.44 -lemma zdiv_leq_prop: "[| 0 < y |] ==> y * (x div y) \<le> (x::int)"
    1.45 +lemma zdiv_leq_prop: assumes "0 < y" shows "y * (x div y) \<le> (x::int)"
    1.46  proof-
    1.47 -  assume "0 < y"
    1.48    from zmod_zdiv_equality have "x = y * (x div y) + x mod y" by auto
    1.49 -  moreover have "0 \<le> x mod y"
    1.50 -    by (auto simp add: prems pos_mod_sign)
    1.51 -  ultimately show ?thesis
    1.52 -    by arith
    1.53 +  moreover have "0 \<le> x mod y" by (auto simp add: assms)
    1.54 +  ultimately show ?thesis by arith
    1.55  qed
    1.56  
    1.57  
    1.58 @@ -87,7 +88,7 @@
    1.59    by (auto simp add: zcong_def)
    1.60  
    1.61  lemma zcong_shift: "[a = b] (mod m) ==> [a + c = b + c] (mod m)"
    1.62 -  by (auto simp add: zcong_refl zcong_zadd)
    1.63 +  by (auto simp add: zcong_zadd)
    1.64  
    1.65  lemma zcong_zpower: "[x = y](mod m) ==> [x^z = y^z](mod m)"
    1.66    by (induct z) (auto simp add: zcong_zmult)
    1.67 @@ -126,11 +127,12 @@
    1.68      x < m; y < m |] ==> x = y"
    1.69    by (metis zcong_not zcong_sym zless_linear)
    1.70  
    1.71 -lemma zcong_neg_1_impl_ne_1: "[| 2 < p; [x = -1] (mod p) |] ==>
    1.72 -    ~([x = 1] (mod p))"
    1.73 +lemma zcong_neg_1_impl_ne_1:
    1.74 +  assumes "2 < p" and "[x = -1] (mod p)"
    1.75 +  shows "~([x = 1] (mod p))"
    1.76  proof
    1.77 -  assume "2 < p" and "[x = 1] (mod p)" and "[x = -1] (mod p)"
    1.78 -  then have "[1 = -1] (mod p)"
    1.79 +  assume "[x = 1] (mod p)"
    1.80 +  with assms have "[1 = -1] (mod p)"
    1.81      apply (auto simp add: zcong_sym)
    1.82      apply (drule zcong_trans, auto)
    1.83      done
    1.84 @@ -140,7 +142,7 @@
    1.85      by auto
    1.86    then have "p dvd 2"
    1.87      by (auto simp add: dvd_def zcong_def)
    1.88 -  with prems show False
    1.89 +  with `2 < p` show False
    1.90      by (auto simp add: zdvd_not_zless)
    1.91  qed
    1.92  
    1.93 @@ -181,15 +183,15 @@
    1.94  lemma MultInv_prop2: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==>
    1.95    [(x * (MultInv p x)) = 1] (mod p)"
    1.96  proof (simp add: MultInv_def zcong_eq_zdvd_prop)
    1.97 -  assume "2 < p" and "zprime p" and "~ p dvd x"
    1.98 +  assume 1: "2 < p" and 2: "zprime p" and 3: "~ p dvd x"
    1.99    have "x * x ^ nat (p - 2) = x ^ (nat (p - 2) + 1)"
   1.100      by auto
   1.101 -  also from prems have "nat (p - 2) + 1 = nat (p - 2 + 1)"
   1.102 +  also from 1 have "nat (p - 2) + 1 = nat (p - 2 + 1)"
   1.103      by (simp only: nat_add_distrib)
   1.104    also have "p - 2 + 1 = p - 1" by arith
   1.105    finally have "[x * x ^ nat (p - 2) = x ^ nat (p - 1)] (mod p)"
   1.106      by (rule ssubst, auto)
   1.107 -  also from prems have "[x ^ nat (p - 1) = 1] (mod p)"
   1.108 +  also from 2 3 have "[x ^ nat (p - 1) = 1] (mod p)"
   1.109      by (auto simp add: Little_Fermat)
   1.110    finally (zcong_trans) show "[x * x ^ nat (p - 2) = 1] (mod p)" .
   1.111  qed