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