Theory Interleave

(*  Title:       Conflict analysis/List Interleaving Operator
    Author:      Peter Lammich <peter.lammich@uni-muenster.de>
    Maintainer:  Peter Lammich <peter.lammich@uni-muenster.de>
*)
section "List Interleaving Operator"
theory Interleave
imports Main Misc
begin
text_raw ‹\label{thy:Interleave}›

text ‹
  This theory defines an operator to return the set of all possible interleavings of two lists.
›

(*
  Is ⨂-operator needed ?
    Should we better do a reformulation of ⊗ on sets of lists, to get an associative, commutative operator with identity (ACI ?) ?
*)

subsection "Definitions"

subsubsection "Prepend and concatenate lifted to sets"

definition list_set_cons :: "'a ⇒ 'a list set ⇒ 'a list set" (infixr ‹⋅› 65)
  where [simp]: "a⋅S = (#) a ` S"

definition list_set_append :: "'a list ⇒ 'a list set ⇒ 'a list set" (infixr ‹⊙› 65)
  where [simp]: "a⊙S = (@) a ` S"

subsubsection "The interleaving operator"

function
  interleave :: "'a list ⇒ 'a list ⇒ 'a list set" (infixr ‹⊗› 64)
where
  "[]⊗b = {b}"
  | "a⊗[] = {a}"
  | "a#l ⊗ b#r = ((a⋅(l ⊗ b#r)) ∪ (b⋅(a#l ⊗ r)))"
by pat_completeness auto
termination by lexicographic_order


subsection "Properties"

subsubsection "Lifted prepend and concatenate operators"
lemma cons_set_cons_eq: "a#l ∈ b⋅S = (a=b & l∈S)"
  by auto
lemma append_set_append_eq: "⟦length a = length b⟧ ⟹ a@l ∈ b⊙S = (a=b & l∈S)"
  by auto

lemma list_set_cons_cases[cases set]: "⟦w∈a⋅S; !!w'. ⟦ w=a#w'; w'∈S ⟧ ⟹ P⟧ ⟹ P"
  by auto
lemma list_set_append_cases[cases set]: "⟦w∈a⊙S; !!w'. ⟦ w=a@w'; w'∈S ⟧ ⟹ P⟧ ⟹ P"
  by auto

subsubsection "Standard simplification-, introduction-, elimination-, and induction rules"
lemma interleave_cons1: "l ∈ a⊗b ⟹ x#l ∈ x#a ⊗ b"
  apply(case_tac b)
  apply(auto)
done
  
lemma interleave_cons2: "l ∈ a⊗b ⟹ x#l ∈ a ⊗ x#b"
  apply(case_tac a)
  apply(auto)
done

lemmas interleave_cons = interleave_cons1 interleave_cons2


lemma interleave_empty[simp]: "[]∈a⊗b = (a=[] & b=[])"
  apply(case_tac a)
  apply(case_tac b)
  apply(simp)
  apply(simp)
  apply(case_tac b)
  apply(auto)
done

(* TODO: Is this wise as default simp ?*)
lemma interleave_length[rule_format, simp]: "ALL x : a⊗b . length x = length a + length b"
  apply(induct rule: interleave.induct)
  apply(auto)
done

lemma interleave_same[simp]: "y∈l⊗y = (l=[])"
  apply (rule iffI)
  apply (subgoal_tac "length y = length l + length y")
  apply (simp del: interleave_length)
  apply (erule interleave_length)
  apply simp
done

lemma interleave_comm[simp]: "a⊗b = b⊗a" (is "?P f a b")
  apply(induct rule: interleave.induct)
  apply(auto)
done

lemma interleave_cont_conc[rule_format, simp]: "ALL b . a@b ∈ a⊗b"
  apply(induct_tac a)
  apply(auto simp add: interleave_cons)
done

lemma interleave_cont_rev_conc[simp]: "b@a ∈ a⊗b"
  apply (subgoal_tac "b@a ∈ b⊗a")
  apply(simp)
  apply(simp only: interleave_cont_conc)
done

lemma interleave_not_empty: "a⊗b ~= {}" 
  apply(induct rule: interleave.induct)
  apply(auto)
done

