18537

1 


2 
(* $Id$ *)


3 


4 
theory logic imports base begin


5 

20470

6 
chapter {* Primitive logic \label{ch:logic} *}

18537

7 

20480

8 
text {*


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


10 
which has been introduced as a naturaldeduction framework in


11 
\cite{paulson700}. This is essentially the same logic as ``@{text

20493

12 
"\<lambda>HOL"}'' in the more abstract setting of Pure Type Systems (PTS)

20480

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

20491

14 
differences in the specific treatment of simple types in


15 
Isabelle/Pure.

20480

16 


17 
Following typetheoretic parlance, the Pure logic consists of three

20543

18 
levels of @{text "\<lambda>"}calculus with corresponding arrows, @{text

20480

19 
"\<Rightarrow>"} for syntactic function space (terms depending on terms), @{text


20 
"\<And>"} for universal quantification (proofs depending on terms), and


21 
@{text "\<Longrightarrow>"} for implication (proofs depending on proofs).


22 

20537

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


24 
constructors, constants, and axioms. Theory declarations support


25 
schematic polymorphism, which is strictly speaking outside the


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


27 
context @{text "\<Theta>"} is separate from the proof context @{text "\<Gamma>"}


28 
of the core calculus.}

20480

29 
*}


30 


31 

20451

32 
section {* Types \label{sec:types} *}

20437

33 


