Add function Defn.Hol_multi_defns.

This involves moving some code from TotalDefn to Defn.

Remove tfl/src/Functional.{sig,sml}; redirect to src/1/Pmatch instead.

This preliminary check-in doesn’t bring across all of the differences
between Functional and Pmatch. On the assumption that the differences
are important, I’ll patch Pmatch as necessary on this branch before
merging back into master.

Intention is to have this done before proceeding with work on
features/case-const-argflip. Given that, this is progress of a sort
with Github issue #97.

Remove trailing whitespace in source files.

Add hooks in Defn to support termination proofs in other Script files.

The new tgoal_no_def and tprove_no_ind functions take the (terminiation
condition constrained) equation and induction theorems as stored in a theory by
Defn.save_defn and start a termination proof. This seems to work because the
existing tgoal and tprove functions do not look at then Defn.defn object other
than to get the equation and induction theorems.

This allows me to write a Hol_defn and save_defn in one Script file and carry
out the termination proof in a different Script file. It might be better to add
the defn object itself to the Theory file, but there doesn't appear to be any
immediate practical benefit (the defn object seems to be undocumented).

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!

Added support for making multiple definitions
in one invocation.

Added proofManagerLib. This adds a type of "goal trees"
as an alternative to goalstacks. Relevant entrypoints:

gt ` .... ` -- start a goaltree proof,
analogous to g
eq ` ... ` -- expand a tactic,
analogous to e (except that
the text of the tactic is
delimited by quotes).

A goaltree manages the construction of the final
tactic, so should ease some of the script maintenance
that the goalstack requires.

Backup and restart are just as for goalstacks.

All the entrypoints for goalstacks are just as they
were before; there shouldn't be any difference.

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.

Support for tDefine.

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.

Moved TotalDefn to num/termination.
Also, fixed up "dec-suc-ification" used in Defn.sml, to use a hook.

Make Hol_defn and friends report location of the definition at fault.
Sorry, can't be more precise at the moment.

Defn.sig needs to change to reflect changed type of tstore_defn.

Minor mods to persistence of things introduced via TFL. In particular,
tstore_defn doesn't call add_funs twice.

Made Define store its resulting equations in the compset in a persistent
manner.

Change stemming from split of TypeBase into TypeBasePure and TypeBase.

Changes to improve interface for nested definitions.

Modifications caused by change of TypeBase signature.

Minor changes.

Defn.tgoal is changed to deliver a goal of the form

?R . TC_1(R) /\ ... /\ TC_k(R) /\ WF R

When the proof is finished, the finalizer in the goalstack will
not return this theorem, but the specified recursion eqns. and
induction theorem.

Things are starting to stabilize. The main change from the last
update is that defns can be saved (in a sense). In the next revision,
defns will be written into a persistent DefnBase.

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.

Big re-organizational changes. Tfl and tflLib are gone ... the relevant
files are instead Defn and TotalDefn.

Re-organization, hopefully to make things clearer.

1. Added a termination interface to Defn. This takes a defn and attaches a
new goalstack to the list of current proofs. There is also an analogue
that wraps up a defn and a tactic and applies the tactic to the
termination constraints of the definition. If the tactic proves the
goal, then the unconstrained recursion equations and induction theorem
are returned.


tgoal : defn -> proofs
tprove : defn * tactic -> thm * thm

In tprove, some cleverness is used to arrange that the ultimate goal
(namely the unconstrained recursion equations and induction theorem) is
not what is initially seen by the user; instead the first goal appears
to be something of the form

?R. TC_1 /\ ... /\ TC_n /\ WF R

Proving this will deliver the top_thm()

|- rec. eqns /\ ind. thm

One problem with this sleight of hand is its behaviour with respect to
"restart" -- restarting takes us to the ultimate goal. To regain the
original state, Defn.TC_TAC <defn> may be used.

2. Halts.TC_SIMP_CONV uses a standard set of theorems about WF to simplify
goals ensuing from giving the witness for R above. Typically, one would
work by going

val foo_defn = Hol_fun "foo" <eqns for foo> ;

Defn.tgoal foo_defn;
e (EXISTS_TAC <some termination relation>);
e (CONV_TAC Halts.TC_SIMP_CONV);

New features in Defn and Halts.

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.