merged

--- a/src/HOL/Library/Nat_Infinity.thy	Fri May 08 08:01:09 2009 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy	Fri May 08 08:07:05 2009 +0200
@@ -24,6 +24,10 @@
   Infty  ("\<infinity>")
 
 
+lemma not_Infty_eq[simp]: "(x ~= Infty) = (EX i. x = Fin i)"
+by (cases x) auto
+
+
 subsection {* Constructors and numbers *}
 
 instantiation inat :: "{zero, one, number}"
@@ -261,6 +265,9 @@
 
 end
 
+instance inat :: linorder
+by intro_classes (auto simp add: less_eq_inat_def split: inat.splits)
+
 instance inat :: pordered_comm_semiring
 proof
   fix a b c :: inat
@@ -413,4 +420,8 @@
 
 lemmas inat_splits = inat.splits
 
+
+instance inat :: linorder
+by intro_classes (auto simp add: inat_defs split: inat.splits)
+
 end

--- a/src/HOL/List.thy	Fri May 08 08:01:09 2009 +0200
+++ b/src/HOL/List.thy	Fri May 08 08:07:05 2009 +0200
@@ -1324,6 +1324,9 @@
 apply simp_all
 done
 
+lemma list_update_nonempty[simp]: "xs[k:=x] = [] \<longleftrightarrow> xs=[]"
+by(metis length_0_conv length_list_update)
+
 lemma list_update_same_conv:
 "i < length xs ==> (xs[i := x] = xs) = (xs!i = x)"
 by (induct xs arbitrary: i) (auto split: nat.split)
@@ -1357,12 +1360,10 @@
 lemma set_update_memI: "n < length xs \<Longrightarrow> x \<in> set (xs[n := x])"
 by (induct xs arbitrary: n) (auto split:nat.splits)
 
-lemma list_update_overwrite:
+lemma list_update_overwrite[simp]:
   "xs [i := x, i := y] = xs [i := y]"
-apply (induct xs arbitrary: i)
-apply simp
-apply (case_tac i)
-apply simp_all
+apply (induct xs arbitrary: i) apply simp
+apply (case_tac i, simp_all)
 done
 
 lemma list_update_swap:
@@ -1444,6 +1445,18 @@
 lemma butlast_conv_take: "butlast xs = take (length xs - 1) xs"
 by (induct xs, simp, case_tac xs, simp_all)
 
+lemma last_list_update:
+  "xs \<noteq> [] \<Longrightarrow> last(xs[k:=x]) = (if k = size xs - 1 then x else last xs)"
+by (auto simp: last_conv_nth)
+
+lemma butlast_list_update:
+  "butlast(xs[k:=x]) =
+ (if k = size xs - 1 then butlast xs else (butlast xs)[k:=x])"
+apply(cases xs rule:rev_cases)
+apply simp
+apply(simp add:list_update_append split:nat.splits)
+done
+
 
 subsubsection {* @{text take} and @{text drop} *}
 
@@ -1723,6 +1736,13 @@
  "(dropWhile P xs = y#ys) = (xs = takeWhile P xs @ y # ys & \<not> P y)"
 by(induct xs, auto)
 
+lemma distinct_takeWhile[simp]: "distinct xs ==> distinct (takeWhile P xs)"
+by (induct xs) (auto dest: set_takeWhileD)
+
+lemma distinct_dropWhile[simp]: "distinct xs ==> distinct (dropWhile P xs)"
+by (induct xs) auto
+
+
 text{* The following two lemmmas could be generalized to an arbitrary
 property. *}
 
@@ -2140,6 +2160,10 @@
 lemma listsum[code unfold]: "listsum xs = foldl (op +) 0 xs"
 by(simp add:listsum_foldr foldl_foldr1)
 
+lemma distinct_listsum_conv_Setsum:
+  "distinct xs \<Longrightarrow> listsum xs = Setsum(set xs)"
+by (induct xs) simp_all
+
 
 text{* Some syntactic sugar for summing a function over a list: *}