# HG changeset patch
# User desharna
# Date 1671093890 -3600
# Node ID d8ca2d0e81e57cbb4653700fc4a46e4e113a6e37
# Parent  6b75499e52d1c0a5a8bf6e72fa5e216dd8abd8b9
added lemma antisymp_reflcp

diff -r 6b75499e52d1 -r d8ca2d0e81e5 NEWS
--- a/NEWS	Thu Dec 15 10:25:55 2022 +0100
+++ b/NEWS	Thu Dec 15 09:44:50 2022 +0100
@@ -72,9 +72,11 @@
       totalp_on_singleton[simp]
 
 * Theory "HOL.Transitive_Closure":
-  - Strengthened lemma reflp_rtranclp and renamed to reflp_on_rtranclp.
-    Minor INCOMPATIBILITY.
+  - Strengthened (and renamed) lemmas. Minor INCOMPATIBILITY.
+      antisym_reflcl[simp] ~> antisym_on_reflcl[simp]
+      reflp_rtranclp[simp] ~> reflp_on_rtranclp[simp]
   - Added lemmas.
+      antisymp_on_reflcp[simp]
       reflclp_ident_if_reflp[simp]
       reflp_on_reflclp[simp]
       transp_reflclp[simp]
diff -r 6b75499e52d1 -r d8ca2d0e81e5 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Thu Dec 15 10:25:55 2022 +0100
+++ b/src/HOL/Transitive_Closure.thy	Thu Dec 15 09:44:50 2022 +0100
@@ -67,14 +67,20 @@
 
 subsection \<open>Reflexive closure\<close>
 
+lemma reflcl_set_eq [pred_set_conv]: "(sup (\<lambda>x y. (x, y) \<in> r) (=)) = (\<lambda>x y. (x, y) \<in> r \<union> Id)"
+  by (auto simp: fun_eq_iff)
+
 lemma refl_reflcl[simp]: "refl (r\<^sup>=)"
   by (simp add: refl_on_def)
 
 lemma reflp_on_reflclp[simp]: "reflp_on A R\<^sup>=\<^sup>="
   by (simp add: reflp_on_def)
 
-lemma antisym_reflcl[simp]: "antisym (r\<^sup>=) = antisym r"
-  by (simp add: antisym_def)
+lemma antisym_on_reflcl[simp]: "antisym_on A (r\<^sup>=) \<longleftrightarrow> antisym_on A r"
+  by (simp add: antisym_on_def)
+
+lemma antisymp_on_reflcp[simp]: "antisymp_on A R\<^sup>=\<^sup>= \<longleftrightarrow> antisymp_on A R"
+  by (rule antisym_on_reflcl[to_pred])
 
 lemma trans_reflclI[simp]: "trans r \<Longrightarrow> trans (r\<^sup>=)"
   unfolding trans_def by blast
@@ -91,9 +97,6 @@
 
 subsection \<open>Reflexive-transitive closure\<close>
 
-lemma reflcl_set_eq [pred_set_conv]: "(sup (\<lambda>x y. (x, y) \<in> r) (=)) = (\<lambda>x y. (x, y) \<in> r \<union> Id)"
-  by (auto simp: fun_eq_iff)
-
 lemma r_into_rtrancl [intro]: "\<And>p. p \<in> r \<Longrightarrow> p \<in> r\<^sup>*"
   \<comment> \<open>\<open>rtrancl\<close> of \<open>r\<close> contains \<open>r\<close>\<close>
   by (simp add: split_tupled_all rtrancl_refl [THEN rtrancl_into_rtrancl])