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

lemma VLambdaD[dest!]: 
  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)"
      by (simp add: vpairs_iff_elts)
    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}" 
  by (simp add: app_vfield_def vinsert_set_insert_eq)

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)"
  by (simp add: vimage_VLambda_vrange)

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 "vbrelation (r ∪∘ s)"
  shows "vbrelation r" and "vbrelation s"
  using assms by auto

lemma (in vbrelation) vbrelation_vintersectionI: "vbrelation (r ∩∘ s)"
  using vbrelation_axioms by auto

lemma (in vbrelation) vbrelation_vdiffI: "vbrelation (r -∘ s)"
  using vbrelation_axioms by auto


text‹Connections.›

lemma vbrelation_vempty: "vbrelation 0" by auto

lemma vbrelation_vsingleton: "vbrelation (set {⟨a, b⟩})" by auto

lemma vbrelation_vdoubleton: "vbrelation (set {⟨a, b⟩, ⟨c, d⟩})" by auto

lemma vbrelation_vid_on[simp]: "vbrelation (vid_on A)" by auto

lemma vbrelation_vconst_on[simp]: "vbrelation (vconst_on A c)" by auto

lemma vbrelation_VLambda[simp]: "vbrelation (VLambda A f)"
  unfolding VLambda_def by (intro vbrelationI) auto
  
global_interpretation rel_VLambda: vbrelation ‹VLambda U f› 
  by (rule vbrelation_VLambda)

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

lemma (in vbrelation) vbrelation_vconverse: "vbrelation (r¯∘)"
  using vbrelation_axioms by clarsimp

lemma vbrelation_vlrestriction[intro, simp]: "vbrelation (r ↾l∘ A)" by auto

lemma vbrelation_vrrestriction[intro, simp]: "vbrelation (r ↾r∘ A)" by auto

lemma vbrelation_vrestriction[intro, simp]: "vbrelation (r ↾∘ A)" by auto


text‹Previous connections.›

lemma (in vbrelation) vconverse_vconverse[simp]: "(r¯∘)¯∘ = r"
  using vbrelation_axioms by auto

lemma vconverse_mono[simp]: 
  assumes "vbrelation r" and "vbrelation s"
  shows "r¯∘ ⊆∘ s¯∘ ⟷ r ⊆∘ s"
  using assms by (force intro: vconverse_vunion)+

lemma vconverse_inject[simp]: 
  assumes "vbrelation r" and "vbrelation s"
  shows "r¯∘ = s¯∘ ⟷ r = s"
  using assms by fast

lemma (in vbrelation) vconverse_vsubset_swap_2: 
  assumes "r¯∘ ⊆∘ s"
  shows "r ⊆∘ s¯∘" 
  using assms vbrelation_axioms by auto

lemma (in vbrelation) vlrestriction_vdomain[simp]: "r ↾l∘ 𝒟∘ r = r"
  using vbrelation_axioms by (elim vbrelationE) auto

lemma (in vbrelation) vrrestriction_vrange[simp]: "r ↾r∘ ℛ∘ r = r"
  using vbrelation_axioms by (elim vbrelationE) auto


text‹Special properties.›

lemma brel_vsubset_vtimes:
  "vbrelation r ⟷ r ⊆∘ set (vfst ` elts r) ×∘ set (vsnd ` elts r)"
  by force

lemma vsubset_vtimes_vbrelation: 
  assumes "r ⊆∘ A ×∘ B"
  shows "vbrelation r" 
  using assms by auto

lemma (in vbrelation) vbrelation_vintersection_vdomain:
  assumes "vdisjnt (𝒟∘ r) (𝒟∘ s)"
  shows "vdisjnt r s"
proof(intro vsubset_antisym vsubsetI)
  fix x assume "x ∈∘ r ∩∘ s"
  then obtain a b where "⟨a, b⟩ ∈∘ r ∩∘ s"
    by (metis vbrelationE1 vbrelation_vintersectionI)
  with assms show "x ∈∘ 0" by auto
qed simp

lemma (in vbrelation) vbrelation_vintersection_vrange:
  assumes "vdisjnt (ℛ∘ r) (ℛ∘ s)"
  shows "vdisjnt r s"
proof(intro vsubset_antisym vsubsetI)
  fix x assume "x ∈∘ r ∩∘ s"
  then obtain a b where "⟨a, b⟩ ∈∘ r ∩∘ s"
    by (metis vbrelationE1 vbrelation_vintersectionI)
  with assms show "x ∈∘ 0" by auto
qed simp

lemma (in vbrelation) vbrelation_vintersection_vfield:
  assumes "vdisjnt (vfield r) (vfield s)"
  shows "vdisjnt r s"
proof(intro vsubset_antisym vsubsetI)
  fix x assume "x ∈∘ r ∩∘ s"
  then obtain a b where "⟨a, b⟩ ∈∘ r ∩∘ s"
    by (metis vbrelationE1 vbrelation_vintersectionI)
  with assms show "x ∈∘ 0" by auto
qed auto

lemma (in vbrelation) vdomain_vrange_vtimes: "r ⊆∘ 𝒟∘ r ×∘ ℛ∘ r"
  using vbrelation by auto

lemma (in vbrelation) vbrelation_vsubset_vtimes:
  assumes "𝒟∘ r ⊆∘ A" and "ℛ∘ r ⊆∘ B"
  shows "r ⊆∘ A ×∘ B"
proof(intro vsubsetI)
  fix x assume prems: "x ∈∘ r"
  with vbrelation obtain a b where x_def: "x = ⟨a, b⟩" by auto
  from prems have a: "a ∈∘ 𝒟∘ r" and b: "b ∈∘ ℛ∘ r" unfolding x_def by auto
  with assms have "a ∈∘ A" and "b ∈∘ B" by auto
  then show "x ∈∘ A ×∘ B" unfolding x_def by simp
qed

lemma (in vbrelation) vlrestriction_vsubset_vrange[intro, simp]:
  assumes "𝒟∘ r ⊆∘ A"
  shows "r ↾l∘ A = r"
proof(intro vsubset_antisym)
  show "r ⊆∘ r ↾l∘ A"
    by (rule vlrestriction_mono[OF assms, of r, unfolded vlrestriction_vdomain])
qed auto

lemma (in vbrelation) vrrestriction_vsubset_vrange[intro, simp]:
  assumes "ℛ∘ r ⊆∘ B"
  shows "r ↾r∘ B = r"
proof(intro vsubset_antisym)
  show "r ⊆∘ r ↾r∘ B"
    by (rule vrrestriction_mono[OF assms, of r, unfolded vrrestriction_vrange])
qed auto

lemma (in vbrelation) vbrelation_vcomp_vid_on_left[simp]:
  assumes "ℛ∘ r ⊆∘ A"
  shows "vid_on A ∘∘ r = r"
  using assms by auto

lemma (in vbrelation) vbrelation_vcomp_vid_on_right[simp]:
  assumes "𝒟∘ r ⊆∘ A"
  shows "r ∘∘ vid_on A = r"
  using assms by auto


text‹Alternative forms of existing results.›

