Quelle More_List.thy Sprache: Isabelle

(* Author: Andreas Lochbihler, ETH Zürich
   Author: Florian Haftmann, TU Muenchen  *)

section \<open>Less common functions on lists\<close>

theory More_List
imports Main
begin

definition strip_while :: "('a \ bool) \ 'a list \ 'a list"
where
  "strip_while P = rev \ dropWhile P \ rev"

lemma strip_while_rev [simp]:
  "strip_while P (rev xs) = rev (dropWhile P xs)"
  by (simp add: strip_while_def)

lemma strip_while_Nil [simp]:
  "strip_while P [] = []"
  by (simp add: strip_while_def)

lemma strip_while_append [simp]:
  "\ P x \ strip_while P (xs @ [x]) = xs @ [x]"
  by (simp add: strip_while_def)

lemma strip_while_append_rec [simp]:
  "P x \ strip_while P (xs @ [x]) = strip_while P xs"
  by (simp add: strip_while_def)

lemma strip_while_Cons [simp]:
  "\ P x \ strip_while P (x # xs) = x # strip_while P xs"
  by (induct xs rule: rev_induct) (simp_all add: strip_while_def)

lemma strip_while_eq_Nil [simp]:
  "strip_while P xs = [] \ (\x\set xs. P x)"
  by (simp add: strip_while_def)

lemma strip_while_eq_Cons_rec:
  "strip_while P (x # xs) = x # strip_while P xs \ \ (P x \ (\x\set xs. P x))"
  by (induct xs rule: rev_induct) (simp_all add: strip_while_def)

lemma split_strip_while_append:
  fixes xs :: "'a list"
  obtains ys zs :: "'a list"
  where "strip_while P xs = ys" and "\x\set zs. P x" and "xs = ys @ zs"
proof (rule that)
  show "strip_while P xs = strip_while P xs" ..
  show "\x\set (rev (takeWhile P (rev xs))). P x" by (simp add: takeWhile_eq_all_conv [symmetric])
  have "rev xs = rev (strip_while P xs @ rev (takeWhile P (rev xs)))"
    by (simp add: strip_while_def)
  then show "xs = strip_while P xs @ rev (takeWhile P (rev xs))"
    by (simp only: rev_is_rev_conv)
qed

lemma strip_while_snoc [simp]:
  "strip_while P (xs @ [x]) = (if P x then strip_while P xs else xs @ [x])"
  by (simp add: strip_while_def)

lemma strip_while_map:
  "strip_while P (map f xs) = map f (strip_while (P \ f) xs)"
  by (simp add: strip_while_def rev_map dropWhile_map)

lemma strip_while_dropWhile_commute:
  "strip_while P (dropWhile Q xs) = dropWhile Q (strip_while P xs)"
proof (induct xs)
  case Nil
  then show ?case
    by simp
next
  case (Cons x xs)
  show ?case
  proof (cases "\y\set xs. P y")
    case True
    with dropWhile_append2 [of "rev xs"] show ?thesis
      by (auto simp add: strip_while_def dest: set_dropWhileD)
  next
    case False
    then obtain y where "y \ set xs" and "\ P y"
      by blast
    with Cons dropWhile_append3 [of P y "rev xs"] show ?thesis
      by (simp add: strip_while_def)
  qed
qed

lemma dropWhile_strip_while_commute:
  "dropWhile P (strip_while Q xs) = strip_while Q (dropWhile P xs)"
  by (simp add: strip_while_dropWhile_commute)

definition no_leading :: "('a \ bool) \ 'a list \ bool"
where
  "no_leading P xs \ (xs \ [] \ \ P (hd xs))"

lemma no_leading_Nil [iff]:
  "no_leading P []"
  by (simp add: no_leading_def)

lemma no_leading_Cons [iff]:
  "no_leading P (x # xs) \ \ P x"
  by (simp add: no_leading_def)

lemma no_leading_append [simp]:
  "no_leading P (xs @ ys) \ no_leading P xs \ (xs = [] \ no_leading P ys)"
  by (induct xs) simp_all

