# Re: [isabelle] Redundant Information?

*To*: José Manuel Rodríguez Caballero <josephcmac at gmail.com>
*Subject*: Re: [isabelle] Redundant Information?
*From*: Lawrence Paulson <lp15 at cam.ac.uk>
*Date*: Mon, 22 Jul 2019 11:28:11 +0100
*Cc*: cl-isabelle-users at lists.cam.ac.uk
*In-reply-to*: <CAA8xVUgxQ=HqRj3=k5x+x_Y7C_=5NS1ugFe0XzJKLC0Atmmn0Q@mail.gmail.com>
*References*: <CAA8xVUgxQ=HqRj3=k5x+x_Y7C_=5NS1ugFe0XzJKLC0Atmmn0Q@mail.gmail.com>

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
> On 22 Jul 2019, at 08:22, José Manuel Rodríguez Caballero <josephcmac at gmail.com> wrote:
>
> 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?

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*