Theory CZH_Sets_FBRelations

(* Copyright 2021 (C) Mihails Milehins *)

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



subsection‹Background›


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

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

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

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



subsection‹‹fpairs››

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

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


text‹Rules.›

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

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

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

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


text‹Elementary properties.›

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


text‹Set operations.›

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

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

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

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

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

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

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


text‹Special properties.›

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

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

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



subsection‹Constructors›


subsubsection‹Identity relation›

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

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


text‹Rules.›

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

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

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

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

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


text‹Set operations.›

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

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

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

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

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

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

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

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


text‹Special properties.›

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


subsubsection‹Constant function›

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

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


text‹Rules.›

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

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

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

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


text‹Set operations.›

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

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

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

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

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

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

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

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


text‹Special properties.›

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


subsubsection‹Composition›

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

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


text‹Rules.›

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

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

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


text‹Elementary properties.›

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


text‹Set operations.›

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

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

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

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

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

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

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


text‹Connections.›

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

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

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


text‹Special properties.›

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

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


subsubsection‹Converse relation›

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

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


text‹Rules.›

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

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

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

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


text‹Set operations.›

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

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

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

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

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

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


text‹Connections.›

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

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

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

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


text‹Special properties.›

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


subsubsection‹Left restriction›

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

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


text‹Rules.›

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

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

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


text‹Set operations.›

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

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

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

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

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

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

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

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

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

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


text‹Connections.›

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

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

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

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


text‹Previous connections.›

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

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


text‹Special properties.›

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

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


subsubsection‹Right restriction›

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

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


text‹Rules.›

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

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

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


text‹Set operations.›

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

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

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

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

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

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

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

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

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

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


text‹Connections.›

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

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

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


text‹Previous connections.›

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

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

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

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


text‹Special properties.›

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

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


subsubsection‹Restriction›

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

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


text‹Rules.›

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

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

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


text‹Set operations.›

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

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

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

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

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

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

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

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

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

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

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


text‹Connections.›

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

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

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

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

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


text‹Previous connections.›

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

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

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

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


text‹Special properties.›

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

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

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



subsection‹Properties›


subsubsection‹Domain›

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

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


text‹Rules.›

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

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

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

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


text‹Set operations.›

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

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

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

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

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

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

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

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


text‹Connections.›

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

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

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


text‹Special properties.›

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

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


subsubsection‹Range›

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

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


text‹Rules.›

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

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

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

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


text‹Set operations.›

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

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

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

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

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

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

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

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


text‹Connections.›

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

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

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

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


text‹Previous connections›

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

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


text‹Special properties.›

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

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

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

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

subsubsection‹Field›

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

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


text‹Rules.›

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

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

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

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

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

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

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


text‹Set operations.›

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

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

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

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

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

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


text‹Connections.›

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

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

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

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


text‹Special properties.›

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


subsubsection‹Image›

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

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


text‹Rules.›

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

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

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

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

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


text‹Set operations.›

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

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

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

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

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

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

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

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

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

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

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


text‹Special properties.›

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

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


text‹Connections.›

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

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

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

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

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

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

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

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

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

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

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


text‹Previous connections.›

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


text‹Further special properties.›

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

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

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

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


subsubsection‹Inverse image›

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

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


text‹Rules.›

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

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

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

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

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

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

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

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

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

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

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

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


text‹Set operations.›

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

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

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

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

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

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

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

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

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

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

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


text‹Special properties.›

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

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

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

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


text‹Connections.›

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

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

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

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

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

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

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

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

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


text‹Previous connections.›

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



subsection‹Classification of relations›


subsubsection‹Binary relation›

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

locale fbrelation_pair = r1: fbrelation r1 + r2: fbrelation r2 for r1 r2


text‹Rules.›

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

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

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

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

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

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

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


text‹Set operations.›

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

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

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

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

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

lemma (in fbrelation_pair) fbrelation_vunionI: "fbrelation (r1 ∪∘ r2)"
  using r1.fbrelation_axioms r2.fbrelation_axioms by auto

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

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

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


text‹Connections.›

lemma fbrelation_vempty: "fbrelation 0" by auto

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

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

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

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

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

lemma (in fbrelation_pair) fbrelation_fcomp: "fbrelation (r1 ∘∙ r2)" 
  using r1.fbrelation_axioms r2.fbrelation_axioms by auto

sublocale fbrelation_pair ⊆ fcomp21: fbrelation ‹r2 ∘∙ r1›
  by 
    (
      simp add: 
        fbrelation_pair.fbrelation_fcomp 
        fbrelation_pair_def 
        r1.fbrelation_axioms 
        r2.fbrelation_axioms
     )

sublocale fbrelation_pair ⊆ fcomp12: fbrelation ‹r1 ∘∙ r2› 
  by (rule fbrelation_fcomp)

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

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

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

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


text‹Previous connections.›

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

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

lemma (in fbrelation_pair) fconverse_inject[simp]: "r1¯∙ = r2¯∙ ⟷ r1 = r2"
  using r1.fbrelation_axioms r2.fbrelation_axioms by fast

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

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

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


text‹Special properties.›

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

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

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

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

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

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

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


text‹Alternative forms of existing results.›

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

context
  fixes r1 r2
  assumes r1: "fbrelation r1"
    and r2: "fbrelation r2"
begin

lemmas_with[OF fbrelation_pair.intro[OF r1 r2]] :
  fbrelation_fconverse_mono[intro, simp] = fbrelation_pair.fconverse_mono
  and fbrelation_frrestriction_srange[intro, simp] = 
    fbrelation_pair.fconverse_inject

end

text‹\newpage›

end