1831 from yne c eq_divide_eq[of "y" "- ?Nt x s" "?N c"] have ?case |
1831 from yne c eq_divide_eq[of "y" "- ?Nt x s" "?N c"] have ?case |
1832 by (simp add: ring_simps tmbound0_I[OF lin(3), of vs x bs y] sum_eq[symmetric]) } |
1832 by (simp add: ring_simps tmbound0_I[OF lin(3), of vs x bs y] sum_eq[symmetric]) } |
1833 ultimately show ?case by blast |
1833 ultimately show ?case by blast |
1834 qed (auto simp add: nth_pos2 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"]) |
1834 qed (auto simp add: nth_pos2 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"]) |
1835 |
1835 |
1836 lemma one_plus_one_pos[simp]: "(1::'a::{ordered_field}) + 1 > 0" |
1836 lemma one_plus_one_pos[simp]: "(1::'a::{linordered_field}) + 1 > 0" |
1837 proof- |
1837 proof- |
1838 have op: "(1::'a) > 0" by simp |
1838 have op: "(1::'a) > 0" by simp |
1839 from add_pos_pos[OF op op] show ?thesis . |
1839 from add_pos_pos[OF op op] show ?thesis . |
1840 qed |
1840 qed |
1841 |
1841 |
1842 lemma one_plus_one_nonzero[simp]: "(1::'a::{ordered_field}) + 1 \<noteq> 0" |
1842 lemma one_plus_one_nonzero[simp]: "(1::'a::{linordered_field}) + 1 \<noteq> 0" |
1843 using one_plus_one_pos[where ?'a = 'a] by (simp add: less_le) |
1843 using one_plus_one_pos[where ?'a = 'a] by (simp add: less_le) |
1844 |
1844 |
1845 lemma half_sum_eq: "(u + u) / (1+1) = (u::'a::{ordered_field})" |
1845 lemma half_sum_eq: "(u + u) / (1+1) = (u::'a::{linordered_field})" |
1846 proof- |
1846 proof- |
1847 have "(u + u) = (1 + 1) * u" by (simp add: ring_simps) |
1847 have "(u + u) = (1 + 1) * u" by (simp add: ring_simps) |
1848 hence "(u + u) / (1+1) = (1 + 1)*u / (1 + 1)" by simp |
1848 hence "(u + u) / (1+1) = (1 + 1)*u / (1 + 1)" by simp |
1849 with nonzero_mult_divide_cancel_left[OF one_plus_one_nonzero, of u] show ?thesis by simp |
1849 with nonzero_mult_divide_cancel_left[OF one_plus_one_nonzero, of u] show ?thesis by simp |
1850 qed |
1850 qed |
3170 (fn (T,ps) => fn ctxt => SIMPLE_METHOD' (FRParTac.frpar2_tac T ps ctxt)) |
3170 (fn (T,ps) => fn ctxt => SIMPLE_METHOD' (FRParTac.frpar2_tac T ps ctxt)) |
3171 end |
3171 end |
3172 *} "Parametric QE for linear Arithmetic over fields, Version 2" |
3172 *} "Parametric QE for linear Arithmetic over fields, Version 2" |
3173 |
3173 |
3174 |
3174 |
3175 lemma "\<exists>(x::'a::{division_by_zero,ordered_field,number_ring}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0" |
3175 lemma "\<exists>(x::'a::{division_by_zero,linordered_field,number_ring}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0" |
3176 apply (frpar type: "'a::{division_by_zero,ordered_field,number_ring}" pars: "y::'a::{division_by_zero,ordered_field,number_ring}") |
3176 apply (frpar type: "'a::{division_by_zero,linordered_field,number_ring}" pars: "y::'a::{division_by_zero,linordered_field,number_ring}") |
3177 apply (simp add: ring_simps) |
3177 apply (simp add: ring_simps) |
3178 apply (rule spec[where x=y]) |
3178 apply (rule spec[where x=y]) |
3179 apply (frpar type: "'a::{division_by_zero,ordered_field,number_ring}" pars: "z::'a::{division_by_zero,ordered_field,number_ring}") |
3179 apply (frpar type: "'a::{division_by_zero,linordered_field,number_ring}" pars: "z::'a::{division_by_zero,linordered_field,number_ring}") |
3180 by simp |
3180 by simp |
3181 |
3181 |
3182 text{* Collins/Jones Problem *} |
3182 text{* Collins/Jones Problem *} |
3183 (* |
3183 (* |
3184 lemma "\<exists>(r::'a::{division_by_zero,ordered_field,number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0" |
3184 lemma "\<exists>(r::'a::{division_by_zero,linordered_field,number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0" |
3185 proof- |
3185 proof- |
3186 have "(\<exists>(r::'a::{division_by_zero,ordered_field,number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \<longleftrightarrow> (\<exists>(r::'a::{division_by_zero,ordered_field,number_ring}). 0 < r \<and> r < 1 \<and> 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \<and> 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \<longleftrightarrow> ?rhs") |
3186 have "(\<exists>(r::'a::{division_by_zero,linordered_field,number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \<longleftrightarrow> (\<exists>(r::'a::{division_by_zero,linordered_field,number_ring}). 0 < r \<and> r < 1 \<and> 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \<and> 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \<longleftrightarrow> ?rhs") |
3187 by (simp add: ring_simps) |
3187 by (simp add: ring_simps) |
3188 have "?rhs" |
3188 have "?rhs" |
3189 |
3189 |
3190 apply (frpar type: "'a::{division_by_zero,ordered_field,number_ring}" pars: "a::'a::{division_by_zero,ordered_field,number_ring}" "b::'a::{division_by_zero,ordered_field,number_ring}") |
3190 apply (frpar type: "'a::{division_by_zero,linordered_field,number_ring}" pars: "a::'a::{division_by_zero,linordered_field,number_ring}" "b::'a::{division_by_zero,linordered_field,number_ring}") |
3191 apply (simp add: ring_simps) |
3191 apply (simp add: ring_simps) |
3192 oops |
3192 oops |
3193 *) |
3193 *) |
3194 (* |
3194 (* |
3195 lemma "ALL (x::'a::{division_by_zero,ordered_field,number_ring}) y. (1 - t)*x \<le> (1+t)*y \<and> (1 - t)*y \<le> (1+t)*x --> 0 \<le> y" |
3195 lemma "ALL (x::'a::{division_by_zero,linordered_field,number_ring}) y. (1 - t)*x \<le> (1+t)*y \<and> (1 - t)*y \<le> (1+t)*x --> 0 \<le> y" |
3196 apply (frpar type: "'a::{division_by_zero,ordered_field,number_ring}" pars: "t::'a::{division_by_zero,ordered_field,number_ring}") |
3196 apply (frpar type: "'a::{division_by_zero,linordered_field,number_ring}" pars: "t::'a::{division_by_zero,linordered_field,number_ring}") |
3197 oops |
3197 oops |
3198 *) |
3198 *) |
3199 |
3199 |
3200 lemma "\<exists>(x::'a::{division_by_zero,ordered_field,number_ring}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0" |
3200 lemma "\<exists>(x::'a::{division_by_zero,linordered_field,number_ring}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0" |
3201 apply (frpar2 type: "'a::{division_by_zero,ordered_field,number_ring}" pars: "y::'a::{division_by_zero,ordered_field,number_ring}") |
3201 apply (frpar2 type: "'a::{division_by_zero,linordered_field,number_ring}" pars: "y::'a::{division_by_zero,linordered_field,number_ring}") |
3202 apply (simp add: ring_simps) |
3202 apply (simp add: ring_simps) |
3203 apply (rule spec[where x=y]) |
3203 apply (rule spec[where x=y]) |
3204 apply (frpar2 type: "'a::{division_by_zero,ordered_field,number_ring}" pars: "z::'a::{division_by_zero,ordered_field,number_ring}") |
3204 apply (frpar2 type: "'a::{division_by_zero,linordered_field,number_ring}" pars: "z::'a::{division_by_zero,linordered_field,number_ring}") |
3205 by simp |
3205 by simp |
3206 |
3206 |
3207 text{* Collins/Jones Problem *} |
3207 text{* Collins/Jones Problem *} |
3208 |
3208 |
3209 (* |
3209 (* |
3210 lemma "\<exists>(r::'a::{division_by_zero,ordered_field,number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0" |
3210 lemma "\<exists>(r::'a::{division_by_zero,linordered_field,number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0" |
3211 proof- |
3211 proof- |
3212 have "(\<exists>(r::'a::{division_by_zero,ordered_field,number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \<longleftrightarrow> (\<exists>(r::'a::{division_by_zero,ordered_field,number_ring}). 0 < r \<and> r < 1 \<and> 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \<and> 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \<longleftrightarrow> ?rhs") |
3212 have "(\<exists>(r::'a::{division_by_zero,linordered_field,number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \<longleftrightarrow> (\<exists>(r::'a::{division_by_zero,linordered_field,number_ring}). 0 < r \<and> r < 1 \<and> 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \<and> 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \<longleftrightarrow> ?rhs") |
3213 by (simp add: ring_simps) |
3213 by (simp add: ring_simps) |
3214 have "?rhs" |
3214 have "?rhs" |
3215 apply (frpar2 type: "'a::{division_by_zero,ordered_field,number_ring}" pars: "a::'a::{division_by_zero,ordered_field,number_ring}" "b::'a::{division_by_zero,ordered_field,number_ring}") |
3215 apply (frpar2 type: "'a::{division_by_zero,linordered_field,number_ring}" pars: "a::'a::{division_by_zero,linordered_field,number_ring}" "b::'a::{division_by_zero,linordered_field,number_ring}") |
3216 apply simp |
3216 apply simp |
3217 oops |
3217 oops |
3218 *) |
3218 *) |
3219 |
3219 |
3220 (* |
3220 (* |
3221 lemma "ALL (x::'a::{division_by_zero,ordered_field,number_ring}) y. (1 - t)*x \<le> (1+t)*y \<and> (1 - t)*y \<le> (1+t)*x --> 0 \<le> y" |
3221 lemma "ALL (x::'a::{division_by_zero,linordered_field,number_ring}) y. (1 - t)*x \<le> (1+t)*y \<and> (1 - t)*y \<le> (1+t)*x --> 0 \<le> y" |
3222 apply (frpar2 type: "'a::{division_by_zero,ordered_field,number_ring}" pars: "t::'a::{division_by_zero,ordered_field,number_ring}") |
3222 apply (frpar2 type: "'a::{division_by_zero,linordered_field,number_ring}" pars: "t::'a::{division_by_zero,linordered_field,number_ring}") |
3223 apply (simp add: field_simps linorder_neq_iff[symmetric]) |
3223 apply (simp add: field_simps linorder_neq_iff[symmetric]) |
3224 apply ferrack |
3224 apply ferrack |
3225 oops |
3225 oops |
3226 *) |
3226 *) |
3227 end |
3227 end |