Re: [isabelle] Recursion on finite, lazy lists (llists)

Blast doesn't look like the right tool for this problem.

You can prove it like this:

   "noBot LNil = True" unfolding noBot_def
     by (simp add: finlsts_rec_LNil)

Larry Paulson

On 12 Jun 2008, at 16:37, Denis Bueno wrote:

When ProofGeneral has consumed everything up to "(*here*)", the
proofstate looks like:

   using this:
     finlsts_rec ?c ?d LNil = ?c

   goal (1 subgoal):
    1. finlsts_rec True (%s r b. b & s ~= BottomState) LNil = True

This looks like it can be proved directly by unification.  Consuming
the blast does not prove the theorem, even after a long time.

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