# HG changeset patch
# User boehmes
# Date 1273701229 -7200
# Node ID 9407b8d0f6ad032749ab2469326726d71969a11f
# Parent  88cf4896b980096c8162f0c377622b0f150c390c
added simplification for distinctness of small lists

diff -r 88cf4896b980 -r 9407b8d0f6ad src/HOL/SMT/Tools/smt_normalize.ML
--- 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