Quelle Relation.thy Sprache: Isabelle

(*  Title:      HOL/Relation.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Author:     Stefan Berghofer, TU Muenchen
    Author:     Martin Desharnais, MPI-INF Saarbruecken
*)

section \<open>Relations -- as sets of pairs, and binary predicates\<close>

theory Relation
  imports Product_Type Sum_Type Fields
begin

text \<open>A preliminary: classical rules for reasoning on predicates\<close>

declare predicate1I [Pure.intro!, intro!]
declare predicate1D [Pure.dest, dest]
declare predicate2I [Pure.intro!, intro!]
declare predicate2D [Pure.dest, dest]
declare bot1E [elim!]
declare bot2E [elim!]
declare top1I [intro!]
declare top2I [intro!]
declare inf1I [intro!]
declare inf2I [intro!]
declare inf1E [elim!]
declare inf2E [elim!]
declare sup1I1 [intro?]
declare sup2I1 [intro?]
declare sup1I2 [intro?]
declare sup2I2 [intro?]
declare sup1E [elim!]
declare sup2E [elim!]
declare sup1CI [intro!]
declare sup2CI [intro!]
declare Inf1_I [intro!]
declare INF1_I [intro!]
declare Inf2_I [intro!]
declare INF2_I [intro!]
declare Inf1_D [elim]
declare INF1_D [elim]
declare Inf2_D [elim]
declare INF2_D [elim]
declare Inf1_E [elim]
declare INF1_E [elim]
declare Inf2_E [elim]
declare INF2_E [elim]
declare Sup1_I [intro]
declare SUP1_I [intro]
declare Sup2_I [intro]
declare SUP2_I [intro]
declare Sup1_E [elim!]
declare SUP1_E [elim!]
declare Sup2_E [elim!]
declare SUP2_E [elim!]

subsection \<open>Fundamental\<close>

subsubsection \<open>Relations as sets of pairs\<close>

type_synonym 'a rel = "('a \<times> 'a) set"

lemma subrelI: "(\x y. (x, y) \ r \ (x, y) \ s) \ r \ s"
  \<comment> \<open>Version of @{thm [source] subsetI} for binary relations\<close>
  by auto

lemma lfp_induct2:
  "(a, b) \ lfp f \ mono f \
    (\<And>a b. (a, b) \<in> f (lfp f \<inter> {(x, y). P x y}) \<Longrightarrow> P a b) \<Longrightarrow> P a b"
  \<comment> \<open>Version of @{thm [source] lfp_induct} for binary relations\<close>
  using lfp_induct_set [of "(a, b)" f "case_prod P"] by auto

subsubsection \<open>Conversions between set and predicate relations\<close>

lemma pred_equals_eq [pred_set_conv]: "(\x. x \ R) = (\x. x \ S) \ R = S"
  by (simp add: set_eq_iff fun_eq_iff)

lemma pred_equals_eq2 [pred_set_conv]: "(\x y. (x, y) \ R) = (\x y. (x, y) \ S) \ R = S"
  by (simp add: set_eq_iff fun_eq_iff)

lemma pred_subset_eq [pred_set_conv]: "(\x. x \ R) \ (\x. x \ S) \ R \ S"
  by (simp add: subset_iff le_fun_def)

lemma pred_subset_eq2 [pred_set_conv]: "(\x y. (x, y) \ R) \ (\x y. (x, y) \ S) \ R \ S"
  by (simp add: subset_iff le_fun_def)

lemma bot_empty_eq [pred_set_conv]: "\ = (\x. x \ {})"
  by (auto simp add: fun_eq_iff)

lemma bot_empty_eq2 [pred_set_conv]: "\ = (\x y. (x, y) \ {})"
  by (auto simp add: fun_eq_iff)

lemma top_empty_eq: "\ = (\x. x \ UNIV)"
  by (auto simp add: fun_eq_iff)

lemma top_empty_eq2: "\ = (\x y. (x, y) \ UNIV)"
  by (auto simp add: fun_eq_iff)

lemma inf_Int_eq [pred_set_conv]: "(\x. x \ R) \ (\x. x \ S) = (\x. x \ R \ S)"
  by (simp add: inf_fun_def)

lemma inf_Int_eq2 [pred_set_conv]: "(\x y. (x, y) \ R) \ (\x y. (x, y) \ S) = (\x y. (x, y) \ R \ S)"
  by (simp add: inf_fun_def)

lemma sup_Un_eq [pred_set_conv]: "(\x. x \ R) \ (\x. x \ S) = (\x. x \ R \ S)"
  by (simp add: sup_fun_def)

lemma sup_Un_eq2 [pred_set_conv]: "(\x y. (x, y) \ R) \ (\x y. (x, y) \ S) = (\x y. (x, y) \ R \ S)"
  by (simp add: sup_fun_def)

lemma INF_INT_eq [pred_set_conv]: "(\i\S. (\x. x \ r i)) = (\x. x \ (\i\S. r i))"
  by (simp add: fun_eq_iff)

lemma INF_INT_eq2 [pred_set_conv]: "(\i\S. (\x y. (x, y) \ r i)) = (\x y. (x, y) \ (\i\S. r i))"
  by (simp add: fun_eq_iff)

lemma SUP_UN_eq [pred_set_conv]: "(\i\S. (\x. x \ r i)) = (\x. x \ (\i\S. r i))"
  by (simp add: fun_eq_iff)

lemma SUP_UN_eq2 [pred_set_conv]: "(\i\S. (\x y. (x, y) \ r i)) = (\x y. (x, y) \ (\i\S. r i))"
  by (simp add: fun_eq_iff)

lemma Inf_INT_eq [pred_set_conv]: "\S = (\x. x \ (\(Collect ` S)))"
  by (simp add: fun_eq_iff)

lemma INF_Int_eq [pred_set_conv]: "(\i\S. (\x. x \ i)) = (\x. x \ \S)"
  by (simp add: fun_eq_iff)

lemma Inf_INT_eq2 [pred_set_conv]: "\S = (\x y. (x, y) \ (\(Collect ` case_prod ` S)))"
  by (simp add: fun_eq_iff)

lemma INF_Int_eq2 [pred_set_conv]: "(\i\S. (\x y. (x, y) \ i)) = (\x y. (x, y) \ \S)"
  by (simp add: fun_eq_iff)

lemma Sup_SUP_eq [pred_set_conv]: "\S = (\x. x \ \(Collect ` S))"
  by (simp add: fun_eq_iff)

lemma SUP_Sup_eq [pred_set_conv]: "(\i\S. (\x. x \ i)) = (\x. x \ \S)"
  by (simp add: fun_eq_iff)

lemma Sup_SUP_eq2 [pred_set_conv]: "\S = (\x y. (x, y) \ (\(Collect ` case_prod ` S)))"
  by (simp add: fun_eq_iff)

lemma SUP_Sup_eq2 [pred_set_conv]: "(\i\S. (\x y. (x, y) \ i)) = (\x y. (x, y) \ \S)"
  by (simp add: fun_eq_iff)

subsection \<open>Properties of relations\<close>

subsubsection \<open>Reflexivity\<close>

definition refl_on :: "'a set \ 'a rel \ bool"
  where "refl_on A r \ (\x\A. (x, x) \ r)"

abbreviation refl :: "'a rel \ bool" \ \reflexivity over a type\
  where "refl \ refl_on UNIV"

definition reflp_on :: "'a set \ ('a \ 'a \ bool) \ bool"
  where "reflp_on A R \ (\x\A. R x x)"

abbreviation reflp :: "('a \ 'a \ bool) \ bool"
  where "reflp \ reflp_on UNIV"

lemma reflp_def[no_atp]: "reflp R \ (\x. R x x)"
  by (simp add: reflp_on_def)

text \<open>@{thm [source] reflp_def} is for backward compatibility.\<close>

lemma reflp_on_refl_on_eq[pred_set_conv]: "reflp_on A (\a b. (a, b) \ r) \ refl_on A r"
  by (simp add: refl_on_def reflp_on_def)

lemmas reflp_refl_eq = reflp_on_refl_on_eq[of UNIV]

lemma refl_onI [intro?]: "(\x. x \ A \ (x, x) \ r) \ refl_on A r"
  unfolding refl_on_def by (iprover intro!: ballI)

lemma reflI: "(\x. (x, x) \ r) \ refl r"
  by (auto intro: refl_onI)

lemma reflp_onI:
  "(\x. x \ A \ R x x) \ reflp_on A R"
  by (simp add: reflp_on_def)

lemma reflpI[intro?]: "(\x. R x x) \ reflp R"
  by (rule reflp_onI)

lemma refl_onD: "refl_on A r \ a \ A \ (a, a) \ r"
  unfolding refl_on_def by blast

lemma reflD: "refl r \ (a, a) \ r"
  unfolding refl_on_def by blast

