Shodan Pasting Service

Paste "Insertion sort" by Anonymous

Time of creation: 2015-07-21 06:50:36.516097 UTC

fun insert_sorted :: "('a::linorder) ⇒ 'a list ⇒ 'a list" where
  "insert_sorted x [] = [x]"
| "insert_sorted x (y#ys) = (if x ≤ y then x # y # ys else y # insert_sorted x ys)"

(* List has all the elements it should have, including multiplicities *)
lemma multiset_insert_sorted: "multiset_of (insert_sorted x ys) = multiset_of ys + {#x#}"
  by (induction ys) (auto simp: add_ac)

(* Same thing but without multiplicities *)
lemma set_insert_sorted [simp]: "set (insert_sorted x ys) = set ys ∪ {x}"
  by (induction ys) auto

(* Insertion preserves sortedness *)
lemma "sorted ys ⟹ sorted (insert_sorted x ys)"
  by (induction ys) (auto simp: sorted_Cons)

export_code insert_sorted in Haskell