18537

1 
%


2 
\begin{isabellebody}%


3 
\def\isabellecontext{logic}%


4 
%


5 
\isadelimtheory


6 
\isanewline


7 
\isanewline


8 
\isanewline


9 
%


10 
\endisadelimtheory


11 
%


12 
\isatagtheory


13 
\isacommand{theory}\isamarkupfalse%


14 
\ logic\ \isakeyword{imports}\ base\ \isakeyword{begin}%


15 
\endisatagtheory


16 
{\isafoldtheory}%


17 
%


18 
\isadelimtheory


19 
%


20 
\endisadelimtheory


21 
%

20471

22 
\isamarkupchapter{Primitive logic \label{ch:logic}%

18537

23 
}


24 
\isamarkuptrue%


25 
%

20481

26 
\begin{isamarkuptext}%


27 
The logical foundations of Isabelle/Isar are that of the Pure logic,


28 
which has been introduced as a naturaldeduction framework in

20493

29 
\cite{paulson700}. This is essentially the same logic as ``\isa{{\isasymlambda}HOL}'' in the more abstract setting of Pure Type Systems (PTS)

20481

30 
\cite{BarendregtGeuvers:2001}, although there are some key

20491

31 
differences in the specific treatment of simple types in


32 
Isabelle/Pure.

20481

33 


34 
Following typetheoretic parlance, the Pure logic consists of three

20543

35 
levels of \isa{{\isasymlambda}}calculus with corresponding arrows, \isa{{\isasymRightarrow}} for syntactic function space (terms depending on terms), \isa{{\isasymAnd}} for universal quantification (proofs depending on terms), and

20481

36 
\isa{{\isasymLongrightarrow}} for implication (proofs depending on proofs).


37 

20537

38 
Derivations are relative to a logical theory, which declares type


39 
constructors, constants, and axioms. Theory declarations support


40 
schematic polymorphism, which is strictly speaking outside the


41 
logic.\footnote{This is the deeper logical reason, why the theory


42 
context \isa{{\isasymTheta}} is separate from the proof context \isa{{\isasymGamma}}


43 
of the core calculus.}%

20481

44 
\end{isamarkuptext}%


45 
\isamarkuptrue%


46 
%

20451

47 
\isamarkupsection{Types \label{sec:types}%

18537

48 
}


49 
\isamarkuptrue%


50 
%


51 
\begin{isamarkuptext}%

20481

52 
The language of types is an uninterpreted ordersorted firstorder


53 
algebra; types are qualified by ordered type classes.

20451

54 

20481

55 
\medskip A \emph{type class} is an abstract syntactic entity


56 
declared in the theory context. The \emph{subclass relation} \isa{c\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlisub {\isadigit{2}}} is specified by stating an acyclic

20491

57 
generating relation; the transitive closure is maintained


58 
internally. The resulting relation is an ordering: reflexive,


59 
transitive, and antisymmetric.

20451

60 

20537

61 
A \emph{sort} is a list of type classes written as \isa{s\ {\isacharequal}\ {\isacharbraceleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlisub m{\isacharbraceright}}, which represents symbolic

20481

62 
intersection. Notationally, the curly braces are omitted for


63 
singleton intersections, i.e.\ any class \isa{c} may be read as


64 
a sort \isa{{\isacharbraceleft}c{\isacharbraceright}}. The ordering on type classes is extended to

20491

65 
sorts according to the meaning of intersections: \isa{{\isacharbraceleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}\ c\isactrlisub m{\isacharbraceright}\ {\isasymsubseteq}\ {\isacharbraceleft}d\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ d\isactrlisub n{\isacharbraceright}} iff


66 
\isa{{\isasymforall}j{\isachardot}\ {\isasymexists}i{\isachardot}\ c\isactrlisub i\ {\isasymsubseteq}\ d\isactrlisub j}. The empty intersection


67 
\isa{{\isacharbraceleft}{\isacharbraceright}} refers to the universal sort, which is the largest


68 
element wrt.\ the sort order. The intersections of all (finitely


69 
many) classes declared in the current theory are the minimal


70 
elements wrt.\ the sort order.

20451

71 

20491

72 
\medskip A \emph{fixed type variable} is a pair of a basic name

20537

73 
(starting with a \isa{{\isacharprime}} character) and a sort constraint, e.g.\


74 
\isa{{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ s{\isacharparenright}} which is usually printed as \isa{{\isasymalpha}\isactrlisub s}.


75 
A \emph{schematic type variable} is a pair of an indexname and a


76 
sort constraint, e.g.\ \isa{{\isacharparenleft}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}{\isacharcomma}\ s{\isacharparenright}} which is usually


77 
printed as \isa{{\isacharquery}{\isasymalpha}\isactrlisub s}.

20481

78 


79 
Note that \emph{all} syntactic components contribute to the identity

20493

80 
of type variables, including the sort constraint. The core logic


81 
handles type variables with the same name but different sorts as


82 
different, although some outer layers of the system make it hard to


83 
produce anything like this.

18537

84 

20493

85 
A \emph{type constructor} \isa{{\isasymkappa}} is a \isa{k}ary operator


86 
on types declared in the theory. Type constructor application is

20537

87 
written postfix as \isa{{\isacharparenleft}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlisub k{\isacharparenright}{\isasymkappa}}. For


88 
\isa{k\ {\isacharequal}\ {\isadigit{0}}} the argument tuple is omitted, e.g.\ \isa{prop}


89 
instead of \isa{{\isacharparenleft}{\isacharparenright}prop}. For \isa{k\ {\isacharequal}\ {\isadigit{1}}} the parentheses


90 
are omitted, e.g.\ \isa{{\isasymalpha}\ list} instead of \isa{{\isacharparenleft}{\isasymalpha}{\isacharparenright}list}.


91 
Further notation is provided for specific constructors, notably the


92 
rightassociative infix \isa{{\isasymalpha}\ {\isasymRightarrow}\ {\isasymbeta}} instead of \isa{{\isacharparenleft}{\isasymalpha}{\isacharcomma}\ {\isasymbeta}{\isacharparenright}fun}.

20481

93 

20537

94 
A \emph{type} is defined inductively over type variables and type

20543

95 
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}{\isasymkappa}}.

20451

96 

20514

97 
A \emph{type abbreviation} is a syntactic definition \isa{{\isacharparenleft}\isactrlvec {\isasymalpha}{\isacharparenright}{\isasymkappa}\ {\isacharequal}\ {\isasymtau}} of an arbitrary type expression \isa{{\isasymtau}} over

20537

98 
variables \isa{\isactrlvec {\isasymalpha}}. Type abbreviations appear as type


99 
constructors in the syntax, but are expanded before entering the


100 
logical core.

20451

101 

20481

102 
A \emph{type arity} declares the image behavior of a type

20494

103 
constructor wrt.\ the algebra of sorts: \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlisub k{\isacharparenright}s} means that \isa{{\isacharparenleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub k{\isacharparenright}{\isasymkappa}} is


104 
of sort \isa{s} if every argument type \isa{{\isasymtau}\isactrlisub i} is


105 
of sort \isa{s\isactrlisub i}. Arity declarations are implicitly


106 
completed, i.e.\ \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c} entails \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isacharprime}} for any \isa{c{\isacharprime}\ {\isasymsupseteq}\ c}.

20451

107 

20491

108 
\medskip The sort algebra is always maintained as \emph{coregular},


109 
which means that type arities are consistent with the subclass

20537

110 
relation: for any type constructor \isa{{\isasymkappa}}, and classes \isa{c\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlisub {\isadigit{2}}}, and arities \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlisub {\isadigit{1}}{\isacharparenright}c\isactrlisub {\isadigit{1}}} and \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlisub {\isadigit{2}}{\isacharparenright}c\isactrlisub {\isadigit{2}}} holds \isa{\isactrlvec s\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ \isactrlvec s\isactrlisub {\isadigit{2}}} componentwise.

20491

111 


112 
The key property of a coregular ordersorted algebra is that sort

20537

113 
constraints can be solved in a most general fashion: for each type


114 
constructor \isa{{\isasymkappa}} and sort \isa{s} there is a most general


