src/HOL/Euclidean_Division.thy
author haftmann
Sun Oct 08 22:28:19 2017 +0200 (21 months ago)
changeset 66798 39bb2462e681
parent 64785 ae0bbc8e45ad
child 66806 a4e82b58d833
permissions -rw-r--r--
fundamental property of division by units
haftmann@64785
     1
(*  Title:      HOL/Euclidean_Division.thy
haftmann@64785
     2
    Author:     Manuel Eberl, TU Muenchen
haftmann@64785
     3
    Author:     Florian Haftmann, TU Muenchen
haftmann@64785
     4
*)
haftmann@64785
     5
haftmann@64785
     6
section \<open>Uniquely determined division in euclidean (semi)rings\<close>
haftmann@64785
     7
haftmann@64785
     8
theory Euclidean_Division
haftmann@64785
     9
  imports Nat_Transfer
haftmann@64785
    10
begin
haftmann@64785
    11
haftmann@64785
    12
subsection \<open>Quotient and remainder in integral domains\<close>
haftmann@64785
    13
haftmann@64785
    14
class semidom_modulo = algebraic_semidom + semiring_modulo
haftmann@64785
    15
begin
haftmann@64785
    16
haftmann@64785
    17
lemma mod_0 [simp]: "0 mod a = 0"
haftmann@64785
    18
  using div_mult_mod_eq [of 0 a] by simp
haftmann@64785
    19
haftmann@64785
    20
lemma mod_by_0 [simp]: "a mod 0 = a"
haftmann@64785
    21
  using div_mult_mod_eq [of a 0] by simp
haftmann@64785
    22
haftmann@64785
    23
lemma mod_by_1 [simp]:
haftmann@64785
    24
  "a mod 1 = 0"
haftmann@64785
    25
proof -
haftmann@64785
    26
  from div_mult_mod_eq [of a one] div_by_1 have "a + a mod 1 = a" by simp
haftmann@64785
    27
  then have "a + a mod 1 = a + 0" by simp
haftmann@64785
    28
  then show ?thesis by (rule add_left_imp_eq)
haftmann@64785
    29
qed
haftmann@64785
    30
haftmann@64785
    31
lemma mod_self [simp]:
haftmann@64785
    32
  "a mod a = 0"
haftmann@64785
    33
  using div_mult_mod_eq [of a a] by simp
haftmann@64785
    34
haftmann@64785
    35
lemma dvd_imp_mod_0 [simp]:
haftmann@64785
    36
  assumes "a dvd b"
haftmann@64785
    37
  shows "b mod a = 0"
haftmann@64785
    38
  using assms minus_div_mult_eq_mod [of b a] by simp
haftmann@64785
    39
haftmann@64785
    40
lemma mod_0_imp_dvd: 
haftmann@64785
    41
  assumes "a mod b = 0"
haftmann@64785
    42
  shows   "b dvd a"
haftmann@64785
    43
proof -
haftmann@64785
    44
  have "b dvd ((a div b) * b)" by simp
haftmann@64785
    45
  also have "(a div b) * b = a"
haftmann@64785
    46
    using div_mult_mod_eq [of a b] by (simp add: assms)
haftmann@64785
    47
  finally show ?thesis .
haftmann@64785
    48
qed
haftmann@64785
    49
haftmann@64785
    50
lemma mod_eq_0_iff_dvd:
haftmann@64785
    51
  "a mod b = 0 \<longleftrightarrow> b dvd a"
haftmann@64785
    52
  by (auto intro: mod_0_imp_dvd)
haftmann@64785
    53
haftmann@64785
    54
lemma dvd_eq_mod_eq_0 [nitpick_unfold, code]:
haftmann@64785
    55
  "a dvd b \<longleftrightarrow> b mod a = 0"
haftmann@64785
    56
  by (simp add: mod_eq_0_iff_dvd)
haftmann@64785
    57
haftmann@64785
    58
lemma dvd_mod_iff: 
haftmann@64785
    59
  assumes "c dvd b"
haftmann@64785
    60
  shows "c dvd a mod b \<longleftrightarrow> c dvd a"
