# HG changeset patch
# User nipkow
# Date 1238768270 -7200
# Node ID 5dc392a59bb70aae42fbdefd50ba6f5d46f53f64
# Parent  29eb80cef6b74f0f683c1876361312a554f30ec7
Finite_Set: lemma
IsarRef: attribute arith

diff -r 29eb80cef6b7 -r 5dc392a59bb7 doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Apr 03 09:27:31 2009 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Apr 03 16:17:50 2009 +0200
@@ -756,6 +756,7 @@
 text {*
   \begin{matharray}{rcl}
     @{method_def (HOL) arith} & : & @{text method} \\
+    @{attribute_def (HOL) arith} & : & @{text attribute} \\
     @{attribute_def (HOL) arith_split} & : & @{text attribute} \\
   \end{matharray}
 
@@ -763,11 +764,14 @@
   (on types @{text nat}, @{text int}, @{text real}).  Any current
   facts are inserted into the goal before running the procedure.
 
-  The @{attribute (HOL) arith_split} attribute declares case split
-  rules to be expanded before the arithmetic procedure is invoked.
+  The @{attribute (HOL) arith} attribute declares facts that are
+  always supplied to the arithmetic provers implicitly.
 
-  Note that a simpler (but faster) version of arithmetic reasoning is
-  already performed by the Simplifier.
+  The @{attribute (HOL) arith_split} attribute declares case split
+  rules to be expanded before @{method_def (HOL) arith} is invoked.
+
+  Note that a simpler (but faster) arithmetic prover is
+  already invoked by the Simplifier.
 *}
 
 
diff -r 29eb80cef6b7 -r 5dc392a59bb7 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Apr 03 09:27:31 2009 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Apr 03 16:17:50 2009 +0200
@@ -764,6 +764,7 @@
 \begin{isamarkuptext}%
 \begin{matharray}{rcl}
     \indexdef{HOL}{method}{arith}\hypertarget{method.HOL.arith}{\hyperlink{method.HOL.arith}{\mbox{\isa{arith}}}} & : & \isa{method} \\
+    \indexdef{HOL}{attribute}{arith}\hypertarget{attribute.HOL.arith}{\hyperlink{attribute.HOL.arith}{\mbox{\isa{arith}}}} & : & \isa{attribute} \\
     \indexdef{HOL}{attribute}{arith\_split}\hypertarget{attribute.HOL.arith-split}{\hyperlink{attribute.HOL.arith-split}{\mbox{\isa{arith{\isacharunderscore}split}}}} & : & \isa{attribute} \\
   \end{matharray}
 
@@ -771,11 +772,14 @@
   (on types \isa{nat}, \isa{int}, \isa{real}).  Any current
   facts are inserted into the goal before running the procedure.
 
-  The \hyperlink{attribute.HOL.arith-split}{\mbox{\isa{arith{\isacharunderscore}split}}} attribute declares case split
-  rules to be expanded before the arithmetic procedure is invoked.
+  The \hyperlink{attribute.HOL.arith}{\mbox{\isa{arith}}} attribute declares facts that are
+  always supplied to the arithmetic provers implicitly.
 
-  Note that a simpler (but faster) version of arithmetic reasoning is
-  already performed by the Simplifier.%
+  The \hyperlink{attribute.HOL.arith-split}{\mbox{\isa{arith{\isacharunderscore}split}}} attribute declares case split
+  rules to be expanded before \indexdef{HOL}{method}{arith}\hypertarget{method.HOL.arith}{\hyperlink{method.HOL.arith}{\mbox{\isa{arith}}}} is invoked.
+
+  Note that a simpler (but faster) arithmetic prover is
+  already invoked by the Simplifier.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r 29eb80cef6b7 -r 5dc392a59bb7 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Apr 03 09:27:31 2009 +0200
+++ b/src/HOL/Finite_Set.thy	Fri Apr 03 16:17:50 2009 +0200
@@ -1812,6 +1812,10 @@
   "finite S ==> (ALL x : S. f x > (0::nat)) ==> setprod f S > 0"
 using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
 
+lemma setprod_pos_nat_iff[simp]:
+  "finite S ==> (setprod f S > 0) = (ALL x : S. f x > (0::nat))"
+using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
+
 lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
   (setprod f (A Un B) :: 'a ::{field})
    = setprod f A * setprod f B / setprod f (A Int B)"