--- a/src/HOL/SMT/Tools/smt_normalize.ML Wed May 12 23:53:48 2010 +0200
+++ b/src/HOL/SMT/Tools/smt_normalize.ML Wed May 12 23:53:49 2010 +0200
@@ -3,6 +3,7 @@
Normalization steps on theorems required by SMT solvers:
* unfold trivial let expressions,
+ * simplify trivial distincts (those with less than three elements),
* replace negative numerals by negated positive numerals,
* embed natural numbers into integers,
* add extra rules specifying types and constants which occur frequently,
@@ -140,6 +141,7 @@
fun if_true_conv c cv = if_conv c cv Conv.all_conv
+
(* simplification of trivial let expressions (whose bound variables occur at
most once) *)
@@ -161,6 +163,30 @@
end
+
+(* simplification of trivial distincts (distinct should have at least
+ three elements in the argument list) *)
+
+local
+ fun is_trivial_distinct (Const (@{const_name distinct}, _) $ t) =
+ length (HOLogic.dest_list t) <= 2
+ | is_trivial_distinct _ = false
+
+ val thms = @{lemma
+ "distinct [] == True"
+ "distinct [x] == True"
+ "distinct [x, y] == (x ~= y)"
+ by simp_all}
+ fun distinct_conv _ =
+ if_true_conv is_trivial_distinct (More_Conv.rewrs_conv thms)
+in
+fun trivial_distinct ctxt =
+ map ((Term.exists_subterm is_trivial_distinct o Thm.prop_of) ??
+ Conv.fconv_rule (More_Conv.top_conv distinct_conv ctxt))
+end
+
+
+
(* rewriting of negative integer numerals into positive numerals *)
local
@@ -194,6 +220,7 @@
end
+
(* embedding of standard natural number operations into integer operations *)
local
@@ -260,6 +287,7 @@
end
+
(* include additional rules *)
local
@@ -280,6 +308,7 @@
end
+
(* unfold definitions of specific constants *)
local
@@ -319,6 +348,7 @@
end
+
(* lift lambda terms into additional rules *)
local
@@ -412,6 +442,7 @@
end
+
(* make application explicit for functions with varying number of arguments *)
local
@@ -468,11 +499,13 @@
end
+
(* combined normalization *)
fun normalize ctxt thms =
thms
|> trivial_let ctxt
+ |> trivial_distinct ctxt
|> positive_numerals ctxt
|> nat_as_int ctxt
|> add_pair_rules ctxt