# HG changeset patch
# User huffman
# Date 1166120988 -3600
# Node ID a2e7a79159e40ca8f9e552e572db7dd30e75523d
# Parent  b35faf14a89f152562eb56622592d61f6a2f1110
add lemmas singleton and insert_iff

diff -r b35faf14a89f -r a2e7a79159e4 src/HOL/Hyperreal/Filter.thy
--- a/src/HOL/Hyperreal/Filter.thy	Thu Dec 14 19:15:16 2006 +0100
+++ b/src/HOL/Hyperreal/Filter.thy	Thu Dec 14 19:29:48 2006 +0100
@@ -68,6 +68,15 @@
 lemma (in freeultrafilter) finite: "finite A \<Longrightarrow> A \<notin> F"
 by (erule contrapos_pn, erule infinite)
 
+lemma (in freeultrafilter) singleton: "{x} \<notin> F"
+by (rule finite, simp)
+
+lemma (in freeultrafilter) insert_iff: "(insert x A \<in> F) = (A \<in> F)"
+apply (subst insert_is_Un)
+apply (subst Un_iff)
+apply (simp add: singleton)
+done
+
 lemma (in freeultrafilter) filter: "filter F" by unfold_locales
 
 lemma (in freeultrafilter) ultrafilter: "ultrafilter F"