126 |
126 |
127 lemma mset_msort: "mset (msort xs) = mset xs" |
127 lemma mset_msort: "mset (msort xs) = mset xs" |
128 proof(induction xs rule: msort.induct) |
128 proof(induction xs rule: msort.induct) |
129 case (1 xs) |
129 case (1 xs) |
130 let ?n = "length xs" |
130 let ?n = "length xs" |
131 let ?xs1 = "take (?n div 2) xs" |
131 let ?ys = "take (?n div 2) xs" |
132 let ?xs2 = "drop (?n div 2) xs" |
132 let ?zs = "drop (?n div 2) xs" |
133 show ?case |
133 show ?case |
134 proof cases |
134 proof cases |
135 assume "?n \<le> 1" |
135 assume "?n \<le> 1" |
136 thus ?thesis by(simp add: msort.simps[of xs]) |
136 thus ?thesis by(simp add: msort.simps[of xs]) |
137 next |
137 next |
138 assume "\<not> ?n \<le> 1" |
138 assume "\<not> ?n \<le> 1" |
139 hence "mset (msort xs) = mset (msort ?xs1) + mset (msort ?xs2)" |
139 hence "mset (msort xs) = mset (msort ?ys) + mset (msort ?zs)" |
140 by(simp add: msort.simps[of xs] mset_merge) |
140 by(simp add: msort.simps[of xs] mset_merge) |
141 also have "\<dots> = mset ?xs1 + mset ?xs2" |
141 also have "\<dots> = mset ?ys + mset ?zs" |
142 using \<open>\<not> ?n \<le> 1\<close> by(simp add: "1.IH") |
142 using \<open>\<not> ?n \<le> 1\<close> by(simp add: "1.IH") |
143 also have "\<dots> = mset (?xs1 @ ?xs2)" by (simp del: append_take_drop_id) |
143 also have "\<dots> = mset (?ys @ ?zs)" by (simp del: append_take_drop_id) |
144 also have "\<dots> = mset xs" by simp |
144 also have "\<dots> = mset xs" by simp |
145 finally show ?thesis . |
145 finally show ?thesis . |
146 qed |
146 qed |
147 qed |
147 qed |
148 |
148 |
149 text \<open>Via the previous lemma or directtly:\<close> |
149 text \<open>Via the previous lemma or directly:\<close> |
150 |
150 |
151 lemma set_merge: "set(merge xs ys) = set xs \<union> set ys" |
151 lemma set_merge: "set(merge xs ys) = set xs \<union> set ys" |
152 by (metis mset_merge set_mset_mset set_mset_union) |
152 by (metis mset_merge set_mset_mset set_mset_union) |
153 |
153 |
154 lemma "set(merge xs ys) = set xs \<union> set ys" |
154 lemma "set(merge xs ys) = set xs \<union> set ys" |
155 by(induction xs ys rule: merge.induct) (auto) |
155 by(induction xs ys rule: merge.induct) (auto) |
156 |
156 |
157 lemma sorted_merge: "sorted (merge xs ys) \<longleftrightarrow> (sorted xs \<and> sorted ys)" |
157 lemma sorted_merge: "sorted (merge xs ys) \<longleftrightarrow> (sorted xs \<and> sorted ys)" |
158 by(induction xs ys rule: merge.induct) (auto simp: set_merge) |
158 by(induction xs ys rule: merge.induct) (auto simp: set_merge) |
159 |
159 |
160 lemma "sorted (msort xs)" |
160 lemma sorted_msort: "sorted (msort xs)" |
161 proof(induction xs rule: msort.induct) |
161 proof(induction xs rule: msort.induct) |
162 case (1 xs) |
162 case (1 xs) |
163 let ?n = "length xs" |
163 let ?n = "length xs" |
164 show ?case |
164 show ?case |
165 proof cases |
165 proof cases |
166 assume "?n \<le> 1" |
166 assume "?n \<le> 1" |
167 thus ?thesis by(simp add: msort.simps[of xs] sorted01) |
167 thus ?thesis by(simp add: msort.simps[of xs] sorted01) |
168 next |
168 next |
169 assume "\<not> ?n \<le> 1" |
169 assume "\<not> ?n \<le> 1" |
170 thus ?thesis using "1.IH" |
170 thus ?thesis using "1.IH" |
171 by(simp add: sorted_merge msort.simps[of xs] mset_merge) |
171 by(simp add: sorted_merge msort.simps[of xs]) |
172 qed |
172 qed |
173 qed |
173 qed |
174 |
174 |
175 |
175 |
176 subsubsection "Time Complexity" |
176 subsubsection "Time Complexity" |