doc-src/IsarImplementation/Thy/logic.thy
changeset 20493 48fea5e99505
parent 20491 98ba42f19995
child 20494 99ad217b6974
     1.1 --- a/doc-src/IsarImplementation/Thy/logic.thy	Fri Sep 08 13:33:11 2006 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy	Fri Sep 08 17:33:05 2006 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4    The logical foundations of Isabelle/Isar are that of the Pure logic,
     1.5    which has been introduced as a natural-deduction framework in
     1.6    \cite{paulson700}.  This is essentially the same logic as ``@{text
     1.7 -  "\<lambda>HOL"}'' in the more abstract framework of Pure Type Systems (PTS)
     1.8 +  "\<lambda>HOL"}'' in the more abstract setting of Pure Type Systems (PTS)
     1.9    \cite{Barendregt-Geuvers:2001}, although there are some key
    1.10    differences in the specific treatment of simple types in
    1.11    Isabelle/Pure.
    1.12 @@ -56,26 +56,27 @@
    1.13    elements wrt.\ the sort order.
    1.14  
    1.15    \medskip A \emph{fixed type variable} is a pair of a basic name
    1.16 -  (starting with @{text "'"} character) and a sort constraint.  For
    1.17 +  (starting with a @{text "'"} character) and a sort constraint.  For
    1.18    example, @{text "('a, s)"} which is usually printed as @{text
    1.19    "\<alpha>\<^isub>s"}.  A \emph{schematic type variable} is a pair of an
    1.20    indexname and a sort constraint.  For example, @{text "(('a, 0),
    1.21    s)"} which is usually printed as @{text "?\<alpha>\<^isub>s"}.
    1.22  
    1.23    Note that \emph{all} syntactic components contribute to the identity
    1.24 -  of type variables, including the literal sort constraint.  The core
    1.25 -  logic handles type variables with the same name but different sorts
    1.26 -  as different, although some outer layers of the system make it hard
    1.27 -  to produce anything like this.
    1.28 +  of type variables, including the sort constraint.  The core logic
    1.29 +  handles type variables with the same name but different sorts as
    1.30 +  different, although some outer layers of the system make it hard to
    1.31 +  produce anything like this.
    1.32  
    1.33 -  A \emph{type constructor} is a @{text "k"}-ary operator on types
    1.34 -  declared in the theory.  Type constructor application is usually
    1.35 -  written postfix.  For @{text "k = 0"} the argument tuple is omitted,
    1.36 -  e.g.\ @{text "prop"} instead of @{text "()prop"}.  For @{text "k =
    1.37 -  1"} the parentheses are omitted, e.g.\ @{text "\<alpha> list"} instead of
    1.38 -  @{text "(\<alpha>)list"}.  Further notation is provided for specific
    1.39 -  constructors, notably right-associative infix @{text "\<alpha> \<Rightarrow> \<beta>"}
    1.40 -  instead of @{text "(\<alpha>, \<beta>)fun"} constructor.
    1.41 +  A \emph{type constructor} @{text "\<kappa>"} is a @{text "k"}-ary operator
    1.42 +  on types declared in the theory.  Type constructor application is
    1.43 +  usually written postfix as @{text "(FIXME)\<kappa>"}.  For @{text "k = 0"}
    1.44 +  the argument tuple is omitted, e.g.\ @{text "prop"} instead of
    1.45 +  @{text "()prop"}.  For @{text "k = 1"} the parentheses are omitted,
    1.46 +  e.g.\ @{text "\<alpha> list"} instead of @{text "(\<alpha>)list"}.  Further
    1.47 +  notation is provided for specific constructors, notably
    1.48 +  right-associative infix @{text "\<alpha> \<Rightarrow> \<beta>"} instead of @{text "(\<alpha>,
    1.49 +  \<beta>)fun"} constructor.
    1.50    
    1.51    A \emph{type} is defined inductively over type variables and type
    1.52    constructors as follows: @{text "\<tau> = \<alpha>\<^isub>s | ?\<alpha>\<^isub>s |