(* 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 ram_{1}ram_{2}≡ let (pre_{1}, post_{1}) = splitAt ram_{1}vs in if ram_{2}mem post_{1}then let (pre_{2}, post_{2}) = splitAt ram_{2}post_{1}in pre_{2}else let (pre_{2}, post_{2}) = splitAt ram_{2}pre_{1}in post_{1}@ pre_{2}" 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

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}

lemma length3D:

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

lemma length4D:

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

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)

lemma

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

lemma

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

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)

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

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

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|

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)

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

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

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

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

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)

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)

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

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)