# HG changeset patch
# User desharna
# Date 1709201906 -3600
# Node ID ba8fb71587ae42a7947172a1361f73688153fc51
# Parent  1f7dcfdb3e671a537a49f2092f9227b2f144aeef
added lemmas reflclp_(less|greater)_eq[simp], rtranclp_(less|greater)_eq[simp], and tranclp_(less|greater|less_eq|greater_eq)[simp]

diff -r 1f7dcfdb3e67 -r ba8fb71587ae NEWS
--- a/NEWS	Wed Mar 06 21:52:58 2024 +0100
+++ b/NEWS	Thu Feb 29 11:18:26 2024 +0100
@@ -64,14 +64,22 @@
 
 * Theory "HOL.Transitive_Closure":
   - Added lemmas.
+      reflclp_greater_eq[simp]
+      reflclp_less_eq[simp]
       relpow_left_unique
       relpow_right_unique
       relpow_trans[trans]
       relpowp_left_unique
       relpowp_right_unique
       relpowp_trans[trans]
+      rtranclp_greater_eq[simp]
       rtranclp_ident_if_reflp_and_transp
+      rtranclp_less_eq[simp]
+      tranclp_greater[simp]
+      tranclp_greater_eq[simp]
       tranclp_ident_if_and_transp
+      tranclp_less[simp]
+      tranclp_less_eq[simp]
 
 * Theory "HOL-Library.Multiset":
   - Added lemmas.
diff -r 1f7dcfdb3e67 -r ba8fb71587ae src/HOL/Library/Numeral_Type.thy
--- a/src/HOL/Library/Numeral_Type.thy	Wed Mar 06 21:52:58 2024 +0100
+++ b/src/HOL/Library/Numeral_Type.thy	Thu Feb 29 11:18:26 2024 +0100
@@ -360,9 +360,6 @@
     (auto simp add: less_eq_bit0_def less_bit0_def less_eq_bit1_def less_bit1_def Rep_bit0_inject Rep_bit1_inject)
 end
 
-lemma (in preorder) tranclp_less: "(<) \<^sup>+\<^sup>+ = (<)"
-by(auto simp add: fun_eq_iff intro: less_trans elim: tranclp.induct)
-
 instance bit0 and bit1 :: (finite) wellorder
 proof -
   have "wf {(x :: 'a bit0, y). x < y}"
diff -r 1f7dcfdb3e67 -r ba8fb71587ae src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Wed Mar 06 21:52:58 2024 +0100
+++ b/src/HOL/Transitive_Closure.thy	Thu Feb 29 11:18:26 2024 +0100
@@ -94,6 +94,15 @@
 lemma reflclp_ident_if_reflp[simp]: "reflp R \<Longrightarrow> R\<^sup>=\<^sup>= = R"
   by (auto dest: reflpD)
 
+text \<open>The following are special cases of @{thm [source] reflclp_ident_if_reflp},
+but they appear duplicated in multiple, independent theories, which causes name clashes.\<close>
+
+lemma (in preorder) reflclp_less_eq[simp]: "(\<le>)\<^sup>=\<^sup>= = (\<le>)"
+  using reflp_on_le by (simp only: reflclp_ident_if_reflp)
+
+lemma (in preorder) reflclp_greater_eq[simp]: "(\<ge>)\<^sup>=\<^sup>= = (\<ge>)"
+  using reflp_on_ge by (simp only: reflclp_ident_if_reflp)
+
 
 subsection \<open>Reflexive-transitive closure\<close>
 
@@ -342,6 +351,15 @@
     using r_into_rtranclp .
 qed
 
+text \<open>The following are special cases of @{thm [source] rtranclp_ident_if_reflp_and_transp},
+but they appear duplicated in multiple, independent theories, which causes name clashes.\<close>
+
+lemma (in preorder) rtranclp_less_eq[simp]: "(\<le>)\<^sup>*\<^sup>* = (\<le>)"
+  using reflp_on_le transp_on_le by (simp only: rtranclp_ident_if_reflp_and_transp)
+
+lemma (in preorder) rtranclp_greater_eq[simp]: "(\<ge>)\<^sup>*\<^sup>* = (\<ge>)"
+  using reflp_on_ge transp_on_ge by (simp only: rtranclp_ident_if_reflp_and_transp)
+
 
 subsection \<open>Transitive closure\<close>
 
@@ -777,6 +795,20 @@
     using tranclp.r_into_trancl .
 qed
 
+text \<open>The following are special cases of @{thm [source] tranclp_ident_if_transp},
+but they appear duplicated in multiple, independent theories, which causes name clashes.\<close>
+
+lemma (in preorder) tranclp_less[simp]: "(<)\<^sup>+\<^sup>+ = (<)"
+  using transp_on_less by (simp only: tranclp_ident_if_transp)
+
+lemma (in preorder) tranclp_less_eq[simp]: "(\<le>)\<^sup>+\<^sup>+ = (\<le>)"
+  using transp_on_le by (simp only: tranclp_ident_if_transp)
+
+lemma (in preorder) tranclp_greater[simp]: "(>)\<^sup>+\<^sup>+ = (>)"
+  using transp_on_greater by (simp only: tranclp_ident_if_transp)
+
+lemma (in preorder) tranclp_greater_eq[simp]: "(\<ge>)\<^sup>+\<^sup>+ = (\<ge>)"
+  using transp_on_ge by (simp only: tranclp_ident_if_transp)
 
 subsection \<open>Symmetric closure\<close>