theory EQSort imports Universe
begin


(* SPLITTING FUNCTION *)

primrec qsplit :: "'a :: universe \<Rightarrow> 'a list \<Rightarrow> 'a list * 'a list" where
  "qsplit p []       = ([], [])"
| "qsplit p (x # xr) = (let (below, above) = qsplit p xr in 
     if ge x p then (below, x # above) else (x # below, above))"

lemma qsplit_length_below [rule_format]:
  "\<forall>bl ab. (bl, ab) = qsplit p l \<longrightarrow> length bl \<le> length l"

apply (induct l, auto)
apply (case_tac "qsplit p l", auto)
apply (case_tac "lt a p", auto)
done

lemma qsplit_length_above [rule_format]:
  "\<forall>bl ab. (bl, ab) = qsplit p l \<longrightarrow> length ab \<le> length l"

apply (induct l, auto)
apply (case_tac "qsplit p l", auto)
apply (case_tac "lt a p", auto)
done


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

function qsort :: "'a :: universe list \<Rightarrow> 'a list" where 
  "qsort [] = []"
| "qsort (p # rest) = (let (below, above) = qsplit p rest in 
     qsort below @ [p] @ qsort above)"

by pat_completeness auto

termination by (relation "measure length", auto dest: qsplit_length_above qsplit_length_below)


(* 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_below [rule_format, simp]:
  "\<forall>bl ab. qsplit p l = (bl, ab) \<longrightarrow> qall lt p bl"

apply (induct l, auto)
apply (case_tac "qsplit p l", auto)
apply (case_tac "lt a p", auto)
done

theorem qsplit_splits_above [rule_format, simp]:
  "\<forall>bl ab. qsplit p l = (bl, ab) \<longrightarrow> qall ge p ab"

apply (induct l, auto)
apply (case_tac "qsplit p l", auto)
apply (case_tac "lt a p", auto)
done

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_below [rule_format, simp]:
  "\<forall>bl ab. (bl, ab) = qsplit q l \<longrightarrow> qall f p l \<longrightarrow> qall f p bl"

apply (induct l, auto)
apply (case_tac "qsplit q l", auto)
apply (case_tac "lt a q", auto)
done

theorem qall_qsplit_above [rule_format, simp]:
  "\<forall>bl ab. (bl, ab) = qsplit q l \<longrightarrow> qall f p l \<longrightarrow> qall f p ab"

apply (induct l, auto)
apply (case_tac "qsplit q l", auto)
apply (case_tac "lt a q", auto)
done

theorem qall_qsort [rule_format, intro!]:
  "qall f p l \<longrightarrow> qall f p (qsort l)"

apply (induct l rule: qsort.induct, auto)
apply (case_tac "qsplit pa rest")
apply force+
done


(* 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 [intro!]:
  "\<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 [rule_format, iff]:
  "\<forall>bl ab. (bl, ab) = qsplit p l \<longrightarrow> count bl x + count ab x = count l x"
apply (induct l, auto)
apply (case_tac "qsplit p l", auto)
apply (case_tac "lt x p", auto)
apply (case_tac "qsplit p l", auto)
apply (case_tac "lt a p", auto)
done


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

theorem qsort_sorts:
  "qsorted (qsort l)"

apply (induct l rule: qsort.induct, auto)
apply (case_tac "qsplit p rest", auto)
apply force
done

theorem qsort_preserves:
  "count (qsort l) = count l"
apply (induct l rule: qsort.induct, auto, rule ext, auto)
apply (case_tac "qsplit p rest", auto)
apply (metis count_concat count_qsplit_lt_ge)
apply (case_tac "qsplit p rest", auto)
apply (metis count_concat count_qsplit_lt_ge)
done

end