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