added some simp rules
authornipkow
Sat Jan 31 09:04:16 2009 +0100 (2009-01-31)
changeset 2970022faf21db3df
parent 29698 91feea8e41e4
child 29701 caf1dc04e116
added some simp rules
src/HOL/Algebra/IntRing.thy
src/HOL/GCD.thy
src/HOL/Int.thy
src/HOL/IntDiv.thy
src/HOL/Matrix/Matrix.thy
src/HOL/Ring_and_Field.thy
src/HOL/ex/Reflected_Presburger.thy
     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.16 +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.12 +by(simp add: nat_eq_iff) arith
    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.5    apply (simp add: prems)+
     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