Theory ListAux

(*  ID:         $Id: ListAux.thy,v 1.3 2006/01/11 19:40:44 nipkow Exp $
    Author:     Gertrud Bauer, Tobias Nipkow
*)

header {* Basic Functions Old and New *}

theory ListAux
imports Main EfficientNat
begin

declare Let_def[simp]

declare comp_def[code unfold]

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


lemma [code unfold]: "max x y == (let u = x; v = y in if u <= v then v else u)"
by(simp add:max_def)
lemma [code unfold]: "min x y == (let u = x; v = y in if u <= v then u else v)"
by(simp add:min_def)

lemmas[code] = lessThan_0 lessThan_Suc


subsection {* Lists *}

declare mem_iff[simp] list_all_iff[simp] list_ex_iff[simp]


subsubsection{* @{text length} *}

syntax "_length" :: "'a list => nat"  ("|_|")
translations 
 "|xs|" == "length xs"

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 filter1: " [x∈xs . P x] = [] ==> 
    [x∈ xs. Q x ∧ P x] = []"
  by (induct xs)  (simp_all split: split_if_asm)

lemma filter_prop: "!!x. x ∈ set [u∈ys . P u] ==> P x"
proof (induct ys)
  case Nil then show ?case by simp 
next 
  case (Cons y ys) then show ?case 
    by (auto split: split_if_asm) 
qed
   
lemma filter_Cons_prop: "[u∈ys . P u] = x # xs ==> P x"
proof -
  assume "[u∈ys . P u] = x # xs"
  then have "x ∈ set [u∈ys . P u]" by simp
  then show "P x" by (rule filter_prop)
qed

lemma filter_compl1: 
 "([x ∈ xs. P x] = []) = ([x ∈ xs. ¬ 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 "[u∈xs . ¬ P u] ≠ x # xs"
    proof 
      assume "[u∈xs . ¬ P u] = x # xs" 
      then have "|x # xs| = |[u∈xs . ¬ 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: split_if_asm)
qed
lemma [simp]: "Not o (Not o P) = P"
  by (rule ext) simp

lemma filter_compl2: "!!P. (filter (Not o P) xs = []) = (filter P xs = xs)"
  by (simp add: filter_compl1) 

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

lemma filter_simp: "(!!x. x ∈ set xs ==> P x) ==> [x ∈ xs. P x ∧ Q x] = [x ∈ xs. Q x]"
 by (induct xs) auto

lemma filter_True_eq1: 
  "(length [y ∈ xs. 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)" .
  then have "P x"  by (simp split: split_if_asm) (insert l, arith)
  moreover with hyp have "length (filter P xs) = length xs" 
    by (simp split: split_if_asm)
  moreover have "y ∈ set (x#xs)" .
  ultimately show ?case by (auto dest: Cons(1))
qed

lemma length_filter_True_eq: 
  "(length [y ∈ xs. P y] = length xs) = (∀y. y ∈ set xs --> P y)"
  by (intro iffI allI impI, erule filter_True_eq1) simp_all


subsubsection {* @{const map} *}

syntax (xsymbols)
  "@map" :: "[ 'b, pttrn, 'a list] => 'a list"("(1[_. _ ∈ _])")
syntax 
  "@map" :: "[ 'b, pttrn, 'a list] => 'a list"("(1[_./ _ : _])")

translations
  "[f. x ∈ xs]"== "map (λx. f) xs" 
  "[f. x : xs]"== "map (λx. f) xs";



subsubsection {* @{const map_filter} *}

syntax (xsymbols)
  "@map_filter" :: "['b, pttrn, 'a list, bool] => 'a list"("(1[_. _ ∈ _, _])")
syntax 
  "@map_filter" :: "['b, pttrn, 'a list, bool] => 'a list"("(1[_./ _ : _, _])")

translations
  "[f. x ∈ xs, P]"== "map_filter (λx. f) P xs" 
  "[f. x : xs, P]"== "map_filter (λx. f) P xs"

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


subsubsection {* @{const concat} *}

syntax (xsymbols)
  "@concat"     :: "idt => 'a list => 'a list => 'a list"  ("\<Squnion>_∈ _ _" 10)
translations "\<Squnion>x∈xs f" == "concat [f. x ∈ xs]" 


subsubsection {* List product *}

constdefs listProd1 :: "'a => 'b list => ('a × 'b) list"
 "listProd1 a bs ≡ [(a,b). b ∈ bs]"

