# HG changeset patch # User desharna # Date 1665844459 -7200 # Node ID 5836811fe5490d27d28529d7056403ce29644bc9 # Parent 0ad6f6508274290a0aa068f65ccb62214259fd32 added lemma wfP_subset_mset[simp] diff -r 0ad6f6508274 -r 5836811fe549 NEWS --- a/NEWS Fri Oct 14 15:48:31 2022 +0100 +++ b/NEWS Sat Oct 15 16:34:19 2022 +0200 @@ -46,6 +46,9 @@ fimage_strict_mono wfP_pfsubset +* Theory "HOL-Library.Multiset": + - Added lemma wfP_subset_mset[simp]. + New in Isabelle2022 (October 2022) ---------------------------------- diff -r 0ad6f6508274 -r 5836811fe549 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Fri Oct 14 15:48:31 2022 +0100 +++ b/src/HOL/Library/Multiset.thy Sat Oct 15 16:34:19 2022 +0200 @@ -1575,6 +1575,9 @@ apply (clarsimp simp: measure_def inv_image_def mset_subset_size) done +lemma wfP_subset_mset[simp]: "wfP (\#)" + by (rule wf_subset_mset_rel[to_pred]) + lemma full_multiset_induct [case_names less]: assumes ih: "\B. \(A::'a multiset). A \# B \ P A \ P B" shows "P B"