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".

Larry Paulson


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 MHonArc.