Fix an occurrence of augment_srw_ss to be “logged”

flip arguments of UNION

add UNION_DIFF_EQ to the simp set

simplify `s ∪ (t DIFF s)`

Prove FINITE (POW s) <=> FINITE s as automatic rewrite

Only had R-to-L direction previously.

Add some easy automatic results about closures of SUBSET and PSUBSET

Things like

RTC $SUBSET = $SUBSET

Also facts like

transitive $SUBSET

Attempt at better Abbrev protection

This in the face of simplification and the variable elimination done
by RW_TAC and friends. Core sequence, -t1 and some of -t2 builds (up
to category theory example).

Machinery for dynamically reverting to the old behaviours possible
through diminish_srw_ss and a trace variable.

This is work on github issue #800

Define a disjoint-union function ('a set -> 'b set -> ('a + 'b) set)

Prove a "deep intro" rule for pred_set$CHOICE (for DEEP_INTRO_TAC)

It's vaguely annoying that we even have CHOICE when we could just use
$@...

Product measure and Tonelli's theorem

Updated HOL Description for mathematical theories (with other cumulative fixes)

Enhanced fcpTheory (FCP_FST, FCP_SND, FCP_CONCAT_THM, ...); moved duplicated HAS_SIZE to upstream

Strong Law of Large Numbers for uncorrelated r.v.'s (SLLN_uncorrelated)