lemma cons_interleave_split: "⟦a#l ∈ l1⊗l2⟧ ⟹ (EX lh . l1=a#lh & l ∈ lh⊗l2 | l2=a#lh & l ∈ l1⊗lh )"
  apply(case_tac l1)
  apply(auto)
  apply(case_tac l2)
  apply(auto)
done

lemma cons_interleave_cases[cases set, case_names left right]: "⟦a#l ∈ l1⊗l2; !!lh . ⟦l1=a#lh; l ∈ lh⊗l2⟧ ⟹ P; !!lh. ⟦l2=a#lh; l ∈ l1⊗lh⟧ ⟹ P⟧ ⟹ P"
  by (blast dest: cons_interleave_split)

lemma interleave_cases[cases set, case_names empty left right]: "⟦l∈l1⊗l2; ⟦ l=[]; l1=[]; l2=[] ⟧ ⟹ P; !!a l' l1'. ⟦l=a#l'; l1=a#l1'; l'∈l1'⊗l2⟧ ⟹ P; !!a l' l2'. ⟦l=a#l'; l2=a#l2'; l'∈l1⊗l2'⟧ ⟹ P ⟧ ⟹ P"
  apply (cases l)
  apply (simp)
  apply simp
  apply (erule cons_interleave_cases)
  apply simp_all
  done

lemma interleave_elem_induct[induct set, case_names empty left right]: 
  "!!w1 w2. ⟦ w∈w1⊗w2; P [] [] []; !!e w w1 w2. ⟦ P w w1 w2; w∈w1⊗w2 ⟧ ⟹ P (e#w) (e#w1) w2; !!e w w1 w2. ⟦ P w w1 w2; w∈w1⊗w2 ⟧ ⟹ P (e#w) w1 (e#w2) ⟧ ⟹ P w w1 w2"
  by (induct w) (auto elim!: cons_interleave_cases intro!: interleave_cons)

lemma interleave_rev_cons1[rule_format]: "ALL a b . l ∈ a⊗b ⟶ l@[x] ∈ a@[x] ⊗ b" (is "?P l") 
proof (induct l)
  case Nil show ?case by (simp)
  case (Cons e l)
    assume IH[rule_format]: "?P l"
    show "?P (e#l)" proof (intro allI impI)
      fix a b
      assume "e#l ∈ a⊗b"
      then obtain c where SPLIT: "a=e#c & l∈c⊗b | b=e#c & l∈a⊗c" by (blast dest: cons_interleave_split)
      with IH have "a=e#c & l@[x]∈c@[x]⊗b | b=e#c & l@[x]∈a@[x]⊗c" by auto
      hence "a=e#c & e#l@[x]∈e#c@[x]⊗b | b=e#c & e#l@[x]∈a@[x]⊗e#c" by (auto simp add: interleave_cons)
      thus "(e#l)@[x]∈a@[x]⊗b" by auto
    qed
qed

corollary interleave_rev_cons2: "l ∈ a⊗b ⟹ l@[x] ∈ a ⊗ b@[x]"
proof -
  assume "l ∈ a⊗b"
  hence "l∈b⊗a" by auto
  hence "l@[x] ∈ b@[x] ⊗ a" by (blast dest: interleave_rev_cons1)
  thus ?thesis by auto
qed

lemmas interleave_rev_cons = interleave_rev_cons1 interleave_rev_cons2


subsubsection "Interleaving and list concatenation"

lemma interleave_append1: "⟦l ∈ a⊗b⟧ ⟹ x@l ∈ x@a ⊗ b" proof -
  have "ALL l a b . l ∈ a⊗b ⟶ x@l ∈ x@a ⊗ b" (is "?P x") proof (induct x)
    show "?P []" by simp
  next
    fix e
    fix x::"'a list"
    assume IH: "?P x"
    show "?P (e#x)" proof (intro impI allI)
      fix l::"'a list" 
      fix a b
      assume "l ∈ a ⊗ b"
      with IH have "x@l ∈ x@a ⊗ b" by auto
      with interleave_cons1 show "(e # x) @ l ∈ (e # x) @ a ⊗ b" by force
    qed
  qed
  moreover assume "l ∈ a ⊗ b"
  ultimately show ?thesis by blast
qed

