<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<p>I have been very busy, but I will find time to work on it. <br>
</p>
<p>Viorel<br>
</p>
<br>
<div class="moz-cite-prefix">On 11/23/2017 6:46 PM, Lawrence Paulson
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:4D913E87-1921-451E-B75A-4E4142F77021@cam.ac.uk">
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
Whatever happened with this? The new release has been out for a
while, and it would make sense to integrate your work now, well
before any thought of a new release.<br class="">
<div class="">
<span class="Apple-style-span" style="border-collapse: separate;
font-family: Helvetica; font-size: 11px;
font-variant-ligatures: normal; font-variant-east-asian:
normal; font-variant-position: normal; line-height: normal;
border-spacing: 0px;">
<div style="word-wrap: break-word; -webkit-nbsp-mode: space;
-webkit-line-break: after-white-space;" class="">
<div class="">Larry</div>
</div>
</span>
</div>
<div><br class="">
<blockquote type="cite" class="">
<div class="">On 27 Aug 2017, at 15:59, Viorel Preoteasa <<a
href="mailto:viorel.preoteasa@aalto.fi" class=""
moz-do-not-send="true">viorel.preoteasa@aalto.fi</a>>
wrote:</div>
<br class="Apple-interchange-newline">
<div class="">
<div class="">I managed to integrate the new complete
distributive lattice into HOL library.<br class="">
<br class="">
The changes are these:<br class="">
<br class="">
Complete_Lattice.thy<br class="">
- replaced the complete_distrib_lattice with the new
stronger version.<br class="">
- moved some proofs about complete_distrib_lattice and
some instantiations to Hilbert_Choice<br class="">
<br class="">
Hilbert_Choice.thy<br class="">
- added all results complete_distrib_lattice, including
instantiations<br class="">
of set, fun that uses uses Hilbert choice.<br class="">
<br class="">
Enum.thy<br class="">
- new proofs that finite_3 and finite_4 are
complete_distrib_lattice.<br class="">
- I added here the classes finite_lattice and
finite_distrib_lattice<br class="">
and proved that they are complete. This simplified quite
much the proofs<br class="">
that finite_3 and finite_4 are complete_distrib_lattice.<br
class="">
<br class="">
Predicate.thy<br class="">
- new proof that predicates are complete_distrib_lattice.<br
class="">
<br class="">
I compiled HOL in Isabelle2017-RC0 using<br class="">
<br class="">
isabelle build -v -c HOL<br class="">
<br class="">
and I got:<br class="">
<br class="">
Timing HOL (2 threads, 266.231s elapsed time, 487.094s cpu
time, 43.344s GC time, factor 1.83)<br class="">
Finished HOL (0:04:26 elapsed time)<br class="">
<br class="">
Finished at Sun Aug 27 17:41:30 GMT+3 2017<br class="">
0:04:37 elapsed time<br class="">
<br class="">
But I don't now how to go from here to have these changes
into Isabelle.<br class="">
<br class="">
There is also AFP. If there are instantiations of
complete_distrib_lattice, then most probably they will
fail.<br class="">
<br class="">
One simple solution in this case could be to keep also the<br
class="">
old complete_distrib_lattice as
complete_pseudo_distrib_lattice.<br class="">
<br class="">
Viorel<br class="">
<br class="">
<br class="">
On 8/26/2017 3:06 PM, Lawrence Paulson wrote:<br class="">
<blockquote type="cite" class="">
<blockquote type="cite" class="">On 25 Aug 2017, at
20:14, Viorel Preoteasa <<a
href="mailto:viorel.preoteasa@aalto.fi" class=""
moz-do-not-send="true">viorel.preoteasa@aalto.fi</a>
<<a href="mailto:viorel.preoteasa@aalto.fi"
class="" moz-do-not-send="true">mailto:viorel.preoteasa@aalto.fi</a>>>
wrote:<br class="">
<br class="">
One possible solution:<br class="">
<br class="">
Add the new class in Complete_Lattice.thy, replacing
the existing class<br class="">
<br class="">
Prove the instantiations and the complete_linearord
subclass later<br class="">
in Hilbert_Choice.<br class="">
<br class="">
On the other hand, it seems inconvenient to have the
Hilbert Choice<br class="">
to depend on so many other theories.<br class="">
</blockquote>
I’d prefer this provided the instantiations aren’t
needed earlier.<br class="">
The delay in the introduction of the Axiom of Choice is
partly historical, but it’s worth noting how much of HOL
can be developed without it.<br class="">
Larry<br class="">
</blockquote>
</div>
</div>
</blockquote>
</div>
<br class="">
</blockquote>
<br>
</body>
</html>