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