add equality, unfolding TC to the right

This adds RIGHT1 versions of EXTEND_RTC_TC{,_EQN}.

Avoid combining star for RTC operator; use Slavonic Asterisk instead

The meaning of "combining" in the combining star character (U+20F0) is
that it should combine with previous characters in the same way as
separate accent characters (such as acutes: é) can combine with
predecessors. Using it as a pseudo-superscript just because it looks
OK in my particular Emacs handling of fonts and characters is a bad
idea. In other contexts, I have seen it actually combine, and it
looks terrible.

So, instead of trying to solve the problem of general superscripting,
I'm changing to U+A673, which is a whole character in itself (not a
combining accent), is an asterisk, and seems to be generally typeset
relatively high on the line. It's "open" which is a bit strange, but
otherwise seems to look OK. Here's an example:

RTC_SUBSET: ⊢ R x y ⇒ R꙳ x y

Provide default inductions for TC, RTC, and EQC

I hesitated to do this previously because there are a bunch of
reasonable alternatives for these, and I was unsure about "forcing"
people into one choice. But the new 'using' tactical makes this less
of an issue.

Make a bunch of rewrites about relation$inv automatic

Make a bunch of rewrites about relation$inv automatic

Tidy up some src directories for line-lengths

Add special Overload syntax to map to overload_on

Use in a few random places in src and examples, and document in
release notes and DESCRIPTION.

Provide Triviality syntax as alias for Theorem[local]

This works with both

Triviality foo:
statement
Proof
tactic
QED

and

Triviality foo = ML-expression-of-type-thm

Illustrate in relationScript.sml.

Moved BISIM(_REL) theorems to bisimulationTheory with coinduction principles added

Some supporting theorems of relation$BISIM

Got rid of last pesky unicode

Changed bisimulation work in relationTheory to use ASCII not Unicode

Added bisimulation and bisimulation relations to relationTheory (alongside proof the latter is an equivalence)

Use new Inductive syntax to define relation$RTC

Adjust some proofs that used the old RTC_DEF theorem, which has
disappeared.

Find a superscript * (sort of) in Unicode to use for RTC syntax

Make equality of "tight" precedence by default

Start to work through knock-on effects of this.

Import a theorem about RINTER from CakeML

Provide alternative Theorem-syntax for store_thm

Reconcile store_thms with diverging names in db and val binding

Remove TABs from src

Will also make selftest to check that they aren't introduced

Added TeX notation for relation inversion (relinv)

Fix pretty-printing of real and relation inverses

Now both get to keep their pretty superscript forms (-1 for the reals,
and T for the relations) even when both theories are loaded. The cost
is that neither will be printed as "inv" when unapplied to arguments,
instead appearing as "realinv" and "relinv" respectively.

Closes #481

Added TeX notation for O (relation composition)

TeX notations for RUNION, RINTER and RSUBSET in relationTheory

Move Q.ID_EX_TAC to Tactic.

ID_EX_TAC doesn't take any arguments, let alone a quotation, so
doesn't belong in Q.

Closes #359

more flexible INDUCT thms for TC

more flexible INDUCT thms for RTC

Provide Unicode syntax for some relation operators

Using the subscript r character on various set notations.

Document these forms in Description manual.

Also extend definition of inv (aka "transpose") to be

:(α -> β -> bool) -> (β -> α -> bool)

rather than

:(α -> α -> bool) -> (α -> α -> bool)

which is needlessly specific.

Remove unnecessary structure bracketting

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

Fix pre-boss theories in light of pat_assum renaming

a couple of missed relationTheory OpenTheory names

add some OpenTheory names to relationTheory

EMPTY_REL does not quite match Relation.empty, since it is not
as polymorphic. The other definitions not covered by this commit appear
not to be in the OpenTheory standard library at present.

Change API of Q's MATCH...RENAME_TACs.

Now rather than a string list hanging off the end specifying which
variable bindings aren't supposed to induce a renaming, just put
underscores into the pattern in those positions.

Documentation and release notes updated.

Implement new scheme to allow simple addition of theorems to theorem "sets".

When saving or storing theorems, simply add [name1,name2] strings to the
end of the binding, and the theorem being saved will be added to the
theorem set with that name.

Rename implicational theorems in relation to make room for equivalences

This affects TC_CASES1 and TC_CASES2 that were hardly ever being used.
See the release notes change for more discussion.

