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 


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

20491

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

20494

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

20451

84 

20494

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


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


191 
with deBruijn indices for bound variables, and named free


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


193 
usually considered malformed. The types of variables and constants


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


195 
known performance issue).


196 

20451

197 
FIXME deBruijn representation of lambda terms

20480

198 


199 
Term syntax provides explicit abstraction @{text "\<lambda>x :: \<alpha>. b(x)"}


200 
and application @{text "t u"}, while types are usually implicit


201 
thanks to typeinference.


202 


203 
Terms of type @{text "prop"} are called


204 
propositions. Logical statements are composed via @{text "\<And>x ::


205 
\<alpha>. B(x)"} and @{text "A \<Longrightarrow> B"}.

18537

206 
*}


207 


208 


209 
text {*


210 


211 
FIXME


212 


213 
\glossary{Schematic polymorphism}{FIXME}


214 


215 
\glossary{Type variable}{FIXME}


216 


217 
*}


218 


219 

20451

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

18537

221 


222 
text {*


223 

20480

224 
Primitive reasoning operates on judgments of the form @{text "\<Gamma> \<turnstile>


225 
\<phi>"}, with standard introduction and elimination rules for @{text


226 
"\<And>"} and @{text "\<Longrightarrow>"} that refer to fixed parameters @{text "x"} and


227 
hypotheses @{text "A"} from the context @{text "\<Gamma>"}. The


228 
corresponding proof terms are left implicit in the classic


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


230 
\cite{BerghoferNipkow:2000}.


231 


232 
The framework also provides definitional equality @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha>


233 
\<Rightarrow> prop"}, with @{text "\<alpha>\<beta>\<eta>"}conversion rules. The internal


234 
conjunction @{text "& :: prop \<Rightarrow> prop \<Rightarrow> prop"} enables the view of


235 
assumptions and conclusions emerging uniformly as simultaneous


236 
statements.


237 


238 


239 

18537

240 
FIXME


241 


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


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


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


245 
clear distinction. Propositions are structured via implication @{text


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


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


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


249 


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


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


252 
rarely spelled out explicitly. Theorems are usually normalized


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


254 


255 
\glossary{Fact}{Sometimes used interchangably for


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


257 
essentially an extralogical conjunction. Facts emerge either as


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


259 
be simultaneous, hence the list representation.}


260 


261 
\glossary{Schematic variable}{FIXME}


262 


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


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


265 
text.}


266 


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


268 


269 
\glossary{Bound variable}{FIXME}


270 


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


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


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


274 
variables is their binding scope.}


275 


276 
*}


277 

20491

278 


279 
section {* Proof terms *}

18537

280 

20491

281 
text {*


282 
FIXME !?


283 
*}

18537

284 

20480

285 

20491

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

18537

287 


288 
text {*


289 


290 
FIXME


291 

20491

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


293 
separate calculus for rule composition, which is modeled after


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


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


296 


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


298 
Lowlevel inferences are occasional required internally, but the


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


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


301 
important to maintain this invariant in addon applications!


302 


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


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


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


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


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


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


309 
rule calculus.


310 


311 
Rules are treated modulo general higherorder unification, which is


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


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


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


315 


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


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


318 
practice not to contract or expand unnecessarily. Some mechanisms


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


320 
danger to produce some oscillation!


321 


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


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


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


325 

18537

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


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


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


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


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


331 
quantifier prefix is represented via \seeglossary{schematic


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


333 
\seeglossary{Horn Clause}}.


334 


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


336 


337 
*}


338 


339 
end
