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