author desharna Sat, 27 Nov 2021 10:05:59 +0100 changeset 74860 3e55e47a37e7 parent 74859 250ab1334309 child 74861 74ac414618e2
```--- a/src/HOL/Library/Multiset.thy	Sat Nov 27 10:01:40 2021 +0100
+++ b/src/HOL/Library/Multiset.thy	Sat Nov 27 10:05:59 2021 +0100
@@ -2789,8 +2789,6 @@

subsection \<open>The multiset order\<close>

-subsubsection \<open>Well-foundedness\<close>
-
definition mult1 :: "('a \<times> 'a) set \<Rightarrow> ('a multiset \<times> 'a multiset) set" where
"mult1 r = {(N, M). \<exists>a M0 K. M = add_mset a M0 \<and> N = M0 + K \<and>
(\<forall>b. b \<in># K \<longrightarrow> (b, a) \<in> r)}"
@@ -2834,6 +2832,9 @@
lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r"

+
+subsubsection \<open>Well-foundedness\<close>
+
assumes mult1: "(N, add_mset a M0) \<in> mult1 r"
shows
@@ -2934,11 +2935,15 @@
qed
qed

-theorem wf_mult1: "wf r \<Longrightarrow> wf (mult1 r)"
-by (rule acc_wfI) (rule all_accessible)
-
-theorem wf_mult: "wf r \<Longrightarrow> wf (mult r)"
-unfolding mult_def by (rule wf_trancl) (rule wf_mult1)
+lemma wf_mult1: "wf r \<Longrightarrow> wf (mult1 r)"
+  by (rule acc_wfI) (rule all_accessible)
+
+lemma wf_mult: "wf r \<Longrightarrow> wf (mult r)"
+  unfolding mult_def by (rule wf_trancl) (rule wf_mult1)
+
+lemma wfP_multp: "wfP r \<Longrightarrow> wfP (multp r)"
+  unfolding multp_def wfP_def