Theory DL_Missing_Sublist

theory DL_Missing_Sublist
imports Main
(* Author: Alexander Bentkamp, Universit├Ąt des Saarlandes
*)
section ‹Missing Lemmas of Sublist›

theory DL_Missing_Sublist
imports Main
begin

lemma nths_only_one:
assumes "{i. i < length xs ∧ i∈I} = {j}"
shows "nths xs I = [xs!j]"
proof -
  have "set (nths xs I) = {xs!j}"
    unfolding set_nths using subset_antisym assms by fastforce
  moreover have "length (nths xs I) = 1"
    unfolding length_nths assms by auto
  ultimately show ?thesis
    by (metis One_nat_def length_0_conv length_Suc_conv the_elem_eq the_elem_set)
qed

lemma nths_replicate:
"nths (replicate n x) A = (replicate (card {i. i < n ∧ i ∈ A}) x)"
proof (induction n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  then show ?case
  proof (cases "n∈A")
    case True
    then have 0:"(if 0 ∈ {j. j + length (replicate n x) ∈ A} then [x] else []) = [x]" by simp
    have "{i. i < Suc n ∧ i ∈ A} = insert n {i. i < n ∧ i ∈ A}" using True by auto
    have "Suc (card {i. i < n ∧ i ∈ A}) = card {i. i < Suc n ∧ i ∈ A}"
      unfolding ‹{i. i < Suc n ∧ i ∈ A} = insert n {i. i < n ∧ i ∈ A}›
      using finite_Collect_conjI[THEN card_insert_if] finite_Collect_less_nat
       less_irrefl_nat mem_Collect_eq by simp
    then show ?thesis unfolding replicate_Suc replicate_append_same[symmetric] nths_append Suc nths_singleton 0
      unfolding replicate_append_same replicate_Suc[symmetric] by simp
  next
    case False
    then have 0:"(if 0 ∈ {j. j + length (replicate n x) ∈ A} then [x] else []) = []" by simp
    have "{i. i < Suc n ∧ i ∈ A} = {i. i < n ∧ i ∈ A}" using False using le_less less_Suc_eq_le by auto
    then show ?thesis unfolding replicate_Suc replicate_append_same[symmetric] nths_append Suc nths_singleton 0
      by simp
  qed
qed

lemma length_nths_even:
assumes "even (length xs)"
shows "length (nths xs (Collect even)) = length (nths xs (Collect odd))"
using assms proof (induction "length xs div 2" arbitrary:xs)
  case 0
  then have "length xs = 0"
    by (auto elim: evenE)
  then show ?case by simp
next
  case (Suc l xs)
  then have length_drop2: "length (nths (drop 2 xs) (Collect even)) = length (nths (drop 2 xs) {a. odd a})" by simp

  have "length (take 2 xs) = 2" using Suc.hyps(2) by auto
  then have plus_odd: "{j. j + length (take 2 xs) ∈ Collect odd} = Collect odd" and
            plus_even: "{j. j + length (take 2 xs) ∈ Collect even} = Collect even" by simp_all
  have nths_take2: "nths (take 2 xs) (Collect even) = [take 2 xs ! 0]" "nths (take 2 xs) (Collect odd) = [take 2 xs ! 1]"
    using ‹length (take 2 xs) = 2› less_2_cases nths_only_one[of "take 2 xs" "Collect even" 0]
    nths_only_one[of "take 2 xs" "Collect odd" 1]
    by fastforce+
  then have "length (nths (take 2 xs @ drop 2 xs) (Collect even))
           = length (nths (take 2 xs @ drop 2 xs) {a. odd a})"
    unfolding nths_append length_append plus_odd plus_even nths_take2 length_drop2
    by auto
  then show ?case using append_take_drop_id[of 2 xs] by simp
qed

lemma nths_map:
"nths (map f xs) A = map f (nths xs A)"
proof (induction xs arbitrary:A)
  case Nil
  then show ?case by simp
next
  case (Cons x xs)
  then show ?case
  by (simp add: nths_Cons)
qed


section "Pick"

fun pick :: "nat set ⇒ nat ⇒ nat" where
"pick S 0 = (LEAST a. a∈S)" |
"pick S (Suc n) = (LEAST a. a∈S ∧ a > pick S n)"

lemma pick_in_set_inf:
assumes "infinite S"
shows "pick S n ∈ S"
proof (cases n)
  show "n = 0 ⟹ pick S n ∈ S"
    unfolding pick.simps using ‹infinite S› LeastI pick.simps(1) by (metis Collect_mem_eq not_finite_existsD)
next
  fix n' assume "n = Suc n'"
  obtain a where "a∈S ∧ a > pick S n'" using assms by (metis bounded_nat_set_is_finite less_Suc_eq nat_neq_iff)
  show "pick S n ∈ S" unfolding ‹n = Suc n'› pick.simps(2)
    using LeastI[of "λa. a ∈ S ∧ pick S n' < a" a, OF ‹a∈S ∧ a > pick S n'›] by blast
qed

lemma pick_mono_inf:
assumes "infinite S"
shows "m < n ⟹ pick S m < pick S n"
using assms proof (induction n)
  case 0
  then show ?case by auto
next
  case (Suc n)
  then obtain a where "a ∈ S ∧ pick S n < a" by (metis bounded_nat_set_is_finite less_Suc_eq nat_neq_iff)
  then have "pick S n < pick S (Suc n)" unfolding pick.simps
    using LeastI[of "λa. a ∈ S ∧ pick S n < a" a, OF ‹a∈S ∧ a > pick S n›] by simp
  then show ?case using Suc.IH Suc.prems(1) assms dual_order.strict_trans less_Suc_eq by auto
qed

lemma pick_eq_iff_inf:
assumes "infinite S"
shows "x = y ⟷ pick S x = pick S y"
  by (metis assms nat_neq_iff pick_mono_inf)

lemma card_le_pick_inf:
assumes "infinite S"
and "pick S n ≥ i"
shows "card {a∈S. a < i} ≤ n"
using assms proof (induction n arbitrary:i)
  case 0
  then show ?case unfolding pick.simps using not_less_Least
    by (metis (no_types, lifting) Collect_empty_eq card_0_eq card_ge_0_finite dual_order.strict_trans1 leI le_0_eq)
next
  case (Suc n)
  then show ?case
  proof -
    have "card {a ∈ S. a < pick S n} ≤ n" using Suc by blast
    have "{a ∈ S. a < i} ⊆ {a ∈ S. a < pick S (Suc n)}" using Suc.prems(2) by auto
    have "{a ∈ S. a < pick S (Suc n)} = {a ∈ S. a < pick S n} ∪ {pick S n}"
      apply (rule subset_antisym; rule subsetI)
      using not_less_Least UnCI mem_Collect_eq nat_neq_iff singleton_conv
       pick_mono_inf[OF Suc.prems(1), of n "Suc n"] pick_in_set_inf[OF Suc.prems(1), of n] by fastforce+
    then have "card {a ∈ S. a < i} ≤ card {a ∈ S. a < pick S n} + card {pick S n}"
      using card_Un_disjoint  card_mono[OF _ ‹{a ∈ S. a < i} ⊆ {a ∈ S. a < pick S (Suc n)}›] by simp
    then show ?thesis using ‹card {a ∈ S. a < pick S n} ≤ n›  by auto
  qed
qed

lemma card_pick_inf:
assumes "infinite S"
shows "card {a∈S. a < pick S n} = n"
using assms proof (induction n)
  case 0
  then show ?case unfolding pick.simps using not_less_Least by auto
next
  case (Suc n)
  then show "card {a∈S. a < pick S (Suc n)} = Suc n"
  proof -
    have "{a ∈ S. a < pick S (Suc n)} = {a ∈ S. a < pick S n} ∪ {pick S n}"
      apply (rule subset_antisym; rule subsetI)
      using not_less_Least UnCI mem_Collect_eq nat_neq_iff singleton_conv
       pick_mono_inf[OF Suc.prems, of n "Suc n"] pick_in_set_inf[OF Suc.prems, of n] by fastforce+
    then have "card {a ∈ S. a < pick S (Suc n)} = card {a ∈ S. a < pick S n} + card {pick S n}"  using card_Un_disjoint by auto
    then show ?thesis by (metis One_nat_def Suc_eq_plus1 Suc card_empty card_insert_if empty_iff finite.emptyI)
  qed
qed

lemma
assumes "n < card S"
shows
  pick_in_set_le:"pick S n ∈ S" and
  card_pick_le: "card {a∈S. a < pick S n} = n" and
  pick_mono_le: "m < n ⟹ pick S m < pick S n"
using assms proof (induction n)
  assume "0 < card S"
  then obtain x where "x∈S" by fastforce
  then show "pick S 0 ∈ S" unfolding pick.simps by (meson LeastI)
  then show "card {a ∈ S. a < pick S 0} = 0" using not_less_Least by auto
  show "m < 0 ⟹  pick S m < pick S 0" by auto
next
  fix n
  assume "n < card S ⟹ pick S n ∈ S"
    and "n < card S ⟹ card {a ∈ S. a < pick S n} = n"
    and "Suc n < card S"
    and "m < n ⟹ n < card S ⟹ pick S m < pick S n"
  then have "card {a ∈ S. a < pick S n} = n" "pick S n ∈ S" by linarith+
  have "card {a ∈ S. a > pick S n} > 0"
  proof -
    have "S = {a ∈ S. a < pick S n} ∪ {a ∈ S. a ≥ pick S n}" by fastforce
    then have "card {a ∈ S. a ≥ pick S n} > 1"
      using ‹Suc n < card S› ‹card {a ∈ S. a < pick S n} = n›
      card_Un_le[of "{a ∈ S. a < pick S n}" "{a ∈ S. pick S n ≤ a}"] by force
    then have 0:"{a ∈ S. a ≥ pick S n} ⊆ {pick S n} ∪ {a ∈ S. a > pick S n}" by auto
    have 1:"finite ({pick S n} ∪ {a ∈ S. pick S n < a})"
      unfolding finite_Un using Collect_mem_eq assms card_infinite conjI by force
    have "1 < card {pick S n} + card {a ∈ S. pick S n < a}"
      using card_mono[OF 1 0] card_Un_le[of "{pick S n}" "{a ∈ S. a > pick S n}"]  ‹card {a ∈ S. a ≥ pick S n} > 1›
      by linarith
    then show ?thesis by simp
  qed
  then show "pick S (Suc n) ∈ S" unfolding pick.simps
    by (metis (no_types, lifting) Collect_empty_eq LeastI card_0_eq card_infinite less_numeral_extra(3))
  have "pick S (Suc n) > pick S n"
    by (metis (no_types, lifting) pick.simps(2) ‹card {a ∈ S. a > pick S n} > 0› Collect_empty_eq LeastI card_0_eq card_infinite less_numeral_extra(3))
  then show "m < Suc n ⟹ pick S m < pick S (Suc n)"
    using ‹m < n ⟹ n < card S ⟹ pick S m < pick S n›
    using ‹Suc n < card S› dual_order.strict_trans less_Suc_eq by auto
  then show "card {a∈S. a < pick S (Suc n)} = Suc n"
  proof -
    have "{a ∈ S. a < pick S (Suc n)} = {a ∈ S. a < pick S n} ∪ {pick S n}"
      apply (rule subset_antisym; rule subsetI)
      using pick.simps not_less_Least ‹pick S (Suc n) > pick S n› ‹pick S n ∈ S› by fastforce+
    then have "card {a ∈ S. a < pick S (Suc n)} = card {a ∈ S. a < pick S n} + card {pick S n}"  using card_Un_disjoint by auto
    then show ?thesis by (metis One_nat_def Suc_eq_plus1 ‹card {a ∈ S. a < pick S n} = n› card_empty card_insert_if empty_iff finite.emptyI)
  qed
qed

lemma card_le_pick_le:
assumes "n < card S"
and "pick S n ≥ i"
shows "card {a∈S. a < i} ≤ n"
using assms proof (induction n arbitrary:i)
  case 0
  then show ?case unfolding pick.simps using not_less_Least
    by (metis (no_types, lifting) Collect_empty_eq card_0_eq card_ge_0_finite dual_order.strict_trans1 leI le_0_eq)
next
  case (Suc n)
  have "card {a ∈ S. a < pick S n} ≤ n" using Suc by (simp add: less_eq_Suc_le nat_less_le)
  have "{a ∈ S. a < i} ⊆ {a ∈ S. a < pick S (Suc n)}" using Suc.prems(2) by auto
  have "{a ∈ S. a < pick S (Suc n)} = {a ∈ S. a < pick S n} ∪ {pick S n}"
    apply (rule subset_antisym; rule subsetI)
    using pick.simps not_less_Least  pick_mono_le[OF Suc.prems(1), of n, OF lessI] pick_in_set_le[of n S] Suc by fastforce+
  then have "card {a ∈ S. a < i} ≤ card {a ∈ S. a < pick S n} + card {pick S n}"
    using card_Un_disjoint  card_mono[OF _ ‹{a ∈ S. a < i} ⊆ {a ∈ S. a < pick S (Suc n)}›] by simp
  then show ?case using ‹card {a ∈ S. a < pick S n} ≤ n›  by auto
qed

lemma
assumes "n < card S ∨ infinite S"
shows
  pick_in_set:"pick S n ∈ S" and
  card_le_pick: "i ≤ pick S n ==> card {a∈S. a < i} ≤ n" and
  card_pick: "card {a∈S. a < pick S n} = n" and
  pick_mono: "m < n ⟹ pick S m < pick S n"
    using assms pick_in_set_inf pick_in_set_le card_pick_inf card_pick_le card_le_pick_le card_le_pick_inf
    pick_mono_inf pick_mono_le by auto

lemma pick_card:
"pick I (card {a∈I. a < i}) = (LEAST a. a∈I ∧ a ≥ i)"
proof (induction i)
  case 0
  then show ?case by (simp add: pick_in_set_le)
next
  case (Suc i)
  then show ?case
  proof (cases "i∈I")
    case True
    then have 1:"pick I (card {a∈I. a < i}) = i" by (metis (mono_tags, lifting) Least_equality Suc.IH order_refl)
    have "{a ∈ I. a < Suc i} = {a ∈ I. a < i} ∪ {i}" using True by auto
    then have 2:"card {a ∈ I. a < Suc i} = Suc (card {a ∈ I. a < i})" by auto
    then show ?thesis unfolding 2 pick.simps 1 using Suc_le_eq by auto
  next
    case False
    then have 1:"{a ∈ I. a < Suc i} = {a ∈ I. a < i}" using Collect_cong less_Suc_eq by auto
    have 2:"⋀a. (a ∈ I ∧ Suc i ≤ a) = (a ∈ I ∧ i ≤ a)" using False Suc_leD le_less_Suc_eq not_le by blast
    then show ?thesis unfolding 1 2 using Suc.IH by blast
  qed
qed

lemma pick_card_in_set: "i∈I ⟹ pick I (card {a∈I. a < i}) = i"
  unfolding pick_card using Least_equality order_refl by (metis (no_types, lifting))

section "Sublist"

lemma nth_nths_card:
assumes "j<length xs"
and "j∈J"
shows "nths xs J ! card {j0. j0 < j ∧ j0 ∈ J} = xs!j"
using assms proof (induction xs rule:rev_induct)
  case Nil
  then show ?case using gr_implies_not0 list.size(3) by auto
next
  case (snoc x xs)
  then show ?case
  proof (cases "j < length xs")
    case True
    have "{j0. j0 < j ∧ j0 ∈ J} ⊂ {i. i < length xs ∧ i ∈ J}"
      using True snoc.prems(2) by auto
    then have "card {j0. j0 < j ∧ j0 ∈ J} < length (nths xs J)" unfolding length_nths
      using psubset_card_mono[of "{i. i < length xs ∧ i ∈ J}"] by simp
    then show ?thesis unfolding nths_append nth_append by (simp add: True snoc.IH snoc.prems(2))
  next
    case False
    then have "length xs = j"
      using length_append_singleton less_antisym snoc.prems(1) by auto
    then show ?thesis unfolding nths_append nth_append length_nths ‹length xs = j›
      by (simp add: snoc.prems(2))
  qed
qed

lemma pick_reduce_set:
assumes "i<card {a. a<m ∧ a∈I}"
shows "pick I i = pick {a. a < m ∧ a ∈ I} i"
using assms proof (induction i)
  let ?L = "LEAST a. a ∈ {a. a < m ∧ a ∈ I}"
  case 0
  then have "{a. a < m ∧ a ∈ I} ≠ {}" using card_empty less_numeral_extra(3) by fastforce
  then have "?L ∈ I" "?L < m" by (metis (mono_tags, lifting) Collect_empty_eq LeastI mem_Collect_eq)+
  have "⋀x. x ∈ {a. a < m ∧ a ∈ I} ⟹ ?L ≤ x" by (simp add: Least_le)
  have "⋀x. x ∈ I ⟹ ?L ≤ x"
    by (metis (mono_tags) ‹?L < m› ‹⋀x. x ∈ {a. a < m ∧ a ∈ I} ⟹ ?L ≤ x› dual_order.strict_trans2 le_cases mem_Collect_eq)
  then show ?case unfolding pick.simps using Least_equality[of "λx. x∈I", OF ‹?L ∈ I›] by blast
next
  case (Suc i)
  let ?L = "LEAST x. x ∈ {a. a < m ∧ a ∈ I} ∧ pick I i < x"
  have 0:"pick {a. a < m ∧ a ∈ I} i = pick I i" using Suc_lessD Suc by linarith
  then have "?L ∈ {a. a < m ∧ a ∈ I}" "pick I i < ?L"
    using LeastI[of "λa. a ∈ {a. a < m ∧ a ∈ I} ∧ pick I i < a"] using Suc.prems pick_in_set_le pick_mono_le by fastforce+
  then have "?L ∈ I" by blast
  show ?case unfolding pick.simps 0 using Least_equality[of "λa. a ∈ I ∧ pick I i < a" ?L]
    by (metis (no_types, lifting) Least_le ‹?L ∈ {a. a < m ∧ a ∈ I}› ‹pick I i < ?L› mem_Collect_eq not_le not_less_iff_gr_or_eq order.trans)
qed

lemma nth_nths:
assumes "i<card {i. i<length xs ∧ i∈I}"
shows "nths xs I ! i = xs ! pick I i"
proof -
  have "{a ∈ {i. i < length xs ∧ i ∈ I}. a < pick {i. i < length xs ∧ i ∈ I} i}
        = {a.  a < pick {i. i < length xs ∧ i ∈ I} i ∧ a ∈ I}"
    using assms pick_in_set by fastforce
  then have "card {a. a < pick {i. i < length xs ∧ i ∈ I} i ∧ a ∈ I} = i"
    using card_pick_le[OF assms] by simp
  then have "nths xs I ! i = xs ! pick {i. i < length xs ∧ i ∈ I} i"
    using nth_nths_card[where j = "pick {i. i < length xs ∧ i ∈ I} i", of xs I]
    assms pick_in_set pick_in_set by auto
  then show ?thesis using pick_reduce_set using assms by auto
qed

lemma pick_UNIV: "pick UNIV j = j"
by (induction j, simp, metis (no_types, lifting) LeastI pick.simps(2)  Suc_mono UNIV_I less_Suc_eq not_less_Least)

lemma pick_le:
assumes "n < card {a. a < i ∧ a ∈ S}"
shows "pick S n < i"
proof -
  have 0:"{a ∈ {a. a < i ∧ a ∈ S}. a < i} = {a. a < i ∧ a ∈ S}" by blast
  show ?thesis apply (rule ccontr)
    using card_le_pick_le[OF assms, unfolded pick_reduce_set[OF assms, symmetric], of i, unfolded 0]
    assms not_less not_le by blast
qed

lemma prod_list_complementary_nthss:
fixes f ::"'a ⇒ 'b::comm_monoid_mult"
shows "prod_list (map f xs) = prod_list (map f (nths xs A)) *  prod_list (map f (nths xs (-A)))"
proof (induction xs rule:rev_induct)
  case Nil
  then show ?case by simp
next
  case (snoc x xs)
  show ?case unfolding map_append "prod_list.append" nths_append nths_singleton snoc
    by (cases "(length xs)∈A"; simp;metis mult.assoc mult.commute)
qed

lemma nths_zip: "nths (zip xs ys) I = zip (nths xs I) (nths ys I)"
proof (rule nth_equalityI)
  show "length (nths (zip xs ys) I) = length (zip (nths xs I) (nths ys I))"
  proof (cases "length xs ≤ length ys")
    case True
    then have "{i. i < length xs ∧ i ∈ I} ⊆ {i. i < length ys ∧ i ∈ I}" by (simp add: Collect_mono less_le_trans)
    then have "card {i. i < length xs ∧ i ∈ I} ≤ card {i. i < length ys ∧ i ∈ I}"
      by (metis (mono_tags, lifting) card_mono finite_nat_set_iff_bounded mem_Collect_eq)
    then show ?thesis unfolding length_nths length_zip using True using min_def by linarith
  next
    case False
    then have "{i. i < length ys ∧ i ∈ I} ⊆ {i. i < length xs ∧ i ∈ I}" by (simp add: Collect_mono less_le_trans)
    then have "card {i. i < length ys ∧ i ∈ I} ≤ card {i. i < length xs ∧ i ∈ I}"
      by (metis (mono_tags, lifting) card_mono finite_nat_set_iff_bounded mem_Collect_eq)
    then show ?thesis unfolding length_nths length_zip using False using min_def by linarith
  qed
  show "nths (zip xs ys) I ! i = zip (nths xs I) (nths ys I) ! i" if "i < length (nths (zip xs ys) I)" for i
  proof -
   have "i < length (nths xs I)" "i < length (nths ys I)"
     using that by (simp_all add: ‹length (nths (zip xs ys) I) = length (zip (nths xs I) (nths ys I))›)
   show "nths (zip xs ys) I ! i = zip (nths xs I) (nths ys I) ! i"
     unfolding nth_nths[OF ‹i < length (nths (zip xs ys) I)›[unfolded length_nths]]
     unfolding nth_zip[OF ‹i < length (nths xs I)› ‹i < length (nths ys I)›]
     unfolding nth_zip[OF pick_le[OF ‹i < length (nths xs I)›[unfolded length_nths]]
                          pick_le[OF ‹i < length (nths ys I)›[unfolded length_nths]]]
     by (metis (full_types) ‹i < length (nths xs I)› ‹i < length (nths ys I)› length_nths nth_nths)
  qed
qed

section "weave"
    
definition weave :: "nat set ⇒ 'a list ⇒ 'a list ⇒ 'a list" where
"weave A xs ys = map (λi. if i∈A then xs!(card {a∈A. a<i}) else ys!(card {a∈-A. a<i})) [0..<length xs + length ys]"

lemma length_weave:
shows "length (weave A xs ys) = length xs + length ys"
unfolding weave_def length_map by simp

lemma nth_weave:
assumes "i < length (weave A xs ys)"
shows "weave A xs ys ! i = (if i∈A then xs!(card {a∈A. a<i}) else ys!(card {a∈-A. a<i}))"
proof -
  have "i < length xs + length ys" using length_weave using assms by metis
  then have "i < length [0..<length xs + length ys]" by auto
  then have "[0..<length xs + length ys] ! i = i"
    by (metis ‹i < length xs + length ys› add.left_neutral nth_upt)
  then show ?thesis
    unfolding weave_def nth_map[OF ‹i < length [0..<length xs + length ys]›] by presburger
qed

lemma weave_append1:
assumes "length xs + length ys ∈ A"
assumes "length xs = card {a∈A. a < length xs + length ys}"
shows "weave A (xs @ [x]) ys = weave A xs ys @ [x]"
proof (rule nth_equalityI)
  show "length (weave A (xs @ [x]) ys) = length (weave A xs ys @ [x])"
    unfolding weave_def length_map by simp
  show "weave A (xs @ [x]) ys ! i = (weave A xs ys @ [x]) ! i"
    if "i < length (weave A (xs @ [x]) ys)" for i
  proof -
    show "weave A (xs @ [x]) ys ! i = (weave A xs ys @ [x]) ! i"
    proof (cases "i = length xs + length ys")
      case True
      then have "(weave A xs ys @ [x]) ! i = x" using length_weave by (metis nth_append_length)
      have "card {a ∈ A. a < i} = length xs" using assms(2) True by auto
      then show ?thesis unfolding nth_weave[OF ‹i < length (weave A (xs @ [x]) ys)›]
        ‹(weave A xs ys @ [x]) ! i = x› using True assms(1) by simp
    next
      case False
      have "i < length (weave A xs ys)" using ‹i < length (weave A (xs @ [x]) ys)›
        ‹length (weave A (xs @ [x]) ys) = length (weave A xs ys @ [x])› length_append_singleton
        length_weave less_antisym False by fastforce
      then have "(weave A xs ys @ [x]) ! i = (weave A xs ys) ! i" by (simp add: nth_append)
      {
        assume "i∈A"
        have  "i<length xs + length ys" by (metis ‹i < length (weave A xs ys)› length_weave)
        then have "{a ∈ A. a < i} ⊂ {a∈A. a < length xs + length ys}"
          using assms(1) ‹i<length xs + length ys› ‹i∈A› by auto
        then have "card {a ∈ A. a < i} < card {a∈A. a < length xs + length ys}"
          using psubset_card_mono[of "{a∈A. a < length xs + length ys}" "{a ∈ A. a < i}"]  by simp
        then have "(xs @ [x]) ! card {a ∈ A. a < i} = xs ! card {a ∈ A. a < i}"
        by (metis (no_types, lifting)  assms(2) nth_append)
      }
      then show ?thesis unfolding nth_weave[OF ‹i < length (weave A (xs @ [x]) ys)›]
        ‹(weave A xs ys @ [x]) ! i = (weave A xs ys) ! i› nth_weave[OF ‹i < length (weave A xs ys)›]
        by simp
    qed
  qed
qed

lemma weave_append2:
assumes "length xs + length ys ∉ A"
assumes "length ys = card {a∈-A. a < length xs + length ys}"
shows "weave A xs (ys @ [y]) = weave A xs ys @ [y]"
proof (rule nth_equalityI)
  show "length (weave A xs (ys @ [y])) = length (weave A xs ys @ [y])"
    unfolding weave_def length_map by simp
  show "weave A xs (ys @ [y]) ! i = (weave A xs ys @ [y]) ! i" if "i < length (weave A xs (ys @ [y]))" for i
  proof -
    show "weave A xs (ys @ [y]) ! i = (weave A xs ys @ [y]) ! i"
    proof (cases "i = length xs + length ys")
      case True
      then have "(weave A xs ys @ [y]) ! i = y" using length_weave by (metis nth_append_length)
      have "card {a ∈ -A. a < i} = length ys" using assms(2) True by auto
      then show ?thesis unfolding nth_weave[OF ‹i < length (weave A xs (ys @ [y]))›]
        ‹(weave A xs ys @ [y]) ! i = y› using True assms(1) by simp
    next
      case False
      have "i < length (weave A xs ys)" using ‹i < length (weave A xs (ys @ [y]))›
        ‹length (weave A xs (ys @ [y])) = length (weave A xs ys @ [y])› length_append_singleton
        length_weave less_antisym False by fastforce
      then have "(weave A xs ys @ [y]) ! i = (weave A xs ys) ! i" by (simp add: nth_append)
      {
        assume "i∉A"
        have  "i<length xs + length ys" by (metis ‹i < length (weave A xs ys)› length_weave)
        then have "{a ∈ -A. a < i} ⊂ {a∈-A. a < length xs + length ys}"
          using assms(1) ‹i<length xs + length ys› ‹i∉A› by auto
        then have "card {a ∈ -A. a < i} < card {a∈-A. a < length xs + length ys}"
          using psubset_card_mono[of "{a∈-A. a < length xs + length ys}" "{a ∈ -A. a < i}"]  by simp
        then have "(ys @ [y]) ! card {a ∈ -A. a < i} = ys ! card {a ∈ -A. a < i}"
        by (metis (no_types, lifting)  assms(2) nth_append)
      }
      then show ?thesis unfolding nth_weave[OF ‹i < length (weave A xs (ys @ [y]))›]
        ‹(weave A xs ys @ [y]) ! i = (weave A xs ys) ! i› nth_weave[OF ‹i < length (weave A xs ys)›]
        by simp
    qed
  qed
qed

lemma nths_nth:
assumes "n∈A" "n<length xs"
shows "nths xs A ! (card {i. i<n ∧ i∈A}) = xs ! n"
using assms proof (induction xs rule:rev_induct)
  case (snoc x xs)
  then show ?case
  proof (cases "n = length xs")
    case True
    then show ?thesis unfolding nths_append[of xs "[x]" A] nth_append
      using length_nths[of xs A] nths_singleton snoc.prems(1) by auto
  next
    case False
    then have "n < length xs" using snoc by auto
    then have 0:"nths xs A ! card {i. i < n ∧ i ∈ A} = xs ! n" using snoc by auto

    have "{i. i < n ∧ i ∈ A} ⊂ {i. i < length xs ∧ i ∈ A}" using ‹n < length xs› snoc by force
    then have "card {i. i < n ∧ i ∈ A} < length (nths xs A)" unfolding length_nths
      by (simp add: psubset_card_mono)
    then show ?thesis unfolding nths_append[of xs "[x]" A] nth_append using 0
      by (simp add: ‹n < length xs›)
  qed
qed simp

lemma list_all2_nths:
assumes "list_all2 P (nths xs A) (nths ys A)"
and     "list_all2 P (nths xs (-A)) (nths ys (-A))"
shows "list_all2 P xs ys"
proof -
  have "length xs = length ys"
  proof (rule ccontr; cases "length xs < length ys")
    case True
    then show False
    proof (cases "length xs ∈ A")
      case False
      have "{i. i < length xs ∧ i ∈ - A} ⊂ {i. i < length ys ∧ i ∈ - A}"
        using False ‹length xs < length ys› by force
      then have "length (nths ys (-A)) > length (nths xs (-A))"
        unfolding length_nths by (simp add: psubset_card_mono)
      then show False using assms(2) list_all2_lengthD not_less_iff_gr_or_eq by blast
    next
      case True
      have "{i. i < length xs ∧ i ∈ A} ⊂ {i. i < length ys ∧ i ∈ A}"
        using True ‹length xs < length ys› by force
      then have "length (nths ys A) > length (nths xs A)"
        unfolding length_nths by (simp add: psubset_card_mono)
      then show False using assms(1) list_all2_lengthD not_less_iff_gr_or_eq by blast
    qed
  next
    assume "length xs ≠ length ys"
    case False
    then have "length xs > length ys" using ‹length xs ≠ length ys› by auto
    then show False
    proof (cases "length ys ∈ A")
      case False
      have "{i. i < length ys ∧ i ∈ -A} ⊂ {i. i < length xs ∧ i ∈ -A}"
        using False ‹length xs > length ys›  by force
      then have "length (nths xs (-A)) > length (nths ys (-A))"
        unfolding length_nths by (simp add: psubset_card_mono)
      then show False using assms(2) list_all2_lengthD dual_order.strict_implies_not_eq by blast
    next
      case True
      have "{i. i < length ys ∧ i ∈ A} ⊂ {i. i < length xs ∧ i ∈ A}"
        using True ‹length xs > length ys› by force
      then have "length (nths xs A) > length (nths ys A)"
        unfolding length_nths by (simp add: psubset_card_mono)
      then show False using assms(1) list_all2_lengthD dual_order.strict_implies_not_eq by blast
    qed
  qed

  have "⋀n. n < length xs ⟹ P (xs ! n) (ys ! n)"
  proof -
    fix n assume "n < length xs"
    then have "n < length ys" using ‹length xs = length ys› by auto
    then show "P (xs ! n) (ys ! n)"
    proof (cases "n∈A")
      case True
      have "{i. i < n ∧ i ∈ A} ⊂ {i. i < length xs ∧ i ∈ A}" using ‹n < length xs› ‹n∈A› by force
      then have "card {i. i < n ∧ i ∈ A} < length (nths xs A)" unfolding length_nths
        by (simp add: psubset_card_mono)
      show ?thesis using nths_nth[OF ‹n∈A› ‹n < length xs›] nths_nth[OF ‹n∈A› ‹n < length ys›]
        list_all2_nthD[OF assms(1), of "card {i. i < n ∧ i ∈ A}"] length_nths
        by (simp add: ‹card {i. i < n ∧ i ∈ A} < length (nths xs A)›)
    next
      case False then have "n∈-A" by auto
      have "{i. i < n ∧ i ∈ -A} ⊂ {i. i < length xs ∧ i ∈ -A}" using ‹n < length xs› ‹n∈-A› by force
      then have "card {i. i < n ∧ i ∈ -A} < length (nths xs (-A))" unfolding length_nths
        by (simp add: psubset_card_mono)
      show ?thesis using nths_nth[OF ‹n∈-A› ‹n < length xs›] nths_nth[OF ‹n∈-A› ‹n < length ys›]
        list_all2_nthD[OF assms(2), of "card {i. i < n ∧ i ∈ -A}"] length_nths
        using ‹card {i. i < n ∧ i ∈ - A} < length (nths xs (- A))› by auto   next
    qed
  qed
  then show ?thesis using ‹length xs = length ys› list_all2_all_nthI by blast
qed

lemma nths_weave:
assumes "length xs = card {a∈A. a < length xs + length ys}"
assumes "length ys = card {a∈(-A). a < length xs + length ys}"
shows "nths (weave A xs ys) A = xs ∧ nths (weave A xs ys) (-A) = ys"
using assms proof (induction "length xs + length ys" arbitrary: xs ys)
  case 0
  then show ?case
    unfolding weave_def nths_map by simp
next
  case (Suc l)
  then show ?case
  proof (cases "l∈A")
    case True
    then have "l∈{a ∈ A. a < length xs + length ys}" using Suc.hyps mem_Collect_eq zero_less_Suc by auto
    then have "length xs > 0" using Suc by fastforce
    then obtain xs' x where "xs = xs' @ [x]" by (metis append_butlast_last_id length_greater_0_conv)
    then have "l = length xs' + length ys" using Suc.hyps by simp
    have length_xs':"length xs' = card {a ∈ A. a < length xs' + length ys}"
    proof -
      have "{a ∈ A. a < length xs + length ys} = {a ∈ A. a < length xs' + length ys} ∪ {l}"
        using ‹xs = xs' @ [x]› ‹l∈{a ∈ A. a < length xs + length ys}› ‹l = length xs' + length ys›
        by force
      then have "card {a ∈ A. a < length xs + length ys} = card {a ∈ A. a < length xs' + length ys} + 1"
        using ‹l = length xs' + length ys› by fastforce
      then show ?thesis by (metis One_nat_def Suc.prems(1) ‹xs = xs' @ [x]› add_right_imp_eq
        length_Cons length_append list.size(3))
    qed
    have length_ys:"length ys = card {a ∈ - A. a < length xs' + length ys}"
    proof -
      have "l∉{a ∈ - A. a < length xs + length ys}" using ‹l∈A› ‹l = length xs' + length ys› by blast
      have "{a ∈ -A. a < length xs + length ys} = {a ∈ -A. a < length xs' + length ys}"
        apply (rule subset_antisym)
        using  ‹l = length xs' + length ys› ‹Suc l = length xs + length ys› ‹l∉{a ∈ - A. a < length xs + length ys}›
        apply (metis (no_types, lifting) Collect_mono less_Suc_eq mem_Collect_eq)
        using Collect_mono Suc.hyps(2) ‹l = length xs' + length ys› by auto
      then show ?thesis using Suc.prems(2) by auto
    qed
    have "length xs' + length ys ∈ A" using ‹l∈A› ‹l = length xs' + length ys› by blast

    then have "nths (weave A xs ys) A = nths (weave A xs' ys @ [x]) A" unfolding
       ‹xs = xs' @ [x]› using weave_append1[OF ‹length xs' + length ys ∈ A› length_xs'] by metis
    also have "... = nths (weave A xs' ys) A @ nths [x] {a. a + (length xs' + length ys) ∈ A}"
      using nths_append length_weave by metis
    also have "... = nths (weave A xs' ys) A @ [x]"
      using nths_singleton ‹length xs' + length ys ∈ A› by auto
    also have "... = xs" using Suc.hyps(1)[OF ‹l = length xs' + length ys› length_xs' length_ys]
     ‹xs = xs' @ [x]› by presburger
    finally have "nths (weave A xs ys) A = xs" by metis

    have "nths (weave A xs ys) (-A) = nths (weave A xs' ys @ [x]) (-A)" unfolding
       ‹xs = xs' @ [x]› using weave_append1[OF ‹length xs' + length ys ∈ A› length_xs'] by metis
    also have "... = nths (weave A xs' ys) (-A) @ nths [x] {a. a + (length xs' + length ys) ∈ (-A)}"
      using nths_append length_weave by metis
    also have "... = nths (weave A xs' ys) (-A)"
      using nths_singleton ‹length xs' + length ys ∈ A› by auto
    also have "... = ys"
      using Suc.hyps(1)[OF ‹l = length xs' + length ys› length_xs' length_ys] by presburger
    finally show ?thesis using ‹nths (weave A xs ys) A = xs› by auto
  next
    case False
    then have "l∉{a ∈ A. a < length xs + length ys}" using Suc.hyps mem_Collect_eq zero_less_Suc by auto
    then have "length ys > 0" using Suc by fastforce
    then obtain ys' y where "ys = ys' @ [y]" by (metis append_butlast_last_id length_greater_0_conv)
    then have "l = length xs + length ys'" using Suc.hyps by simp
    have length_ys':"length ys' = card {a ∈ -A. a < length xs + length ys'}"
    proof -
      have "{a ∈ -A. a < length xs + length ys} = {a ∈ -A. a < length xs + length ys'} ∪ {l}"
        using ‹ys = ys' @ [y]› ‹l∉{a ∈ A. a < length xs + length ys}› ‹l = length xs + length ys'›
        by force
      then have "card {a ∈ -A. a < length xs + length ys} = card {a ∈ -A. a < length xs + length ys'} + 1"
        using ‹l = length xs + length ys'› by fastforce
      then show ?thesis by (metis One_nat_def Suc.prems(2) ‹ys = ys' @ [y]› add_right_imp_eq
        length_Cons length_append list.size(3))
    qed
    have length_xs:"length xs = card {a ∈ A. a < length xs + length ys'}"
    proof -
      have "l∉{a ∈ A. a < length xs + length ys}" using ‹l∉A› ‹l = length xs + length ys'› by blast
      have "{a ∈ A. a < length xs + length ys} = {a ∈ A. a < length xs + length ys'}"
        apply (rule subset_antisym)
        using  ‹l = length xs + length ys'› ‹Suc l = length xs + length ys› ‹l∉{a ∈ A. a < length xs + length ys}›
        apply (metis (no_types, lifting) Collect_mono less_Suc_eq mem_Collect_eq)
        using Collect_mono Suc.hyps(2) ‹l = length xs + length ys'› by auto
      then show ?thesis using Suc.prems(1) by auto
    qed
    have "length xs + length ys' ∉ A" using ‹l∉A› ‹l = length xs + length ys'› by blast

    then have "nths (weave A xs ys) A = nths (weave A xs ys' @ [y]) A" unfolding
       ‹ys = ys' @ [y]› using weave_append2[OF ‹length xs + length ys' ∉ A› length_ys'] by metis
    also have "... = nths (weave A xs ys') A @ nths [y] {a. a + (length xs + length ys') ∈ A}"
      using nths_append length_weave by metis
    also have "... = nths (weave A xs ys') A"
      using nths_singleton ‹length xs + length ys' ∉ A› by auto
    also have "... = xs"
      using Suc.hyps(1)[OF ‹l = length xs + length ys'› length_xs length_ys'] by auto
    finally have "nths (weave A xs ys) A = xs" by auto

    have "nths (weave A xs ys) (-A) = nths (weave A xs ys' @ [y]) (-A)" unfolding
       ‹ys = ys' @ [y]› using weave_append2[OF ‹length xs + length ys' ∉ A› length_ys'] by metis
    also have "... = nths (weave A xs ys') (-A) @ nths [y] {a. a + (length xs + length ys') ∈ (-A)}"
      using nths_append length_weave by metis
    also have "... = nths (weave A xs ys') (-A) @ [y]"
      using nths_singleton ‹length xs + length ys' ∉ A› by auto
    also have "... = ys"
      using Suc.hyps(1)[OF ‹l = length xs + length ys'› length_xs length_ys'] ‹ys = ys' @ [y]› by simp
    finally show ?thesis using ‹nths (weave A xs ys) A = xs› by auto
  qed
qed

lemma set_weave:
assumes "length xs = card {a∈A. a < length xs + length ys}"
assumes "length ys = card {a∈-A. a < length xs + length ys}"
shows "set (weave A xs ys) = set xs ∪ set ys"
proof
  show "set (weave A xs ys) ⊆ set xs ∪ set ys"
  proof
    fix x assume "x∈set (weave A xs ys)"
    then obtain i where "weave A xs ys ! i = x" "i<length (weave A xs ys)" by (meson in_set_conv_nth)
    show "x ∈ set xs ∪ set ys"
    proof (cases "i∈A")
      case True
      then have "i ∈ {a∈A. a < length xs + length ys}" unfolding length_weave
        by (metis ‹i < length (weave A xs ys)› length_weave mem_Collect_eq)
      then have "{a ∈ A. a < i} ⊂ {a∈A. a < length xs + length ys}"
        using Collect_mono ‹i < length (weave A xs ys)›[unfolded length_weave] le_Suc_ex  less_imp_le_nat trans_less_add1
        le_neq_trans less_irrefl mem_Collect_eq by auto
      then have "card {a ∈ A. a < i} < card {a∈A. a < length xs + length ys}" by (simp add: psubset_card_mono)
      then show "x ∈ set xs ∪ set ys"
        unfolding nth_weave[OF ‹i<length (weave A xs ys)›, unfolded ‹weave A xs ys ! i = x›] using True
        using UnI1 assms(1) nth_mem by auto
    next
      case False
      have "i∉A ⟹ i ∈ {a∈-A. a < length xs + length ys}" unfolding length_weave
        by (metis ComplI ‹i < length (weave A xs ys)› length_weave mem_Collect_eq)
      then have "{a ∈ -A. a < i} ⊂ {a∈-A. a < length xs + length ys}"
        using Collect_mono ‹i < length (weave A xs ys)›[unfolded length_weave] le_Suc_ex  less_imp_le_nat trans_less_add1
        le_neq_trans less_irrefl mem_Collect_eq using False by auto
      then have "card {a ∈ -A. a < i} < card {a∈-A. a < length xs + length ys}" by (simp add: psubset_card_mono)
      then show "x ∈ set xs ∪ set ys"
        unfolding nth_weave[OF ‹i<length (weave A xs ys)›, unfolded ‹weave A xs ys ! i = x›] using False
        using UnI1 assms(2) nth_mem by auto
    qed
  qed
  show "set xs ∪ set ys ⊆ set (weave A xs ys)"
    using nths_weave[OF assms] by (metis Un_subset_iff set_nths_subset)
qed


lemma weave_complementary_nthss[simp]:
 "weave A (nths xs A) (nths xs (-A)) = xs"
proof (induction xs rule:rev_induct)
  case Nil
  then show ?case by (metis gen_length_def length_0_conv length_code length_weave nths_nil)
next
  case (snoc x xs)
  have length_xs:"length xs = length (nths xs A) + length (nths xs (-A))" by (metis length_weave snoc.IH)
  show ?case
  proof (cases "(length xs)∈A")
    case True
    have 0:"length (nths xs A) + length (nths xs (-A)) ∈ A" using length_xs True by metis
    have 1:"length (nths xs A) = card {a ∈ A. a < length (nths xs A) + length (nths xs (-A))}"
      using length_nths[of xs A] by (metis (no_types, lifting) Collect_cong length_xs)
    have 2:"nths (xs @ [x]) A = nths xs A @ [x]"
      unfolding nths_append[of xs "[x]" A] using nths_singleton True by auto
    have 3:"nths (xs @ [x]) (-A) = nths xs (-A)"
      unfolding nths_append[of xs "[x]" "-A"] using True by auto
    show ?thesis unfolding 2 3 weave_append1[OF 0 1] snoc.IH by metis
  next
    case False
    have 0:"length (nths xs A) + length (nths xs (-A)) ∉ A" using length_xs False by metis
    have 1:"length (nths xs (-A)) = card {a ∈ -A. a < length (nths xs A) + length (nths xs (-A))}"
      using length_nths[of xs "-A"] by (metis (no_types, lifting) Collect_cong length_xs)
    have 2:"nths (xs @ [x]) A = nths xs A"
      unfolding nths_append[of xs "[x]" A] using nths_singleton False by auto
    have 3:"nths (xs @ [x]) (-A) = nths xs (-A) @ [x]"
      unfolding nths_append[of xs "[x]" "-A"] using False by auto
    show ?thesis unfolding 2 3 weave_append2[OF 0 1] snoc.IH by metis
  qed
qed

lemma length_nths': "length (nths xs I) = card {i∈I. i < length xs}"
unfolding length_nths by meson

end