# HG changeset patch
# User chaieb
# Date 1181552764 -7200
# Node ID df3a7e9ebadba81ee91ea17141bc4d6c1fe3d9b1
# Parent  6894137e854a52a53b8e0809358e64fa1058aa38
tuned Proof

diff -r 6894137e854a -r df3a7e9ebadb src/HOL/Auth/Public.thy
--- a/src/HOL/Auth/Public.thy	Mon Jun 11 11:06:00 2007 +0200
+++ b/src/HOL/Auth/Public.thy	Mon Jun 11 11:06:04 2007 +0200
@@ -62,7 +62,8 @@
    apply (rule exI [of _ 
        "%b A. 2 * agent_case 0 (\<lambda>n. n + 2) 1 A + keymode_case 0 1 b"])
    apply (auto simp add: inj_on_def split: agent.split keymode.split)
-   apply presburger+
+   apply presburger
+   apply presburger
    done                       
 
 
diff -r 6894137e854a -r df3a7e9ebadb src/HOL/Hyperreal/Integration.thy
--- a/src/HOL/Hyperreal/Integration.thy	Mon Jun 11 11:06:00 2007 +0200
+++ b/src/HOL/Hyperreal/Integration.thy	Mon Jun 11 11:06:04 2007 +0200
@@ -766,7 +766,9 @@
 apply (drule_tac x = "na + n" in spec, safe)
 apply (rule_tac y="D (na + n)" in order_trans)
 apply (case_tac "na = 0", auto)
-apply (erule partition_lt_gen [THEN order_less_imp_le], arith+)
+apply (erule partition_lt_gen [THEN order_less_imp_le])
+apply arith
+apply arith
 done
 
 lemma rsum_add: "rsum (D, p) (%x. f x + g x) =  rsum (D, p) f + rsum(D, p) g"
diff -r 6894137e854a -r df3a7e9ebadb src/HOL/Hyperreal/Poly.thy
--- a/src/HOL/Hyperreal/Poly.thy	Mon Jun 11 11:06:00 2007 +0200
+++ b/src/HOL/Hyperreal/Poly.thy	Mon Jun 11 11:06:04 2007 +0200
@@ -496,7 +496,9 @@
 apply (rule_tac x = "abs a + abs (j N) + 1" in exI)
 apply safe
 apply (drule_tac x = x in spec, safe) 
-apply (drule_tac x = "j n" in spec, arith+)
+apply (drule_tac x = "j n" in spec)
+apply arith
+apply arith
 done
 
 lemma poly_roots_finite: "(poly p \<noteq> poly []) =
diff -r 6894137e854a -r df3a7e9ebadb src/HOL/Library/Executable_Real.thy
--- a/src/HOL/Library/Executable_Real.thy	Mon Jun 11 11:06:00 2007 +0200
+++ b/src/HOL/Library/Executable_Real.thy	Mon Jun 11 11:06:04 2007 +0200
@@ -24,6 +24,7 @@
   "normNum \<equiv> \<lambda>(a,b). (if a=0 \<or> b = 0 then (0,0) else 
   (let g = igcd a b 
    in if b > 0 then (a div g, b div g) else (- (a div g), - (b div g))))"
+
 lemma normNum_isnormNum[simp]: "isnormNum (normNum x)"
 proof-
   have " \<exists> a b. x = (a,b)" by auto
@@ -57,7 +58,7 @@
 	from gpos have th: "?g \<ge> 0" by arith
 	from mult_nonneg_nonneg[OF th b'] zdvd_mult_div_cancel[OF gdvd(2)]
 	have False using b by simp }
-      hence b': "?b' < 0" by arith
+      hence b': "?b' < 0" by (auto simp add: linorder_not_le[symmetric])
       from anz bnz nz' b b' gp1 have ?thesis 
 	by (simp add: isnormNum_def normNum_def Let_def split_def fst_conv snd_conv)}
     ultimately have ?thesis by blast
diff -r 6894137e854a -r df3a7e9ebadb src/HOL/Library/Nat_Infinity.thy
--- a/src/HOL/Library/Nat_Infinity.thy	Mon Jun 11 11:06:00 2007 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy	Mon Jun 11 11:06:04 2007 +0200
@@ -51,120 +51,120 @@
 subsection "Constructors"
 
 lemma Fin_0: "Fin 0 = 0"
