src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
changeset 49962 a8cc904a6820
parent 48562 f6d6d58fa318
child 50045 2214bc566f88
     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Oct 19 10:46:42 2012 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Oct 19 15:12:52 2012 +0200
     1.3 @@ -224,7 +224,7 @@
     1.4  apply (induct t s rule: tmadd.induct, simp_all add: Let_def)
     1.5  apply (case_tac "c1 +\<^sub>p c2 = 0\<^sub>p",case_tac "n1 \<le> n2", simp_all)
     1.6  apply (case_tac "n1 = n2", simp_all add: field_simps)
     1.7 -apply (simp only: right_distrib[symmetric]) 
     1.8 +apply (simp only: distrib_left[symmetric]) 
     1.9  by (auto simp del: polyadd simp add: polyadd[symmetric])
    1.10  
    1.11  lemma tmadd_nb0[simp]: "\<lbrakk> tmbound0 t ; tmbound0 s\<rbrakk> \<Longrightarrow> tmbound0 (tmadd (t,s))"
    1.12 @@ -358,7 +358,7 @@
    1.13    apply (simp add: Let_def split_def field_simps)
    1.14    apply (simp add: Let_def split_def field_simps)
    1.15    apply (simp add: Let_def split_def field_simps)
    1.16 -  apply (simp add: Let_def split_def mult_assoc right_distrib[symmetric])
    1.17 +  apply (simp add: Let_def split_def mult_assoc distrib_left[symmetric])
    1.18    apply (simp add: Let_def split_def field_simps)
    1.19    apply (simp add: Let_def split_def field_simps)
    1.20    done
    1.21 @@ -1933,7 +1933,7 @@
    1.22      also have "\<dots> \<longleftrightarrow> 2*?d * (?a * (-?s / (2*?d)) + ?r) = 0"
    1.23        using d mult_cancel_left[of "2*?d" "(?a * (-?s / (2*?d)) + ?r)" 0] by simp
    1.24      also have "\<dots> \<longleftrightarrow> (- ?a * ?s) * (2*?d / (2*?d)) + 2*?d*?r= 0"
    1.25 -      by (simp add: field_simps right_distrib[of "2*?d"] del: right_distrib)
    1.26 +      by (simp add: field_simps distrib_left[of "2*?d"] del: distrib_left)
    1.27      
    1.28      also have "\<dots> \<longleftrightarrow> - (?a * ?s) + 2*?d*?r = 0" using d by simp 
    1.29      finally have ?thesis using c d 
    1.30 @@ -1947,7 +1947,7 @@
    1.31      also have "\<dots> \<longleftrightarrow> 2*?c * (?a * (-?t / (2*?c)) + ?r) = 0" 
    1.32        using c mult_cancel_left[of "2*?c" "(?a * (-?t / (2*?c)) + ?r)" 0] by simp
    1.33      also have "\<dots> \<longleftrightarrow> (?a * -?t)* (2*?c) / (2*?c) + 2*?c*?r= 0"
    1.34 -      by (simp add: field_simps right_distrib[of "2*?c"] del: right_distrib)
    1.35 +      by (simp add: field_simps distrib_left[of "2*?c"] del: distrib_left)
    1.36      also have "\<dots> \<longleftrightarrow> - (?a * ?t) + 2*?c*?r = 0" using c by simp 
    1.37      finally have ?thesis using c d 
    1.38        by (simp add: r[of "- (?t/ (2*?c))"] msubsteq_def Let_def evaldjf_ex)
    1.39 @@ -1964,7 +1964,7 @@
    1.40        using c d mult_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0] by simp
    1.41      also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r =0" 
    1.42        using nonzero_mult_divide_cancel_left [OF dc] c d
    1.43 -      by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
    1.44 +      by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
    1.45      finally  have ?thesis using c d 
    1.46        by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubsteq_def Let_def evaldjf_ex field_simps)
    1.47    }
    1.48 @@ -2015,7 +2015,7 @@
    1.49      also have "\<dots> \<longleftrightarrow> 2*?d * (?a * (-?s / (2*?d)) + ?r) \<noteq> 0" 
    1.50        using d mult_cancel_left[of "2*?d" "(?a * (-?s / (2*?d)) + ?r)" 0] by simp
    1.51      also have "\<dots> \<longleftrightarrow> (- ?a * ?s) * (2*?d / (2*?d)) + 2*?d*?r\<noteq> 0"
    1.52 -      by (simp add: field_simps right_distrib[of "2*?d"] del: right_distrib)
    1.53 +      by (simp add: field_simps distrib_left[of "2*?d"] del: distrib_left)
    1.54      
    1.55      also have "\<dots> \<longleftrightarrow> - (?a * ?s) + 2*?d*?r \<noteq> 0" using d by simp 
    1.56      finally have ?thesis using c d 
    1.57 @@ -2029,7 +2029,7 @@
    1.58      also have "\<dots> \<longleftrightarrow> 2*?c * (?a * (-?t / (2*?c)) + ?r) \<noteq> 0" 
    1.59        using c mult_cancel_left[of "2*?c" "(?a * (-?t / (2*?c)) + ?r)" 0] by simp
    1.60      also have "\<dots> \<longleftrightarrow> (?a * -?t)* (2*?c) / (2*?c) + 2*?c*?r \<noteq> 0"
    1.61 -      by (simp add: field_simps right_distrib[of "2*?c"] del: right_distrib)
    1.62 +      by (simp add: field_simps distrib_left[of "2*?c"] del: distrib_left)
    1.63      also have "\<dots> \<longleftrightarrow> - (?a * ?t) + 2*?c*?r \<noteq> 0" using c by simp 
    1.64      finally have ?thesis using c d 
    1.65        by (simp add: r[of "- (?t/ (2*?c))"] msubstneq_def Let_def evaldjf_ex)
    1.66 @@ -2046,7 +2046,7 @@
    1.67        using c d mult_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0] by simp
    1.68      also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r \<noteq> 0" 
    1.69        using nonzero_mult_divide_cancel_left[OF dc] c d
    1.70 -      by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
    1.71 +      by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
    1.72      finally  have ?thesis using c d 
    1.73        by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubstneq_def Let_def evaldjf_ex field_simps)
    1.74    }
    1.75 @@ -2112,7 +2112,7 @@
    1.76        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.77      also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r < 0" 
    1.78        using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d
    1.79 -      by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
    1.80 +      by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
    1.81      finally  have ?thesis using dc c d  nc nd dc'
    1.82        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.83    }
    1.84 @@ -2134,7 +2134,7 @@
    1.85        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.86      also have "\<dots> \<longleftrightarrow> ?a * ((?d * ?t + ?c* ?s )) - 2*?c*?d*?r < 0" 
    1.87        using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d
    1.88 -      by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
    1.89 +      by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
    1.90      finally  have ?thesis using dc c d  nc nd
    1.91        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.92    }
    1.93 @@ -2149,7 +2149,7 @@
    1.94        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.95      also have "\<dots> \<longleftrightarrow> - ?a*?t+  2*?c *?r < 0" 
    1.96        using nonzero_mult_divide_cancel_left[OF c'] c
    1.97 -      by (simp add: algebra_simps diff_divide_distrib less_le del: left_distrib)
    1.98 +      by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
    1.99      finally have ?thesis using c d nc nd 
   1.100        by(simp add: r[of "- (?t / (2*?c))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
   1.101    }
   1.102 @@ -2163,7 +2163,7 @@
   1.103        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.104      also have "\<dots> \<longleftrightarrow> ?a*?t -  2*?c *?r < 0" 
   1.105        using nonzero_mult_divide_cancel_left[OF c'] c order_less_not_sym[OF c''] less_imp_neq[OF c''] c''
   1.106 -        by (simp add: algebra_simps diff_divide_distrib del:  left_distrib)
   1.107 +        by (simp add: algebra_simps diff_divide_distrib del:  distrib_right)
   1.108      finally have ?thesis using c d nc nd 
   1.109        by(simp add: r[of "- (?t / (2*?c))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
   1.110    }
   1.111 @@ -2179,7 +2179,7 @@
   1.112        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.113      also have "\<dots> \<longleftrightarrow> - ?a*?s+  2*?d *?r < 0" 
   1.114        using nonzero_mult_divide_cancel_left[OF d'] d
   1.115 -      by (simp add: algebra_simps diff_divide_distrib less_le del: left_distrib)
   1.116 +      by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
   1.117      finally have ?thesis using c d nc nd 
   1.118        by(simp add: r[of "- (?s / (2*?d))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
   1.119    }
   1.120 @@ -2193,7 +2193,7 @@
   1.121        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.122      also have "\<dots> \<longleftrightarrow> ?a*?s -  2*?d *?r < 0" 
   1.123        using nonzero_mult_divide_cancel_left[OF d'] d order_less_not_sym[OF d''] less_imp_neq[OF d''] d''
   1.124 -        by (simp add: algebra_simps diff_divide_distrib del:  left_distrib)
   1.125 +        by (simp add: algebra_simps diff_divide_distrib del:  distrib_right)
   1.126      finally have ?thesis using c d nc nd 
   1.127        by(simp add: r[of "- (?s / (2*?d))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
   1.128    }
   1.129 @@ -2258,7 +2258,7 @@
   1.130        using dc' dc'' mult_le_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0] by simp
   1.131      also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r <= 0" 
   1.132        using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d
   1.133 -      by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
   1.134 +      by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
   1.135      finally  have ?thesis using dc c d  nc nd dc'
   1.136        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.137    }
   1.138 @@ -2280,7 +2280,7 @@
   1.139        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.140      also have "\<dots> \<longleftrightarrow> ?a * ((?d * ?t + ?c* ?s )) - 2*?c*?d*?r <= 0" 
   1.141        using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d
   1.142 -      by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
   1.143 +      by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
   1.144      finally  have ?thesis using dc c d  nc nd
   1.145        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.146    }
   1.147 @@ -2295,7 +2295,7 @@
   1.148        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.149      also have "\<dots> \<longleftrightarrow> - ?a*?t+  2*?c *?r <= 0" 
   1.150        using nonzero_mult_divide_cancel_left[OF c'] c
   1.151 -      by (simp add: algebra_simps diff_divide_distrib less_le del: left_distrib)
   1.152 +      by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
   1.153      finally have ?thesis using c d nc nd 
   1.154        by(simp add: r[of "- (?t / (2*?c))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
   1.155    }
   1.156 @@ -2309,7 +2309,7 @@
   1.157        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.158      also have "\<dots> \<longleftrightarrow> ?a*?t -  2*?c *?r <= 0" 
   1.159        using nonzero_mult_divide_cancel_left[OF c'] c order_less_not_sym[OF c''] less_imp_neq[OF c''] c''
   1.160 -        by (simp add: algebra_simps diff_divide_distrib del:  left_distrib)
   1.161 +        by (simp add: algebra_simps diff_divide_distrib del:  distrib_right)
   1.162      finally have ?thesis using c d nc nd 
   1.163        by(simp add: r[of "- (?t / (2*?c))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
   1.164    }
   1.165 @@ -2325,7 +2325,7 @@
   1.166        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.167      also have "\<dots> \<longleftrightarrow> - ?a*?s+  2*?d *?r <= 0" 
   1.168        using nonzero_mult_divide_cancel_left[OF d'] d
   1.169 -      by (simp add: algebra_simps diff_divide_distrib less_le del: left_distrib)
   1.170 +      by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
   1.171      finally have ?thesis using c d nc nd 
   1.172        by(simp add: r[of "- (?s / (2*?d))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
   1.173    }
   1.174 @@ -2339,7 +2339,7 @@
   1.175        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.176      also have "\<dots> \<longleftrightarrow> ?a*?s -  2*?d *?r <= 0" 
   1.177        using nonzero_mult_divide_cancel_left[OF d'] d order_less_not_sym[OF d''] less_imp_neq[OF d''] d''
   1.178 -        by (simp add: algebra_simps diff_divide_distrib del:  left_distrib)
   1.179 +        by (simp add: algebra_simps diff_divide_distrib del:  distrib_right)
   1.180      finally have ?thesis using c d nc nd 
   1.181        by(simp add: r[of "- (?s / (2*?d))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
   1.182    }