Re: [isabelle] Nonlinear arithmetic for real numbers
Use "auto" or "simp" to perform constant folding.
We aren't especially geared up for real literals, but you can perform
simple arithmetic on fixed-point constants as shown in this example:
lemma "3/10 + 70/100 = (x::real)"
apply (simp add: Ring_and_Field.add_frac_eq)
This simplifies to "x=1".
On 14 Mar 2006, at 20:44, <jdavis27 at uiuc.edu> <jdavis27 at uiuc.edu> wrote:
I am having difficulty proving the following:
lemma "(1::real) * (1::real) = (1::real)";
lemma "(1::real) / (1::real) = (1::real)";
The "arith" tactic does not support multiplication, as
explained in previous messages.
This archive was generated by a fusion of
Pipermail (Mailman edition) and