author  wenzelm 
Wed, 13 Oct 2010 13:05:23 +0100  
changeset 39846  cb6634eb8926 
parent 39840  3eb0694e6fcb 
child 39861  b8d89db3e238 
permissions  rwrr 
29755  1 
theory Logic 
2 
imports Base 

3 
begin 

18537  4 

20470  5 
chapter {* Primitive logic \label{ch:logic} *} 
18537  6 

20480  7 
text {* 
8 
The logical foundations of Isabelle/Isar are that of the Pure logic, 

29774  9 
which has been introduced as a Natural Deduction framework in 
20480  10 
\cite{paulson700}. This is essentially the same logic as ``@{text 
20493  11 
"\<lambda>HOL"}'' in the more abstract setting of Pure Type Systems (PTS) 
20480  12 
\cite{BarendregtGeuvers:2001}, although there are some key 
20491  13 
differences in the specific treatment of simple types in 
14 
Isabelle/Pure. 

20480  15 

16 
Following typetheoretic parlance, the Pure logic consists of three 

20543  17 
levels of @{text "\<lambda>"}calculus with corresponding arrows, @{text 
20480  18 
"\<Rightarrow>"} for syntactic function space (terms depending on terms), @{text 
19 
"\<And>"} for universal quantification (proofs depending on terms), and 

20 
@{text "\<Longrightarrow>"} for implication (proofs depending on proofs). 

21 

20537  22 
Derivations are relative to a logical theory, which declares type 
23 
constructors, constants, and axioms. Theory declarations support 

24 
schematic polymorphism, which is strictly speaking outside the 

25 
logic.\footnote{This is the deeper logical reason, why the theory 

26 
context @{text "\<Theta>"} is separate from the proof context @{text "\<Gamma>"} 

34929  27 
of the core calculus: type constructors, term constants, and facts 
28 
(proof constants) may involve arbitrary type schemes, but the type 

29 
of a locally fixed term parameter is also fixed!} 

20480  30 
*} 
31 

32 

20451  33 
section {* Types \label{sec:types} *} 
20437  34 

35 
text {* 

20480  36 
The language of types is an uninterpreted ordersorted firstorder 
37 
algebra; types are qualified by ordered type classes. 

38 

39 
\medskip A \emph{type class} is an abstract syntactic entity 

40 
declared in the theory context. The \emph{subclass relation} @{text 

41 
"c\<^isub>1 \<subseteq> c\<^isub>2"} is specified by stating an acyclic 

20491  42 
generating relation; the transitive closure is maintained 
43 
internally. The resulting relation is an ordering: reflexive, 

44 
transitive, and antisymmetric. 

20451  45 

34929  46 
A \emph{sort} is a list of type classes written as @{text "s = {c\<^isub>1, 
47 
\<dots>, c\<^isub>m}"}, it represents symbolic intersection. Notationally, the 

48 
curly braces are omitted for singleton intersections, i.e.\ any 

49 
class @{text "c"} may be read as a sort @{text "{c}"}. The ordering 

50 
on type classes is extended to sorts according to the meaning of 

51 
intersections: @{text "{c\<^isub>1, \<dots> c\<^isub>m} \<subseteq> {d\<^isub>1, \<dots>, d\<^isub>n}"} iff @{text 

52 
"\<forall>j. \<exists>i. c\<^isub>i \<subseteq> d\<^isub>j"}. The empty intersection @{text "{}"} refers to 

53 
the universal sort, which is the largest element wrt.\ the sort 

54 
order. Thus @{text "{}"} represents the ``full sort'', not the 

55 
empty one! The intersection of all (finitely many) classes declared 

56 
in the current theory is the least element wrt.\ the sort ordering. 

20480  57 

20491  58 
\medskip A \emph{fixed type variable} is a pair of a basic name 
20537  59 
(starting with a @{text "'"} character) and a sort constraint, e.g.\ 
60 
@{text "('a, s)"} which is usually printed as @{text "\<alpha>\<^isub>s"}. 

61 
A \emph{schematic type variable} is a pair of an indexname and a 

62 
sort constraint, e.g.\ @{text "(('a, 0), s)"} which is usually 

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

20451  64 

20480  65 
Note that \emph{all} syntactic components contribute to the identity 
34929  66 
of type variables: basic name, index, and sort constraint. The core 
67 
logic handles type variables with the same name but different sorts 

68 
as different, although the typeinference layer (which is outside 

69 
the core) rejects anything like that. 

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 

20537  73 
written postfix as @{text "(\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>k)\<kappa>"}. For 
74 
@{text "k = 0"} the argument tuple is omitted, e.g.\ @{text "prop"} 

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

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

77 
Further notation is provided for specific constructors, notably the 

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

79 
\<beta>)fun"}. 

20480  80 

34929  81 
The logical category \emph{type} is defined inductively over type 
82 
variables and type constructors as follows: @{text "\<tau> = \<alpha>\<^isub>s  ?\<alpha>\<^isub>s  

20543  83 
(\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)\<kappa>"}. 
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 
20537  87 
variables @{text "\<^vec>\<alpha>"}. Type abbreviations appear as type 
88 
constructors in the syntax, but are expanded before entering the 

89 
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 

20537  101 
relation: for any type constructor @{text "\<kappa>"}, and classes @{text 
102 
"c\<^isub>1 \<subseteq> c\<^isub>2"}, and arities @{text "\<kappa> :: 

103 
(\<^vec>s\<^isub>1)c\<^isub>1"} and @{text "\<kappa> :: 

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

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

20451  106 

20491  107 
The key property of a coregular ordersorted algebra is that sort 
20537  108 
constraints can be solved in a most general fashion: for each type 
109 
constructor @{text "\<kappa>"} and sort @{text "s"} there is a most general 

110 
vector of argument sorts @{text "(s\<^isub>1, \<dots>, s\<^isub>k)"} such 

111 
that a type scheme @{text "(\<alpha>\<^bsub>s\<^isub>1\<^esub>, \<dots>, 

112 
\<alpha>\<^bsub>s\<^isub>k\<^esub>)\<kappa>"} is of sort @{text "s"}. 

20543  113 
Consequently, type unification has most general solutions (modulo 
114 
equivalence of sorts), so typeinference produces primary types as 

115 
expected \cite{nipkowprehofer}. 

20480  116 
*} 
20451  117 

20480  118 
text %mlref {* 
119 
\begin{mldecls} 

34921  120 
@{index_ML_type class: string} \\ 
121 
@{index_ML_type sort: "class list"} \\ 

122 
@{index_ML_type arity: "string * sort list * sort"} \\ 

20480  123 
@{index_ML_type typ} \\ 
39846  124 
@{index_ML Term.map_atyps: "(typ > typ) > typ > typ"} \\ 
125 
@{index_ML Term.fold_atyps: "(typ > 'a > 'a) > typ > 'a > 'a"} \\ 

20547  126 
\end{mldecls} 
127 
\begin{mldecls} 

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

30355  130 
@{index_ML Sign.add_types: "(binding * int * mixfix) list > theory > theory"} \\ 
36345  131 
@{index_ML Sign.add_type_abbrev: "binding * string list * typ > theory > theory"} \\ 
30355  132 
@{index_ML Sign.primitive_class: "binding * class list > theory > theory"} \\ 
20480  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 

34921  139 
\item @{ML_type class} represents type classes. 
20480  140 

34921  141 
\item @{ML_type sort} represents sorts, i.e.\ finite intersections 
142 
of classes. The empty list @{ML "[]: sort"} refers to the empty 

143 
class intersection, i.e.\ the ``full sort''. 

20451  144 

34921  145 
\item @{ML_type arity} represents type arities. A triple @{text 
146 
"(\<kappa>, \<^vec>s, s) : arity"} represents @{text "\<kappa> :: (\<^vec>s)s"} as 

147 
described above. 

20480  148 

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

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

151 

39846  152 
\item @{ML Term.map_atyps}~@{text "f \<tau>"} applies the mapping @{text 
153 
"f"} to all atomic types (@{ML TFree}, @{ML TVar}) occurring in 

154 
@{text "\<tau>"}. 

20519  155 

39846  156 
\item @{ML Term.fold_atyps}~@{text "f \<tau>"} iterates the operation 
157 
@{text "f"} over all occurrences of atomic types (@{ML TFree}, @{ML 

158 
TVar}) in @{text "\<tau>"}; the type structure is traversed from left to 

159 
right. 

20494  160 

20480  161 
\item @{ML Sign.subsort}~@{text "thy (s\<^isub>1, s\<^isub>2)"} 
162 
tests the subsort relation @{text "s\<^isub>1 \<subseteq> s\<^isub>2"}. 

163 

20537  164 
\item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether type 
165 
@{text "\<tau>"} is of sort @{text "s"}. 

20480  166 

20537  167 
\item @{ML Sign.add_types}~@{text "[(\<kappa>, k, mx), \<dots>]"} declares a new 
20494  168 
type constructors @{text "\<kappa>"} with @{text "k"} arguments and 
20480  169 
optional mixfix syntax. 
20451  170 

36345  171 
\item @{ML Sign.add_type_abbrev}~@{text "(\<kappa>, \<^vec>\<alpha>, 
172 
\<tau>)"} defines a new type abbreviation @{text 

173 
"(\<^vec>\<alpha>)\<kappa> = \<tau>"}. 

20480  174 

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

20537  176 
c\<^isub>n])"} declares a new class @{text "c"}, together with class 
20494  177 
relations @{text "c \<subseteq> c\<^isub>i"}, for @{text "i = 1, \<dots>, n"}. 
20480  178 

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

