Remove unnecessary structure bracketting

As per 89fc99bc3, but on as many examples as a grep -R can find.

better match intended semantics of OpenTheory names

rather than using strings, now have a type abbreviation otname for
string list * string. it might be worth writing more operations on this
type (like for manipulating the namespace).

add a few more names to the OpenTheory map

specifically, bool$ARB, bool$TYPE_DEFINITION, and some stuff from
ind_type

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.

src/num/theories/SingleStep.{sig,sml} is gone. The
defininitions of Cases, Cases_on, Induct, Induct_on,
CASE_TAC (and co.) are now in basicProof/BasicProvers.
completeInduct_on and measureInduct_on are now in
numLib. recInduct is now in src/tfl/Induction.sml.
All these are collected in bossLib, so the changes
should be invisible to ordinary users.

SingleStep.*.doc has been changed accordingly.

BasicProvers.NORM_TAC should now automatically perform
all case splits (from if-then-else expressions as
well as case expression) arising anywhere in the goal.

Additions to multiset and primeFactor
theories. Fixed definition of PRIMES
sequence in dividesTheory. Also added misc.
theorems to arithmetic. Some amount of
meaningless shuffling about.

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

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
`;

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.

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.

Modify the numeral and ind_type theories to "hide" their constants so that
they don't contaminate the standard constant name-space. All such can
be retrieved by using the thy$cname syntax. (Am tempted to do the same
for NUMERAL, BIT1, BIT2 and ZERO, which live in arithmeticTheory.)

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.

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.

Change to type of new_specification, and made it tell that parser about
the introduced constants. Lots of knock-on (trivial) mods.

* Slight modification to behaviour of conditional expression elimination
simpset fragment in boolSimps
* Addition of new simpset fragment to do no more than just lift
conditional expressions as high as possible (can blow terms up in size
dramatically)
* Removal of ETA_ss from bool_ss. Doing this resulted in 6 proofs needing
a simple modification (++ ETA_ss). The change to integerScript is a
result of the change in conditional expression behaviour.

Changing arithLib to numLib.

Minor changes to map latest changes in IndDefLib.

Minor changes, to accomodate changed interface to
IndDefLib.new_inductive_definition.

Minor adjustments to fit with changes in IndDefLib.

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.

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

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.