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    }"