(* ========================================================================= *)
(* DERIVED RULES FOR CREATING FIRST ORDER LOGIC THEOREMS *)
(* Copyright (c) 2001-2006 Joe 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) = 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";
fun traceConv s conv tm =
let
val res as (tm',th) = conv tm
val () = print (s ^ ": " ^ Term.toString tm ^ " --> " ^
Term.toString tm' ^ " " ^ Thm.toString th ^ "\n")
in
res
end
handle Error err =>
(print (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 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 (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
(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 (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 (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 = removeSym (Thm.subst sub th)
in
map fact (factor' (Thm.clause th))
end;
end