author haftmann Sat, 30 Aug 2014 11:15:47 +0200 changeset 58098 ff478d85129b parent 58097 cfd3cff9387b child 58099 7f232ae7de7c
inlined unused definition
```--- a/src/HOL/Library/Multiset.thy	Fri Aug 29 11:24:31 2014 +0200
+++ b/src/HOL/Library/Multiset.thy	Sat Aug 30 11:15:47 2014 +0200
@@ -262,6 +262,18 @@
"x \<in># M \<Longrightarrow> \<exists>A. M = A + {#x#}"
by (rule_tac x = "M - {#x#}" in exI, simp)

+  assumes "c \<in># B" and "b \<noteq> c"
+  shows "B - {#c#} + {#b#} = B + {#b#} - {#c#}"
+proof -
+  from `c \<in># B` obtain A where B: "B = A + {#c#}"
+    by (blast dest: multi_member_split)
+  have "A + {#b#} = A + {#b#} + {#c#} - {#c#}" by simp
+  then have "A + {#b#} = A + {#c#} + {#b#} - {#c#}"
+  then show ?thesis using B by simp
+qed
+

subsubsection {* Pointwise ordering induced by count *}

@@ -712,39 +724,18 @@

subsubsection {* Strong induction and subset induction for multisets *}

-text {* Well-foundedness of proper subset operator: *}
-
-text {* proper multiset subset *}
-
-definition
-  mset_less_rel :: "('a multiset * 'a multiset) set" where
-  "mset_less_rel = {(A,B). A < B}"
-
-  assumes "c \<in># B" and "b \<noteq> c"
-  shows "B - {#c#} + {#b#} = B + {#b#} - {#c#}"
-proof -
-  from `c \<in># B` obtain A where B: "B = A + {#c#}"
-    by (blast dest: multi_member_split)
-  have "A + {#b#} = A + {#b#} + {#c#} - {#c#}" by simp
-  then have "A + {#b#} = A + {#c#} + {#b#} - {#c#}"
-  then show ?thesis using B by simp
-qed
-
-lemma wf_mset_less_rel: "wf mset_less_rel"
-apply (unfold mset_less_rel_def)
+text {* Well-foundedness of strict subset relation *}
+
+lemma wf_less_mset_rel: "wf {(M, N :: 'a multiset). M < N}"
apply (rule wf_measure [THEN wf_subset, where f1=size])
apply (clarsimp simp: measure_def inv_image_def mset_less_size)
done

-text {* The induction rules: *}
-
lemma full_multiset_induct [case_names less]:
assumes ih: "\<And>B. \<forall>(A::'a multiset). A < B \<longrightarrow> P A \<Longrightarrow> P B"
shows "P B"
-apply (rule wf_mset_less_rel [THEN wf_induct])
-apply (rule ih, auto simp: mset_less_rel_def)
+apply (rule wf_less_mset_rel [THEN wf_induct])
+apply (rule ih, auto)
done

lemma multi_subset_induct [consumes 2, case_names empty add]:```