# HG changeset patch
# User boehmes
# Date 1273701233 -7200
# Node ID 1355523fb07d977a61567ea323ab3e3ca976d879
# Parent  d9b9bec6ff8d24d5847db48965af0986b7dbb1d6
added missing rewrite rules for natural min and max

diff -r d9b9bec6ff8d -r 1355523fb07d src/HOL/SMT/Tools/smt_normalize.ML
--- a/src/HOL/SMT/Tools/smt_normalize.ML	Wed May 12 23:53:52 2010 +0200
+++ b/src/HOL/SMT/Tools/smt_normalize.ML	Wed May 12 23:53:53 2010 +0200
@@ -166,10 +166,14 @@
     "a * b = nat (int a * int b)"
     "a div b = nat (int a div int b)"
     "a mod b = nat (int a mod int b)"
+    "min a b = nat (min (int a) (int b))"
+    "max a b = nat (max (int a) (int b))"
     "int (nat (int a + int b)) = int a + int b"
     "int (nat (int a * int b)) = int a * int b"
     "int (nat (int a div int b)) = int a div int b"
     "int (nat (int a mod int b)) = int a mod int b"
+    "int (nat (min (int a) (int b))) = min (int a) (int b)"
+    "int (nat (max (int a) (int b))) = max (int a) (int b)"
     by (simp add: nat_mult_distrib nat_div_distrib nat_mod_distrib
       int_mult[symmetric] zdiv_int[symmetric] zmod_int[symmetric])+}