src/HOL/Computational_Algebra/Euclidean_Algorithm.thy
author Manuel Eberl <eberlm@in.tum.de>
Tue Dec 12 10:01:14 2017 +0100 (18 months ago)
changeset 67167 88d1c9d86f48
parent 66817 0b12755ccbb2
child 67399 eab6ce8368fa
permissions -rw-r--r--
Moved analysis material from AFP
wenzelm@65435
     1
(*  Title:      HOL/Computational_Algebra/Euclidean_Algorithm.thy
haftmann@64784
     2
    Author:     Manuel Eberl, TU Muenchen
haftmann@64784
     3
*)
haftmann@58023
     4
haftmann@64784
     5
section \<open>Abstract euclidean algorithm in euclidean (semi)rings\<close>
haftmann@58023
     6
haftmann@58023
     7
theory Euclidean_Algorithm
haftmann@65417
     8
  imports Factorial_Ring
haftmann@58023
     9
begin
haftmann@58023
    10
haftmann@64786
    11
subsection \<open>Generic construction of the (simple) euclidean algorithm\<close>
haftmann@66817
    12
haftmann@66817
    13
class normalization_euclidean_semiring = euclidean_semiring + normalization_semidom
haftmann@64784
    14
begin
eberlm@63498
    15
haftmann@66817
    16
lemma euclidean_size_normalize [simp]:
haftmann@66817
    17
  "euclidean_size (normalize a) = euclidean_size a"
haftmann@66817
    18
proof (cases "a = 0")
haftmann@66817
    19
  case True
haftmann@66817
    20
  then show ?thesis
haftmann@66817
    21
    by simp
haftmann@66817
    22
next
haftmann@66817
    23
  case [simp]: False
haftmann@66817
    24
  have "euclidean_size (normalize a) \<le> euclidean_size (normalize a * unit_factor a)"
haftmann@66817
    25
    by (rule size_mult_mono) simp
haftmann@66817
    26
  moreover have "euclidean_size a \<le> euclidean_size (a * (1 div unit_factor a))"
haftmann@66817
    27
    by (rule size_mult_mono) simp
haftmann@66817
    28
  ultimately show ?thesis
haftmann@66817
    29
    by simp
haftmann@66817
    30
qed
haftmann@66817
    31
haftmann@64786
    32
context
haftmann@64786
    33
begin
haftmann@64786
    34
haftmann@64786
    35
qualified function gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
haftmann@64786
    36
  where "gcd a b = (if b = 0 then normalize a else gcd b (a mod b))"
haftmann@60572
    37
  by pat_completeness simp
haftmann@60569
    38
termination
haftmann@60569
    39
  by (relation "measure (euclidean_size \<circ> snd)") (simp_all add: mod_size_less)
haftmann@58023
    40
haftmann@64786
    41
declare gcd.simps [simp del]
haftmann@58023
    42
haftmann@64786
    43
lemma eucl_induct [case_names zero mod]:
haftmann@60569
    44
  assumes H1: "\<And>b. P b 0"
haftmann@60569
    45
  and H2: "\<And>a b. b \<noteq> 0 \<Longrightarrow> P b (a mod b) \<Longrightarrow> P a b"
haftmann@60569
    46
  shows "P a b"
haftmann@64786
    47
proof (induct a b rule: gcd.induct)
haftmann@64786
    48
  case (1 a b)
haftmann@60569
    49
  show ?case
haftmann@60569
    50
  proof (cases "b = 0")
haftmann@60569
    51
    case True then show "P a b" by simp (rule H1)
haftmann@60569
    52
  next
haftmann@60569
    53
    case False
haftmann@60600
    54
    then have "P b (a mod b)"
haftmann@60600
    55
      by (rule "1.hyps")
haftmann@60569
    56
    with \<open>b \<noteq> 0\<close> show "P a b"
haftmann@60569
    57
      by (blast intro: H2)
haftmann@60569
    58
  qed
haftmann@58023
    59
qed
haftmann@64786
    60
  
haftmann@64786
    61
qualified lemma gcd_0:
haftmann@64786
    62
  "gcd a 0 = normalize a"
haftmann@64786
    63
  by (simp add: gcd.simps [of a 0])
haftmann@64786
    64
  
haftmann@64786
    65
qualified lemma gcd_mod:
haftmann@64786
    66
  "a \<noteq> 0 \<Longrightarrow> gcd a (b mod a) = gcd b a"
haftmann@64786
    67
  by (simp add: gcd.simps [of b 0] gcd.simps [of b a])
haftmann@58023
    68
haftmann@64786
    69
qualified definition lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
haftmann@64786
    70
  where "lcm a b = normalize (a * b) div gcd a b"
haftmann@64786
    71
haftmann@64786
    72
qualified definition Lcm :: "'a set \<Rightarrow> 'a" \<comment>
haftmann@64786
    73
    \<open>Somewhat complicated definition of Lcm that has the advantage of working
haftmann@64786
    74
    for infinite sets as well\<close>
haftmann@64786
    75
  where
haftmann@64786
    76
  [code del]: "Lcm A = (if \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) then
haftmann@60430
    77
     let l = SOME l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l =
haftmann@60430
    78
       (LEAST n. \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n)
haftmann@60634
    79
       in normalize l 
haftmann@58023
    80
      else 0)"
haftmann@58023
    81
haftmann@64786
    82
qualified definition Gcd :: "'a set \<Rightarrow> 'a"
haftmann@64786
    83
  where [code del]: "Gcd A = Lcm {d. \<forall>a\<in>A. d dvd a}"
eberlm@62428
    84
haftmann@64786
    85
end    
haftmann@60572
    86
haftmann@64786
    87
lemma semiring_gcd:
haftmann@64786
    88
  "class.semiring_gcd one zero times gcd lcm
haftmann@64848
    89
    divide plus minus unit_factor normalize"
haftmann@64786
    90
proof
haftmann@64786
    91
  show "gcd a b dvd a"
haftmann@64786
    92
    and "gcd a b dvd b" for a b
haftmann@64786
    93
    by (induct a b rule: eucl_induct)
