<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<title></title>
</head>
<body>
<div name="messageBodySection">
<div dir="auto">In the AFP we have four separate copies of the definition<br>
<br>
definition list :: "nat \<Rightarrow> 'a set \<Rightarrow> 'a list set"<br>
where<br>
"list n A = {xs. size xs = n \<and> set xs \<subseteq> A}"<br>
<br>
Interestingly, the exact same concept is coded in three different ways in the four definitions. We also have a number of theorems in the repository referring to this concept:<br>
<br>
finite_lists_length_eq<br>
set_n_lists<br>
card_lists_length_eq<br>
lists_length_Suc_eq<br>
<br>
And we have three copies of Listn.thy in MicroJava and JinjaThreads. Could maybe some fragment of this, if not the whole thing, be moved into Library?</div>
</div>
<div name="messageSignatureSection"><br>
<div class="matchFont">
<div dir="auto">Larry</div>
</div>
</div>
</body>
</html>