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