haftmann@64786
    94
      (simp_all add: local.gcd_0 local.gcd_mod dvd_mod_iff)
eberlm@62422
    95
next
haftmann@64786
    96
  show "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> c dvd gcd a b" for a b c
haftmann@64786
    97
  proof (induct a b rule: eucl_induct)
haftmann@64786
    98
    case (zero a) from \<open>c dvd a\<close> show ?case
haftmann@64786
    99
      by (rule dvd_trans) (simp add: local.gcd_0)
eberlm@62422
   100
  next
haftmann@64786
   101
    case (mod a b)
haftmann@64786
   102
    then show ?case
haftmann@64786
   103
      by (simp add: local.gcd_mod dvd_mod_iff)
eberlm@62422
   104
  qed
eberlm@62422
   105
next
haftmann@64786
   106
  show "normalize (gcd a b) = gcd a b" for a b
haftmann@64786
   107
    by (induct a b rule: eucl_induct)
haftmann@64786
   108
      (simp_all add: local.gcd_0 local.gcd_mod)
haftmann@64786
   109
next
haftmann@64786
   110
  show "lcm a b = normalize (a * b) div gcd a b" for a b
haftmann@64786
   111
    by (fact local.lcm_def)
eberlm@63498
   112
qed
eberlm@63498
   113
haftmann@64786
   114
interpretation semiring_gcd one zero times gcd lcm
haftmann@64848
   115
  divide plus minus unit_factor normalize
haftmann@64786
   116
  by (fact semiring_gcd)
eberlm@63498
   117
  
haftmann@64786
   118
lemma semiring_Gcd:
haftmann@64786
   119
  "class.semiring_Gcd one zero times gcd lcm Gcd Lcm
haftmann@64848
   120
    divide plus minus unit_factor normalize"
haftmann@64786
   121
proof -
haftmann@64786
   122
  show ?thesis
haftmann@64786
   123
  proof
haftmann@64786
   124
    have "(\<forall>a\<in>A. a dvd Lcm A) \<and> (\<forall>b. (\<forall>a\<in>A. a dvd b) \<longrightarrow> Lcm A dvd b)" for A
haftmann@64786
   125
    proof (cases "\<exists>l. l \<noteq>  0 \<and> (\<forall>a\<in>A. a dvd l)")
eberlm@63498
   126
      case False
haftmann@64786
   127
      then have "Lcm A = 0"
haftmann@64786
   128
        by (auto simp add: local.Lcm_def)
haftmann@64786
   129
      with False show ?thesis
haftmann@64786
   130
        by auto
eberlm@63498
   131
    next
eberlm@63498
   132
      case True
haftmann@64786
   133
      then obtain l\<^sub>0 where l\<^sub>0_props: "l\<^sub>0 \<noteq> 0" "\<forall>a\<in>A. a dvd l\<^sub>0" by blast
haftmann@64786
   134
      define n where "n = (LEAST n. \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n)"
haftmann@64786
   135
      define l where "l = (SOME l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n)"
haftmann@64786
   136
      have "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n"
haftmann@64786
   137
        apply (subst n_def)
haftmann@64786
   138
        apply (rule LeastI [of _ "euclidean_size l\<^sub>0"])
haftmann@64786
   139
        apply (rule exI [of _ l\<^sub>0])
haftmann@64786
   140
        apply (simp add: l\<^sub>0_props)
haftmann@64786
   141
        done
haftmann@64786
   142
      from someI_ex [OF this] have "l \<noteq> 0" and "\<forall>a\<in>A. a dvd l"
haftmann@64786
   143
        and "euclidean_size l = n" 
haftmann@64786
   144
        unfolding l_def by simp_all
