*To*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Where to learn about HOL vs FOL?*From*: IG BI <igbi at gmx.com>*Date*: Mon, 06 Jan 2014 00:30:58 -0600*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

* /Date/: Wed, 01 Jan 2014 20:28:11 +0100 ------------------------------------------------------------------------Le Fri, 01 Feb 2013 15:22:53 +0100, Gottfried Barrow <gottfried.barrowat gmx.com> a écrit:...but it's not, it's the perfect place tolearn about HOL4's formal logic:http://hol.sourceforge.net/documentation.html [...]The one titled "Logic" (file name "kananaskis-8-logic.pdf") still saysin the preface:...Because this logic is shared with other theorem-proving systems (HOL Light, ProofPower), and is similar to that implemented in Isabelle, where it is called Isabelle/HOL, it is now presented in its own manual.

*COMPLEX TYPED TERMS, NO MOTIVE TO SORT THROUGH A SIMILAR GRAMMAR*

*SOME ISABELLE SOURCE BEFORE SOME ORIGINAL SOURCES*

Consider the following: term "x::(('a::{type,equal,ord}) list)"

*SOME ORIGINAL SOURCES*

*1987: LOGIC AND COMPUTATION, INTERACTIVE PROOF WITH CAMBRIDGE LCF* By L. C. Paulson Published by Cambridge Tracts in hardcopy form.

*1994: ISABELLE, A GENERIC THEOREM PROVER* by Lawrence Paulson, with Contributions by Tobias Nipkow Published by Springer-Verlag in hardcopy form.

http://isabelle.in.tum.de/website-Isabelle2013-2/dist/Isabelle2013-2/doc/intro.pdf

term "a::int"

*1995: TYPE RECONSTRUCTION FOR TYPE CLASSES* by Tobias Nipkow and Christian Prehofer http://www21.in.tum.de/~nipkow/pubs/jfp95.html There's a grammar for a Mini-Haskell on page 3.

*1997: TYPE CLASSES AND OVERLOADING IN HIGHER-ORDER LOGIC* by Makarius Wenzel http://www4.in.tum.de/~wenzelm/papers/axclass-TPHOLs97.pdf

As a quite harmless simplification, HOL can be identified directly with Isbelle/Pure.

In section 3.1 HOL Syntax, he quickly describes the HOL types and terms. *OUTRO*

Regards, GB (******************************************************************************) theory i140105a imports Complex_Main begin declare[[show_sorts=true]] declare[[show_brackets=true]]

type (the type variable type class), and type constructor. Does the type constructor 'list' also have a type? *) term "x::(('a::{type,equal,ord}) list)" (*OJB_EXP_2: Do type variable constants such as 'int' have a type? Type

type constants have a type, such as "nat:Set": http://www.labri.fr/perso/casteran/CoqArt/Tsinghua/C5.pdf

same. Do 0-ary type constructors have a type? *) term "x::int" (*Displayed: "(x::int)"::int.*) (*EXP_3: Inferred: x::('a::{}) *) term "x" term "x::('a::{})" (*META_EXP_4: Inferred: x::('a::{}). *) term "x == x" theorem "x == x" by(simp) theorem "x == (x::('a::{}))" by(simp) (*OBJ_EXP_5: Type: x::('a::ab_semigroup_add). *) theorem "(x::('a::{type, plus, semigroup_add, ab_semigroup_add})) = x" by(simp) (*OBJ_EXP_6: Type: x::('a::{plus,equal}). *) theorem "(x::('a::{plus,equal})) = x" by(simp) (*META_EXP_7: Inferred: x::prop. There is no type variable. *) term "PROP x" theorem "PROP x == PROP x" by(simp) (*OBJ_EXP_8: Inferred: x::('a::type). *) term "x = x" theorem "x = x" by(simp) theorem "x = (x::('a::type))" by(simp) (*OBJ_EXP_9: Trying to make 'a to be type {} gives an error. *) (* theorem "x = (x::('a::{}))" (*ERROR: Type unification failed: Variable 'a::{} not of sort type.*) *) (*META_EXP_10: defining 'a to have type "type". *) theorem "x == (x::('a::type))" by(simp) (******************************************************************************) end

- Previous by Date: [isabelle] Easy And Language Integrated Use
- Next by Date: Re: [isabelle] Instantiating type classes
- Previous by Thread: Re: [isabelle] Where to learn about HOL vs FOL?
- Next by Thread: [isabelle] Prooving the existence of a splitting field
- Cl-isabelle-users January 2014 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