#
72a44fd3 |
|
21-Jan-2020 |
Manuel Eberl <eberlm@in.tum.de> |
Removed multiplicativity assumption from normalization_semidom
|
#
6e12876d |
|
26-Nov-2019 |
paulson <lp15@cam.ac.uk> |
Rearrangement of material in Complex_Analysis_Basics, which contained much that had nothing to do with complex analysis.
|
#
d16c1cf3 |
|
19-Oct-2019 |
haftmann <none@none> |
generalized
|
#
a4784f6f |
|
09-Oct-2019 |
haftmann <none@none> |
dedicated fact collections for algebraic simplification rules potentially splitting goals --HG-- extra : rebase_source : ebbd8d0c13409f8fb536c42910e904c24e43dbe6
|
#
a1c1e852 |
|
14-Jun-2019 |
haftmann <none@none> |
official fact collection sign_simps
|
#
4d2c32ff |
|
16-Apr-2019 |
haftmann <none@none> |
removed unused fact collections
|
#
699a497b |
|
13-Apr-2019 |
haftmann <none@none> |
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
|
#
851fe13c |
|
13-Apr-2019 |
haftmann <none@none> |
tuned --HG-- extra : rebase_source : 994f20cd611bcdd96775107d47e69a12c13a553c
|
#
4b992152 |
|
13-Apr-2019 |
haftmann <none@none> |
more document structure --HG-- extra : rebase_source : 25bedddd8d62a1123f6c95436ff194025ef344cb
|
#
b68ee0d0 |
|
13-Apr-2019 |
haftmann <none@none> |
tuned --HG-- extra : rebase_source : ebf4a99af3d387cb1075e3093d8c3b3acea006cc
|
#
a4a6b144 |
|
09-Apr-2019 |
haftmann <none@none> |
common type class for distributive division
|
#
504acaca |
|
14-Jan-2019 |
haftmann <none@none> |
tuned proofs
|
#
e60cf64d |
|
06-Jan-2019 |
wenzelm <none@none> |
isabelle update -u path_cartouches;
|
#
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
7bdeab0d |
|
23-May-2018 |
haftmann <none@none> |
grouped material on numeral division
|
#
f58e606d |
|
22-May-2018 |
haftmann <none@none> |
automatic classical rule to derive a dvd b from b mod a = 0
|
#
07d79256 |
|
22-May-2018 |
haftmann <none@none> |
consider dvdE for automated classical proving
|
#
cbf14186 |
|
22-Feb-2018 |
paulson <lp15@cam.ac.uk> |
type class linordered_nonzero_semiring has new axiom to guarantee characteristic 0
|
#
a1b2af0a |
|
21-Dec-2017 |
eberlm <eberlm@in.tum.de> |
Some lemmas on complex numbers and coprimality --HG-- extra : rebase_source : 37434802fd420fdcbc9750dcf9b734797e86eb61
|
#
1387b04b |
|
19-Dec-2017 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
603884cc |
|
23-Nov-2017 |
haftmann <none@none> |
tuned
|
#
85b3e948 |
|
11-Nov-2017 |
haftmann <none@none> |
dedicated definition for coprimality --HG-- extra : rebase_source : 891168c98ce62efae6b7e72c7d3365fea12b33ae
|
#
c297118b |
|
30-Oct-2017 |
haftmann <none@none> |
rule out pathologic instances --HG-- extra : rebase_source : b04515f7600d4314068b2fe100baa5b177111e0c
|
#
f740f805 |
|
08-Oct-2017 |
haftmann <none@none> |
more fundamental definition of div and mod on int --HG-- extra : rebase_source : 95b72d036b88e199c61235ea5833a905f5632800
|
#
5a89ad88 |
|
08-Oct-2017 |
haftmann <none@none> |
generalized simproc --HG-- extra : rebase_source : 1a484c6a7a8374a73f471204dea8be4ee982845f
|
#
b01640ea |
|
08-Oct-2017 |
haftmann <none@none> |
elementary definition of division on natural numbers --HG-- extra : rebase_source : 23767fa1baf28db39b18de60e52d4d7f852e48dd
|
#
6165cb7f |
|
08-Oct-2017 |
haftmann <none@none> |
tuned structure --HG-- extra : rebase_source : ad5aac8dba5969d5cd3c3923df071b0e5dad9747
|
#
5c09067f |
|
09-Oct-2017 |
paulson <lp15@cam.ac.uk> |
new material about connectedness, etc.
|
#
3a436e5d |
|
11-May-2017 |
haftmann <none@none> |
more lemmas --HG-- extra : rebase_source : e39561a47214aaf67eea524bde7eb12dcffc8801
|
#
ef5da5a8 |
|
09-Jan-2017 |
haftmann <none@none> |
slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization --HG-- extra : rebase_source : 0d5af77e2a7d66625c22923a19c456b1ca17652e
|
#
b540770d |
|
30-Dec-2016 |
haftmann <none@none> |
more facts on sgn, abs --HG-- extra : rebase_source : a98552b24ddce791c14679ddb3d0f5a27e23b00a
|
#
40424ca4 |
|
17-Dec-2016 |
haftmann <none@none> |
more fine-grained type class hierarchy for div and mod --HG-- extra : rebase_source : fffbeef99e834ca17596f478178e94bed8a014bc
|
#
8863117a |
|
17-Dec-2016 |
haftmann <none@none> |
restructured matter on polynomials and normalized fractions --HG-- extra : rebase_source : 71508900ff150d54097ae5c4c2da7176f09cb625
|
#
049952fc |
|
18-Oct-2016 |
haftmann <none@none> |
suitable logical type class for abs, sgn --HG-- extra : rebase_source : 27e95dd7f038f114d0cad11ec69599a166229041
|
#
54a0a039 |
|
16-Oct-2016 |
haftmann <none@none> |
more standardized theorem names for facts involving the div and mod identity
|
#
7cb68da2 |
|
16-Oct-2016 |
haftmann <none@none> |
more standardized names
|
#
fbcf6dd7 |
|
16-Oct-2016 |
haftmann <none@none> |
added lemma
|
#
b627764f |
|
12-Oct-2016 |
haftmann <none@none> |
separate type class for arbitrary quotient and remainder partitions --HG-- extra : rebase_source : c803a2a721f660672d64831c56088100891baa86
|
#
3c2b07e1 |
|
25-Sep-2016 |
haftmann <none@none> |
syntactic type class for operation mod named after mod; simplified assumptions of type class semiring_div --HG-- extra : rebase_source : 3714be7474835787b2a513b731c9864d1ac9d2c4
|
#
bebccfd5 |
|
25-Sep-2016 |
haftmann <none@none> |
more lemmas --HG-- extra : rebase_source : 3446eb0648af16d2212d2a3e40591332dd90c26c
|
#
23930628 |
|
18-Sep-2016 |
haftmann <none@none> |
more generic algebraic lemmas --HG-- extra : rebase_source : afd1b38644ce9418dc6eeaf977c35a8502e396b5
|
#
9b9c2176 |
|
12-Aug-2016 |
wenzelm <none@none> |
more symbols;
|
#
f937778a |
|
02-Aug-2016 |
wenzelm <none@none> |
misc tuning and modernization;
|
#
53ecc8a7 |
|
12-Jul-2016 |
fleury <Mathias.Fleury@mpi-inf.mpg.de> |
sharing simp rules between ordered monoids and rings
|
#
ae5f3742 |
|
01-Jul-2016 |
Manuel Eberl <eberlm@in.tum.de> |
More lemmas on Gcd/Lcm
|
#
e842a6c2 |
|
20-Jun-2016 |
wenzelm <none@none> |
misc tuning and modernization;
|
#
a2bc0021 |
|
25-Apr-2016 |
wenzelm <none@none> |
eliminated old 'def'; tuned comments;
|
#
041061bc |
|
16-Mar-2016 |
paulson <lp15@cam.ac.uk> |
Contractible sets. Also removal of obsolete theorems and refactoring
|
#
07a7e7cf |
|
13-Mar-2016 |
haftmann <none@none> |
more theorems on orderings --HG-- extra : rebase_source : 4e5a14cb68359f057eb65c380c103e23971ad09c
|
#
70cb89b7 |
|
01-Mar-2016 |
haftmann <none@none> |
tuned bootstrap order to provide type classes in a more sensible order --HG-- extra : rebase_source : b4008b5f377525bc1866d515a16702fbb0b463c9
|
#
35f7dccd |
|
23-Feb-2016 |
nipkow <none@none> |
more canonical names
|
#
3a51760b |
|
19-Feb-2016 |
hoelzl <none@none> |
generalize more theorems to support enat and ennreal --HG-- extra : rebase_source : 11176604a37483aa41462153f0aa289df506590d
|
#
3042fd7a |
|
12-Feb-2016 |
hoelzl <none@none> |
moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add --HG-- extra : rebase_source : 8674c79985a670cee921b8193965bb0767549a5c
|
#
cef8f2ad |
|
10-Feb-2016 |
hoelzl <none@none> |
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
|
#
a4a135aa |
|
18-Feb-2016 |
haftmann <none@none> |
more theorems --HG-- extra : rebase_source : de1d0718cda85a6dd4693328efc096fe8f9dfb2e
|
#
b376ab94 |
|
17-Feb-2016 |
haftmann <none@none> |
cleansed junk-producing interpretations for gcd/lcm on nat altogether
|
#
a6f23363 |
|
17-Feb-2016 |
haftmann <none@none> |
generalized some lemmas; moved some lemmas in more appropriate places; deleted potentially dangerous simp rule
|
#
08cabf03 |
|
27-Dec-2015 |
wenzelm <none@none> |
prefer symbols for "abs";
|
#
0df376fc |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
4b76bc27 |
|
01-Dec-2015 |
paulson <lp15@cam.ac.uk> |
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
|
#
420aaf4c |
|
12-Nov-2015 |
paulson <lp15@cam.ac.uk> |
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
|
#
6ee65982 |
|
06-Aug-2015 |
haftmann <none@none> |
slight cleanup of lemmas --HG-- extra : rebase_source : 17dbf1b3c59a40c2a2ac93ab58d3e6371773af6c
|
#
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
#
8ddc1a1c |
|
08-Jul-2015 |
haftmann <none@none> |
tuned facts
|
#
81da5767 |
|
08-Jul-2015 |
haftmann <none@none> |
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
|
#
2a11bf54 |
|
08-Jul-2015 |
haftmann <none@none> |
moved normalization and unit_factor into Main HOL corpus
|
#
7d3b4baf |
|
30-Jun-2015 |
paulson <lp15@cam.ac.uk> |
Useful lemmas. The theorem concerning swapping the variables in a double integral.
|
#
ca155b5f |
|
25-Jun-2015 |
haftmann <none@none> |
more theorems
|
#
456b0fa3 |
|
23-Jun-2015 |
paulson <lp15@cam.ac.uk> |
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.
|
#
16c97520 |
|
20-Jun-2015 |
wenzelm <none@none> |
avoid suspicious Unicode;
|
#
52933f0b |
|
18-Jun-2015 |
haftmann <none@none> |
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial --HG-- extra : rebase_source : 0045d1e39f330613bb1913e52e231f8be282a80a
|
#
76d32dc6 |
|
18-Jun-2015 |
haftmann <none@none> |
generalized some theorems about integral domains and moved to HOL theories --HG-- extra : rebase_source : 2e548495060b9f818a41b1e5333ed921a3b84ac4
|
#
603f8dfb |
|
12-Jun-2015 |
haftmann <none@none> |
uniform _ div _ as infix syntax for ring division --HG-- extra : rebase_source : c4a1892078772c7ce9af33ad66e2abfefe7adea9
|
#
a596c25e |
|
01-Jun-2015 |
haftmann <none@none> |
implicit partial divison operation in integral domains
|
#
f2ba2c03 |
|
01-Jun-2015 |
haftmann <none@none> |
separate class for division operator, with particular syntax added in more specific classes
|
#
922f2a27 |
|
02-Apr-2015 |
haftmann <none@none> |
semidom contains distributive minus, by convention --HG-- extra : rebase_source : 4420e031f4e23e206f70aacf7e83ad435f0ecaf1
|
#
afcf79aa |
|
31-Mar-2015 |
paulson <lp15@cam.ac.uk> |
rationalised and generalised some theorems concerning abs and x^2.
|
#
20f0204e |
|
28-Mar-2015 |
haftmann <none@none> |
clarified no_zero_devisors: makes only sense in a semiring; actually turn linorder_semidom into a integral domain --HG-- extra : rebase_source : 20e224f329987c38e10dba58521b744a19110ced
|
#
c706ba26 |
|
28-Mar-2015 |
haftmann <none@none> |
dropped long-outdated comments --HG-- extra : rebase_source : c3805cc7b8142bcb3c3f9ab78422964cfc979e5e
|
#
8c67c983 |
|
23-Mar-2015 |
haftmann <none@none> |
distributivity of partial minus establishes desired properties of dvd in semirings --HG-- extra : rebase_source : 99dad957de0410b3a1ca21ff1f8723495b31194f
|
#
55832464 |
|
19-Feb-2015 |
haftmann <none@none> |
establish unique preferred fact names
|
#
ca009b8d |
|
18-Feb-2015 |
haftmann <none@none> |
eliminated fact duplicates
|
#
20475beb |
|
14-Feb-2015 |
haftmann <none@none> |
fact consolidation
|
#
03e4974d |
|
17-Nov-2014 |
haftmann <none@none> |
generalized lemmas (particularly concerning dvd) as far as appropriate
|
#
ff53cb2b |
|
13-Nov-2014 |
hoelzl <none@none> |
import general theorems from AFP/Markov_Models
|
#
54a5703c |
|
08-Nov-2014 |
haftmann <none@none> |
equivalence rules for structures without zero divisors --HG-- extra : rebase_source : 117d7728292b1473f0416ee8615654859adf7216
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
2227b563 |
|
24-Oct-2014 |
hoelzl <none@none> |
use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
|
#
e88c2d7e |
|
12-Oct-2014 |
haftmann <none@none> |
generalized and consolidated some theorems concerning divisibility
|
#
8e17a876 |
|
12-Oct-2014 |
haftmann <none@none> |
more facts about abstract divisibility
|
#
8688f84c |
|
07-Sep-2014 |
haftmann <none@none> |
generalized
|
#
caa51abc |
|
06-Sep-2014 |
haftmann <none@none> |
added various facts
|
#
38907e37 |
|
05-Jul-2014 |
haftmann <none@none> |
prefer ac_simps collections over separate name bindings for add and mult
|
#
e46c07fd |
|
04-Jul-2014 |
haftmann <none@none> |
reduced name variants for assoc and commute on plus and mult
|
#
5723122d |
|
12-Apr-2014 |
nipkow <none@none> |
made mult_pos_pos a simp rule
|
#
a444e184 |
|
11-Apr-2014 |
nipkow <none@none> |
made mult_nonneg_nonneg a simp rule --HG-- extra : rebase_source : 3f70ac991fa0f02839309ce9b8f418ff53f87c36
|
#
d749d414 |
|
09-Apr-2014 |
hoelzl <none@none> |
field_simps: better support for negation and division, and power
|
#
956719cb |
|
19-Mar-2014 |
paulson <lp15@cam.ac.uk> |
Some rationalisation of basic lemmas
|
#
47cef352 |
|
04-Mar-2014 |
huffman <none@none> |
fix typo
|
#
a6ac997e |
|
30-Jan-2014 |
haftmann <none@none> |
split rules for of_bool, similar to if --HG-- extra : rebase_source : 46c3590318b4d30449a1b2cb0c2e36b7eaf0b895
|
#
b9995ead |
|
08-Dec-2013 |
wenzelm <none@none> |
more antiquotations;
|
#
138816de |
|
19-Nov-2013 |
haftmann <none@none> |
eliminiated neg_numeral in favour of - (numeral _)
|
#
68f78efa |
|
04-Nov-2013 |
haftmann <none@none> |
fact generalization and name consolidation
|
#
d2ef840a |
|
01-Nov-2013 |
haftmann <none@none> |
more simplification rules on unary and binary minus --HG-- extra : rebase_source : 7c88c9f33c4be8eae76f508a1a73ba79c8b769b1
|
#
7e25bf37 |
|
31-Oct-2013 |
haftmann <none@none> |
generalized of_bool conversion --HG-- extra : rebase_source : 0f21b3a0abf378a5790fe67ade4b7943cb3b0220
|
#
03633065 |
|
18-Oct-2013 |
blanchet <none@none> |
killed most "no_atp", to make Sledgehammer more complete
|
#
a7b3de52 |
|
23-Jun-2013 |
haftmann <none@none> |
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier --HG-- extra : rebase_source : ff8027ac9606264aa4b2d4f8da037c426a3db98b
|
#
68956f3f |
|
25-Mar-2013 |
hoelzl <none@none> |
move real_isLub_unique to isLub_unique in Lubs; real_sum_of_halves to RealDef; abs_diff_less_iff to Rings
|
#
825ed833 |
|
07-Dec-2012 |
nipkow <none@none> |
corrected nonsensical associativity of `` and dvd
|
#
d9333ba5 |
|
19-Oct-2012 |
webertj <none@none> |
Renamed {left,right}_distrib to distrib_{right,left}.
|
#
15635718 |
|
13-Sep-2011 |
huffman <none@none> |
tuned proofs
|
#
a76b916d |
|
20-Aug-2011 |
huffman <none@none> |
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
|
#
14b4f0dd |
|
20-Aug-2011 |
huffman <none@none> |
rename real_squared_diff_one_factored to square_diff_one_factored and move to Rings.thy
|
#
c6f0818a |
|
08-Aug-2011 |
huffman <none@none> |
moved division ring stuff from Rings.thy to Fields.thy
|
#
3ce93f38 |
|
23-Aug-2010 |
haftmann <none@none> |
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
|
#
140c6b08 |
|
12-Jul-2010 |
haftmann <none@none> |
dropped superfluous [code del]s
|
#
acf09750 |
|
17-May-2010 |
huffman <none@none> |
declare add_nonneg_nonneg [simp]; remove now-redundant lemmas realpow_two_le_order(2)
|
#
edfe12e9 |
|
17-May-2010 |
huffman <none@none> |
remove simp attribute from square_eq_1_iff
|
#
12069e19 |
|
10-May-2010 |
huffman <none@none> |
move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
|
#
754cf751 |
|
06-May-2010 |
haftmann <none@none> |
moved some lemmas from Groebner_Basis here
|
#
7e21e473 |
|
26-Apr-2010 |
haftmann <none@none> |
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
|
#
a2cff576 |
|
23-Apr-2010 |
haftmann <none@none> |
less special treatment of times_divide_eq [simp]
|
#
8f9b71d9 |
|
23-Apr-2010 |
haftmann <none@none> |
more localization; factored out lemmas for division_ring
|
#
a65fbeaf |
|
20-Apr-2010 |
hoelzl <none@none> |
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
|
#
206a5436 |
|
17-Mar-2010 |
blanchet <none@none> |
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
|
#
7417b1b7 |
|
06-Mar-2010 |
huffman <none@none> |
generalize some lemmas from class linordered_ring_strict to linordered_ring
|
#
43598f8f |
|
22-Feb-2010 |
haftmann <none@none> |
tuned text
|
#
aaaa7964 |
|
18-Feb-2010 |
huffman <none@none> |
get rid of many duplicate simp rule warnings
|
#
205de29f |
|
10-Feb-2010 |
haftmann <none@none> |
dropped last occurence of the linlinordered accident
|
#
75f69d99 |
|
10-Feb-2010 |
haftmann <none@none> |
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
|
#
eaea32cb |
|
10-Feb-2010 |
haftmann <none@none> |
division ring assumes divide_inverse
|
#
875c5b73 |
|
08-Feb-2010 |
haftmann <none@none> |
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
|