haftmann@64786
   145
      {
haftmann@64786
   146
        fix l' assume "\<forall>a\<in>A. a dvd l'"
haftmann@64786
   147
        with \<open>\<forall>a\<in>A. a dvd l\<close> have "\<forall>a\<in>A. a dvd gcd l l'"
haftmann@64786
   148
          by (auto intro: gcd_greatest)
haftmann@64786
   149
        moreover from \<open>l \<noteq> 0\<close> have "gcd l l' \<noteq> 0"
haftmann@64786
   150
          by simp
haftmann@64786
   151
        ultimately have "\<exists>b. b \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd b) \<and> 
haftmann@64786
   152
          euclidean_size b = euclidean_size (gcd l l')"
haftmann@64786
   153
          by (intro exI [of _ "gcd l l'"], auto)
haftmann@64786
   154
        then have "euclidean_size (gcd l l') \<ge> n"
haftmann@64786
   155
          by (subst n_def) (rule Least_le)
haftmann@64786
   156
        moreover have "euclidean_size (gcd l l') \<le> n"
haftmann@64786
   157
        proof -
haftmann@64786
   158
          have "gcd l l' dvd l"
haftmann@64786
   159
            by simp
haftmann@64786
   160
          then obtain a where "l = gcd l l' * a" ..
haftmann@64786
   161
          with \<open>l \<noteq> 0\<close> have "a \<noteq> 0"
haftmann@64786
   162
            by auto
haftmann@64786
   163
          hence "euclidean_size (gcd l l') \<le> euclidean_size (gcd l l' * a)"
haftmann@64786
   164
            by (rule size_mult_mono)
haftmann@64786
   165
          also have "gcd l l' * a = l" using \<open>l = gcd l l' * a\<close> ..
haftmann@64786
   166
          also note \<open>euclidean_size l = n\<close>
haftmann@64786
   167
          finally show "euclidean_size (gcd l l') \<le> n" .
haftmann@64786
   168
        qed
haftmann@64786
   169
        ultimately have *: "euclidean_size l = euclidean_size (gcd l l')" 
haftmann@64786
   170
          by (intro le_antisym, simp_all add: \<open>euclidean_size l = n\<close>)
haftmann@64786
   171
        from \<open>l \<noteq> 0\<close> have "l dvd gcd l l'"
haftmann@64786
   172
          by (rule dvd_euclidean_size_eq_imp_dvd) (auto simp add: *)
haftmann@64786
   173
        hence "l dvd l'" by (rule dvd_trans [OF _ gcd_dvd2])
haftmann@64786
   174
      }
haftmann@64786
   175
      with \<open>\<forall>a\<in>A. a dvd l\<close> and \<open>l \<noteq> 0\<close>
haftmann@64786
   176
        have "(\<forall>a\<in>A. a dvd normalize l) \<and> 
haftmann@64786
   177
          (\<forall>l'. (\<forall>a\<in>A. a dvd l') \<longrightarrow> normalize l dvd l')"
haftmann@64786
   178
        by auto
haftmann@64786
   179
      also from True have "normalize l = Lcm A"
haftmann@64786
   180
        by (simp add: local.Lcm_def Let_def n_def l_def)
eberlm@63498
   181
      finally show ?thesis .
eberlm@63498
   182
    qed
haftmann@64786
   183
    then show dvd_Lcm: "a \<in> A \<Longrightarrow> a dvd Lcm A"
haftmann@64786
   184
      and Lcm_least: "(\<And>a. a \<in> A \<Longrightarrow> a dvd b) \<Longrightarrow> Lcm A dvd b" for A and a b
haftmann@64786
   185
      by auto
haftmann@64786
   186
    show "a \<in> A \<Longrightarrow> Gcd A dvd a" for A and a
haftmann@64786
   187
      by (auto simp add: local.Gcd_def intro: Lcm_least)
haftmann@64786
   188
    show "(\<And>a. a \<in> A \<Longrightarrow> b dvd a) \<Longrightarrow> b dvd Gcd A" for A and b
haftmann@64786
   189
      by (auto simp add: local.Gcd_def intro: dvd_Lcm)
haftmann@64786
   190
    show [simp]: "normalize (Lcm A) = Lcm A" for A
haftmann@64786
   191
      by (simp add: local.Lcm_def)
haftmann@64786
   192
    show "normalize (Gcd A) = Gcd A" for A
haftmann@64786
   193
      by (simp add: local.Gcd_def)
eberlm@62442
   194
  qed
eberlm@62442
   195
qed
eberlm@62442
   196
haftmann@64786
   197
interpretation semiring_Gcd one zero times gcd lcm Gcd Lcm
haftmann@64848
   198
    divide plus minus unit_factor normalize
haftmann@64786
   199
  by (fact semiring_Gcd)
haftmann@60598
   200
haftmann@64786
   201
subclass factorial_semiring
haftmann@64786
   202
proof -
haftmann@64786
   203
  show "class.factorial_semiring divide plus minus zero times one
haftmann@64848
   204
     unit_factor normalize"
wenzelm@64911
   205
  proof (standard, rule factorial_semiring_altI_aux) \<comment> \<open>FIXME rule\<close>
haftmann@64786
   206
    fix x assume "x \<noteq> 0"
haftmann@64786
   207
    thus "finite {p. p dvd x \<and> normalize p = p}"
haftmann@64786
   208
    proof (induction "euclidean_size x" arbitrary: x rule: less_induct)
haftmann@64786
   209
      case (less x)
haftmann@64786
   210
      show ?case
haftmann@64786
   211
      proof (cases "\<exists>y. y dvd x \<and> \<not>x dvd y \<and> \<not>is_unit y")
haftmann@64786
   212
        case False
haftmann@64786
   213
        have "{p. p dvd x \<and> normalize p = p} \<subseteq> {1, normalize x}"
haftmann@64786
   214
        proof
haftmann@64786
   215
          fix p assume p: "p \<in> {p. p dvd x \<and> normalize p = p}"
haftmann@64786
   216
          with False have "is_unit p \<or> x dvd p" by blast
haftmann@64786
   217
          thus "p \<in> {1, normalize x}"
haftmann@64786
   218
          proof (elim disjE)
haftmann@64786
   219
            assume "is_unit p"
haftmann@64786
   220
            hence "normalize p = 1" by (simp add: is_unit_normalize)
haftmann@64786
   221
            with p show ?thesis by simp
haftmann@64786
   222
          next
haftmann@64786
   223
            assume "x dvd p"
haftmann@64786
   224
            with p have "normalize p = normalize x" by (intro associatedI) simp_all
haftmann@64786
   225
            with p show ?thesis by simp
haftmann@64786
   226
          qed
haftmann@64786
   227
        qed
haftmann@64786
   228
        moreover have "finite \<dots>" by simp
haftmann@64786
   229
        ultimately show ?thesis by (rule finite_subset)
haftmann@64786
   230
      next
haftmann@64786
   231
        case True
haftmann@64786
   232
        then obtain y where y: "y dvd x" "\<not>x dvd y" "\<not>is_unit y" by blast
haftmann@64786
   233
        define z where "z = x div y"
haftmann@64786
   234
        let ?fctrs = "\<lambda>x. {p. p dvd x \<and> normalize p = p}"
haftmann@64786
   235
        from y have x: "x = y * z" by (simp add: z_def)
haftmann@64786
   236
        with less.prems have "y \<noteq> 0" "z \<noteq> 0" by auto
haftmann@64786
   237
        have normalized_factors_product:
haftmann@64786
   238
          "{p. p dvd a * b \<and> normalize p = p} = 
haftmann@64786
   239
             (\<lambda>(x,y). x * y) ` ({p. p dvd a \<and> normalize p = p} \<times> {p. p dvd b \<and> normalize p = p})" for a b
haftmann@64786
   240
        proof safe
haftmann@64786
   241
          fix p assume p: "p dvd a * b" "normalize p = p"
haftmann@64786
   242
          from dvd_productE[OF p(1)] guess x y . note xy = this
haftmann@64786
   243
          define x' y' where "x' = normalize x" and "y' = normalize y"
haftmann@64786
   244
          have "p = x' * y'"
haftmann@64786
   245
            by (subst p(2) [symmetric]) (simp add: xy x'_def y'_def normalize_mult)
haftmann@64786
   246
          moreover from xy have "normalize x' = x'" "normalize y' = y'" "x' dvd a" "y' dvd b" 
haftmann@64786
   247
            by (simp_all add: x'_def y'_def)
haftmann@64786
   248
          ultimately show "p \<in> (\<lambda>(x, y). x * y) ` 
haftmann@64786
   249
            ({p. p dvd a \<and> normalize p = p} \<times> {p. p dvd b \<and> normalize p = p})"
haftmann@64786
   250
            by blast
haftmann@64786
   251
        qed (auto simp: normalize_mult mult_dvd_mono)
haftmann@64786
   252
        from x y have "\<not>is_unit z" by (auto simp: mult_unit_dvd_iff)
haftmann@64786
   253
        have "?fctrs x = (\<lambda>(p,p'). p * p') ` (?fctrs y \<times> ?fctrs z)"
haftmann@64786
   254
          by (subst x) (rule normalized_factors_product)
haftmann@64786
   255
        also have "\<not>y * z dvd y * 1" "\<not>y * z dvd 1 * z"
haftmann@64786
   256
          by (subst dvd_times_left_cancel_iff dvd_times_right_cancel_iff; fact)+
haftmann@64786
   257
        hence "finite ((\<lambda>(p,p'). p * p') ` (?fctrs y \<times> ?fctrs z))"
haftmann@64786
   258
          by (intro finite_imageI finite_cartesian_product less dvd_proper_imp_size_less)
haftmann@64786
   259
             (auto simp: x)
haftmann@64786
   260
        finally show ?thesis .
haftmann@64786
   261
      qed
haftmann@64786
   262
    qed
haftmann@64786
   263
  next
haftmann@64786
   264
    fix p
haftmann@64786
   265
    assume "irreducible p"
haftmann@64786
   266
    then show "prime_elem p"
haftmann@64786
   267
      by (rule irreducible_imp_prime_elem_gcd)
haftmann@64786
   268
  qed
haftmann@64786
   269
qed
haftmann@60598
   270
haftmann@64786
   271
lemma Gcd_eucl_set [code]:
haftmann@64850
   272
  "Gcd (set xs) = fold gcd xs 0"
haftmann@64850
   273
  by (fact Gcd_set_eq_fold)
haftmann@60598
   274
haftmann@64786
   275
lemma Lcm_eucl_set [code]:
haftmann@64850
   276
  "Lcm (set xs) = fold lcm xs 1"
haftmann@64850
   277
  by (fact Lcm_set_eq_fold)
haftmann@64786
   278
 
haftmann@60598
   279
end
haftmann@60598
   280
haftmann@64786
   281
hide_const (open) gcd lcm Gcd Lcm
haftmann@64786
   282
haftmann@64786
   283
lemma prime_elem_int_abs_iff [simp]:
haftmann@64786
   284
  fixes p :: int
haftmann@64786
   285
  shows "prime_elem \<bar>p\<bar> \<longleftrightarrow> prime_elem p"
haftmann@64786
   286
  using prime_elem_normalize_iff [of p] by simp
haftmann@64786
   287
  
haftmann@64786
   288
lemma prime_elem_int_minus_iff [simp]:
haftmann@64786
   289
  fixes p :: int
haftmann@64786
   290
  shows "prime_elem (- p) \<longleftrightarrow> prime_elem p"
haftmann@64786
   291
  using prime_elem_normalize_iff [of "- p"] by simp
haftmann@64786
   292
haftmann@64786
   293
lemma prime_int_iff:
haftmann@64786
   294
  fixes p :: int
haftmann@64786
   295
  shows "prime p \<longleftrightarrow> p > 0 \<and> prime_elem p"
haftmann@64786
   296
  by (auto simp add: prime_def dest: prime_elem_not_zeroI)
haftmann@64786
   297
  
haftmann@64786
   298
  
haftmann@64786
   299
subsection \<open>The (simple) euclidean algorithm as gcd computation\<close>
haftmann@64786
   300
  
haftmann@66817
   301
class euclidean_semiring_gcd = normalization_euclidean_semiring + gcd + Gcd +
haftmann@64786
   302
  assumes gcd_eucl: "Euclidean_Algorithm.gcd = GCD.gcd"
haftmann@64786
   303
    and lcm_eucl: "Euclidean_Algorithm.lcm = GCD.lcm"
haftmann@64786
   304
  assumes Gcd_eucl: "Euclidean_Algorithm.Gcd = GCD.Gcd"
haftmann@64786
   305
    and Lcm_eucl: "Euclidean_Algorithm.Lcm = GCD.Lcm"
haftmann@58023
   306
begin
haftmann@58023
   307
eberlm@62422
   308
subclass semiring_gcd
haftmann@64786
   309
  unfolding gcd_eucl [symmetric] lcm_eucl [symmetric]
haftmann@64786
   310
  by (fact semiring_gcd)
haftmann@58023
   311
eberlm@62422
   312
subclass semiring_Gcd
haftmann@64786
   313
  unfolding  gcd_eucl [symmetric] lcm_eucl [symmetric]
haftmann@64786
   314
    Gcd_eucl [symmetric] Lcm_eucl [symmetric]
haftmann@64786
   315
  by (fact semiring_Gcd)
eberlm@63498
   316
eberlm@63498
   317
subclass factorial_semiring_gcd
eberlm@63498
   318
proof
haftmann@64786
   319
  show "gcd a b = gcd_factorial a b" for a b
haftmann@64786
   320
    apply (rule sym)
haftmann@64786
   321
    apply (rule gcdI)
haftmann@64786
   322
       apply (fact gcd_lcm_factorial)+
haftmann@64786
   323
    done
haftmann@64786
   324
  then show "lcm a b = lcm_factorial a b" for a b
eberlm@63498
   325
    by (simp add: lcm_factorial_gcd_factorial lcm_gcd)
haftmann@64786
   326
  show "Gcd A = Gcd_factorial A" for A
haftmann@64786
   327
    apply (rule sym)
haftmann@64786
   328
    apply (rule GcdI)
haftmann@64786
   329
       apply (fact gcd_lcm_factorial)+
haftmann@64786
   330
    done
haftmann@64786
   331
  show "Lcm A = Lcm_factorial A" for A
haftmann@64786
   332
    apply (rule sym)
haftmann@64786
   333
    apply (rule LcmI)
haftmann@64786
   334
       apply (fact gcd_lcm_factorial)+
haftmann@64786
   335
    done
eberlm@63498
   336
qed
eberlm@63498
   337
haftmann@64786
   338
lemma gcd_mod_right [simp]:
haftmann@64786
   339
  "a \<noteq> 0 \<Longrightarrow> gcd a (b mod a) = gcd a b"
haftmann@64786
   340
  unfolding gcd.commute [of a b]
haftmann@64786
   341
  by (simp add: gcd_eucl [symmetric] local.gcd_mod)
haftmann@58023
   342
haftmann@64786
   343
lemma gcd_mod_left [simp]:
haftmann@64786
   344
  "b \<noteq> 0 \<Longrightarrow> gcd (a mod b) b = gcd a b"
haftmann@64786
   345
  by (drule gcd_mod_right [of _ a]) (simp add: gcd.commute)
haftmann@58023
   346
haftmann@58023
   347
lemma euclidean_size_gcd_le1 [simp]:
haftmann@58023
   348
  assumes "a \<noteq> 0"
haftmann@58023
   349
  shows "euclidean_size (gcd a b) \<le> euclidean_size a"
haftmann@58023
   350
proof -
haftmann@64786
   351
  from gcd_dvd1 obtain c where A: "a = gcd a b * c" ..
haftmann@64786
   352
  with assms have "c \<noteq> 0"
haftmann@64786
   353
    by auto
haftmann@64786
   354
  moreover from this
haftmann@64786
   355
  have "euclidean_size (gcd a b) \<le> euclidean_size (gcd a b * c)"
haftmann@64786
   356
    by (rule size_mult_mono)
haftmann@64786
   357
  with A show ?thesis
haftmann@64786
   358
    by simp
haftmann@58023
   359
qed
haftmann@58023
   360
haftmann@58023
   361
lemma euclidean_size_gcd_le2 [simp]:
haftmann@58023
   362
  "b \<noteq> 0 \<Longrightarrow> euclidean_size (gcd a b) \<le> euclidean_size b"
haftmann@58023
   363
  by (subst gcd.commute, rule euclidean_size_gcd_le1)
haftmann@58023
   364
haftmann@58023
   365
lemma euclidean_size_gcd_less1:
haftmann@64786
   366
  assumes "a \<noteq> 0" and "\<not> a dvd b"
haftmann@58023
   367
  shows "euclidean_size (gcd a b) < euclidean_size a"
haftmann@58023
   368
proof (rule ccontr)
haftmann@58023
   369
  assume "\<not>euclidean_size (gcd a b) < euclidean_size a"
eberlm@62422
   370
  with \<open>a \<noteq> 0\<close> have A: "euclidean_size (gcd a b) = euclidean_size a"
haftmann@58023
   371
    by (intro le_antisym, simp_all)
eberlm@62422
   372
  have "a dvd gcd a b"
eberlm@62422
   373
    by (rule dvd_euclidean_size_eq_imp_dvd) (simp_all add: assms A)
eberlm@62422
   374
  hence "a dvd b" using dvd_gcdD2 by blast
haftmann@64786
   375
  with \<open>\<not> a dvd b\<close> show False by contradiction
haftmann@58023
   376
qed
haftmann@58023
   377
haftmann@58023
   378
lemma euclidean_size_gcd_less2:
haftmann@64786
   379
  assumes "b \<noteq> 0" and "\<not> b dvd a"
haftmann@58023
   380
  shows "euclidean_size (gcd a b) < euclidean_size b"
haftmann@58023
   381
  using assms by (subst gcd.commute, rule euclidean_size_gcd_less1)
haftmann@58023
   382
haftmann@58023
   383
lemma euclidean_size_lcm_le1: 
haftmann@58023
   384
  assumes "a \<noteq> 0" and "b \<noteq> 0"
haftmann@58023
   385
  shows "euclidean_size a \<le> euclidean_size (lcm a b)"
haftmann@58023
   386
proof -
haftmann@60690
   387
  have "a dvd lcm a b" by (rule dvd_lcm1)
haftmann@60690
   388
  then obtain c where A: "lcm a b = a * c" ..
eberlm@62429
   389
  with \<open>a \<noteq> 0\<close> and \<open>b \<noteq> 0\<close> have "c \<noteq> 0" by (auto simp: lcm_eq_0_iff)
haftmann@58023
   390
  then show ?thesis by (subst A, intro size_mult_mono)
haftmann@58023
   391
qed
haftmann@58023
   392
haftmann@58023
   393
lemma euclidean_size_lcm_le2:
haftmann@58023
   394
  "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> euclidean_size b \<le> euclidean_size (lcm a b)"
haftmann@58023
   395
  using euclidean_size_lcm_le1 [of b a] by (simp add: ac_simps)
haftmann@58023
   396
haftmann@58023
   397
lemma euclidean_size_lcm_less1:
haftmann@64786
   398
  assumes "b \<noteq> 0" and "\<not> b dvd a"
haftmann@58023
   399
  shows "euclidean_size a < euclidean_size (lcm a b)"
haftmann@58023
   400
proof (rule ccontr)
haftmann@58023
   401
  from assms have "a \<noteq> 0" by auto
haftmann@58023
   402
  assume "\<not>euclidean_size a < euclidean_size (lcm a b)"
wenzelm@60526
   403
  with \<open>a \<noteq> 0\<close> and \<open>b \<noteq> 0\<close> have "euclidean_size (lcm a b) = euclidean_size a"
haftmann@58023
   404
    by (intro le_antisym, simp, intro euclidean_size_lcm_le1)
haftmann@58023
   405
  with assms have "lcm a b dvd a" 
eberlm@62429
   406
    by (rule_tac dvd_euclidean_size_eq_imp_dvd) (auto simp: lcm_eq_0_iff)
eberlm@62422
   407
  hence "b dvd a" by (rule lcm_dvdD2)
wenzelm@60526
   408
  with \<open>\<not>b dvd a\<close> show False by contradiction
haftmann@58023
   409
qed
haftmann@58023
   410
haftmann@58023
   411
lemma euclidean_size_lcm_less2:
haftmann@64786
   412
  assumes "a \<noteq> 0" and "\<not> a dvd b"
haftmann@58023
   413
  shows "euclidean_size b < euclidean_size (lcm a b)"
haftmann@58023
   414
  using assms euclidean_size_lcm_less1 [of a b] by (simp add: ac_simps)
haftmann@58023
   415
haftmann@58023
   416
end
haftmann@58023
   417
haftmann@64786
   418
lemma factorial_euclidean_semiring_gcdI:
haftmann@66817
   419
  "OFCLASS('a::{factorial_semiring_gcd, normalization_euclidean_semiring}, euclidean_semiring_gcd_class)"
haftmann@64786
   420
proof
haftmann@64786
   421
  interpret semiring_Gcd 1 0 times
haftmann@64786
   422
    Euclidean_Algorithm.gcd Euclidean_Algorithm.lcm
haftmann@64786
   423
    Euclidean_Algorithm.Gcd Euclidean_Algorithm.Lcm
haftmann@64848
   424
    divide plus minus unit_factor normalize
haftmann@64786
   425
    rewrites "dvd.dvd op * = Rings.dvd"
haftmann@64786
   426
    by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
haftmann@64786
   427
  show [simp]: "Euclidean_Algorithm.gcd = (gcd :: 'a \<Rightarrow> _)"
haftmann@64786
   428
  proof (rule ext)+
haftmann@64786
   429
    fix a b :: 'a
haftmann@64786
   430
    show "Euclidean_Algorithm.gcd a b = gcd a b"
haftmann@64786
   431
    proof (induct a b rule: eucl_induct)
haftmann@64786
   432
      case zero
haftmann@64786
   433
      then show ?case
haftmann@64786
   434
        by simp
haftmann@64786
   435
    next
haftmann@64786
   436
      case (mod a b)
haftmann@64786
   437
      moreover have "gcd b (a mod b) = gcd b a"
haftmann@64786
   438
        using GCD.gcd_add_mult [of b "a div b" "a mod b", symmetric]
haftmann@64786
   439
          by (simp add: div_mult_mod_eq)
haftmann@64786
   440
      ultimately show ?case
haftmann@64786
   441
        by (simp add: Euclidean_Algorithm.gcd_mod ac_simps)
haftmann@64786
   442
    qed
haftmann@64786
   443
  qed
haftmann@64786
   444
  show [simp]: "Euclidean_Algorithm.Lcm = (Lcm :: 'a set \<Rightarrow> _)"
haftmann@64786
   445
    by (auto intro!: Lcm_eqI GCD.dvd_Lcm GCD.Lcm_least)
haftmann@64786
   446
  show "Euclidean_Algorithm.lcm = (lcm :: 'a \<Rightarrow> _)"
haftmann@64786
   447
    by (simp add: fun_eq_iff Euclidean_Algorithm.lcm_def semiring_gcd_class.lcm_gcd)
haftmann@64786
   448
  show "Euclidean_Algorithm.Gcd = (Gcd :: 'a set \<Rightarrow> _)"
haftmann@64786
   449
    by (simp add: fun_eq_iff Euclidean_Algorithm.Gcd_def semiring_Gcd_class.Gcd_Lcm)
haftmann@64786
   450
qed
eberlm@63498
   451
haftmann@58023
   452
haftmann@64786
   453
subsection \<open>The extended euclidean algorithm\<close>
haftmann@64786
   454
  
haftmann@58023
   455
class euclidean_ring_gcd = euclidean_semiring_gcd + idom
haftmann@58023
   456
begin
haftmann@58023
   457
haftmann@58023
   458
subclass euclidean_ring ..
haftmann@60439
   459
subclass ring_gcd ..
eberlm@63498
   460
subclass factorial_ring_gcd ..
haftmann@60439
   461
haftmann@64786
   462
function euclid_ext_aux :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> ('a \<times> 'a) \<times> 'a"
haftmann@64786
   463
  where "euclid_ext_aux s' s t' t r' r = (
haftmann@64786
   464
     if r = 0 then let c = 1 div unit_factor r' in ((s' * c, t' * c), normalize r')
