# Re: [isabelle] obtain command failure

On Mon, 22 Sep 2008, David Streader wrote:
> I have a small problem with obtain - it fails with predicate " x : Set"
> and some values of Set.
>
> definition inx :: "('a * nat ) set"
> where " inx = {z. EX s n.((s:: 'a) ,n)= z }"
> lemma "~ (EX e. e : inx)"
> proof
> assume as: "EX x. x : inx" show False
> proof -
> from as obtain x where "x : inx" .. --"NOT OK"
Since inx is polymorphic, special care is required when writing closed
expression without any syntactic correlation via fixed variables -- bound
variables (like e, x) and constants (like inx) do not propagate type
constraints.
It works with explicit type constraints, e.g. like this:
lemma "~ (EX e :: 'a * nat. e : inx)"
proof
assume "EX x :: 'a * nat. x : inx"
then obtain x :: "'a * nat" where "x : inx" ..
oops
BTW, you can use pattern comprehension when defining the "inx" set.
E.g. like this:
definition "inx = {(s :: 'a, n :: nat). True}"
Makarius

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