--- 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:
--- 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 \<Rightarrow> (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> 'a process"
where
"random_process s f n =
@@ -2098,6 +2102,9 @@
else
Choice (random_process (every_snd s) (f \<circ> f) (f n))
(random_process (every_snd (stl s)) (f \<circ> 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}\]
--- 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 \<le> 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 \<le> 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 (\<lambda>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 "(\<Prod>i\<Colon>nat\<in>{0\<Colon>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 "\<Prod>i<k. (n - i) / (k - i)"} *}
lemma gbinomial_altdef_of_nat:
fixes k :: nat
- and x :: "'a :: {field_char_0,field_inverse_zero}"
+ and x :: "'a :: {field_char_0,field}"
shows "x gchoose k = (\<Prod>i<k. (x - of_nat i) / of_nat (k - i) :: 'a)"
proof -
have "(x gchoose k) = (\<Prod>i<k. x - of_nat i) / of_nat (fact k)"
@@ -737,7 +731,7 @@
lemma gbinomial_ge_n_over_k_pow_k:
fixes k :: nat
- and x :: "'a :: linordered_field_inverse_zero"
+ and x :: "'a :: linordered_field"
assumes "of_nat k \<le> x"
shows "(x / of_nat k :: 'a) ^ k \<le> 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 \<le> n"
shows "of_nat (n choose k) = (\<Prod>i<k. of_nat (n - i) / of_nat (k - i) :: 'a)"
using assms
@@ -775,7 +769,7 @@
lemma binomial_ge_n_over_k_pow_k:
fixes k n :: nat
- and x :: "'a :: linordered_field_inverse_zero"
+ and x :: "'a :: linordered_field"
assumes "k \<le> n"
shows "(of_nat n / of_nat k :: 'a) ^ k \<le> of_nat (n choose k)"
by (simp add: assms gbinomial_ge_n_over_k_pow_k binomial_gbinomial of_nat_diff)
--- 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 \<Longrightarrow> Re (x ^ n) = Re x ^ n "
+lemma Re_power_real [simp]: "Im x = 0 \<Longrightarrow> Re (x ^ n) = Re x ^ n "
by (induct n) simp_all
-lemma Im_power_real: "Im x = 0 \<Longrightarrow> Im (x ^ n) = 0"
+lemma Im_power_real [simp]: "Im x = 0 \<Longrightarrow> 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 \<Longrightarrow> Re x \<le> 0 \<Longrightarrow> csqrt x = \<i> * sqrt \<bar>Re x\<bar>"
by (simp add: complex_eq_iff norm_complex_def)
+lemma of_real_sqrt: "x \<ge> 0 \<Longrightarrow> 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
--- 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 \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a"
+primrec Itm :: "'a::{field_char_0, field} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> '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 \<Longrightarrow> isnpoly c \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> allpolys isnpoly s \<Longrightarrow> 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 \<Longrightarrow> 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') \<Longrightarrow> 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 \<Longrightarrow> 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 \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> bool"
+primrec Ifm ::"'a::{linordered_field} list \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 "\<exists>(x::'a::{linordered_field_inverse_zero}). y \<noteq> -1 \<longrightarrow> (y + 1) * x < 0"
+lemma "\<exists>(x::'a::{linordered_field}). y \<noteq> -1 \<longrightarrow> (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 "\<exists>(x::'a::{linordered_field_inverse_zero}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
+lemma "\<exists>(x::'a::{linordered_field}). y \<noteq> -1 \<longrightarrow> (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 "\<exists>(r::'a::{linordered_field_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0"
+lemma "\<exists>(r::'a::{linordered_field, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0"
proof-
- have "(\<exists>(r::'a::{linordered_field_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \<longleftrightarrow> (\<exists>(r::'a::{linordered_field_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \<and> 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \<longleftrightarrow> ?rhs")
+ have "(\<exists>(r::'a::{linordered_field, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \<longleftrightarrow> (\<exists>(r::'a::{linordered_field, number_ring}). 0 < r \<and> r < 1 \<and> 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \<and> 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \<longleftrightarrow> ?rhs")
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 \<le> (1+t)*y \<and> (1 - t)*y \<le> (1+t)*x --> 0 \<le> 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 \<le> (1+t)*y \<and> (1 - t)*y \<le> (1+t)*x --> 0 \<le> y"
+apply (frpar type: "'a::{linordered_field, number_ring}" pars: "t::'a::{linordered_field, number_ring}")
oops
*)
text{* Collins/Jones Problem *}
(*
-lemma "\<exists>(r::'a::{linordered_field_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0"
+lemma "\<exists>(r::'a::{linordered_field, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0"
proof-
- have "(\<exists>(r::'a::{linordered_field_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \<longleftrightarrow> (\<exists>(r::'a::{linordered_field_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \<and> 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \<longleftrightarrow> ?rhs")
+ have "(\<exists>(r::'a::{linordered_field, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \<longleftrightarrow> (\<exists>(r::'a::{linordered_field, number_ring}). 0 < r \<and> r < 1 \<and> 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \<and> 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \<longleftrightarrow> ?rhs")
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 \<le> (1+t)*y \<and> (1 - t)*y \<le> (1+t)*x --> 0 \<le> 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 \<le> (1+t)*y \<and> (1 - t)*y \<le> (1+t)*x --> 0 \<le> 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
--- 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 \<Longrightarrow> (INum x = (0::'a::{field_char_0, field_inverse_zero})) = (x = 0\<^sub>N)"
+ "isnormNum x \<Longrightarrow> (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 \<or> b = 0"
@@ -228,7 +228,7 @@
qed
lemma INum_normNum_iff:
- "(INum x ::'a::{field_char_0, field_inverse_zero}) = INum y \<longleftrightarrow> normNum x = normNum y"
+ "(INum x ::'a::{field_char_0, field}) = INum y \<longleftrightarrow> normNum x = normNum y"
(is "?lhs = ?rhs")
proof -
have "normNum x = normNum y \<longleftrightarrow> (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 \<div>\<^sub>N y) = INum x / (INum y ::'a :: {field_char_0, field_inverse_zero})"
+lemma Ndiv[simp]: "INum (x \<div>\<^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}) \<le> 0) = 0\<ge>\<^sub>N x"
+ shows "((INum x :: 'a :: {field_char_0, linordered_field}) \<le> 0) = 0\<ge>\<^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}) \<ge> 0) = 0\<le>\<^sub>N x"
+ shows "((INum x :: 'a :: {field_char_0, linordered_field}) \<ge> 0) = 0\<le>\<^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})\<le> INum y) = (x \<le>\<^sub>N y)"
+ shows "((INum x :: 'a :: {field_char_0, linordered_field})\<le> INum y) = (x \<le>\<^sub>N y)"
proof -
have "((INum x ::'a) \<le> INum y) = (INum (x -\<^sub>N y) \<le> (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 \<longleftrightarrow> 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 \<longleftrightarrow> x = 0\<^sub>N \<or> y = 0\<^sub>N"
proof -
--- 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 \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0,field_inverse_zero,power}"
+primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> '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 \<Rightarrow> 'a list \<Rightarrow>'a::{field_char_0,field_inverse_zero,power}"
+abbreviation Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{field_char_0,field,power}"
("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
where "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<equiv> 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 \<le> 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 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> 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 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> p *\<^sub>p q = 0\<^sub>p \<longleftrightarrow> p = 0\<^sub>p \<or> 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 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> m \<le> min n0 n1 \<Longrightarrow>
degreen (p *\<^sub>p q) m = (if p = 0\<^sub>p \<or> 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 \<Longrightarrow> isnpoly q \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> p -\<^sub>p q = 0\<^sub>p \<longleftrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 :"\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a::{field_char_0,field_inverse_zero, power})"
+ and eq :"\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^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 "(\<forall>bs. \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (\<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup> :: 'a::{field_char_0,field_inverse_zero,power})) \<longleftrightarrow> p = q"
+ shows "(\<forall>bs. \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (\<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup> :: 'a::{field_char_0,field,power})) \<longleftrightarrow> p = q"
proof auto
assume H: "\<forall>bs. (\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> ::'a) = \<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup>"
then have "\<forall>bs.\<lparr>p -\<^sub>p q\<rparr>\<^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) = (\<lambda>x:: 'a ::{field_char_0,field_inverse_zero}. \<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup>)"
+ "poly (poly_nate bs p) = (\<lambda>x:: 'a ::{field_char_0,field}. \<lparr>p\<rparr>\<^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 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> p \<noteq> 0\<^sub>p \<Longrightarrow> q \<noteq> 0\<^sub>p \<Longrightarrow> 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) \<le> 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 "\<forall>bs :: 'a::{field_char_0,field_inverse_zero} list.
+ from asp have "\<forall>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 "\<forall>bs :: 'a::{field_char_0,field_inverse_zero} list.
+ then have "\<forall>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 "\<forall>bs :: 'a::{field_char_0,field_inverse_zero} list.
+ then have "\<forall>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 "\<forall>bs:: 'a::{field_char_0,field_inverse_zero} list.
+ then have "\<forall>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 "\<forall>bs:: 'a::{field_char_0,field_inverse_zero} list.
+ then have "\<forall>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 "\<forall>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 "\<forall>bs:: 'a::{field_char_0,field} list. Ipoly bs s = Ipoly bs ?p'"
by simp
- then have "\<forall>bs:: 'a::{field_char_0,field_inverse_zero} list. Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)"
+ then have "\<forall>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:"\<forall>bs :: 'a::{field_char_0,field_inverse_zero} list.
+ then have ieq:"\<forall>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: "\<forall>bs :: 'a::{field_char_0,field_inverse_zero} list.
+ then have hth: "\<forall>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 \<noteq> 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
--- 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
- "\<exists>(y::'a::{linordered_field_inverse_zero}) <2. x + 3* y < 0 \<and> x - y >0"
+ "\<exists>(y::'a::{linordered_field}) <2. x + 3* y < 0 \<and> 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) \<le> 0 )"
+lemma "EX x. (ALL (y::'a::{linordered_field}). y < 2 --> 2*(y - x) \<le> 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 \<noteq> 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 \<noteq> 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) \<noteq> 0 \<longrightarrow> (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) \<noteq> 0 \<longrightarrow> (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
--- 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 @@
\<Longrightarrow> (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) \<Longrightarrow> (f has_field_derivative f') (at x within s)"
+ using DERIV_subset by blast
+
abbreviation (input)
DERIV :: "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 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) \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow>
- ((\<lambda>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 \<noteq> 0"
+ shows "((\<lambda>x. inverse (f x)) has_field_derivative - (inverse (f x) * D * inverse (f x))) (at x within s)"
+proof -
+ have "(f has_derivative (\<lambda>x. x * D)) = (f has_derivative op * D)"
+ by (rule arg_cong [of "\<lambda>x. x * D"]) (simp add: fun_eq_iff)
+ with assms have "(f has_derivative (\<lambda>x. x * D)) (at x within s)"
+ by (auto dest!: has_field_derivative_imp_has_derivative)
+ then show ?thesis using `f x \<noteq> 0`
+ by (auto intro: has_derivative_imp_has_field_derivative has_derivative_inverse)
+qed
text {* Power of @{text "-1"} *}
--- 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) \<Rightarrow> a\<^sub>1 | (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>1 | _ \<Rightarrow> 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
--- 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 \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
assumes right_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> 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 \<noteq> 0 \<Longrightarrow> - (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 \<noteq> 0 \<Longrightarrow> 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 \<le> 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)
--- 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 \<in> 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 \<Longrightarrow> setprod (inverse \<circ> 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 \<Longrightarrow> (\<Prod>x\<in>A. f x / g x) = setprod f A / setprod g A"
using setprod_inversef [of A g] by (simp add: divide_inverse setprod.distrib)
--- 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 \<Longrightarrow> True) \<equiv> Trueprop True"
+by default (intro TrueI)
+
+lemma False_implies_equals: "(False \<Longrightarrow> P) \<equiv> 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))"
--- 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 \<noteq> 0 \<Longrightarrow> f \<in> O(\<lambda>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 = "\<lambda>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]: "(\<lambda>x. c) *o O(f) \<subseteq> O(f)"
--- 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:
--- 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<..<pi/2} UNIV"
- using arctan_ubound by (intro bij_betw_byWitness[where f'=arctan]) (auto simp: arctan_tan)
+ using arctan_ubound by (intro bij_betw_byWitness[where f'=arctan]) (auto simp: arctan arctan_tan)
lemma uncountable_open_interval:
fixes a b :: real assumes ab: "a < b"
--- a/src/HOL/Library/Convex.thy Wed Apr 01 22:40:07 2015 +0200
+++ b/src/HOL/Library/Convex.thy Wed Apr 01 22:40:41 2015 +0200
@@ -121,6 +121,9 @@
then show "convex {a<..<b}" by (simp only: convex_Int 3 4)
qed
+lemma convex_Reals: "convex Reals"
+ by (simp add: convex_def scaleR_conv_of_real)
+
subsection {* Explicit expressions for convexity in terms of arbitrary sums. *}
lemma convex_setsum:
--- a/src/HOL/Library/Formal_Power_Series.thy Wed Apr 01 22:40:07 2015 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Wed Apr 01 22:40:41 2015 +0200
@@ -2555,9 +2555,7 @@
let ?KM = "{(k,m). k + m \<le> n}"
let ?f = "\<lambda>s. UNION {(0::nat)..s} (\<lambda>i. {(i,s - i)})"
have th0: "?KM = UNION {0..n} ?f"
- apply (simp add: set_eq_iff)
- apply presburger (* FIXME: slow! *)
- done
+ by (auto simp add: set_eq_iff Bex_def)
show "?l = ?r "
unfolding th0
apply (subst setsum.UNION_disjoint)
@@ -3230,11 +3228,11 @@
then obtain m where m: "n = Suc m" by (cases n) auto
from k0 obtain h where h: "k = Suc h" by (cases k) auto
{
- assume kn: "k = n"
+ assume "k = n"
then have "b gchoose (n - k) =
(?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k)"
- using kn pochhammer_minus'[where k=k and n=n and b=b]
- apply (simp add: pochhammer_same)
+ using pochhammer_minus'[where k=k and b=b]
+ apply (simp add: pochhammer_same)
using bn0
apply (simp add: field_simps power_add[symmetric])
done
@@ -3357,10 +3355,10 @@
apply (auto simp add: of_nat_diff algebra_simps)
done
have th0: "pochhammer (- (?a + ?b)) n = (- 1)^n * pochhammer (c - a) n"
- unfolding pochhammer_minus[OF le_refl]
+ unfolding pochhammer_minus
by (simp add: algebra_simps)
have th1: "pochhammer (- ?b) n = (- 1)^n * pochhammer c n"
- unfolding pochhammer_minus[OF le_refl]
+ unfolding pochhammer_minus
by simp
have nz: "pochhammer c n \<noteq> 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 (\<lambda>n. (foldl (\<lambda>r a. r* pochhammer a n) 1 as * c^n) /
(foldl (\<lambda>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 \<le> 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 \<le> 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 "\<lambda>x. x < e"]
have "eventually (\<lambda>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 (\<lambda>x. M i \<le> x) sequentially" by (auto simp: eventually_sequentially)
--- 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 \<le> r"
--- 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 :: "_ \<Rightarrow> 'a\<Colon>{real_normed_div_algebra, division_ring_inverse_zero}"
+ fixes x :: "_ \<Rightarrow> 'a\<Colon>{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 \<Rightarrow> 'b\<Colon>{real_normed_div_algebra, division_ring_inverse_zero}"
+ fixes g :: "'a \<Rightarrow> 'b\<Colon>{real_normed_div_algebra, division_ring}"
shows "(LIM x F. inverse (g x) :> at 0) \<longleftrightarrow> (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 \<Colon> {real_normed_field,field_inverse_zero}"
+ fixes x :: "'a \<Colon> {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 \<longleftrightarrow> ((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 "((\<lambda>x. f(1 / x)) ---> l) (at (0::'a)) \<Longrightarrow> (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 :: "_ \<Rightarrow> 'a\<Colon>{real_normed_div_algebra, division_ring_inverse_zero}"
+ fixes f :: "_ \<Rightarrow> 'a\<Colon>{real_normed_div_algebra, division_ring}"
assumes f: "(f ---> c) F"
assumes g: "LIM x F. g x :> at_infinity"
shows "((\<lambda>x. f x / g x) ---> 0) F"
--- 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((\<lambda>x. 1 / f x) * (f * g))"
by (rule bigo_mult2)
also have "(\<lambda>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 "(\<lambda>x. (1\<Colon>'b) / f x) * h : O(g)".
then have "f * ((\<lambda>x. (1\<Colon>'b) / f x) * h) : f *o O(g)"
by auto
@@ -458,8 +457,8 @@
using F3 by metis
hence "\<exists>(v\<Colon>'a) (u\<Colon>'a) SKF\<^sub>7\<Colon>'a \<Rightarrow> 'b. \<bar>inverse c\<bar> * \<bar>g (SKF\<^sub>7 (u * v))\<bar> \<le> u * (v * \<bar>f (SKF\<^sub>7 (u * v))\<bar>)"
by (metis mult_left_mono)
- thus "\<exists>ca\<Colon>'a. \<forall>x\<Colon>'b. \<bar>inverse c\<bar> * \<bar>g x\<bar> \<le> ca * \<bar>f x\<bar>"
- using A2 F4 by (metis mult.assoc mult_left_mono)
+ then show "\<exists>ca\<Colon>'a. \<forall>x\<Colon>'b. inverse \<bar>c\<bar> * \<bar>g x\<bar> \<le> ca * \<bar>f x\<bar>"
+ using A2 F4 by (metis F1 `0 < \<bar>inverse c\<bar>` linordered_field_class.sign_simps(23) mult_le_cancel_left_pos)
qed
lemma bigo_const_mult6 [intro]: "(\<lambda>x. c) *o O(f) <= O(f)"
--- 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 "(\<Sum>i\<in>Basis. (dist (clamp a b y \<bullet> i) (clamp a b x \<bullet> i))\<^sup>2)
\<le> (\<Sum>i\<in>Basis. (dist (y \<bullet> i) (x \<bullet> 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)
--- 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 \<noteq> 0" "r\<noteq>0"
+ shows "cmod (z + r) < cmod z + abs r"
+proof (cases z)
+ case (Complex x y)
+ have "r * x / \<bar>r\<bar> < 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 \<noteq> 0 \<Longrightarrow> x\<noteq>0 \<Longrightarrow> 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 \<Longrightarrow> \<bar>Re z\<bar> < 1"
+ shows "(cmod z)\<^sup>2 < 1 + cmod (1 - z\<^sup>2)"
+ using assms
+ apply (cases "Im z = 0 \<or> 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 "(\<lambda>n. (cos_coeff n + ii * sin_coeff n) * z^n)
+ have "(\<lambda>n. (cos_coeff n + ii * sin_coeff n) * z^n)
= (\<lambda>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 "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) sums (exp (cnj z))" .
moreover have "(\<lambda>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 \<in> \<real> \<Longrightarrow> exp z \<in> \<real>"
- by (metis Reals_cases Reals_of_real exp_of_real)
-
-lemma sin_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> sin z \<in> \<real>"
- by (metis Reals_cases Reals_of_real sin_of_real)
-
-lemma cos_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> cos z \<in> \<real>"
- 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 \<Longrightarrow> Re z < pi \<Longrightarrow> Re (sin z) > 0"
+ by (auto simp: Re_sin Im_sin add_pos_pos sin_gt_zero)
+
+lemma Im_sin_nonneg: "Re z = 0 \<Longrightarrow> 0 \<le> Im z \<Longrightarrow> 0 \<le> Im (sin z)"
+ by (simp add: Re_sin Im_sin algebra_simps)
+
+lemma Im_sin_nonneg2: "Re z = pi \<Longrightarrow> Im z \<le> 0 \<Longrightarrow> 0 \<le> 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 \<longleftrightarrow> Re(z) = 0 \<and> (\<exists>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 \<Longrightarrow> exp w = exp z \<Longrightarrow> w = z"
by (auto simp: exp_eq abs_mult)
-lemma exp_integer_2pi:
+lemma exp_integer_2pi:
assumes "n \<in> 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(\<i> * of_real x) \<noteq> 1"
-proof
+proof
assume "exp (\<i> * of_real x) = 1"
then have "exp (\<i> * 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 \<longleftrightarrow> (\<exists>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 \<longleftrightarrow> (\<exists>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 \<longleftrightarrow> (\<exists>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 \<longleftrightarrow> (\<exists>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 \<longleftrightarrow> (\<exists>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 \<longleftrightarrow> (\<exists>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 \<longleftrightarrow> (\<exists>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) \<le> 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) \<le> 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) \<le> 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 - (\<Sum>k\<le>n. z ^ k / (fact k))) \<le> exp\<bar>Re z\<bar> * (norm z) ^ (Suc n) / (fact n)"
proof (rule complex_taylor [of _ n "\<lambda>k. exp" "exp\<bar>Re z\<bar>" 0 z, simplified])
show "convex (closed_segment 0 z)"
@@ -459,11 +490,11 @@
show "z \<in> 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 \<le> u" "u \<le> 1"
- shows cmod_sin_le_exp: "cmod (sin (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>"
+ shows cmod_sin_le_exp: "cmod (sin (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>"
and cmod_cos_le_exp: "cmod (cos (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>"
proof -
have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> 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 - (\<Sum>k\<le>n. complex_of_real (sin_coeff k) * z ^ k))
+
+lemma Taylor_sin:
+ "norm(sin z - (\<Sum>k\<le>n. complex_of_real (sin_coeff k) * z ^ k))
\<le> exp\<bar>Im z\<bar> * (norm z) ^ (Suc n) / (fact n)"
proof -
have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2"
by arith
have *: "cmod (sin z -
(\<Sum>i\<le>n. (-1) ^ (i div 2) * (if even i then sin 0 else cos 0) * z ^ i / (fact i)))
- \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)"
+ \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)"
proof (rule complex_taylor [of "closed_segment 0 z" n "\<lambda>k x. (-1)^(k div 2) * (if even k then sin x else cos x)" "exp\<bar>Im z\<bar>" 0 z,
simplified])
show "convex (closed_segment 0 z)"
@@ -519,7 +550,7 @@
show "z \<in> 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 **: "\<And>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 - (\<Sum>k\<le>n. complex_of_real (cos_coeff k) * z ^ k))
+lemma Taylor_cos:
+ "norm(cos z - (\<Sum>k\<le>n. complex_of_real (cos_coeff k) * z ^ k))
\<le> exp\<bar>Im z\<bar> * (norm z) ^ Suc n / (fact n)"
proof -
have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2"
by arith
have *: "cmod (cos z -
(\<Sum>i\<le>n. (-1) ^ (Suc i div 2) * (if even i then cos 0 else sin 0) * z ^ i / (fact i)))
- \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)"
+ \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)"
proof (rule complex_taylor [of "closed_segment 0 z" n "\<lambda>k x. (-1)^(Suc k div 2) * (if even k then cos x else sin x)" "exp\<bar>Im z\<bar>" 0 z,
simplified])
show "convex (closed_segment 0 z)"
@@ -563,7 +594,7 @@
show "z \<in> 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 **: "\<And>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 \<Rightarrow> 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 \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> 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 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z) Ln"
by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_Ln)
+lemma isCont_Ln' [simp]:
+ "\<lbrakk>isCont f z; Im(f z) = 0 \<Longrightarrow> 0 < Re(f z)\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. Ln (f x)) z"
+ by (blast intro: isCont_o2 [OF _ continuous_at_Ln])
+
lemma continuous_within_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> 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 \<in> \<real> \<Longrightarrow> Re z > 0 \<Longrightarrow> Ln z \<in> \<real>"
+ 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 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z) csqrt"
by (simp add: complex_differentiable_within_csqrt complex_differentiable_imp_continuous_at)
+corollary isCont_csqrt' [simp]:
+ "\<lbrakk>isCont f z; Im(f z) = 0 \<Longrightarrow> 0 < Re(f z)\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. csqrt (f x)) z"
+ by (blast intro: isCont_o2 [OF _ continuous_at_csqrt])
+
lemma continuous_within_csqrt:
"(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> 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 \<Rightarrow> complex" where
+ "Arctan \<equiv> \<lambda>z. (\<i>/2) * Ln((1 - \<i>*z) / (1 + \<i>*z))"
+
+lemma Arctan_0 [simp]: "Arctan 0 = 0"
+ by (simp add: Arctan_def)
+
+lemma Im_complex_div_lemma: "Im((1 - \<i>*z) / (1 + \<i>*z)) = 0 \<longleftrightarrow> Re z = 0"
+ by (auto simp: Im_complex_div_eq_0 algebra_simps)
+
+lemma Re_complex_div_lemma: "0 < Re((1 - \<i>*z) / (1 + \<i>*z)) \<longleftrightarrow> 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 \<noteq> -1"
+ shows [simp]:"tan(Arctan z) = z"
+proof -
+ have "1 + \<i>*z \<noteq> 0"
+ by (metis assms complex_i_mult_minus i_squared minus_unique power2_eq_square power2_minus)
+ moreover
+ have "1 - \<i>*z \<noteq> 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 "\<bar>Re z\<bar> < pi/2"
+ shows "Arctan(tan z) = z"
+proof -
+ have ge_pi2: "\<And>n::int. abs (of_int (2*n + 1) * pi/2) \<ge> pi/2"
+ by (case_tac n rule: int_cases) (auto simp: abs_mult)
+ have "exp (\<i>*z)*exp (\<i>*z) = -1 \<longleftrightarrow> exp (2*\<i>*z) = -1"
+ by (metis distrib_right exp_add mult_2)
+ also have "... \<longleftrightarrow> exp (2*\<i>*z) = exp (\<i>*pi)"
+ using cis_conv_exp cis_pi by auto
+ also have "... \<longleftrightarrow> exp (2*\<i>*z - \<i>*pi) = 1"
+ by (metis (no_types) diff_add_cancel diff_minus_eq_add exp_add exp_minus_inverse mult.commute)
+ also have "... \<longleftrightarrow> Re(\<i>*2*z - \<i>*pi) = 0 \<and> (\<exists>n::int. Im(\<i>*2*z - \<i>*pi) = of_int (2 * n) * pi)"
+ by (simp add: exp_eq_1)
+ also have "... \<longleftrightarrow> Im z = 0 \<and> (\<exists>n::int. 2 * Re z = of_int (2*n + 1) * pi)"
+ by (simp add: algebra_simps)
+ also have "... \<longleftrightarrow> 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 (\<i>*z)*exp (\<i>*z) + 1 \<noteq> 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 \<Longrightarrow> 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 + \<i>*z \<noteq> 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 \<noteq> -\<i>" using assms
+ by auto
+ then have zz: "1 + z * z \<noteq> 0"
+ by (metis abs_one assms i_squared ii.simps less_irrefl minus_unique square_eq_iff)
+ have nz1: "1 - \<i>*z \<noteq> 0"
+ using assms by (force simp add: ii_times_eq_iff)
+ have nz2: "inverse (1 + \<i>*z) \<noteq> 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 - \<i>*z) * inverse (1 + \<i>*z)) \<noteq> 0"
+ using nz1 nz2 by auto
+ have *: "Im ((1 - \<i>*z) / (1 + \<i>*z)) = 0 \<Longrightarrow> 0 < Re ((1 - \<i>*z) / (1 + \<i>*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 \<Longrightarrow> abs(Im z) < 1) \<Longrightarrow> Arctan complex_differentiable at z"
+ using has_field_derivative_Arctan
+ by (auto simp: complex_differentiable_def)
+
+lemma complex_differentiable_within_Arctan:
+ "(Re z = 0 \<Longrightarrow> abs(Im z) < 1) \<Longrightarrow> 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 \<Longrightarrow> abs(Im z) < 1) \<Longrightarrow> continuous (at z) Arctan"
+ by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_Arctan)
+
+lemma continuous_within_Arctan:
+ "(Re z = 0 \<Longrightarrow> abs(Im z) < 1) \<Longrightarrow> continuous (at z within s) Arctan"
+ using continuous_at_Arctan continuous_at_imp_continuous_within by blast
+
+lemma continuous_on_Arctan [continuous_intros]:
+ "(\<And>z. z \<in> s \<Longrightarrow> Re z = 0 \<Longrightarrow> abs \<bar>Im z\<bar> < 1) \<Longrightarrow> continuous_on s Arctan"
+ by (auto simp: continuous_at_imp_continuous_on continuous_within_Arctan)
+
+lemma holomorphic_on_Arctan:
+ "(\<And>z. z \<in> s \<Longrightarrow> Re z = 0 \<Longrightarrow> abs \<bar>Im z\<bar> < 1) \<Longrightarrow> 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(\<i> * of_real y)) = 1"
+ by simp
+
+lemma norm_exp_imaginary: "norm(exp z) = 1 \<Longrightarrow> 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 - \<i>*x) / (1 + \<i>*x) \<noteq> 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 \<in> \<real> \<Longrightarrow> Arctan z \<in> \<real>"
+ by (metis Reals_cases Reals_of_real Arctan_of_real)
+
+declare arctan_one [simp]
+
+lemma arctan_less_pi4_pos: "x < 1 \<Longrightarrow> arctan x < pi/4"
+ by (metis arctan_less_iff arctan_one)
+
+lemma arctan_less_pi4_neg: "-1 < x \<Longrightarrow> -(pi/4) < arctan x"
+ by (metis arctan_less_iff arctan_minus arctan_one)
+
+lemma arctan_less_pi4: "abs x < 1 \<Longrightarrow> abs(arctan x) < pi/4"
+ by (metis abs_less_iff arctan_less_pi4_pos arctan_minus)
+
+lemma arctan_le_pi4: "abs x \<le> 1 \<Longrightarrow> abs(arctan x) \<le> 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 \<or> y = 0")
+ case True then show ?thesis
+ by auto
+next
+ case False
+ then have *: "\<bar>arctan x\<bar> < pi / 2 - \<bar>arctan y\<bar>" 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) \<le> abs x"
+proof -
+ { fix w::complex and z::complex
+ assume *: "w \<in> \<real>" "z \<in> \<real>"
+ have "cmod (Arctan w - Arctan z) \<le> 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) \<le> 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 \<le> x \<Longrightarrow> arctan x \<le> x"
+ by (metis abs_arctan_le abs_of_nonneg zero_le_arctan_iff)
+
+lemma abs_tan_ge: "abs x < pi/2 \<Longrightarrow> abs x \<le> abs(tan x)"
+ by (metis abs_arctan_le abs_less_iff arctan_tan minus_less_iff)
+
+
+subsection{*Inverse Sine*}
+
+definition Arcsin :: "complex \<Rightarrow> complex" where
+ "Arcsin \<equiv> \<lambda>z. -\<i> * Ln(\<i> * z + csqrt(1 - z\<^sup>2))"
+
+lemma Arcsin_body_lemma: "\<i> * z + csqrt(1 - z\<^sup>2) \<noteq> 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 \<Longrightarrow> 0 < Re(\<i> * 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 (\<i> * z + csqrt(1 - z\<^sup>2)))"
+ by (simp add: Arcsin_def)
+
+lemma Im_Arcsin: "Im(Arcsin z) = - ln (cmod (\<i> * z + csqrt (1 - z\<^sup>2)))"
+ by (simp add: Arcsin_def Arcsin_body_lemma)
+
+lemma isCont_Arcsin:
+ assumes "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
+ shows "isCont Arcsin z"
+proof -
+ have rez: "Im (1 - z\<^sup>2) = 0 \<Longrightarrow> 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 \<Longrightarrow> (Im (f z) = 0 \<Longrightarrow> \<bar>Re (f z)\<bar> < 1) \<Longrightarrow> isCont (\<lambda>x. Arcsin (f x)) z"
+ by (blast intro: isCont_o2 [OF _ isCont_Arcsin])
+
+lemma sin_Arcsin [simp]: "sin(Arcsin z) = z"
+proof -
+ have "\<i>*z*2 + csqrt (1 - z\<^sup>2)*2 = 0 \<longleftrightarrow> (\<i>*z)*2 + csqrt (1 - z\<^sup>2)*2 = 0"
+ by (simp add: algebra_simps) --{*Cancelling a factor of 2*}
+ moreover have "... \<longleftrightarrow> (\<i>*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:
+ "\<bar>Re z\<bar> = pi/2 \<Longrightarrow> Im z = 0 \<Longrightarrow>
+ Re ((exp (\<i>*z) + inverse (exp (\<i>*z))) / 2) = 0 \<and> 0 \<le> Im ((exp (\<i>*z) + inverse (exp (\<i>*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 "\<bar>Re z\<bar> < pi / 2"
+ shows "0 < Re ((exp (\<i>*z) + inverse (exp (\<i>*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 "\<bar>Re z\<bar> < pi/2 \<or> (\<bar>Re z\<bar> = pi/2 \<and> Im z = 0)"
+ shows "Arcsin(sin z) = z"
+proof -
+ have "Arcsin(sin z) = - (\<i> * Ln (csqrt (1 - (\<i> * (exp (\<i>*z) - inverse (exp (\<i>*z))))\<^sup>2 / 4) - (inverse (exp (\<i>*z)) - exp (\<i>*z)) / 2))"
+ by (simp add: sin_exp_eq Arcsin_def exp_minus)
+ also have "... = - (\<i> * Ln (csqrt (((exp (\<i>*z) + inverse (exp (\<i>*z)))/2)\<^sup>2) - (inverse (exp (\<i>*z)) - exp (\<i>*z)) / 2))"
+ by (simp add: field_simps power2_eq_square)
+ also have "... = - (\<i> * Ln (((exp (\<i>*z) + inverse (exp (\<i>*z)))/2) - (inverse (exp (\<i>*z)) - exp (\<i>*z)) / 2))"
+ apply (subst csqrt_square)
+ using assms Re_eq_pihalf_lemma Re_less_pihalf_lemma
+ apply auto
+ done
+ also have "... = - (\<i> * Ln (exp (\<i>*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:
+ "\<lbrakk>sin z = w; \<bar>Re z\<bar> < pi/2 \<or> (\<bar>Re z\<bar> = pi/2 \<and> Im z = 0)\<rbrakk> \<Longrightarrow> 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 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
+ shows "(Arcsin has_field_derivative inverse(cos(Arcsin z))) (at z)"
+proof -
+ have "(sin (Arcsin z))\<^sup>2 \<noteq> 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) \<noteq> 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 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arcsin complex_differentiable at z"
+ using complex_differentiable_def has_field_derivative_Arcsin by blast
+
+lemma complex_differentiable_within_Arcsin:
+ "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> 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 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> continuous (at z within s) Arcsin"
+ using continuous_at_imp_continuous_within isCont_Arcsin by blast
+
+lemma continuous_on_Arcsin [continuous_intros]:
+ "(\<And>z. z \<in> s \<Longrightarrow> Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> continuous_on s Arcsin"
+ by (simp add: continuous_at_imp_continuous_on)
+
+lemma holomorphic_on_Arcsin: "(\<And>z. z \<in> s \<Longrightarrow> Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arcsin holomorphic_on s"
+ by (simp add: complex_differentiable_within_Arcsin holomorphic_on_def)
+
+
+subsection{*Inverse Cosine*}
+
+definition Arccos :: "complex \<Rightarrow> complex" where
+ "Arccos \<equiv> \<lambda>z. -\<i> * Ln(z + \<i> * csqrt(1 - z\<^sup>2))"
+
+lemma Arccos_range_lemma: "\<bar>Re z\<bar> < 1 \<Longrightarrow> 0 < Im(z + \<i> * csqrt(1 - z\<^sup>2))"
+ using Arcsin_range_lemma [of "-z"]
+ by simp
+
+lemma Arccos_body_lemma: "z + \<i> * csqrt(1 - z\<^sup>2) \<noteq> 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 + \<i> * csqrt(1 - z\<^sup>2)))"
+ by (simp add: Arccos_def)
+
+lemma Im_Arccos: "Im(Arccos z) = - ln (cmod (z + \<i> * 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 \<Longrightarrow> \<bar>Re z\<bar> < 1)" "Im (z + \<i> * csqrt (1 - z\<^sup>2)) = 0"
+ shows "0 < Re (z + \<i> * 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 \<noteq> 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 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
+ shows "isCont Arccos z"
+proof -
+ have rez: "Im (1 - z\<^sup>2) = 0 \<Longrightarrow> 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 \<Longrightarrow> (Im (f z) = 0 \<Longrightarrow> \<bar>Re (f z)\<bar> < 1) \<Longrightarrow> isCont (\<lambda>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 + \<i> * (2 * csqrt (1 - z\<^sup>2)) = 0 \<longleftrightarrow> z*2 + \<i> * csqrt (1 - z\<^sup>2)*2 = 0"
+ by (simp add: algebra_simps) --{*Cancelling a factor of 2*}
+ moreover have "... \<longleftrightarrow> z + \<i> * 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 \<or>
+ Re z = 0 & 0 \<le> Im z \<or>
+ Re z = pi & Im z \<le> 0"
+ shows "Arccos(cos z) = z"
+proof -
+ have *: "((\<i> - (Exp (\<i> * z))\<^sup>2 * \<i>) / (2 * Exp (\<i> * z))) = sin z"
+ by (simp add: sin_exp_eq exp_minus field_simps power2_eq_square)
+ have "1 - (exp (\<i> * z) + inverse (exp (\<i> * z)))\<^sup>2 / 4 = ((\<i> - (Exp (\<i> * z))\<^sup>2 * \<i>) / (2 * Exp (\<i> * z)))\<^sup>2"
+ by (simp add: field_simps power2_eq_square)
+ then have "Arccos(cos z) = - (\<i> * Ln ((exp (\<i> * z) + inverse (exp (\<i> * z))) / 2 +
+ \<i> * csqrt (((\<i> - (Exp (\<i> * z))\<^sup>2 * \<i>) / (2 * Exp (\<i> * z)))\<^sup>2)))"
+ by (simp add: cos_exp_eq Arccos_def exp_minus)
+ also have "... = - (\<i> * Ln ((exp (\<i> * z) + inverse (exp (\<i> * z))) / 2 +
+ \<i> * ((\<i> - (Exp (\<i> * z))\<^sup>2 * \<i>) / (2 * Exp (\<i> * 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 "... = - (\<i> * Ln (exp (\<i>*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:
+ "\<lbrakk>cos z = w;
+ 0 < Re z \<and> Re z < pi \<or>
+ Re z = 0 \<and> 0 \<le> Im z \<or>
+ Re z = pi \<and> Im z \<le> 0\<rbrakk> \<Longrightarrow> 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 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
+ shows "(Arccos has_field_derivative - inverse(sin(Arccos z))) (at z)"
+proof -
+ have "(cos (Arccos z))\<^sup>2 \<noteq> 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) \<noteq> 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 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arccos complex_differentiable at z"
+ using complex_differentiable_def has_field_derivative_Arccos by blast
+
+lemma complex_differentiable_within_Arccos:
+ "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> 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 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> continuous (at z within s) Arccos"
+ using continuous_at_imp_continuous_within isCont_Arccos by blast
+
+lemma continuous_on_Arccos [continuous_intros]:
+ "(\<And>z. z \<in> s \<Longrightarrow> Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> continuous_on s Arccos"
+ by (simp add: continuous_at_imp_continuous_on)
+
+lemma holomorphic_on_Arccos: "(\<And>z. z \<in> s \<Longrightarrow> Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> 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: "\<bar>Re z\<bar> < 1 \<Longrightarrow> abs(Re(Arcsin z)) < pi/2"
+ unfolding Re_Arcsin
+ by (blast intro: Re_Ln_pos_lt_imp Arcsin_range_lemma)
+
+lemma Arccos_bounds: "\<bar>Re z\<bar> < 1 \<Longrightarrow> 0 < Re(Arccos z) \<and> 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) \<and> Re(Arccos z) \<le> 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)) \<le> 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) \<le> 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)) \<le> 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 \<noteq> 1" shows "cos(Arcsin z) \<noteq> 0"
+proof -
+ have eq: "(\<i> * z * (csqrt (1 - z\<^sup>2)))\<^sup>2 = z\<^sup>2 * (z\<^sup>2 - 1)"
+ by (simp add: power_mult_distrib algebra_simps)
+ have "\<i> * z * (csqrt (1 - z\<^sup>2)) \<noteq> z\<^sup>2 - 1"
+ proof
+ assume "\<i> * z * (csqrt (1 - z\<^sup>2)) = z\<^sup>2 - 1"
+ then have "(\<i> * 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 + \<i> * z * (csqrt (1 - z * z)) \<noteq> z\<^sup>2"
+ by (metis add_minus_cancel power2_eq_square uminus_add_conv_diff)
+ then have "2*(1 + \<i> * z * (csqrt (1 - z * z))) \<noteq> 2*z\<^sup>2" (*FIXME cancel_numeral_factor*)
+ by (metis mult_cancel_left zero_neq_numeral)
+ then have "(\<i> * z + csqrt (1 - z\<^sup>2))\<^sup>2 \<noteq> -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 \<noteq> 1" shows "sin(Arccos z) \<noteq> 0"
+proof -
+ have eq: "(\<i> * z * (csqrt (1 - z\<^sup>2)))\<^sup>2 = -(z\<^sup>2) * (1 - z\<^sup>2)"
+ by (simp add: power_mult_distrib algebra_simps)
+ have "\<i> * z * (csqrt (1 - z\<^sup>2)) \<noteq> 1 - z\<^sup>2"
+ proof
+ assume "\<i> * z * (csqrt (1 - z\<^sup>2)) = 1 - z\<^sup>2"
+ then have "(\<i> * 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 + \<i> * z * (csqrt (1 - z\<^sup>2)) \<noteq> 1"
+ by (simp add: algebra_simps)
+ then have "2*(z\<^sup>2 + \<i> * z * (csqrt (1 - z\<^sup>2))) \<noteq> 2*1"
+ by (metis mult_cancel_left2 zero_neq_numeral) (*FIXME cancel_numeral_factor*)
+ then have "(z + \<i> * csqrt (1 - z\<^sup>2))\<^sup>2 \<noteq> 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) \<or> cos(Re z) = 0 \<and> Im z * sin(Re z) \<le> 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) \<or> sin(Re z) = 0 \<and> 0 \<le> 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 \<le> Im z) \<Longrightarrow> 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 \<le> Im z) \<Longrightarrow> 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 \<le> Im z \<Longrightarrow> 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 \<le> Im z \<Longrightarrow> 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 \<le> 1"
+ shows "Im (Arcsin (of_real x)) = 0"
+proof -
+ have "csqrt (1 - (of_real x)\<^sup>2) = (if x^2 \<le> 1 then sqrt (1 - x^2) else \<i> * sqrt (x^2 - 1))"
+ by (simp add: of_real_sqrt del: csqrt_of_real_nonneg)
+ then have "cmod (\<i> * 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 (\<i> * 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 \<in> \<real> \<Longrightarrow> \<bar>Re z\<bar> \<le> 1 \<Longrightarrow> Arcsin z \<in> \<real>"
+ by (metis Im_Arcsin_of_real Re_complex_of_real Reals_cases complex_is_Real_iff)
+
+lemma arcsin_eq_Re_Arcsin:
+ assumes "abs x \<le> 1"
+ shows "arcsin x = Re (Arcsin (of_real x))"
+unfolding arcsin_def
+proof (rule the_equality, safe)
+ show "- (pi / 2) \<le> 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)) \<le> 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) \<le> x'" "x' \<le> 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 \<le> 1 \<Longrightarrow> 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 \<le> 1"
+ shows "Im (Arccos (of_real x)) = 0"
+proof -
+ have "csqrt (1 - (of_real x)\<^sup>2) = (if x^2 \<le> 1 then sqrt (1 - x^2) else \<i> * sqrt (x^2 - 1))"
+ by (simp add: of_real_sqrt del: csqrt_of_real_nonneg)
+ then have "cmod (of_real x + \<i> * 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 + \<i> * 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 \<in> \<real> \<Longrightarrow> \<bar>Re z\<bar> \<le> 1 \<Longrightarrow> Arccos z \<in> \<real>"
+ by (metis Im_Arccos_of_real Re_complex_of_real Reals_cases complex_is_Real_iff)
+
+lemma arccos_eq_Re_Arccos:
+ assumes "abs x \<le> 1"
+ shows "arccos x = Re (Arccos (of_real x))"
+unfolding arccos_def
+proof (rule the_equality, safe)
+ show "0 \<le> 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)) \<le> 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 \<le> x'" "x' \<le> 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 \<le> 1 \<Longrightarrow> 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
--- 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 \<Longrightarrow> setprod (inverse \<circ> f) A = (inverse (setprod f A) :: 'a:: field_inverse_zero)"
+ "finite A \<Longrightarrow> setprod (inverse \<circ> f) A = (inverse (setprod f A) :: 'a:: field)"
apply (erule finite_induct)
apply (simp)
apply simp
--- 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 \<longleftrightarrow> 0 \<le> a \<and> x \<bullet> x = a\<^sup>2"
by (auto simp add: norm_eq_sqrt_inner)
-lemma real_abs_le_square_iff: "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> (x::real)\<^sup>2 \<le> y\<^sup>2"
-proof
- assume "\<bar>x\<bar> \<le> \<bar>y\<bar>"
- then have "\<bar>x\<bar>\<^sup>2 \<le> \<bar>y\<bar>\<^sup>2" by (rule power_mono, simp)
- then show "x\<^sup>2 \<le> y\<^sup>2" by simp
-next
- assume "x\<^sup>2 \<le> y\<^sup>2"
- then have "sqrt (x\<^sup>2) \<le> sqrt (y\<^sup>2)" by (rule real_sqrt_le_mono)
- then show "\<bar>x\<bar> \<le> \<bar>y\<bar>" by simp
-qed
-
lemma norm_le_square: "norm x \<le> a \<longleftrightarrow> 0 \<le> a \<and> x \<bullet> x \<le> 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 \<ge> a \<longleftrightarrow> a \<le> 0 \<or> x \<bullet> x \<ge> 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
--- 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 "(\<Sum>i\<le>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 "(\<Sum>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 "(\<Sum>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 "(\<Sum>i<n. x^i) = (if x = 1 then of_nat n else (1 - x^n) / (1 - x))"
by (induct n) (auto simp: algebra_simps divide_simps)
--- a/src/HOL/NSA/HDeriv.thy Wed Apr 01 22:40:07 2015 +0200
+++ b/src/HOL/NSA/HDeriv.thy Wed Apr 01 22:40:41 2015 +0200
@@ -366,7 +366,7 @@
done
ultimately have "(inverse (star_of x + h) - inverse (star_of x)) / h \<approx>
- (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
--- 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]:
"\<And>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]:
"\<And>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:
- "\<And>r n. r \<noteq> (0::'a::field_inverse_zero star)
+ "\<And>r n. r \<noteq> (0::'a::field star)
\<Longrightarrow> inverse (r pow n) = (inverse r) pow n"
by transfer (rule power_inverse)
--- 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:
- "\<And>a::'a::{real_normed_div_algebra, division_ring_inverse_zero} star.
+ "\<And>a::'a::{real_normed_div_algebra, division_ring} star.
hnorm (inverse a) = inverse (hnorm a)"
by transfer (rule norm_inverse)
lemma hnorm_divide:
- "\<And>a b::'a::{real_normed_field, field_inverse_zero} star.
+ "\<And>a b::'a::{real_normed_field, field} star.
hnorm (a / b) = hnorm a / hnorm b"
by transfer (rule norm_divide)
--- 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 *}
--- 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:
--- 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"
--- 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 \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
unfolding not_le [symmetric] by (simp add: sum_power2_le_zero_iff)
+lemma abs_le_square_iff:
+ "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> x\<^sup>2 \<le> y\<^sup>2"
+proof
+ assume "\<bar>x\<bar> \<le> \<bar>y\<bar>"
+ then have "\<bar>x\<bar>\<^sup>2 \<le> \<bar>y\<bar>\<^sup>2" by (rule power_mono, simp)
+ then show "x\<^sup>2 \<le> y\<^sup>2" by simp
+next
+ assume "x\<^sup>2 \<le> y\<^sup>2"
+ then show "\<bar>x\<bar> \<le> \<bar>y\<bar>"
+ by (auto intro!: power2_le_imp_le [OF _ abs_ge_zero])
+qed
+
+lemma abs_square_le_1:"x\<^sup>2 \<le> 1 \<longleftrightarrow> abs(x) \<le> 1"
+ using abs_le_square_iff [of x 1]
+ by simp
+
+lemma abs_square_eq_1: "x\<^sup>2 = 1 \<longleftrightarrow> abs(x) = 1"
+ by (auto simp add: abs_if power2_eq_1_iff)
+
+lemma abs_square_less_1: "x\<^sup>2 < 1 \<longleftrightarrow> 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)
--- 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 \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>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 \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>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 (\<lambda>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
--- 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 \<Rightarrow> 'a::{banach, real_normed_field, field_inverse_zero, second_countable_topology}"
+ fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, field, second_countable_topology}"
shows "(c \<noteq> 0 \<Longrightarrow> interval_lebesgue_integrable M a b f) \<Longrightarrow>
interval_lebesgue_integrable M a b (\<lambda>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 \<Rightarrow> 'a::{banach, real_normed_field, field_inverse_zero, second_countable_topology}"
+ fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, field, second_countable_topology}"
shows "interval_lebesgue_integral M a b (\<lambda>x. f x / c) =
interval_lebesgue_integral M a b f / c"
by (simp add: interval_lebesgue_integral_def)
--- 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 "\<lambda>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 \<noteq> 0 \<Longrightarrow> set_integrable M A f"
shows "set_integrable M A (\<lambda>t. f t / a)"
proof -
--- 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))"
--- 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
--- 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 @@
"\<not> positive x \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> 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 \<in> Rats \<Longrightarrow> inverse a \<in> 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 "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a / b \<in> Rats"
apply (auto simp add: Rats_def)
apply (rule range_eqI)
--- 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 "\<lambda>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
--- 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 \<in> Reals \<Longrightarrow> inverse a \<in> 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 \<in> \<real> \<longleftrightarrow> x \<in> \<real>"
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 "\<lbrakk>a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> a / b \<in> 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)
--- 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 @@
"\<bar>x - a\<bar> < r \<longleftrightarrow> a - r < x \<and> x < a + r"
by (auto simp add: diff_less_eq ac_simps abs_less_iff)
+lemma abs_diff_le_iff:
+ "\<bar>x - a\<bar> \<le> r \<longleftrightarrow> a - r \<le> x \<and> x \<le> 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
--- 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 =
--- 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)))
--- 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 =
--- 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 \<in> \<real> \<Longrightarrow> exp z \<in> \<real>"
+ by (metis Reals_cases Reals_of_real exp_of_real)
+
lemma exp_not_eq_zero [simp]: "exp x \<noteq> 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 \<in> \<real> \<Longrightarrow> sin z \<in> \<real>"
+ 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 \<in> \<real> \<Longrightarrow> cos z \<in> \<real>"
+ 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 \<Rightarrow> 'a::{real_normed_field,banach}"
where "tan = (\<lambda>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 \<in> \<real> \<Longrightarrow> tan z \<in> \<real>"
+ 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 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> 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 \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> (arcsin x = arcsin y \<longleftrightarrow> x = y)"
+ by (metis abs_le_interval_iff arcsin)
+
+lemma cos_arcsin_nonzero: "-1 < x \<Longrightarrow> x < 1 \<Longrightarrow> cos(arcsin x) \<noteq> 0"
+ using arcsin_lt_bounded cos_gt_zero_pi by force
+
lemma arccos:
"\<lbrakk>-1 \<le> y; y \<le> 1\<rbrakk>
\<Longrightarrow> 0 \<le> arccos y & arccos y \<le> pi & cos(arccos y) = y"
@@ -4012,8 +4052,7 @@
by (blast dest: arccos)
lemma arccos_lt_bounded:
- "\<lbrakk>-1 < y; y < 1\<rbrakk>
- \<Longrightarrow> 0 < arccos y & arccos y < pi"
+ "\<lbrakk>-1 < y; y < 1\<rbrakk> \<Longrightarrow> 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 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> 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 \<Longrightarrow> x < 1 \<Longrightarrow> ~(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) \<noteq> 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 \<noteq> 0 \<Longrightarrow> 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="\<lambda>x. - pi/2 < x \<and> x < pi/2" and P="\<lambda>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="\<lambda>x. - pi/2 < x \<and> x < pi/2" and P="\<lambda>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: "\<bar>y\<bar> \<le> 1 \<Longrightarrow> cos (arccos y) = y"
+ by (simp add: abs_le_iff)
+
+lemma sin_arccos_abs: "\<bar>y\<bar> \<le> 1 \<Longrightarrow> sin (arccos y) = sqrt (1 - y\<^sup>2)"
+ by (simp add: sin_arccos abs_le_iff)
+
lemma sin_mono_less_eq: "\<lbrakk>-(pi/2) \<le> x; x \<le> pi/2; -(pi/2) \<le> y; y \<le> pi/2\<rbrakk>
\<Longrightarrow> (sin(x) < sin(y) \<longleftrightarrow> x < y)"
by (metis not_less_iff_gr_or_eq sin_monotone_2pi)
@@ -4301,12 +4355,12 @@
\<Longrightarrow> (sin(x) \<le> sin(y) \<longleftrightarrow> x \<le> y)"
by (meson leD le_less_linear sin_monotone_2pi sin_monotone_2pi_le)
-lemma sin_inj_pi: "-(pi/2) \<le> x ==> x \<le> pi/2 ==>
- -(pi/2) \<le> y ==> y \<le> pi/2 ==> sin(x) = sin(y) \<Longrightarrow> x = y"
+lemma sin_inj_pi:
+ "\<lbrakk>-(pi/2) \<le> x; x \<le> pi/2;-(pi/2) \<le> y; y \<le> pi/2; sin(x) = sin(y)\<rbrakk> \<Longrightarrow> x = y"
by (metis arcsin_sin)
-lemma cos_mono_lt_eq: "0 \<le> x ==> x \<le> pi ==> 0 \<le> y ==> y \<le> pi
- \<Longrightarrow> (cos(x) < cos(y) \<longleftrightarrow> y < x)"
+lemma cos_mono_less_eq:
+ "0 \<le> x ==> x \<le> pi ==> 0 \<le> y ==> y \<le> pi \<Longrightarrow> (cos(x) < cos(y) \<longleftrightarrow> y < x)"
by (meson cos_monotone_0_pi cos_monotone_0_pi_le leD le_less_linear)
lemma cos_mono_le_eq: "0 \<le> x ==> x \<le> pi ==> 0 \<le> y ==> y \<le> pi
@@ -4388,6 +4442,40 @@
done
qed
+lemma arcsin_less_mono: "abs x \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> arcsin x < arcsin y \<longleftrightarrow> 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 \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> arcsin x \<le> arcsin y \<longleftrightarrow> x \<le> y"
+ using arcsin_less_mono not_le by blast
+
+lemma arcsin_less_arcsin: "-1 \<le> x \<Longrightarrow> x < y \<Longrightarrow> y \<le> 1 \<Longrightarrow> arcsin x < arcsin y"
+ using arcsin_less_mono by auto
+
+lemma arcsin_le_arcsin: "-1 \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> arcsin x \<le> arcsin y"
+ using arcsin_le_mono by auto
+
+lemma arccos_less_mono: "abs x \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> (arccos x < arccos y \<longleftrightarrow> 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 \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> arccos x \<le> arccos y \<longleftrightarrow> y \<le> x"
+ using arccos_less_mono [of y x]
+ by (simp add: not_le [symmetric])
+
+lemma arccos_less_arccos: "-1 \<le> x \<Longrightarrow> x < y \<Longrightarrow> y \<le> 1 \<Longrightarrow> arccos y < arccos x"
+ using arccos_less_mono by auto
+
+lemma arccos_le_arccos: "-1 \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> arccos y \<le> arccos x"
+ using arccos_le_mono by auto
+
+lemma arccos_eq_iff: "abs x \<le> 1 & abs y \<le> 1 \<Longrightarrow> (arccos x = arccos y \<longleftrightarrow> 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 \<and> arctan x < pi / 4 \<and> 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 "\<bar>x\<bar> < 1"
- shows "x\<^sup>2 < 1"
-proof -
- have "\<bar>x\<^sup>2\<bar> < 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 "\<bar> x \<bar> < 1"
shows "DERIV (\<lambda> x'. \<Sum> k. (-1)^k * (1 / real (k*2+1) * x' ^ (k*2+1))) x :> (\<Sum> k. (-1)^k * x^(k*2))"
@@ -4549,7 +4628,7 @@
{
fix x :: real
assume "\<bar>x\<bar> < 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 (\<lambda> 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 (\<lambda> n. (- 1) ^ n * x^(2*n))" unfolding power_mult .
@@ -4657,7 +4736,7 @@
hence "\<bar>x\<bar> < r" by auto
hence "\<bar>x\<bar> < 1" using `r < 1` by auto
have "\<bar> - (x\<^sup>2) \<bar> < 1"
- using less_one_imp_sqr_less_one[OF `\<bar>x\<bar> < 1`] by auto
+ using abs_square_less_1 `\<bar>x\<bar> < 1` by auto
hence "(\<lambda> 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: "\<bar>y\<bar> \<le> 1 \<Longrightarrow> cos (arccos y) = y"
- by (simp add: abs_le_iff)
-
-lemma sin_arccos_abs: "\<bar>y\<bar> \<le> 1 \<Longrightarrow> 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]
--- /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 \<le> a" "a \<le> b" "b \<le> 4" "sin(a/6) \<le> 1/2" "1/2 \<le> sin(b/6)"
+ shows "a \<le> pi \<and> pi \<le> b"
+proof -
+ have *: "\<And>x::real. 0 < x & x < 7/5 \<Longrightarrow> 0 < sin x"
+ using pi_ge_two
+ by (auto intro: sin_gt_zero)
+ have ab: "(b \<le> pi * 3 \<Longrightarrow> pi \<le> b)" "(a \<le> pi * 3 \<Longrightarrow> a \<le> 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) \<le> 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
--- 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 *}
--- 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 \<noteq> 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 \<le> y ==> z + x \<le> z + y" by (rule real_add_left_mono)
--- 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"