Fix λ-calculus examples in light of pat_assum rename

Documentation reflecting preference for Datatype over Hol_datatype.

Some code changes as well, most importantly in TUTORIAL's
examples/ind_def/clScript.sml.

New goalstack pretty-printing trace & rationalise goalstack trace names

New trace prints a count of the sub-goals at the end of the stack.
This saves the user from having to scroll back over the several
hundred goals they've just generated to find out the number.

Rename a variable away from now-used-as-constant 'PI'.

Adopt ML-style syntax for case expressions and use freed up "||" for bitwise-or. See issue #24.

WIP: perm_type wasn't building; now it's closer to building.

I probably mangled my attempt to extract the 'good stuff' from the old
nominal_datatype branch. I have cleaned things up slightly by hiding
the 'raw' lswapstr constant. Now the string "lswapstr" maps to a term
that is a permutation action, making all the permutation rewrites
apply for lswapstr automatically.

Extract a usable half-way point from nominal_datatype branch.

This replaces the is_perm predicate with a type embodying that predicate.
It doesn't include the subsequent work on allowing multiple 'atom' types.

Terms and labelled terms now derived from generic terms.

This is a big change that points to the implementation of a complete
nominal datatype package. The use of generic terms means that we only
need to do one hairy quotient, and one hairy derivation of a recursion
principle.

The recursion principle in question features a new "FCB" (one of the
side-conditions that need to be proved in order to get a recursive
function admitted). Though I think it's better, it can be a little
fiddlier to prove. It's also stronger, so in theory, there may be
reasonable functions that the new FCB rejects. It should certainly be
possible to automate the bulk of the new fiddly proofs.

Slight strengthening of generic term recursion principle.

Derive a parameter-free version of the generic recursion principle.

I can't figure out how to properly lift the parameterised version, and I can re-derive it from a
normal recursion principle, so for the moment, it does rather look as if the work to
derive the parameterised principle for generic terms was unnecessary.

Being able to the do the re-derivation is a step forward though, so that's a little
consolation.

use sidecond_tac more in generic_termsScript

Slightly strengthen the FCB in generic terms' recursion principle.

Recursion axiom with parameters for generic (nominal) terms

Squashed commit of the following:

commit e1391ec39161f689623666ca9048556ff6bfdd27
Merge: c0d1a80 9767cb0
Author: Ramana Kumar <ramana.kumar@gmail.com>
Date: Fri Jul 8 12:15:03 2011 +0100

Merge branch 'master' into nominal_datatype

commit c0d1a8003b7b3c2a5f96bcc5ccb0aea7a456bc16
Author: Michael Norrish <Michael.Norrish@nicta.com.au>
Date: Fri Jul 8 19:30:15 2011 +1000

Complete all proofs in generic_termsTheory.

commit 1011a430c1969c9c15a80a0a161cff153c429990
Author: Michael Norrish <Michael.Norrish@nicta.com.au>
Date: Fri Jul 8 17:44:09 2011 +1000

eqv property proved.

commit 7c319bc2715b4e8115dbaf70271c8de14084d550
Author: Michael Norrish <Michael.Norrish@nicta.com.au>
Date: Thu Jul 7 16:56:04 2011 +1000

Some more proof hacking - introduce relsupp constant.

commit 6e0e2fcc04f15858e9758485cc5cb281aa7bde5a
Author: Michael Norrish <Michael.Norrish@nicta.com.au>
Date: Thu Jul 7 14:54:45 2011 +1000

Add suggested lemmas/rewrite rules early on in proof.

See COMPLETE THIS comment.

commit c4d6fa0ac61ff776bd91f81c979a9014386121b5
Author: Ramana Kumar <ramana.kumar@gmail.com>
Date: Wed Jul 6 22:10:27 2011 +0100

more proof attempt

commit 30bc99bc410af3416e98ff6a94a4909aabff0021
Author: Ramana Kumar <ramana.kumar@gmail.com>
Date: Wed Jul 6 13:43:49 2011 +0100

finish a side case that was put off earlier

(and more attempts at the difficult case)

commit d43ab6cc89876f12e0d90d557b433389170eaf7c
Author: Ramana Kumar <ramana.kumar@gmail.com>
Date: Mon Jul 4 22:06:17 2011 +0100

a bit more

commit c2c254869a39d81b086a63b8185459345ccb05b3
Author: Ramana Kumar <ramana.kumar@gmail.com>
Date: Mon Jul 4 16:36:13 2011 +0100

more proof attempt

commit da7919e0af20fd8496619a1e47a2f2ed2ba21f13
Author: Ramana Kumar <ramana.kumar@gmail.com>
Date: Mon Jul 4 09:55:29 2011 +0100

attempting to do more cases of tmrec_equivariant at once

