Question 9
A structure combining information from songs and plays can be defined using the following definition:
SongsAndPlaysList == seq SongDetails
We assume the existence of the following abbreviation:
SongDetails == Id × SongName × Artist × AlbumTitle × Length × Time × Time × N
Here, the details of each song consists of: an identifier; a song name; an artist; an album title; the song length; the date it was added; the last time it was played; and the number of times it has been played.
(a) A valid element of SongsAndPlaysList will: ensure that there are no duplicate identifiers and ensure that any 'last played' time is later than
any 'date added' time. Define such a ValidSongsAndPlaysList structure. (b) Define a specific ValidSongsAndPlaysList, songs_and_plays, the values of which are defined by the values of songs and plays of Question 6.
(c) Show how the set comprehensions of Question 7 might be recast as set comprehensions on the sequence of part (b).
(d) Show how the recursive function of Question 8 might be recast as a function that takes a sequence of type seq SongDetails as input.
Question 10
You have been informed that the following statements are true:
- "If the team wins all of its league matches, then the team will win the league."
- "The team wins the cup if, and only if, the team wins all of its cup matches."
Assume that: AC represents "wins all cup matches"; AL represents "wins all league matches"; WC represents "wins the cup"; and WL represents "wins the league".
By using the above, prove each of the following via a proof tree.
(a) AC Ù AL => WC Ù WL ( where AND = Ù)
(b) AC V AL => WC V WL (where V = or)
Each step in your tree should be labelled and justified by a basic introduction or elimination rule from our system.