[isabelle] Problems with Real addition



Hi,

I'm trying out addition in Real, but have run into some problems. Does
anyone know why the first example below doesn't work but the second does? Is
it a problem with the types?

1)

theory Test
imports Real
begin

typedecl T

consts
F :: "T => real"
t :: "T"

axioms
ax : "F(t) = 0"

lemma test: "EX x. F(x) + 1 ~= 0"
using ax
by auto

2)

theory Test
imports Real
begin

typedecl T

consts
F :: "T => real"
t :: "T"

axioms
ax : "F(t) = 0"

lemma test: "EX x. F(x) + 0 = 0"
using ax
by auto

Thanks in advance for any help.

Regards,
Steve




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