# HG changeset patch
# User desharna
# Date 1742821700 -3600
# Node ID df714fc6c6bb2026f50b428aee7c7b95e47fe5e6
# Parent  81c920587d49fad2527d6f6ab2240d72a119cffe
moved lemmas around

diff -r 81c920587d49 -r df714fc6c6bb src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Mon Mar 24 14:05:55 2025 +0100
+++ b/src/HOL/Relation.thy	Mon Mar 24 14:08:20 2025 +0100
@@ -209,6 +209,13 @@
 lemma reflp_on_top[simp]: "reflp_on A \<top>"
   by (simp add: reflp_on_def)
 
+lemma reflp_on_mono_strong:
+  "reflp_on B R \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> R x y \<Longrightarrow> Q x y) \<Longrightarrow> reflp_on A Q"
+  by (rule reflp_onI) (auto dest: reflp_onD)
+
+lemma reflp_on_mono[mono]: "A \<subseteq> B \<Longrightarrow> R \<le> Q \<Longrightarrow> reflp_on B R \<le> reflp_on A Q"
+  by (simp add: reflp_on_mono_strong le_fun_def)
+
 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)
 
@@ -257,13 +264,6 @@
 lemma reflp_on_equality [simp]: "reflp_on A (=)"
   by (simp add: reflp_on_def)
 
-lemma reflp_on_mono_strong:
-  "reflp_on B R \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> R x y \<Longrightarrow> Q x y) \<Longrightarrow> reflp_on A Q"
-  by (rule reflp_onI) (auto dest: reflp_onD)
-
-lemma reflp_on_mono[mono]: "A \<subseteq> B \<Longrightarrow> R \<le> Q \<Longrightarrow> reflp_on B R \<le> reflp_on A Q"
-  by (simp add: reflp_on_mono_strong le_fun_def)
-
 lemma (in preorder) reflp_on_le[simp]: "reflp_on A (\<le>)"
   by (simp add: reflp_onI)