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