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



On Fri, Jun 13, 2008 at 10:38, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> Blast doesn't look like the right tool for this problem.
>
> You can prove it like this:
>
>   lemma
>   "noBot LNil = True" unfolding noBot_def
>     by (simp add: finlsts_rec_LNil)

I had the same thought, but I tried:

    lemma
    "noBot LNil = True" unfolding noBot_def
                        using finlsts_rec_LNil
    by simp

And it failed.  I expected to be able to substitute "using" in Isar
for the "add:" argument to simp.  What is different?

-- 
 Denis





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