replaced old METAHYPS by FOCUS;
authorwenzelm
Sun Jul 26 22:28:31 2009 +0200 (2009-07-26)
changeset 3221587806301a813
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
src/HOL/Transitive_Closure.thy
src/Provers/order.ML
src/Provers/quasi.ML
src/Provers/trancl.ML
     1.1 --- a/src/HOL/Orderings.thy	Sun Jul 26 22:24:13 2009 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Sun Jul 26 22:28:31 2009 +0200
     1.3 @@ -6,7 +6,9 @@
     1.4  
     1.5  theory Orderings
     1.6  imports HOL
     1.7 -uses "~~/src/Provers/order.ML"
     1.8 +uses
     1.9 +  "~~/src/Provers/order.ML"
    1.10 +  "~~/src/Provers/quasi.ML"  (* FIXME unused? *)
    1.11  begin
    1.12  
    1.13  subsection {* Quasi orders *}
    1.14 @@ -289,7 +291,7 @@
    1.15  sig
    1.16    val print_structures: Proof.context -> unit
    1.17    val setup: theory -> theory
    1.18 -  val order_tac: thm list -> Proof.context -> int -> tactic
    1.19 +  val order_tac: Proof.context -> thm list -> int -> tactic
    1.20  end;
    1.21  
    1.22  structure Orders: ORDERS =
    1.23 @@ -329,7 +331,7 @@
    1.24  
    1.25  (** Method **)
    1.26  
    1.27 -fun struct_tac ((s, [eq, le, less]), thms) prems =
    1.28 +fun struct_tac ((s, [eq, le, less]), thms) ctxt prems =
    1.29    let
    1.30      fun decomp thy (@{const Trueprop} $ t) =
    1.31        let
    1.32 @@ -354,13 +356,13 @@
    1.33        | decomp thy _ = NONE;
    1.34    in
    1.35      case s of
    1.36 -      "order" => Order_Tac.partial_tac decomp thms prems
    1.37 -    | "linorder" => Order_Tac.linear_tac decomp thms prems
    1.38 +      "order" => Order_Tac.partial_tac decomp thms ctxt prems
    1.39 +    | "linorder" => Order_Tac.linear_tac decomp thms ctxt prems
    1.40      | _ => error ("Unknown kind of order `" ^ s ^ "' encountered in transitivity reasoner.")
    1.41    end
    1.42  
    1.43 -fun order_tac prems ctxt =
    1.44 -  FIRST' (map (fn s => CHANGED o struct_tac s prems) (Data.get (Context.Proof ctxt)));
    1.45 +fun order_tac ctxt prems =
    1.46 +  FIRST' (map (fn s => CHANGED o struct_tac s ctxt prems) (Data.get (Context.Proof ctxt)));
    1.47  
    1.48  
    1.49  (** Attribute **)
    1.50 @@ -394,7 +396,7 @@
    1.51  (** Setup **)
    1.52  
    1.53  val setup =
    1.54 -  Method.setup @{binding order} (Scan.succeed (SIMPLE_METHOD' o order_tac []))
    1.55 +  Method.setup @{binding order} (Scan.succeed (fn ctxt => SIMPLE_METHOD' (order_tac ctxt [])))
    1.56      "transitivity reasoner" #>
    1.57    attrib_setup;
    1.58  
    1.59 @@ -532,7 +534,7 @@
    1.60        Simplifier.simproc thy name raw_ts proc) procs)) thy;
    1.61  fun add_solver name tac =
    1.62    Simplifier.map_simpset (fn ss => ss addSolver
    1.63 -    mk_solver' name (fn ss => tac (Simplifier.prems_of_ss ss) (Simplifier.the_context ss)));
    1.64 +    mk_solver' name (fn ss => tac (Simplifier.the_context ss) (Simplifier.prems_of_ss ss)));
    1.65  
    1.66  in
    1.67    add_simprocs [
     2.1 --- a/src/HOL/Transitive_Closure.thy	Sun Jul 26 22:24:13 2009 +0200
     2.2 +++ b/src/HOL/Transitive_Closure.thy	Sun Jul 26 22:28:31 2009 +0200
     2.3 @@ -811,16 +811,16 @@
     2.4  
     2.5  ML {*
     2.6  
     2.7 -structure Trancl_Tac = Trancl_Tac_Fun (
     2.8 -  struct
     2.9 -    val r_into_trancl = @{thm trancl.r_into_trancl};
    2.10 -    val trancl_trans  = @{thm trancl_trans};
    2.11 -    val rtrancl_refl = @{thm rtrancl.rtrancl_refl};
    2.12 -    val r_into_rtrancl = @{thm r_into_rtrancl};
    2.13 -    val trancl_into_rtrancl = @{thm trancl_into_rtrancl};
    2.14 -    val rtrancl_trancl_trancl = @{thm rtrancl_trancl_trancl};
    2.15 -    val trancl_rtrancl_trancl = @{thm trancl_rtrancl_trancl};
    2.16 -    val rtrancl_trans = @{thm rtrancl_trans};
    2.17 +structure Trancl_Tac = Trancl_Tac
    2.18 +(
    2.19 +  val r_into_trancl = @{thm trancl.r_into_trancl};
    2.20 +  val trancl_trans  = @{thm trancl_trans};
    2.21 +  val rtrancl_refl = @{thm rtrancl.rtrancl_refl};
    2.22 +  val r_into_rtrancl = @{thm r_into_rtrancl};
    2.23 +  val trancl_into_rtrancl = @{thm trancl_into_rtrancl};
    2.24 +  val rtrancl_trancl_trancl = @{thm rtrancl_trancl_trancl};
    2.25 +  val trancl_rtrancl_trancl = @{thm trancl_rtrancl_trancl};
    2.26 +  val rtrancl_trans = @{thm rtrancl_trans};
    2.27  
    2.28    fun decomp (@{const Trueprop} $ t) =
    2.29      let fun dec (Const ("op :", _) $ (Const ("Pair", _) $ a $ b) $ rel ) =
    2.30 @@ -832,19 +832,18 @@
    2.31        | dec _ =  NONE
    2.32      in dec t end
    2.33      | decomp _ = NONE;
    2.34 -
    2.35 -  end);
    2.36 +);
    2.37  
    2.38 -structure Tranclp_Tac = Trancl_Tac_Fun (
    2.39 -  struct
    2.40 -    val r_into_trancl = @{thm tranclp.r_into_trancl};
    2.41 -    val trancl_trans  = @{thm tranclp_trans};
    2.42 -    val rtrancl_refl = @{thm rtranclp.rtrancl_refl};
    2.43 -    val r_into_rtrancl = @{thm r_into_rtranclp};
    2.44 -    val trancl_into_rtrancl = @{thm tranclp_into_rtranclp};
    2.45 -    val rtrancl_trancl_trancl = @{thm rtranclp_tranclp_tranclp};
    2.46 -    val trancl_rtrancl_trancl = @{thm tranclp_rtranclp_tranclp};
    2.47 -    val rtrancl_trans = @{thm rtranclp_trans};
    2.48 +structure Tranclp_Tac = Trancl_Tac
    2.49 +(
    2.50 +  val r_into_trancl = @{thm tranclp.r_into_trancl};
    2.51 +  val trancl_trans  = @{thm tranclp_trans};
    2.52 +  val rtrancl_refl = @{thm rtranclp.rtrancl_refl};
    2.53 +  val r_into_rtrancl = @{thm r_into_rtranclp};
    2.54 +  val trancl_into_rtrancl = @{thm tranclp_into_rtranclp};
    2.55 +  val rtrancl_trancl_trancl = @{thm rtranclp_tranclp_tranclp};
    2.56 +  val trancl_rtrancl_trancl = @{thm tranclp_rtranclp_tranclp};
    2.57 +  val rtrancl_trans = @{thm rtranclp_trans};
    2.58  
    2.59    fun decomp (@{const Trueprop} $ t) =
    2.60      let fun dec (rel $ a $ b) =
    2.61 @@ -856,31 +855,31 @@
    2.62        | dec _ =  NONE
    2.63      in dec t end
    2.64      | decomp _ = NONE;
    2.65 -
    2.66 -  end);
    2.67 +);
    2.68  *}
    2.69  
    2.70  declaration {* fn _ =>
    2.71    Simplifier.map_ss (fn ss => ss
    2.72 -    addSolver (mk_solver "Trancl" (fn _ => Trancl_Tac.trancl_tac))
    2.73 -    addSolver (mk_solver "Rtrancl" (fn _ => Trancl_Tac.rtrancl_tac))
    2.74 -    addSolver (mk_solver "Tranclp" (fn _ => Tranclp_Tac.trancl_tac))
    2.75 -    addSolver (mk_solver "Rtranclp" (fn _ => Tranclp_Tac.rtrancl_tac)))
    2.76 +    addSolver (mk_solver' "Trancl" (Trancl_Tac.trancl_tac o Simplifier.the_context))
    2.77 +    addSolver (mk_solver' "Rtrancl" (Trancl_Tac.rtrancl_tac o Simplifier.the_context))
    2.78 +    addSolver (mk_solver' "Tranclp" (Tranclp_Tac.trancl_tac o Simplifier.the_context))
    2.79 +    addSolver (mk_solver' "Rtranclp" (Tranclp_Tac.rtrancl_tac o Simplifier.the_context)))
    2.80  *}
    2.81  
    2.82 -(* Optional methods *)
    2.83 +
    2.84 +text {* Optional methods. *}
    2.85  
    2.86  method_setup trancl =
    2.87 -  {* Scan.succeed (K (SIMPLE_METHOD' Trancl_Tac.trancl_tac)) *}
    2.88 +  {* Scan.succeed (SIMPLE_METHOD' o Trancl_Tac.trancl_tac) *}
    2.89    {* simple transitivity reasoner *}
    2.90  method_setup rtrancl =
    2.91 -  {* Scan.succeed (K (SIMPLE_METHOD' Trancl_Tac.rtrancl_tac)) *}
    2.92 +  {* Scan.succeed (SIMPLE_METHOD' o Trancl_Tac.rtrancl_tac) *}
    2.93    {* simple transitivity reasoner *}
    2.94  method_setup tranclp =
    2.95 -  {* Scan.succeed (K (SIMPLE_METHOD' Tranclp_Tac.trancl_tac)) *}
    2.96 +  {* Scan.succeed (SIMPLE_METHOD' o Tranclp_Tac.trancl_tac) *}
    2.97    {* simple transitivity reasoner (predicate version) *}
    2.98  method_setup rtranclp =
    2.99 -  {* Scan.succeed (K (SIMPLE_METHOD' Tranclp_Tac.rtrancl_tac)) *}
   2.100 +  {* Scan.succeed (SIMPLE_METHOD' o Tranclp_Tac.rtrancl_tac) *}
   2.101    {* simple transitivity reasoner (predicate version) *}
   2.102  
   2.103  end
     3.1 --- a/src/Provers/order.ML	Sun Jul 26 22:24:13 2009 +0200
     3.2 +++ b/src/Provers/order.ML	Sun Jul 26 22:28:31 2009 +0200
     3.3 @@ -35,9 +35,11 @@
     3.4  
     3.5    (* Tactics *)
     3.6    val partial_tac:
     3.7 -    (theory -> term -> (term * string * term) option) -> less_arith -> thm list -> int -> tactic
     3.8 +    (theory -> term -> (term * string * term) option) -> less_arith ->
     3.9 +    Proof.context -> thm list -> int -> tactic
    3.10    val linear_tac:
    3.11 -    (theory -> term -> (term * string * term) option) -> less_arith -> thm list -> int -> tactic
    3.12 +    (theory -> term -> (term * string * term) option) -> less_arith ->
    3.13 +    Proof.context -> thm list -> int -> tactic
    3.14  end;
    3.15  
    3.16  structure Order_Tac: ORDER_TAC =
    3.17 @@ -259,34 +261,28 @@
    3.18        less_le_trans, le_less_trans, le_trans, le_neq_trans, neq_le_trans,
    3.19        not_sym, not_lessD, not_leD, not_lessI, not_leI, less_imp_neq, thm));
    3.20  
    3.21 -
    3.22 -(* Extract subgoal with signature *)
    3.23 -fun SUBGOAL goalfun i st =
    3.24 -  goalfun (List.nth(prems_of st, i-1),  i, Thm.theory_of_thm st) st
    3.25 -                             handle Subscript => Seq.empty;
    3.26 -
    3.27  (* Internal datatype for the proof *)
    3.28  datatype proof
    3.29 -  = Asm of int 
    3.30 -  | Thm of proof list * thm; 
    3.31 -  
    3.32 +  = Asm of int
    3.33 +  | Thm of proof list * thm;
    3.34 +
    3.35  exception Cannot;
    3.36   (* Internal exception, raised if conclusion cannot be derived from
    3.37       assumptions. *)
    3.38  exception Contr of proof;
    3.39    (* Internal exception, raised if contradiction ( x < x ) was derived *)
    3.40  
    3.41 -fun prove asms = 
    3.42 +fun prove asms =
    3.43    let fun pr (Asm i) = List.nth (asms, i)
    3.44    |       pr (Thm (prfs, thm)) = (map pr prfs) MRS thm
    3.45    in pr end;
    3.46  
    3.47  (* Internal datatype for inequalities *)
    3.48 -datatype less 
    3.49 -   = Less  of term * term * proof 
    3.50 +datatype less
    3.51 +   = Less  of term * term * proof
    3.52     | Le    of term * term * proof
    3.53 -   | NotEq of term * term * proof; 
    3.54 -   
    3.55 +   | NotEq of term * term * proof;
    3.56 +
    3.57  (* Misc functions for datatype less *)
    3.58  fun lower (Less (x, _, _)) = x
    3.59    | lower (Le (x, _, _)) = x
    3.60 @@ -314,17 +310,17 @@
    3.61  fun mkasm_partial decomp (less_thms : less_arith) sign (t, n) =
    3.62    case decomp sign t of
    3.63      SOME (x, rel, y) => (case rel of
    3.64 -      "<"   => if (x aconv y) then raise Contr (Thm ([Asm n], #less_reflE less_thms)) 
    3.65 +      "<"   => if (x aconv y) then raise Contr (Thm ([Asm n], #less_reflE less_thms))
    3.66                 else [Less (x, y, Asm n)]
    3.67      | "~<"  => []
    3.68      | "<="  => [Le (x, y, Asm n)]
    3.69 -    | "~<=" => [] 
    3.70 +    | "~<=" => []
    3.71      | "="   => [Le (x, y, Thm ([Asm n], #eqD1 less_thms)),
    3.72                  Le (y, x, Thm ([Asm n], #eqD2 less_thms))]
    3.73 -    | "~="  => if (x aconv y) then 
    3.74 +    | "~="  => if (x aconv y) then
    3.75                    raise Contr (Thm ([(Thm ([(Thm ([], #le_refl less_thms)) ,(Asm n)], #le_neq_trans less_thms))], #less_reflE less_thms))
    3.76                 else [ NotEq (x, y, Asm n),
    3.77 -                      NotEq (y, x,Thm ( [Asm n], #not_sym less_thms))] 
    3.78 +                      NotEq (y, x,Thm ( [Asm n], #not_sym less_thms))]
    3.79      | _     => error ("partial_tac: unknown relation symbol ``" ^ rel ^
    3.80                   "''returned by decomp."))
    3.81    | NONE => [];
    3.82 @@ -338,23 +334,23 @@
    3.83  (* Linear orders only.                                                      *)
    3.84  (*                                                                          *)
    3.85  (* ************************************************************************ *)
    3.86 - 
    3.87 +
    3.88  fun mkasm_linear decomp (less_thms : less_arith) sign (t, n) =
    3.89    case decomp sign t of
    3.90      SOME (x, rel, y) => (case rel of
    3.91 -      "<"   => if (x aconv y) then raise Contr (Thm ([Asm n], #less_reflE less_thms)) 
    3.92 +      "<"   => if (x aconv y) then raise Contr (Thm ([Asm n], #less_reflE less_thms))
    3.93                 else [Less (x, y, Asm n)]
    3.94      | "~<"  => [Le (y, x, Thm ([Asm n], #not_lessD less_thms))]
    3.95      | "<="  => [Le (x, y, Asm n)]
    3.96 -    | "~<=" => if (x aconv y) then 
    3.97 -                  raise (Contr (Thm ([Thm ([Asm n], #not_leD less_thms)], #less_reflE less_thms))) 
    3.98 -               else [Less (y, x, Thm ([Asm n], #not_leD less_thms))] 
    3.99 +    | "~<=" => if (x aconv y) then
   3.100 +                  raise (Contr (Thm ([Thm ([Asm n], #not_leD less_thms)], #less_reflE less_thms)))
   3.101 +               else [Less (y, x, Thm ([Asm n], #not_leD less_thms))]
   3.102      | "="   => [Le (x, y, Thm ([Asm n], #eqD1 less_thms)),
   3.103                  Le (y, x, Thm ([Asm n], #eqD2 less_thms))]
   3.104 -    | "~="  => if (x aconv y) then 
   3.105 +    | "~="  => if (x aconv y) then
   3.106                    raise Contr (Thm ([(Thm ([(Thm ([], #le_refl less_thms)) ,(Asm n)], #le_neq_trans less_thms))], #less_reflE less_thms))
   3.107                 else [ NotEq (x, y, Asm n),
   3.108 -                      NotEq (y, x,Thm ( [Asm n], #not_sym less_thms))] 
   3.109 +                      NotEq (y, x,Thm ( [Asm n], #not_sym less_thms))]
   3.110      | _     => error ("linear_tac: unknown relation symbol ``" ^ rel ^
   3.111                   "''returned by decomp."))
   3.112    | NONE => [];
   3.113 @@ -409,7 +405,7 @@
   3.114       where Rel is one of "<", "<=", "~<", "~<=", "=" and "~=",
   3.115       other relation symbols cause an error message *)
   3.116  
   3.117 -fun gen_order_tac mkasm mkconcl decomp' (less_thms : less_arith) prems =
   3.118 +fun gen_order_tac mkasm mkconcl decomp' (less_thms : less_arith) ctxt prems =
   3.119  
   3.120  let
   3.121  
   3.122 @@ -440,19 +436,19 @@
   3.123  |   mergeLess (Le (x, _, p) , Less (_ , z, q)) =
   3.124        Less (x, z, Thm ([p,q] , #le_less_trans less_thms))
   3.125  |   mergeLess (Le (x, z, p) , NotEq (x', z', q)) =
   3.126 -      if (x aconv x' andalso z aconv z' ) 
   3.127 +      if (x aconv x' andalso z aconv z' )
   3.128        then Less (x, z, Thm ([p,q] , #le_neq_trans less_thms))
   3.129        else error "linear/partial_tac: internal error le_neq_trans"
   3.130  |   mergeLess (NotEq (x, z, p) , Le (x' , z', q)) =
   3.131 -      if (x aconv x' andalso z aconv z') 
   3.132 +      if (x aconv x' andalso z aconv z')
   3.133        then Less (x, z, Thm ([p,q] , #neq_le_trans less_thms))
   3.134        else error "linear/partial_tac: internal error neq_le_trans"
   3.135  |   mergeLess (NotEq (x, z, p) , Less (x' , z', q)) =
   3.136 -      if (x aconv x' andalso z aconv z') 
   3.137 +      if (x aconv x' andalso z aconv z')
   3.138        then Less ((x' , z', q))
   3.139        else error "linear/partial_tac: internal error neq_less_trans"
   3.140  |   mergeLess (Less (x, z, p) , NotEq (x', z', q)) =
   3.141 -      if (x aconv x' andalso z aconv z') 
   3.142 +      if (x aconv x' andalso z aconv z')
   3.143        then Less (x, z, p)
   3.144        else error "linear/partial_tac: internal error less_neq_trans"
   3.145  |   mergeLess (Le (x, _, p) , Le (_ , z, q)) =
   3.146 @@ -471,8 +467,8 @@
   3.147    | (Less (_, y, _)) tr (Less (x', _, _)) = ( y aconv x' )
   3.148    | (Le (_, y, _))   tr (Le (x', _, _))   = ( y aconv x' )
   3.149    | _ tr _ = false;
   3.150 -  
   3.151 -  
   3.152 +
   3.153 +
   3.154  (* ******************************************************************* *)
   3.155  (*                                                                     *)
   3.156  (* transPath (Lesslist, Less): (less list * less) -> less              *)
   3.157 @@ -488,7 +484,7 @@
   3.158  |   transPath (x::xs,lesss) =
   3.159        if lesss tr x then transPath (xs, mergeLess(lesss,x))
   3.160        else error "linear/partial_tac: internal error transpath";
   3.161 -  
   3.162 +
   3.163  (* ******************************************************************* *)
   3.164  (*                                                                     *)
   3.165  (* less1 subsumes less2 : less -> less -> bool                         *)
   3.166 @@ -496,7 +492,7 @@
   3.167  (* subsumes checks whether less1 implies less2                         *)
   3.168  (*                                                                     *)
   3.169  (* ******************************************************************* *)
   3.170 -  
   3.171 +
   3.172  infix subsumes;
   3.173  fun (Less (x, y, _)) subsumes (Le (x', y', _)) =
   3.174        (x aconv x' andalso y aconv y')
   3.175 @@ -554,7 +550,7 @@
   3.176  (*                                                                     *)
   3.177  (* ******************************************************************* *)
   3.178  
   3.179 -   
   3.180 +
   3.181  (* *********************************************************** *)
   3.182  (* Functions for constructing graphs                           *)
   3.183  (* *********************************************************** *)
   3.184 @@ -562,27 +558,27 @@
   3.185  fun addEdge (v,d,[]) = [(v,d)]
   3.186  |   addEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el)
   3.187      else (u,dl):: (addEdge(v,d,el));
   3.188 -    
   3.189 +
   3.190  (* ********************************************************************* *)
   3.191  (*                                                                       *)
   3.192 -(* mkGraphs constructs from a list of objects of type less a graph g,    *) 
   3.193 +(* mkGraphs constructs from a list of objects of type less a graph g,    *)
   3.194  (* by taking all edges that are candidate for a <=, and a list neqE, by  *)
   3.195  (* taking all edges that are candiate for a ~=                           *)
   3.196  (*                                                                       *)
   3.197  (* ********************************************************************* *)
   3.198  
   3.199  fun mkGraphs [] = ([],[],[])
   3.200 -|   mkGraphs lessList = 
   3.201 +|   mkGraphs lessList =
   3.202   let
   3.203  
   3.204  fun buildGraphs ([],leqG,neqG,neqE) = (leqG, neqG, neqE)
   3.205 -|   buildGraphs (l::ls, leqG,neqG, neqE) = case l of 
   3.206 -  (Less (x,y,p)) =>    
   3.207 -       buildGraphs (ls, addEdge (x,[(y,(Less (x, y, p)))],leqG) , 
   3.208 -                        addEdge (x,[(y,(Less (x, y, p)))],neqG), l::neqE) 
   3.209 +|   buildGraphs (l::ls, leqG,neqG, neqE) = case l of
   3.210 +  (Less (x,y,p)) =>
   3.211 +       buildGraphs (ls, addEdge (x,[(y,(Less (x, y, p)))],leqG) ,
   3.212 +                        addEdge (x,[(y,(Less (x, y, p)))],neqG), l::neqE)
   3.213  | (Le (x,y,p)) =>
   3.214 -      buildGraphs (ls, addEdge (x,[(y,(Le (x, y,p)))],leqG) , neqG, neqE) 
   3.215 -| (NotEq  (x,y,p)) => 
   3.216 +      buildGraphs (ls, addEdge (x,[(y,(Le (x, y,p)))],leqG) , neqG, neqE)
   3.217 +| (NotEq  (x,y,p)) =>
   3.218        buildGraphs (ls, leqG , addEdge (x,[(y,(NotEq (x, y, p)))],neqG), l::neqE) ;
   3.219  
   3.220    in buildGraphs (lessList, [], [], []) end;
   3.221 @@ -595,12 +591,12 @@
   3.222  (* List of successors of u in graph g                                      *)
   3.223  (*                                                                         *)
   3.224  (* *********************************************************************** *)
   3.225 - 
   3.226 -fun adjacent eq_comp ((v,adj)::el) u = 
   3.227 +
   3.228 +fun adjacent eq_comp ((v,adj)::el) u =
   3.229      if eq_comp (u, v) then adj else adjacent eq_comp el u
   3.230 -|   adjacent _  []  _ = []  
   3.231 -  
   3.232 -     
   3.233 +|   adjacent _  []  _ = []
   3.234 +
   3.235 +
   3.236  (* *********************************************************************** *)
   3.237  (*                                                                         *)
   3.238  (* transpose g:                                                            *)
   3.239 @@ -616,7 +612,7 @@
   3.240     (* Compute list of reversed edges for each adjacency list *)
   3.241     fun flip (u,(v,l)::el) = (v,(u,l)) :: flip (u,el)
   3.242       | flip (_,nil) = nil
   3.243 -   
   3.244 +
   3.245     (* Compute adjacency list for node u from the list of edges
   3.246        and return a likewise reduced list of edges.  The list of edges
   3.247        is searches for edges starting from u, and these edges are removed. *)
   3.248 @@ -640,19 +636,19 @@
   3.249     (* Compute, for each adjacency list, the list with reversed edges,
   3.250        and concatenate these lists. *)
   3.251     val flipped = List.foldr (op @) nil (map flip g)
   3.252 - 
   3.253 - in assemble g flipped end    
   3.254 -      
   3.255 +
   3.256 + in assemble g flipped end
   3.257 +
   3.258  (* *********************************************************************** *)
   3.259 -(*                                                                         *)      
   3.260 +(*                                                                         *)
   3.261  (* scc_term : (term * term list) list -> term list list                    *)
   3.262  (*                                                                         *)
   3.263  (* The following is based on the algorithm for finding strongly connected  *)
   3.264  (* components described in Introduction to Algorithms, by Cormon, Leiserson*)
   3.265  (* and Rivest, section 23.5. The input G is an adjacency list description  *)
   3.266  (* of a directed graph. The output is a list of the strongly connected     *)
   3.267 -(* components (each a list of vertices).                                   *)          
   3.268 -(*                                                                         *)   
   3.269 +(* components (each a list of vertices).                                   *)
   3.270 +(*                                                                         *)
   3.271  (*                                                                         *)
   3.272  (* *********************************************************************** *)
   3.273  
   3.274 @@ -664,11 +660,11 @@
   3.275  
   3.276    (* List of vertices which have been visited. *)
   3.277    val visited : term list ref = ref nil
   3.278 -  
   3.279 +
   3.280    fun been_visited v = exists (fn w => w aconv v) (!visited)
   3.281 -  
   3.282 +
   3.283    (* Given the adjacency list rep of a graph (a list of pairs),
   3.284 -     return just the first element of each pair, yielding the 
   3.285 +     return just the first element of each pair, yielding the
   3.286       vertex list. *)
   3.287    val members = map (fn (v,_) => v)
   3.288  
   3.289 @@ -701,7 +697,7 @@
   3.290       dfs_visit along with u form a connected component. We
   3.291       collect all the connected components together in a
   3.292       list, which is what is returned. *)
   3.293 -  Library.foldl (fn (comps,u) =>  
   3.294 +  Library.foldl (fn (comps,u) =>
   3.295        if been_visited u then comps
   3.296        else ((u :: dfs_visit (transpose (op aconv) G) u) :: comps))  (nil,(!finish))
   3.297  end;
   3.298 @@ -710,17 +706,17 @@
   3.299  (* *********************************************************************** *)
   3.300  (*                                                                         *)
   3.301  (* dfs_int_reachable g u:                                                  *)
   3.302 -(* (int * int list) list -> int -> int list                                *) 
   3.303 +(* (int * int list) list -> int -> int list                                *)
   3.304  (*                                                                         *)
   3.305  (* Computes list of all nodes reachable from u in g.                       *)
   3.306  (*                                                                         *)
   3.307  (* *********************************************************************** *)
   3.308  
   3.309 -fun dfs_int_reachable g u = 
   3.310 +fun dfs_int_reachable g u =
   3.311   let
   3.312    (* List of vertices which have been visited. *)
   3.313    val visited : int list ref = ref nil
   3.314 -  
   3.315 +
   3.316    fun been_visited v = exists (fn w => w = v) (!visited)
   3.317  
   3.318    fun dfs_visit g u : int list =
   3.319 @@ -731,59 +727,59 @@
   3.320              else v :: dfs_visit g v @ ds)
   3.321          nil (adjacent (op =) g u)
   3.322     in  descendents end
   3.323 - 
   3.324 +
   3.325   in u :: dfs_visit g u end;
   3.326  
   3.327 -    
   3.328 -fun indexComps components = 
   3.329 +
   3.330 +fun indexComps components =
   3.331      ListPair.map (fn (a,b) => (a,b)) (0 upto (length components -1), components);
   3.332  
   3.333 -fun indexNodes IndexComp = 
   3.334 +fun indexNodes IndexComp =
   3.335      List.concat (map (fn (index, comp) => (map (fn v => (v,index)) comp)) IndexComp);
   3.336 -    
   3.337 +
   3.338  fun getIndex v [] = ~1
   3.339 -|   getIndex v ((v',k)::vs) = if v aconv v' then k else getIndex v vs; 
   3.340 -    
   3.341 +|   getIndex v ((v',k)::vs) = if v aconv v' then k else getIndex v vs;
   3.342 +
   3.343  
   3.344  
   3.345  (* *********************************************************************** *)
   3.346  (*                                                                         *)
   3.347  (* dfs eq_comp g u v:                                                       *)
   3.348  (* ('a * 'a -> bool) -> ('a  *( 'a * less) list) list ->                   *)
   3.349 -(* 'a -> 'a -> (bool * ('a * less) list)                                   *) 
   3.350 +(* 'a -> 'a -> (bool * ('a * less) list)                                   *)
   3.351  (*                                                                         *)
   3.352  (* Depth first search of v from u.                                         *)
   3.353  (* Returns (true, path(u, v)) if successful, otherwise (false, []).        *)
   3.354  (*                                                                         *)
   3.355  (* *********************************************************************** *)
   3.356  
   3.357 -fun dfs eq_comp g u v = 
   3.358 - let 
   3.359 +fun dfs eq_comp g u v =
   3.360 + let
   3.361      val pred = ref nil;
   3.362      val visited = ref nil;
   3.363 -    
   3.364 +
   3.365      fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
   3.366 -    
   3.367 -    fun dfs_visit u' = 
   3.368 +
   3.369 +    fun dfs_visit u' =
   3.370      let val _ = visited := u' :: (!visited)
   3.371 -    
   3.372 +
   3.373      fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end;
   3.374 -    
   3.375 -    in if been_visited v then () 
   3.376 +
   3.377 +    in if been_visited v then ()
   3.378      else (app (fn (v',l) => if been_visited v' then () else (
   3.379 -       update (v',l); 
   3.380 +       update (v',l);
   3.381         dfs_visit v'; ()) )) (adjacent eq_comp g u')
   3.382       end
   3.383 -  in 
   3.384 -    dfs_visit u; 
   3.385 -    if (been_visited v) then (true, (!pred)) else (false , [])   
   3.386 +  in
   3.387 +    dfs_visit u;
   3.388 +    if (been_visited v) then (true, (!pred)) else (false , [])
   3.389    end;
   3.390  
   3.391 -  
   3.392 +
   3.393  (* *********************************************************************** *)
   3.394  (*                                                                         *)
   3.395  (* completeTermPath u v g:                                                 *)
   3.396 -(* Term.term -> Term.term -> (Term.term * (Term.term * less) list) list    *) 
   3.397 +(* Term.term -> Term.term -> (Term.term * (Term.term * less) list) list    *)
   3.398  (* -> less list                                                            *)
   3.399  (*                                                                         *)
   3.400  (* Complete the path from u to v in graph g.  Path search is performed     *)
   3.401 @@ -793,36 +789,36 @@
   3.402  (*                                                                         *)
   3.403  (* *********************************************************************** *)
   3.404  
   3.405 -  
   3.406 -fun completeTermPath u v g  = 
   3.407 -  let 
   3.408 +
   3.409 +fun completeTermPath u v g  =
   3.410 +  let
   3.411     val (found, tmp) =  dfs (op aconv) g u v ;
   3.412     val pred = map snd tmp;
   3.413 -   
   3.414 +
   3.415     fun path x y  =
   3.416        let
   3.417 - 
   3.418 +
   3.419        (* find predecessor u of node v and the edge u -> v *)
   3.420  
   3.421        fun lookup v [] = raise Cannot
   3.422        |   lookup v (e::es) = if (upper e) aconv v then e else lookup v es;
   3.423  
   3.424 -      (* traverse path backwards and return list of visited edges *)   
   3.425 -      fun rev_path v = 
   3.426 +      (* traverse path backwards and return list of visited edges *)
   3.427 +      fun rev_path v =
   3.428         let val l = lookup v pred
   3.429             val u = lower l;
   3.430         in
   3.431          if u aconv x then [l]
   3.432 -        else (rev_path u) @ [l] 
   3.433 +        else (rev_path u) @ [l]
   3.434         end
   3.435       in rev_path y end;
   3.436 -       
   3.437 -  in 
   3.438 +
   3.439 +  in
   3.440    if found then (if u aconv v then [(Le (u, v, (Thm ([], #le_refl less_thms))))]
   3.441    else path u v ) else raise Cannot
   3.442 -end;  
   3.443 +end;
   3.444  
   3.445 -      
   3.446 +
   3.447  (* *********************************************************************** *)
   3.448  (*                                                                         *)
   3.449  (* findProof (sccGraph, neqE, ntc, sccSubgraphs) subgoal:                  *)
   3.450 @@ -834,133 +830,133 @@
   3.451  (* proof for subgoal.  Raises exception Cannot if this is not possible.    *)
   3.452  (*                                                                         *)
   3.453  (* *********************************************************************** *)
   3.454 -     
   3.455 +
   3.456  fun findProof (sccGraph, neqE, ntc, sccSubgraphs) subgoal =
   3.457  let
   3.458 -   
   3.459 +
   3.460   (* complete path x y from component graph *)
   3.461 - fun completeComponentPath x y predlist = 
   3.462 -   let         
   3.463 -	  val xi = getIndex x ntc
   3.464 -	  val yi = getIndex y ntc 
   3.465 -	  
   3.466 -	  fun lookup k [] =  raise Cannot
   3.467 -	  |   lookup k ((h: int,l)::us) = if k = h then l else lookup k us;	  
   3.468 -	  
   3.469 -	  fun rev_completeComponentPath y' = 
   3.470 -	   let val edge = lookup (getIndex y' ntc) predlist
   3.471 -	       val u = lower edge
   3.472 -	       val v = upper edge
   3.473 -	   in
   3.474 -             if (getIndex u ntc) = xi then 
   3.475 -	       (completeTermPath x u (List.nth(sccSubgraphs, xi)) )@[edge]
   3.476 -	       @(completeTermPath v y' (List.nth(sccSubgraphs, getIndex y' ntc)) )
   3.477 -	     else (rev_completeComponentPath u)@[edge]
   3.478 -	          @(completeTermPath v y' (List.nth(sccSubgraphs, getIndex y' ntc)) )
   3.479 + fun completeComponentPath x y predlist =
   3.480 +   let
   3.481 +          val xi = getIndex x ntc
   3.482 +          val yi = getIndex y ntc
   3.483 +
   3.484 +          fun lookup k [] =  raise Cannot
   3.485 +          |   lookup k ((h: int,l)::us) = if k = h then l else lookup k us;
   3.486 +
   3.487 +          fun rev_completeComponentPath y' =
   3.488 +           let val edge = lookup (getIndex y' ntc) predlist
   3.489 +               val u = lower edge
   3.490 +               val v = upper edge
   3.491 +           in
   3.492 +             if (getIndex u ntc) = xi then
   3.493 +               (completeTermPath x u (List.nth(sccSubgraphs, xi)) )@[edge]
   3.494 +               @(completeTermPath v y' (List.nth(sccSubgraphs, getIndex y' ntc)) )
   3.495 +             else (rev_completeComponentPath u)@[edge]
   3.496 +                  @(completeTermPath v y' (List.nth(sccSubgraphs, getIndex y' ntc)) )
   3.497             end
   3.498 -   in  
   3.499 -      if x aconv y then 
   3.500 +   in
   3.501 +      if x aconv y then
   3.502          [(Le (x, y, (Thm ([], #le_refl less_thms))))]
   3.503        else ( if xi = yi then completeTermPath x y (List.nth(sccSubgraphs, xi))
   3.504 -             else rev_completeComponentPath y )  
   3.505 +             else rev_completeComponentPath y )
   3.506     end;
   3.507  
   3.508 -(* ******************************************************************* *) 
   3.509 +(* ******************************************************************* *)
   3.510  (* findLess e x y xi yi xreachable yreachable                          *)
   3.511  (*                                                                     *)
   3.512  (* Find a path from x through e to y, of weight <                      *)
   3.513 -(* ******************************************************************* *) 
   3.514 - 
   3.515 - fun findLess e x y xi yi xreachable yreachable = 
   3.516 -  let val u = lower e 
   3.517 +(* ******************************************************************* *)
   3.518 +
   3.519 + fun findLess e x y xi yi xreachable yreachable =
   3.520 +  let val u = lower e
   3.521        val v = upper e
   3.522        val ui = getIndex u ntc
   3.523        val vi = getIndex v ntc
   3.524 -            
   3.525 -  in 
   3.526 -      if ui mem xreachable andalso vi mem xreachable andalso 
   3.527 +
   3.528 +  in
   3.529 +      if ui mem xreachable andalso vi mem xreachable andalso
   3.530           ui mem yreachable andalso vi mem yreachable then (
   3.531 -       
   3.532 -  (case e of (Less (_, _, _)) =>  
   3.533 +
   3.534 +  (case e of (Less (_, _, _)) =>
   3.535         let
   3.536          val (xufound, xupred) =  dfs (op =) sccGraph xi (getIndex u ntc)
   3.537 -	    in 
   3.538 -	     if xufound then (
   3.539 -	      let 
   3.540 -	       val (vyfound, vypred) =  dfs (op =) sccGraph (getIndex v ntc) yi  
   3.541 -	      in 
   3.542 -	       if vyfound then (
   3.543 -	        let 
   3.544 -	         val xypath = (completeComponentPath x u xupred)@[e]@(completeComponentPath v y vypred)
   3.545 -	         val xyLesss = transPath (tl xypath, hd xypath)
   3.546 -	        in 
   3.547 -		 if xyLesss subsumes subgoal then SOME (getprf xyLesss) 
   3.548 +            in
   3.549 +             if xufound then (
   3.550 +              let
   3.551 +               val (vyfound, vypred) =  dfs (op =) sccGraph (getIndex v ntc) yi
   3.552 +              in
   3.553 +               if vyfound then (
   3.554 +                let
   3.555 +                 val xypath = (completeComponentPath x u xupred)@[e]@(completeComponentPath v y vypred)
   3.556 +                 val xyLesss = transPath (tl xypath, hd xypath)
   3.557 +                in
   3.558 +                 if xyLesss subsumes subgoal then SOME (getprf xyLesss)
   3.559                   else NONE
   3.560 -	       end)
   3.561 -	       else NONE
   3.562 -	      end)
   3.563 -	     else NONE
   3.564 -	    end
   3.565 -       |  _   => 
   3.566 -         let val (uvfound, uvpred) =  dfs (op =) sccGraph (getIndex u ntc) (getIndex v ntc) 
   3.567 -             in 
   3.568 -	      if uvfound then (
   3.569 -	       let 
   3.570 -	        val (xufound, xupred) = dfs (op =) sccGraph xi (getIndex u ntc)
   3.571 -	       in
   3.572 -		if xufound then (
   3.573 -		 let 
   3.574 -		  val (vyfound, vypred) =  dfs (op =) sccGraph (getIndex v ntc) yi
   3.575 -		 in 
   3.576 -		  if vyfound then (
   3.577 -		   let
   3.578 -		    val uvpath = completeComponentPath u v uvpred
   3.579 -		    val uvLesss = mergeLess ( transPath (tl uvpath, hd uvpath), e)
   3.580 -		    val xypath = (completeComponentPath  x u xupred)@[uvLesss]@(completeComponentPath v y vypred)
   3.581 -		    val xyLesss = transPath (tl xypath, hd xypath)
   3.582 -		   in 
   3.583 -		    if xyLesss subsumes subgoal then SOME (getprf xyLesss)
   3.584 +               end)
   3.585 +               else NONE
   3.586 +              end)
   3.587 +             else NONE
   3.588 +            end
   3.589 +       |  _   =>
   3.590 +         let val (uvfound, uvpred) =  dfs (op =) sccGraph (getIndex u ntc) (getIndex v ntc)
   3.591 +             in
   3.592 +              if uvfound then (
   3.593 +               let
   3.594 +                val (xufound, xupred) = dfs (op =) sccGraph xi (getIndex u ntc)
   3.595 +               in
   3.596 +                if xufound then (
   3.597 +                 let
   3.598 +                  val (vyfound, vypred) =  dfs (op =) sccGraph (getIndex v ntc) yi
   3.599 +                 in
   3.600 +                  if vyfound then (
   3.601 +                   let
   3.602 +                    val uvpath = completeComponentPath u v uvpred
   3.603 +                    val uvLesss = mergeLess ( transPath (tl uvpath, hd uvpath), e)
   3.604 +                    val xypath = (completeComponentPath  x u xupred)@[uvLesss]@(completeComponentPath v y vypred)
   3.605 +                    val xyLesss = transPath (tl xypath, hd xypath)
   3.606 +                   in
   3.607 +                    if xyLesss subsumes subgoal then SOME (getprf xyLesss)
   3.608                      else NONE
   3.609 -		   end )
   3.610 -		  else NONE   
   3.611 -	         end)
   3.612 -		else NONE
   3.613 -	       end ) 
   3.614 -	      else NONE
   3.615 -	     end )
   3.616 +                   end )
   3.617 +                  else NONE
   3.618 +                 end)
   3.619 +                else NONE
   3.620 +               end )
   3.621 +              else NONE
   3.622 +             end )
   3.623      ) else NONE
   3.624 -end;  
   3.625 -   
   3.626 -         
   3.627 +end;
   3.628 +
   3.629 +
   3.630  in
   3.631    (* looking for x <= y: any path from x to y is sufficient *)
   3.632    case subgoal of (Le (x, y, _)) => (
   3.633 -  if null sccGraph then raise Cannot else ( 
   3.634 -   let 
   3.635 +  if null sccGraph then raise Cannot else (
   3.636 +   let
   3.637      val xi = getIndex x ntc
   3.638      val yi = getIndex y ntc
   3.639      (* searches in sccGraph a path from xi to yi *)
   3.640      val (found, pred) = dfs (op =) sccGraph xi yi
   3.641 -   in 
   3.642 +   in
   3.643      if found then (
   3.644 -       let val xypath = completeComponentPath x y pred 
   3.645 -           val xyLesss = transPath (tl xypath, hd xypath) 
   3.646 -       in  
   3.647 -	  (case xyLesss of
   3.648 -	    (Less (_, _, q)) => if xyLesss subsumes subgoal then (Thm ([q], #less_imp_le less_thms))  
   3.649 -				else raise Cannot
   3.650 -	     | _   => if xyLesss subsumes subgoal then (getprf xyLesss) 
   3.651 -	              else raise Cannot)
   3.652 +       let val xypath = completeComponentPath x y pred
   3.653 +           val xyLesss = transPath (tl xypath, hd xypath)
   3.654 +       in
   3.655 +          (case xyLesss of
   3.656 +            (Less (_, _, q)) => if xyLesss subsumes subgoal then (Thm ([q], #less_imp_le less_thms))
   3.657 +                                else raise Cannot
   3.658 +             | _   => if xyLesss subsumes subgoal then (getprf xyLesss)
   3.659 +                      else raise Cannot)
   3.660         end )
   3.661 -     else raise Cannot 
   3.662 -   end 
   3.663 +     else raise Cannot
   3.664 +   end
   3.665      )
   3.666     )
   3.667   (* looking for x < y: particular path required, which is not necessarily
   3.668      found by normal dfs *)
   3.669   |   (Less (x, y, _)) => (
   3.670    if null sccGraph then raise Cannot else (
   3.671 -   let 
   3.672 +   let
   3.673      val xi = getIndex x ntc
   3.674      val yi = getIndex y ntc
   3.675      val sccGraph_transpose = transpose (op =) sccGraph
   3.676 @@ -969,13 +965,13 @@
   3.677      (* all comonents reachable from y in the transposed graph sccGraph' *)
   3.678      val yreachable = dfs_int_reachable sccGraph_transpose yi
   3.679      (* for all edges u ~= v or u < v check if they are part of path x < y *)
   3.680 -    fun processNeqEdges [] = raise Cannot 
   3.681 -    |   processNeqEdges (e::es) = 
   3.682 -      case  (findLess e x y xi yi xreachable yreachable) of (SOME prf) => prf  
   3.683 +    fun processNeqEdges [] = raise Cannot
   3.684 +    |   processNeqEdges (e::es) =
   3.685 +      case  (findLess e x y xi yi xreachable yreachable) of (SOME prf) => prf
   3.686        | _ => processNeqEdges es
   3.687 -        
   3.688 -    in 
   3.689 -       processNeqEdges neqE 
   3.690 +
   3.691 +    in
   3.692 +       processNeqEdges neqE
   3.693      end
   3.694    )
   3.695   )
   3.696 @@ -986,99 +982,99 @@
   3.697    else if null sccSubgraphs then (
   3.698       (case (Library.find_first (fn fact => fact subsumes subgoal) neqE, subgoal) of
   3.699         ( SOME (NotEq (x, y, p)), NotEq (x', y', _)) =>
   3.700 -          if  (x aconv x' andalso y aconv y') then p 
   3.701 -	  else Thm ([p], #not_sym less_thms)
   3.702 -     | ( SOME (Less (x, y, p)), NotEq (x', y', _)) => 
   3.703 +          if  (x aconv x' andalso y aconv y') then p
   3.704 +          else Thm ([p], #not_sym less_thms)
   3.705 +     | ( SOME (Less (x, y, p)), NotEq (x', y', _)) =>
   3.706            if x aconv x' andalso y aconv y' then (Thm ([p], #less_imp_neq less_thms))
   3.707            else (Thm ([(Thm ([p], #less_imp_neq less_thms))], #not_sym less_thms))
   3.708 -     | _ => raise Cannot) 
   3.709 +     | _ => raise Cannot)
   3.710     ) else (
   3.711 -   
   3.712 -   let  val xi = getIndex x ntc 
   3.713 +
   3.714 +   let  val xi = getIndex x ntc
   3.715          val yi = getIndex y ntc
   3.716 -	val sccGraph_transpose = transpose (op =) sccGraph
   3.717 +        val sccGraph_transpose = transpose (op =) sccGraph
   3.718          val xreachable = dfs_int_reachable sccGraph xi
   3.719 -	val yreachable = dfs_int_reachable sccGraph_transpose yi
   3.720 -	
   3.721 -	fun processNeqEdges [] = raise Cannot  
   3.722 -  	|   processNeqEdges (e::es) = (
   3.723 -	    let val u = lower e 
   3.724 -	        val v = upper e
   3.725 -		val ui = getIndex u ntc
   3.726 -		val vi = getIndex v ntc
   3.727 -		
   3.728 -	    in  
   3.729 -	        (* if x ~= y follows from edge e *)
   3.730 -	    	if e subsumes subgoal then (
   3.731 -		     case e of (Less (u, v, q)) => (
   3.732 -		       if u aconv x andalso v aconv y then (Thm ([q], #less_imp_neq less_thms))
   3.733 -		       else (Thm ([(Thm ([q], #less_imp_neq less_thms))], #not_sym less_thms))
   3.734 -		     )
   3.735 -		     |    (NotEq (u,v, q)) => (
   3.736 -		       if u aconv x andalso v aconv y then q
   3.737 -		       else (Thm ([q],  #not_sym less_thms))
   3.738 -		     )
   3.739 -		 )
   3.740 +        val yreachable = dfs_int_reachable sccGraph_transpose yi
   3.741 +
   3.742 +        fun processNeqEdges [] = raise Cannot
   3.743 +        |   processNeqEdges (e::es) = (
   3.744 +            let val u = lower e
   3.745 +                val v = upper e
   3.746 +                val ui = getIndex u ntc
   3.747 +                val vi = getIndex v ntc
   3.748 +
   3.749 +            in
   3.750 +                (* if x ~= y follows from edge e *)
   3.751 +                if e subsumes subgoal then (
   3.752 +                     case e of (Less (u, v, q)) => (
   3.753 +                       if u aconv x andalso v aconv y then (Thm ([q], #less_imp_neq less_thms))
   3.754 +                       else (Thm ([(Thm ([q], #less_imp_neq less_thms))], #not_sym less_thms))
   3.755 +                     )
   3.756 +                     |    (NotEq (u,v, q)) => (
   3.757 +                       if u aconv x andalso v aconv y then q
   3.758 +                       else (Thm ([q],  #not_sym less_thms))
   3.759 +                     )
   3.760 +                 )
   3.761                  (* if SCC_x is linked to SCC_y via edge e *)
   3.762 -		 else if ui = xi andalso vi = yi then (
   3.763 +                 else if ui = xi andalso vi = yi then (
   3.764                     case e of (Less (_, _,_)) => (
   3.765 -		        let val xypath = (completeTermPath x u (List.nth(sccSubgraphs, ui)) ) @ [e] @ (completeTermPath v y (List.nth(sccSubgraphs, vi)) )
   3.766 -			    val xyLesss = transPath (tl xypath, hd xypath)
   3.767 -			in  (Thm ([getprf xyLesss], #less_imp_neq less_thms)) end)
   3.768 -		   | _ => (   
   3.769 -		        let 
   3.770 -			    val xupath = completeTermPath x u  (List.nth(sccSubgraphs, ui))
   3.771 -			    val uxpath = completeTermPath u x  (List.nth(sccSubgraphs, ui))
   3.772 -			    val vypath = completeTermPath v y  (List.nth(sccSubgraphs, vi))
   3.773 -			    val yvpath = completeTermPath y v  (List.nth(sccSubgraphs, vi))
   3.774 -			    val xuLesss = transPath (tl xupath, hd xupath)     
   3.775 -			    val uxLesss = transPath (tl uxpath, hd uxpath)			    
   3.776 -			    val vyLesss = transPath (tl vypath, hd vypath)			
   3.777 -			    val yvLesss = transPath (tl yvpath, hd yvpath)
   3.778 -			    val x_eq_u =  (Thm ([(getprf xuLesss),(getprf uxLesss)], #eqI less_thms))
   3.779 -			    val v_eq_y =  (Thm ([(getprf vyLesss),(getprf yvLesss)], #eqI less_thms))
   3.780 -			in 
   3.781 -                           (Thm ([x_eq_u , (getprf e), v_eq_y ], #eq_neq_eq_imp_neq less_thms)) 
   3.782 -			end
   3.783 -			)       
   3.784 -		  ) else if ui = yi andalso vi = xi then (
   3.785 -		     case e of (Less (_, _,_)) => (
   3.786 -		        let val xypath = (completeTermPath y u (List.nth(sccSubgraphs, ui)) ) @ [e] @ (completeTermPath v x (List.nth(sccSubgraphs, vi)) )
   3.787 -			    val xyLesss = transPath (tl xypath, hd xypath)
   3.788 -			in (Thm ([(Thm ([getprf xyLesss], #less_imp_neq less_thms))] , #not_sym less_thms)) end ) 
   3.789 -		     | _ => (
   3.790 -		        
   3.791 -			let val yupath = completeTermPath y u (List.nth(sccSubgraphs, ui))
   3.792 -			    val uypath = completeTermPath u y (List.nth(sccSubgraphs, ui))
   3.793 -			    val vxpath = completeTermPath v x (List.nth(sccSubgraphs, vi))
   3.794 -			    val xvpath = completeTermPath x v (List.nth(sccSubgraphs, vi))
   3.795 -			    val yuLesss = transPath (tl yupath, hd yupath)     
   3.796 -			    val uyLesss = transPath (tl uypath, hd uypath)			    
   3.797 -			    val vxLesss = transPath (tl vxpath, hd vxpath)			
   3.798 -			    val xvLesss = transPath (tl xvpath, hd xvpath)
   3.799 -			    val y_eq_u =  (Thm ([(getprf yuLesss),(getprf uyLesss)], #eqI less_thms))
   3.800 -			    val v_eq_x =  (Thm ([(getprf vxLesss),(getprf xvLesss)], #eqI less_thms))
   3.801 -			in
   3.802 -			    (Thm ([(Thm ([y_eq_u , (getprf e), v_eq_x ], #eq_neq_eq_imp_neq less_thms))], #not_sym less_thms))
   3.803 -		        end
   3.804 -		       )
   3.805 -		  ) else (
   3.806 +                        let val xypath = (completeTermPath x u (List.nth(sccSubgraphs, ui)) ) @ [e] @ (completeTermPath v y (List.nth(sccSubgraphs, vi)) )
   3.807 +                            val xyLesss = transPath (tl xypath, hd xypath)
   3.808 +                        in  (Thm ([getprf xyLesss], #less_imp_neq less_thms)) end)
   3.809 +                   | _ => (
   3.810 +                        let
   3.811 +                            val xupath = completeTermPath x u  (List.nth(sccSubgraphs, ui))
   3.812 +                            val uxpath = completeTermPath u x  (List.nth(sccSubgraphs, ui))
   3.813 +                            val vypath = completeTermPath v y  (List.nth(sccSubgraphs, vi))
   3.814 +                            val yvpath = completeTermPath y v  (List.nth(sccSubgraphs, vi))
   3.815 +                            val xuLesss = transPath (tl xupath, hd xupath)
   3.816 +                            val uxLesss = transPath (tl uxpath, hd uxpath)
   3.817 +                            val vyLesss = transPath (tl vypath, hd vypath)
   3.818 +                            val yvLesss = transPath (tl yvpath, hd yvpath)
   3.819 +                            val x_eq_u =  (Thm ([(getprf xuLesss),(getprf uxLesss)], #eqI less_thms))
   3.820 +                            val v_eq_y =  (Thm ([(getprf vyLesss),(getprf yvLesss)], #eqI less_thms))
   3.821 +                        in
   3.822 +                           (Thm ([x_eq_u , (getprf e), v_eq_y ], #eq_neq_eq_imp_neq less_thms))
   3.823 +                        end
   3.824 +                        )
   3.825 +                  ) else if ui = yi andalso vi = xi then (
   3.826 +                     case e of (Less (_, _,_)) => (
   3.827 +                        let val xypath = (completeTermPath y u (List.nth(sccSubgraphs, ui)) ) @ [e] @ (completeTermPath v x (List.nth(sccSubgraphs, vi)) )
   3.828 +                            val xyLesss = transPath (tl xypath, hd xypath)
   3.829 +                        in (Thm ([(Thm ([getprf xyLesss], #less_imp_neq less_thms))] , #not_sym less_thms)) end )
   3.830 +                     | _ => (
   3.831 +
   3.832 +                        let val yupath = completeTermPath y u (List.nth(sccSubgraphs, ui))
   3.833 +                            val uypath = completeTermPath u y (List.nth(sccSubgraphs, ui))
   3.834 +                            val vxpath = completeTermPath v x (List.nth(sccSubgraphs, vi))
   3.835 +                            val xvpath = completeTermPath x v (List.nth(sccSubgraphs, vi))
   3.836 +                            val yuLesss = transPath (tl yupath, hd yupath)
   3.837 +                            val uyLesss = transPath (tl uypath, hd uypath)
   3.838 +                            val vxLesss = transPath (tl vxpath, hd vxpath)
   3.839 +                            val xvLesss = transPath (tl xvpath, hd xvpath)
   3.840 +                            val y_eq_u =  (Thm ([(getprf yuLesss),(getprf uyLesss)], #eqI less_thms))
   3.841 +                            val v_eq_x =  (Thm ([(getprf vxLesss),(getprf xvLesss)], #eqI less_thms))
   3.842 +                        in
   3.843 +                            (Thm ([(Thm ([y_eq_u , (getprf e), v_eq_x ], #eq_neq_eq_imp_neq less_thms))], #not_sym less_thms))
   3.844 +                        end
   3.845 +                       )
   3.846 +                  ) else (
   3.847                         (* there exists a path x < y or y < x such that
   3.848                            x ~= y may be concluded *)
   3.849 -	        	case  (findLess e x y xi yi xreachable yreachable) of 
   3.850 -		              (SOME prf) =>  (Thm ([prf], #less_imp_neq less_thms))  
   3.851 +                        case  (findLess e x y xi yi xreachable yreachable) of
   3.852 +                              (SOME prf) =>  (Thm ([prf], #less_imp_neq less_thms))
   3.853                               | NONE =>  (
   3.854 -		               let 
   3.855 -		                val yr = dfs_int_reachable sccGraph yi
   3.856 -	                        val xr = dfs_int_reachable sccGraph_transpose xi
   3.857 -		               in 
   3.858 -		                case  (findLess e y x yi xi yr xr) of 
   3.859 -		                      (SOME prf) => (Thm ([(Thm ([prf], #less_imp_neq less_thms))], #not_sym less_thms)) 
   3.860 +                               let
   3.861 +                                val yr = dfs_int_reachable sccGraph yi
   3.862 +                                val xr = dfs_int_reachable sccGraph_transpose xi
   3.863 +                               in
   3.864 +                                case  (findLess e y x yi xi yr xr) of
   3.865 +                                      (SOME prf) => (Thm ([(Thm ([prf], #less_imp_neq less_thms))], #not_sym less_thms))
   3.866                                        | _ => processNeqEdges es
   3.867 -		               end)
   3.868 -		 ) end) 
   3.869 +                               end)
   3.870 +                 ) end)
   3.871       in processNeqEdges neqE end)
   3.872 -  )    
   3.873 +  )
   3.874  end;
   3.875  
   3.876  
   3.877 @@ -1110,115 +1106,115 @@
   3.878  (* ******************************************************************* *)
   3.879  
   3.880  fun mk_sccGraphs _ [] _ _ = ([],[])
   3.881 -|   mk_sccGraphs components leqG neqG ntc = 
   3.882 +|   mk_sccGraphs components leqG neqG ntc =
   3.883      let
   3.884      (* Liste (Index der Komponente, Komponente *)
   3.885      val IndexComp = indexComps components;
   3.886  
   3.887 -       
   3.888 -    fun handleContr edge g = 
   3.889 -       (case edge of 
   3.890 +
   3.891 +    fun handleContr edge g =
   3.892 +       (case edge of
   3.893            (Less  (x, y, _)) => (
   3.894 -	    let 
   3.895 -	     val xxpath = edge :: (completeTermPath y x g )
   3.896 -	     val xxLesss = transPath (tl xxpath, hd xxpath)
   3.897 -	     val q = getprf xxLesss
   3.898 -	    in 
   3.899 -	     raise (Contr (Thm ([q], #less_reflE less_thms ))) 
   3.900 -	    end 
   3.901 -	  )
   3.902 +            let
   3.903 +             val xxpath = edge :: (completeTermPath y x g )
   3.904 +             val xxLesss = transPath (tl xxpath, hd xxpath)
   3.905 +             val q = getprf xxLesss
   3.906 +            in
   3.907 +             raise (Contr (Thm ([q], #less_reflE less_thms )))
   3.908 +            end
   3.909 +          )
   3.910          | (NotEq (x, y, _)) => (
   3.911 -	    let 
   3.912 -	     val xypath = (completeTermPath x y g )
   3.913 -	     val yxpath = (completeTermPath y x g )
   3.914 -	     val xyLesss = transPath (tl xypath, hd xypath)
   3.915 -	     val yxLesss = transPath (tl yxpath, hd yxpath)
   3.916 -             val q = getprf (mergeLess ((mergeLess (edge, xyLesss)),yxLesss )) 
   3.917 -	    in 
   3.918 -	     raise (Contr (Thm ([q], #less_reflE less_thms )))
   3.919 -	    end  
   3.920 -	 )
   3.921 -	| _ =>  error "trans_tac/handleContr: invalid Contradiction");
   3.922 - 
   3.923 -   	
   3.924 -    (* k is index of the actual component *)   
   3.925 -       
   3.926 -    fun processComponent (k, comp) = 
   3.927 -     let    
   3.928 -        (* all edges with weight <= of the actual component *)  
   3.929 +            let
   3.930 +             val xypath = (completeTermPath x y g )
   3.931 +             val yxpath = (completeTermPath y x g )
   3.932 +             val xyLesss = transPath (tl xypath, hd xypath)
   3.933 +             val yxLesss = transPath (tl yxpath, hd yxpath)
   3.934 +             val q = getprf (mergeLess ((mergeLess (edge, xyLesss)),yxLesss ))
   3.935 +            in
   3.936 +             raise (Contr (Thm ([q], #less_reflE less_thms )))
   3.937 +            end
   3.938 +         )
   3.939 +        | _ =>  error "trans_tac/handleContr: invalid Contradiction");
   3.940 +
   3.941 +
   3.942 +    (* k is index of the actual component *)
   3.943 +
   3.944 +    fun processComponent (k, comp) =
   3.945 +     let
   3.946 +        (* all edges with weight <= of the actual component *)
   3.947          val leqEdges = List.concat (map (adjacent (op aconv) leqG) comp);
   3.948 -        (* all edges with weight ~= of the actual component *)  
   3.949 +        (* all edges with weight ~= of the actual component *)
   3.950          val neqEdges = map snd (List.concat (map (adjacent (op aconv) neqG) comp));
   3.951  
   3.952 -       (* find an edge leading to a contradiction *)   
   3.953 +       (* find an edge leading to a contradiction *)
   3.954         fun findContr [] = NONE
   3.955 -       |   findContr (e::es) = 
   3.956 -		    let val ui = (getIndex (lower e) ntc) 
   3.957 -			val vi = (getIndex (upper e) ntc) 
   3.958 -		    in 
   3.959 -		        if ui = vi then  SOME e
   3.960 -		        else findContr es
   3.961 -		    end; 
   3.962 -		   
   3.963 -		(* sort edges into component internal edges and 
   3.964 -		   edges pointing away from the component *)
   3.965 -		fun sortEdges  [] (intern,extern)  = (intern,extern)
   3.966 -		|   sortEdges  ((v,l)::es) (intern, extern) = 
   3.967 -		    let val k' = getIndex v ntc in 
   3.968 -		        if k' = k then 
   3.969 -			    sortEdges es (l::intern, extern)
   3.970 -			else sortEdges  es (intern, (k',l)::extern) end;
   3.971 -		
   3.972 -		(* Insert edge into sorted list of edges, where edge is
   3.973 +       |   findContr (e::es) =
   3.974 +                    let val ui = (getIndex (lower e) ntc)
   3.975 +                        val vi = (getIndex (upper e) ntc)
   3.976 +                    in
   3.977 +                        if ui = vi then  SOME e
   3.978 +                        else findContr es
   3.979 +                    end;
   3.980 +
   3.981 +                (* sort edges into component internal edges and
   3.982 +                   edges pointing away from the component *)
   3.983 +                fun sortEdges  [] (intern,extern)  = (intern,extern)
   3.984 +                |   sortEdges  ((v,l)::es) (intern, extern) =
   3.985 +                    let val k' = getIndex v ntc in
   3.986 +                        if k' = k then
   3.987 +                            sortEdges es (l::intern, extern)
   3.988 +                        else sortEdges  es (intern, (k',l)::extern) end;
   3.989 +
   3.990 +                (* Insert edge into sorted list of edges, where edge is
   3.991                      only added if
   3.992                      - it is found for the first time
   3.993                      - it is a <= edge and no parallel < edge was found earlier
   3.994                      - it is a < edge
   3.995                   *)
   3.996 -          	 fun insert (h: int,l) [] = [(h,l)]
   3.997 -		 |   insert (h,l) ((k',l')::es) = if h = k' then (
   3.998 -		     case l of (Less (_, _, _)) => (h,l)::es
   3.999 -		     | _  => (case l' of (Less (_, _, _)) => (h,l')::es
  3.1000 -	                      | _ => (k',l)::es) )
  3.1001 -		     else (k',l'):: insert (h,l) es;
  3.1002 -		
  3.1003 -		(* Reorganise list of edges such that
  3.1004 +                 fun insert (h: int,l) [] = [(h,l)]
  3.1005 +                 |   insert (h,l) ((k',l')::es) = if h = k' then (
  3.1006 +                     case l of (Less (_, _, _)) => (h,l)::es
  3.1007 +                     | _  => (case l' of (Less (_, _, _)) => (h,l')::es
  3.1008 +                              | _ => (k',l)::es) )
  3.1009 +                     else (k',l'):: insert (h,l) es;
  3.1010 +
  3.1011 +                (* Reorganise list of edges such that
  3.1012                      - duplicate edges are removed
  3.1013                      - if a < edge and a <= edge exist at the same time,
  3.1014                        remove <= edge *)
  3.1015 -    		 fun reOrganizeEdges [] sorted = sorted: (int * less) list
  3.1016 -		 |   reOrganizeEdges (e::es) sorted = reOrganizeEdges es (insert e sorted); 
  3.1017 -	
  3.1018 +                 fun reOrganizeEdges [] sorted = sorted: (int * less) list
  3.1019 +                 |   reOrganizeEdges (e::es) sorted = reOrganizeEdges es (insert e sorted);
  3.1020 +
  3.1021                   (* construct the subgraph forming the strongly connected component
  3.1022 -		    from the edge list *)    
  3.1023 -		 fun sccSubGraph [] g  = g
  3.1024 -		 |   sccSubGraph (l::ls) g = 
  3.1025 -		          sccSubGraph ls (addEdge ((lower l),[((upper l),l)],g))
  3.1026 -		 
  3.1027 -		 val (intern, extern) = sortEdges leqEdges ([], []);
  3.1028 +                    from the edge list *)
  3.1029 +                 fun sccSubGraph [] g  = g
  3.1030 +                 |   sccSubGraph (l::ls) g =
  3.1031 +                          sccSubGraph ls (addEdge ((lower l),[((upper l),l)],g))
  3.1032 +
  3.1033 +                 val (intern, extern) = sortEdges leqEdges ([], []);
  3.1034                   val subGraph = sccSubGraph intern [];
  3.1035 -		  
  3.1036 -     in  
  3.1037 +
  3.1038 +     in
  3.1039           case findContr neqEdges of SOME e => handleContr e subGraph
  3.1040 -	 | _ => ((k, (reOrganizeEdges (extern) [])), subGraph)
  3.1041 -     end; 
  3.1042 -  
  3.1043 -    val tmp =  map processComponent IndexComp    
  3.1044 -in 
  3.1045 -     ( (map fst tmp), (map snd tmp))  
  3.1046 -end; 
  3.1047 +         | _ => ((k, (reOrganizeEdges (extern) [])), subGraph)
  3.1048 +     end;
  3.1049 +
  3.1050 +    val tmp =  map processComponent IndexComp
  3.1051 +in
  3.1052 +     ( (map fst tmp), (map snd tmp))
  3.1053 +end;
  3.1054  
  3.1055  
  3.1056  (** Find proof if possible. **)
  3.1057  
  3.1058  fun gen_solve mkconcl sign (asms, concl) =
  3.1059 - let 
  3.1060 + let
  3.1061    val (leqG, neqG, neqE) = mkGraphs asms
  3.1062 -  val components = scc_term leqG   
  3.1063 +  val components = scc_term leqG
  3.1064    val ntc = indexNodes (indexComps components)
  3.1065    val (sccGraph, sccSubgraphs) = mk_sccGraphs components leqG neqG ntc
  3.1066   in
  3.1067 -   let 
  3.1068 +   let
  3.1069     val (subgoals, prf) = mkconcl decomp less_thms sign concl
  3.1070     fun solve facts less =
  3.1071        (case triv_solv less of NONE => findProof (sccGraph, neqE, ntc, sccSubgraphs) less
  3.1072 @@ -1229,24 +1225,25 @@
  3.1073   end;
  3.1074  
  3.1075  in
  3.1076 -
  3.1077 -    SUBGOAL (fn (A, n, sign) =>
  3.1078 -     let
  3.1079 -      val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A))
  3.1080 -      val Hs = map prop_of prems @ map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
  3.1081 -      val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
  3.1082 -      val lesss = List.concat (ListPair.map (mkasm decomp less_thms sign) (Hs, 0 upto (length Hs - 1)))
  3.1083 -      val prfs = gen_solve mkconcl sign (lesss, C);
  3.1084 -      val (subgoals, prf) = mkconcl decomp less_thms sign C;
  3.1085 -     in
  3.1086 -      METAHYPS (fn asms =>
  3.1087 -	let val thms = map (prove (prems @ asms)) prfs
  3.1088 -	in rtac (prove thms prf) 1 end) n
  3.1089 -     end
  3.1090 -     handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n
  3.1091 -	  | Cannot  => no_tac
  3.1092 -	  )
  3.1093 -
  3.1094 + SUBGOAL (fn (A, n) => fn st =>
  3.1095 +  let
  3.1096 +   val thy = ProofContext.theory_of ctxt;
  3.1097 +   val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A));
  3.1098 +   val Hs = map prop_of prems @ map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
  3.1099 +   val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
  3.1100 +   val lesss = List.concat (ListPair.map (mkasm decomp less_thms thy) (Hs, 0 upto (length Hs - 1)))
  3.1101 +   val prfs = gen_solve mkconcl thy (lesss, C);
  3.1102 +   val (subgoals, prf) = mkconcl decomp less_thms thy C;
  3.1103 +  in
  3.1104 +   FOCUS (fn {prems = asms, ...} =>
  3.1105 +     let val thms = map (prove (prems @ asms)) prfs
  3.1106 +     in rtac (prove thms prf) 1 end) ctxt n st
  3.1107 +  end
  3.1108 +  handle Contr p =>
  3.1109 +      (FOCUS (fn {prems = asms, ...} => rtac (prove asms p) 1) ctxt n st
  3.1110 +        handle Subscript => Seq.empty)
  3.1111 +   | Cannot => Seq.empty
  3.1112 +   | Subscript => Seq.empty)
  3.1113  end;
  3.1114  
  3.1115  (* partial_tac - solves partial orders *)
  3.1116 @@ -1255,5 +1252,4 @@
  3.1117  (* linear_tac - solves linear/total orders *)
  3.1118  val linear_tac = gen_order_tac mkasm_linear mkconcl_linear;
  3.1119  
  3.1120 -       
  3.1121  end;
     4.1 --- a/src/Provers/quasi.ML	Sun Jul 26 22:24:13 2009 +0200
     4.2 +++ b/src/Provers/quasi.ML	Sun Jul 26 22:28:31 2009 +0200
     4.3 @@ -3,10 +3,10 @@
     4.4  Reasoner for simple transitivity and quasi orders.
     4.5  *)
     4.6  
     4.7 -(* 
     4.8 - 
     4.9 +(*
    4.10 +
    4.11  The package provides tactics trans_tac and quasi_tac that use
    4.12 -premises of the form 
    4.13 +premises of the form
    4.14  
    4.15    t = u, t ~= u, t < u and t <= u
    4.16  
    4.17 @@ -29,15 +29,15 @@
    4.18     the assumptions.
    4.19     Note that the presence of a strict relation is not necessary for
    4.20     quasi_tac.  Configure decomp_quasi to ignore < and ~=.  A list of
    4.21 -   required theorems for both situations is given below. 
    4.22 +   required theorems for both situations is given below.
    4.23  *)
    4.24  
    4.25  signature LESS_ARITH =
    4.26  sig
    4.27    (* Transitivity of <=
    4.28 -     Note that transitivities for < hold for partial orders only. *) 
    4.29 +     Note that transitivities for < hold for partial orders only. *)
    4.30    val le_trans: thm  (* [| x <= y; y <= z |] ==> x <= z *)
    4.31 - 
    4.32 +
    4.33    (* Additional theorem for quasi orders *)
    4.34    val le_refl: thm  (* x <= x *)
    4.35    val eqD1: thm (* x = y ==> x <= y *)
    4.36 @@ -64,41 +64,36 @@
    4.37    val decomp_quasi: theory -> term -> (term * string * term) option
    4.38  end;
    4.39  
    4.40 -signature QUASI_TAC = 
    4.41 +signature QUASI_TAC =
    4.42  sig
    4.43 -  val trans_tac: int -> tactic
    4.44 -  val quasi_tac: int -> tactic
    4.45 +  val trans_tac: Proof.context -> int -> tactic
    4.46 +  val quasi_tac: Proof.context -> int -> tactic
    4.47  end;
    4.48  
    4.49 -functor Quasi_Tac_Fun (Less: LESS_ARITH): QUASI_TAC =
    4.50 +functor Quasi_Tac(Less: LESS_ARITH): QUASI_TAC =
    4.51  struct
    4.52  
    4.53 -(* Extract subgoal with signature *)
    4.54 -fun SUBGOAL goalfun i st =
    4.55 -  goalfun (List.nth(prems_of st, i-1),  i, Thm.theory_of_thm st) st
    4.56 -                             handle Subscript => Seq.empty;
    4.57 -
    4.58  (* Internal datatype for the proof *)
    4.59  datatype proof
    4.60 -  = Asm of int 
    4.61 -  | Thm of proof list * thm; 
    4.62 -  
    4.63 +  = Asm of int
    4.64 +  | Thm of proof list * thm;
    4.65 +
    4.66  exception Cannot;
    4.67   (* Internal exception, raised if conclusion cannot be derived from
    4.68       assumptions. *)
    4.69  exception Contr of proof;
    4.70    (* Internal exception, raised if contradiction ( x < x ) was derived *)
    4.71  
    4.72 -fun prove asms = 
    4.73 +fun prove asms =
    4.74    let fun pr (Asm i) = List.nth (asms, i)
    4.75    |       pr (Thm (prfs, thm)) = (map pr prfs) MRS thm
    4.76    in pr end;
    4.77  
    4.78  (* Internal datatype for inequalities *)
    4.79 -datatype less 
    4.80 -   = Less  of term * term * proof 
    4.81 +datatype less
    4.82 +   = Less  of term * term * proof
    4.83     | Le    of term * term * proof
    4.84 -   | NotEq of term * term * proof; 
    4.85 +   | NotEq of term * term * proof;
    4.86  
    4.87   (* Misc functions for datatype less *)
    4.88  fun lower (Less (x, _, _)) = x
    4.89 @@ -125,13 +120,13 @@
    4.90  
    4.91  fun mkasm_trans sign (t, n) =
    4.92    case Less.decomp_trans sign t of
    4.93 -    SOME (x, rel, y) => 
    4.94 +    SOME (x, rel, y) =>
    4.95      (case rel of
    4.96       "<="  =>  [Le (x, y, Asm n)]
    4.97      | _     => error ("trans_tac: unknown relation symbol ``" ^ rel ^
    4.98                   "''returned by decomp_trans."))
    4.99    | NONE => [];
   4.100 -  
   4.101 +
   4.102  (* ************************************************************************ *)
   4.103  (*                                                                          *)
   4.104  (* mkasm_quasi sign (t, n) : theory -> (Term.term * int) -> less            *)
   4.105 @@ -145,15 +140,15 @@
   4.106  fun mkasm_quasi sign (t, n) =
   4.107    case Less.decomp_quasi sign t of
   4.108      SOME (x, rel, y) => (case rel of
   4.109 -      "<"   => if (x aconv y) then raise Contr (Thm ([Asm n], Less.less_reflE)) 
   4.110 +      "<"   => if (x aconv y) then raise Contr (Thm ([Asm n], Less.less_reflE))
   4.111                 else [Less (x, y, Asm n)]
   4.112      | "<="  => [Le (x, y, Asm n)]
   4.113      | "="   => [Le (x, y, Thm ([Asm n], Less.eqD1)),
   4.114                  Le (y, x, Thm ([Asm n], Less.eqD2))]
   4.115 -    | "~="  => if (x aconv y) then 
   4.116 +    | "~="  => if (x aconv y) then
   4.117                    raise Contr (Thm ([(Thm ([(Thm ([], Less.le_refl)) ,(Asm n)], Less.le_neq_trans))], Less.less_reflE))
   4.118                 else [ NotEq (x, y, Asm n),
   4.119 -                      NotEq (y, x,Thm ( [Asm n], thm "not_sym"))] 
   4.120 +                      NotEq (y, x,Thm ( [Asm n], thm "not_sym"))]
   4.121      | _     => error ("quasi_tac: unknown relation symbol ``" ^ rel ^
   4.122                   "''returned by decomp_quasi."))
   4.123    | NONE => [];
   4.124 @@ -168,15 +163,15 @@
   4.125  (*                                                                          *)
   4.126  (* ************************************************************************ *)
   4.127  
   4.128 -  
   4.129 +
   4.130  fun mkconcl_trans sign t =
   4.131    case Less.decomp_trans sign t of
   4.132      SOME (x, rel, y) => (case rel of
   4.133 -     "<="  => (Le (x, y, Asm ~1), Asm 0) 
   4.134 +     "<="  => (Le (x, y, Asm ~1), Asm 0)
   4.135      | _  => raise Cannot)
   4.136    | NONE => raise Cannot;
   4.137 -  
   4.138 -  
   4.139 +
   4.140 +
   4.141  (* ************************************************************************ *)
   4.142  (*                                                                          *)
   4.143  (* mkconcl_quasi sign t : theory -> Term.term -> less                       *)
   4.144 @@ -194,8 +189,8 @@
   4.145      | "~="  => ([NotEq (x,y, Asm ~1)], Asm 0)
   4.146      | _  => raise Cannot)
   4.147  | NONE => raise Cannot;
   4.148 -  
   4.149 -  
   4.150 +
   4.151 +
   4.152  (* ******************************************************************* *)
   4.153  (*                                                                     *)
   4.154  (* mergeLess (less1,less2):  less * less -> less                       *)
   4.155 @@ -211,11 +206,11 @@
   4.156  fun mergeLess (Le (x, _, p) , Le (_ , z, q)) =
   4.157        Le (x, z, Thm ([p,q] , Less.le_trans))
   4.158  |   mergeLess (Le (x, z, p) , NotEq (x', z', q)) =
   4.159 -      if (x aconv x' andalso z aconv z' ) 
   4.160 +      if (x aconv x' andalso z aconv z' )
   4.161         then Less (x, z, Thm ([p,q] , Less.le_neq_trans))
   4.162          else error "quasi_tac: internal error le_neq_trans"
   4.163  |   mergeLess (NotEq (x, z, p) , Le (x' , z', q)) =
   4.164 -      if (x aconv x' andalso z aconv z') 
   4.165 +      if (x aconv x' andalso z aconv z')
   4.166        then Less (x, z, Thm ([p,q] , Less.neq_le_trans))
   4.167        else error "quasi_tac: internal error neq_le_trans"
   4.168  |   mergeLess (_, _) =
   4.169 @@ -229,7 +224,7 @@
   4.170  infix tr;
   4.171  fun (Le (_, y, _))   tr (Le (x', _, _))   = ( y aconv x' )
   4.172    | _ tr _ = false;
   4.173 -  
   4.174 +
   4.175  (* ******************************************************************* *)
   4.176  (*                                                                     *)
   4.177  (* transPath (Lesslist, Less): (less list * less) -> less              *)
   4.178 @@ -245,7 +240,7 @@
   4.179  |   transPath (x::xs,lesss) =
   4.180        if lesss tr x then transPath (xs, mergeLess(lesss,x))
   4.181        else error "trans/quasi_tac: internal error transpath";
   4.182 -  
   4.183 +
   4.184  (* ******************************************************************* *)
   4.185  (*                                                                     *)
   4.186  (* less1 subsumes less2 : less -> less -> bool                         *)
   4.187 @@ -253,7 +248,7 @@
   4.188  (* subsumes checks whether less1 implies less2                         *)
   4.189  (*                                                                     *)
   4.190  (* ******************************************************************* *)
   4.191 -  
   4.192 +
   4.193  infix subsumes;
   4.194  fun (Le (x, y, _)) subsumes (Le (x', y', _)) =
   4.195        (x aconv x' andalso y aconv y')
   4.196 @@ -271,7 +266,7 @@
   4.197  (* ******************************************************************* *)
   4.198  
   4.199  fun triv_solv (Le (x, x', _)) =
   4.200 -    if x aconv x' then  SOME (Thm ([], Less.le_refl)) 
   4.201 +    if x aconv x' then  SOME (Thm ([], Less.le_refl))
   4.202      else NONE
   4.203  |   triv_solv _ = NONE;
   4.204  
   4.205 @@ -286,33 +281,33 @@
   4.206  fun addEdge (v,d,[]) = [(v,d)]
   4.207  |   addEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el)
   4.208      else (u,dl):: (addEdge(v,d,el));
   4.209 -    
   4.210 +
   4.211  (* ********************************************************************** *)
   4.212  (*                                                                        *)
   4.213 -(* mkQuasiGraph constructs from a list of objects of type less a graph g, *) 
   4.214 +(* mkQuasiGraph constructs from a list of objects of type less a graph g, *)
   4.215  (* by taking all edges that are candidate for a <=, and a list neqE, by   *)
   4.216  (* taking all edges that are candiate for a ~=                            *)
   4.217  (*                                                                        *)
   4.218  (* ********************************************************************** *)
   4.219  
   4.220  fun mkQuasiGraph [] = ([],[])
   4.221 -|   mkQuasiGraph lessList = 
   4.222 +|   mkQuasiGraph lessList =
   4.223   let
   4.224   fun buildGraphs ([],leG, neqE) = (leG,  neqE)
   4.225 -  |   buildGraphs (l::ls, leG,  neqE) = case l of 
   4.226 +  |   buildGraphs (l::ls, leG,  neqE) = case l of
   4.227         (Less (x,y,p)) =>
   4.228 -         let 
   4.229 -	  val leEdge  = Le (x,y, Thm ([p], Less.less_imp_le)) 
   4.230 -	  val neqEdges = [ NotEq (x,y, Thm ([p], Less.less_imp_neq)),
   4.231 -	                   NotEq (y,x, Thm ( [Thm ([p], Less.less_imp_neq)], thm "not_sym"))]
   4.232 -	 in
   4.233 -           buildGraphs (ls, addEdge(y,[],(addEdge (x,[(y,leEdge)],leG))), neqEdges@neqE) 
   4.234 -	 end
   4.235 -     |  (Le (x,y,p))   => buildGraphs (ls, addEdge(y,[],(addEdge (x,[(y,l)],leG))), neqE) 
   4.236 +         let
   4.237 +          val leEdge  = Le (x,y, Thm ([p], Less.less_imp_le))
   4.238 +          val neqEdges = [ NotEq (x,y, Thm ([p], Less.less_imp_neq)),
   4.239 +                           NotEq (y,x, Thm ( [Thm ([p], Less.less_imp_neq)], thm "not_sym"))]
   4.240 +         in
   4.241 +           buildGraphs (ls, addEdge(y,[],(addEdge (x,[(y,leEdge)],leG))), neqEdges@neqE)
   4.242 +         end
   4.243 +     |  (Le (x,y,p))   => buildGraphs (ls, addEdge(y,[],(addEdge (x,[(y,l)],leG))), neqE)
   4.244       | _ =>  buildGraphs (ls, leG,  l::neqE) ;
   4.245  
   4.246  in buildGraphs (lessList, [],  []) end;
   4.247 -  
   4.248 +
   4.249  (* ********************************************************************** *)
   4.250  (*                                                                        *)
   4.251  (* mkGraph constructs from a list of objects of type less a graph g       *)
   4.252 @@ -321,11 +316,11 @@
   4.253  (* ********************************************************************** *)
   4.254  
   4.255  fun mkGraph [] = []
   4.256 -|   mkGraph lessList = 
   4.257 +|   mkGraph lessList =
   4.258   let
   4.259    fun buildGraph ([],g) = g
   4.260 -  |   buildGraph (l::ls, g) =  buildGraph (ls, (addEdge ((lower l),[((upper l),l)],g))) 
   4.261 -     
   4.262 +  |   buildGraph (l::ls, g) =  buildGraph (ls, (addEdge ((lower l),[((upper l),l)],g)))
   4.263 +
   4.264  in buildGraph (lessList, []) end;
   4.265  
   4.266  (* *********************************************************************** *)
   4.267 @@ -335,42 +330,42 @@
   4.268  (* List of successors of u in graph g                                      *)
   4.269  (*                                                                         *)
   4.270  (* *********************************************************************** *)
   4.271 - 
   4.272 -fun adjacent eq_comp ((v,adj)::el) u = 
   4.273 +
   4.274 +fun adjacent eq_comp ((v,adj)::el) u =
   4.275      if eq_comp (u, v) then adj else adjacent eq_comp el u
   4.276 -|   adjacent _  []  _ = []  
   4.277 +|   adjacent _  []  _ = []
   4.278  
   4.279  (* *********************************************************************** *)
   4.280  (*                                                                         *)
   4.281  (* dfs eq_comp g u v:                                                      *)
   4.282  (* ('a * 'a -> bool) -> ('a  *( 'a * less) list) list ->                   *)
   4.283 -(* 'a -> 'a -> (bool * ('a * less) list)                                   *) 
   4.284 +(* 'a -> 'a -> (bool * ('a * less) list)                                   *)
   4.285  (*                                                                         *)
   4.286  (* Depth first search of v from u.                                         *)
   4.287  (* Returns (true, path(u, v)) if successful, otherwise (false, []).        *)
   4.288  (*                                                                         *)
   4.289  (* *********************************************************************** *)
   4.290  
   4.291 -fun dfs eq_comp g u v = 
   4.292 - let 
   4.293 +fun dfs eq_comp g u v =
   4.294 + let
   4.295      val pred = ref nil;
   4.296      val visited = ref nil;
   4.297 -    
   4.298 +
   4.299      fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
   4.300 -    
   4.301 -    fun dfs_visit u' = 
   4.302 +
   4.303 +    fun dfs_visit u' =
   4.304      let val _ = visited := u' :: (!visited)
   4.305 -    
   4.306 +
   4.307      fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end;
   4.308 -    
   4.309 -    in if been_visited v then () 
   4.310 +
   4.311 +    in if been_visited v then ()
   4.312      else (app (fn (v',l) => if been_visited v' then () else (
   4.313 -       update (v',l); 
   4.314 +       update (v',l);
   4.315         dfs_visit v'; ()) )) (adjacent eq_comp g u')
   4.316       end
   4.317 -  in 
   4.318 -    dfs_visit u; 
   4.319 -    if (been_visited v) then (true, (!pred)) else (false , [])   
   4.320 +  in
   4.321 +    dfs_visit u;
   4.322 +    if (been_visited v) then (true, (!pred)) else (false , [])
   4.323    end;
   4.324  
   4.325  (* ************************************************************************ *)
   4.326 @@ -393,8 +388,8 @@
   4.327  (* ************************************************************************ *)
   4.328  
   4.329  
   4.330 - fun findPath x y g = 
   4.331 -  let 
   4.332 + fun findPath x y g =
   4.333 +  let
   4.334      val (found, tmp) =  dfs (op aconv) g x y ;
   4.335      val pred = map snd tmp;
   4.336  
   4.337 @@ -403,38 +398,38 @@
   4.338         (* find predecessor u of node v and the edge u -> v *)
   4.339         fun lookup v [] = raise Cannot
   4.340         |   lookup v (e::es) = if (upper e) aconv v then e else lookup v es;
   4.341 -		
   4.342 -       (* traverse path backwards and return list of visited edges *)   
   4.343 -       fun rev_path v = 
   4.344 - 	let val l = lookup v pred
   4.345 +
   4.346 +       (* traverse path backwards and return list of visited edges *)
   4.347 +       fun rev_path v =
   4.348 +        let val l = lookup v pred
   4.349              val u = lower l;
   4.350 - 	in
   4.351 -           if u aconv x then [l] else (rev_path u) @ [l] 
   4.352 -	end
   4.353 +        in
   4.354 +           if u aconv x then [l] else (rev_path u) @ [l]
   4.355 +        end
   4.356        in rev_path y end;
   4.357 -		
   4.358 -  in 
   4.359 +
   4.360 +  in
   4.361     if found then (
   4.362      if x aconv y then (found,[(Le (x, y, (Thm ([], Less.le_refl))))])
   4.363 -    else (found, (path x y) )) 
   4.364 +    else (found, (path x y) ))
   4.365     else (found,[])
   4.366 -  end; 
   4.367 -	
   4.368 -      
   4.369 -(* ************************************************************************ *) 
   4.370 +  end;
   4.371 +
   4.372 +
   4.373 +(* ************************************************************************ *)
   4.374  (*                                                                          *)
   4.375  (* findQuasiProof (leqG, neqE) subgoal:                                     *)
   4.376  (* (Term.term * (Term.term * less list) list) * less list  -> less -> proof *)
   4.377  (*                                                                          *)
   4.378  (* Constructs a proof for subgoal by searching a special path in leqG and   *)
   4.379 -(* neqE. Raises Cannot if construction of the proof fails.                  *)   
   4.380 +(* neqE. Raises Cannot if construction of the proof fails.                  *)
   4.381  (*                                                                          *)
   4.382 -(* ************************************************************************ *) 
   4.383 +(* ************************************************************************ *)
   4.384  
   4.385  
   4.386  (* As the conlusion can be either of form x <= y, x < y or x ~= y we have        *)
   4.387  (* three cases to deal with. Finding a transitivity path from x to y with label  *)
   4.388 -(* 1. <=                                                                         *) 
   4.389 +(* 1. <=                                                                         *)
   4.390  (*    This is simply done by searching any path from x to y in the graph leG.    *)
   4.391  (*    The graph leG contains only edges with label <=.                           *)
   4.392  (*                                                                               *)
   4.393 @@ -450,54 +445,54 @@
   4.394  
   4.395  fun findQuasiProof (leG, neqE) subgoal =
   4.396    case subgoal of (Le (x,y, _)) => (
   4.397 -   let 
   4.398 -    val (xyLefound,xyLePath) = findPath x y leG 
   4.399 +   let
   4.400 +    val (xyLefound,xyLePath) = findPath x y leG
   4.401     in
   4.402      if xyLefound then (
   4.403 -     let 
   4.404 +     let
   4.405        val Le_x_y = (transPath (tl xyLePath, hd xyLePath))
   4.406       in getprf Le_x_y end )
   4.407      else raise Cannot
   4.408     end )
   4.409    | (Less (x,y,_))  => (
   4.410 -   let 
   4.411 +   let
   4.412      fun findParallelNeq []  = NONE
   4.413      |   findParallelNeq (e::es)  =
   4.414       if      (x aconv (lower e) andalso y aconv (upper e)) then SOME e
   4.415       else if (y aconv (lower e) andalso x aconv (upper e)) then SOME (NotEq (x,y, (Thm ([getprf e], thm "not_sym"))))
   4.416 -     else findParallelNeq es ;  
   4.417 +     else findParallelNeq es ;
   4.418     in
   4.419     (* test if there is a edge x ~= y respectivly  y ~= x and     *)
   4.420     (* if it possible to find a path x <= y in leG, thus we can conclude x < y *)
   4.421 -    (case findParallelNeq neqE of (SOME e) => 
   4.422 -      let 
   4.423 -       val (xyLeFound,xyLePath) = findPath x y leG 
   4.424 +    (case findParallelNeq neqE of (SOME e) =>
   4.425 +      let
   4.426 +       val (xyLeFound,xyLePath) = findPath x y leG
   4.427        in
   4.428         if xyLeFound then (
   4.429 -        let 
   4.430 +        let
   4.431           val Le_x_y = (transPath (tl xyLePath, hd xyLePath))
   4.432           val Less_x_y = mergeLess (e, Le_x_y)
   4.433          in getprf Less_x_y end
   4.434         ) else raise Cannot
   4.435 -      end 
   4.436 -    | _ => raise Cannot)    
   4.437 +      end
   4.438 +    | _ => raise Cannot)
   4.439     end )
   4.440 - | (NotEq (x,y,_)) => 
   4.441 + | (NotEq (x,y,_)) =>
   4.442    (* First check if a single premiss is sufficient *)
   4.443    (case (Library.find_first (fn fact => fact subsumes subgoal) neqE, subgoal) of
   4.444      (SOME (NotEq (x, y, p)), NotEq (x', y', _)) =>
   4.445 -      if  (x aconv x' andalso y aconv y') then p 
   4.446 +      if  (x aconv x' andalso y aconv y') then p
   4.447        else Thm ([p], thm "not_sym")
   4.448 -    | _  => raise Cannot 
   4.449 +    | _  => raise Cannot
   4.450    )
   4.451  
   4.452 -      
   4.453 -(* ************************************************************************ *) 
   4.454 -(*                                                                          *) 
   4.455 -(* End: Quasi Order relevant functions                                      *) 
   4.456 -(*                                                                          *) 
   4.457 -(*                                                                          *) 
   4.458 -(* ************************************************************************ *) 
   4.459 +
   4.460 +(* ************************************************************************ *)
   4.461 +(*                                                                          *)
   4.462 +(* End: Quasi Order relevant functions                                      *)
   4.463 +(*                                                                          *)
   4.464 +(*                                                                          *)
   4.465 +(* ************************************************************************ *)
   4.466  
   4.467  (* *********************************************************************** *)
   4.468  (*                                                                         *)
   4.469 @@ -509,14 +504,14 @@
   4.470  (* *********************************************************************** *)
   4.471  
   4.472  fun solveLeTrans sign (asms, concl) =
   4.473 - let 
   4.474 + let
   4.475    val g = mkGraph asms
   4.476   in
   4.477 -   let 
   4.478 +   let
   4.479      val (subgoal, prf) = mkconcl_trans sign concl
   4.480 -    val (found, path) = findPath (lower subgoal) (upper subgoal) g 
   4.481 +    val (found, path) = findPath (lower subgoal) (upper subgoal) g
   4.482     in
   4.483 -    if found then [getprf (transPath (tl path, hd path))] 
   4.484 +    if found then [getprf (transPath (tl path, hd path))]
   4.485      else raise Cannot
   4.486    end
   4.487   end;
   4.488 @@ -532,10 +527,10 @@
   4.489  (* *********************************************************************** *)
   4.490  
   4.491  fun solveQuasiOrder sign (asms, concl) =
   4.492 - let 
   4.493 + let
   4.494    val (leG, neqE) = mkQuasiGraph asms
   4.495   in
   4.496 -   let 
   4.497 +   let
   4.498     val (subgoals, prf) = mkconcl_quasi sign concl
   4.499     fun solve facts less =
   4.500         (case triv_solv less of NONE => findQuasiProof (leG, neqE) less
   4.501 @@ -543,54 +538,56 @@
   4.502    in   map (solve asms) subgoals end
   4.503   end;
   4.504  
   4.505 -(* ************************************************************************ *) 
   4.506 -(*                                                                          *) 
   4.507 +(* ************************************************************************ *)
   4.508 +(*                                                                          *)
   4.509  (* Tactics                                                                  *)
   4.510  (*                                                                          *)
   4.511 -(*  - trans_tac                                                          *)                     
   4.512 -(*  - quasi_tac, solves quasi orders                                        *)                     
   4.513 -(* ************************************************************************ *) 
   4.514 +(*  - trans_tac                                                          *)
   4.515 +(*  - quasi_tac, solves quasi orders                                        *)
   4.516 +(* ************************************************************************ *)
   4.517  
   4.518  
   4.519  (* trans_tac - solves transitivity chains over <= *)
   4.520 -val trans_tac  =  SUBGOAL (fn (A, n, sign) =>
   4.521 +
   4.522 +fun trans_tac ctxt = SUBGOAL (fn (A, n) =>
   4.523   let
   4.524 -  val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A))
   4.525 -  val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
   4.526 -  val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
   4.527 -  val lesss = List.concat (ListPair.map (mkasm_trans  sign) (Hs, 0 upto (length Hs - 1)))
   4.528 -  val prfs = solveLeTrans  sign (lesss, C);
   4.529 -  
   4.530 -  val (subgoal, prf) = mkconcl_trans  sign C;
   4.531 +  val thy = ProofContext.theory_of ctxt;
   4.532 +  val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A));
   4.533 +  val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A);
   4.534 +  val C = subst_bounds (rfrees, Logic.strip_assums_concl A);
   4.535 +  val lesss = List.concat (ListPair.map (mkasm_trans thy) (Hs, 0 upto (length Hs - 1)));
   4.536 +  val prfs = solveLeTrans thy (lesss, C);
   4.537 +
   4.538 +  val (subgoal, prf) = mkconcl_trans thy C;
   4.539   in
   4.540 -  
   4.541 -  METAHYPS (fn asms =>
   4.542 -    let val thms = map (prove asms) prfs
   4.543 -    in rtac (prove thms prf) 1 end) n
   4.544 -  
   4.545 +  FOCUS (fn {prems, ...} =>
   4.546 +    let val thms = map (prove prems) prfs
   4.547 +    in rtac (prove thms prf) 1 end) ctxt n
   4.548   end
   4.549 - handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n
   4.550 -      | Cannot  => no_tac
   4.551 -);
   4.552 + handle Contr p => FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n
   4.553 +  | Cannot  => no_tac);
   4.554 +
   4.555  
   4.556  (* quasi_tac - solves quasi orders *)
   4.557 -val quasi_tac = SUBGOAL (fn (A, n, sign) =>
   4.558 +
   4.559 +fun quasi_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
   4.560   let
   4.561 -  val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A))
   4.562 -  val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
   4.563 -  val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
   4.564 -  val lesss = List.concat (ListPair.map (mkasm_quasi sign) (Hs, 0 upto (length Hs - 1)))
   4.565 -  val prfs = solveQuasiOrder sign (lesss, C);
   4.566 -  val (subgoals, prf) = mkconcl_quasi sign C;
   4.567 +  val thy = ProofContext.theory_of ctxt;
   4.568 +  val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A));
   4.569 +  val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A);
   4.570 +  val C = subst_bounds (rfrees, Logic.strip_assums_concl A);
   4.571 +  val lesss = flat (ListPair.map (mkasm_quasi thy) (Hs, 0 upto (length Hs - 1)));
   4.572 +  val prfs = solveQuasiOrder thy (lesss, C);
   4.573 +  val (subgoals, prf) = mkconcl_quasi thy C;
   4.574   in
   4.575 - 
   4.576 -  METAHYPS (fn asms =>
   4.577 -    let val thms = map (prove asms) prfs
   4.578 -    in rtac (prove thms prf) 1 end) n
   4.579 - 
   4.580 +  FOCUS (fn {prems, ...} =>
   4.581 +    let val thms = map (prove prems) prfs
   4.582 +    in rtac (prove thms prf) 1 end) ctxt n st
   4.583   end
   4.584 - handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n
   4.585 -      | Cannot  => no_tac
   4.586 -);
   4.587 -   
   4.588 + handle Contr p =>
   4.589 +    (FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n st
   4.590 +      handle Subscript => Seq.empty)
   4.591 +  | Cannot => Seq.empty
   4.592 +  | Subscript => Seq.empty);
   4.593 +
   4.594  end;
     5.1 --- a/src/Provers/trancl.ML	Sun Jul 26 22:24:13 2009 +0200
     5.2 +++ b/src/Provers/trancl.ML	Sun Jul 26 22:28:31 2009 +0200
     5.3 @@ -26,7 +26,7 @@
     5.4  
     5.5  *)
     5.6  
     5.7 -signature TRANCL_ARITH = 
     5.8 +signature TRANCL_ARITH =
     5.9  sig
    5.10  
    5.11    (* theorems for transitive closure *)
    5.12 @@ -63,25 +63,25 @@
    5.13              "r":   the relation itself,
    5.14              "r^+": transitive closure of the relation,
    5.15              "r^*": reflexive-transitive closure of the relation
    5.16 -  *)  
    5.17 +  *)
    5.18  
    5.19 -  val decomp: term ->  (term * term * term * string) option 
    5.20 +  val decomp: term ->  (term * term * term * string) option
    5.21  
    5.22  end;
    5.23  
    5.24 -signature TRANCL_TAC = 
    5.25 +signature TRANCL_TAC =
    5.26  sig
    5.27 -  val trancl_tac: int -> tactic;
    5.28 -  val rtrancl_tac: int -> tactic;
    5.29 +  val trancl_tac: Proof.context -> int -> tactic
    5.30 +  val rtrancl_tac: Proof.context -> int -> tactic
    5.31  end;
    5.32  
    5.33 -functor Trancl_Tac_Fun (Cls : TRANCL_ARITH): TRANCL_TAC = 
    5.34 +functor Trancl_Tac(Cls: TRANCL_ARITH): TRANCL_TAC =
    5.35  struct
    5.36  
    5.37 - 
    5.38 +
    5.39  datatype proof
    5.40 -  = Asm of int 
    5.41 -  | Thm of proof list * thm; 
    5.42 +  = Asm of int
    5.43 +  | Thm of proof list * thm;
    5.44  
    5.45  exception Cannot; (* internal exception: raised if no proof can be found *)
    5.46  
    5.47 @@ -89,7 +89,7 @@
    5.48    (Envir.beta_eta_contract x, Envir.beta_eta_contract y,
    5.49     Envir.beta_eta_contract rel, r)) (Cls.decomp t);
    5.50  
    5.51 -fun prove thy r asms = 
    5.52 +fun prove thy r asms =
    5.53    let
    5.54      fun inst thm =
    5.55        let val SOME (_, _, r', _) = decomp (concl_of thm)
    5.56 @@ -98,12 +98,12 @@
    5.57        | pr (Thm (prfs, thm)) = map pr prfs MRS inst thm
    5.58    in pr end;
    5.59  
    5.60 -  
    5.61 +
    5.62  (* Internal datatype for inequalities *)
    5.63 -datatype rel 
    5.64 +datatype rel
    5.65     = Trans  of term * term * proof  (* R^+ *)
    5.66     | RTrans of term * term * proof; (* R^* *)
    5.67 -   
    5.68 +
    5.69   (* Misc functions for datatype rel *)
    5.70  fun lower (Trans (x, _, _)) = x
    5.71    | lower (RTrans (x,_,_)) = x;
    5.72 @@ -112,8 +112,8 @@
    5.73    | upper (RTrans (_,y,_)) = y;
    5.74  
    5.75  fun getprf   (Trans   (_, _, p)) = p
    5.76 -|   getprf   (RTrans (_,_, p)) = p; 
    5.77 - 
    5.78 +|   getprf   (RTrans (_,_, p)) = p;
    5.79 +
    5.80  (* ************************************************************************ *)
    5.81  (*                                                                          *)
    5.82  (*  mkasm_trancl Rel (t,n): term -> (term , int) -> rel list                *)
    5.83 @@ -127,16 +127,16 @@
    5.84  
    5.85  fun mkasm_trancl  Rel  (t, n) =
    5.86    case decomp t of
    5.87 -    SOME (x, y, rel,r) => if rel aconv Rel then  
    5.88 -    
    5.89 +    SOME (x, y, rel,r) => if rel aconv Rel then
    5.90 +
    5.91      (case r of
    5.92        "r"   => [Trans (x,y, Thm([Asm n], Cls.r_into_trancl))]
    5.93      | "r+"  => [Trans (x,y, Asm n)]
    5.94      | "r*"  => []
    5.95      | _     => error ("trancl_tac: unknown relation symbol"))
    5.96 -    else [] 
    5.97 +    else []
    5.98    | NONE => [];
    5.99 -  
   5.100 +
   5.101  (* ************************************************************************ *)
   5.102  (*                                                                          *)
   5.103  (*  mkasm_rtrancl Rel (t,n): term -> (term , int) -> rel list               *)
   5.104 @@ -156,7 +156,7 @@
   5.105      | "r+"  => [ Trans (x,y, Asm n)]
   5.106      | "r*"  => [ RTrans(x,y, Asm n)]
   5.107      | _     => error ("rtrancl_tac: unknown relation symbol" ))
   5.108 -   else [] 
   5.109 +   else []
   5.110    | NONE => [];
   5.111  
   5.112  (* ************************************************************************ *)
   5.113 @@ -204,7 +204,7 @@
   5.114  fun makeStep (Trans (a,_,p), Trans(_,c,q))  = Trans (a,c, Thm ([p,q], Cls.trancl_trans))
   5.115  (* refl. + trans. cls. rules *)
   5.116  |   makeStep (RTrans (a,_,p), Trans(_,c,q))  = Trans (a,c, Thm ([p,q], Cls.rtrancl_trancl_trancl))
   5.117 -|   makeStep (Trans (a,_,p), RTrans(_,c,q))  = Trans (a,c, Thm ([p,q], Cls.trancl_rtrancl_trancl))   
   5.118 +|   makeStep (Trans (a,_,p), RTrans(_,c,q))  = Trans (a,c, Thm ([p,q], Cls.trancl_rtrancl_trancl))
   5.119  |   makeStep (RTrans (a,_,p), RTrans(_,c,q))  = RTrans (a,c, Thm ([p,q], Cls.rtrancl_trans));
   5.120  
   5.121  (* ******************************************************************* *)
   5.122 @@ -220,7 +220,7 @@
   5.123  
   5.124  fun transPath ([],acc) = acc
   5.125  |   transPath (x::xs,acc) = transPath (xs, makeStep(acc,x))
   5.126 -      
   5.127 +
   5.128  (* ********************************************************************* *)
   5.129  (* Graph functions                                                       *)
   5.130  (* ********************************************************************* *)
   5.131 @@ -232,7 +232,7 @@
   5.132  fun addEdge (v,d,[]) = [(v,d)]
   5.133  |   addEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el)
   5.134      else (u,dl):: (addEdge(v,d,el));
   5.135 -    
   5.136 +
   5.137  (* ********************************************************************** *)
   5.138  (*                                                                        *)
   5.139  (* mkGraph constructs from a list of objects of type rel  a graph g       *)
   5.140 @@ -241,13 +241,13 @@
   5.141  (* ********************************************************************** *)
   5.142  
   5.143  fun mkGraph [] = ([],[])
   5.144 -|   mkGraph ys =  
   5.145 +|   mkGraph ys =
   5.146   let
   5.147    fun buildGraph ([],g,zs) = (g,zs)
   5.148 -  |   buildGraph (x::xs, g, zs) = 
   5.149 -        case x of (Trans (_,_,_)) => 
   5.150 -	       buildGraph (xs, addEdge((upper x), [],(addEdge ((lower x),[((upper x),x)],g))), x::zs) 
   5.151 -	| _ => buildGraph (xs, addEdge((upper x), [],(addEdge ((lower x),[((upper x),x)],g))), zs)
   5.152 +  |   buildGraph (x::xs, g, zs) =
   5.153 +        case x of (Trans (_,_,_)) =>
   5.154 +               buildGraph (xs, addEdge((upper x), [],(addEdge ((lower x),[((upper x),x)],g))), x::zs)
   5.155 +        | _ => buildGraph (xs, addEdge((upper x), [],(addEdge ((lower x),[((upper x),x)],g))), zs)
   5.156  in buildGraph (ys, [], []) end;
   5.157  
   5.158  (* *********************************************************************** *)
   5.159 @@ -257,42 +257,42 @@
   5.160  (* List of successors of u in graph g                                      *)
   5.161  (*                                                                         *)
   5.162  (* *********************************************************************** *)
   5.163 - 
   5.164 -fun adjacent eq_comp ((v,adj)::el) u = 
   5.165 +
   5.166 +fun adjacent eq_comp ((v,adj)::el) u =
   5.167      if eq_comp (u, v) then adj else adjacent eq_comp el u
   5.168 -|   adjacent _  []  _ = []  
   5.169 +|   adjacent _  []  _ = []
   5.170  
   5.171  (* *********************************************************************** *)
   5.172  (*                                                                         *)
   5.173  (* dfs eq_comp g u v:                                                      *)
   5.174  (* ('a * 'a -> bool) -> ('a  *( 'a * rel) list) list ->                    *)
   5.175 -(* 'a -> 'a -> (bool * ('a * rel) list)                                    *) 
   5.176 +(* 'a -> 'a -> (bool * ('a * rel) list)                                    *)
   5.177  (*                                                                         *)
   5.178  (* Depth first search of v from u.                                         *)
   5.179  (* Returns (true, path(u, v)) if successful, otherwise (false, []).        *)
   5.180  (*                                                                         *)
   5.181  (* *********************************************************************** *)
   5.182  
   5.183 -fun dfs eq_comp g u v = 
   5.184 - let 
   5.185 +fun dfs eq_comp g u v =
   5.186 + let
   5.187      val pred = ref nil;
   5.188      val visited = ref nil;
   5.189 -    
   5.190 +
   5.191      fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
   5.192 -    
   5.193 -    fun dfs_visit u' = 
   5.194 +
   5.195 +    fun dfs_visit u' =
   5.196      let val _ = visited := u' :: (!visited)
   5.197 -    
   5.198 +
   5.199      fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end;
   5.200 -    
   5.201 -    in if been_visited v then () 
   5.202 +
   5.203 +    in if been_visited v then ()
   5.204      else (app (fn (v',l) => if been_visited v' then () else (
   5.205 -       update (v',l); 
   5.206 +       update (v',l);
   5.207         dfs_visit v'; ()) )) (adjacent eq_comp g u')
   5.208       end
   5.209 -  in 
   5.210 -    dfs_visit u; 
   5.211 -    if (been_visited v) then (true, (!pred)) else (false , [])   
   5.212 +  in
   5.213 +    dfs_visit u;
   5.214 +    if (been_visited v) then (true, (!pred)) else (false , [])
   5.215    end;
   5.216  
   5.217  (* *********************************************************************** *)
   5.218 @@ -310,7 +310,7 @@
   5.219     (* Compute list of reversed edges for each adjacency list *)
   5.220     fun flip (u,(v,l)::el) = (v,(u,l)) :: flip (u,el)
   5.221       | flip (_,nil) = nil
   5.222 -   
   5.223 +
   5.224     (* Compute adjacency list for node u from the list of edges
   5.225        and return a likewise reduced list of edges.  The list of edges
   5.226        is searches for edges starting from u, and these edges are removed. *)
   5.227 @@ -334,23 +334,23 @@
   5.228     (* Compute, for each adjacency list, the list with reversed edges,
   5.229        and concatenate these lists. *)
   5.230     val flipped = List.foldr (op @) nil (map flip g)
   5.231 - 
   5.232 - in assemble g flipped end    
   5.233 - 
   5.234 +
   5.235 + in assemble g flipped end
   5.236 +
   5.237  (* *********************************************************************** *)
   5.238  (*                                                                         *)
   5.239  (* dfs_reachable eq_comp g u:                                              *)
   5.240 -(* (int * int list) list -> int -> int list                                *) 
   5.241 +(* (int * int list) list -> int -> int list                                *)
   5.242  (*                                                                         *)
   5.243  (* Computes list of all nodes reachable from u in g.                       *)
   5.244  (*                                                                         *)
   5.245  (* *********************************************************************** *)
   5.246  
   5.247 -fun dfs_reachable eq_comp g u = 
   5.248 +fun dfs_reachable eq_comp g u =
   5.249   let
   5.250    (* List of vertices which have been visited. *)
   5.251    val visited  = ref nil;
   5.252 -  
   5.253 +
   5.254    fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
   5.255  
   5.256    fun dfs_visit g u  =
   5.257 @@ -361,13 +361,13 @@
   5.258              else v :: dfs_visit g v @ ds)
   5.259          nil (adjacent eq_comp g u)
   5.260     in  descendents end
   5.261 - 
   5.262 +
   5.263   in u :: dfs_visit g u end;
   5.264  
   5.265  (* *********************************************************************** *)
   5.266  (*                                                                         *)
   5.267  (* dfs_term_reachable g u:                                                  *)
   5.268 -(* (term * term list) list -> term -> term list                            *) 
   5.269 +(* (term * term list) list -> term -> term list                            *)
   5.270  (*                                                                         *)
   5.271  (* Computes list of all nodes reachable from u in g.                       *)
   5.272  (*                                                                         *)
   5.273 @@ -375,45 +375,45 @@
   5.274  
   5.275  fun dfs_term_reachable g u = dfs_reachable (op aconv) g u;
   5.276  
   5.277 -(* ************************************************************************ *) 
   5.278 +(* ************************************************************************ *)
   5.279  (*                                                                          *)
   5.280  (* findPath x y g: Term.term -> Term.term ->                                *)
   5.281 -(*                  (Term.term * (Term.term * rel list) list) ->            *) 
   5.282 +(*                  (Term.term * (Term.term * rel list) list) ->            *)
   5.283  (*                  (bool, rel list)                                        *)
   5.284  (*                                                                          *)
   5.285  (*  Searches a path from vertex x to vertex y in Graph g, returns true and  *)
   5.286  (*  the list of edges if path is found, otherwise false and nil.            *)
   5.287  (*                                                                          *)
   5.288 -(* ************************************************************************ *) 
   5.289 - 
   5.290 -fun findPath x y g = 
   5.291 -  let 
   5.292 +(* ************************************************************************ *)
   5.293 +
   5.294 +fun findPath x y g =
   5.295 +  let
   5.296     val (found, tmp) =  dfs (op aconv) g x y ;
   5.297     val pred = map snd tmp;
   5.298 -	 
   5.299 +
   5.300     fun path x y  =
   5.301      let
   5.302 -	 (* find predecessor u of node v and the edge u -> v *)
   5.303 -		
   5.304 +         (* find predecessor u of node v and the edge u -> v *)
   5.305 +
   5.306        fun lookup v [] = raise Cannot
   5.307        |   lookup v (e::es) = if (upper e) aconv v then e else lookup v es;
   5.308 -		
   5.309 -      (* traverse path backwards and return list of visited edges *)   
   5.310 -      fun rev_path v = 
   5.311 -	let val l = lookup v pred
   5.312 -	    val u = lower l;
   5.313 -	in
   5.314 -	  if u aconv x then [l] else (rev_path u) @ [l] 
   5.315 -	end
   5.316 -       
   5.317 +
   5.318 +      (* traverse path backwards and return list of visited edges *)
   5.319 +      fun rev_path v =
   5.320 +        let val l = lookup v pred
   5.321 +            val u = lower l;
   5.322 +        in
   5.323 +          if u aconv x then [l] else (rev_path u) @ [l]
   5.324 +        end
   5.325 +
   5.326      in rev_path y end;
   5.327 -		
   5.328 -   in 
   5.329 +
   5.330 +   in
   5.331 +
   5.332  
   5.333 -     
   5.334        if found then ( (found, (path x y) )) else (found,[])
   5.335 -   
   5.336 -     
   5.337 +
   5.338 +
   5.339  
   5.340     end;
   5.341  
   5.342 @@ -426,143 +426,142 @@
   5.343  (*                                                                          *)
   5.344  (* ************************************************************************ *)
   5.345  
   5.346 -fun findRtranclProof g tranclEdges subgoal = 
   5.347 +fun findRtranclProof g tranclEdges subgoal =
   5.348     case subgoal of (RTrans (x,y,_)) => if x aconv y then [Thm ([], Cls.rtrancl_refl)] else (
   5.349       let val (found, path) = findPath (lower subgoal) (upper subgoal) g
   5.350 -     in 
   5.351 +     in
   5.352         if found then (
   5.353            let val path' = (transPath (tl path, hd path))
   5.354 -	  in 
   5.355 -	   
   5.356 -	    case path' of (Trans (_,_,p)) => [Thm ([p], Cls.trancl_into_rtrancl )] 
   5.357 -	    | _ => [getprf path']
   5.358 -	   
   5.359 -	  end
   5.360 +          in
   5.361 +
   5.362 +            case path' of (Trans (_,_,p)) => [Thm ([p], Cls.trancl_into_rtrancl )]
   5.363 +            | _ => [getprf path']
   5.364 +
   5.365 +          end
   5.366         )
   5.367         else raise Cannot
   5.368       end
   5.369     )
   5.370 -   
   5.371 +
   5.372  | (Trans (x,y,_)) => (
   5.373 - 
   5.374 +
   5.375    let
   5.376     val Vx = dfs_term_reachable g x;
   5.377     val g' = transpose (op aconv) g;
   5.378     val Vy = dfs_term_reachable g' y;
   5.379 -   
   5.380 +
   5.381     fun processTranclEdges [] = raise Cannot
   5.382 -   |   processTranclEdges (e::es) = 
   5.383 +   |   processTranclEdges (e::es) =
   5.384            if (upper e) mem Vx andalso (lower e) mem Vx
   5.385 -	  andalso (upper e) mem Vy andalso (lower e) mem Vy
   5.386 -	  then (
   5.387 -	      
   5.388 -	   
   5.389 -	    if (lower e) aconv x then (
   5.390 -	      if (upper e) aconv y then (
   5.391 -	          [(getprf e)] 
   5.392 -	      )
   5.393 -	      else (
   5.394 -	          let 
   5.395 -		    val (found,path) = findPath (upper e) y g
   5.396 -		  in
   5.397 +          andalso (upper e) mem Vy andalso (lower e) mem Vy
   5.398 +          then (
   5.399 +
   5.400 +
   5.401 +            if (lower e) aconv x then (
   5.402 +              if (upper e) aconv y then (
   5.403 +                  [(getprf e)]
   5.404 +              )
   5.405 +              else (
   5.406 +                  let
   5.407 +                    val (found,path) = findPath (upper e) y g
   5.408 +                  in
   5.409 +
   5.410 +                   if found then (
   5.411 +                       [getprf (transPath (path, e))]
   5.412 +                      ) else processTranclEdges es
   5.413 +
   5.414 +                  end
   5.415 +              )
   5.416 +            )
   5.417 +            else if (upper e) aconv y then (
   5.418 +               let val (xufound,xupath) = findPath x (lower e) g
   5.419 +               in
   5.420 +
   5.421 +                  if xufound then (
   5.422  
   5.423 -		   if found then ( 
   5.424 -		       [getprf (transPath (path, e))]
   5.425 -		      ) else processTranclEdges es
   5.426 -		  
   5.427 -		  end 
   5.428 -	      )   
   5.429 -	    )
   5.430 -	    else if (upper e) aconv y then (
   5.431 -	       let val (xufound,xupath) = findPath x (lower e) g
   5.432 -	       in 
   5.433 -	       
   5.434 -	          if xufound then (
   5.435 -		  	    
   5.436 -		    let val xuRTranclEdge = transPath (tl xupath, hd xupath)
   5.437 -			    val xyTranclEdge = makeStep(xuRTranclEdge,e)
   5.438 -				
   5.439 -				in [getprf xyTranclEdge] end
   5.440 -				
   5.441 -	         ) else processTranclEdges es
   5.442 -	       
   5.443 -	       end
   5.444 -	    )
   5.445 -	    else ( 
   5.446 -	   
   5.447 -	        let val (xufound,xupath) = findPath x (lower e) g
   5.448 -		    val (vyfound,vypath) = findPath (upper e) y g
   5.449 -		 in 
   5.450 -		    if xufound then (
   5.451 -		         if vyfound then ( 
   5.452 -			    let val xuRTranclEdge = transPath (tl xupath, hd xupath)
   5.453 -			        val vyRTranclEdge = transPath (tl vypath, hd vypath)
   5.454 -				val xyTranclEdge = makeStep (makeStep(xuRTranclEdge,e),vyRTranclEdge)
   5.455 -				
   5.456 -				in [getprf xyTranclEdge] end
   5.457 -				
   5.458 -			 ) else processTranclEdges es
   5.459 -		    ) 
   5.460 -		    else processTranclEdges es
   5.461 -		 end
   5.462 -	    )
   5.463 -	  )
   5.464 -	  else processTranclEdges es;
   5.465 +                    let val xuRTranclEdge = transPath (tl xupath, hd xupath)
   5.466 +                            val xyTranclEdge = makeStep(xuRTranclEdge,e)
   5.467 +
   5.468 +                                in [getprf xyTranclEdge] end
   5.469 +
   5.470 +                 ) else processTranclEdges es
   5.471 +
   5.472 +               end
   5.473 +            )
   5.474 +            else (
   5.475 +
   5.476 +                let val (xufound,xupath) = findPath x (lower e) g
   5.477 +                    val (vyfound,vypath) = findPath (upper e) y g
   5.478 +                 in
   5.479 +                    if xufound then (
   5.480 +                         if vyfound then (
   5.481 +                            let val xuRTranclEdge = transPath (tl xupath, hd xupath)
   5.482 +                                val vyRTranclEdge = transPath (tl vypath, hd vypath)
   5.483 +                                val xyTranclEdge = makeStep (makeStep(xuRTranclEdge,e),vyRTranclEdge)
   5.484 +
   5.485 +                                in [getprf xyTranclEdge] end
   5.486 +
   5.487 +                         ) else processTranclEdges es
   5.488 +                    )
   5.489 +                    else processTranclEdges es
   5.490 +                 end
   5.491 +            )
   5.492 +          )
   5.493 +          else processTranclEdges es;
   5.494     in processTranclEdges tranclEdges end )
   5.495  | _ => raise Cannot
   5.496  
   5.497 -   
   5.498 -fun solveTrancl (asms, concl) = 
   5.499 +
   5.500 +fun solveTrancl (asms, concl) =
   5.501   let val (g,_) = mkGraph asms
   5.502   in
   5.503    let val (_, subgoal, _) = mkconcl_trancl concl
   5.504        val (found, path) = findPath (lower subgoal) (upper subgoal) g
   5.505    in
   5.506      if found then  [getprf (transPath (tl path, hd path))]
   5.507 -    else raise Cannot 
   5.508 +    else raise Cannot
   5.509    end
   5.510   end;
   5.511 -  
   5.512 -fun solveRtrancl (asms, concl) = 
   5.513 +
   5.514 +fun solveRtrancl (asms, concl) =
   5.515   let val (g,tranclEdges) = mkGraph asms
   5.516       val (_, subgoal, _) = mkconcl_rtrancl concl
   5.517  in
   5.518    findRtranclProof g tranclEdges subgoal
   5.519  end;
   5.520 - 
   5.521 -   
   5.522 -val trancl_tac =   SUBGOAL (fn (A, n) => fn st =>
   5.523 +
   5.524 +
   5.525 +fun trancl_tac ctxt = SUBGOAL (fn (A, n) =>
   5.526   let
   5.527 -  val thy = theory_of_thm st;
   5.528 +  val thy = ProofContext.theory_of ctxt;
   5.529    val Hs = Logic.strip_assums_hyp A;
   5.530    val C = Logic.strip_assums_concl A;
   5.531 -  val (rel,subgoals, prf) = mkconcl_trancl C;
   5.532 -  val prems = List.concat (ListPair.map (mkasm_trancl rel) (Hs, 0 upto (length Hs - 1)))
   5.533 +  val (rel, subgoals, prf) = mkconcl_trancl C;
   5.534 +
   5.535 +  val prems = flat (ListPair.map (mkasm_trancl rel) (Hs, 0 upto (length Hs - 1)));
   5.536    val prfs = solveTrancl (prems, C);
   5.537 -
   5.538   in
   5.539 -  METAHYPS (fn asms =>
   5.540 -    let val thms = map (prove thy rel asms) prfs
   5.541 -    in rtac (prove thy rel thms prf) 1 end) n st
   5.542 +  FOCUS (fn {prems, ...} =>
   5.543 +    let val thms = map (prove thy rel prems) prfs
   5.544 +    in rtac (prove thy rel thms prf) 1 end) ctxt n
   5.545   end
   5.546 -handle  Cannot  => no_tac st);
   5.547 + handle Cannot => no_tac);
   5.548  
   5.549 - 
   5.550 - 
   5.551 -val rtrancl_tac =   SUBGOAL (fn (A, n) => fn st =>
   5.552 +
   5.553 +fun rtrancl_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
   5.554   let
   5.555 -  val thy = theory_of_thm st;
   5.556 +  val thy = ProofContext.theory_of ctxt;
   5.557    val Hs = Logic.strip_assums_hyp A;
   5.558    val C = Logic.strip_assums_concl A;
   5.559 -  val (rel,subgoals, prf) = mkconcl_rtrancl C;
   5.560 +  val (rel, subgoals, prf) = mkconcl_rtrancl C;
   5.561  
   5.562 -  val prems = List.concat (ListPair.map (mkasm_rtrancl rel) (Hs, 0 upto (length Hs - 1)))
   5.563 +  val prems = flat (ListPair.map (mkasm_rtrancl rel) (Hs, 0 upto (length Hs - 1)));
   5.564    val prfs = solveRtrancl (prems, C);
   5.565   in
   5.566 -  METAHYPS (fn asms =>
   5.567 -    let val thms = map (prove thy rel asms) prfs
   5.568 -    in rtac (prove thy rel thms prf) 1 end) n st
   5.569 +  FOCUS (fn {prems, ...} =>
   5.570 +    let val thms = map (prove thy rel prems) prfs
   5.571 +    in rtac (prove thy rel thms prf) 1 end) ctxt n st
   5.572   end
   5.573 -handle  Cannot  => no_tac st);
   5.574 + handle Cannot => Seq.empty | Subscript => Seq.empty);
   5.575  
   5.576  end;