equal
deleted
inserted
replaced
4773 qed |
4773 qed |
4774 |
4774 |
4775 lemma rotate_append: "rotate (length l) (l @ q) = q @ l" |
4775 lemma rotate_append: "rotate (length l) (l @ q) = q @ l" |
4776 by (induct l arbitrary: q) (auto simp add: rotate1_rotate_swap) |
4776 by (induct l arbitrary: q) (auto simp add: rotate1_rotate_swap) |
4777 |
4777 |
|
4778 lemma nth_rotate: |
|
4779 \<open>rotate m xs ! n = xs ! ((m + n) mod length xs)\<close> if \<open>n < length xs\<close> |
|
4780 using that apply (auto simp add: rotate_drop_take nth_append not_less less_diff_conv ac_simps dest!: le_Suc_ex) |
|
4781 apply (metis add.commute mod_add_right_eq mod_less) |
|
4782 apply (metis (no_types, lifting) Nat.diff_diff_right add.commute add_diff_cancel_right' diff_le_self dual_order.strict_trans2 length_greater_0_conv less_nat_zero_code list.size(3) mod_add_right_eq mod_add_self2 mod_le_divisor mod_less) |
|
4783 done |
|
4784 |
|
4785 lemma nth_rotate1: |
|
4786 \<open>rotate1 xs ! n = xs ! (Suc n mod length xs)\<close> if \<open>n < length xs\<close> |
|
4787 using that nth_rotate [of n xs 1] by simp |
|
4788 |
4778 |
4789 |
4779 subsubsection \<open>\<^const>\<open>nths\<close> --- a generalization of \<^const>\<open>nth\<close> to sets\<close> |
4790 subsubsection \<open>\<^const>\<open>nths\<close> --- a generalization of \<^const>\<open>nth\<close> to sets\<close> |
4780 |
4791 |
4781 lemma nths_empty [simp]: "nths xs {} = []" |
4792 lemma nths_empty [simp]: "nths xs {} = []" |
4782 by (auto simp add: nths_def) |
4793 by (auto simp add: nths_def) |