# Theory CZH_Sets_BRelations

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

section‹Elementary binary relations›
theory CZH_Sets_BRelations
imports CZH_Sets_Sets
keywords "mk_VLambda" :: thy_defn
and "|app" "|vsv" "|vdomain"
begin

subsection‹Background›

text‹
This section presents a theory of binary relations internalized in the
type \<^typ>‹V› and exposes elementary properties of two special types of
binary relations: single-valued binary relations and injective single-valued
binary relations.

Many of the results that are presented in this section were carried over
(with amendments) from the theories \<^text>‹Set› and \<^text>‹Relation› in the main
library.
›

subsection‹Constructors›

subsubsection‹Identity relation›

definition vid_on :: "V ⇒ V"
where "vid_on A = set {⟨a, a⟩ | a. a ∈⇩∘ A}"

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

text‹Rules.›

lemma vid_on_eqI:
assumes "a = b" and "a ∈⇩∘ A"
shows "⟨a, b⟩ ∈⇩∘ vid_on A"
using assms by (simp add: vid_on_def)

lemma vid_onI[intro!]:
assumes "a ∈⇩∘ A"
shows "⟨a, a⟩ ∈⇩∘ vid_on A"
by (rule vid_on_eqI) (simp_all add: assms)

lemma vid_onD[dest!]:
assumes "⟨a, a⟩ ∈⇩∘ vid_on A"
shows "a ∈⇩∘ A"
using assms unfolding vid_on_def by auto

lemma vid_onE[elim!]:
assumes "x ∈⇩∘ vid_on A" and "∃a∈⇩∘A. x = ⟨a, a⟩ ⟹ P"
shows P
using assms unfolding vid_on_def by auto

lemma vid_on_iff: "⟨a, b⟩ ∈⇩∘ vid_on A ⟷ a = b ∧ a ∈⇩∘ A" by auto

text‹Set operations.›

lemma vid_on_vempty[simp]: "vid_on 0 = 0" by auto

lemma vid_on_vsingleton[simp]: "vid_on (set {a}) = set {⟨a, a⟩}" by auto

lemma vid_on_vdoubleton[simp]: "vid_on (set {a, b}) = set {⟨a, a⟩, ⟨b, b⟩}"
by (auto simp: vinsert_set_insert_eq)

lemma vid_on_mono:
assumes "A ⊆⇩∘ B"
shows "vid_on A ⊆⇩∘ vid_on B"
using assms by auto

lemma vid_on_vinsert: "(vinsert ⟨a, a⟩ (vid_on A)) = (vid_on (vinsert a A))"
by auto

lemma vid_on_vintersection: "vid_on (A ∩⇩∘ B) = vid_on A ∩⇩∘ vid_on B" by auto

lemma vid_on_vunion: "vid_on (A ∪⇩∘ B) = vid_on A ∪⇩∘ vid_on B" by auto

lemma vid_on_vdiff: "vid_on (A -⇩∘ B) = vid_on A -⇩∘ vid_on B" by auto

text‹Special properties.›

lemma vid_on_vsubset_vtimes: "vid_on A ⊆⇩∘ A ×⇩∘ A" by clarsimp

lemma VLambda_id[simp]: "VLambda A id = vid_on A"
by (simp add: id_def vid_on_def Setcompr_eq_image VLambda_def)

subsubsection‹Constant function›

definition vconst_on :: "V ⇒ V ⇒ V"
where "vconst_on A c = set {⟨a, c⟩ | a. a ∈⇩∘ A}"

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

text‹Rules.›

lemma vconst_onI[intro!]:
assumes "a ∈⇩∘ A"
shows "⟨a, c⟩ ∈⇩∘ vconst_on A c"
using assms unfolding vconst_on_def by simp

lemma vconst_onD[dest!]:
assumes "⟨a, c⟩ ∈⇩∘ vconst_on A c"
shows "a ∈⇩∘ A"
using assms unfolding vconst_on_def by simp

lemma vconst_onE[elim!]:
assumes "x ∈⇩∘ vconst_on A c"
obtains a where "a ∈⇩∘ A" and "x = ⟨a, c⟩"
using assms unfolding vconst_on_def by auto

lemma vconst_on_iff: "⟨a, c⟩ ∈⇩∘ vconst_on A c ⟷ a ∈⇩∘ A" by auto

text‹Set operations.›

lemma vconst_on_vempty[simp]: "vconst_on 0 c = 0"
unfolding vconst_on_def by auto

lemma vconst_on_vsingleton[simp]: "vconst_on (set {a}) c = set {⟨a, c⟩}" by auto

lemma vconst_on_vdoubleton[simp]: "vconst_on (set {a, b}) c = set {⟨a, c⟩, ⟨b, c⟩}"
by (auto simp: vinsert_set_insert_eq)

lemma vconst_on_mono:
assumes "A ⊆⇩∘ B"
shows "vconst_on A c ⊆⇩∘ vconst_on B c"
using assms by auto

lemma vconst_on_vinsert:
"(vinsert ⟨a, c⟩ (vconst_on A c)) = (vconst_on (vinsert a A) c)"
by auto

lemma vconst_on_vintersection:
"vconst_on (A ∩⇩∘ B) c = vconst_on A c ∩⇩∘ vconst_on B c"
by auto

lemma vconst_on_vunion: "vconst_on (A ∪⇩∘ B) c = vconst_on A c ∪⇩∘ vconst_on B c"
by auto

lemma vconst_on_vdiff: "vconst_on (A -⇩∘ B) c = vconst_on A c -⇩∘ vconst_on B c"
by auto

text‹Special properties.›

lemma vconst_on_eq_vtimes: "vconst_on A c = A ×⇩∘ set {c}"
by standard (auto intro!: vsubset_antisym)

subsubsection‹‹VLambda››

text‹Rules.›

lemma VLambdaI[intro!]:
assumes "a ∈⇩∘ A"
shows "⟨a, f a⟩ ∈⇩∘ (λa∈⇩∘A. f a)"
using assms unfolding VLambda_def by auto

assumes "⟨a, f a⟩ ∈⇩∘ (λa∈⇩∘A. f a)"
shows "a ∈⇩∘ A"
using assms unfolding VLambda_def by auto

lemma VLambdaE[elim!]:
assumes "x ∈⇩∘ (λa∈⇩∘A. f a)"
obtains a where "a ∈⇩∘ A" and "x = ⟨a, f a⟩"
using assms unfolding VLambda_def by auto

lemma VLambda_iff1: "x ∈⇩∘ (λa∈⇩∘A. f a) ⟷ (∃a∈⇩∘A. x = ⟨a, f a⟩)" by auto

lemma VLambda_iff2: "⟨a, b⟩ ∈⇩∘ (λa∈⇩∘A. f a) ⟷ b = f a ∧ a ∈⇩∘ A" by auto

lemma small_VLambda[simp]: "small {⟨a, f a⟩ | a. a ∈⇩∘ A}" by auto

lemma VLambda_set_def: "(λa∈⇩∘A. f a) = set {⟨a, f a⟩ | a. a ∈⇩∘ A}" by auto

text‹Set operations.›

lemma VLambda_vempty[simp]: "(λa∈⇩∘0. f a) = 0" by auto

lemma VLambda_vsingleton(*not simp*): "(λa∈⇩∘set {a}. f a) = set {⟨a, f a⟩}"
by auto

lemma VLambda_vdoubleton(*not simp*):
"(λa∈⇩∘set {a, b}. f a) = set {⟨a, f a⟩, ⟨b, f b⟩}"
by (auto simp: vinsert_set_insert_eq)

lemma VLambda_mono:
assumes "A ⊆⇩∘ B"
shows "(λa∈⇩∘A. f a) ⊆⇩∘ (λa∈⇩∘B. f a)"
using assms by auto

lemma VLambda_vinsert:
"(λa∈⇩∘vinsert a A. f a) = (λa∈⇩∘set {a}. f a) ∪⇩∘ (λa∈⇩∘A. f a)"
by auto

lemma VLambda_vintersection: "(λa∈⇩∘A ∩⇩∘ B. f a) = (λa∈⇩∘A. f a) ∩⇩∘ (λa∈⇩∘B. f a)"
by auto

