# Theory CZH_Sets_FBRelations

```(* Copyright 2021 (C) Mihails Milehins *)

section‹Binary relation as a finite sequence›
theory CZH_Sets_FBRelations
imports CZH_Sets_FSequences
begin

subsection‹Background›

text‹
This section exposes the theory of binary relations that are represented by
a two element finite sequence ‹[a, b]⇩∘› (as opposed to a pair ‹⟨a, b⟩›).
Many results were adapted from the theory ‹CZH_Sets_BRelations›.

As previously, many of the results that are presented in this
section can be assumed to have been adapted (with amendments) from the
theory \<^text>‹Relation› in the main library.
›

lemma fpair_iff[simp]: "([a, b]⇩∘ = [a', b']⇩∘) = (a = a' ∧ b = b')" by simp

lemmas fpair_inject[elim!] = fpair_iff[THEN iffD1, THEN conjE]

subsection‹‹fpairs››

definition fpairs :: "V ⇒ V" where
"fpairs r = set {x. x ∈⇩∘ r ∧ (∃a b. x = [a, b]⇩∘)}"

lemma small_fpairs[simp]: "small {x. x ∈⇩∘ r ∧ (∃a b. x = [a, b]⇩∘)}"
by (rule down[of _ r]) clarsimp

text‹Rules.›

lemma fpairsI[intro]:
assumes "x ∈⇩∘ r" and "x = [a, b]⇩∘"
shows "x ∈⇩∘ fpairs r"
using assms unfolding fpairs_def by auto

lemma fpairsD[dest]:
assumes "x ∈⇩∘ fpairs r"
shows "x ∈⇩∘ r" and "∃a b. x = [a, b]⇩∘"
using assms unfolding fpairs_def by auto

lemma fpairsE[elim]:
assumes "x ∈⇩∘ fpairs r"
obtains a b where "x = [a, b]⇩∘" and "[a, b]⇩∘ ∈⇩∘ r"
using assms unfolding fpairs_def by auto

lemma fpairs_iff: "x ∈⇩∘ fpairs r ⟷ x ∈⇩∘ r ∧ (∃a b. x = [a, b]⇩∘)" by auto

text‹Elementary properties.›

lemma fpairs_iff_elts: "[a, b]⇩∘ ∈⇩∘ fpairs r ⟷ [a, b]⇩∘ ∈⇩∘ r" by auto

text‹Set operations.›

lemma fpairs_vempty[simp]: "fpairs 0 = 0" by auto

lemma fpairs_vsingleton[simp]: "fpairs (set {[a, b]⇩∘}) = set {[a, b]⇩∘}" by auto

lemma fpairs_vinsert: "fpairs (vinsert [a, b]⇩∘ A) = set {[a, b]⇩∘} ∪⇩∘ fpairs A"
by auto

lemma fpairs_mono:
assumes "r ⊆⇩∘ s"
shows "fpairs r ⊆⇩∘ fpairs s"
using assms by blast

lemma fpairs_vunion: "fpairs (A ∪⇩∘ B) = fpairs A ∪⇩∘ fpairs B" by auto

lemma fpairs_vintersection: "fpairs (A ∩⇩∘ B) = fpairs A ∩⇩∘ fpairs B" by auto

lemma fpairs_vdiff: "fpairs (A -⇩∘ B) = fpairs A -⇩∘ fpairs B" by auto

text‹Special properties.›

lemma fpairs_ex_vfst:
assumes "x ∈⇩∘ fpairs r"
shows "∃b. [x⦇0⇩ℕ⦈, b]⇩∘ ∈⇩∘ r"
proof-
from assms have xr: "x ∈⇩∘ r" by auto
moreover from assms obtain b where x_def: "x = [x⦇0⇩ℕ⦈, b]⇩∘" by auto
ultimately have "[x⦇0⇩ℕ⦈, b]⇩∘ ∈⇩∘ r" by auto
then show ?thesis by auto
qed

lemma fpairs_ex_vsnd:
assumes "x ∈⇩∘ fpairs r"
shows "∃a. [a, x⦇1⇩ℕ⦈]⇩∘ ∈⇩∘ r"
proof-
from assms have xr: "x ∈⇩∘ r" by auto
moreover from assms obtain a where x_def: "x = [a, x⦇1⇩ℕ⦈]⇩∘"
by (auto simp: nat_omega_simps)
ultimately have "[a, x⦇1⇩ℕ⦈]⇩∘ ∈⇩∘ r" by auto
then show ?thesis by auto
qed

lemma fpair_vcpower2I[intro]:
assumes "a ∈⇩∘ A ^⇩× 1⇩ℕ" and "b ∈⇩∘ A ^⇩× 1⇩ℕ"
shows "vconcat [a, b]⇩∘ ∈⇩∘ A ^⇩× 2⇩ℕ"
proof-
from assms obtain a' b'
where a_def: "a = [a']⇩∘" and b_def: "b = [b']⇩∘" and "a'∈⇩∘ A" and "b'∈⇩∘ A"
by (force elim: vcons_vcpower1E)
then show ?thesis by (auto simp: nat_omega_simps)
qed

subsection‹Constructors›

subsubsection‹Identity relation›

definition fid_on :: "V ⇒ V"
where "fid_on A = set {[a, a]⇩∘ | a. a ∈⇩∘ A}"

lemma fid_on_small[simp]: "small {[a, a]⇩∘ | a. a ∈⇩∘ A}"
proof(rule down[of _ ‹A ^⇩× (2⇩ℕ)›], intro subsetI)
fix x assume "x ∈ {[a, a]⇩∘ |a. a ∈⇩∘ A}"
then obtain a where x_def: "x = [a, a]⇩∘" and "a ∈⇩∘ A" by clarsimp
interpret vfsequence ‹[a, a]⇩∘› by simp
have vcard_aa: "2⇩ℕ = vcard [a, a]⇩∘" by (simp add: nat_omega_simps)
from ‹a ∈⇩∘ A› show "x ∈⇩∘ A ^⇩× 2⇩ℕ"
unfolding x_def vcard_aa by (intro vfsequence_vrange_vcpower) auto
qed

text‹Rules.›

lemma fid_on_eqI:
assumes "a = b" and "a ∈⇩∘ A"
shows "[a, b]⇩∘ ∈⇩∘ fid_on A"
using assms by (simp add: fid_on_def)

lemma fid_onI[intro!]:
assumes "a ∈⇩∘ A"
shows "[a, a]⇩∘ ∈⇩∘ fid_on A"
by (rule fid_on_eqI) (simp_all add: assms)

lemma fid_onD[dest!]:
assumes "[a, a]⇩∘ ∈⇩∘ fid_on A"
shows "a ∈⇩∘ A"
using assms unfolding fid_on_def by auto

lemma fid_onE[elim!]:
assumes "x ∈⇩∘ fid_on A" and "∃a∈⇩∘A. x = [a, a]⇩∘ ⟹ P"
shows P
using assms unfolding fid_on_def by auto

lemma fid_on_iff: "[a, b]⇩∘ ∈⇩∘ fid_on A ⟷ a = b ∧ a ∈⇩∘ A" by auto

text‹Set operations.›

lemma fid_on_vempty[simp]: "fid_on 0 = 0" by auto

lemma fid_on_vsingleton[simp]: "fid_on (set {a}) = set {[a, a]⇩∘}" by auto

lemma fid_on_vdoubleton: "fid_on (set {a, b}) = set {[a, a]⇩∘, [b, b]⇩∘}" by force

lemma fid_on_mono:
assumes "A ⊆⇩∘ B"
shows "fid_on A ⊆⇩∘ fid_on B"
using assms by auto

lemma fid_on_vinsert: "vinsert [a, a]⇩∘ (fid_on A) = fid_on (vinsert a A)"
by auto

lemma fid_on_vintersection: "fid_on (A ∩⇩∘ B) = fid_on A ∩⇩∘ fid_on B" by auto

lemma fid_on_vunion: "fid_on (A ∪⇩∘ B) = fid_on A ∪⇩∘ fid_on B" by auto

lemma fid_on_vdiff: "fid_on (A -⇩∘ B) = fid_on A -⇩∘ fid_on B" by auto

text‹Special properties.›

lemma fid_on_vsubset_vcpower: "fid_on A ⊆⇩∘ A ^⇩× 2⇩ℕ" by force

subsubsection‹Constant function›

definition fconst_on :: "V ⇒ V ⇒ V"
where "fconst_on A c = set {[a, c]⇩∘ | a. a ∈⇩∘ A}"

lemma small_fconst_on[simp]: "small {[a, c]⇩∘ | a. a ∈⇩∘ A}"
by (rule down[of _ ‹A ×⇩∙ set {c}›]) blast

text‹Rules.›

lemma fconst_onI[intro!]:
assumes "a ∈⇩∘ A"
shows "[a, c]⇩∘ ∈⇩∘ fconst_on A c"
using assms unfolding fconst_on_def by simp

lemma fconst_onD[dest!]:
assumes "[a, c]⇩∘ ∈⇩∘ fconst_on A c"
shows "a ∈⇩∘ A"
using assms unfolding fconst_on_def by simp

lemma fconst_onE[elim!]:
assumes "x ∈⇩∘ fconst_on A c"
obtains a where "a ∈⇩∘ A" and "x = [a, c]⇩∘"
using assms unfolding fconst_on_def by auto

lemma fconst_on_iff: "[a, c]⇩∘ ∈⇩∘ fconst_on A c ⟷ a ∈⇩∘ A" by auto

text‹Set operations.›

lemma fconst_on_vempty[simp]: "fconst_on 0 c = 0"
unfolding fconst_on_def by auto

lemma fconst_on_vsingleton[simp]: "fconst_on (set {a}) c = set {[a, c]⇩∘}"
by auto

lemma fconst_on_vdoubleton: "fconst_on (set {a, b}) c = set {[a, c]⇩∘, [b, c]⇩∘}"
by force

lemma fconst_on_mono:
assumes "A ⊆⇩∘ B"
shows "fconst_on A c ⊆⇩∘ fconst_on B c"
using assms by auto

lemma fconst_on_vinsert:
"(vinsert [a, c]⇩∘ (fconst_on A c)) = (fconst_on (vinsert a A) c)"
by auto

lemma fconst_on_vintersection:
"fconst_on (A ∩⇩∘ B) c = fconst_on A c ∩⇩∘ fconst_on B c"
by auto

lemma fconst_on_vunion: "fconst_on (A ∪⇩∘ B) c = fconst_on A c ∪⇩∘ fconst_on B c"
by auto

lemma fconst_on_vdiff: "fconst_on (A -⇩∘ B) c = fconst_on A c -⇩∘ fconst_on B c"
by auto

text‹Special properties.›

lemma fconst_on_eq_ftimes: "fconst_on A c = A ×⇩∙ set {c}" by blast

subsubsection‹Composition›

definition fcomp :: "V ⇒ V ⇒ V" (infixr ‹∘⇩∙› 75)
where "r ∘⇩∙ s = set {[a, c]⇩∘ | a c. ∃b. [a, b]⇩∘ ∈⇩∘ s ∧ [b, c]⇩∘ ∈⇩∘ r}"
notation fcomp (infixr "∘⇩∙" 75)

lemma fcomp_small[simp]: "small {[a, c]⇩∘ | a c. ∃b. [a, b]⇩∘ ∈⇩∘ s ∧ [b, c]⇩∘ ∈⇩∘ r}"
(is ‹small ?s›)
proof-
define comp' where "comp' = (λ⟨ab, cd⟩. [ab⦇0⇩ℕ⦈, cd⦇1⇩ℕ⦈]⇩∘)"
have "small (elts (vpairs (s ×⇩∘ r)))" by simp
then have small_comp: "small (comp' ` elts (vpairs (s ×⇩∘ r)))" by simp
have ss: "?s ⊆ (comp' ` elts (vpairs (s ×⇩∘ r)))"
proof
fix x assume "x ∈ ?s"
then obtain a b c where x_def: "x = [a, c]⇩∘"
and "[a, b]⇩∘ ∈⇩∘ s"
and "[b, c]⇩∘ ∈⇩∘ r"
by auto
then have abbc: "⟨[a, b]⇩∘, [b, c]⇩∘⟩ ∈⇩∘ vpairs (s ×⇩∘ r)"
have x_def': "x = comp' ⟨[a, b]⇩∘, [b, c]⇩∘⟩"
unfolding comp'_def x_def by (auto simp: nat_omega_simps)
then show "x ∈ comp' ` elts (vpairs (s ×⇩∘ r))"
unfolding x_def' using abbc by auto
qed
with small_comp show ?thesis by (meson smaller_than_small)
qed

