[isabelle-dev] Redundant definitions in Analysis

[Fabian Immler]

On 3/7/2019 7:36 AM, Lawrence Paulson wrote:
> In Analysis, we have two equivalent definitions of continuous functions between two topological spaces:
> 
> lemma "continuous_map X Y f = continuous_on_topo X Y f"
>    by (auto simp add: continuous_map_def continuous_on_topo_def vimage_def image_def Collect_conj_eq inf_commute)
> 
> The first one comes from HOL Light and is defined in Abstract_Topology. The latter is declared in Function_Topology.
> 
> Obviously we need to eliminate one of them, and I prefer the former name. The latter is more logical but clunky, especially when compound with others in theorem names.
Sébastien might have a stronger opinion (I don't), but I would also go 
for continuous_map: it is in line with open_map, closed_map, 
quotient_map (which we don't have as constants, but use in theorem 
names). Moreover, we have more occurrences of continuous_map (174+0 vs 
83+39 in isabelle+AFP).

Fabian

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5581 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190311/967df179/attachment.bin>