summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

doc-src/IsarImplementation/Thy/logic.thy

author | wenzelm |

Fri Sep 08 17:33:05 2006 +0200 (2006-09-08) | |

changeset 20493 | 48fea5e99505 |

parent 20491 | 98ba42f19995 |

child 20494 | 99ad217b6974 |

permissions | -rw-r--r-- |

tuned;

2 (* $Id$ *)

4 theory logic imports base begin

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

8 text {*

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

10 which has been introduced as a natural-deduction framework in

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

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

13 \cite{Barendregt-Geuvers:2001}, although there are some key

14 differences in the specific treatment of simple types in

15 Isabelle/Pure.

17 Following type-theoretic 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).

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

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

29 *}

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

34 text {*

35 The language of types is an uninterpreted order-sorted first-order

36 algebra; types are qualified by ordered type classes.

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

41 generating relation; the transitive closure is maintained

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

43 transitive, and antisymmetric.

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

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.

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

59 (starting with a @{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),

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

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

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.

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

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

73 usually written postfix as @{text "(FIXME)\<kappa>"}. For @{text "k = 0"}

74 the argument tuple is omitted, e.g.\ @{text "prop"} instead of

75 @{text "()prop"}. For @{text "k = 1"} the parentheses are omitted,

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

77 notation is provided for specific constructors, notably

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

79 \<beta>)fun"} constructor.

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

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

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

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

86 arbitrary type expression of the theory. Type abbreviations looks

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

88 core logic encounters them.

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

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

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

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

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

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

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

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

99 which means that type arities are consistent with the subclass

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

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

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

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

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

106 The key property of a coregular order-sorted algebra is that sort

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

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

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

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

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

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

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

114 equivalence of sorts). Moreover, the usual type-inference algorithm

115 will produce primary types as expected \cite{nipkow-prehofer}.

116 *}

118 text %mlref {*

119 \begin{mldecls}

120 @{index_ML_type class} \\

121 @{index_ML_type sort} \\

122 @{index_ML_type typ} \\

123 @{index_ML_type arity} \\

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

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

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

127 @{index_ML Sign.add_tyabbrs_i: "

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

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

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

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

132 \end{mldecls}

134 \begin{description}

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

137 @{ML_type string}.

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

140 @{ML_type "class list"}.

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

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

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

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

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

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

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

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

153 is of a given sort.

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

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

157 optional mixfix syntax.

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

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

161 optional mixfix syntax.

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

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

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

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

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

169 c\<^isub>2"}.

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

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

174 \end{description}

175 *}

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

181 text {*

182 \glossary{Term}{FIXME}

184 The language of terms is that of simply-typed @{text "\<lambda>"}-calculus

185 with de-Bruijn indices for bound variables, and named free

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

187 usually considered malformed. The types of variables and constants

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

189 known performance issue).

191 FIXME de-Bruijn representation of lambda terms

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

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

195 thanks to type-inference.

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

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

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

200 *}

203 text {*

205 FIXME

207 \glossary{Schematic polymorphism}{FIXME}

209 \glossary{Type variable}{FIXME}

211 *}

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

216 text {*

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

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

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

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

222 corresponding proof terms are left implicit in the classic

223 ``LCF-approach'', although they could be exploited separately

224 \cite{Berghofer-Nipkow:2000}.

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

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

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

229 assumptions and conclusions emerging uniformly as simultaneous

230 statements.

234 FIXME

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

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

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

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

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

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

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

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

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

246 rarely spelled out explicitly. Theorems are usually normalized

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

249 \glossary{Fact}{Sometimes used interchangably for

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

251 essentially an extra-logical conjunction. Facts emerge either as

252 local assumptions, or as results of local goal statements --- both may

253 be simultaneous, hence the list representation.}

255 \glossary{Schematic variable}{FIXME}

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

258 proof context; an arbitrary-but-fixed entity within a portion of proof

259 text.}

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

263 \glossary{Bound variable}{FIXME}

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

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

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

268 variables is their binding scope.}

270 *}

273 section {* Proof terms *}

275 text {*

276 FIXME !?

277 *}

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

282 text {*

284 FIXME

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

287 separate calculus for rule composition, which is modeled after

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

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

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

292 Low-level inferences are occasional required internally, but the

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

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

295 important to maintain this invariant in add-on applications!

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

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

299 "by-assumption"} (i.e.\ closing a branch); both principles are

300 combined in the variants of @{text "elim-resosultion"} and @{text

301 "dest-resolution"}. Raw @{text "composition"} is occasionally

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

303 rule calculus.

305 Rules are treated modulo general higher-order unification, which is

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

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

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

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

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

312 practice not to contract or expand unnecessarily. Some mechanisms

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

314 danger to produce some oscillation!

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

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

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

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

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

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

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

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

325 quantifier prefix is represented via \seeglossary{schematic

326 variables}, such that the top-level structure is merely that of a

327 \seeglossary{Horn Clause}}.

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

331 *}

333 end