Tuned and simplified proofs
authorchaieb
Mon Jul 21 13:36:59 2008 +0200 (2008-07-21)
changeset 276686eb20b2cecf8
parent 27667 62500b980749
child 27669 4b1642284dd7
Tuned and simplified proofs
src/HOL/Complex/Fundamental_Theorem_Algebra.thy
src/HOL/Hyperreal/Deriv.thy
src/HOL/Library/Abstract_Rat.thy
src/HOL/Library/Parity.thy
src/HOL/Library/Pocklington.thy
src/HOL/Presburger.thy
src/HOL/Real/Rational.thy
src/HOL/Real/RealDef.thy
     1.1 --- a/src/HOL/Complex/Fundamental_Theorem_Algebra.thy	Mon Jul 21 13:36:44 2008 +0200
     1.2 +++ b/src/HOL/Complex/Fundamental_Theorem_Algebra.thy	Mon Jul 21 13:36:59 2008 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4             else Complex (sqrt((cmod z + Re z) /2))
     1.5                          ((Im z / abs(Im z)) * sqrt((cmod z - Re z) /2)))"
     1.6  
     1.7 -lemma csqrt: "csqrt z ^ 2 = z"
     1.8 +lemma csqrt[algebra]: "csqrt z ^ 2 = z"
     1.9  proof-
    1.10    obtain x y where xy: "z = Complex x y" by (cases z, simp_all)
    1.11    {assume y0: "y = 0"
    1.12 @@ -34,10 +34,10 @@
    1.13      {fix x y
    1.14        let ?z = "Complex x y"
    1.15        from abs_Re_le_cmod[of ?z] have tha: "abs x \<le> cmod ?z" by auto
    1.16 -      hence "cmod ?z - x \<ge> 0" "cmod ?z + x \<ge> 0" by (cases "x \<ge> 0", arith+)
    1.17 +      hence "cmod ?z - x \<ge> 0" "cmod ?z + x \<ge> 0" by arith+ 
    1.18        hence "(sqrt (x * x + y * y) + x) / 2 \<ge> 0" "(sqrt (x * x + y * y) - x) / 2 \<ge> 0" by (simp_all add: power2_eq_square) }
    1.19      note th = this
    1.20 -    have sq4: "\<And>x::real. x^2 / 4 = (x / 2) ^ 2"
    1.21 +    have sq4: "\<And>x::real. x^2 / 4 = (x / 2) ^ 2" 
    1.22        by (simp add: power2_eq_square) 
    1.23      from th[of x y]
    1.24      have sq4': "sqrt (((sqrt (x * x + y * y) + x)^2 / 4)) = (sqrt (x * x + y * y) + x) / 2" "sqrt (((sqrt (x * x + y * y) - x)^2 / 4)) = (sqrt (x * x + y * y) - x) / 2" unfolding sq4 by simp_all
     2.1 --- a/src/HOL/Hyperreal/Deriv.thy	Mon Jul 21 13:36:44 2008 +0200
     2.2 +++ b/src/HOL/Hyperreal/Deriv.thy	Mon Jul 21 13:36:59 2008 +0200
     2.3 @@ -846,6 +846,7 @@
     2.4  lemma lemma_interval_lt:
     2.5       "[| a < x;  x < b |]
     2.6        ==> \<exists>d::real. 0 < d & (\<forall>y. \<bar>x-y\<bar> < d --> a < y & y < b)"
     2.7 +
     2.8  apply (simp add: abs_less_iff)
     2.9  apply (insert linorder_linear [of "x-a" "b-x"], safe)
    2.10  apply (rule_tac x = "x-a" in exI)
    2.11 @@ -883,7 +884,7 @@
    2.12    proof cases
    2.13      assume axb: "a < x & x < b"
    2.14          --{*@{term f} attains its maximum within the interval*}
    2.15 -    hence ax: "a<x" and xb: "x<b" by auto
    2.16 +    hence ax: "a<x" and xb: "x<b" by arith + 
    2.17      from lemma_interval [OF ax xb]
    2.18      obtain d where d: "0<d" and bound: "\<forall>y. \<bar>x-y\<bar> < d \<longrightarrow> a \<le> y \<and> y \<le> b"
    2.19        by blast
    2.20 @@ -902,7 +903,7 @@
    2.21      proof cases
    2.22        assume ax'b: "a < x' & x' < b"
    2.23          --{*@{term f} attains its minimum within the interval*}
    2.24 -      hence ax': "a<x'" and x'b: "x'<b" by auto
    2.25 +      hence ax': "a<x'" and x'b: "x'<b" by arith+ 
    2.26        from lemma_interval [OF ax' x'b]
    2.27        obtain d where d: "0<d" and bound: "\<forall>y. \<bar>x'-y\<bar> < d \<longrightarrow> a \<le> y \<and> y \<le> b"
    2.28    by blast
    2.29 @@ -1194,7 +1195,7 @@
    2.30        with e have "L \<le> y \<and> y \<le> M" by arith
    2.31        from all2 [OF this]
    2.32        obtain z where "x - d \<le> z" "z \<le> x + d" "f z = y" by blast
    2.33 -      thus "\<exists>z. \<bar>z - x\<bar> \<le> d \<and> f z = y"
    2.34 +      thus "\<exists>z. \<bar>z - x\<bar> \<le> d \<and> f z = y" 
    2.35          by (force simp add: abs_le_iff)
    2.36      qed
    2.37    qed
    2.38 @@ -1251,11 +1252,11 @@
    2.39  unfolding DERIV_iff2
    2.40  proof (rule LIM_equal2)
    2.41    show "0 < min (x - a) (b - x)"
    2.42 -    using a b by simp
    2.43 +    using a b by arith 
    2.44  next
    2.45    fix y
    2.46    assume "norm (y - x) < min (x - a) (b - x)"
    2.47 -  hence "a < y" and "y < b"
    2.48 +  hence "a < y" and "y < b" 
    2.49      by (simp_all add: abs_less_iff)
    2.50    thus "(g y - g x) / (y - x) =
    2.51          inverse ((f (g y) - x) / (g y - g x))"
     3.1 --- a/src/HOL/Library/Abstract_Rat.thy	Mon Jul 21 13:36:44 2008 +0200
     3.2 +++ b/src/HOL/Library/Abstract_Rat.thy	Mon Jul 21 13:36:59 2008 +0200
     3.3 @@ -31,6 +31,8 @@
     3.4    (let g = zgcd a b 
     3.5     in if b > 0 then (a div g, b div g) else (- (a div g), - (b div g)))))"
     3.6  
     3.7 +declare zgcd_zdvd1[presburger] 
     3.8 +declare zgcd_zdvd2[presburger]
     3.9  lemma normNum_isnormNum [simp]: "isnormNum (normNum x)"
    3.10  proof -
    3.11    have " \<exists> a b. x = (a,b)" by auto
    3.12 @@ -44,26 +46,26 @@
    3.13      let ?g' = "zgcd ?a' ?b'"
    3.14      from anz bnz have "?g \<noteq> 0" by simp  with zgcd_pos[of a b] 
    3.15      have gpos: "?g > 0"  by arith
    3.16 -    have gdvd: "?g dvd a" "?g dvd b" by (simp_all add: zgcd_zdvd1 zgcd_zdvd2)
    3.17 +    have gdvd: "?g dvd a" "?g dvd b" by arith+ 
    3.18      from zdvd_mult_div_cancel[OF gdvd(1)] zdvd_mult_div_cancel[OF gdvd(2)]
    3.19      anz bnz
    3.20      have nz':"?a' \<noteq> 0" "?b' \<noteq> 0" 
    3.21        by - (rule notI,simp add:zgcd_def)+
    3.22 -    from anz bnz have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by blast
    3.23 +    from anz bnz have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by arith 
    3.24      from div_zgcd_relprime[OF stupid] have gp1: "?g' = 1" .
    3.25      from bnz have "b < 0 \<or> b > 0" by arith
    3.26      moreover
    3.27      {assume b: "b > 0"
    3.28 -      from pos_imp_zdiv_nonneg_iff[OF gpos] b
    3.29 -      have "?b' \<ge> 0" by simp
    3.30 -      with nz' have b': "?b' > 0" by simp
    3.31 +      from b have "?b' \<ge> 0" 
    3.32 +	by (presburger add: pos_imp_zdiv_nonneg_iff[OF gpos])  
    3.33 +      with nz' have b': "?b' > 0" by arith 
    3.34        from b b' anz bnz nz' gp1 have ?thesis 
    3.35  	by (simp add: isnormNum_def normNum_def Let_def split_def fst_conv snd_conv)}
    3.36      moreover {assume b: "b < 0"
    3.37        {assume b': "?b' \<ge> 0" 
    3.38  	from gpos have th: "?g \<ge> 0" by arith
    3.39  	from mult_nonneg_nonneg[OF th b'] zdvd_mult_div_cancel[OF gdvd(2)]
    3.40 -	have False using b by simp }
    3.41 +	have False using b by arith }
    3.42        hence b': "?b' < 0" by (presburger add: linorder_not_le[symmetric]) 
    3.43        from anz bnz nz' b b' gp1 have ?thesis 
    3.44  	by (simp add: isnormNum_def normNum_def Let_def split_def fst_conv snd_conv)}
    3.45 @@ -203,16 +205,16 @@
    3.46        by (simp add: INum_def  eq_divide_eq divide_eq_eq of_int_mult[symmetric] del: of_int_mult)
    3.47      from prems have gcd1: "zgcd a b = 1" "zgcd b a = 1" "zgcd a' b' = 1" "zgcd b' a' = 1"       
    3.48        by (simp_all add: isnormNum_def add: zgcd_commute)
    3.49 -    from eq have raw_dvd: "a dvd a'*b" "b dvd b'*a" "a' dvd a*b'" "b' dvd b*a'" 
    3.50 -      apply(unfold dvd_def)
    3.51 -      apply (rule_tac x="b'" in exI, simp add: mult_ac)
    3.52 -      apply (rule_tac x="a'" in exI, simp add: mult_ac)
    3.53 -      apply (rule_tac x="b" in exI, simp add: mult_ac)
    3.54 -      apply (rule_tac x="a" in exI, simp add: mult_ac)
    3.55 +    from eq have raw_dvd: "a dvd a'*b" "b dvd b'*a" "a' dvd a*b'" "b' dvd b*a'"
    3.56 +      apply - 
    3.57 +      apply algebra
    3.58 +      apply algebra
    3.59 +      apply simp
    3.60 +      apply algebra
    3.61        done
    3.62      from zdvd_dvd_eq[OF bz zrelprime_dvd_mult[OF gcd1(2) raw_dvd(2)]
    3.63        zrelprime_dvd_mult[OF gcd1(4) raw_dvd(4)]]
    3.64 -      have eq1: "b = b'" using pos by simp_all
    3.65 +      have eq1: "b = b'" using pos by arith  
    3.66        with eq have "a = a'" using pos by simp
    3.67        with eq1 have ?rhs by simp}
    3.68    ultimately show ?rhs by blast
     4.1 --- a/src/HOL/Library/Parity.thy	Mon Jul 21 13:36:44 2008 +0200
     4.2 +++ b/src/HOL/Library/Parity.thy	Mon Jul 21 13:36:59 2008 +0200
     4.3 @@ -41,14 +41,18 @@
     4.4  
     4.5  
     4.6  subsection {* Behavior under integer arithmetic operations *}
     4.7 +declare dvd_def[algebra]
     4.8 +lemma nat_even_iff_2_dvd[algebra]: "even (x::nat) \<longleftrightarrow> 2 dvd x"
     4.9 +  by (presburger add: even_nat_def even_def)
    4.10 +lemma int_even_iff_2_dvd[algebra]: "even (x::int) \<longleftrightarrow> 2 dvd x"
    4.11 +  by presburger
    4.12  
    4.13  lemma even_times_anything: "even (x::int) ==> even (x * y)"
    4.14 -  by (simp add: even_def zmod_zmult1_eq')
    4.15 +  by algebra
    4.16  
    4.17 -lemma anything_times_even: "even (y::int) ==> even (x * y)"
    4.18 -  by (simp add: even_def zmod_zmult1_eq)
    4.19 +lemma anything_times_even: "even (y::int) ==> even (x * y)" by algebra
    4.20  
    4.21 -lemma odd_times_odd: "odd (x::int) ==> odd y ==> odd (x * y)"
    4.22 +lemma odd_times_odd: "odd (x::int) ==> odd y ==> odd (x * y)" 
    4.23    by (simp add: even_def zmod_zmult1_eq)
    4.24  
    4.25  lemma even_product[presburger]: "even((x::int) * y) = (even x | even y)"
    4.26 @@ -71,7 +75,7 @@
    4.27  lemma even_sum[presburger]: "even ((x::int) + y) = ((even x & even y) | (odd x & odd y))"
    4.28    by presburger
    4.29  
    4.30 -lemma even_neg[presburger]: "even (-(x::int)) = even x" by presburger
    4.31 +lemma even_neg[presburger, algebra]: "even (-(x::int)) = even x" by presburger
    4.32  
    4.33  lemma even_difference:
    4.34      "even ((x::int) - y) = ((even x & even y) | (odd x & odd y))" by presburger
    4.35 @@ -80,7 +84,8 @@
    4.36      "even (x::int) ==> 0 < n ==> even (x^n)"
    4.37    by (induct n) (auto simp add: even_product)
    4.38  
    4.39 -lemma odd_pow_iff[presburger]: "odd ((x::int) ^ n) \<longleftrightarrow> (n = 0 \<or> odd x)"
    4.40 +lemma odd_pow_iff[presburger, algebra]: 
    4.41 +  "odd ((x::int) ^ n) \<longleftrightarrow> (n = 0 \<or> odd x)"
    4.42    apply (induct n, simp_all)
    4.43    apply presburger
    4.44    apply (case_tac n, auto)
    4.45 @@ -120,19 +125,19 @@
    4.46  lemma pos_int_even_equiv_nat_even: "0 \<le> x ==> even x = even (nat x)"
    4.47    by (simp add: even_nat_def)
    4.48  
    4.49 -lemma even_nat_product[presburger]: "even((x::nat) * y) = (even x | even y)"
    4.50 +lemma even_nat_product[presburger, algebra]: "even((x::nat) * y) = (even x | even y)"
    4.51    by (simp add: even_nat_def int_mult)
    4.52  
    4.53 -lemma even_nat_sum[presburger]: "even ((x::nat) + y) =
    4.54 +lemma even_nat_sum[presburger, algebra]: "even ((x::nat) + y) =
    4.55      ((even x & even y) | (odd x & odd y))" by presburger
    4.56  
    4.57 -lemma even_nat_difference[presburger]:
    4.58 +lemma even_nat_difference[presburger, algebra]:
    4.59      "even ((x::nat) - y) = (x < y | (even x & even y) | (odd x & odd y))"
    4.60  by presburger
    4.61  
    4.62 -lemma even_nat_Suc[presburger]: "even (Suc x) = odd x" by presburger
    4.63 +lemma even_nat_Suc[presburger, algebra]: "even (Suc x) = odd x" by presburger
    4.64  
    4.65 -lemma even_nat_power[presburger]: "even ((x::nat)^y) = (even x & 0 < y)"
    4.66 +lemma even_nat_power[presburger, algebra]: "even ((x::nat)^y) = (even x & 0 < y)"
    4.67    by (simp add: even_nat_def int_power)
    4.68  
    4.69  lemma even_nat_zero[presburger]: "even (0::nat)" by presburger
    4.70 @@ -249,29 +254,11 @@
    4.71  
    4.72  lemma zero_less_power_eq[presburger]: "(0 < (x::'a::{recpower,ordered_idom}) ^ n) =
    4.73      (n = 0 | (even n & x ~= 0) | (odd n & 0 < x))"
    4.74 -  apply (rule iffI)
    4.75 -  apply clarsimp
    4.76 -  apply (rule conjI)
    4.77 -  apply clarsimp
    4.78 -  apply (rule ccontr)
    4.79 -  apply (subgoal_tac "~ (0 <= x^n)")
    4.80 -  apply simp
    4.81 -  apply (subst zero_le_odd_power)
    4.82 -  apply assumption
    4.83 -  apply simp
    4.84 -  apply (rule notI)
    4.85 -  apply (simp add: power_0_left)
    4.86 -  apply (rule notI)
    4.87 -  apply (simp add: power_0_left)
    4.88 -  apply auto
    4.89 -  apply (subgoal_tac "0 <= x^n")
    4.90 -  apply (frule order_le_imp_less_or_eq)
    4.91 -  apply simp
    4.92 -  apply (erule zero_le_even_power)
    4.93 -  done
    4.94 +
    4.95 +  unfolding order_less_le zero_le_power_eq by auto
    4.96  
    4.97  lemma power_less_zero_eq[presburger]: "((x::'a::{recpower,ordered_idom}) ^ n < 0) =
    4.98 -    (odd n & x < 0)" 
    4.99 +    (odd n & x < 0)"
   4.100    apply (subst linorder_not_le [symmetric])+
   4.101    apply (subst zero_le_power_eq)
   4.102    apply auto
   4.103 @@ -324,6 +311,7 @@
   4.104  lemma div_2_gt_zero [simp]: "(1::nat) < n ==> 0 < n div 2" 
   4.105  by arith
   4.106  
   4.107 +  (* Potential use of algebra : Equality modulo n*)
   4.108  lemma mod_mult_self3 [simp]: "(k*n + m) mod n = m mod (n::nat)"
   4.109  by (simp add: mult_ac add_ac)
   4.110  
   4.111 @@ -342,17 +330,11 @@
   4.112  
   4.113  subsection {* More Even/Odd Results *}
   4.114   
   4.115 -lemma even_mult_two_ex: "even(n) = (\<exists>m::nat. n = 2*m)"
   4.116 -by (simp add: even_nat_equiv_def2 numeral_2_eq_2)
   4.117 -
   4.118 -lemma odd_Suc_mult_two_ex: "odd(n) = (\<exists>m. n = Suc (2*m))"
   4.119 -by (simp add: odd_nat_equiv_def2 numeral_2_eq_2)
   4.120 +lemma even_mult_two_ex: "even(n) = (\<exists>m::nat. n = 2*m)" by presburger
   4.121 +lemma odd_Suc_mult_two_ex: "odd(n) = (\<exists>m. n = Suc (2*m))" by presburger
   4.122 +lemma even_add [simp]: "even(m + n::nat) = (even m = even n)"  by presburger
   4.123  
   4.124 -lemma even_add [simp]: "even(m + n::nat) = (even m = even n)" 
   4.125 -by auto
   4.126 -
   4.127 -lemma odd_add [simp]: "odd(m + n::nat) = (odd m \<noteq> odd n)"
   4.128 -by auto
   4.129 +lemma odd_add [simp]: "odd(m + n::nat) = (odd m \<noteq> odd n)" by presburger
   4.130  
   4.131  lemma div_Suc: "Suc a div c = a div c + Suc 0 div c +
   4.132      (a mod c + Suc 0 mod c) div c" 
   4.133 @@ -361,35 +343,18 @@
   4.134    apply (rule div_add1_eq, simp)
   4.135    done
   4.136  
   4.137 -lemma lemma_even_div2 [simp]: "even (n::nat) ==> (n + 1) div 2 = n div 2"
   4.138 -apply (simp add: numeral_2_eq_2) 
   4.139 -apply (subst div_Suc)  
   4.140 -apply (simp add: even_nat_mod_two_eq_zero) 
   4.141 -done
   4.142 +lemma lemma_even_div2 [simp]: "even (n::nat) ==> (n + 1) div 2 = n div 2" by presburger
   4.143  
   4.144  lemma lemma_not_even_div2 [simp]: "~even n ==> (n + 1) div 2 = Suc (n div 2)"
   4.145 -apply (simp add: numeral_2_eq_2) 
   4.146 -apply (subst div_Suc)  
   4.147 -apply (simp add: odd_nat_mod_two_eq_one) 
   4.148 -done
   4.149 -
   4.150 -lemma even_num_iff: "0 < n ==> even n = (~ even(n - 1 :: nat))" 
   4.151 -by (case_tac "n", auto)
   4.152 +by presburger
   4.153  
   4.154 -lemma even_even_mod_4_iff: "even (n::nat) = even (n mod 4)"
   4.155 -apply (induct n, simp)
   4.156 -apply (subst mod_Suc, simp) 
   4.157 -done
   4.158 +lemma even_num_iff: "0 < n ==> even n = (~ even(n - 1 :: nat))"  by presburger
   4.159 +lemma even_even_mod_4_iff: "even (n::nat) = even (n mod 4)" by presburger
   4.160  
   4.161 -lemma lemma_odd_mod_4_div_2: "n mod 4 = (3::nat) ==> odd((n - 1) div 2)"
   4.162 -apply (rule mod_div_equality [of n 4, THEN subst])
   4.163 -apply (simp add: even_num_iff)
   4.164 -done
   4.165 +lemma lemma_odd_mod_4_div_2: "n mod 4 = (3::nat) ==> odd((n - 1) div 2)" by presburger
   4.166  
   4.167  lemma lemma_even_mod_4_div_2: "n mod 4 = (1::nat) ==> even ((n - 1) div 2)"
   4.168 -apply (rule mod_div_equality [of n 4, THEN subst])
   4.169 -apply simp
   4.170 -done
   4.171 +  by presburger
   4.172  
   4.173  text {* Simplify, when the exponent is a numeral *}
   4.174  
   4.175 @@ -441,8 +406,7 @@
   4.176  
   4.177  subsection {* Miscellaneous *}
   4.178  
   4.179 -lemma odd_pos: "odd (n::nat) \<Longrightarrow> 0 < n"
   4.180 -  by (cases n, simp_all)
   4.181 +lemma odd_pos: "odd (n::nat) \<Longrightarrow> 0 < n" by presburger
   4.182  
   4.183  lemma [presburger]:"(x + 1) div 2 = x div 2 \<longleftrightarrow> even (x::int)" by presburger
   4.184  lemma [presburger]: "(x + 1) div 2 = x div 2 + 1 \<longleftrightarrow> odd (x::int)" by presburger
     5.1 --- a/src/HOL/Library/Pocklington.thy	Mon Jul 21 13:36:44 2008 +0200
     5.2 +++ b/src/HOL/Library/Pocklington.thy	Mon Jul 21 13:36:59 2008 +0200
     5.3 @@ -20,50 +20,13 @@
     5.4    "\<lbrakk> [a = b] (mod p); [b = c] (mod p) \<rbrakk> \<Longrightarrow> [a = c] (mod p)"
     5.5    by (simp add:modeq_def)
     5.6  
     5.7 -lemma zmod_eq_dvd_iff: "(x::int) mod n = y mod n \<longleftrightarrow> n dvd x - y"
     5.8 -proof
     5.9 -  assume H: "x mod n = y mod n"
    5.10 -  hence "x mod n - y mod n = 0" by simp
    5.11 -  hence "(x mod n - y mod n) mod n = 0" by simp 
    5.12 -  hence "(x - y) mod n = 0" by (simp add: zmod_zdiff1_eq[symmetric])
    5.13 -  thus "n dvd x - y" by (simp add: zdvd_iff_zmod_eq_0)
    5.14 -next
    5.15 -  assume H: "n dvd x - y"
    5.16 -  then obtain k where k: "x-y = n*k" unfolding dvd_def by blast
    5.17 -  hence "x = n*k + y" by simp
    5.18 -  hence "x mod n = (n*k + y) mod n" by simp
    5.19 -  thus "x mod n = y mod n" by (simp add: zmod_zadd_left_eq)
    5.20 -qed
    5.21  
    5.22  lemma nat_mod_lemma: assumes xyn: "[x = y] (mod n)" and xy:"y \<le> x"
    5.23    shows "\<exists>q. x = y + n * q"
    5.24 -proof-
    5.25 -  from xy have th: "int x - int y = int (x - y)" by presburger
    5.26 -  from xyn have "int x mod int n = int y mod int n" 
    5.27 -    by (simp add: modeq_def zmod_int[symmetric])
    5.28 -  hence "int n dvd int x - int y" by (simp only: zmod_eq_dvd_iff[symmetric]) 
    5.29 -  hence "n dvd x - y" by (simp add: th zdvd_int)
    5.30 -  then show ?thesis using xy unfolding dvd_def apply clarsimp apply (rule_tac x="k" in exI) by arith
    5.31 -qed
    5.32 +using xyn xy unfolding modeq_def using nat_mod_eq_lemma by blast
    5.33  
    5.34 -lemma nat_mod: "[x = y] (mod n) \<longleftrightarrow> (\<exists>q1 q2. x + n * q1 = y + n * q2)" 
    5.35 -  (is "?lhs = ?rhs")
    5.36 -proof
    5.37 -  assume H: "[x = y] (mod n)"
    5.38 -  {assume xy: "x \<le> y"
    5.39 -    from H have th: "[y = x] (mod n)" by (simp add: modeq_def)
    5.40 -    from nat_mod_lemma[OF th xy] have ?rhs 
    5.41 -      apply clarify  apply (rule_tac x="q" in exI) by (rule exI[where x="0"], simp)}
    5.42 -  moreover
    5.43 -  {assume xy: "y \<le> x"
    5.44 -    from nat_mod_lemma[OF H xy] have ?rhs 
    5.45 -      apply clarify  apply (rule_tac x="0" in exI) by (rule_tac x="q" in exI, simp)}
    5.46 -  ultimately  show ?rhs using linear[of x y] by blast  
    5.47 -next
    5.48 -  assume ?rhs then obtain q1 q2 where q12: "x + n * q1 = y + n * q2" by blast
    5.49 -  hence "(x + n * q1) mod n = (y + n * q2) mod n" by simp
    5.50 -  thus  ?lhs by (simp add: modeq_def)
    5.51 -qed
    5.52 +lemma nat_mod[algebra]: "[x = y] (mod n) \<longleftrightarrow> (\<exists>q1 q2. x + n * q1 = y + n * q2)" 
    5.53 +unfolding modeq_def nat_mod_eq_iff ..
    5.54  
    5.55  (* Lemmas about previously defined terms.                                    *)
    5.56  
     6.1 --- a/src/HOL/Presburger.thy	Mon Jul 21 13:36:44 2008 +0200
     6.2 +++ b/src/HOL/Presburger.thy	Mon Jul 21 13:36:59 2008 +0200
     6.3 @@ -62,7 +62,8 @@
     6.4    "\<forall>x k. F = F"
     6.5  apply (auto elim!: dvdE simp add: ring_simps)
     6.6  unfolding mult_assoc [symmetric] left_distrib [symmetric] left_diff_distrib [symmetric]
     6.7 -unfolding dvd_def mult_commute [of d] by auto
     6.8 +unfolding dvd_def mult_commute [of d] 
     6.9 +by auto
    6.10  
    6.11  subsection{* The A and B sets *}
    6.12  lemma bset:
    6.13 @@ -84,12 +85,13 @@
    6.14  proof (blast, blast)
    6.15    assume dp: "D > 0" and tB: "t - 1\<in> B"
    6.16    show "(\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x = t) \<longrightarrow> (x - D = t))" 
    6.17 -    apply (rule allI, rule impI,erule ballE[where x="1"],erule ballE[where x="t - 1"])
    6.18 -    using dp tB by simp_all
    6.19 +    apply (rule allI, rule impI,erule ballE[where x="1"],erule ballE[where x="t - 1"]) 
    6.20 +    apply algebra using dp tB by simp_all
    6.21  next
    6.22    assume dp: "D > 0" and tB: "t \<in> B"
    6.23    show "(\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x \<noteq> t) \<longrightarrow> (x - D \<noteq> t))" 
    6.24      apply (rule allI, rule impI,erule ballE[where x="D"],erule ballE[where x="t"])
    6.25 +    apply algebra
    6.26      using dp tB by simp_all
    6.27  next
    6.28    assume dp: "D > 0" thus "(\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x < t) \<longrightarrow> (x - D < t))" by arith
    6.29 @@ -113,9 +115,7 @@
    6.30    thus "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x \<ge> t) \<longrightarrow> (x - D \<ge> t)" by blast
    6.31  next
    6.32    assume d: "d dvd D"
    6.33 -  {fix x assume H: "d dvd x + t" with d have "d dvd (x - D) + t"
    6.34 -      by (auto elim!: dvdE simp add: ring_simps)
    6.35 -        (auto simp only: left_diff_distrib [symmetric] dvd_def mult_commute)}
    6.36 +  {fix x assume H: "d dvd x + t" with d have "d dvd (x - D) + t" by algebra}
    6.37    thus "\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (d dvd x+t) \<longrightarrow> (d dvd (x - D) + t)" by simp
    6.38  next
    6.39    assume d: "d dvd D"
    6.40 @@ -470,25 +470,20 @@
    6.41  end
    6.42  *} "Cooper's algorithm for Presburger arithmetic"
    6.43  
    6.44 -lemma [presburger]: "m mod 2 = (1::nat) \<longleftrightarrow> \<not> 2 dvd m " by presburger
    6.45 -lemma [presburger]: "m mod 2 = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
    6.46 -lemma [presburger]: "m mod (Suc (Suc 0)) = (1::nat) \<longleftrightarrow> \<not> 2 dvd m " by presburger
    6.47 -lemma [presburger]: "m mod (Suc (Suc 0)) = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
    6.48 -lemma [presburger]: "m mod 2 = (1::int) \<longleftrightarrow> \<not> 2 dvd m " by presburger
    6.49 +lemma [presburger, algebra]: "m mod 2 = (1::nat) \<longleftrightarrow> \<not> 2 dvd m " by presburger
    6.50 +lemma [presburger, algebra]: "m mod 2 = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
    6.51 +lemma [presburger, algebra]: "m mod (Suc (Suc 0)) = (1::nat) \<longleftrightarrow> \<not> 2 dvd m " by presburger
    6.52 +lemma [presburger, algebra]: "m mod (Suc (Suc 0)) = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
    6.53 +lemma [presburger, algebra]: "m mod 2 = (1::int) \<longleftrightarrow> \<not> 2 dvd m " by presburger
    6.54  
    6.55  
    6.56  lemma zdvd_period:
    6.57    fixes a d :: int
    6.58    assumes advdd: "a dvd d"
    6.59    shows "a dvd (x + t) \<longleftrightarrow> a dvd ((x + c * d) + t)"
    6.60 -proof-
    6.61 -  {
    6.62 -    fix x k
    6.63 -    from inf_period(3) [OF advdd, rule_format, where x=x and k="-k"]  
    6.64 -    have "a dvd (x + t) \<longleftrightarrow> a dvd (x + k * d + t)" by simp
    6.65 -  }
    6.66 -  hence "\<forall>x.\<forall>k. ((a::int) dvd (x + t)) = (a dvd (x+k*d + t))"  by simp
    6.67 -  then show ?thesis by simp
    6.68 -qed
    6.69 +  using advdd
    6.70 +  apply -
    6.71 +  apply (rule iffI)
    6.72 +  by algebra+
    6.73  
    6.74  end
     7.1 --- a/src/HOL/Real/Rational.thy	Mon Jul 21 13:36:44 2008 +0200
     7.2 +++ b/src/HOL/Real/Rational.thy	Mon Jul 21 13:36:59 2008 +0200
     7.3 @@ -163,7 +163,7 @@
     7.4    | rat_power_Suc: "q ^ Suc n = (q\<Colon>rat) * (q ^ n)"
     7.5  
     7.6  instance proof
     7.7 -  fix q r s :: rat show "(q * r) * s = q * (r * s)"
     7.8 +  fix q r s :: rat show "(q * r) * s = q * (r * s)" 
     7.9      by (cases q, cases r, cases s) (simp add: eq_rat)
    7.10  next
    7.11    fix q r :: rat show "q * r = r * q"
    7.12 @@ -356,7 +356,7 @@
    7.13      from neq have "?D' \<noteq> 0" by simp
    7.14      hence "?le a b c d = ?le (a * ?D') (b * ?D') c d"
    7.15        by (rule le_factor)
    7.16 -    also have "... = ((a * b') * ?D * ?D' * d * d' \<le> (c * d') * ?D * ?D' * b * b')"
    7.17 +    also have "... = ((a * b') * ?D * ?D' * d * d' \<le> (c * d') * ?D * ?D' * b * b')" 
    7.18        by (simp add: mult_ac)
    7.19      also have "... = ((a' * b) * ?D * ?D' * d * d' \<le> (c' * d) * ?D * ?D' * b * b')"
    7.20        by (simp only: eq1 eq2)
    7.21 @@ -396,8 +396,7 @@
    7.22              by simp
    7.23            with ff show ?thesis by (simp add: mult_le_cancel_right)
    7.24          qed
    7.25 -        also have "... = (c * f) * (d * f) * (b * b)"
    7.26 -          by (simp only: mult_ac)
    7.27 +        also have "... = (c * f) * (d * f) * (b * b)" by algebra
    7.28          also have "... \<le> (e * d) * (d * f) * (b * b)"
    7.29          proof -
    7.30            from neq 2 have "(c * f) * (d * f) \<le> (e * d) * (d * f)"
     8.1 --- a/src/HOL/Real/RealDef.thy	Mon Jul 21 13:36:44 2008 +0200
     8.2 +++ b/src/HOL/Real/RealDef.thy	Mon Jul 21 13:36:59 2008 +0200
     8.3 @@ -376,7 +376,7 @@
     8.4  lemma real_add_left_mono: 
     8.5    assumes le: "x \<le> y" shows "z + x \<le> z + (y::real)"
     8.6  proof -
     8.7 -  have "z + x - (z + y) = (z + -z) + (x - y)"
     8.8 +  have "z + x - (z + y) = (z + -z) + (x - y)" 
     8.9      by (simp add: diff_minus add_ac) 
    8.10    with le show ?thesis 
    8.11      by (simp add: real_le_eq_diff[of x] real_le_eq_diff[of "z+x"] diff_minus)
    8.12 @@ -604,28 +604,28 @@
    8.13    apply (rule of_int_setprod)
    8.14  done
    8.15  
    8.16 -lemma real_of_int_zero_cancel [simp]: "(real x = 0) = (x = (0::int))"
    8.17 +lemma real_of_int_zero_cancel [simp, algebra, presburger]: "(real x = 0) = (x = (0::int))"
    8.18  by (simp add: real_of_int_def) 
    8.19  
    8.20 -lemma real_of_int_inject [iff]: "(real (x::int) = real y) = (x = y)"
    8.21 +lemma real_of_int_inject [iff, algebra, presburger]: "(real (x::int) = real y) = (x = y)"
    8.22  by (simp add: real_of_int_def) 
    8.23  
    8.24 -lemma real_of_int_less_iff [iff]: "(real (x::int) < real y) = (x < y)"
    8.25 +lemma real_of_int_less_iff [iff, presburger]: "(real (x::int) < real y) = (x < y)"
    8.26  by (simp add: real_of_int_def) 
    8.27  
    8.28 -lemma real_of_int_le_iff [simp]: "(real (x::int) \<le> real y) = (x \<le> y)"
    8.29 +lemma real_of_int_le_iff [simp, presburger]: "(real (x::int) \<le> real y) = (x \<le> y)"
    8.30  by (simp add: real_of_int_def) 
    8.31  
    8.32 -lemma real_of_int_gt_zero_cancel_iff [simp]: "(0 < real (n::int)) = (0 < n)"
    8.33 +lemma real_of_int_gt_zero_cancel_iff [simp, presburger]: "(0 < real (n::int)) = (0 < n)"
    8.34  by (simp add: real_of_int_def) 
    8.35  
    8.36 -lemma real_of_int_ge_zero_cancel_iff [simp]: "(0 <= real (n::int)) = (0 <= n)"
    8.37 +lemma real_of_int_ge_zero_cancel_iff [simp, presburger]: "(0 <= real (n::int)) = (0 <= n)"
    8.38  by (simp add: real_of_int_def) 
    8.39  
    8.40 -lemma real_of_int_lt_zero_cancel_iff [simp]: "(real (n::int) < 0) = (n < 0)"
    8.41 +lemma real_of_int_lt_zero_cancel_iff [simp, presburger]: "(real (n::int) < 0) = (n < 0)" 
    8.42  by (simp add: real_of_int_def)
    8.43  
    8.44 -lemma real_of_int_le_zero_cancel_iff [simp]: "(real (n::int) <= 0) = (n <= 0)"
    8.45 +lemma real_of_int_le_zero_cancel_iff [simp, presburger]: "(real (n::int) <= 0) = (n <= 0)"
    8.46  by (simp add: real_of_int_def)
    8.47  
    8.48  lemma real_of_int_abs [simp]: "real (abs x) = abs(real (x::int))"