Simple updates for compatibility with KG

Now loads the theory "Let". Could add it to FOL, but this appears to

be incompatible with CCL.

be incompatible with CCL.

HOL.thy:

"@" is no longer introduced as a "binder" but has its own explicit

translation rule "@x.b" == "Eps(%x.b)". If x is a proper pattern, further

translation rules for abstractions with patterns take care of the rest. This

is very modular and avoids problems with "binders" such as "!" mentioned

below.

let now allows pttrn (let (x,y) = t in u) instead of just idt (let x = t in u)

Set.thy:

UN, INT, ALL, EX, etc all use "pttrn" instead of idt. Same change as for "@"

above, except that "@" was a "binder" originally.

Prod.thy:

Added new syntax for pttrn which allows arbitrarily nested tuples. Two

translation rules take care of %pttrn. Unfortunately they cannot be

reversed. Hence a little ML-code is used as well.

Note that now "! (x,y). ..." is syntactically valid but leads to a

translation error. This is because "!" is introduced as a "binder" which

means that its translation into lambda-terms is not done by a rewrite rule

(aka macro) but by some fixed ML-code which comes after the rewriting stage

and does not know how to handle patterns. This looks like a minor blemish

since patterns in unbounded quantifiers are not that useful (well, except

maybe in unique existence ...). Ideally, there should be two syntactic

categories:

idts, as we know and love it, which does not admit patterns.

patterns, which is what idts has become now.

There is one more point where patterns are now allowed but don't make sense:

{e | idts . P}

where idts is the list of local variables.

Univ.thy: converted the defs for <++> and <**> into pattern form. It worked

perfectly.

"@" is no longer introduced as a "binder" but has its own explicit

translation rule "@x.b" == "Eps(%x.b)". If x is a proper pattern, further

translation rules for abstractions with patterns take care of the rest. This

is very modular and avoids problems with "binders" such as "!" mentioned

below.

let now allows pttrn (let (x,y) = t in u) instead of just idt (let x = t in u)

Set.thy:

UN, INT, ALL, EX, etc all use "pttrn" instead of idt. Same change as for "@"

above, except that "@" was a "binder" originally.

Prod.thy:

Added new syntax for pttrn which allows arbitrarily nested tuples. Two

translation rules take care of %pttrn. Unfortunately they cannot be

reversed. Hence a little ML-code is used as well.

Note that now "! (x,y). ..." is syntactically valid but leads to a

translation error. This is because "!" is introduced as a "binder" which

means that its translation into lambda-terms is not done by a rewrite rule

(aka macro) but by some fixed ML-code which comes after the rewriting stage

and does not know how to handle patterns. This looks like a minor blemish

since patterns in unbounded quantifiers are not that useful (well, except

maybe in unique existence ...). Ideally, there should be two syntactic

categories:

idts, as we know and love it, which does not admit patterns.

patterns, which is what idts has become now.

There is one more point where patterns are now allowed but don't make sense:

{e | idts . P}

where idts is the list of local variables.

Univ.thy: converted the defs for <++> and <**> into pattern form. It worked

perfectly.

I have modified the grammar for idts (sequences of identifiers with optional

type annotations). idts are generally used as in abstractions, be it

lambda-abstraction or quantifiers. It now has roughly the form

idts = pttrn*

pttrn = idt

where pttrn is a new nonterminal (type) not used anywhere else.

This means that the Pure syntax for idts is in fact unchanged.

The point is that the new nontermianl pttrn allows later extensions of this

syntax. (See, for example, HOL/Prod.thy).

The name idts is not quite accurate any longer and may become downright

confusing once pttrn has been extended. Something should be done about this,

in particular wrt to the manual.

type annotations). idts are generally used as in abstractions, be it

lambda-abstraction or quantifiers. It now has roughly the form

idts = pttrn*

pttrn = idt

where pttrn is a new nonterminal (type) not used anywhere else.

This means that the Pure syntax for idts is in fact unchanged.

The point is that the new nontermianl pttrn allows later extensions of this

syntax. (See, for example, HOL/Prod.thy).

The name idts is not quite accurate any longer and may become downright

confusing once pttrn has been extended. Something should be done about this,

in particular wrt to the manual.

Fixed old bug in the simplifier. Term to be simplified now carries around its

maxidx. Needed for renaming rewrite or congruence rules. maxidx should be ~1

in most cases (ie no Vars), hence reasonable overhead.

maxidx. Needed for renaming rewrite or congruence rules. maxidx should be ~1

in most cases (ie no Vars), hence reasonable overhead.