(* Title: HOL/Order_Relation.thy Author: Tobias Nipkow Author: Andrei Popescu, TU Muenchen *) section ‹Orders as Relations› theory Order_Relation imports Wfrec begin subsection ‹Orders on a set› 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 ‹Orders on the field› 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 ⊆ r `` B ⟷ (∀a∈A.∃b∈B. (b, a) ∈ 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 ‹antisym r›[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)" proof - have "Field r ⊆ Field (r - Id)" proof (rule subsetI) 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 * ‹Total r› have "(a, d) ∈ r ∨ (d, a) ∈ r" by (simp add: total_on_def) with ‹d ≠ a› show "a ∈ Field (r - Id)" unfolding Field_def by blast qed then show ?thesis using mono_Field[of "r - Id" r] Diff_subset[of r Id] by auto qed subsection‹Relations given by a predicate and the field› 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 ‹Orders on a type› abbreviation "strict_linear_order ≡ strict_linear_order_on UNIV" abbreviation "linear_order ≡ linear_order_on UNIV" abbreviation "well_order ≡ well_order_on UNIV" subsection ‹Order-like relations› text ‹ 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. › subsubsection ‹Auxiliaries› 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 ‹r ⊆ Id› 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 ‹Total r› unfolding total_on_def by blast with ‹r ⊆ Id› 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 ‹The upper and lower bounds operators› text ‹ Here we define upper (``above") and lower (``below") bounds operators. We think of ‹r› as a ∗‹non-strict› relation. The suffix ‹S› at the names of some operators indicates that the bounds are strict -- e.g., ‹underS a› is the set of all strict lower bounds of ‹a› (w.r.t. ‹r›). Capitalization of the first letter in the name reminds that the operator acts on sets, rather than on individual elements. › 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 ‹ Note: In the definitions of ‹Above[S]› and ‹Under[S]›, we bounded comprehension by ‹Field r› in order to properly cover the case of ‹A› being empty. › 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 safe 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 safe assume *: "b ≠ a" and **: "(b, a) ∈ r" with ‹antisym r› antisym_def[of r] ab show False by blast next fix x assume "x ≠ a" "(x, a) ∈ r" with ab ‹trans r› trans_def[of r] show "(x, b) ∈ 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 ‹Linear_order r› 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 ‹auto simp: aboveS_def intro: FieldI2›) 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 ‹auto simp: aboveS_def intro: FieldI2›) qed subsection ‹Variations on Well-Founded Relations› text ‹ This subsection contains some variations of the results from \<^theory>‹HOL.Wellfounded›: ▪ means for slightly more direct definitions by well-founded recursion; ▪ variations of well-founded induction; ▪ means for proving a linear order to be a well-order. › subsubsection ‹Characterizations of well-foundedness› text ‹ 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. › 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 safe fix b assume "∀c. (c, b) ∈ R a ⟶ chi c" moreover have "(b, a) ∈ r ⟹ ∀c. (c, b) ∈ r ∧ (c, a) ∈ r ⟶ phi c ⟹ phi b" proof - 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 ultimately show "chi b" by (auto simp add: chi_def R_def) 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‹A transitive relation is well-founded if all initial segments are finite.› corollary wf_finite_segments: assumes "irrefl r" and "trans r" and "⋀x. finite {y. (y, x) ∈ r}" shows "wf r" proof - have "⋀a. acyclic (r ∩ {x. (x, a) ∈ r} × {x. (x, a) ∈ r})" proof - 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 then show ?thesis by (clarsimp simp: trans_wf_iff wf_iff_acyclic_if_finite converse_def assms) qed text ‹The next lemma is a variation of ‹wf_eq_minimal› from Wellfounded, allowing one to assume the set included in the field.› 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)" proof assume "wf r" show "∀A. ?phi A" proof clarify fix A:: "'a set" assume "A ≠ {}" then obtain x where "x ∈ A" by auto show "∃a∈A. ∀a'∈A. (a', a) ∉ r" apply (rule wfE_min[of r x A]) apply fact+ by blast qed next assume *: "∀A. ?phi A" then show "wf r" apply (clarsimp simp: ex_in_conv [THEN sym]) apply (rule wfI_min) by fast qed 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) ∈ 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 ‹Characterizations of well-foundedness› text ‹ 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. › 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 ‹Linear_order r› 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 ‹Linear_order r› 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 ‹Linear_order r›] ** 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 ‹Linear_order r›] ** 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 ⟷ (∀A ⊆ Field r. A ≠ {} ⟶ (∃a ∈ A. ∀a' ∈ A. (a, a') ∈ r))" unfolding well_order_on_def using Linear_order_wf_diff_Id[of r] by blast end