author blanchet Fri, 21 Apr 2017 21:06:02 +0200 changeset 65545 42c4b87e98c2 parent 65544 c09c11386ca5 child 65546 7c58f69451b0 child 65548 b7caa2b8bdbf
two new induction principles on multisets
```--- 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 {#}"
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

+  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)
+
+  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)