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