--- a/thys2/Sort_ops.thy~	Sat Sep 13 10:07:14 2014 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,65 +0,0 @@
-theory Sort_ops
-imports Main
-begin
-
-ML {*
-local 
-  open Array
-in
-
- fun swap i j a = let val ai = sub(a, i);
-                       val _ = update(a, i, sub(a, j))
-                       val _ = update(a, j, ai)
-                   in
-                        a
-                   end
-
-  fun pre_ops_of a = 
-   getM :|-- (fn (l, r, piv, i, j) => let
-       (* val _ = Output.tracing ("("^string_of_int i^","^string_of_int j^")") *)
-    in
-    if (j < i) then (returnM (swap l j a) |-- returnM [(l, j)])
-    else (if (sub(a, i) <= piv andalso i <= r) then (setM (l, r, piv, i + 1, j)
-                                                        |-- pre_ops_of a)
-          else if (sub(a, j) > piv ) then (setM (l, r, piv, i, j - 1) |-- pre_ops_of a)
-          else (pre_ops_of (swap i j a) :|-- (fn ops => returnM ((i,j)::ops))))
-    end  
-   )
-
-  fun ops_of i j a = 
-     if (j < i) then []
-  else let
-     val piv = sub(a, i)
-     val (ops1, (_, _, _, i', j')) = pre_ops_of a (i, j, piv, i, j) |> normVal
-     val ops2 = ops_of i (j' - 1) a
-     val ops3 = ops_of (j' + 1) j a
-  in
-     ops1 @ ops2 @ ops3 
-  end
-
-  fun rem_sdup [] = []
-    | rem_sdup [c] = [c]
-    | rem_sdup ((i, j)::(i', j')::xs) = if ((i = i' andalso j = j') orelse
-                                            (i = j' andalso j = i')) then rem_sdup (xs)
-                            else (i, j)::rem_sdup ((i', j')::xs)
-  fun sexec [] a = a
-   | sexec ((i, j)::ops) a = sexec ops (swap i j a)
-
-  fun swaps_of (l:int list) = 
-    ops_of 0 (List.length l - 1) (fromList l) |> rem_sdup
-      |> filter (fn (i, j) => i <> j)
-end
-
-*}
-
-text {* Examples *}
-
-ML {*
-  val l = [8, 9, 10, 1, 12, 13, 14] 
-  val ops = (swaps_of l)
-  val a = (sexec ops (Array.fromList l))
-  val l' = Array.vector a
-  val a = sexec (rev ops) a
-*}
-
-end
\ No newline at end of file