src/HOL/Proofs/Extraction/Euclid.thy
author wenzelm
Wed Dec 29 17:34:41 2010 +0100 (2010-12-29)
changeset 41413 64cd30d6b0b8
parent 39157 b98909faaea8
child 45170 7dd207fe7b6e
permissions -rw-r--r--
explicit file specifications -- avoid secondary load path;
wenzelm@39157
     1
(*  Title:      HOL/Proofs/Extraction/Euclid.thy
berghofe@25422
     2
    Author:     Markus Wenzel, TU Muenchen
wenzelm@32960
     3
    Author:     Freek Wiedijk, Radboud University Nijmegen
wenzelm@32960
     4
    Author:     Stefan Berghofer, TU Muenchen
berghofe@25422
     5
*)
berghofe@25422
     6
berghofe@25422
     7
header {* Euclid's theorem *}
berghofe@25422
     8
berghofe@25422
     9
theory Euclid
wenzelm@41413
    10
imports
wenzelm@41413
    11
  "~~/src/HOL/Number_Theory/UniqueFactorization"
wenzelm@41413
    12
  Util
wenzelm@41413
    13
  "~~/src/HOL/Library/Efficient_Nat"
berghofe@25422
    14
begin
berghofe@25422
    15
berghofe@25422
    16
text {*
berghofe@25422
    17
A constructive version of the proof of Euclid's theorem by
berghofe@25422
    18
Markus Wenzel and Freek Wiedijk \cite{Wenzel-Wiedijk-JAR2002}.
berghofe@25422
    19
*}
berghofe@25422
    20
haftmann@37288
    21
lemma factor_greater_one1: "n = m * k \<Longrightarrow> m < n \<Longrightarrow> k < n \<Longrightarrow> Suc 0 < m"
haftmann@37288
    22
  by (induct m) auto
haftmann@37288
    23
haftmann@37288
    24
lemma factor_greater_one2: "n = m * k \<Longrightarrow> m < n \<Longrightarrow> k < n \<Longrightarrow> Suc 0 < k"
haftmann@37288
    25
  by (induct k) auto
haftmann@37288
    26
haftmann@37288
    27
lemma prod_mn_less_k:
haftmann@37288
    28
  "(0::nat) < n ==> 0 < k ==> Suc 0 < m ==> m * n = k ==> n < k"
haftmann@37288
    29
  by (induct m) auto
haftmann@37288
    30
haftmann@37288
    31
lemma prime_eq: "prime (p::nat) = (1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> 1 < m \<longrightarrow> m = p))"
haftmann@37288
    32
  apply (simp add: prime_nat_def)
berghofe@25422
    33
  apply (rule iffI)
berghofe@25422
    34
  apply blast
berghofe@25422
    35
  apply (erule conjE)
berghofe@25422
    36
  apply (rule conjI)
berghofe@25422
    37
  apply assumption
berghofe@25422
    38
  apply (rule allI impI)+
berghofe@25422
    39
  apply (erule allE)
berghofe@25422
    40
  apply (erule impE)
berghofe@25422
    41
  apply assumption
berghofe@25422
    42
  apply (case_tac "m=0")
berghofe@25422
    43
  apply simp
berghofe@25422
    44
  apply (case_tac "m=Suc 0")
berghofe@25422
    45
  apply simp
berghofe@25422
    46
  apply simp
berghofe@25422
    47
  done
berghofe@25422
    48
haftmann@37288
    49
lemma prime_eq': "prime (p::nat) = (1 < p \<and> (\<forall>m k. p = m * k \<longrightarrow> 1 < m \<longrightarrow> m = p))"
haftmann@37598
    50
  by (simp add: prime_eq dvd_def HOL.all_simps [symmetric] del: HOL.all_simps)
berghofe@25422
    51
berghofe@25422
    52
lemma not_prime_ex_mk:
berghofe@25422
    53
  assumes n: "Suc 0 < n"
berghofe@25422
    54
  shows "(\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k) \<or> prime n"
berghofe@25422
    55
proof -
berghofe@25422
    56
  {
berghofe@25422
    57
    fix k
berghofe@25422
    58
    from nat_eq_dec
berghofe@25422
    59
    have "(\<exists>m<n. n = m * k) \<or> \<not> (\<exists>m<n. n = m * k)"
berghofe@25422
    60
      by (rule search)
berghofe@25422
    61
  }
berghofe@25422
    62
  hence "(\<exists>k<n. \<exists>m<n. n = m * k) \<or> \<not> (\<exists>k<n. \<exists>m<n. n = m * k)"
berghofe@25422
    63
    by (rule search)
berghofe@25422
    64
  thus ?thesis
berghofe@25422
    65
  proof
berghofe@25422
    66
    assume "\<exists>k<n. \<exists>m<n. n = m * k"
berghofe@25422
    67
    then obtain k m where k: "k<n" and m: "m<n" and nmk: "n = m * k"
berghofe@25422
    68
      by iprover
berghofe@25422
    69
    from nmk m k have "Suc 0 < m" by (rule factor_greater_one1)
berghofe@25422
    70
    moreover from nmk m k have "Suc 0 < k" by (rule factor_greater_one2)
berghofe@25422
    71
    ultimately show ?thesis using k m nmk by iprover
berghofe@25422
    72
  next
berghofe@25422
    73
    assume "\<not> (\<exists>k<n. \<exists>m<n. n = m * k)"
berghofe@25422
    74
    hence A: "\<forall>k<n. \<forall>m<n. n \<noteq> m * k" by iprover
berghofe@25422
    75
    have "\<forall>m k. n = m * k \<longrightarrow> Suc 0 < m \<longrightarrow> m = n"
berghofe@25422
    76
    proof (intro allI impI)
berghofe@25422
    77
      fix m k
berghofe@25422
    78
      assume nmk: "n = m * k"
berghofe@25422
    79
      assume m: "Suc 0 < m"
berghofe@25422
    80
      from n m nmk have k: "0 < k"
wenzelm@32960
    81
        by (cases k) auto
berghofe@25422
    82
      moreover from n have n: "0 < n" by simp
berghofe@25422
    83
      moreover note m
berghofe@25422
    84
      moreover from nmk have "m * k = n" by simp
berghofe@25422
    85
      ultimately have kn: "k < n" by (rule prod_mn_less_k)
berghofe@25422
    86
      show "m = n"
berghofe@25422
    87
      proof (cases "k = Suc 0")
wenzelm@32960
    88
        case True
wenzelm@32960
    89
        with nmk show ?thesis by (simp only: mult_Suc_right)
berghofe@25422
    90
      next
wenzelm@32960
    91
        case False
wenzelm@32960
    92
        from m have "0 < m" by simp
wenzelm@32960
    93
        moreover note n
wenzelm@32960
    94
        moreover from False n nmk k have "Suc 0 < k" by auto
wenzelm@32960
    95
        moreover from nmk have "k * m = n" by (simp only: mult_ac)
wenzelm@32960
    96
        ultimately have mn: "m < n" by (rule prod_mn_less_k)
wenzelm@32960
    97
        with kn A nmk show ?thesis by iprover
berghofe@25422
    98
      qed
berghofe@25422
    99
    qed
berghofe@25422
   100
    with n have "prime n"
berghofe@25422
   101
      by (simp only: prime_eq' One_nat_def simp_thms)
berghofe@25422
   102
    thus ?thesis ..
berghofe@25422
   103
  qed
berghofe@25422
   104
qed
berghofe@25422
   105
haftmann@37288
   106
lemma dvd_factorial: "0 < m \<Longrightarrow> m \<le> n \<Longrightarrow> m dvd fact (n::nat)"
haftmann@37288
   107
proof (induct n rule: nat_induct)
haftmann@37288
   108
  case 0
haftmann@37288
   109
  then show ?case by simp
haftmann@37288
   110
next
haftmann@37288
   111
  case (Suc n)
haftmann@37288
   112
  from `m \<le> Suc n` show ?case
haftmann@37288
   113
  proof (rule le_SucE)
haftmann@37288
   114
    assume "m \<le> n"
haftmann@37288
   115
    with `0 < m` have "m dvd fact n" by (rule Suc)
haftmann@37288
   116
    then have "m dvd (fact n * Suc n)" by (rule dvd_mult2)
haftmann@37288
   117
    then show ?thesis by (simp add: mult_commute)
haftmann@37288
   118
  next
haftmann@37288
   119
    assume "m = Suc n"
haftmann@37288
   120
    then have "m dvd (fact n * Suc n)"
haftmann@37288
   121
      by (auto intro: dvdI simp: mult_ac)
haftmann@37288
   122
    then show ?thesis by (simp add: mult_commute)
haftmann@37288
   123
  qed
haftmann@37288
   124
qed
haftmann@37288
   125
haftmann@37288
   126
lemma dvd_prod [iff]: "n dvd (PROD m\<Colon>nat:#multiset_of (n # ns). m)"
haftmann@37288
   127
  by (simp add: msetprod_Un msetprod_singleton)
haftmann@37288
   128
haftmann@37335
   129
definition all_prime :: "nat list \<Rightarrow> bool" where
haftmann@37335
   130
  "all_prime ps \<longleftrightarrow> (\<forall>p\<in>set ps. prime p)"
haftmann@37335
   131
haftmann@37335
   132
lemma all_prime_simps:
haftmann@37335
   133
  "all_prime []"
haftmann@37335
   134
  "all_prime (p # ps) \<longleftrightarrow> prime p \<and> all_prime ps"
haftmann@37335
   135
  by (simp_all add: all_prime_def)
haftmann@37288
   136
haftmann@37335
   137
lemma all_prime_append:
haftmann@37335
   138
  "all_prime (ps @ qs) \<longleftrightarrow> all_prime ps \<and> all_prime qs"
haftmann@37335
   139
  by (simp add: all_prime_def ball_Un)
haftmann@37288
   140
haftmann@37335
   141
lemma split_all_prime:
haftmann@37335
   142
  assumes "all_prime ms" and "all_prime ns"
haftmann@37335
   143
  shows "\<exists>qs. all_prime qs \<and> (PROD m\<Colon>nat:#multiset_of qs. m) =
haftmann@37288
   144
    (PROD m\<Colon>nat:#multiset_of ms. m) * (PROD m\<Colon>nat:#multiset_of ns. m)" (is "\<exists>qs. ?P qs \<and> ?Q qs")
haftmann@37288
   145
proof -
haftmann@37335
   146
  from assms have "all_prime (ms @ ns)"
haftmann@37335
   147
    by (simp add: all_prime_append)
haftmann@37288
   148
  moreover from assms have "(PROD m\<Colon>nat:#multiset_of (ms @ ns). m) =
haftmann@37288
   149
    (PROD m\<Colon>nat:#multiset_of ms. m) * (PROD m\<Colon>nat:#multiset_of ns. m)"
haftmann@37288
   150
    by (simp add: msetprod_Un)
haftmann@37288
   151
  ultimately have "?P (ms @ ns) \<and> ?Q (ms @ ns)" ..
haftmann@37288
   152
  then show ?thesis ..
haftmann@37288
   153
qed
haftmann@37288
   154
haftmann@37335
   155
lemma all_prime_nempty_g_one:
haftmann@37335
   156
  assumes "all_prime ps" and "ps \<noteq> []"
haftmann@37288
   157
  shows "Suc 0 < (PROD m\<Colon>nat:#multiset_of ps. m)"
haftmann@37335
   158
  using `ps \<noteq> []` `all_prime ps` unfolding One_nat_def [symmetric] by (induct ps rule: list_nonempty_induct)
haftmann@37336
   159
    (simp_all add: all_prime_simps msetprod_singleton msetprod_Un prime_gt_1_nat less_1_mult del: One_nat_def)
haftmann@37288
   160
haftmann@37335
   161
lemma factor_exists: "Suc 0 < n \<Longrightarrow> (\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#multiset_of ps. m) = n)"
berghofe@25422
   162
proof (induct n rule: nat_wf_ind)
berghofe@25422
   163
  case (1 n)
berghofe@25422
   164
  from `Suc 0 < n`
berghofe@25422
   165
  have "(\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k) \<or> prime n"
berghofe@25422
   166
    by (rule not_prime_ex_mk)
berghofe@25422
   167
  then show ?case
berghofe@25422
   168
  proof 
berghofe@25422
   169
    assume "\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k"
berghofe@25422
   170
    then obtain m k where m: "Suc 0 < m" and k: "Suc 0 < k" and mn: "m < n"
berghofe@25422
   171
      and kn: "k < n" and nmk: "n = m * k" by iprover
haftmann@37335
   172
    from mn and m have "\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#multiset_of ps. m) = m" by (rule 1)
haftmann@37335
   173
    then obtain ps1 where "all_prime ps1" and prod_ps1_m: "(PROD m\<Colon>nat:#multiset_of ps1. m) = m"
berghofe@25422
   174
      by iprover
haftmann@37335
   175
    from kn and k have "\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#multiset_of ps. m) = k" by (rule 1)
haftmann@37335
   176
    then obtain ps2 where "all_prime ps2" and prod_ps2_k: "(PROD m\<Colon>nat:#multiset_of ps2. m) = k"
berghofe@25422
   177
      by iprover
haftmann@37335
   178
    from `all_prime ps1` `all_prime ps2`
haftmann@37335
   179
    have "\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#multiset_of ps. m) =
haftmann@37335
   180
      (PROD m\<Colon>nat:#multiset_of ps1. m) * (PROD m\<Colon>nat:#multiset_of ps2. m)"
haftmann@37335
   181
      by (rule split_all_prime)
haftmann@37335
   182
    with prod_ps1_m prod_ps2_k nmk show ?thesis by simp
berghofe@25422
   183
  next
haftmann@37335
   184
    assume "prime n" then have "all_prime [n]" by (simp add: all_prime_simps)
haftmann@37288
   185
    moreover have "(PROD m\<Colon>nat:#multiset_of [n]. m) = n" by (simp add: msetprod_singleton)
haftmann@37335
   186
    ultimately have "all_prime [n] \<and> (PROD m\<Colon>nat:#multiset_of [n]. m) = n" ..
haftmann@37288
   187
    then show ?thesis ..
berghofe@25422
   188
  qed
berghofe@25422
   189
qed
berghofe@25422
   190
berghofe@25422
   191
lemma prime_factor_exists:
berghofe@25422
   192
  assumes N: "(1::nat) < n"
berghofe@25422
   193
  shows "\<exists>p. prime p \<and> p dvd n"
berghofe@25422
   194
proof -
haftmann@37335
   195
  from N obtain ps where "all_prime ps"
haftmann@37335
   196
    and prod_ps: "n = (PROD m\<Colon>nat:#multiset_of ps. m)" using factor_exists
berghofe@25422
   197
    by simp iprover
haftmann@37335
   198
  with N have "ps \<noteq> []"
haftmann@37335
   199
    by (auto simp add: all_prime_nempty_g_one msetprod_empty)
haftmann@37335
   200
  then obtain p qs where ps: "ps = p # qs" by (cases ps) simp
haftmann@37335
   201
  with `all_prime ps` have "prime p" by (simp add: all_prime_simps)
haftmann@37335
   202
  moreover from `all_prime ps` ps prod_ps
haftmann@37335
   203
  have "p dvd n" by (simp only: dvd_prod)
berghofe@25422
   204
  ultimately show ?thesis by iprover
berghofe@25422
   205
qed
berghofe@25422
   206
berghofe@25422
   207
text {*
berghofe@25422
   208
Euclid's theorem: there are infinitely many primes.
berghofe@25422
   209
*}
berghofe@25422
   210
haftmann@37288
   211
lemma Euclid: "\<exists>p::nat. prime p \<and> n < p"
berghofe@25422
   212
proof -
haftmann@37288
   213
  let ?k = "fact n + 1"
haftmann@37288
   214
  have "1 < fact n + 1" by simp
berghofe@25422
   215
  then obtain p where prime: "prime p" and dvd: "p dvd ?k" using prime_factor_exists by iprover
berghofe@25422
   216
  have "n < p"
berghofe@25422
   217
  proof -
berghofe@25422
   218
    have "\<not> p \<le> n"
berghofe@25422
   219
    proof
berghofe@25422
   220
      assume pn: "p \<le> n"
haftmann@37288
   221
      from `prime p` have "0 < p" by (rule prime_gt_0_nat)
haftmann@37288
   222
      then have "p dvd fact n" using pn by (rule dvd_factorial)
haftmann@37288
   223
      with dvd have "p dvd ?k - fact n" by (rule dvd_diff_nat)
berghofe@25422
   224
      then have "p dvd 1" by simp
haftmann@37288
   225
      with prime show False by auto
berghofe@25422
   226
    qed
berghofe@25422
   227
    then show ?thesis by simp
berghofe@25422
   228
  qed
berghofe@25422
   229
  with prime show ?thesis by iprover
berghofe@25422
   230
qed
berghofe@25422
   231
berghofe@25422
   232
extract Euclid
berghofe@25422
   233
berghofe@25422
   234
text {*
berghofe@25422
   235
The program extracted from the proof of Euclid's theorem looks as follows.
berghofe@25422
   236
@{thm [display] Euclid_def}
berghofe@25422
   237
The program corresponding to the proof of the factorization theorem is
berghofe@25422
   238
@{thm [display] factor_exists_def}
berghofe@25422
   239
*}
berghofe@25422
   240
haftmann@27982
   241
instantiation nat :: default
haftmann@27982
   242
begin
haftmann@27982
   243
haftmann@27982
   244
definition "default = (0::nat)"
haftmann@27982
   245
haftmann@27982
   246
instance ..
haftmann@27982
   247
haftmann@27982
   248
end
berghofe@25422
   249
haftmann@27982
   250
instantiation list :: (type) default
haftmann@27982
   251
begin
haftmann@27982
   252
haftmann@27982
   253
definition "default = []"
haftmann@27982
   254
haftmann@27982
   255
instance ..
haftmann@27982
   256
haftmann@27982
   257
end
haftmann@27982
   258
haftmann@37288
   259
primrec iterate :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list" where
haftmann@37288
   260
  "iterate 0 f x = []"
haftmann@37288
   261
  | "iterate (Suc n) f x = (let y = f x in y # iterate n f y)"
haftmann@37288
   262
haftmann@37288
   263
lemma "factor_exists 1007 = [53, 19]" by eval
haftmann@37288
   264
lemma "factor_exists 567 = [7, 3, 3, 3, 3]" by eval
haftmann@37288
   265
lemma "factor_exists 345 = [23, 5, 3]" by eval
haftmann@37288
   266
lemma "factor_exists 999 = [37, 3, 3, 3]" by eval
haftmann@37288
   267
lemma "factor_exists 876 = [73, 3, 2, 2]" by eval
haftmann@37288
   268
haftmann@37288
   269
lemma "iterate 4 Euclid 0 = [2, 3, 7, 71]" by eval
haftmann@37288
   270
haftmann@27982
   271
consts_code
haftmann@27982
   272
  default ("(error \"default\")")
berghofe@25422
   273
haftmann@27982
   274
lemma "factor_exists 1007 = [53, 19]" by evaluation
haftmann@27982
   275
lemma "factor_exists 567 = [7, 3, 3, 3, 3]" by evaluation
haftmann@27982
   276
lemma "factor_exists 345 = [23, 5, 3]" by evaluation
haftmann@27982
   277
lemma "factor_exists 999 = [37, 3, 3, 3]" by evaluation
haftmann@27982
   278
lemma "factor_exists 876 = [73, 3, 2, 2]" by evaluation
haftmann@37291
   279
haftmann@27982
   280
lemma "iterate 4 Euclid 0 = [2, 3, 7, 71]" by evaluation
haftmann@27982
   281
berghofe@25422
   282
end