Re: [isabelle] Recursion on finite, lazy lists (llists)
On Fri, 13 Jun 2008, Denis Bueno wrote:
> 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?
Automated proof methods like "simp" merely insert the facts being "used"
into the goal before doing their usual business. This means a polymorphic
rule like using finlsts_rec_LNil essentially looses its polymorphism, it
can be instantiated at most once for logical reasons, and the Simplifier
does not instantiate even do that, but ignores it due to schematic type
variables in the goal premises.
In contrast, the "add" method modifier inserts the rule into the
Simplifier context as an independented fact. It is eventually matched
against a redex in the goal, and its types get instantiated as expected.
As a rule of thumb (and a matter of style), the "using" part typically
refers to local things from the very proof, while rules from the library
are specified via extra method modifiers (simp add/del, blast
intro/elim/dest etc.).
Makarius
This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.