src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
 changeset 30689 b14b2cc4e25e parent 29793 86cac1fab613 child 31873 00878e406bf5
```     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Mon Mar 23 19:01:17 2009 +0100
1.3 @@ -0,0 +1,639 @@
1.4 +(* Author: Lukas Bulwahn, TU Muenchen *)
1.5 +
1.6 +theory Imperative_Quicksort
1.7 +imports "~~/src/HOL/Imperative_HOL/Imperative_HOL" Subarray Multiset Efficient_Nat
1.8 +begin
1.9 +
1.10 +text {* We prove QuickSort correct in the Relational Calculus. *}
1.11 +
1.12 +definition swap :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap"
1.13 +where
1.14 +  "swap arr i j = (
1.15 +     do
1.16 +       x \<leftarrow> nth arr i;
1.17 +       y \<leftarrow> nth arr j;
1.18 +       upd i y arr;
1.19 +       upd j x arr;
1.20 +       return ()
1.21 +     done)"
1.22 +
1.23 +lemma swap_permutes:
1.24 +  assumes "crel (swap a i j) h h' rs"
1.25 +  shows "multiset_of (get_array a h')
1.26 +  = multiset_of (get_array a h)"
1.27 +  using assms
1.28 +  unfolding swap_def
1.29 +  by (auto simp add: Heap.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: crelE crel_nth crel_return crel_upd)
1.30 +
1.31 +function part1 :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
1.32 +where
1.33 +  "part1 a left right p = (
1.34 +     if (right \<le> left) then return right
1.35 +     else (do
1.36 +       v \<leftarrow> nth a left;
1.37 +       (if (v \<le> p) then (part1 a (left + 1) right p)
1.38 +                    else (do swap a left right;
1.39 +  part1 a left (right - 1) p done))
1.40 +     done))"
1.41 +by pat_completeness auto
1.42 +
1.43 +termination
1.44 +by (relation "measure (\<lambda>(_,l,r,_). r - l )") auto
1.45 +
1.46 +declare part1.simps[simp del]
1.47 +
1.48 +lemma part_permutes:
1.49 +  assumes "crel (part1 a l r p) h h' rs"
1.50 +  shows "multiset_of (get_array a h')
1.51 +  = multiset_of (get_array a h)"
1.52 +  using assms
1.53 +proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
1.54 +  case (1 a l r p h h' rs)
1.55 +  thus ?case
1.56 +    unfolding part1.simps [of a l r p]
1.57 +    by (elim crelE crel_if crel_return crel_nth) (auto simp add: swap_permutes)
1.58 +qed
1.59 +
1.60 +lemma part_returns_index_in_bounds:
1.61 +  assumes "crel (part1 a l r p) h h' rs"
1.62 +  assumes "l \<le> r"
1.63 +  shows "l \<le> rs \<and> rs \<le> r"
1.64 +using assms
1.65 +proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
1.66 +  case (1 a l r p h h' rs)
1.67 +  note cr = `crel (part1 a l r p) h h' rs`
1.68 +  show ?case
1.69 +  proof (cases "r \<le> l")
1.70 +    case True (* Terminating case *)
1.71 +    with cr `l \<le> r` show ?thesis
1.72 +      unfolding part1.simps[of a l r p]
1.73 +      by (elim crelE crel_if crel_return crel_nth) auto
1.74 +  next
1.75 +    case False (* recursive case *)
1.76 +    note rec_condition = this
1.77 +    let ?v = "get_array a h ! l"
1.78 +    show ?thesis
1.79 +    proof (cases "?v \<le> p")
1.80 +      case True
1.81 +      with cr False
1.82 +      have rec1: "crel (part1 a (l + 1) r p) h h' rs"
1.83 +        unfolding part1.simps[of a l r p]
1.84 +        by (elim crelE crel_nth crel_if crel_return) auto
1.85 +      from rec_condition have "l + 1 \<le> r" by arith
1.86 +      from 1(1)[OF rec_condition True rec1 `l + 1 \<le> r`]
1.87 +      show ?thesis by simp
1.88 +    next
1.89 +      case False
1.90 +      with rec_condition cr
1.91 +      obtain h1 where swp: "crel (swap a l r) h h1 ()"
1.92 +        and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
1.93 +        unfolding part1.simps[of a l r p]
1.94 +        by (elim crelE crel_nth crel_if crel_return) auto
1.95 +      from rec_condition have "l \<le> r - 1" by arith
1.96 +      from 1(2) [OF rec_condition False rec2 `l \<le> r - 1`] show ?thesis by fastsimp
1.97 +    qed
1.98 +  qed
1.99 +qed
1.100 +
1.101 +lemma part_length_remains:
1.102 +  assumes "crel (part1 a l r p) h h' rs"
1.103 +  shows "Heap.length a h = Heap.length a h'"
1.104 +using assms
1.105 +proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
1.106 +  case (1 a l r p h h' rs)
1.107 +  note cr = `crel (part1 a l r p) h h' rs`
1.108 +
1.109 +  show ?case
1.110 +  proof (cases "r \<le> l")
1.111 +    case True (* Terminating case *)
1.112 +    with cr show ?thesis
1.113 +      unfolding part1.simps[of a l r p]
1.114 +      by (elim crelE crel_if crel_return crel_nth) auto
1.115 +  next
1.116 +    case False (* recursive case *)
1.117 +    with cr 1 show ?thesis
1.118 +      unfolding part1.simps [of a l r p] swap_def
1.119 +      by (auto elim!: crelE crel_if crel_nth crel_return crel_upd) fastsimp
1.120 +  qed
1.121 +qed
1.122 +
1.123 +lemma part_outer_remains:
1.124 +  assumes "crel (part1 a l r p) h h' rs"
1.125 +  shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array (a::nat array) h ! i = get_array a h' ! i"
1.126 +  using assms
1.127 +proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
1.128 +  case (1 a l r p h h' rs)
1.129 +  note cr = `crel (part1 a l r p) h h' rs`
1.130 +
1.131 +  show ?case
1.132 +  proof (cases "r \<le> l")
1.133 +    case True (* Terminating case *)
1.134 +    with cr show ?thesis
1.135 +      unfolding part1.simps[of a l r p]
1.136 +      by (elim crelE crel_if crel_return crel_nth) auto
1.137 +  next
1.138 +    case False (* recursive case *)
1.139 +    note rec_condition = this
1.140 +    let ?v = "get_array a h ! l"
1.141 +    show ?thesis
1.142 +    proof (cases "?v \<le> p")
1.143 +      case True
1.144 +      with cr False
1.145 +      have rec1: "crel (part1 a (l + 1) r p) h h' rs"
1.146 +        unfolding part1.simps[of a l r p]
1.147 +        by (elim crelE crel_nth crel_if crel_return) auto
1.148 +      from 1(1)[OF rec_condition True rec1]
1.149 +      show ?thesis by fastsimp
1.150 +    next
1.151 +      case False
1.152 +      with rec_condition cr
1.153 +      obtain h1 where swp: "crel (swap a l r) h h1 ()"
1.154 +        and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
1.155 +        unfolding part1.simps[of a l r p]
1.156 +        by (elim crelE crel_nth crel_if crel_return) auto
1.157 +      from swp rec_condition have
1.158 +        "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array a h ! i = get_array a h1 ! i"
1.159 +	unfolding swap_def
1.160 +	by (elim crelE crel_nth crel_upd crel_return) auto
1.161 +      with 1(2) [OF rec_condition False rec2] show ?thesis by fastsimp
1.162 +    qed
1.163 +  qed
1.164 +qed
1.165 +
1.166 +
1.167 +lemma part_partitions:
1.168 +  assumes "crel (part1 a l r p) h h' rs"
1.169 +  shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> get_array (a::nat array) h' ! i \<le> p)
1.170 +  \<and> (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> get_array a h' ! i \<ge> p)"
1.171 +  using assms
1.172 +proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
1.173 +  case (1 a l r p h h' rs)
1.174 +  note cr = `crel (part1 a l r p) h h' rs`
1.175 +
1.176 +  show ?case
1.177 +  proof (cases "r \<le> l")
1.178 +    case True (* Terminating case *)
1.179 +    with cr have "rs = r"
1.180 +      unfolding part1.simps[of a l r p]
1.181 +      by (elim crelE crel_if crel_return crel_nth) auto
1.182 +    with True
1.183 +    show ?thesis by auto
1.184 +  next
1.185 +    case False (* recursive case *)
1.186 +    note lr = this
1.187 +    let ?v = "get_array a h ! l"
1.188 +    show ?thesis
1.189 +    proof (cases "?v \<le> p")
1.190 +      case True
1.191 +      with lr cr
1.192 +      have rec1: "crel (part1 a (l + 1) r p) h h' rs"
1.193 +        unfolding part1.simps[of a l r p]
1.194 +        by (elim crelE crel_nth crel_if crel_return) auto
1.195 +      from True part_outer_remains[OF rec1] have a_l: "get_array a h' ! l \<le> p"
1.196 +	by fastsimp
1.197 +      have "\<forall>i. (l \<le> i = (l = i \<or> Suc l \<le> i))" by arith
1.198 +      with 1(1)[OF False True rec1] a_l show ?thesis
1.199 +	by auto
1.200 +    next
1.201 +      case False
1.202 +      with lr cr
1.203 +      obtain h1 where swp: "crel (swap a l r) h h1 ()"
1.204 +        and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
1.205 +        unfolding part1.simps[of a l r p]
1.206 +        by (elim crelE crel_nth crel_if crel_return) auto
1.207 +      from swp False have "get_array a h1 ! r \<ge> p"
1.208 +	unfolding swap_def
1.209 +	by (auto simp add: Heap.length_def elim!: crelE crel_nth crel_upd crel_return)
1.210 +      with part_outer_remains [OF rec2] lr have a_r: "get_array a h' ! r \<ge> p"
1.211 +	by fastsimp
1.212 +      have "\<forall>i. (i \<le> r = (i = r \<or> i \<le> r - 1))" by arith
1.213 +      with 1(2)[OF lr False rec2] a_r show ?thesis
1.214 +	by auto
1.215 +    qed
1.216 +  qed
1.217 +qed
1.218 +
1.219 +
1.220 +fun partition :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
1.221 +where
1.222 +  "partition a left right = (do
1.223 +     pivot \<leftarrow> nth a right;
1.224 +     middle \<leftarrow> part1 a left (right - 1) pivot;
1.225 +     v \<leftarrow> nth a middle;
1.226 +     m \<leftarrow> return (if (v \<le> pivot) then (middle + 1) else middle);
1.227 +     swap a m right;
1.228 +     return m
1.229 +   done)"
1.230 +
1.231 +declare partition.simps[simp del]
1.232 +
1.233 +lemma partition_permutes:
1.234 +  assumes "crel (partition a l r) h h' rs"
1.235 +  shows "multiset_of (get_array a h')
1.236 +  = multiset_of (get_array a h)"
1.237 +proof -
1.238 +    from assms part_permutes swap_permutes show ?thesis
1.239 +      unfolding partition.simps
1.240 +      by (elim crelE crel_return crel_nth crel_if crel_upd) auto
1.241 +qed
1.242 +
1.243 +lemma partition_length_remains:
1.244 +  assumes "crel (partition a l r) h h' rs"
1.245 +  shows "Heap.length a h = Heap.length a h'"
1.246 +proof -
1.247 +  from assms part_length_remains show ?thesis
1.248 +    unfolding partition.simps swap_def
1.249 +    by (elim crelE crel_return crel_nth crel_if crel_upd) auto
1.250 +qed
1.251 +
1.252 +lemma partition_outer_remains:
1.253 +  assumes "crel (partition a l r) h h' rs"
1.254 +  assumes "l < r"
1.255 +  shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array (a::nat array) h ! i = get_array a h' ! i"
1.256 +proof -
1.257 +  from assms part_outer_remains part_returns_index_in_bounds show ?thesis
1.258 +    unfolding partition.simps swap_def
1.259 +    by (elim crelE crel_return crel_nth crel_if crel_upd) fastsimp
1.260 +qed
1.261 +
1.262 +lemma partition_returns_index_in_bounds:
1.263 +  assumes crel: "crel (partition a l r) h h' rs"
1.264 +  assumes "l < r"
1.265 +  shows "l \<le> rs \<and> rs \<le> r"
1.266 +proof -
1.267 +  from crel obtain middle h'' p where part: "crel (part1 a l (r - 1) p) h h'' middle"
1.268 +    and rs_equals: "rs = (if get_array a h'' ! middle \<le> get_array a h ! r then middle + 1
1.269 +         else middle)"
1.270 +    unfolding partition.simps
1.271 +    by (elim crelE crel_return crel_nth crel_if crel_upd) simp
1.272 +  from `l < r` have "l \<le> r - 1" by arith
1.273 +  from part_returns_index_in_bounds[OF part this] rs_equals `l < r` show ?thesis by auto
1.274 +qed
1.275 +
1.276 +lemma partition_partitions:
1.277 +  assumes crel: "crel (partition a l r) h h' rs"
1.278 +  assumes "l < r"
1.279 +  shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> get_array (a::nat array) h' ! i \<le> get_array a h' ! rs) \<and>
1.280 +  (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> get_array a h' ! rs \<le> get_array a h' ! i)"
1.281 +proof -
1.282 +  let ?pivot = "get_array a h ! r"
1.283 +  from crel obtain middle h1 where part: "crel (part1 a l (r - 1) ?pivot) h h1 middle"
1.284 +    and swap: "crel (swap a rs r) h1 h' ()"
1.285 +    and rs_equals: "rs = (if get_array a h1 ! middle \<le> ?pivot then middle + 1
1.286 +         else middle)"
1.287 +    unfolding partition.simps
1.288 +    by (elim crelE crel_return crel_nth crel_if crel_upd) simp
1.289 +  from swap have h'_def: "h' = Heap.upd a r (get_array a h1 ! rs)
1.290 +    (Heap.upd a rs (get_array a h1 ! r) h1)"
1.291 +    unfolding swap_def
1.292 +    by (elim crelE crel_return crel_nth crel_upd) simp
1.293 +  from swap have in_bounds: "r < Heap.length a h1 \<and> rs < Heap.length a h1"
1.294 +    unfolding swap_def
1.295 +    by (elim crelE crel_return crel_nth crel_upd) simp
1.296 +  from swap have swap_length_remains: "Heap.length a h1 = Heap.length a h'"
1.297 +    unfolding swap_def by (elim crelE crel_return crel_nth crel_upd) auto
1.298 +  from `l < r` have "l \<le> r - 1" by simp
1.299 +  note middle_in_bounds = part_returns_index_in_bounds[OF part this]
1.300 +  from part_outer_remains[OF part] `l < r`
1.301 +  have "get_array a h ! r = get_array a h1 ! r"
1.302 +    by fastsimp
1.303 +  with swap
1.304 +  have right_remains: "get_array a h ! r = get_array a h' ! rs"
1.305 +    unfolding swap_def
1.306 +    by (auto simp add: Heap.length_def elim!: crelE crel_return crel_nth crel_upd) (cases "r = rs", auto)
1.307 +  from part_partitions [OF part]
1.308 +  show ?thesis
1.309 +  proof (cases "get_array a h1 ! middle \<le> ?pivot")
1.310 +    case True
1.311 +    with rs_equals have rs_equals: "rs = middle + 1" by simp
1.312 +    {
1.313 +      fix i
1.314 +      assume i_is_left: "l \<le> i \<and> i < rs"
1.315 +      with swap_length_remains in_bounds middle_in_bounds rs_equals `l < r`
1.316 +      have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
1.317 +      from i_is_left rs_equals have "l \<le> i \<and> i < middle \<or> i = middle" by arith
1.318 +      with part_partitions[OF part] right_remains True
1.319 +      have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
1.320 +      with i_props h'_def in_bounds have "get_array a h' ! i \<le> get_array a h' ! rs"
1.321 +	unfolding Heap.upd_def Heap.length_def by simp
1.322 +    }
1.323 +    moreover
1.324 +    {
1.325 +      fix i
1.326 +      assume "rs < i \<and> i \<le> r"
1.327 +
1.328 +      hence "(rs < i \<and> i \<le> r - 1) \<or> (rs < i \<and> i = r)" by arith
1.329 +      hence "get_array a h' ! rs \<le> get_array a h' ! i"
1.330 +      proof
1.331 +	assume i_is: "rs < i \<and> i \<le> r - 1"
1.332 +	with swap_length_remains in_bounds middle_in_bounds rs_equals
1.333 +	have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
1.334 +	from part_partitions[OF part] rs_equals right_remains i_is
1.335 +	have "get_array a h' ! rs \<le> get_array a h1 ! i"
1.336 +	  by fastsimp
1.337 +	with i_props h'_def show ?thesis by fastsimp
1.338 +      next
1.339 +	assume i_is: "rs < i \<and> i = r"
1.340 +	with rs_equals have "Suc middle \<noteq> r" by arith
1.341 +	with middle_in_bounds `l < r` have "Suc middle \<le> r - 1" by arith
1.342 +	with part_partitions[OF part] right_remains
1.343 +	have "get_array a h' ! rs \<le> get_array a h1 ! (Suc middle)"
1.344 +	  by fastsimp
1.345 +	with i_is True rs_equals right_remains h'_def
1.346 +	show ?thesis using in_bounds
1.347 +	  unfolding Heap.upd_def Heap.length_def
1.348 +	  by auto
1.349 +      qed
1.350 +    }
1.351 +    ultimately show ?thesis by auto
1.352 +  next
1.353 +    case False
1.354 +    with rs_equals have rs_equals: "middle = rs" by simp
1.355 +    {
1.356 +      fix i
1.357 +      assume i_is_left: "l \<le> i \<and> i < rs"
1.358 +      with swap_length_remains in_bounds middle_in_bounds rs_equals
1.359 +      have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
1.360 +      from part_partitions[OF part] rs_equals right_remains i_is_left
1.361 +      have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
1.362 +      with i_props h'_def have "get_array a h' ! i \<le> get_array a h' ! rs"
1.363 +	unfolding Heap.upd_def by simp
1.364 +    }
1.365 +    moreover
1.366 +    {
1.367 +      fix i
1.368 +      assume "rs < i \<and> i \<le> r"
1.369 +      hence "(rs < i \<and> i \<le> r - 1) \<or> i = r" by arith
1.370 +      hence "get_array a h' ! rs \<le> get_array a h' ! i"
1.371 +      proof
1.372 +	assume i_is: "rs < i \<and> i \<le> r - 1"
1.373 +	with swap_length_remains in_bounds middle_in_bounds rs_equals
1.374 +	have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
1.375 +	from part_partitions[OF part] rs_equals right_remains i_is
1.376 +	have "get_array a h' ! rs \<le> get_array a h1 ! i"
1.377 +	  by fastsimp
1.378 +	with i_props h'_def show ?thesis by fastsimp
1.379 +      next
1.380 +	assume i_is: "i = r"
1.381 +	from i_is False rs_equals right_remains h'_def
1.382 +	show ?thesis using in_bounds
1.383 +	  unfolding Heap.upd_def Heap.length_def
1.384 +	  by auto
1.385 +      qed
1.386 +    }
1.387 +    ultimately
1.388 +    show ?thesis by auto
1.389 +  qed
1.390 +qed
1.391 +
1.392 +
1.393 +function quicksort :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap"
1.394 +where
1.395 +  "quicksort arr left right =
1.396 +     (if (right > left)  then
1.397 +        do
1.398 +          pivotNewIndex \<leftarrow> partition arr left right;
1.399 +          pivotNewIndex \<leftarrow> assert (\<lambda>x. left \<le> x \<and> x \<le> right) pivotNewIndex;
1.400 +          quicksort arr left (pivotNewIndex - 1);
1.401 +          quicksort arr (pivotNewIndex + 1) right
1.402 +        done
1.403 +     else return ())"
1.404 +by pat_completeness auto
1.405 +
1.406 +(* For termination, we must show that the pivotNewIndex is between left and right *)
1.407 +termination
1.408 +by (relation "measure (\<lambda>(a, l, r). (r - l))") auto
1.409 +
1.410 +declare quicksort.simps[simp del]
1.411 +
1.412 +
1.413 +lemma quicksort_permutes:
1.414 +  assumes "crel (quicksort a l r) h h' rs"
1.415 +  shows "multiset_of (get_array a h')
1.416 +  = multiset_of (get_array a h)"
1.417 +  using assms
1.418 +proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
1.419 +  case (1 a l r h h' rs)
1.420 +  with partition_permutes show ?case
1.421 +    unfolding quicksort.simps [of a l r]
1.422 +    by (elim crel_if crelE crel_assert crel_return) auto
1.423 +qed
1.424 +
1.425 +lemma length_remains:
1.426 +  assumes "crel (quicksort a l r) h h' rs"
1.427 +  shows "Heap.length a h = Heap.length a h'"
1.428 +using assms
1.429 +proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
1.430 +  case (1 a l r h h' rs)
1.431 +  with partition_length_remains show ?case
1.432 +    unfolding quicksort.simps [of a l r]
1.433 +    by (elim crel_if crelE crel_assert crel_return) auto
1.434 +qed
1.435 +
1.436 +lemma quicksort_outer_remains:
1.437 +  assumes "crel (quicksort a l r) h h' rs"
1.438 +   shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array (a::nat array) h ! i = get_array a h' ! i"
1.439 +  using assms
1.440 +proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
1.441 +  case (1 a l r h h' rs)
1.442 +  note cr = `crel (quicksort a l r) h h' rs`
1.443 +  thus ?case
1.444 +  proof (cases "r > l")
1.445 +    case False
1.446 +    with cr have "h' = h"
1.447 +      unfolding quicksort.simps [of a l r]
1.448 +      by (elim crel_if crel_return) auto
1.449 +    thus ?thesis by simp
1.450 +  next
1.451 +  case True
1.452 +   {
1.453 +      fix h1 h2 p ret1 ret2 i
1.454 +      assume part: "crel (partition a l r) h h1 p"
1.455 +      assume qs1: "crel (quicksort a l (p - 1)) h1 h2 ret1"
1.456 +      assume qs2: "crel (quicksort a (p + 1) r) h2 h' ret2"
1.457 +      assume pivot: "l \<le> p \<and> p \<le> r"
1.458 +      assume i_outer: "i < l \<or> r < i"
1.459 +      from  partition_outer_remains [OF part True] i_outer
1.460 +      have "get_array a h !i = get_array a h1 ! i" by fastsimp
1.461 +      moreover
1.462 +      with 1(1) [OF True pivot qs1] pivot i_outer
1.463 +      have "get_array a h1 ! i = get_array a h2 ! i" by auto
1.464 +      moreover
1.465 +      with qs2 1(2) [of p h2 h' ret2] True pivot i_outer
1.466 +      have "get_array a h2 ! i = get_array a h' ! i" by auto
1.467 +      ultimately have "get_array a h ! i= get_array a h' ! i" by simp
1.468 +    }
1.469 +    with cr show ?thesis
1.470 +      unfolding quicksort.simps [of a l r]
1.471 +      by (elim crel_if crelE crel_assert crel_return) auto
1.472 +  qed
1.473 +qed
1.474 +
1.475 +lemma quicksort_is_skip:
1.476 +  assumes "crel (quicksort a l r) h h' rs"
1.477 +  shows "r \<le> l \<longrightarrow> h = h'"
1.478 +  using assms
1.479 +  unfolding quicksort.simps [of a l r]
1.480 +  by (elim crel_if crel_return) auto
1.481 +
1.482 +lemma quicksort_sorts:
1.483 +  assumes "crel (quicksort a l r) h h' rs"
1.484 +  assumes l_r_length: "l < Heap.length a h" "r < Heap.length a h"
1.485 +  shows "sorted (subarray l (r + 1) a h')"
1.486 +  using assms
1.487 +proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
1.488 +  case (1 a l r h h' rs)
1.489 +  note cr = `crel (quicksort a l r) h h' rs`
1.490 +  thus ?case
1.491 +  proof (cases "r > l")
1.492 +    case False
1.493 +    hence "l \<ge> r + 1 \<or> l = r" by arith
1.494 +    with length_remains[OF cr] 1(5) show ?thesis
1.495 +      by (auto simp add: subarray_Nil subarray_single)
1.496 +  next
1.497 +    case True
1.498 +    {
1.499 +      fix h1 h2 p
1.500 +      assume part: "crel (partition a l r) h h1 p"
1.501 +      assume qs1: "crel (quicksort a l (p - 1)) h1 h2 ()"
1.502 +      assume qs2: "crel (quicksort a (p + 1) r) h2 h' ()"
1.503 +      from partition_returns_index_in_bounds [OF part True]
1.504 +      have pivot: "l\<le> p \<and> p \<le> r" .
1.505 +     note length_remains = length_remains[OF qs2] length_remains[OF qs1] partition_length_remains[OF part]
1.506 +      from quicksort_outer_remains [OF qs2] quicksort_outer_remains [OF qs1] pivot quicksort_is_skip[OF qs1]
1.507 +      have pivot_unchanged: "get_array a h1 ! p = get_array a h' ! p" by (cases p, auto)
1.508 +        (*-- First of all, by induction hypothesis both sublists are sorted. *)
1.509 +      from 1(1)[OF True pivot qs1] length_remains pivot 1(5)
1.510 +      have IH1: "sorted (subarray l p a h2)"  by (cases p, auto simp add: subarray_Nil)
1.511 +      from quicksort_outer_remains [OF qs2] length_remains
1.512 +      have left_subarray_remains: "subarray l p a h2 = subarray l p a h'"
1.513 +	by (simp add: subarray_eq_samelength_iff)
1.514 +      with IH1 have IH1': "sorted (subarray l p a h')" by simp
1.515 +      from 1(2)[OF True pivot qs2] pivot 1(5) length_remains
1.516 +      have IH2: "sorted (subarray (p + 1) (r + 1) a h')"
1.517 +        by (cases "Suc p \<le> r", auto simp add: subarray_Nil)
1.518 +           (* -- Secondly, both sublists remain partitioned. *)
1.519 +      from partition_partitions[OF part True]
1.520 +      have part_conds1: "\<forall>j. j \<in> set (subarray l p a h1) \<longrightarrow> j \<le> get_array a h1 ! p "
1.521 +        and part_conds2: "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h1) \<longrightarrow> get_array a h1 ! p \<le> j"
1.522 +        by (auto simp add: all_in_set_subarray_conv)
1.523 +      from quicksort_outer_remains [OF qs1] quicksort_permutes [OF qs1] True
1.524 +        length_remains 1(5) pivot multiset_of_sublist [of l p "get_array a h1" "get_array a h2"]
1.525 +      have multiset_partconds1: "multiset_of (subarray l p a h2) = multiset_of (subarray l p a h1)"
1.526 +	unfolding Heap.length_def subarray_def by (cases p, auto)
1.527 +      with left_subarray_remains part_conds1 pivot_unchanged
1.528 +      have part_conds2': "\<forall>j. j \<in> set (subarray l p a h') \<longrightarrow> j \<le> get_array a h' ! p"
1.529 +        by (simp, subst set_of_multiset_of[symmetric], simp)
1.530 +          (* -- These steps are the analogous for the right sublist \<dots> *)
1.531 +      from quicksort_outer_remains [OF qs1] length_remains
1.532 +      have right_subarray_remains: "subarray (p + 1) (r + 1) a h1 = subarray (p + 1) (r + 1) a h2"
1.533 +	by (auto simp add: subarray_eq_samelength_iff)
1.534 +      from quicksort_outer_remains [OF qs2] quicksort_permutes [OF qs2] True
1.535 +        length_remains 1(5) pivot multiset_of_sublist [of "p + 1" "r + 1" "get_array a h2" "get_array a h'"]
1.536 +      have multiset_partconds2: "multiset_of (subarray (p + 1) (r + 1) a h') = multiset_of (subarray (p + 1) (r + 1) a h2)"
1.537 +        unfolding Heap.length_def subarray_def by auto
1.538 +      with right_subarray_remains part_conds2 pivot_unchanged
1.539 +      have part_conds1': "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h') \<longrightarrow> get_array a h' ! p \<le> j"
1.540 +        by (simp, subst set_of_multiset_of[symmetric], simp)
1.541 +          (* -- Thirdly and finally, we show that the array is sorted
1.542 +          following from the facts above. *)
1.543 +      from True pivot 1(5) length_remains have "subarray l (r + 1) a h' = subarray l p a h' @ [get_array a h' ! p] @ subarray (p + 1) (r + 1) a h'"
1.544 +	by (simp add: subarray_nth_array_Cons, cases "l < p") (auto simp add: subarray_append subarray_Nil)
1.545 +      with IH1' IH2 part_conds1' part_conds2' pivot have ?thesis
1.546 +	unfolding subarray_def
1.547 +	apply (auto simp add: sorted_append sorted_Cons all_in_set_sublist'_conv)
1.548 +	by (auto simp add: set_sublist' dest: le_trans [of _ "get_array a h' ! p"])
1.549 +    }
1.550 +    with True cr show ?thesis
1.551 +      unfolding quicksort.simps [of a l r]
1.552 +      by (elim crel_if crel_return crelE crel_assert) auto
1.553 +  qed
1.554 +qed
1.555 +
1.556 +
1.557 +lemma quicksort_is_sort:
1.558 +  assumes crel: "crel (quicksort a 0 (Heap.length a h - 1)) h h' rs"
1.559 +  shows "get_array a h' = sort (get_array a h)"
1.560 +proof (cases "get_array a h = []")
1.561 +  case True
1.562 +  with quicksort_is_skip[OF crel] show ?thesis
1.563 +  unfolding Heap.length_def by simp
1.564 +next
1.565 +  case False
1.566 +  from quicksort_sorts [OF crel] False have "sorted (sublist' 0 (List.length (get_array a h)) (get_array a h'))"
1.567 +    unfolding Heap.length_def subarray_def by auto
1.568 +  with length_remains[OF crel] have "sorted (get_array a h')"
1.569 +    unfolding Heap.length_def by simp
1.570 +  with quicksort_permutes [OF crel] properties_for_sort show ?thesis by fastsimp
1.571 +qed
1.572 +
1.573 +subsection {* No Errors in quicksort *}
1.574 +text {* We have proved that quicksort sorts (if no exceptions occur).
1.575 +We will now show that exceptions do not occur. *}
1.576 +
1.577 +lemma noError_part1:
1.578 +  assumes "l < Heap.length a h" "r < Heap.length a h"
1.579 +  shows "noError (part1 a l r p) h"
1.580 +  using assms
1.581 +proof (induct a l r p arbitrary: h rule: part1.induct)
1.582 +  case (1 a l r p)
1.583 +  thus ?case
1.584 +    unfolding part1.simps [of a l r] swap_def
1.585 +    by (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd elim!: crelE crel_upd crel_nth crel_return)
1.586 +qed
1.587 +
1.588 +lemma noError_partition:
1.589 +  assumes "l < r" "l < Heap.length a h" "r < Heap.length a h"
1.590 +  shows "noError (partition a l r) h"
1.591 +using assms
1.592 +unfolding partition.simps swap_def
1.593 +apply (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd noError_part1 elim!: crelE crel_upd crel_nth crel_return)
1.594 +apply (frule part_length_remains)
1.595 +apply (frule part_returns_index_in_bounds)
1.596 +apply auto
1.597 +apply (frule part_length_remains)
1.598 +apply (frule part_returns_index_in_bounds)
1.599 +apply auto
1.600 +apply (frule part_length_remains)
1.601 +apply auto
1.602 +done
1.603 +
1.604 +lemma noError_quicksort:
1.605 +  assumes "l < Heap.length a h" "r < Heap.length a h"
1.606 +  shows "noError (quicksort a l r) h"
1.607 +using assms
1.608 +proof (induct a l r arbitrary: h rule: quicksort.induct)
1.609 +  case (1 a l ri h)
1.610 +  thus ?case
1.611 +    unfolding quicksort.simps [of a l ri]
1.612 +    apply (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd noError_assert noError_partition)
1.613 +    apply (frule partition_returns_index_in_bounds)
1.614 +    apply auto
1.615 +    apply (frule partition_returns_index_in_bounds)
1.616 +    apply auto
1.617 +    apply (auto elim!: crel_assert dest!: partition_length_remains length_remains)
1.618 +    apply (subgoal_tac "Suc r \<le> ri \<or> r = ri")
1.619 +    apply (erule disjE)
1.620 +    apply auto
1.621 +    unfolding quicksort.simps [of a "Suc ri" ri]
1.622 +    apply (auto intro!: noError_if noError_return)
1.623 +    done
1.624 +qed
1.625 +
1.626 +
1.627 +subsection {* Example *}
1.628 +
1.629 +definition "qsort a = do
1.630 +    k \<leftarrow> length a;
1.631 +    quicksort a 0 (k - 1);
1.632 +    return a
1.633 +  done"
1.634 +
1.635 +ML {* @{code qsort} (Array.fromList [42, 2, 3, 5, 0, 1705, 8, 3, 15]) () *}
1.636 +
1.637 +export_code qsort in SML_imp module_name QSort
1.638 +export_code qsort in OCaml module_name QSort file -
1.639 +export_code qsort in OCaml_imp module_name QSort file -
1.640 +export_code qsort in Haskell module_name QSort file -
1.641 +
1.642 +end
1.643 \ No newline at end of file
```