[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.