Make a couple of important termination theorems automatic rewrites.

In particular:

|- WF $<
|- inv_image R f x y <=> R (f x) (f y)

Some relational properties of inv_image.

There doesn't seem to be anything to be said about anti-symmetry.

Add domain restriction and deletion to relations (reusing \\ syntax).

Move some results from enumfset earlier into relationTheory.

add some more OpenTheory names to the map

Simplify definition of relation$StrongOrder.

Thanks to an observation of Paul Loewenstein's.

Change RTC and TC syntax so that bare TC prints as TC, not $^+.

Analogously for RTC and ^*. EQC was already set up to do the right thing.
When these constants have arguments, they continue to print with the special
syntax.

Avoid some more "Matches are not exhaustive" compiler warnings.

Prove that subsets of irreflexive relations are irreflexive.

Two simple properties about RINTER.

Prove easy consequences of being a well-founded rlation.

Remove Unicode that has crept in to some source scripts.

Added theorem reflexive_TC, analogous to symmetric_TC.

Add a bunch of export_rewrites to relationTheory.

Added some theorems to relation theory:
reflexive, transitive, and symmetric for EQC;
EQC moves in over (and replaces) RC, TC, and SC; and
a (TC R) step from x to z implies an R step from x to some y (y and z not equal to x).

3 more RTC 'lifts' theorems, analogous to TC's (and others').

New theorem about RTC by analogy with (e.g.) TC_lifts_monotonicities.

Move IndDef earlier in the build sequence (just before BasicProof).

This will let me reinstate my new Induct_on functionality.

TeX macros in TeX_notation calls need to be terminated with {}.

Move more TeX notations into appropriate theory files.

Word-related notation still to do.

Add a theorem suggested by Ramana Kumar: WF_TC_EQN |- WF (R^+) <=> WF R

Add another explicit dependency on satTheory to work around Holmake's
problems.

Add yet another cases theorem for RTC, this time relating it to TC and
an equality.

an equality version of EXTEND_RTC_TC was added

Add a new theorem (stating that RTC R x y ==> EQC R x y), and also add
a new notation ^= for EQC, making the above theorem print as
R^* x y ==> R^= x y

Fairly dramatic change, supporting the use of "syntactic patterns".
It is now possible to overload a name to term (typically a
lambda-abstraction) in order to create syntax-only definitions. For
example, there is a definition of not-equals now in the system:
val _ = overload_on ("<>", ``\x y. ~(x = y)``)
val _ = set_fixity "<>" (Infix(NONASSOC, 450))
This definition is parsed and pretty-printed.

