| Tue, 26 Oct 2021 14:43:59 +0000 |
haftmann |
more generic bit/word lemmas for distribution
|
file |
diff |
annotate
|
| Mon, 02 Aug 2021 10:01:06 +0000 |
haftmann |
moved theory Bit_Operations into Main corpus
|
file |
diff |
annotate
|
| Mon, 12 Jul 2021 11:41:02 +0000 |
haftmann |
operations for symbolic computation of bit operations
|
file |
diff |
annotate
|
| Thu, 24 Jun 2021 06:06:32 +0000 |
haftmann |
more word cleanup
|
file |
diff |
annotate
|
| Wed, 16 Jun 2021 08:19:09 +0000 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
| Tue, 06 Apr 2021 18:12:20 +0000 |
haftmann |
new lemmas
|
file |
diff |
annotate
|
| Mon, 30 Nov 2020 17:10:49 +0100 |
wenzelm |
tuned whitespace --- avoid TABs;
|
file |
diff |
annotate
|
| Sun, 15 Nov 2020 10:13:03 +0000 |
haftmann |
official collection for bit projection simplifications
|
file |
diff |
annotate
|
| Tue, 27 Oct 2020 16:59:44 +0000 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
| Wed, 23 Sep 2020 11:14:38 +0000 |
haftmann |
more thorough treatment of division, particularly signed division on int and word
|
file |
diff |
annotate
|
| Thu, 17 Sep 2020 09:57:31 +0000 |
haftmann |
integrated generic conversions into word corpse
|
file |
diff |
annotate
|
| Thu, 17 Sep 2020 09:57:30 +0000 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
| Sat, 05 Sep 2020 08:32:27 +0000 |
haftmann |
generalized
|
file |
diff |
annotate
|
| Sun, 30 Aug 2020 15:15:28 +0000 |
haftmann |
more on conversions
|
file |
diff |
annotate
|
| Fri, 21 Aug 2020 18:59:30 +0000 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
| Sat, 01 Aug 2020 17:43:30 +0000 |
haftmann |
more consequent transferability
|
file |
diff |
annotate
|
| Sun, 12 Jul 2020 18:10:06 +0000 |
haftmann |
more simp rules for concrete numerical values
|
file |
diff |
annotate
|
| Sat, 11 Jul 2020 18:09:09 +0000 |
haftmann |
a generic horner sum operation
|
file |
diff |
annotate
|
| Sat, 11 Jul 2020 18:09:08 +0000 |
haftmann |
more thms
|
file |
diff |
annotate
|
| Fri, 03 Jul 2020 06:18:29 +0000 |
haftmann |
misc lemma tuning
|
file |
diff |
annotate
|
| Sat, 20 Jun 2020 05:56:28 +0000 |
haftmann |
simp rules for conversions
|
file |
diff |
annotate
|
| Sat, 20 Jun 2020 05:56:28 +0000 |
haftmann |
more class operations for the sake of efficient generated code
|
file |
diff |
annotate
|
| Thu, 18 Jun 2020 09:07:54 +0000 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
| Thu, 21 May 2020 20:00:08 +0000 |
haftmann |
tuned module name space for generated code
|
file |
diff |
annotate
|
| Wed, 13 May 2020 12:55:33 +0200 |
Manuel Eberl |
new constant power_int in HOL
|
file |
diff |
annotate
|
| Fri, 08 May 2020 06:26:28 +0000 |
haftmann |
prefer _ mod 2 over of_bool (odd _)
|
file |
diff |
annotate
|
| Mon, 27 Apr 2020 16:18:51 +0000 |
haftmann |
simplified construction of binary bit operations
|
file |
diff |
annotate
|
| Sat, 25 Apr 2020 13:26:24 +0000 |
haftmann |
more rules
|
file |
diff |
annotate
|
| Fri, 24 Apr 2020 13:16:41 +0000 |
haftmann |
numeral rules for take_bit / drop_bit on int
|
file |
diff |
annotate
|
| Thu, 16 Apr 2020 08:09:31 +0200 |
haftmann |
more theorems
|
file |
diff |
annotate
|
| Thu, 16 Apr 2020 08:09:29 +0200 |
haftmann |
bit on numerals
|
file |
diff |
annotate
|
| Thu, 16 Apr 2020 08:09:28 +0200 |
haftmann |
more complete rules on numerals
|
file |
diff |
annotate
|
| Sun, 08 Mar 2020 17:07:49 +0000 |
haftmann |
more frugal simp rules for bit operations; more pervasive use of bit selector
|
file |
diff |
annotate
|
| Tue, 11 Feb 2020 19:03:56 +0100 |
haftmann |
tuned proof
|
file |
diff |
annotate
|
| Sun, 09 Feb 2020 22:03:07 +0000 |
haftmann |
easy abstraction over pointwise bit operations
|
file |
diff |
annotate
|
| Sun, 09 Feb 2020 10:46:32 +0000 |
haftmann |
rule concerning bit (push_bit ...)
|
file |
diff |
annotate
|
| Sun, 09 Feb 2020 10:21:01 +0000 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
| Mon, 03 Feb 2020 20:42:04 +0000 |
haftmann |
more theorems
|
file |
diff |
annotate
|
| Sat, 01 Feb 2020 19:10:40 +0100 |
haftmann |
more specific class assumptions
|
file |
diff |
annotate
|
| Sat, 01 Feb 2020 19:10:37 +0100 |
haftmann |
more theorems
|
file |
diff |
annotate
|
| Sun, 26 Jan 2020 20:35:32 +0000 |
haftmann |
more theorems
|
file |
diff |
annotate
|
| Mon, 02 Dec 2019 17:15:16 +0000 |
haftmann |
tuned material
|
file |
diff |
annotate
|
| Sun, 01 Dec 2019 08:00:59 +0000 |
haftmann |
characterization of singleton bit operation
|
file |
diff |
annotate
|
| Wed, 27 Nov 2019 16:54:33 +0000 |
haftmann |
bit accessor and fundamental properties
|
file |
diff |
annotate
|
| Sat, 23 Nov 2019 09:56:11 +0000 |
haftmann |
tuned theory structure
|
file |
diff |
annotate
|
| Sun, 17 Nov 2019 20:44:35 +0000 |
haftmann |
strengthened type class for bit operations
|
file |
diff |
annotate
|
| Sat, 09 Nov 2019 15:39:21 +0000 |
haftmann |
bit shifts as class operations
|
file |
diff |
annotate
|
| Thu, 31 Oct 2019 09:02:02 +0000 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
| Sat, 19 Oct 2019 20:41:03 +0200 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
| Wed, 17 Jul 2019 14:02:42 +0100 |
paulson |
a few new lemmas and a bit of tidying
|
file |
diff |
annotate
|
| Sun, 16 Jun 2019 16:40:57 +0000 |
haftmann |
even more appropriate fact name
|
file |
diff |
annotate
|
| Fri, 14 Jun 2019 08:34:27 +0000 |
haftmann |
generalized type classes for parity to cover word types also, which contain zero divisors
|
file |
diff |
annotate
|
| Fri, 14 Jun 2019 08:34:27 +0000 |
haftmann |
slightly more specialized name for type class
|
file |
diff |
annotate
|
| Fri, 14 Jun 2019 08:34:27 +0000 |
haftmann |
dropped weaker legacy alias
|
file |
diff |
annotate
|
| Fri, 14 Jun 2019 08:34:27 +0000 |
haftmann |
slightly more stringent ordering of theorems
|
file |
diff |
annotate
|
| Wed, 01 May 2019 10:40:42 +0000 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Sun, 23 Dec 2018 20:51:23 +0000 |
haftmann |
more rules
|
file |
diff |
annotate
|
| Sat, 27 Oct 2018 15:30:38 +0200 |
nipkow |
moved lemmas
|
file |
diff |
annotate
|
| Wed, 06 Jun 2018 11:41:37 +0200 |
wenzelm |
proper white space;
|
file |
diff |
annotate
|
| Sat, 12 May 2018 22:20:46 +0200 |
haftmann |
removed some non-essential rules
|
file |
diff |
annotate
|
| Tue, 24 Apr 2018 14:17:58 +0000 |
haftmann |
proper datatype for 8-bit characters
|
file |
diff |
annotate
|
| Fri, 20 Apr 2018 07:36:58 +0000 |
haftmann |
algebraic embeddings for bit operations
|
file |
diff |
annotate
|
| Mon, 16 Apr 2018 05:34:25 +0000 |
haftmann |
explicit simp rules for computing abstract bit operations
|
file |
diff |
annotate
|
| Thu, 05 Apr 2018 06:15:02 +0000 |
haftmann |
even more on bit operations
|
file |
diff |
annotate
|
| Wed, 04 Apr 2018 20:52:36 +0200 |
haftmann |
more bit operation conversions
|
file |
diff |
annotate
|
| Wed, 21 Mar 2018 19:39:24 +0100 |
haftmann |
tuned proof
|
file |
diff |
annotate
|
| Wed, 21 Mar 2018 19:39:23 +0100 |
haftmann |
prefer convention to place operation name before type name
|
file |
diff |
annotate
|
| Tue, 20 Mar 2018 09:27:40 +0000 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
| Tue, 20 Mar 2018 09:27:39 +0000 |
haftmann |
generalized
|
file |
diff |
annotate
|
| Mon, 12 Mar 2018 08:25:35 +0000 |
haftmann |
eliminiated superfluous class semiring_bits
|
file |
diff |
annotate
|
| Sat, 10 Mar 2018 19:36:59 +0000 |
haftmann |
abstract algebraic bit operations
|
file |
diff |
annotate
|
| Mon, 08 Jan 2018 17:11:25 +0000 |
paulson |
moved in some material from Euler-MacLaurin
|
file |
diff |
annotate
|
| Thu, 23 Nov 2017 13:00:00 +0000 |
haftmann |
new simp rule
|
file |
diff |
annotate
|
| Sat, 11 Nov 2017 18:41:08 +0000 |
haftmann |
dedicated definition for coprimality
|
file |
diff |
annotate
|
| Mon, 09 Oct 2017 19:10:52 +0200 |
haftmann |
canonical multiplicative euclidean size
|
file |
diff |
annotate
|
| Mon, 09 Oct 2017 19:10:51 +0200 |
haftmann |
clarified parity
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:22 +0200 |
haftmann |
more fundamental definition of div and mod on int
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:22 +0200 |
haftmann |
one uniform type class for parity structures
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:21 +0200 |
haftmann |
elementary definition of division on natural numbers
|
file |
diff |
annotate
|
| Sun, 27 Aug 2017 06:27:01 +0200 |
bulwahn |
another fact on (- 1) ^ _
|
file |
diff |
annotate
|
| Wed, 04 Jan 2017 21:28:29 +0100 |
haftmann |
moved euclidean ring to HOL
|
file |
diff |
annotate
|
| Wed, 10 Aug 2016 22:05:36 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Sat, 12 Mar 2016 22:04:52 +0100 |
haftmann |
model characters directly as range 0..255
|
file |
diff |
annotate
|
| Wed, 06 Jan 2016 12:18:53 +0100 |
hoelzl |
add the proof of the central limit theorem
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 10:38:04 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Mon, 02 Nov 2015 11:56:28 +0100 |
eberlm |
Rounding function, uniform limits, cotangent, binomial identities
|
file |
diff |
annotate
|
| Thu, 06 Aug 2015 23:56:48 +0200 |
haftmann |
slight cleanup of lemmas
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Tue, 23 Jun 2015 16:55:28 +0100 |
paulson |
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.
|
file |
diff |
annotate
|
| Mon, 01 Jun 2015 18:59:20 +0200 |
haftmann |
correct sort constraints for abbreviations in type classes
|
file |
diff |
annotate
|
| Mon, 23 Mar 2015 19:05:14 +0100 |
haftmann |
distributivity of partial minus establishes desired properties of dvd in semirings
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Sun, 26 Oct 2014 19:11:16 +0100 |
haftmann |
eliminated redundancies;
|
file |
diff |
annotate
|
| Thu, 23 Oct 2014 19:40:41 +0200 |
haftmann |
even further downshift of theory Parity in the hierarchy
|
file |
diff |
annotate
|
| Thu, 23 Oct 2014 19:40:39 +0200 |
haftmann |
further downshift of theory Parity in the hierarchy
|
file |
diff |
annotate
|
| Thu, 23 Oct 2014 14:04:05 +0200 |
haftmann |
slight generalization and unification of simp rules for algebraic procedures
|
file |
diff |
annotate
|
| Thu, 23 Oct 2014 14:04:05 +0200 |
haftmann |
downshift of theory Parity in the hierarchy
|
file |
diff |
annotate
|
| Thu, 23 Oct 2014 14:04:05 +0200 |
haftmann |
parity induction over natural numbers
|
file |
diff |
annotate
|
| Tue, 21 Oct 2014 21:10:44 +0200 |
haftmann |
turn even into an abbreviation
|
file |
diff |
annotate
|
| Mon, 20 Oct 2014 17:00:13 +0200 |
wenzelm |
repared document;
|
file |
diff |
annotate
|
| Mon, 20 Oct 2014 07:57:33 +0200 |
haftmann |
more standard declaration for presburger
|
file |
diff |
annotate
|
| Mon, 20 Oct 2014 07:45:58 +0200 |
haftmann |
augmented and tuned facts on even/odd and division
|
file |
diff |
annotate
|
| Sun, 19 Oct 2014 18:05:26 +0200 |
haftmann |
prefer generic elimination rules for even/odd over specialized unfold rules for nat
|
file |
diff |
annotate
|
| Thu, 16 Oct 2014 19:26:28 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Thu, 16 Oct 2014 19:26:27 +0200 |
haftmann |
standard elimination rule for even
|
file |
diff |
annotate
|
| Thu, 16 Oct 2014 19:26:26 +0200 |
haftmann |
tuned facts on even and power
|
file |
diff |
annotate
|
| Thu, 16 Oct 2014 19:26:14 +0200 |
haftmann |
restructured
|
file |
diff |
annotate
|
| Thu, 16 Oct 2014 19:26:13 +0200 |
haftmann |
even more cleanup
|
file |
diff |
annotate
|
| Tue, 14 Oct 2014 08:23:23 +0200 |
haftmann |
legacy cleanup
|
file |
diff |
annotate
|
| Tue, 14 Oct 2014 08:23:23 +0200 |
haftmann |
more algebraic deductions for facts on even/odd
|
file |
diff |
annotate
|
| Tue, 14 Oct 2014 08:23:23 +0200 |
haftmann |
more algebraic deductions for facts on even/odd
|
file |
diff |
annotate
|
| Tue, 14 Oct 2014 08:23:23 +0200 |
haftmann |
purely algebraic characterization of even and odd
|
file |
diff |
annotate
|
| Thu, 09 Oct 2014 22:43:48 +0200 |
haftmann |
more foundational definition for predicate even
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 10:05:53 +0100 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
file |
diff |
annotate
|
| Thu, 31 Oct 2013 11:44:20 +0100 |
haftmann |
purely algebraic foundation for even/odd
|
file |
diff |
annotate
|
| Thu, 31 Oct 2013 11:44:20 +0100 |
haftmann |
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
|
file |
diff |
annotate
|
| Fri, 30 Mar 2012 15:43:30 +0200 |
huffman |
remove redundant simp rule
|
file |
diff |
annotate
|
| Fri, 30 Mar 2012 15:24:24 +0200 |
huffman |
add simp rules for eve/odd on numerals
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 15:53:48 +0200 |
huffman |
remove redundant lemma
|
file |
diff |
annotate
|