115 
vector of argument sorts \isa{{\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlisub k{\isacharparenright}} such


116 
that a type scheme \isa{{\isacharparenleft}{\isasymalpha}\isactrlbsub s\isactrlisub {\isadigit{1}}\isactrlesub {\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlbsub s\isactrlisub k\isactrlesub {\isacharparenright}{\isasymkappa}} is of sort \isa{s}.

20543

117 
Consequently, type unification has most general solutions (modulo


118 
equivalence of sorts), so typeinference produces primary types as


119 
expected \cite{nipkowprehofer}.%

18537

120 
\end{isamarkuptext}%


121 
\isamarkuptrue%


122 
%

20481

123 
\isadelimmlref


124 
%


125 
\endisadelimmlref


126 
%


127 
\isatagmlref


128 
%


129 
\begin{isamarkuptext}%


130 
\begin{mldecls}


131 
\indexmltype{class}\verbtype class \\


132 
\indexmltype{sort}\verbtype sort \\

20494

133 
\indexmltype{arity}\verbtype arity \\

20481

134 
\indexmltype{typ}\verbtype typ \\

20519

135 
\indexml{mapatyps}\verbmap_atyps: (typ > typ) > typ > typ \\

20494

136 
\indexml{foldatyps}\verbfold_atyps: (typ > 'a > 'a) > typ > 'a > 'a \\

20547

137 
\end{mldecls}


138 
\begin{mldecls}

20481

139 
\indexml{Sign.subsort}\verbSign.subsort: theory > sort * sort > bool \\


140 
\indexml{Sign.ofsort}\verbSign.of_sort: theory > typ * sort > bool \\

20520

141 
\indexml{Sign.addtypes}\verbSign.add_types: (string * int * mixfix) list > theory > theory \\

20481

142 
\indexml{Sign.addtyabbrsi}\verbSign.add_tyabbrs_i: \isasep\isanewline%

20520

143 
\verb (string * string list * typ * mixfix) list > theory > theory \\

20481

144 
\indexml{Sign.primitiveclass}\verbSign.primitive_class: string * class list > theory > theory \\


145 
\indexml{Sign.primitiveclassrel}\verbSign.primitive_classrel: class * class > theory > theory \\


146 
\indexml{Sign.primitivearity}\verbSign.primitive_arity: arity > theory > theory \\


147 
\end{mldecls}


148 


149 
\begin{description}


150 


151 
\item \verbclass represents type classes; this is an alias for


152 
\verbstring.


153 


154 
\item \verbsort represents sorts; this is an alias for


155 
\verbclass list.


156 


157 
\item \verbarity represents type arities; this is an alias for

20494

158 
triples of the form \isa{{\isacharparenleft}{\isasymkappa}{\isacharcomma}\ \isactrlvec s{\isacharcomma}\ s{\isacharparenright}} for \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}s} described above.

20481

159 


160 
\item \verbtyp represents types; this is a datatype with


161 
constructors \verbTFree, \verbTVar, \verbType.


162 

20537

163 
\item \verbmap_atyps~\isa{f\ {\isasymtau}} applies the mapping \isa{f}


164 
to all atomic types (\verbTFree, \verbTVar) occurring in \isa{{\isasymtau}}.

20519

165 

20537

166 
\item \verbfold_atyps~\isa{f\ {\isasymtau}} iterates the operation \isa{f} over all occurrences of atomic types (\verbTFree, \verbTVar)


167 
in \isa{{\isasymtau}}; the type structure is traversed from left to right.

20494

168 

20481

169 
\item \verbSign.subsort~\isa{thy\ {\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ s\isactrlisub {\isadigit{2}}{\isacharparenright}}


170 
tests the subsort relation \isa{s\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ s\isactrlisub {\isadigit{2}}}.


171 

20537

172 
\item \verbSign.of_sort~\isa{thy\ {\isacharparenleft}{\isasymtau}{\isacharcomma}\ s{\isacharparenright}} tests whether type


173 
\isa{{\isasymtau}} is of sort \isa{s}.

20481

174 

20537

175 
\item \verbSign.add_types~\isa{{\isacharbrackleft}{\isacharparenleft}{\isasymkappa}{\isacharcomma}\ k{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} declares a new

20494

176 
type constructors \isa{{\isasymkappa}} with \isa{k} arguments and

20481

177 
optional mixfix syntax.


178 

20494

179 
\item \verbSign.add_tyabbrs_i~\isa{{\isacharbrackleft}{\isacharparenleft}{\isasymkappa}{\isacharcomma}\ \isactrlvec {\isasymalpha}{\isacharcomma}\ {\isasymtau}{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}}


180 
defines a new type abbreviation \isa{{\isacharparenleft}\isactrlvec {\isasymalpha}{\isacharparenright}{\isasymkappa}\ {\isacharequal}\ {\isasymtau}} with

20491

181 
optional mixfix syntax.

20481

182 

20537

183 
\item \verbSign.primitive_class~\isa{{\isacharparenleft}c{\isacharcomma}\ {\isacharbrackleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlisub n{\isacharbrackright}{\isacharparenright}} declares a new class \isa{c}, together with class

20494

184 
relations \isa{c\ {\isasymsubseteq}\ c\isactrlisub i}, for \isa{i\ {\isacharequal}\ {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ n}.

20481

185 

20543

186 
\item \verbSign.primitive_classrel~\isa{{\isacharparenleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ c\isactrlisub {\isadigit{2}}{\isacharparenright}} declares the class relation \isa{c\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlisub {\isadigit{2}}}.

20481

187 

20494

188 
\item \verbSign.primitive_arity~\isa{{\isacharparenleft}{\isasymkappa}{\isacharcomma}\ \isactrlvec s{\isacharcomma}\ s{\isacharparenright}} declares

20537

189 
the arity \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}s}.

20481

190 


191 
\end{description}%


192 
\end{isamarkuptext}%


193 
\isamarkuptrue%


194 
%


195 
\endisatagmlref


196 
{\isafoldmlref}%


197 
%


198 
\isadelimmlref


199 
%


200 
\endisadelimmlref


201 
%

20451

202 
\isamarkupsection{Terms \label{sec:terms}%

18537

203 
}


204 
\isamarkuptrue%


205 
%


206 
\begin{isamarkuptext}%

20451

207 
\glossary{Term}{FIXME}

18537

208 

20491

209 
The language of terms is that of simplytyped \isa{{\isasymlambda}}calculus

20520

210 
with deBruijn indices for bound variables (cf.\ \cite{debruijn72}

20537

211 
or \cite{paulsonml2}), with the types being determined determined


212 
by the corresponding binders. In contrast, free variables and


213 
constants are have an explicit name and type in each occurrence.

20514

214 


215 
\medskip A \emph{bound variable} is a natural number \isa{b},

20537

216 
which accounts for the number of intermediate binders between the


217 
variable occurrence in the body and its binding position. For

20543

218 
example, the deBruijn term \isa{{\isasymlambda}\isactrlbsub nat\isactrlesub {\isachardot}\ {\isasymlambda}\isactrlbsub nat\isactrlesub {\isachardot}\ {\isadigit{1}}\ {\isacharplus}\ {\isadigit{0}}} would


219 
correspond to \isa{{\isasymlambda}x\isactrlbsub nat\isactrlesub {\isachardot}\ {\isasymlambda}y\isactrlbsub nat\isactrlesub {\isachardot}\ x\ {\isacharplus}\ y} in a named


220 
representation. Note that a bound variable may be represented by


221 
different deBruijn indices at different occurrences, depending on


222 
the nesting of abstractions.

20537

223 

20543

224 
A \emph{loose variable} is a bound variable that is outside the

20537

225 
scope of local binders. The types (and names) for loose variables

20543

226 
can be managed as a separate context, that is maintained as a stack


227 
of hypothetical binders. The core logic operates on closed terms,


228 
without any loose variables.

20514

229 

20537

230 
A \emph{fixed variable} is a pair of a basic name and a type, e.g.\


231 
\isa{{\isacharparenleft}x{\isacharcomma}\ {\isasymtau}{\isacharparenright}} which is usually printed \isa{x\isactrlisub {\isasymtau}}. A


232 
\emph{schematic variable} is a pair of an indexname and a type,


233 
e.g.\ \isa{{\isacharparenleft}{\isacharparenleft}x{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}{\isacharcomma}\ {\isasymtau}{\isacharparenright}} which is usually printed as \isa{{\isacharquery}x\isactrlisub {\isasymtau}}.

20491

234 

20537

235 
\medskip A \emph{constant} is a pair of a basic name and a type,


236 
e.g.\ \isa{{\isacharparenleft}c{\isacharcomma}\ {\isasymtau}{\isacharparenright}} which is usually printed as \isa{c\isactrlisub {\isasymtau}}. Constants are declared in the context as polymorphic

20543

237 
families \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}}, meaning that all substitution instances


238 
\isa{c\isactrlisub {\isasymtau}} for \isa{{\isasymtau}\ {\isacharequal}\ {\isasymsigma}{\isasymvartheta}} are valid.

20514

239 

20537

240 
The vector of \emph{type arguments} of constant \isa{c\isactrlisub {\isasymtau}}


241 
wrt.\ the declaration \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} is defined as the codomain of


