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