kings-crown/FVELER_Isabelle huggingface dataset:
theory Bits_Int

lemma sbintrunc_rest [simp]: "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n ((\<lambda>k::int. k div 2) ((signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n bin)) = (\<lambda>k::int. k div 2) ((signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n bin)" by (induct n arbitrary: bin) (simp_all add: signed_take_bit_Suc mod2_eq_if)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. signed_take_bit n (signed_take_bit n bin div 2) = signed_take_bit n bin div 2
theory Bits_Int

lemma bintrunc_rest': "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n \<circ> (\<lambda>k::int. k div 2) \<circ> (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n = (\<lambda>k::int. k div 2) \<circ> (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n" by (rule ext) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. take_bit n \<circ> (\<lambda>k. k div 2) \<circ> take_bit n = (\<lambda>k. k div 2) \<circ> take_bit n
theory Bits_Int

lemma sbintrunc_rest': "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n \<circ> (\<lambda>k::int. k div 2) \<circ> (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n = (\<lambda>k::int. k div 2) \<circ> (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n" by (rule ext) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. signed_take_bit n \<circ> (\<lambda>k. k div 2) \<circ> signed_take_bit n = (\<lambda>k. k div 2) \<circ> signed_take_bit n
theory Bits_Int

lemma rco_lem: "f \<circ> g \<circ> f = g \<circ> f \<Longrightarrow> f \<circ> (g \<circ> f) ^^ n = g ^^ n \<circ> f" apply (rule ext) apply (induct_tac n) apply (simp_all (no_asm)) apply (drule fun_cong) apply (unfold o_def) apply (erule trans) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f \<circ> g \<circ> f = g \<circ> f \<Longrightarrow> f \<circ> (g \<circ> f) ^^ n = g ^^ n \<circ> f proof (prove)
goal (1 subgoal):
 1. \<And>x. f \<circ> g \<circ> f = g \<circ> f \<Longrightarrow> (f \<circ> (g \<circ> f) ^^ n) x = (g ^^ n \<circ> f) x proof (prove)
goal (2 subgoals):
 1. \<And>x. f \<circ> g \<circ> f = g \<circ> f \<Longrightarrow> (f \<circ> (g \<circ> f) ^^ 0) x = (g ^^ 0 \<circ> f) x
 2. \<And>x n. \<lbrakk>f \<circ> g \<circ> f = g \<circ> f; (f \<circ> (g \<circ> f) ^^ n) x = (g ^^ n \<circ> f) x\<rbrakk> \<Longrightarrow> (f \<circ> (g \<circ> f) ^^ Suc n) x = (g ^^ Suc n \<circ> f) x proof (prove)
goal (1 subgoal):
 1. \<And>x n. \<lbrakk>f \<circ> g \<circ> f = g \<circ> f; (f \<circ> (g \<circ> f) ^^ n) x = (g ^^ n \<circ> f) x\<rbrakk> \<Longrightarrow> f (g (f (((\<lambda>a. g (f a)) ^^ n) x))) = g ((g ^^ n) (f x)) proof (prove)
goal (1 subgoal):
 1. \<And>x n. \<lbrakk>(f \<circ> (g \<circ> f) ^^ n) x = (g ^^ n \<circ> f) x; (f \<circ> g \<circ> f) (?x3 x n) = (g \<circ> f) (?x3 x n)\<rbrakk> \<Longrightarrow> f (g (f (((\<lambda>a. g (f a)) ^^ n) x))) = g ((g ^^ n) (f x)) proof (prove)
goal (1 subgoal):
 1. \<And>x n. \<lbrakk>f (((\<lambda>a. g (f a)) ^^ n) x) = (g ^^ n) (f x); f (g (f (?x3 x n))) = g (f (?x3 x n))\<rbrakk> \<Longrightarrow> f (g (f (((\<lambda>a. g (f a)) ^^ n) x))) = g ((g ^^ n) (f x)) proof (prove)
goal (1 subgoal):
 1. \<And>x n. f (((\<lambda>a. g (f a)) ^^ n) x) = (g ^^ n) (f x) \<Longrightarrow> g (f (((\<lambda>a. g (f a)) ^^ n) x)) = g ((g ^^ n) (f x)) proof (prove)
