# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1597768731 -3600
# Node ID 721a05da8fe7d770bd51b84f3404b4f7ca1db551
# Parent  e5765cfd4338b8caa8f1d72a4726ad30da2faccb
lexicographic ordering: new simp setup to prioritise the simpler "less_than" case

diff -r e5765cfd4338 -r 721a05da8fe7 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Tue Aug 18 14:45:09 2020 +0100
+++ b/src/HOL/Wellfounded.thy	Tue Aug 18 17:38:51 2020 +0100
@@ -768,7 +768,11 @@
     (infixr "<*lex*>" 80)
     where "ra <*lex*> rb = {((a, b), (a', b')). a \<noteq> a' \<and> (a, a') \<in> ra \<or> a = a' \<and> (b, b') \<in> rb}"
 
-lemma in_lex_prod[simp]: "((a, b), (a', b')) \<in> r <*lex*> s \<longleftrightarrow> a \<noteq> a' \<and> (a, a') \<in> r \<or> a = a' \<and> (b, b') \<in> s"
+lemma in_lex_prod[simp]: "NO_MATCH less_than r \<Longrightarrow> ((a, b), (a', b')) \<in> r <*lex*> s \<longleftrightarrow> a \<noteq> a' \<and> (a, a') \<in> r \<or> a = a' \<and> (b, b') \<in> s"
+  by (auto simp:lex_prod_def)
+
+text\<open>compared with @{thm[source]in_lex_prod} this yields simpler results\<close>
+lemma in_lex_prod_less_than[simp]: "((a, b), (a', b')) \<in> less_than <*lex*> s \<longleftrightarrow>a<a' \<or> a = a' \<and> (b, b') \<in> s"
   by (auto simp:lex_prod_def)
 
 lemma wf_lex_prod [intro!]: