--- a/src/HOL/Word/Bit_Lists.thy Wed Jul 29 14:23:19 2020 +0200
+++ b/src/HOL/Word/Bit_Lists.thy Sat Aug 01 17:43:30 2020 +0000
@@ -134,4 +134,166 @@
lemma bl_bin_bl_rtf: "bin_to_bl n (bl_to_bin bl) = rev (takefill False n (rev bl))"
by (simp add: takefill_bintrunc)
+
+subsection \<open>More\<close>
+
+definition rotater1 :: "'a list \<Rightarrow> 'a list"
+ where "rotater1 ys =
+ (case ys of [] \<Rightarrow> [] | x # xs \<Rightarrow> last ys # butlast ys)"
+
+definition rotater :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
+ where "rotater n = rotater1 ^^ n"
+
+lemmas rotater_0' [simp] = rotater_def [where n = "0", simplified]
+
+lemma rotate1_rl': "rotater1 (l @ [a]) = a # l"
+ by (cases l) (auto simp: rotater1_def)
+
+lemma rotate1_rl [simp] : "rotater1 (rotate1 l) = l"
+ apply (unfold rotater1_def)
+ apply (cases "l")
+ apply (case_tac [2] "list")
+ apply auto
+ done
+
+lemma rotate1_lr [simp] : "rotate1 (rotater1 l) = l"
+ by (cases l) (auto simp: rotater1_def)
+
+lemma rotater1_rev': "rotater1 (rev xs) = rev (rotate1 xs)"
+ by (cases "xs") (simp add: rotater1_def, simp add: rotate1_rl')
+
+lemma rotater_rev': "rotater n (rev xs) = rev (rotate n xs)"
+ by (induct n) (auto simp: rotater_def intro: rotater1_rev')
+
+lemma rotater_rev: "rotater n ys = rev (rotate n (rev ys))"
+ using rotater_rev' [where xs = "rev ys"] by simp
+
+lemma rotater_drop_take:
+ "rotater n xs =
+ drop (length xs - n mod length xs) xs @
+ take (length xs - n mod length xs) xs"
+ by (auto simp: rotater_rev rotate_drop_take rev_take rev_drop)
+
+lemma rotater_Suc [simp]: "rotater (Suc n) xs = rotater1 (rotater n xs)"
+ unfolding rotater_def by auto
+
+lemma nth_rotater:
+ \<open>rotater m xs ! n = xs ! ((n + (length xs - m mod length xs)) mod length xs)\<close> if \<open>n < length xs\<close>
+ using that by (simp add: rotater_drop_take nth_append not_less less_diff_conv ac_simps le_mod_geq)
+
+lemma nth_rotater1:
+ \<open>rotater1 xs ! n = xs ! ((n + (length xs - 1)) mod length xs)\<close> if \<open>n < length xs\<close>
+ using that nth_rotater [of n xs 1] by simp
+
+lemma rotate_inv_plus [rule_format]:
+ "\<forall>k. k = m + n \<longrightarrow> rotater k (rotate n xs) = rotater m xs \<and>
+ rotate k (rotater n xs) = rotate m xs \<and>
+ rotater n (rotate k xs) = rotate m xs \<and>
+ rotate n (rotater k xs) = rotater m xs"
+ by (induct n) (auto simp: rotater_def rotate_def intro: funpow_swap1 [THEN trans])
+
+lemmas rotate_inv_rel = le_add_diff_inverse2 [symmetric, THEN rotate_inv_plus]
+
+lemmas rotate_inv_eq = order_refl [THEN rotate_inv_rel, simplified]
+
+lemmas rotate_lr [simp] = rotate_inv_eq [THEN conjunct1]
+lemmas rotate_rl [simp] = rotate_inv_eq [THEN conjunct2, THEN conjunct1]
+
+lemma rotate_gal: "rotater n xs = ys \<longleftrightarrow> rotate n ys = xs"
+ by auto
+
+lemma rotate_gal': "ys = rotater n xs \<longleftrightarrow> xs = rotate n ys"
+ by auto
+
+lemma length_rotater [simp]: "length (rotater n xs) = length xs"
+ by (simp add : rotater_rev)
+
+lemma rotate_eq_mod: "m mod length xs = n mod length xs \<Longrightarrow> rotate m xs = rotate n xs"
+ apply (rule box_equals)
+ defer
+ apply (rule rotate_conv_mod [symmetric])+
+ apply simp
+ done
+
+lemma restrict_to_left: "x = y \<Longrightarrow> x = z \<longleftrightarrow> y = z"
+ by simp
+
+lemmas rotate_eqs =
+ trans [OF rotate0 [THEN fun_cong] id_apply]
+ rotate_rotate [symmetric]
+ rotate_id
+ rotate_conv_mod
+ rotate_eq_mod
+
+lemmas rrs0 = rotate_eqs [THEN restrict_to_left,
+ simplified rotate_gal [symmetric] rotate_gal' [symmetric]]
+lemmas rrs1 = rrs0 [THEN refl [THEN rev_iffD1]]
+lemmas rotater_eqs = rrs1 [simplified length_rotater]
+lemmas rotater_0 = rotater_eqs (1)
+lemmas rotater_add = rotater_eqs (2)
+
+lemma butlast_map: "xs \<noteq> [] \<Longrightarrow> butlast (map f xs) = map f (butlast xs)"
+ by (induct xs) auto
+
+lemma rotater1_map: "rotater1 (map f xs) = map f (rotater1 xs)"
+ by (cases xs) (auto simp: rotater1_def last_map butlast_map)
+
+lemma rotater_map: "rotater n (map f xs) = map f (rotater n xs)"
+ by (induct n) (auto simp: rotater_def rotater1_map)
+
+lemma but_last_zip [rule_format] :
+ "\<forall>ys. length xs = length ys \<longrightarrow> xs \<noteq> [] \<longrightarrow>
+ last (zip xs ys) = (last xs, last ys) \<and>
+ butlast (zip xs ys) = zip (butlast xs) (butlast ys)"
+ apply (induct xs)
+ apply auto
+ apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
+ done
+
+lemma but_last_map2 [rule_format] :
+ "\<forall>ys. length xs = length ys \<longrightarrow> xs \<noteq> [] \<longrightarrow>
+ last (map2 f xs ys) = f (last xs) (last ys) \<and>
+ butlast (map2 f xs ys) = map2 f (butlast xs) (butlast ys)"
+ apply (induct xs)
+ apply auto
+ apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
+ done
+
+lemma rotater1_zip:
+ "length xs = length ys \<Longrightarrow>
+ rotater1 (zip xs ys) = zip (rotater1 xs) (rotater1 ys)"
+ apply (unfold rotater1_def)
+ apply (cases xs)
+ apply auto
+ apply ((case_tac ys, auto simp: neq_Nil_conv but_last_zip)[1])+
+ done
+
+lemma rotater1_map2:
+ "length xs = length ys \<Longrightarrow>
+ rotater1 (map2 f xs ys) = map2 f (rotater1 xs) (rotater1 ys)"
+ by (simp add: rotater1_map rotater1_zip)
+
+lemmas lrth =
+ box_equals [OF asm_rl length_rotater [symmetric]
+ length_rotater [symmetric],
+ THEN rotater1_map2]
+
+lemma rotater_map2:
+ "length xs = length ys \<Longrightarrow>
+ rotater n (map2 f xs ys) = map2 f (rotater n xs) (rotater n ys)"
+ by (induct n) (auto intro!: lrth)
+
+lemma rotate1_map2:
+ "length xs = length ys \<Longrightarrow>
+ rotate1 (map2 f xs ys) = map2 f (rotate1 xs) (rotate1 ys)"
+ by (cases xs; cases ys) auto
+
+lemmas lth = box_equals [OF asm_rl length_rotate [symmetric]
+ length_rotate [symmetric], THEN rotate1_map2]
+
+lemma rotate_map2:
+ "length xs = length ys \<Longrightarrow>
+ rotate n (map2 f xs ys) = map2 f (rotate n xs) (rotate n ys)"
+ by (induct n) (auto intro!: lth)
+
end