text‹Rules.›

lemma fcompI[intro]:
assumes "[b, c]⇩∘ ∈⇩∘ r" and "[a, b]⇩∘ ∈⇩∘ s"
shows "[a, c]⇩∘ ∈⇩∘ r ∘⇩∙ s"
using assms unfolding fcomp_def by auto

lemma fcompD[dest]:
assumes "[a, c]⇩∘ ∈⇩∘ r ∘⇩∙ s"
shows "∃b. [b, c]⇩∘ ∈⇩∘ r ∧ [a, b]⇩∘ ∈⇩∘ s"
using assms unfolding fcomp_def by auto

lemma fcompE[elim]:
assumes "ac ∈⇩∘ r ∘⇩∙ s"
obtains a b c where "ac = [a, c]⇩∘" and "[a, b]⇩∘ ∈⇩∘ s" and "[b, c]⇩∘ ∈⇩∘ r"
using assms unfolding fcomp_def by clarsimp

text‹Elementary properties.›

lemma fcomp_assoc: "(r ∘⇩∙ s) ∘⇩∙ t = r ∘⇩∙ (s ∘⇩∙ t)" by fast

text‹Set operations.›

lemma fcomp_vempty_left[simp]: "0 ∘⇩∙ r = 0" unfolding vcomp_def by force

lemma fcomp_vempty_right[simp]: "r ∘⇩∙ 0 = 0" unfolding vcomp_def by force

lemma fcomp_mono:
assumes "r' ⊆⇩∘ r" and "s' ⊆⇩∘ s"
shows "r' ∘⇩∙ s' ⊆⇩∘ r ∘⇩∙ s"
using assms by force

lemma fcomp_vinsert_left[simp]:
"vinsert ([a, b]⇩∘) s ∘⇩∙ r = (set {[a, b]⇩∘} ∘⇩∙ r) ∪⇩∘ (s ∘⇩∙ r)"
by auto

lemma fcomp_vinsert_right[simp]:
"r ∘⇩∙ vinsert [a, b]⇩∘ s = (r ∘⇩∙ set {[a, b]⇩∘}) ∪⇩∘ (r ∘⇩∙ s)"
by auto

lemma fcomp_vunion_left[simp]: "(s ∪⇩∘ t) ∘⇩∙ r = (s ∘⇩∙ r) ∪⇩∘ (t ∘⇩∙ r)" by auto

lemma fcomp_vunion_right[simp]: "r ∘⇩∙ (s ∪⇩∘ t) = (r ∘⇩∙ s) ∪⇩∘ (r ∘⇩∙ t)" by auto

text‹Connections.›

lemma fcomp_fid_on_idem[simp]: "fid_on A ∘⇩∙ fid_on A = fid_on A" by force

lemma fcomp_fid_on[simp]: "fid_on A ∘⇩∙ fid_on B = fid_on (A ∩⇩∘ B)" by force

lemma fcomp_fconst_on_fid_on[simp]: "fconst_on A c ∘⇩∙ fid_on A = fconst_on A c"
by auto

text‹Special properties.›

lemma fcomp_vsubset_vtimes:
assumes "r ⊆⇩∘ B ×⇩∙ C" and "s ⊆⇩∘ A ×⇩∙ B"
shows "r ∘⇩∙ s ⊆⇩∘ A ×⇩∙ C"
using assms by blast

lemma fcomp_obtain_middle[elim]:
assumes "[a, c]⇩∘ ∈⇩∘ f ∘⇩∙ g"
obtains b where "[a, b]⇩∘ ∈⇩∘ g" and "[b, c]⇩∘ ∈⇩∘ f"
using assms by auto

subsubsection‹Converse relation›

definition fconverse :: "V ⇒ V" (‹(_¯⇩∙)› [1000] 999)
where "r¯⇩∙ = set {[b, a]⇩∘ | a b. [a, b]⇩∘ ∈⇩∘ r}"

lemma fconverse_small[simp]: "small {[b, a]⇩∘ | a b. [a, b]⇩∘ ∈⇩∘ r}"
proof-
have eq:
"{[b, a]⇩∘ | a b. [a, b]⇩∘ ∈⇩∘ r} = (λx. [x⦇1⇩ℕ⦈, x⦇0⇩ℕ⦈]⇩∘) ` elts (fpairs r)"
proof(rule subset_antisym; rule subsetI, unfold mem_Collect_eq)
fix x assume "x ∈ (λx. [x⦇1⇩ℕ⦈, x⦇0⇩ℕ⦈]⇩∘) ` elts (fpairs r)"
then obtain a b where "[a, b]⇩∘ ∈⇩∘ fpairs r"
and "x = (λx. [x⦇1⇩ℕ⦈, x⦇0⇩ℕ⦈]⇩∘) [a, b]⇩∘"
by blast
then show "∃a b. x = [b, a]⇩∘ ∧ [a, b]⇩∘ ∈⇩∘ r" by (auto simp: nat_omega_simps)
qed (use image_iff fpairs_iff_elts in ‹fastforce simp: nat_omega_simps›)
show ?thesis unfolding eq by (rule replacement) auto
qed

text‹Rules.›

lemma fconverseI[sym, intro!]:
assumes "[a, b]⇩∘ ∈⇩∘ r"
shows "[b, a]⇩∘ ∈⇩∘ r¯⇩∙"
using assms unfolding fconverse_def by simp

lemma fconverseD[sym, dest]:
assumes "[a, b]⇩∘ ∈⇩∘ r¯⇩∙"
shows "[b, a]⇩∘ ∈⇩∘ r"
using assms unfolding fconverse_def by simp

lemma fconverseE[elim!]:
assumes "x ∈⇩∘ r¯⇩∙"
obtains a b where "x = [b, a]⇩∘" and "[a, b]⇩∘ ∈⇩∘ r"
using assms unfolding fconverse_def by auto

lemma fconverse_iff: "[b, a]⇩∘ ∈⇩∘ r¯⇩∙ ⟷ [a, b]⇩∘ ∈⇩∘ r" by auto

text‹Set operations.›

