kings-crown/FVELER_Isabelle huggingface dataset:
theory Reversed_Bit_Lists

lemma nth_takefill: "m < n \<Longrightarrow> takefill fill n l ! m = (if m < length l then l ! m else fill)" apply (induct n arbitrary: m l) apply clarsimp apply clarsimp apply (case_tac m) apply (simp split: list.split) apply (simp split: list.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m < n \<Longrightarrow> takefill fill n l ! m = (if m < length l then l ! m else fill) proof (prove)
goal (2 subgoals):
 1. \<And>m l. m < 0 \<Longrightarrow> takefill fill 0 l ! m = (if m < length l then l ! m else fill)
 2. \<And>n m l. \<lbrakk>\<And>m l. m < n \<Longrightarrow> takefill fill n l ! m = (if m < length l then l ! m else fill); m < Suc n\<rbrakk> \<Longrightarrow> takefill fill (Suc n) l ! m = (if m < length l then l ! m else fill) proof (prove)
goal (1 subgoal):
 1. \<And>n m l. \<lbrakk>\<And>m l. m < n \<Longrightarrow> takefill fill n l ! m = (if m < length l then l ! m else fill); m < Suc n\<rbrakk> \<Longrightarrow> takefill fill (Suc n) l ! m = (if m < length l then l ! m else fill) proof (prove)
goal (1 subgoal):
 1. \<And>n m l. \<lbrakk>\<And>m l. m < n \<Longrightarrow> takefill fill n l ! m = (if m < length l then l ! m else fill); m < Suc n\<rbrakk> \<Longrightarrow> (m < length l \<longrightarrow> (case l of [] \<Rightarrow> fill # takefill fill n l | y # ys \<Rightarrow> y # takefill fill n ys) ! m = l ! m) \<and> (\<not> m < length l \<longrightarrow> (case l of [] \<Rightarrow> fill # takefill fill n l | y # ys \<Rightarrow> y # takefill fill n ys) ! m = fill) proof (prove)
goal (2 subgoals):
 1. \<And>n m l. \<lbrakk>\<And>m l. m < n \<Longrightarrow> takefill fill n l ! m = (if m < length l then l ! m else fill); m < Suc n; m = 0\<rbrakk> \<Longrightarrow> (m < length l \<longrightarrow> (case l of [] \<Rightarrow> fill # takefill fill n l | y # ys \<Rightarrow> y # takefill fill n ys) ! m = l ! m) \<and> (\<not> m < length l \<longrightarrow> (case l of [] \<Rightarrow> fill # takefill fill n l | y # ys \<Rightarrow> y # takefill fill n ys) ! m = fill)
 2. \<And>n m l nat. \<lbrakk>\<And>m l. m < n \<Longrightarrow> takefill fill n l ! m = (if m < length l then l ! m else fill); m < Suc n; m = Suc nat\<rbrakk> \<Longrightarrow> (m < length l \<longrightarrow> (case l of [] \<Rightarrow> fill # takefill fill n l | y # ys \<Rightarrow> y # takefill fill n ys) ! m = l ! m) \<and> (\<not> m < length l \<longrightarrow> (case l of [] \<Rightarrow> fill # takefill fill n l | y # ys \<Rightarrow> y # takefill fill n ys) ! m = fill) proof (prove)
goal (1 subgoal):
 1. \<And>n m l nat. \<lbrakk>\<And>m l. m < n \<Longrightarrow> takefill fill n l ! m = (if m < length l then l ! m else fill); m < Suc n; m = Suc nat\<rbrakk> \<Longrightarrow> (m < length l \<longrightarrow> (case l of [] \<Rightarrow> fill # takefill fill n l | y # ys \<Rightarrow> y # takefill fill n ys) ! m = l ! m) \<and> (\<not> m < length l \<longrightarrow> (case l of [] \<Rightarrow> fill # takefill fill n l | y # ys \<Rightarrow> y # takefill fill n ys) ! m = fill) proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma takefill_replicate [simp]: "takefill fill n (replicate m fill) = replicate n fill" by (simp add: takefill_alt replicate_add [symmetric])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. takefill fill n (replicate m fill) = replicate n fill
theory Reversed_Bit_Lists

lemma takefill_le': "n = m + k \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l" by (induct m arbitrary: l n) (auto split: list.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n = m + k \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l
theory Reversed_Bit_Lists

lemma length_takefill [simp]: "length (takefill fill n l) = n" by (simp add: takefill_alt)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length (takefill fill n l) = n
theory Reversed_Bit_Lists

lemma take_takefill': "n = k + m \<Longrightarrow> take k (takefill fill n w) = takefill fill k w" by (induct k arbitrary: w n) (auto split: list.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n = k + m \<Longrightarrow> take k (takefill fill n w) = takefill fill k w
theory Reversed_Bit_Lists

lemma drop_takefill: "drop k (takefill fill (m + k) w) = takefill fill m (drop k w)" by (induct k arbitrary: w) (auto split: list.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. drop k (takefill fill (m + k) w) = takefill fill m (drop k w)
theory Reversed_Bit_Lists

lemma takefill_le [simp]: "m \<le> n \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l" by (auto simp: le_iff_add takefill_le')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<le> n \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l
theory Reversed_Bit_Lists

lemma take_takefill [simp]: "m \<le> n \<Longrightarrow> take m (takefill fill n w) = takefill fill m w" by (auto simp: le_iff_add take_takefill')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<le> n \<Longrightarrow> take m (takefill fill n w) = takefill fill m w
theory Reversed_Bit_Lists

lemma takefill_append: "takefill fill (m + length xs) (xs @ w) = xs @ (takefill fill m w)" by (induct xs) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. takefill fill (m + length xs) (xs @ w) = xs @ takefill fill m w
theory Reversed_Bit_Lists

lemma takefill_same': "l = length xs \<Longrightarrow> takefill fill l xs = xs" by (induct xs arbitrary: l) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. l = length xs \<Longrightarrow> takefill fill l xs = xs
theory Reversed_Bit_Lists

lemma tf_rev:
  "n + k = m + length bl \<Longrightarrow> takefill x m (rev (takefill y n bl)) =
    rev (takefill y m (rev (takefill x k (rev bl))))" apply (rule nth_equalityI) apply (auto simp add: nth_takefill rev_nth) apply (rule_tac f = "\<lambda>n. bl ! n" in arg_cong) apply arith done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n + k = m + length bl \<Longrightarrow> takefill x m (rev (takefill y n bl)) = rev (takefill y m (rev (takefill x k (rev bl)))) proof (prove)
goal (2 subgoals):
 1. n + k = m + length bl \<Longrightarrow> length (takefill x m (rev (takefill y n bl))) = length (rev (takefill y m (rev (takefill x k (rev bl)))))
 2. \<And>i. \<lbrakk>n + k = m + length bl; i < length (takefill x m (rev (takefill y n bl)))\<rbrakk> \<Longrightarrow> takefill x m (rev (takefill y n bl)) ! i = rev (takefill y m (rev (takefill x k (rev bl)))) ! i proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>n + k = m + length bl; i < m; n - Suc i < length bl; k + i - m < length bl; i < n; m - Suc i < k\<rbrakk> \<Longrightarrow> bl ! (n - Suc i) = bl ! (length bl + m - Suc (k + i)) proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>n + k = m + length bl; i < m; n - Suc i < length bl; k + i - m < length bl; i < n; m - Suc i < k\<rbrakk> \<Longrightarrow> n - Suc i = length bl + m - Suc (k + i) proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma takefill_minus: "0 < n \<Longrightarrow> takefill fill (Suc (n - 1)) w = takefill fill n w" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> takefill fill (Suc (n - 1)) w = takefill fill n w
theory Reversed_Bit_Lists

lemma takefill_numeral_Nil [simp]:
  "takefill fill (numeral k) [] = fill # takefill fill (pred_numeral k) []" by (simp add: numeral_eq_Suc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. takefill fill (numeral k) [] = fill # takefill fill (pred_numeral k) []
theory Reversed_Bit_Lists

lemma takefill_numeral_Cons [simp]:
  "takefill fill (numeral k) (x # xs) = x # takefill fill (pred_numeral k) xs" by (simp add: numeral_eq_Suc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. takefill fill (numeral k) (x # xs) = x # takefill fill (pred_numeral k) xs
theory Reversed_Bit_Lists

lemma bl_of_nth_simps [simp, code]:
  "bl_of_nth 0 f = []"
  "bl_of_nth (Suc n) f = f n # bl_of_nth n f" by (simp_all add: bl_of_nth_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bl_of_nth 0 f = [] &&& bl_of_nth (Suc n) f = f n # bl_of_nth n f
theory Reversed_Bit_Lists

lemma length_bl_of_nth [simp]: "length (bl_of_nth n f) = n" by (simp add: bl_of_nth_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length (bl_of_nth n f) = n
theory Reversed_Bit_Lists

lemma nth_bl_of_nth [simp]: "m < n \<Longrightarrow> rev (bl_of_nth n f) ! m = f m" by (simp add: bl_of_nth_def rev_map)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m < n \<Longrightarrow> rev (bl_of_nth n f) ! m = f m
theory Reversed_Bit_Lists

lemma bl_of_nth_inj: "(\<And>k. k < n \<Longrightarrow> f k = g k) \<Longrightarrow> bl_of_nth n f = bl_of_nth n g" by (simp add: bl_of_nth_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>k. k < n \<Longrightarrow> f k = g k) \<Longrightarrow> bl_of_nth n f = bl_of_nth n g
theory Reversed_Bit_Lists

lemma bl_of_nth_nth [simp]: "bl_of_nth (length xs) ((!) (rev xs)) = xs" by (simp add: bl_of_nth_nth_le)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bl_of_nth (length xs) ((!) (rev xs)) = xs
theory Reversed_Bit_Lists

lemma rotate1_rl': "rotater1 (l @ [a]) = a # l" by (cases l) (auto simp: rotater1_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rotater1 (l @ [a]) = a # l
theory Reversed_Bit_Lists

lemma rotate1_rl [simp] : "rotater1 (rotate1 l) = l" apply (unfold rotater1_def) apply (cases "l") apply (case_tac [2] "list") apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rotater1 (rotate1 l) = l proof (prove)
goal (1 subgoal):
 1. (case rotate1 l of [] \<Rightarrow> [] | x # xs \<Rightarrow> last (rotate1 l) # butlast (rotate1 l)) = l proof (prove)
goal (2 subgoals):
 1. l = [] \<Longrightarrow> (case rotate1 l of [] \<Rightarrow> [] | x # xs \<Rightarrow> last (rotate1 l) # butlast (rotate1 l)) = l
 2. \<And>a list. l = a # list \<Longrightarrow> (case rotate1 l of [] \<Rightarrow> [] | x # xs \<Rightarrow> last (rotate1 l) # butlast (rotate1 l)) = l proof (prove)
goal (3 subgoals):
 1. l = [] \<Longrightarrow> (case rotate1 l of [] \<Rightarrow> [] | x # xs \<Rightarrow> last (rotate1 l) # butlast (rotate1 l)) = l
 2. \<And>a list. \<lbrakk>l = a # list; list = []\<rbrakk> \<Longrightarrow> (case rotate1 l of [] \<Rightarrow> [] | x # xs \<Rightarrow> last (rotate1 l) # butlast (rotate1 l)) = l
 3. \<And>a list aa lista. \<lbrakk>l = a # list; list = aa # lista\<rbrakk> \<Longrightarrow> (case rotate1 l of [] \<Rightarrow> [] | x # xs \<Rightarrow> last (rotate1 l) # butlast (rotate1 l)) = l proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma rotate1_lr [simp] : "rotate1 (rotater1 l) = l" by (cases l) (auto simp: rotater1_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rotate1 (rotater1 l) = l
theory Reversed_Bit_Lists

lemma rotater1_rev': "rotater1 (rev xs) = rev (rotate1 xs)" by (cases "xs") (simp add: rotater1_def, simp add: rotate1_rl')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rotater1 (rev xs) = rev (rotate1 xs)
theory Reversed_Bit_Lists

lemma rotater_rev': "rotater n (rev xs) = rev (rotate n xs)" by (induct n) (auto simp: rotater_def intro: rotater1_rev')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rotater n (rev xs) = rev (rotate n xs)
theory Reversed_Bit_Lists

lemma rotater_rev: "rotater n ys = rev (rotate n (rev ys))" using rotater_rev' [where xs = "rev ys"] by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rotater n ys = rev (rotate n (rev ys)) proof (prove)
using this:
rotater ?n (rev (rev ys)) = rev (rotate ?n (rev ys))

goal (1 subgoal):
 1. rotater n ys = rev (rotate n (rev ys))
theory Reversed_Bit_Lists

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rotater n xs = drop (length xs - n mod length xs) xs @ take (length xs - n mod length xs) xs
theory Reversed_Bit_Lists

lemma rotater_Suc [simp]: "rotater (Suc n) xs = rotater1 (rotater n xs)" unfolding rotater_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rotater (Suc n) xs = rotater1 (rotater n xs) proof (prove)
goal (1 subgoal):
 1. (rotater1 ^^ Suc n) xs = rotater1 ((rotater1 ^^ n) xs)
theory Reversed_Bit_Lists

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rotater1 xs ! n = xs ! ((n + (length xs - 1)) mod length xs) proof (prove)
using this:
n < length xs
n < length xs \<Longrightarrow> rotater 1 xs ! n = xs ! ((n + (length xs - 1 mod length xs)) mod length xs)

goal (1 subgoal):
 1. rotater1 xs ! n = xs ! ((n + (length xs - 1)) mod length xs)
theory Reversed_Bit_Lists

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<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
theory Reversed_Bit_Lists

lemma rotate_gal: "rotater n xs = ys \<longleftrightarrow> rotate n ys = xs" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (rotater n xs = ys) = (rotate n ys = xs)
theory Reversed_Bit_Lists

lemma rotate_gal': "ys = rotater n xs \<longleftrightarrow> xs = rotate n ys" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (ys = rotater n xs) = (xs = rotate n ys)
theory Reversed_Bit_Lists

lemma length_rotater [simp]: "length (rotater n xs) = length xs" by (simp add : rotater_rev)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length (rotater n xs) = length xs
theory Reversed_Bit_Lists

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m mod length xs = n mod length xs \<Longrightarrow> rotate m xs = rotate n xs proof (prove)
goal (3 subgoals):
 1. m mod length xs = n mod length xs \<Longrightarrow> ?a = ?b
 2. m mod length xs = n mod length xs \<Longrightarrow> ?a = rotate m xs
 3. m mod length xs = n mod length xs \<Longrightarrow> ?b = rotate n xs proof (prove)
goal (3 subgoals):
 1. m mod length xs = n mod length xs \<Longrightarrow> ?a = rotate m xs
 2. m mod length xs = n mod length xs \<Longrightarrow> ?b = rotate n xs
 3. m mod length xs = n mod length xs \<Longrightarrow> ?a = ?b proof (prove)
goal (1 subgoal):
 1. m mod length xs = n mod length xs \<Longrightarrow> rotate (m mod length xs) xs = rotate (n mod length xs) xs proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma restrict_to_left: "x = y \<Longrightarrow> x = z \<longleftrightarrow> y = z" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x = y \<Longrightarrow> (x = z) = (y = z)
theory Reversed_Bit_Lists

lemma butlast_map: "xs \<noteq> [] \<Longrightarrow> butlast (map f xs) = map f (butlast xs)" by (induct xs) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> butlast (map f xs) = map f (butlast xs)
theory Reversed_Bit_Lists

lemma rotater1_map: "rotater1 (map f xs) = map f (rotater1 xs)" by (cases xs) (auto simp: rotater1_def last_map butlast_map)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rotater1 (map f xs) = map f (rotater1 xs)
theory Reversed_Bit_Lists

lemma rotater_map: "rotater n (map f xs) = map f (rotater n xs)" by (induct n) (auto simp: rotater_def rotater1_map)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rotater n (map f xs) = map f (rotater n xs)
theory Reversed_Bit_Lists

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<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) proof (prove)
goal (2 subgoals):
 1. \<forall>ys. length [] = length ys \<longrightarrow> [] \<noteq> [] \<longrightarrow> last (zip [] ys) = (last [], last ys) \<and> butlast (zip [] ys) = zip (butlast []) (butlast ys)
 2. \<And>a xs. \<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) \<Longrightarrow> \<forall>ys. length (a # xs) = length ys \<longrightarrow> a # xs \<noteq> [] \<longrightarrow> last (zip (a # xs) ys) = (last (a # xs), last ys) \<and> butlast (zip (a # xs) ys) = zip (butlast (a # xs)) (butlast ys) proof (prove)
goal (4 subgoals):
 1. \<And>a ys. Suc 0 = length ys \<Longrightarrow> last (zip [a] ys) = (a, last ys)
 2. \<And>a ys. Suc 0 = length ys \<Longrightarrow> butlast (zip [a] ys) = []
 3. \<And>a xs ys. \<lbrakk>\<forall>ys. length xs = length ys \<longrightarrow> last (zip xs ys) = (last xs, last ys) \<and> butlast (zip xs ys) = zip (butlast xs) (butlast ys); xs \<noteq> []; Suc (length xs) = length ys\<rbrakk> \<Longrightarrow> last (zip (a # xs) ys) = (last xs, last ys)
 4. \<And>a xs ys. \<lbrakk>\<forall>ys. length xs = length ys \<longrightarrow> last (zip xs ys) = (last xs, last ys) \<and> butlast (zip xs ys) = zip (butlast xs) (butlast ys); xs \<noteq> []; Suc (length xs) = length ys\<rbrakk> \<Longrightarrow> butlast (zip (a # xs) ys) = zip (a # butlast xs) (butlast ys) proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<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) proof (prove)
goal (2 subgoals):
 1. \<forall>ys. length [] = length ys \<longrightarrow> [] \<noteq> [] \<longrightarrow> last (map2 f [] ys) = f (last []) (last ys) \<and> butlast (map2 f [] ys) = map2 f (butlast []) (butlast ys)
 2. \<And>a xs. \<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) \<Longrightarrow> \<forall>ys. length (a # xs) = length ys \<longrightarrow> a # xs \<noteq> [] \<longrightarrow> last (map2 f (a # xs) ys) = f (last (a # xs)) (last ys) \<and> butlast (map2 f (a # xs) ys) = map2 f (butlast (a # xs)) (butlast ys) proof (prove)
goal (4 subgoals):
 1. \<And>a ys. Suc 0 = length ys \<Longrightarrow> last (map2 f [a] ys) = f a (last ys)
 2. \<And>a ys. Suc 0 = length ys \<Longrightarrow> butlast (map2 f [a] ys) = []
 3. \<And>a xs ys. \<lbrakk>\<forall>ys. length xs = length ys \<longrightarrow> last (map2 f xs ys) = f (last xs) (last ys) \<and> butlast (map2 f xs ys) = map2 f (butlast xs) (butlast ys); xs \<noteq> []; Suc (length xs) = length ys\<rbrakk> \<Longrightarrow> last (map2 f (a # xs) ys) = f (last xs) (last ys)
 4. \<And>a xs ys. \<lbrakk>\<forall>ys. length xs = length ys \<longrightarrow> last (map2 f xs ys) = f (last xs) (last ys) \<and> butlast (map2 f xs ys) = map2 f (butlast xs) (butlast ys); xs \<noteq> []; Suc (length xs) = length ys\<rbrakk> \<Longrightarrow> butlast (map2 f (a # xs) ys) = map2 f (a # butlast xs) (butlast ys) proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length xs = length ys \<Longrightarrow> rotater1 (zip xs ys) = zip (rotater1 xs) (rotater1 ys) proof (prove)
goal (1 subgoal):
 1. length xs = length ys \<Longrightarrow> (case zip xs ys of [] \<Rightarrow> [] | x # xsa \<Rightarrow> last (zip xs ys) # butlast (zip xs ys)) = zip (case xs of [] \<Rightarrow> [] | x # xsa \<Rightarrow> last xs # butlast xs) (case ys of [] \<Rightarrow> [] | x # xs \<Rightarrow> last ys # butlast ys) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>length xs = length ys; xs = []\<rbrakk> \<Longrightarrow> (case zip xs ys of [] \<Rightarrow> [] | x # xsa \<Rightarrow> last (zip xs ys) # butlast (zip xs ys)) = zip (case xs of [] \<Rightarrow> [] | x # xsa \<Rightarrow> last xs # butlast xs) (case ys of [] \<Rightarrow> [] | x # xs \<Rightarrow> last ys # butlast ys)
 2. \<And>a list. \<lbrakk>length xs = length ys; xs = a # list\<rbrakk> \<Longrightarrow> (case zip xs ys of [] \<Rightarrow> [] | x # xsa \<Rightarrow> last (zip xs ys) # butlast (zip xs ys)) = zip (case xs of [] \<Rightarrow> [] | x # xsa \<Rightarrow> last xs # butlast xs) (case ys of [] \<Rightarrow> [] | x # xs \<Rightarrow> last ys # butlast ys) proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>Suc 0 = length ys; xs = [a]\<rbrakk> \<Longrightarrow> (case zip [a] ys of [] \<Rightarrow> [] | x # xs \<Rightarrow> last (zip [a] ys) # butlast (zip [a] ys)) = zip [a] (case ys of [] \<Rightarrow> [] | x # xs \<Rightarrow> last ys # butlast ys)
 2. \<And>a list. \<lbrakk>Suc (length list) = length ys; xs = a # list; list \<noteq> []\<rbrakk> \<Longrightarrow> (case zip (a # list) ys of [] \<Rightarrow> [] | x # xs \<Rightarrow> last (zip (a # list) ys) # butlast (zip (a # list) ys)) = zip (last list # a # butlast list) (case ys of [] \<Rightarrow> [] | x # xs \<Rightarrow> last ys # butlast ys) proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length xs = length ys \<Longrightarrow> rotater1 (map2 f xs ys) = map2 f (rotater1 xs) (rotater1 ys)
theory Reversed_Bit_Lists

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length xs = length ys \<Longrightarrow> rotater n (map2 f xs ys) = map2 f (rotater n xs) (rotater n ys)
theory Reversed_Bit_Lists

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length xs = length ys \<Longrightarrow> rotate1 (map2 f xs ys) = map2 f (rotate1 xs) (rotate1 ys)
theory Reversed_Bit_Lists

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length xs = length ys \<Longrightarrow> rotate n (map2 f xs ys) = map2 f (rotate n xs) (rotate n ys)