[isabelle-dev] NEWS -> Redundant lemmas

[Brian Huffman]

On Tue, Sep 20, 2011 at 10:03 AM, Christian Urban <urbanc at in.tum.de> wrote:
>
> Hi All,
>
> Somebody recently added in the NEWS the entry
>
>   Redundant lemmas Inf_singleton, Sup_singleton, Inf_binary, Sup_binary,
>   INF_eq, SUP_eq, INF_UNIV_range, SUP_UNIV_range, Int_eq_Inter,
>   INTER_eq_Inter_image, Inter_def, INT_eq, Un_eq_Union, INF_subset,
>   UNION_eq_Union_image, Union_def, UN_singleton, UN_eq have been
>   discarded.

It looks like most of these lemmas were removed in the following changesets:

http://isabelle.in.tum.de/repos/isabelle/rev/22c0857b8aab
http://isabelle.in.tum.de/repos/isabelle/rev/eff5bccc9b76

I was able to put together replacement theorems for a few of these lemmas:

Inf_singleton ~> Inf_insert [where A="{}", unfolded Inf_empty inf_top_right]
Sup_singleton ~> Sup_insert [where A="{}", unfolded Sup_empty sup_bot_right]
INTER_eq_Inter_image ~> INF_def
UNION_eq_Union_image ~> SUP_def
INF_subset ~> INF_superset_mono [OF _ order_refl]

Lemmas Inf_binary could in principle be constructed from Inf_insert,
Inf_empty, and inf_top_right, just like Inf_singleton is, but the
theorem expression would be a lot bigger and uglier (similarly for
Sup_binary).

If Inf_binary and Sup_binary were reinstated, then we could use the
substitutions

Int_eq_Inter ~> Inf_binary [symmetric]
Un_eq_Union ~> Sup_binary [symmetric]

The lemmas INF_UNIV_range and SUP_UNIV_range were not present in
Isabelle2011, so it is not necessary to say anything about their
removal.

Similarly, INF_eq and SUP_eq were not present in Isabelle2011 either.
They are generalizations of INT_eq and UN_eq, so if they were to be
reinstated, the NEWS file could give the substitutions INT_eq ~>
INF_eq and UN_eq ~> SUP_eq.

The NEWS entry calls these lemmas "redundant", but it appears that
none of them are exact duplications or specializations of other
pre-existing lemmas; they can only be said to be redundant in the more
limited sense of "not very useful". I am not suggesting that we need
to keep them all - I do think it is useful to get rid of old cruft
from the libraries from time to time - but I agree with Christian that
the NEWS file should give better hints for those users that might need
to adapt to their absence.

Perhaps we should start using a standardized process for phasing out
legacy theorems, like moving them into a separate theory file
"Legacy.thy" that would not be imported by default, and would be
cleared out after each release. When upgrading Isabelle, users could
import Legacy.thy as needed to get their theories working, and then
work gradually to eliminate the dependencies on it. What do you think?

- Brian