summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Wed, 05 Mar 2014 17:36:40 +0100 | |

changeset 55921 | 22e9fc998d65 |

parent 55920 | f376f18fd0b7 |

child 55922 | 710bc66f432c |

tuned proofs;

--- a/src/HOL/Decision_Procs/Cooper.thy Wed Mar 05 16:16:36 2014 +0100 +++ b/src/HOL/Decision_Procs/Cooper.thy Wed Mar 05 17:36:40 2014 +0100 @@ -405,10 +405,10 @@ fun bnds :: "num \<Rightarrow> nat list" where "bnds (Bound n) = [n]" -| "bnds (CN n c a) = n#(bnds a)" +| "bnds (CN n c a) = n # bnds a" | "bnds (Neg a) = bnds a" -| "bnds (Add a b) = (bnds a)@(bnds b)" -| "bnds (Sub a b) = (bnds a)@(bnds b)" +| "bnds (Add a b) = bnds a @ bnds b" +| "bnds (Sub a b) = bnds a @ bnds b" | "bnds (Mul i a) = bnds a" | "bnds a = []" @@ -422,12 +422,12 @@ where "lex_bnd t s = lex_ns (bnds t) (bnds s)" consts numadd:: "num \<times> num \<Rightarrow> num" -recdef numadd "measure (\<lambda>(t,s). num_size t + num_size s)" +recdef numadd "measure (\<lambda>(t, s). num_size t + num_size s)" "numadd (CN n1 c1 r1 ,CN n2 c2 r2) = (if n1 = n2 then (let c = c1 + c2 - in if c=0 then numadd (r1, r2) else CN n1 c (numadd (r1, r2))) - else if n1 \<le> n2 then CN n1 c1 (numadd (r1,Add (Mul c2 (Bound n2)) r2)) + in if c = 0 then numadd (r1, r2) else CN n1 c (numadd (r1, r2))) + else if n1 \<le> n2 then CN n1 c1 (numadd (r1, Add (Mul c2 (Bound n2)) r2)) else CN n2 c2 (numadd (Add (Mul c1 (Bound n1)) r1, r2)))" "numadd (CN n1 c1 r1, t) = CN n1 c1 (numadd (r1, t))" "numadd (t, CN n2 c2 r2) = CN n2 c2 (numadd (t, r2))" @@ -608,20 +608,20 @@ | "simpfm (Imp p q) = imp (simpfm p) (simpfm q)" | "simpfm (Iff p q) = iff (simpfm p) (simpfm q)" | "simpfm (NOT p) = not (simpfm p)" -| "simpfm (Lt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v < 0) then T else F | _ \<Rightarrow> Lt a')" -| "simpfm (Le a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<le> 0) then T else F | _ \<Rightarrow> Le a')" -| "simpfm (Gt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v > 0) then T else F | _ \<Rightarrow> Gt a')" -| "simpfm (Ge a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<ge> 0) then T else F | _ \<Rightarrow> Ge a')" -| "simpfm (Eq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v = 0) then T else F | _ \<Rightarrow> Eq a')" -| "simpfm (NEq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<noteq> 0) then T else F | _ \<Rightarrow> NEq a')" +| "simpfm (Lt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if v < 0 then T else F | _ \<Rightarrow> Lt a')" +| "simpfm (Le a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if v \<le> 0 then T else F | _ \<Rightarrow> Le a')" +| "simpfm (Gt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if v > 0 then T else F | _ \<Rightarrow> Gt a')" +| "simpfm (Ge a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if v \<ge> 0 then T else F | _ \<Rightarrow> Ge a')" +| "simpfm (Eq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if v = 0 then T else F | _ \<Rightarrow> Eq a')" +| "simpfm (NEq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if v \<noteq> 0 then T else F | _ \<Rightarrow> NEq a')" | "simpfm (Dvd i a) = (if i = 0 then simpfm (Eq a) else if abs i = 1 then T - else let a' = simpnum a in case a' of C v \<Rightarrow> if (i dvd v) then T else F | _ \<Rightarrow> Dvd i a')" + else let a' = simpnum a in case a' of C v \<Rightarrow> if i dvd v then T else F | _ \<Rightarrow> Dvd i a')" | "simpfm (NDvd i a) = (if i = 0 then simpfm (NEq a) else if abs i = 1 then F - else let a' = simpnum a in case a' of C v \<Rightarrow> if (\<not>(i dvd v)) then T else F | _ \<Rightarrow> NDvd i a')" + else let a' = simpnum a in case a' of C v \<Rightarrow> if \<not>( i dvd v) then T else F | _ \<Rightarrow> NDvd i a')" | "simpfm p = p" by pat_completeness auto termination by (relation "measure fmsize") auto @@ -823,7 +823,8 @@ | "zsplit0 (Mul i a) = (let (i', a') = zsplit0 a in (i*i', Mul i a'))" lemma zsplit0_I: - shows "\<And>n a. zsplit0 t = (n,a) \<Longrightarrow> (Inum ((x::int) #bs) (CN 0 n a) = Inum (x #bs) t) \<and> numbound0 a" + shows "\<And>n a. zsplit0 t = (n, a) \<Longrightarrow> + (Inum ((x::int) # bs) (CN 0 n a) = Inum (x # bs) t) \<and> numbound0 a" (is "\<And>n a. ?S t = (n,a) \<Longrightarrow> (?I x (CN 0 n a) = ?I x t) \<and> ?N a") proof (induct t rule: zsplit0.induct) case (1 c n a) @@ -1308,7 +1309,7 @@ qed simp_all -consts a_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm" -- {* adjust the coeffitients of a formula *} +consts a_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm" -- {* adjust the coefficients of a formula *} recdef a_\<beta> "measure size" "a_\<beta> (And p q) = (\<lambda>k. And (a_\<beta> p k) (a_\<beta> q k))" "a_\<beta> (Or p q) = (\<lambda>k. Or (a_\<beta> p k) (a_\<beta> q k))" @@ -1428,110 +1429,147 @@ by simp_all fix a from 4 have "\<forall>x < (- Inum (a#bs) e). c*x + Inum (x#bs) e \<noteq> 0" - proof(clarsimp) - fix x assume "x < (- Inum (a#bs) e)" and"x + Inum (x#bs) e = 0" + proof clarsimp + fix x + assume "x < (- Inum (a#bs) e)" and"x + Inum (x # bs) e = 0" with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"] show "False" by simp qed then show ?case by auto next - case (5 c e) then have c1: "c=1" and nb: "numbound0 e" by simp_all + case (5 c e) + then have c1: "c = 1" and nb: "numbound0 e" + by simp_all fix a from 5 have "\<forall>x<(- Inum (a#bs) e). c*x + Inum (x#bs) e < 0" - proof(clarsimp) - fix x assume "x < (- Inum (a#bs) e)" + proof clarsimp + fix x + assume "x < (- Inum (a#bs) e)" with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"] - show "x + Inum (x#bs) e < 0" by simp + show "x + Inum (x # bs) e < 0" + by simp qed then show ?case by auto next - case (6 c e) then have c1: "c=1" and nb: "numbound0 e" by simp_all + case (6 c e) + then have c1: "c = 1" and nb: "numbound0 e" + by simp_all fix a from 6 have "\<forall>x<(- Inum (a#bs) e). c*x + Inum (x#bs) e \<le> 0" - proof(clarsimp) - fix x assume "x < (- Inum (a#bs) e)" + proof clarsimp + fix x + assume "x < (- Inum (a#bs) e)" with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"] show "x + Inum (x#bs) e \<le> 0" by simp qed then show ?case by auto next - case (7 c e) then have c1: "c=1" and nb: "numbound0 e" by simp_all + case (7 c e) + then have c1: "c = 1" and nb: "numbound0 e" + by simp_all fix a from 7 have "\<forall>x<(- Inum (a#bs) e). \<not> (c*x + Inum (x#bs) e > 0)" - proof(clarsimp) - fix x assume "x < (- Inum (a#bs) e)" and"x + Inum (x#bs) e > 0" + proof clarsimp + fix x + assume "x < (- Inum (a#bs) e)" and"x + Inum (x#bs) e > 0" with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"] - show "False" by simp + show False by simp qed then show ?case by auto next - case (8 c e) then have c1: "c=1" and nb: "numbound0 e" by simp_all + case (8 c e) + then have c1: "c = 1" and nb: "numbound0 e" + by simp_all fix a from 8 have "\<forall>x<(- Inum (a#bs) e). \<not> (c*x + Inum (x#bs) e \<ge> 0)" - proof(clarsimp) - fix x assume "x < (- Inum (a#bs) e)" and"x + Inum (x#bs) e \<ge> 0" + proof clarsimp + fix x + assume "x < (- Inum (a#bs) e)" and "x + Inum (x#bs) e \<ge> 0" with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"] - show "False" by simp + show False by simp qed then show ?case by auto qed auto lemma minusinf_repeats: - assumes d: "d_\<delta> p d" and linp: "iszlfm p" - shows "Ifm bbs ((x - k*d)#bs) (minusinf p) = Ifm bbs (x #bs) (minusinf p)" + assumes d: "d_\<delta> p d" + and linp: "iszlfm p" + shows "Ifm bbs ((x - k * d) # bs) (minusinf p) = Ifm bbs (x # bs) (minusinf p)" using linp d proof (induct p rule: iszlfm.induct) case (9 i c e) - then have nbe: "numbound0 e" and id: "i dvd d" by simp_all - then have "\<exists>k. d=i*k" by (simp add: dvd_def) - then obtain "di" where di_def: "d=i*di" by blast + then have nbe: "numbound0 e" and id: "i dvd d" + by simp_all + then have "\<exists>k. d = i * k" + by (simp add: dvd_def) + then obtain "di" where di_def: "d = i * di" + by blast show ?case proof (simp add: numbound0_I[OF nbe,where bs="bs" and b="x - k * d" and b'="x"] right_diff_distrib, rule iffI) - assume "i dvd c * x - c*(k*d) + Inum (x # bs) e" + assume "i dvd c * x - c * (k * d) + Inum (x # bs) e" (is "?ri dvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri dvd ?rt") - then have "\<exists>(l::int). ?rt = i * l" by (simp add: dvd_def) - then have "\<exists>(l::int). c*x+ ?I x e = i*l+c*(k * i*di)" + then have "\<exists>l::int. ?rt = i * l" + by (simp add: dvd_def) + then have "\<exists>l::int. c*x+ ?I x e = i * l + c * (k * i * di)" by (simp add: algebra_simps di_def) - then have "\<exists>(l::int). c*x+ ?I x e = i*(l + c*k*di)" + then have "\<exists>l::int. c*x+ ?I x e = i*(l + c * k * di)" by (simp add: algebra_simps) - then have "\<exists>(l::int). c*x+ ?I x e = i*l" by blast - then show "i dvd c*x + Inum (x # bs) e" by (simp add: dvd_def) + then have "\<exists>l::int. c * x + ?I x e = i * l" + by blast + then show "i dvd c * x + Inum (x # bs) e" + by (simp add: dvd_def) next - assume "i dvd c*x + Inum (x # bs) e" (is "?ri dvd ?rc*?rx+?e") - then have "\<exists>(l::int). c*x+?e = i*l" by (simp add: dvd_def) - then have "\<exists>(l::int). c*x - c*(k*d) +?e = i*l - c*(k*d)" by simp - then have "\<exists>(l::int). c*x - c*(k*d) +?e = i*l - c*(k*i*di)" by (simp add: di_def) - then have "\<exists>(l::int). c*x - c*(k*d) +?e = i*((l - c*k*di))" by (simp add: algebra_simps) - then have "\<exists>(l::int). c*x - c * (k*d) +?e = i*l" by blast - then show "i dvd c*x - c*(k*d) + Inum (x # bs) e" by (simp add: dvd_def) + assume "i dvd c*x + Inum (x # bs) e" (is "?ri dvd ?rc * ?rx + ?e") + then have "\<exists>l::int. c * x + ?e = i * l" + by (simp add: dvd_def) + then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * l - c * (k * d)" + by simp + then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * l - c * (k * i * di)" + by (simp add: di_def) + then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * ((l - c * k * di))" + by (simp add: algebra_simps) + then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * l" + by blast + then show "i dvd c * x - c * (k * d) + Inum (x # bs) e" + by (simp add: dvd_def) qed next case (10 i c e) - then have nbe: "numbound0 e" and id: "i dvd d" by simp_all - then have "\<exists>k. d=i*k" by (simp add: dvd_def) - then obtain "di" where di_def: "d=i*di" by blast + then have nbe: "numbound0 e" and id: "i dvd d" + by simp_all + then have "\<exists>k. d = i * k" + by (simp add: dvd_def) + then obtain di where di_def: "d = i * di" + by blast show ?case - proof(simp add: numbound0_I[OF nbe,where bs="bs" and b="x - k * d" and b'="x"] right_diff_distrib, rule iffI) - assume "i dvd c * x - c*(k*d) + Inum (x # bs) e" + proof (simp add: numbound0_I[OF nbe,where bs="bs" and b="x - k * d" and b'="x"] right_diff_distrib, rule iffI) + assume "i dvd c * x - c * (k * d) + Inum (x # bs) e" (is "?ri dvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri dvd ?rt") - then have "\<exists>(l::int). ?rt = i * l" by (simp add: dvd_def) - then have "\<exists>(l::int). c*x+ ?I x e = i*l+c*(k * i*di)" + then have "\<exists>l::int. ?rt = i * l" + by (simp add: dvd_def) + then have "\<exists>l::int. c * x + ?I x e = i * l + c * (k * i * di)" by (simp add: algebra_simps di_def) - then have "\<exists>(l::int). c*x+ ?I x e = i*(l + c*k*di)" + then have "\<exists>l::int. c * x+ ?I x e = i * (l + c * k * di)" by (simp add: algebra_simps) - then have "\<exists>(l::int). c*x+ ?I x e = i*l" by blast - then show "i dvd c*x + Inum (x # bs) e" by (simp add: dvd_def) + then have "\<exists>l::int. c * x + ?I x e = i * l" + by blast + then show "i dvd c * x + Inum (x # bs) e" + by (simp add: dvd_def) next - assume - "i dvd c*x + Inum (x # bs) e" (is "?ri dvd ?rc*?rx+?e") - then have "\<exists>(l::int). c*x+?e = i*l" by (simp add: dvd_def) - then have "\<exists>(l::int). c*x - c*(k*d) +?e = i*l - c*(k*d)" by simp - then have "\<exists>(l::int). c*x - c*(k*d) +?e = i*l - c*(k*i*di)" by (simp add: di_def) - then have "\<exists>(l::int). c*x - c*(k*d) +?e = i*((l - c*k*di))" by (simp add: algebra_simps) - then have "\<exists>(l::int). c*x - c * (k*d) +?e = i*l" + assume "i dvd c * x + Inum (x # bs) e" (is "?ri dvd ?rc * ?rx + ?e") + then have "\<exists>l::int. c * x + ?e = i * l" + by (simp add: dvd_def) + then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * l - c * (k * d)" + by simp + then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * l - c * (k * i * di)" + by (simp add: di_def) + then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * ((l - c * k * di))" + by (simp add: algebra_simps) + then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * l" by blast - then show "i dvd c*x - c*(k*d) + Inum (x # bs) e" by (simp add: dvd_def) + then show "i dvd c * x - c * (k * d) + Inum (x # bs) e" + by (simp add: dvd_def) qed qed (auto simp add: gr0_conv_Suc numbound0_I[where bs="bs" and b="x - k*d" and b'="x"]) @@ -1542,7 +1580,7 @@ lemma mirror: assumes lp: "iszlfm p" - shows "Ifm bbs (x#bs) (mirror p) = Ifm bbs ((- x)#bs) p" + shows "Ifm bbs (x # bs) (mirror p) = Ifm bbs ((- x) # bs) p" using lp proof (induct p rule: iszlfm.induct) case (9 j c e) @@ -1616,22 +1654,27 @@ qed (auto simp add: lcm_pos_int) lemma a_\<beta>: - assumes linp: "iszlfm p" and d: "d_\<beta> p l" and lp: "l > 0" + assumes linp: "iszlfm p" + and d: "d_\<beta> p l" + and lp: "l > 0" shows "iszlfm (a_\<beta> p l) \<and> d_\<beta> (a_\<beta> p l) 1 \<and> (Ifm bbs (l*x #bs) (a_\<beta> p l) = Ifm bbs (x#bs) p)" using linp d proof (induct p rule: iszlfm.induct) case (5 c e) - then have cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all - from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) - from cp have cnz: "c \<noteq> 0" by simp - have "c div c\<le> l div c" + then have cp: "c>0" and be: "numbound0 e" and d': "c dvd l" + by simp_all + from lp cp have clel: "c \<le> l" + by (simp add: zdvd_imp_le [OF d' lp]) + from cp have cnz: "c \<noteq> 0" + by simp + have "c div c \<le> l div c" by (simp add: zdiv_mono1[OF clel cp]) then have ldcp:"0 < l div c" by (simp add: div_self[OF cnz]) - have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] - by simp - then have cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] - by simp + have "c * (l div c) = c * (l div c) + l mod c" + using d' dvd_eq_mod_eq_0[of "c" "l"] by simp + then have cl: "c * (l div c) =l" + using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp then have "(l*x + (l div c) * Inum (x # bs) e < 0) = ((c * (l div c)) * x + (l div c) * Inum (x # bs) e < 0)" by simp @@ -1643,19 +1686,23 @@ using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] be by simp next case (6 c e) - then have cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all - from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) - from cp have cnz: "c \<noteq> 0" by simp + then have cp: "c > 0" and be: "numbound0 e" and d': "c dvd l" + by simp_all + from lp cp have clel: "c \<le> l" + by (simp add: zdvd_imp_le [OF d' lp]) + from cp have cnz: "c \<noteq> 0" + by simp have "c div c\<le> l div c" by (simp add: zdiv_mono1[OF clel cp]) then have ldcp:"0 < l div c" by (simp add: div_self[OF cnz]) - have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] + have "c * (l div c) = c* (l div c) + l mod c" + using d' dvd_eq_mod_eq_0[of "c" "l"] by simp + then have cl: "c * (l div c) = l" + using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp + then have "(l*x + (l div c) * Inum (x# bs) e \<le> 0) = + ((c * (l div c)) * x + (l div c) * Inum (x # bs) e \<le> 0)" by simp - then have cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] - by simp - then have "(l*x + (l div c) * Inum (x# bs) e \<le> 0) = - ((c * (l div c)) * x + (l div c) * Inum (x # bs) e \<le> 0)" by simp also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) \<le> ((l div c)) * 0)" by (simp add: algebra_simps) also have "\<dots> = (c*x + Inum (x # bs) e \<le> 0)" @@ -1664,10 +1711,68 @@ using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] be by simp next case (7 c e) - then have cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all - from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) - from cp have cnz: "c \<noteq> 0" by simp - have "c div c\<le> l div c" + then have cp: "c > 0" and be: "numbound0 e" and d': "c dvd l" + by simp_all + from lp cp have clel: "c \<le> l" + by (simp add: zdvd_imp_le [OF d' lp]) + from cp have cnz: "c \<noteq> 0" + by simp + have "c div c \<le> l div c" + by (simp add: zdiv_mono1[OF clel cp]) + then have ldcp:"0 < l div c" + by (simp add: div_self[OF cnz]) + have "c * (l div c) = c* (l div c) + l mod c" + using d' dvd_eq_mod_eq_0[of "c" "l"] by simp + then have cl:"c * (l div c) = l" + using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp + then have "(l * x + (l div c) * Inum (x # bs) e > 0) = + ((c * (l div c)) * x + (l div c) * Inum (x # bs) e > 0)" + by simp + also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) > ((l div c)) * 0)" + by (simp add: algebra_simps) + also have "\<dots> = (c * x + Inum (x # bs) e > 0)" + using zero_less_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp + by simp + finally show ?case + using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be + by simp +next + case (8 c e) + then have cp: "c > 0" and be: "numbound0 e" and d': "c dvd l" + by simp_all + from lp cp have clel: "c \<le> l" + by (simp add: zdvd_imp_le [OF d' lp]) + from cp have cnz: "c \<noteq> 0" + by simp + have "c div c \<le> l div c" + by (simp add: zdiv_mono1[OF clel cp]) + then have ldcp: "0 < l div c" + by (simp add: div_self[OF cnz]) + have "c * (l div c) = c* (l div c) + l mod c" + using d' dvd_eq_mod_eq_0[of "c" "l"] by simp + then have cl: "c * (l div c) =l" + using zmod_zdiv_equality[where a="l" and b="c", symmetric] + by simp + then have "(l*x + (l div c)* Inum (x # bs) e \<ge> 0) = + ((c*(l div c))*x + (l div c)* Inum (x # bs) e \<ge> 0)" + by simp + also have "\<dots> = ((l div c)*(c*x + Inum (x # bs) e) \<ge> ((l div c)) * 0)" + by (simp add: algebra_simps) + also have "\<dots> = (c*x + Inum (x # bs) e \<ge> 0)" + using ldcp zero_le_mult_iff [where a="l div c" and b="c*x + Inum (x # bs) e"] + by simp + finally show ?case + using be numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] + by simp +next + case (3 c e) + then have cp: "c > 0" and be: "numbound0 e" and d': "c dvd l" + by simp_all + from lp cp have clel: "c \<le> l" + by (simp add: zdvd_imp_le [OF d' lp]) + from cp have cnz: "c \<noteq> 0" + by simp + have "c div c \<le> l div c" by (simp add: zdiv_mono1[OF clel cp]) then have ldcp:"0 < l div c" by (simp add: div_self[OF cnz]) @@ -1675,105 +1780,50 @@ using d' dvd_eq_mod_eq_0[of "c" "l"] by simp then have cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp - then have "(l*x + (l div c)* Inum (x # bs) e > 0) = - ((c * (l div c)) * x + (l div c) * Inum (x # bs) e > 0)" by simp - also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) > ((l div c)) * 0)" - by (simp add: algebra_simps) - also have "\<dots> = (c * x + Inum (x # bs) e > 0)" - using zero_less_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp by simp - finally show ?case - using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be by simp -next - case (8 c e) - then have cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all - from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) - from cp have cnz: "c \<noteq> 0" by simp - have "c div c\<le> l div c" - by (simp add: zdiv_mono1[OF clel cp]) - then have ldcp:"0 < l div c" - by (simp add: div_self[OF cnz]) - have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] - by simp - then have cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] + then have "(l * x + (l div c) * Inum (x # bs) e = 0) = + ((c * (l div c)) * x + (l div c) * Inum (x # bs) e = 0)" by simp - then have "(l*x + (l div c)* Inum (x # bs) e \<ge> 0) = - ((c*(l div c))*x + (l div c)* Inum (x # bs) e \<ge> 0)" by simp - also have "\<dots> = ((l div c)*(c*x + Inum (x # bs) e) \<ge> ((l div c)) * 0)" - by (simp add: algebra_simps) - also have "\<dots> = (c*x + Inum (x # bs) e \<ge> 0)" - using ldcp zero_le_mult_iff [where a="l div c" and b="c*x + Inum (x # bs) e"] by simp - finally show ?case - using be numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] by simp -next - case (3 c e) - then have cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all - from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) - from cp have cnz: "c \<noteq> 0" by simp - have "c div c\<le> l div c" - by (simp add: zdiv_mono1[OF clel cp]) - then have ldcp:"0 < l div c" - by (simp add: div_self[OF cnz]) - have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] - by simp - then have cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] - by simp - then have "(l * x + (l div c) * Inum (x # bs) e = 0) = - ((c * (l div c)) * x + (l div c) * Inum (x # bs) e = 0)" by simp also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) = ((l div c)) * 0)" by (simp add: algebra_simps) also have "\<dots> = (c * x + Inum (x # bs) e = 0)" - using mult_eq_0_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp by simp + using mult_eq_0_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp + by simp finally show ?case - using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be by simp + using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be + by simp next case (4 c e) - then have cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all - from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) - from cp have cnz: "c \<noteq> 0" by simp - have "c div c\<le> l div c" + then have cp: "c > 0" and be: "numbound0 e" and d': "c dvd l" + by simp_all + from lp cp have clel: "c \<le> l" + by (simp add: zdvd_imp_le [OF d' lp]) + from cp have cnz: "c \<noteq> 0" + by simp + have "c div c \<le> l div c" by (simp add: zdiv_mono1[OF clel cp]) then have ldcp:"0 < l div c" by (simp add: div_self[OF cnz]) - have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] - by simp - then have cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] + have "c * (l div c) = c* (l div c) + l mod c" + using d' dvd_eq_mod_eq_0[of "c" "l"] by simp + then have cl: "c * (l div c) = l" + using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp + then have "(l * x + (l div c) * Inum (x # bs) e \<noteq> 0) \<longleftrightarrow> + (c * (l div c)) * x + (l div c) * Inum (x # bs) e \<noteq> 0" by simp - then have "(l * x + (l div c) * Inum (x # bs) e \<noteq> 0) = - ((c * (l div c)) * x + (l div c) * Inum (x # bs) e \<noteq> 0)" by simp - also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) \<noteq> ((l div c)) * 0)" + also have "\<dots> \<longleftrightarrow> (l div c) * (c * x + Inum (x # bs) e) \<noteq> (l div c) * 0" by (simp add: algebra_simps) - also have "\<dots> = (c * x + Inum (x # bs) e \<noteq> 0)" - using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp by simp + also have "\<dots> \<longleftrightarrow> c * x + Inum (x # bs) e \<noteq> 0" + using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp + by simp finally show ?case - using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be by simp + using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be + by simp next case (9 j c e) - then have cp: "c>0" and be: "numbound0 e" and jp: "j > 0" and d': "c dvd l" by simp_all - from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) - from cp have cnz: "c \<noteq> 0" by simp - have "c div c\<le> l div c" - by (simp add: zdiv_mono1[OF clel cp]) - then have ldcp:"0 < l div c" - by (simp add: div_self[OF cnz]) - have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] - by simp - then have cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] - by simp - then have "(\<exists>(k::int). l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) = - (\<exists>(k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)" by simp - also have "\<dots> = (\<exists>(k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c)*0)" - by (simp add: algebra_simps) - also have "\<dots> = (\<exists>(k::int). c * x + Inum (x # bs) e - j * k = 0)" - using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k"] ldcp - by simp - also have "\<dots> = (\<exists>(k::int). c * x + Inum (x # bs) e = j * k)" by simp - finally show ?case - using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be mult_strict_mono[OF ldcp jp ldcp ] - by (simp add: dvd_def) -next - case (10 j c e) - then have cp: "c>0" and be: "numbound0 e" and jp: "j > 0" and d': "c dvd l" by simp_all - from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) + then have cp: "c > 0" and be: "numbound0 e" and jp: "j > 0" and d': "c dvd l" + by simp_all + from lp cp have clel: "c \<le> l" + by (simp add: zdvd_imp_le [OF d' lp]) from cp have cnz: "c \<noteq> 0" by simp have "c div c\<le> l div c" by (simp add: zdiv_mono1[OF clel cp]) @@ -1781,25 +1831,70 @@ by (simp add: div_self[OF cnz]) have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp - then have cl:"c * (l div c) =l" + then have cl: "c * (l div c) = l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp - then have "(\<exists>(k::int). l * x + (l div c) * Inum (x # bs) e = - ((l div c) * j) * k) = (\<exists>(k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)" + then have "(\<exists>k::int. l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) \<longleftrightarrow> + (\<exists>(k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)" + by simp + also have "\<dots> \<longleftrightarrow> (\<exists>(k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c) * 0)" + by (simp add: algebra_simps) + also + fix k + have "\<dots> \<longleftrightarrow> (\<exists>k::int. c * x + Inum (x # bs) e - j * k = 0)" + using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k"] ldcp + by simp + also have "\<dots> \<longleftrightarrow> (\<exists>k::int. c * x + Inum (x # bs) e = j * k)" + by simp + finally show ?case + using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] + be mult_strict_mono[OF ldcp jp ldcp ] + by (simp add: dvd_def) +next + case (10 j c e) + then have cp: "c > 0" and be: "numbound0 e" and jp: "j > 0" and d': "c dvd l" + by simp_all + from lp cp have clel: "c \<le> l" + by (simp add: zdvd_imp_le [OF d' lp]) + from cp have cnz: "c \<noteq> 0" by simp - also have "\<dots> = (\<exists>(k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c)*0)" by (simp add: algebra_simps) - also fix k have "\<dots> = (\<exists>(k::int). c * x + Inum (x # bs) e - j * k = 0)" - using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k"] ldcp by simp - also have "\<dots> = (\<exists>(k::int). c * x + Inum (x # bs) e = j * k)" by simp - finally show ?case using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be mult_strict_mono[OF ldcp jp ldcp ] by (simp add: dvd_def) + have "c div c \<le> l div c" + by (simp add: zdiv_mono1[OF clel cp]) + then have ldcp: "0 < l div c" + by (simp add: div_self[OF cnz]) + have "c * (l div c) = c* (l div c) + l mod c" + using d' dvd_eq_mod_eq_0[of "c" "l"] by simp + then have cl:"c * (l div c) =l" + using zmod_zdiv_equality[where a="l" and b="c", symmetric] + by simp + then have "(\<exists>k::int. l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) \<longleftrightarrow> + (\<exists>k::int. (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)" + by simp + also have "\<dots> \<longleftrightarrow> (\<exists>k::int. (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c) * 0)" + by (simp add: algebra_simps) + also + fix k + have "\<dots> = (\<exists>k::int. c * x + Inum (x # bs) e - j * k = 0)" + using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k"] ldcp + by simp + also have "\<dots> = (\<exists>k::int. c * x + Inum (x # bs) e = j * k)" + by simp + finally show ?case + using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be + mult_strict_mono[OF ldcp jp ldcp ] + by (simp add: dvd_def) qed (auto simp add: gr0_conv_Suc numbound0_I[where bs="bs" and b="(l * x)" and b'="x"]) -lemma a_\<beta>_ex: assumes linp: "iszlfm p" and d: "d_\<beta> p l" and lp: "l>0" - shows "(\<exists>x. l dvd x \<and> Ifm bbs (x #bs) (a_\<beta> p l)) = (\<exists>(x::int). Ifm bbs (x#bs) p)" - (is "(\<exists>x. l dvd x \<and> ?P x) = (\<exists>x. ?P' x)") +lemma a_\<beta>_ex: + assumes linp: "iszlfm p" + and d: "d_\<beta> p l" + and lp: "l > 0" + shows "(\<exists>x. l dvd x \<and> Ifm bbs (x #bs) (a_\<beta> p l)) \<longleftrightarrow> (\<exists>x::int. Ifm bbs (x#bs) p)" + (is "(\<exists>x. l dvd x \<and> ?P x) \<longleftrightarrow> (\<exists>x. ?P' x)") proof- - have "(\<exists>x. l dvd x \<and> ?P x) = (\<exists>(x::int). ?P (l*x))" + have "(\<exists>x. l dvd x \<and> ?P x) \<longleftrightarrow> (\<exists>(x::int). ?P (l*x))" using unity_coeff_ex[where l="l" and P="?P", simplified] by simp - also have "\<dots> = (\<exists>(x::int). ?P' x)" using a_\<beta>[OF linp d lp] by simp + also have "\<dots> = (\<exists>x::int. ?P' x)" + using a_\<beta>[OF linp d lp] by simp finally show ?thesis . qed @@ -2157,7 +2252,7 @@ lq: "iszlfm ?q" and Bn: "\<forall>b\<in> set ?B. numbound0 b" by auto from zlin_qfree[OF lq] have qfq: "qfree ?q" . - from simpfm_qf[OF minusinf_qfree[OF qfq]] have qfmq: "qfree ?smq". + from simpfm_qf[OF minusinf_qfree[OF qfq]] have qfmq: "qfree ?smq" . have jsnb: "\<forall>j \<in> set ?js. numbound0 (C j)" by simp then have "\<forall>j\<in> set ?js. bound0 (subst0 (C j) ?smq)" by (auto simp only: subst0_bound0[OF qfmq]) @@ -2174,10 +2269,13 @@ by auto from evaldjf_bound0 [OF th'] have qdb: "bound0 ?qd" by simp from mdb qdb - have mdqdb: "bound0 (disj ?md ?qd)" unfolding disj_def by (cases "?md=T \<or> ?qd=T") simp_all + have mdqdb: "bound0 (disj ?md ?qd)" + unfolding disj_def by (cases "?md=T \<or> ?qd=T") simp_all from trans [OF pq_ex cp_thm'[OF lq uq dd dp,where i="i"]] B - have "?lhs = (\<exists>j\<in> {1.. ?d}. ?I j ?mq \<or> (\<exists>b\<in> ?N ` set ?B. Ifm bbs ((b+ j)#bs) ?q))" by auto - also have "\<dots> = (\<exists>j\<in> {1.. ?d}. ?I j ?mq \<or> (\<exists>b\<in> set ?B. Ifm bbs ((?N b+ j)#bs) ?q))" by simp + have "?lhs = (\<exists>j\<in> {1.. ?d}. ?I j ?mq \<or> (\<exists>b\<in> ?N ` set ?B. Ifm bbs ((b+ j)#bs) ?q))" + by auto + also have "\<dots> = (\<exists>j\<in> {1.. ?d}. ?I j ?mq \<or> (\<exists>b\<in> set ?B. Ifm bbs ((?N b+ j)#bs) ?q))" + by simp also have "\<dots> = ((\<exists>j\<in> {1.. ?d}. ?I j ?mq ) \<or> (\<exists>j\<in> {1.. ?d}. \<exists>b\<in> set ?B. Ifm bbs ((?N (Add b (C j)))#bs) ?q))" by (simp only: Inum.simps) blast @@ -2195,27 +2293,38 @@ also have "\<dots> = (?I i ?md \<or> (?I i (evaldjf (\<lambda>(b,j). simpfm (subst0 (Add b (C j)) ?q)) ?Bjs)))" by (simp only: evaldjf_ex[where bs="i#bs" and f="\<lambda>(b,j). simpfm (subst0 (Add b (C j)) ?q)" and ps="?Bjs"]) (auto simp add: split_def) - finally have mdqd: "?lhs = (?I i ?md \<or> ?I i ?qd)" by simp - also have "\<dots> = (?I i (disj ?md ?qd))" by (simp add: disj) - also have "\<dots> = (Ifm bbs bs (decr (disj ?md ?qd)))" by (simp only: decr [OF mdqdb]) + finally have mdqd: "?lhs = (?I i ?md \<or> ?I i ?qd)" + by simp + also have "\<dots> = (?I i (disj ?md ?qd))" + by (simp add: disj) + also have "\<dots> = (Ifm bbs bs (decr (disj ?md ?qd)))" + by (simp only: decr [OF mdqdb]) finally have mdqd2: "?lhs = (Ifm bbs bs (decr (disj ?md ?qd)))" . - { assume mdT: "?md = T" - then have cT:"cooper p = T" + { + assume mdT: "?md = T" + then have cT: "cooper p = T" by (simp only: cooper_def unit_def split_def Let_def if_True) simp - from mdT have lhs:"?lhs" using mdqd by simp - from mdT have "?rhs" by (simp add: cooper_def unit_def split_def) - with lhs cT have ?thesis by simp } + from mdT have lhs: "?lhs" + using mdqd by simp + from mdT have "?rhs" + by (simp add: cooper_def unit_def split_def) + with lhs cT have ?thesis by simp + } moreover - { assume mdT: "?md \<noteq> T" then have "cooper p = decr (disj ?md ?qd)" + { + assume mdT: "?md \<noteq> T" + then have "cooper p = decr (disj ?md ?qd)" by (simp only: cooper_def unit_def split_def Let_def if_False) - with mdqd2 decr_qf[OF mdqdb] have ?thesis by simp } + with mdqd2 decr_qf[OF mdqdb] have ?thesis + by simp + } ultimately show ?thesis by blast qed -definition pa :: "fm \<Rightarrow> fm" where - "pa p = qelim (prep p) cooper" +definition pa :: "fm \<Rightarrow> fm" + where "pa p = qelim (prep p) cooper" -theorem mirqe: "(Ifm bbs bs (pa p) = Ifm bbs bs p) \<and> qfree (pa p)" +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) definition cooper_test :: "unit \<Rightarrow> fm" @@ -2436,7 +2545,7 @@ by cooper lemma "\<not> (\<forall>(x::int). - (2 dvd x \<longleftrightarrow> (ALL(y::int). x \<noteq> 2*y+1) \<or> + (2 dvd x \<longleftrightarrow> (\<forall>(y::int). x \<noteq> 2*y+1) \<or> (\<exists>(q::int) (u::int) i. 3*i + 2*q - u < 17) \<longrightarrow> 0 < x \<or> (\<not> 3 dvd x \<and> x + 8 = 0)))" by cooper