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
```