theory Signed_Division_Word

lemma sdiv_word_max:
  \<open>sint a sdiv sint b \<le> 2 ^ (size a - Suc 0)\<close>
  for a b :: \<open>'a::len word\<close> proof (cases \<open>sint a = 0 \<or> sint b = 0 \<or> sgn (sint a) \<noteq> sgn (sint b)\<close>) case True then show ?thesis apply (auto simp add: sgn_if not_less signed_divide_int_def split: if_splits) apply (smt (z3) pos_imp_zdiv_neg_iff zero_le_power) apply (smt (z3) not_exp_less_eq_0_int pos_imp_zdiv_neg_iff) done next case False then have \<open>\<bar>sint a\<bar> div \<bar>sint b\<bar> \<le> \<bar>sint a\<bar>\<close> by (subst nat_le_eq_zle [symmetric]) (simp_all add: div_abs_eq_div_nat) also have \<open>\<bar>sint a\<bar> \<le> 2 ^ (size a - Suc 0)\<close> using sint_range_size [of a] by auto finally show ?thesis using False by (simp add: signed_divide_int_def) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sint a sdiv sint b \<le> 2 ^ (size a - Suc 0) proof (state)
goal (2 subgoals):
 1. sint a = 0 \<or> sint b = 0 \<or> sgn (sint a) \<noteq> sgn (sint b) \<Longrightarrow> sint a sdiv sint b \<le> 2 ^ (size a - Suc 0)
 2. \<not> (sint a = 0 \<or> sint b = 0 \<or> sgn (sint a) \<noteq> sgn (sint b)) \<Longrightarrow> sint a sdiv sint b \<le> 2 ^ (size a - Suc 0) proof (state)
this:
sint a = 0 \<or> sint b = 0 \<or> sgn (sint a) \<noteq> sgn (sint b)

goal (2 subgoals):
 1. sint a = 0 \<or> sint b = 0 \<or> sgn (sint a) \<noteq> sgn (sint b) \<Longrightarrow> sint a sdiv sint b \<le> 2 ^ (size a - Suc 0)
 2. \<not> (sint a = 0 \<or> sint b = 0 \<or> sgn (sint a) \<noteq> sgn (sint b)) \<Longrightarrow> sint a sdiv sint b \<le> 2 ^ (size a - Suc 0) proof (chain)
picking this:
sint a = 0 \<or> sint b = 0 \<or> sgn (sint a) \<noteq> sgn (sint b) proof (prove)
using this:
sint a = 0 \<or> sint b = 0 \<or> sgn (sint a) \<noteq> sgn (sint b)

goal (1 subgoal):
 1. sint a sdiv sint b \<le> 2 ^ (size a - Suc 0) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < sint b; sint a \<noteq> 0; sint a \<le> 0\<rbrakk> \<Longrightarrow> - (- sint a div sint b) \<le> 2 ^ (size a - Suc 0)
 2. \<lbrakk>sint b \<noteq> 0; sint b \<le> 0; 0 < sint a\<rbrakk> \<Longrightarrow> - (sint a div - sint b) \<le> 2 ^ (size a - Suc 0) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sint b \<noteq> 0; sint b \<le> 0; 0 < sint a\<rbrakk> \<Longrightarrow> - (sint a div - sint b) \<le> 2 ^ (size a - Suc 0) proof (prove)
goal:
No subgoals! proof (state)
this:
sint a sdiv sint b \<le> 2 ^ (size a - Suc 0)

goal (1 subgoal):
 1. \<not> (sint a = 0 \<or> sint b = 0 \<or> sgn (sint a) \<noteq> sgn (sint b)) \<Longrightarrow> sint a sdiv sint b \<le> 2 ^ (size a - Suc 0) proof (state)
goal (1 subgoal):
 1. \<not> (sint a = 0 \<or> sint b = 0 \<or> sgn (sint a) \<noteq> sgn (sint b)) \<Longrightarrow> sint a sdiv sint b \<le> 2 ^ (size a - Suc 0) proof (state)
this:
\<not> (sint a = 0 \<or> sint b = 0 \<or> sgn (sint a) \<noteq> sgn (sint b))

goal (1 subgoal):
 1. \<not> (sint a = 0 \<or> sint b = 0 \<or> sgn (sint a) \<noteq> sgn (sint b)) \<Longrightarrow> sint a sdiv sint b \<le> 2 ^ (size a - Suc 0) proof (chain)
picking this:
\<not> (sint a = 0 \<or> sint b = 0 \<or> sgn (sint a) \<noteq> sgn (sint b)) proof (prove)
using this:
\<not> (sint a = 0 \<or> sint b = 0 \<or> sgn (sint a) \<noteq> sgn (sint b))

goal (1 subgoal):
 1. \<bar>sint a\<bar> div \<bar>sint b\<bar> \<le> \<bar>sint a\<bar> proof (state)
this:
\<bar>sint a\<bar> div \<bar>sint b\<bar> \<le> \<bar>sint a\<bar>

goal (1 subgoal):
 1. \<not> (sint a = 0 \<or> sint b = 0 \<or> sgn (sint a) \<noteq> sgn (sint b)) \<Longrightarrow> sint a sdiv sint b \<le> 2 ^ (size a - Suc 0) proof (state)
this:
\<bar>sint a\<bar> div \<bar>sint b\<bar> \<le> \<bar>sint a\<bar>

goal (1 subgoal):
 1. \<not> (sint a = 0 \<or> sint b = 0 \<or> sgn (sint a) \<noteq> sgn (sint b)) \<Longrightarrow> sint a sdiv sint b \<le> 2 ^ (size a - Suc 0) proof (prove)
goal (1 subgoal):
 1. \<bar>sint a\<bar> \<le> 2 ^ (size a - Suc 0) proof (prove)
using this:
- (2 ^ (size a - Suc 0)) \<le> sint a \<and> sint a < 2 ^ (size a - Suc 0)

goal (1 subgoal):
 1. \<bar>sint a\<bar> \<le> 2 ^ (size a - Suc 0) proof (state)
this:
\<bar>sint a\<bar> \<le> 2 ^ (size a - Suc 0)

goal (1 subgoal):
 1. \<not> (sint a = 0 \<or> sint b = 0 \<or> sgn (sint a) \<noteq> sgn (sint b)) \<Longrightarrow> sint a sdiv sint b \<le> 2 ^ (size a - Suc 0) proof (chain)
picking this:
\<bar>sint a\<bar> div \<bar>sint b\<bar> \<le> 2 ^ (size a - Suc 0) proof (prove)
using this:
\<bar>sint a\<bar> div \<bar>sint b\<bar> \<le> 2 ^ (size a - Suc 0)

goal (1 subgoal):
 1. sint a sdiv sint b \<le> 2 ^ (size a - Suc 0) proof (prove)
using this:
\<bar>sint a\<bar> div \<bar>sint b\<bar> \<le> 2 ^ (size a - Suc 0)
\<not> (sint a = 0 \<or> sint b = 0 \<or> sgn (sint a) \<noteq> sgn (sint b))

goal (1 subgoal):
 1. sint a sdiv sint b \<le> 2 ^ (size a - Suc 0) proof (state)
this:
sint a sdiv sint b \<le> 2 ^ (size a - Suc 0)

goal:
No subgoals!