Removed multiplicativity assumption from normalization_semidom

Rearrangement of material in Complex_Analysis_Basics, which contained much that had nothing to do with complex analysis.

generalized

dedicated fact collections for algebraic simplification rules potentially splitting goals

--HG--
extra : rebase_source : ebbd8d0c13409f8fb536c42910e904c24e43dbe6

official fact collection sign_simps

removed unused fact collections

backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is

--HG--
extra : rebase_source : 7ac166208fa2a49e90c60865e74188d18da004a9

tuned

--HG--
extra : rebase_source : 994f20cd611bcdd96775107d47e69a12c13a553c

more document structure

--HG--
extra : rebase_source : 25bedddd8d62a1123f6c95436ff194025ef344cb

tuned

--HG--
extra : rebase_source : ebf4a99af3d387cb1075e3093d8c3b3acea006cc

common type class for distributive division

tuned proofs

isabelle update -u path_cartouches;

isabelle update -u control_cartouches;

grouped material on numeral division

automatic classical rule to derive a dvd b from b mod a = 0

consider dvdE for automated classical proving

type class linordered_nonzero_semiring has new axiom to guarantee characteristic 0

Some lemmas on complex numbers and coprimality

--HG--
extra : rebase_source : 37434802fd420fdcbc9750dcf9b734797e86eb61

isabelle update_cartouches -c -t;

tuned

dedicated definition for coprimality

--HG--
extra : rebase_source : 891168c98ce62efae6b7e72c7d3365fea12b33ae

rule out pathologic instances

--HG--
extra : rebase_source : b04515f7600d4314068b2fe100baa5b177111e0c

more fundamental definition of div and mod on int

--HG--
extra : rebase_source : 95b72d036b88e199c61235ea5833a905f5632800

generalized simproc

--HG--
extra : rebase_source : 1a484c6a7a8374a73f471204dea8be4ee982845f

elementary definition of division on natural numbers

--HG--
extra : rebase_source : 23767fa1baf28db39b18de60e52d4d7f852e48dd

tuned structure

--HG--
extra : rebase_source : ad5aac8dba5969d5cd3c3923df071b0e5dad9747

new material about connectedness, etc.

more lemmas

--HG--
extra : rebase_source : e39561a47214aaf67eea524bde7eb12dcffc8801

slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization

--HG--
extra : rebase_source : 0d5af77e2a7d66625c22923a19c456b1ca17652e

more facts on sgn, abs

--HG--
extra : rebase_source : a98552b24ddce791c14679ddb3d0f5a27e23b00a

more fine-grained type class hierarchy for div and mod

--HG--
extra : rebase_source : fffbeef99e834ca17596f478178e94bed8a014bc

restructured matter on polynomials and normalized fractions

--HG--
extra : rebase_source : 71508900ff150d54097ae5c4c2da7176f09cb625

suitable logical type class for abs, sgn

--HG--
extra : rebase_source : 27e95dd7f038f114d0cad11ec69599a166229041

more standardized theorem names for facts involving the div and mod identity

more standardized names

added lemma

separate type class for arbitrary quotient and remainder partitions

--HG--
extra : rebase_source : c803a2a721f660672d64831c56088100891baa86

syntactic type class for operation mod named after mod;
simplified assumptions of type class semiring_div

--HG--
extra : rebase_source : 3714be7474835787b2a513b731c9864d1ac9d2c4

more lemmas

--HG--
extra : rebase_source : 3446eb0648af16d2212d2a3e40591332dd90c26c

more generic algebraic lemmas

--HG--
extra : rebase_source : afd1b38644ce9418dc6eeaf977c35a8502e396b5

more symbols;

misc tuning and modernization;

sharing simp rules between ordered monoids and rings

More lemmas on Gcd/Lcm

misc tuning and modernization;

eliminated old 'def';
tuned comments;

Contractible sets. Also removal of obsolete theorems and refactoring

more theorems on orderings

--HG--
extra : rebase_source : 4e5a14cb68359f057eb65c380c103e23971ad09c

tuned bootstrap order to provide type classes in a more sensible order

--HG--
extra : rebase_source : b4008b5f377525bc1866d515a16702fbb0b463c9

more canonical names

generalize more theorems to support enat and ennreal

--HG--
extra : rebase_source : 11176604a37483aa41462153f0aa289df506590d

moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add

--HG--
extra : rebase_source : 8674c79985a670cee921b8193965bb0767549a5c

Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.

--HG--
extra : rebase_source : 54bd3e5fcde04ef38241be91231c48d078b850f2

more theorems

--HG--
extra : rebase_source : de1d0718cda85a6dd4693328efc096fe8f9dfb2e

cleansed junk-producing interpretations for gcd/lcm on nat altogether