lemma reflp_onD:
  "reflp_on A R \ x \ A \ R x x"
  by (simp add: reflp_on_def)

lemma reflpD[dest?]: "reflp R \ R x x"
  by (simp add: reflp_onD)

lemma reflpE:
  assumes "reflp r"
  obtains "r x x"
  using assms by (auto dest: refl_onD simp add: reflp_def)

lemma refl_on_top[simp]: "refl_on A \"
  by (simp add: refl_on_def)

lemma reflp_on_top[simp]: "reflp_on A \"
  by (simp add: reflp_on_def)

lemma reflp_on_mono_strong:
  "reflp_on B R \ A \ B \ (\x y. x \ A \ y \ A \ R x y \ Q x y) \ reflp_on A Q"
  by (rule reflp_onI) (auto dest: reflp_onD)

lemma reflp_on_mono[mono]: "A \ B \ R \ Q \ reflp_on B R \ reflp_on A Q"
  by (simp add: reflp_on_mono_strong le_fun_def)

lemma reflp_on_subset: "reflp_on B R \ A \ B \ reflp_on A R"
  using reflp_on_mono_strong .

lemma reflp_on_image: "reflp_on (f ` A) R \ reflp_on A (\a b. R (f a) (f b))"
  by (simp add: reflp_on_def)

lemma refl_on_Int: "refl_on A r \ refl_on B s \ refl_on (A \ B) (r \ s)"
  unfolding refl_on_def by blast

lemma reflp_on_inf: "reflp_on A R \ reflp_on B S \ reflp_on (A \ B) (R \ S)"
  by (auto intro: reflp_onI dest: reflp_onD)

lemma reflp_inf: "reflp r \ reflp s \ reflp (r \ s)"
  by (rule reflp_on_inf[of UNIV _ UNIV, unfolded Int_absorb])

lemma refl_on_Un: "refl_on A r \ refl_on B s \ refl_on (A \ B) (r \ s)"
  unfolding refl_on_def by blast

lemma reflp_on_sup: "reflp_on A R \ reflp_on B S \ reflp_on (A \ B) (R \ S)"
  by (auto intro: reflp_onI dest: reflp_onD)

lemma reflp_sup: "reflp r \ reflp s \ reflp (r \ s)"
  by (rule reflp_on_sup[of UNIV _ UNIV, unfolded Un_absorb])

lemma refl_on_INTER: "\x\S. refl_on (A x) (r x) \ refl_on (\(A ` S)) (\(r ` S))"
  unfolding refl_on_def by fast

lemma reflp_on_Inf: "\x\S. reflp_on (A x) (R x) \ reflp_on (\(A ` S)) (\(R ` S))"
  by (auto intro: reflp_onI dest: reflp_onD)

lemma refl_on_UNION: "\x\S. refl_on (A x) (r x) \ refl_on (\(A ` S)) (\(r ` S))"
  unfolding refl_on_def by blast

lemma reflp_on_Sup: "\x\S. reflp_on (A x) (R x) \ reflp_on (\(A ` S)) (\(R ` S))"
  by (auto intro: reflp_onI dest: reflp_onD)

lemma refl_on_empty [simp]: "refl_on {} r"
  by (simp add: refl_on_def)

lemma reflp_on_empty [simp]: "reflp_on {} R"
  by (auto intro: reflp_onI)

lemma refl_on_singleton [simp]: "refl_on {x} {(x, x)}"
by (blast intro: refl_onI)

lemma reflp_on_equality [simp]: "reflp_on A (=)"
  by (simp add: reflp_on_def)

lemma (in preorder) reflp_on_le[simp]: "reflp_on A (\)"
  by (simp add: reflp_onI)

lemma (in preorder) reflp_on_ge[simp]: "reflp_on A (\)"
  by (simp add: reflp_onI)

subsubsection \<open>Irreflexivity\<close>

definition irrefl_on :: "'a set \ 'a rel \ bool" where
  "irrefl_on A r \ (\a \ A. (a, a) \ r)"

abbreviation irrefl :: "'a rel \ bool" where
  "irrefl \ irrefl_on UNIV"

definition irreflp_on :: "'a set \ ('a \ 'a \ bool) \ bool" where
  "irreflp_on A R \ (\a \ A. \ R a a)"

abbreviation irreflp :: "('a \ 'a \ bool) \ bool" where
  "irreflp \ irreflp_on UNIV"

lemma irrefl_def[no_atp]: "irrefl r \ (\a. (a, a) \ r)"
  by (simp add: irrefl_on_def)

lemma irreflp_def[no_atp]: "irreflp R \ (\a. \ R a a)"
  by (simp add: irreflp_on_def)

text \<open>@{thm [source] irrefl_def} and @{thm [source] irreflp_def} are for backward compatibility.\<close>

lemma irreflp_on_irrefl_on_eq [pred_set_conv]: "irreflp_on A (\a b. (a, b) \ r) \ irrefl_on A r"
  by (simp add: irrefl_on_def irreflp_on_def)

lemmas irreflp_irrefl_eq = irreflp_on_irrefl_on_eq[of UNIV]

lemma irrefl_onI: "(\a. a \ A \ (a, a) \ r) \ irrefl_on A r"
  by (simp add: irrefl_on_def)

lemma irreflI[intro?]: "(\a. (a, a) \ r) \ irrefl r"
  by (rule irrefl_onI[of UNIV, simplified])

lemma irreflp_onI: "(\a. a \ A \ \ R a a) \ irreflp_on A R"
  by (rule irrefl_onI[to_pred])

lemma irreflpI[intro?]: "(\a. \ R a a) \ irreflp R"
  by (rule irreflI[to_pred])

lemma irrefl_onD: "irrefl_on A r \ a \ A \ (a, a) \ r"
  by (simp add: irrefl_on_def)

lemma irreflD: "irrefl r \ (x, x) \ r"
  by (rule irrefl_onD[of UNIV, simplified])

lemma irreflp_onD: "irreflp_on A R \ a \ A \ \ R a a"
  by (rule irrefl_onD[to_pred])

lemma irreflpD: "irreflp R \ \ R x x"
  by (rule irreflD[to_pred])

lemma irrefl_on_bot[simp]: "irrefl_on A \"
  by (simp add: irrefl_on_def)

lemma irreflp_on_bot[simp]: "irreflp_on A \"
  using irrefl_on_bot[to_pred] .

lemma irrefl_on_distinct [code]: "irrefl_on A r \ (\(a, b) \ r. a \ A \ b \ A \ a \ b)"
  by (auto simp add: irrefl_on_def)

lemmas irrefl_distinct = irrefl_on_distinct \<comment> \<open>For backward compatibility\<close>

lemma irreflp_on_mono_strong:
  "irreflp_on B Q \ A \ B \ (\x y. x \ A \ y \ A \ R x y \ Q x y) \ irreflp_on A R"
  by (rule irreflp_onI) (auto dest: irreflp_onD)

lemma irreflp_on_mono[mono]: "A \ B \ R \ Q \ irreflp_on B Q \ irreflp_on A R"
  by (simp add: irreflp_on_mono_strong le_fun_def)

lemma irrefl_on_subset: "irrefl_on B r \ A \ B \ irrefl_on A r"
  by (auto simp: irrefl_on_def)

lemma irreflp_on_subset: "irreflp_on B R \ A \ B \ irreflp_on A R"
  using irreflp_on_mono_strong .

lemma irreflp_on_image: "irreflp_on (f ` A) R \ irreflp_on A (\a b. R (f a) (f b))"
  by (simp add: irreflp_on_def)

lemma (in preorder) irreflp_on_less[simp]: "irreflp_on A (<)"
  by (simp add: irreflp_onI)

lemma (in preorder) irreflp_on_greater[simp]: "irreflp_on A (>)"
  by (simp add: irreflp_onI)

subsubsection \<open>Asymmetry\<close>

definition asym_on :: "'a set \ 'a rel \ bool" where
  "asym_on A r \ (\x \ A. \y \ A. (x, y) \ r \ (y, x) \ r)"

abbreviation asym :: "'a rel \ bool" where
  "asym \ asym_on UNIV"

definition asymp_on :: "'a set \ ('a \ 'a \ bool) \ bool" where
  "asymp_on A R \ (\x \ A. \y \ A. R x y \ \ R y x)"

abbreviation asymp :: "('a \ 'a \ bool) \ bool" where
  "asymp \ asymp_on UNIV"

lemma asymp_on_asym_on_eq[pred_set_conv]: "asymp_on A (\x y. (x, y) \ r) \ asym_on A r"
  by (simp add: asymp_on_def asym_on_def)

lemmas asymp_asym_eq = asymp_on_asym_on_eq[of UNIV] \<comment> \<open>For backward compatibility\<close>

