# HG changeset patch
# User desharna
# Date 1671445408 -3600
# Node ID 2f8219460ac9f526434877fa0c4450e4ad327442
# Parent  0fbe27cf295a63c2a7af65d819d2cd488cee858d
added lemmas irrefl_on_lex_prod[simp] and irrefl_lex_prod[simp]

diff -r 0fbe27cf295a -r 2f8219460ac9 NEWS
--- a/NEWS	Mon Dec 19 08:44:18 2022 +0100
+++ b/NEWS	Mon Dec 19 11:23:28 2022 +0100
@@ -118,6 +118,8 @@
 
 * Theory "HOL.Wellfounded":
   - Added lemmas.
+      irrefl_lex_prod[simp]
+      irrefl_on_lex_prod[simp]
       wfP_if_convertible_to_nat
       wfP_if_convertible_to_wfP
       wf_if_convertible_to_wf
diff -r 0fbe27cf295a -r 2f8219460ac9 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Mon Dec 19 08:44:18 2022 +0100
+++ b/src/HOL/Wellfounded.thy	Mon Dec 19 11:23:28 2022 +0100
@@ -849,19 +849,27 @@
     by (simp add: zeq)
 qed auto
 
+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)
+
+lemma irrefl_lex_prod[simp]: "irrefl r\<^sub>A \<Longrightarrow> irrefl r\<^sub>B \<Longrightarrow> irrefl (r\<^sub>A <*lex*> r\<^sub>B)"
+  by (rule irrefl_on_lex_prod[of UNIV _ UNIV, unfolded UNIV_Times_UNIV])
+
 text \<open>\<open><*lex*>\<close> preserves transitivity\<close>
 lemma trans_lex_prod [simp,intro!]: "trans R1 \<Longrightarrow> trans R2 \<Longrightarrow> trans (R1 <*lex*> R2)"
   unfolding trans_def lex_prod_def by blast
 
-lemma total_on_lex_prod [simp]: "total_on A r \<Longrightarrow> total_on B s \<Longrightarrow> total_on (A \<times> B) (r <*lex*> s)"
+lemma total_on_lex_prod[simp]:
+  "total_on A r\<^sub>A \<Longrightarrow> total_on B r\<^sub>B \<Longrightarrow> total_on (A \<times> B) (r\<^sub>A <*lex*> r\<^sub>B)"
   by (auto simp: total_on_def)
 
+lemma total_lex_prod[simp]: "total r\<^sub>A \<Longrightarrow> total r\<^sub>B \<Longrightarrow> total (r\<^sub>A <*lex*> r\<^sub>B)"
+  by (rule total_on_lex_prod[of UNIV _ UNIV, unfolded UNIV_Times_UNIV])
+
 lemma asym_lex_prod: "\<lbrakk>asym R; asym S\<rbrakk> \<Longrightarrow> asym (R <*lex*> S)"
   by (auto simp add: asym_iff lex_prod_def)
 
-lemma total_lex_prod [simp]: "total r \<Longrightarrow> total s \<Longrightarrow> total (r <*lex*> s)"
-  by (auto simp: total_on_def)
-
 text \<open>lexicographic combinations with measure functions\<close>
 
 definition mlex_prod :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (infixr "<*mlex*>" 80)