| Mon, 02 Apr 2012 09:18:16 +0200 |
huffman |
add simp rules for dvd on negative numerals
|
file |
diff |
annotate
|
| Sun, 01 Apr 2012 16:09:58 +0200 |
huffman |
removed Nat_Numeral.thy, moving all theorems elsewhere
|
file |
diff |
annotate
|
| Fri, 30 Mar 2012 11:16:35 +0200 |
huffman |
removed redundant nat-specific copies of theorems
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 20:19:23 +0200 |
huffman |
remove more redundant lemmas
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 16:49:23 +0200 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 19:21:05 +0200 |
huffman |
remove redundant lemmas
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 16:04:51 +0200 |
huffman |
generalized lemma zpower_zmod
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 15:53:48 +0200 |
huffman |
remove redundant lemma
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 15:40:11 +0200 |
huffman |
remove redundant lemma
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 15:34:04 +0200 |
huffman |
generalize more div/mod lemmas
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 15:27:49 +0200 |
huffman |
generalize some theorems about div/mod
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 14:49:56 +0200 |
huffman |
remove redundant lemmas
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 12:42:54 +0200 |
huffman |
move int::ring_div instance upward, simplify several proofs
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 11:45:02 +0200 |
huffman |
rename lemmas {divmod_int_rel_{div,mod} -> {div,mod}_int_unique, for consistency with nat lemma names
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 11:41:16 +0200 |
huffman |
extend definition of divmod_int_rel to handle denominator=0 case
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 11:02:18 +0200 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 10:34:12 +0200 |
huffman |
shorten a proof
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 10:20:31 +0200 |
huffman |
simplify some proofs
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 09:54:39 +0200 |
huffman |
rename lemmas {div,mod}_eq -> {div,mod}_nat_unique, for consistency with minus_unique, inverse_unique, etc.
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 09:44:56 +0200 |
huffman |
simplify some proofs
|
file |
diff |
annotate
|
| Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| Tue, 21 Feb 2012 11:04:38 +0100 |
huffman |
remove constant negateSnd in favor of 'apsnd uminus' (from Florian Haftmann)
|
file |
diff |
annotate
|
| Mon, 20 Feb 2012 15:17:03 +0100 |
bulwahn |
removing some unnecessary premises from Divides
|
file |
diff |
annotate
|
| Mon, 20 Feb 2012 14:23:46 +0100 |
huffman |
simplify projections on simultaneous computations of div and mod; tuned structure (from Florian Haftmann)
|
file |
diff |
annotate
|
| Thu, 29 Dec 2011 10:47:54 +0100 |
haftmann |
semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 21:07:10 +0100 |
wenzelm |
eliminated obsolete "standard";
|
file |
diff |
annotate
|
| Wed, 16 Nov 2011 15:20:27 +0100 |
huffman |
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
|
file |
diff |
annotate
|
| Fri, 21 Oct 2011 11:17:14 +0200 |
bulwahn |
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
| Tue, 06 Sep 2011 19:03:41 -0700 |
huffman |
avoid using legacy theorem names
|
file |
diff |
annotate
|
| Wed, 29 Jun 2011 17:35:46 +0200 |
wenzelm |
modernized some simproc setup;
|
file |
diff |
annotate
|
| Mon, 21 Feb 2011 10:44:19 +0100 |
blanchet |
renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
|
file |
diff |
annotate
|
| Fri, 14 Jan 2011 15:44:47 +0100 |
wenzelm |
eliminated global prems;
|
file |
diff |
annotate
|
| Fri, 17 Sep 2010 16:15:33 +0200 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 18:36:22 +0200 |
wenzelm |
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 10:48:37 +0200 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
| Tue, 04 May 2010 08:55:39 +0200 |
haftmann |
a ring_div is a ring_1_no_zero_divisors
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 19:55:07 +0100 |
boehmes |
tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
|
file |
diff |
annotate
|
| Tue, 09 Mar 2010 15:47:15 +0100 |
haftmann |
weakend class ring_div; tuned
|
file |
diff |
annotate
|
| Mon, 08 Mar 2010 09:38:58 +0100 |
haftmann |
transfer: avoid camel case
|
file |
diff |
annotate
|
| Wed, 24 Feb 2010 14:19:53 +0100 |
haftmann |
lemma div_mult_swap, dvd_div_eq_mult, dvd_div_div_eq_mult
|
file |
diff |
annotate
|
| Thu, 18 Feb 2010 14:21:44 -0800 |
huffman |
get rid of many duplicate simp rule warnings
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 17:12:38 +0100 |
haftmann |
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
|
file |
diff |
annotate
|
| Tue, 02 Feb 2010 11:38:38 +0100 |
blanchet |
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
|
file |
diff |
annotate
|
| Sat, 02 Jan 2010 21:31:15 +0100 |
nipkow |
removed legacy asm_lr
|
file |
diff |
annotate
|
| Fri, 18 Dec 2009 12:00:29 +0100 |
blanchet |
polished Nitpick's binary integer support etc.;
|
file |
diff |
annotate
|
| Fri, 20 Nov 2009 07:23:36 +0100 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Tue, 17 Nov 2009 11:10:22 +0000 |
webertj |
Fixed splitting of div and mod on integers (split theorem differed from implementation).
|
file |
diff |
annotate
|
| Tue, 17 Nov 2009 10:17:53 +0000 |
webertj |
Fixed splitting of div and mod on integers (split theorem differed from implementation).
|
file |
diff |
annotate
|
| Fri, 30 Oct 2009 18:32:40 +0100 |
haftmann |
tuned code setup
|
file |
diff |
annotate
|
| Fri, 30 Oct 2009 14:00:43 +0100 |
haftmann |
combined former theories Divides and IntDiv to one theory Divides
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 22:13:09 +0100 |
haftmann |
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 11:41:36 +0100 |
haftmann |
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 19:09:47 +0100 |
haftmann |
moved theory Divides after theory Nat_Numeral; tuned some proof texts
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 17:44:03 +0100 |
haftmann |
moved lemmas for dvd on nat to theories Nat and Power
|
file |
diff |
annotate
|
| Wed, 15 Jul 2009 23:48:21 +0200 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Tue, 14 Jul 2009 10:54:04 +0200 |
haftmann |
code attributes use common underscore convention
|
file |
diff |
annotate
|
| Tue, 07 Jul 2009 17:39:51 +0200 |
nipkow |
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
|
file |
diff |
annotate
|
| Mon, 15 Jun 2009 21:29:04 -0700 |
huffman |
generalize lemmas dvd_mod and dvd_mod_iff to class semiring_div
|
file |
diff |
annotate
|
| Mon, 15 Jun 2009 17:59:36 -0700 |
huffman |
move lemma div_power into semiring_div context; class ring_div inherits from idom
|
file |
diff |
annotate
|
| Tue, 28 Apr 2009 13:34:45 +0200 |
haftmann |
dropped reference to class recpower and lemma duplicate
|
file |
diff |
annotate
|
| Thu, 16 Apr 2009 14:02:11 +0200 |
haftmann |
tuned setups of CancelDivMod
|
file |
diff |
annotate
|
| Thu, 16 Apr 2009 10:11:34 +0200 |
haftmann |
tightended specification of class semiring_div
|
file |
diff |
annotate
|
| Wed, 15 Apr 2009 15:30:37 +0200 |
haftmann |
more coherent developement in Divides.thy and IntDiv.thy
|
file |
diff |
annotate
|
| Wed, 01 Apr 2009 18:41:15 +0200 |
nipkow |
added nat_div_gt_0 [simp]
|
file |
diff |
annotate
|
| Wed, 01 Apr 2009 16:03:00 +0200 |
nipkow |
added strong_setprod_cong[cong] (in analogy with setsum)
|
file |
diff |
annotate
|
| Thu, 26 Mar 2009 20:08:55 +0100 |
wenzelm |
interpretation/interpret: prefixes are mandatory by default;
|
file |
diff |
annotate
|
| Sun, 22 Mar 2009 20:46:11 +0100 |
haftmann |
lemma nat_dvd_not_less moved here from Arith_Tools
|
file |
diff |
annotate
|
| Thu, 12 Mar 2009 23:01:25 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Thu, 12 Mar 2009 18:01:26 +0100 |
haftmann |
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
|
file |
diff |
annotate
|
| Thu, 12 Mar 2009 15:31:26 +0100 |
nipkow |
added div lemmas
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Tue, 03 Mar 2009 17:05:18 +0100 |
nipkow |
removed and renamed redundant lemmas
|
file |
diff |
annotate
|
| Sun, 01 Mar 2009 10:24:57 +0100 |
nipkow |
added lemmas by Jeremy Avigad
|
file |
diff |
annotate
|
| Mon, 23 Feb 2009 16:25:52 -0800 |
huffman |
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
|
file |
diff |
annotate
|
| Mon, 23 Feb 2009 13:55:36 -0800 |
huffman |
move lemma dvd_mod_imp_dvd into class semiring_div
|
file |
diff |
annotate
|
| Sun, 22 Feb 2009 11:30:41 +0100 |
nipkow |
added dvd_div_mult
|
file |
diff |
annotate
|
| Sat, 21 Feb 2009 20:52:30 +0100 |
nipkow |
Removed subsumed lemmas
|
file |
diff |
annotate
|
| Fri, 20 Feb 2009 20:50:49 +0100 |
nipkow |
removed subsumed lemmas
|
file |
diff |
annotate
|
| Wed, 18 Feb 2009 10:24:48 -0800 |
huffman |
generalize le_imp_power_dvd and power_le_dvd; move from Divides to Power
|
file |
diff |
annotate
|
| Tue, 17 Feb 2009 18:48:17 +0100 |
nipkow |
Cleaned up IntDiv and removed subsumed lemmas.
|
file |
diff |
annotate
|
| Sun, 15 Feb 2009 22:58:02 +0100 |
nipkow |
dvd and setprod lemmas
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 16:29:16 +0100 |
nipkow |
Replaced group_ and ring_simps by algebra_simps;
|
file |
diff |
annotate
|
| Fri, 16 Jan 2009 14:58:11 +0100 |
haftmann |
migrated class package to new locale implementation
|
file |
diff |
annotate
|
| Thu, 08 Jan 2009 09:12:29 -0800 |
huffman |
add class ring_div; generalize mod/diff/minus proofs for class ring_div
|
file |
diff |
annotate
|
| Thu, 08 Jan 2009 08:36:16 -0800 |
huffman |
generalize zmod_zmod_cancel -> mod_mod_cancel
|
file |
diff |
annotate
|
| Thu, 08 Jan 2009 08:24:08 -0800 |
huffman |
generalize some div/mod lemmas; remove type-specific proofs
|
file |
diff |
annotate
|
| Tue, 30 Dec 2008 11:10:01 +0100 |
ballarin |
Merged.
|
file |
diff |
annotate
|
| Thu, 11 Dec 2008 18:30:26 +0100 |
ballarin |
Conversion of HOL-Main and ZF to new locales.
|
file |
diff |
annotate
|
| Thu, 11 Dec 2008 08:56:02 +0100 |
nipkow |
codegen
|
file |
diff |
annotate
|
| Mon, 17 Nov 2008 17:00:55 +0100 |
haftmann |
tuned unfold_locales invocation
|
file |
diff |
annotate
|
| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| Wed, 17 Sep 2008 21:27:08 +0200 |
wenzelm |
back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
|
file |
diff |
annotate
|
| Mon, 21 Jul 2008 15:27:23 +0200 |
haftmann |
(re-)added simp rules for (_ + _) div/mod _
|
file |
diff |
annotate
|
| Fri, 18 Jul 2008 18:25:53 +0200 |
haftmann |
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
|
file |
diff |
annotate
|
| Fri, 11 Jul 2008 09:02:22 +0200 |
haftmann |
separate class dvd for divisibility predicate
|
file |
diff |
annotate
|
| Fri, 25 Apr 2008 15:30:33 +0200 |
krauss |
Merged theories about wellfoundedness into one: Wellfounded.thy
|
file |
diff |
annotate
|
| Mon, 17 Mar 2008 18:37:00 +0100 |
wenzelm |
removed duplicate lemmas;
|
file |
diff |
annotate
|
| Wed, 20 Feb 2008 14:52:34 +0100 |
haftmann |
using only an relation predicate to construct div and mod
|
file |
diff |
annotate
|
| Fri, 15 Feb 2008 16:09:12 +0100 |
haftmann |
<= and < on nat no longer depend on wellfounded relations
|
file |
diff |
annotate
|
| Wed, 13 Feb 2008 09:35:31 +0100 |
haftmann |
more abstract lemmas
|
file |
diff |
annotate
|
| Wed, 23 Jan 2008 22:57:09 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Tue, 22 Jan 2008 23:07:21 +0100 |
haftmann |
added class semiring_div
|
file |
diff |
annotate
|
| Fri, 07 Dec 2007 15:07:59 +0100 |
haftmann |
instantiation target rather than legacy instance
|
file |
diff |
annotate
|
| Tue, 23 Oct 2007 23:27:23 +0200 |
nipkow |
went back to >0
|
file |
diff |
annotate
|
| Sun, 21 Oct 2007 14:53:44 +0200 |
nipkow |
Eliminated most of the neq0_conv occurrences. As a result, many
|
file |
diff |
annotate
|
| Sat, 20 Oct 2007 12:09:33 +0200 |
chaieb |
fixed proofs
|
file |
diff |
annotate
|
| Tue, 16 Oct 2007 23:12:45 +0200 |
haftmann |
global class syntax
|
file |
diff |
annotate
|
| Fri, 12 Oct 2007 08:20:46 +0200 |
haftmann |
class div inherits from class times
|
file |
diff |
annotate
|
| Sat, 29 Sep 2007 08:58:51 +0200 |
haftmann |
proper syntax during class specification
|
file |
diff |
annotate
|
| Wed, 15 Aug 2007 12:52:56 +0200 |
paulson |
ATP blacklisting is now in theory data, attribute noatp
|
file |
diff |
annotate
|
| Tue, 14 Aug 2007 23:04:27 +0200 |
huffman |
minimize imports
|
file |
diff |
annotate
|
| Tue, 24 Jul 2007 15:20:45 +0200 |
haftmann |
using class target
|
file |
diff |
annotate
|
| Tue, 10 Jul 2007 09:23:10 +0200 |
haftmann |
introduced (auxiliary) class dvd_mod for more convenient code generation
|
file |
diff |
annotate
|
| Thu, 31 May 2007 18:16:50 +0200 |
wenzelm |
removed dead code;
|
file |
diff |
annotate
|
| Sat, 19 May 2007 11:33:21 +0200 |
haftmann |
uniform module names for code generation
|
file |
diff |
annotate
|
| Thu, 17 May 2007 19:49:16 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Thu, 10 May 2007 10:21:44 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Sun, 06 May 2007 21:50:17 +0200 |
haftmann |
changed code generator invocation syntax
|
file |
diff |
annotate
|