lemma asym_onI[intro]:
  "(\x y. x \ A \ y \ A \ (x, y) \ r \ (y, x) \ r) \ asym_on A r"
  by (simp add: asym_on_def)

lemma asymI[intro]: "(\x y. (x, y) \ r \ (y, x) \ r) \ asym r"
  by (simp add: asym_onI)

lemma asymp_onI[intro]:
  "(\x y. x \ A \ y \ A \ R x y \ \ R y x) \ asymp_on A R"
  by (rule asym_onI[to_pred])

lemma asympI[intro]: "(\x y. R x y \ \ R y x) \ asymp R"
  by (rule asymI[to_pred])

lemma asym_onD: "asym_on A r \ x \ A \ y \ A \ (x, y) \ r \ (y, x) \ r"
  by (simp add: asym_on_def)

lemma asymD: "asym r \ (x, y) \ r \ (y, x) \ r"
  by (simp add: asym_onD)

lemma asymp_onD: "asymp_on A R \ x \ A \ y \ A \ R x y \ \ R y x"
  by (rule asym_onD[to_pred])

lemma asympD: "asymp R \ R x y \ \ R y x"
  by (rule asymD[to_pred])

lemma asym_on_bot[simp]: "asym_on A \"
  by (simp add: asym_on_def)

lemma asymp_on_bot[simp]: "asymp_on A \"
  using asym_on_bot[to_pred] .

lemma asym_iff: "asym r \ (\x y. (x,y) \ r \ (y,x) \ r)"
  by (blast dest: asymD)

lemma asymp_on_mono_strong:
  "asymp_on B Q \ A \ B \ (\x y. x \ A \ y \ A \ R x y \ Q x y) \ asymp_on A R"
  by (rule asymp_onI) (auto dest: asymp_onD)

lemma asymp_on_mono[mono]: "A \ B \ R \ Q \ asymp_on B Q \ asymp_on A R"
  by (simp add: asymp_on_mono_strong le_fun_def)

lemma asym_on_subset: "asym_on B r \ A \ B \ asym_on A r"
  by (auto simp: asym_on_def)

lemma asymp_on_subset: "asymp_on B R \ A \ B \ asymp_on A R"
  using asymp_on_mono_strong .

lemma asymp_on_image: "asymp_on (f ` A) R \ asymp_on A (\a b. R (f a) (f b))"
  by (simp add: asymp_on_def)

lemma irrefl_on_if_asym_on[simp]: "asym_on A r \ irrefl_on A r"
  by (auto intro: irrefl_onI dest: asym_onD)

lemma irreflp_on_if_asymp_on[simp]: "asymp_on A r \ irreflp_on A r"
  by (rule irrefl_on_if_asym_on[to_pred])

lemma (in preorder) asymp_on_less[simp]: "asymp_on A (<)"
  by (auto intro: dual_order.asym)

lemma (in preorder) asymp_on_greater[simp]: "asymp_on A (>)"
  by (auto intro: dual_order.asym)

subsubsection \<open>Symmetry\<close>

definition sym_on :: "'a set \ 'a rel \ bool" where
  "sym_on A r \ (\x \ A. \y \ A. (x, y) \ r \ (y, x) \ r)"

abbreviation sym :: "'a rel \ bool" where
  "sym \ sym_on UNIV"

definition symp_on :: "'a set \ ('a \ 'a \ bool) \ bool" where
  "symp_on A R \ (\x \ A. \y \ A. R x y \ R y x)"

abbreviation symp :: "('a \ 'a \ bool) \ bool" where
  "symp \ symp_on UNIV"

lemma sym_def[no_atp]: "sym r \ (\x y. (x, y) \ r \ (y, x) \ r)"
  by (simp add: sym_on_def)

lemma symp_def[no_atp]: "symp R \ (\x y. R x y \ R y x)"
  by (simp add: symp_on_def)

text \<open>@{thm [source] sym_def} and @{thm [source] symp_def} are for backward compatibility.\<close>

lemma symp_on_sym_on_eq[pred_set_conv]: "symp_on A (\x y. (x, y) \ r) \ sym_on A r"
  by (simp add: sym_on_def symp_on_def)

lemmas symp_sym_eq = symp_on_sym_on_eq[of UNIV] \<comment> \<open>For backward compatibility\<close>

lemma sym_onI: "(\x y. x \ A \ y \ A \ (x, y) \ r \ (y, x) \ r) \ sym_on A r"
  by (simp add: sym_on_def)

lemma symI [intro?]: "(\x y. (x, y) \ r \ (y, x) \ r) \ sym r"
  by (simp add: sym_onI)

lemma symp_onI: "(\x y. x \ A \ y \ A \ R x y \ R y x) \ symp_on A R"
  by (rule sym_onI[to_pred])

lemma sympI [intro?]: "(\x y. R x y \ R y x) \ symp R"
  by (rule symI[to_pred])

lemma symE:
  assumes "sym r" and "(b, a) \ r"
  obtains "(a, b) \ r"
  using assms by (simp add: sym_def)

lemma sympE:
  assumes "symp r" and "r b a"
  obtains "r a b"
  using assms by (rule symE [to_pred])

lemma sym_onD: "sym_on A r \ x \ A \ y \ A \ (x, y) \ r \ (y, x) \ r"
  by (simp add: sym_on_def)

lemma symD [dest?]: "sym r \ (x, y) \ r \ (y, x) \ r"
  by (simp add: sym_onD)

lemma symp_onD: "symp_on A R \ x \ A \ y \ A \ R x y \ R y x"
  by (rule sym_onD[to_pred])

lemma sympD [dest?]: "symp R \ R x y \ R y x"
  by (rule symD[to_pred])

lemma sym_on_bot[simp]: "sym_on A \"
  by (simp add: sym_on_def)

lemma symp_on_bot[simp]: "symp_on A \"
  using sym_on_bot[to_pred] .

lemma sym_on_top[simp]: "sym_on A \"
  by (simp add: sym_on_def)

lemma symp_on_top[simp]: "symp_on A \"
  by (simp add: symp_on_def)

lemma sym_on_subset: "sym_on B r \ A \ B \ sym_on A r"
  by (auto simp: sym_on_def)

lemma symp_on_subset: "symp_on B R \ A \ B \ symp_on A R"
  by (auto simp: symp_on_def)

lemma symp_on_image: "symp_on (f ` A) R \ symp_on A (\a b. R (f a) (f b))"
  by (simp add: symp_on_def)

lemma symp_on_equality[simp]: "symp_on A (=)"
  by (simp add: symp_on_def)

lemma sym_Int: "sym r \ sym s \ sym (r \ s)"
  by (fast intro: symI elim: symE)

lemma symp_inf: "symp r \ symp s \ symp (r \ s)"
  by (fact sym_Int [to_pred])

lemma sym_Un: "sym r \ sym s \ sym (r \ s)"
  by (fast intro: symI elim: symE)

lemma symp_sup: "symp r \ symp s \ symp (r \ s)"
  by (fact sym_Un [to_pred])

lemma sym_INTER: "\x\S. sym (r x) \ sym (\(r ` S))"
  by (fast intro: symI elim: symE)

lemma symp_INF: "\x\S. symp (r x) \ symp (\(r ` S))"
  by (fact sym_INTER [to_pred])

lemma sym_UNION: "\x\S. sym (r x) \ sym (\(r ` S))"
  by (fast intro: symI elim: symE)

lemma symp_SUP: "\x\S. symp (r x) \ symp (\(r ` S))"
  by (fact sym_UNION [to_pred])

subsubsection \<open>Antisymmetry\<close>

definition antisym_on :: "'a set \ 'a rel \ bool" where
  "antisym_on A r \ (\x \ A. \y \ A. (x, y) \ r \ (y, x) \ r \ x = y)"

abbreviation antisym :: "'a rel \ bool" where
  "antisym \ antisym_on UNIV"

definition antisymp_on :: "'a set \ ('a \ 'a \ bool) \ bool" where
  "antisymp_on A R \ (\x \ A. \y \ A. R x y \ R y x \ x = y)"

abbreviation antisymp :: "('a \ 'a \ bool) \ bool" where
  "antisymp \ antisymp_on UNIV"

lemma antisym_def[no_atp]: "antisym r \ (\x y. (x, y) \ r \ (y, x) \ r \ x = y)"
  by (simp add: antisym_on_def)

lemma antisymp_def[no_atp]: "antisymp R \ (\x y. R x y \ R y x \ x = y)"
  by (simp add: antisymp_on_def)

text \<open>@{thm [source] antisym_def} and @{thm [source] antisymp_def} are for backward compatibility.\<close>

lemma antisymp_on_antisym_on_eq[pred_set_conv]:
  "antisymp_on A (\x y. (x, y) \ r) \ antisym_on A r"
  by (simp add: antisym_on_def antisymp_on_def)

