author nipkow Sat Jan 31 09:04:16 2009 +0100 (2009-01-31 ago) changeset 29700 22faf21db3df parent 29698 91feea8e41e4 child 29701 caf1dc04e116
 src/HOL/Algebra/IntRing.thy file | annotate | diff | revisions src/HOL/GCD.thy file | annotate | diff | revisions src/HOL/Int.thy file | annotate | diff | revisions src/HOL/IntDiv.thy file | annotate | diff | revisions src/HOL/Matrix/Matrix.thy file | annotate | diff | revisions src/HOL/Ring_and_Field.thy file | annotate | diff | revisions src/HOL/ex/Reflected_Presburger.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Algebra/IntRing.thy	Fri Jan 30 13:41:45 2009 +0000
1.2 +++ b/src/HOL/Algebra/IntRing.thy	Sat Jan 31 09:04:16 2009 +0100
1.3 @@ -265,6 +265,7 @@
1.4  apply fast
1.5  done
1.6
1.7 +
1.8  lemma prime_primeideal:
1.9    assumes prime: "prime (nat p)"
1.10    shows "primeideal (Idl\<^bsub>\<Z>\<^esub> {p}) \<Z>"
1.11 @@ -293,17 +294,7 @@
1.12
1.13    assume "a * b = x * p"
1.14    hence "p dvd a * b" by simp
1.15 -  hence "nat p dvd nat (abs (a * b))"
1.16 -  apply (subst nat_dvd_iff, clarsimp)
1.17 -  apply (rule conjI, clarsimp, simp add: zabs_def)
1.18 -  proof (clarsimp)
1.19 -    assume a: " ~ 0 <= p"
1.20 -    from prime
1.21 -        have "0 < p" by (simp add: prime_def)
1.22 -    from a and this
1.23 -        have "False" by simp
1.24 -    thus "nat (abs (a * b)) = 0" ..
1.25 -  qed
1.26 +  hence "nat p dvd nat (abs (a * b))" using ppos by (simp add: nat_dvd_iff)
1.27    hence "nat p dvd (nat (abs a) * nat (abs b))" by (simp add: nat_abs_mult_distrib)
1.28    hence "nat p dvd nat (abs a) | nat p dvd nat (abs b)" by (rule prime_dvd_mult[OF prime])
1.29    hence "p dvd a | p dvd b" by (fast intro: unnat)
```
```     2.1 --- a/src/HOL/GCD.thy	Fri Jan 30 13:41:45 2009 +0000
2.2 +++ b/src/HOL/GCD.thy	Sat Jan 31 09:04:16 2009 +0100
2.3 @@ -562,25 +562,25 @@
2.4    "zgcd i j = int (gcd (nat (abs i)) (nat (abs j)))"
2.5
2.6  lemma zgcd_zdvd1 [iff,simp, algebra]: "zgcd i j dvd i"
2.7 -  by (simp add: zgcd_def int_dvd_iff)
2.8 +by (simp add: zgcd_def int_dvd_iff)
2.9
2.10  lemma zgcd_zdvd2 [iff,simp, algebra]: "zgcd i j dvd j"
2.11 -  by (simp add: zgcd_def int_dvd_iff)
2.12 +by (simp add: zgcd_def int_dvd_iff)
2.13
2.14  lemma zgcd_pos: "zgcd i j \<ge> 0"
2.15 -  by (simp add: zgcd_def)
2.17
2.18  lemma zgcd0 [simp,algebra]: "(zgcd i j = 0) = (i = 0 \<and> j = 0)"
2.19 -  by (simp add: zgcd_def gcd_zero) arith
2.20 +by (simp add: zgcd_def gcd_zero)
2.21
2.22  lemma zgcd_commute: "zgcd i j = zgcd j i"
2.23 -  unfolding zgcd_def by (simp add: gcd_commute)
2.24 +unfolding zgcd_def by (simp add: gcd_commute)
2.25
2.26  lemma zgcd_zminus [simp, algebra]: "zgcd (- i) j = zgcd i j"
2.27 -  unfolding zgcd_def by simp
2.28 +unfolding zgcd_def by simp
2.29
2.30  lemma zgcd_zminus2 [simp, algebra]: "zgcd i (- j) = zgcd i j"
2.31 -  unfolding zgcd_def by simp
2.32 +unfolding zgcd_def by simp
2.33
2.34    (* should be solved by algebra*)
2.35  lemma zrelprime_dvd_mult: "zgcd i j = 1 \<Longrightarrow> i dvd k * j \<Longrightarrow> i dvd k"
```
```     3.1 --- a/src/HOL/Int.thy	Fri Jan 30 13:41:45 2009 +0000
3.2 +++ b/src/HOL/Int.thy	Sat Jan 31 09:04:16 2009 +0100
3.3 @@ -442,9 +442,12 @@
3.4
3.5  lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < of_nat m)"
3.6  apply (cases w)
3.7 -apply (simp add: nat le int_def Zero_int_def linorder_not_le [symmetric], arith)
3.8 +apply (simp add: nat le int_def Zero_int_def linorder_not_le[symmetric], arith)
3.9  done
3.10
3.11 +lemma nat_0_iff[simp]: "nat(i::int) = 0 \<longleftrightarrow> i\<le>0"
3.13 +
3.14  lemma int_eq_iff: "(of_nat m = z) = (m = nat z & 0 \<le> z)"
3.15  by (auto simp add: nat_eq_iff2)
3.16
```
```     4.1 --- a/src/HOL/IntDiv.thy	Fri Jan 30 13:41:45 2009 +0000
4.2 +++ b/src/HOL/IntDiv.thy	Sat Jan 31 09:04:16 2009 +0100
4.3 @@ -1173,16 +1173,16 @@
4.4  lemma zdvd_trans: "m dvd n ==> n dvd k ==> m dvd (k::int)"
4.5    by (rule dvd_trans)
4.6
4.7 -lemma zdvd_zminus_iff: "m dvd -n \<longleftrightarrow> m dvd (n::int)"
4.8 +lemma zdvd_zminus_iff[simp]: "m dvd -n \<longleftrightarrow> m dvd (n::int)"
4.9    by (rule dvd_minus_iff)
4.10
4.11 -lemma zdvd_zminus2_iff: "-m dvd n \<longleftrightarrow> m dvd (n::int)"
4.12 +lemma zdvd_zminus2_iff[simp]: "-m dvd n \<longleftrightarrow> m dvd (n::int)"
4.13    by (rule minus_dvd_iff)
4.14
4.15 -lemma zdvd_abs1: "( \<bar>i::int\<bar> dvd j) = (i dvd j)"
4.16 +lemma zdvd_abs1[simp]: "( \<bar>i::int\<bar> dvd j) = (i dvd j)"
4.17    by (cases "i > 0") (simp_all add: zdvd_zminus2_iff)
4.18
4.19 -lemma zdvd_abs2: "( (i::int) dvd \<bar>j\<bar>) = (i dvd j)"
4.20 +lemma zdvd_abs2[simp]: "( (i::int) dvd \<bar>j\<bar>) = (i dvd j)"
4.21    by (cases "j > 0") (simp_all add: zdvd_zminus_iff)
4.22
4.23  lemma zdvd_anti_sym:
```
```     5.1 --- a/src/HOL/Matrix/Matrix.thy	Fri Jan 30 13:41:45 2009 +0000
5.2 +++ b/src/HOL/Matrix/Matrix.thy	Sat Jan 31 09:04:16 2009 +0100
5.3 @@ -1005,15 +1005,8 @@
5.4    apply (subst foldseq_almostzero[of _ j])
5.6    apply (auto)
5.7 -  proof -
5.8 -    fix k
5.9 -    fix l
5.10 -    assume a:"~neg(int l - int i)"
5.11 -    assume b:"nat (int l - int i) = 0"
5.12 -    from a b have a: "l = i" by(insert not_neg_nat[of "int l - int i"], simp add: a b)
5.13 -    assume c: "i \<noteq> l"
5.14 -    from c a show "fmul (Rep_matrix A k j) e = 0" by blast
5.15 -  qed
5.16 +  apply (metis comm_monoid_add.mult_1 le_anti_sym le_diff_eq not_neg_nat zero_le_imp_of_nat zle_int)
5.17 +  done
5.18
5.19  lemma mult_matrix_ext:
5.20    assumes
```
```     6.1 --- a/src/HOL/Ring_and_Field.thy	Fri Jan 30 13:41:45 2009 +0000
6.2 +++ b/src/HOL/Ring_and_Field.thy	Sat Jan 31 09:04:16 2009 +0100
6.3 @@ -1053,26 +1053,53 @@
6.4
6.5  lemma sgn_sgn [simp]:
6.6    "sgn (sgn a) = sgn a"
6.7 -  unfolding sgn_if by simp
6.8 +unfolding sgn_if by simp
6.9
6.10  lemma sgn_0_0:
6.11    "sgn a = 0 \<longleftrightarrow> a = 0"
6.12 -  unfolding sgn_if by simp
6.13 +unfolding sgn_if by simp
6.14
6.15  lemma sgn_1_pos:
6.16    "sgn a = 1 \<longleftrightarrow> a > 0"
6.17 -  unfolding sgn_if by (simp add: neg_equal_zero)
6.18 +unfolding sgn_if by (simp add: neg_equal_zero)
6.19
6.20  lemma sgn_1_neg:
6.21    "sgn a = - 1 \<longleftrightarrow> a < 0"
6.22 -  unfolding sgn_if by (auto simp add: equal_neg_zero)
6.23 +unfolding sgn_if by (auto simp add: equal_neg_zero)
6.24
6.25  lemma sgn_times:
6.26    "sgn (a * b) = sgn a * sgn b"
6.27  by (auto simp add: sgn_if zero_less_mult_iff)
6.28
6.29  lemma abs_sgn: "abs k = k * sgn k"
6.30 -  unfolding sgn_if abs_if by auto
6.31 +unfolding sgn_if abs_if by auto
6.32 +
6.33 +(* The int instances are proved, these generic ones are tedious to prove here.
6.34 +And not very useful, as int seems to be the only instance.
6.35 +If needed, they should be proved later, when metis is available.
6.36 +lemma dvd_abs[simp]: "(abs m) dvd k \<longleftrightarrow> m dvd k"
6.37 +proof-
6.38 +  have "\<forall>k.\<exists>ka. - (m * k) = m * ka"
6.39 +    by(simp add: mult_minus_right[symmetric] del: mult_minus_right)
6.40 +  moreover
6.41 +  have "\<forall>k.\<exists>ka. m * k = - (m * ka)"
6.42 +    by(auto intro!: minus_minus[symmetric]
6.43 +         simp add: mult_minus_right[symmetric] simp del: mult_minus_right)
6.44 +  ultimately show ?thesis by (auto simp: abs_if dvd_def)
6.45 +qed
6.46 +
6.47 +lemma dvd_abs2[simp]: "m dvd (abs k) \<longleftrightarrow> m dvd k"
6.48 +proof-
6.49 +  have "\<forall>k.\<exists>ka. - (m * k) = m * ka"
6.50 +    by(simp add: mult_minus_right[symmetric] del: mult_minus_right)
6.51 +  moreover
6.52 +  have "\<forall>k.\<exists>ka. - (m * ka) = m * k"
6.53 +    by(auto intro!: minus_minus
6.54 +         simp add: mult_minus_right[symmetric] simp del: mult_minus_right)
6.55 +  ultimately show ?thesis
6.56 +    by (auto simp add:abs_if dvd_def minus_equation_iff[of k])
6.57 +qed
6.58 +*)
6.59
6.60  end
6.61
```
```     7.1 --- a/src/HOL/ex/Reflected_Presburger.thy	Fri Jan 30 13:41:45 2009 +0000
7.2 +++ b/src/HOL/ex/Reflected_Presburger.thy	Sat Jan 31 09:04:16 2009 +0100
7.3 @@ -995,7 +995,7 @@
7.4      hence ?case using prems by (simp del: zlfm.simps add: zdvd_0_left)}
7.5    moreover
7.6    {assume "?c=0" and "j\<noteq>0" hence ?case
7.7 -      using zsplit0_I[OF spl, where x="i" and bs="bs"] zdvd_abs1[where i="j"]
7.8 +      using zsplit0_I[OF spl, where x="i" and bs="bs"]
7.9      apply (auto simp add: Let_def split_def algebra_simps)
7.10      apply (cases "?r",auto)
7.11      apply (case_tac nat, auto)
7.12 @@ -1003,14 +1003,12 @@
7.13    moreover
7.14    {assume cp: "?c > 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))"
7.15        by (simp add: nb Let_def split_def)
7.16 -    hence ?case using Ia cp jnz by (simp add: Let_def split_def
7.17 -	zdvd_abs1[where i="j" and j="(?c*i) + ?N ?r", symmetric])}
7.18 +    hence ?case using Ia cp jnz by (simp add: Let_def split_def)}
7.19    moreover
7.20    {assume cn: "?c < 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))"
7.21        by (simp add: nb Let_def split_def)
7.22      hence ?case using Ia cn jnz zdvd_zminus_iff[where m="abs j" and n="?c*i + ?N ?r" ]
7.23 -      by (simp add: Let_def split_def
7.24 -      zdvd_abs1[where i="j" and j="(?c*i) + ?N ?r", symmetric])}
7.25 +      by (simp add: Let_def split_def) }
7.26    ultimately show ?case by blast
7.27  next
7.28    case (12 j a)
7.29 @@ -1026,7 +1024,7 @@
7.30      hence ?case using prems by (simp del: zlfm.simps add: zdvd_0_left)}
7.31    moreover
7.32    {assume "?c=0" and "j\<noteq>0" hence ?case
7.33 -      using zsplit0_I[OF spl, where x="i" and bs="bs"] zdvd_abs1[where i="j"]
7.34 +      using zsplit0_I[OF spl, where x="i" and bs="bs"]
7.35      apply (auto simp add: Let_def split_def algebra_simps)
7.36      apply (cases "?r",auto)
7.37      apply (case_tac nat, auto)
7.38 @@ -1034,14 +1032,12 @@
7.39    moreover
7.40    {assume cp: "?c > 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))"
7.41        by (simp add: nb Let_def split_def)
7.42 -    hence ?case using Ia cp jnz by (simp add: Let_def split_def
7.43 -	zdvd_abs1[where i="j" and j="(?c*i) + ?N ?r", symmetric])}
7.44 +    hence ?case using Ia cp jnz by (simp add: Let_def split_def) }
7.45    moreover
7.46    {assume cn: "?c < 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))"
7.47        by (simp add: nb Let_def split_def)
7.48      hence ?case using Ia cn jnz zdvd_zminus_iff[where m="abs j" and n="?c*i + ?N ?r" ]
7.49 -      by (simp add: Let_def split_def
7.50 -      zdvd_abs1[where i="j" and j="(?c*i) + ?N ?r", symmetric])}
7.51 +      by (simp add: Let_def split_def)}
7.52    ultimately show ?case by blast
7.53  qed auto
7.54
7.55 @@ -1210,7 +1206,7 @@
7.56    "mirror p = p"
7.57      (* Lemmas for the correctness of \<sigma>\<rho> *)
7.58  lemma dvd1_eq1: "x >0 \<Longrightarrow> (x::int) dvd 1 = (x = 1)"
7.59 -by auto
7.60 +by simp
7.61
7.62  lemma minusinf_inf:
7.63    assumes linp: "iszlfm p"
7.64 @@ -1220,12 +1216,12 @@
7.65  using linp u
7.66  proof (induct p rule: minusinf.induct)
7.67    case (1 p q) thus ?case
7.68 -    by (auto simp add: dvd1_eq1) (rule_tac x="min z za" in exI,simp)
7.69 +    by auto (rule_tac x="min z za" in exI,simp)
7.70  next
7.71    case (2 p q) thus ?case
7.72 -    by (auto simp add: dvd1_eq1) (rule_tac x="min z za" in exI,simp)
7.73 +    by auto (rule_tac x="min z za" in exI,simp)
7.74  next
7.75 -  case (3 c e) hence c1: "c=1" and nb: "numbound0 e" using dvd1_eq1 by simp+
7.76 +  case (3 c e) hence c1: "c=1" and nb: "numbound0 e" by simp+
7.77    fix a
7.78    from 3 have "\<forall> x<(- Inum (a#bs) e). c*x + Inum (x#bs) e \<noteq> 0"
7.79    proof(clarsimp)
7.80 @@ -1235,7 +1231,7 @@
7.81    qed
7.82    thus ?case by auto
7.83  next
7.84 -  case (4 c e) hence c1: "c=1" and nb: "numbound0 e" using dvd1_eq1 by simp+
7.85 +  case (4 c e) hence c1: "c=1" and nb: "numbound0 e" by simp+
7.86    fix a
7.87    from 4 have "\<forall> x<(- Inum (a#bs) e). c*x + Inum (x#bs) e \<noteq> 0"
7.88    proof(clarsimp)
7.89 @@ -1245,7 +1241,7 @@
7.90    qed
7.91    thus ?case by auto
7.92  next
7.93 -  case (5 c e) hence c1: "c=1" and nb: "numbound0 e" using dvd1_eq1 by simp+
7.94 +  case (5 c e) hence c1: "c=1" and nb: "numbound0 e" by simp+
7.95    fix a
7.96    from 5 have "\<forall> x<(- Inum (a#bs) e). c*x + Inum (x#bs) e < 0"
7.97    proof(clarsimp)
7.98 @@ -1255,7 +1251,7 @@
7.99    qed
7.100    thus ?case by auto
7.101  next
7.102 -  case (6 c e) hence c1: "c=1" and nb: "numbound0 e" using dvd1_eq1 by simp+
7.103 +  case (6 c e) hence c1: "c=1" and nb: "numbound0 e" by simp+
7.104    fix a
7.105    from 6 have "\<forall> x<(- Inum (a#bs) e). c*x + Inum (x#bs) e \<le> 0"
7.106    proof(clarsimp)
7.107 @@ -1265,7 +1261,7 @@
7.108    qed
7.109    thus ?case by auto
7.110  next
7.111 -  case (7 c e) hence c1: "c=1" and nb: "numbound0 e" using dvd1_eq1 by simp+
7.112 +  case (7 c e) hence c1: "c=1" and nb: "numbound0 e" by simp+
7.113    fix a
7.114    from 7 have "\<forall> x<(- Inum (a#bs) e). \<not> (c*x + Inum (x#bs) e > 0)"
7.115    proof(clarsimp)
7.116 @@ -1275,7 +1271,7 @@
7.117    qed
7.118    thus ?case by auto
7.119  next
7.120 -  case (8 c e) hence c1: "c=1" and nb: "numbound0 e" using dvd1_eq1 by simp+
7.121 +  case (8 c e) hence c1: "c=1" and nb: "numbound0 e" by simp+
7.122    fix a
7.123    from 8 have "\<forall> x<(- Inum (a#bs) e). \<not> (c*x + Inum (x#bs) e \<ge> 0)"
7.124    proof(clarsimp)
7.125 @@ -1595,15 +1591,15 @@
7.126    shows "?P (x - d)"
7.127  using lp u d dp nob p
7.128  proof(induct p rule: iszlfm.induct)
7.129 -  case (5 c e) hence c1: "c=1" and  bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
7.130 +  case (5 c e) hence c1: "c=1" and  bn:"numbound0 e" by simp+
7.131      with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] prems
7.132      show ?case by simp
7.133  next
7.134 -  case (6 c e)  hence c1: "c=1" and  bn:"numbound0 e" using dvd1_eq1[where x="c"] by simp+
7.135 +  case (6 c e)  hence c1: "c=1" and  bn:"numbound0 e" by simp+
7.136      with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] prems
7.137      show ?case by simp
7.138  next
7.139 -  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+
7.140 +  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+
7.141      let ?e = "Inum (x # bs) e"
7.142      {assume "(x-d) +?e > 0" hence ?case using c1
7.143        numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] by simp}
7.144 @@ -1622,7 +1618,7 @@
7.145      ultimately show ?case by blast
7.146  next
7.147    case (8 c e) hence p: "Ifm bbs (x #bs) (Ge (CN 0 c e))" and c1: "c=1" and bn:"numbound0 e"
7.148 -    using dvd1_eq1[where x="c"] by simp+
7.149 +    by simp+
7.150      let ?e = "Inum (x # bs) e"
7.151      {assume "(x-d) +?e \<ge> 0" hence ?case using  c1
7.152        numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"]
7.153 @@ -1640,7 +1636,7 @@
7.154        with nob have ?case by simp }
7.155      ultimately show ?case by blast
7.156  next
7.157 -  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+
7.158 +  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+
7.159      let ?e = "Inum (x # bs) e"
7.160      let ?v="(Sub (C -1) e)"
7.161      have vb: "?v \<in> set (\<beta> (Eq (CN 0 c e)))" by simp
7.162 @@ -1648,7 +1644,7 @@
7.163        by simp (erule ballE[where x="1"],
7.164  	simp_all add:algebra_simps numbound0_I[OF bn,where b="x"and b'="a"and bs="bs"])
7.165  next
7.166 -  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+
7.167 +  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+
7.168      let ?e = "Inum (x # bs) e"
7.169      let ?v="Neg e"
7.170      have vb: "?v \<in> set (\<beta> (NEq (CN 0 c e)))" by simp
7.171 @@ -1662,7 +1658,7 @@
7.172         with prems(11) have ?case using dp by simp}
7.173    ultimately show ?case by blast
7.174  next
7.175 -  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+
7.176 +  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+
7.177      let ?e = "Inum (x # bs) e"
7.178      from prems have id: "j dvd d" by simp
7.179      from c1 have "?p x = (j dvd (x+ ?e))" by simp
7.180 @@ -1671,7 +1667,7 @@
7.181      finally show ?case
7.182        using numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] c1 p by simp
7.183  next
7.184 -  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+
7.185 +  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+
7.186      let ?e = "Inum (x # bs) e"
7.187      from prems have id: "j dvd d" by simp
7.188      from c1 have "?p x = (\<not> j dvd (x+ ?e))" by simp
```