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.