lemma VLambda_vunion: "(λa∈⇩∘A ∪⇩∘ B. f a) = (λa∈⇩∘A. f a) ∪⇩∘ (λa∈⇩∘B. f a)" by auto

lemma VLambda_vdiff: "(λa∈⇩∘A -⇩∘ B. f a) = (λa∈⇩∘A. f a) -⇩∘ (λa∈⇩∘B. f a)" by auto

text‹Connections.›

lemma VLambda_vid_on: "(λa∈⇩∘A. a) = vid_on A" by auto

lemma VLambda_vconst_on: "(λa∈⇩∘A. c) = vconst_on A c" by auto

subsubsection‹Composition›

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

lemma vcomp_small[simp]: "small {⟨a, c⟩ | a c. ∃b. ⟨a, b⟩ ∈⇩∘ s ∧ ⟨b, c⟩ ∈⇩∘ r}"
(is ‹small ?s›)
proof-
define comp' where "comp' = (λ⟨⟨a, b⟩, ⟨c, d⟩⟩. ⟨a, d⟩)"
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
then show "x ∈ comp' ` elts (vpairs (s ×⇩∘ r))"
unfolding x_def' using abbc by auto
qed
with small_comp show ?thesis by (metis (lifting) smaller_than_small)
qed

text‹Rules.›

lemma vcompI[intro!]:
assumes "⟨b, c⟩ ∈⇩∘ r" and "⟨a, b⟩ ∈⇩∘ s"
shows "⟨a, c⟩ ∈⇩∘ r ∘⇩∘ s"
using assms unfolding vcomp_def by auto

lemma vcompD[dest!]:
assumes "⟨a, c⟩ ∈⇩∘ r ∘⇩∘ s"
shows "∃b. ⟨b, c⟩ ∈⇩∘ r ∧ ⟨a, b⟩ ∈⇩∘ s"
using assms unfolding vcomp_def by auto

lemma vcompE[elim!]:
assumes "ac ∈⇩∘ r ∘⇩∘ s"
obtains a b c where "ac = ⟨a, c⟩" and "⟨a, b⟩ ∈⇩∘ s" and "⟨b, c⟩ ∈⇩∘ r"
using assms unfolding vcomp_def by clarsimp

text‹Elementary properties.›

lemma vcomp_assoc: "(r ∘⇩∘ s) ∘⇩∘ t = r ∘⇩∘ (s ∘⇩∘ t)" by auto

text‹Set operations.›

lemma vcomp_vempty_left[simp]: "0 ∘⇩∘ r = 0" by auto

lemma vcomp_vempty_right[simp]: "r ∘⇩∘ 0 = 0" by auto

lemma vcomp_mono:
assumes "r' ⊆⇩∘ r" and "s' ⊆⇩∘ s"
shows "r' ∘⇩∘ s' ⊆⇩∘ r ∘⇩∘ s"
using assms by auto

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

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

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

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

text‹Connections.›

lemma vcomp_vid_on_idem[simp]: "vid_on A ∘⇩∘ vid_on A = vid_on A" by auto

lemma vcomp_vid_on[simp]: "vid_on A ∘⇩∘ vid_on B = vid_on (A ∩⇩∘ B)" by auto

lemma vcomp_vconst_on_vid_on[simp]: "vconst_on A c ∘⇩∘ vid_on A = vconst_on A c"
by auto

lemma vcomp_VLambda_vid_on[simp]: "(λa∈⇩∘A. f a) ∘⇩∘ vid_on A = (λa∈⇩∘A. f a)"
by auto

text‹Special properties.›

lemma vcomp_vsubset_vtimes:
assumes "r ⊆⇩∘ B ×⇩∘ C" and "s ⊆⇩∘ A ×⇩∘ B"
shows "r ∘⇩∘ s ⊆⇩∘ A ×⇩∘ C"
using assms by auto

lemma vcomp_obtain_middle[elim]:
assumes "⟨a, c⟩ ∈⇩∘ r ∘⇩∘ s"
obtains b where "⟨a, b⟩ ∈⇩∘ s" and "⟨b, c⟩ ∈⇩∘ r"
using assms by auto

subsubsection‹Converse relation›

definition vconverse :: "V ⇒ V"
where "vconverse A = (λr∈⇩∘A. set {⟨b, a⟩ | a b. ⟨a, b⟩ ∈⇩∘ r})"

abbreviation app_vconverse (‹(_¯⇩∘)› [1000] 999)
where "r¯⇩∘ ≡ vconverse (set {r}) ⦇r⦈"

lemma app_vconverse_def: "r¯⇩∘ = set {⟨b, a⟩ | a b. ⟨a, b⟩ ∈⇩∘ r}"
unfolding vconverse_def by simp

lemma vconverse_small[simp]: "small {⟨b, a⟩ | a b. ⟨a, b⟩ ∈⇩∘ r}"
proof-
have eq: "{⟨b, a⟩ | a b. ⟨a, b⟩ ∈⇩∘ r} = (λ⟨a, b⟩. ⟨b, a⟩) ` elts (vpairs r)"
proof(rule subset_antisym; rule subsetI, unfold mem_Collect_eq)
fix x assume "x ∈ (λ⟨a, b⟩. ⟨b, a⟩) ` elts (vpairs r)"
then obtain a b where "⟨a, b⟩ ∈⇩∘ vpairs r" and "x = (λ⟨a, b⟩. ⟨b, a⟩) ⟨a, b⟩"
by blast
then show "∃a b. x = ⟨b, a⟩ ∧ ⟨a, b⟩ ∈⇩∘ r" by auto
qed (use image_iff vpairs_iff_elts in fastforce)
show ?thesis unfolding eq by (rule replacement) auto
qed

text‹Rules.›

lemma vconverseI[intro!]:
assumes "r ∈⇩∘ A"
shows "⟨r, r¯⇩∘⟩ ∈⇩∘ vconverse A"
using assms unfolding vconverse_def by auto

lemma vconverseD[dest]:
assumes "⟨r, s⟩ ∈⇩∘ vconverse A"
shows "r ∈⇩∘ A" and "s = r¯⇩∘"
using assms unfolding vconverse_def by auto

lemma vconverseE[elim]:
assumes "x ∈⇩∘ vconverse A"
obtains r where "x = ⟨r, r¯⇩∘⟩" and "r ∈⇩∘ A"
using assms unfolding vconverse_def by auto

lemma app_vconverseI[sym, intro!]:
assumes "⟨a, b⟩ ∈⇩∘ r"
shows "⟨b, a⟩ ∈⇩∘ r¯⇩∘"
using assms unfolding vconverse_def by auto

lemma app_vconverseD[sym, dest]:
assumes "⟨a, b⟩ ∈⇩∘ r¯⇩∘"
shows "⟨b, a⟩ ∈⇩∘ r"
using assms unfolding vconverse_def by simp

lemma app_vconverseE[elim!]:
assumes "x ∈⇩∘ r¯⇩∘"
obtains a b where "x = ⟨b, a⟩" and "⟨a, b⟩ ∈⇩∘ r"
using assms unfolding vconverse_def by auto

lemma vconverse_iff: "⟨b, a⟩ ∈⇩∘ r¯⇩∘ ⟷ ⟨a, b⟩ ∈⇩∘ r" by auto

text‹Set operations.›

lemma vconverse_vempty[simp]: "0¯⇩∘ = 0" by auto

lemma vconverse_vsingleton: "(set {⟨a, b⟩})¯⇩∘ = set {⟨b, a⟩}" by auto

lemma vconverse_vdoubleton[simp]: "(set {⟨a, b⟩, ⟨c, d⟩})¯⇩∘ = set {⟨b, a⟩, ⟨d, c⟩}"
by (auto simp: vinsert_set_insert_eq)

lemma vconverse_vinsert: "(vinsert ⟨a, b⟩ r)¯⇩∘ = vinsert ⟨b, a⟩ (r¯⇩∘)" by auto

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

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

text‹Connections.›

lemma vconverse_vid_on[simp]: "(vid_on A)¯⇩∘ = vid_on A" by auto

