o7 (Feb 04 2025 at 05:10): o7 (Feb 04 2025 at 05:10):I have the following function and lemma:
fun shuffles' :: "'a list ⇒ 'a list ⇒ 'a list ⇒ 'a list list" where
"shuffles' [] ys s = [s @ ys]" |
"shuffles' xs [] s = [s @ xs]" |
"shuffles' (x#xs) (y#ys) s = shuffles' xs (y#ys) (s @ [x]) @ shuffles' (x#xs) ys (s @ [y])"
fun shuffles :: "'a list ⇒ 'a list ⇒ 'a list list" where
"shuffles xs ys = shuffles' xs ys []"
lemma l13: "zs ∈ set (shuffles' xs ys ss) ⟹ length zs = length xs + length ys + length ss"
apply (induct xs arbitrary: ys ss)
apply auto
sorry
theorem "zs ∈ set (shuffles xs ys) ⟹ length zs = length xs + length ys"
apply (induct xs arbitrary: ys)
apply (auto simp: l13)
done
Unfortunately I am struggling to find an intermediate lemma that will help prove l13. I have tried using case_tac ys but it only seems that the proof would only continue expanding in size. Could I please have some help with this?
Mathias Fleury (Feb 04 2025 at 06:01):When you do an induction over the parameter of a function, you should use the induction principle from the function
apply (induct xs ys ss rule: shuffles'.induct)
Last updated: Mar 09 2025 at 12:28 UTC