# HG changeset patch
# User desharna
# Date 1742806397 -3600
# Node ID 3726705befa546eec2b4f5f102f870f69a96ccb3
# Parent  81715228617c1a8839964d1a5ce29b2cb36981ba
moved lemmas around

diff -r 81715228617c -r 3726705befa5 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Mon Mar 24 09:04:53 2025 +0100
+++ b/src/HOL/Relation.thy	Mon Mar 24 09:53:17 2025 +0100
@@ -563,23 +563,6 @@
 
 lemmas antisymp_antisym_eq = antisymp_on_antisym_on_eq[of UNIV] \<comment> \<open>For backward compatibility\<close>
 
-lemma antisym_on_bot[simp]: "antisym_on A \<bottom>"
-  by (simp add: antisym_on_def)
-
-lemma antisymp_on_bot[simp]: "antisymp_on A \<bottom>"
-  using antisym_on_bot[to_pred] .
-
-lemma antisym_on_subset: "antisym_on A r \<Longrightarrow> B \<subseteq> A \<Longrightarrow> antisym_on B r"
-  by (auto simp: antisym_on_def)
-
-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
@@ -612,6 +595,23 @@
   "antisymp R \<Longrightarrow> R x y \<Longrightarrow> R y x \<Longrightarrow> x = y"
   by (rule antisymD[to_pred])
 
+lemma antisym_on_bot[simp]: "antisym_on A \<bottom>"
+  by (simp add: antisym_on_def)
+
+lemma antisymp_on_bot[simp]: "antisymp_on A \<bottom>"
+  using antisym_on_bot[to_pred] .
+
+lemma antisym_on_subset: "antisym_on A r \<Longrightarrow> B \<subseteq> A \<Longrightarrow> antisym_on B r"
+  by (auto simp: antisym_on_def)
+
+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_subset:
   "r \<subseteq> s \<Longrightarrow> antisym s \<Longrightarrow> antisym r"
   unfolding antisym_def by blast