[isabelle] Worrying response from remote_vampire for property of complete_lattice (in Main)



Dear Isabelle experts,

I'm getting strange Isabelle behaviour which I've narrowed down to the following theory.
---
section {* remote_vampire complains about inconsistent axioms *}

theory Issue
  imports Main
begin

lemma "Inf {} = (top::'a::complete_lattice)"

end
---

When I run sledgehammer on the lemma I get the following output.

---
Proof found...
"z3": Try this: by simp (0.3 ms)
"cvc4": Try this: by simp (0.3 ms)
"e": Try this: by simp (0.2 ms)
"spass": Try this: by simp (0.3 ms)
"remote_vampire": The prover derived "False", which could be due to inconsistent axioms (including "sorry"s) or to a bug in Sledgehammer
---

What I'm concerned about is the response from remote_vampire:
are there inconsistencies in the axioms for a complete lattice,
or a bug in Sledgehammer,
or (what remote_vampire fails to acknowledge) a bug in remote_vampire,
or have I done some obvious stupid error that I can't see for looking?

The lemma in question follows directly from the axiom
     Inf_empty [simp]: "â{} = â"
i.e. Inf_empty [simp]: Inf {} = top"
in complete_lattice in Complete_Lattices.thy.

Thanks in advance
Ian




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