haftmann@64786
   465
     else let q = r' div r
haftmann@64786
   466
          in euclid_ext_aux s (s' - q * s) t (t' - q * t) r (r' mod r))"
haftmann@64786
   467
  by auto
haftmann@64786
   468
termination
haftmann@64786
   469
  by (relation "measure (\<lambda>(_, _, _, _, _, b). euclidean_size b)")
haftmann@64786
   470
    (simp_all add: mod_size_less)
eberlm@62442
   471
haftmann@64786
   472
abbreviation (input) euclid_ext :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<times> 'a) \<times> 'a"
haftmann@64786
   473
  where "euclid_ext \<equiv> euclid_ext_aux 1 0 0 1"
haftmann@64786
   474
    
haftmann@64786
   475
lemma
haftmann@64786
   476
  assumes "gcd r' r = gcd a b"
haftmann@64786
   477
  assumes "s' * a + t' * b = r'"
haftmann@64786
   478
  assumes "s * a + t * b = r"
haftmann@64786
   479
  assumes "euclid_ext_aux s' s t' t r' r = ((x, y), c)"
haftmann@64786
   480
  shows euclid_ext_aux_eq_gcd: "c = gcd a b"
haftmann@64786
   481
    and euclid_ext_aux_bezout: "x * a + y * b = gcd a b"
haftmann@64786
   482
proof -
haftmann@64786
   483
  have "case euclid_ext_aux s' s t' t r' r of ((x, y), c) \<Rightarrow> 
haftmann@64786
   484
    x * a + y * b = c \<and> c = gcd a b" (is "?P (euclid_ext_aux s' s t' t r' r)")
haftmann@64786
   485
    using assms(1-3)
haftmann@64786
   486
  proof (induction s' s t' t r' r rule: euclid_ext_aux.induct)
haftmann@64786
   487
    case (1 s' s t' t r' r)
haftmann@64786
   488
    show ?case
haftmann@64786
   489
    proof (cases "r = 0")
haftmann@64786
   490
      case True
haftmann@64786
   491
      hence "euclid_ext_aux s' s t' t r' r = 
haftmann@64786
   492
               ((s' div unit_factor r', t' div unit_factor r'), normalize r')"
haftmann@64786
   493
        by (subst euclid_ext_aux.simps) (simp add: Let_def)
haftmann@64786
   494
      also have "?P \<dots>"
haftmann@64786
   495
      proof safe
haftmann@64786
   496
        have "s' div unit_factor r' * a + t' div unit_factor r' * b = 
haftmann@64786
   497
                (s' * a + t' * b) div unit_factor r'"
haftmann@64786
   498
          by (cases "r' = 0") (simp_all add: unit_div_commute)
haftmann@64786
   499
        also have "s' * a + t' * b = r'" by fact
haftmann@64786
   500
        also have "\<dots> div unit_factor r' = normalize r'" by simp
haftmann@64786
   501
        finally show "s' div unit_factor r' * a + t' div unit_factor r' * b = normalize r'" .
haftmann@64786
   502
      next
haftmann@64786
   503
        from "1.prems" True show "normalize r' = gcd a b"
haftmann@64786
   504
          by simp
haftmann@64786
   505
      qed
haftmann@64786
   506
      finally show ?thesis .
haftmann@64786
   507
    next
haftmann@64786
   508
      case False
haftmann@64786
   509
      hence "euclid_ext_aux s' s t' t r' r = 
haftmann@64786
   510
             euclid_ext_aux s (s' - r' div r * s) t (t' - r' div r * t) r (r' mod r)"
haftmann@64786
   511
        by (subst euclid_ext_aux.simps) (simp add: Let_def)
haftmann@64786
   512
      also from "1.prems" False have "?P \<dots>"
haftmann@64786
   513
      proof (intro "1.IH")
haftmann@64786
   514
        have "(s' - r' div r * s) * a + (t' - r' div r * t) * b =
haftmann@64786
   515
              (s' * a + t' * b) - r' div r * (s * a + t * b)" by (simp add: algebra_simps)
haftmann@64786
   516
        also have "s' * a + t' * b = r'" by fact
haftmann@64786
   517
        also have "s * a + t * b = r" by fact
haftmann@64786
   518
        also have "r' - r' div r * r = r' mod r" using div_mult_mod_eq [of r' r]
haftmann@64786
   519
          by (simp add: algebra_simps)
haftmann@64786
   520
        finally show "(s' - r' div r * s) * a + (t' - r' div r * t) * b = r' mod r" .
haftmann@66817
   521
      qed (auto simp: algebra_simps minus_mod_eq_div_mult [symmetric] gcd.commute)
haftmann@64786
   522
      finally show ?thesis .
haftmann@64786
   523
    qed
haftmann@64786
   524
  qed
haftmann@64786
   525
  with assms(4) show "c = gcd a b" "x * a + y * b = gcd a b"
haftmann@64786
   526
    by simp_all
haftmann@64786
   527
qed
haftmann@60572
   528
haftmann@64786
   529
declare euclid_ext_aux.simps [simp del]
haftmann@64786
   530
haftmann@64786
   531
definition bezout_coefficients :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<times> 'a"
haftmann@64786
   532
  where [code]: "bezout_coefficients a b = fst (euclid_ext a b)"
haftmann@64786
   533
haftmann@64786
   534
lemma bezout_coefficients_0: 
haftmann@64786
   535
  "bezout_coefficients a 0 = (1 div unit_factor a, 0)"
haftmann@64786
   536
  by (simp add: bezout_coefficients_def euclid_ext_aux.simps)
haftmann@64786
   537
haftmann@64786
   538
lemma bezout_coefficients_left_0: 
haftmann@64786
   539
  "bezout_coefficients 0 a = (0, 1 div unit_factor a)"
haftmann@64786
   540
  by (simp add: bezout_coefficients_def euclid_ext_aux.simps)
haftmann@64786
   541
haftmann@64786
   542
lemma bezout_coefficients:
haftmann@64786
   543
  assumes "bezout_coefficients a b = (x, y)"
haftmann@64786
   544
  shows "x * a + y * b = gcd a b"
haftmann@64786
   545
  using assms by (simp add: bezout_coefficients_def
haftmann@64786
   546
    euclid_ext_aux_bezout [of a b a b 1 0 0 1 x y] prod_eq_iff)
haftmann@64786
   547
haftmann@64786
   548
lemma bezout_coefficients_fst_snd:
haftmann@64786
   549
  "fst (bezout_coefficients a b) * a + snd (bezout_coefficients a b) * b = gcd a b"
haftmann@64786
   550
  by (rule bezout_coefficients) simp
haftmann@64786
   551
haftmann@64786
   552
lemma euclid_ext_eq [simp]:
haftmann@64786
   553
  "euclid_ext a b = (bezout_coefficients a b, gcd a b)" (is "?p = ?q")
haftmann@64786
   554
proof
haftmann@64786
   555
  show "fst ?p = fst ?q"
haftmann@64786
   556
    by (simp add: bezout_coefficients_def)
haftmann@64786
   557
  have "snd (euclid_ext_aux 1 0 0 1 a b) = gcd a b"
haftmann@64786
   558
    by (rule euclid_ext_aux_eq_gcd [of a b a b 1 0 0 1])
haftmann@64786
   559
      (simp_all add: prod_eq_iff)
haftmann@64786
   560
  then show "snd ?p = snd ?q"
haftmann@64786
   561
    by simp
haftmann@64786
   562
qed
haftmann@64786
   563
haftmann@64786
   564
declare euclid_ext_eq [symmetric, code_unfold]
haftmann@60572
   565
haftmann@60572
   566
end
haftmann@58023
   567
haftmann@58023
   568
haftmann@60572
   569
subsection \<open>Typical instances\<close>
haftmann@58023
   570
haftmann@66817
   571
instance nat :: normalization_euclidean_semiring ..
haftmann@66817
   572
eberlm@62422
   573
instance nat :: euclidean_semiring_gcd
eberlm@62422
   574
proof
haftmann@64786
   575
  interpret semiring_Gcd 1 0 times
haftmann@64786
   576
    "Euclidean_Algorithm.gcd" "Euclidean_Algorithm.lcm"
haftmann@64786
   577
    "Euclidean_Algorithm.Gcd" "Euclidean_Algorithm.Lcm"
haftmann@64848
   578
    divide plus minus unit_factor normalize
haftmann@64786
   579
    rewrites "dvd.dvd op * = Rings.dvd"
haftmann@64786
   580
    by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
haftmann@64786
   581
  show [simp]: "(Euclidean_Algorithm.gcd :: nat \<Rightarrow> _) = gcd"
haftmann@64786
   582
  proof (rule ext)+
haftmann@64786
   583
    fix m n :: nat
haftmann@64786
   584
    show "Euclidean_Algorithm.gcd m n = gcd m n"
haftmann@64786
   585
    proof (induct m n rule: eucl_induct)
haftmann@64786
   586
      case zero
haftmann@64786
   587
      then show ?case
haftmann@64786
   588
        by simp
haftmann@64786
   589
    next
haftmann@64786
   590
      case (mod m n)
haftmann@64786
   591
      then have "gcd n (m mod n) = gcd n m"
haftmann@64786
   592
        using gcd_nat.simps [of m n] by (simp add: ac_simps)
haftmann@64786
   593
      with mod show ?case
haftmann@64786
   594
        by (simp add: Euclidean_Algorithm.gcd_mod ac_simps)
haftmann@64786
   595
    qed
haftmann@64786
   596
  qed
haftmann@64786
   597
  show [simp]: "(Euclidean_Algorithm.Lcm :: nat set \<Rightarrow> _) = Lcm"
haftmann@64786
   598
    by (auto intro!: ext Lcm_eqI)
haftmann@64786
   599
  show "(Euclidean_Algorithm.lcm :: nat \<Rightarrow> _) = lcm"
haftmann@64786
   600
    by (simp add: fun_eq_iff Euclidean_Algorithm.lcm_def semiring_gcd_class.lcm_gcd)
haftmann@64786
   601
  show "(Euclidean_Algorithm.Gcd :: nat set \<Rightarrow> _) = Gcd"
haftmann@64786
   602
    by (simp add: fun_eq_iff Euclidean_Algorithm.Gcd_def semiring_Gcd_class.Gcd_Lcm)
eberlm@62422
   603
qed
eberlm@62422
   604
eberlm@67167
   605
lemma prime_factorization_Suc_0 [simp]: "prime_factorization (Suc 0) = {#}"
eberlm@67167
   606
  unfolding One_nat_def [symmetric] using prime_factorization_1 .
eberlm@67167
   607
haftmann@66817
   608
instance int :: normalization_euclidean_semiring ..
haftmann@66817
   609
eberlm@62422
   610
instance int :: euclidean_ring_gcd
eberlm@62422
   611
proof
haftmann@64786
   612
  interpret semiring_Gcd 1 0 times
haftmann@64786
   613
    "Euclidean_Algorithm.gcd" "Euclidean_Algorithm.lcm"
haftmann@64786
   614
    "Euclidean_Algorithm.Gcd" "Euclidean_Algorithm.Lcm"
haftmann@64848
   615
    divide plus minus unit_factor normalize
haftmann@64786
   616
    rewrites "dvd.dvd op * = Rings.dvd"
haftmann@64786
   617
    by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
haftmann@64786
   618
  show [simp]: "(Euclidean_Algorithm.gcd :: int \<Rightarrow> _) = gcd"
haftmann@64786
   619
  proof (rule ext)+
haftmann@64786
   620
    fix k l :: int
haftmann@64786
   621
    show "Euclidean_Algorithm.gcd k l = gcd k l"
haftmann@64786
   622
    proof (induct k l rule: eucl_induct)
haftmann@64786
   623
      case zero
haftmann@64786
   624
      then show ?case
haftmann@64786
   625
        by simp
haftmann@64786
   626
    next
haftmann@64786
   627
      case (mod k l)
haftmann@64786
   628
      have "gcd l (k mod l) = gcd l k"
haftmann@64786
   629
      proof (cases l "0::int" rule: linorder_cases)
haftmann@64786
   630
        case less
haftmann@64786
   631
        then show ?thesis
haftmann@64786
   632
          using gcd_non_0_int [of "- l" "- k"] by (simp add: ac_simps)
haftmann@64786
   633
      next
haftmann@64786
   634
        case equal
haftmann@64786
   635
        with mod show ?thesis
haftmann@64786
   636
          by simp
haftmann@64786
   637
      next
haftmann@64786
   638
        case greater
haftmann@64786
   639
        then show ?thesis
haftmann@64786
   640
          using gcd_non_0_int [of l k] by (simp add: ac_simps)
haftmann@64786
   641
      qed
haftmann@64786
   642
      with mod show ?case
haftmann@64786
   643
        by (simp add: Euclidean_Algorithm.gcd_mod ac_simps)
haftmann@64786
   644
    qed
haftmann@64786
   645
  qed
haftmann@64786
   646
  show [simp]: "(Euclidean_Algorithm.Lcm :: int set \<Rightarrow> _) = Lcm"
haftmann@64786
   647
    by (auto intro!: ext Lcm_eqI)
haftmann@64786
   648
  show "(Euclidean_Algorithm.lcm :: int \<Rightarrow> _) = lcm"
haftmann@64786
   649
    by (simp add: fun_eq_iff Euclidean_Algorithm.lcm_def semiring_gcd_class.lcm_gcd)
haftmann@64786
   650
  show "(Euclidean_Algorithm.Gcd :: int set \<Rightarrow> _) = Gcd"
haftmann@64786
   651
    by (simp add: fun_eq_iff Euclidean_Algorithm.Gcd_def semiring_Gcd_class.Gcd_Lcm)
eberlm@62422
   652
qed
eberlm@62422
   653
haftmann@63924
   654
end