diff -r 78a82c37b4b2 -r 484559628038 src/HOL/Imperative_HOL/ex/Sublist.thy --- a/src/HOL/Imperative_HOL/ex/Sublist.thy Thu Jun 18 16:17:51 2015 +0200 +++ b/src/HOL/Imperative_HOL/ex/Sublist.thy Fri Jun 19 15:55:22 2015 +0200 @@ -471,26 +471,26 @@ unfolding set_sublist' by blast -lemma multiset_of_sublist: +lemma mset_sublist: assumes l_r: "l \ r \ r \ List.length xs" assumes left: "\ i. i < l \ (xs::'a list) ! i = ys ! i" assumes right: "\ i. i \ r \ (xs::'a list) ! i = ys ! i" -assumes multiset: "multiset_of xs = multiset_of ys" - shows "multiset_of (sublist' l r xs) = multiset_of (sublist' l r ys)" +assumes multiset: "mset xs = mset ys" + shows "mset (sublist' l r xs) = mset (sublist' l r ys)" proof - from l_r have xs_def: "xs = (sublist' 0 l xs) @ (sublist' l r xs) @ (sublist' r (List.length xs) xs)" (is "_ = ?xs_long") by (simp add: sublist'_append) - from multiset have length_eq: "List.length xs = List.length ys" by (rule multiset_of_eq_length) + from multiset have length_eq: "List.length xs = List.length ys" by (rule mset_eq_length) with l_r have ys_def: "ys = (sublist' 0 l ys) @ (sublist' l r ys) @ (sublist' r (List.length ys) ys)" (is "_ = ?ys_long") by (simp add: sublist'_append) - from xs_def ys_def multiset have "multiset_of ?xs_long = multiset_of ?ys_long" by simp + from xs_def ys_def multiset have "mset ?xs_long = mset ?ys_long" by simp moreover from left l_r length_eq have "sublist' 0 l xs = sublist' 0 l ys" by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI) moreover from right l_r length_eq have "sublist' r (List.length xs) xs = sublist' r (List.length ys) ys" by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI) - ultimately show ?thesis by (simp add: multiset_of_append) + ultimately show ?thesis by (simp add: mset_append) qed