lemma interleave_append2: "⟦l ∈ a⊗b⟧ ⟹ x@l ∈ a ⊗ x@b" proof -
  have "ALL l a b . l ∈ a⊗b ⟶ x@l ∈ a ⊗ x@b" (is "?P x") proof (induct x)
    show "?P []" by simp
  next
    fix a 
    fix x::"'a list"
    assume IH: "∀l a b. l ∈ a ⊗ b ⟶ x @ l ∈ a ⊗ x @ b"
    show "∀l aa b. l ∈ aa ⊗ b ⟶ (a # x) @ l ∈ aa ⊗ (a # x) @ b" proof (intro impI allI)
      fix l::"'a list" 
      fix aa b
      assume "l ∈ aa ⊗ b"

      with IH have "x@l ∈ aa ⊗ x@b" by auto
      with interleave_cons2 show "(a # x) @ l ∈ aa ⊗ (a # x) @ b" by force
    qed
  qed
  moreover assume "l ∈ a ⊗ b"
  ultimately show ?thesis by blast
qed

lemmas interleave_append = interleave_append1 interleave_append2

lemma interleave_rev_append1: "!!a b w. w∈a⊗b ⟹ w@w' ∈ a@w' ⊗ b"
proof (induct w' rule: rev_induct)
  case Nil thus ?case by simp
next
  case (snoc e w') note IHP=this
  hence "w@w'∈a@w'⊗b" by auto
  thus ?case using interleave_rev_cons1[of "w@w'" "a@w'" "b"] by (simp)
qed
lemma interleave_rev_append2: "w∈a⊗b ⟹ w@w' ∈ a ⊗ b@w'"
  by (simp only: interleave_comm[of a b] interleave_comm[of a "b@w'"]) (blast dest: interleave_rev_append1)
lemmas interleave_rev_append = interleave_rev_append1 interleave_rev_append2

lemma interleave_rev1[rule_format]: "ALL w1 w2 . (w∈w1⊗w2) ⟶ (rev w ∈ rev w1 ⊗ rev w2)" (is "?P w")
proof (induct w)
  case Nil show ?case by (simp)
  case (Cons e w)
    assume IH[rule_format]: "?P w"
    show ?case proof (clarsimp)
      fix w1 w2
      assume "e # w ∈ w1 ⊗ w2"
      then obtain w' where "w1=e#w' & w∈w'⊗w2 | w2=e#w' & w∈w1⊗w'" by (blast dest: cons_interleave_split)
      with IH have "w1=e#w' & rev w∈rev w' ⊗ rev w2 | w2=e#w' & rev w ∈ rev w1 ⊗ rev w'" by auto
      thus "rev w @ [e]∈rev w1 ⊗ rev w2" by (auto simp add: interleave_rev_cons)
    qed
qed

corollary interleave_rev2: "(rev w ∈ rev w1 ⊗ rev w2) ⟹ (w∈w1⊗w2)" 
  apply (subgoal_tac "(rev w∈rev w1⊗rev w2) = (rev (rev w) ∈ rev (rev w1) ⊗ rev (rev w2))")
  apply(simp)
  apply (blast dest: interleave_rev1)
done

lemmas interleave_rev = interleave_rev1 interleave_rev2

lemma rev_cons_interleave_split: "⟦l@[a] ∈ l1⊗l2⟧ ⟹ (EX lh . l1=lh@[a] & l ∈ lh⊗l2 | l2=lh@[a] & l ∈ l1⊗lh )"
proof -
  assume "l@[a] ∈ l1⊗l2"
  hence "a#rev l ∈ rev l1 ⊗ rev l2" by (auto dest: interleave_rev)
  then obtain lh where "rev l1 = a#lh & rev l ∈ lh⊗rev l2 | rev l2 = a#lh & rev l ∈ rev l1 ⊗ lh" by (blast dest: cons_interleave_split)
  hence "rev l1 = a#lh & l ∈ rev lh ⊗ l2 | rev l2 = a#lh & l ∈ l1 ⊗ rev lh" by (auto dest: interleave_rev)
  hence "l1 = rev lh @ [a] & l ∈ rev lh ⊗ l2 | l2 = rev lh @ [a] & l ∈ l1 ⊗ rev lh" by (simp add: rev_swap)
  thus ?thesis by blast
qed

subsubsection "Associativity"
 
lemma interleave_s_assoc1[rule_format]: "ALL w1 ws w2 w3 . (w∈w1⊗ws & ws∈w2⊗w3 ⟶ (EX ws' : w1⊗w2 . w ∈ ws'⊗w3))" proof (induct w)
  case Nil show ?case by (auto)
  case (Cons e w)
    assume IH: "ALL w1 ws w2 w3 . w∈w1⊗ws & ws∈w2⊗w3 ⟶ (EX ws' : w1⊗w2 . w ∈ ws'⊗w3)"
    show ?case proof (intro impI allI)
      fix w1 ws w2 w3
      assume A: "e#w ∈ w1 ⊗ ws ∧ ws ∈ w2 ⊗ w3"
      then obtain wh where CASES: "w1=e#wh & w∈wh⊗ws | ws=e#wh & w∈w1⊗wh" by (blast dest!: cons_interleave_split)
      moreover {
        assume CASE: "w1=e#wh & w∈wh⊗ws"
        with A IH obtain ws' where "ws'∈wh⊗w2 & w∈ws'⊗w3" by (blast)
        hence "e#ws'∈ (e#wh)⊗w2 & e#w ∈ (e#ws')⊗w3" by (auto simp add: interleave_cons)
        with CASE have "∃ws'∈w1 ⊗ w2. e # w ∈ ws' ⊗ w3" by blast
      } moreover {
        assume CASE: "ws=e#wh & w∈w1⊗wh"
        with A obtain whh where "w2=e#whh & wh∈whh⊗w3 | w3=e#whh & wh∈w2⊗whh" by (blast dest!: cons_interleave_split)
        moreover {
          assume SCASE: "w2=e#whh & wh∈whh⊗w3"
          with CASE IH obtain ws' where "ws'∈w1⊗whh & w∈ws'⊗w3" by blast
          with SCASE have "e#ws'∈w1⊗w2 & e#w ∈ (e#ws')⊗w3" by (auto simp add: interleave_cons)
          hence "∃ws'∈w1 ⊗ w2. e # w ∈ ws' ⊗ w3" by blast
        } moreover {
          assume SCASE: "w3=e#whh & wh∈w2⊗whh"
          with CASE IH obtain ws' where "ws'∈w1⊗w2 & w∈ws'⊗whh" by blast
          with SCASE have "ws'∈w1⊗w2 & e#w ∈ ws'⊗w3" by (auto simp add: interleave_cons)
          hence "∃ws'∈w1 ⊗ w2. e # w ∈ ws' ⊗ w3" by blast
        } ultimately have "∃ws'∈w1 ⊗ w2. e # w ∈ ws' ⊗ w3" by blast
      } ultimately show "∃ws'∈w1 ⊗ w2. e # w ∈ ws' ⊗ w3" by blast
    qed
qed

lemma interleave_s_assoc2: "⟦w∈ws⊗w3; ws∈w1⊗w2⟧ ⟹ EX ws' : w2⊗w3 . w ∈ w1⊗ws'" proof -
  assume "w ∈ ws ⊗ w3" "ws ∈ w1 ⊗ w2"
  hence "w ∈ w3 ⊗ ws & ws ∈ w2 ⊗ w1" by simp
  hence "EX ws':w3⊗w2 . w∈ws'⊗w1" by (simp only: interleave_s_assoc1)
  thus ?thesis by simp
qed
  
lemmas interleave_s_assoc = interleave_s_assoc1 interleave_s_assoc2

subsubsection "Relation to other standard list operations"

lemma interleave_set: "w∈w1⊗w2 ⟹ set w = set w1 ∪ set w2"
  by (induct rule: interleave_elem_induct) auto
lemma interleave_map: "w∈w1⊗w2 ⟹ map f w ∈ map f w1 ⊗ map f w2"
  by (induct rule: interleave_elem_induct) (auto intro!: interleave_cons)
lemma interleave_filter: "w∈w1⊗w2 ⟹ filter f w ∈ filter f w1 ⊗ filter f w2"
  by (induct rule: interleave_elem_induct) (auto intro!: interleave_cons)


subsubsection "Relation to sublist order"

lemma ileq_interleave_alt: "l'≼l == ∃lb. l∈lb ⊗ l'" proof (rule eq_reflection)
  {fix l' l have "l'≼l ⟹ ∃lb. l∈lb ⊗ l'" by (induct rule: less_eq_list_induct) (simp, (blast intro: interleave_cons)+)}
  moreover {fix l have "!!lb l'. l∈lb⊗l' ⟹ l'≼l" by (induct l) (auto intro: less_eq_list_drop elim!: cons_interleave_cases)}
  ultimately show "(l'≼l) = (∃lb. l∈lb ⊗ l')" by blast
qed

lemma ileq_interleave: "w∈w1⊗w2 ⟹ w1≼w & w2≼w"
  by (unfold ileq_interleave_alt, auto)

lemma ilt_ex_notempty: "x < y ⟷ (∃xs. xs ≠ [] ∧ y ∈ xs ⊗ x)"
  apply (auto simp add: order_less_le ileq_interleave_alt)
  apply (case_tac lb)
  apply auto
done


lemma ilt_interleave1: "⟦w∈w1⊗w2; w1~=[]⟧ ⟹ w2<w"
  by (simp only: ilt_ex_notempty, blast)
lemma ilt_interleave2: "⟦w∈w1⊗w2; w2~=[]⟧ ⟹ w1<w"
  by (simp only: ilt_ex_notempty interleave_comm[of w1 w2], blast)
lemmas ilt_interleave = ilt_interleave1 ilt_interleave2


subsubsection "Exotic/specialized lemmas"
― ‹Recover structure of @{text w} wrt. to structure of @{text "w1"}›
lemma interleave_recover1[rule_format]: "ALL w1a w1b w2 . w∈(w1a@w1b)⊗w2 ⟶ (EX wa wb w2a w2b . w=wa@wb & w2=w2a@w2b & wa∈w1a⊗w2a & wb∈w1b⊗w2b)" 
  (is "?P w" is "ALL w1a w1b w2 . ?PRE w w1a w1b w2 ⟶ ?CONS w w1a w1b w2")
proof (induct w)
  case Nil show ?case by (auto)
  case (Cons e w)
    assume IH[rule_format]: "?P w"
    show "?P (e#w)" proof (intro allI impI)
      fix w1a w1b w2
      assume PRE: "e # w ∈ w1a @ w1b ⊗ w2"
      {
        assume CASE: "w1a=[]"
        with PRE have "e#w=[]@(e#w) & w2=[]@w2 & []∈w1a⊗[] & e#w∈w1b⊗w2" by (auto)
        hence "?CONS (e#w) w1a w1b w2" by blast
      } moreover {
        assume CASE: "w1a~=[]"
        with PRE obtain wh where SCASES: "w1a@w1b=e#wh & w∈wh⊗w2 | w2=e#wh & w∈w1a@w1b⊗wh" by (blast dest: cons_interleave_split)
        moreover {
          assume SCASE: "w1a@w1b=e#wh & w∈wh⊗w2"
          with CASE obtain w1ah where W1AFMT: "w1a=e#w1ah & w1ah@w1b=wh" by (cases w1a, auto)
          with SCASE have "w∈w1ah@w1b⊗w2" by auto
          with IH[of w1ah w1b w2] obtain wa wb w2a w2b where "w=wa@wb & w2=w2a@w2b & wa∈w1ah⊗w2a & wb∈w1b⊗w2b" by (blast)
          with W1AFMT have "e#w=(e#wa)@wb & e#w∈e#wa⊗wb & w2=w2a@w2b & e#wa∈w1a⊗w2a & wb∈w1b⊗w2b" by (auto simp add: interleave_cons)
          hence "?CONS (e#w) w1a w1b w2" by blast
        } moreover {
          assume SCASE: "w2=e#wh & w∈w1a@w1b⊗wh"
          with IH[of w1a w1b wh] obtain wa wb w2a w2b where "w=wa@wb & wh=w2a@w2b & wa∈w1a⊗w2a & wb∈w1b⊗w2b" by blast
          with SCASE have "e#w=(e#wa)@wb & w2=(e#w2a)@w2b & e#wa∈w1a⊗e#w2a & wb∈w1b⊗w2b" by (auto simp add: interleave_cons)
          hence "?CONS (e#w) w1a w1b w2" by blast
        }
        ultimately have "?CONS (e#w) w1a w1b w2" by blast
      }
      ultimately show "?CONS (e#w) w1a w1b w2" by blast
    qed
qed

lemma interleave_recover2: "w∈w1⊗(w2a@w2b) ⟹ EX wa wb w1a w1b . w=wa@wb & w1=w1a@w1b & wa∈w1a⊗w2a & wb∈w1b⊗w2b"
proof -
  assume "w∈w1⊗(w2a@w2b)"
  hence "w∈(w2a@w2b)⊗w1" by auto
  hence "EX wa wb w1a w1b . w=wa@wb & w1=w1a@w1b & wa∈w2a⊗w1a & wb∈w2b⊗w1b" by (blast dest: interleave_recover1)
  thus ?thesis by auto
qed

lemmas interleave_recover = interleave_recover1 interleave_recover2

― ‹Split operands according to element of result›
lemma interleave_unconc: "!! l2 w1 w2 . l1@l2 ∈ w1⊗w2 ⟹ ∃ w11 w12 w21 w22 . w1=w11@w12 ∧ w2=w21@w22 ∧ l1∈w11⊗w21 ∧ l2∈w12⊗w22"
proof (induct l1)
  case Nil hence "w1=[]@w1 & w2=[]@w2 & []∈[]⊗[] & l2∈w1⊗w2" by auto
  thus ?case by fast
next
  case (Cons e l1') note IHP=this
  hence "e#(l1'@l2)∈w1⊗w2" by auto
  with cons_interleave_split obtain w' where "(w1=e#w' & l1'@l2∈w'⊗w2) | (w2=e#w' & l1'@l2∈w1⊗w')" (is "?C1 | ?C2") by (fast)
  moreover {
    assume CASE: ?C1
    moreover then obtain w11' w12' w21 w22 where "w'=w11'@w12' ∧ w2=w21@w22 ∧ l1'∈w11'⊗w21 ∧ l2∈w12'⊗w22" by (fast dest: IHP(1))
    moreover hence "e#w'=(e#w11')@w12' & e#l1'∈(e#w11')⊗w21" by (auto dest: interleave_cons)
    ultimately have ?case by fast
  } moreover {
    assume CASE: ?C2
    moreover then obtain w11 w12 w21' w22' where "w1=w11@w12 ∧ w'=w21'@w22' ∧ l1'∈w11⊗w21' ∧ l2∈w12⊗w22'" by (fast dest: IHP(1))
    moreover hence "e#w'=(e#w21')@w22' & e#l1'∈w11⊗(e#w21')" by (auto dest: interleave_cons)
    ultimately have ?case by fast
  } ultimately show ?case by fast
qed

― ‹Reverse direction of @{thm [source] "interleave_unconc"}›
lemma interleave_reconc: "!!w11 w21 l2 w12 w22 . ⟦l1∈w11⊗w21;l2∈w12⊗w22⟧ ⟹ l1@l2∈(w11@w12)⊗(w21@w22)"
proof (induct l1)
  case Nil thus ?case by (auto)
next
  case (Cons e l1') note IHP=this
  then obtain w' where "(w11=e#w' & l1'∈w'⊗w21) | (w21=e#w' & l1'∈w11⊗w')" (is "?C1 | ?C2") by (fast dest: cons_interleave_split)
  moreover {
    assume CASE: ?C1
    moreover with IHP have "l1'@l2∈(w'@w12)⊗(w21@w22)" by auto
    ultimately have ?case by (auto dest: interleave_cons)
  } moreover {
    assume CASE: ?C2
    moreover with IHP have "l1'@l2∈(w11@w12)⊗(w'@w22)" by auto
    ultimately have ?case by (auto dest: interleave_cons)
  } ultimately show ?case by fast
qed

(* interleave_unconc and interleave_reconc as equivalence *)
lemma interleave_unconc_eq: "!! l2 w1 w2 . l1@l2 ∈ w1⊗w2 = (∃ w11 w12 w21 w22 . w1=w11@w12 ∧ w2=w21@w22 ∧ l1∈w11⊗w21 ∧ l2∈w12⊗w22)"
  by (fast dest: interleave_reconc interleave_unconc)


end