# HG changeset patch
# User desharna
# Date 1638123168 -3600
# Node ID 2741ef11ccf6be06af888795d9f737b0991b2ca8
# Parent  4220dcd6c22eefff7a174b673914782504b6d378
added wfP_less to wellorder and wfP_less_multiset

diff -r 4220dcd6c22e -r 2741ef11ccf6 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sun Nov 28 09:57:48 2021 +0100
+++ b/src/HOL/Library/Multiset.thy	Sun Nov 28 19:12:48 2021 +0100
@@ -3193,6 +3193,12 @@
   shows "M < M \<Longrightarrow> R"
   by simp
 
+lemma wfP_less_multiset[simp]:
+  assumes wfP_less: "wfP ((<) :: ('a :: preorder) \<Rightarrow> 'a \<Rightarrow> bool)"
+  shows "wfP ((<) :: 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool)"
+  using wfP_multp[OF wfP_less] less_multiset_def
+  by (metis wfPUNIVI wfP_induct)
+
 
 subsection \<open>Quasi-executable version of the multiset extension\<close>
 
diff -r 4220dcd6c22e -r 2741ef11ccf6 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Sun Nov 28 09:57:48 2021 +0100
+++ b/src/HOL/Wellfounded.thy	Sun Nov 28 19:12:48 2021 +0100
@@ -79,6 +79,9 @@
 lemma (in wellorder) wf: "wf {(x, y). x < y}"
   unfolding wf_def by (blast intro: less_induct)
 
+lemma (in wellorder) wfP_less[simp]: "wfP (<)"
+  by (simp add: wf wfP_def)
+
 
 subsection \<open>Basic Results\<close>