author wenzelm Sun, 26 Jul 2009 22:28:31 +0200 changeset 32215 87806301a813 parent 32214 6a6827bad05f child 32216 2f3d65d15149
replaced old METAHYPS by FOCUS; eliminated homegrown SUBGOAL combinator -- beware of exception Subscript in body; modernized functor names; minimal tuning of sources; reactivated dead quasi.ML (ever used?);
 src/HOL/Orderings.thy file | annotate | diff | comparison | revisions src/HOL/Transitive_Closure.thy file | annotate | diff | comparison | revisions src/Provers/order.ML file | annotate | diff | comparison | revisions src/Provers/quasi.ML file | annotate | diff | comparison | revisions src/Provers/trancl.ML file | annotate | diff | comparison | revisions
```--- a/src/HOL/Orderings.thy	Sun Jul 26 22:24:13 2009 +0200
+++ b/src/HOL/Orderings.thy	Sun Jul 26 22:28:31 2009 +0200
@@ -6,7 +6,9 @@

theory Orderings
imports HOL
-uses "~~/src/Provers/order.ML"
+uses
+  "~~/src/Provers/order.ML"
+  "~~/src/Provers/quasi.ML"  (* FIXME unused? *)
begin

subsection {* Quasi orders *}
@@ -289,7 +291,7 @@
sig
val print_structures: Proof.context -> unit
val setup: theory -> theory
-  val order_tac: thm list -> Proof.context -> int -> tactic
+  val order_tac: Proof.context -> thm list -> int -> tactic
end;

structure Orders: ORDERS =
@@ -329,7 +331,7 @@

(** Method **)

-fun struct_tac ((s, [eq, le, less]), thms) prems =
+fun struct_tac ((s, [eq, le, less]), thms) ctxt prems =
let
fun decomp thy (@{const Trueprop} \$ t) =
let
@@ -354,13 +356,13 @@
| decomp thy _ = NONE;
in
case s of
-      "order" => Order_Tac.partial_tac decomp thms prems
-    | "linorder" => Order_Tac.linear_tac decomp thms prems
+      "order" => Order_Tac.partial_tac decomp thms ctxt prems
+    | "linorder" => Order_Tac.linear_tac decomp thms ctxt prems
| _ => error ("Unknown kind of order `" ^ s ^ "' encountered in transitivity reasoner.")
end

-fun order_tac prems ctxt =
-  FIRST' (map (fn s => CHANGED o struct_tac s prems) (Data.get (Context.Proof ctxt)));
+fun order_tac ctxt prems =
+  FIRST' (map (fn s => CHANGED o struct_tac s ctxt prems) (Data.get (Context.Proof ctxt)));

(** Attribute **)
@@ -394,7 +396,7 @@
(** Setup **)