lemma fconverse_vempty[simp]: "0¯⇩∙ = 0" by auto

lemma fconverse_vsingleton: "(set {[a, b]⇩∘})¯⇩∙ = set {[b, a]⇩∘}" by auto

lemma fconverse_vdoubleton: "(set {[a, b]⇩∘, [c, d]⇩∘})¯⇩∙ = set {[b, a]⇩∘, [d, c]⇩∘}"
by force

lemma fconverse_vinsert: "(vinsert [a, b]⇩∘ r)¯⇩∙ = vinsert [b, a]⇩∘ (r¯⇩∙)" by auto

lemma fconverse_vintersection: "(r ∩⇩∘ s)¯⇩∙ = r¯⇩∙ ∩⇩∘ s¯⇩∙" by auto

lemma fconverse_vunion: "(r ∪⇩∘ s)¯⇩∙ = r¯⇩∙ ∪⇩∘ s¯⇩∙" by auto

text‹Connections.›

lemma fconverse_fid_on[simp]: "(fid_on A)¯⇩∙ = fid_on A" by auto

lemma fconverse_fconst_on[simp]: "(fconst_on A c)¯⇩∙ = set {c} ×⇩∙ A" by blast

lemma fconverse_fcomp: "(r ∘⇩∙ s)¯⇩∙ = s¯⇩∙ ∘⇩∙ r¯⇩∙" by auto

lemma fconverse_ftimes: "(A ×⇩∙ B)¯⇩∙ = (B ×⇩∙ A)" by auto

text‹Special properties.›

lemma fconverse_pred:
assumes "small {[a, b]⇩∘ | a b. P a b}"
shows "(set {[a, b]⇩∘ | a b. P a b})¯⇩∙ = set {[b, a]⇩∘ | a b. P a b}"
using assms unfolding fconverse_def by simp

subsubsection‹Left restriction›

definition flrestriction :: "V ⇒ V ⇒ V" (infixr ‹↾⇧l⇩∙› 80)
where "r ↾⇧l⇩∙ A = set {[a, b]⇩∘ | a b. a ∈⇩∘ A ∧ [a, b]⇩∘ ∈⇩∘ r}"

lemma flrestriction_small[simp]: "small {[a, b]⇩∘ | a b. a ∈⇩∘ A ∧ [a, b]⇩∘ ∈⇩∘ r}"
by (rule down[of _ r]) auto

text‹Rules.›

lemma flrestrictionI[intro!]:
assumes "a ∈⇩∘ A" and "[a, b]⇩∘ ∈⇩∘ r"
shows "[a, b]⇩∘ ∈⇩∘ r ↾⇧l⇩∙ A"
using assms unfolding flrestriction_def by simp

lemma flrestrictionD[dest]:
assumes "[a, b]⇩∘ ∈⇩∘ r ↾⇧l⇩∙ A"
shows "a ∈⇩∘ A" and "[a, b]⇩∘ ∈⇩∘ r"
using assms unfolding flrestriction_def by auto

lemma flrestrictionE[elim!]:
assumes "x ∈⇩∘ r ↾⇧l⇩∙ A"
obtains a b where "x = [a, b]⇩∘" and "a ∈⇩∘ A" and "[a, b]⇩∘ ∈⇩∘ r"
using assms unfolding flrestriction_def by auto

text‹Set operations.›

lemma flrestriction_on_vempty[simp]: "r ↾⇧l⇩∙ 0 = 0" by auto

lemma flrestriction_vempty[simp]: "0 ↾⇧l⇩∙ A = 0" by auto

lemma flrestriction_vsingleton_in[simp]:
assumes "a ∈⇩∘ A"
shows "set {[a, b]⇩∘} ↾⇧l⇩∙ A = set {[a, b]⇩∘}"
using assms by auto

lemma flrestriction_vsingleton_nin[simp]:
assumes "a ∉⇩∘ A"
shows "set {[a, b]⇩∘} ↾⇧l⇩∙ A = 0"
using assms by auto

lemma flrestriction_mono:
assumes "A ⊆⇩∘ B"
shows "r ↾⇧l⇩∙ A ⊆⇩∘ r ↾⇧l⇩∙ B"
using assms by auto

lemma flrestriction_vinsert_nin[simp]:
assumes "a ∉⇩∘ A"
shows "(vinsert [a, b]⇩∘ r) ↾⇧l⇩∙ A = r ↾⇧l⇩∙ A"
using assms by auto

lemma flrestriction_vinsert_in:
assumes "a ∈⇩∘ A"
shows "(vinsert [a, b]⇩∘ r) ↾⇧l⇩∙ A = vinsert [a, b]⇩∘ (r ↾⇧l⇩∙ A)"
using assms by auto

lemma flrestriction_vintersection: "(r ∩⇩∘ s) ↾⇧l⇩∙ A = r ↾⇧l⇩∙ A ∩⇩∘ s ↾⇧l⇩∙ A" by auto

lemma flrestriction_vunion: "(r ∪⇩∘ s) ↾⇧l⇩∙ A = r ↾⇧l⇩∙ A ∪⇩∘ s ↾⇧l⇩∙ A" by auto

lemma flrestriction_vdiff: "(r -⇩∘ s) ↾⇧l⇩∙ A = r ↾⇧l⇩∙ A -⇩∘ s ↾⇧l⇩∙ A" by auto

text‹Connections.›

lemma flrestriction_fid_on[simp]: "(fid_on A) ↾⇧l⇩∙ B = fid_on (A ∩⇩∘ B)" by auto

lemma flrestriction_fconst_on: "(fconst_on A c) ↾⇧l⇩∙ B = (fconst_on B c) ↾⇧l⇩∙ A"
by auto

lemma flrestriction_fconst_on_commute:
assumes "x ∈⇩∘ fconst_on A c ↾⇧l⇩∙ B"
shows "x ∈⇩∘ fconst_on B c ↾⇧l⇩∙ A"
using assms by auto

lemma flrestriction_fcomp[simp]: "(r ∘⇩∙ s) ↾⇧l⇩∙ A = r ∘⇩∙ (s ↾⇧l⇩∙ A)" by auto

text‹Previous connections.›

lemma fcomp_rel_fid_on[simp]: "r ∘⇩∙ fid_on A = r ↾⇧l⇩∙ A" by auto

lemma fcomp_fconst_on:
"r ∘⇩∙ (fconst_on A c) = (r ↾⇧l⇩∙ set {c}) ∘⇩∙ (fconst_on A c)"
by auto

text‹Special properties.›

lemma flrestriction_vsubset_fpairs: "r ↾⇧l⇩∙ A ⊆⇩∘ fpairs r"
by (rule vsubsetI) (metis fpairs_iff_elts flrestrictionE)

lemma flrestriction_vsubset_frel: "r ↾⇧l⇩∙ A ⊆⇩∘ r" by auto

subsubsection‹Right restriction›

definition frrestriction :: "V ⇒ V ⇒ V" (infixr ‹↾⇧r⇩∙› 80)
where "r ↾⇧r⇩∙ A = set {[a, b]⇩∘ | a b. b ∈⇩∘ A ∧ [a, b]⇩∘ ∈⇩∘ r}"

lemma frrestriction_small[simp]: "small {[a, b]⇩∘ | a b. b ∈⇩∘ A ∧ [a, b]⇩∘ ∈⇩∘ r}"
by (rule down[of _ r]) auto

text‹Rules.›

lemma frrestrictionI[intro!]:
assumes "b ∈⇩∘ A" and "[a, b]⇩∘ ∈⇩∘ r"
shows "[a, b]⇩∘ ∈⇩∘ r ↾⇧r⇩∙ A"
using assms unfolding frrestriction_def by simp

lemma frrestrictionD[dest]:
assumes "[a, b]⇩∘ ∈⇩∘ r ↾⇧r⇩∙ A"
shows "b ∈⇩∘ A" and "[a, b]⇩∘ ∈⇩∘ r"
using assms unfolding frrestriction_def by auto

lemma frrestrictionE[elim!]:
assumes "x ∈⇩∘ r ↾⇧r⇩∙ A"
obtains a b where "x = [a, b]⇩∘" and "b ∈⇩∘ A" and "[a, b]⇩∘ ∈⇩∘ r"
using assms unfolding frrestriction_def by auto

text‹Set operations.›

lemma frrestriction_on_vempty[simp]: "r ↾⇧r⇩∙ 0 = 0" by auto

lemma frrestriction_vempty[simp]: "0 ↾⇧r⇩∙ A = 0" by auto

lemma frrestriction_vsingleton_in[simp]:
assumes "b ∈⇩∘ A"
shows "set {[a, b]⇩∘} ↾⇧r⇩∙ A = set {[a, b]⇩∘}"
using assms by auto

lemma frrestriction_vsingleton_nin[simp]:
assumes "b ∉⇩∘ A"
shows "set {[a, b]⇩∘} ↾⇧r⇩∙ A = 0"
using assms by auto

lemma frrestriction_mono:
assumes "A ⊆⇩∘ B"
shows "r ↾⇧r⇩∙ A ⊆⇩∘ r ↾⇧r⇩∙ B"
using assms by auto

lemma frrestriction_vinsert_nin[simp]:
assumes "b ∉⇩∘ A"
shows "(vinsert [a, b]⇩∘ r) ↾⇧r⇩∙ A = r ↾⇧r⇩∙ A"
using assms by auto

