[isabelle-dev] [isabelle] Good name for "sublist" predicates

[Sebastien Gouezel]

Le 30/06/2017 à 16:57, Manuel Eberl a écrit :
> I agree about 90%, I think, but one could argue that "subseq" contains
> additional meta-information: the semantic meaning is that it is a
> strictly monotonic function, but the idea behind it is that it describes
> a sub-sequence of some other sequence.
>
> Still, I for one think this is not really worth the trouble of keeping
> an entirely separate constant around, especially because "subseq h" does
> not make much sense: "h" itself is not a subsequence of anything, "f ∘
> h" is a sub-sequence of "f".
>
> It would be interesting to know what other users of Complex_Main think
> about that.

I used subseq quite heavily in my ergodic theory developments. From
a mathematician point of view, taking subsequences of sequences
from nat to nat is very common and very useful in analysis (much
more than taking subsequences of lists). For instance, the fact that a 
sequence of functions which converges in L^2 has a subsequence which 
converges everywhere, is extremely powerful. Having to type
topological_spaces.subseq all the time would be very cumbersome, on
the other hand using something like subsequence would be perfectly
OK (and I am strongly in favour of keeping it).

By the way, I recently encountered a similar (and even more nasty)
name clash, with compact. The following works perfectly

theory Foo
   imports Analysis
begin

lemma infdist_compact_attained:
   assumes "compact C" "C ≠ {}"
   shows "∃c∈C. infdist x C = dist x c"
proof -
   have "∃c∈C. ∀d∈C. dist x c ≤ dist x d"
     by (rule continuous_attains_inf[OF assms], intro continuous_intros)
   then show ?thesis unfolding infdist_def using `C ≠ {}`
     by (metis antisym bdd_below_infdist cINF_lower le_cINF_iff)
qed

end


But if one imports Probability instead of Analysis, then compact
becomes the one from Complete_Partial_Order2 (which, I think, is
much less commonly used than the compactness for topological
spaces). Strangely enough, even replacing compact with
topological_space.compact does not solve the issue.

Sebastien Gouezel