# HG changeset patch
# User nipkow
# Date 1224539579 -7200
# Node ID 658b598d8af4eebf95402596cb2ff52ce4e1367a
# Parent  f6e1b2beb766b76fca8d01315628e1c0d962fe17
added lemmas

diff -r f6e1b2beb766 -r 658b598d8af4 src/HOL/List.thy
--- a/src/HOL/List.thy	Sun Oct 19 21:20:55 2008 +0200
+++ b/src/HOL/List.thy	Mon Oct 20 23:52:59 2008 +0200
@@ -2580,6 +2580,21 @@
   by (induct i) (simp_all add: replicate_append_same)
 
 
+lemma replicate_empty[simp]: "(replicate n x = []) \<longleftrightarrow> n=0"
+by (induct n) auto
+
+lemma empty_replicate[simp]: "([] = replicate n x) \<longleftrightarrow> n=0"
+by (induct n) auto
+
+lemma replicate_eq_replicate[simp]:
+  "(replicate m x = replicate n y) \<longleftrightarrow> (m=n & (m\<noteq>0 \<longrightarrow> x=y))"
+apply(induct m arbitrary: n)
+ apply simp
+apply(induct_tac n)
+apply auto
+done
+
+
 subsubsection{*@{text rotate1} and @{text rotate}*}
 
 lemma rotate_simps[simp]: "rotate1 [] = [] \<and> rotate1 (x#xs) = xs @ [x]"
@@ -2779,6 +2794,26 @@
 done
 
 
+subsubsection {* Infiniteness *}
+
+lemma finite_maxlen:
+  "finite (M::'a list set) ==> EX n. ALL s:M. size s < n"
+proof (induct rule: finite.induct)
+  case emptyI show ?case by simp
+next
+  case (insertI M xs)
+  then obtain n where "\<forall>s\<in>M. length s < n" by blast
+  hence "ALL s:insert xs M. size s < max n (size xs) + 1" by auto
+  thus ?case ..
+qed
+
+lemma infinite_UNIV_listI: "~ finite(UNIV::'a list set)"
+apply(rule notI)
+apply(drule finite_maxlen)
+apply (metis UNIV_I length_replicate less_not_refl)
+done
+
+
 subsection {*Sorting*}
 
 text{* Currently it is not shown that @{const sort} returns a