-  by (simp add: inat_defs split:inat_splits, arith?)
+  by (simp add: inat_defs split:inat_splits)
 
 lemma Infty_ne_i0 [simp]: "\<infinity> \<noteq> 0"
-  by (simp add: inat_defs split:inat_splits, arith?)
+  by (simp add: inat_defs split:inat_splits)
 
 lemma i0_ne_Infty [simp]: "0 \<noteq> \<infinity>"
-  by (simp add: inat_defs split:inat_splits, arith?)
+  by (simp add: inat_defs split:inat_splits)
 
 lemma iSuc_Fin [simp]: "iSuc (Fin n) = Fin (Suc n)"
-  by (simp add: inat_defs split:inat_splits, arith?)
+  by (simp add: inat_defs split:inat_splits)
 
 lemma iSuc_Infty [simp]: "iSuc \<infinity> = \<infinity>"
-  by (simp add: inat_defs split:inat_splits, arith?)
+  by (simp add: inat_defs split:inat_splits)
 
 lemma iSuc_ne_0 [simp]: "iSuc n \<noteq> 0"
-  by (simp add: inat_defs split:inat_splits, arith?)
+  by (simp add: inat_defs split:inat_splits)
 
 lemma iSuc_inject [simp]: "(iSuc x = iSuc y) = (x = y)"
-  by (simp add: inat_defs split:inat_splits, arith?)
+  by (simp add: inat_defs split:inat_splits)
 
 
 subsection "Ordering relations"
 
 lemma Infty_ilessE [elim!]: "\<infinity> < Fin m ==> R"
-  by (simp add: inat_defs split:inat_splits, arith?)
+  by (simp add: inat_defs split:inat_splits)
 
 lemma iless_linear: "m < n \<or> m = n \<or> n < (m::inat)"
-  by (simp add: inat_defs split:inat_splits, arith?)
+  by (simp add: inat_defs split:inat_splits, arith)
 
 lemma iless_not_refl [simp]: "\<not> n < (n::inat)"
-  by (simp add: inat_defs split:inat_splits, arith?)
+  by (simp add: inat_defs split:inat_splits)
 
 lemma iless_trans: "i < j ==> j < k ==> i < (k::inat)"
-  by (simp add: inat_defs split:inat_splits, arith?)
+  by (simp add: inat_defs split:inat_splits)
 
 lemma iless_not_sym: "n < m ==> \<not> m < (n::inat)"
-  by (simp add: inat_defs split:inat_splits, arith?)
+  by (simp add: inat_defs split:inat_splits)
 
 lemma Fin_iless_mono [simp]: "(Fin n < Fin m) = (n < m)"
-  by (simp add: inat_defs split:inat_splits, arith?)
+  by (simp add: inat_defs split:inat_splits)
 
 lemma Fin_iless_Infty [simp]: "Fin n < \<infinity>"
-  by (simp add: inat_defs split:inat_splits, arith?)
+  by (simp add: inat_defs split:inat_splits)
 
 lemma Infty_eq [simp]: "(n < \<infinity>) = (n \<noteq> \<infinity>)"
-  by (simp add: inat_defs split:inat_splits, arith?)
+  by (simp add: inat_defs split:inat_splits)
 
 lemma i0_eq [simp]: "((0::inat) < n) = (n \<noteq> 0)"
-  by (simp add: inat_defs split:inat_splits, arith?)
+  by (simp add: inat_defs split:inat_splits)
 
 lemma i0_iless_iSuc [simp]: "0 < iSuc n"
-  by (simp add: inat_defs split:inat_splits, arith?)
+  by (simp add: inat_defs split:inat_splits)
 
 lemma not_ilessi0 [simp]: "\<not> n < (0::inat)"
-  by (simp add: inat_defs split:inat_splits, arith?)
+  by (simp add: inat_defs split:inat_splits)
 
 lemma Fin_iless: "n < Fin m ==> \<exists>k. n = Fin k"
-  by (simp add: inat_defs split:inat_splits, arith?)
+  by (simp add: inat_defs split:inat_splits)
 
 lemma iSuc_mono [simp]: "(iSuc n < iSuc m) = (n < m)"
-  by (simp add: inat_defs split:inat_splits, arith?)
+  by (simp add: inat_defs split:inat_splits)
 
 
 
 lemma ile_def2: "(m \<le> n) = (m < n \<or> m = (n::inat))"
