src/HOL/Finite_Set.thy
 changeset 44890 22f665a2e91c parent 44835 ff6b9eb9c5ef child 44919 482f1807976e
```--- a/src/HOL/Finite_Set.thy	Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Finite_Set.thy	Mon Sep 12 07:55:43 2011 +0200
@@ -124,7 +124,7 @@

lemma finite_Collect_less_nat [iff]:
"finite {n::nat. n < k}"
-  by (fastsimp simp: finite_conv_nat_seg_image)
+  by (fastforce simp: finite_conv_nat_seg_image)

lemma finite_Collect_le_nat [iff]:
"finite {n::nat. n \<le> k}"
@@ -2040,7 +2040,7 @@
show "A = insert b (A-{b})" using b by blast
show "b \<notin> A - {b}" by blast
show "card (A - {b}) = k" and "k = 0 \<longrightarrow> A - {b} = {}"
-      using assms b fin by(fastsimp dest:mk_disjoint_insert)+
+      using assms b fin by(fastforce dest:mk_disjoint_insert)+
qed
qed

@@ -2056,7 +2056,7 @@

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
+by (fastforce simp: card_Suc_eq less_eq_nat.simps(2) insert_eq_iff
dest: subset_singletonD split: nat.splits if_splits)

lemma finite_fun_UNIVD2:
@@ -2242,7 +2242,7 @@

lemma finite_UNIV_inj_surj: fixes f :: "'a \<Rightarrow> 'a"
shows "finite(UNIV:: 'a set) \<Longrightarrow> inj f \<Longrightarrow> surj f"
-by(fastsimp simp:surj_def dest!: endo_inj_surj)
+by(fastforce simp:surj_def dest!: endo_inj_surj)

corollary infinite_UNIV_nat[iff]: "~finite(UNIV::nat set)"
proof```