summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | berghofe |

Tue, 13 Nov 2007 10:58:46 +0100 | |

changeset 25422 | 37e991068d96 |

parent 25421 | 1c5b8d54a339 |

child 25423 | 2c6167e2c587 |

New case studies for program extraction.

src/HOL/Extraction/Euclid.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Extraction/Greatest_Common_Divisor.thy | file | annotate | diff | comparison | revisions |

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Extraction/Euclid.thy Tue Nov 13 10:58:46 2007 +0100 @@ -0,0 +1,240 @@ +(* Title: HOL/Extraction/Euclid.thy + ID: $Id$ + Author: Markus Wenzel, TU Muenchen + Freek Wiedijk, Radboud University Nijmegen + Stefan Berghofer, TU Muenchen +*) + +header {* Euclid's theorem *} + +theory Euclid +imports "~~/src/HOL/NumberTheory/Factorization" Efficient_Nat Util +begin + +text {* +A constructive version of the proof of Euclid's theorem by +Markus Wenzel and Freek Wiedijk \cite{Wenzel-Wiedijk-JAR2002}. +*} + +lemma prime_eq: "prime p = (1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> 1 < m \<longrightarrow> m = p))" + apply (simp add: prime_def) + apply (rule iffI) + apply blast + apply (erule conjE) + apply (rule conjI) + apply assumption + apply (rule allI impI)+ + apply (erule allE) + apply (erule impE) + apply assumption + apply (case_tac "m=0") + apply simp + apply (case_tac "m=Suc 0") + apply simp + apply simp + done + +lemma prime_eq': "prime p = (1 < p \<and> (\<forall>m k. p = m * k \<longrightarrow> 1 < m \<longrightarrow> m = p))" + by (simp add: prime_eq dvd_def all_simps [symmetric] del: all_simps) + +lemma factor_greater_one1: "n = m * k \<Longrightarrow> m < n \<Longrightarrow> k < n \<Longrightarrow> Suc 0 < m" + by (induct m) auto + +lemma factor_greater_one2: "n = m * k \<Longrightarrow> m < n \<Longrightarrow> k < n \<Longrightarrow> Suc 0 < k" + by (induct k) auto + +lemma not_prime_ex_mk: + assumes n: "Suc 0 < n" + shows "(\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k) \<or> prime n" +proof - + { + fix k + from nat_eq_dec + have "(\<exists>m<n. n = m * k) \<or> \<not> (\<exists>m<n. n = m * k)" + by (rule search) + } + hence "(\<exists>k<n. \<exists>m<n. n = m * k) \<or> \<not> (\<exists>k<n. \<exists>m<n. n = m * k)" + by (rule search) + thus ?thesis + proof + assume "\<exists>k<n. \<exists>m<n. n = m * k" + then obtain k m where k: "k<n" and m: "m<n" and nmk: "n = m * k" + by iprover + from nmk m k have "Suc 0 < m" by (rule factor_greater_one1) + moreover from nmk m k have "Suc 0 < k" by (rule factor_greater_one2) + ultimately show ?thesis using k m nmk by iprover + next + assume "\<not> (\<exists>k<n. \<exists>m<n. n = m * k)" + hence A: "\<forall>k<n. \<forall>m<n. n \<noteq> m * k" by iprover + have "\<forall>m k. n = m * k \<longrightarrow> Suc 0 < m \<longrightarrow> m = n" + proof (intro allI impI) + fix m k + assume nmk: "n = m * k" + assume m: "Suc 0 < m" + from n m nmk have k: "0 < k" + by (cases k) auto + moreover from n have n: "0 < n" by simp + moreover note m + moreover from nmk have "m * k = n" by simp + ultimately have kn: "k < n" by (rule prod_mn_less_k) + show "m = n" + proof (cases "k = Suc 0") + case True + with nmk show ?thesis by (simp only: mult_Suc_right) + next + case False + from m have "0 < m" by simp + moreover note n + moreover from False n nmk k have "Suc 0 < k" by auto + moreover from nmk have "k * m = n" by (simp only: mult_ac) + ultimately have mn: "m < n" by (rule prod_mn_less_k) + with kn A nmk show ?thesis by iprover + qed + qed + with n have "prime n" + by (simp only: prime_eq' One_nat_def simp_thms) + thus ?thesis .. + qed +qed + +text {* +Unfortunately, the proof in the @{text Factorization} theory using @{text metis} +is non-constructive. +*} + +lemma split_primel': + "primel xs \<Longrightarrow> primel ys \<Longrightarrow> \<exists>l. primel l \<and> prod l = prod xs * prod ys" + apply (rule exI) + apply safe + apply (rule_tac [2] prod_append) + apply (simp add: primel_append) + done + +lemma factor_exists: "Suc 0 < n \<Longrightarrow> (\<exists>l. primel l \<and> prod l = n)" +proof (induct n rule: nat_wf_ind) + case (1 n) + from `Suc 0 < n` + have "(\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k) \<or> prime n" + by (rule not_prime_ex_mk) + then show ?case + proof + assume "\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k" + then obtain m k where m: "Suc 0 < m" and k: "Suc 0 < k" and mn: "m < n" + and kn: "k < n" and nmk: "n = m * k" by iprover + from mn and m have "\<exists>l. primel l \<and> prod l = m" by (rule 1) + then obtain l1 where primel_l1: "primel l1" and prod_l1_m: "prod l1 = m" + by iprover + from kn and k have "\<exists>l. primel l \<and> prod l = k" by (rule 1) + then obtain l2 where primel_l2: "primel l2" and prod_l2_k: "prod l2 = k" + by iprover + from primel_l1 primel_l2 + have "\<exists>l. primel l \<and> prod l = prod l1 * prod l2" + by (rule split_primel') + with prod_l1_m prod_l2_k nmk show ?thesis by simp + next + assume "prime n" + hence "primel [n] \<and> prod [n] = n" by (rule prime_primel) + thus ?thesis .. + qed +qed + +lemma dvd_prod [iff]: "n dvd prod (n # ns)" + by simp + +consts fact :: "nat \<Rightarrow> nat" ("(_!)" [1000] 999) +primrec + "0! = 1" + "(Suc n)! = n! * Suc n" + +lemma fact_greater_0 [iff]: "0 < n!" + by (induct n) simp_all + +lemma dvd_factorial: "0 < m \<Longrightarrow> m \<le> n \<Longrightarrow> m dvd n!" +proof (induct n) + case 0 + then show ?case by simp +next + case (Suc n) + from `m \<le> Suc n` show ?case + proof (rule le_SucE) + assume "m \<le> n" + with `0 < m` have "m dvd n!" by (rule Suc) + then have "m dvd (n! * Suc n)" by (rule dvd_mult2) + then show ?thesis by simp + next + assume "m = Suc n" + then have "m dvd (n! * Suc n)" + by (auto intro: dvdI simp: mult_ac) + then show ?thesis by simp + qed +qed + +lemma prime_factor_exists: + assumes N: "(1::nat) < n" + shows "\<exists>p. prime p \<and> p dvd n" +proof - + from N obtain l where primel_l: "primel l" + and prod_l: "n = prod l" using factor_exists + by simp iprover + from prems have "l \<noteq> []" + by (auto simp add: primel_nempty_g_one) + then obtain x xs where l: "l = x # xs" + by (cases l) simp + from primel_l l have "prime x" by (simp add: primel_hd_tl) + moreover from primel_l l prod_l + have "x dvd n" by (simp only: dvd_prod) + ultimately show ?thesis by iprover +qed + +text {* +Euclid's theorem: there are infinitely many primes. +*} + +lemma Euclid: "\<exists>p. prime p \<and> n < p" +proof - + let ?k = "n! + 1" + have "1 < n! + 1" by simp + then obtain p where prime: "prime p" and dvd: "p dvd ?k" using prime_factor_exists by iprover + have "n < p" + proof - + have "\<not> p \<le> n" + proof + assume pn: "p \<le> n" + from `prime p` have "0 < p" by (rule prime_g_zero) + then have "p dvd n!" using pn by (rule dvd_factorial) + with dvd have "p dvd ?k - n!" by (rule dvd_diff) + then have "p dvd 1" by simp + with prime show False using prime_nd_one by auto + qed + then show ?thesis by simp + qed + with prime show ?thesis by iprover +qed + +extract Euclid + +text {* +The program extracted from the proof of Euclid's theorem looks as follows. +@{thm [display] Euclid_def} +The program corresponding to the proof of the factorization theorem is +@{thm [display] factor_exists_def} +*} + +consts_code + arbitrary ("(error \"arbitrary\")") + +code_module Prime +contains Euclid + +ML "Prime.factor_exists 1007" +ML "Prime.factor_exists 567" +ML "Prime.factor_exists 345" +ML "Prime.factor_exists 999" +ML "Prime.factor_exists 876" + +ML "Prime.Euclid 0" +ML "Prime.Euclid it" +ML "Prime.Euclid it" +ML "Prime.Euclid it" + +end

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Extraction/Greatest_Common_Divisor.thy Tue Nov 13 10:58:46 2007 +0100 @@ -0,0 +1,73 @@ +(* Title: HOL/Extraction/Greatest_Common_Divisor.thy + ID: $Id$ + Author: Stefan Berghofer, TU Muenchen + Helmut Schwichtenberg, LMU Muenchen +*) + +header {* Greatest common divisor *} + +theory Greatest_Common_Divisor +imports QuotRem +begin + +theorem greatest_common_divisor: + "\<And>n::nat. Suc m < n \<Longrightarrow> \<exists>k n1 m1. k * n1 = n \<and> k * m1 = Suc m \<and> + (\<forall>l l1 l2. l * l1 = n \<longrightarrow> l * l2 = Suc m \<longrightarrow> l \<le> k)" +proof (induct m rule: nat_wf_ind) + case (1 m n) + from division obtain r q where h1: "n = Suc m * q + r" and h2: "r \<le> m" + by iprover + show ?case + proof (cases r) + case 0 + with h1 have "Suc m * q = n" by simp + moreover have "Suc m * 1 = Suc m" by simp + moreover { + fix l2 have "\<And>l l1. l * l1 = n \<Longrightarrow> l * l2 = Suc m \<Longrightarrow> l \<le> Suc m" + by (cases l2) simp_all } + ultimately show ?thesis by iprover + next + case (Suc nat) + with h2 have h: "nat < m" by simp + moreover from h have "Suc nat < Suc m" by simp + ultimately have "\<exists>k m1 r1. k * m1 = Suc m \<and> k * r1 = Suc nat \<and> + (\<forall>l l1 l2. l * l1 = Suc m \<longrightarrow> l * l2 = Suc nat \<longrightarrow> l \<le> k)" + by (rule 1) + then obtain k m1 r1 where + h1': "k * m1 = Suc m" + and h2': "k * r1 = Suc nat" + and h3': "\<And>l l1 l2. l * l1 = Suc m \<Longrightarrow> l * l2 = Suc nat \<Longrightarrow> l \<le> k" + by iprover + have mn: "Suc m < n" by (rule 1) + from h1 h1' h2' Suc have "k * (m1 * q + r1) = n" + by (simp add: add_mult_distrib2 nat_mult_assoc [symmetric]) + moreover have "\<And>l l1 l2. l * l1 = n \<Longrightarrow> l * l2 = Suc m \<Longrightarrow> l \<le> k" + proof - + fix l l1 l2 + assume ll1n: "l * l1 = n" + assume ll2m: "l * l2 = Suc m" + moreover have "l * (l1 - l2 * q) = Suc nat" + by (simp add: diff_mult_distrib2 h1 Suc [symmetric] mn ll1n ll2m [symmetric]) + ultimately show "l \<le> k" by (rule h3') + qed + ultimately show ?thesis using h1' by iprover + qed +qed + +extract greatest_common_divisor + +text {* +The extracted program for computing the greatest common divisor is +@{thm [display] greatest_common_divisor_def} +*} + +consts_code + arbitrary ("(error \"arbitrary\")") + +code_module GCD +contains + test = "greatest_common_divisor 7 12" + +ML GCD.test + +end