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)
On 12 Jun 2008, at 16:37, Denis Bueno wrote:
When ProofGeneral has consumed everything up to "(*here*)", the
proofstate looks like:
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