20543  180 
c\<^isub>2)"} declares the class relation @{text "c\<^isub>1 \<subseteq> 
20480  181 
c\<^isub>2"}. 
182 

20494  183 
\item @{ML Sign.primitive_arity}~@{text "(\<kappa>, \<^vec>s, s)"} declares 
20537  184 
the arity @{text "\<kappa> :: (\<^vec>s)s"}. 
20480  185 

186 
\end{description} 

20437  187 
*} 
188 

39832  189 
text %mlantiq {* 
190 
\begin{matharray}{rcl} 

191 
@{ML_antiquotation_def "class"} & : & @{text ML_antiquotation} \\ 

192 
@{ML_antiquotation_def "sort"} & : & @{text ML_antiquotation} \\ 

193 
@{ML_antiquotation_def "type_name"} & : & @{text ML_antiquotation} \\ 

194 
@{ML_antiquotation_def "type_abbrev"} & : & @{text ML_antiquotation} \\ 

195 
@{ML_antiquotation_def "nonterminal"} & : & @{text ML_antiquotation} \\ 

196 
@{ML_antiquotation_def "typ"} & : & @{text ML_antiquotation} \\ 

197 
\end{matharray} 

198 

199 
\begin{rail} 

200 
'class' nameref 

201 
; 

202 
'sort' sort 

203 
; 

204 
('type\_name'  'type\_abbrev'  'nonterminal') nameref 

205 
; 

206 
'typ' type 

207 
; 

208 
\end{rail} 

209 

210 
\begin{description} 

211 

212 
\item @{text "@{class c}"} inlines the internalized class @{text 

213 
"c"}  as @{ML_type string} literal. 

214 

215 
\item @{text "@{sort s}"} inlines the internalized sort @{text "s"} 

216 
 as @{ML_type "string list"} literal. 

217 

218 
\item @{text "@{type_name c}"} inlines the internalized type 

219 
constructor @{text "c"}  as @{ML_type string} literal. 

220 

221 
\item @{text "@{type_abbrev c}"} inlines the internalized type 

222 
abbreviation @{text "c"}  as @{ML_type string} literal. 

223 

224 
\item @{text "@{nonterminal c}"} inlines the internalized syntactic 

225 
type~/ grammar nonterminal @{text "c"}  as @{ML_type string} 

226 
literal. 

227 

228 
\item @{text "@{typ \<tau>}"} inlines the internalized type @{text "\<tau>"} 

229 
 as constructor term for datatype @{ML_type typ}. 

230 

231 
\end{description} 

232 
*} 

233 

20437  234 

20451  235 
section {* Terms \label{sec:terms} *} 
18537  236 

237 
text {* 

20491  238 
The language of terms is that of simplytyped @{text "\<lambda>"}calculus 
20520  239 
with deBruijn indices for bound variables (cf.\ \cite{debruijn72} 
29761  240 
or \cite{paulsonml2}), with the types being determined by the 
241 
corresponding binders. In contrast, free variables and constants 

34929  242 
have an explicit name and type in each occurrence. 
20514  243 

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

20537  245 
which accounts for the number of intermediate binders between the 
246 
variable occurrence in the body and its binding position. For 

34929  247 
example, the deBruijn term @{text "\<lambda>\<^bsub>bool\<^esub>. \<lambda>\<^bsub>bool\<^esub>. 1 \<and> 0"} would 
248 
correspond to @{text "\<lambda>x\<^bsub>bool\<^esub>. \<lambda>y\<^bsub>bool\<^esub>. x \<and> y"} in a named 

20543  249 
representation. Note that a bound variable may be represented by 
250 
different deBruijn indices at different occurrences, depending on 

251 
the nesting of abstractions. 

20537  252 

20543  253 
A \emph{loose variable} is a bound variable that is outside the 
20537  254 
scope of local binders. The types (and names) for loose variables 
20543  255 
can be managed as a separate context, that is maintained as a stack 
256 
of hypothetical binders. The core logic operates on closed terms, 

257 
without any loose variables. 

20514  258 

20537  259 
A \emph{fixed variable} is a pair of a basic name and a type, e.g.\ 
34929  260 
@{text "(x, \<tau>)"} which is usually printed @{text "x\<^isub>\<tau>"} here. A 
20537  261 
\emph{schematic variable} is a pair of an indexname and a type, 
34929  262 
e.g.\ @{text "((x, 0), \<tau>)"} which is likewise printed as @{text 
20537  263 
"?x\<^isub>\<tau>"}. 
20491  264 

20537  265 
\medskip A \emph{constant} is a pair of a basic name and a type, 
34929  266 
e.g.\ @{text "(c, \<tau>)"} which is usually printed as @{text "c\<^isub>\<tau>"} 
267 
here. Constants are declared in the context as polymorphic families 

268 
@{text "c :: \<sigma>"}, meaning that all substitution instances @{text 

269 
"c\<^isub>\<tau>"} for @{text "\<tau> = \<sigma>\<vartheta>"} are valid. 

20514  270 

34929  271 
The vector of \emph{type arguments} of constant @{text "c\<^isub>\<tau>"} wrt.\ 
272 
the declaration @{text "c :: \<sigma>"} is defined as the codomain of the 

273 
matcher @{text "\<vartheta> = {?\<alpha>\<^isub>1 \<mapsto> \<tau>\<^isub>1, \<dots>, ?\<alpha>\<^isub>n \<mapsto> \<tau>\<^isub>n}"} presented in 

274 
canonical order @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n)"}, corresponding to the 

275 
lefttoright occurrences of the @{text "\<alpha>\<^isub>i"} in @{text "\<sigma>"}. 

276 
Within a given theory context, there is a onetoone correspondence 

277 
between any constant @{text "c\<^isub>\<tau>"} and the application @{text "c(\<tau>\<^isub>1, 

278 
\<dots>, \<tau>\<^isub>n)"} of its type arguments. For example, with @{text "plus :: \<alpha> 

279 
\<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"}, the instance @{text "plus\<^bsub>nat \<Rightarrow> nat \<Rightarrow> nat\<^esub>"} corresponds to 

280 
@{text "plus(nat)"}. 

20480  281 

20514  282 
Constant declarations @{text "c :: \<sigma>"} may contain sort constraints 
283 
for type variables in @{text "\<sigma>"}. These are observed by 

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

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

20537  286 
polymorphic constants that the userlevel typechecker would reject 
287 
due to violation of type class restrictions. 

20480  288 

