theory "List-Interleavings" imports Main begin inductive interleave' :: "'a list ⇒ 'a list ⇒ 'a list ⇒ bool" where [simp]: "interleave' [] [] []" | "interleave' xs ys zs ⟹interleave' (x#xs) ys (x#zs)" | "interleave' xs ys zs ⟹interleave' xs (x#ys) (x#zs)" definition interleave :: "'a list ⇒ 'a list ⇒ 'a list set" (infixr "⊗" 64) where "xs ⊗ ys = Collect (interleave' xs ys)" lemma elim_interleave'[pred_set_conv]: "interleave' xs ys zs ⟷ zs ∈ xs ⊗ ys" unfolding interleave_def by simp lemmas interleave_intros[intro?] = interleave'.intros[to_set] lemmas interleave_intros(1)[simp] lemmas interleave_induct[consumes 1, induct set: interleave, case_names Nil left right] = interleave'.induct[to_set] lemmas interleave_cases[consumes 1, cases set: interleave] = interleave'.cases[to_set] lemmas interleave_simps = interleave'.simps[to_set] inductive_cases interleave_ConsE[elim]: "(x#xs) ∈ ys ⊗ zs" inductive_cases interleave_ConsConsE[elim]: "xs ∈ y#ys ⊗ z#zs" inductive_cases interleave_ConsE2[elim]: "xs ∈ x#ys ⊗ zs" inductive_cases interleave_ConsE3[elim]: "xs ∈ ys ⊗ x#zs" lemma interleave_comm: "xs ∈ ys ⊗ zs ⟹ xs ∈ zs ⊗ ys" by (induction rule: interleave_induct) (auto intro: interleave_intros) lemma interleave_Nil1[simp]: "[] ⊗ xs = {xs}" by (induction xs) (auto intro: interleave_intros elim: interleave_cases) lemma interleave_Nil2[simp]: "xs ⊗ [] = {xs}" by (induction xs) (auto intro: interleave_intros elim: interleave_cases) lemma interleave_nil_simp[simp]: "[] ∈ xs ⊗ ys ⟷ xs = [] ∧ ys = []" by (auto elim: interleave_cases) lemma append_interleave: "xs @ ys ∈ xs ⊗ ys" by (induction xs) (auto intro: interleave_intros) lemma interleave_assoc1: "a ∈ xs ⊗ ys ⟹ b ∈ a ⊗ zs ⟹ ∃ c. c ∈ ys ⊗ zs ∧ b ∈ xs ⊗ c" by (induction b arbitrary: a xs ys zs) (simp, fastforce del: interleave_ConsE elim!: interleave_ConsE intro: interleave_intros) lemma interleave_assoc2: "a ∈ ys ⊗ zs ⟹ b ∈ xs ⊗ a ⟹ ∃ c. c ∈ xs ⊗ ys ∧ b ∈ c ⊗ zs" by (induction b arbitrary: a xs ys zs ) (simp, fastforce del: interleave_ConsE elim!: interleave_ConsE intro: interleave_intros) lemma interleave_set: "zs ∈ xs ⊗ ys ⟹ set zs = set xs ∪ set ys" by(induction rule:interleave_induct) auto lemma interleave_tl: "xs ∈ ys ⊗ zs ⟹ tl xs ∈ tl ys ⊗ zs ∨ tl xs ∈ ys ⊗ (tl zs)" by(induction rule:interleave_induct) auto lemma interleave_butlast: "xs ∈ ys ⊗ zs ⟹ butlast xs ∈ butlast ys ⊗ zs ∨ butlast xs ∈ ys ⊗ (butlast zs)" by (induction rule:interleave_induct) (auto intro: interleave_intros) lemma interleave_take: "zs ∈ xs ⊗ ys ⟹ ∃ n⇩1 n⇩2. n = n⇩1 + n⇩2 ∧ take n zs ∈ take n⇩1 xs ⊗ take n⇩2 ys" apply(induction arbitrary: n rule:interleave_induct) apply auto apply arith apply (case_tac n, simp) apply (drule_tac x = nat in meta_spec) apply auto apply (rule_tac x = "Suc n⇩1" in exI) apply (rule_tac x = "n⇩2" in exI) apply (auto intro: interleave_intros)[1] apply (case_tac n, simp) apply (drule_tac x = nat in meta_spec) apply auto apply (rule_tac x = "n⇩1" in exI) apply (rule_tac x = "Suc n⇩2" in exI) apply (auto intro: interleave_intros)[1] done lemma filter_interleave: "xs ∈ ys ⊗ zs ⟹ filter P xs ∈ filter P ys ⊗ filter P zs" by (induction rule: interleave_induct) (auto intro: interleave_intros) lemma interleave_filtered: "xs ∈ interleave (filter P xs) (filter (λx'. ¬ P x') xs)" by (induction xs) (auto intro: interleave_intros) function foo where "foo [] [] = undefined" | "foo xs [] = undefined" | "foo [] ys = undefined" | "foo (x#xs) (y#ys) = undefined (foo xs (y#ys)) (foo (x#xs) ys)" by pat_completeness auto termination by lexicographic_order lemmas list_induct2'' = foo.induct[case_names NilNil ConsNil NilCons ConsCons] lemma interleave_filter: assumes "xs ∈ filter P ys ⊗ filter P zs" obtains xs' where "xs' ∈ ys ⊗ zs" and "xs = filter P xs'" using assms apply atomize_elim proof(induction ys zs arbitrary: xs rule: list_induct2'') case NilNil thus ?case by simp next case (ConsNil ys xs) thus ?case by auto next case (NilCons zs xs) thus ?case by auto next case (ConsCons y ys z zs xs) show ?case proof(cases "P y") case False with ConsCons.prems(1) have "xs ∈ filter P ys ⊗ filter P (z#zs)" by simp from ConsCons.IH(1)[OF this] obtain xs' where "xs' ∈ ys ⊗ (z # zs)" "xs = filter P xs'" by auto hence "y#xs' ∈ y#ys ⊗ z#zs" and "xs = filter P (y#xs')" using False by (auto intro: interleave_intros) thus ?thesis by blast next case True show ?thesis proof(cases "P z") case False with ConsCons.prems(1) have "xs ∈ filter P (y#ys) ⊗ filter P zs" by simp from ConsCons.IH(2)[OF this] obtain xs' where "xs' ∈ y#ys ⊗ zs" "xs = filter P xs'" by auto hence "z#xs' ∈ y#ys ⊗ z#zs" and "xs = filter P (z#xs')" using False by (auto intro: interleave_intros) thus ?thesis by blast next case True from ConsCons.prems(1) `P y` `P z` have "xs ∈ y # filter P ys ⊗ z # filter P zs" by simp thus ?thesis proof(rule interleave_ConsConsE) fix xs' assume "xs = y # xs'" and "xs' ∈ interleave (filter P ys) (z # filter P zs)" hence "xs' ∈ filter P ys ⊗ filter P (z#zs)" using `P z` by simp from ConsCons.IH(1)[OF this] obtain xs'' where "xs'' ∈ ys ⊗ (z # zs)" and "xs' = filter P xs''" by auto hence "y#xs'' ∈ y#ys ⊗ z#zs" and "y#xs' = filter P (y#xs'')" using `P y` by (auto intro: interleave_intros) thus ?thesis using `xs = _` by blast next fix xs' assume "xs = z # xs'" and "xs' ∈ y # filter P ys ⊗ filter P zs" hence "xs' ∈ filter P (y#ys) ⊗ filter P zs" using `P y` by simp from ConsCons.IH(2)[OF this] obtain xs'' where "xs'' ∈ y#ys ⊗ zs" and "xs' = filter P xs''" by auto hence "z#xs'' ∈ y#ys ⊗ z#zs" and "z#xs' = filter P (z#xs'')" using `P z` by (auto intro: interleave_intros) thus ?thesis using `xs = _` by blast qed qed qed qed end