[isabelle-dev] Update of Haskell Stack

2018-12-28 Thread Makarius
Here are some notable changes concerning the Haskell Stack, which is a
build tool with a package repository behind it:

changeset:   69526:5574d504cf36
tag: tip
date:Fri Dec 28 19:01:35 2018 +0100
files:   etc/settings
more conservative update of Haskell stack (amending 04e54f57a869): 13.0
still lacks notable packages like "Agda" or "darcs";

changeset:   69512:04e54f57a869
parent:  69506:7d59af98af29
user:Lars Hupel 
date:Thu Dec 27 17:36:19 2018 +0100
files:   etc/settings src/Pure/General/path.ML
update LTS Haskell version

I am myself still in the process of learning how the Stack community and
release process works. Spending 5 min with the announcement of lts-13.0
from Isabelle/04e54f57a869 leaves the impression that a new major
release is merely the factual start for package maintainers to become
serious about updating and publishing their stuff.

Haskell Stack LTS versions should appear every 3-6 months -- according
to the official statement

So it looks like it is better to stay one major release version behind
the frontier of ongoing LTS development. Moreover, I have so far
refrained from updating minor versions without particular reasons: it
always causes a lot of network traffic and disk usage increase for local
.stack directories.

Here is also a concrete project that refers to Isabelle/Haskell from
isabelle-dev and is in sync with its Stack version:


This proves the use and usability of the emerging Isabelle/Haskell
infrastructure. In the longer term it might help more users out there to
develop Haskell-based projects for Isabelle; or just use other ITP
systems like Agda -- when OPAM gets into better shape we could also
apply this principle to Coq.

Overall, the general approach of the Isabelle distribution is to deliver
canonical versions of add-on tools that just work without manual tinkering.

Thus "latest" things require more than one close look before adopting them.

isabelle-dev mailing list

Re: [isabelle-dev] cardinality primitives in Isabelle/HOL?

2018-12-28 Thread Lawrence Paulson
Tons of useful stuff here.

Some syntactic ambiguities, particularly around the =o relation, which is also 
defined as Set_Algebras.elt_set_eq.

I don’t suppose there’s any chance of using quotients to define actual 
cardinals and use ordinary equality? And it still makes sense to introduce the 
actual notion of equipollence and similar relations.


> On 27 Dec 2018, at 20:29, Makarius  wrote:
> On 27/12/2018 17:45, Traytel  Dmitriy wrote:
>> Hi Larry,
>> the HOL-Cardinals library might be just right for the purpose:
>> theory Scratch
>>  imports "HOL-Cardinals.Cardinals"
>> begin
>> lemma "|A| ≤o |B| ⟷ (∃f. inj_on f A ∧ f ` A ⊆ B)"
>>  by (rule card_of_ordLeq[symmetric])
>> lemma "|A| =o |B| ⟷ (∃f. bij_betw f A B)"
>>  by (rule card_of_ordIso[symmetric])
>> lemma
>>  assumes "|A| ≤o |B|" "|B| ≤o |A|"
>>  shows "|A| =o |B|"
>>  by (simp only: assms ordIso_iff_ordLeq)
>> end
>> The canonical entry point for the library is the above 
>> HOL-Cardinals.Cardinals. Many of the theorems and definitions are already in 
>> Main, because the (co)datatype package is based on them. The syntax is 
>> hidden in main—one gets it by importing HOL-Library.Cardinal_Notations 
>> (which HOL-Cardinals.Cardinals does transitively).
> It would be great to see this all consolidated and somehow unified, i.e.
> some standard notation in Main as proposed by Larry (potentially as
> bundles as proposed by Florian), and avoidance of too much no_syntax
> remove non-standard notation from Main.
>   Makarius

isabelle-dev mailing list