--- a/src/HOL/Complex/Fundamental_Theorem_Algebra.thy Mon Jul 21 13:36:44 2008 +0200
+++ b/src/HOL/Complex/Fundamental_Theorem_Algebra.thy Mon Jul 21 13:36:59 2008 +0200
@@ -17,7 +17,7 @@
else Complex (sqrt((cmod z + Re z) /2))
((Im z / abs(Im z)) * sqrt((cmod z - Re z) /2)))"
-lemma csqrt: "csqrt z ^ 2 = z"
+lemma csqrt[algebra]: "csqrt z ^ 2 = z"
proof-
obtain x y where xy: "z = Complex x y" by (cases z, simp_all)
{assume y0: "y = 0"
@@ -34,10 +34,10 @@
{fix x y
let ?z = "Complex x y"
from abs_Re_le_cmod[of ?z] have tha: "abs x \<le> cmod ?z" by auto
- hence "cmod ?z - x \<ge> 0" "cmod ?z + x \<ge> 0" by (cases "x \<ge> 0", arith+)
+ hence "cmod ?z - x \<ge> 0" "cmod ?z + x \<ge> 0" by arith+
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) }
note th = this
- have sq4: "\<And>x::real. x^2 / 4 = (x / 2) ^ 2"
+ have sq4: "\<And>x::real. x^2 / 4 = (x / 2) ^ 2"
by (simp add: power2_eq_square)
from th[of x y]
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
--- a/src/HOL/Hyperreal/Deriv.thy Mon Jul 21 13:36:44 2008 +0200
+++ b/src/HOL/Hyperreal/Deriv.thy Mon Jul 21 13:36:59 2008 +0200
@@ -846,6 +846,7 @@
lemma lemma_interval_lt:
"[| a < x; x < b |]
==> \<exists>d::real. 0 < d & (\<forall>y. \<bar>x-y\<bar> < d --> a < y & y < b)"
+
apply (simp add: abs_less_iff)
apply (insert linorder_linear [of "x-a" "b-x"], safe)
apply (rule_tac x = "x-a" in exI)
@@ -883,7 +884,7 @@
proof cases
assume axb: "a < x & x < b"
--{*@{term f} attains its maximum within the interval*}
- hence ax: "a<x" and xb: "x<b" by auto
+ hence ax: "a<x" and xb: "x<b" by arith +
from lemma_interval [OF ax xb]
obtain d where d: "0<d" and bound: "\<forall>y. \<bar>x-y\<bar> < d \<longrightarrow> a \<le> y \<and> y \<le> b"
by blast
@@ -902,7 +903,7 @@
proof cases
assume ax'b: "a < x' & x' < b"
--{*@{term f} attains its minimum within the interval*}
- hence ax': "a<x'" and x'b: "x'<b" by auto
+ hence ax': "a<x'" and x'b: "x'<b" by arith+
from lemma_interval [OF ax' x'b]
obtain d where d: "0<d" and bound: "\<forall>y. \<bar>x'-y\<bar> < d \<longrightarrow> a \<le> y \<and> y \<le> b"
by blast
@@ -1194,7 +1195,7 @@
with e have "L \<le> y \<and> y \<le> M" by arith
from all2 [OF this]
obtain z where "x - d \<le> z" "z \<le> x + d" "f z = y" by blast
- thus "\<exists>z. \<bar>z - x\<bar> \<le> d \<and> f z = y"
+ thus "\<exists>z. \<bar>z - x\<bar> \<le> d \<and> f z = y"
by (force simp add: abs_le_iff)
qed
qed
@@ -1251,11 +1252,11 @@
unfolding DERIV_iff2
proof (rule LIM_equal2)
show "0 < min (x - a) (b - x)"
- using a b by simp
+ using a b by arith
next
fix y
assume "norm (y - x) < min (x - a) (b - x)"
- hence "a < y" and "y < b"
+ hence "a < y" and "y < b"
by (simp_all add: abs_less_iff)
thus "(g y - g x) / (y - x) =
inverse ((f (g y) - x) / (g y - g x))"
--- a/src/HOL/Library/Abstract_Rat.thy Mon Jul 21 13:36:44 2008 +0200
+++ b/src/HOL/Library/Abstract_Rat.thy Mon Jul 21 13:36:59 2008 +0200
@@ -31,6 +31,8 @@
(let g = zgcd a b
in if b > 0 then (a div g, b div g) else (- (a div g), - (b div g)))))"
+declare zgcd_zdvd1[presburger]
+declare zgcd_zdvd2[presburger]
lemma normNum_isnormNum [simp]: "isnormNum (normNum x)"
proof -
have " \<exists> a b. x = (a,b)" by auto
@@ -44,26 +46,26 @@
let ?g' = "zgcd ?a' ?b'"
from anz bnz have "?g \<noteq> 0" by simp with zgcd_pos[of a b]
have gpos: "?g > 0" by arith
- have gdvd: "?g dvd a" "?g dvd b" by (simp_all add: zgcd_zdvd1 zgcd_zdvd2)
+ have gdvd: "?g dvd a" "?g dvd b" by arith+
from zdvd_mult_div_cancel[OF gdvd(1)] zdvd_mult_div_cancel[OF gdvd(2)]
anz bnz
have nz':"?a' \<noteq> 0" "?b' \<noteq> 0"
by - (rule notI,simp add:zgcd_def)+
- from anz bnz have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by blast
+ from anz bnz have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by arith
from div_zgcd_relprime[OF stupid] have gp1: "?g' = 1" .
from bnz have "b < 0 \<or> b > 0" by arith
moreover
{assume b: "b > 0"
- from pos_imp_zdiv_nonneg_iff[OF gpos] b
- have "?b' \<ge> 0" by simp
- with nz' have b': "?b' > 0" by simp
+ from b have "?b' \<ge> 0"
+ by (presburger add: pos_imp_zdiv_nonneg_iff[OF gpos])
+ with nz' have b': "?b' > 0" by arith
from b b' anz bnz nz' gp1 have ?thesis
by (simp add: isnormNum_def normNum_def Let_def split_def fst_conv snd_conv)}
moreover {assume b: "b < 0"
{assume b': "?b' \<ge> 0"
from gpos have th: "?g \<ge> 0" by arith
from mult_nonneg_nonneg[OF th b'] zdvd_mult_div_cancel[OF gdvd(2)]
- have False using b by simp }
+ have False using b by arith }
hence b': "?b' < 0" by (presburger add: linorder_not_le[symmetric])
from anz bnz nz' b b' gp1 have ?thesis
by (simp add: isnormNum_def normNum_def Let_def split_def fst_conv snd_conv)}
@@ -203,16 +205,16 @@
by (simp add: INum_def eq_divide_eq divide_eq_eq of_int_mult[symmetric] del: of_int_mult)
from prems have gcd1: "zgcd a b = 1" "zgcd b a = 1" "zgcd a' b' = 1" "zgcd b' a' = 1"
by (simp_all add: isnormNum_def add: zgcd_commute)
- from eq have raw_dvd: "a dvd a'*b" "b dvd b'*a" "a' dvd a*b'" "b' dvd b*a'"
- apply(unfold dvd_def)
- apply (rule_tac x="b'" in exI, simp add: mult_ac)
- apply (rule_tac x="a'" in exI, simp add: mult_ac)
- apply (rule_tac x="b" in exI, simp add: mult_ac)
- apply (rule_tac x="a" in exI, simp add: mult_ac)
+ from eq have raw_dvd: "a dvd a'*b" "b dvd b'*a" "a' dvd a*b'" "b' dvd b*a'"
+ apply -
+ apply algebra
+ apply algebra
+ apply simp
+ apply algebra
done
from zdvd_dvd_eq[OF bz zrelprime_dvd_mult[OF gcd1(2) raw_dvd(2)]
zrelprime_dvd_mult[OF gcd1(4) raw_dvd(4)]]
- have eq1: "b = b'" using pos by simp_all
+ have eq1: "b = b'" using pos by arith
with eq have "a = a'" using pos by simp
with eq1 have ?rhs by simp}
ultimately show ?rhs by blast
--- a/src/HOL/Library/Parity.thy Mon Jul 21 13:36:44 2008 +0200
+++ b/src/HOL/Library/Parity.thy Mon Jul 21 13:36:59 2008 +0200
@@ -41,14 +41,18 @@
subsection {* Behavior under integer arithmetic operations *}
+declare dvd_def[algebra]
+lemma nat_even_iff_2_dvd[algebra]: "even (x::nat) \<longleftrightarrow> 2 dvd x"
+ by (presburger add: even_nat_def even_def)
+lemma int_even_iff_2_dvd[algebra]: "even (x::int) \<longleftrightarrow> 2 dvd x"
+ by presburger
lemma even_times_anything: "even (x::int) ==> even (x * y)"
- by (simp add: even_def zmod_zmult1_eq')
+ by algebra
-lemma anything_times_even: "even (y::int) ==> even (x * y)"
- by (simp add: even_def zmod_zmult1_eq)
+lemma anything_times_even: "even (y::int) ==> even (x * y)" by algebra
-lemma odd_times_odd: "odd (x::int) ==> odd y ==> odd (x * y)"
+lemma odd_times_odd: "odd (x::int) ==> odd y ==> odd (x * y)"
by (simp add: even_def zmod_zmult1_eq)
lemma even_product[presburger]: "even((x::int) * y) = (even x | even y)"
@@ -71,7 +75,7 @@
lemma even_sum[presburger]: "even ((x::int) + y) = ((even x & even y) | (odd x & odd y))"
by presburger
-lemma even_neg[presburger]: "even (-(x::int)) = even x" by presburger
+lemma even_neg[presburger, algebra]: "even (-(x::int)) = even x" by presburger
lemma even_difference:
"even ((x::int) - y) = ((even x & even y) | (odd x & odd y))" by presburger
@@ -80,7 +84,8 @@
"even (x::int) ==> 0 < n ==> even (x^n)"
by (induct n) (auto simp add: even_product)
-lemma odd_pow_iff[presburger]: "odd ((x::int) ^ n) \<longleftrightarrow> (n = 0 \<or> odd x)"
+lemma odd_pow_iff[presburger, algebra]:
+ "odd ((x::int) ^ n) \<longleftrightarrow> (n = 0 \<or> odd x)"
apply (induct n, simp_all)
apply presburger
apply (case_tac n, auto)
@@ -120,19 +125,19 @@
lemma pos_int_even_equiv_nat_even: "0 \<le> x ==> even x = even (nat x)"
by (simp add: even_nat_def)
-lemma even_nat_product[presburger]: "even((x::nat) * y) = (even x | even y)"
+lemma even_nat_product[presburger, algebra]: "even((x::nat) * y) = (even x | even y)"
by (simp add: even_nat_def int_mult)
-lemma even_nat_sum[presburger]: "even ((x::nat) + y) =
+lemma even_nat_sum[presburger, algebra]: "even ((x::nat) + y) =
((even x & even y) | (odd x & odd y))" by presburger
-lemma even_nat_difference[presburger]:
+lemma even_nat_difference[presburger, algebra]:
"even ((x::nat) - y) = (x < y | (even x & even y) | (odd x & odd y))"
by presburger
-lemma even_nat_Suc[presburger]: "even (Suc x) = odd x" by presburger
+lemma even_nat_Suc[presburger, algebra]: "even (Suc x) = odd x" by presburger
-lemma even_nat_power[presburger]: "even ((x::nat)^y) = (even x & 0 < y)"
+lemma even_nat_power[presburger, algebra]: "even ((x::nat)^y) = (even x & 0 < y)"
by (simp add: even_nat_def int_power)
lemma even_nat_zero[presburger]: "even (0::nat)" by presburger
@@ -249,29 +254,11 @@
lemma zero_less_power_eq[presburger]: "(0 < (x::'a::{recpower,ordered_idom}) ^ n) =
(n = 0 | (even n & x ~= 0) | (odd n & 0 < x))"
- apply (rule iffI)
- apply clarsimp
- apply (rule conjI)
- apply clarsimp
- apply (rule ccontr)
- apply (subgoal_tac "~ (0 <= x^n)")
- apply simp
- apply (subst zero_le_odd_power)
- apply assumption
- apply simp
- apply (rule notI)
- apply (simp add: power_0_left)
- apply (rule notI)
- apply (simp add: power_0_left)
- apply auto
- apply (subgoal_tac "0 <= x^n")
- apply (frule order_le_imp_less_or_eq)
- apply simp
- apply (erule zero_le_even_power)
- done
+
+ unfolding order_less_le zero_le_power_eq by auto
lemma power_less_zero_eq[presburger]: "((x::'a::{recpower,ordered_idom}) ^ n < 0) =
- (odd n & x < 0)"
+ (odd n & x < 0)"
apply (subst linorder_not_le [symmetric])+
apply (subst zero_le_power_eq)
apply auto
@@ -324,6 +311,7 @@
lemma div_2_gt_zero [simp]: "(1::nat) < n ==> 0 < n div 2"
by arith
+ (* Potential use of algebra : Equality modulo n*)
lemma mod_mult_self3 [simp]: "(k*n + m) mod n = m mod (n::nat)"
by (simp add: mult_ac add_ac)
@@ -342,17 +330,11 @@
subsection {* More Even/Odd Results *}
-lemma even_mult_two_ex: "even(n) = (\<exists>m::nat. n = 2*m)"
-by (simp add: even_nat_equiv_def2 numeral_2_eq_2)
-
-lemma odd_Suc_mult_two_ex: "odd(n) = (\<exists>m. n = Suc (2*m))"
-by (simp add: odd_nat_equiv_def2 numeral_2_eq_2)
+lemma even_mult_two_ex: "even(n) = (\<exists>m::nat. n = 2*m)" by presburger
+lemma odd_Suc_mult_two_ex: "odd(n) = (\<exists>m. n = Suc (2*m))" by presburger
+lemma even_add [simp]: "even(m + n::nat) = (even m = even n)" by presburger
-lemma even_add [simp]: "even(m + n::nat) = (even m = even n)"
-by auto
-
-lemma odd_add [simp]: "odd(m + n::nat) = (odd m \<noteq> odd n)"
-by auto
+lemma odd_add [simp]: "odd(m + n::nat) = (odd m \<noteq> odd n)" by presburger
lemma div_Suc: "Suc a div c = a div c + Suc 0 div c +
(a mod c + Suc 0 mod c) div c"
@@ -361,35 +343,18 @@
apply (rule div_add1_eq, simp)
done
-lemma lemma_even_div2 [simp]: "even (n::nat) ==> (n + 1) div 2 = n div 2"
-apply (simp add: numeral_2_eq_2)
-apply (subst div_Suc)
-apply (simp add: even_nat_mod_two_eq_zero)
-done
+lemma lemma_even_div2 [simp]: "even (n::nat) ==> (n + 1) div 2 = n div 2" by presburger
lemma lemma_not_even_div2 [simp]: "~even n ==> (n + 1) div 2 = Suc (n div 2)"
-apply (simp add: numeral_2_eq_2)
-apply (subst div_Suc)
-apply (simp add: odd_nat_mod_two_eq_one)
-done
-
-lemma even_num_iff: "0 < n ==> even n = (~ even(n - 1 :: nat))"
-by (case_tac "n", auto)
+by presburger
-lemma even_even_mod_4_iff: "even (n::nat) = even (n mod 4)"
-apply (induct n, simp)
-apply (subst mod_Suc, simp)
-done
+lemma even_num_iff: "0 < n ==> even n = (~ even(n - 1 :: nat))" by presburger
+lemma even_even_mod_4_iff: "even (n::nat) = even (n mod 4)" by presburger
-lemma lemma_odd_mod_4_div_2: "n mod 4 = (3::nat) ==> odd((n - 1) div 2)"
-apply (rule mod_div_equality [of n 4, THEN subst])
-apply (simp add: even_num_iff)
-done
+lemma lemma_odd_mod_4_div_2: "n mod 4 = (3::nat) ==> odd((n - 1) div 2)" by presburger
lemma lemma_even_mod_4_div_2: "n mod 4 = (1::nat) ==> even ((n - 1) div 2)"
-apply (rule mod_div_equality [of n 4, THEN subst])
-apply simp
-done
+ by presburger
text {* Simplify, when the exponent is a numeral *}
@@ -441,8 +406,7 @@
subsection {* Miscellaneous *}
-lemma odd_pos: "odd (n::nat) \<Longrightarrow> 0 < n"
- by (cases n, simp_all)
+lemma odd_pos: "odd (n::nat) \<Longrightarrow> 0 < n" by presburger
lemma [presburger]:"(x + 1) div 2 = x div 2 \<longleftrightarrow> even (x::int)" by presburger
lemma [presburger]: "(x + 1) div 2 = x div 2 + 1 \<longleftrightarrow> odd (x::int)" by presburger
--- a/src/HOL/Library/Pocklington.thy Mon Jul 21 13:36:44 2008 +0200
+++ b/src/HOL/Library/Pocklington.thy Mon Jul 21 13:36:59 2008 +0200
@@ -20,50 +20,13 @@
"\<lbrakk> [a = b] (mod p); [b = c] (mod p) \<rbrakk> \<Longrightarrow> [a = c] (mod p)"
by (simp add:modeq_def)
-lemma zmod_eq_dvd_iff: "(x::int) mod n = y mod n \<longleftrightarrow> n dvd x - y"
-proof
- assume H: "x mod n = y mod n"
- hence "x mod n - y mod n = 0" by simp
- hence "(x mod n - y mod n) mod n = 0" by simp
- hence "(x - y) mod n = 0" by (simp add: zmod_zdiff1_eq[symmetric])
- thus "n dvd x - y" by (simp add: zdvd_iff_zmod_eq_0)
-next
- assume H: "n dvd x - y"
- then obtain k where k: "x-y = n*k" unfolding dvd_def by blast
- hence "x = n*k + y" by simp
- hence "x mod n = (n*k + y) mod n" by simp
- thus "x mod n = y mod n" by (simp add: zmod_zadd_left_eq)
-qed
lemma nat_mod_lemma: assumes xyn: "[x = y] (mod n)" and xy:"y \<le> x"
shows "\<exists>q. x = y + n * q"
-proof-
- from xy have th: "int x - int y = int (x - y)" by presburger
- from xyn have "int x mod int n = int y mod int n"
- by (simp add: modeq_def zmod_int[symmetric])
- hence "int n dvd int x - int y" by (simp only: zmod_eq_dvd_iff[symmetric])
- hence "n dvd x - y" by (simp add: th zdvd_int)
- then show ?thesis using xy unfolding dvd_def apply clarsimp apply (rule_tac x="k" in exI) by arith
-qed
+using xyn xy unfolding modeq_def using nat_mod_eq_lemma by blast
-lemma nat_mod: "[x = y] (mod n) \<longleftrightarrow> (\<exists>q1 q2. x + n * q1 = y + n * q2)"
- (is "?lhs = ?rhs")
-proof
- assume H: "[x = y] (mod n)"
- {assume xy: "x \<le> y"
- from H have th: "[y = x] (mod n)" by (simp add: modeq_def)
- from nat_mod_lemma[OF th xy] have ?rhs
- apply clarify apply (rule_tac x="q" in exI) by (rule exI[where x="0"], simp)}
- moreover
- {assume xy: "y \<le> x"
- from nat_mod_lemma[OF H xy] have ?rhs
- apply clarify apply (rule_tac x="0" in exI) by (rule_tac x="q" in exI, simp)}
- ultimately show ?rhs using linear[of x y] by blast
-next
- assume ?rhs then obtain q1 q2 where q12: "x + n * q1 = y + n * q2" by blast
- hence "(x + n * q1) mod n = (y + n * q2) mod n" by simp
- thus ?lhs by (simp add: modeq_def)
-qed
+lemma nat_mod[algebra]: "[x = y] (mod n) \<longleftrightarrow> (\<exists>q1 q2. x + n * q1 = y + n * q2)"
+unfolding modeq_def nat_mod_eq_iff ..
(* Lemmas about previously defined terms. *)
--- a/src/HOL/Presburger.thy Mon Jul 21 13:36:44 2008 +0200
+++ b/src/HOL/Presburger.thy Mon Jul 21 13:36:59 2008 +0200
@@ -62,7 +62,8 @@
"\<forall>x k. F = F"
apply (auto elim!: dvdE simp add: ring_simps)
unfolding mult_assoc [symmetric] left_distrib [symmetric] left_diff_distrib [symmetric]
-unfolding dvd_def mult_commute [of d] by auto
+unfolding dvd_def mult_commute [of d]
+by auto
subsection{* The A and B sets *}
lemma bset:
@@ -84,12 +85,13 @@
proof (blast, blast)
assume dp: "D > 0" and tB: "t - 1\<in> B"
show "(\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x = t) \<longrightarrow> (x - D = t))"
- apply (rule allI, rule impI,erule ballE[where x="1"],erule ballE[where x="t - 1"])
- using dp tB by simp_all
+ apply (rule allI, rule impI,erule ballE[where x="1"],erule ballE[where x="t - 1"])
+ apply algebra using dp tB by simp_all
next
assume dp: "D > 0" and tB: "t \<in> B"
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))"
apply (rule allI, rule impI,erule ballE[where x="D"],erule ballE[where x="t"])
+ apply algebra
using dp tB by simp_all
next
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
@@ -113,9 +115,7 @@
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
next
assume d: "d dvd D"
- {fix x assume H: "d dvd x + t" with d have "d dvd (x - D) + t"
- by (auto elim!: dvdE simp add: ring_simps)
- (auto simp only: left_diff_distrib [symmetric] dvd_def mult_commute)}
+ {fix x assume H: "d dvd x + t" with d have "d dvd (x - D) + t" by algebra}
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
next
assume d: "d dvd D"
@@ -470,25 +470,20 @@
end
*} "Cooper's algorithm for Presburger arithmetic"
-lemma [presburger]: "m mod 2 = (1::nat) \<longleftrightarrow> \<not> 2 dvd m " by presburger
-lemma [presburger]: "m mod 2 = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
-lemma [presburger]: "m mod (Suc (Suc 0)) = (1::nat) \<longleftrightarrow> \<not> 2 dvd m " by presburger
-lemma [presburger]: "m mod (Suc (Suc 0)) = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
-lemma [presburger]: "m mod 2 = (1::int) \<longleftrightarrow> \<not> 2 dvd m " by presburger
+lemma [presburger, algebra]: "m mod 2 = (1::nat) \<longleftrightarrow> \<not> 2 dvd m " by presburger
+lemma [presburger, algebra]: "m mod 2 = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
+lemma [presburger, algebra]: "m mod (Suc (Suc 0)) = (1::nat) \<longleftrightarrow> \<not> 2 dvd m " by presburger
+lemma [presburger, algebra]: "m mod (Suc (Suc 0)) = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
+lemma [presburger, algebra]: "m mod 2 = (1::int) \<longleftrightarrow> \<not> 2 dvd m " by presburger
lemma zdvd_period:
fixes a d :: int
assumes advdd: "a dvd d"
shows "a dvd (x + t) \<longleftrightarrow> a dvd ((x + c * d) + t)"
-proof-
- {
- fix x k
- from inf_period(3) [OF advdd, rule_format, where x=x and k="-k"]
- have "a dvd (x + t) \<longleftrightarrow> a dvd (x + k * d + t)" by simp
- }
- hence "\<forall>x.\<forall>k. ((a::int) dvd (x + t)) = (a dvd (x+k*d + t))" by simp
- then show ?thesis by simp
-qed
+ using advdd
+ apply -
+ apply (rule iffI)
+ by algebra+
end
--- a/src/HOL/Real/Rational.thy Mon Jul 21 13:36:44 2008 +0200
+++ b/src/HOL/Real/Rational.thy Mon Jul 21 13:36:59 2008 +0200
@@ -163,7 +163,7 @@
| rat_power_Suc: "q ^ Suc n = (q\<Colon>rat) * (q ^ n)"
instance proof
- fix q r s :: rat show "(q * r) * s = q * (r * s)"
+ fix q r s :: rat show "(q * r) * s = q * (r * s)"
by (cases q, cases r, cases s) (simp add: eq_rat)
next
fix q r :: rat show "q * r = r * q"
@@ -356,7 +356,7 @@
from neq have "?D' \<noteq> 0" by simp
hence "?le a b c d = ?le (a * ?D') (b * ?D') c d"
by (rule le_factor)
- also have "... = ((a * b') * ?D * ?D' * d * d' \<le> (c * d') * ?D * ?D' * b * b')"
+ also have "... = ((a * b') * ?D * ?D' * d * d' \<le> (c * d') * ?D * ?D' * b * b')"
by (simp add: mult_ac)
also have "... = ((a' * b) * ?D * ?D' * d * d' \<le> (c' * d) * ?D * ?D' * b * b')"
by (simp only: eq1 eq2)
@@ -396,8 +396,7 @@
by simp
with ff show ?thesis by (simp add: mult_le_cancel_right)
qed
- also have "... = (c * f) * (d * f) * (b * b)"
- by (simp only: mult_ac)
+ also have "... = (c * f) * (d * f) * (b * b)" by algebra
also have "... \<le> (e * d) * (d * f) * (b * b)"
proof -
from neq 2 have "(c * f) * (d * f) \<le> (e * d) * (d * f)"
--- a/src/HOL/Real/RealDef.thy Mon Jul 21 13:36:44 2008 +0200
+++ b/src/HOL/Real/RealDef.thy Mon Jul 21 13:36:59 2008 +0200
@@ -376,7 +376,7 @@
lemma real_add_left_mono:
assumes le: "x \<le> y" shows "z + x \<le> z + (y::real)"
proof -
- have "z + x - (z + y) = (z + -z) + (x - y)"
+ have "z + x - (z + y) = (z + -z) + (x - y)"
by (simp add: diff_minus add_ac)
with le show ?thesis
by (simp add: real_le_eq_diff[of x] real_le_eq_diff[of "z+x"] diff_minus)
@@ -604,28 +604,28 @@
apply (rule of_int_setprod)
done
-lemma real_of_int_zero_cancel [simp]: "(real x = 0) = (x = (0::int))"
+lemma real_of_int_zero_cancel [simp, algebra, presburger]: "(real x = 0) = (x = (0::int))"
by (simp add: real_of_int_def)
-lemma real_of_int_inject [iff]: "(real (x::int) = real y) = (x = y)"
+lemma real_of_int_inject [iff, algebra, presburger]: "(real (x::int) = real y) = (x = y)"
by (simp add: real_of_int_def)
-lemma real_of_int_less_iff [iff]: "(real (x::int) < real y) = (x < y)"
+lemma real_of_int_less_iff [iff, presburger]: "(real (x::int) < real y) = (x < y)"
by (simp add: real_of_int_def)
-lemma real_of_int_le_iff [simp]: "(real (x::int) \<le> real y) = (x \<le> y)"
+lemma real_of_int_le_iff [simp, presburger]: "(real (x::int) \<le> real y) = (x \<le> y)"
by (simp add: real_of_int_def)
-lemma real_of_int_gt_zero_cancel_iff [simp]: "(0 < real (n::int)) = (0 < n)"
+lemma real_of_int_gt_zero_cancel_iff [simp, presburger]: "(0 < real (n::int)) = (0 < n)"
by (simp add: real_of_int_def)
-lemma real_of_int_ge_zero_cancel_iff [simp]: "(0 <= real (n::int)) = (0 <= n)"
+lemma real_of_int_ge_zero_cancel_iff [simp, presburger]: "(0 <= real (n::int)) = (0 <= n)"
by (simp add: real_of_int_def)
-lemma real_of_int_lt_zero_cancel_iff [simp]: "(real (n::int) < 0) = (n < 0)"
+lemma real_of_int_lt_zero_cancel_iff [simp, presburger]: "(real (n::int) < 0) = (n < 0)"
by (simp add: real_of_int_def)
-lemma real_of_int_le_zero_cancel_iff [simp]: "(real (n::int) <= 0) = (n <= 0)"
+lemma real_of_int_le_zero_cancel_iff [simp, presburger]: "(real (n::int) <= 0) = (n <= 0)"
by (simp add: real_of_int_def)
lemma real_of_int_abs [simp]: "real (abs x) = abs(real (x::int))"