[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.