Parametric_Ferrante_Rackoff.thy: restrict to class number_ring, replace '1+1' with '2' everywhere
authorhuffman
Mon Nov 14 19:35:05 2011 +0100 (2011-11-14)
changeset 45499849d697adf1e
parent 45498 2dc373f1867a
child 45500 e2e27909bb66
Parametric_Ferrante_Rackoff.thy: restrict to class number_ring, replace '1+1' with '2' everywhere
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
     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.153 -      apply (simp only: one_add_one_is_two[symmetric] of_int_add)
   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.178 -      apply (simp only: one_add_one_is_two[symmetric] of_int_add)
   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.189        by (simp add: field_simps)
   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.206 -      apply (simp only: one_add_one_is_two[symmetric] of_int_add)
   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.246 -      apply (simp only: one_add_one_is_two[symmetric] of_int_add)
   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.271 -      apply (simp only: one_add_one_is_two[symmetric] of_int_add)
   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.282        by (simp add: field_simps)
   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.299 -      apply (simp only: one_add_one_is_two[symmetric] of_int_add)
   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.328        by (simp add: field_simps)
   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.347 -    apply (simp only: one_add_one_is_two[symmetric] of_int_add)
   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.361        by (simp add: field_simps)
   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.381 -      apply (simp only: one_add_one_is_two[symmetric] of_int_add)
   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.407 -      apply (simp only: one_add_one_is_two[symmetric] of_int_add)
   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.433 -      apply (simp only: one_add_one_is_two[symmetric] of_int_add)
   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.461 -      apply (simp only: one_add_one_is_two[symmetric] of_int_add)
   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.487 -      apply (simp only: one_add_one_is_two[symmetric] of_int_add)
   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.516        by (simp add: field_simps)
   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.535 -    apply (simp only: one_add_one_is_two[symmetric] of_int_add)
   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.544        by (simp add: mult_less_0_iff field_simps add_neg_neg add_pos_pos)
   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.549        by (simp add: field_simps)
   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.569 -      apply (simp only: one_add_one_is_two[symmetric] of_int_add)
   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.595 -      apply (simp only: one_add_one_is_two[symmetric] of_int_add)
   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.621 -      apply (simp only: one_add_one_is_two[symmetric] of_int_add)
   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.649 -      apply (simp only: one_add_one_is_two[symmetric] of_int_add)
   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.675 -      apply (simp only: one_add_one_is_two[symmetric] of_int_add)
   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.732        by  (simp add: field_simps)
   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.774 -        using H(2) nn2 by (simp add: of_int_minus2 del: minus_add_distrib)}
   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.798 -        apply (simp add: add_divide_distrib of_int_minus2 del: minus_add_distrib)
   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.800 +        apply (simp add: add_divide_distrib mult_minus2_left)
   1.801          by (simp add: mult_commute)}
   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