Email Gateway (Aug 17 2022 at 14:14): Email Gateway (Aug 17 2022 at 14:14):From: jdavis27@uiuc.edu
Hello,
The following snippet works as expected in Isabelle2005:
ML "add_path \"$ISABELLE_HOME/src/HOL/Real\"";
theory Test = Main + Real:
lemma "ALL a. a --> a" by auto;
lemma "(1::real) + (1::real) = (2::real)" by arith;
I would also like to do something like this:
lemma "(1.5::real) + (1.5::real) = (3.0::real)" by arith;
The first period raises a syntax error in Isabelle2005.
What is the correct way to specify a real constant
as a mixed decimal?
Thanks,
Justin S. Davis
Formal Methods Group @ UIUC
Email Gateway (Aug 17 2022 at 14:14):From: nipkow@in.tum.de
lemma "(1.5::real) + (1.5::real) = (3.0::real)" by arith;
Isabelle does not support the dot-syntax for real numbers. You have to write
something like 15/10:
lemma "15/10 + 15/10 = (3::real)";
by arith
lemma "(1::real) * (1::real) = (1::real)";
lemma "(1::real) / (1::real) = (1::real)";
Both are solved by simp.
Tobias
Email Gateway (Aug 17 2022 at 14:14):From: Lawrence Paulson <lp15@cam.ac.uk>
Here I suggest that you build the logic HOL-Complex and then use as
your first line
theory Test imports Complex_Main
Larry Paulson
Last updated: May 03 2024 at 08:18 UTC