author  wenzelm 
Thu, 11 Oct 2007 16:38:42 +0200  
changeset 24972  acafb18a47dc 
parent 24828  137c242e7277 
child 26872  336dfd860744 
permissions  rwrr 
18537  1 

2 
(* $Id$ *) 

3 

4 
theory logic imports base begin 

5 

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

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

10 
which has been introduced as a naturaldeduction framework in 

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

20493  12 
"\<lambda>HOL"}'' in the more abstract setting of Pure Type Systems (PTS) 
20480  13 
\cite{BarendregtGeuvers:2001}, although there are some key 
20491  14 
differences in the specific treatment of simple types in 
15 
Isabelle/Pure. 

20480  16 

17 
Following typetheoretic parlance, the Pure logic consists of three 

20543  18 
levels of @{text "\<lambda>"}calculus with corresponding arrows, @{text 
20480  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 

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

25 
schematic polymorphism, which is strictly speaking outside the 

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

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

28 
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 

20537  45 
A \emph{sort} is a list of type classes written as @{text "s = 
46 
{c\<^isub>1, \<dots>, c\<^isub>m}"}, which represents symbolic 

20480  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 
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 
20493  66 
of type variables, including the sort constraint. The core logic 
67 
handles type variables with the same name but different sorts as 

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

69 
produce anything like this. 

20451  70 

20493  71 
A \emph{type constructor} @{text "\<kappa>"} is a @{text "k"}ary operator 
72 
on types declared in the theory. Type constructor application is 

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 

20537  81 
A \emph{type} is defined inductively over type variables and type 
82 
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} 

120 
@{index_ML_type class} \\ 

121 
@{index_ML_type sort} \\ 

20494  122 
@{index_ML_type arity} \\ 
20480  123 
@{index_ML_type typ} \\ 
20519  124 
@{index_ML map_atyps: "(typ > typ) > typ > typ"} \\ 
20494  125 
@{index_ML 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"} \\ 

20520  130 
@{index_ML Sign.add_types: "(string * int * mixfix) list > theory > theory"} \\ 
20480  131 
@{index_ML Sign.add_tyabbrs_i: " 
20520  132 
(string * string list * typ * mixfix) list > theory > theory"} \\ 
20480  133 
@{index_ML Sign.primitive_class: "string * class list > theory > theory"} \\ 
134 
@{index_ML Sign.primitive_classrel: "class * class > theory > theory"} \\ 

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

136 
\end{mldecls} 

137 

138 
\begin{description} 

139 

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

141 
@{ML_type string}. 

142 

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

144 
@{ML_type "class list"}. 

20451  145 

20480  146 
\item @{ML_type arity} represents type arities; this is an alias for 
20494  147 
triples of the form @{text "(\<kappa>, \<^vec>s, s)"} for @{text "\<kappa> :: 
20480  148 
(\<^vec>s)s"} described above. 
149 

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

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

152 

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

155 
"\<tau>"}. 

20519  156 

20537  157 
\item @{ML fold_atyps}~@{text "f \<tau>"} iterates the operation @{text 
158 
"f"} over all occurrences of atomic types (@{ML TFree}, @{ML TVar}) 

159 
in @{text "\<tau>"}; the type structure is traversed from left to 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 

20494  171 
\item @{ML Sign.add_tyabbrs_i}~@{text "[(\<kappa>, \<^vec>\<alpha>, \<tau>, mx), \<dots>]"} 
172 
defines a new type abbreviation @{text "(\<^vec>\<alpha>)\<kappa> = \<tau>"} with 

20491  173 
optional mixfix syntax. 
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 

189 

20480  190 

20451  191 
section {* Terms \label{sec:terms} *} 
18537  192 

193 
text {* 

20451  194 
\glossary{Term}{FIXME} 
18537  195 

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

200 
constants are have an explicit name and type in each occurrence. 

20514  201 

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

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

20543  205 
example, the deBruijn term @{text 
206 
"\<lambda>\<^bsub>nat\<^esub>. \<lambda>\<^bsub>nat\<^esub>. 1 + 0"} would 

207 
correspond to @{text 

208 
"\<lambda>x\<^bsub>nat\<^esub>. \<lambda>y\<^bsub>nat\<^esub>. x + y"} in a named 

209 
representation. Note that a bound variable may be represented by 

210 
different deBruijn indices at different occurrences, depending on 

211 
the nesting of abstractions. 

20537  212 

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

217 
without any loose variables. 

20514  218 

20537  219 
A \emph{fixed variable} is a pair of a basic name and a type, e.g.\ 
220 
@{text "(x, \<tau>)"} which is usually printed @{text "x\<^isub>\<tau>"}. A 

221 
\emph{schematic variable} is a pair of an indexname and a type, 

222 
e.g.\ @{text "((x, 0), \<tau>)"} which is usually printed as @{text 

223 
"?x\<^isub>\<tau>"}. 

20491  224 

20537  225 
\medskip A \emph{constant} is a pair of a basic name and a type, 
226 
e.g.\ @{text "(c, \<tau>)"} which is usually printed as @{text 

227 
"c\<^isub>\<tau>"}. Constants are declared in the context as polymorphic 

20543  228 
families @{text "c :: \<sigma>"}, meaning that all substitution instances 
229 
@{text "c\<^isub>\<tau>"} for @{text "\<tau> = \<sigma>\<vartheta>"} are valid. 

20514  230 

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

233 
the matcher @{text "\<vartheta> = {?\<alpha>\<^isub>1 \<mapsto> \<tau>\<^isub>1, \<dots>, 

234 
?\<alpha>\<^isub>n \<mapsto> \<tau>\<^isub>n}"} presented in canonical order @{text 

235 
"(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n)"}. Within a given theory context, 

236 
there is a onetoone correspondence between any constant @{text 

237 
"c\<^isub>\<tau>"} and the application @{text "c(\<tau>\<^isub>1, \<dots>, 

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

239 
:: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"}, the instance @{text "plus\<^bsub>nat \<Rightarrow> nat \<Rightarrow> 

240 
nat\<^esub>"} corresponds to @{text "plus(nat)"}. 

20480  241 

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

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

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

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

20480  248 

20543  249 
\medskip An \emph{atomic} term is either a variable or constant. A 
250 
\emph{term} is defined inductively over atomic terms, with 

251 
abstraction and application as follows: @{text "t = b  x\<^isub>\<tau>  

252 
?x\<^isub>\<tau>  c\<^isub>\<tau>  \<lambda>\<^isub>\<tau>. t  t\<^isub>1 t\<^isub>2"}. 

253 
Parsing and printing takes care of converting between an external 

254 
representation with named bound variables. Subsequently, we shall 

255 
use the latter notation instead of internal deBruijn 

256 
representation. 

20498  257 

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

260 
applicatins: 

20498  261 
\[ 
20501  262 
\infer{@{text "a\<^isub>\<tau> :: \<tau>"}}{} 
20498  263 
\qquad 
20501  264 
\infer{@{text "(\<lambda>x\<^sub>\<tau>. t) :: \<tau> \<Rightarrow> \<sigma>"}}{@{text "t :: \<sigma>"}} 
265 
\qquad 

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

20498  267 
\] 
20514  268 
A \emph{welltyped term} is a term that can be typed according to these rules. 
20498  269 

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

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

273 
Typeinference depends on a context of type constraints for fixed 

274 
variables, and declarations for polymorphic constants. 

275 

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

278 
"x\<^bsub>\<tau>\<^isub>1\<^esub>"} and @{text 

279 
"x\<^bsub>\<tau>\<^isub>2\<^esub>"} may become the same after type 

280 
instantiation. Some outer layers of the system make it hard to 

281 
produce variables of the same name, but different types. In 

20543  282 
contrast, mixed instances of polymorphic constants occur frequently. 
20514  283 

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

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

20537  286 
@{text "\<sigma>"}. This means that the term implicitly depends on type 
20543  287 
arguments that are not accounted in the result type, i.e.\ there are 
20537  288 
different type instances @{text "t\<vartheta> :: \<sigma>"} and @{text 
289 
"t\<vartheta>' :: \<sigma>"} with the same type. This slightly 

20543  290 
pathological situation notoriously demands additional care. 
20514  291 

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

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

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

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

20519  298 

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

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

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

20537  306 
does not occur in @{text "f"}. 
20519  307 

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

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

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

20543  312 
commonplace in various standard operations (\secref{sec:rules}) that 
20537  313 
are based on higherorder unification and matching. 
18537  314 
*} 
315 

20514  316 
text %mlref {* 
317 
\begin{mldecls} 

318 
@{index_ML_type term} \\ 

20519  319 
@{index_ML "op aconv": "term * term > bool"} \\ 
20547  320 
@{index_ML map_types: "(typ > typ) > term > term"} \\ 
20519  321 
@{index_ML fold_types: "(typ > 'a > 'a) > term > 'a > 'a"} \\ 
20514  322 
@{index_ML map_aterms: "(term > term) > term > term"} \\ 
323 
@{index_ML fold_aterms: "(term > 'a > 'a) > term > 'a > 'a"} \\ 

20547  324 
\end{mldecls} 
325 
\begin{mldecls} 

20514  326 
@{index_ML fastype_of: "term > typ"} \\ 
20519  327 
@{index_ML lambda: "term > term > term"} \\ 
328 
@{index_ML betapply: "term * term > term"} \\ 

24972
acafb18a47dc
replaced Sign.add_consts_i by Sign.declare_const;
wenzelm
parents:
24828
diff
changeset

329 
@{index_ML Sign.declare_const: "Markup.property list > bstring * typ * mixfix > 
acafb18a47dc
replaced Sign.add_consts_i by Sign.declare_const;
wenzelm
parents:
24828
diff
changeset

330 
theory > term * theory"} \\ 
acafb18a47dc
replaced Sign.add_consts_i by Sign.declare_const;
wenzelm
parents:
24828
diff
changeset

331 
@{index_ML Sign.add_abbrev: "string > Markup.property list > bstring * term > 
acafb18a47dc
replaced Sign.add_consts_i by Sign.declare_const;
wenzelm
parents:
24828
diff
changeset

332 
theory > (term * term) * theory"} \\ 
20519  333 
@{index_ML Sign.const_typargs: "theory > string * typ > typ list"} \\ 
334 
@{index_ML Sign.const_instance: "theory > string * typ list > typ"} \\ 

20514  335 
\end{mldecls} 
18537  336 

20514  337 
\begin{description} 
18537  338 

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

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

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

20519  343 

344 
\item @{text "t"}~@{ML aconv}~@{text "u"} checks @{text 

345 
"\<alpha>"}equivalence of two terms. This is the basic equality relation 

346 
on type @{ML_type term}; raw datatype equality should only be used 

347 
for operations related to parsing or printing! 

348 

20547  349 
\item @{ML map_types}~@{text "f t"} applies the mapping @{text 
20537  350 
"f"} to all types occurring in @{text "t"}. 
351 

352 
\item @{ML fold_types}~@{text "f t"} iterates the operation @{text 

353 
"f"} over all occurrences of types in @{text "t"}; the term 

354 
structure is traversed from left to right. 

20519  355 

20537  356 
\item @{ML map_aterms}~@{text "f t"} applies the mapping @{text "f"} 
357 
to all atomic terms (@{ML Bound}, @{ML Free}, @{ML Var}, @{ML 

358 
Const}) occurring in @{text "t"}. 

359 

360 
\item @{ML fold_aterms}~@{text "f t"} iterates the operation @{text 

361 
"f"} over all occurrences of atomic terms (@{ML Bound}, @{ML Free}, 

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

20519  363 
traversed from left to right. 
364 

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

367 
omission of any sanity checks. 

20519  368 

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

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

20519  372 

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

375 
abstraction. 

20519  376 

24972
acafb18a47dc
replaced Sign.add_consts_i by Sign.declare_const;
wenzelm
parents:
24828
diff
changeset

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

378 
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

379 
syntax. 
20519  380 

24828  381 
\item @{ML Sign.add_abbrev}~@{text "print_mode properties (c, t)"} 
21827  382 
introduces a new term abbreviation @{text "c \<equiv> t"}. 
20519  383 

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

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

18537  388 

20514  389 
\end{description} 
18537  390 
*} 
391 

392 

20451  393 
section {* Theorems \label{sec:thms} *} 
18537  394 

395 
text {* 

20521  396 
\glossary{Proposition}{FIXME A \seeglossary{term} of 
397 
\seeglossary{type} @{text "prop"}. Internally, there is nothing 

398 
special about propositions apart from their type, but the concrete 

399 
syntax enforces a clear distinction. Propositions are structured 

400 
via implication @{text "A \<Longrightarrow> B"} or universal quantification @{text 

401 
"\<And>x. B x"}  anything else is considered atomic. The canonical 

402 
form for propositions is that of a \seeglossary{Hereditary Harrop 

403 
Formula}. FIXME} 

20480  404 

20501  405 
\glossary{Theorem}{A proven proposition within a certain theory and 
406 
proof context, formally @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; both contexts are 

407 
rarely spelled out explicitly. Theorems are usually normalized 

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

20480  409 

20519  410 
\glossary{Fact}{Sometimes used interchangeably for 
20501  411 
\seeglossary{theorem}. Strictly speaking, a list of theorems, 
412 
essentially an extralogical conjunction. Facts emerge either as 

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

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

18537  415 

20501  416 
\glossary{Schematic variable}{FIXME} 
417 

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

419 
proof context; an arbitrarybutfixed entity within a portion of 

420 
proof text. FIXME} 

18537  421 

20501  422 
\glossary{Free variable}{Synonymous for \seeglossary{fixed 
423 
variable}. FIXME} 

424 

425 
\glossary{Bound variable}{FIXME} 

18537  426 

20501  427 
\glossary{Variable}{See \seeglossary{schematic variable}, 
428 
\seeglossary{fixed variable}, \seeglossary{bound variable}, or 

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

430 
different variables is their binding scope. FIXME} 

18537  431 

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

435 
plain natural deduction rules for the primary connectives @{text 

20537  436 
"\<And>"} and @{text "\<Longrightarrow>"} of the framework. There is also a builtin 
437 
notion of equality/equivalence @{text "\<equiv>"}. 

20521  438 
*} 
439 

22322  440 
subsection {* Primitive connectives and rules \label{sec:prim_rules} *} 
18537  441 

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

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

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

447 
defined inductively by the primitive inferences given in 

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

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

450 
builtin equality is conceptually axiomatized as shown in 

20521  451 
\figref{fig:pureequality}, although the implementation works 
20543  452 
directly with derived inferences. 
20521  453 

454 
\begin{figure}[htb] 

455 
\begin{center} 

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

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

20521  459 
@{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop"} & equality relation (infix) \\ 
20501  460 
\end{tabular} 
20537  461 
\caption{Primitive connectives of Pure}\label{fig:pureconnectives} 
20521  462 
\end{center} 
463 
\end{figure} 

18537  464 

20501  465 
\begin{figure}[htb] 
466 
\begin{center} 

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

469 
\qquad 

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

471 
\] 

472 
\[ 

20537  473 
\infer[@{text "(\<And>_intro)"}]{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}}{@{text "\<Gamma> \<turnstile> b[x]"} & @{text "x \<notin> \<Gamma>"}} 
20498  474 
\qquad 
20537  475 
\infer[@{text "(\<And>_elim)"}]{@{text "\<Gamma> \<turnstile> b[a]"}}{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}} 
20498  476 
\] 
477 
\[ 

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

479 
\qquad 

480 
\infer[@{text "(\<Longrightarrow>_elim)"}]{@{text "\<Gamma>\<^sub>1 \<union> \<Gamma>\<^sub>2 \<turnstile> B"}}{@{text "\<Gamma>\<^sub>1 \<turnstile> A \<Longrightarrow> B"} & @{text "\<Gamma>\<^sub>2 \<turnstile> A"}} 

481 
\] 

20521  482 
\caption{Primitive inferences of Pure}\label{fig:primrules} 
483 
\end{center} 

484 
\end{figure} 

485 

486 
\begin{figure}[htb] 

487 
\begin{center} 

488 
\begin{tabular}{ll} 

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

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

20537  493 
@{text "\<turnstile> (A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<equiv> B"} & logical equivalence \\ 
20521  494 
\end{tabular} 
20542  495 
\caption{Conceptual axiomatization of Pure equality}\label{fig:pureequality} 
20501  496 
\end{center} 
497 
\end{figure} 

18537  498 

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

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

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

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

20491  508 

20537  509 
Observe that locally fixed parameters (as in @{text "\<And>_intro"}) need 
510 
not be recorded in the hypotheses, because the simple syntactic 

20543  511 
types of Pure are always inhabitable. ``Assumptions'' @{text "x :: 
512 
\<tau>"} for typemembership are only present as long as some @{text 

513 
"x\<^isub>\<tau>"} occurs in the statement body.\footnote{This is the key 

514 
difference to ``@{text "\<lambda>HOL"}'' in the PTS framework 

515 
\cite{BarendregtGeuvers:2001}, where hypotheses @{text "x : A"} are 

516 
treated uniformly for propositions and types.} 

20501  517 

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

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

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

523 
"instance"} rules as shown in \figref{fig:substrules}. 

20501  524 

525 
\begin{figure}[htb] 

526 
\begin{center} 

20498  527 
\[ 
20501  528 
\infer{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}{@{text "\<Gamma> \<turnstile> B[\<alpha>]"} & @{text "\<alpha> \<notin> \<Gamma>"}} 
529 
\quad 

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

20498  531 
\] 
532 
\[ 

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

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

20498  536 
\] 
20501  537 
\caption{Admissible substitution rules}\label{fig:substrules} 
538 
\end{center} 

539 
\end{figure} 

18537  540 

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

543 
variables. 

544 

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

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

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

549 
the result belongs to a different proof context. 

20542  550 

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

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

554 
The system always records oracle invocations within derivations of 

555 
theorems. Tracing plain axioms (and named theorems) is optional. 

20542  556 

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

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

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

20542  561 

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

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

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

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

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

20542  568 

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

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

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

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

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

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

576 
primitive recursion over the syntactic structure of a single type 

577 
argument. 

20521  578 
*} 
20498  579 

20521  580 
text %mlref {* 
581 
\begin{mldecls} 

582 
@{index_ML_type ctyp} \\ 

583 
@{index_ML_type cterm} \\ 

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

586 
\end{mldecls} 

587 
\begin{mldecls} 

20521  588 
@{index_ML_type thm} \\ 
20542  589 
@{index_ML proofs: "int ref"} \\ 
590 
@{index_ML Thm.assume: "cterm > thm"} \\ 

591 
@{index_ML Thm.forall_intr: "cterm > thm > thm"} \\ 

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

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

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

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

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

597 
@{index_ML Thm.get_axiom_i: "theory > string > thm"} \\ 

598 
@{index_ML Thm.invoke_oracle_i: "theory > string > theory * Object.T > thm"} \\ 

20547  599 
\end{mldecls} 
600 
\begin{mldecls} 

20542  601 
@{index_ML Theory.add_axioms_i: "(string * term) list > theory > theory"} \\ 
602 
@{index_ML Theory.add_deps: "string > string * typ > (string * typ) list > theory > theory"} \\ 

603 
@{index_ML Theory.add_oracle: "string * (theory * Object.T > term) > theory > theory"} \\ 

604 
@{index_ML Theory.add_defs_i: "bool > bool > (bstring * term) list > theory > theory"} \\ 

20521  605 
\end{mldecls} 
606 

607 
\begin{description} 

608 

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

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

612 
welltypedness) checks, relative to the declarations of type 

613 
constructors, constants etc. in the theory. 

614 

20547  615 
\item @{ML ctyp_of}~@{text "thy \<tau>"} and @{ML cterm_of}~@{text "thy 
616 
t"} explicitly checks types and terms, respectively. This also 

617 
involves some basic normalizations, such expansion of type and term 

618 
abbreviations from the theory context. 

619 

620 
Recertification is relatively slow and should be avoided in tight 

621 
reasoning loops. There are separate operations to decompose 

622 
certified entities (including actual theorems). 

20542  623 

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

625 
abstract datatype that guarantees that its values have been 

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

20543  627 
Every @{ML thm} value contains a sliding backreference to the 
628 
enclosing theory, cf.\ \secref{sec:contexttheory}. 

20542  629 

20543  630 
\item @{ML proofs} determines the detail of proof recording within 
631 
@{ML_type thm} values: @{ML 0} records only oracles, @{ML 1} records 

632 
oracles, axioms and named theorems, @{ML 2} records full proof 

633 
terms. 

20542  634 

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

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

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

638 

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

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

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

643 
basic names. 

20521  644 

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

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

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

649 
refer to the instantiated versions. 

650 

651 
\item @{ML Thm.get_axiom_i}~@{text "thy name"} retrieves a named 

652 
axiom, cf.\ @{text "axiom"} in \figref{fig:primrules}. 

653 

20543  654 
\item @{ML Thm.invoke_oracle_i}~@{text "thy name arg"} invokes a 
655 
named oracle function, cf.\ @{text "axiom"} in 

656 
\figref{fig:primrules}. 

20521  657 

20543  658 
\item @{ML Theory.add_axioms_i}~@{text "[(name, A), \<dots>]"} declares 
659 
arbitrary propositions as axioms. 

20542  660 

20543  661 
\item @{ML Theory.add_oracle}~@{text "(name, f)"} declares an oracle 
662 
function for generating arbitrary axioms on the fly. 

20542  663 

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

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

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

20542  668 

669 
\item @{ML Theory.add_defs_i}~@{text "unchecked overloaded [(name, c 

20543  670 
\<^vec>x \<equiv> t), \<dots>]"} states a definitional axiom for an existing 
671 
constant @{text "c"}. Dependencies are recorded (cf.\ @{ML 

672 
Theory.add_deps}), unless the @{text "unchecked"} option is set. 

20521  673 

674 
\end{description} 

675 
*} 

676 

677 

20543  678 
subsection {* Auxiliary definitions *} 
20521  679 

680 
text {* 

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

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

20501  684 

685 
\begin{figure}[htb] 

686 
\begin{center} 

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

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

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

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

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

20498  696 
\end{tabular} 
20521  697 
\caption{Definitions of auxiliary connectives}\label{fig:pureaux} 
20501  698 
\end{center} 
699 
\end{figure} 

700 

20537  701 
Derived conjunction rules include introduction @{text "A \<Longrightarrow> B \<Longrightarrow> A & 
702 
B"}, and destructions @{text "A & B \<Longrightarrow> A"} and @{text "A & B \<Longrightarrow> B"}. 

703 
Conjunction allows to treat simultaneous assumptions and conclusions 

704 
uniformly. For example, multiple claims are intermediately 

20543  705 
represented as explicit conjunction, but this is refined into 
706 
separate subgoals before the user continues the proof; the final 

707 
result is projected into a list of theorems (cf.\ 

20537  708 
\secref{sec:tacticalgoals}). 
20498  709 

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

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

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

20521  714 

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

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

718 
uniformly, similar to a typetheoretic framework. 

20498  719 

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

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

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

20521  724 
itself\<^esub>"}. 
20537  725 
Although being devoid of any particular meaning, the @{text 
726 
"TYPE(\<tau>)"} accounts for the type @{text "\<tau>"} within the term 

727 
language. In particular, @{text "TYPE(\<alpha>)"} may be used as formal 

728 
argument in primitive definitions, in order to circumvent hidden 

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

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

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

732 
argument, which is essentially a predicate on types. 

20521  733 
*} 
20501  734 

20521  735 
text %mlref {* 
736 
\begin{mldecls} 

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

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

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

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

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

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

743 
\end{mldecls} 

744 

745 
\begin{description} 

746 

20542  747 
\item @{ML Conjunction.intr} derives @{text "A & B"} from @{text 
748 
"A"} and @{text "B"}. 

749 

20543  750 
\item @{ML Conjunction.elim} derives @{text "A"} and @{text "B"} 
20542  751 
from @{text "A & B"}. 
752 

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

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

20542  757 

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

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

760 

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

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

20521  763 

764 
\end{description} 

20491  765 
*} 
18537  766 

20480  767 

20491  768 
section {* Rules \label{sec:rules} *} 
18537  769 

20929  770 
text %FIXME {* 
18537  771 

772 
FIXME 

773 

20491  774 
A \emph{rule} is any Pure theorem in HHF normal form; there is a 
775 
separate calculus for rule composition, which is modeled after 

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

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

778 

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

780 
Lowlevel inferences are occasional required internally, but the 

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

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

783 
important to maintain this invariant in addon applications! 

784 

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

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

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

20519  788 
combined in the variants of @{text "elimresolution"} and @{text 
20491  789 
"destresolution"}. Raw @{text "composition"} is occasionally 
790 
useful as well, also it is strictly speaking outside of the proper 

791 
rule calculus. 

792 

793 
Rules are treated modulo general higherorder unification, which is 

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

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

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

797 

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

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

800 
practice not to contract or expand unnecessarily. Some mechanisms 

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

802 
danger to produce some oscillation! 

803 

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

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

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

807 

18537  808 
\glossary{Hereditary Harrop Formula}{The set of propositions in HHF 
809 
format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow> 

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

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

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

813 
quantifier prefix is represented via \seeglossary{schematic 

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

815 
\seeglossary{Horn Clause}}. 

816 

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

818 

20498  819 

820 
\[ 

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

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

823 
\] 

824 

825 

826 
\[ 

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

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

829 
\] 

830 

831 

832 
\[ 

833 
\infer[@{text "(\<And>_lift)"}]{@{text "(\<And>\<^vec>x. \<^vec>A (?\<^vec>a \<^vec>x)) \<Longrightarrow> (\<And>\<^vec>x. B (?\<^vec>a \<^vec>x))"}}{@{text "\<^vec>A ?\<^vec>a \<Longrightarrow> B ?\<^vec>a"}} 

834 
\] 

835 
\[ 

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

837 
\] 

838 

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

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

841 

842 
\[ 

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

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

845 
{\begin{tabular}{l} 

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

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

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

849 
\end{tabular}} 

850 
\] 

851 

852 

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

18537  854 
*} 
855 

20498  856 

18537  857 
end 