--- 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]
--- 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])