34 
text {*

20480

35 
The language of types is an uninterpreted ordersorted firstorder


36 
algebra; types are qualified by ordered type classes.


37 


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


39 
declared in the theory context. The \emph{subclass relation} @{text


40 
"c\<^isub>1 \<subseteq> c\<^isub>2"} is specified by stating an acyclic

20491

41 
generating relation; the transitive closure is maintained


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


43 
transitive, and antisymmetric.

20451

44 

20537

45 
A \emph{sort} is a list of type classes written as @{text "s =


46 
{c\<^isub>1, \<dots>, c\<^isub>m}"}, which represents symbolic

20480

47 
intersection. Notationally, the curly braces are omitted for


48 
singleton intersections, i.e.\ any class @{text "c"} may be read as


49 
a sort @{text "{c}"}. The ordering on type classes is extended to

20491

50 
sorts according to the meaning of intersections: @{text


51 
"{c\<^isub>1, \<dots> c\<^isub>m} \<subseteq> {d\<^isub>1, \<dots>, d\<^isub>n}"} iff


52 
@{text "\<forall>j. \<exists>i. c\<^isub>i \<subseteq> d\<^isub>j"}. The empty intersection


53 
@{text "{}"} refers to the universal sort, which is the largest


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


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


56 
elements wrt.\ the sort order.

20480

57 

20491

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

20537

59 
(starting with a @{text "'"} character) and a sort constraint, e.g.\


60 
@{text "('a, s)"} which is usually printed as @{text "\<alpha>\<^isub>s"}.


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


62 
sort constraint, e.g.\ @{text "(('a, 0), s)"} which is usually


63 
printed as @{text "?\<alpha>\<^isub>s"}.

20451

64 

20480

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

20493

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


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


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


69 
produce anything like this.

20451

70 

20493

71 
A \emph{type constructor} @{text "\<kappa>"} is a @{text "k"}ary operator


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

20537

73 
written postfix as @{text "(\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>k)\<kappa>"}. For


74 
@{text "k = 0"} the argument tuple is omitted, e.g.\ @{text "prop"}


75 
instead of @{text "()prop"}. For @{text "k = 1"} the parentheses


76 
are omitted, e.g.\ @{text "\<alpha> list"} instead of @{text "(\<alpha>)list"}.


77 
Further notation is provided for specific constructors, notably the


78 
rightassociative infix @{text "\<alpha> \<Rightarrow> \<beta>"} instead of @{text "(\<alpha>,


79 
\<beta>)fun"}.

20480

80 

20537

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


82 
constructors as follows: @{text "\<tau> = \<alpha>\<^isub>s  ?\<alpha>\<^isub>s 

20543

83 
(\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)\<kappa>"}.

20451

84 

20514

85 
A \emph{type abbreviation} is a syntactic definition @{text

20494

86 
"(\<^vec>\<alpha>)\<kappa> = \<tau>"} of an arbitrary type expression @{text "\<tau>"} over

20537

87 
variables @{text "\<^vec>\<alpha>"}. Type abbreviations appear as type


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


89 
logical core.

20480

90 


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

20494

92 
constructor wrt.\ the algebra of sorts: @{text "\<kappa> :: (s\<^isub>1, \<dots>,


93 
s\<^isub>k)s"} means that @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>k)\<kappa>"} is


94 
of sort @{text "s"} if every argument type @{text "\<tau>\<^isub>i"} is


95 
of sort @{text "s\<^isub>i"}. Arity declarations are implicitly


96 
completed, i.e.\ @{text "\<kappa> :: (\<^vec>s)c"} entails @{text "\<kappa> ::

20491

97 
(\<^vec>s)c'"} for any @{text "c' \<supseteq> c"}.


98 


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


100 
which means that type arities are consistent with the subclass

20537

101 
relation: for any type constructor @{text "\<kappa>"}, and classes @{text


102 
"c\<^isub>1 \<subseteq> c\<^isub>2"}, and arities @{text "\<kappa> ::


103 
(\<^vec>s\<^isub>1)c\<^isub>1"} and @{text "\<kappa> ::


104 
(\<^vec>s\<^isub>2)c\<^isub>2"} holds @{text "\<^vec>s\<^isub>1 \<subseteq>


105 
\<^vec>s\<^isub>2"} componentwise.

20451

106 

20491

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

20537

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


109 
constructor @{text "\<kappa>"} and sort @{text "s"} there is a most general


110 
vector of argument sorts @{text "(s\<^isub>1, \<dots>, s\<^isub>k)"} such


111 
that a type scheme @{text "(\<alpha>\<^bsub>s\<^isub>1\<^esub>, \<dots>,


112 
\<alpha>\<^bsub>s\<^isub>k\<^esub>)\<kappa>"} is of sort @{text "s"}.

20543

113 
Consequently, type unification has most general solutions (modulo


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


115 
expected \cite{nipkowprehofer}.

20480

116 
*}

20451

117 

20480

118 
text %mlref {*


119 
\begin{mldecls}


120 
@{index_ML_type class} \\


121 
@{index_ML_type sort} \\

20494

122 
@{index_ML_type arity} \\

20480

123 
@{index_ML_type typ} \\

20519

124 
@{index_ML map_atyps: "(typ > typ) > typ > typ"} \\

20494

125 
@{index_ML fold_atyps: "(typ > 'a > 'a) > typ > 'a > 'a"} \\

20547

126 
\end{mldecls}


127 
\begin{mldecls}

20480

128 
@{index_ML Sign.subsort: "theory > sort * sort > bool"} \\


129 
@{index_ML Sign.of_sort: "theory > typ * sort > bool"} \\

20520

130 
@{index_ML Sign.add_types: "(string * int * mixfix) list > theory > theory"} \\

20480

131 
@{index_ML Sign.add_tyabbrs_i: "

20520

132 
(string * string list * typ * mixfix) list > theory > theory"} \\

20480

133 
@{index_ML Sign.primitive_class: "string * class list > theory > theory"} \\


134 
@{index_ML Sign.primitive_classrel: "class * class > theory > theory"} \\


135 
@{index_ML Sign.primitive_arity: "arity > theory > theory"} \\


136 
\end{mldecls}


137 


138 
\begin{description}


139 


140 
\item @{ML_type class} represents type classes; this is an alias for


141 
@{ML_type string}.


142 


143 
\item @{ML_type sort} represents sorts; this is an alias for


144 
@{ML_type "class list"}.

20451

145 

20480

146 
\item @{ML_type arity} represents type arities; this is an alias for

20494

147 
triples of the form @{text "(\<kappa>, \<^vec>s, s)"} for @{text "\<kappa> ::

20480

148 
(\<^vec>s)s"} described above.


149 


150 
\item @{ML_type typ} represents types; this is a datatype with


151 
constructors @{ML TFree}, @{ML TVar}, @{ML Type}.


152 

20537

153 
\item @{ML map_atyps}~@{text "f \<tau>"} applies the mapping @{text "f"}


154 
to all atomic types (@{ML TFree}, @{ML TVar}) occurring in @{text


155 
"\<tau>"}.

20519

156 

20537

157 
\item @{ML fold_atyps}~@{text "f \<tau>"} iterates the operation @{text


158 
"f"} over all occurrences of atomic types (@{ML TFree}, @{ML TVar})


159 
in @{text "\<tau>"}; the type structure is traversed from left to right.

20494

160 

20480

161 
\item @{ML Sign.subsort}~@{text "thy (s\<^isub>1, s\<^isub>2)"}


162 
tests the subsort relation @{text "s\<^isub>1 \<subseteq> s\<^isub>2"}.


163 

20537

164 
\item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether type


165 
@{text "\<tau>"} is of sort @{text "s"}.

20480

166 

20537

167 
\item @{ML Sign.add_types}~@{text "[(\<kappa>, k, mx), \<dots>]"} declares a new

20494

168 
type constructors @{text "\<kappa>"} with @{text "k"} arguments and

20480

169 
optional mixfix syntax.

20451

170 

20494

171 
\item @{ML Sign.add_tyabbrs_i}~@{text "[(\<kappa>, \<^vec>\<alpha>, \<tau>, mx), \<dots>]"}


172 
defines a new type abbreviation @{text "(\<^vec>\<alpha>)\<kappa> = \<tau>"} with

20491

173 
optional mixfix syntax.

20480

174 


175 
\item @{ML Sign.primitive_class}~@{text "(c, [c\<^isub>1, \<dots>,

20537

176 
c\<^isub>n])"} declares a new class @{text "c"}, together with class

20494

177 
relations @{text "c \<subseteq> c\<^isub>i"}, for @{text "i = 1, \<dots>, n"}.

20480

178 


179 
\item @{ML Sign.primitive_classrel}~@{text "(c\<^isub>1,

20543

180 
c\<^isub>2)"} declares the class relation @{text "c\<^isub>1 \<subseteq>

20480

181 
c\<^isub>2"}.


182 

20494

183 
\item @{ML Sign.primitive_arity}~@{text "(\<kappa>, \<^vec>s, s)"} declares

20537

184 
the arity @{text "\<kappa> :: (\<^vec>s)s"}.

20480

185 


186 
\end{description}

20437

187 
*}


188 


189 

20480

190 

20451

191 
section {* Terms \label{sec:terms} *}

18537

192 


193 
text {*

20451

194 
\glossary{Term}{FIXME}

18537

195 

20491

196 
The language of terms is that of simplytyped @{text "\<lambda>"}calculus

20520

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

20537

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


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


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

20514

201 


202 
\medskip A \emph{bound variable} is a natural number @{text "b"},

20537

203 
which accounts for the number of intermediate binders between the


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

20543

205 
example, the deBruijn term @{text


206 
"\<lambda>\<^bsub>nat\<^esub>. \<lambda>\<^bsub>nat\<^esub>. 1 + 0"} would


207 
correspond to @{text


208 
"\<lambda>x\<^bsub>nat\<^esub>. \<lambda>y\<^bsub>nat\<^esub>. x + y"} in a named


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


210 
different deBruijn indices at different occurrences, depending on


211 
the nesting of abstractions.

20537

212 

20543

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

20537

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

20543

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


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


217 
without any loose variables.

20514

218 

20537

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


220 
@{text "(x, \<tau>)"} which is usually printed @{text "x\<^isub>\<tau>"}. A


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


222 
e.g.\ @{text "((x, 0), \<tau>)"} which is usually printed as @{text


223 
"?x\<^isub>\<tau>"}.

20491

224 

20537

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


226 
e.g.\ @{text "(c, \<tau>)"} which is usually printed as @{text


227 
"c\<^isub>\<tau>"}. Constants are declared in the context as polymorphic

20543

228 
families @{text "c :: \<sigma>"}, meaning that all substitution instances


229 
@{text "c\<^isub>\<tau>"} for @{text "\<tau> = \<sigma>\<vartheta>"} are valid.

20514

230 

20537

231 
The vector of \emph{type arguments} of constant @{text "c\<^isub>\<tau>"}


232 
wrt.\ the declaration @{text "c :: \<sigma>"} is defined as the codomain of


233 
the matcher @{text "\<vartheta> = {?\<alpha>\<^isub>1 \<mapsto> \<tau>\<^isub>1, \<dots>,


234 
?\<alpha>\<^isub>n \<mapsto> \<tau>\<^isub>n}"} presented in canonical order @{text


235 
"(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n)"}. Within a given theory context,


236 
there is a onetoone correspondence between any constant @{text


237 
"c\<^isub>\<tau>"} and the application @{text "c(\<tau>\<^isub>1, \<dots>,


238 
\<tau>\<^isub>n)"} of its type arguments. For example, with @{text "plus


239 
:: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"}, the instance @{text "plus\<^bsub>nat \<Rightarrow> nat \<Rightarrow>


240 
nat\<^esub>"} corresponds to @{text "plus(nat)"}.

20480

241 

20514

242 
Constant declarations @{text "c :: \<sigma>"} may contain sort constraints


243 
for type variables in @{text "\<sigma>"}. These are observed by


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


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

20537

246 
polymorphic constants that the userlevel typechecker would reject


247 
due to violation of type class restrictions.

20480

248 

20543

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


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


251 
abstraction and application as follows: @{text "t = b  x\<^isub>\<tau> 


252 
?x\<^isub>\<tau>  c\<^isub>\<tau>  \<lambda>\<^isub>\<tau>. t  t\<^isub>1 t\<^isub>2"}.


253 
Parsing and printing takes care of converting between an external


254 
representation with named bound variables. Subsequently, we shall


255 
use the latter notation instead of internal deBruijn


256 
representation.

20498

257 

20537

258 
The inductive relation @{text "t :: \<tau>"} assigns a (unique) type to a


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


260 
applicatins:

20498

261 
\[

20501

262 
\infer{@{text "a\<^isub>\<tau> :: \<tau>"}}{}

20498

263 
\qquad

20501

264 
\infer{@{text "(\<lambda>x\<^sub>\<tau>. t) :: \<tau> \<Rightarrow> \<sigma>"}}{@{text "t :: \<sigma>"}}


265 
\qquad


266 
\infer{@{text "t u :: \<sigma>"}}{@{text "t :: \<tau> \<Rightarrow> \<sigma>"} & @{text "u :: \<tau>"}}

20498

267 
\]

20514

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

20498

269 

20514

270 
Typing information can be omitted: typeinference is able to


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


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


273 
Typeinference depends on a context of type constraints for fixed


274 
variables, and declarations for polymorphic constants.


275 

20537

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


277 
component. This means that different variables @{text


278 
"x\<^bsub>\<tau>\<^isub>1\<^esub>"} and @{text


279 
"x\<^bsub>\<tau>\<^isub>2\<^esub>"} 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 @{text "t :: \<sigma>"}


285 
is the set of type variables occurring in @{text "t"}, but not in

20537

286 
@{text "\<sigma>"}. 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 @{text "t\<vartheta> :: \<sigma>"} and @{text


289 
"t\<vartheta>' :: \<sigma>"} with the same type. This slightly

20543

290 
pathological situation notoriously demands additional care.

20514

291 


292 
\medskip A \emph{term abbreviation} is a syntactic definition @{text

20537

293 
"c\<^isub>\<sigma> \<equiv> t"} of a closed term @{text "t"} of type @{text "\<sigma>"},


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

20543

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


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


297 
@{text "t \<rightarrow> c\<^isub>\<sigma>"} as rules for higherorder rewriting.

20519

298 


299 
\medskip Canonical operations on @{text "\<lambda>"}terms include @{text

20537

300 
"\<alpha>\<beta>\<eta>"}conversion: @{text "\<alpha>"}conversion refers to capturefree

20519

301 
renaming of bound variables; @{text "\<beta>"}conversion contracts an

20537

302 
abstraction applied to an argument term, substituting the argument

20519

303 
in the body: @{text "(\<lambda>x. b)a"} becomes @{text "b[a/x]"}; @{text


304 
"\<eta>"}conversion contracts vacuous applicationabstraction: @{text


305 
"\<lambda>x. f x"} becomes @{text "f"}, provided that the bound variable

20537

306 
does not occur in @{text "f"}.

20519

307 

20537

308 
Terms are normally treated modulo @{text "\<alpha>"}conversion, which is


309 
implicit in the deBruijn representation. Names for bound variables


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


311 
mostly for parsing and printing. Full @{text "\<alpha>\<beta>\<eta>"}conversion is

20543

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

20537

313 
are based on higherorder unification and matching.

18537

314 
*}


315 

20514

316 
text %mlref {*


317 
\begin{mldecls}


318 
@{index_ML_type term} \\

20519

319 
@{index_ML "op aconv": "term * term > bool"} \\

20547

320 
@{index_ML map_types: "(typ > typ) > term > term"} \\

20519

321 
@{index_ML fold_types: "(typ > 'a > 'a) > term > 'a > 'a"} \\

20514

322 
@{index_ML map_aterms: "(term > term) > term > term"} \\


323 
@{index_ML fold_aterms: "(term > 'a > 'a) > term > 'a > 'a"} \\

20547

324 
\end{mldecls}


325 
\begin{mldecls}

20514

326 
@{index_ML fastype_of: "term > typ"} \\

20519

327 
@{index_ML lambda: "term > term > term"} \\


328 
@{index_ML betapply: "term * term > term"} \\

20520

329 
@{index_ML Sign.add_consts_i: "(string * typ * mixfix) list > theory > theory"} \\

24828

330 
@{index_ML Sign.add_abbrev: "string > Markup.property list > bstring * term > theory > (term * term) * theory"} \\

20519

331 
@{index_ML Sign.const_typargs: "theory > string * typ > typ list"} \\


332 
@{index_ML Sign.const_instance: "theory > string * typ list > typ"} \\

20514

333 
\end{mldecls}

18537

334 

20514

335 
\begin{description}

18537

336 

20537

337 
\item @{ML_type term} represents deBruijn terms, with comments in


338 
abstractions, and explicitly named free variables and constants;


339 
this is a datatype with constructors @{ML Bound}, @{ML Free}, @{ML


340 
Var}, @{ML Const}, @{ML Abs}, @{ML "op $"}.

20519

341 


342 
\item @{text "t"}~@{ML aconv}~@{text "u"} checks @{text


343 
"\<alpha>"}equivalence of two terms. This is the basic equality relation


344 
on type @{ML_type term}; raw datatype equality should only be used


345 
for operations related to parsing or printing!


346 

20547

347 
\item @{ML map_types}~@{text "f t"} applies the mapping @{text

20537

348 
"f"} to all types occurring in @{text "t"}.


349 


350 
\item @{ML fold_types}~@{text "f t"} iterates the operation @{text


351 
"f"} over all occurrences of types in @{text "t"}; the term


352 
structure is traversed from left to right.

20519

353 

20537

354 
\item @{ML map_aterms}~@{text "f t"} applies the mapping @{text "f"}


355 
to all atomic terms (@{ML Bound}, @{ML Free}, @{ML Var}, @{ML


356 
Const}) occurring in @{text "t"}.


357 


358 
\item @{ML fold_aterms}~@{text "f t"} iterates the operation @{text


359 
"f"} over all occurrences of atomic terms (@{ML Bound}, @{ML Free},


360 
@{ML Var}, @{ML Const}) in @{text "t"}; the term structure is

20519

361 
traversed from left to right.


362 

20537

363 
\item @{ML fastype_of}~@{text "t"} determines the type of a


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


365 
omission of any sanity checks.

20519

366 


367 
\item @{ML lambda}~@{text "a b"} produces an abstraction @{text

20537

368 
"\<lambda>a. b"}, where occurrences of the atomic term @{text "a"} in the


369 
body @{text "b"} are replaced by bound variables.

20519

370 

20537

371 
\item @{ML betapply}~@{text "(t, u)"} produces an application @{text


372 
"t u"}, with topmost @{text "\<beta>"}conversion if @{text "t"} is an


373 
abstraction.

20519

374 


375 
\item @{ML Sign.add_consts_i}~@{text "[(c, \<sigma>, mx), \<dots>]"} declares a


376 
new constant @{text "c :: \<sigma>"} with optional mixfix syntax.


377 

24828

378 
\item @{ML Sign.add_abbrev}~@{text "print_mode properties (c, t)"}

21827

379 
introduces a new term abbreviation @{text "c \<equiv> t"}.

20519

380 

20520

381 
\item @{ML Sign.const_typargs}~@{text "thy (c, \<tau>)"} and @{ML


382 
Sign.const_instance}~@{text "thy (c, [\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n])"}

20543

383 
convert between two representations of polymorphic constants: full


384 
type instance vs.\ compact type arguments form.

18537

385 

20514

386 
\end{description}

18537

387 
*}


388 


389 

20451

390 
section {* Theorems \label{sec:thms} *}

18537

391 


392 
text {*

20521

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


394 
\seeglossary{type} @{text "prop"}. Internally, there is nothing


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


396 
syntax enforces a clear distinction. Propositions are structured


397 
via implication @{text "A \<Longrightarrow> B"} or universal quantification @{text


398 
"\<And>x. B x"}  anything else is considered atomic. The canonical


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


400 
Formula}. FIXME}

20480

401 

20501

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


403 
proof context, formally @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; both contexts are


404 
rarely spelled out explicitly. Theorems are usually normalized


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

20480

406 

20519

407 
\glossary{Fact}{Sometimes used interchangeably for

20501

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


409 
essentially an extralogical conjunction. Facts emerge either as


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


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

18537

412 

20501

413 
\glossary{Schematic variable}{FIXME}


414 


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


416 
proof context; an arbitrarybutfixed entity within a portion of


417 
proof text. FIXME}

18537

418 

20501

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


420 
variable}. FIXME}


421 


422 
\glossary{Bound variable}{FIXME}

18537

423 

20501

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


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


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


427 
different variables is their binding scope. FIXME}

18537

428 

20543

429 
A \emph{proposition} is a welltyped term of type @{text "prop"}, a

20521

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


431 
hypotheses and the background theory). Primitive inferences include


