(* Title: HOL/Order_Relation.thy
Author: Tobias Nipkow
Author: Andrei Popescu, TU Muenchen
*)
section \<open>Orders as Relations\<close>
theory Order_Relation
imports Wfrec
begin
subsection \<open>Orders on a set\<close>
definition "preorder_on A r \ refl_on A r \ trans r"
definition "partial_order_on A r \ preorder_on A r \ antisym r"
definition "linear_order_on A r \ partial_order_on A r \ total_on A r"
definition "strict_linear_order_on A r \ trans r \ irrefl r \ total_on A r"
definition "well_order_on A r \ linear_order_on A r \ wf(r - Id)"
lemmas order_on_defs =
preorder_on_def partial_order_on_def linear_order_on_def
strict_linear_order_on_def well_order_on_def
lemma partial_order_onD:
assumes "partial_order_on A r" shows "refl_on A r" and "trans r" and "antisym r"
using assms unfolding partial_order_on_def preorder_on_def by auto
lemma preorder_on_empty[simp]: "preorder_on {} {}"
by (simp add: preorder_on_def trans_def)
lemma partial_order_on_empty[simp]: "partial_order_on {} {}"
by (simp add: partial_order_on_def)
lemma lnear_order_on_empty[simp]: "linear_order_on {} {}"
by (simp add: linear_order_on_def)
lemma well_order_on_empty[simp]: "well_order_on {} {}"
by (simp add: well_order_on_def)
lemma preorder_on_converse[simp]: "preorder_on A (r\) = preorder_on A r"
by (simp add: preorder_on_def)
lemma partial_order_on_converse[simp]: "partial_order_on A (r\) = partial_order_on A r"
by (simp add: partial_order_on_def)
lemma linear_order_on_converse[simp]: "linear_order_on A (r\) = linear_order_on A r"
by (simp add: linear_order_on_def)
lemma partial_order_on_acyclic:
"partial_order_on A r \ acyclic (r - Id)"
by (simp add: acyclic_irrefl partial_order_on_def preorder_on_def trans_diff_Id)
lemma partial_order_on_well_order_on:
"finite r \ partial_order_on A r \ wf (r - Id)"
by (simp add: finite_acyclic_wf partial_order_on_acyclic)
lemma strict_linear_order_on_diff_Id: "linear_order_on A r \ 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)}"
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)
lemma linear_order_on_well_order_on:
assumes "finite r"
shows "linear_order_on A r \ well_order_on A r"
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>
abbreviation "Refl r \ refl_on (Field r) r"
abbreviation "Preorder r \ preorder_on (Field r) r"
abbreviation "Partial_order r \ partial_order_on (Field r) r"
abbreviation "Total r \ total_on (Field r) r"
abbreviation "Linear_order r \ linear_order_on (Field r) r"
abbreviation "Well_order r \ well_order_on (Field r) r"
lemma subset_Image_Image_iff:
"Preorder r \ A \ Field r \ B \ Field r \
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:
"Preorder r \ a \ Field r \ b \ Field r \ r `` {a} \ r `` {b} \ (b, a) \ r"
by (simp add: subset_Image_Image_iff)
lemma Refl_antisym_eq_Image1_Image1_iff:
assumes "Refl r"
and as: "antisym r"
and abf: "a \ Field r" "b \ Field r"
shows "r `` {a} = r `` {b} \ a = b"
(is "?lhs \ ?rhs")
proof
assume ?lhs
then have *: "\x. (a, x) \ r \ (b, x) \ r"
by (simp add: set_eq_iff)
have "(a, a) \ r" "(b, b) \ r" using \Refl r\ abf by (simp_all add: refl_on_def)
then have "(a, b) \ r" "(b, a) \ 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:
"Partial_order r \ a \ Field r \ b \ Field r \ r `` {a} = r `` {b} \ a = b"
by (auto simp: order_on_defs Refl_antisym_eq_Image1_Image1_iff)
lemma Total_Id_Field:
assumes "Total r"
and not_Id: "\ r \ 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 \ Field r"
from not_Id have "r \ {}" by fast
with not_Id obtain b and c where "b \ c \ (b,c) \ r" by auto
then have "b \ c \ {b, c} \ Field r" by (auto simp: Field_def)
with * obtain d where "d \ Field r" "d \ 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>Relations given by a predicate and the field\<close>
definition relation_of :: "('a \ 'a \ bool) \ 'a set \ ('a \ 'a) set"
where "relation_of P A \ { (a, b) \ A \ A. P a b }"
lemma Field_relation_of:
assumes "refl_on A (relation_of P A)" shows "Field (relation_of P A) = A"
using assms unfolding refl_on_def Field_def by auto
lemma partial_order_on_relation_ofI:
assumes refl: "\a. a \ A \ P a a"
and trans: "\a b c. \ a \ A; b \ A; c \ A \ \ P a b \ P b c \ P a c"
and antisym: "\a b. \ a \ A; b \ A \ \ P a b \ P b a \ a = b"
shows "partial_order_on A (relation_of P A)"
proof -
from refl have "refl_on A (relation_of P A)"
unfolding refl_on_def relation_of_def by auto
moreover have "trans (relation_of P A)" and "antisym (relation_of P A)"
unfolding relation_of_def
by (auto intro: transI dest: trans, auto intro: antisymI dest: antisym)
ultimately show ?thesis
unfolding partial_order_on_def preorder_on_def by simp
qed
lemma Partial_order_relation_ofI:
assumes "partial_order_on A (relation_of P A)" shows "Partial_order (relation_of P A)"
using Field_relation_of assms partial_order_on_def preorder_on_def by fastforce
subsection \<open>Orders on a type\<close>
abbreviation "strict_linear_order \ strict_linear_order_on UNIV"
abbreviation "linear_order \ linear_order_on UNIV"
abbreviation "well_order \ well_order_on UNIV"
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>
subsubsection \<open>Auxiliaries\<close>
lemma refl_on_domain: "refl_on A r \ (a, b) \ r \ a \ A \ b \ A"
by (auto simp add: refl_on_def)
corollary well_order_on_domain: "well_order_on A r \ (a, b) \ r \ a \ A \ b \ A"
by (auto simp add: refl_on_domain order_on_defs)
lemma well_order_on_Field: "well_order_on A r \ 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 \ A = Field r \ Well_order r"
using well_order_on_Field [of A] by auto
lemma Total_subset_Id:
assumes "Total r"
and "r \ Id"
shows "r = {} \ (\a. r = {(a, a)})"
proof -
have "\a. r = {(a, a)}" if "r \ {}"
proof -
from that obtain a b where ab: "(a, b) \ r" by fast
with \<open>r \<subseteq> Id\<close> have "a = b" by blast
with ab have aa: "(a, a) \ r" by simp
have "a = c \ a = d" if "(c, d) \ r" for c d
proof -
from that have "{a, c, d} \ Field r"
using ab unfolding Field_def by blast
then have "((a, c) \ r \ (c, a) \ r \ a = c) \ ((a, d) \ r \ (d, a) \ r \ 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 \ {(a, a)}" by auto
with aa show ?thesis by blast
qed
then show ?thesis by blast
qed
lemma Linear_order_in_diff_Id:
assumes "Linear_order r"
and "a \ Field r"
and "b \ Field r"
shows "(a, b) \ r \ (b, a) \ 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 \<^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 \ 'a \ 'a set"
where "under r a \ {b. (b, a) \ r}"
definition underS :: "'a rel \ 'a \ 'a set"
where "underS r a \ {b. b \ a \ (b, a) \ r}"
definition Under :: "'a rel \ 'a set \ 'a set"
where "Under r A \ {b \ Field r. \a \ A. (b, a) \ r}"
definition UnderS :: "'a rel \ 'a set \ 'a set"
where "UnderS r A \ {b \ Field r. \a \ A. b \ a \ (b, a) \ r}"
definition above :: "'a rel \ 'a \ 'a set"
where "above r a \ {b. (a, b) \ r}"
definition aboveS :: "'a rel \ 'a \ 'a set"
where "aboveS r a \ {b. b \ a \ (a, b) \ r}"
definition Above :: "'a rel \ 'a set \ 'a set"
where "Above r A \ {b \ Field r. \a \ A. (a, b) \ r}"
definition AboveS :: "'a rel \ 'a set \ 'a set"
where "AboveS r A \ {b \ Field r. \a \ A. b \ a \ (a, b) \ r}"
definition ofilter :: "'a rel \ 'a set \ bool"
where "ofilter r A \ A \ Field r \ (\a \ A. under r a \ 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>
lemma underS_subset_under: "underS r a \ under r a"
by (auto simp add: underS_def under_def)
lemma underS_notIn: "a \ underS r a"
by (simp add: underS_def)
lemma Refl_under_in: "Refl r \ a \ Field r \ a \ under r a"
by (simp add: refl_on_def under_def)
lemma AboveS_disjoint: "A \ (AboveS r A) = {}"
by (auto simp add: AboveS_def)
lemma in_AboveS_underS: "a \ Field r \ a \ AboveS r (underS r a)"
by (auto simp add: AboveS_def underS_def)
lemma Refl_under_underS: "Refl r \ a \ Field r \ under r a = underS r a \ {a}"
unfolding under_def underS_def
using refl_on_def[of _ r] by fastforce
lemma underS_empty: "a \ Field r \ underS r a = {}"
by (auto simp: Field_def underS_def)
lemma under_Field: "under r a \ Field r"
by (auto simp: under_def Field_def)
lemma underS_Field: "underS r a \ Field r"
by (auto simp: underS_def Field_def)
lemma underS_Field2: "a \ Field r \ underS r a \ Field r"
using underS_notIn underS_Field by fast
lemma underS_Field3: "Field r \ {} \ underS r a \ Field r"
by (cases "a \ Field r") (auto simp: underS_Field2 underS_empty)
lemma AboveS_Field: "AboveS r A \ Field r"
by (auto simp: AboveS_def Field_def)
lemma under_incr:
assumes "trans r"
and "(a, b) \ r"
shows "under r a \ under r b"
unfolding under_def
proof auto
fix x assume "(x, a) \ r"
with assms trans_def[of r] show "(x, b) \ r" by blast
qed
lemma underS_incr:
assumes "trans r"
and "antisym r"
and ab: "(a, b) \ r"
shows "underS r a \ underS r b"
unfolding underS_def
proof auto
assume *: "b \ a" and **: "(b, a) \ r"
with \<open>antisym r\<close> antisym_def[of r] ab show False
by blast
next
fix x assume "x \ a" "(x, a) \ 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 \ Field r"
and INb: "b \ Field r"
shows "underS r a \ underS r b \ (a, b) \ r"
(is "?lhs \ ?rhs")
proof
assume ?rhs
with \<open>Linear_order r\<close> show ?lhs
by (simp add: order_on_defs underS_incr)
next
assume *: ?lhs
have "(a, b) \ r" if "a = b"
using assms that by (simp add: order_on_defs refl_on_def)
moreover have False if "a \ b" "(b, a) \ r"
proof -
from that have "b \ underS r a" unfolding underS_def by blast
with * have "b \ underS r b" by blast
then show ?thesis by (simp add: underS_notIn)
qed
ultimately show "(a,b) \ r"
using assms order_on_defs[of "Field r" r] total_on_def[of "Field r" r] by blast
qed
lemma finite_Partial_order_induct[consumes 3, case_names step]:
assumes "Partial_order r"
and "x \ Field r"
and "finite r"
and step: "\x. x \ Field r \ (\y. y \ aboveS r x \ P y) \ P x"
shows "P x"
using assms(2)
proof (induct rule: wf_induct[of "r\ - Id"])
case 1
from assms(1,3) show "wf (r\ - Id)"
using partial_order_on_well_order_on partial_order_on_converse by blast
next
case prems: (2 x)
show ?case
by (rule step) (use prems in \<open>auto simp: aboveS_def intro: FieldI2\<close>)
qed
lemma finite_Linear_order_induct[consumes 3, case_names step]:
assumes "Linear_order r"
and "x \ Field r"
and "finite r"
and step: "\x. x \ Field r \ (\y. y \ aboveS r x \ P y) \ P x"
shows "P x"
using assms(2)
proof (induct rule: wf_induct[of "r\ - Id"])
case 1
from assms(1,3) show "wf (r\ - Id)"
using linear_order_on_well_order_on linear_order_on_converse
unfolding well_order_on_def by blast
next
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>\<open>HOL.Wellfounded\<close>:
\<^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>
lemma trans_wf_iff:
assumes "trans r"
shows "wf r \ (\a. wf (r \ (r\``{a} \ r\``{a})))"
proof -
define R where "R a = r \ (r\``{a} \ r\``{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
have "wf r" if *: "\a. wf(R a)"
unfolding wf_def
proof clarify
fix phi a
assume **: "\a. (\b. (b, a) \ r \ phi b) \ phi a"
define chi where "chi b \ (b, a) \ r \ phi b" for b
with * have "wf (R a)" by auto
then have "(\b. (\c. (c, b) \ R a \ chi c) \ chi b) \ (\b. chi b)"
unfolding wf_def by blast
also have "\b. (\c. (c, b) \ R a \ chi c) \ chi b"
proof (auto simp add: chi_def R_def)
fix b
assume "(b, a) \ r" and "\c. (c, b) \ r \ (c, a) \ r \ phi c"
then have "\c. (c, b) \ r \ phi c"
using assms trans_def[of r] by blast
with ** show "phi b" by blast
qed
finally have "\b. chi b" .
with ** chi_def show "phi a" by blast
qed
ultimately show ?thesis unfolding R_def by blast
qed
text\<open>A transitive relation is well-founded if all initial segments are finite.\<close>
corollary wf_finite_segments:
assumes "irrefl r" and "trans r" and "\x. finite {y. (y, x) \ r}"
shows "wf (r)"
proof (clarsimp simp: trans_wf_iff wf_iff_acyclic_if_finite converse_def assms)
fix a
have "trans (r \ ({x. (x, a) \ r} \ {x. (x, a) \ r}))"
using assms unfolding trans_def Field_def by blast
then show "acyclic (r \ {x. (x, a) \ r} \ {x. (x, a) \ r})"
using assms acyclic_def assms irrefl_def by fastforce
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>
lemma wf_eq_minimal2: "wf r \ (\A. A \ Field r \ A \ {} \ (\a \ A. \a' \ A. (a', a) \ r))"
proof-
let ?phi = "\A. A \ {} \ (\a \ A. \a' \ A. (a',a) \ r)"
have "wf r \ (\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 "(\A. ?phi A) \ (\B \ Field r. ?phi B)"
proof
assume "\A. ?phi A"
then show "\B \ Field r. ?phi B" by simp
next
assume *: "\B \ Field r. ?phi B"
show "\A. ?phi A"
proof clarify
fix A :: "'a set"
assume **: "A \ {}"
define B where "B = A \ Field r"
show "\a \ A. \a' \ A. (a', a) \ r"
proof (cases "B = {}")
case True
with ** obtain a where a: "a \ A" "a \ Field r"
unfolding B_def by blast
with a have "\a' \ A. (a',a) \ r"
unfolding Field_def by blast
with a show ?thesis by blast
next
case False
have "B \ Field r" unfolding B_def by blast
with False * obtain a where a: "a \ B" "\a' \ B. (a', a) \ r"
by blast
have "(a', a) \ r" if "a' \ A" for a'
proof
assume a'a: "(a', a) \<in> r"
with that have "a' \ B" unfolding B_def Field_def by blast
with a a'a show False by blast
qed
with a show ?thesis unfolding B_def by blast
qed
qed
qed
finally show ?thesis by blast
qed
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>
lemma Linear_order_wf_diff_Id:
assumes "Linear_order r"
shows "wf (r - Id) \ (\A \ Field r. A \ {} \ (\a \ A. \a' \ A. (a, a') \ r))"
proof (cases "r \ Id")
case True
then have *: "r - Id = {}" by blast
have "wf (r - Id)" by (simp add: *)
moreover have "\a \ A. \a' \ A. (a, a') \ r"
if *: "A \ Field r" and **: "A \ {}" for A
proof -
from \<open>Linear_order r\<close> True
obtain a where a: "r = {} \ r = {(a, a)}"
unfolding order_on_defs using Total_subset_Id [of r] by blast
with * ** have "A = {a} \ r = {(a, a)}"
unfolding Field_def by blast
with a show ?thesis by blast
qed
ultimately show ?thesis by blast
next
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 "\A \ Field r. A \ {} \ (\a \ A. \a' \ A. (a, a') \ r)"
proof clarify
fix A
assume **: "A \ Field r" and ***: "A \ {}"
then have "\a \ A. \a' \ A. (a',a) \ r - Id"
using Field * unfolding wf_eq_minimal2 by simp
moreover have "\a \ A. \a' \ A. (a, a') \ r \ (a', a) \ r - Id"
using Linear_order_in_diff_Id [OF \<open>Linear_order r\<close>] ** by blast
ultimately show "\a \ A. \a' \ A. (a, a') \ r" by blast
qed
next
assume *: "\A \ Field r. A \ {} \ (\a \ A. \a' \ A. (a, a') \ r)"
show "wf (r - Id)"
unfolding wf_eq_minimal2
proof clarify
fix A
assume **: "A \ Field(r - Id)" and ***: "A \ {}"
then have "\a \ A. \a' \ A. (a,a') \ r"
using Field * by simp
moreover have "\a \ A. \a' \ A. (a, a') \ r \ (a', a) \ r - Id"
using Linear_order_in_diff_Id [OF \<open>Linear_order r\<close>] ** mono_Field[of "r - Id" r] by blast
ultimately show "\a \ A. \a' \ A. (a',a) \ r - Id"
by blast
qed
qed
qed
corollary Linear_order_Well_order_iff:
"Linear_order r \
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
¤ Dauer der Verarbeitung: 0.4 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
