Rationalisation of complex transcendentals, esp the Arg function

Some lemmas on complex numbers and coprimality

--HG--
extra : rebase_source : 37434802fd420fdcbc9750dcf9b734797e86eb61

Facts about complex n-th roots

new material about connectedness, etc.

Further new material. The simprule status of some exp and ln identities was reverted.

Fixed LaTeX issue

New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series

Removed [simp] status for Complex_eq. Also tidied some proofs

Renamed ii to imaginary_unit in order to free up ii as a variable name. Also replaced some legacy def commands

Many new theorems, and more tidying

suitable logical type class for abs, sgn

--HG--
extra : rebase_source : 27e95dd7f038f114d0cad11ec69599a166229041

setprod -> prod

setsum -> sum

misc tuning and modernization;

Lots of new material for multivariate analysis

eliminated old 'def';
tuned comments;

New results about paths, segments, etc. The notion of simply_connected.

An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!

fix code generation for uniformity: uniformity is a non-computable pure data.

add uniform spaces

more symbols;

more symbols;

prefer symbols for "abs";

New complex analysis material

isabelle update_cartouches -c -t;

Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.

Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.

Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.

Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer

Rounding function, uniform limits, cotangent, binomial identities

new lemmas about vector_derivative, complex numbers, paths, etc.

eliminated \<Colon>;

isabelle update_cartouches;

uniform _ div _ as infix syntax for ring division

--HG--
extra : rebase_source : c4a1892078772c7ce9af33ad66e2abfefe7adea9

separate class for division operator, with particular syntax added in more specific classes

Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.

given up separate type classes demanding `inverse 0 = 0`

New material and binomial fix

new HOL Light material about exp, sin, cos

Lots of new material on complex-valued functions. Modified simplification of (x/n)^k

sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex

The function frac. Various lemmas about limits, series, the exp function, etc.

import general theorems from AFP/Markov_Models

modernized header uniformly as section;

turn even into an abbreviation

prefer generic elimination rules for even/odd over specialized unfold rules for nat

codatatypes are not datatypes

reduced name variants for assoc and commute on plus and mult

add more derivative and continuity rules for complex-values functions

avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.

--HG--
extra : rebase_source : 899541490c73fe6897445f97dc2a5a3c929cf153

made divide_pos_pos a simp rule

revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules

removing simprule status for divide_minus_left and divide_minus_right

merged DERIV_intros, has_derivative_intros into derivative_intros

moved generic theorems from Complex_Analysis_Basic; fixed some theorem names

add complex_of_real coercion

a few new lemmas and generalisations of old ones

Some rationalisation of basic lemmas

replaced smt-based proof with metis proof that requires no external tool

More complex-related lemmas

eliminiated neg_numeral in favour of - (numeral _)

more simplification rules on unary and binary minus

--HG--
extra : rebase_source : 7c88c9f33c4be8eae76f508a1a73ba79c8b769b1

tuned proofs -- clarified flow of facts wrt. calculation;

standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;

remove unnecessary assumption from real_normed_vector

--HG--
extra : rebase_source : 4a68de89541842f1b91794ddd73c625b6a822085

Renamed {left,right}_distrib to distrib_{right,left}.

merged fork with new numeral representation (see NEWS)

move lemmas about complex number 'i' to Complex.thy and Library/Inner_Product.thy

remove unnecessary intermediate lemmas

prove existence, uniqueness, and other properties of complex arg function

tuned

remove obsolete intermediate lemma complex_inverse_complex_split

tuned

add some new lemmas about cis and rcis;
simplify some proofs;

Complex.thy: move theorems into appropriate subsections

remove redundant lemma complex_of_real_minus_one

--HG--
extra : transplant_source : %93%21%A4%91%08%9C%3B%F6h%13%0A%84%F3%2B%ACGz%2B%3AU

simplify proof of lemma DeMoivre, removing unnecessary intermediate lemma

removed unused lemma sin_cos_squared_add2_mult

remove redundant lemmas i_mult_eq and i_mult_eq2 in favor of i_squared

remove some unnecessary simp rules from simpset

remove redundant lemma real_sum_squared_expand in favor of power2_sum

remove redundant lemma LIMSEQ_Complex in favor of tendsto_Complex

tuned indentation

tuned comments

replace lemma expi_imaginary with reoriented lemma cis_conv_exp

remove redundant lemmas expi_add and expi_zero

move sin_coeff and cos_coeff lemmas to Transcendental.thy; simplify some proofs

define complex exponential 'expi' as abbreviation for 'exp'

remove more bounded_linear locale interpretations (cf. f0de18b62d63)

lemma bounded_linear_intro

standard theorem naming scheme: complex_eqI, complex_eq_iff

tuned headers;

diff_minus subsumes diff_def

dropped superfluous [code del]s

add lemma tendsto_Complex

avoid using real-specific versions of generic lemmas

use new classes (linordered_)field_inverse_zero

class division_ring_inverse_zero

replace 'topo' with 'open'; add extra type constraint for 'open'

more [code del] declarations

replace class open with class topo

introduce class topological_space as a superclass of metric_space

definition of dist for complex

farewell to class recpower

power operation defined generic