constdefs listProd :: "'a list => 'b list => ('a × 'b) list" (infix "×" 50)
 "as × bs ≡ \<Squnion>a ∈ as listProd1 a bs"

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


subsubsection {*  Minimum and maximum *}

(* FIXME combine minimal with min_list *)
(* more general:
 foldl1 f (x#xs) = if xs=[] then x else f x (foldl1 f xs)
 min_list = foldl1 min
 max_list = foldl1 max
 sum_list = foldl1 (op +)
Put in separate ExecList.thy
*)
consts minimal:: "('a => nat) => 'a list => 'a"
primrec
 "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

lemma minimal_Cons1:
 "∀y ∈ set xs. f x ≤ f y ==> minimal f (x#xs) = x"
by (induct xs) auto

lemma minimal_append2:
  "∀x ∈ set xs. f x > f y ==> minimal f (xs @ y # ys) = minimal f (y # ys)"
by (induct xs) simp_all

lemma minimal_neq_lowerbound:
 "xs ≠ [] ==> ALL x: set xs. f x ≥ n ==> f(minimal f xs) ≠ n
 ==> ALL x: set xs. f x ≠ n"
apply(induct xs)
 apply simp
apply (auto split:split_if_asm)
done

(* FIXME minList to min_list *)
consts minList :: "nat list => nat"
primrec
 "minList (x#xs) = (if xs=[] then x else min x (minList xs))"

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


lemma minList_conv_Min[simp]:
 "xs ≠ [] ==> minList 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 *}

(* FIXME replace "remove1" by "replace1" in List.thy? *)

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

consts mapAt :: "nat list => ('a => 'a) => ('a list => 'a list)"
primrec
 "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 filter_replace:
 "¬ P y ==> filter P (replace x [y] xs) = remove1 x (filter P xs)"
by(induct xs) simp_all

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: split_if_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: split_if_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: split_if_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 replace_delete_oldF:
  "oldF ∉ set fs ==> distinct ls ==> oldF ∉ set (replace oldF fs ls)"
by (induct ls)  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 fastsimp
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_filter_single:
"distinct ls ==> v ∈ set ls ==> [a∈ ls . a = v] = [v]"
proof (induct ls)
  case Nil then show ?case by auto
next
  case (Cons l ls) then show ?case
  proof (cases "l = v")
    case True with Cons
    have "v ∉ set ls" by auto
    then have "[a∈ls . a = v] = []" by (induct ls) auto
    with Cons True show ?thesis by auto
  next
    case False with Cons show ?thesis by auto
  qed
qed

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
  def 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 -
  def 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_inv': "ls = rotate ((length ls) - (n mod length ls)) ms ==>
 rotate n ls = ms"
proof (cases "ls  = []")
  assume r: "ls = rotate ((length ls) - (n mod length ls)) ms"
  case True with r show ?thesis by auto
next
  assume r: "ls = rotate ((length ls) - (n mod length ls)) ms"
  case False
  def len ≡ "length ls"
  with r have r': "ls = rotate (len - (n mod len)) ms" by simp
  with len_def have lms: "length ms = len" by auto
  def y ≡ "n mod len"
  from len_def False have ll: "len > 0" by auto
  with y_def have small_y: "y < len" by auto
  then have len_gz: "len > 0" by auto
  from r' len_def have mem0: "rotate n ls = rotate n (rotate (len - (n mod len)) ms)" by auto
  have "rotate n (rotate (len - (n mod len)) ms) = rotate (n + (len - (n mod len))) ms"
    by (rule rotate_rotate)
  with mem0 have mem1: "rotate n ls = rotate (n + (len - (n mod len))) ms" by auto
  have "n mod len - n mod len = 0" by arith
  then have "len + n mod len - n mod len = len" by arith
  from y_def have ymod: "n mod len = y" by auto
  with len_gz obtain r where n: "n = y + r*len" apply (drule_tac mod_eqD) by auto
  then have "n + len = (r*len)+len  + y" by arith
  then have "n + len = ((r+1)*len) + y" by auto
  with len_gz small_y have "n + (len - y) = ((r+1)*len)" by auto
  then have zero: "(n + (len - y)) mod len = 0" by auto
  have "rotate (n + (len - y)) ms = rotate ((n + (len - y)) mod length ms) ms" by (rule_tac rotate_conv_mod)
  with lms zero have "rotate (n + (len - y)) ms = ms" by auto
  with mem1 y_def show ?thesis 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 (auto simp: rotate1_def) 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 simp: rotate1_def)

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
  def 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:split_if_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: split_if_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)
  def 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

