Re: [isabelle-dev] cardinality primitives in Isabelle/HOL?
Hi Larry, if you want to put the definitions and the basic properties in Main, then Fun.thy would probably be the place. But then I would argue that the syntax should be hidden, as users might want to use these symbols for something else. For the advanced material, do you need some theorems from HOL-Cardinals or just the syntax from HOL-Library.Cardinal_Notations in addition to what is already there in Main about cardinals? If it is only the syntax, then a separate theory in HOL-Library is probably a good fit. Otherwise, a separate theory in HOL-Cardinals would make sense. Dmitriy > On 22 Jan 2019, at 15:58, Lawrence Paulson wrote: > > I’m trying to install some of my new material and I’m wondering what to do > with equipollence and related concepts: > > definition eqpoll :: "'a set ⇒ 'b set ⇒ bool" (infixl "≈" 50) > where "eqpoll A B ≡ ∃f. bij_betw f A B" > > definition lepoll :: "'a set ⇒ 'b set ⇒ bool" (infixl "≲" 50) > where "lepoll A B ≡ ∃f. inj_on f A ∧ f ` A ⊆ B" > > definition lesspoll :: "'a set ⇒ 'b set ⇒ bool" (infixl ‹≺› 50) > where "A ≺ B == A ≲ B ∧ ~(A ≈ B)" > > The raw definitions are extremely simple and could even be installed in the > main Isabelle/HOL distribution. The basic properties of these concepts > require few requisites. However, more advanced material requires the > Cardinals development. > > Where do people think these definitions and proofs should be installed? > > 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
Re: [isabelle-dev] cardinality primitives in Isabelle/HOL?
> On 28 Dec 2018, at 19:36, Lawrence Paulson wrote: > > Tons of useful stuff here. > > Some syntactic ambiguities, particularly around the =o relation, which is > also defined as Set_Algebras.elt_set_eq. True. The same holds for +o and *o (which are less widely used in the ordinals library). I'm not sure what a good naming is in these cases. "=o" makes sense for me as "equality on ordinals". It would be ok for me to play with capitalization or other abbreviations of ordinals, e.g., "=O" or "=ord". Maybe Andrei can comment, as he picked the current notation. I don't know what "=o" stands for in the case of Set_Algebras.elt_set_eq (is this a reference to the Oh-notation?) and why there is need for an alternative notation for ∈. I believe the better textbooks are those that write "f ∈ O(g)" instead of "f = O(g)". Along similar lines, I find the notation "f > I don’t suppose there’s any chance of using quotients to define actual > cardinals and use ordinary equality? Not really. "(=o) :: 'a rel ⇒ 'b rel ⇒ bool" is too polymorphic for this to work properly. (The relation arguments are ordinals represented by well-orders.) One can quotient modulo a restricted relation "(=o) :: 'a rel ⇒ 'a rel ⇒ bool", but then the equality on the quotient type won't allow us to compare "|UNIV :: nat set| :: nat rel" to "|UNIV :: real set| :: real rel". > And it still makes sense to introduce the actual notion of equipollence and > similar relations. This is the usual trade-off between many similar definitions with dedicated reasoning support (transitivity, congruence, and monotonicity rules and such) or a few core ones. Possibly an abbreviation is sufficient in this case. Dmitriy ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] cardinality primitives in Isabelle/HOL?
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). Our ITP'14 paper explains the design of the library: http://people.inf.ethz.ch/trayteld/papers/itp14-card/card.pdf Dmitriy > On 27 Dec 2018, at 13:31, Lawrence Paulson wrote: > > I am inclined to introduce these definitions: > > definition lepoll :: "'a set ⇒ 'b set ⇒ bool" (infixl "≲" 50) >where "lepoll A B ≡ ∃f. inj_on f A ∧ f ` A ⊆ B" > > definition eqpoll :: "'a set ⇒ 'b set ⇒ bool" (infixl "≈" 50) >where "eqpoll A B ≡ ∃f. bij_betw f A B” > > They allow, for example, this: > > theorem Schroeder_Bernstein_eqpoll: > assumes "A ≲ B" "B ≲ A" shows "A ≈ B" > using assms unfolding eqpoll_def lepoll_def by (metis Schroeder_Bernstein) > > The names and syntax are borrowed from Isabelle/ZF, and they are needed for > some HOL Light proofs. > > But do they exist in some form already? And are there any comments on those > relation symbols? > > Larry > > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
