Re: [isabelle] Pending sort hypotheses



On 04.07.2012 11:54, Johannes Hölzl wrote:
Am Mittwoch, den 04.07.2012, 11:34 +0200 schrieb Lars Noschinski:

This means, you assumptions are inconsistent. The SORT_CONSTRAINT you
gave adds the assumption, that there exists a type, which is finite, a
perfect_space, and a real_normed_vector. I guess such a type does not
exist -- maybe somebody more familiar with this field can confirm
this?

real_normed_vector includes open_dist, which together with finite
forces it to be a discrete topology, i.e. "!!x. open {x}".
The opposite of a perfect space "!!x. ~ open {x}".

However, I have now idea how blast can deduce False by itself. I don't
think there is any theorem in the library which relates finite with
topology.

I had now a look in the proof terms. One can see, that this proof uses in particular the following three theorems:

not_bounded_univ:
  "¬bounded (UNIV :: ('a :: {perfect_space,real_normed_vector})  set)"

finite_imp_bounded:
  "finite (S :: ('a :: metric_space) set) ⟹ bounded S"

finite_UNIV:
  "finite (UNIV :: ('a :: finite) set)"

If there existed a type 'a satisfying these four sorts, we could prove false (a real_normed_vector is in particular a metric space, so we only need to mention three sorts explicitly):

lemma Y:
assumes S: "SORT_CONSTRAINT('a::{finite,perfect_space,real_normed_vector})"
  shows False
proof -
  from finite_UNIV have "bounded (UNIV :: 'a set)"
    by (rule finite_imp_bounded)
  moreover have "¬bounded (UNIV :: 'a set)"
    by (rule not_bounded_UNIV)
  ultimately show False by metis
qed

So, blast did not really find a proof for you, it just gave you an error message which might lead you into thinking it found a proof.

  -- Lars





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