# [isabelle] obtain command failure

Hi

` 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"
But the expanded existential elimination works
lemma "~ (EX e. e : inx)"
proof
assume as: "EX x. x : inx" show False
proof -
from as show ?thesis
proof
fix x assume "x : inx" show ?thesis --"OK"
oops

`And wit a small change to the definition of the set the obtain command
``works.
`
definition inw :: "(nat * nat) set"
where " inw = {z. EX n . (1,n) = z }"
lemma "~ (EX e. e : inw)"
proof
assume as: "EX x. x : inw" show False
proof -
from as obtain x where "x : inw" .. --"OK"
oops

`Hope this is helpful and I have not slipped up some where. Example is
``in attached file.
`
kind regards
david streader

theory ex
imports Main
begin
definition inw :: "(nat * nat) set"
where " inw = {z. EX n . (1,n) = z }"
definition inx :: "('a * nat ) set"
where " inx = {z. EX s n.((s:: 'a) ,n)= z }"
lemma "~ (EX e. e : inw)"
proof
assume as: "EX x. x : inw" show False
proof -
from as obtain x where "x : inw" .. --"OK"
oops
lemma "~ (EX e. e : inx)"
proof
assume as: "EX x. x : inx" show False
proof -
from as show ?thesis
proof
fix x assume "x : inx" show ?thesis --"OK"
oops
lemma "~ (EX e. e : inx)"
proof
assume as: "EX x. x : inx" show False
proof -
from as obtain x where "x : inx" .. --"NOT OK"

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