lemma no_leading_dropWhile [simp]:
  "no_leading P (dropWhile P xs)"
  by (induct xs) simp_all

lemma dropWhile_eq_obtain_leading:
  assumes "dropWhile P xs = ys"
  obtains zs where "xs = zs @ ys" and "\z. z \ set zs \ P z" and "no_leading P ys"
proof -
  from assms have "\zs. xs = zs @ ys \ (\z \ set zs. P z) \ no_leading P ys"
  proof (induct xs arbitrary: ys)
    case Nil then show ?case by simp
  next
    case (Cons x xs ys)
    show ?case proof (cases "P x")
      case True with Cons.hyps [of ys] Cons.prems
      have "\zs. xs = zs @ ys \ (\a\set zs. P a) \ no_leading P ys"
        by simp
      then obtain zs where "xs = zs @ ys" and "\z. z \ set zs \ P z"
        and *: "no_leading P ys"
        by blast
      with True have "x # xs = (x # zs) @ ys" and "\z. z \ set (x # zs) \ P z"
        by auto
      with * show ?thesis
        by blast    next
      case False
      with Cons show ?thesis by (cases ys) simp_all
    qed
  qed
  with that show thesis
    by blast
qed

lemma dropWhile_idem_iff:
  "dropWhile P xs = xs \ no_leading P xs"
  by (cases xs) (auto elim: dropWhile_eq_obtain_leading)

abbreviation no_trailing :: "('a \ bool) \ 'a list \ bool"
where
  "no_trailing P xs \ no_leading P (rev xs)"

lemma no_trailing_unfold:
  "no_trailing P xs \ (xs \ [] \ \ P (last xs))"
  by (induct xs) simp_all

lemma no_trailing_Nil [iff]:
  "no_trailing P []"
  by simp

lemma no_trailing_Cons [simp]:
  "no_trailing P (x # xs) \ no_trailing P xs \ (xs = [] \ \ P x)"
  by simp

lemma no_trailing_append:
  "no_trailing P (xs @ ys) \ no_trailing P ys \ (ys = [] \ no_trailing P xs)"
  by (induct xs) simp_all

lemma no_trailing_append_Cons [simp]:
  "no_trailing P (xs @ y # ys) \ no_trailing P (y # ys)"
  by simp

lemma no_trailing_strip_while [simp]:
  "no_trailing P (strip_while P xs)"
  by (induct xs rule: rev_induct) simp_all

lemma strip_while_idem [simp]:
  "no_trailing P xs \ strip_while P xs = xs"
  by (cases xs rule: rev_cases) simp_all

lemma strip_while_eq_obtain_trailing:
  assumes "strip_while P xs = ys"
  obtains zs where "xs = ys @ zs" and "\z. z \ set zs \ P z" and "no_trailing P ys"
proof -
  from assms have "rev (rev (dropWhile P (rev xs))) = rev ys"
    by (simp add: strip_while_def)
  then have "dropWhile P (rev xs) = rev ys"
    by simp
  then obtain zs where A: "rev xs = zs @ rev ys" and B: "\z. z \ set zs \ P z"
    and C: "no_trailing P ys"
    using dropWhile_eq_obtain_leading by blast
  from A have "rev (rev xs) = rev (zs @ rev ys)"
    by simp
  then have "xs = ys @ rev zs"
    by simp
  moreover from B have "\z. z \ set (rev zs) \ P z"
    by simp
  ultimately show thesis using that C by blast
qed

lemma strip_while_idem_iff:
  "strip_while P xs = xs \ no_trailing P xs"
proof -
  define ys where "ys = rev xs"
  moreover have "strip_while P (rev ys) = rev ys \ no_trailing P (rev ys)"
    by (simp add: dropWhile_idem_iff)
  ultimately show ?thesis by simp
qed

lemma no_trailing_map:
  "no_trailing P (map f xs) \ no_trailing (P \ f) xs"
  by (simp add: last_map no_trailing_unfold)

lemma no_trailing_drop [simp]:
  "no_trailing P (drop n xs)" if "no_trailing P xs"