lemma frrestriction_vinsert_in:
assumes "b ∈⇩∘ A"
shows "(vinsert [a, b]⇩∘ r) ↾⇧r⇩∙ A = vinsert [a, b]⇩∘ (r ↾⇧r⇩∙ A)"
using assms by auto

lemma frrestriction_vintersection: "(r ∩⇩∘ s) ↾⇧r⇩∙ A = r ↾⇧r⇩∙ A ∩⇩∘ s ↾⇧r⇩∙ A" by auto

lemma frrestriction_vunion: "(r ∪⇩∘ s) ↾⇧r⇩∙ A = r ↾⇧r⇩∙ A ∪⇩∘ s ↾⇧r⇩∙ A" by auto

lemma frrestriction_vdiff: "(r -⇩∘ s) ↾⇧r⇩∙ A = r ↾⇧r⇩∙ A -⇩∘ s ↾⇧r⇩∙ A" by auto

text‹Connections.›

lemma frrestriction_fid_on[simp]: "(fid_on A) ↾⇧r⇩∙ B = fid_on (A ∩⇩∘ B)" by auto

lemma frrestriction_fconst_on:
assumes "c ∈⇩∘ B"
shows "(fconst_on A c) ↾⇧r⇩∙ B = fconst_on A c"
using assms by auto

lemma frrestriction_fcomp[simp]: "(r ∘⇩∙ s) ↾⇧r⇩∙ A = (r ↾⇧r⇩∙ A) ∘⇩∙ s" by auto

text‹Previous connections.›

lemma fcomp_fid_on_rel[simp]: "fid_on A ∘⇩∙ r = r ↾⇧r⇩∙ A" by force

lemma fcomp_fconst_on_rel: "(fconst_on A c) ∘⇩∙ r = (fconst_on A c) ∘⇩∙ (r ↾⇧r⇩∙ A)"
by auto

lemma flrestriction_fconverse: "r¯⇩∙ ↾⇧l⇩∙ A = (r ↾⇧r⇩∙ A)¯⇩∙" by auto

lemma frrestriction_fconverse: "r¯⇩∙ ↾⇧r⇩∙ A = (r ↾⇧l⇩∙ A)¯⇩∙" by auto

text‹Special properties.›

lemma frrestriction_vsubset_rel: "r ↾⇧r⇩∙ A ⊆⇩∘ r" by auto

lemma frrestriction_vsubset_vpairs: "r ↾⇧r⇩∙ A ⊆⇩∘ fpairs r" by auto

subsubsection‹Restriction›

definition frestriction :: "V ⇒ V ⇒ V" (infixr ‹↾⇩∙› 80)
where "r ↾⇩∙ A = set {[a, b]⇩∘ | a b. a ∈⇩∘ A ∧ b ∈⇩∘ A ∧ [a, b]⇩∘ ∈⇩∘ r}"

lemma frestriction_small[simp]:
"small {[a, b]⇩∘ | a b. a ∈⇩∘ A ∧ b ∈⇩∘ A ∧ [a, b]⇩∘ ∈⇩∘ r}"
by (rule down[of _ r]) auto

text‹Rules.›

lemma frestrictionI[intro!]:
assumes "a ∈⇩∘ A" and "b ∈⇩∘ A" and "[a, b]⇩∘ ∈⇩∘ r"
shows "[a, b]⇩∘ ∈⇩∘ r ↾⇩∙ A"
using assms unfolding frestriction_def by simp

lemma frestrictionD[dest]:
assumes "[a, b]⇩∘ ∈⇩∘ r ↾⇩∙ A"
shows "a ∈⇩∘ A" and "b ∈⇩∘ A" and "[a, b]⇩∘ ∈⇩∘ r"
using assms unfolding frestriction_def by auto

lemma frestrictionE[elim!]:
assumes "x ∈⇩∘ r ↾⇩∙ A"
obtains a b where "x = [a, b]⇩∘" and "a ∈⇩∘ A" and "b ∈⇩∘ A" and "[a, b]⇩∘ ∈⇩∘ r"
using assms unfolding frestriction_def by clarsimp

text‹Set operations.›

lemma frestriction_on_vempty[simp]: "r ↾⇩∙ 0 = 0" by auto

lemma frestriction_vempty[simp]: "0 ↾⇩∙ A = 0" by auto

lemma frestriction_vsingleton_in[simp]:
assumes "a ∈⇩∘ A" and "b ∈⇩∘ A"
shows "set {[a, b]⇩∘} ↾⇩∙ A = set {[a, b]⇩∘}"
using assms by auto

lemma frestriction_vsingleton_nin_left[simp]:
assumes "a ∉⇩∘ A"
shows "set {[a, b]⇩∘} ↾⇩∙ A = 0"
using assms by auto

lemma frestriction_vsingleton_nin_right[simp]:
assumes "b ∉⇩∘ A"
shows "set {[a, b]⇩∘} ↾⇩∙ A = 0"
using assms by auto

lemma frestriction_mono:
assumes "A ⊆⇩∘ B"
shows "r ↾⇩∙ A ⊆⇩∘ r ↾⇩∙ B"
using assms by auto

lemma frestriction_vinsert_nin[simp]:
assumes "a ∉⇩∘ A" and "b ∉⇩∘ A"
shows "(vinsert [a, b]⇩∘ r) ↾⇩∙ A = r ↾⇩∙ A"
using assms by auto

lemma frestriction_vinsert_in:
assumes "a ∈⇩∘ A" and "b ∈⇩∘ A"
shows "(vinsert [a, b]⇩∘ r) ↾⇩∙ A = vinsert [a, b]⇩∘ (r ↾⇩∙ A)"
using assms by auto

lemma frestriction_vintersection: "(r ∩⇩∘ s) ↾⇩∙ A = r ↾⇩∙ A ∩⇩∘ s ↾⇩∙ A" by auto

lemma frestriction_vunion: "(r ∪⇩∘ s) ↾⇩∙ A = r ↾⇩∙ A ∪⇩∘ s ↾⇩∙ A" by auto

lemma frestriction_vdiff: "(r -⇩∘ s) ↾⇩∙ A = r ↾⇩∙ A -⇩∘ s ↾⇩∙ A" by auto

text‹Connections.›

lemma fid_on_frestriction[simp]: "(fid_on A) ↾⇩∙ B = fid_on (A ∩⇩∘ B)" by auto

lemma frestriction_fconst_on_ex:
assumes "c ∈⇩∘ B"
shows "(fconst_on A c) ↾⇩∙ B = fconst_on (A ∩⇩∘ B) c"
using assms by auto

lemma frestriction_fconst_on_nex:
assumes "c ∉⇩∘ B"
shows "(fconst_on A c) ↾⇩∙ B = 0"
using assms by auto

lemma frestriction_fcomp[simp]: "(r ∘⇩∙ s) ↾⇩∙ A = (r ↾⇧r⇩∙ A) ∘⇩∙ (s ↾⇧l⇩∙ A)" by auto

lemma frestriction_fconverse: "r¯⇩∙ ↾⇩∙ A = (r ↾⇩∙ A)¯⇩∙" by auto

text‹Previous connections.›

lemma frrestriction_flrestriction[simp]: "(r ↾⇧r⇩∙ A) ↾⇧l⇩∙ A = r ↾⇩∙ A" by auto

lemma flrestriction_frrestriction[simp]: "(r ↾⇧l⇩∙ A) ↾⇧r⇩∙ A = r ↾⇩∙ A" by auto

lemma frestriction_flrestriction[simp]: "(r ↾⇩∙ A) ↾⇧l⇩∙ A = r ↾⇩∙ A" by auto

lemma frestriction_frrestriction[simp]: "(r ↾⇩∙ A) ↾⇧r⇩∙ A = r ↾⇩∙ A" by auto

text‹Special properties.›

lemma frestriction_vsubset_fpairs: "r ↾⇩∙ A ⊆⇩∘ fpairs r" by auto

lemma frestriction_vsubset_ftimes: "r ↾⇩∙ A ⊆⇩∘ A ^⇩× 2⇩ℕ" by force

lemma frestriction_vsubset_rel: "r ↾⇩∙ A ⊆⇩∘ r" by auto

subsection‹Properties›

subsubsection‹Domain›

definition fdomain :: "V ⇒ V" (‹𝒟⇩∙›)
where "𝒟⇩∙ r = set {a. ∃b. [a, b]⇩∘ ∈⇩∘ r}"
notation fdomain (‹𝒟⇩∙›)

lemma fdomain_small[simp]: "small {a. ∃b. [a, b]⇩∘ ∈⇩∘ r}"
proof-
have ss: "{a. ∃b. [a, b]⇩∘ ∈⇩∘ r} ⊆ (λx. x⦇0⇩ℕ⦈) ` elts r"
using image_iff by force
have small: "small ((λx. x⦇0⇩ℕ⦈) ` elts r)" by (rule replacement) simp
show ?thesis by (rule smaller_than_small, rule small, rule ss)
qed

text‹Rules.›

lemma fdomainI[intro]:
assumes "[a, b]⇩∘ ∈⇩∘ r"
shows "a ∈⇩∘ 𝒟⇩∙ r"
using assms unfolding fdomain_def by auto

lemma fdomainD[dest]:
assumes "a ∈⇩∘ 𝒟⇩∙ r"
shows "∃b. [a, b]⇩∘ ∈⇩∘ r"
using assms unfolding fdomain_def by auto