Tactic to automate some routine set theory by reduction to FOL (#722)

* Moved SET_TAC into pred_setLib; some additions in pred_set and real theories

* Added quantifiers to COUNT_11

* Added missing "from_def" and related theorems (moved from real_topology to util_prob)

* Renamed SET_RULE to SET_CONV

* Added util_probTheory (from_def) into dependencies of real_topologyTheory

* Cancel changes in seqTheory

* Cancelled SUBSET_DIFF_DISJOINT and SUBSET_BIGUNION

* Further canceled two "tail_*" theorems

* IMAGE_EMPTY_FUN -> IMAGE_CONST (more general)

* Canceled IMAGE_EMPTY_FUN/IMAGE_CONST (IMAGE_EQ_SING is more general)

* Moved SET_TAC, ASM_SET_TAC and SET_RULE to bossLib with documentation (help and release notes)

* Reverted (original) empty lines in pred_setLib files

Implement new Type syntax to stand in for type_abbrev{,_pp}

Use it in pred_set and words theories

Make some PREIMAGE theorems automatic rewrites

Also remove |- SING s ==> FINITE s from the set of automatic rewrites.

The presence of this is bad because a "Once" simplification theorem
meant for s may fire when the simplifier attempts to discharge the
hypothesis, and so it won't get to fire when actually rewriting s in
the "main" goal. (And no-one uses SING.)

Knock-on effects simplify folCanonScript.sml, the experience of
writing which prompted these changes in the first place.

Use new and improved Induct_on to simplify some proofs in pred_set

Fix LaTeX for universal set: \ensuremath{\cal U} leaks \cal mode

Instead, need to write \ensuremath{{\cal U}}

Fixes for pred_set to build under MoscowML+tightequality

Remove older of Theorem syntaxes (the one with the quotes)

It's confusing to allow two, and it seems pretty clear that the
Proof-QED proof is nicer.

Fix handling of "IN_" thms in pred_setScript given Theorem syntax

Issue is that Theorem foo: ... Proof .. QED turns into a call to
Q.store_thm, but the code in pred_setScript wants to intercept calls
to store_thm to add _applied versions of various theorems. Rebind Q
structure at head of file to achieve this.

Get src/pred_set to build given tight equality

Use Theorem syntax more in pred_setScript.sml

Add theorem about triangular numbers (SUM_SET (count n))

This is inspired by a theorem from CakeML, but generalised as the
CakeML theorem unnecessarily restricted itself to n > 0.

Move some theorems into HOL from CakeML

Touched theories include alist, list, option, pred_set.

Remove Unicode in src that my last commit introduced

Move some theorems into pred_setTheory from CakeML

One, INFINITE_INJ_NOT_SURJ prompts a complete reworking of the very
old proof in this script that establishes something similar but only
for universal sets. The new result is stronger, and is used to
establish the old one.

The new proof is in a similar style, but uses technology (METIS_TAC
and the simplifier) that wasn't available in HOL88. It also uses a
newer result (the statement of the pigeonhole principle). It's rather
shorter therefore.

Change type_abbrev to not alter printing behaviour

If printing of abbreviations is desired, users must now use
type_abbrev_pp.

Closes #599

Move p/printing of set comprehensions out of src/parse

The code for this can be put into pred_set/src/pred_setpp, making the
core pretty-printer slightly simpler (which has to be a good thing).

Also fix the minor pretty-printing indentation bug identified in
github issue #610.

Making this a "user pretty printer" means that it takes precedence
over overloads. Introduce a new feature whereby adding a
(dummy) user-printer with the empty name causes terms matching this
pattern to be printed without any user-printers getting a chance to
fire. This gives terms that are handled by overloads a chance to be
seen by the core printing machinery. (User printers are checked for
first and can otherwise mask everything else.)

Closes #610

Delete trailing whitespace in src/

Merged hol-light's cardTheory (rich_cardinalTheory) with HOL4's cardinalTheory

Merged HOL4's original topologyTheory with HOL-light's version

Added rich_topologyTheory and dependents

Add is_measure_maximal constant to pred_set; include minor cleanups

Cleanups include making automatic rewrites happen in the flow of the
script file rather than being delayed until the end.

The is_measure_maximal constant has definition:

is_measure_maximal m s x <=> x IN s /\ !y. y IN s ==> m y <= m x

Prove some simple theorems about this.

Revert "Add hypotheses count check to TAC_PROOF."

This reverts commit 01930d56ce7a31c10ff7f422a0cf535a8c502a59.

I don't believe that changing this primitive is a good idea. I'd like
TAC_PROOF to stay as the base primitive that applies a tactic to a
goal state without checking for validity or similar.

This change is also causing breakages in CakeML and
examples/machine-code/lisp. If there is a need for this sort of
validity-style check (apart from what is done by expand), it could be
added to prove quite reasonably, possibly there under the control of
another trace variable, or just permanently on (as it is easy enough
to change the behaviour of prove by adjusting the reference it
consults).

Add hypotheses count check to TAC_PROOF.

This helps guard against the following:

val lem = Q.prove(
`F`,
ACCEPT_TAC (ASSUME ``F``)
)

Before this returned the theorem [F] |-> F without complaint, despite an "Invalid tactic" exception being raised when using proofManagerLib.e. This proof will now fail. The new check falls short of requiring alpha equivalence of assumption lists, which would be safer.

This change has identified a few areas of imprecision within automation, namely within "dep_rewrite" and "Satisfy". There it may be the case that a subset of the stated assumptions appear in the final theorem.

Remove TABs from src

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

Change irule to not include a rpt conj_tac effect

Closes #465

Re-implement Datatype package with TypeBase sexps (not adjoin)

Fix multi-line list forms (incl. records)

Add some theorems from CakeML

pred_set: to do with bijections and surjections
list: MAP2 and LIST_REL results
pair: rewrites with (FST x = y) and (SND x = y) as LHSs

other changes are fixes for broken proofs.

Remove -- as an alias for Term parser.

As per comment in release notes this has long been replaced as
appropriate style.

Provide new automatic rewrite for “UNIV x” (rewrites to T)

Correctly isolate univ user-pretty-printer

This preserves it across set_grammar_ancestry calls, and simplifies
the script file slightly.

Closes #445

Move FINITE_BIJ_COUNT_EQ to pred_setTheory to simplify FINITE_BIJ_COUNT, with miller and diningcryptos examples adjusted

Clean up of extra_pred_setScript.sml

More additions in pred_set and util_probTheory

Simplified cardleq_ANTISYM (using SCHROEDER_BERNSTEIN in pred_setTheory); moved INJ_BIJ_SUBSET to pred_setTheory

Fixed remain issues in examples/miller

Move BIJ_FINITE_SUBSET and IMAGE_II from util_prob to pred_setTheory

Move basic PREIMAGE lemmas from util_prob to pred_setTheory

Moved FINITE_BIJ and BIJ_ALT to pred_setTheory

Renamed countable_alt to upper cases

Moved COUNTABLE_ALT (as COUNTABLE_ALT_BIJ) and dependencies to pred_setTheory

Removed some duplicated countable theorems from util_probTheory

Merged more countable theorems into pred_setTheory

Remove duplicated countable_def (in util_prob) and prove it as an alternative definition (countable_alt)

Move Schroeder-Bernstein theorem (and related settings) to pred_setTheory (from util_prob):

SUBSET_THM
K_SUBSET
SUBSET_K
FUNSET
DFUNSET
IN_FUNSET
IN_DFUNSET
FUNSET_THM
UNIV_FUNSET_UNIV
FUNSET_DFUNSET
EMPTY_FUNSET
FUNSET_EMPTY
FUNSET_INTER
schroeder_close
SCHROEDER_CLOSE
SCHROEDER_CLOSED
SCHROEDER_CLOSE_SUBSET
SCHROEDER_CLOSE_SET
SCHROEDER_BERNSTEIN_AUTO
SCHROEDER_BERNSTEIN
BIJ_INJ_SURJ

Moved 23 small theorems from util_prob to pred_setTheory:

BIGINTER_SUBSET
BIGUNION_IMAGE_UNIV
BIJ_SYM
BIJ_SYM_IMP
BIJ_TRANS
DIFF_BIGINTER
DIFF_INTER
DIFF_INTER2
DISJOINT_ALT
DISJOINT_COUNT
DISJOINT_DIFF
DISJOINT_DIFFS
EQ_SUBSET_SUBSET
FINITE_REST_EQ
INFINITE_INJ
INJ_IMAGE_BIJ
IN_BIGINTER_IMAGE
IN_BIGUNION_IMAGE
IN_EQ_UNIV_IMP
SUBSET_ADD
SUBSET_INTER1
SUBSET_INTER2
SURJ_IMP_INJ

Get core HOL to build with new definition of "by"

Progress with github issue #407

quicker proof of SURJ_INJ_INV

pred_setTheory.INJ_LINV_OPT_IMAGE, lemmas

clearer proof of INJ_CARD, extra lemmas

DELETE_SUBSET_INSERT and SUBSET_INSERT_DELETE almost the same

new thm SUBSET_OF_INSERT

Fix pre-boss theories in light of pat_assum renaming

Add various theorems from CakeML

Add Theory.quote_adjoin_to_theory. Use this in llistTheory.

This should close #304.

This has been implemented using a new function Portable.quote_to_string_list. Other uses of adjoin_to_theory under src/ have been updated.

Remove some duplicates of the theorem TRUTH.

These are:
• INFINITE_DEF and IN_LIST_TO_SET (replaced with overloadings)
• IN_APP_applied and IN_ABS_applied (inadvertently generated)

Also, made changes to try to avoid new definitions in listTheory accidentally having a "_DEF" suffix instead of "_def". Old naming inconsistencies still remain in listTheory (e.g. EXISTS_DEF, FIND_def and FLAT).

These changes will break a few proofs but patches should be trivial (i.e. removing references to these TRUTH theorems and/ or renaming "_DEF" to "_def").

Add 2 theorems about SUM_IMAGE to pred_setTheory

* g injective ⇒ Σ f (IMAGE g s) = Σ (f o g) s
* g bijective on s ⇒ Σ (f o g) s = Σ f s

From Joseph Chan

User pp fns can note terms as binders to system printer

This allows better behaviour in a test case shown to me by Mike, where
annotations in monad-syntax weren't appearing.

more faster proofs in set_relation

faster proof of extend_linear_order

tweaking of slow proofs - strict_linear_order

lemmas re tc, rrestrict

prove FINITE_ISO_NUM using FINITE_BIJ_CARD_EQ

changing Unicode to ASCII

FINITE_BIJ_COUNT, and proved FINITE_WEAK_ENUMERATE from it

shorter proof of FINITE_WEAK_ENUMERATE

also IN_GSPEC(_IFF)

Delete trailing whitespace in src/

lemmas about CARD (IMAGE ...)

LINV and RINV can be defined in terms of LINV_OPT

which also makes LINV and RINV equal to each other

LINV_OPT, Left inverse, to option type

result is NONE outside image of domain
also new result CARD_IMAGE

start towards OpenTheory compatibility for relation and pred_set

This is potentially going to be complicated since OpenTheory defines a
type of sets and HOL4 does not.

Remove vacuous quantification in SUBSET_MAX_SET

There was a stray universally quantified variable that didn't appear in
the statement of the theorem.

Also slightly simplify proof.

Attempt to tidy-up some proof scripts. Much of this has come from CakeML.

Removed Unicode and tried to eliminate lines longer than 80 characters.

Also added a few new constants to listTheory: INDEX_FIND, FIND and INDEX_OF.

Added "nub" to listSyntax.

various theorems about cardinality and sets

from CakeML, probably some are originally from HOL Light

Added lemma about going in MAX_SET

A few set lemmas from CakeML.

Make some pred_set rewrites automatic.

Also fix up the script file's redefinition of store_thm (used to make
alternative versions of IN_<x> theorems).