lemmas antisymp_antisym_eq = antisymp_on_antisym_on_eq[of UNIV] \<comment> \<open>For backward compatibility\<close>

lemma antisym_onI:
  "(\x y. x \ A \ y \ A \ (x, y) \ r \ (y, x) \ r \ x = y) \ antisym_on A r"
  unfolding antisym_on_def by simp

lemma antisymI [intro?]:
  "(\x y. (x, y) \ r \ (y, x) \ r \ x = y) \ antisym r"
  by (simp add: antisym_onI)

lemma antisymp_onI:
  "(\x y. x \ A \ y \ A \ R x y \ R y x \ x = y) \ antisymp_on A R"
  by (rule antisym_onI[to_pred])

lemma antisympI [intro?]:
  "(\x y. R x y \ R y x \ x = y) \ antisymp R"
  by (rule antisymI[to_pred])

lemma antisym_onD:
  "antisym_on A r \ x \ A \ y \ A \ (x, y) \ r \ (y, x) \ r \ x = y"
  by (simp add: antisym_on_def)

lemma antisymD [dest?]:
  "antisym r \ (x, y) \ r \ (y, x) \ r \ x = y"
  by (simp add: antisym_onD)

lemma antisymp_onD:
  "antisymp_on A R \ x \ A \ y \ A \ R x y \ R y x \ x = y"
  by (rule antisym_onD[to_pred])

lemma antisympD [dest?]:
  "antisymp R \ R x y \ R y x \ x = y"
  by (rule antisymD[to_pred])

lemma antisym_on_bot[simp]: "antisym_on A \"
  by (simp add: antisym_on_def)

lemma antisymp_on_bot[simp]: "antisymp_on A \"
  using antisym_on_bot[to_pred] .

lemma antisymp_on_mono_stronger:
  fixes
    A :: "'a set" and R :: "'a \ 'a \ bool" and
    B :: "'b set" and Q :: "'b \ 'b \ bool" and
    f :: "'a \ 'b"
  assumes "antisymp_on B Q" and "f ` A \ B" and
    Q_imp_R: "\x y. x \ A \ y \ A \ R x y \ Q (f x) (f y)" and
    inj_f: "inj_on f A"
  shows "antisymp_on A R"
proof (rule antisymp_onI)
  fix x y :: 'a
  assume "x \ A" and "y \ A" and "R x y" and "R y x"
  hence "Q (f x) (f y)" and "Q (f y) (f x)"
    using Q_imp_R by iprover+
  moreover have "f x \ B" and "f y \ B"
    using \<open>f ` A \<subseteq> B\<close> \<open>x \<in> A\<close> \<open>y \<in> A\<close> by blast+
  ultimately have "f x = f y"
    using \<open>antisymp_on B Q\<close>[THEN antisymp_onD] by iprover
  thus "x = y"
    using inj_f[THEN inj_onD] \<open>x \<in> A\<close> \<open>y \<in> A\<close> by iprover
qed

lemma antisymp_on_mono_strong:
  "antisymp_on B Q \ A \ B \ (\x y. x \ A \ y \ A \ R x y \ Q x y) \ antisymp_on A R"
  using antisymp_on_mono_stronger[of B Q "\x. x" A R, OF _ _ _ inj_on_id2, unfolded image_ident] .

lemma antisymp_on_mono[mono]: "A \ B \ R \ Q \ antisymp_on B Q \ antisymp_on A R"
  by (simp add: antisymp_on_mono_strong le_fun_def)

lemma antisym_on_subset: "antisym_on B r \ A \ B \ antisym_on A r"
  by (auto simp: antisym_on_def)

lemma antisymp_on_subset: "antisymp_on B R \ A \ B \ antisymp_on A R"
  using antisymp_on_mono_strong .

lemma antisymp_on_image:
  assumes "inj_on f A"
  shows "antisymp_on (f ` A) R \ antisymp_on A (\a b. R (f a) (f b))"
  using assms by (auto simp: antisymp_on_def inj_on_def)

lemma antisym_subset:
  "r \ s \ antisym s \ antisym r"
  unfolding antisym_def by blast

lemma antisymp_less_eq:
  "r \ s \ antisymp s \ antisymp r"
  by (fact antisym_subset [to_pred])

lemma antisymp_on_equality[simp]: "antisymp_on A (=)"
  by (auto intro: antisymp_onI)

lemma antisym_singleton [simp]:
  "antisym {x}"
  by (blast intro: antisymI)

lemma antisym_on_if_asym_on: "asym_on A r \ antisym_on A r"
  by (auto intro: antisym_onI dest: asym_onD)

lemma antisymp_on_if_asymp_on: "asymp_on A R \ antisymp_on A R"
  by (rule antisym_on_if_asym_on[to_pred])

lemma (in preorder) antisymp_on_less[simp]: "antisymp_on A (<)"
  by (rule antisymp_on_if_asymp_on[OF asymp_on_less])

lemma (in preorder) antisymp_on_greater[simp]: "antisymp_on A (>)"
  by (rule antisymp_on_if_asymp_on[OF asymp_on_greater])

lemma (in order) antisymp_on_le[simp]: "antisymp_on A (\)"
  by (simp add: antisymp_onI)

lemma (in order) antisymp_on_ge[simp]: "antisymp_on A (\)"
  by (simp add: antisymp_onI)

subsubsection \<open>Transitivity\<close>

definition trans_on :: "'a set \ 'a rel \ bool" where
  "trans_on A r \ (\x \ A. \y \ A. \z \ A. (x, y) \ r \ (y, z) \ r \ (x, z) \ r)"

abbreviation trans :: "'a rel \ bool" where
  "trans \ trans_on UNIV"

definition transp_on :: "'a set \ ('a \ 'a \ bool) \ bool" where
  "transp_on A R \ (\x \ A. \y \ A. \z \ A. R x y \ R y z \ R x z)"

abbreviation transp :: "('a \ 'a \ bool) \ bool" where
  "transp \ transp_on UNIV"

lemma trans_def[no_atp]: "trans r \ (\x y z. (x, y) \ r \ (y, z) \ r \ (x, z) \ r)"
  by (simp add: trans_on_def)

lemma transp_def: "transp R \ (\x y z. R x y \ R y z \ R x z)"
  by (simp add: transp_on_def)

text \<open>@{thm [source] trans_def} and @{thm [source] transp_def} are for backward compatibility.\<close>

lemma transp_on_trans_on_eq[pred_set_conv]: "transp_on A (\x y. (x, y) \ r) \ trans_on A r"
  by (simp add: trans_on_def transp_on_def)

lemmas transp_trans_eq = transp_on_trans_on_eq[of UNIV] \<comment> \<open>For backward compatibility\<close>

lemma trans_onI:
  "(\x y z. x \ A \ y \ A \ z \ A \ (x, y) \ r \ (y, z) \ r \ (x, z) \ r) \
  trans_on A r"
  unfolding trans_on_def
  by (intro ballI) iprover

lemma transI [intro?]: "(\x y z. (x, y) \ r \ (y, z) \ r \ (x, z) \ r) \ trans r"
  by (rule trans_onI)

lemma transp_onI:
  "(\x y z. x \ A \ y \ A \ z \ A \ R x y \ R y z \ R x z) \ transp_on A R"
  by (rule trans_onI[to_pred])

lemma transpI [intro?]: "(\x y z. R x y \ R y z \ R x z) \ transp R"
  by (rule transI[to_pred])

lemma transE:
  assumes "trans r" and "(x, y) \ r" and "(y, z) \ r"
  obtains "(x, z) \ r"
  using assms by (unfold trans_def) iprover

lemma transpE:
  assumes "transp r" and "r x y" and "r y z"
  obtains "r x z"
  using assms by (rule transE [to_pred])

lemma trans_onD:
  "trans_on A r \ x \ A \ y \ A \ z \ A \ (x, y) \ r \ (y, z) \ r \ (x, z) \ r"
  unfolding trans_on_def
  by (elim ballE) iprover+

lemma transD[dest?]: "trans r \ (x, y) \ r \ (y, z) \ r \ (x, z) \ r"
  by (simp add: trans_onD[of UNIV r x y z])

lemma transp_onD: "transp_on A R \ x \ A \ y \ A \ z \ A \ R x y \ R y z \ R x z"
  by (rule trans_onD[to_pred])

lemma transpD[dest?]: "transp R \ R x y \ R y z \ R x z"
  by (rule transD[to_pred])

lemma trans_on_subset: "trans_on B r \ A \ B \ trans_on A r"
  by (auto simp: trans_on_def)

lemma transp_on_subset: "transp_on B R \ A \ B \ transp_on A R"
  by (auto simp: transp_on_def)

lemma transp_on_image: "transp_on (f ` A) R \ transp_on A (\a b. R (f a) (f b))"
  by (simp add: transp_on_def)

