# Theory ListAux

Up to index of Isabelle/HOL/Tame

theory ListAux
imports Main EfficientNat
begin

```(*  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)"
lemma [code unfold]: "min x y == (let u = x; v = y in if u <= v then u else v)"

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"

lemma filter_comm: "[x ∈ xs. P x ∧ Q x] = [x ∈ xs. Q x ∧ P x]"

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)"

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"
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")
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"

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

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))"

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"

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}"

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))"

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))"

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)) = {}"

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))"

lemma snd_splitAt_rev:
"distinct xs ==> x ∈ set xs ==>
snd(splitAt x (rev xs)) = rev(fst(splitAt x xs))"

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(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(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(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"

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"

lemma length_removeKey[simp]: "|removeKey w ps| ≤ |ps|"

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 [] = []"
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
```

### HOL

lemma pairD:

`  (a, b) = p ==> a = fst p ∧ b = snd p`

lemmas conj_aci:

`  (P ∧ Q) = (Q ∧ P)`
`  (P ∧ Q ∧ R) = (Q ∧ P ∧ R)`
`  ((P ∧ Q) ∧ R) = (P ∧ Q ∧ R)`
`  (A ∧ A) = A`
`  (A ∧ A ∧ B) = (A ∧ B)`

lemmas conj_aci:

`  (P ∧ Q) = (Q ∧ P)`
`  (P ∧ Q ∧ R) = (Q ∧ P ∧ R)`
`  ((P ∧ Q) ∧ R) = (P ∧ Q ∧ R)`
`  (A ∧ A) = A`
`  (A ∧ A ∧ B) = (A ∧ B)`

lemma

`  max x y == let u = x; v = y in if u ≤ v then v else u`

lemma

`  min x y == let u = x; v = y in if u ≤ v then u else v`

lemmas

`  {..<0} = {}`
`  {..<Suc k} = insert k {..<k}`

lemmas

`  {..<0} = {}`
`  {..<Suc k} = insert k {..<k}`

### Lists

#### @{text length}

lemma length3D:

`  |xs| = 3 ==> ∃x y z. xs = [x, y, z]`

lemma length4D:

`  |xs| = 4 ==> ∃a b c d. xs = [a, b, c, d]`

#### @{const filter}

lemma filter_emptyE:

`  [| filter P xs = []; x ∈ set xs |] ==> ¬ P x`

lemma filter_comm:

`  [x∈xs . P x ∧ Q x] = [x∈xs . Q x ∧ P x]`

lemma filter1:

`  filter P xs = [] ==> [x∈xs . Q x ∧ P x] = []`

lemma filter_prop:

`  x ∈ set (filter P ys) ==> P x`

lemma filter_Cons_prop:

`  filter P ys = x # xs ==> P x`

lemma filter_compl1:

`  (filter P xs = []) = ([x∈xs . ¬ P x] = xs)`

lemma

`  Not o (Not o P) = P`

lemma filter_compl2:

`  (filter (Not o P) xs = []) = (filter P xs = xs)`

lemma filter_eqI:

`  (!!v. v ∈ set vs ==> P v = Q v) ==> filter P vs = filter Q vs`

lemma filter_simp:

`  (!!x. x ∈ set xs ==> P x) ==> [x∈xs . P x ∧ Q x] = filter Q xs`

lemma filter_True_eq1:

`  [| |filter P xs| = |xs|; y ∈ set xs |] ==> P y`

lemma length_filter_True_eq:

`  (|filter P xs| = |xs|) = (∀y. y ∈ set xs --> P y)`

#### @{const map_filter}

lemma

`  map_filter f P xs = map f (filter P xs)`

#### List product

lemma

`  set (xs × ys) = set xs × set ys`

#### Minimum and maximum

lemma minimal_in_set:

`  xs ≠ [] ==> minimal f xs ∈ set xs`

lemma minimal_Cons1:

`  ∀y∈set xs. f x ≤ f y ==> minimal f (x # xs) = x`

lemma minimal_append2:

`  ∀x∈set xs. f y < f x ==> minimal f (xs @ y # ys) = minimal f (y # ys)`

lemma minimal_neq_lowerbound:

`  [| xs ≠ []; ∀x∈set xs. n ≤ f x; f (minimal f xs) ≠ n |] ==> ∀x∈set xs. f x ≠ n`

lemma minList_conv_Min:

