1.1 --- a/src/HOL/Extraction/Euclid.thy Wed Jun 02 16:42:58 2010 +0200
1.2 +++ b/src/HOL/Extraction/Euclid.thy Wed Jun 02 18:48:30 2010 +0200
1.3 @@ -7,7 +7,7 @@
1.4 header {* Euclid's theorem *}
1.5
1.6 theory Euclid
1.7 -imports "~~/src/HOL/Old_Number_Theory/Factorization" Util Efficient_Nat
1.8 +imports "~~/src/HOL/Number_Theory/UniqueFactorization" Util Efficient_Nat
1.9 begin
1.10
1.11 text {*
1.12 @@ -15,8 +15,18 @@
1.13 Markus Wenzel and Freek Wiedijk \cite{Wenzel-Wiedijk-JAR2002}.
1.14 *}
1.15
1.16 -lemma prime_eq: "prime p = (1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> 1 < m \<longrightarrow> m = p))"
1.17 - apply (simp add: prime_def)
1.18 +lemma factor_greater_one1: "n = m * k \<Longrightarrow> m < n \<Longrightarrow> k < n \<Longrightarrow> Suc 0 < m"
1.19 + by (induct m) auto
1.20 +
1.21 +lemma factor_greater_one2: "n = m * k \<Longrightarrow> m < n \<Longrightarrow> k < n \<Longrightarrow> Suc 0 < k"
1.22 + by (induct k) auto
1.23 +
1.24 +lemma prod_mn_less_k:
1.25 + "(0::nat) < n ==> 0 < k ==> Suc 0 < m ==> m * n = k ==> n < k"
1.26 + by (induct m) auto
1.27 +
1.28 +lemma prime_eq: "prime (p::nat) = (1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> 1 < m \<longrightarrow> m = p))"
1.29 + apply (simp add: prime_nat_def)
1.30 apply (rule iffI)
1.31 apply blast
1.32 apply (erule conjE)
1.33 @@ -33,15 +43,9 @@
1.34 apply simp
1.35 done
1.36
1.37 -lemma prime_eq': "prime p = (1 < p \<and> (\<forall>m k. p = m * k \<longrightarrow> 1 < m \<longrightarrow> m = p))"
1.38 +lemma prime_eq': "prime (p::nat) = (1 < p \<and> (\<forall>m k. p = m * k \<longrightarrow> 1 < m \<longrightarrow> m = p))"
1.39 by (simp add: prime_eq dvd_def all_simps [symmetric] del: all_simps)
1.40
1.41 -lemma factor_greater_one1: "n = m * k \<Longrightarrow> m < n \<Longrightarrow> k < n \<Longrightarrow> Suc 0 < m"
1.42 - by (induct m) auto
1.43 -
1.44 -lemma factor_greater_one2: "n = m * k \<Longrightarrow> m < n \<Longrightarrow> k < n \<Longrightarrow> Suc 0 < k"
1.45 - by (induct k) auto
1.46 -
1.47 lemma not_prime_ex_mk:
1.48 assumes n: "Suc 0 < n"
1.49 shows "(\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k) \<or> prime n"
1.50 @@ -96,7 +100,55 @@
1.51 qed
1.52 qed
1.53
1.54 -lemma factor_exists: "Suc 0 < n \<Longrightarrow> (\<exists>l. primel l \<and> prod l = n)"
1.55 +lemma dvd_factorial: "0 < m \<Longrightarrow> m \<le> n \<Longrightarrow> m dvd fact (n::nat)"
1.56 +proof (induct n rule: nat_induct)
1.57 + case 0
1.58 + then show ?case by simp
1.59 +next
1.60 + case (Suc n)
1.61 + from `m \<le> Suc n` show ?case
1.62 + proof (rule le_SucE)
1.63 + assume "m \<le> n"
1.64 + with `0 < m` have "m dvd fact n" by (rule Suc)
1.65 + then have "m dvd (fact n * Suc n)" by (rule dvd_mult2)
1.66 + then show ?thesis by (simp add: mult_commute)
1.67 + next
1.68 + assume "m = Suc n"
1.69 + then have "m dvd (fact n * Suc n)"
1.70 + by (auto intro: dvdI simp: mult_ac)
1.71 + then show ?thesis by (simp add: mult_commute)
1.72 + qed
1.73 +qed
1.74 +
1.75 +lemma dvd_prod [iff]: "n dvd (PROD m\<Colon>nat:#multiset_of (n # ns). m)"
1.76 + by (simp add: msetprod_Un msetprod_singleton)
1.77 +
1.78 +abbreviation (input) "primel ps \<equiv> (\<forall>(p::nat)\<in>set ps. prime p)"
1.79 +
1.80 +lemma prime_primel: "prime n \<Longrightarrow> primel [n]"
1.81 + by simp
1.82 +
1.83 +lemma split_primel:
1.84 + assumes "primel ms" and "primel ns"
1.85 + shows "\<exists>qs. primel qs \<and> (PROD m\<Colon>nat:#multiset_of qs. m) =
1.86 + (PROD m\<Colon>nat:#multiset_of ms. m) * (PROD m\<Colon>nat:#multiset_of ns. m)" (is "\<exists>qs. ?P qs \<and> ?Q qs")
1.87 +proof -
1.88 + from assms have "primel (ms @ ns)"
1.89 + unfolding set_append ball_Un by iprover
1.90 + moreover from assms have "(PROD m\<Colon>nat:#multiset_of (ms @ ns). m) =
1.91 + (PROD m\<Colon>nat:#multiset_of ms. m) * (PROD m\<Colon>nat:#multiset_of ns. m)"
1.92 + by (simp add: msetprod_Un)
1.93 + ultimately have "?P (ms @ ns) \<and> ?Q (ms @ ns)" ..
1.94 + then show ?thesis ..
1.95 +qed
1.96 +
1.97 +lemma primel_nempty_g_one:
1.98 + assumes "primel ps" and "ps \<noteq> []"
1.99 + shows "Suc 0 < (PROD m\<Colon>nat:#multiset_of ps. m)"
1.100 + using `ps \<noteq> []` `primel ps` unfolding One_nat_def [symmetric] by (induct ps rule: list_nonempty_induct)
1.101 + (simp_all add: msetprod_singleton msetprod_Un prime_gt_1_nat less_1_mult del: One_nat_def)
1.102 +
1.103 +lemma factor_exists: "Suc 0 < n \<Longrightarrow> (\<exists>l. primel l \<and> (PROD m\<Colon>nat:#multiset_of l. m) = n)"
1.104 proof (induct n rule: nat_wf_ind)
1.105 case (1 n)
1.106 from `Suc 0 < n`
1.107 @@ -107,51 +159,22 @@
1.108 assume "\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k"
1.109 then obtain m k where m: "Suc 0 < m" and k: "Suc 0 < k" and mn: "m < n"
1.110 and kn: "k < n" and nmk: "n = m * k" by iprover
1.111 - from mn and m have "\<exists>l. primel l \<and> prod l = m" by (rule 1)
1.112 - then obtain l1 where primel_l1: "primel l1" and prod_l1_m: "prod l1 = m"
1.113 + from mn and m have "\<exists>l. primel l \<and> (PROD m\<Colon>nat:#multiset_of l. m) = m" by (rule 1)
1.114 + then obtain l1 where primel_l1: "primel l1" and prod_l1_m: "(PROD m\<Colon>nat:#multiset_of l1. m) = m"
1.115 by iprover
1.116 - from kn and k have "\<exists>l. primel l \<and> prod l = k" by (rule 1)
1.117 - then obtain l2 where primel_l2: "primel l2" and prod_l2_k: "prod l2 = k"
1.118 + from kn and k have "\<exists>l. primel l \<and> (PROD m\<Colon>nat:#multiset_of l. m) = k" by (rule 1)
1.119 + then obtain l2 where primel_l2: "primel l2" and prod_l2_k: "(PROD m\<Colon>nat:#multiset_of l2. m) = k"
1.120 by iprover
1.121 from primel_l1 primel_l2
1.122 - have "\<exists>l. primel l \<and> prod l = prod l1 * prod l2"
1.123 + have "\<exists>l. primel l \<and> (PROD m\<Colon>nat:#multiset_of l. m) =
1.124 + (PROD m\<Colon>nat:#multiset_of l1. m) * (PROD m\<Colon>nat:#multiset_of l2. m)"
1.125 by (rule split_primel)
1.126 with prod_l1_m prod_l2_k nmk show ?thesis by simp
1.127 next
1.128 - assume "prime n"
1.129 - hence "primel [n] \<and> prod [n] = n" by (rule prime_primel)
1.130 - thus ?thesis ..
1.131 - qed
1.132 -qed
1.133 -
1.134 -lemma dvd_prod [iff]: "n dvd prod (n # ns)"
1.135 - by simp
1.136 -
1.137 -primrec fact :: "nat \<Rightarrow> nat" ("(_!)" [1000] 999)
1.138 -where
1.139 - "0! = 1"
1.140 - | "(Suc n)! = n! * Suc n"
1.141 -
1.142 -lemma fact_greater_0 [iff]: "0 < n!"
1.143 - by (induct n) simp_all
1.144 -
1.145 -lemma dvd_factorial: "0 < m \<Longrightarrow> m \<le> n \<Longrightarrow> m dvd n!"
1.146 -proof (induct n)
1.147 - case 0
1.148 - then show ?case by simp
1.149 -next
1.150 - case (Suc n)
1.151 - from `m \<le> Suc n` show ?case
1.152 - proof (rule le_SucE)
1.153 - assume "m \<le> n"
1.154 - with `0 < m` have "m dvd n!" by (rule Suc)
1.155 - then have "m dvd (n! * Suc n)" by (rule dvd_mult2)
1.156 - then show ?thesis by simp
1.157 - next
1.158 - assume "m = Suc n"
1.159 - then have "m dvd (n! * Suc n)"
1.160 - by (auto intro: dvdI simp: mult_ac)
1.161 - then show ?thesis by simp
1.162 + assume "prime n" then have "primel [n]" by (rule prime_primel)
1.163 + moreover have "(PROD m\<Colon>nat:#multiset_of [n]. m) = n" by (simp add: msetprod_singleton)
1.164 + ultimately have "primel [n] \<and> (PROD m\<Colon>nat:#multiset_of [n]. m) = n" ..
1.165 + then show ?thesis ..
1.166 qed
1.167 qed
1.168
1.169 @@ -160,13 +183,14 @@
1.170 shows "\<exists>p. prime p \<and> p dvd n"
1.171 proof -
1.172 from N obtain l where primel_l: "primel l"
1.173 - and prod_l: "n = prod l" using factor_exists
1.174 + and prod_l: "n = (PROD m\<Colon>nat:#multiset_of l. m)" using factor_exists
1.175 by simp iprover
1.176 - from prems have "l \<noteq> []"
1.177 - by (auto simp add: primel_nempty_g_one)
1.178 + with N have "l \<noteq> []"
1.179 + by (auto simp add: primel_nempty_g_one msetprod_empty)
1.180 then obtain x xs where l: "l = x # xs"
1.181 by (cases l) simp
1.182 - from primel_l l have "prime x" by (simp add: primel_hd_tl)
1.183 + then have "x \<in> set l" by (simp only: insert_def set.simps) (iprover intro: UnI1 CollectI)
1.184 + with primel_l have "prime x" ..
1.185 moreover from primel_l l prod_l
1.186 have "x dvd n" by (simp only: dvd_prod)
1.187 ultimately show ?thesis by iprover
1.188 @@ -176,21 +200,21 @@
1.189 Euclid's theorem: there are infinitely many primes.
1.190 *}
1.191
1.192 -lemma Euclid: "\<exists>p. prime p \<and> n < p"
1.193 +lemma Euclid: "\<exists>p::nat. prime p \<and> n < p"
1.194 proof -
1.195 - let ?k = "n! + 1"
1.196 - have "1 < n! + 1" by simp
1.197 + let ?k = "fact n + 1"
1.198 + have "1 < fact n + 1" by simp
1.199 then obtain p where prime: "prime p" and dvd: "p dvd ?k" using prime_factor_exists by iprover
1.200 have "n < p"
1.201 proof -
1.202 have "\<not> p \<le> n"
1.203 proof
1.204 assume pn: "p \<le> n"
1.205 - from `prime p` have "0 < p" by (rule prime_g_zero)
1.206 - then have "p dvd n!" using pn by (rule dvd_factorial)
1.207 - with dvd have "p dvd ?k - n!" by (rule dvd_diff_nat)
1.208 + from `prime p` have "0 < p" by (rule prime_gt_0_nat)
1.209 + then have "p dvd fact n" using pn by (rule dvd_factorial)
1.210 + with dvd have "p dvd ?k - fact n" by (rule dvd_diff_nat)
1.211 then have "p dvd 1" by simp
1.212 - with prime show False using prime_nd_one by auto
1.213 + with prime show False by auto
1.214 qed
1.215 then show ?thesis by simp
1.216 qed
1.217 @@ -224,29 +248,27 @@
1.218
1.219 end
1.220
1.221 +primrec iterate :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list" where
1.222 + "iterate 0 f x = []"
1.223 + | "iterate (Suc n) f x = (let y = f x in y # iterate n f y)"
1.224 +
1.225 +lemma "factor_exists 1007 = [53, 19]" by eval
1.226 +lemma "factor_exists 567 = [7, 3, 3, 3, 3]" by eval
1.227 +lemma "factor_exists 345 = [23, 5, 3]" by eval
1.228 +lemma "factor_exists 999 = [37, 3, 3, 3]" by eval
1.229 +lemma "factor_exists 876 = [73, 3, 2, 2]" by eval
1.230 +
1.231 +lemma "iterate 4 Euclid 0 = [2, 3, 7, 71]" by eval
1.232 +
1.233 consts_code
1.234 default ("(error \"default\")")
1.235
1.236 lemma "factor_exists 1007 = [53, 19]" by evaluation
1.237 -lemma "factor_exists 1007 = [53, 19]" by eval
1.238 -
1.239 lemma "factor_exists 567 = [7, 3, 3, 3, 3]" by evaluation
1.240 -lemma "factor_exists 567 = [7, 3, 3, 3, 3]" by eval
1.241 -
1.242 lemma "factor_exists 345 = [23, 5, 3]" by evaluation
1.243 -lemma "factor_exists 345 = [23, 5, 3]" by eval
1.244 -
1.245 lemma "factor_exists 999 = [37, 3, 3, 3]" by evaluation
1.246 -lemma "factor_exists 999 = [37, 3, 3, 3]" by eval
1.247 -
1.248 lemma "factor_exists 876 = [73, 3, 2, 2]" by evaluation
1.249 -lemma "factor_exists 876 = [73, 3, 2, 2]" by eval
1.250 -
1.251 -primrec iterate :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list" where
1.252 - "iterate 0 f x = []"
1.253 - | "iterate (Suc n) f x = (let y = f x in y # iterate n f y)"
1.254
1.255 lemma "iterate 4 Euclid 0 = [2, 3, 7, 71]" by evaluation
1.256 -lemma "iterate 4 Euclid 0 = [2, 3, 7, 71]" by eval
1.257
1.258 end
2.1 --- a/src/HOL/Extraction/Pigeonhole.thy Wed Jun 02 16:42:58 2010 +0200
2.2 +++ b/src/HOL/Extraction/Pigeonhole.thy Wed Jun 02 18:48:30 2010 +0200
2.3 @@ -236,10 +236,6 @@
2.4
2.5 end
2.6
2.7 -consts_code
2.8 - "default :: nat" ("{* 0::nat *}")
2.9 - "default :: nat \<times> nat" ("{* (0::nat, 0::nat) *}")
2.10 -
2.11 definition
2.12 "test n u = pigeonhole n (\<lambda>m. m - 1)"
2.13 definition
2.14 @@ -247,6 +243,19 @@
2.15 definition
2.16 "test'' u = pigeonhole 8 (op ! [0, 1, 2, 3, 4, 5, 6, 3, 7, 8])"
2.17
2.18 +ML "timeit (@{code test} 10)"
2.19 +ML "timeit (@{code test'} 10)"
2.20 +ML "timeit (@{code test} 20)"
2.21 +ML "timeit (@{code test'} 20)"
2.22 +ML "timeit (@{code test} 25)"
2.23 +ML "timeit (@{code test'} 25)"
2.24 +ML "timeit (@{code test} 500)"
2.25 +ML "timeit @{code test''}"
2.26 +
2.27 +consts_code
2.28 + "default :: nat" ("{* 0::nat *}")
2.29 + "default :: nat \<times> nat" ("{* (0::nat, 0::nat) *}")
2.30 +
2.31 code_module PH
2.32 contains
2.33 test = test
2.34 @@ -254,27 +263,13 @@
2.35 test'' = test''
2.36
2.37 ML "timeit (PH.test 10)"
2.38 -ML "timeit (@{code test} 10)"
2.39 -
2.40 ML "timeit (PH.test' 10)"
2.41 -ML "timeit (@{code test'} 10)"
2.42 -
2.43 ML "timeit (PH.test 20)"
2.44 -ML "timeit (@{code test} 20)"
2.45 -
2.46 ML "timeit (PH.test' 20)"
2.47 -ML "timeit (@{code test'} 20)"
2.48 -
2.49 ML "timeit (PH.test 25)"
2.50 -ML "timeit (@{code test} 25)"
2.51 -
2.52 ML "timeit (PH.test' 25)"
2.53 -ML "timeit (@{code test'} 25)"
2.54 -
2.55 ML "timeit (PH.test 500)"
2.56 -ML "timeit (@{code test} 500)"
2.57 -
2.58 ML "timeit PH.test''"
2.59 -ML "timeit @{code test''}"
2.60
2.61 end
2.62 +
3.1 --- a/src/HOL/Extraction/ROOT.ML Wed Jun 02 16:42:58 2010 +0200
3.2 +++ b/src/HOL/Extraction/ROOT.ML Wed Jun 02 18:48:30 2010 +0200
3.3 @@ -2,5 +2,5 @@
3.4
3.5 Proofterm.proofs := 2;
3.6
3.7 -no_document use_thys ["Efficient_Nat", "~~/src/HOL/Old_Number_Theory/Factorization"];
3.8 +no_document use_thys ["Efficient_Nat", "~~/src/HOL/Number_Theory/UniqueFactorization"];
3.9 use_thys ["Greatest_Common_Divisor", "Warshall", "Higman", "Pigeonhole", "Euclid"];
4.1 --- a/src/HOL/IsaMakefile Wed Jun 02 16:42:58 2010 +0200
4.2 +++ b/src/HOL/IsaMakefile Wed Jun 02 18:48:30 2010 +0200
4.3 @@ -352,6 +352,9 @@
4.4 $(OUT)/HOL-Main: main.ML $(MAIN_DEPENDENCIES)
4.5 @$(ISABELLE_TOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main
4.6
4.7 +$(OUT)/HOL-Proofs: main.ML $(MAIN_DEPENDENCIES)
4.8 + @$(ISABELLE_TOOL) usedir -b -f main.ML -g true -p 2 -q 0 $(OUT)/Pure HOL-Proofs
4.9 +
4.10 HOL_DEPENDENCIES = $(MAIN_DEPENDENCIES) \
4.11 Archimedean_Field.thy \
4.12 Complex.thy \
4.13 @@ -383,9 +386,6 @@
4.14 $(OUT)/HOL: ROOT.ML $(HOL_DEPENDENCIES)
4.15 @$(ISABELLE_TOOL) usedir -b -g true $(OUT)/Pure HOL
4.16
4.17 -$(OUT)/HOL-Proofs: ROOT.ML $(HOL_DEPENDENCIES)
4.18 - @$(ISABELLE_TOOL) usedir -b -g true -p 2 -q 0 $(OUT)/Pure HOL-Proofs
4.19 -
4.20
4.21
4.22 ## HOL-Library
5.1 --- a/src/HOL/List.thy Wed Jun 02 16:42:58 2010 +0200
5.2 +++ b/src/HOL/List.thy Wed Jun 02 18:48:30 2010 +0200
5.3 @@ -451,6 +451,23 @@
5.4 "(\<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> P ys \<Longrightarrow> P xs) \<Longrightarrow> P xs"
5.5 by (rule measure_induct [of length]) iprover
5.6
5.7 +lemma list_nonempty_induct [consumes 1, case_names single cons]:
5.8 + assumes "xs \<noteq> []"
5.9 + assumes single: "\<And>x. P [x]"
5.10 + assumes cons: "\<And>x xs. xs \<noteq> [] \<Longrightarrow> P xs \<Longrightarrow> P (x # xs)"
5.11 + shows "P xs"
5.12 +using `xs \<noteq> []` proof (induct xs)
5.13 + case Nil then show ?case by simp
5.14 +next
5.15 + case (Cons x xs) show ?case proof (cases xs)
5.16 + case Nil with single show ?thesis by simp
5.17 + next
5.18 + case Cons then have "xs \<noteq> []" by simp
5.19 + moreover with Cons.hyps have "P xs" .
5.20 + ultimately show ?thesis by (rule cons)
5.21 + qed
5.22 +qed
5.23 +
5.24
5.25 subsubsection {* @{const length} *}
5.26
6.1 --- a/src/HOL/Number_Theory/Cong.thy Wed Jun 02 16:42:58 2010 +0200
6.2 +++ b/src/HOL/Number_Theory/Cong.thy Wed Jun 02 18:48:30 2010 +0200
6.3 @@ -30,7 +30,7 @@
6.4 header {* Congruence *}
6.5
6.6 theory Cong
6.7 -imports GCD Primes
6.8 +imports Primes
6.9 begin
6.10
6.11 subsection {* Turn off One_nat_def *}
7.1 --- a/src/HOL/Number_Theory/Primes.thy Wed Jun 02 16:42:58 2010 +0200
7.2 +++ b/src/HOL/Number_Theory/Primes.thy Wed Jun 02 18:48:30 2010 +0200
7.3 @@ -28,7 +28,7 @@
7.4 header {* Primes *}
7.5
7.6 theory Primes
7.7 -imports GCD
7.8 +imports "~~/src/HOL/GCD"
7.9 begin
7.10
7.11 declare One_nat_def [simp del]
8.1 --- a/src/HOL/Number_Theory/UniqueFactorization.thy Wed Jun 02 16:42:58 2010 +0200
8.2 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy Wed Jun 02 18:48:30 2010 +0200
8.3 @@ -72,6 +72,14 @@
8.4 translations
8.5 "PROD i :# A. b" == "CONST msetprod (%i. b) A"
8.6
8.7 +lemma msetprod_empty:
8.8 + "msetprod f {#} = 1"
8.9 + by (simp add: msetprod_def)
8.10 +
8.11 +lemma msetprod_singleton:
8.12 + "msetprod f {#x#} = f x"
8.13 + by (simp add: msetprod_def)
8.14 +
8.15 lemma msetprod_Un: "msetprod f (A+B) = msetprod f A * msetprod f B"
8.16 apply (simp add: msetprod_def power_add)
8.17 apply (subst setprod_Un2)