# [isabelle] 5 proofs of concept satisfied and awesomeness revisited

Hi,

`I don't like making this mailing list my personal playground, and after
``this email, I'll make a belated New Year's resolution to make a
``concerted effort to use this list for what it's best used for, showing
``experts a piece a code with a problem, which the experts are good at
``analyzing fast and can reply to fast.
`

`If I had a blog, which I do, I could turn this email into a preliminary
``product review for Isabelle, which I won't at this time. If there's any
``value in this, it could be that a potential user out there has some of
``the same questions I had.
`

`You can also consider me an early representative of the new wave of
``users who will come here and either complain about the product and
``disrespect the product, because they don't know what they're looking at,
``or tell you how awesome it is, because they've figured out what they're
``looking at.
`

`[I interrupt this email for an important message. I don't know if I
``would have been excited enough to write this email if I wouldn't have
``gotten a structured proof out of sledgehammer on my first try. My
``current run of sledgehammer failed on the structured proof. I'll try to
``set the timeout longer. However, I did get a couple of lines that say
``something like "Found proof (284 ms)", but I don't know which ATP proved
``it. Anyway, I got a screenshot of the first results. Getting any proof
``could be considered exciting, but the structured proof gives more visual
``excitement.]
`

`Not trying anymore to make this into a polished review, I throw out some
``ideas.
`

`I dropped Isabelle for about 6 months, up until about May 2012, but in a
``period of about 4 to 5 months, I satisfied at least 5 "proof of concept"
``questions I had, where there was and always will be the ongoing question
``of how powerful Isabelle's logic engine is.
`

`(1) Can proofs in Isabelle be made to look and flow like traditional
``mathematical proofs?
`

`I answered that fairly quickly after working through
``http://dream.inf.ed.ac.uk/projects/isabelle/Isabelle_Primer.pdf. Many
``people don't take the time and make the choices to make their proofs
``look great, but formatting a document to look good takes time.
`
(2) Can I become an advanced user of Isabelle with minimal help?

`It took me a while to get confidence about that, because I knew I would
``have a need to understand some of the distribution source, and the style
``of proofs in the distribution source is all over the place; the theories
``have been, after all, produced over many years. After reading Makarius's
``twenty ways to prove (A /\ B) --> (B /\ A) in his PhD thesis, along with
``all the documentation that I've collected, I got the confidence that I'm
``not going to hit a brick learning wall I can't get over.
`
(3) Can the syntax of Isabelle be made to look very, very mathematical?

`I already knew about the available math symbols, and the structured
``proofs, which was part of the initial attraction. I showed in a recent
``email that Isar identifiers can be made to look mathematical. Let no man
``or woman say that single, subscripted Latin, Greek, mathcal, or mathfrak
``alphabet characters do not meet the requirements of looking mathematical.
`

`For those who don't know, an Isar identifier can use 0-9, ', and _,
``though it can't start with those characters. In addition, it can use
``a-z, A-Z, \<a> - \<z>, \<A> - \<Z>, \<aa> - \<zz>, \<AA> - \<ZZ> (but
``not II and RR) , and the lower and upper case Greek alphabet, such as
``\<alpha>. You can use \<^isub> and \<^isup> followed by the
``aforementioned characters anywhere you want, and as many times as you
``want. That's some major naming options, compared to most programming
``languages.
`
(4) Can I get axiomatic ZF sets in HOL?

`This whole thing of axiomatic sets in Isabelle is a big subject. I make
``sure here that I don't go off telling you all my thoughts and opinions
``on this subject. I only say that there are many practical reasons why I
``choose Isabelle/HOL over Isabelle/ZF, and I have a sufficient interest
``in sets to want to try my hand at reinventing the wheel.
`

`Also, what has evolved is my understanding of the concept of
``meta-languages and object languages. I leave it at that. Sort of. I'll
``actually be working through Jech and Hrbacek's "Introduction to Set
``Theory, 3rd", which is one of the standard texts on axiomatic sets. My
``intent is to try to imitate their development of sets. Got to have goals
``in life, even if the goals don't always work out.
`

`(5) Does Isabelle allow me to choose between proving a proof step
``automatically and explicitly specifying how to prove the step?
`

`Yes. For this, I'm already starting to forget that this was a "big
``question issue". I assure you, if Isabelle only had the ability to
``provide "mysterious proof results" by auto, I wouldn't be trying to
``learn it. On the other hand, if I knew I was never ever going to have
``the option to not prove every little detail, then I would be buckling
``down for some major brainwave pain in the future.
`
A TALE TO TELL

`The above questions were some of my questions. It's not that they've set
``things in stone, but up to this point, the answers to my big questions
``have been positive.
`

`Last year, I started looking at HOL.thy very early in the game to try
``and figure out if "I can learn this". From November to May, I did
``nothing and was simply waiting on the next release. Recently, when I got
``to "type_synonym" on page 12, the light bulb came on for a way to try
``and set up sets. I put down a little bit of code just to try my hand at
``using some of the keywords.
`

`I layed down some type commands, a few axioms, defined the first theorem
``to be proved (that the empty set is unique), and tried my hand at using
``"apply(auto)", which requires, of course, knowing how to type on the
``keyboard.
`

`It was a no go, which was okay because I wasn't trying to be in "serious
``prover mode". A few days passed, and it occurred to me, "How about that
``axiom of extension, bro? Defining set equality would be a good thing,
``don't you think?"
`

`So I put in the axiom of extension and tried auto again. No go. But,
``hey, doing the easy stuff can count for a lot, because last year I put
``quite a bit of effort into looking at sledgehammer's options. The idea
``is, if sledgehammer gives you the option to try something, then make it
``try it. It turns out that I end up using fairly simple options for
``sledgehammer.
`

`Last year, I had viper installed, but I only have the default setup now,
``so I give it these options:
`

`sledgehammer_params [provers = "e cvc3 spass z3 z3_tptp metis",
``verbose=true, isar_proof=true]
`

`What you should know is that with Isabelle2011-1, sledgehammer running
``under Cygwin was useless. It wouldn't ever come back, or it would
``timeout. I knew sledgehammer worked because I tried it out under Linux.
`

`I tried sledgehammer, not expecting any results. I got results. In
``particular, the structured proof stood out because it's not a one-line
``statement telling you, "Found proof".
`

`Having a healthy amount of paranoia, and preferring to think like a
``lawyer, I wouldn't consider an auto proof meaningful without trying to
``figure out any details it gives me, checking my code setup, and, in
``general, trying to decide whether I gave sledgehammer meaningful
``information.
`

`However, I took out the axiom of extension, and sledgehammer found no
``solution. I put it back in, and sledghammer finds a solution.
``Conclusive? No. But not bad news either. The easy part is done, I
``assume. Using the axiom of separation and the power set? I don't know
``about that. Oh yea, and replacing the auto proof with a non-auto proof.
`

`Okay. I completed this to partly get this type of thing out of my
``system. I could have waited months, or a year, and said, "Hey, this
``Jech's set theory thing worked out." It may not work out. It's no big
``deal if it doesn't, since there would probably be a good reason why it
``didn't work out.
`

`It's also to say, "Hey, I like that magic". And to say, "Dude, how do
``you do that? But please, don't even try to tell me."
`

`Two screen shots are attached. One shows the structured proof that it
``found that it doesn't find anymore. I assume it's because CPU resources
``got sucked up by Windows for something else. I'll try setting the
``options later.
`
Regards,
GB

**Attachment:
**`120712_structured_proof_found.png`

*Description:* PNG image

**Attachment:
**`120712_axiom_setup.png`

*Description:* PNG image

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