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.
> 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