lemma vconverse_vconst_on[simp]: "(vconst_on A c)¯⇩∘ = set {c} ×⇩∘ A" by auto

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

lemma vconverse_vtimes: "(A ×⇩∘ B)¯⇩∘ = (B ×⇩∘ A)" by auto

subsubsection‹Left restriction›

definition vlrestriction :: "V ⇒ V"
where "vlrestriction D =
VLambda D (λ⟨r, A⟩. set {⟨a, b⟩ | a b. a ∈⇩∘ A ∧ ⟨a, b⟩ ∈⇩∘ r})"

abbreviation app_vlrestriction :: "V ⇒ V ⇒ V" (infixr ‹↾⇧l⇩∘› 80)
where "r ↾⇧l⇩∘ A ≡ vlrestriction (set {⟨r, A⟩}) ⦇⟨r, A⟩⦈"

lemma app_vlrestriction_def: "r ↾⇧l⇩∘ A = set {⟨a, b⟩ | a b. a ∈⇩∘ A ∧ ⟨a, b⟩ ∈⇩∘ r}"
unfolding vlrestriction_def by simp

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

text‹Rules.›

lemma vlrestrictionI[intro!]:
assumes "⟨r, A⟩ ∈⇩∘ D"
shows "⟨⟨r, A⟩, r ↾⇧l⇩∘ A⟩ ∈⇩∘ vlrestriction D"
using assms unfolding vlrestriction_def by (simp add: VLambda_iff2)

lemma vlrestrictionD[dest]:
assumes "⟨⟨r, A⟩, s⟩ ∈⇩∘ vlrestriction D"
shows "⟨r, A⟩ ∈⇩∘ D" and "s = r ↾⇧l⇩∘ A"
using assms unfolding vlrestriction_def by auto

lemma vlrestrictionE[elim]:
assumes "x ∈⇩∘ vlrestriction D" and "D ⊆⇩∘ R ×⇩∘ X"
obtains r A where "x = ⟨⟨r, A⟩, r ↾⇧l⇩∘ A⟩" and "r ∈⇩∘ R" and "A ∈⇩∘ X"
using assms unfolding vlrestriction_def by auto

lemma app_vlrestrictionI[intro!]:
assumes "a ∈⇩∘ A" and "⟨a, b⟩ ∈⇩∘ r"
shows "⟨a, b⟩ ∈⇩∘ r ↾⇧l⇩∘ A"
using assms unfolding vlrestriction_def by simp

lemma app_vlrestrictionD[dest]:
assumes "⟨a, b⟩ ∈⇩∘ r ↾⇧l⇩∘ A"
shows "a ∈⇩∘ A" and "⟨a, b⟩ ∈⇩∘ r"
using assms unfolding vlrestriction_def by auto

lemma app_vlrestrictionE[elim]:
assumes "x ∈⇩∘ r ↾⇧l⇩∘ A"
obtains a b where "x = ⟨a, b⟩" and "a ∈⇩∘ A" and "⟨a, b⟩ ∈⇩∘ r"
using assms unfolding vlrestriction_def by auto

text‹Set operations.›

lemma vlrestriction_on_vempty[simp]: "r ↾⇧l⇩∘ 0 = 0"
by (auto intro!: vsubset_antisym)

lemma vlrestriction_vempty[simp]: "0 ↾⇧l⇩∘ A = 0" by auto

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

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

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

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

lemma vlrestriction_vinsert_in:
assumes "a ∈⇩∘ A"
shows "(vinsert ⟨a, b⟩ r) ↾⇧l⇩∘ A = vinsert ⟨a, b⟩ (r ↾⇧l⇩∘ A)"
using assms by auto

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

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

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

text‹Connections.›

lemma vlrestriction_vid_on[simp]: "(vid_on A) ↾⇧l⇩∘ B = vid_on (A ∩⇩∘ B)" by auto

lemma vlrestriction_vconst_on: "(vconst_on A c) ↾⇧l⇩∘ B = (vconst_on B c) ↾⇧l⇩∘ A"
by auto

lemma vlrestriction_vconst_on_commute:
assumes "x ∈⇩∘ vconst_on A c ↾⇧l⇩∘ B"
shows "x ∈⇩∘ vconst_on B c ↾⇧l⇩∘ A"
using assms by auto

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

text‹Previous connections.›

lemma vcomp_rel_vid_on[simp]: "r ∘⇩∘ vid_on A = r ↾⇧l⇩∘ A" by auto

lemma vcomp_vconst_on:
"r ∘⇩∘ (vconst_on A c) = (r ↾⇧l⇩∘ set {c}) ∘⇩∘ (vconst_on A c)"
by auto

text‹Special properties.›

lemma vlrestriction_vsubset_vpairs: "r ↾⇧l⇩∘ A ⊆⇩∘ vpairs r"
by (rule vsubsetI) blast

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

lemma vlrestriction_VLambda: "(λa∈⇩∘A. f a) ↾⇧l⇩∘ B = (λa∈⇩∘A ∩⇩∘ B. f a)" by auto

subsubsection‹Right restriction›

definition vrrestriction :: "V ⇒ V"
where "vrrestriction D =
VLambda D (λ⟨r, A⟩. set {⟨a, b⟩ | a b. b ∈⇩∘ A ∧ ⟨a, b⟩ ∈⇩∘ r})"

abbreviation app_vrrestriction :: "V ⇒ V ⇒ V" (infixr ‹↾⇧r⇩∘› 80)
where "r ↾⇧r⇩∘ A ≡ vrrestriction (set {⟨r, A⟩}) ⦇⟨r, A⟩⦈"

lemma app_vrrestriction_def: "r ↾⇧r⇩∘ A = set {⟨a, b⟩ | a b. b ∈⇩∘ A ∧ ⟨a, b⟩ ∈⇩∘ r}"
unfolding vrrestriction_def by simp

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

text‹Rules.›

lemma vrrestrictionI[intro!]:
assumes "⟨r, A⟩ ∈⇩∘ D"
shows "⟨⟨r, A⟩, r ↾⇧r⇩∘ A⟩ ∈⇩∘ vrrestriction D"
using assms unfolding vrrestriction_def by (simp add: VLambda_iff2)

lemma vrrestrictionD[dest]:
assumes "⟨⟨r, A⟩, s⟩ ∈⇩∘ vrrestriction D"
shows "⟨r, A⟩ ∈⇩∘ D" and "s = r ↾⇧r⇩∘ A"
using assms unfolding vrrestriction_def by auto

lemma vrrestrictionE[elim]:
assumes "x ∈⇩∘ vrrestriction D" and "D ⊆⇩∘ R ×⇩∘ X"
obtains r A where "x = ⟨⟨r, A⟩, r ↾⇧r⇩∘ A⟩" and "r ∈⇩∘ R" and "A ∈⇩∘ X"
using assms unfolding vrrestriction_def by auto

lemma app_vrrestrictionI[intro!]:
assumes "b ∈⇩∘ A" and "⟨a, b⟩ ∈⇩∘ r"
shows "⟨a, b⟩ ∈⇩∘ r ↾⇧r⇩∘ A"
using assms unfolding vrrestriction_def by simp

lemma app_vrrestrictionD[dest]:
assumes "⟨a, b⟩ ∈⇩∘ r ↾⇧r⇩∘ A"
shows "b ∈⇩∘ A" and "⟨a, b⟩ ∈⇩∘ r"
using assms unfolding vrrestriction_def by auto

lemma app_vrrestrictionE[elim]:
assumes "x ∈⇩∘ r ↾⇧r⇩∘ A"
obtains a b where "x = ⟨a, b⟩" and "b ∈⇩∘ A" and "⟨a, b⟩ ∈⇩∘ r"
using assms unfolding vrrestriction_def by auto

text‹Set operations.›

lemma vrrestriction_on_vempty[simp]: "r ↾⇧r⇩∘ 0 = 0"
by (auto intro!: vsubset_antisym)

lemma vrrestriction_vempty[simp]: "0 ↾⇧r⇩∘ A = 0" by auto

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

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

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

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

