Theory Binary_Relations
section ‹Binary Relations›
text ‹We start with basic properties of binary relations.›
theory Binary_Relations
imports
Main
begin
unbundle lattice_syntax
lemma conj_iff_conj_iff_imp_iff: "Trueprop (x ∧ y ⟷ x ∧ z) ≡ (x ⟹ (y ⟷ z))"
by (auto intro!: equal_intr_rule)
lemma conj_imp_eq_imp_imp: "(P ∧ Q ⟹ PROP R) ≡ (P ⟹ Q ⟹ PROP R)"
by standard simp_all
lemma tranclp_trancl: "r⇧+⇧+ = (λx y. (x,y) ∈ {(a,b). r a b}⇧+)"
by (auto simp: tranclp_trancl_eq[symmetric])
lemma tranclp_id[simp]: "transp r ⟹ tranclp r = r"
using trancl_id[of "{(x,y). r x y}", folded transp_trans] by (auto simp:tranclp_trancl)
lemma transp_tranclp[simp]: "transp (tranclp r)" by (auto simp: tranclp_trancl transp_trans)
lemma funpow_dom: "f ` A ⊆ A ⟹ (f^^n) ` A ⊆ A" by (induct n, auto)
lemma image_subsetD: "f ` A ⊆ B ⟹ a ∈ A ⟹ f a ∈ B" by auto
text ‹Below we introduce an Isabelle-notation for $\{ \ldots x\ldots \mid x \in X \}$.›
syntax
"_range" :: "'a ⇒ idts ⇒ 'a set" ("(1{_ /|./ _})")
"_image" :: "'a ⇒ pttrn ⇒ 'a set ⇒ 'a set" ("(1{_ /|./ (_/ ∈ _)})")
translations
"{e |. p}" ⇌ "CONST range (λp. e)"
"{e |. p ∈ A}" ⇌ "CONST image (λp. e) A"
lemma image_constant:
assumes "⋀i. i ∈ I ⟹ f i = y"
shows "f ` I = (if I = {} then {} else {y})"
using assms by auto
subsection ‹Various Definitions›
text ‹Here we introduce various definitions for binary relations.
The first one is our abbreviation for the dual of a relation.›
abbreviation(input) dual ("(_⇧-)" [1000] 1000) where "r⇧- x y ≡ r y x"
lemma conversep_is_dual[simp]: "conversep = dual" by auto
lemma dual_inf: "(r ⊓ s)⇧- = r⇧- ⊓ s⇧-" by (auto intro!: ext)
text ‹Monotonicity is already defined in the library, but we want one restricted to a domain.›
lemmas monotone_onE = monotone_on_def[unfolded atomize_eq, THEN iffD1, elim_format, rule_format]
lemma monotone_on_dual: "monotone_on X r s f ⟹ monotone_on X r⇧- s⇧- f"
by (auto simp: monotone_on_def)
lemma monotone_on_id: "monotone_on X r r id"
by (auto simp: monotone_on_def)
lemma monotone_on_cmono: "A ⊆ B ⟹ monotone_on B ≤ monotone_on A"
by (intro le_funI, auto simp: monotone_on_def)
text ‹Here we define the following notions in a standard manner›
text ‹The symmetric part of a relation:›
definition sympartp where "sympartp r x y ≡ r x y ∧ r y x"
lemma sympartpI[intro]:
fixes r (infix "⊑" 50)
assumes "x ⊑ y" and "y ⊑ x" shows "sympartp (⊑) x y"
using assms by (auto simp: sympartp_def)
lemma sympartpE[elim]:
fixes r (infix "⊑" 50)
assumes "sympartp (⊑) x y" and "x ⊑ y ⟹ y ⊑ x ⟹ thesis" shows thesis
using assms by (auto simp: sympartp_def)
lemma sympartp_dual: "sympartp r⇧- = sympartp r"
by (auto intro!:ext simp: sympartp_def)
lemma sympartp_eq[simp]: "sympartp (=) = (=)" by auto
lemma sympartp_sympartp[simp]: "sympartp (sympartp r) = sympartp r" by (auto intro!:ext)
lemma reflclp_sympartp[simp]: "(sympartp r)⇧=⇧= = sympartp r⇧=⇧=" by auto
definition "equivpartp r x y ≡ x = y ∨ r x y ∧ r y x"
lemma sympartp_reflclp_equivp[simp]: "sympartp r⇧=⇧= = equivpartp r" by (auto intro!:ext simp: equivpartp_def)
lemma equivpartI[simp]: "equivpartp r x x"
and sympartp_equivpartpI: "sympartp r x y ⟹ equivpartp r x y"
and equivpartpCI[intro]: "(x ≠ y ⟹ sympartp r x y) ⟹ equivpartp r x y"
by (auto simp:equivpartp_def)
lemma equivpartpE[elim]:
assumes "equivpartp r x y"
and "x = y ⟹ thesis"
and "r x y ⟹ r y x ⟹ thesis"
shows "thesis"
using assms by (auto simp: equivpartp_def)
lemma equivpartp_eq[simp]: "equivpartp (=) = (=)" by auto
lemma sympartp_equivpartp[simp]: "sympartp (equivpartp r) = (equivpartp r)"
and equivpartp_equivpartp[simp]: "equivpartp (equivpartp r) = (equivpartp r)"
and equivpartp_sympartp[simp]: "equivpartp (sympartp r) = (equivpartp r)"
by (auto 0 5 intro!:ext)
lemma equivpartp_dual: "equivpartp r⇧- = equivpartp r"
by (auto intro!:ext simp: equivpartp_def)
text ‹The asymmetric part:›
definition "asympartp r x y ≡ r x y ∧ ¬ r y x"
lemma asympartpE[elim]:
fixes r (infix "⊑" 50)
shows "asympartp (⊑) x y ⟹ (x ⊑ y ⟹ ¬y ⊑ x ⟹ thesis) ⟹ thesis"
by (auto simp: asympartp_def)
lemmas asympartpI[intro] = asympartp_def[unfolded atomize_eq, THEN iffD2, unfolded conj_imp_eq_imp_imp, rule_format]
lemma asympartp_eq[simp]: "asympartp (=) = bot" by auto
lemma asympartp_sympartp [simp]: "asympartp (sympartp r) = bot"
and sympartp_asympartp [simp]: "sympartp (asympartp r) = bot"
by (auto intro!: ext)
lemma asympartp_dual: "asympartp r⇧- = (asympartp r)⇧-" by auto
text ‹Restriction to a set:›
definition Restrp (infixl "↾" 60) where "(r ↾ A) a b ≡ a ∈ A ∧ b ∈ A ∧ r a b"
lemmas RestrpI[intro!] = Restrp_def[unfolded atomize_eq, THEN iffD2, unfolded conj_imp_eq_imp_imp]
lemmas RestrpE[elim!] = Restrp_def[unfolded atomize_eq, THEN iffD1, elim_format, unfolded conj_imp_eq_imp_imp]
lemma Restrp_simp[simp]: "a ∈ A ⟹ b ∈ A ⟹ (r ↾ A) a b ⟷ r a b" by auto
lemma Restrp_UNIV[simp]: "r ↾ UNIV ≡ r" by (auto simp: atomize_eq)
lemma Restrp_Restrp[simp]: "r ↾ A ↾ B ≡ r ↾ A ∩ B" by (auto simp: atomize_eq Restrp_def)
lemma sympartp_Restrp[simp]: "sympartp (r ↾ A) ≡ sympartp r ↾ A"
by (auto simp: atomize_eq)
text ‹Relational images:›
definition Imagep (infixr "```" 59) where "r ``` A ≡ {b. ∃a ∈ A. r a b}"
lemma Imagep_Image: "r ``` A = {(a,b). r a b} `` A"
by (auto simp: Imagep_def)
lemma in_Imagep: "b ∈ r ``` A ⟷ (∃a ∈ A. r a b)" by (auto simp: Imagep_def)
lemma ImagepI: "a ∈ A ⟹ r a b ⟹ b ∈ r ``` A" by (auto simp: in_Imagep)
lemma subset_Imagep: "B ⊆ r ``` A ⟷ (∀b∈B. ∃a∈A. r a b)"
by (auto simp: Imagep_def)
text ‹Bounds of a set:›
definition "bound X (⊑) b ≡ ∀x ∈ X. x ⊑ b" for r (infix "⊑" 50)
lemma
fixes r (infix "⊑" 50)
shows boundI[intro!]: "(⋀x. x ∈ X ⟹ x ⊑ b) ⟹ bound X (⊑) b"
and boundE[elim]: "bound X (⊑) b ⟹ ((⋀x. x ∈ X ⟹ x ⊑ b) ⟹ thesis) ⟹ thesis"
and boundD: "bound X (⊑) b ⟹ a ∈ X ⟹ a ⊑ b"
by (auto simp: bound_def)
lemma bound_empty: "bound {} = (λr x. True)" by auto
lemma bound_cmono: assumes "X ⊆ Y" shows "bound Y ≤ bound X"
using assms by auto
lemmas bound_subset = bound_cmono[THEN le_funD, THEN le_funD, THEN le_boolD, folded atomize_imp]
lemma bound_un: "bound (A ∪ B) = bound A ⊓ bound B"
by auto
lemma bound_insert[simp]:
fixes r (infix "⊑" 50)
shows "bound (insert x X) (⊑) b ⟷ x ⊑ b ∧ bound X (⊑) b" by auto
lemma bound_cong:
assumes "A = A'"
and "b = b'"
and "⋀a. a ∈ A' ⟹ le a b' = le' a b'"
shows "bound A le b = bound A' le' b'"
by (auto simp: assms)
lemma bound_subsel: "le ≤ le' ⟹ bound A le ≤ bound A le'"
by (auto simp add: bound_def)
text ‹Extreme (greatest) elements in a set:›
definition "extreme X (⊑) e ≡ e ∈ X ∧ (∀x ∈ X. x ⊑ e)" for r (infix "⊑" 50)
lemma
fixes r (infix "⊑" 50)
shows extremeI[intro]: "e ∈ X ⟹ (⋀x. x ∈ X ⟹ x ⊑ e) ⟹ extreme X (⊑) e"
and extremeD: "extreme X (⊑) e ⟹ e ∈ X" "extreme X (⊑) e ⟹ (⋀x. x ∈ X ⟹ x ⊑ e)"
and extremeE[elim]: "extreme X (⊑) e ⟹ (e ∈ X ⟹ (⋀x. x ∈ X ⟹ x ⊑ e) ⟹ thesis) ⟹ thesis"
by (auto simp: extreme_def)
lemma
fixes r (infix "⊑" 50)
shows extreme_UNIV[simp]: "extreme UNIV (⊑) t ⟷ (∀x. x ⊑ t)" by auto
lemma extreme_iff_bound: "extreme X r e ⟷ bound X r e ∧ e ∈ X" by auto
lemma extreme_imp_bound: "extreme X r x ⟹ bound X r x" by auto
lemma extreme_inf: "extreme X (r ⊓ s) x ⟷ extreme X r x ∧ extreme X s x" by auto
lemma extremes_equiv: "extreme X r b ⟹ extreme X r c ⟹ sympartp r b c" by blast
lemma extreme_cong:
assumes "A = A'"
and "b = b'"
and "⋀a. a ∈ A' ⟹ b' ∈ A' ⟹ le a b' = le' a b'"
shows "extreme A le b = extreme A' le' b'"
by (auto simp: assms extreme_def)
lemma extreme_subset: "X ⊆ Y ⟹ extreme X r x ⟹ extreme Y r y ⟹ r x y" by blast
lemma extreme_subrel:
"le ≤ le' ⟹ extreme A le ≤ extreme A le'" by (auto simp: extreme_def)
text ‹Now suprema and infima are given uniformly as follows.
The definition is restricted to a given set.
›
definition
"extreme_bound A (⊑) X ≡ extreme {b ∈ A. bound X (⊑) b} (⊑)⇧-" for r (infix "⊑" 50)
lemmas extreme_boundI_extreme = extreme_bound_def[unfolded atomize_eq, THEN fun_cong, THEN iffD2]
lemmas extreme_boundD_extreme = extreme_bound_def[unfolded atomize_eq, THEN fun_cong, THEN iffD1]
context
fixes A :: "'a set" and less_eq :: "'a ⇒ 'a ⇒ bool" (infix "⊑" 50)
begin
lemma extreme_boundI[intro]:
assumes "⋀b. bound X (⊑) b ⟹ b ∈ A ⟹ s ⊑ b" and "⋀x. x ∈ X ⟹ x ⊑ s" and "s ∈ A"
shows "extreme_bound A (⊑) X s"
using assms by (auto simp: extreme_bound_def)
lemma extreme_boundD:
assumes "extreme_bound A (⊑) X s"
shows "x ∈ X ⟹ x ⊑ s"
and "bound X (⊑) b ⟹ b ∈ A ⟹ s ⊑ b"
and extreme_bound_in: "s ∈ A"
using assms by (auto simp: extreme_bound_def)
lemma extreme_boundE[elim]:
assumes "extreme_bound A (⊑) X s"
and "s ∈ A ⟹ bound X (⊑) s ⟹ (⋀b. bound X (⊑) b ⟹ b ∈ A ⟹ s ⊑ b) ⟹ thesis"
shows thesis
using assms by (auto simp: extreme_bound_def)
lemma extreme_bound_imp_bound: "extreme_bound A (⊑) X s ⟹ bound X (⊑) s" by auto
lemma extreme_imp_extreme_bound:
assumes Xs: "extreme X (⊑) s" and XA: "X ⊆ A" shows "extreme_bound A (⊑) X s"
using assms by force
lemma extreme_bound_subset_bound:
assumes XY: "X ⊆ Y"
and sX: "extreme_bound A (⊑) X s"
and b: "bound Y (⊑) b" and bA: "b ∈ A"
shows "s ⊑ b"
using bound_subset[OF XY b] sX bA by auto
lemma extreme_bound_subset:
assumes XY: "X ⊆ Y"
and sX: "extreme_bound A (⊑) X sX"
and sY: "extreme_bound A (⊑) Y sY"
shows "sX ⊑ sY"
using extreme_bound_subset_bound[OF XY sX] sY by auto
lemma extreme_bound_iff:
"extreme_bound A (⊑) X s ⟷ s ∈ A ∧ (∀c ∈ A. (∀x ∈ X. x ⊑ c) ⟶ s ⊑ c) ∧ (∀x ∈ X. x ⊑ s)"
by (auto simp: extreme_bound_def extreme_def)
lemma extreme_bound_empty: "extreme_bound A (⊑) {} x ⟷ extreme A (⊑)⇧- x"
by auto
lemma extreme_bound_singleton_refl[simp]:
"extreme_bound A (⊑) {x} x ⟷ x ∈ A ∧ x ⊑ x" by auto
lemma extreme_bound_image_const:
"x ⊑ x ⟹ I ≠ {} ⟹ (⋀i. i ∈ I ⟹ f i = x) ⟹ x ∈ A ⟹ extreme_bound A (⊑) (f ` I) x"
by (auto simp: image_constant)
lemma extreme_bound_UN_const:
"x ⊑ x ⟹ I ≠ {} ⟹ (⋀i y. i ∈ I ⟹ P i y ⟷ x = y) ⟹ x ∈ A ⟹
extreme_bound A (⊑) (⋃i∈I. {y. P i y}) x"
by auto
lemma extreme_bounds_equiv:
assumes s: "extreme_bound A (⊑) X s" and s': "extreme_bound A (⊑) X s'"
shows "sympartp (⊑) s s'"
using s s'
apply (unfold extreme_bound_def)
apply (subst sympartp_dual)
by (rule extremes_equiv)
lemma extreme_bound_sqweeze:
assumes XY: "X ⊆ Y" and YZ: "Y ⊆ Z"
and Xs: "extreme_bound A (⊑) X s" and Zs: "extreme_bound A (⊑) Z s"
shows "extreme_bound A (⊑) Y s"
proof
from Xs show "s ∈ A" by auto
fix b assume Yb: "bound Y (⊑) b" and bA: "b ∈ A"
from bound_subset[OF XY Yb] have "bound X (⊑) b".
with Xs bA
show "s ⊑ b" by auto
next
fix y assume yY: "y ∈ Y"
with YZ have "y ∈ Z" by auto
with Zs show "y ⊑ s" by auto
qed
lemma bound_closed_imp_extreme_bound_eq_extreme:
assumes closed: "∀b ∈ A. bound X (⊑) b ⟶ b ∈ X" and XA: "X ⊆ A"
shows "extreme_bound A (⊑) X = extreme X (⊑)"
proof (intro ext iffI extreme_boundI extremeI)
fix e
assume "extreme_bound A (⊑) X e"
then have Xe: "bound X (⊑) e" and "e ∈ A" by auto
with closed show "e ∈ X" by auto
fix x assume "x ∈ X"
with Xe show "x ⊑ e" by auto
next
fix e
assume Xe: "extreme X (⊑) e"
then have eX: "e ∈ X" by auto
with XA show "e ∈ A" by auto
{ fix b assume Xb: "bound X (⊑) b" and "b ∈ A"
from eX Xb show "e ⊑ b" by auto
}
fix x assume xX: "x ∈ X" with Xe show "x ⊑ e" by auto
qed
end
lemma extreme_bound_cong:
assumes "A = A'"
and "X = X'"
and "⋀a b. a ∈ A' ⟹ b ∈ A' ⟹ le a b ⟷ le' a b"
and "⋀a b. a ∈ X' ⟹ b ∈ A' ⟹ le a b ⟷ le' a b"
shows "extreme_bound A le X s = extreme_bound A le' X s"
apply (unfold extreme_bound_def)
apply (rule extreme_cong)
by (auto simp: assms)
text ‹Maximal or Minimal›
definition "extremal X (⊑) x ≡ x ∈ X ∧ (∀y ∈ X. x ⊑ y ⟶ y ⊑ x)" for r (infix "⊑" 50)
context
fixes r :: "'a ⇒ 'a ⇒ bool" (infix "⊑" 50)
begin
lemma extremalI:
assumes "x ∈ X" "⋀y. y ∈ X ⟹ x ⊑ y ⟹ y ⊑ x"
shows "extremal X (⊑) x"
using assms by (auto simp: extremal_def)
lemma extremalE:
assumes "extremal X (⊑) x"
and "x ∈ X ⟹ (⋀y. y ∈ X ⟹ x ⊑ y ⟹ y ⊑ x) ⟹ thesis"
shows thesis
using assms by (auto simp: extremal_def)
lemma extremalD:
assumes "extremal X (⊑) x" shows "x ∈ X" "y ∈ X ⟹ x ⊑ y ⟹ y ⊑ x"
using assms by (auto elim!: extremalE)
end
context
fixes ir (infix "≼" 50) and r (infix "⊑" 50) and I f
assumes mono: "monotone_on I (≼) (⊑) f"
begin
lemma monotone_image_bound:
assumes "X ⊆ I" and "b ∈ I" and "bound X (≼) b"
shows "bound (f ` X) (⊑) (f b)"
using assms monotone_onD[OF mono]
by (auto simp: bound_def)
lemma monotone_image_extreme:
assumes e: "extreme I (≼) e"
shows "extreme (f ` I) (⊑) (f e)"
using e[unfolded extreme_iff_bound] monotone_image_bound[of I e] by auto
end
context
fixes ir :: "'i ⇒ 'i ⇒ bool" (infix "≼" 50)
and r :: "'a ⇒ 'a ⇒ bool" (infix "⊑" 50)
and f and A and e and I
assumes fIA: "f ` I ⊆ A"
and mono: "monotone_on I (≼) (⊑) f"
and e: "extreme I (≼) e"
begin
lemma monotone_extreme_imp_extreme_bound:
"extreme_bound A (⊑) (f ` I) (f e)"
using monotone_onD[OF mono] e fIA
by (intro extreme_boundI, auto simp: image_def elim!: extremeE)
lemma monotone_extreme_extreme_boundI:
"x = f e ⟹ extreme_bound A (⊑) (f ` I) x"
using monotone_extreme_imp_extreme_bound by auto
end
subsection ‹Locales for Binary Relations›
text ‹We now define basic properties of binary relations,
in form of \emph{locales}~\cite{Kammuller00,locale}.›
subsubsection ‹Syntactic Locales›
text ‹The following locales do not assume anything, but provide infix notations for
relations.›
locale less_eq_syntax =
fixes less_eq :: "'a ⇒ 'a ⇒ bool" (infix "⊑" 50)
locale less_syntax =
fixes less :: "'a ⇒ 'a ⇒ bool" (infix "⊏" 50)
locale equivalence_syntax =
fixes equiv :: "'a ⇒ 'a ⇒ bool" (infix "∼" 50)
begin
abbreviation equiv_class ("[_]⇩∼") where "[x]⇩∼ ≡ { y. x ∼ y }"
end
text ‹Next ones introduce abbreviations for dual etc.
To avoid needless constants, one should be careful when declaring them as sublocales.›
locale less_eq_dualize = less_eq_syntax
begin
abbreviation (input) greater_eq (infix "⊒" 50) where "x ⊒ y ≡ y ⊑ x"
end
locale less_eq_symmetrize = less_eq_dualize
begin
abbreviation sym (infix "∼" 50) where "(∼) ≡ sympartp (⊑)"
abbreviation equiv (infix "(≃)" 50) where "(≃) ≡ equivpartp (⊑)"
end
locale less_eq_asymmetrize = less_eq_symmetrize
begin
abbreviation less (infix "⊏" 50) where "(⊏) ≡ asympartp (⊑)"
abbreviation greater (infix "⊐" 50) where "(⊐) ≡ (⊏)⇧-"
lemma asym_cases[consumes 1, case_names asym sym]:
assumes "x ⊑ y" and "x ⊏ y ⟹ thesis" and "x ∼ y ⟹ thesis"
shows thesis
using assms by auto
end
locale less_dualize = less_syntax
begin
abbreviation (input) greater (infix "⊐" 50) where "x ⊐ y ≡ y ⊏ x"
end
locale related_set =
fixes A :: "'a set" and less_eq :: "'a ⇒ 'a ⇒ bool" (infix "⊑" 50)
subsubsection ‹Basic Properties of Relations›
text ‹In the following we define basic properties in form of locales.›
text ‹Reflexivity restricted on a set:›
locale reflexive = related_set +
assumes refl[intro]: "x ∈ A ⟹ x ⊑ x"
begin
lemma eq_implies: "x = y ⟹ x ∈ A ⟹ x ⊑ y" by auto
lemma reflexive_subset: "B ⊆ A ⟹ reflexive B (⊑)" apply unfold_locales by auto
lemma extreme_singleton[simp]: "x ∈ A ⟹ extreme {x} (⊑) y ⟷ x = y" by auto
lemma extreme_bound_singleton: "x ∈ A ⟹ extreme_bound A (⊑) {x} x" by auto
lemma extreme_bound_cone: "x ∈ A ⟹ extreme_bound A (⊑) {a ∈ A. a ⊑ x} x" by auto
end
lemmas reflexiveI[intro!] = reflexive.intro
lemma reflexiveE[elim]:
assumes "reflexive A r" and "(⋀x. x ∈ A ⟹ r x x) ⟹ thesis" shows thesis
using assms by (auto simp: reflexive.refl)
lemma reflexive_cong:
"(⋀a b. a ∈ A ⟹ b ∈ A ⟹ r a b ⟷ r' a b) ⟹ reflexive A r ⟷ reflexive A r'"
by (simp add: reflexive_def)
locale irreflexive = related_set A "(⊏)" for A and less (infix "⊏" 50) +
assumes irrefl: "x ∈ A ⟹ ¬ x ⊏ x"
begin
lemma irreflD[simp]: "x ⊏ x ⟹ ¬x ∈ A" by (auto simp: irrefl)
lemma implies_not_eq: "x ⊏ y ⟹ x ∈ A ⟹ x ≠ y" by auto
lemma Restrp_irreflexive: "irreflexive UNIV ((⊏)↾A)"
apply unfold_locales by auto
lemma irreflexive_subset: "B ⊆ A ⟹ irreflexive B (⊏)" apply unfold_locales by auto
end
lemmas irreflexiveI[intro!] = irreflexive.intro
lemma irreflexive_cong:
"(⋀a b. a ∈ A ⟹ b ∈ A ⟹ r a b ⟷ r' a b) ⟹ irreflexive A r ⟷ irreflexive A r'"
by (simp add: irreflexive_def)
context reflexive begin
interpretation less_eq_asymmetrize.
lemma asympartp_irreflexive: "irreflexive A (⊏)" by auto
end
locale transitive = related_set +
assumes trans[trans]: "x ⊑ y ⟹ y ⊑ z ⟹ x ∈ A ⟹ y ∈ A ⟹ z ∈ A ⟹ x ⊑ z"
begin
lemma Restrp_transitive: "transitive UNIV ((⊑)↾A)"
apply unfold_locales
by (auto intro: trans)
lemma bound_trans[trans]: "bound X (⊑) b ⟹ b ⊑ c ⟹ X ⊆ A ⟹ b ∈ A ⟹ c ∈ A ⟹ bound X (⊑) c"
by (auto 0 4 dest: trans)
lemma extreme_bound_mono:
assumes XY: "∀x∈X. ∃y∈Y. x ⊑ y" and XA: "X ⊆ A" and YA: "Y ⊆ A"
and sX: "extreme_bound A (⊑) X sX"
and sY: "extreme_bound A (⊑) Y sY"
shows "sX ⊑ sY"
proof (intro extreme_boundD(2)[OF sX] CollectI conjI boundI)
from sY show sYA: "sY ∈ A" by auto
from sY have "bound Y (⊑) sY" by auto
fix x assume xX: "x ∈ X" with XY obtain y where yY: "y ∈ Y" and xy: "x ⊑ y" by auto
from yY sY have "y ⊑ sY" by auto
from trans[OF xy this] xX XA yY YA sYA show "x ⊑ sY" by auto
qed
lemma transitive_subset:
assumes BA: "B ⊆ A" shows "transitive B (⊑)"
apply unfold_locales
using trans BA by blast
lemma asympartp_transitive: "transitive A (asympartp (⊑))"
apply unfold_locales by (auto dest:trans)
lemma reflclp_transitive: "transitive A (⊑)⇧=⇧="
apply unfold_locales by (auto dest: trans)
text ‹The symmetric part is also transitive, but this is done in the later semiattractive locale›
end
lemmas transitiveI = transitive.intro
lemma transitive_ball[code]:
"transitive A (⊑) ⟷ (∀x ∈ A. ∀y ∈ A. ∀z ∈ A. x ⊑ y ⟶ y ⊑ z ⟶ x ⊑ z)"
for less_eq (infix "⊑" 50)
by (auto simp: transitive_def)
lemma transitive_cong:
assumes r: "⋀a b. a ∈ A ⟹ b ∈ A ⟹ r a b ⟷ r' a b" shows "transitive A r ⟷ transitive A r'"
proof (intro iffI)
show "transitive A r ⟹ transitive A r'"
apply (intro transitive.intro)
apply (unfold r[symmetric])
using transitive.trans.
show "transitive A r' ⟹ transitive A r"
apply (intro transitive.intro)
apply (unfold r)
using transitive.trans.
qed
lemma transitive_empty[intro!]: "transitive {} r" by (auto intro!: transitive.intro)
lemma tranclp_transitive: "transitive A (tranclp r)"
using tranclp_trans by unfold_locales
locale symmetric = related_set A "(∼)" for A and equiv (infix "∼" 50) +
assumes sym[sym]: "x ∼ y ⟹ x ∈ A ⟹ y ∈ A ⟹ y ∼ x"
begin
lemma sym_iff: "x ∈ A ⟹ y ∈ A ⟹ x ∼ y ⟷ y ∼ x"
by (auto dest: sym)
lemma Restrp_symmetric: "symmetric UNIV ((∼)↾A)"
apply unfold_locales by (auto simp: sym_iff)
lemma symmetric_subset: "B ⊆ A ⟹ symmetric B (∼)"
apply unfold_locales by (auto dest: sym)
end
lemmas symmetricI[intro] = symmetric.intro
lemma symmetric_cong:
"(⋀a b. a ∈ A ⟹ b ∈ A ⟹ r a b ⟷ r' a b) ⟹ symmetric A r ⟷ symmetric A r'"
by (auto simp: symmetric_def)
lemma symmetric_empty[intro!]: "symmetric {} r" by auto
global_interpretation sympartp: symmetric UNIV "sympartp r"
rewrites "⋀r. r ↾ UNIV ≡ r"
and "⋀x. x ∈ UNIV ≡ True"
and "⋀P1. (True ⟹ P1) ≡ Trueprop P1"
and "⋀P1 P2. (True ⟹ PROP P1 ⟹ PROP P2) ≡ (PROP P1 ⟹ PROP P2)"
by auto
lemma sympartp_symmetric: "symmetric A (sympartp r)" by auto
locale antisymmetric = related_set +
assumes antisym: "x ⊑ y ⟹ y ⊑ x ⟹ x ∈ A ⟹ y ∈ A ⟹ x = y"
begin
interpretation less_eq_symmetrize.
lemma sym_iff_eq_refl: "x ∈ A ⟹ y ∈ A ⟹ x ∼ y ⟷ x = y ∧ y ⊑ y" by (auto dest: antisym)
lemma equiv_iff_eq[simp]: "x ∈ A ⟹ y ∈ A ⟹ x ≃ y ⟷ x = y" by (auto dest: antisym elim: equivpartpE)
lemma extreme_unique: "X ⊆ A ⟹ extreme X (⊑) x ⟹ extreme X (⊑) y ⟷ x = y"
by (elim extremeE, auto dest!: antisym[OF _ _ subsetD])
lemma ex_extreme_iff_ex1:
"X ⊆ A ⟹ Ex (extreme X (⊑)) ⟷ Ex1 (extreme X (⊑))" by (auto simp: extreme_unique)
lemma ex_extreme_iff_the:
"X ⊆ A ⟹ Ex (extreme X (⊑)) ⟷ extreme X (⊑) (The (extreme X (⊑)))"
apply (rule iffI)
apply (rule theI')
using extreme_unique by auto
lemma eq_The_extreme: "X ⊆ A ⟹ extreme X (⊑) x ⟹ x = The (extreme X (⊑))"
by (rule the1_equality[symmetric], auto simp: ex_extreme_iff_ex1[symmetric])
lemma Restrp_antisymmetric: "antisymmetric UNIV ((⊑)↾A)"
apply unfold_locales
by (auto dest: antisym)
lemma antisymmetric_subset: "B ⊆ A ⟹ antisymmetric B (⊑)"
apply unfold_locales using antisym by auto
end
lemmas antisymmetricI[intro] = antisymmetric.intro
lemma antisymmetric_cong:
"(⋀a b. a ∈ A ⟹ b ∈ A ⟹ r a b ⟷ r' a b) ⟹ antisymmetric A r ⟷ antisymmetric A r'"
by (auto simp: antisymmetric_def)
lemma antisymmetric_empty[intro!]: "antisymmetric {} r" by auto
lemma antisymmetric_union:
fixes less_eq (infix "⊑" 50)
assumes A: "antisymmetric A (⊑)" and B: "antisymmetric B (⊑)"
and AB: "∀a ∈ A. ∀b ∈ B. a ⊑ b ⟶ b ⊑ a ⟶ a = b"
shows "antisymmetric (A ∪ B) (⊑)"
proof-
interpret A: antisymmetric A "(⊑)" using A.
interpret B: antisymmetric B "(⊑)" using B.
show ?thesis by (auto dest: AB[rule_format] A.antisym B.antisym)
qed
text ‹The following notion is new, generalizing antisymmetry and transitivity.›
locale semiattractive = related_set +
assumes attract: "x ⊑ y ⟹ y ⊑ x ⟹ y ⊑ z ⟹ x ∈ A ⟹ y ∈ A ⟹ z ∈ A ⟹ x ⊑ z"
begin
interpretation less_eq_symmetrize.
lemma equiv_order_trans[trans]:
assumes xy: "x ≃ y" and yz: "y ⊑ z" and x: "x ∈ A" and y: "y ∈ A" and z: "z ∈ A"
shows "x ⊑ z"
using attract[OF _ _ _ x y z] xy yz by (auto elim: equivpartpE)
lemma equiv_transitive: "transitive A (≃)"
proof unfold_locales
fix x y z
assume x: "x ∈ A" and y: "y ∈ A" and z: "z ∈ A" and xy: "x ≃ y" and yz: "y ≃ z"
show "x ≃ z"
using equiv_order_trans[OF xy _ x y z] attract[OF _ _ _ z y x] xy yz by (auto simp:equivpartp_def)
qed
lemma sym_order_trans[trans]:
assumes xy: "x ∼ y" and yz: "y ⊑ z" and x: "x ∈ A" and y: "y ∈ A" and z: "z ∈ A"
shows "x ⊑ z"
using attract[OF _ _ _ x y z] xy yz by auto
interpretation sym: transitive A "(∼)"
proof unfold_locales
fix x y z
assume x: "x ∈ A" and y: "y ∈ A" and z: "z ∈ A" and xy: "x ∼ y" and yz: "y ∼ z"
show "x ∼ z"
using sym_order_trans[OF xy _ x y z] attract[OF _ _ _ z y x] xy yz by auto
qed
lemmas sym_transitive = sym.transitive_axioms
lemma extreme_bound_quasi_const:
assumes C: "C ⊆ A" and x: "x ∈ A" and C0: "C ≠ {}" and const: "∀y ∈ C. y ∼ x"
shows "extreme_bound A (⊑) C x"
proof (intro extreme_boundI x)
from C0 obtain c where cC: "c ∈ C" by auto
with C have c: "c ∈ A" by auto
from cC const have cx: "c ∼ x" by auto
fix b assume b: "b ∈ A" and "bound C (⊑) b"
with cC have cb: "c ⊑ b" by auto
from attract[OF _ _ cb x c b] cx show "x ⊑ b" by auto
next
fix c assume "c ∈ C"
with const show "c ⊑ x" by auto
qed
lemma extreme_bound_quasi_const_iff:
assumes C: "C ⊆ A" and x: "x ∈ A" and y: "y ∈ A" and C0: "C ≠ {}" and const: "∀z ∈ C. z ∼ x"
shows "extreme_bound A (⊑) C y ⟷ x ∼ y"
proof (intro iffI)
assume y: "extreme_bound A (⊑) C y"
note x = extreme_bound_quasi_const[OF C x C0 const]
from extreme_bounds_equiv[OF y x]
show "x ∼ y" by auto
next
assume xy: "x ∼ y"
with const C sym.trans[OF _ xy _ x y] have Cy: "∀z ∈ C. z ∼ y" by auto
show "extreme_bound A (⊑) C y"
using extreme_bound_quasi_const[OF C y C0 Cy].
qed
lemma Restrp_semiattractive: "semiattractive UNIV ((⊑)↾A)"
apply unfold_locales
by (auto dest: attract)
lemma semiattractive_subset: "B ⊆ A ⟹ semiattractive B (⊑)"
apply unfold_locales using attract by blast
end
lemmas semiattractiveI = semiattractive.intro
lemma semiattractive_cong:
assumes r: "⋀a b. a ∈ A ⟹ b ∈ A ⟹ r a b ⟷ r' a b"
shows "semiattractive A r ⟷ semiattractive A r'" (is "?l ⟷ ?r")
proof
show "?l ⟹ ?r"
apply (intro semiattractive.intro)
apply (unfold r[symmetric])
using semiattractive.attract.
show "?r ⟹ ?l"
apply (intro semiattractive.intro)
apply (unfold r)
using semiattractive.attract.
qed
lemma semiattractive_empty[intro!]: "semiattractive {} r"
by (auto intro!: semiattractiveI)
locale attractive = semiattractive +
assumes "semiattractive A (⊑)⇧-"
begin
interpretation less_eq_symmetrize.
sublocale dual: semiattractive A "(⊑)⇧-"
rewrites "⋀r. sympartp (r ↾ A) ≡ sympartp r ↾ A"
and "⋀r. sympartp (sympartp r) ≡ sympartp r"
and "sympartp ((⊑) ↾ A)⇧- ≡ (∼) ↾ A"
and "sympartp (⊑)⇧- ≡ (∼)"
and "equivpartp (⊑)⇧- ≡ (≃)"
using attractive_axioms[unfolded attractive_def]
by (auto intro!: ext simp: attractive_axioms_def atomize_eq equivpartp_def)
lemma order_equiv_trans[trans]:
assumes xy: "x ⊑ y" and yz: "y ≃ z" and x: "x ∈ A" and y: "y ∈ A" and z: "z ∈ A"
shows "x ⊑ z"
using dual.attract[OF _ _ _ z y x] xy yz by auto
lemma order_sym_trans[trans]:
assumes xy: "x ⊑ y" and yz: "y ∼ z" and x: "x ∈ A" and y: "y ∈ A" and z: "z ∈ A"
shows "x ⊑ z"
using dual.attract[OF _ _ _ z y x] xy yz by auto
lemma extreme_bound_sym_trans:
assumes XA: "X ⊆ A" and Xx: "extreme_bound A (⊑) X x"
and xy: "x ∼ y" and yA: "y ∈ A"
shows "extreme_bound A (⊑) X y"
proof (intro extreme_boundI yA)
from Xx have xA: "x ∈ A" by auto
{
fix b assume Xb: "bound X (⊑) b" and bA: "b ∈ A"
with Xx have xb: "x ⊑ b" by auto
from sym_order_trans[OF _ xb yA xA bA] xy show "y ⊑ b" by auto
}
fix a assume aX: "a ∈ X"
with Xx have ax: "a ⊑ x" by auto
from aX XA have aA: "a ∈ A" by auto
from order_sym_trans[OF ax xy aA xA yA] show "a ⊑ y" by auto
qed
interpretation Restrp: semiattractive UNIV "(⊑)↾A" using Restrp_semiattractive.
interpretation dual.Restrp: semiattractive UNIV "(⊑)⇧-↾A" using dual.Restrp_semiattractive.
lemma Restrp_attractive: "attractive UNIV ((⊑)↾A)"
apply unfold_locales
using dual.Restrp.attract by auto
lemma attractive_subset: "B ⊆ A ⟹ attractive B (⊑)"
apply (intro attractive.intro attractive_axioms.intro)
using semiattractive_subset dual.semiattractive_subset by auto
end
lemmas attractiveI = attractive.intro[OF _ attractive_axioms.intro]
lemma attractive_cong:
assumes r: "⋀a b. a ∈ A ⟹ b ∈ A ⟹ r a b ⟷ r' a b"
shows "attractive A r ⟷ attractive A r'"
by (simp add: attractive_def attractive_axioms_def r cong: semiattractive_cong)
lemma attractive_empty[intro!]: "attractive {} r"
by (auto intro!: attractiveI)
context antisymmetric begin
sublocale attractive
apply unfold_locales by (auto dest: antisym)
end
context transitive begin
sublocale attractive
rewrites "⋀r. sympartp (r ↾ A) ≡ sympartp r ↾ A"
and "⋀r. sympartp (sympartp r) ≡ sympartp r"
and "sympartp (⊑)⇧- ≡ sympartp (⊑)"
and "(sympartp (⊑))⇧- ≡ sympartp (⊑)"
and "(sympartp (⊑) ↾ A)⇧- ≡ sympartp (⊑) ↾ A"
and "asympartp (asympartp (⊑)) = asympartp (⊑)"
and "asympartp (sympartp (⊑)) = bot"
and "asympartp (⊑) ↾ A = asympartp ((⊑) ↾ A)"
apply unfold_locales
by (auto intro!:ext dest: trans simp: atomize_eq)
end
subsection ‹Combined Properties›
text ‹Some combinations of the above basic properties are given names.›
locale asymmetric = related_set A "(⊏)" for A and less (infix "⊏" 50) +
assumes asym: "x ⊏ y ⟹ y ⊏ x ⟹ x ∈ A ⟹ y ∈ A ⟹ False"
begin
sublocale irreflexive
apply unfold_locales by (auto dest: asym)
lemma antisymmetric_axioms: "antisymmetric A (⊏)"
apply unfold_locales by (auto dest: asym)
lemma Restrp_asymmetric: "asymmetric UNIV ((⊏)↾A)"
apply unfold_locales
by (auto dest:asym)
lemma asymmetric_subset: "B ⊆ A ⟹ asymmetric B (⊏)"
apply unfold_locales using asym by auto
end
lemmas asymmetricI = asymmetric.intro
lemma asymmetric_iff_irreflexive_antisymmetric:
fixes less (infix "⊏" 50)
shows "asymmetric A (⊏) ⟷ irreflexive A (⊏) ∧ antisymmetric A (⊏)" (is "?l ⟷ ?r")
proof
assume ?l
then interpret asymmetric.
show ?r by (auto dest: asym)
next
assume ?r
then interpret irreflexive + antisymmetric A "(⊏)" by auto
show ?l by (auto intro!:asymmetricI dest: antisym irrefl)
qed
lemma asymmetric_cong:
assumes r: "⋀a b. a ∈ A ⟹ b ∈ A ⟹ r a b ⟷ r' a b"
shows "asymmetric A r ⟷ asymmetric A r'"
by (simp add: asymmetric_iff_irreflexive_antisymmetric r cong: irreflexive_cong antisymmetric_cong)
lemma asymmetric_empty: "asymmetric {} r"
by (auto simp: asymmetric_iff_irreflexive_antisymmetric)
locale quasi_ordered_set = reflexive + transitive
begin
lemma quasi_ordered_subset: "B ⊆ A ⟹ quasi_ordered_set B (⊑)"
apply intro_locales
using reflexive_subset transitive_subset by auto
end
lemmas quasi_ordered_setI = quasi_ordered_set.intro
lemma quasi_ordered_set_cong:
assumes r: "⋀a b. a ∈ A ⟹ b ∈ A ⟹ r a b ⟷ r' a b"
shows "quasi_ordered_set A r ⟷ quasi_ordered_set A r'"
by (simp add: quasi_ordered_set_def r cong: reflexive_cong transitive_cong)
lemma quasi_ordered_set_empty[intro!]: "quasi_ordered_set {} r"
by (auto intro!: quasi_ordered_set.intro)
lemma rtranclp_quasi_ordered: "quasi_ordered_set A (rtranclp r)"
by (unfold_locales, auto)
locale near_ordered_set = antisymmetric + transitive
begin
interpretation Restrp: antisymmetric UNIV "(⊑)↾A" using Restrp_antisymmetric.
interpretation Restrp: transitive UNIV "(⊑)↾A" using Restrp_transitive.
lemma Restrp_near_order: "near_ordered_set UNIV ((⊑)↾A)"..
lemma near_ordered_subset: "B ⊆ A ⟹ near_ordered_set B (⊑)"
apply intro_locales
using antisymmetric_subset transitive_subset by auto
end
lemmas near_ordered_setI = near_ordered_set.intro
lemma near_ordered_set_cong:
assumes r: "⋀a b. a ∈ A ⟹ b ∈ A ⟹ r a b ⟷ r' a b"
shows "near_ordered_set A r ⟷ near_ordered_set A r'"
by (simp add: near_ordered_set_def r cong: antisymmetric_cong transitive_cong)
lemma near_ordered_set_empty[intro!]: "near_ordered_set {} r"
by (auto intro!: near_ordered_set.intro)
locale pseudo_ordered_set = reflexive + antisymmetric
begin
interpretation less_eq_symmetrize.
lemma sym_eq[simp]: "x ∈ A ⟹ y ∈ A ⟹ x ∼ y ⟷ x = y"
by (auto simp: refl dest: antisym)
lemma extreme_bound_singleton_eq[simp]: "x ∈ A ⟹ extreme_bound A (⊑) {x} y ⟷ x = y"
by (auto intro!: antisym)
lemma eq_iff: "x ∈ A ⟹ y ∈ A ⟹ x = y ⟷ x ⊑ y ∧ y ⊑ x" by (auto dest: antisym simp:refl)
lemma extreme_order_iff_eq: "e ∈ A ⟹ extreme {x ∈ A. x ⊑ e} (⊑) s ⟷ e = s"
by (auto intro!: antisym)
lemma pseudo_ordered_subset: "B ⊆ A ⟹ pseudo_ordered_set B (⊑)"
apply intro_locales
using reflexive_subset antisymmetric_subset by auto
end
lemmas pseudo_ordered_setI = pseudo_ordered_set.intro
lemma pseudo_ordered_set_cong:
assumes r: "⋀a b. a ∈ A ⟹ b ∈ A ⟹ r a b ⟷ r' a b"
shows "pseudo_ordered_set A r ⟷ pseudo_ordered_set A r'"
by (simp add: pseudo_ordered_set_def r cong: reflexive_cong antisymmetric_cong)
lemma pseudo_ordered_set_empty[intro!]: "pseudo_ordered_set {} r"
by (auto intro!: pseudo_ordered_setI)
locale partially_ordered_set = reflexive + antisymmetric + transitive
begin
sublocale pseudo_ordered_set + quasi_ordered_set + near_ordered_set ..
lemma partially_ordered_subset: "B ⊆ A ⟹ partially_ordered_set B (⊑)"
apply intro_locales
using reflexive_subset transitive_subset antisymmetric_subset by auto
end
lemmas partially_ordered_setI = partially_ordered_set.intro
lemma partially_ordered_set_cong:
assumes r: "⋀a b. a ∈ A ⟹ b ∈ A ⟹ r a b ⟷ r' a b"
shows "partially_ordered_set A r ⟷ partially_ordered_set A r'"
by (simp add: partially_ordered_set_def r cong: reflexive_cong antisymmetric_cong transitive_cong)
lemma partially_ordered_set_empty[intro!]: "partially_ordered_set {} r"
by (auto intro!: partially_ordered_setI)
locale strict_ordered_set = irreflexive + transitive A "(⊏)"
begin
sublocale asymmetric
proof
fix x y
assume x: "x ∈ A" and y: "y ∈ A"
assume xy: "x ⊏ y"
also assume yx: "y ⊏ x"
finally have "x ⊏ x" using x y by auto
with x show False by auto
qed
lemma near_ordered_set_axioms: "near_ordered_set A (⊏)"
using antisymmetric_axioms by intro_locales
interpretation Restrp: asymmetric UNIV "(⊏)↾A" using Restrp_asymmetric.
interpretation Restrp: transitive UNIV "(⊏)↾A" using Restrp_transitive.
lemma Restrp_strict_order: "strict_ordered_set UNIV ((⊏)↾A)"..
lemma strict_ordered_subset: "B ⊆ A ⟹ strict_ordered_set B (⊏)"
apply intro_locales
using irreflexive_subset transitive_subset by auto
end
lemmas strict_ordered_setI = strict_ordered_set.intro
lemma strict_ordered_set_cong:
assumes r: "⋀a b. a ∈ A ⟹ b ∈ A ⟹ r a b ⟷ r' a b"
shows "strict_ordered_set A r ⟷ strict_ordered_set A r'"
by (simp add: strict_ordered_set_def r cong: irreflexive_cong transitive_cong)
lemma strict_ordered_set_empty[intro!]: "strict_ordered_set {} r"
by (auto intro!: strict_ordered_set.intro)
locale tolerance = symmetric + reflexive A "(∼)"
begin
lemma tolerance_subset: "B ⊆ A ⟹ tolerance B (∼)"
apply intro_locales
using symmetric_subset reflexive_subset by auto
end
lemmas toleranceI = tolerance.intro
lemma tolerance_cong:
assumes r: "⋀a b. a ∈ A ⟹ b ∈ A ⟹ r a b ⟷ r' a b"
shows "tolerance A r ⟷ tolerance A r'"
by (simp add: tolerance_def r cong: reflexive_cong symmetric_cong)
lemma tolerance_empty[intro!]: "tolerance {} r" by (auto intro!: toleranceI)
global_interpretation equiv: tolerance UNIV "equivpartp r"
rewrites "⋀r. r ↾ UNIV ≡ r"
and "⋀x. x ∈ UNIV ≡ True"
and "⋀P1. (True ⟹ P1) ≡ Trueprop P1"
and "⋀P1 P2. (True ⟹ PROP P1 ⟹ PROP P2) ≡ (PROP P1 ⟹ PROP P2)"
by unfold_locales (auto simp:equivpartp_def)
locale partial_equivalence = symmetric +
assumes "transitive A (∼)"
begin
sublocale transitive A "(∼)"
rewrites "sympartp (∼)↾A ≡ (∼)↾A"
and "sympartp ((∼)↾A) ≡ (∼)↾A"
using partial_equivalence_axioms
unfolding partial_equivalence_axioms_def partial_equivalence_def
by (auto simp: atomize_eq sym intro!:ext)
lemma partial_equivalence_subset: "B ⊆ A ⟹ partial_equivalence B (∼)"
apply (intro partial_equivalence.intro partial_equivalence_axioms.intro)
using symmetric_subset transitive_subset by auto
end
lemmas partial_equivalenceI = partial_equivalence.intro[OF _ partial_equivalence_axioms.intro]
lemma partial_equivalence_cong:
assumes r: "⋀a b. a ∈ A ⟹ b ∈ A ⟹ r a b ⟷ r' a b"
shows "partial_equivalence A r ⟷ partial_equivalence A r'"
by (simp add: partial_equivalence_def partial_equivalence_axioms_def r
cong: transitive_cong symmetric_cong)
lemma partial_equivalence_empty[intro!]: "partial_equivalence {} r"
by (auto intro!: partial_equivalenceI)
locale equivalence = symmetric + reflexive A "(∼)" + transitive A "(∼)"
begin
sublocale tolerance + partial_equivalence + quasi_ordered_set A "(∼)"..
lemma equivalence_subset: "B ⊆ A ⟹ equivalence B (∼)"
apply (intro equivalence.intro)
using symmetric_subset transitive_subset by auto
end
lemmas equivalenceI = equivalence.intro
lemma equivalence_cong:
assumes r: "⋀a b. a ∈ A ⟹ b ∈ A ⟹ r a b ⟷ r' a b"
shows "equivalence A r ⟷ equivalence A r'"
by (simp add: equivalence_def r cong: reflexive_cong transitive_cong symmetric_cong)
text ‹Some combinations lead to uninteresting relations.›
context
fixes r :: "'a ⇒ 'a ⇒ bool" (infix "⨝" 50)
begin
proposition reflexive_irreflexive_is_empty:
assumes r: "reflexive A (⨝)" and ir: "irreflexive A (⨝)"
shows "A = {}"
proof (rule ccontr)
interpret irreflexive A "(⨝)" using ir.
interpret reflexive A "(⨝)" using r.
assume "A ≠ {}"
then obtain a where a: "a ∈ A" by auto
from a refl have "a ⨝ a" by auto
with irrefl a show False by auto
qed
proposition symmetric_antisymmetric_imp_eq:
assumes s: "symmetric A (⨝)" and as: "antisymmetric A (⨝)"
shows "(⨝)↾A ≤ (=)"
proof-
interpret symmetric A "(⨝)" + antisymmetric A "(⨝)" using assms by auto
show "?thesis" using antisym by (auto dest: sym)
qed
proposition nontolerance:
shows "irreflexive A (⨝) ∧ symmetric A (⨝) ⟷ tolerance A (λx y. ¬ x ⨝ y)"
proof (intro iffI conjI, elim conjE)
assume "irreflexive A (⨝)" and "symmetric A (⨝)"
then interpret irreflexive A "(⨝)" + symmetric A "(⨝)".
show "tolerance A (λx y. ¬ x ⨝ y)" by (unfold_locales, auto dest: sym irrefl)
next
assume "tolerance A (λx y. ¬ x ⨝ y)"
then interpret tolerance A "λx y. ¬ x ⨝ y".
show "irreflexive A (⨝)" by (auto simp: eq_implies)
show "symmetric A (⨝)" using sym by auto
qed
proposition irreflexive_transitive_symmetric_is_empty:
assumes irr: "irreflexive A (⨝)" and tr: "transitive A (⨝)" and sym: "symmetric A (⨝)"
shows "(⨝)↾A = bot"
proof (intro ext, unfold bot_fun_def bot_bool_def eq_False, rule notI, erule RestrpE)
interpret strict_ordered_set A "(⨝)" using assms by (unfold strict_ordered_set_def, auto)
interpret symmetric A "(⨝)" using assms by auto
fix x y assume x: "x ∈ A" and y: "y ∈ A"
assume xy: "x ⨝ y"
also note sym[OF xy x y]
finally have "x ⨝ x" using x y by auto
with x show False by auto
qed
end
subsection ‹Totality›
locale semiconnex = related_set _ "(⊏)" + less_syntax +
assumes semiconnex: "x ∈ A ⟹ y ∈ A ⟹ x ⊏ y ∨ x = y ∨ y ⊏ x"
begin
lemma cases[consumes 2, case_names less eq greater]:
assumes "x ∈ A" and "y ∈ A" and "x ⊏ y ⟹ P" and "x = y ⟹ P" and "y ⊏ x ⟹ P"
shows "P" using semiconnex assms by auto
lemma neqE:
assumes "x ∈ A" and "y ∈ A"
shows "x ≠ y ⟹ (x ⊏ y ⟹ P) ⟹ (y ⊏ x ⟹ P) ⟹ P"
by (cases rule: cases[OF assms], auto)
lemma semiconnex_subset: "B ⊆ A ⟹ semiconnex B (⊏)"
apply (intro semiconnex.intro)
using semiconnex by auto
end
lemmas semiconnexI[intro] = semiconnex.intro
text ‹Totality is negated antisymmetry \cite[Proposition 2.2.4]{Schmidt1993}.›
proposition semiconnex_iff_neg_antisymmetric:
fixes less (infix "⊏" 50)
shows "semiconnex A (⊏) ⟷ antisymmetric A (λx y. ¬ x ⊏ y)" (is "?l ⟷ ?r")
proof (intro iffI semiconnexI antisymmetricI)
assume ?l
then interpret semiconnex.
fix x y
assume "x ∈ A" "y ∈ A" "¬ x ⊏ y" and "¬ y ⊏ x"
then show "x = y" by (cases rule: cases, auto)
next
assume ?r
then interpret neg: antisymmetric A "(λx y. ¬ x ⊏ y)".
fix x y
show "x ∈ A ⟹ y ∈ A ⟹ x ⊏ y ∨ x = y ∨ y ⊏ x" using neg.antisym by auto
qed
lemma semiconnex_cong:
assumes r: "⋀a b. a ∈ A ⟹ b ∈ A ⟹ r a b ⟷ r' a b"
shows "semiconnex A r ⟷ semiconnex A r'"
by (simp add: semiconnex_iff_neg_antisymmetric r cong: antisymmetric_cong)
locale semiconnex_irreflexive = semiconnex + irreflexive
begin
lemma neq_iff: "x ∈ A ⟹ y ∈ A ⟹ x ≠ y ⟷ x ⊏ y ∨ y ⊏ x" by (auto elim:neqE dest: irrefl)
lemma semiconnex_irreflexive_subset: "B ⊆ A ⟹ semiconnex_irreflexive B (⊏)"
apply (intro semiconnex_irreflexive.intro)
using semiconnex_subset irreflexive_subset by auto
end
lemmas semiconnex_irreflexiveI = semiconnex_irreflexive.intro
lemma semiconnex_irreflexive_cong:
assumes r: "⋀a b. a ∈ A ⟹ b ∈ A ⟹ r a b ⟷ r' a b"
shows "semiconnex_irreflexive A r ⟷ semiconnex_irreflexive A r'"
by (simp add: semiconnex_irreflexive_def r cong: semiconnex_cong irreflexive_cong)
locale connex = related_set +
assumes comparable: "x ∈ A ⟹ y ∈ A ⟹ x ⊑ y ∨ y ⊑ x"
begin
interpretation less_eq_asymmetrize.
sublocale reflexive apply unfold_locales using comparable by auto
lemma comparable_cases[consumes 2, case_names le ge]:
assumes "x ∈ A" and "y ∈ A" and "x ⊑ y ⟹ P" and "y ⊑ x ⟹ P" shows "P"
using assms comparable by auto
lemma comparable_three_cases[consumes 2, case_names less eq greater]:
assumes "x ∈ A" and "y ∈ A" and "x ⊏ y ⟹ P" and "x ∼ y ⟹ P" and "y ⊏ x ⟹ P" shows "P"
using assms comparable by auto
lemma
assumes x: "x ∈ A" and y: "y ∈ A"
shows not_iff_asym: "¬x ⊑ y ⟷ y ⊏ x"
and not_asym_iff: "¬x ⊏ y ⟷ y ⊑ x"
using comparable[OF x y] by auto
lemma connex_subset: "B ⊆ A ⟹ connex B (⊑)"
by (intro connex.intro comparable, auto)
interpretation less_eq_asymmetrize.
end
lemmas connexI[intro] = connex.intro
lemmas connexE = connex.comparable_cases
lemma connex_empty: "connex {} A" by auto
context
fixes less_eq :: "'a ⇒ 'a ⇒ bool" (infix "⊑" 50)
begin
lemma connex_iff_semiconnex_reflexive: "connex A (⊑) ⟷ semiconnex A (⊑) ∧ reflexive A (⊑)"
(is "?c ⟷ ?t ∧ ?r")
proof (intro iffI conjI; (elim conjE)?)
assume ?c then interpret connex.
show ?t apply unfold_locales using comparable by auto
show ?r by unfold_locales
next
assume ?t then interpret semiconnex A "(⊑)".
assume ?r then interpret reflexive.
from semiconnex show ?c by auto
qed
lemma chain_connect: "Complete_Partial_Order.chain r A ≡ connex A r"
by (auto intro!: ext simp: atomize_eq connex_def Complete_Partial_Order.chain_def)
lemma connex_union:
assumes "connex X (⊑)" and "connex Y (⊑)" and "∀x ∈ X. ∀y ∈ Y. x ⊑ y ∨ y ⊑ x"
shows "connex (X∪Y) (⊑)"
using assms by (auto simp: connex_def)
end
lemma connex_cong:
assumes r: "⋀a b. a ∈ A ⟹ b ∈ A ⟹ r a b ⟷ r' a b"
shows "connex A r ⟷ connex A r'"
by (simp add: connex_iff_semiconnex_reflexive r cong: semiconnex_cong reflexive_cong)
locale total_pseudo_ordered_set = connex + antisymmetric
begin
sublocale pseudo_ordered_set ..
lemma not_weak_iff:
assumes x: "x ∈ A" and y: "y ∈ A" shows "¬ y ⊑ x ⟷ x ⊑ y ∧ x ≠ y"
using x y by (cases rule: comparable_cases, auto intro:antisym)
lemma total_pseudo_ordered_subset: "B ⊆ A ⟹ total_pseudo_ordered_set B (⊑)"
apply (intro_locales)
using antisymmetric_subset connex_subset by auto
interpretation less_eq_asymmetrize.
interpretation asympartp: semiconnex_irreflexive A "(⊏)"
proof (intro semiconnex_irreflexive.intro asympartp_irreflexive semiconnexI)
fix x y assume xA: "x ∈ A" and yA: "y ∈ A"
with comparable antisym
show "x ⊏ y ∨ x = y ∨ y ⊏ x" by (auto simp: asympartp_def)
qed
lemmas asympartp_semiconnex = asympartp.semiconnex_axioms
lemmas asympartp_semiconnex_irreflexive = asympartp.semiconnex_irreflexive_axioms
end
lemmas total_pseudo_ordered_setI = total_pseudo_ordered_set.intro
lemma total_pseudo_ordered_set_cong:
assumes r: "⋀a b. a ∈ A ⟹ b ∈ A ⟹ r a b ⟷ r' a b"
shows "total_pseudo_ordered_set A r ⟷ total_pseudo_ordered_set A r'"
by (simp add: total_pseudo_ordered_set_def r cong: connex_cong antisymmetric_cong)
locale total_quasi_ordered_set = connex + transitive
begin
sublocale quasi_ordered_set ..
lemma total_quasi_ordered_subset: "B ⊆ A ⟹ total_quasi_ordered_set B (⊑)"
using transitive_subset connex_subset by intro_locales
end
lemmas total_quasi_ordered_setI = total_quasi_ordered_set.intro
lemma total_quasi_ordered_set_cong:
assumes r: "⋀a b. a ∈ A ⟹ b ∈ A ⟹ r a b ⟷ r' a b"
shows "total_quasi_ordered_set A r ⟷ total_quasi_ordered_set A r'"
by (simp add: total_quasi_ordered_set_def r cong: connex_cong transitive_cong)
locale total_ordered_set = total_quasi_ordered_set + antisymmetric
begin
sublocale partially_ordered_set + total_pseudo_ordered_set ..
lemma total_ordered_subset: "B ⊆ A ⟹ total_ordered_set B (⊑)"
using total_quasi_ordered_subset antisymmetric_subset by (intro total_ordered_set.intro)
lemma weak_semiconnex: "semiconnex A (⊑)"
using connex_axioms by (simp add: connex_iff_semiconnex_reflexive)
interpretation less_eq_asymmetrize.
end
lemmas total_ordered_setI = total_ordered_set.intro[OF total_quasi_ordered_setI]
lemma total_ordered_set_cong:
assumes r: "⋀a b. a ∈ A ⟹ b ∈ A ⟹ r a b ⟷ r' a b"
shows "total_ordered_set A r ⟷ total_ordered_set A r'"
by (simp add: total_ordered_set_def r cong: total_quasi_ordered_set_cong antisymmetric_cong)
lemma monotone_connex_image:
fixes ir (infix "≼" 50) and r (infix "⊑" 50)
assumes mono: "monotone_on I (≼) (⊑) f" and connex: "connex I (≼)"
shows "connex (f ` I) (⊑)"
proof (rule connexI)
fix x y
assume "x ∈ f ` I" and "y ∈ f ` I"
then obtain i j where ij: "i ∈ I" "j ∈ I" and [simp]: "x = f i" "y = f j" by auto
from connex ij have "i ≼ j ∨ j ≼ i" by (auto elim: connexE)
with ij mono show "x ⊑ y ∨ y ⊑ x" by (elim disjE, auto dest: monotone_onD)
qed
subsection ‹Order Pairs›
text ‹We pair a relation (weak part) with a well-behaving ``strict'' part. Here no assumption is
put on the ``weak'' part.›
locale compatible_ordering =
related_set + irreflexive +
assumes strict_implies_weak: "x ⊏ y ⟹ x ∈ A ⟹ y ∈ A ⟹ x ⊑ y"
assumes weak_strict_trans[trans]: "x ⊑ y ⟹ y ⊏ z ⟹ x ∈ A ⟹ y ∈ A ⟹ z ∈ A ⟹ x ⊏ z"
assumes strict_weak_trans[trans]: "x ⊏ y ⟹ y ⊑ z ⟹ x ∈ A ⟹ y ∈ A ⟹ z ∈ A ⟹ x ⊏ z"
begin
text ‹The following sequence of declarations are in order to obtain fact names in a manner
similar to the Isabelle/HOL facts of orders.›
text ‹The strict part is necessarily transitive.›
sublocale strict: transitive A "(⊏)"
using weak_strict_trans[OF strict_implies_weak] by unfold_locales
sublocale strict_ordered_set A "(⊏)" ..
thm strict.trans asym irrefl
lemma Restrp_compatible_ordering: "compatible_ordering UNIV ((⊑)↾A) ((⊏)↾A)"
apply (unfold_locales)
by (auto dest: weak_strict_trans strict_weak_trans strict_implies_weak)
lemma strict_implies_not_weak: "x ⊏ y ⟹ x ∈ A ⟹ y ∈ A ⟹ ¬ y ⊑ x"
using irrefl weak_strict_trans by blast
lemma weak_implies_not_strict:
assumes xy: "x ⊑ y" and [simp]: "x ∈ A" "y ∈ A"
shows "¬y ⊏ x"
proof
assume "y ⊏ x"
also note xy
finally show False using irrefl by auto
qed
lemma compatible_ordering_subset: assumes "X ⊆ A" shows "compatible_ordering X (⊑) (⊏)"
apply unfold_locales
using assms strict_implies_weak by (auto intro: strict_weak_trans weak_strict_trans)
end
context transitive begin
interpretation less_eq_asymmetrize.
lemma asym_trans[trans]:
shows "x ⊏ y ⟹ y ⊑ z ⟹ x ∈ A ⟹ y ∈ A ⟹ z ∈ A ⟹ x ⊏ z"
and "x ⊑ y ⟹ y ⊏ z ⟹ x ∈ A ⟹ y ∈ A ⟹ z ∈ A ⟹ x ⊏ z"
by (auto 0 3 dest: trans)
lemma asympartp_compatible_ordering: "compatible_ordering A (⊑) (⊏)"
apply unfold_locales
by (auto dest: asym_trans)
end
locale reflexive_ordering = reflexive + compatible_ordering
locale reflexive_attractive_ordering = reflexive_ordering + attractive
locale pseudo_ordering = pseudo_ordered_set + compatible_ordering
begin
sublocale reflexive_attractive_ordering..
end
locale quasi_ordering = quasi_ordered_set + compatible_ordering
begin
sublocale reflexive_attractive_ordering..
lemma quasi_ordering_subset: assumes "X ⊆ A" shows "quasi_ordering X (⊑) (⊏)"
by (intro quasi_ordering.intro quasi_ordered_subset compatible_ordering_subset assms)
end
context quasi_ordered_set begin
interpretation less_eq_asymmetrize.
lemma asympartp_quasi_ordering: "quasi_ordering A (⊑) (⊏)"
by (intro quasi_ordering.intro quasi_ordered_set_axioms asympartp_compatible_ordering)
end
locale partial_ordering = partially_ordered_set + compatible_ordering
begin
sublocale quasi_ordering + pseudo_ordering..
lemma partial_ordering_subset: assumes "X ⊆ A" shows "partial_ordering X (⊑) (⊏)"
by (intro partial_ordering.intro partially_ordered_subset compatible_ordering_subset assms)
end
context partially_ordered_set begin
interpretation less_eq_asymmetrize.
lemma asympartp_partial_ordering: "partial_ordering A (⊑) (⊏)"
by (intro partial_ordering.intro partially_ordered_set_axioms asympartp_compatible_ordering)
end
locale total_quasi_ordering = total_quasi_ordered_set + compatible_ordering
begin
sublocale quasi_ordering..
lemma total_quasi_ordering_subset: assumes "X ⊆ A" shows "total_quasi_ordering X (⊑) (⊏)"
by (intro total_quasi_ordering.intro total_quasi_ordered_subset compatible_ordering_subset assms)
end
context total_quasi_ordered_set begin
interpretation less_eq_asymmetrize.
lemma asympartp_total_quasi_ordering: "total_quasi_ordering A (⊑) (⊏)"
by (intro total_quasi_ordering.intro total_quasi_ordered_set_axioms asympartp_compatible_ordering)
end
text ‹Fixing the definition of the strict part is very common, though it looks restrictive
to the author.›
locale strict_quasi_ordering = quasi_ordered_set + less_syntax +
assumes strict_iff: "x ∈ A ⟹ y ∈ A ⟹ x ⊏ y ⟷ x ⊑ y ∧ ¬y ⊑ x"
begin
sublocale compatible_ordering
proof unfold_locales
fix x y z
show "x ∈ A ⟹ ¬ x ⊏ x" by (auto simp: strict_iff)
{ assume xy: "x ⊑ y" and yz: "y ⊏ z" and x: "x ∈ A" and y: "y ∈ A" and z: "z ∈ A"
from yz y z have ywz: "y ⊑ z" and zy: "¬z ⊑ y" by (auto simp: strict_iff)
from trans[OF xy ywz]x y z have xz: "x ⊑ z" by auto
from trans[OF _ xy] x y z zy have zx: "¬z ⊑ x" by auto
from xz zx x z show "x ⊏ z" by (auto simp: strict_iff)
}
{ assume xy: "x ⊏ y" and yz: "y ⊑ z" and x: "x ∈ A" and y: "y ∈ A" and z: "z ∈ A"
from xy x y have xwy: "x ⊑ y" and yx: "¬y ⊑ x" by (auto simp: strict_iff)
from trans[OF xwy yz]x y z have xz: "x ⊑ z" by auto
from trans[OF yz] x y z yx have zx: "¬z ⊑ x" by auto
from xz zx x z show "x ⊏ z" by (auto simp: strict_iff)
}
{ show "x ⊏ y ⟹ x ∈ A ⟹ y ∈ A ⟹ x ⊑ y" by (auto simp: strict_iff) }
qed
end
locale strict_partial_ordering = strict_quasi_ordering + antisymmetric
begin
sublocale partial_ordering..
lemma strict_iff_neq: "x ∈ A ⟹ y ∈ A ⟹ x ⊏ y ⟷ x ⊑ y ∧ x ≠ y"
by (auto simp: strict_iff antisym)
end
locale total_ordering = reflexive + compatible_ordering + semiconnex A "(⊏)"
begin
sublocale semiconnex_irreflexive ..
sublocale connex
proof
fix x y assume x: "x ∈ A" and y: "y ∈ A"
then show "x ⊑ y ∨ y ⊑ x"
by (cases rule: cases, auto dest: strict_implies_weak)
qed
lemma not_weak:
assumes "x ∈ A" and "y ∈ A" shows "¬ x ⊑ y ⟷ y ⊏ x"
using assms by (cases rule:cases, auto simp: strict_implies_not_weak dest: strict_implies_weak)
lemma not_strict: "x ∈ A ⟹ y ∈ A ⟹ ¬ x ⊏ y ⟷ y ⊑ x"
using not_weak by blast
sublocale strict_partial_ordering
proof
fix a b
assume a: "a ∈ A" and b: "b ∈ A"
then show "a ⊏ b ⟷ a ⊑ b ∧ ¬ b ⊑ a" by (auto simp: not_strict[symmetric] dest: asym)
next
fix x y z assume xy: "x ⊑ y" and yz: "y ⊑ z" and xA: "x ∈ A" and yA: "y ∈ A" and zA: "z ∈ A"
with weak_strict_trans[OF yz] show "x ⊑ z" by (auto simp: not_strict[symmetric])
next
fix x y assume xy: "x ⊑ y" and yx: "y ⊑ x" and xA: "x ∈ A" and yA: "y ∈ A"
with semiconnex show "x = y" by (auto dest: weak_implies_not_strict)
qed
sublocale total_ordered_set..
context
fixes s
assumes s: "∀x ∈ A. x ⊏ s ⟶ (∃z ∈ A. x ⊏ z ∧ z ⊏ s)" and sA: "s ∈ A"
begin
lemma dense_weakI:
assumes bound: "⋀x. x ⊏ s ⟹ x ∈ A ⟹ x ⊑ y" and yA: "y ∈ A"
shows "s ⊑ y"
proof (rule ccontr)
assume "¬ ?thesis"
with yA sA have "y ⊏ s" by (simp add: not_weak)
from s[rule_format, OF yA this]
obtain x where xA: "x ∈ A" and xs: "x ⊏ s" and yx: "y ⊏ x" by safe
have xy: "x ⊑ y" using bound[OF xs xA] .
from yx xy xA yA
show False by (simp add: weak_implies_not_strict)
qed
lemma dense_bound_iff:
assumes bA: "b ∈ A" shows "bound {x∈A. x ⊏ s} (⊑) b ⟷ s ⊑ b"
using assms sA
by (auto simp: bound_def intro: strict_implies_weak strict_weak_trans dense_weakI)
lemma dense_extreme_bound:
"extreme_bound A (⊑) {x ∈ A. x ⊏ s} s"
by (auto intro!: extreme_boundI intro: strict_implies_weak simp: dense_bound_iff sA)
end
lemma ordinal_cases[consumes 1, case_names suc lim]:
assumes aA: "a ∈ A"
and suc: "⋀p. extreme {x ∈ A. x ⊏ a} (⊑) p ⟹ thesis"
and lim: "extreme_bound A (⊑) {x ∈ A. x ⊏ a} a ⟹ thesis"
shows "thesis"
proof (cases "∃p. extreme {x ∈ A. x ⊏ a} (⊑) p")
case True
with suc show ?thesis by auto
next
case False
show ?thesis
proof (rule lim, rule dense_extreme_bound, safe intro!: aA)
fix x assume xA: "x ∈ A" and xa: "x ⊏ a"
show "∃z∈A. x ⊏ z ∧ z ⊏ a"
proof (rule ccontr)
assume "¬?thesis"
with xA xa have "extreme {x ∈ A. x ⊏ a} (⊑) x" by (auto simp: not_strict)
with False show False by auto
qed
qed
qed
end
context total_ordered_set begin
interpretation less_eq_asymmetrize.
lemma asympartp_total_ordering: "total_ordering A (⊑) (⊏)"
by (intro total_ordering.intro reflexive_axioms asympartp_compatible_ordering asympartp_semiconnex)
end
subsection ‹Functions›
definition "pointwise I r f g ≡ ∀i ∈ I. r (f i) (g i)"
lemmas pointwiseI = pointwise_def[unfolded atomize_eq, THEN iffD2, rule_format]
lemmas pointwiseD[simp] = pointwise_def[unfolded atomize_eq, THEN iffD1, rule_format]
lemma pointwise_cong:
assumes "r = r'" "⋀i. i ∈ I ⟹ f i = f' i" "⋀i. i ∈ I ⟹ g i = g' i"
shows "pointwise I r f g = pointwise I r' f' g'"
using assms by (auto simp: pointwise_def)
lemma pointwise_empty[simp]: "pointwise {} = ⊤" by (auto intro!: ext pointwiseI)
lemma dual_pointwise[simp]: "(pointwise I r)⇧- = pointwise I r⇧-"
by (auto intro!: ext pointwiseI dest: pointwiseD)
lemma pointwise_dual: "pointwise I r⇧- f g ⟹ pointwise I r g f" by (auto simp: pointwise_def)
lemma pointwise_un: "pointwise (I∪J) r = pointwise I r ⊓ pointwise J r"
by (auto intro!: ext pointwiseI)
lemma pointwise_unI[intro!]: "pointwise I r f g ⟹ pointwise J r f g ⟹ pointwise (I ∪ J) r f g"
by (auto simp: pointwise_un)
lemma pointwise_bound: "bound F (pointwise I r) f ⟷ (∀i ∈ I. bound {f i |. f ∈ F} r (f i))"
by (auto intro!:pointwiseI elim!: boundE)
lemma pointwise_extreme:
shows "extreme F (pointwise X r) e ⟷ e ∈ F ∧ (∀x ∈ X. extreme {f x |. f ∈ F} r (e x))"
by (auto intro!: pointwiseI extremeI elim!: extremeE)
lemma pointwise_extreme_bound:
fixes r (infix "⊑" 50)
assumes F: "F ⊆ {f. f ` X ⊆ A}"
shows "extreme_bound {f. f ` X ⊆ A} (pointwise X (⊑)) F s ⟷
(∀x ∈ X. extreme_bound A (⊑) {f x |. f ∈ F} (s x))" (is "?p ⟷ ?a")
proof (safe intro!: extreme_boundI pointwiseI)
fix x
assume s: ?p and xX: "x ∈ X"
{ fix b
assume b: "bound {f x |. f ∈ F} (⊑) b" and bA: "b ∈ A"
have "pointwise X (⊑) s (s(x:=b))"
proof (rule extreme_boundD(2)[OF s], safe intro!: pointwiseI)
fix f y
assume fF: "f ∈ F" and yX: "y ∈ X"
show "f y ⊑ (s(x:=b)) y"
proof (cases "x = y")
case True
with b fF show "?thesis" by auto
next
case False
with s[THEN extreme_bound_imp_bound] fF yX show ?thesis by (auto dest: boundD)
qed
next
fix y assume "y ∈ X" with bA s show "(s(x := b)) y ∈ A" by auto
qed
with xX show "s x ⊑ b" by (auto dest: pointwiseD)
next
fix f assume "f ∈ F"
from extreme_boundD(1)[OF s this] F xX
show "f x ⊑ s x" by auto
next
show "s x ∈ A" using s xX by auto
}
next
fix x
assume s: ?a and xX: "x ∈ X"
{ from s xX show "s x ∈ A" by auto
next
fix b assume b: "bound F (pointwise X (⊑)) b" and bA: "b ` X ⊆ A"
with xX have "bound {f x |. f ∈ F} (⊑) (b x)" by (auto simp: pointwise_bound)
with s[rule_format, OF xX] bA xX show "s x ⊑ b x" by auto
next
fix f assume "f ∈ F"
with s[rule_format, OF xX] show "f x ⊑ s x" by auto
}
qed
lemma dual_pointwise_extreme_bound:
"extreme_bound FA (pointwise X r)⇧- F = extreme_bound FA (pointwise X r⇧-) F"
by (simp)
lemma pointwise_monotone_on:
fixes less_eq (infix "⊑" 50) and prec_eq (infix "≼" 50)
shows "monotone_on I (≼) (pointwise A (⊑)) f ⟷
(∀a ∈ A. monotone_on I (≼) (⊑) (λi. f i a))" (is "?l ⟷ ?r")
proof (safe intro!: monotone_onI pointwiseI)
fix a i j assume aA: "a ∈ A" and *: ?l "i ≼ j" "i ∈ I" "j ∈ I"
then
show "f i a ⊑ f j a" by (auto dest: monotone_onD)
next
fix a i j assume ?r and "a ∈ A" and ij: "i ≼ j" "i ∈ I" "j ∈ I"
then have "monotone_on I (≼) (⊑) (λi. f i a)" by auto
from monotone_onD[OF this]ij
show "f i a ⊑ f j a" by auto
qed
lemmas pointwise_monotone = pointwise_monotone_on[of UNIV]
lemma (in reflexive) pointwise_reflexive: "reflexive {f. f ` I ⊆ A} (pointwise I (⊑))"
apply unfold_locales by (auto intro!: pointwiseI simp: subsetD[OF _ imageI])
lemma (in irreflexive) pointwise_irreflexive:
assumes I0: "I ≠ {}" shows "irreflexive {f. f ` I ⊆ A} (pointwise I (⊏))"
proof (safe intro!: irreflexive.intro)
fix f
assume f: "f ` I ⊆ A" and ff: "pointwise I (⊏) f f"
from I0 obtain i where i: "i ∈ I" by auto
with ff have "f i ⊏ f i" by auto
with f i show False by auto
qed
lemma (in semiattractive) pointwise_semiattractive: "semiattractive {f. f ` I ⊆ A} (pointwise I (⊑))"
proof (unfold_locales, safe intro!: pointwiseI)
fix f g h i
assume fg: "pointwise I (⊑) f g" and gf: "pointwise I (⊑) g f" and gh: "pointwise I (⊑) g h"
and [simp]: "i ∈ I" and f: "f ` I ⊆ A" and g: "g ` I ⊆ A" and h: "h ` I ⊆ A"
show "f i ⊑ h i"
proof (rule attract)
from fg show "f i ⊑ g i" by auto
from gf show "g i ⊑ f i" by auto
from gh show "g i ⊑ h i" by auto
qed (insert f g h, auto simp: subsetD[OF _ imageI])
qed
lemma (in attractive) pointwise_attractive: "attractive {f. f ` I ⊆ A} (pointwise I (⊑))"
apply (intro attractive.intro attractive_axioms.intro)
using pointwise_semiattractive dual.pointwise_semiattractive by auto
text ‹Antisymmetry will not be preserved by pointwise extension over restricted domain.›
lemma (in antisymmetric) pointwise_antisymmetric:
"antisymmetric {f. f ` I ⊆ A} (pointwise I (⊑))"
oops
lemma (in transitive) pointwise_transitive: "transitive {f. f ` I ⊆ A} (pointwise I (⊑))"
proof (unfold_locales, safe intro!: pointwiseI)
fix f g h i
assume fg: "pointwise I (⊑) f g" and gh: "pointwise I (⊑) g h"
and [simp]: "i ∈ I" and f: "f ` I ⊆ A" and g: "g ` I ⊆ A" and h: "h ` I ⊆ A"
from fg have "f i ⊑ g i" by auto
also from gh have "g i ⊑ h i" by auto
finally show "f i ⊑ h i" using f g h by (auto simp: subsetD[OF _ imageI])
qed
lemma (in quasi_ordered_set) pointwise_quasi_order:
"quasi_ordered_set {f. f ` I ⊆ A} (pointwise I (⊑))"
by (intro quasi_ordered_setI pointwise_transitive pointwise_reflexive)
lemma (in compatible_ordering) pointwise_compatible_ordering:
assumes I0: "I ≠ {}"
shows "compatible_ordering {f. f ` I ⊆ A} (pointwise I (⊑)) (pointwise I (⊏))"
proof (intro compatible_ordering.intro compatible_ordering_axioms.intro pointwise_irreflexive[OF I0], safe intro!: pointwiseI)
fix f g h i
assume fg: "pointwise I (⊑) f g" and gh: "pointwise I (⊏) g h"
and [simp]: "i ∈ I" and f: "f ` I ⊆ A" and g: "g ` I ⊆ A" and h: "h ` I ⊆ A"
from fg have "f i ⊑ g i" by auto
also from gh have "g i ⊏ h i" by auto
finally show "f i ⊏ h i" using f g h by (auto simp: subsetD[OF _ imageI])
next
fix f g h i
assume fg: "pointwise I (⊏) f g" and gh: "pointwise I (⊑) g h"
and [simp]: "i ∈ I" and f: "f ` I ⊆ A" and g: "g ` I ⊆ A" and h: "h ` I ⊆ A"
from fg have "f i ⊏ g i" by auto
also from gh have "g i ⊑ h i" by auto
finally show "f i ⊏ h i" using f g h by (auto simp: subsetD[OF _ imageI])
next
fix f g i
assume fg: "pointwise I (⊏) f g"
and [simp]: "i ∈ I"
and f: "f ` I ⊆ A" and g: "g ` I ⊆ A"
from fg have "f i ⊏ g i" by auto
with f g show "f i ⊑ g i" by (auto simp: subsetD[OF _ imageI] strict_implies_weak)
qed
subsection ‹Relating to Classes›
text ‹In Isabelle 2020, we should declare sublocales in class before declaring dual
sublocales, since otherwise facts would be prefixed by ``dual.dual.''›
context ord begin
abbreviation least where "least X ≡ extreme X (λx y. y ≤ x)"
abbreviation greatest where "greatest X ≡ extreme X (≤)"
abbreviation supremum where "supremum X ≡ least (Collect (bound X (≤)))"
abbreviation infimum where "infimum X ≡ greatest (Collect (bound X (λx y. y ≤ x)))"
lemma supremumI: "bound X (≤) s ⟹ (⋀b. bound X (≤) b ⟹ s ≤ b) ⟹ supremum X s"
and infimumI: "bound X (≥) i ⟹ (⋀b. bound X (≥) b ⟹ b ≤ i) ⟹ infimum X i"
by (auto intro!: extremeI)
lemma supremumE: "supremum X s ⟹
(bound X (≤) s ⟹ (⋀b. bound X (≤) b ⟹ s ≤ b) ⟹ thesis) ⟹ thesis"
and infimumE: "infimum X i ⟹
(bound X (≥) i ⟹ (⋀b. bound X (≥) b ⟹ b ≤ i) ⟹ thesis) ⟹ thesis"
by (auto)
lemma extreme_bound_supremum[simp]: "extreme_bound UNIV (≤) = supremum" by (auto intro!: ext)
lemma extreme_bound_infimum[simp]: "extreme_bound UNIV (≥) = infimum" by (auto intro!: ext)
lemma Least_eq_The_least: "Least P = The (least {x. P x})"
by (auto simp: Least_def extreme_def[unfolded atomize_eq, THEN ext])
lemma Greatest_eq_The_greatest: "Greatest P = The (greatest {x. P x})"
by (auto simp: Greatest_def extreme_def[unfolded atomize_eq, THEN ext])
end
lemma Ball_UNIV[simp]: "Ball UNIV = All" by auto
lemma Bex_UNIV[simp]: "Bex UNIV = Ex" by auto
lemma pointwise_UNIV_le[simp]: "pointwise UNIV (≤) = (≤)" by (intro ext, simp add: pointwise_def le_fun_def)
lemma pointwise_UNIV_ge[simp]: "pointwise UNIV (≥) = (≥)" by (intro ext, simp add: pointwise_def le_fun_def)
lemma fun_supremum_iff: "supremum F e ⟷ (∀x. supremum {f x |. f ∈ F} (e x))"
using pointwise_extreme_bound[of F UNIV UNIV "(≤)"] by simp
lemma fun_infimum_iff: "infimum F e ⟷ (∀x. infimum {f x |. f ∈ F} (e x))"
using pointwise_extreme_bound[of F UNIV UNIV "(≥)"] by simp
class reflorder = ord + assumes "reflexive_ordering UNIV (≤) (<)"
begin
sublocale order: reflexive_ordering UNIV
rewrites "⋀x. x ∈ UNIV ≡ True"
and "⋀X. X ⊆ UNIV ≡ True"
and "⋀r. r ↾ UNIV ≡ r"
and "⋀P. True ∧ P ≡ P"
and "Ball UNIV ≡ All"
and "Bex UNIV ≡ Ex"
and "sympartp (≤)⇧- ≡ sympartp (≤)"
and "⋀P1. (True ⟹ PROP P1) ≡ PROP P1"
and "⋀P1. (True ⟹ P1) ≡ Trueprop P1"
and "⋀P1 P2. (True ⟹ PROP P1 ⟹ PROP P2) ≡ (PROP P1 ⟹ PROP P2)"
using reflorder_axioms unfolding class.reflorder_def by (auto 0 4 simp:atomize_eq)
end
text ‹We should have imported locale-based facts in classes, e.g.:›
thm order.trans order.strict.trans order.refl order.irrefl order.asym order.extreme_bound_singleton
class attrorder = ord +
assumes "reflexive_attractive_ordering UNIV (≤) (<)"
begin
text ‹We need to declare subclasses before sublocales in order to preserve facts for superclasses.›
subclass reflorder
proof-
interpret reflexive_attractive_ordering UNIV
using attrorder_axioms unfolding class.attrorder_def by auto
show "class.reflorder (≤) (<)"..
qed
sublocale order: reflexive_attractive_ordering UNIV
rewrites "⋀x. x ∈ UNIV ≡ True"
and "⋀X. X ⊆ UNIV ≡ True"
and "⋀r. r ↾ UNIV ≡ r"
and "⋀P. True ∧ P ≡ P"
and "Ball UNIV ≡ All"
and "Bex UNIV ≡ Ex"
and "sympartp (≤)⇧- ≡ sympartp (≤)"
and "⋀P1. (True ⟹ PROP P1) ≡ PROP P1"
and "⋀P1. (True ⟹ P1) ≡ Trueprop P1"
and "⋀P1 P2. (True ⟹ PROP P1 ⟹ PROP P2) ≡ (PROP P1 ⟹ PROP P2)"
using attrorder_axioms unfolding class.attrorder_def
by (auto simp:atomize_eq)
end
thm order.extreme_bound_quasi_const
class psorder = ord + assumes "pseudo_ordering UNIV (≤) (<)"
begin
subclass attrorder
proof-
interpret pseudo_ordering UNIV
using psorder_axioms unfolding class.psorder_def by auto
show "class.attrorder (≤) (<)"..
qed
sublocale order: pseudo_ordering UNIV
rewrites "⋀x. x ∈ UNIV ≡ True"
and "⋀X. X ⊆ UNIV ≡ True"
and "⋀r. r ↾ UNIV ≡ r"
and "⋀P. True ∧ P ≡ P"
and "Ball UNIV ≡ All"
and "Bex UNIV ≡ Ex"
and "sympartp (≤)⇧- ≡ sympartp (≤)"
and "⋀P1. (True ⟹ PROP P1) ≡ PROP P1"
and "⋀P1. (True ⟹ P1) ≡ Trueprop P1"
and "⋀P1 P2. (True ⟹ PROP P1 ⟹ PROP P2) ≡ (PROP P1 ⟹ PROP P2)"
using psorder_axioms unfolding class.psorder_def by (auto simp:atomize_eq)
end
class qorder = ord + assumes "quasi_ordering UNIV (≤) (<)"
begin
subclass attrorder
proof-
interpret quasi_ordering UNIV
using qorder_axioms unfolding class.qorder_def by auto
show "class.attrorder (≤) (<)"..
qed
sublocale order: quasi_ordering UNIV
rewrites "⋀x. x ∈ UNIV ≡ True"
and "⋀X. X ⊆ UNIV ≡ True"
and "⋀r. r ↾ UNIV ≡ r"
and "⋀P. True ∧ P ≡ P"
and "Ball UNIV ≡ All"
and "Bex UNIV ≡ Ex"
and "sympartp (≤)⇧- ≡ sympartp (≤)"
and "⋀P1. (True ⟹ PROP P1) ≡ PROP P1"
and "⋀P1. (True ⟹ P1) ≡ Trueprop P1"
and "⋀P1 P2. (True ⟹ PROP P1 ⟹ PROP P2) ≡ (PROP P1 ⟹ PROP P2)"
using qorder_axioms unfolding class.qorder_def by (auto simp:atomize_eq)
lemmas [intro!] = order.quasi_ordered_subset
end
class porder = ord + assumes "partial_ordering UNIV (≤) (<)"
begin
interpretation partial_ordering UNIV
using porder_axioms unfolding class.porder_def by auto
subclass psorder..
subclass qorder..
sublocale order: partial_ordering UNIV
rewrites "⋀x. x ∈ UNIV ≡ True"
and "⋀X. X ⊆ UNIV ≡ True"
and "⋀r. r ↾ UNIV ≡ r"
and "⋀P. True ∧ P ≡ P"
and "Ball UNIV ≡ All"
and "Bex UNIV ≡ Ex"
and "sympartp (≤)⇧- ≡ sympartp (≤)"
and "⋀P1. (True ⟹ PROP P1) ≡ PROP P1"
and "⋀P1. (True ⟹ P1) ≡ Trueprop P1"
and "⋀P1 P2. (True ⟹ PROP P1 ⟹ PROP P2) ≡ (PROP P1 ⟹ PROP P2)"
apply unfold_locales by (auto simp:atomize_eq)
end
class linqorder = ord + assumes "total_quasi_ordering UNIV (≤) (<)"
begin
interpretation total_quasi_ordering UNIV
using linqorder_axioms unfolding class.linqorder_def by auto
subclass qorder..
sublocale order: total_quasi_ordering UNIV
rewrites "⋀x. x ∈ UNIV ≡ True"
and "⋀X. X ⊆ UNIV ≡ True"
and "⋀r. r ↾ UNIV ≡ r"
and "⋀P. True ∧ P ≡ P"
and "Ball UNIV ≡ All"
and "Bex UNIV ≡ Ex"
and "sympartp (≤)⇧- ≡ sympartp (≤)"
and "⋀P1. (True ⟹ PROP P1) ≡ PROP P1"
and "⋀P1. (True ⟹ P1) ≡ Trueprop P1"
and "⋀P1 P2. (True ⟹ PROP P1 ⟹ PROP P2) ≡ (PROP P1 ⟹ PROP P2)"
using linqorder_axioms unfolding class.linqorder_def
by (auto simp:atomize_eq)
lemmas asympartp_le = order.not_iff_asym[symmetric, abs_def]
end
text ‹Isabelle/HOL's @{class preorder} belongs to @{class qorder}, but not vice versa.›
context preorder begin
text ‹The relation @{term "(<)"} is defined as the antisymmetric part of @{term "(≤)"}.›
lemma [simp]:
shows asympartp_le: "asympartp (≤) = (<)"
and asympartp_ge: "asympartp (≥) = (>)"
by (intro ext, auto simp: asympartp_def less_le_not_le)
interpretation strict_quasi_ordering UNIV "(≤)" "(<)"
apply unfold_locales
using order_refl apply assumption
using order_trans apply assumption
using less_le_not_le apply assumption
done
subclass qorder..
sublocale order: strict_quasi_ordering UNIV
rewrites "⋀x. x ∈ UNIV ≡ True"
and "⋀X. X ⊆ UNIV ≡ True"
and "⋀r. r ↾ UNIV ≡ r"
and "⋀P. True ∧ P ≡ P"
and "Ball UNIV ≡ All"
and "Bex UNIV ≡ Ex"
and "sympartp (≤)⇧- ≡ sympartp (≤)"
and "⋀P1. (True ⟹ PROP P1) ≡ PROP P1"
and "⋀P1. (True ⟹ P1) ≡ Trueprop P1"
and "⋀P1 P2. (True ⟹ PROP P1 ⟹ PROP P2) ≡ (PROP P1 ⟹ PROP P2)"
apply unfold_locales
by (auto simp:atomize_eq)
end
context order begin
interpretation strict_partial_ordering UNIV "(≤)" "(<)"
apply unfold_locales
using order_antisym by assumption
subclass porder..
sublocale order: strict_partial_ordering UNIV
rewrites "⋀x. x ∈ UNIV ≡ True"
and "⋀X. X ⊆ UNIV ≡ True"
and "⋀r. r ↾ UNIV ≡ r"
and "⋀P. True ∧ P ≡ P"
and "Ball UNIV ≡ All"
and "Bex UNIV ≡ Ex"
and "sympartp (≤)⇧- ≡ sympartp (≤)"
and "⋀P1. (True ⟹ PROP P1) ≡ PROP P1"
and "⋀P1. (True ⟹ P1) ≡ Trueprop P1"
and "⋀P1 P2. (True ⟹ PROP P1 ⟹ PROP P2) ≡ (PROP P1 ⟹ PROP P2)"
apply unfold_locales
by (auto simp:atomize_eq)
end
text ‹Isabelle/HOL's @{class linorder} is equivalent to our locale @{locale total_ordering}.›
context linorder begin
subclass linqorder apply unfold_locales by auto
sublocale order: total_ordering UNIV
rewrites "⋀x. x ∈ UNIV ≡ True"
and "⋀X. X ⊆ UNIV ≡ True"
and "⋀r. r ↾ UNIV ≡ r"
and "⋀P. True ∧ P ≡ P"
and "Ball UNIV ≡ All"
and "Bex UNIV ≡ Ex"
and "sympartp (≤)⇧- ≡ sympartp (≤)"
and "⋀P1. (True ⟹ PROP P1) ≡ PROP P1"
and "⋀P1. (True ⟹ P1) ≡ Trueprop P1"
and "⋀P1 P2. (True ⟹ PROP P1 ⟹ PROP P2) ≡ (PROP P1 ⟹ PROP P2)"
apply unfold_locales by (auto simp:atomize_eq)
end
text ‹Tests: facts should be available in the most general classes.›
thm order.strict.trans[where 'a="'a::reflorder"]
thm order.extreme_bound_quasi_const[where 'a="'a::attrorder"]
thm order.extreme_bound_singleton_eq[where 'a="'a::psorder"]
thm order.trans[where 'a="'a::qorder"]
thm order.comparable_cases[where 'a="'a::linqorder"]
thm order.cases[where 'a="'a::linorder"]
subsection ‹Declaring Duals›
sublocale reflexive ⊆ sym: reflexive A "sympartp (⊑)"
rewrites "sympartp (⊑)⇧- ≡ sympartp (⊑)"
and "⋀r. sympartp (sympartp r) ≡ sympartp r"
and "⋀r. sympartp r ↾ A ≡ sympartp (r ↾ A)"
by (auto 0 4 simp:atomize_eq)
sublocale quasi_ordered_set ⊆ sym: quasi_ordered_set A "sympartp (⊑)"
rewrites "sympartp (⊑)⇧- = sympartp (⊑)"
and "sympartp (sympartp (⊑)) = sympartp (⊑)"
apply unfold_locales by (auto 0 4 dest: trans)
text ‹At this point, we declare dual as sublocales.
In the following, ``rewrites'' eventually cleans up redundant facts.›
sublocale reflexive ⊆ dual: reflexive A "(⊑)⇧-"
rewrites "sympartp (⊑)⇧- ≡ sympartp (⊑)"
and "⋀r. sympartp (r ↾ A) ≡ sympartp r ↾ A"
and "(⊑)⇧- ↾ A ≡ ((⊑) ↾ A)⇧-"
by (auto simp: atomize_eq)
context attractive begin
interpretation less_eq_symmetrize.
sublocale dual: attractive A "(⊒)"
rewrites "sympartp (⊒) = (∼)"
and "equivpartp (⊒) ≡ (≃)"
and "⋀r. sympartp (r ↾ A) ≡ sympartp r ↾ A"
and "⋀r. sympartp (sympartp r) ≡ sympartp r"
and "(⊑)⇧- ↾ A ≡ ((⊑) ↾ A)⇧-"
apply unfold_locales by (auto intro!: ext dest: attract dual.attract simp: atomize_eq)
end
context irreflexive begin
sublocale dual: irreflexive A "(⊏)⇧-"
rewrites "(⊏)⇧- ↾ A ≡ ((⊏) ↾ A)⇧-"
apply unfold_locales by (auto dest: irrefl simp: atomize_eq)
end
sublocale transitive ⊆ dual: transitive A "(⊑)⇧-"
rewrites "(⊑)⇧- ↾ A ≡ ((⊑) ↾ A)⇧-"
and "sympartp (⊑)⇧- = sympartp (⊑)"
and "asympartp (⊑)⇧- = (asympartp (⊑))⇧-"
apply unfold_locales by (auto dest: trans simp: atomize_eq intro!:ext)
sublocale antisymmetric ⊆ dual: antisymmetric A "(⊑)⇧-"
rewrites "(⊑)⇧- ↾ A ≡ ((⊑) ↾ A)⇧-"
and "sympartp (⊑)⇧- = sympartp (⊑)"
by (auto dest: antisym simp: atomize_eq)
context antisymmetric begin
lemma extreme_bound_unique:
"extreme_bound A (⊑) X x ⟹ extreme_bound A (⊑) X y ⟷ x = y"
apply (unfold extreme_bound_def)
apply (rule dual.extreme_unique) by auto
lemma ex_extreme_bound_iff_ex1:
"Ex (extreme_bound A (⊑) X) ⟷ Ex1 (extreme_bound A (⊑) X)"
apply (unfold extreme_bound_def)
apply (rule dual.ex_extreme_iff_ex1) by auto
lemma ex_extreme_bound_iff_the:
"Ex (extreme_bound A (⊑) X) ⟷ extreme_bound A (⊑) X (The (extreme_bound A (⊑) X))"
apply (rule iffI)
apply (rule theI')
using extreme_bound_unique by auto
end
sublocale semiconnex ⊆ dual: semiconnex A "(⊏)⇧-"
rewrites "sympartp (⊏)⇧- = sympartp (⊏)"
using semiconnex by auto
sublocale connex ⊆ dual: connex A "(⊑)⇧-"
rewrites "sympartp (⊑)⇧- = sympartp (⊑)"
by (auto intro!: chainI dest:comparable)
sublocale semiconnex_irreflexive ⊆ dual: semiconnex_irreflexive A "(⊏)⇧-"
rewrites "sympartp (⊏)⇧- = sympartp (⊏)"
by unfold_locales auto
sublocale pseudo_ordered_set ⊆ dual: pseudo_ordered_set A "(⊑)⇧-"
rewrites "sympartp (⊑)⇧- = sympartp (⊑)"
by unfold_locales (auto 0 4)
sublocale quasi_ordered_set ⊆ dual: quasi_ordered_set A "(⊑)⇧-"
rewrites "sympartp (⊑)⇧- = sympartp (⊑)"
by unfold_locales auto
sublocale partially_ordered_set ⊆ dual: partially_ordered_set A "(⊑)⇧-"
rewrites "sympartp (⊑)⇧- = sympartp (⊑)"
by unfold_locales (auto 0 4)
sublocale total_pseudo_ordered_set ⊆ dual: total_pseudo_ordered_set A "(⊑)⇧-"
rewrites "sympartp (⊑)⇧- = sympartp (⊑)"
by unfold_locales (auto 0 4)
sublocale total_quasi_ordered_set ⊆ dual: total_quasi_ordered_set A "(⊑)⇧-"
rewrites "sympartp (⊑)⇧- = sympartp (⊑)"
by unfold_locales auto
sublocale compatible_ordering ⊆ dual: compatible_ordering A "(⊑)⇧-" "(⊏)⇧-"
rewrites "sympartp (⊑)⇧- = sympartp (⊑)"
apply unfold_locales
by (auto dest: strict_implies_weak strict_weak_trans weak_strict_trans)
lemmas(in qorder) [intro!] = order.dual.quasi_ordered_subset
sublocale reflexive_ordering ⊆ dual: reflexive_ordering A "(⊑)⇧-" "(⊏)⇧-"
rewrites "sympartp (⊑)⇧- = sympartp (⊑)"
by unfold_locales auto
sublocale reflexive_attractive_ordering ⊆ dual: reflexive_attractive_ordering A "(⊑)⇧-" "(⊏)⇧-"
rewrites "sympartp (⊑)⇧- = sympartp (⊑)"
by unfold_locales auto
sublocale pseudo_ordering ⊆ dual: pseudo_ordering A "(⊑)⇧-" "(⊏)⇧-"
rewrites "sympartp (⊑)⇧- = sympartp (⊑)"
by unfold_locales auto
sublocale quasi_ordering ⊆ dual: quasi_ordering A "(⊑)⇧-" "(⊏)⇧-"
rewrites "sympartp (⊑)⇧- = sympartp (⊑)"
by unfold_locales auto
sublocale partial_ordering ⊆ dual: partial_ordering A "(⊑)⇧-" "(⊏)⇧-"
rewrites "sympartp (⊑)⇧- = sympartp (⊑)"
by unfold_locales auto
sublocale total_quasi_ordering ⊆ dual: total_quasi_ordering A "(⊑)⇧-" "(⊏)⇧-"
rewrites "sympartp (⊑)⇧- = sympartp (⊑)"
by unfold_locales auto
sublocale total_ordering ⊆ dual: total_ordering A "(⊑)⇧-" "(⊏)⇧-"
rewrites "sympartp (⊑)⇧- = sympartp (⊑)"
by unfold_locales auto
sublocale strict_quasi_ordering ⊆ dual: strict_quasi_ordering A "(⊑)⇧-" "(⊏)⇧-"
rewrites "sympartp (⊑)⇧- = sympartp (⊑)"
by unfold_locales (auto simp: strict_iff)
sublocale strict_partial_ordering ⊆ dual: strict_partial_ordering A "(⊑)⇧-" "(⊏)⇧-"
rewrites "sympartp (⊑)⇧- = sympartp (⊑)"
by unfold_locales auto
sublocale total_ordering ⊆ dual: total_ordering A "(⊑)⇧-" "(⊏)⇧-"
rewrites "sympartp (⊑)⇧- = sympartp (⊑)"
by unfold_locales auto
lemma(in antisymmetric) monotone_extreme_imp_extreme_bound_iff:
fixes ir (infix "≼" 50)
assumes "f ` C ⊆ A" and "monotone_on C (≼) (⊑) f" and i: "extreme C (≼) i"
shows "extreme_bound A (⊑) (f ` C) x ⟷ f i = x"
using dual.extreme_unique monotone_extreme_extreme_boundI[OF assms]
by (auto simp: extreme_bound_def)
subsection ‹Instantiations›
text ‹Finally, we instantiate our classes for sanity check.›
instance nat :: linorder ..
text ‹Pointwise ordering of functions are compatible only if the weak part is transitive.›
instance "fun" :: (type,qorder) reflorder
proof (intro_classes, unfold_locales)
note [simp] = le_fun_def less_fun_def
fix f g h :: "'a ⇒ 'b"
{ assume fg: "f ≤ g" and gh: "g < h"
show "f < h"
proof (unfold less_fun_def, intro conjI le_funI notI)
from fg have "f x ≤ g x" for x by auto
also from gh have "g x ≤ h x" for x by auto
finally (order.trans) show "f x ≤ h x" for x.
assume hf: "h ≤ f"
then have "h x ≤ f x" for x by auto
also from fg have "f x ≤ g x" for x by auto
finally have "h ≤ g" by auto
with gh show False by auto
qed
}
{ assume fg: "f < g" and gh: "g ≤ h"
show "f < h"
proof (unfold less_fun_def, intro conjI le_funI notI)
from fg have "f x ≤ g x" for x by auto
also from gh have "g x ≤ h x" for x by auto
finally show "f x ≤ h x" for x.
from gh have "g x ≤ h x" for x by auto
also assume hf: "h ≤ f"
then have "h x ≤ f x" for x by auto
finally have "g ≤ f" by auto
with fg show False by auto
qed
}
show "f < g ⟹ f ≤ g" by auto
show "¬f < f" by auto
show "f ≤ f" by auto
qed
instance "fun" :: (type,qorder) qorder
apply intro_classes
apply unfold_locales
by (auto simp: le_fun_def dest: order.trans)
instance "fun" :: (type,porder) porder
apply intro_classes
apply unfold_locales
proof (intro ext)
fix f g :: "'a ⇒ 'b" and x :: 'a
assume fg: "f ≤ g" and gf: "g ≤ f"
then have "f x ≤ g x" and "g x ≤ f x" by (auto elim: le_funE)
from order.antisym[OF this] show "f x = g x" by auto
qed
end