lemma trans_Int: "trans r \ trans s \ trans (r \ s)"
  by (fast intro: transI elim: transE)

lemma transp_inf: "transp r \ transp s \ transp (r \ s)"
  by (fact trans_Int [to_pred])

lemma trans_INTER: "\x\S. trans (r x) \ trans (\(r ` S))"
  by (fast intro: transI elim: transD)

lemma transp_INF: "\x\S. transp (r x) \ transp (\(r ` S))"
  by (fact trans_INTER [to_pred])

lemma trans_on_join [code]:
  "trans_on A r \ (\(x, y1) \ r. x \ A \ y1 \ A \
    (\<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> z \<in> A \<longrightarrow> (x, z) \<in> r))"
  by (auto simp: trans_on_def)

lemma trans_join: "trans r \ (\(x, y1) \ r. \(y2, z) \ r. y1 = y2 \ (x, z) \ r)"
  by (auto simp add: trans_def)

lemma transp_trans: "transp r \ trans {(x, y). r x y}"
  by (simp add: trans_def transp_def)

lemma transp_on_equality[simp]: "transp_on A (=)"
  by (auto intro: transp_onI)

lemma trans_on_bot[simp]: "trans_on A \"
  by (simp add: trans_on_def)

lemma transp_on_bot[simp]: "transp_on A \"
  using trans_on_bot[to_pred] .

lemma trans_on_top[simp]: "trans_on A \"
  by (simp add: trans_on_def)

lemma transp_on_top[simp]: "transp_on A \"
  by (simp add: transp_on_def)

lemma transp_empty [simp]: "transp (\x y. False)"
  using transp_on_bot unfolding bot_fun_def bot_bool_def .

lemma trans_singleton [simp]: "trans {(a, a)}"
  by (blast intro: transI)

lemma transp_singleton [simp]: "transp (\x y. x = a \ y = a)"
  by (simp add: transp_def)

lemma asym_on_iff_irrefl_on_if_trans_on: "trans_on A r \ asym_on A r \ irrefl_on A r"
  by (auto intro: irrefl_on_if_asym_on dest: trans_onD irrefl_onD)

lemma asymp_on_iff_irreflp_on_if_transp_on: "transp_on A R \ asymp_on A R \ irreflp_on A R"
  by (rule asym_on_iff_irrefl_on_if_trans_on[to_pred])

lemma (in preorder) transp_on_le[simp]: "transp_on A (\)"
  by (auto intro: transp_onI order_trans)

lemma (in preorder) transp_on_less[simp]: "transp_on A (<)"
  by (auto intro: transp_onI less_trans)

lemma (in preorder) transp_on_ge[simp]: "transp_on A (\)"
  by (auto intro: transp_onI order_trans)

lemma (in preorder) transp_on_greater[simp]: "transp_on A (>)"
  by (auto intro: transp_onI less_trans)

subsubsection \<open>Totality\<close>

definition total_on :: "'a set \ 'a rel \ bool" where
  "total_on A r \ (\x\A. \y\A. x \ y \ (x, y) \ r \ (y, x) \ r)"

abbreviation total :: "'a rel \ bool" where
  "total \ total_on UNIV"

definition totalp_on :: "'a set \ ('a \ 'a \ bool) \ bool" where
  "totalp_on A R \ (\x \ A. \y \ A. x \ y \ R x y \ R y x)"

abbreviation totalp :: "('a \ 'a \ bool) \ bool" where
  "totalp \ totalp_on UNIV"

lemma totalp_on_total_on_eq[pred_set_conv]: "totalp_on A (\x y. (x, y) \ r) \ total_on A r"
  by (simp add: totalp_on_def total_on_def)

lemma total_onI [intro?]:
  "(\x y. x \ A \ y \ A \ x \ y \ (x, y) \ r \ (y, x) \ r) \ total_on A r"
  unfolding total_on_def by blast

lemma totalI: "(\x y. x \ y \ (x, y) \ r \ (y, x) \ r) \ total r"
  by (rule total_onI)

lemma totalp_onI: "(\x y. x \ A \ y \ A \ x \ y \ R x y \ R y x) \ totalp_on A R"
  by (rule total_onI[to_pred])

lemma totalpI: "(\x y. x \ y \ R x y \ R y x) \ totalp R"
  by (rule totalI[to_pred])

lemma totalp_onD:
  "totalp_on A R \ x \ A \ y \ A \ x \ y \ R x y \ R y x"
  by (simp add: totalp_on_def)

lemma totalpD: "totalp R \ x \ y \ R x y \ R y x"
  by (simp add: totalp_onD)

lemma total_on_top[simp]: "total_on A \"
  by (simp add: total_on_def)

lemma totalp_on_top[simp]: "totalp_on A \"
  by (simp add: totalp_on_def)

lemma totalp_on_mono_stronger:
  fixes
    A :: "'a set" and R :: "'a \ 'a \ bool" and
    B :: "'b set" and Q :: "'b \ 'b \ bool" and
    f :: "'a \ 'b"
  assumes "totalp_on B Q" and "f ` A \ B" and
    Q_imp_R: "\x y. x \ A \ y \ A \ Q (f x) (f y) \ R x y" and
    inj_f: "inj_on f A"
  shows "totalp_on A R"
proof (rule totalp_onI)
  fix x y :: 'a
  assume "x \ A" and "y \ A" and "x \ y"
  hence "f x \ B" and "f y \ B" and "f x \ f y"
    using \<open>f ` A \<subseteq> B\<close> inj_f by (auto dest: inj_onD)
  hence "Q (f x) (f y) \ Q (f y) (f x)"
    using \<open>totalp_on B Q\<close> by (iprover dest: totalp_onD)
  thus "R x y \ R y x"
    using Q_imp_R \<open>x \<in> A\<close> \<open>y \<in> A\<close> by iprover
qed

lemma totalp_on_mono_stronger_alt:
  fixes
    A :: "'a set" and R :: "'a \ 'a \ bool" and
    B :: "'b set" and Q :: "'b \ 'b \ bool" and
    f :: "'b \ 'a"
  assumes "totalp_on B Q" and "A \ f ` B" and
    Q_imp_R: "\x y. x \ B \ y \ B \ Q x y \ R (f x) (f y)"
  shows "totalp_on A R"
proof (rule totalp_onI)
  fix x y :: 'a
  assume "x \ A" and "y \ A" and "x \ y"
  then obtain x' y' where "x' \ B" and "x = f x'" and "y' \ B" and "y = f y'" and "x' \ y'"
    using \<open>A \<subseteq> f ` B\<close> by blast
  hence "Q x' y' \ Q y' x'"
    using \<open>totalp_on B Q\<close>[THEN totalp_onD] by blast
  hence "R (f x') (f y') \ R (f y') (f x')"
    using Q_imp_R \<open>x' \<in> B\<close> \<open>y' \<in> B\<close> by blast
  thus "R x y \ R y x"
    using \<open>x = f x'\<close> \<open>y = f y'\<close> by blast
qed

lemma totalp_on_mono_strong:
  "totalp_on B Q \ A \ B \ (\x y. x \ A \ y \ A \ Q x y \ R x y) \ totalp_on A R"
  using totalp_on_mono_stronger[of B Q "\x. x" A R, simplified] .

lemma totalp_on_mono[mono]: "A \ B \ Q \ R \ totalp_on B Q \ totalp_on A R"
  by (auto intro: totalp_on_mono_strong)

lemma total_on_subset: "total_on B r \ A \ B \ total_on A r"
  by (auto simp: total_on_def)

lemma totalp_on_subset: "totalp_on B R \ A \ B \ totalp_on A R"
  using totalp_on_mono_strong .

lemma totalp_on_image:
  assumes "inj_on f A"
  shows "totalp_on (f ` A) R \ totalp_on A (\a b. R (f a) (f b))"
  using assms by (auto simp: totalp_on_def inj_on_def)

lemma total_on_empty [simp]: "total_on {} r"
  by (simp add: total_on_def)

lemma totalp_on_empty [simp]: "totalp_on {} R"
  by (simp add: totalp_on_def)

lemma total_on_singleton [simp]: "total_on {x} r"
  by (simp add: total_on_def)

lemma totalp_on_singleton [simp]: "totalp_on {x} R"
  by (simp add: totalp_on_def)

lemma (in linorder) totalp_on_less[simp]: "totalp_on A (<)"
  by (auto intro: totalp_onI)

lemma (in linorder) totalp_on_greater[simp]: "totalp_on A (>)"
  by (auto intro: totalp_onI)

lemma (in linorder) totalp_on_le[simp]: "totalp_on A (\)"
  by (rule totalp_onI, rule linear)

lemma (in linorder) totalp_on_ge[simp]: "totalp_on A (\)"
  by (rule totalp_onI, rule linear)

