[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Questions on conversion/coercion.


I have a question about conversion/coercion. 

I specified two enumerated types. Every member of A type  
is the member of B type. And I want to verify every member 
of A is the member of B (theorem t). But I cannot do it. 
Because the  set A type and the set B type is different. 
How can I prove it? 

comp : THEORY 
  aset : TYPE = {a, b} 
  bset : TYPE = {a, b, c, d, e, f} 
  t : THEOREM FORALL (e1:aset): EXISTS (e2:bset): e1 = e2 
END comp 

I tried to define and use a conversion funtion. It is 
incorrect. What is the false? How can I modify it?
I know that conv function is incorrect (skipping g), 
but I cannot find theorem t is incorrect. 
comp1 : THEORY 
  aset : TYPE = {a, b, g}    
  bset : TYPE = {a, b, c, d, e, f} 

  conv(aele:aset): bset = 
    cases aele OF
      a : a:bset,
      b : b:bset
  t : THEOREM FORALL(e1:aset):EXISTS (e2:bset): conv(e1) = e2
END comp1 

Kim, Tae-ho