5 |
5 |
6 theory Divides |
6 theory Divides |
7 imports Parity |
7 imports Parity |
8 begin |
8 begin |
9 |
9 |
10 class unique_euclidean_semiring_numeral = unique_euclidean_semiring_with_nat + linordered_semidom + |
10 class unique_euclidean_semiring_numeral = unique_euclidean_semiring_with_nat + discrete_linordered_semidom + |
11 assumes div_less [no_atp]: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0" |
11 assumes div_less [no_atp]: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0" |
12 and mod_less [no_atp]: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a" |
12 and mod_less [no_atp]: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a" |
13 and div_positive [no_atp]: "0 < b \<Longrightarrow> b \<le> a \<Longrightarrow> a div b > 0" |
13 and div_positive [no_atp]: "0 < b \<Longrightarrow> b \<le> a \<Longrightarrow> a div b > 0" |
14 and mod_less_eq_dividend [no_atp]: "0 \<le> a \<Longrightarrow> a mod b \<le> a" |
14 and mod_less_eq_dividend [no_atp]: "0 \<le> a \<Longrightarrow> a mod b \<le> a" |
15 and pos_mod_bound [no_atp]: "0 < b \<Longrightarrow> a mod b < b" |
15 and pos_mod_bound [no_atp]: "0 < b \<Longrightarrow> a mod b < b" |
16 and pos_mod_sign [no_atp]: "0 < b \<Longrightarrow> 0 \<le> a mod b" |
16 and pos_mod_sign [no_atp]: "0 < b \<Longrightarrow> 0 \<le> a mod b" |
17 and mod_mult2_eq [no_atp]: "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b" |
17 and mod_mult2_eq [no_atp]: "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b" |
18 and div_mult2_eq [no_atp]: "0 \<le> c \<Longrightarrow> a div (b * c) = a div b div c" |
18 and div_mult2_eq [no_atp]: "0 \<le> c \<Longrightarrow> a div (b * c) = a div b div c" |
19 assumes discrete [no_atp]: "a < b \<longleftrightarrow> a + 1 \<le> b" |
|
20 |
19 |
21 hide_fact (open) div_less mod_less div_positive mod_less_eq_dividend pos_mod_bound pos_mod_sign mod_mult2_eq div_mult2_eq discrete |
20 hide_fact (open) div_less mod_less div_positive mod_less_eq_dividend pos_mod_bound pos_mod_sign mod_mult2_eq div_mult2_eq |
22 |
21 |
23 context unique_euclidean_semiring_numeral |
22 context unique_euclidean_semiring_numeral |
24 begin |
23 begin |
25 |
24 |
26 context |
25 context |
27 begin |
26 begin |
|
27 |
|
28 qualified lemma discrete [no_atp]: |
|
29 "a < b \<longleftrightarrow> a + 1 \<le> b" |
|
30 by (fact less_iff_succ_less_eq) |
28 |
31 |
29 qualified lemma divmod_digit_1 [no_atp]: |
32 qualified lemma divmod_digit_1 [no_atp]: |
30 assumes "0 \<le> a" "0 < b" and "b \<le> a mod (2 * b)" |
33 assumes "0 \<le> a" "0 < b" and "b \<le> a mod (2 * b)" |
31 shows "2 * (a div (2 * b)) + 1 = a div b" (is "?P") |
34 shows "2 * (a div (2 * b)) + 1 = a div b" (is "?P") |
32 and "a mod (2 * b) - b = a mod b" (is "?Q") |
35 and "a mod (2 * b) - b = a mod b" (is "?Q") |