lemma vrrestriction_vinsert_in:
assumes "b ∈⇩∘ A"
shows "(vinsert ⟨a, b⟩ r) ↾⇧r⇩∘ A = vinsert ⟨a, b⟩ (r ↾⇧r⇩∘ A)"
using assms by auto

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

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

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

text‹Connections.›

lemma vrrestriction_vid_on[simp]: "(vid_on A) ↾⇧r⇩∘ B = vid_on (A ∩⇩∘ B)" by auto

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

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

text‹Previous connections.›

lemma vcomp_vid_on_rel[simp]: "vid_on A ∘⇩∘ r = r ↾⇧r⇩∘ A"
by (auto intro!: vsubset_antisym)

lemma vcomp_vconst_on_rel: "(vconst_on A c) ∘⇩∘ r = (vconst_on A c) ∘⇩∘ (r ↾⇧r⇩∘ A)"
by auto

lemma vlrestriction_vconverse: "r¯⇩∘ ↾⇧l⇩∘ A = (r ↾⇧r⇩∘ A)¯⇩∘" by auto

lemma vrrestriction_vconverse: "r¯⇩∘ ↾⇧r⇩∘ A = (r ↾⇧l⇩∘ A)¯⇩∘" by auto

text‹Special properties.›

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

lemma vrrestriction_vsubset_vpairs: "r ↾⇧r⇩∘ A ⊆⇩∘ vpairs r" by auto

subsubsection‹Restriction›

definition vrestriction :: "V ⇒ V"
where "vrestriction D =
VLambda D (λ⟨r, A⟩. set {⟨a, b⟩ | a b. a ∈⇩∘ A ∧ b ∈⇩∘ A ∧ ⟨a, b⟩ ∈⇩∘ r})"

abbreviation app_vrestriction :: "V ⇒ V ⇒ V" (infixr ‹↾⇩∘› 80)
where "r ↾⇩∘ A ≡ vrestriction (set {⟨r, A⟩}) ⦇⟨r, A⟩⦈"

lemma app_vrestriction_def:
"r ↾⇩∘ A = set {⟨a, b⟩ | a b. a ∈⇩∘ A ∧ b ∈⇩∘ A ∧ ⟨a, b⟩ ∈⇩∘ r}"
unfolding vrestriction_def by simp

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

text‹Rules.›

lemma vrestrictionI[intro!]:
assumes "⟨r, A⟩ ∈⇩∘ D"
shows "⟨⟨r, A⟩, r ↾⇩∘ A⟩ ∈⇩∘ vrestriction D"
using assms unfolding vrestriction_def by (simp add: VLambda_iff2)

lemma vrestrictionD[dest]:
assumes "⟨⟨r, A⟩, s⟩ ∈⇩∘ vrestriction D"
shows "⟨r, A⟩ ∈⇩∘ D" and "s = r ↾⇩∘ A"
using assms unfolding vrestriction_def by auto

lemma vrestrictionE[elim]:
assumes "x ∈⇩∘ vrestriction D" and "D ⊆⇩∘ R ×⇩∘ X"
obtains r A where "x = ⟨⟨r, A⟩, r ↾⇩∘ A⟩" and "r ∈⇩∘ R" and "A ∈⇩∘ X"
using assms unfolding vrestriction_def by auto

lemma app_vrestrictionI[intro!]:
assumes "a ∈⇩∘ A" and "b ∈⇩∘ A" and "⟨a, b⟩ ∈⇩∘ r"
shows "⟨a, b⟩ ∈⇩∘ r ↾⇩∘ A"
using assms unfolding vrestriction_def by simp

lemma app_vrestrictionD[dest]:
assumes "⟨a, b⟩ ∈⇩∘ r ↾⇩∘ A"
shows "a ∈⇩∘ A" and "b ∈⇩∘ A" and "⟨a, b⟩ ∈⇩∘ r"
using assms unfolding vrestriction_def by auto

