equal
deleted
inserted
replaced
2507 by(induct xs)(simp_all add:distinct_insort set_sort) |
2507 by(induct xs)(simp_all add:distinct_insort set_sort) |
2508 |
2508 |
2509 lemma sorted_insort: "sorted (insort x xs) = sorted xs" |
2509 lemma sorted_insort: "sorted (insort x xs) = sorted xs" |
2510 apply (induct xs) |
2510 apply (induct xs) |
2511 apply(auto simp:sorted_Cons set_insort not_le less_imp_le) |
2511 apply(auto simp:sorted_Cons set_insort not_le less_imp_le) |
2512 apply(blast intro:order_trans) |
|
2513 done |
2512 done |
2514 |
2513 |
2515 theorem sorted_sort[simp]: "sorted (sort xs)" |
2514 theorem sorted_sort[simp]: "sorted (sort xs)" |
2516 by (induct xs) (auto simp:sorted_insort) |
2515 by (induct xs) (auto simp:sorted_insort) |
2517 |
2516 |