commit 82b8619f85102f96c969c22953a0fbc676263557
Author: Ramana Kumar <ramana.kumar@gmail.com>
Date: Sun Jul 3 19:06:20 2011 +0100

try removing one of the ARB cases earlier...

commit 147cfff5f0ee5f8b154634f1c473f7b76daa1629
Author: Ramana Kumar <ramana.kumar@gmail.com>
Date: Sun Jul 3 15:03:13 2011 +0100

possible progress on tmrec_equivariant

commit 52a08746cee9a4834efcf1e4cf4d3a76466dc163
Author: Ramana Kumar <ramana.kumar@gmail.com>
Date: Sun Jul 3 13:30:24 2011 +0100

fix tmrec_equivariant proof attempt for recent patches

commit 1e4199d9fd7d040100a25554a4116b1514c917d9
Author: Michael Norrish <Michael.Norrish@nicta.com.au>
Date: Sun Jul 3 20:53:28 2011 +1000

All of generic terms now works with GFV done away with.

Signed-off-by: Ramana Kumar <ramana.kumar@gmail.com>

commit c905c71885f8d1b9849f2d779ba1609c071d978f
Author: Michael Norrish <Michael.Norrish@nicta.com.au>
Date: Sun Jul 3 20:16:51 2011 +1000

Move some generic listpm results from genericTerms to nomsetTheory.

Signed-off-by: Ramana Kumar <ramana.kumar@gmail.com>

commit 967fc0f76f43a9036116cbcaac399d7719588588
Author: Michael Norrish <Michael.Norrish@nicta.com.au>
Date: Sun Jul 3 15:28:20 2011 +1000

Do away with GFV as a separate constant soon after quotienting.

Signed-off-by: Ramana Kumar <ramana.kumar@gmail.com>

commit d088807f66be44aeaa2a8d493eaa0d51563ae583
Author: Michael Norrish <Michael.Norrish@nicta.com.au>
Date: Sat Jul 2 20:56:41 2011 +1000

Delete remnants of old generic terms stuff so the new theory builds.

Yes, there's still a mk_thm in there, but we can now parallelise work
on the mkterm code and getting the details of the recursion proof out.

Signed-off-by: Ramana Kumar <ramana.kumar@gmail.com>

commit fabd19ec1757ce71b521a30963067e73971147b0
Author: Ramana Kumar <ramana.kumar@gmail.com>
Date: Sun Jul 3 11:58:16 2011 +0100

finish a (deeply nested, easy) subgoal in tmrec_equivariant

commit 07be34c7908745500544711346168186605d6c14
Author: Ramana Kumar <ramana.kumar@gmail.com>
Date: Sun Jul 3 10:29:48 2011 +0100

bit of progress on tmrec_equivariant

commit fc22b9a2afc0d1b1bba932f4f365f2cffb60c31b
Author: Ramana Kumar <ramana.kumar@gmail.com>
Date: Sun Jul 3 00:23:13 2011 +0100

start an attempt with gtmsize induction

commit 28accbeecf8f5c17627d422facee7ea23a97bff8
Author: Ramana Kumar <ramana.kumar@gmail.com>
Date: Sat Jul 2 11:13:40 2011 +0100

clean statement of tmrec_equivariant and start using bvc_genind

commit 5d94e2cd1ecfef5856d28d61132ed8e020d028cd
Author: Ramana Kumar <ramana.kumar@gmail.com>
Date: Sat Jul 2 09:04:56 2011 +0100

finish proof of parameter_tm_recursion

an awful proof full of duplication, but it works...
generates a MK_THM tag because haven't proved tmrec_equivariant yet.

commit 144a6520ffd20dbdb50dd411b6d0f66c2716e02d
Author: Ramana Kumar <ramana.kumar@gmail.com>
Date: Sat Jul 2 08:11:31 2011 +0100

Michael's work on tmrec_equivariant

+ corresponding fixes to my stuff after

commit 27a3596e3c2f3f2fd5d741d5bb9d0bf6a15e99b2
Author: Ramana Kumar <ramana.kumar@gmail.com>
Date: Fri Jul 1 18:29:54 2011 +0100

reorganize proof attempt a little

commit 07b5739db009803fa79a248eb4da56e6148504d5
Author: Ramana Kumar <ramana.kumar@gmail.com>
Date: Fri Jul 1 13:03:38 2011 +0100

progress including possibly more correct definition of FCB

commit 147a503758d74dc26c309733b4af263ca3001ab5
Author: Ramana Kumar <ramana.kumar@gmail.com>
Date: Fri Jul 1 00:05:46 2011 +0100

possible progress

but seems like somethings may be wrong with assumptions about the terms
that don't contain the bound variable, and about the parameters...

commit 405cc0e5d49b9e199879c5ba6de8f8340d887083
Author: Ramana Kumar <ramana.kumar@gmail.com>
Date: Wed Jun 29 22:46:06 2011 +0100

