--- a/src/HOL/SMT/Tools/smt_normalize.ML Wed May 12 23:53:56 2010 +0200
+++ b/src/HOL/SMT/Tools/smt_normalize.ML Wed May 12 23:53:57 2010 +0200
@@ -9,9 +9,9 @@
numerals),
* embed natural numbers into integers,
* add extra rules specifying types and constants which occur frequently,
+ * fully translate into object logic, add universal closure,
* lift lambda terms,
- * make applications explicit for functions with varying number of arguments,
- * fully translate into object logic, add universal closure.
+ * make applications explicit for functions with varying number of arguments.
*)
signature SMT_NORMALIZE =
@@ -45,28 +45,6 @@
-(* simplification of trivial let expressions (whose bound variables occur at
- most once) *)
-
-local
- fun count i (Bound j) = if j = i then 1 else 0
- | count i (t $ u) = count i t + count i u
- | count i (Abs (_, _, t)) = count (i + 1) t
- | count _ _ = 0
-
- fun is_trivial_let (Const (@{const_name Let}, _) $ _ $ Abs (_, _, t)) =
- (count 0 t <= 1)
- | is_trivial_let _ = false
-
- fun let_conv _ = if_true_conv is_trivial_let (Conv.rewr_conv @{thm Let_def})
-in
-fun trivial_let ctxt =
- map ((Term.exists_subterm is_trivial_let o Thm.prop_of) ??
- Conv.fconv_rule (More_Conv.top_conv let_conv ctxt))
-end
-
-
-
(* simplification of trivial distincts (distinct should have at least
three elements in the argument list) *)
@@ -507,7 +485,6 @@
fun normalize ctxt thms =
thms
- |> trivial_let ctxt
|> trivial_distinct ctxt
|> rewrite_bool_cases ctxt
|> normalize_numerals ctxt