Re: [isabelle] primrec_new error: extra vars on RHS, option return type works




[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








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.