# 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
``in mathematics.
`

`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
``sciencey".
`
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
``Isabelle/HOL.
`

`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
``arithmetic:
`

`1) Fundamentals of Digital Logic with Verilog Design, 3rd, by Brown &
``Vranesic
`
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
Regards,
GB

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