#
7f94f460 |
|
22-Aug-2018 |
Chun Tian (binghe) <binghe.lisp@gmail.com> |
Added rich_topologyTheory and dependents
|
#
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.
|
#
5d5a8494 |
|
09-Mar-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Preserve add_user_printer properly in grammar data This requires a slightly involved process for storing references to code in theory files. Update the .doc file on add_user_printer (which was already incredibly long), and add a test. Closes #367
|
#
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.
|
#
8859e568 |
|
28-Jul-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix real theories in light of pat_assum rename
|
#
9524847d |
|
10-Mar-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Remove some duplicates of the theorem TRUTH. These are: • INFINITE_DEF and IN_LIST_TO_SET (replaced with overloadings) • IN_APP_applied and IN_ABS_applied (inadvertently generated) Also, made changes to try to avoid new definitions in listTheory accidentally having a "_DEF" suffix instead of "_def". Old naming inconsistencies still remain in listTheory (e.g. EXISTS_DEF, FIND_def and FLAT). These changes will break a few proofs but patches should be trivial (i.e. removing references to these TRUTH theorems and/ or renaming "_DEF" to "_def").
|
#
7a5f60ec |
|
04-Dec-2015 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Provide support for evaluating float to int and real to int operations. For example, the following weren't working before (with intLib and realLib loaded): EVAL ``NUM_FLOOR (-0.5)``; (* |- flr (-0.5) = 0 *) EVAL ``NUM_CEILING 0.5``; (* |- clg 0.5 = 1 *) EVAL ``INT_FLOOR 0.5``; (* |- flr 0.5 = 0 *) EVAL ``INT_CEILING 0.5``; (* |- clg 0.5 = 1 *)
|
#
11b6c7f2 |
|
13-Mar-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Improvements to evaluation coverage for realTheory. Previously, the follow terms were failing to evaluate: ``sum (1, 4) real_of_num`` ``1 > 1 / 2`` ``1 >= 1 / 2`` ``flr (232 / 3)`` The operation "sum" is now introduced using Define.
|
#
285fb9ea |
|
28-Jul-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Give the real numbers decimal fractions.
|
#
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.
|
#
0e2788b5 |
|
22-Jun-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
INFINITE is now an abbreviation for ``\s. ~FINITE s``.
|
#
38724691 |
|
14-Jun-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Prove some results about the finite-ness or otherwise of some universal sets.
|
#
52fb1be0 |
|
21-Sep-2009 |
Tjark Weber <Tjark.Weber@cl.cam.ac.uk> |
Removed further functions from hol88Lib.
|
#
d9003833 |
|
26-Nov-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fairly dramatic change, supporting the use of "syntactic patterns". It is now possible to overload a name to term (typically a lambda-abstraction) in order to create syntax-only definitions. For example, there is a definition of not-equals now in the system: val _ = overload_on ("<>", ``\x y. ~(x = y)``) val _ = set_fixity "<>" (Infix(NONASSOC, 450)) This definition is parsed and pretty-printed. Two other annoying changes. The interface for adding unicode variants has changed, and I have made precedence level 450 of the parser non-associative. This latter change has caused most of the (minor) adjustments to the files below. The regression test doesn't go through yet. (Currently there is a failure in quotient/examples/sigma that I don't understand.)
|
#
effc431b |
|
01-Oct-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Change export_rewrites back to its old API (without requiring an extra string). When exported, the resulting simpset fragment always picked up the name of the theory to be the base of its name, so there didn't seem much point in giving users a false impression of naming power.
|
#
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.
|
#
c76376ed |
|
29-Apr-2008 |
Konrad Slind <konrad.slind@gmail.com> |
Additional functionality for abbreviations. 1. The labels library has been merged into markerLib and the src/labels directory eliminated. 2. Have added markerSyntax structure. 3. Operations on abbrevs used to all be in structure Q, even those that didn't deal with quotations (like UNABBREV_ALL_TAC). Now markerLib provides all abbrev. operations and these take terms. Operations that benefit from quotes, e.g., ABBREV_TAC, MATCH_ABBREV_TAC, etc. are still to be found in Q. 4. Abbrevs are kept reduced by the simplifiers and there is a REABBREV_TAC which can be separately called. This sorts abbrevs topologically, so that they get restored in a sensible order. 5. For situations where one wants to get rid of all abbrevs, apply a tactic, and then restore the abbrevs, there is WITHOUT_ABBREVS: tactic->tactic. 6. Have added a simple topological sort to Lib. 7. Updated proofs in the src directories, and also in examples/lambda.
|
#
a156bcaa |
|
25-Jun-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix a silly hole in the automatic simplification of real number arithmetic.
|
#
115d66cf |
|
14-May-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix a number of calculation bugs, mostly calculations involving zero. The new tests all used to fail.
|
#
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.
|
#
13f030c2 |
|
07-Feb-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Wide-ranging change to make the TypeBase export an interface forcing users to be concerned about which theory their types are from. Interactive users of the "induction_of", "axiom_of" and similar functions are thrown the only bone: they can effectively omit the theory parameter by using "" instead of a theory name. Prompted by a bug found by Tom Ridge where it was impossible to define a pattern matching function on a type with the same name as another type because the pattern-matching code was using dest_type and TypeBase.read on just the type-operator name.
|
#
05780524 |
|
12-Dec-2005 |
Konrad Slind <konrad.slind@gmail.com> |
Added floor and ceiling operations (mostly from Michael's NETSEM stuff).
|
#
bd417ac8 |
|
17-Mar-2005 |
Peter Homeier <palantir@trustworthytools.com> |
---------------------------------------------------------------------- Edited the "real" library to use the new quotient library. The hrealScript.sml and realScript.sml files only had a mention of EquivType in a comment, not for actual use; these have been deleted. The hratScript.sml and realaxScript.sml actually used the EquivType tool to do quotients; this has now been revised to use the quotient tool. In each case one new well-formedness (respectfulness) theorem had to be proven and included as an argument to the tool. In seqScript.sml, there was a small incompatibility where a definition of a new constant named "-->" conflicted with the constant "--> defined in the quotient library. This was healed by hiding the previous definition before making the new one. All of this was very straightforward. Modified Files: hol98/src/real/hratScript.sml hol98/src/real/hrealScript.sml hol98/src/real/realScript.sml hol98/src/real/realaxScript.sml hol98/src/real/seqScript.sml ----------------------------------------------------------------------
|
#
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.
|
#
1eadaac4 |
|
07-Jul-2004 |
Konrad Slind <konrad.slind@gmail.com> |
Upgrades to ML code generation. It now works for numerals, although the results of a computation will be incomprehensible usually. Writing a prettyprinter needs to be done.
|
#
af6ef7a9 |
|
10-Nov-2003 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Handle exponentiation in the "real reduction" functionality. Done through one big rewrite theorem (pow_rat) proved in realScript.sml.
|
#
16e384f8 |
|
01-Jul-2003 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Put this back the way it was.
|
#
f72b1d87 |
|
01-Jul-2003 |
Konrad Slind <konrad.slind@gmail.com> |
Hmm. Not sure what this is.
|
#
70bd7c6a |
|
30-Jun-2003 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
First cut at calculation with the reals. Doesn't include a treatment of exponentiation, nor does it eliminate divisors in fractions. Updates stateful rewriter and global compset, so that EVAL will do calculations with fractions. Am about to go home with build just in the middle of probability. If I've broken anything, apologies! Fix the bug by commenting out ++ REAL_REDUCE_ss in the definition of real_ss in realSimps.sml
|
#
e18ade2d |
|
27-Jun-2003 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Little more progress with this stuff.
|
#
72d00f8b |
|
26-Jun-2003 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Moving towards calculation with the reals.
|
#
aea4b061 |
|
21-Apr-2003 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Added a lot of rewrite exports. Am tempted to add versions of store_thm and save_thm to BasicProvers that do this exporting automatically. I could call them "Store_thm" and "Save_thm", say. Please write if you think this is a revolting idea. I'm not entirely convinced myself.
|
#
049a18d0 |
|
31-Mar-2003 |
Joe Hurd <joe@gilith.com> |
A few extra theorems to help with calculating with rational numbers.
|
#
1706b989 |
|
14-Jan-2003 |
Joe Hurd <joe@gilith.com> |
Some more useful theorems about sup and inf.
|
#
e4f6ae1d |
|
15-Dec-2002 |
Joe Hurd <joe@gilith.com> |
A really useful theorem about supremums: for any 0 < e, you can always gets within e of the supremum.
|
#
d852736d |
|
05-Dec-2002 |
Joe Hurd <joe@gilith.com> |
More theorems, this time about sup and inf.
|
#
7785b417 |
|
05-Dec-2002 |
Joe Hurd <joe@gilith.com> |
More useful theorems about reals and real-valued sequences.
|
#
dce55f69 |
|
03-Dec-2002 |
Joe Hurd <joe@gilith.com> |
More real simplifications, and more theorems about pos, max and min.
|
#
495a35f0 |
|
02-Dec-2002 |
Joe Hurd <joe@gilith.com> |
As predicted, I need a few more simplifying rewrites.
|
#
432f2556 |
|
01-Dec-2002 |
Joe Hurd <joe@gilith.com> |
Finally got around to fleshing out the real simpset (the other changes are the ramifications of this!) Major changes: 1. Got rid of AC rewrites for + and *. If you want them (perhaps for compatibility with the old real_ss), use real_ac_ss. 2. Added a huge bunch of useful rewrites to real_ss, though I'm sure I'll need to add a huge bunch more before I'm finished with it.
|
#
df700013 |
|
28-Feb-2002 |
Konrad Slind <konrad.slind@gmail.com> |
Some additions from HOL Light, in order to have proper basis for the irrationality of root 2 proof.
|
#
18c87632 |
|
14-Dec-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Added new facilities for dropping or preferring certain numeric types all at once. Documented one of the new functions, and fixed the documentation for add_numeral_form, which now automatically adds the appropriate overloading for "&" (I realised that we didn't need to force the user to do this themselves).
|
#
33f0914b |
|
14-Dec-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Changed the way overloading handles numerals slightly so that &x will now always be resolved as a function away from :num. (Whether it be from :int or :real.) The drawback is that people need to explicitly overload & if they develop a new numeric type.
|
#
805fdd4e |
|
13-Sep-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Removed gratuitous incompatibility with Taupo-6 in type of set_fixity; its type is now string -> fixity -> unit, rather than (string * fixity) -> unit.
|
#
de343a0a |
|
18-Jun-2001 |
Konrad Slind <konrad.slind@gmail.com> |
Changing arithLib to numLib. And RealSS to realSimps.
|
#
6cf562f4 |
|
28-Nov-2000 |
Konrad Slind <konrad.slind@gmail.com> |
The reals library builds on Kan.0.
|
#
9f67e582 |
|
10-Jul-2000 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
The function allow_for_overloading_on has been completely removed from the system. The overload code now uses anti-unification of types to figure out the least generalisation of all the types that an overloaded operator needs to represent.
|
#
cbd30609 |
|
12-Dec-1999 |
Konrad Slind <konrad.slind@gmail.com> |
Minor changes.
|
#
cb114e51 |
|
11-Dec-1999 |
Konrad Slind <konrad.slind@gmail.com> |
In polyScript, the polynomial operators have been overloaded. We are not sure whether this is a good idea or not.
|
#
2ab3f6db |
|
10-Dec-1999 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Changes due to the incorporation of John Harrison's datatype definition package. Many of these due to the fact that `n:num + b` parses differently because sumTheory is now in the ancestry. A couple of other changes due to explicit references one or two proofs made to num_Axiom. These are now to num_Axiom_old.
|
#
c64241de |
|
01-Dec-1999 |
Konrad Slind <konrad.slind@gmail.com> |
Minor changes to use "jrhUtils" instead of "useful".
|
#
0c538d42 |
|
11-Oct-1999 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Removed a stray right parenthesis that the old parser hadn't been catching as an error.
|
#
9b4cee77 |
|
22-Sep-1999 |
Konrad Slind <konrad.slind@gmail.com> |
Upgraded to use overloading.
|
#
0058df84 |
|
28-Jun-1999 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fixed to bring it up to date with Taupo release 0. (Changes have come across from parse_branch development.)
|
#
58841e67 |
|
29-Apr-1999 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Initial revision
|