On Tue, Sep 20, 2011 at 10:03 AM, Christian Urban <[email protected]> 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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
