[isabelle] an inductive datatype and n inductively defined set



Dear Yongjian,

 > Who could introduce more technical papers on the relation between the two
 > features.

I think two good starting pointers to the 
(Isabelle-centric) literature on this 
topic are

 Inductive datatypes in HOL - lessons learned in 
 Formal-Logic Engineering. 
 by Stefan Berghofer and Markus Wenzel

 http://www4.in.tum.de/~berghofe/papers/TPHOLs99.pdf

and

 A fixedpoint approach to (co)inductive and (co)datatype definitions
 by Larry Paulson
 
 http://www.cl.cam.ac.uk/~lp15/papers/Sets/milner-ind-defs.pdf

However, I assume there are experts on this
mailing list, which can give more detailed 
answers.

Best wishes,
Christian





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