Theory List-Interleavings

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