make permsupp_sidecond and FCB defined constants

commit 4d3c44b84024ec77794d007373238841da5e392e
Author: Ramana Kumar <ramana.kumar@gmail.com>
Date: Wed Jun 29 12:48:18 2011 +0100

unsure work towards parameter_tm_recursion

commit d0180624b133c1330db7e3fcddcb00120af1b9c2
Author: Ramana Kumar <ramana.kumar@gmail.com>
Date: Wed Jun 29 11:49:05 2011 +0100

fix inconsistent argument ordering, and use LIST_REL more

commit 804ef91fb80f71a8e9b43cb3bfcfefd3e37086e9
Author: Ramana Kumar <ramana.kumar@gmail.com>
Date: Mon Jun 27 15:38:41 2011 +0100

attempt to state (and prove easy bits) of parameter_tm_recursion

commit a5ae6d223de9643af43a61404f9d992f758d076a
Author: Ramana Kumar <ramana.kumar@gmail.com>
Date: Mon Jun 27 12:54:58 2011 +0100

direct definition of tmrec

commit 194ed71243e13cec7ec090da22151593ae6f894b
Author: Ramana Kumar <ramana.kumar@gmail.com>
Date: Mon Jun 27 12:52:57 2011 +0100

define a size measure for generic terms

commit 879e1cfcda485e0f6c348222647b9ec58f3c12fa
Author: Ramana Kumar <ramana.kumar@gmail.com>
Date: Thu Jun 23 09:23:18 2011 +0100

remove EVERY_AND and conj1_assum from generic_termsScript

Rename TruePrefix to Prefix; use fixity options with NONE for what was Prefix.

90+% of this work was done by Ramana Kumar. The following list are
the commits for a series of individual commits that have been squished
into one big change:
* remove mention of TruePrefix from the add_rule docfile
* first batch of changes removing TruePrefix from src/parse
* replace TruePrefix by Prefix in boolScript.sml
* remove TruePrefix from Rsyntax
is a fixity ever required for new_specification?
* some more Prefix -> NONE and TruePrefix -> Prefix in theories
* TruePrefix changes for datatype
* TruePrefix changes for res_quan
* TruePrefix->Prefix in a TeX selftest
* TruePrefix changes for quotient
* TruePrefix changes for integer and real
* fix quotient examples for TruePrefix removal
* more fixes for quotient examples
* fixes for lambda example for TruePrefix removal
* Reword description manual in light of removal of TruePrefix.
* Fix msgTheory quotient example; Poly 5.3 had problems with monotypes.
* Fixes for files in examples/lambda given removal of TruePrefix.
* Fix in examples/unification given removal of TruePrefix.
* Fix in examples/HolCheck given removal of TruePrefix.
* Fixes in examples/acl2 given removal of TruePrefix.

Further slight weakening of the FCB side-condition.

Slightly weaken the FCB side-condition on the recursion axiom.

Strength generic terms' recursion axiom.

Provide an extra assumption when discharging the side condition.

Revise generic terms' recursion axiom to be wrt a subset of the type.

This will help when defining new types, which will all naturally be
constructed from a subset of the generic type.

Make overload for -p-> local to generic_termsScript.

Export induction from generic_terms; minor progress with mkTerm.

Start to demonstrate how generic terms can model normal lambda-terms.

genind principle more general to support mutually recursive types.

Remove the redundant GAPP constructor from the generic term type.

Start of 'generic subset' construction for generic terms.

Prove the recursion axiom for generic terms.

Complete proof of uniqueness for generic terms' recursion combinator.

More progress towards generic terms' uniqueness result.

Start on generic_terms' uniqueness lemma; fix distinctness.

Move LIST_REL from quotient_list to list, and make it more polymorphic.

The extra polymorphism makes LIST_REL usable in inductive definitions, as
I have done in the generic_terms example. It doesn't interfere with the
use made of it in the quotient library.

Prove freshness lemma for generic terms' recursion combinator.

Slow progress on freshness lemma for generic term recursion combinator.

Progress with generic terms.

- Prove their BVC-compatible structural induction principle.
- Prove lemmas from Urban-Barendregt towards recursion principle.

Start hacking towards a nominal recursion principle for generic terms.

Lift generic term induction thm; prove some results about lifted type.

Michael Norrish posed this as an example for the higher order quotient package.
This example now works with the recently revised package. The problem was forming a quotient of a polymorphic type. The code to lift theorems previously expected only monomorphic types.

generic_terms: work towards isolating problem in my quotient attempt.

Minor twiddling with generic terms.

More theorems for generic terms - quotient not far away (I hope\!)

Prove another lemma about "generic" terms.

Progress with generic terms - transitivity of alpha-equivalence shown.

New theory to be basis for Tom-Melham-style nominal datatype package.

May all fail completely - but it will be an interesting experiment.