# HG changeset patch # User haftmann # Date 1272289070 -7200 # Node ID d323e7773aa84dbd5902cf0200921814660771f1 # Parent bc7982c54e377f9de13d4ebc28ebd64d3958ae09 use new classes (linordered_)field_inverse_zero diff -r bc7982c54e37 -r d323e7773aa8 src/HOL/Big_Operators.thy --- a/src/HOL/Big_Operators.thy Mon Apr 26 11:34:19 2010 +0200 +++ b/src/HOL/Big_Operators.thy Mon Apr 26 15:37:50 2010 +0200 @@ -1033,12 +1033,12 @@ by (erule finite_induct) (auto simp add: insert_Diff_if) lemma setprod_inversef: - fixes f :: "'b \ 'a::{field,division_ring_inverse_zero}" + fixes f :: "'b \ 'a::field_inverse_zero" shows "finite A ==> setprod (inverse \ f) A = inverse (setprod f A)" by (erule finite_induct) auto lemma setprod_dividef: - fixes f :: "'b \ 'a::{field,division_ring_inverse_zero}" + fixes f :: "'b \ 'a::field_inverse_zero" shows "finite A ==> setprod (%x. f x / g x) A = setprod f A / setprod g A" apply (subgoal_tac diff -r bc7982c54e37 -r d323e7773aa8 src/HOL/Complex.thy --- a/src/HOL/Complex.thy Mon Apr 26 11:34:19 2010 +0200 +++ b/src/HOL/Complex.thy Mon Apr 26 15:37:50 2010 +0200 @@ -99,7 +99,7 @@ subsection {* Multiplication and Division *} -instantiation complex :: "{field, division_ring_inverse_zero}" +instantiation complex :: field_inverse_zero begin definition diff -r bc7982c54e37 -r d323e7773aa8 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Mon Apr 26 11:34:19 2010 +0200 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Mon Apr 26 15:37:50 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_ring_inverse_zero,field} list \ 'a list \ tm \ 'a" +consts Itm :: "'a::{field_char_0, field_inverse_zero} list \ 'a list \ tm \ 'a" primrec "Itm vs bs (CP c) = (Ipoly vs c)" "Itm vs bs (Bound n) = bs!n" @@ -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_ring_inverse_zero, field})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 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_ring_inverse_zero, field})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 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_ring_inverse_zero, field})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 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_ring_inverse_zero, field})" - shows "polynate t = 0\<^sub>p \ Ipoly bs t = (0::'a::{ring_char_0,division_ring_inverse_zero, field})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + shows "polynate t = 0\<^sub>p \ Ipoly bs t = (0::'a::{field_char_0, field_inverse_zero})" 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_ring_inverse_zero, field})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "allpolys isnpoly (simptm p)" by (induct p rule: simptm.induct, auto simp add: Let_def) @@ -387,7 +387,7 @@ qed lemma split0_nb0: - assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero, field})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 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_ring_inverse_zero, field})" +lemma split0_nb0'[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 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_ring_inverse_zero, field})" +lemma isnpoly_fst_split0: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 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_ring_inverse_zero,linordered_field} list \ 'a list \ fm \ bool" +consts Ifm ::"'a::{linordered_field_inverse_zero} 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_ring_inverse_zero,field})" +lemma simplt_islin[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 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_ring_inverse_zero,field})" +lemma simple_islin[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 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_ring_inverse_zero,field})" +lemma simpeq_islin[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 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_ring_inverse_zero,field})" +lemma simpneq_islin[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 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_ring_inverse_zero,field})" +lemma split0_npoly: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 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_ring_inverse_zero,field})" +lemma simplt_nb[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 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_ring_inverse_zero,field})" +lemma simple_nb[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 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_ring_inverse_zero,field})" +lemma simpeq_nb[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 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_ring_inverse_zero,field})" +lemma simpneq_nb[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 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_ring_inverse_zero,field})" +lemma simpfm_bound0: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 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_ring_inverse_zero,field})" +lemma assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "qfree p \ islin (simpfm p)" apply (induct p rule: simpfm.induct) apply (simp_all add: conj_lin disj_lin) @@ -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_ring_inverse_zero,field})" +lemma simpfm_lin: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "qfree p \ islin (simpfm p)" by (induct p rule: simpfm.induct, auto simp add: conj_lin disj_lin) @@ -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_ring_inverse_zero,field})" and lp: "islin p" and tnb: "tmbound0 t" +lemma msubstneg_nb: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 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_ring_inverse_zero,field})" and lp: "islin p" and tnb: "tmbound0 t" +lemma msubst2_nb: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 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) @@ -3156,54 +3156,54 @@ *} "Parametric QE for linear Arithmetic over fields, Version 2" -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}") +lemma "\(x::'a::{linordered_field_inverse_zero, number_ring}). y \ -1 \ (y + 1)*x < 0" + apply (frpar type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "y::'a::{linordered_field_inverse_zero, number_ring}") apply (simp add: field_simps) apply (rule spec[where x=y]) - apply (frpar type: "'a::{linordered_field, division_ring_inverse_zero, number_ring}" pars: "z::'a::{linordered_field, division_ring_inverse_zero, number_ring}") + apply (frpar type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "z::'a::{linordered_field_inverse_zero, number_ring}") by simp text{* Collins/Jones Problem *} (* -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" +lemma "\(r::'a::{linordered_field_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::{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") + have "(\(r::'a::{linordered_field_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_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::{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 (frpar type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "a::'a::{linordered_field_inverse_zero, number_ring}" "b::'a::{linordered_field_inverse_zero, number_ring}") apply (simp add: field_simps) oops *) (* -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}") +lemma "ALL (x::'a::{linordered_field_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_inverse_zero, number_ring}" pars: "t::'a::{linordered_field_inverse_zero, number_ring}") oops *) -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}") +lemma "\(x::'a::{linordered_field_inverse_zero, number_ring}). y \ -1 \ (y + 1)*x < 0" + apply (frpar2 type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "y::'a::{linordered_field_inverse_zero, number_ring}") apply (simp add: field_simps) apply (rule spec[where x=y]) - apply (frpar2 type: "'a::{linordered_field, division_ring_inverse_zero, number_ring}" pars: "z::'a::{linordered_field, division_ring_inverse_zero, number_ring}") + apply (frpar2 type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "z::'a::{linordered_field_inverse_zero, number_ring}") by simp text{* Collins/Jones Problem *} (* -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" +lemma "\(r::'a::{linordered_field_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::{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") + have "(\(r::'a::{linordered_field_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_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::{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 (frpar2 type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "a::'a::{linordered_field_inverse_zero, number_ring}" "b::'a::{linordered_field_inverse_zero, number_ring}") apply simp oops *) (* -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}") +lemma "ALL (x::'a::{linordered_field_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_inverse_zero, number_ring}" pars: "t::'a::{linordered_field_inverse_zero, number_ring}") apply (simp add: field_simps linorder_neq_iff[symmetric]) apply ferrack oops diff -r bc7982c54e37 -r d323e7773aa8 src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Mon Apr 26 11:34:19 2010 +0200 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Mon Apr 26 15:37:50 2010 +0200 @@ -230,7 +230,7 @@ subsection{* Semantics of the polynomial representation *} -consts Ipoly :: "'a list \ poly \ 'a::{ring_char_0,power,division_ring_inverse_zero,field}" +consts Ipoly :: "'a list \ poly \ 'a::{field_char_0, field_inverse_zero, power}" primrec "Ipoly bs (C c) = INum c" "Ipoly bs (Bound n) = bs!n" @@ -241,7 +241,7 @@ "Ipoly bs (Pw t n) = (Ipoly bs t) ^ n" "Ipoly bs (CN c n p) = (Ipoly bs c) + (bs!n)*(Ipoly bs p)" abbreviation - Ipoly_syntax :: "poly \ 'a list \'a::{ring_char_0,power,division_ring_inverse_zero,field}" ("\_\\<^sub>p\<^bsup>_\<^esup>") + Ipoly_syntax :: "poly \ 'a list \'a::{field_char_0, field_inverse_zero, power}" ("\_\\<^sub>p\<^bsup>_\<^esup>") where "\p\\<^sub>p\<^bsup>bs\<^esup> \ Ipoly bs p" lemma Ipoly_CInt: "Ipoly bs (C (i,1)) = of_int i" @@ -394,7 +394,7 @@ qed simp_all lemma polymul_properties: - assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and m: "m \ min n0 n1" shows "isnpolyh (p *\<^sub>p q) (min n0 n1)" and "(p *\<^sub>p q = 0\<^sub>p) = (p = 0\<^sub>p \ q = 0\<^sub>p)" @@ -568,19 +568,19 @@ by(induct p q rule: polymul.induct, auto simp add: field_simps) lemma polymul_normh: - assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "\isnpolyh p n0 ; isnpolyh q n1\ \ isnpolyh (p *\<^sub>p q) (min n0 n1)" using polymul_properties(1) by blast lemma polymul_eq0_iff: - assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "\ isnpolyh p n0 ; isnpolyh q n1\ \ (p *\<^sub>p q = 0\<^sub>p) = (p = 0\<^sub>p \ q = 0\<^sub>p) " using polymul_properties(2) by blast lemma polymul_degreen: - assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "\ isnpolyh p n0 ; isnpolyh q n1 ; m \ min n0 n1\ \ degreen (p *\<^sub>p q) m = (if (p = 0\<^sub>p \ q = 0\<^sub>p) then 0 else degreen p m + degreen q m)" using polymul_properties(3) by blast lemma polymul_norm: - assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "\ isnpoly p; isnpoly q\ \ isnpoly (polymul (p,q))" using polymul_normh[of "p" "0" "q" "0"] isnpoly_def by simp @@ -591,7 +591,7 @@ by (induct p arbitrary: n0, auto) lemma monic_eqI: assumes np: "isnpolyh p n0" - shows "INum (headconst p) * Ipoly bs (fst (monic p)) = (Ipoly bs p ::'a::{ring_char_0,power,division_ring_inverse_zero,field})" + shows "INum (headconst p) * Ipoly bs (fst (monic p)) = (Ipoly bs p ::'a::{field_char_0, field_inverse_zero, power})" unfolding monic_def Let_def proof(cases "headconst p = 0\<^sub>N", simp_all add: headconst_zero[OF np]) let ?h = "headconst p" @@ -629,13 +629,13 @@ lemma polysub_norm: "\ isnpoly p; isnpoly q\ \ isnpoly (polysub(p,q))" using polyadd_norm polyneg_norm by (simp add: polysub_def) -lemma polysub_same_0[simp]: assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})" +lemma polysub_same_0[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "isnpolyh p n0 \ polysub (p, p) = 0\<^sub>p" unfolding polysub_def split_def fst_conv snd_conv by (induct p arbitrary: n0,auto simp add: Let_def Nsub0[simplified Nsub_def]) lemma polysub_0: - assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "\ isnpolyh p n0 ; isnpolyh q n1\ \ (p -\<^sub>p q = 0\<^sub>p) = (p = q)" unfolding polysub_def split_def fst_conv snd_conv apply (induct p q arbitrary: n0 n1 rule:polyadd.induct, simp_all add: Nsub0[simplified Nsub_def]) @@ -657,7 +657,7 @@ done text{* polypow is a power function and preserves normal forms *} -lemma polypow[simp]: "Ipoly bs (polypow n p) = ((Ipoly bs p :: 'a::{field, division_ring_inverse_zero, ring_char_0})) ^ n" +lemma polypow[simp]: "Ipoly bs (polypow n p) = ((Ipoly bs p :: 'a::{field_char_0, field_inverse_zero})) ^ n" proof(induct n rule: polypow.induct) case 1 thus ?case by simp next @@ -688,7 +688,7 @@ qed lemma polypow_normh: - assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "isnpolyh p n \ isnpolyh (polypow k p) n" proof (induct k arbitrary: n rule: polypow.induct) case (2 k n) @@ -701,17 +701,17 @@ qed auto lemma polypow_norm: - assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "isnpoly p \ isnpoly (polypow k p)" by (simp add: polypow_normh isnpoly_def) text{* Finally the whole normalization*} -lemma polynate[simp]: "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field, division_ring_inverse_zero, ring_char_0})" +lemma polynate[simp]: "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0, field_inverse_zero})" by (induct p rule:polynate.induct, auto) lemma polynate_norm[simp]: - assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "isnpoly (polynate p)" by (induct p rule: polynate.induct, simp_all add: polyadd_norm polymul_norm polysub_norm polyneg_norm polypow_norm) (simp_all add: isnpoly_def) @@ -736,14 +736,14 @@ shows "isnpolyh (funpow k f p) n" using f np by (induct k arbitrary: p, auto) -lemma funpow_shift1: "(Ipoly bs (funpow n shift1 p) :: 'a :: {field, division_ring_inverse_zero, ring_char_0}) = Ipoly bs (Mul (Pw (Bound 0) n) p)" +lemma funpow_shift1: "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) = Ipoly bs (Mul (Pw (Bound 0) n) p)" by (induct n arbitrary: p, simp_all add: shift1_isnpoly shift1 power_Suc ) lemma shift1_isnpolyh: "isnpolyh p n0 \ p\ 0\<^sub>p \ isnpolyh (shift1 p) 0" using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by (simp add: shift1_def) lemma funpow_shift1_1: - "(Ipoly bs (funpow n shift1 p) :: 'a :: {field, division_ring_inverse_zero, ring_char_0}) = Ipoly bs (funpow n shift1 1\<^sub>p *\<^sub>p p)" + "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) = Ipoly bs (funpow n shift1 1\<^sub>p *\<^sub>p p)" by (simp add: funpow_shift1) lemma poly_cmul[simp]: "Ipoly bs (poly_cmul c p) = Ipoly bs (Mul (C c) p)" @@ -751,7 +751,7 @@ lemma behead: assumes np: "isnpolyh p n" - shows "Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = (Ipoly bs p :: 'a :: {field, division_ring_inverse_zero, ring_char_0})" + shows "Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = (Ipoly bs p :: 'a :: {field_char_0, field_inverse_zero})" using np proof (induct p arbitrary: n rule: behead.induct) case (1 c p n) hence pn: "isnpolyh p n" by simp @@ -981,7 +981,7 @@ by (simp add: head_eq_headn0) lemma isnpolyh_zero_iff: - assumes nq: "isnpolyh p n0" and eq :"\bs. wf_bs bs p \ \p\\<^sub>p\<^bsup>bs\<^esup> = (0::'a::{ring_char_0,power,division_ring_inverse_zero,field})" + assumes nq: "isnpolyh p n0" and eq :"\bs. wf_bs bs p \ \p\\<^sub>p\<^bsup>bs\<^esup> = (0::'a::{field_char_0, field_inverse_zero, power})" shows "p = 0\<^sub>p" using nq eq proof (induct "maxindex p" arbitrary: p n0 rule: less_induct) @@ -1033,7 +1033,7 @@ lemma isnpolyh_unique: assumes np:"isnpolyh p n0" and nq: "isnpolyh q n1" - shows "(\bs. \p\\<^sub>p\<^bsup>bs\<^esup> = (\q\\<^sub>p\<^bsup>bs\<^esup> :: 'a::{ring_char_0,power,division_ring_inverse_zero,field})) \ p = q" + shows "(\bs. \p\\<^sub>p\<^bsup>bs\<^esup> = (\q\\<^sub>p\<^bsup>bs\<^esup> :: 'a::{field_char_0, field_inverse_zero, power})) \ p = q" proof(auto) assume H: "\bs. (\p\\<^sub>p\<^bsup>bs\<^esup> ::'a)= \q\\<^sub>p\<^bsup>bs\<^esup>" hence "\bs.\p -\<^sub>p q\\<^sub>p\<^bsup>bs\<^esup>= (0::'a)" by simp @@ -1046,50 +1046,50 @@ text{* consequenses of unicity on the algorithms for polynomial normalization *} -lemma polyadd_commute: assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})" +lemma polyadd_commute: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" and np: "isnpolyh p n0" and nq: "isnpolyh q n1" shows "p +\<^sub>p q = q +\<^sub>p p" using isnpolyh_unique[OF polyadd_normh[OF np nq] polyadd_normh[OF nq np]] by simp lemma zero_normh: "isnpolyh 0\<^sub>p n" by simp lemma one_normh: "isnpolyh 1\<^sub>p n" by simp lemma polyadd_0[simp]: - assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" and np: "isnpolyh p n0" shows "p +\<^sub>p 0\<^sub>p = p" and "0\<^sub>p +\<^sub>p p = p" using isnpolyh_unique[OF polyadd_normh[OF np zero_normh] np] isnpolyh_unique[OF polyadd_normh[OF zero_normh np] np] by simp_all lemma polymul_1[simp]: - assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" and np: "isnpolyh p n0" shows "p *\<^sub>p 1\<^sub>p = p" and "1\<^sub>p *\<^sub>p p = p" using isnpolyh_unique[OF polymul_normh[OF np one_normh] np] isnpolyh_unique[OF polymul_normh[OF one_normh np] np] by simp_all lemma polymul_0[simp]: - assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" and np: "isnpolyh p n0" shows "p *\<^sub>p 0\<^sub>p = 0\<^sub>p" and "0\<^sub>p *\<^sub>p p = 0\<^sub>p" using isnpolyh_unique[OF polymul_normh[OF np zero_normh] zero_normh] isnpolyh_unique[OF polymul_normh[OF zero_normh np] zero_normh] by simp_all lemma polymul_commute: - assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" and np:"isnpolyh p n0" and nq: "isnpolyh q n1" shows "p *\<^sub>p q = q *\<^sub>p p" -using isnpolyh_unique[OF polymul_normh[OF np nq] polymul_normh[OF nq np], where ?'a = "'a\{ring_char_0,power,division_ring_inverse_zero,field}"] by simp +using isnpolyh_unique[OF polymul_normh[OF np nq] polymul_normh[OF nq np], where ?'a = "'a\{field_char_0, field_inverse_zero, power}"] by simp declare polyneg_polyneg[simp] lemma isnpolyh_polynate_id[simp]: - assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" and np:"isnpolyh p n0" shows "polynate p = p" - using isnpolyh_unique[where ?'a= "'a::{field, division_ring_inverse_zero, ring_char_0}", OF polynate_norm[of p, unfolded isnpoly_def] np] polynate[where ?'a = "'a::{field, division_ring_inverse_zero, ring_char_0}"] by simp + using isnpolyh_unique[where ?'a= "'a::{field_char_0, field_inverse_zero}", OF polynate_norm[of p, unfolded isnpoly_def] np] polynate[where ?'a = "'a::{field_char_0, field_inverse_zero}"] by simp lemma polynate_idempotent[simp]: - assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "polynate (polynate p) = polynate p" using isnpolyh_polynate_id[OF polynate_norm[of p, unfolded isnpoly_def]] . lemma poly_nate_polypoly': "poly_nate bs p = polypoly' bs (polynate p)" unfolding poly_nate_def polypoly'_def .. -lemma poly_nate_poly: shows "poly (poly_nate bs p) = (\x:: 'a ::{field, division_ring_inverse_zero, ring_char_0}. \p\\<^sub>p\<^bsup>x # bs\<^esup>)" +lemma poly_nate_poly: shows "poly (poly_nate bs p) = (\x:: 'a ::{field_char_0, field_inverse_zero}. \p\\<^sub>p\<^bsup>x # bs\<^esup>)" using polypoly'_poly[OF polynate_norm[unfolded isnpoly_def], symmetric, of bs p] unfolding poly_nate_polypoly' by (auto intro: ext) @@ -1116,7 +1116,7 @@ qed lemma degree_polysub_samehead: - assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and h: "head p = head q" and d: "degree p = degree q" shows "degree (p -\<^sub>p q) < degree p \ (p -\<^sub>p q = 0\<^sub>p)" @@ -1226,7 +1226,7 @@ done lemma polymul_head_polyeq: - assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "\isnpolyh p n0; isnpolyh q n1 ; p \ 0\<^sub>p ; q \ 0\<^sub>p \ \ head (p *\<^sub>p q) = head p *\<^sub>p head q" proof (induct p q arbitrary: n0 n1 rule: polymul.induct) case (2 a b c' n' p' n0 n1) @@ -1300,7 +1300,7 @@ by (induct p arbitrary: n0 rule: polyneg.induct, auto) lemma degree_polymul: - assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" and np: "isnpolyh p n0" and nq: "isnpolyh q n1" shows "degree (p *\<^sub>p q) \ degree p + degree q" using polymul_degreen[OF np nq, where m="0"] degree_eq_degreen0 by simp @@ -1344,7 +1344,7 @@ qed lemma polydivide_aux_properties: - assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" and np: "isnpolyh p n0" and ns: "isnpolyh s n1" and ap: "head p = a" and ndp: "degree p = n" and pnz: "p \ 0\<^sub>p" shows "polydivide_aux_dom (a,n,p,k,s) \ @@ -1415,19 +1415,19 @@ from polyadd_normh[OF polymul_normh[OF np polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]] nr'] have nqr': "isnpolyh (p *\<^sub>p (?akk' *\<^sub>p ?xdn +\<^sub>p q) +\<^sub>p r) 0" by simp - from asp have "\ (bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs (a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p')) = + from asp have "\ (bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p')) = Ipoly bs (p *\<^sub>p q +\<^sub>p r)" by simp - hence " \(bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs (a^\<^sub>p (k' - k)*\<^sub>p s) = + hence " \(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a^\<^sub>p (k' - k)*\<^sub>p s) = Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs ?p' + Ipoly bs p * Ipoly bs q + Ipoly bs r" by (simp add: field_simps) - hence " \(bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = + hence " \(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 1\<^sub>p *\<^sub>p p) + Ipoly bs p * Ipoly bs q + Ipoly bs r" by (auto simp only: funpow_shift1_1) - hence "\(bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = + hence "\(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 1\<^sub>p) + Ipoly bs q) + Ipoly bs r" by (simp add: field_simps) - hence "\(bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = + hence "\(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = Ipoly bs (p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 1\<^sub>p) +\<^sub>p q) +\<^sub>p r)" by simp with isnpolyh_unique[OF nakks' nqr'] have "a ^\<^sub>p (k' - k) *\<^sub>p s = @@ -1444,9 +1444,9 @@ apply (simp) by (rule polydivide_aux_real_domintros, simp_all) have dom: ?dths apply (rule polydivide_aux_real_domintros) using ba dn' domsp by simp_all - from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::{field, division_ring_inverse_zero, ring_char_0}"] - have " \(bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs s = Ipoly bs ?p'" by simp - hence "\(bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)" using np nxdn apply simp + from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::{field_char_0, field_inverse_zero}"] + have " \(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs s = Ipoly bs ?p'" by simp + hence "\(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)" using np nxdn apply simp by (simp only: funpow_shift1_1) simp hence sp': "s = ?xdn *\<^sub>p p" using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]] by blast {assume h1: "polydivide_aux (a,n,p,k,s) = (k',r)" @@ -1501,7 +1501,7 @@ and dr: "degree r = 0 \ degree r < degree p" and qr: "a ^\<^sub>p (k' - Suc k) *\<^sub>p ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = p *\<^sub>p q +\<^sub>p r" by auto from kk' have kk'':"Suc (k' - Suc k) = k' - k" by arith - {fix bs:: "'a::{field, division_ring_inverse_zero, ring_char_0} list" + {fix bs:: "'a::{field_char_0, field_inverse_zero} list" from qr isnpolyh_unique[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k", simplified ap] nasbp', symmetric] have "Ipoly bs (a ^\<^sub>p (k' - Suc k) *\<^sub>p ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p'))) = Ipoly bs (p *\<^sub>p q +\<^sub>p r)" by simp @@ -1511,7 +1511,7 @@ by (simp add:kk'' funpow_shift1_1[where n="degree s - n" and p="p"]) hence "Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = Ipoly bs p * (Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn) + Ipoly bs r" by (simp add: field_simps)} - hence ieq:"\(bs :: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = + hence ieq:"\(bs :: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = Ipoly bs (p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r)" by auto let ?q = "q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)" from polyadd_normh[OF nq polymul_normh[OF polymul_normh[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k"] head_isnpolyh[OF ns], simplified ap ] nxdn]] @@ -1532,17 +1532,17 @@ apply (simp) by (rule polydivide_aux_real_domintros, simp_all) have dom: ?dths using sz ba dn' domsp by - (rule polydivide_aux_real_domintros, simp_all) - {fix bs :: "'a::{field, division_ring_inverse_zero, ring_char_0} list" + {fix bs :: "'a::{field_char_0, field_inverse_zero} list" from isnpolyh_unique[OF nth, where ?'a="'a" and q="0\<^sub>p",simplified,symmetric] spz have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'" by simp hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (?b *\<^sub>p ?xdn) * Ipoly bs p" by (simp add: funpow_shift1_1[where n="degree s - n" and p="p"]) hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" by simp } - hence hth: "\ (bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" .. + hence hth: "\ (bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" .. from hth have asq: "a *\<^sub>p s = p *\<^sub>p (?b *\<^sub>p ?xdn)" - using isnpolyh_unique[where ?'a = "'a::{field, division_ring_inverse_zero, ring_char_0}", OF polymul_normh[OF head_isnpolyh[OF np] ns] + using isnpolyh_unique[where ?'a = "'a::{field_char_0, field_inverse_zero}", OF polymul_normh[OF head_isnpolyh[OF np] ns] polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]], simplified ap] by simp {assume h1: "polydivide_aux (a,n,p,k,s) = (k', r)" @@ -1566,7 +1566,7 @@ qed lemma polydivide_properties: - assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" and np: "isnpolyh p n0" and ns: "isnpolyh s n1" and pnz: "p \ 0\<^sub>p" shows "(\ k r. polydivide s p = (k,r) \ (\nr. isnpolyh r nr) \ (degree r = 0 \ degree r < degree p) \ (\q n1. isnpolyh q n1 \ ((polypow k (head p)) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)))" @@ -1698,11 +1698,11 @@ definition "swapnorm n m t = polynate (swap n m t)" lemma swapnorm: assumes nbs: "n < length bs" and mbs: "m < length bs" - shows "((Ipoly bs (swapnorm n m t) :: 'a\{field, division_ring_inverse_zero, ring_char_0})) = Ipoly ((bs[n:= bs!m])[m:= bs!n]) t" + shows "((Ipoly bs (swapnorm n m t) :: 'a\{field_char_0, field_inverse_zero})) = Ipoly ((bs[n:= bs!m])[m:= bs!n]) t" using swap[OF prems] swapnorm_def by simp lemma swapnorm_isnpoly[simp]: - assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "isnpoly (swapnorm n m p)" unfolding swapnorm_def by simp diff -r bc7982c54e37 -r d323e7773aa8 src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy --- a/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy Mon Apr 26 11:34:19 2010 +0200 +++ b/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy Mon Apr 26 15:37:50 2010 +0200 @@ -7,147 +7,147 @@ begin lemma - "\(y::'a::{linordered_field, division_ring_inverse_zero, number_ring}) <2. x + 3* y < 0 \ x - y >0" + "\(y::'a::{linordered_field_inverse_zero, number_ring}) <2. x + 3* y < 0 \ x - y >0" by ferrack -lemma "~ (ALL x (y::'a::{linordered_field, division_ring_inverse_zero, number_ring}). x < y --> 10*x < 11*y)" +lemma "~ (ALL x (y::'a::{linordered_field_inverse_zero, number_ring}). x < y --> 10*x < 11*y)" by ferrack -lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. x < y --> (10*(x + 5*y + -1) < 60*y)" +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y. x < y --> (10*(x + 5*y + -1) < 60*y)" by ferrack -lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. x ~= y --> x < y" +lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}) y. x ~= y --> x < y" by ferrack -lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (x ~= y & 10*x ~= 9*y & 10*x < y) --> x < y" +lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}) y. (x ~= y & 10*x ~= 9*y & 10*x < y) --> x < y" by ferrack -lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (x ~= y & 5*x <= y) --> 500*x <= 100*y" +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y. (x ~= y & 5*x <= y) --> 500*x <= 100*y" by ferrack -lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (EX (y::'a::{linordered_field, division_ring_inverse_zero, number_ring}). 4*x + 3*y <= 0 & 4*x + 3*y >= -1)" +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}). (EX (y::'a::{linordered_field_inverse_zero, number_ring}). 4*x + 3*y <= 0 & 4*x + 3*y >= -1)" by ferrack -lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) < 0. (EX (y::'a::{linordered_field, division_ring_inverse_zero, number_ring}) > 0. 7*x + y > 0 & x - y <= 9)" +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) < 0. (EX (y::'a::{linordered_field_inverse_zero, number_ring}) > 0. 7*x + y > 0 & x - y <= 9)" by ferrack -lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (0 < x & x < 1) --> (ALL y > 1. x + y ~= 1)" +lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}). (0 < x & x < 1) --> (ALL y > 1. x + y ~= 1)" by ferrack -lemma "EX x. (ALL (y::'a::{linordered_field, division_ring_inverse_zero, number_ring}). y < 2 --> 2*(y - x) \ 0 )" +lemma "EX x. (ALL (y::'a::{linordered_field_inverse_zero, number_ring}). y < 2 --> 2*(y - x) \ 0 )" by ferrack -lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). x < 10 | x > 20 | (EX y. y>= 0 & y <= 10 & x+y = 20)" +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}). x < 10 | x > 20 | (EX y. y>= 0 & y <= 10 & x+y = 20)" by ferrack -lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y z. x + y < z --> y >= z --> x < 0" +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y z. x + y < z --> y >= z --> x < 0" by ferrack -lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y z. x + 7*y < 5* z & 5*y >= 7*z & x < 0" +lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}) y z. x + 7*y < 5* z & 5*y >= 7*z & x < 0" by ferrack -lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y z. abs (x + y) <= z --> (abs z = z)" +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y z. abs (x + y) <= z --> (abs z = z)" by ferrack -lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y z. x + 7*y - 5* z < 0 & 5*y + 7*z + 3*x < 0" +lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}) y z. x + 7*y - 5* z < 0 & 5*y + 7*z + 3*x < 0" by ferrack -lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y z. (abs (5*x+3*y+z) <= 5*x+3*y+z & abs (5*x+3*y+z) >= - (5*x+3*y+z)) | (abs (5*x+3*y+z) >= 5*x+3*y+z & abs (5*x+3*y+z) <= - (5*x+3*y+z))" +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y z. (abs (5*x+3*y+z) <= 5*x+3*y+z & abs (5*x+3*y+z) >= - (5*x+3*y+z)) | (abs (5*x+3*y+z) >= 5*x+3*y+z & abs (5*x+3*y+z) <= - (5*x+3*y+z))" by ferrack -lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. x < y --> (EX z>0. x+z = y)" +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y. x < y --> (EX z>0. x+z = y)" by ferrack -lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. x < y --> (EX z>0. x+z = y)" +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y. x < y --> (EX z>0. x+z = y)" by ferrack -lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (EX z>0. abs (x - y) <= z )" +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y. (EX z>0. abs (x - y) <= z )" by ferrack -lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))" +lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))" by ferrack -lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (ALL z>=0. abs (3*x+7*y) <= 2*z + 1)" +lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}) y. (ALL z>=0. abs (3*x+7*y) <= 2*z + 1)" by ferrack -lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))" +lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))" by ferrack -lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring})>0. (ALL y. (EX z. 13* abs z \ abs (12*y - x) & 5*x - 3*(abs y) <= 7*z))" +lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring})>0. (ALL y. (EX z. 13* abs z \ abs (12*y - x) & 5*x - 3*(abs y) <= 7*z))" by ferrack -lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). abs (4*x + 17) < 4 & (ALL y . abs (x*34 - 34*y - 9) \ 0 \ (EX z. 5*x - 3*abs y <= 7*z))" +lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}). abs (4*x + 17) < 4 & (ALL y . abs (x*34 - 34*y - 9) \ 0 \ (EX z. 5*x - 3*abs y <= 7*z))" by ferrack -lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (EX y > abs (23*x - 9). (ALL z > abs (3*y - 19* abs x). x+z > 2*y))" +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}). (EX y > abs (23*x - 9). (ALL z > abs (3*y - 19* abs x). x+z > 2*y))" by ferrack -lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (EX y< abs (3*x - 1). (ALL z >= (3*abs x - 1). abs (12*x - 13*y + 19*z) > abs (23*x) ))" +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}). (EX y< abs (3*x - 1). (ALL z >= (3*abs x - 1). abs (12*x - 13*y + 19*z) > abs (23*x) ))" by ferrack -lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). abs x < 100 & (ALL y > x. (EX z<2*y - x. 5*x - 3*y <= 7*z))" +lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}). abs x < 100 & (ALL y > x. (EX z<2*y - x. 5*x - 3*y <= 7*z))" by ferrack -lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y z w. 7*x<3*y --> 5*y < 7*z --> z < 2*w --> 7*(2*w-x) > 2*y" +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y z w. 7*x<3*y --> 5*y < 7*z --> z < 2*w --> 7*(2*w-x) > 2*y" by ferrack -lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y z w. 5*x + 3*z - 17*w + abs (y - 8*x + z) <= 89" +lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}) y z w. 5*x + 3*z - 17*w + abs (y - 8*x + z) <= 89" by ferrack -lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y z w. 5*x + 3*z - 17*w + 7* (y - 8*x + z) <= max y (7*z - x + w)" +lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}) y z w. 5*x + 3*z - 17*w + 7* (y - 8*x + z) <= max y (7*z - x + w)" by ferrack -lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)" +lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)" by ferrack -lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y z. (EX w >= (x+y+z). w <= abs x + abs y + abs z)" +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y z. (EX w >= (x+y+z). w <= abs x + abs y + abs z)" by ferrack -lemma "~(ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (EX y z w. 3* x + z*4 = 3*y & x + y < z & x> w & 3*x < w + y))" +lemma "~(ALL (x::'a::{linordered_field_inverse_zero, number_ring}). (EX y z w. 3* x + z*4 = 3*y & x + y < z & x> w & 3*x < w + y))" by ferrack -lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (EX z w. abs (x-y) = (z-w) & z*1234 < 233*x & w ~= y)" +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y. (EX z w. abs (x-y) = (z-w) & z*1234 < 233*x & w ~= y)" by ferrack -lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (EX y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w))" +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}). (EX y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w))" by ferrack -lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y z. (ALL w >= abs (x+y+z). w >= abs x + abs y + abs z)" +lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}) y z. (ALL w >= abs (x+y+z). w >= abs x + abs y + abs z)" by ferrack -lemma "EX z. (ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (EX w >= (x+y+z). w <= abs x + abs y + abs z))" +lemma "EX z. (ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y. (EX w >= (x+y+z). w <= abs x + abs y + abs z))" by ferrack -lemma "EX z. (ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) < abs z. (EX y w. x< y & x < z & x> w & 3*x < w + y))" +lemma "EX z. (ALL (x::'a::{linordered_field_inverse_zero, number_ring}) < abs z. (EX y w. x< y & x < z & x> w & 3*x < w + y))" by ferrack -lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (EX z. (ALL w. abs (x-y) = abs (z-w) --> z < x & w ~= y))" +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y. (EX z. (ALL w. abs (x-y) = abs (z-w) --> z < x & w ~= y))" by ferrack -lemma "EX y. (ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (EX z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)))" +lemma "EX y. (ALL (x::'a::{linordered_field_inverse_zero, number_ring}). (EX z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)))" by ferrack -lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) z. (ALL w >= 13*x - 4*z. (EX y. w >= abs x + abs y + z))" +lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}) z. (ALL w >= 13*x - 4*z. (EX y. w >= abs x + abs y + z))" by ferrack -lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (ALL y < x. (EX z > (x+y). +lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}). (ALL y < x. (EX z > (x+y). (ALL w. 5*w + 10*x - z >= y --> w + 7*x + 3*z >= 2*y)))" by ferrack -lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (ALL y. (EX z > y. +lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}). (ALL y. (EX z > y. (ALL w . w < 13 --> w + 10*x - z >= y --> 5*w + 7*x + 13*z >= 2*y)))" by ferrack -lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)" +lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)" by ferrack -lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (y - x) < w)))" +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (y - x) < w)))" by ferrack -lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (x + z) < w - y)))" +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (x + z) < w - y)))" by ferrack -lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (EX y. abs y ~= abs x & (ALL z> max x y. (EX w. w ~= y & w ~= z & 3*w - z >= x + y)))" +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}). (EX y. abs y ~= abs x & (ALL z> max x y. (EX w. w ~= y & w ~= z & 3*w - z >= x + y)))" by ferrack end diff -r bc7982c54e37 -r d323e7773aa8 src/HOL/Fields.thy --- a/src/HOL/Fields.thy Mon Apr 26 11:34:19 2010 +0200 +++ b/src/HOL/Fields.thy Mon Apr 26 15:37:50 2010 +0200 @@ -129,22 +129,20 @@ 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_ring_inverse_zero})" - proof cases - assume "a \ 0 & b \ 0" - thus ?thesis by (simp add: nonzero_inverse_mult_distrib mult_ac) - next - assume "~ (a \ 0 & b \ 0)" - thus ?thesis by force - qed + "inverse (a * b) = inverse a * inverse b" +proof cases + assume "a \ 0 & b \ 0" + thus ?thesis by (simp add: nonzero_inverse_mult_distrib mult_ac) +next + assume "~ (a \ 0 & b \ 0)" + thus ?thesis by force +qed lemma inverse_divide [simp]: - "inverse (a/b) = b / (a::'a::{field,division_ring_inverse_zero})" + "inverse (a / b) = b / a" by (simp add: divide_inverse mult_commute) @@ -155,86 +153,88 @@ 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_ring_inverse_zero})" + "c \ 0 \ (c * a) / (c * b) = a / b" 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_ring_inverse_zero})" + "c \ 0 \ (a * c) / (b * c) = a / b" 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_ring_inverse_zero})" -by (simp add: divide_inverse mult_ac) +lemma divide_divide_eq_right [simp, no_atp]: + "a / (b / c) = (a * c) / b" + by (simp add: divide_inverse mult_ac) -lemma divide_divide_eq_left [simp,no_atp]: - "(a / b) / (c::'a::{field,division_ring_inverse_zero}) = a / (b*c)" -by (simp add: divide_inverse mult_assoc) +lemma divide_divide_eq_left [simp, no_atp]: + "(a / b) / c = 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_ring_inverse_zero}" -shows "(c*a) / (c*b) = (if c=0 then 0 else a/b)" -by (simp add: mult_divide_mult_cancel_left) +lemma mult_divide_mult_cancel_left_if [simp,no_atp]: + 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_ring_inverse_zero})" -by (simp add: divide_inverse) +lemma minus_divide_right: + "- (a / b) = a / - b" + by (simp add: divide_inverse) lemma divide_minus_right [simp, no_atp]: - "a / -(b::'a::{field,division_ring_inverse_zero}) = -(a / b)" -by (simp add: divide_inverse) + "a / - b = - (a / b)" + by (simp add: divide_inverse) lemma minus_divide_divide: - "(-a)/(-b) = a / (b::'a::{field,division_ring_inverse_zero})" + "(- a) / (- b) = a / b" apply (cases "b=0", simp) apply (simp add: nonzero_minus_divide_divide) done lemma eq_divide_eq: - "((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) + "a = 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_ring_inverse_zero})) = (if c\0 then b = a*c else a=0)" -by (force simp add: nonzero_divide_eq_eq) + "b / c = a \ (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_ring_inverse_zero}))" -by (insert inverse_eq_iff_eq [of x 1], simp) + "inverse x = 1 \ x = 1" + 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_ring_inverse_zero}))" -by (simp add: divide_inverse) +lemma divide_eq_0_iff [simp, no_atp]: + "a / b = 0 \ a = 0 \ b = 0" + by (simp add: divide_inverse) -lemma divide_cancel_right [simp,no_atp]: - "(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_right [simp, no_atp]: + "a / c = b / c \ c = 0 \ a = b" + 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_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" + 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_ring_inverse_zero}))" -apply (cases "b=0", simp) -apply (simp add: right_inverse_eq) -done +lemma divide_eq_1_iff [simp, no_atp]: + "a / b = 1 \ b \ 0 \ a = b" + 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_ring_inverse_zero}))" -by (simp add: eq_commute [of 1]) +lemma one_eq_divide_iff [simp, no_atp]: + "1 = a / b \ b \ 0 \ a = b" + by (simp add: eq_commute [of 1]) + +end text {* Ordered Fields *} @@ -650,39 +650,37 @@ 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_ring_inverse_zero}))" + else a \ 0)" 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_ring_inverse_zero}))" + "(0 < inverse a) = (0 < a)" 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_ring_inverse_zero}))" + "(inverse a < 0) = (a < 0)" 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_ring_inverse_zero}))" -by (simp add: linorder_not_less [symmetric]) + "0 \ inverse a \ 0 \ a" + by (simp add: not_less [symmetric]) lemma inverse_nonpositive_iff_nonpositive [simp]: - "(inverse a \ 0) = (a \ (0::'a::{linordered_field,division_ring_inverse_zero}))" -by (simp add: linorder_not_less [symmetric]) + "inverse a \ 0 \ a \ 0" + by (simp add: not_less [symmetric]) lemma one_less_inverse_iff: - "(1 < inverse x) = (0 < x & x < (1::'a::{linordered_field,division_ring_inverse_zero}))" + "1 < inverse x \ 0 < x \ x < 1" proof cases assume "0 < x" with inverse_less_iff_less [OF zero_less_one, of x] @@ -692,7 +690,7 @@ have "~ (1 < inverse x)" proof assume "1 < inverse x" - also with notless have "... \ 0" by (simp add: linorder_not_less) + also with notless have "... \ 0" by simp also have "... < 1" by (rule zero_less_one) finally show False by auto qed @@ -700,62 +698,69 @@ qed lemma one_le_inverse_iff: - "(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) + "1 \ inverse x \ 0 < x \ x \ 1" +proof (cases "x = 1") + case True then show ?thesis by simp +next + case False then have "inverse x \ 1" by simp + then have "1 \ inverse x" by blast + then have "1 \ inverse x \ 1 < inverse x" by (simp add: le_less) + with False show ?thesis by (auto simp add: one_less_inverse_iff) +qed lemma inverse_less_1_iff: - "(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) + "inverse x < 1 \ x \ 0 \ 1 < x" + by (simp add: not_le [symmetric] one_le_inverse_iff) lemma inverse_le_1_iff: - "(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) + "inverse x \ 1 \ x \ 0 \ 1 \ x" + by (simp add: 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 \ (a::'a::{linordered_field,division_ring_inverse_zero}))" + else 0 \ a)" apply (cases "c=0", simp) -apply (force simp add: pos_divide_le_eq neg_divide_le_eq linorder_neq_iff) +apply (force simp add: pos_divide_le_eq neg_divide_le_eq) done lemma less_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_ring_inverse_zero}))" + else a < 0)" apply (cases "c=0", simp) -apply (force simp add: pos_less_divide_eq neg_less_divide_eq linorder_neq_iff) +apply (force simp add: pos_less_divide_eq neg_less_divide_eq) done lemma divide_less_eq: "(b/c < a) = (if 0 < c then b < a*c else if c < 0 then a*c < b - else 0 < (a::'a::{linordered_field,division_ring_inverse_zero}))" + else 0 < a)" apply (cases "c=0", simp) -apply (force simp add: pos_divide_less_eq neg_divide_less_eq linorder_neq_iff) +apply (force simp add: pos_divide_less_eq neg_divide_less_eq) done text {*Division and Signs*} lemma zero_less_divide_iff: - "((0::'a::{linordered_field,division_ring_inverse_zero}) < a/b) = (0 < a & 0 < b | a < 0 & b < 0)" + "(0 < a/b) = (0 < a & 0 < b | a < 0 & b < 0)" by (simp add: divide_inverse zero_less_mult_iff) lemma divide_less_0_iff: - "(a/b < (0::'a::{linordered_field,division_ring_inverse_zero})) = + "(a/b < 0) = (0 < a & b < 0 | a < 0 & 0 < b)" by (simp add: divide_inverse mult_less_0_iff) lemma zero_le_divide_iff: - "((0::'a::{linordered_field,division_ring_inverse_zero}) \ a/b) = + "(0 \ a/b) = (0 \ a & 0 \ b | a \ 0 & b \ 0)" by (simp add: divide_inverse zero_le_mult_iff) lemma divide_le_0_iff: - "(a/b \ (0::'a::{linordered_field,division_ring_inverse_zero})) = + "(a/b \ 0) = (0 \ a & b \ 0 | a \ 0 & 0 \ b)" by (simp add: divide_inverse mult_le_0_iff) @@ -764,13 +769,13 @@ text{*Simplify expressions equated with 1*} lemma zero_eq_1_divide_iff [simp,no_atp]: - "((0::'a::{linordered_field,division_ring_inverse_zero}) = 1/a) = (a = 0)" + "(0 = 1/a) = (a = 0)" apply (cases "a=0", simp) apply (auto simp add: nonzero_eq_divide_eq) done lemma one_divide_eq_0_iff [simp,no_atp]: - "(1/a = (0::'a::{linordered_field,division_ring_inverse_zero})) = (a = 0)" + "(1/a = 0) = (a = 0)" apply (cases "a=0", simp) apply (insert zero_neq_one [THEN not_sym]) apply (auto simp add: nonzero_divide_eq_eq) @@ -788,16 +793,16 @@ declare divide_le_0_1_iff [simp,no_atp] lemma divide_right_mono: - "[|a \ b; 0 \ c|] ==> a/c \ b/(c::'a::{linordered_field,division_ring_inverse_zero})" -by (force simp add: divide_strict_right_mono order_le_less) + "[|a \ b; 0 \ c|] ==> a/c \ b/c" +by (force simp add: divide_strict_right_mono le_less) -lemma divide_right_mono_neg: "(a::'a::{linordered_field,division_ring_inverse_zero}) <= b +lemma divide_right_mono_neg: "a <= b ==> c <= 0 ==> b / c <= a / c" apply (drule divide_right_mono [of _ _ "- c"]) apply auto done -lemma divide_left_mono_neg: "(a::'a::{linordered_field,division_ring_inverse_zero}) <= b +lemma divide_left_mono_neg: "a <= b ==> c <= 0 ==> 0 < a * b ==> c / a <= c / b" apply (drule divide_left_mono [of _ _ "- c"]) apply (auto simp add: mult_commute) @@ -808,99 +813,84 @@ text{*Simplify quotients that are compared with the value 1.*} lemma le_divide_eq_1 [no_atp]: - fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}" - shows "(1 \ b / a) = ((0 < a & a \ b) | (a < 0 & b \ a))" + "(1 \ b / a) = ((0 < a & a \ b) | (a < 0 & b \ a))" by (auto simp add: le_divide_eq) lemma divide_le_eq_1 [no_atp]: - fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}" - shows "(b / a \ 1) = ((0 < a & b \ a) | (a < 0 & a \ b) | a=0)" + "(b / a \ 1) = ((0 < a & b \ a) | (a < 0 & a \ b) | a=0)" by (auto simp add: divide_le_eq) lemma less_divide_eq_1 [no_atp]: - fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}" - shows "(1 < b / a) = ((0 < a & a < b) | (a < 0 & b < a))" + "(1 < b / a) = ((0 < a & a < b) | (a < 0 & b < a))" by (auto simp add: less_divide_eq) lemma divide_less_eq_1 [no_atp]: - fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}" - shows "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)" + "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)" by (auto simp add: divide_less_eq) text {*Conditional Simplification Rules: No Case Splits*} lemma le_divide_eq_1_pos [simp,no_atp]: - fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}" - shows "0 < a \ (1 \ b/a) = (a \ b)" + "0 < a \ (1 \ b/a) = (a \ b)" by (auto simp add: le_divide_eq) lemma le_divide_eq_1_neg [simp,no_atp]: - fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}" - shows "a < 0 \ (1 \ b/a) = (b \ a)" + "a < 0 \ (1 \ b/a) = (b \ a)" by (auto simp add: le_divide_eq) lemma divide_le_eq_1_pos [simp,no_atp]: - fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}" - shows "0 < a \ (b/a \ 1) = (b \ a)" + "0 < a \ (b/a \ 1) = (b \ a)" by (auto simp add: divide_le_eq) lemma divide_le_eq_1_neg [simp,no_atp]: - fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}" - shows "a < 0 \ (b/a \ 1) = (a \ b)" + "a < 0 \ (b/a \ 1) = (a \ b)" by (auto simp add: divide_le_eq) lemma less_divide_eq_1_pos [simp,no_atp]: - fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}" - shows "0 < a \ (1 < b/a) = (a < b)" + "0 < a \ (1 < b/a) = (a < b)" by (auto simp add: less_divide_eq) lemma less_divide_eq_1_neg [simp,no_atp]: - fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}" - shows "a < 0 \ (1 < b/a) = (b < a)" + "a < 0 \ (1 < b/a) = (b < a)" by (auto simp add: less_divide_eq) lemma divide_less_eq_1_pos [simp,no_atp]: - fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}" - shows "0 < a \ (b/a < 1) = (b < a)" + "0 < a \