1.1 --- a/src/HOL/SMT/Tools/smt_normalize.ML	Wed May 12 23:53:48 2010 +0200
     1.2 +++ b/src/HOL/SMT/Tools/smt_normalize.ML	Wed May 12 23:53:49 2010 +0200
     1.3 @@ -3,6 +3,7 @@
     1.4  
     1.5  Normalization steps on theorems required by SMT solvers:
     1.6    * unfold trivial let expressions,
     1.7 +  * simplify trivial distincts (those with less than three elements),
     1.8    * replace negative numerals by negated positive numerals,
     1.9    * embed natural numbers into integers,
    1.10    * add extra rules specifying types and constants which occur frequently,
    1.11 @@ -140,6 +141,7 @@
    1.12  fun if_true_conv c cv = if_conv c cv Conv.all_conv
    1.13  
    1.14  
    1.15 +
    1.16  (* simplification of trivial let expressions (whose bound variables occur at
    1.17     most once) *)
    1.18  
    1.19 @@ -161,6 +163,30 @@
    1.20  end
    1.21  
    1.22  
    1.23 +
    1.24 +(* simplification of trivial distincts (distinct should have at least
    1.25 +   three elements in the argument list) *)
    1.26 +
    1.27 +local
    1.28 +  fun is_trivial_distinct (Const (@{const_name distinct}, _) $ t) =
    1.29 +        length (HOLogic.dest_list t) <= 2
    1.30 +    | is_trivial_distinct _ = false
    1.31 +
    1.32 +  val thms = @{lemma
    1.33 +    "distinct [] == True"
    1.34 +    "distinct [x] == True"
    1.35 +    "distinct [x, y] == (x ~= y)"
    1.36 +    by simp_all}
    1.37 +  fun distinct_conv _ =
    1.38 +    if_true_conv is_trivial_distinct (More_Conv.rewrs_conv thms)
    1.39 +in
    1.40 +fun trivial_distinct ctxt =
    1.41 +  map ((Term.exists_subterm is_trivial_distinct o Thm.prop_of) ??
    1.42 +    Conv.fconv_rule (More_Conv.top_conv distinct_conv ctxt))
    1.43 +end
    1.44 +
    1.45 +
    1.46 +
    1.47  (* rewriting of negative integer numerals into positive numerals *)
    1.48  
    1.49  local
    1.50 @@ -194,6 +220,7 @@
    1.51  end
    1.52  
    1.53  
    1.54 +
    1.55  (* embedding of standard natural number operations into integer operations *)
    1.56  
    1.57  local
    1.58 @@ -260,6 +287,7 @@
    1.59  end
    1.60  
    1.61  
    1.62 +
    1.63  (* include additional rules *)
    1.64  
    1.65  local
    1.66 @@ -280,6 +308,7 @@
    1.67  end
    1.68  
    1.69  
    1.70 +
    1.71  (* unfold definitions of specific constants *)
    1.72  
    1.73  local
    1.74 @@ -319,6 +348,7 @@
    1.75  end
    1.76  
    1.77  
    1.78 +
    1.79  (* lift lambda terms into additional rules *)
    1.80  
    1.81  local
    1.82 @@ -412,6 +442,7 @@
    1.83  end
    1.84  
    1.85  
    1.86 +
    1.87  (* make application explicit for functions with varying number of arguments *)
    1.88  
    1.89  local
    1.90 @@ -468,11 +499,13 @@
    1.91  end
    1.92  
    1.93  
    1.94 +
    1.95  (* combined normalization *)
    1.96  
    1.97  fun normalize ctxt thms =
    1.98    thms
    1.99    |> trivial_let ctxt
   1.100 +  |> trivial_distinct ctxt
   1.101    |> positive_numerals ctxt
   1.102    |> nat_as_int ctxt
   1.103    |> add_pair_rules ctxt