Two other annoying changes. The interface for adding unicode variants
has changed, and I have made precedence level 450 of the parser
non-associative. This latter change has caused most of the (minor)
adjustments to the files below. The regression test doesn't go
through yet. (Currently there is a failure in
quotient/examples/sigma that I don't understand.)

Change export_rewrites back to its old API (without requiring an extra
string). When exported, the resulting simpset fragment always picked
up the name of the theory to be the base of its name, so there didn't
seem much point in giving users a false impression of naming power.

Use superscript plus to make transitive closure look nice in "Unicode mode".

Make ^* and ^+ available as suffix forms of RTC and TC respectively.
These will take precedence by default. Use, for example,
overload_on ("RTC", ``RTC``) to revert.

Add another automatic rewrite about RTC, that:
!R x y. R x y ==> RTC R x y

Add a very obvious rewrite (|- RTC R x x) to the srw_ss().

A whole mess of small changes intended
at making simpsets prettyprint informatively
in the interactive loop. Very possibly
I haven't updated all the files in the examples
directories.

Fix relation composition to treat the arguments by analogy with
function composition. This is the way I decided to do it in r3606,
inviting "counter-arguments". Konrad silently changed it in r3626.
(I didn't notice because I had typically been doing things like
alpha O beta O alpha
until today.)

Did some community service expunging all occurrences of the old syntax for
if-then-else from the HOL distribution.

Apologies if I've broken your example or development: you can either upgrade
it to use the new syntax or else issue the magic parser incantation that
I chopped out of boolScript.sml on this check in.

Add inductive definition support for constants from relationTheory (TC, RTC,
EQC and SC).

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

Add an export directive for an obvious rewrite.

I thought this generalisation worth stating too, though I think the three
specific results will be most commonly used.

Some simple results about how the closure operations preserve certain
properties of the underlying relation.

Mostly minor changes. Mainly, have changed FUPDATE_LIST in
finite_mapTheory to be a prefix, and have replaced it with
the infix notation |++.

Michael said it was OK.

Moved contents of TermRewritingScript.sml to relationScript.sml

Added definition of "total" to relationScript and the other changes
are odd-and-sods.

Restore some theorems that Konrad's latest check-ins brutally removed.
Moral of the story: if you see a check-in in hol-checkins you really
should do a cvs update to bring those changes into your working
directory ASAP. Otherwise you're storing up potential trouble for
yourself.

Can't forget this!

Added Krstic/Matthews theorems supporting nested recursion.

I think this is wrong: relation composition should look like function
composition, so that the first relation to be "applied" is the second
argument to the composition operator. Am happy to hear counter-arguments.

Some new and useful facts about the equivalence closure operation.

Fix for bug 916157 (from Lockwood Morris). Q.UNDISCH_THEN now behaves
like UNDISCH_TAC rather than PAT_UNDISCH_TAC.

Fix a naming mix-up; spotted by Lockwood Morris.

Factoids 'R' Us.

A whole lot of new stuff, mainly based on a script file that Lockwood
Morris sent me.

More induction principles for TC and RTC. These provide inductions that
allow you to work on a problem a step at a time from the right hand
end of the steps between source and destination. Without doing proofs
by induction on the number of steps taken, I can't see a nice way of
deriving these principles from each other. The fiddly approach for
TC_INDUCT_RIGHT1 doesn't need to be repeated for RTC because RTC's
principle can be proved given TC's.

Prove a cute little theorem about the K combinator. This is a necessary
prelude to one last change I'm contemplating to make record type
definition roughly twice as fast as it is at the moment. The change to
relationScript makes it explictly depend on combinTheory, something the
automatic dependency analysis can't figure out on its own.

Some easy extra theorems about symmetric closures, about taking the
reflexive, transtive and symmetric closure (here called EQC), about
inverting relations, and a simple separate theory with basic
rewriting theory (diamond properties, Church-Rosser, strong normalisation).

Added definition of the wellfounded part of a relation. Useful in the
slick proof of the multiset relation, which has not yet been implemented,

Also added an "equality" version of WF_INDUCTION_THM.

Fixes for bugs caused by using direct equality on terms. Exploits for these
require creation of terms that have explicit substitutions in just the
right places, but shouldn't be too hard to imagine. Also added
term_eq to the Term signature to be a safe curried equality.

A couple more useful theorems about TC and RTC.

More useful induction principles for TC (transitive closure).

Big terms can be constructed in finite time now. On my laptop,

list_mk_abs(1Mvars,list_mk_conj 1Mvars)

gets built in about 20 seconds. list_mk_forall and list_mk_exists are
twice as slow. If you are going to build terms with lots of
binding, please use these things in favour of

itlist (curry mk_forall) vlist tm

which 1) is slow because of the iterated mk_forall and 2) blows the stack
because of the itlist, at least in MoscowML, which allocates the call stack
on the stack.

Still to do: 1) upgrading this treatment to strip_abs, strip_forall, and
strip_exists; 2) upgrading it to paired abstractions; 3) efficienct versions
of SPECL and GENL (if possible); and 4) a rewriter that uses these facilities
to traverse deeply nested binders efficiently (this will (1) be a first
order rewriter and ... uh lost my train of thought).

There are some tests in src/0/big.term.tests. These should also be fleshed
out to have more strenuous tests, say ones with multiple parallel deeply
nested scopes.

... uh, the above 20 second claim is true if the list_mk_conj had
been done previously (I was mainly testing list_mk_abs).

The implementation uses Polyhash to represent the list of variables to
be bound, and utilizes continuation passing style to get tail recursion.
Otherwise, I couldn't get to 500K variables without blowing the stack.

Updated higher-order matching algorithm to be direct translation of
latest version of algorithm in HOL Light. A couple of script files in the
distribution needed altering.

Slew of theorems about RC and RTC (new constants).

Changed Empty to EMPTY_REL and renamed various theorems accordingly.

paired syntax.

Changes to handle new type for Q.prove.

relationScript.sml is intended to grow into a general theory about
relations taken as functions of type 'a -> 'a -> bool. Currently,
only transitive closure and wellfoundedness are dealt with.