generalized some lemmas;
moved some lemmas in more appropriate places;
deleted potentially dangerous simp rule

prefer symbols for "abs";

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.

slight cleanup of lemmas

--HG--
extra : rebase_source : 17dbf1b3c59a40c2a2ac93ab58d3e6371773af6c

isabelle update_cartouches;

tuned facts

avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead

moved normalization and unit_factor into Main HOL corpus

Useful lemmas. The theorem concerning swapping the variables in a double integral.

more theorems

Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.

avoid suspicious Unicode;

separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial

--HG--
extra : rebase_source : 0045d1e39f330613bb1913e52e231f8be282a80a

generalized some theorems about integral domains and moved to HOL theories

--HG--
extra : rebase_source : 2e548495060b9f818a41b1e5333ed921a3b84ac4

uniform _ div _ as infix syntax for ring division

--HG--
extra : rebase_source : c4a1892078772c7ce9af33ad66e2abfefe7adea9

implicit partial divison operation in integral domains

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

semidom contains distributive minus, by convention

--HG--
extra : rebase_source : 4420e031f4e23e206f70aacf7e83ad435f0ecaf1

rationalised and generalised some theorems concerning abs and x^2.

clarified no_zero_devisors: makes only sense in a semiring;
actually turn linorder_semidom into a integral domain

--HG--
extra : rebase_source : 20e224f329987c38e10dba58521b744a19110ced

dropped long-outdated comments

--HG--
extra : rebase_source : c3805cc7b8142bcb3c3f9ab78422964cfc979e5e

distributivity of partial minus establishes desired properties of dvd in semirings

--HG--
extra : rebase_source : 99dad957de0410b3a1ca21ff1f8723495b31194f

establish unique preferred fact names

eliminated fact duplicates

fact consolidation

generalized lemmas (particularly concerning dvd) as far as appropriate

import general theorems from AFP/Markov_Models

equivalence rules for structures without zero divisors

--HG--
extra : rebase_source : 117d7728292b1473f0416ee8615654859adf7216

modernized header uniformly as section;

use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating

generalized and consolidated some theorems concerning divisibility

more facts about abstract divisibility

generalized

added various facts

prefer ac_simps collections over separate name bindings for add and mult

reduced name variants for assoc and commute on plus and mult

made mult_pos_pos a simp rule

made mult_nonneg_nonneg a simp rule

--HG--
extra : rebase_source : 3f70ac991fa0f02839309ce9b8f418ff53f87c36

field_simps: better support for negation and division, and power

Some rationalisation of basic lemmas

fix typo

split rules for of_bool, similar to if

--HG--
extra : rebase_source : 46c3590318b4d30449a1b2cb0c2e36b7eaf0b895

more antiquotations;

eliminiated neg_numeral in favour of - (numeral _)

fact generalization and name consolidation

more simplification rules on unary and binary minus

--HG--
extra : rebase_source : 7c88c9f33c4be8eae76f508a1a73ba79c8b769b1

generalized of_bool conversion

--HG--
extra : rebase_source : 0f21b3a0abf378a5790fe67ade4b7943cb3b0220

killed most "no_atp", to make Sledgehammer more complete

migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier

--HG--
extra : rebase_source : ff8027ac9606264aa4b2d4f8da037c426a3db98b

move real_isLub_unique to isLub_unique in Lubs; real_sum_of_halves to RealDef; abs_diff_less_iff to Rings

corrected nonsensical associativity of `` and dvd

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

tuned proofs

replace lemma realpow_two_diff with new lemma square_diff_square_factored

--HG--
extra : transplant_source : %8C%269%B5%E7%86%82%3E%BF%C7%19%EA%2CN%BA%3A%E8%D3%CD%00

rename real_squared_diff_one_factored to square_diff_one_factored and move to Rings.thy

moved division ring stuff from Rings.thy to Fields.thy

dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates

dropped superfluous [code del]s

declare add_nonneg_nonneg [simp]; remove now-redundant lemmas realpow_two_le_order(2)

remove simp attribute from square_eq_1_iff

move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff

moved some lemmas from Groebner_Basis here

dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero

less special treatment of times_divide_eq [simp]

more localization; factored out lemmas for division_ring

Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.

now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"

generalize some lemmas from class linordered_ring_strict to linordered_ring

tuned text

get rid of many duplicate simp rule warnings

dropped last occurence of the linlinordered accident

moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy

division ring assumes divide_inverse

renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields

--HG--
rename : src/HOL/Ring_and_Field.thy => src/HOL/Fields.thy
rename : src/HOL/OrderedGroup.thy => src/HOL/Groups.thy
rename : src/HOL/Ring_and_Field.thy => src/HOL/Rings.thy