--- a/src/HOL/Cardinals/Order_Union.thy Fri Jan 13 11:05:48 2023 +0000
+++ b/src/HOL/Cardinals/Order_Union.thy Fri Jan 13 16:19:56 2023 +0000
@@ -85,9 +85,7 @@
assumes FLD: "Field r Int Field r' = {}" and
TRANS: "trans r" and TRANS': "trans r'"
shows "trans (r Osum r')"
- using assms
- apply (clarsimp simp: trans_def disjoint_iff)
- by (smt (verit) Domain.DomainI Field_def Osum_def Pair_inject Range.intros Un_iff case_prodE case_prodI mem_Collect_eq)
+ using assms unfolding Osum_def trans_def disjoint_iff Field_iff by blast
lemma Osum_Preorder:
"\<lbrakk>Field r Int Field r' = {}; Preorder r; Preorder r'\<rbrakk> \<Longrightarrow> Preorder (r Osum r')"
@@ -97,66 +95,7 @@
assumes FLD: "Field r Int Field r' = {}" and
AN: "antisym r" and AN': "antisym r'"
shows "antisym (r Osum r')"
-proof(unfold antisym_def, auto)
- fix x y assume *: "(x, y) \<in> r \<union>o r'" and **: "(y, x) \<in> r \<union>o r'"
- show "x = y"
- proof-
- {assume Case1: "(x,y) \<in> r"
- hence 1: "x \<in> Field r \<and> y \<in> Field r" unfolding Field_def by auto
- have ?thesis
- proof-
- have "(y,x) \<in> r \<Longrightarrow> ?thesis"
- using Case1 AN antisym_def[of r] by blast
- moreover
- {assume "(y,x) \<in> r'"
- hence "y \<in> Field r'" unfolding Field_def by auto
- hence False using FLD 1 by auto
- }
- moreover
- have "x \<in> Field r' \<Longrightarrow> False" using FLD 1 by auto
- ultimately show ?thesis using ** unfolding Osum_def by blast
- qed
- }
- moreover
- {assume Case2: "(x,y) \<in> r'"
- hence 2: "x \<in> Field r' \<and> y \<in> Field r'" unfolding Field_def by auto
- have ?thesis
- proof-
- {assume "(y,x) \<in> r"
- hence "y \<in> Field r" unfolding Field_def by auto
- hence False using FLD 2 by auto
- }
- moreover
- have "(y,x) \<in> r' \<Longrightarrow> ?thesis"
- using Case2 AN' antisym_def[of r'] by blast
- moreover
- {assume "y \<in> Field r"
- hence False using FLD 2 by auto
- }
- ultimately show ?thesis using ** unfolding Osum_def by blast
- qed
- }
- moreover
- {assume Case3: "x \<in> Field r \<and> y \<in> Field r'"
- have ?thesis
- proof-
- {assume "(y,x) \<in> r"
- hence "y \<in> Field r" unfolding Field_def by auto
- hence False using FLD Case3 by auto
- }
- moreover
- {assume Case32: "(y,x) \<in> r'"
- hence "x \<in> Field r'" unfolding Field_def by blast
- hence False using FLD Case3 by auto
- }
- moreover
- have "\<not> y \<in> Field r" using FLD Case3 by auto
- ultimately show ?thesis using ** unfolding Osum_def by blast
- qed
- }
- ultimately show ?thesis using * unfolding Osum_def by blast
- qed
-qed
+ using assms by (auto simp: disjoint_iff antisym_def Osum_def Field_def)
lemma Osum_Partial_order:
"\<lbrakk>Field r Int Field r' = {}; Partial_order r; Partial_order r'\<rbrakk> \<Longrightarrow>
@@ -171,74 +110,24 @@
unfolding total_on_def Field_Osum unfolding Osum_def by blast
lemma Osum_Linear_order:
- "\<lbrakk>Field r Int Field r' = {}; Linear_order r; Linear_order r'\<rbrakk> \<Longrightarrow>
- Linear_order (r Osum r')"
- unfolding linear_order_on_def using Osum_Partial_order Osum_Total by blast
+ "\<lbrakk>Field r Int Field r' = {}; Linear_order r; Linear_order r'\<rbrakk> \<Longrightarrow> Linear_order (r Osum r')"
+ by (simp add: Osum_Partial_order Osum_Total linear_order_on_def)
lemma Osum_minus_Id1:
assumes "r \<le> Id"
shows "(r Osum r') - Id \<le> (r' - Id) \<union> (Field r \<times> Field r')"
-proof-
- let ?Left = "(r Osum r') - Id"
- let ?Right = "(r' - Id) \<union> (Field r \<times> Field r')"
- {fix a::'a and b assume *: "(a,b) \<notin> Id"
- {assume "(a,b) \<in> r"
- with * have False using assms by auto
- }
- moreover
- {assume "(a,b) \<in> r'"
- with * have "(a,b) \<in> r' - Id" by auto
- }
- ultimately
- have "(a,b) \<in> ?Left \<Longrightarrow> (a,b) \<in> ?Right"
- unfolding Osum_def by auto
- }
- thus ?thesis by auto
-qed
+using assms by (force simp: Osum_def)
lemma Osum_minus_Id2:
assumes "r' \<le> Id"
shows "(r Osum r') - Id \<le> (r - Id) \<union> (Field r \<times> Field r')"
-proof-
- let ?Left = "(r Osum r') - Id"
- let ?Right = "(r - Id) \<union> (Field r \<times> Field r')"
- {fix a::'a and b assume *: "(a,b) \<notin> Id"
- {assume "(a,b) \<in> r'"
- with * have False using assms by auto
- }
- moreover
- {assume "(a,b) \<in> r"
- with * have "(a,b) \<in> r - Id" by auto
- }
- ultimately
- have "(a,b) \<in> ?Left \<Longrightarrow> (a,b) \<in> ?Right"
- unfolding Osum_def by auto
- }
- thus ?thesis by auto
-qed
+using assms by (force simp: Osum_def)
lemma Osum_minus_Id:
assumes TOT: "Total r" and TOT': "Total r'" and
NID: "\<not> (r \<le> Id)" and NID': "\<not> (r' \<le> Id)"
shows "(r Osum r') - Id \<le> (r - Id) Osum (r' - Id)"
-proof-
- {fix a a' assume *: "(a,a') \<in> (r Osum r')" and **: "a \<noteq> a'"
- have "(a,a') \<in> (r - Id) Osum (r' - Id)"
- proof-
- {assume "(a,a') \<in> r \<or> (a,a') \<in> r'"
- with ** have ?thesis unfolding Osum_def by auto
- }
- moreover
- {assume "a \<in> Field r \<and> a' \<in> Field r'"
- hence "a \<in> Field(r - Id) \<and> a' \<in> Field (r' - Id)"
- using assms Total_Id_Field by blast
- hence ?thesis unfolding Osum_def by auto
- }
- ultimately show ?thesis using * unfolding Osum_def by fast
- qed
- }
- thus ?thesis by(auto simp add: Osum_def)
-qed
+ using assms Total_Id_Field by (force simp: Osum_def)
lemma wf_Int_Times:
assumes "A Int B = {}"
@@ -253,11 +142,9 @@
proof(cases "r \<le> Id \<or> r' \<le> Id")
assume Case1: "\<not>(r \<le> Id \<or> r' \<le> Id)"
have "Field(r - Id) Int Field(r' - Id) = {}"
- using FLD mono_Field[of "r - Id" r] mono_Field[of "r' - Id" r']
- Diff_subset[of r Id] Diff_subset[of r' Id] by blast
+ using Case1 FLD TOT TOT' Total_Id_Field by blast
thus ?thesis
- using Case1 Osum_minus_Id[of r r'] assms Osum_wf[of "r - Id" "r' - Id"]
- wf_subset[of "(r - Id) \<union>o (r' - Id)" "(r Osum r') - Id"] by auto
+ by (meson Case1 Osum_minus_Id Osum_wf TOT TOT' WF WF' wf_subset)
next
have 1: "wf(Field r \<times> Field r')"
using FLD by (auto simp add: wf_Int_Times)
--- a/src/HOL/Cardinals/Ordinal_Arithmetic.thy Fri Jan 13 11:05:48 2023 +0000
+++ b/src/HOL/Cardinals/Ordinal_Arithmetic.thy Fri Jan 13 16:19:56 2023 +0000
@@ -8,12 +8,12 @@
section \<open>Ordinal Arithmetic\<close>
theory Ordinal_Arithmetic
-imports Wellorder_Constructions
+ imports Wellorder_Constructions
begin
definition osum :: "'a rel \<Rightarrow> 'b rel \<Rightarrow> ('a + 'b) rel" (infixr "+o" 70)
-where
- "r +o r' = map_prod Inl Inl ` r \<union> map_prod Inr Inr ` r' \<union>
+ where
+ "r +o r' = map_prod Inl Inl ` r \<union> map_prod Inr Inr ` r' \<union>
{(Inl a, Inr a') | a a' . a \<in> Field r \<and> a' \<in> Field r'}"
lemma Field_osum: "Field(r +o r') = Inl ` Field r \<union> Inr ` Field r'"
@@ -24,9 +24,10 @@
unfolding refl_on_def Field_osum unfolding osum_def by blast
lemma osum_trans:
-assumes TRANS: "trans r" and TRANS': "trans r'"
-shows "trans (r +o r')"
-proof(unfold trans_def, safe)
+ assumes TRANS: "trans r" and TRANS': "trans r'"
+ shows "trans (r +o r')"
+ unfolding trans_def
+proof(safe)
fix x y z assume *: "(x, y) \<in> r +o r'" "(y, z) \<in> r +o r'"
thus "(x, z) \<in> r +o r'"
proof (cases x y z rule: sum.exhaust[case_product sum.exhaust sum.exhaust])
@@ -66,9 +67,9 @@
unfolding linear_order_on_def using osum_Partial_order osum_Total by blast
lemma osum_wf:
-assumes WF: "wf r" and WF': "wf r'"
-shows "wf (r +o r')"
-unfolding wf_eq_minimal2 unfolding Field_osum
+ assumes WF: "wf r" and WF': "wf r'"
+ shows "wf (r +o r')"
+ unfolding wf_eq_minimal2 unfolding Field_osum
proof(intro allI impI, elim conjE)
fix A assume *: "A \<subseteq> Inl ` Field r \<union> Inr ` Field r'" and **: "A \<noteq> {}"
obtain B where B_def: "B = A Int Inl ` Field r" by blast
@@ -113,8 +114,8 @@
proof(cases "r \<le> Id \<or> r' \<le> Id")
case False
thus ?thesis
- using osum_minus_Id[of r r'] assms osum_wf[of "r - Id" "r' - Id"]
- wf_subset[of "(r - Id) +o (r' - Id)" "(r +o r') - Id"] by auto
+ using osum_minus_Id[of r r'] assms osum_wf[of "r - Id" "r' - Id"]
+ wf_subset[of "(r - Id) +o (r' - Id)" "(r +o r') - Id"] by auto
next
have 1: "wf (Inl ` Field r \<times> Inr ` Field r')" by (rule wf_Int_Times) auto
case True
@@ -131,13 +132,9 @@
qed
lemma osum_Well_order:
-assumes WELL: "Well_order r" and WELL': "Well_order r'"
-shows "Well_order (r +o r')"
-proof-
- have "Total r \<and> Total r'" using WELL WELL' by (auto simp add: order_on_defs)
- thus ?thesis using assms unfolding well_order_on_def
- using osum_Linear_order osum_wf_Id by blast
-qed
+ assumes WELL: "Well_order r" and WELL': "Well_order r'"
+ shows "Well_order (r +o r')"
+ by (meson WELL WELL' osum_Linear_order osum_wf_Id well_order_on_def wo_rel.TOTAL wo_rel.intro)
lemma osum_embedL:
assumes WELL: "Well_order r" and WELL': "Well_order r'"
@@ -162,10 +159,10 @@
unfolding dir_image_def map_prod_def by auto
lemma map_prod_ordIso: "\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> map_prod f f ` r =o r"
- unfolding dir_image_alt[symmetric] by (rule ordIso_symmetric[OF dir_image_ordIso])
+ by (metis dir_image_alt dir_image_ordIso ordIso_symmetric)
definition oprod :: "'a rel \<Rightarrow> 'b rel \<Rightarrow> ('a \<times> 'b) rel" (infixr "*o" 80)
-where "r *o r' = {((x1, y1), (x2, y2)).
+ where "r *o r' = {((x1, y1), (x2, y2)).
(((y1, y2) \<in> r' - Id \<and> x1 \<in> Field r \<and> x2 \<in> Field r) \<or>
((y1, y2) \<in> Restr Id (Field r') \<and> (x1, x2) \<in> r))}"
@@ -178,30 +175,7 @@
lemma oprod_trans:
assumes "trans r" "trans r'" "antisym r" "antisym r'"
shows "trans (r *o r')"
-proof(unfold trans_def, safe)
- fix x y z assume *: "(x, y) \<in> r *o r'" "(y, z) \<in> r *o r'"
- thus "(x, z) \<in> r *o r'"
- unfolding oprod_def
- apply safe
- apply (metis assms(2) transE)
- apply (metis assms(2) transE)
- apply (metis assms(2) transE)
- apply (metis assms(4) antisymD)
- apply (metis assms(4) antisymD)
- apply (metis assms(2) transE)
- apply (metis assms(4) antisymD)
- apply (metis Field_def Range_iff Un_iff)
- apply (metis Field_def Range_iff Un_iff)
- apply (metis Field_def Range_iff Un_iff)
- apply (metis Field_def Domain_iff Un_iff)
- apply (metis Field_def Domain_iff Un_iff)
- apply (metis Field_def Domain_iff Un_iff)
- apply (metis assms(1) transE)
- apply (metis assms(1) transE)
- apply (metis assms(1) transE)
- apply (metis assms(1) transE)
- done
-qed
+ using assms by (clarsimp simp: trans_def antisym_def oprod_def) (metis FieldI1 FieldI2)
lemma oprod_Preorder: "\<lbrakk>Preorder r; Preorder r'; antisym r; antisym r'\<rbrakk> \<Longrightarrow> Preorder (r *o r')"
unfolding preorder_on_def using oprod_Refl oprod_trans by blast
@@ -219,9 +193,9 @@
unfolding linear_order_on_def using oprod_Partial_order oprod_Total by blast
lemma oprod_wf:
-assumes WF: "wf r" and WF': "wf r'"
-shows "wf (r *o r')"
-unfolding wf_eq_minimal2 unfolding Field_oprod
+ assumes WF: "wf r" and WF': "wf r'"
+ shows "wf (r *o r')"
+ unfolding wf_eq_minimal2 unfolding Field_oprod
proof(intro allI impI, elim conjE)
fix A assume *: "A \<subseteq> Field r \<times> Field r'" and **: "A \<noteq> {}"
then obtain y where y: "y \<in> snd ` A" "\<forall>y'\<in>snd ` A. (y', y) \<notin> r'"
@@ -285,22 +259,17 @@
proof(cases "r \<le> Id \<or> r' \<le> Id")
case False
thus ?thesis
- using oprod_minus_Id[of r r'] assms oprod_wf[of "r - Id" "r' - Id"]
- wf_subset[of "(r - Id) *o (r' - Id)" "(r *o r') - Id"] by auto
+ by (meson TOT TOT' WF WF' oprod_minus_Id oprod_wf wf_subset)
next
case True
thus ?thesis using wf_subset[OF wf_extend_oprod1[OF WF'] oprod_minus_Id1]
- wf_subset[OF wf_extend_oprod2[OF WF] oprod_minus_Id2] by auto
+ wf_subset[OF wf_extend_oprod2[OF WF] oprod_minus_Id2] by auto
qed
lemma oprod_Well_order:
-assumes WELL: "Well_order r" and WELL': "Well_order r'"
-shows "Well_order (r *o r')"
-proof-
- have "Total r \<and> Total r'" using WELL WELL' by (auto simp add: order_on_defs)
- thus ?thesis using assms unfolding well_order_on_def
- using oprod_Linear_order oprod_wf_Id by blast
-qed
+ assumes WELL: "Well_order r" and WELL': "Well_order r'"
+ shows "Well_order (r *o r')"
+ by (meson WELL WELL' linear_order_on_def oprod_Linear_order oprod_wf_Id well_order_on_def)
lemma oprod_embed:
assumes WELL: "Well_order r" and WELL': "Well_order r'" and "r' \<noteq> {}"
@@ -344,14 +313,8 @@
lemma fun_unequal_in_support:
assumes "f \<noteq> g" "f \<in> Func A B" "g \<in> Func A C"
- shows "(support z A f \<union> support z A g) \<inter> {a. f a \<noteq> g a} \<noteq> {}" (is "?L \<inter> ?R \<noteq> {}")
-proof -
- from assms(1) obtain x where x: "f x \<noteq> g x" by blast
- hence "x \<in> ?R" by simp
- moreover from assms(2-3) x have "x \<in> A" unfolding Func_def by fastforce
- with x have "x \<in> ?L" unfolding support_def by auto
- ultimately show ?thesis by auto
-qed
+ shows "(support z A f \<union> support z A g) \<inter> {a. f a \<noteq> g a} \<noteq> {}"
+ using assms by (simp add: Func_def support_def disjoint_iff fun_eq_iff) metis
definition fin_support where
"fin_support z A = {f. finite (support z A f)}"
@@ -381,18 +344,18 @@
begin
definition isMaxim :: "'a set \<Rightarrow> 'a \<Rightarrow> bool"
-where "isMaxim A b \<equiv> b \<in> A \<and> (\<forall>a \<in> A. (a,b) \<in> r)"
+ where "isMaxim A b \<equiv> b \<in> A \<and> (\<forall>a \<in> A. (a,b) \<in> r)"
definition maxim :: "'a set \<Rightarrow> 'a"
-where "maxim A \<equiv> THE b. isMaxim A b"
+ where "maxim A \<equiv> THE b. isMaxim A b"
lemma isMaxim_unique[intro]: "\<lbrakk>isMaxim A x; isMaxim A y\<rbrakk> \<Longrightarrow> x = y"
unfolding isMaxim_def using antisymD[OF ANTISYM, of x y] by auto
lemma maxim_isMaxim: "\<lbrakk>finite A; A \<noteq> {}; A \<subseteq> Field r\<rbrakk> \<Longrightarrow> isMaxim A (maxim A)"
-unfolding maxim_def
+ unfolding maxim_def
proof (rule theI', rule ex_ex1I[OF _ isMaxim_unique, rotated], assumption+,
- induct A rule: finite_induct)
+ induct A rule: finite_induct)
case (insert x A)
thus ?case
proof (cases "A = {}")
@@ -426,9 +389,10 @@
show ?thesis
proof (cases "(x, maxim A) \<in> r")
case True
- with *(2) have "isMaxim (insert x A) (maxim A)" unfolding isMaxim_def
- using transD[OF TRANS, of _ x "maxim A"] by blast
- with *(1) True show ?thesis unfolding max2_def by (metis isMaxim_unique)
+ with *(2) have "isMaxim (insert x A) (maxim A)"
+ by (simp add: isMaxim_def)
+ with *(1) True show ?thesis
+ unfolding max2_def by (metis isMaxim_unique)
next
case False
hence "(maxim A, x) \<in> r" by (metis *(2) assms(3,4) in_mono in_notinI isMaxim_def)
@@ -453,8 +417,8 @@
next
case False
hence "(maxim B, maxim A) \<in> r" by (metis *(2,3) assms(3,6) in_mono in_notinI isMaxim_def)
- with *(2,3) have "isMaxim (A \<union> B) (maxim A)" unfolding isMaxim_def
- using transD[OF TRANS, of _ "maxim B" "maxim A"] by blast
+ with *(2,3) have "isMaxim (A \<union> B) (maxim A)"
+ by (metis "*"(1) False Un_iff isMaxim_def isMaxim_unique)
with *(1) False show ?thesis unfolding max2_def by (metis isMaxim_unique)
qed
qed
@@ -462,7 +426,7 @@
lemma maxim_insert_zero:
assumes "finite A" "A \<noteq> {}" "A \<subseteq> Field r"
shows "maxim (insert zero A) = maxim A"
-using assms zero_in_Field maxim_in[OF assms] by (subst maxim_insert[unfolded max2_def]) auto
+ using assms finite.cases in_mono max2_def maxim_in maxim_insert subset_empty zero_in_Field zero_smallest by fastforce
lemma maxim_equality: "isMaxim A x \<Longrightarrow> maxim A = x"
unfolding maxim_def by (rule the_equality) auto
@@ -495,7 +459,7 @@
locale wo_rel2 =
fixes r s
assumes rWELL: "Well_order r"
- and sWELL: "Well_order s"
+ and sWELL: "Well_order s"
begin
interpretation r: wo_rel r by unfold_locales (rule rWELL)
@@ -510,7 +474,7 @@
lemma max_fun_diff_alt:
"s.max_fun_diff f g = s.maxim ((SUPP f \<union> SUPP g) \<inter> {a. f a \<noteq> g a})"
- unfolding s.max_fun_diff_def fun_diff_alt ..
+ unfolding s.max_fun_diff_def fun_diff_alt ..
lemma isMaxim_max_fun_diff: "\<lbrakk>f \<noteq> g; f \<in> FINFUNC; g \<in> FINFUNC\<rbrakk> \<Longrightarrow>
s.isMaxim {a \<in> Field s. f a \<noteq> g a} (s.max_fun_diff f g)"
@@ -552,13 +516,7 @@
hence "(x, ?fg) \<in> s"
proof (cases "x = ?fg")
case False show ?thesis
- proof (rule ccontr)
- assume "(x, ?fg) \<notin> s"
- with max_fun_diff_in[OF fg f g] x False have *: "(?fg, x) \<in> s" by (blast intro: s.in_notinI)
- hence "f x = g x" by (rule max_fun_diff_le_eq[OF _ fg f g False])
- moreover have "g x = h x" using max_fun_diff_le_eq[OF _ gh g h] False True * by simp
- ultimately show False using x by simp
- qed
+ by (metis (mono_tags, lifting) True assms(5-7) max_fun_diff_max mem_Collect_eq x)
qed (simp add: refl_onD[OF s.REFL])
}
ultimately have "s.isMaxim {a \<in> Field s. f a \<noteq> h a} ?fg"
@@ -572,7 +530,7 @@
case True
hence *: "f ?gh = g ?gh" by (rule max_fun_diff_le_eq[OF _ fg f g *[symmetric]])
hence "s.isMaxim {a \<in> Field s. f a \<noteq> h a} ?gh" using isMaxim_max_fun_diff[OF gh g h]
- isMaxim_max_fun_diff[OF fg f g] transD[OF s.TRANS _ True]
+ isMaxim_max_fun_diff[OF fg f g] transD[OF s.TRANS _ True]
unfolding s.isMaxim_def by auto
hence "?fh = ?gh" using isMaxim_max_fun_diff[OF fh f h] by blast
thus ?thesis using True unfolding s.max2_def by simp
@@ -582,7 +540,7 @@
by (blast intro: s.in_notinI)
hence *: "g ?fg = h ?fg" by (rule max_fun_diff_le_eq[OF _ gh g h *])
hence "s.isMaxim {a \<in> Field s. f a \<noteq> h a} ?fg" using isMaxim_max_fun_diff[OF gh g h]
- isMaxim_max_fun_diff[OF fg f g] True transD[OF s.TRANS, of _ _ ?fg]
+ isMaxim_max_fun_diff[OF fg f g] True transD[OF s.TRANS, of _ _ ?fg]
unfolding s.isMaxim_def by auto
hence "?fh = ?fg" using isMaxim_max_fun_diff[OF fh f h] by blast
thus ?thesis using False unfolding s.max2_def by simp
@@ -603,8 +561,8 @@
proof (unfold trans_def, safe)
fix f g h :: "'b \<Rightarrow> 'a"
let ?fg = "s.max_fun_diff f g"
- and ?gh = "s.max_fun_diff g h"
- and ?fh = "s.max_fun_diff f h"
+ and ?gh = "s.max_fun_diff g h"
+ and ?fh = "s.max_fun_diff f h"
assume oexp: "(f, g) \<in> oexp" "(g, h) \<in> oexp"
thus "(f, h) \<in> oexp"
proof (cases "f = g \<or> g = h")
@@ -619,8 +577,8 @@
proof (cases "?fg = ?gh \<longrightarrow> f ?fg \<noteq> h ?gh")
case True
show ?thesis using max_fun_diff_max2[of f g h, OF True] * \<open>f \<noteq> h\<close> max_fun_diff_in
- r.max2_iff[OF FINFUNCD FINFUNCD] r.max2_equals1[OF FINFUNCD FINFUNCD] max_fun_diff_le_eq
- s.in_notinI[OF disjI1] unfolding oexp_def Let_def s.max2_def mem_Collect_eq by safe metis
+ r.max2_iff[OF FINFUNCD FINFUNCD] r.max2_equals1[OF FINFUNCD FINFUNCD] max_fun_diff_le_eq
+ s.in_notinI[OF disjI1] unfolding oexp_def Let_def s.max2_def mem_Collect_eq by safe metis
next
case False with * show ?thesis unfolding oexp_def Let_def
using antisymD[OF r.ANTISYM, of "g ?gh" "h ?gh"] max_fun_diff_in[of g h] by auto
@@ -667,13 +625,7 @@
lemma const_least:
assumes "Field r \<noteq> {}" "f \<in> FINFUNC"
shows "(const, f) \<in> oexp"
-proof (cases "f = const")
- case True thus ?thesis using refl_onD[OF oexp_Refl] assms(2) unfolding Field_oexp by auto
-next
- case False
- with assms show ?thesis using max_fun_diff_in[of f const]
- unfolding oexp_def Let_def by (auto intro: r.zero_smallest FinFuncD simp: s.max_fun_diff_commute)
-qed
+ using assms const_FINFUNC max_fun_diff max_fun_diff_in oexp_def by fastforce
lemma support_not_const:
assumes "F \<subseteq> FINFUNC" and "const \<notin> F"
@@ -693,15 +645,15 @@
qed
lemma maxim_isMaxim_support:
- assumes f: "F \<subseteq> FINFUNC" and "const \<notin> F"
+ assumes "F \<subseteq> FINFUNC" and "const \<notin> F"
shows "\<forall>f \<in> F. s.isMaxim (SUPP f) (s.maxim (SUPP f))"
- using support_not_const[OF assms] by (auto intro!: s.maxim_isMaxim)
+ using assms s.maxim_isMaxim support_not_const by force
lemma oexp_empty2: "Field s = {} \<Longrightarrow> oexp = {(\<lambda>x. undefined, \<lambda>x. undefined)}"
unfolding oexp_def FinFunc_def fin_support_def support_def by auto
lemma oexp_empty: "\<lbrakk>Field r = {}; Field s \<noteq> {}\<rbrakk> \<Longrightarrow> oexp = {}"
- unfolding oexp_def FinFunc_def Let_def by auto
+ using FINFUNCD oexp_def by auto
lemma fun_upd_FINFUNC: "\<lbrakk>f \<in> FINFUNC; x \<in> Field s; y \<in> Field r\<rbrakk> \<Longrightarrow> f(x := y) \<in> FINFUNC"
unfolding FinFunc_def Func_def fin_support_def
@@ -734,7 +686,7 @@
have const[simp]: "\<And>F. \<lbrakk>const \<in> F; F \<subseteq> FINFUNC\<rbrakk> \<Longrightarrow> \<exists>f0\<in>F. \<forall>f\<in>F. (f0, f) \<in> oexp"
using const_least[OF Fields(2)] by auto
show ?thesis
- unfolding Linear_order_wf_diff_Id[OF oexp_Linear_order] Field_oexp
+ unfolding Linear_order_wf_diff_Id[OF oexp_Linear_order] Field_oexp
proof (intro allI impI)
fix A assume A: "A \<subseteq> FINFUNC" "A \<noteq> {}"
{ fix y F
@@ -758,7 +710,7 @@
hence zField: "z \<in> Field s" unfolding Field_def by auto
define x0 where "x0 = r.minim {f z | f. f \<in> F \<and> z = s.maxim (SUPP f)}"
from F(1,2) maxF(1) SUPPF zmin
- have x0min: "r.isMinim {f z | f. f \<in> F \<and> z = s.maxim (SUPP f)} x0"
+ have x0min: "r.isMinim {f z | f. f \<in> F \<and> z = s.maxim (SUPP f)} x0"
unfolding x0_def s.isMaxim_def s.isMinim_def
by (blast intro!: r.minim_isMinim FinFuncD[of _ r s])
with maxF(1) SUPPF F(1) have x0Field: "x0 \<in> Field r"
@@ -770,13 +722,8 @@
from zmin x0min have "G \<noteq> {}" unfolding G_def z_def s.isMinim_def r.isMinim_def by blast
have GF: "G \<subseteq> (\<lambda>f. f(z := r.zero)) ` F" unfolding G_def by auto
have "G \<subseteq> fin_support r.zero (Field s)"
- unfolding FinFunc_def fin_support_def proof safe
- fix g assume "g \<in> G"
- with GF obtain f where f: "f \<in> F" "g = f(z := r.zero)" by auto
- with SUPPF have "finite (SUPP f)" by blast
- with f show "finite (SUPP g)"
- by (elim finite_subset[rotated]) (auto simp: support_def)
- qed
+ unfolding FinFunc_def fin_support_def
+ using F(1) FinFunc_def G_def fin_support_def by fastforce
moreover from F GF zField have "G \<subseteq> Func (Field s) (Field r)"
using Func_upd[of _ "Field s" "Field r" z r.zero] unfolding FinFunc_def by auto
ultimately have G: "G \<subseteq> FINFUNC" unfolding FinFunc_def by blast
@@ -799,7 +746,7 @@
unfolding z by (intro s.maxim_mono) auto
}
moreover from y'min have "\<And>g. g \<in> G \<Longrightarrow> (y', s.maxim (SUPP g)) \<in> s"
- unfolding s.isMinim_def by auto
+ unfolding s.isMinim_def by auto
ultimately have "y' \<noteq> z" "(y', z) \<in> s" using maxG
unfolding s.isMinim_def s.isMaxim_def by auto
with zy have "y' \<noteq> y" "(y', y) \<in> s" using antisymD[OF s.ANTISYM] transD[OF s.TRANS]
@@ -814,7 +761,7 @@
with x0notzero zField have SUPP: "SUPP f0 = SUPP g0 \<union> {z}" unfolding support_def by auto
from g0z have f0z: "f0(z := r.zero) = g0" unfolding f0_def fun_upd_upd by auto
have f0: "f0 \<in> F" using x0min g0(1)
- Func_elim[OF subsetD[OF subset_trans[OF F(1)[unfolded FinFunc_def] Int_lower1]] zField]
+ Func_elim[OF subsetD[OF subset_trans[OF F(1)[unfolded FinFunc_def] Int_lower1]] zField]
unfolding f0_def r.isMinim_def G_def by (force simp: fun_upd_idem)
from g0(1) maxF(1) have maxf0: "s.maxim (SUPP f0) = z" unfolding SUPP G_def
by (intro s.maxim_equality) (auto simp: s.isMaxim_def)
@@ -834,7 +781,7 @@
hence oexp: "(f0(z := r.zero, z := x0), f(z := r.zero, z := x0)) \<in> oexp"
by (elim fun_upd_same_oexp[OF _ _ zField x0Field]) simp
with f F(1) x0min True
- have "(f(z := x0), f) \<in> oexp" unfolding G_def r.isMinim_def
+ have "(f(z := x0), f) \<in> oexp" unfolding G_def r.isMinim_def
by (intro fun_upd_smaller_oexp[OF _ zField x0Field]) auto
with oexp show ?thesis using transD[OF oexp_trans, of f0 "f(z := x0)" f]
unfolding f0_def by auto
@@ -868,12 +815,12 @@
have "f (s.maxim (SUPP f)) \<noteq> r.zero"
using bspec[OF maxF(1) f, unfolded s.isMaxim_def] by (auto simp: support_def)
with f0f * f f0 maxf0 SUPPF
- have "s.max_fun_diff f0 f = s.maxim (SUPP f0 \<union> SUPP f)"
+ have "s.max_fun_diff f0 f = s.maxim (SUPP f0 \<union> SUPP f)"
unfolding max_fun_diff_alt using s.maxim_Un[of "SUPP f0" "SUPP f"]
by (intro s.maxim_Int) (auto simp: s.max2_def)
moreover have "s.maxim (SUPP f0 \<union> SUPP f) = s.maxim (SUPP f)"
- using s.maxim_Un[of "SUPP f0" "SUPP f"] * maxf0 SUPPF f0 f
- by (auto simp: s.max2_def)
+ using s.maxim_Un[of "SUPP f0" "SUPP f"] * maxf0 SUPPF f0 f
+ by (auto simp: s.max2_def)
ultimately show ?thesis using f f0 F(1) maxF(1) SUPPF unfolding oexp_def Let_def
by (fastforce simp: s.isMaxim_def intro!: r.zero_smallest FINFUNCD)
qed
@@ -883,13 +830,9 @@
qed simp
qed
qed
- } note * = mp[OF this]
- from A(2) obtain f where f: "f \<in> A" by blast
- with A(1) show "\<exists>a\<in>A. \<forall>a'\<in>A. (a, a') \<in> oexp"
- proof (cases "f = const")
- case False with f A(1) show ?thesis using maxim_isMaxim_support[of "{f}"]
- by (intro *[of _ "s.maxim (SUPP f)"]) (auto simp: s.isMaxim_def support_def)
- qed simp
+ }
+ with A show "\<exists>a\<in>A. \<forall>a'\<in>A. (a, a') \<in> oexp"
+ by blast
qed
qed
@@ -899,8 +842,7 @@
interpretation o: wo_rel oexp by unfold_locales (rule oexp_Well_order)
lemma zero_oexp: "Field r \<noteq> {} \<Longrightarrow> o.zero = const"
- by (rule sym[OF o.leq_zero_imp[OF const_least]])
- (auto intro!: o.zero_in_Field[unfolded Field_oexp] dest!: const_FINFUNC)
+ by (metis Field_oexp const_FINFUNC const_least o.Field_ofilter o.equals_minim o.ofilter_def o.zero_def)
end
@@ -925,8 +867,8 @@
by (auto dest: well_order_on_domain)
lemma ozero_ordLeq:
-assumes "Well_order r" shows "ozero \<le>o r"
-using assms unfolding ozero_def ordLeq_def embed_def[abs_def] under_def by auto
+ assumes "Well_order r" shows "ozero \<le>o r"
+ using assms unfolding ozero_def ordLeq_def embed_def[abs_def] under_def by auto
definition "oone = {((),())}"
@@ -985,8 +927,8 @@
lemma osum_cong:
assumes "t =o u" and "r =o s"
shows "t +o r =o u +o s"
-using ordIso_transitive[OF osum_congL[OF assms(1)] osum_congR[OF assms(2)]]
- assms[unfolded ordIso_def] by auto
+ using ordIso_transitive[OF osum_congL[OF assms(1)] osum_congR[OF assms(2)]]
+ assms[unfolded ordIso_def] by auto
lemma Well_order_empty[simp]: "Well_order {}"
unfolding Field_empty by (rule well_order_on_empty)
@@ -1005,8 +947,8 @@
shows "{} ^o r = {}"
proof -
from assms(2) have "Field r \<noteq> {}" unfolding Field_def by auto
- thus ?thesis unfolding oexp_def[OF Well_order_empty assms(1)] FinFunc_def fin_support_def support_def
- by auto
+ thus ?thesis
+ by (simp add: assms(1) wo_rel2.intro wo_rel2.oexp_empty)
qed
lemma oprod_zero[simp]: "{} *o r = {}" "r *o {} = {}"
@@ -1051,8 +993,8 @@
lemma oprod_cong:
assumes "t =o u" and "r =o s"
shows "t *o r =o u *o s"
-using ordIso_transitive[OF oprod_congL[OF assms(1)] oprod_congR[OF assms(2)]]
- assms[unfolded ordIso_def] by auto
+ using ordIso_transitive[OF oprod_congL[OF assms(1)] oprod_congR[OF assms(2)]]
+ assms[unfolded ordIso_def] by auto
lemma Field_singleton[simp]: "Field {(z,z)} = {z}"
by (metis well_order_on_Field well_order_on_singleton)
@@ -1155,7 +1097,7 @@
let ?f = "map_sum f id"
from f have "\<forall>a\<in>Field (r +o t).
?f a \<in> Field (s +o t) \<and> ?f ` underS (r +o t) a \<subseteq> underS (s +o t) (?f a)"
- unfolding Field_osum underS_def by (fastforce simp: osum_def)
+ unfolding Field_osum underS_def by (fastforce simp: osum_def)
thus ?thesis unfolding ordLeq_def2 by (auto intro: osum_Well_order r s t)
qed
@@ -1224,7 +1166,7 @@
let ?f = "map_prod f id"
from f have "\<forall>a\<in>Field (r *o t).
?f a \<in> Field (s *o t) \<and> ?f ` underS (r *o t) a \<subseteq> underS (s *o t) (?f a)"
- unfolding Field_oprod underS_def unfolding map_prod_def oprod_def by auto
+ unfolding Field_oprod underS_def unfolding map_prod_def oprod_def by auto
thus ?thesis unfolding ordLeq_def2 by (auto intro: oprod_Well_order r s t)
qed
@@ -1266,8 +1208,7 @@
qed
lemma ozero_oexp: "\<not> (s =o ozero) \<Longrightarrow> ozero ^o s =o ozero"
- unfolding oexp_def[OF ozero_Well_order s] FinFunc_def
- by simp (metis Func_emp2 bot.extremum_uniqueI emptyE well_order_on_domain s subrelI)
+ by (fastforce simp add: oexp_def[OF ozero_Well_order s] FinFunc_def Func_def intro: FieldI1)
lemma oone_oexp: "oone ^o s =o oone" (is "?L =o ?R")
by (rule oone_ordIso_oexp[OF ordIso_reflexive[OF oone_Well_order] s])
@@ -1315,17 +1256,17 @@
"let m = s.max_fun_diff g h in (g m, h m) \<in> r"
hence "g \<noteq> h" by auto
note max_fun_diff_in = rs.max_fun_diff_in[OF \<open>g \<noteq> h\<close> gh(1,2)]
- and max_fun_diff_max = rs.max_fun_diff_max[OF \<open>g \<noteq> h\<close> gh(1,2)]
+ and max_fun_diff_max = rs.max_fun_diff_max[OF \<open>g \<noteq> h\<close> gh(1,2)]
with *(4) invff *(2) have "t.max_fun_diff (F g) (F h) = f (s.max_fun_diff g h)"
unfolding t.max_fun_diff_def compat_def
by (intro t.maxim_equality) (auto simp: t.isMaxim_def F_def dest: injfD)
with gh invff max_fun_diff_in
- show "let m = t.max_fun_diff (F g) (F h) in (F g m, F h m) \<in> r"
+ show "let m = t.max_fun_diff (F g) (F h) in (F g m, F h m) \<in> r"
unfolding F_def Let_def by (auto simp: dest: injfD)
qed
moreover
from FLR have "ofilter ?R (F ` Field ?L)"
- unfolding rexpt.ofilter_def under_def rs.Field_oexp rt.Field_oexp unfolding rt.oexp_def
+ unfolding rexpt.ofilter_def under_def rs.Field_oexp rt.Field_oexp unfolding rt.oexp_def
proof (safe elim!: imageI)
fix g h assume gh: "g \<in> FinFunc r s" "h \<in> FinFunc r t" "F g \<in> FinFunc r t"
"let m = t.max_fun_diff h (F g) in (h m, F g m) \<in> r"
@@ -1345,13 +1286,13 @@
proof (rule ccontr)
assume "(t.max_fun_diff h (F g), z) \<notin> t"
hence "(z, t.max_fun_diff h (F g)) \<in> t" using t.in_notinI[of "t.max_fun_diff h (F g)" z]
- z max_Field by auto
+ z max_Field by auto
hence "z \<in> f ` Field s" using *(3) max_f_Field unfolding t.ofilter_def under_def
by fastforce
with z show False by blast
qed
hence "h z = r.zero" using rt.max_fun_diff_le_eq[OF _ False gh(2,3), of z]
- z max_f_Field unfolding F_def by auto
+ z max_f_Field unfolding F_def by auto
} note ** = this
with *(3) gh(2) have "h = F (\<lambda>x. if x \<in> Field s then h (f x) else undefined)" using invff
unfolding F_def fun_eq_iff FinFunc_def Func_def Let_def t.ofilter_def under_def by auto
@@ -1437,8 +1378,8 @@
by (subst t.max_fun_diff_def, intro t.maxim_equality)
(auto simp: t.isMaxim_def intro: inj_onD[OF inj] intro!: rt.max_fun_diff_max)
with Field_fg Field_fh hg fz f_underS compat neq have "(?f h, ?f g) \<in> st.oexp"
- using rt.max_fun_diff[OF \<open>h \<noteq> g\<close>] rt.max_fun_diff_in[OF \<open>h \<noteq> g\<close>] unfolding st.Field_oexp
- unfolding rt.oexp_def st.oexp_def Let_def compat_def by auto
+ using rt.max_fun_diff[OF \<open>h \<noteq> g\<close>] rt.max_fun_diff_in[OF \<open>h \<noteq> g\<close>] unfolding st.Field_oexp
+ unfolding rt.oexp_def st.oexp_def Let_def compat_def by auto
with neq show "?f h \<in> underS (s ^o t) (?f g)" unfolding underS_def by auto
qed
ultimately have "?f g \<in> Field (s ^o t) \<and> ?f ` underS (r ^o t) g \<subseteq> underS (s ^o t) (?f g)"
@@ -1460,7 +1401,7 @@
x: "x \<in> Field r" "r.zero \<in> Field r" "x \<noteq> r.zero"
unfolding ordLess_def oone_def embedS_def[abs_def] bij_betw_def embed_def under_def
by (auto simp: image_def)
- (metis (lifting) equals0D mem_Collect_eq r.zero_in_Field singletonI)
+ (metis (lifting) equals0D mem_Collect_eq r.zero_in_Field singletonI)
let ?f = "\<lambda>a b. if b \<in> Field s then if b = a then x else r.zero else undefined"
from x(3) have SUPP: "\<And>y. y \<in> Field s \<Longrightarrow> rs.SUPP (?f y) = {y}" unfolding support_def by auto
{ fix y assume y: "y \<in> Field s"
@@ -1553,7 +1494,7 @@
interpret rt: wo_rel2 r t by unfold_locales (rule r, rule t)
let ?f = "\<lambda>(f, g). case_sum f g"
have "bij_betw ?f (Field ?L) (Field ?R)"
- unfolding bij_betw_def rst.Field_oexp rs.Field_oexp rt.Field_oexp Field_oprod proof (intro conjI)
+ unfolding bij_betw_def rst.Field_oexp rs.Field_oexp rt.Field_oexp Field_oprod proof (intro conjI)
show "inj_on ?f (FinFunc r s \<times> FinFunc r t)" unfolding inj_on_def
by (auto simp: fun_eq_iff split: sum.splits)
show "?f ` (FinFunc r s \<times> FinFunc r t) = FinFunc r (s +o t)"
@@ -1567,7 +1508,7 @@
moreover have "compat ?L ?R ?f"
unfolding compat_def rst.Field_oexp rs.Field_oexp rt.Field_oexp oprod_def
unfolding rst.oexp_def Let_def rs.oexp_def rt.oexp_def
- by (fastforce simp: Field_osum FinFunc_osum o_def split: sum.splits
+ by (fastforce simp: Field_osum FinFunc_osum o_def split: sum.splits
dest: max_fun_diff_eq_Inl max_fun_diff_eq_Inr)
ultimately have "iso ?L ?R ?f" using r s t
by (subst iso_iff3) (auto intro: oexp_Well_order oprod_Well_order osum_Well_order)
@@ -1638,8 +1579,8 @@
interpret rs: wo_rel2 r s by unfold_locales (rule r, rule s)
interpret rst: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
from fun_unequal_in_support[OF assms(2), of "Field (s *o t)" "Field r" "Field r"] assms(3,4)
- have diff1: "rev_curr f \<noteq> rev_curr g"
- "rev_curr f \<in> FinFunc (r ^o s) t" "rev_curr g \<in> FinFunc (r ^o s) t" using rev_curr_FinFunc[OF Field]
+ have diff1: "rev_curr f \<noteq> rev_curr g"
+ "rev_curr f \<in> FinFunc (r ^o s) t" "rev_curr g \<in> FinFunc (r ^o s) t" using rev_curr_FinFunc[OF Field]
unfolding fun_eq_iff rev_curr_def[abs_def] FinFunc_def support_def Field_oprod
by auto fast
hence diff2: "rev_curr f m \<noteq> rev_curr g m" "rev_curr f m \<in> FinFunc r s" "rev_curr g m \<in> FinFunc r s"
@@ -1653,7 +1594,7 @@
next
assume "f (s.max_fun_diff (rev_curr f m) (rev_curr g m), m) =
g (s.max_fun_diff (rev_curr f m) (rev_curr g m), m)"
- (is "f (?x, m) = g (?x, m)")
+ (is "f (?x, m) = g (?x, m)")
hence "rev_curr f m ?x = rev_curr g m ?x" unfolding rev_curr_def by auto
with rs.max_fun_diff[OF diff2] show False by auto
next
@@ -1674,14 +1615,14 @@
proof (cases "s = {} \<or> t = {}")
case True with \<open>r = {}\<close> show ?thesis
by (auto simp: oexp_empty[OF oexp_Well_order[OF Well_order_empty s]]
- intro!: ordIso_transitive[OF ordIso_symmetric[OF oone_ordIso] oone_ordIso]
+ intro!: ordIso_transitive[OF ordIso_symmetric[OF oone_ordIso] oone_ordIso]
ordIso_transitive[OF oone_ordIso_oexp[OF ordIso_symmetric[OF oone_ordIso] t] oone_ordIso])
next
- case False
- hence "s *o t \<noteq> {}" unfolding oprod_def Field_def by fastforce
- with False show ?thesis
- using \<open>r = {}\<close> ozero_ordIso
- by (auto simp add: s t oprod_Well_order ozero_def)
+ case False
+ hence "s *o t \<noteq> {}" unfolding oprod_def Field_def by fastforce
+ with False show ?thesis
+ using \<open>r = {}\<close> ozero_ordIso
+ by (auto simp add: s t oprod_Well_order ozero_def)
qed
next
case False
@@ -1692,7 +1633,7 @@
interpret rs: wo_rel2 r s by unfold_locales (rule r, rule s)
interpret rst: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
have bij: "bij_betw rev_curr (Field ?L) (Field ?R)"
- unfolding bij_betw_def r_st.Field_oexp rst.Field_oexp Field_oprod proof (intro conjI)
+ unfolding bij_betw_def r_st.Field_oexp rst.Field_oexp Field_oprod proof (intro conjI)
show "inj_on rev_curr (FinFunc r (s *o t))"
unfolding inj_on_def FinFunc_def Func_def Field_oprod rs.Field_oexp rev_curr_def[abs_def]
by (auto simp: fun_eq_iff) metis
@@ -1700,16 +1641,16 @@
qed
moreover
have "compat ?L ?R rev_curr"
- unfolding compat_def proof safe
+ unfolding compat_def proof safe
fix fg1 fg2 assume fg: "(fg1, fg2) \<in> r ^o (s *o t)"
show "(rev_curr fg1, rev_curr fg2) \<in> r ^o s ^o t"
proof (cases "fg1 = fg2")
assume "fg1 \<noteq> fg2"
with fg show ?thesis
- using rst.max_fun_diff_in[of "rev_curr fg1" "rev_curr fg2"]
- max_fun_diff_oprod[OF Field, of fg1 fg2] rev_curr_FinFunc[OF Field, symmetric]
- unfolding r_st.Field_oexp rs.Field_oexp rst.Field_oexp unfolding r_st.oexp_def rst.oexp_def
- by (auto simp: rs.oexp_def Let_def) (auto simp: rev_curr_def[abs_def])
+ using rst.max_fun_diff_in[of "rev_curr fg1" "rev_curr fg2"]
+ max_fun_diff_oprod[OF Field, of fg1 fg2] rev_curr_FinFunc[OF Field, symmetric]
+ unfolding r_st.Field_oexp rs.Field_oexp rst.Field_oexp unfolding r_st.oexp_def rst.oexp_def
+ by (auto simp: rs.oexp_def Let_def) (auto simp: rev_curr_def[abs_def])
next
assume "fg1 = fg2"
with fg bij show ?thesis unfolding r_st.Field_oexp rs.Field_oexp rst.Field_oexp bij_betw_def
--- a/src/HOL/Cardinals/Wellorder_Constructions.thy Fri Jan 13 11:05:48 2023 +0000
+++ b/src/HOL/Cardinals/Wellorder_Constructions.thy Fri Jan 13 16:19:56 2023 +0000
@@ -93,12 +93,7 @@
lemma ofilter_ordLeq:
assumes "Well_order r" and "ofilter r A"
shows "Restr r A \<le>o r"
-proof-
- have "A \<le> Field r" using assms by (auto simp add: wo_rel_def wo_rel.ofilter_def)
- thus ?thesis using assms
- by (simp add: ofilter_subset_ordLeq wo_rel.Field_ofilter
- wo_rel_def Restr_Field)
-qed
+by (metis assms inf.orderE ofilter_embed ofilter_subset_ordLeq refl_on_def wo_rel.Field_ofilter wo_rel.REFL wo_rel.intro)
corollary under_Restr_ordLeq:
"Well_order r \<Longrightarrow> Restr r (under r a) \<le>o r"
@@ -122,20 +117,7 @@
using assms unfolding dir_image_def inj_on_def by auto
next
show "(dir_image r1 f) Int (dir_image r2 f) \<le> dir_image (r1 Int r2) f"
- proof(clarify)
- fix a' b'
- assume "(a',b') \<in> dir_image r1 f" "(a',b') \<in> dir_image r2 f"
- then obtain a1 b1 a2 b2
- where 1: "a' = f a1 \<and> b' = f b1 \<and> a' = f a2 \<and> b' = f b2" and
- 2: "(a1,b1) \<in> r1 \<and> (a2,b2) \<in> r2" and
- 3: "{a1,b1} \<le> Field r1 \<and> {a2,b2} \<le> Field r2"
- unfolding dir_image_def Field_def by blast
- hence "a1 = a2 \<and> b1 = b2" using assms unfolding inj_on_def by auto
- hence "a' = f a1 \<and> b' = f b1 \<and> (a1,b1) \<in> r1 Int r2 \<and> (a2,b2) \<in> r1 Int r2"
- using 1 2 by auto
- thus "(a',b') \<in> dir_image (r1 \<inter> r2) f"
- unfolding dir_image_def by blast
- qed
+ by (clarsimp simp: dir_image_def) (metis FieldI1 FieldI2 UnCI assms inj_on_def)
qed
(* More facts on ordinal sum: *)
@@ -154,21 +136,8 @@
have "inj_on id (Field r)" by simp
moreover
have "ofilter (r Osum r') (Field r)"
- using 1 proof(auto simp add: wo_rel_def wo_rel.ofilter_def
- Field_Osum under_def)
- fix a b assume 2: "a \<in> Field r" and 3: "(b,a) \<in> r Osum r'"
- moreover
- {assume "(b,a) \<in> r'"
- hence "a \<in> Field r'" using Field_def[of r'] by blast
- hence False using 2 FLD by blast
- }
- moreover
- {assume "a \<in> Field r'"
- hence False using 2 FLD by blast
- }
- ultimately
- show "b \<in> Field r" by (auto simp add: Osum_def Field_def)
- qed
+ using 1 FLD
+ by (auto simp add: wo_rel_def wo_rel.ofilter_def Osum_def under_def Field_iff disjoint_iff)
ultimately show ?thesis
using assms by (auto simp add: embed_iff_compat_inj_on_ofilter)
qed
@@ -237,8 +206,8 @@
show "\<exists>p'. (isOmax ?R' p')"
proof(cases "R = {}")
case True
- thus ?thesis unfolding isOmax_def using ***
- by (simp add: ordLeq_reflexive)
+ thus ?thesis
+ by (simp add: "***" isOmax_def ordLeq_reflexive)
next
case False
then obtain p where p: "isOmax R p" using IH by auto
@@ -249,14 +218,9 @@
}
moreover
{assume Case22: "p \<le>o r"
- {fix r' assume "r' \<in> ?R'"
- moreover
- {assume "r' \<in> R"
- hence "r' \<le>o p" using p unfolding isOmax_def by simp
- hence "r' \<le>o r" using Case22 by(rule ordLeq_transitive)
- }
- moreover have "r \<le>o r" using *** by(rule ordLeq_reflexive)
- ultimately have "r' \<le>o r" by auto
+ { fix r' assume "r' \<in> ?R'"
+ then have "r' \<le>o r"
+ by (metis "***" Case22 insert_iff isOmax_def ordLeq_transitive p ordLeq_reflexive)
}
hence "isOmax ?R' r" unfolding isOmax_def by simp
hence ?thesis by auto
@@ -374,7 +338,8 @@
by simp (metis REFL in_mono max2_def max2_greater refl_on_domain)
have "(supr A, b) \<in> r"
by (simp add: "0" A bb supr_least)
- thus False using bA unfolding underS_def by simp (metis ANTISYM antisymD)
+ thus False
+ by (metis antisymD bA underS_E wo_rel.ANTISYM wo_rel_axioms)
qed
lemma underS_suc:
@@ -387,17 +352,15 @@
by (metis bb in_mono max2_def max2_greater mem_Collect_eq underS_I under_def)
have "(suc A, b) \<in> r"
by (metis "0" A bb suc_least underS_E)
- thus False using bA unfolding underS_def by simp (metis ANTISYM antisymD)
+ thus False
+ by (metis antisymD bA underS_E wo_rel.ANTISYM wo_rel_axioms)
qed
lemma (in wo_rel) in_underS_supr:
assumes j: "j \<in> underS i" and i: "i \<in> A" and A: "A \<subseteq> Field r" and AA: "Above A \<noteq> {}"
shows "j \<in> underS (supr A)"
-proof-
- have "(i,supr A) \<in> r" using supr_greater[OF A AA i] .
- thus ?thesis using j unfolding underS_def
- by simp (metis REFL TRANS max2_def max2_equals1 refl_on_domain transD)
-qed
+ using supr_greater[OF A AA i]
+ by (metis FieldI1 j max2_equals1 max2_equals2 max2_iff underS_E underS_I)
lemma inj_on_Field:
assumes A: "A \<subseteq> Field r" and f: "\<And> a b. \<lbrakk>a \<in> A; b \<in> A; a \<in> underS b\<rbrakk> \<Longrightarrow> f a \<noteq> f b"
@@ -412,29 +375,13 @@
lemma underS_init_seg_of_Collect:
assumes "\<And>j1 j2. \<lbrakk>j2 \<in> underS i; (j1, j2) \<in> r\<rbrakk> \<Longrightarrow> R j1 initial_segment_of R j2"
shows "{R j |j. j \<in> underS i} \<in> Chains init_seg_of"
- unfolding Chains_def proof safe
- fix j ja assume jS: "j \<in> underS i" and jaS: "ja \<in> underS i"
- and init: "(R ja, R j) \<notin> init_seg_of"
- hence jja: "{j,ja} \<subseteq> Field r" and j: "j \<in> Field r" and ja: "ja \<in> Field r"
- and jjai: "(j,i) \<in> r" "(ja,i) \<in> r"
- and i: "i \<notin> {j,ja}" unfolding Field_def underS_def by auto
- have jj: "(j,j) \<in> r" and jaja: "(ja,ja) \<in> r" using j ja by (metis in_notinI)+
- show "R j initial_segment_of R ja"
- using jja init TOTALS assms jS jaS by auto
-qed
+ using TOTALS assms
+ by (clarsimp simp: Chains_def) (meson BNF_Least_Fixpoint.underS_Field)
lemma (in wo_rel) Field_init_seg_of_Collect:
assumes "\<And>j1 j2. \<lbrakk>j2 \<in> Field r; (j1, j2) \<in> r\<rbrakk> \<Longrightarrow> R j1 initial_segment_of R j2"
shows "{R j |j. j \<in> Field r} \<in> Chains init_seg_of"
- unfolding Chains_def proof safe
- fix j ja assume jS: "j \<in> Field r" and jaS: "ja \<in> Field r"
- and init: "(R ja, R j) \<notin> init_seg_of"
- hence jja: "{j,ja} \<subseteq> Field r" and j: "j \<in> Field r" and ja: "ja \<in> Field r"
- unfolding Field_def underS_def by auto
- have jj: "(j,j) \<in> r" and jaja: "(ja,ja) \<in> r" using j ja by (metis in_notinI)+
- show "R j initial_segment_of R ja"
- using TOTALS assms init jS jaS by blast
-qed
+ using TOTALS assms by (auto simp: Chains_def)
subsubsection \<open>Successor and limit elements of an ordinal\<close>
@@ -448,8 +395,7 @@
lemma zero_smallest[simp]:
assumes "j \<in> Field r" shows "(zero, j) \<in> r"
- unfolding zero_def
- by (metis AboveS_Field assms subset_AboveS_UnderS subset_antisym subset_refl suc_def suc_least_AboveS)
+ by (simp add: assms wo_rel.ofilter_linord wo_rel_axioms zero_def)
lemma zero_in_Field: assumes "Field r \<noteq> {}" shows "zero \<in> Field r"
using assms unfolding zero_def by (metis Field_ofilter minim_in ofilter_def)
@@ -496,8 +442,7 @@
lemma succ_smallest:
assumes "(i,j) \<in> r" and "i \<noteq> j"
shows "(succ i, j) \<in> r"
- unfolding succ_def apply(rule suc_least)
- using assms unfolding Field_def by auto
+ by (metis Field_iff assms empty_subsetI insert_subset singletonD suc_least succ_def)
lemma isLim_supr:
assumes f: "i \<in> Field r" and l: "isLim i"
@@ -755,44 +700,19 @@
moreover have "f a1 \<in> underS s (f a)" using f[OF a] a1 by auto
ultimately have "g a1 \<in> underS s (f a)" by (metis s.ANTISYM s.TRANS under_underS_trans)
}
- hence "f a \<in> AboveS s (g ` underS r a)" unfolding AboveS_def
+ hence fa_in: "f a \<in> AboveS s (g ` underS r a)" unfolding AboveS_def
using fa by simp (metis (lifting, full_types) mem_Collect_eq underS_def)
hence A: "AboveS s (g ` underS r a) \<noteq> {}" by auto
- have B: "\<And> a1. a1 \<in> underS r a \<Longrightarrow> g a1 \<in> underS s (g a)"
- unfolding g apply(rule s.suc_underS[OF A0 A]) by auto
- {fix a1 a2 assume a2: "a2 \<in> underS r a" and 1: "a1 \<in> underS r a2"
- hence a12: "{a1,a2} \<subseteq> under r a2" and "a1 \<noteq> a2" using r.REFL a
- unfolding underS_def under_def refl_on_def Field_def by auto
- hence "g a1 \<noteq> g a2" using IH1a[OF a2] unfolding inj_on_def by auto
- hence "g a1 \<in> underS s (g a2)" using IH1b[OF a2] a12
- unfolding underS_def under_def by auto
- } note C = this
have ga: "g a \<in> Field s" unfolding g using s.suc_inField[OF A0 A] .
- have aa: "a \<in> under r a"
- using a r.REFL unfolding under_def underS_def refl_on_def by auto
- show ?case proof safe
- show "bij_betw g (under r a) (under s (g a))" unfolding bij_betw_def proof safe
- show "inj_on g (under r a)"
- by (metis A IH1a IH1b a bij_betw_def g ga r s s.suc_greater subsetI wellorders_totally_ordered_aux)
- next
- fix a1 assume a1: "a1 \<in> under r a"
- show "g a1 \<in> under s (g a)"
- by (metis (mono_tags, lifting) B a1 ga mem_Collect_eq s.in_notinI underS_def under_def)
- next
- fix b1 assume b1: "b1 \<in> under s (g a)"
- show "b1 \<in> g ` under r a"
- proof(cases "b1 = g a")
- case True thus ?thesis using aa by auto
- next
- case False
- show ?thesis
- by (metis b1 A IH1a IH1b a bij_betw_def g ga r s s.suc_greater subsetI wellorders_totally_ordered_aux)
- qed
- qed
- next
- have "(g a, f a) \<in> s" unfolding g
- using \<open>f a \<in> s.AboveS (g ` r.underS a)\<close> s.suc_least_AboveS by blast
- thus "g a \<in> under s (f a)" unfolding under_def by auto
+ show ?case
+ unfolding bij_betw_def
+ proof (intro conjI)
+ show "inj_on g (r.under a)"
+ by (metis A IH1a IH1b a bij_betw_def g ga r s s.suc_greater subsetI wellorders_totally_ordered_aux)
+ show "g ` r.under a = s.under (g a)"
+ by (metis A A0 IH1a IH1b a bij_betw_def g ga r s s.suc_greater wellorders_totally_ordered_aux)
+ show "g a \<in> s.under (f a)"
+ by (simp add: fa_in g s.suc_least_AboveS under_def)
qed
qed
}
@@ -808,8 +728,7 @@
lemma iso_oproj:
assumes r: "Well_order r" and s: "Well_order s" and f: "iso r s f"
shows "oproj r s f"
- using assms unfolding oproj_def
- by (metis iso_Field iso_iff3 order_refl)
+ by (metis embed_Field f iso_Field iso_iff iso_iff3 oproj_def r s)
theorem oproj_embed:
assumes r: "Well_order r" and s: "Well_order s" and f: "oproj r s f"
@@ -843,6 +762,6 @@
corollary oproj_ordLeq:
assumes r: "Well_order r" and s: "Well_order s" and f: "oproj r s f"
shows "s \<le>o r"
- using oproj_embed[OF assms] r s unfolding ordLeq_def by auto
+ using f oproj_embed ordLess_iff ordLess_or_ordLeq r s by blast
end
--- a/src/HOL/Cardinals/Wellorder_Embedding.thy Fri Jan 13 11:05:48 2023 +0000
+++ b/src/HOL/Cardinals/Wellorder_Embedding.thy Fri Jan 13 16:19:56 2023 +0000
@@ -8,22 +8,22 @@
section \<open>Well-Order Embeddings\<close>
theory Wellorder_Embedding
-imports Fun_More Wellorder_Relation
+ imports Fun_More Wellorder_Relation
begin
subsection \<open>Auxiliaries\<close>
lemma UNION_bij_betw_ofilter:
-assumes WELL: "Well_order r" and
- OF: "\<And> i. i \<in> I \<Longrightarrow> ofilter r (A i)" and
- BIJ: "\<And> i. i \<in> I \<Longrightarrow> bij_betw f (A i) (A' i)"
-shows "bij_betw f (\<Union>i \<in> I. A i) (\<Union>i \<in> I. A' i)"
+ assumes WELL: "Well_order r" and
+ OF: "\<And> i. i \<in> I \<Longrightarrow> ofilter r (A i)" and
+ BIJ: "\<And> i. i \<in> I \<Longrightarrow> bij_betw f (A i) (A' i)"
+ shows "bij_betw f (\<Union>i \<in> I. A i) (\<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 \<le> A j \<or> A j \<le> A i"
- using wo_rel.ofilter_linord[of r] OF by blast
+ using wo_rel.ofilter_linord[of r] OF by blast
with WELL BIJ show ?thesis
- by (auto simp add: bij_betw_UNION_chain)
+ by (auto simp add: bij_betw_UNION_chain)
qed
@@ -31,144 +31,98 @@
functions\<close>
lemma embed_halfcong:
-assumes EQ: "\<And> a. a \<in> Field r \<Longrightarrow> f a = g a" and
- EMB: "embed r r' f"
-shows "embed r r' g"
-proof(unfold embed_def, auto)
- fix a assume *: "a \<in> Field r"
- hence "bij_betw f (under r a) (under r' (f a))"
- using EMB unfolding embed_def by simp
- moreover
- {have "under r a \<le> Field r"
- by (auto simp add: under_Field)
- hence "\<And> b. b \<in> under r a \<Longrightarrow> f b = g b"
- using EQ by blast
- }
- moreover have "f a = g a" using * EQ by auto
- ultimately show "bij_betw g (under r a) (under r' (g a))"
- using bij_betw_cong[of "under r a" f g "under r' (f a)"] by auto
-qed
+ assumes "\<And> a. a \<in> Field r \<Longrightarrow> f a = g a" and "embed r r' f"
+ shows "embed r r' g"
+ by (smt (verit, del_insts) assms bij_betw_cong embed_def in_mono under_Field)
lemma embed_cong[fundef_cong]:
-assumes "\<And> a. a \<in> Field r \<Longrightarrow> f a = g a"
-shows "embed r r' f = embed r r' g"
-using assms embed_halfcong[of r f g r']
- embed_halfcong[of r g f r'] by auto
+ assumes "\<And> a. a \<in> Field r \<Longrightarrow> f a = g a"
+ shows "embed r r' f = embed r r' g"
+ by (metis assms embed_halfcong)
lemma embedS_cong[fundef_cong]:
-assumes "\<And> a. a \<in> Field r \<Longrightarrow> f a = g a"
-shows "embedS r r' f = embedS r r' g"
-unfolding embedS_def using assms
-embed_cong[of r f g r'] bij_betw_cong[of "Field r" f g "Field r'"] by blast
+ assumes "\<And> a. a \<in> Field r \<Longrightarrow> f a = g a"
+ shows "embedS r r' f = embedS r r' g"
+ unfolding embedS_def using assms
+ embed_cong[of r f g r'] bij_betw_cong[of "Field r" f g "Field r'"] by blast
lemma iso_cong[fundef_cong]:
-assumes "\<And> a. a \<in> Field r \<Longrightarrow> f a = g a"
-shows "iso r r' f = iso r r' g"
-unfolding iso_def using assms
-embed_cong[of r f g r'] bij_betw_cong[of "Field r" f g "Field r'"] by blast
+ assumes "\<And> a. a \<in> Field r \<Longrightarrow> f a = g a"
+ shows "iso r r' f = iso r r' g"
+ unfolding iso_def using assms
+ embed_cong[of r f g r'] bij_betw_cong[of "Field r" f g "Field r'"] by blast
lemma id_compat: "compat r r id"
-by(auto simp add: id_def compat_def)
+ by(auto simp add: id_def compat_def)
lemma comp_compat:
-"\<lbrakk>compat r r' f; compat r' r'' f'\<rbrakk> \<Longrightarrow> compat r r'' (f' o f)"
-by(auto simp add: comp_def compat_def)
+ "\<lbrakk>compat r r' f; compat r' r'' f'\<rbrakk> \<Longrightarrow> compat r r'' (f' o f)"
+ by(auto simp add: comp_def compat_def)
corollary one_set_greater:
-"(\<exists>f::'a \<Rightarrow> 'a'. f ` A \<le> A' \<and> inj_on f A) \<or> (\<exists>g::'a' \<Rightarrow> 'a. g ` A' \<le> A \<and> inj_on g A')"
+ "(\<exists>f::'a \<Rightarrow> 'a'. f ` A \<le> A' \<and> inj_on f A) \<or> (\<exists>g::'a' \<Rightarrow> 'a. g ` A' \<le> A \<and> inj_on g A')"
proof-
obtain r where "well_order_on A r" by (fastforce simp add: well_order_on)
hence 1: "A = Field r \<and> Well_order r"
- using well_order_on_Well_order by auto
+ using well_order_on_Well_order by auto
obtain r' where 2: "well_order_on A' r'" by (fastforce simp add: well_order_on)
hence 2: "A' = Field r' \<and> Well_order r'"
- using well_order_on_Well_order by auto
+ using well_order_on_Well_order by auto
hence "(\<exists>f. embed r r' f) \<or> (\<exists>g. embed r' r g)"
- using 1 2 by (auto simp add: wellorders_totally_ordered)
+ using 1 2 by (auto simp add: wellorders_totally_ordered)
moreover
{fix f assume "embed r r' f"
- hence "f`A \<le> A' \<and> inj_on f A"
- using 1 2 by (auto simp add: embed_Field embed_inj_on)
+ hence "f`A \<le> A' \<and> inj_on f A"
+ using 1 2 by (auto simp add: embed_Field embed_inj_on)
}
moreover
{fix g assume "embed r' r g"
- hence "g`A' \<le> A \<and> inj_on g A'"
- using 1 2 by (auto simp add: embed_Field embed_inj_on)
+ hence "g`A' \<le> A \<and> inj_on g A'"
+ using 1 2 by (auto simp add: embed_Field embed_inj_on)
}
ultimately show ?thesis by blast
qed
corollary one_type_greater:
-"(\<exists>f::'a \<Rightarrow> 'a'. inj f) \<or> (\<exists>g::'a' \<Rightarrow> 'a. inj g)"
-using one_set_greater[of UNIV UNIV] by auto
+ "(\<exists>f::'a \<Rightarrow> 'a'. inj f) \<or> (\<exists>g::'a' \<Rightarrow> 'a. inj g)"
+ using one_set_greater[of UNIV UNIV] by auto
subsection \<open>Uniqueness of embeddings\<close>
lemma comp_embedS:
-assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
- and EMB: "embedS r r' f" and EMB': "embedS r' r'' f'"
-shows "embedS r r'' (f' o f)"
-proof-
- have "embed r' r'' f'" using EMB' unfolding embedS_def by simp
- thus ?thesis using assms by (auto simp add: embedS_comp_embed)
-qed
+ assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
+ and EMB: "embedS r r' f" and EMB': "embedS r' r'' f'"
+ shows "embedS r r'' (f' o f)"
+ using EMB EMB' WELL WELL' embedS_comp_embed embedS_def by blast
lemma iso_iff4:
-assumes WELL: "Well_order r" and WELL': "Well_order r'"
-shows "iso r r' f = (embed r r' f \<and> embed r' r (inv_into (Field r) f))"
-using assms embed_bothWays_iso
-by(unfold iso_def, auto simp add: inv_into_Field_embed_bij_betw)
+ assumes WELL: "Well_order r" and WELL': "Well_order r'"
+ shows "iso r r' f = (embed r r' f \<and> embed r' r (inv_into (Field r) f))"
+ using assms embed_bothWays_iso
+ by(unfold iso_def, auto simp add: inv_into_Field_embed_bij_betw)
lemma embed_embedS_iso:
-"embed r r' f = (embedS r r' f \<or> iso r r' f)"
-unfolding embedS_def iso_def by blast
+ "embed r r' f = (embedS r r' f \<or> iso r r' f)"
+ unfolding embedS_def iso_def by blast
lemma not_embedS_iso:
-"\<not> (embedS r r' f \<and> iso r r' f)"
-unfolding embedS_def iso_def by blast
+ "\<not> (embedS r r' f \<and> iso r r' f)"
+ unfolding embedS_def iso_def by blast
lemma embed_embedS_iff_not_iso:
-assumes "embed r r' f"
-shows "embedS r r' f = (\<not> iso r r' f)"
-using assms unfolding embedS_def iso_def by blast
+ assumes "embed r r' f"
+ shows "embedS r r' f = (\<not> iso r r' f)"
+ using assms unfolding embedS_def iso_def by blast
lemma iso_inv_into:
-assumes WELL: "Well_order r" and ISO: "iso r r' f"
-shows "iso r' r (inv_into (Field r) f)"
-using assms unfolding iso_def
-using bij_betw_inv_into inv_into_Field_embed_bij_betw by blast
+ assumes WELL: "Well_order r" and ISO: "iso r r' f"
+ shows "iso r' r (inv_into (Field r) f)"
+ by (meson ISO WELL bij_betw_inv_into inv_into_Field_embed_bij_betw iso_def iso_iff iso_iff2)
lemma embedS_or_iso:
-assumes WELL: "Well_order r" and WELL': "Well_order r'"
-shows "(\<exists>g. embedS r r' g) \<or> (\<exists>h. embedS r' r h) \<or> (\<exists>f. iso r r' f)"
-proof-
- {fix f assume *: "embed r r' f"
- {assume "bij_betw f (Field r) (Field r')"
- hence ?thesis using * by (auto simp add: iso_def)
- }
- moreover
- {assume "\<not> bij_betw f (Field r) (Field r')"
- hence ?thesis using * by (auto simp add: embedS_def)
- }
- ultimately have ?thesis by auto
- }
- moreover
- {fix f assume *: "embed r' r f"
- {assume "bij_betw f (Field r') (Field r)"
- hence "iso r' r f" using * by (auto simp add: iso_def)
- hence "iso r r' (inv_into (Field r') f)"
- using WELL' by (auto simp add: iso_inv_into)
- hence ?thesis by blast
- }
- moreover
- {assume "\<not> bij_betw f (Field r') (Field r)"
- hence ?thesis using * by (auto simp add: embedS_def)
- }
- ultimately have ?thesis by auto
- }
- ultimately show ?thesis using WELL WELL'
- wellorders_totally_ordered[of r r'] by blast
-qed
+ assumes WELL: "Well_order r" and WELL': "Well_order r'"
+ shows "(\<exists>g. embedS r r' g) \<or> (\<exists>h. embedS r' r h) \<or> (\<exists>f. iso r r' f)"
+ by (metis WELL WELL' embed_embedS_iso embed_embedS_iso iso_iff4 wellorders_totally_ordered)
end
--- a/src/HOL/Cardinals/Wellorder_Relation.thy Fri Jan 13 11:05:48 2023 +0000
+++ b/src/HOL/Cardinals/Wellorder_Relation.thy Fri Jan 13 16:19:56 2023 +0000
@@ -8,7 +8,7 @@
section \<open>Well-Order Relations\<close>
theory Wellorder_Relation
-imports Wellfounded_More
+ imports Wellfounded_More
begin
context wo_rel
@@ -17,29 +17,29 @@
subsection \<open>Auxiliaries\<close>
lemma PREORD: "Preorder r"
-using WELL order_on_defs[of _ r] by auto
+ using WELL order_on_defs[of _ r] by auto
lemma PARORD: "Partial_order r"
-using WELL order_on_defs[of _ r] by auto
+ using WELL order_on_defs[of _ r] by auto
lemma cases_Total2:
-"\<And> phi a b. \<lbrakk>{a,b} \<le> Field r; ((a,b) \<in> r - Id \<Longrightarrow> phi a b);
+ "\<And> phi a b. \<lbrakk>{a,b} \<le> Field r; ((a,b) \<in> r - Id \<Longrightarrow> phi a b);
((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>
lemma worec_unique_fixpoint:
-assumes ADM: "adm_wo H" and fp: "f = H f"
-shows "f = worec H"
+ assumes ADM: "adm_wo H" and fp: "f = H f"
+ shows "f = worec H"
proof-
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 "f = wfrec (r - Id) H"
- using fp WF wfrec_unique_fixpoint[of "r - Id" H] by simp
+ using fp WF wfrec_unique_fixpoint[of "r - Id" H] by simp
thus ?thesis unfolding worec_def .
qed
@@ -47,121 +47,66 @@
subsubsection \<open>Properties of max2\<close>
lemma max2_iff:
-assumes "a \<in> Field r" and "b \<in> Field r"
-shows "((max2 a b, c) \<in> r) = ((a,c) \<in> r \<and> (b,c) \<in> r)"
+ assumes "a \<in> Field r" and "b \<in> Field r"
+ shows "((max2 a b, c) \<in> r) = ((a,c) \<in> r \<and> (b,c) \<in> r)"
proof
assume "(max2 a b, c) \<in> r"
thus "(a,c) \<in> r \<and> (b,c) \<in> r"
- using assms max2_greater[of a b] TRANS trans_def[of r] by blast
+ using assms max2_greater[of a b] TRANS trans_def[of r] by blast
next
assume "(a,c) \<in> r \<and> (b,c) \<in> r"
thus "(max2 a b, c) \<in> r"
- using assms max2_among[of a b] by auto
+ using assms max2_among[of a b] by auto
qed
subsubsection \<open>Properties of minim\<close>
lemma minim_Under:
-"\<lbrakk>B \<le> Field r; B \<noteq> {}\<rbrakk> \<Longrightarrow> minim B \<in> Under B"
-by(auto simp add: Under_def minim_inField minim_least)
+ "\<lbrakk>B \<le> Field r; B \<noteq> {}\<rbrakk> \<Longrightarrow> minim B \<in> Under B"
+ by(auto simp add: Under_def minim_inField minim_least)
lemma equals_minim_Under:
-"\<lbrakk>B \<le> Field r; a \<in> B; a \<in> Under B\<rbrakk>
+ "\<lbrakk>B \<le> Field r; a \<in> B; a \<in> Under B\<rbrakk>
\<Longrightarrow> a = minim B"
-by(auto simp add: Under_def equals_minim)
+ by(auto simp add: Under_def equals_minim)
lemma minim_iff_In_Under:
-assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}"
-shows "(a = minim B) = (a \<in> B \<and> a \<in> Under B)"
+ assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}"
+ shows "(a = minim B) = (a \<in> B \<and> a \<in> Under B)"
proof
assume "a = minim B"
thus "a \<in> B \<and> a \<in> Under B"
- using assms minim_in minim_Under by simp
+ using assms minim_in minim_Under by simp
next
assume "a \<in> B \<and> a \<in> Under B"
thus "a = minim B"
- using assms equals_minim_Under by simp
+ using assms equals_minim_Under by simp
qed
lemma minim_Under_under:
-assumes NE: "A \<noteq> {}" and SUB: "A \<le> Field r"
-shows "Under A = under (minim A)"
+ assumes NE: "A \<noteq> {}" and SUB: "A \<le> Field r"
+ shows "Under A = under (minim A)"
proof-
- (* Preliminary facts *)
- have 1: "minim A \<in> A"
- using assms minim_in by auto
- have 2: "\<forall>x \<in> A. (minim A, x) \<in> r"
- using assms minim_least by auto
- (* Main proof *)
- have "Under A \<le> under (minim A)"
- proof
- fix x assume "x \<in> Under A"
- with 1 Under_def[of r] have "(x,minim A) \<in> r" by auto
- thus "x \<in> under(minim A)" unfolding under_def by simp
- qed
- (* *)
- moreover
- (* *)
- have "under (minim A) \<le> Under A"
- proof
- fix x assume "x \<in> under(minim A)"
- hence 11: "(x,minim A) \<in> r" unfolding under_def by simp
- hence "x \<in> Field r" unfolding Field_def by auto
- moreover
- {fix a assume "a \<in> A"
- with 2 have "(minim A, a) \<in> r" by simp
- with 11 have "(x,a) \<in> r"
- using TRANS trans_def[of r] by blast
- }
- ultimately show "x \<in> Under A" by (unfold Under_def, auto)
- qed
- (* *)
+ have "minim A \<in> A"
+ using assms minim_in by auto
+ then have "Under A \<le> under (minim A)"
+ by (simp add: Under_decr under_Under_singl)
+ moreover have "under (minim A) \<le> Under A"
+ by (meson NE SUB TRANS minim_Under subset_eq under_Under_trans)
ultimately show ?thesis by blast
qed
lemma minim_UnderS_underS:
-assumes NE: "A \<noteq> {}" and SUB: "A \<le> Field r"
-shows "UnderS A = underS (minim A)"
+ assumes NE: "A \<noteq> {}" and SUB: "A \<le> Field r"
+ shows "UnderS A = underS (minim A)"
proof-
- (* Preliminary facts *)
- have 1: "minim A \<in> A"
- using assms minim_in by auto
- have 2: "\<forall>x \<in> A. (minim A, x) \<in> r"
- using assms minim_least by auto
- (* Main proof *)
- have "UnderS A \<le> underS (minim A)"
- proof
- fix x assume "x \<in> UnderS A"
- with 1 UnderS_def[of r] have "x \<noteq> minim A \<and> (x,minim A) \<in> r" by auto
- thus "x \<in> underS(minim A)" unfolding underS_def by simp
- qed
- (* *)
- moreover
- (* *)
- have "underS (minim A) \<le> UnderS A"
- proof
- fix x assume "x \<in> underS(minim A)"
- hence 11: "x \<noteq> minim A \<and> (x,minim A) \<in> r" unfolding underS_def by simp
- hence "x \<in> Field r" unfolding Field_def by auto
- moreover
- {fix a assume "a \<in> A"
- with 2 have 3: "(minim A, a) \<in> r" by simp
- with 11 have "(x,a) \<in> r"
- using TRANS trans_def[of r] by blast
- moreover
- have "x \<noteq> a"
- proof
- assume "x = a"
- with 11 3 ANTISYM antisym_def[of r]
- show False by auto
- qed
- ultimately
- have "x \<noteq> a \<and> (x,a) \<in> r" by simp
- }
- ultimately show "x \<in> UnderS A" by (unfold UnderS_def, auto)
- qed
- (* *)
+ have "minim A \<in> A"
+ using assms minim_in by auto
+ then have "UnderS A \<le> underS (minim A)"
+ by (simp add: UnderS_decr underS_UnderS_singl)
+ moreover have "underS (minim A) \<le> UnderS A"
+ by (meson ANTISYM NE SUB TRANS minim_Under subset_eq underS_Under_trans)
ultimately show ?thesis by blast
qed
@@ -169,150 +114,103 @@
subsubsection \<open>Properties of supr\<close>
lemma supr_Above:
-assumes SUB: "B \<le> Field r" and ABOVE: "Above B \<noteq> {}"
-shows "supr B \<in> Above B"
-proof(unfold supr_def)
- have "Above B \<le> Field r"
- using Above_Field[of r] by auto
- thus "minim (Above B) \<in> Above B"
- using assms by (simp add: minim_in)
-qed
+ assumes "Above B \<noteq> {}"
+ shows "supr B \<in> Above B"
+ by (simp add: assms Above_Field minim_in supr_def)
lemma supr_greater:
-assumes SUB: "B \<le> Field r" and ABOVE: "Above B \<noteq> {}" and
- IN: "b \<in> B"
-shows "(b, supr B) \<in> r"
-proof-
- from assms supr_Above
- have "supr B \<in> Above B" by simp
- with IN Above_def[of r] show ?thesis by simp
-qed
+ assumes "Above B \<noteq> {}" "b \<in> B"
+ shows "(b, supr B) \<in> r"
+ using assms Above_def supr_Above by fastforce
lemma supr_least_Above:
-assumes SUB: "B \<le> Field r" and
- ABOVE: "a \<in> Above B"
-shows "(supr B, a) \<in> r"
-proof(unfold supr_def)
- have "Above B \<le> Field r"
- using Above_Field[of r] by auto
- thus "(minim (Above B), a) \<in> r"
- using assms minim_least
- by simp
-qed
+ assumes "a \<in> Above B"
+ shows "(supr B, a) \<in> r"
+ by (simp add: assms Above_Field minim_least supr_def)
lemma supr_least:
-"\<lbrakk>B \<le> Field r; a \<in> Field r; (\<And> b. b \<in> B \<Longrightarrow> (b,a) \<in> r)\<rbrakk>
+ "\<lbrakk>B \<le> Field r; a \<in> Field r; (\<And> b. b \<in> B \<Longrightarrow> (b,a) \<in> r)\<rbrakk>
\<Longrightarrow> (supr B, a) \<in> r"
-by(auto simp add: supr_least_Above Above_def)
+ by(auto simp add: supr_least_Above Above_def)
lemma equals_supr_Above:
-assumes SUB: "B \<le> Field r" and ABV: "a \<in> Above B" and
- MINIM: "\<And> a'. a' \<in> Above B \<Longrightarrow> (a,a') \<in> r"
-shows "a = supr B"
-proof(unfold supr_def)
- have "Above B \<le> Field r"
- using Above_Field[of r] by auto
- thus "a = minim (Above B)"
- using assms equals_minim by simp
-qed
+ assumes "a \<in> Above B" "\<And> a'. a' \<in> Above B \<Longrightarrow> (a,a') \<in> r"
+ shows "a = supr B"
+ by (simp add: assms Above_Field equals_minim supr_def)
lemma equals_supr:
-assumes SUB: "B \<le> Field r" and IN: "a \<in> Field r" and
- ABV: "\<And> b. b \<in> B \<Longrightarrow> (b,a) \<in> r" and
- MINIM: "\<And> a'. \<lbrakk> a' \<in> Field r; \<And> b. b \<in> B \<Longrightarrow> (b,a') \<in> r\<rbrakk> \<Longrightarrow> (a,a') \<in> r"
-shows "a = supr B"
+ assumes SUB: "B \<le> Field r" and IN: "a \<in> Field r" and
+ ABV: "\<And> b. b \<in> B \<Longrightarrow> (b,a) \<in> r" and
+ MINIM: "\<And> a'. \<lbrakk> a' \<in> Field r; \<And> b. b \<in> B \<Longrightarrow> (b,a') \<in> r\<rbrakk> \<Longrightarrow> (a,a') \<in> r"
+ shows "a = supr B"
proof-
have "a \<in> Above B"
- unfolding Above_def using ABV IN by simp
+ unfolding Above_def using ABV IN by simp
moreover
have "\<And> a'. a' \<in> Above B \<Longrightarrow> (a,a') \<in> r"
- unfolding Above_def using MINIM by simp
+ unfolding Above_def using MINIM by simp
ultimately show ?thesis
- using equals_supr_Above SUB by auto
+ using equals_supr_Above SUB by auto
qed
lemma supr_inField:
-assumes "B \<le> Field r" and "Above B \<noteq> {}"
-shows "supr B \<in> Field r"
-proof-
- have "supr B \<in> Above B" using supr_Above assms by simp
- thus ?thesis using assms Above_Field[of r] by auto
-qed
+ assumes "Above B \<noteq> {}"
+ shows "supr B \<in> Field r"
+ by (simp add: Above_Field assms minim_inField supr_def)
lemma supr_above_Above:
-assumes SUB: "B \<le> Field r" and ABOVE: "Above B \<noteq> {}"
-shows "Above B = above (supr B)"
-proof(unfold Above_def above_def, auto)
- fix a assume "a \<in> Field r" "\<forall>b \<in> B. (b,a) \<in> r"
- with supr_least assms
- show "(supr B, a) \<in> r" by auto
-next
- fix b assume "(supr B, b) \<in> r"
- thus "b \<in> Field r"
- using REFL refl_on_def[of _ r] by auto
-next
- fix a b
- assume 1: "(supr B, b) \<in> r" and 2: "a \<in> B"
- with assms supr_greater
- have "(a,supr B) \<in> r" by auto
- thus "(a,b) \<in> r"
- using 1 TRANS trans_def[of r] by blast
-qed
+ assumes SUB: "B \<le> Field r" and ABOVE: "Above B \<noteq> {}"
+ shows "Above B = above (supr B)"
+ apply (clarsimp simp: Above_def above_def set_eq_iff)
+ by (meson ABOVE FieldI2 SUB TRANS supr_greater supr_least transD)
lemma supr_under:
-assumes IN: "a \<in> Field r"
-shows "a = supr (under a)"
+ assumes "a \<in> Field r"
+ shows "a = supr (under a)"
proof-
have "under a \<le> Field r"
- using under_Field[of r] by auto
+ using under_Field[of r] by auto
moreover
have "under a \<noteq> {}"
- using IN Refl_under_in[of r] REFL by auto
+ using assms Refl_under_in[of r] REFL by auto
moreover
have "a \<in> Above (under a)"
- using in_Above_under[of _ r] IN by auto
+ using in_Above_under[of _ r] assms by auto
moreover
have "\<forall>a' \<in> Above (under a). (a,a') \<in> r"
- proof(unfold Above_def under_def, auto)
- fix a'
- assume "\<forall>aa. (aa, a) \<in> r \<longrightarrow> (aa, a') \<in> r"
- hence "(a,a) \<in> r \<longrightarrow> (a,a') \<in> r" by blast
- moreover have "(a,a) \<in> r"
- using REFL IN by (auto simp add: refl_on_def)
- ultimately
- show "(a, a') \<in> r" by (rule mp)
- qed
+ by (auto simp: Above_def above_def REFL Refl_under_in assms)
ultimately show ?thesis
- using equals_supr_Above by auto
+ using equals_supr_Above by auto
qed
subsubsection \<open>Properties of successor\<close>
lemma suc_least:
-"\<lbrakk>B \<le> Field r; a \<in> Field r; (\<And> b. b \<in> B \<Longrightarrow> a \<noteq> b \<and> (b,a) \<in> r)\<rbrakk>
+ "\<lbrakk>B \<le> Field r; a \<in> Field r; (\<And> b. b \<in> B \<Longrightarrow> a \<noteq> b \<and> (b,a) \<in> r)\<rbrakk>
\<Longrightarrow> (suc B, a) \<in> r"
-by(auto simp add: suc_least_AboveS AboveS_def)
+ by(auto simp add: suc_least_AboveS AboveS_def)
lemma equals_suc:
-assumes SUB: "B \<le> Field r" and IN: "a \<in> Field r" and
- ABVS: "\<And> b. b \<in> B \<Longrightarrow> a \<noteq> b \<and> (b,a) \<in> r" and
- MINIM: "\<And> a'. \<lbrakk>a' \<in> Field r; \<And> b. b \<in> B \<Longrightarrow> a' \<noteq> b \<and> (b,a') \<in> r\<rbrakk> \<Longrightarrow> (a,a') \<in> r"
-shows "a = suc B"
+ assumes SUB: "B \<le> Field r" and IN: "a \<in> Field r" and
+ ABVS: "\<And> b. b \<in> B \<Longrightarrow> a \<noteq> b \<and> (b,a) \<in> r" and
+ MINIM: "\<And> a'. \<lbrakk>a' \<in> Field r; \<And> b. b \<in> B \<Longrightarrow> a' \<noteq> b \<and> (b,a') \<in> r\<rbrakk> \<Longrightarrow> (a,a') \<in> r"
+ shows "a = suc B"
proof-
have "a \<in> AboveS B"
- unfolding AboveS_def using ABVS IN by simp
+ unfolding AboveS_def using ABVS IN by simp
moreover
have "\<And> a'. a' \<in> AboveS B \<Longrightarrow> (a,a') \<in> r"
- unfolding AboveS_def using MINIM by simp
+ unfolding AboveS_def using MINIM by simp
ultimately show ?thesis
- using equals_suc_AboveS SUB by auto
+ using equals_suc_AboveS SUB by auto
qed
lemma suc_above_AboveS:
-assumes SUB: "B \<le> Field r" and
- ABOVE: "AboveS B \<noteq> {}"
-shows "AboveS B = above (suc B)"
+ assumes SUB: "B \<le> Field r" and
+ ABOVE: "AboveS B \<noteq> {}"
+ shows "AboveS B = above (suc B)"
+ using assms
proof(unfold AboveS_def above_def, auto)
fix a assume "a \<in> Field r" "\<forall>b \<in> B. a \<noteq> b \<and> (b,a) \<in> r"
with suc_least assms
@@ -320,82 +218,57 @@
next
fix b assume "(suc B, b) \<in> r"
thus "b \<in> Field r"
- using REFL refl_on_def[of _ r] by auto
+ using REFL refl_on_def[of _ r] by auto
next
fix a b
assume 1: "(suc B, b) \<in> r" and 2: "a \<in> B"
with assms suc_greater[of B a]
have "(a,suc B) \<in> r" by auto
thus "(a,b) \<in> r"
- using 1 TRANS trans_def[of r] by blast
+ using 1 TRANS trans_def[of r] by blast
next
fix a
- assume 1: "(suc B, a) \<in> r" and 2: "a \<in> B"
- with assms suc_greater[of B a]
- have "(a,suc B) \<in> r" by auto
- moreover have "suc B \<in> Field r"
- using assms suc_inField by simp
- ultimately have "a = suc B"
- using 1 2 SUB ANTISYM antisym_def[of r] by auto
+ assume "(suc B, a) \<in> r" and 2: "a \<in> B"
thus False
- using assms suc_greater[of B a] 2 by auto
+ by (metis ABOVE ANTISYM SUB antisymD suc_greater)
qed
lemma suc_singl_pred:
-assumes IN: "a \<in> Field r" and ABOVE_NE: "aboveS a \<noteq> {}" and
- REL: "(a',suc {a}) \<in> r" and DIFF: "a' \<noteq> suc {a}"
-shows "a' = a \<or> (a',a) \<in> r"
+ assumes IN: "a \<in> Field r" and ABOVE_NE: "aboveS a \<noteq> {}" and
+ REL: "(a',suc {a}) \<in> r" and DIFF: "a' \<noteq> suc {a}"
+ shows "a' = a \<or> (a',a) \<in> r"
proof-
have *: "suc {a} \<in> Field r \<and> a' \<in> Field r"
- using WELL REL well_order_on_domain by metis
+ using WELL REL well_order_on_domain by metis
{assume **: "a' \<noteq> a"
- hence "(a,a') \<in> r \<or> (a',a) \<in> r"
- using TOTAL IN * by (auto simp add: total_on_def)
- moreover
- {assume "(a,a') \<in> r"
- with ** * assms WELL suc_least[of "{a}" a']
- have "(suc {a},a') \<in> r" by auto
- with REL DIFF * ANTISYM antisym_def[of r]
- have False by simp
- }
- ultimately have "(a',a) \<in> r"
- by blast
+ hence "(a,a') \<in> r \<or> (a',a) \<in> r"
+ using TOTAL IN * by (auto simp add: total_on_def)
+ moreover
+ {assume "(a,a') \<in> r"
+ with ** * assms WELL suc_least[of "{a}" a']
+ have "(suc {a},a') \<in> r" by auto
+ with REL DIFF * ANTISYM antisym_def[of r]
+ have False by simp
+ }
+ ultimately have "(a',a) \<in> r"
+ by blast
}
thus ?thesis by blast
qed
lemma under_underS_suc:
-assumes IN: "a \<in> Field r" and ABV: "aboveS a \<noteq> {}"
-shows "underS (suc {a}) = under a"
-proof-
- have 1: "AboveS {a} \<noteq> {}"
- using ABV aboveS_AboveS_singl[of r] by auto
- have 2: "a \<noteq> suc {a} \<and> (a,suc {a}) \<in> r"
- using suc_greater[of "{a}" a] IN 1 by auto
- (* *)
+ assumes IN: "a \<in> Field r" and ABV: "aboveS a \<noteq> {}"
+ shows "underS (suc {a}) = under a"
+proof -
+ have "AboveS {a} \<noteq> {}"
+ using ABV aboveS_AboveS_singl[of r] by auto
+ then have 2: "a \<noteq> suc {a} \<and> (a,suc {a}) \<in> r"
+ using suc_greater[of "{a}" a] IN by auto
have "underS (suc {a}) \<le> under a"
- proof(unfold underS_def under_def, auto)
- fix x assume *: "x \<noteq> suc {a}" and **: "(x,suc {a}) \<in> r"
- with suc_singl_pred[of a x] IN ABV
- have "x = a \<or> (x,a) \<in> r" by auto
- with REFL refl_on_def[of _ r] IN
- show "(x,a) \<in> r" by auto
- qed
- (* *)
+ using ABV IN REFL Refl_under_in underS_E under_def wo_rel.suc_singl_pred wo_rel_axioms by fastforce
moreover
- (* *)
have "under a \<le> underS (suc {a})"
- proof(unfold underS_def under_def, auto)
- assume "(suc {a}, a) \<in> r"
- with 2 ANTISYM antisym_def[of r]
- show False by auto
- next
- fix x assume *: "(x,a) \<in> r"
- with 2 TRANS trans_def[of r]
- show "(x,suc {a}) \<in> r" by blast
- (* blast is often better than auto/auto for transitivity-like properties *)
- qed
- (* *)
+ by (simp add: "2" ANTISYM TRANS subsetI underS_I under_underS_trans)
ultimately show ?thesis by blast
qed
@@ -403,113 +276,49 @@
subsubsection \<open>Properties of order filters\<close>
lemma ofilter_Under[simp]:
-assumes "A \<le> Field r"
-shows "ofilter(Under A)"
-proof(unfold ofilter_def, auto)
- fix x assume "x \<in> Under A"
- thus "x \<in> Field r"
- using Under_Field[of r] assms by auto
-next
- fix a x
- assume "a \<in> Under A" and "x \<in> under a"
- thus "x \<in> Under A"
- using TRANS under_Under_trans[of r] by auto
-qed
+ assumes "A \<le> Field r"
+ shows "ofilter(Under A)"
+ by (clarsimp simp: ofilter_def) (meson TRANS Under_Field subset_eq under_Under_trans)
lemma ofilter_UnderS[simp]:
-assumes "A \<le> Field r"
-shows "ofilter(UnderS A)"
-proof(unfold ofilter_def, auto)
- fix x assume "x \<in> UnderS A"
- thus "x \<in> Field r"
- using UnderS_Field[of r] assms by auto
-next
- fix a x
- assume "a \<in> UnderS A" and "x \<in> under a"
- thus "x \<in> UnderS A"
- using TRANS ANTISYM under_UnderS_trans[of r] by auto
-qed
+ assumes "A \<le> Field r"
+ shows "ofilter(UnderS A)"
+ by (clarsimp simp: ofilter_def) (meson ANTISYM TRANS UnderS_Field subset_eq under_UnderS_trans)
lemma ofilter_Int[simp]: "\<lbrakk>ofilter A; ofilter B\<rbrakk> \<Longrightarrow> ofilter(A Int B)"
-unfolding ofilter_def by blast
+ unfolding ofilter_def by blast
lemma ofilter_Un[simp]: "\<lbrakk>ofilter A; ofilter B\<rbrakk> \<Longrightarrow> ofilter(A \<union> B)"
-unfolding ofilter_def by blast
+ unfolding ofilter_def by blast
lemma ofilter_INTER:
-"\<lbrakk>I \<noteq> {}; \<And> i. i \<in> I \<Longrightarrow> ofilter(A i)\<rbrakk> \<Longrightarrow> ofilter (\<Inter>i \<in> I. A i)"
-unfolding ofilter_def by blast
+ "\<lbrakk>I \<noteq> {}; \<And> i. i \<in> I \<Longrightarrow> ofilter(A i)\<rbrakk> \<Longrightarrow> ofilter (\<Inter>i \<in> I. A i)"
+ unfolding ofilter_def by blast
lemma ofilter_Inter:
-"\<lbrakk>S \<noteq> {}; \<And> A. A \<in> S \<Longrightarrow> ofilter A\<rbrakk> \<Longrightarrow> ofilter (\<Inter>S)"
-unfolding ofilter_def by blast
+ "\<lbrakk>S \<noteq> {}; \<And> A. A \<in> S \<Longrightarrow> ofilter A\<rbrakk> \<Longrightarrow> ofilter (\<Inter>S)"
+ unfolding ofilter_def by blast
lemma ofilter_Union:
-"(\<And> A. A \<in> S \<Longrightarrow> ofilter A) \<Longrightarrow> ofilter (\<Union>S)"
-unfolding ofilter_def by blast
+ "(\<And> A. A \<in> S \<Longrightarrow> ofilter A) \<Longrightarrow> ofilter (\<Union>S)"
+ unfolding ofilter_def by blast
lemma ofilter_under_Union:
-"ofilter A \<Longrightarrow> A = \<Union>{under a| a. a \<in> A}"
-using ofilter_under_UNION [of A] by auto
+ "ofilter A \<Longrightarrow> A = \<Union>{under a| a. a \<in> A}"
+ using ofilter_under_UNION [of A] by auto
subsubsection \<open>Other properties\<close>
lemma Trans_Under_regressive:
-assumes NE: "A \<noteq> {}" and SUB: "A \<le> Field r"
-shows "Under(Under A) \<le> Under A"
-proof
- let ?a = "minim A"
- (* Preliminary facts *)
- have 1: "minim A \<in> Under A"
- using assms minim_Under by auto
- have 2: "\<forall>y \<in> A. (minim A, y) \<in> r"
- using assms minim_least by auto
- (* Main proof *)
- fix x assume "x \<in> Under(Under A)"
- with 1 have 1: "(x,minim A) \<in> r"
- using Under_def[of r] by auto
- with Field_def have "x \<in> Field r" by fastforce
- moreover
- {fix y assume *: "y \<in> A"
- hence "(x,y) \<in> r"
- using 1 2 TRANS trans_def[of r] by blast
- with Field_def have "(x,y) \<in> r" by auto
- }
- ultimately
- show "x \<in> Under A" unfolding Under_def by auto
-qed
+ assumes NE: "A \<noteq> {}" and SUB: "A \<le> Field r"
+ shows "Under(Under A) \<le> Under A"
+ by (metis INT_E NE REFL Refl_under_Under SUB empty_iff minim_Under minim_Under_under subsetI)
lemma ofilter_suc_Field:
-assumes OF: "ofilter A" and NE: "A \<noteq> Field r"
-shows "ofilter (A \<union> {suc A})"
-proof-
- (* Preliminary facts *)
- have 1: "A \<le> Field r" using OF ofilter_def by auto
- hence 2: "AboveS A \<noteq> {}"
- using ofilter_AboveS_Field NE OF by blast
- from 1 2 suc_inField
- have 3: "suc A \<in> Field r" by auto
- (* Main proof *)
- show ?thesis
- proof(unfold ofilter_def, auto simp add: 1 3)
- fix a x
- assume "a \<in> A" "x \<in> under a" "x \<notin> A"
- with OF ofilter_def have False by auto
- thus "x = suc A" by simp
- next
- fix x assume *: "x \<in> under (suc A)" and **: "x \<notin> A"
- hence "x \<in> Field r" using under_def Field_def by fastforce
- with ** have "x \<in> AboveS A"
- using ofilter_AboveS_Field[of A] OF by auto
- hence "(suc A,x) \<in> r"
- using suc_least_AboveS by auto
- moreover
- have "(x,suc A) \<in> r" using * under_def[of r] by auto
- ultimately show "x = suc A"
- using ANTISYM antisym_def[of r] by auto
- qed
-qed
+ assumes OF: "ofilter A" and NE: "A \<noteq> Field r"
+ shows "ofilter (A \<union> {suc A})"
+ by (metis NE OF REFL Refl_under_underS ofilter_underS_Field suc_underS under_ofilter)
(* FIXME: needed? *)
declare
--- a/src/HOL/Relation.thy Fri Jan 13 11:05:48 2023 +0000
+++ b/src/HOL/Relation.thy Fri Jan 13 16:19:56 2023 +0000
@@ -1247,6 +1247,9 @@
definition Field :: "'a rel \<Rightarrow> 'a set"
where "Field r = Domain r \<union> Range r"
+lemma Field_iff: "x \<in> Field r \<longleftrightarrow> (\<exists>y. (x,y) \<in> r \<or> (y,x) \<in> r)"
+ by (auto simp: Field_def)
+
lemma FieldI1: "(i, j) \<in> R \<Longrightarrow> i \<in> Field R"
unfolding Field_def by blast