242 
the matcher \isa{{\isasymvartheta}\ {\isacharequal}\ {\isacharbraceleft}{\isacharquery}{\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isasymmapsto}\ {\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isacharquery}{\isasymalpha}\isactrlisub n\ {\isasymmapsto}\ {\isasymtau}\isactrlisub n{\isacharbraceright}} presented in canonical order \isa{{\isacharparenleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub n{\isacharparenright}}. Within a given theory context,


243 
there is a onetoone correspondence between any constant \isa{c\isactrlisub {\isasymtau}} and the application \isa{c{\isacharparenleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub n{\isacharparenright}} of its type arguments. For example, with \isa{plus\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}}, the instance \isa{plus\isactrlbsub nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat\isactrlesub } corresponds to \isa{plus{\isacharparenleft}nat{\isacharparenright}}.

20481

244 

20514

245 
Constant declarations \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} may contain sort constraints


246 
for type variables in \isa{{\isasymsigma}}. These are observed by


247 
typeinference as expected, but \emph{ignored} by the core logic.


248 
This means the primitive logic is able to reason with instances of

20537

249 
polymorphic constants that the userlevel typechecker would reject


250 
due to violation of type class restrictions.

20481

251 

20543

252 
\medskip An \emph{atomic} term is either a variable or constant. A


253 
\emph{term} is defined inductively over atomic terms, with


254 
abstraction and application as follows: \isa{t\ {\isacharequal}\ b\ {\isacharbar}\ x\isactrlisub {\isasymtau}\ {\isacharbar}\ {\isacharquery}x\isactrlisub {\isasymtau}\ {\isacharbar}\ c\isactrlisub {\isasymtau}\ {\isacharbar}\ {\isasymlambda}\isactrlisub {\isasymtau}{\isachardot}\ t\ {\isacharbar}\ t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}}.


255 
Parsing and printing takes care of converting between an external


256 
representation with named bound variables. Subsequently, we shall


257 
use the latter notation instead of internal deBruijn


258 
representation.

20499

259 

20537

260 
The inductive relation \isa{t\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}} assigns a (unique) type to a


261 
term according to the structure of atomic terms, abstractions, and


262 
applicatins:

20499

263 
\[

20502

264 
\infer{\isa{a\isactrlisub {\isasymtau}\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}}}{}

20499

265 
\qquad

20502

266 
\infer{\isa{{\isacharparenleft}{\isasymlambda}x\isactrlsub {\isasymtau}{\isachardot}\ t{\isacharparenright}\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymsigma}}}{\isa{t\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}}}


267 
\qquad


268 
\infer{\isa{t\ u\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}}}{\isa{t\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymsigma}} & \isa{u\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}}}

20514

269 
\]


270 
A \emph{welltyped term} is a term that can be typed according to these rules.


271 


272 
Typing information can be omitted: typeinference is able to


273 
reconstruct the most general type of a raw term, while assigning


274 
most general types to all of its variables and constants.


275 
Typeinference depends on a context of type constraints for fixed


276 
variables, and declarations for polymorphic constants.


277 

20537

278 
The identity of atomic terms consists both of the name and the type


279 
component. This means that different variables \isa{x\isactrlbsub {\isasymtau}\isactrlisub {\isadigit{1}}\isactrlesub } and \isa{x\isactrlbsub {\isasymtau}\isactrlisub {\isadigit{2}}\isactrlesub } may become the same after type


280 
instantiation. Some outer layers of the system make it hard to


281 
produce variables of the same name, but different types. In

20543

282 
contrast, mixed instances of polymorphic constants occur frequently.

20514

283 


284 
\medskip The \emph{hidden polymorphism} of a term \isa{t\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}}


285 
is the set of type variables occurring in \isa{t}, but not in

20537

286 
\isa{{\isasymsigma}}. This means that the term implicitly depends on type

20543

287 
arguments that are not accounted in the result type, i.e.\ there are

20537

