[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

[Brian Huffman]

On Thu, Aug 25, 2011 at 1:45 PM, Florian Haftmann
<florian.haftmann at informatik.tu-muenchen.de> wrote:
> HOL-Hoare_Parallel FAILED

> Also Hoare_Parallel is non-terminating.

I have a patch for this one:

http://isabelle.in.tum.de/repos/isabelle/rev/5e681762d538

Once this changeset gets merged into the isabelle_set repo,
Hoare_Parallel should start working.

Here's what happened: After a "clarify" step in a proof script,
Isabelle yields a variable called "xb" (renamed from "x" to avoid
clashes with pre-existing "x" and "xa"), while Isabelle_set calls the
same variable "i". It turns out that the Isabelle_set is actually
doing the right thing here. There is a goal of the form "x : (INT i:A.
B i))", and clarify applies the rule INT_I. In Isabelle_set, the new
variable name is inherited from the bound variable "i" in the goal.
But in the current version, the subgoal ends up in the eta-expanded
form "x : (%a. (INT i:A. B i) a)" and the name "i" doesn't get used.

To summarize: eta-expansion is a problem. Eta-expansion seems to
happen with induction (either from "induct" or "rule"), although the
"eta-contract" pretty-printing option tries to prevent people from
noticing (why does this option exist?!?) Switching to a separate set
type greatly reduces the number of opportunities for unwanted
eta-expansion.

- Brian