lemma fdomainE[elim]:
assumes "a ∈⇩∘ 𝒟⇩∙ r"
obtains b where "[a, b]⇩∘ ∈⇩∘ r"
using assms unfolding fdomain_def by clarsimp

lemma fdomain_iff: "a ∈⇩∘ 𝒟⇩∙ r ⟷ (∃y. [a, y]⇩∘ ∈⇩∘ r)" by auto

text‹Set operations.›

lemma fdomain_vempty[simp]: "𝒟⇩∙ 0 = 0" by force

lemma fdomain_vsingleton[simp]: "𝒟⇩∙ (set {[a, b]⇩∘}) = set {a}" by auto

lemma fdomain_vdoubleton[simp]: "𝒟⇩∙ (set {[a, b]⇩∘, [c, d]⇩∘}) = set {a, c}"
by force

lemma fdomain_mono:
assumes "r ⊆⇩∘ s"
shows "𝒟⇩∙ r ⊆⇩∘ 𝒟⇩∙ s"
using assms by blast

lemma fdomain_vinsert[simp]: "𝒟⇩∙ (vinsert [a, b]⇩∘ r) = vinsert a (𝒟⇩∙ r)"
by force

lemma fdomain_vunion: "𝒟⇩∙ (A ∪⇩∘ B) = 𝒟⇩∙ A ∪⇩∘ 𝒟⇩∙ B" by force

lemma fdomain_vintersection_vsubset: "𝒟⇩∙ (A ∩⇩∘ B) ⊆⇩∘ 𝒟⇩∙ A ∩⇩∘ 𝒟⇩∙ B" by auto

lemma fdomain_vdiff_vsubset: "𝒟⇩∙ A -⇩∘ 𝒟⇩∙ B ⊆⇩∘ 𝒟⇩∙ (A -⇩∘ B)" by auto

text‹Connections.›

lemma fdomain_fid_on[simp]: "𝒟⇩∙ (fid_on A) = A" by force

lemma fdomain_fconst_on[simp]: "𝒟⇩∙ (fconst_on A c) = A" by force

lemma fdomain_flrestriction: "𝒟⇩∙ (r ↾⇧l⇩∙ A) = 𝒟⇩∙ r ∩⇩∘ A" by auto

text‹Special properties.›

lemma fdomain_vsubset_ftimes:
assumes "fpairs r ⊆⇩∘ A ×⇩∙ B"
shows "𝒟⇩∙ r ⊆⇩∘ A"
using assms by blast

lemma fdomain_vsubset_VUnion2: "𝒟⇩∙ r ⊆⇩∘ ⋃⇩∘(⋃⇩∘(⋃⇩∘r))"
proof(intro vsubsetI)
fix x assume "x ∈⇩∘ 𝒟⇩∙ r"
then obtain y where "[x, y]⇩∘ ∈⇩∘ r" by auto
then have "set {⟨0⇩ℕ, x⟩, ⟨1⇩ℕ, y⟩} ∈⇩∘ r" unfolding vcons_vdoubleton by simp
with insert_commute have "⟨0⇩ℕ, x⟩ ∈⇩∘ ⋃⇩∘r" by auto
then show "x ∈⇩∘ ⋃⇩∘(⋃⇩∘(⋃⇩∘r))"
unfolding vpair_def
by (metis (full_types) VUnion_iff insert_commute vintersection_vdoubleton)
qed

subsubsection‹Range›

definition frange :: "V ⇒ V" (‹ℛ⇩∙›)
where "frange r = set {b. ∃a. [a, b]⇩∘ ∈⇩∘ r}"
notation frange (‹ℛ⇩∙›)

lemma frange_small[simp]: "small {b. ∃a. [a, b]⇩∘ ∈⇩∘ r}"
proof-
have ss: "{b. ∃a. [a, b]⇩∘ ∈⇩∘ r} ⊆ (λx. x⦇1⇩ℕ⦈) ` elts r"
using image_iff by (fastforce simp: nat_omega_simps)
have small: "small ((λx. x⦇1⇩ℕ⦈) ` elts r)" by (rule replacement) simp
show ?thesis by (rule smaller_than_small, rule small, rule ss)
qed

text‹Rules.›

lemma frangeI[intro]:
assumes "[a, b]⇩∘ ∈⇩∘ r"
shows "b ∈⇩∘ ℛ⇩∙ r"
using assms unfolding frange_def by auto

lemma frangeD[dest]:
assumes "b ∈⇩∘ ℛ⇩∙ r"
shows "∃a. [a, b]⇩∘ ∈⇩∘ r"
using assms unfolding frange_def by simp

lemma frangeE[elim!]:
assumes "b ∈⇩∘ ℛ⇩∙ r"
obtains a where "[a, b]⇩∘ ∈⇩∘ r"
using assms unfolding frange_def by clarsimp

lemma frange_iff: "b ∈⇩∘ ℛ⇩∙ r ⟷ (∃a. [a, b]⇩∘ ∈⇩∘ r)" by auto

text‹Set operations.›

lemma frange_vempty[simp]: "ℛ⇩∙ 0 = 0" by auto

lemma frange_vsingleton[simp]: "ℛ⇩∙ (set {[a, b]⇩∘}) = set {b}" by auto

lemma frange_vdoubleton[simp]: "ℛ⇩∙ (set {[a, b]⇩∘, [c, d]⇩∘}) = set {b, d}"
by force

lemma frange_mono:
assumes "r ⊆⇩∘ s"
shows "ℛ⇩∙ r ⊆⇩∘ ℛ⇩∙ s"
using assms by force

lemma frange_vinsert[simp]: "ℛ⇩∙ (vinsert [a, b]⇩∘ r) = vinsert b (ℛ⇩∙ r)" by auto

lemma frange_vunion: "ℛ⇩∙ (r ∪⇩∘ s) = ℛ⇩∙ r ∪⇩∘ ℛ⇩∙ s" by auto

lemma frange_vintersection_vsubset: "ℛ⇩∙ (r ∩⇩∘ s) ⊆⇩∘ ℛ⇩∙ r ∩⇩∘ ℛ⇩∙ s" by auto

lemma frange_vdiff_vsubset: "ℛ⇩∙ r -⇩∘ ℛ⇩∙ s ⊆⇩∘ ℛ⇩∙ (r -⇩∘ s)" by auto

text‹Connections.›

lemma frange_fid_on[simp]: "ℛ⇩∙ (fid_on A) = A" by force

lemma frange_fconst_on_vempty[simp]: "ℛ⇩∙ (fconst_on 0 c) = 0" by auto

lemma frange_fconst_on_ne[simp]:
assumes "A ≠ 0"
shows "ℛ⇩∙ (fconst_on A c) = set {c}"
using assms by force

lemma frange_vrrestriction: "ℛ⇩∙ (r ↾⇧r⇩∙ A) = ℛ⇩∙ r ∩⇩∘ A" by auto

text‹Previous connections›

lemma fdomain_fconverse[simp]: "𝒟⇩∙ (r¯⇩∙) = ℛ⇩∙ r" by auto

lemma frange_fconverse[simp]: "ℛ⇩∙ (r¯⇩∙) = 𝒟⇩∙ r" by force

text‹Special properties.›

lemma frange_iff_vdomain: "b ∈⇩∘ ℛ⇩∙ r ⟷ (∃a∈⇩∘𝒟⇩∙ r. [a, b]⇩∘ ∈⇩∘ r)" by auto

lemma frange_vsubset_ftimes:
assumes "fpairs r ⊆⇩∘ A ×⇩∙ B"
shows "ℛ⇩∙ r ⊆⇩∘ B"
using assms by blast

lemma fpairs_vsubset_fdomain_frange[simp]: "fpairs r ⊆⇩∘ (𝒟⇩∙ r) ×⇩∙ (ℛ⇩∙ r)"
by blast

lemma frange_vsubset_VUnion2: "ℛ⇩∙ r ⊆⇩∘ ⋃⇩∘(⋃⇩∘(⋃⇩∘r))"
proof(intro vsubsetI)
fix y assume "y ∈⇩∘ ℛ⇩∙ r"
then obtain x where "[x, y]⇩∘ ∈⇩∘ r" by auto
then have "set {⟨0⇩ℕ, x⟩, ⟨1⇩ℕ, y⟩} ∈⇩∘ r" unfolding vcons_vdoubleton by simp
with insert_commute have "⟨1⇩ℕ, y⟩ ∈⇩∘ ⋃⇩∘r" by auto
then show "y ∈⇩∘ ⋃⇩∘(⋃⇩∘(⋃⇩∘r))"
unfolding vpair_def
by (metis (full_types) VUnion_iff insert_commute vintersection_vdoubleton)
qed

subsubsection‹Field›

definition ffield :: "V ⇒ V"
where "ffield r = 𝒟⇩∙ r ∪⇩∘ ℛ⇩∙ r"

abbreviation app_ffield :: "V ⇒ V" (‹ℱ⇩∙›)
where "ℱ⇩∙ r ≡ ffield r"

text‹Rules.›

lemma ffieldI1[intro]:
assumes "a ∈⇩∘ 𝒟⇩∙ r ∪⇩∘ ℛ⇩∙ r"
shows "a ∈⇩∘ ffield r"
using assms unfolding ffield_def by simp