lemmas [intro, simp] = vbrelation.vconverse_vconverse
  and [intro, simp] = vbrelation.vlrestriction_vsubset_vrange
  and [intro, simp] = vbrelation.vrrestriction_vsubset_vrange



subsubsection‹Simple single-valued relation›

locale vsv = vbrelation r for r + 
  assumes vsv: "⟦ ⟨a, b⟩ ∈∘ r; ⟨a, c⟩ ∈∘ r ⟧ ⟹ b = c"


text‹Rules.›

lemmas (in vsv) [intro] = vsv_axioms

mk_ide rf vsv_def[unfolded vsv_axioms_def]
  |intro vsvI[intro]| 
  |dest vsvD[dest]|
  |elim vsvE[elim]|


text‹Set operations.›

lemma (in vsv) vsv_vinsert[simp]:
  assumes "a ∉∘ 𝒟∘ r"
  shows "vsv (vinsert ⟨a, b⟩ r)" 
  using assms vsv_axioms by blast

lemma vsv_vinsertD:
  assumes "vsv (vinsert x r)"
  shows "vsv r"
  using assms by (intro vsvI) auto

lemma vsv_vunion[intro, simp]:
  assumes "vsv r" and "vsv s" and "vdisjnt (𝒟∘ r) (𝒟∘ s)"
  shows "vsv (r ∪∘ s)"
proof
  from assms have F: "⟦ ⟨a, b⟩ ∈∘ r; ⟨a, c⟩ ∈∘ s ⟧ ⟹ False" for a b c
    using elts_0 by blast
  fix a b c assume "⟨a, b⟩ ∈∘ r ∪∘ s" and "⟨a, c⟩ ∈∘ r ∪∘ s" 
  then consider 
      "⟨a, b⟩ ∈∘ r ∧ ⟨a, c⟩ ∈∘ r"
    | "⟨a, b⟩ ∈∘ r ∧ ⟨a, c⟩ ∈∘ s"
    | "⟨a, b⟩ ∈∘ s ∧ ⟨a, c⟩ ∈∘ r"
    | "⟨a, b⟩ ∈∘ s ∧ ⟨a, c⟩ ∈∘ s"
    by blast
  then show "b = c" using assms by cases auto
qed (use assms in auto) 

lemma (in vsv) vsv_vintersection[intro, simp]: "vsv (r ∩∘ s)" 
  using vsv_axioms by blast

lemma (in vsv) vsv_vdiff[intro, simp]: "vsv (r -∘ s)" using vsv_axioms by blast


text‹Connections.›

lemma vsv_vempty[simp]: "vsv 0" by auto

lemma vsv_vsingleton[simp]: "vsv (set {⟨a, b⟩})" by auto

global_interpretation rel_vsingleton: vsv ‹set {⟨a, b⟩}›
  by (rule vsv_vsingleton)

lemma vsv_vdoubleton: 
  assumes "a ≠ c"
  shows "vsv (set {⟨a, b⟩, ⟨c, d⟩})" 
  using assms by (auto simp: vinsert_set_insert_eq)

lemma vsv_vid_on[simp]: "vsv (vid_on A)" by auto

lemma vsv_vconst_on[simp]: "vsv (vconst_on A c)" by auto

lemma vsv_VLambda[simp]: "vsv (λa∈∘A. f a)" by auto

global_interpretation rel_VLambda: vsv ‹(λa∈∘A. f a)›
  unfolding VLambda_def by (intro vsvI) auto

lemma vsv_vcomp: 
  assumes "vsv r" and "vsv s"
  shows "vsv (r ∘∘ s)" 
  using assms
  by (intro vsvI; elim vsvE) (simp add: vbrelation_vcomp, metis vcompD)

lemma (in vsv) vsv_vlrestriction[intro, simp]: "vsv (r ↾l∘ A)" 
  using vsv_axioms by blast

lemma (in vsv) vsv_vrrestriction[intro, simp]: "vsv (r ↾r∘ A)" 
  using vsv_axioms by blast

lemma (in vsv) vsv_vrestriction[intro, simp]: "vsv (r ↾∘ A)" 
  using vsv_axioms by blast


text‹Special properties.›

lemma small_vsv[simp]: "small {f. vsv f ∧ 𝒟∘ f = A ∧ ℛ∘ f ⊆∘ B}"
proof-
  have "small {f. f ⊆∘ A ×∘ B}" by (auto simp: small_iff)
  moreover have "{f. vsv f ∧ 𝒟∘ f = A ∧ ℛ∘ f ⊆∘ B} ⊆ {f. f ⊆∘ A ×∘ B}"
    by auto
  ultimately show "small {f. vsv f ∧ 𝒟∘ f = A ∧ ℛ∘ f ⊆∘ B}" 
    by (auto simp: smaller_than_small)
qed

context vsv
begin

lemma vsv_ex1: 
  assumes "a ∈∘ 𝒟∘ r"
  shows "∃!b. ⟨a, b⟩ ∈∘ r"
  using vsv_axioms assms by auto

lemma vsv_ex1_app1: 
  assumes "a ∈∘ 𝒟∘ r"
  shows "b = r⦇a⦈ ⟷ ⟨a, b⟩ ∈∘ r"
