Prevent bad constant names at Definition level

Enforces a constraint I'd long assumed to be true.

Closes #268

WIP fixing problems with 57d38bd4

Delete the 'rep' and 'abs' constants after a datatype is made.

These hang around completely unnecessarily at the moment.

Avoid a bunch of pattern completion warning messages.

Another Substring problem. Sorry for piece-meal checkins.

A proper fix for what r6851 attempted to fix. The problem was
demonstrated by ideaMultScript in examples/Crypto/IDEA. This loaded
its ancestor theory ExtendedEuclid before it loaded the ind_types
module. The problem is that ExtendedEuclid makes "P" a constant, and
ind_types attempts to prove a lemma internally where P has to be a
variable. Now, it also sets up its parser to be with respect to a
grammar not contaminated by ExtendedEuclid, so its statement of the
goal is fine.

The goal is

!P t. (!x. (x = t) ==> P x) ==> $? P

Unfortunately, when the tactic that comes to solve this goal calls

REPEAT GEN_TAC

the code in GEN_TAC spots the "P" and checks the *global* grammar for
clashes with known constants. P is such a beast, and so the goal
after the GEN_TAC is

(!x. (x = t) ==> P' x) ==> $? P'

A later tactic that mentions P (which is still parsed correctly as a
variable called "P") then causes the tactic to derail and the proof to
fail.

It's possible to make the tactic work by using X_GEN_TAC (but not
Q.X_GEN_TAC), but it's all terribly ugly, and so I decided to prove
the theorem in boolTheory, so that the *three* places where the same
code was being duplicated could pick up the theorem without reproving
it. I also removed the code duplication by making the one version in
Prim_rec the source for the two other users.

Now examples/Crypto/IDEA builds properly.

This fix will have to be merged into

branches/release-development/kananaskis-5

This does suggest, incidentally, that Konrad's solution to parsing
protection, involving setting the global grammar reference at the head
of library files, is pragmatically better, for all that futzing around
with references is ugly, and requires the end of the file to set the
global reference back to what it was (yergh). I will have to give up
on my "clean" solution, which rebinds/redefines the Parse structure at
the head of library files.

Fix for problems caused by a theory that defined P to be a constant,
and then caused pain when interacting with files that wanted P to be a
variable. The protection already in ind_types.sml wasn't enough
because of the use of Q, which then caused parsing to refer back to
the global grammar rather than the rebinding of it at the top of the
file.

Removing the "prod" modification, as this is redundant with Michael's recent improvement to the sorting used.

Fix for bug reported by Tom Ridge. Change to ind_types.sml includes
some reformatting/re-indentation of the source code around the change,
so it looks more significant than it is. It turns out that the
problem was in the behaviour of the sorting function (which seems to
be the place where the HOL Light and HOL4 implementations diverge: in
their underlying libraries!).

The code gets the list of type arguments to constructors that mention
types about to be defined underneath other operators. For example, in

'a list = NIL | CONS of 'a => 'a list

there are none. In complicated cases like Tom's, there are lots. He
had