288 
different type instances \isa{t{\isasymvartheta}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} and \isa{t{\isasymvartheta}{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} with the same type. This slightly

20543

289 
pathological situation notoriously demands additional care.

20514

290 

20537

291 
\medskip A \emph{term abbreviation} is a syntactic definition \isa{c\isactrlisub {\isasymsigma}\ {\isasymequiv}\ t} of a closed term \isa{t} of type \isa{{\isasymsigma}},


292 
without any hidden polymorphism. A term abbreviation looks like a

20543

293 
constant in the syntax, but is expanded before entering the logical


294 
core. Abbreviations are usually reverted when printing terms, using


295 
\isa{t\ {\isasymrightarrow}\ c\isactrlisub {\isasymsigma}} as rules for higherorder rewriting.

20519

296 

20537

297 
\medskip Canonical operations on \isa{{\isasymlambda}}terms include \isa{{\isasymalpha}{\isasymbeta}{\isasymeta}}conversion: \isa{{\isasymalpha}}conversion refers to capturefree

20519

298 
renaming of bound variables; \isa{{\isasymbeta}}conversion contracts an

20537

299 
abstraction applied to an argument term, substituting the argument

20519

300 
in the body: \isa{{\isacharparenleft}{\isasymlambda}x{\isachardot}\ b{\isacharparenright}a} becomes \isa{b{\isacharbrackleft}a{\isacharslash}x{\isacharbrackright}}; \isa{{\isasymeta}}conversion contracts vacuous applicationabstraction: \isa{{\isasymlambda}x{\isachardot}\ f\ x} becomes \isa{f}, provided that the bound variable

20537

301 
does not occur in \isa{f}.

20519

302 

20537

303 
Terms are normally treated modulo \isa{{\isasymalpha}}conversion, which is


304 
implicit in the deBruijn representation. Names for bound variables


305 
in abstractions are maintained separately as (meaningless) comments,


306 
mostly for parsing and printing. Full \isa{{\isasymalpha}{\isasymbeta}{\isasymeta}}conversion is

20543

307 
commonplace in various standard operations (\secref{sec:rules}) that

20537

308 
are based on higherorder unification and matching.%

18537

309 
\end{isamarkuptext}%


310 
\isamarkuptrue%


311 
%

20514

312 
\isadelimmlref


313 
%


314 
\endisadelimmlref


315 
%


316 
\isatagmlref


317 
%

18537

318 
\begin{isamarkuptext}%

20514

319 
\begin{mldecls}


320 
\indexmltype{term}\verbtype term \\

20519

321 
\indexml{op aconv}\verbop aconv: term * term > bool \\

20547

322 
\indexml{maptypes}\verbmap_types: (typ > typ) > term > term \\

20519

323 
\indexml{foldtypes}\verbfold_types: (typ > 'a > 'a) > term > 'a > 'a \\

20514

324 
\indexml{mapaterms}\verbmap_aterms: (term > term) > term > term \\


325 
\indexml{foldaterms}\verbfold_aterms: (term > 'a > 'a) > term > 'a > 'a \\

20547

326 
\end{mldecls}


327 
\begin{mldecls}

20514

328 
\indexml{fastypeof}\verbfastype_of: term > typ \\

20519

329 
\indexml{lambda}\verblambda: term > term > term \\


330 
\indexml{betapply}\verbbetapply: term * term > term \\

20520

331 
\indexml{Sign.addconstsi}\verbSign.add_consts_i: (string * typ * mixfix) list > theory > theory \\

20519

332 
\indexml{Sign.addabbrevs}\verbSign.add_abbrevs: string * bool >\isasep\isanewline%

20520

333 
\verb ((string * mixfix) * term) list > theory > theory \\

20519

334 
\indexml{Sign.consttypargs}\verbSign.const_typargs: theory > string * typ > typ list \\


335 
\indexml{Sign.constinstance}\verbSign.const_instance: theory > string * typ list > typ \\

20514

336 
\end{mldecls}

18537

337 

20514

338 
\begin{description}

18537

339 

20537

340 
\item \verbterm represents deBruijn terms, with comments in


341 
abstractions, and explicitly named free variables and constants;


342 
this is a datatype with constructors \verbBound, \verbFree, \verbVar, \verbConst, \verbAbs, \verbop $.

20519

343 


344 
\item \isa{t}~\verbaconv~\isa{u} checks \isa{{\isasymalpha}}equivalence of two terms. This is the basic equality relation


345 
on type \verbterm; raw datatype equality should only be used


346 
for operations related to parsing or printing!


347 

20547

348 
\item \verbmap_types~\isa{f\ t} applies the mapping \isa{f} to all types occurring in \isa{t}.

20537

349 


350 
\item \verbfold_types~\isa{f\ t} iterates the operation \isa{f} over all occurrences of types in \isa{t}; the term


351 
structure is traversed from left to right.

20519

352 

20537

353 
\item \verbmap_aterms~\isa{f\ t} applies the mapping \isa{f}


354 
to all atomic terms (\verbBound, \verbFree, \verbVar, \verbConst) occurring in \isa{t}.


355 


356 
\item \verbfold_aterms~\isa{f\ t} iterates the operation \isa{f} over all occurrences of atomic terms (\verbBound, \verbFree,


357 
\verbVar, \verbConst) in \isa{t}; the term structure is

20519

358 
traversed from left to right.


359 

20537

360 
\item \verbfastype_of~\isa{t} determines the type of a


361 
welltyped term. This operation is relatively slow, despite the


362 
omission of any sanity checks.

20519

363 

20537

364 
\item \verblambda~\isa{a\ b} produces an abstraction \isa{{\isasymlambda}a{\isachardot}\ b}, where occurrences of the atomic term \isa{a} in the


365 
body \isa{b} are replaced by bound variables.

20519

366 

20537

367 
\item \verbbetapply~\isa{{\isacharparenleft}t{\isacharcomma}\ u{\isacharparenright}} produces an application \isa{t\ u}, with topmost \isa{{\isasymbeta}}conversion if \isa{t} is an


368 
abstraction.

20519

369 


370 
\item \verbSign.add_consts_i~\isa{{\isacharbrackleft}{\isacharparenleft}c{\isacharcomma}\ {\isasymsigma}{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} declares a


371 
new constant \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} with optional mixfix syntax.


372 


373 
\item \verbSign.add_abbrevs~\isa{print{\isacharunderscore}mode\ {\isacharbrackleft}{\isacharparenleft}{\isacharparenleft}c{\isacharcomma}\ t{\isacharparenright}{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}}


374 
declares a new term abbreviation \isa{c\ {\isasymequiv}\ t} with optional


375 
mixfix syntax.


376 

20520

377 
\item \verbSign.const_typargs~\isa{thy\ {\isacharparenleft}c{\isacharcomma}\ {\isasymtau}{\isacharparenright}} and \verbSign.const_instance~\isa{thy\ {\isacharparenleft}c{\isacharcomma}\ {\isacharbrackleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub n{\isacharbrackright}{\isacharparenright}}

20543

378 
convert between two representations of polymorphic constants: full


379 
type instance vs.\ compact type arguments form.

20514

380 


381 
\end{description}%

18537

382 
\end{isamarkuptext}%


383 
\isamarkuptrue%


384 
%

20514

385 
\endisatagmlref


386 
{\isafoldmlref}%


387 
%


388 
\isadelimmlref


389 
%


390 
\endisadelimmlref


391 
%

20451

392 
\isamarkupsection{Theorems \label{sec:thms}%

18537

393 
}


394 
\isamarkuptrue%


395 
%


396 
\begin{isamarkuptext}%

20521

397 
\glossary{Proposition}{FIXME A \seeglossary{term} of


398 
\seeglossary{type} \isa{prop}. Internally, there is nothing


399 
special about propositions apart from their type, but the concrete


400 
syntax enforces a clear distinction. Propositions are structured


401 
via implication \isa{A\ {\isasymLongrightarrow}\ B} or universal quantification \isa{{\isasymAnd}x{\isachardot}\ B\ x}  anything else is considered atomic. The canonical


402 
form for propositions is that of a \seeglossary{Hereditary Harrop


403 
Formula}. FIXME}

20481

404 

20502

405 
\glossary{Theorem}{A proven proposition within a certain theory and


406 
proof context, formally \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}; both contexts are


407 
rarely spelled out explicitly. Theorems are usually normalized


408 
according to the \seeglossary{HHF} format. FIXME}

18537

409 

20519

410 
\glossary{Fact}{Sometimes used interchangeably for

20502

411 
\seeglossary{theorem}. Strictly speaking, a list of theorems,


412 
essentially an extralogical conjunction. Facts emerge either as


413 
local assumptions, or as results of local goal statements  both


414 
may be simultaneous, hence the list representation. FIXME}


415 


416 
\glossary{Schematic variable}{FIXME}


417 


418 
\glossary{Fixed variable}{A variable that is bound within a certain


419 
proof context; an arbitrarybutfixed entity within a portion of


420 
proof text. FIXME}

18537

421 

20502

422 
\glossary{Free variable}{Synonymous for \seeglossary{fixed


423 
variable}. FIXME}


424 


425 
\glossary{Bound variable}{FIXME}

18537

426 

20502

427 
\glossary{Variable}{See \seeglossary{schematic variable},


428 
\seeglossary{fixed variable}, \seeglossary{bound variable}, or


429 
\seeglossary{type variable}. The distinguishing feature of


430 
different variables is their binding scope. FIXME}

18537

431 

20543

432 
A \emph{proposition} is a welltyped term of type \isa{prop}, a

20521

433 
\emph{theorem} is a proven proposition (depending on a context of


434 
hypotheses and the background theory). Primitive inferences include

20537

435 
plain natural deduction rules for the primary connectives \isa{{\isasymAnd}} and \isa{{\isasymLongrightarrow}} of the framework. There is also a builtin


436 
notion of equality/equivalence \isa{{\isasymequiv}}.%

20521

437 
\end{isamarkuptext}%


438 
\isamarkuptrue%


439 
%

20537

440 
\isamarkupsubsection{Primitive connectives and rules%

20521

441 
}


442 
\isamarkuptrue%


443 
%


444 
\begin{isamarkuptext}%

20543

445 
The theory \isa{Pure} contains constant declarations for the


446 
primitive connectives \isa{{\isasymAnd}}, \isa{{\isasymLongrightarrow}}, and \isa{{\isasymequiv}} of


447 
the logical framework, see \figref{fig:pureconnectives}. The


448 
derivability judgment \isa{A\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ A\isactrlisub n\ {\isasymturnstile}\ B} is


449 
defined inductively by the primitive inferences given in


450 
\figref{fig:primrules}, with the global restriction that the


451 
hypotheses must \emph{not} contain any schematic variables. The


452 
builtin equality is conceptually axiomatized as shown in

20521

453 
\figref{fig:pureequality}, although the implementation works

20543

454 
directly with derived inferences.

18537

455 

20521

456 
\begin{figure}[htb]


457 
\begin{center}

20502

458 
\begin{tabular}{ll}


459 
\isa{all\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isasymalpha}\ {\isasymRightarrow}\ prop{\isacharparenright}\ {\isasymRightarrow}\ prop} & universal quantification (binder \isa{{\isasymAnd}}) \\


