Проверка свойств сгенерированных списков

Question

Моя цель - доказать свойства списков, содержащих сгенерированные шаблоны.В первом примере шаблон представляет собой просто последовательность 0, и лемма pattern_0_len доказывает, что длина сгенерированного списка действительно равна параметру длины функции генератора.

theory pattern_0
imports Main
begin

fun pattern_0 :: "nat ⇒ nat list" where
"pattern_0 0 = []" |
"pattern_0 len =  (pattern_0 (len - 1)) @ [0]"

lemma pattern_0_len [simp]: "length (pattern_0 lng) = lng"
apply(induction lng)
apply(simp)
apply(auto)
done

end

Во втором примере генератор создаетпоследовательность из 0, 1 предметов.

theory pattern_0_1
imports Main
begin

fun pattern_0_1 :: "nat ⇒ nat ⇒ nat list" where
"pattern_0_1 0 item  = []" |
"pattern_0_1 len item =  (pattern_0_1 (len - 1) (if item = 0 then 1 else 0)) @ [item]"

lemma pattern_0_1_len [simp]: "length (pattern_0_1 lng item) = lng"
apply(induction lng)
apply(simp)
apply(auto)
done

end

К сожалению, pattern_0_1_len не доказывает (после простого цель - именно шаг индукции), и я хотел бы понять причину, почему нет.Присутствие параметра item «сбивает с толку» Изабель?Что можно сделать в этой ситуации, желательно не сообщая ничего о том, как генерируется шаблон?

Answer 1

Дополнительный параметр действительно является проблемой.Например, рассмотрим эту подцель:

1. ⋀lng. length (pattern_0_1 lng 0) = lng ⟹ item = 0 ⟹ length (pattern_0_1 lng (Suc 0)) = lng

Вы видите, что индукционная гипотеза применима только для нуля, но она нужна для одного.

Исправление простое:

apply(induction lng arbitrary: item)

Это инструктирует индукционный метод сначала обобщить переменную item.Затем гипотеза об индукции становится более широко применимой.