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>

20494

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

20494

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

20480

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


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


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


129 
@{index_ML Sign.add_tyabbrs_i: "


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


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


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


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


134 
\end{mldecls}


135 


136 
\begin{description}


137 


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


139 
@{ML_type string}.


140 


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


142 
@{ML_type "class list"}.

20451

143 

20480

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

20494

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

20480

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


147 


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


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


150 

20494

151 
\item @{ML fold_atyps}~@{text "f \<tau>"} iterates function @{text "f"}


152 
over all occurrences of atoms (@{ML TFree} or @{ML TVar}) of @{text


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


154 

20480

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


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


157 


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

20491

159 
is of a given sort.

20480

160 

20494

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


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

20480

163 
optional mixfix syntax.

20451

164 

20494

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


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

20491

167 
optional mixfix syntax.

20480

168 


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

20494

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


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

20480

172 


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


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


175 
c\<^isub>2"}.


176 

20494

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


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

20480

179 


180 
\end{description}

20437

181 
*}


182 


183 

20480

184 

20451

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

18537

186 


187 
text {*

20451

188 
\glossary{Term}{FIXME}

18537

189 

20491

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

20514

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


192 
and constants. Terms with loose bound variables are usually


193 
considered malformed. The types of variables and constants is


194 
stored explicitly at each occurrence in the term.


195 


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


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


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


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


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


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


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


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


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


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


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


207 
different numbers at different occurrences.


208 


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


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


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


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


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

20491

214 

20514

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


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


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


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


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


220 


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


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


223 
presented in canonical order (according to the lefttoright


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


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


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


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


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


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

20480

230 

20514

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


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


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


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


235 
polymorphic constants that the userlevel typechecker would reject.

20480

236 

20514

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


238 
variables and constants, with abstraction and application as


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


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


241 
care of converting between an external representation with named


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


243 
instead of internal deBruijn representation.

20498

244 

20514

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


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


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

20498

248 
\[

20501

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

20498

250 
\qquad

20501

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


252 
\qquad


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

20498

254 
\]

20514

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

20498

256 

20514

257 
Typing information can be omitted: typeinference is able to


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


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


260 
Typeinference depends on a context of type constraints for fixed


261 
variables, and declarations for polymorphic constants.


262 


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


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


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


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


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


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


269 
commonplace, this rarely happens for variables: typeinference


270 
always demands ``consistent'' type constraints.


271 


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


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


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


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


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


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


278 
slightly pathological situation is apt to cause strange effects.


279 


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


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


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


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


284 
entering the logical core. Abbreviations are usually reverted when


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


286 
higherorder term rewrite system.

18537

287 
*}


288 

20514

289 
text %mlref {*


290 
\begin{mldecls}


291 
@{index_ML_type term} \\


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


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


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


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


296 
\end{mldecls}

18537

297 

20514

298 
\begin{description}

18537

299 

20514

300 
\item @{ML_type term} FIXME

18537

301 

20514

302 
\end{description}

18537

303 
*}


304 


305 

20451

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

18537

307 


308 
text {*

20501

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


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


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


312 
a clear distinction. Propositions are structured via implication


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


314 
anything else is considered atomic. The canonical form for


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

20480

316 

20501

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


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


319 
rarely spelled out explicitly. Theorems are usually normalized


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

20480

321 

20501

322 
\glossary{Fact}{Sometimes used interchangably for


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


324 
essentially an extralogical conjunction. Facts emerge either as


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


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

18537

327 

20501

328 
\glossary{Schematic variable}{FIXME}


329 


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


331 
proof context; an arbitrarybutfixed entity within a portion of


332 
proof text. FIXME}

18537

333 

20501

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


335 
variable}. FIXME}


336 


337 
\glossary{Bound variable}{FIXME}

18537

338 

20501

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


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


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


342 
different variables is their binding scope. FIXME}

18537

343 

20501

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


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


346 
basic theory:

18537

347 

20501

348 
\smallskip


349 
\begin{tabular}{ll}


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


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


352 
\end{tabular}

18537

353 

20501

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


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


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


357 
inductively by the primitive inferences given in


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


359 
that the hypotheses may not contain schematic variables.

18537

360 

20501

361 
\begin{figure}[htb]


362 
\begin{center}

20498

363 
\[


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


365 
\qquad


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


367 
\]


368 
\[


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


370 
\qquad


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


372 
\]


373 
\[


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


375 
\qquad


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


377 
\]

20501

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


379 
\end{center}


380 
\end{figure}

18537

381 

20501

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


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


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


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


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


387 
nondependent one.

20491

388 

20501

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


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


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


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


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


394 
hypothetical terms.


395 


396 
The corresponding proof terms are left implicit in the classic


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


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


399 
option to control the generation of full proof terms.


400 


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


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

20514

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

20501

404 
substitution through derivations inductively, we get admissible


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


406 


407 
\begin{figure}[htb]


408 
\begin{center}

20498

409 
\[

20501

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


411 
\quad


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

20498

413 
\]


414 
\[

20501

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


416 
\quad


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

20498

418 
\]

20501

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


420 
\end{center}


421 
\end{figure}

18537

422 

20498

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


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

20501

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


426 
true polymorphism in the logic.

20498

427 

20501

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


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


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


431 
this could disrupt monotonicity of the basic calculus: derivations


432 
could leave the current proof context.

20498

433 

20501

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


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


436 
although the implementation provides derived rules directly:


437 


438 
\begin{figure}[htb]


439 
\begin{center}

20498

440 
\begin{tabular}{ll}


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

20501

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

20498

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


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


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


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


447 
\end{tabular}

20501

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


449 
\end{center}


450 
\end{figure}


451 


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


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


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

20498

455 


456 

20501

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


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


459 
simultaneous statements behind the scenes  framework conjunction


460 
is usually not exposed to the user.

20498

461 

20501

462 
\begin{figure}[htb]


463 
\begin{center}


464 
\begin{tabular}{ll}


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


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


467 
\end{tabular}


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


469 
\end{center}


470 
\end{figure}


471 


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


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


474 
\<Longrightarrow> B"}.

20491

475 
*}

18537

476 

20480

477 

20491

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

18537

479 


480 
text {*


481 


482 
FIXME


483 

20491

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


485 
separate calculus for rule composition, which is modeled after


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


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


488 


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


490 
Lowlevel inferences are occasional required internally, but the


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


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


493 
important to maintain this invariant in addon applications!


494 


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


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


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


498 
combined in the variants of @{text "elimresosultion"} and @{text


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


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


501 
rule calculus.


502 


503 
Rules are treated modulo general higherorder unification, which is


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


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


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


507 


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


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


510 
practice not to contract or expand unnecessarily. Some mechanisms


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


512 
danger to produce some oscillation!


513 


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


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


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


517 

18537

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


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


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


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


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


523 
quantifier prefix is represented via \seeglossary{schematic


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


525 
\seeglossary{Horn Clause}}.


526 


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


528 

20498

529 


530 
\[


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


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


533 
\]


534 


535 


536 
\[


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


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


539 
\]


540 


541 


542 
\[


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


544 
\]


545 
\[


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


547 
\]


548 


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


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


551 


552 
\[


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


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


555 
{\begin{tabular}{l}


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


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


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


559 
\end{tabular}}


560 
\]


561 


562 


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

18537

564 
*}


565 

20498

566 

18537

567 
end
