Theory Quicksort

(*
    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 = ⇗σ⇖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 = ⇗σ⇖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 ⇗σ⇖cont sortedPs) ∧
        mset Ps = mset sortedPs) ∧
        (∀x. x∉set Ps ⟶ ´next x = ⇗σ⇖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 ⇗σ⇖cont sortedPs) ∧
                 mset Ps = mset sortedPs) ∧
                 (∀x. x∉set Ps ⟶ ´next x = ⇗σ⇖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=⇗σ⇖p ∧
               ´cont=⇗σ⇖cont ∧
               List ⇗σ⇖p ⇗σ⇖next Ps ∧
               (∀x. x∉set Ps ⟶ ´next x = ⇗σ⇖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