# [isabelle] unexpected conversion from real to int

The code below seeks to establish that any real triple (a,b,c) satisfying a
\<ge> b \<ge> c \<ge> 0 also satisfies at least one of the 10 conditions
below (expressions 6, 7/8, 9, 10, 11, 12, 13, 14, 15 or 16). I am running
it in Isabelle2016 under 64-bit Windows 7.
It seems to work, but with an ugly correction for an unexpected type
conversion: if expression 9 does not re-declare 'a' as a real (already
declared as such in expression 6), then 'a', 'b' and 'c' from that term are
cast to int, and the whole term cast back to real_of_int.
Can anyone tell me why this happens, and whether there's a cleaner solution
than to re-declare 'a' as real?
Thank you,
Colin Rowat
University of Birmingham
theory "160429-cores-partition"
imports Real
begin
lemma Coro1: " (* expression 6*)
((real a) < (real b) + (real c) -1.0
| (* expression 7 & 8 *)
(a - b - c \<ge> -1.0) \<and> (-(real a) + b - c) < -1.0
| (* expression 9 *)
(-(real a) + b - c \<ge> -1.0) \<and> (0.0 < c) \<and> (c < a
+b -1.0)
| (* expression 10 *)
(c = 0.0) \<and> (b > 0.0) \<and> (b = a -1.0)
| (* expression 11 *)
(c = 0.0) \<and> (b > abs(1.0 - a))
| (* expression 12 *)
(c \<ge> a + b - 1.0) \<and> (c > 0.0)
| (* expression 13 *)
(a = 1.0) \<and> (b = 0.0) \<and> (c = 0.0)
| (* expression 14 *)
(c = 0.0) \<and> (b > 0.0) \<and> (b \<le> 1.0 -a)
| (* expression 15 *)
(c = 0.0) \<and> (b = 0.0) \<and> (a > b) \<and> (a \<le> 1.0)
| (* expression 16 *)
(c = 0.0) \<and> (b = 0.0) \<and> (a = 0.0)
)
\<and> (a \<ge> b) \<and> (b \<ge> c) \<and> (c \<ge> 0)
" by arith
end

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*