Re: [isabelle] Proofs using inductively defined sets.



I think you will also need a lemma:

  theorem reverse_append2:
"\<lbrakk> append r [h] l; reverse r t \<rbrakk> \<Longrightarrow> reverse l (h#t)"
    sorry

This is the opposite case of your reverse definition. With this you should be able to prove:

  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)
apply(rule exE) (* the exE step you mentioned: for the result of append in the definition of reverse *)
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

I'm not sure if this is the most efficient proof... the structure of the proof is hard to see in apply style. But with this you can at least see the incremental instantiation of the introduced meta-variables.

best,
lucas

D Mulligan wrote:
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






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