460 
\isa{{\isasymLongrightarrow}\ {\isacharcolon}{\isacharcolon}\ prop\ {\isasymRightarrow}\ prop\ {\isasymRightarrow}\ prop} & implication (right associative infix) \\

20521

461 
\isa{{\isasymequiv}\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ prop} & equality relation (infix) \\

20502

462 
\end{tabular}

20537

463 
\caption{Primitive connectives of Pure}\label{fig:pureconnectives}

20521

464 
\end{center}


465 
\end{figure}

18537

466 

20502

467 
\begin{figure}[htb]


468 
\begin{center}

20499

469 
\[


470 
\infer[\isa{{\isacharparenleft}axiom{\isacharparenright}}]{\isa{{\isasymturnstile}\ A}}{\isa{A\ {\isasymin}\ {\isasymTheta}}}


471 
\qquad


472 
\infer[\isa{{\isacharparenleft}assume{\isacharparenright}}]{\isa{A\ {\isasymturnstile}\ A}}{}


473 
\]


474 
\[

20537

475 
\infer[\isa{{\isacharparenleft}{\isasymAnd}{\isacharunderscore}intro{\isacharparenright}}]{\isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ b{\isacharbrackleft}x{\isacharbrackright}}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ b{\isacharbrackleft}x{\isacharbrackright}} & \isa{x\ {\isasymnotin}\ {\isasymGamma}}}

20499

476 
\qquad

20537

477 
\infer[\isa{{\isacharparenleft}{\isasymAnd}{\isacharunderscore}elim{\isacharparenright}}]{\isa{{\isasymGamma}\ {\isasymturnstile}\ b{\isacharbrackleft}a{\isacharbrackright}}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ b{\isacharbrackleft}x{\isacharbrackright}}}

20499

478 
\]


479 
\[


480 
\infer[\isa{{\isacharparenleft}{\isasymLongrightarrow}{\isacharunderscore}intro{\isacharparenright}}]{\isa{{\isasymGamma}\ {\isacharminus}\ A\ {\isasymturnstile}\ A\ {\isasymLongrightarrow}\ B}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B}}


481 
\qquad


482 
\infer[\isa{{\isacharparenleft}{\isasymLongrightarrow}{\isacharunderscore}elim{\isacharparenright}}]{\isa{{\isasymGamma}\isactrlsub {\isadigit{1}}\ {\isasymunion}\ {\isasymGamma}\isactrlsub {\isadigit{2}}\ {\isasymturnstile}\ B}}{\isa{{\isasymGamma}\isactrlsub {\isadigit{1}}\ {\isasymturnstile}\ A\ {\isasymLongrightarrow}\ B} & \isa{{\isasymGamma}\isactrlsub {\isadigit{2}}\ {\isasymturnstile}\ A}}


483 
\]

20521

484 
\caption{Primitive inferences of Pure}\label{fig:primrules}


485 
\end{center}


486 
\end{figure}


487 


488 
\begin{figure}[htb]


489 
\begin{center}


490 
\begin{tabular}{ll}

20537

491 
\isa{{\isasymturnstile}\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ b{\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}\ a\ {\isasymequiv}\ b{\isacharbrackleft}a{\isacharbrackright}} & \isa{{\isasymbeta}}conversion \\

20521

492 
\isa{{\isasymturnstile}\ x\ {\isasymequiv}\ x} & reflexivity \\


493 
\isa{{\isasymturnstile}\ x\ {\isasymequiv}\ y\ {\isasymLongrightarrow}\ P\ x\ {\isasymLongrightarrow}\ P\ y} & substitution \\


494 
\isa{{\isasymturnstile}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ f\ x\ {\isasymequiv}\ g\ x{\isacharparenright}\ {\isasymLongrightarrow}\ f\ {\isasymequiv}\ g} & extensionality \\

20537

495 
\isa{{\isasymturnstile}\ {\isacharparenleft}A\ {\isasymLongrightarrow}\ B{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}B\ {\isasymLongrightarrow}\ A{\isacharparenright}\ {\isasymLongrightarrow}\ A\ {\isasymequiv}\ B} & logical equivalence \\

20521

496 
\end{tabular}

20542

497 
\caption{Conceptual axiomatization of Pure equality}\label{fig:pureequality}

20502

498 
\end{center}


499 
\end{figure}

20499

500 

20537

501 
The introduction and elimination rules for \isa{{\isasymAnd}} and \isa{{\isasymLongrightarrow}} are analogous to formation of dependently typed \isa{{\isasymlambda}}terms representing the underlying proof objects. Proof terms

20543

502 
are irrelevant in the Pure logic, though; they cannot occur within


503 
propositions. The system provides a runtime option to record

20537

504 
explicit proof terms for primitive inferences. Thus all three


505 
levels of \isa{{\isasymlambda}}calculus become explicit: \isa{{\isasymRightarrow}} for


506 
terms, and \isa{{\isasymAnd}{\isacharslash}{\isasymLongrightarrow}} for proofs (cf.\


507 
\cite{BerghoferNipkow:2000:TPHOL}).

20499

508 

20537

509 
Observe that locally fixed parameters (as in \isa{{\isasymAnd}{\isacharunderscore}intro}) need


510 
not be recorded in the hypotheses, because the simple syntactic

20543

511 
types of Pure are always inhabitable. ``Assumptions'' \isa{x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}} for typemembership are only present as long as some \isa{x\isactrlisub {\isasymtau}} occurs in the statement body.\footnote{This is the key


512 
difference to ``\isa{{\isasymlambda}HOL}'' in the PTS framework


513 
\cite{BarendregtGeuvers:2001}, where hypotheses \isa{x\ {\isacharcolon}\ A} are


514 
treated uniformly for propositions and types.}

20502

515 


516 
\medskip The axiomatization of a theory is implicitly closed by

20537

517 
forming all instances of type and term variables: \isa{{\isasymturnstile}\ A{\isasymvartheta}} holds for any substitution instance of an axiom

20543

518 
\isa{{\isasymturnstile}\ A}. By pushing substitutions through derivations


519 
inductively, we also get admissible \isa{generalize} and \isa{instance} rules as shown in \figref{fig:substrules}.

20502

520 


521 
\begin{figure}[htb]


522 
\begin{center}

20499

523 
\[

20502

524 
\infer{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}{\isacharquery}{\isasymalpha}{\isacharbrackright}}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}} & \isa{{\isasymalpha}\ {\isasymnotin}\ {\isasymGamma}}}


525 
\quad


526 
\infer[\quad\isa{{\isacharparenleft}generalize{\isacharparenright}}]{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}x{\isacharbrackright}} & \isa{x\ {\isasymnotin}\ {\isasymGamma}}}

20499

527 
\]


528 
\[

20502

529 
\infer{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}{\isasymtau}{\isacharbrackright}}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}{\isacharquery}{\isasymalpha}{\isacharbrackright}}}


530 
\quad


531 
\infer[\quad\isa{{\isacharparenleft}instantiate{\isacharparenright}}]{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}t{\isacharbrackright}}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}}}

20499

532 
\]

20502

533 
\caption{Admissible substitution rules}\label{fig:substrules}


534 
\end{center}


535 
\end{figure}

20499

536 

20537

537 
Note that \isa{instantiate} does not require an explicit


538 
sidecondition, because \isa{{\isasymGamma}} may never contain schematic


539 
variables.


540 


541 
In principle, variables could be substituted in hypotheses as well,

20543

542 
but this would disrupt the monotonicity of reasoning: deriving


543 
\isa{{\isasymGamma}{\isasymvartheta}\ {\isasymturnstile}\ B{\isasymvartheta}} from \isa{{\isasymGamma}\ {\isasymturnstile}\ B} is


544 
correct, but \isa{{\isasymGamma}{\isasymvartheta}\ {\isasymsupseteq}\ {\isasymGamma}} does not necessarily hold:


545 
the result belongs to a different proof context.

20542

