(*
    Author:      Norbert Schirmer
    Maintainer:  Norbert Schirmer, norbert.schirmer at web de

Copyright (C) 2006-2008 Norbert Schirmer
*)

section "Example: Quicksort on Heap Lists"

theory Quicksort
imports "../Vcg" "../HeapList" "HOL-Library.Multiset"
begin

record globals_heap =
  next_' :: "ref → ref"
  cont_' :: "ref → nat"

record 'g vars = "'g state" +
  p_'    :: "ref"
  q_'    :: "ref"
  le_'   :: "ref"
  gt_'   :: "ref"
  hd_'   :: "ref"
  tl_'   :: "ref"

procedures
  append(p,q|p) =
    "IF 🚫p=Null THEN 🚫p :== 🚫q ELSE 🚫p→🚫next :== CALL append(🚫p→🚫next,🚫q) FI"

  append_spec:
   "∀σ Ps Qs.
     Γ⊨ {σ. List 🚫p 🚫next Ps ∧ List 🚫q 🚫next Qs ∧ set Ps ∩ set Qs = {}}
           🚫p :== PROC append(🚫p,🚫q)
         {List 🚫p 🚫next (Ps@Qs) ∧ (∀x. x∉set Ps ⟶ 🚫next x = ^<sigma>next x)}"

  append_modifies:
   "∀σ. Γ⊨ {σ} 🚫p :== PROC append(🚫p,🚫q){t. t may_only_modify_globals σ in [next]}"


lemma (in append_impl) append_modifies:
  shows
   "∀σ. Γ⊨ {σ} 🚫p :== PROC append(🚫p,🚫q){t. t may_only_modify_globals σ in [next]}"
  apply (hoare_rule HoarePartial.ProcRec1)
  apply (vcg spec=modifies)
  done


lemma (in append_impl) append_spec:
  shows "∀σ Ps Qs. Γ⊨
            {σ. List 🚫p 🚫next Ps ∧ List 🚫q 🚫next Qs ∧ set Ps ∩ set Qs = {}}
                🚫p :== PROC append(🚫p,🚫q)
            {List 🚫p 🚫next (Ps@Qs) ∧ (∀x. x∉set Ps ⟶ 🚫next x = ^<sigma>next x)}"
  apply (hoare_rule HoarePartial.ProcRec1)
  apply vcg
  apply fastforce
  done

primrec sorted:: "('a → 'a → bool) → 'a list → bool"
where
"sorted le [] = True" |
"sorted le (x#xs) = ((∀y∈set xs. le x y) ∧ sorted le xs)"

lemma sorted_append[simp]:
 "sorted le (xs@ys) = (sorted le xs ∧ sorted le ys ∧
                       (∀x ∈ set xs. ∀y ∈ set ys. le x y))"
by (induct xs, auto)

procedures quickSort(p|p) =
 "IF 🚫p=Null THEN SKIP
  ELSE 🚫tl :== 🚫p→🚫next;;
       🚫le :== Null;;
       🚫gt :== Null;;
       WHILE 🚫tl≠Null DO
         🚫hd :== 🚫tl;;
         🚫tl :== 🚫tl→🚫next;;
         IF 🚫hd→🚫cont ≤ 🚫p→🚫cont
         THEN 🚫hd→🚫next :== 🚫le;;
              🚫le :== 🚫hd
         ELSE 🚫hd→🚫next :== 🚫gt;;
              🚫gt :== 🚫hd
         FI
       OD;;
       🚫le :== CALL quickSort(🚫le);;
       🚫gt :== CALL quickSort(🚫gt);;
       🚫p→🚫next :== 🚫gt;;
       🚫le :== CALL append(🚫le,🚫p);;
       🚫p :== 🚫le
  FI"

  quickSort_spec:
  "∀σ Ps. Γ⊨ {σ. List 🚫p 🚫next Ps} 🚫p :== PROC quickSort(🚫p)
       {(∃sortedPs. List 🚫p 🚫next sortedPs ∧
        sorted (≤) (map ^<sigma>cont sortedPs) ∧
        mset Ps = mset sortedPs) ∧
        (∀x. x∉set Ps ⟶ 🚫next x = ^<sigma>next x)}"

  quickSort_modifies:
  "∀σ. Γ⊨ {σ} 🚫p :== PROC quickSort(🚫p) {t. t may_only_modify_globals σ in [next]}"


