My aim is to prove properties of lists containing generated patterns. In the first example the pattern is simply a sequence of 0s and lemma pattern_0_len proves that the length of the generated list indeed equals to the length parameter of the generator function.
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
In the second example the generator produces a sequence of 0, 1 items.
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
Unfortunately, pattern_0_1_len does not prove (after simp the goal is exactly the induction step) and I'd like to understand the reason why not. Is it the presence of the item parameter that 'confuses' Isabelle? What can be done in this situation, preferably without declaring anything about how the pattern is generated?
The additional parameter is indeed the problem. For example, consider this subgoal:
1. ⋀lng. length (pattern_0_1 lng 0) = lng ⟹ item = 0 ⟹ length (pattern_0_1 lng (Suc 0)) = lng
You see that the induction hypothesis is only applicable for zero, but you need it for one.
The fix is simple:
apply(induction lng arbitrary: item)
This instructs the induction method to first generalize the variable item. Then, the induction hypothesis becomes more broadly applicable.