Re: [isabelle] Redundant Information?



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.