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


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


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 


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

20491

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


25 
support schematic polymorphism, which is strictly speaking outside


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


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


28 
"\<Gamma>"} 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 

20480

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


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


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

20493

59 
(starting with a @{text "'"} character) and a sort constraint. For

20480

60 
example, @{text "('a, s)"} which is usually printed as @{text


61 
"\<alpha>\<^isub>s"}. A \emph{schematic type variable} is a pair of an


62 
indexname and a sort constraint. For example, @{text "(('a, 0),

20491

63 
s)"} which is usually 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

20494

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


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


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


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


77 
"(\<alpha>)list"}. Further notation is provided for specific constructors,


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


79 
@{text "(\<alpha>, \<beta>)fun"}.

20480

80 

20514

81 
A \emph{type} @{text "\<tau>"} is defined inductively over type variables


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


83 
?\<alpha>\<^isub>s  (\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)k"}.

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


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


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


89 
the 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

20494

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


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


103 
(\<^vec>s\<^isub>1)c\<^isub>1"} has a corresponding arity @{text "\<kappa>

20480

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

20519

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

20451

106 

20491

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

20494

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


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


110 
general vector of argument sorts @{text "(s\<^isub>1, \<dots>,

20491

111 
s\<^isub>k)"} such that a type scheme @{text

20494

112 
"(\<alpha>\<^bsub>s\<^isub>1\<^esub>, \<dots>, \<alpha>\<^bsub>s\<^isub>k\<^esub>)\<kappa>"} is

20491

113 
of sort @{text "s"}. Consequently, the unification problem on the


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


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


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

20480

117 
*}

20451

118 

20480

119 
text %mlref {*


120 
\begin{mldecls}


121 
@{index_ML_type class} \\


122 
@{index_ML_type sort} \\

20494

123 
@{index_ML_type arity} \\

20480

124 
@{index_ML_type typ} \\

20519

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

20494

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

20480

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


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


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


130 
@{index_ML Sign.add_tyabbrs_i: "


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


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


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


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


135 
\end{mldecls}


136 


137 
\begin{description}


138 


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


140 
@{ML_type string}.


141 


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


143 
@{ML_type "class list"}.

20451

144 

20480

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

20494

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

20480

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


148 


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


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


151 

20519

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


153 
all atomic types (@{ML TFree}, @{ML TVar}) occurring in @{text "\<tau>"}.


154 


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


156 
over all occurrences of atoms (@{ML TFree}, @{ML TVar}) in @{text

20494

157 
"\<tau>"}; the type structure is traversed from left to right.


158 

20480

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


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


161 


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

20491

163 
is of a given sort.

20480

164 

20494

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


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

20480

167 
optional mixfix syntax.

20451

168 

20494

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


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

20491

171 
optional mixfix syntax.

20480

172 


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

20494

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


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

20480

176 


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


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


179 
c\<^isub>2"}.


180 

20494

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


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

20480

183 


184 
\end{description}

20437

185 
*}


186 


187 

20480

188 

20451

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

18537

190 


191 
text {*

20451

192 
\glossary{Term}{FIXME}

18537

193 

20491

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

20519

195 
with deBruijn indices for bound variables


196 
\cite{debruijn72,paulsonml2}, and named free variables and


197 
constants. Terms with loose bound variables are usually considered


198 
malformed. The types of variables and constants is stored


199 
explicitly at each occurrence in the term.

20514

200 


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


202 
which refers to the next binder that is @{text "b"} steps upwards


203 
from the occurrence of @{text "b"} (counting from zero). Bindings


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


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

20519

206 
with a type. A \emph{loose variables} is a bound variable that is

20514

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


208 
example, the deBruijn term @{text "\<lambda>\<^isub>\<tau>. \<lambda>\<^isub>\<tau>. 1 + 0"}


209 
corresponds to @{text "\<lambda>x\<^isub>\<tau>. \<lambda>y\<^isub>\<tau>. x + y"} in a named


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


211 
different numbers at different occurrences.


212 


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


214 
example, @{text "(x, \<tau>)"} which is usually printed @{text


215 
"x\<^isub>\<tau>"}. A \emph{schematic variable} is a pair of an


216 
indexname and a type. For example, @{text "((x, 0), \<tau>)"} which is


217 
usually printed as @{text "?x\<^isub>\<tau>"}.

20491

218 

20514

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


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


221 
polymorphic families @{text "c :: \<sigma>"}, meaning that any @{text


222 
"c\<^isub>\<tau>"} is a valid constant for all substitution instances


223 
@{text "\<tau> \<le> \<sigma>"}.


224 


225 
The list of \emph{type arguments} of @{text "c\<^isub>\<tau>"} wrt.\ the


226 
declaration @{text "c :: \<sigma>"} is the codomain of the type matcher


227 
presented in canonical order (according to the lefttoright


228 
occurrences of type variables in in @{text "\<sigma>"}). Thus @{text


229 
"c\<^isub>\<tau>"} can be represented more compactly as @{text


230 
"c(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n)"}. For example, the instance @{text


231 
"plus\<^bsub>nat \<Rightarrow> nat \<Rightarrow> nat\<^esub>"} of some @{text "plus :: \<alpha> \<Rightarrow> \<alpha>


232 
\<Rightarrow> \<alpha>"} has the singleton list @{text "nat"} as type arguments, the


233 
constant may be represented as @{text "plus(nat)"}.

20480

234 

20514

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


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


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


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


239 
polymorphic constants that the userlevel typechecker would reject.

20480

240 

20514

241 
\medskip A \emph{term} @{text "t"} is defined inductively over


242 
variables and constants, with abstraction and application as


243 
follows: @{text "t = b  x\<^isub>\<tau>  ?x\<^isub>\<tau>  c\<^isub>\<tau> 


244 
\<lambda>\<^isub>\<tau>. t  t\<^isub>1 t\<^isub>2"}. Parsing and printing takes


245 
care of converting between an external representation with named


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


247 
instead of internal deBruijn representation.

20498

248 

20514

249 
The subsequent inductive relation @{text "t :: \<tau>"} assigns a


250 
(unique) type to a term, using the special type constructor @{text


251 
"(\<alpha>, \<beta>)fun"}, which is written @{text "\<alpha> \<Rightarrow> \<beta>"}.

20498

252 
\[

20501

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

20498

254 
\qquad

20501

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


256 
\qquad


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

20498

258 
\]

20514

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

20498

260 

20514

261 
Typing information can be omitted: typeinference is able to


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


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


264 
Typeinference depends on a context of type constraints for fixed


265 
variables, and declarations for polymorphic constants.


266 


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


268 
Thus different entities @{text "c\<^bsub>\<tau>\<^isub>1\<^esub>"} and


269 
@{text "c\<^bsub>\<tau>\<^isub>2\<^esub>"} may well identified by type


270 
instantiation, by mapping @{text "\<tau>\<^isub>1"} and @{text


271 
"\<tau>\<^isub>2"} to the same @{text "\<tau>"}. Although,


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


273 
commonplace, this rarely happens for variables: typeinference


274 
always demands ``consistent'' type constraints.


275 


276 
\medskip The \emph{hidden polymorphism} of a term @{text "t :: \<sigma>"}


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


278 
@{text "\<sigma>"}. This means that the term implicitly depends on the


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


280 
type, i.e.\ there are different type instances @{text "t\<vartheta>


281 
:: \<sigma>"} and @{text "t\<vartheta>' :: \<sigma>"} with the same type. This


282 
slightly pathological situation is apt to cause strange effects.


283 


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


285 
"c\<^isub>\<sigma> \<equiv> t"} of an arbitrary closed term @{text "t"} of type


286 
@{text "\<sigma>"} without any hidden polymorphism. A term abbreviation


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


288 
entering the logical core. Abbreviations are usually reverted when


289 
printing terms, using rules @{text "t \<rightarrow> c\<^isub>\<sigma>"} has a


290 
higherorder term rewrite system.

20519

291 


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


293 
"\<alpha>\<beta>\<eta>"}conversion. @{text "\<alpha>"}conversion refers to capturefree


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


295 
abstraction applied to some argument term, substituting the argument


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


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


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


299 
@{text "0"} does not occur in @{text "f"}.


300 


301 
Terms are almost always treated module @{text "\<alpha>"}conversion, which


302 
is implicit in the deBruijn representation. The names in


303 
abstractions of bound variables are maintained only as a comment for


304 
parsing and printing. Full @{text "\<alpha>\<beta>\<eta>"}equivalence is usually


305 
taken for granted higher rules (\secref{sec:rules}), anything


306 
depending on higherorder unification or rewriting.

18537

307 
*}


308 

20514

309 
text %mlref {*


310 
\begin{mldecls}


311 
@{index_ML_type term} \\

20519

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


313 
@{index_ML map_term_types: "(typ > typ) > term > term"} \\ %FIXME rename map_types


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

20514

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


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


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

20519

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


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


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


321 
@{index_ML Sign.add_abbrevs: "string * bool >


322 
((bstring * mixfix) * term) list > theory > theory"} \\


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


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

20514

325 
\end{mldecls}

18537

326 

20514

327 
\begin{description}

18537

328 

20519

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


330 
abstractions for bound variable names. This is a datatype with


331 
constructors @{ML Bound}, @{ML Free}, @{ML Var}, @{ML Const}, @{ML


332 
Abs}, @{ML "op $"}.


333 


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


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


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


337 
for operations related to parsing or printing!


338 


339 
\item @{ML map_term_types}~@{text "f t"} applies mapping @{text "f"}


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


341 


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


343 
over all occurrences of types in @{text "t"}; the term structure is


344 
traversed from left to right.


345 


346 
\item @{ML map_aterms}~@{text "f t"} applies mapping @{text "f"} to


347 
all atomic terms (@{ML Bound}, @{ML Free}, @{ML Var}, @{ML Const})


348 
occurring in @{text "t"}.


349 


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


351 
over all occurrences of atomic terms in (@{ML Bound}, @{ML Free},


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


353 
from left to right.


354 


355 
\item @{ML fastype_of}~@{text "t"} recomputes the type of a


356 
wellformed term, while omitting any sanity checks. This operation


357 
is relatively slow.


358 


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


360 
"\<lambda>a. b"}, where occurrences of the original (atomic) term @{text


361 
"a"} are replaced by bound variables.


362 


363 
\item @{ML betapply}~@{text "t u"} produces an application @{text "t


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


365 
abstraction.


366 


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


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


369 


370 
\item @{ML Sign.add_abbrevs}~@{text "print_mode [((c, t), mx), \<dots>]"}


371 
declares a new term abbreviation @{text "c \<equiv> t"} with optional


372 
mixfix syntax.


373 


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


375 
type arguments of the instance @{text "c\<^isub>\<tau>"} wrt.\ its


376 
declaration in the theory.


377 


378 
\item @{ML Sign.const_instance}~@{text "thy (c, [\<tau>\<^isub>1, \<dots>,


379 
\<tau>\<^isub>n])"} produces the full instance @{text "c(\<tau>\<^isub>1, \<dots>,


380 
\<tau>\<^isub>n)"} wrt.\ its declaration in the theory.

18537

381 

20514

382 
\end{description}

18537

383 
*}


384 


385 

20451

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

18537

387 


388 
text {*

20501

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


390 
@{text "prop"}. Internally, there is nothing special about


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


392 
a clear distinction. Propositions are structured via implication


393 
@{text "A \<Longrightarrow> B"} or universal quantification @{text "\<And>x. B x"} 


394 
anything else is considered atomic. The canonical form for


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

20480

396 

20501

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


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


399 
rarely spelled out explicitly. Theorems are usually normalized


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

20480

401 

20519

402 
\glossary{Fact}{Sometimes used interchangeably for

20501

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


404 
essentially an extralogical conjunction. Facts emerge either as


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


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

18537

407 

20501

408 
\glossary{Schematic variable}{FIXME}


409 


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


411 
proof context; an arbitrarybutfixed entity within a portion of


412 
proof text. FIXME}

18537

413 

20501

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


415 
variable}. FIXME}


416 


417 
\glossary{Bound variable}{FIXME}

18537

418 

20501

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


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


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


422 
different variables is their binding scope. FIXME}

18537

423 

20501

424 
A \emph{proposition} is a wellformed term of type @{text "prop"}.


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


426 
basic theory:

18537

427 

20501

428 
\smallskip


429 
\begin{tabular}{ll}


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


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


432 
\end{tabular}

18537

433 

20501

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


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


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


437 
inductively by the primitive inferences given in


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


439 
that the hypotheses may not contain schematic variables.

18537

440 

20501

441 
\begin{figure}[htb]


442 
\begin{center}

20498

443 
\[


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


445 
\qquad


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


447 
\]


448 
\[


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


450 
\qquad


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


452 
\]


453 
\[


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


455 
\qquad


456 
\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"}}


457 
\]

20501

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


459 
\end{center}


460 
\end{figure}

18537

461 

20501

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


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


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


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


466 
propositions, i.e.\ the @{text "\<Longrightarrow>"} arrow of the framework is a


467 
nondependent one.

20491

468 

20501

469 
Also note that fixed parameters as in @{text "\<And>_intro"} need not be


470 
recorded in the context @{text "\<Gamma>"}, since syntactic types are


471 
always inhabitable. An ``assumption'' @{text "x :: \<tau>"} is logically


472 
vacuous, because @{text "\<tau>"} is always nonempty. This is the deeper


473 
reason why @{text "\<Gamma>"} only consists of hypothetical proofs, but no


474 
hypothetical terms.


475 


476 
The corresponding proof terms are left implicit in the classic


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


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


479 
option to control the generation of full proof terms.


480 


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


482 
forming all instances of type and term variables: @{text "\<turnstile> A\<theta>"} for

20514

483 
any substitution instance of axiom @{text "\<turnstile> A"}. By pushing

20501

484 
substitution through derivations inductively, we get admissible


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


486 


487 
\begin{figure}[htb]


488 
\begin{center}

20498

489 
\[

20501

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


491 
\quad


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

20498

493 
\]


494 
\[

20501

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


496 
\quad


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

20498

498 
\]

20501

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


500 
\end{center}


501 
\end{figure}

18537

502 

20498

503 
Note that @{text "instantiate_term"} could be derived using @{text


504 
"\<And>_intro/elim"}, but this is not how it is implemented. The type

20501

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


506 
true polymorphism in the logic.

20498

507 

20501

508 
Since @{text "\<Gamma>"} may never contain any schematic variables, the


509 
@{text "instantiate"} do not require an explicit sidecondition. In


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


511 
this could disrupt monotonicity of the basic calculus: derivations


512 
could leave the current proof context.

20498

513 

20501

514 
\medskip The framework also provides builtin equality @{text "\<equiv>"},


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


516 
although the implementation provides derived rules directly:


517 


518 
\begin{figure}[htb]


519 
\begin{center}

20498

520 
\begin{tabular}{ll}


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

20501

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

20498

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


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


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


526 
@{text "\<turnstile> (A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<equiv> B"} & coincidence with equivalence \\


527 
\end{tabular}

20501

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


529 
\end{center}


530 
\end{figure}


531 


532 
Since the basic representation of terms already accounts for @{text


533 
"\<alpha>"}conversion, Pure equality essentially acts like @{text


534 
"\<alpha>\<beta>\<eta>"}equivalence on terms, while coinciding with biimplication.

20498

535 


536 

20501

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


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


539 
simultaneous statements behind the scenes  framework conjunction


540 
is usually not exposed to the user.

20498

541 

20501

542 
\begin{figure}[htb]


543 
\begin{center}


544 
\begin{tabular}{ll}


545 
@{text "& :: prop \<Rightarrow> prop \<Rightarrow> prop"} & conjunction (hidden) \\


546 
@{text "\<turnstile> A & B \<equiv> (\<And>C. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)"} \\


547 
\end{tabular}


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


549 
\end{center}


550 
\end{figure}


551 


552 
The definition allows to derive the usual introduction @{text "\<turnstile> A \<Longrightarrow>


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


554 
\<Longrightarrow> B"}.

20491

555 
*}

18537

556 

20480

557 

20491

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

18537

559 


560 
text {*


561 


562 
FIXME


563 

20491

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


565 
separate calculus for rule composition, which is modeled after


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


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


568 


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


570 
Lowlevel inferences are occasional required internally, but the


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


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


573 
important to maintain this invariant in addon applications!


574 


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


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


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

20519

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

20491

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


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


581 
rule calculus.


582 


583 
Rules are treated modulo general higherorder unification, which is


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


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


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


587 


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


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


590 
practice not to contract or expand unnecessarily. Some mechanisms


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


592 
danger to produce some oscillation!


593 


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


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


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


597 

18537

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


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


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


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


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


603 
quantifier prefix is represented via \seeglossary{schematic


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


605 
\seeglossary{Horn Clause}}.


606 


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


608 

20498

609 


610 
\[


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


612 
{@{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})}}


613 
\]


614 


615 


616 
\[


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


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


619 
\]


620 


621 


622 
\[


623 
\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"}}


624 
\]


625 
\[


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


627 
\]


628 


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


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


631 


632 
\[


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


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


635 
{\begin{tabular}{l}


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


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


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


639 
\end{tabular}}


640 
\]


641 


642 


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

18537

644 
*}


645 

20498

646 

18537

647 
end
