--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Apr 03 12:08:09 2009 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Apr 03 16:18:14 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.
*}
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Apr 03 12:08:09 2009 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Apr 03 16:18:14 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%
%
--- a/src/HOL/Finite_Set.thy Fri Apr 03 12:08:09 2009 +0200
+++ b/src/HOL/Finite_Set.thy Fri Apr 03 16:18:14 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)"