Removed Lib.gather. Use {Lib,List}.filter instead.

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!

Fix to bug spotted by Anthony, whereby the induction
theorem for functions defined by pattern-matching
on literals was failing to be proved. Misc.
simplifications to TFL code plus adding "trypluck" to Lib.

Fixed a subtle bug in termination condition extraction,
whereby multiple let-bindings for a variable would
cause Define to be unpredictable and sometimes broken.
Now variables get renamed in order to make the definition
process succeed. So the definition

Define `field_exp_aux (r5:word32,r6:word32,r7:word32,r10) =
if r6 = 0w then (r7,r10) else
if r6 && 1w = 0w then
let r6 = r6 >>> 1 in
let r2 = r5 in
let r3 = r5 in
let (r4,r10) = field_mult (r2,r3,r10) in
let r5 = r4 in
field_exp_aux (r5:word32,r6:word32,r7:word32,r10)
else
let r6 = r6 >>> 1 in
let r2 = r7 in
let r3 = r5 in
let (r4,r10) = field_mult (r2,r3,r10) in
let r7 = r4 in
let r2 = r5 in
let r3 = r5 in
let (r4,r10) = field_mult (r2,r3,r10) in
let r5 = r4 in
field_exp_aux (r5:word32,r6:word32,r7:word32,r10)`;

will, in the second recursive call, rename r7,r2,r3,r4,r5,r6,
and r10 (twice):

|- field_exp_aux (r5,r6,r7,r10) =
(if r6 = 0w then
(r7,r10)
else
(if r6 && 1w = 0w then
(let r6' = r6 >>> 1 in
let r2 = r5 in
let r3 = r5 in
let (r4,r10') = field_mult (r2,r3,r10) in
let r5' = r4 in
field_exp_aux (r5',r6',r7,r10'))
else
(let r6' = r6 >>> 1 in
let r2 = r7 in
let r3 = r5 in
let (r4,r10') = field_mult (r2,r3,r10) in
let r7' = r4 in
let r2' = r5 in
let r3' = r5 in
let (r4',r10'') = field_mult (r2',r3',r10') in
let r5' = r4' in
field_exp_aux (r5',r6',r7',r10'')))) : thm

Thanks to Magnus for bringing this to my attention.

Fix to bug in production of induction theorem for nested recursions.

Drop obviously-looping rewrites. Causes a problem in fn definition
that Tom Ridge was trying to make.

First version of function definition with constant patterns.
Basic definitions seem to work, but the induction theorems
can be simplified.

- Defn.const_eq_ref := reduceLib.NEQ_CONV;;

Here's the definition of Fibonacci:

- Define
`(f 0 = 1) /\
(f 1 = 1) /\
(f n = f (n-1) + f (n-2))`;

This yields the definition

> |- (f 0 = 1) /\
(f 1 = 1) /\
(f v = case v of 0 -> 1 || 1 -> 1 || v -> f (v - 1) + f (v - 2)) : thm

which may or may not suit your idea of what should be returned.
It could return a conditional theorem for the last clause of
the definition, but then EVAL would probably not know how
to evaluate it.

The induction theorem is mostly in the right format, although
I wonder if it could be made nicer ..

- val ind = REWRITE_RULE [] (fetch "-" "f_ind");;
> val ind =
|- !P.
P 0 /\ P 1 /\
(!v.
(~(v = 0) /\ ~(v = 1) ==> P (v - 1)) /\
(~(v = 0) /\ ~(v = 1) ==> P (v - 2)) ==> P v)
==>
!v. P v : thm

Here's a more complicated definition (others solicited), which
shows that better post-definition simplification is definitely
needed. But that should be pretty easy to add now that the basics
are working.

Define
`(h (0,0) = T) /\
(h (0,1) = F) /\
(h (1,0) = F) /\
(h (1,1) = T) /\
(h (u,v) = h (u-1, v-1))`;

<<HOL message: mk_functional:
pattern completion has added 2 clauses to the original specification.>>
Equations stored under "h_def".
Induction stored under "h_ind".
> val it =
|- (h (0,0) = case 0 of 0 -> T || 1 -> F || v7 -> h (0 - 1,v7 - 1)) /\
(h (0,1) = case 1 of 0 -> T || 1 -> F || v7 -> h (0 - 1,v7 - 1)) /\
(h (1,0) = case 0 of 0 -> F || 1 -> T || v11 -> h (1 - 1,v11 - 1)) /\
(h (1,1) = case 1 of 0 -> F || 1 -> T || v11 -> h (1 - 1,v11 - 1)) /\
(h (v3,v) =
case v3 of
0 -> (case v of 0 -> T || 1 -> F || v7 -> h (0 - 1,v7 - 1))
|| 1 -> (case v of 0 -> F || 1 -> T || v11 -> h (1 - 1,v11 - 1))
|| v3 -> h (v3 - 1,v - 1)) /\
(h (1,v11) =
case v11 of 0 -> F || 1 -> T || v11' -> h (1 - 1,v11' - 1)) /\
(h (0,v7) = case v7 of 0 -> T || 1 -> F || v7' -> h (0 - 1,v7' - 1))
: thm

Define now handles simple definitions defined by
pattern-matching against (numeric) constants, e.g.

Define `(f 0 = 1) /\ (f 1 = 1) /\ (f n = f (n-1) + f (n-2)`;

But more testing/robustification needs to be done.

Bugfix for an example of Michael (plus other preliminary fixes aimed at
other bugs.

The bug was

Hol_datatype `goo = Ctr of bool # bool # bool`;
Define `f(Ctr(x,_,_)) = x`;

Minor changes, most having to do with Boultonization.

noCVS: Committing in .

Upgraded tflLib to Kan.0.

Kananaskis compatibility.

Fixed some bugs coming from Kim Sunesen.

Ongoing revisions. Defn has been split into a basic datastructure
and manipulations (Defn0) and the definition entrypoints (Defn).
This allows a prettyprinter for the "defn" type to be automatically
installed when the std.prelude runs. Defn0 is part of basicHol90.

Start of a re-organization of the TFL library. The idea is to get rid
of the generality stemming from making it work for both Hol and Isabelle.
Maybe this is a step backwards, but I got sick of all the cruft.

Fixing bugs in definitions. The change to RW.sml means quantification
differences in antecedents of congruence rules are now accomodated.
The change to Tfl.sml means that mutual recursions can now be given
such that some clauses can be filled in by pattern matching.

Major changes to accomodate TFL advances. Now mutual, nested, and
schematic recursions can be given. Termination relations can be
deferred for these (in fact, deferred definitions are the only
way of making such definitions currently).

WFScript.sml has been eliminated and its components have been
dispersed to the appropriate theories (pairTheory, prim_recTheory,
and listTheory).

Defn provides a high-level interface to deferred definitions.
Defn relies on very little background support, so it can be
used when one does not need (or desire) the full weight of
bossLib.

Halts has been moved from bossLib.

tflLib may soon go away, since its functionality should in the
longer run be subsumed by Defn + Halts.

Initial revision