lemma app_vrestrictionE[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 vrestriction_def by clarsimp

text‹Set operations.›

lemma vrestriction_on_vempty[simp]: "r ↾⇩∘ 0 = 0"
by (auto intro!: vsubset_antisym)

lemma vrestriction_vempty[simp]: "0 ↾⇩∘ A = 0" by auto

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

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

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

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

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

lemma vrestriction_vinsert_in:
assumes "a ∈⇩∘ A" and "b ∈⇩∘ A"
shows "(vinsert ⟨a, b⟩ r) ↾⇩∘ A = vinsert ⟨a, b⟩ (r ↾⇩∘ A)"
using assms by auto

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

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

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

text‹Connections.›

lemma vrestriction_vid_on[simp]: "(vid_on A) ↾⇩∘ B = vid_on (A ∩⇩∘ B)" by auto

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

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

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

lemma vrestriction_vconverse: "r¯⇩∘ ↾⇩∘ A = (r ↾⇩∘ A)¯⇩∘" by auto

text‹Previous connections.›

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

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

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

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

text‹Special properties.›

lemma vrestriction_vsubset_vpairs: "r ↾⇩∘ A ⊆⇩∘ vpairs r" by auto

lemma vrestriction_vsubset_vtimes: "r ↾⇩∘ A ⊆⇩∘ A ×⇩∘ A" by auto

lemma vrestriction_vsubset_rel: "r ↾⇩∘ A ⊆⇩∘ r" by auto

subsection‹Properties›

subsubsection‹Domain›

definition vdomain :: "V ⇒ V"
where "vdomain D = (λr∈⇩∘D. set {a. ∃b. ⟨a, b⟩ ∈⇩∘ r})"

abbreviation app_vdomain :: "V ⇒ V" (‹𝒟⇩∘›)
where "𝒟⇩∘ r ≡ vdomain (set {r}) ⦇r⦈"

lemma app_vdomain_def: "𝒟⇩∘ r = set {a. ∃b. ⟨a, b⟩ ∈⇩∘ r}"
unfolding vdomain_def by simp

lemma vdomain_small[simp]: "small {a. ∃b. ⟨a, b⟩ ∈⇩∘ r}"
proof-
have ss: "{a. ∃b. ⟨a, b⟩ ∈⇩∘ r} ⊆ vfst ` elts r" using image_iff by fastforce
have small: "small (vfst ` elts r)" by (rule replacement) simp
show ?thesis by (rule smaller_than_small, rule small, rule ss)
qed

text‹Rules.›

lemma vdomainI[intro!]:
assumes "r ∈⇩∘ A"
shows "⟨r, 𝒟⇩∘ r⟩ ∈⇩∘ vdomain A"
using assms unfolding vdomain_def by auto

lemma vdomainD[dest]:
assumes "⟨r, s⟩ ∈⇩∘ vdomain A"
shows "r ∈⇩∘ A" and "s = 𝒟⇩∘ r"
using assms unfolding vdomain_def by auto

lemma vdomainE[elim]:
assumes "x ∈⇩∘ vdomain A"
obtains r where "x = ⟨r, 𝒟⇩∘ r⟩" and "r ∈⇩∘ A"
using assms unfolding vdomain_def by auto

lemma app_vdomainI[intro]:
assumes "⟨a, b⟩ ∈⇩∘ r"
shows "a ∈⇩∘ 𝒟⇩∘ r"
using assms unfolding vdomain_def by auto

lemma app_vdomainD[dest]:
assumes "a ∈⇩∘ 𝒟⇩∘ r"
shows "∃b. ⟨a, b⟩ ∈⇩∘ r"
using assms unfolding vdomain_def by auto

lemma app_vdomainE[elim]:
assumes "a ∈⇩∘ 𝒟⇩∘ r"
obtains b where "⟨a, b⟩ ∈⇩∘ r"
using assms unfolding vdomain_def by clarsimp

lemma vdomain_iff: "a ∈⇩∘ 𝒟⇩∘ r ⟷ (∃y. ⟨a, y⟩ ∈⇩∘ r)" by auto

text‹Set operations.›

lemma vdomain_vempty[simp]: "𝒟⇩∘ 0 = 0" by (auto intro!: vsubset_antisym)

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

lemma vdomain_vdoubleton[simp]: "𝒟⇩∘ (set {⟨a, b⟩, ⟨c, d⟩}) = set {a, c}"
by (auto simp: vinsert_set_insert_eq)

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

lemma vdomain_vinsert[simp]: "𝒟⇩∘ (vinsert ⟨a, b⟩ r) = vinsert a (𝒟⇩∘ r)"
by (auto intro!: vsubset_antisym)

lemma vdomain_vunion: "𝒟⇩∘ (A ∪⇩∘ B) = 𝒟⇩∘ A ∪⇩∘ 𝒟⇩∘ B"
by (auto intro!: vsubset_antisym)

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

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

text‹Connections.›

lemma vdomain_vid_on[simp]: "𝒟⇩∘ (vid_on A) = A"
by (auto intro!: vsubset_antisym)

lemma vdomain_vconst_on[simp]: "𝒟⇩∘ (vconst_on A c) = A"
by (auto intro!: vsubset_antisym)

lemma vdomain_VLambda[simp]: "𝒟⇩∘ (λa∈⇩∘A. f a) = A"
by (auto intro!: vsubset_antisym)

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

lemma vdomain_vlrestriction_vsubset:
assumes "A ⊆⇩∘ 𝒟⇩∘ r"
shows "𝒟⇩∘ (r ↾⇧l⇩∘ A) = A"
using assms by (auto simp: vdomain_vlrestriction)

text‹Special properties.›

lemma vdomain_vsubset_vtimes:
assumes "vpairs r ⊆⇩∘ x ×⇩∘ y"
shows "𝒟⇩∘ r ⊆⇩∘ x"
using assms by auto

subsubsection‹Range›

definition vrange :: "V ⇒ V"
where "vrange D = (λr∈⇩∘D. set {b. ∃a. ⟨a, b⟩ ∈⇩∘ r})"

abbreviation app_vrange :: "V ⇒ V" (‹ℛ⇩∘›)
where "ℛ⇩∘ r ≡ vrange (set {r}) ⦇r⦈"

lemma app_vrange_def: "ℛ⇩∘ r = set {b. ∃a. ⟨a, b⟩ ∈⇩∘ r}"
unfolding vrange_def by simp

lemma vrange_small[simp]: "small {b. ∃a. ⟨a, b⟩ ∈⇩∘ r}"
proof-
have ss: "{b. ∃a. ⟨a, b⟩ ∈⇩∘ r} ⊆ vsnd ` elts r" using image_iff by fastforce
have small: "small (vsnd ` elts r)" by (rule replacement) simp
show ?thesis by (rule smaller_than_small, rule small, rule ss)
qed

text‹Rules.›

lemma vrangeI[intro]:
assumes "r ∈⇩∘ A"
shows "⟨r, ℛ⇩∘ r⟩ ∈⇩∘ vrange A"
using assms unfolding vrange_def by auto

lemma vrangeD[dest]:
assumes "⟨r, s⟩ ∈⇩∘ vrange A"
shows "r ∈⇩∘ A" and "s = ℛ⇩∘ r"
using assms unfolding vrange_def by auto

lemma vrangeE[elim]:
assumes "x ∈⇩∘ vrange A"
obtains r where "x = ⟨r, ℛ⇩∘ r⟩" and "r ∈⇩∘ A"
using assms unfolding vrange_def by auto

lemma app_vrangeI[intro]:
assumes "⟨a, b⟩ ∈⇩∘ r"
shows "b ∈⇩∘ ℛ⇩∘ r"
using assms unfolding vrange_def by auto

lemma app_vrangeD[dest]:
assumes "b ∈⇩∘ ℛ⇩∘ r"
shows "∃a. ⟨a, b⟩ ∈⇩∘ r"
using assms unfolding vrange_def by simp

lemma app_vrangeE[elim]:
assumes "b ∈⇩∘ ℛ⇩∘ r"
obtains a where "⟨a, b⟩ ∈⇩∘ r"
using assms unfolding vrange_def by clarsimp

lemma vrange_iff: "b ∈⇩∘ ℛ⇩∘ r ⟷ (∃a. ⟨a, b⟩ ∈⇩∘ r)" by auto

text‹Set operations.›

lemma vrange_vempty[simp]: "ℛ⇩∘ 0 = 0" by (auto intro!: vsubset_antisym)

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

lemma vrange_vdoubleton[simp]: "ℛ⇩∘ (set {⟨a, b⟩, ⟨c, d⟩}) = set {b, d}"
by (auto simp: vinsert_set_insert_eq)

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

lemma vrange_vinsert[simp]: "ℛ⇩∘ (vinsert ⟨a, b⟩ r) = vinsert b (ℛ⇩∘ r)"
by (auto intro!: vsubset_antisym)

lemma vrange_vunion: "ℛ⇩∘ (r ∪⇩∘ s) = ℛ⇩∘ r ∪⇩∘ ℛ⇩∘ s"
by (auto intro!: vsubset_antisym)

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

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

text‹Connections.›

lemma vrange_vid_on[simp]: "ℛ⇩∘ (vid_on A) = A" by (auto intro!: vsubset_antisym)

lemma vrange_vconst_on_vempty[simp]: "ℛ⇩∘ (vconst_on 0 c) = 0" by auto

lemma vrange_vconst_on_ne[simp]:
assumes "A ≠ 0"
shows "ℛ⇩∘ (vconst_on A c) = set {c}"
using assms by (auto intro!: vsubset_antisym)

lemma vrange_VLambda: "ℛ⇩∘ (λa∈⇩∘A. f a) = set (f ` elts A)"
by (intro vsubset_antisym vsubsetI) auto

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

text‹Previous connections›

lemma vdomain_vconverse[simp]: "𝒟⇩∘ (r¯⇩∘) = ℛ⇩∘ r"
by (auto intro!: vsubset_antisym)

lemma vrange_vconverse[simp]: "ℛ⇩∘ (r¯⇩∘) = 𝒟⇩∘ r"
by (auto intro!: vsubset_antisym)

text‹Special properties.›

lemma vrange_iff_vdomain: "b ∈⇩∘ ℛ⇩∘ r ⟷ (∃a∈⇩∘𝒟⇩∘ r. ⟨a, b⟩ ∈⇩∘ r)" by auto

lemma vrange_vsubset_vtimes:
assumes "vpairs r ⊆⇩∘ x ×⇩∘ y"
shows "ℛ⇩∘ r ⊆⇩∘ y"
using assms by auto

lemma vrange_VLambda_vsubset:
assumes "⋀x. x ∈⇩∘ A ⟹ f x ∈⇩∘ B"
shows "ℛ⇩∘ (VLambda A f) ⊆⇩∘ B"
using assms by auto

lemma vpairs_vsubset_vdomain_vrange[simp]: "vpairs r ⊆⇩∘ 𝒟⇩∘ r ×⇩∘ ℛ⇩∘ r"
by (rule vsubsetI) auto

lemma vrange_vsubset:
assumes "⋀x y. ⟨x, y⟩ ∈⇩∘ r ⟹ y ∈⇩∘ A"
shows "ℛ⇩∘ r ⊆⇩∘ A"
using assms by auto

subsubsection‹Field›

definition vfield :: "V ⇒ V"
where "vfield D = (λr∈⇩∘D. 𝒟⇩∘ r ∪⇩∘ ℛ⇩∘ r)"

abbreviation app_vfield :: "V ⇒ V" (‹ℱ⇩∘›)
where "ℱ⇩∘ r ≡ vfield (set {r}) ⦇r⦈"

lemma app_vfield_def: "ℱ⇩∘ r = 𝒟⇩∘ r ∪⇩∘ ℛ⇩∘ r" unfolding vfield_def by simp

text‹Rules.›

lemma vfieldI[intro!]:
assumes "r ∈⇩∘ A"
shows "⟨r, ℱ⇩∘ r⟩ ∈⇩∘ vfield A"
using assms unfolding vfield_def by auto

lemma vfieldD[dest]:
assumes "⟨r, s⟩ ∈⇩∘ vfield A"
shows "r ∈⇩∘ A" and "s = ℱ⇩∘ r"
using assms unfolding vfield_def by auto

lemma vfieldE[elim]:
assumes "x ∈⇩∘ vfield A"
obtains r where "x = ⟨r, ℱ⇩∘ r⟩" and "r ∈⇩∘ A"
using assms unfolding vfield_def by auto

lemma app_vfieldI1[intro]:
assumes "a ∈⇩∘ 𝒟⇩∘ r ∪⇩∘ ℛ⇩∘ r"
shows "a ∈⇩∘ ℱ⇩∘ r"
using assms unfolding vfield_def by simp

lemma app_vfieldI2[intro]:
assumes "⟨a, b⟩ ∈⇩∘ r"
shows "a ∈⇩∘ ℱ⇩∘ r"
using assms by auto

lemma app_vfieldI3[intro]:
assumes "⟨a, b⟩ ∈⇩∘ r"
shows "b ∈⇩∘ ℱ⇩∘ r"
using assms by auto

lemma app_vfieldD[dest]:
assumes "a ∈⇩∘ ℱ⇩∘ r"
shows "a ∈⇩∘ 𝒟⇩∘ r ∪⇩∘ ℛ⇩∘ r"
using assms unfolding vfield_def by simp

lemma app_vfieldE[elim]:
assumes "a ∈⇩∘ ℱ⇩∘ r" and "a ∈⇩∘ 𝒟⇩∘ r ∪⇩∘ ℛ⇩∘ r ⟹ P"
shows P
using assms by auto

lemma app_vfield_vpairE[elim]:
assumes "a ∈⇩∘ ℱ⇩∘ r"
obtains b where "⟨a, b⟩ ∈⇩∘ r ∨ ⟨b, a⟩ ∈⇩∘ r "
using assms unfolding app_vfield_def by blast

lemma vfield_iff: "a ∈⇩∘ ℱ⇩∘ r ⟷ (∃b. ⟨a, b⟩ ∈⇩∘ r ∨ ⟨b, a⟩ ∈⇩∘ r)" by auto

text‹Set operations.›

lemma vfield_vempty[simp]: "ℱ⇩∘ 0 = 0" by (auto intro!: vsubset_antisym)

lemma vfield_vsingleton[simp]: "ℱ⇩∘ (set {⟨a, b⟩}) = set {a, b}"

lemma vfield_vdoubleton[simp]: "ℱ⇩∘ (set {⟨a, b⟩, ⟨c, d⟩}) = set {a, b, c, d}"
by (auto simp: vinsert_set_insert_eq)

lemma vfield_mono:
assumes "r ⊆⇩∘ s"
shows "ℱ⇩∘ r ⊆⇩∘ ℱ⇩∘ s"
using assms by fastforce

lemma vfield_vinsert[simp]: "ℱ⇩∘ (vinsert ⟨a, b⟩ r) = set {a, b} ∪⇩∘ ℱ⇩∘ r"
by (auto intro!: vsubset_antisym)

lemma vfield_vunion[simp]: "ℱ⇩∘ (r ∪⇩∘ s) = ℱ⇩∘ r ∪⇩∘ ℱ⇩∘ s"
by (auto intro!: vsubset_antisym)

text‹Connections.›

lemma vid_on_vfield[simp]: "ℱ⇩∘ (vid_on A) = A" by (auto intro!: vsubset_antisym)

lemma vconst_on_vfield_ne[intro, simp]:
assumes "A ≠ 0"
shows "ℱ⇩∘ (vconst_on A c) = vinsert c A"
using assms by (auto intro!: vsubset_antisym)

lemma vconst_on_vfield_vempty[simp]: "ℱ⇩∘ (vconst_on 0 c) = 0" by auto

lemma vfield_vconverse[simp]: "ℱ⇩∘ (r¯⇩∘) = ℱ⇩∘ r"
by (auto intro!: vsubset_antisym)

subsubsection‹Image›

definition vimage :: "V ⇒ V"
where "vimage D = VLambda D (λ⟨r, A⟩. ℛ⇩∘ (r ↾⇧l⇩∘ A))"

abbreviation app_vimage :: "V ⇒ V ⇒ V" (infixr ‹`⇩∘› 90)
where "r `⇩∘ A ≡ vimage (set {⟨r, A⟩}) ⦇⟨r, A⟩⦈"

lemma app_vimage_def: "r `⇩∘ A = ℛ⇩∘ (r ↾⇧l⇩∘ A)" unfolding vimage_def by simp

lemma vimage_small[simp]: "small {b. ∃a∈⇩∘A. ⟨a, b⟩ ∈⇩∘ r}"
proof-
have ss: "{b. ∃a∈⇩∘A. ⟨a, b⟩ ∈⇩∘ r} ⊆ vsnd ` elts r"
using image_iff by fastforce
have small: "small (vsnd ` elts r)" by (rule replacement) simp
show ?thesis by (rule smaller_than_small, rule small, rule ss)
qed

lemma app_vimage_set_def: "r `⇩∘ A = set {b. ∃a∈⇩∘A. ⟨a, b⟩ ∈⇩∘ r}"
unfolding vimage_def vrange_def by auto

text‹Rules.›

lemma vimageI[intro!]:
assumes "⟨r, A⟩ ∈⇩∘ D"
shows "⟨⟨r, A⟩, r `⇩∘ A⟩ ∈⇩∘ vimage D"
using assms unfolding vimage_def by (simp add: VLambda_iff2)

lemma vimageD[dest]:
assumes "⟨⟨r, A⟩, s⟩ ∈⇩∘ vimage D"
shows "⟨r, A⟩ ∈⇩∘ D" and "s = r `⇩∘ A"
using assms unfolding vimage_def by auto

lemma vimageE[elim]:
assumes "x ∈⇩∘ vimage (R ×⇩∘ X)"
obtains r A where "x = ⟨⟨r, A⟩, r `⇩∘ A⟩" and "r ∈⇩∘ R" and "A ∈⇩∘ X"
using assms unfolding vimage_def by auto

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

lemma app_vimageI2[intro]:
assumes "⟨a, b⟩ ∈⇩∘ r" and "a ∈⇩∘ A"
shows "b ∈⇩∘ r `⇩∘ A"
using assms app_vimageI1 by auto

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

lemma app_vimageE[elim]:
assumes "b ∈⇩∘ r `⇩∘ A"
obtains a where "⟨a, b⟩ ∈⇩∘ r" and "a ∈⇩∘ A"
using assms unfolding vimage_def by auto

lemma app_vimage_iff: "b ∈⇩∘ r `⇩∘ A ⟷ (∃a∈⇩∘A. ⟨a, b⟩ ∈⇩∘ r)" by auto

text‹Set operations.›

lemma vimage_vempty[simp]: "0 `⇩∘ A = 0" by (auto intro!: vsubset_antisym)

lemma vimage_of_vempty[simp]: "r `⇩∘ 0 = 0" by (auto intro!: vsubset_antisym)

lemma vimage_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 vrange_small[of r]])
show ?thesis using app_vimage_set_def by auto
qed

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

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

