src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
changeset 56479 91958d4b30f7
parent 56410 a14831ac3023
child 57512 cc97b347b301
     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Tue Apr 08 23:16:00 2014 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Apr 09 09:37:47 2014 +0200
     1.3 @@ -2708,7 +2708,7 @@
     1.4      have "?rhs = Ifm vs (-?s / (2*?d) # bs) (Eq (CNP 0 a r))"
     1.5        by (simp only: th)
     1.6      also have "\<dots> \<longleftrightarrow> ?a * (-?s / (2*?d)) + ?r = 0"
     1.7 -      by (simp add: field_simps r[of "- (Itm vs (x # bs) s / (2 * \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>))"])
     1.8 +      by (simp add: r[of "- (Itm vs (x # bs) s / (2 * \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>))"])
     1.9      also have "\<dots> \<longleftrightarrow> 2 * ?d * (?a * (-?s / (2*?d)) + ?r) = 0"
    1.10        using d mult_cancel_left[of "2*?d" "(?a * (-?s / (2*?d)) + ?r)" 0] by simp
    1.11      also have "\<dots> \<longleftrightarrow> (- ?a * ?s) * (2*?d / (2*?d)) + 2 * ?d * ?r= 0"
    1.12 @@ -2728,12 +2728,12 @@
    1.13      have "?rhs = Ifm vs (-?t / (2*?c) # bs) (Eq (CNP 0 a r))"
    1.14        by (simp only: th)
    1.15      also have "\<dots> \<longleftrightarrow> ?a * (-?t / (2*?c)) + ?r = 0"
    1.16 -      by (simp add: field_simps r[of "- (?t/ (2 * ?c))"])
    1.17 +      by (simp add: r[of "- (?t/ (2 * ?c))"])
    1.18      also have "\<dots> \<longleftrightarrow> 2 * ?c * (?a * (-?t / (2 * ?c)) + ?r) = 0"
    1.19        using c mult_cancel_left[of "2 * ?c" "(?a * (-?t / (2 * ?c)) + ?r)" 0] by simp
    1.20      also have "\<dots> \<longleftrightarrow> (?a * -?t)* (2 * ?c) / (2 * ?c) + 2 * ?c * ?r= 0"
    1.21        by (simp add: field_simps distrib_left[of "2 * ?c"] del: distrib_left)
    1.22 -    also have "\<dots> \<longleftrightarrow> - (?a * ?t) + 2 * ?c * ?r = 0" using c by (simp add: field_simps)
    1.23 +    also have "\<dots> \<longleftrightarrow> - (?a * ?t) + 2 * ?c * ?r = 0" using c by simp
    1.24      finally have ?thesis using c d
    1.25        by (simp add: r[of "- (?t/ (2 * ?c))"] msubsteq_def Let_def evaldjf_ex)
    1.26    }
    1.27 @@ -2755,7 +2755,7 @@
    1.28        by simp
    1.29      also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2 * ?c * ?d * ?r = 0"
    1.30        using nonzero_mult_divide_cancel_left [OF dc] c d
    1.31 -      by (simp add: divide_minus_left algebra_simps diff_divide_distrib del: distrib_right)
    1.32 +      by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
    1.33      finally  have ?thesis using c d
    1.34        by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"]
    1.35            msubsteq_def Let_def evaldjf_ex field_simps)
    1.36 @@ -2825,7 +2825,7 @@
    1.37      have "?rhs = Ifm vs (-?s / (2*?d) # bs) (NEq (CNP 0 a r))"
    1.38        by (simp only: th)
    1.39      also have "\<dots> \<longleftrightarrow> ?a * (-?s / (2*?d)) + ?r \<noteq> 0"
    1.40 -      by (simp add: field_simps r[of "- (Itm vs (x # bs) s / (2 * \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>))"])
    1.41 +      by (simp add: r[of "- (Itm vs (x # bs) s / (2 * \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>))"])
    1.42      also have "\<dots> \<longleftrightarrow> 2*?d * (?a * (-?s / (2*?d)) + ?r) \<noteq> 0"
    1.43        using d mult_cancel_left[of "2*?d" "(?a * (-?s / (2*?d)) + ?r)" 0] by simp
    1.44      also have "\<dots> \<longleftrightarrow> (- ?a * ?s) * (2*?d / (2*?d)) + 2*?d*?r\<noteq> 0"
    1.45 @@ -2845,13 +2845,13 @@
    1.46      have "?rhs = Ifm vs (-?t / (2*?c) # bs) (NEq (CNP 0 a r))"
    1.47        by (simp only: th)
    1.48      also have "\<dots> \<longleftrightarrow> ?a * (-?t / (2*?c)) + ?r \<noteq> 0"
    1.49 -      by (simp add: field_simps r[of "- (?t/ (2 * ?c))"])
    1.50 +      by (simp add: r[of "- (?t/ (2 * ?c))"])
    1.51      also have "\<dots> \<longleftrightarrow> 2*?c * (?a * (-?t / (2*?c)) + ?r) \<noteq> 0"
    1.52        using c mult_cancel_left[of "2*?c" "(?a * (-?t / (2*?c)) + ?r)" 0] by simp
    1.53      also have "\<dots> \<longleftrightarrow> (?a * -?t)* (2*?c) / (2*?c) + 2*?c*?r \<noteq> 0"
    1.54        by (simp add: field_simps distrib_left[of "2*?c"] del: distrib_left)
    1.55      also have "\<dots> \<longleftrightarrow> - (?a * ?t) + 2*?c*?r \<noteq> 0"
    1.56 -      using c by (simp add: field_simps)
    1.57 +      using c by simp
    1.58      finally have ?thesis
    1.59        using c d by (simp add: r[of "- (?t/ (2*?c))"] msubstneq_def Let_def evaldjf_ex)
    1.60    }
    1.61 @@ -2873,7 +2873,7 @@
    1.62        by simp
    1.63      also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r \<noteq> 0"
    1.64        using nonzero_mult_divide_cancel_left[OF dc] c d
    1.65 -      by (simp add: divide_minus_left algebra_simps diff_divide_distrib del: distrib_right)
    1.66 +      by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
    1.67      finally have ?thesis
    1.68        using c d
    1.69        by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"]
    1.70 @@ -2963,7 +2963,7 @@
    1.71        by simp
    1.72      also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r < 0"
    1.73        using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d
    1.74 -      by (simp add: divide_minus_left algebra_simps diff_divide_distrib del: distrib_right)
    1.75 +      by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
    1.76      finally  have ?thesis using dc c d  nc nd dc'
    1.77        by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"]
    1.78            msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
    1.79 @@ -2988,7 +2988,7 @@
    1.80        by simp
    1.81      also have "\<dots> \<longleftrightarrow> ?a * ((?d * ?t + ?c* ?s )) - 2 * ?c * ?d * ?r < 0"
    1.82        using nonzero_mult_divide_cancel_left[of "2 * ?c * ?d"] c d
    1.83 -      by (simp add: divide_minus_left algebra_simps diff_divide_distrib del: distrib_right)
    1.84 +      by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
    1.85      finally have ?thesis using dc c d nc nd
    1.86        by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"]
    1.87            msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
    1.88 @@ -3005,14 +3005,14 @@
    1.89      have "?rhs \<longleftrightarrow> Ifm vs (- ?t / (2 * ?c) # bs) (Lt (CNP 0 a r))"
    1.90        by (simp only: th)
    1.91      also have "\<dots> \<longleftrightarrow> ?a * (- ?t / (2 * ?c))+ ?r < 0"
    1.92 -      by (simp add: field_simps r[of "- (?t / (2 * ?c))"])
    1.93 +      by (simp add: r[of "- (?t / (2 * ?c))"])
    1.94      also have "\<dots> \<longleftrightarrow> 2 * ?c * (?a * (- ?t / (2 * ?c))+ ?r) < 0"
    1.95        using c mult_less_cancel_left_disj[of "2 * ?c" "?a* (- ?t / (2*?c))+ ?r" 0] c' c''
    1.96          order_less_not_sym[OF c'']
    1.97        by simp
    1.98      also have "\<dots> \<longleftrightarrow> - ?a * ?t + 2 * ?c * ?r < 0"
    1.99        using nonzero_mult_divide_cancel_left[OF c'] c
   1.100 -      by (simp add: divide_minus_left algebra_simps diff_divide_distrib less_le del: distrib_right)
   1.101 +      by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
   1.102      finally have ?thesis using c d nc nd
   1.103        by (simp add: r[of "- (?t / (2*?c))"] msubstlt_def Let_def evaldjf_ex field_simps
   1.104            lt polyneg_norm polymul_norm)
   1.105 @@ -3029,7 +3029,7 @@
   1.106      have "?rhs \<longleftrightarrow> Ifm vs (- ?t / (2*?c) # bs) (Lt (CNP 0 a r))"
   1.107        by (simp only: th)
   1.108      also have "\<dots> \<longleftrightarrow> ?a * (- ?t / (2*?c))+ ?r < 0"
   1.109 -      by (simp add: field_simps r[of "- (?t / (2*?c))"])
   1.110 +      by (simp add: r[of "- (?t / (2*?c))"])
   1.111      also have "\<dots> \<longleftrightarrow> 2 * ?c * (?a * (- ?t / (2 * ?c))+ ?r) > 0"
   1.112        using c order_less_not_sym[OF c''] less_imp_neq[OF c''] c''
   1.113          mult_less_cancel_left_disj[of "2 * ?c" 0 "?a* (- ?t / (2*?c))+ ?r"]
   1.114 @@ -3037,7 +3037,7 @@
   1.115      also have "\<dots> \<longleftrightarrow> ?a*?t -  2*?c *?r < 0"
   1.116        using nonzero_mult_divide_cancel_left[OF c'] c order_less_not_sym[OF c'']
   1.117            less_imp_neq[OF c''] c''
   1.118 -        by (simp add: divide_minus_left algebra_simps diff_divide_distrib del: distrib_right)
   1.119 +        by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
   1.120      finally have ?thesis using c d nc nd
   1.121        by (simp add: r[of "- (?t / (2*?c))"] msubstlt_def Let_def evaldjf_ex field_simps
   1.122            lt polyneg_norm polymul_norm)
   1.123 @@ -3054,14 +3054,14 @@
   1.124      have "?rhs \<longleftrightarrow> Ifm vs (- ?s / (2 * ?d) # bs) (Lt (CNP 0 a r))"
   1.125        by (simp only: th)
   1.126      also have "\<dots> \<longleftrightarrow> ?a * (- ?s / (2 * ?d))+ ?r < 0"
   1.127 -      by (simp add: field_simps r[of "- (?s / (2 * ?d))"])
   1.128 +      by (simp add: r[of "- (?s / (2 * ?d))"])
   1.129      also have "\<dots> \<longleftrightarrow> 2 * ?d * (?a * (- ?s / (2 * ?d))+ ?r) < 0"
   1.130        using d mult_less_cancel_left_disj[of "2 * ?d" "?a * (- ?s / (2 * ?d))+ ?r" 0] d' d''
   1.131          order_less_not_sym[OF d'']
   1.132        by simp
   1.133      also have "\<dots> \<longleftrightarrow> - ?a * ?s+  2 * ?d * ?r < 0"
   1.134        using nonzero_mult_divide_cancel_left[OF d'] d
   1.135 -      by (simp add: divide_minus_left algebra_simps diff_divide_distrib less_le del: distrib_right)
   1.136 +      by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
   1.137      finally have ?thesis using c d nc nd
   1.138        by (simp add: r[of "- (?s / (2*?d))"] msubstlt_def Let_def evaldjf_ex field_simps
   1.139            lt polyneg_norm polymul_norm)
   1.140 @@ -3078,7 +3078,7 @@
   1.141      have "?rhs \<longleftrightarrow> Ifm vs (- ?s / (2 * ?d) # bs) (Lt (CNP 0 a r))"
   1.142        by (simp only: th)
   1.143      also have "\<dots> \<longleftrightarrow> ?a * (- ?s / (2 * ?d)) + ?r < 0"
   1.144 -      by (simp add: field_simps r[of "- (?s / (2 * ?d))"])
   1.145 +      by (simp add: r[of "- (?s / (2 * ?d))"])
   1.146      also have "\<dots> \<longleftrightarrow> 2 * ?d * (?a * (- ?s / (2 * ?d)) + ?r) > 0"
   1.147        using d order_less_not_sym[OF d''] less_imp_neq[OF d''] d''
   1.148          mult_less_cancel_left_disj[of "2 * ?d" 0 "?a* (- ?s / (2*?d))+ ?r"]
   1.149 @@ -3086,7 +3086,7 @@
   1.150      also have "\<dots> \<longleftrightarrow> ?a * ?s -  2 * ?d * ?r < 0"
   1.151        using nonzero_mult_divide_cancel_left[OF d'] d order_less_not_sym[OF d'']
   1.152            less_imp_neq[OF d''] d''
   1.153 -        by (simp add: divide_minus_left algebra_simps diff_divide_distrib del: distrib_right)
   1.154 +        by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
   1.155      finally have ?thesis using c d nc nd
   1.156        by (simp add: r[of "- (?s / (2*?d))"] msubstlt_def Let_def evaldjf_ex field_simps
   1.157            lt polyneg_norm polymul_norm)
   1.158 @@ -3177,7 +3177,7 @@
   1.159        by simp
   1.160      also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r \<le> 0"
   1.161        using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d
   1.162 -      by (simp add: divide_minus_left algebra_simps diff_divide_distrib del: distrib_right)
   1.163 +      by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
   1.164      finally  have ?thesis using dc c d  nc nd dc'
   1.165        by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubstle_def
   1.166            Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
   1.167 @@ -3202,7 +3202,7 @@
   1.168        by simp
   1.169      also have "\<dots> \<longleftrightarrow> ?a * ((?d * ?t + ?c* ?s )) - 2 * ?c * ?d * ?r \<le> 0"
   1.170        using nonzero_mult_divide_cancel_left[of "2 * ?c * ?d"] c d
   1.171 -      by (simp add: divide_minus_left algebra_simps diff_divide_distrib del: distrib_right)
   1.172 +      by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
   1.173      finally  have ?thesis using dc c d  nc nd
   1.174        by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubstle_def
   1.175            Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
   1.176 @@ -3219,14 +3219,14 @@
   1.177      have "?rhs \<longleftrightarrow> Ifm vs (- ?t / (2 * ?c) # bs) (Le (CNP 0 a r))"
   1.178        by (simp only: th)
   1.179      also have "\<dots> \<longleftrightarrow> ?a * (- ?t / (2 * ?c))+ ?r \<le> 0"
   1.180 -      by (simp add: field_simps r[of "- (?t / (2 * ?c))"])
   1.181 +      by (simp add: r[of "- (?t / (2 * ?c))"])
   1.182      also have "\<dots> \<longleftrightarrow> 2 * ?c * (?a * (- ?t / (2 * ?c))+ ?r) \<le> 0"
   1.183        using c mult_le_cancel_left[of "2 * ?c" "?a* (- ?t / (2*?c))+ ?r" 0] c' c''
   1.184          order_less_not_sym[OF c'']
   1.185        by simp
   1.186      also have "\<dots> \<longleftrightarrow> - ?a*?t+  2*?c *?r \<le> 0"
   1.187        using nonzero_mult_divide_cancel_left[OF c'] c
   1.188 -      by (simp add: divide_minus_left algebra_simps diff_divide_distrib less_le del: distrib_right)
   1.189 +      by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
   1.190      finally have ?thesis using c d nc nd
   1.191        by (simp add: r[of "- (?t / (2*?c))"] msubstle_def Let_def
   1.192            evaldjf_ex field_simps lt polyneg_norm polymul_norm)
   1.193 @@ -3243,7 +3243,7 @@
   1.194      have "?rhs \<longleftrightarrow> Ifm vs (- ?t / (2 * ?c) # bs) (Le (CNP 0 a r))"
   1.195        by (simp only: th)
   1.196      also have "\<dots> \<longleftrightarrow> ?a * (- ?t / (2*?c))+ ?r \<le> 0"
   1.197 -      by (simp add: field_simps r[of "- (?t / (2*?c))"])
   1.198 +      by (simp add: r[of "- (?t / (2*?c))"])
   1.199      also have "\<dots> \<longleftrightarrow> 2 * ?c * (?a * (- ?t / (2 * ?c))+ ?r) \<ge> 0"
   1.200        using c order_less_not_sym[OF c''] less_imp_neq[OF c''] c''
   1.201          mult_le_cancel_left[of "2 * ?c" 0 "?a* (- ?t / (2*?c))+ ?r"]
   1.202 @@ -3251,7 +3251,7 @@
   1.203      also have "\<dots> \<longleftrightarrow> ?a * ?t - 2 * ?c * ?r \<le> 0"
   1.204        using nonzero_mult_divide_cancel_left[OF c'] c order_less_not_sym[OF c'']
   1.205            less_imp_neq[OF c''] c''
   1.206 -        by (simp add: divide_minus_left algebra_simps diff_divide_distrib del: distrib_right)
   1.207 +        by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
   1.208      finally have ?thesis using c d nc nd
   1.209        by (simp add: r[of "- (?t / (2*?c))"] msubstle_def Let_def
   1.210            evaldjf_ex field_simps lt polyneg_norm polymul_norm)
   1.211 @@ -3268,14 +3268,14 @@
   1.212      have "?rhs \<longleftrightarrow> Ifm vs (- ?s / (2 * ?d) # bs) (Le (CNP 0 a r))"
   1.213        by (simp only: th)
   1.214      also have "\<dots> \<longleftrightarrow> ?a * (- ?s / (2 * ?d))+ ?r \<le> 0"
   1.215 -      by (simp add: field_simps r[of "- (?s / (2*?d))"])
   1.216 +      by (simp add: r[of "- (?s / (2*?d))"])
   1.217      also have "\<dots> \<longleftrightarrow> 2 * ?d * (?a * (- ?s / (2 * ?d)) + ?r) \<le> 0"
   1.218        using d mult_le_cancel_left[of "2 * ?d" "?a* (- ?s / (2*?d))+ ?r" 0] d' d''
   1.219          order_less_not_sym[OF d'']
   1.220        by simp
   1.221      also have "\<dots> \<longleftrightarrow> - ?a * ?s + 2 * ?d * ?r \<le> 0"
   1.222        using nonzero_mult_divide_cancel_left[OF d'] d
   1.223 -      by (simp add: divide_minus_left algebra_simps diff_divide_distrib less_le del: distrib_right)
   1.224 +      by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
   1.225      finally have ?thesis using c d nc nd
   1.226        by (simp add: r[of "- (?s / (2*?d))"] msubstle_def Let_def
   1.227            evaldjf_ex field_simps lt polyneg_norm polymul_norm)
   1.228 @@ -3292,7 +3292,7 @@
   1.229      have "?rhs \<longleftrightarrow> Ifm vs (- ?s / (2*?d) # bs) (Le (CNP 0 a r))"
   1.230        by (simp only: th)
   1.231      also have "\<dots> \<longleftrightarrow> ?a* (- ?s / (2*?d))+ ?r \<le> 0"
   1.232 -      by (simp add: field_simps r[of "- (?s / (2*?d))"])
   1.233 +      by (simp add: r[of "- (?s / (2*?d))"])
   1.234      also have "\<dots> \<longleftrightarrow> 2*?d * (?a* (- ?s / (2*?d))+ ?r) \<ge> 0"
   1.235        using d order_less_not_sym[OF d''] less_imp_neq[OF d''] d''
   1.236          mult_le_cancel_left[of "2 * ?d" 0 "?a* (- ?s / (2*?d))+ ?r"]
   1.237 @@ -3300,7 +3300,7 @@
   1.238      also have "\<dots> \<longleftrightarrow> ?a * ?s -  2 * ?d * ?r \<le> 0"
   1.239        using nonzero_mult_divide_cancel_left[OF d'] d order_less_not_sym[OF d'']
   1.240            less_imp_neq[OF d''] d''
   1.241 -        by (simp add: divide_minus_left algebra_simps diff_divide_distrib del: distrib_right)
   1.242 +        by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
   1.243      finally have ?thesis using c d nc nd
   1.244        by (simp add: r[of "- (?s / (2*?d))"] msubstle_def Let_def
   1.245            evaldjf_ex field_simps lt polyneg_norm polymul_norm)
   1.246 @@ -3326,10 +3326,10 @@
   1.247      Ifm vs (((- Itm vs (x#bs) t /  Ipoly vs c + - Itm vs (x#bs) s / Ipoly vs d) /2)#bs) p"
   1.248    using lp
   1.249    by (induct p rule: islin.induct)
   1.250 -    (auto simp add: tmbound0_I 
   1.251 +    (auto simp add: tmbound0_I
   1.252        [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"
   1.253          and b' = x and bs = bs and vs = vs]
   1.254 -      msubsteq msubstneq msubstlt [OF nc nd] msubstle [OF nc nd] divide_minus_left)
   1.255 +      msubsteq msubstneq msubstlt [OF nc nd] msubstle [OF nc nd])
   1.256  
   1.257  lemma msubst_nb:
   1.258    assumes lp: "islin p"
   1.259 @@ -3767,7 +3767,7 @@
   1.260          by (auto simp add: msubst2_def lt zero_less_mult_iff mult_less_0_iff)
   1.261        from msubst2[OF lp nn nn2(1), of x bs t]
   1.262        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.263 -        using H(2) nn2 by (simp add: divide_minus_left divide_minus_right mult_minus2_right)
   1.264 +        using H(2) nn2 by (simp add: mult_minus2_right)
   1.265      }
   1.266      moreover
   1.267      {
   1.268 @@ -3780,7 +3780,7 @@
   1.269        then have nn: "isnpoly (n *\<^sub>p (C (-2,1)))" "\<lparr>n *\<^sub>p(C (-2,1)) \<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0"
   1.270          using H(2) by (simp_all add: polymul_norm n2)
   1.271        from msubst2[OF lp nn, of x bs t] have "?I (msubst2 p (n *\<^sub>p (C (-2,1))) t)"
   1.272 -        using H(2,3) by (simp add: divide_minus_left divide_minus_right mult_minus2_right)
   1.273 +        using H(2,3) by (simp add: mult_minus2_right)
   1.274      }
   1.275      ultimately show ?thesis by blast
   1.276    qed
   1.277 @@ -3811,7 +3811,7 @@
   1.278        from msubst2[OF lp nn nn'(1), of x bs ] H(3) nn'
   1.279        have "\<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and> \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and>
   1.280            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.281 -        by (simp add: divide_minus_left divide_minus_right add_divide_distrib diff_divide_distrib mult_minus2_left mult_commute)
   1.282 +        by (simp add: add_divide_distrib diff_divide_distrib mult_minus2_left mult_commute)
   1.283      }
   1.284      moreover
   1.285      {
   1.286 @@ -3828,7 +3828,7 @@
   1.287          using H(3,4) by (simp_all add: polymul_norm n2)
   1.288        from msubst2[OF lp nn, of x bs ] H(3,4,5)
   1.289        have "Ifm vs (x#bs) (msubst2 p (C (-2, 1) *\<^sub>p c*\<^sub>p d) (Add (Mul d t) (Mul c s)))"
   1.290 -        by (simp add: divide_minus_left divide_minus_right diff_divide_distrib add_divide_distrib mult_minus2_left mult_commute)
   1.291 +        by (simp add: diff_divide_distrib add_divide_distrib mult_minus2_left mult_commute)
   1.292      }
   1.293      ultimately show ?thesis by blast
   1.294    qed