theory Signed_Division_Word

lemma smod_word_min:
  "- (2 ^ (LENGTH('a::len) - Suc 0)) \<le> sint (a::'a word) smod sint (b::'a word)" apply (cases \<open>LENGTH('a)\<close>) apply simp_all apply (cases \<open>sint b = 0\<close>) apply simp_all apply (metis diff_Suc_1 sint_ge) using smod_int_range [where a="sint a" and b="sint b"] apply auto apply (rule order_trans) defer apply assumption apply (auto simp add: algebra_simps abs_le_iff) apply (metis abs_zero add.left_neutral add_mono_thms_linordered_semiring(1) diff_Suc_1 le_cases linorder_not_less sint_lt zabs_less_one_iff) apply (metis abs_zero add.inverse_inverse add.left_neutral add_mono_thms_linordered_semiring(1) diff_Suc_1 le_cases le_minus_iff linorder_not_less sint_ge zabs_less_one_iff) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. - (2 ^ (LENGTH('a) - Suc 0)) \<le> sint a smod sint b proof (prove)
goal (2 subgoals):
 1. LENGTH('a) = 0 \<Longrightarrow> - (2 ^ (LENGTH('a) - Suc 0)) \<le> sint a smod sint b
 2. \<And>nat. LENGTH('a) = Suc nat \<Longrightarrow> - (2 ^ (LENGTH('a) - Suc 0)) \<le> sint a smod sint b proof (prove)
goal (1 subgoal):
 1. \<And>nat. LENGTH('a) = Suc nat \<Longrightarrow> - (2 ^ nat) \<le> sint a smod sint b proof (prove)
goal (2 subgoals):
 1. \<And>nat. \<lbrakk>LENGTH('a) = Suc nat; sint b = 0\<rbrakk> \<Longrightarrow> - (2 ^ nat) \<le> sint a smod sint b
 2. \<And>nat. \<lbrakk>LENGTH('a) = Suc nat; sint b \<noteq> 0\<rbrakk> \<Longrightarrow> - (2 ^ nat) \<le> sint a smod sint b proof (prove)
goal (2 subgoals):
 1. \<And>nat. \<lbrakk>LENGTH('a) = Suc nat; sint b = 0\<rbrakk> \<Longrightarrow> - (2 ^ nat) \<le> sint a
 2. \<And>nat. \<lbrakk>LENGTH('a) = Suc nat; sint b \<noteq> 0\<rbrakk> \<Longrightarrow> - (2 ^ nat) \<le> sint a smod sint b proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>LENGTH('a) = Suc nat; sint b \<noteq> 0\<rbrakk> \<Longrightarrow> - (2 ^ nat) \<le> sint a smod sint b proof (prove)
using this:
sint b \<noteq> 0 \<Longrightarrow> sint a smod sint b \<in> {- \<bar>sint b\<bar> + 1..\<bar>sint b\<bar> - 1}

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