(* Author: Tobias Nipkow
Copyright 2000 TUM
*)
section ‹Fixed Length Lists
›
theory NList
imports Main
begin
definition nlists ::
"nat \ 'a set \ 'a list set"
where "nlists n A = {xs. size xs = n \ set xs \ A}"
lemma nlistsI:
"\ size xs = n; set xs \ A \ \ xs \ nlists n A"
by (simp add: nlists_def)
text ‹These [simp] attributes are double-edged.
Many proofs
in Jinja rely on it but they can degrade performance.
›
lemma nlistsE_length [simp]:
"xs \ nlists n A \ size xs = n"
by (simp add: nlists_def)
lemma in_nlists_UNIV:
"xs \ nlists k UNIV \ length xs = k"
unfolding nlists_def
by(auto)
lemma less_lengthI:
"\ xs \ nlists n A; p < n \ \ p < size xs"
by (simp)
lemma nlistsE_set[simp]:
"xs \ nlists n A \ set xs \ A"
unfolding nlists_def
by (simp)
lemma nlists_mono:
assumes "A \ B" shows "nlists n A \ nlists n B"
proof
fix xs
assume "xs \ nlists n A"
then obtain size:
"size xs = n" and inA:
"set xs \ A" by (simp)
with assms
have "set xs \ B" by simp
with size
show "xs \ nlists n B" by(clarsimp intro!: nlistsI)
qed
lemma nlists_singleton:
"nlists n {a} = {replicate n a}"
unfolding nlists_def
by(auto simp: replicate_length_same dest!: subset_singletonD)
lemma nlists_n_0 [simp]:
"nlists 0 A = {[]}"
unfolding nlists_def
by (auto)
lemma in_nlists_Suc_iff:
"(xs \ nlists (Suc n) A) = (\y\A. \ys \ nlists n A. xs = y#ys)"
unfolding nlists_def
by (cases
"xs") auto
lemma Cons_in_nlists_Suc [iff]:
"(x#xs \ nlists (Suc n) A) \ (x\A \ xs \ nlists n A)"
unfolding nlists_def
by (auto)
lemma nlists_Suc:
"nlists (Suc n) A = (\a\A. (#) a ` nlists n A)"
by(auto simp: set_eq_iff image_iff in_nlists_Suc_iff)
lemma nlists_not_empty:
"A\{} \ \xs. xs \ nlists n A"
by (induct
"n") (auto simp: in_nlists_Suc_iff)
lemma nlistsE_nth_in:
"\ xs \ nlists n A; i < n \ \ xs!i \ A"
unfolding nlists_def
by (auto)
lemma nlists_Cons_Suc [elim!]:
"l#xs \ nlists n A \ (\n'. n = Suc n' \ l \ A \ xs \ nlists n' A \ P) \ P"
unfolding nlists_def
by (auto)
lemma nlists_appendE [elim!]:
"a@b \ nlists n A \ (\n1 n2. n=n1+n2 \ a \ nlists n1 A \ b \ nlists n2 A \ P) \ P"
proof -
have "\n. a@b \ nlists n A \ \n1 n2. n=n1+n2 \ a \ nlists n1 A \ b \ nlists n2 A"
(
is "\n. ?list a n \ \n1 n2. ?P a n n1 n2")
proof (induct a)
fix n
assume "?list [] n"
hence "?P [] n 0 n" by simp
thus "\n1 n2. ?P [] n n1 n2" by fast
next
fix n l ls
assume "?list (l#ls) n"
then obtain n
' where n: "n = Suc n'" "l
∈ A
" and n': "ls@b
∈ nlists n
' A" by fastforce
assume "\n. ls @ b \ nlists n A \ \n1 n2. n = n1 + n2 \ ls \ nlists n1 A \ b \ nlists n2 A"
from this
and n
' have "\n1 n2. n' = n1 + n2
∧ ls
∈ nlists n1 A
∧ b
∈ nlists n2 A
" .
then obtain n1 n2
where "n' = n1 + n2" "ls \ nlists n1 A" "b \ nlists n2 A" by fast
with n
have "?P (l#ls) n (n1+1) n2" by simp
thus "\n1 n2. ?P (l#ls) n n1 n2" by fastforce
qed
moreover assume "a@b \ nlists n A" "\n1 n2. n=n1+n2 \ a \ nlists n1 A \ b \ nlists n2 A \ P"
ultimately show ?thesis
by blast
qed
lemma nlists_update_in_list [simp, intro!]:
"\ xs \ nlists n A; x\A \ \ xs[i := x] \ nlists n A"
by (metis length_list_update nlistsE_length nlistsE_set nlistsI set_update_subsetI)
lemma nlists_appendI [intro?]:
"\ a \ nlists n A; b \ nlists m A \ \ a @ b \ nlists (n+m) A"
unfolding nlists_def
by (auto)
lemma nlists_append:
"xs @ ys \ nlists k A \
k = length(xs @ ys)
∧ xs
∈ nlists (length xs) A
∧ ys
∈ nlists (length ys) A
"
unfolding nlists_def
by (auto)
lemma nlists_map [simp]:
"(map f xs \ nlists (size xs) A) = (f ` set xs \ A)"
unfolding nlists_def
by (auto)
lemma nlists_replicateI [intro]:
"x \ A \ replicate n x \ nlists n A"
by (induct n) auto
text ‹Link
to an executable version on lists
in List.
›
lemma nlists_set[code]:
"nlists n (set xs) = set(List.n_lists n xs)"
by (metis nlists_def set_n_lists)
end
