--- a/src/HOL/Order_Relation.thy Sun Jul 31 19:09:21 2016 +0200
+++ b/src/HOL/Order_Relation.thy Sun Jul 31 22:56:18 2016 +0200
@@ -9,7 +9,7 @@
imports Wfrec
begin
-subsection\<open>Orders on a set\<close>
+subsection \<open>Orders on a set\<close>
definition "preorder_on A r \<equiv> refl_on A r \<and> trans r"
@@ -27,51 +27,48 @@
lemma preorder_on_empty[simp]: "preorder_on {} {}"
-by(simp add:preorder_on_def trans_def)
+ by (simp add: preorder_on_def trans_def)
lemma partial_order_on_empty[simp]: "partial_order_on {} {}"
-by(simp add:partial_order_on_def)
+ by (simp add: partial_order_on_def)
lemma lnear_order_on_empty[simp]: "linear_order_on {} {}"
-by(simp add:linear_order_on_def)
+ by (simp add: linear_order_on_def)
lemma well_order_on_empty[simp]: "well_order_on {} {}"
-by(simp add:well_order_on_def)
+ by (simp add: well_order_on_def)
-lemma preorder_on_converse[simp]: "preorder_on A (r^-1) = preorder_on A r"
-by (simp add:preorder_on_def)
+lemma preorder_on_converse[simp]: "preorder_on A (r\<inverse>) = preorder_on A r"
+ by (simp add: preorder_on_def)
-lemma partial_order_on_converse[simp]:
- "partial_order_on A (r^-1) = partial_order_on A r"
-by (simp add: partial_order_on_def)
+lemma partial_order_on_converse[simp]: "partial_order_on A (r\<inverse>) = partial_order_on A r"
+ by (simp add: partial_order_on_def)
-lemma linear_order_on_converse[simp]:
- "linear_order_on A (r^-1) = linear_order_on A r"
-by (simp add: linear_order_on_def)
+lemma linear_order_on_converse[simp]: "linear_order_on A (r\<inverse>) = linear_order_on A r"
+ by (simp add: linear_order_on_def)
-lemma strict_linear_order_on_diff_Id:
- "linear_order_on A r \<Longrightarrow> strict_linear_order_on A (r-Id)"
-by(simp add: order_on_defs trans_diff_Id)
+lemma strict_linear_order_on_diff_Id: "linear_order_on A r \<Longrightarrow> strict_linear_order_on A (r - Id)"
+ by (simp add: order_on_defs trans_diff_Id)
lemma linear_order_on_singleton [simp]: "linear_order_on {x} {(x, x)}"
-unfolding order_on_defs by simp
+ by (simp add: order_on_defs)
lemma linear_order_on_acyclic:
assumes "linear_order_on A r"
shows "acyclic (r - Id)"
-using strict_linear_order_on_diff_Id[OF assms]
-by(auto simp add: acyclic_irrefl strict_linear_order_on_def)
+ using strict_linear_order_on_diff_Id[OF assms]
+ by (auto simp add: acyclic_irrefl strict_linear_order_on_def)
lemma linear_order_on_well_order_on:
assumes "finite r"
shows "linear_order_on A r \<longleftrightarrow> well_order_on A r"
-unfolding well_order_on_def
-using assms finite_acyclic_wf[OF _ linear_order_on_acyclic, of r] by blast
+ unfolding well_order_on_def
+ using assms finite_acyclic_wf[OF _ linear_order_on_acyclic, of r] by blast
-subsection\<open>Orders on the field\<close>
+subsection \<open>Orders on the field\<close>
abbreviation "Refl r \<equiv> refl_on (Field r) r"
@@ -87,50 +84,57 @@
lemma subset_Image_Image_iff:
- "\<lbrakk> Preorder r; A \<subseteq> Field r; B \<subseteq> Field r\<rbrakk> \<Longrightarrow>
- r `` A \<subseteq> r `` B \<longleftrightarrow> (\<forall>a\<in>A.\<exists>b\<in>B. (b,a):r)"
-unfolding preorder_on_def refl_on_def Image_def
-apply (simp add: subset_eq)
-unfolding trans_def by fast
+ "Preorder r \<Longrightarrow> A \<subseteq> Field r \<Longrightarrow> B \<subseteq> Field r \<Longrightarrow>
+ r `` A \<subseteq> r `` B \<longleftrightarrow> (\<forall>a\<in>A.\<exists>b\<in>B. (b, a) \<in> r)"
+ apply (simp add: preorder_on_def refl_on_def Image_def subset_eq)
+ apply (simp only: trans_def)
+ apply fast
+ done
lemma subset_Image1_Image1_iff:
- "\<lbrakk> Preorder r; a : Field r; b : Field r\<rbrakk> \<Longrightarrow> r `` {a} \<subseteq> r `` {b} \<longleftrightarrow> (b,a):r"
-by(simp add:subset_Image_Image_iff)
+ "Preorder r \<Longrightarrow> a \<in> Field r \<Longrightarrow> b \<in> Field r \<Longrightarrow> r `` {a} \<subseteq> r `` {b} \<longleftrightarrow> (b, a) \<in> r"
+ by (simp add: subset_Image_Image_iff)
lemma Refl_antisym_eq_Image1_Image1_iff:
- assumes r: "Refl r" and as: "antisym r" and abf: "a \<in> Field r" "b \<in> Field r"
+ assumes "Refl r"
+ and as: "antisym r"
+ and abf: "a \<in> Field r" "b \<in> Field r"
shows "r `` {a} = r `` {b} \<longleftrightarrow> a = b"
+ (is "?lhs \<longleftrightarrow> ?rhs")
proof
- assume "r `` {a} = r `` {b}"
- hence e: "\<And>x. (a, x) \<in> r \<longleftrightarrow> (b, x) \<in> r" by (simp add: set_eq_iff)
- have "(a, a) \<in> r" "(b, b) \<in> r" using r abf by (simp_all add: refl_on_def)
- hence "(a, b) \<in> r" "(b, a) \<in> r" using e[of a] e[of b] by simp_all
- thus "a = b" using as[unfolded antisym_def] by blast
-qed fast
+ assume ?lhs
+ then have *: "\<And>x. (a, x) \<in> r \<longleftrightarrow> (b, x) \<in> r"
+ by (simp add: set_eq_iff)
+ have "(a, a) \<in> r" "(b, b) \<in> r" using \<open>Refl r\<close> abf by (simp_all add: refl_on_def)
+ then have "(a, b) \<in> r" "(b, a) \<in> r" using *[of a] *[of b] by simp_all
+ then show ?rhs
+ using \<open>antisym r\<close>[unfolded antisym_def] by blast
+next
+ assume ?rhs
+ then show ?lhs by fast
+qed
lemma Partial_order_eq_Image1_Image1_iff:
- "\<lbrakk>Partial_order r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b"
-by(auto simp:order_on_defs Refl_antisym_eq_Image1_Image1_iff)
+ "Partial_order r \<Longrightarrow> a \<in> Field r \<Longrightarrow> b \<in> Field r \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a = b"
+ by (auto simp: order_on_defs Refl_antisym_eq_Image1_Image1_iff)
lemma Total_Id_Field:
-assumes TOT: "Total r" and NID: "\<not> (r <= Id)"
-shows "Field r = Field(r - Id)"
-using mono_Field[of "r - Id" r] Diff_subset[of r Id]
-proof(auto)
- have "r \<noteq> {}" using NID by fast
- then obtain b and c where "b \<noteq> c \<and> (b,c) \<in> r" using NID by auto
- hence 1: "b \<noteq> c \<and> {b,c} \<le> Field r" by (auto simp: Field_def)
-
+ assumes "Total r"
+ and not_Id: "\<not> r \<subseteq> Id"
+ shows "Field r = Field (r - Id)"
+ using mono_Field[of "r - Id" r] Diff_subset[of r Id]
+proof auto
fix a assume *: "a \<in> Field r"
- obtain d where 2: "d \<in> Field r" and 3: "d \<noteq> a"
- using * 1 by auto
- hence "(a,d) \<in> r \<or> (d,a) \<in> r" using * TOT
- by (simp add: total_on_def)
- thus "a \<in> Field(r - Id)" using 3 unfolding Field_def by blast
+ from not_Id have "r \<noteq> {}" by fast
+ with not_Id obtain b and c where "b \<noteq> c \<and> (b,c) \<in> r" by auto
+ then have "b \<noteq> c \<and> {b, c} \<subseteq> Field r" by (auto simp: Field_def)
+ with * obtain d where "d \<in> Field r" "d \<noteq> a" by auto
+ with * \<open>Total r\<close> have "(a, d) \<in> r \<or> (d, a) \<in> r" by (simp add: total_on_def)
+ with \<open>d \<noteq> a\<close> show "a \<in> Field (r - Id)" unfolding Field_def by blast
qed
-subsection\<open>Orders on a type\<close>
+subsection \<open>Orders on a type\<close>
abbreviation "strict_linear_order \<equiv> strict_linear_order_on UNIV"
@@ -141,297 +145,303 @@
subsection \<open>Order-like relations\<close>
-text\<open>In this subsection, we develop basic concepts and results pertaining
-to order-like relations, i.e., to reflexive and/or transitive and/or symmetric and/or
-total relations. We also further define upper and lower bounds operators.\<close>
+text \<open>
+ In this subsection, we develop basic concepts and results pertaining
+ to order-like relations, i.e., to reflexive and/or transitive and/or symmetric and/or
+ total relations. We also further define upper and lower bounds operators.
+\<close>
subsubsection \<open>Auxiliaries\<close>
-lemma refl_on_domain:
-"\<lbrakk>refl_on A r; (a,b) : r\<rbrakk> \<Longrightarrow> a \<in> A \<and> b \<in> A"
-by(auto simp add: refl_on_def)
+lemma refl_on_domain: "refl_on A r \<Longrightarrow> (a, b) \<in> r \<Longrightarrow> a \<in> A \<and> b \<in> A"
+ by (auto simp add: refl_on_def)
-corollary well_order_on_domain:
-"\<lbrakk>well_order_on A r; (a,b) \<in> r\<rbrakk> \<Longrightarrow> a \<in> A \<and> b \<in> A"
-by (auto simp add: refl_on_domain order_on_defs)
+corollary well_order_on_domain: "well_order_on A r \<Longrightarrow> (a, b) \<in> r \<Longrightarrow> a \<in> A \<and> b \<in> A"
+ by (auto simp add: refl_on_domain order_on_defs)
-lemma well_order_on_Field:
-"well_order_on A r \<Longrightarrow> A = Field r"
-by(auto simp add: refl_on_def Field_def order_on_defs)
+lemma well_order_on_Field: "well_order_on A r \<Longrightarrow> A = Field r"
+ by (auto simp add: refl_on_def Field_def order_on_defs)
-lemma well_order_on_Well_order:
-"well_order_on A r \<Longrightarrow> A = Field r \<and> Well_order r"
-using well_order_on_Field by auto
+lemma well_order_on_Well_order: "well_order_on A r \<Longrightarrow> A = Field r \<and> Well_order r"
+ using well_order_on_Field [of A] by auto
lemma Total_subset_Id:
-assumes TOT: "Total r" and SUB: "r \<le> Id"
-shows "r = {} \<or> (\<exists>a. r = {(a,a)})"
-proof-
- {assume "r \<noteq> {}"
- then obtain a b where 1: "(a,b) \<in> r" by fast
- hence "a = b" using SUB by blast
- hence 2: "(a,a) \<in> r" using 1 by simp
- {fix c d assume "(c,d) \<in> r"
- hence "{a,c,d} \<le> Field r" using 1 unfolding Field_def by blast
- hence "((a,c) \<in> r \<or> (c,a) \<in> r \<or> a = c) \<and>
- ((a,d) \<in> r \<or> (d,a) \<in> r \<or> a = d)"
- using TOT unfolding total_on_def by blast
- hence "a = c \<and> a = d" using SUB by blast
- }
- hence "r \<le> {(a,a)}" by auto
- with 2 have "\<exists>a. r = {(a,a)}" by blast
- }
- thus ?thesis by blast
+ assumes "Total r"
+ and "r \<subseteq> Id"
+ shows "r = {} \<or> (\<exists>a. r = {(a, a)})"
+proof -
+ have "\<exists>a. r = {(a, a)}" if "r \<noteq> {}"
+ proof -
+ from that obtain a b where ab: "(a, b) \<in> r" by fast
+ with \<open>r \<subseteq> Id\<close> have "a = b" by blast
+ with ab have aa: "(a, a) \<in> r" by simp
+ have "a = c \<and> a = d" if "(c, d) \<in> r" for c d
+ proof -
+ from that have "{a, c, d} \<subseteq> Field r"
+ using ab unfolding Field_def by blast
+ then have "((a, c) \<in> r \<or> (c, a) \<in> r \<or> a = c) \<and> ((a, d) \<in> r \<or> (d, a) \<in> r \<or> a = d)"
+ using \<open>Total r\<close> unfolding total_on_def by blast
+ with \<open>r \<subseteq> Id\<close> show ?thesis by blast
+ qed
+ then have "r \<subseteq> {(a, a)}" by auto
+ with aa show ?thesis by blast
+ qed
+ then show ?thesis by blast
qed
lemma Linear_order_in_diff_Id:
-assumes LI: "Linear_order r" and
- IN1: "a \<in> Field r" and IN2: "b \<in> Field r"
-shows "((a,b) \<in> r) = ((b,a) \<notin> r - Id)"
-using assms unfolding order_on_defs total_on_def antisym_def Id_def refl_on_def by force
+ assumes "Linear_order r"
+ and "a \<in> Field r"
+ and "b \<in> Field r"
+ shows "(a, b) \<in> r \<longleftrightarrow> (b, a) \<notin> r - Id"
+ using assms unfolding order_on_defs total_on_def antisym_def Id_def refl_on_def by force
subsubsection \<open>The upper and lower bounds operators\<close>
-text\<open>Here we define upper (``above") and lower (``below") bounds operators.
-We think of \<open>r\<close> as a {\em non-strict} relation. The suffix ``S"
-at the names of some operators indicates that the bounds are strict -- e.g.,
-\<open>underS a\<close> is the set of all strict lower bounds of \<open>a\<close> (w.r.t. \<open>r\<close>).
-Capitalization of the first letter in the name reminds that the operator acts on sets, rather
-than on individual elements.\<close>
+text \<open>
+ Here we define upper (``above") and lower (``below") bounds operators. We
+ think of \<open>r\<close> as a \<^emph>\<open>non-strict\<close> relation. The suffix \<open>S\<close> at the names of
+ some operators indicates that the bounds are strict -- e.g., \<open>underS a\<close> is
+ the set of all strict lower bounds of \<open>a\<close> (w.r.t. \<open>r\<close>). Capitalization of
+ the first letter in the name reminds that the operator acts on sets, rather
+ than on individual elements.
+\<close>
-definition under::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
-where "under r a \<equiv> {b. (b,a) \<in> r}"
+definition under :: "'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
+ where "under r a \<equiv> {b. (b, a) \<in> r}"
-definition underS::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
-where "underS r a \<equiv> {b. b \<noteq> a \<and> (b,a) \<in> r}"
+definition underS :: "'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
+ where "underS r a \<equiv> {b. b \<noteq> a \<and> (b, a) \<in> r}"
-definition Under::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
-where "Under r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (b,a) \<in> r}"
+definition Under :: "'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
+ where "Under r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (b, a) \<in> r}"
-definition UnderS::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
-where "UnderS r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (b,a) \<in> r}"
+definition UnderS :: "'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
+ where "UnderS r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (b, a) \<in> r}"
-definition above::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
-where "above r a \<equiv> {b. (a,b) \<in> r}"
+definition above :: "'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
+ where "above r a \<equiv> {b. (a, b) \<in> r}"
-definition aboveS::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
-where "aboveS r a \<equiv> {b. b \<noteq> a \<and> (a,b) \<in> r}"
+definition aboveS :: "'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
+ where "aboveS r a \<equiv> {b. b \<noteq> a \<and> (a, b) \<in> r}"
-definition Above::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
-where "Above r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (a,b) \<in> r}"
+definition Above :: "'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
+ where "Above r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (a, b) \<in> r}"
-definition AboveS::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
-where "AboveS r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (a,b) \<in> r}"
+definition AboveS :: "'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
+ where "AboveS r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (a, b) \<in> r}"
definition ofilter :: "'a rel \<Rightarrow> 'a set \<Rightarrow> bool"
-where "ofilter r A \<equiv> (A \<le> Field r) \<and> (\<forall>a \<in> A. under r a \<le> A)"
+ where "ofilter r A \<equiv> A \<subseteq> Field r \<and> (\<forall>a \<in> A. under r a \<subseteq> A)"
-text\<open>Note: In the definitions of \<open>Above[S]\<close> and \<open>Under[S]\<close>,
- we bounded comprehension by \<open>Field r\<close> in order to properly cover
- the case of \<open>A\<close> being empty.\<close>
+text \<open>
+ Note: In the definitions of \<open>Above[S]\<close> and \<open>Under[S]\<close>, we bounded
+ comprehension by \<open>Field r\<close> in order to properly cover the case of \<open>A\<close> being
+ empty.
+\<close>
-lemma underS_subset_under: "underS r a \<le> under r a"
-by(auto simp add: underS_def under_def)
+lemma underS_subset_under: "underS r a \<subseteq> under r a"
+ by (auto simp add: underS_def under_def)
lemma underS_notIn: "a \<notin> underS r a"
-by(simp add: underS_def)
+ by (simp add: underS_def)
-lemma Refl_under_in: "\<lbrakk>Refl r; a \<in> Field r\<rbrakk> \<Longrightarrow> a \<in> under r a"
-by(simp add: refl_on_def under_def)
+lemma Refl_under_in: "Refl r \<Longrightarrow> a \<in> Field r \<Longrightarrow> a \<in> under r a"
+ by (simp add: refl_on_def under_def)
-lemma AboveS_disjoint: "A Int (AboveS r A) = {}"
-by(auto simp add: AboveS_def)
+lemma AboveS_disjoint: "A \<inter> (AboveS r A) = {}"
+ by (auto simp add: AboveS_def)
lemma in_AboveS_underS: "a \<in> Field r \<Longrightarrow> a \<in> AboveS r (underS r a)"
-by(auto simp add: AboveS_def underS_def)
+ by (auto simp add: AboveS_def underS_def)
-lemma Refl_under_underS:
- assumes "Refl r" "a \<in> Field r"
- shows "under r a = underS r a \<union> {a}"
-unfolding under_def underS_def
-using assms refl_on_def[of _ r] by fastforce
+lemma Refl_under_underS: "Refl r \<Longrightarrow> a \<in> Field r \<Longrightarrow> under r a = underS r a \<union> {a}"
+ unfolding under_def underS_def
+ using refl_on_def[of _ r] by fastforce
lemma underS_empty: "a \<notin> Field r \<Longrightarrow> underS r a = {}"
-by (auto simp: Field_def underS_def)
+ by (auto simp: Field_def underS_def)
-lemma under_Field: "under r a \<le> Field r"
-by(unfold under_def Field_def, auto)
+lemma under_Field: "under r a \<subseteq> Field r"
+ by (auto simp: under_def Field_def)
-lemma underS_Field: "underS r a \<le> Field r"
-by(unfold underS_def Field_def, auto)
+lemma underS_Field: "underS r a \<subseteq> Field r"
+ by (auto simp: underS_def Field_def)
-lemma underS_Field2:
-"a \<in> Field r \<Longrightarrow> underS r a < Field r"
-using underS_notIn underS_Field by fast
+lemma underS_Field2: "a \<in> Field r \<Longrightarrow> underS r a \<subset> Field r"
+ using underS_notIn underS_Field by fast
-lemma underS_Field3:
-"Field r \<noteq> {} \<Longrightarrow> underS r a < Field r"
-by(cases "a \<in> Field r", simp add: underS_Field2, auto simp add: underS_empty)
+lemma underS_Field3: "Field r \<noteq> {} \<Longrightarrow> underS r a \<subset> Field r"
+ by (cases "a \<in> Field r") (auto simp: underS_Field2 underS_empty)
-lemma AboveS_Field: "AboveS r A \<le> Field r"
-by(unfold AboveS_def Field_def, auto)
+lemma AboveS_Field: "AboveS r A \<subseteq> Field r"
+ by (auto simp: AboveS_def Field_def)
lemma under_incr:
- assumes TRANS: "trans r" and REL: "(a,b) \<in> r"
- shows "under r a \<le> under r b"
-proof(unfold under_def, auto)
- fix x assume "(x,a) \<in> r"
- with REL TRANS trans_def[of r]
- show "(x,b) \<in> r" by blast
+ assumes "trans r"
+ and "(a, b) \<in> r"
+ shows "under r a \<subseteq> under r b"
+ unfolding under_def
+proof auto
+ fix x assume "(x, a) \<in> r"
+ with assms trans_def[of r] show "(x, b) \<in> r" by blast
qed
lemma underS_incr:
-assumes TRANS: "trans r" and ANTISYM: "antisym r" and
- REL: "(a,b) \<in> r"
-shows "underS r a \<le> underS r b"
-proof(unfold underS_def, auto)
- assume *: "b \<noteq> a" and **: "(b,a) \<in> r"
- with ANTISYM antisym_def[of r] REL
- show False by blast
+ assumes "trans r"
+ and "antisym r"
+ and ab: "(a, b) \<in> r"
+ shows "underS r a \<subseteq> underS r b"
+ unfolding underS_def
+proof auto
+ assume *: "b \<noteq> a" and **: "(b, a) \<in> r"
+ with \<open>antisym r\<close> antisym_def[of r] ab show False
+ by blast
next
- fix x assume "x \<noteq> a" "(x,a) \<in> r"
- with REL TRANS trans_def[of r]
- show "(x,b) \<in> r" by blast
+ fix x assume "x \<noteq> a" "(x, a) \<in> r"
+ with ab \<open>trans r\<close> trans_def[of r] show "(x, b) \<in> r"
+ by blast
qed
lemma underS_incl_iff:
-assumes LO: "Linear_order r" and
- INa: "a \<in> Field r" and INb: "b \<in> Field r"
-shows "(underS r a \<le> underS r b) = ((a,b) \<in> r)"
+ assumes LO: "Linear_order r"
+ and INa: "a \<in> Field r"
+ and INb: "b \<in> Field r"
+ shows "underS r a \<subseteq> underS r b \<longleftrightarrow> (a, b) \<in> r"
+ (is "?lhs \<longleftrightarrow> ?rhs")
proof
- assume "(a,b) \<in> r"
- thus "underS r a \<le> underS r b" using LO
- by (simp add: order_on_defs underS_incr)
+ assume ?rhs
+ with \<open>Linear_order r\<close> show ?lhs
+ by (simp add: order_on_defs underS_incr)
next
- assume *: "underS r a \<le> underS r b"
- {assume "a = b"
- hence "(a,b) \<in> r" using assms
- by (simp add: order_on_defs refl_on_def)
- }
- moreover
- {assume "a \<noteq> b \<and> (b,a) \<in> r"
- hence "b \<in> underS r a" unfolding underS_def by blast
- hence "b \<in> underS r b" using * by blast
- hence False by (simp add: underS_notIn)
- }
- ultimately
- show "(a,b) \<in> r" using assms
- order_on_defs[of "Field r" r] total_on_def[of "Field r" r] by blast
+ assume *: ?lhs
+ have "(a, b) \<in> r" if "a = b"
+ using assms that by (simp add: order_on_defs refl_on_def)
+ moreover have False if "a \<noteq> b" "(b, a) \<in> r"
+ proof -
+ from that have "b \<in> underS r a" unfolding underS_def by blast
+ with * have "b \<in> underS r b" by blast
+ then show ?thesis by (simp add: underS_notIn)
+ qed
+ ultimately show "(a,b) \<in> r"
+ using assms order_on_defs[of "Field r" r] total_on_def[of "Field r" r] by blast
qed
lemma finite_Linear_order_induct[consumes 3, case_names step]:
assumes "Linear_order r"
- and "x \<in> Field r"
- and "finite r"
- and step: "\<And>x. \<lbrakk>x \<in> Field r; \<And>y. y \<in> aboveS r x \<Longrightarrow> P y\<rbrakk> \<Longrightarrow> P x"
+ and "x \<in> Field r"
+ and "finite r"
+ and step: "\<And>x. x \<in> Field r \<Longrightarrow> (\<And>y. y \<in> aboveS r x \<Longrightarrow> P y) \<Longrightarrow> P x"
shows "P x"
-using assms(2)
-proof(induct rule: wf_induct[of "r\<inverse> - Id"])
+ using assms(2)
+proof (induct rule: wf_induct[of "r\<inverse> - Id"])
+ case 1
from assms(1,3) show "wf (r\<inverse> - Id)"
using linear_order_on_well_order_on linear_order_on_converse
unfolding well_order_on_def by blast
next
- case (2 x) then show ?case
- by - (rule step; auto simp: aboveS_def intro: FieldI2)
+ case prems: (2 x)
+ show ?case
+ by (rule step) (use prems in \<open>auto simp: aboveS_def intro: FieldI2\<close>)
qed
subsection \<open>Variations on Well-Founded Relations\<close>
text \<open>
-This subsection contains some variations of the results from @{theory Wellfounded}:
-\begin{itemize}
-\item means for slightly more direct definitions by well-founded recursion;
-\item variations of well-founded induction;
-\item means for proving a linear order to be a well-order.
-\end{itemize}
+ This subsection contains some variations of the results from @{theory Wellfounded}:
+ \<^item> means for slightly more direct definitions by well-founded recursion;
+ \<^item> variations of well-founded induction;
+ \<^item> means for proving a linear order to be a well-order.
\<close>
subsubsection \<open>Characterizations of well-foundedness\<close>
-text \<open>A transitive relation is well-founded iff it is ``locally'' well-founded,
-i.e., iff its restriction to the lower bounds of of any element is well-founded.\<close>
+text \<open>
+ A transitive relation is well-founded iff it is ``locally'' well-founded,
+ i.e., iff its restriction to the lower bounds of of any element is
+ well-founded.
+\<close>
lemma trans_wf_iff:
-assumes "trans r"
-shows "wf r = (\<forall>a. wf(r Int (r^-1``{a} \<times> r^-1``{a})))"
-proof-
- obtain R where R_def: "R = (\<lambda> a. r Int (r^-1``{a} \<times> r^-1``{a}))" by blast
- {assume *: "wf r"
- {fix a
- have "wf(R a)"
- using * R_def wf_subset[of r "R a"] by auto
- }
- }
- (* *)
+ assumes "trans r"
+ shows "wf r \<longleftrightarrow> (\<forall>a. wf (r \<inter> (r\<inverse>``{a} \<times> r\<inverse>``{a})))"
+proof -
+ define R where "R a = r \<inter> (r\<inverse>``{a} \<times> r\<inverse>``{a})" for a
+ have "wf (R a)" if "wf r" for a
+ using that R_def wf_subset[of r "R a"] by auto
moreover
- {assume *: "\<forall>a. wf(R a)"
- have "wf r"
- proof(unfold wf_def, clarify)
- fix phi a
- assume **: "\<forall>a. (\<forall>b. (b,a) \<in> r \<longrightarrow> phi b) \<longrightarrow> phi a"
- obtain chi where chi_def: "chi = (\<lambda>b. (b,a) \<in> r \<longrightarrow> phi b)" by blast
- with * have "wf (R a)" by auto
- hence "(\<forall>b. (\<forall>c. (c,b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b) \<longrightarrow> (\<forall>b. chi b)"
- unfolding wf_def by blast
- moreover
- have "\<forall>b. (\<forall>c. (c,b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b"
- proof(auto simp add: chi_def R_def)
- fix b
- assume 1: "(b,a) \<in> r" and 2: "\<forall>c. (c, b) \<in> r \<and> (c, a) \<in> r \<longrightarrow> phi c"
- hence "\<forall>c. (c, b) \<in> r \<longrightarrow> phi c"
- using assms trans_def[of r] by blast
- thus "phi b" using ** by blast
- qed
- ultimately have "\<forall>b. chi b" by (rule mp)
- with ** chi_def show "phi a" by blast
- qed
- }
- ultimately show ?thesis using R_def by blast
+ have "wf r" if *: "\<forall>a. wf(R a)"
+ unfolding wf_def
+ proof clarify
+ fix phi a
+ assume **: "\<forall>a. (\<forall>b. (b, a) \<in> r \<longrightarrow> phi b) \<longrightarrow> phi a"
+ define chi where "chi b \<longleftrightarrow> (b, a) \<in> r \<longrightarrow> phi b" for b
+ with * have "wf (R a)" by auto
+ then have "(\<forall>b. (\<forall>c. (c, b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b) \<longrightarrow> (\<forall>b. chi b)"
+ unfolding wf_def by blast
+ also have "\<forall>b. (\<forall>c. (c, b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b"
+ proof (auto simp add: chi_def R_def)
+ fix b
+ assume "(b, a) \<in> r" and "\<forall>c. (c, b) \<in> r \<and> (c, a) \<in> r \<longrightarrow> phi c"
+ then have "\<forall>c. (c, b) \<in> r \<longrightarrow> phi c"
+ using assms trans_def[of r] by blast
+ with ** show "phi b" by blast
+ qed
+ finally have "\<forall>b. chi b" .
+ with ** chi_def show "phi a" by blast
+ qed
+ ultimately show ?thesis unfolding R_def by blast
qed
text \<open>The next lemma is a variation of \<open>wf_eq_minimal\<close> from Wellfounded,
-allowing one to assume the set included in the field.\<close>
+ allowing one to assume the set included in the field.\<close>
-lemma wf_eq_minimal2:
-"wf r = (\<forall>A. A <= Field r \<and> A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. \<not> (a',a) \<in> r))"
+lemma wf_eq_minimal2: "wf r \<longleftrightarrow> (\<forall>A. A \<subseteq> Field r \<and> A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a', a) \<notin> r))"
proof-
- let ?phi = "\<lambda> A. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. \<not> (a',a) \<in> r)"
- have "wf r = (\<forall>A. ?phi A)"
- by (auto simp: ex_in_conv [THEN sym], erule wfE_min, assumption, blast)
- (rule wfI_min, fast)
- (* *)
- also have "(\<forall>A. ?phi A) = (\<forall>B \<le> Field r. ?phi B)"
+ let ?phi = "\<lambda>A. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r)"
+ have "wf r \<longleftrightarrow> (\<forall>A. ?phi A)"
+ apply (auto simp: ex_in_conv [THEN sym])
+ apply (erule wfE_min)
+ apply assumption
+ apply blast
+ apply (rule wfI_min)
+ apply fast
+ done
+ also have "(\<forall>A. ?phi A) \<longleftrightarrow> (\<forall>B \<subseteq> Field r. ?phi B)"
proof
assume "\<forall>A. ?phi A"
- thus "\<forall>B \<le> Field r. ?phi B" by simp
+ then show "\<forall>B \<subseteq> Field r. ?phi B" by simp
next
- assume *: "\<forall>B \<le> Field r. ?phi B"
+ assume *: "\<forall>B \<subseteq> Field r. ?phi B"
show "\<forall>A. ?phi A"
- proof(clarify)
- fix A::"'a set" assume **: "A \<noteq> {}"
- obtain B where B_def: "B = A Int (Field r)" by blast
- show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r"
- proof(cases "B = {}")
- assume Case1: "B = {}"
- obtain a where 1: "a \<in> A \<and> a \<notin> Field r"
- using ** Case1 unfolding B_def by blast
- hence "\<forall>a' \<in> A. (a',a) \<notin> r" using 1 unfolding Field_def by blast
- thus ?thesis using 1 by blast
+ proof clarify
+ fix A :: "'a set"
+ assume **: "A \<noteq> {}"
+ define B where "B = A \<inter> Field r"
+ show "\<exists>a \<in> A. \<forall>a' \<in> A. (a', a) \<notin> r"
+ proof (cases "B = {}")
+ case True
+ with ** obtain a where a: "a \<in> A" "a \<notin> Field r"
+ unfolding B_def by blast
+ with a have "\<forall>a' \<in> A. (a',a) \<notin> r"
+ unfolding Field_def by blast
+ with a show ?thesis by blast
next
- assume Case2: "B \<noteq> {}" have 1: "B \<le> Field r" unfolding B_def by blast
- obtain a where 2: "a \<in> B \<and> (\<forall>a' \<in> B. (a',a) \<notin> r)"
- using Case2 1 * by blast
- have "\<forall>a' \<in> A. (a',a) \<notin> r"
- proof(clarify)
- fix a' assume "a' \<in> A" and **: "(a',a) \<in> r"
- hence "a' \<in> B" unfolding B_def Field_def by blast
- thus False using 2 ** by blast
+ case False
+ have "B \<subseteq> Field r" unfolding B_def by blast
+ with False * obtain a where a: "a \<in> B" "\<forall>a' \<in> B. (a', a) \<notin> r"
+ by blast
+ have "(a', a) \<notin> r" if "a' \<in> A" for a'
+ proof
+ assume a'a: "(a', a) \<in> r"
+ with that have "a' \<in> B" unfolding B_def Field_def by blast
+ with a a'a show False by blast
qed
- thus ?thesis using 2 unfolding B_def by blast
+ with a show ?thesis unfolding B_def by blast
qed
qed
qed
@@ -441,58 +451,67 @@
subsubsection \<open>Characterizations of well-foundedness\<close>
-text \<open>The next lemma and its corollary enable one to prove that
-a linear order is a well-order in a way which is more standard than
-via well-foundedness of the strict version of the relation.\<close>
+text \<open>
+ The next lemma and its corollary enable one to prove that a linear order is
+ a well-order in a way which is more standard than via well-foundedness of
+ the strict version of the relation.
+\<close>
lemma Linear_order_wf_diff_Id:
-assumes LI: "Linear_order r"
-shows "wf(r - Id) = (\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r))"
-proof(cases "r \<le> Id")
- assume Case1: "r \<le> Id"
- hence temp: "r - Id = {}" by blast
- hence "wf(r - Id)" by (simp add: temp)
- moreover
- {fix A assume *: "A \<le> Field r" and **: "A \<noteq> {}"
- obtain a where 1: "r = {} \<or> r = {(a,a)}" using LI
- unfolding order_on_defs using Case1 Total_subset_Id by auto
- hence "A = {a} \<and> r = {(a,a)}" using * ** unfolding Field_def by blast
- hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" using 1 by blast
- }
+ assumes "Linear_order r"
+ shows "wf (r - Id) \<longleftrightarrow> (\<forall>A \<subseteq> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a, a') \<in> r))"
+proof (cases "r \<subseteq> Id")
+ case True
+ then have *: "r - Id = {}" by blast
+ have "wf (r - Id)" by (simp add: *)
+ moreover have "\<exists>a \<in> A. \<forall>a' \<in> A. (a, a') \<in> r"
+ if *: "A \<subseteq> Field r" and **: "A \<noteq> {}" for A
+ proof -
+ from \<open>Linear_order r\<close> True
+ obtain a where a: "r = {} \<or> r = {(a, a)}"
+ unfolding order_on_defs using Total_subset_Id [of r] by blast
+ with * ** have "A = {a} \<and> r = {(a, a)}"
+ unfolding Field_def by blast
+ with a show ?thesis by blast
+ qed
ultimately show ?thesis by blast
next
- assume Case2: "\<not> r \<le> Id"
- hence 1: "Field r = Field(r - Id)" using Total_Id_Field LI
- unfolding order_on_defs by blast
+ case False
+ with \<open>Linear_order r\<close> have Field: "Field r = Field (r - Id)"
+ unfolding order_on_defs using Total_Id_Field [of r] by blast
show ?thesis
proof
- assume *: "wf(r - Id)"
- show "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)"
- proof(clarify)
- fix A assume **: "A \<le> Field r" and ***: "A \<noteq> {}"
- hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id"
- using 1 * unfolding wf_eq_minimal2 by simp
- moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. ((a,a') \<in> r) = ((a',a) \<notin> r - Id)"
- using Linear_order_in_diff_Id[of r] ** LI by blast
- ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" by blast
+ assume *: "wf (r - Id)"
+ show "\<forall>A \<subseteq> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a, a') \<in> r)"
+ proof clarify
+ fix A
+ assume **: "A \<subseteq> Field r" and ***: "A \<noteq> {}"
+ then have "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id"
+ using Field * unfolding wf_eq_minimal2 by simp
+ moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. (a, a') \<in> r \<longleftrightarrow> (a', a) \<notin> r - Id"
+ using Linear_order_in_diff_Id [OF \<open>Linear_order r\<close>] ** by blast
+ ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a, a') \<in> r" by blast
qed
next
- assume *: "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)"
- show "wf(r - Id)"
- proof(unfold wf_eq_minimal2, clarify)
- fix A assume **: "A \<le> Field(r - Id)" and ***: "A \<noteq> {}"
- hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r"
- using 1 * by simp
- moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. ((a,a') \<in> r) = ((a',a) \<notin> r - Id)"
- using Linear_order_in_diff_Id[of r] ** LI mono_Field[of "r - Id" r] by blast
- ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id" by blast
+ assume *: "\<forall>A \<subseteq> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a, a') \<in> r)"
+ show "wf (r - Id)"
+ unfolding wf_eq_minimal2
+ proof clarify
+ fix A
+ assume **: "A \<subseteq> Field(r - Id)" and ***: "A \<noteq> {}"
+ then have "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r"
+ using Field * by simp
+ moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. (a, a') \<in> r \<longleftrightarrow> (a', a) \<notin> r - Id"
+ using Linear_order_in_diff_Id [OF \<open>Linear_order r\<close>] ** mono_Field[of "r - Id" r] by blast
+ ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id"
+ by blast
qed
qed
qed
corollary Linear_order_Well_order_iff:
-assumes "Linear_order r"
-shows "Well_order r = (\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r))"
-using assms unfolding well_order_on_def using Linear_order_wf_diff_Id[of r] by blast
+ "Linear_order r \<Longrightarrow>
+ Well_order r \<longleftrightarrow> (\<forall>A \<subseteq> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a, a') \<in> r))"
+ unfolding well_order_on_def using Linear_order_wf_diff_Id[of r] by blast
end