432 
plain natural deduction rules for the primary connectives @{text

20537

433 
"\<And>"} and @{text "\<Longrightarrow>"} of the framework. There is also a builtin


434 
notion of equality/equivalence @{text "\<equiv>"}.

20521

435 
*}


436 

22322

437 
subsection {* Primitive connectives and rules \label{sec:prim_rules} *}

18537

438 

20521

439 
text {*

20543

440 
The theory @{text "Pure"} contains constant declarations for the


441 
primitive connectives @{text "\<And>"}, @{text "\<Longrightarrow>"}, and @{text "\<equiv>"} of


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


443 
derivability judgment @{text "A\<^isub>1, \<dots>, A\<^isub>n \<turnstile> B"} is


444 
defined inductively by the primitive inferences given in


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


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


447 
builtin equality is conceptually axiomatized as shown in

20521

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

20543

449 
directly with derived inferences.

20521

450 


451 
\begin{figure}[htb]


452 
\begin{center}

20501

453 
\begin{tabular}{ll}


454 
@{text "all :: (\<alpha> \<Rightarrow> prop) \<Rightarrow> prop"} & universal quantification (binder @{text "\<And>"}) \\


455 
@{text "\<Longrightarrow> :: prop \<Rightarrow> prop \<Rightarrow> prop"} & implication (right associative infix) \\

20521

456 
@{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop"} & equality relation (infix) \\

20501

457 
\end{tabular}

20537

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

20521

459 
\end{center}


460 
\end{figure}

18537

461 

20501

462 
\begin{figure}[htb]


463 
\begin{center}

20498

464 
\[


465 
\infer[@{text "(axiom)"}]{@{text "\<turnstile> A"}}{@{text "A \<in> \<Theta>"}}


466 
\qquad


467 
\infer[@{text "(assume)"}]{@{text "A \<turnstile> A"}}{}


468 
\]


469 
\[

20537

470 
\infer[@{text "(\<And>_intro)"}]{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}}{@{text "\<Gamma> \<turnstile> b[x]"} & @{text "x \<notin> \<Gamma>"}}

20498

471 
\qquad

20537

472 
\infer[@{text "(\<And>_elim)"}]{@{text "\<Gamma> \<turnstile> b[a]"}}{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}}

20498

473 
\]