lemma help1: "∃ n.  filter f (rotate1 ls) = rotate n (filter f ls)"
proof (cases ls)
  case Nil then show ?thesis by auto
next
  case (Cons m ms)
  then show ?thesis
  proof (cases "f m")
    case True with Cons
    have "filter f (rotate1 (ls)) = rotate 1 (filter f (ls))" by auto
    then show ?thesis apply (rule_tac exI) .
  next
    case False with Cons
    have "filter f (rotate1 (ls)) = rotate 0 (filter f (ls))" by auto
    then show ?thesis apply (rule_tac exI) .
  qed
qed

lemma help3: "¬ f l ==> n < length ls ==> filter f (rotate n ls) = filter f (rotate n (rotate1 (l # ls)))"
proof -
  assume fl: "¬ f l" and n: "n < length ls"
  then have n2: "n - length ls = 0"  by auto
  from fl n show ?thesis apply simp
    apply (subst rotate_drop_take)+ by auto
qed

lemma help4: "¬ f l ==> n < length ls ==> filter f (rotate n ls) = filter f (rotate (Suc n) (l # ls))"
proof -
  assume fl: "¬ f l" and n: "n < length ls"
  then have r1: "filter f (rotate n ls) = filter f (rotate n (rotate1 (l # ls)))" by (rule help3)
  def ms ≡ "l # ls"
  have "rotate n (rotate1 (ms)) = rotate (Suc n) (ms)" by simp
  with ms_def have "rotate n (rotate1 (l # ls)) = rotate (Suc n) (l # ls)" by simp
  with r1 show ?thesis by auto
qed

lemma help2: "∃ n.  rotate1 (filter f ls) = filter f (rotate n ls)"
proof (induct ls)
  case Nil then show ?case by auto
next
  case (Cons m ms)
  then show ?case
  proof (cases "f m")
    case True with Cons
    have "filter f (m # ms) = m # filter f  ms" by auto
    from True Cons have
      "rotate1 (filter f (m # ms)) = filter f (rotate 1 (m # ms))" by auto
    then show ?thesis apply (rule_tac exI) .
  next
    case False with Cons
    have f1: "filter f (m # ms) = filter f  ms" by auto
    then have mem: "rotate1 (filter f (m # ms)) = rotate1 (filter f ms)" by auto
    from False have f2: "!! ks. filter f (ks @ [m]) = filter f ks" by auto
    from  Cons obtain n where n: "rotate1 (filter f ms) = filter f (rotate n ms)" by auto
    with mem have mem1: "rotate1 (filter f (m # ms)) = filter f (rotate n ms)" by auto
    def n' ≡ "n mod length ms"
    then have "filter f (rotate n ms) = filter f (rotate n' ms)" by auto
    with mem1 have mem2: "rotate1 (filter f (m # ms)) = filter f (rotate n' ms)" by auto
    from n'_def have "ms ≠ [] ==> n' < length ms" by auto
    with False have "filter f (rotate n' ms) = filter f (rotate (Suc n') (m # ms))"
      apply (case_tac "ms = []") apply force apply (rule_tac help4) by auto
    with mem2 have "rotate1 (filter f (m # ms)) = filter f ((rotate (Suc n') (m # ms)))" by auto
    then show ?thesis apply (rule_tac exI) .
  qed
qed

lemma rotate_help5: "∃ n. filter f (rotate m ls) = rotate n (filter f ls)"
proof (induct m)
  case 0 then have "filter f (rotate 0 ls) = rotate 0 (filter f ls)" by auto
  then show ?case by (rule exI)
next
  case (Suc m)
  def ks ≡ "rotate m ls"
  then have mem0: "filter f (rotate (Suc m) ls) = filter f (rotate1 ks)" by auto
  from ks_def Suc obtain n where n: "filter f ks = rotate n (filter f ls)" by auto
  have "∃ n'. filter f (rotate1 ks) = rotate n' (filter f ks)" by (rule help1)
  then obtain n' where "filter f (rotate1 ks) = rotate n' (filter f ks)" by auto
  with n have  "filter f (rotate1 ks) = rotate n' (rotate n (filter f ls))" by auto
  with mem0 have mem1: "filter f (rotate (Suc m) ls) = rotate n' (rotate n (filter f ls))" by auto
  have "rotate n' (rotate n (filter f ls)) = rotate (n'+n) (filter f ls)" by (rule rotate_rotate)
  with mem1 have "filter f (rotate (Suc m) ls) =  rotate (n'+n) (filter f ls)" by auto
  then show ?case apply (rule_tac exI) .
