Artur,
You can use:
a(conv_tac(ONCE_MAP_C z_float_conv));
to change things like "3.0" into "real 3" or "3.5" into "7/2" and then
rewriting in the proof context 'z_reals will do the arithmetic for you.
We don't do this automatically in the proof context 'z_reals in case
you have floating l
Rob,
Thank you.
Just one more question: and how about floating numbers?
How to prove it?
For example:
set_merge_pcs["'z_reals", "z_library"];
set_goal([], %SZT% 0.4 %mem% 0.1 ..%down%R 1.9 %>%);
a(rewrite_tac[z_%bbR%_dot_dot_def]);
With those steps, ProofPower change the goal to:
%SZT%0.1 %le
Artur,
You may like to know that there is a so-called "component" proof context called
'z_reals which will make evaluation of real arithmetic expressions happen
automatically when you rewrite.
Try:
set_merge_pcs["'z_reals", "z_library"];
set_goal([], %SZT% real 30 %mem% real 20 ..%down%R re
Hi there
Now I know how to prove it: using z_R_<=_conv.
Thanks anyway,
Artur
2009/3/25 Artur Oliveira Gomes
> Hi there,
>
> How could I prove that given two real numbers, 20 and 30, that 20 <=40?
> Moreover, given three real numbers, 20, 30 and 40,
> how could I prove that 30 20..40.
>
> Reg