val setup =
-  Method.setup @{binding order} (Scan.succeed (SIMPLE_METHOD' o order_tac []))
+  Method.setup @{binding order} (Scan.succeed (fn ctxt => SIMPLE_METHOD' (order_tac ctxt [])))
"transitivity reasoner" #>
attrib_setup;

@@ -532,7 +534,7 @@
Simplifier.simproc thy name raw_ts proc) procs)) thy;
Simplifier.map_simpset (fn ss => ss addSolver
-    mk_solver' name (fn ss => tac (Simplifier.prems_of_ss ss) (Simplifier.the_context ss)));
+    mk_solver' name (fn ss => tac (Simplifier.the_context ss) (Simplifier.prems_of_ss ss)));

in
```--- a/src/HOL/Transitive_Closure.thy	Sun Jul 26 22:24:13 2009 +0200
+++ b/src/HOL/Transitive_Closure.thy	Sun Jul 26 22:28:31 2009 +0200
@@ -811,16 +811,16 @@

ML {*

-structure Trancl_Tac = Trancl_Tac_Fun (
-  struct
-    val r_into_trancl = @{thm trancl.r_into_trancl};
-    val trancl_trans  = @{thm trancl_trans};
-    val rtrancl_refl = @{thm rtrancl.rtrancl_refl};
-    val r_into_rtrancl = @{thm r_into_rtrancl};
-    val trancl_into_rtrancl = @{thm trancl_into_rtrancl};
-    val rtrancl_trancl_trancl = @{thm rtrancl_trancl_trancl};
-    val trancl_rtrancl_trancl = @{thm trancl_rtrancl_trancl};
-    val rtrancl_trans = @{thm rtrancl_trans};
+structure Trancl_Tac = Trancl_Tac
+(
+  val r_into_trancl = @{thm trancl.r_into_trancl};
+  val trancl_trans  = @{thm trancl_trans};
+  val rtrancl_refl = @{thm rtrancl.rtrancl_refl};
+  val r_into_rtrancl = @{thm r_into_rtrancl};
+  val trancl_into_rtrancl = @{thm trancl_into_rtrancl};
+  val rtrancl_trancl_trancl = @{thm rtrancl_trancl_trancl};
+  val trancl_rtrancl_trancl = @{thm trancl_rtrancl_trancl};
+  val rtrancl_trans = @{thm rtrancl_trans};

fun decomp (@{const Trueprop} \$ t) =
let fun dec (Const ("op :", _) \$ (Const ("Pair", _) \$ a \$ b) \$ rel ) =
@@ -832,19 +832,18 @@
| dec _ =  NONE
in dec t end
| decomp _ = NONE;
-
-  end);
+);

-structure Tranclp_Tac = Trancl_Tac_Fun (
-  struct
-    val r_into_trancl = @{thm tranclp.r_into_trancl};
-    val trancl_trans  = @{thm tranclp_trans};
-    val rtrancl_refl = @{thm rtranclp.rtrancl_refl};
-    val r_into_rtrancl = @{thm r_into_rtranclp};
-    val trancl_into_rtrancl = @{thm tranclp_into_rtranclp};
-    val rtrancl_trancl_trancl = @{thm rtranclp_tranclp_tranclp};
-    val trancl_rtrancl_trancl = @{thm tranclp_rtranclp_tranclp};
-    val rtrancl_trans = @{thm rtranclp_trans};
+structure Tranclp_Tac = Trancl_Tac
+(
+  val r_into_trancl = @{thm tranclp.r_into_trancl};
+  val trancl_trans  = @{thm tranclp_trans};
+  val rtrancl_refl = @{thm rtranclp.rtrancl_refl};
+  val r_into_rtrancl = @{thm r_into_rtranclp};
+  val trancl_into_rtrancl = @{thm tranclp_into_rtranclp};
+  val rtrancl_trancl_trancl = @{thm rtranclp_tranclp_tranclp};
+  val trancl_rtrancl_trancl = @{thm tranclp_rtranclp_tranclp};
+  val rtrancl_trans = @{thm rtranclp_trans};

fun decomp (@{const Trueprop} \$ t) =
let fun dec (rel \$ a \$ b) =
@@ -856,31 +855,31 @@
| dec _ =  NONE
in dec t end
| decomp _ = NONE;
-
-  end);
+);
*}

declaration {* fn _ =>
Simplifier.map_ss (fn ss => ss
-    addSolver (mk_solver "Trancl" (fn _ => Trancl_Tac.trancl_tac))
-    addSolver (mk_solver "Rtrancl" (fn _ => Trancl_Tac.rtrancl_tac))
-    addSolver (mk_solver "Tranclp" (fn _ => Tranclp_Tac.trancl_tac))
-    addSolver (mk_solver "Rtranclp" (fn _ => Tranclp_Tac.rtrancl_tac)))
+    addSolver (mk_solver' "Trancl" (Trancl_Tac.trancl_tac o Simplifier.the_context))
+    addSolver (mk_solver' "Rtrancl" (Trancl_Tac.rtrancl_tac o Simplifier.the_context))
+    addSolver (mk_solver' "Tranclp" (Tranclp_Tac.trancl_tac o Simplifier.the_context))
+    addSolver (mk_solver' "Rtranclp" (Tranclp_Tac.rtrancl_tac o Simplifier.the_context)))
*}

-(* Optional methods *)
+
+text {* Optional methods. *}

method_setup trancl =
-  {* Scan.succeed (K (SIMPLE_METHOD' Trancl_Tac.trancl_tac)) *}
+  {* Scan.succeed (SIMPLE_METHOD' o Trancl_Tac.trancl_tac) *}
{* simple transitivity reasoner *}
method_setup rtrancl =
-  {* Scan.succeed (K (SIMPLE_METHOD' Trancl_Tac.rtrancl_tac)) *}
+  {* Scan.succeed (SIMPLE_METHOD' o Trancl_Tac.rtrancl_tac) *}
{* simple transitivity reasoner *}
method_setup tranclp =
-  {* Scan.succeed (K (SIMPLE_METHOD' Tranclp_Tac.trancl_tac)) *}
+  {* Scan.succeed (SIMPLE_METHOD' o Tranclp_Tac.trancl_tac) *}
{* simple transitivity reasoner (predicate version) *}
method_setup rtranclp =
-  {* Scan.succeed (K (SIMPLE_METHOD' Tranclp_Tac.rtrancl_tac)) *}
+  {* Scan.succeed (SIMPLE_METHOD' o Tranclp_Tac.rtrancl_tac) *}
{* simple transitivity reasoner (predicate version) *}

end```
```--- a/src/Provers/order.ML	Sun Jul 26 22:24:13 2009 +0200
+++ b/src/Provers/order.ML	Sun Jul 26 22:28:31 2009 +0200
@@ -35,9 +35,11 @@

(* Tactics *)
val partial_tac:
-    (theory -> term -> (term * string * term) option) -> less_arith -> thm list -> int -> tactic
+    (theory -> term -> (term * string * term) option) -> less_arith ->
+    Proof.context -> thm list -> int -> tactic
val linear_tac:
-    (theory -> term -> (term * string * term) option) -> less_arith -> thm list -> int -> tactic
+    (theory -> term -> (term * string * term) option) -> less_arith ->
+    Proof.context -> thm list -> int -> tactic
end;

structure Order_Tac: ORDER_TAC =
@@ -259,34 +261,28 @@
less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, thm));

-
-(* Extract subgoal with signature *)
-fun SUBGOAL goalfun i st =
-  goalfun (List.nth(prems_of st, i-1),  i, Thm.theory_of_thm st) st
-                             handle Subscript => Seq.empty;
-
(* Internal datatype for the proof *)
datatype proof
-  = Asm of int
-  | Thm of proof list * thm;
-
+  = Asm of int
+  | Thm of proof list * thm;
+
exception Cannot;
(* Internal exception, raised if conclusion cannot be derived from
assumptions. *)
exception Contr of proof;
(* Internal exception, raised if contradiction ( x < x ) was derived *)

-fun prove asms =
+fun prove asms =
let fun pr (Asm i) = List.nth (asms, i)
|       pr (Thm (prfs, thm)) = (map pr prfs) MRS thm
in pr end;

(* Internal datatype for inequalities *)
-datatype less
-   = Less  of term * term * proof
+datatype less
+   = Less  of term * term * proof
| Le    of term * term * proof
-   | NotEq of term * term * proof;
-
+   | NotEq of term * term * proof;
+
(* Misc functions for datatype less *)
fun lower (Less (x, _, _)) = x
| lower (Le (x, _, _)) = x
@@ -314,17 +310,17 @@
fun mkasm_partial decomp (less_thms : less_arith) sign (t, n) =
case decomp sign t of
SOME (x, rel, y) => (case rel of
-      "<"   => if (x aconv y) then raise Contr (Thm ([Asm n], #less_reflE less_thms))
+      "<"   => if (x aconv y) then raise Contr (Thm ([Asm n], #less_reflE less_thms))
else [Less (x, y, Asm n)]
| "~<"  => []
| "<="  => [Le (x, y, Asm n)]
-    | "~<=" => []
+    | "~<=" => []
| "="   => [Le (x, y, Thm ([Asm n], #eqD1 less_thms)),
Le (y, x, Thm ([Asm n], #eqD2 less_thms))]
-    | "~="  => if (x aconv y) then
+    | "~="  => if (x aconv y) then
raise Contr (Thm ([(Thm ([(Thm ([], #le_refl less_thms)) ,(Asm n)], #le_neq_trans less_thms))], #less_reflE less_thms))
else [ NotEq (x, y, Asm n),
-                      NotEq (y, x,Thm ( [Asm n], #not_sym less_thms))]
+                      NotEq (y, x,Thm ( [Asm n], #not_sym less_thms))]
| _     => error ("partial_tac: unknown relation symbol ``" ^ rel ^
"''returned by decomp."))
| NONE => [];
@@ -338,23 +334,23 @@
(* Linear orders only.                                                      *)
(*                                                                          *)
(* ************************************************************************ *)
-
+
fun mkasm_linear decomp (less_thms : less_arith) sign (t, n) =
case decomp sign t of
SOME (x, rel, y) => (case rel of
-      "<"   => if (x aconv y) then raise Contr (Thm ([Asm n], #less_reflE less_thms))
+      "<"   => if (x aconv y) then raise Contr (Thm ([Asm n], #less_reflE less_thms))
else [Less (x, y, Asm n)]
| "~<"  => [Le (y, x, Thm ([Asm n], #not_lessD less_thms))]
| "<="  => [Le (x, y, Asm n)]
-    | "~<=" => if (x aconv y) then
-                  raise (Contr (Thm ([Thm ([Asm n], #not_leD less_thms)], #less_reflE less_thms)))
-               else [Less (y, x, Thm ([Asm n], #not_leD less_thms))]
+    | "~<=" => if (x aconv y) then
+                  raise (Contr (Thm ([Thm ([Asm n], #not_leD less_thms)], #less_reflE less_thms)))
+               else [Less (y, x, Thm ([Asm n], #not_leD less_thms))]
| "="   => [Le (x, y, Thm ([Asm n], #eqD1 less_thms)),
Le (y, x, Thm ([Asm n], #eqD2 less_thms))]
-    | "~="  => if (x aconv y) then
+    | "~="  => if (x aconv y) then
raise Contr (Thm ([(Thm ([(Thm ([], #le_refl less_thms)) ,(Asm n)], #le_neq_trans less_thms))], #less_reflE less_thms))
else [ NotEq (x, y, Asm n),
-                      NotEq (y, x,Thm ( [Asm n], #not_sym less_thms))]
+                      NotEq (y, x,Thm ( [Asm n], #not_sym less_thms))]
| _     => error ("linear_tac: unknown relation symbol ``" ^ rel ^
"''returned by decomp."))
| NONE => [];
@@ -409,7 +405,7 @@
where Rel is one of "<", "<=", "~<", "~<=", "=" and "~=",
other relation symbols cause an error message *)

-fun gen_order_tac mkasm mkconcl decomp' (less_thms : less_arith) prems =
+fun gen_order_tac mkasm mkconcl decomp' (less_thms : less_arith) ctxt prems =

let

@@ -440,19 +436,19 @@
|   mergeLess (Le (x, _, p) , Less (_ , z, q)) =
Less (x, z, Thm ([p,q] , #le_less_trans less_thms))
|   mergeLess (Le (x, z, p) , NotEq (x', z', q)) =
-      if (x aconv x' andalso z aconv z' )
+      if (x aconv x' andalso z aconv z' )
then Less (x, z, Thm ([p,q] , #le_neq_trans less_thms))
else error "linear/partial_tac: internal error le_neq_trans"
|   mergeLess (NotEq (x, z, p) , Le (x' , z', q)) =
-      if (x aconv x' andalso z aconv z')
+      if (x aconv x' andalso z aconv z')
then Less (x, z, Thm ([p,q] , #neq_le_trans less_thms))
else error "linear/partial_tac: internal error neq_le_trans"
|   mergeLess (NotEq (x, z, p) , Less (x' , z', q)) =
-      if (x aconv x' andalso z aconv z')
+      if (x aconv x' andalso z aconv z')
then Less ((x' , z', q))
else error "linear/partial_tac: internal error neq_less_trans"
|   mergeLess (Less (x, z, p) , NotEq (x', z', q)) =
-      if (x aconv x' andalso z aconv z')
+      if (x aconv x' andalso z aconv z')
then Less (x, z, p)
else error "linear/partial_tac: internal error less_neq_trans"
|   mergeLess (Le (x, _, p) , Le (_ , z, q)) =
@@ -471,8 +467,8 @@
| (Less (_, y, _)) tr (Less (x', _, _)) = ( y aconv x' )
| (Le (_, y, _))   tr (Le (x', _, _))   = ( y aconv x' )
| _ tr _ = false;
-
-
+
+
(* ******************************************************************* *)
(*                                                                     *)
(* transPath (Lesslist, Less): (less list * less) -> less              *)
@@ -488,7 +484,7 @@
|   transPath (x::xs,lesss) =
if lesss tr x then transPath (xs, mergeLess(lesss,x))
else error "linear/partial_tac: internal error transpath";
-
+
(* ******************************************************************* *)
(*                                                                     *)
(* less1 subsumes less2 : less -> less -> bool                         *)
@@ -496,7 +492,7 @@
(* subsumes checks whether less1 implies less2                         *)
(*                                                                     *)
(* ******************************************************************* *)
-
+
infix subsumes;
fun (Less (x, y, _)) subsumes (Le (x', y', _)) =
(x aconv x' andalso y aconv y')
@@ -554,7 +550,7 @@
(*                                                                     *)
(* ******************************************************************* *)

-
+
(* *********************************************************** *)
(* Functions for constructing graphs                           *)
(* *********************************************************** *)
@@ -562,27 +558,27 @@
|   addEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el)
-
+
(* ********************************************************************* *)
(*                                                                       *)
-(* mkGraphs constructs from a list of objects of type less a graph g,    *)
+(* mkGraphs constructs from a list of objects of type less a graph g,    *)
(* by taking all edges that are candidate for a <=, and a list neqE, by  *)
(* taking all edges that are candiate for a ~=                           *)
(*                                                                       *)
(* ********************************************************************* *)

fun mkGraphs [] = ([],[],[])
-|   mkGraphs lessList =
+|   mkGraphs lessList =
let

fun buildGraphs ([],leqG,neqG,neqE) = (leqG, neqG, neqE)
-|   buildGraphs (l::ls, leqG,neqG, neqE) = case l of
-  (Less (x,y,p)) =>
-       buildGraphs (ls, addEdge (x,[(y,(Less (x, y, p)))],leqG) ,
-                        addEdge (x,[(y,(Less (x, y, p)))],neqG), l::neqE)
+|   buildGraphs (l::ls, leqG,neqG, neqE) = case l of
+  (Less (x,y,p)) =>
+       buildGraphs (ls, addEdge (x,[(y,(Less (x, y, p)))],leqG) ,
+                        addEdge (x,[(y,(Less (x, y, p)))],neqG), l::neqE)
| (Le (x,y,p)) =>
-      buildGraphs (ls, addEdge (x,[(y,(Le (x, y,p)))],leqG) , neqG, neqE)
-| (NotEq  (x,y,p)) =>
+      buildGraphs (ls, addEdge (x,[(y,(Le (x, y,p)))],leqG) , neqG, neqE)
+| (NotEq  (x,y,p)) =>
buildGraphs (ls, leqG , addEdge (x,[(y,(NotEq (x, y, p)))],neqG), l::neqE) ;

in buildGraphs (lessList, [], [], []) end;
@@ -595,12 +591,12 @@
(* List of successors of u in graph g                                      *)
(*                                                                         *)
(* *********************************************************************** *)
-
+
-|   adjacent _  []  _ = []
-
-
+|   adjacent _  []  _ = []
+
+
(* *********************************************************************** *)
(*                                                                         *)
(* transpose g:                                                            *)
@@ -616,7 +612,7 @@
(* Compute list of reversed edges for each adjacency list *)
fun flip (u,(v,l)::el) = (v,(u,l)) :: flip (u,el)
| flip (_,nil) = nil
-
+
(* Compute adjacency list for node u from the list of edges
and return a likewise reduced list of edges.  The list of edges
is searches for edges starting from u, and these edges are removed. *)
@@ -640,19 +636,19 @@
(* Compute, for each adjacency list, the list with reversed edges,
and concatenate these lists. *)
val flipped = List.foldr (op @) nil (map flip g)
-
- in assemble g flipped end
-
+
+ in assemble g flipped end
+
(* *********************************************************************** *)
-(*                                                                         *)
+(*                                                                         *)
(* scc_term : (term * term list) list -> term list list                    *)
(*                                                                         *)
(* The following is based on the algorithm for finding strongly connected  *)
(* components described in Introduction to Algorithms, by Cormon, Leiserson*)
(* and Rivest, section 23.5. The input G is an adjacency list description  *)
(* of a directed graph. The output is a list of the strongly connected     *)
-(* components (each a list of vertices).                                   *)
-(*                                                                         *)
+(* components (each a list of vertices).                                   *)
+(*                                                                         *)
(*                                                                         *)
(* *********************************************************************** *)

@@ -664,11 +660,11 @@

(* List of vertices which have been visited. *)
val visited : term list ref = ref nil
-
+
fun been_visited v = exists (fn w => w aconv v) (!visited)
-
+
(* Given the adjacency list rep of a graph (a list of pairs),
-     return just the first element of each pair, yielding the
+     return just the first element of each pair, yielding the
vertex list. *)
val members = map (fn (v,_) => v)

@@ -701,7 +697,7 @@
dfs_visit along with u form a connected component. We
collect all the connected components together in a
list, which is what is returned. *)
-  Library.foldl (fn (comps,u) =>
+  Library.foldl (fn (comps,u) =>
if been_visited u then comps
else ((u :: dfs_visit (transpose (op aconv) G) u) :: comps))  (nil,(!finish))
end;
@@ -710,17 +706,17 @@
(* *********************************************************************** *)
(*                                                                         *)
(* dfs_int_reachable g u:                                                  *)
-(* (int * int list) list -> int -> int list                                *)
+(* (int * int list) list -> int -> int list                                *)
(*                                                                         *)
(* Computes list of all nodes reachable from u in g.                       *)
(*                                                                         *)
(* *********************************************************************** *)

-fun dfs_int_reachable g u =
+fun dfs_int_reachable g u =
let
(* List of vertices which have been visited. *)
val visited : int list ref = ref nil
-
+
fun been_visited v = exists (fn w => w = v) (!visited)

fun dfs_visit g u : int list =
@@ -731,59 +727,59 @@
else v :: dfs_visit g v @ ds)
nil (adjacent (op =) g u)
in  descendents end
-
+
in u :: dfs_visit g u end;

-
-fun indexComps components =
+
+fun indexComps components =
ListPair.map (fn (a,b) => (a,b)) (0 upto (length components -1), components);

-fun indexNodes IndexComp =
+fun indexNodes IndexComp =
List.concat (map (fn (index, comp) => (map (fn v => (v,index)) comp)) IndexComp);
-
+
fun getIndex v [] = ~1
-|   getIndex v ((v',k)::vs) = if v aconv v' then k else getIndex v vs;
-
+|   getIndex v ((v',k)::vs) = if v aconv v' then k else getIndex v vs;
+

(* *********************************************************************** *)
(*                                                                         *)
(* dfs eq_comp g u v:                                                       *)
(* ('a * 'a -> bool) -> ('a  *( 'a * less) list) list ->                   *)
-(* 'a -> 'a -> (bool * ('a * less) list)                                   *)
+(* 'a -> 'a -> (bool * ('a * less) list)                                   *)
(*                                                                         *)
(* Depth first search of v from u.                                         *)
(* Returns (true, path(u, v)) if successful, otherwise (false, []).        *)
(*                                                                         *)
(* *********************************************************************** *)

-fun dfs eq_comp g u v =
- let
+fun dfs eq_comp g u v =
+ let
val pred = ref nil;
val visited = ref nil;
-
+
fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
-
-    fun dfs_visit u' =
+
+    fun dfs_visit u' =
let val _ = visited := u' :: (!visited)
-
+
fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end;
-
-    in if been_visited v then ()
+
+    in if been_visited v then ()
else (app (fn (v',l) => if been_visited v' then () else (
-       update (v',l);
+       update (v',l);
dfs_visit v'; ()) )) (adjacent eq_comp g u')
end
-  in
-    dfs_visit u;
-    if (been_visited v) then (true, (!pred)) else (false , [])
+  in
+    dfs_visit u;
+    if (been_visited v) then (true, (!pred)) else (false , [])
end;

-
+
(* *********************************************************************** *)
(*                                                                         *)
(* completeTermPath u v g:                                                 *)
-(* Term.term -> Term.term -> (Term.term * (Term.term * less) list) list    *)
+(* Term.term -> Term.term -> (Term.term * (Term.term * less) list) list    *)
(* -> less list                                                            *)
(*                                                                         *)
(* Complete the path from u to v in graph g.  Path search is performed     *)
@@ -793,36 +789,36 @@
(*                                                                         *)
(* *********************************************************************** *)

-
-fun completeTermPath u v g  =
-  let
+
+fun completeTermPath u v g  =
+  let
val (found, tmp) =  dfs (op aconv) g u v ;
val pred = map snd tmp;
-
+
fun path x y  =
let
-
+
(* find predecessor u of node v and the edge u -> v *)

fun lookup v [] = raise Cannot
|   lookup v (e::es) = if (upper e) aconv v then e else lookup v es;

-      (* traverse path backwards and return list of visited edges *)
-      fun rev_path v =
+      (* traverse path backwards and return list of visited edges *)
+      fun rev_path v =
let val l = lookup v pred
val u = lower l;
in
if u aconv x then [l]
-        else (rev_path u) @ [l]
+        else (rev_path u) @ [l]
end
in rev_path y end;
-
-  in
+
+  in
if found then (if u aconv v then [(Le (u, v, (Thm ([], #le_refl less_thms))))]
else path u v ) else raise Cannot
-end;
+end;

-
+
(* *********************************************************************** *)
(*                                                                         *)
(* findProof (sccGraph, neqE, ntc, sccSubgraphs) subgoal:                  *)
@@ -834,133 +830,133 @@
(* proof for subgoal.  Raises exception Cannot if this is not possible.    *)
(*                                                                         *)
(* *********************************************************************** *)
-
+
fun findProof (sccGraph, neqE, ntc, sccSubgraphs) subgoal =
let
-
+
(* complete path x y from component graph *)
- fun completeComponentPath x y predlist =
-   let
-	  val xi = getIndex x ntc
-	  val yi = getIndex y ntc
-
-	  fun lookup k [] =  raise Cannot
-	  |   lookup k ((h: int,l)::us) = if k = h then l else lookup k us;
-
-	  fun rev_completeComponentPath y' =
-	   let val edge = lookup (getIndex y' ntc) predlist
-	       val u = lower edge
-	       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)) )
+ fun completeComponentPath x y predlist =
+   let
+          val xi = getIndex x ntc
+          val yi = getIndex y ntc
+
+          fun lookup k [] =  raise Cannot
+          |   lookup k ((h: int,l)::us) = if k = h then l else lookup k us;
+
+          fun rev_completeComponentPath y' =
+           let val edge = lookup (getIndex y' ntc) predlist
+               val u = lower edge
+               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)) )
end
-   in
-      if x aconv y then
+   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 )
+             else rev_completeComponentPath y )
end;

-(* ******************************************************************* *)
+(* ******************************************************************* *)
(* findLess e x y xi yi xreachable yreachable                          *)
(*                                                                     *)
(* Find a path from x through e to y, of weight <                      *)
-(* ******************************************************************* *)
-
- fun findLess e x y xi yi xreachable yreachable =
-  let val u = lower e
+(* ******************************************************************* *)
+
+ fun findLess e x y xi yi xreachable yreachable =
+  let val u = lower e
val v = upper e
val ui = getIndex u ntc
val vi = getIndex v ntc
-
-  in
-      if ui mem xreachable andalso vi mem xreachable andalso
+
+  in
+      if ui mem xreachable andalso vi mem xreachable andalso
ui mem yreachable andalso vi mem yreachable then (
-
-  (case e of (Less (_, _, _)) =>
+
+  (case e of (Less (_, _, _)) =>
let
val (xufound, xupred) =  dfs (op =) sccGraph xi (getIndex u ntc)
-	    in
-	     if xufound then (
-	      let
-	       val (vyfound, vypred) =  dfs (op =) sccGraph (getIndex v ntc) yi
-	      in
-	       if vyfound then (
-	        let
-	         val xypath = (completeComponentPath x u xupred)@[e]@(completeComponentPath v y vypred)
-	         val xyLesss = transPath (tl xypath, hd xypath)
-	        in
-		 if xyLesss subsumes subgoal then SOME (getprf xyLesss)
+            in
+             if xufound then (
+              let
+               val (vyfound, vypred) =  dfs (op =) sccGraph (getIndex v ntc) yi
+              in
+               if vyfound then (
+                let
+                 val xypath = (completeComponentPath x u xupred)@[e]@(completeComponentPath v y vypred)
+                 val xyLesss = transPath (tl xypath, hd xypath)
+                in
+                 if xyLesss subsumes subgoal then SOME (getprf xyLesss)
else NONE
-	       end)
-	       else NONE
-	      end)
-	     else NONE
-	    end
-       |  _   =>
-         let val (uvfound, uvpred) =  dfs (op =) sccGraph (getIndex u ntc) (getIndex v ntc)
-             in
-	      if uvfound then (
-	       let
-	        val (xufound, xupred) = dfs (op =) sccGraph xi (getIndex u ntc)
-	       in
-		if xufound then (
-		 let
-		  val (vyfound, vypred) =  dfs (op =) sccGraph (getIndex v ntc) yi
-		 in
-		  if vyfound then (
-		   let
-		    val uvpath = completeComponentPath u v uvpred
-		    val uvLesss = mergeLess ( transPath (tl uvpath, hd uvpath), e)
-		    val xypath = (completeComponentPath  x u xupred)@[uvLesss]@(completeComponentPath v y vypred)
-		    val xyLesss = transPath (tl xypath, hd xypath)
-		   in
-		    if xyLesss subsumes subgoal then SOME (getprf xyLesss)
+               end)
+               else NONE
+              end)
+             else NONE
+            end
+       |  _   =>
+         let val (uvfound, uvpred) =  dfs (op =) sccGraph (getIndex u ntc) (getIndex v ntc)
+             in
+              if uvfound then (
+               let
+                val (xufound, xupred) = dfs (op =) sccGraph xi (getIndex u ntc)
+               in
+                if xufound then (
+                 let
+                  val (vyfound, vypred) =  dfs (op =) sccGraph (getIndex v ntc) yi
+                 in
+                  if vyfound then (
+                   let
+                    val uvpath = completeComponentPath u v uvpred
+                    val uvLesss = mergeLess ( transPath (tl uvpath, hd uvpath), e)
+                    val xypath = (completeComponentPath  x u xupred)@[uvLesss]@(completeComponentPath v y vypred)
+                    val xyLesss = transPath (tl xypath, hd xypath)
+                   in
+                    if xyLesss subsumes subgoal then SOME (getprf xyLesss)
else NONE
-		   end )
-		  else NONE
-	         end)
-		else NONE
-	       end )
-	      else NONE
-	     end )
+                   end )
+                  else NONE
+                 end)
+                else NONE
+               end )
+              else NONE
+             end )
) else NONE
-end;
-
-
+end;
+
+
in
(* looking for x <= y: any path from x to y is sufficient *)
case subgoal of (Le (x, y, _)) => (
-  if null sccGraph then raise Cannot else (
-   let
+  if null sccGraph then raise Cannot else (
+   let
val xi = getIndex x ntc
val yi = getIndex y ntc
(* searches in sccGraph a path from xi to yi *)
val (found, pred) = dfs (op =) sccGraph xi yi
-   in
+   in
if found then (
-       let val xypath = completeComponentPath x y pred
-           val xyLesss = transPath (tl xypath, hd xypath)
-       in
-	  (case xyLesss of
-	    (Less (_, _, q)) => if xyLesss subsumes subgoal then (Thm ([q], #less_imp_le less_thms))
-				else raise Cannot
-	     | _   => if xyLesss subsumes subgoal then (getprf xyLesss)
-	              else raise Cannot)
+       let val xypath = completeComponentPath x y pred
+           val xyLesss = transPath (tl xypath, hd xypath)
+       in
+          (case xyLesss of
+            (Less (_, _, q)) => if xyLesss subsumes subgoal then (Thm ([q], #less_imp_le less_thms))
+                                else raise Cannot
+             | _   => if xyLesss subsumes subgoal then (getprf xyLesss)
+                      else raise Cannot)
end )
-     else raise Cannot
-   end
+     else raise Cannot
+   end
)
)
(* looking for x < y: particular path required, which is not necessarily
found by normal dfs *)
|   (Less (x, y, _)) => (
if null sccGraph then raise Cannot else (
-   let
+   let
val xi = getIndex x ntc
val yi = getIndex y ntc
val sccGraph_transpose = transpose (op =) sccGraph
@@ -969,13 +965,13 @@
(* all comonents reachable from y in the transposed graph sccGraph' *)
val yreachable = dfs_int_reachable sccGraph_transpose yi
(* for all edges u ~= v or u < v check if they are part of path x < y *)
-    fun processNeqEdges [] = raise Cannot
-    |   processNeqEdges (e::es) =
-      case  (findLess e x y xi yi xreachable yreachable) of (SOME prf) => prf
+    fun processNeqEdges [] = raise Cannot
+    |   processNeqEdges (e::es) =
+      case  (findLess e x y xi yi xreachable yreachable) of (SOME prf) => prf
| _ => processNeqEdges es
-
-    in
-       processNeqEdges neqE
+
+    in
+       processNeqEdges neqE
end
)
)
@@ -986,99 +982,99 @@
else if null sccSubgraphs then (
(case (Library.find_first (fn fact => fact subsumes subgoal) neqE, subgoal) of
( SOME (NotEq (x, y, p)), NotEq (x', y', _)) =>
-          if  (x aconv x' andalso y aconv y') then p
-	  else Thm ([p], #not_sym less_thms)
-     | ( SOME (Less (x, y, p)), NotEq (x', y', _)) =>
+          if  (x aconv x' andalso y aconv y') then p
+          else Thm ([p], #not_sym less_thms)
+     | ( SOME (Less (x, y, p)), NotEq (x', y', _)) =>
if x aconv x' andalso y aconv y' then (Thm ([p], #less_imp_neq less_thms))
else (Thm ([(Thm ([p], #less_imp_neq less_thms))], #not_sym less_thms))
-     | _ => raise Cannot)
+     | _ => raise Cannot)
) else (
-
-   let  val xi = getIndex x ntc
+
+   let  val xi = getIndex x ntc
val yi = getIndex y ntc
-	val sccGraph_transpose = transpose (op =) sccGraph
+        val sccGraph_transpose = transpose (op =) sccGraph
val xreachable = dfs_int_reachable sccGraph xi
-	val yreachable = dfs_int_reachable sccGraph_transpose yi
-
-	fun processNeqEdges [] = raise Cannot
-  	|   processNeqEdges (e::es) = (
-	    let val u = lower e
-	        val v = upper e
-		val ui = getIndex u ntc
-		val vi = getIndex v ntc
-
-	    in
-	        (* if x ~= y follows from edge e *)
-	    	if e subsumes subgoal then (
-		     case e of (Less (u, v, q)) => (
-		       if u aconv x andalso v aconv y then (Thm ([q], #less_imp_neq less_thms))
-		       else (Thm ([(Thm ([q], #less_imp_neq less_thms))], #not_sym less_thms))
-		     )
-		     |    (NotEq (u,v, q)) => (
-		       if u aconv x andalso v aconv y then q
-		       else (Thm ([q],  #not_sym less_thms))
-		     )
-		 )
+        val yreachable = dfs_int_reachable sccGraph_transpose yi
+
+        fun processNeqEdges [] = raise Cannot
+        |   processNeqEdges (e::es) = (
+            let val u = lower e
+                val v = upper e
+                val ui = getIndex u ntc
+                val vi = getIndex v ntc
+
+            in
+                (* if x ~= y follows from edge e *)
+                if e subsumes subgoal then (
+                     case e of (Less (u, v, q)) => (
+                       if u aconv x andalso v aconv y then (Thm ([q], #less_imp_neq less_thms))
+                       else (Thm ([(Thm ([q], #less_imp_neq less_thms))], #not_sym less_thms))
+                     )
+                     |    (NotEq (u,v, q)) => (
+                       if u aconv x andalso v aconv y then q
+                       else (Thm ([q],  #not_sym less_thms))
+                     )
+                 )
(* if SCC_x is linked to SCC_y via edge e *)
-		 else if ui = xi andalso vi = yi then (
+                 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)
-			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 xuLesss = transPath (tl xupath, hd xupath)
-			    val uxLesss = transPath (tl uxpath, hd uxpath)
-			    val vyLesss = transPath (tl vypath, hd vypath)
-			    val yvLesss = transPath (tl yvpath, hd yvpath)
-			    val x_eq_u =  (Thm ([(getprf xuLesss),(getprf uxLesss)], #eqI less_thms))
-			    val v_eq_y =  (Thm ([(getprf vyLesss),(getprf yvLesss)], #eqI less_thms))
-			in
-                           (Thm ([x_eq_u , (getprf e), v_eq_y ], #eq_neq_eq_imp_neq less_thms))
-			end
-			)
-		  ) 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)
-			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))
-			    val yuLesss = transPath (tl yupath, hd yupath)
-			    val uyLesss = transPath (tl uypath, hd uypath)
-			    val vxLesss = transPath (tl vxpath, hd vxpath)
-			    val xvLesss = transPath (tl xvpath, hd xvpath)
-			    val y_eq_u =  (Thm ([(getprf yuLesss),(getprf uyLesss)], #eqI less_thms))
-			    val v_eq_x =  (Thm ([(getprf vxLesss),(getprf xvLesss)], #eqI less_thms))
-			in
-			    (Thm ([(Thm ([y_eq_u , (getprf e), v_eq_x ], #eq_neq_eq_imp_neq less_thms))], #not_sym less_thms))
-		        end
-		       )
-		  ) else (
+                        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)
+                        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 xuLesss = transPath (tl xupath, hd xupath)
+                            val uxLesss = transPath (tl uxpath, hd uxpath)
+                            val vyLesss = transPath (tl vypath, hd vypath)
+                            val yvLesss = transPath (tl yvpath, hd yvpath)
+                            val x_eq_u =  (Thm ([(getprf xuLesss),(getprf uxLesss)], #eqI less_thms))
+                            val v_eq_y =  (Thm ([(getprf vyLesss),(getprf yvLesss)], #eqI less_thms))
+                        in
+                           (Thm ([x_eq_u , (getprf e), v_eq_y ], #eq_neq_eq_imp_neq less_thms))
+                        end
+                        )
+                  ) 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)
+                        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))
+                            val yuLesss = transPath (tl yupath, hd yupath)
+                            val uyLesss = transPath (tl uypath, hd uypath)
+                            val vxLesss = transPath (tl vxpath, hd vxpath)
+                            val xvLesss = transPath (tl xvpath, hd xvpath)
+                            val y_eq_u =  (Thm ([(getprf yuLesss),(getprf uyLesss)], #eqI less_thms))
+                            val v_eq_x =  (Thm ([(getprf vxLesss),(getprf xvLesss)], #eqI less_thms))
+                        in
+                            (Thm ([(Thm ([y_eq_u , (getprf e), v_eq_x ], #eq_neq_eq_imp_neq less_thms))], #not_sym less_thms))
+                        end
+                       )
+                  ) else (
(* there exists a path x < y or y < x such that
x ~= y may be concluded *)
-	        	case  (findLess e x y xi yi xreachable yreachable) of
-		              (SOME prf) =>  (Thm ([prf], #less_imp_neq less_thms))
+                        case  (findLess e x y xi yi xreachable yreachable) of
+                              (SOME prf) =>  (Thm ([prf], #less_imp_neq less_thms))
| NONE =>  (
-		               let
-		                val yr = dfs_int_reachable sccGraph yi
-	                        val xr = dfs_int_reachable sccGraph_transpose xi
-		               in
-		                case  (findLess e y x yi xi yr xr) of
-		                      (SOME prf) => (Thm ([(Thm ([prf], #less_imp_neq less_thms))], #not_sym less_thms))
+                               let
+                                val yr = dfs_int_reachable sccGraph yi
+                                val xr = dfs_int_reachable sccGraph_transpose xi
+                               in
+                                case  (findLess e y x yi xi yr xr) of
+                                      (SOME prf) => (Thm ([(Thm ([prf], #less_imp_neq less_thms))], #not_sym less_thms))
| _ => processNeqEdges es
-		               end)
-		 ) end)
+                               end)
+                 ) end)
in processNeqEdges neqE end)
-  )
+  )
end;

@@ -1110,115 +1106,115 @@
(* ******************************************************************* *)

fun mk_sccGraphs _ [] _ _ = ([],[])
-|   mk_sccGraphs components leqG neqG ntc =
+|   mk_sccGraphs components leqG neqG ntc =
let
(* Liste (Index der Komponente, Komponente *)
val IndexComp = indexComps components;

-
-    fun handleContr edge g =
-       (case edge of
+
+    fun handleContr edge g =
+       (case edge of
(Less  (x, y, _)) => (
-	    let
-	     val xxpath = edge :: (completeTermPath y x g )
-	     val xxLesss = transPath (tl xxpath, hd xxpath)
-	     val q = getprf xxLesss
-	    in
-	     raise (Contr (Thm ([q], #less_reflE less_thms )))
-	    end
-	  )
+            let
+             val xxpath = edge :: (completeTermPath y x g )
+             val xxLesss = transPath (tl xxpath, hd xxpath)
+             val q = getprf xxLesss
+            in
+             raise (Contr (Thm ([q], #less_reflE less_thms )))
+            end
+          )
| (NotEq (x, y, _)) => (
-	    let
-	     val xypath = (completeTermPath x y g )
-	     val yxpath = (completeTermPath y x g )
-	     val xyLesss = transPath (tl xypath, hd xypath)
-	     val yxLesss = transPath (tl yxpath, hd yxpath)
-             val q = getprf (mergeLess ((mergeLess (edge, xyLesss)),yxLesss ))
-	    in
-	     raise (Contr (Thm ([q], #less_reflE less_thms )))
-	    end
-	 )
-	| _ =>  error "trans_tac/handleContr: invalid Contradiction");
-
-
-    (* k is index of the actual component *)
-
-    fun processComponent (k, comp) =
-     let
-        (* all edges with weight <= of the actual component *)
+            let
+             val xypath = (completeTermPath x y g )
+             val yxpath = (completeTermPath y x g )
+             val xyLesss = transPath (tl xypath, hd xypath)
+             val yxLesss = transPath (tl yxpath, hd yxpath)
+             val q = getprf (mergeLess ((mergeLess (edge, xyLesss)),yxLesss ))
+            in
+             raise (Contr (Thm ([q], #less_reflE less_thms )))
+            end
+         )
+        | _ =>  error "trans_tac/handleContr: invalid Contradiction");
+
+
+    (* k is index of the actual component *)
+
+    fun processComponent (k, comp) =
+     let
+        (* all edges with weight <= of the actual component *)
val leqEdges = List.concat (map (adjacent (op aconv) leqG) comp);
-        (* all edges with weight ~= of the actual component *)
+        (* all edges with weight ~= of the actual component *)
val neqEdges = map snd (List.concat (map (adjacent (op aconv) neqG) comp));

fun findContr [] = NONE
-       |   findContr (e::es) =
-		    let val ui = (getIndex (lower e) ntc)
-			val vi = (getIndex (upper e) ntc)
-		    in
-		        if ui = vi then  SOME e
-		        else findContr es
-		    end;
-
-		(* sort edges into component internal edges and
-		   edges pointing away from the component *)
-		fun sortEdges  [] (intern,extern)  = (intern,extern)
-		|   sortEdges  ((v,l)::es) (intern, extern) =
-		    let val k' = getIndex v ntc in
-		        if k' = k then
-			    sortEdges es (l::intern, extern)
-			else sortEdges  es (intern, (k',l)::extern) end;
-
-		(* Insert edge into sorted list of edges, where edge is
+       |   findContr (e::es) =
+                    let val ui = (getIndex (lower e) ntc)
+                        val vi = (getIndex (upper e) ntc)
+                    in
+                        if ui = vi then  SOME e
+                        else findContr es
+                    end;
+
+                (* sort edges into component internal edges and
+                   edges pointing away from the component *)
+                fun sortEdges  [] (intern,extern)  = (intern,extern)
+                |   sortEdges  ((v,l)::es) (intern, extern) =
+                    let val k' = getIndex v ntc in
+                        if k' = k then
+                            sortEdges es (l::intern, extern)
+                        else sortEdges  es (intern, (k',l)::extern) end;
+
+                (* Insert edge into sorted list of edges, where edge is
- it is found for the first time
- it is a <= edge and no parallel < edge was found earlier
- it is a < edge
*)
-          	 fun insert (h: int,l) [] = [(h,l)]
-		 |   insert (h,l) ((k',l')::es) = if h = k' then (
-		     case l of (Less (_, _, _)) => (h,l)::es
-		     | _  => (case l' of (Less (_, _, _)) => (h,l')::es
-	                      | _ => (k',l)::es) )
-		     else (k',l'):: insert (h,l) es;
-
-		(* Reorganise list of edges such that
+                 fun insert (h: int,l) [] = [(h,l)]
+                 |   insert (h,l) ((k',l')::es) = if h = k' then (
+                     case l of (Less (_, _, _)) => (h,l)::es
+                     | _  => (case l' of (Less (_, _, _)) => (h,l')::es
+                              | _ => (k',l)::es) )
+                     else (k',l'):: insert (h,l) es;
+
+                (* Reorganise list of edges such that
- duplicate edges are removed
- if a < edge and a <= edge exist at the same time,
remove <= edge *)
-    		 fun reOrganizeEdges [] sorted = sorted: (int * less) list
-		 |   reOrganizeEdges (e::es) sorted = reOrganizeEdges es (insert e sorted);
-
+                 fun reOrganizeEdges [] sorted = sorted: (int * less) list
+                 |   reOrganizeEdges (e::es) sorted = reOrganizeEdges es (insert e sorted);
+
(* construct the subgraph forming the strongly connected component
-		    from the edge list *)
-		 fun sccSubGraph [] g  = g
-		 |   sccSubGraph (l::ls) g =
-		          sccSubGraph ls (addEdge ((lower l),[((upper l),l)],g))
-
-		 val (intern, extern) = sortEdges leqEdges ([], []);
+                    from the edge list *)
+                 fun sccSubGraph [] g  = g
+                 |   sccSubGraph (l::ls) g =
+                          sccSubGraph ls (addEdge ((lower l),[((upper l),l)],g))
+
+                 val (intern, extern) = sortEdges leqEdges ([], []);
val subGraph = sccSubGraph intern [];
-
-     in
+
+     in
case findContr neqEdges of SOME e => handleContr e subGraph
-	 | _ => ((k, (reOrganizeEdges (extern) [])), subGraph)
-     end;
-
-    val tmp =  map processComponent IndexComp
-in
-     ( (map fst tmp), (map snd tmp))
-end;
+         | _ => ((k, (reOrganizeEdges (extern) [])), subGraph)
+     end;
+
+    val tmp =  map processComponent IndexComp
+in
+     ( (map fst tmp), (map snd tmp))
+end;

(** Find proof if possible. **)

fun gen_solve mkconcl sign (asms, concl) =
- let
+ let
val (leqG, neqG, neqE) = mkGraphs asms
-  val components = scc_term leqG
+  val components = scc_term leqG
val ntc = indexNodes (indexComps components)
val (sccGraph, sccSubgraphs) = mk_sccGraphs components leqG neqG ntc
in
-   let
+   let
val (subgoals, prf) = mkconcl decomp less_thms sign concl
fun solve facts less =
(case triv_solv less of NONE => findProof (sccGraph, neqE, ntc, sccSubgraphs) less
@@ -1229,24 +1225,25 @@
end;

in
-
-    SUBGOAL (fn (A, n, sign) =>
-     let
-      val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A))
-      val Hs = map prop_of prems @ map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
-      val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
-      val lesss = List.concat (ListPair.map (mkasm decomp less_thms sign) (Hs, 0 upto (length Hs - 1)))
-      val prfs = gen_solve mkconcl sign (lesss, C);
-      val (subgoals, prf) = mkconcl decomp less_thms sign C;
-     in
-      METAHYPS (fn asms =>
-	let val thms = map (prove (prems @ asms)) prfs
-	in rtac (prove thms prf) 1 end) n
-     end
-     handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n
-	  | Cannot  => no_tac
-	  )
-
+ SUBGOAL (fn (A, n) => fn st =>
+  let
+   val thy = ProofContext.theory_of ctxt;
+   val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A));
+   val Hs = map prop_of prems @ map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
+   val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
+   val lesss = List.concat (ListPair.map (mkasm decomp less_thms thy) (Hs, 0 upto (length Hs - 1)))
+   val prfs = gen_solve mkconcl thy (lesss, C);
+   val (subgoals, prf) = mkconcl decomp less_thms thy C;
+  in
+   FOCUS (fn {prems = asms, ...} =>
+     let val thms = map (prove (prems @ asms)) prfs
+     in rtac (prove thms prf) 1 end) ctxt n st
+  end
+  handle Contr p =>
+      (FOCUS (fn {prems = asms, ...} => rtac (prove asms p) 1) ctxt n st
+        handle Subscript => Seq.empty)
+   | Cannot => Seq.empty
+   | Subscript => Seq.empty)
end;

(* partial_tac - solves partial orders *)
@@ -1255,5 +1252,4 @@
(* linear_tac - solves linear/total orders *)
val linear_tac = gen_order_tac mkasm_linear mkconcl_linear;

-
end;```
```--- a/src/Provers/quasi.ML	Sun Jul 26 22:24:13 2009 +0200
+++ b/src/Provers/quasi.ML	Sun Jul 26 22:28:31 2009 +0200
@@ -3,10 +3,10 @@
Reasoner for simple transitivity and quasi orders.
*)

-(*
-
+(*
+
The package provides tactics trans_tac and quasi_tac that use
-premises of the form
+premises of the form

t = u, t ~= u, t < u and t <= u

@@ -29,15 +29,15 @@
the assumptions.
Note that the presence of a strict relation is not necessary for
quasi_tac.  Configure decomp_quasi to ignore < and ~=.  A list of
-   required theorems for both situations is given below.
+   required theorems for both situations is given below.
*)

signature LESS_ARITH =
sig
(* Transitivity of <=
-     Note that transitivities for < hold for partial orders only. *)
+     Note that transitivities for < hold for partial orders only. *)
val le_trans: thm  (* [| x <= y; y <= z |] ==> x <= z *)
-
+
(* Additional theorem for quasi orders *)
val le_refl: thm  (* x <= x *)
val eqD1: thm (* x = y ==> x <= y *)
@@ -64,41 +64,36 @@
val decomp_quasi: theory -> term -> (term * string * term) option
end;

-signature QUASI_TAC =
+signature QUASI_TAC =
sig
-  val trans_tac: int -> tactic
-  val quasi_tac: int -> tactic
+  val trans_tac: Proof.context -> int -> tactic
+  val quasi_tac: Proof.context -> int -> tactic
end;

-functor Quasi_Tac_Fun (Less: LESS_ARITH): QUASI_TAC =
+functor Quasi_Tac(Less: LESS_ARITH): QUASI_TAC =
struct

-(* Extract subgoal with signature *)
-fun SUBGOAL goalfun i st =
-  goalfun (List.nth(prems_of st, i-1),  i, Thm.theory_of_thm st) st
-                             handle Subscript => Seq.empty;
-
(* Internal datatype for the proof *)
datatype proof
-  = Asm of int
-  | Thm of proof list * thm;
-
+  = Asm of int
+  | Thm of proof list * thm;
+
exception Cannot;
(* Internal exception, raised if conclusion cannot be derived from
assumptions. *)
exception Contr of proof;
(* Internal exception, raised if contradiction ( x < x ) was derived *)

-fun prove asms =
+fun prove asms =
let fun pr (Asm i) = List.nth (asms, i)
|       pr (Thm (prfs, thm)) = (map pr prfs) MRS thm
in pr end;

(* Internal datatype for inequalities *)
-datatype less
-   = Less  of term * term * proof
+datatype less
+   = Less  of term * term * proof
| Le    of term * term * proof
-   | NotEq of term * term * proof;
+   | NotEq of term * term * proof;

(* Misc functions for datatype less *)
fun lower (Less (x, _, _)) = x
@@ -125,13 +120,13 @@

fun mkasm_trans sign (t, n) =
case Less.decomp_trans sign t of
-    SOME (x, rel, y) =>
+    SOME (x, rel, y) =>
(case rel of
"<="  =>  [Le (x, y, Asm n)]
| _     => error ("trans_tac: unknown relation symbol ``" ^ rel ^
"''returned by decomp_trans."))
| NONE => [];
-
+
(* ************************************************************************ *)
(*                                                                          *)
(* mkasm_quasi sign (t, n) : theory -> (Term.term * int) -> less            *)
@@ -145,15 +140,15 @@
fun mkasm_quasi sign (t, n) =
case Less.decomp_quasi sign t of
SOME (x, rel, y) => (case rel of
-      "<"   => if (x aconv y) then raise Contr (Thm ([Asm n], Less.less_reflE))
+      "<"   => if (x aconv y) then raise Contr (Thm ([Asm n], Less.less_reflE))
else [Less (x, y, Asm n)]
| "<="  => [Le (x, y, Asm n)]
| "="   => [Le (x, y, Thm ([Asm n], Less.eqD1)),
Le (y, x, Thm ([Asm n], Less.eqD2))]
-    | "~="  => if (x aconv y) then
+    | "~="  => if (x aconv y) then
raise Contr (Thm ([(Thm ([(Thm ([], Less.le_refl)) ,(Asm n)], Less.le_neq_trans))], Less.less_reflE))
else [ NotEq (x, y, Asm n),
-                      NotEq (y, x,Thm ( [Asm n], thm "not_sym"))]
+                      NotEq (y, x,Thm ( [Asm n], thm "not_sym"))]
| _     => error ("quasi_tac: unknown relation symbol ``" ^ rel ^
"''returned by decomp_quasi."))
| NONE => [];
@@ -168,15 +163,15 @@
(*                                                                          *)
(* ************************************************************************ *)

-
+
fun mkconcl_trans sign t =
case Less.decomp_trans sign t of
SOME (x, rel, y) => (case rel of
-     "<="  => (Le (x, y, Asm ~1), Asm 0)
+     "<="  => (Le (x, y, Asm ~1), Asm 0)
| _  => raise Cannot)
| NONE => raise Cannot;
-
-
+
+
(* ************************************************************************ *)
(*                                                                          *)
(* mkconcl_quasi sign t : theory -> Term.term -> less                       *)
@@ -194,8 +189,8 @@
| "~="  => ([NotEq (x,y, Asm ~1)], Asm 0)
| _  => raise Cannot)
| NONE => raise Cannot;
-
-
+
+
(* ******************************************************************* *)
(*                                                                     *)
(* mergeLess (less1,less2):  less * less -> less                       *)
@@ -211,11 +206,11 @@
fun mergeLess (Le (x, _, p) , Le (_ , z, q)) =
Le (x, z, Thm ([p,q] , Less.le_trans))
|   mergeLess (Le (x, z, p) , NotEq (x', z', q)) =
-      if (x aconv x' andalso z aconv z' )
+      if (x aconv x' andalso z aconv z' )
then Less (x, z, Thm ([p,q] , Less.le_neq_trans))
else error "quasi_tac: internal error le_neq_trans"
|   mergeLess (NotEq (x, z, p) , Le (x' , z', q)) =
-      if (x aconv x' andalso z aconv z')
+      if (x aconv x' andalso z aconv z')
then Less (x, z, Thm ([p,q] , Less.neq_le_trans))
else error "quasi_tac: internal error neq_le_trans"
|   mergeLess (_, _) =
@@ -229,7 +224,7 @@
infix tr;
fun (Le (_, y, _))   tr (Le (x', _, _))   = ( y aconv x' )
| _ tr _ = false;
-
+
(* ******************************************************************* *)
(*                                                                     *)
(* transPath (Lesslist, Less): (less list * less) -> less              *)
@@ -245,7 +240,7 @@
|   transPath (x::xs,lesss) =
if lesss tr x then transPath (xs, mergeLess(lesss,x))
else error "trans/quasi_tac: internal error transpath";
-
+
(* ******************************************************************* *)
(*                                                                     *)
(* less1 subsumes less2 : less -> less -> bool                         *)
@@ -253,7 +248,7 @@
(* subsumes checks whether less1 implies less2                         *)
(*                                                                     *)
(* ******************************************************************* *)
-
+
infix subsumes;
fun (Le (x, y, _)) subsumes (Le (x', y', _)) =
(x aconv x' andalso y aconv y')
@@ -271,7 +266,7 @@
(* ******************************************************************* *)

fun triv_solv (Le (x, x', _)) =
-    if x aconv x' then  SOME (Thm ([], Less.le_refl))
+    if x aconv x' then  SOME (Thm ([], Less.le_refl))
else NONE
|   triv_solv _ = NONE;

@@ -286,33 +281,33 @@
|   addEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el)
-
+
(* ********************************************************************** *)
(*                                                                        *)
-(* mkQuasiGraph constructs from a list of objects of type less a graph g, *)
+(* mkQuasiGraph constructs from a list of objects of type less a graph g, *)
(* by taking all edges that are candidate for a <=, and a list neqE, by   *)
(* taking all edges that are candiate for a ~=                            *)
(*                                                                        *)
(* ********************************************************************** *)

fun mkQuasiGraph [] = ([],[])
-|   mkQuasiGraph lessList =
+|   mkQuasiGraph lessList =
let
fun buildGraphs ([],leG, neqE) = (leG,  neqE)
-  |   buildGraphs (l::ls, leG,  neqE) = case l of
+  |   buildGraphs (l::ls, leG,  neqE) = case l of
(Less (x,y,p)) =>
-         let
-	  val leEdge  = Le (x,y, Thm ([p], Less.less_imp_le))
-	  val neqEdges = [ NotEq (x,y, Thm ([p], Less.less_imp_neq)),
-	                   NotEq (y,x, Thm ( [Thm ([p], Less.less_imp_neq)], thm "not_sym"))]
-	 in
-	 end
+         let
+          val leEdge  = Le (x,y, Thm ([p], Less.less_imp_le))
+          val neqEdges = [ NotEq (x,y, Thm ([p], Less.less_imp_neq)),
+                           NotEq (y,x, Thm ( [Thm ([p], Less.less_imp_neq)], thm "not_sym"))]
+         in
+         end
| _ =>  buildGraphs (ls, leG,  l::neqE) ;

in buildGraphs (lessList, [],  []) end;
-
+
(* ********************************************************************** *)
(*                                                                        *)
(* mkGraph constructs from a list of objects of type less a graph g       *)
@@ -321,11 +316,11 @@
(* ********************************************************************** *)

fun mkGraph [] = []
-|   mkGraph lessList =
+|   mkGraph lessList =
let
fun buildGraph ([],g) = g
-  |   buildGraph (l::ls, g) =  buildGraph (ls, (addEdge ((lower l),[((upper l),l)],g)))
-
+  |   buildGraph (l::ls, g) =  buildGraph (ls, (addEdge ((lower l),[((upper l),l)],g)))
+
in buildGraph (lessList, []) end;

(* *********************************************************************** *)
@@ -335,42 +330,42 @@
(* List of successors of u in graph g                                      *)
(*                                                                         *)
(* *********************************************************************** *)
-
+
-|   adjacent _  []  _ = []
+|   adjacent _  []  _ = []

(* *********************************************************************** *)
(*                                                                         *)
(* dfs eq_comp g u v:                                                      *)
(* ('a * 'a -> bool) -> ('a  *( 'a * less) list) list ->                   *)
-(* 'a -> 'a -> (bool * ('a * less) list)                                   *)
+(* 'a -> 'a -> (bool * ('a * less) list)                                   *)
(*                                                                         *)
(* Depth first search of v from u.                                         *)
(* Returns (true, path(u, v)) if successful, otherwise (false, []).        *)
(*                                                                         *)
(* *********************************************************************** *)

-fun dfs eq_comp g u v =
- let
+fun dfs eq_comp g u v =
+ let
val pred = ref nil;
val visited = ref nil;
-
+
fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
-
-    fun dfs_visit u' =
+
+    fun dfs_visit u' =
let val _ = visited := u' :: (!visited)
-
+
fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end;
-
-    in if been_visited v then ()
+
+    in if been_visited v then ()
else (app (fn (v',l) => if been_visited v' then () else (
-       update (v',l);
+       update (v',l);
dfs_visit v'; ()) )) (adjacent eq_comp g u')
end
-  in
-    dfs_visit u;
-    if (been_visited v) then (true, (!pred)) else (false , [])
+  in
+    dfs_visit u;
+    if (been_visited v) then (true, (!pred)) else (false , [])
end;

(* ************************************************************************ *)
@@ -393,8 +388,8 @@
(* ************************************************************************ *)

- fun findPath x y g =
-  let
+ fun findPath x y g =
+  let
val (found, tmp) =  dfs (op aconv) g x y ;
val pred = map snd tmp;

@@ -403,38 +398,38 @@
(* find predecessor u of node v and the edge u -> v *)
fun lookup v [] = raise Cannot
|   lookup v (e::es) = if (upper e) aconv v then e else lookup v es;
-
-       (* traverse path backwards and return list of visited edges *)
-       fun rev_path v =
- 	let val l = lookup v pred
+
+       (* traverse path backwards and return list of visited edges *)
+       fun rev_path v =
+        let val l = lookup v pred
val u = lower l;
- 	in
-           if u aconv x then [l] else (rev_path u) @ [l]
-	end
+        in
+           if u aconv x then [l] else (rev_path u) @ [l]
+        end
in rev_path y end;
-
-  in
+
+  in
if found then (
if x aconv y then (found,[(Le (x, y, (Thm ([], Less.le_refl))))])
-    else (found, (path x y) ))
+    else (found, (path x y) ))
else (found,[])
-  end;
-
-
-(* ************************************************************************ *)
+  end;
+
+
+(* ************************************************************************ *)
(*                                                                          *)
(* findQuasiProof (leqG, neqE) subgoal:                                     *)
(* (Term.term * (Term.term * less list) list) * less list  -> less -> proof *)
(*                                                                          *)
(* Constructs a proof for subgoal by searching a special path in leqG and   *)
-(* neqE. Raises Cannot if construction of the proof fails.                  *)
+(* neqE. Raises Cannot if construction of the proof fails.                  *)
(*                                                                          *)
-(* ************************************************************************ *)
+(* ************************************************************************ *)

(* As the conlusion can be either of form x <= y, x < y or x ~= y we have        *)
(* three cases to deal with. Finding a transitivity path from x to y with label  *)
-(* 1. <=                                                                         *)
+(* 1. <=                                                                         *)
(*    This is simply done by searching any path from x to y in the graph leG.    *)
(*    The graph leG contains only edges with label <=.                           *)
(*                                                                               *)
@@ -450,54 +445,54 @@

fun findQuasiProof (leG, neqE) subgoal =
case subgoal of (Le (x,y, _)) => (
-   let
-    val (xyLefound,xyLePath) = findPath x y leG
+   let
+    val (xyLefound,xyLePath) = findPath x y leG
in
if xyLefound then (
-     let
+     let
val Le_x_y = (transPath (tl xyLePath, hd xyLePath))
in getprf Le_x_y end )
else raise Cannot
end )
| (Less (x,y,_))  => (
-   let
+   let
fun findParallelNeq []  = NONE
|   findParallelNeq (e::es)  =
if      (x aconv (lower e) andalso y aconv (upper e)) then SOME e
else if (y aconv (lower e) andalso x aconv (upper e)) then SOME (NotEq (x,y, (Thm ([getprf e], thm "not_sym"))))
-     else findParallelNeq es ;
+     else findParallelNeq es ;
in
(* test if there is a edge x ~= y respectivly  y ~= x and     *)
(* if it possible to find a path x <= y in leG, thus we can conclude x < y *)
-    (case findParallelNeq neqE of (SOME e) =>
-      let
-       val (xyLeFound,xyLePath) = findPath x y leG
+    (case findParallelNeq neqE of (SOME e) =>
+      let
+       val (xyLeFound,xyLePath) = findPath x y leG
in
if xyLeFound then (
-        let
+        let
val Le_x_y = (transPath (tl xyLePath, hd xyLePath))
val Less_x_y = mergeLess (e, Le_x_y)
in getprf Less_x_y end
) else raise Cannot
-      end
-    | _ => raise Cannot)
+      end
+    | _ => raise Cannot)
end )
- | (NotEq (x,y,_)) =>
+ | (NotEq (x,y,_)) =>
(* First check if a single premiss is sufficient *)
(case (Library.find_first (fn fact => fact subsumes subgoal) neqE, subgoal) of
(SOME (NotEq (x, y, p)), NotEq (x', y', _)) =>
-      if  (x aconv x' andalso y aconv y') then p
+      if  (x aconv x' andalso y aconv y') then p
else Thm ([p], thm "not_sym")
-    | _  => raise Cannot
+    | _  => raise Cannot
)

-
-(* ************************************************************************ *)
-(*                                                                          *)
-(* End: Quasi Order relevant functions                                      *)
-(*                                                                          *)
-(*                                                                          *)
-(* ************************************************************************ *)
+
+(* ************************************************************************ *)
+(*                                                                          *)
+(* End: Quasi Order relevant functions                                      *)
+(*                                                                          *)
+(*                                                                          *)
+(* ************************************************************************ *)

(* *********************************************************************** *)
(*                                                                         *)
@@ -509,14 +504,14 @@
(* *********************************************************************** *)

fun solveLeTrans sign (asms, concl) =
- let
+ let
val g = mkGraph asms
in
-   let
+   let
val (subgoal, prf) = mkconcl_trans sign concl
-    val (found, path) = findPath (lower subgoal) (upper subgoal) g
+    val (found, path) = findPath (lower subgoal) (upper subgoal) g
in
-    if found then [getprf (transPath (tl path, hd path))]
+    if found then [getprf (transPath (tl path, hd path))]
else raise Cannot
end
end;
@@ -532,10 +527,10 @@
(* *********************************************************************** *)

fun solveQuasiOrder sign (asms, concl) =
- let
+ let
val (leG, neqE) = mkQuasiGraph asms
in
-   let
+   let
val (subgoals, prf) = mkconcl_quasi sign concl
fun solve facts less =
(case triv_solv less of NONE => findQuasiProof (leG, neqE) less
@@ -543,54 +538,56 @@
in   map (solve asms) subgoals end
end;

-(* ************************************************************************ *)
-(*                                                                          *)
+(* ************************************************************************ *)
+(*                                                                          *)
(* Tactics                                                                  *)
(*                                                                          *)
-(*  - trans_tac                                                          *)
-(*  - quasi_tac, solves quasi orders                                        *)
-(* ************************************************************************ *)
+(*  - trans_tac                                                          *)
+(*  - quasi_tac, solves quasi orders                                        *)
+(* ************************************************************************ *)

(* trans_tac - solves transitivity chains over <= *)
-val trans_tac  =  SUBGOAL (fn (A, n, sign) =>
+
+fun trans_tac ctxt = SUBGOAL (fn (A, n) =>
let
-  val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A))
-  val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
-  val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
-  val lesss = List.concat (ListPair.map (mkasm_trans  sign) (Hs, 0 upto (length Hs - 1)))
-  val prfs = solveLeTrans  sign (lesss, C);
-
-  val (subgoal, prf) = mkconcl_trans  sign C;
+  val thy = ProofContext.theory_of ctxt;
+  val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A));
+  val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A);
+  val C = subst_bounds (rfrees, Logic.strip_assums_concl A);
+  val lesss = List.concat (ListPair.map (mkasm_trans thy) (Hs, 0 upto (length Hs - 1)));
+  val prfs = solveLeTrans thy (lesss, C);
+
+  val (subgoal, prf) = mkconcl_trans thy C;
in
-
-  METAHYPS (fn asms =>
-    let val thms = map (prove asms) prfs
-    in rtac (prove thms prf) 1 end) n
-
+  FOCUS (fn {prems, ...} =>
+    let val thms = map (prove prems) prfs
+    in rtac (prove thms prf) 1 end) ctxt n
end
- handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n
-      | Cannot  => no_tac
-);
+ handle Contr p => FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n
+  | Cannot  => no_tac);
+

(* quasi_tac - solves quasi orders *)
-val quasi_tac = SUBGOAL (fn (A, n, sign) =>
+
+fun quasi_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
let
-  val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A))
-  val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
-  val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
-  val lesss = List.concat (ListPair.map (mkasm_quasi sign) (Hs, 0 upto (length Hs - 1)))
-  val prfs = solveQuasiOrder sign (lesss, C);
-  val (subgoals, prf) = mkconcl_quasi sign C;
+  val thy = ProofContext.theory_of ctxt;
+  val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A));
+  val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A);
+  val C = subst_bounds (rfrees, Logic.strip_assums_concl A);
+  val lesss = flat (ListPair.map (mkasm_quasi thy) (Hs, 0 upto (length Hs - 1)));
+  val prfs = solveQuasiOrder thy (lesss, C);
+  val (subgoals, prf) = mkconcl_quasi thy C;
in
-
-  METAHYPS (fn asms =>
-    let val thms = map (prove asms) prfs
-    in rtac (prove thms prf) 1 end) n
-
+  FOCUS (fn {prems, ...} =>
+    let val thms = map (prove prems) prfs
+    in rtac (prove thms prf) 1 end) ctxt n st
end
- handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n
-      | Cannot  => no_tac
-);
-
+ handle Contr p =>
+    (FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n st
+      handle Subscript => Seq.empty)
+  | Cannot => Seq.empty
+  | Subscript => Seq.empty);
+
end;```
```--- a/src/Provers/trancl.ML	Sun Jul 26 22:24:13 2009 +0200
+++ b/src/Provers/trancl.ML	Sun Jul 26 22:28:31 2009 +0200
@@ -26,7 +26,7 @@

*)

-signature TRANCL_ARITH =
+signature TRANCL_ARITH =
sig

(* theorems for transitive closure *)
@@ -63,25 +63,25 @@
"r":   the relation itself,
"r^+": transitive closure of the relation,
"r^*": reflexive-transitive closure of the relation
-  *)
+  *)

-  val decomp: term ->  (term * term * term * string) option
+  val decomp: term ->  (term * term * term * string) option

end;

-signature TRANCL_TAC =
+signature TRANCL_TAC =
sig
-  val trancl_tac: int -> tactic;
-  val rtrancl_tac: int -> tactic;
+  val trancl_tac: Proof.context -> int -> tactic
+  val rtrancl_tac: Proof.context -> int -> tactic
end;

-functor Trancl_Tac_Fun (Cls : TRANCL_ARITH): TRANCL_TAC =
+functor Trancl_Tac(Cls: TRANCL_ARITH): TRANCL_TAC =
struct

-
+
datatype proof
-  = Asm of int
-  | Thm of proof list * thm;
+  = Asm of int
+  | Thm of proof list * thm;

exception Cannot; (* internal exception: raised if no proof can be found *)

@@ -89,7 +89,7 @@
(Envir.beta_eta_contract x, Envir.beta_eta_contract y,
Envir.beta_eta_contract rel, r)) (Cls.decomp t);

-fun prove thy r asms =
+fun prove thy r asms =
let
fun inst thm =
let val SOME (_, _, r', _) = decomp (concl_of thm)
@@ -98,12 +98,12 @@
| pr (Thm (prfs, thm)) = map pr prfs MRS inst thm
in pr end;

-
+
(* Internal datatype for inequalities *)
-datatype rel
+datatype rel
= Trans  of term * term * proof  (* R^+ *)
| RTrans of term * term * proof; (* R^* *)
-
+
(* Misc functions for datatype rel *)
fun lower (Trans (x, _, _)) = x
| lower (RTrans (x,_,_)) = x;
@@ -112,8 +112,8 @@
| upper (RTrans (_,y,_)) = y;

fun getprf   (Trans   (_, _, p)) = p
-|   getprf   (RTrans (_,_, p)) = p;
-
+|   getprf   (RTrans (_,_, p)) = p;
+
(* ************************************************************************ *)
(*                                                                          *)
(*  mkasm_trancl Rel (t,n): term -> (term , int) -> rel list                *)
@@ -127,16 +127,16 @@

fun mkasm_trancl  Rel  (t, n) =
case decomp t of
-    SOME (x, y, rel,r) => if rel aconv Rel then
-
+    SOME (x, y, rel,r) => if rel aconv Rel then
+
(case r of
"r"   => [Trans (x,y, Thm([Asm n], Cls.r_into_trancl))]
| "r+"  => [Trans (x,y, Asm n)]
| "r*"  => []
| _     => error ("trancl_tac: unknown relation symbol"))
-    else []
+    else []
| NONE => [];
-
+
(* ************************************************************************ *)
(*                                                                          *)
(*  mkasm_rtrancl Rel (t,n): term -> (term , int) -> rel list               *)
@@ -156,7 +156,7 @@
| "r+"  => [ Trans (x,y, Asm n)]
| "r*"  => [ RTrans(x,y, Asm n)]
| _     => error ("rtrancl_tac: unknown relation symbol" ))
-   else []
+   else []
| NONE => [];

(* ************************************************************************ *)
@@ -204,7 +204,7 @@
fun makeStep (Trans (a,_,p), Trans(_,c,q))  = Trans (a,c, Thm ([p,q], Cls.trancl_trans))
(* refl. + trans. cls. rules *)
|   makeStep (RTrans (a,_,p), Trans(_,c,q))  = Trans (a,c, Thm ([p,q], Cls.rtrancl_trancl_trancl))
-|   makeStep (Trans (a,_,p), RTrans(_,c,q))  = Trans (a,c, Thm ([p,q], Cls.trancl_rtrancl_trancl))
+|   makeStep (Trans (a,_,p), RTrans(_,c,q))  = Trans (a,c, Thm ([p,q], Cls.trancl_rtrancl_trancl))
|   makeStep (RTrans (a,_,p), RTrans(_,c,q))  = RTrans (a,c, Thm ([p,q], Cls.rtrancl_trans));

(* ******************************************************************* *)
@@ -220,7 +220,7 @@

fun transPath ([],acc) = acc
|   transPath (x::xs,acc) = transPath (xs, makeStep(acc,x))
-
+
(* ********************************************************************* *)
(* Graph functions                                                       *)
(* ********************************************************************* *)
@@ -232,7 +232,7 @@
|   addEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el)
-
+
(* ********************************************************************** *)
(*                                                                        *)
(* mkGraph constructs from a list of objects of type rel  a graph g       *)
@@ -241,13 +241,13 @@
(* ********************************************************************** *)

fun mkGraph [] = ([],[])
-|   mkGraph ys =
+|   mkGraph ys =
let
fun buildGraph ([],g,zs) = (g,zs)
-  |   buildGraph (x::xs, g, zs) =
-        case x of (Trans (_,_,_)) =>
-	| _ => buildGraph (xs, addEdge((upper x), [],(addEdge ((lower x),[((upper x),x)],g))), zs)
+  |   buildGraph (x::xs, g, zs) =
+        case x of (Trans (_,_,_)) =>
+        | _ => buildGraph (xs, addEdge((upper x), [],(addEdge ((lower x),[((upper x),x)],g))), zs)
in buildGraph (ys, [], []) end;

(* *********************************************************************** *)
@@ -257,42 +257,42 @@
(* List of successors of u in graph g                                      *)
(*                                                                         *)
(* *********************************************************************** *)
-
+
-|   adjacent _  []  _ = []
+|   adjacent _  []  _ = []

(* *********************************************************************** *)
(*                                                                         *)
(* dfs eq_comp g u v:                                                      *)
(* ('a * 'a -> bool) -> ('a  *( 'a * rel) list) list ->                    *)
-(* 'a -> 'a -> (bool * ('a * rel) list)                                    *)
+(* 'a -> 'a -> (bool * ('a * rel) list)                                    *)
(*                                                                         *)
(* Depth first search of v from u.                                         *)
(* Returns (true, path(u, v)) if successful, otherwise (false, []).        *)
(*                                                                         *)
(* *********************************************************************** *)

-fun dfs eq_comp g u v =
- let
+fun dfs eq_comp g u v =
+ let
val pred = ref nil;
val visited = ref nil;
-
+
fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
-
-    fun dfs_visit u' =
+
+    fun dfs_visit u' =
let val _ = visited := u' :: (!visited)
-
+
fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end;
-
-    in if been_visited v then ()
+
+    in if been_visited v then ()
else (app (fn (v',l) => if been_visited v' then () else (
-       update (v',l);
+       update (v',l);
dfs_visit v'; ()) )) (adjacent eq_comp g u')
end
-  in
-    dfs_visit u;
-    if (been_visited v) then (true, (!pred)) else (false , [])
+  in
+    dfs_visit u;
+    if (been_visited v) then (true, (!pred)) else (false , [])
end;

(* *********************************************************************** *)
@@ -310,7 +310,7 @@
(* Compute list of reversed edges for each adjacency list *)
fun flip (u,(v,l)::el) = (v,(u,l)) :: flip (u,el)
| flip (_,nil) = nil
-
+
(* Compute adjacency list for node u from the list of edges
and return a likewise reduced list of edges.  The list of edges
is searches for edges starting from u, and these edges are removed. *)
@@ -334,23 +334,23 @@
(* Compute, for each adjacency list, the list with reversed edges,
and concatenate these lists. *)
val flipped = List.foldr (op @) nil (map flip g)
-
- in assemble g flipped end
-
+
+ in assemble g flipped end
+
(* *********************************************************************** *)
(*                                                                         *)
(* dfs_reachable eq_comp g u:                                              *)
-(* (int * int list) list -> int -> int list                                *)
+(* (int * int list) list -> int -> int list                                *)
(*                                                                         *)
(* Computes list of all nodes reachable from u in g.                       *)
(*                                                                         *)
(* *********************************************************************** *)

-fun dfs_reachable eq_comp g u =
+fun dfs_reachable eq_comp g u =
let
(* List of vertices which have been visited. *)
val visited  = ref nil;
-
+
fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)

fun dfs_visit g u  =
@@ -361,13 +361,13 @@
else v :: dfs_visit g v @ ds)
in  descendents end
-
+
in u :: dfs_visit g u end;

(* *********************************************************************** *)
(*                                                                         *)
(* dfs_term_reachable g u:                                                  *)
-(* (term * term list) list -> term -> term list                            *)
+(* (term * term list) list -> term -> term list                            *)
(*                                                                         *)
(* Computes list of all nodes reachable from u in g.                       *)
(*                                                                         *)
@@ -375,45 +375,45 @@

fun dfs_term_reachable g u = dfs_reachable (op aconv) g u;

-(* ************************************************************************ *)
+(* ************************************************************************ *)
(*                                                                          *)
(* findPath x y g: Term.term -> Term.term ->                                *)
-(*                  (Term.term * (Term.term * rel list) list) ->            *)
+(*                  (Term.term * (Term.term * rel list) list) ->            *)
(*                  (bool, rel list)                                        *)
(*                                                                          *)
(*  Searches a path from vertex x to vertex y in Graph g, returns true and  *)
(*  the list of edges if path is found, otherwise false and nil.            *)
(*                                                                          *)
-(* ************************************************************************ *)
-
-fun findPath x y g =
-  let
+(* ************************************************************************ *)
+
+fun findPath x y g =
+  let
val (found, tmp) =  dfs (op aconv) g x y ;
val pred = map snd tmp;
-
+
fun path x y  =
let
-	 (* find predecessor u of node v and the edge u -> v *)
-
+         (* find predecessor u of node v and the edge u -> v *)
+
fun lookup v [] = raise Cannot
|   lookup v (e::es) = if (upper e) aconv v then e else lookup v es;
-
-      (* traverse path backwards and return list of visited edges *)
-      fun rev_path v =
-	let val l = lookup v pred
-	    val u = lower l;
-	in
-	  if u aconv x then [l] else (rev_path u) @ [l]
-	end
-
+
+      (* traverse path backwards and return list of visited edges *)
+      fun rev_path v =
+        let val l = lookup v pred
+            val u = lower l;
+        in
+          if u aconv x then [l] else (rev_path u) @ [l]
+        end
+
in rev_path y end;
-
-   in
+
+   in
+

-
if found then ( (found, (path x y) )) else (found,[])
-
-
+
+

end;

@@ -426,143 +426,142 @@
(*                                                                          *)
(* ************************************************************************ *)

-fun findRtranclProof g tranclEdges subgoal =
+fun findRtranclProof g tranclEdges subgoal =
case subgoal of (RTrans (x,y,_)) => if x aconv y then [Thm ([], Cls.rtrancl_refl)] else (
let val (found, path) = findPath (lower subgoal) (upper subgoal) g
-     in
+     in
if found then (
let val path' = (transPath (tl path, hd path))
-	  in
-
-	    case path' of (Trans (_,_,p)) => [Thm ([p], Cls.trancl_into_rtrancl )]
-	    | _ => [getprf path']
-
-	  end
+          in
+
+            case path' of (Trans (_,_,p)) => [Thm ([p], Cls.trancl_into_rtrancl )]
+            | _ => [getprf path']
+
+          end
)
else raise Cannot
end
)
-
+
| (Trans (x,y,_)) => (
-
+
let
val Vx = dfs_term_reachable g x;
val g' = transpose (op aconv) g;
val Vy = dfs_term_reachable g' y;
-
+
fun processTranclEdges [] = raise Cannot
-   |   processTranclEdges (e::es) =
+   |   processTranclEdges (e::es) =
if (upper e) mem Vx andalso (lower e) mem Vx
-	  andalso (upper e) mem Vy andalso (lower e) mem Vy
-	  then (
-
-
-	    if (lower e) aconv x then (
-	      if (upper e) aconv y then (
-	          [(getprf e)]
-	      )
-	      else (
-	          let
-		    val (found,path) = findPath (upper e) y g
-		  in
+          andalso (upper e) mem Vy andalso (lower e) mem Vy
+          then (
+
+
+            if (lower e) aconv x then (
+              if (upper e) aconv y then (
+                  [(getprf e)]
+              )
+              else (
+                  let
+                    val (found,path) = findPath (upper e) y g
+                  in
+
+                   if found then (
+                       [getprf (transPath (path, e))]
+                      ) else processTranclEdges es
+
+                  end
+              )
+            )
+            else if (upper e) aconv y then (
+               let val (xufound,xupath) = findPath x (lower e) g
+               in
+
+                  if xufound then (

-		   if found then (
-		       [getprf (transPath (path, e))]
-		      ) else processTranclEdges es
-
-		  end
-	      )
-	    )
-	    else if (upper e) aconv y then (
-	       let val (xufound,xupath) = findPath x (lower e) g
-	       in
-
-	          if xufound then (
-
-		    let val xuRTranclEdge = transPath (tl xupath, hd xupath)
-			    val xyTranclEdge = makeStep(xuRTranclEdge,e)
-
-				in [getprf xyTranclEdge] end
-
-	         ) else processTranclEdges es
-
-	       end
-	    )
-	    else (
-
-	        let val (xufound,xupath) = findPath x (lower e) g
-		    val (vyfound,vypath) = findPath (upper e) y g
-		 in
-		    if xufound then (
-		         if vyfound then (
-			    let val xuRTranclEdge = transPath (tl xupath, hd xupath)
-			        val vyRTranclEdge = transPath (tl vypath, hd vypath)
-				val xyTranclEdge = makeStep (makeStep(xuRTranclEdge,e),vyRTranclEdge)
-
-				in [getprf xyTranclEdge] end
-
-			 ) else processTranclEdges es
-		    )
-		    else processTranclEdges es
-		 end
-	    )
-	  )
-	  else processTranclEdges es;
+                    let val xuRTranclEdge = transPath (tl xupath, hd xupath)
+                            val xyTranclEdge = makeStep(xuRTranclEdge,e)
+
+                                in [getprf xyTranclEdge] end
+
+                 ) else processTranclEdges es
+
+               end
+            )
+            else (
+
+                let val (xufound,xupath) = findPath x (lower e) g
+                    val (vyfound,vypath) = findPath (upper e) y g
+                 in
+                    if xufound then (
+                         if vyfound then (
+                            let val xuRTranclEdge = transPath (tl xupath, hd xupath)
+                                val vyRTranclEdge = transPath (tl vypath, hd vypath)
+                                val xyTranclEdge = makeStep (makeStep(xuRTranclEdge,e),vyRTranclEdge)
+
+                                in [getprf xyTranclEdge] end
+
+                         ) else processTranclEdges es
+                    )
+                    else processTranclEdges es
+                 end
+            )
+          )
+          else processTranclEdges es;
in processTranclEdges tranclEdges end )
| _ => raise Cannot

-
-fun solveTrancl (asms, concl) =
+
+fun solveTrancl (asms, concl) =
let val (g,_) = mkGraph asms
in
let val (_, subgoal, _) = mkconcl_trancl concl
val (found, path) = findPath (lower subgoal) (upper subgoal) g
in
if found then  [getprf (transPath (tl path, hd path))]
-    else raise Cannot
+    else raise Cannot
end
end;
-
-fun solveRtrancl (asms, concl) =
+
+fun solveRtrancl (asms, concl) =
let val (g,tranclEdges) = mkGraph asms
val (_, subgoal, _) = mkconcl_rtrancl concl
in
findRtranclProof g tranclEdges subgoal
end;
-
-
-val trancl_tac =   SUBGOAL (fn (A, n) => fn st =>
+
+
+fun trancl_tac ctxt = SUBGOAL (fn (A, n) =>
let
-  val thy = theory_of_thm st;
+  val thy = ProofContext.theory_of ctxt;
val Hs = Logic.strip_assums_hyp A;
val C = Logic.strip_assums_concl A;
-  val (rel,subgoals, prf) = mkconcl_trancl C;
-  val prems = List.concat (ListPair.map (mkasm_trancl rel) (Hs, 0 upto (length Hs - 1)))
+  val (rel, subgoals, prf) = mkconcl_trancl C;
+
+  val prems = flat (ListPair.map (mkasm_trancl rel) (Hs, 0 upto (length Hs - 1)));
val prfs = solveTrancl (prems, C);
-
in
-  METAHYPS (fn asms =>
-    let val thms = map (prove thy rel asms) prfs
-    in rtac (prove thy rel thms prf) 1 end) n st
+  FOCUS (fn {prems, ...} =>
+    let val thms = map (prove thy rel prems) prfs
+    in rtac (prove thy rel thms prf) 1 end) ctxt n
end
-handle  Cannot  => no_tac st);
+ handle Cannot => no_tac);

-
-
-val rtrancl_tac =   SUBGOAL (fn (A, n) => fn st =>
+
+fun rtrancl_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
let
-  val thy = theory_of_thm st;
+  val thy = ProofContext.theory_of ctxt;
val Hs = Logic.strip_assums_hyp A;
val C = Logic.strip_assums_concl A;
-  val (rel,subgoals, prf) = mkconcl_rtrancl C;
+  val (rel, subgoals, prf) = mkconcl_rtrancl C;

-  val prems = List.concat (ListPair.map (mkasm_rtrancl rel) (Hs, 0 upto (length Hs - 1)))
+  val prems = flat (ListPair.map (mkasm_rtrancl rel) (Hs, 0 upto (length Hs - 1)));
val prfs = solveRtrancl (prems, C);
in
-  METAHYPS (fn asms =>
-    let val thms = map (prove thy rel asms) prfs
-    in rtac (prove thy rel thms prf) 1 end) n st
+  FOCUS (fn {prems, ...} =>
+    let val thms = map (prove thy rel prems) prfs
+    in rtac (prove thy rel thms prf) 1 end) ctxt n st
end
-handle  Cannot  => no_tac st);
+ handle Cannot => Seq.empty | Subscript => Seq.empty);

end;```