author haftmann Wed, 02 Jun 2010 16:24:13 +0200 changeset 37291 bc874e1a7758 parent 37290 3464d7232670 child 37292 12a514e0319a
dropped lemma duplicate
```--- 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```