Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: List_Sublist.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Imperative_HOL/ex/List_Sublist.thy
    Author:     Lukas Bulwahn, TU Muenchen
*)

section \<open>Slices of lists\<close>

theory List_Sublist
imports "HOL-Library.Multiset"
begin

lemma nths_split: "i \ j \ j \ k \ nths xs {i..
apply (induct xs arbitrary: i j k)
apply simp
apply (simp only: nths_Cons)
apply simp
apply safe
apply simp
apply (erule_tac x="0" in meta_allE)
apply (erule_tac x="j - 1" in meta_allE)
apply (erule_tac x="k - 1" in meta_allE)
apply (subgoal_tac "0 \ j - 1 \ j - 1 \ k - 1")
apply simp
apply (subgoal_tac "{ja. Suc ja < j} = {0..)
apply (subgoal_tac "{ja. j \ Suc ja \ Suc ja < k} = {j - Suc 0..
apply (subgoal_tac "{j. Suc j < k} = {0..)
apply simp
apply fastforce
apply fastforce
apply fastforce
apply fastforce
apply (erule_tac x="i - 1" in meta_allE)
apply (erule_tac x="j - 1" in meta_allE)
apply (erule_tac x="k - 1" in meta_allE)
apply (subgoal_tac " {ja. i \ Suc ja \ Suc ja < j} = {i - 1 ..
apply (subgoal_tac " {ja. j \ Suc ja \ Suc ja < k} = {j - 1..
apply (subgoal_tac "{j. i \ Suc j \ Suc j < k} = {i - 1..
apply (subgoal_tac " i - 1 \ j - 1 \ j - 1 \ k - 1")
apply simp
apply fastforce
apply fastforce
apply fastforce
apply fastforce
done

lemma nths_update1: "i \ inds \ nths (xs[i := v]) inds = nths xs inds"
apply (induct xs arbitrary: i inds)
apply simp
apply (case_tac i)
apply (simp add: nths_Cons)
apply (simp add: nths_Cons)
done

lemma nths_update2: "i \ inds \ nths (xs[i := v]) inds = (nths xs inds)[(card {k \ inds. k < i}):= v]"
proof (induct xs arbitrary: i inds)
  case Nil thus ?case by simp
next
  case (Cons x xs)
  thus ?case
  proof (cases i)
    case 0 with Cons show ?thesis by (simp add: nths_Cons)
  next
    case (Suc i')
    with Cons show ?thesis
      apply simp
      apply (simp add: nths_Cons)
      apply auto
      apply (auto simp add: nat.split)
      apply (simp add: card_less_Suc[symmetric])
      apply (simp add: card_less_Suc2)
      done
  qed
qed

lemma nths_update: "nths (xs[i := v]) inds = (if i \ inds then (nths xs inds)[(card {k \ inds. k < i}) := v] else nths xs inds)"
by (simp add: nths_update1 nths_update2)

lemma nths_take: "nths xs {j. j < m} = take m xs"
apply (induct xs arbitrary: m)
apply simp
apply (case_tac m)
apply simp
apply (simp add: nths_Cons)
done

lemma nths_take': "nths xs {0..
apply (induct xs arbitrary: m)
apply simp
apply (case_tac m)
apply simp
apply (simp add: nths_Cons nths_take)
done

lemma nths_all[simp]: "nths xs {j. j < length xs} = xs"
apply (induct xs)
apply simp
apply (simp add: nths_Cons)
done

lemma nths_all'[simp]: "nths xs {0..
apply (induct xs)
apply simp
apply (simp add: nths_Cons)
done

lemma nths_single: "a < length xs \ nths xs {a} = [xs ! a]"
apply (induct xs arbitrary: a)
apply simp
apply(case_tac aa)
apply simp
apply (simp add: nths_Cons)
apply simp
apply (simp add: nths_Cons)
done

lemma nths_is_Nil: "\i \ inds. i \ length xs \ nths xs inds = []"
apply (induct xs arbitrary: inds)
apply simp
apply (simp add: nths_Cons)
apply auto
apply (erule_tac x="{j. Suc j \ inds}" in meta_allE)
apply auto
done

lemma nths_Nil': "nths xs inds = [] \ \i \ inds. i \ length xs"
apply (induct xs arbitrary: inds)
apply simp
apply (simp add: nths_Cons)
apply (auto split: if_splits)
apply (erule_tac x="{j. Suc j \ inds}" in meta_allE)
apply (case_tac x, auto)
done

lemma nths_Nil[simp]: "(nths xs inds = []) = (\i \ inds. i \ length xs)"
apply (induct xs arbitrary: inds)
apply simp
apply (simp add: nths_Cons)
apply auto
apply (erule_tac x="{j. Suc j \ inds}" in meta_allE)
apply (case_tac x, auto)
done

lemma nths_eq_subseteq: " \ inds' \ inds; nths xs inds = nths ys inds \ \ nths xs inds' = nths ys inds'"
apply (induct xs arbitrary: ys inds inds')
apply simp
apply (drule sym, rule sym)
apply (simp add: nths_Nil, fastforce)
apply (case_tac ys)
apply (simp add: nths_Nil, fastforce)
apply (auto simp add: nths_Cons)
apply (erule_tac x="list" in meta_allE)
apply (erule_tac x="{j. Suc j \ inds}" in meta_allE)
apply (erule_tac x="{j. Suc j \ inds'}" in meta_allE)
apply fastforce
apply (erule_tac x="list" in meta_allE)
apply (erule_tac x="{j. Suc j \ inds}" in meta_allE)
apply (erule_tac x="{j. Suc j \ inds'}" in meta_allE)
apply fastforce
done

lemma nths_eq: "\ \i \ inds. ((i < length xs) \ (i < length ys)) \ ((i \ length xs ) \ (i \ length ys)); \i \ inds. xs ! i = ys ! i \ \ nths xs inds = nths ys inds"
apply (induct xs arbitrary: ys inds)
apply simp
apply (rule sym, simp add: nths_Nil)
apply (case_tac ys)
apply (simp add: nths_Nil)
apply (auto simp add: nths_Cons)
apply (erule_tac x="list" in meta_allE)
apply (erule_tac x="{j. Suc j \ inds}" in meta_allE)
apply fastforce
apply (erule_tac x="list" in meta_allE)
apply (erule_tac x="{j. Suc j \ inds}" in meta_allE)
apply fastforce
done

lemma nths_eq_samelength: "\ length xs = length ys; \i \ inds. xs ! i = ys ! i \ \ nths xs inds = nths ys inds"
by (rule nths_eq, auto)

lemma nths_eq_samelength_iff: "length xs = length ys \ (nths xs inds = nths ys inds) = (\i \ inds. xs ! i = ys ! i)"
apply (induct xs arbitrary: ys inds)
apply simp
apply (rule sym, simp add: nths_Nil)
apply (case_tac ys)
apply (simp add: nths_Nil)
apply (auto simp add: nths_Cons)
apply (case_tac i)
apply auto
apply (case_tac i)
apply auto
done

section \<open>Another nths function\<close>

function nths' :: "nat \ nat \ 'a list \ 'a list"
where
  "nths' n m [] = []"
| "nths' n 0 xs = []"
| "nths' 0 (Suc m) (x#xs) = (x#nths' 0 m xs)"
| "nths' (Suc n) (Suc m) (x#xs) = nths' n m xs"
by pat_completeness auto
termination by lexicographic_order

subsection \<open>Proving equivalence to the other nths command\<close>

lemma nths'_nths: "nths' n m xs = nths xs {j. n \<le> j \<and> j < m}"
apply (induct xs arbitrary: n m)
apply simp
apply (case_tac n)
apply (case_tac m)
apply simp
apply (simp add: nths_Cons)
apply (case_tac m)
apply simp
apply (simp add: nths_Cons)
done

lemma "nths' n m xs = nths xs {n..
apply (induct xs arbitrary: n m)
apply simp
apply (case_tac n, case_tac m)
apply simp
apply simp
apply (simp add: nths_take')
apply (case_tac m)
apply simp
apply (simp add: nths_Cons nths'_nths)
done

subsection \<open>Showing equivalence to use of drop and take for definition\<close>

lemma "nths' n m xs = take (m - n) (drop n xs)"
apply (induct xs arbitrary: n m)
apply simp
apply (case_tac m)
apply simp
apply (case_tac n)
apply simp
apply simp
done

subsection \<open>General lemma about nths\<close>

lemma nths'_Nil[simp]: "nths' i j [] = []"
by simp

lemma nths'_Cons[simp]: "nths' i (Suc j) (x#xs) = (case i of 0 \<Rightarrow> (x # nths' 0 j xs) | Suc i' \<Rightarrow>  nths' i' j xs)"
by (cases i) auto

lemma nths'_Cons2[simp]: "nths' i j (x#xs) = (if (j = 0) then [] else ((if (i = 0) then [x] else []) @ nths' (i - 1) (j - 1) xs))"
apply (cases j)
apply auto
apply (cases i)
apply auto
done

lemma nths_n_0: "nths' n 0 xs = []"
by (induct xs, auto)

lemma nths'_Nil': "n \ m \ nths' n m xs = []"
apply (induct xs arbitrary: n m)
apply simp
apply (case_tac m)
apply simp
apply (case_tac n)
apply simp
apply simp
done

lemma nths'_Nil2: "n \ length xs \ nths' n m xs = []"
apply (induct xs arbitrary: n m)
apply simp
apply (case_tac m)
apply simp
apply (case_tac n)
apply simp
apply simp
done

lemma nths'_Nil3: "(nths' n m xs = []) = ((n \<ge> m) \<or> (n \<ge> length xs))"
apply (induct xs arbitrary: n m)
apply simp
apply (case_tac m)
apply simp
apply (case_tac n)
apply simp
apply simp
done

lemma nths'_notNil: "\ n < length xs; n < m \ \ nths' n m xs \ []"
apply (induct xs arbitrary: n m)
apply simp
apply (case_tac m)
apply simp
apply (case_tac n)
apply simp
apply simp
done

lemma nths'_single: "n < length xs \ nths' n (Suc n) xs = [xs ! n]"
apply (induct xs arbitrary: n)
apply simp
apply simp
apply (case_tac n)
apply (simp add: nths_n_0)
apply simp
done

lemma nths'_update1: "i \ m \ nths' n m (xs[i:=v]) = nths' n m xs"
apply (induct xs arbitrary: n m i)
apply simp
apply simp
apply (case_tac i)
apply simp
apply simp
done

lemma nths'_update2: "i < n \ nths' n m (xs[i:=v]) = nths' n m xs"
apply (induct xs arbitrary: n m i)
apply simp
apply simp
apply (case_tac i)
apply simp
apply simp
done

lemma nths'_update3: "\n \ i; i < m\ \ nths' n m (xs[i := v]) = (nths' n m xs)[i - n := v]"
proof (induct xs arbitrary: n m i)
  case Nil thus ?case by auto
next
  case (Cons x xs)
  thus ?case
    apply -
    apply auto
    apply (cases i)
    apply auto
    apply (cases i)
    apply auto
    done
qed

lemma "\ nths' i j xs = nths' i j ys; n \ i; m \ j \ \ nths' n m xs = nths' n m ys"
proof (induct xs arbitrary: i j ys n m)
  case Nil
  thus ?case
    apply -
    apply (rule sym, drule sym)
    apply (simp add: nths'_Nil)
    apply (simp add: nths'_Nil3)
    apply arith
    done
next
  case (Cons x xs i j ys n m)
  note c = this
  thus ?case
  proof (cases m)
    case 0 thus ?thesis by (simp add: nths_n_0)
  next
    case (Suc m')
    note a = this
    thus ?thesis
    proof (cases n)
      case 0 note b = this
      show ?thesis
      proof (cases ys)
        case Nil  with a b Cons.prems show ?thesis by (simp add: nths'_Nil3)
      next
        case (Cons y ys)
        show ?thesis
        proof (cases j)
          case 0 with a b Cons.prems show ?thesis by simp
        next
          case (Suc j') with a b Cons.prems Cons show ?thesis
            apply -
            apply (simp, rule Cons.hyps [of "0" "j'" "ys" "0" "m'"], auto)
            done
        qed
      qed
    next
      case (Suc n')
      show ?thesis
      proof (cases ys)
        case Nil with Suc a Cons.prems show ?thesis by (auto simp add: nths'_Nil3)
      next
        case (Cons y ys) with Suc a Cons.prems show ?thesis
          apply -
          apply simp
          apply (cases j)
          apply simp
          apply (cases i)
          apply simp
          apply (rule_tac j="nat" in Cons.hyps [of "0" _ "ys" "n'" "m'"])
          apply simp
          apply simp
          apply simp
          apply simp
          apply (rule_tac i="nata" and j="nat" in Cons.hyps [of _ _ "ys" "n'" "m'"])
          apply simp
          apply simp
          apply simp
          done
      qed
    qed
  qed
qed

lemma length_nths': "j \ length xs \ length (nths' i j xs) = j - i"
by (induct xs arbitrary: i j, auto)

lemma nths'_front: "\ i < j; i < length xs \ \ nths' i j xs = xs ! i # nths' (Suc i) j xs"
apply (induct xs arbitrary: i j)
apply simp
apply (case_tac j)
apply simp
apply (case_tac i)
apply simp
apply simp
done

lemma nths'_back: "\ i < j; j \ length xs \ \ nths' i j xs = nths' i (j - 1) xs @ [xs ! (j - 1)]"
apply (induct xs arbitrary: i j)
apply simp
apply simp
done

(* suffices that j \<le> length xs and length ys *)
lemma nths'_eq_samelength_iff: "length xs = length ys \ (nths' i j xs = nths' i j ys) = (\i'. i \ i' \ i' < j \ xs ! i' = ys ! i')"
proof (induct xs arbitrary: ys i j)
  case Nil thus ?case by simp
next
  case (Cons x xs)
  thus ?case
    apply -
    apply (cases ys)
    apply simp
    apply simp
    apply auto
    apply (case_tac i', auto)
    apply (erule_tac x="Suc i'" in allE, auto)
    apply (erule_tac x="i' - 1" in allE, auto)
    apply (erule_tac x="Suc i'" in allE, auto)
    done
qed

lemma nths'_all[simp]: "nths' 0 (length xs) xs = xs"
by (induct xs, auto)

lemma nths'_nths': "nths' n m (nths' i j xs) = nths' (i + n) (min (i + m) j) xs"
by (induct xs arbitrary: i j n m) (auto simp add: min_diff)

lemma nths'_append: "\ i \ j; j \ k \ \(nths' i j xs) @ (nths' j k xs) = nths' i k xs"
by (induct xs arbitrary: i j k) auto

lemma nth_nths': "\ k < j - i; j \ length xs \ \ (nths' i j xs) ! k = xs ! (i + k)"
apply (induct xs arbitrary: i j k)
apply simp
apply (case_tac k)
apply auto
done

lemma set_nths': "set (nths' i j xs) = {x. \<exists>k. i \<le> k \<and> k < j \<and> k < List.length xs \<and> x = xs ! k}"
apply (simp add: nths'_nths)
apply (simp add: set_nths)
apply auto
done

lemma all_in_set_nths'_conv: "(\j. j \ set (nths' l r xs) \ P j) = (\k. l \ k \ k < r \ k < List.length xs \ P (xs ! k))"
unfolding set_nths' by blast

lemma ball_in_set_nths'_conv: "(\j \ set (nths' l r xs). P j) = (\k. l \ k \ k < r \ k < List.length xs \ P (xs ! k))"
unfolding set_nths' by blast

lemma mset_nths:
assumes l_r: "l \ r \ r \ List.length xs"
assumes left: "\ i. i < l \ (xs::'a list) ! i = ys ! i"
assumes right: "\ i. i \ r \ (xs::'a list) ! i = ys ! i"
assumes multiset: "mset xs = mset ys"
  shows "mset (nths' l r xs) = mset (nths' l r ys)"
proof -
  from l_r have xs_def: "xs = (nths' 0 l xs) @ (nths' l r xs) @ (nths' r (List.length xs) xs)" (is "_ = ?xs_long")
    by (simp add: nths'_append)
  from multiset have length_eq: "List.length xs = List.length ys" by (rule mset_eq_length)
  with l_r have ys_def: "ys = (nths' 0 l ys) @ (nths' l r ys) @ (nths' r (List.length ys) ys)" (is "_ = ?ys_long")
    by (simp add: nths'_append)
  from xs_def ys_def multiset have "mset ?xs_long = mset ?ys_long" by simp
  moreover
  from left l_r length_eq have "nths' 0 l xs = nths' 0 l ys"
    by (auto simp add: length_nths' nth_nths' intro!: nth_equalityI)
  moreover
  from right l_r length_eq have "nths' r (List.length xs) xs = nths' r (List.length ys) ys"
    by (auto simp add: length_nths' nth_nths' intro!: nth_equalityI)
  ultimately show ?thesis by (simp add: mset_append)
qed

end

¤ Dauer der Verarbeitung: 0.4 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.