author nipkow Wed, 22 Jan 2020 14:37:23 +0100 changeset 71399 a77a3506548d parent 71397 028edb1e5b99 child 71400 58ddd7c5c84e
```--- a/src/HOL/Data_Structures/Array_Braun.thy	Sun Jan 19 14:50:03 2020 +0100
+++ b/src/HOL/Data_Structures/Array_Braun.thy	Wed Jan 22 14:37:23 2020 +0100
@@ -340,6 +340,30 @@
"take_nths i k (x # xs) = (if i = 0 then x # take_nths (2^k - 1) k xs
else take_nths (i - 1) k xs)"

+text \<open>This is the more concise definition but seems to complicate the proofs:\<close>
+
+lemma take_nths_eq_nths: "take_nths i k xs = nths xs (\<Union>n. {n*2^k + i})"
+proof(induction xs arbitrary: i)
+  case Nil
+  then show ?case by simp
+next
+  case (Cons x xs)
+  show ?case
+  proof cases
+    assume [simp]: "i = 0"
+    have "(\<Union>n. {(n+1) * 2 ^ k - 1}) = {m. \<exists>n. Suc m = n * 2 ^ k}"
+      apply (auto simp del: mult_Suc)
+      by (metis diff_Suc_Suc diff_zero mult_eq_0_iff not0_implies_Suc)
+    thus ?thesis by (simp add: Cons.IH ac_simps nths_Cons)
+  next
+    assume [arith]: "i \<noteq> 0"
+    have "(\<Union>n. {n * 2 ^ k + i - 1}) = {m. \<exists>n. Suc m = n * 2 ^ k + i}"
+      apply auto
+      by (metis diff_Suc_Suc diff_zero)
+    thus ?thesis by (simp add: Cons.IH nths_Cons)
+  qed
+qed
+
lemma take_nths_drop:
"take_nths i k (drop j xs) = take_nths (i + j) k xs"
by (induct xs arbitrary: i j; simp add: drop_Cons split: nat.split)```