equal
deleted
inserted
replaced
5188 "sorted [x\<leftarrow>xs. x = g xs]" |
5188 "sorted [x\<leftarrow>xs. x = g xs]" |
5189 using sorted_map_same [of "\<lambda>x. x"] by simp |
5189 using sorted_map_same [of "\<lambda>x. x"] by simp |
5190 |
5190 |
5191 end |
5191 end |
5192 |
5192 |
|
5193 lemma sorted_upt[simp]: "sorted [m..<n]" |
|
5194 by(simp add: sorted_sorted_wrt sorted_wrt_mono_rel[OF _ sorted_wrt_upt]) |
|
5195 |
|
5196 lemma sorted_upto[simp]: "sorted [m..n]" |
|
5197 by(simp add: sorted_sorted_wrt sorted_wrt_mono_rel[OF _ sorted_wrt_upto]) |
|
5198 |
5193 |
5199 |
5194 subsubsection \<open>Sorting functions\<close> |
5200 subsubsection \<open>Sorting functions\<close> |
5195 |
5201 |
5196 text\<open>Currently it is not shown that @{const sort} returns a |
5202 text\<open>Currently it is not shown that @{const sort} returns a |
5197 permutation of its input because the nicest proof is via multisets, |
5203 permutation of its input because the nicest proof is via multisets, |