src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
 changeset 45499 849d697adf1e parent 44064 5bce8ff0d9ae child 47108 2a1953f0d20d
```     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Nov 14 09:49:05 2011 +0100
1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Nov 14 19:35:05 2011 +0100
1.3 @@ -25,7 +25,7 @@
1.4  | "tmsize (CNP n c a) = 3 + polysize c + tmsize a "
1.5
1.6    (* Semantics of terms tm *)
1.7 -primrec Itm :: "'a::{field_char_0, field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a" where
1.8 +primrec Itm :: "'a::{field_char_0, field_inverse_zero, number_ring} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a" where
1.9    "Itm vs bs (CP c) = (Ipoly vs c)"
1.10  | "Itm vs bs (Bound n) = bs!n"
1.11  | "Itm vs bs (Neg a) = -(Itm vs bs a)"
1.12 @@ -266,9 +266,6 @@
1.13  lemma tmneg[simp]: "Itm vs bs (tmneg t) = Itm vs bs (Neg t)"
1.14  using tmneg_def[of t]
1.15  apply simp
1.16 -apply (subst number_of_Min)
1.17 -apply (simp only: of_int_minus)
1.18 -apply simp
1.19  done
1.20
1.21  lemma tmneg_nb0[simp]: "tmbound0 t \<Longrightarrow> tmbound0 (tmneg t)"
1.22 @@ -309,7 +306,7 @@
1.23
1.24  lemma polynate_stupid:
1.25    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.26 -  shows "polynate t = 0\<^sub>p \<Longrightarrow> Ipoly bs t = (0::'a::{field_char_0, field_inverse_zero})"
1.27 +  shows "polynate t = 0\<^sub>p \<Longrightarrow> Ipoly bs t = (0::'a)"
1.28  apply (subst polynate[symmetric])
1.29  apply simp
1.30  done
1.31 @@ -433,7 +430,7 @@
1.32  by (induct p rule: fmsize.induct) simp_all
1.33
1.34    (* Semantics of formulae (fm) *)
1.35 -primrec Ifm ::"'a::{linordered_field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> bool" where
1.36 +primrec Ifm ::"'a::{linordered_field_inverse_zero, number_ring} list \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> bool" where
1.37    "Ifm vs bs T = True"
1.38  | "Ifm vs bs F = False"
1.39  | "Ifm vs bs (Lt a) = (Itm vs bs a < 0)"
1.40 @@ -1798,28 +1795,12 @@
1.41    ultimately show ?case by blast
1.42  qed (auto simp add: tmbound0_I[where vs=vs and bs="bs" and b="y" and b'="x"] bound0_I[where vs=vs and bs="bs" and b="y" and b'="x"])
1.43
1.44 -lemma one_plus_one_pos[simp]: "(1::'a::{linordered_field}) + 1 > 0"
1.45 -proof-
1.46 -  have op: "(1::'a) > 0" by simp
1.47 -  from add_pos_pos[OF op op] show ?thesis .
1.48 -qed
1.49 -
1.50 -lemma one_plus_one_nonzero[simp]: "(1::'a::{linordered_field}) + 1 \<noteq> 0"
1.51 -  using one_plus_one_pos[where ?'a = 'a] by (simp add: less_le)
1.52 -
1.53 -lemma half_sum_eq: "(u + u) / (1+1) = (u::'a::{linordered_field})"
1.54 -proof-
1.55 -  have "(u + u) = (1 + 1) * u" by (simp add: field_simps)
1.56 -  hence "(u + u) / (1+1) = (1 + 1)*u / (1 + 1)" by simp
1.57 -  with nonzero_mult_divide_cancel_left[OF one_plus_one_nonzero, of u] show ?thesis by simp
1.58 -qed
1.59 -
1.60  lemma inf_uset:
1.61    assumes lp: "islin p"
1.62    and nmi: "\<not> (Ifm vs (x#bs) (minusinf p))" (is "\<not> (Ifm vs (x#bs) (?M p))")
1.63    and npi: "\<not> (Ifm vs (x#bs) (plusinf p))" (is "\<not> (Ifm vs (x#bs) (?P p))")
1.64    and ex: "\<exists> x.  Ifm vs (x#bs) p" (is "\<exists> x. ?I x p")
1.65 -  shows "\<exists> (c,t) \<in> set (uset p). \<exists> (d,s) \<in> set (uset p). ?I ((- Itm vs (x#bs) t / Ipoly vs c + - Itm vs (x#bs) s / Ipoly vs d) / (1 + 1)) p"
1.66 +  shows "\<exists> (c,t) \<in> set (uset p). \<exists> (d,s) \<in> set (uset p). ?I ((- Itm vs (x#bs) t / Ipoly vs c + - Itm vs (x#bs) s / Ipoly vs d) / 2) p"
1.67  proof-
1.68    let ?Nt = "\<lambda> x t. Itm vs (x#bs) t"
1.69    let ?N = "Ipoly vs"
1.70 @@ -1829,7 +1810,7 @@
1.71    have nmi': "\<not> (?I a (?M p))" by simp
1.72    from bound0_I[OF plusinf_nb[OF lp], where bs="bs" and b="x" and b'="a"] npi
1.73    have npi': "\<not> (?I a (?P p))" by simp
1.74 -  have "\<exists> (c,t) \<in> set (uset p). \<exists> (d,s) \<in> set (uset p). ?I ((- ?Nt a t/?N c + - ?Nt a s /?N d) / (1 + 1)) p"
1.75 +  have "\<exists> (c,t) \<in> set (uset p). \<exists> (d,s) \<in> set (uset p). ?I ((- ?Nt a t/?N c + - ?Nt a s /?N d) / 2) p"
1.76    proof-
1.77      let ?M = "(\<lambda> (c,t). - ?Nt a t / ?N c) ` ?U"
1.78      have fM: "finite ?M" by auto
1.79 @@ -1858,8 +1839,8 @@
1.80      moreover {fix u assume um: "u\<in> ?M" and pu: "?I u p"
1.81        hence "\<exists> (nu,tu) \<in> ?U. u = - ?Nt a tu / ?N nu" by auto
1.82        then obtain "tu" "nu" where tuU: "(nu,tu) \<in> ?U" and tuu:"u= - ?Nt a tu / ?N nu" by blast
1.83 -      from half_sum_eq[of u] pu tuu
1.84 -      have "?I (((- ?Nt a tu / ?N nu) + (- ?Nt a tu / ?N nu)) / (1 + 1)) p" by simp
1.85 +      from pu tuu
1.86 +      have "?I (((- ?Nt a tu / ?N nu) + (- ?Nt a tu / ?N nu)) / 2) p" by simp
1.87        with tuU have ?thesis by blast}
1.88      moreover{
1.89        assume "\<exists> t1\<in> ?M. \<exists> t2 \<in> ?M. (\<forall> y. t1 < y \<and> y < t2 \<longrightarrow> y \<notin> ?M) \<and> t1 < a \<and> a < t2 \<and> ?I a p"
1.90 @@ -1871,18 +1852,18 @@
1.91        from t2M have "\<exists> (t2n,t2u) \<in> ?U. t2 = - ?Nt a t2u / ?N t2n" by auto
1.92        then obtain "t2u" "t2n" where t2uU: "(t2n,t2u) \<in> ?U" and t2u: "t2 = - ?Nt a t2u / ?N t2n" by blast
1.93        from t1x xt2 have t1t2: "t1 < t2" by simp
1.94 -      let ?u = "(t1 + t2) / (1 + 1)"
1.95 +      let ?u = "(t1 + t2) / 2"
1.96        from less_half_sum[OF t1t2] gt_half_sum[OF t1t2] have t1lu: "t1 < ?u" and ut2: "?u < t2" by auto
1.97        from lin_dense[OF lp noM t1x xt2 px t1lu ut2] have "?I ?u p" .
1.98        with t1uU t2uU t1u t2u have ?thesis by blast}
1.99      ultimately show ?thesis by blast
1.100    qed
1.101    then obtain "l" "n" "s"  "m" where lnU: "(n,l) \<in> ?U" and smU:"(m,s) \<in> ?U"
1.102 -    and pu: "?I ((- ?Nt a l / ?N n + - ?Nt a s / ?N m) / (1 + 1)) p" by blast
1.103 +    and pu: "?I ((- ?Nt a l / ?N n + - ?Nt a s / ?N m) / 2) p" by blast
1.104    from lnU smU uset_l[OF lp] have nbl: "tmbound0 l" and nbs: "tmbound0 s" by auto
1.105    from tmbound0_I[OF nbl, where bs="bs" and b="a" and b'="x"]
1.106      tmbound0_I[OF nbs, where bs="bs" and b="a" and b'="x"] pu
1.107 -  have "?I ((- ?Nt x l / ?N n + - ?Nt x s / ?N m) / (1 + 1)) p" by simp
1.108 +  have "?I ((- ?Nt x l / ?N n + - ?Nt x s / ?N m) / 2) p" by simp
1.109    with lnU smU
1.110    show ?thesis by auto
1.111  qed
1.112 @@ -1891,7 +1872,7 @@
1.113
1.114  theorem fr_eq:
1.115    assumes lp: "islin p"
1.116 -  shows "(\<exists> x. Ifm vs (x#bs) p) = ((Ifm vs (x#bs) (minusinf p)) \<or> (Ifm vs (x#bs) (plusinf p)) \<or> (\<exists> (n,t) \<in> set (uset p). \<exists> (m,s) \<in> set (uset p). Ifm vs (((- Itm vs (x#bs) t /  Ipoly vs n + - Itm vs (x#bs) s / Ipoly vs m) /(1 + 1))#bs) p))"
1.117 +  shows "(\<exists> x. Ifm vs (x#bs) p) = ((Ifm vs (x#bs) (minusinf p)) \<or> (Ifm vs (x#bs) (plusinf p)) \<or> (\<exists> (n,t) \<in> set (uset p). \<exists> (m,s) \<in> set (uset p). Ifm vs (((- Itm vs (x#bs) t /  Ipoly vs n + - Itm vs (x#bs) s / Ipoly vs m) / 2)#bs) p))"
1.118    (is "(\<exists> x. ?I x p) = (?M \<or> ?P \<or> ?F)" is "?E = ?D")
1.119  proof
1.120    assume px: "\<exists> x. ?I x p"
1.121 @@ -1928,7 +1909,7 @@
1.122  qed
1.123
1.124  lemma msubsteq: assumes lp: "islin (Eq (CNP 0 a r))"
1.125 -  shows "Ifm vs (x#bs) (msubsteq c t d s a r) = Ifm vs (((- Itm vs (x#bs) t /  Ipoly vs c + - Itm vs (x#bs) s / Ipoly vs d) /(1 + 1))#bs) (Eq (CNP 0 a r))" (is "?lhs = ?rhs")
1.126 +  shows "Ifm vs (x#bs) (msubsteq c t d s a r) = Ifm vs (((- Itm vs (x#bs) t /  Ipoly vs c + - Itm vs (x#bs) s / Ipoly vs d) / 2)#bs) (Eq (CNP 0 a r))" (is "?lhs = ?rhs")
1.127  proof-
1.128    let ?Nt = "\<lambda>(x::'a) t. Itm vs (x#bs) t"
1.129    let ?N = "\<lambda>p. Ipoly vs p"
1.130 @@ -1946,53 +1927,47 @@
1.131      hence ?thesis  by (simp add: r[of 0] msubsteq_def Let_def evaldjf_ex)}
1.132    moreover
1.133    {assume c: "?c = 0" and d: "?d\<noteq>0"
1.134 -    from c have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = -?s / ((1 + 1)*?d)" by simp
1.135 -    have "?rhs = Ifm vs (-?s / ((1 + 1)*?d) # bs) (Eq (CNP 0 a r))" by (simp only: th)
1.136 -    also have "\<dots> \<longleftrightarrow> ?a * (-?s / ((1 + 1)*?d)) + ?r = 0" by (simp add: r[of "- (Itm vs (x # bs) s / ((1 + 1) * \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>))"])
1.137 -    also have "\<dots> \<longleftrightarrow> (1 + 1)*?d * (?a * (-?s / ((1 + 1)*?d)) + ?r) = 0"
1.138 -      using d mult_cancel_left[of "(1 + 1)*?d" "(?a * (-?s / ((1 + 1)*?d)) + ?r)" 0] by simp
1.139 -    also have "\<dots> \<longleftrightarrow> (- ?a * ?s) * ((1 + 1)*?d / ((1 + 1)*?d)) + (1 + 1)*?d*?r= 0"
1.140 -      by (simp add: field_simps right_distrib[of "(1 + 1)*?d"] del: right_distrib)
1.141 +    from c have th: "(- ?t / ?c + - ?s / ?d)/2 = -?s / (2*?d)" by simp
1.142 +    have "?rhs = Ifm vs (-?s / (2*?d) # bs) (Eq (CNP 0 a r))" by (simp only: th)
1.143 +    also have "\<dots> \<longleftrightarrow> ?a * (-?s / (2*?d)) + ?r = 0" by (simp add: r[of "- (Itm vs (x # bs) s / (2 * \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>))"])
1.144 +    also have "\<dots> \<longleftrightarrow> 2*?d * (?a * (-?s / (2*?d)) + ?r) = 0"
1.145 +      using d mult_cancel_left[of "2*?d" "(?a * (-?s / (2*?d)) + ?r)" 0] by simp
1.146 +    also have "\<dots> \<longleftrightarrow> (- ?a * ?s) * (2*?d / (2*?d)) + 2*?d*?r= 0"
1.147 +      by (simp add: field_simps right_distrib[of "2*?d"] del: right_distrib)
1.148
1.149 -    also have "\<dots> \<longleftrightarrow> - (?a * ?s) + (1 + 1)*?d*?r = 0" using d by simp
1.150 +    also have "\<dots> \<longleftrightarrow> - (?a * ?s) + 2*?d*?r = 0" using d by simp
1.151      finally have ?thesis using c d
1.152 -      apply (simp add: r[of "- (Itm vs (x # bs) s / ((1 + 1) * \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>))"] msubsteq_def Let_def evaldjf_ex del: one_add_one_is_two)
1.154 -      apply simp
1.155 -      done}
1.156 +      by (simp add: r[of "- (Itm vs (x # bs) s / (2 * \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>))"] msubsteq_def Let_def evaldjf_ex del: one_add_one_is_two)
1.157 +  }
1.158    moreover
1.159    {assume c: "?c \<noteq> 0" and d: "?d=0"
1.160 -    from d have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = -?t / ((1 + 1)*?c)" by simp
1.161 -    have "?rhs = Ifm vs (-?t / ((1 + 1)*?c) # bs) (Eq (CNP 0 a r))" by (simp only: th)
1.162 -    also have "\<dots> \<longleftrightarrow> ?a * (-?t / ((1 + 1)*?c)) + ?r = 0" by (simp add: r[of "- (?t/ ((1 + 1)* ?c))"])
1.163 -    also have "\<dots> \<longleftrightarrow> (1 + 1)*?c * (?a * (-?t / ((1 + 1)*?c)) + ?r) = 0"
1.164 -      using c mult_cancel_left[of "(1 + 1)*?c" "(?a * (-?t / ((1 + 1)*?c)) + ?r)" 0] by simp
1.165 -    also have "\<dots> \<longleftrightarrow> (?a * -?t)* ((1 + 1)*?c) / ((1 + 1)*?c) + (1 + 1)*?c*?r= 0"
1.166 -      by (simp add: field_simps right_distrib[of "(1 + 1)*?c"] del: right_distrib)
1.167 -    also have "\<dots> \<longleftrightarrow> - (?a * ?t) + (1 + 1)*?c*?r = 0" using c by simp
1.168 +    from d have th: "(- ?t / ?c + - ?s / ?d)/2 = -?t / (2*?c)" by simp
1.169 +    have "?rhs = Ifm vs (-?t / (2*?c) # bs) (Eq (CNP 0 a r))" by (simp only: th)
1.170 +    also have "\<dots> \<longleftrightarrow> ?a * (-?t / (2*?c)) + ?r = 0" by (simp add: r[of "- (?t/ (2 * ?c))"])
1.171 +    also have "\<dots> \<longleftrightarrow> 2*?c * (?a * (-?t / (2*?c)) + ?r) = 0"
1.172 +      using c mult_cancel_left[of "2*?c" "(?a * (-?t / (2*?c)) + ?r)" 0] by simp
1.173 +    also have "\<dots> \<longleftrightarrow> (?a * -?t)* (2*?c) / (2*?c) + 2*?c*?r= 0"
1.174 +      by (simp add: field_simps right_distrib[of "2*?c"] del: right_distrib)
1.175 +    also have "\<dots> \<longleftrightarrow> - (?a * ?t) + 2*?c*?r = 0" using c by simp
1.176      finally have ?thesis using c d
1.177 -      apply (simp add: r[of "- (?t/ ((1 + 1)*?c))"] msubsteq_def Let_def evaldjf_ex del: one_add_one_is_two)
1.179 -      apply simp
1.180 -      done }
1.181 +      by (simp add: r[of "- (?t/ (2*?c))"] msubsteq_def Let_def evaldjf_ex del: one_add_one_is_two)
1.182 +  }
1.183    moreover
1.184 -  {assume c: "?c \<noteq> 0" and d: "?d\<noteq>0" hence dc: "?c * ?d *(1 + 1) \<noteq> 0" by simp
1.185 +  {assume c: "?c \<noteq> 0" and d: "?d\<noteq>0" hence dc: "?c * ?d *2 \<noteq> 0" by simp
1.186      from add_frac_eq[OF c d, of "- ?t" "- ?s"]
1.187 -    have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)"
1.188 +    have th: "(- ?t / ?c + - ?s / ?d)/2 = - (?d * ?t + ?c* ?s )/ (2*?c*?d)"
1.190 -    have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d) # bs) (Eq (CNP 0 a r))" by (simp only: th)
1.191 -    also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)) + ?r = 0"
1.192 -      by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"])
1.193 -    also have "\<dots> \<longleftrightarrow> ((1 + 1) * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)) + ?r) =0 "
1.194 -      using c d mult_cancel_left[of "(1 + 1) * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ ((1 + 1)*?c*?d)) + ?r" 0] by simp
1.195 -    also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + (1 + 1)*?c*?d*?r =0"
1.196 +    have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ (2*?c*?d) # bs) (Eq (CNP 0 a r))" by (simp only: th)
1.197 +    also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r = 0"
1.198 +      by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"])
1.199 +    also have "\<dots> \<longleftrightarrow> (2 * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r) =0 "
1.200 +      using c d mult_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0] by simp
1.201 +    also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r =0"
1.202        using nonzero_mult_divide_cancel_left [OF dc] c d
1.203        by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
1.204      finally  have ?thesis using c d
1.205 -      apply (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"] msubsteq_def Let_def evaldjf_ex field_simps)
1.207 -      apply (simp add: field_simps)
1.208 -      done }
1.209 +      by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubsteq_def Let_def evaldjf_ex field_simps)
1.210 +  }
1.211    ultimately show ?thesis by blast
1.212  qed
1.213
1.214 @@ -2016,7 +1991,7 @@
1.215  qed
1.216
1.217  lemma msubstneq: assumes lp: "islin (Eq (CNP 0 a r))"
1.218 -  shows "Ifm vs (x#bs) (msubstneq c t d s a r) = Ifm vs (((- Itm vs (x#bs) t /  Ipoly vs c + - Itm vs (x#bs) s / Ipoly vs d) /(1 + 1))#bs) (NEq (CNP 0 a r))" (is "?lhs = ?rhs")
1.219 +  shows "Ifm vs (x#bs) (msubstneq c t d s a r) = Ifm vs (((- Itm vs (x#bs) t /  Ipoly vs c + - Itm vs (x#bs) s / Ipoly vs d) /2)#bs) (NEq (CNP 0 a r))" (is "?lhs = ?rhs")
1.220  proof-
1.221    let ?Nt = "\<lambda>(x::'a) t. Itm vs (x#bs) t"
1.222    let ?N = "\<lambda>p. Ipoly vs p"
1.223 @@ -2034,53 +2009,47 @@
1.224      hence ?thesis  by (simp add: r[of 0] msubstneq_def Let_def evaldjf_ex)}
1.225    moreover
1.226    {assume c: "?c = 0" and d: "?d\<noteq>0"
1.227 -    from c have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = -?s / ((1 + 1)*?d)" by simp
1.228 -    have "?rhs = Ifm vs (-?s / ((1 + 1)*?d) # bs) (NEq (CNP 0 a r))" by (simp only: th)
1.229 -    also have "\<dots> \<longleftrightarrow> ?a * (-?s / ((1 + 1)*?d)) + ?r \<noteq> 0" by (simp add: r[of "- (Itm vs (x # bs) s / ((1 + 1) * \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>))"])
1.230 -    also have "\<dots> \<longleftrightarrow> (1 + 1)*?d * (?a * (-?s / ((1 + 1)*?d)) + ?r) \<noteq> 0"
1.231 -      using d mult_cancel_left[of "(1 + 1)*?d" "(?a * (-?s / ((1 + 1)*?d)) + ?r)" 0] by simp
1.232 -    also have "\<dots> \<longleftrightarrow> (- ?a * ?s) * ((1 + 1)*?d / ((1 + 1)*?d)) + (1 + 1)*?d*?r\<noteq> 0"
1.233 -      by (simp add: field_simps right_distrib[of "(1 + 1)*?d"] del: right_distrib)
1.234 +    from c have th: "(- ?t / ?c + - ?s / ?d)/2 = -?s / (2*?d)" by simp
1.235 +    have "?rhs = Ifm vs (-?s / (2*?d) # bs) (NEq (CNP 0 a r))" by (simp only: th)
1.236 +    also have "\<dots> \<longleftrightarrow> ?a * (-?s / (2*?d)) + ?r \<noteq> 0" by (simp add: r[of "- (Itm vs (x # bs) s / (2 * \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>))"])
1.237 +    also have "\<dots> \<longleftrightarrow> 2*?d * (?a * (-?s / (2*?d)) + ?r) \<noteq> 0"
1.238 +      using d mult_cancel_left[of "2*?d" "(?a * (-?s / (2*?d)) + ?r)" 0] by simp
1.239 +    also have "\<dots> \<longleftrightarrow> (- ?a * ?s) * (2*?d / (2*?d)) + 2*?d*?r\<noteq> 0"
1.240 +      by (simp add: field_simps right_distrib[of "2*?d"] del: right_distrib)
1.241
1.242 -    also have "\<dots> \<longleftrightarrow> - (?a * ?s) + (1 + 1)*?d*?r \<noteq> 0" using d by simp
1.243 +    also have "\<dots> \<longleftrightarrow> - (?a * ?s) + 2*?d*?r \<noteq> 0" using d by simp
1.244      finally have ?thesis using c d
1.245 -      apply (simp add: r[of "- (Itm vs (x # bs) s / ((1 + 1) * \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>))"] msubstneq_def Let_def evaldjf_ex del: one_add_one_is_two)
1.247 -      apply simp
1.248 -      done}
1.249 +      by (simp add: r[of "- (Itm vs (x # bs) s / (2 * \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>))"] msubstneq_def Let_def evaldjf_ex del: one_add_one_is_two)
1.250 +  }
1.251    moreover
1.252    {assume c: "?c \<noteq> 0" and d: "?d=0"
1.253 -    from d have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = -?t / ((1 + 1)*?c)" by simp
1.254 -    have "?rhs = Ifm vs (-?t / ((1 + 1)*?c) # bs) (NEq (CNP 0 a r))" by (simp only: th)
1.255 -    also have "\<dots> \<longleftrightarrow> ?a * (-?t / ((1 + 1)*?c)) + ?r \<noteq> 0" by (simp add: r[of "- (?t/ ((1 + 1)* ?c))"])
1.256 -    also have "\<dots> \<longleftrightarrow> (1 + 1)*?c * (?a * (-?t / ((1 + 1)*?c)) + ?r) \<noteq> 0"
1.257 -      using c mult_cancel_left[of "(1 + 1)*?c" "(?a * (-?t / ((1 + 1)*?c)) + ?r)" 0] by simp
1.258 -    also have "\<dots> \<longleftrightarrow> (?a * -?t)* ((1 + 1)*?c) / ((1 + 1)*?c) + (1 + 1)*?c*?r \<noteq> 0"
1.259 -      by (simp add: field_simps right_distrib[of "(1 + 1)*?c"] del: right_distrib)
1.260 -    also have "\<dots> \<longleftrightarrow> - (?a * ?t) + (1 + 1)*?c*?r \<noteq> 0" using c by simp
1.261 +    from d have th: "(- ?t / ?c + - ?s / ?d)/2 = -?t / (2*?c)" by simp
1.262 +    have "?rhs = Ifm vs (-?t / (2*?c) # bs) (NEq (CNP 0 a r))" by (simp only: th)
1.263 +    also have "\<dots> \<longleftrightarrow> ?a * (-?t / (2*?c)) + ?r \<noteq> 0" by (simp add: r[of "- (?t/ (2 * ?c))"])
1.264 +    also have "\<dots> \<longleftrightarrow> 2*?c * (?a * (-?t / (2*?c)) + ?r) \<noteq> 0"
1.265 +      using c mult_cancel_left[of "2*?c" "(?a * (-?t / (2*?c)) + ?r)" 0] by simp
1.266 +    also have "\<dots> \<longleftrightarrow> (?a * -?t)* (2*?c) / (2*?c) + 2*?c*?r \<noteq> 0"
1.267 +      by (simp add: field_simps right_distrib[of "2*?c"] del: right_distrib)
1.268 +    also have "\<dots> \<longleftrightarrow> - (?a * ?t) + 2*?c*?r \<noteq> 0" using c by simp
1.269      finally have ?thesis using c d
1.270 -      apply (simp add: r[of "- (?t/ ((1 + 1)*?c))"] msubstneq_def Let_def evaldjf_ex del: one_add_one_is_two)
1.272 -      apply simp
1.273 -      done }
1.274 +      by (simp add: r[of "- (?t/ (2*?c))"] msubstneq_def Let_def evaldjf_ex del: one_add_one_is_two)
1.275 +  }
1.276    moreover
1.277 -  {assume c: "?c \<noteq> 0" and d: "?d\<noteq>0" hence dc: "?c * ?d *(1 + 1) \<noteq> 0" by simp
1.278 +  {assume c: "?c \<noteq> 0" and d: "?d\<noteq>0" hence dc: "?c * ?d *2 \<noteq> 0" by simp
1.279      from add_frac_eq[OF c d, of "- ?t" "- ?s"]
1.280 -    have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)"
1.281 +    have th: "(- ?t / ?c + - ?s / ?d)/2 = - (?d * ?t + ?c* ?s )/ (2*?c*?d)"
1.283 -    have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d) # bs) (NEq (CNP 0 a r))" by (simp only: th)
1.284 -    also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)) + ?r \<noteq> 0"
1.285 -      by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"])
1.286 -    also have "\<dots> \<longleftrightarrow> ((1 + 1) * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)) + ?r) \<noteq> 0 "
1.287 -      using c d mult_cancel_left[of "(1 + 1) * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ ((1 + 1)*?c*?d)) + ?r" 0] by simp
1.288 -    also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + (1 + 1)*?c*?d*?r \<noteq> 0"
1.289 +    have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ (2*?c*?d) # bs) (NEq (CNP 0 a r))" by (simp only: th)
1.290 +    also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r \<noteq> 0"
1.291 +      by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"])
1.292 +    also have "\<dots> \<longleftrightarrow> (2 * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r) \<noteq> 0 "
1.293 +      using c d mult_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0] by simp
1.294 +    also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r \<noteq> 0"
1.295        using nonzero_mult_divide_cancel_left[OF dc] c d
1.296        by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
1.297      finally  have ?thesis using c d
1.298 -      apply (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"] msubstneq_def Let_def evaldjf_ex field_simps)
1.300 -      apply (simp add: field_simps)
1.301 -      done }
1.302 +      by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubstneq_def Let_def evaldjf_ex field_simps)
1.303 +  }
1.304    ultimately show ?thesis by blast
1.305  qed
1.306
1.307 @@ -2111,7 +2080,7 @@
1.308
1.309  lemma msubstlt: assumes nc: "isnpoly c" and nd: "isnpoly d" and lp: "islin (Lt (CNP 0 a r))"
1.310    shows "Ifm vs (x#bs) (msubstlt c t d s a r) \<longleftrightarrow>
1.311 -  Ifm vs (((- Itm vs (x#bs) t /  Ipoly vs c + - Itm vs (x#bs) s / Ipoly vs d) /(1 + 1))#bs) (Lt (CNP 0 a r))" (is "?lhs = ?rhs")
1.312 +  Ifm vs (((- Itm vs (x#bs) t /  Ipoly vs c + - Itm vs (x#bs) s / Ipoly vs d) /2)#bs) (Lt (CNP 0 a r))" (is "?lhs = ?rhs")
1.313  proof-
1.314    let ?Nt = "\<lambda>x t. Itm vs (x#bs) t"
1.315    let ?N = "\<lambda>p. Ipoly vs p"
1.316 @@ -2129,115 +2098,105 @@
1.317      hence ?thesis  using nc nd by (simp add: polyneg_norm lt r[of 0] msubstlt_def Let_def evaldjf_ex)}
1.318    moreover
1.319    {assume dc: "?c*?d > 0"
1.320 -    from mult_pos_pos[OF one_plus_one_pos dc] have dc': "(1 + 1)*?c *?d > 0" by simp
1.321 +    from dc have dc': "2*?c *?d > 0" by simp
1.322      hence c:"?c \<noteq> 0" and d: "?d\<noteq> 0" by auto
1.323 -    from dc' have dc'': "\<not> (1 + 1)*?c *?d < 0" by simp
1.324 +    from dc' have dc'': "\<not> 2*?c *?d < 0" by simp
1.325      from add_frac_eq[OF c d, of "- ?t" "- ?s"]
1.326 -    have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)"
1.327 +    have th: "(- ?t / ?c + - ?s / ?d)/2 = - (?d * ?t + ?c* ?s )/ (2*?c*?d)"
1.329 -    have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d) # bs) (Lt (CNP 0 a r))" by (simp only: th)
1.330 -    also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)) + ?r < 0"
1.331 -      by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"])
1.332 -    also have "\<dots> \<longleftrightarrow> ((1 + 1) * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)) + ?r) < 0"
1.333 +    have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ (2*?c*?d) # bs) (Lt (CNP 0 a r))" by (simp only: th)
1.334 +    also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r < 0"
1.335 +      by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"])
1.336 +    also have "\<dots> \<longleftrightarrow> (2 * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r) < 0"
1.337
1.338 -      using dc' dc'' mult_less_cancel_left_disj[of "(1 + 1) * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ ((1 + 1)*?c*?d)) + ?r" 0] by simp
1.339 -    also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + (1 + 1)*?c*?d*?r < 0"
1.340 -      using nonzero_mult_divide_cancel_left[of "(1 + 1)*?c*?d"] c d
1.341 +      using dc' dc'' mult_less_cancel_left_disj[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0] by simp
1.342 +    also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r < 0"
1.343 +      using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d
1.344        by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
1.345      finally  have ?thesis using dc c d  nc nd dc'
1.346 -      apply (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
1.348 -    by (simp add: field_simps order_less_not_sym[OF dc])}
1.349 +      by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
1.350 +  }
1.351    moreover
1.352    {assume dc: "?c*?d < 0"
1.353
1.354 -    from dc one_plus_one_pos[where ?'a='a] have dc': "(1 + 1)*?c *?d < 0"
1.355 +    from dc have dc': "2*?c *?d < 0"
1.356        by (simp add: mult_less_0_iff field_simps)
1.357      hence c:"?c \<noteq> 0" and d: "?d\<noteq> 0" by auto
1.358      from add_frac_eq[OF c d, of "- ?t" "- ?s"]
1.359 -    have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)"
1.360 +    have th: "(- ?t / ?c + - ?s / ?d)/2 = - (?d * ?t + ?c* ?s )/ (2*?c*?d)"
1.362 -    have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d) # bs) (Lt (CNP 0 a r))" by (simp only: th)
1.363 -    also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)) + ?r < 0"
1.364 -      by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"])
1.365 +    have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ (2*?c*?d) # bs) (Lt (CNP 0 a r))" by (simp only: th)
1.366 +    also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r < 0"
1.367 +      by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"])
1.368
1.369 -    also have "\<dots> \<longleftrightarrow> ((1 + 1) * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)) + ?r) > 0"
1.370 +    also have "\<dots> \<longleftrightarrow> (2 * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r) > 0"
1.371
1.372 -      using dc' order_less_not_sym[OF dc'] mult_less_cancel_left_disj[of "(1 + 1) * ?c * ?d" 0 "?a * (- (?d * ?t + ?c* ?s)/ ((1 + 1)*?c*?d)) + ?r"] by simp
1.373 -    also have "\<dots> \<longleftrightarrow> ?a * ((?d * ?t + ?c* ?s )) - (1 + 1)*?c*?d*?r < 0"
1.374 -      using nonzero_mult_divide_cancel_left[of "(1 + 1)*?c*?d"] c d
1.375 +      using dc' order_less_not_sym[OF dc'] mult_less_cancel_left_disj[of "2 * ?c * ?d" 0 "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r"] by simp
1.376 +    also have "\<dots> \<longleftrightarrow> ?a * ((?d * ?t + ?c* ?s )) - 2*?c*?d*?r < 0"
1.377 +      using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d
1.378        by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
1.379      finally  have ?thesis using dc c d  nc nd
1.380 -      apply (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
1.382 -      by (simp add: field_simps order_less_not_sym[OF dc]) }
1.383 +      by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
1.384 +  }
1.385    moreover
1.386    {assume c: "?c > 0" and d: "?d=0"
1.387 -    from c have c'': "(1 + 1)*?c > 0" by (simp add: zero_less_mult_iff)
1.388 -    from c have c': "(1 + 1)*?c \<noteq> 0" by simp
1.389 -    from d have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?t / ((1 + 1)*?c)"  by (simp add: field_simps)
1.390 -    have "?rhs \<longleftrightarrow> Ifm vs (- ?t / ((1 + 1)*?c) # bs) (Lt (CNP 0 a r))" by (simp only: th)
1.391 -    also have "\<dots> \<longleftrightarrow> ?a* (- ?t / ((1 + 1)*?c))+ ?r < 0" by (simp add: r[of "- (?t / ((1 + 1)*?c))"])
1.392 -    also have "\<dots> \<longleftrightarrow> (1 + 1)*?c * (?a* (- ?t / ((1 + 1)*?c))+ ?r) < 0"
1.393 -      using c mult_less_cancel_left_disj[of "(1 + 1) * ?c" "?a* (- ?t / ((1 + 1)*?c))+ ?r" 0] c' c'' order_less_not_sym[OF c''] by simp
1.394 -    also have "\<dots> \<longleftrightarrow> - ?a*?t+  (1 + 1)*?c *?r < 0"
1.395 +    from c have c'': "2*?c > 0" by (simp add: zero_less_mult_iff)
1.396 +    from c have c': "2*?c \<noteq> 0" by simp
1.397 +    from d have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?t / (2*?c)"  by (simp add: field_simps)
1.398 +    have "?rhs \<longleftrightarrow> Ifm vs (- ?t / (2*?c) # bs) (Lt (CNP 0 a r))" by (simp only: th)
1.399 +    also have "\<dots> \<longleftrightarrow> ?a* (- ?t / (2*?c))+ ?r < 0" by (simp add: r[of "- (?t / (2*?c))"])
1.400 +    also have "\<dots> \<longleftrightarrow> 2*?c * (?a* (- ?t / (2*?c))+ ?r) < 0"
1.401 +      using c mult_less_cancel_left_disj[of "2 * ?c" "?a* (- ?t / (2*?c))+ ?r" 0] c' c'' order_less_not_sym[OF c''] by simp
1.402 +    also have "\<dots> \<longleftrightarrow> - ?a*?t+  2*?c *?r < 0"
1.403        using nonzero_mult_divide_cancel_left[OF c'] c
1.404        by (simp add: algebra_simps diff_divide_distrib less_le del: left_distrib)
1.405      finally have ?thesis using c d nc nd
1.406 -      apply(simp add: r[of "- (?t / ((1 + 1)*?c))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
1.408 -      using c order_less_not_sym[OF c] less_imp_neq[OF c]
1.409 -      by (simp add: field_simps )  }
1.410 +      by(simp add: r[of "- (?t / (2*?c))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
1.411 +  }
1.412    moreover
1.413 -  {assume c: "?c < 0" and d: "?d=0"  hence c': "(1 + 1)*?c \<noteq> 0" by simp
1.414 -    from c have c'': "(1 + 1)*?c < 0" by (simp add: mult_less_0_iff)
1.415 -    from d have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?t / ((1 + 1)*?c)"  by (simp add: field_simps)
1.416 -    have "?rhs \<longleftrightarrow> Ifm vs (- ?t / ((1 + 1)*?c) # bs) (Lt (CNP 0 a r))" by (simp only: th)
1.417 -    also have "\<dots> \<longleftrightarrow> ?a* (- ?t / ((1 + 1)*?c))+ ?r < 0" by (simp add: r[of "- (?t / ((1 + 1)*?c))"])
1.418 -    also have "\<dots> \<longleftrightarrow> (1 + 1)*?c * (?a* (- ?t / ((1 + 1)*?c))+ ?r) > 0"
1.419 -      using c order_less_not_sym[OF c''] less_imp_neq[OF c''] c'' mult_less_cancel_left_disj[of "(1 + 1) * ?c" 0 "?a* (- ?t / ((1 + 1)*?c))+ ?r"] by simp
1.420 -    also have "\<dots> \<longleftrightarrow> ?a*?t -  (1 + 1)*?c *?r < 0"
1.421 +  {assume c: "?c < 0" and d: "?d=0"  hence c': "2*?c \<noteq> 0" by simp
1.422 +    from c have c'': "2*?c < 0" by (simp add: mult_less_0_iff)
1.423 +    from d have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?t / (2*?c)"  by (simp add: field_simps)
1.424 +    have "?rhs \<longleftrightarrow> Ifm vs (- ?t / (2*?c) # bs) (Lt (CNP 0 a r))" by (simp only: th)
1.425 +    also have "\<dots> \<longleftrightarrow> ?a* (- ?t / (2*?c))+ ?r < 0" by (simp add: r[of "- (?t / (2*?c))"])
1.426 +    also have "\<dots> \<longleftrightarrow> 2*?c * (?a* (- ?t / (2*?c))+ ?r) > 0"
1.427 +      using c order_less_not_sym[OF c''] less_imp_neq[OF c''] c'' mult_less_cancel_left_disj[of "2 * ?c" 0 "?a* (- ?t / (2*?c))+ ?r"] by simp
1.428 +    also have "\<dots> \<longleftrightarrow> ?a*?t -  2*?c *?r < 0"
1.429        using nonzero_mult_divide_cancel_left[OF c'] c order_less_not_sym[OF c''] less_imp_neq[OF c''] c''
1.430          by (simp add: algebra_simps diff_divide_distrib del:  left_distrib)
1.431      finally have ?thesis using c d nc nd
1.432 -      apply(simp add: r[of "- (?t / ((1 + 1)*?c))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
1.434 -      using c order_less_not_sym[OF c] less_imp_neq[OF c]
1.435 -      by (simp add: field_simps )    }
1.436 +      by(simp add: r[of "- (?t / (2*?c))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
1.437 +  }
1.438    moreover
1.439    moreover
1.440    {assume c: "?c = 0" and d: "?d>0"
1.441 -    from d have d'': "(1 + 1)*?d > 0" by (simp add: zero_less_mult_iff)
1.442 -    from d have d': "(1 + 1)*?d \<noteq> 0" by simp
1.443 -    from c have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?s / ((1 + 1)*?d)"  by (simp add: field_simps)
1.444 -    have "?rhs \<longleftrightarrow> Ifm vs (- ?s / ((1 + 1)*?d) # bs) (Lt (CNP 0 a r))" by (simp only: th)
1.445 -    also have "\<dots> \<longleftrightarrow> ?a* (- ?s / ((1 + 1)*?d))+ ?r < 0" by (simp add: r[of "- (?s / ((1 + 1)*?d))"])
1.446 -    also have "\<dots> \<longleftrightarrow> (1 + 1)*?d * (?a* (- ?s / ((1 + 1)*?d))+ ?r) < 0"
1.447 -      using d mult_less_cancel_left_disj[of "(1 + 1) * ?d" "?a* (- ?s / ((1 + 1)*?d))+ ?r" 0] d' d'' order_less_not_sym[OF d''] by simp
1.448 -    also have "\<dots> \<longleftrightarrow> - ?a*?s+  (1 + 1)*?d *?r < 0"
1.449 +    from d have d'': "2*?d > 0" by (simp add: zero_less_mult_iff)
1.450 +    from d have d': "2*?d \<noteq> 0" by simp
1.451 +    from c have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?s / (2*?d)"  by (simp add: field_simps)
1.452 +    have "?rhs \<longleftrightarrow> Ifm vs (- ?s / (2*?d) # bs) (Lt (CNP 0 a r))" by (simp only: th)
1.453 +    also have "\<dots> \<longleftrightarrow> ?a* (- ?s / (2*?d))+ ?r < 0" by (simp add: r[of "- (?s / (2*?d))"])
1.454 +    also have "\<dots> \<longleftrightarrow> 2*?d * (?a* (- ?s / (2*?d))+ ?r) < 0"
1.455 +      using d mult_less_cancel_left_disj[of "2 * ?d" "?a* (- ?s / (2*?d))+ ?r" 0] d' d'' order_less_not_sym[OF d''] by simp
1.456 +    also have "\<dots> \<longleftrightarrow> - ?a*?s+  2*?d *?r < 0"
1.457        using nonzero_mult_divide_cancel_left[OF d'] d
1.458        by (simp add: algebra_simps diff_divide_distrib less_le del: left_distrib)
1.459      finally have ?thesis using c d nc nd
1.460 -      apply(simp add: r[of "- (?s / ((1 + 1)*?d))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
1.462 -      using d order_less_not_sym[OF d] less_imp_neq[OF d]
1.463 -      by (simp add: field_simps)  }
1.464 +      by(simp add: r[of "- (?s / (2*?d))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
1.465 +  }
1.466    moreover
1.467 -  {assume c: "?c = 0" and d: "?d<0"  hence d': "(1 + 1)*?d \<noteq> 0" by simp
1.468 -    from d have d'': "(1 + 1)*?d < 0" by (simp add: mult_less_0_iff)
1.469 -    from c have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?s / ((1 + 1)*?d)"  by (simp add: field_simps)
1.470 -    have "?rhs \<longleftrightarrow> Ifm vs (- ?s / ((1 + 1)*?d) # bs) (Lt (CNP 0 a r))" by (simp only: th)
1.471 -    also have "\<dots> \<longleftrightarrow> ?a* (- ?s / ((1 + 1)*?d))+ ?r < 0" by (simp add: r[of "- (?s / ((1 + 1)*?d))"])
1.472 -    also have "\<dots> \<longleftrightarrow> (1 + 1)*?d * (?a* (- ?s / ((1 + 1)*?d))+ ?r) > 0"
1.473 -      using d order_less_not_sym[OF d''] less_imp_neq[OF d''] d'' mult_less_cancel_left_disj[of "(1 + 1) * ?d" 0 "?a* (- ?s / ((1 + 1)*?d))+ ?r"] by simp
1.474 -    also have "\<dots> \<longleftrightarrow> ?a*?s -  (1 + 1)*?d *?r < 0"
1.475 +  {assume c: "?c = 0" and d: "?d<0"  hence d': "2*?d \<noteq> 0" by simp
1.476 +    from d have d'': "2*?d < 0" by (simp add: mult_less_0_iff)
1.477 +    from c have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?s / (2*?d)"  by (simp add: field_simps)
1.478 +    have "?rhs \<longleftrightarrow> Ifm vs (- ?s / (2*?d) # bs) (Lt (CNP 0 a r))" by (simp only: th)
1.479 +    also have "\<dots> \<longleftrightarrow> ?a* (- ?s / (2*?d))+ ?r < 0" by (simp add: r[of "- (?s / (2*?d))"])
1.480 +    also have "\<dots> \<longleftrightarrow> 2*?d * (?a* (- ?s / (2*?d))+ ?r) > 0"
1.481 +      using d order_less_not_sym[OF d''] less_imp_neq[OF d''] d'' mult_less_cancel_left_disj[of "2 * ?d" 0 "?a* (- ?s / (2*?d))+ ?r"] by simp
1.482 +    also have "\<dots> \<longleftrightarrow> ?a*?s -  2*?d *?r < 0"
1.483        using nonzero_mult_divide_cancel_left[OF d'] d order_less_not_sym[OF d''] less_imp_neq[OF d''] d''
1.484          by (simp add: algebra_simps diff_divide_distrib del:  left_distrib)
1.485      finally have ?thesis using c d nc nd
1.486 -      apply(simp add: r[of "- (?s / ((1 + 1)*?d))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
1.488 -      using d order_less_not_sym[OF d] less_imp_neq[OF d]
1.489 -      by (simp add: field_simps )    }
1.490 +      by(simp add: r[of "- (?s / (2*?d))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
1.491 +  }
1.492  ultimately show ?thesis by blast
1.493  qed
1.494
1.495 @@ -2267,7 +2226,7 @@
1.496
1.497  lemma msubstle: assumes nc: "isnpoly c" and nd: "isnpoly d" and lp: "islin (Le (CNP 0 a r))"
1.498    shows "Ifm vs (x#bs) (msubstle c t d s a r) \<longleftrightarrow>
1.499 -  Ifm vs (((- Itm vs (x#bs) t /  Ipoly vs c + - Itm vs (x#bs) s / Ipoly vs d) /(1 + 1))#bs) (Le (CNP 0 a r))" (is "?lhs = ?rhs")
1.500 +  Ifm vs (((- Itm vs (x#bs) t /  Ipoly vs c + - Itm vs (x#bs) s / Ipoly vs d) /2)#bs) (Le (CNP 0 a r))" (is "?lhs = ?rhs")
1.501  proof-
1.502    let ?Nt = "\<lambda>x t. Itm vs (x#bs) t"
1.503    let ?N = "\<lambda>p. Ipoly vs p"
1.504 @@ -2285,115 +2244,105 @@
1.505      hence ?thesis  using nc nd by (simp add: polyneg_norm polymul_norm lt r[of 0] msubstle_def Let_def evaldjf_ex)}
1.506    moreover
1.507    {assume dc: "?c*?d > 0"
1.508 -    from mult_pos_pos[OF one_plus_one_pos dc] have dc': "(1 + 1)*?c *?d > 0" by simp
1.509 +    from dc have dc': "2*?c *?d > 0" by simp
1.510      hence c:"?c \<noteq> 0" and d: "?d\<noteq> 0" by auto
1.511 -    from dc' have dc'': "\<not> (1 + 1)*?c *?d < 0" by simp
1.512 +    from dc' have dc'': "\<not> 2*?c *?d < 0" by simp
1.513      from add_frac_eq[OF c d, of "- ?t" "- ?s"]
1.514 -    have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)"
1.515 +    have th: "(- ?t / ?c + - ?s / ?d)/2 = - (?d * ?t + ?c* ?s )/ (2*?c*?d)"
1.517 -    have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d) # bs) (Le (CNP 0 a r))" by (simp only: th)
1.518 -    also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)) + ?r <= 0"
1.519 -      by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"])
1.520 -    also have "\<dots> \<longleftrightarrow> ((1 + 1) * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)) + ?r) <= 0"
1.521 +    have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ (2*?c*?d) # bs) (Le (CNP 0 a r))" by (simp only: th)
1.522 +    also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r <= 0"
1.523 +      by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"])
1.524 +    also have "\<dots> \<longleftrightarrow> (2 * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r) <= 0"
1.525
1.526 -      using dc' dc'' mult_le_cancel_left[of "(1 + 1) * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ ((1 + 1)*?c*?d)) + ?r" 0] by simp
1.527 -    also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + (1 + 1)*?c*?d*?r <= 0"
1.528 -      using nonzero_mult_divide_cancel_left[of "(1 + 1)*?c*?d"] c d
1.529 +      using dc' dc'' mult_le_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0] by simp
1.530 +    also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r <= 0"
1.531 +      using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d
1.532        by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
1.533      finally  have ?thesis using dc c d  nc nd dc'
1.534 -      apply (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
1.536 -    by (simp add: field_simps order_less_not_sym[OF dc])}
1.537 +      by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
1.538 +  }
1.539    moreover
1.540    {assume dc: "?c*?d < 0"
1.541
1.542 -    from dc one_plus_one_pos[where ?'a='a] have dc': "(1 + 1)*?c *?d < 0"
1.543 +    from dc have dc': "2*?c *?d < 0"
1.545      hence c:"?c \<noteq> 0" and d: "?d\<noteq> 0" by auto
1.546      from add_frac_eq[OF c d, of "- ?t" "- ?s"]
1.547 -    have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)"
1.548 +    have th: "(- ?t / ?c + - ?s / ?d)/2 = - (?d * ?t + ?c* ?s )/ (2*?c*?d)"
1.550 -    have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d) # bs) (Le (CNP 0 a r))" by (simp only: th)
1.551 -    also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)) + ?r <= 0"
1.552 -      by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"])
1.553 +    have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ (2*?c*?d) # bs) (Le (CNP 0 a r))" by (simp only: th)
1.554 +    also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r <= 0"
1.555 +      by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"])
1.556
1.557 -    also have "\<dots> \<longleftrightarrow> ((1 + 1) * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)) + ?r) >= 0"
1.558 +    also have "\<dots> \<longleftrightarrow> (2 * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r) >= 0"
1.559
1.560 -      using dc' order_less_not_sym[OF dc'] mult_le_cancel_left[of "(1 + 1) * ?c * ?d" 0 "?a * (- (?d * ?t + ?c* ?s)/ ((1 + 1)*?c*?d)) + ?r"] by simp
1.561 -    also have "\<dots> \<longleftrightarrow> ?a * ((?d * ?t + ?c* ?s )) - (1 + 1)*?c*?d*?r <= 0"
1.562 -      using nonzero_mult_divide_cancel_left[of "(1 + 1)*?c*?d"] c d
1.563 +      using dc' order_less_not_sym[OF dc'] mult_le_cancel_left[of "2 * ?c * ?d" 0 "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r"] by simp
1.564 +    also have "\<dots> \<longleftrightarrow> ?a * ((?d * ?t + ?c* ?s )) - 2*?c*?d*?r <= 0"
1.565 +      using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d
1.566        by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
1.567      finally  have ?thesis using dc c d  nc nd
1.568 -      apply (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
1.570 -      by (simp add: field_simps order_less_not_sym[OF dc]) }
1.571 +      by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
1.572 +  }
1.573    moreover
1.574    {assume c: "?c > 0" and d: "?d=0"
1.575 -    from c have c'': "(1 + 1)*?c > 0" by (simp add: zero_less_mult_iff)
1.576 -    from c have c': "(1 + 1)*?c \<noteq> 0" by simp
1.577 -    from d have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?t / ((1 + 1)*?c)"  by (simp add: field_simps)
1.578 -    have "?rhs \<longleftrightarrow> Ifm vs (- ?t / ((1 + 1)*?c) # bs) (Le (CNP 0 a r))" by (simp only: th)
1.579 -    also have "\<dots> \<longleftrightarrow> ?a* (- ?t / ((1 + 1)*?c))+ ?r <= 0" by (simp add: r[of "- (?t / ((1 + 1)*?c))"])
1.580 -    also have "\<dots> \<longleftrightarrow> (1 + 1)*?c * (?a* (- ?t / ((1 + 1)*?c))+ ?r) <= 0"
1.581 -      using c mult_le_cancel_left[of "(1 + 1) * ?c" "?a* (- ?t / ((1 + 1)*?c))+ ?r" 0] c' c'' order_less_not_sym[OF c''] by simp
1.582 -    also have "\<dots> \<longleftrightarrow> - ?a*?t+  (1 + 1)*?c *?r <= 0"
1.583 +    from c have c'': "2*?c > 0" by (simp add: zero_less_mult_iff)
1.584 +    from c have c': "2*?c \<noteq> 0" by simp
1.585 +    from d have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?t / (2*?c)"  by (simp add: field_simps)
1.586 +    have "?rhs \<longleftrightarrow> Ifm vs (- ?t / (2*?c) # bs) (Le (CNP 0 a r))" by (simp only: th)
1.587 +    also have "\<dots> \<longleftrightarrow> ?a* (- ?t / (2*?c))+ ?r <= 0" by (simp add: r[of "- (?t / (2*?c))"])
1.588 +    also have "\<dots> \<longleftrightarrow> 2*?c * (?a* (- ?t / (2*?c))+ ?r) <= 0"
1.589 +      using c mult_le_cancel_left[of "2 * ?c" "?a* (- ?t / (2*?c))+ ?r" 0] c' c'' order_less_not_sym[OF c''] by simp
1.590 +    also have "\<dots> \<longleftrightarrow> - ?a*?t+  2*?c *?r <= 0"
1.591        using nonzero_mult_divide_cancel_left[OF c'] c
1.592        by (simp add: algebra_simps diff_divide_distrib less_le del: left_distrib)
1.593      finally have ?thesis using c d nc nd
1.594 -      apply(simp add: r[of "- (?t / ((1 + 1)*?c))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
1.596 -      using c order_less_not_sym[OF c] less_imp_neq[OF c]
1.597 -      by (simp add: field_simps )  }
1.598 +      by(simp add: r[of "- (?t / (2*?c))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
1.599 +  }
1.600    moreover
1.601 -  {assume c: "?c < 0" and d: "?d=0"  hence c': "(1 + 1)*?c \<noteq> 0" by simp
1.602 -    from c have c'': "(1 + 1)*?c < 0" by (simp add: mult_less_0_iff)
1.603 -    from d have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?t / ((1 + 1)*?c)"  by (simp add: field_simps)
1.604 -    have "?rhs \<longleftrightarrow> Ifm vs (- ?t / ((1 + 1)*?c) # bs) (Le (CNP 0 a r))" by (simp only: th)
1.605 -    also have "\<dots> \<longleftrightarrow> ?a* (- ?t / ((1 + 1)*?c))+ ?r <= 0" by (simp add: r[of "- (?t / ((1 + 1)*?c))"])
1.606 -    also have "\<dots> \<longleftrightarrow> (1 + 1)*?c * (?a* (- ?t / ((1 + 1)*?c))+ ?r) >= 0"
1.607 -      using c order_less_not_sym[OF c''] less_imp_neq[OF c''] c'' mult_le_cancel_left[of "(1 + 1) * ?c" 0 "?a* (- ?t / ((1 + 1)*?c))+ ?r"] by simp
1.608 -    also have "\<dots> \<longleftrightarrow> ?a*?t -  (1 + 1)*?c *?r <= 0"
1.609 +  {assume c: "?c < 0" and d: "?d=0"  hence c': "2*?c \<noteq> 0" by simp
1.610 +    from c have c'': "2*?c < 0" by (simp add: mult_less_0_iff)
1.611 +    from d have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?t / (2*?c)"  by (simp add: field_simps)
1.612 +    have "?rhs \<longleftrightarrow> Ifm vs (- ?t / (2*?c) # bs) (Le (CNP 0 a r))" by (simp only: th)
1.613 +    also have "\<dots> \<longleftrightarrow> ?a* (- ?t / (2*?c))+ ?r <= 0" by (simp add: r[of "- (?t / (2*?c))"])
1.614 +    also have "\<dots> \<longleftrightarrow> 2*?c * (?a* (- ?t / (2*?c))+ ?r) >= 0"
1.615 +      using c order_less_not_sym[OF c''] less_imp_neq[OF c''] c'' mult_le_cancel_left[of "2 * ?c" 0 "?a* (- ?t / (2*?c))+ ?r"] by simp
1.616 +    also have "\<dots> \<longleftrightarrow> ?a*?t -  2*?c *?r <= 0"
1.617        using nonzero_mult_divide_cancel_left[OF c'] c order_less_not_sym[OF c''] less_imp_neq[OF c''] c''
1.618          by (simp add: algebra_simps diff_divide_distrib del:  left_distrib)
1.619      finally have ?thesis using c d nc nd
1.620 -      apply(simp add: r[of "- (?t / ((1 + 1)*?c))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
1.622 -      using c order_less_not_sym[OF c] less_imp_neq[OF c]
1.623 -      by (simp add: field_simps )    }
1.624 +      by(simp add: r[of "- (?t / (2*?c))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
1.625 +  }
1.626    moreover
1.627    moreover
1.628    {assume c: "?c = 0" and d: "?d>0"
1.629 -    from d have d'': "(1 + 1)*?d > 0" by (simp add: zero_less_mult_iff)
1.630 -    from d have d': "(1 + 1)*?d \<noteq> 0" by simp
1.631 -    from c have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?s / ((1 + 1)*?d)"  by (simp add: field_simps)
1.632 -    have "?rhs \<longleftrightarrow> Ifm vs (- ?s / ((1 + 1)*?d) # bs) (Le (CNP 0 a r))" by (simp only: th)
1.633 -    also have "\<dots> \<longleftrightarrow> ?a* (- ?s / ((1 + 1)*?d))+ ?r <= 0" by (simp add: r[of "- (?s / ((1 + 1)*?d))"])
1.634 -    also have "\<dots> \<longleftrightarrow> (1 + 1)*?d * (?a* (- ?s / ((1 + 1)*?d))+ ?r) <= 0"
1.635 -      using d mult_le_cancel_left[of "(1 + 1) * ?d" "?a* (- ?s / ((1 + 1)*?d))+ ?r" 0] d' d'' order_less_not_sym[OF d''] by simp
1.636 -    also have "\<dots> \<longleftrightarrow> - ?a*?s+  (1 + 1)*?d *?r <= 0"
1.637 +    from d have d'': "2*?d > 0" by (simp add: zero_less_mult_iff)
1.638 +    from d have d': "2*?d \<noteq> 0" by simp
1.639 +    from c have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?s / (2*?d)"  by (simp add: field_simps)
1.640 +    have "?rhs \<longleftrightarrow> Ifm vs (- ?s / (2*?d) # bs) (Le (CNP 0 a r))" by (simp only: th)
1.641 +    also have "\<dots> \<longleftrightarrow> ?a* (- ?s / (2*?d))+ ?r <= 0" by (simp add: r[of "- (?s / (2*?d))"])
1.642 +    also have "\<dots> \<longleftrightarrow> 2*?d * (?a* (- ?s / (2*?d))+ ?r) <= 0"
1.643 +      using d mult_le_cancel_left[of "2 * ?d" "?a* (- ?s / (2*?d))+ ?r" 0] d' d'' order_less_not_sym[OF d''] by simp
1.644 +    also have "\<dots> \<longleftrightarrow> - ?a*?s+  2*?d *?r <= 0"
1.645        using nonzero_mult_divide_cancel_left[OF d'] d
1.646        by (simp add: algebra_simps diff_divide_distrib less_le del: left_distrib)
1.647      finally have ?thesis using c d nc nd
1.648 -      apply(simp add: r[of "- (?s / ((1 + 1)*?d))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
1.650 -      using d order_less_not_sym[OF d] less_imp_neq[OF d]
1.651 -      by (simp add: field_simps )  }
1.652 +      by(simp add: r[of "- (?s / (2*?d))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
1.653 +  }
1.654    moreover
1.655 -  {assume c: "?c = 0" and d: "?d<0"  hence d': "(1 + 1)*?d \<noteq> 0" by simp
1.656 -    from d have d'': "(1 + 1)*?d < 0" by (simp add: mult_less_0_iff)
1.657 -    from c have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?s / ((1 + 1)*?d)"  by (simp add: field_simps)
1.658 -    have "?rhs \<longleftrightarrow> Ifm vs (- ?s / ((1 + 1)*?d) # bs) (Le (CNP 0 a r))" by (simp only: th)
1.659 -    also have "\<dots> \<longleftrightarrow> ?a* (- ?s / ((1 + 1)*?d))+ ?r <= 0" by (simp add: r[of "- (?s / ((1 + 1)*?d))"])
1.660 -    also have "\<dots> \<longleftrightarrow> (1 + 1)*?d * (?a* (- ?s / ((1 + 1)*?d))+ ?r) >= 0"
1.661 -      using d order_less_not_sym[OF d''] less_imp_neq[OF d''] d'' mult_le_cancel_left[of "(1 + 1) * ?d" 0 "?a* (- ?s / ((1 + 1)*?d))+ ?r"] by simp
1.662 -    also have "\<dots> \<longleftrightarrow> ?a*?s -  (1 + 1)*?d *?r <= 0"
1.663 +  {assume c: "?c = 0" and d: "?d<0"  hence d': "2*?d \<noteq> 0" by simp
1.664 +    from d have d'': "2*?d < 0" by (simp add: mult_less_0_iff)
1.665 +    from c have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?s / (2*?d)"  by (simp add: field_simps)
1.666 +    have "?rhs \<longleftrightarrow> Ifm vs (- ?s / (2*?d) # bs) (Le (CNP 0 a r))" by (simp only: th)
1.667 +    also have "\<dots> \<longleftrightarrow> ?a* (- ?s / (2*?d))+ ?r <= 0" by (simp add: r[of "- (?s / (2*?d))"])
1.668 +    also have "\<dots> \<longleftrightarrow> 2*?d * (?a* (- ?s / (2*?d))+ ?r) >= 0"
1.669 +      using d order_less_not_sym[OF d''] less_imp_neq[OF d''] d'' mult_le_cancel_left[of "2 * ?d" 0 "?a* (- ?s / (2*?d))+ ?r"] by simp
1.670 +    also have "\<dots> \<longleftrightarrow> ?a*?s -  2*?d *?r <= 0"
1.671        using nonzero_mult_divide_cancel_left[OF d'] d order_less_not_sym[OF d''] less_imp_neq[OF d''] d''
1.672          by (simp add: algebra_simps diff_divide_distrib del:  left_distrib)
1.673      finally have ?thesis using c d nc nd
1.674 -      apply(simp add: r[of "- (?s / ((1 + 1)*?d))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
1.676 -      using d order_less_not_sym[OF d] less_imp_neq[OF d]
1.677 -      by (simp add: field_simps )    }
1.678 +      by(simp add: r[of "- (?s / (2*?d))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
1.679 +  }
1.680  ultimately show ?thesis by blast
1.681  qed
1.682
1.683 @@ -2408,9 +2357,9 @@
1.684  | "msubst p ((c,t),(d,s)) = p"
1.685
1.686  lemma msubst_I: assumes lp: "islin p" and nc: "isnpoly c" and nd: "isnpoly d"
1.687 -  shows "Ifm vs (x#bs) (msubst p ((c,t),(d,s))) = Ifm vs (((- Itm vs (x#bs) t /  Ipoly vs c + - Itm vs (x#bs) s / Ipoly vs d) /(1 + 1))#bs) p"
1.688 +  shows "Ifm vs (x#bs) (msubst p ((c,t),(d,s))) = Ifm vs (((- Itm vs (x#bs) t /  Ipoly vs c + - Itm vs (x#bs) s / Ipoly vs d) /2)#bs) p"
1.689    using lp
1.690 -by (induct p rule: islin.induct, auto simp add: tmbound0_I[where b="(- (Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>) + - (Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>)) /(1 + 1)" and b'=x and bs = bs and vs=vs] bound0_I[where b="(- (Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>) + - (Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>)) /(1 + 1)" and b'=x and bs = bs and vs=vs] msubsteq msubstneq msubstlt[OF nc nd] msubstle[OF nc nd])
1.691 +by (induct p rule: islin.induct, auto simp add: tmbound0_I[where b="(- (Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>) + - (Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>)) / 2" and b'=x and bs = bs and vs=vs] bound0_I[where b="(- (Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>) + - (Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>)) / 2" and b'=x and bs = bs and vs=vs] msubsteq msubstneq msubstlt[OF nc nd] msubstle[OF nc nd])
1.692
1.693  lemma msubst_nb: assumes lp: "islin p" and t: "tmbound0 t" and s: "tmbound0 s"
1.694    shows "bound0 (msubst p ((c,t),(d,s)))"
1.695 @@ -2424,7 +2373,7 @@
1.696  proof-
1.697  from uset_l[OF lp] have th: "\<forall>(c, s)\<in>set (uset p). isnpoly c \<and> tmbound0 s" by blast
1.698  {fix c t d s assume ctU: "(c,t) \<in>set (uset p)" and dsU: "(d,s) \<in>set (uset p)"
1.699 -  and pts: "Ifm vs ((- Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>) / (1+1) # bs) p"
1.700 +  and pts: "Ifm vs ((- Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>) / 2 # bs) p"
1.701    from th[rule_format, OF ctU] th[rule_format, OF dsU] have norm:"isnpoly c" "isnpoly d" by simp_all
1.702    from msubst_I[OF lp norm, of vs x bs t s] pts
1.703    have "Ifm vs (x # bs) (msubst p ((c, t), d, s))" ..}
1.704 @@ -2433,8 +2382,8 @@
1.705    and pts: "Ifm vs (x # bs) (msubst p ((c, t), d, s))"
1.706    from th[rule_format, OF ctU] th[rule_format, OF dsU] have norm:"isnpoly c" "isnpoly d" by simp_all
1.707    from msubst_I[OF lp norm, of vs x bs t s] pts
1.708 -  have "Ifm vs ((- Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>) / (1+1) # bs) p" ..}
1.709 -ultimately have th': "(\<exists> (c,t) \<in> set (uset p). \<exists> (d,s) \<in> set (uset p). Ifm vs ((- Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>) / (1+1) # bs) p) \<longleftrightarrow> ?F" by blast
1.710 +  have "Ifm vs ((- Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>) / 2 # bs) p" ..}
1.711 +ultimately have th': "(\<exists> (c,t) \<in> set (uset p). \<exists> (d,s) \<in> set (uset p). Ifm vs ((- Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>) / 2 # bs) p) \<longleftrightarrow> ?F" by blast
1.712  from fr_eq[OF lp, of vs bs x, simplified th'] show ?thesis .
1.713  qed
1.714
1.715 @@ -2510,8 +2459,8 @@
1.716    shows "(\<exists> x. Ifm vs (x#bs) p) \<longleftrightarrow>
1.717     ((Ifm vs (x#bs) (minusinf p)) \<or> (Ifm vs (x#bs) (plusinf p)) \<or>
1.718      (Ifm vs (0#bs) p) \<or>
1.719 -    (\<exists> (n,t) \<in> set (uset p). Ipoly vs n \<noteq> 0 \<and> Ifm vs ((- Itm vs (x#bs) t /  (Ipoly vs n * (1 + 1)))#bs) p) \<or>
1.720 -    (\<exists> (n,t) \<in> set (uset p). \<exists> (m,s) \<in> set (uset p). Ipoly vs n \<noteq> 0 \<and> Ipoly vs m \<noteq> 0 \<and> Ifm vs (((- Itm vs (x#bs) t /  Ipoly vs n + - Itm vs (x#bs) s / Ipoly vs m) /(1 + 1))#bs) p))"
1.721 +    (\<exists> (n,t) \<in> set (uset p). Ipoly vs n \<noteq> 0 \<and> Ifm vs ((- Itm vs (x#bs) t /  (Ipoly vs n * 2))#bs) p) \<or>
1.722 +    (\<exists> (n,t) \<in> set (uset p). \<exists> (m,s) \<in> set (uset p). Ipoly vs n \<noteq> 0 \<and> Ipoly vs m \<noteq> 0 \<and> Ifm vs (((- Itm vs (x#bs) t /  Ipoly vs n + - Itm vs (x#bs) s / Ipoly vs m) /2)#bs) p))"
1.723    (is "(\<exists> x. ?I x p) = (?M \<or> ?P \<or> ?Z \<or> ?U \<or> ?F)" is "?E = ?D")
1.724  proof
1.725    assume px: "\<exists> x. ?I x p"
1.726 @@ -2525,7 +2474,7 @@
1.727      let ?d = "\<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>"
1.728      let ?s = "Itm vs (x # bs) s"
1.729      let ?t = "Itm vs (x # bs) t"
1.730 -    have eq2: "\<And>(x::'a). x + x = (1 + 1) * x"
1.731 +    have eq2: "\<And>(x::'a). x + x = 2 * x"
1.733      {assume "?c = 0 \<and> ?d = 0"
1.734        with ct have ?D by simp}
1.735 @@ -2666,20 +2615,12 @@
1.736    shows "bound0 (msubst2 p c t)"
1.737  using lp tnb
1.738  by (simp add: msubst2_def msubstneg_nb msubstpos_nb conj_nb disj_nb lt_nb simpfm_bound0)
1.739 -
1.740 -lemma of_int2: "of_int 2 = 1 + 1"
1.741 -proof-
1.742 -  have "(2::int) = 1 + 1" by simp
1.743 -  hence "of_int 2 = of_int (1 + 1)" by simp
1.744 -  thus ?thesis unfolding of_int_add by simp
1.745 -qed
1.746
1.747 -lemma of_int_minus2: "of_int (-2) = - (1 + 1)"
1.748 -proof-
1.749 -  have th: "(-2::int) = - 2" by simp
1.750 -  show ?thesis unfolding th by (simp only: of_int_minus of_int2)
1.751 -qed
1.752 +lemma mult_minus2_left: "-2 * (x::'a::number_ring) = - (2 * x)"
1.753 +  by simp
1.754
1.755 +lemma mult_minus2_right: "(x::'a::number_ring) * -2 = - (x * 2)"
1.756 +  by simp
1.757
1.758  lemma islin_qf: "islin p \<Longrightarrow> qfree p"
1.759    by (induct p rule: islin.induct, auto simp add: bound0_qf)
1.760 @@ -2693,7 +2634,7 @@
1.761    have n2: "isnpoly (C (-2,1))" by (simp add: isnpoly_def)
1.762    note eq0 = subst0[OF islin_qf[OF lp], of vs x bs "CP 0\<^sub>p", simplified]
1.763
1.764 -  have eq1: "(\<exists>(n, t)\<in>set (uset p). ?I (msubst2 p (n *\<^sub>p (C (-2,1))) t)) \<longleftrightarrow> (\<exists>(n, t)\<in>set (uset p). \<lparr>n\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and> Ifm vs (- Itm vs (x # bs) t / (\<lparr>n\<rparr>\<^sub>p\<^bsup>vs\<^esup> * (1 + 1)) # bs) p)"
1.765 +  have eq1: "(\<exists>(n, t)\<in>set (uset p). ?I (msubst2 p (n *\<^sub>p (C (-2,1))) t)) \<longleftrightarrow> (\<exists>(n, t)\<in>set (uset p). \<lparr>n\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and> Ifm vs (- Itm vs (x # bs) t / (\<lparr>n\<rparr>\<^sub>p\<^bsup>vs\<^esup> * 2) # bs) p)"
1.766    proof-
1.767      {fix n t assume H: "(n, t)\<in>set (uset p)" "?I(msubst2 p (n *\<^sub>p C (-2, 1)) t)"
1.768        from H(1) th have "isnpoly n" by blast
1.769 @@ -2703,18 +2644,18 @@
1.770        hence nn2: "\<lparr>n *\<^sub>p(C (-2,1)) \<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "\<lparr>n \<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" using H(2) nn' nn
1.771          by (auto simp add: msubst2_def lt zero_less_mult_iff mult_less_0_iff)
1.772        from msubst2[OF lp nn nn2(1), of x bs t]
1.773 -      have "\<lparr>n\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and> Ifm vs (- Itm vs (x # bs) t / (\<lparr>n\<rparr>\<^sub>p\<^bsup>vs\<^esup> * (1 + 1)) # bs) p"
1.775 +      have "\<lparr>n\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and> Ifm vs (- Itm vs (x # bs) t / (\<lparr>n\<rparr>\<^sub>p\<^bsup>vs\<^esup> * 2) # bs) p"
1.776 +        using H(2) nn2 by (simp add: mult_minus2_right)}
1.777      moreover
1.778 -    {fix n t assume H: "(n, t)\<in>set (uset p)" "\<lparr>n\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "Ifm vs (- Itm vs (x # bs) t / (\<lparr>n\<rparr>\<^sub>p\<^bsup>vs\<^esup> * (1 + 1)) # bs) p"
1.779 +    {fix n t assume H: "(n, t)\<in>set (uset p)" "\<lparr>n\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "Ifm vs (- Itm vs (x # bs) t / (\<lparr>n\<rparr>\<^sub>p\<^bsup>vs\<^esup> * 2) # bs) p"
1.780        from H(1) th have "isnpoly n" by blast
1.781        hence nn: "isnpoly (n *\<^sub>p (C (-2,1)))" "\<lparr>n *\<^sub>p(C (-2,1)) \<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0"
1.782          using H(2) by (simp_all add: polymul_norm n2)
1.783 -      from msubst2[OF lp nn, of x bs t] have "?I (msubst2 p (n *\<^sub>p (C (-2,1))) t)" using H(2,3) by (simp add: of_int_minus2 del: minus_add_distrib)}
1.784 +      from msubst2[OF lp nn, of x bs t] have "?I (msubst2 p (n *\<^sub>p (C (-2,1))) t)" using H(2,3) by (simp add: mult_minus2_right)}
1.785      ultimately show ?thesis by blast
1.786    qed
1.787    have eq2: "(\<exists> (c,t) \<in> set (uset p). \<exists> (d,s) \<in> set (uset p). Ifm vs (x#bs) (msubst2 p (C (-2, 1) *\<^sub>p c*\<^sub>p d) (Add (Mul d t) (Mul c s)))) \<longleftrightarrow> (\<exists>(n, t)\<in>set (uset p).
1.788 -     \<exists>(m, s)\<in>set (uset p). \<lparr>n\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and> \<lparr>m\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and> Ifm vs ((- Itm vs (x # bs) t / \<lparr>n\<rparr>\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \<lparr>m\<rparr>\<^sub>p\<^bsup>vs\<^esup>) / (1 + 1) # bs) p)"
1.789 +     \<exists>(m, s)\<in>set (uset p). \<lparr>n\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and> \<lparr>m\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and> Ifm vs ((- Itm vs (x # bs) t / \<lparr>n\<rparr>\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \<lparr>m\<rparr>\<^sub>p\<^bsup>vs\<^esup>) / 2 # bs) p)"
1.790    proof-
1.791      {fix c t d s assume H: "(c,t) \<in> set (uset p)" "(d,s) \<in> set (uset p)"
1.792       "Ifm vs (x#bs) (msubst2 p (C (-2, 1) *\<^sub>p c*\<^sub>p d) (Add (Mul d t) (Mul c s)))"
1.793 @@ -2726,17 +2667,17 @@
1.794        have nn': "\<lparr>(C (-2, 1) *\<^sub>p c*\<^sub>p d)\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "\<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "\<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0"
1.795          using H(3) by (auto simp add: msubst2_def lt[OF stupid(1)]  lt[OF stupid(2)] zero_less_mult_iff mult_less_0_iff)
1.796        from msubst2[OF lp nn nn'(1), of x bs ] H(3) nn'
1.797 -      have "\<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and> \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and> Ifm vs ((- Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>) / (1 + 1) # bs) p"
1.799 +      have "\<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and> \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and> Ifm vs ((- Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>) / 2 # bs) p"
1.802      moreover
1.803      {fix c t d s assume H: "(c,t) \<in> set (uset p)" "(d,s) \<in> set (uset p)"
1.804 -      "\<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "\<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "Ifm vs ((- Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>) / (1 + 1) # bs) p"
1.805 +      "\<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "\<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "Ifm vs ((- Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>) / 2 # bs) p"
1.806       from H(1,2) th have "isnpoly c" "isnpoly d" by blast+
1.807        hence nn: "isnpoly (C (-2, 1) *\<^sub>p c*\<^sub>p d)" "\<lparr>(C (-2, 1) *\<^sub>p c*\<^sub>p d)\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0"
1.808          using H(3,4) by (simp_all add: polymul_norm n2)
1.809        from msubst2[OF lp nn, of x bs ] H(3,4,5)
1.810 -      have "Ifm vs (x#bs) (msubst2 p (C (-2, 1) *\<^sub>p c*\<^sub>p d) (Add (Mul d t) (Mul c s)))" apply (simp add: add_divide_distrib of_int_minus2 del: minus_add_distrib)by (simp add: mult_commute)}
1.811 +      have "Ifm vs (x#bs) (msubst2 p (C (-2, 1) *\<^sub>p c*\<^sub>p d) (Add (Mul d t) (Mul c s)))" apply (simp add: add_divide_distrib mult_minus2_left) by (simp add: mult_commute)}
1.812      ultimately show ?thesis by blast
1.813    qed
1.814    from fr_eq2[OF lp, of vs bs x] show ?thesis
1.815 @@ -3116,4 +3057,4 @@
1.816  apply ferrack
1.817  oops
1.818  *)
1.819 -end
1.820 \ No newline at end of file
1.821 +end
```