# HG changeset patch
# User desharna
# Date 1710525255 -3600
# Node ID 1f509d01c9e349d6cb5f926c7569a905451376a5
# Parent  c73a36081b1c5a6448c80a1bbffc91a399bd2522
added lemmas antisymp_on_image, asymp_on_image, irreflp_on_image, reflp_on_image, symp_on_image, totalp_on_image, and transp_on_image

diff -r c73a36081b1c -r 1f509d01c9e3 NEWS
--- a/NEWS	Fri Mar 15 17:57:03 2024 +0100
+++ b/NEWS	Fri Mar 15 18:54:15 2024 +0100
@@ -65,6 +65,16 @@
 * Lemma even_succ_div_2 renamed to even_half_succ_eq. Minor
 INCOMPATIBILITY.
 
+* Theory "HOL.Relation":
+  - Added lemmas.
+      antisymp_on_image
+      asymp_on_image
+      irreflp_on_image
+      reflp_on_image
+      symp_on_image
+      totalp_on_image
+      transp_on_image
+
 * Theory "HOL.Transitive_Closure":
   - Added lemmas.
       reflclp_greater_eq[simp]
diff -r c73a36081b1c -r 1f509d01c9e3 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Fri Mar 15 17:57:03 2024 +0100
+++ b/src/HOL/Relation.thy	Fri Mar 15 18:54:15 2024 +0100
@@ -210,6 +210,9 @@
 lemma reflp_on_subset: "reflp_on A R \<Longrightarrow> B \<subseteq> A \<Longrightarrow> reflp_on B R"
   by (auto intro: reflp_onI dest: reflp_onD)
 
+lemma reflp_on_image: "reflp_on (f ` A) R \<longleftrightarrow> reflp_on A (\<lambda>a b. R (f a) (f b))"
+  by (simp add: reflp_on_def)
+
 lemma refl_on_Int: "refl_on A r \<Longrightarrow> refl_on B s \<Longrightarrow> refl_on (A \<inter> B) (r \<inter> s)"
   unfolding refl_on_def by blast
 
@@ -332,6 +335,9 @@
 lemma irreflp_on_subset: "irreflp_on A R \<Longrightarrow> B \<subseteq> A \<Longrightarrow> irreflp_on B R"
   by (auto simp: irreflp_on_def)
 
+lemma irreflp_on_image: "irreflp_on (f ` A) R \<longleftrightarrow> irreflp_on A (\<lambda>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)
 
@@ -393,6 +399,9 @@
 lemma asymp_on_subset: "asymp_on A R \<Longrightarrow> B \<subseteq> A \<Longrightarrow> asymp_on B R"
   by (auto simp: asymp_on_def)
 
+lemma asymp_on_image: "asymp_on (f ` A) R \<longleftrightarrow> asymp_on A (\<lambda>a b. R (f a) (f b))"
+  by (simp add: asymp_on_def)
+
 lemma irrefl_on_if_asym_on[simp]: "asym_on A r \<Longrightarrow> irrefl_on A r"
   by (auto intro: irrefl_onI dest: asym_onD)
 
@@ -439,6 +448,9 @@
 lemma symp_on_subset: "symp_on A R \<Longrightarrow> B \<subseteq> A \<Longrightarrow> symp_on B R"
   by (auto simp: symp_on_def)
 
+lemma symp_on_image: "symp_on (f ` A) R \<longleftrightarrow> symp_on A (\<lambda>a b. R (f a) (f b))"
+  by (simp add: symp_on_def)
+
 lemma sym_onI: "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, x) \<in> r) \<Longrightarrow> sym_on A r"
   by (simp add: sym_on_def)
 
@@ -532,6 +544,11 @@
 lemma antisymp_on_subset: "antisymp_on A R \<Longrightarrow> B \<subseteq> A \<Longrightarrow> antisymp_on B R"
   by (auto simp: antisymp_on_def)
 
+lemma antisymp_on_image:
+  assumes "inj_on f A"
+  shows "antisymp_on (f ` A) R \<longleftrightarrow> antisymp_on A (\<lambda>a b. R (f a) (f b))"
+  using assms by (auto simp: antisymp_on_def inj_on_def)
+
 lemma antisym_onI:
   "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, x) \<in> r \<Longrightarrow> x = y) \<Longrightarrow> antisym_on A r"
   unfolding antisym_on_def by simp
@@ -680,6 +697,9 @@
 lemma transp_on_subset: "transp_on A R \<Longrightarrow> B \<subseteq> A \<Longrightarrow> transp_on B R"
   by (auto simp: transp_on_def)
 
+lemma transp_on_image: "transp_on (f ` A) R \<longleftrightarrow> transp_on A (\<lambda>a b. R (f a) (f b))"
+  by (simp add: transp_on_def)
+
 lemma trans_Int: "trans r \<Longrightarrow> trans s \<Longrightarrow> trans (r \<inter> s)"
   by (fast intro: transI elim: transE)
 
@@ -780,6 +800,11 @@
 lemma totalp_on_subset: "totalp_on A R \<Longrightarrow> B \<subseteq> A \<Longrightarrow> totalp_on B R"
   by (auto intro: totalp_onI dest: totalp_onD)
 
+lemma totalp_on_image:
+  assumes "inj_on f A"
+  shows "totalp_on (f ` A) R \<longleftrightarrow> totalp_on A (\<lambda>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)