Quelle NList.thy Sprache: Isabelle

(*  Author:     Tobias Nipkow
    Copyright   2000 TUM
*)

section \<open>Fixed Length Lists\<close>

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 \<open>These [simp] attributes are double-edged.
Many proofs in Jinja rely on it but they can degrade performance.\<close>

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

quality100%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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.