src/HOL/Euclidean_Division.thy
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (21 months ago)
changeset 66695 91500c024c7f
parent 64785 ae0bbc8e45ad
child 66798 39bb2462e681
permissions -rw-r--r--
tuned;
     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 end
   196 
   197 class euclidean_ring = idom_modulo + euclidean_semiring
   198 
   199   
   200 subsection \<open>Uniquely determined division\<close>
   201   
   202 class unique_euclidean_semiring = euclidean_semiring + 
   203   fixes uniqueness_constraint :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   204   assumes size_mono_mult:
   205     "b \<noteq> 0 \<Longrightarrow> euclidean_size a < euclidean_size c
   206       \<Longrightarrow> euclidean_size (a * b) < euclidean_size (c * b)"
   207     -- \<open>FIXME justify\<close>
   208   assumes uniqueness_constraint_mono_mult:
   209     "uniqueness_constraint a b \<Longrightarrow> uniqueness_constraint (a * c) (b * c)"
   210   assumes uniqueness_constraint_mod:
   211     "b \<noteq> 0 \<Longrightarrow> \<not> b dvd a \<Longrightarrow> uniqueness_constraint (a mod b) b"
   212   assumes div_bounded:
   213     "b \<noteq> 0 \<Longrightarrow> uniqueness_constraint r b
   214     \<Longrightarrow> euclidean_size r < euclidean_size b
   215     \<Longrightarrow> (q * b + r) div b = q"
   216 begin
   217 
   218 lemma divmod_cases [case_names divides remainder by0]:
   219   obtains 
   220     (divides) q where "b \<noteq> 0"
   221       and "a div b = q"
   222       and "a mod b = 0"
   223       and "a = q * b"
   224   | (remainder) q r where "b \<noteq> 0" and "r \<noteq> 0"
   225       and "uniqueness_constraint r b"
   226       and "euclidean_size r < euclidean_size b"
   227       and "a div b = q"
   228       and "a mod b = r"
   229       and "a = q * b + r"
   230   | (by0) "b = 0"
   231 proof (cases "b = 0")
   232   case True
   233   then show thesis
   234   by (rule by0)
   235 next
   236   case False
   237   show thesis
   238   proof (cases "b dvd a")
   239     case True
   240     then obtain q where "a = b * q" ..
   241     with \<open>b \<noteq> 0\<close> divides
   242     show thesis
   243       by (simp add: ac_simps)
   244   next
   245     case False
   246     then have "a mod b \<noteq> 0"
   247       by (simp add: mod_eq_0_iff_dvd)
   248     moreover from \<open>b \<noteq> 0\<close> \<open>\<not> b dvd a\<close> have "uniqueness_constraint (a mod b) b"
   249       by (rule uniqueness_constraint_mod)
   250     moreover have "euclidean_size (a mod b) < euclidean_size b"
   251       using \<open>b \<noteq> 0\<close> by (rule mod_size_less)
   252     moreover have "a = a div b * b + a mod b"
   253       by (simp add: div_mult_mod_eq)
   254     ultimately show thesis
   255       using \<open>b \<noteq> 0\<close> by (blast intro: remainder)
   256   qed
   257 qed
   258 
   259 lemma div_eqI:
   260   "a div b = q" if "b \<noteq> 0" "uniqueness_constraint r b"
   261     "euclidean_size r < euclidean_size b" "q * b + r = a"
   262 proof -
   263   from that have "(q * b + r) div b = q"
   264     by (auto intro: div_bounded)
   265   with that show ?thesis
   266     by simp
   267 qed
   268 
   269 lemma mod_eqI:
   270   "a mod b = r" if "b \<noteq> 0" "uniqueness_constraint r b"
   271     "euclidean_size r < euclidean_size b" "q * b + r = a" 
   272 proof -
   273   from that have "a div b = q"
   274     by (rule div_eqI)
   275   moreover have "a div b * b + a mod b = a"
   276     by (fact div_mult_mod_eq)
   277   ultimately have "a div b * b + a mod b = a div b * b + r"
   278     using \<open>q * b + r = a\<close> by simp
   279   then show ?thesis
   280     by simp
   281 qed
   282 
   283 end
   284 
   285 class unique_euclidean_ring = euclidean_ring + unique_euclidean_semiring
   286 
   287 end