theory Word_Lemmas

lemma sdiv_word_max:
    "(sint (a :: ('a::len) word) sdiv sint (b :: ('a::len) word) < (2 ^ (size a - 1))) =
          ((a \<noteq> - (2 ^ (size a - 1)) \<or> (b \<noteq> -1)))"
    (is "?lhs = (\<not> ?a_int_min \<or> \<not> ?b_minus1)") proof (rule classical) assume not_thesis: "\<not> ?thesis" have not_zero: "b \<noteq> 0" using not_thesis by (clarsimp) let ?range = \<open>{- (2 ^ (size a - 1))..<2 ^ (size a - 1)} :: int set\<close> have result_range: "sint a sdiv sint b \<in> ?range \<union> {2 ^ (size a - 1)}" using sdiv_word_min [of a b] sdiv_word_max [of a b] by auto have result_range_overflow: "(sint a sdiv sint b = 2 ^ (size a - 1)) = (?a_int_min \<and> ?b_minus1)" apply (rule iffI [rotated]) apply (clarsimp simp: signed_divide_int_def sgn_if word_size sint_int_min) apply (rule classical) apply (case_tac "?a_int_min") apply (clarsimp simp: word_size sint_int_min) apply (metis diff_0_right
              int_sdiv_negated_is_minus1 minus_diff_eq minus_int_code(2)
              power_eq_0_iff sint_minus1 zero_neq_numeral) apply (subgoal_tac "abs (sint a) < 2 ^ (size a - 1)") apply (insert sdiv_int_range [where a="sint a" and b="sint b"])[1] apply (clarsimp simp: word_size) apply (insert sdiv_int_range [where a="sint a" and b="sint b"])[1] by (smt (verit, best) One_nat_def signed_word_eqI sint_greater_eq sint_int_min sint_less wsst_TYs(3)) have result_range_simple: "(sint a sdiv sint b \<in> ?range) \<Longrightarrow> ?thesis" apply (insert sdiv_int_range [where a="sint a" and b="sint b"]) apply (clarsimp simp: word_size sint_int_min) done show ?thesis apply (rule UnE [OF result_range result_range_simple]) apply simp apply (clarsimp simp: word_size) using result_range_overflow apply (clarsimp simp: word_size) done qed

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

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

goal (1 subgoal):
 1. b \<noteq> 0 proof (state)
this:
b \<noteq> 0

goal (1 subgoal):
 1. (sint a sdiv sint b < 2 ^ (size a - 1)) \<noteq> (a \<noteq> - (2 ^ (size a - 1)) \<or> b \<noteq> - 1) \<Longrightarrow> (sint a sdiv sint b < 2 ^ (size a - 1)) = (a \<noteq> - (2 ^ (size a - 1)) \<or> b \<noteq> - 1) proof (state)
goal (1 subgoal):
 1. (sint a sdiv sint b < 2 ^ (size a - 1)) \<noteq> (a \<noteq> - (2 ^ (size a - 1)) \<or> b \<noteq> - 1) \<Longrightarrow> (sint a sdiv sint b < 2 ^ (size a - 1)) = (a \<noteq> - (2 ^ (size a - 1)) \<or> b \<noteq> - 1) proof (prove)
goal (1 subgoal):
 1. sint a sdiv sint b \<in> {- (2 ^ (size a - 1))..<2 ^ (size a - 1)} \<union> {2 ^ (size a - 1)} proof (prove)
using this:
- (2 ^ (size a - 1)) \<le> sint a sdiv sint b
sint a sdiv sint b \<le> 2 ^ (size a - Suc 0)

goal (1 subgoal):
 1. sint a sdiv sint b \<in> {- (2 ^ (size a - 1))..<2 ^ (size a - 1)} \<union> {2 ^ (size a - 1)} proof (state)
this:
sint a sdiv sint b \<in> {- (2 ^ (size a - 1))..<2 ^ (size a - 1)} \<union> {2 ^ (size a - 1)}

goal (1 subgoal):
 1. (sint a sdiv sint b < 2 ^ (size a - 1)) \<noteq> (a \<noteq> - (2 ^ (size a - 1)) \<or> b \<noteq> - 1) \<Longrightarrow> (sint a sdiv sint b < 2 ^ (size a - 1)) = (a \<noteq> - (2 ^ (size a - 1)) \<or> b \<noteq> - 1) proof (prove)
goal (1 subgoal):
 1. (sint a sdiv sint b = 2 ^ (size a - 1)) = (a = - (2 ^ (size a - 1)) \<and> b = - 1) proof (prove)
goal (2 subgoals):
 1. a = - (2 ^ (size a - 1)) \<and> b = - 1 \<Longrightarrow> sint a sdiv sint b = 2 ^ (size a - 1)
 2. sint a sdiv sint b = 2 ^ (size a - 1) \<Longrightarrow> a = - (2 ^ (size a - 1)) \<and> b = - 1 proof (prove)
goal (1 subgoal):
 1. sint a sdiv sint b = 2 ^ (size a - 1) \<Longrightarrow> a = - (2 ^ (size a - 1)) \<and> b = - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sint a sdiv sint b = 2 ^ (size a - 1); \<not> (a = - (2 ^ (size a - 1)) \<and> b = - 1)\<rbrakk> \<Longrightarrow> a = - (2 ^ (size a - 1)) \<and> b = - 1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sint a sdiv sint b = 2 ^ (size a - 1); \<not> (a = - (2 ^ (size a - 1)) \<and> b = - 1); a = - (2 ^ (size a - 1))\<rbrakk> \<Longrightarrow> a = - (2 ^ (size a - 1)) \<and> b = - 1
 2. \<lbrakk>sint a sdiv sint b = 2 ^ (size a - 1); \<not> (a = - (2 ^ (size a - 1)) \<and> b = - 1); a \<noteq> - (2 ^ (size a - 1))\<rbrakk> \<Longrightarrow> a = - (2 ^ (size a - 1)) \<and> b = - 1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>- (2 ^ (LENGTH('a) - Suc 0) sdiv sint b) = 2 ^ (LENGTH('a) - Suc 0); b \<noteq> - 1; a = - (2 ^ (LENGTH('a) - Suc 0))\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>sint a sdiv sint b = 2 ^ (size a - 1); \<not> (a = - (2 ^ (size a - 1)) \<and> b = - 1); a \<noteq> - (2 ^ (size a - 1))\<rbrakk> \<Longrightarrow> a = - (2 ^ (size a - 1)) \<and> b = - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sint a sdiv sint b = 2 ^ (size a - 1); \<not> (a = - (2 ^ (size a - 1)) \<and> b = - 1); a \<noteq> - (2 ^ (size a - 1))\<rbrakk> \<Longrightarrow> a = - (2 ^ (size a - 1)) \<and> b = - 1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sint a sdiv sint b = 2 ^ (size a - 1); \<not> (a = - (2 ^ (size a - 1)) \<and> b = - 1); a \<noteq> - (2 ^ (size a - 1)); \<bar>sint a\<bar> < 2 ^ (size a - 1)\<rbrakk> \<Longrightarrow> a = - (2 ^ (size a - 1)) \<and> b = - 1
 2. \<lbrakk>sint a sdiv sint b = 2 ^ (size a - 1); \<not> (a = - (2 ^ (size a - 1)) \<and> b = - 1); a \<noteq> - (2 ^ (size a - 1))\<rbrakk> \<Longrightarrow> \<bar>sint a\<bar> < 2 ^ (size a - 1) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sint a sdiv sint b = 2 ^ (size a - 1); \<not> (a = - (2 ^ (size a - 1)) \<and> b = - 1); a \<noteq> - (2 ^ (size a - 1)); \<bar>sint a\<bar> < 2 ^ (size a - 1); sint a sdiv sint b \<in> {- \<bar>sint a\<bar>..\<bar>sint a\<bar>}\<rbrakk> \<Longrightarrow> a = - (2 ^ (size a - 1)) \<and> b = - 1
 2. \<lbrakk>sint a sdiv sint b = 2 ^ (size a - 1); \<not> (a = - (2 ^ (size a - 1)) \<and> b = - 1); a \<noteq> - (2 ^ (size a - 1))\<rbrakk> \<Longrightarrow> \<bar>sint a\<bar> < 2 ^ (size a - 1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sint a sdiv sint b = 2 ^ (size a - 1); \<not> (a = - (2 ^ (size a - 1)) \<and> b = - 1); a \<noteq> - (2 ^ (size a - 1))\<rbrakk> \<Longrightarrow> \<bar>sint a\<bar> < 2 ^ (size a - 1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sint a sdiv sint b = 2 ^ (size a - 1); \<not> (a = - (2 ^ (size a - 1)) \<and> b = - 1); a \<noteq> - (2 ^ (size a - 1)); sint a sdiv sint b \<in> {- \<bar>sint a\<bar>..\<bar>sint a\<bar>}\<rbrakk> \<Longrightarrow> \<bar>sint a\<bar> < 2 ^ (size a - 1) proof (state)
this:
(sint a sdiv sint b = 2 ^ (size a - 1)) = (a = - (2 ^ (size a - 1)) \<and> b = - 1)

goal (1 subgoal):
 1. (sint a sdiv sint b < 2 ^ (size a - 1)) \<noteq> (a \<noteq> - (2 ^ (size a - 1)) \<or> b \<noteq> - 1) \<Longrightarrow> (sint a sdiv sint b < 2 ^ (size a - 1)) = (a \<noteq> - (2 ^ (size a - 1)) \<or> b \<noteq> - 1) proof (prove)
goal (1 subgoal):
 1. sint a sdiv sint b \<in> {- (2 ^ (size a - 1))..<2 ^ (size a - 1)} \<Longrightarrow> (sint a sdiv sint b < 2 ^ (size a - 1)) = (a \<noteq> - (2 ^ (size a - 1)) \<or> b \<noteq> - 1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sint a sdiv sint b \<in> {- (2 ^ (size a - 1))..<2 ^ (size a - 1)}; sint a sdiv sint b \<in> {- \<bar>sint a\<bar>..\<bar>sint a\<bar>}\<rbrakk> \<Longrightarrow> (sint a sdiv sint b < 2 ^ (size a - 1)) = (a \<noteq> - (2 ^ (size a - 1)) \<or> b \<noteq> - 1) proof (prove)
goal:
No subgoals! proof (state)
this:
sint a sdiv sint b \<in> {- (2 ^ (size a - 1))..<2 ^ (size a - 1)} \<Longrightarrow> (sint a sdiv sint b < 2 ^ (size a - 1)) = (a \<noteq> - (2 ^ (size a - 1)) \<or> b \<noteq> - 1)

goal (1 subgoal):
 1. (sint a sdiv sint b < 2 ^ (size a - 1)) \<noteq> (a \<noteq> - (2 ^ (size a - 1)) \<or> b \<noteq> - 1) \<Longrightarrow> (sint a sdiv sint b < 2 ^ (size a - 1)) = (a \<noteq> - (2 ^ (size a - 1)) \<or> b \<noteq> - 1) proof (prove)
goal (1 subgoal):
 1. (sint a sdiv sint b < 2 ^ (size a - 1)) = (a \<noteq> - (2 ^ (size a - 1)) \<or> b \<noteq> - 1) proof (prove)
goal (2 subgoals):
 1. sint a sdiv sint b \<in> {- (2 ^ (size a - 1))..<2 ^ (size a - 1)} \<Longrightarrow> sint a sdiv sint b \<in> {- (2 ^ (size a - 1))..<2 ^ (size a - 1)}
 2. sint a sdiv sint b \<in> {2 ^ (size a - 1)} \<Longrightarrow> (sint a sdiv sint b < 2 ^ (size a - 1)) = (a \<noteq> - (2 ^ (size a - 1)) \<or> b \<noteq> - 1) proof (prove)
goal (1 subgoal):
 1. sint a sdiv sint b \<in> {2 ^ (size a - 1)} \<Longrightarrow> (sint a sdiv sint b < 2 ^ (size a - 1)) = (a \<noteq> - (2 ^ (size a - 1)) \<or> b \<noteq> - 1) proof (prove)
goal (1 subgoal):
 1. sint a sdiv sint b = 2 ^ (LENGTH('a) - Suc 0) \<Longrightarrow> a = - (2 ^ (LENGTH('a) - Suc 0)) \<and> b = - 1 proof (prove)
using this:
(sint a sdiv sint b = 2 ^ (size a - 1)) = (a = - (2 ^ (size a - 1)) \<and> b = - 1)

goal (1 subgoal):
 1. sint a sdiv sint b = 2 ^ (LENGTH('a) - Suc 0) \<Longrightarrow> a = - (2 ^ (LENGTH('a) - Suc 0)) \<and> b = - 1 proof (prove)
goal:
No subgoals! proof (state)
this:
(sint a sdiv sint b < 2 ^ (size a - 1)) = (a \<noteq> - (2 ^ (size a - 1)) \<or> b \<noteq> - 1)

goal:
No subgoals!