--- 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
--- 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"
--- 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 []) =
--- 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
--- 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)
--- 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"
--- 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)
--- 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
--- 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
--- 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
--- 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:
--- 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}.*}
--- 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
--- 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)"
--- 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
--- 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
--- 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"