src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
 changeset 37798 0b0570445a2a parent 37797 96551d6b1414 child 37802 f2e9c104cebd
```     1.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Tue Jul 13 12:05:20 2010 +0200
1.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Tue Jul 13 12:16:24 2010 +0200
1.3 @@ -14,17 +14,17 @@
1.4  where
1.5    "swap arr i j =
1.6       do {
1.7 -       x \<leftarrow> nth arr i;
1.8 -       y \<leftarrow> nth arr j;
1.9 -       upd i y arr;
1.10 -       upd j x arr;
1.11 +       x \<leftarrow> Array.nth arr i;
1.12 +       y \<leftarrow> Array.nth arr j;
1.13 +       Array.upd i y arr;
1.14 +       Array.upd j x arr;
1.15         return ()
1.16       }"
1.17
1.18  lemma crel_swapI [crel_intros]:
1.19    assumes "i < Array.length a h" "j < Array.length a h"
1.20      "x = get_array a h ! i" "y = get_array a h ! j"
1.21 -    "h' = Array.change a j x (Array.change a i y h)"
1.22 +    "h' = Array.update a j x (Array.update a i y h)"
1.23    shows "crel (swap a i j) h h' r"
1.24    unfolding swap_def using assms by (auto intro!: crel_intros)
1.25
1.26 @@ -41,7 +41,7 @@
1.27    "part1 a left right p = (
1.28       if (right \<le> left) then return right
1.29       else do {
1.30 -       v \<leftarrow> nth a left;
1.31 +       v \<leftarrow> Array.nth a left;
1.32         (if (v \<le> p) then (part1 a (left + 1) right p)
1.33                      else (do { swap a left right;
1.34    part1 a left (right - 1) p }))
1.35 @@ -228,9 +228,9 @@
1.36  fun partition :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
1.37  where
1.38    "partition a left right = do {
1.39 -     pivot \<leftarrow> nth a right;
1.40 +     pivot \<leftarrow> Array.nth a right;
1.41       middle \<leftarrow> part1 a left (right - 1) pivot;
1.42 -     v \<leftarrow> nth a middle;
1.43 +     v \<leftarrow> Array.nth a middle;
1.44       m \<leftarrow> return (if (v \<le> pivot) then (middle + 1) else middle);
1.45       swap a m right;
1.46       return m
1.47 @@ -294,8 +294,8 @@
1.48           else middle)"
1.49      unfolding partition.simps
1.50      by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) simp
1.51 -  from swap have h'_def: "h' = Array.change a r (get_array a h1 ! rs)
1.52 -    (Array.change a rs (get_array a h1 ! r) h1)"
1.53 +  from swap have h'_def: "h' = Array.update a r (get_array a h1 ! rs)
1.54 +    (Array.update a rs (get_array a h1 ! r) h1)"
1.55      unfolding swap_def
1.56      by (elim crel_bindE crel_returnE crel_nthE crel_updE) simp
1.57    from swap have in_bounds: "r < Array.length a h1 \<and> rs < Array.length a h1"
1.58 @@ -326,7 +326,7 @@
1.59        with part_partitions[OF part] right_remains True
1.60        have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
1.61        with i_props h'_def in_bounds have "get_array a h' ! i \<le> get_array a h' ! rs"
1.62 -        unfolding Array.change_def Array.length_def by simp
1.63 +        unfolding Array.update_def Array.length_def by simp
1.64      }
1.65      moreover
1.66      {
1.67 @@ -352,7 +352,7 @@
1.68            by fastsimp
1.69          with i_is True rs_equals right_remains h'_def
1.70          show ?thesis using in_bounds
1.71 -          unfolding Array.change_def Array.length_def
1.72 +          unfolding Array.update_def Array.length_def
1.73            by auto
1.74        qed
1.75      }
1.76 @@ -368,7 +368,7 @@
1.77        from part_partitions[OF part] rs_equals right_remains i_is_left
1.78        have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
1.79        with i_props h'_def have "get_array a h' ! i \<le> get_array a h' ! rs"
1.80 -        unfolding Array.change_def by simp
1.81 +        unfolding Array.update_def by simp
1.82      }
1.83      moreover
1.84      {
1.85 @@ -388,7 +388,7 @@
1.86          assume i_is: "i = r"
1.87          from i_is False rs_equals right_remains h'_def
1.88          show ?thesis using in_bounds
1.89 -          unfolding Array.change_def Array.length_def
1.90 +          unfolding Array.update_def Array.length_def
1.91            by auto
1.92        qed
1.93      }
1.94 @@ -646,7 +646,7 @@
1.95  subsection {* Example *}
1.96
1.97  definition "qsort a = do {
1.98 -    k \<leftarrow> len a;
1.99 +    k \<leftarrow> Array.len a;
1.100      quicksort a 0 (k - 1);
1.101      return a
1.102    }"
```