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

[Makarius <makarius at sketis.net>]

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