proof 
  assume b_def: "b = r⦇a⦈" show "⟨a, b⟩ ∈∘ r" 
    unfolding app_def b_def by (rule theI') (rule vsv_ex1[OF assms])
next
  assume [simp]: "⟨a, b⟩ ∈∘ r"
  from assms vsv_axioms vsvD have THE_b: "(THE y. ⟨a, y⟩ ∈∘ r) = b" by auto
  show "b = r⦇a⦈" unfolding app_def THE_b[symmetric] by (rule refl)  
qed

lemma vsv_ex1_app2[iff]: 
  assumes "a ∈∘ 𝒟∘ r"
  shows "r⦇a⦈ = b ⟷ ⟨a, b⟩ ∈∘ r"
  using vsv_ex1_app1[OF assms] by auto

lemma vsv_appI[intro, simp]: 
  assumes "⟨a, b⟩ ∈∘ r"
  shows "r⦇a⦈ = b" 
  using assms by (subgoal_tac ‹a ∈∘ 𝒟∘ r›) auto

lemma vsv_appE:
  assumes "r⦇a⦈ = b" and "a ∈∘ 𝒟∘ r" and "⟨a, b⟩ ∈∘ r ⟹ P"
  shows P
  using assms vsv_ex1_app1 by blast

lemma vdomain_vrange_is_vempty: "𝒟∘ r = 0 ⟷ ℛ∘ r = 0" by fastforce

lemma vsv_vrange_vempty: 
  assumes "ℛ∘ r = 0"
  shows "r = 0"
  using assms vdomain_vrange_is_vempty vlrestriction_vdomain by auto

lemma vsv_vdomain_vempty_vrange_vempty:
  assumes "𝒟∘ r ≠ 0"
  shows "ℛ∘ r ≠ 0"
  using assms by fastforce

lemma vsv_vdomain_vsingleton_vrange_vsingleton:
  assumes "𝒟∘ r = set {a}"
  obtains b where "ℛ∘ r = set {b}"
proof-
  from assms obtain b where ab: "⟨a, b⟩ ∈∘ r" by auto
  then have "⟨a, c⟩ ∈∘ r ⟹ c = b" for c by (auto simp: vsv)
  moreover with assms have "⟨b, c⟩ ∈∘ r ⟹ c = a" for c by force
  ultimately have "⟨c, d⟩ ∈∘ r ⟹ d = b" for c d
    by (metis app_vdomainI assms vsingletonD)
  with ab have "ℛ∘ r = set {b}" by blast
  with that show ?thesis by simp
qed

lemma vsv_vsubset_vimageE:
  assumes "B ⊆∘ r `∘ A"
  obtains C where "C ⊆∘ A" and "B = r `∘ C"
proof-
  define C where C_def: "C = (r¯∘ `∘ B) ∩∘ A"
  then have "C ⊆∘ A" by auto
  moreover have "B = r `∘ C"
    unfolding C_def
  proof(intro vsubset_antisym vsubsetI)
    fix b assume "b ∈∘ B"
    with assms obtain a where "a ∈∘ A" and "⟨a, b⟩ ∈∘ r" 
      using app_vimageE vsubsetD by metis
    then have "a ∈∘ r¯∘ `∘ B ∩∘ A" by (auto simp: ‹b ∈∘ B›)
    then show "b ∈∘ r `∘ (r¯∘ `∘ B ∩∘ A)" by (auto intro: ‹⟨a, b⟩ ∈∘ r›)
  qed (use vsv_axioms in auto)
  ultimately show ?thesis using that by auto
qed

lemma vsv_vimage_eqI[intro]:
  assumes "a ∈∘ 𝒟∘ r" and "r⦇a⦈ = b" and "a ∈∘ A"
  shows "b ∈∘ r `∘ A"
  using assms(2)[unfolded vsv_ex1_app2[OF assms(1)]] assms(3) by auto

lemma vsv_vimageI1: 
  assumes "a ∈∘ 𝒟∘ r" and "a ∈∘ A" 
  shows "r⦇a⦈ ∈∘ r `∘ A"
  using assms by (simp add: vsv_vimage_eqI)

lemma vsv_vimageI2: 
  assumes "a ∈∘ 𝒟∘ r"
  shows "r⦇a⦈ ∈∘ ℛ∘ r"
  using assms by (blast dest: vsv_ex1_app1)

lemma vsv_vimageI2':
  assumes "b = r⦇a⦈" and "a ∈∘ 𝒟∘ r"
  shows "b ∈∘ ℛ∘ r"
  using assms by (blast dest: vsv_ex1_app1)

lemma vsv_value: 
  assumes "a ∈∘ 𝒟∘ r"
  obtains b where "r⦇a⦈ = b" and "b ∈∘ ℛ∘ r"
  using assms by (blast dest: vsv_ex1_app1)

lemma vsv_vimageE:
  assumes "b ∈∘ r `∘ A"
  obtains x where "r⦇x⦈ = b" and "x ∈∘ A"
  using assms vsv_axioms vsv_ex1_app2 by blast

lemma vsv_vimage_iff: "b ∈∘ r `∘ A ⟷ (∃a. a ∈∘ A ∧ a ∈∘ 𝒟∘ r ∧ r⦇a⦈ = b)"
  using vsv_axioms by (blast intro: vsv_ex1_app1[THEN iffD1])+

lemma vsv_vimage_vsingleton:
  assumes "a ∈∘ 𝒟∘ r"
  shows "r `∘ set {a} = set {r⦇a⦈}"
  using assms by force

lemma vsv_vimage_vsubsetI: 
  assumes "⋀a. ⟦ a ∈∘ A; a ∈∘ 𝒟∘ r ⟧ ⟹ r⦇a⦈ ∈∘ B" 
  shows "r `∘ A ⊆∘ B"
  using assms by (metis vsv_vimage_iff vsubsetI)

lemma vsv_image_vsubset_iff: 
  "r `∘ A ⊆∘ B ⟷ (∀a∈∘A. a ∈∘ 𝒟∘ r ⟶ r⦇a⦈ ∈∘ B)"
  by (auto simp: vsv_vimage_iff)

lemma vsv_vimage_vinsert:
  assumes "a ∈∘ 𝒟∘ r"
  shows "r `∘ vinsert a A = vinsert (r⦇a⦈) (r `∘ A)"
  using assms vsv_vimage_iff by (intro vsubset_antisym vsubsetI) auto  

lemma vsv_vinsert_vimage[intro, simp]: 
  assumes "a ∈∘ 𝒟∘ r" and "a ∈∘ A" 
  shows "vinsert (r⦇a⦈) (r `∘ A) = r `∘ A"
  using assms by auto

lemma vsv_is_VLambda[simp]: "(λx∈∘𝒟∘ r. r⦇x⦈) = r"
  using vbrelation 
  by (auto simp: app_vdomainI VLambda_iff2 intro!: vsubset_antisym)

lemma vsv_is_VLambda_on_vlrestriction[intro, simp]: 
  assumes "A ⊆∘ 𝒟∘ r"
  shows "(λx∈∘A. r⦇x⦈) = r ↾l∘ A"
  using assms by (force simp: VLambda_iff2)+

lemma pairwise_vimageI:
  assumes "⋀x y. 
    ⟦ x ∈∘ 𝒟∘ r; y ∈∘ 𝒟∘ r; x ≠ y; r⦇x⦈ ≠ r⦇y⦈ ⟧ ⟹ P (r⦇x⦈) (r⦇y⦈)"
  shows "vpairwise P (ℛ∘ r)"
  by (intro vpairwiseI) (metis assms app_vdomainI app_vrangeE vsv_appI)

lemma vsv_vrange_vsubset:
  assumes "⋀x. x ∈∘ 𝒟∘ r ⟹ r⦇x⦈ ∈∘ A"
  shows "ℛ∘ r ⊆∘ A"
  using assms by fastforce

lemma vsv_vlrestriction_vinsert:
  assumes "a ∈∘ 𝒟∘ r"
  shows "r ↾l∘ vinsert a A = vinsert ⟨a, r⦇a⦈⟩ (r ↾l∘ A)"  
  using assms by (auto intro!: vsubset_antisym)

end

lemma vsv_eqI: 
  assumes "vsv r" 
    and "vsv s"
    and "𝒟∘ r = 𝒟∘ s" 
    and "⋀a. a ∈∘ 𝒟∘ r ⟹ r⦇a⦈ = s⦇a⦈"
  shows "r = s"
proof(intro vsubset_antisym vsubsetI)
  interpret r: vsv r by (rule assms(1))
  interpret s: vsv s by (rule assms(2))
  fix x assume "x ∈∘ r"
  then obtain a b where x_def[simp]: "x = ⟨a, b⟩" and "a ∈∘ 𝒟∘ r" 
    by (elim r.vbrelation_vinE)
  with ‹x ∈∘ r› have "r⦇a⦈ = b" by simp
  with assms ‹a ∈∘ 𝒟∘ r› show "x ∈∘ s" by fastforce
next
  interpret r: vsv r by (rule assms(1))
  interpret s: vsv s by (rule assms(2))
  fix x assume "x ∈∘ s"
  with assms(2) obtain a b where x_def[simp]: "x = ⟨a, b⟩" and "a ∈∘ 𝒟∘ s" 
    by (elim vsvE) blast
  with assms ‹x ∈∘ s› have "s⦇a⦈ = b" by blast
  with assms ‹a ∈∘ 𝒟∘ s› show "x ∈∘ r" by fastforce
qed

lemma (in vsv) vsv_VLambda_cong: 
  assumes "⋀a. a ∈∘ 𝒟∘ r ⟹ r⦇a⦈ = f a"
  shows "(λa∈∘𝒟∘ r. f a) = r"
proof(rule vsv_eqI[symmetric])
  show "𝒟∘ r = 𝒟∘ (VLambda (𝒟∘ r) f)" by simp
  fix a assume a: "a ∈∘ 𝒟∘ r"
  then show "r⦇a⦈ = VLambda (𝒟∘ r) f ⦇a⦈" using assms(1)[OF a] by auto
qed auto

lemma Axiom_of_Choice:
  obtains f where "⋀x. x ∈∘ A ⟹ x ≠ 0 ⟹ f⦇x⦈ ∈∘ x" and "vsv f"
proof-
  obtain f where f: "x ∈∘ A ⟹ x ≠ 0 ⟹ f⦇x⦈ ∈∘ x" for x
    by (metis beta vemptyE)
  define f' where "f' = (λx∈∘A. f⦇x⦈)"
  have "x ∈∘ A ⟹ x ≠ 0 ⟹ f'⦇x⦈ ∈∘ x" for x
    unfolding f'_def using f by simp
  moreover have "vsv f'" unfolding f'_def by simp
  ultimately show ?thesis using that by auto
qed

lemma VLambda_eqI:
  assumes "X = Y" and "⋀x. x ∈∘ X ⟹ f x = g x"
  shows "(λx∈∘X. f x) = (λy∈∘Y. g y)"
proof(rule vsv_eqI, unfold vdomain_VLambda; (intro assms(1) vsv_VLambda)?)
  fix x assume "x ∈∘ X"
  with assms show "VLambda X f⦇x⦈ = VLambda Y g⦇x⦈" by simp
qed

lemma VLambda_vsingleton_def: "(λi∈∘set {j}. f i) = (λi∈∘set {j}. f j)" by auto


text‹Alternative forms of the available results.›

lemmas [iff] = vsv.vsv_ex1_app2
  and [intro, simp] = vsv.vsv_appI
  and [elim] = vsv.vsv_appE
  and [intro] = vsv.vsv_vimage_eqI
  and [simp] = vsv.vsv_vinsert_vimage
  and [intro] = vsv.vsv_is_VLambda_on_vlrestriction
  and [simp] = vsv.vsv_is_VLambda
  and [intro, simp] = vsv.vsv_vintersection
  and [intro, simp] = vsv.vsv_vdiff
  and [intro, simp] = vsv.vsv_vlrestriction
  and [intro, simp] = vsv.vsv_vrrestriction
  and [intro, simp] = vsv.vsv_vrestriction


subsubsection‹Specialization of existing properties to single-valued relations.›


text‹Identity relation.›

lemma vid_on_eq_atI[intro, simp]: 
  assumes "a = b" and "a ∈∘ A"
  shows "vid_on A ⦇a⦈ = b"
  using assms by auto

lemma vid_on_atI[intro, simp]: 
  assumes "a ∈∘ A"
  shows "vid_on A ⦇a⦈ = a"
  using assms by auto

lemma vid_on_at_iff[intro, simp]:
  assumes "a ∈∘ A"
  shows "vid_on A ⦇a⦈ = b ⟷ a = b" 
  using assms by auto


text‹Constant function.›

lemma vconst_on_atI[simp]: 
  assumes "a ∈∘ A"
  shows "vconst_on A c ⦇a⦈ = c"
  using assms by auto


text‹Composition.›

lemma vcomp_atI[intro, simp]: 
  assumes "vsv r" 
    and "vsv s" 
    and "a ∈∘ 𝒟∘ r" 
    and "b ∈∘ 𝒟∘ s" 
    and "s⦇b⦈ = c" 
    and "r⦇a⦈ = b" 
  shows "(s ∘∘ r)⦇a⦈ = c"
  using assms by (auto simp: app_invimageI intro!: vsv_vcomp)

lemma vcomp_atD[dest]: 
  assumes "(s ∘∘ r)⦇a⦈ = c"
    and "vsv r" 
    and "vsv s"  
    and "a ∈∘ 𝒟∘ r" 
    and "r⦇a⦈ ∈∘ 𝒟∘ s" 
  shows "∃b. s⦇b⦈ = c ∧ r⦇a⦈ = b" 
  using assms by (metis vcomp_atI)

lemma vcomp_atE1: 
  assumes "(s ∘∘ r)⦇a⦈ = c"
    and "vsv r" 
    and "vsv s" 
    and "a ∈∘ 𝒟∘ r"
    and "r⦇a⦈ ∈∘ 𝒟∘ s"
    and "∃b. s⦇b⦈ = c ∧ r⦇a⦈ = b ⟹ P"  
  shows P
  using assms assms vcomp_atD by blast

lemma vcomp_atE[elim]:
  assumes "(s ∘∘ r)⦇a⦈ = c"
    and "vsv r" 
    and "vsv s"  
    and "a ∈∘ 𝒟∘ r" 
    and "r⦇a⦈ ∈∘ 𝒟∘ s"
  obtains b where "r⦇a⦈ = b" and "s⦇b⦈ = c"
  using assms that by (force elim!: vcomp_atE1)

lemma vsv_vcomp_at[simp]:
  assumes "vsv r" and "vsv s" and "a ∈∘ 𝒟∘ r" and "r⦇a⦈ ∈∘ 𝒟∘ s"
  shows "(s ∘∘ r)⦇a⦈ = s⦇r⦇a⦈⦈"
  using assms by auto

context vsv
begin


text‹Converse relation.›

lemma vconverse_atI[intro]: 
  assumes "a ∈∘ 𝒟∘ r" and "r⦇a⦈ = b" 
  shows "⟨b, a⟩ ∈∘ r¯∘"
  using assms by auto

lemma vconverse_atD[dest]: 
  assumes "⟨b, a⟩ ∈∘ r¯∘"
  shows "r⦇a⦈ = b" 
  using assms by auto

lemma vconverse_atE[elim]: 
  assumes "⟨b, a⟩ ∈∘ r¯∘" and "r⦇a⦈ = b ⟹ P" 
  shows P
  using assms by auto

lemma vconverse_iff: 
  assumes "a ∈∘ 𝒟∘ r"
  shows "⟨b, a⟩ ∈∘ r¯∘ ⟷ r⦇a⦈ = b" 
  using assms by auto


text‹Left restriction.›

interpretation vlrestriction: vsv ‹r ↾l∘ A› by (rule vsv_vlrestriction)

lemma vlrestriction_atI[intro, simp]: 
  assumes "a ∈∘ 𝒟∘ r" and "a ∈∘ A" and "r⦇a⦈ = b" 
  shows "(r ↾l∘ A)⦇a⦈ = b"
  using assms by (auto simp: vdomain_vlrestriction)

lemma vlrestriction_atD[dest]: 
  assumes "(r ↾l∘ A)⦇a⦈ = b" and "a ∈∘ 𝒟∘ r" and "a ∈∘ A"
  shows "r⦇a⦈ = b"
  using assms by (auto simp: vdomain_vlrestriction)

lemma vlrestriction_atE1[elim]: 
  assumes "(r ↾l∘ A)⦇a⦈ = b" 
    and "a ∈∘ 𝒟∘ r"
    and "a ∈∘ A"
    and "r⦇a⦈ = b ⟹ P"
  shows P
  using assms vlrestrictionD by blast

lemma vlrestriction_atE2[elim]: 
  assumes "x ∈∘ r ↾l∘ A"
  obtains a b where "x = ⟨a, b⟩" and "a ∈∘ A" and "r⦇a⦈ = b"
  using assms by auto


text‹Right restriction.›

interpretation vrrestriction: vsv ‹r ↾r∘ A› by (rule vsv_vrrestriction)

lemma vrrestriction_atI[intro, simp]: 
  assumes "a ∈∘ 𝒟∘ r" and "b ∈∘ A" and "r⦇a⦈ = b" 
  shows "(r ↾r∘ A)⦇a⦈ = b" 
  using assms by (auto simp: app_vrrestrictionI)

lemma vrrestriction_atD[dest]: 
  assumes "(r ↾r∘ A)⦇a⦈ = b" and "a ∈∘ r -`∘ A"
  shows "b ∈∘ A" and "r⦇a⦈ = b"
  using assms by force+

lemma vrrestriction_atE1[elim]: 
  assumes "(r ↾r∘ A)⦇a⦈ = b" and "a ∈∘ r -`∘ A" and "r⦇a⦈ = b ⟹ P"
  shows P
  using assms by (auto simp: vrrestriction_atD(2))

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


text‹Restriction.›

interpretation vrestriction: vsv ‹r ↾∘ A› by (rule vsv_vrestriction)

lemma vlrestriction_app[intro, simp]: 
  assumes "a ∈∘ 𝒟∘ r" and "a ∈∘ A"
  shows "(r ↾l∘ A)⦇a⦈ = r⦇a⦈"
  using assms by auto

lemma vrestriction_atD[dest]:
  assumes "(r ↾∘ A)⦇a⦈ = b" and "a ∈∘ r -`∘ A" and "a ∈∘ A"
  shows "b ∈∘ A" and "r⦇a⦈ = b"
proof-
  from assms have "a ∈∘ 𝒟∘ r" by auto
  then show "r⦇a⦈ = b"  
    by 
      (
        metis 
          assms 
          app_invimageD1 
          vrrestriction.vlrestriction_atD 
          vrrestriction_atD(2) 
          vrrestriction_vlrestriction
      )
  then show "b ∈∘ A" using assms(2) by blast
qed
 
lemma vrestriction_atE1[elim]: 
  assumes "(r ↾∘ A)⦇a⦈ = b" 
    and "a ∈∘ r -`∘ A" 
    and "a ∈∘ A" 
    and "r⦇a⦈ = b ⟹ P"
  shows P
  using assms vrestriction_atD(2) by blast

lemma vrestriction_atE2[elim]:
  assumes "x ∈∘ r ↾∘ A"
  obtains a b where "x = ⟨a, b⟩" and "a ∈∘ A" and "b ∈∘ A" and "r⦇a⦈ = b"
  using assms unfolding vrestriction_def by clarsimp


text‹Domain.›

lemma vdomain_atD: 
  assumes "a ∈∘ 𝒟∘ r"
  shows "∃b∈∘ℛ∘ r. r⦇a⦈ = b" 
  using assms by (blast intro: vsv_vimageI2)

lemma vdomain_atE:
  assumes "a ∈∘ 𝒟∘ r" 
  obtains b where "b ∈∘ ℛ∘ r" and "r⦇a⦈ = b"
  using assms by auto


text‹Range.›

lemma vrange_atD: 
  assumes "b ∈∘ ℛ∘ r"
  shows "∃a∈∘𝒟∘ r. r⦇a⦈ = b" 
  using assms by auto

lemma vrange_atE:
  assumes "b ∈∘ ℛ∘ r" 
  obtains a where "a ∈∘ 𝒟∘ r" and "r⦇a⦈ = b"
  using assms by auto


text‹Image.›

lemma vimage_set_eq_at: 
  "{b. ∃a∈∘A ∩∘ 𝒟∘ r. r⦇a⦈ = b} = {b. ∃a∈∘A. ⟨a, b⟩ ∈∘ r}"
  by (rule subset_antisym; rule subsetI; unfold mem_Collect_eq) auto

lemma vimage_small[simp]: "small {b. ∃a∈∘A ∩∘ 𝒟∘ r. r⦇a⦈ = b}"
  unfolding vimage_set_eq_at by auto

lemma vimage_set_def: "r `∘ A = set {b. ∃a∈∘A ∩∘ 𝒟∘ r. r⦇a⦈ = b}"
  unfolding vimage_set_eq_at by (simp add: app_vimage_set_def)

lemma vimage_set_iff: "b ∈∘ r `∘ A ⟷ (∃a∈∘A ∩∘ 𝒟∘ r. r⦇a⦈ = b)"
  unfolding vimage_set_eq_at using vsv_vimage_iff by auto


text‹Further derived results.›

lemma vimage_image:
  assumes "A ⊆∘ 𝒟∘ r"
  shows "elts (r `∘ A) = (λx. r⦇x⦈) ` (elts A)"
  using vimage_def assms small_elts by blast

lemma vsv_vinsert_match_appI[intro, simp]:
  assumes "a ∉∘ 𝒟∘ r" 
  shows "vinsert ⟨a, b⟩ r ⦇a⦈ = b" 
  using assms vsv_axioms by simp

lemma vsv_vinsert_no_match_appI:
  assumes "a ∉∘ 𝒟∘ r" and "c ∈∘ 𝒟∘ r" and "r ⦇c⦈ = d" 
  shows "vinsert ⟨a, b⟩ r ⦇c⦈ = d" 
  using assms vsv_axioms by simp

lemma vsv_is_vconst_onI:
  assumes "𝒟∘ r = A" and "ℛ∘ r = set {a}"
  shows "r = vconst_on A a"
  unfolding assms(1)[symmetric]
proof(cases ‹𝒟∘ r = 0›)
  case True
  with assms show "r = vconst_on (𝒟∘ r) a" 
    by (auto simp: vdomain_vrange_is_vempty)
next
  case False
  show "r = vconst_on (𝒟∘ r) a"
  proof(rule vsv_eqI)
    fix a' assume prems: "a' ∈∘ 𝒟∘ r"
    then obtain b where "r⦇a'⦈ = b" and "b ∈∘ ℛ∘ r" by auto
    moreover then have "b = a" unfolding assms by simp
    ultimately show "r⦇a'⦈ = vconst_on (𝒟∘ r) a⦇a'⦈" by (simp add: prems)
  qed auto
qed

lemma vsv_vdomain_vrange_vsingleton:
  assumes "𝒟∘ r = set {a}" and "ℛ∘ r = set{b}"
  shows "r = set {⟨a, b⟩}"
  using assms vsv_is_vconst_onI by auto

end


text‹Alternative forms of existing results.›

lemmas [intro] = vsv.vconverse_atI
  and vsv_vconverse_atD[dest] = vsv.vconverse_atD[rotated]
  and vsv_vconverse_atE[elim] = vsv.vconverse_atE[rotated]
  and [intro, simp] = vsv.vlrestriction_atI
  and vsv_vlrestriction_atD[dest] = vsv.vlrestriction_atD[rotated]
  and vsv_vlrestriction_atE1[elim] = vsv.vlrestriction_atE1[rotated]
  and vsv_vlrestriction_atE2[elim] = vsv.vlrestriction_atE2[rotated]
  and [intro, simp] = vsv.vrrestriction_atI
  and vsv_vrrestriction_atD[dest] = vsv.vrrestriction_atD[rotated]
  and vsv_vrrestriction_atE1[elim] = vsv.vrrestriction_atE1[rotated]
  and vsv_vrrestriction_atE2[elim] = vsv.vrrestriction_atE2[rotated]
  and [intro, simp] = vsv.vlrestriction_app
  and vsv_vrestriction_atD[dest] = vsv.vrestriction_atD[rotated]
  and vsv_vrestriction_atE1[elim] = vsv.vrestriction_atE1[rotated]
  and vsv_vrestriction_atE2[elim] = vsv.vrestriction_atE2[rotated]
  and vsv_vdomain_atD = vsv.vdomain_atD[rotated]
  and vsv_vdomain_atE = vsv.vdomain_atE[rotated]
  and vrange_atD = vsv.vrange_atD[rotated]
  and vrange_atE = vsv.vrange_atE[rotated]
  and vsv_vinsert_match_appI[intro, simp] = vsv.vsv_vinsert_match_appI 
  and vsv_vinsert_no_match_appI[intro, simp] = 
    vsv.vsv_vinsert_no_match_appI[rotated 3]


text‹Corollaries of the alternative forms of existing results.›

lemma vsv_vlrestriction_vrange:
  assumes "vsv s" and "vsv (r ↾l∘ ℛ∘ s)"
  shows "vsv (r ∘∘ s)"
proof(rule vsvI)
  show "vbrelation (r ∘∘ s)" by auto
  fix a c c' assume "⟨a, c⟩ ∈∘ r ∘∘ s" "⟨a, c'⟩ ∈∘ r ∘∘ s"
  then obtain b and b' 
    where ab: "⟨a, b⟩ ∈∘ s" 
      and bc: "⟨b, c⟩ ∈∘ r"
      and ab': "⟨a, b'⟩ ∈∘ s" 
      and b'c': "⟨b', c'⟩ ∈∘ r"
    by clarsimp
  moreover then have "b ∈∘ ℛ∘ s" and "b' ∈∘ ℛ∘ s" by auto
  ultimately have "⟨b, c⟩ ∈∘ (r ↾l∘ ℛ∘ s)" and "⟨b', c'⟩ ∈∘ (r ↾l∘ ℛ∘ s)" by auto
  with ab ab' have "⟨a, c⟩ ∈∘ (r ↾l∘ ℛ∘ s) ∘∘ s" and "⟨a, c'⟩ ∈∘ (r ↾l∘ ℛ∘ s) ∘∘ s"
    by blast+
  moreover from assms have "vsv ((r ↾l∘ ℛ∘ s) ∘∘ s)" by (intro vsv_vcomp)
  ultimately show "c = c'" by auto
qed

lemma vsv_vunion_app_right[simp]:
  assumes "vsv r" and "vsv s" and "vdisjnt (𝒟∘ r) (𝒟∘ s)" and "x ∈∘ 𝒟∘ s"
  shows "(r ∪∘ s)⦇x⦈ = s⦇x⦈"
  using assms vsubsetD by blast  

lemma vsv_vunion_app_left[simp]:
  assumes "vsv r" and "vsv s" and "vdisjnt (𝒟∘ r) (𝒟∘ s)" and "x ∈∘ 𝒟∘ r"
  shows "(r ∪∘ s)⦇x⦈ = r⦇x⦈"
  using assms vsubsetD by blast  


subsubsection‹One-to-one relation›

locale v11 = vsv r for r +
  assumes vsv_vconverse: "vsv (r¯∘)"


text‹Rules.›

lemmas (in v11) [intro] = v11_axioms

mk_ide rf v11_def[unfolded v11_axioms_def]
  |intro v11I[intro]| 
  |dest v11D[dest]|
  |elim v11E[elim]|


text‹Set operations.›

lemma (in v11) v11_vinsert[intro, simp]:
  assumes "a ∉∘ 𝒟∘ r" and "b ∉∘ ℛ∘ r"
  shows "v11 (vinsert ⟨a, b⟩ r)" 
  using assms v11_axioms 
  by (intro v11I; elim v11E) (simp_all add: vconverse_vinsert vsv.vsv_vinsert)

lemma v11_vinsertD:
  assumes "v11 (vinsert x r)"
  shows "v11 r"
  using assms by (intro v11I) (auto simp: vsv_vinsertD)

lemma v11_vunion:
  assumes "v11 r" 
    and "v11 s" 
    and "vdisjnt (𝒟∘ r) (𝒟∘ s)" 
    and "vdisjnt (ℛ∘ r) (ℛ∘ s)"
  shows "v11 (r ∪∘ s)"
proof
  interpret r: v11 r by (rule assms(1))
  interpret s: v11 s by (rule assms(2))
  show "vsv (r ∪∘ s)" by (simp add: assms v11D)
  from assms show "vsv ((r ∪∘ s)¯∘)"
    by (simp add: assms r.vsv_vconverse s.vsv_vconverse vconverse_vunion)
qed

lemma (in v11) v11_vintersection[intro, simp]: "v11 (r ∩∘ s)"
  using v11_axioms by (intro v11I) auto

lemma (in v11) v11_vdiff[intro, simp]: "v11 (r -∘ s)"
  using v11_axioms by (intro v11I) auto


text‹Special properties.›

lemma (in vsv) vsv_valneq_v11I:
  assumes "⋀x y. ⟦ x ∈∘ 𝒟∘ r; y ∈∘ 𝒟∘ r; x ≠ y ⟧ ⟹ r⦇x⦈ ≠ r⦇y⦈"
  shows "v11 r"
proof(intro v11I)
  from vsv_axioms show "vsv r" by simp
  show "vsv (r¯∘)"
    by 
      (
        metis
          assms 
          vbrelation_vconverse 
          vconverse_atD 
          app_vrangeI 
          vrange_vconverse 
          vsvI
      )
qed

lemma (in vsv) vsv_valeq_v11I:
  assumes "⋀x y. ⟦ x ∈∘ 𝒟∘ r; y ∈∘ 𝒟∘ r; r⦇x⦈ = r⦇y⦈ ⟧ ⟹ x = y"
  shows "v11 r"
  using assms vsv_valneq_v11I by auto


text‹Connections.›

lemma v11_vempty[simp]: "v11 0" by (simp add: v11I)

lemma v11_vsingleton[simp]: "v11 (set {⟨a, b⟩})" by auto

lemma v11_vdoubleton: 
  assumes "a ≠ c" and "b ≠ d"
  shows "v11 (set {⟨a, b⟩, ⟨c, d⟩})" 
  using assms by (auto simp: vinsert_set_insert_eq)

lemma v11_vid_on[simp]: "v11 (vid_on A)" by auto

lemma v11_VLambda[intro]:
  assumes "inj_on f (elts A)"
  shows "v11 (λa∈∘A. f a)"
proof(rule rel_VLambda.vsv_valneq_v11I)
  fix x y 
  assume "x ∈∘ 𝒟∘ (λa∈∘A. f a)" and "y ∈∘ 𝒟∘ (λa∈∘A. f a)" and "x ≠ y"
  then have "x ∈∘ A" and "y ∈∘ A" by auto
  with assms ‹x ≠ y› have "f x ≠ f y" by (auto dest: inj_onD)
  then show "(λa∈∘A. f a)⦇x⦈ ≠ (λa∈∘A. f a)⦇y⦈" 
    by (simp add: ‹x ∈∘ A› ‹y ∈∘ A›)
qed

lemma v11_vcomp:  
  assumes "v11 r" and "v11 s"
  shows "v11 (r ∘∘ s)"
  using assms by (intro v11I; elim v11E) (auto simp: vsv_vcomp vconverse_vcomp)

context v11
begin

lemma v11_vconverse: "v11 (r¯∘)" by (auto simp: vsv_axioms vsv_vconverse)

interpretation v11 ‹r¯∘› by (rule v11_vconverse)

lemma v11_vlrestriction[intro, simp]: "v11 (r ↾l∘ A)"
  using vsv_vrrestriction by (auto simp: vrrestriction_vconverse)

lemma v11_vrrestriction[intro, simp]: "v11 (r ↾r∘ A)"
  using vsv_vlrestriction by (auto simp: vlrestriction_vconverse)

lemma v11_vrestriction[intro, simp]: "v11 (r ↾∘ A)"
  using vsv_vrestriction by (auto simp: vrestriction_vconverse)

end


text‹Further Special properties.›

context v11
begin

lemma v11_injective: 
  assumes "a ∈∘ 𝒟∘ r" and "b ∈∘ 𝒟∘ r" and "r⦇a⦈ = r⦇b⦈" 
  shows "a = b"
  using assms v11_axioms by auto

lemma v11_double_pair: 
  assumes "a ∈∘ 𝒟∘ r" and "a' ∈∘ 𝒟∘ r" and "r⦇a⦈ = b" and "r⦇a'⦈ = b'" 
  shows "a = a' ⟷ b = b'"
  using assms v11_axioms by auto

lemma v11_vrange_ex1_eq: "b ∈∘ ℛ∘ r ⟷ (∃!a∈∘𝒟∘ r. r⦇a⦈ = b)"
proof(rule iffI)
  from app_vdomainI v11_injective show 
    "b ∈∘ ℛ∘ r ⟹ ∃!a. a ∈∘ 𝒟∘ r ∧ r⦇a⦈ = b"
    by (elim app_vrangeE) auto
  show "∃!a. a ∈∘ 𝒟∘ r ∧ r⦇a⦈ = b ⟹ b ∈∘ ℛ∘ r"
    by (auto intro: vsv_vimageI2)
qed

lemma v11_VLambda_iff: "inj_on f (elts A) ⟷ v11 (λa∈∘A. f a)"
  by (rule iffI; (intro inj_onI | tactic‹all_tac›)) 
    (auto simp: v11.v11_injective)

lemma v11_vimage_vpsubset_neq:
  assumes "A ⊆∘ 𝒟∘ r" and "B ⊆∘ 𝒟∘ r" and "A ≠ B"
  shows "r `∘ A ≠ r `∘ B" 
proof-
  from assms obtain a where AB: "a ∈∘ A ∨ a ∈∘ B" and nAB: "a ∉∘ A ∨ a ∉∘ B" 
    by auto
  then have "r⦇a⦈ ∉∘ r `∘ A ∨ r⦇a⦈ ∉∘ r `∘ B"
    unfolding vsv_vimage_iff by (metis assms(1,2) v11_injective vsubsetD)
  moreover from AB nAB assms(1,2) have "r⦇a⦈ ∈∘ r `∘ A ∨ r⦇a⦈ ∈∘ r `∘ B"
    by auto
  ultimately show "r `∘ A ≠ r `∘ B" by clarsimp
qed

lemma v11_eq_iff[simp]:
  assumes "a ∈∘ 𝒟∘ r" and "b ∈∘ 𝒟∘ r"
  shows "r⦇a⦈ = r⦇b⦈ ⟷ a = b"
  using assms v11_double_pair by blast

lemma v11_vcomp_vconverse: "r¯∘ ∘∘ r = vid_on (𝒟∘ r)"
proof(intro vsubset_antisym vsubsetI)
  fix x assume prems: "x ∈∘ r¯∘ ∘∘ r"
  then obtain a c where x_def: "x = ⟨a, c⟩" and a: "a ∈∘ 𝒟∘ r" by auto
  with prems obtain b where "⟨a, b⟩ ∈∘ r" and "⟨b, c⟩ ∈∘ r¯∘" by auto
  with v11.vsv_vconverse v11_axioms have ca: "c = a" by auto
  from a show "x ∈∘ vid_on (𝒟∘ r)" unfolding x_def ca by auto
next
  fix x assume "x ∈∘ vid_on (𝒟∘ r)"
  then obtain a where x_def: "x = ⟨a, a⟩" and a: "a ∈∘ 𝒟∘ r" by clarsimp
  then obtain b where "⟨a, b⟩ ∈∘ r" by auto
  then show "x ∈∘ r¯∘ ∘∘ r" unfolding x_def using a by auto
qed

lemma v11_vcomp_vconverse': "r ∘∘ r¯∘ = vid_on (ℛ∘ r)"
  using v11.v11_vcomp_vconverse v11_vconverse by force

lemma v11_vconverse_app[simp]:
  assumes "r⦇a⦈ = b" and "a ∈∘ 𝒟∘ r"
  shows "r¯∘⦇b⦈ = a"
  using assms by (simp add: vsv.vconverse_iff vsv_axioms vsv_vconverse)

lemma v11_vconverse_app_in_vdomain:
  assumes "y ∈∘ ℛ∘ r"
  shows "r¯∘⦇y⦈ ∈∘ 𝒟∘ r"
  using assms v11_vconverse 
  unfolding vrange_vconverse[symmetric] 
  by (auto simp: v11_def)

lemma v11_app_if_vconverse_app:
  assumes "y ∈∘ ℛ∘ r" and "r¯∘⦇y⦈ = x"
  shows "r⦇x⦈ = y"
  using assms vsv_vconverse by auto

lemma v11_app_vconverse_app:
  assumes "a ∈∘ ℛ∘ r"
  shows "r⦇r¯∘⦇a⦈⦈ = a"
  using assms by (meson v11_app_if_vconverse_app)

lemma v11_vconverse_app_app:
  assumes "a ∈∘ 𝒟∘ r"
  shows "r¯∘⦇r⦇a⦈⦈ = a"
  using assms v11_vconverse_app by auto

end

lemma v11_vlrestriction_vsubset:
  assumes "v11 (f ↾l∘ A)" and "B ⊆∘ A"
  shows "v11 (f ↾l∘ B)"
proof-
  from assms have fB_def: "f ↾l∘ B = (f ↾l∘ A) ↾l∘ B" by auto
  show ?thesis unfolding fB_def by (intro v11.v11_vlrestriction assms(1))
qed

lemma v11_vlrestriction_vrange:
  assumes "v11 s" and "v11 (r ↾l∘ ℛ∘ s)"
  shows "v11 (r ∘∘ s)"
proof(intro v11I)
  interpret v11 s by (rule assms(1)) 
  from assms vsv_vlrestriction_vrange show "vsv (r ∘∘ s)"
    by (simp add: v11.axioms(1))
  show "vsv ((r ∘∘ s)¯∘)"
    unfolding vconverse_vcomp
  proof(rule vsvI)
    fix a c c' assume "⟨a, c⟩ ∈∘ s¯∘ ∘∘ r¯∘" "⟨a, c'⟩ ∈∘ s¯∘ ∘∘ r¯∘"
    then obtain b and b' 
      where "⟨b, a⟩ ∈∘ r" 
      and bc: "⟨c, b⟩ ∈∘ s"
      and "⟨b', a⟩ ∈∘ r" 
      and b'c': "⟨c', b'⟩ ∈∘ s"
      by auto
    moreover then have "b ∈∘ ℛ∘ s" and "b' ∈∘ ℛ∘ s" by auto
    ultimately have "⟨b, a⟩ ∈∘ (r ↾l∘ ℛ∘ s)" and "⟨b', a⟩ ∈∘ (r ↾l∘ ℛ∘ s)" by auto
    with assms(2) have bb': "b = b'" by auto
    from assms bc[unfolded bb'] b'c' show "c = c'" by auto
  qed auto
qed

lemma v11_vlrestriction_vcomp:
  assumes "v11 (f ↾l∘ A)" and "v11 (g ↾l∘ (f `∘ A))"
  shows "v11 ((g ∘∘ f) ↾l∘ A)"
  using assms v11_vlrestriction_vrange by (auto simp: assms(2) app_vimage_def)


text‹Alternative forms of existing results.›

lemmas [intro, simp] = v11.v11_vinsert
  and [intro, simp] = v11.v11_vintersection
  and [intro, simp] = v11.v11_vdiff
  and [intro, simp] = v11.v11_vrrestriction
  and [intro, simp] = v11.v11_vlrestriction
  and [intro, simp] = v11.v11_vrestriction
  and [intro] = v11.v11_vimage_vpsubset_neq



subsection‹Tools: ‹mk_VLambda››

ML‹

(* low level unfold *)
(*Designed based on an algorithm from HOL-Types_To_Sets/unoverload_def.ML*)
fun pure_unfold ctxt thms = ctxt
  |> 
    (
      thms
      |> Conv.rewrs_conv 
      |> Conv.try_conv 
      |> K
      |> Conv.top_conv
    )
  |> Conv.fconv_rule;

val msg_args = "mk_VLambda: invalid arguments"

val vsv_VLambda_thm = @{thm vsv_VLambda};
val vsv_VLambda_match = vsv_VLambda_thm 
  |> Thm.full_prop_of
  |> HOLogic.dest_Trueprop
  |> dest_comb 
  |> #2;

val vdomain_VLambda_thm = @{thm vdomain_VLambda};
val vdomain_VLambda_match = vdomain_VLambda_thm 
  |> Thm.full_prop_of
  |> HOLogic.dest_Trueprop
  |> HOLogic.dest_eq
  |> #1
  |> dest_comb
  |> #2;

val app_VLambda_thm = @{thm ZFC_Cardinals.beta};
val app_VLambda_match = app_VLambda_thm 
  |> Thm.concl_of
  |> HOLogic.dest_Trueprop
  |> HOLogic.dest_eq
  |> #1
  |> strip_comb
  |> #2
  |> hd;

fun mk_VLabmda_thm match_t match_thm ctxt thm =
  let
    val thm_ct = Thm.cprop_of thm
    val (_, rhs_ct) = Thm.dest_equals thm_ct
      handle TERM ("dest_equals", _) => error msg_args
    val insts = Thm.match (Thm.cterm_of ctxt match_t, rhs_ct)
      handle Pattern.MATCH => error msg_args
  in 
    match_thm
    |> Drule.instantiate_normalize insts
    |> pure_unfold ctxt (thm |> Thm.symmetric |> single) 
  end;

val mk_VLambda_vsv =
  mk_VLabmda_thm vsv_VLambda_match vsv_VLambda_thm;
val mk_VLambda_vdomain =
  mk_VLabmda_thm vdomain_VLambda_match vdomain_VLambda_thm;
val mk_VLambda_app = 
  mk_VLabmda_thm app_VLambda_match app_VLambda_thm;

val mk_VLambda_parser = Parse.thm --
  (
    Scan.repeat
      (
        (keyword‹|vsv› -- Parse_Spec.opt_thm_name "|") ||
        (keyword‹|app› -- Parse_Spec.opt_thm_name "|") ||
        (keyword‹|vdomain› -- Parse_Spec.opt_thm_name "|")
      )
  );

fun process_mk_VLambda_thm mk_VLambda_thm (b, thm) ctxt =
  let 
    val thm' = mk_VLambda_thm ctxt thm
    val (res, ctxt') = ctxt
      |> Local_Theory.note (b ||> map (Attrib.check_src ctxt), single thm') 
    val _ = Proof_Display.print_theorem (Position.thread_data ()) ctxt' res
  in ctxt' end;

fun folder_mk_VLambda (("|vsv", b), thm) ctxt =
      process_mk_VLambda_thm mk_VLambda_vsv (b, thm) ctxt
  | folder_mk_VLambda (("|app", b), thm) ctxt =
      process_mk_VLambda_thm mk_VLambda_app (b, thm) ctxt
  | folder_mk_VLambda (("|vdomain", b), thm) ctxt =
      process_mk_VLambda_thm mk_VLambda_vdomain (b, thm) ctxt
  | folder_mk_VLambda _ _ = error msg_args

fun process_mk_VLambda (thm, ins) ctxt =
  let
    val _ = ins |> map fst |> has_duplicates op= |> not orelse error msg_args
    val thm' = thm
      |> singleton (Attrib.eval_thms ctxt)
      |> Local_Defs.meta_rewrite_rule ctxt;
  in fold folder_mk_VLambda (map (fn x => (x, thm')) ins) ctxt end;

val _ =
  Outer_Syntax.local_theory
    command_keyword‹mk_VLambda›
    "VLambda"
    (mk_VLambda_parser >> process_mk_VLambda);

›

text‹\newpage›

end