com = skip | seq of bool # com # com | if of bool # num # com # com
| while of (num # num) # bool # com

Then the list of types is

[bool # (com # com), bool # (num # (com # com)), (num # num) # (bool # com)]

Each of these is dealt with in turn, and it is important that they be
done in order with bigger types being done first. The constructors in
each argument are broken down one level at a time, so the
implementation would eventually get itself into a state where the list
of recursive nested types was something like

[com # com, bool # com, num # (com # com)]

Unfortunately, in this situation, the sorting function did the wrong
thing and didn't see that

num # (com # com)

should be done before (com # com). The ordering function passed to
the sort function was the flip of sub-type inclusion, with
incomparable types being treated as EQUAL. In the situation above,
num # (com # com) didn't move to the front of the list. This sort of
thing is a risk with a sorting comparison that doesn't respect
equality. (I.e., num # (com # com) < com # com, but it isn't less
than bool # com, which is, however, 'equal' to com # com.)

I see that HOL Light has a quicksort as its sort function, whereas our
Listsort.sort (from the Moscow ML library) is a mergesort. Perhaps
quicksort does provide some sort of useful guarantee in this
situation. Anyway, the fix is easy enough: just sort by (flip of)
type size.

Here's a fix to the datatype code for Hol_datatype, to deal with the example raised by Tom Ridge (repeated below).

I expanded the definition of ind_types.lift_type_bijections to now handle "cty" arguments which have a bijection nested under a pair type operator. Before, it only handled arguments which were either directly listed as a bijection, or which were nested under a "fun" type operator (which as far as I could tell, would never be exercised by this code).

This makes use of a new theorem in ind_typeScript.sml, called ISO_PROD, crafted similarly to ISO_FUN:

ISO_PROD
|- ind_type$ISO f f' /\ ind_type$ISO g g' ==>
ind_type$ISO (f ## g) (f' ## g')

There also needed to be some modifications to the code in ind_types.sml, in the (first) routine named "define_type_nested", around the line 1471, where additional simplifications needed to be performed to get rid of the ##'s introduced. Note that REWRITE_FUN_EQ_RULE has been augmented as well.

This seems to work for Tom's example, so that the normal theorems are produced.

(* * interactive *)
app load ["finite_mapTheory"];
(* also need libTheory transition_systemTheory *)

(* * start *)
local open HolKernel boolLib Parse bossLib (* cheat *) finite_mapTheory in end;
(* local open in end; *)

val _ = new_theory "hoare_tso";

(* + types *)
(* . mem_location, reg_name *)

val _ = type_abbrev("mem_location",``:num``);
val _ = type_abbrev("reg_name",``:num``);
val _ = type_abbrev("label",``:num``);
val _ = type_abbrev("lbl_pair",``:label#label``);

(* . language *)

val numexp_def = Hol_datatype `
numexp =
IdentM of mem_location
| IdentR of reg_name
| Num of num
| Plus of numexp # numexp
`;

val bexp_def = Hol_datatype `
bexp =
Equals of numexp # numexp
| Conj of bexp # bexp
| Disj of bexp # bexp
| Not of bexp
| TT
| FF
`;

val command2_def = Hol_datatype `
command2 =
Skip2 of lbl_pair
| AssignM2 of lbl_pair # mem_location # numexp
| AssignR2 of lbl_pair # reg_name # numexp
| Seq2 of lbl_pair # command2 # command2
| IfThenElse2 of lbl_pair # bexp # command2 # command2
| While2 of lbl_pair # bexp # command2
| LoopUntil2 of lbl_pair # bexp # bexp
| Barrier2 of lbl_pair
| Xcmpxchg2 of lbl_pair # mem_location # reg_name # reg_name
`;

Get choice of appropriate letter for list types to cope with
possibility that list operator's argument may be a variable type.

Alter the construction of induction theorems so that bound variables
with string type get "s" as their names (subject to variation so as to
avoid other variables in the context). This should make the change of
``:string`` to be ``:char list`` less disruptive. (The fact that we
may have already done the hard work to cope with this is neither here
nor there: in fact, I think the fixes I have made have made the proofs
concerned more robust.)

End of the *v saga. I found the spot in Pmatch.sml
that was failing to collect all the free vars
that needed to be renamed away from.

Misc. other tidying, including an incomplete
attempt at getting datatype constructors to
be defined in terms of numerals rather
than successors.

Fix for a Define bug spotted by mjcg. When
dealing with recursive calls under a case,
if variables with certain names (those
starting with v) are bound in the case
pattern then it can happen that variables
generated during pattern matching can be
the same, leading to failed proofs. Totally
obscure, and dealt with properly (I think)
in normal pattern matching. So, a difference
between Pmatch and Functional. The fix is
to invent a class of variables not accepted
by the parser (i.e. starting *v) and to later eliminate
the weird names from any theorems coming out of Hol_defn.

Some other trivial mods made in passing also, plus
tests for the new behaviour.

Also a new conversional, MAP_THM, which applies the
given conversion to the assumptions and conclusion
of the given theorem.

When defining a nested recursive data type, had been getting a
complaint about invalid vartype format. This was caused by internal
creation of magic type variables. Temporarily shut off the complaint
during the reasoning rather than invent reasonable names.

Fix bug whereby the term grammar would fail to print in an interactive
session following a Hol_datatype call. Temporary, deleted constants were
lingering in the overload map, which led to the following exception being
raised:

<installed prettyprinter failed: Fail "term_grammar.prettyprint:
should never happen">

Constants are no longer considered out of date if their witnesses
become out of date. Thus, one might define
c = rhs
and save this definition with name "c_def". Subsequently, if
something in rhs becomes out-of-date, then c_def will be removed from
the theory. However, this change means that the constant c will
remain, as will any theorems mentioning it and not otherwise
out-of-date.

Next change in this area will be to attempt to share Sig or something
like it between both kernels.

Make the revised code in these directories use the common interface in
Theory.sig rather than stuff that only appears in the
experimental-kernel.

Make the datatype package remove the intermediate cruft that it
generates in the process of setting up a new algebraic datatype. This
knocks the ladder away once the summit is reached, but definitions as
a conservative extension mean this is sound, as well as healthier for
our bloated theory files.
The change to abstraction.sml comes about because it was making the
mistake of thinking the the definitions and theorems functions
necessarily returned up-to-date theorems.
The change to Parse.sml stops it from emitting theory-instructions
that refer to out-of-date constants.

Changed the TypeBase to be indexed by types. Originally it was
indexed by a single string (representing the type operator), then
Michael changed it to a pair of strings (precise representation
of the type operator). The latest change allows non-datatypes to
be added to the TypeBase. This will allow case analysis and
termination proofs to be supported for non-datatypes.

I reckon there are still a few bugs left after the massive
revision, so you might want to wait a while before upgrading.

Wide-ranging change to make the TypeBase export an interface forcing users
to be concerned about which theory their types are from. Interactive users
of the "induction_of", "axiom_of" and similar functions are thrown the only
bone: they can effectively omit the theory parameter by using "" instead
of a theory name.
Prompted by a bug found by Tom Ridge where it was impossible to define
a pattern matching function on a type with the same name as another type
because the pattern-matching code was using dest_type and TypeBase.read
on just the type-operator name.

Revised exportML so that it takes a path parameter, which tells
where the ML corresponding to a theory is to be written.

This has been propagated to all the theories that already export
ML, and the mkword.exe tool has been upgraded to also take a
path where it should write the generated ML. This is useful,
because doing an exportML to the same directory as the theory
files will end up confusing Holmake.

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

Fairly radical changes: theorems' hypotheses now stored in a binary tree.

Change stemming from split of TypeBase into TypeBasePure and TypeBase.

Modifications caused by change of TypeBase signature.

New work aimed at making a single global EVAL function, with
an underlying compset.

Minor adjustments to fit with changes in IndDefLib.

Minor changes.

Fixing up problems that I introduced while in a fit of passionate revision.

Upgraded to build under Kan. 0.

Made it all Kananaskis compatible. Datatype fails to load because of
something going wrong in loading pairTheory. This is BAD.

Somewhat hackish fix for bug reported by Kim Sunesen, whereby
`repDatatype =
repBool of bool
| repMap of (bool list) # (repDatatype list)
| repSet of bool list
| repEnum of bool list
| repTuple of repDatatype list `;
worked, but
`repDatatype =
repBool of bool
| repTuple of repDatatype list
| repMap of (bool list) # (repDatatype list)
| repSet of bool list
| repEnum of bool list `;
didn't, because of the order in which type bijections were attempted.
I've written to John Harrison to see if there is a better solution.

Fix to make the following example (due to Trent Larson) work correctly:
foo = T1 of 'a # 'b | T2 of foo list
Wasn't avoiding the types 'a and 'b because they were hidden under a type
operator. Use of type_varsl fixed this.

Trent Larson pointed out that when type variables in a datatype were
not at the top level, then the axiom produced by datatype definition
was not quite right. Fixed.

Fix to put back obscure names for the representation and abstraction
functions of a type; thereby fixing Kim Sunesen's bug:
Hol_datatype `Ty = mk_Ty of bool`
failed.

Changes to accomodate proper definition of size functions for nested types.
Also, elimination of dependence on Ho_theorems.

Changed names generated for representation and abstraction functions of
new inductive types. Hitherto, these were "mk_Ty" and "dest_Ty". These
names are too nice, and may be wanted by users, possibly even as
constructors. Now, these internal constants have names prefixed by
"ii_internal_", which should do the business.

Fixed a bug introduced by my previous fix. Problem was spotted by Konrad
and caused

Hol_datatype `xtree = Leafx of 'A
| Branchx of xtree list`;
Hol_datatype `simper = LAF of 'A | BUB of simper xtree`;

to fail (with the second definition), while

Hol_datatype `xtree = Leafx of 'A
| Branchx of xtree list`;
Hol_datatype `simper = LAF of 'a | BUB of simper xtree`;

worked. The bug was caused by me remapping type variables in the
recursion theorem returned by the lookup to TypeBase, but not in the
induction theorem.

Proper size definitions.

Fixed a bug discovered by Konrad whereby nested type definition attempts
failed if a type variable under a constructor was the same as the type
variable used as the range of the function asserted to exist by the
type axiom of the operator under which the nesting occurred.
Also canonicalised the type variables in the final recursion theorem to
avoid use of 'Z, 'Z0 etc. Instead the smallest names available in the
sequence defined by Lib.tyvar_vary are chosen.

Tiny fix (parsing bug that manifested itself with "s" combinator from
examples/ind_def/clScript.sml).

When defining a nested recursive type, John's code was expecting an
induction theorem in his style, but was getting one in hol98 style. This
problem has now been fixed. Nested recursive types still don't work
because they don't get a size function defined for them, but they're
closer.

Appropriate letter for a variable with a variable type is the second
character in the string of the vartype name, not the first.

Changes due to the incorporation of John Harrison's datatype definition
package.
Here are the rest of the significant changes. The interface in Datatype
has been fleshed out quite a bit, but what was there has stayed pretty
much the same (except that prim_Hol_datatype doesn't write stuff out
to disk anymore; it's hardly very pure if it does so).

The ind_type theory is the basis for ind_types, which is in turn called
from Datatype.