[mizar] fraenkel terms over possibly empty types

[Jesse Alama <alama@stanford.edu>]

While cleaning up my MIZAR proof of Euler's polyhedron formula, I came
across a problem that I was unable to solve satisfactorily, and I'm not
entirely sure why; I thought I would pose the problem on the mailing
list to see what the experts think.

The problem is this: for the fraenkel term

  X := (*) { x where x is Element of A : <whatever> }

I was unable to prove the typing judgment

  X is Subset of A .

A is a term that depends on some parameters, and it is not provably non
empty (for some values of the paramters it is provably empty, for other
values it is provably non empty).  I first tried showing

(**)  X c= A,

which suffices to get the desired typing judgment, but I couldn't prove
the subset relation directly.  Still focusing on the subset relation
(**), I then tried splitting into cases, depending on whether A is
empty:

  X c= A
  proof  
    per cases;
    suppose A is empty;
      X = {}
      proof
        <...>
      end;
      hence thesis;
    end;
    suppose A is non empty;
      <...>
      hence thesis;
    end;
  end;

I can get the second case to go through, but the first case, where A is
assumed to be empty, gives me trouble: I can't finish the proof that X
is empty.

I then gave up on (*) and moved to

  X := (***) { x where x is Element of A : <whatever> & x in A }

With this change my proofs go through, but (***) seems ham-handed to me.
My question for the experts: what other ways are there of dealing with
the problem besides (***)?  Why was I unable to get the desired typing
judgment with (*)?

Thanks,

Jesse

-- 
Jesse Alama (alama@stanford.edu)
*65: "thesis" is allowed only inside a proof