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


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


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


37 


38 
Pure derivations are relative to a logical theory, which declares

20491

39 
type constructors, term constants, and axioms. Theory declarations


40 
support schematic polymorphism, which is strictly speaking outside


41 
the logic.\footnote{Incidently, this is the main logical reason, why


42 
the theory context \isa{{\isasymTheta}} is separate from the context \isa{{\isasymGamma}} of the core calculus.}%

20481

43 
\end{isamarkuptext}%


44 
\isamarkuptrue%


45 
%

20451

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

18537

47 
}


48 
\isamarkuptrue%


49 
%


50 
\begin{isamarkuptext}%

20481

51 
The language of types is an uninterpreted ordersorted firstorder


52 
algebra; types are qualified by ordered type classes.

20451

53 

20481

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


55 
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

56 
generating relation; the transitive closure is maintained


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


58 
transitive, and antisymmetric.

20451

59 

20481

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


61 
intersection. Notationally, the curly braces are omitted for


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


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

20491

64 
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


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


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


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


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


69 
elements wrt.\ the sort order.

20451

70 

20491

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

20493

72 
(starting with a \isa{{\isacharprime}} character) and a sort constraint. For

20481

73 
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

20491

74 
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}.

20481

75 


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

20493

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


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


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


80 
produce anything like this.

18537

81 

20493

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


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

20494

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


85 
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


86 
parentheses are omitted, e.g.\ \isa{{\isasymalpha}\ list} instead of \isa{{\isacharparenleft}{\isasymalpha}{\isacharparenright}list}. Further notation is provided for specific constructors,


87 
notably the rightassociative infix \isa{{\isasymalpha}\ {\isasymRightarrow}\ {\isasymbeta}} instead of


88 
\isa{{\isacharparenleft}{\isasymalpha}{\isacharcomma}\ {\isasymbeta}{\isacharparenright}fun}.

20481

89 

20514

90 
A \emph{type} \isa{{\isasymtau}} is defined inductively over type variables


91 
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}k}.

20451

92 

20514

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

20494

94 
variables \isa{\isactrlvec {\isasymalpha}}. Type abbreviations looks like type


95 
constructors at the surface, but are fully expanded before entering


96 
the logical core.

20451

97 

20481

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

20494

99 
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


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


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


102 
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

103 

20491

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


105 
which means that type arities are consistent with the subclass

20494

106 
relation: for each type constructor \isa{{\isasymkappa}} and classes \isa{c\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlisub {\isadigit{2}}}, any arity \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlisub {\isadigit{1}}{\isacharparenright}c\isactrlisub {\isadigit{1}}} has a corresponding arity \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlisub {\isadigit{2}}{\isacharparenright}c\isactrlisub {\isadigit{2}}} where \isa{\isactrlvec s\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ \isactrlvec s\isactrlisub {\isadigit{2}}} holds componentwise.

20491

107 


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

20494

109 
constraints may be always solved in a most general fashion: for each


110 
type constructor \isa{{\isasymkappa}} and sort \isa{s} there is a most


111 
general vector of argument sorts \isa{{\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlisub k{\isacharparenright}} such 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

20491

112 
of sort \isa{s}. Consequently, the unification problem on the


113 
algebra of types has most general solutions (modulo renaming and


114 
equivalence of sorts). Moreover, the usual typeinference algorithm


115 
will produce primary types as expected \cite{nipkowprehofer}.%

18537

116 
\end{isamarkuptext}%


117 
\isamarkuptrue%


118 
%

20481

119 
\isadelimmlref


120 
%


121 
\endisadelimmlref


122 
%


123 
\isatagmlref


124 
%


125 
\begin{isamarkuptext}%


126 
\begin{mldecls}


127 
\indexmltype{class}\verbtype class \\


128 
\indexmltype{sort}\verbtype sort \\

20494

129 
\indexmltype{arity}\verbtype arity \\

20481

130 
\indexmltype{typ}\verbtype typ \\

20494

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

20481

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


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


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


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


136 
\verb (bstring * string list * typ * mixfix) list > theory > theory \\


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


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


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


140 
\end{mldecls}


141 


142 
\begin{description}


143 


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


145 
\verbstring.


146 


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


148 
\verbclass list.


149 


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

20494

151 
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

152 


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


154 
constructors \verbTFree, \verbTVar, \verbType.


155 

20494

156 
\item \verbfold_atyps~\isa{f\ {\isasymtau}} iterates function \isa{f}


157 
over all occurrences of atoms (\verbTFree or \verbTVar) of \isa{{\isasymtau}}; the type structure is traversed from left to right.


158 

20481

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


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


161 


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

20491

163 
is of a given sort.

20481

164 

20494

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


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

20481

167 
optional mixfix syntax.


168 

20494

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


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

20491

171 
optional mixfix syntax.

20481

172 

20494

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


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

20481

175 


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


177 

20494

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


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

20481

180 


181 
\end{description}%


182 
\end{isamarkuptext}%


183 
\isamarkuptrue%


184 
%


185 
\endisatagmlref


186 
{\isafoldmlref}%


187 
%


188 
\isadelimmlref


189 
%


190 
\endisadelimmlref


191 
%

20451

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

18537

193 
}


194 
\isamarkuptrue%


195 
%


196 
\begin{isamarkuptext}%

20451

197 
\glossary{Term}{FIXME}

18537

198 

20491

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

20514

200 
with deBruijn indices for bound variables, and named free variables


201 
and constants. Terms with loose bound variables are usually


202 
considered malformed. The types of variables and constants is


203 
stored explicitly at each occurrence in the term.


204 


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


206 
which refers to the next binder that is \isa{b} steps upwards


207 
from the occurrence of \isa{b} (counting from zero). Bindings


208 
may be introduced as abstractions within the term, or as a separate


209 
context (an insideout list). This associates each bound variable


210 
with a type, and a name that is maintained as a comment for parsing


211 
and printing. A \emph{loose variables} is a bound variable that is


212 
outside the current scope of local binders or the context. For


213 
example, the deBruijn term \isa{{\isasymlambda}\isactrlisub {\isasymtau}{\isachardot}\ {\isasymlambda}\isactrlisub {\isasymtau}{\isachardot}\ {\isadigit{1}}\ {\isacharplus}\ {\isadigit{0}}}


214 
corresponds to \isa{{\isasymlambda}x\isactrlisub {\isasymtau}{\isachardot}\ {\isasymlambda}y\isactrlisub {\isasymtau}{\isachardot}\ x\ {\isacharplus}\ y} in a named


215 
representation. Also note that the very same bound variable may get


216 
different numbers at different occurrences.


217 


218 
A \emph{fixed variable} is a pair of a basic name and a type. For


219 
example, \isa{{\isacharparenleft}x{\isacharcomma}\ {\isasymtau}{\isacharparenright}} which is usually printed \isa{x\isactrlisub {\isasymtau}}. A \emph{schematic variable} is a pair of an


220 
indexname and a type. For example, \isa{{\isacharparenleft}{\isacharparenleft}x{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}{\isacharcomma}\ {\isasymtau}{\isacharparenright}} which is


221 
usually printed as \isa{{\isacharquery}x\isactrlisub {\isasymtau}}.

20491

222 

20514

223 
\medskip A \emph{constant} is a atomic terms consisting of a basic


224 
name and a type. Constants are declared in the context as


225 
polymorphic families \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}}, meaning that any \isa{c\isactrlisub {\isasymtau}} is a valid constant for all substitution instances


226 
\isa{{\isasymtau}\ {\isasymle}\ {\isasymsigma}}.


227 


228 
The list of \emph{type arguments} of \isa{c\isactrlisub {\isasymtau}} wrt.\ the


229 
declaration \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} is the codomain of the type matcher


230 
presented in canonical order (according to the lefttoright


231 
occurrences of type variables in in \isa{{\isasymsigma}}). Thus \isa{c\isactrlisub {\isasymtau}} can be represented more compactly as \isa{c{\isacharparenleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub n{\isacharparenright}}. For example, the instance \isa{plus\isactrlbsub nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat\isactrlesub } of some \isa{plus\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}} has the singleton list \isa{nat} as type arguments, the


232 
constant may be represented as \isa{plus{\isacharparenleft}nat{\isacharparenright}}.

20481

233 

20514

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


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


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


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


238 
polymorphic constants that the userlevel typechecker would reject.

20481

239 

20514

240 
\medskip A \emph{term} \isa{t} is defined inductively over


241 
variables and constants, with abstraction and application as


242 
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}}}. Parsing and printing takes


243 
care of converting between an external representation with named


244 
bound variables. Subsequently, we shall use the latter notation


245 
instead of internal deBruijn representation.

20499

246 

20514

247 
The subsequent inductive relation \isa{t\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}} assigns a


248 
(unique) type to a term, using the special type constructor \isa{{\isacharparenleft}{\isasymalpha}{\isacharcomma}\ {\isasymbeta}{\isacharparenright}fun}, which is written \isa{{\isasymalpha}\ {\isasymRightarrow}\ {\isasymbeta}}.

20499

249 
\[

20502

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

20499

251 
\qquad

20502

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


253 
\qquad


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

20514

255 
\]


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


257 


258 
Typing information can be omitted: typeinference is able to


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


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


261 
Typeinference depends on a context of type constraints for fixed


262 
variables, and declarations for polymorphic constants.


263 


264 
The identity of atomic terms consists both of the name and the type.


265 
Thus different entities \isa{c\isactrlbsub {\isasymtau}\isactrlisub {\isadigit{1}}\isactrlesub } and


266 
\isa{c\isactrlbsub {\isasymtau}\isactrlisub {\isadigit{2}}\isactrlesub } may well identified by type


267 
instantiation, by mapping \isa{{\isasymtau}\isactrlisub {\isadigit{1}}} and \isa{{\isasymtau}\isactrlisub {\isadigit{2}}} to the same \isa{{\isasymtau}}. Although,


268 
different type instances of constants of the same basic name are


269 
commonplace, this rarely happens for variables: typeinference


270 
always demands ``consistent'' type constraints.


271 


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


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


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


275 
values of various type variables that are not visible in the overall


276 
type, i.e.\ there are different type instances \isa{t{\isasymvartheta}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} and \isa{t{\isasymvartheta}{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} with the same type. This


277 
slightly pathological situation is apt to cause strange effects.


278 


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


280 
\isa{{\isasymsigma}} without any hidden polymorphism. A term abbreviation


281 
looks like a constant at the surface, but is fully expanded before


282 
entering the logical core. Abbreviations are usually reverted when


283 
printing terms, using rules \isa{t\ {\isasymrightarrow}\ c\isactrlisub {\isasymsigma}} has a


284 
higherorder term rewrite system.%

18537

285 
\end{isamarkuptext}%


286 
\isamarkuptrue%


287 
%

20514

288 
\isadelimmlref


289 
%


290 
\endisadelimmlref


291 
%


292 
\isatagmlref


293 
%

18537

294 
\begin{isamarkuptext}%

20514

295 
\begin{mldecls}


296 
\indexmltype{term}\verbtype term \\


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


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


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


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


301 
\end{mldecls}

18537

302 

20514

303 
\begin{description}

18537

304 

20514

305 
\item \verbterm FIXME


306 


307 
\end{description}%

18537

308 
\end{isamarkuptext}%


309 
\isamarkuptrue%


310 
%

20514

311 
\endisatagmlref


312 
{\isafoldmlref}%


313 
%


314 
\isadelimmlref


315 
%


316 
\endisadelimmlref


317 
%

20451

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

18537

319 
}


320 
\isamarkuptrue%


321 
%


322 
\begin{isamarkuptext}%

20502

323 
\glossary{Proposition}{A \seeglossary{term} of \seeglossary{type}


324 
\isa{prop}. Internally, there is nothing special about


325 
propositions apart from their type, but the concrete syntax enforces


326 
a clear distinction. Propositions are structured via implication


327 
\isa{A\ {\isasymLongrightarrow}\ B} or universal quantification \isa{{\isasymAnd}x{\isachardot}\ B\ x} 


328 
anything else is considered atomic. The canonical form for


329 
propositions is that of a \seeglossary{Hereditary Harrop Formula}. FIXME}

20481

330 

20502

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


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


333 
rarely spelled out explicitly. Theorems are usually normalized


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

18537

335 

20502

336 
\glossary{Fact}{Sometimes used interchangably for


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


338 
essentially an extralogical conjunction. Facts emerge either as


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


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


341 


342 
\glossary{Schematic variable}{FIXME}


343 


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


345 
proof context; an arbitrarybutfixed entity within a portion of


346 
proof text. FIXME}

18537

347 

20502

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


349 
variable}. FIXME}


350 


351 
\glossary{Bound variable}{FIXME}

18537

352 

20502

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


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


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


356 
different variables is their binding scope. FIXME}

18537

357 

20502

358 
A \emph{proposition} is a wellformed term of type \isa{prop}.


359 
The connectives of minimal logic are declared as constants of the


360 
basic theory:

18537

361 

20502

362 
\smallskip


363 
\begin{tabular}{ll}


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


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


366 
\end{tabular}

18537

367 

20502

368 
\medskip A \emph{theorem} is a proven proposition, depending on a


369 
collection of assumptions, and axioms from the theory context. The


370 
judgment \isa{A\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ A\isactrlisub n\ {\isasymturnstile}\ B} is defined


371 
inductively by the primitive inferences given in


372 
\figref{fig:primrules}; there is a global syntactic restriction


373 
that the hypotheses may not contain schematic variables.

18537

374 

20502

375 
\begin{figure}[htb]


376 
\begin{center}

20499

377 
\[


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


379 
\qquad


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


381 
\]


382 
\[


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


384 
\qquad


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


386 
\]


387 
\[


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


389 
\qquad


390 
\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}}


391 
\]

20502

392 
\caption{Primitive inferences of the Pure logic}\label{fig:primrules}


393 
\end{center}


394 
\end{figure}

20499

395 

20502

396 
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


397 
are \emph{irrelevant} in the Pure logic, they may never occur within


398 
propositions, i.e.\ the \isa{{\isasymLongrightarrow}} arrow of the framework is a


399 
nondependent one.

20499

400 

20502

401 
Also note that fixed parameters as in \isa{{\isasymAnd}{\isacharunderscore}intro} need not be


402 
recorded in the context \isa{{\isasymGamma}}, since syntactic types are


403 
always inhabitable. An ``assumption'' \isa{x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}} is logically


404 
vacuous, because \isa{{\isasymtau}} is always nonempty. This is the deeper


405 
reason why \isa{{\isasymGamma}} only consists of hypothetical proofs, but no


406 
hypothetical terms.


407 


408 
The corresponding proof terms are left implicit in the classic


409 
``LCFapproach'', although they could be exploited separately


410 
\cite{BerghoferNipkow:2000}. The implementation provides a runtime


411 
option to control the generation of full proof terms.


412 


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


414 
forming all instances of type and term variables: \isa{{\isasymturnstile}\ A{\isasymtheta}} for

20514

415 
any substitution instance of axiom \isa{{\isasymturnstile}\ A}. By pushing

20502

416 
substitution through derivations inductively, we get admissible


417 
substitution rules for theorems shown in \figref{fig:substrules}.


418 


419 
\begin{figure}[htb]


420 
\begin{center}

20499

421 
\[

20502

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


423 
\quad


424 
\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

425 
\]


426 
\[

20502

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


428 
\quad


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

20499

430 
\]

20502

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


432 
\end{center}


433 
\end{figure}

20499

434 


435 
Note that \isa{instantiate{\isacharunderscore}term} could be derived using \isa{{\isasymAnd}{\isacharunderscore}intro{\isacharslash}elim}, but this is not how it is implemented. The type

20502

436 
instantiation rule is a genuine admissible one, due to the lack of


437 
true polymorphism in the logic.

20499

438 

20502

439 
Since \isa{{\isasymGamma}} may never contain any schematic variables, the


440 
\isa{instantiate} do not require an explicit sidecondition. In


441 
principle, variables could be substituted in hypotheses as well, but


442 
this could disrupt monotonicity of the basic calculus: derivations


443 
could leave the current proof context.

20499

444 

20502

445 
\medskip The framework also provides builtin equality \isa{{\isasymequiv}},


446 
which is conceptually axiomatized shown in \figref{fig:equality},


447 
although the implementation provides derived rules directly:


448 


449 
\begin{figure}[htb]


450 
\begin{center}

20499

451 
\begin{tabular}{ll}


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

20502

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

20499

454 
\isa{{\isasymturnstile}\ x\ {\isasymequiv}\ x} & reflexivity law \\


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


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


457 
\isa{{\isasymturnstile}\ {\isacharparenleft}A\ {\isasymLongrightarrow}\ B{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}B\ {\isasymLongrightarrow}\ A{\isacharparenright}\ {\isasymLongrightarrow}\ A\ {\isasymequiv}\ B} & coincidence with equivalence \\


458 
\end{tabular}

20502

459 
\caption{Conceptual axiomatization of equality.}\label{fig:equality}


460 
\end{center}


461 
\end{figure}


462 


463 
Since the basic representation of terms already accounts for \isa{{\isasymalpha}}conversion, Pure equality essentially acts like \isa{{\isasymalpha}{\isasymbeta}{\isasymeta}}equivalence on terms, while coinciding with biimplication.


464 


465 


466 
\medskip Conjunction is defined in Pure as a derived connective, see


467 
\figref{fig:conjunction}. This is occasionally useful to represent


468 
simultaneous statements behind the scenes  framework conjunction


469 
is usually not exposed to the user.


470 


471 
\begin{figure}[htb]


472 
\begin{center}


473 
\begin{tabular}{ll}


474 
\isa{{\isacharampersand}\ {\isacharcolon}{\isacharcolon}\ prop\ {\isasymRightarrow}\ prop\ {\isasymRightarrow}\ prop} & conjunction (hidden) \\


475 
\isa{{\isasymturnstile}\ A\ {\isacharampersand}\ B\ {\isasymequiv}\ {\isacharparenleft}{\isasymAnd}C{\isachardot}\ {\isacharparenleft}A\ {\isasymLongrightarrow}\ B\ {\isasymLongrightarrow}\ C{\isacharparenright}\ {\isasymLongrightarrow}\ C{\isacharparenright}} \\


476 
\end{tabular}


477 
\caption{Definition of conjunction.}\label{fig:equality}


478 
\end{center}


479 
\end{figure}


480 


481 
The definition allows to derive the usual introduction \isa{{\isasymturnstile}\ A\ {\isasymLongrightarrow}\ B\ {\isasymLongrightarrow}\ A\ {\isacharampersand}\ B}, and destructions \isa{A\ {\isacharampersand}\ B\ {\isasymLongrightarrow}\ A} and \isa{A\ {\isacharampersand}\ B\ {\isasymLongrightarrow}\ B}.%

18537

482 
\end{isamarkuptext}%


483 
\isamarkuptrue%


484 
%

20491

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

18537

486 
}


487 
\isamarkuptrue%


488 
%


489 
\begin{isamarkuptext}%


490 
FIXME


491 

20491

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


493 
separate calculus for rule composition, which is modeled after


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


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


496 


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


498 
Lowlevel inferences are occasional required internally, but the


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


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


501 
important to maintain this invariant in addon applications!


502 


503 
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


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


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


506 
rule calculus.


507 


508 
Rules are treated modulo general higherorder unification, which is


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


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


511 
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}}.


512 


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


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


515 
practice not to contract or expand unnecessarily. Some mechanisms


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


517 
danger to produce some oscillation!


518 


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


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


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


522 

18537

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


524 
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}.


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


526 
\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


527 
quantifier prefix is represented via \seeglossary{schematic


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


529 
\seeglossary{Horn Clause}}.


530 

20499

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


532 


533 


534 
\[


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


536 
{\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})}}


537 
\]


538 


539 


540 
\[


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


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


543 
\]


544 


545 


546 
\[


547 
\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}}


548 
\]


549 
\[


550 
\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}}


551 
\]


552 


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


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


555 


556 
\[


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


558 
{\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}}}


559 
{\begin{tabular}{l}


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


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


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


563 
\end{tabular}}


564 
\]


565 


566 


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

18537

568 
\end{isamarkuptext}%


569 
\isamarkuptrue%


570 
%


571 
\isadelimtheory


572 
%


573 
\endisadelimtheory


574 
%


575 
\isatagtheory


576 
\isacommand{end}\isamarkupfalse%


577 
%


578 
\endisatagtheory


579 
{\isafoldtheory}%


580 
%


581 
\isadelimtheory


582 
%


583 
\endisadelimtheory


584 
\isanewline


585 
\end{isabellebody}%


586 
%%% Local Variables:


587 
%%% mode: latex


588 
%%% TeXmaster: "root"


589 
%%% End:
