From 7bf55e0eb37d0d68268a5b6c2d55dc2895fd6361 Mon Sep 17 00:00:00 2001 From: Michael Norrish Date: Mon, 9 Sep 2024 14:53:02 +1000 Subject: [PATCH] Fix bug in reduceLib.NOT_CONV Thanks to someplaceguy for bug report. --- src/num/reduce/src/Boolconv.sml | 2 +- src/num/reduce/src/selftest.sml | 7 ++++++- 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/src/num/reduce/src/Boolconv.sml b/src/num/reduce/src/Boolconv.sml index 97e266c885..ac093bce37 100644 --- a/src/num/reduce/src/Boolconv.sml +++ b/src/num/reduce/src/Boolconv.sml @@ -46,7 +46,7 @@ fun NOT_CONV tm = let val xn = dest_neg tm in if aconv xn T then c1 else if aconv xn F then c2 - else let val xn' = dest_neg xn in SPEC xn c3 end + else let val xn' = dest_neg xn in SPEC xn' c3 end end handle HOL_ERR _ => raise ERR "NOT_CONV" "" end; diff --git a/src/num/reduce/src/selftest.sml b/src/num/reduce/src/selftest.sml index 89ab77763b..f67b7eed41 100644 --- a/src/num/reduce/src/selftest.sml +++ b/src/num/reduce/src/selftest.sml @@ -38,5 +38,10 @@ val _ = app (fn (n,c,t) => convtest(n,c,lhs t,rhs t)) [ ("EVEN_CONV(3)", EVEN_CONV, “EVEN 0 <=> T”), ("ODD_CONV(1)", ODD_CONV, “ODD 106 <=> F”), ("ODD_CONV(2)", ODD_CONV, “ODD 103 <=> T”), - ("ODD_CONV(3)", ODD_CONV, “ODD 0 <=> F”) + ("ODD_CONV(3)", ODD_CONV, “ODD 0 <=> F”), + + ("NOT_CONV(1)", NOT_CONV, “~T <=> F”), + ("NOT_CONV(2)", NOT_CONV, “~F <=> T”), + ("NOT_CONV(3)", NOT_CONV, “~~p <=> p”), + ("NOT_CONV(4)", NOT_CONV, “~~~q <=> ~q”) ]