Remove TABs from src

Will also make selftest to check that they aren't introduced

Fix normalisation issue in numSimps.ARITH_ss

Rather than use a custom (and broken) term-comparison function, it
suffices to use Term.compare.

With regression test. Thanks to Brian Campbell for the report.

Closes #473

Add MOD_ss to srw_ss()

If it breaks proofs, this is easy to reverse in a script by doing

val _ = diminish_srw_ss ["MOD_ss"]

before the old behaviour is being relied upon

Move bitTheory into src/num/extra_theories and move evaluations theorems in wordsLib further up the build sequence.

Includes some tidying-up work.

This closes issue #120. Evaluation for "toNum" and "toString" can now be enabled by loading up stringLib (or, more precisely, ASCIInumbersLib), without the need to load up wordsLib.

This check-in can be viewed as finishing off the (many) loose ends left over from work on issue #70.

REDUCE_ss no longer loops on, e.g., 0 DIV 0. Corresponding self-test added.

Use relsimps in fragments functionality to define a MOD_ss.

This is capable (as per the provided selftest) of simplifying

(6 * x + 7 + 10 * y) MOD 6 to (1 + 4 * y) MOD 6

and

(4 + 3 * n + 1) MOD n to 5 MOD n

(when 0 < n is in the context).

It will also remove superfluous (nested) repetitions of "MOD-n"
applications.

Get ARITH_ss to avoid doing some unnecessary work.

In particular, there is no point in ever getting it to attempt a
goal whose conclusion is of the form p /\ q. This is because it
will have already attempted p and q independently, and doing them
together can't make the goal any more solvable. One wrinkle though:
the simpset tries to prove them equal to true, and to false. So,
if the term to be simplified is p /\ q, it's still worth trying to
prove this is false.

Move ARITH_NORM_ss to numSimps.

Rework the handling of bounded rewrites to fix bug in previous check-in.

Unfortunately, the type of the filter field of a ssfrag has to change;
I'll adjust our documentation shortly.

ARITH_DP_FILTER_ss added. This simpset-fragment is similar to ARITH_DP_ss. It contains the arithmetic decision procedure. However, I get's an additional filter function as an argument that filters the context theorems given to the decision procedure. This can be used to avoid the DP becomming very slow thanks to too much input.

Adding an ssfrag to a simpset now adds frag rwts to set's dprocs as context.

This has a few knock-on effects, mainly on use of ARITH_ss, which had
hitherto only been getting context from goal assumptions and theorems
passed to the simp-tactics at the top-level. The ARITH_ss addctxt
function needs to be a bit fussier in order to avoid picking up
unusable junk.

The intention with the change is to get exported rewrites for
relations other than equality to work, as per the change to
churchboolScript (this should be the first of many). One change this
then required in add_relsimps was to have it check for looping
rewrites (particularly: if reflexivity of the relation is added as a
normal equality rewrite, which is reasonable, this can't be allowed to
put the relation-rewriter into a loop).

Removed trailing whitespace from all .sml and .sig files.

This affects over 900 files and was done using emacs's delete-trailing-whitespace
function in batch mode. Building the system with Poly/ML and Moscow ML seems to
work, so I'm hoping these changes don't break anything. Please complain if
they do!

Add some rewrites that should take care of annoying terms like
b <= a * b
and variations on this theme. They are part of std_ss and srw_ss().

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.

Overhaul of automated termination prover. It now does a better job
of guessing termination relations, using a relevance criterion
to cut down the number of lexicographic combinations that are tried.
It can handle DIV and MOD now, through the "termination_simps"
variable, which can be added to in order to support other
destructor functions.

Also added DIV_LESS and MOD_LESS to arith_ss. This breaks some proofs,
and I've fixed the broken ones in the standard system build. But there
may still be proofs among the examples directories that will now fail.
If there's a problem with this, I will happily revert.

Add reduction of DIV2 and MOD_2EXP to num compset and standard simpsets.

The condition that assume-able arithmetic formulas not have hypotheses
didn't seem to play any useful role, except possibly to stop the arith
tool trying to work with universally quantified theorems that might appear
in theorem lists passed to the simplifier. But such theorems would be
eliminated by the check for positive universals anyway. Finally, the
check eliminated perfectly reasonable behaviours, as illustrated by the
new case in the selftest.

