author  wenzelm 
Sun, 01 May 2011 17:42:21 +0200  
changeset 42517  b68e1c27709a 
parent 42510  b9c106763325 
child 42666  fee67c099d03 
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"} \\ 

42401
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40255
diff
changeset

130 
@{index_ML Sign.add_types: "Proof.context > 
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40255
diff
changeset

131 
(binding * int * mixfix) list > theory > theory"} \\ 
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40255
diff
changeset

132 
@{index_ML Sign.add_type_abbrev: "Proof.context > 
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40255
diff
changeset

133 
binding * string list * typ > theory > theory"} \\ 
30355  134 
@{index_ML Sign.primitive_class: "binding * class list > theory > theory"} \\ 
20480  135 
@{index_ML Sign.primitive_classrel: "class * class > theory > theory"} \\ 
136 
@{index_ML Sign.primitive_arity: "arity > theory > theory"} \\ 

137 
\end{mldecls} 

138 

139 
\begin{description} 

140 

39864  141 
\item Type @{ML_type class} represents type classes. 
20480  142 

39864  143 
\item Type @{ML_type sort} represents sorts, i.e.\ finite 
144 
intersections of classes. The empty list @{ML "[]: sort"} refers to 

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

20451  146 

39864  147 
\item Type @{ML_type arity} represents type arities. A triple 
148 
@{text "(\<kappa>, \<^vec>s, s) : arity"} represents @{text "\<kappa> :: 

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

20480  150 

39864  151 
\item Type @{ML_type typ} represents types; this is a datatype with 
20480  152 
constructors @{ML TFree}, @{ML TVar}, @{ML Type}. 
153 

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

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

20519  157 

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

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

161 
right. 

20494  162 

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

165 

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

20480  168 

42401
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40255
diff
changeset

169 
\item @{ML Sign.add_types}~@{text "ctxt [(\<kappa>, k, mx), \<dots>]"} declares a 
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40255
diff
changeset

170 
new type constructors @{text "\<kappa>"} with @{text "k"} arguments and 
20480  171 
optional mixfix syntax. 
20451  172 

42401
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40255
diff
changeset

173 
\item @{ML Sign.add_type_abbrev}~@{text "ctxt (\<kappa>, \<^vec>\<alpha>, \<tau>)"} 
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40255
diff
changeset

174 
defines a new type abbreviation @{text "(\<^vec>\<alpha>)\<kappa> = \<tau>"}. 
20480  175 

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

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

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

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

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

187 
\end{description} 

20437  188 
*} 
189 

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

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

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

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

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

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

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

198 
\end{matharray} 

199 

42510
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset

200 
@{rail " 
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset

201 
@@{ML_antiquotation class} nameref 
39832  202 
; 
42510
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset

203 
@@{ML_antiquotation sort} sort 
39832  204 
; 
42510
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset

205 
(@@{ML_antiquotation type_name}  
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset

206 
@@{ML_antiquotation type_abbrev}  
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset

207 
@@{ML_antiquotation nonterminal}) nameref 
39832  208 
; 
42510
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset

209 
@@{ML_antiquotation typ} type 
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset

210 
"} 
39832  211 

212 
\begin{description} 

213 

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

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

216 

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

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

219 

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

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

222 

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

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

225 

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

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

228 
literal. 

229 

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

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

232 

233 
\end{description} 

234 
*} 

235 

20437  236 

20451  237 
section {* Terms \label{sec:terms} *} 
18537  238 

239 
text {* 

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

34929  244 
have an explicit name and type in each occurrence. 
20514  245 

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

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

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

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

253 
the nesting of abstractions. 

20537  254 

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

259 
without any loose variables. 

20514  260 

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

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

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

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

20514  272 

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

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

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

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

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

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

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

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

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

20480  283 

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

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

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

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

20480  290 

39861
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39846
diff
changeset

291 
\medskip An \emph{atomic term} is either a variable or constant. 
34929  292 
The logical category \emph{term} is defined inductively over atomic 
293 
terms, with abstraction and application as follows: @{text "t = b  

294 
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 

295 
converting between an external representation with named bound 

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

297 
of internal deBruijn representation. 

20498  298 

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

301 
applicatins: 

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

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

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

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

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

314 
Typeinference depends on a context of type constraints for fixed 

315 
variables, and declarations for polymorphic constants. 

316 

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

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

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

322 
polymorphic constants occur routinely. 

20514  323 

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

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

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

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

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

20543  330 
pathological situation notoriously demands additional care. 
20514  331 

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

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

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

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

20519  338 

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

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

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

20537  346 
does not occur in @{text "f"}. 
20519  347 

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

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

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

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

18537  354 
*} 
355 

20514  356 
text %mlref {* 
357 
\begin{mldecls} 

358 
@{index_ML_type term} \\ 

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

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

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

20547  364 
\end{mldecls} 
365 
\begin{mldecls} 

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

42401
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40255
diff
changeset

369 
@{index_ML Sign.declare_const: "Proof.context > 
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40255
diff
changeset

370 
(binding * typ) * mixfix > theory > term * theory"} \\ 
33174  371 
@{index_ML Sign.add_abbrev: "string > binding * term > 
24972
acafb18a47dc
replaced Sign.add_consts_i by Sign.declare_const;
wenzelm
parents:
24828
diff
changeset

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

20514  375 
\end{mldecls} 
18537  376 

20514  377 
\begin{description} 
18537  378 

39864  379 
\item Type @{ML_type term} represents deBruijn terms, with comments 
380 
in abstractions, and explicitly named free variables and constants; 

20537  381 
this is a datatype with constructors @{ML Bound}, @{ML Free}, @{ML 
382 
Var}, @{ML Const}, @{ML Abs}, @{ML "op $"}. 

20519  383 

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

387 
for operations related to parsing or printing! 

388 

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

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

20537  394 
structure is traversed from left to right. 
20519  395 

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

20537  398 
Const}) occurring in @{text "t"}. 
399 

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

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

20519  403 
traversed from left to right. 
404 

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

407 
omission of any sanity checks. 

20519  408 

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

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

20519  412 

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

415 
abstraction. 

20519  416 

42401
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40255
diff
changeset

417 
\item @{ML Sign.declare_const}~@{text "ctxt ((c, \<sigma>), mx)"} declares 
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40255
diff
changeset

418 
a new constant @{text "c :: \<sigma>"} with optional mixfix syntax. 
20519  419 

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

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

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

18537  427 

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

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

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

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

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

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

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

438 
\end{matharray} 

439 

42510
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset

440 
@{rail " 
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset

441 
(@@{ML_antiquotation const_name}  
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset

442 
@@{ML_antiquotation const_abbrev}) nameref 
39832  443 
; 
42510
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset

444 
@@{ML_antiquotation const} ('(' (type + ',') ')')? 
39832  445 
; 
42510
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset

446 
@@{ML_antiquotation term} term 
39832  447 
; 
42510
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset

448 
@@{ML_antiquotation prop} prop 
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset

449 
"} 
39832  450 

451 
\begin{description} 

452 

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

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

455 

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

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

458 
literal. 

459 

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

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

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

463 
datatype @{ML_type term}. 

464 

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

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

467 

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

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

470 

471 
\end{description} 

472 
*} 

473 

18537  474 

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

477 
text {* 

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

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

20521  484 
*} 
485 

29758  486 

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

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

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

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

494 
defined inductively by the primitive inferences given in 

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

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

497 
builtin equality is conceptually axiomatized as shown in 

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

501 
\begin{figure}[htb] 

502 
\begin{center} 

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

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

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

18537  511 

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

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

516 
\qquad 

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

518 
\] 

519 
\[ 

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

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

531 
\end{figure} 

532 

533 
\begin{figure}[htb] 

534 
\begin{center} 

535 
\begin{tabular}{ll} 

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

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

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

18537  545 

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

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

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

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

20491  555 

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

558 
the simple syntactic types of Pure are always inhabitable. 

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

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

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

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

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

20501  564 

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

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

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

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

572 
\begin{figure}[htb] 

573 
\begin{center} 

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

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

20498  578 
\] 
579 
\[ 

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

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

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

586 
\end{figure} 

18537  587 

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

590 
variables. 

591 

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

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

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

596 
the result belongs to a different proof context. 

20542  597 

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

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

601 
The system always records oracle invocations within derivations of 

29768  602 
theorems by a unique tag. 
20542  603 

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

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

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

20542  608 

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

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

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

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

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

20542  615 

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

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

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

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

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

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

623 
primitive recursion over the syntactic structure of a single type 

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

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

629 
@{index_ML_type ctyp} \\ 

630 
@{index_ML_type cterm} \\ 

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

633 
\end{mldecls} 

634 
\begin{mldecls} 

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

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

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

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

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

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

42401
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40255
diff
changeset

644 
@{index_ML Thm.add_axiom: "Proof.context > 
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40255
diff
changeset

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

42401
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40255
diff
changeset

648 
@{index_ML Thm.add_def: "Proof.context > bool > bool > 
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40255
diff
changeset

649 
binding * term > theory > (string * thm) * theory"} \\ 
20547  650 
\end{mldecls} 
651 
\begin{mldecls} 

42401
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40255
diff
changeset

652 
@{index_ML Theory.add_deps: "Proof.context > string > 
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40255
diff
changeset

653 
string * typ > (string * typ) list > theory > theory"} \\ 
20521  654 
\end{mldecls} 
655 

656 
\begin{description} 

657 

39864  658 
\item Types @{ML_type ctyp} and @{ML_type cterm} represent certified 
659 
types and terms, respectively. These are abstract datatypes that 

20542  660 
guarantee that its values have passed the full wellformedness (and 
661 
welltypedness) checks, relative to the declarations of type 

662 
constructors, constants etc. in the theory. 

663 

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

666 
respectively. This also involves some basic normalizations, such 

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

20547  668 

669 
Recertification is relatively slow and should be avoided in tight 

670 
reasoning loops. There are separate operations to decompose 

671 
certified entities (including actual theorems). 

20542  672 

39864  673 
\item Type @{ML_type thm} represents proven propositions. This is 
674 
an abstract datatype that guarantees that its values have been 

20542  675 
constructed by basic principles of the @{ML_struct Thm} module. 
39281  676 
Every @{ML_type thm} value contains a sliding backreference to the 
20543  677 
enclosing theory, cf.\ \secref{sec:contexttheory}. 
20542  678 

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

682 
records full proof terms. Officially named theorems that contribute 

34929  683 
to a result are recorded in any case. 
20542  684 

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

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

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

688 

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

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

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

693 
basic names. 

20521  694 

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

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

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

699 
refer to the instantiated versions. 

700 

42401
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40255
diff
changeset

701 
\item @{ML Thm.add_axiom}~@{text "ctxt (name, A)"} declares an 
35927  702 
arbitrary proposition as axiom, and retrieves it as a theorem from 
703 
the resulting theory, cf.\ @{text "axiom"} in 

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

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

20542  706 

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

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

20521  710 

42401
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40255
diff
changeset

711 
\item @{ML Thm.add_def}~@{text "ctxt unchecked overloaded (name, c 
35927  712 
\<^vec>x \<equiv> t)"} states a definitional axiom for an existing constant 
713 
@{text "c"}. Dependencies are recorded via @{ML Theory.add_deps}, 

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

715 
lowlevel representation in the axiom table may differ slightly from 

716 
the returned theorem. 

20542  717 

42401
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40255
diff
changeset

718 
\item @{ML Theory.add_deps}~@{text "ctxt name c\<^isub>\<tau> \<^vec>d\<^isub>\<sigma>"} 
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40255
diff
changeset

719 
declares dependencies of a named specification for constant @{text 
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40255
diff
changeset

720 
"c\<^isub>\<tau>"}, relative to existing specifications for constants @{text 
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40255
diff
changeset

721 
"\<^vec>d\<^isub>\<sigma>"}. 
20542  722 

20521  723 
\end{description} 
724 
*} 

725 

726 

39832  727 
text %mlantiq {* 
728 
\begin{matharray}{rcl} 

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

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

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

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

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

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

735 
\end{matharray} 

736 

42510
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset

737 
@{rail " 
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset

738 
@@{ML_antiquotation ctyp} typ 
39832  739 
; 
42510
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset

740 
@@{ML_antiquotation cterm} term 
39832  741 
; 
42510
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset

742 
@@{ML_antiquotation cprop} prop 
39832  743 
; 
42510
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset

744 
@@{ML_antiquotation thm} thmref 
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset

745 
; 
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset

746 
@@{ML_antiquotation thms} thmrefs 
39832  747 
; 
42517
b68e1c27709a
simplified keyword markup (without formal checking);
wenzelm
parents:
42510
diff
changeset

748 
@@{ML_antiquotation lemma} ('(' @'open' ')')? ((prop +) + @'and') \\ 
b68e1c27709a
simplified keyword markup (without formal checking);
wenzelm
parents:
42510
diff
changeset

749 
@'by' method method? 
42510
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
42401
diff
changeset

750 
"} 
39832  751 

752 
\begin{description} 

753 

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

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

756 
ctyp}. 

757 

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

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

760 
value of type @{ML_type cterm}. 

761 

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

763 
value of type @{ML_type thm}. 

764 

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

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

767 

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

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

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

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

772 
given here. 

773 

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

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

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

777 

778 
Since ML antiquotations are always evaluated at compiletime, there 

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

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

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

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

783 
the result. 

784 

785 
\end{description} 

786 

787 
*} 

788 

789 

40126  790 
subsection {* Auxiliary definitions \label{sec:logicaux} *} 
20521  791 

792 
text {* 

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

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

20501  796 

797 
\begin{figure}[htb] 

798 
\begin{center} 

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

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

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

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

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

20498  808 
\end{tabular} 
20521  809 
\caption{Definitions of auxiliary connectives}\label{fig:pureaux} 
20501  810 
\end{center} 
811 
\end{figure} 

812 

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

815 
available as derived rules. Conjunction allows to treat 

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

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

818 
represents multiple claims as explicit conjunction internally, but 

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

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

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

20537  822 
\secref{sec:tacticalgoals}). 
20498  823 

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

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

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

20521  828 

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

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

832 
uniformly, similar to a typetheoretic framework. 

20498  833 

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

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

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

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

842 
argument in primitive definitions, in order to circumvent hidden 

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

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

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

846 
argument, which is essentially a predicate on types. 

20521  847 
*} 
20501  848 

20521  849 
text %mlref {* 
850 
\begin{mldecls} 

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

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

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

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

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

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

857 
\end{mldecls} 

858 

859 
\begin{description} 

860 

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

20543  864 
\item @{ML Conjunction.elim} derives @{text "A"} and @{text "B"} 
34929  865 
from @{text "A &&& B"}. 
20542  866 

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

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

20542  871 

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

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

874 

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

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

20521  877 

878 
\end{description} 

20491  879 
*} 
18537  880 

20480  881 

28784  882 
section {* Objectlevel rules \label{sec:objrules} *} 
18537  883 

29768  884 
text {* 
885 
The primitive inferences covered so far mostly serve foundational 

886 
purposes. Userlevel reasoning usually works via objectlevel rules 

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

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

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

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

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

893 
*} 
20491  894 

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

895 

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

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

897 

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

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

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

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

903 
\[ 

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

905 
\] 

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

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

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

909 
objectlevel inference corresponds to an iterated implication in 

910 
Pure like this: 

911 
\[ 

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

913 
\] 

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

914 
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

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

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

918 
@{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  919 
\] 
20491  920 

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

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

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

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

925 
inductive characterization as follows: 
29768  926 

927 
\medskip 

928 
\begin{tabular}{ll} 

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

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

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

932 
\end{tabular} 

933 
\medskip 

934 

39861
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39846
diff
changeset

935 
Thus we essentially impose nesting levels on propositions formed 
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39846
diff
changeset

936 
from @{text "\<And>"} and @{text "\<Longrightarrow>"}. At each level there is a prefix 
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39846
diff
changeset

937 
of parameters and compound premises, concluding an atomic 
29770  938 
proposition. Typical examples are @{text "\<longrightarrow>"}introduction @{text 
939 
"(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B"} or mathematical induction @{text "P 0 \<Longrightarrow> (\<And>n. P n 

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

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

34929  942 
already marks the limit of rule complexity that is usually seen in 
943 
practice. 

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

944 

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

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

947 

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

948 
\begin{itemize} 
29768  949 

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

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

953 
Hereditary Harrop Formula. 

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

954 

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

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

959 
parameters, and vacuous quantifiers vanish automatically. 

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

960 

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

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

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

963 

29771  964 
text %mlref {* 
965 
\begin{mldecls} 

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

966 
@{index_ML Simplifier.norm_hhf: "thm > thm"} \\ 
29771  967 
\end{mldecls} 
968 

969 
\begin{description} 

970 

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

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

974 
handle Hereditary Harrop Formulae properly. 

975 

976 
\end{description} 

977 
*} 

978 

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

979 

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

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

981 

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

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

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

986 
higherorder unification. There are also combined variants, notably 

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

20491  988 

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

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

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

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

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

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

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

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

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

20498  1003 

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

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

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

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

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

1010 
by means of iterated application of the following inferences: 

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

29771  1015 
\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  1016 
\] 
29771  1017 
By combining raw composition with lifting, we get full @{inference 
1018 
resolution} as follows: 

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

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

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

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

1026 
\end{tabular}} 

1027 
\] 

1028 

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

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

1032 
solved situation (again modulo unification): 

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

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

1036 
\] 

20498  1037 

29771  1038 
FIXME @{inference_def elim_resolution}, @{inference_def dest_resolution} 
18537  1039 
*} 
1040 

29768  1041 
text %mlref {* 
1042 
\begin{mldecls} 

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

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

1045 
\end{mldecls} 

1046 

1047 
\begin{description} 

1048 

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

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

1052 
Isar language is called @{attribute THEN}. 

29768  1053 

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

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

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

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

29768  1060 

1061 
\end{description} 

1062 
*} 

30272  1063 

18537  1064 
end 