I want to prove the following
lemma
fixes pi :: "'a path" and T :: "'a ts"
shows "valid_path T pi s ⟹ ∀ op ∈ set pi. valid_operator T op"
by induction on pi where
fun valid_path :: "'a ts ⇒ 'a path ⇒ 'a state ⇒ bool" where
"valid_path T [] s = True" |
"valid_path T (op#ops) s = (valid_operator T op ∧ valid_path T ops (effect op s))
and path is just a type synonym for an operator list. The other definitions should not play a role for the proof.
The base case works fine.
The problem is that, informally, for the inductive step where pi = (x # xs) I'm assuming that
if valid_path T xs s
then ∀ op ∈ set xs. valid_operator T op
and I must show that this implies
if valid_path T (x#xs) s
then ∀ op ∈ set (x#xs). valid_operator T op
I can use the definition of valid_path here, so this last expression is equivalent to
if valid_path T (xs) (effect x s)
then ∀ op ∈ set (x#xs). valid_operator T op
If I could be able to use the induction hypothesis on valid_path T (xs) (effect x s) I would be done.
I can't since the hypothesis only holds for valid_path T (xs) s instead of valid_path T xs (effect x s).
But this does not really matter since the predicate of that if statement does not depend on s at all!
But Isabelle does not know that so it complains.
How can I make it such that I can apply the inductive hypothesis on valid_path T (xs) (effect x s)?
I have a feeling that I have to make the claim more general, so that I can use the hypothesis on the proof, but I don't know how.
It is very common that you have to generalize some terms in an induction. Use the keyword arbitrary in the induct method.
proof (induct pi arbitrary: s)
This is explained in Chapter 2.4 of Programming and Proving in Isabelle/HOL.