Re: [isabelle] Proofs using inductively defined sets.
I think you will also need a lemma:
"\<lbrakk> append r [h] l; reverse r t \<rbrakk> \<Longrightarrow>
reverse l (h#t)"
This is the opposite case of your reverse definition. With this you
should be able to prove:
"\<exists>l'.(reverse l l') \<and> (reverse l' l)"
apply(rule exE) (* the exE step you mentioned: for the result of
append in the definition of reverse *)
apply (rule ex_append)
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.
D Mulligan wrote:
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:
reverse_inductive :: "('a list * 'a list) set"
reverse :: "'a list => 'a list => bool"
"reverse l r" == "(l, r) \<in> reverse_inductive"
nil [intro!]: "reverse  "
notnil [intro!]: "(append r [h] a) /\ (reverse t r) ==> (reverse
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:
"\<exists>l'.(reverse l l') /\ (reverse l' l)"
apply(rule exE[OF ex_append])
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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and