34929  289 
\medskip An \emph{atomic} term is either a variable or constant. 
290 
The logical category \emph{term} is defined inductively over atomic 

291 
terms, with abstraction and application as follows: @{text "t = b  

292 
x\<^isub>\<tau>  ?x\<^isub>\<tau>  c\<^isub>\<tau>  \<lambda>\<^isub>\<tau>. t  t\<^isub>1 t\<^isub>2"}. Parsing and printing takes care of 

293 
converting between an external representation with named bound 

294 
variables. Subsequently, we shall use the latter notation instead 

295 
of internal deBruijn representation. 

20498  296 

20537  297 
The inductive relation @{text "t :: \<tau>"} assigns a (unique) type to a 
298 
term according to the structure of atomic terms, abstractions, and 

299 
applicatins: 

20498  300 
\[ 
20501  301 
\infer{@{text "a\<^isub>\<tau> :: \<tau>"}}{} 
20498  302 
\qquad 
20501  303 
\infer{@{text "(\<lambda>x\<^sub>\<tau>. t) :: \<tau> \<Rightarrow> \<sigma>"}}{@{text "t :: \<sigma>"}} 
304 
\qquad 

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

20498  306 
\] 
20514  307 
A \emph{welltyped term} is a term that can be typed according to these rules. 
20498  308 

20514  309 
Typing information can be omitted: typeinference is able to 
310 
reconstruct the most general type of a raw term, while assigning 

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

312 
Typeinference depends on a context of type constraints for fixed 

313 
variables, and declarations for polymorphic constants. 

314 

20537  315 
The identity of atomic terms consists both of the name and the type 
316 
component. This means that different variables @{text 

34929  317 
"x\<^bsub>\<tau>\<^isub>1\<^esub>"} and @{text "x\<^bsub>\<tau>\<^isub>2\<^esub>"} may become the same after 
318 
type instantiation. Typeinference rejects variables of the same 

319 
name, but different types. In contrast, mixed instances of 

320 
polymorphic constants occur routinely. 

20514  321 

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

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

34929  324 
its type @{text "\<sigma>"}. This means that the term implicitly depends 
325 
on type arguments that are not accounted in the result type, i.e.\ 

326 
there are different type instances @{text "t\<vartheta> :: \<sigma>"} and 

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

20543  328 
pathological situation notoriously demands additional care. 
20514  329 

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

20537  331 
"c\<^isub>\<sigma> \<equiv> t"} of a closed term @{text "t"} of type @{text "\<sigma>"}, 
332 
without any hidden polymorphism. A term abbreviation looks like a 

20543  333 
constant in the syntax, but is expanded before entering the logical 
334 
core. Abbreviations are usually reverted when printing terms, using 

335 
@{text "t \<rightarrow> c\<^isub>\<sigma>"} as rules for higherorder rewriting. 

20519  336 

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

20537  338 
"\<alpha>\<beta>\<eta>"}conversion: @{text "\<alpha>"}conversion refers to capturefree 
20519  339 
renaming of bound variables; @{text "\<beta>"}conversion contracts an 
20537  340 
abstraction applied to an argument term, substituting the argument 
20519  341 
in the body: @{text "(\<lambda>x. b)a"} becomes @{text "b[a/x]"}; @{text 
342 
"\<eta>"}conversion contracts vacuous applicationabstraction: @{text 

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

20537  344 
does not occur in @{text "f"}. 
20519  345 

20537  346 
Terms are normally treated modulo @{text "\<alpha>"}conversion, which is 
347 
implicit in the deBruijn representation. Names for bound variables 

348 
in abstractions are maintained separately as (meaningless) comments, 

349 
mostly for parsing and printing. Full @{text "\<alpha>\<beta>\<eta>"}conversion is 

28784  350 
commonplace in various standard operations (\secref{sec:objrules}) 
351 
that are based on higherorder unification and matching. 

18537  352 
*} 
353 

