Email Gateway (Aug 22 2022 at 20:18): Email Gateway (Aug 22 2022 at 20:18):From: José Manuel Rodríguez Caballero <josephcmac@gmail.com>
Hello,
In some libraries in Isabelle/HOL I saw the following structure:
proposition uniform_limit_iff:
"uniform_limit S f l F ⟷ (∀e>0. ∀⇩F n in F. ∀x∈S. dist (f n x) (l x) < e)"
lemma uniform_limitD:
"uniform_limit S f l F ⟹ e > 0 ⟹ ∀⇩F n in F. ∀x∈S. dist (f n x) (l x) < e"
lemma uniform_limitI:
"(⋀e. e > 0 ⟹ ∀⇩F n in F. ∀x∈S. dist (f n x) (l x) < e) ⟹ uniform_limit S
f l F"
The disadvantage of this approach is that it increases the search space of
lemmas for automatic reasoning tools. My questions are the following ones:
a) Is there any advantage in including the equivalence A ⟷ B as a lemma,
when we already have both A ⟹ B and B ⟹ A as lemmas?
b) Is there any advantage in including both A ⟹ B and B ⟹ A as lemmas, when
we already have the equivalence A ⟷ B as a lemma?
c) Is there any case when it is useful to have two definitions A and B,
even if we have the fact A ⟷ B? The typical example is:
theorem LIMSEQ_NSLIMSEQ_iff: "f ⇢ L ⟷ f ⇢⇩N⇩S L"
Kind Regards,
José M.
Email Gateway (Aug 22 2022 at 20:18):From: Lawrence Paulson <lp15@cam.ac.uk>
It’s quite common to see a definition (which may be quite technical) supplemented by derived rules that make certain kinds of reasoning easier. In particular we have many introduction rules, with names ending with I and which work with the intro method or “blast intro: …”. Analogously we have elimination rules with names ending with D or E, for “blast dest: …” or “blast elim: …”. The variant forms are also convenient with attributes such as OF and THEN, while the equality forms are convenient with the simplifier.
Larry
Email Gateway (Aug 22 2022 at 20:18):From: Lawrence Paulson <lp15@cam.ac.uk>
In this case it’s surely significant that two notions of limit — one based on traditional epsilon-delta reasoning and the other on nonstandard analysis derived from ultrafilters — are equivalent.
Larry
Last updated: May 06 2024 at 12:29 UTC