src/Tools/Metis/src/Rule.sml

clarified signature;

(* ========================================================================= *)
(* DERIVED RULES FOR CREATING FIRST ORDER LOGIC THEOREMS                     *)
(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License     *)
(* ========================================================================= *)

structure Rule :> Rule =
struct

open Useful;

(* ------------------------------------------------------------------------- *)
(* Variable names.                                                           *)
(* ------------------------------------------------------------------------- *)

val xVarName = Name.fromString "x";
val xVar = Term.Var xVarName;

val yVarName = Name.fromString "y";
val yVar = Term.Var yVarName;

val zVarName = Name.fromString "z";
val zVar = Term.Var zVarName;

fun xIVarName i = Name.fromString ("x" ^ Int.toString i);
fun xIVar i = Term.Var (xIVarName i);

fun yIVarName i = Name.fromString ("y" ^ Int.toString i);
fun yIVar i = Term.Var (yIVarName i);

(* ------------------------------------------------------------------------- *)
(*                                                                           *)
(* --------- reflexivity                                                     *)
(*   x = x                                                                   *)
(* ------------------------------------------------------------------------- *)

fun reflexivityRule x = Thm.refl x;

val reflexivity = reflexivityRule xVar;

(* ------------------------------------------------------------------------- *)
(*                                                                           *)
(* --------------------- symmetry                                            *)
(*   ~(x = y) \/ y = x                                                       *)
(* ------------------------------------------------------------------------- *)

fun symmetryRule x y =
    let
      val reflTh = reflexivityRule x
      val reflLit = Thm.destUnit reflTh
      val eqTh = Thm.equality reflLit [0] y
    in
      Thm.resolve reflLit reflTh eqTh
    end;

val symmetry = symmetryRule xVar yVar;

(* ------------------------------------------------------------------------- *)
(*                                                                           *)
(* --------------------------------- transitivity                            *)
(*   ~(x = y) \/ ~(y = z) \/ x = z                                           *)
(* ------------------------------------------------------------------------- *)

val transitivity =
    let
      val eqTh = Thm.equality (Literal.mkEq (yVar,zVar)) [0] xVar
    in
      Thm.resolve (Literal.mkEq (yVar,xVar)) symmetry eqTh
    end;

(* ------------------------------------------------------------------------- *)
(*   x = y \/ C                                                              *)
(* -------------- symEq (x = y)                                              *)
(*   y = x \/ C                                                              *)
(* ------------------------------------------------------------------------- *)

fun symEq lit th =
    let
      val (x,y) = Literal.destEq lit
    in
      if Term.equal x y then th
      else
        let
          val sub = Subst.fromList [(xVarName,x),(yVarName,y)]

          val symTh = Thm.subst sub symmetry
        in
          Thm.resolve lit th symTh
        end
    end;

(* ------------------------------------------------------------------------- *)
(* An equation consists of two terms (t,u) plus a theorem (stronger than)    *)
(* t = u \/ C.                                                               *)
(* ------------------------------------------------------------------------- *)

type equation = (Term.term * Term.term) * Thm.thm;

fun ppEquation ((_,th) : equation) = Thm.pp th;

val equationToString = Print.toString ppEquation;

fun equationLiteral (t_u,th) =
    let
      val lit = Literal.mkEq t_u
    in
      if LiteralSet.member lit (Thm.clause th) then SOME lit else NONE
    end;

fun reflEqn t = ((t,t), Thm.refl t);

fun symEqn (eqn as ((t,u), th)) =
    if Term.equal t u then eqn
    else
      ((u,t),
       case equationLiteral eqn of
         SOME t_u => symEq t_u th
       | NONE => th);

fun transEqn (eqn1 as ((x,y), th1)) (eqn2 as ((_,z), th2)) =
    if Term.equal x y then eqn2
    else if Term.equal y z then eqn1
    else if Term.equal x z then reflEqn x
    else
      ((x,z),
       case equationLiteral eqn1 of
         NONE => th1
       | SOME x_y =>
         case equationLiteral eqn2 of
           NONE => th2
         | SOME y_z =>
           let
             val sub = Subst.fromList [(xVarName,x),(yVarName,y),(zVarName,z)]
             val th = Thm.subst sub transitivity
             val th = Thm.resolve x_y th1 th
             val th = Thm.resolve y_z th2 th
           in
             th
           end);