New automatic rewrite for GSPEC f x, which shouldn't happen much.

New automatic rewrite: !s. POW s <> {}

Export pred_setTheory's BIJ_EMPTY as an automatic rewrite.

Prove ⊢ x ∉ s ⇒ s DELETE x = s and export as a rewrite

It turns out that the implication can be an iff (which is the existing
DELETE_NOT_ELEMENT theorem), but this is less useful for most
simplification.

Define MAX_SET on the empty set to equal 0.

This make the relevant equation

FINITE s ==> (MAX_SET (e INSERT s) = MAX e (MAX_SET s))

Some new theorems about injectivity, surjectivity and countability

Minor polish in pred_set + theorem about CARD(BIGUNION s)

Polish pred_setTheory with new rewrites for CARD applied to DIFF and UNION.

Preserve old theorems for the sake of backwards compatibility, so give
new theorems names with _EQN as suffix.

add various more constants to OpenTheoryMap

Put some syntax operations for bool$IN into boolSyntax.

Automatically prove a bunch of “applied” results for set constants.

An “applied” theorem is of the form

(set construction) x <=> ...

where the ... will be from the theorem

x ∈ (set construction) <=> ...

So, for example, INSERT_applied is

|- (x INSERT s) y <=> (x = y) \/ y ∈ s

