(* Title: HOL/Cardinals/Order_Relation_More.thy Author: Andrei Popescu, TU Muenchen Copyright 2012 Basics on order-like relations. *) section ‹Basics on Order-Like Relations› theory Order_Relation_More imports Main begin subsection ‹The upper and lower bounds operators› lemma aboveS_subset_above: "aboveS r a ≤ above r a" by(auto simp add: aboveS_def above_def) lemma AboveS_subset_Above: "AboveS r A ≤ Above r A" by(auto simp add: AboveS_def Above_def) lemma UnderS_disjoint: "A Int (UnderS r A) = {}" by(auto simp add: UnderS_def) lemma aboveS_notIn: "a ∉ aboveS r a" by(auto simp add: aboveS_def) lemma Refl_above_in: "⟦Refl r; a ∈ Field r⟧ ⟹ a ∈ above r a" by(auto simp add: refl_on_def above_def) lemma in_Above_under: "a ∈ Field r ⟹ a ∈ Above r (under r a)" by(auto simp add: Above_def under_def) lemma in_Under_above: "a ∈ Field r ⟹ a ∈ Under r (above r a)" by(auto simp add: Under_def above_def) lemma in_UnderS_aboveS: "a ∈ Field r ⟹ a ∈ UnderS r (aboveS r a)" by(auto simp add: UnderS_def aboveS_def) lemma UnderS_subset_Under: "UnderS r A ≤ Under r A" by(auto simp add: UnderS_def Under_def) lemma subset_Above_Under: "B ≤ Field r ⟹ B ≤ Above r (Under r B)" by(auto simp add: Above_def Under_def) lemma subset_Under_Above: "B ≤ Field r ⟹ B ≤ Under r (Above r B)" by(auto simp add: Under_def Above_def) lemma subset_AboveS_UnderS: "B ≤ Field r ⟹ B ≤ AboveS r (UnderS r B)" by(auto simp add: AboveS_def UnderS_def) lemma subset_UnderS_AboveS: "B ≤ Field r ⟹ B ≤ UnderS r (AboveS r B)" by(auto simp add: UnderS_def AboveS_def) lemma Under_Above_Galois: "⟦B ≤ Field r; C ≤ Field r⟧ ⟹ (B ≤ Above r C) = (C ≤ Under r B)" by(unfold Above_def Under_def, blast) lemma UnderS_AboveS_Galois: "⟦B ≤ Field r; C ≤ Field r⟧ ⟹ (B ≤ AboveS r C) = (C ≤ UnderS r B)" by(unfold AboveS_def UnderS_def, blast) lemma Refl_above_aboveS: assumes REFL: "Refl r" and IN: "a ∈ Field r" shows "above r a = aboveS r a ∪ {a}" proof(unfold above_def aboveS_def, auto) show "(a,a) ∈ r" using REFL IN refl_on_def[of _ r] by blast qed lemma Linear_order_under_aboveS_Field: assumes LIN: "Linear_order r" and IN: "a ∈ Field r" shows "Field r = under r a ∪ aboveS r a" proof(unfold under_def aboveS_def, auto) assume "a ∈ Field r" "(a, a) ∉ r" with LIN IN order_on_defs[of _ r] refl_on_def[of _ r] show False by auto next fix b assume "b ∈ Field r" "(b, a) ∉ r" with LIN IN order_on_defs[of "Field r" r] total_on_def[of "Field r" r] have "(a,b) ∈ r ∨ a = b" by blast thus "(a,b) ∈ r" using LIN IN order_on_defs[of _ r] refl_on_def[of _ r] by auto next fix b assume "(b, a) ∈ r" thus "b ∈ Field r" using LIN order_on_defs[of _ r] refl_on_def[of _ r] by blast next fix b assume "b ≠ a" "(a, b) ∈ r" thus "b ∈ Field r" using LIN order_on_defs[of "Field r" r] refl_on_def[of "Field r" r] by blast qed lemma Linear_order_underS_above_Field: assumes LIN: "Linear_order r" and IN: "a ∈ Field r" shows "Field r = underS r a ∪ above r a" proof(unfold underS_def above_def, auto) assume "a ∈ Field r" "(a, a) ∉ r" with LIN IN order_on_defs[of _ r] refl_on_def[of _ r] show False by metis next fix b assume "b ∈ Field r" "(a, b) ∉ r" with LIN IN order_on_defs[of "Field r" r] total_on_def[of "Field r" r] have "(b,a) ∈ r ∨ b = a" by blast thus "(b,a) ∈ r" using LIN IN order_on_defs[of _ r] refl_on_def[of _ r] by auto next fix b assume "b ≠ a" "(b, a) ∈ r" thus "b ∈ Field r" using LIN order_on_defs[of _ r] refl_on_def[of _ r] by blast next fix b assume "(a, b) ∈ r" thus "b ∈ Field r" using LIN order_on_defs[of "Field r" r] refl_on_def[of "Field r" r] by blast qed lemma under_empty: "a ∉ Field r ⟹ under r a = {}" unfolding Field_def under_def by auto lemma Under_Field: "Under r A ≤ Field r" by(unfold Under_def Field_def, auto) lemma UnderS_Field: "UnderS r A ≤ Field r" by(unfold UnderS_def Field_def, auto) lemma above_Field: "above r a ≤ Field r" by(unfold above_def Field_def, auto) lemma aboveS_Field: "aboveS r a ≤ Field r" by(unfold aboveS_def Field_def, auto) lemma Above_Field: "Above r A ≤ Field r" by(unfold Above_def Field_def, auto) lemma Refl_under_Under: assumes REFL: "Refl r" and NE: "A ≠ {}" shows "Under r A = (⋂a ∈ A. under r a)" proof show "Under r A ⊆ (⋂a ∈ A. under r a)" by(unfold Under_def under_def, auto) next show "(⋂a ∈ A. under r a) ⊆ Under r A" proof(auto) fix x assume *: "∀xa ∈ A. x ∈ under r xa" hence "∀xa ∈ A. (x,xa) ∈ r" by (simp add: under_def) moreover {from NE obtain a where "a ∈ A" by blast with * have "x ∈ under r a" by simp hence "x ∈ Field r" using under_Field[of r a] by auto } ultimately show "x ∈ Under r A" unfolding Under_def by auto qed qed lemma Refl_underS_UnderS: assumes REFL: "Refl r" and NE: "A ≠ {}" shows "UnderS r A = (⋂a ∈ A. underS r a)" proof show "UnderS r A ⊆ (⋂a ∈ A. underS r a)" by(unfold UnderS_def underS_def, auto) next show "(⋂a ∈ A. underS r a) ⊆ UnderS r A" proof(auto) fix x assume *: "∀xa ∈ A. x ∈ underS r xa" hence "∀xa ∈ A. x ≠ xa ∧ (x,xa) ∈ r" by (auto simp add: underS_def) moreover {from NE obtain a where "a ∈ A" by blast with * have "x ∈ underS r a" by simp hence "x ∈ Field r" using underS_Field[of _ r a] by auto } ultimately show "x ∈ UnderS r A" unfolding UnderS_def by auto qed qed lemma Refl_above_Above: assumes REFL: "Refl r" and NE: "A ≠ {}" shows "Above r A = (⋂a ∈ A. above r a)" proof show "Above r A ⊆ (⋂a ∈ A. above r a)" by(unfold Above_def above_def, auto) next show "(⋂a ∈ A. above r a) ⊆ Above r A" proof(auto) fix x assume *: "∀xa ∈ A. x ∈ above r xa" hence "∀xa ∈ A. (xa,x) ∈ r" by (simp add: above_def) moreover {from NE obtain a where "a ∈ A" by blast with * have "x ∈ above r a" by simp hence "x ∈ Field r" using above_Field[of r a] by auto } ultimately show "x ∈ Above r A" unfolding Above_def by auto qed qed lemma Refl_aboveS_AboveS: assumes REFL: "Refl r" and NE: "A ≠ {}" shows "AboveS r A = (⋂a ∈ A. aboveS r a)" proof show "AboveS r A ⊆ (⋂a ∈ A. aboveS r a)" by(unfold AboveS_def aboveS_def, auto) next show "(⋂a ∈ A. aboveS r a) ⊆ AboveS r A" proof(auto) fix x assume *: "∀xa ∈ A. x ∈ aboveS r xa" hence "∀xa ∈ A. xa ≠ x ∧ (xa,x) ∈ r" by (auto simp add: aboveS_def) moreover {from NE obtain a where "a ∈ A" by blast with * have "x ∈ aboveS r a" by simp hence "x ∈ Field r" using aboveS_Field[of r a] by auto } ultimately show "x ∈ AboveS r A" unfolding AboveS_def by auto qed qed lemma under_Under_singl: "under r a = Under r {a}" by(unfold Under_def under_def, auto simp add: Field_def) lemma underS_UnderS_singl: "underS r a = UnderS r {a}" by(unfold UnderS_def underS_def, auto simp add: Field_def) lemma above_Above_singl: "above r a = Above r {a}" by(unfold Above_def above_def, auto simp add: Field_def) lemma aboveS_AboveS_singl: "aboveS r a = AboveS r {a}" by(unfold AboveS_def aboveS_def, auto simp add: Field_def) lemma Under_decr: "A ≤ B ⟹ Under r B ≤ Under r A" by(unfold Under_def, auto) lemma UnderS_decr: "A ≤ B ⟹ UnderS r B ≤ UnderS r A" by(unfold UnderS_def, auto) lemma Above_decr: "A ≤ B ⟹ Above r B ≤ Above r A" by(unfold Above_def, auto) lemma AboveS_decr: "A ≤ B ⟹ AboveS r B ≤ AboveS r A" by(unfold AboveS_def, auto) lemma under_incl_iff: assumes TRANS: "trans r" and REFL: "Refl r" and IN: "a ∈ Field r" shows "(under r a ≤ under r b) = ((a,b) ∈ r)" proof assume "(a,b) ∈ r" thus "under r a ≤ under r b" using TRANS by (auto simp add: under_incr) next assume "under r a ≤ under r b" moreover have "a ∈ under r a" using REFL IN by (auto simp add: Refl_under_in) ultimately show "(a,b) ∈ r" by (auto simp add: under_def) qed lemma above_decr: assumes TRANS: "trans r" and REL: "(a,b) ∈ r" shows "above r b ≤ above r a" proof(unfold above_def, auto) fix x assume "(b,x) ∈ r" with REL TRANS trans_def[of r] show "(a,x) ∈ r" by blast qed lemma aboveS_decr: assumes TRANS: "trans r" and ANTISYM: "antisym r" and REL: "(a,b) ∈ r" shows "aboveS r b ≤ aboveS r a" proof(unfold aboveS_def, auto) assume *: "a ≠ b" and **: "(b,a) ∈ r" with ANTISYM antisym_def[of r] REL show False by auto next fix x assume "x ≠ b" "(b,x) ∈ r" with REL TRANS trans_def[of r] show "(a,x) ∈ r" by blast qed lemma under_trans: assumes TRANS: "trans r" and IN1: "a ∈ under r b" and IN2: "b ∈ under r c" shows "a ∈ under r c" proof- have "(a,b) ∈ r ∧ (b,c) ∈ r" using IN1 IN2 under_def by fastforce hence "(a,c) ∈ r" using TRANS trans_def[of r] by blast thus ?thesis unfolding under_def by simp qed lemma under_underS_trans: assumes TRANS: "trans r" and ANTISYM: "antisym r" and IN1: "a ∈ under r b" and IN2: "b ∈ underS r c" shows "a ∈ underS r c" proof- have 0: "(a,b) ∈ r ∧ (b,c) ∈ r" using IN1 IN2 under_def underS_def by fastforce hence 1: "(a,c) ∈ r" using TRANS trans_def[of r] by blast have 2: "b ≠ c" using IN2 underS_def by force have 3: "a ≠ c" proof assume "a = c" with 0 2 ANTISYM antisym_def[of r] show False by auto qed from 1 3 show ?thesis unfolding underS_def by simp qed lemma underS_under_trans: assumes TRANS: "trans r" and ANTISYM: "antisym r" and IN1: "a ∈ underS r b" and IN2: "b ∈ under r c" shows "a ∈ underS r c" proof- have 0: "(a,b) ∈ r ∧ (b,c) ∈ r" using IN1 IN2 under_def underS_def by fast hence 1: "(a,c) ∈ r" using TRANS trans_def[of r] by fast have 2: "a ≠ b" using IN1 underS_def by force have 3: "a ≠ c" proof assume "a = c" with 0 2 ANTISYM antisym_def[of r] show False by auto qed from 1 3 show ?thesis unfolding underS_def by simp qed lemma underS_underS_trans: assumes TRANS: "trans r" and ANTISYM: "antisym r" and IN1: "a ∈ underS r b" and IN2: "b ∈ underS r c" shows "a ∈ underS r c" proof- have "a ∈ under r b" using IN1 underS_subset_under by fast with assms under_underS_trans show ?thesis by fast qed lemma above_trans: assumes TRANS: "trans r" and IN1: "b ∈ above r a" and IN2: "c ∈ above r b" shows "c ∈ above r a" proof- have "(a,b) ∈ r ∧ (b,c) ∈ r" using IN1 IN2 above_def by fast hence "(a,c) ∈ r" using TRANS trans_def[of r] by blast thus ?thesis unfolding above_def by simp qed lemma above_aboveS_trans: assumes TRANS: "trans r" and ANTISYM: "antisym r" and IN1: "b ∈ above r a" and IN2: "c ∈ aboveS r b" shows "c ∈ aboveS r a" proof- have 0: "(a,b) ∈ r ∧ (b,c) ∈ r" using IN1 IN2 above_def aboveS_def by fast hence 1: "(a,c) ∈ r" using TRANS trans_def[of r] by blast have 2: "b ≠ c" using IN2 aboveS_def by force have 3: "a ≠ c" proof assume "a = c" with 0 2 ANTISYM antisym_def[of r] show False by auto qed from 1 3 show ?thesis unfolding aboveS_def by simp qed lemma aboveS_above_trans: assumes TRANS: "trans r" and ANTISYM: "antisym r" and IN1: "b ∈ aboveS r a" and IN2: "c ∈ above r b" shows "c ∈ aboveS r a" proof- have 0: "(a,b) ∈ r ∧ (b,c) ∈ r" using IN1 IN2 above_def aboveS_def by fast hence 1: "(a,c) ∈ r" using TRANS trans_def[of r] by blast have 2: "a ≠ b" using IN1 aboveS_def by force have 3: "a ≠ c" proof assume "a = c" with 0 2 ANTISYM antisym_def[of r] show False by auto qed from 1 3 show ?thesis unfolding aboveS_def by simp qed lemma aboveS_aboveS_trans: assumes TRANS: "trans r" and ANTISYM: "antisym r" and IN1: "b ∈ aboveS r a" and IN2: "c ∈ aboveS r b" shows "c ∈ aboveS r a" proof- have "b ∈ above r a" using IN1 aboveS_subset_above by fast with assms above_aboveS_trans show ?thesis by fast qed lemma under_Under_trans: assumes TRANS: "trans r" and IN1: "a ∈ under r b" and IN2: "b ∈ Under r C" shows "a ∈ Under r C" proof- have "b ∈ {u ∈ Field r. ∀x. x ∈ C ⟶ (u, x) ∈ r}" using IN2 Under_def by force hence "(a,b) ∈ r ∧ (∀c ∈ C. (b,c) ∈ r)" using IN1 under_def by fast hence "∀c ∈ C. (a,c) ∈ r" using TRANS trans_def[of r] by blast moreover have "a ∈ Field r" using IN1 unfolding Field_def under_def by blast ultimately show ?thesis unfolding Under_def by blast qed lemma underS_Under_trans: assumes TRANS: "trans r" and ANTISYM: "antisym r" and IN1: "a ∈ underS r b" and IN2: "b ∈ Under r C" shows "a ∈ UnderS r C" proof- from IN1 have "a ∈ under r b" using underS_subset_under[of r b] by fast with assms under_Under_trans have "a ∈ Under r C" by fast (* *) moreover have "a ∉ C" proof assume *: "a ∈ C" have 1: "b ≠ a ∧ (a,b) ∈ r" using IN1 underS_def[of r b] by auto have "∀c ∈ C. (b,c) ∈ r" using IN2 Under_def[of r C] by auto with * have "(b,a) ∈ r" by simp with 1 ANTISYM antisym_def[of r] show False by blast qed (* *) ultimately show ?thesis unfolding UnderS_def using Under_def by force qed lemma underS_UnderS_trans: assumes TRANS: "trans r" and ANTISYM: "antisym r" and IN1: "a ∈ underS r b" and IN2: "b ∈ UnderS r C" shows "a ∈ UnderS r C" proof- from IN2 have "b ∈ Under r C" using UnderS_subset_Under[of r C] by blast with underS_Under_trans assms show ?thesis by force qed lemma above_Above_trans: assumes TRANS: "trans r" and IN1: "a ∈ above r b" and IN2: "b ∈ Above r C" shows "a ∈ Above r C" proof- have "(b,a) ∈ r ∧ (∀c ∈ C. (c,b) ∈ r)" using IN1[unfolded above_def] IN2[unfolded Above_def] by simp hence "∀c ∈ C. (c,a) ∈ r" using TRANS trans_def[of r] by blast moreover have "a ∈ Field r" using IN1[unfolded above_def] Field_def by fast ultimately show ?thesis unfolding Above_def by auto qed lemma aboveS_Above_trans: assumes TRANS: "trans r" and ANTISYM: "antisym r" and IN1: "a ∈ aboveS r b" and IN2: "b ∈ Above r C" shows "a ∈ AboveS r C" proof- from IN1 have "a ∈ above r b" using aboveS_subset_above[of r b] by blast with assms above_Above_trans have "a ∈ Above r C" by fast (* *) moreover have "a ∉ C" proof assume *: "a ∈ C" have 1: "b ≠ a ∧ (b,a) ∈ r" using IN1 aboveS_def[of r b] by auto have "∀c ∈ C. (c,b) ∈ r" using IN2 Above_def[of r C] by auto with * have "(a,b) ∈ r" by simp with 1 ANTISYM antisym_def[of r] show False by blast qed (* *) ultimately show ?thesis unfolding AboveS_def using Above_def by force qed lemma above_AboveS_trans: assumes TRANS: "trans r" and ANTISYM: "antisym r" and IN1: "a ∈ above r b" and IN2: "b ∈ AboveS r C" shows "a ∈ AboveS r C" proof- from IN2 have "b ∈ Above r C" using AboveS_subset_Above[of r C] by blast with assms above_Above_trans have "a ∈ Above r C" by force (* *) moreover have "a ∉ C" proof assume *: "a ∈ C" have 1: "(b,a) ∈ r" using IN1 above_def[of r b] by auto have "∀c ∈ C. b ≠ c ∧ (c,b) ∈ r" using IN2 AboveS_def[of r C] by auto with * have "b ≠ a ∧ (a,b) ∈ r" by simp with 1 ANTISYM antisym_def[of r] show False by blast qed (* *) ultimately show ?thesis unfolding AboveS_def using Above_def by force qed lemma aboveS_AboveS_trans: assumes TRANS: "trans r" and ANTISYM: "antisym r" and IN1: "a ∈ aboveS r b" and IN2: "b ∈ AboveS r C" shows "a ∈ AboveS r C" proof- from IN2 have "b ∈ Above r C" using AboveS_subset_Above[of r C] by blast with aboveS_Above_trans assms show ?thesis by force qed lemma under_UnderS_trans: assumes TRANS: "trans r" and ANTISYM: "antisym r" and IN1: "a ∈ under r b" and IN2: "b ∈ UnderS r C" shows "a ∈ UnderS r C" proof- from IN2 have "b ∈ Under r C" using UnderS_subset_Under[of r C] by blast with assms under_Under_trans have "a ∈ Under r C" by force (* *) moreover have "a ∉ C" proof assume *: "a ∈ C" have 1: "(a,b) ∈ r" using IN1 under_def[of r b] by auto have "∀c ∈ C. b ≠ c ∧ (b,c) ∈ r" using IN2 UnderS_def[of r C] by blast with * have "b ≠ a ∧ (b,a) ∈ r" by blast with 1 ANTISYM antisym_def[of r] show False by blast qed (* *) ultimately show ?thesis unfolding UnderS_def Under_def by fast qed subsection ‹Properties depending on more than one relation› lemma under_incr2: "r ≤ r' ⟹ under r a ≤ under r' a" unfolding under_def by blast lemma underS_incr2: "r ≤ r' ⟹ underS r a ≤ underS r' a" unfolding underS_def by blast (* FIXME: r ↝ r' lemma Under_incr: "r ≤ r' ⟹ Under r A ≤ Under r A" unfolding Under_def by blast lemma UnderS_incr: "r ≤ r' ⟹ UnderS r A ≤ UnderS r A" unfolding UnderS_def by blast lemma Under_incr_decr: "⟦r ≤ r'; A' ≤ A⟧ ⟹ Under r A ≤ Under r A'" unfolding Under_def by blast lemma UnderS_incr_decr: "⟦r ≤ r'; A' ≤ A⟧ ⟹ UnderS r A ≤ UnderS r A'" unfolding UnderS_def by blast *) lemma above_incr2: "r ≤ r' ⟹ above r a ≤ above r' a" unfolding above_def by blast lemma aboveS_incr2: "r ≤ r' ⟹ aboveS r a ≤ aboveS r' a" unfolding aboveS_def by blast (* FIXME lemma Above_incr: "r ≤ r' ⟹ Above r A ≤ Above r A" unfolding Above_def by blast lemma AboveS_incr: "r ≤ r' ⟹ AboveS r A ≤ AboveS r A" unfolding AboveS_def by blast lemma Above_incr_decr: "⟦r ≤ r'; A' ≤ A⟧ ⟹ Above r A ≤ Above r A'" unfolding Above_def by blast lemma AboveS_incr_decr: "⟦r ≤ r'; A' ≤ A⟧ ⟹ AboveS r A ≤ AboveS r A'" unfolding AboveS_def by blast *) end