`  xs ≠ [] ==> minList xs = Min (set xs)`

lemma max_list_conv_Max:

`  xs ≠ [] ==> max_list xs = Max (set xs)`

#### replace

lemma length_mapAt:

`  |mapAt vs f xs| = |xs|`

lemma length_replace1:

`  |replace x [y] xs| = |xs|`

lemma replace_id:

`  replace x [x] xs = xs`

lemma len_replace_ge_same:

`  1 ≤ |ys| ==> |xs| ≤ |replace x ys xs|`

lemma len_replace_ge:

`  [| 1 ≤ |ys|; |zs| ≤ |xs| |] ==> |zs| ≤ |replace x ys xs|`

lemma replace_append:

```  replace x ys (as @ bs) =
(if x ∈ set as then replace x ys as @ bs else as @ replace x ys bs)```

lemma filter_replace:

`  ¬ P y ==> filter P (replace x [y] xs) = remove1 x (filter P xs)`

lemma distinct_set_replace:

```  distinct xs
==> set (replace x ys xs) =
(if x ∈ set xs then set xs - {x} ∪ set ys else set xs)```

lemma replace1:

`  [| f ∈ set (replace f' fs ls); f ∉ set ls |] ==> f ∈ set fs`

lemma replace2:

`  f' ∉ set ls ==> replace f' fs ls = ls`

lemma replace3:

`  [| f' ∈ set ls; f ∈ set fs |] ==> f ∈ set (replace f' fs ls)`

lemma replace4:

`  [| f ∈ set ls; oldF ≠ f |] ==> f ∈ set (replace oldF fs ls)`

lemma replace5:

`  f ∈ set (replace oldF newfs fs) ==> f ∈ set fs ∨ f ∈ set newfs`

lemma replace6:

```  distinct oldfs
==> (x ∈ set (replace oldF newfs oldfs)) =
((x ≠ oldF ∨ oldF ∈ set newfs) ∧
(oldF ∈ set oldfs ∧ x ∈ set newfs ∨ x ∈ set oldfs))```

lemma replace_delete_oldF:

`  [| oldF ∉ set fs; distinct ls |] ==> oldF ∉ set (replace oldF fs ls)`

lemma distinct_replace:

```  [| distinct fs; distinct newFs; set fs ∩ set newFs ⊆ {oldF} |]
==> distinct (replace oldF newFs fs)```

lemma replace_replace:

```  [| oldf ∉ set newfs; distinct xs |]
==> replace oldf newfs (replace oldf newfs xs) = replace oldf newfs xs```

lemma replace_distinct:

```  [| distinct fs; distinct newfs; oldf ∈ set fs --> set newfs ∩ set fs ⊆ {oldf} |]
==> distinct (replace oldf newfs fs)```

lemma filter_replace2:

`  [| ¬ P x; ∀y∈set ys. ¬ P y |] ==> filter P (replace x ys xs) = filter P xs`

lemma length_filter_replace1:

```  [| x ∈ set xs; ¬ P x |]
==> |filter P (replace x ys xs)| = |filter P xs| + |filter P ys|```

lemma length_filter_replace2:

```  [| x ∈ set xs; P x |]
==> |filter P (replace x ys xs)| = |filter P xs| + |filter P ys| - 1```

#### @{const"distinct"}

lemma dist_filter_single:

`  [| distinct ls; v ∈ set ls |] ==> [a∈ls . a = v] = [v]`

lemma dist_at1:

`  [| distinct vs; vs = a @ r # b; vs = c @ r # d |] ==> a = c`

lemma dist_at:

`  [| distinct vs; vs = a @ r # b; vs = c @ r # d |] ==> a = c ∧ b = d`

lemma dist_at2:

`  [| distinct vs; vs = a @ r # b; vs = c @ r # d |] ==> b = d`

lemma distinct_split1:

`  [| distinct xs; xs = y @ [r] @ z |] ==> r ∉ set y`

lemma distinct_split2:

`  [| distinct xs; xs = y @ [r] @ z |] ==> r ∉ set z`

lemma distinct_hd_not_cons:

`  [| distinct vs; ∃as bs. vs = as @ x # hd vs # bs |] ==> False`

#### Misc

lemma drop_last_in:

`  n < |ls| ==> last ls ∈ set (drop n ls)`

lemma nth_last_Suc_n:

`  [| distinct ls; n < |ls|; last ls = ls ! n |] ==> Suc n = |ls|`