These theorems are all exported as rewrites, and provide a way of
getting users out of holes where they have “set world” constructions
but have lost the ∈ connection between the set and the possible
element. Note that these theorems will attempt to put the users back
into the “set world” because the RHSs will retain their uses of ∈.

These theorems will still work fine when rewriting with IN_DEF:
something like

SIMP_TAC (srw_ss()) [IN_DEF]

will eliminate the “IN”s, even as the “applied” theorems help to make
progress with the other bits of the goal.

There’s no handling of GSPEC yet, but perhaps that can wait for HOL
Light style set-comprehension (see issue #85). The alternative is
probably a special conversion to do the right thing, though perhaps
just rewriting with

GSPEC f v <=> ∃x. (v,T) = f x

would do the trick in most cases. (The problem in general is that to
get the above rewrite to work you have to throw in
pairTheory.EXISTS_PROD as well.)

Move theorem |- univ(:'a -> bool) = POW univ(:'a) to pred_setTheory.

Theorems about countable, including countability of various universes.

A simplification-friendly version of the insert-absorption theorem.

move some theorems about DIFF into pred_setTheory

Revert "make patricia play nice..."

This reverts commit da47401d5163b28a320790e7acca897d8374880c.
Reason: qualified names in the list of add_persistent_funs exports are
supposed to work.
See comments on #73.
The reason why they probably weren't working before is that you need to
use a name like:
"pred_set.FINITE_EMPTY"
not
"pred_setTheory.FINITE_EMPTY"

Conflicts:
src/list/src/listScript.sml
src/patricia/patriciaScript.sml
src/patricia/patricia_castsScript.sml
src/pred_set/src/pred_setScript.sml

(Conflicts all due to change in add_persistent_funs interface.)

change interface to add_persistent_funs (#73) and fix more calls

The new interface takes a list of strings naming theorems.
(The old interface took a list of (string * thm) pairs.)
The new way better ensures consistency of theory development and theory
load behaviour: you can no longer pass a name with a theorem that isn't
actually saved under it.

Theorems are looked up with DB.theorem, or failing that, DB.definition
or DB.axiom.

Alas, I found more examples using add_persistent_funs to add theorems in
ancestor theories. Rather than modify the ancestor theories, I have
opted to make the offending theories save the theorems they want to add
to computeLib themselves so they have a name in the current theory to
pass to add_persistent_funs.

If this behavior was appropriate for patricia too (da47401) change it.
Alternatively, if the ancestor theories should have exported those
things for computeLib anyway, search this commit for new instances of
"save_thm" to see what needs fixing.

make patricia play nice with new add_persistent_funs (#73)

Some theories in src/patricia were calling add_persistent_funs for
definitions from other theories (list and pred_set) and using the
arbitrary code string to refer to those theorems with fully qualified
names.

The fix adopted here is to call add_persistent_funs for those constants
in the theories where they are defined.

Prep for pull.

Remove some trailing whitespace.

Added size functions for finite sets, maps, and bags.

These are helpful for measures supporting recursive definitions and
induction schemes. The size functions have been added to the TypeBase,
with the intent that Induct, Induct_on, Cases, and Cases_on should be
applicable. (However, this has not been checked yet, so these might
not work.)

The size of a finite set is the number of elements in it, plus the
sizes of all the elements. (The size of a set with 0 as an element is
larger than that set with the zero deleted.)

The size of a finite map is the number of mapped elements, plus the
sizes of the mapped elements. Key size is ignored.

The size of a finite multiset is the number of elements in the
multiset plus the sizes of the elements. There are more extensive
orderings (e.g. the multiset order) but they aren't measures, which is
important for the way termination proofs are automated.

Allow "non-datatypes" in TypeBase to have optional induction thm.

Provide appropriate values for this field for finite sets, strings,
integers, finite maps and words.

Simple new (automatic rewrite) theorem about SURJ and IMAGE.

Congruence theorem for IMAGE

Ensure tDefine quantifies variables, making it consistent with Define.

Obviously this will break code that relies on the former behaviour.

theorem: MAP preserves injectivity

Maybe the statement/name should match my commit summary better?

Also, proved a simple lemma about replacing the set arguments to INJ
with super/subsets.

theorem characterising INJ f (x INSERT s) t

Add a couple of results about pred_set$BIJ.

Make FINITE_INDUCT available to the Induct_on tactic.

Remove structure ... = struct ... end bracketing from pred_setScript.sml.

Add a theorem telling us what univ(:bool) is.

Slight simplifications of two results about partition.

Thanks to Joseph Chan for the observation that the equiv_on precondition was not
necessary in these cases.

Add new theorem about cardinalities of sets under injective images.

Move some rewrite exporting to happen immediately after the rewrite is
proved so that later proofs within the same theory can benefit.
Effect on dependent theories is unchanged of course.

Prove that IMAGE f is injective if f is.

New theorem stating that pred_set's count operation is injective.

Document new PROD_IMAGE and PROD_SET constants in release notes.

Also perform overloading to Unicode Pi and PI.

add various names to the OpenTheory map

This is in preparation for logging llistTheory.

Notes:
- Sent combin$C to Function.Combinator.c (same for combin$S).
Another name might be preferred on the OpenTheory side.
- Not sure what bool$BOUNDED is about; dumped it in the HOL4 namespace.
- Put lots of pred_set constants in the Set namespace, but in the
standard (OpenTheory) library it seems like Set is for constants
operating on an abstract type of sets (rather than predicates). I'm
not sure whether we should use a different namespace when working with
sets-as-predicates or just pretend predicates are the abstract type
and do a bit of magic on article reading/writing as necessary (don't
know what that would be exactly yet).
- Similar for constants in set_relation, which I'm currently putting in
the Relation namespace. Although it looks like currently OpenTheory
doesn't use an abstract type of relations (but probably it will
later).
- Sent marker$Cong and marker$Abbrev to Unwanted.id, but not sure if
Unwanted.id is supposed to be polymorphic (whereas those are identity
functions restricted to bool). Similar for numeral$iZ
- sent GSPEC to Set.specification; maybe not an obvious name...
- Using top-level "While" namespace for whileTheory
- dumped numeral$iiSUC in HOL4 namespace; not sure what to do with it
- BIT2 is going to Number.Numeral.bit2; this is in line with wanting the
base library to be liberal, i.e. a union of all useful basic constants
and theorems (so has bit0, bit1 and bit2)... but I think there may be
competing goals for base

Revert change to gspec2 syntax; we can use { .. | .. | .. } here.

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

Add PROD_IMAGE and PROD_SET constants (analogous to SUM_IMAGE etc).

From Joseph Chan.

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.

Add LaTeX notation for set cross-product operation.

New results and automatic rewrites about pred_set$SING.

Due to a meeting with Joseph Chan.

Characterization of BIJ as existence of an inverse

A couple of theorems about "SIGMA f s <= SIGMA g s".

A couple more theorems about ABS_DIFF

Also some lemmas about relationship between subtraction and less-than.
If only DECIDE_TAC were available here...

Significant change to pretty-printing; affects user-printing API.

The change allows user-printers to alter the main printer's notion of
what is a "seen free variable", and what is bound. The latter causes
the colouring. The first notion is important when show_types is on,
as types are only given for the first occurrence of a free variable.

This allows the monadsyntax to do the right thing with the colouring
of variables.

Add Unicode version for SIGMA

Theorem about exactly when SIGMA f s equals 0

Tactic for eliminating MAX_SET

Add congruence theorem for SUM_IMAGE

We might want one for ITSET too one day.

Added new constant 'pairwise' for asserting a predicate on all pairs of elements in a set.

New REL_RESTRICT constant; variety of proofs.

Best is probably that strong partial orders on finite sets are
well-founded. REL_RESTRICT could live in relationTheory, most of the
subsequent proofs need to be in pred_setTheory because of the use of
the FINITE constant.

Added rewrite FINITE_REST.

Make TeX of UNIV look better (removing a stray space to the left).

Also make the nice TeX form work if Unicode-pretty-printing of UNIV
has been turned off.

Added theorem BIGINTER_UNION, analogous to BIGUNION_UNION.

A couple of theorems about SUBSET respecting PSUBSET's transitivity.

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.

New statement of SUBSET_FINITE that can be directly MATCH_MP_TAC'ed.

I've been so annoyed by SUBSET_FINITE so many times, but those days have
finally come to an end.

INFINITE is now an abbreviation for ``\s. ~FINITE s``.

Prove some results about the finite-ness or otherwise of some universal sets.

Allow empty list forms to be overloaded ([], {}, etc).

This gives us the ability to get nice TeX for them. Instantiate this ability
for emptyset.

Add TeX notation for 'proper subset'.

Fix handling of special 'U' constant, retaining better backwards compatibility.

In particular, there is now a special form 'univ' that behaves as 'U' did.
Further, with Unicode on, the character U+1D54C is used in the same way.
This character may not be in many fonts, so add another trace to turn its
use off. If you can see it, it's a nice 'double-struck' U. I would have
gone for a script-style U, but it leant over too much, and so overlapped
the following left-paren character.

Make U syntax for UNIV consistent in its parsing and printing.

Now you can write FINITE U(:'a), and it parses. This used to require
FINITE (U(:'a)), which is so many parentheses that one wonders about the
usefulness of the abbreviation.

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.

Added a number of theorems, mainly to finite_mapTheory.

finite_map:
FLOOKUP_FUNION
FEVERY_FLOOKUP
FLOOKUP_o_f
FUPDATE_LIST_APPEND
FUPDATE_FUPDATE_LIST_COMMUTES
FUPDATE_FUPDATE_LIST_MEM
pred_set:
COMPL_UNION

Better support for sets as predicates in HolSmtLib, replacing {x | P x} by P.

Unicode version for PSUBSET

Add some automatic rewrites for SUM_SET and count (of pred_setTheory).

Slight tidy-up of countability theorems in pred_setTheory.

Define the num_to_pair and pair_to_num functions used there in terms
of the same functions given in numpairTheory.

Also add Unicode symbol (LaTeX's \times, U+D7) for CROSS.

Add syntax for universal sets ``U(:ty)``, where ty is the type of element.

The parsing can be done with an overload, but the pretty-printing is
done with a custom user-level pretty-printer. It comes with its own
trace variable to turn it off. To turn it off permanently, use

Parse.remove_user_printer "UNIVprinter"

Another lemma from Ramana Kumar, this one about showing what I expect
is a relatively common case for subset of a "big" union.

Make FINITE_DIFF an exported rewrite and prove a little "arithmetic"
rewrite UNION_DIFF (s <= t ==> (s + (t - s) = t)).

Addition of some mixed theorems

Forgot to store a theorem in the last commit.

A definition of countable sets, some basic theorems about them, and an few
misc. supporting theorems.

Implement ML code generation for large records.

Attempt to tidy up (fix) EmitML and finish off the transition that Scott
started. EmitML has been moved to the end of the build sequence. "Hooks"
have been eliminated and all EmitML related stuff has been removed from the
various theory directories. All code for generating ML/Caml is now
self-contained within src/emit. I've not tested the generated Caml code but
the SML seems to build fine.

The directories:

src/theoryML
src/theoryOcaml
src/emitScript

have been replaced by

src/emit/theories/ML
src/emit/theories/Caml
src/emit/theories

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.

Disable the printing of EMPTY as the Unicode emptyset character
because this breaks the "list form" printing of literal sets ({5}
prints as ``5 INSERT UEMPTY`` (where UEMPTY is the Unicode emptyset
character)). I am not sure how to fix the logic in the pretty-printer
to handle this properly at the moment.

Getting rid of some pattern-matching complaints,
as Anthony suggested.

Modify Unicode to use an interface whereby theories can specify
Unicode alternatives for their constants. These can be turned on and
off by fiddling with the trace variable "Unicode". I.e., to see
pretty stuff, run hol and then
- set_trace "Unicode" 1;
> val it = () : unit

- FORALL_SIMP;
> val it = <...pretty stuff...>
I haven't gone through and done the words because it's time for me to
go home.

Remaining issues:
* type abbreviations
* the lambda binder (this is not a constant, so we can't use
overloading)
* restricted quantifiers
* whether automatically having Unicode stuff in the grammar (even if
disabled) might cause non-Unicode users pain

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.

This check-in mainly fixes a problem with
literals occurring in patterns of TFL-style
definitions. There are a host of other minor
changes as well.

hanges to upgrade EVAL on BIGUNION {}.



M src/parse/term_grammar.sig
M src/pred_set/src/pred_setScript.sml
M src/pred_set/src/pred_setLib.sml
M src/pred_set/src/PFset_conv.sml

Use tDefine to define ITSET.

Type abbreviations now print by default. Where this is "problematic",
as with the set and bag abbreviations, this printing can be turned off
by calling disable_tyabbrev_printing, which takes the abbreviation name
as an argument. (There is also a trace variable controlling tyabbrev
printing globally.)
Bag and set abbreviations are "problematic" because if left on they
do things like
- type_of ``(/\)``;
> val it = ``:bool -> bool set`` : hol_type
and
- type_of ``(+)``;
> val it = ``:num -> num multiset`` : hol_type
This code isn't done yet because it doesn't pick between multiple possibilities
in an intelligent way. The heuristic I want to implement will take the most
specific abbreviation first, and then the most recently asserted if two
are equally specific.

Smoothing out ML code generation in the case of pseudo-constructors
like pred_set$INSERT.

Add a new exported rewrite to pred_set, and use it to prove another
export-worthy rewrite in the theory of containers, namely that
SET_TO_LIST {x} = [x]

Fixing up bugs spotted by Anthony.

Changes having to do with generating ML. System should build again.

Fixing up treatment of "ABSDATATYPE" thingies, where ordinary
constants are treated as datatype constructors in the generatd
ML.

Minor changes and bugfixes to ML code generation. Have renamed
EmitML.exportML to EmitML.emitML, since exportML is used in
SML/NJ to dump the image. Also renamed Globals.exportMLPath
to Globals.emitMLDir (since it's a directory and not a path).

Also fixed bug in code generated for constructors and tuples.

Upgrading EmitML to support records. Lots of associated changes
as well.

The new changes to records have been fixed so that the system
will rebuild without error. Whether the record stuff actually
does what it should, I am still checking. The big record
stuff will have to be checked in Australia, probably, since
I don't really understand it.

Extend the add_listform interface so that the user can specify a printing
"consistency" for the block of list elements. Previously, it was just
assumed that the user always wanted (INCONSISTENT,0). This is the value
now specified in the various places where add_listform is used.

Export more rewrites, and prove a trivial result about complement.

Upgrading Define so that it proves more termination goals.
Generates lex. combinations and tries them out, so gets
some more ordinary recursions. Gets all iterated primitive
recursions. Also has been taught about some operations
on words (so recursion from w to w-1w will terminate,
for example).

Let me know of any bugs/slowdowns, etc.

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.

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.

Added Pigeon Hole Principle (PHP).

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.

Implement and document a new, unambiguous set comprehension syntax.
Only fixes required are to ieeeScript where old style =>-| if-then-else
syntax was nested to extraordinary degree without any parentheses.
Adding parentheses was the only thing required to fix the problem.

Added powerset operator and simple theorems (finiteness, cardinality).
EVAL has been taught about it, etc.

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.

Changed a couple of misleading/annoying names. The type ssdata is now
called ssfrag (to bring it into line with documentation that talks about
simpset fragments), and the constructor SIMPSET is now called SSFRAG.
It never created a simpset, so the latter was a stupid name.

Added theorems BIJ_LINV_BIJ and BIJ_LINV_INV

Added a few more theorems about MIN_SET and MAX_SET.

Getting rid of HTML output on xTheory.sig files.

Trivial change to bound var. names in definitions of BIGUNION and
BIGINTER. Motivated by documenting pred_setTheory in the
Description.

Hacking around to get HTML symbols put in generated `Theory.sig'
files. Allows usual logic symbols (and some set theory symbols)
in the generated html files, see help/HOLindex.html after a
complete build of the system (examine a theory file).

Only symbol not currently dealt with properly is lambda. Also,
I thought I had emptyset sussed, but it stopped working for
some reason ... not a problem since "{}" works just as well,
and may be nicer.

Remove a couple of exported rewrites because they will cause the simplifier
to loop unnecessarily trying to solve an existential problem.

ML code generation for finite_map now added. Also, a whole host
of minor changes and robustifications have been applied.

Exposed EMPTY and INSERT in the signature of the generated ML. This
allows them to be used to build sets, but they still can't be used
to take sets apart by pattern matching.

Minor mods to add error messages in generated ML code. The current
body of generated ML code now builds without any pattern-match
warnings.

Added some theorem-proving to FAIL-based exceptions for partial
set operations (just BINGINTER, I think, which doesn't make sense
in the EMPTY case for finite sets).

ML code now generated from pred_set. Most of the operators can be
handled, but the model is a concrete datatype with constructors
EMPTY and INSERT. Reasons for this choice are discussed in the
code. Also proved some extra theorems.

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.

New treatment of abbreviations. Documentation still to be updated.
Backwards compatibility illustrated in examples/lambda/standardisationScript
and examples/arm6. New techniques and entry-points illustrated in
core distribution and some of the lambda example scripts.

Changing "prove" to store_thm so that the newly added theorems
from Scott actually appear in the theory.

Adding a few theorems. Proved by Scott Owens.

A couple of theorems about SUM_IMAGE, and a new (trivial) rewrite for
GSPEC.

More automatic rewrites.

Useful finite-ness results, including the converse of
"the finite union of finite sets is finite"
giving an equivalence for FINITE (BIGUNION P).

Another very useful rewrite exported.

Export a useful rewrite.

A change to make this proof renaming-independent; I don't see that this
one would have ever worked with the standard kernel.

Add a useful theorem about finiteness of images.

A start on proving some theorems about the action of partitioning a set
according to an equivalence relation. (Joe if you fancy hacking METIS_TAC,
you might look into why it seems to do so miserably on those places in
what I've checked in where PROVE_TAC is used. PROVE_TAC in these places
takes a while to normalise, but having done so proves the goals quite
quickly. METIS starts quickly but doesn't seem to get anywhere.)

Some new theorems; one just an old one recast to be more suitable for
rewriting.

Modify the add_listform function in line with a suggestion of Lockwood
Morris's to provide slightly more flexibility in the way that list forms
are pretty-printed. Previously, the format was fixed as
<left-delimiter> el1 <sep> <a space> el2 <sep> <a space> ...
Now, the spacing is more directly under user-control.

These files needed changing because of the new STRIP_TAC.

Many small changes, most associated with boolification or lifting.

Add a very useful automatic rewrite.

Added a couple of extra rewrite exports.

A proof of Koenig's Lemma, where the notion of a tree being finite is
generalised to the notion of a reachable set being finite.

Prove some useful (trivial) theorems about GSPEC. Also shift definition
of SET_SPEC_ss (simpset for handling x IN {y | ...}) to pred_setTheory
itself (using adjoin_to_theory magic) so that loading pred_setTheory
can automatically install it in srw_ss as the theory loads.
(Preivously, you had to remember to also load pred_setLib.)

Added another useful automatic rewrite.

Realised that my particular application didn't want SUM_SET at all, but
rather something that calculates something that looks a bit like the
sum of the image of a function. E.g., you have a finite set of widgets
and you want to know the sum of their weights. It's not right to
write
SUM_SET (IMAGE weight s)
because this relies on the weight function being injective.

Instead, you now write
SUM_IMAGE weight s
and I can redefine SUM_SET to be equal to SUM_IMAGE I.

Someday I (or anyone else who fancies it) should prove that if f is injective,
then SUM_SET (IMAGE f s) = SUM_IMAGE f s.

Slight clean-up of SUM_SET work. In particular, there's a general
result possible justifying recursion equations that look like:
ITSET f (x INSERT s) b = f x (ITSET f s b)
This is the FOLDR version, as opposed to the FOLDL version, or the
recursing version rather than the accumulator version.
Also define functions to get the minimum and maximum elements of sets
of numbers. The former is just the LEAST quantifier. (Just realised that
perhaps shouldn't even have a new constant for MIN_SET; could do it with
overloading; but then the pretty-printing system would pick one or the
other to be "the way" to print that constant, which could be confusing
too. Dunno.

Proved that the condition on the function being iterated doesn't need to
be quite AC; it can have a weaker condition instead.

More useful (but obvious) theorems about SUM_SET.

Proved that if you give ITSET an associative and commutative operator, then
it gives you nice recursion equations (that don't feature CHOICE and REST).
Used this to define a SUM_SET function that sums the elements of a finite
set of numbers.

Export of more obvious rewrites.

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

Added a couple of obvious rewrites for the stateful rewriter.

Made definition of BIGINTER more consistent with style of definition of
BIGUNION.

Prompted by Konrad's useful change to the AC stuff in the simplifier,
I have "fixed" a long-standing irritation in the associativity theorems
in pred_setTheory: they're the wrong way round. All other associativity
theorems in the system are oriented x _ (y _ z) = (x _ y) _ z, which is
the direction that AC_CONV expects. So, I've put them right. The changes
I had to make in pred_setScript are such that the proofs no longer depend
on any particular orientation, so this could always be changed back without
much grief.
Elsewhere, probability is the only place in the core distribution where
problems arose. There, and in the examples where similar things happened,
I replaced all occurrences of {UNION,INTER}_ASSOC with
GSYM {INTER,UNION}_ASSOC.
I also fixed the m scripts in the examples/miller so that they cause a
stop when they hit an error.
Finally, I changed developers/build-examples to clean up in the miller
directory before building. This is consistent with what is done for all
of the other examples.

* Added a small new theory about fixed points (least, and greatest) and
monotone functions.
* Added an export_rewrites clause to the end of pred_setScript. (No more
having to write SIMP_TAC std_ss [IN_UNION, IN_DELETE, IN_SING,....])
* Added SET_SPEC_CONV to the stateful rewriter and also to the PRED_SET_ss
simpset fragment.
* Added BIGINTER constant to pred_setTheory; companion to BIGUNION.

Added a type abbreviation 'a set = 'a -> bool

Fixed bug in set conversions: the constant IN is no longer defined in
pred_setTheory, but in boolTheory, for some reason.

Also added rudimentary syntax support for sets.

Miscellaneous cosmetic changes.

Added the definition

count n = {m | m < n}

as a canonical n-element set, and proved the obvious theorems.

Removed IN as a constant from pred_set theory now that it's in bool.
Somewhat to my surprise, things built anyway, but it was distracting
seeing the messages complaining about the ambigous grammars and the
overloading resolution. (I shouldn't be surprised of course, this is
the whole point of all the Kananaskis work!)

Added the definition of set complementation (COMPL) and some related theorems.

Removed gratuitous incompatibility with Taupo-6 in type of set_fixity;
its type is now string -> fixity -> unit, rather than
(string * fixity) -> unit.

Changing arithLib to numLib.

Moved to bagLib/containerScript so that I could do some stuff
with bags there.:;

Added ITSET (fold for sets) to pred_setScript. Added a tiny theory
relating sets and lists. Should probably also add bags to this.

Now builds in Kan.0.

Kananaskis compatibility.

Strengthening of UNWIND_FORALL_CONV requires minor alteration to one
proof.

Not sure what this is.

I realised on porting this theory to the companion theory of sets as
their own datatype, that my definition of BIGUNION wasn't abstract
enough. In particular, it assumed the pred_set nature. I fixed the
proof in setScript, and have moved the proof back to pred_set too.
Now all of the new material in both script files is identical.

A couple of new results: BIGUNION (x INSERT S) = x UNION (BIGUNION S)
and that the finite union of finite sets is finite.

A complete induction principle for finite sets. Finite-ness of cross
products completely characterised. Some other minor results.

Added treatment of cross products and big union, and some new finite-ness
theorems (due to Konrad).

Updates due to new pretty-printing support.

Modified to let back old style conditional expressions (given alteration
to parsing code's construction of precedence matrix).

Fixed to bring it up to date with Taupo release 0.
(Changes have come across from parse_branch development.)

Initial revision