# Theory SelectionSort_Functional

(*  Title:      Sort.thy
Author:     Danijela Petrovi\'c, Facylty of Mathematics, University of Belgrade *)

section ‹Verification of functional Selection Sort›

theory SelectionSort_Functional
imports RemoveMax
begin

subsection ‹Defining data structure›

text‹Selection sort works with list and that is the reason why {\em
Collection} should be interpreted as list.›

interpretation Collection "[]" "λ l. l = []" id mset
by (unfold_locales, auto)

subsection ‹Defining function remove\_max›

text‹The following is definition of {\em remove\_max} function.
The idea is very well known -- assume that the maximum element is the
first one and then compare with each element of the list. Function
{\em f} is one step in iteration, it compares current maximum {\em m}
with one element {\em x}, if it is bigger then {\em m} stays current
maximum and {\em x} is added in the resulting list, otherwise {\em x}
is current maximum and {\em m} is added in the resulting
list.
›

fun f where "f (m, l) x = (if x ≥ m then (x, m#l) else (m, x#l))"

definition remove_max where
"remove_max l = foldl f (hd l, []) (tl l)"

lemma max_Max_commute:
"finite A ⟹ max (Max (insert m A)) x = max m (Max (insert x A))"
apply (cases "A = {}", simp)
by (metis Max_insert max.commute max.left_commute)

text‹The function really returned the
maximum value.›

lemma remove_max_max_lemma:
shows "fst (foldl f (m, t) l) =  Max (set (m # l))"
proof (induct l arbitrary: m t rule: rev_induct)
case (snoc x xs)
let ?a = "foldl f (m, t) xs"
let ?m' = "fst ?a" and ?t' = "snd ?a"
have "fst (foldl f (m, t) (xs @ [x])) = max ?m' x"
by (cases ?a) (auto simp add: max_def)
thus ?case
using snoc
by (simp add: max_Max_commute)
qed simp

lemma remove_max_max:
assumes "l ≠ []" "(m, l') = remove_max l"
shows "m = Max (set l)"
using assms
unfolding remove_max_def
using remove_max_max_lemma[of "hd l" "[]" "tl l"]
using fst_conv[of m l']
by simp

text‹Nothing new is added in the list and noting is deleted
from the list except the maximum element.›

lemma remove_max_mset_lemma:
assumes "(m, l') = foldl f (m', t') l"
shows "mset (m # l') = mset (m' # t' @ l)"
using assms
proof (induct l arbitrary: l' m m' t' rule: rev_induct)
case (snoc x xs)
let ?a = "foldl f (m', t') xs"
let ?m' = "fst ?a" and ?t' = "snd ?a"
have "mset (?m' # ?t') = mset (m' # t' @ xs)"
using snoc(1)[of ?m' ?t' m' t']
by simp
thus ?case
using snoc(2)
apply (cases "?a")
by (auto split: if_split_asm)
qed simp

lemma remove_max_mset:
assumes "l ≠ []" "(m, l') = remove_max l"
shows "add_mset m (mset l') = mset l"
using assms
unfolding remove_max_def
using remove_max_mset_lemma[of m l' "hd l" "[]" "tl l"]
by auto

definition ssf_ssort' where
[simp, code del]: "ssf_ssort' = RemoveMax.ssort' (λ l. l = []) remove_max"
definition ssf_ssort where
[simp, code del]: "ssf_ssort = RemoveMax.ssort (λ l. l = []) id remove_max"

interpretation SSRemoveMax:
RemoveMax "[]" "λ l. l = []" id mset remove_max "λ _. True"
rewrites
"RemoveMax.ssort' (λ l. l = []) remove_max = ssf_ssort'" and
"RemoveMax.ssort (λ l. l = []) id remove_max = ssf_ssort"
using remove_max_max
by (unfold_locales, auto simp add: remove_max_mset)

end