#
e2db1817 |
|
21-Apr-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Make selftest output line up with parallel Holmake's Also make tests use testutils.OK to report OK
|
#
8c47c9df |
|
15-Jul-2015 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Detect and abort on vacuous inductive relation clauses A vacuous clause is something like !x y. R x y where R is the relation being defined. Such a thing makes the relation the universal relation. If you really want such a thing, you can always write !x y. T ==> R x y Closes #269
|
#
7d7c7fed |
|
15-Jul-2015 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Prevent bad constant names at Definition level Enforces a constraint I'd long assumed to be true. Closes #268
|
#
0a263dd6 |
|
05-Nov-2012 |
Ramana Kumar <ramana.kumar@gmail.com> |
add MONO_COND to bool_monoset (and hence the_monoset) This enables inductive definitions that make recursive calls in the branches of conditionals expressed with COND (if_then_else). Also added a selftest.
|
#
1ea88f67 |
|
19-Jul-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Move IndDef earlier in the build sequence (just before BasicProof). This will let me reinstate my new Induct_on functionality.
|
#
1f982641 |
|
19-Jun-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Make IndDefLib lose its unnecessary dependency on arithmeticTheory. Its selftest then needs to fake an arithmetic theory in order to get some of its test-cases to look similar to what they used to be.
|
#
63bbfe51 |
|
07-Jun-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Delete a misplaced comment.
|
#
b770bc48 |
|
07-Jun-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Bug fix, with test-case and release notes write-up.
|
#
7cd07edc |
|
04-Dec-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove some unnecessary fluff from the selftest script, and also make it executable in an interactive session without it causing the session to exit on hitting an error.
|
#
47b71c9d |
|
04-Dec-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
A new bug - strong induction derivation doesn't work for definitions with only a single rule.
|
#
b8aea703 |
|
19-Nov-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
IndDefLib fails this example because a term arises of the form UNCURRY f x y, which does not match the conclusion of the UNCURRY monotonicity rule. As the range of UNCURRY is polymorphic (rather than bool), it's impossible to tell how many arguments UNCURRY will be applied to before the resulting term is boolean. This suggests that the implementation of monotonicity proving needs to change to special-case UNCURRY, just as lambda is special-cased.
|
#
ccc5f621 |
|
19-Sep-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Check behaviour more consistently and more thoroughly.
|
#
fe358cf0 |
|
19-Sep-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
A new bug, reported by Peter, where the Inductive definitions package fails to do its stuff.
|
#
b458dfe5 |
|
12-Sep-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Change to the inductive relations definition code to support a global, and updated "monoset", which can be updated as theories load, thereby invisibly increasing the capabilities of Hol_reln. Also simplify the implementation of derive_strong_induction, and move the entrypoint to IndDefLib. New test in src/IndDef/selftest.sml wouldn't have passed before (I believe). It is more onerous than Peter's original monoset example, which didn't feature recursion under the EVERY operator. Documented in Description and release notes. Still to update theories with appropriate calls to export_mono. (export_mono and export_rewrites are now part of bossLib's interface.)
|
#
4a2594f4 |
|
11-Sep-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix output of selftest slightly; adjust its dependencies in Holmakefile.
|
#
eed9233f |
|
11-Sep-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
This example causes grief to a new way of implementing back-chaining that I am investigating.
|
#
c4575b55 |
|
09-Sep-2006 |
Peter Homeier <palantir@trustworthytools.com> |
---------------------------------------------------------------------- Committing in fix so that a fresh build of HOL4 works. A recent addition caused a build to break since lists, etc. were not built before this library. Modified Files: selftest.sml ----------------------------------------------------------------------
|
#
f713d85e |
|
08-Sep-2006 |
Peter Homeier <palantir@trustworthytools.com> |
---------------------------------------------------------------------- Committing in slight tuneups to rule inductive definitions. Modified Files: IndDefRules.sml selftest.sml ----------------------------------------------------------------------
|
#
9d05ef44 |
|
08-Sep-2006 |
Peter Homeier <palantir@trustworthytools.com> |
---------------------------------------------------------------------- Committing in revisions to rule induction library, supporting the proof of strong induction theorems for rules that involve new monotonic operators. There is now a new function, prim_derive_strong_induction, available in IndDefLib. Modified Files: IndDefLib.sig IndDefLib.sml IndDefRules.sig IndDefRules.sml selftest.sml ----------------------------------------------------------------------
|
#
fe73bb13 |
|
22-Aug-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Add a test case that one might argue we should support. Currently, the Hol_reln call is fine, but the call to derive_strong_induction fails.
|
#
a865157b |
|
22-Aug-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Regression testing for inductive definitions.
|