author blanchet Mon, 18 Nov 2013 18:04:45 +0100 changeset 54477 f001ef2637d3 parent 54476 478b4aa26a4c child 54478 215d41768e51
moved theorems out of LFP
--- 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"
-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

--- 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