theory Bitwise

lemma word_sless_rbl:
  "x <s y \<longleftrightarrow> rev_bl_order False (map_last Not (rev (to_bl x))) (map_last Not (rev (to_bl y)))" using word_msb_alt[where w=x] word_msb_alt[where w=y] apply (simp add: word_sless_msb_less word_less_rbl) apply (subgoal_tac "length (to_bl x) = length (to_bl y)") apply (cases "to_bl x", simp) apply (cases "to_bl y", simp) apply (clarsimp simp: map_last_def rev_bl_order_rev_simp) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x <s y) = rev_bl_order False (map_last Not (rev (to_bl x))) (map_last Not (rev (to_bl y))) proof (prove)
using this:
msb x = hd (to_bl x)
msb y = hd (to_bl y)

goal (1 subgoal):
 1. (x <s y) = rev_bl_order False (map_last Not (rev (to_bl x))) (map_last Not (rev (to_bl y))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>msb x = hd (to_bl x); msb y = hd (to_bl y)\<rbrakk> \<Longrightarrow> ((hd (to_bl y) \<longrightarrow> hd (to_bl x)) \<and> (hd (to_bl x) \<and> \<not> hd (to_bl y) \<or> rev_bl_order False (rev (to_bl x)) (rev (to_bl y)))) = rev_bl_order False (map_last Not (rev (to_bl x))) (map_last Not (rev (to_bl y))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>msb x = hd (to_bl x); msb y = hd (to_bl y); length (to_bl x) = length (to_bl y)\<rbrakk> \<Longrightarrow> ((hd (to_bl y) \<longrightarrow> hd (to_bl x)) \<and> (hd (to_bl x) \<and> \<not> hd (to_bl y) \<or> rev_bl_order False (rev (to_bl x)) (rev (to_bl y)))) = rev_bl_order False (map_last Not (rev (to_bl x))) (map_last Not (rev (to_bl y)))
 2. \<lbrakk>msb x = hd (to_bl x); msb y = hd (to_bl y)\<rbrakk> \<Longrightarrow> length (to_bl x) = length (to_bl y) proof (prove)
goal (2 subgoals):
 1. \<And>a list. \<lbrakk>msb x = hd (to_bl x); msb y = hd (to_bl y); length (to_bl x) = length (to_bl y); to_bl x = a # list\<rbrakk> \<Longrightarrow> ((hd (to_bl y) \<longrightarrow> hd (to_bl x)) \<and> (hd (to_bl x) \<and> \<not> hd (to_bl y) \<or> rev_bl_order False (rev (to_bl x)) (rev (to_bl y)))) = rev_bl_order False (map_last Not (rev (to_bl x))) (map_last Not (rev (to_bl y)))
 2. \<lbrakk>msb x = hd (to_bl x); msb y = hd (to_bl y)\<rbrakk> \<Longrightarrow> length (to_bl x) = length (to_bl y) proof (prove)
goal (2 subgoals):
 1. \<And>a list aa lista. \<lbrakk>msb x = hd (to_bl x); msb y = hd (to_bl y); length (to_bl x) = length (to_bl y); to_bl x = a # list; to_bl y = aa # lista\<rbrakk> \<Longrightarrow> ((hd (to_bl y) \<longrightarrow> hd (to_bl x)) \<and> (hd (to_bl x) \<and> \<not> hd (to_bl y) \<or> rev_bl_order False (rev (to_bl x)) (rev (to_bl y)))) = rev_bl_order False (map_last Not (rev (to_bl x))) (map_last Not (rev (to_bl y)))
 2. \<lbrakk>msb x = hd (to_bl x); msb y = hd (to_bl y)\<rbrakk> \<Longrightarrow> length (to_bl x) = length (to_bl y) proof (prove)
goal (2 subgoals):
 1. \<And>list lista. \<lbrakk>length list = length lista; to_bl x = msb x # list; to_bl y = msb y # lista\<rbrakk> \<Longrightarrow> ((msb y \<longrightarrow> msb x) \<and> (msb x \<and> \<not> msb y \<or> msb y \<and> \<not> msb x \<or> (msb y \<or> \<not> msb x) \<and> rev_bl_order False (rev list) (rev lista))) = (\<not> msb y \<and> msb x \<or> (msb y \<longrightarrow> msb x) \<and> rev_bl_order False (rev list) (rev lista))
 2. \<lbrakk>msb x = hd (to_bl x); msb y = hd (to_bl y)\<rbrakk> \<Longrightarrow> length (to_bl x) = length (to_bl y) proof (prove)
goal:
No subgoals!