subsubsection \<open>Left uniqueness\<close>

definition left_unique :: "('a \ 'b \ bool) \ bool" where
  "left_unique R \ (\x y z. R x z \ R y z \ x = y)"

lemma left_uniqueI: "(\x y z. A x z \ A y z \ x = y) \ left_unique A"
  unfolding left_unique_def by blast

lemma left_uniqueD: "left_unique A \ A x z \ A y z \ x = y"
  unfolding left_unique_def by blast

lemma left_unique_iff_Uniq: "left_unique r \ (\y. \\<^sub>\\<^sub>1x. r x y)"
  unfolding Uniq_def left_unique_def by blast

lemma left_unique_bot[simp]: "left_unique \"
  by (simp add: left_unique_def)

lemma left_unique_mono_strong:
  "left_unique Q \ (\x y. R x y \ Q x y) \ left_unique R"
  by (rule left_uniqueI) (auto dest: left_uniqueD)

lemma left_unique_mono[mono]: "R \ Q \ left_unique Q \ left_unique R"
  using left_unique_mono_strong[of Q R]
  by (simp add: le_fun_def)

subsubsection \<open>Right uniqueness\<close>

definition single_valued :: "('a \ 'b) set \ bool"
  where "single_valued r \ (\x y. (x, y) \ r \ (\z. (x, z) \ r \ y = z))"

definition right_unique :: "('a \ 'b \ bool) \ bool" where
  "right_unique R \ (\x y z. R x y \ R x z \ y = z)"

lemma right_unique_single_valued_eq [pred_set_conv]:
  "right_unique (\x y. (x, y) \ r) \ single_valued r"
  by (simp add: single_valued_def right_unique_def)

lemma right_unique_iff_Uniq:
  "right_unique r \ (\x. \\<^sub>\\<^sub>1y. r x y)"
  unfolding Uniq_def right_unique_def by auto

lemma single_valuedI:
  "(\x y. (x, y) \ r \ (\z. (x, z) \ r \ y = z)) \ single_valued r"
  unfolding single_valued_def by blast

lemma right_uniqueI: "(\x y z. R x y \ R x z \ y = z) \ right_unique R"
  unfolding right_unique_def by fast

lemma single_valuedD:
  "single_valued r \ (x, y) \ r \ (x, z) \ r \ y = z"
  by (simp add: single_valued_def)

lemma right_uniqueD: "right_unique R \ R x y \ R x z \ y = z"
  unfolding right_unique_def by fast

lemma single_valued_empty [simp]:
  "single_valued {}"
  by (simp add: single_valued_def)

lemma right_unique_bot[simp]: "right_unique \"
  by (fact single_valued_empty[to_pred])

lemma right_unique_mono_strong:
  "right_unique Q \ (\x y. R x y \ Q x y) \ right_unique R"
  by (rule right_uniqueI) (auto dest: right_uniqueD)

lemma right_unique_mono[mono]: "R \ Q \ right_unique Q \ right_unique R"
  using right_unique_mono_strong[of Q R]
  by (simp add: le_fun_def)

lemma single_valued_subset:
  "r \ s \ single_valued s \ single_valued r"
  unfolding single_valued_def by blast

lemma right_unique_less_eq: "r \ s \ right_unique s \ right_unique r"
  by (fact single_valued_subset [to_pred])

subsection \<open>Relation operations\<close>

subsubsection \<open>The identity relation\<close>

definition Id :: "'a rel"
  where "Id = {p. \x. p = (x, x)}"

lemma IdI [intro]: "(a, a) \ Id"
  by (simp add: Id_def)

lemma IdE [elim!]: "p \ Id \ (\x. p = (x, x) \ P) \ P"
  unfolding Id_def by (iprover elim: CollectE)

lemma pair_in_Id_conv [iff]: "(a, b) \ Id \ a = b"
  unfolding Id_def by blast

lemma refl_Id: "refl Id"
  by (simp add: refl_on_def)

lemma antisym_Id: "antisym Id"
  \<comment> \<open>A strange result, since \<open>Id\<close> is also symmetric.\<close>
  by (simp add: antisym_def)

lemma sym_Id: "sym Id"
  by (simp add: sym_def)

lemma trans_Id: "trans Id"
  by (simp add: trans_def)

lemma single_valued_Id [simp]: "single_valued Id"
  by (unfold single_valued_def) blast

lemma irrefl_diff_Id [simp]: "irrefl (r - Id)"
  by (simp add: irrefl_def)

lemma trans_on_diff_Id: "trans_on A r \ antisym_on A r \ trans_on A (r - Id)"
  by (blast intro: trans_onI dest: trans_onD antisym_onD)

lemma trans_diff_Id[no_atp]: "trans r \ antisym r \ trans (r - Id)"
  using trans_on_diff_Id .

lemma total_on_diff_Id [simp]: "total_on A (r - Id) = total_on A r"
  by (simp add: total_on_def)

lemma Id_fstsnd_eq: "Id = {x. fst x = snd x}"
  by force

subsubsection \<open>Diagonal: identity over a set\<close>

definition Id_on :: "'a set \ 'a rel"
  where "Id_on A = (\x\A. {(x, x)})"

lemma Id_on_empty [simp]: "Id_on {} = {}"
  by (simp add: Id_on_def)

lemma Id_on_eqI: "a = b \ a \ A \ (a, b) \ Id_on A"
  by (simp add: Id_on_def)

lemma Id_onI [intro!]: "a \ A \ (a, a) \ Id_on A"
  by (rule Id_on_eqI) (rule refl)

lemma Id_onE [elim!]: "c \ Id_on A \ (\x. x \ A \ c = (x, x) \ P) \ P"
  \<comment> \<open>The general elimination rule.\<close>
  unfolding Id_on_def by (iprover elim!: UN_E singletonE)

lemma Id_on_iff: "(x, y) \ Id_on A \ x = y \ x \ A"
  by blast

lemma Id_on_def' [nitpick_unfold]: "Id_on {x. A x} = Collect (\(x, y). x = y \ A x)"
  by auto

lemma Id_on_subset_Times: "Id_on A \ A \ A"
  by blast

lemma refl_on_Id_on: "refl_on A (Id_on A)"
  by (rule refl_onI[OF Id_onI])

lemma antisym_Id_on [simp]: "antisym (Id_on A)"
  unfolding antisym_def by blast

lemma sym_Id_on [simp]: "sym (Id_on A)"
  by (rule symI) clarify

lemma trans_Id_on [simp]: "trans (Id_on A)"
  by (fast intro: transI elim: transD)

lemma single_valued_Id_on [simp]: "single_valued (Id_on A)"
  unfolding single_valued_def by blast

subsubsection \<open>Composition\<close>

inductive_set relcomp  :: "('a \ 'b) set \ ('b \ 'c) set \ ('a \ 'c) set"
  for r :: "('a \ 'b) set" and s :: "('b \ 'c) set"
  where relcompI [intro]: "(a, b) \ r \ (b, c) \ s \ (a, c) \ relcomp r s"

open_bundle relcomp_syntax
begin
notation relcomp  (infixr \<open>O\<close> 75) and relcompp  (infixr \<open>OO\<close> 75)
end

lemmas relcomppI = relcompp.intros

text \<open>
  For historic reasons, the elimination rules are not wholly corresponding.
  Feel free to consolidate this.
\<close>

inductive_cases relcompEpair: "(a, c) \ r O s"
inductive_cases relcomppE [elim!]: "(r OO s) a c"

lemma relcompE [elim!]: "xz \ r O s \
  (\<And>x y z. xz = (x, z) \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, z) \<in> s  \<Longrightarrow> P) \<Longrightarrow> P"
  apply (cases xz)
  apply simp
  apply (erule relcompEpair)
  apply iprover
  done

lemma R_O_Id [simp]: "R O Id = R"
  by fast

lemma Id_O_R [simp]: "Id O R = R"
  by fast

lemma relcomp_empty1 [simp]: "{} O R = {}"
  by blast

lemma relcompp_bot1 [simp]: "\ OO R = \"
  by (fact relcomp_empty1 [to_pred])

lemma relcomp_empty2 [simp]: "R O {} = {}"
  by blast

lemma relcompp_bot2 [simp]: "R OO \ = \"
  by (fact relcomp_empty2 [to_pred])

lemma O_assoc: "(R O S) O T = R O (S O T)"
  by blast

lemma relcompp_assoc: "(r OO s) OO t = r OO (s OO t)"
  by (fact O_assoc [to_pred])

lemma trans_O_subset: "trans r \ r O r \ r"
  by (unfold trans_def) blast

lemma transp_relcompp_less_eq: "transp r \ r OO r \ r "
  by (fact trans_O_subset [to_pred])

