*To*: Bill Richter <richter at math.northwestern.edu>, cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle*From*: Makarius <makarius at sketis.net>*Date*: Thu, 31 May 2012 23:34:17 +0200 (CEST)*In-reply-to*: <201205310412.q4V4CCrj014777@poisson.math.northwestern.edu>*References*: <201204282058.q3SKw9NF008441@poisson.math.northwestern.edu> <CAFP4q14YwNi6RksUOkGNGWYYzkNi3ca92FH4kYW19kJeOBcT2Q@mail.gmail.com> <alpine.LNX.2.00.1204301125350.6594@macbroy21.informatik.tu-muenchen.de> <201205020207.q4227VoC013147@poisson.math.northwestern.edu> <4FA0A63C.7030904@jaist.ac.jp> <201205020409.q42497Ou014411@poisson.math.northwestern.edu> <4FA0BBE7.4060302@jaist.ac.jp> <201205030338.q433ciL9026861@poisson.math.northwestern.edu> <201205250512.q4P5Cgns004328@poisson.math.northwestern.edu> <alpine.LNX.2.00.1205251146380.8953@macbroy22.informatik.tu-muenchen.de> <201205270818.q4R8IUWm022240@poisson.math.northwestern.edu> <alpine.LNX.2.00.1205292251410.19391@macbroy22.informatik.tu-muenchen.de> <201205310412.q4V4CCrj014777@poisson.math.northwestern.edu>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Wed, 30 May 2012, Bill Richter wrote:

I'd be happy for you to post there about miz3 ocaml dirty code cacheissues.

The Isabelle/Pure framework is centered around higher-order natural deduction, and Isabelle/Isar as a proof language continues these ideas. To understand these things properly, you should first blot out "FOL", then get used to Pure + Isar, then add HOL as object-logic, and then rediscover what predicate logic (including FOL) will do for you here via some add-on tools. I'm not opposed to learning Pure + Isar, but it would be a whole lot easier for me to learn if I knew in advance how it related to FOL, which as a mathematician I have a rudimentary (but not practical) understanding of.

Let me make a rudimentary FOL point: I think writing down strict axiomatic FOL proofs would really be tedious because e.g. you have manually substitute variables every time you want to use an axiom. I don't have a full list of the tedium strict FOL can cause. But I'm only willing to write up FOL-type proofs if the proof assistant will automate that tedium. Do similar issues arise with Pure + Isar?

Also, as you may have observed on hol info, I know next to nothing about HOL. Basically I understand the 20 pages of set theory John explains in his reference manual. Isn't Isabelle HOL much the same as HOL as in HOL Light HOL? Where is a good place to learn about HOL?

In principle any of the HOL systems could provide their own locale mechanism, or something similar. It is not possible to "just" do it, though. Isabelle has required 10+ years to get this all done right. It is also a matter of culture. John Harrison would certainly not add such complexity to his system. You have to use Isabelle or Coq for such sophisticated module concepts, or maybe Mizar. Sure, but I really dislike the Mizar type system, and I want to lightly typed sets to avoid any hard typing.

> But instead we could look at all models of Tarski's axioms, a > model being some sets and functions with some properties. Can > you do this in Isabelle too? If this means you want to study the meta-theory of Tarski axioms, then any of the HOL systems -- Isabelle/HOL included -- can do this for you, if you define the syntax and inference system more concretely (via datatypes and inductive relations). Great, but I don't know what meta-theory means. A model of Tarski's geometry axioms is be a set S (of points), a 3-ary relation Between on S and a 4-ary relation Equiv on S satisfying Tarski's axioms (so far I only use his first 7 axioms, and you coded them up in Isabelle). So there might be a predicate TarskiModel(S, Between, Equiv), and theorems in a Tarski model would begin

term "tarski_first7" The system will check that and print the most general type for it:

assume TarskiModel(S, Between, Equiv)...

I don't understand HOL well enough to actually pull this off, but John explained how to get started. My point is that I don't think any typing is involved here, beyond maybe something rudimentary like new_type("point",0);; new_type_abbrev("TarskiPlane",`:point->bool`);;

axiomatization

Cong3 ("_ _ _ ≐≐ _ _ _" [1000, 1000, 1000, 1000, 1000, 1000] 50) and Bet :: "point ⇒ point ⇒ point ⇒ bool" where Cong3_def: "a b c ≐≐ x y z ≡ a b ≐ x y ∧ a c ≐ x z ∧ b c ≐ y z" and A1: "a b ≐ b a" and A2: "a b ≐ p q ⟹ a b ≐ r s ⟹ p q ≐ r s" and A3: "a b ≐ c c ⟹ a = b" and A4: "∃x. Bet q a x ∧ a x ≐ b c" and A5: "a ≠ b ⟹ Bet a b d ⟹ Bet a' b' d' ⟹ a b c ≐≐ a' b' c' ⟹ b d ≐ b' d' ⟹ c d ≐ c' d'" and A6: "Bet a b a ⟹ a = b" and A7: "Bet a p c ⟹ Bet b q c ⟹ ∃x. Bet p x b ∧ Bet q x a"

Makarius

**References**:**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Bill Richter

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Christian Sternagel

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Bill Richter

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Christian Sternagel

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Bill Richter

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Bill Richter

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Makarius

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Bill Richter

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Makarius

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Bill Richter

- Previous by Date: Re: [isabelle] Automation is awesome; one bibliography leads to another
- Previous by Thread: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Next by Thread: [isabelle] locales, including documentation & possible programming bugs
- Cl-isabelle-users May 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list