The issues that particularly concern me are (in descending order of importance):
Download for testing
(* some types I'll need in a minute for matching *)
val boolfunt = Tyapp("fun",[Tyapp("bool",[]),
Tyapp("bool",[])]);
val boolopt = Tyapp("fun",[Tyapp("bool",[]),
boolfunt]);
val condt = Tyapp("fun",[Tyapp("bool",[]),
boolopt]);
val COND = Const("COND",condt);
(* convert a bool term into an if-expression,
mainly looking for the typical boolean connectives
anything else (a quantifier, a predicate application,
the result of applying a non-typical boolean connective)
will be treated like an ordinary proposition *)
fun iffify (tm as Comb (Comb(Const(f,boolopt),lrand),rrand)) =
(case f of
"/\\" => (mk_cond (convert lrand,convert rrand, X "F")) |
"\\/" => (mk_cond (convert lrand, X "T", convert rrand)) |
"==>" => (mk_cond (convert lrand, convert rrand, X "T")) |
"=" => (mk_cond (convert lrand, convert rrand,
mk_cond (convert rrand, X "F", X "T"))) |
_ => tm ) |
iffify (Comb (Const("~",boolfunt),rand)) =
(mk_cond(convert rand, X "F", X "T")) |
iffify (Comb (Comb (Comb (COND,
onerand),tworand),threerand)) =
(mk_cond (convert onerand, convert tworand,convert threerand)) |
iffify x = x
(* just screen out the non-bool terms *)
and convert x = if ((type_of x) = Y "bool") then iffify x
else raise Failure ("convert: non-bool term");
(* apply an assignment in a assoc-list to a term *)
fun assignment x alist = assoc x alist handle Failure str =>
raise (Failure ("assignment: "^str));
(* normalize the if-expressions,
i.e. get rid of "if"'s in the branch part of "if"'s *)
fun norm (Comb (Comb (Comb (COND,a),b),c)) =
(case a of (Comb (Comb (Comb (COND,a'),b'),c')) =>
(norm (mk_cond (a',
mk_cond(b',b,c),
mk_cond(c',b,c)))) |
tm => mk_cond (a,(norm b),(norm c))) |
norm tm = tm;
(* check if a normalized if-expression is a tautology *)
fun tautp (Comb (Comb (Comb (COND,a),b),c)) alist =
if (mem a (fst (unzip alist)))
then if (assignment a alist)
then (tautp b alist)
else (tautp c alist)
else ((tautp b ((a,true)::alist))
andalso
(tautp c ((a,false)::alist))) |
tautp x alist = assignment x alist handle Failure _ => false;
(* put the pieces together *)
fun taut x = (tautp (norm x) [(X "T",true),(X "F",false)]);
fun check_taut x = taut (convert x);
fun bmTAUT x = if (check_taut x) then X "T" else x;
(* should work (and do) *)
val dem1a = X "(a ==> b) = (~a \\/ b)";
val dem2 = X "(a /\\ b) = ~(~a \\/ ~b)";
val dem3 = X "(a \\/ b) = ~(~a /\\ ~b)";
val taut1 = X "(a \\/ ~a)";
val taut1a = X "(a \\/ ~a) = T";
(* shouldn't work -- and don't *)
val unsat1 = X "(a /\\ ~a)";
val unsat2 = X "T ==> F";
val sat1 = X "a /\\ b";
val sat2 = X "(a:bool) = b";
Download for testing
(* check the known rules to determine if we can reduce a term to
zero *)
fun opred lrand rator rrand =
let val l' = zred lrand
val r' = zred rrand
val zero = X "0"
val binopt = Tyapp("fun",[Tyapp("num",[]),
Tyapp("fun",[Tyapp("num",[]),
Tyapp("num",[])])])
in
if (rator = (Const("*",binopt)))
then (if ((l' = zero ) orelse (r' = zero))
then zero
else Comb (Comb (rator,l'), r'))
else if (rator = (Const("+",binopt)))
then if (l' = zero)
then r'
else if (r' = zero)
then l'
else Comb (Comb(rator,l'), r')
else if (rator = (Const ("-",binopt)))
then if (r' = zero)
then l'
else Comb (Comb(rator,l'), r')
else Comb (Comb(rator,l'),r') end
(* find the terms which actually have feature an operator on a
numeric term *)
and numred (Comb (x,y)) b = if (type_of(y) = (Y "num"))
then (opred y x b)
else Comb (zred (Comb(x,y)), zred b) |
numred (Const ("-",t1)) b = let val b' = zred b
in if (b' = (X "0"))
then b'
else Comb(Const("-",t1),b') end |
numred a b = Comb (zred a, zred b)
(* just find the terms of type num which could be reduced *)
and zred (Var(x,y)) = Var(x,y) |
zred (Const(x,y)) = Const(x,y) |
zred (Comb(x,y)) = if (type_of (Comb(x,y)) = (Y "num"))
then numred x y
else Comb(zred x, zred y) |
zred (Abs(x,y)) = Abs(x, zred y);
The issues that particularly concern me are (in descending order of importance):
(*===========================================================================*)
(* Discriminator functions for T (true) and F (false) *)
(*===========================================================================*)
val T = X "T"
and F = X "F";
fun is_T tm = (tm = T)
and is_F tm = (tm = F);
val boolty = Y "bool";
val boolopty = Y "bool->bool";
val boolfunty = Y "bool->bool->bool";
val boolthreety = Y "bool->bool->bool->bool";
(*===========================================================================*)
(* Conversions used for simplifying Boolean terms *)
(*===========================================================================*)
(*---------------------------------------------------------------------------*)
(* NOT_CONV : conv *)
(* *)
(* |- !t. ~~t = t *)
(* |- ~T = F *)
(* |- ~F = T *)
(*---------------------------------------------------------------------------*)
fun NOT_FUN tm =
let val arg = dest_neg tm
in if (is_T arg)
then F
else if (is_F arg)
then T
else if (is_neg arg)
then dest_neg arg
else tm
end handle Failure x => raise (Failure ("NOT_FUN: "^x));
(*---------------------------------------------------------------------------*)
(* EQ_CONV : conv *)
(* *)
(* |- (t = t) = T *)
(* |- (T = t) = t *)
(* |- (t = T) = t *)
(* |- (F = t) = ~t *)
(* |- (t = F) = ~t *)
(*---------------------------------------------------------------------------*)
fun EQ_FUN tm =
let val (lhs,rhs) = dest_eq tm
val neg = Const("~",boolopty)
in
if (is_T rhs)
then lhs
else if (is_T lhs)
then rhs
else if (is_F rhs)
then Comb(neg,lhs)
else if (is_F lhs)
then Comb(neg,rhs)
else if (lhs=rhs)
then T
else tm
end handle Failure x => raise (Failure ("EQ_FUN: "^x));
(*---------------------------------------------------------------------------*)
(* AND_CONV : conv *)
(* *)
(* |- T /\ t = t *)
(* |- t /\ T = t *)
(* |- F /\ t = F *)
(* |- t /\ F = F *)
(* |- t /\ t = t *)
(*---------------------------------------------------------------------------*)
fun AND_FUN tm =
let val (c1,c2) = dest_conj tm
in
if (is_T c1)
then c2
else if (is_T c2)
then c1
else if (is_F c1)
then F
else if (is_F c2)
then F
else if (c1 = c2)
then T
else c1
end handle Failure x => raise Failure ("AND_FUN: "^x);
(*---------------------------------------------------------------------------*)
(* OR_CONV : conv *)
(* *)
(* |- T \/ t = T *)
(* |- t \/ T = T *)
(* |- F \/ t = t *)
(* |- t \/ F = t *)
(* |- t \/ t = t *)
(*---------------------------------------------------------------------------*)
fun OR_FUN tm =
let val (d1,d2) = dest_disj tm
in
if (is_T d1)
then T
else if (is_T d2)
then T
else if (is_F d1)
then d2
else if (is_F d2)
then d1
else if (d1 = d2)
then d1
else tm
end handle Failure x => raise Failure ("OR_FUN: "^x);
(*---------------------------------------------------------------------------*)
(* IMP_CONV : conv *)
(* *)
(* |- T ==> t = t *)
(* |- t ==> T = T *)
(* |- F ==> t = T *)
(* |- t ==> t = T *)
(* |- t ==> F = ~t *)
(*---------------------------------------------------------------------------*)
fun IMP_FUN tm =
let val (ant,cons) = dest_imp tm
val neg = Const("~",Tyapp("fun",[Tyapp("bool",[]),Tyapp("bool",[])]))
in
if (is_T ant)
then cons
else if (is_T cons)
then T
else if (is_F ant)
then T
else if (is_F cons)
then Comb(neg,ant)
else if (ant = cons)
then T
else tm
end handle Failure x => raise Failure ("IMP_FUN: "^x);
(*---------------------------------------------------------------------------*)
(* IF_CONV : conv *)
(* *)
(* |- (T => t1 | t2) = t1 *)
(* |- (F => t1 | t2) = t2 *)
(*---------------------------------------------------------------------------*)
fun IF_FUN tm =
let val (br,(lef,rig)) = dest_cond tm
in
if (is_T br)
then lef
else if (is_F br)
then rig
else tm
end handle Failure x => raise Failure ("IF_FUN: "^x);
(*---------------------------------------------------------------------------*)
(* SIMP_PROP_QCONV : conv *)
(* *)
(* Conversion for simplifying propositional terms containing constants, *)
(* variables, equality, implication, AND, OR, NOT and conditionals. *)
(* Uses failure to avoid rebuilding unchanged subterms. *)
(*---------------------------------------------------------------------------*)
fun SIMP_PROP_FUN (tm as Const(_,_)) = tm |
SIMP_PROP_FUN (tm as Var (_,_)) = tm |
SIMP_PROP_FUN (tm as Comb(x,y)) =
let val NEG = Const("~",boolopty)
in
((if (is_neg tm)
then NOT_FUN (Comb(NEG,SIMP_PROP_FUN y))
else
(case x of (Comb(v,w)) =>
if (is_conj tm)
then let val x1' = SIMP_PROP_FUN w
val y' = SIMP_PROP_FUN y
in AND_FUN (Comb(Comb(v,x1'),y')) end
else if (is_disj tm)
then let val x1' = SIMP_PROP_FUN w
val y' = SIMP_PROP_FUN y
in OR_FUN (Comb(Comb(v,x1'),y')) end
else if (is_imp tm)
then let val x1' = SIMP_PROP_FUN w
val y' = SIMP_PROP_FUN y
in IMP_FUN (Comb(Comb(v,x1'),y')) end
else if (is_eq tm)
then let val x1' = SIMP_PROP_FUN w
val y' = SIMP_PROP_FUN y
in SIMP_PROP_FUN
(EQ_FUN (Comb(Comb(v,x1'),y')))
end
else (case v of (Comb(r,s)) =>
(if (is_cond tm) then
let val x1' = SIMP_PROP_FUN w
val y' = SIMP_PROP_FUN y
val z' = SIMP_PROP_FUN s
in IF_FUN (Comb(Comb(Comb(r,
z'),
x1'),
y')) end
else tm) |
_ => tm) |
_ => tm ))
handle UNCHANGED => tm) end |
SIMP_PROP_FUN (Abs (v,b)) = Abs(v,SIMP_PROP_FUN b);
(*---------------------------------------------------------------------------*)
(* TAUT_CHECK_CONV : conv *)
(* *)
(* Given a propositional term with all variables universally quantified, *)
(* e.g. `!x1 ... xn. f[x1,...,xn]`, this conversion proves the term to be *)
(* either true or false, i.e. it returns one of: *)
(* *)
(* |- (!x1 ... xn. f[x1,...,xn]) = T *)
(* |- (!x1 ... xn. f[x1,...,xn]) = F *)
(*---------------------------------------------------------------------------*)
fun TAUT_CHECK tm =
let val (vars,tm') = strip_forall tm
in
if (is_T tm')
then true
else if (is_F tm')
then false
else let val (var,bod) = dest_forall tm
val tmT = subst [(T,var)] bod
val tmT1 = SIMP_PROP_FUN tmT
in
(TAUT_CHECK tmT1) andalso
(let val tmF = subst [(F,var)] bod
val tmF1 = SIMP_PROP_FUN tmF
in
TAUT_CHECK tmF1
end)
end
end handle Failure x => raise Failure ("TAUT_CHECK: "^x);
fun TAUT tm =
if TAUT_CHECK tm then T else tm;
val rtaut1 = X "!a. a \\/ ~a";
val rtaut2 = X "!a. a ==> a";
val rsat1 = X "!a. a /\\ a";
val rsat2 = X "!a. a \\/ a";
val rnonsat1 = X "!a. a /\\ ~a";
val rtaut3 = X "!a b c. (a ==> b) \\/ (b ==> c) \\/ (c ==> a)";