# HG changeset patch # User wenzelm # Date 1157729585 -7200 # Node ID 48fea5e99505e97959f073a2cf0a7b18e8528aa1 # Parent c9bfc874488cee46afe59b2087ebb448706885bc tuned; diff -r c9bfc874488c -r 48fea5e99505 doc-src/IsarImplementation/Thy/document/logic.tex --- a/doc-src/IsarImplementation/Thy/document/logic.tex Fri Sep 08 13:33:11 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/document/logic.tex Fri Sep 08 17:33:05 2006 +0200 @@ -26,7 +26,7 @@ \begin{isamarkuptext}% The logical foundations of Isabelle/Isar are that of the Pure logic, which has been introduced as a natural-deduction framework in - \cite{paulson700}. This is essentially the same logic as ``\isa{{\isasymlambda}HOL}'' in the more abstract framework of Pure Type Systems (PTS) + \cite{paulson700}. This is essentially the same logic as ``\isa{{\isasymlambda}HOL}'' in the more abstract setting of Pure Type Systems (PTS) \cite{Barendregt-Geuvers:2001}, although there are some key differences in the specific treatment of simple types in Isabelle/Pure. @@ -69,23 +69,24 @@ elements wrt.\ the sort order. \medskip A \emph{fixed type variable} is a pair of a basic name - (starting with \isa{{\isacharprime}} character) and a sort constraint. For + (starting with a \isa{{\isacharprime}} character) and a sort constraint. For example, \isa{{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ s{\isacharparenright}} which is usually printed as \isa{{\isasymalpha}\isactrlisub s}. A \emph{schematic type variable} is a pair of an indexname and a sort constraint. For example, \isa{{\isacharparenleft}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}{\isacharcomma}\ s{\isacharparenright}} which is usually printed as \isa{{\isacharquery}{\isasymalpha}\isactrlisub s}. Note that \emph{all} syntactic components contribute to the identity - of type variables, including the literal sort constraint. The core - logic handles type variables with the same name but different sorts - as different, although some outer layers of the system make it hard - to produce anything like this. + of type variables, including the sort constraint. The core logic + handles type variables with the same name but different sorts as + different, although some outer layers of the system make it hard to + produce anything like this. - A \emph{type constructor} is a \isa{k}-ary operator on types - declared in the theory. Type constructor application is usually - written postfix. For \isa{k\ {\isacharequal}\ {\isadigit{0}}} the argument tuple is omitted, - e.g.\ \isa{prop} instead of \isa{{\isacharparenleft}{\isacharparenright}prop}. For \isa{k\ {\isacharequal}\ {\isadigit{1}}} the parentheses are omitted, e.g.\ \isa{{\isasymalpha}\ list} instead of - \isa{{\isacharparenleft}{\isasymalpha}{\isacharparenright}list}. Further notation is provided for specific - constructors, notably right-associative infix \isa{{\isasymalpha}\ {\isasymRightarrow}\ {\isasymbeta}} - instead of \isa{{\isacharparenleft}{\isasymalpha}{\isacharcomma}\ {\isasymbeta}{\isacharparenright}fun} constructor. + A \emph{type constructor} \isa{{\isasymkappa}} is a \isa{k}-ary operator + on types declared in the theory. Type constructor application is + usually written postfix as \isa{{\isacharparenleft}FIXME{\isacharparenright}{\isasymkappa}}. For \isa{k\ {\isacharequal}\ {\isadigit{0}}} + the argument tuple is omitted, e.g.\ \isa{prop} instead of + \isa{{\isacharparenleft}{\isacharparenright}prop}. For \isa{k\ {\isacharequal}\ {\isadigit{1}}} the parentheses are omitted, + e.g.\ \isa{{\isasymalpha}\ list} instead of \isa{{\isacharparenleft}{\isasymalpha}{\isacharparenright}list}. Further + notation is provided for specific constructors, notably + right-associative infix \isa{{\isasymalpha}\ {\isasymRightarrow}\ {\isasymbeta}} instead of \isa{{\isacharparenleft}{\isasymalpha}{\isacharcomma}\ {\isasymbeta}{\isacharparenright}fun} constructor. A \emph{type} is defined inductively over type variables and type constructors as follows: \isa{{\isasymtau}\ {\isacharequal}\ {\isasymalpha}\isactrlisub s\ {\isacharbar}\ {\isacharquery}{\isasymalpha}\isactrlisub s\ {\isacharbar}\ {\isacharparenleft}{\isasymtau}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlsub k{\isacharparenright}c}. diff -r c9bfc874488c -r 48fea5e99505 doc-src/IsarImplementation/Thy/logic.thy --- a/doc-src/IsarImplementation/Thy/logic.thy Fri Sep 08 13:33:11 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/logic.thy Fri Sep 08 17:33:05 2006 +0200 @@ -9,7 +9,7 @@ The logical foundations of Isabelle/Isar are that of the Pure logic, which has been introduced as a natural-deduction framework in \cite{paulson700}. This is essentially the same logic as ``@{text - "\HOL"}'' in the more abstract framework of Pure Type Systems (PTS) + "\HOL"}'' in the more abstract setting of Pure Type Systems (PTS) \cite{Barendregt-Geuvers:2001}, although there are some key differences in the specific treatment of simple types in Isabelle/Pure. @@ -56,26 +56,27 @@ elements wrt.\ the sort order. \medskip A \emph{fixed type variable} is a pair of a basic name - (starting with @{text "'"} character) and a sort constraint. For + (starting with a @{text "'"} character) and a sort constraint. For example, @{text "('a, s)"} which is usually printed as @{text "\\<^isub>s"}. A \emph{schematic type variable} is a pair of an indexname and a sort constraint. For example, @{text "(('a, 0), s)"} which is usually printed as @{text "?\\<^isub>s"}. Note that \emph{all} syntactic components contribute to the identity - of type variables, including the literal sort constraint. The core - logic handles type variables with the same name but different sorts - as different, although some outer layers of the system make it hard - to produce anything like this. + of type variables, including the sort constraint. The core logic + handles type variables with the same name but different sorts as + different, although some outer layers of the system make it hard to + produce anything like this. - A \emph{type constructor} is a @{text "k"}-ary operator on types - declared in the theory. Type constructor application is usually - written postfix. For @{text "k = 0"} the argument tuple is omitted, - e.g.\ @{text "prop"} instead of @{text "()prop"}. For @{text "k = - 1"} the parentheses are omitted, e.g.\ @{text "\ list"} instead of - @{text "(\)list"}. Further notation is provided for specific - constructors, notably right-associative infix @{text "\ \ \"} - instead of @{text "(\, \)fun"} constructor. + A \emph{type constructor} @{text "\"} is a @{text "k"}-ary operator + on types declared in the theory. Type constructor application is + usually written postfix as @{text "(FIXME)\"}. For @{text "k = 0"} + the argument tuple is omitted, e.g.\ @{text "prop"} instead of + @{text "()prop"}. For @{text "k = 1"} the parentheses are omitted, + e.g.\ @{text "\ list"} instead of @{text "(\)list"}. Further + notation is provided for specific constructors, notably + right-associative infix @{text "\ \ \"} instead of @{text "(\, + \)fun"} constructor. A \emph{type} is defined inductively over type variables and type constructors as follows: @{text "\ = \\<^isub>s | ?\\<^isub>s |