o7 (Feb 05 2025 at 15:36): o7 (Feb 05 2025 at 15:36):I am trying to prove the set_shuffles1 lemma which uses the shuffle_map function. I am able to prove the same lemma using the accumulator version of the function (shuffles and shuffles') but I cannot see how to get around the map functions when proving the inductive subgoals, nor come up with a stronger lemma that will help with this. Could I please have some advice on this?
theory Sample
imports Main
begin
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 []"
fun shuffles_map :: "'a list ⇒ 'a list ⇒ 'a list list" where
"shuffles_map xs [] = [xs]"
| "shuffles_map [] ys = [ys]"
| "shuffles_map (x#xs) (y#ys) = map (λxs. x # xs) (shuffles_map xs (y#ys)) @ map (λys. y # ys) (shuffles_map (x#xs) ys)"
lemma set_shuffles': "zs ∈ set (shuffles' xs ys ss) ⟹ set zs = set xs ∪ set ys ∪ set ss"
apply (induct xs ys ss rule: shuffles'.induct)
apply auto
done
lemma set_shuffles: "zs ∈ set (shuffles xs ys) ⟹ set zs = set xs ∪ set ys"
apply (auto simp: set_shuffles')
done
lemma l2: "shuffles_map [] ys = [ys]"
by (metis shuffles_map.simps(1) shuffles_map.simps(2) list.exhaust)
lemma set_shuffles1: "zs ∈ set (shuffles_map xs ys) ⟹ set zs = set xs ∪ set ys"
apply (induct ys xs rule: shuffles_map.induct)
apply (auto simp: l2 map_def)
end
Your zs parameter changes during the induction, so you need to generalize it:
lemma set_shuffles1: "zs ∈ set (shuffles_map xs ys) ⟹ set zs = set xs ∪ set ys"
by (induct xs ys arbitrary: zs rule: shuffles_map.induct) auto
Last updated: Mar 09 2025 at 12:28 UTC