lemma (in quickSort_impl) quickSort_modifies:
  shows
  "∀σ. Γ⊨ {σ} 🚫p :== PROC quickSort(🚫p) {t. t may_only_modify_globals σ in [next]}"
apply (hoare_rule HoarePartial.ProcRec1)
apply (vcg spec=modifies)
done

lemma (in quickSort_impl) quickSort_spec:
shows
  "∀σ Ps. Γ⊨ {σ. List 🚫p 🚫next Ps}
                  🚫p :== PROC quickSort(🚫p)
                {(∃sortedPs. List 🚫p 🚫next sortedPs ∧
                 sorted (≤) (map ^<sigma>cont sortedPs) ∧
                 mset Ps = mset sortedPs) ∧
                 (∀x. x∉set Ps ⟶ 🚫next x = ^<sigma>next x)}"
apply (hoare_rule HoarePartial.ProcRec1)
apply (hoare_rule anno =
 "IF 🚫p=Null THEN SKIP
  ELSE 🚫tl :== 🚫p→🚫next;;
       🚫le :== Null;;
       🚫gt :== Null;;
       WHILE 🚫tl≠Null
       INV { (∃les grs tls. List 🚫le 🚫next les ∧ List 🚫gt 🚫next grs ∧
               List 🚫tl 🚫next tls ∧
               mset Ps = mset (🚫p#tls@les@grs) ∧
               distinct(🚫p#tls@les@grs) ∧
               (∀x∈set les. x→🚫cont ≤ 🚫p→🚫cont) ∧
               (∀x∈set grs. 🚫p→🚫cont < x→🚫cont)) ∧
               🚫p=^<sigma>p ∧
               🚫cont=^<sigma>cont ∧
               List ^<sigma>p ^<sigma>next Ps ∧
               (∀x. x∉set Ps ⟶ 🚫next x = ^<sigma>next x)}
       DO
         🚫hd :== 🚫tl;;
         🚫tl :== 🚫tl→🚫next;;
         IF 🚫hd→🚫cont ≤ 🚫p→🚫cont
         THEN 🚫hd→🚫next :== 🚫le;;
              🚫le :== 🚫hd
         ELSE 🚫hd→🚫next :== 🚫gt;;
              🚫gt :== 🚫hd
         FI
       OD;;
       🚫le :== CALL quickSort(🚫le);;
       🚫gt :== CALL quickSort(🚫gt);;
       🚫p→🚫next :== 🚫gt;;
       🚫le :== CALL append(🚫le,🚫p);;
       🚫p :== 🚫le
  FI" in HoarePartial.annotateI)
  apply vcg
    apply fastforce
   apply clarsimp
   apply (rule conjI)
    apply clarify
    apply (rule conjI)
     apply (rule_tac x="tl#les" in exI)
     apply simp
     apply (rule_tac x="grs" in exI)
     apply simp
     apply (rule_tac x="ps" in exI)
     apply simp
    apply (metis insertCI set_mset_add_mset_insert set_mset_mset)
   apply clarify
   apply (rule conjI)
    apply (rule_tac x="les" in exI)
    apply simp
    apply (rule_tac x="tl#grs" in exI)
    apply simp
    apply (rule_tac x="ps" in exI)
    apply simp
   apply (metis insertCI set_mset_add_mset_insert set_mset_mset)
  apply clarsimp
  apply (rule_tac ?x=grs in exI)
  apply (rule conjI)
  apply (erule heap_eq_ListI1)
   apply clarify
   apply (erule_tac x=x in allE) back
   apply blast
  apply clarsimp
  apply (rule_tac x="sortedPs" in exI)
  apply (rule conjI)
   apply (erule heap_eq_ListI1)
   apply (clarsimp)
   apply (erule_tac x=x in allE) back back
   apply (metis IntI empty_iff set_mset_mset)
  apply (rule_tac x="p#sortedPsa" in exI)
  apply (rule conjI)
   apply (metis List_cons List_updateI Null_notin_List fun_upd_same insert_iff set_mset_add_mset_insert set_mset_mset)
  apply (rule conjI)
   apply (metis disjoint_iff mset_eq_setD set_ConsD)
  apply clarsimp
  apply (rule conjI)
   apply (metis less_or_eq_imp_le mset_eq_setD)
  apply (rule conjI)
   apply (metis leD less_le_trans mset_eq_setD nat_le_linear)
  apply clarsimp
  apply (erule_tac x=x in allE)+
  apply (metis Un_iff insert_iff list.set(2) mset.simps(2) mset_append set_append set_mset_mset)
  done

end