Re: [isabelle] The theory Option
On 14-10-08 14:45, Gottfried Barrow wrote:
If I knew anything much more about HOL numbers than that the successor
of 0 is 1, I would define a new type, real_minus_zero, using typedef
of course, and then I would define division so that the denominator of
division is of type real_minus_zero...
An excellent opportunity to reply to myself, since what I have to say is
to no one in particular.
I guess division of real numbers is completely tied into type classes,
so things aren't so simple as I said.
But it's actually a sign of great progress when people can do a lot of
talking about what they don't understand, yet be doing legitimate work
For example, how is it possible, with "only" a foundation of college
algebra and trig, that many students, with absolutely no previous
exposure to calculus, can blow through so much material in 3 to 4 months
of the first course of the "mother of all foundational math sequence of
courses" (calculus, vector calculus, and differential equations)?
The reason is one single word, "textbooks". Even novices work through
proofs using the delta-epsilon definition of a limit, which was
formalized as recently as about 1820 by Weierstrass.
So how does Isabelle/HOL measure up when it comes to my ability to do
math in Isabelle/HOL? It doesn't. I can't do any of combinatorics,
number theory, or real analysis in Isabelle/HOL. I could do the abstract
part of abstract algebra, but nothing involving concrete mathematics.
The problem is not that I don't know enough. The problem is that I need
to know too much. My lack of knowledge is no obstacle to my being able
to work in math in a traditional manner. I actually understand way more
math that I'm able to use in Isbelle/HOL.
The problem? Concrete numbers. Arithmetic. That's the problem. That's
the road block.
We have this situation. Isabelle/HOL formalizes mathematics up to
complex numbers, which is its standard entry point. Even more, HOL
formalizes the standard number systems, N, Z, Q, R, and C, in a classic
way, therefore making it "very mathematical", as opposed to "computer
You might think that makes me happy. It made me happy, past tense.
Continuing with "the situation", I can't use the number systems for
arithmetic because I don't know the details, and because I don't know
the details, I don't even know that the classic formalizations are
actually sufficient for concrete arithmetic, so that I don't eventually
hit a brick wall, which is an ever present risk when trying to use
Now, I go back to that single word, "textbooks". The mechanics of how to
use Isabelle/HOL, as a software product, is documented fairly well, but
the mathematics that makes up the foundation of Isabelle/HOL, it's not
documented at all. A person might take exception to my generalizations,
but they're close enough for me.
Isabelle/HOL is a logic of its own, and it's used to lay a type-theory
foundation of mathematics up to complex numbers. I ask, "After more than
20 years of development of mathematics in HOL, how many textbooks are
there that explain the basic mathematics that's developed in HOL?" The
answer is zero.
It's not like I'm picky. I'm flexible. Combinatorics, number theory,
abstract algebra, or real analysis, I could go with any of those. I just
need to work through some math, as it's developed and proved in HOL,
where there's some heavy use of numbers, and I need to do it in a
methodical manner, as in "textbook manner".
I say I have a need. I don't actually have a need at all. If I had a
need, I'd be in big trouble, because computer scientists who develop
mathematics in HOL, those computer scientists don't write textbooks
about HOL-based mathematics. What they do is develop libraries, and I
think I understand why, because to teach what you know is to spend time
not advancing where you want to go. Just because I understand doesn't
mean I let myself be happy.
It's best to see that someone has published explanations of the details
of where I think I want to go. With HOL, it's not enough that someone
would tell me, "It's all there. The formalization of N, Z, Q, R, and C
in Isabelle/HOL, or in src/HOL, or the AFP, that gives you the
foundation of what you need."
That's not enough. I shouldn't trust someone that much.
The consequence is that I have to start at the bottom, and slowly work
my way up, even though the number systems are already there.
Okay, given that fact, my first choice is to build on what others have
done, so where do I find documented guidance, commonly called
"textbooks", to teach me the details of number systems? (These details,
I wouldn't have to know if I was content working in traditional math, or
if textbooks existed to start me out at a high level of math in HOL,
such as real analysis.)
I don't find the details from computer scientists who have developed
mathematics in Isabelle/HOL, because rather than writing textbooks about
the details they've implemented, they forge ahead, for their own
pleasure and enjoyment, which, I grudgingly admit, has undoubtedly
resulted in better automation tools, which do their own form of teaching.
The details come from electrical engineers, and computer scientists who
do research in computer arithmetic, and who also have taken the time to
write textbooks. I've done the hard work of tracking these down. It
wasn't obvious that these are where the details would come from, and it
could be I won't use any of them to do the required work, just to do
1) Fundamentals of Digital Logic with Verilog Design, 3rd, by Brown &
2) Computer Arithmetic and Verilog HDL Fundamentals, by Cavanagh
3) Arithmetic and Logic in Computer Systems, by Lu
4) Modern Computer Algebra, 3rd, by Gathen & Gerhard
This archive was generated by a fusion of
Pipermail (Mailman edition) and