\<^sub>N y) = INum x / (INum y ::'a :: {field_char_0, field_inverse_zero})" +lemma Ndiv[simp]: "INum (x \

\<^sub>N y) = INum x / (INum y ::'a :: {field_char_0, field})" by (simp add: Ndiv_def) lemma Nlt0_iff[simp]: assumes nx: "isnormNum x" - shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})< 0) = 0>\<^sub>N x" + shows "((INum x :: 'a :: {field_char_0, linordered_field})< 0) = 0>\<^sub>N x" proof - obtain a b where x: "x = (a, b)" by (cases x) { assume "a = 0" hence ?thesis by (simp add: x Nlt0_def INum_def) } @@ -323,7 +323,7 @@ lemma Nle0_iff[simp]: assumes nx: "isnormNum x" - shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) \ 0) = 0\\<^sub>N x" + shows "((INum x :: 'a :: {field_char_0, linordered_field}) \ 0) = 0\\<^sub>N x" proof - obtain a b where x: "x = (a, b)" by (cases x) { assume "a = 0" hence ?thesis by (simp add: x Nle0_def INum_def) } @@ -337,7 +337,7 @@ lemma Ngt0_iff[simp]: assumes nx: "isnormNum x" - shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})> 0) = 0<\<^sub>N x" + shows "((INum x :: 'a :: {field_char_0, linordered_field})> 0) = 0<\<^sub>N x" proof - obtain a b where x: "x = (a, b)" by (cases x) { assume "a = 0" hence ?thesis by (simp add: x Ngt0_def INum_def) } @@ -351,7 +351,7 @@ lemma Nge0_iff[simp]: assumes nx: "isnormNum x" - shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) \ 0) = 0\\<^sub>N x" + shows "((INum x :: 'a :: {field_char_0, linordered_field}) \ 0) = 0\\<^sub>N x" proof - obtain a b where x: "x = (a, b)" by (cases x) { assume "a = 0" hence ?thesis by (simp add: x Nge0_def INum_def) } @@ -365,7 +365,7 @@ lemma Nlt_iff[simp]: assumes nx: "isnormNum x" and ny: "isnormNum y" - shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) < INum y) = (x <\<^sub>N y)" + shows "((INum x :: 'a :: {field_char_0, linordered_field}) < INum y) = (x <\<^sub>N y)" proof - let ?z = "0::'a" have "((INum x ::'a) < INum y) = (INum (x -\<^sub>N y) < ?z)" @@ -377,7 +377,7 @@ lemma Nle_iff[simp]: assumes nx: "isnormNum x" and ny: "isnormNum y" - shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})\ INum y) = (x \\<^sub>N y)" + shows "((INum x :: 'a :: {field_char_0, linordered_field})\ INum y) = (x \\<^sub>N y)" proof - have "((INum x ::'a) \ INum y) = (INum (x -\<^sub>N y) \ (0::'a))" using nx ny by simp @@ -387,7 +387,7 @@ qed lemma Nadd_commute: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field})" shows "x +\<^sub>N y = y +\<^sub>N x" proof - have n: "isnormNum (x +\<^sub>N y)" "isnormNum (y +\<^sub>N x)" by simp_all @@ -396,7 +396,7 @@ qed lemma [simp]: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field})" shows "(0, b) +\<^sub>N y = normNum y" and "(a, 0) +\<^sub>N y = normNum y" and "x +\<^sub>N (0, b) = normNum x" @@ -408,7 +408,7 @@ done lemma normNum_nilpotent_aux[simp]: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field})" assumes nx: "isnormNum x" shows "normNum x = x" proof - @@ -419,7 +419,7 @@ qed lemma normNum_nilpotent[simp]: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field})" shows "normNum (normNum x) = normNum x" by simp @@ -427,11 +427,11 @@ by (simp_all add: normNum_def) lemma normNum_Nadd: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field})" shows "normNum (x +\<^sub>N y) = x +\<^sub>N y" by simp lemma Nadd_normNum1[simp]: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field})" shows "normNum x +\<^sub>N y = x +\<^sub>N y" proof - have n: "isnormNum (normNum x +\<^sub>N y)" "isnormNum (x +\<^sub>N y)" by simp_all @@ -441,7 +441,7 @@ qed lemma Nadd_normNum2[simp]: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field})" shows "x +\<^sub>N normNum y = x +\<^sub>N y" proof - have n: "isnormNum (x +\<^sub>N normNum y)" "isnormNum (x +\<^sub>N y)" by simp_all @@ -451,7 +451,7 @@ qed lemma Nadd_assoc: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field})" shows "x +\<^sub>N y +\<^sub>N z = x +\<^sub>N (y +\<^sub>N z)" proof - have n: "isnormNum (x +\<^sub>N y +\<^sub>N z)" "isnormNum (x +\<^sub>N (y +\<^sub>N z))" by simp_all @@ -463,7 +463,7 @@ by (simp add: Nmul_def split_def Let_def gcd_commute_int mult.commute) lemma Nmul_assoc: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field})" assumes nx: "isnormNum x" and ny: "isnormNum y" and nz: "isnormNum z" shows "x *\<^sub>N y *\<^sub>N z = x *\<^sub>N (y *\<^sub>N z)" proof - @@ -474,7 +474,7 @@ qed lemma Nsub0: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field})" assumes x: "isnormNum x" and y: "isnormNum y" shows "x -\<^sub>N y = 0\<^sub>N \ x = y" proof - @@ -490,7 +490,7 @@ by (simp_all add: Nmul_def Let_def split_def) lemma Nmul_eq0[simp]: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field})" assumes nx: "isnormNum x" and ny: "isnormNum y" shows "x*\<^sub>N y = 0\<^sub>N \ x = 0\<^sub>N \ y = 0\<^sub>N" proof - diff -r eebe69f31474 -r 58043346ca64 src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Tue Mar 31 16:49:41 2015 +0100 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Tue Mar 31 21:54:32 2015 +0200 @@ -235,7 +235,7 @@ subsection{* Semantics of the polynomial representation *} -primrec Ipoly :: "'a list \ poly \ 'a::{field_char_0,field_inverse_zero,power}" +primrec Ipoly :: "'a list \ poly \ 'a::{field_char_0,field,power}" where "Ipoly bs (C c) = INum c" | "Ipoly bs (Bound n) = bs!n" @@ -246,7 +246,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::{field_char_0,field_inverse_zero,power}" +abbreviation Ipoly_syntax :: "poly \ 'a list \'a::{field_char_0,field,power}" ("\_\\<^sub>p\<^bsup>_\<^esup>") where "\p\\<^sub>p\<^bsup>bs\<^esup> \ Ipoly bs p" @@ -481,7 +481,7 @@ qed simp_all lemma polymul_properties: - assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0,field})" and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and m: "m \ min n0 n1" @@ -670,23 +670,23 @@ by (induct p q rule: polymul.induct) (auto simp add: field_simps) lemma polymul_normh: - assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0,field})" 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_char_0,field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0,field})" 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_char_0,field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0,field})" 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)" by (fact polymul_properties(3)) lemma polymul_norm: - assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0,field})" shows "isnpoly p \ isnpoly q \ isnpoly (polymul p q)" using polymul_normh[of "p" "0" "q" "0"] isnpoly_def by simp @@ -699,7 +699,7 @@ lemma monic_eqI: assumes np: "isnpolyh p n0" shows "INum (headconst p) * Ipoly bs (fst (monic p)) = - (Ipoly bs p ::'a::{field_char_0,field_inverse_zero, power})" + (Ipoly bs p ::'a::{field_char_0,field, power})" unfolding monic_def Let_def proof (cases "headconst p = 0\<^sub>N", simp_all add: headconst_zero[OF np]) let ?h = "headconst p" @@ -750,13 +750,13 @@ using polyadd_norm polyneg_norm by (simp add: polysub_def) lemma polysub_same_0[simp]: - assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0,field})" 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_char_0,field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0,field})" 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 by (induct p q arbitrary: n0 n1 rule:polyadd.induct) @@ -765,7 +765,7 @@ text{* polypow is a power function and preserves normal forms *} lemma polypow[simp]: - "Ipoly bs (polypow n p) = (Ipoly bs p :: 'a::{field_char_0,field_inverse_zero}) ^ n" + "Ipoly bs (polypow n p) = (Ipoly bs p :: 'a::{field_char_0,field}) ^ n" proof (induct n rule: polypow.induct) case 1 then show ?case @@ -806,7 +806,7 @@ qed lemma polypow_normh: - assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0,field})" shows "isnpolyh p n \ isnpolyh (polypow k p) n" proof (induct k arbitrary: n rule: polypow.induct) case 1 @@ -826,18 +826,18 @@ qed lemma polypow_norm: - assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0,field})" 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_char_0,field_inverse_zero})" + "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0,field})" by (induct p rule:polynate.induct) auto lemma polynate_norm[simp]: - assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0,field})" shows "isnpoly (polynate p)" by (induct p rule: polynate.induct) (simp_all add: polyadd_norm polymul_norm polysub_norm polyneg_norm polypow_norm, @@ -868,7 +868,7 @@ using assms by (induct k arbitrary: p) auto lemma funpow_shift1: - "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0,field_inverse_zero}) = + "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0,field}) = Ipoly bs (Mul (Pw (Bound 0) n) p)" by (induct n arbitrary: p) (simp_all add: shift1_isnpoly shift1) @@ -876,7 +876,7 @@ 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_char_0,field_inverse_zero}) = + "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0,field}) = Ipoly bs (funpow n shift1 (1)\<^sub>p *\<^sub>p p)" by (simp add: funpow_shift1) @@ -886,7 +886,7 @@ lemma behead: assumes "isnpolyh p n" shows "Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = - (Ipoly bs p :: 'a :: {field_char_0,field_inverse_zero})" + (Ipoly bs p :: 'a :: {field_char_0,field})" using assms proof (induct p arbitrary: n rule: behead.induct) case (1 c p n) @@ -1160,7 +1160,7 @@ lemma isnpolyh_zero_iff: 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})" + and eq :"\bs. wf_bs bs p \ \p\\<^sub>p\<^bsup>bs\<^esup> = (0::'a::{field_char_0,field, power})" shows "p = 0\<^sub>p" using nq eq proof (induct "maxindex p" arbitrary: p n0 rule: less_induct) @@ -1242,7 +1242,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::{field_char_0,field_inverse_zero,power})) \ p = q" + shows "(\bs. \p\\<^sub>p\<^bsup>bs\<^esup> = (\q\\<^sub>p\<^bsup>bs\<^esup> :: 'a::{field_char_0,field,power})) \ p = q" proof auto assume H: "\bs. (\p\\<^sub>p\<^bsup>bs\<^esup> ::'a) = \q\\<^sub>p\<^bsup>bs\<^esup>" then have "\bs.\p -\<^sub>p q\\<^sub>p\<^bsup>bs\<^esup>= (0::'a)" @@ -1257,7 +1257,7 @@ text{* consequences of unicity on the algorithms for polynomial normalization *} lemma polyadd_commute: - assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0,field})" and np: "isnpolyh p n0" and nq: "isnpolyh q n1" shows "p +\<^sub>p q = q +\<^sub>p p" @@ -1271,7 +1271,7 @@ by simp lemma polyadd_0[simp]: - assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0,field})" and np: "isnpolyh p n0" shows "p +\<^sub>p 0\<^sub>p = p" and "0\<^sub>p +\<^sub>p p = p" @@ -1279,7 +1279,7 @@ isnpolyh_unique[OF polyadd_normh[OF zero_normh np] np] by simp_all lemma polymul_1[simp]: - assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0,field})" and np: "isnpolyh p n0" shows "p *\<^sub>p (1)\<^sub>p = p" and "(1)\<^sub>p *\<^sub>p p = p" @@ -1287,7 +1287,7 @@ isnpolyh_unique[OF polymul_normh[OF one_normh np] np] by simp_all lemma polymul_0[simp]: - assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0,field})" 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" @@ -1295,27 +1295,27 @@ isnpolyh_unique[OF polymul_normh[OF zero_normh np] zero_normh] by simp_all lemma polymul_commute: - assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0,field})" 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::{field_char_0,field_inverse_zero, power}"] + where ?'a = "'a::{field_char_0,field, power}"] by simp declare polyneg_polyneg [simp] lemma isnpolyh_polynate_id [simp]: - assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0,field})" and np: "isnpolyh p n0" shows "polynate p = p" - using isnpolyh_unique[where ?'a= "'a::{field_char_0,field_inverse_zero}", + using isnpolyh_unique[where ?'a= "'a::{field_char_0,field}", OF polynate_norm[of p, unfolded isnpoly_def] np] - polynate[where ?'a = "'a::{field_char_0,field_inverse_zero}"] + polynate[where ?'a = "'a::{field_char_0,field}"] by simp lemma polynate_idempotent[simp]: - assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0,field})" shows "polynate (polynate p) = polynate p" using isnpolyh_polynate_id[OF polynate_norm[of p, unfolded isnpoly_def]] . @@ -1323,7 +1323,7 @@ unfolding poly_nate_def polypoly'_def .. lemma poly_nate_poly: - "poly (poly_nate bs p) = (\x:: 'a ::{field_char_0,field_inverse_zero}. \p\\<^sub>p\<^bsup>x # bs\<^esup>)" + "poly (poly_nate bs p) = (\x:: 'a ::{field_char_0,field}. \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 @@ -1362,7 +1362,7 @@ qed lemma degree_polysub_samehead: - assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0,field})" and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and h: "head p = head q" @@ -1531,7 +1531,7 @@ done lemma polymul_head_polyeq: - assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0,field})" 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 c c' n' p' n0 n1) @@ -1634,7 +1634,7 @@ by (induct p arbitrary: n0 rule: polyneg.induct) auto lemma degree_polymul: - assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0,field})" and np: "isnpolyh p n0" and nq: "isnpolyh q n1" shows "degree (p *\<^sub>p q) \ degree p + degree q" @@ -1650,7 +1650,7 @@ subsection {* Correctness of polynomial pseudo division *} lemma polydivide_aux_properties: - assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0,field})" and np: "isnpolyh p n0" and ns: "isnpolyh s n1" and ap: "head p = a" @@ -1745,24 +1745,24 @@ 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_char_0,field_inverse_zero} list. + from asp have "\bs :: 'a::{field_char_0,field} 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 - then have "\bs :: 'a::{field_char_0,field_inverse_zero} list. + then have "\bs :: 'a::{field_char_0,field} 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) - then have "\bs :: 'a::{field_char_0,field_inverse_zero} list. + then have "\bs :: 'a::{field_char_0,field} 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) - then have "\bs:: 'a::{field_char_0,field_inverse_zero} list. + then have "\bs:: 'a::{field_char_0,field} 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) - then have "\bs:: 'a::{field_char_0,field_inverse_zero} list. + then have "\bs:: 'a::{field_char_0,field} 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 @@ -1784,10 +1784,10 @@ moreover { assume spz:"s -\<^sub>p ?p' = 0\<^sub>p" - 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'" + from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::{field_char_0,field}"] + have "\bs:: 'a::{field_char_0,field} list. Ipoly bs s = Ipoly bs ?p'" by simp - then have "\bs:: 'a::{field_char_0,field_inverse_zero} list. Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)" + then have "\bs:: 'a::{field_char_0,field} list. Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)" using np nxdn apply simp apply (simp only: funpow_shift1_1) @@ -1861,7 +1861,7 @@ from kk' have kk'': "Suc (k' - Suc k) = k' - k" by arith { - fix bs :: "'a::{field_char_0,field_inverse_zero} list" + fix bs :: "'a::{field_char_0,field} 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 @@ -1875,7 +1875,7 @@ 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) } - then have ieq:"\bs :: 'a::{field_char_0,field_inverse_zero} list. + then have ieq:"\bs :: 'a::{field_char_0,field} 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 @@ -1900,7 +1900,7 @@ { assume spz: "a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p') = 0\<^sub>p" { - fix bs :: "'a::{field_char_0,field_inverse_zero} list" + fix bs :: "'a::{field_char_0,field} 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 @@ -1909,10 +1909,10 @@ then have "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" by simp } - then have hth: "\bs :: 'a::{field_char_0,field_inverse_zero} list. + then have hth: "\bs :: 'a::{field_char_0,field} 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_char_0,field_inverse_zero}", OF polymul_normh[OF head_isnpolyh[OF np] ns] + using isnpolyh_unique[where ?'a = "'a::{field_char_0,field}", 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 @@ -1945,7 +1945,7 @@ qed lemma polydivide_properties: - assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0,field})" and np: "isnpolyh p n0" and ns: "isnpolyh s n1" and pnz: "p \ 0\<^sub>p" @@ -2112,12 +2112,12 @@ lemma swapnorm: assumes nbs: "n < length bs" and mbs: "m < length bs" - shows "((Ipoly bs (swapnorm n m t) :: 'a::{field_char_0,field_inverse_zero})) = + shows "((Ipoly bs (swapnorm n m t) :: 'a::{field_char_0,field})) = Ipoly ((bs[n:= bs!m])[m:= bs!n]) t" using swap[OF assms] swapnorm_def by simp lemma swapnorm_isnpoly [simp]: - assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0,field})" shows "isnpoly (swapnorm n m p)" unfolding swapnorm_def by simp diff -r eebe69f31474 -r 58043346ca64 src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy --- a/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy Tue Mar 31 16:49:41 2015 +0100 +++ b/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy Tue Mar 31 21:54:32 2015 +0200 @@ -7,147 +7,147 @@ begin lemma - "\(y::'a::{linordered_field_inverse_zero}) <2. x + 3* y < 0 \ x - y >0" + "\(y::'a::{linordered_field}) <2. x + 3* y < 0 \ x - y >0" by ferrack -lemma "~ (ALL x (y::'a::{linordered_field_inverse_zero}). x < y --> 10*x < 11*y)" +lemma "~ (ALL x (y::'a::{linordered_field}). x < y --> 10*x < 11*y)" by ferrack -lemma "ALL (x::'a::{linordered_field_inverse_zero}) y. x < y --> (10*(x + 5*y + -1) < 60*y)" +lemma "ALL (x::'a::{linordered_field}) y. x < y --> (10*(x + 5*y + -1) < 60*y)" by ferrack -lemma "EX (x::'a::{linordered_field_inverse_zero}) y. x ~= y --> x < y" +lemma "EX (x::'a::{linordered_field}) y. x ~= y --> x < y" by ferrack -lemma "EX (x::'a::{linordered_field_inverse_zero}) y. (x ~= y & 10*x ~= 9*y & 10*x < y) --> x < y" +lemma "EX (x::'a::{linordered_field}) y. (x ~= y & 10*x ~= 9*y & 10*x < y) --> x < y" by ferrack -lemma "ALL (x::'a::{linordered_field_inverse_zero}) y. (x ~= y & 5*x <= y) --> 500*x <= 100*y" +lemma "ALL (x::'a::{linordered_field}) y. (x ~= y & 5*x <= y) --> 500*x <= 100*y" by ferrack -lemma "ALL (x::'a::{linordered_field_inverse_zero}). (EX (y::'a::{linordered_field_inverse_zero}). 4*x + 3*y <= 0 & 4*x + 3*y >= -1)" +lemma "ALL (x::'a::{linordered_field}). (EX (y::'a::{linordered_field}). 4*x + 3*y <= 0 & 4*x + 3*y >= -1)" by ferrack -lemma "ALL (x::'a::{linordered_field_inverse_zero}) < 0. (EX (y::'a::{linordered_field_inverse_zero}) > 0. 7*x + y > 0 & x - y <= 9)" +lemma "ALL (x::'a::{linordered_field}) < 0. (EX (y::'a::{linordered_field}) > 0. 7*x + y > 0 & x - y <= 9)" by ferrack -lemma "EX (x::'a::{linordered_field_inverse_zero}). (0 < x & x < 1) --> (ALL y > 1. x + y ~= 1)" +lemma "EX (x::'a::{linordered_field}). (0 < x & x < 1) --> (ALL y > 1. x + y ~= 1)" by ferrack -lemma "EX x. (ALL (y::'a::{linordered_field_inverse_zero}). y < 2 --> 2*(y - x) \ 0 )" +lemma "EX x. (ALL (y::'a::{linordered_field}). y < 2 --> 2*(y - x) \ 0 )" by ferrack -lemma "ALL (x::'a::{linordered_field_inverse_zero}). x < 10 | x > 20 | (EX y. y>= 0 & y <= 10 & x+y = 20)" +lemma "ALL (x::'a::{linordered_field}). x < 10 | x > 20 | (EX y. y>= 0 & y <= 10 & x+y = 20)" by ferrack -lemma "ALL (x::'a::{linordered_field_inverse_zero}) y z. x + y < z --> y >= z --> x < 0" +lemma "ALL (x::'a::{linordered_field}) y z. x + y < z --> y >= z --> x < 0" by ferrack -lemma "EX (x::'a::{linordered_field_inverse_zero}) y z. x + 7*y < 5* z & 5*y >= 7*z & x < 0" +lemma "EX (x::'a::{linordered_field}) y z. x + 7*y < 5* z & 5*y >= 7*z & x < 0" by ferrack -lemma "ALL (x::'a::{linordered_field_inverse_zero}) y z. abs (x + y) <= z --> (abs z = z)" +lemma "ALL (x::'a::{linordered_field}) y z. abs (x + y) <= z --> (abs z = z)" by ferrack -lemma "EX (x::'a::{linordered_field_inverse_zero}) y z. x + 7*y - 5* z < 0 & 5*y + 7*z + 3*x < 0" +lemma "EX (x::'a::{linordered_field}) y z. x + 7*y - 5* z < 0 & 5*y + 7*z + 3*x < 0" by ferrack -lemma "ALL (x::'a::{linordered_field_inverse_zero}) 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}) 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_inverse_zero}) y. x < y --> (EX z>0. x+z = y)" +lemma "ALL (x::'a::{linordered_field}) y. x < y --> (EX z>0. x+z = y)" by ferrack -lemma "ALL (x::'a::{linordered_field_inverse_zero}) y. x < y --> (EX z>0. x+z = y)" +lemma "ALL (x::'a::{linordered_field}) y. x < y --> (EX z>0. x+z = y)" by ferrack -lemma "ALL (x::'a::{linordered_field_inverse_zero}) y. (EX z>0. abs (x - y) <= z )" +lemma "ALL (x::'a::{linordered_field}) y. (EX z>0. abs (x - y) <= z )" by ferrack -lemma "EX (x::'a::{linordered_field_inverse_zero}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))" +lemma "EX (x::'a::{linordered_field}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))" by ferrack -lemma "EX (x::'a::{linordered_field_inverse_zero}) y. (ALL z>=0. abs (3*x+7*y) <= 2*z + 1)" +lemma "EX (x::'a::{linordered_field}) y. (ALL z>=0. abs (3*x+7*y) <= 2*z + 1)" by ferrack -lemma "EX (x::'a::{linordered_field_inverse_zero}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))" +lemma "EX (x::'a::{linordered_field}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))" by ferrack -lemma "EX (x::'a::{linordered_field_inverse_zero})>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})>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_inverse_zero}). 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}). 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_inverse_zero}). (EX y > abs (23*x - 9). (ALL z > abs (3*y - 19* abs x). x+z > 2*y))" +lemma "ALL (x::'a::{linordered_field}). (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_inverse_zero}). (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}). (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_inverse_zero}). abs x < 100 & (ALL y > x. (EX z<2*y - x. 5*x - 3*y <= 7*z))" +lemma "EX (x::'a::{linordered_field}). 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_inverse_zero}) 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}) 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_inverse_zero}) y z w. 5*x + 3*z - 17*w + abs (y - 8*x + z) <= 89" +lemma "EX (x::'a::{linordered_field}) y z w. 5*x + 3*z - 17*w + abs (y - 8*x + z) <= 89" by ferrack -lemma "EX (x::'a::{linordered_field_inverse_zero}) 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}) 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_inverse_zero}) 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}) 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_inverse_zero}) y z. (EX w >= (x+y+z). w <= abs x + abs y + abs z)" +lemma "ALL (x::'a::{linordered_field}) y z. (EX w >= (x+y+z). w <= abs x + abs y + abs z)" by ferrack -lemma "~(ALL (x::'a::{linordered_field_inverse_zero}). (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}). (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_inverse_zero}) y. (EX z w. abs (x-y) = (z-w) & z*1234 < 233*x & w ~= y)" +lemma "ALL (x::'a::{linordered_field}) y. (EX z w. abs (x-y) = (z-w) & z*1234 < 233*x & w ~= y)" by ferrack -lemma "ALL (x::'a::{linordered_field_inverse_zero}). (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}). (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_inverse_zero}) y z. (ALL w >= abs (x+y+z). w >= abs x + abs y + abs z)" +lemma "EX (x::'a::{linordered_field}) 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_inverse_zero}) y. (EX w >= (x+y+z). w <= abs x + abs y + abs z))" +lemma "EX z. (ALL (x::'a::{linordered_field}) y. (EX w >= (x+y+z). w <= abs x + abs y + abs z))" by ferrack -lemma "EX z. (ALL (x::'a::{linordered_field_inverse_zero}) < abs z. (EX y w. x< y & x < z & x> w & 3*x < w + y))" +lemma "EX z. (ALL (x::'a::{linordered_field}) < abs z. (EX y w. x< y & x < z & x> w & 3*x < w + y))" by ferrack -lemma "ALL (x::'a::{linordered_field_inverse_zero}) y. (EX z. (ALL w. abs (x-y) = abs (z-w) --> z < x & w ~= y))" +lemma "ALL (x::'a::{linordered_field}) 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_inverse_zero}). (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}). (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_inverse_zero}) z. (ALL w >= 13*x - 4*z. (EX y. w >= abs x + abs y + z))" +lemma "EX (x::'a::{linordered_field}) z. (ALL w >= 13*x - 4*z. (EX y. w >= abs x + abs y + z))" by ferrack -lemma "EX (x::'a::{linordered_field_inverse_zero}). (ALL y < x. (EX z > (x+y). +lemma "EX (x::'a::{linordered_field}). (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_inverse_zero}). (ALL y. (EX z > y. +lemma "EX (x::'a::{linordered_field}). (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_inverse_zero}) 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}) 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_inverse_zero}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (y - x) < w)))" +lemma "ALL (x::'a::{linordered_field}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (y - x) < w)))" by ferrack -lemma "ALL (x::'a::{linordered_field_inverse_zero}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (x + z) < w - y)))" +lemma "ALL (x::'a::{linordered_field}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (x + z) < w - y)))" by ferrack -lemma "ALL (x::'a::{linordered_field_inverse_zero}). (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}). (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 eebe69f31474 -r 58043346ca64 src/HOL/Deriv.thy --- a/src/HOL/Deriv.thy Tue Mar 31 16:49:41 2015 +0100 +++ b/src/HOL/Deriv.thy Tue Mar 31 21:54:32 2015 +0200 @@ -698,10 +698,17 @@ (auto simp: setsum_right_distrib mult_commute_abs dest: has_field_derivative_imp_has_derivative) lemma DERIV_inverse'[derivative_intros]: - "(f has_field_derivative D) (at x within s) \ f x \ 0 \ - ((\x. inverse (f x)) has_field_derivative - (inverse (f x) * D * inverse (f x))) (at x within s)" - by (rule has_derivative_imp_has_field_derivative[OF has_derivative_inverse]) - (auto dest: has_field_derivative_imp_has_derivative) + assumes "(f has_field_derivative D) (at x within s)" + and "f x \ 0" + shows "((\x. inverse (f x)) has_field_derivative - (inverse (f x) * D * inverse (f x))) (at x within s)" +proof - + have "(f has_derivative (\x. x * D)) = (f has_derivative op * D)" + by (rule arg_cong [of "\x. x * D"]) (simp add: fun_eq_iff) + with assms have "(f has_derivative (\x. x * D)) (at x within s)" + by (auto dest!: has_field_derivative_imp_has_derivative) + then show ?thesis using `f x \ 0` + by (auto intro: has_derivative_imp_has_field_derivative has_derivative_inverse) +qed text {* Power of @{text "-1"} *} diff -r eebe69f31474 -r 58043346ca64 src/HOL/Enum.thy --- a/src/HOL/Enum.thy Tue Mar 31 16:49:41 2015 +0100 +++ b/src/HOL/Enum.thy Tue Mar 31 21:54:32 2015 +0200 @@ -683,7 +683,7 @@ instance finite_2 :: complete_linorder .. -instantiation finite_2 :: "{field_inverse_zero, abs_if, ring_div, sgn_if, semiring_div}" begin +instantiation finite_2 :: "{field, abs_if, ring_div, sgn_if, semiring_div}" begin definition [simp]: "0 = a\<^sub>1" definition [simp]: "1 = a\<^sub>2" definition "x + y = (case (x, y) of (a\<^sub>1, a\<^sub>1) \ a\<^sub>1 | (a\<^sub>2, a\<^sub>2) \ a\<^sub>1 | _ \ a\<^sub>2)" @@ -807,7 +807,7 @@ instance finite_3 :: complete_linorder .. -instantiation finite_3 :: "{field_inverse_zero, abs_if, ring_div, semiring_div, sgn_if}" begin +instantiation finite_3 :: "{field, abs_if, ring_div, semiring_div, sgn_if}" begin definition [simp]: "0 = a\<^sub>1" definition [simp]: "1 = a\<^sub>2" definition diff -r eebe69f31474 -r 58043346ca64 src/HOL/Fields.thy --- a/src/HOL/Fields.thy Tue Mar 31 16:49:41 2015 +0100 +++ b/src/HOL/Fields.thy Tue Mar 31 21:54:32 2015 +0200 @@ -56,6 +56,7 @@ assumes left_inverse [simp]: "a \ 0 \ inverse a * a = 1" assumes right_inverse [simp]: "a \ 0 \ a * inverse a = 1" assumes divide_inverse: "a / b = a * inverse b" + assumes inverse_zero [simp]: "inverse 0 = 0" begin subclass ring_1_no_zero_divisors @@ -239,12 +240,6 @@ "z \ 0 \ - (x / z) - y = (- x - y * z) / z" by (simp add: divide_diff_eq_iff[symmetric]) -end - -class division_ring_inverse_zero = division_ring + - assumes inverse_zero [simp]: "inverse 0 = 0" -begin - lemma divide_zero [simp]: "a / 0 = 0" by (simp add: divide_inverse) @@ -307,6 +302,7 @@ class field = comm_ring_1 + inverse + assumes field_inverse: "a \ 0 \ inverse a * a = 1" assumes field_divide_inverse: "a / b = a * inverse b" + assumes field_inverse_zero: "inverse 0 = 0" begin subclass division_ring @@ -318,6 +314,9 @@ next fix a b :: 'a show "a / b = a * inverse b" by (rule field_divide_inverse) +next + show "inverse 0 = 0" + by (fact field_inverse_zero) qed subclass idom .. @@ -395,15 +394,6 @@ lemma divide_minus1 [simp]: "x / - 1 = - x" using nonzero_minus_divide_right [of "1" x] by simp -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) - text{*This version builds in division by zero while also re-orienting the right-hand side.*} lemma inverse_mult_distrib [simp]: @@ -963,11 +953,6 @@ then show "t \ y" by (simp add: algebra_simps) qed -end - -class linordered_field_inverse_zero = linordered_field + field_inverse_zero -begin - lemma inverse_positive_iff_positive [simp]: "(0 < inverse a) = (0 < a)" apply (cases "a = 0", simp) diff -r eebe69f31474 -r 58043346ca64 src/HOL/Groups_Big.thy --- a/src/HOL/Groups_Big.thy Tue Mar 31 16:49:41 2015 +0100 +++ b/src/HOL/Groups_Big.thy Tue Mar 31 21:54:32 2015 +0200 @@ -1158,11 +1158,11 @@ (setprod f (A - {a})) = (if a \ A then setprod f A / f a else setprod f A)" by (induct A rule: finite_induct) (auto simp add: insert_Diff_if) -lemma (in field_inverse_zero) setprod_inversef: +lemma (in field) setprod_inversef: "finite A \ setprod (inverse \ f) A = inverse (setprod f A)" by (induct A rule: finite_induct) simp_all -lemma (in field_inverse_zero) setprod_dividef: +lemma (in field) setprod_dividef: "finite A \ (\x\A. f x / g x) = setprod f A / setprod g A" using setprod_inversef [of A g] by (simp add: divide_inverse setprod.distrib) diff -r eebe69f31474 -r 58043346ca64 src/HOL/Library/BigO.thy --- a/src/HOL/Library/BigO.thy Tue Mar 31 16:49:41 2015 +0100 +++ b/src/HOL/Library/BigO.thy Tue Mar 31 21:54:32 2015 +0200 @@ -489,7 +489,7 @@ shows "c \ 0 \ f \ O(\x. c * f x)" apply (simp add: bigo_def) apply (rule_tac x = "abs (inverse c)" in exI) - apply (simp add: abs_mult [symmetric] mult.assoc [symmetric]) + apply (simp add: abs_mult mult.assoc [symmetric]) done lemma bigo_const_mult4: @@ -519,11 +519,7 @@ apply (rule_tac x = "\y. inverse c * x y" in exI) apply (simp add: mult.assoc [symmetric] abs_mult) apply (rule_tac x = "abs (inverse c) * ca" in exI) - apply (rule allI) - apply (subst mult.assoc) - apply (rule mult_left_mono) - apply (erule spec) - apply force + apply auto done lemma bigo_const_mult6 [intro]: "(\x. c) *o O(f) \ O(f)" diff -r eebe69f31474 -r 58043346ca64 src/HOL/Library/Bit.thy --- a/src/HOL/Library/Bit.thy Tue Mar 31 16:49:41 2015 +0100 +++ b/src/HOL/Library/Bit.thy Tue Mar 31 21:54:32 2015 +0200 @@ -98,7 +98,7 @@ subsection {* Type @{typ bit} forms a field *} -instantiation bit :: field_inverse_zero +instantiation bit :: field begin definition plus_bit_def: diff -r eebe69f31474 -r 58043346ca64 src/HOL/Library/Formal_Power_Series.thy --- a/src/HOL/Library/Formal_Power_Series.thy Tue Mar 31 16:49:41 2015 +0100 +++ b/src/HOL/Library/Formal_Power_Series.thy Tue Mar 31 21:54:32 2015 +0200 @@ -3628,7 +3628,7 @@ subsection {* Hypergeometric series *} -definition "F as bs (c::'a::{field_char_0,field_inverse_zero}) = +definition "F as bs (c::'a::{field_char_0,field}) = Abs_fps (\n. (foldl (\r a. r* pochhammer a n) 1 as * c^n) / (foldl (\r b. r * pochhammer b n) 1 bs * of_nat (fact n)))" @@ -3711,11 +3711,11 @@ by (simp add: fps_eq_iff fps_integral_def) lemma F_minus_nat: - "F [- of_nat n] [- of_nat (n + m)] (c::'a::{field_char_0,field_inverse_zero}) $ k = + "F [- of_nat n] [- of_nat (n + m)] (c::'a::{field_char_0,field}) $ k = (if k \ n then pochhammer (- of_nat n) k * c ^ k / (pochhammer (- of_nat (n + m)) k * of_nat (fact k)) else 0)" - "F [- of_nat m] [- of_nat (m + n)] (c::'a::{field_char_0,field_inverse_zero}) $ k = + "F [- of_nat m] [- of_nat (m + n)] (c::'a::{field_char_0,field}) $ k = (if k \ m then pochhammer (- of_nat m) k * c ^ k / (pochhammer (- of_nat (m + n)) k * of_nat (fact k)) else 0)" diff -r eebe69f31474 -r 58043346ca64 src/HOL/Library/Fraction_Field.thy --- a/src/HOL/Library/Fraction_Field.thy Tue Mar 31 16:49:41 2015 +0100 +++ b/src/HOL/Library/Fraction_Field.thy Tue Mar 31 21:54:32 2015 +0200 @@ -224,7 +224,7 @@ end -instantiation fract :: (idom) field_inverse_zero +instantiation fract :: (idom) field begin definition inverse_fract_def: @@ -428,7 +428,7 @@ end -instance fract :: (linordered_idom) linordered_field_inverse_zero +instance fract :: (linordered_idom) linordered_field proof fix q r s :: "'a fract" assume "q \ r" diff -r eebe69f31474 -r 58043346ca64 src/HOL/Limits.thy --- a/src/HOL/Limits.thy Tue Mar 31 16:49:41 2015 +0100 +++ b/src/HOL/Limits.thy Tue Mar 31 21:54:32 2015 +0200 @@ -1062,7 +1062,7 @@ unfolding filterlim_def at_top_to_right filtermap_filtermap .. lemma filterlim_inverse_at_infinity: - fixes x :: "_ \ 'a\{real_normed_div_algebra, division_ring_inverse_zero}" + fixes x :: "_ \ 'a\{real_normed_div_algebra, division_ring}" shows "filterlim inverse at_infinity (at (0::'a))" unfolding filterlim_at_infinity[OF order_refl] proof safe @@ -1074,7 +1074,7 @@ qed lemma filterlim_inverse_at_iff: - fixes g :: "'a \ 'b\{real_normed_div_algebra, division_ring_inverse_zero}" + fixes g :: "'a \ 'b\{real_normed_div_algebra, division_ring}" shows "(LIM x F. inverse (g x) :> at 0) \ (LIM x F. g x :> at_infinity)" unfolding filterlim_def filtermap_filtermap[symmetric] proof @@ -1099,7 +1099,7 @@ lemma at_to_infinity: - fixes x :: "'a \ {real_normed_field,field_inverse_zero}" + fixes x :: "'a \ {real_normed_field,field}" shows "(at (0::'a)) = filtermap inverse at_infinity" proof (rule antisym) have "(inverse ---> (0::'a)) at_infinity" @@ -1117,12 +1117,12 @@ qed lemma lim_at_infinity_0: - fixes l :: "'a :: {real_normed_field,field_inverse_zero}" + fixes l :: "'a :: {real_normed_field,field}" shows "(f ---> l) at_infinity \ ((f o inverse) ---> l) (at (0::'a))" by (simp add: tendsto_compose_filtermap at_to_infinity filtermap_filtermap) lemma lim_zero_infinity: - fixes l :: "'a :: {real_normed_field,field_inverse_zero}" + fixes l :: "'a :: {real_normed_field,field}" shows "((\x. f(1 / x)) ---> l) (at (0::'a)) \ (f ---> l) at_infinity" by (simp add: inverse_eq_divide lim_at_infinity_0 comp_def) @@ -1241,7 +1241,7 @@ qed lemma tendsto_divide_0: - fixes f :: "_ \ 'a\{real_normed_div_algebra, division_ring_inverse_zero}" + fixes f :: "_ \ 'a\{real_normed_div_algebra, division_ring}" assumes f: "(f ---> c) F" assumes g: "LIM x F. g x :> at_infinity" shows "((\x. f x / g x) ---> 0) F" diff -r eebe69f31474 -r 58043346ca64 src/HOL/Metis_Examples/Big_O.thy --- a/src/HOL/Metis_Examples/Big_O.thy Tue Mar 31 16:49:41 2015 +0100 +++ b/src/HOL/Metis_Examples/Big_O.thy Tue Mar 31 21:54:32 2015 +0200 @@ -333,8 +333,7 @@ also have "... <= O((\x. 1 / f x) * (f * g))" by (rule bigo_mult2) also have "(\x. 1 / f x) * (f * g) = g" - apply (simp add: func_times) - by (metis (lifting, no_types) a ext mult.commute nonzero_divide_eq_eq) + by (simp add: fun_eq_iff a) finally have "(\x. (1\'b) / f x) * h : O(g)". then have "f * ((\x. (1\'b) / f x) * h) : f *o O(g)" by auto @@ -458,8 +457,8 @@ using F3 by metis hence "$v\'a) (u\'a) SKF\<^sub>7\'a \ 'b. \inverse c\ * \g (SKF\<^sub>7 (u * v))\ \ u * (v * \f (SKF\<^sub>7 (u * v))$" by (metis mult_left_mono) - thus "\ca\'a. \x\'b. \inverse c\ * \g x\ \ ca * \f x\" - using A2 F4 by (metis mult.assoc mult_left_mono) + then show "\ca\'a. \x\'b. inverse \c\ * \g x\ \ ca * \f x\" + using A2 F4 by (metis F1 `0 < \inverse c\` linordered_field_class.sign_simps(23) mult_le_cancel_left_pos) qed lemma bigo_const_mult6 [intro]: "(\x. c) *o O(f) <= O(f)" diff -r eebe69f31474 -r 58043346ca64 src/HOL/Multivariate_Analysis/Determinants.thy --- a/src/HOL/Multivariate_Analysis/Determinants.thy Tue Mar 31 16:49:41 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Determinants.thy Tue Mar 31 21:54:32 2015 +0200 @@ -64,7 +64,7 @@ (* FIXME: In Finite_Set there is a useless further assumption *) lemma setprod_inversef: - "finite A \ setprod (inverse \ f) A = (inverse (setprod f A) :: 'a:: field_inverse_zero)" + "finite A \ setprod (inverse \ f) A = (inverse (setprod f A) :: 'a:: field)" apply (erule finite_induct) apply (simp) apply simp diff -r eebe69f31474 -r 58043346ca64 src/HOL/Multivariate_Analysis/PolyRoots.thy --- a/src/HOL/Multivariate_Analysis/PolyRoots.thy Tue Mar 31 16:49:41 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/PolyRoots.thy Tue Mar 31 21:54:32 2015 +0200 @@ -17,7 +17,7 @@ by (simp only: one_diff_power_eq [of "Suc n" x] lessThan_Suc_atMost) lemma setsum_gp0: - fixes x :: "'a::{comm_ring,division_ring_inverse_zero}" + fixes x :: "'a::{comm_ring,division_ring}" shows "(\i\n. x^i) = (if x = 1 then of_nat(n + 1) else (1 - x^Suc n) / (1 - x))" using setsum_gp_basic[of x n] by (simp add: real_of_nat_def mult.commute divide_simps) @@ -55,7 +55,7 @@ qed lemma setsum_gp: - fixes x :: "'a::{comm_ring,division_ring_inverse_zero}" + fixes x :: "'a::{comm_ring,division_ring}" shows "(\i=m..n. x^i) = (if n < m then 0 else if x = 1 then of_nat((n + 1) - m) @@ -65,14 +65,14 @@ by (metis eq_iff_diff_eq_0 mult.commute nonzero_divide_eq_eq) lemma setsum_gp_offset: - fixes x :: "'a::{comm_ring,division_ring_inverse_zero}" + fixes x :: "'a::{comm_ring,division_ring}" shows "(\i=m..m+n. x^i) = (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))" using setsum_gp [of x m "m+n"] by (auto simp: power_add algebra_simps) lemma setsum_gp_strict: - fixes x :: "'a::{comm_ring,division_ring_inverse_zero}" + fixes x :: "'a::{comm_ring,division_ring}" shows "(\i - (inverse (star_of x) * inverse (star_of x))" - using assms by (simp add: nonzero_inverse_mult_distrib [symmetric] nonzero_inverse_minus_eq [symmetric]) + using assms by simp } then show ?thesis by (simp add: nsderiv_def) qed diff -r eebe69f31474 -r 58043346ca64 src/HOL/NSA/HyperDef.thy --- a/src/HOL/NSA/HyperDef.thy Tue Mar 31 16:49:41 2015 +0100 +++ b/src/HOL/NSA/HyperDef.thy Tue Mar 31 21:54:32 2015 +0200 @@ -140,12 +140,12 @@ lemma of_hypreal_inverse [simp]: "\x. of_hypreal (inverse x) = - inverse (of_hypreal x :: 'a::{real_div_algebra, division_ring_inverse_zero} star)" + inverse (of_hypreal x :: 'a::{real_div_algebra, division_ring} star)" by transfer (rule of_real_inverse) lemma of_hypreal_divide [simp]: "\x y. of_hypreal (x / y) = - (of_hypreal x / of_hypreal y :: 'a::{real_field, field_inverse_zero} star)" + (of_hypreal x / of_hypreal y :: 'a::{real_field, field} star)" by transfer (rule of_real_divide) lemma of_hypreal_eq_iff [simp]: @@ -445,7 +445,7 @@ by transfer (rule field_power_not_zero) lemma hyperpow_inverse: - "\r n. r \ (0::'a::field_inverse_zero star) + "\r n. r \ (0::'a::field star) \ inverse (r pow n) = (inverse r) pow n" by transfer (rule power_inverse) diff -r eebe69f31474 -r 58043346ca64 src/HOL/NSA/NSA.thy --- a/src/HOL/NSA/NSA.thy Tue Mar 31 16:49:41 2015 +0100 +++ b/src/HOL/NSA/NSA.thy Tue Mar 31 21:54:32 2015 +0200 @@ -145,12 +145,12 @@ by transfer (rule nonzero_norm_inverse) lemma hnorm_inverse: - "\a::'a::{real_normed_div_algebra, division_ring_inverse_zero} star. + "\a::'a::{real_normed_div_algebra, division_ring} star. hnorm (inverse a) = inverse (hnorm a)" by transfer (rule norm_inverse) lemma hnorm_divide: - "\a b::'a::{real_normed_field, field_inverse_zero} star. + "\a b::'a::{real_normed_field, field} star. hnorm (a / b) = hnorm a / hnorm b" by transfer (rule norm_divide) diff -r eebe69f31474 -r 58043346ca64 src/HOL/NSA/StarDef.thy --- a/src/HOL/NSA/StarDef.thy Tue Mar 31 16:49:41 2015 +0100 +++ b/src/HOL/NSA/StarDef.thy Tue Mar 31 21:54:32 2015 +0200 @@ -881,20 +881,14 @@ apply (transfer, erule left_inverse) apply (transfer, erule right_inverse) apply (transfer, fact divide_inverse) +apply (transfer, fact inverse_zero) done -instance star :: (division_ring_inverse_zero) division_ring_inverse_zero -by (intro_classes, transfer, rule inverse_zero) - instance star :: (field) field apply (intro_classes) apply (transfer, erule left_inverse) apply (transfer, rule divide_inverse) -done - -instance star :: (field_inverse_zero) field_inverse_zero -apply intro_classes -apply (rule inverse_zero) +apply (transfer, fact inverse_zero) done instance star :: (ordered_semiring) ordered_semiring @@ -937,7 +931,6 @@ instance star :: (linordered_idom) linordered_idom .. instance star :: (linordered_field) linordered_field .. -instance star :: (linordered_field_inverse_zero) linordered_field_inverse_zero .. subsection {* Power *} diff -r eebe69f31474 -r 58043346ca64 src/HOL/Num.thy --- a/src/HOL/Num.thy Tue Mar 31 16:49:41 2015 +0100 +++ b/src/HOL/Num.thy Tue Mar 31 21:54:32 2015 +0200 @@ -1075,7 +1075,7 @@ subsection {* Particular lemmas concerning @{term 2} *} -context linordered_field_inverse_zero +context linordered_field begin lemma half_gt_zero_iff: diff -r eebe69f31474 -r 58043346ca64 src/HOL/Numeral_Simprocs.thy --- a/src/HOL/Numeral_Simprocs.thy Tue Mar 31 16:49:41 2015 +0100 +++ b/src/HOL/Numeral_Simprocs.thy Tue Mar 31 21:54:32 2015 +0200 @@ -115,8 +115,8 @@ {* fn phi => Numeral_Simprocs.combine_numerals *} simproc_setup field_combine_numerals - ("(i::'a::{field_inverse_zero,ring_char_0}) + j" - |"(i::'a::{field_inverse_zero,ring_char_0}) - j") = + ("(i::'a::{field,ring_char_0}) + j" + |"(i::'a::{field,ring_char_0}) - j") = {* fn phi => Numeral_Simprocs.field_combine_numerals *} simproc_setup inteq_cancel_numerals @@ -174,9 +174,9 @@ {* fn phi => Numeral_Simprocs.div_cancel_numeral_factor *} simproc_setup divide_cancel_numeral_factor - ("((l::'a::{field_inverse_zero,ring_char_0}) * m) / n" - |"(l::'a::{field_inverse_zero,ring_char_0}) / (m * n)" - |"((numeral v)::'a::{field_inverse_zero,ring_char_0}) / (numeral w)") = + ("((l::'a::{field,ring_char_0}) * m) / n" + |"(l::'a::{field,ring_char_0}) / (m * n)" + |"((numeral v)::'a::{field,ring_char_0}) / (numeral w)") = {* fn phi => Numeral_Simprocs.divide_cancel_numeral_factor *} simproc_setup ring_eq_cancel_factor @@ -209,8 +209,8 @@ {* fn phi => Numeral_Simprocs.dvd_cancel_factor *} simproc_setup divide_cancel_factor - ("((l::'a::field_inverse_zero) * m) / n" - |"(l::'a::field_inverse_zero) / (m * n)") = + ("((l::'a::field) * m) / n" + |"(l::'a::field) / (m * n)") = {* fn phi => Numeral_Simprocs.divide_cancel_factor *} ML_file "Tools/nat_numeral_simprocs.ML" diff -r eebe69f31474 -r 58043346ca64 src/HOL/Power.thy --- a/src/HOL/Power.thy Tue Mar 31 16:49:41 2015 +0100 +++ b/src/HOL/Power.thy Tue Mar 31 21:54:32 2015 +0200 @@ -705,7 +705,7 @@ text{*Perhaps these should be simprules.*} lemma power_inverse: - fixes a :: "'a::division_ring_inverse_zero" + fixes a :: "'a::division_ring" shows "inverse (a ^ n) = inverse a ^ n" apply (cases "a = 0") apply (simp add: power_0_left) @@ -713,11 +713,11 @@ done (* TODO: reorient or rename to inverse_power *) lemma power_one_over: - "1 / (a::'a::{field_inverse_zero, power}) ^ n = (1 / a) ^ n" + "1 / (a::'a::{field, power}) ^ n = (1 / a) ^ n" by (simp add: divide_inverse) (rule power_inverse) lemma power_divide [field_simps, divide_simps]: - "(a / b) ^ n = (a::'a::field_inverse_zero) ^ n / b ^ n" + "(a / b) ^ n = (a::'a::field) ^ n / b ^ n" apply (cases "b = 0") apply (simp add: power_0_left) apply (rule nonzero_power_divide) diff -r eebe69f31474 -r 58043346ca64 src/HOL/Probability/Bochner_Integration.thy --- a/src/HOL/Probability/Bochner_Integration.thy Tue Mar 31 16:49:41 2015 +0100 +++ b/src/HOL/Probability/Bochner_Integration.thy Tue Mar 31 21:54:32 2015 +0200 @@ -676,7 +676,7 @@ has_bochner_integral_bounded_linear[OF bounded_linear_divide] lemma has_bochner_integral_divide_zero[intro]: - fixes c :: "_::{real_normed_field, field_inverse_zero, second_countable_topology}" + fixes c :: "_::{real_normed_field, field, second_countable_topology}" shows "(c \ 0 \ has_bochner_integral M f x) \ has_bochner_integral M (\x. f x / c) (x / c)" using has_bochner_integral_divide by (cases "c = 0") auto @@ -990,7 +990,7 @@ unfolding integrable.simps by fastforce lemma integrable_divide_zero[simp, intro]: - fixes c :: "_::{real_normed_field, field_inverse_zero, second_countable_topology}" + fixes c :: "_::{real_normed_field, field, second_countable_topology}" shows "(c \ 0 \ integrable M f) \ integrable M (\x. f x / c)" unfolding integrable.simps by fastforce @@ -1098,7 +1098,7 @@ by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_inner_right) lemma integral_divide_zero[simp]: - fixes c :: "_::{real_normed_field, field_inverse_zero, second_countable_topology}" + fixes c :: "_::{real_normed_field, field, second_countable_topology}" shows "integral\<^sup>L M (\x. f x / c) = integral\<^sup>L M f / c" by (rule integral_bounded_linear'[OF bounded_linear_divide bounded_linear_mult_left[of c]]) simp diff -r eebe69f31474 -r 58043346ca64 src/HOL/Probability/Interval_Integral.thy --- a/src/HOL/Probability/Interval_Integral.thy Tue Mar 31 16:49:41 2015 +0100 +++ b/src/HOL/Probability/Interval_Integral.thy Tue Mar 31 21:54:32 2015 +0200 @@ -220,7 +220,7 @@ by (simp add: interval_lebesgue_integrable_def) lemma interval_lebesgue_integrable_divide [intro, simp]: - fixes M a b c and f :: "real \ 'a::{banach, real_normed_field, field_inverse_zero, second_countable_topology}" + fixes M a b c and f :: "real \ 'a::{banach, real_normed_field, field, second_countable_topology}" shows "(c \ 0 \ interval_lebesgue_integrable M a b f) \ interval_lebesgue_integrable M a b (\x. f x / c)" by (simp add: interval_lebesgue_integrable_def) @@ -238,7 +238,7 @@ by (simp add: interval_lebesgue_integral_def) lemma interval_lebesgue_integral_divide [simp]: - fixes M a b c and f :: "real \ 'a::{banach, real_normed_field, field_inverse_zero, second_countable_topology}" + fixes M a b c and f :: "real \ 'a::{banach, real_normed_field, field, second_countable_topology}" shows "interval_lebesgue_integral M a b (\x. f x / c) = interval_lebesgue_integral M a b f / c" by (simp add: interval_lebesgue_integral_def) diff -r eebe69f31474 -r 58043346ca64 src/HOL/Probability/Set_Integral.thy --- a/src/HOL/Probability/Set_Integral.thy Tue Mar 31 16:49:41 2015 +0100 +++ b/src/HOL/Probability/Set_Integral.thy Tue Mar 31 21:54:32 2015 +0200 @@ -125,7 +125,7 @@ by (subst integral_mult_left_zero[symmetric]) (auto intro!: integral_cong) lemma set_integral_divide_zero [simp]: - fixes a :: "'a::{real_normed_field, field_inverse_zero, second_countable_topology}" + fixes a :: "'a::{real_normed_field, field, second_countable_topology}" shows "LINT t:A|M. f t / a = (LINT t:A|M. f t) / a" by (subst integral_divide_zero[symmetric], intro integral_cong) (auto split: split_indicator) @@ -150,7 +150,7 @@ using integrable_mult_left[of a M "\x. indicator A x *\<^sub>R f x"] by simp lemma set_integrable_divide [simp, intro]: - fixes a :: "'a::{real_normed_field, field_inverse_zero, second_countable_topology}" + fixes a :: "'a::{real_normed_field, field, second_countable_topology}" assumes "a \ 0 \ set_integrable M A f" shows "set_integrable M A (\t. f t / a)" proof - diff -r eebe69f31474 -r 58043346ca64 src/HOL/Quotient_Examples/Quotient_Rat.thy --- a/src/HOL/Quotient_Examples/Quotient_Rat.thy Tue Mar 31 16:49:41 2015 +0100 +++ b/src/HOL/Quotient_Examples/Quotient_Rat.thy Tue Mar 31 21:54:32 2015 +0200 @@ -161,7 +161,7 @@ apply auto done -instantiation rat :: field_inverse_zero begin +instantiation rat :: field begin fun rat_inverse_raw where "rat_inverse_raw (a :: int, b :: int) = (if a = 0 then (0, 1) else (b, a))" diff -r eebe69f31474 -r 58043346ca64 src/HOL/Rat.thy --- a/src/HOL/Rat.thy Tue Mar 31 16:49:41 2015 +0100 +++ b/src/HOL/Rat.thy Tue Mar 31 21:54:32 2015 +0200 @@ -101,7 +101,7 @@ shows "P q" using assms by (cases q) simp -instantiation rat :: field_inverse_zero +instantiation rat :: field begin lift_definition zero_rat :: "rat" is "(0, 1)" @@ -441,7 +441,7 @@ "\ positive x \ x \ 0 \ positive (- x)" by transfer (force simp: neq_iff zero_less_mult_iff mult_less_0_iff) -instantiation rat :: linordered_field_inverse_zero +instantiation rat :: linordered_field begin definition @@ -689,7 +689,7 @@ done lemma of_rat_inverse: - "(of_rat (inverse a)::'a::{field_char_0, field_inverse_zero}) = + "(of_rat (inverse a)::'a::{field_char_0, field}) = inverse (of_rat a)" by (cases "a = 0", simp_all add: nonzero_of_rat_inverse) @@ -698,7 +698,7 @@ by (simp add: divide_inverse of_rat_mult nonzero_of_rat_inverse) lemma of_rat_divide: - "(of_rat (a / b)::'a::{field_char_0, field_inverse_zero}) + "(of_rat (a / b)::'a::{field_char_0, field}) = of_rat a / of_rat b" by (cases "b = 0") (simp_all add: nonzero_of_rat_divide) @@ -875,7 +875,7 @@ done lemma Rats_inverse [simp]: - fixes a :: "'a::{field_char_0, field_inverse_zero}" + fixes a :: "'a::{field_char_0, field}" shows "a \ Rats \ inverse a \ Rats" apply (auto simp add: Rats_def) apply (rule range_eqI) @@ -891,7 +891,7 @@ done lemma Rats_divide [simp]: - fixes a b :: "'a::{field_char_0, field_inverse_zero}" + fixes a b :: "'a::{field_char_0, field}" shows "\a \ Rats; b \ Rats\ \ a / b \ Rats" apply (auto simp add: Rats_def) apply (rule range_eqI) diff -r eebe69f31474 -r 58043346ca64 src/HOL/Real.thy --- a/src/HOL/Real.thy Tue Mar 31 16:49:41 2015 +0100 +++ b/src/HOL/Real.thy Tue Mar 31 21:54:32 2015 +0200 @@ -393,7 +393,7 @@ lemma Domainp_pcr_real [transfer_domain_rule]: "Domainp pcr_real = cauchy" by (simp add: real.domain_eq realrel_def) -instantiation real :: field_inverse_zero +instantiation real :: field begin lift_definition zero_real :: "real" is "\n. 0" @@ -575,7 +575,7 @@ apply (drule (1) cauchy_not_vanishes_cases, safe, fast, fast) done -instantiation real :: linordered_field_inverse_zero +instantiation real :: linordered_field begin definition diff -r eebe69f31474 -r 58043346ca64 src/HOL/Real_Vector_Spaces.thy --- a/src/HOL/Real_Vector_Spaces.thy Tue Mar 31 16:49:41 2015 +0100 +++ b/src/HOL/Real_Vector_Spaces.thy Tue Mar 31 21:54:32 2015 +0200 @@ -221,7 +221,7 @@ by (rule inverse_unique, simp) lemma inverse_scaleR_distrib: - fixes x :: "'a::{real_div_algebra, division_ring_inverse_zero}" + fixes x :: "'a::{real_div_algebra, division_ring}" shows "inverse (scaleR a x) = scaleR (inverse a) (inverse x)" apply (case_tac "a = 0", simp) apply (case_tac "x = 0", simp) @@ -270,7 +270,7 @@ lemma of_real_inverse [simp]: "of_real (inverse x) = - inverse (of_real x :: 'a::{real_div_algebra, division_ring_inverse_zero})" + inverse (of_real x :: 'a::{real_div_algebra, division_ring})" by (simp add: of_real_def inverse_scaleR_distrib) lemma nonzero_of_real_divide: @@ -280,7 +280,7 @@ lemma of_real_divide [simp]: "of_real (x / y) = - (of_real x / of_real y :: 'a::{real_field, field_inverse_zero})" + (of_real x / of_real y :: 'a::{real_field, field})" by (simp add: divide_inverse) lemma of_real_power [simp]: @@ -398,7 +398,7 @@ done lemma Reals_inverse: - fixes a :: "'a::{real_div_algebra, division_ring_inverse_zero}" + fixes a :: "'a::{real_div_algebra, division_ring}" shows "a \ Reals \ inverse a \ Reals" apply (auto simp add: Reals_def) apply (rule range_eqI) @@ -406,7 +406,7 @@ done lemma Reals_inverse_iff [simp]: - fixes x:: "'a :: {real_div_algebra, division_ring_inverse_zero}" + fixes x:: "'a :: {real_div_algebra, division_ring}" shows "inverse x \ \ \ x \ \" by (metis Reals_inverse inverse_inverse_eq) @@ -419,7 +419,7 @@ done lemma Reals_divide [simp]: - fixes a b :: "'a::{real_field, field_inverse_zero}" + fixes a b :: "'a::{real_field, field}" shows "\a \ Reals; b \ Reals\ \ a / b \ Reals" apply (auto simp add: Reals_def) apply (rule range_eqI) @@ -819,7 +819,7 @@ done lemma norm_inverse: - fixes a :: "'a::{real_normed_div_algebra, division_ring_inverse_zero}" + fixes a :: "'a::{real_normed_div_algebra, division_ring}" shows "norm (inverse a) = inverse (norm a)" apply (case_tac "a = 0", simp) apply (erule nonzero_norm_inverse) @@ -831,7 +831,7 @@ by (simp add: divide_inverse norm_mult nonzero_norm_inverse) lemma norm_divide: - fixes a b :: "'a::{real_normed_field, field_inverse_zero}" + fixes a b :: "'a::{real_normed_field, field}" shows "norm (a / b) = norm a / norm b" by (simp add: divide_inverse norm_mult norm_inverse) diff -r eebe69f31474 -r 58043346ca64 src/HOL/Tools/numeral_simprocs.ML --- a/src/HOL/Tools/numeral_simprocs.ML Tue Mar 31 16:49:41 2015 +0100 +++ b/src/HOL/Tools/numeral_simprocs.ML Tue Mar 31 21:54:32 2015 +0200 @@ -449,12 +449,12 @@ val field_divide_cancel_numeral_factor = [prep_simproc @{theory} ("field_divide_cancel_numeral_factor", - ["((l::'a::field_inverse_zero) * m) / n", - "(l::'a::field_inverse_zero) / (m * n)", - "((numeral v)::'a::field_inverse_zero) / (numeral w)", - "((numeral v)::'a::field_inverse_zero) / (- numeral w)", - "((- numeral v)::'a::field_inverse_zero) / (numeral w)", - "((- numeral v)::'a::field_inverse_zero) / (- numeral w)"], + ["((l::'a::field) * m) / n", + "(l::'a::field) / (m * n)", + "((numeral v)::'a::field) / (numeral w)", + "((numeral v)::'a::field) / (- numeral w)", + "((- numeral v)::'a::field) / (numeral w)", + "((- numeral v)::'a::field) / (- numeral w)"], DivideCancelNumeralFactor.proc)]; val field_cancel_numeral_factors = diff -r eebe69f31474 -r 58043346ca64 src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Tue Mar 31 16:49:41 2015 +0100 +++ b/src/HOL/Transcendental.thy Tue Mar 31 21:54:32 2015 +0200 @@ -2231,7 +2231,7 @@ lemma ln_powr_bound: "1 <= x ==> 0 < a ==> ln x <= (x powr a) / a" by (metis less_eq_real_def ln_less_self mult_imp_le_div_pos ln_powr mult.commute - order.strict_trans2 powr_gt_zero zero_less_one) + powr_gt_zero) lemma ln_powr_bound2: assumes "1 < x" and "0 < a" @@ -3109,29 +3109,29 @@ shows "cos(w) * cos(z) = (cos(w - z) + cos(w + z)) / 2" by (simp add: cos_diff cos_add) -lemma sin_plus_sin: (*FIXME field_inverse_zero should not be necessary*) - fixes w :: "'a::{real_normed_field,banach,field_inverse_zero}" +lemma sin_plus_sin: (*FIXME field should not be necessary*) + fixes w :: "'a::{real_normed_field,banach,field}" shows "sin(w) + sin(z) = 2 * sin((w + z) / 2) * cos((w - z) / 2)" apply (simp add: mult.assoc sin_times_cos) apply (simp add: field_simps) done lemma sin_diff_sin: - fixes w :: "'a::{real_normed_field,banach,field_inverse_zero}" + fixes w :: "'a::{real_normed_field,banach,field}" shows "sin(w) - sin(z) = 2 * sin((w - z) / 2) * cos((w + z) / 2)" apply (simp add: mult.assoc sin_times_cos) apply (simp add: field_simps) done lemma cos_plus_cos: - fixes w :: "'a::{real_normed_field,banach,field_inverse_zero}" + fixes w :: "'a::{real_normed_field,banach,field}" shows "cos(w) + cos(z) = 2 * cos((w + z) / 2) * cos((w - z) / 2)" apply (simp add: mult.assoc cos_times_cos) apply (simp add: field_simps) done lemma cos_diff_cos: - fixes w :: "'a::{real_normed_field,banach,field_inverse_zero}" + fixes w :: "'a::{real_normed_field,banach,field}" shows "cos(w) - cos(z) = 2 * sin((w + z) / 2) * sin((z - w) / 2)" apply (simp add: mult.assoc sin_times_sin) apply (simp add: field_simps) @@ -3671,12 +3671,12 @@ where "tan = (\x. sin x / cos x)" lemma tan_of_real: - fixes XXX :: "'a::{real_normed_field,banach,field_inverse_zero}" + fixes XXX :: "'a::{real_normed_field,banach}" shows "of_real(tan x) = (tan(of_real x) :: 'a)" by (simp add: tan_def sin_of_real cos_of_real) lemma tan_in_Reals [simp]: - fixes z :: "'a::{real_normed_field,banach,field_inverse_zero}" + fixes z :: "'a::{real_normed_field,banach}" shows "z \ \ \ tan z \ \" by (simp add: tan_def) @@ -3730,7 +3730,7 @@ qed lemma tan_half: - fixes x :: "'a::{real_normed_field,banach,field_inverse_zero}" + fixes x :: "'a::{real_normed_field,banach,field}" shows "tan x = sin (2 * x) / (cos (2 * x) + 1)" unfolding tan_def sin_double cos_double sin_squared_eq by (simp add: power2_eq_square) @@ -4137,7 +4137,7 @@ by (simp add: eq_divide_eq) lemma tan_sec: - fixes x :: "'a::{real_normed_field,banach,field_inverse_zero}" + fixes x :: "'a::{real_normed_field,banach,field}" shows "cos x \ 0 \ 1 + (tan x)\<^sup>2 = (inverse (cos x))\<^sup>2" apply (rule power_inverse [THEN subst]) apply (rule_tac c1 = "(cos x)\<^sup>2" in mult_right_cancel [THEN iffD1]) diff -r eebe69f31474 -r 58043346ca64 src/HOL/ex/Dedekind_Real.thy --- a/src/HOL/ex/Dedekind_Real.thy Tue Mar 31 16:49:41 2015 +0100 +++ b/src/HOL/ex/Dedekind_Real.thy Tue Mar 31 21:54:32 2015 +0200 @@ -1435,7 +1435,7 @@ subsection{*The Real Numbers form a Field*} -instance real :: field_inverse_zero +instance real :: field proof fix x y z :: real show "x \ 0 ==> inverse x * x = 1" by (rule real_mult_inverse_left) @@ -1574,7 +1574,7 @@ subsection{*The Reals Form an Ordered Field*} -instance real :: linordered_field_inverse_zero +instance real :: linordered_field proof fix x y z :: real show "x \ y ==> z + x \ z + y" by (rule real_add_left_mono) diff -r eebe69f31474 -r 58043346ca64 src/HOL/ex/Simproc_Tests.thy --- a/src/HOL/ex/Simproc_Tests.thy Tue Mar 31 16:49:41 2015 +0100 +++ b/src/HOL/ex/Simproc_Tests.thy Tue Mar 31 21:54:32 2015 +0200 @@ -279,7 +279,7 @@ subsection {* @{text divide_cancel_numeral_factor} *} notepad begin - fix x y z :: "'a::{field_inverse_zero,ring_char_0}" + fix x y z :: "'a::{field,ring_char_0}" { assume "(3*x) / (4*y) = z" have "(9*x) / (12 * y) = z" by (tactic {* test @{context} [@{simproc divide_cancel_numeral_factor}] *}) fact @@ -346,13 +346,13 @@ } end -lemma shows "a*(b*c)/(y*z) = d*(b::'a::linordered_field_inverse_zero)*(x*a)/z" +lemma shows "a*(b*c)/(y*z) = d*(b::'a::linordered_field)*(x*a)/z" oops -- "FIXME: need simproc to cover this case" subsection {* @{text divide_cancel_factor} *} notepad begin - fix a b c d k uu x y :: "'a::field_inverse_zero" + fix a b c d k uu x y :: "'a::field" { assume "(if k = 0 then 0 else x / y) = uu" have "(x*k) / (k*y) = uu" @@ -373,7 +373,7 @@ end lemma - fixes a b c d x y z :: "'a::linordered_field_inverse_zero" + fixes a b c d x y z :: "'a::linordered_field" shows "a*(b*c)/(y*z) = d*(b)*(x*a)/z" oops -- "FIXME: need simproc to cover this case" @@ -420,7 +420,7 @@ subsection {* @{text field_combine_numerals} *} notepad begin - fix x y z uu :: "'a::{field_inverse_zero,ring_char_0}" + fix x y z uu :: "'a::{field,ring_char_0}" { assume "5 / 6 * x = uu" have "x / 2 + x / 3 = uu" by (tactic {* test @{context} [@{simproc field_combine_numerals}] *}) fact @@ -442,7 +442,7 @@ end lemma - fixes x :: "'a::{linordered_field_inverse_zero}" + fixes x :: "'a::{linordered_field}" shows "2/3 * x + x / 3 = uu" apply (tactic {* test @{context} [@{simproc field_combine_numerals}] *})? oops -- "FIXME: test fails"