546 

20543

547 
\medskip An \emph{oracle} is a function that produces axioms on the


548 
fly. Logically, this is an instance of the \isa{axiom} rule


549 
(\figref{fig:primrules}), but there is an operational difference.


550 
The system always records oracle invocations within derivations of


551 
theorems. Tracing plain axioms (and named theorems) is optional.

20542

552 


553 
Axiomatizations should be limited to the bare minimum, typically as


554 
part of the initial logical basis of an objectlogic formalization.

20543

555 
Later on, theories are usually developed in a strictly definitional


556 
fashion, by stating only certain equalities over new constants.

20542

557 

20543

558 
A \emph{simple definition} consists of a constant declaration \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} together with an axiom \isa{{\isasymturnstile}\ c\ {\isasymequiv}\ t}, where \isa{t\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} is a closed term without any hidden polymorphism. The RHS


559 
may depend on further defined constants, but not \isa{c} itself.


560 
Definitions of functions may be presented as \isa{c\ \isactrlvec x\ {\isasymequiv}\ t} instead of the puristic \isa{c\ {\isasymequiv}\ {\isasymlambda}\isactrlvec x{\isachardot}\ t}.

20542

561 

20543

562 
An \emph{overloaded definition} consists of a collection of axioms


563 
for the same constant, with zero or one equations \isa{c{\isacharparenleft}{\isacharparenleft}\isactrlvec {\isasymalpha}{\isacharparenright}{\isasymkappa}{\isacharparenright}\ {\isasymequiv}\ t} for each type constructor \isa{{\isasymkappa}} (for


564 
distinct variables \isa{\isactrlvec {\isasymalpha}}). The RHS may mention


565 
previously defined constants as above, or arbitrary constants \isa{d{\isacharparenleft}{\isasymalpha}\isactrlisub i{\isacharparenright}} for some \isa{{\isasymalpha}\isactrlisub i} projected from \isa{\isactrlvec {\isasymalpha}}. Thus overloaded definitions essentially work by


566 
primitive recursion over the syntactic structure of a single type


567 
argument.%

20521

568 
\end{isamarkuptext}%


569 
\isamarkuptrue%


570 
%


571 
\isadelimmlref


572 
%


573 
\endisadelimmlref


574 
%


575 
\isatagmlref


576 
%


577 
\begin{isamarkuptext}%


578 
\begin{mldecls}


579 
\indexmltype{ctyp}\verbtype ctyp \\


580 
\indexmltype{cterm}\verbtype cterm \\

20547

581 
\indexml{Thm.ctypof}\verbThm.ctyp_of: theory > typ > ctyp \\


582 
\indexml{Thm.ctermof}\verbThm.cterm_of: theory > term > cterm \\


583 
\end{mldecls}


584 
\begin{mldecls}

20521

585 
\indexmltype{thm}\verbtype thm \\

20542

586 
\indexml{proofs}\verbproofs: int ref \\


587 
\indexml{Thm.assume}\verbThm.assume: cterm > thm \\


588 
\indexml{Thm.forallintr}\verbThm.forall_intr: cterm > thm > thm \\


589 
\indexml{Thm.forallelim}\verbThm.forall_elim: cterm > thm > thm \\


590 
\indexml{Thm.impliesintr}\verbThm.implies_intr: cterm > thm > thm \\


591 
\indexml{Thm.implieselim}\verbThm.implies_elim: thm > thm > thm \\


592 
\indexml{Thm.generalize}\verbThm.generalize: string list * string list > int > thm > thm \\


593 
\indexml{Thm.instantiate}\verbThm.instantiate: (ctyp * ctyp) list * (cterm * cterm) list > thm > thm \\


594 
\indexml{Thm.getaxiomi}\verbThm.get_axiom_i: theory > string > thm \\


595 
\indexml{Thm.invokeoraclei}\verbThm.invoke_oracle_i: theory > string > theory * Object.T > thm \\

20547

596 
\end{mldecls}


597 
\begin{mldecls}

20542

598 
\indexml{Theory.addaxiomsi}\verbTheory.add_axioms_i: (string * term) list > theory > theory \\


599 
\indexml{Theory.adddeps}\verbTheory.add_deps: string > string * typ > (string * typ) list > theory > theory \\


600 
\indexml{Theory.addoracle}\verbTheory.add_oracle: string * (theory * Object.T > term) > theory > theory \\


601 
\indexml{Theory.adddefsi}\verbTheory.add_defs_i: bool > bool > (bstring * term) list > theory > theory \\

20521

602 
\end{mldecls}


603 


604 
\begin{description}


605 

20542

606 
\item \verbctyp and \verbcterm represent certified types


607 
and terms, respectively. These are abstract datatypes that


608 
guarantee that its values have passed the full wellformedness (and


609 
welltypedness) checks, relative to the declarations of type


610 
constructors, constants etc. in the theory.


611 

20547

612 
\item \verbctyp_of~\isa{thy\ {\isasymtau}} and \verbcterm_of~\isa{thy\ t} explicitly checks types and terms, respectively. This also


613 
involves some basic normalizations, such expansion of type and term


614 
abbreviations from the theory context.


615 


616 
Recertification is relatively slow and should be avoided in tight


617 
reasoning loops. There are separate operations to decompose


618 
certified entities (including actual theorems).

20542

619 


620 
\item \verbthm represents proven propositions. This is an


621 
abstract datatype that guarantees that its values have been


622 
constructed by basic principles of the \verbThm module.

20543

623 
Every \verbthm value contains a sliding backreference to the


624 
enclosing theory, cf.\ \secref{sec:contexttheory}.

20542

625 

20543

626 
\item \verbproofs determines the detail of proof recording within


627 
\verbthm values: \verb0 records only oracles, \verb1 records


628 
oracles, axioms and named theorems, \verb2 records full proof


629 
terms.

20542

630 


631 
\item \verbThm.assume, \verbThm.forall_intr, \verbThm.forall_elim, \verbThm.implies_intr, and \verbThm.implies_elim


632 
correspond to the primitive inferences of \figref{fig:primrules}.


633 


634 
\item \verbThm.generalize~\isa{{\isacharparenleft}\isactrlvec {\isasymalpha}{\isacharcomma}\ \isactrlvec x{\isacharparenright}}


635 
corresponds to the \isa{generalize} rules of

20543

636 
\figref{fig:substrules}. Here collections of type and term


637 
variables are generalized simultaneously, specified by the given


638 
basic names.

20499

639 

20542

640 
\item \verbThm.instantiate~\isa{{\isacharparenleft}\isactrlvec {\isasymalpha}\isactrlisub s{\isacharcomma}\ \isactrlvec x\isactrlisub {\isasymtau}{\isacharparenright}} corresponds to the \isa{instantiate} rules


641 
of \figref{fig:substrules}. Type variables are substituted before


642 
term variables. Note that the types in \isa{\isactrlvec x\isactrlisub {\isasymtau}}


643 
refer to the instantiated versions.


644 


645 
\item \verbThm.get_axiom_i~\isa{thy\ name} retrieves a named


646 
axiom, cf.\ \isa{axiom} in \figref{fig:primrules}.

20521

647 

20543

648 
\item \verbThm.invoke_oracle_i~\isa{thy\ name\ arg} invokes a


649 
named oracle function, cf.\ \isa{axiom} in


650 
\figref{fig:primrules}.

20542

651 

20543

652 
\item \verbTheory.add_axioms_i~\isa{{\isacharbrackleft}{\isacharparenleft}name{\isacharcomma}\ A{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} declares


653 
arbitrary propositions as axioms.

20542

654 

20543

655 
\item \verbTheory.add_oracle~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}} declares an oracle


656 
function for generating arbitrary axioms on the fly.

20542

657 

20543

658 
\item \verbTheory.add_deps~\isa{name\ c\isactrlisub {\isasymtau}\ \isactrlvec d\isactrlisub {\isasymsigma}} declares dependencies of a named specification


659 
for constant \isa{c\isactrlisub {\isasymtau}}, relative to existing


660 
specifications for constants \isa{\isactrlvec d\isactrlisub {\isasymsigma}}.

20542

661 

20543

662 
\item \verbTheory.add_defs_i~\isa{unchecked\ overloaded\ {\isacharbrackleft}{\isacharparenleft}name{\isacharcomma}\ c\ \isactrlvec x\ {\isasymequiv}\ t{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} states a definitional axiom for an existing


663 
constant \isa{c}. Dependencies are recorded (cf.\ \verbTheory.add_deps), unless the \isa{unchecked} option is set.

20521

664 


665 
\end{description}%


666 
\end{isamarkuptext}%


667 
\isamarkuptrue%


668 
%


669 
\endisatagmlref


670 
{\isafoldmlref}%


671 
%


672 
\isadelimmlref


673 
%


674 
\endisadelimmlref


675 
%

20543

676 
\isamarkupsubsection{Auxiliary definitions%

20521

677 
}


678 
\isamarkuptrue%


679 
%


680 
\begin{isamarkuptext}%

20543

681 
Theory \isa{Pure} provides a few auxiliary definitions, see


682 
\figref{fig:pureaux}. These special constants are normally not


683 
exposed to the user, but appear in internal encodings.

20502

684 


685 
\begin{figure}[htb]


686 
\begin{center}

20499

687 
\begin{tabular}{ll}

20521

688 
\isa{conjunction\ {\isacharcolon}{\isacharcolon}\ prop\ {\isasymRightarrow}\ prop\ {\isasymRightarrow}\ prop} & (infix \isa{{\isacharampersand}}) \\


689 
\isa{{\isasymturnstile}\ A\ {\isacharampersand}\ B\ {\isasymequiv}\ {\isacharparenleft}{\isasymAnd}C{\isachardot}\ {\isacharparenleft}A\ {\isasymLongrightarrow}\ B\ {\isasymLongrightarrow}\ C{\isacharparenright}\ {\isasymLongrightarrow}\ C{\isacharparenright}} \\[1ex]

20543

690 
\isa{prop\ {\isacharcolon}{\isacharcolon}\ prop\ {\isasymRightarrow}\ prop} & (prefix \isa{{\isacharhash}}, suppressed) \\

20521

691 
\isa{{\isacharhash}A\ {\isasymequiv}\ A} \\[1ex]


692 
\isa{term\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymRightarrow}\ prop} & (prefix \isa{TERM}) \\


693 
\isa{term\ x\ {\isasymequiv}\ {\isacharparenleft}{\isasymAnd}A{\isachardot}\ A\ {\isasymLongrightarrow}\ A{\isacharparenright}} \\[1ex]


694 
\isa{TYPE\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ itself} & (prefix \isa{TYPE}) \\


695 
\isa{{\isacharparenleft}unspecified{\isacharparenright}} \\

20499

696 
\end{tabular}

20521

697 
\caption{Definitions of auxiliary connectives}\label{fig:pureaux}

20502

698 
\end{center}


699 
\end{figure}


700 

20537

701 
Derived conjunction rules include introduction \isa{A\ {\isasymLongrightarrow}\ B\ {\isasymLongrightarrow}\ A\ {\isacharampersand}\ B}, and destructions \isa{A\ {\isacharampersand}\ B\ {\isasymLongrightarrow}\ A} and \isa{A\ {\isacharampersand}\ B\ {\isasymLongrightarrow}\ B}.


702 
Conjunction allows to treat simultaneous assumptions and conclusions


703 
uniformly. For example, multiple claims are intermediately

20543

704 
represented as explicit conjunction, but this is refined into


705 
separate subgoals before the user continues the proof; the final


706 
result is projected into a list of theorems (cf.\

20537

707 
\secref{sec:tacticalgoals}).

20502

708 

20537

709 
The \isa{prop} marker (\isa{{\isacharhash}}) makes arbitrarily complex


710 
propositions appear as atomic, without changing the meaning: \isa{{\isasymGamma}\ {\isasymturnstile}\ A} and \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isacharhash}A} are interchangeable. See


711 
\secref{sec:tacticalgoals} for specific operations.

20502

712 

20543

713 
The \isa{term} marker turns any welltyped term into a derivable


714 
proposition: \isa{{\isasymturnstile}\ TERM\ t} holds unconditionally. Although


715 
this is logically vacuous, it allows to treat terms and proofs


716 
uniformly, similar to a typetheoretic framework.

20502

717 

20537

718 
The \isa{TYPE} constructor is the canonical representative of


719 
the unspecified type \isa{{\isasymalpha}\ itself}; it essentially injects the


720 
language of types into that of terms. There is specific notation


721 
\isa{TYPE{\isacharparenleft}{\isasymtau}{\isacharparenright}} for \isa{TYPE\isactrlbsub {\isasymtau}\ itself\isactrlesub }.


722 
Although being devoid of any particular meaning, the \isa{TYPE{\isacharparenleft}{\isasymtau}{\isacharparenright}} accounts for the type \isa{{\isasymtau}} within the term


723 
language. In particular, \isa{TYPE{\isacharparenleft}{\isasymalpha}{\isacharparenright}} may be used as formal


724 
argument in primitive definitions, in order to circumvent hidden


725 
polymorphism (cf.\ \secref{sec:terms}). For example, \isa{c\ TYPE{\isacharparenleft}{\isasymalpha}{\isacharparenright}\ {\isasymequiv}\ A{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}} defines \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ itself\ {\isasymRightarrow}\ prop} in terms of


726 
a proposition \isa{A} that depends on an additional type


727 
argument, which is essentially a predicate on types.%

18537

728 
\end{isamarkuptext}%


729 
\isamarkuptrue%


730 
%

20521

731 
\isadelimmlref


732 
%


733 
\endisadelimmlref


734 
%


735 
\isatagmlref


736 
%


737 
\begin{isamarkuptext}%


738 
\begin{mldecls}


739 
\indexml{Conjunction.intr}\verbConjunction.intr: thm > thm > thm \\


740 
\indexml{Conjunction.elim}\verbConjunction.elim: thm > thm * thm \\


741 
\indexml{Drule.mkterm}\verbDrule.mk_term: cterm > thm \\


742 
\indexml{Drule.destterm}\verbDrule.dest_term: thm > cterm \\


743 
\indexml{Logic.mktype}\verbLogic.mk_type: typ > term \\


744 
\indexml{Logic.desttype}\verbLogic.dest_type: term > typ \\


745 
\end{mldecls}


746 


747 
\begin{description}


748 

20542

749 
\item \verbConjunction.intr derives \isa{A\ {\isacharampersand}\ B} from \isa{A} and \isa{B}.


750 

20543

751 
\item \verbConjunction.elim derives \isa{A} and \isa{B}

20542

752 
from \isa{A\ {\isacharampersand}\ B}.


753 

20543

754 
\item \verbDrule.mk_term derives \isa{TERM\ t}.

20542

755 

20543

756 
\item \verbDrule.dest_term recovers term \isa{t} from \isa{TERM\ t}.

20542

757 


758 
\item \verbLogic.mk_type~\isa{{\isasymtau}} produces the term \isa{TYPE{\isacharparenleft}{\isasymtau}{\isacharparenright}}.


759 


760 
\item \verbLogic.dest_type~\isa{TYPE{\isacharparenleft}{\isasymtau}{\isacharparenright}} recovers the type


761 
\isa{{\isasymtau}}.

20521

762 


763 
\end{description}%


764 
\end{isamarkuptext}%


765 
\isamarkuptrue%


766 
%


767 
\endisatagmlref


768 
{\isafoldmlref}%


769 
%


770 
\isadelimmlref


771 
%


772 
\endisadelimmlref


773 
%

20491

774 
\isamarkupsection{Rules \label{sec:rules}%

18537

775 
}


776 
\isamarkuptrue%


777 
%

20929

778 
\isadelimFIXME


779 
%


780 
\endisadelimFIXME


781 
%


782 
\isatagFIXME


783 
%

18537

784 
\begin{isamarkuptext}%


785 
FIXME


786 

20491

787 
A \emph{rule} is any Pure theorem in HHF normal form; there is a


788 
separate calculus for rule composition, which is modeled after