-  by (simp add: inat_defs split:inat_splits, arith?)
+  by (simp add: inat_defs split:inat_splits, arith)
 
 lemma ile_refl [simp]: "n \<le> (n::inat)"
-  by (simp add: inat_defs split:inat_splits, arith?)
+  by (simp add: inat_defs split:inat_splits)
 
 lemma ile_trans: "i \<le> j ==> j \<le> k ==> i \<le> (k::inat)"
-  by (simp add: inat_defs split:inat_splits, arith?)
+  by (simp add: inat_defs split:inat_splits)
 
 lemma ile_iless_trans: "i \<le> j ==> j < k ==> i < (k::inat)"
-  by (simp add: inat_defs split:inat_splits, arith?)
+  by (simp add: inat_defs split:inat_splits)
 
 lemma iless_ile_trans: "i < j ==> j \<le> k ==> i < (k::inat)"
-  by (simp add: inat_defs split:inat_splits, arith?)
+  by (simp add: inat_defs split:inat_splits)
 
 lemma Infty_ub [simp]: "n \<le> \<infinity>"
-  by (simp add: inat_defs split:inat_splits, arith?)
+  by (simp add: inat_defs split:inat_splits)
 
 lemma i0_lb [simp]: "(0::inat) \<le> n"
-  by (simp add: inat_defs split:inat_splits, arith?)
+  by (simp add: inat_defs split:inat_splits)
 
 lemma Infty_ileE [elim!]: "\<infinity> \<le> Fin m ==> R"
-  by (simp add: inat_defs split:inat_splits, arith?)
+  by (simp add: inat_defs split:inat_splits)
 
 lemma Fin_ile_mono [simp]: "(Fin n \<le> Fin m) = (n \<le> m)"
-  by (simp add: inat_defs split:inat_splits, arith?)
+  by (simp add: inat_defs split:inat_splits, arith)
 
 lemma ilessI1: "n \<le> m ==> n \<noteq> m ==> n < (m::inat)"
-  by (simp add: inat_defs split:inat_splits, arith?)
+  by (simp add: inat_defs split:inat_splits)
 
 lemma ileI1: "m < n ==> iSuc m \<le> n"
-  by (simp add: inat_defs split:inat_splits, arith?)
+  by (simp add: inat_defs split:inat_splits)
 
 lemma Suc_ile_eq: "(Fin (Suc m) \<le> n) = (Fin m < n)"
-  by (simp add: inat_defs split:inat_splits, arith?)
+  by (simp add: inat_defs split:inat_splits, arith)
 
 lemma iSuc_ile_mono [simp]: "(iSuc n \<le> iSuc m) = (n \<le> m)"
-  by (simp add: inat_defs split:inat_splits, arith?)
+  by (simp add: inat_defs split:inat_splits)
 
 lemma iless_Suc_eq [simp]: "(Fin m < iSuc n) = (Fin m \<le> n)"
-  by (simp add: inat_defs split:inat_splits, arith?)
+  by (simp add: inat_defs split:inat_splits, arith)
 
 lemma not_iSuc_ilei0 [simp]: "\<not> iSuc n \<le> 0"
-  by (simp add: inat_defs split:inat_splits, arith?)
+  by (simp add: inat_defs split:inat_splits)
 
 lemma ile_iSuc [simp]: "n \<le> iSuc n"
-  by (simp add: inat_defs split:inat_splits, arith?)
+  by (simp add: inat_defs split:inat_splits)
 
 lemma Fin_ile: "n \<le> Fin m ==> \<exists>k. n = Fin k"
-  by (simp add: inat_defs split:inat_splits, arith?)
+  by (simp add: inat_defs split:inat_splits)
 
 lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. Fin k < Y j"
   apply (induct_tac k)
diff -r 6894137e854a -r df3a7e9ebadb src/HOL/Library/SCT_Theorem.thy
--- a/src/HOL/Library/SCT_Theorem.thy	Mon Jun 11 11:06:00 2007 +0200
+++ b/src/HOL/Library/SCT_Theorem.thy	Mon Jun 11 11:06:04 2007 +0200
@@ -1023,14 +1023,16 @@
 lemma repeated_edge:
   assumes "\<And>i. i > n \<Longrightarrow> dsc (snd (p i)) k k"
   shows "is_desc_thread (\<lambda>i. k) p"
