*To*: D Mulligan <s0346804 at sms.ed.ac.uk>*Subject*: Re: [isabelle] Proofs using inductively defined sets.*From*: Lucas Dixon <ldixon at inf.ed.ac.uk>*Date*: Thu, 05 Oct 2006 15:12:49 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <20061004125718.s81oqpor480sos0s@www.sms.ed.ac.uk>*References*: <20061004125718.s81oqpor480sos0s@www.sms.ed.ac.uk>*User-agent*: Thunderbird 1.5.0.7 (Macintosh/20060909)

I think you will also need a lemma: theorem reverse_append2:

sorry

theorem reverse_reverse_l: "\<exists>l'.(reverse l l') \<and> (reverse l' l)" apply(induct_tac l) apply(rule exI) apply(rule conjI) apply(rule reverse_inductive.nil)+ apply(erule exE) apply(erule conjE)

defer apply(rule exI) apply(rule conjI) apply(rule reverse_inductive.notnil) apply(rule conjI) defer apply assumption apply(rule reverse_append2) defer apply assumption defer apply assumption apply assumption apply (rule ex_append) done

best, lucas D Mulligan wrote:

Hi,I've been formulating some Prolog relations in Isabelle usinginductively defined sets. I've managed to prove some theorems aboutrelations that are defined entirely within themselves (i.e. plus), butwhen I try to prove theorems about relations defined in terms of otherrelations, for example the reverse of a list, defined in terms of itselfand append, I hit a wall. My reverse definition is below:consts reverse_inductive :: "('a list * 'a list) set" syntax reverse :: "'a list => 'a list => bool" translations "reverse l r" == "(l, r) \<in> reverse_inductive" inductive reverse_inductive intros nil [intro!]: "reverse [] []"notnil [intro!]: "(append r [h] a) /\ (reverse t r) ==> (reverse(h#t) a)"I'm attempting to prove that the reverse of a reverse of a list is thesame list. I have a lemma that states that states \<exists>c. append ab 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 theproof 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)+ apply(rule exE[OF ex_append]) apply(rule exI) apply(erule exE) apply(erule conjE) apply(rule conjI) apply(rule reverse_inductive.notnil) apply(rule conjI) apply(assumption) sorry (* Stuck! *)The problem (as I see it) is in the step case when I applyreverse_inductive.notnil. Is anybody able to offer any advice as to howI would go about proving this theorem?Please note, I'm not using the Isar proof style for a reason. For yourconvenience I've attached a theory file with my relations and proofs in(scroll to the bottom for the relevant proof attempt).Many thanks for any help offered, Dominic Mulligan

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

- Previous by Date: [isabelle] Proofs using inductively defined sets.
- Next by Date: [isabelle] Post-doctoral position on verification for domain-specific languages
- Previous by Thread: [isabelle] Proofs using inductively defined sets.
- Next by Thread: Re: [isabelle] Proofs using inductively defined sets.
- 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