# HG changeset patch
# User desharna
# Date 1671445537 -3600
# Node ID e321569ec7a137d8f12f91fc951b4bf8fb1f64b3
# Parent  2f8219460ac9f526434877fa0c4450e4ad327442
added lemmas sym_on_lex_prod[simp] and sym_lex_prod[simp]

diff -r 2f8219460ac9 -r e321569ec7a1 NEWS
--- a/NEWS	Mon Dec 19 11:23:28 2022 +0100
+++ b/NEWS	Mon Dec 19 11:25:37 2022 +0100
@@ -120,6 +120,8 @@
   - Added lemmas.
       irrefl_lex_prod[simp]
       irrefl_on_lex_prod[simp]
+      sym_lex_prod[simp]
+      sym_on_lex_prod[simp]
       wfP_if_convertible_to_nat
       wfP_if_convertible_to_wfP
       wf_if_convertible_to_wf
diff -r 2f8219460ac9 -r e321569ec7a1 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Mon Dec 19 11:23:28 2022 +0100
+++ b/src/HOL/Wellfounded.thy	Mon Dec 19 11:25:37 2022 +0100
@@ -856,6 +856,14 @@
 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])
 
+lemma sym_on_lex_prod[simp]:
+  "sym_on A r\<^sub>A \<Longrightarrow> sym_on B r\<^sub>B \<Longrightarrow> sym_on (A \<times> B) (r\<^sub>A <*lex*> r\<^sub>B)"
+  by (auto intro!: sym_onI dest: sym_onD)
+
+lemma sym_lex_prod[simp]:
+  "sym r\<^sub>A \<Longrightarrow> sym r\<^sub>B \<Longrightarrow> sym (r\<^sub>A <*lex*> r\<^sub>B)"
+  by (rule sym_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