(* ID: $Id: ListAux.thy,v 1.3 2006/01/11 19:40:44 nipkow Exp $
Author: Gertrud Bauer, Tobias Nipkow
*)
header {* Basic Functions Old and New *}
theory ListAux
imports Main EfficientNat
begin
declare Let_def[simp]
declare comp_def[code unfold]
subsection {* HOL *}
lemma pairD: "(a,b) = p ==> a = fst p ∧ b = snd p"
by auto
lemmas conj_aci = conj_comms conj_assoc conj_absorb conj_left_absorb
lemma [code unfold]: "max x y == (let u = x; v = y in if u <= v then v else u)"
by(simp add:max_def)
lemma [code unfold]: "min x y == (let u = x; v = y in if u <= v then u else v)"
by(simp add:min_def)
lemmas[code] = lessThan_0 lessThan_Suc
subsection {* Lists *}
declare mem_iff[simp] list_all_iff[simp] list_ex_iff[simp]
subsubsection{* @{text length} *}
syntax "_length" :: "'a list => nat" ("|_|")
translations
"|xs|" == "length xs"
lemma length3D: "|xs| = 3 ==> ∃x y z. xs = [x, y, z]"
apply (cases xs) apply simp
apply (case_tac list) apply simp
apply (case_tac lista) by simp_all
lemma length4D: "|xs| = 4 ==> ∃ a b c d. xs = [a, b, c, d]"
apply (case_tac xs) apply simp
apply (case_tac list) apply simp
apply (case_tac lista) apply simp
apply (case_tac listb) by simp_all
subsubsection {* @{const filter} *}
lemma filter_emptyE[dest]: "(filter P xs = []) ==> x ∈ set xs ==> ¬ P x"
by (simp add: filter_empty_conv)
lemma filter_comm: "[x ∈ xs. P x ∧ Q x] = [x ∈ xs. Q x ∧ P x]"
by (simp add: conj_aci)
lemma filter1: " [x∈xs . P x] = [] ==>
[x∈ xs. Q x ∧ P x] = []"
by (induct xs) (simp_all split: split_if_asm)
lemma filter_prop: "!!x. x ∈ set [u∈ys . P u] ==> P x"
proof (induct ys)
case Nil then show ?case by simp
next
case (Cons y ys) then show ?case
by (auto split: split_if_asm)
qed
lemma filter_Cons_prop: "[u∈ys . P u] = x # xs ==> P x"
proof -
assume "[u∈ys . P u] = x # xs"
then have "x ∈ set [u∈ys . P u]" by simp
then show "P x" by (rule filter_prop)
qed
lemma filter_compl1:
"([x ∈ xs. P x] = []) = ([x ∈ xs. ¬ P x] = xs)" (is "?lhs = ?rhs")
proof
show "?rhs ==> ?lhs"
proof (induct xs)
case Nil then show ?case by simp
next
case (Cons x xs)
have "[u∈xs . ¬ P u] ≠ x # xs"
proof
assume "[u∈xs . ¬ P u] = x # xs"
then have "|x # xs| = |[u∈xs . ¬ P u]|" by simp
also have "... ≤ |xs|" by simp
finally show False by simp
qed
with Cons show ?case by auto
qed
next
show "?lhs ==> ?rhs"
by (induct xs) (simp_all split: split_if_asm)
qed
lemma [simp]: "Not o (Not o P) = P"
by (rule ext) simp
lemma filter_compl2: "!!P. (filter (Not o P) xs = []) = (filter P xs = xs)"
by (simp add: filter_compl1)
lemma filter_eqI:
"(!!v. v ∈ set vs ==> P v = Q v) ==> [v ∈ vs . P v] = [v ∈ vs . Q v]"
by (induct vs) simp_all
lemma filter_simp: "(!!x. x ∈ set xs ==> P x) ==> [x ∈ xs. P x ∧ Q x] = [x ∈ xs. Q x]"
by (induct xs) auto
lemma filter_True_eq1:
"(length [y ∈ xs. P y] = length xs) ==> (!!y. y ∈ set xs ==> P y)"
proof (induct xs)
case Nil then show ?case by simp
next
case (Cons x xs)
have l: "length (filter P xs) ≤ length xs"
by (simp add: length_filter_le)
have hyp: "length (filter P (x # xs)) = length (x # xs)" .
then have "P x" by (simp split: split_if_asm) (insert l, arith)
moreover with hyp have "length (filter P xs) = length xs"
by (simp split: split_if_asm)
moreover have "y ∈ set (x#xs)" .
ultimately show ?case by (auto dest: Cons(1))
qed
lemma length_filter_True_eq:
"(length [y ∈ xs. P y] = length xs) = (∀y. y ∈ set xs --> P y)"
by (intro iffI allI impI, erule filter_True_eq1) simp_all
subsubsection {* @{const map} *}
syntax (xsymbols)
"@map" :: "[ 'b, pttrn, 'a list] => 'a list"("(1[_. _ ∈ _])")
syntax
"@map" :: "[ 'b, pttrn, 'a list] => 'a list"("(1[_./ _ : _])")
translations
"[f. x ∈ xs]"== "map (λx. f) xs"
"[f. x : xs]"== "map (λx. f) xs";
subsubsection {* @{const map_filter} *}
syntax (xsymbols)
"@map_filter" :: "['b, pttrn, 'a list, bool] => 'a list"("(1[_. _ ∈ _, _])")
syntax
"@map_filter" :: "['b, pttrn, 'a list, bool] => 'a list"("(1[_./ _ : _, _])")
translations
"[f. x ∈ xs, P]"== "map_filter (λx. f) P xs"
"[f. x : xs, P]"== "map_filter (λx. f) P xs"
lemma [simp]: "[f x. x ∈ xs, P] = [f x. x ∈ [x ∈ xs. P x]]"
by (induct xs) auto
subsubsection {* @{const concat} *}
syntax (xsymbols)
"@concat" :: "idt => 'a list => 'a list => 'a list" ("\<Squnion>_∈ _ _" 10)
translations "\<Squnion>x∈xs f" == "concat [f. x ∈ xs]"
subsubsection {* List product *}
constdefs listProd1 :: "'a => 'b list => ('a × 'b) list"
"listProd1 a bs ≡ [(a,b). b ∈ bs]"
constdefs listProd :: "'a list => 'b list => ('a × 'b) list" (infix "×" 50)
"as × bs ≡ \<Squnion>a ∈ as listProd1 a bs"
lemma(*<*)[simp]: (*>*) "set (xs × ys) = (set xs) × (set ys)"
by (auto simp: listProd_def listProd1_def)
subsubsection {* Minimum and maximum *}
(* FIXME combine minimal with min_list *)
(* more general:
foldl1 f (x#xs) = if xs=[] then x else f x (foldl1 f xs)
min_list = foldl1 min
max_list = foldl1 max
sum_list = foldl1 (op +)
Put in separate ExecList.thy
*)
consts minimal:: "('a => nat) => 'a list => 'a"
primrec
"minimal m (x#xs) =
(if xs=[] then x else
let mxs = minimal m xs in
if m x ≤ m mxs then x else mxs)"
lemma minimal_in_set[simp]: "xs ≠ [] ==> minimal f xs : set xs"
by(induct xs) auto
lemma minimal_Cons1:
"∀y ∈ set xs. f x ≤ f y ==> minimal f (x#xs) = x"
by (induct xs) auto
lemma minimal_append2:
"∀x ∈ set xs. f x > f y ==> minimal f (xs @ y # ys) = minimal f (y # ys)"
by (induct xs) simp_all
lemma minimal_neq_lowerbound:
"xs ≠ [] ==> ALL x: set xs. f x ≥ n ==> f(minimal f xs) ≠ n
==> ALL x: set xs. f x ≠ n"
apply(induct xs)
apply simp
apply (auto split:split_if_asm)
done
(* FIXME minList to min_list *)
consts minList :: "nat list => nat"
primrec
"minList (x#xs) = (if xs=[] then x else min x (minList xs))"
consts max_list :: "nat list => nat"
primrec
"max_list (x#xs) = (if xs=[] then x else max x (max_list xs))"
lemma minList_conv_Min[simp]:
"xs ≠ [] ==> minList xs = Min(set xs)"
by (induct xs) auto
lemma max_list_conv_Max[simp]:
"xs ≠ [] ==> max_list xs = Max(set xs)"
by (induct xs) auto
subsubsection {* replace *}
(* FIXME replace "remove1" by "replace1" in List.thy? *)
consts replace :: "'a => 'a list => 'a list => 'a list"
primrec
"replace x ys [] = []"
"replace x ys (z#zs) =
(if z = x then ys @ zs else z # (replace x ys zs))"
consts mapAt :: "nat list => ('a => 'a) => ('a list => 'a list)"
primrec
"mapAt [] f as = as"
"mapAt (n#ns) f as =
(if n < |as| then mapAt ns f (as[n:= f (as!n)])
else mapAt ns f as)"
lemma length_mapAt[simp]: "!!xs. length(mapAt vs f xs) = length xs"
by(induct vs) auto
lemma length_replace1[simp]: "length(replace x [y] xs) = length xs"
by(induct xs) simp_all
lemma replace_id[simp]: "replace x [x] xs = xs"
by(induct xs) simp_all
lemma len_replace_ge_same:
"length ys ≥ 1 ==> length(replace x ys xs) ≥ length xs"
by (induct xs) auto
lemma len_replace_ge[simp]:
"[| length ys ≥ 1; length xs ≥ length zs |] ==>
length(replace x ys xs) ≥ length zs"
apply(drule len_replace_ge_same[where x = x and xs = xs])
apply arith
done
lemma replace_append[simp]:
"replace x ys (as @ bs) =
(if x ∈ set as then replace x ys as @ bs else as @ replace x ys bs)"
by(induct as) auto
lemma filter_replace:
"¬ P y ==> filter P (replace x [y] xs) = remove1 x (filter P xs)"
by(induct xs) simp_all
lemma distinct_set_replace: "distinct xs ==>
set (replace x ys xs) =
(if x ∈ set xs then (set xs - {x}) ∪ set ys else set xs)"
apply(induct xs)
apply(simp)
apply simp
apply blast
done
lemma replace1:
"f ∈ set (replace f' fs ls ) ==> f ∉ set ls ==> f ∈ set fs"
proof (induct ls)
case Nil then show ?case by simp
next
case (Cons l ls) then show ?case by (simp split: split_if_asm)
qed
lemma replace2:
"f' ∉ set ls ==> replace f' fs ls = ls"
proof (induct ls)
case Nil then show ?case by simp
next
case (Cons l ls) then show ?case by (auto split: split_if_asm)
qed
lemma replace3[intro]:
"f' ∈ set ls ==> f ∈ set fs ==> f ∈ set (replace f' fs ls)"
by (induct ls) auto
lemma replace4:
"f ∈ set ls ==> oldF ≠ f ==> f ∈ set (replace oldF fs ls)"
by (induct ls) auto
lemma replace5: "f ∈ set (replace oldF newfs fs) ==> f ∈ set fs ∨ f ∈ set newfs"
by (induct fs) (auto split: split_if_asm)
lemma replace6: "distinct oldfs ==> x ∈ set (replace oldF newfs oldfs) =
((x ≠ oldF ∨ oldF ∈ set newfs) ∧ ((oldF ∈ set oldfs ∧ x ∈ set newfs) ∨ x ∈ set oldfs))"
by (induct oldfs) auto
lemma replace_delete_oldF:
"oldF ∉ set fs ==> distinct ls ==> oldF ∉ set (replace oldF fs ls)"
by (induct ls) auto
lemma distinct_replace:
"distinct fs ==> distinct newFs ==> set fs ∩ set newFs ⊆ {oldF} ==>
distinct (replace oldF newFs fs)"
proof (induct fs)
case Nil then show ?case by simp
next
case (Cons f fs)
then show ?case
proof (cases "f = oldF")
case True with Cons show ?thesis by simp blast
next
case False
moreover with Cons have "f ∉ set newFs" by simp blast
with Cons have "f ∉ set (replace oldF newFs fs)"
by simp (blast dest: replace1)
moreover from Cons have "distinct (replace oldF newFs fs)"
by (rule_tac Cons) auto
ultimately show ?thesis by simp
qed
qed
lemma replace_replace[simp]: "oldf ∉ set newfs ==> distinct xs ==>
replace oldf newfs (replace oldf newfs xs) = replace oldf newfs xs"
apply (induct xs) apply auto apply (rule replace2) by simp
lemma replace_distinct: "distinct fs ==> distinct newfs ==> oldf ∈ set fs --> set newfs ∩ set fs ⊆ {oldf} ==>
distinct (replace oldf newfs fs)"
apply (case_tac "oldf ∈ set fs") apply simp
apply (induct fs) apply simp
apply (auto simp: replace2) apply (drule replace1)
by auto
lemma filter_replace2:
"[| ¬ P x; ∀y∈ set ys. ¬ P y |] ==>
filter P (replace x ys xs) = filter P xs"
apply(cases "x ∈ set xs")
prefer 2 apply(simp add:replace2)
apply(induct xs)
apply simp
apply clarsimp
done
lemma length_filter_replace1:
"[| x ∈ set xs; ¬ P x |] ==>
length(filter P (replace x ys xs)) =
length(filter P xs) + length(filter P ys)"
apply(induct xs)
apply simp
apply fastsimp
done
lemma length_filter_replace2:
"[| x ∈ set xs; P x |] ==>
length(filter P (replace x ys xs)) =
length(filter P xs) + length(filter P ys) - 1"
apply(induct xs)
apply simp
apply auto
apply(drule split_list)
apply clarsimp
done
subsubsection {* @{const"distinct"} *}
lemma dist_filter_single:
"distinct ls ==> v ∈ set ls ==> [a∈ ls . a = v] = [v]"
proof (induct ls)
case Nil then show ?case by auto
next
case (Cons l ls) then show ?case
proof (cases "l = v")
case True with Cons
have "v ∉ set ls" by auto
then have "[a∈ls . a = v] = []" by (induct ls) auto
with Cons True show ?thesis by auto
next
case False with Cons show ?thesis by auto
qed
qed
lemma dist_at1: "!! c vs. distinct vs ==> vs = a @ r # b ==> vs = c @ r # d ==> a = c"
proof (induct a)
case Nil
assume dist: "distinct vs" and vs1: "vs = [] @ r # b" and vs2: "vs = c @ r # d"
from dist vs2 have rc: "r ∉ set c" by auto
from vs1 vs2 have "c @ r # d = r # b" by auto
then have "hd (c @ r # d) = r" by auto
then have "c ≠ [] ==> hd c = r" by auto
then have "c ≠ [] ==> r ∈ set c" by (induct c) auto
with rc have c: "c = []" by auto
then show ?case by auto
next
case (Cons x xs) then show ?case by (induct c) auto
qed
lemma dist_at: "distinct vs ==> vs = a @ r # b ==> vs = c @ r # d ==> a = c ∧ b = d"
proof -
assume dist: "distinct vs" and vs1: "vs = a @ r # b" and vs2: "vs = c @ r # d"
then have "a = c" by (rule_tac dist_at1) auto
with dist vs1 vs2 show ?thesis by simp
qed
lemma dist_at2: "distinct vs ==> vs = a @ r # b ==> vs = c @ r # d ==> b = d"
proof -
assume dist: "distinct vs" and vs1: "vs = a @ r # b" and vs2: "vs = c @ r # d"
then have "a = c ∧ b = d" by (rule_tac dist_at) auto
then show ?thesis by auto
qed
lemma distinct_split1: "distinct xs ==> xs = y @ [r] @ z ==> r ∉ set y"
apply auto done
lemma distinct_split2: "distinct xs ==> xs = y @ [r] @ z ==> r ∉ set z" apply auto done
lemma distinct_hd_not_cons: "distinct vs ==> ∃ as bs. vs = as @ x # hd vs # bs ==> False"
proof -
assume d: "distinct vs" and ex: "∃ as bs. vs = as @ x # hd vs # bs"
from ex have vsne: "vs ≠ []" by auto
with d ex show ?thesis apply (elim exE) apply (case_tac "as")
apply (subgoal_tac "hd vs = x") apply simp apply (rule sym) apply simp
apply (subgoal_tac "x = hd (x # (hd vs # bs))") apply simp apply (thin_tac "vs = x # hd vs # bs")
apply auto
apply (subgoal_tac "hd vs = a") apply simp
apply (subgoal_tac "a = hd (a # list @ x # hd vs # bs)") apply simp
apply (thin_tac "vs = a # list @ x # hd vs # bs") by auto
qed
subsubsection {* Misc *}
(* FIXME move to List *)
lemma drop_last_in: "!!n. n < length ls ==> last ls ∈ set (drop n ls)"
apply (frule_tac last_drop) apply(erule subst)
apply (case_tac "drop n ls" rule: rev_exhaust) by simp_all
lemma nth_last_Suc_n: "distinct ls ==> n < length ls ==> last ls = ls ! n ==> Suc n = length ls"
proof (rule ccontr)
assume d: "distinct ls" and n: "n < length ls" and l: "last ls = ls ! n" and not: "Suc n ≠ length ls"
then have s: "Suc n < length ls" by auto
def lls ≡ "ls!n"
with n have "take (Suc n) ls = take n ls @ [lls]" apply simp by (rule take_Suc_conv_app_nth)
then have "take (Suc n) ls @ drop (Suc n) ls = take n ls @ [lls] @ drop (Suc n) ls" by auto
then have ls: "ls = take n ls @ [lls] @ drop (Suc n) ls" by auto
with d have dls: "distinct (take n ls @ [lls] @ drop (Suc n) ls)" by auto
from lls_def l have "lls = (last ls)" by auto
with s have "lls ∈ set (drop (Suc n) ls)" apply simp by (rule_tac drop_last_in)
with dls show False by auto
qed
(****************************** rotate *************************)
subsubsection {* @{const rotate} *}
lemma plus_length1[simp]: "rotate (k+(length ls)) ls = rotate k ls "
proof -
have "!! k ls. rotate k (rotate (length ls) ls) = rotate (k+(length ls)) ls"
by (rule rotate_rotate)
then have "!! k ls. rotate k ls = rotate (k+(length ls)) ls" by auto
then show ?thesis by (rule sym)
qed
lemma plus_length2[simp]: "rotate ((length ls)+k) ls = rotate k ls "
proof -
def x ≡ "(length ls)+k"
then have "x = k+(length ls)" by auto
with x_def have "rotate x ls = rotate (k+(length ls)) ls" by simp
then have "rotate x ls = rotate k ls" by simp
with x_def show ?thesis by simp
qed
lemma rotate_minus1: "n > 0 ==> m > 0 ==>
rotate n ls = rotate m ms ==> rotate (n - 1) ls = rotate (m - 1) ms"
proof (cases "ls = []")
assume r: "rotate n ls = rotate m ms"
case True with r
have "rotate m ms = []" by auto
then have "ms = []" by auto
with True show ?thesis by auto
next
assume n: "n > 0" and m: "m > 0" and r: "rotate n ls = rotate m ms"
case False
then have lls: "length ls > 0" by auto
with r have lms: "length ms > 0" by auto
have mem1: "rotate (n - 1) ls = rotate ((n - 1) + length ls) ls" by auto
from n lls have "(n - 1) + length ls = (length ls - 1) + n" by arith
then have "rotate ((n - 1) + length ls) ls = rotate ((length ls - 1) + n) ls" by auto
with mem1 have mem2: "rotate (n - 1) ls = rotate ((length ls - 1) + n) ls" by auto
have "rotate ((length ls - 1) + n) ls = rotate (length ls - 1) (rotate n ls)" apply (rule sym)
by (rule rotate_rotate)
with mem2 have mem3: "rotate (n - 1) ls = rotate (length ls - 1) (rotate n ls)" by auto
from r have "rotate (length ls - 1) (rotate n ls) = rotate (length ls - 1) (rotate m ms)" by auto
with mem3 have mem4: "rotate (n - 1) ls = rotate (length ls - 1) (rotate m ms)" by auto
have "rotate (length ls - 1) (rotate m ms) = rotate (length ls - 1 + m) ms" by (rule rotate_rotate)
with mem4 have mem5: "rotate (n - 1) ls = rotate (length ls - 1 + m) ms" by auto
from r have "length (rotate n ls) = length (rotate m ms)" by simp
then have "length ls = length ms" by auto
with m lms have "length ls - 1 + m = (m - 1) + length ms" by arith
with mem5 have mem6: "rotate (n - 1) ls = rotate ((m - 1) + length ms) ms" by auto
have "rotate ((m - 1) + length ms) ms = rotate (m - 1) (rotate (length ms) ms)" by auto
then have "rotate ((m - 1) + length ms) ms = rotate (m - 1) ms" by auto
with mem6 show ?thesis by auto
qed
lemma rotate_minus1': "n > 0 ==> rotate n ls = ms ==>
rotate (n - 1) ls = rotate (length ms - 1) ms"
proof (cases "ls = []")
assume r: "rotate n ls = ms"
case True with r show ?thesis by auto
next
assume n: "n > 0" and r:"rotate n ls = ms"
then have r': "rotate n ls = rotate (length ms) ms" by auto
case False
with n r' show ?thesis apply (rule_tac rotate_minus1) by auto
qed
lemma rotate_inv1: "!! ms. n < length ls ==> rotate n ls = ms ==>
ls = rotate ((length ls) - n) ms"
proof (induct n)
case 0 then show ?case by auto
next
case (Suc n) then show ?case
proof (cases "ls = []")
case True with Suc
show ?thesis by auto
next
case False
then have ll: "length ls > 0" by auto
from Suc have nl: "n < length ls" by auto
from Suc have r: "rotate (Suc n) ls = ms" by auto
then have "rotate (Suc n - 1) ls = rotate (length ms - 1) ms" apply (rule_tac rotate_minus1') by auto
then have "rotate n ls = rotate (length ms - 1) ms" by auto
then have mem: "ls = rotate (length ls - n) (rotate (length ms - 1) ms)"
apply (rule_tac Suc) by (auto simp: nl)
have " rotate (length ls - n) (rotate (length ms - 1) ms) = rotate (length ls - n + (length ms - 1)) ms"
by (rule rotate_rotate)
with mem have mem2: "ls = rotate (length ls - n + (length ms - 1)) ms" by auto
from r have leq: "length ms = length ls" by auto
with False nl have "length ls - n + (length ms - 1) = length ms + (length ms - (Suc n))"
by arith
then have "rotate (length ls - n + (length ms - 1)) ms = rotate (length ms + (length ms - (Suc n))) ms"
by auto
with mem2 have mem3: "ls = rotate (length ms + (length ms - (Suc n))) ms" by auto
have "rotate (length ms + (length ms - (Suc n))) ms = rotate (length ms - (Suc n)) ms" by simp
with mem3 leq show ?thesis by auto
qed
qed
lemma rotate_conv_mod'[simp]: "rotate (n mod length ls) ls = rotate n ls"
by(simp add:rotate_drop_take)
lemma rotate_inv2: "rotate n ls = ms ==>
ls = rotate ((length ls) - (n mod length ls)) ms"
proof (cases "ls = []")
assume r: "rotate n ls = ms"
case True with r show ?thesis by auto
next
assume r: "rotate n ls = ms"
then have r': "rotate (n mod length ls) ls = ms" by auto
case False
then have "length ls > 0" by auto
with r' show ?thesis apply (rule_tac rotate_inv1) by auto
qed
lemma rotate_inv': "ls = rotate ((length ls) - (n mod length ls)) ms ==>
rotate n ls = ms"
proof (cases "ls = []")
assume r: "ls = rotate ((length ls) - (n mod length ls)) ms"
case True with r show ?thesis by auto
next
assume r: "ls = rotate ((length ls) - (n mod length ls)) ms"
case False
def len ≡ "length ls"
with r have r': "ls = rotate (len - (n mod len)) ms" by simp
with len_def have lms: "length ms = len" by auto
def y ≡ "n mod len"
from len_def False have ll: "len > 0" by auto
with y_def have small_y: "y < len" by auto
then have len_gz: "len > 0" by auto
from r' len_def have mem0: "rotate n ls = rotate n (rotate (len - (n mod len)) ms)" by auto
have "rotate n (rotate (len - (n mod len)) ms) = rotate (n + (len - (n mod len))) ms"
by (rule rotate_rotate)
with mem0 have mem1: "rotate n ls = rotate (n + (len - (n mod len))) ms" by auto
have "n mod len - n mod len = 0" by arith
then have "len + n mod len - n mod len = len" by arith
from y_def have ymod: "n mod len = y" by auto
with len_gz obtain r where n: "n = y + r*len" apply (drule_tac mod_eqD) by auto
then have "n + len = (r*len)+len + y" by arith
then have "n + len = ((r+1)*len) + y" by auto
with len_gz small_y have "n + (len - y) = ((r+1)*len)" by auto
then have zero: "(n + (len - y)) mod len = 0" by auto
have "rotate (n + (len - y)) ms = rotate ((n + (len - y)) mod length ms) ms" by (rule_tac rotate_conv_mod)
with lms zero have "rotate (n + (len - y)) ms = ms" by auto
with mem1 y_def show ?thesis by auto
qed
lemma rotate_id[simp]: "rotate ((length ls) - (n mod length ls)) (rotate n ls) = ls"
apply (rule sym) apply (rule rotate_inv2) by simp
lemma nth_rotate1_Suc: "Suc n < length ls ==> ls!(Suc n) = (rotate1 ls)!n"
apply (auto simp: rotate1_def) apply (cases ls) apply auto
by (simp add: nth_append)
lemma nth_rotate1_0: "ls!0 = (rotate1 ls)!(length ls - 1)" apply (cases ls) by (auto simp: rotate1_def)
lemma nth_rotate1: "0 < length ls ==> ls!((Suc n) mod (length ls)) = (rotate1 ls)!(n mod (length ls))"
proof (cases "0 < (Suc n) mod (length ls)")
assume lls: "0 < length ls"
case True
def m ≡ "(Suc n) mod (length ls) - 1"
with True have m: "Suc m = (Suc n) mod (length ls)" by auto
with lls have a: "(Suc m) < length ls" by auto
from lls m have "m = n mod (length ls)" by (simp add: mod_Suc split:split_if_asm)
with a m show ?thesis apply (drule_tac nth_rotate1_Suc) by auto
next
assume lls: "0 < length ls"
case False
then have a: "(Suc n) mod (length ls) = 0" by auto
with lls have "Suc (n mod (length ls)) = (length ls)" by (auto simp: mod_Suc split: split_if_asm)
then have "(n mod (length ls)) = (length ls) - 1" by arith
with a show ?thesis by (auto simp: nth_rotate1_0)
qed
lemma rotate_Suc2[simp]: "rotate n (rotate1 xs) = rotate (Suc n) xs"
apply (simp add:rotate_def) apply (induct n) by auto
lemma nth_rotate: "!! ls. 0 < length ls ==> ls!((n+m) mod (length ls)) = (rotate m ls)!(n mod (length ls))"
proof (induct m)
case 0 then show ?case by auto
next
case (Suc m)
def z ≡ "n + m"
then have "n + Suc m = Suc (z)" by auto
with Suc have r1: "ls ! ((Suc z) mod length ls) = rotate1 ls ! (z mod length ls)"
by (rule_tac nth_rotate1)
from Suc have "0 < length (rotate1 ls)" by auto
then have "(rotate1 ls) ! ((n + m) mod length (rotate1 ls))
= rotate m (rotate1 ls) ! (n mod length (rotate1 ls))" by (rule Suc)
with r1 z_def have "ls ! ((n + Suc m) mod length ls)
= rotate m (rotate1 ls) ! (n mod length (rotate1 ls))" by auto
then show ?case by auto
qed
lemma help1: "∃ n. filter f (rotate1 ls) = rotate n (filter f ls)"
proof (cases ls)
case Nil then show ?thesis by auto
next
case (Cons m ms)
then show ?thesis
proof (cases "f m")
case True with Cons
have "filter f (rotate1 (ls)) = rotate 1 (filter f (ls))" by auto
then show ?thesis apply (rule_tac exI) .
next
case False with Cons
have "filter f (rotate1 (ls)) = rotate 0 (filter f (ls))" by auto
then show ?thesis apply (rule_tac exI) .
qed
qed
lemma help3: "¬ f l ==> n < length ls ==> filter f (rotate n ls) = filter f (rotate n (rotate1 (l # ls)))"
proof -
assume fl: "¬ f l" and n: "n < length ls"
then have n2: "n - length ls = 0" by auto
from fl n show ?thesis apply simp
apply (subst rotate_drop_take)+ by auto
qed
lemma help4: "¬ f l ==> n < length ls ==> filter f (rotate n ls) = filter f (rotate (Suc n) (l # ls))"
proof -
assume fl: "¬ f l" and n: "n < length ls"
then have r1: "filter f (rotate n ls) = filter f (rotate n (rotate1 (l # ls)))" by (rule help3)
def ms ≡ "l # ls"
have "rotate n (rotate1 (ms)) = rotate (Suc n) (ms)" by simp
with ms_def have "rotate n (rotate1 (l # ls)) = rotate (Suc n) (l # ls)" by simp
with r1 show ?thesis by auto
qed
lemma help2: "∃ n. rotate1 (filter f ls) = filter f (rotate n ls)"
proof (induct ls)
case Nil then show ?case by auto
next
case (Cons m ms)
then show ?case
proof (cases "f m")
case True with Cons
have "filter f (m # ms) = m # filter f ms" by auto
from True Cons have
"rotate1 (filter f (m # ms)) = filter f (rotate 1 (m # ms))" by auto
then show ?thesis apply (rule_tac exI) .
next
case False with Cons
have f1: "filter f (m # ms) = filter f ms" by auto
then have mem: "rotate1 (filter f (m # ms)) = rotate1 (filter f ms)" by auto
from False have f2: "!! ks. filter f (ks @ [m]) = filter f ks" by auto
from Cons obtain n where n: "rotate1 (filter f ms) = filter f (rotate n ms)" by auto
with mem have mem1: "rotate1 (filter f (m # ms)) = filter f (rotate n ms)" by auto
def n' ≡ "n mod length ms"
then have "filter f (rotate n ms) = filter f (rotate n' ms)" by auto
with mem1 have mem2: "rotate1 (filter f (m # ms)) = filter f (rotate n' ms)" by auto
from n'_def have "ms ≠ [] ==> n' < length ms" by auto
with False have "filter f (rotate n' ms) = filter f (rotate (Suc n') (m # ms))"
apply (case_tac "ms = []") apply force apply (rule_tac help4) by auto
with mem2 have "rotate1 (filter f (m # ms)) = filter f ((rotate (Suc n') (m # ms)))" by auto
then show ?thesis apply (rule_tac exI) .
qed
qed
lemma rotate_help5: "∃ n. filter f (rotate m ls) = rotate n (filter f ls)"
proof (induct m)
case 0 then have "filter f (rotate 0 ls) = rotate 0 (filter f ls)" by auto
then show ?case by (rule exI)
next
case (Suc m)
def ks ≡ "rotate m ls"
then have mem0: "filter f (rotate (Suc m) ls) = filter f (rotate1 ks)" by auto
from ks_def Suc obtain n where n: "filter f ks = rotate n (filter f ls)" by auto
have "∃ n'. filter f (rotate1 ks) = rotate n' (filter f ks)" by (rule help1)
then obtain n' where "filter f (rotate1 ks) = rotate n' (filter f ks)" by auto
with n have "filter f (rotate1 ks) = rotate n' (rotate n (filter f ls))" by auto
with mem0 have mem1: "filter f (rotate (Suc m) ls) = rotate n' (rotate n (filter f ls))" by auto
have "rotate n' (rotate n (filter f ls)) = rotate (n'+n) (filter f ls)" by (rule rotate_rotate)
with mem1 have "filter f (rotate (Suc m) ls) = rotate (n'+n) (filter f ls)" by auto
then show ?case apply (rule_tac exI) .
qed
lemma rotate_help6: "∃ n. rotate m (filter f ls) = filter f (rotate n ls)"
proof (induct m)
case 0 then have "rotate 0 (filter f ls) = filter f (rotate 0 ls)" by auto
then show ?case by (rule exI)
next
case (Suc m)
have mem0: "rotate (Suc m) (filter f ls) = rotate1 (rotate m (filter f ls))" by auto
from Suc obtain n where n: "rotate m (filter f ls) = filter f (rotate n ls)" by auto
with mem0 have mem1: "rotate (Suc m) (filter f ls) = rotate1 (filter f (rotate n ls))" by auto
def ks ≡ "rotate n ls"
from help2 obtain n' where "rotate1 (filter f ks) = filter f (rotate n' ks)" by auto
with mem1 ks_def have mem2: "rotate (Suc m) (filter f ls) = filter f (rotate n' ks)" by auto
from ks_def have "rotate n' ks = rotate (n'+n) ls" apply simp by (rule rotate_rotate)
with mem2 have "rotate (Suc m) (filter f ls) = filter f(rotate (n'+n) ls)" by simp
then show ?case apply (rule_tac exI) .
qed
(************************* SplitAt *******************************************)
subsection {* @{text splitAt} *}
consts splitAtRec ::
"'a => 'a list => 'a list => 'a list × 'a list"
primrec
"splitAtRec c bs [] = (bs,[])"
"splitAtRec c bs (a#as) = (if a = c then (bs, as)
else splitAtRec c (bs@[a]) as)"
constdefs splitAt :: "'a => 'a list => 'a list × 'a list"
"splitAt c as ≡ splitAtRec c [] as"
subsubsection {* @{const splitAtRec} *}
lemma splitAtRec_conv: "!!bs.
splitAtRec x bs xs =
(bs @ takeWhile (%y. y≠x) xs, tl(dropWhile (%y. y≠x) xs))"
by(induct xs) auto
lemma splitAtRec_distinct_fst: "!! s. distinct vs ==> distinct s ==> (set s) ∩ (set vs) = {} ==> distinct (fst (splitAtRec ram1 s vs))"
by (induct vs) auto
lemma splitAtRec_distinct_snd: "!! s. distinct vs ==> distinct s ==> (set s) ∩ (set vs) = {} ==> distinct (snd (splitAtRec ram1 s vs))"
by (induct vs) auto
lemma splitAtRec_ram:
"!! us a b. ram ∈ set vs ==> (a, b) = splitAtRec ram us vs ==>
us @ vs = a @ [ram] @ b"
proof (induct vs)
case Nil then show ?case by simp
next
case (Cons v vs) then show ?case by (auto dest: Cons(1) split: split_if_asm)
qed
lemma splitAtRec_notRam:
"!! us. ram ∉ set vs ==> splitAtRec ram us vs = (us @ vs, [])"
proof (induct vs)
case Nil then show ?case by simp
next
case (Cons v vs) then show ?case by auto
qed
lemma splitAtRec_distinct: "!! s. distinct vs ==>
distinct s ==> (set s) ∩ (set vs) = {} ==>
set (fst (splitAtRec ram s vs)) ∩ set (snd (splitAtRec ram s vs)) = {}"
by (induct vs) auto
subsubsection {* @{const splitAt} *}
lemma splitAt_conv:
"splitAt x xs = (takeWhile (%y. y≠x) xs, tl(dropWhile (%y. y≠x) xs))"
by(simp add: splitAt_def splitAtRec_conv)
lemma splitAt_no_ram[simp]:
"ram ∉ set vs ==> splitAt ram vs = (vs, [])"
by (auto simp: splitAt_def splitAtRec_notRam)
lemma splitAt_split:
"ram ∈ set vs ==> (a,b) = splitAt ram vs ==> vs = a @ ram # b"
by (auto simp: splitAt_def dest: splitAtRec_ram)
lemma splitAt_ram:
"ram ∈ set vs ==> vs = fst (splitAt ram vs) @ ram # snd (splitAt ram vs)"
by (rule_tac splitAt_split) auto
lemma fst_splitAt_last:
"[| xs ≠ []; distinct xs |] ==> fst (splitAt (last xs) xs) = butlast xs"
by(simp add:splitAt_conv takeWhile_not_last)
subsubsection {* Sets *}
lemma splitAtRec_union:
"!! a b s. (a,b) = splitAtRec ram s vs ==> (set a ∪ set b) - {ram} = (set vs ∪ set s) - {ram}"
apply (induct vs) by (auto split: split_if_asm)
lemma splitAt_union:
"(a,b) = splitAt ram vs ==> (set a ∪ set b) - {ram} = set vs - {ram}"
by (simp add: splitAt_def splitAtRec_union)
lemma splitAt_subset_ab:
"(a,b) = splitAt ram vs ==> set a ⊆ set vs ∧ set b ⊆ set vs"
apply (cases "ram ∈ set vs")
by (auto dest: splitAt_split simp: splitAt_no_ram)
lemma splitAt_subset_fst:
"set (fst (splitAt ram vs)) ⊆ set vs"
proof -
def a: a ≡ "fst (splitAt ram vs)"
def b: b ≡ "snd (splitAt ram vs)"
with a have "(a,b) = splitAt ram vs" by auto
with a show ?thesis by (auto dest: splitAt_subset_ab)
qed
lemma splitAt_subset_snd:
"set (snd (splitAt ram vs)) ⊆ set vs"
proof -
def a: a ≡ "fst (splitAt ram vs)"
def b: b ≡ "snd (splitAt ram vs)"
with a have "(a,b) = splitAt ram vs" by auto
with b show ?thesis by (auto dest: splitAt_subset_ab)
qed
lemma splitAt_in_fst[dest]: "v ∈ set (fst (splitAt ram vs)) ==> v ∈ set vs"
proof (cases "ram ∈ set vs")
assume v: "v ∈ set (fst (splitAt ram vs))"
def a ≡ "fst (splitAt ram vs)"
with v have vin: "v ∈ set a" by auto
def b ≡ "snd (splitAt ram vs)"
case True with a_def b_def have "vs = a @ ram # b" by (auto dest: splitAt_ram)
with vin show "v ∈ set vs" by auto
next
assume v: "v ∈ set (fst (splitAt ram vs))"
case False with v show ?thesis by (auto dest: splitAt_no_ram del: notI)
qed
lemma splitAt_not1:
"v ∉ set vs ==> v ∉ set (fst (splitAt ram vs))" by (auto dest: splitAt_in_fst)
lemma splitAt_in_snd[dest]: "v ∈ set (snd (splitAt ram vs)) ==> v ∈ set vs"
proof (cases "ram ∈ set vs")
assume v: "v ∈ set (snd (splitAt ram vs))"
def a ≡ "fst (splitAt ram vs)"
def b ≡ "snd (splitAt ram vs)"
with v have vin: "v ∈ set b" by auto
case True with a_def b_def have "vs = a @ ram # b" by (auto dest: splitAt_ram)
with vin show "v ∈ set vs" by auto
next
assume v: "v ∈ set (snd (splitAt ram vs))"
case False with v show ?thesis by (auto dest: splitAt_no_ram del: notI)
qed
subsubsection {* Distinctness *}
lemma splitAt_distinct_ab:
"distinct vs ==> (a,b) = splitAt ram vs ==> distinct a ∧ distinct b"
apply (cases "ram ∈ set vs") by (auto dest: splitAt_split simp: splitAt_no_ram)
lemma splitAt_distinct_a:
"distinct vs ==> (a,b) = splitAt ram vs ==> distinct a"
apply (cases "ram ∈ set vs") by (auto dest: splitAt_split simp: splitAt_no_ram)
lemma splitAt_distinct_b:
"distinct vs ==> (a,b) = splitAt ram vs ==> distinct b"
apply (cases "ram ∈ set vs") by (auto dest: splitAt_split simp: splitAt_no_ram)
lemma splitAt_distinct_fst[intro]:
"distinct vs ==> distinct (fst (splitAt ram vs))"
proof -
assume d: "distinct vs"
def b: b ≡ "snd (splitAt ram vs)"
def a: a ≡ "fst (splitAt ram vs)"
with b have "(a,b) = splitAt ram vs" by auto
with a d show ?thesis by (auto dest: splitAt_distinct_ab)
qed
lemma splitAt_distinct_snd[intro]:
"distinct vs ==> distinct (snd (splitAt ram vs))"
proof -
assume d: "distinct vs"
def b: b ≡ "snd (splitAt ram vs)"
def a: a ≡ "fst (splitAt ram vs)"
with b have "(a,b) = splitAt ram vs" by auto
with b d show ?thesis by (auto dest: splitAt_distinct_ab)
qed
lemma splitAt_distinct_ab:
"distinct vs ==> (a,b) = splitAt ram vs ==> set a ∩ set b = {}"
apply (cases "ram ∈ set vs") apply (drule_tac splitAt_split)
by (auto simp: splitAt_no_ram)
lemma splitAt_distinct_fst_snd:
"distinct vs ==> set (fst (splitAt ram vs)) ∩ set (snd (splitAt ram vs)) = {}"
by (rule_tac splitAt_distinct_ab) simp_all
lemma splitAt_distinct_ram_fst[intro]:
"distinct vs ==> ram ∉ set (fst (splitAt ram vs))"
apply (case_tac "ram ∈ set vs") apply (drule_tac splitAt_ram)
apply (rule distinct_split1) by (force dest: splitAt_in_fst)+
(* apply (frule splitAt_no_ram) by auto *)
lemma splitAt_distinct_ram_snd[intro]:
"distinct vs ==> ram ∉ set (snd (splitAt ram vs))"
apply (case_tac "ram ∈ set vs") apply (drule_tac splitAt_ram)
apply (rule distinct_split2) by (force dest: splitAt_in_fst)+
lemma splitAt_1[simp]:
"splitAt ram [] = ([],[])" by (simp add: splitAt_def)
lemma splitAt_2:
"v ∈ set vs ==> (a,b) = splitAt ram vs ==> v ∈ set a ∨ v ∈ set b ∨ v = ram "
apply (cases "ram ∈ set vs")
by (auto dest: splitAt_split simp: splitAt_no_ram)
lemma splitAt_or:
"v ∈ set vs ==> v ∈ set (fst (splitAt ram vs)) ∨ v ∈ set (snd (splitAt ram vs)) ∨ v = ram"
by (rule splitAt_2) auto
lemma splitAt_distinct_fst: "distinct vs ==> distinct (fst (splitAt ram1 vs))"
by (simp add: splitAt_def splitAtRec_distinct_fst)
lemma splitAt_distinct_a: "distinct vs ==> (a,b) = splitAt ram vs ==> distinct a"
by (auto dest: splitAt_distinct_fst pairD)
lemma splitAt_distinct_snd: "distinct vs ==> distinct (snd (splitAt ram1 vs))"
by (simp add: splitAt_def splitAtRec_distinct_snd)
lemma splitAt_distinct_b: "distinct vs ==> (a,b) = splitAt ram vs ==> distinct b"
by (auto dest: splitAt_distinct_snd pairD)
lemma splitAt_distinct: "distinct vs ==> set (fst (splitAt ram vs)) ∩ set (snd (splitAt ram vs)) = {}"
by (simp add: splitAt_def splitAtRec_distinct)
lemma splitAt_subset: "(a,b) = splitAt ram vs ==> (set a ⊆ set vs) ∧ (set b ⊆ set vs)"
apply (cases "ram ∈ set vs") by (auto dest: splitAt_split simp: splitAt_no_ram)
lemma splitAt_subset1: "(a,b) = splitAt ram vs ==> (set a ⊆ set vs)"
by (auto dest: splitAt_subset)
lemma splitAt_subset2: "(a,b) = splitAt ram vs ==> (set b ⊆ set vs)"
by (auto dest: splitAt_subset)
subsubsection {* @{const splitAt} composition *}
lemma set_help: "v ∈ set ( as @ bs) ==> v ∈ set as ∨ v ∈ set bs" by auto
lemma splitAt_elements: "ram1 ∈ set vs ==> ram2 ∈ set vs ==> ram2 ∈ set( fst (splitAt ram1 vs)) ∨ ram2 ∈ set [ram1] ∨ ram2 ∈ set( snd (splitAt ram1 vs))"
proof -
assume r1: "ram1 ∈ set vs" and r2: "ram2 ∈ set vs"
then have "ram2 ∈ set( fst (splitAt ram1 vs) @ [ram1]) ∨ ram2 ∈ set( snd (splitAt ram1 vs))"
apply (rule_tac set_help)
apply (drule_tac splitAt_ram) by auto
then show ?thesis by auto
qed
lemma splitAt_ram2: "ram2 ∉ set (snd (splitAt ram1 vs)) ==>
ram1 ∈ set vs ==> ram2 ∈ set vs ==> ram1 ≠ ram2 ==>
ram2 ∈ set (fst (splitAt ram1 vs))" by (auto dest: splitAt_elements)
lemma splitAt_ram3: "ram2 ∉ set (fst (splitAt ram1 vs)) ==>
ram1 ∈ set vs ==> ram2 ∈ set vs ==> ram1 ≠ ram2 ==>
ram2 ∈ set (snd (splitAt ram1 vs))" by (auto dest: splitAt_elements)
lemma splitAt_dist_ram: "distinct vs ==>
vs = a @ ram # b ==> (a,b) = splitAt ram vs"
proof -
assume dist: "distinct vs" and vs: "vs = a @ ram # b"
from vs have r:"ram ∈ set vs" by auto
with dist vs have "fst (splitAt ram vs) = a" apply (drule_tac splitAt_ram) by (rule_tac dist_at1) auto
then have first:"a = fst (splitAt ram vs)" by auto
from r dist have second: "b = snd (splitAt ram vs)" apply (drule_tac splitAt_ram) apply (rule dist_at2) apply simp
by (auto simp: vs)
show ?thesis by (auto simp: first second)
qed
lemma distinct_unique1: "distinct vs ==> ram ∈ set vs ==> EX! s. vs = (fst s) @ ram # (snd s)"
proof
assume d: "distinct vs" and r: "ram ∈ set vs"
def s ≡ "splitAt ram vs" with r show "vs = (fst s) @ ram # (snd s)"
by (auto intro: splitAt_ram)
next
fix s
assume d: "distinct vs" and vs1: "vs = fst s @ ram # snd s"
from d vs1 show "s = splitAt ram vs" apply (drule_tac splitAt_dist_ram) apply simp by simp
qed
lemma splitAt_dist_ram2: "distinct vs ==> vs = a @ ram1 # b @ ram2 # c ==>
(a @ ram1 # b, c) = splitAt ram2 vs"
by (auto intro: splitAt_dist_ram)
lemma splitAt_dist_ram20: "distinct vs ==> vs = a @ ram1 # b @ ram2 # c ==>
c = snd (splitAt ram2 vs)"
proof -
assume dist: "distinct vs" and vs: "vs = a @ ram1 # b @ ram2 # c"
then show "c = snd (splitAt ram2 vs)" apply (drule_tac splitAt_dist_ram2) by (auto dest: pairD)
qed
lemma splitAt_dist_ram21: "distinct vs ==> vs = a @ ram1 # b @ ram2 # c ==> (a, b) = splitAt ram1 (fst (splitAt ram2 vs))"
proof -
assume dist: "distinct vs" and vs: "vs = a @ ram1 # b @ ram2 # c"
then have "fst (splitAt ram2 vs) = a @ ram1 # b" apply (drule_tac splitAt_dist_ram2) by (auto dest: pairD)
with dist vs show ?thesis by (rule_tac splitAt_dist_ram) auto
qed
lemma splitAt_dist_ram22: "distinct vs ==> vs = a @ ram1 # b @ ram2 # c ==> (c, []) = splitAt ram1 (snd (splitAt ram2 vs))"
proof -
assume dist: "distinct vs" and vs: "vs = a @ ram1 # b @ ram2 # c"
then have "snd (splitAt ram2 vs) = c" apply (drule_tac splitAt_dist_ram2) by (auto dest: pairD)
with dist vs have "splitAt ram1 (snd (splitAt ram2 vs)) = (c, [])" by (auto intro: splitAt_no_ram)
then show ?thesis by auto
qed
lemma splitAt_dist_ram1: "distinct vs ==> vs = a @ ram1 # b @ ram2 # c ==> (a, b @ ram2 # c) = splitAt ram1 vs"
by (auto intro: splitAt_dist_ram)
lemma splitAt_dist_ram10: "distinct vs ==> vs = a @ ram1 # b @ ram2 # c ==> a = fst (splitAt ram1 vs)"
proof -
assume dist: "distinct vs" and vs: "vs = a @ ram1 # b @ ram2 # c"
then show "a = fst (splitAt ram1 vs)" apply (drule_tac splitAt_dist_ram1) by (auto dest: pairD)
qed
lemma splitAt_dist_ram11: "distinct vs ==> vs = a @ ram1 # b @ ram2 # c ==> (a, []) = splitAt ram2 (fst (splitAt ram1 vs))"
proof -
assume dist: "distinct vs" and vs: "vs = a @ ram1 # b @ ram2 # c"
then have "fst (splitAt ram1 vs) = a" apply (drule_tac splitAt_dist_ram1) by (auto dest: pairD)
with dist vs have "splitAt ram2 (fst (splitAt ram1 vs)) = (a, [])" by (auto intro: splitAt_no_ram)
then show ?thesis by auto
qed
lemma splitAt_dist_ram12: "distinct vs ==> vs = a @ ram1 # b @ ram2 # c ==> (b, c) = splitAt ram2 (snd (splitAt ram1 vs))"
proof -
assume dist: "distinct vs" and vs: "vs = a @ ram1 # b @ ram2 # c"
then have "snd (splitAt ram1 vs) = b @ ram2 # c" apply (drule_tac splitAt_dist_ram1) by (auto dest: pairD)
with dist vs show ?thesis by (rule_tac splitAt_dist_ram) auto
qed
lemma splitAt_dist_ram_all:
"distinct vs ==> vs = a @ ram1 # b @ ram2 # c
==> (a, b) = splitAt ram1 (fst (splitAt ram2 vs))
∧ (c, []) = splitAt ram1 (snd (splitAt ram2 vs))
∧ (a, []) = splitAt ram2 (fst (splitAt ram1 vs))
∧ (b, c) = splitAt ram2 (snd (splitAt ram1 vs))
∧ c = snd (splitAt ram2 vs)
∧ a = fst (splitAt ram1 vs)"
apply (rule_tac conjI) apply (rule_tac splitAt_dist_ram21) apply simp apply simp
apply (rule_tac conjI) apply (rule_tac splitAt_dist_ram22) apply simp apply simp
apply (rule_tac conjI) apply (rule_tac splitAt_dist_ram11 splitAt_dist_ram22) apply simp apply simp
apply (rule_tac conjI) apply (rule_tac splitAt_dist_ram12)apply simp apply simp
apply (rule_tac conjI) apply (rule_tac splitAt_dist_ram20) apply simp apply simp
by (rule_tac splitAt_dist_ram10) auto
subsubsection {* Mixed *}
lemma fst_splitAt_rev:
"distinct xs ==> x ∈ set xs ==>
fst(splitAt x (rev xs)) = rev(snd(splitAt x xs))"
by(simp add:splitAt_conv takeWhile_neq_rev)
lemma snd_splitAt_rev:
"distinct xs ==> x ∈ set xs ==>
snd(splitAt x (rev xs)) = rev(fst(splitAt x xs))"
by(simp add:splitAt_conv dropWhile_neq_rev)
lemma splitAt_take[simp]: "distinct ls ==> i < length ls ==> fst (splitAt (ls!i) ls) = take i ls"
proof -
assume d: "distinct ls" and si: "i < length ls"
then have ls1: "ls = take i ls @ ls!i # drop (Suc i) ls" by (rule_tac id_take_nth_drop)
from si have "ls!i ∈ set ls" by auto
then have ls2: "ls = fst (splitAt (ls!i) ls) @ ls!i # snd (splitAt (ls!i) ls)" by (auto dest: splitAt_ram)
from d ls2 ls1 have "fst (splitAt (ls!i) ls) = take i ls ∧ snd (splitAt (ls!i) ls) = drop (Suc i) ls" by (rule dist_at)
then show ?thesis by auto
qed
lemma splitAt_drop[simp]: "distinct ls ==> i < length ls ==> snd (splitAt (ls!i) ls) = drop (Suc i) ls"
proof -
assume d: "distinct ls" and si: "i < length ls"
then have ls1: "ls = take i ls @ ls!i # drop (Suc i) ls" by (rule_tac id_take_nth_drop)
from si have "ls!i ∈ set ls" by auto
then have ls2: "ls = fst (splitAt (ls!i) ls) @ ls!i # snd (splitAt (ls!i) ls)" by (auto dest: splitAt_ram)
from d ls2 ls1 have "fst (splitAt (ls!i) ls) = take i ls ∧ snd (splitAt (ls!i) ls) = drop (Suc i) ls" by (rule dist_at)
then show ?thesis by auto
qed
lemma fst_splitAt_upt:
"j <= i ==> i < k ==> fst(splitAt i [j..<k]) = [j..<i]"
using splitAt_take[where ls = "[j..<k]" and i="i-j"]
apply (simp del:splitAt_take) apply arith
done
lemma snd_splitAt_upt:
"j <= i ==> i < k ==> snd(splitAt i [j..<k]) = [i+1..<k]"
using splitAt_drop[where ls = "[j..<k]" and i="i-j"]
apply (simp del:splitAt_drop) apply arith
done
lemma local_help1: "!! a vs. vs = c @ r # d ==> vs = a @ r # b ==> r ∉ set a ==> r ∉ set b ==> a = c"
proof (induct c)
case Nil
then have ra: "r ∉ set a" and vs1: "vs = a @ r # b" and vs2: "vs = [] @ r # d"
by auto
from vs1 vs2 have "a @ r # b = r # d" by auto
then have "hd (a @ r # b) = r" by auto
then have "a ≠ [] ==> hd a = r" by auto
then have "a ≠ [] ==> r ∈ set a" by (induct a) auto
with ra have a: "a = []" by auto
then show ?case by auto
next
case (Cons x xs) then show ?case by (induct a) auto
qed
lemma local_help: "vs = a @ r # b ==> vs = c @ r # d ==> r ∉ set a ==> r ∉ set b ==> a = c ∧ b = d"
proof -
assume dist: "r ∉ set a" "r ∉ set b" and vs1: "vs = a @ r # b" and vs2: "vs = c @ r # d"
then have "a = c" apply (rule_tac local_help1) .
with dist vs1 vs2 show ?thesis by simp
qed
lemma local_help': "a @ r # b = c @ r # d ==> r ∉ set a ==> r ∉ set b ==> a = c ∧ b = d"
by (rule local_help) auto
lemma splitAt_simp1: "ram ∉ set a ==> ram ∉ set b ==> fst (splitAt ram (a @ ram # b)) = a "
proof -
assume ramab: "ram ∉ set a" "ram ∉ set b"
def vs ≡ "a @ ram # b"
then have vs: "vs = a @ ram # b" by auto
then have "ram ∈ set vs" by auto
then have "vs = fst (splitAt ram vs) @ ram # snd (splitAt ram vs)" by (auto dest: splitAt_ram)
with vs ramab show ?thesis apply simp apply (rule_tac sym) apply (rule_tac local_help1) apply simp
apply (rule sym) apply assumption by auto
qed
lemma splitAt_simp2: "ram ∉ set b ==> fst (splitAt ram (ram # b)) = [] "
apply (subgoal_tac " fst (splitAt ram ([] @ ram # b)) = []") apply force
apply (rule splitAt_simp1) by auto
lemma splitAt_simp3: "ram ∉ set a ==> fst (splitAt ram (a @ [ram])) = a "
apply (subgoal_tac " fst (splitAt ram (a @ ram # [])) = a") apply force
apply (rule splitAt_simp1) by auto
lemma splitAt_simp4: "ram ∉ set a ==> ram ∉ set b ==> snd (splitAt ram (a @ ram # b)) = b "
proof -
assume ramab: "ram ∉ set a" "ram ∉ set b"
def vs ≡ "a @ ram # b"
then have vs: "vs = a @ ram # b" by auto
then have "ram ∈ set vs" by auto
then have "vs = fst (splitAt ram vs) @ ram # snd (splitAt ram vs)" by (auto dest: splitAt_ram)
with vs ramab show ?thesis by (simp add: splitAt_simp1)
qed
lemma help'''_in: "!! xs. ram ∈ set b ==> fst (splitAtRec ram xs b) = xs @ fst (splitAtRec ram [] b)"
proof (induct b)
case Nil then show ?case by auto
next
case (Cons b bs) show ?case using Cons(2)
apply (case_tac "b = ram") apply simp
apply simp
apply (subgoal_tac "fst (splitAtRec ram (xs @ [b]) bs) = (xs@[b]) @ fst (splitAtRec ram [] bs)") apply simp
apply (subgoal_tac "fst (splitAtRec ram [b] bs) = [b] @ fst (splitAtRec ram [] bs)") apply simp
apply (rule Cons) apply force
apply (rule Cons) by force
qed
lemma help'''_notin: "!! xs. ram ∉ set b ==> fst (splitAtRec ram xs b) = xs @ fst (splitAtRec ram [] b)"
proof (induct b)
case Nil then show ?case by auto
next
case (Cons b bs)
then have "ram ∉ set bs" by auto
then show ?case
apply (case_tac "b = ram") apply simp
apply simp
apply (subgoal_tac "fst (splitAtRec ram (xs @ [b]) bs) = (xs@[b]) @ fst (splitAtRec ram [] bs)") apply simp
apply (subgoal_tac "fst (splitAtRec ram [b] bs) = [b] @ fst (splitAtRec ram [] bs)") apply simp
apply (rule Cons) apply simp
apply (rule Cons) by simp
qed
lemma help''': "fst (splitAtRec ram xs b) = xs @ fst (splitAtRec ram [] b)"
apply (cases "ram ∈ set b")
apply (rule_tac help'''_in) apply simp
apply (rule_tac help'''_notin) apply simp done
lemma splitAt_simpA[simp]: "fst (splitAt ram (ram # b)) = []" by (simp add: splitAt_def)
lemma splitAt_simpB[simp]: "ram ≠ a ==> fst (splitAt ram (a # b)) = a # fst (splitAt ram b)" apply (simp add: splitAt_def)
apply (subgoal_tac "fst (splitAtRec ram [a] b) = [a] @ fst (splitAtRec ram [] b)") apply simp by (rule help''')
lemma splitAt_simpB'[simp]: "a ≠ ram ==> fst (splitAt ram (a # b)) = a # fst (splitAt ram b)" apply (rule splitAt_simpB) by auto
lemma splitAt_simpC[simp]: "ram ∉ set a ==> fst (splitAt ram (a @ b)) = a @ fst (splitAt ram b)"
apply (induct a) by auto
lemma help'''': "!! xs ys. snd (splitAtRec ram xs b) = snd (splitAtRec ram ys b)"
apply (induct b) by auto
lemma splitAt_simpD[simp]: "!! a. ram ≠ a ==> snd (splitAt ram (a # b)) = snd (splitAt ram b)" apply (simp add: splitAt_def)
by (rule help'''')
lemma splitAt_simpD'[simp]: "!! a. a ≠ ram ==> snd (splitAt ram (a # b)) = snd (splitAt ram b)" apply (rule splitAt_simpD) by auto
lemma splitAt_simpE[simp]: "snd (splitAt ram (ram # b)) = b" by (simp add: splitAt_def)
lemma splitAt_simpF[simp]: "ram ∉ set a ==> snd (splitAt ram (a @ b)) = snd (splitAt ram b) "
apply (induct a) by auto
lemma splitAt_rotate_pair_conv:
"!!xs. [| distinct xs; x ∈ set xs |]
==> snd (splitAt x (rotate n xs)) @ fst (splitAt x (rotate n xs)) =
snd (splitAt x xs) @ fst (splitAt x xs)"
apply(induct n) apply simp
apply(simp del:rotate_Suc2 add:rotate1_rotate_swap)
apply(clarsimp simp add:rotate1_def split:list.split)
apply(erule disjE) apply simp
apply(drule split_list)
apply clarsimp
done
subsection {* @{text between} *}
constdefs between :: "'a list => 'a => 'a => 'a list"
"between vs ram1 ram2 ≡
let (pre1, post1) = splitAt ram1 vs in
if ram2 mem post1
then let (pre2, post2) = splitAt ram2 post1 in pre2
else let (pre2, post2) = splitAt ram2 pre1 in post1 @ pre2"
lemma inbetween_inset:
"x ∈ set(between xs a b) ==> x ∈ set xs"
apply(simp add:between_def split_def split:split_if_asm)
apply(blast dest:splitAt_in_snd)
apply(blast dest:splitAt_in_snd)
done
lemma notinset_notinbetween:
"x ∉ set xs ==> x ∉ set(between xs a b)"
by(blast dest:inbetween_inset)
lemma set_between_id:
"distinct xs ==> x ∈ set xs ==>
set(between xs x x) = set xs - {x}"
apply(drule split_list)
apply (clarsimp simp:between_def split_def Un_commute)
done
lemma split_between:
"[| distinct vs; r ∈ set vs; v ∈ set vs; u ∈ set(between vs r v) |] ==>
between vs r v =
(if r=u then [] else between vs r u @ [u]) @ between vs u v"
apply(cases "r = v")
apply(clarsimp)
apply(frule split_list[of v])
apply(clarsimp)
apply(simp add:between_def split_def split:split_if_asm)
apply(erule disjE)
apply(frule split_list[of u])
apply(clarsimp)
apply(frule split_list[of u])
apply(clarsimp)
apply(clarsimp)
apply(frule split_list[of r])
apply(clarsimp)
apply(rename_tac as bs)
apply(erule disjE)
apply(frule split_list[of v])
apply(clarsimp)
apply(rename_tac cs ds)
apply(subgoal_tac "between (cs @ v # ds @ r # bs) r v = bs @ cs")
prefer 2 apply(simp add:between_def split_def split:split_if_asm)
apply simp
apply(erule disjE)
apply(frule split_list[of u])
apply(clarsimp simp:between_def split_def split:split_if_asm)
apply(frule split_list[of u])
apply(clarsimp simp:between_def split_def split:split_if_asm)
apply(frule split_list[of v])
apply(clarsimp)
apply(rename_tac cs ds)
apply(subgoal_tac "between (as @ r # cs @ v # ds) r v = cs")
prefer 2 apply(simp add:between_def split_def split:split_if_asm)
apply simp
apply(frule split_list[of u])
apply(clarsimp simp:between_def split_def split:split_if_asm)
done
subsection {* Tables *}
types ('a, 'b) table = "('a × 'b) list"
constdefs isTable :: "('a => 'b) => 'a list => ('a, 'b) table => bool"
"isTable f vs t ≡ ∀p. p ∈ set t --> snd p = f (fst p) ∧ fst p ∈ set vs"
lemma isTable_eq: "isTable E vs ((a,b)#ps) ==> b = E a"
by (auto simp add: isTable_def)
lemma isTable_subset:
"set qs ⊆ set ps ==> isTable E vs ps ==> isTable E vs qs"
by (unfold isTable_def) auto
lemma isTable_Cons: "isTable E vs ((a,b)#ps) ==> isTable E vs ps"
by (unfold isTable_def) auto
constdefs
removeKey :: "'a => ('a × 'b) list => ('a × 'b) list"
"removeKey a ps ≡ [p ∈ ps. a ≠ fst p]"
consts removeKeyList :: "'a list => ('a × 'b) list => ('a × 'b) list"
primrec
"removeKeyList [] ps = ps"
"removeKeyList (w#ws) ps = removeKey w (removeKeyList ws ps)"
lemma removeKey_subset[simp]: "set (removeKey a ps) ⊆ set ps"
by (simp add: removeKey_def) blast
lemma length_removeKey[simp]: "|removeKey w ps| ≤ |ps|"
by (simp add: removeKey_def)
lemma length_removeKeyList:
"length (removeKeyList ws ps) ≤ length ps" (is "?P ws")
proof (induct ws)
show "?P []" by simp
fix w ws
have "length (removeKey w (removeKeyList ws ps))
≤ length (removeKeyList ws ps)"
by (rule length_removeKey)
also assume "?P ws"
finally show "?P (w#ws)" by simp
qed
lemma removeKeyList_subset[simp]: "set (removeKeyList ws ps) ⊆ set ps"
proof (induct ws)
case Nil then show ?case by simp
next
case (Cons w ws)
have "set (removeKey w (removeKeyList ws ps)) ⊆ set (removeKeyList ws ps)"
by (rule removeKey_subset)
with Cons show ?case by (simp add: removeKey_def)
qed
lemma notin_removeKey1: "(a, b) ∉ set (removeKey a ps)"
by (induct ps) (auto simp add: removeKey_def)
lemma notin_removeKey: "r ∉ fst ` set (removeKey r ps)"
by (induct ps) (auto simp add: removeKey_def)
lemma notin_removeKeyList1:
"!!a. a ∈ set rs ==> (a, b) ∉ set (removeKeyList rs ps)"
proof (induct rs)
case Nil then show ?case by simp
next
case (Cons r rs) then show ?case
proof cases
assume "a = r" then show ?thesis
by (auto simp add: split_beta Let_def notin_removeKey1 removeKey_subset)
next
assume a: "a ≠ r"
with Cons have"(a, b) ∉ set (removeKeyList rs ps)" by simp
moreover have "set (removeKey r (removeKeyList rs ps))
⊆ set (removeKeyList rs ps)"
by (rule removeKey_subset) (* fixme : finally *)
ultimately have "(a, b) ∉ set (removeKey r (removeKeyList rs ps))"
by blast
then show ?thesis by simp
qed
qed
lemma notin_removeKeyList: "!!r. r ∈ set rs ==> r ∉ fst ` set (removeKeyList rs ps)"
proof (induct rs)
case Nil then show ?case by simp
next
case (Cons r' rs) then show ?case
by (auto simp add: notin_removeKey1 split_paired_all removeKey_def)
qed
lemma removeKeyList_eq:
"removeKeyList as ps = [p ∈ ps. ∀a ∈ set as. a ≠ fst p]"
by (induct as) (simp_all add: filter_comm removeKey_def)
lemma removeKey_empty[simp]: "removeKey a [] = []"
by (simp add: removeKey_def)
lemma removeKeyList_empty[simp]: "removeKeyList ps [] = []"
by (induct ps) simp_all
lemma removeKeyList_cons[simp]:
"removeKeyList ws (p#ps)
= (if fst p ∈ set ws then removeKeyList ws ps else p#(removeKeyList ws ps))"
by (induct ws) (simp_all split: split_if_asm add: removeKey_def)
end
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)