theory Bitwise

lemma rev_bl_order_simps:
  "rev_bl_order F [] [] = F"
  "rev_bl_order F (x # xs) (y # ys) = rev_bl_order ((y \<and> \<not> x) \<or> ((y \<or> \<not> x) \<and> F)) xs ys" apply (simp_all add: rev_bl_order_def) apply (rule conj_cong[OF refl]) apply (cases "xs = ys") apply (simp add: nth_Cons') apply blast apply (simp add: nth_Cons') apply safe apply (rule_tac x="n - 1" in exI) apply simp apply (rule_tac x="Suc n" in exI) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rev_bl_order F [] [] = F &&& rev_bl_order F (x # xs) (y # ys) = rev_bl_order (y \<and> \<not> x \<or> (y \<or> \<not> x) \<and> F) xs ys proof (prove)
goal (1 subgoal):
 1. (length xs = length ys \<and> (x = y \<and> xs = ys \<and> F \<or> (\<exists>n<Suc (length xs). drop n xs = drop n ys \<and> \<not> (x # xs) ! n \<and> (y # ys) ! n))) = (length xs = length ys \<and> (xs = ys \<and> (y \<and> \<not> x \<or> (y \<or> \<not> x) \<and> F) \<or> (\<exists>n<length xs. drop (Suc n) xs = drop (Suc n) ys \<and> \<not> xs ! n \<and> ys ! n))) proof (prove)
goal (1 subgoal):
 1. length xs = length ys \<Longrightarrow> (x = y \<and> xs = ys \<and> F \<or> (\<exists>n<Suc (length xs). drop n xs = drop n ys \<and> \<not> (x # xs) ! n \<and> (y # ys) ! n)) = (xs = ys \<and> (y \<and> \<not> x \<or> (y \<or> \<not> x) \<and> F) \<or> (\<exists>n<length xs. drop (Suc n) xs = drop (Suc n) ys \<and> \<not> xs ! n \<and> ys ! n)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>length xs = length ys; xs = ys\<rbrakk> \<Longrightarrow> (x = y \<and> xs = ys \<and> F \<or> (\<exists>n<Suc (length xs). drop n xs = drop n ys \<and> \<not> (x # xs) ! n \<and> (y # ys) ! n)) = (xs = ys \<and> (y \<and> \<not> x \<or> (y \<or> \<not> x) \<and> F) \<or> (\<exists>n<length xs. drop (Suc n) xs = drop (Suc n) ys \<and> \<not> xs ! n \<and> ys ! n))
 2. \<lbrakk>length xs = length ys; xs \<noteq> ys\<rbrakk> \<Longrightarrow> (x = y \<and> xs = ys \<and> F \<or> (\<exists>n<Suc (length xs). drop n xs = drop n ys \<and> \<not> (x # xs) ! n \<and> (y # ys) ! n)) = (xs = ys \<and> (y \<and> \<not> x \<or> (y \<or> \<not> x) \<and> F) \<or> (\<exists>n<length xs. drop (Suc n) xs = drop (Suc n) ys \<and> \<not> xs ! n \<and> ys ! n)) proof (prove)
goal (2 subgoals):
 1. xs = ys \<Longrightarrow> (x = y \<and> F \<or> \<not> x \<and> y) = (y \<and> \<not> x \<or> (y \<or> \<not> x) \<and> F)
 2. \<lbrakk>length xs = length ys; xs \<noteq> ys\<rbrakk> \<Longrightarrow> (x = y \<and> xs = ys \<and> F \<or> (\<exists>n<Suc (length xs). drop n xs = drop n ys \<and> \<not> (x # xs) ! n \<and> (y # ys) ! n)) = (xs = ys \<and> (y \<and> \<not> x \<or> (y \<or> \<not> x) \<and> F) \<or> (\<exists>n<length xs. drop (Suc n) xs = drop (Suc n) ys \<and> \<not> xs ! n \<and> ys ! n)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length xs = length ys; xs \<noteq> ys\<rbrakk> \<Longrightarrow> (x = y \<and> xs = ys \<and> F \<or> (\<exists>n<Suc (length xs). drop n xs = drop n ys \<and> \<not> (x # xs) ! n \<and> (y # ys) ! n)) = (xs = ys \<and> (y \<and> \<not> x \<or> (y \<or> \<not> x) \<and> F) \<or> (\<exists>n<length xs. drop (Suc n) xs = drop (Suc n) ys \<and> \<not> xs ! n \<and> ys ! n)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length xs = length ys; xs \<noteq> ys\<rbrakk> \<Longrightarrow> (\<exists>n>0. 0 < n \<longrightarrow> n < Suc (length ys) \<and> drop n xs = drop n ys \<and> \<not> xs ! (n - Suc 0) \<and> ys ! (n - Suc 0)) = (\<exists>n<length ys. drop (Suc n) xs = drop (Suc n) ys \<and> \<not> xs ! n \<and> ys ! n) proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>length xs = length ys; xs \<noteq> ys; 0 < n; n < Suc (length ys); drop n xs = drop n ys; \<not> xs ! (n - Suc 0); ys ! (n - Suc 0)\<rbrakk> \<Longrightarrow> \<exists>n<length ys. drop (Suc n) xs = drop (Suc n) ys \<and> \<not> xs ! n \<and> ys ! n
 2. \<And>n. \<lbrakk>length xs = length ys; xs \<noteq> ys; n < length ys; drop (Suc n) xs = drop (Suc n) ys; \<not> xs ! n; ys ! n\<rbrakk> \<Longrightarrow> \<exists>n>0. 0 < n \<longrightarrow> n < Suc (length ys) \<and> drop n xs = drop n ys \<and> \<not> xs ! (n - Suc 0) \<and> ys ! (n - Suc 0) proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>length xs = length ys; xs \<noteq> ys; 0 < n; n < Suc (length ys); drop n xs = drop n ys; \<not> xs ! (n - Suc 0); ys ! (n - Suc 0)\<rbrakk> \<Longrightarrow> n - 1 < length ys \<and> drop (Suc (n - 1)) xs = drop (Suc (n - 1)) ys \<and> \<not> xs ! (n - 1) \<and> ys ! (n - 1)
 2. \<And>n. \<lbrakk>length xs = length ys; xs \<noteq> ys; n < length ys; drop (Suc n) xs = drop (Suc n) ys; \<not> xs ! n; ys ! n\<rbrakk> \<Longrightarrow> \<exists>n>0. 0 < n \<longrightarrow> n < Suc (length ys) \<and> drop n xs = drop n ys \<and> \<not> xs ! (n - Suc 0) \<and> ys ! (n - Suc 0) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>length xs = length ys; xs \<noteq> ys; n < length ys; drop (Suc n) xs = drop (Suc n) ys; \<not> xs ! n; ys ! n\<rbrakk> \<Longrightarrow> \<exists>n>0. 0 < n \<longrightarrow> n < Suc (length ys) \<and> drop n xs = drop n ys \<and> \<not> xs ! (n - Suc 0) \<and> ys ! (n - Suc 0) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>length xs = length ys; xs \<noteq> ys; n < length ys; drop (Suc n) xs = drop (Suc n) ys; \<not> xs ! n; ys ! n\<rbrakk> \<Longrightarrow> 0 < Suc n \<and> (0 < Suc n \<longrightarrow> Suc n < Suc (length ys) \<and> drop (Suc n) xs = drop (Suc n) ys \<and> \<not> xs ! (Suc n - Suc 0) \<and> ys ! (Suc n - Suc 0)) proof (prove)
goal:
No subgoals!