lemma relcomp_mono: "r' \ r \ s' \ s \ r' O s' \ r O s"
  by blast

lemma relcompp_mono: "r' \ r \ s' \ s \ r' OO s' \ r OO s "
  by (fact relcomp_mono [to_pred])

lemma relcomp_subset_Sigma: "r \ A \ B \ s \ B \ C \ r O s \ A \ C"
  by blast

lemma relcomp_distrib [simp]: "R O (S \ T) = (R O S) \ (R O T)"
  by auto

lemma relcompp_distrib [simp]: "R OO (S \ T) = R OO S \ R OO T"
  by (fact relcomp_distrib [to_pred])

lemma relcomp_distrib2 [simp]: "(S \ T) O R = (S O R) \ (T O R)"
  by auto

lemma relcompp_distrib2 [simp]: "(S \ T) OO R = S OO R \ T OO R"
  by (fact relcomp_distrib2 [to_pred])

lemma relcomp_UNION_distrib: "s O \(r ` I) = (\i\I. s O r i) "
  by auto

lemma relcompp_SUP_distrib: "s OO \(r ` I) = (\i\I. s OO r i)"
  by (fact relcomp_UNION_distrib [to_pred])

lemma relcomp_UNION_distrib2: "\(r ` I) O s = (\i\I. r i O s) "
  by auto

lemma relcompp_SUP_distrib2: "\(r ` I) OO s = (\i\I. r i OO s)"
  by (fact relcomp_UNION_distrib2 [to_pred])

lemma single_valued_relcomp: "single_valued r \ single_valued s \ single_valued (r O s)"
  unfolding single_valued_def by blast

lemma relcomp_unfold: "r O s = {(x, z). \y. (x, y) \ r \ (y, z) \ s}"
  by (auto simp add: set_eq_iff)

lemma relcompp_apply: "(R OO S) a c \ (\b. R a b \ S b c)"
  unfolding relcomp_unfold [to_pred] ..

lemma eq_OO: "(=) OO R = R"
  by blast

lemma OO_eq: "R OO (=) = R"
  by blast

subsubsection \<open>Converse\<close>

inductive_set converse :: "('a \ 'b) set \ ('b \ 'a) set"
  for r :: "('a \ 'b) set"
  where "(a, b) \ r \ (b, a) \ converse r"

open_bundle converse_syntax
begin
notation
  converse  (\<open>(\<open>notation=\<open>postfix -1\<close>\<close>_\<inverse>)\<close> [1000] 999) and
  conversep  (\<open>(\<open>notation=\<open>postfix -1-1\<close>\<close>_\<inverse>\<inverse>)\<close> [1000] 1000)
notation (ASCII)
  converse  (\<open>(\<open>notation=\<open>postfix -1\<close>\<close>_^-1)\<close> [1000] 999) and
  conversep (\<open>(\<open>notation=\<open>postfix -1-1\<close>\<close>_^--1)\<close> [1000] 1000)
end

lemma converseI [sym]: "(a, b) \ r \ (b, a) \ r\"
  by (fact converse.intros)

lemma conversepI (* CANDIDATE [sym] *): "r a b \<Longrightarrow> r\<inverse>\<inverse> b a"
  by (fact conversep.intros)

lemma converseD [sym]: "(a, b) \ r\ \ (b, a) \ r"
  by (erule converse.cases) iprover

lemma conversepD (* CANDIDATE [sym] *): "r\<inverse>\<inverse> b a \<Longrightarrow> r a b"
  by (fact converseD [to_pred])

lemma converseE [elim!]: "yx \ r\ \ (\x y. yx = (y, x) \ (x, y) \ r \ P) \ P"
  \<comment> \<open>More general than \<open>converseD\<close>, as it ``splits'' the member of the relation.\<close>
  apply (cases yx)
  apply simp
  apply (erule converse.cases)
  apply iprover
  done

lemmas conversepE [elim!] = conversep.cases

lemma converse_iff [iff]: "(a, b) \ r\ \ (b, a) \ r"
  by (auto intro: converseI)

lemma conversep_iff [iff]: "r\\ a b = r b a"
  by (fact converse_iff [to_pred])

lemma converse_converse [simp]: "(r\)\ = r"
  by (simp add: set_eq_iff)

lemma conversep_conversep [simp]: "(r\\)\\ = r"
  by (fact converse_converse [to_pred])

lemma converse_empty[simp]: "{}\ = {}"
  by auto

lemma converse_UNIV[simp]: "UNIV\ = UNIV"
  by auto

lemma converse_relcomp: "(r O s)\ = s\ O r\"
  by blast

lemma converse_relcompp: "(r OO s)\\ = s\\ OO r\\"
  by (iprover intro: order_antisym conversepI relcomppI elim: relcomppE dest: conversepD)

lemma converse_Int: "(r \ s)\ = r\ \ s\"
  by blast

lemma converse_meet: "(r \ s)\\ = r\\ \ s\\"
  by (simp add: inf_fun_def) (iprover intro: conversepI ext dest: conversepD)

lemma converse_Un: "(r \ s)\ = r\ \ s\"
  by blast

lemma converse_join: "(r \ s)\\ = r\\ \ s\\"
  by (simp add: sup_fun_def) (iprover intro: conversepI ext dest: conversepD)

lemma converse_INTER: "(\(r ` S))\ = (\x\S. (r x)\)"
  by fast

lemma converse_UNION: "(\(r ` S))\ = (\x\S. (r x)\)"
  by blast

lemma converse_mono[simp]: "r\ \ s \ \ r \ s"
  by auto

lemma conversep_mono[simp]: "r\\ \ s \\ \ r \ s"
  by (fact converse_mono[to_pred])

lemma converse_inject[simp]: "r\ = s \ \ r = s"
  by auto

lemma conversep_inject[simp]: "r\\ = s \\ \ r = s"
  by (fact converse_inject[to_pred])

lemma converse_subset_swap: "r \ s \ \ r \ \ s"
  by auto

lemma conversep_le_swap: "r \ s \\ \ r \\ \ s"
  by (fact converse_subset_swap[to_pred])

lemma converse_Id [simp]: "Id\ = Id"
  by blast

lemma converse_Id_on [simp]: "(Id_on A)\ = Id_on A"
  by blast

lemma refl_on_converse [simp]: "refl_on A (r\) = refl_on A r"
  by (auto simp: refl_on_def)

lemma reflp_on_conversp [simp]: "reflp_on A R\\ \ reflp_on A R"
  by (auto simp: reflp_on_def)

lemma irrefl_on_converse [simp]: "irrefl_on A (r\) = irrefl_on A r"
  by (simp add: irrefl_on_def)

lemma irreflp_on_converse [simp]: "irreflp_on A (r\\) = irreflp_on A r"
  by (rule irrefl_on_converse[to_pred])

lemma sym_on_converse [simp]: "sym_on A (r\) = sym_on A r"
  by (auto intro: sym_onI dest: sym_onD)

lemma symp_on_conversep [simp]: "symp_on A R\\ = symp_on A R"
  by (rule sym_on_converse[to_pred])

lemma asym_on_converse [simp]: "asym_on A (r\) = asym_on A r"
  by (auto dest: asym_onD)

lemma asymp_on_conversep [simp]: "asymp_on A R\\ = asymp_on A R"
  by (rule asym_on_converse[to_pred])

lemma antisym_on_converse [simp]: "antisym_on A (r\) = antisym_on A r"
  by (auto intro: antisym_onI dest: antisym_onD)

lemma antisymp_on_conversep [simp]: "antisymp_on A R\\ = antisymp_on A R"
  by (rule antisym_on_converse[to_pred])

lemma trans_on_converse [simp]: "trans_on A (r\) = trans_on A r"
  by (auto intro: trans_onI dest: trans_onD)

lemma transp_on_conversep [simp]: "transp_on A R\\ = transp_on A R"
  by (rule trans_on_converse[to_pred])

lemma sym_conv_converse_eq: "sym r \ r\ = r"
  unfolding sym_def by fast

lemma sym_Un_converse: "sym (r \ r\)"
  unfolding sym_def by blast

lemma sym_Int_converse: "sym (r \ r\)"
  unfolding sym_def by blast

lemma total_on_converse [simp]: "total_on A (r\) = total_on A r"
  by (auto simp: total_on_def)

lemma totalp_on_converse [simp]: "totalp_on A R\\ = totalp_on A R"
  by (rule total_on_converse[to_pred])

lemma left_unique_conversep[simp]: "left_unique A\\ \ right_unique A"
  by (auto simp add: left_unique_def right_unique_def)

lemma right_unique_conversep[simp]: "right_unique A\\ \ left_unique A"
  by (auto simp add: left_unique_def right_unique_def)

lemma conversep_noteq [simp]: "(\)\\ = (\)"
  by (auto simp add: fun_eq_iff)

