Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Finite_Set.card_ge_0_finite and a few other le...

Email Gateway (Aug 19 2022 at 11:46):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Christoph,

as Finite_Set.card_ge_0_finite reads as follows

lemma card_ge_0_finite:
"card A > 0 ⟹ finite A"
by (rule ccontr) simp

i.e. as there is ">" ("greater than") and not ">=" ("greater or equal"),
shouldn't it be renamed into card_gt_0_finite?

the naming conventions for comparisions are not wholly consistent, but
the following is quote usual:

< less
<= less_eq, le
> greater
>= greater_eq, ge

So gt and lt are not among those.

The last two only occur with at least one argument fixed, since
otherwise it would just be < or <=.

The following command line helps to identify more such candidates:

find ~/tools/Isabelle2013/src/HOL -name '*.thy' | xargs egrep -A 5
"(lemma|theorem) .*_ge_"

Use a larger number than 5 to find lemmas with a lot of assumptions.

If you are eager to pursue a consolidation here, I would indeed
recommend as first step to compile a list of candidates.

Cheers,
Florian
signature.asc

Email Gateway (Aug 19 2022 at 11:46):

From: Makarius <makarius@sketis.net>
Just two side-remarks on finding things in Isabelle:

* Searching sources works best with hypersearch in jedit, which is one
of the big assets of that editor. It also supports regular
expressions (according to the Java standard library).

* Finding within a given formal context works via the 'find_theorems'
command. It allows basic patterns on theorem names as well. See the
documentation in isar-ref.

Makarius

Email Gateway (Aug 19 2022 at 12:01):

From: Christoph LANGE <math.semantic.web@gmail.com>
Dear all,

as Finite_Set.card_ge_0_finite reads as follows

lemma card_ge_0_finite:
"card A > 0 ⟹ finite A"
by (rule ccontr) simp

i.e. as there is ">" ("greater than") and not ">=" ("greater or equal"),
shouldn't it be renamed into card_gt_0_finite?

The following command line helps to identify more such candidates:

find ~/tools/Isabelle2013/src/HOL -name '*.thy' | xargs egrep -A 5
"(lemma|theorem) .*_ge_"

Use a larger number than 5 to find lemmas with a lot of assumptions.

Cheers,

Christoph

Last updated: Apr 25 2024 at 16:19 UTC