# HG changeset patch
# User nipkow
# Date 1071804525 -3600
# Node ID 6c24235e8d5de545351e1febb2ee1759912fc0c2
# Parent  48dc606749bd6f32c367074c8ac6fb3204300ac3
*** empty log message ***

diff -r 48dc606749bd -r 6c24235e8d5d src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Thu Dec 18 15:06:24 2003 +0100
+++ b/src/HOL/Finite_Set.thy	Fri Dec 19 04:28:45 2003 +0100
@@ -431,7 +431,9 @@
   by (simp add: insert_absorb)
 
 lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
-by (rule_tac t = A in insert_Diff [THEN subst], assumption, simp)
+apply(rule_tac t = A in insert_Diff [THEN subst], assumption)
+apply(simp del:insert_Diff_single)
+done
 
 lemma card_Diff_singleton:
     "finite A ==> x: A ==> card (A - {x}) = card A - 1"
@@ -860,7 +862,7 @@
   apply (erule ssubst)
   apply (drule spec)
   apply (erule (1) notE impE)
-  apply (simp add: Ball_def)
+  apply (simp add: Ball_def del:insert_Diff_single)
   done
 
 subsubsection{* Min and Max of finite linearly ordered sets *}
diff -r 48dc606749bd -r 6c24235e8d5d src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Dec 18 15:06:24 2003 +0100
+++ b/src/HOL/List.thy	Fri Dec 19 04:28:45 2003 +0100
@@ -758,6 +758,23 @@
 lemma butlast_snoc [simp]: "butlast (xs @ [x]) = xs"
 by (induct xs) auto
 
+lemma last_ConsL: "xs = [] \<Longrightarrow> last(x#xs) = x"
+by(simp add:last.simps)
+
+lemma last_ConsR: "xs \<noteq> [] \<Longrightarrow> last(x#xs) = last xs"
+by(simp add:last.simps)
+
+lemma last_append: "last(xs @ ys) = (if ys = [] then last xs else last ys)"
+by (induct xs) (auto)
+
+lemma last_appendL[simp]: "ys = [] \<Longrightarrow> last(xs @ ys) = last xs"
+by(simp add:last_append)
+
+lemma last_appendR[simp]: "ys \<noteq> [] \<Longrightarrow> last(xs @ ys) = last ys"
+by(simp add:last_append)
+
+
+
 lemma length_butlast [simp]: "length (butlast xs) = length xs - 1"
 by (induct xs rule: rev_induct) auto
 
@@ -1111,6 +1128,10 @@
   "\<lbrakk> list_all2 P xs ys; p < size xs \<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
   by (simp add: list_all2_conv_all_nth)
 
+lemma list_all2_nthD2:
+  "\<lbrakk>list_all2 P xs ys; p < size ys\<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
+  by (frule list_all2_lengthD) (auto intro: list_all2_nthD)
+
 lemma list_all2_map1: 
   "list_all2 P (map f as) bs = list_all2 (\<lambda>x y. P (f x) y) as bs"
   by (simp add: list_all2_conv_all_nth)
@@ -1131,7 +1152,16 @@
   "\<lbrakk>list_all2 P xs ys; P x y; i < length ys\<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
   by (simp add: list_all2_lengthD list_all2_update_cong)
 
-lemma list_all2_dropI [intro?]:
+lemma list_all2_takeI [simp,intro?]:
+  "\<And>n ys. list_all2 P xs ys \<Longrightarrow> list_all2 P (take n xs) (take n ys)"
+  apply (induct xs)
+   apply simp
+  apply (clarsimp simp add: list_all2_Cons1)
+  apply (case_tac n)
+  apply auto
+  done
+
+lemma list_all2_dropI [simp,intro?]:
   "\<And>n bs. list_all2 P as bs \<Longrightarrow> list_all2 P (drop n as) (drop n bs)"
   apply (induct as, simp)
   apply (clarsimp simp add: list_all2_Cons1)
diff -r 48dc606749bd -r 6c24235e8d5d src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Thu Dec 18 15:06:24 2003 +0100
+++ b/src/HOL/Nat.thy	Fri Dec 19 04:28:45 2003 +0100
@@ -268,6 +268,12 @@
   apply (blast intro: Suc_mono less_SucI elim: lessE)
   done
 
+text {* "Less than" is antisymmetric, sort of *}
+lemma less_antisym: "\<lbrakk> \<not> n < m; n < Suc m \<rbrakk> \<Longrightarrow> m = n"
+apply(simp only:less_Suc_eq)
+apply blast
+done
+
 lemma nat_neq_iff: "((m::nat) \<noteq> n) = (m < n | n < m)"
   using less_linear by blast
 
diff -r 48dc606749bd -r 6c24235e8d5d src/HOL/Set.thy
--- a/src/HOL/Set.thy	Thu Dec 18 15:06:24 2003 +0100
+++ b/src/HOL/Set.thy	Fri Dec 19 04:28:45 2003 +0100
@@ -895,6 +895,9 @@
   apply (erule insertI2)
   done
 
+lemma subset_insertI2: "A \<subseteq> B \<Longrightarrow> A \<subseteq> insert b B"
+by blast
+
 lemma subset_insert: "x \<notin> A ==> (A \<subseteq> insert x B) = (A \<subseteq> B)"
   by blast
 
@@ -961,6 +964,9 @@
 lemma Diff_subset: "A - B \<subseteq> A"
   by blast
 
+lemma Diff_subset_conv: "(A - B \<subseteq> C) = (A \<subseteq> B \<union> C)"
+by blast
+
 
 text {* \medskip Monotonicity. *}
 
@@ -1052,6 +1058,9 @@
 lemma UN_insert_distrib: "u \<in> A ==> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)"
   by blast
 
+lemma insert_inter_insert[simp]: "insert a A \<inter> insert a B = insert a (A \<inter> B)"
+by blast
+
 lemma insert_disjoint[simp]:
  "(insert a A \<inter> B = {}) = (a \<notin> B \<and> A \<inter> B = {})"
 by blast
@@ -1495,6 +1504,9 @@
 lemma Diff_cancel [simp]: "A - A = {}"
   by blast
 
+lemma Diff_idemp [simp]: "(A - B) - B = A - (B::'a set)"
+by blast
+
 lemma Diff_triv: "A \<inter> B = {} ==> A - B = A"
   by (blast elim: equalityE)
 
@@ -1524,6 +1536,9 @@
 lemma insert_Diff1 [simp]: "x \<in> B ==> insert x A - B = A - B"
   by blast
 
+lemma insert_Diff_single[simp]: "insert a (A - {a}) = insert a A"
+by blast
+
 lemma insert_Diff: "a \<in> A ==> insert a (A - {a}) = A"
   by blast