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
Description: Binary data