src/HOL/Extraction/Euclid.thy
author wenzelm
Tue, 07 Jul 2009 20:16:06 +0200
changeset 31953 eeb8a300f362
parent 30047 46c88406e6c0
child 32479 521cc9bf2958
permissions -rw-r--r--
fixed proof (cf. 40501bb2d57c);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
25422
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
     1
(*  Title:      HOL/Extraction/Euclid.thy
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
     2
    ID:         $Id$
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
     4
                Freek Wiedijk, Radboud University Nijmegen
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
     5
                Stefan Berghofer, TU Muenchen
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
     6
*)
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
     7
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
     8
header {* Euclid's theorem *}
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
     9
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    10
theory Euclid
27982
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
    11
imports "~~/src/HOL/NumberTheory/Factorization" Util Efficient_Nat
25422
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    12
begin
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    13
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    14
text {*
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    15
A constructive version of the proof of Euclid's theorem by
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    16
Markus Wenzel and Freek Wiedijk \cite{Wenzel-Wiedijk-JAR2002}.
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    17
*}
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    18
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    19
lemma prime_eq: "prime p = (1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> 1 < m \<longrightarrow> m = p))"
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    20
  apply (simp add: prime_def)
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    21
  apply (rule iffI)
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    22
  apply blast
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    23
  apply (erule conjE)
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    24
  apply (rule conjI)
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    25
  apply assumption
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    26
  apply (rule allI impI)+
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    27
  apply (erule allE)
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    28
  apply (erule impE)
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    29
  apply assumption
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    30
  apply (case_tac "m=0")
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    31
  apply simp
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    32
  apply (case_tac "m=Suc 0")
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    33
  apply simp
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    34
  apply simp
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    35
  done
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    36
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    37
lemma prime_eq': "prime p = (1 < p \<and> (\<forall>m k. p = m * k \<longrightarrow> 1 < m \<longrightarrow> m = p))"
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    38
  by (simp add: prime_eq dvd_def all_simps [symmetric] del: all_simps)
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    39
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    40
lemma factor_greater_one1: "n = m * k \<Longrightarrow> m < n \<Longrightarrow> k < n \<Longrightarrow> Suc 0 < m"
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    41
  by (induct m) auto
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    42
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    43
lemma factor_greater_one2: "n = m * k \<Longrightarrow> m < n \<Longrightarrow> k < n \<Longrightarrow> Suc 0 < k"
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    44
  by (induct k) auto
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    45
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    46
lemma not_prime_ex_mk:
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    47
  assumes n: "Suc 0 < n"
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    48
  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
    49
proof -
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    50
  {
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    51
    fix k
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    52
    from nat_eq_dec
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    53
    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
    54
      by (rule search)
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    55
  }
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    56
  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
    57
    by (rule search)
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    58
  thus ?thesis
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    59
  proof
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    60
    assume "\<exists>k<n. \<exists>m<n. n = m * k"
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    61
    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
    62
      by iprover
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    63
    from nmk m k have "Suc 0 < m" by (rule factor_greater_one1)
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    64
    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
    65
    ultimately show ?thesis using k m nmk by iprover
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    66
  next
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    67
    assume "\<not> (\<exists>k<n. \<exists>m<n. n = m * k)"
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    68
    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
    69
    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
    70
    proof (intro allI impI)
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    71
      fix m k
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    72
      assume nmk: "n = m * k"
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    73
      assume m: "Suc 0 < m"
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    74
      from n m nmk have k: "0 < k"
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    75
	by (cases k) auto
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    76
      moreover from n have n: "0 < n" by simp
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    77
      moreover note m
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    78
      moreover from nmk have "m * k = n" by simp
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    79
      ultimately have kn: "k < n" by (rule prod_mn_less_k)
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    80
      show "m = n"
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    81
      proof (cases "k = Suc 0")
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    82
	case True
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    83
	with nmk show ?thesis by (simp only: mult_Suc_right)
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    84
      next
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    85
	case False
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    86
	from m have "0 < m" by simp
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    87
	moreover note n
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    88
	moreover from False n nmk k have "Suc 0 < k" by auto
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    89
	moreover from nmk have "k * m = n" by (simp only: mult_ac)
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    90
	ultimately have mn: "m < n" by (rule prod_mn_less_k)
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    91
	with kn A nmk show ?thesis by iprover
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    92
      qed
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    93
    qed
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    94
    with n have "prime n"
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    95
      by (simp only: prime_eq' One_nat_def simp_thms)
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    96
    thus ?thesis ..
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
    97
  qed
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
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   100
lemma factor_exists: "Suc 0 < n \<Longrightarrow> (\<exists>l. primel l \<and> prod l = n)"
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   101
proof (induct n rule: nat_wf_ind)
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   102
  case (1 n)
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   103
  from `Suc 0 < n`
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   104
  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
   105
    by (rule not_prime_ex_mk)
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   106
  then show ?case
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   107
  proof 
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   108
    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
   109
    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
   110
      and kn: "k < n" and nmk: "n = m * k" by iprover
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   111
    from mn and m have "\<exists>l. primel l \<and> prod l = m" by (rule 1)
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   112
    then obtain l1 where primel_l1: "primel l1" and prod_l1_m: "prod l1 = m"
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   113
      by iprover
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   114
    from kn and k have "\<exists>l. primel l \<and> prod l = k" by (rule 1)
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   115
    then obtain l2 where primel_l2: "primel l2" and prod_l2_k: "prod l2 = k"
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   116
      by iprover
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   117
    from primel_l1 primel_l2
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   118
    have "\<exists>l. primel l \<and> prod l = prod l1 * prod l2"
25687
f92c9dfa7681 split_primel: salvaged original proof after blow with sledghammer
wenzelm
parents: 25422
diff changeset
   119
      by (rule split_primel)
25422
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   120
    with prod_l1_m prod_l2_k nmk show ?thesis by simp
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   121
  next
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   122
    assume "prime n"
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   123
    hence "primel [n] \<and> prod [n] = n" by (rule prime_primel)
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   124
    thus ?thesis ..
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   125
  qed
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   126
qed
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   127
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   128
lemma dvd_prod [iff]: "n dvd prod (n # ns)"
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   129
  by simp
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   130
25976
11c6811f232c modernized primrec;
wenzelm
parents: 25687
diff changeset
   131
primrec fact :: "nat \<Rightarrow> nat"    ("(_!)" [1000] 999)
11c6811f232c modernized primrec;
wenzelm
parents: 25687
diff changeset
   132
where
11c6811f232c modernized primrec;
wenzelm
parents: 25687
diff changeset
   133
    "0! = 1"
11c6811f232c modernized primrec;
wenzelm
parents: 25687
diff changeset
   134
  | "(Suc n)! = n! * Suc n"
25422
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   135
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   136
lemma fact_greater_0 [iff]: "0 < n!"
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   137
  by (induct n) simp_all
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   138
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   139
lemma dvd_factorial: "0 < m \<Longrightarrow> m \<le> n \<Longrightarrow> m dvd n!"
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   140
proof (induct n)
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   141
  case 0
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   142
  then show ?case by simp
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   143
next
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   144
  case (Suc n)
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   145
  from `m \<le> Suc n` show ?case
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   146
  proof (rule le_SucE)
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   147
    assume "m \<le> n"
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   148
    with `0 < m` have "m dvd n!" by (rule Suc)
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   149
    then have "m dvd (n! * Suc n)" by (rule dvd_mult2)
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   150
    then show ?thesis by simp
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   151
  next
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   152
    assume "m = Suc n"
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   153
    then have "m dvd (n! * Suc n)"
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   154
      by (auto intro: dvdI simp: mult_ac)
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   155
    then show ?thesis by simp
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   156
  qed
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   157
qed
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   158
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   159
lemma prime_factor_exists:
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   160
  assumes N: "(1::nat) < n"
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   161
  shows "\<exists>p. prime p \<and> p dvd n"
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   162
proof -
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   163
  from N obtain l where primel_l: "primel l"
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   164
    and prod_l: "n = prod l" using factor_exists
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   165
    by simp iprover
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   166
  from prems have "l \<noteq> []"
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   167
    by (auto simp add: primel_nempty_g_one)
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   168
  then obtain x xs where l: "l = x # xs"
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   169
    by (cases l) simp
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   170
  from primel_l l have "prime x" by (simp add: primel_hd_tl)
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   171
  moreover from primel_l l prod_l
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   172
  have "x dvd n" by (simp only: dvd_prod)
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   173
  ultimately show ?thesis by iprover
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   174
qed
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   175
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   176
text {*
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   177
Euclid's theorem: there are infinitely many primes.
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   178
*}
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   179
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   180
lemma Euclid: "\<exists>p. prime p \<and> n < p"
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   181
proof -
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   182
  let ?k = "n! + 1"
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   183
  have "1 < n! + 1" by simp
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   184
  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
   185
  have "n < p"
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   186
  proof -
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   187
    have "\<not> p \<le> n"
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   188
    proof
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   189
      assume pn: "p \<le> n"
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   190
      from `prime p` have "0 < p" by (rule prime_g_zero)
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   191
      then have "p dvd n!" using pn by (rule dvd_factorial)
31953
eeb8a300f362 fixed proof (cf. 40501bb2d57c);
wenzelm
parents: 30047
diff changeset
   192
      with dvd have "p dvd ?k - n!" by (rule dvd_diff_nat)
25422
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   193
      then have "p dvd 1" by simp
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   194
      with prime show False using prime_nd_one by auto
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   195
    qed
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   196
    then show ?thesis by simp
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   197
  qed
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   198
  with prime show ?thesis by iprover
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   199
qed
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   200
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   201
extract Euclid
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   202
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   203
text {*
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   204
The program extracted from the proof of Euclid's theorem looks as follows.
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   205
@{thm [display] Euclid_def}
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   206
The program corresponding to the proof of the factorization theorem is
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   207
@{thm [display] factor_exists_def}
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   208
*}
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   209
27982
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   210
instantiation nat :: default
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   211
begin
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   212
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   213
definition "default = (0::nat)"
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   214
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   215
instance ..
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   216
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   217
end
25422
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   218
27982
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   219
instantiation list :: (type) default
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   220
begin
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   221
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   222
definition "default = []"
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   223
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   224
instance ..
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   225
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   226
end
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   227
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   228
consts_code
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   229
  default ("(error \"default\")")
25422
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   230
27982
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   231
lemma "factor_exists 1007 = [53, 19]" by evaluation
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   232
lemma "factor_exists 1007 = [53, 19]" by eval
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   233
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   234
lemma "factor_exists 567 = [7, 3, 3, 3, 3]" by evaluation
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   235
lemma "factor_exists 567 = [7, 3, 3, 3, 3]" by eval
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   236
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   237
lemma "factor_exists 345 = [23, 5, 3]" by evaluation
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   238
lemma "factor_exists 345 = [23, 5, 3]" by eval
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   239
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   240
lemma "factor_exists 999 = [37, 3, 3, 3]" by evaluation
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   241
lemma "factor_exists 999 = [37, 3, 3, 3]" by eval
25422
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   242
27982
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   243
lemma "factor_exists 876 = [73, 3, 2, 2]" by evaluation
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   244
lemma "factor_exists 876 = [73, 3, 2, 2]" by eval
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   245
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   246
primrec iterate :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list" where
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   247
  "iterate 0 f x = []"
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   248
  | "iterate (Suc n) f x = (let y = f x in y # iterate n f y)"
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   249
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   250
lemma "iterate 4 Euclid 0 = [2, 3, 7, 71]" by evaluation
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   251
lemma "iterate 4 Euclid 0 = [2, 3, 7, 71]" by eval
2aaa4a5569a6 default replaces arbitrary
haftmann
parents: 25976
diff changeset
   252
25422
37e991068d96 New case studies for program extraction.
berghofe
parents:
diff changeset
   253
end