theory Most_significant_bit

lemma msb_big:
  \<open>msb a \<longleftrightarrow> 2 ^ (LENGTH('a) - Suc 0) \<le> a\<close>
  for a :: \<open>'a::len word\<close> using bang_is_le [of a \<open>LENGTH('a) - Suc 0\<close>] apply (auto simp add: msb_nth word_le_not_less) apply (rule ccontr) apply (erule notE) apply (rule ccontr) apply (clarsimp simp: not_less) apply (subgoal_tac "a = take_bit (LENGTH('a) - Suc 0) a") apply (cut_tac and_mask_less' [where w=a and n="LENGTH('a) - Suc 0"]) apply auto apply (simp flip: take_bit_eq_mask) apply (rule sym) apply (simp add: take_bit_eq_self_iff_drop_bit_eq_0 drop_bit_eq_zero_iff_not_bit_last) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. msb a = (2 ^ (LENGTH('a) - Suc 0) \<le> a) proof (prove)
using this:
bit a (LENGTH('a) - Suc 0) \<Longrightarrow> 2 ^ (LENGTH('a) - Suc 0) \<le> a

goal (1 subgoal):
 1. msb a = (2 ^ (LENGTH('a) - Suc 0) \<le> a) proof (prove)
goal (1 subgoal):
 1. \<not> a < 2 ^ (LENGTH('a) - Suc 0) \<Longrightarrow> bit a (LENGTH('a) - Suc 0) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> a < 2 ^ (LENGTH('a) - Suc 0); \<not> bit a (LENGTH('a) - Suc 0)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<not> bit a (LENGTH('a) - Suc 0) \<Longrightarrow> a < 2 ^ (LENGTH('a) - Suc 0) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> bit a (LENGTH('a) - Suc 0); \<not> a < 2 ^ (LENGTH('a) - Suc 0)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> bit a (LENGTH('a) - Suc 0); 2 ^ (LENGTH('a) - Suc 0) \<le> a\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> bit a (LENGTH('a) - Suc 0); 2 ^ (LENGTH('a) - Suc 0) \<le> a; a = take_bit (LENGTH('a) - Suc 0) a\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>\<not> bit a (LENGTH('a) - Suc 0); 2 ^ (LENGTH('a) - Suc 0) \<le> a\<rbrakk> \<Longrightarrow> a = take_bit (LENGTH('a) - Suc 0) a proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<not> bit a (LENGTH('a) - Suc 0); 2 ^ (LENGTH('a) - Suc 0) \<le> a; a = take_bit (LENGTH('a) - Suc 0) a; and a (mask (LENGTH('a) - Suc 0)) < 2 ^ (LENGTH('a) - Suc 0)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>\<not> bit a (LENGTH('a) - Suc 0); 2 ^ (LENGTH('a) - Suc 0) \<le> a; a = take_bit (LENGTH('a) - Suc 0) a\<rbrakk> \<Longrightarrow> LENGTH('a) - Suc 0 < LENGTH('a)
 3. \<lbrakk>\<not> bit a (LENGTH('a) - Suc 0); 2 ^ (LENGTH('a) - Suc 0) \<le> a\<rbrakk> \<Longrightarrow> a = take_bit (LENGTH('a) - Suc 0) a proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> bit a (LENGTH('a) - Suc 0); 2 ^ (LENGTH('a) - Suc 0) \<le> a; a = take_bit (LENGTH('a) - Suc 0) a; and a (mask (LENGTH('a) - Suc 0)) < 2 ^ (LENGTH('a) - Suc 0)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>\<not> bit a (LENGTH('a) - Suc 0); 2 ^ (LENGTH('a) - Suc 0) \<le> a\<rbrakk> \<Longrightarrow> a = take_bit (LENGTH('a) - Suc 0) a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> bit a (LENGTH('a) - Suc 0); 2 ^ (LENGTH('a) - Suc 0) \<le> a\<rbrakk> \<Longrightarrow> a = take_bit (LENGTH('a) - Suc 0) a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> bit a (LENGTH('a) - Suc 0); 2 ^ (LENGTH('a) - Suc 0) \<le> a\<rbrakk> \<Longrightarrow> take_bit (LENGTH('a) - Suc 0) a = a proof (prove)
goal:
No subgoals!