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

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