--- a/src/HOL/BNF_Cardinal_Order_Relation.thy Tue Jan 21 16:56:34 2014 +0100
+++ b/src/HOL/BNF_Cardinal_Order_Relation.thy Wed Jan 22 09:45:30 2014 +0100
@@ -38,7 +38,7 @@
text{* A cardinal order in our setting shall be a well-order {\em minim} w.r.t. the
order-embedding relation, @{text "\<le>o"} (which is the same as being {\em minimal} w.r.t. the
-strict order-embedding relation, @{text "<o"}), among all the well-orders on its field. *}
+strict order-embedding relation, @{text "<o"}), among all the well-orders on its field. *}
definition card_order_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool"
where
@@ -115,7 +115,7 @@
text{* We define the cardinal of set to be {\em some} cardinal order on that set.
We shall prove that this notion is unique up to order isomorphism, meaning
-that order isomorphism shall be the true identity of cardinals. *}
+that order isomorphism shall be the true identity of cardinals. *}
definition card_of :: "'a set \<Rightarrow> 'a rel" ("|_|" )
where "card_of A = (SOME r. card_order_on A r)"
@@ -827,7 +827,7 @@
theorem @{text "Card_order_Times_same_infinite"}, which states that self-product
does not increase cardinality -- the proof of this fact adapts a standard
set-theoretic argument, as presented, e.g., in the proof of theorem 1.5.11
-at page 47 in \cite{card-book}. Then everything else follows fairly easily. *}
+at page 47 in \cite{card-book}. Then everything else follows fairly easily. *}
lemma infinite_iff_card_of_nat:
"\<not> finite A \<longleftrightarrow> ( |UNIV::nat set| \<le>o |A| )"
@@ -1141,13 +1141,13 @@
qed
-subsection {* The cardinal $\omega$ and the finite cardinals *}
+subsection {* The cardinal $\omega$ and the finite cardinals *}
text{* The cardinal $\omega$, of natural numbers, shall be the standard non-strict
order relation on
@{text "nat"}, that we abbreviate by @{text "natLeq"}. The finite cardinals
shall be the restrictions of these relations to the numbers smaller than
-fixed numbers @{text "n"}, that we abbreviate by @{text "natLeq_on n"}. *}
+fixed numbers @{text "n"}, that we abbreviate by @{text "natLeq_on n"}. *}
abbreviation "(natLeq::(nat * nat) set) \<equiv> {(x,y). x \<le> y}"
abbreviation "(natLess::(nat * nat) set) \<equiv> {(x,y). x < y}"
@@ -1263,7 +1263,7 @@
text{* First we define @{text "isCardSuc r r'"}, the notion of @{text "r'"}
being a successor cardinal of @{text "r"}. Although the definition does
-not require @{text "r"} to be a cardinal, only this case will be meaningful. *}
+not require @{text "r"} to be a cardinal, only this case will be meaningful. *}
definition isCardSuc :: "'a rel \<Rightarrow> 'a set rel \<Rightarrow> bool"
where
@@ -1314,7 +1314,7 @@
using cardSuc_greater ordLeq_iff_ordLess_or_ordIso by blast
text{* The minimality property of @{text "cardSuc"} originally present in its definition
-is local to the type @{text "'a set rel"}, i.e., that of @{text "cardSuc r"}: *}
+is local to the type @{text "'a set rel"}, i.e., that of @{text "cardSuc r"}: *}
lemma cardSuc_least_aux:
"\<lbrakk>Card_order (r::'a rel); Card_order (r'::'a set rel); r <o r'\<rbrakk> \<Longrightarrow> cardSuc r \<le>o r'"
--- a/src/HOL/BNF_Constructions_on_Wellorders.thy Tue Jan 21 16:56:34 2014 +0100
+++ b/src/HOL/BNF_Constructions_on_Wellorders.thy Wed Jan 22 09:45:30 2014 +0100
@@ -11,7 +11,6 @@
imports BNF_Wellorder_Embedding
begin
-
text {* In this section, we study basic constructions on well-orders, such as restriction to
a set/order filter, copy via direct images, ordinal-like sum of disjoint well-orders,
and bounded square. We also define between well-orders
@@ -19,59 +18,48 @@
@{text "ordLess"}, of being strictly embedded (abbreviated @{text "<o"}), and
@{text "ordIso"}, of being isomorphic (abbreviated @{text "=o"}). We study the
connections between these relations, order filters, and the aforementioned constructions.
-A main result of this section is that @{text "<o"} is well-founded. *}
+A main result of this section is that @{text "<o"} is well-founded. *}
-subsection {* Restriction to a set *}
-
+subsection {* Restriction to a set *}
abbreviation Restr :: "'a rel \<Rightarrow> 'a set \<Rightarrow> 'a rel"
where "Restr r A \<equiv> r Int (A \<times> A)"
-
lemma Restr_subset:
"A \<le> B \<Longrightarrow> Restr (Restr r B) A = Restr r A"
by blast
-
lemma Restr_Field: "Restr r (Field r) = r"
unfolding Field_def by auto
-
lemma Refl_Restr: "Refl r \<Longrightarrow> Refl(Restr r A)"
unfolding refl_on_def Field_def by auto
-
lemma antisym_Restr:
"antisym r \<Longrightarrow> antisym(Restr r A)"
unfolding antisym_def Field_def by auto
-
lemma Total_Restr:
"Total r \<Longrightarrow> Total(Restr r A)"
unfolding total_on_def Field_def by auto
-
lemma trans_Restr:
"trans r \<Longrightarrow> trans(Restr r A)"
unfolding trans_def Field_def by blast
-
lemma Preorder_Restr:
"Preorder r \<Longrightarrow> Preorder(Restr r A)"
unfolding preorder_on_def by (simp add: Refl_Restr trans_Restr)
-
lemma Partial_order_Restr:
"Partial_order r \<Longrightarrow> Partial_order(Restr r A)"
unfolding partial_order_on_def by (simp add: Preorder_Restr antisym_Restr)
-
lemma Linear_order_Restr:
"Linear_order r \<Longrightarrow> Linear_order(Restr r A)"
unfolding linear_order_on_def by (simp add: Partial_order_Restr Total_Restr)
-
lemma Well_order_Restr:
assumes "Well_order r"
shows "Well_order(Restr r A)"
@@ -83,21 +71,17 @@
by (simp add: Linear_order_Restr)
qed
-
lemma Field_Restr_subset: "Field(Restr r A) \<le> A"
by (auto simp add: Field_def)
-
lemma Refl_Field_Restr:
"Refl r \<Longrightarrow> Field(Restr r A) = (Field r) Int A"
unfolding refl_on_def Field_def by blast
-
lemma Refl_Field_Restr2:
"\<lbrakk>Refl r; A \<le> Field r\<rbrakk> \<Longrightarrow> Field(Restr r A) = A"
by (auto simp add: Refl_Field_Restr)
-
lemma well_order_on_Restr:
assumes WELL: "Well_order r" and SUB: "A \<le> Field r"
shows "well_order_on A (Restr r A)"
@@ -106,14 +90,12 @@
order_on_defs[of "Field r" r] by auto
-subsection {* Order filters versus restrictions and embeddings *}
-
+subsection {* Order filters versus restrictions and embeddings *}
lemma Field_Restr_ofilter:
"\<lbrakk>Well_order r; wo_rel.ofilter r A\<rbrakk> \<Longrightarrow> Field(Restr r A) = A"
by (auto simp add: wo_rel_def wo_rel.ofilter_def wo_rel.REFL Refl_Field_Restr2)
-
lemma ofilter_Restr_under:
assumes WELL: "Well_order r" and OF: "wo_rel.ofilter r A" and IN: "a \<in> A"
shows "under (Restr r A) a = under r a"
@@ -125,7 +107,6 @@
thus "b \<in> A" using * assms by (auto simp add: wo_rel_def wo_rel.ofilter_def)
qed
-
lemma ofilter_embed:
assumes "Well_order r"
shows "wo_rel.ofilter r A = (A \<le> Field r \<and> embed (Restr r A) r id)"
@@ -159,7 +140,6 @@
thus "wo_rel.ofilter r A" using assms * by (simp add: wo_rel_def wo_rel.ofilter_def)
qed
-
lemma ofilter_Restr_Int:
assumes WELL: "Well_order r" and OFA: "wo_rel.ofilter r A"
shows "wo_rel.ofilter (Restr r B) (A Int B)"
@@ -183,7 +163,6 @@
qed
qed
-
lemma ofilter_Restr_subset:
assumes WELL: "Well_order r" and OFA: "wo_rel.ofilter r A" and SUB: "A \<le> B"
shows "wo_rel.ofilter (Restr r B) A"
@@ -192,7 +171,6 @@
thus ?thesis using assms ofilter_Restr_Int[of r A B] by auto
qed
-
lemma ofilter_subset_embed:
assumes WELL: "Well_order r" and
OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B"
@@ -231,7 +209,6 @@
qed
qed
-
lemma ofilter_subset_embedS_iso:
assumes WELL: "Well_order r" and
OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B"
@@ -255,14 +232,12 @@
FieldA FieldB bij_betw_id_iff[of A B] by auto
qed
-
lemma ofilter_subset_embedS:
assumes WELL: "Well_order r" and
OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B"
shows "(A < B) = embedS (Restr r A) (Restr r B) id"
using assms by (simp add: ofilter_subset_embedS_iso)
-
lemma embed_implies_iso_Restr:
assumes WELL: "Well_order r" and WELL': "Well_order r'" and
EMB: "embed r' r f"
@@ -288,13 +263,11 @@
subsection {* The strict inclusion on proper ofilters is well-founded *}
-
definition ofilterIncl :: "'a rel \<Rightarrow> 'a set rel"
where
"ofilterIncl r \<equiv> {(A,B). wo_rel.ofilter r A \<and> A \<noteq> Field r \<and>
wo_rel.ofilter r B \<and> B \<noteq> Field r \<and> A < B}"
-
lemma wf_ofilterIncl:
assumes WELL: "Well_order r"
shows "wf(ofilterIncl r)"
@@ -329,10 +302,8 @@
qed
-
subsection {* Ordering the well-orders by existence of embeddings *}
-
text {* We define three relations between well-orders:
\begin{itemize}
\item @{text "ordLeq"}, of being embedded (abbreviated @{text "\<le>o"});
@@ -345,20 +316,16 @@
@{text "\<le>"}, @{text "<"}, @{text "="} associated to a total order on a set.
*}
-
definition ordLeq :: "('a rel * 'a' rel) set"
where
"ordLeq = {(r,r'). Well_order r \<and> Well_order r' \<and> (\<exists>f. embed r r' f)}"
-
abbreviation ordLeq2 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "<=o" 50)
where "r <=o r' \<equiv> (r,r') \<in> ordLeq"
-
abbreviation ordLeq3 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "\<le>o" 50)
where "r \<le>o r' \<equiv> r <=o r'"
-
definition ordLess :: "('a rel * 'a' rel) set"
where
"ordLess = {(r,r'). Well_order r \<and> Well_order r' \<and> (\<exists>f. embedS r r' f)}"
@@ -366,7 +333,6 @@
abbreviation ordLess2 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "<o" 50)
where "r <o r' \<equiv> (r,r') \<in> ordLess"
-
definition ordIso :: "('a rel * 'a' rel) set"
where
"ordIso = {(r,r'). Well_order r \<and> Well_order r' \<and> (\<exists>f. iso r r' f)}"
@@ -374,7 +340,6 @@
abbreviation ordIso2 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "=o" 50)
where "r =o r' \<equiv> (r,r') \<in> ordIso"
-
lemmas ordRels_def = ordLeq_def ordLess_def ordIso_def
lemma ordLeq_Well_order_simp:
@@ -382,18 +347,15 @@
shows "Well_order r \<and> Well_order r'"
using assms unfolding ordLeq_def by simp
-
text{* Notice that the relations @{text "\<le>o"}, @{text "<o"}, @{text "=o"} connect well-orders
on potentially {\em distinct} types. However, some of the lemmas below, including the next one,
restrict implicitly the type of these relations to @{text "(('a rel) * ('a rel)) set"} , i.e.,
-to @{text "'a rel rel"}. *}
-
+to @{text "'a rel rel"}. *}
lemma ordLeq_reflexive:
"Well_order r \<Longrightarrow> r \<le>o r"
unfolding ordLeq_def using id_embed[of r] by blast
-
lemma ordLeq_transitive[trans]:
assumes *: "r \<le>o r'" and **: "r' \<le>o r''"
shows "r \<le>o r''"
@@ -407,17 +369,14 @@
thus "r \<le>o r''" unfolding ordLeq_def using 1 by auto
qed
-
lemma ordLeq_total:
"\<lbrakk>Well_order r; Well_order r'\<rbrakk> \<Longrightarrow> r \<le>o r' \<or> r' \<le>o r"
unfolding ordLeq_def using wellorders_totally_ordered by blast
-
lemma ordIso_reflexive:
"Well_order r \<Longrightarrow> r =o r"
unfolding ordIso_def using id_iso[of r] by blast
-
lemma ordIso_transitive[trans]:
assumes *: "r =o r'" and **: "r' =o r''"
shows "r =o r''"
@@ -431,7 +390,6 @@
thus "r =o r''" unfolding ordIso_def using 1 by auto
qed
-
lemma ordIso_symmetric:
assumes *: "r =o r'"
shows "r' =o r"
@@ -445,7 +403,6 @@
thus "r' =o r" unfolding ordIso_def using 1 by (auto simp add: iso_def)
qed
-
lemma ordLeq_ordLess_trans[trans]:
assumes "r \<le>o r'" and " r' <o r''"
shows "r <o r''"
@@ -456,7 +413,6 @@
using embed_comp_embedS by blast
qed
-
lemma ordLess_ordLeq_trans[trans]:
assumes "r <o r'" and " r' \<le>o r''"
shows "r <o r''"
@@ -467,7 +423,6 @@
using embedS_comp_embed by blast
qed
-
lemma ordLeq_ordIso_trans[trans]:
assumes "r \<le>o r'" and " r' =o r''"
shows "r \<le>o r''"
@@ -478,7 +433,6 @@
using embed_comp_iso by blast
qed
-
lemma ordIso_ordLeq_trans[trans]:
assumes "r =o r'" and " r' \<le>o r''"
shows "r \<le>o r''"
@@ -489,7 +443,6 @@
using iso_comp_embed by blast
qed
-
lemma ordLess_ordIso_trans[trans]:
assumes "r <o r'" and " r' =o r''"
shows "r <o r''"
@@ -500,7 +453,6 @@
using embedS_comp_iso by blast
qed
-
lemma ordIso_ordLess_trans[trans]:
assumes "r =o r'" and " r' <o r''"
shows "r <o r''"
@@ -511,7 +463,6 @@
using iso_comp_embedS by blast
qed
-
lemma ordLess_not_embed:
assumes "r <o r'"
shows "\<not>(\<exists>f'. embed r' r f')"
@@ -527,7 +478,6 @@
thus ?thesis by blast
qed
-
lemma ordLess_Field:
assumes OL: "r1 <o r2" and EMB: "embed r1 r2 f"
shows "\<not> (f`(Field r1) = Field r2)"
@@ -546,7 +496,6 @@
ultimately show ?thesis by (simp add: bij_betw_def)
qed
-
lemma ordLess_iff:
"r <o r' = (Well_order r \<and> Well_order r' \<and> \<not>(\<exists>f'. embed r' r f'))"
proof
@@ -568,7 +517,6 @@
unfolding ordLess_def using * by (fastforce simp add: embedS_def)
qed
-
lemma ordLess_irreflexive: "\<not> r <o r"
proof
assume "r <o r"
@@ -578,12 +526,10 @@
ultimately show False by blast
qed
-
lemma ordLeq_iff_ordLess_or_ordIso:
"r \<le>o r' = (r <o r' \<or> r =o r')"
unfolding ordRels_def embedS_defs iso_defs by blast
-
lemma ordIso_iff_ordLeq:
"(r =o r') = (r \<le>o r' \<and> r' \<le>o r)"
proof
@@ -604,12 +550,10 @@
thus "r =o r'" unfolding ordIso_def using 1 by auto
qed
-
lemma not_ordLess_ordLeq:
"r <o r' \<Longrightarrow> \<not> r' \<le>o r"
using ordLess_ordLeq_trans ordLess_irreflexive by blast
-
lemma ordLess_or_ordLeq:
assumes WELL: "Well_order r" and WELL': "Well_order r'"
shows "r <o r' \<or> r' \<le>o r"
@@ -624,46 +568,37 @@
ultimately show ?thesis by blast
qed
-
lemma not_ordLess_ordIso:
"r <o r' \<Longrightarrow> \<not> r =o r'"
using assms ordLess_ordIso_trans ordIso_symmetric ordLess_irreflexive by blast
-
lemma not_ordLeq_iff_ordLess:
assumes WELL: "Well_order r" and WELL': "Well_order r'"
shows "(\<not> r' \<le>o r) = (r <o r')"
using assms not_ordLess_ordLeq ordLess_or_ordLeq by blast
-
lemma not_ordLess_iff_ordLeq:
assumes WELL: "Well_order r" and WELL': "Well_order r'"
shows "(\<not> r' <o r) = (r \<le>o r')"
using assms not_ordLess_ordLeq ordLess_or_ordLeq by blast
-
lemma ordLess_transitive[trans]:
"\<lbrakk>r <o r'; r' <o r''\<rbrakk> \<Longrightarrow> r <o r''"
using assms ordLess_ordLeq_trans ordLeq_iff_ordLess_or_ordIso by blast
-
corollary ordLess_trans: "trans ordLess"
unfolding trans_def using ordLess_transitive by blast
-
lemmas ordIso_equivalence = ordIso_transitive ordIso_reflexive ordIso_symmetric
-
lemma ordIso_imp_ordLeq:
"r =o r' \<Longrightarrow> r \<le>o r'"
using ordIso_iff_ordLeq by blast
-
lemma ordLess_imp_ordLeq:
"r <o r' \<Longrightarrow> r \<le>o r'"
using ordLeq_iff_ordLess_or_ordIso by blast
-
lemma ofilter_subset_ordLeq:
assumes WELL: "Well_order r" and
OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B"
@@ -687,7 +622,6 @@
wo_rel_def[of r] wo_rel.ofilter_linord[of r A B] by blast
qed
-
lemma ofilter_subset_ordLess:
assumes WELL: "Well_order r" and
OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B"
@@ -705,13 +639,11 @@
finally show ?thesis .
qed
-
lemma ofilter_ordLess:
"\<lbrakk>Well_order r; wo_rel.ofilter r A\<rbrakk> \<Longrightarrow> (A < Field r) = (Restr r A <o r)"
by (simp add: ofilter_subset_ordLess wo_rel.Field_ofilter
wo_rel_def Restr_Field)
-
corollary underS_Restr_ordLess:
assumes "Well_order r" and "Field r \<noteq> {}"
shows "Restr r (underS r a) <o r"
@@ -722,7 +654,6 @@
by (simp add: ofilter_ordLess wo_rel.underS_ofilter wo_rel_def)
qed
-
lemma embed_ordLess_ofilterIncl:
assumes
OL12: "r1 <o r2" and OL23: "r2 <o r3" and
@@ -769,7 +700,6 @@
unfolding ofilterIncl_def by auto
qed
-
lemma ordLess_iff_ordIso_Restr:
assumes WELL: "Well_order r" and WELL': "Well_order r'"
shows "(r' <o r) = (\<exists>a \<in> Field r. r' =o Restr r (underS r a))"
@@ -795,7 +725,6 @@
thus "\<exists>a \<in> Field r. r' =o Restr r (underS r a)" using 3 by auto
qed
-
lemma internalize_ordLess:
"(r' <o r) = (\<exists>p. Field p < Field r \<and> r' =o p \<and> p <o r)"
proof
@@ -816,7 +745,6 @@
thus "r' <o r" using ordIso_ordLess_trans by blast
qed
-
lemma internalize_ordLeq:
"(r' \<le>o r) = (\<exists>p. Field p \<le> Field r \<and> r' =o p \<and> p \<le>o r)"
proof
@@ -837,7 +765,6 @@
thus "r' \<le>o r" using ordIso_ordLeq_trans by blast
qed
-
lemma ordLeq_iff_ordLess_Restr:
assumes WELL: "Well_order r" and WELL': "Well_order r'"
shows "(r \<le>o r') = (\<forall>a \<in> Field r. Restr r (underS r a) <o r')"
@@ -858,7 +785,6 @@
thus "r \<le>o r'" using ordLess_or_ordLeq assms by blast
qed
-
lemma finite_ordLess_infinite:
assumes WELL: "Well_order r" and WELL': "Well_order r'" and
FIN: "finite(Field r)" and INF: "\<not>finite(Field r')"
@@ -872,7 +798,6 @@
thus ?thesis using WELL WELL' ordLess_or_ordLeq by blast
qed
-
lemma finite_well_order_on_ordIso:
assumes FIN: "finite A" and
WELL: "well_order_on A r" and WELL': "well_order_on A r'"
@@ -897,21 +822,17 @@
ultimately show ?thesis using assms ordLeq_total ordIso_symmetric by metis
qed
-
subsection{* @{text "<o"} is well-founded *}
-
text {* Of course, it only makes sense to state that the @{text "<o"} is well-founded
on the restricted type @{text "'a rel rel"}. We prove this by first showing that, for any set
of well-orders all embedded in a fixed well-order, the function mapping each well-order
in the set to an order filter of the fixed well-order is compatible w.r.t. to @{text "<o"} versus
{\em strict inclusion}; and we already know that strict inclusion of order filters is well-founded. *}
-
definition ord_to_filter :: "'a rel \<Rightarrow> 'a rel \<Rightarrow> 'a set"
where "ord_to_filter r0 r \<equiv> (SOME f. embed r r0 f) ` (Field r)"
-
lemma ord_to_filter_compat:
"compat (ordLess Int (ordLess^-1``{r0} \<times> ordLess^-1``{r0}))
(ofilterIncl r0)
@@ -929,7 +850,6 @@
using * ** by (simp add: embed_ordLess_ofilterIncl)
qed
-
theorem wf_ordLess: "wf ordLess"
proof-
{fix r0 :: "('a \<times> 'a) set"
@@ -963,30 +883,24 @@
qed
-
-subsection {* Copy via direct images *}
-
+subsection {* Copy via direct images *}
text{* The direct image operator is the dual of the inverse image operator @{text "inv_image"}
from @{text "Relation.thy"}. It is useful for transporting a well-order between
different types. *}
-
definition dir_image :: "'a rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> 'a' rel"
where
"dir_image r f = {(f a, f b)| a b. (a,b) \<in> r}"
-
lemma dir_image_Field:
"Field(dir_image r f) \<le> f ` (Field r)"
unfolding dir_image_def Field_def by auto
-
lemma dir_image_minus_Id:
"inj_on f (Field r) \<Longrightarrow> (dir_image r f) - Id = dir_image (r - Id) f"
unfolding inj_on_def Field_def dir_image_def by auto
-
lemma Refl_dir_image:
assumes "Refl r"
shows "Refl(dir_image r f)"
@@ -1004,7 +918,6 @@
by(unfold refl_on_def Field_def Domain_def Range_def, auto)
qed
-
lemma trans_dir_image:
assumes TRANS: "trans r" and INJ: "inj_on f (Field r)"
shows "trans(dir_image r f)"
@@ -1022,12 +935,10 @@
unfolding dir_image_def using 1 by auto
qed
-
lemma Preorder_dir_image:
"\<lbrakk>Preorder r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Preorder (dir_image r f)"
by (simp add: preorder_on_def Refl_dir_image trans_dir_image)
-
lemma antisym_dir_image:
assumes AN: "antisym r" and INJ: "inj_on f (Field r)"
shows "antisym(dir_image r f)"
@@ -1043,12 +954,10 @@
thus "a' = b'" using 1 by auto
qed
-
lemma Partial_order_dir_image:
"\<lbrakk>Partial_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Partial_order (dir_image r f)"
by (simp add: partial_order_on_def Preorder_dir_image antisym_dir_image)
-
lemma Total_dir_image:
assumes TOT: "Total r" and INJ: "inj_on f (Field r)"
shows "Total(dir_image r f)"
@@ -1064,12 +973,10 @@
using 1 unfolding dir_image_def by auto
qed
-
lemma Linear_order_dir_image:
"\<lbrakk>Linear_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Linear_order (dir_image r f)"
by (simp add: linear_order_on_def Partial_order_dir_image Total_dir_image)
-
lemma wf_dir_image:
assumes WF: "wf r" and INJ: "inj_on f (Field r)"
shows "wf(dir_image r f)"
@@ -1095,7 +1002,6 @@
using A_def 1 by blast
qed
-
lemma Well_order_dir_image:
"\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Well_order (dir_image r f)"
using assms unfolding well_order_on_def
@@ -1104,33 +1010,27 @@
subset_inj_on[of f "Field r" "Field(r - Id)"]
mono_Field[of "r - Id" r] by auto
-
lemma dir_image_Field2:
"Refl r \<Longrightarrow> Field(dir_image r f) = f ` (Field r)"
unfolding Field_def dir_image_def refl_on_def Domain_def Range_def by blast
-
lemma dir_image_bij_betw:
"\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> bij_betw f (Field r) (Field (dir_image r f))"
unfolding bij_betw_def
by (simp add: dir_image_Field2 order_on_defs)
-
lemma dir_image_compat:
"compat r (dir_image r f) f"
unfolding compat_def dir_image_def by auto
-
lemma dir_image_iso:
"\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> iso r (dir_image r f) f"
using iso_iff3 dir_image_compat dir_image_bij_betw Well_order_dir_image by blast
-
lemma dir_image_ordIso:
"\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> r =o dir_image r f"
unfolding ordIso_def using dir_image_iso Well_order_dir_image by blast
-
lemma Well_order_iso_copy:
assumes WELL: "well_order_on A r" and BIJ: "bij_betw f A A'"
shows "\<exists>r'. well_order_on A' r' \<and> r =o r'"
@@ -1149,9 +1049,7 @@
qed
-
-subsection {* Bounded square *}
-
+subsection {* Bounded square *}
text{* This construction essentially defines, for an order relation @{text "r"}, a lexicographic
order @{text "bsqr r"} on @{text "(Field r) \<times> (Field r)"}, applying the
@@ -1168,7 +1066,6 @@
construction) is that any proper order filter of the product order is included in a rectangle, i.e.,
in a product of proper filters on the original relation (assumed to be a well-order). *}
-
definition bsqr :: "'a rel => ('a * 'a)rel"
where
"bsqr r = {((a1,a2),(b1,b2)).
@@ -1179,7 +1076,6 @@
wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> a1 = b1 \<and> (a2,b2) \<in> r - Id
)}"
-
lemma Field_bsqr:
"Field (bsqr r) = Field r \<times> Field r"
proof
@@ -1202,11 +1098,9 @@
qed
qed
-
lemma bsqr_Refl: "Refl(bsqr r)"
by(unfold refl_on_def Field_bsqr, auto simp add: bsqr_def)
-
lemma bsqr_Trans:
assumes "Well_order r"
shows "trans (bsqr r)"
@@ -1296,7 +1190,6 @@
qed
qed
-
lemma bsqr_antisym:
assumes "Well_order r"
shows "antisym (bsqr r)"
@@ -1367,7 +1260,6 @@
qed
qed
-
lemma bsqr_Total:
assumes "Well_order r"
shows "Total(bsqr r)"
@@ -1485,14 +1377,12 @@
thus ?thesis unfolding total_on_def by fast
qed
-
lemma bsqr_Linear_order:
assumes "Well_order r"
shows "Linear_order(bsqr r)"
unfolding order_on_defs
using assms bsqr_Refl bsqr_Trans bsqr_antisym bsqr_Total by blast
-
lemma bsqr_Well_order:
assumes "Well_order r"
shows "Well_order(bsqr r)"
@@ -1557,7 +1447,6 @@
ultimately show "\<exists>d \<in> D. \<forall>d' \<in> D. (d,d') \<in> bsqr r" by fastforce
qed
-
lemma bsqr_max2:
assumes WELL: "Well_order r" and LEQ: "((a1,a2),(b1,b2)) \<in> bsqr r"
shows "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r"
@@ -1572,7 +1461,6 @@
ultimately show ?thesis using WELL unfolding order_on_defs refl_on_def by auto
qed
-
lemma bsqr_ofilter:
assumes WELL: "Well_order r" and
OF: "wo_rel.ofilter (bsqr r) D" and SUB: "D < Field r \<times> Field r" and
--- a/src/HOL/BNF_Wellorder_Embedding.thy Tue Jan 21 16:56:34 2014 +0100
+++ b/src/HOL/BNF_Wellorder_Embedding.thy Wed Jan 22 09:45:30 2014 +0100
@@ -11,7 +11,6 @@
imports Zorn BNF_Wellorder_Relation
begin
-
text{* In this section, we introduce well-order {\em embeddings} and {\em isomorphisms} and
prove their basic properties. The notion of embedding is considered from the point
of view of the theory of ordinals, and therefore requires the source to be injected
@@ -36,7 +35,6 @@
by (auto simp add: inj_on_UNION_chain)
qed
-
lemma under_underS_bij_betw:
assumes WELL: "Well_order r" and WELL': "Well_order r'" and
IN: "a \<in> Field r" and IN': "f a \<in> Field r'" and
@@ -57,10 +55,8 @@
qed
-
subsection {* (Well-order) embeddings, strict embeddings, isomorphisms and order-compatible
-functions *}
-
+functions *}
text{* Standardly, a function is an embedding of a well-order in another if it injectively and
order-compatibly maps the former into an order filter of the latter.
@@ -70,40 +66,32 @@
and the set of strict lower bounds of its image. (Later we prove equivalence with
the standard definition -- lemma @{text "embed_iff_compat_inj_on_ofilter"}.)
A {\em strict embedding} (operator @{text "embedS"}) is a non-bijective embedding
-and an isomorphism (operator @{text "iso"}) is a bijective embedding. *}
-
+and an isomorphism (operator @{text "iso"}) is a bijective embedding. *}
definition embed :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool"
where
"embed r r' f \<equiv> \<forall>a \<in> Field r. bij_betw f (under r a) (under r' (f a))"
-
lemmas embed_defs = embed_def embed_def[abs_def]
-
text {* Strict embeddings: *}
definition embedS :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool"
where
"embedS r r' f \<equiv> embed r r' f \<and> \<not> bij_betw f (Field r) (Field r')"
-
lemmas embedS_defs = embedS_def embedS_def[abs_def]
-
definition iso :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool"
where
"iso r r' f \<equiv> embed r r' f \<and> bij_betw f (Field r) (Field r')"
-
lemmas iso_defs = iso_def iso_def[abs_def]
-
definition compat :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool"
where
"compat r r' f \<equiv> \<forall>a b. (a,b) \<in> r \<longrightarrow> (f a, f b) \<in> r'"
-
lemma compat_wf:
assumes CMP: "compat r r' f" and WF: "wf r'"
shows "wf r"
@@ -115,15 +103,12 @@
using wf_inv_image[of r' f] wf_subset[of "inv_image r' f"] by auto
qed
-
lemma id_embed: "embed r r id"
by(auto simp add: id_def embed_def bij_betw_def)
-
lemma id_iso: "iso r r id"
by(auto simp add: id_def embed_def iso_def bij_betw_def)
-
lemma embed_in_Field:
assumes WELL: "Well_order r" and
EMB: "embed r r' f" and IN: "a \<in> Field r"
@@ -140,7 +125,6 @@
by (auto simp: under_def)
qed
-
lemma comp_embed:
assumes WELL: "Well_order r" and
EMB: "embed r r' f" and EMB': "embed r' r'' f'"
@@ -160,7 +144,6 @@
by(auto simp add: bij_betw_trans)
qed
-
lemma comp_iso:
assumes WELL: "Well_order r" and
EMB: "iso r r' f" and EMB': "iso r' r'' f'"
@@ -168,15 +151,12 @@
using assms unfolding iso_def
by (auto simp add: comp_embed bij_betw_trans)
-
-text{* That @{text "embedS"} is also preserved by function composition shall be proved only later. *}
-
+text{* That @{text "embedS"} is also preserved by function composition shall be proved only later. *}
lemma embed_Field:
"\<lbrakk>Well_order r; embed r r' f\<rbrakk> \<Longrightarrow> f`(Field r) \<le> Field r'"
by (auto simp add: embed_in_Field)
-
lemma embed_preserves_ofilter:
assumes WELL: "Well_order r" and WELL': "Well_order r'" and
EMB: "embed r r' f" and OF: "wo_rel.ofilter r A"
@@ -204,7 +184,6 @@
qed
qed
-
lemma embed_Field_ofilter:
assumes WELL: "Well_order r" and WELL': "Well_order r'" and
EMB: "embed r r' f"
@@ -216,7 +195,6 @@
show ?thesis by (auto simp add: embed_preserves_ofilter)
qed
-
lemma embed_compat:
assumes EMB: "embed r r' f"
shows "compat r r' f"
@@ -234,7 +212,6 @@
by (auto simp add: under_def)
qed
-
lemma embed_inj_on:
assumes WELL: "Well_order r" and EMB: "embed r r' f"
shows "inj_on f (Field r)"
@@ -271,7 +248,6 @@
by (auto simp add: total_on_def)
qed
-
lemma embed_underS:
assumes WELL: "Well_order r" and WELL': "Well_order r'" and
EMB: "embed r r' f" and IN: "a \<in> Field r"
@@ -293,7 +269,6 @@
by (auto simp add: notIn_Un_bij_betw3)
qed
-
lemma embed_iff_compat_inj_on_ofilter:
assumes WELL: "Well_order r" and WELL': "Well_order r'"
shows "embed r r' f = (compat r r' f \<and> inj_on f (Field r) \<and> wo_rel.ofilter r' (f`(Field r)))"
@@ -366,7 +341,6 @@
qed
qed
-
lemma inv_into_ofilter_embed:
assumes WELL: "Well_order r" and OF: "wo_rel.ofilter r A" and
BIJ: "\<forall>b \<in> A. bij_betw f (under r b) (under r' (f b))" and
@@ -442,7 +416,6 @@
thus ?thesis unfolding embed_def .
qed
-
lemma inv_into_underS_embed:
assumes WELL: "Well_order r" and
BIJ: "\<forall>b \<in> underS r a. bij_betw f (under r b) (under r' (f b))" and
@@ -452,7 +425,6 @@
using assms
by(auto simp add: wo_rel_def wo_rel.underS_ofilter inv_into_ofilter_embed)
-
lemma inv_into_Field_embed:
assumes WELL: "Well_order r" and EMB: "embed r r' f" and
IMAGE: "Field r' \<le> f ` (Field r)"
@@ -468,7 +440,6 @@
by(auto simp add: wo_rel_def wo_rel.Field_ofilter inv_into_ofilter_embed)
qed
-
lemma inv_into_Field_embed_bij_betw:
assumes WELL: "Well_order r" and
EMB: "embed r r' f" and BIJ: "bij_betw f (Field r) (Field r')"
@@ -481,12 +452,8 @@
qed
-
-
-
subsection {* Given any two well-orders, one can be embedded in the other *}
-
text{* Here is an overview of the proof of of this fact, stated in theorem
@{text "wellorders_totally_ordered"}:
@@ -506,7 +473,6 @@
(lemma @{text "wellorders_totally_ordered_aux2"}).
*}
-
lemma wellorders_totally_ordered_aux:
fixes r ::"'a rel" and r'::"'a' rel" and
f :: "'a \<Rightarrow> 'a'" and a::'a
@@ -616,7 +582,6 @@
using WELL WELL' IN BIJ under_underS_bij_betw[of r r' a f] by auto
qed
-
lemma wellorders_totally_ordered_aux2:
fixes r ::"'a rel" and r'::"'a' rel" and
f :: "'a \<Rightarrow> 'a'" and g :: "'a \<Rightarrow> bool" and a::'a
@@ -696,7 +661,6 @@
unfolding embed_def by blast
qed
-
theorem wellorders_totally_ordered:
fixes r ::"'a rel" and r'::"'a' rel"
assumes WELL: "Well_order r" and WELL': "Well_order r'"
@@ -805,15 +769,13 @@
qed
-subsection {* Uniqueness of embeddings *}
-
+subsection {* Uniqueness of embeddings *}
text{* Here we show a fact complementary to the one from the previous subsection -- namely,
that between any two well-orders there is {\em at most} one embedding, and is the one
definable by the expected well-order recursive equation. As a consequence, any two
embeddings of opposite directions are mutually inverse. *}
-
lemma embed_determined:
assumes WELL: "Well_order r" and WELL': "Well_order r'" and
EMB: "embed r r' f" and IN: "a \<in> Field r"
@@ -832,7 +794,6 @@
ultimately show ?thesis by simp
qed
-
lemma embed_unique:
assumes WELL: "Well_order r" and WELL': "Well_order r'" and
EMBf: "embed r r' f" and EMBg: "embed r r' g"
@@ -848,7 +809,6 @@
using assms * embed_determined[of r r' f a] embed_determined[of r r' g a] by auto
qed
-
lemma embed_bothWays_inverse:
assumes WELL: "Well_order r" and WELL': "Well_order r'" and
EMB: "embed r r' f" and EMB': "embed r' r f'"
@@ -871,7 +831,6 @@
ultimately show ?thesis by blast
qed
-
lemma embed_bothWays_bij_betw:
assumes WELL: "Well_order r" and WELL': "Well_order r'" and
EMB: "embed r r' f" and EMB': "embed r' r g"
@@ -899,7 +858,6 @@
qed
qed
-
lemma embed_bothWays_iso:
assumes WELL: "Well_order r" and WELL': "Well_order r'" and
EMB: "embed r r' f" and EMB': "embed r' r g"
@@ -907,8 +865,7 @@
unfolding iso_def using assms by (auto simp add: embed_bothWays_bij_betw)
-subsection {* More properties of embeddings, strict embeddings and isomorphisms *}
-
+subsection {* More properties of embeddings, strict embeddings and isomorphisms *}
lemma embed_bothWays_Field_bij_betw:
assumes WELL: "Well_order r" and WELL': "Well_order r'" and
@@ -924,7 +881,6 @@
show ?thesis using bij_betw_byWitness[of "Field r" f' f "Field r'"] by auto
qed
-
lemma embedS_comp_embed:
assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
and EMB: "embedS r r' f" and EMB': "embed r' r'' f'"
@@ -948,7 +904,6 @@
ultimately show ?thesis unfolding embedS_def by auto
qed
-
lemma embed_comp_embedS:
assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
and EMB: "embed r r' f" and EMB': "embedS r' r'' f'"
@@ -972,7 +927,6 @@
ultimately show ?thesis unfolding embedS_def by auto
qed
-
lemma embed_comp_iso:
assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
and EMB: "embed r r' f" and EMB': "iso r' r'' f'"
@@ -980,7 +934,6 @@
using assms unfolding iso_def
by (auto simp add: comp_embed)
-
lemma iso_comp_embed:
assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
and EMB: "iso r r' f" and EMB': "embed r' r'' f'"
@@ -988,7 +941,6 @@
using assms unfolding iso_def
by (auto simp add: comp_embed)
-
lemma embedS_comp_iso:
assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
and EMB: "embedS r r' f" and EMB': "iso r' r'' f'"
@@ -996,7 +948,6 @@
using assms unfolding iso_def
by (auto simp add: embedS_comp_embed)
-
lemma iso_comp_embedS:
assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
and EMB: "iso r r' f" and EMB': "embedS r' r'' f'"
@@ -1004,7 +955,6 @@
using assms unfolding iso_def using embed_comp_embedS
by (auto simp add: embed_comp_embedS)
-
lemma embedS_Field:
assumes WELL: "Well_order r" and EMB: "embedS r r' f"
shows "f ` (Field r) < Field r'"
@@ -1020,7 +970,6 @@
ultimately show ?thesis by blast
qed
-
lemma embedS_iff:
assumes WELL: "Well_order r" and ISO: "embed r r' f"
shows "embedS r r' f = (f ` (Field r) < Field r')"
@@ -1036,12 +985,10 @@
using ISO by auto
qed
-
lemma iso_Field:
"iso r r' f \<Longrightarrow> f ` (Field r) = Field r'"
using assms by (auto simp add: iso_def bij_betw_def)
-
lemma iso_iff:
assumes "Well_order r"
shows "iso r r' f = (embed r r' f \<and> f ` (Field r) = Field r')"
@@ -1057,7 +1004,6 @@
with * show "iso r r' f" unfolding iso_def by auto
qed
-
lemma iso_iff2:
assumes "Well_order r"
shows "iso r r' f = (bij_betw f (Field r) (Field r') \<and>
@@ -1110,7 +1056,6 @@
thus "embed r r' f" unfolding embed_def using * by auto
qed
-
lemma iso_iff3:
assumes WELL: "Well_order r" and WELL': "Well_order r'"
shows "iso r r' f = (bij_betw f (Field r) (Field r') \<and> compat r r' f)"
@@ -1140,6 +1085,4 @@
qed
qed
-
-
end
--- a/src/HOL/BNF_Wellorder_Relation.thy Tue Jan 21 16:56:34 2014 +0100
+++ b/src/HOL/BNF_Wellorder_Relation.thy Wed Jan 22 09:45:30 2014 +0100
@@ -11,13 +11,11 @@
imports Order_Relation
begin
-
text{* In this section, we develop basic concepts and results pertaining
to well-order relations. Note that we consider well-order relations
as {\em non-strict relations},
i.e., as containing the diagonals of their fields. *}
-
locale wo_rel =
fixes r :: "'a rel"
assumes WELL: "Well_order r"
@@ -40,49 +38,39 @@
subsection {* Auxiliaries *}
-
lemma REFL: "Refl r"
using WELL order_on_defs[of _ r] by auto
-
lemma TRANS: "trans r"
using WELL order_on_defs[of _ r] by auto
-
lemma ANTISYM: "antisym r"
using WELL order_on_defs[of _ r] by auto
-
lemma TOTAL: "Total r"
using WELL order_on_defs[of _ r] by auto
-
lemma TOTALS: "\<forall>a \<in> Field r. \<forall>b \<in> Field r. (a,b) \<in> r \<or> (b,a) \<in> r"
using REFL TOTAL refl_on_def[of _ r] total_on_def[of _ r] by force
-
lemma LIN: "Linear_order r"
using WELL well_order_on_def[of _ r] by auto
-
lemma WF: "wf (r - Id)"
using WELL well_order_on_def[of _ r] by auto
-
lemma cases_Total:
"\<And> phi a b. \<lbrakk>{a,b} <= Field r; ((a,b) \<in> r \<Longrightarrow> phi a b); ((b,a) \<in> r \<Longrightarrow> phi a b)\<rbrakk>
\<Longrightarrow> phi a b"
using TOTALS by auto
-
lemma cases_Total3:
"\<And> phi a b. \<lbrakk>{a,b} \<le> Field r; ((a,b) \<in> r - Id \<or> (b,a) \<in> r - Id \<Longrightarrow> phi a b);
(a = b \<Longrightarrow> phi a b)\<rbrakk> \<Longrightarrow> phi a b"
using TOTALS by auto
-subsection {* Well-founded induction and recursion adapted to non-strict well-order relations *}
-
+subsection {* Well-founded induction and recursion adapted to non-strict well-order relations *}
text{* Here we provide induction and recursion principles specific to {\em non-strict}
well-order relations.
@@ -90,7 +78,6 @@
for doing away with the tediousness of
having to take out the diagonal each time in order to switch to a well-founded relation. *}
-
lemma well_order_induct:
assumes IND: "\<And>x. \<forall>y. y \<noteq> x \<and> (y, x) \<in> r \<longrightarrow> P y \<Longrightarrow> P x"
shows "P a"
@@ -100,19 +87,16 @@
thus "P a" using WF wf_induct[of "r - Id" P a] by blast
qed
-
definition
worec :: "(('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
where
"worec F \<equiv> wfrec (r - Id) F"
-
definition
adm_wo :: "(('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> bool"
where
"adm_wo H \<equiv> \<forall>f g x. (\<forall>y \<in> underS x. f y = g y) \<longrightarrow> H f x = H g x"
-
lemma worec_fixpoint:
assumes ADM: "adm_wo H"
shows "worec H = H (worec H)"
@@ -127,8 +111,7 @@
qed
-subsection {* The notions of maximum, minimum, supremum, successor and order filter *}
-
+subsection {* The notions of maximum, minimum, supremum, successor and order filter *}
text{*
We define the successor {\em of a set}, and not of an element (the latter is of course
@@ -141,18 +124,15 @@
meaningful for sets for which strict upper bounds exist.
Order filters for well-orders are also known as ``initial segments". *}
-
definition max2 :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
where "max2 a b \<equiv> if (a,b) \<in> r then b else a"
-
definition isMinim :: "'a set \<Rightarrow> 'a \<Rightarrow> bool"
where "isMinim A b \<equiv> b \<in> A \<and> (\<forall>a \<in> A. (b,a) \<in> r)"
definition minim :: "'a set \<Rightarrow> 'a"
where "minim A \<equiv> THE b. isMinim A b"
-
definition supr :: "'a set \<Rightarrow> 'a"
where "supr A \<equiv> minim (Above A)"
@@ -166,7 +146,6 @@
subsubsection {* Properties of max2 *}
-
lemma max2_greater_among:
assumes "a \<in> Field r" and "b \<in> Field r"
shows "(a, max2 a b) \<in> r \<and> (b, max2 a b) \<in> r \<and> max2 a b \<in> {a,b}"
@@ -191,26 +170,22 @@
total_on_def[of "Field r" r] by blast
qed
-
lemma max2_greater:
assumes "a \<in> Field r" and "b \<in> Field r"
shows "(a, max2 a b) \<in> r \<and> (b, max2 a b) \<in> r"
using assms by (auto simp add: max2_greater_among)
-
lemma max2_among:
assumes "a \<in> Field r" and "b \<in> Field r"
shows "max2 a b \<in> {a, b}"
using assms max2_greater_among[of a b] by simp
-
lemma max2_equals1:
assumes "a \<in> Field r" and "b \<in> Field r"
shows "(max2 a b = a) = ((b,a) \<in> r)"
using assms ANTISYM unfolding antisym_def using TOTALS
by(auto simp add: max2_def max2_among)
-
lemma max2_equals2:
assumes "a \<in> Field r" and "b \<in> Field r"
shows "(max2 a b = b) = ((a,b) \<in> r)"
@@ -220,7 +195,6 @@
subsubsection {* Existence and uniqueness for isMinim and well-definedness of minim *}
-
lemma isMinim_unique:
assumes MINIM: "isMinim B a" and MINIM': "isMinim B a'"
shows "a = a'"
@@ -240,7 +214,6 @@
show ?thesis using ANTISYM antisym_def[of r] by blast
qed
-
lemma Well_order_isMinim_exists:
assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}"
shows "\<exists>b. isMinim B b"
@@ -269,7 +242,6 @@
qed
qed
-
lemma minim_isMinim:
assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}"
shows "isMinim B (minim B)"
@@ -284,10 +256,8 @@
unfolding minim_def using theI[of ?phi b] by blast
qed
-
subsubsection{* Properties of minim *}
-
lemma minim_in:
assumes "B \<le> Field r" and "B \<noteq> {}"
shows "minim B \<in> B"
@@ -297,7 +267,6 @@
thus ?thesis by (simp add: isMinim_def)
qed
-
lemma minim_inField:
assumes "B \<le> Field r" and "B \<noteq> {}"
shows "minim B \<in> Field r"
@@ -306,7 +275,6 @@
thus ?thesis using assms by blast
qed
-
lemma minim_least:
assumes SUB: "B \<le> Field r" and IN: "b \<in> B"
shows "(minim B, b) \<in> r"
@@ -316,7 +284,6 @@
thus ?thesis by (auto simp add: isMinim_def IN)
qed
-
lemma equals_minim:
assumes SUB: "B \<le> Field r" and IN: "a \<in> B" and
LEAST: "\<And> b. b \<in> B \<Longrightarrow> (a,b) \<in> r"
@@ -329,10 +296,8 @@
using isMinim_unique by auto
qed
-
subsubsection{* Properties of successor *}
-
lemma suc_AboveS:
assumes SUB: "B \<le> Field r" and ABOVES: "AboveS B \<noteq> {}"
shows "suc B \<in> AboveS B"
@@ -343,7 +308,6 @@
using assms by (simp add: minim_in)
qed
-
lemma suc_greater:
assumes SUB: "B \<le> Field r" and ABOVES: "AboveS B \<noteq> {}" and
IN: "b \<in> B"
@@ -354,7 +318,6 @@
with IN AboveS_def[of r] show ?thesis by simp
qed
-
lemma suc_least_AboveS:
assumes ABOVES: "a \<in> AboveS B"
shows "(suc B,a) \<in> r"
@@ -365,7 +328,6 @@
using assms minim_least by simp
qed
-
lemma suc_inField:
assumes "B \<le> Field r" and "AboveS B \<noteq> {}"
shows "suc B \<in> Field r"
@@ -375,7 +337,6 @@
using assms AboveS_Field[of r] by auto
qed
-
lemma equals_suc_AboveS:
assumes SUB: "B \<le> Field r" and ABV: "a \<in> AboveS B" and
MINIM: "\<And> a'. a' \<in> AboveS B \<Longrightarrow> (a,a') \<in> r"
@@ -388,7 +349,6 @@
by simp
qed
-
lemma suc_underS:
assumes IN: "a \<in> Field r"
shows "a = suc (underS a)"
@@ -432,7 +392,6 @@
subsubsection {* Properties of order filters *}
-
lemma under_ofilter:
"ofilter (under a)"
proof(unfold ofilter_def under_def, auto simp add: Field_def)
@@ -442,7 +401,6 @@
using TRANS trans_def[of r] by blast
qed
-
lemma underS_ofilter:
"ofilter (underS a)"
proof(unfold ofilter_def underS_def under_def, auto simp add: Field_def)
@@ -456,12 +414,10 @@
using TRANS trans_def[of r] by blast
qed
-
lemma Field_ofilter:
"ofilter (Field r)"
by(unfold ofilter_def under_def, auto simp add: Field_def)
-
lemma ofilter_underS_Field:
"ofilter A = ((\<exists>a \<in> Field r. A = underS a) \<or> (A = Field r))"
proof
@@ -523,12 +479,10 @@
qed
qed
-
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
-
lemma ofilter_under_UNION:
assumes "ofilter A"
shows "A = (\<Union> a \<in> A. under a)"
@@ -542,10 +496,8 @@
thus "A \<le> (\<Union> a \<in> A. under a)" by blast
qed
-
subsubsection{* Other properties *}
-
lemma ofilter_linord:
assumes OF1: "ofilter A" and OF2: "ofilter B"
shows "A \<le> B \<or> B \<le> A"
@@ -587,7 +539,6 @@
qed
qed
-
lemma ofilter_AboveS_Field:
assumes "ofilter A"
shows "A \<union> (AboveS A) = Field r"
@@ -614,7 +565,6 @@
thus "Field r \<le> A \<union> (AboveS A)" by blast
qed
-
lemma suc_ofilter_in:
assumes OF: "ofilter A" and ABOVE_NE: "AboveS A \<noteq> {}" and
REL: "(b,suc A) \<in> r" and DIFF: "b \<noteq> suc A"
@@ -633,10 +583,6 @@
thus ?thesis by blast
qed
-
-
end (* context wo_rel *)
-
-
end