789 
Gentzen's Natural Deduction \cite{Gentzen:1935}, but allows


790 
rules to be nested arbitrarily, similar to \cite{extensions91}.


791 


792 
Normally, all theorems accessible to the user are proper rules.


793 
Lowlevel inferences are occasional required internally, but the


794 
result should be always presented in canonical form. The higher


795 
interfaces of Isabelle/Isar will always produce proper rules. It is


796 
important to maintain this invariant in addon applications!


797 


798 
There are two main principles of rule composition: \isa{resolution} (i.e.\ backchaining of rules) and \isa{by{\isacharminus}assumption} (i.e.\ closing a branch); both principles are

20519

799 
combined in the variants of \isa{elim{\isacharminus}resolution} and \isa{dest{\isacharminus}resolution}. Raw \isa{composition} is occasionally

20491

800 
useful as well, also it is strictly speaking outside of the proper


801 
rule calculus.


802 


803 
Rules are treated modulo general higherorder unification, which is


804 
unification modulo the equational theory of \isa{{\isasymalpha}{\isasymbeta}{\isasymeta}}conversion


805 
on \isa{{\isasymlambda}}terms. Moreover, propositions are understood modulo


806 
the (derived) equivalence \isa{{\isacharparenleft}A\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ B\ x{\isacharparenright}{\isacharparenright}\ {\isasymequiv}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ A\ {\isasymLongrightarrow}\ B\ x{\isacharparenright}}.


807 


808 
This means that any operations within the rule calculus may be


809 
subject to spontaneous \isa{{\isasymalpha}{\isasymbeta}{\isasymeta}}HHF conversions. It is common


810 
practice not to contract or expand unnecessarily. Some mechanisms


811 
prefer an one form, others the opposite, so there is a potential


812 
danger to produce some oscillation!


813 


814 
Only few operations really work \emph{modulo} HHF conversion, but


815 
expect a normal form: quantifiers \isa{{\isasymAnd}} before implications


816 
\isa{{\isasymLongrightarrow}} at each level of nesting.


817 

18537

818 
\glossary{Hereditary Harrop Formula}{The set of propositions in HHF


819 
format is defined inductively as \isa{H\ {\isacharequal}\ {\isacharparenleft}{\isasymAnd}x\isactrlsup {\isacharasterisk}{\isachardot}\ H\isactrlsup {\isacharasterisk}\ {\isasymLongrightarrow}\ A{\isacharparenright}}, for variables \isa{x} and atomic propositions \isa{A}.


820 
Any proposition may be put into HHF form by normalizing with the rule


821 
\isa{{\isacharparenleft}A\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ B\ x{\isacharparenright}{\isacharparenright}\ {\isasymequiv}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ A\ {\isasymLongrightarrow}\ B\ x{\isacharparenright}}. In Isabelle, the outermost


822 
quantifier prefix is represented via \seeglossary{schematic


823 
variables}, such that the toplevel structure is merely that of a


824 
\seeglossary{Horn Clause}}.


825 

20499

826 
\glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}


827 


828 


829 
\[


830 
\infer[\isa{{\isacharparenleft}assumption{\isacharparenright}}]{\isa{C{\isasymvartheta}}}


831 
{\isa{{\isacharparenleft}{\isasymAnd}\isactrlvec x{\isachardot}\ \isactrlvec H\ \isactrlvec x\ {\isasymLongrightarrow}\ A\ \isactrlvec x{\isacharparenright}\ {\isasymLongrightarrow}\ C} & \isa{A{\isasymvartheta}\ {\isacharequal}\ H\isactrlsub i{\isasymvartheta}}~~\text{(for some~\isa{i})}}


832 
\]


833 


834 


835 
\[


836 
\infer[\isa{{\isacharparenleft}compose{\isacharparenright}}]{\isa{\isactrlvec A{\isasymvartheta}\ {\isasymLongrightarrow}\ C{\isasymvartheta}}}


837 
{\isa{\isactrlvec A\ {\isasymLongrightarrow}\ B} & \isa{B{\isacharprime}\ {\isasymLongrightarrow}\ C} & \isa{B{\isasymvartheta}\ {\isacharequal}\ B{\isacharprime}{\isasymvartheta}}}


838 
\]


839 


840 


841 
\[


842 
\infer[\isa{{\isacharparenleft}{\isasymAnd}{\isacharunderscore}lift{\isacharparenright}}]{\isa{{\isacharparenleft}{\isasymAnd}\isactrlvec x{\isachardot}\ \isactrlvec A\ {\isacharparenleft}{\isacharquery}\isactrlvec a\ \isactrlvec x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}\isactrlvec x{\isachardot}\ B\ {\isacharparenleft}{\isacharquery}\isactrlvec a\ \isactrlvec x{\isacharparenright}{\isacharparenright}}}{\isa{\isactrlvec A\ {\isacharquery}\isactrlvec a\ {\isasymLongrightarrow}\ B\ {\isacharquery}\isactrlvec a}}


843 
\]


844 
\[


845 
\infer[\isa{{\isacharparenleft}{\isasymLongrightarrow}{\isacharunderscore}lift{\isacharparenright}}]{\isa{{\isacharparenleft}\isactrlvec H\ {\isasymLongrightarrow}\ \isactrlvec A{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}\isactrlvec H\ {\isasymLongrightarrow}\ B{\isacharparenright}}}{\isa{\isactrlvec A\ {\isasymLongrightarrow}\ B}}


846 
\]


847 


848 
The \isa{resolve} scheme is now acquired from \isa{{\isasymAnd}{\isacharunderscore}lift},


849 
\isa{{\isasymLongrightarrow}{\isacharunderscore}lift}, and \isa{compose}.


850 


851 
\[


852 
\infer[\isa{{\isacharparenleft}resolution{\isacharparenright}}]


853 
{\isa{{\isacharparenleft}{\isasymAnd}\isactrlvec x{\isachardot}\ \isactrlvec H\ \isactrlvec x\ {\isasymLongrightarrow}\ \isactrlvec A\ {\isacharparenleft}{\isacharquery}\isactrlvec a\ \isactrlvec x{\isacharparenright}{\isacharparenright}{\isasymvartheta}\ {\isasymLongrightarrow}\ C{\isasymvartheta}}}


854 
{\begin{tabular}{l}


855 
\isa{\isactrlvec A\ {\isacharquery}\isactrlvec a\ {\isasymLongrightarrow}\ B\ {\isacharquery}\isactrlvec a} \\


856 
\isa{{\isacharparenleft}{\isasymAnd}\isactrlvec x{\isachardot}\ \isactrlvec H\ \isactrlvec x\ {\isasymLongrightarrow}\ B{\isacharprime}\ \isactrlvec x{\isacharparenright}\ {\isasymLongrightarrow}\ C} \\


857 
\isa{{\isacharparenleft}{\isasymlambda}\isactrlvec x{\isachardot}\ B\ {\isacharparenleft}{\isacharquery}\isactrlvec a\ \isactrlvec x{\isacharparenright}{\isacharparenright}{\isasymvartheta}\ {\isacharequal}\ B{\isacharprime}{\isasymvartheta}} \\


858 
\end{tabular}}


859 
\]


860 


861 


862 
FIXME \isa{elim{\isacharunderscore}resolution}, \isa{dest{\isacharunderscore}resolution}%

18537

863 
\end{isamarkuptext}%


864 
\isamarkuptrue%


865 
%

20929

866 
\endisatagFIXME


867 
{\isafoldFIXME}%


868 
%


869 
\isadelimFIXME


870 
%


871 
\endisadelimFIXME


872 
%

18537

873 
\isadelimtheory


874 
%


875 
\endisadelimtheory


876 
%


877 
\isatagtheory


878 
\isacommand{end}\isamarkupfalse%


879 
%


880 
\endisatagtheory


881 
{\isafoldtheory}%


882 
%


883 
\isadelimtheory


884 
%


885 
\endisadelimtheory


886 
\isanewline


887 
\end{isabellebody}%


888 
%%% Local Variables:


889 
%%% mode: latex


890 
%%% TeXmaster: "root"


891 
%%% End:
