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" thenobtain 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" thenobtain n' where n: "n = Suc n'" "l \<in> A" and n': "ls@b \<in> 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" . thenobtain 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 moreoverassume"a@b \ nlists n A" "\n1 n2. n=n1+n2 \ a \ nlists n1 A \ b \ nlists n2 A \ P" ultimatelyshow ?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) \<and> xs \<in> nlists (length xs) A \<and> ys \<in> 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\<open>Link to an executable version on lists in List.\<close> lemma nlists_set[code]: "nlists n (set xs) = set(List.n_lists n xs)" by (metis nlists_def set_n_lists)
end
¤ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
