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 typV 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 "aA. 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)


subsubsectionVLambda›


text‹Rules.›

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

lemma VLambdaD[dest!]: 
  assumes "a, f a  (λaA. f a)"
  shows "a  A"
  using assms unfolding VLambda_def by auto

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

lemma VLambda_iff1: "x  (λaA. f a)  (aA. x = a, f a)" by auto

lemma VLambda_iff2: "a, b  (λaA. 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: "(λaA. f a) = set {a, f a | a. a  A}" by auto


text‹Set operations.›

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

lemma VLambda_vsingleton(*not simp*): "(λaset {a}. f a) = set {a, f a}" 
  by auto

lemma VLambda_vdoubleton(*not simp*): 
  "(λaset {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 "(λaA. f a)  (λaB. f a)"
  using assms by auto

lemma VLambda_vinsert: 
  "(λavinsert a A. f a) = (λaset {a}. f a)  (λaA. f a)" 
  by auto

lemma VLambda_vintersection: "(λaA  B. f a) = (λaA. f a)  (λaB. f a)" 
  by auto

lemma VLambda_vunion: "(λaA  B. f a) = (λaA. f a)  (λaB. f a)" by auto

lemma VLambda_vdiff: "(λaA - B. f a) = (λaA. f a) - (λaB. f a)" by auto


text‹Connections.›

lemma VLambda_vid_on: "(λaA. a) = vid_on A" by auto

lemma VLambda_vconst_on: "(λaA. 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]: "(λaA. f a)  vid_on A = (λaA. 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 = (λrA. 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: "(λaA. f a) l B = (λaA  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 = (λrD. 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]: "𝒟 (λaA. 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 = (λrD. 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: " (λaA. 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 = (λrD. 𝒟 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. aA. a, b  r}"
proof-
  have ss: "{b. aA. 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. aA. 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  (aA. 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  ((λxVPow 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  (λxVPow 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: "(λaA. f a) ` B =  (λaA  B. f a)"
  unfolding vimage_def by (simp add: vlrestriction_VLambda)

lemma vimage_VLambda_vrange_rep: "(λaA. f a) ` A =  (λaA. 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((λaA. g a) ` A). f b)  (λaA. g a) = (λaA. (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. bA. a, b  r}"
proof-
  have ss: "{a. bA. 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  (bA. 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. bA. 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 "