# HG changeset patch # User wenzelm # Date 1427920841 -7200 # Node ID 9d70a39d1cf30287864cf198cd4470aaf06cb455 # Parent 2d929c17828389227d611496fb4683fcff2d6ce6# Parent 6afbe5a9913942c2f676a4f92dff5b938d46eb48 merged diff -r 6afbe5a99139 -r 9d70a39d1cf3 NEWS --- a/NEWS Wed Apr 01 22:40:07 2015 +0200 +++ b/NEWS Wed Apr 01 22:40:41 2015 +0200 @@ -92,6 +92,17 @@ *** HOL *** +* Given up separate type class no_zero_divisors in favour of fully algebraic +semiring_no_zero_divisors. INCOMPATIBILITY. + +* Class linordered_semidom really requires no zero divisors. +INCOMPATIBILITY. + +* Classes division_ring, field and linordered_field always demand +`inverse 0 = 0`. Given up separate classes division_ring_inverse_zero, +field_inverse_zero and linordered_field_inverse_zero. +INCOMPATIBILITY. + * Type classes cancel_ab_semigroup_add / cancel_monoid_add specify explicit additive inverse operation. INCOMPATIBILITY. @@ -103,7 +114,7 @@ Minor INCOMPATIBILITY: type constraints may be needed. * New library of properties of the complex transcendental functions sin, cos, tan, exp, - ported from HOL Light. + Ln, Arctan, Arcsin, Arccos. Ported from HOL Light. * The factorial function, "fact", now has type "nat => 'a" (of a sort that admits numeric types including nat, int, real and complex. INCOMPATIBILITY: diff -r 6afbe5a99139 -r 9d70a39d1cf3 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Wed Apr 01 22:40:41 2015 +0200 @@ -99,16 +99,18 @@ \item Section \ref{sec:defining-datatypes}, ``Defining Datatypes,'' describes how to specify datatypes using the @{command datatype} command. -\item Section \ref{sec:defining-recursive-functions}, ``Defining Recursive -Functions,'' describes how to specify recursive functions using -@{command primrec}. +\item Section \ref{sec:defining-primitively-recursive-functions}, ``Defining +Primitively Recursive Functions,'' describes how to specify recursive functions +using @{command primrec}. (A separate tutorial @{cite "isabelle-function"} +describes the more general \keyw{fun} and \keyw{function} commands.) \item Section \ref{sec:defining-codatatypes}, ``Defining Codatatypes,'' describes how to specify codatatypes using the @{command codatatype} command. -\item Section \ref{sec:defining-corecursive-functions}, ``Defining Corecursive -Functions,'' describes how to specify corecursive functions using the -@{command primcorec} and @{command primcorecursive} commands. +\item Section \ref{sec:defining-primitively-corecursive-functions}, +``Defining Primitively Corecursive Functions,'' describes how to specify +corecursive functions using the @{command primcorec} and +@{command primcorecursive} commands. \item Section \ref{sec:registering-bounded-natural-functors}, ``Registering Bounded Natural Functors,'' explains how to use the @{command bnf} command @@ -1151,17 +1153,15 @@ *} -section {* Defining Recursive Functions - \label{sec:defining-recursive-functions} *} +section {* Defining Primitively Recursive Functions + \label{sec:defining-primitively-recursive-functions} *} text {* Recursive functions over datatypes can be specified using the @{command primrec} command, which supports primitive recursion, or using the more general -\keyw{fun} and \keyw{function} commands. In this tutorial, the focus is on -@{command primrec}; the other two commands are described in a separate -tutorial @{cite "isabelle-function"}. - -%%% TODO: partial_function +\keyw{fun}, \keyw{function}, and \keyw{partial_function} commands. In this +tutorial, the focus is on @{command primrec}; \keyw{fun} and \keyw{function} are +described in a separate tutorial @{cite "isabelle-function"}. *} @@ -1947,8 +1947,8 @@ *} -section {* Defining Corecursive Functions - \label{sec:defining-corecursive-functions} *} +section {* Defining Primitively Corecursive Functions + \label{sec:defining-primitively-corecursive-functions} *} text {* Corecursive functions can be specified using the @{command primcorec} and @@ -2085,7 +2085,11 @@ pseudorandom seed (@{text n}): *} - primcorec(*<*) (in early)(*>*) +(*<*) + context early + begin +(*>*) + primcorec random_process :: "'a stream \ (int \ int) \ int \ 'a process" where "random_process s f n = @@ -2098,6 +2102,9 @@ else Choice (random_process (every_snd s) (f \ f) (f n)) (random_process (every_snd (stl s)) (f \ f) (f (f n))))" +(*<*) + end +(*>*) text {* \noindent @@ -2300,7 +2307,7 @@ the @{const LCons} case. The condition for @{const LCons} is left implicit, as the negation of that for @{const LNil}. -For this example, the constructor view is slighlty more involved than the +For this example, the constructor view is slightly more involved than the code equation. Recall the code view version presented in Section~\ref{sssec:primcorec-simple-corecursion}. % TODO: \[{thm code_view.lappend.code}\] diff -r 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/Binomial.thy --- a/src/HOL/Binomial.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/Binomial.thy Wed Apr 01 22:40:41 2015 +0200 @@ -514,8 +514,7 @@ unfolding pochhammer_eq_0_iff by auto lemma pochhammer_minus: - assumes kn: "k \ n" - shows "pochhammer (- b) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (b - of_nat k + 1) k" + "pochhammer (- b) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (b - of_nat k + 1) k" proof (cases k) case 0 then show ?thesis by simp @@ -531,16 +530,15 @@ qed lemma pochhammer_minus': - assumes kn: "k \ n" - shows "pochhammer (b - of_nat k + 1) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (- b) k" - unfolding pochhammer_minus[OF kn, where b=b] + "pochhammer (b - of_nat k + 1) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (- b) k" + unfolding pochhammer_minus[where b=b] unfolding mult.assoc[symmetric] unfolding power_add[symmetric] by simp lemma pochhammer_same: "pochhammer (- of_nat n) n = ((- 1) ^ n :: 'a::{semiring_char_0,comm_ring_1,semiring_no_zero_divisors}) * (fact n)" - unfolding pochhammer_minus[OF le_refl[of n]] + unfolding pochhammer_minus by (simp add: of_nat_diff pochhammer_fact) @@ -551,11 +549,7 @@ (if n = 0 then 1 else (setprod (\i. a - of_nat i) {0 .. n - 1}) / (fact n))" lemma gbinomial_0 [simp]: "a gchoose 0 = 1" "0 gchoose (Suc n) = 0" - apply (simp_all add: gbinomial_def) - apply (subgoal_tac "(\i\nat\{0\nat..n}. - of_nat i) = (0::'b)") - apply (simp del:setprod_zero_iff) - apply simp - done + by (simp_all add: gbinomial_def) lemma gbinomial_pochhammer: "a gchoose n = (- 1) ^ n * pochhammer (- a) n / (fact n)" proof (cases "n = 0") @@ -723,7 +717,7 @@ Alternative definition of the binomial coefficient as @{term "\iii x" shows "(x / of_nat k :: 'a) ^ k \ x gchoose k" proof - @@ -767,7 +761,7 @@ text{*Versions of the theorems above for the natural-number version of "choose"*} lemma binomial_altdef_of_nat: fixes n k :: nat - and x :: "'a :: {field_char_0,field_inverse_zero}" --{*the point is to constrain @{typ 'a}*} + and x :: "'a :: {field_char_0,field}" --{*the point is to constrain @{typ 'a}*} assumes "k \ n" shows "of_nat (n choose k) = (\i n" shows "(of_nat n / of_nat k :: 'a) ^ k \ of_nat (n choose k)" by (simp add: assms gbinomial_ge_n_over_k_pow_k binomial_gbinomial of_nat_diff) diff -r 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/Complex.thy --- a/src/HOL/Complex.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/Complex.thy Wed Apr 01 22:40:41 2015 +0200 @@ -55,7 +55,7 @@ subsection {* Multiplication and Division *} -instantiation complex :: field_inverse_zero +instantiation complex :: field begin primcorec one_complex where @@ -93,10 +93,10 @@ lemma Im_power2: "Im (x ^ 2) = 2 * Re x * Im x" by (simp add: power2_eq_square) -lemma Re_power_real: "Im x = 0 \ Re (x ^ n) = Re x ^ n " +lemma Re_power_real [simp]: "Im x = 0 \ Re (x ^ n) = Re x ^ n " by (induct n) simp_all -lemma Im_power_real: "Im x = 0 \ Im (x ^ n) = 0" +lemma Im_power_real [simp]: "Im x = 0 \ Im (x ^ n) = 0" by (induct n) simp_all subsection {* Scalar Multiplication *} @@ -823,6 +823,9 @@ lemma csqrt_of_real_nonpos [simp]: "Im x = 0 \ Re x \ 0 \ csqrt x = \ * sqrt \Re x\" by (simp add: complex_eq_iff norm_complex_def) +lemma of_real_sqrt: "x \ 0 \ of_real (sqrt x) = csqrt (of_real x)" + by (simp add: complex_eq_iff norm_complex_def) + lemma csqrt_0 [simp]: "csqrt 0 = 0" by simp diff -r 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Wed Apr 01 22:40:41 2015 +0200 @@ -30,7 +30,7 @@ | "tmsize (CNP n c a) = 3 + polysize c + tmsize a " (* Semantics of terms tm *) -primrec Itm :: "'a::{field_char_0, field_inverse_zero} list \ 'a list \ tm \ 'a" +primrec Itm :: "'a::{field_char_0, field} list \ 'a list \ tm \ 'a" where "Itm vs bs (CP c) = (Ipoly vs c)" | "Itm vs bs (Bound n) = bs!n" @@ -311,7 +311,7 @@ by (induct t arbitrary: i rule: tmmul.induct) (auto simp add: Let_def) lemma tmmul_allpolys_npoly[simp]: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field})" shows "allpolys isnpoly t \ isnpoly c \ allpolys isnpoly (tmmul t c)" by (induct t rule: tmmul.induct) (simp_all add: Let_def polymul_norm) @@ -337,7 +337,7 @@ unfolding isnpoly_def by simp lemma tmneg_allpolys_npoly[simp]: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field})" shows "allpolys isnpoly t \ allpolys isnpoly (tmneg t)" unfolding tmneg_def by auto @@ -354,7 +354,7 @@ using tmsub_def by simp lemma tmsub_allpolys_npoly[simp]: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field})" shows "allpolys isnpoly t \ allpolys isnpoly s \ allpolys isnpoly (tmsub t s)" unfolding tmsub_def by (simp add: isnpoly_def) @@ -371,7 +371,7 @@ (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::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field})" shows "polynate t = 0\<^sub>p \ Ipoly bs t = (0::'a)" apply (subst polynate[symmetric]) apply simp @@ -394,7 +394,7 @@ by (simp_all add: isnpoly_def) lemma simptm_allpolys_npoly[simp]: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field})" shows "allpolys isnpoly (simptm p)" by (induct p rule: simptm.induct) (auto simp add: Let_def) @@ -445,7 +445,7 @@ qed lemma split0_nb0: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field})" shows "split0 t = (c',t') \ tmbound 0 t'" proof - fix c' t' @@ -457,7 +457,7 @@ qed lemma split0_nb0'[simp]: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field})" shows "tmbound0 (snd (split0 t))" using split0_nb0[of t "fst (split0 t)" "snd (split0 t)"] by (simp add: tmbound0_tmbound_iff) @@ -485,7 +485,7 @@ by (induct p rule: split0.induct) (auto simp add: isnpoly_def Let_def split_def) lemma isnpoly_fst_split0: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field})" shows "allpolys isnpoly p \ isnpoly (fst (split0 p))" by (induct p rule: split0.induct) (auto simp add: polyadd_norm polysub_norm polyneg_norm polymul_norm Let_def split_def) @@ -514,7 +514,7 @@ by (induct p rule: fmsize.induct) simp_all (* Semantics of formulae (fm) *) -primrec Ifm ::"'a::{linordered_field_inverse_zero} list \ 'a list \ fm \ bool" +primrec Ifm ::"'a::{linordered_field} list \ 'a list \ fm \ bool" where "Ifm vs bs T = True" | "Ifm vs bs F = False" @@ -1146,7 +1146,7 @@ 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::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field})" shows "islin (simplt t)" unfolding simplt_def using split0_nb0' @@ -1154,7 +1154,7 @@ islin_stupid allpolys_split0[OF simptm_allpolys_npoly]) lemma simple_islin[simp]: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field})" shows "islin (simple t)" unfolding simple_def using split0_nb0' @@ -1162,7 +1162,7 @@ islin_stupid allpolys_split0[OF simptm_allpolys_npoly] le_lin) lemma simpeq_islin[simp]: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field})" shows "islin (simpeq t)" unfolding simpeq_def using split0_nb0' @@ -1170,7 +1170,7 @@ islin_stupid allpolys_split0[OF simptm_allpolys_npoly] eq_lin) lemma simpneq_islin[simp]: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field})" shows "islin (simpneq t)" unfolding simpneq_def using split0_nb0' @@ -1181,7 +1181,7 @@ by (cases "split0 s") auto lemma split0_npoly: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field})" and n: "allpolys isnpoly t" shows "isnpoly (fst (split0 t))" and "allpolys isnpoly (snd (split0 t))" @@ -1305,7 +1305,7 @@ done lemma simplt_nb[simp]: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field})" shows "tmbound0 t \ bound0 (simplt t)" proof (simp add: simplt_def Let_def split_def) assume nb: "tmbound0 t" @@ -1326,7 +1326,7 @@ qed lemma simple_nb[simp]: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field})" shows "tmbound0 t \ bound0 (simple t)" proof(simp add: simple_def Let_def split_def) assume nb: "tmbound0 t" @@ -1347,7 +1347,7 @@ qed lemma simpeq_nb[simp]: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field})" shows "tmbound0 t \ bound0 (simpeq t)" proof (simp add: simpeq_def Let_def split_def) assume nb: "tmbound0 t" @@ -1368,7 +1368,7 @@ qed lemma simpneq_nb[simp]: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field})" shows "tmbound0 t \ bound0 (simpneq t)" proof (simp add: simpneq_def Let_def split_def) assume nb: "tmbound0 t" @@ -1526,7 +1526,7 @@ by (induct p arbitrary: bs rule: simpfm.induct) auto lemma simpfm_bound0: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field})" shows "bound0 p \ bound0 (simpfm p)" by (induct p rule: simpfm.induct) auto @@ -1567,7 +1567,7 @@ by (simp add: conj_def) lemma - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field})" shows "qfree p \ islin (simpfm p)" by (induct p rule: simpfm.induct) (simp_all add: conj_lin disj_lin) @@ -3379,7 +3379,7 @@ qed lemma simpfm_lin: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field})" shows "qfree p \ islin (simpfm p)" by (induct p rule: simpfm.induct) (auto simp add: conj_lin disj_lin) @@ -3704,7 +3704,7 @@ (auto simp add: msubsteq2_nb msubstltpos_nb msubstlepos_nb) lemma msubstneg_nb: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field})" and lp: "islin p" and tnb: "tmbound0 t" shows "bound0 (msubstneg p c t)" @@ -3713,7 +3713,7 @@ (auto simp add: msubsteq2_nb msubstltneg_nb msubstleneg_nb) lemma msubst2_nb: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field})" and lp: "islin p" and tnb: "tmbound0 t" shows "bound0 (msubst2 p c t)" @@ -4196,7 +4196,7 @@ Parametric_Ferrante_Rackoff.method true *} "parametric QE for linear Arithmetic over fields, Version 2" -lemma "\(x::'a::{linordered_field_inverse_zero}). y \ -1 \ (y + 1) * x < 0" +lemma "\(x::'a::{linordered_field}). y \ -1 \ (y + 1) * x < 0" apply (frpar type: 'a pars: y) apply (simp add: field_simps) apply (rule spec[where x=y]) @@ -4204,7 +4204,7 @@ apply simp done -lemma "\(x::'a::{linordered_field_inverse_zero}). y \ -1 \ (y + 1)*x < 0" +lemma "\(x::'a::{linordered_field}). y \ -1 \ (y + 1)*x < 0" apply (frpar2 type: 'a pars: y) apply (simp add: field_simps) apply (rule spec[where x=y]) @@ -4214,38 +4214,38 @@ text{* Collins/Jones Problem *} (* -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" +lemma "\(r::'a::{linordered_field, number_ring}). 0 < r \ r < 1 \ 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \ (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0" proof- - 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") + have "(\(r::'a::{linordered_field, number_ring}). 0 < r \ r < 1 \ 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \ (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \ (\(r::'a::{linordered_field, number_ring}). 0 < r \ r < 1 \ 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \ 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \ ?rhs") by (simp add: field_simps) have "?rhs" - 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 (frpar type: "'a::{linordered_field, number_ring}" pars: "a::'a::{linordered_field, number_ring}" "b::'a::{linordered_field, number_ring}") apply (simp add: field_simps) oops *) (* -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}") +lemma "ALL (x::'a::{linordered_field, number_ring}) y. (1 - t)*x \ (1+t)*y \ (1 - t)*y \ (1+t)*x --> 0 \ y" +apply (frpar type: "'a::{linordered_field, number_ring}" pars: "t::'a::{linordered_field, number_ring}") oops *) text{* Collins/Jones Problem *} (* -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" +lemma "\(r::'a::{linordered_field, number_ring}). 0 < r \ r < 1 \ 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \ (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0" proof- - 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") + have "(\(r::'a::{linordered_field, number_ring}). 0 < r \ r < 1 \ 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \ (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \ (\(r::'a::{linordered_field, number_ring}). 0 < r \ r < 1 \ 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \ 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \ ?rhs") by (simp add: field_simps) have "?rhs" - 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 (frpar2 type: "'a::{linordered_field, number_ring}" pars: "a::'a::{linordered_field, number_ring}" "b::'a::{linordered_field, number_ring}") apply simp oops *) (* -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}") +lemma "ALL (x::'a::{linordered_field, number_ring}) y. (1 - t)*x \ (1+t)*y \ (1 - t)*y \ (1+t)*x --> 0 \ y" +apply (frpar2 type: "'a::{linordered_field, number_ring}" pars: "t::'a::{linordered_field, number_ring}") apply (simp add: field_simps linorder_neq_iff[symmetric]) apply ferrack oops diff -r 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/Decision_Procs/Rat_Pair.thy --- a/src/HOL/Decision_Procs/Rat_Pair.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/Decision_Procs/Rat_Pair.thy Wed Apr 01 22:40:41 2015 +0200 @@ -156,7 +156,7 @@ lemma isnormNum_unique[simp]: assumes na: "isnormNum x" and nb: "isnormNum y" - shows "((INum x ::'a::{field_char_0, field_inverse_zero}) = INum y) = (x = y)" (is "?lhs = ?rhs") + shows "((INum x ::'a::{field_char_0, field}) = INum y) = (x = y)" (is "?lhs = ?rhs") proof obtain a b where x: "x = (a, b)" by (cases x) obtain a' b' where y: "y = (a', b')" by (cases y) @@ -190,7 +190,7 @@ lemma isnormNum0[simp]: - "isnormNum x \ (INum x = (0::'a::{field_char_0, field_inverse_zero})) = (x = 0\<^sub>N)" + "isnormNum x \ (INum x = (0::'a::{field_char_0, field})) = (x = 0\<^sub>N)" unfolding INum_int(2)[symmetric] by (rule isnormNum_unique) simp_all @@ -213,7 +213,7 @@ (of_int(n div d)::'a::field_char_0) = of_int n / of_int d" using of_int_div_aux [of d n, where ?'a = 'a] by simp -lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::{field_char_0, field_inverse_zero})" +lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::{field_char_0, field})" proof - obtain a b where x: "x = (a, b)" by (cases x) { assume "a = 0 \ b = 0" @@ -228,7 +228,7 @@ qed lemma INum_normNum_iff: - "(INum x ::'a::{field_char_0, field_inverse_zero}) = INum y \ normNum x = normNum y" + "(INum x ::'a::{field_char_0, field}) = INum y \ normNum x = normNum y" (is "?lhs = ?rhs") proof - have "normNum x = normNum y \ (INum (normNum x) :: 'a) = INum (normNum y)" @@ -237,7 +237,7 @@ finally show ?thesis by simp qed -lemma Nadd[simp]: "INum (x +\<^sub>N y) = INum x + (INum y :: 'a :: {field_char_0, field_inverse_zero})" +lemma Nadd[simp]: "INum (x +\<^sub>N y) = INum x + (INum y :: 'a :: {field_char_0, field})" proof - let ?z = "0:: 'a" obtain a b where x: "x = (a, b)" by (cases x) @@ -274,7 +274,7 @@ ultimately show ?thesis by blast qed -lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * (INum y:: 'a :: {field_char_0, field_inverse_zero})" +lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * (INum y:: 'a :: {field_char_0, field})" proof - let ?z = "0::'a" obtain a b where x: "x = (a, b)" by (cases x) @@ -298,18 +298,18 @@ lemma Nneg[simp]: "INum (~\<^sub>N x) = - (INum x ::'a:: field)" by (simp add: Nneg_def split_def INum_def) -lemma Nsub[simp]: "INum (x -\<^sub>N y) = INum x - (INum y:: 'a :: {field_char_0, field_inverse_zero})" +lemma Nsub[simp]: "INum (x -\<^sub>N y) = INum x - (INum y:: 'a :: {field_char_0, field})" by (simp add: Nsub_def split_def) -lemma Ninv[simp]: "INum (Ninv x) = (1::'a :: field_inverse_zero) / (INum x)" +lemma Ninv[simp]: "INum (Ninv x) = (1::'a :: field) / (INum x)" by (simp add: Ninv_def INum_def split_def) -lemma Ndiv[simp]: "INum (x \
\<^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 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Wed Apr 01 22:40:41 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 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy --- a/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy Wed Apr 01 22:40:41 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 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/Deriv.thy --- a/src/HOL/Deriv.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/Deriv.thy Wed Apr 01 22:40:41 2015 +0200 @@ -561,6 +561,10 @@ \ (f has_field_derivative f') (at x within t)" by (simp add: has_field_derivative_def has_derivative_within_subset) +lemma has_field_derivative_at_within: + "(f has_field_derivative f') (at x) \ (f has_field_derivative f') (at x within s)" + using DERIV_subset by blast + abbreviation (input) DERIV :: "('a::real_normed_field \ 'a) \ 'a \ 'a \ bool" ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) @@ -694,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 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/Enum.thy --- a/src/HOL/Enum.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/Enum.thy Wed Apr 01 22:40:41 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 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/Fields.thy --- a/src/HOL/Fields.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/Fields.thy Wed Apr 01 22:40:41 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 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/Groups_Big.thy --- a/src/HOL/Groups_Big.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/Groups_Big.thy Wed Apr 01 22:40:41 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 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/HOL.thy Wed Apr 01 22:40:41 2015 +0200 @@ -1264,6 +1264,12 @@ then show "PROP P" . qed +lemma implies_True_equals: "(PROP P \ True) \ Trueprop True" +by default (intro TrueI) + +lemma False_implies_equals: "(False \ P) \ Trueprop True" +by default simp_all + lemma ex_simps: "!!P Q. (EX x. P x & Q) = ((EX x. P x) & Q)" "!!P Q. (EX x. P & Q x) = (P & (EX x. Q x))" diff -r 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/Library/BigO.thy --- a/src/HOL/Library/BigO.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/Library/BigO.thy Wed Apr 01 22:40:41 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 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/Library/Bit.thy --- a/src/HOL/Library/Bit.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/Library/Bit.thy Wed Apr 01 22:40:41 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 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/Library/ContNotDenum.thy --- a/src/HOL/Library/ContNotDenum.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/Library/ContNotDenum.thy Wed Apr 01 22:40:41 2015 +0200 @@ -110,7 +110,7 @@ qed lemma bij_betw_tan: "bij_betw tan {-pi/2<.. 0" using c by (simp add: pochhammer_eq_0_iff) @@ -3630,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)))" @@ -3713,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)" @@ -3794,8 +3792,9 @@ with LIMSEQ_inverse_realpow_zero[of 2, simplified, simplified filterlim_iff, THEN spec, of "\x. x < e"] have "eventually (\i. inverse (2 ^ i) < e) sequentially" + unfolding eventually_nhds apply safe - apply (auto simp: eventually_nhds) --{*slow*} + apply auto --{*slow*} done then obtain i where "inverse (2 ^ i) < e" by (auto simp: eventually_sequentially) have "eventually (\x. M i \ x) sequentially" by (auto simp: eventually_sequentially) diff -r 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/Library/Fraction_Field.thy --- a/src/HOL/Library/Fraction_Field.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/Library/Fraction_Field.thy Wed Apr 01 22:40:41 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 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/Limits.thy --- a/src/HOL/Limits.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/Limits.thy Wed Apr 01 22:40:41 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 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/Metis_Examples/Big_O.thy --- a/src/HOL/Metis_Examples/Big_O.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/Metis_Examples/Big_O.thy Wed Apr 01 22:40:41 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 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy --- a/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy Wed Apr 01 22:40:41 2015 +0200 @@ -407,7 +407,7 @@ hence "(\i\Basis. (dist (clamp a b y \ i) (clamp a b x \ i))\<^sup>2) \ (\i\Basis. (dist (y \ i) (x \ i))\<^sup>2)" by (auto intro!: setsum_mono - simp add: clamp_def dist_real_def real_abs_le_square_iff[symmetric]) + simp add: clamp_def dist_real_def abs_le_square_iff[symmetric]) thus ?thesis by (auto intro: real_sqrt_le_mono simp add: euclidean_dist_l2[where y=x] euclidean_dist_l2[where y="clamp a b x"] setL2_def) diff -r 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/Multivariate_Analysis/Complex_Transcendental.thy --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Wed Apr 01 22:40:41 2015 +0200 @@ -8,6 +8,39 @@ imports "~~/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics" begin + +lemma cmod_add_real_less: + assumes "Im z \ 0" "r\0" + shows "cmod (z + r) < cmod z + abs r" +proof (cases z) + case (Complex x y) + have "r * x / \r\ < sqrt (x*x + y*y)" + apply (rule real_less_rsqrt) + using assms + apply (simp add: Complex power2_eq_square) + using not_real_square_gt_zero by blast + then show ?thesis using assms Complex + apply (auto simp: cmod_def) + apply (rule power2_less_imp_less, auto) + apply (simp add: power2_eq_square field_simps) + done +qed + +lemma cmod_diff_real_less: "Im z \ 0 \ x\0 \ cmod (z - x) < cmod z + abs x" + using cmod_add_real_less [of z "-x"] + by simp + +lemma cmod_square_less_1_plus: + assumes "Im z = 0 \ \Re z\ < 1" + shows "(cmod z)\<^sup>2 < 1 + cmod (1 - z\<^sup>2)" + using assms + apply (cases "Im z = 0 \ Re z = 0") + using abs_square_less_1 + apply (force simp add: Re_power2 Im_power2 cmod_def) + using cmod_diff_real_less [of "1 - z\<^sup>2" "1"] + apply (simp add: norm_power Im_power2) + done + subsection{*The Exponential Function is Differentiable and Continuous*} lemma complex_differentiable_at_exp: "exp complex_differentiable at z" @@ -42,7 +75,7 @@ theorem exp_Euler: "exp(ii * z) = cos(z) + ii * sin(z)" proof - - have "(\n. (cos_coeff n + ii * sin_coeff n) * z^n) + have "(\n. (cos_coeff n + ii * sin_coeff n) * z^n) = (\n. (ii * z) ^ n /\<^sub>R (fact n))" proof fix n @@ -74,13 +107,11 @@ subsection{*Relationships between real and complex trig functions*} -declare sin_of_real [simp] cos_of_real [simp] - lemma real_sin_eq [simp]: fixes x::real shows "Re(sin(of_real x)) = sin x" by (simp add: sin_of_real) - + lemma real_cos_eq [simp]: fixes x::real shows "Re(cos(of_real x)) = cos x" @@ -100,10 +131,10 @@ by (rule exp_converges) finally have "(\n. cnj (z ^ n /\<^sub>R (fact n))) sums (exp (cnj z))" . moreover have "(\n. cnj (z ^ n /\<^sub>R (fact n))) sums (cnj (exp z))" - by (metis exp_converges sums_cnj) + by (metis exp_converges sums_cnj) ultimately show ?thesis using sums_unique2 - by blast + by blast qed lemma cnj_sin: "cnj(sin z) = sin(cnj z)" @@ -112,15 +143,6 @@ lemma cnj_cos: "cnj(cos z) = cos(cnj z)" by (simp add: cos_exp_eq exp_cnj field_simps) -lemma exp_in_Reals [simp]: "z \ \ \ exp z \ \" - by (metis Reals_cases Reals_of_real exp_of_real) - -lemma sin_in_Reals [simp]: "z \ \ \ sin z \ \" - by (metis Reals_cases Reals_of_real sin_of_real) - -lemma cos_in_Reals [simp]: "z \ \ \ cos z \ \" - by (metis Reals_cases Reals_of_real cos_of_real) - lemma complex_differentiable_at_sin: "sin complex_differentiable at z" using DERIV_sin complex_differentiable_def by blast @@ -141,7 +163,7 @@ subsection{* Get a nice real/imaginary separation in Euler's formula.*} -lemma Euler: "exp(z) = of_real(exp(Re z)) * +lemma Euler: "exp(z) = of_real(exp(Re z)) * (of_real(cos(Im z)) + ii * of_real(sin(Im z)))" by (cases z) (simp add: exp_add exp_Euler cos_of_real exp_of_real sin_of_real) @@ -156,11 +178,20 @@ lemma Im_cos: "Im(cos z) = sin(Re z) * (exp(-(Im z)) - exp(Im z)) / 2" by (simp add: cos_exp_eq field_simps Im_divide Im_exp) - + +lemma Re_sin_pos: "0 < Re z \ Re z < pi \ Re (sin z) > 0" + by (auto simp: Re_sin Im_sin add_pos_pos sin_gt_zero) + +lemma Im_sin_nonneg: "Re z = 0 \ 0 \ Im z \ 0 \ Im (sin z)" + by (simp add: Re_sin Im_sin algebra_simps) + +lemma Im_sin_nonneg2: "Re z = pi \ Im z \ 0 \ 0 \ Im (sin z)" + by (simp add: Re_sin Im_sin algebra_simps) + subsection{*More on the Polar Representation of Complex Numbers*} lemma exp_Complex: "exp(Complex r t) = of_real(exp r) * Complex (cos t) (sin t)" - by (simp add: exp_add exp_Euler exp_of_real) + by (simp add: exp_add exp_Euler exp_of_real sin_of_real cos_of_real) lemma exp_eq_1: "exp z = 1 \ Re(z) = 0 \ (\n::int. Im(z) = of_int (2 * n) * pi)" apply auto @@ -183,7 +214,7 @@ lemma exp_complex_eqI: "abs(Im w - Im z) < 2*pi \ exp w = exp z \ w = z" by (auto simp: exp_eq abs_mult) -lemma exp_integer_2pi: +lemma exp_integer_2pi: assumes "n \ Ints" shows "exp((2 * n * pi) * ii) = 1" proof - @@ -208,10 +239,10 @@ done qed -lemma exp_i_ne_1: +lemma exp_i_ne_1: assumes "0 < x" "x < 2*pi" shows "exp(\ * of_real x) \ 1" -proof +proof assume "exp (\ * of_real x) = 1" then have "exp (\ * of_real x) = exp 0" by simp @@ -225,18 +256,18 @@ by (cases n) (auto simp: zero_less_mult_iff mult_less_0_iff) qed -lemma sin_eq_0: +lemma sin_eq_0: fixes z::complex shows "sin z = 0 \ (\n::int. z = of_real(n * pi))" by (simp add: sin_exp_eq exp_eq of_real_numeral) -lemma cos_eq_0: +lemma cos_eq_0: fixes z::complex shows "cos z = 0 \ (\n::int. z = of_real(n * pi) + of_real pi/2)" using sin_eq_0 [of "z - of_real pi/2"] by (simp add: sin_diff algebra_simps) -lemma cos_eq_1: +lemma cos_eq_1: fixes z::complex shows "cos z = 1 \ (\n::int. z = of_real(2 * n * pi))" proof - @@ -248,7 +279,7 @@ by simp show ?thesis by (auto simp: sin_eq_0 of_real_numeral) -qed +qed lemma csin_eq_1: fixes z::complex @@ -275,15 +306,15 @@ apply (simp_all add: algebra_simps) done finally show ?thesis . -qed +qed -lemma ccos_eq_minus1: +lemma ccos_eq_minus1: fixes z::complex shows "cos z = -1 \ (\n::int. z = of_real(2 * n * pi) + pi)" using csin_eq_1 [of "z - of_real pi/2"] apply (simp add: sin_diff) apply (simp add: algebra_simps of_real_numeral equation_minus_iff) - done + done lemma sin_eq_1: "sin x = 1 \ (\n::int. x = (2 * n + 1 / 2) * pi)" (is "_ = ?rhs") @@ -301,7 +332,7 @@ also have "... = ?rhs" by (auto simp: algebra_simps) finally show ?thesis . -qed +qed lemma sin_eq_minus1: "sin x = -1 \ (\n::int. x = (2*n + 3/2) * pi)" (is "_ = ?rhs") proof - @@ -317,7 +348,7 @@ also have "... = ?rhs" by (auto simp: algebra_simps) finally show ?thesis . -qed +qed lemma cos_eq_minus1: "cos x = -1 \ (\n::int. x = (2*n + 1) * pi)" (is "_ = ?rhs") @@ -334,10 +365,10 @@ also have "... = ?rhs" by (auto simp: algebra_simps) finally show ?thesis . -qed +qed lemma dist_exp_ii_1: "norm(exp(ii * of_real t) - 1) = 2 * abs(sin(t / 2))" - apply (simp add: exp_Euler cmod_def power2_diff algebra_simps) + apply (simp add: exp_Euler cmod_def power2_diff sin_of_real cos_of_real algebra_simps) using cos_double_sin [of "t/2"] apply (simp add: real_sqrt_mult) done @@ -369,7 +400,7 @@ lemmas cos_ii_times = cosh_complex [symmetric] -lemma norm_cos_squared: +lemma norm_cos_squared: "norm(cos z) ^ 2 = cos(Re z) ^ 2 + (exp(Im z) - inverse(exp(Im z))) ^ 2 / 4" apply (cases z) apply (simp add: cos_add cmod_power2 cos_of_real sin_of_real) @@ -387,12 +418,12 @@ apply (simp only: left_diff_distrib [symmetric] power_mult_distrib) apply (simp add: cos_squared_eq) apply (simp add: power2_eq_square algebra_simps divide_simps) - done + done lemma exp_uminus_Im: "exp (- Im z) \ exp (cmod z)" using abs_Im_le_cmod linear order_trans by fastforce -lemma norm_cos_le: +lemma norm_cos_le: fixes z::complex shows "norm(cos z) \ exp(norm z)" proof - @@ -405,7 +436,7 @@ done qed -lemma norm_cos_plus1_le: +lemma norm_cos_plus1_le: fixes z::complex shows "norm(1 + cos z) \ 2 * exp(norm z)" proof - @@ -431,12 +462,12 @@ subsection{* Taylor series for complex exponential, sine and cosine.*} -context +context begin declare power_Suc [simp del] -lemma Taylor_exp: +lemma Taylor_exp: "norm(exp z - (\k\n. z ^ k / (fact k))) \ exp\Re z\ * (norm z) ^ (Suc n) / (fact n)" proof (rule complex_taylor [of _ n "\k. exp" "exp\Re z\" 0 z, simplified]) show "convex (closed_segment 0 z)" @@ -459,11 +490,11 @@ show "z \ closed_segment 0 z" apply (simp add: closed_segment_def scaleR_conv_of_real) using of_real_1 zero_le_one by blast -qed +qed -lemma +lemma assumes "0 \ u" "u \ 1" - shows cmod_sin_le_exp: "cmod (sin (u *\<^sub>R z)) \ exp \Im z\" + shows cmod_sin_le_exp: "cmod (sin (u *\<^sub>R z)) \ exp \Im z\" and cmod_cos_le_exp: "cmod (cos (u *\<^sub>R z)) \ exp \Im z\" proof - have mono: "\u w z::real. w \ u \ z \ u \ w + z \ u*2" @@ -485,16 +516,16 @@ apply (meson less_eq_real_def mult_nonneg_nonpos neg_0_le_iff_le order_trans) done qed - -lemma Taylor_sin: - "norm(sin z - (\k\n. complex_of_real (sin_coeff k) * z ^ k)) + +lemma Taylor_sin: + "norm(sin z - (\k\n. complex_of_real (sin_coeff k) * z ^ k)) \ exp\Im z\ * (norm z) ^ (Suc n) / (fact n)" proof - have mono: "\u w z::real. w \ u \ z \ u \ w + z \ u*2" by arith have *: "cmod (sin z - (\i\n. (-1) ^ (i div 2) * (if even i then sin 0 else cos 0) * z ^ i / (fact i))) - \ exp \Im z\ * cmod z ^ Suc n / (fact n)" + \ exp \Im z\ * cmod z ^ Suc n / (fact n)" proof (rule complex_taylor [of "closed_segment 0 z" n "\k x. (-1)^(k div 2) * (if even k then sin x else cos x)" "exp\Im z\" 0 z, simplified]) show "convex (closed_segment 0 z)" @@ -519,7 +550,7 @@ show "z \ closed_segment 0 z" apply (simp add: closed_segment_def scaleR_conv_of_real) using of_real_1 zero_le_one by blast - qed + qed have **: "\k. complex_of_real (sin_coeff k) * z ^ k = (-1)^(k div 2) * (if even k then sin 0 else cos 0) * z^k / of_nat (fact k)" by (auto simp: sin_coeff_def elim!: oddE) @@ -529,15 +560,15 @@ done qed -lemma Taylor_cos: - "norm(cos z - (\k\n. complex_of_real (cos_coeff k) * z ^ k)) +lemma Taylor_cos: + "norm(cos z - (\k\n. complex_of_real (cos_coeff k) * z ^ k)) \ exp\Im z\ * (norm z) ^ Suc n / (fact n)" proof - have mono: "\u w z::real. w \ u \ z \ u \ w + z \ u*2" by arith have *: "cmod (cos z - (\i\n. (-1) ^ (Suc i div 2) * (if even i then cos 0 else sin 0) * z ^ i / (fact i))) - \ exp \Im z\ * cmod z ^ Suc n / (fact n)" + \ exp \Im z\ * cmod z ^ Suc n / (fact n)" proof (rule complex_taylor [of "closed_segment 0 z" n "\k x. (-1)^(Suc k div 2) * (if even k then cos x else sin x)" "exp\Im z\" 0 z, simplified]) show "convex (closed_segment 0 z)" @@ -563,7 +594,7 @@ show "z \ closed_segment 0 z" apply (simp add: closed_segment_def scaleR_conv_of_real) using of_real_1 zero_le_one by blast - qed + qed have **: "\k. complex_of_real (cos_coeff k) * z ^ k = (-1)^(Suc k div 2) * (if even k then cos 0 else sin 0) * z^k / of_nat (fact k)" by (auto simp: cos_coeff_def elim!: evenE) @@ -910,6 +941,21 @@ apply (auto simp: exp_of_nat_mult [symmetric]) done +subsection{*The Unwinding Number and the Ln-product Formula*} + +text{*Note that in this special case the unwinding number is -1, 0 or 1.*} + +definition unwinding :: "complex \ complex" where + "unwinding(z) = (z - Ln(exp z)) / (of_real(2*pi) * ii)" + +lemma unwinding_2pi: "(2*pi) * ii * unwinding(z) = z - Ln(exp z)" + by (simp add: unwinding_def) + +lemma Ln_times_unwinding: + "w \ 0 \ z \ 0 \ Ln(w * z) = Ln(w) + Ln(z) - (2*pi) * ii * unwinding(Ln w + Ln z)" + using unwinding_2pi by (simp add: exp_add) + + subsection{*Derivative of Ln away from the branch cut*} lemma @@ -944,6 +990,10 @@ lemma continuous_at_Ln: "(Im(z) = 0 \ 0 < Re(z)) \ continuous (at z) Ln" by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_Ln) +lemma isCont_Ln' [simp]: + "\isCont f z; Im(f z) = 0 \ 0 < Re(f z)\ \ isCont (\x. Ln (f x)) z" + by (blast intro: isCont_o2 [OF _ continuous_at_Ln]) + lemma continuous_within_Ln: "(Im(z) = 0 \ 0 < Re(z)) \ continuous (at z within s) Ln" using continuous_at_Ln continuous_at_imp_continuous_within by blast @@ -956,7 +1006,7 @@ subsection{*Relation to Real Logarithm*} -lemma ln_of_real: +lemma Ln_of_real: assumes "0 < z" shows "Ln(of_real z) = of_real(ln z)" proof - @@ -969,6 +1019,9 @@ using assms by simp qed +corollary Ln_in_Reals [simp]: "z \ \ \ Re z > 0 \ Ln z \ \" + by (auto simp: Ln_of_real elim: Reals_cases) + subsection{*Quadrant-type results for Ln*} @@ -1091,7 +1144,7 @@ lemma Ln_1 [simp]: "Ln(1) = 0" proof - have "Ln (exp 0) = 0" - by (metis exp_zero ln_exp ln_of_real of_real_0 of_real_1 zero_less_one) + by (metis exp_zero ln_exp Ln_of_real of_real_0 of_real_1 zero_less_one) then show ?thesis by simp qed @@ -1262,6 +1315,10 @@ "(Im z = 0 \ 0 < Re(z)) \ continuous (at z) csqrt" by (simp add: complex_differentiable_within_csqrt complex_differentiable_imp_continuous_at) +corollary isCont_csqrt' [simp]: + "\isCont f z; Im(f z) = 0 \ 0 < Re(f z)\ \ isCont (\x. csqrt (f x)) z" + by (blast intro: isCont_o2 [OF _ continuous_at_csqrt]) + lemma continuous_within_csqrt: "(Im z = 0 \ 0 < Re(z)) \ continuous (at z within s) csqrt" by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_csqrt) @@ -1300,5 +1357,824 @@ by (metis linear not_less real_sqrt_less_iff real_sqrt_pow2_iff real_sqrt_power) qed +subsection{*Complex arctangent*} + +text{*branch cut gives standard bounds in real case.*} + +definition Arctan :: "complex \ complex" where + "Arctan \ \z. (\/2) * Ln((1 - \*z) / (1 + \*z))" + +lemma Arctan_0 [simp]: "Arctan 0 = 0" + by (simp add: Arctan_def) + +lemma Im_complex_div_lemma: "Im((1 - \*z) / (1 + \*z)) = 0 \ Re z = 0" + by (auto simp: Im_complex_div_eq_0 algebra_simps) + +lemma Re_complex_div_lemma: "0 < Re((1 - \*z) / (1 + \*z)) \ norm z < 1" + by (simp add: Re_complex_div_gt_0 algebra_simps cmod_def power2_eq_square) + +lemma tan_Arctan: + assumes "z\<^sup>2 \ -1" + shows [simp]:"tan(Arctan z) = z" +proof - + have "1 + \*z \ 0" + by (metis assms complex_i_mult_minus i_squared minus_unique power2_eq_square power2_minus) + moreover + have "1 - \*z \ 0" + by (metis assms complex_i_mult_minus i_squared power2_eq_square power2_minus right_minus_eq) + ultimately + show ?thesis + by (simp add: Arctan_def tan_def sin_exp_eq cos_exp_eq exp_minus csqrt_exp_Ln [symmetric] + divide_simps power2_eq_square [symmetric]) +qed + +lemma Arctan_tan [simp]: + assumes "\Re z\ < pi/2" + shows "Arctan(tan z) = z" +proof - + have ge_pi2: "\n::int. abs (of_int (2*n + 1) * pi/2) \ pi/2" + by (case_tac n rule: int_cases) (auto simp: abs_mult) + have "exp (\*z)*exp (\*z) = -1 \ exp (2*\*z) = -1" + by (metis distrib_right exp_add mult_2) + also have "... \ exp (2*\*z) = exp (\*pi)" + using cis_conv_exp cis_pi by auto + also have "... \ exp (2*\*z - \*pi) = 1" + by (metis (no_types) diff_add_cancel diff_minus_eq_add exp_add exp_minus_inverse mult.commute) + also have "... \ Re(\*2*z - \*pi) = 0 \ (\n::int. Im(\*2*z - \*pi) = of_int (2 * n) * pi)" + by (simp add: exp_eq_1) + also have "... \ Im z = 0 \ (\n::int. 2 * Re z = of_int (2*n + 1) * pi)" + by (simp add: algebra_simps) + also have "... \ False" + using assms ge_pi2 + apply (auto simp: algebra_simps) + by (metis abs_mult_pos not_less not_real_of_nat_less_zero real_of_nat_numeral) + finally have *: "exp (\*z)*exp (\*z) + 1 \ 0" + by (auto simp: add.commute minus_unique) + show ?thesis + using assms * + apply (simp add: Arctan_def tan_def sin_exp_eq cos_exp_eq exp_minus divide_simps + ii_times_eq_iff power2_eq_square [symmetric]) + apply (rule Ln_unique) + apply (auto simp: divide_simps exp_minus) + apply (simp add: algebra_simps exp_double [symmetric]) + done +qed + +lemma + assumes "Re z = 0 \ abs(Im z) < 1" + shows Re_Arctan_bounds: "abs(Re(Arctan z)) < pi/2" + and has_field_derivative_Arctan: "(Arctan has_field_derivative inverse(1 + z\<^sup>2)) (at z)" +proof - + have nz0: "1 + \*z \ 0" + using assms + by (metis abs_one complex_i_mult_minus diff_0_right diff_minus_eq_add ii.simps(1) ii.simps(2) + less_irrefl minus_diff_eq mult.right_neutral right_minus_eq) + have "z \ -\" using assms + by auto + then have zz: "1 + z * z \ 0" + by (metis abs_one assms i_squared ii.simps less_irrefl minus_unique square_eq_iff) + have nz1: "1 - \*z \ 0" + using assms by (force simp add: ii_times_eq_iff) + have nz2: "inverse (1 + \*z) \ 0" + using assms + by (metis Im_complex_div_lemma Re_complex_div_lemma cmod_eq_Im divide_complex_def + less_irrefl mult_zero_right zero_complex.simps(1) zero_complex.simps(2)) + have nzi: "((1 - \*z) * inverse (1 + \*z)) \ 0" + using nz1 nz2 by auto + have *: "Im ((1 - \*z) / (1 + \*z)) = 0 \ 0 < Re ((1 - \*z) / (1 + \*z))" + apply (simp add: divide_complex_def) + apply (simp add: divide_simps split: split_if_asm) + using assms + apply (auto simp: algebra_simps abs_square_less_1 [unfolded power2_eq_square]) + done + show "abs(Re(Arctan z)) < pi/2" + unfolding Arctan_def divide_complex_def + using mpi_less_Im_Ln [OF nzi] + by (auto simp: abs_if intro: Im_Ln_less_pi * [unfolded divide_complex_def]) + show "(Arctan has_field_derivative inverse(1 + z\<^sup>2)) (at z)" + unfolding Arctan_def scaleR_conv_of_real + apply (rule DERIV_cong) + apply (intro derivative_eq_intros | simp add: nz0 *)+ + using nz0 nz1 zz + apply (simp add: divide_simps power2_eq_square) + apply (auto simp: algebra_simps) + done +qed + +lemma complex_differentiable_at_Arctan: "(Re z = 0 \ abs(Im z) < 1) \ Arctan complex_differentiable at z" + using has_field_derivative_Arctan + by (auto simp: complex_differentiable_def) + +lemma complex_differentiable_within_Arctan: + "(Re z = 0 \ abs(Im z) < 1) \ Arctan complex_differentiable (at z within s)" + using complex_differentiable_at_Arctan complex_differentiable_at_within by blast + +declare has_field_derivative_Arctan [derivative_intros] +declare has_field_derivative_Arctan [THEN DERIV_chain2, derivative_intros] + +lemma continuous_at_Arctan: + "(Re z = 0 \ abs(Im z) < 1) \ continuous (at z) Arctan" + by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_Arctan) + +lemma continuous_within_Arctan: + "(Re z = 0 \ abs(Im z) < 1) \ continuous (at z within s) Arctan" + using continuous_at_Arctan continuous_at_imp_continuous_within by blast + +lemma continuous_on_Arctan [continuous_intros]: + "(\z. z \ s \ Re z = 0 \ abs \Im z\ < 1) \ continuous_on s Arctan" + by (auto simp: continuous_at_imp_continuous_on continuous_within_Arctan) + +lemma holomorphic_on_Arctan: + "(\z. z \ s \ Re z = 0 \ abs \Im z\ < 1) \ Arctan holomorphic_on s" + by (simp add: complex_differentiable_within_Arctan holomorphic_on_def) + + +subsection {*Real arctangent*} + +lemma norm_exp_ii_times [simp]: "norm (exp(\ * of_real y)) = 1" + by simp + +lemma norm_exp_imaginary: "norm(exp z) = 1 \ Re z = 0" + by (simp add: complex_norm_eq_1_exp) + +lemma Im_Arctan_of_real [simp]: "Im (Arctan (of_real x)) = 0" + unfolding Arctan_def divide_complex_def + apply (simp add: complex_eq_iff) + apply (rule norm_exp_imaginary) + apply (subst exp_Ln, auto) + apply (simp_all add: cmod_def complex_eq_iff) + apply (auto simp: divide_simps) + apply (metis power_one realpow_two_sum_zero_iff zero_neq_one, algebra) + done + +lemma arctan_eq_Re_Arctan: "arctan x = Re (Arctan (of_real x))" +proof (rule arctan_unique) + show "- (pi / 2) < Re (Arctan (complex_of_real x))" + apply (simp add: Arctan_def) + apply (rule Im_Ln_less_pi) + apply (auto simp: Im_complex_div_lemma) + done +next + have *: " (1 - \*x) / (1 + \*x) \ 0" + by (simp add: divide_simps) ( simp add: complex_eq_iff) + show "Re (Arctan (complex_of_real x)) < pi / 2" + using mpi_less_Im_Ln [OF *] + by (simp add: Arctan_def) +next + have "tan (Re (Arctan (of_real x))) = Re (tan (Arctan (of_real x)))" + apply (auto simp: tan_def Complex.Re_divide Re_sin Re_cos Im_sin Im_cos) + apply (simp add: field_simps) + by (simp add: power2_eq_square) + also have "... = x" + apply (subst tan_Arctan, auto) + by (metis diff_0_right minus_diff_eq mult_zero_left not_le of_real_1 of_real_eq_iff of_real_minus of_real_power power2_eq_square real_minus_mult_self_le zero_less_one) + finally show "tan (Re (Arctan (complex_of_real x))) = x" . +qed + +lemma Arctan_of_real: "Arctan (of_real x) = of_real (arctan x)" + unfolding arctan_eq_Re_Arctan divide_complex_def + by (simp add: complex_eq_iff) + +lemma Arctan_in_Reals [simp]: "z \ \ \ Arctan z \ \" + by (metis Reals_cases Reals_of_real Arctan_of_real) + +declare arctan_one [simp] + +lemma arctan_less_pi4_pos: "x < 1 \ arctan x < pi/4" + by (metis arctan_less_iff arctan_one) + +lemma arctan_less_pi4_neg: "-1 < x \ -(pi/4) < arctan x" + by (metis arctan_less_iff arctan_minus arctan_one) + +lemma arctan_less_pi4: "abs x < 1 \ abs(arctan x) < pi/4" + by (metis abs_less_iff arctan_less_pi4_pos arctan_minus) + +lemma arctan_le_pi4: "abs x \ 1 \ abs(arctan x) \ pi/4" + by (metis abs_le_iff arctan_le_iff arctan_minus arctan_one) + +lemma abs_arctan: "abs(arctan x) = arctan(abs x)" + by (simp add: abs_if arctan_minus) + +lemma arctan_add_raw: + assumes "abs(arctan x + arctan y) < pi/2" + shows "arctan x + arctan y = arctan((x + y) / (1 - x * y))" +proof (rule arctan_unique [symmetric]) + show 12: "- (pi / 2) < arctan x + arctan y" "arctan x + arctan y < pi / 2" + using assms by linarith+ + show "tan (arctan x + arctan y) = (x + y) / (1 - x * y)" + using cos_gt_zero_pi [OF 12] + by (simp add: arctan tan_add) +qed + +lemma arctan_inverse: + assumes "0 < x" + shows "arctan(inverse x) = pi/2 - arctan x" +proof - + have "arctan(inverse x) = arctan(inverse(tan(arctan x)))" + by (simp add: arctan) + also have "... = arctan (tan (pi / 2 - arctan x))" + by (simp add: tan_cot) + also have "... = pi/2 - arctan x" + proof - + have "0 < pi - arctan x" + using arctan_ubound [of x] pi_gt_zero by linarith + with assms show ?thesis + by (simp add: Transcendental.arctan_tan) + qed + finally show ?thesis . +qed + +lemma arctan_add_small: + assumes "abs(x * y) < 1" + shows "(arctan x + arctan y = arctan((x + y) / (1 - x * y)))" +proof (cases "x = 0 \ y = 0") + case True then show ?thesis + by auto +next + case False + then have *: "\arctan x\ < pi / 2 - \arctan y\" using assms + apply (auto simp add: abs_arctan arctan_inverse [symmetric] arctan_less_iff) + apply (simp add: divide_simps abs_mult) + done + show ?thesis + apply (rule arctan_add_raw) + using * by linarith +qed + +lemma abs_arctan_le: + fixes x::real shows "abs(arctan x) \ abs x" +proof - + { fix w::complex and z::complex + assume *: "w \ \" "z \ \" + have "cmod (Arctan w - Arctan z) \ 1 * cmod (w-z)" + apply (rule complex_differentiable_bound [OF convex_Reals, of Arctan _ 1]) + apply (rule has_field_derivative_at_within [OF has_field_derivative_Arctan]) + apply (force simp add: Reals_def) + apply (simp add: norm_divide divide_simps in_Reals_norm complex_is_Real_iff power2_eq_square) + using * by auto + } + then have "cmod (Arctan (of_real x) - Arctan 0) \ 1 * cmod (of_real x -0)" + using Reals_0 Reals_of_real by blast + then show ?thesis + by (simp add: Arctan_of_real) +qed + +lemma arctan_le_self: "0 \ x \ arctan x \ x" + by (metis abs_arctan_le abs_of_nonneg zero_le_arctan_iff) + +lemma abs_tan_ge: "abs x < pi/2 \ abs x \ abs(tan x)" + by (metis abs_arctan_le abs_less_iff arctan_tan minus_less_iff) + + +subsection{*Inverse Sine*} + +definition Arcsin :: "complex \ complex" where + "Arcsin \ \z. -\ * Ln(\ * z + csqrt(1 - z\<^sup>2))" + +lemma Arcsin_body_lemma: "\ * z + csqrt(1 - z\<^sup>2) \ 0" + using power2_csqrt [of "1 - z\<^sup>2"] + apply auto + by (metis complex_i_mult_minus diff_add_cancel diff_minus_eq_add diff_self mult.assoc mult.left_commute numeral_One power2_csqrt power2_eq_square zero_neq_numeral) + +lemma Arcsin_range_lemma: "abs (Re z) < 1 \ 0 < Re(\ * z + csqrt(1 - z\<^sup>2))" + using Complex.cmod_power2 [of z, symmetric] + by (simp add: real_less_rsqrt algebra_simps Re_power2 cmod_square_less_1_plus) + +lemma Re_Arcsin: "Re(Arcsin z) = Im (Ln (\ * z + csqrt(1 - z\<^sup>2)))" + by (simp add: Arcsin_def) + +lemma Im_Arcsin: "Im(Arcsin z) = - ln (cmod (\ * z + csqrt (1 - z\<^sup>2)))" + by (simp add: Arcsin_def Arcsin_body_lemma) + +lemma isCont_Arcsin: + assumes "(Im z = 0 \ \Re z\ < 1)" + shows "isCont Arcsin z" +proof - + have rez: "Im (1 - z\<^sup>2) = 0 \ 0 < Re (1 - z\<^sup>2)" + using assms + by (auto simp: Re_power2 Im_power2 abs_square_less_1 add_pos_nonneg algebra_simps) + have cmz: "(cmod z)\<^sup>2 < 1 + cmod (1 - z\<^sup>2)" + by (blast intro: assms cmod_square_less_1_plus) + show ?thesis + using assms + apply (simp add: Arcsin_def) + apply (rule isCont_Ln' isCont_csqrt' continuous_intros)+ + apply (erule rez) + apply (auto simp: Re_power2 Im_power2 abs_square_less_1 [symmetric] real_less_rsqrt algebra_simps split: split_if_asm) + apply (simp add: norm_complex_def) + using cmod_power2 [of z, symmetric] cmz + apply (simp add: real_less_rsqrt) + done +qed + +lemma isCont_Arcsin' [simp]: + shows "isCont f z \ (Im (f z) = 0 \ \Re (f z)\ < 1) \ isCont (\x. Arcsin (f x)) z" + by (blast intro: isCont_o2 [OF _ isCont_Arcsin]) + +lemma sin_Arcsin [simp]: "sin(Arcsin z) = z" +proof - + have "\*z*2 + csqrt (1 - z\<^sup>2)*2 = 0 \ (\*z)*2 + csqrt (1 - z\<^sup>2)*2 = 0" + by (simp add: algebra_simps) --{*Cancelling a factor of 2*} + moreover have "... \ (\*z) + csqrt (1 - z\<^sup>2) = 0" + by (metis Arcsin_body_lemma distrib_right no_zero_divisors zero_neq_numeral) + ultimately show ?thesis + apply (simp add: sin_exp_eq Arcsin_def Arcsin_body_lemma exp_minus divide_simps) + apply (simp add: algebra_simps) + apply (simp add: power2_eq_square [symmetric] algebra_simps) + done +qed + +lemma Re_eq_pihalf_lemma: + "\Re z\ = pi/2 \ Im z = 0 \ + Re ((exp (\*z) + inverse (exp (\*z))) / 2) = 0 \ 0 \ Im ((exp (\*z) + inverse (exp (\*z))) / 2)" + apply (simp add: cos_ii_times [symmetric] Re_cos Im_cos abs_if del: eq_divide_eq_numeral1) + by (metis cos_minus cos_pi_half) + +lemma Re_less_pihalf_lemma: + assumes "\Re z\ < pi / 2" + shows "0 < Re ((exp (\*z) + inverse (exp (\*z))) / 2)" +proof - + have "0 < cos (Re z)" using assms + using cos_gt_zero_pi by auto + then show ?thesis + by (simp add: cos_ii_times [symmetric] Re_cos Im_cos add_pos_pos) +qed + +lemma Arcsin_sin: + assumes "\Re z\ < pi/2 \ (\Re z\ = pi/2 \ Im z = 0)" + shows "Arcsin(sin z) = z" +proof - + have "Arcsin(sin z) = - (\ * Ln (csqrt (1 - (\ * (exp (\*z) - inverse (exp (\*z))))\<^sup>2 / 4) - (inverse (exp (\*z)) - exp (\*z)) / 2))" + by (simp add: sin_exp_eq Arcsin_def exp_minus) + also have "... = - (\ * Ln (csqrt (((exp (\*z) + inverse (exp (\*z)))/2)\<^sup>2) - (inverse (exp (\*z)) - exp (\*z)) / 2))" + by (simp add: field_simps power2_eq_square) + also have "... = - (\ * Ln (((exp (\*z) + inverse (exp (\*z)))/2) - (inverse (exp (\*z)) - exp (\*z)) / 2))" + apply (subst csqrt_square) + using assms Re_eq_pihalf_lemma Re_less_pihalf_lemma + apply auto + done + also have "... = - (\ * Ln (exp (\*z)))" + by (simp add: field_simps power2_eq_square) + also have "... = z" + apply (subst Complex_Transcendental.Ln_exp) + using assms + apply (auto simp: abs_if simp del: eq_divide_eq_numeral1 split: split_if_asm) + done + finally show ?thesis . +qed + +lemma Arcsin_unique: + "\sin z = w; \Re z\ < pi/2 \ (\Re z\ = pi/2 \ Im z = 0)\ \ Arcsin w = z" + by (metis Arcsin_sin) + +lemma Arcsin_0 [simp]: "Arcsin 0 = 0" + by (metis Arcsin_sin norm_zero pi_half_gt_zero real_norm_def sin_zero zero_complex.simps(1)) + +lemma Arcsin_1 [simp]: "Arcsin 1 = pi/2" + by (metis Arcsin_sin Im_complex_of_real Re_complex_of_real numeral_One of_real_numeral pi_half_ge_zero real_sqrt_abs real_sqrt_pow2 real_sqrt_power sin_of_real sin_pi_half) + +lemma Arcsin_minus_1 [simp]: "Arcsin(-1) = - (pi/2)" + by (metis Arcsin_1 Arcsin_sin Im_complex_of_real Re_complex_of_real abs_of_nonneg of_real_minus pi_half_ge_zero power2_minus real_sqrt_abs sin_Arcsin sin_minus) + +lemma has_field_derivative_Arcsin: + assumes "(Im z = 0 \ \Re z\ < 1)" + shows "(Arcsin has_field_derivative inverse(cos(Arcsin z))) (at z)" +proof - + have "(sin (Arcsin z))\<^sup>2 \ 1" + using assms + apply atomize + apply (auto simp: complex_eq_iff Re_power2 Im_power2 abs_square_eq_1) + apply (metis abs_minus_cancel abs_one abs_power2 numeral_One numeral_neq_neg_one) + by (metis abs_minus_cancel abs_one abs_power2 one_neq_neg_one) + then have "cos (Arcsin z) \ 0" + by (metis diff_0_right power_zero_numeral sin_squared_eq) + then show ?thesis + apply (rule has_complex_derivative_inverse_basic [OF DERIV_sin]) + apply (auto intro: isCont_Arcsin open_ball [of z 1] assms) + done +qed + +declare has_field_derivative_Arcsin [derivative_intros] +declare has_field_derivative_Arcsin [THEN DERIV_chain2, derivative_intros] + +lemma complex_differentiable_at_Arcsin: + "(Im z = 0 \ \Re z\ < 1) \ Arcsin complex_differentiable at z" + using complex_differentiable_def has_field_derivative_Arcsin by blast + +lemma complex_differentiable_within_Arcsin: + "(Im z = 0 \ \Re z\ < 1) \ Arcsin complex_differentiable (at z within s)" + using complex_differentiable_at_Arcsin complex_differentiable_within_subset by blast + +lemma continuous_within_Arcsin: + "(Im z = 0 \ \Re z\ < 1) \ continuous (at z within s) Arcsin" + using continuous_at_imp_continuous_within isCont_Arcsin by blast + +lemma continuous_on_Arcsin [continuous_intros]: + "(\z. z \ s \ Im z = 0 \ \Re z\ < 1) \ continuous_on s Arcsin" + by (simp add: continuous_at_imp_continuous_on) + +lemma holomorphic_on_Arcsin: "(\z. z \ s \ Im z = 0 \ \Re z\ < 1) \ Arcsin holomorphic_on s" + by (simp add: complex_differentiable_within_Arcsin holomorphic_on_def) + + +subsection{*Inverse Cosine*} + +definition Arccos :: "complex \ complex" where + "Arccos \ \z. -\ * Ln(z + \ * csqrt(1 - z\<^sup>2))" + +lemma Arccos_range_lemma: "\Re z\ < 1 \ 0 < Im(z + \ * csqrt(1 - z\<^sup>2))" + using Arcsin_range_lemma [of "-z"] + by simp + +lemma Arccos_body_lemma: "z + \ * csqrt(1 - z\<^sup>2) \ 0" + using Arcsin_body_lemma [of z] + by (metis complex_i_mult_minus diff_add_cancel minus_diff_eq minus_unique mult.assoc mult.left_commute + power2_csqrt power2_eq_square zero_neq_one) + +lemma Re_Arccos: "Re(Arccos z) = Im (Ln (z + \ * csqrt(1 - z\<^sup>2)))" + by (simp add: Arccos_def) + +lemma Im_Arccos: "Im(Arccos z) = - ln (cmod (z + \ * csqrt (1 - z\<^sup>2)))" + by (simp add: Arccos_def Arccos_body_lemma) + +text{*A very tricky argument to find!*} +lemma abs_Re_less_1_preserve: + assumes "(Im z = 0 \ \Re z\ < 1)" "Im (z + \ * csqrt (1 - z\<^sup>2)) = 0" + shows "0 < Re (z + \ * csqrt (1 - z\<^sup>2))" +proof (cases "Im z = 0") + case True + then show ?thesis + using assms + by (fastforce simp add: cmod_def Re_power2 Im_power2 algebra_simps abs_square_less_1 [symmetric]) +next + case False + have Imz: "Im z = - sqrt ((1 + ((Im z)\<^sup>2 + cmod (1 - z\<^sup>2)) - (Re z)\<^sup>2) / 2)" + using assms abs_Re_le_cmod [of "1-z\<^sup>2"] + by (simp add: Re_power2 algebra_simps) + have "(cmod z)\<^sup>2 - 1 \ cmod (1 - z\<^sup>2)" + proof (clarsimp simp add: cmod_def) + assume "(Re z)\<^sup>2 + (Im z)\<^sup>2 - 1 = sqrt ((1 - Re (z\<^sup>2))\<^sup>2 + (Im (z\<^sup>2))\<^sup>2)" + then have "((Re z)\<^sup>2 + (Im z)\<^sup>2 - 1)\<^sup>2 = ((1 - Re (z\<^sup>2))\<^sup>2 + (Im (z\<^sup>2))\<^sup>2)" + by simp + then show False using False + by (simp add: power2_eq_square algebra_simps) + qed + moreover have "(Im z)\<^sup>2 = ((1 + ((Im z)\<^sup>2 + cmod (1 - z\<^sup>2)) - (Re z)\<^sup>2) / 2)" + apply (subst Imz, simp) + apply (subst real_sqrt_pow2) + using abs_Re_le_cmod [of "1-z\<^sup>2"] + apply (auto simp: Re_power2 field_simps) + done + ultimately show ?thesis + by (simp add: Re_power2 Im_power2 cmod_power2) +qed + +lemma isCont_Arccos: + assumes "(Im z = 0 \ \Re z\ < 1)" + shows "isCont Arccos z" +proof - + have rez: "Im (1 - z\<^sup>2) = 0 \ 0 < Re (1 - z\<^sup>2)" + using assms + by (auto simp: Re_power2 Im_power2 abs_square_less_1 add_pos_nonneg algebra_simps) + show ?thesis + using assms + apply (simp add: Arccos_def) + apply (rule isCont_Ln' isCont_csqrt' continuous_intros)+ + apply (erule rez) + apply (blast intro: abs_Re_less_1_preserve) + done +qed + +lemma isCont_Arccos' [simp]: + shows "isCont f z \ (Im (f z) = 0 \ \Re (f z)\ < 1) \ isCont (\x. Arccos (f x)) z" + by (blast intro: isCont_o2 [OF _ isCont_Arccos]) + +lemma cos_Arccos [simp]: "cos(Arccos z) = z" +proof - + have "z*2 + \ * (2 * csqrt (1 - z\<^sup>2)) = 0 \ z*2 + \ * csqrt (1 - z\<^sup>2)*2 = 0" + by (simp add: algebra_simps) --{*Cancelling a factor of 2*} + moreover have "... \ z + \ * csqrt (1 - z\<^sup>2) = 0" + by (metis distrib_right mult_eq_0_iff zero_neq_numeral) + ultimately show ?thesis + apply (simp add: cos_exp_eq Arccos_def Arccos_body_lemma exp_minus field_simps) + apply (simp add: power2_eq_square [symmetric]) + done +qed + +lemma Arccos_cos: + assumes "0 < Re z & Re z < pi \ + Re z = 0 & 0 \ Im z \ + Re z = pi & Im z \ 0" + shows "Arccos(cos z) = z" +proof - + have *: "((\ - (Exp (\ * z))\<^sup>2 * \) / (2 * Exp (\ * z))) = sin z" + by (simp add: sin_exp_eq exp_minus field_simps power2_eq_square) + have "1 - (exp (\ * z) + inverse (exp (\ * z)))\<^sup>2 / 4 = ((\ - (Exp (\ * z))\<^sup>2 * \) / (2 * Exp (\ * z)))\<^sup>2" + by (simp add: field_simps power2_eq_square) + then have "Arccos(cos z) = - (\ * Ln ((exp (\ * z) + inverse (exp (\ * z))) / 2 + + \ * csqrt (((\ - (Exp (\ * z))\<^sup>2 * \) / (2 * Exp (\ * z)))\<^sup>2)))" + by (simp add: cos_exp_eq Arccos_def exp_minus) + also have "... = - (\ * Ln ((exp (\ * z) + inverse (exp (\ * z))) / 2 + + \ * ((\ - (Exp (\ * z))\<^sup>2 * \) / (2 * Exp (\ * z)))))" + apply (subst csqrt_square) + using assms Re_sin_pos [of z] Im_sin_nonneg [of z] Im_sin_nonneg2 [of z] + apply (auto simp: * Re_sin Im_sin) + done + also have "... = - (\ * Ln (exp (\*z)))" + by (simp add: field_simps power2_eq_square) + also have "... = z" + using assms + apply (subst Complex_Transcendental.Ln_exp, auto) + done + finally show ?thesis . +qed + +lemma Arccos_unique: + "\cos z = w; + 0 < Re z \ Re z < pi \ + Re z = 0 \ 0 \ Im z \ + Re z = pi \ Im z \ 0\ \ Arccos w = z" + using Arccos_cos by blast + +lemma Arccos_0 [simp]: "Arccos 0 = pi/2" + by (rule Arccos_unique) (auto simp: of_real_numeral) + +lemma Arccos_1 [simp]: "Arccos 1 = 0" + by (rule Arccos_unique) auto + +lemma Arccos_minus1: "Arccos(-1) = pi" + by (rule Arccos_unique) auto + +lemma has_field_derivative_Arccos: + assumes "(Im z = 0 \ \Re z\ < 1)" + shows "(Arccos has_field_derivative - inverse(sin(Arccos z))) (at z)" +proof - + have "(cos (Arccos z))\<^sup>2 \ 1" + using assms + apply atomize + apply (auto simp: complex_eq_iff Re_power2 Im_power2 abs_square_eq_1) + apply (metis abs_minus_cancel abs_one abs_power2 numeral_One numeral_neq_neg_one) + apply (metis left_minus less_irrefl power_one sum_power2_gt_zero_iff zero_neq_neg_one) + done + then have "- sin (Arccos z) \ 0" + by (metis cos_squared_eq diff_0_right mult_zero_left neg_0_equal_iff_equal power2_eq_square) + then have "(Arccos has_field_derivative inverse(- sin(Arccos z))) (at z)" + apply (rule has_complex_derivative_inverse_basic [OF DERIV_cos]) + apply (auto intro: isCont_Arccos open_ball [of z 1] assms) + done + then show ?thesis + by simp +qed + +declare has_field_derivative_Arcsin [derivative_intros] +declare has_field_derivative_Arcsin [THEN DERIV_chain2, derivative_intros] + +lemma complex_differentiable_at_Arccos: + "(Im z = 0 \ \Re z\ < 1) \ Arccos complex_differentiable at z" + using complex_differentiable_def has_field_derivative_Arccos by blast + +lemma complex_differentiable_within_Arccos: + "(Im z = 0 \ \Re z\ < 1) \ Arccos complex_differentiable (at z within s)" + using complex_differentiable_at_Arccos complex_differentiable_within_subset by blast + +lemma continuous_within_Arccos: + "(Im z = 0 \ \Re z\ < 1) \ continuous (at z within s) Arccos" + using continuous_at_imp_continuous_within isCont_Arccos by blast + +lemma continuous_on_Arccos [continuous_intros]: + "(\z. z \ s \ Im z = 0 \ \Re z\ < 1) \ continuous_on s Arccos" + by (simp add: continuous_at_imp_continuous_on) + +lemma holomorphic_on_Arccos: "(\z. z \ s \ Im z = 0 \ \Re z\ < 1) \ Arccos holomorphic_on s" + by (simp add: complex_differentiable_within_Arccos holomorphic_on_def) + + +subsection{*Upper and Lower Bounds for Inverse Sine and Cosine*} + +lemma Arcsin_bounds: "\Re z\ < 1 \ abs(Re(Arcsin z)) < pi/2" + unfolding Re_Arcsin + by (blast intro: Re_Ln_pos_lt_imp Arcsin_range_lemma) + +lemma Arccos_bounds: "\Re z\ < 1 \ 0 < Re(Arccos z) \ Re(Arccos z) < pi" + unfolding Re_Arccos + by (blast intro!: Im_Ln_pos_lt_imp Arccos_range_lemma) + +lemma Re_Arccos_bounds: "-pi < Re(Arccos z) \ Re(Arccos z) \ pi" + unfolding Re_Arccos + by (blast intro!: mpi_less_Im_Ln Im_Ln_le_pi Arccos_body_lemma) + +lemma Re_Arccos_bound: "abs(Re(Arccos z)) \ pi" + using Re_Arccos_bounds abs_le_interval_iff less_eq_real_def by blast + +lemma Re_Arcsin_bounds: "-pi < Re(Arcsin z) & Re(Arcsin z) \ pi" + unfolding Re_Arcsin + by (blast intro!: mpi_less_Im_Ln Im_Ln_le_pi Arcsin_body_lemma) + +lemma Re_Arcsin_bound: "abs(Re(Arcsin z)) \ pi" + using Re_Arcsin_bounds abs_le_interval_iff less_eq_real_def by blast + + +subsection{*Interrelations between Arcsin and Arccos*} + +lemma cos_Arcsin_nonzero: + assumes "z\<^sup>2 \ 1" shows "cos(Arcsin z) \ 0" +proof - + have eq: "(\ * z * (csqrt (1 - z\<^sup>2)))\<^sup>2 = z\<^sup>2 * (z\<^sup>2 - 1)" + by (simp add: power_mult_distrib algebra_simps) + have "\ * z * (csqrt (1 - z\<^sup>2)) \ z\<^sup>2 - 1" + proof + assume "\ * z * (csqrt (1 - z\<^sup>2)) = z\<^sup>2 - 1" + then have "(\ * z * (csqrt (1 - z\<^sup>2)))\<^sup>2 = (z\<^sup>2 - 1)\<^sup>2" + by simp + then have "z\<^sup>2 * (z\<^sup>2 - 1) = (z\<^sup>2 - 1)*(z\<^sup>2 - 1)" + using eq power2_eq_square by auto + then show False + using assms by simp + qed + then have "1 + \ * z * (csqrt (1 - z * z)) \ z\<^sup>2" + by (metis add_minus_cancel power2_eq_square uminus_add_conv_diff) + then have "2*(1 + \ * z * (csqrt (1 - z * z))) \ 2*z\<^sup>2" (*FIXME cancel_numeral_factor*) + by (metis mult_cancel_left zero_neq_numeral) + then have "(\ * z + csqrt (1 - z\<^sup>2))\<^sup>2 \ -1" + using assms + apply (auto simp: power2_sum) + apply (simp add: power2_eq_square algebra_simps) + done + then show ?thesis + apply (simp add: cos_exp_eq Arcsin_def exp_minus) + apply (simp add: divide_simps Arcsin_body_lemma) + apply (metis add.commute minus_unique power2_eq_square) + done +qed + +lemma sin_Arccos_nonzero: + assumes "z\<^sup>2 \ 1" shows "sin(Arccos z) \ 0" +proof - + have eq: "(\ * z * (csqrt (1 - z\<^sup>2)))\<^sup>2 = -(z\<^sup>2) * (1 - z\<^sup>2)" + by (simp add: power_mult_distrib algebra_simps) + have "\ * z * (csqrt (1 - z\<^sup>2)) \ 1 - z\<^sup>2" + proof + assume "\ * z * (csqrt (1 - z\<^sup>2)) = 1 - z\<^sup>2" + then have "(\ * z * (csqrt (1 - z\<^sup>2)))\<^sup>2 = (1 - z\<^sup>2)\<^sup>2" + by simp + then have "-(z\<^sup>2) * (1 - z\<^sup>2) = (1 - z\<^sup>2)*(1 - z\<^sup>2)" + using eq power2_eq_square by auto + then have "-(z\<^sup>2) = (1 - z\<^sup>2)" + using assms + by (metis add.commute add.right_neutral diff_add_cancel mult_right_cancel) + then show False + using assms by simp + qed + then have "z\<^sup>2 + \ * z * (csqrt (1 - z\<^sup>2)) \ 1" + by (simp add: algebra_simps) + then have "2*(z\<^sup>2 + \ * z * (csqrt (1 - z\<^sup>2))) \ 2*1" + by (metis mult_cancel_left2 zero_neq_numeral) (*FIXME cancel_numeral_factor*) + then have "(z + \ * csqrt (1 - z\<^sup>2))\<^sup>2 \ 1" + using assms + apply (auto simp: Power.comm_semiring_1_class.power2_sum power_mult_distrib) + apply (simp add: power2_eq_square algebra_simps) + done + then show ?thesis + apply (simp add: sin_exp_eq Arccos_def exp_minus) + apply (simp add: divide_simps Arccos_body_lemma) + apply (simp add: power2_eq_square) + done +qed + +lemma cos_sin_csqrt: + assumes "0 < cos(Re z) \ cos(Re z) = 0 \ Im z * sin(Re z) \ 0" + shows "cos z = csqrt(1 - (sin z)\<^sup>2)" + apply (rule csqrt_unique [THEN sym]) + apply (simp add: cos_squared_eq) + using assms + apply (auto simp: Re_cos Im_cos add_pos_pos mult_le_0_iff zero_le_mult_iff) + apply (auto simp: algebra_simps) + done + +lemma sin_cos_csqrt: + assumes "0 < sin(Re z) \ sin(Re z) = 0 \ 0 \ Im z * cos(Re z)" + shows "sin z = csqrt(1 - (cos z)\<^sup>2)" + apply (rule csqrt_unique [THEN sym]) + apply (simp add: sin_squared_eq) + using assms + apply (auto simp: Re_sin Im_sin add_pos_pos mult_le_0_iff zero_le_mult_iff) + apply (auto simp: algebra_simps) + done + +lemma Arcsin_Arccos_csqrt_pos: + "(0 < Re z | Re z = 0 & 0 \ Im z) \ Arcsin z = Arccos(csqrt(1 - z\<^sup>2))" + by (simp add: Arcsin_def Arccos_def Complex.csqrt_square add.commute) + +lemma Arccos_Arcsin_csqrt_pos: + "(0 < Re z | Re z = 0 & 0 \ Im z) \ Arccos z = Arcsin(csqrt(1 - z\<^sup>2))" + by (simp add: Arcsin_def Arccos_def Complex.csqrt_square add.commute) + +lemma sin_Arccos: + "0 < Re z | Re z = 0 & 0 \ Im z \ sin(Arccos z) = csqrt(1 - z\<^sup>2)" + by (simp add: Arccos_Arcsin_csqrt_pos) + +lemma cos_Arcsin: + "0 < Re z | Re z = 0 & 0 \ Im z \ cos(Arcsin z) = csqrt(1 - z\<^sup>2)" + by (simp add: Arcsin_Arccos_csqrt_pos) + + +subsection{*Relationship with Arcsin on the Real Numbers*} + +lemma Im_Arcsin_of_real: + assumes "abs x \ 1" + shows "Im (Arcsin (of_real x)) = 0" +proof - + have "csqrt (1 - (of_real x)\<^sup>2) = (if x^2 \ 1 then sqrt (1 - x^2) else \ * sqrt (x^2 - 1))" + by (simp add: of_real_sqrt del: csqrt_of_real_nonneg) + then have "cmod (\ * of_real x + csqrt (1 - (of_real x)\<^sup>2))^2 = 1" + using assms abs_square_le_1 + by (force simp add: Complex.cmod_power2) + then have "cmod (\ * of_real x + csqrt (1 - (of_real x)\<^sup>2)) = 1" + by (simp add: norm_complex_def) + then show ?thesis + by (simp add: Im_Arcsin exp_minus) +qed + +corollary Arcsin_in_Reals [simp]: "z \ \ \ \Re z\ \ 1 \ Arcsin z \ \" + by (metis Im_Arcsin_of_real Re_complex_of_real Reals_cases complex_is_Real_iff) + +lemma arcsin_eq_Re_Arcsin: + assumes "abs x \ 1" + shows "arcsin x = Re (Arcsin (of_real x))" +unfolding arcsin_def +proof (rule the_equality, safe) + show "- (pi / 2) \ Re (Arcsin (complex_of_real x))" + using Re_Ln_pos_le [OF Arcsin_body_lemma, of "of_real x"] + by (auto simp: Complex.in_Reals_norm Re_Arcsin) +next + show "Re (Arcsin (complex_of_real x)) \ pi / 2" + using Re_Ln_pos_le [OF Arcsin_body_lemma, of "of_real x"] + by (auto simp: Complex.in_Reals_norm Re_Arcsin) +next + show "sin (Re (Arcsin (complex_of_real x))) = x" + using Re_sin [of "Arcsin (of_real x)"] Arcsin_body_lemma [of "of_real x"] + by (simp add: Im_Arcsin_of_real assms) +next + fix x' + assume "- (pi / 2) \ x'" "x' \ pi / 2" "x = sin x'" + then show "x' = Re (Arcsin (complex_of_real (sin x')))" + apply (simp add: sin_of_real [symmetric]) + apply (subst Arcsin_sin) + apply (auto simp: ) + done +qed + +lemma of_real_arcsin: "abs x \ 1 \ of_real(arcsin x) = Arcsin(of_real x)" + by (metis Im_Arcsin_of_real add.right_neutral arcsin_eq_Re_Arcsin complex_eq mult_zero_right of_real_0) + + +subsection{*Relationship with Arccos on the Real Numbers*} + +lemma Im_Arccos_of_real: + assumes "abs x \ 1" + shows "Im (Arccos (of_real x)) = 0" +proof - + have "csqrt (1 - (of_real x)\<^sup>2) = (if x^2 \ 1 then sqrt (1 - x^2) else \ * sqrt (x^2 - 1))" + by (simp add: of_real_sqrt del: csqrt_of_real_nonneg) + then have "cmod (of_real x + \ * csqrt (1 - (of_real x)\<^sup>2))^2 = 1" + using assms abs_square_le_1 + by (force simp add: Complex.cmod_power2) + then have "cmod (of_real x + \ * csqrt (1 - (of_real x)\<^sup>2)) = 1" + by (simp add: norm_complex_def) + then show ?thesis + by (simp add: Im_Arccos exp_minus) +qed + +corollary Arccos_in_Reals [simp]: "z \ \ \ \Re z\ \ 1 \ Arccos z \ \" + by (metis Im_Arccos_of_real Re_complex_of_real Reals_cases complex_is_Real_iff) + +lemma arccos_eq_Re_Arccos: + assumes "abs x \ 1" + shows "arccos x = Re (Arccos (of_real x))" +unfolding arccos_def +proof (rule the_equality, safe) + show "0 \ Re (Arccos (complex_of_real x))" + using Im_Ln_pos_le [OF Arccos_body_lemma, of "of_real x"] + by (auto simp: Complex.in_Reals_norm Re_Arccos) +next + show "Re (Arccos (complex_of_real x)) \ pi" + using Im_Ln_pos_le [OF Arccos_body_lemma, of "of_real x"] + by (auto simp: Complex.in_Reals_norm Re_Arccos) +next + show "cos (Re (Arccos (complex_of_real x))) = x" + using Re_cos [of "Arccos (of_real x)"] Arccos_body_lemma [of "of_real x"] + by (simp add: Im_Arccos_of_real assms) +next + fix x' + assume "0 \ x'" "x' \ pi" "x = cos x'" + then show "x' = Re (Arccos (complex_of_real (cos x')))" + apply (simp add: cos_of_real [symmetric]) + apply (subst Arccos_cos) + apply (auto simp: ) + done +qed + +lemma of_real_arccos: "abs x \ 1 \ of_real(arccos x) = Arccos(of_real x)" + by (metis Im_Arccos_of_real add.right_neutral arccos_eq_Re_Arccos complex_eq mult_zero_right of_real_0) end diff -r 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/Multivariate_Analysis/Determinants.thy --- a/src/HOL/Multivariate_Analysis/Determinants.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/Determinants.thy Wed Apr 01 22:40:41 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 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/Multivariate_Analysis/Linear_Algebra.thy --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Wed Apr 01 22:40:41 2015 +0200 @@ -68,25 +68,14 @@ lemma norm_eq_square: "norm x = a \ 0 \ a \ x \ x = a\<^sup>2" by (auto simp add: norm_eq_sqrt_inner) -lemma real_abs_le_square_iff: "\x\ \ \y\ \ (x::real)\<^sup>2 \ y\<^sup>2" -proof - assume "\x\ \ \y\" - then have "\x\\<^sup>2 \ \y\\<^sup>2" by (rule power_mono, simp) - then show "x\<^sup>2 \ y\<^sup>2" by simp -next - assume "x\<^sup>2 \ y\<^sup>2" - then have "sqrt (x\<^sup>2) \ sqrt (y\<^sup>2)" by (rule real_sqrt_le_mono) - then show "\x\ \ \y\" by simp -qed - lemma norm_le_square: "norm x \ a \ 0 \ a \ x \ x \ a\<^sup>2" - apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric]) + apply (simp add: dot_square_norm abs_le_square_iff[symmetric]) using norm_ge_zero[of x] apply arith done lemma norm_ge_square: "norm x \ a \ a \ 0 \ x \ x \ a\<^sup>2" - apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric]) + apply (simp add: dot_square_norm abs_le_square_iff[symmetric]) using norm_ge_zero[of x] apply arith done diff -r 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/Multivariate_Analysis/PolyRoots.thy --- a/src/HOL/Multivariate_Analysis/PolyRoots.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/PolyRoots.thy Wed Apr 01 22:40:41 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 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/NSA/HyperDef.thy --- a/src/HOL/NSA/HyperDef.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/NSA/HyperDef.thy Wed Apr 01 22:40:41 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 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/NSA/NSA.thy --- a/src/HOL/NSA/NSA.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/NSA/NSA.thy Wed Apr 01 22:40:41 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 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/NSA/StarDef.thy --- a/src/HOL/NSA/StarDef.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/NSA/StarDef.thy Wed Apr 01 22:40:41 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 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/Num.thy --- a/src/HOL/Num.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/Num.thy Wed Apr 01 22:40:41 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 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/Numeral_Simprocs.thy --- a/src/HOL/Numeral_Simprocs.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/Numeral_Simprocs.thy Wed Apr 01 22:40:41 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 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/Power.thy --- a/src/HOL/Power.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/Power.thy Wed Apr 01 22:40:41 2015 +0200 @@ -645,6 +645,29 @@ "0 < x\<^sup>2 + y\<^sup>2 \ x \ 0 \ y \ 0" unfolding not_le [symmetric] by (simp add: sum_power2_le_zero_iff) +lemma abs_le_square_iff: + "\x\ \ \y\ \ x\<^sup>2 \ y\<^sup>2" +proof + assume "\x\ \ \y\" + then have "\x\\<^sup>2 \ \y\\<^sup>2" by (rule power_mono, simp) + then show "x\<^sup>2 \ y\<^sup>2" by simp +next + assume "x\<^sup>2 \ y\<^sup>2" + then show "\x\ \ \y\" + by (auto intro!: power2_le_imp_le [OF _ abs_ge_zero]) +qed + +lemma abs_square_le_1:"x\<^sup>2 \ 1 \ abs(x) \ 1" + using abs_le_square_iff [of x 1] + by simp + +lemma abs_square_eq_1: "x\<^sup>2 = 1 \ abs(x) = 1" + by (auto simp add: abs_if power2_eq_1_iff) + +lemma abs_square_less_1: "x\<^sup>2 < 1 \ abs(x) < 1" + using abs_square_eq_1 [of x] abs_square_le_1 [of x] + by (auto simp add: le_less) + end @@ -682,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) @@ -690,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 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/Probability/Bochner_Integration.thy --- a/src/HOL/Probability/Bochner_Integration.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/Probability/Bochner_Integration.thy Wed Apr 01 22:40:41 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 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/Probability/Interval_Integral.thy --- a/src/HOL/Probability/Interval_Integral.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/Probability/Interval_Integral.thy Wed Apr 01 22:40:41 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 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/Probability/Set_Integral.thy --- a/src/HOL/Probability/Set_Integral.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/Probability/Set_Integral.thy Wed Apr 01 22:40:41 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 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/Quotient_Examples/Quotient_Rat.thy --- a/src/HOL/Quotient_Examples/Quotient_Rat.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/Quotient_Examples/Quotient_Rat.thy Wed Apr 01 22:40:41 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 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/ROOT --- a/src/HOL/ROOT Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/ROOT Wed Apr 01 22:40:41 2015 +0200 @@ -527,6 +527,7 @@ "~~/src/HOL/Library/Transitive_Closure_Table" Cartouche_Examples theories + Approximations Commands Adhoc_Overloading_Examples Iff_Oracle diff -r 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/Rat.thy --- a/src/HOL/Rat.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/Rat.thy Wed Apr 01 22:40:41 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 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/Real.thy --- a/src/HOL/Real.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/Real.thy Wed Apr 01 22:40:41 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 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/Real_Vector_Spaces.thy --- a/src/HOL/Real_Vector_Spaces.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/Real_Vector_Spaces.thy Wed Apr 01 22:40:41 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 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/Rings.thy --- a/src/HOL/Rings.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/Rings.thy Wed Apr 01 22:40:41 2015 +0200 @@ -1260,6 +1260,10 @@ "\x - a\ < r \ a - r < x \ x < a + r" by (auto simp add: diff_less_eq ac_simps abs_less_iff) +lemma abs_diff_le_iff: + "\x - a\ \ r \ a - r \ x \ x \ a + r" + by (auto simp add: diff_le_eq ac_simps abs_le_iff) + end hide_fact (open) comm_mult_left_mono comm_mult_strict_left_mono distrib diff -r 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Wed Apr 01 22:40:41 2015 +0200 @@ -155,6 +155,7 @@ val Inr_const: typ -> typ -> term val mk_tuple_balanced: term list -> term val mk_tuple1_balanced: typ list -> term list -> term + val abs_curried_balanced: typ list -> term -> term val mk_case_sum: term * term -> term val mk_case_sumN: term list -> term @@ -437,6 +438,10 @@ val mk_tuple_balanced = mk_tuple1_balanced []; +fun abs_curried_balanced Ts t = + t $ mk_tuple1_balanced (List.rev Ts) (map Bound (length Ts - 1 downto 0)) + |> fold_rev (Term.abs o pair Name.uu) Ts; + fun mk_sumprod_balanced T n k ts = Sum_Tree.mk_inj T n k (mk_tuple_balanced ts); fun mk_absumprod absT abs0 n k ts = diff -r 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Wed Apr 01 22:40:41 2015 +0200 @@ -964,10 +964,6 @@ (if exists has_call corec_args then nonprimitive_corec ctxt [] else extra_variable ctxt [] (hd bad)); - fun currys [] t = t - | currys Ts t = t $ mk_tuple1_balanced (List.rev Ts) (map Bound (length Ts - 1 downto 0)) - |> fold_rev (Term.abs o pair Name.uu) Ts; - val excludess' = disc_eqnss |> map (map (fn x => (#fun_args x, #ctr_no x, #prems x, #auto_gen x)) @@ -980,8 +976,7 @@ ||> curry Logic.list_all (map dest_Free fun_args)))); in map (Term.list_comb o rpair corec_args) corecs - |> map2 (fn Ts => fn t => if length Ts = 0 then t $ HOLogic.unit else t) arg_Tss - |> map2 currys arg_Tss + |> map2 abs_curried_balanced arg_Tss |> (fn ts => Syntax.check_terms ctxt ts handle ERROR _ => nonprimitive_corec ctxt []) |> @{map 3} (fn b => fn mx => fn t => ((b, mx), ((Binding.concealed (Thm.def_binding b), []), t))) diff -r 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/Tools/numeral_simprocs.ML --- a/src/HOL/Tools/numeral_simprocs.ML Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/Tools/numeral_simprocs.ML Wed Apr 01 22:40:41 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 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/Transcendental.thy Wed Apr 01 22:40:41 2015 +0200 @@ -1130,6 +1130,9 @@ apply (simp add: scaleR_conv_of_real) done +corollary exp_in_Reals [simp]: "z \ \ \ exp z \ \" + by (metis Reals_cases Reals_of_real exp_of_real) + lemma exp_not_eq_zero [simp]: "exp x \ 0" proof have "exp x * exp (- x) = 1" by (simp add: exp_add_commuting[symmetric]) @@ -2228,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" @@ -2432,6 +2435,9 @@ by blast qed +corollary sin_in_Reals [simp]: "z \ \ \ sin z \ \" + by (metis Reals_cases Reals_of_real sin_of_real) + lemma cos_of_real: fixes x::real shows "cos (of_real x) = of_real (cos x)" @@ -2450,6 +2456,9 @@ by blast qed +corollary cos_in_Reals [simp]: "z \ \ \ cos z \ \" + by (metis Reals_cases Reals_of_real cos_of_real) + lemma diffs_sin_coeff: "diffs sin_coeff = cos_coeff" by (simp add: diffs_def sin_coeff_Suc real_of_nat_def del: of_nat_Suc) @@ -3100,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) @@ -3661,6 +3670,16 @@ definition tan :: "'a \ 'a::{real_normed_field,banach}" where "tan = (\x. sin x / cos x)" +lemma tan_of_real: + 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}" + shows "z \ \ \ tan z \ \" + by (simp add: tan_def) + lemma tan_zero [simp]: "tan 0 = 0" by (simp add: tan_def) @@ -3711,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) @@ -3994,6 +4013,27 @@ apply (rule sin_total, auto) done +lemma arcsin_0 [simp]: "arcsin 0 = 0" + using arcsin_sin [of 0] + by simp + +lemma arcsin_1 [simp]: "arcsin 1 = pi/2" + using arcsin_sin [of "pi/2"] + by simp + +lemma arcsin_minus_1 [simp]: "arcsin (-1) = - (pi/2)" + using arcsin_sin [of "-pi/2"] + by simp + +lemma arcsin_minus: "-1 \ x \ x \ 1 \ arcsin(-x) = -arcsin x" + by (metis (no_types, hide_lams) arcsin arcsin_sin minus_minus neg_le_iff_le sin_minus) + +lemma arcsin_eq_iff: "abs x \ 1 \ abs y \ 1 \ (arcsin x = arcsin y \ x = y)" + by (metis abs_le_interval_iff arcsin) + +lemma cos_arcsin_nonzero: "-1 < x \ x < 1 \ cos(arcsin x) \ 0" + using arcsin_lt_bounded cos_gt_zero_pi by force + lemma arccos: "\-1 \ y; y \ 1\ \ 0 \ arccos y & arccos y \ pi & cos(arccos y) = y" @@ -4012,8 +4052,7 @@ by (blast dest: arccos) lemma arccos_lt_bounded: - "\-1 < y; y < 1\ - \ 0 < arccos y & arccos y < pi" + "\-1 < y; y < 1\ \ 0 < arccos y & arccos y < pi" apply (frule order_less_imp_le) apply (frule_tac y = y in order_less_imp_le) apply (frule arccos_bounded, auto) @@ -4062,17 +4101,27 @@ lemma arccos_1 [simp]: "arccos 1 = 0" using arccos_cos by force -lemma arctan [simp]: "- (pi/2) < arctan y & arctan y < pi/2 & tan (arctan y) = y" +lemma arccos_minus_1 [simp]: "arccos(-1) = pi" + by (metis arccos_cos cos_pi order_refl pi_ge_zero) + +lemma arccos_minus: "-1 \ x \ x \ 1 \ arccos(-x) = pi - arccos x" + by (metis arccos_cos arccos_cos2 cos_minus_pi cos_total diff_le_0_iff_le le_add_same_cancel1 + minus_diff_eq uminus_add_conv_diff) + +lemma sin_arccos_nonzero: "-1 < x \ x < 1 \ ~(sin(arccos x) = 0)" + using arccos_lt_bounded sin_gt_zero by force + +lemma arctan: "- (pi/2) < arctan y & arctan y < pi/2 & tan (arctan y) = y" unfolding arctan_def by (rule theI' [OF tan_total]) lemma tan_arctan: "tan (arctan y) = y" - by auto + by (simp add: arctan) lemma arctan_bounded: "- (pi/2) < arctan y & arctan y < pi/2" by (auto simp only: arctan) lemma arctan_lbound: "- (pi/2) < arctan y" - by auto + by (simp add: arctan) lemma arctan_ubound: "arctan y < pi/2" by (auto simp only: arctan) @@ -4093,7 +4142,7 @@ lemma arctan_minus: "arctan (- x) = - arctan x" apply (rule arctan_unique) apply (simp only: neg_less_iff_less arctan_ubound) - apply (metis minus_less_iff arctan_lbound, simp) + apply (metis minus_less_iff arctan_lbound, simp add: arctan) done lemma cos_arctan_not_zero [simp]: "cos (arctan x) \ 0" @@ -4109,7 +4158,7 @@ have "(cos (arctan x))\<^sup>2 * (1 + (tan (arctan x))\<^sup>2) = 1" unfolding tan_def by (simp add: distrib_left power_divide) thus "(cos (arctan x))\<^sup>2 = (1 / sqrt (1 + x\<^sup>2))\<^sup>2" - using `0 < 1 + x\<^sup>2` by (simp add: power_divide eq_divide_eq) + using `0 < 1 + x\<^sup>2` by (simp add: arctan power_divide eq_divide_eq) qed lemma sin_arctan: "sin (arctan x) = x / sqrt (1 + x\<^sup>2)" @@ -4118,7 +4167,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]) @@ -4202,7 +4251,7 @@ lemma isCont_arctan: "isCont arctan x" apply (rule arctan_lbound [of x, THEN dense, THEN exE], clarify) apply (rule arctan_ubound [of x, THEN dense, THEN exE], clarify) - apply (subgoal_tac "isCont arctan (tan (arctan x))", simp) + apply (subgoal_tac "isCont arctan (tan (arctan x))", simp add: arctan) apply (erule (1) isCont_inverse_function2 [where f=tan]) apply (metis arctan_tan order_le_less_trans order_less_le_trans) apply (metis cos_gt_zero_pi isCont_tan order_less_le_trans less_le) @@ -4243,10 +4292,9 @@ apply (rule DERIV_inverse_function [where f=tan and a="x - 1" and b="x + 1"]) apply (rule DERIV_cong [OF DERIV_tan]) apply (rule cos_arctan_not_zero) - apply (simp add: power_inverse tan_sec [symmetric]) + apply (simp add: arctan power_inverse tan_sec [symmetric]) apply (subgoal_tac "0 < 1 + x\<^sup>2", simp) - apply (simp add: add_pos_nonneg) - apply (simp, simp, simp, rule isCont_arctan) + apply (simp_all add: add_pos_nonneg arctan isCont_arctan) done declare @@ -4256,12 +4304,12 @@ lemma filterlim_tan_at_right: "filterlim tan at_bot (at_right (- pi/2))" by (rule filterlim_at_bot_at_right[where Q="\x. - pi/2 < x \ x < pi/2" and P="\x. True" and g=arctan]) - (auto simp: le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1 + (auto simp: arctan le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1 intro!: tan_monotone exI[of _ "pi/2"]) lemma filterlim_tan_at_left: "filterlim tan at_top (at_left (pi/2))" by (rule filterlim_at_top_at_left[where Q="\x. - pi/2 < x \ x < pi/2" and P="\x. True" and g=arctan]) - (auto simp: le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1 + (auto simp: arctan le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1 intro!: tan_monotone exI[of _ "pi/2"]) lemma tendsto_arctan_at_top: "(arctan ---> (pi/2)) at_top" @@ -4293,6 +4341,12 @@ subsection{* Prove Totality of the Trigonometric Functions *} +lemma cos_arccos_abs: "\y\ \ 1 \ cos (arccos y) = y" + by (simp add: abs_le_iff) + +lemma sin_arccos_abs: "\y\ \ 1 \ sin (arccos y) = sqrt (1 - y\<^sup>2)" + by (simp add: sin_arccos abs_le_iff) + lemma sin_mono_less_eq: "\-(pi/2) \ x; x \ pi/2; -(pi/2) \ y; y \ pi/2\ \ (sin(x) < sin(y) \ x < y)" by (metis not_less_iff_gr_or_eq sin_monotone_2pi) @@ -4301,12 +4355,12 @@ \ (sin(x) \ sin(y) \ x \ y)" by (meson leD le_less_linear sin_monotone_2pi sin_monotone_2pi_le) -lemma sin_inj_pi: "-(pi/2) \ x ==> x \ pi/2 ==> - -(pi/2) \ y ==> y \ pi/2 ==> sin(x) = sin(y) \ x = y" +lemma sin_inj_pi: + "\-(pi/2) \ x; x \ pi/2;-(pi/2) \ y; y \ pi/2; sin(x) = sin(y)\ \ x = y" by (metis arcsin_sin) -lemma cos_mono_lt_eq: "0 \ x ==> x \ pi ==> 0 \ y ==> y \ pi - \ (cos(x) < cos(y) \ y < x)" +lemma cos_mono_less_eq: + "0 \ x ==> x \ pi ==> 0 \ y ==> y \ pi \ (cos(x) < cos(y) \ y < x)" by (meson cos_monotone_0_pi cos_monotone_0_pi_le leD le_less_linear) lemma cos_mono_le_eq: "0 \ x ==> x \ pi ==> 0 \ y ==> y \ pi @@ -4388,6 +4442,40 @@ done qed +lemma arcsin_less_mono: "abs x \ 1 \ abs y \ 1 \ arcsin x < arcsin y \ x < y" + apply (rule trans [OF sin_mono_less_eq [symmetric]]) + using arcsin_ubound arcsin_lbound + apply (auto simp: ) + done + +lemma arcsin_le_mono: "abs x \ 1 \ abs y \ 1 \ arcsin x \ arcsin y \ x \ y" + using arcsin_less_mono not_le by blast + +lemma arcsin_less_arcsin: "-1 \ x \ x < y \ y \ 1 \ arcsin x < arcsin y" + using arcsin_less_mono by auto + +lemma arcsin_le_arcsin: "-1 \ x \ x \ y \ y \ 1 \ arcsin x \ arcsin y" + using arcsin_le_mono by auto + +lemma arccos_less_mono: "abs x \ 1 \ abs y \ 1 \ (arccos x < arccos y \ y < x)" + apply (rule trans [OF cos_mono_less_eq [symmetric]]) + using arccos_ubound arccos_lbound + apply (auto simp: ) + done + +lemma arccos_le_mono: "abs x \ 1 \ abs y \ 1 \ arccos x \ arccos y \ y \ x" + using arccos_less_mono [of y x] + by (simp add: not_le [symmetric]) + +lemma arccos_less_arccos: "-1 \ x \ x < y \ y \ 1 \ arccos y < arccos x" + using arccos_less_mono by auto + +lemma arccos_le_arccos: "-1 \ x \ x \ y \ y \ 1 \ arccos y \ arccos x" + using arccos_le_mono by auto + +lemma arccos_eq_iff: "abs x \ 1 & abs y \ 1 \ (arccos x = arccos y \ x = y)" + using cos_arccos_abs by fastforce + subsection {* Machins formula *} lemma arctan_one: "arctan 1 = pi / 4" @@ -4399,7 +4487,8 @@ proof show "- (pi / 4) < arctan x \ arctan x < pi / 4 \ tan (arctan x) = x" unfolding arctan_one [symmetric] arctan_minus [symmetric] - unfolding arctan_less_iff using assms by auto + unfolding arctan_less_iff using assms by (auto simp add: arctan) + qed lemma arctan_add: @@ -4417,7 +4506,7 @@ from add_le_less_mono [OF this] show 2: "arctan x + arctan y < pi / 2" by simp show "tan (arctan x + arctan y) = (x + y) / (1 - x * y)" - using cos_gt_zero_pi [OF 1 2] by (simp add: tan_add) + using cos_gt_zero_pi [OF 1 2] by (simp add: arctan tan_add) qed theorem machin: "pi / 4 = 4 * arctan (1/5) - arctan (1 / 239)" @@ -4523,16 +4612,6 @@ (is "summable (?c x)") by (rule summable_Leibniz(1), rule zeroseq_arctan_series[OF assms], rule monoseq_arctan_series[OF assms]) -lemma less_one_imp_sqr_less_one: - fixes x :: real - assumes "\x\ < 1" - shows "x\<^sup>2 < 1" -proof - - have "\x\<^sup>2\ < 1" - by (metis abs_power2 assms pos2 power2_abs power_0 power_strict_decreasing zero_eq_power2 zero_less_abs_iff) - thus ?thesis using zero_le_power2 by auto -qed - lemma DERIV_arctan_series: assumes "\ x \ < 1" shows "DERIV (\ x'. \ k. (-1)^k * (1 / real (k*2+1) * x' ^ (k*2+1))) x :> (\ k. (-1)^k * x^(k*2))" @@ -4549,7 +4628,7 @@ { fix x :: real assume "\x\ < 1" - hence "x\<^sup>2 < 1" by (rule less_one_imp_sqr_less_one) + hence "x\<^sup>2 < 1" by (simp add: abs_square_less_1) have "summable (\ n. (- 1) ^ n * (x\<^sup>2) ^n)" by (rule summable_Leibniz(1), auto intro!: LIMSEQ_realpow_zero monoseq_realpow `x\<^sup>2 < 1` order_less_imp_le[OF `x\<^sup>2 < 1`]) hence "summable (\ n. (- 1) ^ n * x^(2*n))" unfolding power_mult . @@ -4657,7 +4736,7 @@ hence "\x\ < r" by auto hence "\x\ < 1" using `r < 1` by auto have "\ - (x\<^sup>2) \ < 1" - using less_one_imp_sqr_less_one[OF `\x\ < 1`] by auto + using abs_square_less_1 `\x\ < 1` by auto hence "(\ n. (- (x\<^sup>2)) ^ n) sums (1 / (1 - (- (x\<^sup>2))))" unfolding real_norm_def[symmetric] by (rule geometric_sums) hence "(?c' x) sums (1 / (1 - (- (x\<^sup>2))))" @@ -4873,7 +4952,7 @@ show "- (pi / 2) < sgn x * pi / 2 - arctan x" using arctan_bounded [of x] assms unfolding sgn_real_def - apply (auto simp add: algebra_simps) + apply (auto simp add: arctan algebra_simps) apply (drule zero_less_arctan_iff [THEN iffD2]) apply arith done @@ -4902,12 +4981,6 @@ apply (simp add: power_divide divide_le_eq not_sum_power2_lt_zero) done -lemma cos_arccos_abs: "\y\ \ 1 \ cos (arccos y) = y" - by (simp add: abs_le_iff) - -lemma sin_arccos_abs: "\y\ \ 1 \ sin (arccos y) = sqrt (1 - y\<^sup>2)" - by (simp add: sin_arccos abs_le_iff) - lemmas cos_arccos_lemma1 = cos_arccos_abs [OF cos_x_y_le_one] lemmas sin_arccos_lemma1 = sin_arccos_abs [OF cos_x_y_le_one] diff -r 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/ex/Approximations.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Approximations.thy Wed Apr 01 22:40:41 2015 +0200 @@ -0,0 +1,39 @@ +section {* Binary Approximations to Constants *} + +theory Approximations +imports "~~/src/HOL/Multivariate_Analysis/Complex_Transcendental" + +begin + +declare of_real_numeral [simp] + +subsection{*Approximation to pi*} + +lemma sin_pi6_straddle: + assumes "0 \ a" "a \ b" "b \ 4" "sin(a/6) \ 1/2" "1/2 \ sin(b/6)" + shows "a \ pi \ pi \ b" +proof - + have *: "\x::real. 0 < x & x < 7/5 \ 0 < sin x" + using pi_ge_two + by (auto intro: sin_gt_zero) + have ab: "(b \ pi * 3 \ pi \ b)" "(a \ pi * 3 \ a \ pi)" + using sin_mono_le_eq [of "pi/6" "b/6"] sin_mono_le_eq [of "a/6" "pi/6"] assms + by (simp_all add: sin_30 power.power_Suc norm_divide) + show ?thesis + using assms Taylor_sin [of "a/6" 0] pi_ge_two + by (auto simp: sin_30 power.power_Suc norm_divide intro: ab) +qed + +(*32-bit approximation. SLOW simplification steps: big calculations with the rewriting engine*) +lemma pi_approx_32: "abs(pi - 13493037705/4294967296) \ inverse(2 ^ 32)" + apply (simp only: abs_diff_le_iff) + apply (rule sin_pi6_straddle, simp_all) + using Taylor_sin [of "1686629713/3221225472" 11] + apply (simp add: in_Reals_norm sin_coeff_def Re_sin atMost_nat_numeral fact_numeral) + apply (simp only: pos_le_divide_eq [symmetric]) + using Taylor_sin [of "6746518853/12884901888" 11] + apply (simp add: in_Reals_norm sin_coeff_def Re_sin atMost_nat_numeral fact_numeral) + apply (simp only: pos_le_divide_eq [symmetric] pos_divide_le_eq [symmetric]) + done + +end diff -r 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/ex/BinEx.thy --- a/src/HOL/ex/BinEx.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/ex/BinEx.thy Wed Apr 01 22:40:41 2015 +0200 @@ -78,6 +78,9 @@ lemma "- (2*i) + 3 + (2*i + 4) = (0::int)" apply simp oops +(*Tobias's example dated 2015-03-02*) +lemma "(pi * (real u * 2) = pi * (real (xa v) * - 2))" +apply simp oops subsection {* Arithmetic Method Tests *} diff -r 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/ex/Dedekind_Real.thy --- a/src/HOL/ex/Dedekind_Real.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/ex/Dedekind_Real.thy Wed Apr 01 22:40:41 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 6afbe5a99139 -r 9d70a39d1cf3 src/HOL/ex/Simproc_Tests.thy --- a/src/HOL/ex/Simproc_Tests.thy Wed Apr 01 22:40:07 2015 +0200 +++ b/src/HOL/ex/Simproc_Tests.thy Wed Apr 01 22:40:41 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"