author | Manuel Eberl <eberlm@in.tum.de> |
Fri, 29 Mar 2024 19:28:59 +0100 | |
changeset 80061 | 4c1347e172b1 |
parent 79950 | 82aaa0d8fc3b |
permissions | -rw-r--r-- |
72281
beeadb35e357
more thorough treatment of division, particularly signed division on int and word
haftmann
parents:
diff
changeset
|
1 |
(* Author: Stefan Berghofer et al. |
beeadb35e357
more thorough treatment of division, particularly signed division on int and word
haftmann
parents:
diff
changeset
|
2 |
*) |
beeadb35e357
more thorough treatment of division, particularly signed division on int and word
haftmann
parents:
diff
changeset
|
3 |
|
77811 | 4 |
section \<open>Signed division: negative results rounded towards zero rather than minus infinity.\<close> |
72281
beeadb35e357
more thorough treatment of division, particularly signed division on int and word
haftmann
parents:
diff
changeset
|
5 |
|
beeadb35e357
more thorough treatment of division, particularly signed division on int and word
haftmann
parents:
diff
changeset
|
6 |
theory Signed_Division |
beeadb35e357
more thorough treatment of division, particularly signed division on int and word
haftmann
parents:
diff
changeset
|
7 |
imports Main |
beeadb35e357
more thorough treatment of division, particularly signed division on int and word
haftmann
parents:
diff
changeset
|
8 |
begin |
beeadb35e357
more thorough treatment of division, particularly signed division on int and word
haftmann
parents:
diff
changeset
|
9 |
|
76232
a7ccb744047b
syntactic type classes for signed division operators
haftmann
parents:
76106
diff
changeset
|
10 |
class signed_divide = |
75875
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
11 |
fixes signed_divide :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixl \<open>sdiv\<close> 70) |
76232
a7ccb744047b
syntactic type classes for signed division operators
haftmann
parents:
76106
diff
changeset
|
12 |
|
a7ccb744047b
syntactic type classes for signed division operators
haftmann
parents:
76106
diff
changeset
|
13 |
class signed_modulo = |
a7ccb744047b
syntactic type classes for signed division operators
haftmann
parents:
76106
diff
changeset
|
14 |
fixes signed_modulo :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixl \<open>smod\<close> 70) |
a7ccb744047b
syntactic type classes for signed division operators
haftmann
parents:
76106
diff
changeset
|
15 |
|
a7ccb744047b
syntactic type classes for signed division operators
haftmann
parents:
76106
diff
changeset
|
16 |
class signed_division = comm_semiring_1_cancel + signed_divide + signed_modulo + |
75875
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
17 |
assumes sdiv_mult_smod_eq: \<open>a sdiv b * b + a smod b = a\<close> |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
18 |
begin |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
19 |
|
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
20 |
lemma mult_sdiv_smod_eq: |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
21 |
\<open>b * (a sdiv b) + a smod b = a\<close> |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
22 |
using sdiv_mult_smod_eq [of a b] by (simp add: ac_simps) |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
23 |
|
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
24 |
lemma smod_sdiv_mult_eq: |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
25 |
\<open>a smod b + a sdiv b * b = a\<close> |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
26 |
using sdiv_mult_smod_eq [of a b] by (simp add: ac_simps) |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
27 |
|
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
28 |
lemma smod_mult_sdiv_eq: |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
29 |
\<open>a smod b + b * (a sdiv b) = a\<close> |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
30 |
using sdiv_mult_smod_eq [of a b] by (simp add: ac_simps) |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
31 |
|
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
32 |
lemma minus_sdiv_mult_eq_smod: |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
33 |
\<open>a - a sdiv b * b = a smod b\<close> |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
34 |
by (rule add_implies_diff [symmetric]) (fact smod_sdiv_mult_eq) |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
35 |
|
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
36 |
lemma minus_mult_sdiv_eq_smod: |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
37 |
\<open>a - b * (a sdiv b) = a smod b\<close> |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
38 |
by (rule add_implies_diff [symmetric]) (fact smod_mult_sdiv_eq) |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
39 |
|
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
40 |
lemma minus_smod_eq_sdiv_mult: |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
41 |
\<open>a - a smod b = a sdiv b * b\<close> |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
42 |
by (rule add_implies_diff [symmetric]) (fact sdiv_mult_smod_eq) |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
43 |
|
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
44 |
lemma minus_smod_eq_mult_sdiv: |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
45 |
\<open>a - a smod b = b * (a sdiv b)\<close> |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
46 |
by (rule add_implies_diff [symmetric]) (fact mult_sdiv_smod_eq) |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
47 |
|
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
48 |
end |
72281
beeadb35e357
more thorough treatment of division, particularly signed division on int and word
haftmann
parents:
diff
changeset
|
49 |
|
77812 | 50 |
text \<open> |
79950 | 51 |
\noindent The following specification of division is named ``T-division'' in \<^cite>\<open>"leijen01"\<close>. |
77812 | 52 |
It is motivated by ISO C99, which in turn adopted the typical behavior of |
53 |
hardware modern in the beginning of the 1990ies; but note ISO C99 describes |
|
54 |
the instance on machine words, not mathematical integers. |
|
55 |
\<close> |
|
56 |
||
72281
beeadb35e357
more thorough treatment of division, particularly signed division on int and word
haftmann
parents:
diff
changeset
|
57 |
instantiation int :: signed_division |
beeadb35e357
more thorough treatment of division, particularly signed division on int and word
haftmann
parents:
diff
changeset
|
58 |
begin |
beeadb35e357
more thorough treatment of division, particularly signed division on int and word
haftmann
parents:
diff
changeset
|
59 |
|
beeadb35e357
more thorough treatment of division, particularly signed division on int and word
haftmann
parents:
diff
changeset
|
60 |
definition signed_divide_int :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close> |
beeadb35e357
more thorough treatment of division, particularly signed division on int and word
haftmann
parents:
diff
changeset
|
61 |
where \<open>k sdiv l = sgn k * sgn l * (\<bar>k\<bar> div \<bar>l\<bar>)\<close> for k l :: int |
beeadb35e357
more thorough treatment of division, particularly signed division on int and word
haftmann
parents:
diff
changeset
|
62 |
|
beeadb35e357
more thorough treatment of division, particularly signed division on int and word
haftmann
parents:
diff
changeset
|
63 |
definition signed_modulo_int :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close> |
75875
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
64 |
where \<open>k smod l = sgn k * (\<bar>k\<bar> mod \<bar>l\<bar>)\<close> for k l :: int |
72281
beeadb35e357
more thorough treatment of division, particularly signed division on int and word
haftmann
parents:
diff
changeset
|
65 |
|
75875
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
66 |
instance by standard |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
67 |
(simp add: signed_divide_int_def signed_modulo_int_def div_abs_eq mod_abs_eq algebra_simps) |
72281
beeadb35e357
more thorough treatment of division, particularly signed division on int and word
haftmann
parents:
diff
changeset
|
68 |
|
beeadb35e357
more thorough treatment of division, particularly signed division on int and word
haftmann
parents:
diff
changeset
|
69 |
end |
beeadb35e357
more thorough treatment of division, particularly signed division on int and word
haftmann
parents:
diff
changeset
|
70 |
|
75875
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
71 |
lemma divide_int_eq_signed_divide_int: |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
72 |
\<open>k div l = k sdiv l - of_bool (l \<noteq> 0 \<and> sgn k \<noteq> sgn l \<and> \<not> l dvd k)\<close> |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
73 |
for k l :: int |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
74 |
by (simp add: div_eq_div_abs [of k l] signed_divide_int_def) |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
75 |
|
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
76 |
lemma signed_divide_int_eq_divide_int: |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
77 |
\<open>k sdiv l = k div l + of_bool (l \<noteq> 0 \<and> sgn k \<noteq> sgn l \<and> \<not> l dvd k)\<close> |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
78 |
for k l :: int |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
79 |
by (simp add: divide_int_eq_signed_divide_int) |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
80 |
|
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
81 |
lemma modulo_int_eq_signed_modulo_int: |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
82 |
\<open>k mod l = k smod l + l * of_bool (sgn k \<noteq> sgn l \<and> \<not> l dvd k)\<close> |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
83 |
for k l :: int |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
84 |
by (simp add: mod_eq_mod_abs [of k l] signed_modulo_int_def) |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
85 |
|
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
86 |
lemma signed_modulo_int_eq_modulo_int: |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
87 |
\<open>k smod l = k mod l - l * of_bool (sgn k \<noteq> sgn l \<and> \<not> l dvd k)\<close> |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
88 |
for k l :: int |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
89 |
by (simp add: modulo_int_eq_signed_modulo_int) |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
90 |
|
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
91 |
lemma sdiv_int_div_0: |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
92 |
"(x :: int) sdiv 0 = 0" |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
93 |
by (clarsimp simp: signed_divide_int_def) |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
94 |
|
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
95 |
lemma sdiv_int_0_div [simp]: |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
96 |
"0 sdiv (x :: int) = 0" |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
97 |
by (clarsimp simp: signed_divide_int_def) |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
98 |
|
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
99 |
lemma smod_int_alt_def: |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
100 |
"(a::int) smod b = sgn (a) * (abs a mod abs b)" |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
101 |
by (fact signed_modulo_int_def) |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
102 |
|
72768 | 103 |
lemma int_sdiv_simps [simp]: |
104 |
"(a :: int) sdiv 1 = a" |
|
105 |
"(a :: int) sdiv 0 = 0" |
|
106 |
"(a :: int) sdiv -1 = -a" |
|
107 |
apply (auto simp: signed_divide_int_def sgn_if) |
|
108 |
done |
|
109 |
||
75875
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
110 |
lemma smod_int_mod_0 [simp]: |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
111 |
"x smod (0 :: int) = x" |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
112 |
by (clarsimp simp: signed_modulo_int_def abs_mult_sgn ac_simps) |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
113 |
|
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
114 |
lemma smod_int_0_mod [simp]: |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
115 |
"0 smod (x :: int) = 0" |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
116 |
by (clarsimp simp: smod_int_alt_def) |
72768 | 117 |
|
118 |
lemma sgn_sdiv_eq_sgn_mult: |
|
119 |
"a sdiv b \<noteq> 0 \<Longrightarrow> sgn ((a :: int) sdiv b) = sgn (a * b)" |
|
120 |
by (auto simp: signed_divide_int_def sgn_div_eq_sgn_mult sgn_mult) |
|
121 |
||
122 |
lemma int_sdiv_same_is_1 [simp]: |
|
123 |
"a \<noteq> 0 \<Longrightarrow> ((a :: int) sdiv b = a) = (b = 1)" |
|
124 |
apply (rule iffI) |
|
125 |
apply (clarsimp simp: signed_divide_int_def) |
|
126 |
apply (subgoal_tac "b > 0") |
|
127 |
apply (case_tac "a > 0") |
|
128 |
apply (clarsimp simp: sgn_if) |
|
129 |
apply (simp_all add: not_less algebra_split_simps sgn_if split: if_splits) |
|
130 |
using int_div_less_self [of a b] apply linarith |
|
131 |
apply (metis add.commute add.inverse_inverse group_cancel.rule0 int_div_less_self linorder_neqE_linordered_idom neg_0_le_iff_le not_less verit_comp_simplify1(1) zless_imp_add1_zle) |
|
132 |
apply (metis div_minus_right neg_imp_zdiv_neg_iff neg_le_0_iff_le not_less order.not_eq_order_implies_strict) |
|
133 |
apply (metis abs_le_zero_iff abs_of_nonneg neg_imp_zdiv_nonneg_iff order.not_eq_order_implies_strict) |
|
134 |
done |
|
135 |
||
136 |
lemma int_sdiv_negated_is_minus1 [simp]: |
|
137 |
"a \<noteq> 0 \<Longrightarrow> ((a :: int) sdiv b = - a) = (b = -1)" |
|
138 |
apply (clarsimp simp: signed_divide_int_def) |
|
139 |
apply (rule iffI) |
|
140 |
apply (subgoal_tac "b < 0") |
|
141 |
apply (case_tac "a > 0") |
|
142 |
apply (clarsimp simp: sgn_if algebra_split_simps not_less) |
|
143 |
apply (case_tac "sgn (a * b) = -1") |
|
144 |
apply (simp_all add: not_less algebra_split_simps sgn_if split: if_splits) |
|
145 |
apply (metis add.inverse_inverse int_div_less_self int_one_le_iff_zero_less less_le neg_0_less_iff_less) |
|
146 |
apply (metis add.inverse_inverse div_minus_right int_div_less_self int_one_le_iff_zero_less less_le neg_0_less_iff_less) |
|
147 |
apply (metis less_le neg_less_0_iff_less not_less pos_imp_zdiv_neg_iff) |
|
148 |
apply (metis div_minus_right dual_order.eq_iff neg_imp_zdiv_nonneg_iff neg_less_0_iff_less) |
|
149 |
done |
|
150 |
||
151 |
lemma sdiv_int_range: |
|
75875
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
152 |
\<open>a sdiv b \<in> {- \<bar>a\<bar>..\<bar>a\<bar>}\<close> for a b :: int |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
153 |
using zdiv_mono2 [of \<open>\<bar>a\<bar>\<close> 1 \<open>\<bar>b\<bar>\<close>] |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
154 |
by (cases \<open>b = 0\<close>; cases \<open>sgn b = sgn a\<close>) |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
155 |
(auto simp add: signed_divide_int_def pos_imp_zdiv_nonneg_iff |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
156 |
dest!: sgn_not_eq_imp intro: order_trans [of _ 0]) |
72768 | 157 |
|
158 |
lemma smod_int_range: |
|
75875
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
159 |
\<open>a smod b \<in> {- \<bar>b\<bar> + 1..\<bar>b\<bar> - 1}\<close> |
48d032035744
streamlined primitive definitions for integer division
haftmann
parents:
74592
diff
changeset
|
160 |
if \<open>b \<noteq> 0\<close> for a b :: int |
76106 | 161 |
proof - |
162 |
define m n where \<open>m = nat \<bar>a\<bar>\<close> \<open>n = nat \<bar>b\<bar>\<close> |
|
163 |
then have \<open>\<bar>a\<bar> = int m\<close> \<open>\<bar>b\<bar> = int n\<close> |
|
164 |
by simp_all |
|
165 |
with that have \<open>n > 0\<close> |
|
166 |
by simp |
|
167 |
with signed_modulo_int_def [of a b] \<open>\<bar>a\<bar> = int m\<close> \<open>\<bar>b\<bar> = int n\<close> |
|
168 |
show ?thesis |
|
169 |
by (auto simp add: sgn_if diff_le_eq int_one_le_iff_zero_less simp flip: of_nat_mod of_nat_diff) |
|
170 |
qed |
|
72768 | 171 |
|
172 |
lemma smod_int_compares: |
|
173 |
"\<lbrakk> 0 \<le> a; 0 < b \<rbrakk> \<Longrightarrow> (a :: int) smod b < b" |
|
174 |
"\<lbrakk> 0 \<le> a; 0 < b \<rbrakk> \<Longrightarrow> 0 \<le> (a :: int) smod b" |
|
175 |
"\<lbrakk> a \<le> 0; 0 < b \<rbrakk> \<Longrightarrow> -b < (a :: int) smod b" |
|
176 |
"\<lbrakk> a \<le> 0; 0 < b \<rbrakk> \<Longrightarrow> (a :: int) smod b \<le> 0" |
|
177 |
"\<lbrakk> 0 \<le> a; b < 0 \<rbrakk> \<Longrightarrow> (a :: int) smod b < - b" |
|
178 |
"\<lbrakk> 0 \<le> a; b < 0 \<rbrakk> \<Longrightarrow> 0 \<le> (a :: int) smod b" |
|
179 |
"\<lbrakk> a \<le> 0; b < 0 \<rbrakk> \<Longrightarrow> (a :: int) smod b \<le> 0" |
|
180 |
"\<lbrakk> a \<le> 0; b < 0 \<rbrakk> \<Longrightarrow> b \<le> (a :: int) smod b" |
|
181 |
apply (insert smod_int_range [where a=a and b=b]) |
|
182 |
apply (auto simp: add1_zle_eq smod_int_alt_def sgn_if) |
|
183 |
done |
|
184 |
||
185 |
lemma smod_mod_positive: |
|
186 |
"\<lbrakk> 0 \<le> (a :: int); 0 \<le> b \<rbrakk> \<Longrightarrow> a smod b = a mod b" |
|
187 |
by (clarsimp simp: smod_int_alt_def zsgn_def) |
|
188 |
||
74592 | 189 |
lemma minus_sdiv_eq [simp]: |
190 |
\<open>- k sdiv l = - (k sdiv l)\<close> for k l :: int |
|
191 |
by (simp add: signed_divide_int_def) |
|
192 |
||
193 |
lemma sdiv_minus_eq [simp]: |
|
194 |
\<open>k sdiv - l = - (k sdiv l)\<close> for k l :: int |
|
195 |
by (simp add: signed_divide_int_def) |
|
196 |
||
197 |
lemma sdiv_int_numeral_numeral [simp]: |
|
198 |
\<open>numeral m sdiv numeral n = numeral m div (numeral n :: int)\<close> |
|
199 |
by (simp add: signed_divide_int_def) |
|
200 |
||
201 |
lemma minus_smod_eq [simp]: |
|
202 |
\<open>- k smod l = - (k smod l)\<close> for k l :: int |
|
203 |
by (simp add: smod_int_alt_def) |
|
204 |
||
205 |
lemma smod_minus_eq [simp]: |
|
206 |
\<open>k smod - l = k smod l\<close> for k l :: int |
|
207 |
by (simp add: smod_int_alt_def) |
|
208 |
||
209 |
lemma smod_int_numeral_numeral [simp]: |
|
210 |
\<open>numeral m smod numeral n = numeral m mod (numeral n :: int)\<close> |
|
211 |
by (simp add: smod_int_alt_def) |
|
212 |
||
72281
beeadb35e357
more thorough treatment of division, particularly signed division on int and word
haftmann
parents:
diff
changeset
|
213 |
end |