474 
\[


475 
\infer[@{text "(\<Longrightarrow>_intro)"}]{@{text "\<Gamma>  A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}


476 
\qquad


477 
\infer[@{text "(\<Longrightarrow>_elim)"}]{@{text "\<Gamma>\<^sub>1 \<union> \<Gamma>\<^sub>2 \<turnstile> B"}}{@{text "\<Gamma>\<^sub>1 \<turnstile> A \<Longrightarrow> B"} & @{text "\<Gamma>\<^sub>2 \<turnstile> A"}}


478 
\]

20521

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


480 
\end{center}


481 
\end{figure}


482 


483 
\begin{figure}[htb]


484 
\begin{center}


485 
\begin{tabular}{ll}

20537

486 
@{text "\<turnstile> (\<lambda>x. b[x]) a \<equiv> b[a]"} & @{text "\<beta>"}conversion \\

20521

487 
@{text "\<turnstile> x \<equiv> x"} & reflexivity \\


488 
@{text "\<turnstile> x \<equiv> y \<Longrightarrow> P x \<Longrightarrow> P y"} & substitution \\


489 
@{text "\<turnstile> (\<And>x. f x \<equiv> g x) \<Longrightarrow> f \<equiv> g"} & extensionality \\

20537

490 
@{text "\<turnstile> (A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<equiv> B"} & logical equivalence \\

20521

491 
\end{tabular}

20542

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

20501

493 
\end{center}


494 
\end{figure}

18537

495 

20501

496 
The introduction and elimination rules for @{text "\<And>"} and @{text

20537

497 
"\<Longrightarrow>"} are analogous to formation of dependently typed @{text

20501

498 
"\<lambda>"}terms representing the underlying proof objects. Proof terms

20543

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


500 
propositions. The system provides a runtime option to record

20537

501 
explicit proof terms for primitive inferences. Thus all three


502 
levels of @{text "\<lambda>"}calculus become explicit: @{text "\<Rightarrow>"} for


503 
terms, and @{text "\<And>/\<Longrightarrow>"} for proofs (cf.\


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

20491

505 

20537

506 
Observe that locally fixed parameters (as in @{text "\<And>_intro"}) need


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

20543

508 
types of Pure are always inhabitable. ``Assumptions'' @{text "x ::


509 
\<tau>"} for typemembership are only present as long as some @{text


510 
"x\<^isub>\<tau>"} occurs in the statement body.\footnote{This is the key


511 
difference to ``@{text "\<lambda>HOL"}'' in the PTS framework


512 
\cite{BarendregtGeuvers:2001}, where hypotheses @{text "x : A"} are


513 
treated uniformly for propositions and types.}

20501

514 


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

20537

516 
forming all instances of type and term variables: @{text "\<turnstile>


517 
A\<vartheta>"} holds for any substitution instance of an axiom

20543

518 
@{text "\<turnstile> A"}. By pushing substitutions through derivations


519 
inductively, we also get admissible @{text "generalize"} and @{text


520 
"instance"} rules as shown in \figref{fig:substrules}.

20501

521 


522 
\begin{figure}[htb]


523 
\begin{center}

20498

524 
\[

20501

525 
\infer{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}{@{text "\<Gamma> \<turnstile> B[\<alpha>]"} & @{text "\<alpha> \<notin> \<Gamma>"}}


526 
\quad


527 
\infer[\quad@{text "(generalize)"}]{@{text "\<Gamma> \<turnstile> B[?x]"}}{@{text "\<Gamma> \<turnstile> B[x]"} & @{text "x \<notin> \<Gamma>"}}

20498

528 
\]


529 
\[

20501

530 
\infer{@{text "\<Gamma> \<turnstile> B[\<tau>]"}}{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}


531 
\quad


532 
\infer[\quad@{text "(instantiate)"}]{@{text "\<Gamma> \<turnstile> B[t]"}}{@{text "\<Gamma> \<turnstile> B[?x]"}}

20498

533 
\]

20501

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


535 
\end{center}


536 
\end{figure}

18537

537 

20537

538 
Note that @{text "instantiate"} does not require an explicit


539 
sidecondition, because @{text "\<Gamma>"} may never contain schematic


540 
variables.


541 


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

20543

543 
but this would disrupt the monotonicity of reasoning: deriving


544 
@{text "\<Gamma>\<vartheta> \<turnstile> B\<vartheta>"} from @{text "\<Gamma> \<turnstile> B"} is


545 
correct, but @{text "\<Gamma>\<vartheta> \<supseteq> \<Gamma>"} does not necessarily hold:


546 
the result belongs to a different proof context.

20542

547 

20543

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


549 
fly. Logically, this is an instance of the @{text "axiom"} rule


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


551 
The system always records oracle invocations within derivations of


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

20542

553 


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


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

20543

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


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

20542

558 


559 
A \emph{simple definition} consists of a constant declaration @{text

20543

560 
"c :: \<sigma>"} together with an axiom @{text "\<turnstile> c \<equiv> t"}, where @{text "t


561 
:: \<sigma>"} is a closed term without any hidden polymorphism. The RHS


562 
may depend on further defined constants, but not @{text "c"} itself.


563 
Definitions of functions may be presented as @{text "c \<^vec>x \<equiv>


564 
t"} instead of the puristic @{text "c \<equiv> \<lambda>\<^vec>x. t"}.

20542

565 

20543

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


567 
for the same constant, with zero or one equations @{text


568 
"c((\<^vec>\<alpha>)\<kappa>) \<equiv> t"} for each type constructor @{text "\<kappa>"} (for


569 
distinct variables @{text "\<^vec>\<alpha>"}). The RHS may mention


570 
previously defined constants as above, or arbitrary constants @{text


571 
"d(\<alpha>\<^isub>i)"} for some @{text "\<alpha>\<^isub>i"} projected from @{text


572 
"\<^vec>\<alpha>"}. Thus overloaded definitions essentially work by


573 
primitive recursion over the syntactic structure of a single type


574 
argument.

20521

575 
*}

20498

576 

20521

577 
text %mlref {*


578 
\begin{mldecls}


579 
@{index_ML_type ctyp} \\


580 
@{index_ML_type cterm} \\

20547

581 
@{index_ML Thm.ctyp_of: "theory > typ > ctyp"} \\


582 
@{index_ML Thm.cterm_of: "theory > term > cterm"} \\


583 
\end{mldecls}


584 
\begin{mldecls}

20521

585 
@{index_ML_type thm} \\

20542

586 
@{index_ML proofs: "int ref"} \\


587 
@{index_ML Thm.assume: "cterm > thm"} \\


588 
@{index_ML Thm.forall_intr: "cterm > thm > thm"} \\


589 
@{index_ML Thm.forall_elim: "cterm > thm > thm"} \\


590 
@{index_ML Thm.implies_intr: "cterm > thm > thm"} \\


591 
@{index_ML Thm.implies_elim: "thm > thm > thm"} \\


592 
@{index_ML Thm.generalize: "string list * string list > int > thm > thm"} \\


593 
@{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list > thm > thm"} \\


594 
@{index_ML Thm.get_axiom_i: "theory > string > thm"} \\


595 
@{index_ML Thm.invoke_oracle_i: "theory > string > theory * Object.T > thm"} \\

20547

596 
\end{mldecls}


597 
\begin{mldecls}

20542

598 
@{index_ML Theory.add_axioms_i: "(string * term) list > theory > theory"} \\


599 
@{index_ML Theory.add_deps: "string > string * typ > (string * typ) list > theory > theory"} \\


600 
@{index_ML Theory.add_oracle: "string * (theory * Object.T > term) > theory > theory"} \\


601 
@{index_ML Theory.add_defs_i: "bool > bool > (bstring * term) list > theory > theory"} \\

20521

602 
\end{mldecls}


603 


604 
\begin{description}


605 

20542

606 
\item @{ML_type ctyp} and @{ML_type cterm} 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 @{ML ctyp_of}~@{text "thy \<tau>"} and @{ML cterm_of}~@{text "thy


613 
t"} explicitly checks types and terms, respectively. This also


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


615 
abbreviations from the theory context.


616 


617 
Recertification is relatively slow and should be avoided in tight


618 
reasoning loops. There are separate operations to decompose


619 
certified entities (including actual theorems).

20542

620 


621 
\item @{ML_type thm} represents proven propositions. This is an


622 
abstract datatype that guarantees that its values have been


623 
constructed by basic principles of the @{ML_struct Thm} module.

20543

624 
Every @{ML thm} value contains a sliding backreference to the


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

20542

626 

20543

627 
\item @{ML proofs} determines the detail of proof recording within


628 
@{ML_type thm} values: @{ML 0} records only oracles, @{ML 1} records


629 
oracles, axioms and named theorems, @{ML 2} records full proof


630 
terms.

20542

631 


632 
\item @{ML Thm.assume}, @{ML Thm.forall_intr}, @{ML


633 
Thm.forall_elim}, @{ML Thm.implies_intr}, and @{ML Thm.implies_elim}


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


635 


636 
\item @{ML Thm.generalize}~@{text "(\<^vec>\<alpha>, \<^vec>x)"}


637 
corresponds to the @{text "generalize"} rules of

20543

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


639 
variables are generalized simultaneously, specified by the given


640 
basic names.

20521

641 

20542

642 
\item @{ML Thm.instantiate}~@{text "(\<^vec>\<alpha>\<^isub>s,


643 
\<^vec>x\<^isub>\<tau>)"} corresponds to the @{text "instantiate"} rules


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


645 
term variables. Note that the types in @{text "\<^vec>x\<^isub>\<tau>"}


646 
refer to the instantiated versions.


647 


648 
\item @{ML Thm.get_axiom_i}~@{text "thy name"} retrieves a named


649 
axiom, cf.\ @{text "axiom"} in \figref{fig:primrules}.


650 

20543

651 
\item @{ML Thm.invoke_oracle_i}~@{text "thy name arg"} invokes a


652 
named oracle function, cf.\ @{text "axiom"} in


653 
\figref{fig:primrules}.

20521

654 

20543

655 
\item @{ML Theory.add_axioms_i}~@{text "[(name, A), \<dots>]"} declares


656 
arbitrary propositions as axioms.

20542

657 

20543

658 
\item @{ML Theory.add_oracle}~@{text "(name, f)"} declares an oracle


659 
function for generating arbitrary axioms on the fly.

20542

660 


661 
\item @{ML Theory.add_deps}~@{text "name c\<^isub>\<tau>

20543

662 
\<^vec>d\<^isub>\<sigma>"} declares dependencies of a named specification


663 
for constant @{text "c\<^isub>\<tau>"}, relative to existing


664 
specifications for constants @{text "\<^vec>d\<^isub>\<sigma>"}.

20542

665 


666 
\item @{ML Theory.add_defs_i}~@{text "unchecked overloaded [(name, c

20543

667 
\<^vec>x \<equiv> t), \<dots>]"} states a definitional axiom for an existing


668 
constant @{text "c"}. Dependencies are recorded (cf.\ @{ML


669 
Theory.add_deps}), unless the @{text "unchecked"} option is set.

20521

670 


671 
\end{description}


672 
*}


673 


674 

20543

675 
subsection {* Auxiliary definitions *}

20521

676 


677 
text {*

20543

678 
Theory @{text "Pure"} provides a few auxiliary definitions, see


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


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

20501

681 


682 
\begin{figure}[htb]


683 
\begin{center}

20498

684 
\begin{tabular}{ll}

20521

685 
@{text "conjunction :: prop \<Rightarrow> prop \<Rightarrow> prop"} & (infix @{text "&"}) \\


686 
@{text "\<turnstile> A & B \<equiv> (\<And>C. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)"} \\[1ex]

20543

687 
@{text "prop :: prop \<Rightarrow> prop"} & (prefix @{text "#"}, suppressed) \\

20521

688 
@{text "#A \<equiv> A"} \\[1ex]


689 
@{text "term :: \<alpha> \<Rightarrow> prop"} & (prefix @{text "TERM"}) \\


690 
@{text "term x \<equiv> (\<And>A. A \<Longrightarrow> A)"} \\[1ex]


691 
@{text "TYPE :: \<alpha> itself"} & (prefix @{text "TYPE"}) \\


692 
@{text "(unspecified)"} \\

20498

693 
\end{tabular}

20521

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

20501

695 
\end{center}


696 
\end{figure}


697 

20537

698 
Derived conjunction rules include introduction @{text "A \<Longrightarrow> B \<Longrightarrow> A &


699 
B"}, and destructions @{text "A & B \<Longrightarrow> A"} and @{text "A & B \<Longrightarrow> B"}.


700 
Conjunction allows to treat simultaneous assumptions and conclusions


701 
uniformly. For example, multiple claims are intermediately

20543

702 
represented as explicit conjunction, but this is refined into


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


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

20537

705 
\secref{sec:tacticalgoals}).

20498

706 

20537

707 
The @{text "prop"} marker (@{text "#"}) makes arbitrarily complex


708 
propositions appear as atomic, without changing the meaning: @{text


709 
"\<Gamma> \<turnstile> A"} and @{text "\<Gamma> \<turnstile> #A"} are interchangeable. See


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

20521

711 

20543

712 
The @{text "term"} marker turns any welltyped term into a derivable


713 
proposition: @{text "\<turnstile> TERM t"} holds unconditionally. Although


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


715 
uniformly, similar to a typetheoretic framework.

20498

716 

20537

717 
The @{text "TYPE"} constructor is the canonical representative of


718 
the unspecified type @{text "\<alpha> itself"}; it essentially injects the


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


720 
@{text "TYPE(\<tau>)"} for @{text "TYPE\<^bsub>\<tau>

20521

721 
itself\<^esub>"}.

20537

722 
Although being devoid of any particular meaning, the @{text


723 
"TYPE(\<tau>)"} accounts for the type @{text "\<tau>"} within the term


724 
language. In particular, @{text "TYPE(\<alpha>)"} may be used as formal


725 
argument in primitive definitions, in order to circumvent hidden


726 
polymorphism (cf.\ \secref{sec:terms}). For example, @{text "c


727 
TYPE(\<alpha>) \<equiv> A[\<alpha>]"} defines @{text "c :: \<alpha> itself \<Rightarrow> prop"} in terms of


728 
a proposition @{text "A"} that depends on an additional type


729 
argument, which is essentially a predicate on types.

20521

730 
*}

20501

731 

20521

732 
text %mlref {*


733 
\begin{mldecls}


734 
@{index_ML Conjunction.intr: "thm > thm > thm"} \\


735 
@{index_ML Conjunction.elim: "thm > thm * thm"} \\


736 
@{index_ML Drule.mk_term: "cterm > thm"} \\


737 
@{index_ML Drule.dest_term: "thm > cterm"} \\


738 
@{index_ML Logic.mk_type: "typ > term"} \\


739 
@{index_ML Logic.dest_type: "term > typ"} \\


740 
\end{mldecls}


741 


742 
\begin{description}


743 

20542

744 
\item @{ML Conjunction.intr} derives @{text "A & B"} from @{text


745 
"A"} and @{text "B"}.


746 

20543

747 
\item @{ML Conjunction.elim} derives @{text "A"} and @{text "B"}

20542

748 
from @{text "A & B"}.


749 

20543

750 
\item @{ML Drule.mk_term} derives @{text "TERM t"}.

20542

751 

20543

752 
\item @{ML Drule.dest_term} recovers term @{text "t"} from @{text


753 
"TERM t"}.

20542

754 


755 
\item @{ML Logic.mk_type}~@{text "\<tau>"} produces the term @{text


756 
"TYPE(\<tau>)"}.


757 


758 
\item @{ML Logic.dest_type}~@{text "TYPE(\<tau>)"} recovers the type


759 
@{text "\<tau>"}.

20521

760 


761 
\end{description}

20491

762 
*}

18537

763 

20480

764 

20491

765 
section {* Rules \label{sec:rules} *}

18537

766 

20929

767 
text %FIXME {*

18537

768 


769 
FIXME


770 

20491

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


772 
separate calculus for rule composition, which is modeled after


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


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


775 


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


777 
Lowlevel inferences are occasional required internally, but the


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


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


780 
important to maintain this invariant in addon applications!


781 


782 
There are two main principles of rule composition: @{text


783 
"resolution"} (i.e.\ backchaining of rules) and @{text


784 
"byassumption"} (i.e.\ closing a branch); both principles are

20519

785 
combined in the variants of @{text "elimresolution"} and @{text

20491

786 
"destresolution"}. Raw @{text "composition"} is occasionally


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


788 
rule calculus.


789 


790 
Rules are treated modulo general higherorder unification, which is


791 
unification modulo the equational theory of @{text "\<alpha>\<beta>\<eta>"}conversion


792 
on @{text "\<lambda>"}terms. Moreover, propositions are understood modulo


793 
the (derived) equivalence @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}.


794 


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


796 
subject to spontaneous @{text "\<alpha>\<beta>\<eta>"}HHF conversions. It is common


797 
practice not to contract or expand unnecessarily. Some mechanisms


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


799 
danger to produce some oscillation!


800 


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


802 
expect a normal form: quantifiers @{text "\<And>"} before implications


803 
@{text "\<Longrightarrow>"} at each level of nesting.


804 

18537

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


806 
format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow>


807 
A)"}, for variables @{text "x"} and atomic propositions @{text "A"}.


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


809 
@{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}. In Isabelle, the outermost


810 
quantifier prefix is represented via \seeglossary{schematic


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


812 
\seeglossary{Horn Clause}}.


813 


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


815 

20498

816 


817 
\[


818 
\infer[@{text "(assumption)"}]{@{text "C\<vartheta>"}}


819 
{@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> A \<^vec>x) \<Longrightarrow> C"} & @{text "A\<vartheta> = H\<^sub>i\<vartheta>"}~~\text{(for some~@{text i})}}


820 
\]


821 


822 


823 
\[


824 
\infer[@{text "(compose)"}]{@{text "\<^vec>A\<vartheta> \<Longrightarrow> C\<vartheta>"}}


825 
{@{text "\<^vec>A \<Longrightarrow> B"} & @{text "B' \<Longrightarrow> C"} & @{text "B\<vartheta> = B'\<vartheta>"}}


826 
\]


827 


828 


829 
\[


830 
\infer[@{text "(\<And>_lift)"}]{@{text "(\<And>\<^vec>x. \<^vec>A (?\<^vec>a \<^vec>x)) \<Longrightarrow> (\<And>\<^vec>x. B (?\<^vec>a \<^vec>x))"}}{@{text "\<^vec>A ?\<^vec>a \<Longrightarrow> B ?\<^vec>a"}}


831 
\]


832 
\[


833 
\infer[@{text "(\<Longrightarrow>_lift)"}]{@{text "(\<^vec>H \<Longrightarrow> \<^vec>A) \<Longrightarrow> (\<^vec>H \<Longrightarrow> B)"}}{@{text "\<^vec>A \<Longrightarrow> B"}}


834 
\]


835 


836 
The @{text resolve} scheme is now acquired from @{text "\<And>_lift"},


837 
@{text "\<Longrightarrow>_lift"}, and @{text compose}.


838 


839 
\[


840 
\infer[@{text "(resolution)"}]


841 
{@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>A (?\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>"}}


842 
{\begin{tabular}{l}


843 
@{text "\<^vec>A ?\<^vec>a \<Longrightarrow> B ?\<^vec>a"} \\


844 
@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C"} \\


845 
@{text "(\<lambda>\<^vec>x. B (?\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>"} \\


846 
\end{tabular}}


847 
\]


848 


849 


850 
FIXME @{text "elim_resolution"}, @{text "dest_resolution"}

18537

851 
*}


852 

20498

853 

18537

854 
end
