equal
deleted
inserted
replaced
1 theory ImperativeQuickSort |
1 theory ImperativeQuickSort |
2 imports Imperative_HOL Subarray Multiset |
2 imports Imperative_HOL Subarray Multiset Efficient_Nat |
3 begin |
3 begin |
4 |
4 |
5 text {* We prove QuickSort correct in the Relational Calculus. *} |
5 text {* We prove QuickSort correct in the Relational Calculus. *} |
6 |
6 |
7 |
7 |
617 unfolding quicksort.simps [of a "Suc ri" ri] run_drop |
617 unfolding quicksort.simps [of a "Suc ri" ri] run_drop |
618 apply (auto intro!: noError_if noError_return) |
618 apply (auto intro!: noError_if noError_return) |
619 done |
619 done |
620 qed |
620 qed |
621 |
621 |
|
622 |
|
623 subsection {* Example *} |
|
624 |
|
625 definition "qsort a = do |
|
626 k \<leftarrow> length a; |
|
627 quicksort a 0 (k - 1); |
|
628 return a |
|
629 done" |
|
630 |
|
631 ML {* @{code qsort} (Array.fromList [42, 2, 3, 5, 0, 1705, 8, 3, 15]) () *} |
|
632 |
|
633 export_code qsort in OCaml module_name Arr file - |
|
634 export_code qsort in Haskell module_name Arr file - |
|
635 |
622 end |
636 end |