Email Gateway (Aug 19 2022 at 13:19): Email Gateway (Aug 19 2022 at 13:19):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Gottfried,
This looks like a primrec_new bug in Isabelle2013-2 (it works with "the" development
version, e.g., 761e40ce91bc). As a workaround, you can wrap x in some function such as id.
primrec_new get_hS_FAILS :: "hD => hD fset" where
"get_hS_FAILS hEM = {||}"
|"get_hS_FAILS (hS x) = id x"
Best,
Andreas
Email Gateway (Aug 19 2022 at 13:19):From: G B <igbi@gmx.com>
[by Andreas]...As a workaround, you can wrap x in some function such as id.
Andreas, thanks again.
Incidentally, I'm wondering whether you really need the "hEM" constructor in
datatype_new hD = hEM | hS "hD fset"
The canonical definition of hereditarily finite sets reads
datatype_new hD = hS "hD fset"
Jasmin,
No, I don't, but I would have wasted a lot of time to find out that I
don't, if you wouldn't have told me, so I'm grateful for you taking the
time to tell me, and for other things also.
I am a foreigner, living among wizards, where I've known mainly only
about the canonical Canon_List_Rule, in which there is Nil and Cons x
xs. Because the Canon_List_Rule demands the existence of Nil, I
concluded that I must claim the existence of a hEM.
True mathematical elegance is a statement that is so simple, it's hard
for a novice to understand what information the statement contains.
Now, I understand the magic of the polymorphic empty set, {||}, along
with the fact that it happens to be type correct for the constructor
hs. The understanding about {||} being type correct didn't come
until I started to try and simplify another datatype, based on your
question/suggestion.
This demonstrates the value of occasionally interacting with actual
humanoids, rather than only indirectly interacting through software.
Error messages and failed proof attempts are valuable in that they tell
me, "Novice, we wizards want to teach you something. It is enough that
we have told you that you are wrong."
But when I don't get an error message and my proofs succeed, and I'm
being logically clumsy, the software alone can't teach me a better way.
It appears that use of datatype_new to define hereditarily finite sets
is not something that is easily hidden.
I actually only defined 'hD` because I figure if wizards are talking
about hereditarily finite sets, then it's something I'm supposed to care
about.
The hS ends up being one of 4 variations of sets I'm trying to work on
that are variations of ZFC sets. I have two more powerful versions that
hopefully will pan out. For a year and a half, I've worked on an axiom
based set that gives me things I can be used with little or no modification.
The appearance of datatype_new has turned me into a closet
constructivist, where I use THE and SOME only to hypocritically
rebel against the constructivists, but never use if THE and SOME
will prevent me from producing what could otherwise be used for computation.
On August 8, 2013, I was getting some foggy ideas on how I thought I
needed to recursively define a certain object using nested sets. On that
day, there came the list email "Re: [isabelle] nested datatypes" [1],
which told of the a new datatype package coming down the pipe, and I saw
that I merely needed to wait for that, because traditional ZFC sets are
like the Hotel California, you can check elements in, but it's a hell in
there, because it's hard to check them out. At least, that's my impression.
A large part of the value of Nitpick and Sledgehammer is the help they
give me in prototyping. In one day, Nitpick showed me I needed to
abandon two different definitions I was trying to implement. Then, after
coming up with a partially good definition, Nitpick and Sledgehammer
helped me get enough other definitions going, and theorems proved, to
know I was on the right track.
I could start hitting these four variations hard, but I have a bad
co-dependent relation with Sledgehammer. It's a high when it gives me an
easy proof, but when it doesn't immediately provide a proof, I have to
get manipulative. I don't care that I'm being manipulative. I only care
that it takes too much time, and that I don't have a bigger toolbox to
be able to optimize the metis proofs it gives me.
So, I have to take a huge, time-consuming tangent on logic.
I am a prophet who makes easy, fail-safe prophecies. In the game of
logic, Isabelle will be a huge gamer-changer with the masses, and
datatype_new will be a big game-changer in the game of Isabelle/HOL.
Regards,
GB
[1]
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-August/msg00017.html
Last updated: Apr 25 2024 at 12:23 UTC