--- a/src/HOL/Extraction/Euclid.thy Wed Jun 02 15:35:14 2010 +0200
+++ b/src/HOL/Extraction/Euclid.thy Wed Jun 02 16:24:13 2010 +0200
@@ -10,23 +10,6 @@
imports "~~/src/HOL/Number_Theory/UniqueFactorization" Util Efficient_Nat
begin
-lemma list_nonempty_induct [consumes 1, case_names single cons]:
- assumes "xs \<noteq> []"
- assumes single: "\<And>x. P [x]"
- assumes cons: "\<And>x xs. xs \<noteq> [] \<Longrightarrow> P xs \<Longrightarrow> P (x # xs)"
- shows "P xs"
-using `xs \<noteq> []` proof (induct xs)
- case Nil then show ?case by simp
-next
- case (Cons x xs) show ?case proof (cases xs)
- case Nil with single show ?thesis by simp
- next
- case Cons then have "xs \<noteq> []" by simp
- moreover with Cons.hyps have "P xs" .
- ultimately show ?thesis by (rule cons)
- qed
-qed
-
text {*
A constructive version of the proof of Euclid's theorem by
Markus Wenzel and Freek Wiedijk \cite{Wenzel-Wiedijk-JAR2002}.
@@ -285,6 +268,7 @@
lemma "factor_exists 345 = [23, 5, 3]" by evaluation
lemma "factor_exists 999 = [37, 3, 3, 3]" by evaluation
lemma "factor_exists 876 = [73, 3, 2, 2]" by evaluation
+
lemma "iterate 4 Euclid 0 = [2, 3, 7, 71]" by evaluation
end