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.