1979 | "\<delta> (Or p q) = lcm (\<delta> p) (\<delta> q)" |
1979 | "\<delta> (Or p q) = lcm (\<delta> p) (\<delta> q)" |
1980 | "\<delta> (Dvd i (CN 0 c e)) = i" |
1980 | "\<delta> (Dvd i (CN 0 c e)) = i" |
1981 | "\<delta> (NDvd i (CN 0 c e)) = i" |
1981 | "\<delta> (NDvd i (CN 0 c e)) = i" |
1982 | "\<delta> p = 1" |
1982 | "\<delta> p = 1" |
1983 |
1983 |
1984 fun d\<delta> :: "fm \<Rightarrow> int \<Rightarrow> bool" where |
1984 fun d_\<delta> :: "fm \<Rightarrow> int \<Rightarrow> bool" where |
1985 "d\<delta> (And p q) = (\<lambda> d. d\<delta> p d \<and> d\<delta> q d)" |
1985 "d_\<delta> (And p q) = (\<lambda> d. d_\<delta> p d \<and> d_\<delta> q d)" |
1986 | "d\<delta> (Or p q) = (\<lambda> d. d\<delta> p d \<and> d\<delta> q d)" |
1986 | "d_\<delta> (Or p q) = (\<lambda> d. d_\<delta> p d \<and> d_\<delta> q d)" |
1987 | "d\<delta> (Dvd i (CN 0 c e)) = (\<lambda> d. i dvd d)" |
1987 | "d_\<delta> (Dvd i (CN 0 c e)) = (\<lambda> d. i dvd d)" |
1988 | "d\<delta> (NDvd i (CN 0 c e)) = (\<lambda> d. i dvd d)" |
1988 | "d_\<delta> (NDvd i (CN 0 c e)) = (\<lambda> d. i dvd d)" |
1989 | "d\<delta> p = (\<lambda> d. True)" |
1989 | "d_\<delta> p = (\<lambda> d. True)" |
1990 |
1990 |
1991 lemma delta_mono: |
1991 lemma delta_mono: |
1992 assumes lin: "iszlfm p bs" |
1992 assumes lin: "iszlfm p bs" |
1993 and d: "d dvd d'" |
1993 and d: "d dvd d'" |
1994 and ad: "d\<delta> p d" |
1994 and ad: "d_\<delta> p d" |
1995 shows "d\<delta> p d'" |
1995 shows "d_\<delta> p d'" |
1996 using lin ad d |
1996 using lin ad d |
1997 proof(induct p rule: iszlfm.induct) |
1997 proof(induct p rule: iszlfm.induct) |
1998 case (9 i c e) thus ?case using d |
1998 case (9 i c e) thus ?case using d |
1999 by (simp add: dvd_trans[of "i" "d" "d'"]) |
1999 by (simp add: dvd_trans[of "i" "d" "d'"]) |
2000 next |
2000 next |
2001 case (10 i c e) thus ?case using d |
2001 case (10 i c e) thus ?case using d |
2002 by (simp add: dvd_trans[of "i" "d" "d'"]) |
2002 by (simp add: dvd_trans[of "i" "d" "d'"]) |
2003 qed simp_all |
2003 qed simp_all |
2004 |
2004 |
2005 lemma \<delta> : assumes lin:"iszlfm p bs" |
2005 lemma \<delta> : assumes lin:"iszlfm p bs" |
2006 shows "d\<delta> p (\<delta> p) \<and> \<delta> p >0" |
2006 shows "d_\<delta> p (\<delta> p) \<and> \<delta> p >0" |
2007 using lin |
2007 using lin |
2008 proof (induct p rule: iszlfm.induct) |
2008 proof (induct p rule: iszlfm.induct) |
2009 case (1 p q) |
2009 case (1 p q) |
2010 let ?d = "\<delta> (And p q)" |
2010 let ?d = "\<delta> (And p q)" |
2011 from 1 lcm_pos_int have dp: "?d >0" by simp |
2011 from 1 lcm_pos_int have dp: "?d >0" by simp |
2012 have d1: "\<delta> p dvd \<delta> (And p q)" using 1 by simp |
2012 have d1: "\<delta> p dvd \<delta> (And p q)" using 1 by simp |
2013 hence th: "d\<delta> p ?d" |
2013 hence th: "d_\<delta> p ?d" |
2014 using delta_mono 1 by (simp only: iszlfm.simps) blast |
2014 using delta_mono 1 by (simp only: iszlfm.simps) blast |
2015 have "\<delta> q dvd \<delta> (And p q)" using 1 by simp |
2015 have "\<delta> q dvd \<delta> (And p q)" using 1 by simp |
2016 hence th': "d\<delta> q ?d" using delta_mono 1 by (simp only: iszlfm.simps) blast |
2016 hence th': "d_\<delta> q ?d" using delta_mono 1 by (simp only: iszlfm.simps) blast |
2017 from th th' dp show ?case by simp |
2017 from th th' dp show ?case by simp |
2018 next |
2018 next |
2019 case (2 p q) |
2019 case (2 p q) |
2020 let ?d = "\<delta> (And p q)" |
2020 let ?d = "\<delta> (And p q)" |
2021 from 2 lcm_pos_int have dp: "?d >0" by simp |
2021 from 2 lcm_pos_int have dp: "?d >0" by simp |
2022 have "\<delta> p dvd \<delta> (And p q)" using 2 by simp |
2022 have "\<delta> p dvd \<delta> (And p q)" using 2 by simp |
2023 hence th: "d\<delta> p ?d" using delta_mono 2 by (simp only: iszlfm.simps) blast |
2023 hence th: "d_\<delta> p ?d" using delta_mono 2 by (simp only: iszlfm.simps) blast |
2024 have "\<delta> q dvd \<delta> (And p q)" using 2 by simp |
2024 have "\<delta> q dvd \<delta> (And p q)" using 2 by simp |
2025 hence th': "d\<delta> q ?d" using delta_mono 2 by (simp only: iszlfm.simps) blast |
2025 hence th': "d_\<delta> q ?d" using delta_mono 2 by (simp only: iszlfm.simps) blast |
2026 from th th' dp show ?case by simp |
2026 from th th' dp show ?case by simp |
2027 qed simp_all |
2027 qed simp_all |
2028 |
2028 |
2029 |
2029 |
2030 lemma minusinf_inf: |
2030 lemma minusinf_inf: |
2230 (\<exists> (x::int)\<in> {1..\<delta> p}. Ifm (real x#bs) (minusinf p))" |
2230 (\<exists> (x::int)\<in> {1..\<delta> p}. Ifm (real x#bs) (minusinf p))" |
2231 (is "(\<exists> x. ?P x) = _") |
2231 (is "(\<exists> x. ?P x) = _") |
2232 proof- |
2232 proof- |
2233 let ?d = "\<delta> p" |
2233 let ?d = "\<delta> p" |
2234 from \<delta> [OF lin] have dpos: "?d >0" by simp |
2234 from \<delta> [OF lin] have dpos: "?d >0" by simp |
2235 from \<delta> [OF lin] have alld: "d\<delta> p ?d" by simp |
2235 from \<delta> [OF lin] have alld: "d_\<delta> p ?d" by simp |
2236 from minusinf_repeats[OF alld lin] have th1:"\<forall> x k. ?P x = ?P (x - (k * ?d))" by simp |
2236 from minusinf_repeats[OF alld lin] have th1:"\<forall> x k. ?P x = ?P (x - (k * ?d))" by simp |
2237 from periodic_finite_ex[OF dpos th1] show ?thesis by blast |
2237 from periodic_finite_ex[OF dpos th1] show ?thesis by blast |
2238 qed |
2238 qed |
2239 |
2239 |
2240 lemma dvd1_eq1: "x >0 \<Longrightarrow> (x::int) dvd 1 = (x = 1)" by auto |
2240 lemma dvd1_eq1: "x >0 \<Longrightarrow> (x::int) dvd 1 = (x = 1)" by auto |
2241 |
2241 |
2242 consts |
2242 consts |
2243 a\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm" (* adjusts the coeffitients of a formula *) |
2243 a_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm" (* adjusts the coeffitients of a formula *) |
2244 d\<beta> :: "fm \<Rightarrow> int \<Rightarrow> bool" (* tests if all coeffs c of c divide a given l*) |
2244 d_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> bool" (* tests if all coeffs c of c divide a given l*) |
2245 \<zeta> :: "fm \<Rightarrow> int" (* computes the lcm of all coefficients of x*) |
2245 \<zeta> :: "fm \<Rightarrow> int" (* computes the lcm of all coefficients of x*) |
2246 \<beta> :: "fm \<Rightarrow> num list" |
2246 \<beta> :: "fm \<Rightarrow> num list" |
2247 \<alpha> :: "fm \<Rightarrow> num list" |
2247 \<alpha> :: "fm \<Rightarrow> num list" |
2248 |
2248 |
2249 recdef a\<beta> "measure size" |
2249 recdef a_\<beta> "measure size" |
2250 "a\<beta> (And p q) = (\<lambda> k. And (a\<beta> p k) (a\<beta> q k))" |
2250 "a_\<beta> (And p q) = (\<lambda> k. And (a_\<beta> p k) (a_\<beta> q k))" |
2251 "a\<beta> (Or p q) = (\<lambda> k. Or (a\<beta> p k) (a\<beta> q k))" |
2251 "a_\<beta> (Or p q) = (\<lambda> k. Or (a_\<beta> p k) (a_\<beta> q k))" |
2252 "a\<beta> (Eq (CN 0 c e)) = (\<lambda> k. Eq (CN 0 1 (Mul (k div c) e)))" |
2252 "a_\<beta> (Eq (CN 0 c e)) = (\<lambda> k. Eq (CN 0 1 (Mul (k div c) e)))" |
2253 "a\<beta> (NEq (CN 0 c e)) = (\<lambda> k. NEq (CN 0 1 (Mul (k div c) e)))" |
2253 "a_\<beta> (NEq (CN 0 c e)) = (\<lambda> k. NEq (CN 0 1 (Mul (k div c) e)))" |
2254 "a\<beta> (Lt (CN 0 c e)) = (\<lambda> k. Lt (CN 0 1 (Mul (k div c) e)))" |
2254 "a_\<beta> (Lt (CN 0 c e)) = (\<lambda> k. Lt (CN 0 1 (Mul (k div c) e)))" |
2255 "a\<beta> (Le (CN 0 c e)) = (\<lambda> k. Le (CN 0 1 (Mul (k div c) e)))" |
2255 "a_\<beta> (Le (CN 0 c e)) = (\<lambda> k. Le (CN 0 1 (Mul (k div c) e)))" |
2256 "a\<beta> (Gt (CN 0 c e)) = (\<lambda> k. Gt (CN 0 1 (Mul (k div c) e)))" |
2256 "a_\<beta> (Gt (CN 0 c e)) = (\<lambda> k. Gt (CN 0 1 (Mul (k div c) e)))" |
2257 "a\<beta> (Ge (CN 0 c e)) = (\<lambda> k. Ge (CN 0 1 (Mul (k div c) e)))" |
2257 "a_\<beta> (Ge (CN 0 c e)) = (\<lambda> k. Ge (CN 0 1 (Mul (k div c) e)))" |
2258 "a\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. Dvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))" |
2258 "a_\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. Dvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))" |
2259 "a\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. NDvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))" |
2259 "a_\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. NDvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))" |
2260 "a\<beta> p = (\<lambda> k. p)" |
2260 "a_\<beta> p = (\<lambda> k. p)" |
2261 |
2261 |
2262 recdef d\<beta> "measure size" |
2262 recdef d_\<beta> "measure size" |
2263 "d\<beta> (And p q) = (\<lambda> k. (d\<beta> p k) \<and> (d\<beta> q k))" |
2263 "d_\<beta> (And p q) = (\<lambda> k. (d_\<beta> p k) \<and> (d_\<beta> q k))" |
2264 "d\<beta> (Or p q) = (\<lambda> k. (d\<beta> p k) \<and> (d\<beta> q k))" |
2264 "d_\<beta> (Or p q) = (\<lambda> k. (d_\<beta> p k) \<and> (d_\<beta> q k))" |
2265 "d\<beta> (Eq (CN 0 c e)) = (\<lambda> k. c dvd k)" |
2265 "d_\<beta> (Eq (CN 0 c e)) = (\<lambda> k. c dvd k)" |
2266 "d\<beta> (NEq (CN 0 c e)) = (\<lambda> k. c dvd k)" |
2266 "d_\<beta> (NEq (CN 0 c e)) = (\<lambda> k. c dvd k)" |
2267 "d\<beta> (Lt (CN 0 c e)) = (\<lambda> k. c dvd k)" |
2267 "d_\<beta> (Lt (CN 0 c e)) = (\<lambda> k. c dvd k)" |
2268 "d\<beta> (Le (CN 0 c e)) = (\<lambda> k. c dvd k)" |
2268 "d_\<beta> (Le (CN 0 c e)) = (\<lambda> k. c dvd k)" |
2269 "d\<beta> (Gt (CN 0 c e)) = (\<lambda> k. c dvd k)" |
2269 "d_\<beta> (Gt (CN 0 c e)) = (\<lambda> k. c dvd k)" |
2270 "d\<beta> (Ge (CN 0 c e)) = (\<lambda> k. c dvd k)" |
2270 "d_\<beta> (Ge (CN 0 c e)) = (\<lambda> k. c dvd k)" |
2271 "d\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. c dvd k)" |
2271 "d_\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. c dvd k)" |
2272 "d\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. c dvd k)" |
2272 "d_\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. c dvd k)" |
2273 "d\<beta> p = (\<lambda> k. True)" |
2273 "d_\<beta> p = (\<lambda> k. True)" |
2274 |
2274 |
2275 recdef \<zeta> "measure size" |
2275 recdef \<zeta> "measure size" |
2276 "\<zeta> (And p q) = lcm (\<zeta> p) (\<zeta> q)" |
2276 "\<zeta> (And p q) = lcm (\<zeta> p) (\<zeta> q)" |
2277 "\<zeta> (Or p q) = lcm (\<zeta> p) (\<zeta> q)" |
2277 "\<zeta> (Or p q) = lcm (\<zeta> p) (\<zeta> q)" |
2278 "\<zeta> (Eq (CN 0 c e)) = c" |
2278 "\<zeta> (Eq (CN 0 c e)) = c" |
2374 |
2374 |
2375 lemma \<beta>_numbound0: assumes lp: "iszlfm p bs" |
2375 lemma \<beta>_numbound0: assumes lp: "iszlfm p bs" |
2376 shows "\<forall> b\<in> set (\<beta> p). numbound0 b" |
2376 shows "\<forall> b\<in> set (\<beta> p). numbound0 b" |
2377 using lp by (induct p rule: \<beta>.induct,auto) |
2377 using lp by (induct p rule: \<beta>.induct,auto) |
2378 |
2378 |
2379 lemma d\<beta>_mono: |
2379 lemma d_\<beta>_mono: |
2380 assumes linp: "iszlfm p (a #bs)" |
2380 assumes linp: "iszlfm p (a #bs)" |
2381 and dr: "d\<beta> p l" |
2381 and dr: "d_\<beta> p l" |
2382 and d: "l dvd l'" |
2382 and d: "l dvd l'" |
2383 shows "d\<beta> p l'" |
2383 shows "d_\<beta> p l'" |
2384 using dr linp dvd_trans[of _ "l" "l'", simplified d] |
2384 using dr linp dvd_trans[of _ "l" "l'", simplified d] |
2385 by (induct p rule: iszlfm.induct) simp_all |
2385 by (induct p rule: iszlfm.induct) simp_all |
2386 |
2386 |
2387 lemma \<alpha>_l: assumes lp: "iszlfm p (a#bs)" |
2387 lemma \<alpha>_l: assumes lp: "iszlfm p (a#bs)" |
2388 shows "\<forall> b\<in> set (\<alpha> p). numbound0 b \<and> isint b (a#bs)" |
2388 shows "\<forall> b\<in> set (\<alpha> p). numbound0 b \<and> isint b (a#bs)" |
2389 using lp |
2389 using lp |
2390 by(induct p rule: \<alpha>.induct, auto simp add: isint_add isint_c) |
2390 by(induct p rule: \<alpha>.induct, auto simp add: isint_add isint_c) |
2391 |
2391 |
2392 lemma \<zeta>: |
2392 lemma \<zeta>: |
2393 assumes linp: "iszlfm p (a #bs)" |
2393 assumes linp: "iszlfm p (a #bs)" |
2394 shows "\<zeta> p > 0 \<and> d\<beta> p (\<zeta> p)" |
2394 shows "\<zeta> p > 0 \<and> d_\<beta> p (\<zeta> p)" |
2395 using linp |
2395 using linp |
2396 proof(induct p rule: iszlfm.induct) |
2396 proof(induct p rule: iszlfm.induct) |
2397 case (1 p q) |
2397 case (1 p q) |
2398 then have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp |
2398 then have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp |
2399 from 1 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp |
2399 from 1 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp |
2400 from 1 d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] |
2400 from 1 d_\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] |
2401 d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"] |
2401 d_\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"] |
2402 dl1 dl2 show ?case by (auto simp add: lcm_pos_int) |
2402 dl1 dl2 show ?case by (auto simp add: lcm_pos_int) |
2403 next |
2403 next |
2404 case (2 p q) |
2404 case (2 p q) |
2405 then have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp |
2405 then have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp |
2406 from 2 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp |
2406 from 2 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp |
2407 from 2 d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] |
2407 from 2 d_\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] |
2408 d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"] |
2408 d_\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"] |
2409 dl1 dl2 show ?case by (auto simp add: lcm_pos_int) |
2409 dl1 dl2 show ?case by (auto simp add: lcm_pos_int) |
2410 qed (auto simp add: lcm_pos_int) |
2410 qed (auto simp add: lcm_pos_int) |
2411 |
2411 |
2412 lemma a\<beta>: assumes linp: "iszlfm p (a #bs)" and d: "d\<beta> p l" and lp: "l > 0" |
2412 lemma a_\<beta>: assumes linp: "iszlfm p (a #bs)" and d: "d_\<beta> p l" and lp: "l > 0" |
2413 shows "iszlfm (a\<beta> p l) (a #bs) \<and> d\<beta> (a\<beta> p l) 1 \<and> (Ifm (real (l * x) #bs) (a\<beta> p l) = Ifm ((real x)#bs) p)" |
2413 shows "iszlfm (a_\<beta> p l) (a #bs) \<and> d_\<beta> (a_\<beta> p l) 1 \<and> (Ifm (real (l * x) #bs) (a_\<beta> p l) = Ifm ((real x)#bs) p)" |
2414 using linp d |
2414 using linp d |
2415 proof (induct p rule: iszlfm.induct) |
2415 proof (induct p rule: iszlfm.induct) |
2416 case (5 c e) hence cp: "c>0" and be: "numbound0 e" and ei:"isint e (a#bs)" and d': "c dvd l" by simp+ |
2416 case (5 c e) hence cp: "c>0" and be: "numbound0 e" and ei:"isint e (a#bs)" and d': "c dvd l" by simp+ |
2417 from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
2417 from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
2418 from cp have cnz: "c \<noteq> 0" by simp |
2418 from cp have cnz: "c \<noteq> 0" by simp |
2554 using zero_le_mult_iff [where a="real (l div c)" and b="real c * real x + Inum (real x # bs) e - real j * real k"] ldcp by simp |
2554 using zero_le_mult_iff [where a="real (l div c)" and b="real c * real x + Inum (real x # bs) e - real j * real k"] ldcp by simp |
2555 also have "\<dots> = (\<exists> (k::int). real c * real x + Inum (real x # bs) e = real j * real k)" by simp |
2555 also have "\<dots> = (\<exists> (k::int). real c * real x + Inum (real x # bs) e = real j * real k)" by simp |
2556 finally show ?case using numbound0_I[OF be,where b="real (l * x)" and b'="real x" and bs="bs"] rdvd_def be isint_Mul[OF ei] mult_strict_mono[OF ldcp jp ldcp ] by simp |
2556 finally show ?case using numbound0_I[OF be,where b="real (l * x)" and b'="real x" and bs="bs"] rdvd_def be isint_Mul[OF ei] mult_strict_mono[OF ldcp jp ldcp ] by simp |
2557 qed (simp_all add: numbound0_I[where bs="bs" and b="real (l * x)" and b'="real x"] isint_Mul del: real_of_int_mult) |
2557 qed (simp_all add: numbound0_I[where bs="bs" and b="real (l * x)" and b'="real x"] isint_Mul del: real_of_int_mult) |
2558 |
2558 |
2559 lemma a\<beta>_ex: assumes linp: "iszlfm p (a#bs)" and d: "d\<beta> p l" and lp: "l>0" |
2559 lemma a_\<beta>_ex: assumes linp: "iszlfm p (a#bs)" and d: "d_\<beta> p l" and lp: "l>0" |
2560 shows "(\<exists> x. l dvd x \<and> Ifm (real x #bs) (a\<beta> p l)) = (\<exists> (x::int). Ifm (real x#bs) p)" |
2560 shows "(\<exists> x. l dvd x \<and> Ifm (real x #bs) (a_\<beta> p l)) = (\<exists> (x::int). Ifm (real x#bs) p)" |
2561 (is "(\<exists> x. l dvd x \<and> ?P x) = (\<exists> x. ?P' x)") |
2561 (is "(\<exists> x. l dvd x \<and> ?P x) = (\<exists> x. ?P' x)") |
2562 proof- |
2562 proof- |
2563 have "(\<exists> x. l dvd x \<and> ?P x) = (\<exists> (x::int). ?P (l*x))" |
2563 have "(\<exists> x. l dvd x \<and> ?P x) = (\<exists> (x::int). ?P (l*x))" |
2564 using unity_coeff_ex[where l="l" and P="?P", simplified] by simp |
2564 using unity_coeff_ex[where l="l" and P="?P", simplified] by simp |
2565 also have "\<dots> = (\<exists> (x::int). ?P' x)" using a\<beta>[OF linp d lp] by simp |
2565 also have "\<dots> = (\<exists> (x::int). ?P' x)" using a_\<beta>[OF linp d lp] by simp |
2566 finally show ?thesis . |
2566 finally show ?thesis . |
2567 qed |
2567 qed |
2568 |
2568 |
2569 lemma \<beta>: |
2569 lemma \<beta>: |
2570 assumes lp: "iszlfm p (a#bs)" |
2570 assumes lp: "iszlfm p (a#bs)" |
2571 and u: "d\<beta> p 1" |
2571 and u: "d_\<beta> p 1" |
2572 and d: "d\<delta> p d" |
2572 and d: "d_\<delta> p d" |
2573 and dp: "d > 0" |
2573 and dp: "d > 0" |
2574 and nob: "\<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists> b\<in> (Inum (a#bs)) ` set(\<beta> p). real x = b + real j)" |
2574 and nob: "\<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists> b\<in> (Inum (a#bs)) ` set(\<beta> p). real x = b + real j)" |
2575 and p: "Ifm (real x#bs) p" (is "?P x") |
2575 and p: "Ifm (real x#bs) p" (is "?P x") |
2576 shows "?P (x - d)" |
2576 shows "?P (x - d)" |
2577 using lp u d dp nob p |
2577 using lp u d dp nob p |
2787 "\<rho> (Le (CN 0 c e)) = []" |
2787 "\<rho> (Le (CN 0 c e)) = []" |
2788 "\<rho> (Gt (CN 0 c e)) = [(Neg e, c)]" |
2788 "\<rho> (Gt (CN 0 c e)) = [(Neg e, c)]" |
2789 "\<rho> (Ge (CN 0 c e)) = [(Sub (C (-1)) e, c)]" |
2789 "\<rho> (Ge (CN 0 c e)) = [(Sub (C (-1)) e, c)]" |
2790 "\<rho> p = []" |
2790 "\<rho> p = []" |
2791 |
2791 |
2792 recdef \<sigma>\<rho> "measure size" |
2792 recdef \<sigma>_\<rho> "measure size" |
2793 "\<sigma>\<rho> (And p q) = (\<lambda> (t,k). And (\<sigma>\<rho> p (t,k)) (\<sigma>\<rho> q (t,k)))" |
2793 "\<sigma>_\<rho> (And p q) = (\<lambda> (t,k). And (\<sigma>_\<rho> p (t,k)) (\<sigma>_\<rho> q (t,k)))" |
2794 "\<sigma>\<rho> (Or p q) = (\<lambda> (t,k). Or (\<sigma>\<rho> p (t,k)) (\<sigma>\<rho> q (t,k)))" |
2794 "\<sigma>_\<rho> (Or p q) = (\<lambda> (t,k). Or (\<sigma>_\<rho> p (t,k)) (\<sigma>_\<rho> q (t,k)))" |
2795 "\<sigma>\<rho> (Eq (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Eq (Add (Mul (c div k) t) e)) |
2795 "\<sigma>_\<rho> (Eq (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Eq (Add (Mul (c div k) t) e)) |
2796 else (Eq (Add (Mul c t) (Mul k e))))" |
2796 else (Eq (Add (Mul c t) (Mul k e))))" |
2797 "\<sigma>\<rho> (NEq (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (NEq (Add (Mul (c div k) t) e)) |
2797 "\<sigma>_\<rho> (NEq (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (NEq (Add (Mul (c div k) t) e)) |
2798 else (NEq (Add (Mul c t) (Mul k e))))" |
2798 else (NEq (Add (Mul c t) (Mul k e))))" |
2799 "\<sigma>\<rho> (Lt (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Lt (Add (Mul (c div k) t) e)) |
2799 "\<sigma>_\<rho> (Lt (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Lt (Add (Mul (c div k) t) e)) |
2800 else (Lt (Add (Mul c t) (Mul k e))))" |
2800 else (Lt (Add (Mul c t) (Mul k e))))" |
2801 "\<sigma>\<rho> (Le (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Le (Add (Mul (c div k) t) e)) |
2801 "\<sigma>_\<rho> (Le (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Le (Add (Mul (c div k) t) e)) |
2802 else (Le (Add (Mul c t) (Mul k e))))" |
2802 else (Le (Add (Mul c t) (Mul k e))))" |
2803 "\<sigma>\<rho> (Gt (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Gt (Add (Mul (c div k) t) e)) |
2803 "\<sigma>_\<rho> (Gt (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Gt (Add (Mul (c div k) t) e)) |
2804 else (Gt (Add (Mul c t) (Mul k e))))" |
2804 else (Gt (Add (Mul c t) (Mul k e))))" |
2805 "\<sigma>\<rho> (Ge (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Ge (Add (Mul (c div k) t) e)) |
2805 "\<sigma>_\<rho> (Ge (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Ge (Add (Mul (c div k) t) e)) |
2806 else (Ge (Add (Mul c t) (Mul k e))))" |
2806 else (Ge (Add (Mul c t) (Mul k e))))" |
2807 "\<sigma>\<rho> (Dvd i (CN 0 c e)) =(\<lambda> (t,k). if k dvd c then (Dvd i (Add (Mul (c div k) t) e)) |
2807 "\<sigma>_\<rho> (Dvd i (CN 0 c e)) =(\<lambda> (t,k). if k dvd c then (Dvd i (Add (Mul (c div k) t) e)) |
2808 else (Dvd (i*k) (Add (Mul c t) (Mul k e))))" |
2808 else (Dvd (i*k) (Add (Mul c t) (Mul k e))))" |
2809 "\<sigma>\<rho> (NDvd i (CN 0 c e))=(\<lambda> (t,k). if k dvd c then (NDvd i (Add (Mul (c div k) t) e)) |
2809 "\<sigma>_\<rho> (NDvd i (CN 0 c e))=(\<lambda> (t,k). if k dvd c then (NDvd i (Add (Mul (c div k) t) e)) |
2810 else (NDvd (i*k) (Add (Mul c t) (Mul k e))))" |
2810 else (NDvd (i*k) (Add (Mul c t) (Mul k e))))" |
2811 "\<sigma>\<rho> p = (\<lambda> (t,k). p)" |
2811 "\<sigma>_\<rho> p = (\<lambda> (t,k). p)" |
2812 |
2812 |
2813 recdef \<alpha>\<rho> "measure size" |
2813 recdef \<alpha>_\<rho> "measure size" |
2814 "\<alpha>\<rho> (And p q) = (\<alpha>\<rho> p @ \<alpha>\<rho> q)" |
2814 "\<alpha>_\<rho> (And p q) = (\<alpha>_\<rho> p @ \<alpha>_\<rho> q)" |
2815 "\<alpha>\<rho> (Or p q) = (\<alpha>\<rho> p @ \<alpha>\<rho> q)" |
2815 "\<alpha>_\<rho> (Or p q) = (\<alpha>_\<rho> p @ \<alpha>_\<rho> q)" |
2816 "\<alpha>\<rho> (Eq (CN 0 c e)) = [(Add (C -1) e,c)]" |
2816 "\<alpha>_\<rho> (Eq (CN 0 c e)) = [(Add (C -1) e,c)]" |
2817 "\<alpha>\<rho> (NEq (CN 0 c e)) = [(e,c)]" |
2817 "\<alpha>_\<rho> (NEq (CN 0 c e)) = [(e,c)]" |
2818 "\<alpha>\<rho> (Lt (CN 0 c e)) = [(e,c)]" |
2818 "\<alpha>_\<rho> (Lt (CN 0 c e)) = [(e,c)]" |
2819 "\<alpha>\<rho> (Le (CN 0 c e)) = [(Add (C -1) e,c)]" |
2819 "\<alpha>_\<rho> (Le (CN 0 c e)) = [(Add (C -1) e,c)]" |
2820 "\<alpha>\<rho> p = []" |
2820 "\<alpha>_\<rho> p = []" |
2821 |
2821 |
2822 (* Simulates normal substituion by modifying the formula see correctness theorem *) |
2822 (* Simulates normal substituion by modifying the formula see correctness theorem *) |
2823 |
2823 |
2824 definition \<sigma> :: "fm \<Rightarrow> int \<Rightarrow> num \<Rightarrow> fm" where |
2824 definition \<sigma> :: "fm \<Rightarrow> int \<Rightarrow> num \<Rightarrow> fm" where |
2825 "\<sigma> p k t \<equiv> And (Dvd k t) (\<sigma>\<rho> p (t,k))" |
2825 "\<sigma> p k t \<equiv> And (Dvd k t) (\<sigma>_\<rho> p (t,k))" |
2826 |
2826 |
2827 lemma \<sigma>\<rho>: |
2827 lemma \<sigma>_\<rho>: |
2828 assumes linp: "iszlfm p (real (x::int)#bs)" |
2828 assumes linp: "iszlfm p (real (x::int)#bs)" |
2829 and kpos: "real k > 0" |
2829 and kpos: "real k > 0" |
2830 and tnb: "numbound0 t" |
2830 and tnb: "numbound0 t" |
2831 and tint: "isint t (real x#bs)" |
2831 and tint: "isint t (real x#bs)" |
2832 and kdt: "k dvd floor (Inum (b'#bs) t)" |
2832 and kdt: "k dvd floor (Inum (b'#bs) t)" |
2833 shows "Ifm (real x#bs) (\<sigma>\<rho> p (t,k)) = |
2833 shows "Ifm (real x#bs) (\<sigma>_\<rho> p (t,k)) = |
2834 (Ifm ((real ((floor (Inum (b'#bs) t)) div k))#bs) p)" |
2834 (Ifm ((real ((floor (Inum (b'#bs) t)) div k))#bs) p)" |
2835 (is "?I (real x) (?s p) = (?I (real ((floor (?N b' t)) div k)) p)" is "_ = (?I ?tk p)") |
2835 (is "?I (real x) (?s p) = (?I (real ((floor (?N b' t)) div k)) p)" is "_ = (?I ?tk p)") |
2836 using linp kpos tnb |
2836 using linp kpos tnb |
2837 proof(induct p rule: \<sigma>\<rho>.induct) |
2837 proof(induct p rule: \<sigma>_\<rho>.induct) |
2838 case (3 c e) |
2838 case (3 c e) |
2839 from 3 have cp: "c > 0" and nb: "numbound0 e" by auto |
2839 from 3 have cp: "c > 0" and nb: "numbound0 e" by auto |
2840 { assume kdc: "k dvd c" |
2840 { assume kdc: "k dvd c" |
2841 from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp |
2841 from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp |
2842 from kdc have ?case using real_of_int_div[OF kdc] real_of_int_div[OF kdt] |
2842 from kdc have ?case using real_of_int_div[OF kdc] real_of_int_div[OF kdt] |
3031 ultimately show ?case by blast |
3031 ultimately show ?case by blast |
3032 qed (simp_all add: bound0_I[where bs="bs" and b="real ((floor (?N b' t)) div k)" and b'="real x"] |
3032 qed (simp_all add: bound0_I[where bs="bs" and b="real ((floor (?N b' t)) div k)" and b'="real x"] |
3033 numbound0_I[where bs="bs" and b="real ((floor (?N b' t)) div k)" and b'="real x"]) |
3033 numbound0_I[where bs="bs" and b="real ((floor (?N b' t)) div k)" and b'="real x"]) |
3034 |
3034 |
3035 |
3035 |
3036 lemma \<sigma>\<rho>_nb: assumes lp:"iszlfm p (a#bs)" and nb: "numbound0 t" |
3036 lemma \<sigma>_\<rho>_nb: assumes lp:"iszlfm p (a#bs)" and nb: "numbound0 t" |
3037 shows "bound0 (\<sigma>\<rho> p (t,k))" |
3037 shows "bound0 (\<sigma>_\<rho> p (t,k))" |
3038 using lp |
3038 using lp |
3039 by (induct p rule: iszlfm.induct, auto simp add: nb) |
3039 by (induct p rule: iszlfm.induct, auto simp add: nb) |
3040 |
3040 |
3041 lemma \<rho>_l: |
3041 lemma \<rho>_l: |
3042 assumes lp: "iszlfm p (real (i::int)#bs)" |
3042 assumes lp: "iszlfm p (real (i::int)#bs)" |
3043 shows "\<forall> (b,k) \<in> set (\<rho> p). k >0 \<and> numbound0 b \<and> isint b (real i#bs)" |
3043 shows "\<forall> (b,k) \<in> set (\<rho> p). k >0 \<and> numbound0 b \<and> isint b (real i#bs)" |
3044 using lp by (induct p rule: \<rho>.induct, auto simp add: isint_sub isint_neg) |
3044 using lp by (induct p rule: \<rho>.induct, auto simp add: isint_sub isint_neg) |
3045 |
3045 |
3046 lemma \<alpha>\<rho>_l: |
3046 lemma \<alpha>_\<rho>_l: |
3047 assumes lp: "iszlfm p (real (i::int)#bs)" |
3047 assumes lp: "iszlfm p (real (i::int)#bs)" |
3048 shows "\<forall> (b,k) \<in> set (\<alpha>\<rho> p). k >0 \<and> numbound0 b \<and> isint b (real i#bs)" |
3048 shows "\<forall> (b,k) \<in> set (\<alpha>_\<rho> p). k >0 \<and> numbound0 b \<and> isint b (real i#bs)" |
3049 using lp isint_add [OF isint_c[where j="- 1"],where bs="real i#bs"] |
3049 using lp isint_add [OF isint_c[where j="- 1"],where bs="real i#bs"] |
3050 by (induct p rule: \<alpha>\<rho>.induct, auto) |
3050 by (induct p rule: \<alpha>_\<rho>.induct, auto) |
3051 |
3051 |
3052 lemma \<rho>: assumes lp: "iszlfm p (real (i::int) #bs)" |
3052 lemma \<rho>: assumes lp: "iszlfm p (real (i::int) #bs)" |
3053 and pi: "Ifm (real i#bs) p" |
3053 and pi: "Ifm (real i#bs) p" |
3054 and d: "d\<delta> p d" |
3054 and d: "d_\<delta> p d" |
3055 and dp: "d > 0" |
3055 and dp: "d > 0" |
3056 and nob: "\<forall>(e,c) \<in> set (\<rho> p). \<forall> j\<in> {1 .. c*d}. real (c*i) \<noteq> Inum (real i#bs) e + real j" |
3056 and nob: "\<forall>(e,c) \<in> set (\<rho> p). \<forall> j\<in> {1 .. c*d}. real (c*i) \<noteq> Inum (real i#bs) e + real j" |
3057 (is "\<forall>(e,c) \<in> set (\<rho> p). \<forall> j\<in> {1 .. c*d}. _ \<noteq> ?N i e + _") |
3057 (is "\<forall>(e,c) \<in> set (\<rho> p). \<forall> j\<in> {1 .. c*d}. _ \<noteq> ?N i e + _") |
3058 shows "Ifm (real(i - d)#bs) p" |
3058 shows "Ifm (real(i - d)#bs) p" |
3059 using lp pi d nob |
3059 using lp pi d nob |
3217 from cp have cp': "real c > 0" by simp |
3217 from cp have cp': "real c > 0" by simp |
3218 from cdej have cdej': "c dvd floor (Inum (real x#bs) (Add e (C j)))" by simp |
3218 from cdej have cdej': "c dvd floor (Inum (real x#bs) (Add e (C j)))" by simp |
3219 from nb have nb': "numbound0 (Add e (C j))" by simp |
3219 from nb have nb': "numbound0 (Add e (C j))" by simp |
3220 have ji: "isint (C j) (real x#bs)" by (simp add: isint_def) |
3220 have ji: "isint (C j) (real x#bs)" by (simp add: isint_def) |
3221 from isint_add[OF ei ji] have ei':"isint (Add e (C j)) (real x#bs)" . |
3221 from isint_add[OF ei ji] have ei':"isint (Add e (C j)) (real x#bs)" . |
3222 from th \<sigma>\<rho>[where b'="real x", OF lp' cp' nb' ei' cdej',symmetric] |
3222 from th \<sigma>_\<rho>[where b'="real x", OF lp' cp' nb' ei' cdej',symmetric] |
3223 have "Ifm (real x#bs) (\<sigma>\<rho> p (Add e (C j), c))" by simp |
3223 have "Ifm (real x#bs) (\<sigma>_\<rho> p (Add e (C j), c))" by simp |
3224 with rcdej have th: "Ifm (real x#bs) (\<sigma> p c (Add e (C j)))" by (simp add: \<sigma>_def) |
3224 with rcdej have th: "Ifm (real x#bs) (\<sigma> p c (Add e (C j)))" by (simp add: \<sigma>_def) |
3225 from th bound0_I[OF \<sigma>_nb[OF lp nb', where k="c"],where bs="bs" and b="real x" and b'="a"] |
3225 from th bound0_I[OF \<sigma>_nb[OF lp nb', where k="c"],where bs="bs" and b="real x" and b'="a"] |
3226 have "Ifm (a#bs) (\<sigma> p c (Add e (C j)))" by blast |
3226 have "Ifm (a#bs) (\<sigma> p c (Add e (C j)))" by blast |
3227 with ecR jD nob1 show "False" by blast |
3227 with ecR jD nob1 show "False" by blast |
3228 qed |
3228 qed |
3235 shows "(\<exists> (x::int). Ifm (real x#bs) p) = ((\<exists> j\<in> {1 .. \<delta> p}. Ifm (real j#bs) (minusinf p)) \<or> (\<exists> (e,c) \<in> set (\<rho> p). \<exists> j\<in> {1 .. c*(\<delta> p)}. Ifm (a#bs) (\<sigma> p c (Add e (C j)))))" |
3235 shows "(\<exists> (x::int). Ifm (real x#bs) p) = ((\<exists> j\<in> {1 .. \<delta> p}. Ifm (real j#bs) (minusinf p)) \<or> (\<exists> (e,c) \<in> set (\<rho> p). \<exists> j\<in> {1 .. c*(\<delta> p)}. Ifm (a#bs) (\<sigma> p c (Add e (C j)))))" |
3236 (is "(\<exists>(x::int). ?P x) = ((\<exists> j\<in> {1.. \<delta> p}. ?MP j)\<or>(\<exists> (e,c) \<in> ?R. \<exists> j\<in> _. ?SP c e j))" |
3236 (is "(\<exists>(x::int). ?P x) = ((\<exists> j\<in> {1.. \<delta> p}. ?MP j)\<or>(\<exists> (e,c) \<in> ?R. \<exists> j\<in> _. ?SP c e j))" |
3237 is "?lhs = (?MD \<or> ?RD)" is "?lhs = ?rhs") |
3237 is "?lhs = (?MD \<or> ?RD)" is "?lhs = ?rhs") |
3238 proof- |
3238 proof- |
3239 let ?d= "\<delta> p" |
3239 let ?d= "\<delta> p" |
3240 from \<delta>[OF lp] have d:"d\<delta> p ?d" and dp: "?d > 0" by auto |
3240 from \<delta>[OF lp] have d:"d_\<delta> p ?d" and dp: "?d > 0" by auto |
3241 { assume H:"?MD" hence th:"\<exists> (x::int). ?MP x" by blast |
3241 { assume H:"?MD" hence th:"\<exists> (x::int). ?MP x" by blast |
3242 from H minusinf_ex[OF lp th] have ?thesis by blast} |
3242 from H minusinf_ex[OF lp th] have ?thesis by blast} |
3243 moreover |
3243 moreover |
3244 { fix e c j assume exR:"(e,c) \<in> ?R" and jD:"j\<in> {1 .. c*?d}" and spx:"?SP c e j" |
3244 { fix e c j assume exR:"(e,c) \<in> ?R" and jD:"j\<in> {1 .. c*?d}" and spx:"?SP c e j" |
3245 from exR \<rho>_l[OF lp] have nb: "numbound0 e" and ei:"isint e (real i#bs)" and cp: "c > 0" |
3245 from exR \<rho>_l[OF lp] have nb: "numbound0 e" and ei:"isint e (real i#bs)" and cp: "c > 0" |
3249 have eji:"isint (Add e (C j)) (real i#bs)" by simp |
3249 have eji:"isint (Add e (C j)) (real i#bs)" by simp |
3250 from nb have nb': "numbound0 (Add e (C j))" by simp |
3250 from nb have nb': "numbound0 (Add e (C j))" by simp |
3251 from spx bound0_I[OF \<sigma>_nb[OF lp nb', where k="c"], where bs="bs" and b="a" and b'="real i"] |
3251 from spx bound0_I[OF \<sigma>_nb[OF lp nb', where k="c"], where bs="bs" and b="a" and b'="real i"] |
3252 have spx': "Ifm (real i # bs) (\<sigma> p c (Add e (C j)))" by blast |
3252 have spx': "Ifm (real i # bs) (\<sigma> p c (Add e (C j)))" by blast |
3253 from spx' have rcdej:"real c rdvd (Inum (real i#bs) (Add e (C j)))" |
3253 from spx' have rcdej:"real c rdvd (Inum (real i#bs) (Add e (C j)))" |
3254 and sr:"Ifm (real i#bs) (\<sigma>\<rho> p (Add e (C j),c))" by (simp add: \<sigma>_def)+ |
3254 and sr:"Ifm (real i#bs) (\<sigma>_\<rho> p (Add e (C j),c))" by (simp add: \<sigma>_def)+ |
3255 from rcdej eji[simplified isint_iff] |
3255 from rcdej eji[simplified isint_iff] |
3256 have "real c rdvd real (floor (Inum (real i#bs) (Add e (C j))))" by simp |
3256 have "real c rdvd real (floor (Inum (real i#bs) (Add e (C j))))" by simp |
3257 hence cdej:"c dvd floor (Inum (real i#bs) (Add e (C j)))" by (simp only: int_rdvd_iff) |
3257 hence cdej:"c dvd floor (Inum (real i#bs) (Add e (C j)))" by (simp only: int_rdvd_iff) |
3258 from cp have cp': "real c > 0" by simp |
3258 from cp have cp': "real c > 0" by simp |
3259 from \<sigma>\<rho>[OF lp cp' nb' eji cdej] spx' have "?P (\<lfloor>Inum (real i # bs) (Add e (C j))\<rfloor> div c)" |
3259 from \<sigma>_\<rho>[OF lp cp' nb' eji cdej] spx' have "?P (\<lfloor>Inum (real i # bs) (Add e (C j))\<rfloor> div c)" |
3260 by (simp add: \<sigma>_def) |
3260 by (simp add: \<sigma>_def) |
3261 hence ?lhs by blast |
3261 hence ?lhs by blast |
3262 with exR jD spx have ?thesis by blast} |
3262 with exR jD spx have ?thesis by blast} |
3263 moreover |
3263 moreover |
3264 { fix x assume px: "?P x" and nob: "\<not> ?RD" |
3264 { fix x assume px: "?P x" and nob: "\<not> ?RD" |
5064 with lr show ?thesis by blast |
5064 with lr show ?thesis by blast |
5065 qed |
5065 qed |
5066 |
5066 |
5067 lemma cp_thm': |
5067 lemma cp_thm': |
5068 assumes lp: "iszlfm p (real (i::int)#bs)" |
5068 assumes lp: "iszlfm p (real (i::int)#bs)" |
5069 and up: "d\<beta> p 1" and dd: "d\<delta> p d" and dp: "d > 0" |
5069 and up: "d_\<beta> p 1" and dd: "d_\<delta> p d" and dp: "d > 0" |
5070 shows "(\<exists> (x::int). Ifm (real x#bs) p) = ((\<exists> j\<in> {1 .. d}. Ifm (real j#bs) (minusinf p)) \<or> (\<exists> j\<in> {1.. d}. \<exists> b\<in> (Inum (real i#bs)) ` set (\<beta> p). Ifm ((b+real j)#bs) p))" |
5070 shows "(\<exists> (x::int). Ifm (real x#bs) p) = ((\<exists> j\<in> {1 .. d}. Ifm (real j#bs) (minusinf p)) \<or> (\<exists> j\<in> {1.. d}. \<exists> b\<in> (Inum (real i#bs)) ` set (\<beta> p). Ifm ((b+real j)#bs) p))" |
5071 using cp_thm[OF lp up dd dp] by auto |
5071 using cp_thm[OF lp up dd dp] by auto |
5072 |
5072 |
5073 definition unit :: "fm \<Rightarrow> fm \<times> num list \<times> int" where |
5073 definition unit :: "fm \<Rightarrow> fm \<times> num list \<times> int" where |
5074 "unit p \<equiv> (let p' = zlfm p ; l = \<zeta> p' ; q = And (Dvd l (CN 0 1 (C 0))) (a\<beta> p' l); d = \<delta> q; |
5074 "unit p \<equiv> (let p' = zlfm p ; l = \<zeta> p' ; q = And (Dvd l (CN 0 1 (C 0))) (a_\<beta> p' l); d = \<delta> q; |
5075 B = remdups (map simpnum (\<beta> q)) ; a = remdups (map simpnum (\<alpha> q)) |
5075 B = remdups (map simpnum (\<beta> q)) ; a = remdups (map simpnum (\<alpha> q)) |
5076 in if length B \<le> length a then (q,B,d) else (mirror q, a,d))" |
5076 in if length B \<le> length a then (q,B,d) else (mirror q, a,d))" |
5077 |
5077 |
5078 lemma unit: assumes qf: "qfree p" |
5078 lemma unit: assumes qf: "qfree p" |
5079 shows "\<And> q B d. unit p = (q,B,d) \<Longrightarrow> ((\<exists> (x::int). Ifm (real x#bs) p) = (\<exists> (x::int). Ifm (real x#bs) q)) \<and> (Inum (real i#bs)) ` set B = (Inum (real i#bs)) ` set (\<beta> q) \<and> d\<beta> q 1 \<and> d\<delta> q d \<and> d >0 \<and> iszlfm q (real (i::int)#bs) \<and> (\<forall> b\<in> set B. numbound0 b)" |
5079 shows "\<And> q B d. unit p = (q,B,d) \<Longrightarrow> ((\<exists> (x::int). Ifm (real x#bs) p) = (\<exists> (x::int). Ifm (real x#bs) q)) \<and> (Inum (real i#bs)) ` set B = (Inum (real i#bs)) ` set (\<beta> q) \<and> d_\<beta> q 1 \<and> d_\<delta> q d \<and> d >0 \<and> iszlfm q (real (i::int)#bs) \<and> (\<forall> b\<in> set B. numbound0 b)" |
5080 proof- |
5080 proof- |
5081 fix q B d |
5081 fix q B d |
5082 assume qBd: "unit p = (q,B,d)" |
5082 assume qBd: "unit p = (q,B,d)" |
5083 let ?thes = "((\<exists> (x::int). Ifm (real x#bs) p) = (\<exists> (x::int). Ifm (real x#bs) q)) \<and> |
5083 let ?thes = "((\<exists> (x::int). Ifm (real x#bs) p) = (\<exists> (x::int). Ifm (real x#bs) q)) \<and> |
5084 Inum (real i#bs) ` set B = Inum (real i#bs) ` set (\<beta> q) \<and> |
5084 Inum (real i#bs) ` set B = Inum (real i#bs) ` set (\<beta> q) \<and> |
5085 d\<beta> q 1 \<and> d\<delta> q d \<and> 0 < d \<and> iszlfm q (real i # bs) \<and> (\<forall> b\<in> set B. numbound0 b)" |
5085 d_\<beta> q 1 \<and> d_\<delta> q d \<and> 0 < d \<and> iszlfm q (real i # bs) \<and> (\<forall> b\<in> set B. numbound0 b)" |
5086 let ?I = "\<lambda> (x::int) p. Ifm (real x#bs) p" |
5086 let ?I = "\<lambda> (x::int) p. Ifm (real x#bs) p" |
5087 let ?p' = "zlfm p" |
5087 let ?p' = "zlfm p" |
5088 let ?l = "\<zeta> ?p'" |
5088 let ?l = "\<zeta> ?p'" |
5089 let ?q = "And (Dvd ?l (CN 0 1 (C 0))) (a\<beta> ?p' ?l)" |
5089 let ?q = "And (Dvd ?l (CN 0 1 (C 0))) (a_\<beta> ?p' ?l)" |
5090 let ?d = "\<delta> ?q" |
5090 let ?d = "\<delta> ?q" |
5091 let ?B = "set (\<beta> ?q)" |
5091 let ?B = "set (\<beta> ?q)" |
5092 let ?B'= "remdups (map simpnum (\<beta> ?q))" |
5092 let ?B'= "remdups (map simpnum (\<beta> ?q))" |
5093 let ?A = "set (\<alpha> ?q)" |
5093 let ?A = "set (\<alpha> ?q)" |
5094 let ?A'= "remdups (map simpnum (\<alpha> ?q))" |
5094 let ?A'= "remdups (map simpnum (\<alpha> ?q))" |
5095 from conjunct1[OF zlfm_I[OF qf, where bs="bs"]] |
5095 from conjunct1[OF zlfm_I[OF qf, where bs="bs"]] |
5096 have pp': "\<forall> i. ?I i ?p' = ?I i p" by auto |
5096 have pp': "\<forall> i. ?I i ?p' = ?I i p" by auto |
5097 from iszlfm_gen[OF conjunct2[OF zlfm_I[OF qf, where bs="bs" and i="i"]]] |
5097 from iszlfm_gen[OF conjunct2[OF zlfm_I[OF qf, where bs="bs" and i="i"]]] |
5098 have lp': "\<forall> (i::int). iszlfm ?p' (real i#bs)" by simp |
5098 have lp': "\<forall> (i::int). iszlfm ?p' (real i#bs)" by simp |
5099 hence lp'': "iszlfm ?p' (real (i::int)#bs)" by simp |
5099 hence lp'': "iszlfm ?p' (real (i::int)#bs)" by simp |
5100 from lp' \<zeta>[where p="?p'" and bs="bs"] have lp: "?l >0" and dl: "d\<beta> ?p' ?l" by auto |
5100 from lp' \<zeta>[where p="?p'" and bs="bs"] have lp: "?l >0" and dl: "d_\<beta> ?p' ?l" by auto |
5101 from a\<beta>_ex[where p="?p'" and l="?l" and bs="bs", OF lp'' dl lp] pp' |
5101 from a_\<beta>_ex[where p="?p'" and l="?l" and bs="bs", OF lp'' dl lp] pp' |
5102 have pq_ex:"(\<exists> (x::int). ?I x p) = (\<exists> x. ?I x ?q)" by (simp add: int_rdvd_iff) |
5102 have pq_ex:"(\<exists> (x::int). ?I x p) = (\<exists> x. ?I x ?q)" by (simp add: int_rdvd_iff) |
5103 from lp'' lp a\<beta>[OF lp'' dl lp] have lq:"iszlfm ?q (real i#bs)" and uq: "d\<beta> ?q 1" |
5103 from lp'' lp a_\<beta>[OF lp'' dl lp] have lq:"iszlfm ?q (real i#bs)" and uq: "d_\<beta> ?q 1" |
5104 by (auto simp add: isint_def) |
5104 by (auto simp add: isint_def) |
5105 from \<delta>[OF lq] have dp:"?d >0" and dd: "d\<delta> ?q ?d" by blast+ |
5105 from \<delta>[OF lq] have dp:"?d >0" and dd: "d_\<delta> ?q ?d" by blast+ |
5106 let ?N = "\<lambda> t. Inum (real (i::int)#bs) t" |
5106 let ?N = "\<lambda> t. Inum (real (i::int)#bs) t" |
5107 have "?N ` set ?B' = ((?N o simpnum) ` ?B)" by (simp add:image_compose) |
5107 have "?N ` set ?B' = ((?N o simpnum) ` ?B)" by (simp add:image_compose) |
5108 also have "\<dots> = ?N ` ?B" using simpnum_ci[where bs="real i #bs"] by auto |
5108 also have "\<dots> = ?N ` ?B" using simpnum_ci[where bs="real i #bs"] by auto |
5109 finally have BB': "?N ` set ?B' = ?N ` ?B" . |
5109 finally have BB': "?N ` set ?B' = ?N ` ?B" . |
5110 have "?N ` set ?A' = ((?N o simpnum) ` ?A)" by (simp add:image_compose) |
5110 have "?N ` set ?A' = ((?N o simpnum) ` ?A)" by (simp add:image_compose) |
5122 with pq_ex dp uq dd lq q d have ?thes by simp} |
5122 with pq_ex dp uq dd lq q d have ?thes by simp} |
5123 moreover |
5123 moreover |
5124 {assume "\<not> (length ?B' \<le> length ?A')" |
5124 {assume "\<not> (length ?B' \<le> length ?A')" |
5125 hence q:"q=mirror ?q" and "B = ?A'" and d:"d = ?d" |
5125 hence q:"q=mirror ?q" and "B = ?A'" and d:"d = ?d" |
5126 using qBd by (auto simp add: Let_def unit_def) |
5126 using qBd by (auto simp add: Let_def unit_def) |
5127 with AA' mirror\<alpha>\<beta>[OF lq] A_nb have b:"?N ` (set B) = ?N ` set (\<beta> q)" |
5127 with AA' mirror_\<alpha>_\<beta>[OF lq] A_nb have b:"?N ` (set B) = ?N ` set (\<beta> q)" |
5128 and bn: "\<forall>b\<in> set B. numbound0 b" by simp+ |
5128 and bn: "\<forall>b\<in> set B. numbound0 b" by simp+ |
5129 from mirror_ex[OF lq] pq_ex q |
5129 from mirror_ex[OF lq] pq_ex q |
5130 have pqm_eq:"(\<exists> (x::int). ?I x p) = (\<exists> (x::int). ?I x q)" by simp |
5130 have pqm_eq:"(\<exists> (x::int). ?I x p) = (\<exists> (x::int). ?I x q)" by simp |
5131 from lq uq q mirror_d\<beta> [where p="?q" and bs="bs" and a="real i"] |
5131 from lq uq q mirror_d_\<beta> [where p="?q" and bs="bs" and a="real i"] |
5132 have lq': "iszlfm q (real i#bs)" and uq: "d\<beta> q 1" by auto |
5132 have lq': "iszlfm q (real i#bs)" and uq: "d_\<beta> q 1" by auto |
5133 from \<delta>[OF lq'] mirror_\<delta>[OF lq] q d have dq:"d\<delta> q d " by auto |
5133 from \<delta>[OF lq'] mirror_\<delta>[OF lq] q d have dq:"d_\<delta> q d " by auto |
5134 from pqm_eq b bn uq lq' dp dq q dp d have ?thes by simp |
5134 from pqm_eq b bn uq lq' dp dq q dp d have ?thes by simp |
5135 } |
5135 } |
5136 ultimately show ?thes by blast |
5136 ultimately show ?thes by blast |
5137 qed |
5137 qed |
5138 (* Cooper's Algorithm *) |
5138 (* Cooper's Algorithm *) |
5166 let ?sbjs = "map (\<lambda> (b,j). simpnum (Add b (C j))) ?bjs" |
5166 let ?sbjs = "map (\<lambda> (b,j). simpnum (Add b (C j))) ?bjs" |
5167 let ?qd = "evaldjf (\<lambda> t. simpfm (subst0 t ?q)) (remdups ?sbjs)" |
5167 let ?qd = "evaldjf (\<lambda> t. simpfm (subst0 t ?q)) (remdups ?sbjs)" |
5168 have qbf:"unit p = (?q,?B,?d)" by simp |
5168 have qbf:"unit p = (?q,?B,?d)" by simp |
5169 from unit[OF qf qbf] have pq_ex: "(\<exists>(x::int). ?I x p) = (\<exists> (x::int). ?I x ?q)" and |
5169 from unit[OF qf qbf] have pq_ex: "(\<exists>(x::int). ?I x p) = (\<exists> (x::int). ?I x ?q)" and |
5170 B:"?N ` set ?B = ?N ` set (\<beta> ?q)" and |
5170 B:"?N ` set ?B = ?N ` set (\<beta> ?q)" and |
5171 uq:"d\<beta> ?q 1" and dd: "d\<delta> ?q ?d" and dp: "?d > 0" and |
5171 uq:"d_\<beta> ?q 1" and dd: "d_\<delta> ?q ?d" and dp: "?d > 0" and |
5172 lq: "iszlfm ?q (real i#bs)" and |
5172 lq: "iszlfm ?q (real i#bs)" and |
5173 Bn: "\<forall> b\<in> set ?B. numbound0 b" by auto |
5173 Bn: "\<forall> b\<in> set ?B. numbound0 b" by auto |
5174 from zlin_qfree[OF lq] have qfq: "qfree ?q" . |
5174 from zlin_qfree[OF lq] have qfq: "qfree ?q" . |
5175 from simpfm_qf[OF minusinf_qfree[OF qfq]] have qfmq: "qfree ?smq". |
5175 from simpfm_qf[OF minusinf_qfree[OF qfq]] have qfmq: "qfree ?smq". |
5176 have jsnb: "\<forall> j \<in> set ?js. numbound0 (C j)" by simp |
5176 have jsnb: "\<forall> j \<in> set ?js. numbound0 (C j)" by simp |
5229 finally show ?thesis using thqf by blast |
5229 finally show ?thesis using thqf by blast |
5230 qed |
5230 qed |
5231 |
5231 |
5232 (* Redy and Loveland *) |
5232 (* Redy and Loveland *) |
5233 |
5233 |
5234 lemma \<sigma>\<rho>_cong: assumes lp: "iszlfm p (a#bs)" and tt': "Inum (a#bs) t = Inum (a#bs) t'" |
5234 lemma \<sigma>_\<rho>_cong: assumes lp: "iszlfm p (a#bs)" and tt': "Inum (a#bs) t = Inum (a#bs) t'" |
5235 shows "Ifm (a#bs) (\<sigma>\<rho> p (t,c)) = Ifm (a#bs) (\<sigma>\<rho> p (t',c))" |
5235 shows "Ifm (a#bs) (\<sigma>_\<rho> p (t,c)) = Ifm (a#bs) (\<sigma>_\<rho> p (t',c))" |
5236 using lp |
5236 using lp |
5237 by (induct p rule: iszlfm.induct, auto simp add: tt') |
5237 by (induct p rule: iszlfm.induct, auto simp add: tt') |
5238 |
5238 |
5239 lemma \<sigma>_cong: assumes lp: "iszlfm p (a#bs)" and tt': "Inum (a#bs) t = Inum (a#bs) t'" |
5239 lemma \<sigma>_cong: assumes lp: "iszlfm p (a#bs)" and tt': "Inum (a#bs) t = Inum (a#bs) t'" |
5240 shows "Ifm (a#bs) (\<sigma> p c t) = Ifm (a#bs) (\<sigma> p c t')" |
5240 shows "Ifm (a#bs) (\<sigma> p c t) = Ifm (a#bs) (\<sigma> p c t')" |
5241 by (simp add: \<sigma>_def tt' \<sigma>\<rho>_cong[OF lp tt']) |
5241 by (simp add: \<sigma>_def tt' \<sigma>_\<rho>_cong[OF lp tt']) |
5242 |
5242 |
5243 lemma \<rho>_cong: assumes lp: "iszlfm p (a#bs)" |
5243 lemma \<rho>_cong: assumes lp: "iszlfm p (a#bs)" |
5244 and RR: "(\<lambda>(b,k). (Inum (a#bs) b,k)) ` R = (\<lambda>(b,k). (Inum (a#bs) b,k)) ` set (\<rho> p)" |
5244 and RR: "(\<lambda>(b,k). (Inum (a#bs) b,k)) ` R = (\<lambda>(b,k). (Inum (a#bs) b,k)) ` set (\<rho> p)" |
5245 shows "(\<exists> (e,c) \<in> R. \<exists> j\<in> {1.. c*(\<delta> p)}. Ifm (a#bs) (\<sigma> p c (Add e (C j)))) = (\<exists> (e,c) \<in> set (\<rho> p). \<exists> j\<in> {1.. c*(\<delta> p)}. Ifm (a#bs) (\<sigma> p c (Add e (C j))))" |
5245 shows "(\<exists> (e,c) \<in> R. \<exists> j\<in> {1.. c*(\<delta> p)}. Ifm (a#bs) (\<sigma> p c (Add e (C j)))) = (\<exists> (e,c) \<in> set (\<rho> p). \<exists> j\<in> {1.. c*(\<delta> p)}. Ifm (a#bs) (\<sigma> p c (Add e (C j))))" |
5246 (is "?lhs = ?rhs") |
5246 (is "?lhs = ?rhs") |
5282 using rl_thm[OF lp] \<rho>_cong[OF iszlfm_gen[OF lp, rule_format, where y="a"] R] by simp |
5282 using rl_thm[OF lp] \<rho>_cong[OF iszlfm_gen[OF lp, rule_format, where y="a"] R] by simp |
5283 |
5283 |
5284 definition chooset :: "fm \<Rightarrow> fm \<times> ((num\<times>int) list) \<times> int" where |
5284 definition chooset :: "fm \<Rightarrow> fm \<times> ((num\<times>int) list) \<times> int" where |
5285 "chooset p \<equiv> (let q = zlfm p ; d = \<delta> q; |
5285 "chooset p \<equiv> (let q = zlfm p ; d = \<delta> q; |
5286 B = remdups (map (\<lambda> (t,k). (simpnum t,k)) (\<rho> q)) ; |
5286 B = remdups (map (\<lambda> (t,k). (simpnum t,k)) (\<rho> q)) ; |
5287 a = remdups (map (\<lambda> (t,k). (simpnum t,k)) (\<alpha>\<rho> q)) |
5287 a = remdups (map (\<lambda> (t,k). (simpnum t,k)) (\<alpha>_\<rho> q)) |
5288 in if length B \<le> length a then (q,B,d) else (mirror q, a,d))" |
5288 in if length B \<le> length a then (q,B,d) else (mirror q, a,d))" |
5289 |
5289 |
5290 lemma chooset: assumes qf: "qfree p" |
5290 lemma chooset: assumes qf: "qfree p" |
5291 shows "\<And> q B d. chooset p = (q,B,d) \<Longrightarrow> ((\<exists> (x::int). Ifm (real x#bs) p) = (\<exists> (x::int). Ifm (real x#bs) q)) \<and> ((\<lambda>(t,k). (Inum (real i#bs) t,k)) ` set B = (\<lambda>(t,k). (Inum (real i#bs) t,k)) ` set (\<rho> q)) \<and> (\<delta> q = d) \<and> d >0 \<and> iszlfm q (real (i::int)#bs) \<and> (\<forall> (e,c)\<in> set B. numbound0 e \<and> c>0)" |
5291 shows "\<And> q B d. chooset p = (q,B,d) \<Longrightarrow> ((\<exists> (x::int). Ifm (real x#bs) p) = (\<exists> (x::int). Ifm (real x#bs) q)) \<and> ((\<lambda>(t,k). (Inum (real i#bs) t,k)) ` set B = (\<lambda>(t,k). (Inum (real i#bs) t,k)) ` set (\<rho> q)) \<and> (\<delta> q = d) \<and> d >0 \<and> iszlfm q (real (i::int)#bs) \<and> (\<forall> (e,c)\<in> set B. numbound0 e \<and> c>0)" |
5292 proof- |
5292 proof- |
5297 let ?q = "zlfm p" |
5297 let ?q = "zlfm p" |
5298 let ?d = "\<delta> ?q" |
5298 let ?d = "\<delta> ?q" |
5299 let ?B = "set (\<rho> ?q)" |
5299 let ?B = "set (\<rho> ?q)" |
5300 let ?f = "\<lambda> (t,k). (simpnum t,k)" |
5300 let ?f = "\<lambda> (t,k). (simpnum t,k)" |
5301 let ?B'= "remdups (map ?f (\<rho> ?q))" |
5301 let ?B'= "remdups (map ?f (\<rho> ?q))" |
5302 let ?A = "set (\<alpha>\<rho> ?q)" |
5302 let ?A = "set (\<alpha>_\<rho> ?q)" |
5303 let ?A'= "remdups (map ?f (\<alpha>\<rho> ?q))" |
5303 let ?A'= "remdups (map ?f (\<alpha>_\<rho> ?q))" |
5304 from conjunct1[OF zlfm_I[OF qf, where bs="bs"]] |
5304 from conjunct1[OF zlfm_I[OF qf, where bs="bs"]] |
5305 have pp': "\<forall> i. ?I i ?q = ?I i p" by auto |
5305 have pp': "\<forall> i. ?I i ?q = ?I i p" by auto |
5306 hence pq_ex:"(\<exists> (x::int). ?I x p) = (\<exists> x. ?I x ?q)" by simp |
5306 hence pq_ex:"(\<exists> (x::int). ?I x p) = (\<exists> x. ?I x ?q)" by simp |
5307 from iszlfm_gen[OF conjunct2[OF zlfm_I[OF qf, where bs="bs" and i="i"]], rule_format, where y="real i"] |
5307 from iszlfm_gen[OF conjunct2[OF zlfm_I[OF qf, where bs="bs" and i="i"]], rule_format, where y="real i"] |
5308 have lq: "iszlfm ?q (real (i::int)#bs)" . |
5308 have lq: "iszlfm ?q (real (i::int)#bs)" . |
5316 also have "\<dots> = ?N ` ?A" using simpnum_ci[where bs="real i #bs"] |
5316 also have "\<dots> = ?N ` ?A" using simpnum_ci[where bs="real i #bs"] |
5317 by(simp add: split_def image_compose simpnum_ci[where bs="real i #bs"] image_def) |
5317 by(simp add: split_def image_compose simpnum_ci[where bs="real i #bs"] image_def) |
5318 finally have AA': "?N ` set ?A' = ?N ` ?A" . |
5318 finally have AA': "?N ` set ?A' = ?N ` ?A" . |
5319 from \<rho>_l[OF lq] have B_nb:"\<forall> (e,c)\<in> set ?B'. numbound0 e \<and> c > 0" |
5319 from \<rho>_l[OF lq] have B_nb:"\<forall> (e,c)\<in> set ?B'. numbound0 e \<and> c > 0" |
5320 by (simp add: simpnum_numbound0 split_def) |
5320 by (simp add: simpnum_numbound0 split_def) |
5321 from \<alpha>\<rho>_l[OF lq] have A_nb: "\<forall> (e,c)\<in> set ?A'. numbound0 e \<and> c > 0" |
5321 from \<alpha>_\<rho>_l[OF lq] have A_nb: "\<forall> (e,c)\<in> set ?A'. numbound0 e \<and> c > 0" |
5322 by (simp add: simpnum_numbound0 split_def) |
5322 by (simp add: simpnum_numbound0 split_def) |
5323 {assume "length ?B' \<le> length ?A'" |
5323 {assume "length ?B' \<le> length ?A'" |
5324 hence q:"q=?q" and "B = ?B'" and d:"d = ?d" |
5324 hence q:"q=?q" and "B = ?B'" and d:"d = ?d" |
5325 using qBd by (auto simp add: Let_def chooset_def) |
5325 using qBd by (auto simp add: Let_def chooset_def) |
5326 with BB' B_nb have b: "?N ` (set B) = ?N ` set (\<rho> q)" |
5326 with BB' B_nb have b: "?N ` (set B) = ?N ` set (\<rho> q)" |