Quelle  Quicksort.thy

(*
    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