-  using prems
+proof-
+  have th: "\<forall> m. \<exists>na>m. n < na" by arith
+  show ?thesis using prems
   unfolding is_desc_thread_def 
   apply (auto)
   apply (rule_tac x="Suc n" in exI, auto)
   apply (rule INF_mono[where P="\<lambda>i. n < i"])
   apply (simp only:INF_nat)
-  by auto arith
-
+  by (auto simp add: th)
+qed
 
 lemma fin_from_inf:
   assumes "is_thread n \<theta> p"
diff -r 6894137e854a -r df3a7e9ebadb src/HOL/Matrix/MatrixGeneral.thy
--- a/src/HOL/Matrix/MatrixGeneral.thy	Mon Jun 11 11:06:00 2007 +0200
+++ b/src/HOL/Matrix/MatrixGeneral.thy	Mon Jun 11 11:06:04 2007 +0200
@@ -862,32 +862,36 @@
   by (simp add: singleton_matrix_def zero_matrix_def)
 
 lemma nrows_singleton[simp]: "nrows(singleton_matrix j i e) = (if e = 0 then 0 else Suc j)"
+proof-
+have th: "\<not> (\<forall>m. m \<le> j)" "\<exists>n. \<not> n \<le> i" by arith+
+from th show ?thesis 
 apply (auto)
 apply (rule le_anti_sym)
 apply (subst nrows_le)
 apply (simp add: singleton_matrix_def, auto)
 apply (subst RepAbs_matrix)
-apply (simp, arith)
-apply (simp, arith)
-apply (simp)
+apply auto
 apply (simp add: Suc_le_eq)
 apply (rule not_leE)
 apply (subst nrows_le)
 by simp
+qed
 
 lemma ncols_singleton[simp]: "ncols(singleton_matrix j i e) = (if e = 0 then 0 else Suc i)"
+proof-
+have th: "\<not> (\<forall>m. m \<le> j)" "\<exists>n. \<not> n \<le> i" by arith+
+from th show ?thesis 
 apply (auto)
 apply (rule le_anti_sym)
 apply (subst ncols_le)
 apply (simp add: singleton_matrix_def, auto)
 apply (subst RepAbs_matrix)
-apply (simp, arith)
-apply (simp, arith)
-apply (simp)
+apply auto
 apply (simp add: Suc_le_eq)
 apply (rule not_leE)
 apply (subst ncols_le)
 by simp
+qed
 
 lemma combine_singleton: "f 0 0 = 0 \<Longrightarrow> combine_matrix f (singleton_matrix j i a) (singleton_matrix j i b) = singleton_matrix j i (f a b)"
 apply (simp add: singleton_matrix_def combine_matrix_def combine_infmatrix_def)