lemma vimage_vsingleton_vinsert[simp]: "set {⟨a, b⟩} `⇩∘ vinsert a A = set {b}"
by auto

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

lemma vimage_vinsert: "r `⇩∘ (vinsert a A) = r `⇩∘ set {a} ∪⇩∘ r `⇩∘ A"
by (auto intro!: vsubset_antisym)

lemma vimage_vunion_left: "(r ∪⇩∘ s) `⇩∘ A = r `⇩∘ A ∪⇩∘ s `⇩∘ A"
by (auto intro!: vsubset_antisym)

lemma vimage_vunion_right: "r `⇩∘ (A ∪⇩∘ B) = r `⇩∘ A ∪⇩∘ r `⇩∘ B"
by (auto intro!: vsubset_antisym)

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

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

text‹Previous set operations.›

lemma VPow_vinsert:
"VPow (vinsert a A) = VPow A ∪⇩∘ ((λx∈⇩∘VPow A. vinsert a x) `⇩∘ VPow A)"
proof(intro vsubset_antisym vsubsetI)
fix x assume "x ∈⇩∘ VPow (vinsert a A)"
then have "x ⊆⇩∘ vinsert a A" by simp
then consider "x ⊆⇩∘ A" | "a ∈⇩∘ x" by auto
then show "x ∈⇩∘ VPow A ∪⇩∘ (λx∈⇩∘VPow A. vinsert a x) `⇩∘ VPow A"
proof cases
case 1 then show ?thesis by simp
next
case 2
define x' where "x' = x -⇩∘ set {a}"
with 2 have "x = vinsert a x'" and "a ∉⇩∘ x'" by auto
with ‹x ⊆⇩∘ vinsert a A› show ?thesis
unfolding vimage_def
by (fastforce simp: vsubset_vinsert vlrestriction_VLambda)
qed
qed (elim vunionE, auto)

