Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Questions about Records


view this post on Zulip Email Gateway (Aug 18 2022 at 11:32):

From: Rajesh Karunamurthy <rajesh.karuna@yahoo.com>
<!--
@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)
list”

record program =
program_name :: string
program_content :: sub

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

definition

class1 :: class

where

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

definition

class2 :: class

where

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,

Rajesh

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


Last updated: May 03 2024 at 04:19 UTC