[isabelle] Redundant Information?



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.



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