summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Imperative_HOL/ex/Sublist.thy

changeset 60515 | 484559628038 |

parent 58889 | 5b7a9633cfa8 |

1.1 --- a/src/HOL/Imperative_HOL/ex/Sublist.thy Thu Jun 18 16:17:51 2015 +0200 1.2 +++ b/src/HOL/Imperative_HOL/ex/Sublist.thy Fri Jun 19 15:55:22 2015 +0200 1.3 @@ -471,26 +471,26 @@ 1.4 unfolding set_sublist' by blast 1.5 1.6 1.7 -lemma multiset_of_sublist: 1.8 +lemma mset_sublist: 1.9 assumes l_r: "l \<le> r \<and> r \<le> List.length xs" 1.10 assumes left: "\<forall> i. i < l \<longrightarrow> (xs::'a list) ! i = ys ! i" 1.11 assumes right: "\<forall> i. i \<ge> r \<longrightarrow> (xs::'a list) ! i = ys ! i" 1.12 -assumes multiset: "multiset_of xs = multiset_of ys" 1.13 - shows "multiset_of (sublist' l r xs) = multiset_of (sublist' l r ys)" 1.14 +assumes multiset: "mset xs = mset ys" 1.15 + shows "mset (sublist' l r xs) = mset (sublist' l r ys)" 1.16 proof - 1.17 from l_r have xs_def: "xs = (sublist' 0 l xs) @ (sublist' l r xs) @ (sublist' r (List.length xs) xs)" (is "_ = ?xs_long") 1.18 by (simp add: sublist'_append) 1.19 - from multiset have length_eq: "List.length xs = List.length ys" by (rule multiset_of_eq_length) 1.20 + from multiset have length_eq: "List.length xs = List.length ys" by (rule mset_eq_length) 1.21 with l_r have ys_def: "ys = (sublist' 0 l ys) @ (sublist' l r ys) @ (sublist' r (List.length ys) ys)" (is "_ = ?ys_long") 1.22 by (simp add: sublist'_append) 1.23 - from xs_def ys_def multiset have "multiset_of ?xs_long = multiset_of ?ys_long" by simp 1.24 + from xs_def ys_def multiset have "mset ?xs_long = mset ?ys_long" by simp 1.25 moreover 1.26 from left l_r length_eq have "sublist' 0 l xs = sublist' 0 l ys" 1.27 by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI) 1.28 moreover 1.29 from right l_r length_eq have "sublist' r (List.length xs) xs = sublist' r (List.length ys) ys" 1.30 by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI) 1.31 - ultimately show ?thesis by (simp add: multiset_of_append) 1.32 + ultimately show ?thesis by (simp add: mset_append) 1.33 qed 1.34 1.35