src/Provers/order.ML
changeset 42364 8c674b3b8e44
parent 42361 23f352990944
child 43278 1fbdcebb364b
--- a/src/Provers/order.ML	Sat Apr 16 16:37:21 2011 +0200
+++ b/src/Provers/order.ML	Sat Apr 16 18:11:20 2011 +0200
@@ -274,8 +274,9 @@
   (* Internal exception, raised if contradiction ( x < x ) was derived *)
 
 fun prove asms =
-  let fun pr (Asm i) = List.nth (asms, i)
-  |       pr (Thm (prfs, thm)) = (map pr prfs) MRS thm
+  let
+    fun pr (Asm i) = nth asms i
+      | pr (Thm (prfs, thm)) = map pr prfs MRS thm;
   in pr end;
 
 (* Internal datatype for inequalities *)
@@ -847,16 +848,17 @@
                val v = upper edge
            in
              if (getIndex u ntc) = xi then
-               (completeTermPath x u (List.nth(sccSubgraphs, xi)) )@[edge]
-               @(completeTermPath v y' (List.nth(sccSubgraphs, getIndex y' ntc)) )
-             else (rev_completeComponentPath u)@[edge]
-                  @(completeTermPath v y' (List.nth(sccSubgraphs, getIndex y' ntc)) )
+               completeTermPath x u (nth sccSubgraphs xi) @ [edge] @
+               completeTermPath v y' (nth sccSubgraphs (getIndex y' ntc))
+             else
+              rev_completeComponentPath u @ [edge] @
+                completeTermPath v y' (nth sccSubgraphs (getIndex y' ntc))
            end
    in
-      if x aconv y then
-        [(Le (x, y, (Thm ([], #le_refl less_thms))))]
-      else ( if xi = yi then completeTermPath x y (List.nth(sccSubgraphs, xi))
-             else rev_completeComponentPath y )
+     if x aconv y then
+       [(Le (x, y, (Thm ([], #le_refl less_thms))))]
+     else if xi = yi then completeTermPath x y (nth sccSubgraphs xi)
+     else rev_completeComponentPath y
    end;
 
 (* ******************************************************************* *)
@@ -1016,15 +1018,18 @@
                 (* if SCC_x is linked to SCC_y via edge e *)
                  else if ui = xi andalso vi = yi then (
                    case e of (Less (_, _,_)) => (
-                        let val xypath = (completeTermPath x u (List.nth(sccSubgraphs, ui)) ) @ [e] @ (completeTermPath v y (List.nth(sccSubgraphs, vi)) )
-                            val xyLesss = transPath (tl xypath, hd xypath)
+                        let
+                          val xypath =
+                            completeTermPath x u (nth sccSubgraphs ui) @ [e] @
+                            completeTermPath v y (nth sccSubgraphs vi)
+                          val xyLesss = transPath (tl xypath, hd xypath)
                         in  (Thm ([getprf xyLesss], #less_imp_neq less_thms)) end)
                    | _ => (
                         let
-                            val xupath = completeTermPath x u  (List.nth(sccSubgraphs, ui))
-                            val uxpath = completeTermPath u x  (List.nth(sccSubgraphs, ui))
-                            val vypath = completeTermPath v y  (List.nth(sccSubgraphs, vi))
-                            val yvpath = completeTermPath y v  (List.nth(sccSubgraphs, vi))
+                            val xupath = completeTermPath x u (nth sccSubgraphs ui)
+                            val uxpath = completeTermPath u x (nth sccSubgraphs ui)
+                            val vypath = completeTermPath v y (nth sccSubgraphs vi)
+                            val yvpath = completeTermPath y v (nth sccSubgraphs vi)
                             val xuLesss = transPath (tl xupath, hd xupath)
                             val uxLesss = transPath (tl uxpath, hd uxpath)
                             val vyLesss = transPath (tl vypath, hd vypath)
@@ -1037,15 +1042,18 @@
                         )
                   ) else if ui = yi andalso vi = xi then (
                      case e of (Less (_, _,_)) => (
-                        let val xypath = (completeTermPath y u (List.nth(sccSubgraphs, ui)) ) @ [e] @ (completeTermPath v x (List.nth(sccSubgraphs, vi)) )
-                            val xyLesss = transPath (tl xypath, hd xypath)
+                        let
+                          val xypath =
+                            completeTermPath y u (nth sccSubgraphs ui) @ [e] @
+                            completeTermPath v x (nth sccSubgraphs vi)
+                          val xyLesss = transPath (tl xypath, hd xypath)
                         in (Thm ([(Thm ([getprf xyLesss], #less_imp_neq less_thms))] , #not_sym less_thms)) end )
                      | _ => (
 
-                        let val yupath = completeTermPath y u (List.nth(sccSubgraphs, ui))
-                            val uypath = completeTermPath u y (List.nth(sccSubgraphs, ui))
-                            val vxpath = completeTermPath v x (List.nth(sccSubgraphs, vi))
-                            val xvpath = completeTermPath x v (List.nth(sccSubgraphs, vi))
+                        let val yupath = completeTermPath y u (nth sccSubgraphs ui)
+                            val uypath = completeTermPath u y (nth sccSubgraphs ui)
+                            val vxpath = completeTermPath v x (nth sccSubgraphs vi)
+                            val xvpath = completeTermPath x v (nth sccSubgraphs vi)
                             val yuLesss = transPath (tl yupath, hd yupath)
                             val uyLesss = transPath (tl uypath, hd uypath)
                             val vxLesss = transPath (tl vxpath, hd vxpath)