<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<p><font size="+1">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.</font></p>
<p><font size="+1">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".<br>
</font></p>
<p><font size="+1">It would be interesting to know what other users
of Complex_Main think about that.</font></p>
<p><font size="+1">Manuel</font><br>
</p>
<br>
<div class="moz-cite-prefix">On 2017-06-30 16:52, Tobias Nipkow
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:c35384a1-b4a9-7de1-6ee3-0f2f72755e5a@in.tum.de">
<br>
On 30/06/2017 16:39, Manuel Eberl wrote:
<br>
<blockquote type="cite">I do understand that argument, but I am
not sure if Topological_Spaces.subseq is really used /that/
often. Actually, going one step further, it is nothing more than
"strict_mono" restricted to "nat ⇒ nat", so one may well argue
that it is superfluous anyway.
<br>
</blockquote>
<br>
If we can get rid of it all together, surely that is the best
option?
<br>
<br>
Tobias
<br>
<br>
<blockquote type="cite">The possibility of renaming one of them to
"subsequence" or "is_subseq" is, in my opinion, not a
satisfactory solution, since we would then /still/ have two
completely different constants with essentially the same name,
just with an arbitrary artificial difference. We might as well
call one of them subseq'.
<br>
<br>
The advantage of qualified names is that they really allow us to
add disambiguating context to ambiguous names when necessary,
e.g. something like "List.subseq" and
"Topological_Spaces.subseq". Still, as I said, I do understand
that typing such lengthy names is tedious.
<br>
<br>
I currently see the following possible solutions:
<br>
<br>
– find another good name for one of the two things currently
named "subseq" and rename it
<br>
– introduce an arbitrary distinction like "subsequence" or
"is_subseq"
<br>
– move "subseq" to List.thy and make it qualified, so that one
must write "List.subseq"
<br>
– remove Topological_Spaces.subseq entirely, replacing it by
strict_mono
<br>
– leave everything as it is
<br>
<br>
Incidentally, I wonder if it is possible to locally prefer one
of the two constants, i.e. say that, in the following block, I
want "subseq" to mean "Topological_Spaces.subseq". That might
also mitigate the problem of long qualified names.
<br>
<br>
Manuel
<br>
<br>
<br>
<br>
On 2017-06-30 16:23, Tobias Nipkow wrote:
<br>
<blockquote type="cite">In theory that solves the problem, but
the point is that Topological_Spaces.subseq is impractical for
a frequently used symbol. It would be nice if non-quaified
names could be found for this case.
<br>
<br>
Tobias
<br>
<br>
On 30/06/2017 16:14, Lawrence Paulson wrote:
<br>
<blockquote type="cite">Indeed we do.
<br>
Larry
<br>
<br>
<blockquote type="cite">On 28 Jun 2017, at 18:49, Manuel
Eberl <<a class="moz-txt-link-abbreviated" href="mailto:eberlm@in.tum.de">eberlm@in.tum.de</a>
<a class="moz-txt-link-rfc2396E" href="mailto:eberlm@in.tum.de"><mailto:eberlm@in.tum.de></a>> wrote:
<br>
<br>
Yes, I noticed that as well. I decided to leave it that
way since, well,
<br>
we do have qualified names.
<br>
</blockquote>
<br>
<br>
<br>
_______________________________________________
<br>
isabelle-dev mailing list
<br>
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<br>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
<br>
<br>
</blockquote>
<br>
<br>
<br>
_______________________________________________
<br>
isabelle-dev mailing list
<br>
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<br>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
<br>
</blockquote>
<br>
<br>
<br>
_______________________________________________
<br>
isabelle-dev mailing list
<br>
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<br>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
<br>
<br>
</blockquote>
<br>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
isabelle-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
</pre>
</blockquote>
<br>
</body>
</html>