Re: [isabelle-dev] cardinality primitives in Isabelle/HOL?
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. Larry > 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 isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Update of Haskell Stack
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 user:wenzelm date:Fri Dec 28 19:01:35 2018 +0100 files: etc/settings description: 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 description: 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 https://github.com/commercialhaskell/lts-haskell#readme 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: https://github.com/Naproche/Naproche-SAD/commit/2af938e09a61c14f57af40679bb340a92b521331 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. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