diff -r 6894137e854a -r df3a7e9ebadb src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Mon Jun 11 11:06:00 2007 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Mon Jun 11 11:06:04 2007 +0200
@@ -522,7 +522,8 @@
 lemma pc_succs_shift: "pc'\<in>set (succs i (pc'' + n))
  \<Longrightarrow> ((pc' - n) \<in>set (succs i pc''))"
 apply (induct i)
-apply (arith|simp)+
+apply simp_all
+apply arith
 done
 
 
@@ -530,7 +531,8 @@
   \<forall> b. ((i = (Goto b) \<or> i=(Ifcmpeq b)) \<longrightarrow> 0 \<le> (int pc'' + b)) \<rbrakk> 
   \<Longrightarrow> n \<le> pc'"
 apply (induct i)
-apply (arith|simp)+
+apply simp_all
+apply arith
 done
 
 
diff -r 6894137e854a -r df3a7e9ebadb src/HOL/Nominal/Examples/Height.thy
--- a/src/HOL/Nominal/Examples/Height.thy	Mon Jun 11 11:06:00 2007 +0200
+++ b/src/HOL/Nominal/Examples/Height.thy	Mon Jun 11 11:06:04 2007 +0200
@@ -47,8 +47,8 @@
 
 lemma height_ge_one: 
   shows "1 \<le> (height e)"
-by (nominal_induct e rule: lam.induct) 
-   (simp | arith)+
+apply (nominal_induct e rule: lam.induct) 
+by simp_all
 
 text {* unlike the proplem suggested by Wang, however, the 
         theorem is here formulated  entirely by using 
diff -r 6894137e854a -r df3a7e9ebadb src/HOL/Nominal/Examples/LocalWeakening.thy
--- a/src/HOL/Nominal/Examples/LocalWeakening.thy	Mon Jun 11 11:06:00 2007 +0200
+++ b/src/HOL/Nominal/Examples/LocalWeakening.thy	Mon Jun 11 11:06:04 2007 +0200
@@ -178,7 +178,9 @@
   have "valid \<Gamma>2" by fact
   then have "valid ((x,T1)#\<Gamma>2)" using vc by (simp add: v2)
   ultimately have "(x,T1)#\<Gamma>2 \<turnstile> freshen t x : T2" using ih by simp
-  with vc show "\<Gamma>2 \<turnstile> lLam t : T1\<rightarrow>T2" by auto 
-qed (auto) (* app case *)
+  with vc show "\<Gamma>2 \<turnstile> lLam t : T1\<rightarrow>T2" by auto
+next 
+  case t_lApp thus ?case by auto
+qed
 
 end
diff -r 6894137e854a -r df3a7e9ebadb src/HOL/NumberTheory/Chinese.thy
--- a/src/HOL/NumberTheory/Chinese.thy	Mon Jun 11 11:06:00 2007 +0200
+++ b/src/HOL/NumberTheory/Chinese.thy	Mon Jun 11 11:06:04 2007 +0200
@@ -197,7 +197,14 @@
      apply (rule_tac [3] zdvd_zmult2)
      apply (rule_tac [4] zdvd_zmult)
      apply (rule_tac [!] funprod_zdvd)
-          apply arith+
+     apply arith
+     apply arith
+     apply arith
+     apply arith
+     apply arith
+     apply arith
+     apply arith
+     apply arith
   done
 
 lemma x_sol_lin:
diff -r 6894137e854a -r df3a7e9ebadb src/HOL/NumberTheory/Fib.thy
--- a/src/HOL/NumberTheory/Fib.thy	Mon Jun 11 11:06:00 2007 +0200
+++ b/src/HOL/NumberTheory/Fib.thy	Mon Jun 11 11:06:04 2007 +0200
@@ -67,13 +67,16 @@
  "int (fib (Suc (Suc n)) * fib n) =
   (if n mod 2 = 0 then int (fib (Suc n) * fib (Suc n)) - 1
    else int (fib (Suc n) * fib (Suc n)) + 1)"
-  apply (induct n rule: fib.induct)
-    apply (simp add: fib.Suc_Suc)
-   apply (simp add: fib.Suc_Suc mod_Suc)
-  apply (simp add: fib.Suc_Suc add_mult_distrib add_mult_distrib2
+proof(induct n rule: fib.induct)
+  case 1 thus ?case by (simp add: fib.Suc_Suc)
+next
+  case 2 thus ?case by (simp add: fib.Suc_Suc mod_Suc)
+next 
+  case (3 x) 
+  have th: "Suc 0 \<noteq> x mod 2 \<longrightarrow> x mod 2 = 0" by presburger
+  with prems show ?case by (simp add: fib.Suc_Suc add_mult_distrib add_mult_distrib2
                    mod_Suc zmult_int [symmetric])
-  apply (presburger (no_abs))
-  done
+qed
 
 text{*We now obtain a version for the natural numbers via the coercion 
    function @{term int}.*}
diff -r 6894137e854a -r df3a7e9ebadb src/HOL/NumberTheory/Int2.thy
--- a/src/HOL/NumberTheory/Int2.thy	Mon Jun 11 11:06:00 2007 +0200
+++ b/src/HOL/NumberTheory/Int2.thy	Mon Jun 11 11:06:04 2007 +0200
@@ -45,10 +45,10 @@
 
 lemma div_prop1: "[| 0 < z; (x::int) < y * z |] ==> x div z < y"
 proof -
-  assume "0 < z"
-  then have "(x div z) * z \<le> (x div z) * z + x mod z"
-    by arith
-  also have "... = x"
+  assume "0 < z" then have modth: "x mod z \<ge> 0" by simp
+  have "(x div z) * z \<le> (x div z) * z" by simp
+  then have "(x div z) * z \<le> (x div z) * z + x mod z" using modth by arith 
+  also have "\<dots> = x"
     by (auto simp add: zmod_zdiv_equality [symmetric] zmult_ac)
   also assume  "x < y * z"
   finally show ?thesis
diff -r 6894137e854a -r df3a7e9ebadb src/HOL/Real/Float.thy
--- a/src/HOL/Real/Float.thy	Mon Jun 11 11:06:00 2007 +0200
+++ b/src/HOL/Real/Float.thy	Mon Jun 11 11:06:04 2007 +0200
@@ -293,7 +293,7 @@
 ML {* simp_depth_limit := 2 *}
 recdef norm_float "measure (% (a,b). nat (abs a))"
   "norm_float (a,b) = (if (a \<noteq> 0) & (even a) then norm_float (a div 2, b+1) else (if a=0 then (0,0) else (a,b)))"
-(hints simp: terminating_norm_float)
+(hints simp: even_def terminating_norm_float)
 ML {* simp_depth_limit := 1000 *}
 
 lemma norm_float: "float x = float (norm_float x)"
diff -r 6894137e854a -r df3a7e9ebadb src/HOL/ZF/HOLZF.thy
--- a/src/HOL/ZF/HOLZF.thy	Mon Jun 11 11:06:00 2007 +0200
+++ b/src/HOL/ZF/HOLZF.thy	Mon Jun 11 11:06:04 2007 +0200
@@ -601,18 +601,25 @@
     ultimately have "False" using u by arith
   }
   note lemma_nat2Nat = this
+  have th:"\<And>x y. \<not> (x < y \<and> (\<forall>(m\<Colon>nat). y \<noteq> x + m))" by presburger
+  have th': "\<And>x y. \<not> (x \<noteq> y \<and> (\<not> x < y) \<and> (\<forall>(m\<Colon>nat). x \<noteq> y + m))" by presburger
   show ?thesis
     apply (auto simp add: inj_on_def)
     apply (case_tac "x = y")
     apply auto
     apply (case_tac "x < y")
     apply (case_tac "? m. y = x + m & 0 < m")
-    apply (auto intro: lemma_nat2Nat, arith)
+    apply (auto intro: lemma_nat2Nat)
     apply (case_tac "y < x")
     apply (case_tac "? m. x = y + m & 0 < m")
-    apply auto
+    apply simp
+    apply simp
+    using th apply blast
+    apply (case_tac "? m. x = y + m")
+    apply (auto intro: lemma_nat2Nat)
     apply (drule sym)
-    apply (auto intro: lemma_nat2Nat, arith)
+    using lemma_nat2Nat apply blast
+    using th' apply blast    
     done
 qed
 
diff -r 6894137e854a -r df3a7e9ebadb src/HOL/ex/Fundefs.thy
--- a/src/HOL/ex/Fundefs.thy	Mon Jun 11 11:06:00 2007 +0200
+++ b/src/HOL/ex/Fundefs.thy	Mon Jun 11 11:06:04 2007 +0200
@@ -149,7 +149,7 @@
     with divmod have "x = 2 * (x div 2) + 1" by simp
     with c2 show "P" .
   qed
-qed presburger+ -- {* solve compatibility with presburger *}
+qed presburger+ -- {* solve compatibility with presburger *} 
 termination by lexicographic_order
 
 thm ev.simps
diff -r 6894137e854a -r df3a7e9ebadb src/HOL/ex/Reflected_Presburger.thy
--- a/src/HOL/ex/Reflected_Presburger.thy	Mon Jun 11 11:06:00 2007 +0200
+++ b/src/HOL/ex/Reflected_Presburger.thy	Mon Jun 11 11:06:04 2007 +0200
@@ -46,13 +46,16 @@
   by auto
 
 (* Periodicity of dvd *)
+
 lemma dvd_period:
   assumes advdd: "(a::int) dvd d"
   shows "(a dvd (x + t)) = (a dvd ((x+ c*d) + t))"
   using advdd  
 proof-
-  from advdd  have "\<forall>x.\<forall>k. (((a::int) dvd (x + t)) = (a dvd (x+k*d + t)))" 
-    by (rule dvd_modd_pinf)
+  {fix x k
+    from inf_period(3)[OF advdd, rule_format, where x=x and k="-k"]  
+    have " ((a::int) dvd (x + t)) = (a dvd (x+k*d + t))" by simp}
+  hence "\<forall>x.\<forall>k. ((a::int) dvd (x + t)) = (a dvd (x+k*d + t))"  by simp
   then show ?thesis by simp
 qed
 
@@ -637,7 +640,8 @@
   moreover 
   {assume i1: "abs i = 1"
       from zdvd_1_left[where m = "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"]
-      have ?case using i1 by (cases "i=0", simp_all add: Let_def) arith}
+      have ?case using i1 apply (cases "i=0", simp_all add: Let_def) 
+	by (cases "i > 0", simp_all)}
   moreover   
   {assume inz: "i\<noteq>0" and cond: "abs i \<noteq> 1"
     {fix v assume "?sa = C v" hence ?case using sa[symmetric] inz cond
@@ -656,7 +660,8 @@
   moreover 
   {assume i1: "abs i = 1"
       from zdvd_1_left[where m = "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"]
-      have ?case using i1 by (cases "i=0", simp_all add: Let_def) arith}
+      have ?case using i1 apply (cases "i=0", simp_all add: Let_def)
+      apply (cases "i > 0", simp_all) done}
   moreover   
   {assume inz: "i\<noteq>0" and cond: "abs i \<noteq> 1"
     {fix v assume "?sa = C v" hence ?case using sa[symmetric] inz cond
@@ -727,12 +732,6 @@
 by(induct p rule: qelim.induct) 
 (auto simp add: not disj conj iff imp not_qf disj_qf conj_qf imp_qf iff_qf 
   simpfm simpfm_qf simp del: simpfm.simps)
-
-
-
-    (**********************************************************************************)
-    (*******                             THE \<int>-PART                                 ***)
-    (**********************************************************************************)
   (* Linearity for fm where Bound 0 ranges over \<int> *)
 consts
   zsplit0 :: "num \<Rightarrow> int \<times> num" (* splits the bounded from the unbounded part*)
@@ -1335,7 +1334,7 @@
   from \<delta> [OF lin] have dpos: "?d >0" by simp
   from \<delta> [OF lin] have alld: "d\<delta> p ?d" by simp
   from minusinf_repeats[OF alld lin] have th1:"\<forall> x k. ?P x = ?P (x - (k * ?d))" by simp
-  from minf_vee[OF dpos th1] show ?thesis by blast
+  from periodic_finite_ex[OF dpos th1] show ?thesis by blast
 qed
 
 
@@ -1690,6 +1689,27 @@
     by auto
   from  \<beta>[OF lp u d dp nb2 px] show "?P (x -d )" .
 qed
+lemma cpmi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. x < z --> (P x = P1 x))
+==> ALL x.~(EX (j::int) : {1..D}. EX (b::int) : B. P(b+j)) --> P (x) --> P (x - D) 
+==> (ALL (x::int). ALL (k::int). ((P1 x)= (P1 (x-k*D))))
+==> (EX (x::int). P(x)) = ((EX (j::int) : {1..D} . (P1(j))) | (EX (j::int) : {1..D}. EX (b::int) : B. P (b+j)))"
+apply(rule iffI)
+prefer 2
+apply(drule minusinfinity)
+apply assumption+
+apply(fastsimp)
+apply clarsimp
+apply(subgoal_tac "!!k. 0<=k \<Longrightarrow> !x. P x \<longrightarrow> P (x - k*D)")
+apply(frule_tac x = x and z=z in decr_lemma)
+apply(subgoal_tac "P1(x - (\<bar>x - z\<bar> + 1) * D)")
+prefer 2
+apply(subgoal_tac "0 <= (\<bar>x - z\<bar> + 1)")
+prefer 2 apply arith
+ apply fastsimp
+apply(drule (1)  periodic_finite_ex)
+apply blast
+apply(blast dest:decr_mult_lemma)
+done
 
 theorem cp_thm:
   assumes lp: "iszlfm p"
@@ -1880,8 +1900,8 @@
 
 theorem mirqe: "(Ifm bbs bs (pa p) = Ifm bbs bs p) \<and> qfree (pa p)"
   using qelim_ci cooper prep by (auto simp add: pa_def)
+declare zdvd_iff_zmod_eq_0 [code]
 
-declare zdvd_iff_zmod_eq_0 [code] 
 code_module GeneratedCooper
 file "generated_cooper.ML"
 contains pa = "pa"