# HG changeset patch
# User nipkow
# Date 1315311916 -7200
# Node ID bdf8eb8f126b1a13df6e58f7f8d0b12764e98036
# Parent  804dfa6d35b65ad21287c327e39e905eab00554e
added new lemmas

diff -r 804dfa6d35b6 -r bdf8eb8f126b src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Sep 06 11:31:01 2011 +0200
+++ b/src/HOL/Finite_Set.thy	Tue Sep 06 14:25:16 2011 +0200
@@ -2054,6 +2054,11 @@
  apply(auto intro:ccontr)
 done
 
+lemma card_le_Suc_iff: "finite A \<Longrightarrow>
+  Suc n \<le> card A = (\<exists>a B. A = insert a B \<and> a \<notin> B \<and> n \<le> card B \<and> finite B)"
+by (fastsimp simp: card_Suc_eq less_eq_nat.simps(2) insert_eq_iff
+  dest: subset_singletonD split: nat.splits if_splits)
+
 lemma finite_fun_UNIVD2:
   assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
   shows "finite (UNIV :: 'b set)"
diff -r 804dfa6d35b6 -r bdf8eb8f126b src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Tue Sep 06 11:31:01 2011 +0200
+++ b/src/HOL/Fun.thy	Tue Sep 06 14:25:16 2011 +0200
@@ -612,6 +612,10 @@
 lemma fun_upd_comp: "f \<circ> (g(x := y)) = (f \<circ> g)(x := f y)"
 by (auto intro: ext)
 
+lemma UNION_fun_upd:
+  "UNION J (A(i:=B)) = (UNION (J-{i}) A \<union> (if i\<in>J then B else {}))"
+by (auto split: if_splits)
+
 
 subsection {* @{text override_on} *}
 
diff -r 804dfa6d35b6 -r bdf8eb8f126b src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue Sep 06 11:31:01 2011 +0200
+++ b/src/HOL/Set.thy	Tue Sep 06 14:25:16 2011 +0200
@@ -785,6 +785,26 @@
 lemma insert_ident: "x ~: A ==> x ~: B ==> (insert x A = insert x B) = (A = B)"
 by auto
 
+lemma insert_eq_iff: assumes "a \<notin> A" "b \<notin> B"
+shows "insert a A = insert b B \<longleftrightarrow>
+  (if a=b then A=B else \<exists>C. A = insert b C \<and> b \<notin> C \<and> B = insert a C \<and> a \<notin> C)"
+  (is "?L \<longleftrightarrow> ?R")
+proof
+  assume ?L
+  show ?R
+  proof cases
+    assume "a=b" with assms `?L` show ?R by (simp add: insert_ident)
+  next
+    assume "a\<noteq>b"
+    let ?C = "A - {b}"
+    have "A = insert b ?C \<and> b \<notin> ?C \<and> B = insert a ?C \<and> a \<notin> ?C"
+      using assms `?L` `a\<noteq>b` by auto
+    thus ?R using `a\<noteq>b` by auto
+  qed
+next
+  assume ?R thus ?L by(auto split: if_splits)
+qed
+
 subsubsection {* Singletons, using insert *}
 
 lemma singletonI [intro!,no_atp]: "a : {a}"