*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Proofs using inductively defined sets.*From*: Brian Huffman <brianh at csee.ogi.edu>*Date*: Thu, 5 Oct 2006 15:47:14 -0700*Cc*: D Mulligan <s0346804 at sms.ed.ac.uk>*In-reply-to*: <20061004125718.s81oqpor480sos0s@www.sms.ed.ac.uk>*References*: <20061004125718.s81oqpor480sos0s@www.sms.ed.ac.uk>*User-agent*: KMail/1.8

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! *)

**References**:**[isabelle] Proofs using inductively defined sets.***From:*D Mulligan

- Previous by Date: [isabelle] Post-doctoral position on verification for domain-specific languages
- Next by Date: [isabelle] FMCAD 2006 Workshop on Pre- and Post-Silicon Verification Call For Participation
- Previous by Thread: Re: [isabelle] Proofs using inductively defined sets.
- Next by Thread: [isabelle] Post-doctoral position on verification for domain-specific languages
- Cl-isabelle-users October 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list