# Re: [isabelle] Proofs using inductively defined sets.

```Hi Dominic,

Since you do not instantiate variables in your rule applications, your proof
state often contains schematic variables that are instantiated later as
needed. (These are the ones written with a leading question mark.)

You need to pay attention to the parameters that these schematic variables
have. In particular, a schematic variable can not be instantiated to a term
that contains variables that were created after the schematic variable was.

In your proof below, "rule exE[OF ex_append]" introduces two schematic
variables, and afterward "erule exE" obtains a new variable l'. Later, you
would like to instantiate the schematic variable to l' but you can't, because
l' did not exist when the schematic variable was created. You might want to
try putting "erule exE" a few steps earlier.

Having unbound schematic variables in your proof state is often very
confusing. I would recommend instantiating your rules as you apply them
instead, i.e. use something like (rule_tac x="list" in exI) instead of just
(rule exI).

Hope this helps.
- Brian

On Wednesday 04 October 2006 04:57, D Mulligan wrote:
...
> I'm attempting to prove that the reverse of a reverse of a list is the
> same list.  I have a lemma that states that states \<exists>c. append a
> b c.  It's been suggested to me that I use this lemma with rule exE[OF
> ..] in the proof, but no matter how I attempt to use it I cannot get
> the proof to go through.
>
> An attempt at the proof is included below:
>
>    theorem reverse_reverse_l:
>      "\<exists>l'.(reverse l l') /\ (reverse l' l)"
>      apply(induct_tac l)
>      apply(rule exI)
>      apply(rule conjI)
>      apply(rule reverse_inductive.nil)+
-- variables from induction rule: a, list
>      apply(rule exE[OF ex_append])
-- introduces schematic variables parameterized on a, list
-- obtains variable x
>      apply(rule exI)
-- introduces schematic variable parameterized on a, list, x
>      apply(erule exE)
-- obtains variable l'
>      apply(erule conjE)
>      apply(rule conjI)
>      apply(rule reverse_inductive.notnil)
>      apply(rule conjI)
>      apply(assumption)
-- can't apply assumption again because schematic variable
-- must not depend on l'
>        sorry (* Stuck! *)

```

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