src/HOL/ex/ImperativeQuicksort.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 29793 86cac1fab613
permissions -rw-r--r--
added lemmas
     1 theory ImperativeQuicksort
     2 imports "~~/src/HOL/Imperative_HOL/Imperative_HOL" Subarray Multiset Efficient_Nat
     3 begin
     4 
     5 text {* We prove QuickSort correct in the Relational Calculus. *}
     6 
     7 definition swap :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap"
     8 where
     9   "swap arr i j = (
    10      do
    11        x \<leftarrow> nth arr i;
    12        y \<leftarrow> nth arr j;
    13        upd i y arr;
    14        upd j x arr;
    15        return ()
    16      done)"
    17 
    18 lemma swap_permutes:
    19   assumes "crel (swap a i j) h h' rs"
    20   shows "multiset_of (get_array a h') 
    21   = multiset_of (get_array a h)"
    22   using assms
    23   unfolding swap_def
    24   by (auto simp add: Heap.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: crelE crel_nth crel_return crel_upd)
    25 
    26 function part1 :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
    27 where
    28   "part1 a left right p = (
    29      if (right \<le> left) then return right
    30      else (do
    31        v \<leftarrow> nth a left;
    32        (if (v \<le> p) then (part1 a (left + 1) right p)
    33                     else (do swap a left right;
    34   part1 a left (right - 1) p done))
    35      done))"
    36 by pat_completeness auto
    37 
    38 termination
    39 by (relation "measure (\<lambda>(_,l,r,_). r - l )") auto
    40 
    41 declare part1.simps[simp del]
    42 
    43 lemma part_permutes:
    44   assumes "crel (part1 a l r p) h h' rs"
    45   shows "multiset_of (get_array a h') 
    46   = multiset_of (get_array a h)"
    47   using assms
    48 proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
    49   case (1 a l r p h h' rs)
    50   thus ?case
    51     unfolding part1.simps [of a l r p]
    52     by (elim crelE crel_if crel_return crel_nth) (auto simp add: swap_permutes)
    53 qed
    54 
    55 lemma part_returns_index_in_bounds:
    56   assumes "crel (part1 a l r p) h h' rs"
    57   assumes "l \<le> r"
    58   shows "l \<le> rs \<and> rs \<le> r"
    59 using assms
    60 proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
    61   case (1 a l r p h h' rs)
    62   note cr = `crel (part1 a l r p) h h' rs`
    63   show ?case
    64   proof (cases "r \<le> l")
    65     case True (* Terminating case *)
    66     with cr `l \<le> r` show ?thesis
    67       unfolding part1.simps[of a l r p]
    68       by (elim crelE crel_if crel_return crel_nth) auto
    69   next
    70     case False (* recursive case *)
    71     note rec_condition = this
    72     let ?v = "get_array a h ! l"
    73     show ?thesis
    74     proof (cases "?v \<le> p")
    75       case True
    76       with cr False
    77       have rec1: "crel (part1 a (l + 1) r p) h h' rs"
    78         unfolding part1.simps[of a l r p]
    79         by (elim crelE crel_nth crel_if crel_return) auto
    80       from rec_condition have "l + 1 \<le> r" by arith
    81       from 1(1)[OF rec_condition True rec1 `l + 1 \<le> r`]
    82       show ?thesis by simp
    83     next
    84       case False
    85       with rec_condition cr
    86       obtain h1 where swp: "crel (swap a l r) h h1 ()"
    87         and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
    88         unfolding part1.simps[of a l r p]
    89         by (elim crelE crel_nth crel_if crel_return) auto
    90       from rec_condition have "l \<le> r - 1" by arith
    91       from 1(2) [OF rec_condition False rec2 `l \<le> r - 1`] show ?thesis by fastsimp
    92     qed
    93   qed
    94 qed
    95 
    96 lemma part_length_remains:
    97   assumes "crel (part1 a l r p) h h' rs"
    98   shows "Heap.length a h = Heap.length a h'"
    99 using assms
   100 proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
   101   case (1 a l r p h h' rs)
   102   note cr = `crel (part1 a l r p) h h' rs`
   103   
   104   show ?case
   105   proof (cases "r \<le> l")
   106     case True (* Terminating case *)
   107     with cr show ?thesis
   108       unfolding part1.simps[of a l r p]
   109       by (elim crelE crel_if crel_return crel_nth) auto
   110   next
   111     case False (* recursive case *)
   112     with cr 1 show ?thesis
   113       unfolding part1.simps [of a l r p] swap_def
   114       by (auto elim!: crelE crel_if crel_nth crel_return crel_upd) fastsimp
   115   qed
   116 qed
   117 
   118 lemma part_outer_remains:
   119   assumes "crel (part1 a l r p) h h' rs"
   120   shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array (a::nat array) h ! i = get_array a h' ! i"
   121   using assms
   122 proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
   123   case (1 a l r p h h' rs)
   124   note cr = `crel (part1 a l r p) h h' rs`
   125   
   126   show ?case
   127   proof (cases "r \<le> l")
   128     case True (* Terminating case *)
   129     with cr show ?thesis
   130       unfolding part1.simps[of a l r p]
   131       by (elim crelE crel_if crel_return crel_nth) auto
   132   next
   133     case False (* recursive case *)
   134     note rec_condition = this
   135     let ?v = "get_array a h ! l"
   136     show ?thesis
   137     proof (cases "?v \<le> p")
   138       case True
   139       with cr False
   140       have rec1: "crel (part1 a (l + 1) r p) h h' rs"
   141         unfolding part1.simps[of a l r p]
   142         by (elim crelE crel_nth crel_if crel_return) auto
   143       from 1(1)[OF rec_condition True rec1]
   144       show ?thesis by fastsimp
   145     next
   146       case False
   147       with rec_condition cr
   148       obtain h1 where swp: "crel (swap a l r) h h1 ()"
   149         and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
   150         unfolding part1.simps[of a l r p]
   151         by (elim crelE crel_nth crel_if crel_return) auto
   152       from swp rec_condition have
   153         "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array a h ! i = get_array a h1 ! i"
   154 	unfolding swap_def
   155 	by (elim crelE crel_nth crel_upd crel_return) auto
   156       with 1(2) [OF rec_condition False rec2] show ?thesis by fastsimp
   157     qed
   158   qed
   159 qed
   160 
   161 
   162 lemma part_partitions:
   163   assumes "crel (part1 a l r p) h h' rs"
   164   shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> get_array (a::nat array) h' ! i \<le> p)
   165   \<and> (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> get_array a h' ! i \<ge> p)"
   166   using assms
   167 proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
   168   case (1 a l r p h h' rs)
   169   note cr = `crel (part1 a l r p) h h' rs`
   170   
   171   show ?case
   172   proof (cases "r \<le> l")
   173     case True (* Terminating case *)
   174     with cr have "rs = r"
   175       unfolding part1.simps[of a l r p]
   176       by (elim crelE crel_if crel_return crel_nth) auto
   177     with True
   178     show ?thesis by auto
   179   next
   180     case False (* recursive case *)
   181     note lr = this
   182     let ?v = "get_array a h ! l"
   183     show ?thesis
   184     proof (cases "?v \<le> p")
   185       case True
   186       with lr cr
   187       have rec1: "crel (part1 a (l + 1) r p) h h' rs"
   188         unfolding part1.simps[of a l r p]
   189         by (elim crelE crel_nth crel_if crel_return) auto
   190       from True part_outer_remains[OF rec1] have a_l: "get_array a h' ! l \<le> p"
   191 	by fastsimp
   192       have "\<forall>i. (l \<le> i = (l = i \<or> Suc l \<le> i))" by arith
   193       with 1(1)[OF False True rec1] a_l show ?thesis
   194 	by auto
   195     next
   196       case False
   197       with lr cr
   198       obtain h1 where swp: "crel (swap a l r) h h1 ()"
   199         and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
   200         unfolding part1.simps[of a l r p]
   201         by (elim crelE crel_nth crel_if crel_return) auto
   202       from swp False have "get_array a h1 ! r \<ge> p"
   203 	unfolding swap_def
   204 	by (auto simp add: Heap.length_def elim!: crelE crel_nth crel_upd crel_return)
   205       with part_outer_remains [OF rec2] lr have a_r: "get_array a h' ! r \<ge> p"
   206 	by fastsimp
   207       have "\<forall>i. (i \<le> r = (i = r \<or> i \<le> r - 1))" by arith
   208       with 1(2)[OF lr False rec2] a_r show ?thesis
   209 	by auto
   210     qed
   211   qed
   212 qed
   213 
   214 
   215 fun partition :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
   216 where
   217   "partition a left right = (do
   218      pivot \<leftarrow> nth a right;
   219      middle \<leftarrow> part1 a left (right - 1) pivot;
   220      v \<leftarrow> nth a middle;
   221      m \<leftarrow> return (if (v \<le> pivot) then (middle + 1) else middle);
   222      swap a m right;
   223      return m
   224    done)"
   225 
   226 declare partition.simps[simp del]
   227 
   228 lemma partition_permutes:
   229   assumes "crel (partition a l r) h h' rs"
   230   shows "multiset_of (get_array a h') 
   231   = multiset_of (get_array a h)"
   232 proof -
   233     from assms part_permutes swap_permutes show ?thesis
   234       unfolding partition.simps
   235       by (elim crelE crel_return crel_nth crel_if crel_upd) auto
   236 qed
   237 
   238 lemma partition_length_remains:
   239   assumes "crel (partition a l r) h h' rs"
   240   shows "Heap.length a h = Heap.length a h'"
   241 proof -
   242   from assms part_length_remains show ?thesis
   243     unfolding partition.simps swap_def
   244     by (elim crelE crel_return crel_nth crel_if crel_upd) auto
   245 qed
   246 
   247 lemma partition_outer_remains:
   248   assumes "crel (partition a l r) h h' rs"
   249   assumes "l < r"
   250   shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array (a::nat array) h ! i = get_array a h' ! i"
   251 proof -
   252   from assms part_outer_remains part_returns_index_in_bounds show ?thesis
   253     unfolding partition.simps swap_def
   254     by (elim crelE crel_return crel_nth crel_if crel_upd) fastsimp
   255 qed
   256 
   257 lemma partition_returns_index_in_bounds:
   258   assumes crel: "crel (partition a l r) h h' rs"
   259   assumes "l < r"
   260   shows "l \<le> rs \<and> rs \<le> r"
   261 proof -
   262   from crel obtain middle h'' p where part: "crel (part1 a l (r - 1) p) h h'' middle"
   263     and rs_equals: "rs = (if get_array a h'' ! middle \<le> get_array a h ! r then middle + 1
   264          else middle)"
   265     unfolding partition.simps
   266     by (elim crelE crel_return crel_nth crel_if crel_upd) simp
   267   from `l < r` have "l \<le> r - 1" by arith
   268   from part_returns_index_in_bounds[OF part this] rs_equals `l < r` show ?thesis by auto
   269 qed
   270 
   271 lemma partition_partitions:
   272   assumes crel: "crel (partition a l r) h h' rs"
   273   assumes "l < r"
   274   shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> get_array (a::nat array) h' ! i \<le> get_array a h' ! rs) \<and>
   275   (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> get_array a h' ! rs \<le> get_array a h' ! i)"
   276 proof -
   277   let ?pivot = "get_array a h ! r" 
   278   from crel obtain middle h1 where part: "crel (part1 a l (r - 1) ?pivot) h h1 middle"
   279     and swap: "crel (swap a rs r) h1 h' ()"
   280     and rs_equals: "rs = (if get_array a h1 ! middle \<le> ?pivot then middle + 1
   281          else middle)"
   282     unfolding partition.simps
   283     by (elim crelE crel_return crel_nth crel_if crel_upd) simp
   284   from swap have h'_def: "h' = Heap.upd a r (get_array a h1 ! rs)
   285     (Heap.upd a rs (get_array a h1 ! r) h1)"
   286     unfolding swap_def
   287     by (elim crelE crel_return crel_nth crel_upd) simp
   288   from swap have in_bounds: "r < Heap.length a h1 \<and> rs < Heap.length a h1"
   289     unfolding swap_def
   290     by (elim crelE crel_return crel_nth crel_upd) simp
   291   from swap have swap_length_remains: "Heap.length a h1 = Heap.length a h'"
   292     unfolding swap_def by (elim crelE crel_return crel_nth crel_upd) auto
   293   from `l < r` have "l \<le> r - 1" by simp 
   294   note middle_in_bounds = part_returns_index_in_bounds[OF part this]
   295   from part_outer_remains[OF part] `l < r`
   296   have "get_array a h ! r = get_array a h1 ! r"
   297     by fastsimp
   298   with swap
   299   have right_remains: "get_array a h ! r = get_array a h' ! rs"
   300     unfolding swap_def
   301     by (auto simp add: Heap.length_def elim!: crelE crel_return crel_nth crel_upd) (cases "r = rs", auto)
   302   from part_partitions [OF part]
   303   show ?thesis
   304   proof (cases "get_array a h1 ! middle \<le> ?pivot")
   305     case True
   306     with rs_equals have rs_equals: "rs = middle + 1" by simp
   307     { 
   308       fix i
   309       assume i_is_left: "l \<le> i \<and> i < rs"
   310       with swap_length_remains in_bounds middle_in_bounds rs_equals `l < r`
   311       have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
   312       from i_is_left rs_equals have "l \<le> i \<and> i < middle \<or> i = middle" by arith
   313       with part_partitions[OF part] right_remains True
   314       have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
   315       with i_props h'_def in_bounds have "get_array a h' ! i \<le> get_array a h' ! rs"
   316 	unfolding Heap.upd_def Heap.length_def by simp
   317     }
   318     moreover
   319     {
   320       fix i
   321       assume "rs < i \<and> i \<le> r"
   322 
   323       hence "(rs < i \<and> i \<le> r - 1) \<or> (rs < i \<and> i = r)" by arith
   324       hence "get_array a h' ! rs \<le> get_array a h' ! i"
   325       proof
   326 	assume i_is: "rs < i \<and> i \<le> r - 1"
   327 	with swap_length_remains in_bounds middle_in_bounds rs_equals
   328 	have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
   329 	from part_partitions[OF part] rs_equals right_remains i_is
   330 	have "get_array a h' ! rs \<le> get_array a h1 ! i"
   331 	  by fastsimp
   332 	with i_props h'_def show ?thesis by fastsimp
   333       next
   334 	assume i_is: "rs < i \<and> i = r"
   335 	with rs_equals have "Suc middle \<noteq> r" by arith
   336 	with middle_in_bounds `l < r` have "Suc middle \<le> r - 1" by arith
   337 	with part_partitions[OF part] right_remains 
   338 	have "get_array a h' ! rs \<le> get_array a h1 ! (Suc middle)"
   339 	  by fastsimp
   340 	with i_is True rs_equals right_remains h'_def
   341 	show ?thesis using in_bounds
   342 	  unfolding Heap.upd_def Heap.length_def
   343 	  by auto
   344       qed
   345     }
   346     ultimately show ?thesis by auto
   347   next
   348     case False
   349     with rs_equals have rs_equals: "middle = rs" by simp
   350     { 
   351       fix i
   352       assume i_is_left: "l \<le> i \<and> i < rs"
   353       with swap_length_remains in_bounds middle_in_bounds rs_equals
   354       have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
   355       from part_partitions[OF part] rs_equals right_remains i_is_left
   356       have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
   357       with i_props h'_def have "get_array a h' ! i \<le> get_array a h' ! rs"
   358 	unfolding Heap.upd_def by simp
   359     }
   360     moreover
   361     {
   362       fix i
   363       assume "rs < i \<and> i \<le> r"
   364       hence "(rs < i \<and> i \<le> r - 1) \<or> i = r" by arith
   365       hence "get_array a h' ! rs \<le> get_array a h' ! i"
   366       proof
   367 	assume i_is: "rs < i \<and> i \<le> r - 1"
   368 	with swap_length_remains in_bounds middle_in_bounds rs_equals
   369 	have i_props: "i < Heap.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
   370 	from part_partitions[OF part] rs_equals right_remains i_is
   371 	have "get_array a h' ! rs \<le> get_array a h1 ! i"
   372 	  by fastsimp
   373 	with i_props h'_def show ?thesis by fastsimp
   374       next
   375 	assume i_is: "i = r"
   376 	from i_is False rs_equals right_remains h'_def
   377 	show ?thesis using in_bounds
   378 	  unfolding Heap.upd_def Heap.length_def
   379 	  by auto
   380       qed
   381     }
   382     ultimately
   383     show ?thesis by auto
   384   qed
   385 qed
   386 
   387 
   388 function quicksort :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap"
   389 where
   390   "quicksort arr left right =
   391      (if (right > left)  then
   392         do
   393           pivotNewIndex \<leftarrow> partition arr left right;
   394           pivotNewIndex \<leftarrow> assert (\<lambda>x. left \<le> x \<and> x \<le> right) pivotNewIndex;
   395           quicksort arr left (pivotNewIndex - 1);
   396           quicksort arr (pivotNewIndex + 1) right
   397         done
   398      else return ())"
   399 by pat_completeness auto
   400 
   401 (* For termination, we must show that the pivotNewIndex is between left and right *) 
   402 termination
   403 by (relation "measure (\<lambda>(a, l, r). (r - l))") auto
   404 
   405 declare quicksort.simps[simp del]
   406 
   407 
   408 lemma quicksort_permutes:
   409   assumes "crel (quicksort a l r) h h' rs"
   410   shows "multiset_of (get_array a h') 
   411   = multiset_of (get_array a h)"
   412   using assms
   413 proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
   414   case (1 a l r h h' rs)
   415   with partition_permutes show ?case
   416     unfolding quicksort.simps [of a l r]
   417     by (elim crel_if crelE crel_assert crel_return) auto
   418 qed
   419 
   420 lemma length_remains:
   421   assumes "crel (quicksort a l r) h h' rs"
   422   shows "Heap.length a h = Heap.length a h'"
   423 using assms
   424 proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
   425   case (1 a l r h h' rs)
   426   with partition_length_remains show ?case
   427     unfolding quicksort.simps [of a l r]
   428     by (elim crel_if crelE crel_assert crel_return) auto
   429 qed
   430 
   431 lemma quicksort_outer_remains:
   432   assumes "crel (quicksort a l r) h h' rs"
   433    shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array (a::nat array) h ! i = get_array a h' ! i"
   434   using assms
   435 proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
   436   case (1 a l r h h' rs)
   437   note cr = `crel (quicksort a l r) h h' rs`
   438   thus ?case
   439   proof (cases "r > l")
   440     case False
   441     with cr have "h' = h"
   442       unfolding quicksort.simps [of a l r]
   443       by (elim crel_if crel_return) auto
   444     thus ?thesis by simp
   445   next
   446   case True
   447    { 
   448       fix h1 h2 p ret1 ret2 i
   449       assume part: "crel (partition a l r) h h1 p"
   450       assume qs1: "crel (quicksort a l (p - 1)) h1 h2 ret1"
   451       assume qs2: "crel (quicksort a (p + 1) r) h2 h' ret2"
   452       assume pivot: "l \<le> p \<and> p \<le> r"
   453       assume i_outer: "i < l \<or> r < i"
   454       from  partition_outer_remains [OF part True] i_outer
   455       have "get_array a h !i = get_array a h1 ! i" by fastsimp
   456       moreover
   457       with 1(1) [OF True pivot qs1] pivot i_outer
   458       have "get_array a h1 ! i = get_array a h2 ! i" by auto
   459       moreover
   460       with qs2 1(2) [of p h2 h' ret2] True pivot i_outer
   461       have "get_array a h2 ! i = get_array a h' ! i" by auto
   462       ultimately have "get_array a h ! i= get_array a h' ! i" by simp
   463     }
   464     with cr show ?thesis
   465       unfolding quicksort.simps [of a l r]
   466       by (elim crel_if crelE crel_assert crel_return) auto
   467   qed
   468 qed
   469 
   470 lemma quicksort_is_skip:
   471   assumes "crel (quicksort a l r) h h' rs"
   472   shows "r \<le> l \<longrightarrow> h = h'"
   473   using assms
   474   unfolding quicksort.simps [of a l r]
   475   by (elim crel_if crel_return) auto
   476  
   477 lemma quicksort_sorts:
   478   assumes "crel (quicksort a l r) h h' rs"
   479   assumes l_r_length: "l < Heap.length a h" "r < Heap.length a h" 
   480   shows "sorted (subarray l (r + 1) a h')"
   481   using assms
   482 proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
   483   case (1 a l r h h' rs)
   484   note cr = `crel (quicksort a l r) h h' rs`
   485   thus ?case
   486   proof (cases "r > l")
   487     case False
   488     hence "l \<ge> r + 1 \<or> l = r" by arith 
   489     with length_remains[OF cr] 1(5) show ?thesis
   490       by (auto simp add: subarray_Nil subarray_single)
   491   next
   492     case True
   493     { 
   494       fix h1 h2 p
   495       assume part: "crel (partition a l r) h h1 p"
   496       assume qs1: "crel (quicksort a l (p - 1)) h1 h2 ()"
   497       assume qs2: "crel (quicksort a (p + 1) r) h2 h' ()"
   498       from partition_returns_index_in_bounds [OF part True]
   499       have pivot: "l\<le> p \<and> p \<le> r" .
   500      note length_remains = length_remains[OF qs2] length_remains[OF qs1] partition_length_remains[OF part]
   501       from quicksort_outer_remains [OF qs2] quicksort_outer_remains [OF qs1] pivot quicksort_is_skip[OF qs1]
   502       have pivot_unchanged: "get_array a h1 ! p = get_array a h' ! p" by (cases p, auto)
   503         (*-- First of all, by induction hypothesis both sublists are sorted. *)
   504       from 1(1)[OF True pivot qs1] length_remains pivot 1(5) 
   505       have IH1: "sorted (subarray l p a h2)"  by (cases p, auto simp add: subarray_Nil)
   506       from quicksort_outer_remains [OF qs2] length_remains
   507       have left_subarray_remains: "subarray l p a h2 = subarray l p a h'"
   508 	by (simp add: subarray_eq_samelength_iff)
   509       with IH1 have IH1': "sorted (subarray l p a h')" by simp
   510       from 1(2)[OF True pivot qs2] pivot 1(5) length_remains
   511       have IH2: "sorted (subarray (p + 1) (r + 1) a h')"
   512         by (cases "Suc p \<le> r", auto simp add: subarray_Nil)
   513            (* -- Secondly, both sublists remain partitioned. *)
   514       from partition_partitions[OF part True]
   515       have part_conds1: "\<forall>j. j \<in> set (subarray l p a h1) \<longrightarrow> j \<le> get_array a h1 ! p "
   516         and part_conds2: "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h1) \<longrightarrow> get_array a h1 ! p \<le> j"
   517         by (auto simp add: all_in_set_subarray_conv)
   518       from quicksort_outer_remains [OF qs1] quicksort_permutes [OF qs1] True
   519         length_remains 1(5) pivot multiset_of_sublist [of l p "get_array a h1" "get_array a h2"]
   520       have multiset_partconds1: "multiset_of (subarray l p a h2) = multiset_of (subarray l p a h1)"
   521 	unfolding Heap.length_def subarray_def by (cases p, auto)
   522       with left_subarray_remains part_conds1 pivot_unchanged
   523       have part_conds2': "\<forall>j. j \<in> set (subarray l p a h') \<longrightarrow> j \<le> get_array a h' ! p"
   524         by (simp, subst set_of_multiset_of[symmetric], simp)
   525           (* -- These steps are the analogous for the right sublist \<dots> *)
   526       from quicksort_outer_remains [OF qs1] length_remains
   527       have right_subarray_remains: "subarray (p + 1) (r + 1) a h1 = subarray (p + 1) (r + 1) a h2"
   528 	by (auto simp add: subarray_eq_samelength_iff)
   529       from quicksort_outer_remains [OF qs2] quicksort_permutes [OF qs2] True
   530         length_remains 1(5) pivot multiset_of_sublist [of "p + 1" "r + 1" "get_array a h2" "get_array a h'"]
   531       have multiset_partconds2: "multiset_of (subarray (p + 1) (r + 1) a h') = multiset_of (subarray (p + 1) (r + 1) a h2)"
   532         unfolding Heap.length_def subarray_def by auto
   533       with right_subarray_remains part_conds2 pivot_unchanged
   534       have part_conds1': "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h') \<longrightarrow> get_array a h' ! p \<le> j"
   535         by (simp, subst set_of_multiset_of[symmetric], simp)
   536           (* -- Thirdly and finally, we show that the array is sorted
   537           following from the facts above. *)
   538       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'"
   539 	by (simp add: subarray_nth_array_Cons, cases "l < p") (auto simp add: subarray_append subarray_Nil)
   540       with IH1' IH2 part_conds1' part_conds2' pivot have ?thesis
   541 	unfolding subarray_def
   542 	apply (auto simp add: sorted_append sorted_Cons all_in_set_sublist'_conv)
   543 	by (auto simp add: set_sublist' dest: le_trans [of _ "get_array a h' ! p"])
   544     }
   545     with True cr show ?thesis
   546       unfolding quicksort.simps [of a l r]
   547       by (elim crel_if crel_return crelE crel_assert) auto
   548   qed
   549 qed
   550 
   551 
   552 lemma quicksort_is_sort:
   553   assumes crel: "crel (quicksort a 0 (Heap.length a h - 1)) h h' rs"
   554   shows "get_array a h' = sort (get_array a h)"
   555 proof (cases "get_array a h = []")
   556   case True
   557   with quicksort_is_skip[OF crel] show ?thesis
   558   unfolding Heap.length_def by simp
   559 next
   560   case False
   561   from quicksort_sorts [OF crel] False have "sorted (sublist' 0 (List.length (get_array a h)) (get_array a h'))"
   562     unfolding Heap.length_def subarray_def by auto
   563   with length_remains[OF crel] have "sorted (get_array a h')"
   564     unfolding Heap.length_def by simp
   565   with quicksort_permutes [OF crel] properties_for_sort show ?thesis by fastsimp
   566 qed
   567 
   568 subsection {* No Errors in quicksort *}
   569 text {* We have proved that quicksort sorts (if no exceptions occur).
   570 We will now show that exceptions do not occur. *}
   571 
   572 lemma noError_part1: 
   573   assumes "l < Heap.length a h" "r < Heap.length a h"
   574   shows "noError (part1 a l r p) h"
   575   using assms
   576 proof (induct a l r p arbitrary: h rule: part1.induct)
   577   case (1 a l r p)
   578   thus ?case
   579     unfolding part1.simps [of a l r] swap_def
   580     by (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd elim!: crelE crel_upd crel_nth crel_return)
   581 qed
   582 
   583 lemma noError_partition:
   584   assumes "l < r" "l < Heap.length a h" "r < Heap.length a h"
   585   shows "noError (partition a l r) h"
   586 using assms
   587 unfolding partition.simps swap_def
   588 apply (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd noError_part1 elim!: crelE crel_upd crel_nth crel_return)
   589 apply (frule part_length_remains)
   590 apply (frule part_returns_index_in_bounds)
   591 apply auto
   592 apply (frule part_length_remains)
   593 apply (frule part_returns_index_in_bounds)
   594 apply auto
   595 apply (frule part_length_remains)
   596 apply auto
   597 done
   598 
   599 lemma noError_quicksort:
   600   assumes "l < Heap.length a h" "r < Heap.length a h"
   601   shows "noError (quicksort a l r) h"
   602 using assms
   603 proof (induct a l r arbitrary: h rule: quicksort.induct)
   604   case (1 a l ri h)
   605   thus ?case
   606     unfolding quicksort.simps [of a l ri]
   607     apply (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd noError_assert noError_partition)
   608     apply (frule partition_returns_index_in_bounds)
   609     apply auto
   610     apply (frule partition_returns_index_in_bounds)
   611     apply auto
   612     apply (auto elim!: crel_assert dest!: partition_length_remains length_remains)
   613     apply (subgoal_tac "Suc r \<le> ri \<or> r = ri") 
   614     apply (erule disjE)
   615     apply auto
   616     unfolding quicksort.simps [of a "Suc ri" ri]
   617     apply (auto intro!: noError_if noError_return)
   618     done
   619 qed
   620 
   621 
   622 subsection {* Example *}
   623 
   624 definition "qsort a = do
   625     k \<leftarrow> length a;
   626     quicksort a 0 (k - 1);
   627     return a
   628   done"
   629 
   630 ML {* @{code qsort} (Array.fromList [42, 2, 3, 5, 0, 1705, 8, 3, 15]) () *}
   631 
   632 export_code qsort in SML_imp module_name QSort
   633 export_code qsort in OCaml module_name QSort file -
   634 export_code qsort in OCaml_imp module_name QSort file -
   635 export_code qsort in Haskell module_name QSort file -
   636 
   637 end