# [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.