# HG changeset patch
# User nipkow
# Date 1233389056 -3600
# Node ID 22faf21db3df91e5f1bf2b39fadbbb78f832d8c1
# Parent  91feea8e41e4db077c1c1381c599b4e98d49d241
added some simp rules

diff -r 91feea8e41e4 -r 22faf21db3df src/HOL/Algebra/IntRing.thy
--- a/src/HOL/Algebra/IntRing.thy	Fri Jan 30 13:41:45 2009 +0000
+++ b/src/HOL/Algebra/IntRing.thy	Sat Jan 31 09:04:16 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)
diff -r 91feea8e41e4 -r 22faf21db3df src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Fri Jan 30 13:41:45 2009 +0000
+++ b/src/HOL/GCD.thy	Sat Jan 31 09:04:16 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"
diff -r 91feea8e41e4 -r 22faf21db3df src/HOL/Int.thy
--- a/src/HOL/Int.thy	Fri Jan 30 13:41:45 2009 +0000
+++ b/src/HOL/Int.thy	Sat Jan 31 09:04:16 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)
 
diff -r 91feea8e41e4 -r 22faf21db3df src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Fri Jan 30 13:41:45 2009 +0000
+++ b/src/HOL/IntDiv.thy	Sat Jan 31 09:04:16 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:
diff -r 91feea8e41e4 -r 22faf21db3df src/HOL/Matrix/Matrix.thy
--- a/src/HOL/Matrix/Matrix.thy	Fri Jan 30 13:41:45 2009 +0000
+++ b/src/HOL/Matrix/Matrix.thy	Sat Jan 31 09:04:16 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
diff -r 91feea8e41e4 -r 22faf21db3df src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Fri Jan 30 13:41:45 2009 +0000
+++ b/src/HOL/Ring_and_Field.thy	Sat Jan 31 09:04:16 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
 
diff -r 91feea8e41e4 -r 22faf21db3df src/HOL/ex/Reflected_Presburger.thy
--- a/src/HOL/ex/Reflected_Presburger.thy	Fri Jan 30 13:41:45 2009 +0000
+++ b/src/HOL/ex/Reflected_Presburger.thy	Sat Jan 31 09:04:16 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