goal:
No subgoals!
theory Bits_Int

lemma [code]:
  "bin_split (Suc n) w = (let (w1, w2) = bin_split n (w div 2) in (w1, of_bool (odd w) + 2 * w2))"
  "bin_split 0 w = (w, 0)" by (simp_all add: drop_bit_Suc take_bit_Suc mod_2_eq_odd)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bin_split (Suc n) w = (let (w1, w2) = bin_split n (w div 2) in (w1, of_bool (odd w) + 2 * w2)) &&& bin_split 0 w = (w, 0)
theory Bits_Int

lemma bin_cat_eq_push_bit_add_take_bit:
  \<open>concat_bit n l k = push_bit n k + take_bit n l\<close> by (simp add: concat_bit_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. concat_bit n l k = push_bit n k + take_bit n l
theory Bits_Int

lemma bin_cat_assoc: "(\<lambda>k n l. concat_bit n l k) ((\<lambda>k n l. concat_bit n l k) x m y) n z = (\<lambda>k n l. concat_bit n l k) x (m + n) ((\<lambda>k n l. concat_bit n l k) y n z)" by (fact concat_bit_assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. concat_bit n z (concat_bit m y x) = concat_bit (m + n) (concat_bit n z y) x
theory Bits_Int

lemma bin_cat_assoc_sym: "(\<lambda>k n l. concat_bit n l k) x m ((\<lambda>k n l. concat_bit n l k) y n z) = (\<lambda>k n l. concat_bit n l k) ((\<lambda>k n l. concat_bit n l k) x (m - n) y) (min m n) z" by (fact concat_bit_assoc_sym)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. concat_bit m (concat_bit n z y) x = concat_bit (min m n) z (concat_bit (m - n) y x)
theory Bits_Int

lemma bin_rcat_eq_foldl:
  \<open>bin_rcat n = foldl (\<lambda>u v. (\<lambda>k n l. concat_bit n l k) u n v) 0\<close> proof fix ks :: \<open>int list\<close> show \<open>bin_rcat n ks = foldl (\<lambda>u v. (\<lambda>k n l. concat_bit n l k) u n v) 0 ks\<close> by (induction ks rule: rev_induct)
      (simp_all add: bin_rcat_def concat_bit_eq push_bit_eq_mult) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bin_rcat n = foldl (\<lambda>u v. concat_bit n v u) 0 proof (state)
goal (1 subgoal):
 1. \<And>x. bin_rcat n x = foldl (\<lambda>u v. concat_bit n v u) 0 x proof (state)
goal (1 subgoal):
 1. \<And>x. bin_rcat n x = foldl (\<lambda>u v. concat_bit n v u) 0 x proof (prove)
goal (1 subgoal):
 1. bin_rcat n ks = foldl (\<lambda>u v. concat_bit n v u) 0 ks proof (state)
this:
bin_rcat n ks = foldl (\<lambda>u v. concat_bit n v u) 0 ks

goal:
No subgoals!
theory Bits_Int

lemma bin_nth_cat:
  "(bit :: int \<Rightarrow> nat \<Rightarrow> bool) ((\<lambda>k n l. concat_bit n l k) x k y) n =
    (if n < k then (bit :: int \<Rightarrow> nat \<Rightarrow> bool) y n else (bit :: int \<Rightarrow> nat \<Rightarrow> bool) x (n - k))" by (simp add: bit_concat_bit_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (concat_bit k y x) n = (if n < k then bit y n else bit x (n - k))
theory Bits_Int

lemma bin_nth_drop_bit_iff:
  \<open>(bit :: int \<Rightarrow> nat \<Rightarrow> bool) (drop_bit n c) k \<longleftrightarrow> (bit :: int \<Rightarrow> nat \<Rightarrow> bool) c (n + k)\<close> by (simp add: bit_drop_bit_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (drop_bit n c) k = bit c (n + k)
theory Bits_Int

lemma bin_nth_take_bit_iff:
  \<open>(bit :: int \<Rightarrow> nat \<Rightarrow> bool) (take_bit n c) k \<longleftrightarrow> k < n \<and> (bit :: int \<Rightarrow> nat \<Rightarrow> bool) c k\<close> by (fact bit_take_bit_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (take_bit n c) k = (k < n \<and> bit c k)
theory Bits_Int

lemma bin_nth_split:
  "bin_split n c = (a, b) \<Longrightarrow>
    (\<forall>k. (bit :: int \<Rightarrow> nat \<Rightarrow> bool) a k = (bit :: int \<Rightarrow> nat \<Rightarrow> bool) c (n + k)) \<and>
    (\<forall>k. (bit :: int \<Rightarrow> nat \<Rightarrow> bool) b k = (k < n \<and> (bit :: int \<Rightarrow> nat \<Rightarrow> bool) c k))" by (auto simp add: bin_nth_drop_bit_iff bin_nth_take_bit_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bin_split n c = (a, b) \<Longrightarrow> (\<forall>k. bit a k = bit c (n + k)) \<and> (\<forall>k. bit b k = (k < n \<and> bit c k))
theory Bits_Int

lemma bin_cat_zero [simp]: "(\<lambda>k n l. concat_bit n l k) 0 n w = (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w" by (simp add: bin_cat_eq_push_bit_add_take_bit)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. concat_bit n w 0 = take_bit n w
theory Bits_Int

lemma bintr_cat1: "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (k + n) ((\<lambda>k n l. concat_bit n l k) a n b) = (\<lambda>k n l. concat_bit n l k) ((take_bit :: nat \<Rightarrow> int \<Rightarrow> int) k a) n b" by (metis bin_cat_assoc bin_cat_zero)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. take_bit (k + n) (concat_bit n b a) = concat_bit n b (take_bit k a)
theory Bits_Int

lemma bintr_cat: "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) m ((\<lambda>k n l. concat_bit n l k) a n b) =
    (\<lambda>k n l. concat_bit n l k) ((take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (m - n) a) n ((take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (min m n) b)" by (rule bin_eqI) (auto simp: bin_nth_cat nth_bintr)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. take_bit m (concat_bit n b a) = concat_bit n (take_bit (min m n) b) (take_bit (m - n) a)
theory Bits_Int

lemma bintr_cat_same [simp]: "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n ((\<lambda>k n l. concat_bit n l k) a n b) = (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n b" by (auto simp add : bintr_cat)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. take_bit n (concat_bit n b a) = take_bit n b
theory Bits_Int

lemma cat_bintr [simp]: "(\<lambda>k n l. concat_bit n l k) a n ((take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n b) = (\<lambda>k n l. concat_bit n l k) a n b" by (simp add: bin_cat_eq_push_bit_add_take_bit)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. concat_bit n (take_bit n b) a = concat_bit n b a
theory Bits_Int

lemma bin_cat_split: "bin_split n w = (u, v) \<Longrightarrow> w = (\<lambda>k n l. concat_bit n l k) u n v" by (auto simp add: bin_cat_eq_push_bit_add_take_bit bits_ident)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bin_split n w = (u, v) \<Longrightarrow> w = concat_bit n v u
theory Bits_Int

lemma drop_bit_bin_cat_eq:
  \<open>drop_bit n ((\<lambda>k n l. concat_bit n l k) v n w) = v\<close> by (rule bit_eqI) (simp add: bit_drop_bit_eq bit_concat_bit_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. drop_bit n (concat_bit n w v) = v
theory Bits_Int

lemma take_bit_bin_cat_eq:
  \<open>take_bit n ((\<lambda>k n l. concat_bit n l k) v n w) = take_bit n w\<close> by (rule bit_eqI) (simp add: bit_concat_bit_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. take_bit n (concat_bit n w v) = take_bit n w
theory Bits_Int

lemma bin_split_cat: "bin_split n ((\<lambda>k n l. concat_bit n l k) v n w) = (v, (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w)" by (simp add: drop_bit_bin_cat_eq take_bit_bin_cat_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bin_split n (concat_bit n w v) = (v, take_bit n w)
theory Bits_Int

lemma bin_split_minus1 [simp]:
  "bin_split n (- 1) = (- 1, (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n (- 1))" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bin_split n (- 1) = (- 1, take_bit n (- 1))
theory Bits_Int

lemma bin_split_trunc:
  "bin_split (min m n) c = (a, b) \<Longrightarrow>
    bin_split n ((take_bit :: nat \<Rightarrow> int \<Rightarrow> int) m c) = ((take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (m - n) a, b)" apply (induct n arbitrary: m b c, clarsimp) apply (simp add: bin_rest_trunc Let_def split: prod.split_asm) apply (case_tac m) apply (auto simp: Let_def drop_bit_Suc take_bit_Suc mod_2_eq_odd split: prod.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bin_split (min m n) c = (a, b) \<Longrightarrow> bin_split n (take_bit m c) = (take_bit (m - n) a, b) proof (prove)
goal (1 subgoal):
 1. \<And>n m b c. \<lbrakk>\<And>m b c. bin_split (min m n) c = (a, b) \<Longrightarrow> bin_split n (take_bit m c) = (take_bit (m - n) a, b); bin_split (min m (Suc n)) c = (a, b)\<rbrakk> \<Longrightarrow> bin_split (Suc n) (take_bit m c) = (take_bit (m - Suc n) a, b) proof (prove)
goal (1 subgoal):
 1. \<And>n m c. \<lbrakk>\<And>m c. drop_bit (min m n) c = a \<Longrightarrow> drop_bit n (take_bit m c) = take_bit (m - n) a \<and> take_bit (min n m) c = take_bit (min m n) c; drop_bit (min m (Suc n)) c = a\<rbrakk> \<Longrightarrow> drop_bit (Suc n) (take_bit m c) = take_bit (m - Suc n) a \<and> take_bit (min (Suc n) m) c = take_bit (min m (Suc n)) c proof (prove)
goal (2 subgoals):
 1. \<And>n m c. \<lbrakk>\<And>m c. drop_bit (min m n) c = a \<Longrightarrow> drop_bit n (take_bit m c) = take_bit (m - n) a \<and> take_bit (min n m) c = take_bit (min m n) c; drop_bit (min m (Suc n)) c = a; m = 0\<rbrakk> \<Longrightarrow> drop_bit (Suc n) (take_bit m c) = take_bit (m - Suc n) a \<and> take_bit (min (Suc n) m) c = take_bit (min m (Suc n)) c
 2. \<And>n m c nat. \<lbrakk>\<And>m c. drop_bit (min m n) c = a \<Longrightarrow> drop_bit n (take_bit m c) = take_bit (m - n) a \<and> take_bit (min n m) c = take_bit (min m n) c; drop_bit (min m (Suc n)) c = a; m = Suc nat\<rbrakk> \<Longrightarrow> drop_bit (Suc n) (take_bit m c) = take_bit (m - Suc n) a \<and> take_bit (min (Suc n) m) c = take_bit (min m (Suc n)) c proof (prove)
goal:
No subgoals!
theory Bits_Int

lemma bin_split_trunc1:
  "bin_split n c = (a, b) \<Longrightarrow>
    bin_split n ((take_bit :: nat \<Rightarrow> int \<Rightarrow> int) m c) = ((take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (m - n) a, (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) m b)" apply (induct n arbitrary: m b c, clarsimp) apply (simp add: bin_rest_trunc Let_def split: prod.split_asm) apply (case_tac m) apply (auto simp: Let_def drop_bit_Suc take_bit_Suc mod_2_eq_odd split: prod.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bin_split n c = (a, b) \<Longrightarrow> bin_split n (take_bit m c) = (take_bit (m - n) a, take_bit m b) proof (prove)
goal (1 subgoal):
 1. \<And>n m b c. \<lbrakk>\<And>m b c. bin_split n c = (a, b) \<Longrightarrow> bin_split n (take_bit m c) = (take_bit (m - n) a, take_bit m b); bin_split (Suc n) c = (a, b)\<rbrakk> \<Longrightarrow> bin_split (Suc n) (take_bit m c) = (take_bit (m - Suc n) a, take_bit m b) proof (prove)
goal (1 subgoal):
 1. \<And>n m c. \<lbrakk>\<And>m c. drop_bit n c = a \<Longrightarrow> drop_bit n (take_bit m c) = take_bit (m - n) a \<and> take_bit (min n m) c = take_bit (min m n) c; drop_bit (Suc n) c = a\<rbrakk> \<Longrightarrow> drop_bit (Suc n) (take_bit m c) = take_bit (m - Suc n) a \<and> take_bit (min (Suc n) m) c = take_bit (min m (Suc n)) c proof (prove)
goal (2 subgoals):
 1. \<And>n m c. \<lbrakk>\<And>m c. drop_bit n c = a \<Longrightarrow> drop_bit n (take_bit m c) = take_bit (m - n) a \<and> take_bit (min n m) c = take_bit (min m n) c; drop_bit (Suc n) c = a; m = 0\<rbrakk> \<Longrightarrow> drop_bit (Suc n) (take_bit m c) = take_bit (m - Suc n) a \<and> take_bit (min (Suc n) m) c = take_bit (min m (Suc n)) c
 2. \<And>n m c nat. \<lbrakk>\<And>m c. drop_bit n c = a \<Longrightarrow> drop_bit n (take_bit m c) = take_bit (m - n) a \<and> take_bit (min n m) c = take_bit (min m n) c; drop_bit (Suc n) c = a; m = Suc nat\<rbrakk> \<Longrightarrow> drop_bit (Suc n) (take_bit m c) = take_bit (m - Suc n) a \<and> take_bit (min (Suc n) m) c = take_bit (min m (Suc n)) c proof (prove)
goal:
No subgoals!
theory Bits_Int

lemma bin_cat_num: "(\<lambda>k n l. concat_bit n l k) a n b = a * 2 ^ n + (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n b" by (simp add: bin_cat_eq_push_bit_add_take_bit push_bit_eq_mult)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. concat_bit n b a = a * 2 ^ n + take_bit n b
theory Bits_Int

lemma bin_split_num: "bin_split n b = (b div 2 ^ n, b mod 2 ^ n)" by (simp add: drop_bit_eq_div take_bit_eq_mod)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bin_split n b = (b div 2 ^ n, b mod 2 ^ n)
theory Bits_Int

lemma bin_rsplit_aux_append: "bin_rsplit_aux n m c (bs @ cs) = bin_rsplit_aux n m c bs @ cs" apply (induct n m c bs rule: bin_rsplit_aux.induct) apply (subst bin_rsplit_aux.simps) apply (subst bin_rsplit_aux.simps) apply (clarsimp split: prod.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bin_rsplit_aux n m c (bs @ cs) = bin_rsplit_aux n m c bs @ cs proof (prove)
goal (1 subgoal):
 1. \<And>n m c bs. (\<And>x xa y. \<lbrakk>\<not> (m = 0 \<or> n = 0); x = bin_split n c; (xa, y) = x\<rbrakk> \<Longrightarrow> bin_rsplit_aux n (m - n) xa ((y # bs) @ cs) = bin_rsplit_aux n (m - n) xa (y # bs) @ cs) \<Longrightarrow> bin_rsplit_aux n m c (bs @ cs) = bin_rsplit_aux n m c bs @ cs proof (prove)
goal (1 subgoal):
 1. \<And>n m c bs. (\<And>x xa y. \<lbrakk>\<not> (m = 0 \<or> n = 0); x = bin_split n c; (xa, y) = x\<rbrakk> \<Longrightarrow> bin_rsplit_aux n (m - n) xa ((y # bs) @ cs) = bin_rsplit_aux n (m - n) xa (y # bs) @ cs) \<Longrightarrow> (if m = 0 \<or> n = 0 then bs @ cs else let (a, b) = bin_split n c in bin_rsplit_aux n (m - n) a (b # bs @ cs)) = bin_rsplit_aux n m c bs @ cs proof (prove)
goal (1 subgoal):
 1. \<And>n m c bs. (\<And>x xa y. \<lbrakk>\<not> (m = 0 \<or> n = 0); x = bin_split n c; (xa, y) = x\<rbrakk> \<Longrightarrow> bin_rsplit_aux n (m - n) xa ((y # bs) @ cs) = bin_rsplit_aux n (m - n) xa (y # bs) @ cs) \<Longrightarrow> (if m = 0 \<or> n = 0 then bs @ cs else let (a, b) = bin_split n c in if m - n = 0 \<or> n = 0 then b # bs @ cs else let (a, ba) = bin_split n a in bin_rsplit_aux n (m - n - n) a (ba # b # bs @ cs)) = bin_rsplit_aux n m c bs @ cs proof (prove)
goal:
No subgoals!
theory Bits_Int

lemma bin_rsplitl_aux_append: "bin_rsplitl_aux n m c (bs @ cs) = bin_rsplitl_aux n m c bs @ cs" apply (induct n m c bs rule: bin_rsplitl_aux.induct) apply (subst bin_rsplitl_aux.simps) apply (subst bin_rsplitl_aux.simps) apply (clarsimp split: prod.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bin_rsplitl_aux n m c (bs @ cs) = bin_rsplitl_aux n m c bs @ cs proof (prove)
goal (1 subgoal):
 1. \<And>n m c bs. (\<And>x xa y. \<lbrakk>\<not> (m = 0 \<or> n = 0); x = bin_split (min m n) c; (xa, y) = x\<rbrakk> \<Longrightarrow> bin_rsplitl_aux n (m - n) xa ((y # bs) @ cs) = bin_rsplitl_aux n (m - n) xa (y # bs) @ cs) \<Longrightarrow> bin_rsplitl_aux n m c (bs @ cs) = bin_rsplitl_aux n m c bs @ cs proof (prove)
goal (1 subgoal):
 1. \<And>n m c bs. (\<And>x xa y. \<lbrakk>\<not> (m = 0 \<or> n = 0); x = bin_split (min m n) c; (xa, y) = x\<rbrakk> \<Longrightarrow> bin_rsplitl_aux n (m - n) xa ((y # bs) @ cs) = bin_rsplitl_aux n (m - n) xa (y # bs) @ cs) \<Longrightarrow> (if m = 0 \<or> n = 0 then bs @ cs else let (a, b) = bin_split (min m n) c in bin_rsplitl_aux n (m - n) a (b # bs @ cs)) = bin_rsplitl_aux n m c bs @ cs proof (prove)
goal (1 subgoal):
 1. \<And>n m c bs. (\<And>x xa y. \<lbrakk>\<not> (m = 0 \<or> n = 0); x = bin_split (min m n) c; (xa, y) = x\<rbrakk> \<Longrightarrow> bin_rsplitl_aux n (m - n) xa ((y # bs) @ cs) = bin_rsplitl_aux n (m - n) xa (y # bs) @ cs) \<Longrightarrow> (if m = 0 \<or> n = 0 then bs @ cs else let (a, b) = bin_split (min m n) c in if m - n = 0 \<or> n = 0 then b # bs @ cs else let (a, ba) = bin_split (min (m - n) n) a in bin_rsplitl_aux n (m - n - n) a (ba # b # bs @ cs)) = bin_rsplitl_aux n m c bs @ cs proof (prove)
goal:
No subgoals!
theory Bits_Int

lemma bin_split_minus: "0 < n \<Longrightarrow> bin_split (Suc (n - 1)) w = bin_split n w" by auto

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

lemma bin_rsplit_aux_simp_alt:
  "bin_rsplit_aux n m c bs =
    (if m = 0 \<or> n = 0 then bs
     else let (a, b) = bin_split n c in bin_rsplit n (m - n, a) @ b # bs)" apply (simp add: bin_rsplit_aux.simps [of n m c bs]) apply (subst rsplit_aux_alts) apply (simp add: bin_rsplit_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bin_rsplit_aux n m c bs = (if m = 0 \<or> n = 0 then bs else let (a, b) = bin_split n c in bin_rsplit n (m - n, a) @ b # bs) proof (prove)
goal (1 subgoal):
 1. 0 < m \<and> 0 < n \<longrightarrow> bin_rsplit_aux n (m - n) (drop_bit n c) (take_bit n c # bs) = bin_rsplit n (m - n, drop_bit n c) @ take_bit n c # bs proof (prove)
goal (1 subgoal):
 1. 0 < m \<and> 0 < n \<longrightarrow> bin_rsplit_aux n (m - n) (drop_bit n c) [] @ take_bit n c # bs = bin_rsplit n (m - n, drop_bit n c) @ take_bit n c # bs proof (prove)
goal:
No subgoals!
theory Bits_Int

lemma bin_rsplit_size_sign' [rule_format]:
  "n > 0 \<Longrightarrow> rev sw = bin_rsplit n (nw, w) \<Longrightarrow> \<forall>v\<in>set sw. (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n v = v" apply (induct sw arbitrary: nw w) apply clarsimp apply clarsimp apply (drule bthrs) apply (simp (no_asm_use) add: Let_def split: prod.split_asm if_split_asm) apply clarify apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; rev sw = bin_rsplit n (nw, w)\<rbrakk> \<Longrightarrow> \<forall>v\<in>set sw. take_bit n v = v proof (prove)
goal (2 subgoals):
 1. \<And>nw w. \<lbrakk>0 < n; rev [] = bin_rsplit n (nw, w)\<rbrakk> \<Longrightarrow> \<forall>v\<in>set []. take_bit n v = v
 2. \<And>a sw nw w. \<lbrakk>\<And>nw w. \<lbrakk>0 < n; rev sw = bin_rsplit n (nw, w)\<rbrakk> \<Longrightarrow> \<forall>v\<in>set sw. take_bit n v = v; 0 < n; rev (a # sw) = bin_rsplit n (nw, w)\<rbrakk> \<Longrightarrow> \<forall>v\<in>set (a # sw). take_bit n v = v proof (prove)
goal (1 subgoal):
 1. \<And>a sw nw w. \<lbrakk>\<And>nw w. \<lbrakk>0 < n; rev sw = bin_rsplit n (nw, w)\<rbrakk> \<Longrightarrow> \<forall>v\<in>set sw. take_bit n v = v; 0 < n; rev (a # sw) = bin_rsplit n (nw, w)\<rbrakk> \<Longrightarrow> \<forall>v\<in>set (a # sw). take_bit n v = v proof (prove)
goal (1 subgoal):
 1. \<And>a sw nw w. \<lbrakk>\<And>nw w. rev sw = bin_rsplit n (nw, w) \<Longrightarrow> \<forall>v\<in>set sw. take_bit n v = v; 0 < n; rev sw @ [a] = bin_rsplit n (nw, w)\<rbrakk> \<Longrightarrow> take_bit n a = a \<and> (\<forall>v\<in>set sw. take_bit n v = v) proof (prove)
goal (1 subgoal):
 1. \<And>a sw nw w. \<lbrakk>\<And>nw w. rev sw = bin_rsplit n (nw, w) \<Longrightarrow> \<forall>v\<in>set sw. take_bit n v = v; 0 < n; rev sw @ [a] = (if fst (nw, w) = 0 \<or> n = 0 then [] else let (a, b) = bin_split n (snd (nw, w)) in bin_rsplit n (fst (nw, w) - n, a) @ [b])\<rbrakk> \<Longrightarrow> take_bit n a = a \<and> (\<forall>v\<in>set sw. take_bit n v = v) proof (prove)
goal (1 subgoal):
 1. \<And>sw nw w. \<lbrakk>\<And>nw w. rev sw = bin_rsplit n (nw, w) \<Longrightarrow> \<forall>v\<in>set sw. take_bit n v = v; 0 < n; 0 < nw \<and> 0 < n; rev sw = bin_rsplit n (nw - n, drop_bit n w)\<rbrakk> \<Longrightarrow> \<forall>v\<in>set sw. take_bit n v = v proof (prove)
goal (1 subgoal):
 1. \<And>sw nw w v. \<lbrakk>\<And>nw w. rev sw = bin_rsplit n (nw, w) \<Longrightarrow> \<forall>v\<in>set sw. take_bit n v = v; 0 < n; rev sw = bin_rsplit n (nw - n, drop_bit n w); v \<in> set sw; 0 < nw; 0 < n\<rbrakk> \<Longrightarrow> take_bit n v = v proof (prove)
goal:
No subgoals!
theory Bits_Int

lemma bin_rsplit_all: "0 < nw \<Longrightarrow> nw \<le> n \<Longrightarrow> bin_rsplit n (nw, w) = [(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w]" by (auto simp: bin_rsplit_def rsplit_aux_simp2ls split: prod.split dest!: split_bintrunc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < nw; nw \<le> n\<rbrakk> \<Longrightarrow> bin_rsplit n (nw, w) = [take_bit n w]