*To*: cl-isabelle-users at lists.cam.ac.uk, hol-info at lists.sourceforge.net*Subject*: [isabelle] Literature on the type system of Isabelle/HOL; text by Mike Gordon*From*: Ken Kubota <mail at kenkubota.de>*Date*: Mon, 8 Aug 2016 13:13:55 +0200*Cc*: Michael.Norrish at data61.csiro.au, "Michael J. C. Gordon" <mjcg at cl.cam.ac.uk>, Corey Richardson <corey at octayn.net>, "Prof. Peter B. Andrews" <andrews at cmu.edu>*In-reply-to*: <1468731439.2162406.668416497.16BBD60D@webmail.messagingengine.com>*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>

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**:**Re: [isabelle] Literature on the type system of Isabelle/HOL; text by Mike Gordon***From:*Lawrence Paulson

- Previous by Date: [isabelle] New AFP Article: Ptolemy's Theorem
- Next by Date: [isabelle] New in the AFP: The Imperative Refinement Framework
- Previous by Thread: [isabelle] New AFP Article: Ptolemy's Theorem
- Next by Thread: Re: [isabelle] Literature on the type system of Isabelle/HOL; text by Mike Gordon
- 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