author boehmes Wed, 12 May 2010 23:53:54 +0200 changeset 36890 0ab4217a07b1 parent 36889 1355523fb07d child 36891 e0d295cb8bfd
normalize numerals: also rewrite Numeral0 into 0
```--- a/src/HOL/SMT/Tools/smt_normalize.ML	Wed May 12 23:53:53 2010 +0200
+++ b/src/HOL/SMT/Tools/smt_normalize.ML	Wed May 12 23:53:54 2010 +0200
@@ -5,7 +5,8 @@
* unfold trivial let expressions,
* simplify trivial distincts (those with less than three elements),
* rewrite bool case expressions as if expressions,
-  * replace negative numerals by negated positive numerals,
+  * normalize numerals (e.g. replace negative numerals by negated positive
+    numerals),
* embed natural numbers into integers,
* add extra rules specifying types and constants which occur frequently,
* lift lambda terms,
@@ -109,20 +110,22 @@

-(* rewriting of negative integer numerals into positive numerals *)
+(* normalization of numerals: rewriting of negative integer numerals into
+   positive numerals, Numeral0 into 0, Numeral1 into 1 *)

local
-  fun neg_numeral @{term Int.Min} = true
-    | neg_numeral _ = false
-  fun is_number_sort thy T = Sign.of_sort thy (T, @{sort number_ring})
-  fun is_neg_number ctxt (Const (@{const_name number_of}, T) \$ t) =
-        Term.exists_subterm neg_numeral t andalso
-        is_number_sort (ProofContext.theory_of ctxt) (Term.body_type T)
-    | is_neg_number _ _ = false
+  fun is_number_sort ctxt T =
+    Sign.of_sort (ProofContext.theory_of ctxt) (T, @{sort number_ring})
+
+  fun is_strange_number ctxt (t as Const (@{const_name number_of}, _) \$ _) =
+        (case try HOLogic.dest_number t of
+          SOME (T, i) => is_number_sort ctxt T andalso i < 2
+        | NONE => false)
+    | is_strange_number _ _ = false

val pos_numeral_ss = HOL_ss
+    addsimps [@{thm Int.number_of_Pls}, @{thm Int.numeral_1_eq_1}]
@@ -132,12 +135,12 @@
"Int.Bit1 (- k) = - Int.Bit1 (Int.pred k)"

-  fun pos_conv ctxt = if_conv (is_neg_number ctxt)
+  fun pos_conv ctxt = if_conv (is_strange_number ctxt)
(Simplifier.rewrite (Simplifier.context ctxt pos_numeral_ss))
Conv.no_conv
in
-fun positive_numerals ctxt =
-  map ((Term.exists_subterm (is_neg_number ctxt) o Thm.prop_of) ??
+fun normalize_numerals ctxt =
+  map ((Term.exists_subterm (is_strange_number ctxt) o Thm.prop_of) ??
Conv.fconv_rule (More_Conv.top_sweep_conv pos_conv ctxt))
end

@@ -532,7 +535,7 @@
|> trivial_let ctxt
|> trivial_distinct ctxt
|> rewrite_bool_cases ctxt
-  |> positive_numerals ctxt
+  |> normalize_numerals ctxt
|> nat_as_int ctxt