# HG changeset patch
# User blanchet
# Date 1384794285 -3600
# Node ID f001ef2637d31c55eafba837eb8127c5be84b7a8
# Parent  478b4aa26a4c18819b1b726267c58a2d0909a1b0
moved theorems out of LFP

diff -r 478b4aa26a4c -r f001ef2637d3 src/HOL/Cardinals/Wellorder_Relation.thy
--- a/src/HOL/Cardinals/Wellorder_Relation.thy	Mon Nov 18 18:04:45 2013 +0100
+++ b/src/HOL/Cardinals/Wellorder_Relation.thy	Mon Nov 18 18:04:45 2013 +0100
@@ -64,17 +64,7 @@
 
 lemma minim_Under:
 "\<lbrakk>B \<le> Field r; B \<noteq> {}\<rbrakk> \<Longrightarrow> minim B \<in> Under B"
-by(auto simp add: Under_def
-minim_in
-minim_inField
-minim_least
-under_ofilter
-underS_ofilter
-Field_ofilter
-ofilter_Under
-ofilter_UnderS
-ofilter_Un
-)
+by(auto simp add: Under_def minim_inField minim_least)
 
 lemma equals_minim_Under:
 "\<lbrakk>B \<le> Field r; a \<in> B; a \<in> Under B\<rbrakk>
@@ -410,7 +400,41 @@
 qed
 
 
-subsubsection {* Properties of order filters  *}
+subsubsection {* Properties of order filters *}
+
+lemma ofilter_Under[simp]:
+assumes "A \<le> Field r"
+shows "ofilter(Under A)"
+proof(unfold ofilter_def, auto)
+  fix x assume "x \<in> Under A"
+  thus "x \<in> Field r"
+  using Under_Field assms by auto
+next
+  fix a x
+  assume "a \<in> Under A" and "x \<in> under a"
+  thus "x \<in> Under A"
+  using TRANS under_Under_trans by auto
+qed
+
+lemma ofilter_UnderS[simp]:
+assumes "A \<le> Field r"
+shows "ofilter(UnderS A)"
+proof(unfold ofilter_def, auto)
+  fix x assume "x \<in> UnderS A"
+  thus "x \<in> Field r"
+  using UnderS_Field assms by auto
+next
+  fix a x
+  assume "a \<in> UnderS A" and "x \<in> under a"
+  thus "x \<in> UnderS A"
+  using TRANS ANTISYM under_UnderS_trans by auto
+qed
+
+lemma ofilter_Int[simp]: "\<lbrakk>ofilter A; ofilter B\<rbrakk> \<Longrightarrow> ofilter(A Int B)"
+unfolding ofilter_def by blast
+
+lemma ofilter_Un[simp]: "\<lbrakk>ofilter A; ofilter B\<rbrakk> \<Longrightarrow> ofilter(A \<union> B)"
+unfolding ofilter_def by blast
 
 lemma ofilter_INTER:
 "\<lbrakk>I \<noteq> {}; \<And> i. i \<in> I \<Longrightarrow> ofilter(A i)\<rbrakk> \<Longrightarrow> ofilter (\<Inter> i \<in> I. A i)"
@@ -496,10 +520,6 @@
   under_ofilter[simp]
   underS_ofilter[simp]
   Field_ofilter[simp]
-  ofilter_Under[simp]
-  ofilter_UnderS[simp]
-  ofilter_Int[simp]
-  ofilter_Un[simp]
 
 end
 
diff -r 478b4aa26a4c -r f001ef2637d3 src/HOL/Cardinals/Wellorder_Relation_LFP.thy
--- a/src/HOL/Cardinals/Wellorder_Relation_LFP.thy	Mon Nov 18 18:04:45 2013 +0100
+++ b/src/HOL/Cardinals/Wellorder_Relation_LFP.thy	Mon Nov 18 18:04:45 2013 +0100
@@ -419,7 +419,7 @@
 qed
 
 
-subsubsection {* Properties of order filters  *}
+subsubsection {* Properties of order filters *}
 
 
 lemma under_ofilter:
@@ -513,44 +513,6 @@
 qed
 
 
-lemma ofilter_Under:
-assumes "A \<le> Field r"
-shows "ofilter(Under A)"
-proof(unfold ofilter_def, auto)
-  fix x assume "x \<in> Under A"
-  thus "x \<in> Field r"
-  using Under_Field assms by auto
-next
-  fix a x
-  assume "a \<in> Under A" and "x \<in> under a"
-  thus "x \<in> Under A"
-  using TRANS under_Under_trans by auto
-qed
-
-
-lemma ofilter_UnderS:
-assumes "A \<le> Field r"
-shows "ofilter(UnderS A)"
-proof(unfold ofilter_def, auto)
-  fix x assume "x \<in> UnderS A"
-  thus "x \<in> Field r"
-  using UnderS_Field assms by auto
-next
-  fix a x
-  assume "a \<in> UnderS A" and "x \<in> under a"
-  thus "x \<in> UnderS A"
-  using TRANS ANTISYM under_UnderS_trans by auto
-qed
-
-
-lemma ofilter_Int: "\<lbrakk>ofilter A; ofilter B\<rbrakk> \<Longrightarrow> ofilter(A Int B)"
-unfolding ofilter_def by blast
-
-
-lemma ofilter_Un: "\<lbrakk>ofilter A; ofilter B\<rbrakk> \<Longrightarrow> ofilter(A \<union> B)"
-unfolding ofilter_def by blast
-
-
 lemma ofilter_UNION:
 "(\<And> i. i \<in> I \<Longrightarrow> ofilter(A i)) \<Longrightarrow> ofilter (\<Union> i \<in> I. A i)"
 unfolding ofilter_def by blast