lemma conversep_eq [simp]: "(=)\\ = (=)"
  by (auto simp add: fun_eq_iff)

lemma converse_unfold [code]: "r\ = {(y, x). (x, y) \ r}"
  by (simp add: set_eq_iff)

subsubsection \<open>Domain, range and field\<close>

inductive_set Domain :: "('a \ 'b) set \ 'a set" for r :: "('a \ 'b) set"
  where DomainI [intro]: "(a, b) \ r \ a \ Domain r"

lemmas DomainPI = Domainp.DomainI

inductive_cases DomainE [elim!]: "a \ Domain r"
inductive_cases DomainpE [elim!]: "Domainp r a"

inductive_set Range :: "('a \ 'b) set \ 'b set" for r :: "('a \ 'b) set"
  where RangeI [intro]: "(a, b) \ r \ b \ Range r"

lemmas RangePI = Rangep.RangeI

inductive_cases RangeE [elim!]: "b \ Range r"
inductive_cases RangepE [elim!]: "Rangep r b"

definition Field :: "'a rel \ 'a set"
  where "Field r = Domain r \ Range r"

lemma Field_iff: "x \ Field r \ (\y. (x,y) \ r \ (y,x) \ r)"
  by (auto simp: Field_def)

lemma FieldI1: "(i, j) \ R \ i \ Field R"
  unfolding Field_def by blast

lemma FieldI2: "(i, j) \ R \ j \ Field R"
  unfolding Field_def by auto

lemma Domain_fst [code]: "Domain r = fst ` r"
  by force

lemma Range_snd [code]: "Range r = snd ` r"
  by force

lemma fst_eq_Domain: "fst ` R = Domain R"
  by force

lemma snd_eq_Range: "snd ` R = Range R"
  by force

lemma range_fst [simp]: "range fst = UNIV"
  by (auto simp: fst_eq_Domain)

lemma range_snd [simp]: "range snd = UNIV"
  by (auto simp: snd_eq_Range)

lemma Domain_empty [simp]: "Domain {} = {}"
  by auto

lemma Range_empty [simp]: "Range {} = {}"
  by auto

lemma Field_empty [simp]: "Field {} = {}"
  by (simp add: Field_def)

lemma Domain_empty_iff: "Domain r = {} \ r = {}"
  by auto

lemma Range_empty_iff: "Range r = {} \ r = {}"
  by auto

lemma Domain_insert [simp]: "Domain (insert (a, b) r) = insert a (Domain r)"
  by blast

lemma Range_insert [simp]: "Range (insert (a, b) r) = insert b (Range r)"
  by blast

lemma Field_insert [simp]: "Field (insert (a, b) r) = {a, b} \ Field r"
  by (auto simp add: Field_def)

lemma Domain_iff: "a \ Domain r \ (\y. (a, y) \ r)"
  by blast

lemma Range_iff: "a \ Range r \ (\y. (y, a) \ r)"
  by blast

lemma Domain_Id [simp]: "Domain Id = UNIV"
  by blast

lemma Range_Id [simp]: "Range Id = UNIV"
  by blast

lemma Domain_Id_on [simp]: "Domain (Id_on A) = A"
  by blast

lemma Range_Id_on [simp]: "Range (Id_on A) = A"
  by blast

lemma Domain_Un_eq: "Domain (A \ B) = Domain A \ Domain B"
  by blast

lemma Range_Un_eq: "Range (A \ B) = Range A \ Range B"
  by blast

lemma Field_Un [simp]: "Field (r \ s) = Field r \ Field s"
  by (auto simp: Field_def)

lemma Domain_Int_subset: "Domain (A \ B) \ Domain A \ Domain B"
  by blast

lemma Range_Int_subset: "Range (A \ B) \ Range A \ Range B"
  by blast

lemma Domain_Diff_subset: "Domain A - Domain B \ Domain (A - B)"
  by blast

lemma Range_Diff_subset: "Range A - Range B \ Range (A - B)"
  by blast

lemma Domain_Union: "Domain (\S) = (\A\S. Domain A)"
  by blast

lemma Range_Union: "Range (\S) = (\A\S. Range A)"
  by blast

lemma Field_Union [simp]: "Field (\R) = \(Field ` R)"
  by (auto simp: Field_def)

lemma Domain_converse [simp]: "Domain (r\) = Range r"
  by auto

lemma Range_converse [simp]: "Range (r\) = Domain r"
  by blast

lemma Field_converse [simp]: "Field (r\) = Field r"
  by (auto simp: Field_def)

lemma Domain_Collect_case_prod [simp]: "Domain {(x, y). P x y} = {x. \y. P x y}"
  by auto

lemma Range_Collect_case_prod [simp]: "Range {(x, y). P x y} = {y. \x. P x y}"
  by auto

lemma Domain_mono: "r \ s \ Domain r \ Domain s"
  by blast

lemma Range_mono: "r \ s \ Range r \ Range s"
  by blast

lemma mono_Field: "r \ s \ Field r \ Field s"
  by (auto simp: Field_def Domain_def Range_def)

lemma Domain_unfold: "Domain r = {x. \y. (x, y) \ r}"
  by blast

lemma Field_square [simp]: "Field (x \ x) = x"
  unfolding Field_def by blast

subsubsection \<open>Image of a set under a relation\<close>

definition Image :: "('a \ 'b) set \ 'a set \ 'b set" (infixr \``\ 90)
  where "r `` s = {y. \x\s. (x, y) \ r}"

lemma Image_iff: "b \ r``A \ (\x\A. (x, b) \ r)"
  by (simp add: Image_def)

lemma Image_singleton: "r``{a} = {b. (a, b) \ r}"
  by (simp add: Image_def)

lemma Image_singleton_iff [iff]: "b \ r``{a} \ (a, b) \ r"
  by (rule Image_iff [THEN trans]) simp

lemma ImageI [intro]: "(a, b) \ r \ a \ A \ b \ r``A"
  unfolding Image_def by blast

lemma ImageE [elim!]: "b \ r `` A \ (\x. (x, b) \ r \ x \ A \ P) \ P"
  unfolding Image_def by (iprover elim!: CollectE bexE)

lemma rev_ImageI: "a \ A \ (a, b) \ r \ b \ r `` A"
  \<comment> \<open>This version's more effective when we already have the required \<open>a\<close>\<close>
  by blast

lemma Image_empty1 [simp]: "{} `` X = {}"
by auto

lemma Image_empty2 [simp]: "R``{} = {}"
by blast

lemma Image_Id [simp]: "Id `` A = A"
  by blast

lemma Image_Id_on [simp]: "Id_on A `` B = A \ B"
  by blast

lemma Image_Int_subset: "R `` (A \ B) \ R `` A \ R `` B"
  by blast

lemma Image_Int_eq: "single_valued (converse R) \ R `` (A \ B) = R `` A \ R `` B"
  by (auto simp: single_valued_def)

lemma Image_Un: "R `` (A \ B) = R `` A \ R `` B"
  by blast

lemma Un_Image: "(R \ S) `` A = R `` A \ S `` A"
  by blast

lemma Image_subset: "r \ A \ B \ r``C \ B"
  by (iprover intro!: subsetI elim!: ImageE dest!: subsetD SigmaD2)

lemma Image_eq_UN: "r``B = (\y\ B. r``{y})"
  \<comment> \<open>NOT suitable for rewriting\<close>
  by blast

lemma Image_mono: "r' \ r \ A' \ A \ (r' `` A') \ (r `` A)"
  by blast

lemma Image_UN: "r `` (\(B ` A)) = (\x\A. r `` (B x))"
  by blast

lemma UN_Image: "(\i\I. X i) `` S = (\i\I. X i `` S)"
  by auto

lemma Image_INT_subset: "(r `` (\(B ` A))) \ (\x\A. r `` (B x))"
  by blast

text \<open>Converse inclusion requires some assumptions\<close>
lemma Image_INT_eq:
  assumes "single_valued (r\)"
    and "A \ {}"
  shows "r `` (\(B ` A)) = (\x\A. r `` B x)"
proof(rule equalityI, rule Image_INT_subset)
  show "(\x\A. r `` B x) \ r `` \ (B ` A)"
  proof
    fix x
    assume "x \ (\x\A. r `` B x)"
    then show "x \ r `` \ (B ` A)"
      using assms unfolding single_valued_def by simp blast
  qed
qed

lemma Image_subset_eq: "r``A \ B \ A \ - ((r\) `` (- B))"
  by blast

lemma Image_Collect_case_prod [simp]: "{(x, y). P x y} `` A = {y. \x\A. P x y}"
  by auto

lemma Sigma_Image: "(SIGMA x:A. B x) `` X = (\x\X \ A. B x)"
  by auto

--> --------------------

--> maximum size reached

--> --------------------

quality100%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.