interpretation/interpret: prefixes are mandatory by default;

declare power_Suc [simp]; remove redundant type-specific versions of power_Suc

Replaced group_ and ring_simps by algebra_simps;
removed compare_rls - use algebra_simps now

Ported HOL and HOL-Library to new locales.

made repository layout more coherent with logical distribution structure; stripped some $Id$s

--HG--
rename : src/HOL/Library/Code_Message.thy => src/HOL/Code_Message.thy
rename : src/HOL/Complex/Complex.thy => src/HOL/Complex.thy
rename : src/HOL/Complex/Complex_Main.thy => src/HOL/Complex_Main.thy
rename : src/HOL/Real/ContNotDenum.thy => src/HOL/ContNotDenum.thy
rename : src/HOL/Hyperreal/Deriv.thy => src/HOL/Deriv.thy
rename : src/HOL/Hyperreal/Fact.thy => src/HOL/Fact.thy
rename : src/HOL/Hyperreal/FrechetDeriv.thy => src/HOL/FrechetDeriv.thy
rename : src/HOL/Library/GCD.thy => src/HOL/GCD.thy
rename : src/HOL/Hyperreal/Integration.thy => src/HOL/Integration.thy
rename : src/HOL/Real/Float.thy => src/HOL/Library/Float.thy
rename : src/HOL/Hyperreal/Lim.thy => src/HOL/Lim.thy
rename : src/HOL/Hyperreal/Ln.thy => src/HOL/Ln.thy
rename : src/HOL/Hyperreal/Log.thy => src/HOL/Log.thy
rename : src/HOL/Real/Lubs.thy => src/HOL/Lubs.thy
rename : src/HOL/Hyperreal/MacLaurin.thy => src/HOL/MacLaurin.thy
rename : src/HOL/Hyperreal/NthRoot.thy => src/HOL/NthRoot.thy
rename : src/HOL/Library/Order_Relation.thy => src/HOL/Order_Relation.thy
rename : src/HOL/Real/PReal.thy => src/HOL/PReal.thy
rename : src/HOL/Library/Parity.thy => src/HOL/Parity.thy
rename : src/HOL/Real/RComplete.thy => src/HOL/RComplete.thy
rename : src/HOL/Real/Rational.thy => src/HOL/Rational.thy
rename : src/HOL/Real/Real.thy => src/HOL/Real.thy
rename : src/HOL/Real/RealDef.thy => src/HOL/RealDef.thy
rename : src/HOL/Real/RealPow.thy => src/HOL/RealPow.thy
rename : src/HOL/Hyperreal/Series.thy => src/HOL/Series.thy
rename : src/HOL/Hyperreal/Taylor.thy => src/HOL/Taylor.thy
rename : src/HOL/arith_data.ML => src/HOL/Tools/arith_data.ML
rename : src/HOL/Real/float_arith.ML => src/HOL/Tools/float_arith.ML
rename : src/HOL/Real/float_syntax.ML => src/HOL/Tools/float_syntax.ML
rename : src/HOL/hologic.ML => src/HOL/Tools/hologic.ML
rename : src/HOL/int_arith1.ML => src/HOL/Tools/int_arith.ML
rename : src/HOL/int_factor_simprocs.ML => src/HOL/Tools/int_factor_simprocs.ML
rename : src/HOL/nat_simprocs.ML => src/HOL/Tools/nat_simprocs.ML
rename : src/HOL/Real/rat_arith.ML => src/HOL/Tools/rat_arith.ML
rename : src/HOL/Real/real_arith.ML => src/HOL/Tools/real_arith.ML
rename : src/HOL/simpdata.ML => src/HOL/Tools/simpdata.ML
rename : src/HOL/Hyperreal/Transcendental.thy => src/HOL/Transcendental.thy
rename : src/HOL/Library/RType.thy => src/HOL/Typerep.thy
rename : src/HOL/Library/Univ_Poly.thy => src/HOL/Univ_Poly.thy
rename : src/HOL/Complex/ex/Arithmetic_Series_Complex.thy => src/HOL/ex/Arithmetic_Series_Complex.thy
rename : src/HOL/Complex/ex/BigO_Complex.thy => src/HOL/ex/BigO_Complex.thy
rename : src/HOL/Complex/ex/HarmonicSeries.thy => src/HOL/ex/HarmonicSeries.thy
rename : src/HOL/Complex/ex/MIR.thy => src/HOL/ex/MIR.thy
rename : src/HOL/Complex/ex/ReflectedFerrack.thy => src/HOL/ex/ReflectedFerrack.thy
rename : src/HOL/Complex/ex/Sqrt.thy => src/HOL/ex/Sqrt.thy
rename : src/HOL/Complex/ex/Sqrt_Script.thy => src/HOL/ex/Sqrt_Script.thy
rename : src/HOL/Complex/ex/linrtac.ML => src/HOL/ex/linrtac.ML
rename : src/HOL/Complex/ex/mirtac.ML => src/HOL/ex/mirtac.ML
rename : src/Pure/Tools/quickcheck.ML => src/Tools/quickcheck.ML
rename : src/Pure/Tools/value.ML => src/Tools/value.ML