--- a/src/HOL/BNF_Wellorder_Constructions.thy Fri Jan 13 16:44:00 2023 +0000
+++ b/src/HOL/BNF_Wellorder_Constructions.thy Fri Jan 13 22:47:40 2023 +0000
@@ -8,7 +8,7 @@
section \<open>Constructions on Wellorders as Needed by Bounded Natural Functors\<close>
theory BNF_Wellorder_Constructions
-imports BNF_Wellorder_Embedding
+ imports BNF_Wellorder_Embedding
begin
text \<open>In this section, we study basic constructions on well-orders, such as restriction to
@@ -70,13 +70,8 @@
lemma Well_order_Restr:
assumes "Well_order r"
shows "Well_order(Restr r A)"
-proof-
- have "Restr r A - Id \<le> r - Id" using Restr_subset by blast
- hence "wf(Restr r A - Id)" using assms
- using well_order_on_def wf_subset by blast
- thus ?thesis using assms unfolding well_order_on_def
- by (simp add: Linear_order_Restr)
-qed
+ using assms
+ by (auto simp: well_order_on_def Linear_order_Restr elim: wf_subset)
lemma Field_Restr_subset: "Field(Restr r A) \<le> A"
by (auto simp add: Field_def)
@@ -92,7 +87,7 @@
lemma well_order_on_Restr:
assumes WELL: "Well_order r" and SUB: "A \<le> Field r"
shows "well_order_on A (Restr r A)"
- using assms
+ using assms
using Well_order_Restr[of r A] Refl_Field_Restr2[of r A]
order_on_defs[of "Field r" r] by auto
@@ -100,12 +95,12 @@
subsection \<open>Order filters versus restrictions and embeddings\<close>
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)
+ "\<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"
+ 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"
unfolding wo_rel.ofilter_def under_def
proof
show "{b. (b, a) \<in> Restr r A} \<subseteq> {b. (b, a) \<in> r}"
@@ -125,51 +120,51 @@
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)"
+ assumes "Well_order r"
+ shows "wo_rel.ofilter r A = (A \<le> Field r \<and> embed (Restr r A) r id)"
proof
assume *: "wo_rel.ofilter r A"
show "A \<le> Field r \<and> embed (Restr r A) r id"
- unfolding embed_def
+ unfolding embed_def
proof safe
fix a assume "a \<in> A" thus "a \<in> Field r" using assms *
- by (auto simp add: wo_rel_def wo_rel.ofilter_def)
+ by (auto simp add: wo_rel_def wo_rel.ofilter_def)
next
fix a assume "a \<in> Field (Restr r A)"
thus "bij_betw id (under (Restr r A) a) (under r (id a))" using assms *
- by (simp add: ofilter_Restr_under Field_Restr_ofilter)
+ by (simp add: ofilter_Restr_under Field_Restr_ofilter)
qed
next
assume *: "A \<le> Field r \<and> embed (Restr r A) r id"
hence "Field(Restr r A) \<le> Field r"
- using assms embed_Field[of "Restr r A" r id] id_def
- Well_order_Restr[of r] by auto
+ using assms embed_Field[of "Restr r A" r id] id_def
+ Well_order_Restr[of r] by auto
{fix a assume "a \<in> A"
- hence "a \<in> Field(Restr r A)" using * assms
- by (simp add: order_on_defs Refl_Field_Restr2)
- hence "bij_betw id (under (Restr r A) a) (under r a)"
- using * unfolding embed_def by auto
- hence "under r a \<le> under (Restr r A) a"
- unfolding bij_betw_def by auto
- also have "\<dots> \<le> Field(Restr r A)" by (simp add: under_Field)
- also have "\<dots> \<le> A" by (simp add: Field_Restr_subset)
- finally have "under r a \<le> A" .
+ hence "a \<in> Field(Restr r A)" using * assms
+ by (simp add: order_on_defs Refl_Field_Restr2)
+ hence "bij_betw id (under (Restr r A) a) (under r a)"
+ using * unfolding embed_def by auto
+ hence "under r a \<le> under (Restr r A) a"
+ unfolding bij_betw_def by auto
+ also have "\<dots> \<le> Field(Restr r A)" by (simp add: under_Field)
+ also have "\<dots> \<le> A" by (simp add: Field_Restr_subset)
+ finally have "under r a \<le> A" .
}
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)"
+ assumes WELL: "Well_order r" and OFA: "wo_rel.ofilter r A"
+ shows "wo_rel.ofilter (Restr r B) (A Int B)"
proof-
let ?rB = "Restr r B"
have Well: "wo_rel r" unfolding wo_rel_def using WELL .
hence Refl: "Refl r" by (simp add: wo_rel.REFL)
hence Field: "Field ?rB = Field r Int B"
- using Refl_Field_Restr by blast
+ using Refl_Field_Restr by blast
have WellB: "wo_rel ?rB \<and> Well_order ?rB" using WELL
- by (simp add: Well_order_Restr wo_rel_def)
- (* Main proof *)
+ by (simp add: Well_order_Restr wo_rel_def)
+ (* Main proof *)
show ?thesis using WellB assms
unfolding wo_rel.ofilter_def under_def ofilter_def
proof safe
@@ -183,84 +178,84 @@
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"
+ 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"
proof-
have "A Int B = A" using SUB by blast
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"
-shows "(A \<le> B) = (embed (Restr r A) (Restr r B) id)"
+ assumes WELL: "Well_order r" and
+ OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B"
+ shows "(A \<le> B) = (embed (Restr r A) (Restr r B) id)"
proof-
let ?rA = "Restr r A" let ?rB = "Restr r B"
have Well: "wo_rel r" unfolding wo_rel_def using WELL .
hence Refl: "Refl r" by (simp add: wo_rel.REFL)
hence FieldA: "Field ?rA = Field r Int A"
- using Refl_Field_Restr by blast
+ using Refl_Field_Restr by blast
have FieldB: "Field ?rB = Field r Int B"
- using Refl Refl_Field_Restr by blast
+ using Refl Refl_Field_Restr by blast
have WellA: "wo_rel ?rA \<and> Well_order ?rA" using WELL
- by (simp add: Well_order_Restr wo_rel_def)
+ by (simp add: Well_order_Restr wo_rel_def)
have WellB: "wo_rel ?rB \<and> Well_order ?rB" using WELL
- by (simp add: Well_order_Restr wo_rel_def)
- (* Main proof *)
+ by (simp add: Well_order_Restr wo_rel_def)
+ (* Main proof *)
show ?thesis
proof
assume *: "A \<le> B"
hence "wo_rel.ofilter (Restr r B) A" using assms
- by (simp add: ofilter_Restr_subset)
+ by (simp add: ofilter_Restr_subset)
hence "embed (Restr ?rB A) (Restr r B) id"
- using WellB ofilter_embed[of "?rB" A] by auto
+ using WellB ofilter_embed[of "?rB" A] by auto
thus "embed (Restr r A) (Restr r B) id"
- using * by (simp add: Restr_subset)
+ using * by (simp add: Restr_subset)
next
assume *: "embed (Restr r A) (Restr r B) id"
{fix a assume **: "a \<in> A"
- hence "a \<in> Field r" using Well OFA by (auto simp add: wo_rel.ofilter_def)
- with ** FieldA have "a \<in> Field ?rA" by auto
- hence "a \<in> Field ?rB" using * WellA embed_Field[of ?rA ?rB id] by auto
- hence "a \<in> B" using FieldB by auto
+ hence "a \<in> Field r" using Well OFA by (auto simp add: wo_rel.ofilter_def)
+ with ** FieldA have "a \<in> Field ?rA" by auto
+ hence "a \<in> Field ?rB" using * WellA embed_Field[of ?rA ?rB id] by auto
+ hence "a \<in> B" using FieldB by auto
}
thus "A \<le> B" by blast
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"
-shows "((A < B) = (embedS (Restr r A) (Restr r B) id)) \<and>
+ 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)) \<and>
((A = B) = (iso (Restr r A) (Restr r B) id))"
proof-
let ?rA = "Restr r A" let ?rB = "Restr r B"
have Well: "wo_rel r" unfolding wo_rel_def using WELL .
hence Refl: "Refl r" by (simp add: wo_rel.REFL)
hence "Field ?rA = Field r Int A"
- using Refl_Field_Restr by blast
+ using Refl_Field_Restr by blast
hence FieldA: "Field ?rA = A" using OFA Well
- by (auto simp add: wo_rel.ofilter_def)
+ by (auto simp add: wo_rel.ofilter_def)
have "Field ?rB = Field r Int B"
- using Refl Refl_Field_Restr by blast
+ using Refl Refl_Field_Restr by blast
hence FieldB: "Field ?rB = B" using OFB Well
- by (auto simp add: wo_rel.ofilter_def)
- (* Main proof *)
+ by (auto simp add: wo_rel.ofilter_def)
+ (* Main proof *)
show ?thesis unfolding embedS_def iso_def
- using assms ofilter_subset_embed[of r A B]
- FieldA FieldB bij_betw_id_iff[of A B] by auto
+ using assms ofilter_subset_embed[of r A B]
+ 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)
+ 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"
-shows "iso r' (Restr r (f ` (Field r'))) f"
+ assumes WELL: "Well_order r" and WELL': "Well_order r'" and
+ EMB: "embed r' r f"
+ shows "iso r' (Restr r (f ` (Field r'))) f"
proof-
let ?A' = "Field r'"
let ?r'' = "Restr r (f ` ?A')"
@@ -268,13 +263,13 @@
have 1: "wo_rel.ofilter r (f ` ?A')" using assms embed_Field_ofilter by blast
hence "Field ?r'' = f ` (Field r')" using WELL Field_Restr_ofilter by blast
hence "bij_betw f ?A' (Field ?r'')"
- using EMB embed_inj_on WELL' unfolding bij_betw_def by blast
+ using EMB embed_inj_on WELL' unfolding bij_betw_def by blast
moreover
{have "\<forall>a b. (a,b) \<in> r' \<longrightarrow> a \<in> Field r' \<and> b \<in> Field r'"
- unfolding Field_def by auto
- hence "compat r' ?r'' f"
- using assms embed_iff_compat_inj_on_ofilter
- unfolding compat_def by blast
+ unfolding Field_def by auto
+ hence "compat r' ?r'' f"
+ using assms embed_iff_compat_inj_on_ofilter
+ unfolding compat_def by blast
}
ultimately show ?thesis using WELL' 0 iso_iff3 by blast
qed
@@ -283,13 +278,13 @@
subsection \<open>The strict inclusion on proper ofilters is well-founded\<close>
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>
+ 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)"
+ assumes WELL: "Well_order r"
+ shows "wf(ofilterIncl r)"
proof-
have Well: "wo_rel r" using WELL by (simp add: wo_rel_def)
hence Lo: "Linear_order r" by (simp add: wo_rel.LIN)
@@ -299,23 +294,23 @@
moreover
have "compat (ofilterIncl r) ?rS ?h"
proof(unfold compat_def ofilterIncl_def,
- intro allI impI, simp, elim conjE)
+ intro allI impI, simp, elim conjE)
fix A B
assume *: "wo_rel.ofilter r A" "A \<noteq> Field r" and
- **: "wo_rel.ofilter r B" "B \<noteq> Field r" and ***: "A < B"
+ **: "wo_rel.ofilter r B" "B \<noteq> Field r" and ***: "A < B"
then obtain a and b where 0: "a \<in> Field r \<and> b \<in> Field r" and
- 1: "A = underS r a \<and> B = underS r b"
- using Well by (auto simp add: wo_rel.ofilter_underS_Field)
+ 1: "A = underS r a \<and> B = underS r b"
+ using Well by (auto simp add: wo_rel.ofilter_underS_Field)
hence "a \<noteq> b" using *** by auto
moreover
have "(a,b) \<in> r" using 0 1 Lo ***
- by (auto simp add: underS_incl_iff)
+ by (auto simp add: underS_incl_iff)
moreover
have "a = wo_rel.suc r A \<and> b = wo_rel.suc r B"
- using Well 0 1 by (simp add: wo_rel.suc_underS)
+ using Well 0 1 by (simp add: wo_rel.suc_underS)
ultimately
show "(wo_rel.suc r A, wo_rel.suc r B) \<in> r \<and> wo_rel.suc r A \<noteq> wo_rel.suc r B"
- by simp
+ by simp
qed
ultimately show "wf (ofilterIncl r)" by (simp add: compat_wf)
qed
@@ -336,35 +331,35 @@
\<close>
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)}"
+ 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"
+ 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'"
+ 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)}"
+ where
+ "ordLess = {(r,r'). Well_order r \<and> Well_order r' \<and> (\<exists>f. embedS r r' f)}"
abbreviation ordLess2 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "<o" 50)
-where "r <o r' \<equiv> (r,r') \<in> ordLess"
+ 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)}"
+ where
+ "ordIso = {(r,r'). Well_order r \<and> Well_order r' \<and> (\<exists>f. iso r r' f)}"
abbreviation ordIso2 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "=o" 50)
-where "r =o r' \<equiv> (r,r') \<in> ordIso"
+ where "r =o r' \<equiv> (r,r') \<in> ordIso"
lemmas ordRels_def = ordLeq_def ordLess_def ordIso_def
lemma ordLeq_Well_order_simp:
-assumes "r \<le>o r'"
-shows "Well_order r \<and> Well_order r'"
-using assms unfolding ordLeq_def by simp
+ assumes "r \<le>o r'"
+ shows "Well_order r \<and> Well_order r'"
+ using assms unfolding ordLeq_def by simp
text\<open>Notice that the relations \<open>\<le>o\<close>, \<open><o\<close>, \<open>=o\<close> connect well-orders
on potentially {\em distinct} types. However, some of the lemmas below, including the next one,
@@ -372,360 +367,313 @@
to \<open>'a rel rel\<close>.\<close>
lemma ordLeq_reflexive:
-"Well_order r \<Longrightarrow> r \<le>o r"
-unfolding ordLeq_def using id_embed[of r] by blast
+ "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''"
-proof-
- obtain f and f'
- where 1: "Well_order r \<and> Well_order r' \<and> Well_order r''" and
- "embed r r' f" and "embed r' r'' f'"
- using * ** unfolding ordLeq_def by blast
- hence "embed r r'' (f' \<circ> f)"
- using comp_embed[of r r' f r'' f'] by auto
- thus "r \<le>o r''" unfolding ordLeq_def using 1 by auto
-qed
+ assumes "r \<le>o r'" and "r' \<le>o r''"
+ shows "r \<le>o r''"
+ using assms by (auto simp: ordLeq_def intro: comp_embed)
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
+ "\<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
+ "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''"
-proof-
- obtain f and f'
- where 1: "Well_order r \<and> Well_order r' \<and> Well_order r''" and
- "iso r r' f" and 3: "iso r' r'' f'"
- using * ** unfolding ordIso_def by auto
- hence "iso r r'' (f' \<circ> f)"
- using comp_iso[of r r' f r'' f'] by auto
- thus "r =o r''" unfolding ordIso_def using 1 by auto
-qed
+ assumes *: "r =o r'" and **: "r' =o r''"
+ shows "r =o r''"
+ using assms by (auto simp: ordIso_def intro: comp_iso)
lemma ordIso_symmetric:
-assumes *: "r =o r'"
-shows "r' =o r"
+ assumes *: "r =o r'"
+ shows "r' =o r"
proof-
obtain f where 1: "Well_order r \<and> Well_order r'" and
- 2: "embed r r' f \<and> bij_betw f (Field r) (Field r')"
- using * by (auto simp add: ordIso_def iso_def)
+ 2: "embed r r' f \<and> bij_betw f (Field r) (Field r')"
+ using * by (auto simp add: ordIso_def iso_def)
let ?f' = "inv_into (Field r) f"
have "embed r' r ?f' \<and> bij_betw ?f' (Field r') (Field r)"
- using 1 2 by (simp add: bij_betw_inv_into inv_into_Field_embed_bij_betw)
+ using 1 2 by (simp add: bij_betw_inv_into inv_into_Field_embed_bij_betw)
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''"
+ assumes "r \<le>o r'" and " r' <o r''"
+ shows "r <o r''"
proof-
have "Well_order r \<and> Well_order r''"
- using assms unfolding ordLeq_def ordLess_def by auto
+ using assms unfolding ordLeq_def ordLess_def by auto
thus ?thesis using assms unfolding ordLeq_def ordLess_def
- using embed_comp_embedS by blast
+ 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''"
-proof-
- have "Well_order r \<and> Well_order r''"
- using assms unfolding ordLeq_def ordLess_def by auto
- thus ?thesis using assms unfolding ordLeq_def ordLess_def
- using embedS_comp_embed by blast
-qed
+ assumes "r <o r'" and " r' \<le>o r''"
+ shows "r <o r''"
+ using embedS_comp_embed assms by (force simp: ordLeq_def ordLess_def)
lemma ordLeq_ordIso_trans[trans]:
-assumes "r \<le>o r'" and " r' =o r''"
-shows "r \<le>o r''"
-proof-
- have "Well_order r \<and> Well_order r''"
- using assms unfolding ordLeq_def ordIso_def by auto
- thus ?thesis using assms unfolding ordLeq_def ordIso_def
- using embed_comp_iso by blast
-qed
+ assumes "r \<le>o r'" and " r' =o r''"
+ shows "r \<le>o r''"
+ using embed_comp_iso assms by (force simp: ordLeq_def ordIso_def)
lemma ordIso_ordLeq_trans[trans]:
-assumes "r =o r'" and " r' \<le>o r''"
-shows "r \<le>o r''"
-proof-
- have "Well_order r \<and> Well_order r''"
- using assms unfolding ordLeq_def ordIso_def by auto
- thus ?thesis using assms unfolding ordLeq_def ordIso_def
- using iso_comp_embed by blast
-qed
+ assumes "r =o r'" and " r' \<le>o r''"
+ shows "r \<le>o r''"
+ using iso_comp_embed assms by (force simp: ordLeq_def ordIso_def)
lemma ordLess_ordIso_trans[trans]:
-assumes "r <o r'" and " r' =o r''"
-shows "r <o r''"
-proof-
- have "Well_order r \<and> Well_order r''"
- using assms unfolding ordLess_def ordIso_def by auto
- thus ?thesis using assms unfolding ordLess_def ordIso_def
- using embedS_comp_iso by blast
-qed
+ assumes "r <o r'" and " r' =o r''"
+ shows "r <o r''"
+ using embedS_comp_iso assms by (force simp: ordLess_def ordIso_def)
lemma ordIso_ordLess_trans[trans]:
-assumes "r =o r'" and " r' <o r''"
-shows "r <o r''"
-proof-
- have "Well_order r \<and> Well_order r''"
- using assms unfolding ordLess_def ordIso_def by auto
- thus ?thesis using assms unfolding ordLess_def ordIso_def
- using iso_comp_embedS by blast
-qed
+ assumes "r =o r'" and " r' <o r''"
+ shows "r <o r''"
+ using iso_comp_embedS assms by (force simp: ordLess_def ordIso_def)
lemma ordLess_not_embed:
-assumes "r <o r'"
-shows "\<not>(\<exists>f'. embed r' r f')"
+ assumes "r <o r'"
+ shows "\<not>(\<exists>f'. embed r' r f')"
proof-
obtain f where 1: "Well_order r \<and> Well_order r'" and 2: "embed r r' f" and
- 3: " \<not> bij_betw f (Field r) (Field r')"
- using assms unfolding ordLess_def by (auto simp add: embedS_def)
+ 3: " \<not> bij_betw f (Field r) (Field r')"
+ using assms unfolding ordLess_def by (auto simp add: embedS_def)
{fix f' assume *: "embed r' r f'"
- hence "bij_betw f (Field r) (Field r')" using 1 2
- by (simp add: embed_bothWays_Field_bij_betw)
- with 3 have False by contradiction
+ hence "bij_betw f (Field r) (Field r')" using 1 2
+ by (simp add: embed_bothWays_Field_bij_betw)
+ with 3 have False by contradiction
}
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)"
+ assumes OL: "r1 <o r2" and EMB: "embed r1 r2 f"
+ shows "\<not> (f`(Field r1) = Field r2)"
proof-
let ?A1 = "Field r1" let ?A2 = "Field r2"
obtain g where
- 0: "Well_order r1 \<and> Well_order r2" and
- 1: "embed r1 r2 g \<and> \<not>(bij_betw g ?A1 ?A2)"
- using OL unfolding ordLess_def by (auto simp add: embedS_def)
+ 0: "Well_order r1 \<and> Well_order r2" and
+ 1: "embed r1 r2 g \<and> \<not>(bij_betw g ?A1 ?A2)"
+ using OL unfolding ordLess_def by (auto simp add: embedS_def)
hence "\<forall>a \<in> ?A1. f a = g a"
- using 0 EMB embed_unique[of r1] by auto
+ using 0 EMB embed_unique[of r1] by auto
hence "\<not>(bij_betw f ?A1 ?A2)"
- using 1 bij_betw_cong[of ?A1] by blast
+ using 1 bij_betw_cong[of ?A1] by blast
moreover
have "inj_on f ?A1" using EMB 0 by (simp add: embed_inj_on)
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'))"
+ "r <o r' = (Well_order r \<and> Well_order r' \<and> \<not>(\<exists>f'. embed r' r f'))"
proof
assume *: "r <o r'"
hence "\<not>(\<exists>f'. embed r' r f')" using ordLess_not_embed[of r r'] by simp
with * show "Well_order r \<and> Well_order r' \<and> \<not> (\<exists>f'. embed r' r f')"
- unfolding ordLess_def by auto
+ unfolding ordLess_def by auto
next
assume *: "Well_order r \<and> Well_order r' \<and> \<not> (\<exists>f'. embed r' r f')"
then obtain f where 1: "embed r r' f"
- using wellorders_totally_ordered[of r r'] by blast
+ using wellorders_totally_ordered[of r r'] by blast
moreover
{assume "bij_betw f (Field r) (Field r')"
- with * 1 have "embed r' r (inv_into (Field r) f) "
- using inv_into_Field_embed_bij_betw[of r r' f] by auto
- with * have False by blast
+ with * 1 have "embed r' r (inv_into (Field r) f) "
+ using inv_into_Field_embed_bij_betw[of r r' f] by auto
+ with * have False by blast
}
ultimately show "(r,r') \<in> ordLess"
- unfolding ordLess_def using * by (fastforce simp add: embedS_def)
+ unfolding ordLess_def using * by (fastforce simp add: embedS_def)
qed
lemma ordLess_irreflexive: "\<not> r <o r"
-proof
- assume "r <o r"
- hence "Well_order r \<and> \<not>(\<exists>f. embed r r f)"
- unfolding ordLess_iff ..
- moreover have "embed r r id" using id_embed[of r] .
- ultimately show False by blast
-qed
+ using id_embed[of r] by (auto simp: ordLess_iff)
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
+ "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)"
+ "(r =o r') = (r \<le>o r' \<and> r' \<le>o r)"
proof
assume "r =o r'"
then obtain f where 1: "Well_order r \<and> Well_order r' \<and>
embed r r' f \<and> bij_betw f (Field r) (Field r')"
- unfolding ordIso_def iso_defs by auto
+ unfolding ordIso_def iso_defs by auto
hence "embed r r' f \<and> embed r' r (inv_into (Field r) f)"
- by (simp add: inv_into_Field_embed_bij_betw)
+ by (simp add: inv_into_Field_embed_bij_betw)
thus "r \<le>o r' \<and> r' \<le>o r"
- unfolding ordLeq_def using 1 by auto
+ unfolding ordLeq_def using 1 by auto
next
assume "r \<le>o r' \<and> r' \<le>o r"
then obtain f and g where 1: "Well_order r \<and> Well_order r' \<and>
embed r r' f \<and> embed r' r g"
- unfolding ordLeq_def by auto
+ unfolding ordLeq_def by auto
hence "iso r r' f" by (auto simp add: embed_bothWays_iso)
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
+ "r <o r' \<Longrightarrow> \<not> r' \<le>o r"
+ using ordLess_ordLeq_trans ordLess_irreflexive by blast
lemma not_ordLeq_ordLess:
-"r \<le>o r' \<Longrightarrow> \<not> r' <o r"
-using not_ordLess_ordLeq by blast
+ "r \<le>o r' \<Longrightarrow> \<not> r' <o r"
+ using not_ordLess_ordLeq 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"
+ assumes WELL: "Well_order r" and WELL': "Well_order r'"
+ shows "r <o r' \<or> r' \<le>o r"
proof-
have "r \<le>o r' \<or> r' \<le>o r"
- using assms by (simp add: ordLeq_total)
+ using assms by (simp add: ordLeq_total)
moreover
{assume "\<not> r <o r' \<and> r \<le>o r'"
- hence "r =o r'" using ordLeq_iff_ordLess_or_ordIso by blast
- hence "r' \<le>o r" using ordIso_symmetric ordIso_iff_ordLeq by blast
+ hence "r =o r'" using ordLeq_iff_ordLess_or_ordIso by blast
+ hence "r' \<le>o r" using ordIso_symmetric ordIso_iff_ordLeq by blast
}
ultimately show ?thesis by blast
qed
lemma not_ordLess_ordIso:
-"r <o r' \<Longrightarrow> \<not> r =o r'"
-using ordLess_ordIso_trans ordIso_symmetric ordLess_irreflexive by blast
+ "r <o r' \<Longrightarrow> \<not> r =o r'"
+ using 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
+ 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
+ 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 ordLess_ordLeq_trans ordLeq_iff_ordLess_or_ordIso by blast
+ "\<lbrakk>r <o r'; r' <o r''\<rbrakk> \<Longrightarrow> r <o r''"
+ using ordLess_ordLeq_trans ordLeq_iff_ordLess_or_ordIso by blast
corollary ordLess_trans: "trans ordLess"
-unfolding trans_def using ordLess_transitive by blast
+ 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
+ "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
+ "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"
-shows "(A \<le> B) = (Restr r A \<le>o Restr r B)"
+ assumes WELL: "Well_order r" and
+ OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B"
+ shows "(A \<le> B) = (Restr r A \<le>o Restr r B)"
proof
assume "A \<le> B"
thus "Restr r A \<le>o Restr r B"
- unfolding ordLeq_def using assms
- Well_order_Restr Well_order_Restr ofilter_subset_embed by blast
+ unfolding ordLeq_def using assms
+ Well_order_Restr Well_order_Restr ofilter_subset_embed by blast
next
assume *: "Restr r A \<le>o Restr r B"
then obtain f where "embed (Restr r A) (Restr r B) f"
- unfolding ordLeq_def by blast
+ unfolding ordLeq_def by blast
{assume "B < A"
- hence "Restr r B <o Restr r A"
- unfolding ordLess_def using assms
- Well_order_Restr Well_order_Restr ofilter_subset_embedS by blast
- hence False using * not_ordLess_ordLeq by blast
+ hence "Restr r B <o Restr r A"
+ unfolding ordLess_def using assms
+ Well_order_Restr Well_order_Restr ofilter_subset_embedS by blast
+ hence False using * not_ordLess_ordLeq by blast
}
thus "A \<le> B" using OFA OFB WELL
- wo_rel_def[of r] wo_rel.ofilter_linord[of r A B] by blast
+ 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"
-shows "(A < B) = (Restr r A <o Restr r B)"
+ assumes WELL: "Well_order r" and
+ OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B"
+ shows "(A < B) = (Restr r A <o Restr r B)"
proof-
let ?rA = "Restr r A" let ?rB = "Restr r B"
have 1: "Well_order ?rA \<and> Well_order ?rB"
- using WELL Well_order_Restr by blast
+ using WELL Well_order_Restr by blast
have "(A < B) = (\<not> B \<le> A)" using assms
- wo_rel_def wo_rel.ofilter_linord[of r A B] by blast
+ wo_rel_def wo_rel.ofilter_linord[of r A B] by blast
also have "\<dots> = (\<not> Restr r B \<le>o Restr r A)"
- using assms ofilter_subset_ordLeq by blast
+ using assms ofilter_subset_ordLeq by blast
also have "\<dots> = (Restr r A <o Restr r B)"
- using 1 not_ordLeq_iff_ordLess by blast
+ using 1 not_ordLeq_iff_ordLess by blast
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)
+ "\<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"
+ assumes "Well_order r" and "Field r \<noteq> {}"
+ shows "Restr r (underS r a) <o r"
proof-
have "underS r a < Field r" using assms
- by (simp add: underS_Field3)
+ by (simp add: underS_Field3)
thus ?thesis using assms
- by (simp add: ofilter_ordLess wo_rel.underS_ofilter wo_rel_def)
+ 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
- EMB13: "embed r1 r3 f13" and EMB23: "embed r2 r3 f23"
-shows "(f13`(Field r1), f23`(Field r2)) \<in> (ofilterIncl r3)"
+ assumes
+ OL12: "r1 <o r2" and OL23: "r2 <o r3" and
+ EMB13: "embed r1 r3 f13" and EMB23: "embed r2 r3 f23"
+ shows "(f13`(Field r1), f23`(Field r2)) \<in> (ofilterIncl r3)"
proof-
have OL13: "r1 <o r3"
- using OL12 OL23 using ordLess_transitive by auto
+ using OL12 OL23 using ordLess_transitive by auto
let ?A1 = "Field r1" let ?A2 ="Field r2" let ?A3 ="Field r3"
obtain f12 g23 where
- 0: "Well_order r1 \<and> Well_order r2 \<and> Well_order r3" and
- 1: "embed r1 r2 f12 \<and> \<not>(bij_betw f12 ?A1 ?A2)" and
- 2: "embed r2 r3 g23 \<and> \<not>(bij_betw g23 ?A2 ?A3)"
- using OL12 OL23 by (auto simp add: ordLess_def embedS_def)
+ 0: "Well_order r1 \<and> Well_order r2 \<and> Well_order r3" and
+ 1: "embed r1 r2 f12 \<and> \<not>(bij_betw f12 ?A1 ?A2)" and
+ 2: "embed r2 r3 g23 \<and> \<not>(bij_betw g23 ?A2 ?A3)"
+ using OL12 OL23 by (auto simp add: ordLess_def embedS_def)
hence "\<forall>a \<in> ?A2. f23 a = g23 a"
- using EMB23 embed_unique[of r2 r3] by blast
+ using EMB23 embed_unique[of r2 r3] by blast
hence 3: "\<not>(bij_betw f23 ?A2 ?A3)"
- using 2 bij_betw_cong[of ?A2 f23 g23] by blast
- (* *)
+ using 2 bij_betw_cong[of ?A2 f23 g23] by blast
+ (* *)
have 4: "wo_rel.ofilter r2 (f12 ` ?A1) \<and> f12 ` ?A1 \<noteq> ?A2"
- using 0 1 OL12 by (simp add: embed_Field_ofilter ordLess_Field)
+ using 0 1 OL12 by (simp add: embed_Field_ofilter ordLess_Field)
have 5: "wo_rel.ofilter r3 (f23 ` ?A2) \<and> f23 ` ?A2 \<noteq> ?A3"
- using 0 EMB23 OL23 by (simp add: embed_Field_ofilter ordLess_Field)
+ using 0 EMB23 OL23 by (simp add: embed_Field_ofilter ordLess_Field)
have 6: "wo_rel.ofilter r3 (f13 ` ?A1) \<and> f13 ` ?A1 \<noteq> ?A3"
- using 0 EMB13 OL13 by (simp add: embed_Field_ofilter ordLess_Field)
- (* *)
+ using 0 EMB13 OL13 by (simp add: embed_Field_ofilter ordLess_Field)
+ (* *)
have "f12 ` ?A1 < ?A2"
- using 0 4 by (auto simp add: wo_rel_def wo_rel.ofilter_def)
+ using 0 4 by (auto simp add: wo_rel_def wo_rel.ofilter_def)
moreover have "inj_on f23 ?A2"
- using EMB23 0 by (simp add: wo_rel_def embed_inj_on)
+ using EMB23 0 by (simp add: wo_rel_def embed_inj_on)
ultimately
have "f23 ` (f12 ` ?A1) < f23 ` ?A2" by (simp add: image_strict_mono)
moreover
{have "embed r1 r3 (f23 \<circ> f12)"
- using 1 EMB23 0 by (auto simp add: comp_embed)
- hence "\<forall>a \<in> ?A1. f23(f12 a) = f13 a"
- using EMB13 0 embed_unique[of r1 r3 "f23 \<circ> f12" f13] by auto
- hence "f23 ` (f12 ` ?A1) = f13 ` ?A1" by force
+ using 1 EMB23 0 by (auto simp add: comp_embed)
+ hence "\<forall>a \<in> ?A1. f23(f12 a) = f13 a"
+ using EMB13 0 embed_unique[of r1 r3 "f23 \<circ> f12" f13] by auto
+ hence "f23 ` (f12 ` ?A1) = f13 ` ?A1" by force
}
ultimately
have "f13 ` ?A1 < f23 ` ?A2" by simp
- (* *)
+ (* *)
with 5 6 show ?thesis
- unfolding ofilterIncl_def by auto
+ 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))"
+ 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))"
proof safe
fix a assume *: "a \<in> Field r" and **: "r' =o Restr r (underS r a)"
hence "Restr r (underS r a) <o r" using WELL underS_Restr_ordLess[of r] by blast
@@ -733,112 +681,107 @@
next
assume "r' <o r"
then obtain f where 1: "Well_order r \<and> Well_order r'" and
- 2: "embed r' r f \<and> f ` (Field r') \<noteq> Field r"
- unfolding ordLess_def embedS_def[abs_def] bij_betw_def using embed_inj_on by blast
+ 2: "embed r' r f \<and> f ` (Field r') \<noteq> Field r"
+ unfolding ordLess_def embedS_def[abs_def] bij_betw_def using embed_inj_on by blast
hence "wo_rel.ofilter r (f ` (Field r'))" using embed_Field_ofilter by blast
then obtain a where 3: "a \<in> Field r" and 4: "underS r a = f ` (Field r')"
- using 1 2 by (auto simp add: wo_rel.ofilter_underS_Field wo_rel_def)
+ using 1 2 by (auto simp add: wo_rel.ofilter_underS_Field wo_rel_def)
have "iso r' (Restr r (f ` (Field r'))) f"
- using embed_implies_iso_Restr 2 assms by blast
+ using embed_implies_iso_Restr 2 assms by blast
moreover have "Well_order (Restr r (f ` (Field r')))"
- using WELL Well_order_Restr by blast
+ using WELL Well_order_Restr by blast
ultimately have "r' =o Restr r (f ` (Field r'))"
- using WELL' unfolding ordIso_def by auto
+ using WELL' unfolding ordIso_def by auto
hence "r' =o Restr r (underS r a)" using 4 by auto
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)"
+ "(r' <o r) = (\<exists>p. Field p < Field r \<and> r' =o p \<and> p <o r)"
proof
assume *: "r' <o r"
hence 0: "Well_order r \<and> Well_order r'" unfolding ordLess_def by auto
with * obtain a where 1: "a \<in> Field r" and 2: "r' =o Restr r (underS r a)"
- using ordLess_iff_ordIso_Restr by blast
+ using ordLess_iff_ordIso_Restr by blast
let ?p = "Restr r (underS r a)"
have "wo_rel.ofilter r (underS r a)" using 0
- by (simp add: wo_rel_def wo_rel.underS_ofilter)
+ by (simp add: wo_rel_def wo_rel.underS_ofilter)
hence "Field ?p = underS r a" using 0 Field_Restr_ofilter by blast
hence "Field ?p < Field r" using underS_Field2 1 by fast
moreover have "?p <o r" using underS_Restr_ordLess[of r a] 0 1 by blast
- ultimately
- show "\<exists>p. Field p < Field r \<and> r' =o p \<and> p <o r" using 2 by blast
+ ultimately show "\<exists>p. Field p < Field r \<and> r' =o p \<and> p <o r" using 2 by blast
next
assume "\<exists>p. Field p < Field r \<and> r' =o p \<and> p <o r"
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)"
+ "(r' \<le>o r) = (\<exists>p. Field p \<le> Field r \<and> r' =o p \<and> p \<le>o r)"
proof
assume *: "r' \<le>o r"
moreover
- {assume "r' <o r"
- then obtain p where "Field p < Field r \<and> r' =o p \<and> p <o r"
- using internalize_ordLess[of r' r] by blast
- hence "\<exists>p. Field p \<le> Field r \<and> r' =o p \<and> p \<le>o r"
- using ordLeq_iff_ordLess_or_ordIso by blast
- }
+ have "r' <o r \<Longrightarrow> \<exists>p. Field p \<le> Field r \<and> r' =o p \<and> p \<le>o r"
+ using ordLeq_iff_ordLess_or_ordIso internalize_ordLess[of r' r] by blast
moreover
have "r \<le>o r" using * ordLeq_def ordLeq_reflexive by blast
ultimately show "\<exists>p. Field p \<le> Field r \<and> r' =o p \<and> p \<le>o r"
- using ordLeq_iff_ordLess_or_ordIso by blast
+ using ordLeq_iff_ordLess_or_ordIso by blast
next
assume "\<exists>p. Field p \<le> Field r \<and> r' =o p \<and> p \<le>o r"
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')"
+ 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')"
proof safe
assume *: "r \<le>o r'"
fix a assume "a \<in> Field r"
hence "Restr r (underS r a) <o r"
- using WELL underS_Restr_ordLess[of r] by blast
+ using WELL underS_Restr_ordLess[of r] by blast
thus "Restr r (underS r a) <o r'"
- using * ordLess_ordLeq_trans by blast
+ using * ordLess_ordLeq_trans by blast
next
assume *: "\<forall>a \<in> Field r. Restr r (underS r a) <o r'"
{assume "r' <o r"
- then obtain a where "a \<in> Field r \<and> r' =o Restr r (underS r a)"
- using assms ordLess_iff_ordIso_Restr by blast
- hence False using * not_ordLess_ordIso ordIso_symmetric by blast
+ then obtain a where "a \<in> Field r \<and> r' =o Restr r (underS r a)"
+ using assms ordLess_iff_ordIso_Restr by blast
+ hence False using * not_ordLess_ordIso ordIso_symmetric by blast
}
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')"
-shows "r <o r'"
+ assumes WELL: "Well_order r" and WELL': "Well_order r'" and
+ FIN: "finite(Field r)" and INF: "\<not>finite(Field r')"
+ shows "r <o r'"
proof-
{assume "r' \<le>o r"
- then obtain h where "inj_on h (Field r') \<and> h ` (Field r') \<le> Field r"
- unfolding ordLeq_def using assms embed_inj_on embed_Field by blast
- hence False using finite_imageD finite_subset FIN INF by blast
+ then obtain h where "inj_on h (Field r') \<and> h ` (Field r') \<le> Field r"
+ unfolding ordLeq_def using assms embed_inj_on embed_Field by blast
+ hence False using finite_imageD finite_subset FIN INF by blast
}
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'"
-shows "r =o r'"
+ assumes FIN: "finite A" and
+ WELL: "well_order_on A r" and WELL': "well_order_on A r'"
+ shows "r =o r'"
proof-
have 0: "Well_order r \<and> Well_order r' \<and> Field r = A \<and> Field r' = A"
- using assms well_order_on_Well_order by blast
+ using assms well_order_on_Well_order by blast
moreover
have "\<forall>r r'. well_order_on A r \<and> well_order_on A r' \<and> r \<le>o r'
\<longrightarrow> r =o r'"
proof(clarify)
fix r r' assume *: "well_order_on A r" and **: "well_order_on A r'"
have 2: "Well_order r \<and> Well_order r' \<and> Field r = A \<and> Field r' = A"
- using * ** well_order_on_Well_order by blast
+ using * ** well_order_on_Well_order by blast
assume "r \<le>o r'"
then obtain f where 1: "embed r r' f" and
- "inj_on f A \<and> f ` A \<le> A"
- unfolding ordLeq_def using 2 embed_inj_on embed_Field by blast
+ "inj_on f A \<and> f ` A \<le> A"
+ unfolding ordLeq_def using 2 embed_inj_on embed_Field by blast
hence "bij_betw f A A" unfolding bij_betw_def using FIN endo_inj_surj by blast
thus "r =o r'" unfolding ordIso_def iso_def[abs_def] using 1 2 by auto
qed
@@ -854,10 +797,10 @@
{\em strict inclusion}; and we already know that strict inclusion of order filters is well-founded.\<close>
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)"
+ where "ord_to_filter r0 r \<equiv> (SOME f. embed r r0 f) ` (Field r)"
lemma ord_to_filter_compat:
-"compat (ordLess Int (ordLess\<inverse>``{r0} \<times> ordLess\<inverse>``{r0}))
+ "compat (ordLess Int (ordLess\<inverse>``{r0} \<times> ordLess\<inverse>``{r0}))
(ofilterIncl r0)
(ord_to_filter r0)"
proof(unfold compat_def ord_to_filter_def, clarify)
@@ -867,41 +810,41 @@
let ?phi20 = "\<lambda> f20. embed r2 r0 f20" let ?f20 = "SOME f. ?phi20 f"
assume *: "r1 <o r0" "r2 <o r0" and **: "r1 <o r2"
hence "(\<exists>f. ?phi10 f) \<and> (\<exists>f. ?phi20 f)"
- by (auto simp add: ordLess_def embedS_def)
+ by (auto simp add: ordLess_def embedS_def)
hence "?phi10 ?f10 \<and> ?phi20 ?f20" by (auto simp add: someI_ex)
thus "(?f10 ` ?A1, ?f20 ` ?A2) \<in> ofilterIncl r0"
- using * ** by (simp add: embed_ordLess_ofilterIncl)
+ using * ** by (simp add: embed_ordLess_ofilterIncl)
qed
theorem wf_ordLess: "wf ordLess"
proof-
{fix r0 :: "('a \<times> 'a) set"
- (* need to annotate here!*)
- let ?ordLess = "ordLess::('d rel * 'd rel) set"
- let ?R = "?ordLess Int (?ordLess\<inverse>``{r0} \<times> ?ordLess\<inverse>``{r0})"
- {assume Case1: "Well_order r0"
- hence "wf ?R"
- using wf_ofilterIncl[of r0]
+ (* need to annotate here!*)
+ let ?ordLess = "ordLess::('d rel * 'd rel) set"
+ let ?R = "?ordLess Int (?ordLess\<inverse>``{r0} \<times> ?ordLess\<inverse>``{r0})"
+ {assume Case1: "Well_order r0"
+ hence "wf ?R"
+ using wf_ofilterIncl[of r0]
compat_wf[of ?R "ofilterIncl r0" "ord_to_filter r0"]
ord_to_filter_compat[of r0] by auto
- }
- moreover
- {assume Case2: "\<not> Well_order r0"
- hence "?R = {}" unfolding ordLess_def by auto
- hence "wf ?R" using wf_empty by simp
- }
- ultimately have "wf ?R" by blast
+ }
+ moreover
+ {assume Case2: "\<not> Well_order r0"
+ hence "?R = {}" unfolding ordLess_def by auto
+ hence "wf ?R" using wf_empty by simp
+ }
+ ultimately have "wf ?R" by blast
}
thus ?thesis by (simp add: trans_wf_iff ordLess_trans)
qed
corollary exists_minim_Well_order:
-assumes NE: "R \<noteq> {}" and WELL: "\<forall>r \<in> R. Well_order r"
-shows "\<exists>r \<in> R. \<forall>r' \<in> R. r \<le>o r'"
+ assumes NE: "R \<noteq> {}" and WELL: "\<forall>r \<in> R. Well_order r"
+ shows "\<exists>r \<in> R. \<forall>r' \<in> R. r \<le>o r'"
proof-
obtain r where "r \<in> R \<and> (\<forall>r' \<in> R. \<not> r' <o r)"
- using NE spec[OF spec[OF subst[OF wf_eq_minimal, of "%x. x", OF wf_ordLess]], of _ R]
- equals0I[of R] by blast
+ using NE spec[OF spec[OF subst[OF wf_eq_minimal, of "%x. x", OF wf_ordLess]], of _ R]
+ equals0I[of R] by blast
with not_ordLeq_iff_ordLess WELL show ?thesis by blast
qed
@@ -913,79 +856,79 @@
different types.\<close>
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}"
+ where
+ "dir_image r f = {(f a, f b)| a b. (a,b) \<in> r}"
lemma dir_image_Field:
-"Field(dir_image r f) = f ` (Field r)"
-unfolding dir_image_def Field_def Range_def Domain_def by fast
+ "Field(dir_image r f) = f ` (Field r)"
+ unfolding dir_image_def Field_def Range_def Domain_def by fast
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
+ "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)"
+ assumes "Refl r"
+ shows "Refl(dir_image r f)"
proof-
{fix a' b'
- assume "(a',b') \<in> dir_image r f"
- then obtain a b where 1: "a' = f a \<and> b' = f b \<and> (a,b) \<in> r"
- unfolding dir_image_def by blast
- hence "a \<in> Field r \<and> b \<in> Field r" using Field_def by fastforce
- hence "(a,a) \<in> r \<and> (b,b) \<in> r" using assms by (simp add: refl_on_def)
- with 1 have "(a',a') \<in> dir_image r f \<and> (b',b') \<in> dir_image r f"
- unfolding dir_image_def by auto
+ assume "(a',b') \<in> dir_image r f"
+ then obtain a b where 1: "a' = f a \<and> b' = f b \<and> (a,b) \<in> r"
+ unfolding dir_image_def by blast
+ hence "a \<in> Field r \<and> b \<in> Field r" using Field_def by fastforce
+ hence "(a,a) \<in> r \<and> (b,b) \<in> r" using assms by (simp add: refl_on_def)
+ with 1 have "(a',a') \<in> dir_image r f \<and> (b',b') \<in> dir_image r f"
+ unfolding dir_image_def by auto
}
thus ?thesis
- by(unfold refl_on_def Field_def Domain_def Range_def, auto)
+ 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)"
-unfolding trans_def
+ assumes TRANS: "trans r" and INJ: "inj_on f (Field r)"
+ shows "trans(dir_image r f)"
+ unfolding trans_def
proof safe
fix a' b' c'
assume "(a',b') \<in> dir_image r f" "(b',c') \<in> dir_image r f"
then obtain a b1 b2 c where 1: "a' = f a \<and> b' = f b1 \<and> b' = f b2 \<and> c' = f c" and
- 2: "(a,b1) \<in> r \<and> (b2,c) \<in> r"
- unfolding dir_image_def by blast
+ 2: "(a,b1) \<in> r \<and> (b2,c) \<in> r"
+ unfolding dir_image_def by blast
hence "b1 \<in> Field r \<and> b2 \<in> Field r"
- unfolding Field_def by auto
+ unfolding Field_def by auto
hence "b1 = b2" using 1 INJ unfolding inj_on_def by auto
hence "(a,c) \<in> r" using 2 TRANS unfolding trans_def by blast
thus "(a',c') \<in> dir_image r f"
- unfolding dir_image_def using 1 by auto
+ 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)
+ "\<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)"
-unfolding antisym_def
+ assumes AN: "antisym r" and INJ: "inj_on f (Field r)"
+ shows "antisym(dir_image r f)"
+ unfolding antisym_def
proof safe
fix a' b'
assume "(a',b') \<in> dir_image r f" "(b',a') \<in> dir_image r f"
then obtain a1 b1 a2 b2 where 1: "a' = f a1 \<and> a' = f a2 \<and> b' = f b1 \<and> b' = f b2" and
- 2: "(a1,b1) \<in> r \<and> (b2,a2) \<in> r " and
- 3: "{a1,a2,b1,b2} \<le> Field r"
- unfolding dir_image_def Field_def by blast
+ 2: "(a1,b1) \<in> r \<and> (b2,a2) \<in> r " and
+ 3: "{a1,a2,b1,b2} \<le> Field r"
+ unfolding dir_image_def Field_def by blast
hence "a1 = a2 \<and> b1 = b2" using INJ unfolding inj_on_def by auto
hence "a1 = b2" using 2 AN unfolding antisym_def by auto
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)
+ "\<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)"
+ assumes TOT: "Total r" and INJ: "inj_on f (Field r)"
+ shows "Total(dir_image r f)"
proof(unfold total_on_def, intro ballI impI)
fix a' b'
assume "a' \<in> Field (dir_image r f)" "b' \<in> Field (dir_image r f)"
@@ -995,76 +938,76 @@
ultimately have "a \<noteq> b" using INJ unfolding inj_on_def by auto
hence "(a,b) \<in> r \<or> (b,a) \<in> r" using 1 TOT unfolding total_on_def by auto
thus "(a',b') \<in> dir_image r f \<or> (b',a') \<in> dir_image r f"
- using 1 unfolding dir_image_def by auto
+ 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)
+ "\<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)"
+ assumes WF: "wf r" and INJ: "inj_on f (Field r)"
+ shows "wf(dir_image r f)"
proof(unfold wf_eq_minimal2, intro allI impI, elim conjE)
fix A'::"'b set"
assume SUB: "A' \<le> Field(dir_image r f)" and NE: "A' \<noteq> {}"
obtain A where A_def: "A = {a \<in> Field r. f a \<in> A'}" by blast
have "A \<noteq> {} \<and> A \<le> Field r" using A_def SUB NE by (auto simp: dir_image_Field)
then obtain a where 1: "a \<in> A \<and> (\<forall>b \<in> A. (b,a) \<notin> r)"
- using spec[OF WF[unfolded wf_eq_minimal2], of A] by blast
+ using spec[OF WF[unfolded wf_eq_minimal2], of A] by blast
have "\<forall>b' \<in> A'. (b',f a) \<notin> dir_image r f"
proof(clarify)
fix b' assume *: "b' \<in> A'" and **: "(b',f a) \<in> dir_image r f"
obtain b1 a1 where 2: "b' = f b1 \<and> f a = f a1" and
- 3: "(b1,a1) \<in> r \<and> {a1,b1} \<le> Field r"
- using ** unfolding dir_image_def Field_def by blast
+ 3: "(b1,a1) \<in> r \<and> {a1,b1} \<le> Field r"
+ using ** unfolding dir_image_def Field_def by blast
hence "a = a1" using 1 A_def INJ unfolding inj_on_def by auto
hence "b1 \<in> A \<and> (b1,a) \<in> r" using 2 3 A_def * by auto
with 1 show False by auto
qed
thus "\<exists>a'\<in>A'. \<forall>b'\<in>A'. (b', a') \<notin> dir_image r f"
- using A_def 1 by blast
+ 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)"
-unfolding well_order_on_def
-using Linear_order_dir_image[of r f] wf_dir_image[of "r - Id" f]
- dir_image_minus_Id[of f r]
- subset_inj_on[of f "Field r" "Field(r - Id)"]
- mono_Field[of "r - Id" r] by auto
+ "\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Well_order (dir_image r f)"
+ unfolding well_order_on_def
+ using Linear_order_dir_image[of r f] wf_dir_image[of "r - Id" f]
+ dir_image_minus_Id[of f r]
+ subset_inj_on[of f "Field r" "Field(r - Id)"]
+ mono_Field[of "r - Id" r] by auto
lemma dir_image_bij_betw:
-"\<lbrakk>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_Field order_on_defs)
+ "\<lbrakk>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_Field order_on_defs)
lemma dir_image_compat:
-"compat r (dir_image r f) f"
-unfolding compat_def dir_image_def by auto
+ "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
+ "\<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
+ "\<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'"
+ 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'"
proof-
- let ?r' = "dir_image r f"
- have 1: "A = Field r \<and> Well_order r"
- using WELL well_order_on_Well_order by blast
- hence 2: "iso r ?r' f"
- using dir_image_iso using BIJ unfolding bij_betw_def by auto
- hence "f ` (Field r) = Field ?r'" using 1 iso_iff[of r ?r'] by blast
- hence "Field ?r' = A'"
- using 1 BIJ unfolding bij_betw_def by auto
- moreover have "Well_order ?r'"
- using 1 Well_order_dir_image BIJ unfolding bij_betw_def by blast
- ultimately show ?thesis unfolding ordIso_def using 1 2 by blast
+ let ?r' = "dir_image r f"
+ have 1: "A = Field r \<and> Well_order r"
+ using WELL well_order_on_Well_order by blast
+ hence 2: "iso r ?r' f"
+ using dir_image_iso using BIJ unfolding bij_betw_def by auto
+ hence "f ` (Field r) = Field ?r'" using 1 iso_iff[of r ?r'] by blast
+ hence "Field ?r' = A'"
+ using 1 BIJ unfolding bij_betw_def by auto
+ moreover have "Well_order ?r'"
+ using 1 Well_order_dir_image BIJ unfolding bij_betw_def by blast
+ ultimately show ?thesis unfolding ordIso_def using 1 2 by blast
qed
@@ -1086,8 +1029,8 @@
in a product of proper filters on the original relation (assumed to be a well-order).\<close>
definition bsqr :: "'a rel => ('a * 'a)rel"
-where
-"bsqr r = {((a1,a2),(b1,b2)).
+ where
+ "bsqr r = {((a1,a2),(b1,b2)).
{a1,a2,b1,b2} \<le> Field r \<and>
(a1 = b1 \<and> a2 = b2 \<or>
(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r - Id \<or>
@@ -1096,15 +1039,15 @@
)}"
lemma Field_bsqr:
-"Field (bsqr r) = Field r \<times> Field r"
+ "Field (bsqr r) = Field r \<times> Field r"
proof
show "Field (bsqr r) \<le> Field r \<times> Field r"
proof-
{fix a1 a2 assume "(a1,a2) \<in> Field (bsqr r)"
- moreover
- have "\<And> b1 b2. ((a1,a2),(b1,b2)) \<in> bsqr r \<or> ((b1,b2),(a1,a2)) \<in> bsqr r \<Longrightarrow>
+ moreover
+ have "\<And> b1 b2. ((a1,a2),(b1,b2)) \<in> bsqr r \<or> ((b1,b2),(a1,a2)) \<in> bsqr r \<Longrightarrow>
a1 \<in> Field r \<and> a2 \<in> Field r" unfolding bsqr_def by auto
- ultimately have "a1 \<in> Field r \<and> a2 \<in> Field r" unfolding Field_def by auto
+ ultimately have "a1 \<in> Field r \<and> a2 \<in> Field r" unfolding Field_def by auto
}
thus ?thesis unfolding Field_def by force
qed
@@ -1118,101 +1061,101 @@
qed
lemma bsqr_Refl: "Refl(bsqr r)"
-by(unfold refl_on_def Field_bsqr, auto simp add: bsqr_def)
+ by(unfold refl_on_def Field_bsqr, auto simp add: bsqr_def)
lemma bsqr_Trans:
-assumes "Well_order r"
-shows "trans (bsqr r)"
-unfolding trans_def
+ assumes "Well_order r"
+ shows "trans (bsqr r)"
+ unfolding trans_def
proof safe
(* Preliminary facts *)
have Well: "wo_rel r" using assms wo_rel_def by auto
hence Trans: "trans r" using wo_rel.TRANS by auto
have Anti: "antisym r" using wo_rel.ANTISYM Well by auto
hence TransS: "trans(r - Id)" using Trans by (simp add: trans_diff_Id)
- (* Main proof *)
+ (* Main proof *)
fix a1 a2 b1 b2 c1 c2
assume *: "((a1,a2),(b1,b2)) \<in> bsqr r" and **: "((b1,b2),(c1,c2)) \<in> bsqr r"
hence 0: "{a1,a2,b1,b2,c1,c2} \<le> Field r" unfolding bsqr_def by auto
have 1: "a1 = b1 \<and> a2 = b2 \<or> (wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r - Id \<or>
wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> (a1,b1) \<in> r - Id \<or>
wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> a1 = b1 \<and> (a2,b2) \<in> r - Id"
- using * unfolding bsqr_def by auto
+ using * unfolding bsqr_def by auto
have 2: "b1 = c1 \<and> b2 = c2 \<or> (wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \<in> r - Id \<or>
wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> (b1,c1) \<in> r - Id \<or>
wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> b1 = c1 \<and> (b2,c2) \<in> r - Id"
- using ** unfolding bsqr_def by auto
+ using ** unfolding bsqr_def by auto
show "((a1,a2),(c1,c2)) \<in> bsqr r"
proof-
{assume Case1: "a1 = b1 \<and> a2 = b2"
- hence ?thesis using ** by simp
+ hence ?thesis using ** by simp
}
moreover
{assume Case2: "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r - Id"
- {assume Case21: "b1 = c1 \<and> b2 = c2"
- hence ?thesis using * by simp
- }
- moreover
- {assume Case22: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \<in> r - Id"
- hence "(wo_rel.max2 r a1 a2, wo_rel.max2 r c1 c2) \<in> r - Id"
- using Case2 TransS trans_def[of "r - Id"] by blast
- hence ?thesis using 0 unfolding bsqr_def by auto
- }
- moreover
- {assume Case23_4: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2"
- hence ?thesis using Case2 0 unfolding bsqr_def by auto
- }
- ultimately have ?thesis using 0 2 by auto
+ {assume Case21: "b1 = c1 \<and> b2 = c2"
+ hence ?thesis using * by simp
+ }
+ moreover
+ {assume Case22: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \<in> r - Id"
+ hence "(wo_rel.max2 r a1 a2, wo_rel.max2 r c1 c2) \<in> r - Id"
+ using Case2 TransS trans_def[of "r - Id"] by blast
+ hence ?thesis using 0 unfolding bsqr_def by auto
+ }
+ moreover
+ {assume Case23_4: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2"
+ hence ?thesis using Case2 0 unfolding bsqr_def by auto
+ }
+ ultimately have ?thesis using 0 2 by auto
}
moreover
{assume Case3: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> (a1,b1) \<in> r - Id"
- {assume Case31: "b1 = c1 \<and> b2 = c2"
- hence ?thesis using * by simp
- }
- moreover
- {assume Case32: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \<in> r - Id"
- hence ?thesis using Case3 0 unfolding bsqr_def by auto
- }
- moreover
- {assume Case33: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> (b1,c1) \<in> r - Id"
- hence "(a1,c1) \<in> r - Id"
- using Case3 TransS trans_def[of "r - Id"] by blast
- hence ?thesis using Case3 Case33 0 unfolding bsqr_def by auto
- }
- moreover
- {assume Case33: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> b1 = c1"
- hence ?thesis using Case3 0 unfolding bsqr_def by auto
- }
- ultimately have ?thesis using 0 2 by auto
+ {assume Case31: "b1 = c1 \<and> b2 = c2"
+ hence ?thesis using * by simp
+ }
+ moreover
+ {assume Case32: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \<in> r - Id"
+ hence ?thesis using Case3 0 unfolding bsqr_def by auto
+ }
+ moreover
+ {assume Case33: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> (b1,c1) \<in> r - Id"
+ hence "(a1,c1) \<in> r - Id"
+ using Case3 TransS trans_def[of "r - Id"] by blast
+ hence ?thesis using Case3 Case33 0 unfolding bsqr_def by auto
+ }
+ moreover
+ {assume Case33: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> b1 = c1"
+ hence ?thesis using Case3 0 unfolding bsqr_def by auto
+ }
+ ultimately have ?thesis using 0 2 by auto
}
moreover
{assume Case4: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> a1 = b1 \<and> (a2,b2) \<in> r - Id"
- {assume Case41: "b1 = c1 \<and> b2 = c2"
- hence ?thesis using * by simp
- }
- moreover
- {assume Case42: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \<in> r - Id"
- hence ?thesis using Case4 0 unfolding bsqr_def by force
- }
- moreover
- {assume Case43: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> (b1,c1) \<in> r - Id"
- hence ?thesis using Case4 0 unfolding bsqr_def by auto
- }
- moreover
- {assume Case44: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> b1 = c1 \<and> (b2,c2) \<in> r - Id"
- hence "(a2,c2) \<in> r - Id"
- using Case4 TransS trans_def[of "r - Id"] by blast
- hence ?thesis using Case4 Case44 0 unfolding bsqr_def by auto
- }
- ultimately have ?thesis using 0 2 by auto
+ {assume Case41: "b1 = c1 \<and> b2 = c2"
+ hence ?thesis using * by simp
+ }
+ moreover
+ {assume Case42: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \<in> r - Id"
+ hence ?thesis using Case4 0 unfolding bsqr_def by force
+ }
+ moreover
+ {assume Case43: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> (b1,c1) \<in> r - Id"
+ hence ?thesis using Case4 0 unfolding bsqr_def by auto
+ }
+ moreover
+ {assume Case44: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> b1 = c1 \<and> (b2,c2) \<in> r - Id"
+ hence "(a2,c2) \<in> r - Id"
+ using Case4 TransS trans_def[of "r - Id"] by blast
+ hence ?thesis using Case4 Case44 0 unfolding bsqr_def by auto
+ }
+ ultimately have ?thesis using 0 2 by auto
}
ultimately show ?thesis using 0 1 by auto
qed
qed
lemma bsqr_antisym:
-assumes "Well_order r"
-shows "antisym (bsqr r)"
+ assumes "Well_order r"
+ shows "antisym (bsqr r)"
proof(unfold antisym_def, clarify)
(* Preliminary facts *)
have Well: "wo_rel r" using assms wo_rel_def by auto
@@ -1220,334 +1163,293 @@
have Anti: "antisym r" using wo_rel.ANTISYM Well by auto
hence TransS: "trans(r - Id)" using Trans by (simp add: trans_diff_Id)
hence IrrS: "\<forall>a b. \<not>((a,b) \<in> r - Id \<and> (b,a) \<in> r - Id)"
- using Anti trans_def[of "r - Id"] antisym_def[of "r - Id"] by blast
- (* Main proof *)
+ using Anti trans_def[of "r - Id"] antisym_def[of "r - Id"] by blast
+ (* Main proof *)
fix a1 a2 b1 b2
assume *: "((a1,a2),(b1,b2)) \<in> bsqr r" and **: "((b1,b2),(a1,a2)) \<in> bsqr r"
- hence 0: "{a1,a2,b1,b2} \<le> Field r" unfolding bsqr_def by auto
- have 1: "a1 = b1 \<and> a2 = b2 \<or> (wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r - Id \<or>
+ hence "{a1,a2,b1,b2} \<le> Field r" unfolding bsqr_def by auto
+ moreover
+ have "a1 = b1 \<and> a2 = b2 \<or> (wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r - Id \<or>
wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> (a1,b1) \<in> r - Id \<or>
wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> a1 = b1 \<and> (a2,b2) \<in> r - Id"
- using * unfolding bsqr_def by auto
- have 2: "b1 = a1 \<and> b2 = a2 \<or> (wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) \<in> r - Id \<or>
+ using * unfolding bsqr_def by auto
+ moreover
+ have "b1 = a1 \<and> b2 = a2 \<or> (wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) \<in> r - Id \<or>
wo_rel.max2 r b1 b2 = wo_rel.max2 r a1 a2 \<and> (b1,a1) \<in> r - Id \<or>
wo_rel.max2 r b1 b2 = wo_rel.max2 r a1 a2 \<and> b1 = a1 \<and> (b2,a2) \<in> r - Id"
- using ** unfolding bsqr_def by auto
- show "a1 = b1 \<and> a2 = b2"
- proof-
- {assume Case1: "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r - Id"
- {assume Case11: "(wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) \<in> r - Id"
- hence False using Case1 IrrS by blast
- }
- moreover
- {assume Case12_3: "wo_rel.max2 r b1 b2 = wo_rel.max2 r a1 a2"
- hence False using Case1 by auto
- }
- ultimately have ?thesis using 0 2 by auto
- }
- moreover
- {assume Case2: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> (a1,b1) \<in> r - Id"
- {assume Case21: "(wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) \<in> r - Id"
- hence False using Case2 by auto
- }
- moreover
- {assume Case22: "(b1,a1) \<in> r - Id"
- hence False using Case2 IrrS by blast
- }
- moreover
- {assume Case23: "b1 = a1"
- hence False using Case2 by auto
- }
- ultimately have ?thesis using 0 2 by auto
- }
- moreover
- {assume Case3: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> a1 = b1 \<and> (a2,b2) \<in> r - Id"
- moreover
- {assume Case31: "(wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) \<in> r - Id"
- hence False using Case3 by auto
- }
- moreover
- {assume Case32: "(b1,a1) \<in> r - Id"
- hence False using Case3 by auto
- }
- moreover
- {assume Case33: "(b2,a2) \<in> r - Id"
- hence False using Case3 IrrS by blast
- }
- ultimately have ?thesis using 0 2 by auto
- }
- ultimately show ?thesis using 0 1 by blast
- qed
+ using ** unfolding bsqr_def by auto
+ ultimately show "a1 = b1 \<and> a2 = b2"
+ using IrrS by auto
qed
lemma bsqr_Total:
-assumes "Well_order r"
-shows "Total(bsqr r)"
+ assumes "Well_order r"
+ shows "Total(bsqr r)"
proof-
(* Preliminary facts *)
have Well: "wo_rel r" using assms wo_rel_def by auto
hence Total: "\<forall>a \<in> Field r. \<forall>b \<in> Field r. (a,b) \<in> r \<or> (b,a) \<in> r"
- using wo_rel.TOTALS by auto
- (* Main proof *)
+ using wo_rel.TOTALS by auto
+ (* Main proof *)
{fix a1 a2 b1 b2 assume "{(a1,a2), (b1,b2)} \<le> Field(bsqr r)"
- hence 0: "a1 \<in> Field r \<and> a2 \<in> Field r \<and> b1 \<in> Field r \<and> b2 \<in> Field r"
- using Field_bsqr by blast
- have "((a1,a2) = (b1,b2) \<or> ((a1,a2),(b1,b2)) \<in> bsqr r \<or> ((b1,b2),(a1,a2)) \<in> bsqr r)"
- proof(rule wo_rel.cases_Total[of r a1 a2], clarsimp simp add: Well, simp add: 0)
- (* Why didn't clarsimp simp add: Well 0 do the same job? *)
- assume Case1: "(a1,a2) \<in> r"
- hence 1: "wo_rel.max2 r a1 a2 = a2"
- using Well 0 by (simp add: wo_rel.max2_equals2)
- show ?thesis
- proof(rule wo_rel.cases_Total[of r b1 b2], clarsimp simp add: Well, simp add: 0)
- assume Case11: "(b1,b2) \<in> r"
- hence 2: "wo_rel.max2 r b1 b2 = b2"
- using Well 0 by (simp add: wo_rel.max2_equals2)
- show ?thesis
- proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0)
- assume Case111: "(a2,b2) \<in> r - Id \<or> (b2,a2) \<in> r - Id"
- thus ?thesis using 0 1 2 unfolding bsqr_def by auto
- next
- assume Case112: "a2 = b2"
- show ?thesis
- proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0)
- assume Case1121: "(a1,b1) \<in> r - Id \<or> (b1,a1) \<in> r - Id"
- thus ?thesis using 0 1 2 Case112 unfolding bsqr_def by auto
- next
- assume Case1122: "a1 = b1"
- thus ?thesis using Case112 by auto
- qed
- qed
- next
- assume Case12: "(b2,b1) \<in> r"
- hence 3: "wo_rel.max2 r b1 b2 = b1" using Well 0 by (simp add: wo_rel.max2_equals1)
- show ?thesis
- proof(rule wo_rel.cases_Total3[of r a2 b1], clarsimp simp add: Well, simp add: 0)
- assume Case121: "(a2,b1) \<in> r - Id \<or> (b1,a2) \<in> r - Id"
- thus ?thesis using 0 1 3 unfolding bsqr_def by auto
- next
- assume Case122: "a2 = b1"
- show ?thesis
- proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0)
- assume Case1221: "(a1,b1) \<in> r - Id \<or> (b1,a1) \<in> r - Id"
- thus ?thesis using 0 1 3 Case122 unfolding bsqr_def by auto
- next
- assume Case1222: "a1 = b1"
- show ?thesis
- proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0)
- assume Case12221: "(a2,b2) \<in> r - Id \<or> (b2,a2) \<in> r - Id"
- thus ?thesis using 0 1 3 Case122 Case1222 unfolding bsqr_def by auto
- next
- assume Case12222: "a2 = b2"
- thus ?thesis using Case122 Case1222 by auto
- qed
- qed
- qed
- qed
- next
- assume Case2: "(a2,a1) \<in> r"
- hence 1: "wo_rel.max2 r a1 a2 = a1" using Well 0 by (simp add: wo_rel.max2_equals1)
- show ?thesis
- proof(rule wo_rel.cases_Total[of r b1 b2], clarsimp simp add: Well, simp add: 0)
- assume Case21: "(b1,b2) \<in> r"
- hence 2: "wo_rel.max2 r b1 b2 = b2" using Well 0 by (simp add: wo_rel.max2_equals2)
- show ?thesis
- proof(rule wo_rel.cases_Total3[of r a1 b2], clarsimp simp add: Well, simp add: 0)
- assume Case211: "(a1,b2) \<in> r - Id \<or> (b2,a1) \<in> r - Id"
- thus ?thesis using 0 1 2 unfolding bsqr_def by auto
- next
- assume Case212: "a1 = b2"
- show ?thesis
- proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0)
- assume Case2121: "(a1,b1) \<in> r - Id \<or> (b1,a1) \<in> r - Id"
- thus ?thesis using 0 1 2 Case212 unfolding bsqr_def by auto
- next
- assume Case2122: "a1 = b1"
- show ?thesis
- proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0)
- assume Case21221: "(a2,b2) \<in> r - Id \<or> (b2,a2) \<in> r - Id"
- thus ?thesis using 0 1 2 Case212 Case2122 unfolding bsqr_def by auto
- next
- assume Case21222: "a2 = b2"
- thus ?thesis using Case2122 Case212 by auto
- qed
- qed
- qed
- next
- assume Case22: "(b2,b1) \<in> r"
- hence 3: "wo_rel.max2 r b1 b2 = b1" using Well 0 by (simp add: wo_rel.max2_equals1)
- show ?thesis
- proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0)
- assume Case221: "(a1,b1) \<in> r - Id \<or> (b1,a1) \<in> r - Id"
- thus ?thesis using 0 1 3 unfolding bsqr_def by auto
- next
- assume Case222: "a1 = b1"
- show ?thesis
- proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0)
- assume Case2221: "(a2,b2) \<in> r - Id \<or> (b2,a2) \<in> r - Id"
- thus ?thesis using 0 1 3 Case222 unfolding bsqr_def by auto
- next
- assume Case2222: "a2 = b2"
- thus ?thesis using Case222 by auto
- qed
- qed
- qed
- qed
+ hence 0: "a1 \<in> Field r \<and> a2 \<in> Field r \<and> b1 \<in> Field r \<and> b2 \<in> Field r"
+ using Field_bsqr by blast
+ have "((a1,a2) = (b1,b2) \<or> ((a1,a2),(b1,b2)) \<in> bsqr r \<or> ((b1,b2),(a1,a2)) \<in> bsqr r)"
+ proof(rule wo_rel.cases_Total[of r a1 a2], clarsimp simp add: Well, simp add: 0)
+ (* Why didn't clarsimp simp add: Well 0 do the same job? *)
+ assume Case1: "(a1,a2) \<in> r"
+ hence 1: "wo_rel.max2 r a1 a2 = a2"
+ using Well 0 by (simp add: wo_rel.max2_equals2)
+ show ?thesis
+ proof(rule wo_rel.cases_Total[of r b1 b2], clarsimp simp add: Well, simp add: 0)
+ assume Case11: "(b1,b2) \<in> r"
+ hence 2: "wo_rel.max2 r b1 b2 = b2"
+ using Well 0 by (simp add: wo_rel.max2_equals2)
+ show ?thesis
+ proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0)
+ assume Case111: "(a2,b2) \<in> r - Id \<or> (b2,a2) \<in> r - Id"
+ thus ?thesis using 0 1 2 unfolding bsqr_def by auto
+ next
+ assume Case112: "a2 = b2"
+ show ?thesis
+ proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0)
+ assume Case1121: "(a1,b1) \<in> r - Id \<or> (b1,a1) \<in> r - Id"
+ thus ?thesis using 0 1 2 Case112 unfolding bsqr_def by auto
+ next
+ assume Case1122: "a1 = b1"
+ thus ?thesis using Case112 by auto
+ qed
+ qed
+ next
+ assume Case12: "(b2,b1) \<in> r"
+ hence 3: "wo_rel.max2 r b1 b2 = b1" using Well 0 by (simp add: wo_rel.max2_equals1)
+ show ?thesis
+ proof(rule wo_rel.cases_Total3[of r a2 b1], clarsimp simp add: Well, simp add: 0)
+ assume Case121: "(a2,b1) \<in> r - Id \<or> (b1,a2) \<in> r - Id"
+ thus ?thesis using 0 1 3 unfolding bsqr_def by auto
+ next
+ assume Case122: "a2 = b1"
+ show ?thesis
+ proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0)
+ assume Case1221: "(a1,b1) \<in> r - Id \<or> (b1,a1) \<in> r - Id"
+ thus ?thesis using 0 1 3 Case122 unfolding bsqr_def by auto
+ next
+ assume Case1222: "a1 = b1"
+ show ?thesis
+ proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0)
+ assume Case12221: "(a2,b2) \<in> r - Id \<or> (b2,a2) \<in> r - Id"
+ thus ?thesis using 0 1 3 Case122 Case1222 unfolding bsqr_def by auto
+ next
+ assume Case12222: "a2 = b2"
+ thus ?thesis using Case122 Case1222 by auto
+ qed
+ qed
+ qed
+ qed
+ next
+ assume Case2: "(a2,a1) \<in> r"
+ hence 1: "wo_rel.max2 r a1 a2 = a1" using Well 0 by (simp add: wo_rel.max2_equals1)
+ show ?thesis
+ proof(rule wo_rel.cases_Total[of r b1 b2], clarsimp simp add: Well, simp add: 0)
+ assume Case21: "(b1,b2) \<in> r"
+ hence 2: "wo_rel.max2 r b1 b2 = b2" using Well 0 by (simp add: wo_rel.max2_equals2)
+ show ?thesis
+ proof(rule wo_rel.cases_Total3[of r a1 b2], clarsimp simp add: Well, simp add: 0)
+ assume Case211: "(a1,b2) \<in> r - Id \<or> (b2,a1) \<in> r - Id"
+ thus ?thesis using 0 1 2 unfolding bsqr_def by auto
+ next
+ assume Case212: "a1 = b2"
+ show ?thesis
+ proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0)
+ assume Case2121: "(a1,b1) \<in> r - Id \<or> (b1,a1) \<in> r - Id"
+ thus ?thesis using 0 1 2 Case212 unfolding bsqr_def by auto
+ next
+ assume Case2122: "a1 = b1"
+ show ?thesis
+ proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0)
+ assume Case21221: "(a2,b2) \<in> r - Id \<or> (b2,a2) \<in> r - Id"
+ thus ?thesis using 0 1 2 Case212 Case2122 unfolding bsqr_def by auto
+ next
+ assume Case21222: "a2 = b2"
+ thus ?thesis using Case2122 Case212 by auto
+ qed
+ qed
+ qed
+ next
+ assume Case22: "(b2,b1) \<in> r"
+ hence 3: "wo_rel.max2 r b1 b2 = b1" using Well 0 by (simp add: wo_rel.max2_equals1)
+ show ?thesis
+ proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0)
+ assume Case221: "(a1,b1) \<in> r - Id \<or> (b1,a1) \<in> r - Id"
+ thus ?thesis using 0 1 3 unfolding bsqr_def by auto
+ next
+ assume Case222: "a1 = b1"
+ show ?thesis
+ proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0)
+ assume Case2221: "(a2,b2) \<in> r - Id \<or> (b2,a2) \<in> r - Id"
+ thus ?thesis using 0 1 3 Case222 unfolding bsqr_def by auto
+ next
+ assume Case2222: "a2 = b2"
+ thus ?thesis using Case222 by auto
+ qed
+ qed
+ qed
+ qed
}
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
+ 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)"
-using assms
+ assumes "Well_order r"
+ shows "Well_order(bsqr r)"
+ using assms
proof(simp add: bsqr_Linear_order Linear_order_Well_order_iff, intro allI impI)
have 0: "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)"
- using assms well_order_on_def Linear_order_Well_order_iff by blast
+ using assms well_order_on_def Linear_order_Well_order_iff by blast
fix D assume *: "D \<le> Field (bsqr r)" and **: "D \<noteq> {}"
hence 1: "D \<le> Field r \<times> Field r" unfolding Field_bsqr by simp
- (* *)
+ (* *)
obtain M where M_def: "M = {wo_rel.max2 r a1 a2| a1 a2. (a1,a2) \<in> D}" by blast
have "M \<noteq> {}" using 1 M_def ** by auto
moreover
have "M \<le> Field r" unfolding M_def
- using 1 assms wo_rel_def[of r] wo_rel.max2_among[of r] by fastforce
+ using 1 assms wo_rel_def[of r] wo_rel.max2_among[of r] by fastforce
ultimately obtain m where m_min: "m \<in> M \<and> (\<forall>a \<in> M. (m,a) \<in> r)"
- using 0 by blast
- (* *)
+ using 0 by blast
+ (* *)
obtain A1 where A1_def: "A1 = {a1. \<exists>a2. (a1,a2) \<in> D \<and> wo_rel.max2 r a1 a2 = m}" by blast
have "A1 \<le> Field r" unfolding A1_def using 1 by auto
moreover have "A1 \<noteq> {}" unfolding A1_def using m_min unfolding M_def by blast
ultimately obtain a1 where a1_min: "a1 \<in> A1 \<and> (\<forall>a \<in> A1. (a1,a) \<in> r)"
- using 0 by blast
- (* *)
+ using 0 by blast
+ (* *)
obtain A2 where A2_def: "A2 = {a2. (a1,a2) \<in> D \<and> wo_rel.max2 r a1 a2 = m}" by blast
have "A2 \<le> Field r" unfolding A2_def using 1 by auto
moreover have "A2 \<noteq> {}" unfolding A2_def
- using m_min a1_min unfolding A1_def M_def by blast
+ using m_min a1_min unfolding A1_def M_def by blast
ultimately obtain a2 where a2_min: "a2 \<in> A2 \<and> (\<forall>a \<in> A2. (a2,a) \<in> r)"
- using 0 by blast
- (* *)
+ using 0 by blast
+ (* *)
have 2: "wo_rel.max2 r a1 a2 = m"
- using a1_min a2_min unfolding A1_def A2_def by auto
+ using a1_min a2_min unfolding A1_def A2_def by auto
have 3: "(a1,a2) \<in> D" using a2_min unfolding A2_def by auto
- (* *)
+ (* *)
moreover
{fix b1 b2 assume ***: "(b1,b2) \<in> D"
- hence 4: "{a1,a2,b1,b2} \<le> Field r" using 1 3 by blast
- have 5: "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r"
- using *** a1_min a2_min m_min unfolding A1_def A2_def M_def by auto
- have "((a1,a2),(b1,b2)) \<in> bsqr r"
- proof(cases "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2")
- assume Case1: "wo_rel.max2 r a1 a2 \<noteq> wo_rel.max2 r b1 b2"
- thus ?thesis unfolding bsqr_def using 4 5 by auto
- next
- assume Case2: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2"
- hence "b1 \<in> A1" unfolding A1_def using 2 *** by auto
- hence 6: "(a1,b1) \<in> r" using a1_min by auto
- show ?thesis
- proof(cases "a1 = b1")
- assume Case21: "a1 \<noteq> b1"
- thus ?thesis unfolding bsqr_def using 4 Case2 6 by auto
- next
- assume Case22: "a1 = b1"
- hence "b2 \<in> A2" unfolding A2_def using 2 *** Case2 by auto
- hence 7: "(a2,b2) \<in> r" using a2_min by auto
- thus ?thesis unfolding bsqr_def using 4 7 Case2 Case22 by auto
- qed
- qed
+ hence 4: "{a1,a2,b1,b2} \<le> Field r" using 1 3 by blast
+ have 5: "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r"
+ using *** a1_min a2_min m_min unfolding A1_def A2_def M_def by auto
+ have "((a1,a2),(b1,b2)) \<in> bsqr r"
+ proof(cases "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2")
+ assume Case1: "wo_rel.max2 r a1 a2 \<noteq> wo_rel.max2 r b1 b2"
+ thus ?thesis unfolding bsqr_def using 4 5 by auto
+ next
+ assume Case2: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2"
+ hence "b1 \<in> A1" unfolding A1_def using 2 *** by auto
+ hence 6: "(a1,b1) \<in> r" using a1_min by auto
+ show ?thesis
+ proof(cases "a1 = b1")
+ assume Case21: "a1 \<noteq> b1"
+ thus ?thesis unfolding bsqr_def using 4 Case2 6 by auto
+ next
+ assume Case22: "a1 = b1"
+ hence "b2 \<in> A2" unfolding A2_def using 2 *** Case2 by auto
+ hence 7: "(a2,b2) \<in> r" using a2_min by auto
+ thus ?thesis unfolding bsqr_def using 4 7 Case2 Case22 by auto
+ qed
+ qed
}
- (* *)
+ (* *)
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"
+ 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"
proof-
have "{(a1,a2),(b1,b2)} \<le> Field(bsqr r)"
- using LEQ unfolding Field_def by auto
+ using LEQ unfolding Field_def by auto
hence "{a1,a2,b1,b2} \<le> Field r" unfolding Field_bsqr by auto
hence "{wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2} \<le> Field r"
- using WELL wo_rel_def[of r] wo_rel.max2_among[of r] by fastforce
+ using WELL wo_rel_def[of r] wo_rel.max2_among[of r] by fastforce
moreover have "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r \<or> wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2"
- using LEQ unfolding bsqr_def by auto
+ using LEQ unfolding bsqr_def by auto
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
- NE: "\<not> (\<exists>a. Field r = under r a)"
-shows "\<exists>A. wo_rel.ofilter r A \<and> A < Field r \<and> D \<le> A \<times> A"
+ assumes WELL: "Well_order r" and
+ OF: "wo_rel.ofilter (bsqr r) D" and SUB: "D < Field r \<times> Field r" and
+ NE: "\<not> (\<exists>a. Field r = under r a)"
+ shows "\<exists>A. wo_rel.ofilter r A \<and> A < Field r \<and> D \<le> A \<times> A"
proof-
let ?r' = "bsqr r"
have Well: "wo_rel r" using WELL wo_rel_def by blast
hence Trans: "trans r" using wo_rel.TRANS by blast
have Well': "Well_order ?r' \<and> wo_rel ?r'"
- using WELL bsqr_Well_order wo_rel_def by blast
- (* *)
+ using WELL bsqr_Well_order wo_rel_def by blast
+ (* *)
have "D < Field ?r'" unfolding Field_bsqr using SUB .
with OF obtain a1 and a2 where
- "(a1,a2) \<in> Field ?r'" and 1: "D = underS ?r' (a1,a2)"
- using Well' wo_rel.ofilter_underS_Field[of ?r' D] by auto
+ "(a1,a2) \<in> Field ?r'" and 1: "D = underS ?r' (a1,a2)"
+ using Well' wo_rel.ofilter_underS_Field[of ?r' D] by auto
hence 2: "{a1,a2} \<le> Field r" unfolding Field_bsqr by auto
let ?m = "wo_rel.max2 r a1 a2"
have "D \<le> (under r ?m) \<times> (under r ?m)"
proof(unfold 1)
{fix b1 b2
- let ?n = "wo_rel.max2 r b1 b2"
- assume "(b1,b2) \<in> underS ?r' (a1,a2)"
- hence 3: "((b1,b2),(a1,a2)) \<in> ?r'"
- unfolding underS_def by blast
- hence "(?n,?m) \<in> r" using WELL by (simp add: bsqr_max2)
- moreover
- {have "(b1,b2) \<in> Field ?r'" using 3 unfolding Field_def by auto
- hence "{b1,b2} \<le> Field r" unfolding Field_bsqr by auto
- hence "(b1,?n) \<in> r \<and> (b2,?n) \<in> r"
- using Well by (simp add: wo_rel.max2_greater)
- }
- ultimately have "(b1,?m) \<in> r \<and> (b2,?m) \<in> r"
- using Trans trans_def[of r] by blast
- hence "(b1,b2) \<in> (under r ?m) \<times> (under r ?m)" unfolding under_def by simp}
- thus "underS ?r' (a1,a2) \<le> (under r ?m) \<times> (under r ?m)" by auto
+ let ?n = "wo_rel.max2 r b1 b2"
+ assume "(b1,b2) \<in> underS ?r' (a1,a2)"
+ hence 3: "((b1,b2),(a1,a2)) \<in> ?r'"
+ unfolding underS_def by blast
+ hence "(?n,?m) \<in> r" using WELL by (simp add: bsqr_max2)
+ moreover
+ {have "(b1,b2) \<in> Field ?r'" using 3 unfolding Field_def by auto
+ hence "{b1,b2} \<le> Field r" unfolding Field_bsqr by auto
+ hence "(b1,?n) \<in> r \<and> (b2,?n) \<in> r"
+ using Well by (simp add: wo_rel.max2_greater)
+ }
+ ultimately have "(b1,?m) \<in> r \<and> (b2,?m) \<in> r"
+ using Trans trans_def[of r] by blast
+ hence "(b1,b2) \<in> (under r ?m) \<times> (under r ?m)" unfolding under_def by simp}
+ thus "underS ?r' (a1,a2) \<le> (under r ?m) \<times> (under r ?m)" by auto
qed
moreover have "wo_rel.ofilter r (under r ?m)"
- using Well by (simp add: wo_rel.under_ofilter)
+ using Well by (simp add: wo_rel.under_ofilter)
moreover have "under r ?m < Field r"
- using NE under_Field[of r ?m] by blast
+ using NE under_Field[of r ?m] by blast
ultimately show ?thesis by blast
qed
definition Func where
-"Func A B = {f . (\<forall> a \<in> A. f a \<in> B) \<and> (\<forall> a. a \<notin> A \<longrightarrow> f a = undefined)}"
+ "Func A B = {f . (\<forall> a \<in> A. f a \<in> B) \<and> (\<forall> a. a \<notin> A \<longrightarrow> f a = undefined)}"
lemma Func_empty:
-"Func {} B = {\<lambda>x. undefined}"
-unfolding Func_def by auto
+ "Func {} B = {\<lambda>x. undefined}"
+ unfolding Func_def by auto
lemma Func_elim:
-assumes "g \<in> Func A B" and "a \<in> A"
-shows "\<exists> b. b \<in> B \<and> g a = b"
-using assms unfolding Func_def by (cases "g a = undefined") auto
+ assumes "g \<in> Func A B" and "a \<in> A"
+ shows "\<exists> b. b \<in> B \<and> g a = b"
+ using assms unfolding Func_def by (cases "g a = undefined") auto
definition curr where
-"curr A f \<equiv> \<lambda> a. if a \<in> A then \<lambda>b. f (a,b) else undefined"
+ "curr A f \<equiv> \<lambda> a. if a \<in> A then \<lambda>b. f (a,b) else undefined"
lemma curr_in:
-assumes f: "f \<in> Func (A \<times> B) C"
-shows "curr A f \<in> Func A (Func B C)"
-using assms unfolding curr_def Func_def by auto
+ assumes f: "f \<in> Func (A \<times> B) C"
+ shows "curr A f \<in> Func A (Func B C)"
+ using assms unfolding curr_def Func_def by auto
lemma curr_inj:
-assumes "f1 \<in> Func (A \<times> B) C" and "f2 \<in> Func (A \<times> B) C"
-shows "curr A f1 = curr A f2 \<longleftrightarrow> f1 = f2"
+ assumes "f1 \<in> Func (A \<times> B) C" and "f2 \<in> Func (A \<times> B) C"
+ shows "curr A f1 = curr A f2 \<longleftrightarrow> f1 = f2"
proof safe
assume c: "curr A f1 = curr A f2"
show "f1 = f2"
@@ -1559,14 +1461,14 @@
next
case True hence a: "a \<in> A" and b: "b \<in> B" by auto
thus ?thesis
- using c unfolding curr_def fun_eq_iff by(elim allE[of _ a]) simp
+ using c unfolding curr_def fun_eq_iff by(elim allE[of _ a]) simp
qed
qed
qed
lemma curr_surj:
-assumes "g \<in> Func A (Func B C)"
-shows "\<exists> f \<in> Func (A \<times> B) C. curr A f = g"
+ assumes "g \<in> Func A (Func B C)"
+ shows "\<exists> f \<in> Func (A \<times> B) C. curr A f = g"
proof
let ?f = "\<lambda> ab. if fst ab \<in> A \<and> snd ab \<in> B then g (fst ab) (snd ab) else undefined"
show "curr A ?f = g"
@@ -1579,7 +1481,7 @@
next
case True
obtain g1 where "g1 \<in> Func B C" and "g a = g1"
- using assms using Func_elim[OF assms True] by blast
+ using assms using Func_elim[OF assms True] by blast
thus ?thesis using True unfolding Func_def curr_def by auto
qed
qed
@@ -1587,24 +1489,21 @@
qed
lemma bij_betw_curr:
-"bij_betw (curr A) (Func (A \<times> B) C) (Func A (Func B C))"
- unfolding bij_betw_def inj_on_def image_def
- apply (intro impI conjI ballI)
- apply (erule curr_inj[THEN iffD1], assumption+, safe)
- using curr_surj curr_in apply blast+
- done
+ "bij_betw (curr A) (Func (A \<times> B) C) (Func A (Func B C))"
+ unfolding bij_betw_def inj_on_def
+ using curr_surj curr_in curr_inj by blast
definition Func_map where
-"Func_map B2 f1 f2 g b2 \<equiv> if b2 \<in> B2 then f1 (g (f2 b2)) else undefined"
+ "Func_map B2 f1 f2 g b2 \<equiv> if b2 \<in> B2 then f1 (g (f2 b2)) else undefined"
lemma Func_map:
-assumes g: "g \<in> Func A2 A1" and f1: "f1 ` A1 \<subseteq> B1" and f2: "f2 ` B2 \<subseteq> A2"
-shows "Func_map B2 f1 f2 g \<in> Func B2 B1"
-using assms unfolding Func_def Func_map_def mem_Collect_eq by auto
+ assumes g: "g \<in> Func A2 A1" and f1: "f1 ` A1 \<subseteq> B1" and f2: "f2 ` B2 \<subseteq> A2"
+ shows "Func_map B2 f1 f2 g \<in> Func B2 B1"
+ using assms unfolding Func_def Func_map_def mem_Collect_eq by auto
lemma Func_non_emp:
-assumes "B \<noteq> {}"
-shows "Func A B \<noteq> {}"
+ assumes "B \<noteq> {}"
+ shows "Func A B \<noteq> {}"
proof-
obtain b where b: "b \<in> B" using assms by auto
hence "(\<lambda> a. if a \<in> A then b else undefined) \<in> Func A B" unfolding Func_def by auto
@@ -1612,27 +1511,21 @@
qed
lemma Func_is_emp:
-"Func A B = {} \<longleftrightarrow> A \<noteq> {} \<and> B = {}" (is "?L \<longleftrightarrow> ?R")
+ "Func A B = {} \<longleftrightarrow> A \<noteq> {} \<and> B = {}" (is "?L \<longleftrightarrow> ?R")
proof
- assume L: ?L
- moreover {assume "A = {}" hence False using L Func_empty by auto}
- moreover {assume "B \<noteq> {}" hence False using L Func_non_emp[of B A] by simp }
- ultimately show ?R by blast
+ assume ?L
+ then show ?R
+ using Func_empty Func_non_emp[of B A] by blast
next
- assume R: ?R
- moreover
- {fix f assume "f \<in> Func A B"
- moreover obtain a where "a \<in> A" using R by blast
- ultimately obtain b where "b \<in> B" unfolding Func_def by blast
- with R have False by blast
- }
- thus ?L by blast
+ assume ?R
+ then show ?L
+ using Func_empty Func_non_emp[of B A] by (auto simp: Func_def)
qed
lemma Func_map_surj:
-assumes B1: "f1 ` A1 = B1" and A2: "inj_on f2 B2" "f2 ` B2 \<subseteq> A2"
-and B2A2: "B2 = {} \<Longrightarrow> A2 = {}"
-shows "Func B2 B1 = Func_map B2 f1 f2 ` Func A2 A1"
+ assumes B1: "f1 ` A1 = B1" and A2: "inj_on f2 B2" "f2 ` B2 \<subseteq> A2"
+ and B2A2: "B2 = {} \<Longrightarrow> A2 = {}"
+ shows "Func B2 B1 = Func_map B2 f1 f2 ` Func A2 A1"
proof(cases "B2 = {}")
case True
thus ?thesis using B2A2 by (auto simp: Func_empty Func_map_def)
@@ -1646,15 +1539,15 @@
then obtain k where k: "\<forall> a2 \<in> f2 ` B2. k a2 \<in> B2 \<and> f2 (k a2) = a2"
by atomize_elim (rule bchoice)
{fix b2 assume b2: "b2 \<in> B2"
- hence "f2 (k (f2 b2)) = f2 b2" using k A2(2) by auto
- moreover have "k (f2 b2) \<in> B2" using b2 A2(2) k by auto
- ultimately have "k (f2 b2) = b2" using b2 A2(1) unfolding inj_on_def by blast
+ hence "f2 (k (f2 b2)) = f2 b2" using k A2(2) by auto
+ moreover have "k (f2 b2) \<in> B2" using b2 A2(2) k by auto
+ ultimately have "k (f2 b2) = b2" using b2 A2(1) unfolding inj_on_def by blast
} note kk = this
obtain b22 where b22: "b22 \<in> B2" using B2 by auto
define j2 where [abs_def]: "j2 a2 = (if a2 \<in> f2 ` B2 then k a2 else b22)" for a2
have j2A2: "j2 ` A2 \<subseteq> B2" unfolding j2_def using k b22 by auto
have j2: "\<And> b2. b2 \<in> B2 \<Longrightarrow> j2 (f2 b2) = b2"
- using kk unfolding j2_def by auto
+ using kk unfolding j2_def by auto
define g where "g = Func_map A2 j1 j2 h"
have "Func_map B2 f1 f2 g = h"
proof (rule ext)
@@ -1668,13 +1561,13 @@
show ?thesis using A2 f_inv_into_f[OF b1]
unfolding True g_def Func_map_def j1_def j2[OF \<open>b2 \<in> B2\<close>] by auto
qed(insert A2 True j2[OF True] h B1, unfold j1_def g_def Func_def Func_map_def,
- auto intro: f_inv_into_f)
+ auto intro: f_inv_into_f)
qed(insert h, unfold Func_def Func_map_def, auto)
qed
moreover have "g \<in> Func A2 A1" unfolding g_def apply(rule Func_map[OF h])
- using j2A2 B1 A2 unfolding j1_def by (fast intro: inv_into_into)+
+ using j2A2 B1 A2 unfolding j1_def by (fast intro: inv_into_into)+
ultimately show "h \<in> Func_map B2 f1 f2 ` Func A2 A1"
- unfolding Func_map_def[abs_def] by auto
+ unfolding Func_map_def[abs_def] by auto
qed(use B1 Func_map[OF _ _ A2(2)] in auto)
qed
--- a/src/HOL/BNF_Wellorder_Embedding.thy Fri Jan 13 16:44:00 2023 +0000
+++ b/src/HOL/BNF_Wellorder_Embedding.thy Fri Jan 13 22:47:40 2023 +0000
@@ -8,7 +8,7 @@
section \<open>Well-Order Embeddings as Needed by Bounded Natural Functors\<close>
theory BNF_Wellorder_Embedding
-imports Hilbert_Choice BNF_Wellorder_Relation
+ imports Hilbert_Choice BNF_Wellorder_Relation
begin
text\<open>In this section, we introduce well-order {\em embeddings} and {\em isomorphisms} and
@@ -23,35 +23,35 @@
subsection \<open>Auxiliaries\<close>
lemma UNION_inj_on_ofilter:
-assumes WELL: "Well_order r" and
- OF: "\<And> i. i \<in> I \<Longrightarrow> wo_rel.ofilter r (A i)" and
- INJ: "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
-shows "inj_on f (\<Union>i \<in> I. A i)"
+ assumes WELL: "Well_order r" and
+ OF: "\<And> i. i \<in> I \<Longrightarrow> wo_rel.ofilter r (A i)" and
+ INJ: "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
+ shows "inj_on f (\<Union>i \<in> I. A i)"
proof-
have "wo_rel r" using WELL by (simp add: wo_rel_def)
hence "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i <= A j \<or> A j <= A i"
- using wo_rel.ofilter_linord[of r] OF by blast
+ using wo_rel.ofilter_linord[of r] OF by blast
with WELL INJ show ?thesis
- by (auto simp add: inj_on_UNION_chain)
+ 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
- BIJ: "bij_betw f (underS r a) (underS r' (f a))"
-shows "bij_betw f (under r a) (under r' (f a))"
+ assumes WELL: "Well_order r" and WELL': "Well_order r'" and
+ IN: "a \<in> Field r" and IN': "f a \<in> Field r'" and
+ BIJ: "bij_betw f (underS r a) (underS r' (f a))"
+ shows "bij_betw f (under r a) (under r' (f a))"
proof-
have "a \<notin> underS r a \<and> f a \<notin> underS r' (f a)"
- unfolding underS_def by auto
+ unfolding underS_def by auto
moreover
{have "Refl r \<and> Refl r'" using WELL WELL'
- by (auto simp add: order_on_defs)
- hence "under r a = underS r a \<union> {a} \<and>
+ by (auto simp add: order_on_defs)
+ hence "under r a = underS r a \<union> {a} \<and>
under r' (f a) = underS r' (f a) \<union> {f a}"
- using IN IN' by(auto simp add: Refl_under_underS)
+ using IN IN' by(auto simp add: Refl_under_underS)
}
ultimately show ?thesis
- using BIJ notIn_Un_bij_betw[of a "underS r a" f "underS r' (f a)"] by auto
+ using BIJ notIn_Un_bij_betw[of a "underS r a" f "underS r' (f a)"] by auto
qed
@@ -69,28 +69,28 @@
and an isomorphism (operator \<open>iso\<close>) is a bijective embedding.\<close>
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))"
+ 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 \<open>Strict embeddings:\<close>
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')"
+ 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')"
+ 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'"
+ 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'"
@@ -168,46 +168,46 @@
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"
-shows "wo_rel.ofilter r' (f`A)"
+ assumes WELL: "Well_order r" and WELL': "Well_order r'" and
+ EMB: "embed r r' f" and OF: "wo_rel.ofilter r A"
+ shows "wo_rel.ofilter r' (f`A)"
proof-
(* Preliminary facts *)
from WELL have Well: "wo_rel r" unfolding wo_rel_def .
from WELL' have Well': "wo_rel r'" unfolding wo_rel_def .
from OF have 0: "A \<le> Field r" by(auto simp add: Well wo_rel.ofilter_def)
- (* Main proof *)
+ (* Main proof *)
show ?thesis using Well' WELL EMB 0 embed_Field[of r r' f]
proof(unfold wo_rel.ofilter_def, auto simp add: image_def)
fix a b'
assume *: "a \<in> A" and **: "b' \<in> under r' (f a)"
hence "a \<in> Field r" using 0 by auto
hence "bij_betw f (under r a) (under r' (f a))"
- using * EMB by (auto simp add: embed_def)
+ using * EMB by (auto simp add: embed_def)
hence "f`(under r a) = under r' (f a)"
- by (simp add: bij_betw_def)
+ by (simp add: bij_betw_def)
with ** image_def[of f "under r a"] obtain b where
- 1: "b \<in> under r a \<and> b' = f b" by blast
+ 1: "b \<in> under r a \<and> b' = f b" by blast
hence "b \<in> A" using Well * OF
- by (auto simp add: wo_rel.ofilter_def)
+ by (auto simp add: wo_rel.ofilter_def)
with 1 show "\<exists>b \<in> A. b' = f b" by blast
qed
qed
lemma embed_Field_ofilter:
-assumes WELL: "Well_order r" and WELL': "Well_order r'" and
- EMB: "embed r r' f"
-shows "wo_rel.ofilter r' (f`(Field r))"
+ assumes WELL: "Well_order r" and WELL': "Well_order r'" and
+ EMB: "embed r r' f"
+ shows "wo_rel.ofilter r' (f`(Field r))"
proof-
have "wo_rel.ofilter r (Field r)"
- using WELL by (auto simp add: wo_rel_def wo_rel.Field_ofilter)
+ using WELL by (auto simp add: wo_rel_def wo_rel.Field_ofilter)
with WELL WELL' EMB
show ?thesis by (auto simp add: embed_preserves_ofilter)
qed
lemma embed_inj_on:
-assumes WELL: "Well_order r" and EMB: "embed r r' f"
-shows "inj_on f (Field r)"
+ assumes WELL: "Well_order r" and EMB: "embed r r' f"
+ shows "inj_on f (Field r)"
proof(unfold inj_on_def, clarify)
(* Preliminary facts *)
from WELL have Well: "wo_rel r" unfolding wo_rel_def .
@@ -215,30 +215,30 @@
have Total: "Total r" by simp
from Well wo_rel.REFL[of r]
have Refl: "Refl r" by simp
- (* Main proof *)
+ (* Main proof *)
fix a b
assume *: "a \<in> Field r" and **: "b \<in> Field r" and
- ***: "f a = f b"
+ ***: "f a = f b"
hence 1: "a \<in> Field r \<and> b \<in> Field r"
- unfolding Field_def by auto
+ unfolding Field_def by auto
{assume "(a,b) \<in> r"
- hence "a \<in> under r b \<and> b \<in> under r b"
- using Refl by(auto simp add: under_def refl_on_def)
- hence "a = b"
- using EMB 1 ***
- by (auto simp add: embed_def bij_betw_def inj_on_def)
+ hence "a \<in> under r b \<and> b \<in> under r b"
+ using Refl by(auto simp add: under_def refl_on_def)
+ hence "a = b"
+ using EMB 1 ***
+ by (auto simp add: embed_def bij_betw_def inj_on_def)
}
moreover
{assume "(b,a) \<in> r"
- hence "a \<in> under r a \<and> b \<in> under r a"
- using Refl by(auto simp add: under_def refl_on_def)
- hence "a = b"
- using EMB 1 ***
- by (auto simp add: embed_def bij_betw_def inj_on_def)
+ hence "a \<in> under r a \<and> b \<in> under r a"
+ using Refl by(auto simp add: under_def refl_on_def)
+ hence "a = b"
+ using EMB 1 ***
+ by (auto simp add: embed_def bij_betw_def inj_on_def)
}
ultimately
show "a = b" using Total 1
- by (auto simp add: total_on_def)
+ by (auto simp add: total_on_def)
qed
lemma embed_underS:
@@ -265,173 +265,173 @@
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)))"
-using assms
+ 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)))"
+ using assms
proof(auto simp add: embed_compat embed_inj_on embed_Field_ofilter,
- unfold embed_def, auto) (* get rid of one implication *)
+ unfold embed_def, auto) (* get rid of one implication *)
fix a
assume *: "inj_on f (Field r)" and
- **: "compat r r' f" and
- ***: "wo_rel.ofilter r' (f`(Field r))" and
- ****: "a \<in> Field r"
- (* Preliminary facts *)
+ **: "compat r r' f" and
+ ***: "wo_rel.ofilter r' (f`(Field r))" and
+ ****: "a \<in> Field r"
+ (* Preliminary facts *)
have Well: "wo_rel r"
- using WELL wo_rel_def[of r] by simp
+ using WELL wo_rel_def[of r] by simp
hence Refl: "Refl r"
- using wo_rel.REFL[of r] by simp
+ using wo_rel.REFL[of r] by simp
have Total: "Total r"
- using Well wo_rel.TOTAL[of r] by simp
+ using Well wo_rel.TOTAL[of r] by simp
have Well': "wo_rel r'"
- using WELL' wo_rel_def[of r'] by simp
+ using WELL' wo_rel_def[of r'] by simp
hence Antisym': "antisym r'"
- using wo_rel.ANTISYM[of r'] by simp
+ using wo_rel.ANTISYM[of r'] by simp
have "(a,a) \<in> r"
- using **** Well wo_rel.REFL[of r]
- refl_on_def[of _ r] by auto
+ using **** Well wo_rel.REFL[of r]
+ refl_on_def[of _ r] by auto
hence "(f a, f a) \<in> r'"
- using ** by(auto simp add: compat_def)
+ using ** by(auto simp add: compat_def)
hence 0: "f a \<in> Field r'"
- unfolding Field_def by auto
+ unfolding Field_def by auto
have "f a \<in> f`(Field r)"
- using **** by auto
+ using **** by auto
hence 2: "under r' (f a) \<le> f`(Field r)"
- using Well' *** wo_rel.ofilter_def[of r' "f`(Field r)"] by fastforce
- (* Main proof *)
+ using Well' *** wo_rel.ofilter_def[of r' "f`(Field r)"] by fastforce
+ (* Main proof *)
show "bij_betw f (under r a) (under r' (f a))"
proof(unfold bij_betw_def, auto)
show "inj_on f (under r a)" by (rule subset_inj_on[OF * under_Field])
next
fix b assume "b \<in> under r a"
thus "f b \<in> under r' (f a)"
- unfolding under_def using **
- by (auto simp add: compat_def)
+ unfolding under_def using **
+ by (auto simp add: compat_def)
next
fix b' assume *****: "b' \<in> under r' (f a)"
hence "b' \<in> f`(Field r)"
- using 2 by auto
+ using 2 by auto
with Field_def[of r] obtain b where
- 3: "b \<in> Field r" and 4: "b' = f b" by auto
+ 3: "b \<in> Field r" and 4: "b' = f b" by auto
have "(b,a) \<in> r"
proof-
{assume "(a,b) \<in> r"
- with ** 4 have "(f a, b') \<in> r'"
- by (auto simp add: compat_def)
- with ***** Antisym' have "f a = b'"
- by(auto simp add: under_def antisym_def)
- with 3 **** 4 * have "a = b"
- by(auto simp add: inj_on_def)
+ with ** 4 have "(f a, b') \<in> r'"
+ by (auto simp add: compat_def)
+ with ***** Antisym' have "f a = b'"
+ by(auto simp add: under_def antisym_def)
+ with 3 **** 4 * have "a = b"
+ by(auto simp add: inj_on_def)
}
moreover
{assume "a = b"
- hence "(b,a) \<in> r" using Refl **** 3
- by (auto simp add: refl_on_def)
+ hence "(b,a) \<in> r" using Refl **** 3
+ by (auto simp add: refl_on_def)
}
ultimately
show ?thesis using Total **** 3 by (fastforce simp add: total_on_def)
qed
with 4 show "b' \<in> f`(under r a)"
- unfolding under_def by auto
+ unfolding under_def by auto
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
- IMAGE: "f ` A = Field r'"
-shows "embed r' r (inv_into A f)"
+ 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
+ IMAGE: "f ` A = Field r'"
+ shows "embed r' r (inv_into A f)"
proof-
(* Preliminary facts *)
have Well: "wo_rel r"
- using WELL wo_rel_def[of r] by simp
+ using WELL wo_rel_def[of r] by simp
have Refl: "Refl r"
- using Well wo_rel.REFL[of r] by simp
+ using Well wo_rel.REFL[of r] by simp
have Total: "Total r"
- using Well wo_rel.TOTAL[of r] by simp
- (* Main proof *)
+ using Well wo_rel.TOTAL[of r] by simp
+ (* Main proof *)
have 1: "bij_betw f A (Field r')"
proof(unfold bij_betw_def inj_on_def, auto simp add: IMAGE)
fix b1 b2
assume *: "b1 \<in> A" and **: "b2 \<in> A" and
- ***: "f b1 = f b2"
+ ***: "f b1 = f b2"
have 11: "b1 \<in> Field r \<and> b2 \<in> Field r"
- using * ** Well OF by (auto simp add: wo_rel.ofilter_def)
+ using * ** Well OF by (auto simp add: wo_rel.ofilter_def)
moreover
{assume "(b1,b2) \<in> r"
- hence "b1 \<in> under r b2 \<and> b2 \<in> under r b2"
- unfolding under_def using 11 Refl
- by (auto simp add: refl_on_def)
- hence "b1 = b2" using BIJ * ** ***
- by (simp add: bij_betw_def inj_on_def)
+ hence "b1 \<in> under r b2 \<and> b2 \<in> under r b2"
+ unfolding under_def using 11 Refl
+ by (auto simp add: refl_on_def)
+ hence "b1 = b2" using BIJ * ** ***
+ by (simp add: bij_betw_def inj_on_def)
}
moreover
- {assume "(b2,b1) \<in> r"
- hence "b1 \<in> under r b1 \<and> b2 \<in> under r b1"
- unfolding under_def using 11 Refl
- by (auto simp add: refl_on_def)
- hence "b1 = b2" using BIJ * ** ***
- by (simp add: bij_betw_def inj_on_def)
+ {assume "(b2,b1) \<in> r"
+ hence "b1 \<in> under r b1 \<and> b2 \<in> under r b1"
+ unfolding under_def using 11 Refl
+ by (auto simp add: refl_on_def)
+ hence "b1 = b2" using BIJ * ** ***
+ by (simp add: bij_betw_def inj_on_def)
}
ultimately
show "b1 = b2"
- using Total by (auto simp add: total_on_def)
+ using Total by (auto simp add: total_on_def)
qed
- (* *)
+ (* *)
let ?f' = "(inv_into A f)"
- (* *)
+ (* *)
have 2: "\<forall>b \<in> A. bij_betw ?f' (under r' (f b)) (under r b)"
proof(clarify)
fix b assume *: "b \<in> A"
hence "under r b \<le> A"
- using Well OF by(auto simp add: wo_rel.ofilter_def)
+ using Well OF by(auto simp add: wo_rel.ofilter_def)
moreover
have "f ` (under r b) = under r' (f b)"
- using * BIJ by (auto simp add: bij_betw_def)
+ using * BIJ by (auto simp add: bij_betw_def)
ultimately
show "bij_betw ?f' (under r' (f b)) (under r b)"
- using 1 by (auto simp add: bij_betw_inv_into_subset)
+ using 1 by (auto simp add: bij_betw_inv_into_subset)
qed
- (* *)
+ (* *)
have 3: "\<forall>b' \<in> Field r'. bij_betw ?f' (under r' b') (under r (?f' b'))"
proof(clarify)
fix b' assume *: "b' \<in> Field r'"
have "b' = f (?f' b')" using * 1
- by (auto simp add: bij_betw_inv_into_right)
+ by (auto simp add: bij_betw_inv_into_right)
moreover
{obtain b where 31: "b \<in> A" and "f b = b'" using IMAGE * by force
- hence "?f' b' = b" using 1 by (auto simp add: bij_betw_inv_into_left)
- with 31 have "?f' b' \<in> A" by auto
+ hence "?f' b' = b" using 1 by (auto simp add: bij_betw_inv_into_left)
+ with 31 have "?f' b' \<in> A" by auto
}
ultimately
show "bij_betw ?f' (under r' b') (under r (?f' b'))"
- using 2 by auto
+ using 2 by auto
qed
- (* *)
+ (* *)
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
- IN: "a \<in> Field r" and
- IMAGE: "f ` (underS r a) = Field r'"
-shows "embed r' r (inv_into (underS r a) f)"
-using assms
-by(auto simp add: wo_rel_def wo_rel.underS_ofilter inv_into_ofilter_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
+ IN: "a \<in> Field r" and
+ IMAGE: "f ` (underS r a) = Field r'"
+ shows "embed r' r (inv_into (underS r a) f)"
+ 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)"
-shows "embed r' r (inv_into (Field r) f)"
+ assumes WELL: "Well_order r" and EMB: "embed r r' f" and
+ IMAGE: "Field r' \<le> f ` (Field r)"
+ shows "embed r' r (inv_into (Field r) f)"
proof-
have "(\<forall>b \<in> Field r. bij_betw f (under r b) (under r' (f b)))"
- using EMB by (auto simp add: embed_def)
+ using EMB by (auto simp add: embed_def)
moreover
have "f ` (Field r) \<le> Field r'"
- using EMB WELL by (auto simp add: embed_Field)
+ using EMB WELL by (auto simp add: embed_Field)
ultimately
show ?thesis using assms
- by(auto simp add: wo_rel_def wo_rel.Field_ofilter inv_into_ofilter_embed)
+ by(auto simp add: wo_rel_def wo_rel.Field_ofilter inv_into_ofilter_embed)
qed
lemma inv_into_Field_embed_bij_betw:
@@ -487,12 +487,12 @@
\<close>
lemma wellorders_totally_ordered_aux:
-fixes r ::"'a rel" and r'::"'a' rel" and
- f :: "'a \<Rightarrow> 'a'" and a::'a
-assumes WELL: "Well_order r" and WELL': "Well_order r'" and IN: "a \<in> Field r" and
- IH: "\<forall>b \<in> underS r a. bij_betw f (under r b) (under r' (f b))" and
- NOT: "f ` (underS r a) \<noteq> Field r'" and SUC: "f a = wo_rel.suc r' (f`(underS r a))"
-shows "bij_betw f (under r a) (under r' (f a))"
+ fixes r ::"'a rel" and r'::"'a' rel" and
+ f :: "'a \<Rightarrow> 'a'" and a::'a
+ assumes WELL: "Well_order r" and WELL': "Well_order r'" and IN: "a \<in> Field r" and
+ IH: "\<forall>b \<in> underS r a. bij_betw f (under r b) (under r' (f b))" and
+ NOT: "f ` (underS r a) \<noteq> Field r'" and SUC: "f a = wo_rel.suc r' (f`(underS r a))"
+ shows "bij_betw f (under r a) (under r' (f a))"
proof-
(* Preliminary facts *)
have Well: "wo_rel r" using WELL unfolding wo_rel_def .
@@ -500,197 +500,197 @@
have Trans: "trans r" using Well wo_rel.TRANS[of r] by auto
have Well': "wo_rel r'" using WELL' unfolding wo_rel_def .
have OF: "wo_rel.ofilter r (underS r a)"
- by (auto simp add: Well wo_rel.underS_ofilter)
+ by (auto simp add: Well wo_rel.underS_ofilter)
hence UN: "underS r a = (\<Union>b \<in> underS r a. under r b)"
- using Well wo_rel.ofilter_under_UNION[of r "underS r a"] by blast
- (* Gather facts about elements of underS r a *)
+ using Well wo_rel.ofilter_under_UNION[of r "underS r a"] by blast
+ (* Gather facts about elements of underS r a *)
{fix b assume *: "b \<in> underS r a"
- hence t0: "(b,a) \<in> r \<and> b \<noteq> a" unfolding underS_def by auto
- have t1: "b \<in> Field r"
- using * underS_Field[of r a] by auto
- have t2: "f`(under r b) = under r' (f b)"
- using IH * by (auto simp add: bij_betw_def)
- hence t3: "wo_rel.ofilter r' (f`(under r b))"
- using Well' by (auto simp add: wo_rel.under_ofilter)
- have "f`(under r b) \<le> Field r'"
- using t2 by (auto simp add: under_Field)
- moreover
- have "b \<in> under r b"
- using t1 by(auto simp add: Refl Refl_under_in)
- ultimately
- have t4: "f b \<in> Field r'" by auto
- have "f`(under r b) = under r' (f b) \<and>
+ hence t0: "(b,a) \<in> r \<and> b \<noteq> a" unfolding underS_def by auto
+ have t1: "b \<in> Field r"
+ using * underS_Field[of r a] by auto
+ have t2: "f`(under r b) = under r' (f b)"
+ using IH * by (auto simp add: bij_betw_def)
+ hence t3: "wo_rel.ofilter r' (f`(under r b))"
+ using Well' by (auto simp add: wo_rel.under_ofilter)
+ have "f`(under r b) \<le> Field r'"
+ using t2 by (auto simp add: under_Field)
+ moreover
+ have "b \<in> under r b"
+ using t1 by(auto simp add: Refl Refl_under_in)
+ ultimately
+ have t4: "f b \<in> Field r'" by auto
+ have "f`(under r b) = under r' (f b) \<and>
wo_rel.ofilter r' (f`(under r b)) \<and>
f b \<in> Field r'"
- using t2 t3 t4 by auto
+ using t2 t3 t4 by auto
}
hence bFact:
- "\<forall>b \<in> underS r a. f`(under r b) = under r' (f b) \<and>
+ "\<forall>b \<in> underS r a. f`(under r b) = under r' (f b) \<and>
wo_rel.ofilter r' (f`(under r b)) \<and>
f b \<in> Field r'" by blast
- (* *)
+ (* *)
have subField: "f`(underS r a) \<le> Field r'"
- using bFact by blast
- (* *)
+ using bFact by blast
+ (* *)
have OF': "wo_rel.ofilter r' (f`(underS r a))"
proof-
have "f`(underS r a) = f`(\<Union>b \<in> underS r a. under r b)"
- using UN by auto
+ using UN by auto
also have "\<dots> = (\<Union>b \<in> underS r a. f`(under r b))" by blast
also have "\<dots> = (\<Union>b \<in> underS r a. (under r' (f b)))"
- using bFact by auto
+ using bFact by auto
finally
have "f`(underS r a) = (\<Union>b \<in> underS r a. (under r' (f b)))" .
thus ?thesis
- using Well' bFact
- wo_rel.ofilter_UNION[of r' "underS r a" "\<lambda> b. under r' (f b)"] by fastforce
+ using Well' bFact
+ wo_rel.ofilter_UNION[of r' "underS r a" "\<lambda> b. under r' (f b)"] by fastforce
qed
- (* *)
+ (* *)
have "f`(underS r a) \<union> AboveS r' (f`(underS r a)) = Field r'"
- using Well' OF' by (auto simp add: wo_rel.ofilter_AboveS_Field)
+ using Well' OF' by (auto simp add: wo_rel.ofilter_AboveS_Field)
hence NE: "AboveS r' (f`(underS r a)) \<noteq> {}"
- using subField NOT by blast
- (* Main proof *)
+ using subField NOT by blast
+ (* Main proof *)
have INCL1: "f`(underS r a) \<le> underS r' (f a) "
proof(auto)
fix b assume *: "b \<in> underS r a"
have "f b \<noteq> f a \<and> (f b, f a) \<in> r'"
- using subField Well' SUC NE *
- wo_rel.suc_greater[of r' "f`(underS r a)" "f b"] by force
+ using subField Well' SUC NE *
+ wo_rel.suc_greater[of r' "f`(underS r a)" "f b"] by force
thus "f b \<in> underS r' (f a)"
- unfolding underS_def by simp
+ unfolding underS_def by simp
qed
- (* *)
+ (* *)
have INCL2: "underS r' (f a) \<le> f`(underS r a)"
proof
fix b' assume "b' \<in> underS r' (f a)"
hence "b' \<noteq> f a \<and> (b', f a) \<in> r'"
- unfolding underS_def by simp
+ unfolding underS_def by simp
thus "b' \<in> f`(underS r a)"
- using Well' SUC NE OF'
- wo_rel.suc_ofilter_in[of r' "f ` underS r a" b'] by auto
+ using Well' SUC NE OF'
+ wo_rel.suc_ofilter_in[of r' "f ` underS r a" b'] by auto
qed
- (* *)
+ (* *)
have INJ: "inj_on f (underS r a)"
proof-
have "\<forall>b \<in> underS r a. inj_on f (under r b)"
- using IH by (auto simp add: bij_betw_def)
+ using IH by (auto simp add: bij_betw_def)
moreover
have "\<forall>b. wo_rel.ofilter r (under r b)"
- using Well by (auto simp add: wo_rel.under_ofilter)
+ using Well by (auto simp add: wo_rel.under_ofilter)
ultimately show ?thesis
- using WELL bFact UN
- UNION_inj_on_ofilter[of r "underS r a" "\<lambda>b. under r b" f]
- by auto
+ using WELL bFact UN
+ UNION_inj_on_ofilter[of r "underS r a" "\<lambda>b. under r b" f]
+ by auto
qed
- (* *)
+ (* *)
have BIJ: "bij_betw f (underS r a) (underS r' (f a))"
- unfolding bij_betw_def
- using INJ INCL1 INCL2 by auto
- (* *)
+ unfolding bij_betw_def
+ using INJ INCL1 INCL2 by auto
+ (* *)
have "f a \<in> Field r'"
- using Well' subField NE SUC
- by (auto simp add: wo_rel.suc_inField)
+ using Well' subField NE SUC
+ by (auto simp add: wo_rel.suc_inField)
thus ?thesis
- using WELL WELL' IN BIJ under_underS_bij_betw[of r r' a f] by auto
+ 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
-assumes WELL: "Well_order r" and WELL': "Well_order r'" and
-MAIN1:
- "\<And> a. (False \<notin> g`(underS r a) \<and> f`(underS r a) \<noteq> Field r'
+ fixes r ::"'a rel" and r'::"'a' rel" and
+ f :: "'a \<Rightarrow> 'a'" and g :: "'a \<Rightarrow> bool" and a::'a
+ assumes WELL: "Well_order r" and WELL': "Well_order r'" and
+ MAIN1:
+ "\<And> a. (False \<notin> g`(underS r a) \<and> f`(underS r a) \<noteq> Field r'
\<longrightarrow> f a = wo_rel.suc r' (f`(underS r a)) \<and> g a = True)
\<and>
(\<not>(False \<notin> (g`(underS r a)) \<and> f`(underS r a) \<noteq> Field r')
\<longrightarrow> g a = False)" and
-MAIN2: "\<And> a. a \<in> Field r \<and> False \<notin> g`(under r a) \<longrightarrow>
+ MAIN2: "\<And> a. a \<in> Field r \<and> False \<notin> g`(under r a) \<longrightarrow>
bij_betw f (under r a) (under r' (f a))" and
-Case: "a \<in> Field r \<and> False \<in> g`(under r a)"
-shows "\<exists>f'. embed r' r f'"
+ Case: "a \<in> Field r \<and> False \<in> g`(under r a)"
+ shows "\<exists>f'. embed r' r f'"
proof-
have Well: "wo_rel r" using WELL unfolding wo_rel_def .
hence Refl: "Refl r" using wo_rel.REFL[of r] by auto
have Trans: "trans r" using Well wo_rel.TRANS[of r] by auto
have Antisym: "antisym r" using Well wo_rel.ANTISYM[of r] by auto
have Well': "wo_rel r'" using WELL' unfolding wo_rel_def .
- (* *)
+ (* *)
have 0: "under r a = underS r a \<union> {a}"
- using Refl Case by(auto simp add: Refl_under_underS)
- (* *)
+ using Refl Case by(auto simp add: Refl_under_underS)
+ (* *)
have 1: "g a = False"
proof-
{assume "g a \<noteq> False"
- with 0 Case have "False \<in> g`(underS r a)" by blast
- with MAIN1 have "g a = False" by blast}
+ with 0 Case have "False \<in> g`(underS r a)" by blast
+ with MAIN1 have "g a = False" by blast}
thus ?thesis by blast
qed
let ?A = "{a \<in> Field r. g a = False}"
let ?a = "(wo_rel.minim r ?A)"
- (* *)
+ (* *)
have 2: "?A \<noteq> {} \<and> ?A \<le> Field r" using Case 1 by blast
- (* *)
+ (* *)
have 3: "False \<notin> g`(underS r ?a)"
proof
assume "False \<in> g`(underS r ?a)"
then obtain b where "b \<in> underS r ?a" and 31: "g b = False" by auto
hence 32: "(b,?a) \<in> r \<and> b \<noteq> ?a"
- by (auto simp add: underS_def)
+ by (auto simp add: underS_def)
hence "b \<in> Field r" unfolding Field_def by auto
with 31 have "b \<in> ?A" by auto
hence "(?a,b) \<in> r" using wo_rel.minim_least 2 Well by fastforce
- (* again: why worked without type annotations? *)
+ (* again: why worked without type annotations? *)
with 32 Antisym show False
- by (auto simp add: antisym_def)
+ by (auto simp add: antisym_def)
qed
have temp: "?a \<in> ?A"
- using Well 2 wo_rel.minim_in[of r ?A] by auto
+ using Well 2 wo_rel.minim_in[of r ?A] by auto
hence 4: "?a \<in> Field r" by auto
- (* *)
+ (* *)
have 5: "g ?a = False" using temp by blast
- (* *)
+ (* *)
have 6: "f`(underS r ?a) = Field r'"
- using MAIN1[of ?a] 3 5 by blast
- (* *)
+ using MAIN1[of ?a] 3 5 by blast
+ (* *)
have 7: "\<forall>b \<in> underS r ?a. bij_betw f (under r b) (under r' (f b))"
proof
fix b assume as: "b \<in> underS r ?a"
moreover
have "wo_rel.ofilter r (underS r ?a)"
- using Well by (auto simp add: wo_rel.underS_ofilter)
+ using Well by (auto simp add: wo_rel.underS_ofilter)
ultimately
have "False \<notin> g`(under r b)" using 3 Well by (subst (asm) wo_rel.ofilter_def) fast+
moreover have "b \<in> Field r"
- unfolding Field_def using as by (auto simp add: underS_def)
+ unfolding Field_def using as by (auto simp add: underS_def)
ultimately
show "bij_betw f (under r b) (under r' (f b))"
- using MAIN2 by auto
+ using MAIN2 by auto
qed
- (* *)
+ (* *)
have "embed r' r (inv_into (underS r ?a) f)"
- using WELL WELL' 7 4 6 inv_into_underS_embed[of r ?a f r'] by auto
+ using WELL WELL' 7 4 6 inv_into_underS_embed[of r ?a f r'] by auto
thus ?thesis
- unfolding embed_def by blast
+ 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'"
-shows "(\<exists>f. embed r r' f) \<or> (\<exists>f'. embed r' r f')"
+ fixes r ::"'a rel" and r'::"'a' rel"
+ assumes WELL: "Well_order r" and WELL': "Well_order r'"
+ shows "(\<exists>f. embed r r' f) \<or> (\<exists>f'. embed r' r f')"
proof-
(* Preliminary facts *)
have Well: "wo_rel r" using WELL unfolding wo_rel_def .
hence Refl: "Refl r" using wo_rel.REFL[of r] by auto
have Trans: "trans r" using Well wo_rel.TRANS[of r] by auto
have Well': "wo_rel r'" using WELL' unfolding wo_rel_def .
- (* Main proof *)
+ (* Main proof *)
obtain H where H_def: "H =
(\<lambda>h a. if False \<notin> (snd \<circ> h)`(underS r a) \<and> (fst \<circ> h)`(underS r a) \<noteq> Field r'
then (wo_rel.suc r' ((fst \<circ> h)`(underS r a)), True)
else (undefined, False))" by blast
have Adm: "wo_rel.adm_wo r H"
- using Well
+ using Well
proof(unfold wo_rel.adm_wo_def, clarify)
fix h1::"'a \<Rightarrow> 'a' * bool" and h2::"'a \<Rightarrow> 'a' * bool" and x
assume "\<forall>y\<in>underS r x. h1 y = h2 y"
@@ -701,52 +701,52 @@
by (auto simp add: image_def)
thus "H h1 x = H h2 x" by (simp add: H_def del: not_False_in_image_Ball)
qed
- (* More constant definitions: *)
+ (* More constant definitions: *)
obtain h::"'a \<Rightarrow> 'a' * bool" and f::"'a \<Rightarrow> 'a'" and g::"'a \<Rightarrow> bool"
- where h_def: "h = wo_rel.worec r H" and
- f_def: "f = fst \<circ> h" and g_def: "g = snd \<circ> h" by blast
+ where h_def: "h = wo_rel.worec r H" and
+ f_def: "f = fst \<circ> h" and g_def: "g = snd \<circ> h" by blast
obtain test where test_def:
- "test = (\<lambda> a. False \<notin> (g`(underS r a)) \<and> f`(underS r a) \<noteq> Field r')" by blast
- (* *)
+ "test = (\<lambda> a. False \<notin> (g`(underS r a)) \<and> f`(underS r a) \<noteq> Field r')" by blast
+ (* *)
have *: "\<And> a. h a = H h a"
- using Adm Well wo_rel.worec_fixpoint[of r H] by (simp add: h_def)
+ using Adm Well wo_rel.worec_fixpoint[of r H] by (simp add: h_def)
have Main1:
- "\<And> a. (test a \<longrightarrow> f a = wo_rel.suc r' (f`(underS r a)) \<and> g a = True) \<and>
+ "\<And> a. (test a \<longrightarrow> f a = wo_rel.suc r' (f`(underS r a)) \<and> g a = True) \<and>
(\<not>(test a) \<longrightarrow> g a = False)"
proof- (* How can I prove this withou fixing a? *)
fix a show "(test a \<longrightarrow> f a = wo_rel.suc r' (f`(underS r a)) \<and> g a = True) \<and>
(\<not>(test a) \<longrightarrow> g a = False)"
- using *[of a] test_def f_def g_def H_def by auto
+ using *[of a] test_def f_def g_def H_def by auto
qed
- (* *)
+ (* *)
let ?phi = "\<lambda> a. a \<in> Field r \<and> False \<notin> g`(under r a) \<longrightarrow>
bij_betw f (under r a) (under r' (f a))"
have Main2: "\<And> a. ?phi a"
proof-
fix a show "?phi a"
proof(rule wo_rel.well_order_induct[of r ?phi],
- simp only: Well, clarify)
+ simp only: Well, clarify)
fix a
assume IH: "\<forall>b. b \<noteq> a \<and> (b,a) \<in> r \<longrightarrow> ?phi b" and
- *: "a \<in> Field r" and
- **: "False \<notin> g`(under r a)"
+ *: "a \<in> Field r" and
+ **: "False \<notin> g`(under r a)"
have 1: "\<forall>b \<in> underS r a. bij_betw f (under r b) (under r' (f b))"
proof(clarify)
fix b assume ***: "b \<in> underS r a"
hence 0: "(b,a) \<in> r \<and> b \<noteq> a" unfolding underS_def by auto
moreover have "b \<in> Field r"
- using *** underS_Field[of r a] by auto
+ using *** underS_Field[of r a] by auto
moreover have "False \<notin> g`(under r b)"
- using 0 ** Trans under_incr[of r b a] by auto
+ using 0 ** Trans under_incr[of r b a] by auto
ultimately show "bij_betw f (under r b) (under r' (f b))"
- using IH by auto
+ using IH by auto
qed
- (* *)
+ (* *)
have 21: "False \<notin> g`(underS r a)"
- using ** underS_subset_under[of r a] by auto
+ using ** underS_subset_under[of r a] by auto
have 22: "g`(under r a) \<le> {True}" using ** by auto
moreover have 23: "a \<in> under r a"
- using Refl * by (auto simp add: Refl_under_in)
+ using Refl * by (auto simp add: Refl_under_in)
ultimately have 24: "g a = True" by blast
have 2: "f`(underS r a) \<noteq> Field r'"
proof
@@ -754,29 +754,29 @@
hence "g a = False" using Main1 test_def by blast
with 24 show False using ** by blast
qed
- (* *)
+ (* *)
have 3: "f a = wo_rel.suc r' (f`(underS r a))"
- using 21 2 Main1 test_def by blast
- (* *)
+ using 21 2 Main1 test_def by blast
+ (* *)
show "bij_betw f (under r a) (under r' (f a))"
- using WELL WELL' 1 2 3 *
- wellorders_totally_ordered_aux[of r r' a f] by auto
+ using WELL WELL' 1 2 3 *
+ wellorders_totally_ordered_aux[of r r' a f] by auto
qed
qed
- (* *)
+ (* *)
let ?chi = "(\<lambda> a. a \<in> Field r \<and> False \<in> g`(under r a))"
show ?thesis
proof(cases "\<exists>a. ?chi a")
assume "\<not> (\<exists>a. ?chi a)"
hence "\<forall>a \<in> Field r. bij_betw f (under r a) (under r' (f a))"
- using Main2 by blast
+ using Main2 by blast
thus ?thesis unfolding embed_def by blast
next
assume "\<exists>a. ?chi a"
then obtain a where "?chi a" by blast
hence "\<exists>f'. embed r' r f'"
- using wellorders_totally_ordered_aux2[of r r' g f a]
- WELL WELL' Main1 Main2 test_def by fast
+ using wellorders_totally_ordered_aux2[of r r' g f a]
+ WELL WELL' Main1 Main2 test_def by fast
thus ?thesis by blast
qed
qed
@@ -790,75 +790,75 @@
embeddings of opposite directions are mutually inverse.\<close>
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"
-shows "f a = wo_rel.suc r' (f`(underS r a))"
+ assumes WELL: "Well_order r" and WELL': "Well_order r'" and
+ EMB: "embed r r' f" and IN: "a \<in> Field r"
+ shows "f a = wo_rel.suc r' (f`(underS r a))"
proof-
have "bij_betw f (underS r a) (underS r' (f a))"
- using assms by (auto simp add: embed_underS)
+ using assms by (auto simp add: embed_underS)
hence "f`(underS r a) = underS r' (f a)"
- by (auto simp add: bij_betw_def)
+ by (auto simp add: bij_betw_def)
moreover
{have "f a \<in> Field r'" using IN
- using EMB WELL embed_Field[of r r' f] by auto
- hence "f a = wo_rel.suc r' (underS r' (f a))"
- using WELL' by (auto simp add: wo_rel_def wo_rel.suc_underS)
+ using EMB WELL embed_Field[of r r' f] by auto
+ hence "f a = wo_rel.suc r' (underS r' (f a))"
+ using WELL' by (auto simp add: wo_rel_def wo_rel.suc_underS)
}
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"
-shows "a \<in> Field r \<longrightarrow> f a = g a"
+ assumes WELL: "Well_order r" and WELL': "Well_order r'" and
+ EMBf: "embed r r' f" and EMBg: "embed r r' g"
+ shows "a \<in> Field r \<longrightarrow> f a = g a"
proof(rule wo_rel.well_order_induct[of r], auto simp add: WELL wo_rel_def)
fix a
assume IH: "\<forall>b. b \<noteq> a \<and> (b,a) \<in> r \<longrightarrow> b \<in> Field r \<longrightarrow> f b = g b" and
- *: "a \<in> Field r"
+ *: "a \<in> Field r"
hence "\<forall>b \<in> underS r a. f b = g b"
- unfolding underS_def by (auto simp add: Field_def)
+ unfolding underS_def by (auto simp add: Field_def)
hence "f`(underS r a) = g`(underS r a)" by force
thus "f a = g a"
- using assms * embed_determined[of r r' f a] embed_determined[of r r' g a] by auto
+ 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'"
-shows "(\<forall>a \<in> Field r. f'(f a) = a) \<and> (\<forall>a' \<in> Field r'. f(f' a') = a')"
+ assumes WELL: "Well_order r" and WELL': "Well_order r'" and
+ EMB: "embed r r' f" and EMB': "embed r' r f'"
+ shows "(\<forall>a \<in> Field r. f'(f a) = a) \<and> (\<forall>a' \<in> Field r'. f(f' a') = a')"
proof-
have "embed r r (f' \<circ> f)" using assms
- by(auto simp add: comp_embed)
+ by(auto simp add: comp_embed)
moreover have "embed r r id" using assms
- by (auto simp add: id_embed)
+ by (auto simp add: id_embed)
ultimately have "\<forall>a \<in> Field r. f'(f a) = a"
- using assms embed_unique[of r r "f' \<circ> f" id] id_def by auto
+ using assms embed_unique[of r r "f' \<circ> f" id] id_def by auto
moreover
{have "embed r' r' (f \<circ> f')" using assms
- by(auto simp add: comp_embed)
- moreover have "embed r' r' id" using assms
- by (auto simp add: id_embed)
- ultimately have "\<forall>a' \<in> Field r'. f(f' a') = a'"
- using assms embed_unique[of r' r' "f \<circ> f'" id] id_def by auto
+ by(auto simp add: comp_embed)
+ moreover have "embed r' r' id" using assms
+ by (auto simp add: id_embed)
+ ultimately have "\<forall>a' \<in> Field r'. f(f' a') = a'"
+ using assms embed_unique[of r' r' "f \<circ> f'" id] id_def by auto
}
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"
-shows "bij_betw f (Field r) (Field r')"
+ assumes WELL: "Well_order r" and WELL': "Well_order r'" and
+ EMB: "embed r r' f" and EMB': "embed r' r g"
+ shows "bij_betw f (Field r) (Field r')"
proof-
let ?A = "Field r" let ?A' = "Field r'"
have "embed r r (g \<circ> f) \<and> embed r' r' (f \<circ> g)"
- using assms by (auto simp add: comp_embed)
+ using assms by (auto simp add: comp_embed)
hence 1: "(\<forall>a \<in> ?A. g(f a) = a) \<and> (\<forall>a' \<in> ?A'. f(g a') = a')"
- using WELL id_embed[of r] embed_unique[of r r "g \<circ> f" id]
- WELL' id_embed[of r'] embed_unique[of r' r' "f \<circ> g" id]
- id_def by auto
+ using WELL id_embed[of r] embed_unique[of r r "g \<circ> f" id]
+ WELL' id_embed[of r'] embed_unique[of r' r' "f \<circ> g" id]
+ id_def by auto
have 2: "(\<forall>a \<in> ?A. f a \<in> ?A') \<and> (\<forall>a' \<in> ?A'. g a' \<in> ?A)"
- using assms embed_Field[of r r' f] embed_Field[of r' r g] by blast
- (* *)
+ using assms embed_Field[of r r' f] embed_Field[of r' r g] by blast
+ (* *)
show ?thesis
proof(unfold bij_betw_def inj_on_def, auto simp add: 2)
fix a b assume *: "a \<in> ?A" "b \<in> ?A" and **: "f a = f b"
@@ -872,24 +872,24 @@
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"
-shows "iso r r' f"
-unfolding iso_def using assms by (auto simp add: 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"
+ shows "iso r r' f"
+ unfolding iso_def using assms by (auto simp add: embed_bothWays_bij_betw)
subsection \<open>More properties of embeddings, strict embeddings and isomorphisms\<close>
lemma embed_bothWays_Field_bij_betw:
-assumes WELL: "Well_order r" and WELL': "Well_order r'" and
- EMB: "embed r r' f" and EMB': "embed r' r f'"
-shows "bij_betw f (Field r) (Field r')"
+ assumes WELL: "Well_order r" and WELL': "Well_order r'" and
+ EMB: "embed r r' f" and EMB': "embed r' r f'"
+ shows "bij_betw f (Field r) (Field r')"
proof-
have "(\<forall>a \<in> Field r. f'(f a) = a) \<and> (\<forall>a' \<in> Field r'. f(f' a') = a')"
- using assms by (auto simp add: embed_bothWays_inverse)
+ using assms by (auto simp add: embed_bothWays_inverse)
moreover
have "f`(Field r) \<le> Field r' \<and> f' ` (Field r') \<le> Field r"
- using assms by (auto simp add: embed_Field)
+ using assms by (auto simp add: embed_Field)
ultimately
show ?thesis using bij_betw_byWitness[of "Field r" f' f "Field r'"] by auto
qed
@@ -928,7 +928,7 @@
hence 2: "embed r r'' ?g"
using WELL EMB comp_embed[of r r' f r'' f'] by auto
moreover have \<section>: "f' ` Field r' \<subseteq> Field r''"
- by (simp add: "1" embed_Field)
+ by (simp add: "1" embed_Field)
{assume \<section>: "bij_betw ?g (Field r) (Field r'')"
hence "embed r'' r ?h" using 2 WELL
by (auto simp add: inv_into_Field_embed_bij_betw)
@@ -974,57 +974,57 @@
using assms unfolding iso_def 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'"
+ assumes WELL: "Well_order r" and EMB: "embedS r r' f"
+ shows "f ` (Field r) < Field r'"
proof-
have "f`(Field r) \<le> Field r'" using assms
- by (auto simp add: embed_Field embedS_def)
+ by (auto simp add: embed_Field embedS_def)
moreover
{have "inj_on f (Field r)" using assms
- by (auto simp add: embedS_def embed_inj_on)
- hence "f`(Field r) \<noteq> Field r'" using EMB
- by (auto simp add: embedS_def bij_betw_def)
+ by (auto simp add: embedS_def embed_inj_on)
+ hence "f`(Field r) \<noteq> Field r'" using EMB
+ by (auto simp add: embedS_def bij_betw_def)
}
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')"
+ assumes WELL: "Well_order r" and ISO: "embed r r' f"
+ shows "embedS r r' f = (f ` (Field r) < Field r')"
proof
assume "embedS r r' f"
thus "f ` Field r \<subset> Field r'"
- using WELL by (auto simp add: embedS_Field)
+ using WELL by (auto simp add: embedS_Field)
next
assume "f ` Field r \<subset> Field r'"
hence "\<not> bij_betw f (Field r) (Field r')"
- unfolding bij_betw_def by blast
+ unfolding bij_betw_def by blast
thus "embedS r r' f" unfolding embedS_def
- using ISO by auto
+ using ISO by auto
qed
lemma iso_Field: "iso r r' f \<Longrightarrow> f ` (Field r) = Field r'"
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')"
+ assumes "Well_order r"
+ shows "iso r r' f = (embed r r' f \<and> f ` (Field r) = Field r')"
proof
assume "iso r r' f"
thus "embed r r' f \<and> f ` (Field r) = Field r'"
- by (auto simp add: iso_Field iso_def)
+ by (auto simp add: iso_Field iso_def)
next
assume *: "embed r r' f \<and> f ` Field r = Field r'"
hence "inj_on f (Field r)" using assms by (auto simp add: embed_inj_on)
with * have "bij_betw f (Field r) (Field r')"
- unfolding bij_betw_def by simp
+ unfolding bij_betw_def by simp
with * show "iso r r' f" unfolding iso_def by auto
qed
lemma iso_iff2: "iso r r' f \<longleftrightarrow>
bij_betw f (Field r) (Field r') \<and>
(\<forall>a \<in> Field r. \<forall>b \<in> Field r. (a, b) \<in> r \<longleftrightarrow> (f a, f b) \<in> r')"
- (is "?lhs = ?rhs")
+ (is "?lhs = ?rhs")
proof
assume L: ?lhs
then have "bij_betw f (Field r) (Field r')" and emb: "embed r r' f"
@@ -1047,31 +1047,31 @@
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)"
+ 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)"
proof
assume "iso r r' f"
thus "bij_betw f (Field r) (Field r') \<and> compat r r' f"
- unfolding compat_def using WELL by (auto simp add: iso_iff2 Field_def)
+ unfolding compat_def using WELL by (auto simp add: iso_iff2 Field_def)
next
have Well: "wo_rel r \<and> wo_rel r'" using WELL WELL'
- by (auto simp add: wo_rel_def)
+ by (auto simp add: wo_rel_def)
assume *: "bij_betw f (Field r) (Field r') \<and> compat r r' f"
thus "iso r r' f"
- unfolding "compat_def" using assms
+ unfolding "compat_def" using assms
proof(auto simp add: iso_iff2)
fix a b assume **: "a \<in> Field r" "b \<in> Field r" and
- ***: "(f a, f b) \<in> r'"
+ ***: "(f a, f b) \<in> r'"
{assume "(b,a) \<in> r \<or> b = a"
- hence "(b,a) \<in> r"using Well ** wo_rel.REFL[of r] refl_on_def[of _ r] by blast
- hence "(f b, f a) \<in> r'" using * unfolding compat_def by auto
- hence "f a = f b"
- using Well *** wo_rel.ANTISYM[of r'] antisym_def[of r'] by blast
- hence "a = b" using * ** unfolding bij_betw_def inj_on_def by auto
- hence "(a,b) \<in> r" using Well ** wo_rel.REFL[of r] refl_on_def[of _ r] by blast
+ hence "(b,a) \<in> r"using Well ** wo_rel.REFL[of r] refl_on_def[of _ r] by blast
+ hence "(f b, f a) \<in> r'" using * unfolding compat_def by auto
+ hence "f a = f b"
+ using Well *** wo_rel.ANTISYM[of r'] antisym_def[of r'] by blast
+ hence "a = b" using * ** unfolding bij_betw_def inj_on_def by auto
+ hence "(a,b) \<in> r" using Well ** wo_rel.REFL[of r] refl_on_def[of _ r] by blast
}
thus "(a,b) \<in> r"
- using Well ** wo_rel.TOTAL[of r] total_on_def[of _ r] by blast
+ using Well ** wo_rel.TOTAL[of r] total_on_def[of _ r] by blast
qed
qed
@@ -1098,12 +1098,7 @@
lemma iso_forward:
assumes "(x,y) \<in> r" "iso r r' f" shows "(f x,f y) \<in> r'"
-proof -
- have "x \<in> Field r" "y \<in> Field r"
- using assms by (auto simp: Field_def)
- with assms show ?thesis unfolding iso_iff2 by blast
-qed
-
+ using assms by (auto simp: Field_def iso_iff2)
lemma iso_trans:
assumes "trans r" and iso: "iso r r' f" shows "trans r'"
@@ -1112,7 +1107,7 @@
fix x y z
assume xyz: "(x, y) \<in> r'" "(y, z) \<in> r'"
then have *: "(inv_into (Field r) f x, inv_into (Field r) f y) \<in> r"
- "(inv_into (Field r) f y, inv_into (Field r) f z) \<in> r"
+ "(inv_into (Field r) f y, inv_into (Field r) f z) \<in> r"
using iso_backward [OF _ iso] by blast+
then have "inv_into (Field r) f x \<in> Field r" "inv_into (Field r) f y \<in> Field r"
by (auto simp: Field_def)
--- a/src/HOL/BNF_Wellorder_Relation.thy Fri Jan 13 16:44:00 2023 +0000
+++ b/src/HOL/BNF_Wellorder_Relation.thy Fri Jan 13 22:47:40 2023 +0000
@@ -8,7 +8,7 @@
section \<open>Well-Order Relations as Needed by Bounded Natural Functors\<close>
theory BNF_Wellorder_Relation
-imports Order_Relation
+ imports Order_Relation
begin
text\<open>In this section, we develop basic concepts and results pertaining
@@ -41,35 +41,35 @@
subsection \<open>Auxiliaries\<close>
lemma REFL: "Refl r"
-using WELL order_on_defs[of _ r] by auto
+ using WELL order_on_defs[of _ r] by auto
lemma TRANS: "trans r"
-using WELL order_on_defs[of _ r] by auto
+ using WELL order_on_defs[of _ r] by auto
lemma ANTISYM: "antisym r"
-using WELL order_on_defs[of _ r] by auto
+ using WELL order_on_defs[of _ r] by auto
lemma TOTAL: "Total r"
-using WELL order_on_defs[of _ r] by auto
+ 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
+ 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
+ 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
+ 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>
+ "\<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
+ 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);
+ "\<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
+ using TOTALS by auto
subsection \<open>Well-founded induction and recursion adapted to non-strict well-order relations\<close>
@@ -81,34 +81,34 @@
having to take out the diagonal each time in order to switch to a well-founded relation.\<close>
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"
+ assumes IND: "\<And>x. \<forall>y. y \<noteq> x \<and> (y, x) \<in> r \<longrightarrow> P y \<Longrightarrow> P x"
+ shows "P a"
proof-
have "\<And>x. \<forall>y. (y, x) \<in> r - Id \<longrightarrow> P y \<Longrightarrow> P x"
- using IND by blast
+ using IND by blast
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"
+ 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"
+ 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)"
+ assumes ADM: "adm_wo H"
+ shows "worec H = H (worec H)"
proof-
let ?rS = "r - Id"
have "adm_wf (r - Id) H"
- unfolding adm_wf_def
- using ADM adm_wo_def[of H] underS_def[of r] by auto
+ unfolding adm_wf_def
+ using ADM adm_wo_def[of H] underS_def[of r] by auto
hence "wfrec ?rS H = H (wfrec ?rS H)"
- using WF wfrec_fixpoint[of ?rS H] by simp
+ using WF wfrec_fixpoint[of ?rS H] by simp
thus ?thesis unfolding worec_def .
qed
@@ -127,97 +127,83 @@
Order filters for well-orders are also known as ``initial segments".\<close>
definition max2 :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
-where "max2 a b \<equiv> if (a,b) \<in> r then b else 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)"
+ 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"
+ where "minim A \<equiv> THE b. isMinim A b"
definition supr :: "'a set \<Rightarrow> 'a"
-where "supr A \<equiv> minim (Above A)"
+ where "supr A \<equiv> minim (Above A)"
definition suc :: "'a set \<Rightarrow> 'a"
-where "suc A \<equiv> minim (AboveS A)"
+ where "suc A \<equiv> minim (AboveS A)"
subsubsection \<open>Properties of max2\<close>
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}"
+ 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}"
proof-
{assume "(a,b) \<in> r"
- hence ?thesis using max2_def assms REFL refl_on_def
- by (auto simp add: refl_on_def)
+ hence ?thesis using max2_def assms REFL refl_on_def
+ by (auto simp add: refl_on_def)
}
moreover
{assume "a = b"
- hence "(a,b) \<in> r" using REFL assms
- by (auto simp add: refl_on_def)
+ hence "(a,b) \<in> r" using REFL assms
+ by (auto simp add: refl_on_def)
}
moreover
{assume *: "a \<noteq> b \<and> (b,a) \<in> r"
- hence "(a,b) \<notin> r" using ANTISYM
- by (auto simp add: antisym_def)
- hence ?thesis using * max2_def assms REFL refl_on_def
- by (auto simp add: refl_on_def)
+ hence "(a,b) \<notin> r" using ANTISYM
+ by (auto simp add: antisym_def)
+ hence ?thesis using * max2_def assms REFL refl_on_def
+ by (auto simp add: refl_on_def)
}
ultimately show ?thesis using assms TOTAL
- total_on_def[of "Field r" r] by blast
+ 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)
+ 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
+ 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)
+ 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)"
-using assms ANTISYM unfolding antisym_def using TOTALS
-unfolding max2_def by auto
+ assumes "a \<in> Field r" and "b \<in> Field r"
+ shows "(max2 a b = b) = ((a,b) \<in> r)"
+ using assms ANTISYM unfolding antisym_def using TOTALS
+ unfolding max2_def by auto
lemma in_notinI:
-assumes "(j,i) \<notin> r \<or> j = i" and "i \<in> Field r" and "j \<in> Field r"
-shows "(i,j) \<in> r" using assms max2_def max2_greater_among by fastforce
+ assumes "(j,i) \<notin> r \<or> j = i" and "i \<in> Field r" and "j \<in> Field r"
+ shows "(i,j) \<in> r" using assms max2_def max2_greater_among by fastforce
subsubsection \<open>Existence and uniqueness for isMinim and well-definedness of minim\<close>
lemma isMinim_unique:
-assumes MINIM: "isMinim B a" and MINIM': "isMinim B a'"
-shows "a = a'"
-proof-
- {have "a \<in> B"
- using MINIM isMinim_def by simp
- hence "(a',a) \<in> r"
- using MINIM' isMinim_def by simp
- }
- moreover
- {have "a' \<in> B"
- using MINIM' isMinim_def by simp
- hence "(a,a') \<in> r"
- using MINIM isMinim_def by simp
- }
- ultimately
- show ?thesis using ANTISYM antisym_def[of r] by blast
-qed
+ assumes "isMinim B a" "isMinim B a'"
+ shows "a = a'"
+ using assms ANTISYM antisym_def[of r] by (auto simp: isMinim_def)
lemma Well_order_isMinim_exists:
-assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}"
-shows "\<exists>b. isMinim B b"
+ assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}"
+ shows "\<exists>b. isMinim B b"
proof-
from spec[OF WF[unfolded wf_eq_minimal[of "r - Id"]], of B] NE obtain b where
*: "b \<in> B \<and> (\<forall>b'. b' \<noteq> b \<and> (b',b) \<in> r \<longrightarrow> b' \<notin> B)" by auto
@@ -232,52 +218,46 @@
moreover have "b' = b \<Longrightarrow> (b, b') \<in> r"
using ** REFL by (auto simp add: refl_on_def)
moreover have "b' \<noteq> b \<and> (b',b) \<notin> r \<Longrightarrow> (b,b') \<in> r"
- using ** TOTAL by (auto simp add: total_on_def)
+ using ** TOTAL by (auto simp add: total_on_def)
ultimately show "(b,b') \<in> r" by blast
qed
qed
- then have "isMinim B b"
+ then show ?thesis
unfolding isMinim_def using * by auto
- then show ?thesis
- by auto
qed
lemma minim_isMinim:
-assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}"
-shows "isMinim B (minim B)"
+ assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}"
+ shows "isMinim B (minim B)"
proof-
let ?phi = "(\<lambda> b. isMinim B b)"
from assms Well_order_isMinim_exists
obtain b where *: "?phi b" by blast
moreover
have "\<And> b'. ?phi b' \<Longrightarrow> b' = b"
- using isMinim_unique * by auto
+ using isMinim_unique * by auto
ultimately show ?thesis
- unfolding minim_def using theI[of ?phi b] by blast
+ unfolding minim_def using theI[of ?phi b] by blast
qed
subsubsection\<open>Properties of minim\<close>
lemma minim_in:
-assumes "B \<le> Field r" and "B \<noteq> {}"
-shows "minim B \<in> B"
-proof-
- from minim_isMinim[of B] assms
- have "isMinim B (minim B)" by simp
- thus ?thesis by (simp add: isMinim_def)
-qed
+ assumes "B \<le> Field r" and "B \<noteq> {}"
+ shows "minim B \<in> B"
+ using assms minim_isMinim[of B] by (auto simp: isMinim_def)
lemma minim_inField:
-assumes "B \<le> Field r" and "B \<noteq> {}"
-shows "minim B \<in> Field r"
+ assumes "B \<le> Field r" and "B \<noteq> {}"
+ shows "minim B \<in> Field r"
proof-
have "minim B \<in> B" using assms by (simp add: minim_in)
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"
+ assumes SUB: "B \<le> Field r" and IN: "b \<in> B"
+ shows "(minim B, b) \<in> r"
proof-
from minim_isMinim[of B] assms
have "isMinim B (minim B)" by auto
@@ -285,137 +265,104 @@
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"
-shows "a = minim B"
+ assumes SUB: "B \<le> Field r" and IN: "a \<in> B" and
+ LEAST: "\<And> b. b \<in> B \<Longrightarrow> (a,b) \<in> r"
+ shows "a = minim B"
proof-
from minim_isMinim[of B] assms
have "isMinim B (minim B)" by auto
moreover have "isMinim B a" using IN LEAST isMinim_def by auto
ultimately show ?thesis
- using isMinim_unique by auto
+ using isMinim_unique by auto
qed
subsubsection\<open>Properties of successor\<close>
lemma suc_AboveS:
-assumes SUB: "B \<le> Field r" and ABOVES: "AboveS B \<noteq> {}"
-shows "suc B \<in> AboveS B"
+ assumes SUB: "B \<le> Field r" and ABOVES: "AboveS B \<noteq> {}"
+ shows "suc B \<in> AboveS B"
proof(unfold suc_def)
have "AboveS B \<le> Field r"
- using AboveS_Field[of r] by auto
+ using AboveS_Field[of r] by auto
thus "minim (AboveS B) \<in> AboveS B"
- using assms by (simp add: minim_in)
+ 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"
-shows "suc B \<noteq> b \<and> (b,suc B) \<in> r"
-proof-
- from assms suc_AboveS
- have "suc B \<in> AboveS B" by simp
- with IN AboveS_def[of r] show ?thesis by simp
-qed
+ assumes SUB: "B \<le> Field r" and ABOVES: "AboveS B \<noteq> {}" and IN: "b \<in> B"
+ shows "suc B \<noteq> b \<and> (b,suc B) \<in> r"
+ using IN AboveS_def[of r] assms suc_AboveS by auto
lemma suc_least_AboveS:
-assumes ABOVES: "a \<in> AboveS B"
-shows "(suc B,a) \<in> r"
-proof(unfold suc_def)
- have "AboveS B \<le> Field r"
- using AboveS_Field[of r] by auto
- thus "(minim (AboveS B),a) \<in> r"
- using assms minim_least by simp
-qed
+ assumes ABOVES: "a \<in> AboveS B"
+ shows "(suc B,a) \<in> r"
+ using assms minim_least AboveS_Field[of r] by (auto simp: suc_def)
lemma suc_inField:
-assumes "B \<le> Field r" and "AboveS B \<noteq> {}"
-shows "suc B \<in> Field r"
-proof-
- have "suc B \<in> AboveS B" using suc_AboveS assms by simp
- thus ?thesis
- using assms AboveS_Field[of r] by auto
-qed
+ assumes "B \<le> Field r" and "AboveS B \<noteq> {}"
+ shows "suc B \<in> Field r"
+ using suc_AboveS assms AboveS_Field[of r] by auto
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"
-shows "a = suc B"
-proof(unfold suc_def)
- have "AboveS B \<le> Field r"
- using AboveS_Field[of r B] by auto
- thus "a = minim (AboveS B)"
- using assms equals_minim
- by simp
-qed
+ assumes "B \<le> Field r" and "a \<in> AboveS B" and "\<And> a'. a' \<in> AboveS B \<Longrightarrow> (a,a') \<in> r"
+ shows "a = suc B"
+ using assms equals_minim AboveS_Field[of r B] by (auto simp: suc_def)
lemma suc_underS:
-assumes IN: "a \<in> Field r"
-shows "a = suc (underS a)"
+ assumes IN: "a \<in> Field r"
+ shows "a = suc (underS a)"
proof-
have "underS a \<le> Field r"
- using underS_Field[of r] by auto
+ using underS_Field[of r] by auto
moreover
have "a \<in> AboveS (underS a)"
- using in_AboveS_underS IN by fast
+ using in_AboveS_underS IN by fast
moreover
have "\<forall>a' \<in> AboveS (underS a). (a,a') \<in> r"
proof(clarify)
fix a'
assume *: "a' \<in> AboveS (underS a)"
hence **: "a' \<in> Field r"
- using AboveS_Field by fast
+ using AboveS_Field by fast
{assume "(a,a') \<notin> r"
- hence "a' = a \<or> (a',a) \<in> r"
- using TOTAL IN ** by (auto simp add: total_on_def)
- moreover
- {assume "a' = a"
- hence "(a,a') \<in> r"
- using REFL IN ** by (auto simp add: refl_on_def)
- }
- moreover
- {assume "a' \<noteq> a \<and> (a',a) \<in> r"
- hence "a' \<in> underS a"
- unfolding underS_def by simp
- hence "a' \<notin> AboveS (underS a)"
- using AboveS_disjoint by fast
- with * have False by simp
- }
- ultimately have "(a,a') \<in> r" by blast
+ hence "a' = a \<or> (a',a) \<in> r"
+ using TOTAL IN ** by (auto simp add: total_on_def)
+ moreover
+ {assume "a' = a"
+ hence "(a,a') \<in> r"
+ using REFL IN ** by (auto simp add: refl_on_def)
+ }
+ moreover
+ {assume "a' \<noteq> a \<and> (a',a) \<in> r"
+ hence "a' \<in> underS a"
+ unfolding underS_def by simp
+ hence "a' \<notin> AboveS (underS a)"
+ using AboveS_disjoint by fast
+ with * have False by simp
+ }
+ ultimately have "(a,a') \<in> r" by blast
}
thus "(a, a') \<in> r" by blast
qed
ultimately show ?thesis
- using equals_suc_AboveS by auto
+ using equals_suc_AboveS by auto
qed
subsubsection \<open>Properties of order filters\<close>
-lemma under_ofilter:
-"ofilter (under a)"
-proof -
- have "\<And>aa x. (aa, a) \<in> r \<Longrightarrow> (x, aa) \<in> r \<Longrightarrow> (x, a) \<in> r"
- proof -
- fix aa x
- assume "(aa,a) \<in> r" "(x,aa) \<in> r"
- then show "(x,a) \<in> r"
- using TRANS trans_def[of r] by blast
- qed
- then show ?thesis unfolding ofilter_def under_def
- by (auto simp add: Field_def)
-qed
+lemma under_ofilter: "ofilter (under a)"
+ using TRANS by (auto simp: ofilter_def under_def Field_iff trans_def)
-lemma underS_ofilter:
-"ofilter (underS a)"
+lemma underS_ofilter: "ofilter (underS a)"
unfolding ofilter_def underS_def under_def
proof safe
- fix aa assume "(a, aa) \<in> r" "(aa, a) \<in> r" and DIFF: "aa \<noteq> a"
+ fix b assume "(a, b) \<in> r" "(b, a) \<in> r" and DIFF: "b \<noteq> a"
thus False
- using ANTISYM antisym_def[of r] by blast
+ using ANTISYM antisym_def[of r] by blast
next
- fix aa x
- assume "(aa,a) \<in> r" "aa \<noteq> a" "(x,aa) \<in> r"
+ fix b x
+ assume "(b,a) \<in> r" "b \<noteq> a" "(x,b) \<in> r"
thus "(x,a) \<in> r"
using TRANS trans_def[of r] by blast
next
@@ -427,15 +374,15 @@
qed
lemma Field_ofilter:
-"ofilter (Field r)"
-by(unfold ofilter_def under_def, auto simp add: Field_def)
+ "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))"
+ "ofilter A = ((\<exists>a \<in> Field r. A = underS a) \<or> (A = Field r))"
proof
assume "(\<exists>a\<in>Field r. A = underS a) \<or> A = Field r"
thus "ofilter A"
- by (auto simp: underS_ofilter Field_ofilter)
+ by (auto simp: underS_ofilter Field_ofilter)
next
assume *: "ofilter A"
let ?One = "(\<exists>a\<in>Field r. A = underS a)"
@@ -451,7 +398,7 @@
have 3: "?a \<in> ?B" using minim_in[of ?B] 1 by blast
hence 4: "?a \<notin> A" by blast
have 5: "A \<le> Field r" using * ofilter_def by auto
- (* *)
+ (* *)
moreover
have "A = underS ?a"
proof
@@ -462,12 +409,12 @@
have 12: "x \<noteq> ?a" using 4 ** by auto
have 13: "under x \<le> A" using * ofilter_def ** by auto
{assume "(x,?a) \<notin> r"
- hence "(?a,x) \<in> r"
- using TOTAL total_on_def[of "Field r" r]
- 2 4 11 12 by auto
- hence "?a \<in> under x" using under_def[of r] by auto
- hence "?a \<in> A" using ** 13 by blast
- with 4 have False by simp
+ hence "(?a,x) \<in> r"
+ using TOTAL total_on_def[of "Field r" r]
+ 2 4 11 12 by auto
+ hence "?a \<in> under x" using under_def[of r] by auto
+ hence "?a \<in> A" using ** 13 by blast
+ with 4 have False by simp
}
then have "(x,?a) \<in> r" by blast
thus "x \<in> underS ?a"
@@ -479,13 +426,13 @@
fix x
assume **: "x \<in> underS ?a"
hence 11: "x \<in> Field r"
- using Field_def unfolding underS_def by fastforce
- {assume "x \<notin> A"
+ using Field_def unfolding underS_def by fastforce
+ {assume "x \<notin> A"
hence "x \<in> ?B" using 11 by auto
hence "(?a,x) \<in> r" using 3 minim_least[of ?B x] by blast
hence False
- using ANTISYM antisym_def[of r] ** unfolding underS_def by auto
- }
+ using ANTISYM antisym_def[of r] ** unfolding underS_def by auto
+ }
thus "x \<in> A" by blast
qed
qed
@@ -499,27 +446,27 @@
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
+ "(\<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)"
+ assumes "ofilter A"
+ shows "A = (\<Union>a \<in> A. under a)"
proof
have "\<forall>a \<in> A. under a \<le> A"
- using assms ofilter_def by auto
+ using assms ofilter_def by auto
thus "(\<Union>a \<in> A. under a) \<le> A" by blast
next
have "\<forall>a \<in> A. a \<in> under a"
- using REFL Refl_under_in[of r] assms ofilter_def[of A] by blast
+ using REFL Refl_under_in[of r] assms ofilter_def[of A] by blast
thus "A \<le> (\<Union>a \<in> A. under a)" by blast
qed
subsubsection\<open>Other properties\<close>
lemma ofilter_linord:
-assumes OF1: "ofilter A" and OF2: "ofilter B"
-shows "A \<le> B \<or> B \<le> A"
+ assumes OF1: "ofilter A" and OF2: "ofilter B"
+ shows "A \<le> B \<or> B \<le> A"
proof(cases "A = Field r")
assume Case1: "A = Field r"
hence "B \<le> A" using OF2 ofilter_def by auto
@@ -527,7 +474,7 @@
next
assume Case2: "A \<noteq> Field r"
with ofilter_underS_Field OF1 obtain a where
- 1: "a \<in> Field r \<and> A = underS a" by auto
+ 1: "a \<in> Field r \<and> A = underS a" by auto
show ?thesis
proof(cases "B = Field r")
assume Case21: "B = Field r"
@@ -536,68 +483,68 @@
next
assume Case22: "B \<noteq> Field r"
with ofilter_underS_Field OF2 obtain b where
- 2: "b \<in> Field r \<and> B = underS b" by auto
+ 2: "b \<in> Field r \<and> B = underS b" by auto
have "a = b \<or> (a,b) \<in> r \<or> (b,a) \<in> r"
- using 1 2 TOTAL total_on_def[of _ r] by auto
+ using 1 2 TOTAL total_on_def[of _ r] by auto
moreover
{assume "a = b" with 1 2 have ?thesis by auto
}
moreover
{assume "(a,b) \<in> r"
- with underS_incr[of r] TRANS ANTISYM 1 2
- have "A \<le> B" by auto
- hence ?thesis by auto
+ with underS_incr[of r] TRANS ANTISYM 1 2
+ have "A \<le> B" by auto
+ hence ?thesis by auto
}
moreover
- {assume "(b,a) \<in> r"
- with underS_incr[of r] TRANS ANTISYM 1 2
- have "B \<le> A" by auto
- hence ?thesis by auto
+ {assume "(b,a) \<in> r"
+ with underS_incr[of r] TRANS ANTISYM 1 2
+ have "B \<le> A" by auto
+ hence ?thesis by auto
}
ultimately show ?thesis by blast
qed
qed
lemma ofilter_AboveS_Field:
-assumes "ofilter A"
-shows "A \<union> (AboveS A) = Field r"
+ assumes "ofilter A"
+ shows "A \<union> (AboveS A) = Field r"
proof
show "A \<union> (AboveS A) \<le> Field r"
- using assms ofilter_def AboveS_Field[of r] by auto
+ using assms ofilter_def AboveS_Field[of r] by auto
next
{fix x assume *: "x \<in> Field r" and **: "x \<notin> A"
- {fix y assume ***: "y \<in> A"
- with ** have 1: "y \<noteq> x" by auto
- {assume "(y,x) \<notin> r"
- moreover
- have "y \<in> Field r" using assms ofilter_def *** by auto
- ultimately have "(x,y) \<in> r"
- using 1 * TOTAL total_on_def[of _ r] by auto
- with *** assms ofilter_def under_def[of r] have "x \<in> A" by auto
- with ** have False by contradiction
+ {fix y assume ***: "y \<in> A"
+ with ** have 1: "y \<noteq> x" by auto
+ {assume "(y,x) \<notin> r"
+ moreover
+ have "y \<in> Field r" using assms ofilter_def *** by auto
+ ultimately have "(x,y) \<in> r"
+ using 1 * TOTAL total_on_def[of _ r] by auto
+ with *** assms ofilter_def under_def[of r] have "x \<in> A" by auto
+ with ** have False by contradiction
+ }
+ hence "(y,x) \<in> r" by blast
+ with 1 have "y \<noteq> x \<and> (y,x) \<in> r" by auto
}
- hence "(y,x) \<in> r" by blast
- with 1 have "y \<noteq> x \<and> (y,x) \<in> r" by auto
- }
- with * have "x \<in> AboveS A" unfolding AboveS_def by auto
+ with * have "x \<in> AboveS A" unfolding AboveS_def by auto
}
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"
-shows "b \<in> A"
+ assumes OF: "ofilter A" and ABOVE_NE: "AboveS A \<noteq> {}" and
+ REL: "(b,suc A) \<in> r" and DIFF: "b \<noteq> suc A"
+ shows "b \<in> A"
proof-
have *: "suc A \<in> Field r \<and> b \<in> Field r"
- using WELL REL well_order_on_domain[of "Field r"] by auto
+ using WELL REL well_order_on_domain[of "Field r"] by auto
{assume **: "b \<notin> A"
- hence "b \<in> AboveS A"
- using OF * ofilter_AboveS_Field by auto
- hence "(suc A, b) \<in> r"
- using suc_least_AboveS by auto
- hence False using REL DIFF ANTISYM *
- by (auto simp add: antisym_def)
+ hence "b \<in> AboveS A"
+ using OF * ofilter_AboveS_Field by auto
+ hence "(suc A, b) \<in> r"
+ using suc_least_AboveS by auto
+ hence False using REL DIFF ANTISYM *
+ by (auto simp add: antisym_def)
}
thus ?thesis by blast
qed