*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] What are the atomic terms in Isabelle/HOL?*From*: gottfried.barrow at gmx.com*Date*: Mon, 04 Jun 2012 08:17:35 -0500*In-reply-to*: <4FCC4AF9.1060304@in.tum.de>*References*: <4FCC2AE7.5020405@gmx.com> <4FCC4AF9.1060304@in.tum.de>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

Tobias, Thanks. I'm trying to get the vocabulary down.

2A1 Definition (Types): An infinite sequence of type-variables is assumed to be given, distinct from term-variables. Types are... (i) each type-variable is a type (called an atom)

Definition 10.1 (Simple types): Assume we have a finite or infinite sequence of symbols called atomic types; then... (a) every atomic type is a type;

Thanks, GB On 6/4/2012 12:43 AM, Tobias Nipkow wrote:

> to Isabelle, not a definition. Just like most textbooks on functional > programming it does not start out with the lambda-calculus on page 1. > > To answer the question in your title: variables and constants. > > Tobias > > Am 04/06/2012 05:26, schrieb gottfried.barrow at gmx.com: >> I'm looking at this sentence in prog-prove.pdf, page 3: >> >> Terms are formed as in functional programming by applying >> functions to arguments. If f is a function of type >> tau1 => tau2 and t is a term of type tau1, then f t >> is a term of type tau2. >>

>> term is: >> >> Terms may also contain lambda-abstractions. >>

>>

>> can correct them if you'd like: >> >> 1) Does a term (of Isabelle/HOL) have a type? (obviously yes) >> 2) Is a term (of Isabelle/HOL) a type? (no) >> 3) Is a type (of Isabelle/HOL) a term? (no) >>

>>

>> that out. >> >> In intro.pdf (Old Introduction to Isabelle), page 1, it says: >> >> The syntax for terms is summarised below... >> t :: tau type constraint, on a term or bound variable >> %x . t abstraction >> %x1...xn . t curried abstraction, %x1...%xn . t >> t(u) application >> t(u1,...,un) curried application, t(u1) ... (un) >> >> This indicates that a lambda-abstraction can be a term. >>

>> "Chapter 5 Syntactic Operations for PP-Lambda", page 142, he says: >> >> Terms come in four syntactic classes: constants, variables, >> abstractions, and combinations (function applications). >>

>> function application. >> >> I'll ask two more questions, in case someone wants to answer them: >> >> 1) Is a term (in Isabelle/HOL) function application only? (probably not)

>> and Computation" apply to Isabelle/HOL? >>

>> need to work through for foundational material on HOL. >> >> Thanks, >> GB > >

**Follow-Ups**:**Re: [isabelle] What are the atomic terms in Isabelle/HOL?***From:*Ramana Kumar

**References**:**[isabelle] What are the atomic terms in Isabelle/HOL?***From:*gottfried . barrow

**Re: [isabelle] What are the atomic terms in Isabelle/HOL?***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] Verification of C Programs
- Next by Date: Re: [isabelle] What are the atomic terms in Isabelle/HOL?
- Previous by Thread: Re: [isabelle] What are the atomic terms in Isabelle/HOL?
- Next by Thread: Re: [isabelle] What are the atomic terms in Isabelle/HOL?
- Cl-isabelle-users June 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