--- a/src/HOL/Algebra/IntRing.thy Fri Jan 30 17:47:34 2009 +0100
+++ b/src/HOL/Algebra/IntRing.thy Sat Jan 31 09:04:42 2009 +0100
@@ -265,6 +265,7 @@
apply fast
done
+
lemma prime_primeideal:
assumes prime: "prime (nat p)"
shows "primeideal (Idl\<^bsub>\<Z>\<^esub> {p}) \<Z>"
@@ -293,17 +294,7 @@
assume "a * b = x * p"
hence "p dvd a * b" by simp
- hence "nat p dvd nat (abs (a * b))"
- apply (subst nat_dvd_iff, clarsimp)
- apply (rule conjI, clarsimp, simp add: zabs_def)
- proof (clarsimp)
- assume a: " ~ 0 <= p"
- from prime
- have "0 < p" by (simp add: prime_def)
- from a and this
- have "False" by simp
- thus "nat (abs (a * b)) = 0" ..
- qed
+ hence "nat p dvd nat (abs (a * b))" using ppos by (simp add: nat_dvd_iff)
hence "nat p dvd (nat (abs a) * nat (abs b))" by (simp add: nat_abs_mult_distrib)
hence "nat p dvd nat (abs a) | nat p dvd nat (abs b)" by (rule prime_dvd_mult[OF prime])
hence "p dvd a | p dvd b" by (fast intro: unnat)
--- a/src/HOL/GCD.thy Fri Jan 30 17:47:34 2009 +0100
+++ b/src/HOL/GCD.thy Sat Jan 31 09:04:42 2009 +0100
@@ -562,25 +562,25 @@
"zgcd i j = int (gcd (nat (abs i)) (nat (abs j)))"
lemma zgcd_zdvd1 [iff,simp, algebra]: "zgcd i j dvd i"
- by (simp add: zgcd_def int_dvd_iff)
+by (simp add: zgcd_def int_dvd_iff)
lemma zgcd_zdvd2 [iff,simp, algebra]: "zgcd i j dvd j"
- by (simp add: zgcd_def int_dvd_iff)
+by (simp add: zgcd_def int_dvd_iff)
lemma zgcd_pos: "zgcd i j \<ge> 0"
- by (simp add: zgcd_def)
+by (simp add: zgcd_def)
lemma zgcd0 [simp,algebra]: "(zgcd i j = 0) = (i = 0 \<and> j = 0)"
- by (simp add: zgcd_def gcd_zero) arith
+by (simp add: zgcd_def gcd_zero)
lemma zgcd_commute: "zgcd i j = zgcd j i"
- unfolding zgcd_def by (simp add: gcd_commute)
+unfolding zgcd_def by (simp add: gcd_commute)
lemma zgcd_zminus [simp, algebra]: "zgcd (- i) j = zgcd i j"
- unfolding zgcd_def by simp
+unfolding zgcd_def by simp
lemma zgcd_zminus2 [simp, algebra]: "zgcd i (- j) = zgcd i j"
- unfolding zgcd_def by simp
+unfolding zgcd_def by simp
(* should be solved by algebra*)
lemma zrelprime_dvd_mult: "zgcd i j = 1 \<Longrightarrow> i dvd k * j \<Longrightarrow> i dvd k"
--- a/src/HOL/Int.thy Fri Jan 30 17:47:34 2009 +0100
+++ b/src/HOL/Int.thy Sat Jan 31 09:04:42 2009 +0100
@@ -442,9 +442,12 @@
lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < of_nat m)"
apply (cases w)
-apply (simp add: nat le int_def Zero_int_def linorder_not_le [symmetric], arith)
+apply (simp add: nat le int_def Zero_int_def linorder_not_le[symmetric], arith)
done
+lemma nat_0_iff[simp]: "nat(i::int) = 0 \<longleftrightarrow> i\<le>0"
+by(simp add: nat_eq_iff) arith
+
lemma int_eq_iff: "(of_nat m = z) = (m = nat z & 0 \<le> z)"
by (auto simp add: nat_eq_iff2)
--- a/src/HOL/IntDiv.thy Fri Jan 30 17:47:34 2009 +0100
+++ b/src/HOL/IntDiv.thy Sat Jan 31 09:04:42 2009 +0100
@@ -1173,16 +1173,16 @@
lemma zdvd_trans: "m dvd n ==> n dvd k ==> m dvd (k::int)"
by (rule dvd_trans)
-lemma zdvd_zminus_iff: "m dvd -n \<longleftrightarrow> m dvd (n::int)"
+lemma zdvd_zminus_iff[simp]: "m dvd -n \<longleftrightarrow> m dvd (n::int)"
by (rule dvd_minus_iff)
-lemma zdvd_zminus2_iff: "-m dvd n \<longleftrightarrow> m dvd (n::int)"
+lemma zdvd_zminus2_iff[simp]: "-m dvd n \<longleftrightarrow> m dvd (n::int)"
by (rule minus_dvd_iff)
-lemma zdvd_abs1: "( \<bar>i::int\<bar> dvd j) = (i dvd j)"
+lemma zdvd_abs1[simp]: "( \<bar>i::int\<bar> dvd j) = (i dvd j)"
by (cases "i > 0") (simp_all add: zdvd_zminus2_iff)
-lemma zdvd_abs2: "( (i::int) dvd \<bar>j\<bar>) = (i dvd j)"
+lemma zdvd_abs2[simp]: "( (i::int) dvd \<bar>j\<bar>) = (i dvd j)"
by (cases "j > 0") (simp_all add: zdvd_zminus_iff)
lemma zdvd_anti_sym:
--- a/src/HOL/Matrix/Matrix.thy Fri Jan 30 17:47:34 2009 +0100
+++ b/src/HOL/Matrix/Matrix.thy Sat Jan 31 09:04:42 2009 +0100
@@ -1005,15 +1005,8 @@
apply (subst foldseq_almostzero[of _ j])
apply (simp add: prems)+
apply (auto)
- proof -
- fix k
- fix l
- assume a:"~neg(int l - int i)"
- assume b:"nat (int l - int i) = 0"
- from a b have a: "l = i" by(insert not_neg_nat[of "int l - int i"], simp add: a b)
- assume c: "i \<noteq> l"
- from c a show "fmul (Rep_matrix A k j) e = 0" by blast
- qed
+ apply (metis comm_monoid_add.mult_1 le_anti_sym le_diff_eq not_neg_nat zero_le_imp_of_nat zle_int)
+ done
lemma mult_matrix_ext:
assumes
--- a/src/HOL/Ring_and_Field.thy Fri Jan 30 17:47:34 2009 +0100
+++ b/src/HOL/Ring_and_Field.thy Sat Jan 31 09:04:42 2009 +0100
@@ -1053,26 +1053,53 @@
lemma sgn_sgn [simp]:
"sgn (sgn a) = sgn a"
- unfolding sgn_if by simp
+unfolding sgn_if by simp
lemma sgn_0_0:
"sgn a = 0 \<longleftrightarrow> a = 0"
- unfolding sgn_if by simp
+unfolding sgn_if by simp
lemma sgn_1_pos:
"sgn a = 1 \<longleftrightarrow> a > 0"
- unfolding sgn_if by (simp add: neg_equal_zero)
+unfolding sgn_if by (simp add: neg_equal_zero)
lemma sgn_1_neg:
"sgn a = - 1 \<longleftrightarrow> a < 0"
- unfolding sgn_if by (auto simp add: equal_neg_zero)
+unfolding sgn_if by (auto simp add: equal_neg_zero)
lemma sgn_times:
"sgn (a * b) = sgn a * sgn b"
by (auto simp add: sgn_if zero_less_mult_iff)
lemma abs_sgn: "abs k = k * sgn k"
- unfolding sgn_if abs_if by auto
+unfolding sgn_if abs_if by auto
+
+(* The int instances are proved, these generic ones are tedious to prove here.
+And not very useful, as int seems to be the only instance.
+If needed, they should be proved later, when metis is available.
+lemma dvd_abs[simp]: "(abs m) dvd k \<longleftrightarrow> m dvd k"
+proof-
+ have "\<forall>k.\<exists>ka. - (m * k) = m * ka"
+ by(simp add: mult_minus_right[symmetric] del: mult_minus_right)
+ moreover
+ have "\<forall>k.\<exists>ka. m * k = - (m * ka)"
+ by(auto intro!: minus_minus[symmetric]
+ simp add: mult_minus_right[symmetric] simp del: mult_minus_right)
+ ultimately show ?thesis by (auto simp: abs_if dvd_def)
+qed
+
+lemma dvd_abs2[simp]: "m dvd (abs k) \<longleftrightarrow> m dvd k"
+proof-
+ have "\<forall>k.\<exists>ka. - (m * k) = m * ka"
+ by(simp add: mult_minus_right[symmetric] del: mult_minus_right)
+ moreover
+ have "\<forall>k.\<exists>ka. - (m * ka) = m * k"
+ by(auto intro!: minus_minus
+ simp add: mult_minus_right[symmetric] simp del: mult_minus_right)
+ ultimately show ?thesis
+ by (auto simp add:abs_if dvd_def minus_equation_iff[of k])
+qed
+*)
end
--- a/src/HOL/ex/Reflected_Presburger.thy Fri Jan 30 17:47:34 2009 +0100
+++ b/src/HOL/ex/Reflected_Presburger.thy Sat Jan 31 09:04:42 2009 +0100
@@ -995,7 +995,7 @@
hence ?case using prems by (simp del: zlfm.simps add: zdvd_0_left)}
moreover
{assume "?c=0" and "j\<noteq>0" hence ?case
- using zsplit0_I[OF spl, where x="i" and bs="bs"] zdvd_abs1[where i="j"]
+ using zsplit0_I[OF spl, where x="i" and bs="bs"]
apply (auto simp add: Let_def split_def algebra_simps)
apply (cases "?r",auto)
apply (case_tac nat, auto)
@@ -1003,14 +1003,12 @@
moreover
{assume cp: "?c > 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))"
by (simp add: nb Let_def split_def)
- hence ?case using Ia cp jnz by (simp add: Let_def split_def
- zdvd_abs1[where i="j" and j="(?c*i) + ?N ?r", symmetric])}
+ hence ?case using Ia cp jnz by (simp add: Let_def split_def)}
moreover
{assume cn: "?c < 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))"
by (simp add: nb Let_def split_def)
hence ?case using Ia cn jnz zdvd_zminus_iff[where m="abs j" and n="?c*i + ?N ?r" ]
- by (simp add: Let_def split_def
- zdvd_abs1[where i="j" and j="(?c*i) + ?N ?r", symmetric])}
+ by (simp add: Let_def split_def) }
ultimately show ?case by blast
next
case (12 j a)
@@ -1026,7 +1024,7 @@
hence ?case using prems by (simp del: zlfm.simps add: zdvd_0_left)}
moreover
{assume "?c=0" and "j\<noteq>0" hence ?case
- using zsplit0_I[OF spl, where x="i" and bs="bs"] zdvd_abs1[where i="j"]
+ using zsplit0_I[OF spl, where x="i" and bs="bs"]
apply (auto simp add: Let_def split_def algebra_simps)
apply (cases "?r",auto)
apply (case_tac nat, auto)
@@ -1034,14 +1032,12 @@
moreover
{assume cp: "?c > 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))"
by (simp add: nb Let_def split_def)
- hence ?case using Ia cp jnz by (simp add: Let_def split_def
- zdvd_abs1[where i="j" and j="(?c*i) + ?N ?r", symmetric])}
+ hence ?case using Ia cp jnz by (simp add: Let_def split_def) }
moreover
{assume cn: "?c < 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))"
by (simp add: nb Let_def split_def)
hence ?case using Ia cn jnz zdvd_zminus_iff[where m="abs j" and n="?c*i + ?N ?r" ]
- by (simp add: Let_def split_def
- zdvd_abs1[where i="j" and j="(?c*i) + ?N ?r", symmetric])}
+ by (simp add: Let_def split_def)}
ultimately show ?case by blast
qed auto
@@ -1210,7 +1206,7 @@
"mirror p = p"
(* Lemmas for the correctness of \<sigma>\<rho> *)
lemma dvd1_eq1: "x >0 \<Longrightarrow> (x::int) dvd 1 = (x = 1)"
-by auto
+by simp
lemma minusinf_inf:
assumes linp: "iszlfm p"
@@ -1220,12 +1216,12 @@
using linp u
proof (induct p rule: minusinf.induct)
case (1 p q) thus ?case
- by (auto simp add: dvd1_eq1) (rule_tac x="min z za" in exI,simp)
+ by auto (rule_tac x="min z za" in exI,simp)
next
case (2 p q) thus ?case
- by (auto simp add: dvd1_eq1) (rule_tac x="min z za" in exI,simp)
+ by auto (rule_tac x="min z za" in exI,simp)
next
- case (3 c e) hence c1: "c=1" and nb: "numbound0 e" using dvd1_eq1 by simp+
+ case (3 c e) hence c1: "c=1" and nb: "numbound0 e" by simp+
fix a
from 3 have "\<forall> x<(- Inum (a#bs) e). c*x + Inum (x#bs) e \<noteq> 0"
proof(clarsimp)
@@ -1235,7 +1231,7 @@
qed
thus ?case by auto
next
- case (4 c e) hence c1: "c=1" and nb: "numbound0 e" using dvd1_eq1 by simp+
+ case (4 c e) hence c1: "c=1" and nb: "numbound0 e" by simp+
fix a
from 4 have "\<forall> x<(- Inum (a#bs) e). c*x + Inum (x#bs) e \<noteq> 0"
proof(clarsimp)
@@ -1245,7 +1241,7 @@
qed
thus ?case by auto
next
- case (5 c e) hence c1: "c=1" and nb: "numbound0 e" using dvd1_eq1 by simp+
+ case (5 c e) hence c1: "c=1" and nb: "numbound0 e" by simp+
fix a
from 5 have "\<forall> x<(- Inum (a#bs) e). c*x + Inum (x#bs) e < 0"
proof(clarsimp)
@@ -1255,7 +1251,7 @@
qed
thus ?case by auto
next
- case (6 c e) hence c1: "c=1" and nb: "numbound0 e" using dvd1_eq1 by simp+
+ case (6 c e) hence c1: "c=1" and nb: "numbound0 e" by simp+
fix a
from 6 have "\<forall> x<(- Inum (a#bs) e). c*x + Inum (x#bs) e \<le> 0"
proof(clarsimp)
@@ -1265,7 +1261,7 @@
qed
thus ?case by auto
next
- case (7 c e) hence c1: "c=1" and nb: "numbound0 e" using dvd1_eq1 by simp+
+ case (7 c e) hence c1: "c=1" and nb: "numbound0 e" by simp+
fix a
from 7 have "\<forall> x<(- Inum (a#bs) e). \<not> (c*x + Inum (x#bs) e > 0)"
proof(clarsimp)
@@ -1275,7 +1271,7 @@
qed
thus ?case by auto
next
- case (8 c e) hence c1: "c=1" and nb: "numbound0 e" using dvd1_eq1 by simp+
+ case (8 c e) hence c1: "c=1" and nb: "numbound0 e" by simp+
fix a
from 8 have "\<forall> x<(- Inum (a#bs) e). \<not> (c*x + Inum (x#bs) e \<ge> 0)"
proof(clarsimp)
@@ -1595,15 +1591,15 @@
shows "?P (x - d)"
using lp u d dp nob p
proof(induct p rule: iszlfm.induct)
- case (5 c e) hence c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
+ case (5 c e) hence c1: "c=1" and bn:"numbound0 e" by simp+
with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] prems
show ?case by simp
next
- case (6 c e) hence c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
+ case (6 c e) hence c1: "c=1" and bn:"numbound0 e" by simp+
with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] prems
show ?case by simp
next
- case (7 c e) hence p: "Ifm bbs (x #bs) (Gt (CN 0 c e))" and c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
+ case (7 c e) hence p: "Ifm bbs (x #bs) (Gt (CN 0 c e))" and c1: "c=1" and bn:"numbound0 e" by simp+
let ?e = "Inum (x # bs) e"
{assume "(x-d) +?e > 0" hence ?case using c1
numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] by simp}
@@ -1622,7 +1618,7 @@
ultimately show ?case by blast
next
case (8 c e) hence p: "Ifm bbs (x #bs) (Ge (CN 0 c e))" and c1: "c=1" and bn:"numbound0 e"
- using dvd1_eq1[where x="c"] by simp+
+ by simp+
let ?e = "Inum (x # bs) e"
{assume "(x-d) +?e \<ge> 0" hence ?case using c1
numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"]
@@ -1640,7 +1636,7 @@
with nob have ?case by simp }
ultimately show ?case by blast
next
- case (3 c e) hence p: "Ifm bbs (x #bs) (Eq (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
+ case (3 c e) hence p: "Ifm bbs (x #bs) (Eq (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" by simp+
let ?e = "Inum (x # bs) e"
let ?v="(Sub (C -1) e)"
have vb: "?v \<in> set (\<beta> (Eq (CN 0 c e)))" by simp
@@ -1648,7 +1644,7 @@
by simp (erule ballE[where x="1"],
simp_all add:algebra_simps numbound0_I[OF bn,where b="x"and b'="a"and bs="bs"])
next
- case (4 c e)hence p: "Ifm bbs (x #bs) (NEq (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
+ case (4 c e)hence p: "Ifm bbs (x #bs) (NEq (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" by simp+
let ?e = "Inum (x # bs) e"
let ?v="Neg e"
have vb: "?v \<in> set (\<beta> (NEq (CN 0 c e)))" by simp
@@ -1662,7 +1658,7 @@
with prems(11) have ?case using dp by simp}
ultimately show ?case by blast
next
- case (9 j c e) hence p: "Ifm bbs (x #bs) (Dvd j (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
+ case (9 j c e) hence p: "Ifm bbs (x #bs) (Dvd j (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" by simp+
let ?e = "Inum (x # bs) e"
from prems have id: "j dvd d" by simp
from c1 have "?p x = (j dvd (x+ ?e))" by simp
@@ -1671,7 +1667,7 @@
finally show ?case
using numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] c1 p by simp
next
- case (10 j c e) hence p: "Ifm bbs (x #bs) (NDvd j (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
+ case (10 j c e) hence p: "Ifm bbs (x #bs) (NDvd j (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" by simp+
let ?e = "Inum (x # bs) e"
from prems have id: "j dvd d" by simp
from c1 have "?p x = (\<not> j dvd (x+ ?e))" by simp