Theory Missing_List

(*  
    Author:      René Thiemann 
                 Akihisa Yamada
    License:     BSD
*)
subsection ‹Missing List›

text ‹The provides some standard algorithms and lemmas on lists.›
theory Missing_List
imports 
  Matrix.Utility
  "HOL-Library.Monad_Syntax"
begin

fun concat_lists :: "'a list list  'a list list" where
  "concat_lists [] = [[]]"
| "concat_lists (as # xs) = concat (map (λvec. map (λa. a # vec) as) (concat_lists xs))"

lemma concat_lists_listset: "set (concat_lists xs) = listset (map set xs)" 
  by (induct xs, auto simp: set_Cons_def)

lemma sum_list_concat: "sum_list (concat ls) = sum_list (map sum_list ls)"
  by (induct ls, auto)


(* TODO: move to src/HOL/List *)
lemma listset: "listset xs = { ys. length ys = length xs  ( i < length xs. ys ! i  xs ! i)}"
proof (induct xs)
  case (Cons x xs)
  let ?n = "length xs" 
  from Cons 
  have "?case = (set_Cons x {ys. length ys = ?n  (i < ?n. ys ! i  xs ! i)} =
    {ys. length ys = Suc ?n  ys ! 0  x  (i < ?n. ys ! Suc i  xs ! i)})" 
    (is "_ = (?L = ?R)")
    by (auto simp: all_Suc_conv)
  also have "?L = ?R"
    by (auto simp: set_Cons_def, case_tac xa, auto)
  finally show ?case by simp
qed auto

lemma set_concat_lists[simp]: "set (concat_lists xs) = {as. length as = length xs  (i<length xs. as ! i  set (xs ! i))}"
  unfolding concat_lists_listset listset by simp

declare concat_lists.simps[simp del]

fun find_map_filter :: "('a  'b)  ('b  bool)  'a list  'b option" where
  "find_map_filter f p [] = None"
| "find_map_filter f p (a # as) = (let b = f a in if p b then Some b else find_map_filter f p as)"

lemma find_map_filter_Some: "find_map_filter f p as = Some b  p b  b  f ` set as"
  by (induct f p as rule: find_map_filter.induct, auto simp: Let_def split: if_splits)

lemma find_map_filter_None: "find_map_filter f p as = None   b  f ` set as. ¬ p b"
  by (induct f p as rule: find_map_filter.induct, auto simp: Let_def split: if_splits)

lemma remdups_adj_sorted_distinct[simp]: "sorted xs  distinct (remdups_adj xs)"
by (induct xs rule: remdups_adj.induct) (auto)

lemma subseqs_length_simple:
  assumes "b  set (subseqs xs)" shows "length b  length xs"
  using assms by(induct xs arbitrary:b;auto simp:Let_def Suc_leD)

lemma subseqs_length_simple_False:
  assumes "b  set (subseqs xs)" " length xs < length b" shows False
  using assms subseqs_length_simple by fastforce

lemma empty_subseqs[simp]: "[]  set (subseqs xs)" by (induct xs, auto simp: Let_def)