lemma ffieldI2[intro]:
assumes "[a, b]⇩∘ ∈⇩∘ r"
shows "a ∈⇩∘ ffield r"
using assms by auto

lemma ffieldI3[intro]:
assumes "[a, b]⇩∘ ∈⇩∘ r"
shows "b ∈⇩∘ ffield r"
using assms by auto

lemma ffieldD[intro]:
assumes "a ∈⇩∘ ffield r"
shows "a ∈⇩∘ 𝒟⇩∙ r ∪⇩∘ ℛ⇩∙ r"
using assms unfolding ffield_def by simp

lemma ffieldE[elim]:
assumes "a ∈⇩∘ ffield r" and "a ∈⇩∘ 𝒟⇩∙ r ∪⇩∘ ℛ⇩∙ r ⟹ P"
shows P
using assms by (auto dest: ffieldD)

lemma ffield_pair[elim]:
assumes "a ∈⇩∘ ffield r"
obtains b where "[a, b]⇩∘ ∈⇩∘ r ∨ [b, a]⇩∘ ∈⇩∘ r "
using assms by auto

lemma ffield_iff: "a ∈⇩∘ ffield r ⟷ (∃b. [a, b]⇩∘ ∈⇩∘ r ∨ [b, a]⇩∘ ∈⇩∘ r)" by auto

text‹Set operations.›

lemma ffield_vempty[simp]: "ffield 0 = 0" by force

lemma ffield_vsingleton[simp]: "ffield (set {[a, b]⇩∘}) = set {a, b}" by force

lemma ffield_vdoubleton[simp]:
"ffield (set {[a, b]⇩∘, [c, d]⇩∘}) = set {a, b, c, d}"
by force

lemma ffield_mono:
assumes "r ⊆⇩∘ s"
shows "ffield r ⊆⇩∘ ffield s"
using assms by fastforce

lemma ffield_vinsert[simp]:
"ffield (vinsert [a, b]⇩∘ r) = set {a, b} ∪⇩∘ (ffield r)"
apply (intro vsubset_antisym; intro vsubsetI)
subgoal by auto
subgoal by (metis ffield_iff vinsert_iff vinsert_vinsert)
done

lemma ffield_vunion[simp]: "ffield (r ∪⇩∘ s) = ffield r ∪⇩∘ ffield s"
unfolding ffield_def by auto

text‹Connections.›

lemma fid_on_ffield[simp]: "ffield (fid_on A) = A" by force

lemma fconst_on_ffield_ne[intro, simp]:
assumes "A ≠ 0"
shows "ffield (fconst_on A c) = vinsert c A"
using assms by force

lemma fconst_on_ffield_vempty[simp]: "ffield (fconst_on 0 c) = 0" by auto

lemma ffield_fconverse[simp]: "ffield (r¯⇩∙) = ffield r" by force

text‹Special properties.›

lemma ffield_vsubset_VUnion2: "ℱ⇩∙ r ⊆⇩∘ ⋃⇩∘(⋃⇩∘(⋃⇩∘r))"
using fdomain_vsubset_VUnion2 frange_vsubset_VUnion2 by (auto simp: ffield_def)

subsubsection‹Image›

