equal
deleted
inserted
replaced
95 by (simp only: prime_eq' One_nat_def simp_thms) |
95 by (simp only: prime_eq' One_nat_def simp_thms) |
96 thus ?thesis .. |
96 thus ?thesis .. |
97 qed |
97 qed |
98 qed |
98 qed |
99 |
99 |
100 text {* |
|
101 Unfortunately, the proof in the @{text Factorization} theory using @{text metis} |
|
102 is non-constructive. |
|
103 *} |
|
104 |
|
105 lemma split_primel': |
|
106 "primel xs \<Longrightarrow> primel ys \<Longrightarrow> \<exists>l. primel l \<and> prod l = prod xs * prod ys" |
|
107 apply (rule exI) |
|
108 apply safe |
|
109 apply (rule_tac [2] prod_append) |
|
110 apply (simp add: primel_append) |
|
111 done |
|
112 |
|
113 lemma factor_exists: "Suc 0 < n \<Longrightarrow> (\<exists>l. primel l \<and> prod l = n)" |
100 lemma factor_exists: "Suc 0 < n \<Longrightarrow> (\<exists>l. primel l \<and> prod l = n)" |
114 proof (induct n rule: nat_wf_ind) |
101 proof (induct n rule: nat_wf_ind) |
115 case (1 n) |
102 case (1 n) |
116 from `Suc 0 < n` |
103 from `Suc 0 < n` |
117 have "(\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k) \<or> prime n" |
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" |
127 from kn and k have "\<exists>l. primel l \<and> prod l = k" by (rule 1) |
114 from kn and k have "\<exists>l. primel l \<and> prod l = k" by (rule 1) |
128 then obtain l2 where primel_l2: "primel l2" and prod_l2_k: "prod l2 = k" |
115 then obtain l2 where primel_l2: "primel l2" and prod_l2_k: "prod l2 = k" |
129 by iprover |
116 by iprover |
130 from primel_l1 primel_l2 |
117 from primel_l1 primel_l2 |
131 have "\<exists>l. primel l \<and> prod l = prod l1 * prod l2" |
118 have "\<exists>l. primel l \<and> prod l = prod l1 * prod l2" |
132 by (rule split_primel') |
119 by (rule split_primel) |
133 with prod_l1_m prod_l2_k nmk show ?thesis by simp |
120 with prod_l1_m prod_l2_k nmk show ?thesis by simp |
134 next |
121 next |
135 assume "prime n" |
122 assume "prime n" |
136 hence "primel [n] \<and> prod [n] = n" by (rule prime_primel) |
123 hence "primel [n] \<and> prod [n] = n" by (rule prime_primel) |
137 thus ?thesis .. |
124 thus ?thesis .. |