theory More_Word

lemma sint_of_nat_le:
  "\<lbrakk> b < 2 ^ (LENGTH('a) - 1); a \<le> b \<rbrakk>
   \<Longrightarrow> sint (of_nat a :: 'a :: len word) \<le> sint (of_nat b :: 'a :: len word)" apply (cases \<open>LENGTH('a)\<close>) apply simp_all apply transfer apply (subst signed_take_bit_eq_if_positive) apply (simp add: bit_simps) apply (metis bit_take_bit_iff nat_less_le order_less_le_trans take_bit_nat_eq_self_iff) apply (subst signed_take_bit_eq_if_positive) apply (simp add: bit_simps) apply (metis bit_take_bit_iff nat_less_le take_bit_nat_eq_self_iff) apply (simp flip: of_nat_take_bit add: take_bit_nat_eq_self) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b < 2 ^ (LENGTH('a) - 1); a \<le> b\<rbrakk> \<Longrightarrow> sint (word_of_nat a) \<le> sint (word_of_nat b) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>b < 2 ^ (LENGTH('a) - 1); a \<le> b; LENGTH('a) = 0\<rbrakk> \<Longrightarrow> sint (word_of_nat a) \<le> sint (word_of_nat b)
 2. \<And>nat. \<lbrakk>b < 2 ^ (LENGTH('a) - 1); a \<le> b; LENGTH('a) = Suc nat\<rbrakk> \<Longrightarrow> sint (word_of_nat a) \<le> sint (word_of_nat b) proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>b < 2 ^ nat; a \<le> b; LENGTH('a) = Suc nat\<rbrakk> \<Longrightarrow> sint (word_of_nat a) \<le> sint (word_of_nat b) proof (prove)
goal (1 subgoal):
 1. \<And>nat b a. \<lbrakk>b < 2 ^ nat; a \<le> b; LENGTH('a) = Suc nat\<rbrakk> \<Longrightarrow> signed_take_bit (LENGTH('a) - Suc 0) (int a) \<le> signed_take_bit (LENGTH('a) - Suc 0) (int b) proof (prove)
goal (2 subgoals):
 1. \<And>nat b a. \<lbrakk>b < 2 ^ nat; a \<le> b; LENGTH('a) = Suc nat\<rbrakk> \<Longrightarrow> \<not> bit (int a) (LENGTH('a) - Suc 0)
 2. \<And>nat b a. \<lbrakk>b < 2 ^ nat; a \<le> b; LENGTH('a) = Suc nat\<rbrakk> \<Longrightarrow> take_bit (LENGTH('a) - Suc 0) (int a) \<le> signed_take_bit (LENGTH('a) - Suc 0) (int b) proof (prove)
goal (2 subgoals):
 1. \<And>nat b a. \<lbrakk>b < 2 ^ nat; a \<le> b; LENGTH('a) = Suc nat\<rbrakk> \<Longrightarrow> \<not> bit a nat
 2. \<And>nat b a. \<lbrakk>b < 2 ^ nat; a \<le> b; LENGTH('a) = Suc nat\<rbrakk> \<Longrightarrow> take_bit (LENGTH('a) - Suc 0) (int a) \<le> signed_take_bit (LENGTH('a) - Suc 0) (int b) proof (prove)
goal (1 subgoal):
 1. \<And>nat b a. \<lbrakk>b < 2 ^ nat; a \<le> b; LENGTH('a) = Suc nat\<rbrakk> \<Longrightarrow> take_bit (LENGTH('a) - Suc 0) (int a) \<le> signed_take_bit (LENGTH('a) - Suc 0) (int b) proof (prove)
goal (2 subgoals):
 1. \<And>nat b a. \<lbrakk>b < 2 ^ nat; a \<le> b; LENGTH('a) = Suc nat\<rbrakk> \<Longrightarrow> \<not> bit (int b) (LENGTH('a) - Suc 0)
 2. \<And>nat b a. \<lbrakk>b < 2 ^ nat; a \<le> b; LENGTH('a) = Suc nat\<rbrakk> \<Longrightarrow> take_bit (LENGTH('a) - Suc 0) (int a) \<le> take_bit (LENGTH('a) - Suc 0) (int b) proof (prove)
goal (2 subgoals):
 1. \<And>nat b a. \<lbrakk>b < 2 ^ nat; a \<le> b; LENGTH('a) = Suc nat\<rbrakk> \<Longrightarrow> \<not> bit b nat
 2. \<And>nat b a. \<lbrakk>b < 2 ^ nat; a \<le> b; LENGTH('a) = Suc nat\<rbrakk> \<Longrightarrow> take_bit (LENGTH('a) - Suc 0) (int a) \<le> take_bit (LENGTH('a) - Suc 0) (int b) proof (prove)
goal (1 subgoal):
 1. \<And>nat b a. \<lbrakk>b < 2 ^ nat; a \<le> b; LENGTH('a) = Suc nat\<rbrakk> \<Longrightarrow> take_bit (LENGTH('a) - Suc 0) (int a) \<le> take_bit (LENGTH('a) - Suc 0) (int b) proof (prove)
goal:
No subgoals!