theory QSort imports Universe
begin


(* SPLITTING FUNCTION *)

primrec qsplit :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a :: universe \<Rightarrow> 'a list \<Rightarrow> 'a list" where
  "qsplit f p [] = []"
| "qsplit f p (h # t) = (if f h p then h # qsplit f p t else qsplit f p t)"

lemma qsplit_length [simp]:
  "length (qsplit f p l) \<le> length l"
  by (induct l, auto)


(* QUICKSORT, i.e. the MODEL *)

function qsort :: "'a :: universe list \<Rightarrow> 'a list" where
  "qsort [] = []"
| "qsort (p # l) = qsort (qsplit lt p l) @ p # qsort (qsplit ge p l)"
by pat_completeness auto

termination by (relation "measure length", auto, (metis le_imp_less_Suc qsplit_length)+)


(* ORDER LIFTING TO LISTS, i.e. part of SPECIFICATION *)

primrec qall :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> bool" where
  "qall f p [] = True"
| "qall f p (h # t) = (f h p \<and> qall f p t)"

theorem qsplit_splits [simp]:
  "qall f p (qsplit f p l)"
  by (induct l, auto)

lemma qall_concat [iff]:
  "qall f p (a @ b) = (qall f p a \<and> qall f p b)"
  by (induct a, auto)

theorem qall_qsplit [simp]:
  "qall f p l \<Longrightarrow> qall f p (qsplit g q l)"
  by (induct l, auto)

theorem qall_qsort [simp]:
  "qall f p l \<Longrightarrow> qall f p (qsort l)"
  by (induct l rule: qsort.induct, auto)


(* SORTEDNESS, i.e. SPECIFICATION *)

fun qsorted :: "'a :: universe list \<Rightarrow> bool" where
  "qsorted [] = True"
| "qsorted [x] = True"
| "qsorted (a # b # l) = (ge b a \<and> qsorted (b # l))"

lemma qsorted_append [simp]:
  "\<lbrakk> qsorted l; qall ge p l\<rbrakk> \<Longrightarrow> qsorted (p # l)"
  by (induct l, auto)

theorem qsorted_concat [simp]:
  "\<lbrakk> qsorted a; qsorted b; qall lt p a; qall ge p b \<rbrakk> \<Longrightarrow> qsorted (a @ p # b)"
  by (induct a, simp, clarsimp, case_tac a2, auto)


(* PERMUTATION, i.e. SPECIFICATION *)

primrec count :: "'a list \<Rightarrow> 'a \<Rightarrow> nat" where
  "count [] = (\<lambda>x. 0)"
| "count (h # t) = (count t) (h := count t h + 1)" 

lemma count_concat [simp]:
  "count (a @ b) x = count a x + count b x"
  by (induct a, auto)

theorem count_qsplit_lt_ge [iff]:
  "count (qsplit lt p l) x + count (qsplit ge p l) x = count l x"
  by (induct l, auto)


(* CORE THEOREMS, i.e. consistency of model and specification *)

theorem qsort_sorts:
  "qsorted (qsort l)"
  by (induct l rule: qsort.induct, auto)

theorem qsort_preserves:
  "count (qsort l) = count l"
  by (induct l rule: qsort.induct, auto, rule ext, auto)

end