# HG changeset patch
# User desharna
# Date 1671463257 -3600
# Node ID 91d2903bfbcbd25ba92c4beef3e2258624f537dd
# Parent  66cae055ac7b0ba84ad4fd9102e906d98322c9b3
added lemma trans_on_lex_prod[simp]

diff -r 66cae055ac7b -r 91d2903bfbcb NEWS
--- a/NEWS	Mon Dec 19 16:12:17 2022 +0100
+++ b/NEWS	Mon Dec 19 16:20:57 2022 +0100
@@ -145,6 +145,7 @@
       refl_lex_prod[simp]
       sym_lex_prod[simp]
       sym_on_lex_prod[simp]
+      trans_on_lex_prod[simp]
       wfP_if_convertible_to_nat
       wfP_if_convertible_to_wfP
       wf_if_convertible_to_wf
diff -r 66cae055ac7b -r 91d2903bfbcb src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Mon Dec 19 16:12:17 2022 +0100
+++ b/src/HOL/Wellfounded.thy	Mon Dec 19 16:20:57 2022 +0100
@@ -875,9 +875,20 @@
   "asym r\<^sub>A \<Longrightarrow> asym r\<^sub>B \<Longrightarrow> asym (r\<^sub>A <*lex*> r\<^sub>B)"
   by (rule asym_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 trans_on_lex_prod[simp]:
+  assumes "trans_on A r\<^sub>A" and "trans_on B r\<^sub>B"
+  shows "trans_on (A \<times> B) (r\<^sub>A <*lex*> r\<^sub>B)"
+proof (rule trans_onI)
+  fix x y z
+  show "x \<in> A \<times> B \<Longrightarrow> y \<in> A \<times> B \<Longrightarrow> z \<in> A \<times> B \<Longrightarrow>
+       (x, y) \<in> r\<^sub>A <*lex*> r\<^sub>B \<Longrightarrow> (y, z) \<in> r\<^sub>A <*lex*> r\<^sub>B \<Longrightarrow> (x, z) \<in> r\<^sub>A <*lex*> r\<^sub>B"
+  using trans_onD[OF \<open>trans_on A r\<^sub>A\<close>, of "fst x" "fst y" "fst z"]
+  using trans_onD[OF \<open>trans_on B r\<^sub>B\<close>, of "snd x" "snd y" "snd z"]
+  by auto
+qed
+
+lemma trans_lex_prod [simp,intro!]: "trans r\<^sub>A \<Longrightarrow> trans r\<^sub>B \<Longrightarrow> trans (r\<^sub>A <*lex*> r\<^sub>B)"
+  by (rule trans_on_lex_prod[of UNIV _ UNIV, unfolded UNIV_Times_UNIV])
 
 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)"