*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Proofs using inductively defined sets.*From*: D Mulligan <s0346804 at sms.ed.ac.uk>*Date*: Wed, 04 Oct 2006 12:57:18 +0100*User-agent*: Internet Messaging Program (IMP) H3 (4.0.4)

Hi,

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 [] []"

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

Many thanks for any help offered, Dominic Mulligan

**Attachment:
PrologInductiveSets.thy**

**Follow-Ups**:**Re: [isabelle] Proofs using inductively defined sets.***From:*Lucas Dixon

**Re: [isabelle] Proofs using inductively defined sets.***From:*Brian Huffman

- Previous by Date: Re: [isabelle] List construction
- Next by Date: Re: [isabelle] Proofs using inductively defined sets.
- Previous by Thread: Re: [isabelle] List construction
- 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