Я хочу доказать следующее
lemma
fixes pi :: "'a path" and T :: "'a ts"
shows "valid_path T pi s ⟹ ∀ op ∈ set pi. valid_operator T op"
по индукции на pi, где
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))
, а путь - это просто синоним типа для списка операторов. Другие определения не должны играть роль для доказательства.
Базовый случай работает нормально.
Проблема заключается в том, что неофициально для индуктивного шага, где pi = (x # xs) Я предполагаю, что
if valid_path T xs s
then ∀ op ∈ set xs. valid_operator T op
и я должен показать, что это подразумевает
if valid_path T (x#xs) s
then ∀ op ∈ set (x#xs). valid_operator T op
Я могу использовать здесь определение valid_path, так что это последнее выражение эквивалентно
if valid_path T (xs) (effect x s)
then ∀ op ∈ set (x#xs). valid_operator T op
Если бы я мог использовать гипотезу индукции на valid_path T (xs) (effect x s), я бы сделал.
Я бы не смог, так как гипотеза верна только для valid_path T (xs) s вместо valid_path T xs (effect x s).
Но это на самом деле не имеет значения, так как предикат того, что оператор if вообще не зависит от s!
Но Изабель не знает этого, поэтому она жалуется.
Как я могу сделать так, чтобы я мог применить индуктивную гипотезу к valid_path T (xs) (effect x s)? У меня есть ощущение, что я должен сделать утверждение более общим, чтобы я мог использовать гипотезу в доказательстве, но я не знаю, как.