theory Signed_Division_Word

lemma smod_word_max:
  "sint (a::'a word) smod sint (b::'a word) < 2 ^ (LENGTH('a::len) - Suc 0)" apply (cases \<open>sint b = 0\<close>) apply (simp_all add: sint_less) apply (cases \<open>LENGTH('a)\<close>) apply simp_all using smod_int_range [where a="sint a" and b="sint b"] apply auto apply (rule less_le_trans) apply assumption apply (auto simp add: abs_le_iff) apply (metis diff_Suc_1 le_cases linorder_not_le sint_lt) apply (metis add.inverse_inverse diff_Suc_1 linorder_not_less neg_less_iff_less sint_ge) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sint a smod sint b < 2 ^ (LENGTH('a) - Suc 0) proof (prove)
goal (2 subgoals):
 1. sint b = 0 \<Longrightarrow> sint a smod sint b < 2 ^ (LENGTH('a) - Suc 0)
 2. sint b \<noteq> 0 \<Longrightarrow> sint a smod sint b < 2 ^ (LENGTH('a) - Suc 0) proof (prove)
goal (1 subgoal):
 1. sint b \<noteq> 0 \<Longrightarrow> sint a smod sint b < 2 ^ (LENGTH('a) - Suc 0) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sint b \<noteq> 0; LENGTH('a) = 0\<rbrakk> \<Longrightarrow> sint a smod sint b < 2 ^ (LENGTH('a) - Suc 0)
 2. \<And>nat. \<lbrakk>sint b \<noteq> 0; LENGTH('a) = Suc nat\<rbrakk> \<Longrightarrow> sint a smod sint b < 2 ^ (LENGTH('a) - Suc 0) proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>sint b \<noteq> 0; LENGTH('a) = Suc nat\<rbrakk> \<Longrightarrow> sint a smod sint b < 2 ^ nat 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>sint b \<noteq> 0; LENGTH('a) = Suc nat\<rbrakk> \<Longrightarrow> sint a smod sint b < 2 ^ nat proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>sint b \<noteq> 0; LENGTH('a) = Suc nat; 1 - \<bar>sint b\<bar> \<le> sint a smod sint b; sint a smod sint b < \<bar>sint b\<bar>\<rbrakk> \<Longrightarrow> sint a smod sint b < 2 ^ nat proof (prove)
goal (2 subgoals):
 1. \<And>nat. \<lbrakk>sint b \<noteq> 0; LENGTH('a) = Suc nat; 1 - \<bar>sint b\<bar> \<le> sint a smod sint b; sint a smod sint b < \<bar>sint b\<bar>\<rbrakk> \<Longrightarrow> sint a smod sint b < ?y5 nat
 2. \<And>nat. \<lbrakk>sint b \<noteq> 0; LENGTH('a) = Suc nat; 1 - \<bar>sint b\<bar> \<le> sint a smod sint b; sint a smod sint b < \<bar>sint b\<bar>\<rbrakk> \<Longrightarrow> ?y5 nat \<le> 2 ^ nat proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>sint b \<noteq> 0; LENGTH('a) = Suc nat; 1 - \<bar>sint b\<bar> \<le> sint a smod sint b; sint a smod sint b < \<bar>sint b\<bar>\<rbrakk> \<Longrightarrow> \<bar>sint b\<bar> \<le> 2 ^ nat proof (prove)
goal (2 subgoals):
 1. \<And>nat. \<lbrakk>sint b \<noteq> 0; LENGTH('a) = Suc nat; 1 - \<bar>sint b\<bar> \<le> sint a smod sint b; sint a smod sint b < \<bar>sint b\<bar>\<rbrakk> \<Longrightarrow> sint b \<le> 2 ^ nat
 2. \<And>nat. \<lbrakk>sint b \<noteq> 0; LENGTH('a) = Suc nat; 1 - \<bar>sint b\<bar> \<le> sint a smod sint b; sint a smod sint b < \<bar>sint b\<bar>\<rbrakk> \<Longrightarrow> - sint b \<le> 2 ^ nat proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>sint b \<noteq> 0; LENGTH('a) = Suc nat; 1 - \<bar>sint b\<bar> \<le> sint a smod sint b; sint a smod sint b < \<bar>sint b\<bar>\<rbrakk> \<Longrightarrow> - sint b \<le> 2 ^ nat proof (prove)
goal:
No subgoals!