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