Add more aggressive simplification of terms involving EXP (natural number
exponentiation). This affects the behaviour both of std_ss and srw_ss().
Various proofs break, so I've fixed these.

Slight re-organisation of the {ADD{L,R},MUL}_CANON_CONV sources, and addition
of new code (with functor no less) to do normalisation over relational
operators. Three instances provided. The next stage will be to put
sum_{leq,lt,eq}_norm into arith_ss, thereby breaking a whole bunch more
proofs no doubt.
For the moment, the code is there but not called, so nothing should
change as a result of this check-in.

New generic code to normalise arithmetic expressions. Will handle
integers and reals too, but this check-in just slots the new code
into ARITH_ss. (The broken proofs in integerScript make me wonder
how they ever worked. As they fiddle about with dangerous BIT1, BIT2 and
NUMERAL constants, I'm not too bothered by their failure).

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.

Add divisibility rewrite to standard arithmetic rewrites.

Add some more "obvious" rewrites to the arith rewrites simpset.
Next step is to move this into std_ss.

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.

Follow-on fixes to changing Term to Parse.Term and Type to Parse.Type
in the quotation pre-processor. A mass of trivial changes, but the
new way of dealing with files containing code that does parsing
(not script files) is to

* grab the ambient grammar(s)
* set the current grammar(s) to the right values
for parsing quotations in the file
* the body of the file
* reset the current grammar to the ambient grammar

For an example, see src/taut/tautLib.sml

Reorganization of numSimps.sml (it was a bit of a jumble). Also,
added MIN and MAX syntax functions.

My last check-in broke the building of the n-bit word theories (should
always try the -selftest option to build to catch this) because the
implementation of relevance analysis didn't believe that SUC a <= 2 ** WL
was relevant to proving 0 < 2 ** WL. The solution is to realise that
even ground terms may end up being treated as variables by decision
procedures. So, there is now an additional parameter to RCACHE : a function
that takes a term and returns a list of terms that should be treated
as free variables in the relevance analysis.

A better cache function, RCACHE that does relevance analysis to speed
up the rejection of formulas that are sure to fail.

Fix for the bug
- SIMP_CONV arith_ss [] ``x + x + x``;
> val it = |- x + x + x = x + 2 * x
reported yesterday. Nothing seems to break.

Alter the way BOUNDED/UNBOUNDED rewriting works, so that the BOUNDED
tag is now a theorem hypothesis of a special form, and so there is no
UNBOUNDED tag at all (i.e., the default is to be unbounded). This is
simpler, and means that if you come to write a simplifier filter (as
in the case of SUC_FILTER_ss) you don't need to worry about whether
or not the rewrite is bounded. (Will add this check-in message to
changed files in src/simp/src that got mistakenly tagged with my change
to selftest there.)

More bad equalities. Mike's suggested we have an infix symbol for aconv,
maybe :=:
Any other ideas?

More bad equalities.

Added DIVMOD to arithmeticScript, which helps complete the suite
of generated code. Unfortunately, arithmetic then depends on pairs,
which I had been trying to avoid, for purely aesthetic reasons.

Also fixed up more of the ML code generation business.

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.

Add a couple of equalities that should be pretty useful, and also
put them into the appropriate simpset.

Sorry! I've realised that there's a better way of doing what I want
within the netsem code-base, and that I don't need to make any changes
to the way HOL currently does things. More, that letting HOL stay
just the way it was is probably better. So, this change is to put the
code I meddled with over the last couple of days back the way it was
originally. (Minor exceptions include changes to comments, elimination
of unnecessary infix declarations, and revealing a PAIR0_ss that is
equal to PAIR_ss minus LET_ss.)

A new approach to handling LETs for the stateful rewriter. Introduces an
incompatibility in that bool_ss no longer rewrites LET f x to f x (std_ss
still does though). The new strategy is:

Don't put LET_THM into any of the simpsets, but rather
put in specialised versions of this that allow "values" to be
substituted into the body. Thus ``let v = e1 in e2`` will only reduce
to e2[e1/v] when e1 has been reduced to a proper value. Better,
allow partial substitution to happen when e1 has become partially
value-like. For example, if we get to

let v = SUC e in v + v

and e isn't necessarily evaluated, we can still move this to

let v = e in SUC v + SUC v

The rewrite for this is |- LET f (SUC e) = LET (\v. f (SUC v)) e
Comparable rewrites for constructors of any type are easy to state
and prove. Arguably, these theorems should be generated when new
types are defined, and stored in the TypeBase. Because I know Konrad
will be (is already?) messing with the TypeBase to support ML lifting,
I haven't done this for Hol_datatype (it's not quite so easy to see
how to capture the notion of "record value").

