[isabelle] Questions about Records

		@page { size: 8.5in 11in; margin: 0.79in }
		P { margin-bottom: 0.08in }
	Hi all,

Thanks to everyone for the previous
replys. I have some questions regarding records. I am giving an
example which is similar to what I want to do. My questions are based
on this example. 

datatype op = a | b | c

record class = 
class_name ::string
class_type :: op

record classext = class +
extension :: “class list”

 datatype sub = “(class, classext)

record  program =
program_name :: string
program_content :: sub

Assume that record class is concretely defined with these 2 definitions:


  class1 :: class


  class1_def: "class1 = (|
class_name = ''man'', class_type = a |)"


  class2 :: class


  class2 _def: "class2 = (|
class_name = ''woman'', class_type = b |)"


Can I extend the record (classext)	from another record (class) and use one of the element of the new	record as the old record ? Similar to the above 'class' definitions, how can I define concretely the 'classext'record which uses the class1 and class2 definitions? When such adefinition has other record definitions embedded in it, can thedefinitions be automatically unfolded and how? Also, how can concretely define the 'program' record?

If I want to define another element inthe 'program' record which can be either of type class or of typeclassext, how can I do it? Should I use datatypes and caseexpressions ? And, how can I concretely define this element? 

Thanks in Advance, 


Looking for last minute shopping deals?  
Find them fast with Yahoo! Search.  http://tools.search.yahoo.com/newsearch/category.php?category=shopping

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