proof -
  from that have "no_trailing P (take n xs @ drop n xs)"
    by simp
  then show ?thesis
    by (simp only: no_trailing_append)
qed

lemma no_trailing_upt [simp]:
  "no_trailing P [n.. (n < m \ \ P (m - 1))"
  by (auto simp add: no_trailing_unfold)

definition nth_default :: "'a \ 'a list \ nat \ 'a"
where
  "nth_default dflt xs n = (if n < length xs then xs ! n else dflt)"

lemma nth_default_nth:
  "n < length xs \ nth_default dflt xs n = xs ! n"
  by (simp add: nth_default_def)

lemma nth_default_beyond:
  "length xs \ n \ nth_default dflt xs n = dflt"
  by (simp add: nth_default_def)

lemma nth_default_Nil [simp]:
  "nth_default dflt [] n = dflt"
  by (simp add: nth_default_def)

lemma nth_default_Cons:
  "nth_default dflt (x # xs) n = (case n of 0 \ x | Suc n' \ nth_default dflt xs n')"
  by (simp add: nth_default_def split: nat.split)

lemma nth_default_Cons_0 [simp]:
  "nth_default dflt (x # xs) 0 = x"
  by (simp add: nth_default_Cons)

lemma nth_default_Cons_Suc [simp]:
  "nth_default dflt (x # xs) (Suc n) = nth_default dflt xs n"
  by (simp add: nth_default_Cons)

lemma nth_default_replicate_dflt [simp]:
  "nth_default dflt (replicate n dflt) m = dflt"
  by (simp add: nth_default_def)

lemma nth_default_append:
  "nth_default dflt (xs @ ys) n =
    (if n < length xs then nth xs n else nth_default dflt ys (n - length xs))"
  by (auto simp add: nth_default_def nth_append)

lemma nth_default_append_trailing [simp]:
  "nth_default dflt (xs @ replicate n dflt) = nth_default dflt xs"
  by (simp add: fun_eq_iff nth_default_append) (simp add: nth_default_def)

lemma nth_default_snoc_default [simp]:
  "nth_default dflt (xs @ [dflt]) = nth_default dflt xs"
  by (auto simp add: nth_default_def fun_eq_iff nth_append)

lemma nth_default_eq_dflt_iff:
  "nth_default dflt xs k = dflt \ (k < length xs \ xs ! k = dflt)"
  by (simp add: nth_default_def)

lemma nth_default_take_eq:
  "nth_default dflt (take m xs) n =
    (if n < m then nth_default dflt xs n else dflt)"
  by (simp add: nth_default_def)

lemma in_enumerate_iff_nth_default_eq:
  "x \ dflt \ (n, x) \ set (enumerate 0 xs) \ nth_default dflt xs n = x"
  by (auto simp add: nth_default_def in_set_conv_nth enumerate_eq_zip)

lemma last_conv_nth_default:
  assumes "xs \ []"
  shows "last xs = nth_default dflt xs (length xs - 1)"
  using assms by (simp add: nth_default_def last_conv_nth)

lemma nth_default_map_eq:
  "f dflt' = dflt \ nth_default dflt (map f xs) n = f (nth_default dflt' xs n)"
  by (simp add: nth_default_def)

lemma finite_nth_default_neq_default [simp]:
  "finite {k. nth_default dflt xs k \ dflt}"
  by (simp add: nth_default_def)

lemma sorted_list_of_set_nth_default:
  "sorted_list_of_set {k. nth_default dflt xs k \ dflt} = map fst (filter (\(_, x). x \ dflt) (enumerate 0 xs))"
  by (rule sorted_distinct_set_unique) (auto simp add: nth_default_def in_set_conv_nth
    sorted_filter distinct_map_filter enumerate_eq_zip intro: rev_image_eqI)

lemma map_nth_default:
  "map (nth_default x xs) [0..
proof -
  have *: "map (nth_default x xs) [0..
    by (rule map_cong) (simp_all add: nth_default_nth)
  show ?thesis by (simp add: * map_nth)
qed