lemma full_list_subseqs: "{ys. ys  set (subseqs xs)  length ys = length xs} = {xs}" 
proof (induct xs)
  case (Cons x xs)
  have "?case = ({ys  (#) x ` set (subseqs xs)  set (subseqs xs). 
    length ys = Suc (length xs)} = (#) x ` {xs})" (is "_ = (?l = ?r)")
    by (auto simp: Let_def)
  also have "?l = {ys  (#) x ` set (subseqs xs). length ys = Suc (length xs)}" 
    using length_subseqs[of xs]
    using subseqs_length_simple_False by force
  also have " = (#) x ` {ys  set (subseqs xs). length ys = length xs}"
    by auto
  also have " = (#) x ` {xs}" unfolding Cons by auto
  finally show ?case by simp
qed simp

lemma nth_concat_split: assumes "i < length (concat xs)" 
  shows " j k. j < length xs  k < length (xs ! j)  concat xs ! i = xs ! j ! k"
  using assms
proof (induct xs arbitrary: i)
  case (Cons x xs i)
  define I where "I = i - length x" 
  show ?case 
  proof (cases "i < length x")
    case True note l = this
    hence i: "concat (Cons x xs) ! i = x ! i" by (auto simp: nth_append)
    show ?thesis unfolding i
      by (rule exI[of _ 0], rule exI[of _ i], insert Cons l, auto)
  next
    case False note l = this
    from l Cons(2) have i: "i = length x + I" "I < length (concat xs)" unfolding I_def by auto
    hence iI: "concat (Cons x xs) ! i = concat xs ! I" by (auto simp: nth_append)
    from Cons(1)[OF i(2)] obtain j k where
      IH: "j < length xs  k < length (xs ! j)  concat xs ! I = xs ! j ! k" by auto
    show ?thesis unfolding iI
      by (rule exI[of _ "Suc j"], rule exI[of _ k], insert IH, auto)
  qed
qed simp

lemma nth_concat_diff: assumes "i1 < length (concat xs)" "i2 < length (concat xs)" "i1  i2"
  shows " j1 k1 j2 k2. (j1,k1)  (j2,k2)  j1 < length xs  j2 < length xs
     k1 < length (xs ! j1)  k2 < length (xs ! j2) 
     concat xs ! i1 = xs ! j1 ! k1  concat xs ! i2 = xs ! j2 ! k2"
  using assms
proof (induct xs arbitrary: i1 i2)
  case (Cons x xs)
  define I1 where "I1 = i1 - length x" 
  define I2 where "I2 = i2 - length x" 
  show ?case 
  proof (cases "i1 < length x")
    case True note l1 = this
    hence i1: "concat (Cons x xs) ! i1 = x ! i1" by (auto simp: nth_append)
    show ?thesis
    proof (cases "i2 < length x")
      case True note l2 = this
      hence i2: "concat (Cons x xs) ! i2 = x ! i2" by (auto simp: nth_append)
      show ?thesis unfolding i1 i2 
        by (rule exI[of _ 0], rule exI[of _ i1], rule exI[of _ 0], rule exI[of _ i2], 
         insert Cons(4) l1 l2, auto)
    next
      case False note l2 = this
      from l2 Cons(3) have i22: "i2 = length x + I2" "I2 < length (concat xs)" unfolding I2_def by auto
      hence i2: "concat (Cons x xs) ! i2 = concat xs ! I2" by (auto simp: nth_append)
      from nth_concat_split[OF i22(2)] obtain j2 k2 where
        *: "j2 < length xs  k2 < length (xs ! j2)  concat xs ! I2 = xs ! j2 ! k2" by auto
      show ?thesis unfolding i1 i2
        by (rule exI[of _ 0], rule exI[of _ i1], rule exI[of _ "Suc j2"], rule exI[of _ k2],
         insert * l1, auto)
    qed
  next
    case False note l1 = this
    from l1 Cons(2) have i11: "i1 = length x + I1" "I1 < length (concat xs)" unfolding I1_def by auto
    hence i1: "concat (Cons x xs) ! i1 = concat xs ! I1" by (auto simp: nth_append)
    show ?thesis
    proof (cases "i2 < length x")
      case False note l2 = this
      from l2 Cons(3) have i22: "i2 = length x + I2" "I2 < length (concat xs)" unfolding I2_def by auto
      hence i2: "concat (Cons x xs) ! i2 = concat xs ! I2" by (auto simp: nth_append)
      from Cons(4) i11 i22 have diff: "I1  I2" by auto
      from Cons(1)[OF i11(2) i22(2) diff] obtain j1 k1 j2 k2
        where IH: "(j1,k1)  (j2,k2)  j1 < length xs  j2 < length xs
         k1 < length (xs ! j1)  k2 < length (xs ! j2) 
         concat xs ! I1 = xs ! j1 ! k1  concat xs ! I2 = xs ! j2 ! k2" by auto
      show ?thesis unfolding i1 i2 
        by (rule exI[of _ "Suc j1"], rule exI[of _ k1], rule exI[of _ "Suc j2"], rule exI[of _ k2],
        insert IH, auto)
    next
      case True note l2 = this
      hence i2: "concat (Cons x xs) ! i2 = x ! i2" by (auto simp: nth_append)
      from nth_concat_split[OF i11(2)] obtain j1 k1 where
        *: "j1 < length xs  k1 < length (xs ! j1)  concat xs ! I1 = xs ! j1 ! k1" by auto
      show ?thesis unfolding i1 i2
        by (rule exI[of _ "Suc j1"], rule exI[of _ k1], rule exI[of _ 0], rule exI[of _ i2],
         insert * l2, auto)
    qed
  qed      
qed auto

lemma list_all2_map_map: "( x. x  set xs  R (f x) (g x))  list_all2 R (map f xs) (map g xs)"
  by (induct xs, auto)

subsection ‹Partitions›
text ‹Check whether a list of sets forms a partition, i.e.,
whether the sets are pairwise disjoint.›
definition is_partition :: "('a set) list  bool" where
  "is_partition cs  (j<length cs. i<j. cs ! i  cs ! j = {})"

(* and an equivalent but more symmetric version *)
definition is_partition_alt :: "('a set) list  bool" where
  "is_partition_alt cs  ( i j. i < length cs  j < length cs  i  j  cs!i  cs!j = {})"

lemma is_partition_alt: "is_partition = is_partition_alt"
proof (intro ext)
  fix cs :: "'a set list"
  {
    assume "is_partition_alt cs"
    hence "is_partition cs" unfolding is_partition_def is_partition_alt_def by auto
  }
  moreover
  {
    assume part: "is_partition cs"
    have "is_partition_alt cs" unfolding is_partition_alt_def
    proof (intro allI impI)
      fix i j
      assume "i < length cs  j < length cs  i  j"
      with part show "cs ! i  cs ! j = {}"
        unfolding is_partition_def
        by (cases "i < j", simp, cases "j < i", force, simp)
    qed
  }
  ultimately
  show "is_partition cs = is_partition_alt cs" by auto
qed
      
lemma is_partition_Nil:
  "is_partition [] = True" unfolding is_partition_def by auto

lemma is_partition_Cons:
  "is_partition (x#xs)  is_partition xs  x  (set xs) = {}" (is "?l = ?r")
proof
  assume ?l
  have one: "is_partition xs"
  proof (unfold is_partition_def, intro allI impI)
    fix j i assume "j < length xs" and "i < j"
    hence "Suc j < length(x#xs)" and "Suc i < Suc j" by auto
    from ?l[unfolded is_partition_def,THEN spec,THEN mp,THEN spec,THEN mp,OF this]
    have "(x#xs)!(Suc i)  (x#xs)!(Suc j) = {}" .
    thus "xs!i  xs!j = {}" by simp
  qed
  have two: "x  (set xs) = {}"
  proof (rule ccontr)
    assume "x  (set xs)  {}"
    then obtain y where "y  x" and "y  (set xs)" by auto
    then obtain z where "z  set xs" and "y  z" by auto
    then obtain i where "i < length xs" and "xs!i = z" using in_set_conv_nth[of z xs] by auto
    with y  z have "y  (x#xs)!Suc i" by auto
    moreover with y  x have "y  (x#xs)!0" by simp
    ultimately have "(x#xs)!0  (x#xs)!Suc i  {}" by auto
    moreover from i < length xs have "Suc i < length(x#xs)" by simp
    ultimately show False using ?l[unfolded is_partition_def] by best
  qed
  from one two show ?r ..
next
  assume ?r
  show ?l
  proof (unfold is_partition_def, intro allI impI)
    fix j i
    assume j: "j < length (x # xs)"
    assume i: "i < j"
    from i obtain j' where j': "j = Suc j'" by (cases j, auto)
    with j have j'len: "j' < length xs" and j'elem: "(x # xs) ! j = xs ! j'" by auto
    show "(x # xs) ! i  (x # xs) ! j = {}"
    proof (cases i)
      case 0
      with j'elem have "(x # xs) ! i  (x # xs) ! j = x  xs ! j'" by auto
      also have "  x  (set xs)" using j'len by force
      finally show ?thesis using ?r by auto
    next
      case (Suc i')
      with i j' have i'j': "i' < j'" by auto
      from Suc j' have "(x # xs) ! i  (x # xs) ! j = xs ! i'  xs ! j'" by auto
      with ?r i'j' j'len show ?thesis unfolding is_partition_def by auto
    qed
  qed
qed

lemma is_partition_sublist:
  assumes "is_partition (us @ xs @ ys @ zs @ vs)" 
  shows "is_partition (xs @ zs)"
proof (rule ccontr)
  assume "¬ is_partition (xs @ zs)"
  then obtain i j where j:"j < length (xs @ zs)" and i:"i < j" and *:"(xs @ zs) ! i  (xs @ zs) ! j  {}" 
    unfolding is_partition_def by blast
  then show False
  proof (cases "j < length xs")
    case True
    let ?m = "j + length us"
    let ?n = "i + length us" 
    from True have "?m < length (us @ xs @ ys @ zs @ vs)" by auto
    moreover from i have "?n < ?m" by auto
    moreover have "(us @ xs @ ys @ zs @ vs) ! ?n  (us @ xs @ ys @ zs @ vs) ! ?m  {}" 
      using i True * nth_append 
      by (metis (no_types, lifting) add_diff_cancel_right' not_add_less2 order.strict_trans)
    ultimately show False using assms unfolding is_partition_def by auto
  next
    case False
    let ?m = "j + length us + length ys"
    from j have m:"?m < length (us @ xs @ ys @ zs @ vs)" by auto
    have mj:"(us @ (xs @ ys @ zs @ vs)) ! ?m = (xs @ zs) ! j" unfolding nth_append using False j by auto
    show False
    proof (cases "i < length xs")
      case True
      let ?n = "i + length us"
      from i have "?n < ?m" by auto
      moreover have "(us @ xs @ ys @ zs @ vs) ! ?n = (xs @ zs) ! i" by (simp add: True nth_append) 
      ultimately show False using * m assms mj unfolding is_partition_def by blast
    next
      case False
      let ?n = "i + length us + length ys"
      from i have i:"?n < ?m" by auto
      moreover have "(us @ xs @ ys @ zs @ vs) ! ?n = (xs @ zs) ! i"
        unfolding nth_append using False i j less_diff_conv2 by auto
      ultimately show False using * m assms mj unfolding is_partition_def by blast
    qed
  qed
qed

lemma is_partition_inj_map:
  assumes "is_partition xs"
  and "inj_on f (x  set xs. x)"
  shows "is_partition (map ((`) f) xs)"
proof (rule ccontr)
  assume "¬ is_partition (map ((`) f) xs)"
  then obtain i j where neq:"i  j" 
    and i:"i < length (map ((`) f) xs)" and j:"j < length (map ((`) f) xs)"
    and "map ((`) f) xs ! i  map ((`) f) xs ! j  {}" 
    unfolding is_partition_alt is_partition_alt_def by auto
  then obtain x where "x  map ((`) f) xs ! i" and "x  map ((`) f) xs ! j" by auto
  then obtain y z where yi:"y  xs ! i" and yx:"f y = x" and zj:"z  xs ! j" and zx:"f z = x" 
    using i j by auto
  show False
  proof (cases "y = z")
    case True
    with zj yi neq assms(1) i j show ?thesis by (auto simp: is_partition_alt is_partition_alt_def)
  next
    case False
    have "y  (x  set xs. x)" using yi i by force
    moreover have "z  (x  set xs. x)" using zj j by force
    ultimately show ?thesis using assms(2) inj_on_def[of f "(xset xs. x)"] False zx yx by blast
  qed
qed

context
begin
private fun is_partition_impl :: "'a set list  'a set option" where
  "is_partition_impl [] = Some {}"
| "is_partition_impl (as # rest) = do {
      all  is_partition_impl rest;
      if as  all = {} then Some (all  as) else None
    }" 

lemma is_partition_code[code]: "is_partition as = (is_partition_impl as  None)" 
proof -
  note [simp] = is_partition_Cons is_partition_Nil
  have " bs. (is_partition as = (is_partition_impl as  None)) 
    (is_partition_impl as = Some bs  bs =  (set as))"
  proof (induct as)
    case (Cons as rest bs)
    show ?case
    proof (cases "is_partition rest")
      case False
      thus ?thesis using Cons by auto
    next
      case True
      with Cons obtain c where rest: "is_partition_impl rest = Some c" 
        by (cases "is_partition_impl rest", auto)
      with Cons True show ?thesis by auto
    qed
  qed auto
  thus ?thesis by blast
qed
end

lemma case_prod_partition:
  "case_prod f (partition p xs) = f (filter p xs) (filter (Not  p) xs)"
  by simp

lemmas map_id[simp] = list.map_id


subsection ‹merging functions›

definition fun_merge :: "('a  'b)list  'a set list  'a  'b"
  where "fun_merge fs as a  (fs ! (LEAST i. i < length as  a  as ! i)) a"

lemma fun_merge: assumes 
      i: "i < length as"
  and a: "a  as ! i"
  and ident: " i j a. i < length as  j < length as  a  as ! i  a  as ! j  (fs ! i) a = (fs ! j) a"
  shows "fun_merge fs as a = (fs ! i) a"
proof -
  let ?p = "λ i. i < length as  a  as ! i"
  let ?l = "LEAST i. ?p i"
  have p: "?p ?l"
    by (rule LeastI, insert i a, auto)
  show ?thesis unfolding fun_merge_def
    by (rule ident[OF _ i _ a], insert p, auto)
qed

lemma fun_merge_part: assumes 
      part: "is_partition as"
  and i: "i < length as"
  and a: "a  as ! i"
  shows "fun_merge fs as a = (fs ! i) a"
proof(rule fun_merge[OF i a])
  fix i j a
  assume "i < length as" and "j < length as" and "a  as ! i" and "a  as ! j"
  hence "i = j" using part[unfolded is_partition_alt is_partition_alt_def] by (cases "i = j", auto)
  thus "(fs ! i) a = (fs ! j) a" by simp
qed


lemma map_nth_conv: "map f ss = map g ts  i < length ss. f(ss!i) = g(ts!i)"
proof (intro allI impI)
  fix i show "map f ss = map g ts  i < length ss  f(ss!i) = g(ts!i)"
  proof (induct ss arbitrary: i ts)
    case Nil thus ?case by (induct ts) auto
  next
    case (Cons s ss) thus ?case
      by (induct ts, simp, (cases i, auto))
  qed
qed

lemma distinct_take_drop:
  assumes dist: "distinct vs" and len: "i < length vs" shows "distinct(take i vs @ drop (Suc i) vs)" (is "distinct(?xs@?ys)")
proof -
  from id_take_nth_drop[OF len] have vs[symmetric]: "vs = ?xs @ vs!i # ?ys" .
  with dist have "distinct ?xs" and "distinct(vs!i#?ys)" and "set ?xs  set(vs!i#?ys) = {}" using distinct_append[of ?xs "vs!i#?ys"] by auto
  hence "distinct ?ys" and "set ?xs  set ?ys = {}" by auto
  with distinct ?xs show ?thesis using distinct_append[of ?xs ?ys] vs by simp
qed

lemma map_nth_eq_conv:
  assumes len: "length xs = length ys"
  shows "(map f xs = ys) = (i<length ys. f (xs ! i) = ys ! i)" (is "?l = ?r")
proof -
  have "(map f xs = ys) = (map f xs = map id ys)" by auto
  also have "... = ( i < length ys. f (xs ! i) = id (ys ! i))" 
    using map_nth_conv[of f xs id ys] nth_map_conv[OF len, of f id] unfolding len
    by blast
  finally  show ?thesis by auto
qed

lemma map_upt_len_conv: 
  "map (λ i . f (xs!i)) [0..<length xs] = map f xs"
  by (rule nth_equalityI, auto)

lemma map_upt_add':
  "map f [a..<a+b] = map (λ i. f (a + i)) [0..<b]"
  by (induct b, auto)


definition generate_lists :: "nat  'a list  'a list list"
  where "generate_lists n xs  concat_lists (map (λ _. xs) [0 ..< n])"

lemma set_generate_lists[simp]: "set (generate_lists n xs) = {as. length as = n  set as  set xs}"
proof -
  {
    fix as
    have "(length as = n  (i<n. as ! i  set xs)) = (length as = n  set as  set xs)"
    proof -
      {
        assume "length as = n"
        hence n: "n = length as" by auto
        have "(i<n. as ! i  set xs) = (set as  set xs)" unfolding n
          unfolding all_set_conv_all_nth[of as "λ x. x  set xs", symmetric] by auto
      }
      thus ?thesis by auto
    qed
  }
  thus ?thesis unfolding generate_lists_def unfolding set_concat_lists by auto
qed

lemma nth_append_take:
  assumes "i  length xs" shows "(take i xs @ y#ys)!i = y"
proof -
  from assms have a: "length(take i xs) = i" by simp
  have "(take i xs @ y#ys)!(length(take i xs)) = y" by (rule nth_append_length)
  thus ?thesis unfolding a .
qed

lemma nth_append_take_is_nth_conv:
  assumes "i < j" and "j  length xs" shows "(take j xs @ ys)!i = xs!i"
proof -
  from assms have "i < length(take j xs)" by simp
  hence "(take j xs @ ys)!i = take j xs ! i" unfolding nth_append by simp
  thus ?thesis unfolding nth_take[OF assms(1)] .
qed

lemma nth_append_drop_is_nth_conv:
  assumes "j < i" and "j  length xs" and "i  length xs"
  shows "(take j xs @ y # drop (Suc j) xs)!i = xs!i"
proof -
  from j < i obtain n where ij: "Suc(j + n) = i" using less_imp_Suc_add by auto
  with assms have i: "i = length(take j xs) + Suc n" by auto
  have len: "Suc j + n  length xs" using assms i by auto
  have "(take j xs @ y # drop (Suc j) xs)!i =
    (y # drop (Suc j) xs)!(i - length(take j xs))" unfolding nth_append i by auto
  also have " = (y # drop (Suc j) xs)!(Suc n)" unfolding i by simp
  also have " = (drop (Suc j) xs)!n" by simp
  finally show ?thesis using ij len by simp
qed

lemma nth_append_take_drop_is_nth_conv: 
 assumes "i  length xs" and "j  length xs" and "i  j" 
 shows "(take j xs @ y # drop (Suc j) xs)!i = xs!i"
proof -
 from assms have "i < j  i > j" by auto
 thus ?thesis using assms 
   by (auto simp: nth_append_take_is_nth_conv nth_append_drop_is_nth_conv)
qed
  
lemma take_drop_imp_nth: "take i ss @ x # drop (Suc i) ss = ss  x = ss!i"
proof (induct ss arbitrary: i)
 case (Cons s ss)
 from take i (s#ss) @ x # drop (Suc i) (s#ss) = (s#ss) show ?case
 proof (induct i)
  case (Suc i)
  from Cons have IH: "take i ss @ x # drop (Suc i) ss = ss  x = ss!i" by auto
  from Suc have "take i ss @ x # drop (Suc i) ss = ss" by auto
  with IH show ?case by auto
 qed auto
qed auto

lemma take_drop_update_first: assumes "j < length ds" and "length cs = length ds"
  shows "(take j ds @ drop j cs)[j := ds ! j] = take (Suc j) ds @ drop (Suc j) cs" 
using assms
proof (induct j arbitrary: ds cs)
  case 0
  then obtain d dds c ccs where ds: "ds = d # dds" and cs: "cs = c # ccs" by (cases ds, simp, cases cs, auto)
  show ?case unfolding ds cs by auto
next
  case (Suc j)
  then obtain d dds c ccs where ds: "ds = d # dds" and cs: "cs = c # ccs" by (cases ds, simp, cases cs, auto)
  from Suc(1)[of dds ccs] Suc(2) Suc(3) show ?case unfolding ds cs by auto
qed

lemma take_drop_update_second: assumes "j < length ds" and "length cs = length ds"
  shows "(take j ds @ drop j cs)[j := cs ! j] = take j ds @ drop j cs"
using assms
proof (induct j arbitrary: ds cs)
  case 0
  then obtain d dds c ccs where ds: "ds = d # dds" and cs: "cs = c # ccs" by (cases ds, simp, cases cs, auto)
  show ?case unfolding ds cs by auto
next
  case (Suc j)
  then obtain d dds c ccs where ds: "ds = d # dds" and cs: "cs = c # ccs" by (cases ds, simp, cases cs, auto)
  from Suc(1)[of dds ccs] Suc(2) Suc(3) show ?case unfolding ds cs by auto
qed


lemma nth_take_prefix:
 "length ys  length xs  i < length ys. xs!i = ys!i  take (length ys) xs = ys"
proof (induct xs ys rule: list_induct2')
  case (4 x xs y ys)
  have "take (length ys) xs = ys"
    by (rule 4(1), insert 4(2-3), auto)
  moreover from 4(3) have "x = y" by auto
  ultimately show ?case by auto
qed auto


lemma take_upt_idx:
  assumes i: "i < length ls"
  shows "take i ls = [ ls ! j . j  [0..<i]]" 
proof -
  have e: "0 + i  i" by auto
  show ?thesis 
    using take_upt[OF e] take_map map_nth
    by (metis (opaque_lifting, no_types) add.left_neutral i nat_less_le take_upt)
qed


fun distinct_eq :: "('a  'a  bool)  'a list  bool" where
  "distinct_eq _ [] = True"
| "distinct_eq eq (x # xs) = (( y  set xs. ¬ (eq y x))  distinct_eq eq xs)"

lemma distinct_eq_append: "distinct_eq eq (xs @ ys) = (distinct_eq eq xs  distinct_eq eq ys  ( x  set xs.  y  set ys. ¬ (eq y x)))"
  by (induct xs, auto)

lemma append_Cons_nth_left:
  assumes "i < length xs"
  shows "(xs @ u # ys) ! i = xs ! i"
  using assms nth_append[of xs _ i] by simp

lemma append_Cons_nth_middle:
  assumes "i = length xs"
  shows "(xs @ y # zs) ! i = y"
using assms by auto

lemma append_Cons_nth_right:
  assumes "i > length xs"
  shows "(xs @ u # ys) ! i = (xs @ z # ys) ! i"
  by (simp add: assms nth_append)

lemma append_Cons_nth_not_middle:
  assumes "i  length xs"
  shows "(xs @ u # ys) ! i = (xs @ z # ys) ! i"
  by (metis assms list_update_length nth_list_update_neq)

lemmas append_Cons_nth = append_Cons_nth_middle append_Cons_nth_not_middle

lemma concat_all_nth:
  assumes "length xs = length ys"
    and "i. i < length xs  length (xs ! i) = length (ys ! i)"
    and "i j. i < length xs  j < length (xs ! i)  P (xs ! i ! j) (ys ! i ! j)"
  shows "k<length (concat xs). P (concat xs ! k) (concat ys ! k)" 
  using assms
proof (induct xs ys rule: list_induct2)
  case (Cons x xs y ys)
  from Cons(3)[of 0] have xy: "length x = length y" by simp
  from Cons(4)[of 0] xy have pxy: " j. j < length x  P (x ! j) (y ! j)" by auto
  {
    fix i
    assume i: "i < length xs"
    with Cons(3)[of "Suc i"] 
    have len: "length (xs ! i) = length (ys ! i)" by simp
    from Cons(4)[of "Suc i"] i have " j. j < length (xs ! i)  P (xs ! i ! j) (ys ! i ! j)"
      by auto
    note len and this
  } 
  from Cons(2)[OF this] have ind: " k. k < length (concat xs)  P (concat xs ! k) (concat ys ! k)" 
    by auto
  show ?case unfolding concat.simps
  proof (intro allI impI) 
    fix k
    assume k: "k < length (x @ concat xs)"
    show "P ((x @ concat xs) ! k) ((y @ concat ys) ! k)"
    proof (cases "k < length x")
      case True
      show ?thesis unfolding nth_append using True xy pxy[OF True]
        by simp
    next
      case False
      with k have "k - (length x) < length (concat xs)" by auto
      then obtain n where n: "k - length x = n" and nxs: "n < length (concat xs)" by auto
      show ?thesis unfolding nth_append n n[unfolded xy] using False xy ind[OF nxs]
        by auto
    qed
  qed
qed auto

lemma eq_length_concat_nth:
  assumes "length xs = length ys"
    and "i. i < length xs  length (xs ! i) = length (ys ! i)"
  shows "length (concat xs) = length (concat ys)"
using assms
proof (induct xs ys rule: list_induct2)
  case (Cons x xs y ys)
  from Cons(3)[of 0] have xy: "length x = length y" by simp
  {
    fix i
    assume "i < length xs"
    with Cons(3)[of "Suc i"] 
    have "length (xs ! i) = length (ys ! i)" by simp
  } 
  from Cons(2)[OF this] have ind: "length (concat xs) = length (concat ys)" by simp
  show ?case using xy ind by auto
qed auto

primrec
  list_union :: "'a list  'a list  'a list"
where
  "list_union [] ys = ys"
| "list_union (x # xs) ys = (let zs = list_union xs ys in if x  set zs then zs else x # zs)"

lemma set_list_union[simp]: "set (list_union xs ys) = set xs  set ys"
proof (induct xs)
  case (Cons x xs) thus ?case by (cases "x  set (list_union xs ys)") (auto)
qed simp

declare list_union.simps[simp del]

(*Why was list_inter thrown out of List.thy?*)
fun list_inter :: "'a list  'a list  'a list" where
  "list_inter [] bs = []"
| "list_inter (a#as) bs =
    (if a  set bs then a # list_inter as bs else list_inter as bs)"

lemma set_list_inter[simp]:
  "set (list_inter xs ys) = set xs  set ys"
  by (induct rule: list_inter.induct) simp_all

declare list_inter.simps[simp del]

primrec list_diff :: "'a list  'a list  'a list" where
  "list_diff [] ys = []"
| "list_diff (x # xs) ys = (let zs = list_diff xs ys in if x  set ys then zs else x # zs)"

lemma set_list_diff[simp]:
  "set (list_diff xs ys) = set xs - set ys"
proof (induct xs)
  case (Cons x xs) thus ?case by (cases "x  set ys") (auto)
qed simp

declare list_diff.simps[simp del]

lemma nth_drop_0: "0 < length ss  (ss!0)#drop (Suc 0) ss = ss"
  by (simp add: Cons_nth_drop_Suc)


lemma set_foldr_remdups_set_map_conv[simp]:
  "set (foldr (λx xs. remdups (f x @ xs)) xs []) = (set (map (set  f) xs))"
  by (induct xs) auto


lemma subset_set_code[code_unfold]: "set xs  set ys  list_all (λx. x  set ys) xs"
  unfolding list_all_iff by auto

fun union_list_sorted where
  "union_list_sorted (x # xs) (y # ys) = 
   (if x = y then x # union_list_sorted xs ys 
    else if x < y then x # union_list_sorted xs (y # ys)
    else y # union_list_sorted (x # xs) ys)"
| "union_list_sorted [] ys = ys"
| "union_list_sorted xs [] = xs"

lemma [simp]: "set (union_list_sorted xs ys) = set xs  set ys"
  by (induct xs ys rule: union_list_sorted.induct, auto)

fun subtract_list_sorted :: "('a :: linorder) list  'a list  'a list" where
  "subtract_list_sorted (x # xs) (y # ys) = 
   (if x = y then subtract_list_sorted xs (y # ys) 
    else if x < y then x # subtract_list_sorted xs (y # ys)
    else subtract_list_sorted (x # xs) ys)"
| "subtract_list_sorted [] ys = []"
| "subtract_list_sorted xs [] = xs"

lemma set_subtract_list_sorted[simp]: "sorted xs  sorted ys 
  set (subtract_list_sorted xs ys) = set xs - set ys"
proof (induct xs ys rule: subtract_list_sorted.induct)
  case (1 x xs y ys)
  have xxs: "sorted (x # xs)" by fact 
  have yys: "sorted (y # ys)" by fact
  have xs: "sorted xs" using xxs by (simp)
  show ?case
  proof (cases "x = y")
    case True
    thus ?thesis using 1(1)[OF True xs yys] by auto
  next 
    case False note neq = this
    note IH = 1(2-3)[OF this]
    show ?thesis 
      by (cases "x < y", insert IH xxs yys False, auto)
  qed
qed auto  

lemma subset_subtract_listed_sorted: "set (subtract_list_sorted xs ys)  set xs"
  by (induct xs ys rule: subtract_list_sorted.induct, auto)

lemma set_subtract_list_distinct[simp]: "distinct xs  distinct (subtract_list_sorted xs ys)"
  by (induct xs ys rule: subtract_list_sorted.induct, insert subset_subtract_listed_sorted, auto)

definition "remdups_sort xs = remdups_adj (sort xs)"

lemma remdups_sort[simp]: "sorted (remdups_sort xs)" "set (remdups_sort xs) = set xs"
  "distinct (remdups_sort xs)"
  by (simp_all add: remdups_sort_def)

text ‹maximum and minimum›
lemma max_list_mono: assumes " x. x  set xs - set ys   y. y  set ys  x  y"
  shows "max_list xs  max_list ys"
  using assms
proof (induct xs)
  case (Cons x xs)
  have "x  max_list ys"
  proof (cases "x  set ys")
    case True
    from max_list[OF this] show ?thesis .
  next
    case False
    with Cons(2)[of x] obtain y where y: "y  set ys"
      and xy: "x  y" by auto
    from xy max_list[OF y] show ?thesis by arith
  qed
  moreover have "max_list xs  max_list ys"
    by (rule Cons(1)[OF Cons(2)], auto)
  ultimately show ?case by auto
qed auto

fun min_list :: "('a :: linorder) list  'a" where
  "min_list [x] = x"
| "min_list (x # xs) = min x (min_list xs)"

lemma min_list: "(x :: 'a :: linorder)  set xs  min_list xs  x"
proof (induct xs)
  case oCons : (Cons y ys) 
  show ?case
  proof (cases ys)
    case Nil
    thus ?thesis using oCons by auto
  next
    case (Cons z zs)
    hence "min_list (y # ys) = min y (min_list ys)" 
      by auto
    then show ?thesis
      using min_le_iff_disj oCons.hyps oCons.prems by auto 
  qed
qed simp

lemma min_list_Cons:
  assumes xy: "x  y"
    and len: "length xs = length ys"
    and xsys: "min_list xs  min_list ys"
  shows "min_list (x # xs)  min_list (y # ys)"
  by (metis min_list.simps len length_greater_0_conv min.mono nth_drop_0 xsys xy)

lemma min_list_nth:
  assumes "length xs = length ys"
    and "i. i < length ys  xs ! i  ys ! i"
  shows "min_list xs  min_list ys"
using assms
proof (induct xs arbitrary: ys)
  case (Cons x xs zs)
  from Cons(2) obtain y ys where zs: "zs = y # ys" by (cases zs, auto)
  note Cons = Cons[unfolded zs]
  from Cons(2) have len: "length xs = length ys" by simp
  from Cons(3)[of 0] have xy: "x  y" by simp
  {
    fix i
    assume "i < length xs"
    with Cons(3)[of "Suc i"] Cons(2)
    have "xs ! i  ys ! i" by simp
  } 
  from Cons(1)[OF len this] Cons(2) have ind: "min_list xs  min_list ys" by simp
  show ?case unfolding zs
    by (rule min_list_Cons[OF xy len ind])
qed auto

lemma min_list_ex:
  assumes "xs  []" shows "xset xs. min_list xs = x"
  using assms
proof (induct xs)
  case oCons : (Cons x xs) 
  show ?case
  proof (cases xs)
    case (Cons y ys)
    hence id: "min_list (x # xs) = min x (min_list xs)" and nNil: "xs  []" by auto
    show ?thesis
    proof (cases "x  min_list xs")
      case True
      show ?thesis unfolding id 
        by (rule bexI[of _ x], insert True, auto simp: min_def)
    next
      case False
      show ?thesis unfolding id min_def
        using oCons(1)[OF nNil] False by auto
    qed
  qed auto
qed auto

lemma min_list_subset:
  assumes subset: "set ys  set xs" and mem: "min_list xs  set ys"
  shows "min_list xs = min_list ys"
  by (metis antisym empty_iff empty_set mem min_list min_list_ex subset subsetD)

text‹Apply a permutation to a list.›

primrec permut_aux :: "'a list  (nat  nat)  'a list  'a list" where
  "permut_aux [] _ _ = []" |
  "permut_aux (a # as) f bs = (bs ! f 0) # (permut_aux as (λn. f (Suc n)) bs)"

definition permut :: "'a list  (nat  nat)  'a list" where
  "permut as f = permut_aux as f as"
declare permut_def[simp]

lemma permut_aux_sound:
  assumes "i < length as"
  shows "permut_aux as f bs ! i = bs ! (f i)"
using assms proof (induct as arbitrary: i f bs)
  case (Cons x xs)
  show ?case 
  proof (cases i)
    case (Suc j)
    with Cons(2) have "j < length xs" by simp
    from Cons(1)[OF this] and Suc show ?thesis by simp
  qed simp
qed simp

lemma permut_sound:
  assumes "i < length as"
  shows "permut as f ! i = as ! (f i)"
using assms and permut_aux_sound by simp

lemma permut_aux_length:
  assumes "bij_betw f {..<length as} {..<length bs}"
  shows "length (permut_aux as f bs) = length as"
by (induct as arbitrary: f bs, simp_all)

lemma permut_length:
  assumes "bij_betw f {..< length as} {..< length as}"
  shows "length (permut as f) = length as"
  using permut_aux_length[OF assms] by simp
 
declare permut_def[simp del]

lemma foldl_assoc:
  fixes b :: "('a  'a)  ('a  'a)  'a  'a" (infixl "" 55)
  assumes "f g h. f  (g  h) = f  g  h"
  shows "foldl (⋅) (x  y) zs = x  foldl (⋅) y zs"
  using assms[symmetric] by (induct zs arbitrary: y) simp_all

lemma foldr_assoc:
  assumes "f g h. b (b f g) h = b f (b g h)"
  shows "foldr b xs (b y z) = b (foldr b xs y) z"
  using assms by (induct xs) simp_all

lemma foldl_foldr_o_id:
  "foldl (∘) id fs = foldr (∘) fs id"
proof (induct fs)
  case (Cons f fs)
  have "id  f = f  id" by simp
  with Cons [symmetric] show ?case
    by (simp only: foldl_Cons foldr_Cons o_apply [of _ _ id] foldl_assoc o_assoc)
qed simp

lemma foldr_o_o_id[simp]:
  "foldr ((∘)  f) xs id a = foldr f xs a"
  by (induct xs) simp_all

lemma Ex_list_of_length_P:
  assumes "i<n. x. P x i"
  shows "xs. length xs = n  (i<n. P (xs ! i) i)"
proof -
  from assms have " i.  x. i < n  P x i" by simp
  from choice[OF this] obtain xs where xs: " i. i < n  P (xs i) i" by auto
  show ?thesis
    by (rule exI[of _ "map xs [0 ..< n]"], insert xs, auto)
qed

lemma ex_set_conv_ex_nth: "(xset xs. P x) = (i<length xs. P (xs ! i))"
  using in_set_conv_nth[of _ xs] by force

lemma map_eq_set_zipD [dest]:
  assumes "map f xs = map f ys"
    and "(x, y)  set (zip xs ys)"
  shows "f x = f y"
using assms
proof (induct xs arbitrary: ys)
  case (Cons x xs)
  then show ?case by (cases ys) auto
qed simp

fun span :: "('a  bool)  'a list  'a list × 'a list" where
  "span P (x # xs) =
    (if P x then let (ys, zs) = span P xs in (x # ys, zs)
    else ([], x # xs))" |
  "span _ [] = ([], [])"

lemma span[simp]: "span P xs = (takeWhile P xs, dropWhile P xs)"
  by (induct xs, auto)

declare span.simps[simp del]

lemma parallel_list_update: assumes 
  one_update: " xs i y. length xs = n  i < n  r (xs ! i) y  p xs  p (xs[i := y])"
  and init: "length xs = n" "p xs"
  and rel: "length ys = n" " i. i < n  r (xs ! i) (ys ! i)"
  shows "p ys"
proof -
  note len = rel(1) init(1)
  {
    fix i
    assume "i  n"
    hence "p (take i ys @ drop i xs)"
    proof (induct i)
      case 0 with init show ?case by simp
    next
      case (Suc i)
      hence IH: "p (take i ys @ drop i xs)" by simp
      from Suc have i: "i < n" by simp
      let ?xs = "(take i ys @ drop i xs)"
      have "length ?xs = n" using i len by simp
      from one_update[OF this i _ IH, of "ys ! i"] rel(2)[OF i] i len
      show ?case by (simp add: nth_append take_drop_update_first)
    qed
  }
  from this[of n] show ?thesis using len by auto
qed

lemma nth_concat_two_lists: 
  "i < length (concat (xs :: 'a list list))  length (ys :: 'b list list) = length xs 
   ( i. i < length xs  length (ys ! i) = length (xs ! i))
    j k. j < length xs  k < length (xs ! j)  (concat xs) ! i = xs ! j ! k 
     (concat ys) ! i = ys ! j ! k"
proof (induct xs arbitrary: i ys)
  case (Cons x xs i yys)
  then obtain y ys where yys: "yys = y # ys" by (cases yys, auto)
  note Cons = Cons[unfolded yys]
  from Cons(4)[of 0] have [simp]: "length y = length x" by simp
  show ?case
  proof (cases "i < length x")
    case True
    show ?thesis unfolding yys
      by (rule exI[of _ 0], rule exI[of _ i], insert True Cons(2-4), auto simp: nth_append)
  next
    case False
    let ?i = "i - length x"
    from False Cons(2-3) have "?i < length (concat xs)" "length ys = length xs" by auto
    note IH = Cons(1)[OF this]
    {
      fix i
      assume "i < length xs"
      with Cons(4)[of "Suc i"] have "length (ys ! i) = length (xs ! i)" by simp
    }
    from IH[OF this]
    obtain j k where IH1: "j < length xs" "k < length (xs ! j)" 
      "concat xs ! ?i = xs ! j ! k"
      "concat ys ! ?i = ys ! j ! k" by auto
    show ?thesis unfolding yys
      by (rule exI[of _ "Suc j"], rule exI[of _ k], insert IH1 False, auto simp: nth_append)
  qed
qed simp

text ‹Removing duplicates w.r.t. some function.›
fun remdups_gen :: "('a  'b)  'a list  'a list" where
  "remdups_gen f [] = []"
| "remdups_gen f (x # xs) = x # remdups_gen f [y <- xs. ¬ f x = f y]"

lemma remdups_gen_subset: "set (remdups_gen f xs)  set xs"
  by (induct f xs rule: remdups_gen.induct, auto)

lemma remdups_gen_elem_imp_elem: "x  set (remdups_gen f xs)  x  set xs"
  using remdups_gen_subset[of f xs] by blast

lemma elem_imp_remdups_gen_elem: "x  set xs   y  set (remdups_gen f xs). f x = f y"
proof (induct f xs rule: remdups_gen.induct)
  case (2 f z zs)
  show ?case
  proof (cases "f x = f z")
    case False
    with 2(2) have "x  set [yzs . f z  f y]" by auto
    from 2(1)[OF this] show ?thesis by auto
  qed auto
qed auto


lemma take_nth_drop_concat:
  assumes "i < length xss" and "xss ! i = ys"
    and "j < length ys" and "ys ! j = z"
  shows "k < length (concat xss).
    take k (concat xss) = concat (take i xss) @ take j ys 
    concat xss ! k = xss ! i ! j 
    drop (Suc k) (concat xss) = drop (Suc j) ys @ concat (drop (Suc i) xss)"
using assms(1, 2)
proof (induct xss arbitrary: i rule: List.rev_induct)
  case (snoc xs xss)
  then show ?case using assms by (cases "i < length xss") (auto simp: nth_append)
qed simp

lemma concat_map_empty [simp]:
  "concat (map (λ_. []) xs) = []"
  by simp

lemma map_upt_len_same_len_conv:
  assumes "length xs = length ys"
  shows "map (λi. f (xs ! i)) [0 ..< length ys] = map f xs"
  unfolding assms [symmetric] by (rule map_upt_len_conv)

lemma concat_map_concat [simp]:
  "concat (map concat xs) = concat (concat xs)"
  by (induct xs) simp_all

lemma concat_concat_map:
  "concat (concat (map f xs)) = concat (map (concat  f) xs)"
  by (induct xs) simp_all

lemma UN_upt_len_conv [simp]:
  "length xs = n  (i  {0 ..< n}. f (xs ! i)) = (set (map f xs))"
  by (force simp: in_set_conv_nth)

lemma Ball_at_Least0LessThan_conv [simp]:
  "length xs = n 
    (i  {0 ..< n}. P (xs ! i))  (x  set xs. P x)"
  by (metis atLeast0LessThan in_set_conv_nth lessThan_iff)

lemma sum_list_replicate_length [simp]:
  "sum_list (replicate (length xs) (Suc 0)) = length xs"
  by (induct xs) simp_all

lemma list_all2_in_set2:
  assumes "list_all2 P xs ys" and "y  set ys"
  obtains x where "x  set xs" and "P x y"
  using assms by (induct) auto

lemma map_eq_conv':
  "map f xs = map g ys  length xs = length ys  (i < length xs. f (xs ! i) = g (ys ! i))"
  using map_equality_iff map_equality_iff nth_map_conv by auto


lemma list_3_cases[case_names Nil 1 2]:
  assumes "xs = []  P"
      and "x. xs = [x]  P"
      and "x y ys. xs = x#y#ys  P"
  shows P
  using assms by (rule remdups_adj.cases)

lemma list_4_cases[case_names Nil 1 2 3]:
  assumes "xs = []  P"
      and "x. xs = [x]  P"
      and "x y. xs = [x,y]  P"
      and "x y z zs. xs = x # y # z # zs  P"
  shows P
  using assms by (cases xs; cases "tl xs"; cases "tl (tl xs)", auto)

lemma foldr_append2 [simp]:
  "foldr ((@)  f) xs (ys @ zs) = foldr ((@)  f) xs ys @ zs"
  by (induct xs) simp_all

lemma foldr_append2_Nil [simp]:
  "foldr ((@)  f) xs [] @ zs = foldr ((@)  f) xs zs"
  unfolding foldr_append2 [symmetric] by simp

lemma UNION_set_zip:
  "(x  set (zip [0..<length xs] (map f xs)). g x) = (i < length xs. g (i, f (xs ! i)))"
  by (auto simp: set_conv_nth)

lemma zip_fst: "p  set (zip as bs)  fst p  set as"
  by (metis in_set_zipE prod.collapse)

lemma zip_snd: "p  set (zip as bs)  snd p  set bs"
  by (metis in_set_zipE prod.collapse)

lemma zip_size_aux: "size_list (size o snd) (zip ts ls)  (size_list size ls)"
proof (induct ls arbitrary: ts)
  case (Cons l ls ts)
  thus ?case by (cases ts, auto)
qed auto

text‹We definie the function that remove the nth element of
a list. It uses take and drop and the soundness is therefore not
too hard to prove thanks to the already existing lemmas.›

definition remove_nth :: "nat  'a list  'a list" where
  "remove_nth n xs  (take n xs) @ (drop (Suc n) xs)"

declare remove_nth_def[simp]

lemma remove_nth_len:
  assumes i: "i < length xs"
  shows "length xs = Suc (length (remove_nth i xs))"
proof -
  show ?thesis unfolding arg_cong[where f = "length", OF id_take_nth_drop[OF i]]
    unfolding remove_nth_def by simp
qed

lemma remove_nth_length :
  assumes n_bd: "n < length xs"
  shows "length (remove_nth n xs) = length xs - 1"
  using n_bd by force

lemma remove_nth_id : "length xs  n  remove_nth n xs = xs"
  by simp

lemma remove_nth_sound_l :
  assumes p_ub: "p < n"
  shows "(remove_nth n xs) ! p = xs ! p"
proof (cases "n < length xs")
 case True  
  from length_take and True have ltk: "length (take n xs) = n" by simp
   {
     assume pltn: "p < n"
     from this and ltk have plttk: "p < length (take n xs)" by simp
     with nth_append[of "take n xs" _ p]
     have "((take n xs) @ (drop (Suc n) xs)) ! p = take n xs ! p" by auto
     with pltn and nth_take have "((take n xs) @ (drop (Suc n) xs)) ! p =  xs ! p" by simp
   }
  from this and ltk and p_ub show ?thesis by simp
 next
 case False
  hence "length xs  n" by arith
  with remove_nth_id show ?thesis by force
qed

lemma remove_nth_sound_r :
  assumes "n  p" and "p < length xs"
  shows "(remove_nth n xs) ! p = xs ! (Suc p)"
proof-
 from n  p and p < length xs have n_ub: "n < length xs" by arith
 from length_take and n_ub have ltk: "length (take n xs) = n" by simp
 from n  p and ltk and nth_append[of "take n xs" _ p]
 have Hrew: "((take n xs) @ (drop (Suc n) xs)) ! p = drop (Suc n) xs ! (p - n)" by auto
 from n  p have idx: "Suc n + (p - n) = Suc p" by arith
 from p < length xs have Sp_ub: "Suc p  length xs" by arith
 from idx and Sp_ub and nth_drop have Hrew': "drop (Suc n) xs ! (p - n) = xs ! (Suc p)" by simp
 from Hrew and Hrew' show ?thesis by simp
qed

lemma nth_remove_nth_conv:
  assumes "i < length (remove_nth n xs)"
  shows "remove_nth n xs ! i = xs ! (if i < n then i else Suc i)"
using assms remove_nth_sound_l remove_nth_sound_r[of n i xs] by auto

lemma remove_nth_P_compat :
  assumes aslbs: "length as = length bs"
  and Pab: "i. i < length as  P (as ! i) (bs ! i)"
  shows "i. i < length (remove_nth p as)  P (remove_nth p as ! i) (remove_nth p bs ! i)"
proof (cases "p < length as")
 case True
  hence p_ub: "p < length as" by assumption
  with remove_nth_length have lr_ub: "length (remove_nth p as) = length as - 1" by auto
  {
    fix i assume i_ub: "i < length (remove_nth p as)"
    have "P (remove_nth p as ! i) (remove_nth p bs ! i)"
     proof (cases "i < p")
     case True
      from i_ub and lr_ub have i_ub2: "i < length as" by arith
      from i_ub2 and Pab have P: "P (as ! i) (bs ! i)" by blast
      from P and remove_nth_sound_l[OF True, of as] and remove_nth_sound_l[OF True, of bs]
      show ?thesis by simp
     next
     case False
      hence p_ub2: "p  i" by arith
      from i_ub and lr_ub have Si_ub: "Suc i < length as" by arith
      with Pab have P: "P (as ! Suc i) (bs ! Suc i)" by blast
      from i_ub and lr_ub have i_uba: "i < length as" by arith
      from i_uba and aslbs have i_ubb: "i < length bs" by simp      
      from P and p_ub and aslbs and remove_nth_sound_r[OF p_ub2 i_uba]
       and remove_nth_sound_r[OF p_ub2 i_ubb]
       show ?thesis by auto
     qed
  }
  thus ?thesis by simp
 next    
 case False
  hence p_lba: "length as  p" by arith
  with aslbs have p_lbb: "length bs  p" by simp
  from remove_nth_id[OF p_lba] and remove_nth_id[OF p_lbb] and Pab
  show ?thesis by simp
qed

declare remove_nth_def[simp del]

definition adjust_idx :: "nat  nat  nat" where
  "adjust_idx i j  (if j < i then j else (Suc j))"

definition adjust_idx_rev :: "nat  nat  nat" where
  "adjust_idx_rev i j  (if j < i then j else j - Suc 0)"

lemma adjust_idx_rev1: "adjust_idx_rev i (adjust_idx i j) = j"
  using adjust_idx_def adjust_idx_rev_def by auto

lemma adjust_idx_rev2:
  assumes "j  i" shows "adjust_idx i (adjust_idx_rev i j) = j"
  using adjust_idx_def adjust_idx_rev_def assms by auto

lemma adjust_idx_i:
  "adjust_idx i j  i"
  using adjust_idx_def lessI less_irrefl_nat by auto

lemma adjust_idx_nth:
  assumes i: "i < length xs"
  shows "remove_nth i xs ! j = xs ! adjust_idx i j" (is "?l = ?r")
proof -
  let ?j = "adjust_idx i j"
  from i have ltake: "length (take i xs) = i" by simp
  note nth_xs = arg_cong[where f = "λ xs. xs ! ?j", OF id_take_nth_drop[OF i], unfolded nth_append ltake]
  show ?thesis
  proof (cases "j < i")
    case True
    hence j: "?j = j" unfolding adjust_idx_def by simp
    show ?thesis unfolding nth_xs unfolding j remove_nth_def nth_append ltake
      using True by simp
  next
    case False
    hence j: "?j = Suc j" unfolding adjust_idx_def by simp
    from i have lxs: "min (length xs) i = i" by simp
    show ?thesis unfolding nth_xs unfolding j remove_nth_def nth_append
      using False by (simp add: lxs)
  qed
qed

lemma adjust_idx_rev_nth:
  assumes i: "i < length xs"
    and ji: "j  i"
  shows "remove_nth i xs ! adjust_idx_rev i j = xs ! j" (is "?l = ?r")
  by (simp add: adjust_idx_nth adjust_idx_rev2 i ji)

lemma adjust_idx_length:
  assumes i: "i < length xs"
    and j: "j < length (remove_nth i xs)"
  shows "adjust_idx i j < length xs"
  using adjust_idx_def i j remove_nth_len by fastforce

lemma adjust_idx_rev_length:
  assumes "i < length xs"
    and "j < length xs"
    and "j  i"
  shows "adjust_idx_rev i j < length (remove_nth i xs)"
  by (metis adjust_idx_def adjust_idx_rev2 assms not_less_eq remove_nth_len)


text‹If a binary relation holds on two couples of lists, then it holds on
the concatenation of the two couples.›

lemma P_as_bs_extend:
  assumes lab: "length as = length bs"
  and lcd: "length cs = length ds"
  and nsab: "i. i < length bs  P (as ! i) (bs ! i)"
  and nscd: "i. i < length ds  P (cs ! i) (ds ! i)"
  shows "i. i < length (bs @ ds)  P ((as @ cs) ! i) ((bs @ ds) ! i)"
  by (simp add: lab nsab nscd nth_append)

text‹Extension of filter and partition to binary relations.›

fun filter2 :: "('a  'b  bool)  'a list  'b list  ('a list × 'b list)" where
  "filter2 P [] _ = ([], [])" |
  "filter2 P _ [] = ([], [])" |
  "filter2 P (a # as) (b # bs) = (if P a b
        then (a # fst (filter2 P as bs), b # snd (filter2 P as bs))
        else filter2 P as bs)"

lemma filter2_length:
  "length (fst (filter2 P as bs))  length (snd (filter2 P as bs))"
proof (induct as arbitrary: bs)
 case Nil
  show ?case by simp
 next
 case (Cons a as) note IH = this
  thus ?case proof (cases bs)
    case Nil
     thus ?thesis by simp
    next
    case (Cons b bs)
     thus ?thesis proof (cases "P a b")
       case True
        with Cons and IH show ?thesis by simp
       next
       case False
        with Cons and IH show ?thesis by simp
     qed
  qed
qed

lemma filter2_sound: "i. i < length (fst (filter2 P as bs))  P (fst (filter2 P as bs) ! i) (snd (filter2 P as bs) ! i)"
proof (induct as arbitrary: bs)
 case Nil
  thus ?case by simp
 next
 case (Cons a as) note IH = this
  thus ?case proof (cases bs)
    case Nil
     thus ?thesis by simp
    next
    case (Cons b bs)
     thus ?thesis proof (cases "P a b")
      case False
       with Cons and IH show ?thesis by simp
      next
      case True
       {
         fix i
         assume i_bd: "i < length (fst (filter2 P (a # as) (b # bs)))"
         have "P (fst (filter2 P (a # as) (b # bs)) ! i) (snd (filter2 P (a # as) (b # bs)) ! i)"         proof (cases i)
          case 0
           with True show ?thesis by simp
          next
          case (Suc j)
           with i_bd and True have "j < length (fst (filter2 P as bs))" by auto
           with Suc and IH and True show ?thesis by simp
         qed
       }
       with Cons show ?thesis by simp
     qed
 qed
qed

definition partition2 :: "('a  'b  bool)  'a list  'b list  ('a list × 'b list) × ('a list × 'b list)" where
  "partition2 P as bs  ((filter2 P as bs) , (filter2 (λa b. ¬ (P a b)) as bs))"

lemma partition2_sound_P: "i. i < length (fst (fst (partition2 P as bs))) 
  P (fst (fst (partition2 P as bs)) ! i) (snd (fst (partition2 P as bs)) ! i)"
  by (simp add: filter2_sound partition2_def)

lemma partition2_sound_nP: "i. i < length (fst (snd (partition2 P as bs))) 
  ¬ P (fst (snd (partition2 P as bs)) ! i) (snd (snd (partition2 P as bs)) ! i)"
  by (metis filter2_sound partition2_def snd_conv) 


text‹Membership decision function that actually returns the
value of the index where the value can be found.›

fun mem_idx :: "'a  'a list  nat Option.option" where
  "mem_idx _ []       = None" |
  "mem_idx x (a # as) = (if x = a then Some 0 else map_option Suc (mem_idx x as))"

lemma mem_idx_sound_output:
  assumes "mem_idx x as = Some i"
  shows "i < length as  as ! i = x"
using assms proof (induct as arbitrary: i)
  case Nil thus ?case by simp
  next
  case (Cons a as) note IH = this
   thus ?case proof (cases "x = a")
     case True with IH(2) show ?thesis by simp
     next
     case False note neq_x_a = this
      show ?thesis proof (cases "mem_idx x as")
       case None with IH(2) and neq_x_a show ?thesis by simp
       next
       case (Some j)
        with IH(2) and neq_x_a have "i = Suc j" by simp
        with IH(1) and Some show ?thesis by simp
      qed
   qed
qed

lemma mem_idx_sound_output2:
  assumes "mem_idx x as = Some i"
  shows "j. j < i  as ! j  x"
using assms proof (induct as arbitrary: i)
  case Nil thus ?case by simp
  next
  case (Cons a as) note IH = this
   thus ?case proof (cases "x = a")
     case True with IH show ?thesis by simp
     next
     case False note neq_x_a = this
      show ?thesis proof (cases "mem_idx x as")
       case None with IH(2) and neq_x_a show ?thesis by simp
       next
       case (Some j)
        with IH(2) and neq_x_a have eq_i_Sj: "i = Suc j" by simp
        {
          fix k assume k_bd: "k < i"
          have "(a # as) ! k  x"
          proof (cases k)
          case 0 with neq_x_a show ?thesis by simp
          next
          case (Suc l)
            with k_bd and eq_i_Sj have l_bd: "l < j" by arith
            with IH(1) and Some have "as ! l  x" by simp
            with Suc show ?thesis by simp
          qed
        }
        thus ?thesis by simp
      qed
   qed
qed

lemma mem_idx_sound:
 "(x  set as) = (i. mem_idx x as = Some i)"
proof (induct as)
 case Nil thus ?case by simp
 next
 case (Cons a as) note IH = this
  show ?case proof (cases "x = a")
   case True thus ?thesis by simp
   next
   case False
    {
      assume "x  set (a # as)"
       with False have "x  set as" by simp
       with IH obtain i where Some_i: "mem_idx x as = Some i" by auto
       with False have "mem_idx x (a # as) = Some (Suc i)" by simp
      hence "i. mem_idx x (a # as) = Some i" by simp
    }
    moreover
    {
      assume "i. mem_idx x (a # as) = Some i"
       then obtain i where Some_i: "mem_idx x (a # as) = Some i" by fast
       have "x  set as" proof (cases i)
         case 0 with mem_idx_sound_output[OF Some_i] and False show ?thesis by simp
         next
         case (Suc j)
          with Some_i and False have "mem_idx x as = Some j" by simp
          hence "i. mem_idx x as = Some i" by simp
          with IH show ?thesis by simp
       qed
       hence "x  set (a # as)" by simp
    }
    ultimately show ?thesis by fast
  qed
qed

lemma mem_idx_sound2:
  "(x  set as) = (mem_idx x as = None)"
  unfolding mem_idx_sound by auto

lemma sum_list_replicate_mono: assumes "w1  (w2 :: nat)"
  shows "sum_list (replicate n w1)  sum_list (replicate n w2)"
proof (induct n)
  case (Suc n)
  thus ?case using w1  w2 by auto
qed simp

lemma all_gt_0_sum_list_map:
  assumes *: "x. f x > (0::nat)"
    and x: "x  set xs" and len: "1 < length xs"
  shows "f x < (xxs. f x)"
  using x len
proof (induct xs)
  case (Cons y xs)
  show ?case
  proof (cases "y = x")
    case True
    with *[of "hd xs"] Cons(3) show ?thesis by (cases xs, auto)
  next
    case False
    with Cons(2) have x: "x  set xs" by auto
    then obtain z zs where xs: "xs = z # zs" by (cases xs, auto)
    show ?thesis
    proof (cases "length zs")
      case 0
      with x xs *[of y] show ?thesis by auto
    next
      case (Suc n)
      with xs have "1 < length xs" by auto
      from Cons(1)[OF x this] show ?thesis by simp
    qed
  qed
qed simp

lemma map_of_filter:
  assumes "P x"
  shows "map_of [(x',y)  ys. P x'] x = map_of ys x"
proof (induct ys)
  case (Cons xy ys)
  obtain x' y where xy: "xy = (x',y)" by force
  show ?case
    using assms local.Cons by auto
qed simp

lemma set_subset_insertI: "set xs  set (List.insert x xs)" 
  by auto

lemma set_removeAll_subset: "set (removeAll x xs)  set xs" 
  by auto

lemma map_of_append_Some:
  "map_of xs y = Some z  map_of (xs @ ys) y = Some z"
  by simp

lemma map_of_append_None:
  "map_of xs y = None  map_of (xs @ ys) y = map_of ys y"
  by (simp add: map_add_def)


end