qed

lemma rotate_help6: "∃ n. rotate m (filter f ls) = filter f (rotate n ls)"
proof (induct m)
  case 0 then have "rotate 0 (filter f ls) = filter f (rotate 0 ls)" by auto
  then show ?case by (rule exI)
next
  case (Suc m)
  have mem0: "rotate (Suc m) (filter f ls) = rotate1 (rotate m (filter f ls))" by auto
  from Suc obtain n where n: "rotate m (filter f ls) = filter f (rotate n ls)" by auto
  with mem0 have mem1: "rotate (Suc m) (filter f ls) = rotate1 (filter f (rotate n ls))" by auto
  def ks ≡ "rotate n ls"
  from help2 obtain n' where "rotate1 (filter f ks) = filter f (rotate n' ks)" by auto
  with mem1 ks_def have mem2: "rotate (Suc m) (filter f ls) = filter f (rotate n' ks)" by auto
  from ks_def have "rotate n' ks = rotate (n'+n) ls" apply simp by (rule rotate_rotate)
  with mem2 have "rotate (Suc m) (filter f ls) = filter f(rotate (n'+n) ls)" by simp
  then show ?case apply (rule_tac exI) .
qed



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

subsection {* @{text splitAt} *}

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

constdefs splitAt :: "'a => 'a list => 'a list × 'a list"
  "splitAt c as  ≡ splitAtRec c [] as"


subsubsection {* @{const splitAtRec} *}

lemma splitAtRec_conv: "!!bs.
 splitAtRec x bs xs =
 (bs @ takeWhile (%y. y≠x) xs, tl(dropWhile (%y. y≠x) 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: split_if_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. y≠x) xs, tl(dropWhile (%y. y≠x) 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: split_if_asm)

lemma splitAt_union:
"(a,b) = splitAt ram vs ==> (set a ∪ set b) - {ram} = set vs - {ram}"
by (simp add: splitAt_def splitAtRec_union)

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_subset_fst:
"set (fst (splitAt ram vs)) ⊆ set vs"
proof -
  def a: a ≡ "fst (splitAt ram vs)"
  def b: b ≡ "snd (splitAt ram vs)"
  with a have "(a,b) = splitAt ram vs" by auto
  with a show ?thesis by (auto dest: splitAt_subset_ab)
qed

lemma splitAt_subset_snd:
"set (snd (splitAt ram vs)) ⊆ set vs"
proof -
  def a: a ≡ "fst (splitAt ram vs)"
  def b: b ≡ "snd (splitAt ram vs)"
  with a have "(a,b) = splitAt ram vs" by auto
  with b show ?thesis by (auto dest: splitAt_subset_ab)
qed

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))"
  def a ≡ "fst (splitAt ram vs)"
  with v have vin: "v ∈ set a" by auto
  def 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))"
  def a ≡ "fst (splitAt ram vs)"
  def 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:
 "distinct vs ==> (a,b) = splitAt ram vs ==> distinct a ∧ distinct b"
apply (cases "ram ∈ set vs") by (auto dest: splitAt_split simp: splitAt_no_ram)

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

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

lemma splitAt_distinct_fst[intro]:
 "distinct vs ==> distinct (fst (splitAt ram vs))"
proof -
  assume d: "distinct vs"
  def b: b ≡ "snd (splitAt ram vs)"
  def a: a ≡ "fst (splitAt ram vs)"
  with b have "(a,b) = splitAt ram vs" by auto
  with a d show ?thesis  by (auto dest: splitAt_distinct_ab)
qed

lemma splitAt_distinct_snd[intro]:
 "distinct vs ==> distinct (snd (splitAt ram vs))"
proof -
  assume d: "distinct vs"
  def b: b ≡ "snd (splitAt ram vs)"
  def a: a ≡ "fst (splitAt ram vs)"
  with b have "(a,b) = splitAt ram vs" by auto
  with b d show ?thesis  by (auto dest: splitAt_distinct_ab)
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_or:
  "v ∈ set vs ==> v ∈ set (fst (splitAt ram vs)) ∨ v ∈ set (snd (splitAt ram vs)) ∨ v = ram"
  by (rule splitAt_2)  auto

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)

lemma splitAt_subset1: "(a,b) = splitAt ram vs ==> (set a ⊆ set vs)"
by (auto dest: splitAt_subset)