text‹Special properties.›

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

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

lemma vcomp_vimage_vtimes_right:
assumes "r `⇩∘ Y = Z"
shows "r ∘⇩∘ (X ×⇩∘ Y) = X ×⇩∘ Z"
proof(intro vsubset_antisym vsubsetI)
fix x assume x: "x ∈⇩∘ r ∘⇩∘ (X ×⇩∘ Y)"
then obtain a c where x_def: "x = ⟨a, c⟩" and "a ∈⇩∘ X" and "c ∈⇩∘ ℛ⇩∘ r" by auto
with x obtain b where "⟨a, b⟩ ∈⇩∘ X ×⇩∘ Y" and "⟨b, c⟩ ∈⇩∘ r" by clarsimp
then show "x ∈⇩∘ X ×⇩∘ Z" unfolding x_def using assms by auto
next
fix x assume "x ∈⇩∘ X ×⇩∘ Z"
then obtain a c where x_def: "x = ⟨a, c⟩" and "a ∈⇩∘ X" and "c ∈⇩∘ Z" by auto
then show "x ∈⇩∘ r ∘⇩∘ X ×⇩∘ Y"
using assms unfolding x_def by (meson VSigmaI app_vimageE vcompI)
qed

text‹Connections.›

lemma vid_on_vimage[simp]: "vid_on A `⇩∘ B = A ∩⇩∘ B"
by (auto intro!: vsubset_antisym)

lemma vimage_vconst_on_ne[simp]:
assumes "B ∩⇩∘ A ≠ 0"
shows "vconst_on A c `⇩∘ B = set {c}"
using assms by auto

lemma vimage_vconst_on_vempty[simp]:
assumes "vdisjnt A B"
shows "vconst_on A c `⇩∘ B = 0"
using assms by auto

lemma vimage_vconst_on_vsubset_vconst: "vconst_on A c `⇩∘ B ⊆⇩∘ set {c}" by auto

lemma vimage_VLambda_vrange: "(λa∈⇩∘A. f a) `⇩∘ B = ℛ⇩∘ (λa∈⇩∘A ∩⇩∘ B. f a)"
unfolding vimage_def by (simp add: vlrestriction_VLambda)

lemma vimage_VLambda_vrange_rep: "(λa∈⇩∘A. f a) `⇩∘ A = ℛ⇩∘ (λa∈⇩∘A. f a)"

lemma vcomp_vimage: "(r ∘⇩∘ s) `⇩∘ A = r `⇩∘ (s `⇩∘ A)"
by (auto intro!: vsubset_antisym)

lemma vimage_vlrestriction[simp]: "(r ↾⇧l⇩∘ A) `⇩∘ B = r `⇩∘ (A ∩⇩∘ B)"
by (auto intro!: vsubset_antisym)

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

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

lemma vimage_vdomain: "r `⇩∘ 𝒟⇩∘ r = ℛ⇩∘ r" by (auto intro!: vsubset_antisym)

lemma vimage_eq_imp_vcomp:
assumes "r `⇩∘ A = s `⇩∘ B"
shows "(t ∘⇩∘ r) `⇩∘ A = (t ∘⇩∘ s) `⇩∘ B"
using assms by (metis vcomp_vimage)

text‹Previous connections.›

lemma vcomp_rel_vconst: "r ∘⇩∘ (vconst_on A c) = A ×⇩∘ (r `⇩∘ set {c})"
by auto

lemma vcomp_VLambda:
"(λb∈⇩∘((λa∈⇩∘A. g a) `⇩∘ A). f b) ∘⇩∘ (λa∈⇩∘A. g a) = (λa∈⇩∘A. (f ∘ g) a)"
using VLambda_iff1 by (auto intro!: vsubset_antisym)+

text‹Further special properties.›

lemma vimage_vsubset:
assumes "r ⊆⇩∘ A ×⇩∘ B"
shows "r `⇩∘ C ⊆⇩∘ B"
using assms by auto

lemma vimage_vdomain_vsubset: "r `⇩∘ A ⊆⇩∘ r `⇩∘ 𝒟⇩∘ r" by auto

lemma vdomain_vsubset_VUnion2: "𝒟⇩∘ r ⊆⇩∘ ⋃⇩∘(⋃⇩∘r)"
proof(intro vsubsetI)
fix x assume "x ∈⇩∘ 𝒟⇩∘ r"
then obtain y where "⟨x, y⟩ ∈⇩∘ r" by auto
then have "set {set {x}, set {x, y}} ∈⇩∘ r" unfolding vpair_def by auto
with insert_commute have xy_Ur: "set {x, y} ∈⇩∘ ⋃⇩∘r"
unfolding VUnion_iff by auto
define Ur where "Ur = ⋃⇩∘r"
from xy_Ur show "x ∈⇩∘ ⋃⇩∘(⋃⇩∘r)"
unfolding Ur_def[symmetric] by (auto dest: VUnionI)
qed

lemma vrange_vsubset_VUnion2: "ℛ⇩∘ r ⊆⇩∘ ⋃⇩∘(⋃⇩∘r)"
proof(intro vsubsetI)
fix y assume "y ∈⇩∘ ℛ⇩∘ r"
then obtain x where "⟨x, y⟩ ∈⇩∘ r" by auto
then have "set {set {x}, set {x, y}} ∈⇩∘ r" unfolding vpair_def by auto
with insert_commute have xy_Ur: "set {x, y} ∈⇩∘ ⋃⇩∘r"
unfolding VUnion_iff by auto
define Ur where "Ur = ⋃⇩∘r"
from xy_Ur show "y ∈⇩∘ ⋃⇩∘(⋃⇩∘r)"
unfolding Ur_def[symmetric] by (auto dest: VUnionI)
qed

lemma vfield_vsubset_VUnion2: "ℱ⇩∘ r ⊆⇩∘ ⋃⇩∘(⋃⇩∘r)"
using vdomain_vsubset_VUnion2 vrange_vsubset_VUnion2
by (auto simp: app_vfield_def)

subsubsection‹Inverse image›

definition invimage :: "V ⇒ V"
where "invimage D = VLambda D (λ⟨r, A⟩. r¯⇩∘ `⇩∘ A)"