I have written the appropriate theorems for the obivous built-in
types. This strategy gives the simplifier a notion of "value" that
is different from "can't reduce any more by the given rewrites"
(which is what CBV_CONV uses). The problem with CBV_CONV, or a
congruence rule that always performs the reduction from LET f e to
f e is that you can get big explosions in term size, which is
particularly bad if you are doing symbolic evaluation.

Have fixed problems arising in probability (which was using its own
version of std_ss, and those places where srw_ss() is being used. The
examples/lambda directory uses SRW_TAC pretty extensively, so there are
fixes required there. The easiest way is to just put LET_THM back into
the stateful simpset and to forget about it. The general problem with
the stateful system as it stands is that it is very easy to put things
into it, but impossible to pull them out. Isabelle has some way of
doing this that might be worth looking into.

Joe noticed that SUC_FILTER_ss wasn't working properly anymore. This was
because rewrite theorems were now being wrapped in BOUNDED/UNBOUNDED tags
by the action of the filter in pure_ss. I updated SUC_FILTER_ss, and added
a selftest to demonstrate the fix.

A new theorem about DIV, some theorems given alternative names, and a
re-statement of MULT_LESS_EQ_SUC that I think is about a zillion times
more useful. Also thrown some of these into the standard numeric
simplification set.

Added some useful arithmetic rewrites to do with the order relations.

A new theorem about MOD, and moving the obvious theorems about MOD and
DIV into numSimps.

Added an AC simpset for addition and multiplication. Occasionally useful.

Added some obvious rewrites to the set, and slightly reorganised their
presentation.

REDUCE_ss should deal with terms of the form {MIN,MAX} n1 n2 (where n1
and n2 are both numerals).

Some code to help with problems brought on by the change to REDUCE_ss.
The new SUC_FILTER_ss simpset fragment can be used to make rewrites
involving SUC into ones that match on any term and have the same semantics
(by using conditions on the rewrite). Unfortunately, just merging
SUC_FILTER_ss into ARITH_ss caused a number of broken proofs.
An example of the sort of things that can go wrong is the following
goal:

.... n EXP (SUC m) ....
-----------------------------
0. p < m

If you rewrite with ASM_SIMP_TAC (arith_ss ++ SUC_FILTER_ss) [EXP]
you get a new goal of

.... n * n * n EXP (PRE m) ....
-----------------------------------
0. p < m

Urk! For the moment, SUC_FILTER_ss will need to be "invoked" by hand.

Modified REDUCE_ss (used in std_ss, and in a lot of other places too) to
reduce terms of the form SUC (SUC (SUC ... n)..)) where n is a numeral.
This breaks a few proofs, but not a huge number. It seems silly to have
REDUCE_CONV do one thing (reduce ground SUC terms) but not REDUCE_ss.

Cause standard simpset fragments to be automatically added to the
stateful rewriter as the relevant theories are loaded, rather than
waiting for bossLib to come and along and do it after the fact.
Strictly speaking, in the case of numSimps and pairSimps it is still
necessary to load these two rather than just the base theories. This
is because the simpset fragments in these cases are more than just
rewrites but include 'real code' (REDUCE_CONV and GEN_BETA_CONV
respectively). Still, rather this than having to load bossLib.

Fix for bug #585828.

More tracing for those moments when arith_ss seems to have gone into an
infinite loop. (It's more likely to have barfed on too many subtractions.)

Enabled reduction of `PRE num` terms.

Changing arithLib to numLib.