Re: [isabelle] an inductive datatype and n inductively defined set



The point of your question is not clear to me. Certainly an algebraic data type can be seen as an instance of an inductive definition, but it can also be seen as a primitive definitional concept in its own right. Because an inductive definition merely identifies a subset of an already existing set, you can only define algebraic datatypes by an inductive definition if you have otherwise demonstrated the existence of a set containing strong enough closure properties. Isabelle's data type package does all the necessary work for you. These technical points have nothing to do with the question of which concept should be adopted when you are defining a model.

Larry Paulson


On 23 Jul 2010, at 10:57, li yongjian wrote:

> Dear all:
> 
> By my understanding, the expressbilty of an inductive datatype and an
> inductively defined set in Isabelle is not the same.
> An inductive datatype can be naturally corresponding to an inductively
> defined set, but not vice and versa.
> 
> Who could introduce more technical papers on the relation between the two
> features.
> 
> Thanks in advance.
> 
> lyj






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