definition fimage :: "V ⇒ V ⇒ V" (infixr ‹`⇩∙› 90)
where "r `⇩∙ A = ℛ⇩∙ (r ↾⇧l⇩∙ A)"
notation fimage (infixr "`⇩∙" 90)

lemma fimage_small[simp]: "small {b. ∃a∈⇩∘A. [a, b]⇩∘ ∈⇩∘ r}"
proof-
from image_iff ord_of_nat_succ_vempty have ss:
"{b. ∃a∈⇩∘A. [a, b]⇩∘ ∈⇩∘ r} ⊆ (λx. x⦇1⇩ℕ⦈) ` elts r"
by fastforce
have small: "small ((λx. x⦇1⇩ℕ⦈) ` elts r)" by (rule replacement) simp
show ?thesis by (rule smaller_than_small, rule small, rule ss)
qed

text‹Rules.›

lemma fimageI1:
assumes "x ∈⇩∘ ℛ⇩∙ (r ↾⇧l⇩∙ A)"
shows "x ∈⇩∘ r `⇩∙ A"
using assms unfolding fimage_def by simp

lemma fimageI2[intro]:
assumes "[a, b]⇩∘ ∈⇩∘ r" and "a ∈⇩∘ A"
shows "b ∈⇩∘ r `⇩∙ A"
using assms fimageI1 by auto

lemma fimageD[dest]:
assumes "x ∈⇩∘ r `⇩∙ A"
shows "x ∈⇩∘ ℛ⇩∙ (r ↾⇧l⇩∙ A)"
using assms unfolding fimage_def by simp

lemma fimageE[elim]:
assumes "b ∈⇩∘ r `⇩∙ A"
obtains a where "[a, b]⇩∘ ∈⇩∘ r" and "a ∈⇩∘ A"
using assms unfolding fimage_def by auto

lemma fimage_iff: "b ∈⇩∘ r `⇩∙ A ⟷ (∃a∈⇩∘A. [a, b]⇩∘ ∈⇩∘ r)" by auto

text‹Set operations.›

lemma fimage_vempty[simp]: "0 `⇩∙ A = 0" by force

lemma fimage_of_vempty[simp]: "r `⇩∙ 0 = 0" by force

lemma fimage_vsingleton_in[intro, simp]:
assumes "a ∈⇩∘ A"
shows "set {[a, b]⇩∘} `⇩∙ A = set {b}"
using assms by auto

lemma fimage_vsingleton_nin[intro, simp]:
assumes "a ∉⇩∘ A"
shows "set {[a, b]⇩∘} `⇩∙ A = 0"
using assms by auto

lemma fimage_vsingleton_vinsert[intro, simp]:
"set {[a, b]⇩∘} `⇩∙ vinsert a A = set {b}"
by auto

lemma fimage_mono:
assumes "r' ⊆⇩∘ r" and "A' ⊆⇩∘ A"
shows "(r' `⇩∙ A') ⊆⇩∘ (r `⇩∙ A)"
using assms by fastforce

lemma fimage_vinsert: "r `⇩∙ (vinsert a A) = r `⇩∙ set {a} ∪⇩∘ r `⇩∙ A" by auto

lemma fimage_vunion_left: "(r ∪⇩∘ s) `⇩∙ A = r `⇩∙ A ∪⇩∘ s `⇩∙ A" by auto

lemma fimage_vunion_right: "r `⇩∙ (A ∪⇩∘ B) = r `⇩∙ A ∪⇩∘ r `⇩∙ B" by auto

lemma fimage_vintersection: "r `⇩∙ (A ∩⇩∘ B) ⊆⇩∘ r `⇩∙ A ∩⇩∘ r `⇩∙ B" by auto

lemma fimage_vdiff: "r `⇩∙ A -⇩∘ r `⇩∙ B ⊆⇩∘ r `⇩∙ (A -⇩∘ B)" by auto

text‹Special properties.›

lemma fimage_vsingleton_iff[iff]: "b ∈⇩∘ r `⇩∙ set {a} ⟷ [a, b]⇩∘ ∈⇩∘ r" by auto

lemma fimage_is_vempty[iff]: "r `⇩∙ A = 0 ⟷ vdisjnt (𝒟⇩∙ r) A" by fastforce

text‹Connections.›

lemma fid_on_fimage[simp]: "(fid_on A) `⇩∙ B = A ∩⇩∘ B" by force

lemma fimage_fconst_on_ne[simp]:
assumes "B ∩⇩∘ A ≠ 0"
shows "(fconst_on A c) `⇩∙ B = set {c}"
using assms by auto

lemma fimage_fconst_on_vempty[simp]:
assumes "vdisjnt A B"
shows "(fconst_on A c) `⇩∙ B = 0"
using assms by auto

lemma fimage_fconst_on_vsubset_const[simp]: "(fconst_on A c) `⇩∙ B ⊆⇩∘ set {c}"
by auto

lemma fcomp_frange: "ℛ⇩∙ (r ∘⇩∙ s) = r `⇩∙ (ℛ⇩∙ s)" by blast

lemma fcomp_fimage: "(r ∘⇩∙ s) `⇩∙ A = r `⇩∙ (s `⇩∙ A)" by blast

lemma fimage_flrestriction[simp]: "(r ↾⇧l⇩∙ A) `⇩∙ B = r `⇩∙ (A ∩⇩∘ B)" by auto

lemma fimage_frrestriction[simp]: "(r ↾⇧r⇩∙ A) `⇩∙ B = A ∩⇩∘ r `⇩∙ B" by auto

lemma fimage_frestriction[simp]: "(r ↾⇩∙ A) `⇩∙ B = A ∩⇩∘ (r `⇩∙ (A ∩⇩∘ B))" by auto

lemma fimage_fdomain: "r `⇩∙ 𝒟⇩∙ r = ℛ⇩∙ r" by auto

lemma fimage_eq_imp_fcomp:
assumes "f `⇩∙ A = g `⇩∙ B"
shows "(h ∘⇩∙ f) `⇩∙ A = (h ∘⇩∙ g) `⇩∙ B"
using assms by (metis fcomp_fimage)

text‹Previous connections.›

lemma fcomp_rel_fconst_on_ftimes: "r ∘⇩∙ (fconst_on A c) = A ×⇩∙ (r `⇩∙ set {c})"
by blast

text‹Further special properties.›

lemma fimage_vsubset:
assumes "r ⊆⇩∘ A ×⇩∙ B"
shows "r `⇩∙ C ⊆⇩∘ B"
using assms by blast

lemma fimage_set_def: "r `⇩∙ A = set {b. ∃a∈⇩∘A. [a, b]⇩∘ ∈⇩∘ r}"
unfolding fimage_def frange_def by auto

lemma fimage_vsingleton: "r `⇩∙ set {a} = set {b. [a, b]⇩∘ ∈⇩∘ r}"
proof-
have "{b. [a, b]⇩∘ ∈⇩∘ r} ⊆ {b. ∃a. [a, b]⇩∘ ∈⇩∘ r}" by auto
then have [simp]: "small {b. [a, b]⇩∘ ∈⇩∘ r}"
by (rule smaller_than_small[OF frange_small[of r]])
show ?thesis by auto
qed

lemma fimage_strict_vsubset: "f `⇩∙ A ⊆⇩∘ f `⇩∙ 𝒟⇩∙ f" by auto

subsubsection‹Inverse image›

definition finvimage :: "V ⇒ V ⇒ V" (infixr ‹-`⇩∙› 90)
where "r -`⇩∙ A = r¯⇩∙ `⇩∙ A"

lemma finvimage_small[simp]: "small {a. ∃b∈⇩∘A. [a, b]⇩∘ ∈⇩∘ r}"
proof-
have ss: "{a. ∃b∈⇩∘A. [a, b]⇩∘ ∈⇩∘ r} ⊆ (λx. x⦇0⇩ℕ⦈) ` elts r"
using image_iff by fastforce
have small: "small ((λx. x⦇0⇩ℕ⦈) ` elts r)" by (rule replacement) simp
show ?thesis by (rule smaller_than_small, rule small, rule ss)
qed

text‹Rules.›

lemma finvimageI[intro]:
assumes "[a, b]⇩∘ ∈⇩∘ r" and "b ∈⇩∘ A"
shows "a ∈⇩∘ r -`⇩∙ A"
using assms finvimage_def by auto

lemma finvimageD[dest]:
assumes "a ∈⇩∘ r -`⇩∙ A"
shows "a ∈⇩∘ 𝒟⇩∙ (r ↾⇧r⇩∙ A)"
using assms using finvimage_def by auto

lemma finvimageE[elim]:
assumes "a ∈⇩∘ r -`⇩∙ A"
obtains b where "[a, b]⇩∘ ∈⇩∘ r" and "b ∈⇩∘ A"
using assms unfolding finvimage_def by auto

lemma finvimageI1:
assumes "a ∈⇩∘ 𝒟⇩∙ (r ↾⇧r⇩∙ A)"
shows "a ∈⇩∘ r -`⇩∙ A"
using assms unfolding fimage_def
by (simp add: finvimage_def fimageI1 flrestriction_fconverse)

lemma finvimageD1:
assumes "a ∈⇩∘ r -`⇩∙ A"
shows "a ∈⇩∘ 𝒟⇩∙ (r ↾⇧r⇩∙ A)"
using assms by fastforce

lemma finvimageE1:
assumes "a ∈⇩∘ r -`⇩∙ A " and "a ∈⇩∘ 𝒟⇩∙ (r ↾⇧r⇩∙ A) ⟹ P"
shows P
using assms by auto

lemma finvimageI2:
assumes "a ∈⇩∘ r¯⇩∙ `⇩∙ A"
shows "a ∈⇩∘ r -`⇩∙ A"
using assms unfolding finvimage_def by simp

lemma finvimageD2:
assumes "a ∈⇩∘ r -`⇩∙ A"
shows "a ∈⇩∘ r¯⇩∙ `⇩∙ A"
using assms unfolding finvimage_def by simp

lemma finvimageE2:
assumes "a ∈⇩∘ r -`⇩∘ A" and "a ∈⇩∘ r¯⇩∘ `⇩∘ A ⟹ P"
shows P
unfolding vimage_def using assms by blast

lemma finvimage_iff: "a ∈⇩∘ r -`⇩∙ A ⟷ (∃b∈⇩∘A. [a, b]⇩∘ ∈⇩∘ r)" by auto

lemma finvimage_iff1: "a ∈⇩∘ r -`⇩∙ A ⟷ a ∈⇩∘ 𝒟⇩∙ (r ↾⇧r⇩∙ A)" by auto

lemma finvimage_iff2: "a ∈⇩∘ r -`⇩∙ A ⟷ a ∈⇩∘ r¯⇩∙ `⇩∙ A" by auto

text‹Set operations.›

lemma finvimage_vempty[simp]: "0 -`⇩∙ A = 0" by force

lemma finvimage_of_vempty[simp]: "r -`⇩∙ 0 = 0" by force

lemma finvimage_vsingleton_in[intro, simp]:
assumes "b ∈⇩∘ A"
shows "set {[a, b]⇩∘} -`⇩∙ A = set {a}"
using assms by auto

lemma finvimage_vsingleton_nin[intro, simp]:
assumes "b ∉⇩∘ A"
shows "set {[a, b]⇩∘} -`⇩∙ A = 0"
using assms by auto

lemma finvimage_vsingleton_vinsert[intro, simp]:
"set {[a, b]⇩∘} -`⇩∙ vinsert b A = set {a}"
by auto

lemma finvimage_mono:
assumes "r' ⊆⇩∘ r" and "A' ⊆⇩∘ A"
shows "(r' -`⇩∙ A') ⊆⇩∘ (r -`⇩∙ A)"
using assms by fastforce

lemma finvimage_vinsert: "r -`⇩∙ (vinsert a A) = r -`⇩∙ set {a} ∪⇩∘ r -`⇩∙ A" by auto

lemma finvimage_vunion_left: "(r ∪⇩∘ s) -`⇩∙ A = r -`⇩∙ A ∪⇩∘ s -`⇩∙ A" by auto

lemma finvimage_vunion_right: "r -`⇩∙ (A ∪⇩∘ B) = r -`⇩∙ A ∪⇩∘ r -`⇩∙ B" by auto

lemma finvimage_vintersection: "r -`⇩∙ (A ∩⇩∘ B) ⊆⇩∘ r -`⇩∙ A ∩⇩∘ r -`⇩∙ B" by auto

lemma finvimage_vdiff: "r -`⇩∙ A -⇩∘ r -`⇩∙ B ⊆⇩∘ r -`⇩∙ (A -⇩∘ B)" by auto

text‹Special properties.›

lemma finvimage_set_def: "r -`⇩∙ A = set {a. ∃b∈⇩∘A. [a, b]⇩∘ ∈⇩∘ r}" by fastforce

lemma finvimage_eq_fdomain_frestriction: "r -`⇩∙ A = 𝒟⇩∙ (r ↾⇧r⇩∙ A)" by fastforce

lemma finvimage_frange[simp]: "r -`⇩∙ ℛ⇩∙ r = 𝒟⇩∙ r"
unfolding invimage_def by force

lemma finvimage_frange_vsubset[simp]:
assumes "ℛ⇩∙ r ⊆⇩∘ B"
shows "r -`⇩∙ B = 𝒟⇩∙ r"
using assms unfolding finvimage_def by force

text‹Connections.›

lemma finvimage_fid_on[simp]: "(fid_on A) -`⇩∙ B = A ∩⇩∘ B" by force

lemma finvimage_fconst_on_vsubset_fdomain[simp]: "(fconst_on A c) -`⇩∙ B ⊆⇩∘ A"
unfolding finvimage_def by blast

lemma finvimage_fconst_on_ne[simp]:
assumes "c ∈⇩∘ B"
shows "(fconst_on A c) -`⇩∙ B = A"
by (simp add: assms finvimage_eq_fdomain_frestriction frrestriction_fconst_on)

lemma finvimage_fconst_on_vempty[simp]:
assumes "c ∉⇩∘ B"
shows "(fconst_on A c) -`⇩∙ B = 0"
using assms by auto

lemma finvimage_fcomp: "(g ∘⇩∙ f) -`⇩∙ x = f -`⇩∙ (g -`⇩∙ x) "
by (simp add: finvimage_def fconverse_fcomp fcomp_fimage)

lemma finvimage_fconverse[simp]: "r¯⇩∙ -`⇩∙ A = r `⇩∙ A" by auto

lemma finvimage_flrestriction[simp]: "(r ↾⇧l⇩∙ A) -`⇩∙ B = A ∩⇩∘ r -`⇩∙ B" by auto

lemma finvimage_frrestriction[simp]: "(r ↾⇧r⇩∙ A) -`⇩∙ B = (r -`⇩∙ (A ∩⇩∘ B))" by auto

lemma finvimage_frestriction[simp]: "(r ↾⇩∙ A) -`⇩∙ B = A ∩⇩∘ (r -`⇩∙ (A ∩⇩∘ B))"
by blast

text‹Previous connections.›

lemma fdomain_fcomp[simp]: "𝒟⇩∙ (r ∘⇩∙ s) = s -`⇩∙ 𝒟⇩∙ r" by force

subsection‹Classification of relations›

subsubsection‹Binary relation›

locale fbrelation =
fixes r :: V
assumes fbrelation[simp]: "fpairs r = r"

locale fbrelation_pair = r⇩1: fbrelation r⇩1 + r⇩2: fbrelation r⇩2 for r⇩1 r⇩2

text‹Rules.›

lemma fpairs_eqI[intro!]:
assumes "⋀x. x ∈⇩∘ r ⟹ ∃a b. x = [a, b]⇩∘"
shows "fpairs r = r"
using assms by auto

lemma fpairs_eqD[dest]:
assumes "fpairs r = r"
shows "⋀x. x ∈⇩∘ r ⟹ ∃a b. x = [a, b]⇩∘"
using assms by auto

lemma fpairs_eqE[elim!]:
assumes "fpairs r = r" and "(⋀x. x ∈⇩∘ r ⟹ ∃a b. x = [a, b]⇩∘) ⟹ P"
shows P
using assms by auto

lemmas fbrelationI[intro!] = fbrelation.intro
lemmas fbrelationD[dest!] = fbrelation.fbrelation

lemma fbrelationE[elim!]:
assumes "fbrelation r" and "(fpairs r = r) ⟹ P"
shows P
using assms unfolding fbrelation_def by auto

lemma fbrelationE1:
assumes "fbrelation r" and "x ∈⇩∘ r"
obtains a b where "x = [a, b]⇩∘"
using assms by auto

lemma fbrelationD1[dest]:
assumes "fbrelation r" and "x ∈⇩∘ r"
shows "∃a b. x = [a, b]⇩∘"
using assms by auto

text‹Set operations.›

lemma fbrelation_vsubset:
assumes "fbrelation s" and "r ⊆⇩∘ s"
shows "fbrelation r"
using assms by auto

lemma fbrelation_vinsert: "fbrelation (vinsert [a, b]⇩∘ r) ⟷ fbrelation r"
by auto

lemma (in fbrelation) fbrelation_vinsertI: "fbrelation (vinsert [a, b]⇩∘ r)"
using fbrelation_axioms by auto

lemma fbrelation_vinsertD[dest]:
assumes "fbrelation (vinsert ⟨a, b⟩ r)"
shows "fbrelation r"
using assms by auto

lemma fbrelation_vunion: "fbrelation (r ∪⇩∘ s) ⟷ fbrelation r ∧ fbrelation s"
by auto

lemma (in fbrelation_pair) fbrelation_vunionI: "fbrelation (r⇩1 ∪⇩∘ r⇩2)"
using r⇩1.fbrelation_axioms r⇩2.fbrelation_axioms by auto

lemma fbrelation_vunionD[dest]:
assumes "fbrelation (r ∪⇩∘ s)"
shows "fbrelation r" and "fbrelation s"
using assms by auto

lemma (in fbrelation) fbrelation_vintersectionI: "fbrelation (r ∩⇩∘ s)"
using fbrelation_axioms by auto

lemma (in fbrelation) fbrelation_vdiffI: "fbrelation (r -⇩∘ s)"
using fbrelation_axioms by auto

text‹Connections.›

lemma fbrelation_vempty: "fbrelation 0" by auto

lemma fbrelation_vsingleton: "fbrelation (set {[a, b]⇩∘})" by auto

global_interpretation frel_vsingleton: fbrelation ‹set {[a, b]⇩∘}›
by (rule fbrelation_vsingleton)

lemma fbrelation_vdoubleton: "fbrelation (set {[a, b]⇩∘, [c, d]⇩∘})" by auto

lemma fbrelation_sid_on[simp]: "fbrelation (fid_on A)" by auto

lemma fbrelation_fconst_on[simp]: "fbrelation (fconst_on A c)" by auto

lemma (in fbrelation_pair) fbrelation_fcomp: "fbrelation (r⇩1 ∘⇩∙ r⇩2)"
using r⇩1.fbrelation_axioms r⇩2.fbrelation_axioms by auto

sublocale fbrelation_pair ⊆ fcomp⇩2⇩1: fbrelation ‹r⇩2 ∘⇩∙ r⇩1›
by
(
fbrelation_pair.fbrelation_fcomp
fbrelation_pair_def
r⇩1.fbrelation_axioms
r⇩2.fbrelation_axioms
)

sublocale fbrelation_pair ⊆ fcomp⇩1⇩2: fbrelation ‹r⇩1 ∘⇩∙ r⇩2›
by (rule fbrelation_fcomp)

lemma (in fbrelation) fbrelation_fconverse: "fbrelation (r¯⇩∙)"
using fbrelation_axioms by clarsimp

lemma fbrelation_flrestriction[intro, simp]: "fbrelation (r ↾⇧l⇩∙ A)" by auto

lemma fbrelation_frrestriction[intro, simp]: "fbrelation (r ↾⇧r⇩∙ A)" by auto

lemma fbrelation_frestriction[intro, simp]: "fbrelation (r ↾⇩∙ A)" by auto

text‹Previous connections.›

lemma (in fbrelation) fconverse_fconverse[simp]: "(r¯⇩∙)¯⇩∙ = r"
using fbrelation_axioms by auto

lemma (in fbrelation_pair) fconverse_mono[simp]: "r⇩1¯⇩∙ ⊆⇩∘ r⇩2¯⇩∙ ⟷ r⇩1 ⊆⇩∘ r⇩2"
using r⇩1.fbrelation_axioms r⇩2.fbrelation_axioms
by (force intro: fconverse_vunion)+

lemma (in fbrelation_pair) fconverse_inject[simp]: "r⇩1¯⇩∙ = r⇩2¯⇩∙ ⟷ r⇩1 = r⇩2"
using r⇩1.fbrelation_axioms r⇩2.fbrelation_axioms by fast

lemma (in fbrelation) fconverse_vsubset_swap_2:
assumes "r¯⇩∙ ⊆⇩∘ s"
shows "r ⊆⇩∘ s¯⇩∙"
using assms fbrelation_axioms by auto

lemma (in fbrelation) flrestriction_fdomain[simp]: "r ↾⇧l⇩∙ 𝒟⇩∙ r = r"
using fbrelation_axioms by (elim fbrelationE) blast

lemma (in fbrelation) frrestriction_frange[simp]: "r ↾⇧r⇩∙ ℛ⇩∙ r = r"
using fbrelation_axioms by (elim fbrelationE) blast

text‹Special properties.›

lemma vsubset_vtimes_fbrelation:
assumes "r ⊆⇩∘ A ×⇩∙ B"
shows "fbrelation r"
using assms by blast

lemma (in fbrelation) fbrelation_vintersection_vdomain:
assumes "vdisjnt (𝒟⇩∙ r) (𝒟⇩∙ s)"
shows "vdisjnt r s"
proof(rule vsubset_antisym; rule vsubsetI)
fix x assume "x ∈⇩∘ r ∩⇩∘ s"
then obtain a b where "[a, b]⇩∘ ∈⇩∘ r ∩⇩∘ s"
by (metis fbrelationE1 fbrelation_vintersectionI)
with assms show "x ∈⇩∘ 0" by auto
qed simp

lemma (in fbrelation) fbrelation_vintersection_vrange:
assumes "vdisjnt (ℛ⇩∙ r) (ℛ⇩∙ s)"
shows "vdisjnt r s"
proof(rule vsubset_antisym; rule vsubsetI)
fix x assume "x ∈⇩∘ r ∩⇩∘ s"
then obtain a b where "[a, b]⇩∘ ∈⇩∘ r ∩⇩∘ s"
by (metis fbrelationE1 fbrelation_vintersectionI)
with assms show "x ∈⇩∘ 0" by auto
qed simp

lemma (in fbrelation) fbrelation_vintersection_vfield:
assumes "vdisjnt (ffield r) (ffield s)"
shows "vdisjnt r s"
proof(rule vsubset_antisym; rule vsubsetI)
fix x assume "x ∈⇩∘ r ∩⇩∘ s"
then obtain a b where "[a, b]⇩∘ ∈⇩∘ r ∩⇩∘ s"
by (metis fbrelationE1 fbrelation_vintersectionI)
with assms show "x ∈⇩∘ 0" by auto
qed auto

lemma (in fbrelation) vdomain_vrange_vtimes: "r ⊆⇩∘ 𝒟⇩∙ r ×⇩∙ ℛ⇩∙ r"
using fbrelation by blast

lemma (in fbrelation) fconverse_eq_frel[intro, simp]:
assumes "⋀a b. [a, b]⇩∘ ∈⇩∘ r ⟹ [b, a]⇩∘ ∈⇩∘ r"
shows "r¯⇩∙ = r"
using assms
apply (intro vsubset_antisym; intro vsubsetI)
subgoal by blast
subgoal by (metis fconverseE fconverseI fconverse_fconverse)
done

lemma fcomp_fconverse_frel_eq_frel_fbrelationI:
assumes "r¯⇩∙ ∘⇩∙ r = r"
shows "fbrelation r"
using assms by (intro fbrelationI, elim vequalityE vsubsetE) force

text‹Alternative forms of existing results.›

lemmas [intro, simp] = fbrelation.fconverse_fconverse
and fconverse_eq_frel[intro, simp] = fbrelation.fconverse_eq_frel

context
fixes r⇩1 r⇩2
assumes r⇩1: "fbrelation r⇩1"
and r⇩2: "fbrelation r⇩2"
begin

lemmas_with[OF fbrelation_pair.intro[OF r⇩1 r⇩2]] :
fbrelation_fconverse_mono[intro, simp] = fbrelation_pair.fconverse_mono
and fbrelation_frrestriction_srange[intro, simp] =
fbrelation_pair.fconverse_inject

end

text‹\newpage›

end```