# [isabelle] Proofs using inductively defined sets.

```Hi,
```
I've been formulating some Prolog relations in Isabelle using inductively defined sets. I've managed to prove some theorems about relations that are defined entirely within themselves (i.e. plus), but when I try to prove theorems about relations defined in terms of other relations, for example the reverse of a list, defined in terms of itself and 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 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)+
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 apply reverse_inductive.notnil. Is anybody able to offer any advice as to how I would go about proving this theorem?
```
```
Please note, I'm not using the Isar proof style for a reason. For your convenience 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
```

Attachment: PrologInductiveSets.thy
Description: Binary data

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