theory Signed_Division_Word

lemma sdiv_word_min:
    "- (2 ^ (size a - 1)) \<le> sint (a :: ('a::len) word) sdiv sint (b :: ('a::len) word)" using sdiv_int_range [where a="sint a" and b="sint b"] apply auto apply (cases \<open>LENGTH('a)\<close>) apply simp_all apply transfer apply simp apply (rule order_trans) defer apply assumption apply simp apply (metis abs_le_iff add.inverse_inverse le_cases le_minus_iff not_le signed_take_bit_int_eq_self_iff signed_take_bit_minus) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. - (2 ^ (size a - 1)) \<le> sint a sdiv sint b proof (prove)
using this:
sint a sdiv sint b \<in> {- \<bar>sint a\<bar>..\<bar>sint a\<bar>}

goal (1 subgoal):
 1. - (2 ^ (size a - 1)) \<le> sint a sdiv sint b proof (prove)
goal (1 subgoal):
 1. \<lbrakk>- \<bar>sint a\<bar> \<le> sint a sdiv sint b; sint a sdiv sint b \<le> \<bar>sint a\<bar>\<rbrakk> \<Longrightarrow> - (2 ^ (size a - Suc 0)) \<le> sint a sdiv sint b proof (prove)
goal (2 subgoals):
 1. \<lbrakk>- \<bar>sint a\<bar> \<le> sint a sdiv sint b; sint a sdiv sint b \<le> \<bar>sint a\<bar>; LENGTH('a) = 0\<rbrakk> \<Longrightarrow> - (2 ^ (size a - Suc 0)) \<le> sint a sdiv sint b
 2. \<And>nat. \<lbrakk>- \<bar>sint a\<bar> \<le> sint a sdiv sint b; sint a sdiv sint b \<le> \<bar>sint a\<bar>; LENGTH('a) = Suc nat\<rbrakk> \<Longrightarrow> - (2 ^ (size a - Suc 0)) \<le> sint a sdiv sint b proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>- \<bar>sint a\<bar> \<le> sint a sdiv sint b; sint a sdiv sint b \<le> \<bar>sint a\<bar>; LENGTH('a) = Suc nat\<rbrakk> \<Longrightarrow> - (2 ^ (size a - Suc 0)) \<le> sint a sdiv sint b proof (prove)
goal (1 subgoal):
 1. \<And>nat a b. \<lbrakk>- \<bar>signed_take_bit (LENGTH('a) - Suc 0) a\<bar> \<le> signed_take_bit (LENGTH('a) - Suc 0) a sdiv signed_take_bit (LENGTH('a) - Suc 0) b; signed_take_bit (LENGTH('a) - Suc 0) a sdiv signed_take_bit (LENGTH('a) - Suc 0) b \<le> \<bar>signed_take_bit (LENGTH('a) - Suc 0) a\<bar>; LENGTH('a) = Suc nat\<rbrakk> \<Longrightarrow> - (2 ^ (LENGTH('a) - Suc 0)) \<le> signed_take_bit (LENGTH('a) - Suc 0) a sdiv signed_take_bit (LENGTH('a) - Suc 0) b proof (prove)
goal (1 subgoal):
 1. \<And>nat a b. \<lbrakk>- \<bar>signed_take_bit nat a\<bar> \<le> signed_take_bit nat a sdiv signed_take_bit nat b; signed_take_bit nat a sdiv signed_take_bit nat b \<le> \<bar>signed_take_bit nat a\<bar>; LENGTH('a) = Suc nat\<rbrakk> \<Longrightarrow> - (2 ^ nat) \<le> signed_take_bit nat a sdiv signed_take_bit nat b proof (prove)
goal (2 subgoals):
 1. \<And>nat a b. \<lbrakk>- \<bar>signed_take_bit nat a\<bar> \<le> signed_take_bit nat a sdiv signed_take_bit nat b; signed_take_bit nat a sdiv signed_take_bit nat b \<le> \<bar>signed_take_bit nat a\<bar>; LENGTH('a) = Suc nat\<rbrakk> \<Longrightarrow> - (2 ^ nat) \<le> ?y300 nat a b
 2. \<And>nat a b. \<lbrakk>- \<bar>signed_take_bit nat a\<bar> \<le> signed_take_bit nat a sdiv signed_take_bit nat b; signed_take_bit nat a sdiv signed_take_bit nat b \<le> \<bar>signed_take_bit nat a\<bar>; LENGTH('a) = Suc nat\<rbrakk> \<Longrightarrow> ?y300 nat a b \<le> signed_take_bit nat a sdiv signed_take_bit nat b proof (prove)
goal (2 subgoals):
 1. \<And>nat a b. \<lbrakk>- \<bar>signed_take_bit nat a\<bar> \<le> signed_take_bit nat a sdiv signed_take_bit nat b; signed_take_bit nat a sdiv signed_take_bit nat b \<le> \<bar>signed_take_bit nat a\<bar>; LENGTH('a) = Suc nat\<rbrakk> \<Longrightarrow> ?y300 nat a b \<le> signed_take_bit nat a sdiv signed_take_bit nat b
 2. \<And>nat a b. \<lbrakk>- \<bar>signed_take_bit nat a\<bar> \<le> signed_take_bit nat a sdiv signed_take_bit nat b; signed_take_bit nat a sdiv signed_take_bit nat b \<le> \<bar>signed_take_bit nat a\<bar>; LENGTH('a) = Suc nat\<rbrakk> \<Longrightarrow> - (2 ^ nat) \<le> ?y300 nat a b proof (prove)
goal (1 subgoal):
 1. \<And>nat a b. \<lbrakk>- \<bar>signed_take_bit nat a\<bar> \<le> signed_take_bit nat a sdiv signed_take_bit nat b; signed_take_bit nat a sdiv signed_take_bit nat b \<le> \<bar>signed_take_bit nat a\<bar>; LENGTH('a) = Suc nat\<rbrakk> \<Longrightarrow> - (2 ^ nat) \<le> - \<bar>signed_take_bit nat a\<bar> proof (prove)
goal (1 subgoal):
 1. \<And>nat a b. \<lbrakk>- \<bar>signed_take_bit nat a\<bar> \<le> signed_take_bit nat a sdiv signed_take_bit nat b; signed_take_bit nat a sdiv signed_take_bit nat b \<le> \<bar>signed_take_bit nat a\<bar>; LENGTH('a) = Suc nat\<rbrakk> \<Longrightarrow> \<bar>signed_take_bit nat a\<bar> \<le> 2 ^ nat proof (prove)
goal:
No subgoals!