abbreviation app_invimage :: "V ⇒ V ⇒ V" (infixr ‹-`⇩∘› 90)
where "r -`⇩∘ A ≡ invimage (set {⟨r, A⟩}) ⦇⟨r, A⟩⦈"

lemma app_invimage_def: "r -`⇩∘ A = r¯⇩∘ `⇩∘ A" unfolding invimage_def by simp

lemma invimage_small[simp]: "small {a. ∃b∈⇩∘A. ⟨a, b⟩ ∈⇩∘ r}"
proof-
have ss: "{a. ∃b∈⇩∘A. ⟨a, b⟩ ∈⇩∘ r} ⊆ vfst ` elts r"
using image_iff by fastforce
have small: "small (vfst ` elts r)" by (rule replacement) simp
show ?thesis by (rule smaller_than_small, rule small, rule ss)
qed

text‹Rules.›

lemma invimageI[intro!]:
assumes "⟨r, A⟩ ∈⇩∘ D"
shows "⟨⟨r, A⟩, r -`⇩∘ A⟩ ∈⇩∘ invimage D"
using assms unfolding invimage_def by (simp add: VLambda_iff2)

lemma invimageD[dest]:
assumes "⟨⟨r, A⟩, s⟩ ∈⇩∘ invimage D"
shows "⟨r, A⟩ ∈⇩∘ D" and "s = r -`⇩∘ A"
using assms unfolding invimage_def by auto

lemma invimageE[elim]:
assumes "x ∈⇩∘ invimage D" and "D ⊆⇩∘ R ×⇩∘ X"
obtains r A where "x = ⟨⟨r, A⟩, r -`⇩∘ A⟩" and "r ∈⇩∘ R" and "A ∈⇩∘ X"
using assms unfolding invimage_def by auto

lemma app_invimageI[intro]:
assumes "⟨a, b⟩ ∈⇩∘ r" and "b ∈⇩∘ A"
shows "a ∈⇩∘ r -`⇩∘ A"
using assms invimage_def by auto

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

lemma app_invimageE[elim]:
assumes "a ∈⇩∘ r -`⇩∘ A"
obtains b where "⟨a, b⟩ ∈⇩∘ r" and "b ∈⇩∘ A"
using assms unfolding invimage_def by auto

lemma app_invimageI1:
assumes "a ∈⇩∘ 𝒟⇩∘ (r ↾⇧r⇩∘ A)"
shows "a ∈⇩∘ r -`⇩∘ A"
using assms unfolding vimage_def
by (simp add: invimage_def app_vimageI1 vlrestriction_vconverse)

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

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

lemma app_invimageI2:
assumes "a ∈⇩∘ r¯⇩∘ `⇩∘ A"
shows "a ∈⇩∘ r -`⇩∘ A"
using assms unfolding invimage_def by simp

lemma app_invimageD2:
assumes "a ∈⇩∘ r -`⇩∘ A"
shows "a ∈⇩∘ r¯⇩∘ `⇩∘ A"
using assms unfolding invimage_def by simp

lemma app_invimageE2:
assumes "a ∈⇩∘ r -`⇩∘ A" and "a ∈⇩∘ r¯⇩∘ `⇩∘ A ⟹ P"
shows P
unfolding vimage_def by (simp add: assms app_invimageD2)

lemma invimage_iff: "a ∈⇩∘ r -`⇩∘ A ⟷ (∃b∈⇩∘A. ⟨a, b⟩ ∈⇩∘ r)" by auto

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

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

text‹Set operations.›

lemma invimage_vempty[simp]: "0 -`⇩∘ A = 0" by (auto intro!: vsubset_antisym)

lemma invimage_of_vempty[simp]: "r -`⇩∘ 0 = 0" by (auto intro!: vsubset_antisym)

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

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

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

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

lemma invimage_vinsert: "r -`⇩∘ (vinsert a A) = r -`⇩∘ set {a} ∪⇩∘ r -`⇩∘ A"
by (auto intro!: vsubset_antisym)

lemma invimage_vunion_left: "(r ∪⇩∘ s) -`⇩∘ A = r -`⇩∘ A ∪⇩∘ s -`⇩∘ A"
by (auto intro!: vsubset_antisym)

lemma invimage_vunion_right: "r -`⇩∘ (A ∪⇩∘ B) = r -`⇩∘ A ∪⇩∘ r -`⇩∘ B"
by (auto intro!: vsubset_antisym)

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

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

text‹Special properties.›

lemma invimage_set_def: "r -`⇩∘ A = set {a. ∃b∈⇩∘A. ⟨a, b⟩ ∈⇩∘ r}" by fastforce

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

lemma invimage_vrange[simp]: "r -`⇩∘ ℛ⇩∘ r = 𝒟⇩∘ r"
unfolding invimage_def by (auto intro!: vsubset_antisym)

lemma invimage_vrange_vsubset[simp]:
assumes "ℛ⇩∘ r ⊆⇩∘ B"
shows "r -`⇩∘ B = 𝒟⇩∘ r"
using assms unfolding app_invimage_def by (blast intro!: vsubset_antisym)

text‹Connections.›

lemma invimage_vid_on[simp]: "vid_on A -`⇩∘ B = A ∩⇩∘ B"
by (auto intro!: vsubset_antisym)

lemma invimage_vconst_on_vsubset_vdomain[simp]: "vconst_on A c -`⇩∘ B ⊆⇩∘ A"
unfolding invimage_def by auto

lemma invimage_vconst_on_ne[simp]:
assumes "c ∈⇩∘ B"
shows "vconst_on A c -`⇩∘ B = A"
by (simp add: assms invimage_eq_vdomain_vrestriction vrrestriction_vconst_on)

lemma invimage_vconst_on_vempty[simp]:
assumes "c ∉⇩∘ B"
shows "vconst_on A c -`⇩∘ B = 0"
using assms by auto

lemma invimage_vcomp: "(r ∘⇩∘ s) -`⇩∘ x = s -`⇩∘ (r -`⇩∘ x) "
by (simp add: invimage_def vconverse_vcomp vcomp_vimage)

lemma invimage_vconverse[simp]: "r¯⇩∘ -`⇩∘ A = r `⇩∘ A"
by (auto intro!: vsubset_antisym)

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

lemma invimage_vrrestriction[simp]: "(r ↾⇧r⇩∘ A) -`⇩∘ B = (r -`⇩∘ (A ∩⇩∘ B))"
by (auto intro!: vsubset_antisym)

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

text‹Previous connections.›

lemma vcomp_vconst_on_rel_vtimes: "vconst_on A c ∘⇩∘ r = (r -`⇩∘ A) ×⇩∘ set {c}"
proof(intro vsubset_antisym vsubsetI)
fix x assume "x ∈⇩∘ r -`⇩∘ A ×⇩∘ set {c}"
then obtain a where x_def: "x = ⟨a, c⟩" and "a ∈⇩∘ r -`⇩∘ A" by auto
then obtain b where ab: "⟨a, b⟩ ∈⇩∘ r" and "b ∈⇩∘ A" using invimage_iff by auto
with ‹b ∈⇩∘ A› show "x ∈⇩∘ vconst_on A c ∘⇩∘ r" unfolding x_def by auto
qed auto

lemma vdomain_vcomp[simp]: "𝒟⇩∘ (r ∘⇩∘ s) = s -`⇩∘ 𝒟⇩∘ r" by blast

lemma vrange_vcomp[simp]: "ℛ⇩∘ (r ∘⇩∘ s) = r `⇩∘ ℛ⇩∘ s" by blast

lemma vdomain_vcomp_vsubset:
assumes "ℛ⇩∘ s ⊆⇩∘ 𝒟⇩∘ r"
shows "𝒟⇩∘ (r ∘⇩∘ s) = 𝒟⇩∘ s"
using assms by simp

subsection‹Classification of relations›

subsubsection‹Binary relation›

locale vbrelation =
fixes r :: V
assumes vbrelation: "vpairs r = r"

text‹Rules.›

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

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

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

lemmas vbrelationI[intro!] = vbrelation.intro
lemmas vbrelationD[dest!] = vbrelation.vbrelation

lemma vbrelationE[elim!]:
assumes "vbrelation r" and "(vpairs r = r) ⟹ P"
shows P
using assms unfolding vbrelation_def by auto

lemma vbrelationE1[elim]:
assumes "vbrelation r" and "x ∈⇩∘ r"
obtains a b where "x = ⟨a, b⟩"
using assms by auto

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

lemma (in vbrelation) vbrelation_vinE:
assumes "x ∈⇩∘ r"
obtains a b where "x = ⟨a, b⟩" and "a ∈⇩∘ 𝒟⇩∘ r" and "b ∈⇩∘ ℛ⇩∘ r"
using assms vbrelation_axioms by blast

text‹Set operations.›

lemma vbrelation_vsubset:
assumes "vbrelation s" and "r ⊆⇩∘ s"
shows "vbrelation r"
using assms by auto

lemma vbrelation_vinsert[simp]: "vbrelation (vinsert ⟨a, b⟩ r) ⟷ vbrelation r"
by auto

lemma (in vbrelation) vbrelation_vinsertI[intro, simp]:
"vbrelation (vinsert ⟨a, b⟩ r)"
using vbrelation_axioms by auto

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

lemma vbrelation_vunion: "vbrelation (r ∪⇩∘ s) ⟷ vbrelation r ∧ vbrelation s"
by auto

lemma vbrelation_vunionI:
assumes "vbrelation r" and "vbrelation s"
shows "vbrelation (r ∪⇩∘ s)"
using assms by auto

lemma vbrelation_vunionD[dest]:
assumes "```