Isabelle Syntax

extract from isabelle- Programming

Basic Syntax
Most statements of logic (inner-syntax) should be places in speech-marks

"numberMonth n = months!(n - 1)"

Isabelle employs LATEX-like tags for unicode syntax 

• e.g.∀x.∃y.y > x  is written as per LATEX. 
• \forall x.\exists y.y > x

HOL(Higher Order Logic) is a typed logic whose type system resembles that of functional programming languages. Thus there are: 

• base types, in particular bool, the type of truth values, nat, the type of natural numbers (), and int, the type of mathematical integers ().

• type constructors, in particular list, the type of lists, and set, the type of sets. Type constructors are written postfix, e.g. nat list is the type of lists whose elements are natural numbers.

• function types, denoted by.

• type variables, denoted by 'a, 'b etc., just like in ML

• Formulae are terms of type bool. There are the basic constants True andFalse and the usual logical connectives (in decreasing order of precedence): 

Theories
Roughly speaking, a theory is a named collection of types, functions, and theorems, much like a module in a programming language. All the Isabelle text that you ever type needs to go into a theory. The general format of a
       
     theory T is
     theory T
     imports T1 : : : T n
     begin
          definitions, theorems and proofs
     end

where T1 : : : T n are the names of existing theories that T is based on. The Ti are the direct parent theories of T. Everything defined in the parent theories (and their parents, recursively) is automatically visible. Each theory T must reside in a theory file named T:thy.