haftmann@64785
    61
proof -
haftmann@64785
    62
  from assms have "(c dvd a mod b) \<longleftrightarrow> (c dvd ((a div b) * b + a mod b))" 
haftmann@64785
    63
    by (simp add: dvd_add_right_iff)
haftmann@64785
    64
  also have "(a div b) * b + a mod b = a"
haftmann@64785
    65
    using div_mult_mod_eq [of a b] by simp
haftmann@64785
    66
  finally show ?thesis .
haftmann@64785
    67
qed
haftmann@64785
    68
haftmann@64785
    69
lemma dvd_mod_imp_dvd:
haftmann@64785
    70
  assumes "c dvd a mod b" and "c dvd b"
haftmann@64785
    71
  shows "c dvd a"
haftmann@64785
    72
  using assms dvd_mod_iff [of c b a] by simp
haftmann@64785
    73
haftmann@64785
    74
end
haftmann@64785
    75
haftmann@64785
    76
class idom_modulo = idom + semidom_modulo
haftmann@64785
    77
begin
haftmann@64785
    78
haftmann@64785
    79
subclass idom_divide ..
haftmann@64785
    80
haftmann@64785
    81
lemma div_diff [simp]:
haftmann@64785
    82
  "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> (a - b) div c = a div c - b div c"
haftmann@64785
    83
  using div_add [of _  _ "- b"] by (simp add: dvd_neg_div)
haftmann@64785
    84
haftmann@64785
    85
end
haftmann@64785
    86
haftmann@64785
    87
  
haftmann@64785
    88
subsection \<open>Euclidean (semi)rings with explicit division and remainder\<close>
haftmann@64785
    89
  
haftmann@64785
    90
class euclidean_semiring = semidom_modulo + normalization_semidom + 
haftmann@64785
    91
  fixes euclidean_size :: "'a \<Rightarrow> nat"
haftmann@64785
    92
  assumes size_0 [simp]: "euclidean_size 0 = 0"
haftmann@64785
    93
  assumes mod_size_less: 
haftmann@64785
    94
    "b \<noteq> 0 \<Longrightarrow> euclidean_size (a mod b) < euclidean_size b"
haftmann@64785
    95
  assumes size_mult_mono:
haftmann@64785
    96
    "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (a * b)"
haftmann@64785
    97
begin
haftmann@64785
    98
haftmann@64785
    99
lemma size_mult_mono': "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (b * a)"
haftmann@64785
   100
  by (subst mult.commute) (rule size_mult_mono)
haftmann@64785
   101
haftmann@64785
   102
lemma euclidean_size_normalize [simp]:
haftmann@64785
   103
  "euclidean_size (normalize a) = euclidean_size a"
haftmann@64785
   104
proof (cases "a = 0")
haftmann@64785
   105
  case True
haftmann@64785
   106
  then show ?thesis
haftmann@64785
   107
    by simp
haftmann@64785
   108
next
haftmann@64785
   109
  case [simp]: False
haftmann@64785
   110
  have "euclidean_size (normalize a) \<le> euclidean_size (normalize a * unit_factor a)"
haftmann@64785
   111
    by (rule size_mult_mono) simp
haftmann@64785
   112
  moreover have "euclidean_size a \<le> euclidean_size (a * (1 div unit_factor a))"
haftmann@64785
   113
    by (rule size_mult_mono) simp
haftmann@64785
   114
  ultimately show ?thesis
haftmann@64785
   115
    by simp
haftmann@64785
   116
qed
haftmann@64785
   117
haftmann@64785
   118
lemma dvd_euclidean_size_eq_imp_dvd:
haftmann@64785
   119
  assumes "a \<noteq> 0" and "euclidean_size a = euclidean_size b"
haftmann@64785
   120
    and "b dvd a" 
haftmann@64785
   121
  shows "a dvd b"
haftmann@64785
   122
proof (rule ccontr)
haftmann@64785
   123
  assume "\<not> a dvd b"
haftmann@64785
   124
  hence "b mod a \<noteq> 0" using mod_0_imp_dvd [of b a] by blast
haftmann@64785
   125
  then have "b mod a \<noteq> 0" by (simp add: mod_eq_0_iff_dvd)
haftmann@64785
   126
  from \<open>b dvd a\<close> have "b dvd b mod a" by (simp add: dvd_mod_iff)
haftmann@64785
   127
  then obtain c where "b mod a = b * c" unfolding dvd_def by blast
haftmann@64785
   128
    with \<open>b mod a \<noteq> 0\<close> have "c \<noteq> 0" by auto
haftmann@64785
   129
  with \<open>b mod a = b * c\<close> have "euclidean_size (b mod a) \<ge> euclidean_size b"
haftmann@64785
   130
    using size_mult_mono by force
haftmann@64785
   131
  moreover from \<open>\<not> a dvd b\<close> and \<open>a \<noteq> 0\<close>
haftmann@64785
   132
  have "euclidean_size (b mod a) < euclidean_size a"
haftmann@64785
   133
    using mod_size_less by blast
haftmann@64785
   134
  ultimately show False using \<open>euclidean_size a = euclidean_size b\<close>
haftmann@64785
   135
    by simp
haftmann@64785
   136
qed
haftmann@64785
   137
haftmann@64785
   138
lemma euclidean_size_times_unit:
haftmann@64785
   139
  assumes "is_unit a"
haftmann@64785
   140
  shows   "euclidean_size (a * b) = euclidean_size b"
haftmann@64785
   141
proof (rule antisym)
haftmann@64785
   142
  from assms have [simp]: "a \<noteq> 0" by auto
