src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
changeset 37792 ba0bc31b90d7
parent 37771 1bec64044b5e
child 37797 96551d6b1414
     1.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Tue Jul 13 11:50:22 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Tue Jul 13 12:00:11 2010 +0200
     1.3 @@ -12,14 +12,14 @@
     1.4  
     1.5  definition swap :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap"
     1.6  where
     1.7 -  "swap arr i j = (
     1.8 -     do
     1.9 +  "swap arr i j =
    1.10 +     do {
    1.11         x \<leftarrow> nth arr i;
    1.12         y \<leftarrow> nth arr j;
    1.13         upd i y arr;
    1.14         upd j x arr;
    1.15         return ()
    1.16 -     done)"
    1.17 +     }"
    1.18  
    1.19  lemma crel_swapI [crel_intros]:
    1.20    assumes "i < Array.length a h" "j < Array.length a h"
    1.21 @@ -40,12 +40,12 @@
    1.22  where
    1.23    "part1 a left right p = (
    1.24       if (right \<le> left) then return right
    1.25 -     else (do
    1.26 +     else do {
    1.27         v \<leftarrow> nth a left;
    1.28         (if (v \<le> p) then (part1 a (left + 1) right p)
    1.29 -                    else (do swap a left right;
    1.30 -  part1 a left (right - 1) p done))
    1.31 -     done))"
    1.32 +                    else (do { swap a left right;
    1.33 +  part1 a left (right - 1) p }))
    1.34 +     })"
    1.35  by pat_completeness auto
    1.36  
    1.37  termination
    1.38 @@ -227,14 +227,14 @@
    1.39  
    1.40  fun partition :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
    1.41  where
    1.42 -  "partition a left right = (do
    1.43 +  "partition a left right = do {
    1.44       pivot \<leftarrow> nth a right;
    1.45       middle \<leftarrow> part1 a left (right - 1) pivot;
    1.46       v \<leftarrow> nth a middle;
    1.47       m \<leftarrow> return (if (v \<le> pivot) then (middle + 1) else middle);
    1.48       swap a m right;
    1.49       return m
    1.50 -   done)"
    1.51 +   }"
    1.52  
    1.53  declare partition.simps[simp del]
    1.54  
    1.55 @@ -402,12 +402,12 @@
    1.56  where
    1.57    "quicksort arr left right =
    1.58       (if (right > left)  then
    1.59 -        do
    1.60 +        do {
    1.61            pivotNewIndex \<leftarrow> partition arr left right;
    1.62            pivotNewIndex \<leftarrow> assert (\<lambda>x. left \<le> x \<and> x \<le> right) pivotNewIndex;
    1.63            quicksort arr left (pivotNewIndex - 1);
    1.64            quicksort arr (pivotNewIndex + 1) right
    1.65 -        done
    1.66 +        }
    1.67       else return ())"
    1.68  by pat_completeness auto
    1.69  
    1.70 @@ -645,11 +645,11 @@
    1.71  
    1.72  subsection {* Example *}
    1.73  
    1.74 -definition "qsort a = do
    1.75 +definition "qsort a = do {
    1.76      k \<leftarrow> len a;
    1.77      quicksort a 0 (k - 1);
    1.78      return a
    1.79 -  done"
    1.80 +  }"
    1.81  
    1.82  code_reserved SML upto
    1.83