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


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


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

20480

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


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

20491

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


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


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


69 
to produce anything like this.

20451

70 

20491

71 
A \emph{type constructor} is a @{text "k"}ary operator on types


72 
declared in the theory. Type constructor application is usually


73 
written postfix. For @{text "k = 0"} the argument tuple is omitted,


74 
e.g.\ @{text "prop"} instead of @{text "()prop"}. For @{text "k =


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


76 
@{text "(\<alpha>)list"}. Further notation is provided for specific


77 
constructors, notably rightassociative infix @{text "\<alpha> \<Rightarrow> \<beta>"}


78 
instead of @{text "(\<alpha>, \<beta>)fun"} constructor.

20480

79 


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

20491

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


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

20451

83 

20480

84 
A \emph{type abbreviation} is a syntactic abbreviation of an


85 
arbitrary type expression of the theory. Type abbreviations looks


86 
like type constructors at the surface, but are expanded before the


87 
core logic encounters them.


88 


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


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

20491

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

20480

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

20491

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


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


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


96 


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


98 
which means that type arities are consistent with the subclass


99 
relation: for each type constructor @{text "c"} and classes @{text


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

20480

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


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


103 
\<^vec>s\<^isub>2"} holds pointwise for all argument sorts.

20451

104 

20491

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

20480

106 
constraints may be always fulfilled in a most general fashion: for


107 
each type constructor @{text "c"} and sort @{text "s"} there is a


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

20491

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


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


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


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


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


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

20480

115 
*}

20451

116 

20480

117 
text %mlref {*


118 
\begin{mldecls}


119 
@{index_ML_type class} \\


120 
@{index_ML_type sort} \\


121 
@{index_ML_type typ} \\


122 
@{index_ML_type arity} \\


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


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


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


126 
@{index_ML Sign.add_tyabbrs_i: "


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


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


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


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


131 
\end{mldecls}


132 


133 
\begin{description}


134 


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


136 
@{ML_type string}.


137 


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


139 
@{ML_type "class list"}.

20451

140 

20480

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


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


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


144 


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


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


147 


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


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


150 


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

20491

152 
is of a given sort.

20480

153 


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

20491

155 
type constructors @{text "c"} with @{text "k"} arguments and

20480

156 
optional mixfix syntax.

20451

157 

20480

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

20491

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


160 
optional mixfix syntax.

20480

161 


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


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

20491

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

20480

165 


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


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


168 
c\<^isub>2"}.


169 


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


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


172 


173 
\end{description}

20437

174 
*}


175 


176 

20480

177 

20451

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

18537

179 


180 
text {*

20451

181 
\glossary{Term}{FIXME}

18537

182 

20491

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


184 
with deBruijn indices for bound variables, and named free


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


186 
usually considered malformed. The types of variables and constants


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


188 
known performance issue).


189 

20451

190 
FIXME deBruijn representation of lambda terms

20480

191 


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


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


194 
thanks to typeinference.


195 


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


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


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

18537

199 
*}


200 


201 


202 
text {*


203 


204 
FIXME


205 


206 
\glossary{Schematic polymorphism}{FIXME}


207 


208 
\glossary{Type variable}{FIXME}


209 


210 
*}


211 


212 

20451

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

18537

214 


215 
text {*


216 

20480

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


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


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


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


221 
corresponding proof terms are left implicit in the classic


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


223 
\cite{BerghoferNipkow:2000}.


224 


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


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


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


228 
assumptions and conclusions emerging uniformly as simultaneous


229 
statements.


230 


231 


232 

18537

233 
FIXME


234 


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


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


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


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


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


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


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


242 


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


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


245 
rarely spelled out explicitly. Theorems are usually normalized


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


247 


248 
\glossary{Fact}{Sometimes used interchangably for


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


250 
essentially an extralogical conjunction. Facts emerge either as


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


252 
be simultaneous, hence the list representation.}


253 


254 
\glossary{Schematic variable}{FIXME}


255 


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


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


258 
text.}


259 


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


261 


262 
\glossary{Bound variable}{FIXME}


263 


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


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


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


267 
variables is their binding scope.}


268 


269 
*}


270 

20491

271 


272 
section {* Proof terms *}

18537

273 

20491

274 
text {*


275 
FIXME !?


276 
*}

18537

277 

20480

278 

20491

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

18537

280 


281 
text {*


282 


283 
FIXME


284 

20491

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


286 
separate calculus for rule composition, which is modeled after


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


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


289 


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


291 
Lowlevel inferences are occasional required internally, but the


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


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


294 
important to maintain this invariant in addon applications!


295 


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


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


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


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


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


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


302 
rule calculus.


303 


304 
Rules are treated modulo general higherorder unification, which is


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


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


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


308 


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


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


311 
practice not to contract or expand unnecessarily. Some mechanisms


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


313 
danger to produce some oscillation!


314 


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


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


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


318 

18537

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


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


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


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


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


324 
quantifier prefix is represented via \seeglossary{schematic


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


326 
\seeglossary{Horn Clause}}.


327 


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


329 


330 
*}


331 


332 
end