haftmann@64785
   143
  thus "euclidean_size (a * b) \<ge> euclidean_size b" by (rule size_mult_mono')
haftmann@64785
   144
  from assms have "is_unit (1 div a)" by simp
haftmann@64785
   145
  hence "1 div a \<noteq> 0" by (intro notI) simp_all
haftmann@64785
   146
  hence "euclidean_size (a * b) \<le> euclidean_size ((1 div a) * (a * b))"
haftmann@64785
   147
    by (rule size_mult_mono')
haftmann@64785
   148
  also from assms have "(1 div a) * (a * b) = b"
haftmann@64785
   149
    by (simp add: algebra_simps unit_div_mult_swap)
haftmann@64785
   150
  finally show "euclidean_size (a * b) \<le> euclidean_size b" .
haftmann@64785
   151
qed
haftmann@64785
   152
haftmann@64785
   153
lemma euclidean_size_unit:
haftmann@64785
   154
  "is_unit a \<Longrightarrow> euclidean_size a = euclidean_size 1"
haftmann@64785
   155
  using euclidean_size_times_unit [of a 1] by simp
haftmann@64785
   156
haftmann@64785
   157
lemma unit_iff_euclidean_size: 
haftmann@64785
   158
  "is_unit a \<longleftrightarrow> euclidean_size a = euclidean_size 1 \<and> a \<noteq> 0"
haftmann@64785
   159
proof safe
haftmann@64785
   160
  assume A: "a \<noteq> 0" and B: "euclidean_size a = euclidean_size 1"
haftmann@64785
   161
  show "is_unit a"
haftmann@64785
   162
    by (rule dvd_euclidean_size_eq_imp_dvd [OF A B]) simp_all
haftmann@64785
   163
qed (auto intro: euclidean_size_unit)
haftmann@64785
   164
haftmann@64785
   165
lemma euclidean_size_times_nonunit:
haftmann@64785
   166
  assumes "a \<noteq> 0" "b \<noteq> 0" "\<not> is_unit a"
haftmann@64785
   167
  shows   "euclidean_size b < euclidean_size (a * b)"
haftmann@64785
   168
proof (rule ccontr)
haftmann@64785
   169
  assume "\<not>euclidean_size b < euclidean_size (a * b)"
haftmann@64785
   170
  with size_mult_mono'[OF assms(1), of b] 
haftmann@64785
   171
    have eq: "euclidean_size (a * b) = euclidean_size b" by simp
haftmann@64785
   172
  have "a * b dvd b"
haftmann@64785
   173
    by (rule dvd_euclidean_size_eq_imp_dvd [OF _ eq]) (insert assms, simp_all)
haftmann@64785
   174
  hence "a * b dvd 1 * b" by simp
haftmann@64785
   175
  with \<open>b \<noteq> 0\<close> have "is_unit a" by (subst (asm) dvd_times_right_cancel_iff)
haftmann@64785
   176
  with assms(3) show False by contradiction
haftmann@64785
   177
qed
haftmann@64785
   178
haftmann@64785
   179
lemma dvd_imp_size_le:
haftmann@64785
   180
  assumes "a dvd b" "b \<noteq> 0" 
haftmann@64785
   181
  shows   "euclidean_size a \<le> euclidean_size b"
haftmann@64785
   182
  using assms by (auto elim!: dvdE simp: size_mult_mono)
haftmann@64785
   183
haftmann@64785
   184
lemma dvd_proper_imp_size_less:
haftmann@64785
   185
  assumes "a dvd b" "\<not> b dvd a" "b \<noteq> 0" 
haftmann@64785
   186
  shows   "euclidean_size a < euclidean_size b"
haftmann@64785
   187
proof -
haftmann@64785
   188
  from assms(1) obtain c where "b = a * c" by (erule dvdE)
haftmann@64785
   189
  hence z: "b = c * a" by (simp add: mult.commute)
haftmann@64785
   190
  from z assms have "\<not>is_unit c" by (auto simp: mult.commute mult_unit_dvd_iff)
haftmann@64785
   191
  with z assms show ?thesis
haftmann@64785
   192
    by (auto intro!: euclidean_size_times_nonunit)
haftmann@64785
   193
qed
haftmann@64785
   194
haftmann@66798
   195
lemma unit_imp_mod_eq_0:
haftmann@66798
   196
  "a mod b = 0" if "is_unit b"
haftmann@66798
   197
  using that by (simp add: mod_eq_0_iff_dvd unit_imp_dvd)
haftmann@66798
   198
haftmann@64785
   199
end
haftmann@64785
   200
haftmann@64785
   201
class euclidean_ring = idom_modulo + euclidean_semiring
haftmann@64785
   202
haftmann@64785
   203
  
haftmann@64785
   204
subsection \<open>Uniquely determined division\<close>
haftmann@64785
   205
  
haftmann@64785
   206
class unique_euclidean_semiring = euclidean_semiring + 
haftmann@64785
   207
  fixes uniqueness_constraint :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
haftmann@64785
   208
  assumes size_mono_mult:
haftmann@64785
   209
    "b \<noteq> 0 \<Longrightarrow> euclidean_size a < euclidean_size c
haftmann@64785
   210
      \<Longrightarrow> euclidean_size (a * b) < euclidean_size (c * b)"
haftmann@64785
   211
    -- \<open>FIXME justify\<close>
haftmann@64785
   212
  assumes uniqueness_constraint_mono_mult:
haftmann@64785
   213
    "uniqueness_constraint a b \<Longrightarrow> uniqueness_constraint (a * c) (b * c)"
haftmann@64785
   214
  assumes uniqueness_constraint_mod:
haftmann@64785
   215
    "b \<noteq> 0 \<Longrightarrow> \<not> b dvd a \<Longrightarrow> uniqueness_constraint (a mod b) b"
haftmann@64785
   216
  assumes div_bounded:
haftmann@64785
   217
    "b \<noteq> 0 \<Longrightarrow> uniqueness_constraint r b
haftmann@64785
   218
    \<Longrightarrow> euclidean_size r < euclidean_size b
haftmann@64785
   219
    \<Longrightarrow> (q * b + r) div b = q"
haftmann@64785
   220
begin
haftmann@64785
   221
haftmann@64785
   222
lemma divmod_cases [case_names divides remainder by0]:
haftmann@64785
   223
  obtains 
haftmann@64785
   224
    (divides) q where "b \<noteq> 0"
haftmann@64785
   225
      and "a div b = q"
haftmann@64785
   226
      and "a mod b = 0"
haftmann@64785
   227
      and "a = q * b"
haftmann@64785
   228
  | (remainder) q r where "b \<noteq> 0" and "r \<noteq> 0"
haftmann@64785
   229
      and "uniqueness_constraint r b"
haftmann@64785
   230
      and "euclidean_size r < euclidean_size b"
haftmann@64785
   231
      and "a div b = q"
haftmann@64785
   232
      and "a mod b = r"
haftmann@64785
   233
      and "a = q * b + r"
haftmann@64785
   234
  | (by0) "b = 0"
haftmann@64785
   235
proof (cases "b = 0")
haftmann@64785
   236
  case True
haftmann@64785
   237
  then show thesis
haftmann@64785
   238
  by (rule by0)
haftmann@64785
   239
next
haftmann@64785
   240
  case False
haftmann@64785
   241
  show thesis
haftmann@64785
   242
  proof (cases "b dvd a")
haftmann@64785
   243
    case True
haftmann@64785
   244
    then obtain q where "a = b * q" ..
haftmann@64785
   245
    with \<open>b \<noteq> 0\<close> divides
haftmann@64785
   246
    show thesis
haftmann@64785
   247
      by (simp add: ac_simps)
haftmann@64785
   248
  next
haftmann@64785
   249
    case False
haftmann@64785
   250
    then have "a mod b \<noteq> 0"
haftmann@64785
   251
      by (simp add: mod_eq_0_iff_dvd)
haftmann@64785
   252
    moreover from \<open>b \<noteq> 0\<close> \<open>\<not> b dvd a\<close> have "uniqueness_constraint (a mod b) b"
haftmann@64785
   253
      by (rule uniqueness_constraint_mod)
haftmann@64785
   254
    moreover have "euclidean_size (a mod b) < euclidean_size b"
haftmann@64785
   255
      using \<open>b \<noteq> 0\<close> by (rule mod_size_less)
haftmann@64785
   256
    moreover have "a = a div b * b + a mod b"
haftmann@64785
   257
      by (simp add: div_mult_mod_eq)
haftmann@64785
   258
    ultimately show thesis
haftmann@64785
   259
      using \<open>b \<noteq> 0\<close> by (blast intro: remainder)
haftmann@64785
   260
  qed
haftmann@64785
   261
qed
haftmann@64785
   262
haftmann@64785
   263
lemma div_eqI:
haftmann@64785
   264
  "a div b = q" if "b \<noteq> 0" "uniqueness_constraint r b"
haftmann@64785
   265
    "euclidean_size r < euclidean_size b" "q * b + r = a"
haftmann@64785
   266
proof -
haftmann@64785
   267
  from that have "(q * b + r) div b = q"
haftmann@64785
   268
    by (auto intro: div_bounded)
haftmann@64785
   269
  with that show ?thesis
haftmann@64785
   270
    by simp
haftmann@64785
   271
qed
haftmann@64785
   272
haftmann@64785
   273
lemma mod_eqI:
haftmann@64785
   274
  "a mod b = r" if "b \<noteq> 0" "uniqueness_constraint r b"
haftmann@64785
   275
    "euclidean_size r < euclidean_size b" "q * b + r = a" 
haftmann@64785
   276
proof -
haftmann@64785
   277
  from that have "a div b = q"
haftmann@64785
   278
    by (rule div_eqI)
haftmann@64785
   279
  moreover have "a div b * b + a mod b = a"
haftmann@64785
   280
    by (fact div_mult_mod_eq)
haftmann@64785
   281
  ultimately have "a div b * b + a mod b = a div b * b + r"
haftmann@64785
   282
    using \<open>q * b + r = a\<close> by simp
haftmann@64785
   283
  then show ?thesis
haftmann@64785
   284
    by simp
haftmann@64785
   285
qed
haftmann@64785
   286
haftmann@64785
   287
end
haftmann@64785
   288
haftmann@64785
   289
class unique_euclidean_ring = euclidean_ring + unique_euclidean_semiring
haftmann@64785
   290
haftmann@64785
   291
end