Re: [isabelle] Strange eta-expansion on induction

> As Tobias points out, the Pure Isabelle system conceptually works modulo 
> eta (and beta and alpha) conversion -- although there are well known 
> traps.  So to continue the thread, I would also like to see the other part 
> -- the proof tool by Peter that fails here.

It's no custom "proof tool" involved here. My setting is roughly like

I have assertions of type "heap => addr set => bool", and hoare-tripels
of type "assertion => program => assertion => bool" (syntax: {P} S {Q})

I defined the assertion 
  definition [simp]: "false h as == False"

Moreover, I have a rule 
  lemma [simp]: "{false} S {Q}"

The proof that fails has the form:
  lemma "{is_list xs p} S Q" proof (induct xs arbitrary: p)
    case Nil show ?case by (cases p, simp_all)

Here, depending on the case for p, "is_list [] p" simplifies to false,
which is then simplified to \lambda _ _. False, before the rule for
{false} S {Q} is applied.

So, if I have to expect eta-expansion at any point, I have to add
additional rules to the simpset to make it confluent again. This
certainly works, but may blow up the simpset.

Just as a remark: The simpset setup from the standard library has such
problems, too --- for example there is id_apply, that happily simplifies
"%x. id x" to "%x. x", but not "id" (I already had problems with that).


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.