author nipkow Sat, 31 Jan 2009 09:04:42 +0100 changeset 29701 caf1dc04e116 parent 29699 987ed08d82cd (current diff) parent 29700 22faf21db3df (diff) child 29704 9a7d84fd83c6
merged
```--- 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)

lemma zgcd_zdvd2 [iff,simp, algebra]: "zgcd i j dvd j"
-  by (simp add: zgcd_def int_dvd_iff)

lemma zgcd_pos: "zgcd i j \<ge> 0"

lemma zgcd0 [simp,algebra]: "(zgcd i j = 0) = (i = 0 \<and> j = 0)"
-  by (simp add: zgcd_def gcd_zero) arith

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"
+
lemma int_eq_iff: "(of_nat m = z) = (m = nat z & 0 \<le> z)"
```
```--- 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 (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```