# HG changeset patch # User haftmann # Date 1272274455 -7200 # Node ID 89c54f51f55ac1f3f08ed52742814ee50972caba # Parent 0ca616bc6c6f5bc0cbd46760bab242073b7aa00c dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero diff -r 0ca616bc6c6f -r 89c54f51f55a NEWS --- a/NEWS Mon Apr 26 11:34:15 2010 +0200 +++ b/NEWS Mon Apr 26 11:34:15 2010 +0200 @@ -119,8 +119,12 @@ *** HOL *** * Abstract algebra: - * class division_by_zero includes division_ring; + * classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero + include rule inverse 0 = 0 -- subsumes former division_by_zero class. * numerous lemmas have been ported from field to division_ring; + * dropped theorem group group_simps, use algebra_simps instead; + * dropped theorem group ring_simps, use field_simps instead; + * proper theorem collection field_simps subsumes former theorem groups field_eq_simps and field_simps; * dropped lemma eq_minus_self_iff which is a duplicate for equal_neg_zero. INCOMPATIBILITY. diff -r 0ca616bc6c6f -r 89c54f51f55a src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Mon Apr 26 11:34:15 2010 +0200 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Mon Apr 26 11:34:15 2010 +0200 @@ -27,7 +27,7 @@ "tmsize (CNP n c a) = 3 + polysize c + tmsize a " (* Semantics of terms tm *) -consts Itm :: "'a::{ring_char_0,division_by_zero,field} list \ 'a list \ tm \ 'a" +consts Itm :: "'a::{ring_char_0,division_ring_inverse_zero,field} list \ 'a list \ tm \ 'a" primrec "Itm vs bs (CP c) = (Ipoly vs c)" "Itm vs bs (Bound n) = bs!n" @@ -239,7 +239,7 @@ lemma tmadd[simp]: "Itm vs bs (tmadd (t,s)) = Itm vs bs (Add t s)" apply (induct t s rule: tmadd.induct, simp_all add: Let_def) apply (case_tac "c1 +\<^sub>p c2 = 0\<^sub>p",case_tac "n1 \ n2", simp_all) -apply (case_tac "n1 = n2", simp_all add: ring_simps) +apply (case_tac "n1 = n2", simp_all add: field_simps) apply (simp only: right_distrib[symmetric]) by (auto simp del: polyadd simp add: polyadd[symmetric]) @@ -259,7 +259,7 @@ "tmmul t = (\ i. Mul i t)" lemma tmmul[simp]: "Itm vs bs (tmmul t i) = Itm vs bs (Mul i t)" -by (induct t arbitrary: i rule: tmmul.induct, simp_all add: ring_simps) +by (induct t arbitrary: i rule: tmmul.induct, simp_all add: field_simps) lemma tmmul_nb0[simp]: "tmbound0 t \ tmbound0 (tmmul t i)" by (induct t arbitrary: i rule: tmmul.induct, auto ) @@ -270,7 +270,7 @@ by (induct t arbitrary: i rule: tmmul.induct, auto simp add: Let_def) lemma tmmul_allpolys_npoly[simp]: - assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero, field})" + assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero, field})" shows "allpolys isnpoly t \ isnpoly c \ allpolys isnpoly (tmmul t c)" by (induct t rule: tmmul.induct, simp_all add: Let_def polymul_norm) definition tmneg :: "tm \ tm" where @@ -296,7 +296,7 @@ using tmneg_def by simp lemma [simp]: "isnpoly (C (-1,1))" unfolding isnpoly_def by simp lemma tmneg_allpolys_npoly[simp]: - assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero, field})" + assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero, field})" shows "allpolys isnpoly t \ allpolys isnpoly (tmneg t)" unfolding tmneg_def by auto @@ -310,7 +310,7 @@ lemma tmsub_blt[simp]: "\tmboundslt n t ; tmboundslt n s\ \ tmboundslt n (tmsub t s )" using tmsub_def by simp lemma tmsub_allpolys_npoly[simp]: - assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero, field})" + assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero, field})" shows "allpolys isnpoly t \ allpolys isnpoly s \ allpolys isnpoly (tmsub t s)" unfolding tmsub_def by (simp add: isnpoly_def) @@ -324,8 +324,8 @@ "simptm (CNP n c t) = (let c' = polynate c in if c' = 0\<^sub>p then simptm t else tmadd (CNP n c' (CP 0\<^sub>p ), simptm t))" lemma polynate_stupid: - assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero, field})" - shows "polynate t = 0\<^sub>p \ Ipoly bs t = (0::'a::{ring_char_0,division_by_zero, field})" + assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero, field})" + shows "polynate t = 0\<^sub>p \ Ipoly bs t = (0::'a::{ring_char_0,division_ring_inverse_zero, field})" apply (subst polynate[symmetric]) apply simp done @@ -345,7 +345,7 @@ lemma [simp]: "isnpoly 0\<^sub>p" and [simp]: "isnpoly (C(1,1))" by (simp_all add: isnpoly_def) lemma simptm_allpolys_npoly[simp]: - assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero, field})" + assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero, field})" shows "allpolys isnpoly (simptm p)" by (induct p rule: simptm.induct, auto simp add: Let_def) @@ -369,14 +369,14 @@ "tmbound 0 (snd (split0 t)) \ (Itm vs bs (CNP 0 (fst (split0 t)) (snd (split0 t))) = Itm vs bs t)" apply (induct t rule: split0.induct) apply simp - apply (simp add: Let_def split_def ring_simps) - apply (simp add: Let_def split_def ring_simps) - apply (simp add: Let_def split_def ring_simps) - apply (simp add: Let_def split_def ring_simps) - apply (simp add: Let_def split_def ring_simps) + apply (simp add: Let_def split_def field_simps) + apply (simp add: Let_def split_def field_simps) + apply (simp add: Let_def split_def field_simps) + apply (simp add: Let_def split_def field_simps) + apply (simp add: Let_def split_def field_simps) apply (simp add: Let_def split_def mult_assoc right_distrib[symmetric]) - apply (simp add: Let_def split_def ring_simps) - apply (simp add: Let_def split_def ring_simps) + apply (simp add: Let_def split_def field_simps) + apply (simp add: Let_def split_def field_simps) done lemma split0_ci: "split0 t = (c',t') \ Itm vs bs t = Itm vs bs (CNP 0 c' t')" @@ -387,7 +387,7 @@ qed lemma split0_nb0: - assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero, field})" + assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero, field})" shows "split0 t = (c',t') \ tmbound 0 t'" proof- fix c' t' @@ -395,7 +395,7 @@ with conjunct1[OF split0[where t="t"]] show "tmbound 0 t'" by simp qed -lemma split0_nb0'[simp]: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero, field})" +lemma split0_nb0'[simp]: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero, field})" shows "tmbound0 (snd (split0 t))" using split0_nb0[of t "fst (split0 t)" "snd (split0 t)"] by (simp add: tmbound0_tmbound_iff) @@ -418,7 +418,7 @@ lemma allpolys_split0: "allpolys isnpoly p \ allpolys isnpoly (snd (split0 p))" by (induct p rule: split0.induct, auto simp add: isnpoly_def Let_def split_def split0_stupid) -lemma isnpoly_fst_split0: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero, field})" +lemma isnpoly_fst_split0: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero, field})" shows "allpolys isnpoly p \ isnpoly (fst (split0 p))" by (induct p rule: split0.induct, @@ -447,7 +447,7 @@ by (induct p rule: fmsize.induct) simp_all (* Semantics of formulae (fm) *) -consts Ifm ::"'a::{division_by_zero,linordered_field} list \ 'a list \ fm \ bool" +consts Ifm ::"'a::{division_ring_inverse_zero,linordered_field} list \ 'a list \ fm \ bool" primrec "Ifm vs bs T = True" "Ifm vs bs F = False" @@ -969,24 +969,24 @@ definition "simpeq t = (let (c,s) = split0 (simptm t) in if c= 0\<^sub>p then eq s else Eq (CNP 0 c s))" definition "simpneq t = (let (c,s) = split0 (simptm t) in if c= 0\<^sub>p then neq s else NEq (CNP 0 c s))" -lemma simplt_islin[simp]: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})" +lemma simplt_islin[simp]: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" shows "islin (simplt t)" unfolding simplt_def using split0_nb0' by (auto simp add: lt_lin Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly] islin_stupid allpolys_split0[OF simptm_allpolys_npoly]) -lemma simple_islin[simp]: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})" +lemma simple_islin[simp]: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" shows "islin (simple t)" unfolding simple_def using split0_nb0' by (auto simp add: Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly] islin_stupid allpolys_split0[OF simptm_allpolys_npoly] le_lin) -lemma simpeq_islin[simp]: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})" +lemma simpeq_islin[simp]: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" shows "islin (simpeq t)" unfolding simpeq_def using split0_nb0' by (auto simp add: Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly] islin_stupid allpolys_split0[OF simptm_allpolys_npoly] eq_lin) -lemma simpneq_islin[simp]: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})" +lemma simpneq_islin[simp]: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" shows "islin (simpneq t)" unfolding simpneq_def using split0_nb0' @@ -994,7 +994,7 @@ lemma really_stupid: "\ (\c1 s'. (c1, s') \ split0 s)" by (cases "split0 s", auto) -lemma split0_npoly: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})" +lemma split0_npoly: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" and n: "allpolys isnpoly t" shows "isnpoly (fst (split0 t))" and "allpolys isnpoly (snd (split0 t))" using n @@ -1083,7 +1083,7 @@ apply (case_tac poly, auto) done -lemma simplt_nb[simp]: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})" +lemma simplt_nb[simp]: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" shows "tmbound0 t \ bound0 (simplt t)" using split0 [of "simptm t" vs bs] proof(simp add: simplt_def Let_def split_def) @@ -1100,7 +1100,7 @@ fst (split0 (simptm t)) = 0\<^sub>p" by (simp add: simplt_def Let_def split_def lt_nb) qed -lemma simple_nb[simp]: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})" +lemma simple_nb[simp]: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" shows "tmbound0 t \ bound0 (simple t)" using split0 [of "simptm t" vs bs] proof(simp add: simple_def Let_def split_def) @@ -1117,7 +1117,7 @@ fst (split0 (simptm t)) = 0\<^sub>p" by (simp add: simplt_def Let_def split_def le_nb) qed -lemma simpeq_nb[simp]: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})" +lemma simpeq_nb[simp]: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" shows "tmbound0 t \ bound0 (simpeq t)" using split0 [of "simptm t" vs bs] proof(simp add: simpeq_def Let_def split_def) @@ -1134,7 +1134,7 @@ fst (split0 (simptm t)) = 0\<^sub>p" by (simp add: simpeq_def Let_def split_def eq_nb) qed -lemma simpneq_nb[simp]: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})" +lemma simpneq_nb[simp]: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" shows "tmbound0 t \ bound0 (simpneq t)" using split0 [of "simptm t" vs bs] proof(simp add: simpneq_def Let_def split_def) @@ -1267,7 +1267,7 @@ lemma simpfm[simp]: "Ifm vs bs (simpfm p) = Ifm vs bs p" by(induct p arbitrary: bs rule: simpfm.induct, auto) -lemma simpfm_bound0: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})" +lemma simpfm_bound0: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" shows "bound0 p \ bound0 (simpfm p)" by (induct p rule: simpfm.induct, auto) @@ -1296,7 +1296,7 @@ lemma disj_lin: "islin p \ islin q \ islin (disj p q)" by (simp add: disj_def) lemma conj_lin: "islin p \ islin q \ islin (conj p q)" by (simp add: conj_def) -lemma assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})" +lemma assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" shows "qfree p \ islin (simpfm p)" apply (induct p rule: simpfm.induct) apply (simp_all add: conj_lin disj_lin) @@ -1698,11 +1698,11 @@ {assume c: "?N c > 0" from px pos_less_divide_eq[OF c, where a="x" and b="-?Nt x s"] have px': "x < - ?Nt x s / ?N c" - by (auto simp add: not_less ring_simps) + by (auto simp add: not_less field_simps) {assume y: "y < - ?Nt x s / ?N c" hence "y * ?N c < - ?Nt x s" by (simp add: pos_less_divide_eq[OF c, where a="y" and b="-?Nt x s", symmetric]) - hence "?N c * y + ?Nt x s < 0" by (simp add: ring_simps) + hence "?N c * y + ?Nt x s < 0" by (simp add: field_simps) hence ?case using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"] by simp} moreover {assume y: "y > -?Nt x s / ?N c" @@ -1715,11 +1715,11 @@ {assume c: "?N c < 0" from px neg_divide_less_eq[OF c, where a="x" and b="-?Nt x s"] have px': "x > - ?Nt x s / ?N c" - by (auto simp add: not_less ring_simps) + by (auto simp add: not_less field_simps) {assume y: "y > - ?Nt x s / ?N c" hence "y * ?N c < - ?Nt x s" by (simp add: neg_divide_less_eq[OF c, where a="y" and b="-?Nt x s", symmetric]) - hence "?N c * y + ?Nt x s < 0" by (simp add: ring_simps) + hence "?N c * y + ?Nt x s < 0" by (simp add: field_simps) hence ?case using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"] by simp} moreover {assume y: "y < -?Nt x s / ?N c" @@ -1743,11 +1743,11 @@ moreover {assume c: "?N c > 0" from px pos_le_divide_eq[OF c, where a="x" and b="-?Nt x s"] - have px': "x <= - ?Nt x s / ?N c" by (simp add: not_less ring_simps) + have px': "x <= - ?Nt x s / ?N c" by (simp add: not_less field_simps) {assume y: "y < - ?Nt x s / ?N c" hence "y * ?N c < - ?Nt x s" by (simp add: pos_less_divide_eq[OF c, where a="y" and b="-?Nt x s", symmetric]) - hence "?N c * y + ?Nt x s < 0" by (simp add: ring_simps) + hence "?N c * y + ?Nt x s < 0" by (simp add: field_simps) hence ?case using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"] by simp} moreover {assume y: "y > -?Nt x s / ?N c" @@ -1759,11 +1759,11 @@ moreover {assume c: "?N c < 0" from px neg_divide_le_eq[OF c, where a="x" and b="-?Nt x s"] - have px': "x >= - ?Nt x s / ?N c" by (simp add: ring_simps) + have px': "x >= - ?Nt x s / ?N c" by (simp add: field_simps) {assume y: "y > - ?Nt x s / ?N c" hence "y * ?N c < - ?Nt x s" by (simp add: neg_divide_less_eq[OF c, where a="y" and b="-?Nt x s", symmetric]) - hence "?N c * y + ?Nt x s < 0" by (simp add: ring_simps) + hence "?N c * y + ?Nt x s < 0" by (simp add: field_simps) hence ?case using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"] by simp} moreover {assume y: "y < -?Nt x s / ?N c" @@ -1787,7 +1787,7 @@ moreover {assume c: "?N c > 0" hence cnz: "?N c \ 0" by simp from px eq_divide_eq[of "x" "-?Nt x s" "?N c"] cnz - have px': "x = - ?Nt x s / ?N c" by (simp add: ring_simps) + have px': "x = - ?Nt x s / ?N c" by (simp add: field_simps) {assume y: "y < -?Nt x s / ?N c" with ly have eu: "l < - ?Nt x s / ?N c" by auto with noS ly yu have th: "- ?Nt x s / ?N c \ u" by (cases "- ?Nt x s / ?N c < u", auto) @@ -1802,7 +1802,7 @@ moreover {assume c: "?N c < 0" hence cnz: "?N c \ 0" by simp from px eq_divide_eq[of "x" "-?Nt x s" "?N c"] cnz - have px': "x = - ?Nt x s / ?N c" by (simp add: ring_simps) + have px': "x = - ?Nt x s / ?N c" by (simp add: field_simps) {assume y: "y < -?Nt x s / ?N c" with ly have eu: "l < - ?Nt x s / ?N c" by auto with noS ly yu have th: "- ?Nt x s / ?N c \ u" by (cases "- ?Nt x s / ?N c < u", auto) @@ -1829,7 +1829,7 @@ moreover {assume c: "?N c \ 0" from yne c eq_divide_eq[of "y" "- ?Nt x s" "?N c"] have ?case - by (simp add: ring_simps tmbound0_I[OF lin(3), of vs x bs y] sum_eq[symmetric]) } + by (simp add: field_simps tmbound0_I[OF lin(3), of vs x bs y] sum_eq[symmetric]) } ultimately show ?case by blast 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"]) @@ -1844,7 +1844,7 @@ lemma half_sum_eq: "(u + u) / (1+1) = (u::'a::{linordered_field})" proof- - have "(u + u) = (1 + 1) * u" by (simp add: ring_simps) + have "(u + u) = (1 + 1) * u" by (simp add: field_simps) hence "(u + u) / (1+1) = (1 + 1)*u / (1 + 1)" by simp with nonzero_mult_divide_cancel_left[OF one_plus_one_nonzero, of u] show ?thesis by simp qed @@ -1987,7 +1987,7 @@ also have "\ \ (1 + 1)*?d * (?a * (-?s / ((1 + 1)*?d)) + ?r) = 0" using d mult_cancel_left[of "(1 + 1)*?d" "(?a * (-?s / ((1 + 1)*?d)) + ?r)" 0] by simp also have "\ \ (- ?a * ?s) * ((1 + 1)*?d / ((1 + 1)*?d)) + (1 + 1)*?d*?r= 0" - by (simp add: ring_simps right_distrib[of "(1 + 1)*?d"] del: right_distrib) + by (simp add: field_simps right_distrib[of "(1 + 1)*?d"] del: right_distrib) also have "\ \ - (?a * ?s) + (1 + 1)*?d*?r = 0" using d by simp finally have ?thesis using c d @@ -2003,7 +2003,7 @@ also have "\ \ (1 + 1)*?c * (?a * (-?t / ((1 + 1)*?c)) + ?r) = 0" using c mult_cancel_left[of "(1 + 1)*?c" "(?a * (-?t / ((1 + 1)*?c)) + ?r)" 0] by simp also have "\ \ (?a * -?t)* ((1 + 1)*?c) / ((1 + 1)*?c) + (1 + 1)*?c*?r= 0" - by (simp add: ring_simps right_distrib[of "(1 + 1)*?c"] del: right_distrib) + by (simp add: field_simps right_distrib[of "(1 + 1)*?c"] del: right_distrib) also have "\ \ - (?a * ?t) + (1 + 1)*?c*?r = 0" using c by simp finally have ?thesis using c d apply (simp add: r[of "- (?t/ ((1 + 1)*?c))"] msubsteq_def Let_def evaldjf_ex del: one_add_one_is_two) @@ -2014,19 +2014,19 @@ {assume c: "?c \ 0" and d: "?d\0" hence dc: "?c * ?d *(1 + 1) \ 0" by simp from add_frac_eq[OF c d, of "- ?t" "- ?s"] have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)" - by (simp add: ring_simps) + by (simp add: field_simps) have "?rhs \ Ifm vs (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d) # bs) (Eq (CNP 0 a r))" by (simp only: th) also have "\ \ ?a * (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)) + ?r = 0" by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"]) also have "\ \ ((1 + 1) * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)) + ?r) =0 " using c d mult_cancel_left[of "(1 + 1) * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ ((1 + 1)*?c*?d)) + ?r" 0] by simp also have "\ \ ?a * (- (?d * ?t + ?c* ?s )) + (1 + 1)*?c*?d*?r =0" - using nonzero_mult_divide_cancel_left[OF dc] c d - by (simp add: ring_simps diff_divide_distrib del: left_distrib) + using nonzero_mult_divide_cancel_left [OF dc] c d + by (simp add: algebra_simps diff_divide_distrib del: left_distrib) finally have ?thesis using c d - apply (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"] msubsteq_def Let_def evaldjf_ex ring_simps) + apply (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"] msubsteq_def Let_def evaldjf_ex field_simps) apply (simp only: one_add_one_is_two[symmetric] of_int_add) - apply (simp add: ring_simps) + apply (simp add: field_simps) done } ultimately show ?thesis by blast qed @@ -2075,7 +2075,7 @@ also have "\ \ (1 + 1)*?d * (?a * (-?s / ((1 + 1)*?d)) + ?r) \ 0" using d mult_cancel_left[of "(1 + 1)*?d" "(?a * (-?s / ((1 + 1)*?d)) + ?r)" 0] by simp also have "\ \ (- ?a * ?s) * ((1 + 1)*?d / ((1 + 1)*?d)) + (1 + 1)*?d*?r\ 0" - by (simp add: ring_simps right_distrib[of "(1 + 1)*?d"] del: right_distrib) + by (simp add: field_simps right_distrib[of "(1 + 1)*?d"] del: right_distrib) also have "\ \ - (?a * ?s) + (1 + 1)*?d*?r \ 0" using d by simp finally have ?thesis using c d @@ -2091,7 +2091,7 @@ also have "\ \ (1 + 1)*?c * (?a * (-?t / ((1 + 1)*?c)) + ?r) \ 0" using c mult_cancel_left[of "(1 + 1)*?c" "(?a * (-?t / ((1 + 1)*?c)) + ?r)" 0] by simp also have "\ \ (?a * -?t)* ((1 + 1)*?c) / ((1 + 1)*?c) + (1 + 1)*?c*?r \ 0" - by (simp add: ring_simps right_distrib[of "(1 + 1)*?c"] del: right_distrib) + by (simp add: field_simps right_distrib[of "(1 + 1)*?c"] del: right_distrib) also have "\ \ - (?a * ?t) + (1 + 1)*?c*?r \ 0" using c by simp finally have ?thesis using c d apply (simp add: r[of "- (?t/ ((1 + 1)*?c))"] msubstneq_def Let_def evaldjf_ex del: one_add_one_is_two) @@ -2102,7 +2102,7 @@ {assume c: "?c \ 0" and d: "?d\0" hence dc: "?c * ?d *(1 + 1) \ 0" by simp from add_frac_eq[OF c d, of "- ?t" "- ?s"] have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)" - by (simp add: ring_simps) + by (simp add: field_simps) have "?rhs \ Ifm vs (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d) # bs) (NEq (CNP 0 a r))" by (simp only: th) also have "\ \ ?a * (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)) + ?r \ 0" by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"]) @@ -2110,11 +2110,11 @@ using c d mult_cancel_left[of "(1 + 1) * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ ((1 + 1)*?c*?d)) + ?r" 0] by simp also have "\ \ ?a * (- (?d * ?t + ?c* ?s )) + (1 + 1)*?c*?d*?r \ 0" using nonzero_mult_divide_cancel_left[OF dc] c d - by (simp add: ring_simps diff_divide_distrib del: left_distrib) + by (simp add: algebra_simps diff_divide_distrib del: left_distrib) finally have ?thesis using c d - apply (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"] msubstneq_def Let_def evaldjf_ex ring_simps) + apply (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"] msubstneq_def Let_def evaldjf_ex field_simps) apply (simp only: one_add_one_is_two[symmetric] of_int_add) - apply (simp add: ring_simps) + apply (simp add: field_simps) done } ultimately show ?thesis by blast qed @@ -2169,7 +2169,7 @@ from dc' have dc'': "\ (1 + 1)*?c *?d < 0" by simp from add_frac_eq[OF c d, of "- ?t" "- ?s"] have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)" - by (simp add: ring_simps) + by (simp add: field_simps) have "?rhs \ Ifm vs (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d) # bs) (Lt (CNP 0 a r))" by (simp only: th) also have "\ \ ?a * (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)) + ?r < 0" by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"]) @@ -2178,11 +2178,11 @@ 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 also have "\ \ ?a * (- (?d * ?t + ?c* ?s )) + (1 + 1)*?c*?d*?r < 0" using nonzero_mult_divide_cancel_left[of "(1 + 1)*?c*?d"] c d - by (simp add: ring_simps diff_divide_distrib del: left_distrib) + by (simp add: algebra_simps diff_divide_distrib del: left_distrib) finally have ?thesis using dc c d nc nd dc' - apply (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"] msubstlt_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm) + 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) apply (simp only: one_add_one_is_two[symmetric] of_int_add) - by (simp add: ring_simps order_less_not_sym[OF dc])} + by (simp add: field_simps order_less_not_sym[OF dc])} moreover {assume dc: "?c*?d < 0" @@ -2191,7 +2191,7 @@ hence c:"?c \ 0" and d: "?d\ 0" by auto from add_frac_eq[OF c d, of "- ?t" "- ?s"] have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)" - by (simp add: ring_simps) + by (simp add: field_simps) have "?rhs \ Ifm vs (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d) # bs) (Lt (CNP 0 a r))" by (simp only: th) also have "\ \ ?a * (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)) + ?r < 0" by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"]) @@ -2201,78 +2201,78 @@ 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 also have "\ \ ?a * ((?d * ?t + ?c* ?s )) - (1 + 1)*?c*?d*?r < 0" using nonzero_mult_divide_cancel_left[of "(1 + 1)*?c*?d"] c d - by (simp add: ring_simps diff_divide_distrib del: left_distrib) + by (simp add: algebra_simps diff_divide_distrib del: left_distrib) finally have ?thesis using dc c d nc nd - apply (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"] msubstlt_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm) + 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) apply (simp only: one_add_one_is_two[symmetric] of_int_add) - by (simp add: ring_simps order_less_not_sym[OF dc]) } + by (simp add: field_simps order_less_not_sym[OF dc]) } moreover {assume c: "?c > 0" and d: "?d=0" from c have c'': "(1 + 1)*?c > 0" by (simp add: zero_less_mult_iff) from c have c': "(1 + 1)*?c \ 0" by simp - from d have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?t / ((1 + 1)*?c)" by (simp add: ring_simps) + from d have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?t / ((1 + 1)*?c)" by (simp add: field_simps) have "?rhs \ Ifm vs (- ?t / ((1 + 1)*?c) # bs) (Lt (CNP 0 a r))" by (simp only: th) also have "\ \ ?a* (- ?t / ((1 + 1)*?c))+ ?r < 0" by (simp add: r[of "- (?t / ((1 + 1)*?c))"]) also have "\ \ (1 + 1)*?c * (?a* (- ?t / ((1 + 1)*?c))+ ?r) < 0" 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 also have "\ \ - ?a*?t+ (1 + 1)*?c *?r < 0" using nonzero_mult_divide_cancel_left[OF c'] c - by (simp add: ring_simps diff_divide_distrib less_le del: left_distrib) + by (simp add: algebra_simps diff_divide_distrib less_le del: left_distrib) finally have ?thesis using c d nc nd - apply(simp add: r[of "- (?t / ((1 + 1)*?c))"] msubstlt_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm) + apply(simp add: r[of "- (?t / ((1 + 1)*?c))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm) apply (simp only: one_add_one_is_two[symmetric] of_int_add) using c order_less_not_sym[OF c] less_imp_neq[OF c] - by (simp add: ring_simps ) } + by (simp add: field_simps ) } moreover {assume c: "?c < 0" and d: "?d=0" hence c': "(1 + 1)*?c \ 0" by simp from c have c'': "(1 + 1)*?c < 0" by (simp add: mult_less_0_iff) - from d have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?t / ((1 + 1)*?c)" by (simp add: ring_simps) + from d have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?t / ((1 + 1)*?c)" by (simp add: field_simps) have "?rhs \ Ifm vs (- ?t / ((1 + 1)*?c) # bs) (Lt (CNP 0 a r))" by (simp only: th) also have "\ \ ?a* (- ?t / ((1 + 1)*?c))+ ?r < 0" by (simp add: r[of "- (?t / ((1 + 1)*?c))"]) also have "\ \ (1 + 1)*?c * (?a* (- ?t / ((1 + 1)*?c))+ ?r) > 0" 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 also have "\ \ ?a*?t - (1 + 1)*?c *?r < 0" using nonzero_mult_divide_cancel_left[OF c'] c order_less_not_sym[OF c''] less_imp_neq[OF c''] c'' - by (simp add: ring_simps diff_divide_distrib del: left_distrib) + by (simp add: algebra_simps diff_divide_distrib del: left_distrib) finally have ?thesis using c d nc nd - apply(simp add: r[of "- (?t / ((1 + 1)*?c))"] msubstlt_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm) + apply(simp add: r[of "- (?t / ((1 + 1)*?c))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm) apply (simp only: one_add_one_is_two[symmetric] of_int_add) using c order_less_not_sym[OF c] less_imp_neq[OF c] - by (simp add: ring_simps ) } + by (simp add: field_simps ) } moreover moreover {assume c: "?c = 0" and d: "?d>0" from d have d'': "(1 + 1)*?d > 0" by (simp add: zero_less_mult_iff) from d have d': "(1 + 1)*?d \ 0" by simp - from c have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?s / ((1 + 1)*?d)" by (simp add: ring_simps) + from c have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?s / ((1 + 1)*?d)" by (simp add: field_simps) have "?rhs \ Ifm vs (- ?s / ((1 + 1)*?d) # bs) (Lt (CNP 0 a r))" by (simp only: th) also have "\ \ ?a* (- ?s / ((1 + 1)*?d))+ ?r < 0" by (simp add: r[of "- (?s / ((1 + 1)*?d))"]) also have "\ \ (1 + 1)*?d * (?a* (- ?s / ((1 + 1)*?d))+ ?r) < 0" 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 also have "\ \ - ?a*?s+ (1 + 1)*?d *?r < 0" using nonzero_mult_divide_cancel_left[OF d'] d - by (simp add: ring_simps diff_divide_distrib less_le del: left_distrib) + by (simp add: algebra_simps diff_divide_distrib less_le del: left_distrib) finally have ?thesis using c d nc nd - apply(simp add: r[of "- (?s / ((1 + 1)*?d))"] msubstlt_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm) + apply(simp add: r[of "- (?s / ((1 + 1)*?d))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm) apply (simp only: one_add_one_is_two[symmetric] of_int_add) using d order_less_not_sym[OF d] less_imp_neq[OF d] - by (simp add: ring_simps ) } + by (simp add: field_simps) } moreover {assume c: "?c = 0" and d: "?d<0" hence d': "(1 + 1)*?d \ 0" by simp from d have d'': "(1 + 1)*?d < 0" by (simp add: mult_less_0_iff) - from c have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?s / ((1 + 1)*?d)" by (simp add: ring_simps) + from c have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?s / ((1 + 1)*?d)" by (simp add: field_simps) have "?rhs \ Ifm vs (- ?s / ((1 + 1)*?d) # bs) (Lt (CNP 0 a r))" by (simp only: th) also have "\ \ ?a* (- ?s / ((1 + 1)*?d))+ ?r < 0" by (simp add: r[of "- (?s / ((1 + 1)*?d))"]) also have "\ \ (1 + 1)*?d * (?a* (- ?s / ((1 + 1)*?d))+ ?r) > 0" 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 also have "\ \ ?a*?s - (1 + 1)*?d *?r < 0" using nonzero_mult_divide_cancel_left[OF d'] d order_less_not_sym[OF d''] less_imp_neq[OF d''] d'' - by (simp add: ring_simps diff_divide_distrib del: left_distrib) + by (simp add: algebra_simps diff_divide_distrib del: left_distrib) finally have ?thesis using c d nc nd - apply(simp add: r[of "- (?s / ((1 + 1)*?d))"] msubstlt_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm) + apply(simp add: r[of "- (?s / ((1 + 1)*?d))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm) apply (simp only: one_add_one_is_two[symmetric] of_int_add) using d order_less_not_sym[OF d] less_imp_neq[OF d] - by (simp add: ring_simps ) } + by (simp add: field_simps ) } ultimately show ?thesis by blast qed @@ -2325,7 +2325,7 @@ from dc' have dc'': "\ (1 + 1)*?c *?d < 0" by simp from add_frac_eq[OF c d, of "- ?t" "- ?s"] have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)" - by (simp add: ring_simps) + by (simp add: field_simps) have "?rhs \ Ifm vs (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d) # bs) (Le (CNP 0 a r))" by (simp only: th) also have "\ \ ?a * (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)) + ?r <= 0" by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"]) @@ -2334,11 +2334,11 @@ 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 also have "\ \ ?a * (- (?d * ?t + ?c* ?s )) + (1 + 1)*?c*?d*?r <= 0" using nonzero_mult_divide_cancel_left[of "(1 + 1)*?c*?d"] c d - by (simp add: ring_simps diff_divide_distrib del: left_distrib) + by (simp add: algebra_simps diff_divide_distrib del: left_distrib) finally have ?thesis using dc c d nc nd dc' - apply (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"] msubstle_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm) + 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) apply (simp only: one_add_one_is_two[symmetric] of_int_add) - by (simp add: ring_simps order_less_not_sym[OF dc])} + by (simp add: field_simps order_less_not_sym[OF dc])} moreover {assume dc: "?c*?d < 0" @@ -2347,7 +2347,7 @@ hence c:"?c \ 0" and d: "?d\ 0" by auto from add_frac_eq[OF c d, of "- ?t" "- ?s"] have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)" - by (simp add: ring_simps) + by (simp add: field_simps) have "?rhs \ Ifm vs (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d) # bs) (Le (CNP 0 a r))" by (simp only: th) also have "\ \ ?a * (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)) + ?r <= 0" by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"]) @@ -2357,78 +2357,78 @@ 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 also have "\ \ ?a * ((?d * ?t + ?c* ?s )) - (1 + 1)*?c*?d*?r <= 0" using nonzero_mult_divide_cancel_left[of "(1 + 1)*?c*?d"] c d - by (simp add: ring_simps diff_divide_distrib del: left_distrib) + by (simp add: algebra_simps diff_divide_distrib del: left_distrib) finally have ?thesis using dc c d nc nd - apply (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"] msubstle_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm) + 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) apply (simp only: one_add_one_is_two[symmetric] of_int_add) - by (simp add: ring_simps order_less_not_sym[OF dc]) } + by (simp add: field_simps order_less_not_sym[OF dc]) } moreover {assume c: "?c > 0" and d: "?d=0" from c have c'': "(1 + 1)*?c > 0" by (simp add: zero_less_mult_iff) from c have c': "(1 + 1)*?c \ 0" by simp - from d have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?t / ((1 + 1)*?c)" by (simp add: ring_simps) + from d have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?t / ((1 + 1)*?c)" by (simp add: field_simps) have "?rhs \ Ifm vs (- ?t / ((1 + 1)*?c) # bs) (Le (CNP 0 a r))" by (simp only: th) also have "\ \ ?a* (- ?t / ((1 + 1)*?c))+ ?r <= 0" by (simp add: r[of "- (?t / ((1 + 1)*?c))"]) also have "\ \ (1 + 1)*?c * (?a* (- ?t / ((1 + 1)*?c))+ ?r) <= 0" 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 also have "\ \ - ?a*?t+ (1 + 1)*?c *?r <= 0" using nonzero_mult_divide_cancel_left[OF c'] c - by (simp add: ring_simps diff_divide_distrib less_le del: left_distrib) + by (simp add: algebra_simps diff_divide_distrib less_le del: left_distrib) finally have ?thesis using c d nc nd - apply(simp add: r[of "- (?t / ((1 + 1)*?c))"] msubstle_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm) + apply(simp add: r[of "- (?t / ((1 + 1)*?c))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm) apply (simp only: one_add_one_is_two[symmetric] of_int_add) using c order_less_not_sym[OF c] less_imp_neq[OF c] - by (simp add: ring_simps ) } + by (simp add: field_simps ) } moreover {assume c: "?c < 0" and d: "?d=0" hence c': "(1 + 1)*?c \ 0" by simp from c have c'': "(1 + 1)*?c < 0" by (simp add: mult_less_0_iff) - from d have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?t / ((1 + 1)*?c)" by (simp add: ring_simps) + from d have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?t / ((1 + 1)*?c)" by (simp add: field_simps) have "?rhs \ Ifm vs (- ?t / ((1 + 1)*?c) # bs) (Le (CNP 0 a r))" by (simp only: th) also have "\ \ ?a* (- ?t / ((1 + 1)*?c))+ ?r <= 0" by (simp add: r[of "- (?t / ((1 + 1)*?c))"]) also have "\ \ (1 + 1)*?c * (?a* (- ?t / ((1 + 1)*?c))+ ?r) >= 0" 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 also have "\ \ ?a*?t - (1 + 1)*?c *?r <= 0" using nonzero_mult_divide_cancel_left[OF c'] c order_less_not_sym[OF c''] less_imp_neq[OF c''] c'' - by (simp add: ring_simps diff_divide_distrib del: left_distrib) + by (simp add: algebra_simps diff_divide_distrib del: left_distrib) finally have ?thesis using c d nc nd - apply(simp add: r[of "- (?t / ((1 + 1)*?c))"] msubstle_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm) + apply(simp add: r[of "- (?t / ((1 + 1)*?c))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm) apply (simp only: one_add_one_is_two[symmetric] of_int_add) using c order_less_not_sym[OF c] less_imp_neq[OF c] - by (simp add: ring_simps ) } + by (simp add: field_simps ) } moreover moreover {assume c: "?c = 0" and d: "?d>0" from d have d'': "(1 + 1)*?d > 0" by (simp add: zero_less_mult_iff) from d have d': "(1 + 1)*?d \ 0" by simp - from c have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?s / ((1 + 1)*?d)" by (simp add: ring_simps) + from c have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?s / ((1 + 1)*?d)" by (simp add: field_simps) have "?rhs \ Ifm vs (- ?s / ((1 + 1)*?d) # bs) (Le (CNP 0 a r))" by (simp only: th) also have "\ \ ?a* (- ?s / ((1 + 1)*?d))+ ?r <= 0" by (simp add: r[of "- (?s / ((1 + 1)*?d))"]) also have "\ \ (1 + 1)*?d * (?a* (- ?s / ((1 + 1)*?d))+ ?r) <= 0" 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 also have "\ \ - ?a*?s+ (1 + 1)*?d *?r <= 0" using nonzero_mult_divide_cancel_left[OF d'] d - by (simp add: ring_simps diff_divide_distrib less_le del: left_distrib) + by (simp add: algebra_simps diff_divide_distrib less_le del: left_distrib) finally have ?thesis using c d nc nd - apply(simp add: r[of "- (?s / ((1 + 1)*?d))"] msubstle_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm) + apply(simp add: r[of "- (?s / ((1 + 1)*?d))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm) apply (simp only: one_add_one_is_two[symmetric] of_int_add) using d order_less_not_sym[OF d] less_imp_neq[OF d] - by (simp add: ring_simps ) } + by (simp add: field_simps ) } moreover {assume c: "?c = 0" and d: "?d<0" hence d': "(1 + 1)*?d \ 0" by simp from d have d'': "(1 + 1)*?d < 0" by (simp add: mult_less_0_iff) - from c have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?s / ((1 + 1)*?d)" by (simp add: ring_simps) + from c have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?s / ((1 + 1)*?d)" by (simp add: field_simps) have "?rhs \ Ifm vs (- ?s / ((1 + 1)*?d) # bs) (Le (CNP 0 a r))" by (simp only: th) also have "\ \ ?a* (- ?s / ((1 + 1)*?d))+ ?r <= 0" by (simp add: r[of "- (?s / ((1 + 1)*?d))"]) also have "\ \ (1 + 1)*?d * (?a* (- ?s / ((1 + 1)*?d))+ ?r) >= 0" 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 also have "\ \ ?a*?s - (1 + 1)*?d *?r <= 0" using nonzero_mult_divide_cancel_left[OF d'] d order_less_not_sym[OF d''] less_imp_neq[OF d''] d'' - by (simp add: ring_simps diff_divide_distrib del: left_distrib) + by (simp add: algebra_simps diff_divide_distrib del: left_distrib) finally have ?thesis using c d nc nd - apply(simp add: r[of "- (?s / ((1 + 1)*?d))"] msubstle_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm) + apply(simp add: r[of "- (?s / ((1 + 1)*?d))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm) apply (simp only: one_add_one_is_two[symmetric] of_int_add) using d order_less_not_sym[OF d] less_imp_neq[OF d] - by (simp add: ring_simps ) } + by (simp add: field_simps ) } ultimately show ?thesis by blast qed @@ -2519,7 +2519,7 @@ lemma remdps_set[simp]: "set (remdps xs) = set xs" by (induct xs rule: remdps.induct, auto) -lemma simpfm_lin: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})" +lemma simpfm_lin: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" shows "qfree p \ islin (simpfm p)" by (induct p rule: simpfm.induct, auto simp add: conj_lin disj_lin) @@ -2551,7 +2551,7 @@ {fix c t d s assume ctU: "(c,t) \ set ?U" and dsU: "(d,s) \ set ?U" from U_l ctU dsU have norm: "isnpoly c" "isnpoly d" by auto from msubst_I[OF lq norm, of vs x bs t s] msubst_I[OF lq norm(2,1), of vs x bs s t] - have "?I (msubst ?q ((c,t),(d,s))) = ?I (msubst ?q ((d,s),(c,t)))" by (simp add: ring_simps)} + have "?I (msubst ?q ((c,t),(d,s))) = ?I (msubst ?q ((d,s),(c,t)))" by (simp add: field_simps)} hence th0: "\x \ set ?U. \y \ set ?U. ?I (msubst ?q (x, y)) \ ?I (msubst ?q (y, x))" by clarsimp {fix x assume xUp: "x \ set ?Up" then obtain c t d s where ctU: "(c,t) \ set ?U" and dsU: "(d,s) \ set ?U" @@ -2616,7 +2616,7 @@ let ?s = "Itm vs (x # bs) s" let ?t = "Itm vs (x # bs) t" have eq2: "\(x::'a). x + x = (1 + 1) * x" - by (simp add: ring_simps) + by (simp add: field_simps) {assume "?c = 0 \ ?d = 0" with ct have ?D by simp} moreover @@ -2747,12 +2747,12 @@ using lp tnb by (induct p c t rule: msubstpos.induct, auto simp add: msubsteq2_nb msubstltpos_nb msubstlepos_nb) -lemma msubstneg_nb: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})" and lp: "islin p" and tnb: "tmbound0 t" +lemma msubstneg_nb: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" and lp: "islin p" and tnb: "tmbound0 t" shows "bound0 (msubstneg p c t)" using lp tnb by (induct p c t rule: msubstneg.induct, auto simp add: msubsteq2_nb msubstltneg_nb msubstleneg_nb) -lemma msubst2_nb: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})" and lp: "islin p" and tnb: "tmbound0 t" +lemma msubst2_nb: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" and lp: "islin p" and tnb: "tmbound0 t" shows "bound0 (msubst2 p c t)" using lp tnb by (simp add: msubst2_def msubstneg_nb msubstpos_nb conj_nb disj_nb lt_nb simpfm_bound0) @@ -2899,14 +2899,14 @@ by (auto simp add: msubst2_def lt[OF stupid(3)] lt[OF stupid(1)] mult_less_0_iff zero_less_mult_iff) from msubst2[OF lq norm2(1) z(1), of x bs] msubst2[OF lq norm2(2) z(2), of x bs] H - show ?rhs by (simp add: ring_simps) + show ?rhs by (simp add: field_simps) next assume H: ?rhs hence z: "\C (-2, 1) *\<^sub>p b *\<^sub>p d\\<^sub>p\<^bsup>vs\<^esup> \ 0" "\C (-2, 1) *\<^sub>p d *\<^sub>p b\\<^sub>p\<^bsup>vs\<^esup> \ 0" by (auto simp add: msubst2_def lt[OF stupid(4)] lt[OF stupid(2)] mult_less_0_iff zero_less_mult_iff) from msubst2[OF lq norm2(1) z(1), of x bs] msubst2[OF lq norm2(2) z(2), of x bs] H - show ?lhs by (simp add: ring_simps) + show ?lhs by (simp add: field_simps) qed} hence th0: "\x \ set ?U. \y \ set ?U. ?I (?s (x, y)) \ ?I (?s (y, x))" by clarsimp @@ -3156,54 +3156,54 @@ *} "Parametric QE for linear Arithmetic over fields, Version 2" -lemma "\(x::'a::{division_by_zero,linordered_field,number_ring}). y \ -1 \ (y + 1)*x < 0" - apply (frpar type: "'a::{division_by_zero,linordered_field,number_ring}" pars: "y::'a::{division_by_zero,linordered_field,number_ring}") - apply (simp add: ring_simps) +lemma "\(x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). y \ -1 \ (y + 1)*x < 0" + apply (frpar type: "'a::{linordered_field, division_ring_inverse_zero, number_ring}" pars: "y::'a::{linordered_field, division_ring_inverse_zero, number_ring}") + apply (simp add: field_simps) apply (rule spec[where x=y]) - apply (frpar type: "'a::{division_by_zero,linordered_field,number_ring}" pars: "z::'a::{division_by_zero,linordered_field,number_ring}") + apply (frpar type: "'a::{linordered_field, division_ring_inverse_zero, number_ring}" pars: "z::'a::{linordered_field, division_ring_inverse_zero, number_ring}") by simp text{* Collins/Jones Problem *} (* -lemma "\(r::'a::{division_by_zero,linordered_field,number_ring}). 0 < r \ r < 1 \ 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \ (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0" +lemma "\(r::'a::{linordered_field, division_ring_inverse_zero, number_ring}). 0 < r \ r < 1 \ 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \ (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0" proof- - have "(\(r::'a::{division_by_zero,linordered_field,number_ring}). 0 < r \ r < 1 \ 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \ (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \ (\(r::'a::{division_by_zero,linordered_field,number_ring}). 0 < r \ r < 1 \ 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \ 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \ ?rhs") -by (simp add: ring_simps) + have "(\(r::'a::{linordered_field, division_ring_inverse_zero, number_ring}). 0 < r \ r < 1 \ 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \ (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \ (\(r::'a::{linordered_field, division_ring_inverse_zero, number_ring}). 0 < r \ r < 1 \ 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \ 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \ ?rhs") +by (simp add: field_simps) have "?rhs" - 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}") - apply (simp add: ring_simps) + apply (frpar type: "'a::{linordered_field, division_ring_inverse_zero, number_ring}" pars: "a::'a::{linordered_field, division_ring_inverse_zero, number_ring}" "b::'a::{linordered_field, division_ring_inverse_zero, number_ring}") + apply (simp add: field_simps) oops *) (* -lemma "ALL (x::'a::{division_by_zero,linordered_field,number_ring}) y. (1 - t)*x \ (1+t)*y \ (1 - t)*y \ (1+t)*x --> 0 \ y" -apply (frpar type: "'a::{division_by_zero,linordered_field,number_ring}" pars: "t::'a::{division_by_zero,linordered_field,number_ring}") +lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (1 - t)*x \ (1+t)*y \ (1 - t)*y \ (1+t)*x --> 0 \ y" +apply (frpar type: "'a::{linordered_field, division_ring_inverse_zero, number_ring}" pars: "t::'a::{linordered_field, division_ring_inverse_zero, number_ring}") oops *) -lemma "\(x::'a::{division_by_zero,linordered_field,number_ring}). y \ -1 \ (y + 1)*x < 0" - apply (frpar2 type: "'a::{division_by_zero,linordered_field,number_ring}" pars: "y::'a::{division_by_zero,linordered_field,number_ring}") - apply (simp add: ring_simps) +lemma "\(x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). y \ -1 \ (y + 1)*x < 0" + apply (frpar2 type: "'a::{linordered_field, division_ring_inverse_zero, number_ring}" pars: "y::'a::{linordered_field, division_ring_inverse_zero, number_ring}") + apply (simp add: field_simps) apply (rule spec[where x=y]) - apply (frpar2 type: "'a::{division_by_zero,linordered_field,number_ring}" pars: "z::'a::{division_by_zero,linordered_field,number_ring}") + apply (frpar2 type: "'a::{linordered_field, division_ring_inverse_zero, number_ring}" pars: "z::'a::{linordered_field, division_ring_inverse_zero, number_ring}") by simp text{* Collins/Jones Problem *} (* -lemma "\(r::'a::{division_by_zero,linordered_field,number_ring}). 0 < r \ r < 1 \ 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \ (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0" +lemma "\(r::'a::{linordered_field, division_ring_inverse_zero, number_ring}). 0 < r \ r < 1 \ 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \ (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0" proof- - have "(\(r::'a::{division_by_zero,linordered_field,number_ring}). 0 < r \ r < 1 \ 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \ (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \ (\(r::'a::{division_by_zero,linordered_field,number_ring}). 0 < r \ r < 1 \ 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \ 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \ ?rhs") -by (simp add: ring_simps) + have "(\(r::'a::{linordered_field, division_ring_inverse_zero, number_ring}). 0 < r \ r < 1 \ 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \ (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \ (\(r::'a::{linordered_field, division_ring_inverse_zero, number_ring}). 0 < r \ r < 1 \ 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \ 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \ ?rhs") +by (simp add: field_simps) have "?rhs" - 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}") + apply (frpar2 type: "'a::{linordered_field, division_ring_inverse_zero, number_ring}" pars: "a::'a::{linordered_field, division_ring_inverse_zero, number_ring}" "b::'a::{linordered_field, division_ring_inverse_zero, number_ring}") apply simp oops *) (* -lemma "ALL (x::'a::{division_by_zero,linordered_field,number_ring}) y. (1 - t)*x \ (1+t)*y \ (1 - t)*y \ (1+t)*x --> 0 \ y" -apply (frpar2 type: "'a::{division_by_zero,linordered_field,number_ring}" pars: "t::'a::{division_by_zero,linordered_field,number_ring}") +lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (1 - t)*x \ (1+t)*y \ (1 - t)*y \ (1+t)*x --> 0 \ y" +apply (frpar2 type: "'a::{linordered_field, division_ring_inverse_zero, number_ring}" pars: "t::'a::{linordered_field, division_ring_inverse_zero, number_ring}") apply (simp add: field_simps linorder_neq_iff[symmetric]) apply ferrack oops diff -r 0ca616bc6c6f -r 89c54f51f55a src/HOL/Fields.thy --- a/src/HOL/Fields.thy Mon Apr 26 11:34:15 2010 +0200 +++ b/src/HOL/Fields.thy Mon Apr 26 11:34:15 2010 +0200 @@ -13,20 +13,6 @@ imports Rings begin -text{* Lemmas @{text field_simps} multiply with denominators in (in)equations -if they can be proved to be non-zero (for equations) or positive/negative -(for inequations). Can be too aggressive and is therefore separate from the -more benign @{text algebra_simps}. *} - -ML {* -structure Field_Simps = Named_Thms( - val name = "field_simps" - val description = "algebra simplification rules for fields" -) -*} - -setup Field_Simps.setup - class field = comm_ring_1 + inverse + assumes field_inverse: "a \ 0 \ inverse a * a = 1" assumes field_divide_inverse: "a / b = a * inverse b" @@ -110,51 +96,45 @@ "\b \ 0; c \ 0\ \ (a * c) / (c * b) = a / b" using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: mult_ac) -lemma add_divide_eq_iff: +lemma add_divide_eq_iff [field_simps]: "z \ 0 \ x + y / z = (z * x + y) / z" by (simp add: add_divide_distrib) -lemma divide_add_eq_iff: +lemma divide_add_eq_iff [field_simps]: "z \ 0 \ x / z + y = (x + z * y) / z" by (simp add: add_divide_distrib) -lemma diff_divide_eq_iff: +lemma diff_divide_eq_iff [field_simps]: "z \ 0 \ x - y / z = (z * x - y) / z" by (simp add: diff_divide_distrib) -lemma divide_diff_eq_iff: +lemma divide_diff_eq_iff [field_simps]: "z \ 0 \ x / z - y = (x - z * y) / z" by (simp add: diff_divide_distrib) -lemmas field_eq_simps [field_simps, no_atp] = algebra_simps - (* pull / out*) - add_divide_eq_iff divide_add_eq_iff - diff_divide_eq_iff divide_diff_eq_iff - (* multiply eqn *) - nonzero_eq_divide_eq nonzero_divide_eq_eq - times_divide_eq_left times_divide_eq_right - -text{*An example:*} -lemma "\a\b; c\d; e\f\ \ ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) = 1" -apply(subgoal_tac "(c-d)*(e-f)*(a-b) \ 0") - apply(simp add:field_eq_simps) -apply(simp) -done - lemma diff_frac_eq: "y \ 0 \ z \ 0 \ x / y - w / z = (x * z - w * y) / (y * z)" - by (simp add: field_eq_simps times_divide_eq) + by (simp add: field_simps) lemma frac_eq_eq: "y \ 0 \ z \ 0 \ (x / y = w / z) = (x * z = w * y)" - by (simp add: field_eq_simps times_divide_eq) + by (simp add: field_simps) + +end + +class field_inverse_zero = field + + assumes field_inverse_zero: "inverse 0 = 0" +begin + +subclass division_ring_inverse_zero proof +qed (fact field_inverse_zero) end text{*This version builds in division by zero while also re-orienting the right-hand side.*} lemma inverse_mult_distrib [simp]: - "inverse(a*b) = inverse(a) * inverse(b::'a::{field,division_by_zero})" + "inverse(a*b) = inverse(a) * inverse(b::'a::{field,division_ring_inverse_zero})" proof cases assume "a \ 0 & b \ 0" thus ?thesis by (simp add: nonzero_inverse_mult_distrib mult_ac) @@ -164,7 +144,7 @@ qed lemma inverse_divide [simp]: - "inverse (a/b) = b / (a::'a::{field,division_by_zero})" + "inverse (a/b) = b / (a::'a::{field,division_ring_inverse_zero})" by (simp add: divide_inverse mult_commute) @@ -175,85 +155,85 @@ because the latter are covered by a simproc. *} lemma mult_divide_mult_cancel_left: - "c\0 ==> (c*a) / (c*b) = a / (b::'a::{field,division_by_zero})" + "c\0 ==> (c*a) / (c*b) = a / (b::'a::{field,division_ring_inverse_zero})" apply (cases "b = 0") apply simp_all done lemma mult_divide_mult_cancel_right: - "c\0 ==> (a*c) / (b*c) = a / (b::'a::{field,division_by_zero})" + "c\0 ==> (a*c) / (b*c) = a / (b::'a::{field,division_ring_inverse_zero})" apply (cases "b = 0") apply simp_all done lemma divide_divide_eq_right [simp,no_atp]: - "a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})" + "a / (b/c) = (a*c) / (b::'a::{field,division_ring_inverse_zero})" by (simp add: divide_inverse mult_ac) lemma divide_divide_eq_left [simp,no_atp]: - "(a / b) / (c::'a::{field,division_by_zero}) = a / (b*c)" + "(a / b) / (c::'a::{field,division_ring_inverse_zero}) = a / (b*c)" by (simp add: divide_inverse mult_assoc) text {*Special Cancellation Simprules for Division*} lemma mult_divide_mult_cancel_left_if[simp,no_atp]: -fixes c :: "'a :: {field,division_by_zero}" +fixes c :: "'a :: {field,division_ring_inverse_zero}" shows "(c*a) / (c*b) = (if c=0 then 0 else a/b)" by (simp add: mult_divide_mult_cancel_left) text {* Division and Unary Minus *} -lemma minus_divide_right: "- (a/b) = a / -(b::'a::{field,division_by_zero})" +lemma minus_divide_right: "- (a/b) = a / -(b::'a::{field,division_ring_inverse_zero})" by (simp add: divide_inverse) lemma divide_minus_right [simp, no_atp]: - "a / -(b::'a::{field,division_by_zero}) = -(a / b)" + "a / -(b::'a::{field,division_ring_inverse_zero}) = -(a / b)" by (simp add: divide_inverse) lemma minus_divide_divide: - "(-a)/(-b) = a / (b::'a::{field,division_by_zero})" + "(-a)/(-b) = a / (b::'a::{field,division_ring_inverse_zero})" apply (cases "b=0", simp) apply (simp add: nonzero_minus_divide_divide) done lemma eq_divide_eq: - "((a::'a::{field,division_by_zero}) = b/c) = (if c\0 then a*c = b else a=0)" + "((a::'a::{field,division_ring_inverse_zero}) = b/c) = (if c\0 then a*c = b else a=0)" by (simp add: nonzero_eq_divide_eq) lemma divide_eq_eq: - "(b/c = (a::'a::{field,division_by_zero})) = (if c\0 then b = a*c else a=0)" + "(b/c = (a::'a::{field,division_ring_inverse_zero})) = (if c\0 then b = a*c else a=0)" by (force simp add: nonzero_divide_eq_eq) lemma inverse_eq_1_iff [simp]: - "(inverse x = 1) = (x = (1::'a::{field,division_by_zero}))" + "(inverse x = 1) = (x = (1::'a::{field,division_ring_inverse_zero}))" by (insert inverse_eq_iff_eq [of x 1], simp) lemma divide_eq_0_iff [simp,no_atp]: - "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))" + "(a/b = 0) = (a=0 | b=(0::'a::{field,division_ring_inverse_zero}))" by (simp add: divide_inverse) lemma divide_cancel_right [simp,no_atp]: - "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))" + "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_ring_inverse_zero}))" apply (cases "c=0", simp) apply (simp add: divide_inverse) done lemma divide_cancel_left [simp,no_atp]: - "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))" + "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_ring_inverse_zero}))" apply (cases "c=0", simp) apply (simp add: divide_inverse) done lemma divide_eq_1_iff [simp,no_atp]: - "(a/b = 1) = (b \ 0 & a = (b::'a::{field,division_by_zero}))" + "(a/b = 1) = (b \ 0 & a = (b::'a::{field,division_ring_inverse_zero}))" apply (cases "b=0", simp) apply (simp add: right_inverse_eq) done lemma one_eq_divide_iff [simp,no_atp]: - "(1 = a/b) = (b \ 0 & a = (b::'a::{field,division_by_zero}))" + "(1 = a/b) = (b \ 0 & a = (b::'a::{field,division_ring_inverse_zero}))" by (simp add: eq_commute [of 1]) @@ -405,7 +385,7 @@ "a < 0 \ b < 0 \ inverse a \ inverse b \ b \ a" by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg) -lemma pos_le_divide_eq: "0 < c ==> (a \ b/c) = (a*c \ b)" +lemma pos_le_divide_eq [field_simps]: "0 < c ==> (a \ b/c) = (a*c \ b)" proof - assume less: "0 b/c) = (a*c \ (b/c)*c)" @@ -415,7 +395,7 @@ finally show ?thesis . qed -lemma neg_le_divide_eq: "c < 0 ==> (a \ b/c) = (b \ a*c)" +lemma neg_le_divide_eq [field_simps]: "c < 0 ==> (a \ b/c) = (b \ a*c)" proof - assume less: "c<0" hence "(a \ b/c) = ((b/c)*c \ a*c)" @@ -425,7 +405,7 @@ finally show ?thesis . qed -lemma pos_less_divide_eq: +lemma pos_less_divide_eq [field_simps]: "0 < c ==> (a < b/c) = (a*c < b)" proof - assume less: "0 (a < b/c) = (b < a*c)" proof - assume less: "c<0" @@ -447,7 +427,7 @@ finally show ?thesis . qed -lemma pos_divide_less_eq: +lemma pos_divide_less_eq [field_simps]: "0 < c ==> (b/c < a) = (b < a*c)" proof - assume less: "0 (b/c < a) = (a*c < b)" proof - assume less: "c<0" @@ -469,7 +449,7 @@ finally show ?thesis . qed -lemma pos_divide_le_eq: "0 < c ==> (b/c \ a) = (b \ a*c)" +lemma pos_divide_le_eq [field_simps]: "0 < c ==> (b/c \ a) = (b \ a*c)" proof - assume less: "0 a) = ((b/c)*c \ a*c)" @@ -479,7 +459,7 @@ finally show ?thesis . qed -lemma neg_divide_le_eq: "c < 0 ==> (b/c \ a) = (a*c \ b)" +lemma neg_divide_le_eq [field_simps]: "c < 0 ==> (b/c \ a) = (a*c \ b)" proof - assume less: "c<0" hence "(b/c \ a) = (a*c \ (b/c)*c)" @@ -489,19 +469,15 @@ finally show ?thesis . qed -lemmas [field_simps, no_atp] = - (* multiply ineqn *) - pos_divide_less_eq neg_divide_less_eq - pos_less_divide_eq neg_less_divide_eq - pos_divide_le_eq neg_divide_le_eq - pos_le_divide_eq neg_le_divide_eq - text{* Lemmas @{text sign_simps} is a first attempt to automate proofs of positivity/negativity needed for @{text field_simps}. Have not added @{text sign_simps} to @{text field_simps} because the former can lead to case explosions. *} -lemmas sign_simps[no_atp] = group_simps +lemmas sign_simps [no_atp] = algebra_simps + zero_less_mult_iff mult_less_0_iff + +lemmas (in -) sign_simps [no_atp] = algebra_simps zero_less_mult_iff mult_less_0_iff (* Only works once linear arithmetic is installed: @@ -667,37 +643,46 @@ end +class linordered_field_inverse_zero = linordered_field + + assumes linordered_field_inverse_zero: "inverse 0 = 0" +begin + +subclass field_inverse_zero proof +qed (fact linordered_field_inverse_zero) + +end + lemma le_divide_eq: "(a \ b/c) = (if 0 < c then a*c \ b else if c < 0 then b \ a*c - else a \ (0::'a::{linordered_field,division_by_zero}))" + else a \ (0::'a::{linordered_field,division_ring_inverse_zero}))" apply (cases "c=0", simp) apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff) done lemma inverse_positive_iff_positive [simp]: - "(0 < inverse a) = (0 < (a::'a::{linordered_field,division_by_zero}))" + "(0 < inverse a) = (0 < (a::'a::{linordered_field,division_ring_inverse_zero}))" apply (cases "a = 0", simp) apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive) done lemma inverse_negative_iff_negative [simp]: - "(inverse a < 0) = (a < (0::'a::{linordered_field,division_by_zero}))" + "(inverse a < 0) = (a < (0::'a::{linordered_field,division_ring_inverse_zero}))" apply (cases "a = 0", simp) apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative) done lemma inverse_nonnegative_iff_nonnegative [simp]: - "(0 \ inverse a) = (0 \ (a::'a::{linordered_field,division_by_zero}))" + "(0 \ inverse a) = (0 \ (a::'a::{linordered_field,division_ring_inverse_zero}))" by (simp add: linorder_not_less [symmetric]) lemma inverse_nonpositive_iff_nonpositive [simp]: - "(inverse a \ 0) = (a \ (0::'a::{linordered_field,division_by_zero}))" + "(inverse a \ 0) = (a \ (0::'a::{linordered_field,division_ring_inverse_zero}))" by (simp add: linorder_not_less [symmetric]) lemma one_less_inverse_iff: - "(1 < inverse x) = (0 < x & x < (1::'a::{linordered_field,division_by_zero}))" + "(1 < inverse x) = (0 < x & x < (1::'a::{linordered_field,division_ring_inverse_zero}))" proof cases assume "0 < x" with inverse_less_iff_less [OF zero_less_one, of x] @@ -715,22 +700,22 @@ qed lemma one_le_inverse_iff: - "(1 \ inverse x) = (0 < x & x \ (1::'a::{linordered_field,division_by_zero}))" + "(1 \ inverse x) = (0 < x & x \ (1::'a::{linordered_field,division_ring_inverse_zero}))" by (force simp add: order_le_less one_less_inverse_iff) lemma inverse_less_1_iff: - "(inverse x < 1) = (x \ 0 | 1 < (x::'a::{linordered_field,division_by_zero}))" + "(inverse x < 1) = (x \ 0 | 1 < (x::'a::{linordered_field,division_ring_inverse_zero}))" by (simp add: linorder_not_le [symmetric] one_le_inverse_iff) lemma inverse_le_1_iff: - "(inverse x \ 1) = (x \ 0 | 1 \ (x::'a::{linordered_field,division_by_zero}))" + "(inverse x \ 1) = (x \ 0 | 1 \ (x::'a::{linordered_field,division_ring_inverse_zero}))" by (simp add: linorder_not_less [symmetric] one_less_inverse_iff) lemma divide_le_eq: "(b/c \ a) = (if 0 < c then b \ a*c else if c < 0 then a*c \ b - else 0 \