(*MetisDebug
val transEqn = fn eqn1 => fn eqn2 =>
    transEqn eqn1 eqn2
    handle Error err =>
      raise Error ("Rule.transEqn:\neqn1 = " ^ equationToString eqn1 ^
                   "\neqn2 = " ^ equationToString eqn2 ^ "\n" ^ err);
*)

(* ------------------------------------------------------------------------- *)
(* A conversion takes a term t and either:                                   *)
(* 1. Returns a term u together with a theorem (stronger than) t = u \/ C.   *)
(* 2. Raises an Error exception.                                             *)
(* ------------------------------------------------------------------------- *)

type conv = Term.term -> Term.term * Thm.thm;

fun allConv tm = (tm, Thm.refl tm);

val noConv : conv = fn _ => raise Error "noConv";

(*MetisDebug
fun traceConv s conv tm =
    let
      val res as (tm',th) = conv tm
      val () = trace (s ^ ": " ^ Term.toString tm ^ " --> " ^
                      Term.toString tm' ^ " " ^ Thm.toString th ^ "\n")
    in
      res
    end
    handle Error err =>
      (trace (s ^ ": " ^ Term.toString tm ^ " --> Error: " ^ err ^ "\n");
       raise Error (s ^ ": " ^ err));
*)

fun thenConvTrans tm (tm',th1) (tm'',th2) =
    let
      val eqn1 = ((tm,tm'),th1)
      and eqn2 = ((tm',tm''),th2)
      val (_,th) = transEqn eqn1 eqn2
    in
      (tm'',th)
    end;

fun thenConv conv1 conv2 tm =
    let
      val res1 as (tm',_) = conv1 tm
      val res2 = conv2 tm'
    in
      thenConvTrans tm res1 res2
    end;

fun orelseConv (conv1 : conv) conv2 tm = conv1 tm handle Error _ => conv2 tm;

fun tryConv conv = orelseConv conv allConv;

fun changedConv conv tm =
    let
      val res as (tm',_) = conv tm
    in
      if tm = tm' then raise Error "changedConv" else res
    end;

fun repeatConv conv tm = tryConv (thenConv conv (repeatConv conv)) tm;

fun firstConv [] _ = raise Error "firstConv"
  | firstConv [conv] tm = conv tm
  | firstConv (conv :: convs) tm = orelseConv conv (firstConv convs) tm;

fun everyConv [] tm = allConv tm
  | everyConv [conv] tm = conv tm
  | everyConv (conv :: convs) tm = thenConv conv (everyConv convs) tm;

fun rewrConv (eqn as ((x,y), eqTh)) path tm =
    if Term.equal x y then allConv tm
    else if List.null path then (y,eqTh)
    else
      let
        val reflTh = Thm.refl tm
        val reflLit = Thm.destUnit reflTh
        val th = Thm.equality reflLit (1 :: path) y
        val th = Thm.resolve reflLit reflTh th
        val th =
            case equationLiteral eqn of
              NONE => th
            | SOME x_y => Thm.resolve x_y eqTh th
        val tm' = Term.replace tm (path,y)
      in
        (tm',th)
      end;

(*MetisDebug
val rewrConv = fn eqn as ((x,y),eqTh) => fn path => fn tm =>
    rewrConv eqn path tm
    handle Error err =>
      raise Error ("Rule.rewrConv:\nx = " ^ Term.toString x ^
                   "\ny = " ^ Term.toString y ^
                   "\neqTh = " ^ Thm.toString eqTh ^
                   "\npath = " ^ Term.pathToString path ^
                   "\ntm = " ^ Term.toString tm ^ "\n" ^ err);
*)

fun pathConv conv path tm =
    let
      val x = Term.subterm tm path
      val (y,th) = conv x
    in
      rewrConv ((x,y),th) path tm
    end;

fun subtermConv conv i = pathConv conv [i];

fun subtermsConv _ (tm as Term.Var _) = allConv tm
  | subtermsConv conv (tm as Term.Fn (_,a)) =
    everyConv (List.map (subtermConv conv) (interval 0 (length a))) tm;

(* ------------------------------------------------------------------------- *)
(* Applying a conversion to every subterm, with some traversal strategy.     *)
(* ------------------------------------------------------------------------- *)

fun bottomUpConv conv tm =
    thenConv (subtermsConv (bottomUpConv conv)) (repeatConv conv) tm;

fun topDownConv conv tm =
    thenConv (repeatConv conv) (subtermsConv (topDownConv conv)) tm;

fun repeatTopDownConv conv =
    let
      fun f tm = thenConv (repeatConv conv) g tm
      and g tm = thenConv (subtermsConv f) h tm
      and h tm = tryConv (thenConv conv f) tm
    in
      f
    end;

(*MetisDebug
val repeatTopDownConv = fn conv => fn tm =>
    repeatTopDownConv conv tm
    handle Error err => raise Error ("repeatTopDownConv: " ^ err);
*)

(* ------------------------------------------------------------------------- *)
(* A literule (bad pun) takes a literal L and either:                        *)
(* 1. Returns a literal L' with a theorem (stronger than) ~L \/ L' \/ C.     *)
(* 2. Raises an Error exception.                                             *)
(* ------------------------------------------------------------------------- *)

type literule = Literal.literal -> Literal.literal * Thm.thm;

fun allLiterule lit = (lit, Thm.assume lit);

val noLiterule : literule = fn _ => raise Error "noLiterule";

fun thenLiterule literule1 literule2 lit =
    let
      val res1 as (lit',th1) = literule1 lit
      val res2 as (lit'',th2) = literule2 lit'
    in
      if Literal.equal lit lit' then res2
      else if Literal.equal lit' lit'' then res1
      else if Literal.equal lit lit'' then allLiterule lit
      else
        (lit'',
         if not (Thm.member lit' th1) then th1
         else if not (Thm.negateMember lit' th2) then th2
         else Thm.resolve lit' th1 th2)
    end;

fun orelseLiterule (literule1 : literule) literule2 lit =
    literule1 lit handle Error _ => literule2 lit;

fun tryLiterule literule = orelseLiterule literule allLiterule;

fun changedLiterule literule lit =
    let
      val res as (lit',_) = literule lit
    in
      if lit = lit' then raise Error "changedLiterule" else res
    end;

fun repeatLiterule literule lit =
    tryLiterule (thenLiterule literule (repeatLiterule literule)) lit;

fun firstLiterule [] _ = raise Error "firstLiterule"
  | firstLiterule [literule] lit = literule lit
  | firstLiterule (literule :: literules) lit =
    orelseLiterule literule (firstLiterule literules) lit;

fun everyLiterule [] lit = allLiterule lit
  | everyLiterule [literule] lit = literule lit
  | everyLiterule (literule :: literules) lit =
    thenLiterule literule (everyLiterule literules) lit;

fun rewrLiterule (eqn as ((x,y),eqTh)) path lit =
    if Term.equal x y then allLiterule lit
    else
      let
        val th = Thm.equality lit path y
        val th =
            case equationLiteral eqn of
              NONE => th
            | SOME x_y => Thm.resolve x_y eqTh th
        val lit' = Literal.replace lit (path,y)
      in
        (lit',th)
      end;

(*MetisDebug
val rewrLiterule = fn eqn => fn path => fn lit =>
    rewrLiterule eqn path lit
    handle Error err =>
      raise Error ("Rule.rewrLiterule:\neqn = " ^ equationToString eqn ^
                   "\npath = " ^ Term.pathToString path ^
                   "\nlit = " ^ Literal.toString lit ^ "\n" ^ err);
*)

fun pathLiterule conv path lit =
    let
      val tm = Literal.subterm lit path
      val (tm',th) = conv tm
    in
      rewrLiterule ((tm,tm'),th) path lit
    end;

fun argumentLiterule conv i = pathLiterule conv [i];

fun allArgumentsLiterule conv lit =
    everyLiterule
      (List.map (argumentLiterule conv) (interval 0 (Literal.arity lit))) lit;

(* ------------------------------------------------------------------------- *)
(* A rule takes one theorem and either deduces another or raises an Error    *)
(* exception.                                                                *)
(* ------------------------------------------------------------------------- *)

type rule = Thm.thm -> Thm.thm;

val allRule : rule = fn th => th;

val noRule : rule = fn _ => raise Error "noRule";

fun thenRule (rule1 : rule) (rule2 : rule) th = rule1 (rule2 th);

fun orelseRule (rule1 : rule) rule2 th = rule1 th handle Error _ => rule2 th;

fun tryRule rule = orelseRule rule allRule;

fun changedRule rule th =
    let
      val th' = rule th
    in
      if not (LiteralSet.equal (Thm.clause th) (Thm.clause th')) then th'
      else raise Error "changedRule"
    end;

fun repeatRule rule lit = tryRule (thenRule rule (repeatRule rule)) lit;

fun firstRule [] _ = raise Error "firstRule"
  | firstRule [rule] th = rule th
  | firstRule (rule :: rules) th = orelseRule rule (firstRule rules) th;

fun everyRule [] th = allRule th
  | everyRule [rule] th = rule th
  | everyRule (rule :: rules) th = thenRule rule (everyRule rules) th;

fun literalRule literule lit th =
    let
      val (lit',litTh) = literule lit
    in
      if Literal.equal lit lit' then th
      else if not (Thm.negateMember lit litTh) then litTh
      else Thm.resolve lit th litTh
    end;

(*MetisDebug
val literalRule = fn literule => fn lit => fn th =>
    literalRule literule lit th
    handle Error err =>
      raise Error ("Rule.literalRule:\nlit = " ^ Literal.toString lit ^
                   "\nth = " ^ Thm.toString th ^ "\n" ^ err);
*)

fun rewrRule eqTh lit path = literalRule (rewrLiterule eqTh path) lit;

fun pathRule conv lit path = literalRule (pathLiterule conv path) lit;

fun literalsRule literule =
    let
      fun f (lit,th) =
          if Thm.member lit th then literalRule literule lit th else th
    in
      fn lits => fn th => LiteralSet.foldl f th lits
    end;

fun allLiteralsRule literule th = literalsRule literule (Thm.clause th) th;

fun convRule conv = allLiteralsRule (allArgumentsLiterule conv);

(* ------------------------------------------------------------------------- *)
(*                                                                           *)
(* ---------------------------------------------- functionCongruence (f,n)   *)
(*   ~(x0 = y0) \/ ... \/ ~(x{n-1} = y{n-1}) \/                              *)
(*   f x0 ... x{n-1} = f y0 ... y{n-1}                                       *)
(* ------------------------------------------------------------------------- *)

fun functionCongruence (f,n) =
    let
      val xs = List.tabulate (n,xIVar)
      and ys = List.tabulate (n,yIVar)

      fun cong ((i,yi),(th,lit)) =
          let
            val path = [1,i]
            val th = Thm.resolve lit th (Thm.equality lit path yi)
            val lit = Literal.replace lit (path,yi)
          in
            (th,lit)
          end

      val reflTh = Thm.refl (Term.Fn (f,xs))
      val reflLit = Thm.destUnit reflTh
    in
      fst (List.foldl cong (reflTh,reflLit) (enumerate ys))
    end;

(* ------------------------------------------------------------------------- *)
(*                                                                           *)
(* ---------------------------------------------- relationCongruence (R,n)   *)
(*   ~(x0 = y0) \/ ... \/ ~(x{n-1} = y{n-1}) \/                              *)
(*   ~R x0 ... x{n-1} \/ R y0 ... y{n-1}                                     *)
(* ------------------------------------------------------------------------- *)

fun relationCongruence (R,n) =
    let
      val xs = List.tabulate (n,xIVar)
      and ys = List.tabulate (n,yIVar)

      fun cong ((i,yi),(th,lit)) =
          let
            val path = [i]
            val th = Thm.resolve lit th (Thm.equality lit path yi)
            val lit = Literal.replace lit (path,yi)
          in
            (th,lit)
          end

      val assumeLit = (false,(R,xs))
      val assumeTh = Thm.assume assumeLit
    in
      fst (List.foldl cong (assumeTh,assumeLit) (enumerate ys))
    end;

(* ------------------------------------------------------------------------- *)
(*   ~(x = y) \/ C                                                           *)
(* ----------------- symNeq ~(x = y)                                         *)
(*   ~(y = x) \/ C                                                           *)
(* ------------------------------------------------------------------------- *)

fun symNeq lit th =
    let
      val (x,y) = Literal.destNeq lit
    in
      if Term.equal x y then th
      else
        let
          val sub = Subst.fromList [(xVarName,y),(yVarName,x)]
          val symTh = Thm.subst sub symmetry
        in
          Thm.resolve lit th symTh
        end
    end;

(* ------------------------------------------------------------------------- *)
(* sym (x = y) = symEq (x = y)  /\  sym ~(x = y) = symNeq ~(x = y)           *)
(* ------------------------------------------------------------------------- *)

fun sym (lit as (pol,_)) th = if pol then symEq lit th else symNeq lit th;

(* ------------------------------------------------------------------------- *)
(*   ~(x = x) \/ C                                                           *)
(* ----------------- removeIrrefl                                            *)
(*         C                                                                 *)
(*                                                                           *)
(* where all irreflexive equalities.                                         *)
(* ------------------------------------------------------------------------- *)

local
  fun irrefl ((true,_),th) = th
    | irrefl (lit as (false,atm), th) =
      case total Atom.destRefl atm of
        SOME x => Thm.resolve lit th (Thm.refl x)
      | NONE => th;
in
  fun removeIrrefl th = LiteralSet.foldl irrefl th (Thm.clause th);
end;

(* ------------------------------------------------------------------------- *)
(*   x = y \/ y = x \/ C                                                     *)
(* ----------------------- removeSym                                         *)
(*       x = y \/ C                                                          *)
(*                                                                           *)
(* where all duplicate copies of equalities and disequalities are removed.   *)
(* ------------------------------------------------------------------------- *)

local
  fun rem (lit as (pol,atm), eqs_th as (eqs,th)) =
      case total Atom.sym atm of
        NONE => eqs_th
      | SOME atm' =>
        if LiteralSet.member lit eqs then
          (eqs, if pol then symEq lit th else symNeq lit th)
        else
          (LiteralSet.add eqs (pol,atm'), th);
in
  fun removeSym th =
      snd (LiteralSet.foldl rem (LiteralSet.empty,th) (Thm.clause th));
end;

(* ------------------------------------------------------------------------- *)
(*   ~(v = t) \/ C                                                           *)
(* ----------------- expandAbbrevs                                           *)
(*      C[t/v]                                                               *)
(*                                                                           *)
(* where t must not contain any occurrence of the variable v.                *)
(* ------------------------------------------------------------------------- *)

local
  fun expand lit =
      let
        val (x,y) = Literal.destNeq lit
        val _ = Term.isTypedVar x orelse Term.isTypedVar y orelse
                raise Error "Rule.expandAbbrevs: no vars"
        val _ = not (Term.equal x y) orelse
                raise Error "Rule.expandAbbrevs: equal vars"
      in
        Subst.unify Subst.empty x y
      end;
in
  fun expandAbbrevs th =
      case LiteralSet.firstl (total expand) (Thm.clause th) of
        NONE => removeIrrefl th
      | SOME sub => expandAbbrevs (Thm.subst sub th);
end;

(* ------------------------------------------------------------------------- *)
(* simplify = isTautology + expandAbbrevs + removeSym                        *)
(* ------------------------------------------------------------------------- *)

fun simplify th =
    if Thm.isTautology th then NONE
    else
      let
        val th' = th
        val th' = expandAbbrevs th'
        val th' = removeSym th'
      in
        if Thm.equal th th' then SOME th else simplify th'
      end;

(* ------------------------------------------------------------------------- *)
(*    C                                                                      *)
(* -------- freshVars                                                        *)
(*   C[s]                                                                    *)
(*                                                                           *)
(* where s is a renaming substitution chosen so that all of the variables in *)
(* C are replaced by fresh variables.                                        *)
(* ------------------------------------------------------------------------- *)

fun freshVars th = Thm.subst (Subst.freshVars (Thm.freeVars th)) th;

(* ------------------------------------------------------------------------- *)
(*               C                                                           *)
(* ---------------------------- factor                                       *)
(*   C_s_1, C_s_2, ..., C_s_n                                                *)
(*                                                                           *)
(* where each s_i is a substitution that factors C, meaning that the theorem *)
(*                                                                           *)
(*   C_s_i = (removeIrrefl o removeSym o Thm.subst s_i) C                    *)
(*                                                                           *)
(* has fewer literals than C.                                                *)
(*                                                                           *)
(* Also, if s is any substitution that factors C, then one of the s_i will   *)
(* result in a theorem C_s_i that strictly subsumes the theorem C_s.         *)
(* ------------------------------------------------------------------------- *)

local
  datatype edge =
      FactorEdge of Atom.atom * Atom.atom
    | ReflEdge of Term.term * Term.term;

  fun ppEdge (FactorEdge atm_atm') = Print.ppPair Atom.pp Atom.pp atm_atm'
    | ppEdge (ReflEdge tm_tm') = Print.ppPair Term.pp Term.pp tm_tm';

  datatype joinStatus =
      Joined
    | Joinable of Subst.subst
    | Apart;

  fun joinEdge sub edge =
      let
        val result =
            case edge of
              FactorEdge (atm,atm') => total (Atom.unify sub atm) atm'
            | ReflEdge (tm,tm') => total (Subst.unify sub tm) tm'
      in
        case result of
          NONE => Apart
        | SOME sub' =>
          if Portable.pointerEqual (sub,sub') then Joined else Joinable sub'
      end;

  fun updateApart sub =
      let
        fun update acc [] = SOME acc
          | update acc (edge :: edges) =
            case joinEdge sub edge of
              Joined => NONE
            | Joinable _ => update (edge :: acc) edges
            | Apart => update acc edges
      in
        update []
      end;

  fun addFactorEdge (pol,atm) ((pol',atm'),acc) =
      if pol <> pol' then acc
      else
        let
          val edge = FactorEdge (atm,atm')
        in
          case joinEdge Subst.empty edge of
            Joined => raise Bug "addFactorEdge: joined"
          | Joinable sub => (sub,edge) :: acc
          | Apart => acc
        end;

  fun addReflEdge (false,_) acc = acc
    | addReflEdge (true,atm) acc =
      let
        val edge = ReflEdge (Atom.destEq atm)
      in
        case joinEdge Subst.empty edge of
          Joined => raise Bug "addRefl: joined"
        | Joinable _ => edge :: acc
        | Apart => acc
      end;

  fun addIrreflEdge (true,_) acc = acc
    | addIrreflEdge (false,atm) acc =
      let
        val edge = ReflEdge (Atom.destEq atm)
      in
        case joinEdge Subst.empty edge of
          Joined => raise Bug "addRefl: joined"
        | Joinable sub => (sub,edge) :: acc
        | Apart => acc
      end;

  fun init_edges acc _ [] =
      let
        fun init ((apart,sub,edge),(edges,acc)) =
            (edge :: edges, (apart,sub,edges) :: acc)
      in
        snd (List.foldl init ([],[]) acc)
      end
    | init_edges acc apart ((sub,edge) :: sub_edges) =
      let
(*MetisDebug
        val () = if not (Subst.null sub) then ()
                 else raise Bug "Rule.factor.init_edges: empty subst"
*)
        val (acc,apart) =
            case updateApart sub apart of
              SOME apart' => ((apart',sub,edge) :: acc, edge :: apart)
            | NONE => (acc,apart)
      in
        init_edges acc apart sub_edges
      end;

  fun mk_edges apart sub_edges [] = init_edges [] apart sub_edges
    | mk_edges apart sub_edges (lit :: lits) =
      let
        val sub_edges = List.foldl (addFactorEdge lit) sub_edges lits

        val (apart,sub_edges) =
            case total Literal.sym lit of
              NONE => (apart,sub_edges)
            | SOME lit' =>
              let
                val apart = addReflEdge lit apart
                val sub_edges = addIrreflEdge lit sub_edges
                val sub_edges = List.foldl (addFactorEdge lit') sub_edges lits
              in
                (apart,sub_edges)
              end
      in
        mk_edges apart sub_edges lits
      end;

  fun fact acc [] = acc
    | fact acc ((_,sub,[]) :: others) = fact (sub :: acc) others
    | fact acc ((apart, sub, edge :: edges) :: others) =
      let
        val others =
            case joinEdge sub edge of
              Joinable sub' =>
              let
                val others = (edge :: apart, sub, edges) :: others
              in
                case updateApart sub' apart of
                  NONE => others
                | SOME apart' => (apart',sub',edges) :: others
              end
            | _ => (apart,sub,edges) :: others
      in
        fact acc others
      end;
in
  fun factor' cl =
      let
(*MetisTrace6
        val () = Print.trace LiteralSet.pp "Rule.factor': cl" cl
*)
        val edges = mk_edges [] [] (LiteralSet.toList cl)
(*MetisTrace6
        val ppEdgesSize = Print.ppMap length Print.ppInt
        val ppEdgel = Print.ppList ppEdge
        val ppEdges = Print.ppList (Print.ppTriple ppEdgel Subst.pp ppEdgel)
        val () = Print.trace ppEdgesSize "Rule.factor': |edges|" edges
        val () = Print.trace ppEdges "Rule.factor': edges" edges
*)
        val result = fact [] edges
(*MetisTrace6
        val ppResult = Print.ppList Subst.pp
        val () = Print.trace ppResult "Rule.factor': result" result
*)
      in
        result
      end;
end;

fun factor th =
    let
      fun fact sub = removeIrrefl (removeSym (Thm.subst sub th))
    in
      List.map fact (factor' (Thm.clause th))
    end;

end