# HG changeset patch
# User desharna
# Date 1638003959 -3600
# Node ID 3e55e47a37e7f569bc710ea4baa1857a5a84c466
# Parent  250ab13343095694af1d04dcfe6fac9f54d97666
added lemma wfP_multp

diff -r 250ab1334309 -r 3e55e47a37e7 src/HOL/Library/Multiset.thy
--- 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"
   by (simp add: mult1_def)
 
+
+subsubsection \<open>Well-foundedness\<close>
+
 lemma less_add:
   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
+  by (simp add: wf_mult)
 
 
 subsubsection \<open>Closure-free presentation\<close>