Theory ListAux

(*  Author:     Gertrud Bauer, Tobias Nipkow
*)

section ‹Basic Functions Old and New›

theory ListAux
imports Main
begin

declare Let_def[simp]

subsection ‹HOL›

lemma pairD:  "(a,b) = p  a = fst p  b = snd p"
by auto


lemmas conj_aci = conj_comms conj_assoc conj_absorb conj_left_absorb

definition enum :: "nat  nat set" where
  [code_abbrev]: "enum n = {..<n}"

lemma [code]:
  "enum 0 = {}"
  "enum (Suc n) = insert n (enum n)"
  unfolding enum_def lessThan_0 lessThan_Suc by rule+


subsection ‹Lists›

declare List.member_def[simp] list_all_iff[simp] list_ex_iff[simp]


subsubsectionlength›

notation length  ("|_|")

lemma length3D: "|xs| = 3  x y z. xs = [x, y, z]"
apply (cases xs) apply simp
apply (case_tac list) apply simp
apply (case_tac lista) by simp_all

lemma length4D: "|xs| = 4   a b c d. xs = [a, b, c, d]"
 apply (case_tac xs) apply simp
 apply (case_tac list) apply simp
 apply (case_tac lista) apply simp
 apply (case_tac listb) by simp_all


subsubsection @{const filter}

lemma filter_emptyE[dest]: "(filter P xs = [])   x  set xs   ¬ P x" 
  by (simp add: filter_empty_conv)

lemma filter_comm: "[x  xs. P x  Q x] = [x  xs. Q x  P x]"
  by (simp add: conj_aci)

lemma filter_prop: "x  set [uys . P u]  P x"
proof (induct ys arbitrary: x)
  case Nil then show ?case by simp 
next 
  case Cons then show ?case by (auto split: if_split_asm)
qed
   
lemma filter_compl1: 
 "([xxs. P x] = []) = ([xxs. ¬ P x] = xs)" (is "?lhs = ?rhs")
proof
  show "?rhs  ?lhs" 
  proof (induct xs) 
    case Nil then show ?case by simp
  next
    case (Cons x xs) 
    have "[uxs . ¬ P u]  x # xs"
    proof 
      assume "[uxs . ¬ P u] = x # xs" 
      then have "|x # xs| = |[uxs . ¬ P u]|" by simp
      also have "...  |xs|" by simp 
      finally show False by simp 
    qed
    with Cons show ?case by auto  
  qed
next
  show "?lhs  ?rhs" 
    by (induct xs) (simp_all split: if_split_asm)
qed
lemma [simp]: "Not  (Not  P) = P"
  by (rule ext) simp

lemma filter_eqI: 
  "(v. v  set vs  P v = Q v)  [vvs . P v] = [vvs . Q v]"
  by (induct vs) simp_all

lemma filter_simp: "(x. x  set xs  P x)  [xxs. P x  Q x] = [xxs. Q x]"
 by (induct xs) auto

lemma filter_True_eq1: 
  "(length [yxs. P y] = length xs)  (y. y  set xs  P y)"
proof (induct xs)
  case Nil then show ?case by simp
next
  case (Cons x xs)
  have l: "length (filter P xs)  length xs"
    by (simp add: length_filter_le)
  have hyp: "length (filter P (x # xs)) = length (x # xs)" by fact
  then have "P x"  by (simp split: if_split_asm) (insert l, arith)
  moreover with hyp have "length (filter P xs) = length xs" 
    by (simp split: if_split_asm)
  moreover have "y  set (x#xs)" by fact
  ultimately show ?case by (auto dest: Cons(1))
qed

lemma [simp]: "[f x. x <- xs, P x] = [f x. x <- [x  xs. P x]]"
  by (induct xs) auto


subsubsection @{const concat}

syntax
  "_concat" :: "idt  'a list  'a list  'a list"  ("⨆⇘_ _ _" 10)
translations
  "⨆⇘xxsf" == "CONST concat [f. x <- xs]" 


subsubsection ‹List product›

definition listProd1 :: "'a  'b list  ('a × 'b) list" where
 "listProd1 a bs  [(a,b). b <- bs]"

definition listProd :: "'a list  'b list  ('a × 'b) list" (infix "×" 50) where
 "as × bs  ⨆⇘a  aslistProd1 a bs"

lemma(*<*)[simp]: (*>*) "set (xs × ys) = (set xs) × (set ys)" 
  by (auto simp: listProd_def listProd1_def)


subsubsection ‹Minimum and maximum›

primrec minimal:: "('a  nat)  'a list  'a" where
 "minimal m (x#xs) =
  (if xs=[] then x else
   let mxs = minimal m xs in
   if m x  m mxs then x else mxs)"


lemma minimal_in_set[simp]: "xs  []  minimal f xs : set xs"
by(induct xs) auto

primrec min_list :: "nat list  nat" where
  "min_list (x#xs) = (if xs=[] then x else min x (min_list xs))"

primrec max_list :: "nat list  nat" where
  "max_list (x#xs) = (if xs=[] then x else max x (max_list xs))"


lemma min_list_conv_Min[simp]:
 "xs  []  min_list xs = Min (set xs)"
by (induct xs) auto

lemma max_list_conv_Max[simp]:
 "xs  []  max_list xs = Max (set xs)"
by (induct xs) auto


subsubsection ‹replace›

primrec replace :: "'a  'a list  'a list   'a list" where
  "replace x ys [] = []"
| "replace x ys (z#zs) = 
     (if z = x then ys @ zs else z # (replace x ys zs))"

primrec mapAt :: "nat list  ('a  'a)  ('a list  'a list)" where
  "mapAt [] f as = as"
| "mapAt (n#ns) f as = 
     (if n < |as| then mapAt ns f (as[n:= f (as!n)])
     else mapAt ns f as)"


lemma length_mapAt[simp]: "xs. length(mapAt vs f xs) = length xs"
by(induct vs) auto

lemma length_replace1[simp]: "length(replace x [y] xs) = length xs"
by(induct xs) simp_all

lemma replace_id[simp]: "replace x [x] xs = xs"
by(induct xs) simp_all

lemma len_replace_ge_same:
"length ys  1  length(replace x ys xs)  length xs"
by (induct xs) auto

lemma len_replace_ge[simp]:
" length ys  1; length xs  length zs  
 length(replace x ys xs)  length zs"
apply(drule len_replace_ge_same[where x = x and xs = xs])
apply arith
done


lemma replace_append[simp]:
  "replace x ys (as @ bs) =
   (if x  set as then replace x ys as @ bs else as @ replace x ys bs)"
by(induct as) auto

lemma distinct_set_replace: "distinct xs 
 set (replace x ys xs) =
 (if x  set xs then (set xs - {x})  set ys else set xs)"
apply(induct xs)
 apply(simp)
apply simp
apply blast
done

lemma replace1:
 "f  set (replace f' fs ls )  f  set ls  f  set fs" 
proof (induct ls)
  case Nil then show ?case by simp
next
  case (Cons l ls) then show ?case by (simp split: if_split_asm)
qed

lemma replace2:
 "f'  set ls  replace f' fs ls  = ls" 
proof (induct ls)
  case Nil then show ?case by simp
next
  case (Cons l ls) then show ?case by (auto split: if_split_asm)
qed

lemma replace3[intro]:
  "f'  set ls  f  set fs  f  set (replace f' fs ls)"
by (induct ls) auto

lemma replace4:
  "f  set ls  oldF  f  f  set (replace oldF fs ls)" 
by (induct ls) auto

lemma replace5: "f  set (replace oldF newfs fs)  f  set fs  f  set newfs"
by (induct fs) (auto split: if_split_asm) 

lemma replace6: "distinct oldfs  x  set (replace oldF newfs oldfs) = 
  ((x  oldF  oldF  set newfs)  ((oldF  set oldfs  x  set newfs)  x  set oldfs))"
by (induct oldfs) auto


lemma distinct_replace: 
"distinct fs  distinct newFs  set fs  set newFs  {oldF} 
 distinct (replace oldF newFs fs)"
proof (induct fs)
  case Nil then show ?case by simp
next
  case (Cons f fs)
  then show ?case
  proof (cases "f = oldF") 
    case True with Cons show ?thesis by simp blast
  next
    case False 
    moreover with Cons have "f  set newFs" by simp blast
    with Cons have "f  set (replace oldF newFs fs)" 
     by simp (blast dest: replace1) 
    moreover from Cons have "distinct (replace oldF newFs fs)"
      by (rule_tac Cons) auto  
    ultimately show ?thesis by simp 
  qed
qed

lemma replace_replace[simp]: "oldf  set newfs  distinct xs  
  replace oldf newfs (replace oldf newfs xs) = replace oldf newfs xs"
apply (induct xs) apply auto apply (rule replace2) by simp 

lemma replace_distinct: "distinct fs  distinct newfs  oldf  set fs  set newfs  set fs  {oldf}  
  distinct (replace oldf newfs fs)"
apply (case_tac "oldf  set fs") apply simp
apply (induct fs) apply simp
apply (auto simp: replace2) apply (drule replace1)
by auto


lemma filter_replace2:
 " ¬ P x; y set ys. ¬ P y  
  filter P (replace x ys xs) = filter P xs"
apply(cases "x  set xs")
 prefer 2 apply(simp add:replace2)
apply(induct xs)
 apply simp
apply clarsimp
done

lemma length_filter_replace1:
 " x  set xs; ¬ P x  
  length(filter P (replace x ys xs)) =
  length(filter P xs) + length(filter P ys)"
apply(induct xs)
 apply simp
apply fastforce
done

lemma length_filter_replace2:
 " x  set xs; P x  
  length(filter P (replace x ys xs)) =
  length(filter P xs) + length(filter P ys) - 1"
apply(induct xs)
 apply simp
apply auto
apply(drule split_list)
apply clarsimp
done


subsubsection @{const"distinct"}

lemma dist_at1: " c vs. distinct vs  vs = a @ r # b  vs = c @ r # d  a = c"
proof (induct a)
  case Nil
  assume dist: "distinct vs" and vs1: "vs = [] @ r # b" and vs2: "vs = c @ r # d"
  from dist vs2 have rc: "r  set c" by auto
  from vs1 vs2 have "c @ r # d = r # b" by auto
  then have "hd (c @ r # d) = r" by auto
  then have "c  []  hd c = r" by auto
  then have "c  []  r  set c" by (induct c) auto
  with rc have c: "c = []" by auto
  then show ?case by auto
next
  case (Cons x xs) then show ?case by (induct c)  auto
qed

lemma dist_at: "distinct vs  vs = a @ r # b  vs = c @ r # d  a = c  b = d"
proof -
  assume dist: "distinct vs" and vs1: "vs = a @ r # b" and vs2: "vs = c @ r # d"
  then have "a = c" by (rule_tac dist_at1) auto
  with dist vs1 vs2 show ?thesis by simp
qed

lemma dist_at2: "distinct vs  vs = a @ r # b  vs = c @ r # d  b = d"
proof -
  assume dist: "distinct vs" and vs1: "vs = a @ r # b" and vs2: "vs = c @ r # d"
  then have "a = c  b = d" by (rule_tac dist_at) auto
  then show ?thesis by auto
qed

lemma distinct_split1: "distinct xs  xs = y @ [r] @ z   r  set y"
  apply auto done

lemma distinct_split2: "distinct xs  xs = y @ [r] @ z   r  set z" apply auto done

lemma distinct_hd_not_cons: "distinct vs   as bs. vs = as @ x # hd vs # bs  False"
proof -
  assume d: "distinct vs" and ex: " as bs. vs = as @ x # hd vs # bs"
  from ex have vsne: "vs  []" by auto
  with d ex show ?thesis apply (elim exE) apply (case_tac "as")
    apply (subgoal_tac "hd vs = x") apply simp apply (rule sym)  apply simp
    apply (subgoal_tac "x = hd (x # (hd vs # bs))") apply simp apply (thin_tac "vs = x # hd vs # bs")
    apply auto
    apply (subgoal_tac "hd vs = a") apply simp
    apply (subgoal_tac "a = hd (a # list @ x # hd vs # bs)") apply simp
    apply (thin_tac "vs = a # list @ x # hd vs # bs") by auto
qed

subsubsection ‹Misc›

(* FIXME move to List *)
lemma drop_last_in: "n. n < length ls  last ls  set (drop n ls)"
apply (frule_tac last_drop) apply(erule subst)
apply (case_tac "drop n ls" rule: rev_exhaust) by simp_all

lemma nth_last_Suc_n: "distinct ls  n < length ls  last ls = ls ! n  Suc n = length ls"
proof (rule ccontr)
  assume d: "distinct ls" and n: "n < length ls" and l: "last ls = ls ! n" and not: "Suc n  length ls"
  then have s: "Suc n < length ls" by auto
  define lls where  "lls = ls!n"
  with n have "take (Suc n) ls = take n ls @ [lls]" apply simp by (rule take_Suc_conv_app_nth)
  then have "take (Suc n) ls @ drop (Suc n) ls = take n ls @ [lls] @ drop (Suc n) ls" by auto
  then have ls: "ls = take n ls @ [lls] @ drop (Suc n) ls" by auto
  with d have dls: "distinct (take n ls @ [lls] @ drop (Suc n) ls)" by auto
  from lls_def l have "lls = (last ls)" by auto
  with s have "lls  set (drop (Suc n) ls)" apply simp by (rule_tac drop_last_in)
  with dls show False by auto
qed


(****************************** rotate *************************)

subsubsection @{const rotate}

lemma  plus_length1[simp]: "rotate (k+(length ls)) ls = rotate k ls "
proof -
  have " k ls. rotate k (rotate (length ls) ls) = rotate (k+(length ls)) ls"
    by (rule rotate_rotate)
  then have " k ls. rotate k ls =  rotate (k+(length ls)) ls" by auto
  then show ?thesis by (rule sym)
qed

lemma  plus_length2[simp]: "rotate ((length ls)+k) ls = rotate k ls "
proof -
  define x where "x = (length ls)+k"
  then have "x = k+(length ls)" by auto
  with x_def have "rotate x ls = rotate (k+(length ls)) ls" by simp
  then have "rotate x ls = rotate k ls" by simp
  with x_def show ?thesis by simp
qed

lemma rotate_minus1: "n > 0  m > 0 
 rotate n ls = rotate m ms  rotate (n - 1) ls = rotate (m - 1) ms"
proof (cases "ls = []")
  assume r: "rotate n ls = rotate m ms"
  case True with r
  have "rotate m ms = []" by auto
  then have "ms = []" by auto
  with True show ?thesis by auto
next
  assume n: "n > 0" and m: "m > 0" and r: "rotate n ls = rotate m ms"
  case False
  then have lls: "length ls > 0" by auto
  with r have lms: "length ms > 0" by auto
  have mem1: "rotate (n - 1) ls = rotate ((n - 1) + length ls) ls" by auto
  from n lls have "(n - 1) + length ls = (length ls - 1) + n" by arith
  then have "rotate ((n - 1) + length ls) ls = rotate ((length ls - 1) + n) ls" by auto
  with mem1 have mem2: "rotate (n - 1) ls = rotate ((length ls - 1) + n) ls" by auto
  have "rotate ((length ls - 1) + n) ls = rotate (length ls - 1) (rotate n ls)" apply (rule sym)
    by (rule rotate_rotate)
  with mem2 have mem3: "rotate (n - 1) ls = rotate (length ls - 1) (rotate n ls)" by auto
  from r have "rotate (length ls - 1) (rotate n ls) = rotate (length ls - 1) (rotate m ms)" by auto
  with mem3 have mem4: "rotate (n - 1) ls = rotate (length ls - 1) (rotate m ms)" by auto
  have "rotate (length ls - 1) (rotate m ms) = rotate (length ls - 1 + m) ms"  by (rule rotate_rotate)
  with mem4 have mem5: "rotate (n - 1) ls = rotate (length ls - 1 + m) ms" by auto
  from r have "length (rotate n ls) = length (rotate m ms)" by simp
  then have "length ls = length ms" by auto
  with m lms have "length ls - 1 + m = (m - 1) + length ms" by arith
  with mem5 have mem6: "rotate (n - 1) ls = rotate ((m - 1) + length ms) ms" by auto
  have "rotate ((m - 1) + length ms) ms = rotate (m - 1) (rotate (length ms) ms)" by auto
  then have "rotate ((m - 1) + length ms) ms = rotate (m - 1) ms" by auto
  with mem6 show ?thesis by auto
qed

lemma rotate_minus1': "n > 0  rotate n ls = ms 
  rotate (n - 1) ls = rotate (length ms - 1) ms"
proof (cases "ls = []")
  assume r: "rotate n ls = ms"
  case True with r show ?thesis by auto
next
  assume n: "n > 0" and r:"rotate n ls = ms"
  then have r': "rotate n ls = rotate (length ms) ms" by auto
  case False
  with n r' show ?thesis apply (rule_tac rotate_minus1) by auto
qed

lemma rotate_inv1: " ms. n < length ls  rotate n ls = ms 
  ls = rotate ((length ls) - n) ms"
proof (induct n)
  case 0 then show ?case by auto
next
  case (Suc n) then show ?case
  proof (cases "ls = []")
    case True with Suc
    show ?thesis by auto
  next
    case False
    then have ll: "length ls > 0" by auto
    from Suc have nl: "n < length ls" by auto
    from Suc have r: "rotate (Suc n) ls = ms" by auto
    then have "rotate (Suc n - 1) ls = rotate (length ms - 1) ms" apply (rule_tac rotate_minus1') by auto
    then have "rotate n ls = rotate (length ms - 1) ms" by auto
    then have mem: "ls = rotate (length ls - n) (rotate (length ms - 1) ms)"
      apply (rule_tac Suc) by (auto simp: nl)
    have " rotate (length ls - n) (rotate (length ms - 1) ms) = rotate (length ls - n + (length ms - 1)) ms"
      by (rule rotate_rotate)
    with mem have mem2: "ls =  rotate (length ls - n + (length ms - 1)) ms" by auto
    from r have leq: "length ms = length ls" by auto
    with False nl have "length ls - n + (length ms - 1) = length ms + (length ms - (Suc n))"
      by arith
    then have "rotate (length ls - n + (length ms - 1)) ms = rotate (length ms + (length ms - (Suc n))) ms"
      by auto
    with mem2 have mem3: "ls = rotate (length ms + (length ms - (Suc n))) ms" by auto
    have "rotate (length ms + (length ms - (Suc n))) ms = rotate (length ms - (Suc n)) ms" by simp
    with mem3 leq show ?thesis by auto
  qed
qed

lemma rotate_conv_mod'[simp]: "rotate (n mod length ls) ls = rotate n ls"
by(simp add:rotate_drop_take)

lemma rotate_inv2: "rotate n ls = ms 
 ls = rotate ((length ls) - (n mod length ls)) ms"
proof (cases "ls  = []")
  assume r: "rotate n ls = ms"
  case True with r show ?thesis by auto
next
  assume r: "rotate n ls = ms"
  then have r': "rotate (n mod length ls) ls = ms" by auto
  case False
  then have "length ls > 0" by auto
  with r' show ?thesis apply (rule_tac rotate_inv1) by auto
qed

lemma rotate_id[simp]: "rotate ((length ls) - (n mod length ls)) (rotate n ls) = ls"
apply (rule sym) apply (rule rotate_inv2) by simp

lemma nth_rotate1_Suc: "Suc n < length ls  ls!(Suc n) = (rotate1 ls)!n"
  apply (cases ls) apply auto
  by (simp add: nth_append)

lemma nth_rotate1_0: "ls!0 = (rotate1 ls)!(length ls - 1)" apply (cases ls)  by auto

lemma nth_rotate1: "0 < length ls  ls!((Suc n) mod (length ls)) = (rotate1 ls)!(n mod (length ls))"
proof (cases "0 < (Suc n) mod (length ls)")
  assume lls: "0 < length ls"
  case True
  define m where "m = (Suc n) mod (length ls) - 1"
  with True have m: "Suc m = (Suc n) mod (length ls)" by auto
  with lls have a: "(Suc m) <   length ls" by auto
  from lls m have "m = n mod (length ls)" by (simp add: mod_Suc split:if_split_asm)
  with a m show ?thesis apply (drule_tac nth_rotate1_Suc) by auto
next
  assume lls: "0 < length ls"
  case False
  then have a: "(Suc n) mod (length ls) = 0" by auto
  with lls have "Suc (n mod (length ls)) = (length ls)" by (auto simp: mod_Suc split: if_split_asm)
  then have "(n mod (length ls)) = (length ls) - 1" by arith
  with a show ?thesis by (auto simp: nth_rotate1_0)
qed

lemma rotate_Suc2[simp]: "rotate n (rotate1 xs) = rotate (Suc n) xs"
apply (simp add:rotate_def) apply (induct n) by auto

lemma nth_rotate: " ls. 0 < length ls  ls!((n+m) mod (length ls)) = (rotate m ls)!(n mod (length ls))"
proof (induct m)
  case 0 then show ?case by auto
next
  case (Suc m)
  define z where "z = n + m"
  then have "n + Suc m = Suc (z)" by auto
  with Suc have r1: "ls ! ((Suc z) mod length ls) = rotate1 ls ! (z mod length ls)"
    by (rule_tac nth_rotate1)
  from Suc have "0 < length (rotate1 ls)" by auto
  then have "(rotate1 ls) ! ((n + m) mod length (rotate1 ls))
    = rotate m (rotate1 ls) ! (n mod length (rotate1 ls))" by (rule Suc)
  with r1 z_def have "ls ! ((n + Suc m) mod length ls)
    = rotate m (rotate1 ls) ! (n mod length (rotate1 ls))" by auto
  then show ?case by auto
qed


(************************* SplitAt *******************************************)

subsection splitAt›

primrec splitAtRec :: "'a  'a list  'a list  'a list × 'a list" where
  "splitAtRec c bs [] = (bs,[])"
| "splitAtRec c bs (a#as) = (if a = c then (bs, as)
                              else splitAtRec c (bs@[a]) as)"

definition splitAt :: "'a  'a list  'a list × 'a list" where
  "splitAt c as   splitAtRec c [] as"


subsubsection @{const splitAtRec}

lemma splitAtRec_conv: "bs.
 splitAtRec x bs xs =
 (bs @ takeWhile (λy. yx) xs, tl(dropWhile (λy. yx) xs))"
by(induct xs) auto

lemma splitAtRec_distinct_fst: " s. distinct vs  distinct s  (set s)   (set vs) = {}  distinct (fst (splitAtRec ram1 s vs))"
by (induct vs) auto

lemma splitAtRec_distinct_snd: " s. distinct vs  distinct s  (set s)   (set vs) = {}  distinct (snd (splitAtRec ram1 s vs))"
by (induct vs) auto

lemma splitAtRec_ram:
  " us a b. ram  set vs  (a, b) = splitAtRec ram us vs 
  us @ vs = a @ [ram] @ b"
proof (induct vs)
case  Nil then show ?case by simp
next
case (Cons v vs) then show ?case by (auto dest: Cons(1) split: if_split_asm)
qed

lemma splitAtRec_notRam:
 " us. ram   set vs  splitAtRec ram us vs = (us @ vs, [])"
proof (induct vs)
case  Nil then show ?case by simp
next
case (Cons v vs) then show ?case by auto
qed

lemma splitAtRec_distinct: " s. distinct vs 
  distinct s  (set s)  (set vs) = {} 
  set (fst (splitAtRec ram s vs))  set (snd (splitAtRec ram s vs)) = {}"
by (induct vs) auto



subsubsection @{const splitAt}

lemma splitAt_conv:
 "splitAt x xs = (takeWhile (λy. yx) xs, tl(dropWhile (λy. yx) xs))"
by(simp add: splitAt_def splitAtRec_conv)

lemma splitAt_no_ram[simp]:
  "ram  set vs  splitAt ram vs = (vs, [])"
  by (auto simp: splitAt_def splitAtRec_notRam)

lemma splitAt_split:
  "ram  set vs  (a,b) = splitAt ram vs  vs = a @ ram # b"
  by (auto simp: splitAt_def dest: splitAtRec_ram)

lemma splitAt_ram:
  "ram  set vs  vs = fst (splitAt ram vs) @ ram # snd (splitAt ram vs)"
 by (rule_tac splitAt_split) auto

lemma fst_splitAt_last:
 " xs  []; distinct xs   fst (splitAt (last xs) xs) = butlast xs"
by(simp add:splitAt_conv takeWhile_not_last)


subsubsection ‹Sets›

lemma splitAtRec_union:
" a b s. (a,b) = splitAtRec ram s vs  (set a  set b) - {ram} = (set vs  set s) - {ram}"
  apply (induct vs) by (auto split: if_split_asm)

lemma splitAt_subset_ab:
  "(a,b) = splitAt ram vs  set a  set vs  set b  set vs"
  apply (cases "ram  set vs")
  by (auto dest: splitAt_split simp: splitAt_no_ram)

lemma splitAt_in_fst[dest]: "v  set (fst (splitAt ram vs))  v  set vs"
proof (cases "ram  set vs")
  assume v: "v  set (fst (splitAt ram vs))"
  define a where "a = fst (splitAt ram vs)"
  with v have vin: "v  set a" by auto
  define b where "b = snd (splitAt ram vs)"
  case True with a_def b_def  have "vs = a @ ram # b" by (auto dest: splitAt_ram)
  with vin show "v  set vs" by auto
next
  assume v: "v  set (fst (splitAt ram vs))"
  case False with v show ?thesis by (auto dest: splitAt_no_ram del: notI)
qed

lemma splitAt_not1:
"v  set vs  v  set (fst (splitAt ram vs))" by (auto dest: splitAt_in_fst)

lemma splitAt_in_snd[dest]: "v  set (snd (splitAt ram vs))  v  set vs"
proof (cases "ram  set vs")
  assume v: "v  set (snd (splitAt ram vs))"
  define a where "a = fst (splitAt ram vs)"
  define b where "b = snd (splitAt ram vs)"
  with v have vin: "v  set b" by auto
  case True with a_def b_def  have "vs = a @ ram # b" by (auto dest: splitAt_ram)
  with vin show "v  set vs" by auto
next
  assume v: "v  set (snd (splitAt ram vs))"
  case False with v show ?thesis by (auto dest: splitAt_no_ram del: notI)
qed


subsubsection ‹Distinctness›

lemma splitAt_distinct_ab_aux:
 "distinct vs  (a,b) = splitAt ram vs  distinct a  distinct b"
  by (cases "ram  set vs") (auto dest: splitAt_split simp: splitAt_no_ram)

lemma splitAt_distinct_fst_aux[intro]:
 "distinct vs  distinct (fst (splitAt ram vs))"
proof -
  assume d: "distinct vs"
  define b where "b = snd (splitAt ram vs)"
  define a where "a = fst (splitAt ram vs)"
  with b_def have "(a,b) = splitAt ram vs" by auto
  with a_def d show ?thesis  by (auto dest: splitAt_distinct_ab_aux)
qed

lemma splitAt_distinct_snd_aux[intro]:
 "distinct vs  distinct (snd (splitAt ram vs))"
proof -
  assume d: "distinct vs"
  define b where "b = snd (splitAt ram vs)"
  define a where "a = fst (splitAt ram vs)"
  with b_def have "(a,b) = splitAt ram vs" by auto
  with b_def d show ?thesis  by (auto dest: splitAt_distinct_ab_aux)
qed

lemma splitAt_distinct_ab:
  "distinct vs   (a,b) = splitAt ram vs  set a  set b = {}"
  apply (cases "ram  set vs") apply (drule_tac splitAt_split)
  by (auto simp: splitAt_no_ram)

lemma splitAt_distinct_fst_snd:
    "distinct vs   set (fst (splitAt ram vs))  set (snd (splitAt ram vs)) = {}"
  by (rule_tac splitAt_distinct_ab) simp_all

lemma splitAt_distinct_ram_fst[intro]:
  "distinct vs  ram  set (fst (splitAt ram vs))"
  apply (case_tac "ram  set vs") apply (drule_tac splitAt_ram)
  apply (rule distinct_split1) by (force dest: splitAt_in_fst)+
(*  apply (frule splitAt_no_ram) by auto  *)

lemma splitAt_distinct_ram_snd[intro]:
  "distinct vs  ram  set (snd (splitAt ram vs))"
  apply (case_tac "ram  set vs") apply (drule_tac splitAt_ram)
  apply (rule distinct_split2) by (force dest: splitAt_in_fst)+

lemma splitAt_1[simp]:
  "splitAt ram [] = ([],[])" by (simp add: splitAt_def)

lemma splitAt_2:
  "v  set vs  (a,b) = splitAt ram vs  v  set a  v  set b  v = ram "
apply (cases "ram  set vs")
 by (auto dest: splitAt_split simp: splitAt_no_ram)

lemma splitAt_distinct_fst: "distinct vs  distinct (fst (splitAt ram1 vs))"
by (simp add: splitAt_def splitAtRec_distinct_fst)

lemma splitAt_distinct_a: "distinct vs  (a,b) = splitAt ram vs  distinct a"
by (auto dest: splitAt_distinct_fst pairD)

lemma splitAt_distinct_snd: "distinct vs  distinct (snd (splitAt ram1 vs))"
by (simp add: splitAt_def splitAtRec_distinct_snd)

lemma splitAt_distinct_b: "distinct vs  (a,b) = splitAt ram vs  distinct b"
by (auto dest: splitAt_distinct_snd pairD)

lemma splitAt_distinct: "distinct vs  set (fst (splitAt ram vs))  set (snd (splitAt ram vs)) = {}"
by (simp add: splitAt_def splitAtRec_distinct)

lemma splitAt_subset: "(a,b) = splitAt ram vs  (set a  set vs)  (set b  set vs)"
apply (cases "ram  set vs") by (auto dest: splitAt_split simp: splitAt_no_ram)


subsubsection @{const splitAt} composition›

lemma set_help: "v  set ( as @ bs)  v  set as  v  set bs" by auto

lemma splitAt_elements: "ram1  set vs  ram2  set vs  ram2  set( fst (splitAt ram1 vs))  ram2  set [ram1]   ram2  set( snd (splitAt ram1 vs))"
proof -
  assume r1: "ram1  set vs" and r2: "ram2  set vs"
  then have "ram2  set( fst (splitAt ram1 vs) @ [ram1])   ram2  set( snd (splitAt ram1 vs))"
  apply (rule_tac set_help)
  apply (drule_tac splitAt_ram) by auto
  then show ?thesis by auto
qed

lemma splitAt_ram3: "ram2   set (fst (splitAt ram1 vs)) 
  ram1  set vs  ram2  set vs  ram1  ram2 
  ram2  set (snd (splitAt ram1 vs))" by (auto dest: splitAt_elements)

lemma splitAt_dist_ram: "distinct vs 
 vs = a @ ram # b  (a,b) = splitAt ram vs"
proof -
  assume dist: "distinct vs" and vs: "vs = a @ ram # b"
  from vs have r:"ram  set vs" by auto
  with dist vs have "fst (splitAt ram vs) = a" apply (drule_tac splitAt_ram) by (rule_tac dist_at1)  auto
  then have first:"a = fst (splitAt ram vs)" by   auto
  from r dist have second: "b = snd (splitAt ram vs)" apply (drule_tac splitAt_ram) apply (rule dist_at2) apply simp
    by (auto simp: vs)
  show ?thesis by (auto simp: first second)
qed

lemma distinct_unique1: "distinct vs  ram  set vs  ∃!s. vs = (fst s) @ ram # (snd s)"
proof
  assume d: "distinct vs" and r: "ram  set vs"
  define s where "s = splitAt ram vs"
  with r show  "vs = (fst s) @ ram # (snd s)"
    by (auto intro: splitAt_ram)
next
  fix s
  assume d: "distinct vs" and vs1: "vs = fst s @ ram # snd s"
  from d vs1 show "s = splitAt ram vs" apply (drule_tac splitAt_dist_ram) apply simp by simp
qed

lemma splitAt_dist_ram2: "distinct vs  vs = a @ ram1 # b @ ram2 # c 
 (a @ ram1 # b, c) = splitAt ram2 vs"
by (auto intro: splitAt_dist_ram)

lemma splitAt_dist_ram20: "distinct vs  vs = a @ ram1 # b @ ram2 # c 
  c = snd (splitAt ram2 vs)"
proof -
  assume dist: "distinct vs" and vs: "vs = a @ ram1 # b @ ram2 # c"
  then show "c = snd (splitAt ram2 vs)" apply (drule_tac splitAt_dist_ram2) by (auto dest: pairD)
qed

lemma splitAt_dist_ram21: "distinct vs  vs = a @ ram1 # b @ ram2 # c  (a, b) = splitAt ram1 (fst (splitAt ram2 vs))"
proof -
  assume dist: "distinct vs" and vs: "vs = a @ ram1 # b @ ram2 # c"
  then have "fst (splitAt ram2 vs) = a @ ram1 # b" apply (drule_tac splitAt_dist_ram2) by (auto dest: pairD)
  with dist vs show ?thesis by (rule_tac splitAt_dist_ram) auto
qed

lemma splitAt_dist_ram22: "distinct vs  vs = a @ ram1 # b @ ram2 # c   (c, []) = splitAt ram1 (snd (splitAt ram2 vs))"
proof -
  assume dist: "distinct vs" and vs: "vs = a @ ram1 # b @ ram2 # c"
  then have "snd (splitAt ram2 vs) = c" apply (drule_tac splitAt_dist_ram2) by (auto dest: pairD)
  with dist vs have "splitAt ram1 (snd (splitAt ram2 vs)) = (c, [])" by (auto intro: splitAt_no_ram)
  then show ?thesis by auto
qed

lemma splitAt_dist_ram1: "distinct vs  vs = a @ ram1 # b @ ram2 # c  (a, b @ ram2 # c) = splitAt ram1 vs"
by (auto intro: splitAt_dist_ram)

lemma splitAt_dist_ram10: "distinct vs  vs = a @ ram1 # b @ ram2 # c  a = fst (splitAt ram1 vs)"
proof -
  assume dist: "distinct vs" and vs: "vs = a @ ram1 # b @ ram2 # c"
  then show "a = fst (splitAt ram1 vs)" apply (drule_tac splitAt_dist_ram1) by (auto dest: pairD)
qed

lemma splitAt_dist_ram11: "distinct vs  vs = a @ ram1 # b @ ram2 # c  (a, []) = splitAt ram2 (fst (splitAt ram1 vs))"
proof -
  assume dist: "distinct vs" and vs: "vs = a @ ram1 # b @ ram2 # c"
  then have "fst (splitAt ram1 vs) = a" apply (drule_tac splitAt_dist_ram1) by (auto dest: pairD)
  with dist vs have "splitAt ram2 (fst (splitAt ram1 vs)) = (a, [])" by (auto intro: splitAt_no_ram)
  then show ?thesis by auto
qed

lemma splitAt_dist_ram12: "distinct vs  vs = a @ ram1 # b @ ram2 # c   (b, c) = splitAt ram2 (snd (splitAt ram1 vs))"
proof -
  assume dist: "distinct vs" and vs: "vs = a @ ram1 # b @ ram2 # c"
  then have "snd (splitAt ram1 vs) = b @ ram2 # c" apply (drule_tac splitAt_dist_ram1) by (auto dest: pairD)
  with dist vs show ?thesis by (rule_tac splitAt_dist_ram)  auto
qed

lemma splitAt_dist_ram_all:
  "distinct vs  vs = a @ ram1 # b @ ram2 # c
   (a, b) = splitAt ram1 (fst (splitAt ram2 vs))
   (c, []) = splitAt ram1 (snd (splitAt ram2 vs))
   (a, []) = splitAt ram2 (fst (splitAt ram1 vs))
   (b, c) = splitAt ram2 (snd (splitAt ram1 vs))
    c = snd (splitAt ram2 vs)
    a = fst (splitAt ram1 vs)"
  apply (rule_tac conjI) apply (rule_tac splitAt_dist_ram21) apply simp apply simp
  apply (rule_tac conjI) apply (rule_tac splitAt_dist_ram22) apply simp apply simp
  apply (rule_tac conjI) apply (rule_tac splitAt_dist_ram11 splitAt_dist_ram22) apply simp apply simp
  apply (rule_tac conjI) apply (rule_tac splitAt_dist_ram12)apply simp apply simp
  apply (rule_tac conjI) apply (rule_tac splitAt_dist_ram20) apply simp apply simp
                            by (rule_tac splitAt_dist_ram10) auto


subsubsection ‹Mixed›

lemma fst_splitAt_rev:
 "distinct xs  x  set xs 
  fst(splitAt x (rev xs)) = rev(snd(splitAt x xs))"
by(simp add:splitAt_conv takeWhile_neq_rev)

lemma snd_splitAt_rev:
 "distinct xs  x  set xs 
  snd(splitAt x (rev xs)) = rev(fst(splitAt x xs))"
by(simp add:splitAt_conv dropWhile_neq_rev)

lemma splitAt_take[simp]: "distinct ls  i < length ls  fst (splitAt (ls!i) ls) = take i ls"
proof -
  assume d: "distinct ls" and si: "i < length ls"
  then have ls1: "ls = take i ls @ ls!i # drop (Suc i) ls" by (rule_tac id_take_nth_drop)
  from si have "ls!i  set ls" by auto
  then have ls2: "ls = fst (splitAt (ls!i) ls) @ ls!i # snd (splitAt (ls!i) ls)" by (auto dest: splitAt_ram)
  from d ls2 ls1 have "fst (splitAt (ls!i) ls) = take i ls  snd (splitAt (ls!i) ls) = drop (Suc i) ls" by (rule dist_at)
   then show ?thesis by auto
qed

lemma splitAt_drop[simp]: "distinct ls   i < length ls  snd (splitAt (ls!i) ls) = drop (Suc i) ls"
proof -
  assume d: "distinct ls" and si: "i < length ls"
  then have ls1: "ls = take i ls @ ls!i # drop (Suc i) ls" by (rule_tac id_take_nth_drop)
  from si have "ls!i  set ls" by auto
  then have ls2: "ls = fst (splitAt (ls!i) ls) @ ls!i # snd (splitAt (ls!i) ls)" by (auto dest: splitAt_ram)
  from d ls2 ls1 have "fst (splitAt (ls!i) ls) = take i ls  snd (splitAt (ls!i) ls) = drop (Suc i) ls" by (rule dist_at)
   then show ?thesis by auto
qed

lemma fst_splitAt_upt:
 "j  i  i < k  fst(splitAt i [j..<k]) = [j..<i]"
using splitAt_take[where ls = "[j..<k]" and i="i-j"]
apply (simp del:splitAt_take)
done

lemma snd_splitAt_upt:
 "j  i  i < k  snd(splitAt i [j..<k]) = [i+1..<k]"
using splitAt_drop[where ls = "[j..<k]" and i="i-j"]
by simp

lemma local_help1: " a vs. vs = c @ r # d  vs = a @ r # b  r  set a  r  set b  a = c"
proof (induct c)
  case Nil
  then have ra: "r  set a" and vs1: "vs = a @ r # b" and vs2: "vs = [] @ r # d"
    by auto
  from vs1 vs2 have "a @ r # b = r # d" by auto
  then have "hd (a @ r # b) = r" by auto
  then have "a  []  hd a = r" by auto
  then have "a  []  r  set a" by (induct a) auto
  with ra have a: "a = []" by auto
  then show ?case by auto
next
  case (Cons x xs) then show ?case by (induct a) auto
qed

lemma local_help: "vs = a @ r # b  vs = c @ r # d  r  set a  r  set b  a = c  b = d"
proof -
  assume dist: "r  set a" "r  set b" and vs1: "vs = a @ r # b" and vs2: "vs = c @ r # d"
  from vs2 vs1 dist have "a = c" by (rule local_help1)
  with dist vs1 vs2 show ?thesis by simp
qed

lemma local_help': "a @ r # b = c @ r # d  r  set a  r  set b  a = c  b = d"
by (rule local_help) auto


lemma splitAt_simp1: "ram  set a  ram  set b  fst (splitAt ram (a @ ram # b)) = a "
proof -
  assume ramab: "ram  set a"  "ram  set b"
  define vs where "vs = a @ ram # b"
  then have vs: "vs = a @ ram # b" by auto
  then have "ram  set vs" by auto
  then have "vs = fst (splitAt ram vs) @ ram # snd (splitAt ram vs)" by (auto dest: splitAt_ram)
  with  vs ramab show ?thesis apply simp apply (rule_tac sym)  apply (rule_tac local_help1) apply simp
    apply (rule sym) apply assumption by auto
qed


lemma help'''_in: " xs. ram  set b  fst (splitAtRec ram xs b) = xs @ fst (splitAtRec ram [] b)"
proof (induct b)
case Nil then show ?case by auto
next
case (Cons b bs) show ?case using Cons(2)
  apply (case_tac "b = ram") apply simp
  apply simp
  apply (subgoal_tac "fst (splitAtRec ram (xs @ [b]) bs) = (xs@[b]) @ fst (splitAtRec ram [] bs)") apply simp
  apply (subgoal_tac "fst (splitAtRec ram [b] bs) = [b] @ fst (splitAtRec ram [] bs)") apply simp
  apply (rule Cons) apply force
  apply (rule Cons) by force
qed

lemma help'''_notin: " xs. ram   set b  fst (splitAtRec ram xs b) = xs @ fst (splitAtRec ram [] b)"
proof (induct b)
case Nil then show ?case by auto
next
case (Cons b bs)
then have "ram  set bs" by auto
then show ?case
  apply (case_tac "b = ram") apply simp
  apply simp
  apply (subgoal_tac "fst (splitAtRec ram (xs @ [b]) bs) = (xs@[b]) @ fst (splitAtRec ram [] bs)") apply simp
  apply (subgoal_tac "fst (splitAtRec ram [b] bs) = [b] @ fst (splitAtRec ram [] bs)") apply simp
  apply (rule Cons) apply simp
  apply (rule Cons) by simp
qed

lemma help''': "fst (splitAtRec ram xs b) = xs @ fst (splitAtRec ram [] b)"
apply (cases "ram  set b")
apply (rule_tac help'''_in) apply simp
apply (rule_tac help'''_notin) apply simp done

lemma splitAt_simpA[simp]: "fst (splitAt ram (ram # b)) = []" by (simp add: splitAt_def)
lemma splitAt_simpB[simp]: "ram  a  fst (splitAt ram (a # b)) = a # fst (splitAt ram b)" apply (simp add: splitAt_def)
  apply (subgoal_tac "fst (splitAtRec ram [a] b) = [a] @ fst (splitAtRec ram [] b)") apply simp by (rule help''')
lemma splitAt_simpB'[simp]: "a  ram  fst (splitAt ram (a # b)) = a # fst (splitAt ram b)" apply (rule splitAt_simpB) by auto
lemma splitAt_simpC[simp]: "ram  set a   fst (splitAt ram (a @ b)) = a @ fst (splitAt ram b)"
apply (induct a) by auto

lemma help'''': " xs ys. snd (splitAtRec ram xs b) = snd (splitAtRec ram ys b)"
apply (induct b) by auto

lemma splitAt_simpD[simp]: " a. ram  a  snd (splitAt ram (a # b)) = snd (splitAt ram b)" apply (simp add: splitAt_def)
by (rule help'''')
lemma splitAt_simpD'[simp]: " a. a  ram  snd (splitAt ram (a # b)) = snd (splitAt ram b)" apply (rule splitAt_simpD) by auto

lemma splitAt_simpE[simp]: "snd (splitAt ram (ram # b)) = b" by (simp add: splitAt_def)

lemma splitAt_simpF[simp]: "ram  set a   snd (splitAt ram (a @ b)) = snd (splitAt ram b) "
apply (induct a) by auto


lemma splitAt_rotate_pair_conv:
  "xs.  distinct xs; x  set xs 
   snd (splitAt x (rotate n xs)) @ fst (splitAt x (rotate n xs)) =
      snd (splitAt x xs) @ fst (splitAt x xs)"
apply(induct n) apply simp
apply(simp del:rotate_Suc2 add:rotate1_rotate_swap)
apply(case_tac xs) apply clarsimp+
apply(erule disjE) apply simp
apply(drule split_list)
apply clarsimp
done


subsection between›

definition between :: "'a list  'a  'a  'a list" where
 "between vs ram1 ram2 
     let (pre1, post1) = splitAt ram1 vs in
     if ram2  set post1
     then let (pre2, post2) = splitAt ram2 post1 in pre2
     else let (pre2, post2) = splitAt ram2 pre1 in post1 @ pre2"

lemma inbetween_inset:
 "x  set(between xs a b)  x  set xs"
apply(simp add:between_def split_def split:if_split_asm)
 apply(blast dest:splitAt_in_snd)
apply(blast dest:splitAt_in_snd)
done

lemma notinset_notinbetween:
 "x  set xs  x  set(between xs a b)"
by(blast dest:inbetween_inset)


lemma set_between_id:
 "distinct xs  x  set xs 
  set(between xs x x) = set xs - {x}"
apply(drule split_list)
apply (clarsimp simp:between_def split_def Un_commute)
done


lemma split_between:
 " distinct vs; r  set vs; v  set vs; u  set(between vs r v)  
  between vs r v =
 (if r=u then [] else between vs r u @ [u]) @ between vs u v"
apply(cases  "r = v")
 apply(clarsimp)
 apply(frule split_list[of v])
 apply(clarsimp)
 apply(simp add:between_def split_def split:if_split_asm)
 apply(erule disjE)
  apply(frule split_list[of u])
  apply(clarsimp)
  apply(frule split_list[of u])
  apply(clarsimp)
 apply(clarsimp)
 apply(frule split_list[of r])
apply(clarsimp)
apply(rename_tac as bs)
apply(erule disjE)
 apply(frule split_list[of v])
 apply(clarsimp)
 apply(rename_tac cs ds)
 apply(subgoal_tac "between (cs @ v # ds @ r # bs) r v = bs @ cs")
  prefer 2 apply(simp add:between_def split_def split:if_split_asm)
 apply simp
 apply(erule disjE)
  apply(frule split_list[of u])
  apply(clarsimp simp:between_def split_def split:if_split_asm)
 apply(frule split_list[of u])
 apply(clarsimp simp:between_def split_def split:if_split_asm)
apply(frule split_list[of v])
apply(clarsimp)
apply(rename_tac cs ds)
apply(subgoal_tac "between (as @ r # cs @ v # ds) r v = cs")
 prefer 2 apply(simp add:between_def split_def split:if_split_asm)
apply simp
apply(frule split_list[of u])
apply(clarsimp simp:between_def split_def split:if_split_asm)
done


subsection ‹Tables›

type_synonym ('a, 'b) table = "('a × 'b) list"

definition isTable :: "('a  'b)  'a list  ('a, 'b) table  bool" where
  "isTable f vs t  p. p  set t  snd p = f (fst p)  fst p  set vs" 

lemma isTable_eq: "isTable E vs ((a,b)#ps)  b = E a"
  by (auto simp add: isTable_def)

lemma isTable_subset: 
  "set qs  set ps  isTable E vs ps  isTable E vs qs"
  by (unfold isTable_def) auto

lemma isTable_Cons: "isTable E vs ((a,b)#ps)  isTable E vs ps"
  by (unfold isTable_def) auto


definition removeKey :: "'a  ('a × 'b) list  ('a × 'b) list" where
"removeKey a ps  [p  ps. a  fst p]"

primrec removeKeyList :: "'a list  ('a × 'b) list  ('a × 'b) list" where
  "removeKeyList [] ps = ps"
| "removeKeyList (w#ws) ps = removeKey w (removeKeyList ws ps)"

lemma removeKey_subset[simp]: "set (removeKey a ps)  set ps"
  by (simp add: removeKey_def) 

lemma length_removeKey[simp]: "|removeKey w ps|  |ps|"
  by (simp add: removeKey_def) 

lemma length_removeKeyList: 
  "length (removeKeyList ws ps)  length ps" (is "?P ws")
proof (induct ws)
    show "?P []" by simp
    fix w ws
    have "length (removeKey w (removeKeyList ws ps)) 
       length (removeKeyList ws ps)" 
      by (rule length_removeKey)
    also assume "?P ws" 
    finally show "?P (w#ws)" by simp
qed

lemma removeKeyList_subset[simp]: "set (removeKeyList ws ps)  set ps"
proof (induct ws) 
  case Nil then show ?case by simp
next
  case (Cons w ws) then show ?case
    by (metis dual_order.trans removeKeyList.simps(2) removeKey_subset)
qed

lemma notin_removeKey1: "(a, b)  set (removeKey a ps)"
  by (induct ps) (auto simp add: removeKey_def)

lemma removeKeyList_eq:
  "removeKeyList as ps = [p  ps. a  set as. a  fst p]"
by (induct as) (simp_all add: filter_comm removeKey_def)

lemma removeKey_empty[simp]: "removeKey a [] = []"
  by (simp add: removeKey_def)
lemma removeKeyList_empty[simp]: "removeKeyList ps [] = []"
  by (induct ps) simp_all
lemma removeKeyList_cons[simp]: 
  "removeKeyList ws (p#ps) 
  = (if fst p  set ws then removeKeyList ws ps else p#(removeKeyList ws ps))"
  by (induct ws) (simp_all split: if_split_asm add: removeKey_def)

end