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

2018-12-27 Thread Traytel Dmitriy
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

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

2018-12-30 Thread Traytel Dmitriy
> 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

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

2019-01-23 Thread Traytel Dmitriy
gt; > 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 m