summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Wed, 22 Jan 2020 14:37:23 +0100 | |

changeset 71399 | a77a3506548d |

parent 71397 | 028edb1e5b99 |

child 71400 | 58ddd7c5c84e |

added lemma

--- 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)