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