lemma range_nth_default [simp]:
  "range (nth_default dflt xs) = insert dflt (set xs)"
  by (auto simp add: nth_default_def [abs_def] in_set_conv_nth)

lemma nth_strip_while:
  assumes "n < length (strip_while P xs)"
  shows "strip_while P xs ! n = xs ! n"
proof -
  have "length (dropWhile P (rev xs)) + length (takeWhile P (rev xs)) = length xs"
    by (subst add.commute)
      (simp add: arg_cong [where f=length, OF takeWhile_dropWhile_id, unfolded length_append])
  then show ?thesis using assms
    by (simp add: strip_while_def rev_nth dropWhile_nth)
qed

lemma length_strip_while_le:
  "length (strip_while P xs) \ length xs"
  unfolding strip_while_def o_def length_rev
  by (subst (2) length_rev[symmetric])
    (simp add: strip_while_def length_dropWhile_le del: length_rev)

lemma nth_default_strip_while_dflt [simp]:
  "nth_default dflt (strip_while ((=) dflt) xs) = nth_default dflt xs"
  by (induct xs rule: rev_induct) auto

lemma nth_default_eq_iff:
  "nth_default dflt xs = nth_default dflt ys
     \<longleftrightarrow> strip_while (HOL.eq dflt) xs = strip_while (HOL.eq dflt) ys" (is "?P \<longleftrightarrow> ?Q")
proof
  let ?strip_while = \<open>strip_while (HOL.eq dflt)\<close>
  let ?xs = "?strip_while xs"
  let ?ys = "?strip_while ys"
  assume ?P
  then have eq: "nth_default dflt ?xs = nth_default dflt ?ys"
    by simp
  have len: "length ?xs = length ?ys"
  proof (rule ccontr)
    assume neq: "\ ?thesis"
    { fix xs ys :: "'a list"
      let ?xs = "?strip_while xs"
      let ?ys = "?strip_while ys"
      assume eq: "nth_default dflt ?xs = nth_default dflt ?ys"
      assume len: "length ?xs < length ?ys"
      then have "length ?ys > 0" by arith
      then have "?ys \ []" by simp
      with last_conv_nth_default [of ?ys dflt]
      have "last ?ys = nth_default dflt ?ys (length ?ys - 1)"
        by auto
      moreover from \<open>?ys \<noteq> []\<close> no_trailing_strip_while [of "HOL.eq dflt" ys]
        have "last ?ys \ dflt" by (simp add: no_trailing_unfold)
      ultimately have "nth_default dflt ?xs (length ?ys - 1) \ dflt"
        using eq by simp
      moreover from len have "length ?ys - 1 \ length ?xs" by simp
      ultimately have False by (simp only: nth_default_beyond) simp
    }
    from this [of xs ys] this [of ys xs] neq eq show False
      by (auto simp only: linorder_class.neq_iff)
  qed
  then show ?Q
  proof (rule nth_equalityI [rule_format])
    fix n
    assume n: "n < length ?xs"
    with len have "n < length ?ys"
      by simp
    with n have xs: "nth_default dflt ?xs n = ?xs ! n"
      and ys: "nth_default dflt ?ys n = ?ys ! n"
      by (simp_all only: nth_default_nth)
    with eq show "?xs ! n = ?ys ! n"
      by simp
  qed
next
  assume ?Q
  then have "nth_default dflt (strip_while (HOL.eq dflt) xs) = nth_default dflt (strip_while (HOL.eq dflt) ys)"
    by simp
  then show ?P
    by simp
qed

lemma nth_default_map2:
  \<open>nth_default d (map2 f xs ys) n = f (nth_default d1 xs n) (nth_default d2 ys n)\<close>
    if \<open>length xs = length ys\<close> and \<open>f d1 d2 = d\<close> for bs cs
using that proof (induction xs ys arbitrary: n rule: list_induct2)
  case Nil
  then show ?case
    by simp
next
  case (Cons x xs y ys)
  then show ?case
    by (cases n) simp_all
qed

end

quality100%

¤ Dauer der Verarbeitung: 0.1Bemerkung: (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.