*To*: Ken Kubota <mail at kenkubota.de>*Subject*: Re: [isabelle] Literature on the type system of Isabelle/HOL; text by Mike Gordon*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Tue, 9 Aug 2016 11:17:20 +0100*Cc*: hol-info at lists.sourceforge.net, Corey Richardson <corey at octayn.net>, cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <25BFF9C0-748B-49E0-9C6F-3E799076E217@kenkubota.de>*References*: <2D14D352-3D4D-4FDE-ABA4-0168BF6E04F3@kenkubota.de> <5F22105EAD3CAD4689EC4570AA1802B0BF0197C539@WGFP-EXMAV1.uni.mdx.ac.uk> <A6A56921-0B58-4CF4-9786-DBF6E77F286C@kenkubota.de> <1468731439.2162406.668416497.16BBD60D@webmail.messagingengine.com> <25BFF9C0-748B-49E0-9C6F-3E799076E217@kenkubota.de>

It can be downloaded from here: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.27.6103 Larry Paulson > On 8 Aug 2016, at 12:13, Ken Kubota <mail at kenkubota.de> wrote: > > Dear Members of the Research Community, > > As part of my efforts to try to understand the type system of Isabelle/HOL, I > have gathered the references from the mails written by Corey Richardson and > Michael Norrish and from The Isabelle/Isar Reference Manual, especially from > a) Chapter 10: Higher-Order Logic (pp. 236 f.) > b) Â 11.7 Semantic subtype definitions (pp. 260-263) > c) Â 11.8 Functorial structure of types (pp. 263 f.). > > In all cases, with one exception, I was able to obtain either the link to the > online version or the ISBN number. > > > The exception is Mike Gordon's text "HOL: A machine oriented formulation of > higher order logic" (Technical Report 68, University of Cambridge Computer > Laboratory), registered at > http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-68.html > > As Isabelle is provided by the University of Cambridge Computer Laboratory, > among others, would it be possible for the Isabelle developers to make this > technical report available online as a PDF file? This was done for the first > five reports listed at > http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-table.html > > According to the references supplied with the traditional (Mike Gordon's) HOL > variant, a revised version exists: "Technical Report No.\ 68 (revised > version)", quoted from > https://github.com/HOL-Theorem-Prover/HOL/blob/master/Manual/Description/references.tex > Either both versions or the revised version should be made available. > > > I would like to take this opportunity to thank Michael Norrish for his advice. > The LOGIC part of HOL4 system's documentation at > http://sourceforge.net/projects/hol/files/hol/kananaskis-10/kananaskis-10-logic.pdf > is the kind of short and precise formulation of the logical core I recently > proposed for Isabelle/HOL, too: > https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-July/msg00105.html > > In this HOL4 document, it is stated: "From a logical point of view it would be > better to have a simpler substitution primitive, such as 'Rule R' of Andrews' > logic Q0, and then to derive more complex rules from it." (p. 27) > This is exactly the same idea that I presented recently: "The main criterion is > expressiveness [cf. Andrews, 2002, p. 205], or, vice versa, the reducibility of > mathematics to a minimal set of primitive rules and symbols. [...] For the > philosopher it is not proof automation but expressiveness that is the main > criterion, such that the method with the least amount of rules of inferences, > i.e., a Hilbert-style system, is preferred, and all other rules become derived > rules." > https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-July/msg00028.html > > Similarly, the HOL4 document argues in favor of definitions instead of > introducing new axioms: "The advantages of postulation over definition have > been likened by Bertrand Russell to the advantages of theft over honest toil. > As it is all too easy to introduce inconsistent axiomatizations, users of the > HOL system are strongly advised to resist the temptation to add axioms, but to > toil through definitional theories honestly." [p. 33] > In the same manner, I wrote: "One consequence [...] is to avoid the use of > non-logical axioms. [...] The appropriate way to deal with objects of certain > properties is to create a set of objects with these properties." [Kubota, 2015, > p. 29] > For this reason, in the R0 implementation, the group axioms are expressed not > as axioms, but as properties in the definition of "Grp" (wff 266): > http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf (p. 359) > > > Kind regards, > > Ken Kubota > > > > Sources > > [S1] The Isabelle/Isar Reference Manual (February 17, 2016) > http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2016/doc/isar-ref.pdf > > [S2] Reference in the e-mail written by Corey Richardson > https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-July/msg00070.html > > Dmitry Traytel / Andrei Popescu / Jasmin C. Blanchette, Foundational, > Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to > Theorem Proving > http://dx.doi.org/10.1109/LICS.2012.75 > https://www21.in.tum.de/~traytel/papers/lics12-codatatypes/codat.pdf > > [S3] Reference in the e-mail written by Michael Norrish > "The chapters from the HOL book mentioned above are available as part of the > HOL4 system's documentation at: > http://sourceforge.net/projects/hol/files/hol/kananaskis-10/kananaskis-10-logic.pdf/download > See Â2.5.4 in particular for a discussion of how the system can be extended > with new types." > > The HOL System: LOGIC (November 6, 2014) > http://sourceforge.net/projects/hol/files/hol/kananaskis-10/kananaskis-10-logic.pdf > > > Derived References (from [S1], pp. 260-263) > > [15] W. M. Farmer. The seven virtues of simple type theory. J. Applied Logic, > 6(3):267-286, 2008. > http://imps.mcmaster.ca/doc/seven-virtues.pdf > > [18] M. J. C. Gordon. HOL: A machine oriented formulation of higher order > logic. Technical Report 68, University of Cambridge Computer Laboratory, 1985. > > [50] A. Pitts. The HOL logic. In M. J. C. Gordon and T. F. Melham, editors, > Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, > pages 191-232. Cambridge University Press, 1993. > ISBN 0-521-44189-7 > > [57] M. Wenzel. Type classes and overloading in higher-order logic. In E. L. > Gunter and A. Felty, editors, Theorem Proving in Higher Order Logics: TPHOLs > '97, volume 1275 of Lecture Notes in Computer Science. Springer-Verlag, 1997. > http://www4.in.tum.de/~wenzelm/papers/axclass-TPHOLs97.pdf > > [22] F. Haftmann and M. Wenzel. Constructive type classes in Isabelle. In T. > Altenkirch and C. McBride, editors, Types for Proofs and Programs, TYPES 2006, > volume 4502 of LNCS. Springer, 2007. > http://www4.in.tum.de/~wenzelm/papers/constructive_classes.pdf > > [27] O. Kuncar and A. Popescu. A consistent foundation for Isabelle/HOL. In C. > Urban and X. Zhang, editors, Interactive Theorem Proving - 6th International > Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings, volume > 9236 of Lecture Notes in Computer Science. Springer, 2015. > http://www21.in.tum.de/~kuncar/kuncar-popescu-jar2016.pdf > http://andreipopescu.uk/pdf/ITP2015.pdf > > > Standard References > > Andrews, Peter B. (1986), An Introduction to Mathematical Logic and Type > Theory: To Truth Through Proof. Orlando: Academic Press. ISBN 0-12-058535-9 > (Hardcover). ISBN 0-12-058536-7 (Paperback). > > Andrews, Peter B. (2002), An Introduction to Mathematical Logic and Type > Theory: To Truth Through Proof. Second edition. Dordrecht / Boston / London: > Kluwer Academic Publishers. ISBN 1-4020-0763-9. DOI: 10.1007/978-94-015-9934-4. > > Andrews, Peter B. (2014), "Church's Type Theory". In: Stanford Encyclopedia of > Philosophy (Spring 2014 Edition). Ed. by Edward N. Zalta. Available online at > http://plato.stanford.edu/archives/spr2014/entries/type-theory-church/ (July 2, > 2016). > > Church, Alonzo (1940), "A Formulation of the Simple Theory of Types". In: > Journal of Symbolic Logic 5, pp. 56-68. > > > Further References > > Kubota, Ken (2015), On the Theory of Mathematical Forms (draft from May 18, > 2015). Unpublished manuscript. SHA-512: a0dfe205eb1a2cb29efaa579d68fa2e5 > 45af74d8cd6c270cf4c95ed1ba6f7944 fdcffaef2e761c8215945a9dcd535a50 > 011d8303fd59f2c8a4e6f64125867dc4. DOI: 10.4444/100.10. See: > http://dx.doi.org/10.4444/100.10 > > Kubota, Ken (2015a), Excerpt from [Kubota, 2015] (pp. 356-364, pp. 411-420, and > pp. 754-755). Available online at > http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf > (January 24, 2016). SHA-512: 67a48ee12a61583bd82c286136459c0c > 9fd77f5fd7bd820e8b6fe6384d977eda 4d92705dac5b3f97e7981d7b709fc783 > 3d1047d1831bc357eb57b263b44c885b. > > ____________________ > > Ken Kubota > doi: 10.4444/100 > http://dx.doi.org/10.4444/100 > >

**Follow-Ups**:

**References**:

- Previous by Date: Re: [isabelle] difficulties with polymorphic record extension
- Next by Date: Re: [isabelle] qed and done take long for large goal states
- Previous by Thread: [isabelle] Literature on the type system of Isabelle/HOL; text by Mike Gordon
- Next by Thread: [isabelle] Literature on the type system of Isabelle/HOL; HOL documentation; non-logical axioms vs. definitions; epsilon vs. description operator (HOL vs. Q0); Rule R of Andrews' logic Q0
- Cl-isabelle-users August 2016 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