# HG changeset patch
# User desharna
# Date 1671447656 -3600
# Node ID e65a50f6c2de22030947341855a9e5141b7ec04c
# Parent  e19a3dbbf5de67f8b2923053bd5b36edcb8e5ca4
added lemma refl_lex_prod[simp]

diff -r e19a3dbbf5de -r e65a50f6c2de NEWS
--- a/NEWS	Mon Dec 19 12:00:15 2022 +0100
+++ b/NEWS	Mon Dec 19 12:00:56 2022 +0100
@@ -124,6 +124,7 @@
       asym_on_lex_prod[simp]
       irrefl_lex_prod[simp]
       irrefl_on_lex_prod[simp]
+      refl_lex_prod[simp]
       sym_lex_prod[simp]
       sym_on_lex_prod[simp]
       wfP_if_convertible_to_nat
diff -r e19a3dbbf5de -r e65a50f6c2de src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Mon Dec 19 12:00:15 2022 +0100
+++ b/src/HOL/Wellfounded.thy	Mon Dec 19 12:00:56 2022 +0100
@@ -849,6 +849,9 @@
     by (simp add: zeq)
 qed auto
 
+lemma refl_lex_prod[simp]: "refl r\<^sub>B \<Longrightarrow> refl (r\<^sub>A <*lex*> r\<^sub>B)"
+  by (auto intro!: reflI dest: refl_onD)
+
 lemma irrefl_on_lex_prod[simp]:
   "irrefl_on A r\<^sub>A \<Longrightarrow> irrefl_on B r\<^sub>B \<Longrightarrow> irrefl_on (A \<times> B) (r\<^sub>A <*lex*> r\<^sub>B)"
   by (auto intro!: irrefl_onI dest: irrefl_onD)