author boehmes Wed, 12 May 2010 23:53:49 +0200 changeset 36885 9407b8d0f6ad parent 36884 88cf4896b980 child 36886 d8ea5bff3ca4
added simplification for distinctness of small lists
```--- 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

+

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