lemma splitAt_subset2: "(a,b) = splitAt ram vs ==> (set b ⊆ set vs)"
by (auto dest: splitAt_subset)



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_ram2: "ram2 ∉  set (snd (splitAt ram1 vs)) ==>
  ram1 ∈ set vs ==> ram2 ∈ set vs ==> ram1 ≠ ram2 ==>
  ram2 ∈ set (fst (splitAt ram1 vs))" by (auto dest: splitAt_elements)

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 ==> EX! s. vs = (fst s) @ ram # (snd s)"
proof
  assume d: "distinct vs" and r: "ram ∈ set vs"
  def 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) apply arith
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"]
apply (simp del:splitAt_drop) apply arith
done


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"
  then have "a = c" apply (rule_tac 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"
  def 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 splitAt_simp2: "ram ∉ set b ==> fst (splitAt ram (ram # b)) = [] "
  apply (subgoal_tac " fst (splitAt ram ([] @ ram # b)) = []") apply force
apply (rule splitAt_simp1) by auto

lemma splitAt_simp3: "ram ∉ set a ==> fst (splitAt ram (a @ [ram])) = a "
  apply (subgoal_tac " fst (splitAt ram (a @ ram # [])) = a") apply force
apply (rule splitAt_simp1) by auto


lemma splitAt_simp4: "ram ∉ set a ==> ram ∉ set b ==> snd (splitAt ram (a @ ram # b)) = b "
proof -
  assume ramab: "ram ∉ set a"  "ram ∉ set b"
  def 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 by (simp  add: splitAt_simp1)
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(clarsimp simp add:rotate1_def split:list.split)
apply(erule disjE) apply simp
apply(drule split_list)
apply clarsimp
done


subsection {* @{text between} *}

constdefs between :: "'a list => 'a => 'a => 'a list"
 "between vs ram1 ram2 ≡
     let (pre1, post1) = splitAt ram1 vs in
     if ram2 mem 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:split_if_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:split_if_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:split_if_asm)
 apply simp
 apply(erule disjE)
  apply(frule split_list[of u])
  apply(clarsimp simp:between_def split_def split:split_if_asm)
 apply(frule split_list[of u])
 apply(clarsimp simp:between_def split_def split:split_if_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:split_if_asm)
apply simp
apply(frule split_list[of u])
apply(clarsimp simp:between_def split_def split:split_if_asm)
done


subsection {* Tables *}

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

constdefs isTable :: "('a => 'b) => 'a list => ('a, 'b) table => bool"
  "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


constdefs
removeKey  :: "'a => ('a × 'b) list => ('a × 'b) list"
"removeKey a ps ≡ [p ∈ ps. a ≠ fst p]"

consts removeKeyList :: "'a list => ('a × 'b) list => ('a × 'b) list"
primrec
  "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) blast

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) 
  have "set (removeKey w (removeKeyList ws ps)) ⊆ set (removeKeyList ws ps)"
    by (rule removeKey_subset)
  with Cons show ?case by (simp add: removeKey_def)
qed

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

lemma notin_removeKey: "r ∉ fst ` set (removeKey r ps)"
  by (induct ps) (auto simp add: removeKey_def)

lemma notin_removeKeyList1: 
  "!!a. a ∈ set rs ==> (a, b) ∉ set (removeKeyList rs ps)"
proof (induct rs)
  case Nil then show ?case by simp
next 
  case (Cons r rs) then show ?case 
  proof cases
    assume "a = r" then show ?thesis
      by (auto simp add: split_beta Let_def notin_removeKey1 removeKey_subset)
  next
    assume a: "a ≠ r" 
    with Cons have"(a, b) ∉ set (removeKeyList rs ps)" by simp 
    moreover have "set (removeKey r (removeKeyList rs ps)) 
        ⊆ set (removeKeyList rs ps)" 
       by (rule removeKey_subset) (* fixme : finally *)
    ultimately have "(a, b) ∉ set (removeKey r (removeKeyList rs ps))"
      by blast 
    then show ?thesis by simp
  qed
qed

lemma notin_removeKeyList: "!!r. r ∈ set rs ==> r ∉ fst ` set (removeKeyList rs ps)"
proof (induct rs)
  case Nil then show ?case by simp
next 
  case (Cons r' rs) then show ?case 
    by (auto simp add: notin_removeKey1 split_paired_all removeKey_def)
qed

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: split_if_asm add: removeKey_def)

end