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 


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

20494

91 
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 

20494

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


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


200 
with deBruijn indices for bound variables, and named free


201 
variables, and constants. Terms with loose bound variables are


202 
usually considered malformed. The types of variables and constants


203 
is stored explicitly at each occurrence in the term (which is a


204 
known performance issue).


205 

20481

206 
FIXME deBruijn representation of lambda terms


207 


208 
Term syntax provides explicit abstraction \isa{{\isasymlambda}x\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}{\isachardot}\ b{\isacharparenleft}x{\isacharparenright}}


209 
and application \isa{t\ u}, while types are usually implicit


210 
thanks to typeinference.


211 


212 
Terms of type \isa{prop} are called


213 
propositions. Logical statements are composed via \isa{{\isasymAnd}x\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}{\isachardot}\ B{\isacharparenleft}x{\isacharparenright}} and \isa{A\ {\isasymLongrightarrow}\ B}.%

18537

214 
\end{isamarkuptext}%


215 
\isamarkuptrue%


216 
%


217 
\begin{isamarkuptext}%


218 
FIXME


219 


220 
\glossary{Schematic polymorphism}{FIXME}


221 


222 
\glossary{Type variable}{FIXME}%


223 
\end{isamarkuptext}%


224 
\isamarkuptrue%


225 
%

20451

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

18537

227 
}


228 
\isamarkuptrue%


229 
%


230 
\begin{isamarkuptext}%

20481

231 
Primitive reasoning operates on judgments of the form \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}}, with standard introduction and elimination rules for \isa{{\isasymAnd}} and \isa{{\isasymLongrightarrow}} that refer to fixed parameters \isa{x} and


232 
hypotheses \isa{A} from the context \isa{{\isasymGamma}}. The


233 
corresponding proof terms are left implicit in the classic


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


235 
\cite{BerghoferNipkow:2000}.


236 


237 
The framework also provides definitional equality \isa{{\isasymequiv}\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ prop}, with \isa{{\isasymalpha}{\isasymbeta}{\isasymeta}}conversion rules. The internal


238 
conjunction \isa{{\isacharampersand}\ {\isacharcolon}{\isacharcolon}\ prop\ {\isasymRightarrow}\ prop\ {\isasymRightarrow}\ prop} enables the view of


239 
assumptions and conclusions emerging uniformly as simultaneous


240 
statements.


241 


242 


243 


244 
FIXME

18537

245 


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


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


248 
propositions apart from their type, but the concrete syntax enforces a


249 
clear distinction. Propositions are structured via implication \isa{A\ {\isasymLongrightarrow}\ B} or universal quantification \isa{{\isasymAnd}x{\isachardot}\ B\ x}  anything


250 
else is considered atomic. The canonical form for propositions is


251 
that of a \seeglossary{Hereditary Harrop Formula}.}


252 


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


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


255 
rarely spelled out explicitly. Theorems are usually normalized


256 
according to the \seeglossary{HHF} format.}


257 


258 
\glossary{Fact}{Sometimes used interchangably for


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


260 
essentially an extralogical conjunction. Facts emerge either as


261 
local assumptions, or as results of local goal statements  both may


262 
be simultaneous, hence the list representation.}


263 


264 
\glossary{Schematic variable}{FIXME}


265 


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


267 
proof context; an arbitrarybutfixed entity within a portion of proof


268 
text.}


269 


270 
\glossary{Free variable}{Synonymous for \seeglossary{fixed variable}.}


271 


272 
\glossary{Bound variable}{FIXME}


273 


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


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


276 
\seeglossary{type variable}. The distinguishing feature of different


277 
variables is their binding scope.}%


278 
\end{isamarkuptext}%


279 
\isamarkuptrue%


280 
%

20491

281 
\isamarkupsection{Proof terms%

18537

282 
}


283 
\isamarkuptrue%


284 
%


285 
\begin{isamarkuptext}%

20491

286 
FIXME !?%

18537

287 
\end{isamarkuptext}%


288 
\isamarkuptrue%


289 
%

20491

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

18537

291 
}


292 
\isamarkuptrue%


293 
%


294 
\begin{isamarkuptext}%


295 
FIXME


296 

20491

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


298 
separate calculus for rule composition, which is modeled after


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


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


301 


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


303 
Lowlevel inferences are occasional required internally, but the


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


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


306 
important to maintain this invariant in addon applications!


307 


308 
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


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


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


311 
rule calculus.


312 


313 
Rules are treated modulo general higherorder unification, which is


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


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


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


317 


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


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


320 
practice not to contract or expand unnecessarily. Some mechanisms


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


322 
danger to produce some oscillation!


323 


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


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


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


327 

18537

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


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


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


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


332 
quantifier prefix is represented via \seeglossary{schematic


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


334 
\seeglossary{Horn Clause}}.


335 


336 
\glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}%


337 
\end{isamarkuptext}%


338 
\isamarkuptrue%


339 
%


340 
\isadelimtheory


341 
%


342 
\endisadelimtheory


343 
%


344 
\isatagtheory


345 
\isacommand{end}\isamarkupfalse%


346 
%


347 
\endisatagtheory


348 
{\isafoldtheory}%


349 
%


350 
\isadelimtheory


351 
%


352 
\endisadelimtheory


353 
\isanewline


354 
\end{isabellebody}%


355 
%%% Local Variables:


356 
%%% mode: latex


357 
%%% TeXmaster: "root"


358 
%%% End:
