theory CommonOpsLemmas

lemma signed_div_range_check:
  assumes len: "size a > 1"
  shows
  "(sint a sdiv sint b = sint (a sdiv b))
    = (a \<noteq> (- (2 ^ (size a - 1))) \<or> b \<noteq> -1)" proof - have sints: "(sint (1 :: 'a word)) = 1"
       "(sint (-1 :: 'a word)) = -1"
       "(sint (0 :: 'a word)) = 0" using len apply (simp_all add: word_size) done have abs_sint_gt_1:
    "b \<noteq> 0 \<and> b \<noteq> 1 \<and> b \<noteq> -1 \<Longrightarrow> abs (sint b) > 1" apply (fold word_sint.Rep_inject,
        simp only: sints abs_if split: if_split) apply arith done have mag: "(a \<noteq> (- (2 ^ (size a - 1))) \<or> (b \<noteq> -1 \<and> b \<noteq> 1))
    \<Longrightarrow> abs (abs (sint a) div abs (sint b)) < 2 ^ (size a - 1)" using word_sint.Rep_inject[where x=a and y="- (2 ^ (size a - 1))"]
          word_sint.Rep_inject[where x=b and y=1] apply (simp add: word_size sint_int_min sints) apply (simp add: nonneg_mod_div) apply (cases "b = 0") apply simp apply (erule impCE) apply (rule order_le_less_trans, rule zdiv_le_dividend, simp_all) apply (cut_tac x=a in sint_range') apply (clarsimp simp add: abs_if word_size) apply (cases "a = 0", simp_all) apply (rule order_less_le_trans, rule int_div_less_self, simp_all) apply (rule abs_sint_gt_1, simp) apply (cut_tac x=a in sint_range') apply (clarsimp simp add: abs_if word_size) done note sint_of_int_eq[simp] signed_take_bit_int_eq_self[simp] show ?thesis using mag len apply (cases "b = 1") apply (case_tac "size a", simp_all)[1] apply (case_tac nat, simp_all add: sint_word_ariths word_size)[1] apply (simp add: sdiv_int_def sdiv_word_def del: of_int_mult) apply (simp add: sbintrunc_eq_in_range range_sbintrunc sgn_if) apply (safe, simp_all add: word_size sint_int_min sint_int_max_plus_1;
           simp add: sint_word_ariths) done qed

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

goal (1 subgoal):
 1. sint 1 = 1 &&& sint (- 1) = - 1 &&& sint 0 = 0 proof (prove)
goal:
No subgoals! proof (state)
this:
sint 1 = 1
sint (- 1) = - 1
sint 0 = 0

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

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

goal (1 subgoal):
 1. a \<noteq> - (2 ^ (size a - 1)) \<or> b \<noteq> - 1 \<and> b \<noteq> 1 \<Longrightarrow> \<bar>\<bar>sint a\<bar> div \<bar>sint b\<bar>\<bar> < 2 ^ (size a - 1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a = - (2 ^ (LENGTH('a) - Suc 0)) \<longrightarrow> b \<noteq> - 1 \<and> b \<noteq> 1; (sint a = - (2 ^ (LENGTH('a) - Suc 0))) = (a = - (2 ^ (LENGTH('a) - Suc 0))); (sint b = (if LENGTH('a) = Suc 0 then - 1 else 1)) = (b = 1)\<rbrakk> \<Longrightarrow> \<bar>\<bar>sint a\<bar> div \<bar>sint b\<bar>\<bar> < 2 ^ (LENGTH('a) - Suc 0) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a = - (2 ^ (LENGTH('a) - Suc 0)) \<longrightarrow> b \<noteq> - 1 \<and> b \<noteq> 1; (sint a = - (2 ^ (LENGTH('a) - Suc 0))) = (a = - (2 ^ (LENGTH('a) - Suc 0))); (sint b = (if LENGTH('a) = Suc 0 then - 1 else 1)) = (b = 1)\<rbrakk> \<Longrightarrow> \<bar>sint a\<bar> div \<bar>sint b\<bar> < 2 ^ (LENGTH('a) - Suc 0) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a = - (2 ^ (LENGTH('a) - Suc 0)) \<longrightarrow> b \<noteq> - 1 \<and> b \<noteq> 1; (sint a = - (2 ^ (LENGTH('a) - Suc 0))) = (a = - (2 ^ (LENGTH('a) - Suc 0))); (sint b = (if LENGTH('a) = Suc 0 then - 1 else 1)) = (b = 1); b = 0\<rbrakk> \<Longrightarrow> \<bar>sint a\<bar> div \<bar>sint b\<bar> < 2 ^ (LENGTH('a) - Suc 0)
 2. \<lbrakk>a = - (2 ^ (LENGTH('a) - Suc 0)) \<longrightarrow> b \<noteq> - 1 \<and> b \<noteq> 1; (sint a = - (2 ^ (LENGTH('a) - Suc 0))) = (a = - (2 ^ (LENGTH('a) - Suc 0))); (sint b = (if LENGTH('a) = Suc 0 then - 1 else 1)) = (b = 1); b \<noteq> 0\<rbrakk> \<Longrightarrow> \<bar>sint a\<bar> div \<bar>sint b\<bar> < 2 ^ (LENGTH('a) - Suc 0) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a = - (2 ^ (LENGTH('a) - Suc 0)) \<longrightarrow> b \<noteq> - 1 \<and> b \<noteq> 1; (sint a = - (2 ^ (LENGTH('a) - Suc 0))) = (a = - (2 ^ (LENGTH('a) - Suc 0))); (sint b = (if LENGTH('a) = Suc 0 then - 1 else 1)) = (b = 1); b \<noteq> 0\<rbrakk> \<Longrightarrow> \<bar>sint a\<bar> div \<bar>sint b\<bar> < 2 ^ (LENGTH('a) - Suc 0) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(sint a = - (2 ^ (LENGTH('a) - Suc 0))) = (a = - (2 ^ (LENGTH('a) - Suc 0))); (sint b = (if LENGTH('a) = Suc 0 then - 1 else 1)) = (b = 1); b \<noteq> 0; a \<noteq> - (2 ^ (LENGTH('a) - Suc 0))\<rbrakk> \<Longrightarrow> \<bar>sint a\<bar> div \<bar>sint b\<bar> < 2 ^ (LENGTH('a) - Suc 0)
 2. \<lbrakk>(sint a = - (2 ^ (LENGTH('a) - Suc 0))) = (a = - (2 ^ (LENGTH('a) - Suc 0))); (sint b = (if LENGTH('a) = Suc 0 then - 1 else 1)) = (b = 1); b \<noteq> 0; b \<noteq> - 1 \<and> b \<noteq> 1\<rbrakk> \<Longrightarrow> \<bar>sint a\<bar> div \<bar>sint b\<bar> < 2 ^ (LENGTH('a) - Suc 0) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sint a \<noteq> - (2 ^ (LENGTH('a) - Suc 0)); (sint b = (if LENGTH('a) = Suc 0 then - 1 else 1)) = (b = 1); 0 < b; a \<noteq> - (2 ^ (LENGTH('a) - Suc 0))\<rbrakk> \<Longrightarrow> \<bar>sint a\<bar> < 2 ^ (LENGTH('a) - Suc 0)
 2. \<lbrakk>(sint a = - (2 ^ (LENGTH('a) - Suc 0))) = (a = - (2 ^ (LENGTH('a) - Suc 0))); sint b \<noteq> (if LENGTH('a) = Suc 0 then - 1 else 1); 0 < b; b \<noteq> - 1 \<and> b \<noteq> 1\<rbrakk> \<Longrightarrow> \<bar>sint a\<bar> div \<bar>sint b\<bar> < 2 ^ (LENGTH('a) - Suc 0) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sint a \<noteq> - (2 ^ (LENGTH('a) - Suc 0)); (sint b = (if LENGTH('a) = Suc 0 then - 1 else 1)) = (b = 1); 0 < b; a \<noteq> - (2 ^ (LENGTH('a) - Suc 0)); - (2 ^ (LENGTH('a) - Suc 0)) \<le> sint a \<and> sint a < 2 ^ (LENGTH('a) - Suc 0)\<rbrakk> \<Longrightarrow> \<bar>sint a\<bar> < 2 ^ (LENGTH('a) - Suc 0)
 2. \<lbrakk>(sint a = - (2 ^ (LENGTH('a) - Suc 0))) = (a = - (2 ^ (LENGTH('a) - Suc 0))); sint b \<noteq> (if LENGTH('a) = Suc 0 then - 1 else 1); 0 < b; b \<noteq> - 1 \<and> b \<noteq> 1\<rbrakk> \<Longrightarrow> \<bar>sint a\<bar> div \<bar>sint b\<bar> < 2 ^ (LENGTH('a) - Suc 0) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(sint a = - (2 ^ (LENGTH('a) - Suc 0))) = (a = - (2 ^ (LENGTH('a) - Suc 0))); sint b \<noteq> (if LENGTH('a) = Suc 0 then - 1 else 1); 0 < b; b \<noteq> - 1 \<and> b \<noteq> 1\<rbrakk> \<Longrightarrow> \<bar>sint a\<bar> div \<bar>sint b\<bar> < 2 ^ (LENGTH('a) - Suc 0) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(sint a = - (2 ^ (LENGTH('a) - Suc 0))) = (a = - (2 ^ (LENGTH('a) - Suc 0))); sint b \<noteq> (if LENGTH('a) = Suc 0 then - 1 else 1); 0 < b; b \<noteq> - 1 \<and> b \<noteq> 1; 0 < a\<rbrakk> \<Longrightarrow> \<bar>sint a\<bar> div \<bar>sint b\<bar> < 2 ^ (LENGTH('a) - Suc 0) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(sint a = - (2 ^ (LENGTH('a) - Suc 0))) = (a = - (2 ^ (LENGTH('a) - Suc 0))); sint b \<noteq> (if LENGTH('a) = Suc 0 then - 1 else 1); 0 < b; b \<noteq> - 1 \<and> b \<noteq> 1; 0 < a\<rbrakk> \<Longrightarrow> 1 < \<bar>sint b\<bar>
 2. \<lbrakk>(sint a = - (2 ^ (LENGTH('a) - Suc 0))) = (a = - (2 ^ (LENGTH('a) - Suc 0))); sint b \<noteq> (if LENGTH('a) = Suc 0 then - 1 else 1); 0 < b; b \<noteq> - 1 \<and> b \<noteq> 1; 0 < a\<rbrakk> \<Longrightarrow> \<bar>sint a\<bar> \<le> 2 ^ (LENGTH('a) - Suc 0) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(sint a = - (2 ^ (LENGTH('a) - Suc 0))) = (a = - (2 ^ (LENGTH('a) - Suc 0))); sint b \<noteq> (if LENGTH('a) = Suc 0 then - 1 else 1); 0 < b; b \<noteq> - 1 \<and> b \<noteq> 1; 0 < a\<rbrakk> \<Longrightarrow> \<bar>sint a\<bar> \<le> 2 ^ (LENGTH('a) - Suc 0) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(sint a = - (2 ^ (LENGTH('a) - Suc 0))) = (a = - (2 ^ (LENGTH('a) - Suc 0))); sint b \<noteq> (if LENGTH('a) = Suc 0 then - 1 else 1); 0 < b; b \<noteq> - 1 \<and> b \<noteq> 1; 0 < a; - (2 ^ (LENGTH('a) - Suc 0)) \<le> sint a \<and> sint a < 2 ^ (LENGTH('a) - Suc 0)\<rbrakk> \<Longrightarrow> \<bar>sint a\<bar> \<le> 2 ^ (LENGTH('a) - Suc 0) proof (prove)
goal:
No subgoals! proof (state)
this:
a \<noteq> - (2 ^ (size a - 1)) \<or> b \<noteq> - 1 \<and> b \<noteq> 1 \<Longrightarrow> \<bar>\<bar>sint a\<bar> div \<bar>sint b\<bar>\<bar> < 2 ^ (size a - 1)

goal (1 subgoal):
 1. (sint a sdiv sint b = sint (a sdiv b)) = (a \<noteq> - (2 ^ (size a - 1)) \<or> b \<noteq> - 1) proof (state)
this:
\<lbrakk>- (2 ^ (LENGTH(?'a) - 1)) \<le> ?x; ?x < 2 ^ (LENGTH(?'a) - 1)\<rbrakk> \<Longrightarrow> sint (word_of_int ?x) = ?x
\<lbrakk>- (2 ^ ?n) \<le> ?k; ?k < 2 ^ ?n\<rbrakk> \<Longrightarrow> signed_take_bit ?n ?k = ?k

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

goal (1 subgoal):
 1. (sint a sdiv sint b = sint (a sdiv b)) = (a \<noteq> - (2 ^ (size a - 1)) \<or> b \<noteq> - 1) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<noteq> - (2 ^ (size a - 1)) \<or> b \<noteq> - 1 \<and> b \<noteq> 1 \<Longrightarrow> \<bar>\<bar>sint a\<bar> div \<bar>sint b\<bar>\<bar> < 2 ^ (size a - 1); 1 < size a; b = 1\<rbrakk> \<Longrightarrow> (sint a sdiv sint b = sint (a sdiv b)) = (a \<noteq> - (2 ^ (size a - 1)) \<or> b \<noteq> - 1)
 2. \<lbrakk>a \<noteq> - (2 ^ (size a - 1)) \<or> b \<noteq> - 1 \<and> b \<noteq> 1 \<Longrightarrow> \<bar>\<bar>sint a\<bar> div \<bar>sint b\<bar>\<bar> < 2 ^ (size a - 1); 1 < size a; b \<noteq> 1\<rbrakk> \<Longrightarrow> (sint a sdiv sint b = sint (a sdiv b)) = (a \<noteq> - (2 ^ (size a - 1)) \<or> b \<noteq> - 1) proof (prove)
goal (2 subgoals):
 1. \<And>nat. \<lbrakk>a \<noteq> - (2 ^ nat) \<Longrightarrow> \<bar>sint a\<bar> div \<bar>if LENGTH('a) = Suc 0 then - 1 else 1\<bar> < 2 ^ nat; 0 < nat; b = 1; size a = Suc nat\<rbrakk> \<Longrightarrow> LENGTH('a) = Suc 0 \<longrightarrow> (a = 0) = (a \<noteq> - (2 ^ nat))
 2. \<lbrakk>a \<noteq> - (2 ^ (size a - 1)) \<or> b \<noteq> - 1 \<and> b \<noteq> 1 \<Longrightarrow> \<bar>\<bar>sint a\<bar> div \<bar>sint b\<bar>\<bar> < 2 ^ (size a - 1); 1 < size a; b \<noteq> 1\<rbrakk> \<Longrightarrow> (sint a sdiv sint b = sint (a sdiv b)) = (a \<noteq> - (2 ^ (size a - 1)) \<or> b \<noteq> - 1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<noteq> - (2 ^ (size a - 1)) \<or> b \<noteq> - 1 \<and> b \<noteq> 1 \<Longrightarrow> \<bar>\<bar>sint a\<bar> div \<bar>sint b\<bar>\<bar> < 2 ^ (size a - 1); 1 < size a; b \<noteq> 1\<rbrakk> \<Longrightarrow> (sint a sdiv sint b = sint (a sdiv b)) = (a \<noteq> - (2 ^ (size a - 1)) \<or> b \<noteq> - 1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a = - (2 ^ (size a - Suc 0)) \<longrightarrow> b \<noteq> - 1 \<Longrightarrow> \<bar>\<bar>sint a\<bar> div \<bar>sint b\<bar>\<bar> < 2 ^ (size a - Suc 0); Suc 0 < size a; b \<noteq> 1\<rbrakk> \<Longrightarrow> (sgn (sint a) * sgn (sint b) * (\<bar>sint a\<bar> div \<bar>sint b\<bar>) = sint (word_of_int (sgn (sint a) * sgn (sint b) * (\<bar>sint a\<bar> div \<bar>sint b\<bar>)))) = (a = - (2 ^ (size a - Suc 0)) \<longrightarrow> b \<noteq> - 1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a = - (2 ^ (size a - Suc 0)) \<longrightarrow> b \<noteq> - 1 \<Longrightarrow> \<bar>\<bar>sint a\<bar> div \<bar>sint b\<bar>\<bar> < 2 ^ (size a - Suc 0); Suc 0 < size a; b \<noteq> 1\<rbrakk> \<Longrightarrow> (0 < sint a \<longrightarrow> (a = 0 \<longrightarrow> 0 < b \<longrightarrow> LENGTH('a) \<le> size 0 - Suc 0 \<longrightarrow> b \<noteq> - 1) \<and> (0 < a \<longrightarrow> (0 < sint b \<longrightarrow> 0 < b \<longrightarrow> (sint a div sint b = sint (word_of_int (sint a div sint b))) = (a = - (2 ^ (size a - Suc 0)) \<longrightarrow> b \<noteq> - 1)) \<and> (\<not> 0 < sint b \<longrightarrow> 0 < b \<longrightarrow> (- (sint a div - sint b) = sint (- word_of_int (sint a div - sint b))) = (a = - (2 ^ (size a - Suc 0)) \<longrightarrow> b \<noteq> - 1)))) \<and> (\<not> 0 < sint a \<longrightarrow> (a = 0 \<longrightarrow> 0 < b \<longrightarrow> LENGTH('a) \<le> size 0 - Suc 0 \<longrightarrow> b \<noteq> - 1) \<and> (0 < a \<longrightarrow> (0 < sint b \<longrightarrow> 0 < b \<longrightarrow> (- (- sint a div sint b) = sint (- word_of_int (- sint a div sint b))) = (a = - (2 ^ (size a - Suc 0)) \<longrightarrow> b \<noteq> - 1)) \<and> (\<not> 0 < sint b \<longrightarrow> 0 < b \<longrightarrow> (sint a div sint b = sint (word_of_int (sint a div sint b))) = (a = - (2 ^ (size a - Suc 0)) \<longrightarrow> b \<noteq> - 1)))) proof (prove)
goal:
No subgoals! proof (state)
this:
(sint a sdiv sint b = sint (a sdiv b)) = (a \<noteq> - (2 ^ (size a - 1)) \<or> b \<noteq> - 1)

goal:
No subgoals!