20514  354 
text %mlref {* 
355 
\begin{mldecls} 

356 
@{index_ML_type term} \\ 

20519  357 
@{index_ML "op aconv": "term * term > bool"} \\ 
39846  358 
@{index_ML Term.map_types: "(typ > typ) > term > term"} \\ 
359 
@{index_ML Term.fold_types: "(typ > 'a > 'a) > term > 'a > 'a"} \\ 

360 
@{index_ML Term.map_aterms: "(term > term) > term > term"} \\ 

361 
@{index_ML Term.fold_aterms: "(term > 'a > 'a) > term > 'a > 'a"} \\ 

20547  362 
\end{mldecls} 
363 
\begin{mldecls} 

20514  364 
@{index_ML fastype_of: "term > typ"} \\ 
20519  365 
@{index_ML lambda: "term > term > term"} \\ 
366 
@{index_ML betapply: "term * term > term"} \\ 

33174  367 
@{index_ML Sign.declare_const: "(binding * typ) * mixfix > 
24972
acafb18a47dc
replaced Sign.add_consts_i by Sign.declare_const;
wenzelm
parents:
24828
diff
changeset

368 
theory > term * theory"} \\ 
33174  369 
@{index_ML Sign.add_abbrev: "string > binding * term > 
24972
acafb18a47dc
replaced Sign.add_consts_i by Sign.declare_const;
wenzelm
parents:
24828
diff
changeset

370 
theory > (term * term) * theory"} \\ 
20519  371 
@{index_ML Sign.const_typargs: "theory > string * typ > typ list"} \\ 
372 
@{index_ML Sign.const_instance: "theory > string * typ list > typ"} \\ 

20514  373 
\end{mldecls} 
18537  374 

20514  375 
\begin{description} 
18537  376 

20537  377 
\item @{ML_type term} represents deBruijn terms, with comments in 
378 
abstractions, and explicitly named free variables and constants; 

379 
this is a datatype with constructors @{ML Bound}, @{ML Free}, @{ML 

380 
Var}, @{ML Const}, @{ML Abs}, @{ML "op $"}. 

20519  381 

36166  382 
\item @{text "t"}~@{ML_text aconv}~@{text "u"} checks @{text 
20519  383 
"\<alpha>"}equivalence of two terms. This is the basic equality relation 
384 
on type @{ML_type term}; raw datatype equality should only be used 

385 
for operations related to parsing or printing! 

386 

39846  387 
\item @{ML Term.map_types}~@{text "f t"} applies the mapping @{text 
20537  388 
"f"} to all types occurring in @{text "t"}. 
389 

39846  390 
\item @{ML Term.fold_types}~@{text "f t"} iterates the operation 
391 
@{text "f"} over all occurrences of types in @{text "t"}; the term 

20537  392 
structure is traversed from left to right. 
20519  393 

39846  394 
\item @{ML Term.map_aterms}~@{text "f t"} applies the mapping @{text 
395 
"f"} to all atomic terms (@{ML Bound}, @{ML Free}, @{ML Var}, @{ML 

20537  396 
Const}) occurring in @{text "t"}. 
397 

39846  398 
\item @{ML Term.fold_aterms}~@{text "f t"} iterates the operation 
399 
@{text "f"} over all occurrences of atomic terms (@{ML Bound}, @{ML 

400 
Free}, @{ML Var}, @{ML Const}) in @{text "t"}; the term structure is 

20519  401 
traversed from left to right. 
402 

20537  403 
\item @{ML fastype_of}~@{text "t"} determines the type of a 
404 
welltyped term. This operation is relatively slow, despite the 

405 
omission of any sanity checks. 

20519  406 

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

20537  408 
"\<lambda>a. b"}, where occurrences of the atomic term @{text "a"} in the 
409 
body @{text "b"} are replaced by bound variables. 

20519  410 

20537  411 
\item @{ML betapply}~@{text "(t, u)"} produces an application @{text 
412 
"t u"}, with topmost @{text "\<beta>"}conversion if @{text "t"} is an 

413 
abstraction. 

20519  414 

33174  415 
\item @{ML Sign.declare_const}~@{text "((c, \<sigma>), mx)"} 
24972
acafb18a47dc
replaced Sign.add_consts_i by Sign.declare_const;
wenzelm
parents:
24828
diff
changeset

416 
declares a new constant @{text "c :: \<sigma>"} with optional mixfix 
acafb18a47dc
replaced Sign.add_consts_i by Sign.declare_const;
wenzelm
parents:
24828
diff
changeset

417 
syntax. 
20519  418 

33174  419 
\item @{ML Sign.add_abbrev}~@{text "print_mode (c, t)"} 
21827  420 
introduces a new term abbreviation @{text "c \<equiv> t"}. 
20519  421 

20520  422 
\item @{ML Sign.const_typargs}~@{text "thy (c, \<tau>)"} and @{ML 
423 
Sign.const_instance}~@{text "thy (c, [\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n])"} 

20543  424 
convert between two representations of polymorphic constants: full 
425 
type instance vs.\ compact type arguments form. 

18537  426 

20514  427 
\end{description} 
18537  428 
*} 
429 

39832  430 
text %mlantiq {* 
431 
\begin{matharray}{rcl} 

432 
@{ML_antiquotation_def "const_name"} & : & @{text ML_antiquotation} \\ 

433 
@{ML_antiquotation_def "const_abbrev"} & : & @{text ML_antiquotation} \\ 

434 
@{ML_antiquotation_def "const"} & : & @{text ML_antiquotation} \\ 

435 
@{ML_antiquotation_def "term"} & : & @{text ML_antiquotation} \\ 

436 
@{ML_antiquotation_def "prop"} & : & @{text ML_antiquotation} \\ 

437 
\end{matharray} 

438 

439 
\begin{rail} 

440 
('const\_name'  'const\_abbrev') nameref 

441 
; 

442 
'const' ('(' (type + ',') ')')? 

443 
; 

444 
'term' term 

445 
; 

446 
'prop' prop 

447 
; 

448 
\end{rail} 

449 

450 
\begin{description} 

451 

452 
\item @{text "@{const_name c}"} inlines the internalized logical 

453 
constant name @{text "c"}  as @{ML_type string} literal. 

454 

455 
\item @{text "@{const_abbrev c}"} inlines the internalized 

456 
abbreviated constant name @{text "c"}  as @{ML_type string} 

457 
literal. 

458 

459 
\item @{text "@{const c(\<^vec>\<tau>)}"} inlines the internalized 

460 
constant @{text "c"} with precise type instantiation in the sense of 

461 
@{ML Sign.const_instance}  as @{ML Const} constructor term for 

462 
datatype @{ML_type term}. 

463 

464 
\item @{text "@{term t}"} inlines the internalized term @{text "t"} 

465 
 as constructor term for datatype @{ML_type term}. 

466 

467 
\item @{text "@{prop \<phi>}"} inlines the internalized proposition 

468 
@{text "\<phi>"}  as constructor term for datatype @{ML_type term}. 

469 

470 
\end{description} 

471 
*} 

472 

18537  473 

20451  474 
section {* Theorems \label{sec:thms} *} 
18537  475 

476 
text {* 

20543  477 
A \emph{proposition} is a welltyped term of type @{text "prop"}, a 
20521  478 
\emph{theorem} is a proven proposition (depending on a context of 
479 
hypotheses and the background theory). Primitive inferences include 

29774  480 
plain Natural Deduction rules for the primary connectives @{text 
20537  481 
"\<And>"} and @{text "\<Longrightarrow>"} of the framework. There is also a builtin 
482 
notion of equality/equivalence @{text "\<equiv>"}. 

20521  483 
*} 
484 

29758  485 

26872  486 
subsection {* Primitive connectives and rules \label{sec:primrules} *} 
18537  487 

20521  488 
text {* 
20543  489 
The theory @{text "Pure"} contains constant declarations for the 
490 
primitive connectives @{text "\<And>"}, @{text "\<Longrightarrow>"}, and @{text "\<equiv>"} of 

491 
the logical framework, see \figref{fig:pureconnectives}. The 

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

493 
defined inductively by the primitive inferences given in 

494 
\figref{fig:primrules}, with the global restriction that the 

495 
hypotheses must \emph{not} contain any schematic variables. The 

496 
builtin equality is conceptually axiomatized as shown in 

20521  497 
\figref{fig:pureequality}, although the implementation works 
20543  498 
directly with derived inferences. 
20521  499 

500 
\begin{figure}[htb] 

501 
\begin{center} 

20501  502 
\begin{tabular}{ll} 
503 
@{text "all :: (\<alpha> \<Rightarrow> prop) \<Rightarrow> prop"} & universal quantification (binder @{text "\<And>"}) \\ 

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

20521  505 
@{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop"} & equality relation (infix) \\ 
20501  506 
\end{tabular} 
20537  507 
\caption{Primitive connectives of Pure}\label{fig:pureconnectives} 
20521  508 
\end{center} 
509 
\end{figure} 

18537  510 

20501  511 
\begin{figure}[htb] 
512 
\begin{center} 

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

515 
\qquad 

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

517 
\] 

518 
\[ 

34929  519 
\infer[@{text "(\<And>\<dash>intro)"}]{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}}{@{text "\<Gamma> \<turnstile> b[x]"} & @{text "x \<notin> \<Gamma>"}} 
20498  520 
\qquad 
34929  521 
\infer[@{text "(\<And>\<dash>elim)"}]{@{text "\<Gamma> \<turnstile> b[a]"}}{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}} 
20498  522 
\] 
523 
\[ 

34929  524 
\infer[@{text "(\<Longrightarrow>\<dash>intro)"}]{@{text "\<Gamma>  A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}} 
20498  525 
\qquad 
34929  526 
\infer[@{text "(\<Longrightarrow>\<dash>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"}} 
20498  527 
\] 
20521  528 
\caption{Primitive inferences of Pure}\label{fig:primrules} 
529 
\end{center} 

530 
\end{figure} 

531 

532 
\begin{figure}[htb] 

533 
\begin{center} 

534 
\begin{tabular}{ll} 

20537  535 
@{text "\<turnstile> (\<lambda>x. b[x]) a \<equiv> b[a]"} & @{text "\<beta>"}conversion \\ 
20521  536 
@{text "\<turnstile> x \<equiv> x"} & reflexivity \\ 
537 
@{text "\<turnstile> x \<equiv> y \<Longrightarrow> P x \<Longrightarrow> P y"} & substitution \\ 

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

20537  539 
@{text "\<turnstile> (A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<equiv> B"} & logical equivalence \\ 
20521  540 
\end{tabular} 
20542  541 
\caption{Conceptual axiomatization of Pure equality}\label{fig:pureequality} 
20501  542 
\end{center} 
543 
\end{figure} 

18537  544 

20501  545 
The introduction and elimination rules for @{text "\<And>"} and @{text 
20537  546 
"\<Longrightarrow>"} are analogous to formation of dependently typed @{text 
20501  547 
"\<lambda>"}terms representing the underlying proof objects. Proof terms 
20543  548 
are irrelevant in the Pure logic, though; they cannot occur within 
549 
propositions. The system provides a runtime option to record 

20537  550 
explicit proof terms for primitive inferences. Thus all three 
551 
levels of @{text "\<lambda>"}calculus become explicit: @{text "\<Rightarrow>"} for 

552 
terms, and @{text "\<And>/\<Longrightarrow>"} for proofs (cf.\ 

553 
\cite{BerghoferNipkow:2000:TPHOL}). 

20491  554 

34929  555 
Observe that locally fixed parameters (as in @{text 
556 
"\<And>\<dash>intro"}) need not be recorded in the hypotheses, because 

557 
the simple syntactic types of Pure are always inhabitable. 

558 
``Assumptions'' @{text "x :: \<tau>"} for typemembership are only 

559 
present as long as some @{text "x\<^isub>\<tau>"} occurs in the statement 

560 
body.\footnote{This is the key difference to ``@{text "\<lambda>HOL"}'' in 

561 
the PTS framework \cite{BarendregtGeuvers:2001}, where hypotheses 

562 
@{text "x : A"} are treated uniformly for propositions and types.} 

20501  563 

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

20537  565 
forming all instances of type and term variables: @{text "\<turnstile> 
566 
A\<vartheta>"} holds for any substitution instance of an axiom 

20543  567 
@{text "\<turnstile> A"}. By pushing substitutions through derivations 
568 
inductively, we also get admissible @{text "generalize"} and @{text 

34929  569 
"instantiate"} rules as shown in \figref{fig:substrules}. 
20501  570 

571 
\begin{figure}[htb] 

572 
\begin{center} 

20498  573 
\[ 
20501  574 
\infer{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}{@{text "\<Gamma> \<turnstile> B[\<alpha>]"} & @{text "\<alpha> \<notin> \<Gamma>"}} 
575 
\quad 

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

20498  577 
\] 
578 
\[ 

20501  579 
\infer{@{text "\<Gamma> \<turnstile> B[\<tau>]"}}{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}} 
580 
\quad 

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

20498  582 
\] 
20501  583 
\caption{Admissible substitution rules}\label{fig:substrules} 
584 
\end{center} 

585 
\end{figure} 

18537  586 

20537  587 
Note that @{text "instantiate"} does not require an explicit 
588 
sidecondition, because @{text "\<Gamma>"} may never contain schematic 

589 
variables. 

590 

591 
In principle, variables could be substituted in hypotheses as well, 

20543  592 
but this would disrupt the monotonicity of reasoning: deriving 
593 
@{text "\<Gamma>\<vartheta> \<turnstile> B\<vartheta>"} from @{text "\<Gamma> \<turnstile> B"} is 

594 
correct, but @{text "\<Gamma>\<vartheta> \<supseteq> \<Gamma>"} does not necessarily hold: 

595 
the result belongs to a different proof context. 

20542  596 

20543  597 
\medskip An \emph{oracle} is a function that produces axioms on the 
598 
fly. Logically, this is an instance of the @{text "axiom"} rule 

599 
(\figref{fig:primrules}), but there is an operational difference. 

600 
The system always records oracle invocations within derivations of 

29768  601 
theorems by a unique tag. 
20542  602 

603 
Axiomatizations should be limited to the bare minimum, typically as 

604 
part of the initial logical basis of an objectlogic formalization. 

20543  605 
Later on, theories are usually developed in a strictly definitional 
606 
fashion, by stating only certain equalities over new constants. 

20542  607 

608 
A \emph{simple definition} consists of a constant declaration @{text 

20543  609 
"c :: \<sigma>"} together with an axiom @{text "\<turnstile> c \<equiv> t"}, where @{text "t 
610 
:: \<sigma>"} is a closed term without any hidden polymorphism. The RHS 

611 
may depend on further defined constants, but not @{text "c"} itself. 

612 
Definitions of functions may be presented as @{text "c \<^vec>x \<equiv> 

613 
t"} instead of the puristic @{text "c \<equiv> \<lambda>\<^vec>x. t"}. 

20542  614 

20543  615 
An \emph{overloaded definition} consists of a collection of axioms 
616 
for the same constant, with zero or one equations @{text 

617 
"c((\<^vec>\<alpha>)\<kappa>) \<equiv> t"} for each type constructor @{text "\<kappa>"} (for 

618 
distinct variables @{text "\<^vec>\<alpha>"}). The RHS may mention 

619 
previously defined constants as above, or arbitrary constants @{text 

620 
"d(\<alpha>\<^isub>i)"} for some @{text "\<alpha>\<^isub>i"} projected from @{text 

621 
"\<^vec>\<alpha>"}. Thus overloaded definitions essentially work by 

622 
primitive recursion over the syntactic structure of a single type 

39840  623 
argument. See also \cite[\S4.3]{HaftmannWenzel:2006:classes}. 
20521  624 
*} 
20498  625 

20521  626 
text %mlref {* 
627 
\begin{mldecls} 

628 
@{index_ML_type ctyp} \\ 

629 
@{index_ML_type cterm} \\ 

20547  630 
@{index_ML Thm.ctyp_of: "theory > typ > ctyp"} \\ 
631 
@{index_ML Thm.cterm_of: "theory > term > cterm"} \\ 

632 
\end{mldecls} 

633 
\begin{mldecls} 

20521  634 
@{index_ML_type thm} \\ 
32833  635 
@{index_ML proofs: "int Unsynchronized.ref"} \\ 
20542  636 
@{index_ML Thm.assume: "cterm > thm"} \\ 
637 
@{index_ML Thm.forall_intr: "cterm > thm > thm"} \\ 

638 
@{index_ML Thm.forall_elim: "cterm > thm > thm"} \\ 

639 
@{index_ML Thm.implies_intr: "cterm > thm > thm"} \\ 

640 
@{index_ML Thm.implies_elim: "thm > thm > thm"} \\ 

641 
@{index_ML Thm.generalize: "string list * string list > int > thm > thm"} \\ 

642 
@{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list > thm > thm"} \\ 

36134  643 
@{index_ML Thm.add_axiom: "binding * term > theory > (string * thm) * theory"} \\ 
39821  644 
@{index_ML Thm.add_oracle: "binding * ('a > cterm) > theory > 
645 
(string * ('a > thm)) * theory"} \\ 

646 
@{index_ML Thm.add_def: "bool > bool > binding * term > theory > 

647 
(string * thm) * theory"} \\ 

20547  648 
\end{mldecls} 
649 
\begin{mldecls} 

39821  650 
@{index_ML Theory.add_deps: "string > string * typ > (string * typ) list > 
651 
theory > theory"} \\ 

20521  652 
\end{mldecls} 
653 

654 
\begin{description} 

655 

20542  656 
\item @{ML_type ctyp} and @{ML_type cterm} represent certified types 
657 
and terms, respectively. These are abstract datatypes that 

658 
guarantee that its values have passed the full wellformedness (and 

659 
welltypedness) checks, relative to the declarations of type 

660 
constructors, constants etc. in the theory. 

661 

29768  662 
\item @{ML Thm.ctyp_of}~@{text "thy \<tau>"} and @{ML 
663 
Thm.cterm_of}~@{text "thy t"} explicitly checks types and terms, 

664 
respectively. This also involves some basic normalizations, such 

665 
expansion of type and term abbreviations from the theory context. 

20547  666 

667 
Recertification is relatively slow and should be avoided in tight 

668 
reasoning loops. There are separate operations to decompose 

669 
certified entities (including actual theorems). 

20542  670 

671 
\item @{ML_type thm} represents proven propositions. This is an 

672 
abstract datatype that guarantees that its values have been 

673 
constructed by basic principles of the @{ML_struct Thm} module. 

39281  674 
Every @{ML_type thm} value contains a sliding backreference to the 
20543  675 
enclosing theory, cf.\ \secref{sec:contexttheory}. 
20542  676 

34929  677 
\item @{ML proofs} specifies the detail of proof recording within 
29768  678 
@{ML_type thm} values: @{ML 0} records only the names of oracles, 
679 
@{ML 1} records oracle names and propositions, @{ML 2} additionally 

680 
records full proof terms. Officially named theorems that contribute 

34929  681 
to a result are recorded in any case. 
20542  682 

683 
\item @{ML Thm.assume}, @{ML Thm.forall_intr}, @{ML 

684 
Thm.forall_elim}, @{ML Thm.implies_intr}, and @{ML Thm.implies_elim} 

685 
correspond to the primitive inferences of \figref{fig:primrules}. 

686 

687 
\item @{ML Thm.generalize}~@{text "(\<^vec>\<alpha>, \<^vec>x)"} 

688 
corresponds to the @{text "generalize"} rules of 

20543  689 
\figref{fig:substrules}. Here collections of type and term 
690 
variables are generalized simultaneously, specified by the given 

691 
basic names. 

20521  692 

20542  693 
\item @{ML Thm.instantiate}~@{text "(\<^vec>\<alpha>\<^isub>s, 
694 
\<^vec>x\<^isub>\<tau>)"} corresponds to the @{text "instantiate"} rules 

695 
of \figref{fig:substrules}. Type variables are substituted before 

696 
term variables. Note that the types in @{text "\<^vec>x\<^isub>\<tau>"} 

697 
refer to the instantiated versions. 

698 

35927  699 
\item @{ML Thm.add_axiom}~@{text "(name, A) thy"} declares an 
700 
arbitrary proposition as axiom, and retrieves it as a theorem from 

701 
the resulting theory, cf.\ @{text "axiom"} in 

702 
\figref{fig:primrules}. Note that the lowlevel representation in 

703 
the axiom table may differ slightly from the returned theorem. 

20542  704 

30288
a32700e45ab3
Thm.add_oracle interface: replaced old bstring by binding;
wenzelm
parents:
30272
diff
changeset

705 
\item @{ML Thm.add_oracle}~@{text "(binding, oracle)"} produces a named 
28290  706 
oracle rule, essentially generating arbitrary axioms on the fly, 
707 
cf.\ @{text "axiom"} in \figref{fig:primrules}. 

20521  708 

35927  709 
\item @{ML Thm.add_def}~@{text "unchecked overloaded (name, c 
710 
\<^vec>x \<equiv> t)"} states a definitional axiom for an existing constant 

711 
@{text "c"}. Dependencies are recorded via @{ML Theory.add_deps}, 

712 
unless the @{text "unchecked"} option is set. Note that the 

713 
lowlevel representation in the axiom table may differ slightly from 

714 
the returned theorem. 

20542  715 

716 
\item @{ML Theory.add_deps}~@{text "name c\<^isub>\<tau> 

20543  717 
\<^vec>d\<^isub>\<sigma>"} declares dependencies of a named specification 
718 
for constant @{text "c\<^isub>\<tau>"}, relative to existing 

719 
specifications for constants @{text "\<^vec>d\<^isub>\<sigma>"}. 

20542  720 

20521  721 
\end{description} 
722 
*} 

723 

724 

39832  725 
text %mlantiq {* 
726 
\begin{matharray}{rcl} 

727 
@{ML_antiquotation_def "ctyp"} & : & @{text ML_antiquotation} \\ 

728 
@{ML_antiquotation_def "cterm"} & : & @{text ML_antiquotation} \\ 

729 
@{ML_antiquotation_def "cprop"} & : & @{text ML_antiquotation} \\ 

730 
@{ML_antiquotation_def "thm"} & : & @{text ML_antiquotation} \\ 

731 
@{ML_antiquotation_def "thms"} & : & @{text ML_antiquotation} \\ 

732 
@{ML_antiquotation_def "lemma"} & : & @{text ML_antiquotation} \\ 

733 
\end{matharray} 

734 

735 
\begin{rail} 

736 
'ctyp' typ 

737 
; 

738 
'cterm' term 

739 
; 

740 
'cprop' prop 

741 
; 

742 
'thm' thmref 

743 
; 

744 
'thms' thmrefs 

745 
; 

746 
'lemma' ('(open)')? ((prop +) + 'and') \\ 'by' method method? 

747 
\end{rail} 

748 

749 
\begin{description} 

750 

751 
\item @{text "@{ctyp \<tau>}"} produces a certified type wrt.\ the 

752 
current background theory  as abstract value of type @{ML_type 

753 
ctyp}. 

754 

755 
\item @{text "@{cterm t}"} and @{text "@{cprop \<phi>}"} produce a 

756 
certified term wrt.\ the current background theory  as abstract 

757 
value of type @{ML_type cterm}. 

758 

759 
\item @{text "@{thm a}"} produces a singleton fact  as abstract 

760 
value of type @{ML_type thm}. 

761 

762 
\item @{text "@{thms a}"} produces a general fact  as abstract 

763 
value of type @{ML_type "thm list"}. 

764 

765 
\item @{text "@{lemma \<phi> by meth}"} produces a fact that is proven on 

766 
the spot according to the minimal proof, which imitates a terminal 

767 
Isar proof. The result is an abstract value of type @{ML_type thm} 

768 
or @{ML_type "thm list"}, depending on the number of propositions 

769 
given here. 

770 

771 
The internal derivation object lacks a proper theorem name, but it 

772 
is formally closed, unless the @{text "(open)"} option is specified 

773 
(this may impact performance of applications with proof terms). 

774 

775 
Since ML antiquotations are always evaluated at compiletime, there 

776 
is no runtime overhead even for nontrivial proofs. Nonetheless, 

777 
the justification is syntactically limited to a single @{command 

778 
"by"} step. More complex Isar proofs should be done in regular 

779 
theory source, before compiling the corresponding ML text that uses 

780 
the result. 

781 

782 
\end{description} 

783 

784 
*} 

785 

786 

20543  787 
subsection {* Auxiliary definitions *} 
20521  788 

789 
text {* 

20543  790 
Theory @{text "Pure"} provides a few auxiliary definitions, see 
791 
\figref{fig:pureaux}. These special constants are normally not 

792 
exposed to the user, but appear in internal encodings. 

20501  793 

794 
\begin{figure}[htb] 

795 
\begin{center} 

20498  796 
\begin{tabular}{ll} 
34929  797 
@{text "conjunction :: prop \<Rightarrow> prop \<Rightarrow> prop"} & (infix @{text "&&&"}) \\ 
798 
@{text "\<turnstile> A &&& B \<equiv> (\<And>C. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)"} \\[1ex] 

20543  799 
@{text "prop :: prop \<Rightarrow> prop"} & (prefix @{text "#"}, suppressed) \\ 
20521  800 
@{text "#A \<equiv> A"} \\[1ex] 
801 
@{text "term :: \<alpha> \<Rightarrow> prop"} & (prefix @{text "TERM"}) \\ 

802 
@{text "term x \<equiv> (\<And>A. A \<Longrightarrow> A)"} \\[1ex] 

803 
@{text "TYPE :: \<alpha> itself"} & (prefix @{text "TYPE"}) \\ 

804 
@{text "(unspecified)"} \\ 

20498  805 
\end{tabular} 
20521  806 
\caption{Definitions of auxiliary connectives}\label{fig:pureaux} 
20501  807 
\end{center} 
808 
\end{figure} 

809 

34929  810 
The introduction @{text "A \<Longrightarrow> B \<Longrightarrow> A &&& B"}, and eliminations 
811 
(projections) @{text "A &&& B \<Longrightarrow> A"} and @{text "A &&& B \<Longrightarrow> B"} are 

812 
available as derived rules. Conjunction allows to treat 

813 
simultaneous assumptions and conclusions uniformly, e.g.\ consider 

814 
@{text "A \<Longrightarrow> B \<Longrightarrow> C &&& D"}. In particular, the goal mechanism 

815 
represents multiple claims as explicit conjunction internally, but 

816 
this is refined (via backwards introduction) into separate subgoals 

817 
before the user commences the proof; the final result is projected 

818 
into a list of theorems using eliminations (cf.\ 

20537  819 
\secref{sec:tacticalgoals}). 
20498  820 

20537  821 
The @{text "prop"} marker (@{text "#"}) makes arbitrarily complex 
822 
propositions appear as atomic, without changing the meaning: @{text 

823 
"\<Gamma> \<turnstile> A"} and @{text "\<Gamma> \<turnstile> #A"} are interchangeable. See 

824 
\secref{sec:tacticalgoals} for specific operations. 

20521  825 

20543  826 
The @{text "term"} marker turns any welltyped term into a derivable 
827 
proposition: @{text "\<turnstile> TERM t"} holds unconditionally. Although 

828 
this is logically vacuous, it allows to treat terms and proofs 

829 
uniformly, similar to a typetheoretic framework. 

20498  830 

20537  831 
The @{text "TYPE"} constructor is the canonical representative of 
832 
the unspecified type @{text "\<alpha> itself"}; it essentially injects the 

833 
language of types into that of terms. There is specific notation 

834 
@{text "TYPE(\<tau>)"} for @{text "TYPE\<^bsub>\<tau> 

20521  835 
itself\<^esub>"}. 
34929  836 
Although being devoid of any particular meaning, the term @{text 
20537  837 
"TYPE(\<tau>)"} accounts for the type @{text "\<tau>"} within the term 
838 
language. In particular, @{text "TYPE(\<alpha>)"} may be used as formal 

839 
argument in primitive definitions, in order to circumvent hidden 

840 
polymorphism (cf.\ \secref{sec:terms}). For example, @{text "c 

841 
TYPE(\<alpha>) \<equiv> A[\<alpha>]"} defines @{text "c :: \<alpha> itself \<Rightarrow> prop"} in terms of 

842 
a proposition @{text "A"} that depends on an additional type 

843 
argument, which is essentially a predicate on types. 

20521  844 
*} 
20501  845 

20521  846 
text %mlref {* 
847 
\begin{mldecls} 

848 
@{index_ML Conjunction.intr: "thm > thm > thm"} \\ 

849 
@{index_ML Conjunction.elim: "thm > thm * thm"} \\ 

850 
@{index_ML Drule.mk_term: "cterm > thm"} \\ 

851 
@{index_ML Drule.dest_term: "thm > cterm"} \\ 

852 
@{index_ML Logic.mk_type: "typ > term"} \\ 

853 
@{index_ML Logic.dest_type: "term > typ"} \\ 

854 
\end{mldecls} 

855 

856 
\begin{description} 

857 

34929  858 
\item @{ML Conjunction.intr} derives @{text "A &&& B"} from @{text 
20542  859 
"A"} and @{text "B"}. 
860 

20543  861 
\item @{ML Conjunction.elim} derives @{text "A"} and @{text "B"} 
34929  862 
from @{text "A &&& B"}. 
20542  863 

20543  864 
\item @{ML Drule.mk_term} derives @{text "TERM t"}. 
20542  865 

20543  866 
\item @{ML Drule.dest_term} recovers term @{text "t"} from @{text 
867 
"TERM t"}. 

20542  868 

869 
\item @{ML Logic.mk_type}~@{text "\<tau>"} produces the term @{text 

870 
"TYPE(\<tau>)"}. 

871 

872 
\item @{ML Logic.dest_type}~@{text "TYPE(\<tau>)"} recovers the type 

873 
@{text "\<tau>"}. 

20521  874 

875 
\end{description} 

20491  876 
*} 
18537  877 

20480  878 

28784  879 
section {* Objectlevel rules \label{sec:objrules} *} 
18537  880 

29768  881 
text {* 
882 
The primitive inferences covered so far mostly serve foundational 

883 
purposes. Userlevel reasoning usually works via objectlevel rules 

884 
that are represented as theorems of Pure. Composition of rules 

29771  885 
involves \emph{backchaining}, \emph{higherorder unification} modulo 
886 
@{text "\<alpha>\<beta>\<eta>"}conversion of @{text "\<lambda>"}terms, and socalled 

887 
\emph{lifting} of rules into a context of @{text "\<And>"} and @{text 

29774  888 
"\<Longrightarrow>"} connectives. Thus the full power of higherorder Natural 
889 
Deduction in Isabelle/Pure becomes readily available. 

29769
03634a9e91ae
improved section on "Hereditary Harrop Formulae";
wenzelm
parents:
29768
diff
changeset

890 
*} 
20491  891 

29769
03634a9e91ae
improved section on "Hereditary Harrop Formulae";
wenzelm
parents:
29768
diff
changeset

892 

03634a9e91ae
improved section on "Hereditary Harrop Formulae";
wenzelm
parents:
29768
diff
changeset

893 
subsection {* Hereditary Harrop Formulae *} 
03634a9e91ae
improved section on "Hereditary Harrop Formulae";
wenzelm
parents:
29768
diff
changeset

894 

03634a9e91ae
improved section on "Hereditary Harrop Formulae";
wenzelm
parents:
29768
diff
changeset

895 
text {* 
29768  896 
The idea of objectlevel rules is to model Natural Deduction 
897 
inferences in the style of Gentzen \cite{Gentzen:1935}, but we allow 

898 
arbitrary nesting similar to \cite{extensions91}. The most basic 

899 
rule format is that of a \emph{Horn Clause}: 

900 
\[ 

901 
\infer{@{text "A"}}{@{text "A\<^sub>1"} & @{text "\<dots>"} & @{text "A\<^sub>n"}} 

902 
\] 

903 
where @{text "A, A\<^sub>1, \<dots>, A\<^sub>n"} are atomic propositions 

904 
of the framework, usually of the form @{text "Trueprop B"}, where 

905 
@{text "B"} is a (compound) objectlevel statement. This 

906 
objectlevel inference corresponds to an iterated implication in 

907 
Pure like this: 

908 
\[ 

909 
@{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> A"} 

910 
\] 

29769
03634a9e91ae
improved section on "Hereditary Harrop Formulae";
wenzelm
parents:
29768
diff
changeset

911 
As an example consider conjunction introduction: @{text "A \<Longrightarrow> B \<Longrightarrow> A \<and> 
03634a9e91ae
improved section on "Hereditary Harrop Formulae";
wenzelm
parents:
29768
diff
changeset

912 
B"}. Any parameters occurring in such rule statements are 
03634a9e91ae
improved section on "Hereditary Harrop Formulae";
wenzelm
parents:
29768
diff
changeset

913 
conceptionally treated as arbitrary: 
29768  914 
\[ 
29769
03634a9e91ae
improved section on "Hereditary Harrop Formulae";
wenzelm
parents:
29768
diff
changeset

915 
@{text "\<And>x\<^sub>1 \<dots> x\<^sub>m. A\<^sub>1 x\<^sub>1 \<dots> x\<^sub>m \<Longrightarrow> \<dots> A\<^sub>n x\<^sub>1 \<dots> x\<^sub>m \<Longrightarrow> A x\<^sub>1 \<dots> x\<^sub>m"} 
29768  916 
\] 
20491  917 

29769
03634a9e91ae
improved section on "Hereditary Harrop Formulae";
wenzelm
parents:
29768
diff
changeset

918 
Nesting of rules means that the positions of @{text "A\<^sub>i"} may 
29770  919 
again hold compound rules, not just atomic propositions. 
29769
03634a9e91ae
improved section on "Hereditary Harrop Formulae";
wenzelm
parents:
29768
diff
changeset

920 
Propositions of this format are called \emph{Hereditary Harrop 
03634a9e91ae
improved section on "Hereditary Harrop Formulae";
wenzelm
parents:
29768
diff
changeset

921 
Formulae} in the literature \cite{Miller:1991}. Here we give an 
03634a9e91ae
improved section on "Hereditary Harrop Formulae";
wenzelm
parents:
29768
diff
changeset

922 
inductive characterization as follows: 
29768  923 

924 
\medskip 

925 
\begin{tabular}{ll} 

926 
@{text "\<^bold>x"} & set of variables \\ 

927 
@{text "\<^bold>A"} & set of atomic propositions \\ 

928 
@{text "\<^bold>H = \<And>\<^bold>x\<^sup>*. \<^bold>H\<^sup>* \<Longrightarrow> \<^bold>A"} & set of Hereditary Harrop Formulas \\ 

929 
\end{tabular} 

930 
\medskip 

931 

29770  932 
\noindent Thus we essentially impose nesting levels on propositions 
933 
formed from @{text "\<And>"} and @{text "\<Longrightarrow>"}. At each level there is a 

934 
prefix of parameters and compound premises, concluding an atomic 

935 
proposition. Typical examples are @{text "\<longrightarrow>"}introduction @{text 

936 
"(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B"} or mathematical induction @{text "P 0 \<Longrightarrow> (\<And>n. P n 

937 
\<Longrightarrow> P (Suc n)) \<Longrightarrow> P n"}. Even deeper nesting occurs in wellfounded 

938 
induction @{text "(\<And>x. (\<And>y. y \<prec> x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P x"}, but this 

34929  939 
already marks the limit of rule complexity that is usually seen in 
940 
practice. 

29769
03634a9e91ae
improved section on "Hereditary Harrop Formulae";
wenzelm
parents:
29768
diff
changeset

941 

29770  942 
\medskip Regular userlevel inferences in Isabelle/Pure always 
943 
maintain the following canonical form of results: 

29769
03634a9e91ae
improved section on "Hereditary Harrop Formulae";
wenzelm
parents:
29768
diff
changeset

944 

03634a9e91ae
improved section on "Hereditary Harrop Formulae";
wenzelm
parents:
29768
diff
changeset

945 
\begin{itemize} 
29768  946 

29774  947 
\item Normalization by @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}, 
948 
which is a theorem of Pure, means that quantifiers are pushed in 

949 
front of implication at each level of nesting. The normal form is a 

950 
Hereditary Harrop Formula. 

29769
03634a9e91ae
improved section on "Hereditary Harrop Formulae";
wenzelm
parents:
29768
diff
changeset

951 

03634a9e91ae
improved section on "Hereditary Harrop Formulae";
wenzelm
parents:
29768
diff
changeset

952 
\item The outermost prefix of parameters is represented via 
29770  953 
schematic variables: instead of @{text "\<And>\<^vec>x. \<^vec>H \<^vec>x 
29774  954 
\<Longrightarrow> A \<^vec>x"} we have @{text "\<^vec>H ?\<^vec>x \<Longrightarrow> A ?\<^vec>x"}. 
955 
Note that this representation looses information about the order of 

956 
parameters, and vacuous quantifiers vanish automatically. 

29769
03634a9e91ae
improved section on "Hereditary Harrop Formulae";
wenzelm
parents:
29768
diff
changeset

957 

03634a9e91ae
improved section on "Hereditary Harrop Formulae";
wenzelm
parents:
29768
diff
changeset

958 
\end{itemize} 
03634a9e91ae
improved section on "Hereditary Harrop Formulae";
wenzelm
parents:
29768
diff
changeset

959 
*} 
03634a9e91ae
improved section on "Hereditary Harrop Formulae";
wenzelm
parents:
29768
diff
changeset

960 

29771  961 
text %mlref {* 
962 
\begin{mldecls} 

30552
58db56278478
provide Simplifier.norm_hhf(_protect) as regular simplifier operation;
wenzelm
parents:
30355
diff
changeset

963 
@{index_ML Simplifier.norm_hhf: "thm > thm"} \\ 
29771  964 
\end{mldecls} 
965 

966 
\begin{description} 

967 

30552
58db56278478
provide Simplifier.norm_hhf(_protect) as regular simplifier operation;
wenzelm
parents:
30355
diff
changeset

968 
\item @{ML Simplifier.norm_hhf}~@{text thm} normalizes the given 
29771  969 
theorem according to the canonical form specified above. This is 
970 
occasionally helpful to repair some lowlevel tools that do not 

971 
handle Hereditary Harrop Formulae properly. 

972 

973 
\end{description} 

974 
*} 

975 

29769
03634a9e91ae
improved section on "Hereditary Harrop Formulae";
wenzelm
parents:
29768
diff
changeset

976 

03634a9e91ae
improved section on "Hereditary Harrop Formulae";
wenzelm
parents:
29768
diff
changeset

977 
subsection {* Rule composition *} 
03634a9e91ae
improved section on "Hereditary Harrop Formulae";
wenzelm
parents:
29768
diff
changeset

978 

03634a9e91ae
improved section on "Hereditary Harrop Formulae";
wenzelm
parents:
29768
diff
changeset

979 
text {* 
29771  980 
The rule calculus of Isabelle/Pure provides two main inferences: 
981 
@{inference resolution} (i.e.\ backchaining of rules) and 

982 
@{inference assumption} (i.e.\ closing a branch), both modulo 

983 
higherorder unification. There are also combined variants, notably 

984 
@{inference elim_resolution} and @{inference dest_resolution}. 

20491  985 

29771  986 
To understand the allimportant @{inference resolution} principle, 
987 
we first consider raw @{inference_def composition} (modulo 

988 
higherorder unification with substitution @{text "\<vartheta>"}): 

20498  989 
\[ 
29771  990 
\infer[(@{inference_def composition})]{@{text "\<^vec>A\<vartheta> \<Longrightarrow> C\<vartheta>"}} 
20498  991 
{@{text "\<^vec>A \<Longrightarrow> B"} & @{text "B' \<Longrightarrow> C"} & @{text "B\<vartheta> = B'\<vartheta>"}} 
992 
\] 

29771  993 
Here the conclusion of the first rule is unified with the premise of 
994 
the second; the resulting rule instance inherits the premises of the 

995 
first and conclusion of the second. Note that @{text "C"} can again 

996 
consist of iterated implications. We can also permute the premises 

997 
of the second rule backandforth in order to compose with @{text 

998 
"B'"} in any position (subsequently we shall always refer to 

999 
position 1 w.l.o.g.). 

20498  1000 

29774  1001 
In @{inference composition} the internal structure of the common 
1002 
part @{text "B"} and @{text "B'"} is not taken into account. For 

1003 
proper @{inference resolution} we require @{text "B"} to be atomic, 

1004 
and explicitly observe the structure @{text "\<And>\<^vec>x. \<^vec>H 

1005 
\<^vec>x \<Longrightarrow> B' \<^vec>x"} of the premise of the second rule. The 

1006 
idea is to adapt the first rule by ``lifting'' it into this context, 

1007 
by means of iterated application of the following inferences: 

20498  1008 
\[ 
29771  1009 
\infer[(@{inference_def imp_lift})]{@{text "(\<^vec>H \<Longrightarrow> \<^vec>A) \<Longrightarrow> (\<^vec>H \<Longrightarrow> B)"}}{@{text "\<^vec>A \<Longrightarrow> B"}} 
20498  1010 
\] 
1011 
\[ 

29771  1012 
\infer[(@{inference_def all_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"}} 
20498  1013 
\] 
29771  1014 
By combining raw composition with lifting, we get full @{inference 
1015 
resolution} as follows: 

20498  1016 
\[ 
29771  1017 
\infer[(@{inference_def resolution})] 
20498  1018 
{@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>A (?\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>"}} 
1019 
{\begin{tabular}{l} 

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

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

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

1023 
\end{tabular}} 

1024 
\] 

1025 

29774  1026 
Continued resolution of rules allows to backchain a problem towards 
1027 
more and subproblems. Branches are closed either by resolving with 

1028 
a rule of 0 premises, or by producing a ``shortcircuit'' within a 

1029 
solved situation (again modulo unification): 

29771  1030 
\[ 
1031 
\infer[(@{inference_def assumption})]{@{text "C\<vartheta>"}} 

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

1033 
\] 

20498  1034 

29771  1035 
FIXME @{inference_def elim_resolution}, @{inference_def dest_resolution} 
18537  1036 
*} 
1037 

29768  1038 
text %mlref {* 
1039 
\begin{mldecls} 

1040 
@{index_ML "op RS": "thm * thm > thm"} \\ 

1041 
@{index_ML "op OF": "thm * thm list > thm"} \\ 

1042 
\end{mldecls} 

1043 

1044 
\begin{description} 

1045 

34929  1046 
\item @{text "rule\<^sub>1 RS rule\<^sub>2"} resolves @{text "rule\<^sub>1"} with @{text 
1047 
"rule\<^sub>2"} according to the @{inference resolution} principle 

1048 
explained above. Note that the corresponding rule attribute in the 

1049 
Isar language is called @{attribute THEN}. 

29768  1050 

29771  1051 
\item @{text "rule OF rules"} resolves a list of rules with the 
29774  1052 
first rule, addressing its premises @{text "1, \<dots>, length rules"} 
1053 
(operating from last to first). This means the newly emerging 

1054 
premises are all concatenated, without interfering. Also note that 

1055 
compared to @{text "RS"}, the rule argument order is swapped: @{text 

1056 
"rule\<^sub>1 RS rule\<^sub>2 = rule\<^sub>2 OF [rule\<^sub>1]"}. 

29768  1057 

1058 
\end{description} 

1059 
*} 

30272  1060 

18537  1061 
end 