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