verified insertino sort by Isabelle

gistfile1.txt

theory Scratch
imports Main
begin

primrec ins :: "int => int list => int list" where
  "ins x [] = [x]" |
  "ins x (y # ys) = (if x <= y then (x # y # ys) else (y # ins x ys))"

primrec sort :: "int list => int list" where
  "sort [] = []" |
  "sort (x # xs) = ins x (sort xs)"

primrec is_minimum :: "int => int list => bool" where
  "is_minimum _ [] = True" |
  "is_minimum v (x # xs) = (True & is_minimum v xs)"

primrec is_sorted :: "int list => bool" where
  "is_sorted [] = True" |
  "is_sorted (x # xs) = (is_minimum x xs & is_sorted xs)"

primrec is_elem :: "int => int list => bool" where
  "is_elem x [] = False" |
  "is_elem x (y # ys) = ((x = y) | is_elem x ys)"

primrec remove :: "int => int list => int list" where
  "remove x [] = []" |
  "remove x (y # ys) = (if x = y then ys else (y # remove x ys))"

primrec is_permutation :: "int list => int list => bool" where
  "is_permutation [] ys = (length ys = 0)" |
  "is_permutation (x # xs) ys = (is_elem x ys & is_permutation xs (remove x ys))"

lemma [simp]: "is_minimum a xs ⟹ x ≤ a ⟹ is_minimum x xs"
  by (induction xs, auto)

lemma [simp]: "is_minimum a xs ⟹ ¬ x ≤ a ⟹ is_minimum a (ins x xs)"
  by (induction xs, auto)

lemma [simp]: "is_sorted xs ⟹ is_sorted (ins x xs)"
  by (induction xs, auto)

lemma order_is_correct [simp]: "is_sorted (sort xs)"
  by (induction xs, auto)

lemma [simp]: "is_elem x (ins x xs)"
  by (induction xs, auto)

lemma rem_ins [simp]: "xs = (remove a (ins a xs))"
  by (induction xs, auto)

lemma is_permutation_correct [simp]: "is_permutation xs (sort xs)"
  by (induction xs, auto, metis rem_ins)

end