#### @{const rotate}

lemma plus_length1:

`  rotate (k + |ls|) ls = rotate k ls`

lemma plus_length2:

`  rotate (|ls| + k) ls = rotate k ls`

lemma rotate_minus1:

```  [| 0 < n; 0 < m; rotate n ls = rotate m ms |]
==> rotate (n - 1) ls = rotate (m - 1) ms```

lemma rotate_minus1':

`  [| 0 < n; rotate n ls = ms |] ==> rotate (n - 1) ls = rotate (|ms| - 1) ms`

lemma rotate_inv1:

`  [| n < |ls|; rotate n ls = ms |] ==> ls = rotate (|ls| - n) ms`

lemma rotate_conv_mod':

`  rotate (n mod |ls|) ls = rotate n ls`

lemma rotate_inv2:

`  rotate n ls = ms ==> ls = rotate (|ls| - n mod |ls|) ms`

lemma rotate_inv':

`  ls = rotate (|ls| - n mod |ls|) ms ==> rotate n ls = ms`

lemma rotate_id:

`  rotate (|ls| - n mod |ls|) (rotate n ls) = ls`

lemma nth_rotate1_Suc:

`  Suc n < |ls| ==> ls ! Suc n = rotate1 ls ! n`

lemma nth_rotate1_0:

`  ls ! 0 = rotate1 ls ! (|ls| - 1)`

lemma nth_rotate1:

`  0 < |ls| ==> ls ! (Suc n mod |ls|) = rotate1 ls ! (n mod |ls|)`

lemma rotate_Suc2:

`  rotate n (rotate1 xs) = rotate (Suc n) xs`

lemma nth_rotate:

`  0 < |ls| ==> ls ! ((n + m) mod |ls|) = rotate m ls ! (n mod |ls|)`

lemma help1:

`  ∃n. filter f (rotate1 ls) = rotate n (filter f ls)`

lemma help3:

```  [| ¬ f l; n < |ls| |]
==> filter f (rotate n ls) = filter f (rotate n (rotate1 (l # ls)))```

lemma help4:

```  [| ¬ f l; n < |ls| |]
==> filter f (rotate n ls) = filter f (rotate (Suc n) (l # ls))```

lemma help2:

`  ∃n. rotate1 (filter f ls) = filter f (rotate n ls)`

lemma rotate_help5:

`  ∃n. filter f (rotate m ls) = rotate n (filter f ls)`

lemma rotate_help6:

`  ∃n. rotate m (filter f ls) = filter f (rotate n ls)`

### @{text splitAt}

#### @{const splitAtRec}

lemma splitAtRec_conv:

```  splitAtRec x bs xs =
(bs @ takeWhile (λy. y ≠ x) xs, tl (dropWhile (λy. y ≠ x) xs))```

lemma splitAtRec_distinct_fst:

```  [| distinct vs; distinct s; set s ∩ set vs = {} |]
==> distinct (fst (splitAtRec ram1.0 s vs))```

lemma splitAtRec_distinct_snd:

```  [| distinct vs; distinct s; set s ∩ set vs = {} |]
==> distinct (snd (splitAtRec ram1.0 s vs))```

lemma splitAtRec_ram:

`  [| ram ∈ set vs; (a, b) = splitAtRec ram us vs |] ==> us @ vs = a @ [ram] @ b`

lemma splitAtRec_notRam:

`  ram ∉ set vs ==> splitAtRec ram us vs = (us @ vs, [])`

lemma splitAtRec_distinct:

```  [| distinct vs; distinct s; set s ∩ set vs = {} |]
==> set (fst (splitAtRec ram s vs)) ∩ set (snd (splitAtRec ram s vs)) = {}```

#### @{const splitAt}

lemma splitAt_conv:

`  splitAt x xs = (takeWhile (λy. y ≠ x) xs, tl (dropWhile (λy. y ≠ x) xs))`

lemma splitAt_no_ram:

`  ram ∉ set vs ==> splitAt ram vs = (vs, [])`

lemma splitAt_split:

`  [| ram ∈ set vs; (a, b) = splitAt ram vs |] ==> vs = a @ ram # b`

lemma splitAt_ram:

`  ram ∈ set vs ==> vs = fst (splitAt ram vs) @ ram # snd (splitAt ram vs)`

lemma fst_splitAt_last:

`  [| xs ≠ []; distinct xs |] ==> fst (splitAt (last xs) xs) = butlast xs`

#### Sets

lemma splitAtRec_union:

`  (a, b) = splitAtRec ram s vs ==> set a ∪ set b - {ram} = set vs ∪ set s - {ram}`

lemma splitAt_union:

`  (a, b) = splitAt ram vs ==> set a ∪ set b - {ram} = set vs - {ram}`

lemma splitAt_subset_ab:

`  (a, b) = splitAt ram vs ==> set a ⊆ set vs ∧ set b ⊆ set vs`

lemma splitAt_subset_fst:

`  set (fst (splitAt ram vs)) ⊆ set vs`

lemma splitAt_subset_snd:

`  set (snd (splitAt ram vs)) ⊆ set vs`

lemma splitAt_in_fst:

`  v ∈ set (fst (splitAt ram vs)) ==> v ∈ set vs`

lemma splitAt_not1:

`  v ∉ set vs ==> v ∉ set (fst (splitAt ram vs))`

lemma splitAt_in_snd:

`  v ∈ set (snd (splitAt ram vs)) ==> v ∈ set vs`

#### Distinctness

lemma splitAt_distinct_ab:

`  [| distinct vs; (a, b) = splitAt ram vs |] ==> distinct a ∧ distinct b`

lemma splitAt_distinct_a:

`  [| distinct vs; (a, b) = splitAt ram vs |] ==> distinct a`

lemma splitAt_distinct_b:

`  [| distinct vs; (a, b) = splitAt ram vs |] ==> distinct b`

lemma splitAt_distinct_fst:

`  distinct vs ==> distinct (fst (splitAt ram vs))`

lemma splitAt_distinct_snd:

`  distinct vs ==> distinct (snd (splitAt ram vs))`

lemma splitAt_distinct_ab:

`  [| distinct vs; (a, b) = splitAt ram vs |] ==> set a ∩ set b = {}`

lemma splitAt_distinct_fst_snd:

`  distinct vs ==> set (fst (splitAt ram vs)) ∩ set (snd (splitAt ram vs)) = {}`

lemma splitAt_distinct_ram_fst:

`  distinct vs ==> ram ∉ set (fst (splitAt ram vs))`

lemma splitAt_distinct_ram_snd:

`  distinct vs ==> ram ∉ set (snd (splitAt ram vs))`

lemma splitAt_1:

`  splitAt ram [] = ([], [])`

lemma splitAt_2:

`  [| v ∈ set vs; (a, b) = splitAt ram vs |] ==> v ∈ set a ∨ v ∈ set b ∨ v = ram`

lemma splitAt_or:

```  v ∈ set vs
==> v ∈ set (fst (splitAt ram vs)) ∨ v ∈ set (snd (splitAt ram vs)) ∨ v = ram```

lemma splitAt_distinct_fst:

`  distinct vs ==> distinct (fst (splitAt ram1.0 vs))`

lemma splitAt_distinct_a:

`  [| distinct vs; (a, b) = splitAt ram vs |] ==> distinct a`

lemma splitAt_distinct_snd:

`  distinct vs ==> distinct (snd (splitAt ram1.0 vs))`

lemma splitAt_distinct_b:

`  [| distinct vs; (a, b) = splitAt ram vs |] ==> distinct b`

lemma splitAt_distinct:

`  distinct vs ==> set (fst (splitAt ram vs)) ∩ set (snd (splitAt ram vs)) = {}`

lemma splitAt_subset:

`  (a, b) = splitAt ram vs ==> set a ⊆ set vs ∧ set b ⊆ set vs`

lemma splitAt_subset1:

`  (a, b) = splitAt ram vs ==> set a ⊆ set vs`

lemma splitAt_subset2:

`  (a, b) = splitAt ram vs ==> set b ⊆ set vs`

#### @{const splitAt} composition

lemma set_help:

`  v ∈ set (as @ bs) ==> v ∈ set as ∨ v ∈ set bs`

lemma splitAt_elements:

```  [| ram1.0 ∈ set vs; ram2.0 ∈ set vs |]
==> ram2.0 ∈ set (fst (splitAt ram1.0 vs)) ∨
ram2.0 ∈ set [ram1.0] ∨ ram2.0 ∈ set (snd (splitAt ram1.0 vs))```

lemma splitAt_ram2:

```  [| ram2.0 ∉ set (snd (splitAt ram1.0 vs)); ram1.0 ∈ set vs; ram2.0 ∈ set vs;
ram1.0 ≠ ram2.0 |]
==> ram2.0 ∈ set (fst (splitAt ram1.0 vs))```

lemma splitAt_ram3:

```  [| ram2.0 ∉ set (fst (splitAt ram1.0 vs)); ram1.0 ∈ set vs; ram2.0 ∈ set vs;
ram1.0 ≠ ram2.0 |]
==> ram2.0 ∈ set (snd (splitAt ram1.0 vs))```

lemma splitAt_dist_ram:

`  [| distinct vs; vs = a @ ram # b |] ==> (a, b) = splitAt ram vs`

lemma distinct_unique1:

`  [| distinct vs; ram ∈ set vs |] ==> ∃!s. vs = fst s @ ram # snd s`

lemma splitAt_dist_ram2:

```  [| distinct vs; vs = a @ ram1.0 # b @ ram2.0 # c |]
==> (a @ ram1.0 # b, c) = splitAt ram2.0 vs```

lemma splitAt_dist_ram20:

```  [| distinct vs; vs = a @ ram1.0 # b @ ram2.0 # c |]
==> c = snd (splitAt ram2.0 vs)```

lemma splitAt_dist_ram21:

```  [| distinct vs; vs = a @ ram1.0 # b @ ram2.0 # c |]
==> (a, b) = splitAt ram1.0 (fst (splitAt ram2.0 vs))```

lemma splitAt_dist_ram22:

```  [| distinct vs; vs = a @ ram1.0 # b @ ram2.0 # c |]
==> (c, []) = splitAt ram1.0 (snd (splitAt ram2.0 vs))```

lemma splitAt_dist_ram1:

```  [| distinct vs; vs = a @ ram1.0 # b @ ram2.0 # c |]
==> (a, b @ ram2.0 # c) = splitAt ram1.0 vs```

lemma splitAt_dist_ram10:

```  [| distinct vs; vs = a @ ram1.0 # b @ ram2.0 # c |]
==> a = fst (splitAt ram1.0 vs)```

lemma splitAt_dist_ram11:

```  [| distinct vs; vs = a @ ram1.0 # b @ ram2.0 # c |]
==> (a, []) = splitAt ram2.0 (fst (splitAt ram1.0 vs))```

lemma splitAt_dist_ram12:

```  [| distinct vs; vs = a @ ram1.0 # b @ ram2.0 # c |]
==> (b, c) = splitAt ram2.0 (snd (splitAt ram1.0 vs))```

lemma splitAt_dist_ram_all:

```  [| distinct vs; vs = a @ ram1.0 # b @ ram2.0 # c |]
==> (a, b) = splitAt ram1.0 (fst (splitAt ram2.0 vs)) ∧
(c, []) = splitAt ram1.0 (snd (splitAt ram2.0 vs)) ∧
(a, []) = splitAt ram2.0 (fst (splitAt ram1.0 vs)) ∧
(b, c) = splitAt ram2.0 (snd (splitAt ram1.0 vs)) ∧
c = snd (splitAt ram2.0 vs) ∧ a = fst (splitAt ram1.0 vs)```

#### Mixed

lemma fst_splitAt_rev:

```  [| distinct xs; x ∈ set xs |]
==> fst (splitAt x (rev xs)) = rev (snd (splitAt x xs))```

lemma snd_splitAt_rev:

```  [| distinct xs; x ∈ set xs |]
==> snd (splitAt x (rev xs)) = rev (fst (splitAt x xs))```

lemma splitAt_take:

`  [| distinct ls; i < |ls| |] ==> fst (splitAt (ls ! i) ls) = take i ls`

lemma splitAt_drop:

`  [| distinct ls; i < |ls| |] ==> snd (splitAt (ls ! i) ls) = drop (Suc i) ls`

lemma fst_splitAt_upt:

`  [| j ≤ i; i < k |] ==> fst (splitAt i [j..<k]) = [j..<i]`

lemma snd_splitAt_upt:

`  [| j ≤ i; i < k |] ==> snd (splitAt i [j..<k]) = [i + 1..<k]`

lemma local_help1:

`  [| vs = c @ r # d; vs = a @ r # b; r ∉ set a; r ∉ set b |] ==> a = c`

lemma local_help:

`  [| vs = a @ r # b; vs = c @ r # d; r ∉ set a; r ∉ set b |] ==> a = c ∧ b = d`

lemma local_help':

`  [| a @ r # b = c @ r # d; r ∉ set a; r ∉ set b |] ==> a = c ∧ b = d`

lemma splitAt_simp1:

`  [| ram ∉ set a; ram ∉ set b |] ==> fst (splitAt ram (a @ ram # b)) = a`

lemma splitAt_simp2:

`  ram ∉ set b ==> fst (splitAt ram (ram # b)) = []`

lemma splitAt_simp3:

`  ram ∉ set a ==> fst (splitAt ram (a @ [ram])) = a`

lemma splitAt_simp4:

`  [| ram ∉ set a; ram ∉ set b |] ==> snd (splitAt ram (a @ ram # b)) = b`

lemma help'''_in:

`  ram ∈ set b ==> fst (splitAtRec ram xs b) = xs @ fst (splitAtRec ram [] b)`

lemma help'''_notin:

`  ram ∉ set b ==> fst (splitAtRec ram xs b) = xs @ fst (splitAtRec ram [] b)`

lemma help''':

`  fst (splitAtRec ram xs b) = xs @ fst (splitAtRec ram [] b)`

lemma splitAt_simpA:

`  fst (splitAt ram (ram # b)) = []`

lemma splitAt_simpB:

`  ram ≠ a ==> fst (splitAt ram (a # b)) = a # fst (splitAt ram b)`

lemma splitAt_simpB':

`  a ≠ ram ==> fst (splitAt ram (a # b)) = a # fst (splitAt ram b)`

lemma splitAt_simpC:

`  ram ∉ set a ==> fst (splitAt ram (a @ b)) = a @ fst (splitAt ram b)`

lemma help'''':

`  snd (splitAtRec ram xs b) = snd (splitAtRec ram ys b)`

lemma splitAt_simpD:

`  ram ≠ a ==> snd (splitAt ram (a # b)) = snd (splitAt ram b)`

lemma splitAt_simpD':

`  a ≠ ram ==> snd (splitAt ram (a # b)) = snd (splitAt ram b)`

lemma splitAt_simpE:

`  snd (splitAt ram (ram # b)) = b`

lemma splitAt_simpF:

`  ram ∉ set a ==> snd (splitAt ram (a @ b)) = snd (splitAt ram b)`

lemma splitAt_rotate_pair_conv:

```  [| 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)```

### @{text between}

lemma inbetween_inset:

`  x ∈ set (between xs a b) ==> x ∈ set xs`

lemma notinset_notinbetween:

`  x ∉ set xs ==> x ∉ set (between xs a b)`

lemma set_between_id:

`  [| distinct xs; x ∈ set xs |] ==> set (between xs x x) = set xs - {x}`

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```

### Tables

lemma isTable_eq:

`  isTable E vs ((a, b) # ps) ==> b = E a`

lemma isTable_subset:

`  [| set qs ⊆ set ps; isTable E vs ps |] ==> isTable E vs qs`

lemma isTable_Cons:

`  isTable E vs ((a, b) # ps) ==> isTable E vs ps`

lemma removeKey_subset:

`  set (removeKey a ps) ⊆ set ps`

lemma length_removeKey:

`  |removeKey w ps| ≤ |ps|`

lemma length_removeKeyList:

`  |removeKeyList ws ps| ≤ |ps|`

lemma removeKeyList_subset:

`  set (removeKeyList ws ps) ⊆ set ps`

lemma notin_removeKey1:

`  (a, b) ∉ set (removeKey a ps)`

lemma notin_removeKey:

`  r ∉ fst ` set (removeKey r ps)`

lemma notin_removeKeyList1:

`  a ∈ set rs ==> (a, b) ∉ set (removeKeyList rs ps)`

lemma notin_removeKeyList:

`  r ∈ set rs ==> r ∉ fst ` set (removeKeyList rs ps)`

lemma removeKeyList_eq:

`  removeKeyList as ps = [p∈ps . ∀a∈set as. a ≠ fst p]`

lemma removeKey_empty:

`  removeKey a [] = []`

lemma removeKeyList_empty:

`  removeKeyList ps [] = []`

lemma removeKeyList_cons:

```  removeKeyList ws (p # ps) =
(if fst p ∈ set ws then removeKeyList ws ps else p # removeKeyList ws ps)```