diff -r c09c11386ca5 -r 42c4b87e98c2 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Apr 21 20:36:20 2017 +0200
+++ b/src/HOL/Library/Multiset.thy	Fri Apr 21 21:06:02 2017 +0200
@@ -1449,7 +1449,7 @@
   assumes empty: "P {#}"
   assumes add: "\<And>x M. P M \<Longrightarrow> P (add_mset x M)"
   shows "P M"
-proof (induct n \<equiv> "size M" arbitrary: M)
+proof (induct "size M" arbitrary: M)
   case 0 thus "P M" by (simp add: empty)
 next
   case (Suc k)
@@ -1459,6 +1459,48 @@
   with Suc add show "P M" by simp
 qed
 
+lemma multiset_induct_min[case_names empty add]:
+  fixes M :: "'a::linorder multiset"
+  assumes
+    empty: "P {#}" and
+    add: "\<And>x M. P M \<Longrightarrow> (\<forall>y \<in># M. y \<ge> x) \<Longrightarrow> P (add_mset x M)"
+  shows "P M"
+proof (induct "size M" arbitrary: M)
+  case (Suc k)
+  note ih = this(1) and Sk_eq_sz_M = this(2)
+
+  let ?y = "Min (set_mset M)"
+  let ?N = "M - {#?y#}"
+
+  have M: "M = add_mset ?y ?N"
+    by (metis Min_in Sk_eq_sz_M finite_set_mset insert_DiffM lessI not_less_zero
+      set_mset_eq_empty_iff size_empty)
+  show ?case
+    by (subst M, rule add, rule ih, metis M Sk_eq_sz_M nat.inject size_add_mset,
+      meson Min_le finite_set_mset in_diffD)
+qed (simp add: empty)
+
+lemma multiset_induct_max[case_names empty add]:
+  fixes M :: "'a::linorder multiset"
+  assumes
+    empty: "P {#}" and
+    add: "\<And>x M. P M \<Longrightarrow> (\<forall>y \<in># M. y \<le> x) \<Longrightarrow> P (add_mset x M)"
+  shows "P M"
+proof (induct "size M" arbitrary: M)
+  case (Suc k)
+  note ih = this(1) and Sk_eq_sz_M = this(2)
+
+  let ?y = "Max (set_mset M)"
+  let ?N = "M - {#?y#}"
+
+  have M: "M = add_mset ?y ?N"
+    by (metis Max_in Sk_eq_sz_M finite_set_mset insert_DiffM lessI not_less_zero
+      set_mset_eq_empty_iff size_empty)
+  show ?case
+    by (subst M, rule add, rule ih, metis M Sk_eq_sz_M nat.inject size_add_mset,
+      meson Max_ge finite_set_mset in_diffD)
+qed (simp add: empty)
+
 lemma multi_nonempty_split: "M \<noteq> {#} \<Longrightarrow> \<exists>A a. M = add_mset a A"
 by (induct M) auto