#
95d60bd3 |
|
02-Oct-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove -- as an alias for Term parser. As per comment in release notes this has long been replaced as appropriate style.
|
#
55622e44 |
|
24-Apr-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Get core HOL to build with new definition of "by" Progress with github issue #407
|
#
94b064b9 |
|
15-Aug-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove unnecessary structure bracketting As per 89fc99bc3, but on as many examples as a grep -R can find.
|
#
22dff31f |
|
28-Jul-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix integer theories in light of pat_assum rename
|
#
7b73c8d7 |
|
16-Jul-2010 |
Konrad Slind <konrad.slind@gmail.com> |
src/num/theories/SingleStep.{sig,sml} is gone. The defininitions of Cases, Cases_on, Induct, Induct_on, CASE_TAC (and co.) are now in basicProof/BasicProvers. completeInduct_on and measureInduct_on are now in numLib. recInduct is now in src/tfl/Induction.sml. All these are collected in bossLib, so the changes should be invisible to ordinary users. SingleStep.*.doc has been changed accordingly. BasicProvers.NORM_TAC should now automatically perform all case splits (from if-then-else expressions as well as case expression) arising anywhere in the goal.
|
#
ff453f9e |
|
11-Sep-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Add an embodiment of the Omega d.p. for use inside the simplifier. It can perform quite badly on goals with too many disjunctive assumptions (and ~(x = y) counts as a disjunction).
|
#
aed05f4e |
|
20-Jul-2008 |
Konrad Slind <konrad.slind@gmail.com> |
A whole mess of small changes intended at making simpsets prettyprint informatively in the interactive loop. Very possibly I haven't updated all the files in the examples directories.
|
#
d8e57a78 |
|
16-Feb-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Add more aggressive normalisation of multiplicative expressions to ARITH_ss. Also provide old_arith_ss values for scripts that don't want this new behaviour. Update proofs to go through again. Some should be a bit more robust in the face of future changes to arith_ss. Others just punt and refer to old_arith_ss.
|
#
4cddaa12 |
|
12-Jul-2005 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Changed a couple of misleading/annoying names. The type ssdata is now called ssfrag (to bring it into line with documentation that talks about simpset fragments), and the constructor SIMPSET is now called SSFRAG. It never created a simpset, so the latter was a stupid name.
|
#
3b9afa98 |
|
07-Jul-2004 |
Konrad Slind <konrad.slind@gmail.com> |
Changed NUMERAL_BIT1 and NUMERAL_BIT2 to BIT1 and BIT2, respectively. Sorry, they were just too long. Also, ALT_ZERO is now named ZERO.
|
#
37c06a9b |
|
21-Jan-2004 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
A fix for the bug in AC-rewriting. Thanks to Tobias Nipkow who showed me the ordering function used by Isabelle. A few changes needed to be made to the integer theory scripts to cope with the changed behaviour.
|
#
1286b18c |
|
21-Apr-2003 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Sorry to have broken the build. By way of recompense, here's my independent fix for the problem (checking it in over Joe's because it's shorter).
|
#
f76e7dc3 |
|
17-Apr-2003 |
Joe Hurd <joe@gilith.com> |
Fixed the build.
|
#
5b7b7cf1 |
|
06-Mar-2002 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Omega now passes all of its tests, and I claim it's probably now a reasonable approximation of a complete procedure for doing Preburger arithmetic. Aggressive preprocessing attempts to minimise DNF blowup, but the fact that EXISTS_OR_CONV can still consume over 10% of the procedure's running time basically sucks.
|
#
f32f2816 |
|
04-Mar-2002 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Omega now works on all of the test case, bar KXSDIV1, on which it blows up. Some investigation suggests that this is "just" an efficiency issue and not one of code correctness. With luck, I'll check in some efficiency changes tomorrow, and then I'll be done.
|
#
8ebf18ee |
|
28-Feb-2002 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Very close to a complete symbolic method.
|
#
bedc114f |
|
20-Nov-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
New proof of the principle that lets me turn 0 <= nx + c into 0 <= x + c/n and a corresponding change in the implementation of gcd_check in OmegaMath.
|
#
ec22eab3 |
|
15-Nov-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Omega equality elimination done. Some new supporting theorems required. Is a bit slow, so will need to profile quite a bit to see just what's wrong.
|
#
c70e7114 |
|
26-Oct-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Added file that will be basis for implementation of Omega Test for Presburger arithmetic. (Also push a divisibility theorem into core integerTheory, and slightly change it.)
|
#
1581a0a8 |
|
25-Oct-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fairly extensive modifications to give integerTheory two division functions (and each gets a corresponding mod function too). They are int_div (int_mod) and int_quot (int_rem). All are abbreviated by the printer-parser: int_mod : % int_div : / int_rem : rem int_quot : quot The behaviour is as for the SML constants of the Basis Library's Integer structure. Most theorems about one function have analogous theorems in the other camp. Cooper's algorithm modified to work with int_div and int_mod. I haven't made it work over the other pair, though I probably should at some stage.
|
#
4ae3e9df |
|
14-Sep-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
More reorganisation, mainly to remove listTheory as an ancestory wherever possible (it still persists as a necessary ancestor of CooperCore, but isn't used un-necessarily elsewhere). Also sped up phase5 of CooperCore some more.
|
#
6e70a142 |
|
24-Aug-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
New constant called bmarker used to mark certain boolean valued terms as interesting; allowing for simple rewriting to move these terms about within a conjunction. Possibly should be earlier in the distribution, as this technique could speed up UNWIND_EXISTS_CONV, which currently uses AC_CONV to do no more than pull one conjunct to the head of a term.
|
#
428c9ddf |
|
14-Aug-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Added another useful theorem to this theory. It's an easy derivation from existing theorems, but it's useful to have things "just so" when applying theorems in the middle of a big proof procedure. (Theorem is n | n * x + c = n | c )
|
#
26dac2a3 |
|
03-Aug-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Now builds, with successful proof of Cooper's first lemma for performing "delta-elimination". Have already proved second lemma, so should now be able to implement optimisation.
|
#
6536870b |
|
02-Aug-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Gotta go home; part-way through proof of delta-elimination lemma for Cooper's algorithm.
|
#
75e6bfb9 |
|
18-Jun-2001 |
Konrad Slind <konrad.slind@gmail.com> |
Changing arithLib to numLib.
|
#
463ce292 |
|
22-Feb-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Not going to change this anymore. Instead I'm going to write about how well it performs. Many improvements since last time, and a little more code factorisation as well. Code should be easy to adjust to use full gcd optimisations in future for pure goals.
|
#
a8d72aad |
|
19-Feb-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
In dividesScript: * change DIVIDES_REF to be DIVIDES_REFL * prove DIVIDES_TRANS In gcdScript: * eliminate a duplicate copy of GCD_0L * prove an efficient rewrite for calculating gcds with computeLib In intSyntax: * add {mk_,dest_,is_}injected functions In int_arithScript: * prove a couple more useful theorems for dealing with gcds In integerScript: * prove that x int_divides 1 = (x = 1) \/ (x = ~1)
|
#
1e6e9ce5 |
|
16-Feb-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Further speed improvements. Average of about 17% quicker. This comes mainly through not converting to NNF and the search for equalities to eliminate is now also more sophisticated.
|
#
695c147a |
|
24-Jan-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Cooper now can eliminate on the a's or the b's. Currently though it's forced into just the a's to test that part of the code, and there may be something very strange happening with the pt11 example. int_arith has picked up some new theorems to support all this.
|
#
8789fdcf |
|
19-Jan-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Added can_get_big theorem (a version of can_get_small really, as its short little proof makes clear).
|
#
1f0043b8 |
|
18-Jan-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
New theories of number theory (divides, prime, gcd) and a simple optimisation in Cooper that divides leaves through by the gcds of variable coefficients.
|
#
a6ab3353 |
|
17-Jan-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
New theorems about gcd and eliminating coefficients for use in Cooper.
|
#
c240c2ea |
|
10-Jan-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Reimplemented REDUCE_CONV in intSimps, by making it use computeLib directly. This should speed it up. Many _REDUCE theorems needed for this additionally proved in integerScript.sml. int_arithScript has just had a couple of minor tidy-ups.
|
#
fc228fee |
|
09-Nov-2000 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Made it all Kananaskis compatible.
|
#
4145a1c0 |
|
19-Apr-2000 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Decision procedure now keeps equality terms rather than normalising them away, and seems a deal quicker as a result, though its performance on pt7 has worsened by at least a factor of two. This will bear investigating.
|
#
bca48947 |
|
10-Apr-2000 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Added better rewrites for ODD and EVEN over :num, and also the (now unused HO_SUB_ELIM).
|
#
4a4282b5 |
|
28-Mar-2000 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Functionality updates for Cooper.sml. Still inefficient though. Code in comments is start of attempt to improve this.
|
#
06f3126a |
|
24-Mar-2000 |
Konrad Slind <konrad.slind@gmail.com> |
Purely notational changes. I thought the name "COOPER_CONV" would be catchy ...
|
#
af0e3845 |
|
24-Mar-2000 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Modifications now mean that decision procedure works over naturals as well.
|
#
8f4f91e8 |
|
23-Mar-2000 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
int_arith now exports a INT_ARITH_CONV and INT_ARITH_PROVE that implement smart integer decision proving. In particular, it attempts to prove things that aren't pure Presburger, by generalising out bad terms.
|
#
2547839a |
|
16-Mar-2000 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fixed a number of bugs and improved performance quite considerably. Performance tweaks could continue indefinitely from this point, but I think my time would be better spent on broadening the scope of the code I have.
|
#
d4b79503 |
|
15-Mar-2000 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Files for Cooper's algorithm, an implementation of a decision procedure for all of Presburger arithmetic, including arbitrary quantifier nesting and alternation. * int_arithScript.sml generates a theory with the pre-proved theorems needed for the algorithm. None of them are really very interesting in themselves, so don't really deserve to be in integerTheory itself. * int_arith.sml actually implements the algorithm. The procedure only works on formulae with no free variables and doesn't handle non-Presburger sub-terms at all. Future work will fix these two problems.
|