author  wenzelm 
Tue, 13 Aug 2013 16:25:47 +0200  
changeset 53015  a1119cf551e8 
parent 52788  da1fdbfebd39 
child 53071  1958a5e65ea5 
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 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

41 
"c\<^sub>1 \<subseteq> c\<^sub>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 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

46 
A \emph{sort} is a list of type classes written as @{text "s = {c\<^sub>1, 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

47 
\<dots>, c\<^sub>m}"}, it represents symbolic intersection. Notationally, the 
34929  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 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

51 
intersections: @{text "{c\<^sub>1, \<dots> c\<^sub>m} \<subseteq> {d\<^sub>1, \<dots>, d\<^sub>n}"} iff @{text 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

52 
"\<forall>j. \<exists>i. c\<^sub>i \<subseteq> d\<^sub>j"}. The empty intersection @{text "{}"} refers to 
34929  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.\ 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

60 
@{text "('a, s)"} which is usually printed as @{text "\<alpha>\<^sub>s"}. 
20537  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 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

63 
printed as @{text "?\<alpha>\<^sub>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 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

73 
written postfix as @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>k)\<kappa>"}. For 
20537  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 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

82 
variables and type constructors as follows: @{text "\<tau> = \<alpha>\<^sub>s  ?\<alpha>\<^sub>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 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

92 
constructor wrt.\ the algebra of sorts: @{text "\<kappa> :: (s\<^sub>1, \<dots>, 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

93 
s\<^sub>k)s"} means that @{text "(\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)\<kappa>"} is 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

94 
of sort @{text "s"} if every argument type @{text "\<tau>\<^sub>i"} is 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

95 
of sort @{text "s\<^sub>i"}. Arity declarations are implicitly 
20494  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 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

102 
"c\<^sub>1 \<subseteq> c\<^sub>2"}, and arities @{text "\<kappa> :: 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

103 
(\<^vec>s\<^sub>1)c\<^sub>1"} and @{text "\<kappa> :: 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

104 
(\<^vec>s\<^sub>2)c\<^sub>2"} holds @{text "\<^vec>s\<^sub>1 \<subseteq> 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

105 
\<^vec>s\<^sub>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 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

110 
vector of argument sorts @{text "(s\<^sub>1, \<dots>, s\<^sub>k)"} such 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

111 
that a type scheme @{text "(\<alpha>\<^bsub>s\<^sub>1\<^esub>, \<dots>, 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

112 
\<alpha>\<^bsub>s\<^sub>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"} \\ 

47174  130 
@{index_ML Sign.add_type: "Proof.context > binding * int * mixfix > theory > theory"} \\ 
42401
9bfaf6819291
updated some theory primitives, which now depend on auxiliary context;
wenzelm
parents:
40255
diff
changeset

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

132 
binding * string list * typ > theory > theory"} \\ 
30355  133 
@{index_ML Sign.primitive_class: "binding * class list > theory > theory"} \\ 
20480  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 

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

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

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

20451  145 

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

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

20480  149 

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

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

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

20519  156 

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

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

160 
right. 

20494  161 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

162 
\item @{ML Sign.subsort}~@{text "thy (s\<^sub>1, s\<^sub>2)"} 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

163 
tests the subsort relation @{text "s\<^sub>1 \<subseteq> s\<^sub>2"}. 
20480  164 

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

20480  167 

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

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

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

172 
\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

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

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

175 
\item @{ML Sign.primitive_class}~@{text "(c, [c\<^sub>1, \<dots>, 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

176 
c\<^sub>n])"} declares a new class @{text "c"}, together with class 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

177 
relations @{text "c \<subseteq> c\<^sub>i"}, for @{text "i = 1, \<dots>, n"}. 
20480  178 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

179 
\item @{ML Sign.primitive_classrel}~@{text "(c\<^sub>1, 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

180 
c\<^sub>2)"} declares the class relation @{text "c\<^sub>1 \<subseteq> 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

181 
c\<^sub>2"}. 
20480  182 

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

186 
\end{description} 

20437  187 
*} 
188 

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

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

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

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

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

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

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

197 
\end{matharray} 

198 

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

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

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

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

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

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

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

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

209 
"} 
39832  210 

211 
\begin{description} 

212 

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

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

215 

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

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

218 

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

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

221 

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

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

224 

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

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

227 
literal. 

228 

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

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

231 

232 
\end{description} 

233 
*} 

234 

20437  235 

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

238 
text {* 

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

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

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

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

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

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

252 
the nesting of abstractions. 

20537  253 

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

258 
without any loose variables. 

20514  259 

20537  260 
A \emph{fixed variable} is a pair of a basic name and a type, e.g.\ 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

261 
@{text "(x, \<tau>)"} which is usually printed @{text "x\<^sub>\<tau>"} here. A 
20537  262 
\emph{schematic variable} is a pair of an indexname and a type, 
34929  263 
e.g.\ @{text "((x, 0), \<tau>)"} which is likewise printed as @{text 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

264 
"?x\<^sub>\<tau>"}. 
20491  265 

20537  266 
\medskip A \emph{constant} is a pair of a basic name and a type, 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

267 
e.g.\ @{text "(c, \<tau>)"} which is usually printed as @{text "c\<^sub>\<tau>"} 
34929  268 
here. Constants are declared in the context as polymorphic families 
269 
@{text "c :: \<sigma>"}, meaning that all substitution instances @{text 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

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

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

272 
The vector of \emph{type arguments} of constant @{text "c\<^sub>\<tau>"} wrt.\ 
34929  273 
the declaration @{text "c :: \<sigma>"} is defined as the codomain of the 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

274 
matcher @{text "\<vartheta> = {?\<alpha>\<^sub>1 \<mapsto> \<tau>\<^sub>1, \<dots>, ?\<alpha>\<^sub>n \<mapsto> \<tau>\<^sub>n}"} presented in 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

275 
canonical order @{text "(\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>n)"}, corresponding to the 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

276 
lefttoright occurrences of the @{text "\<alpha>\<^sub>i"} in @{text "\<sigma>"}. 
34929  277 
Within a given theory context, there is a onetoone correspondence 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

278 
between any constant @{text "c\<^sub>\<tau>"} and the application @{text "c(\<tau>\<^sub>1, 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

279 
\<dots>, \<tau>\<^sub>n)"} of its type arguments. For example, with @{text "plus :: \<alpha> 
34929  280 
\<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"}, the instance @{text "plus\<^bsub>nat \<Rightarrow> nat \<Rightarrow> nat\<^esub>"} corresponds to 
281 
@{text "plus(nat)"}. 

20480  282 

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

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

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

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

20480  289 

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

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

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

293 
x\<^sub>\<tau>  ?x\<^sub>\<tau>  c\<^sub>\<tau>  \<lambda>\<^sub>\<tau>. t  t\<^sub>1 t\<^sub>2"}. Parsing and printing takes care of 
34929  294 
converting between an external representation with named bound 
295 
variables. Subsequently, we shall use the latter notation instead 

296 
of internal deBruijn representation. 

20498  297 

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

300 
applicatins: 

20498  301 
\[ 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

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

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

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

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

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

313 
Typeinference depends on a context of type constraints for fixed 

314 
variables, and declarations for polymorphic constants. 

315 

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

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

318 
"x\<^bsub>\<tau>\<^sub>1\<^esub>"} and @{text "x\<^bsub>\<tau>\<^sub>2\<^esub>"} may become the same after 
34929  319 
type instantiation. Typeinference rejects variables of the same 
320 
name, but different types. In contrast, mixed instances of 

321 
polymorphic constants occur routinely. 

20514  322 

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

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

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

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

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

20543  329 
pathological situation notoriously demands additional care. 
20514  330 

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

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

332 
"c\<^sub>\<sigma> \<equiv> t"} of a closed term @{text "t"} of type @{text "\<sigma>"}, 
20537  333 
without any hidden polymorphism. A term abbreviation looks like a 
20543  334 
constant in the syntax, but is expanded before entering the logical 
335 
core. Abbreviations are usually reverted when printing terms, using 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

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

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

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

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

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

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

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

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

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

18537  353 
*} 
354 

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

357 
@{index_ML_type term} \\ 

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

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

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

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

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

42934  368 
@{index_ML incr_boundvars: "int > 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; 

52408  381 
this is a datatype with constructors @{index_ML Bound}, @{index_ML 
382 
Free}, @{index_ML Var}, @{index_ML Const}, @{index_ML Abs}, 

383 
@{index_ML_op "$"}. 

20519  384 

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

388 
for operations related to parsing or printing! 

389 

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

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

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

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

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

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

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

20519  404 
traversed from left to right. 
405 

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

408 
omission of any sanity checks. 

20519  409 

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

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

20519  413 

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

416 
abstraction. 

20519  417 

42934  418 
\item @{ML incr_boundvars}~@{text "j"} increments a term's dangling 
419 
bound variables by the offset @{text "j"}. This is required when 

420 
moving a subterm into a context where it is enclosed by a different 

421 
number of abstractions. Bound variables with a matching abstraction 

422 
are unaffected. 

423 

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

424 
\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

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

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

20520  430 
\item @{ML Sign.const_typargs}~@{text "thy (c, \<tau>)"} and @{ML 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

431 
Sign.const_instance}~@{text "thy (c, [\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>n])"} 
20543  432 
convert between two representations of polymorphic constants: full 
433 
type instance vs.\ compact type arguments form. 

18537  434 

20514  435 
\end{description} 
18537  436 
*} 
437 

39832  438 
text %mlantiq {* 
439 
\begin{matharray}{rcl} 

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

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

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

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

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

445 
\end{matharray} 

446 

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

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

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

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

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

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

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

456 
"} 
39832  457 

458 
\begin{description} 

459 

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

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

462 

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

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

465 
literal. 

466 

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

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

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

470 
datatype @{ML_type term}. 

471 

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

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

474 

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

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

477 

478 
\end{description} 

479 
*} 

480 

18537  481 

20451  482 
section {* Theorems \label{sec:thms} *} 
18537  483 

484 
text {* 

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

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

20521  491 
*} 
492 

29758  493 

26872  494 
subsection {* Primitive connectives and rules \label{sec:primrules} *} 
18537  495 

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

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

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

500 
derivability judgment @{text "A\<^sub>1, \<dots>, A\<^sub>n \<turnstile> B"} is 
20543  501 
defined inductively by the primitive inferences given in 
502 
\figref{fig:primrules}, with the global restriction that the 

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

504 
builtin equality is conceptually axiomatized as shown in 

20521  505 
\figref{fig:pureequality}, although the implementation works 
20543  506 
directly with derived inferences. 
20521  507 

508 
\begin{figure}[htb] 

509 
\begin{center} 

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

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

20521  513 
@{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop"} & equality relation (infix) \\ 
20501  514 
\end{tabular} 
20537  515 
\caption{Primitive connectives of Pure}\label{fig:pureconnectives} 
20521  516 
\end{center} 
517 
\end{figure} 

18537  518 

20501  519 
\begin{figure}[htb] 
520 
\begin{center} 

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

523 
\qquad 

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

525 
\] 

526 
\[ 

52407  527 
\infer[@{text "(\<And>\<hyphen>intro)"}]{@{text "\<Gamma> \<turnstile> \<And>x. B[x]"}}{@{text "\<Gamma> \<turnstile> B[x]"} & @{text "x \<notin> \<Gamma>"}} 
20498  528 
\qquad 
52407  529 
\infer[@{text "(\<And>\<hyphen>elim)"}]{@{text "\<Gamma> \<turnstile> B[a]"}}{@{text "\<Gamma> \<turnstile> \<And>x. B[x]"}} 
20498  530 
\] 
531 
\[ 

42666  532 
\infer[@{text "(\<Longrightarrow>\<hyphen>intro)"}]{@{text "\<Gamma>  A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}} 
20498  533 
\qquad 
42666  534 
\infer[@{text "(\<Longrightarrow>\<hyphen>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  535 
\] 
20521  536 
\caption{Primitive inferences of Pure}\label{fig:primrules} 
537 
\end{center} 

538 
\end{figure} 

539 

540 
\begin{figure}[htb] 

541 
\begin{center} 

542 
\begin{tabular}{ll} 

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

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

20537  547 
@{text "\<turnstile> (A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<equiv> B"} & logical equivalence \\ 
20521  548 
\end{tabular} 
20542  549 
\caption{Conceptual axiomatization of Pure equality}\label{fig:pureequality} 
20501  550 
\end{center} 
551 
\end{figure} 

18537  552 

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

52408  558 
explicit proof terms for primitive inferences, see also 
559 
\secref{sec:proofterms}. Thus all three levels of @{text 

560 
"\<lambda>"}calculus become explicit: @{text "\<Rightarrow>"} for terms, and @{text 

561 
"\<And>/\<Longrightarrow>"} for proofs (cf.\ \cite{BerghoferNipkow:2000:TPHOL}). 

20491  562 

34929  563 
Observe that locally fixed parameters (as in @{text 
42666  564 
"\<And>\<hyphen>intro"}) need not be recorded in the hypotheses, because 
34929  565 
the simple syntactic types of Pure are always inhabitable. 
566 
``Assumptions'' @{text "x :: \<tau>"} for typemembership are only 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

567 
present as long as some @{text "x\<^sub>\<tau>"} occurs in the statement 
34929  568 
body.\footnote{This is the key difference to ``@{text "\<lambda>HOL"}'' in 
569 
the PTS framework \cite{BarendregtGeuvers:2001}, where hypotheses 

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

20501  571 

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

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

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

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

579 
\begin{figure}[htb] 

580 
\begin{center} 

20498  581 
\[ 
20501  582 
\infer{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}{@{text "\<Gamma> \<turnstile> B[\<alpha>]"} & @{text "\<alpha> \<notin> \<Gamma>"}} 
583 
\quad 

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

20498  585 
\] 
586 
\[ 

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

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

20498  590 
\] 
20501  591 
\caption{Admissible substitution rules}\label{fig:substrules} 
592 
\end{center} 

593 
\end{figure} 

18537  594 

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

597 
variables. 

598 

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

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

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

603 
the result belongs to a different proof context. 

20542  604 

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

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

608 
The system always records oracle invocations within derivations of 

29768  609 
theorems by a unique tag. 
20542  610 

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

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

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

20542  615 

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

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

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

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

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

20542  622 

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

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

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

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

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

628 
"d(\<alpha>\<^sub>i)"} for some @{text "\<alpha>\<^sub>i"} projected from @{text 
20543  629 
"\<^vec>\<alpha>"}. Thus overloaded definitions essentially work by 
630 
primitive recursion over the syntactic structure of a single type 

39840  631 
argument. See also \cite[\S4.3]{HaftmannWenzel:2006:classes}. 
20521  632 
*} 
20498  633 

20521  634 
text %mlref {* 
635 
\begin{mldecls} 

46253  636 
@{index_ML Logic.all: "term > term > term"} \\ 
637 
@{index_ML Logic.mk_implies: "term * term > term"} \\ 

638 
\end{mldecls} 

639 
\begin{mldecls} 

20521  640 
@{index_ML_type ctyp} \\ 
641 
@{index_ML_type cterm} \\ 

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

46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
46262
diff
changeset

644 
@{index_ML Thm.apply: "cterm > cterm > cterm"} \\ 
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
46262
diff
changeset

645 
@{index_ML Thm.lambda: "cterm > cterm > cterm"} \\ 
46253  646 
@{index_ML Thm.all: "cterm > cterm > cterm"} \\ 
647 
@{index_ML Drule.mk_implies: "cterm * cterm > cterm"} \\ 

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

20521  650 
@{index_ML_type thm} \\ 
50126
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
48985
diff
changeset

651 
@{index_ML Thm.peek_status: "thm > {oracle: bool, unfinished: bool, failed: bool}"} \\ 
42933  652 
@{index_ML Thm.transfer: "theory > thm > thm"} \\ 
20542  653 
@{index_ML Thm.assume: "cterm > thm"} \\ 
654 
@{index_ML Thm.forall_intr: "cterm > thm > thm"} \\ 

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

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

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

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

659 
@{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

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

661 
binding * term > theory > (string * thm) * theory"} \\ 
39821  662 
@{index_ML Thm.add_oracle: "binding * ('a > cterm) > theory > 
663 
(string * ('a > thm)) * theory"} \\ 

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

664 
@{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

665 
binding * term > theory > (string * thm) * theory"} \\ 
20547  666 
\end{mldecls} 
667 
\begin{mldecls} 

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

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

669 
string * typ > (string * typ) list > theory > theory"} \\ 
20521  670 
\end{mldecls} 
671 

672 
\begin{description} 

673 

50126
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
48985
diff
changeset

674 
\item @{ML Thm.peek_status}~@{text "thm"} informs about the current 
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
48985
diff
changeset

675 
status of the derivation object behind the given theorem. This is a 
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
48985
diff
changeset

676 
snapshot of a potentially ongoing (parallel) evaluation of proofs. 
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
48985
diff
changeset

677 
The three Boolean values indicate the following: @{verbatim oracle} 
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
48985
diff
changeset

678 
if the finished part contains some oracle invocation; @{verbatim 
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
48985
diff
changeset

679 
unfinished} if some future proofs are still pending; @{verbatim 
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
48985
diff
changeset

680 
failed} if some future proof has failed, rendering the theorem 
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
48985
diff
changeset

681 
invalid! 
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
48985
diff
changeset

682 

46253  683 
\item @{ML Logic.all}~@{text "a B"} produces a Pure quantification 
684 
@{text "\<And>a. B"}, where occurrences of the atomic term @{text "a"} in 

685 
the body proposition @{text "B"} are replaced by bound variables. 

686 
(See also @{ML lambda} on terms.) 

687 

688 
\item @{ML Logic.mk_implies}~@{text "(A, B)"} produces a Pure 

689 
implication @{text "A \<Longrightarrow> B"}. 

690 

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

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

46253  695 
constructors, constants etc.\ in the background theory. The 
696 
abstract types @{ML_type ctyp} and @{ML_type cterm} are part of the 

697 
same inference kernel that is mainly responsible for @{ML_type thm}. 

698 
Thus syntactic operations on @{ML_type ctyp} and @{ML_type cterm} 

699 
are located in the @{ML_struct Thm} module, even though theorems are 

700 
not yet involved at that stage. 

20542  701 

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

704 
respectively. This also involves some basic normalizations, such 

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

46253  706 
Full recertification is relatively slow and should be avoided in 
707 
tight reasoning loops. 

20547  708 

46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
46262
diff
changeset

709 
\item @{ML Thm.apply}, @{ML Thm.lambda}, @{ML Thm.all}, @{ML 
46253  710 
Drule.mk_implies} etc.\ compose certified terms (or propositions) 
711 
incrementally. This is equivalent to @{ML Thm.cterm_of} after 

46262  712 
unchecked @{ML_op "$"}, @{ML lambda}, @{ML Logic.all}, @{ML 
46253  713 
Logic.mk_implies} etc., but there can be a big difference in 
714 
performance when large existing entities are composed by a few extra 

715 
constructions on top. There are separate operations to decompose 

716 
certified terms and theorems to produce certified terms again. 

20542  717 

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

20542  720 
constructed by basic principles of the @{ML_struct Thm} module. 
52788  721 
Every @{ML_type thm} value refers its background theory, 
722 
cf.\ \secref{sec:contexttheory}. 

20542  723 

42933  724 
\item @{ML Thm.transfer}~@{text "thy thm"} transfers the given 
725 
theorem to a \emph{larger} theory, see also \secref{sec:context}. 

726 
This formal adjustment of the background context has no logical 

727 
significance, but is occasionally required for formal reasons, e.g.\ 

728 
when theorems that are imported from more basic theories are used in 

729 
the current situation. 

730 

20542  731 
\item @{ML Thm.assume}, @{ML Thm.forall_intr}, @{ML 
732 
Thm.forall_elim}, @{ML Thm.implies_intr}, and @{ML Thm.implies_elim} 

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

734 

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

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

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

739 
basic names. 

20521  740 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

741 
\item @{ML Thm.instantiate}~@{text "(\<^vec>\<alpha>\<^sub>s, 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

742 
\<^vec>x\<^sub>\<tau>)"} corresponds to the @{text "instantiate"} rules 
20542  743 
of \figref{fig:substrules}. Type variables are substituted before 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

744 
term variables. Note that the types in @{text "\<^vec>x\<^sub>\<tau>"} 
20542  745 
refer to the instantiated versions. 
746 

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

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

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

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

20542  752 

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

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

20521  756 

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

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

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

761 
lowlevel representation in the axiom table may differ slightly from 

762 
the returned theorem. 

20542  763 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

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

765 
declares dependencies of a named specification for constant @{text 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

766 
"c\<^sub>\<tau>"}, relative to existing specifications for constants @{text 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

767 
"\<^vec>d\<^sub>\<sigma>"}. 
20542  768 

20521  769 
\end{description} 
770 
*} 

771 

772 

39832  773 
text %mlantiq {* 
774 
\begin{matharray}{rcl} 

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

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

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

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

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

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

781 
\end{matharray} 

782 

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

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

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

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

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

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

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

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

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

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

796 
"} 
39832  797 

798 
\begin{description} 

799 

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

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

802 
ctyp}. 

803 

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

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

806 
value of type @{ML_type cterm}. 

807 

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

809 
value of type @{ML_type thm}. 

810 

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

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

813 

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

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

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

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

818 
given here. 

819 

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

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

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

823 

824 
Since ML antiquotations are always evaluated at compiletime, there 

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

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

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

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

829 
the result. 

830 

831 
\end{description} 

832 

833 
*} 

834 

835 

46254  836 
subsection {* Auxiliary connectives \label{sec:logicaux} *} 
20521  837 

46254  838 
text {* Theory @{text "Pure"} provides a few auxiliary connectives 
839 
that are defined on top of the primitive ones, see 

840 
\figref{fig:pureaux}. These special constants are useful in 

841 
certain internal encodings, and are normally not directly exposed to 

842 
the user. 

20501  843 

844 
\begin{figure}[htb] 

845 
\begin{center} 

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

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

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

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

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

20498  855 
\end{tabular} 
20521  856 
\caption{Definitions of auxiliary connectives}\label{fig:pureaux} 
20501  857 
\end{center} 
858 
\end{figure} 

859 

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

862 
available as derived rules. Conjunction allows to treat 

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

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

865 
represents multiple claims as explicit conjunction internally, but 

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

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

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

20537  869 
\secref{sec:tacticalgoals}). 
20498  870 

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

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

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

20521  875 

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

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

879 
uniformly, similar to a typetheoretic framework. 

20498  880 

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

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

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

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

889 
argument in primitive definitions, in order to circumvent hidden 

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

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

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

893 
argument, which is essentially a predicate on types. 

20521  894 
*} 
20501  895 

20521  896 
text %mlref {* 
897 
\begin{mldecls} 

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

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

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

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

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

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

904 
\end{mldecls} 

905 

906 
\begin{description} 

907 

34929  908 
\item @{ML Conjunction.intr} derives @{text "A &&& B"} from @{text 
20542  909 
"A"} and @{text "B"}. 
910 

20543  911 
\item @{ML Conjunction.elim} derives @{text "A"} and @{text "B"} 
34929  912 
from @{text "A &&& B"}. 
20542  913 

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

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

20542  918 

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

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

921 

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

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

20521  924 

925 
\end{description} 

20491  926 
*} 
18537  927 

20480  928 

52406  929 
subsection {* Sort hypotheses *} 
930 

931 
text {* Type variables are decorated with sorts, as explained in 

932 
\secref{sec:types}. This constrains type instantiation to certain 

933 
ranges of types: variable @{text "\<alpha>\<^sub>s"} may only be assigned to types 

934 
@{text "\<tau>"} that belong to sort @{text "s"}. Within the logic, sort 

935 
constraints act like implicit preconditions on the result @{text 

936 
"\<lparr>\<alpha>\<^sub>1 : s\<^sub>1\<rparr>, \<dots>, \<lparr>\<alpha>\<^sub>n : s\<^sub>n\<rparr>, \<Gamma> \<turnstile> \<phi>"} where the type variables @{text 

937 
"\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n"} cover the propositions @{text "\<Gamma>"}, @{text "\<phi>"}, as 

938 
well as the proof of @{text "\<Gamma> \<turnstile> \<phi>"}. 

939 

940 
These \emph{sort hypothesis} of a theorem are passed monotonically 

941 
through further derivations. They are redundant, as long as the 

942 
statement of a theorem still contains the type variables that are 

943 
accounted here. The logical significance of sort hypotheses is 

944 
limited to the boundary case where type variables disappear from the 

945 
proposition, e.g.\ @{text "\<lparr>\<alpha>\<^sub>s : s\<rparr> \<turnstile> \<phi>"}. Since such dangling type 

946 
variables can be renamed arbitrarily without changing the 

947 
proposition @{text "\<phi>"}, the inference kernel maintains sort 

948 
hypotheses in anonymous form @{text "s \<turnstile> \<phi>"}. 

949 

950 
In most practical situations, such extra sort hypotheses may be 

951 
stripped in a final bookkeeping step, e.g.\ at the end of a proof: 

952 
they are typically left over from intermediate reasoning with type 

953 
classes that can be satisfied by some concrete type @{text "\<tau>"} of 

954 
sort @{text "s"} to replace the hypothetical type variable @{text 

955 
"\<alpha>\<^sub>s"}. *} 

956 

957 
text %mlref {* 

958 
\begin{mldecls} 

959 
@{index_ML Thm.extra_shyps: "thm > sort list"} \\ 

960 
@{index_ML Thm.strip_shyps: "thm > thm"} \\ 

961 
\end{mldecls} 

962 

963 
\begin{description} 

964 

965 
\item @{ML Thm.extra_shyps}~@{text "thm"} determines the extraneous 

966 
sort hypotheses of the given theorem, i.e.\ the sorts that are not 

967 
present within type variables of the statement. 

968 

969 
\item @{ML Thm.strip_shyps}~@{text "thm"} removes any extraneous 

970 
sort hypotheses that can be witnessed from the type signature. 

971 

972 
\end{description} 

973 
*} 

974 

975 
text %mlex {* The following artificial example demonstrates the 

976 
derivation of @{prop False} with a pending sort hypothesis involving 

977 
a logically empty sort. *} 

978 

979 
class empty = 

980 
assumes bad: "\<And>(x::'a) y. x \<noteq> y" 

981 

982 
theorem (in empty) false: False 

983 
using bad by blast 

984 

985 
ML {* 

986 
@{assert} (Thm.extra_shyps @{thm false} = [@{sort empty}]) 

987 
*} 

988 

989 
text {* Thanks to the inference kernel managing sort hypothesis 

990 
according to their logical significance, this example is merely an 

991 
instance of \emph{ex falso quodlibet consequitur}  not a collapse 

992 
of the logical framework! *} 

993 

994 

28784  995 
section {* Objectlevel rules \label{sec:objrules} *} 
18537  996 

29768  997 
text {* 
998 
The primitive inferences covered so far mostly serve foundational 

999 
purposes. Userlevel reasoning usually works via objectlevel rules 

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

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

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

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

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

1006 
*} 
20491  1007 

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

1008 

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

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

1010 

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

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

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

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

1016 
\[ 

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

1018 
\] 

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

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

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

1022 
objectlevel inference corresponds to an iterated implication in 

1023 
Pure like this: 

1024 
\[ 

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

1026 
\] 

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

1027 
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

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

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

1031 
@{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  1032 
\] 
20491  1033 

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

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

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

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

1038 
inductive characterization as follows: 
29768  1039 

1040 
\medskip 

1041 
\begin{tabular}{ll} 

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

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

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

1045 
\end{tabular} 

1046 
\medskip 

1047 

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

1048 
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

1049 
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

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

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

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

34929  1055 
already marks the limit of rule complexity that is usually seen in 
1056 
practice. 

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

1057 

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

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

1060 

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

1061 
\begin{itemize} 
29768  1062 

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

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

1066 
Hereditary Harrop Formula. 

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

1067 

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

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

1072 
parameters, and vacuous quantifiers vanish automatically. 

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

1073 

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

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

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

1076 

29771  1077 
text %mlref {* 
1078 
\begin{mldecls} 

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

1079 
@{index_ML Simplifier.norm_hhf: "thm > thm"} \\ 
29771  1080 
\end{mldecls} 
1081 

1082 
\begin{description} 

1083 

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

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

1087 
handle Hereditary Harrop Formulae properly. 

1088 

1089 
\end{description} 

1090 
*} 

1091 

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

1092 

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

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

1094 

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

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

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

1099 
higherorder unification. There are also combined variants, notably 

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

20491  1101 

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

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

20498  1105 
\[ 
29771  1106 
\infer[(@{inference_def composition})]{@{text "\<^vec>A\<vartheta> \<Longrightarrow> C\<vartheta>"}} 
20498  1107 
{@{text "\<^vec>A \<Longrightarrow> B"} & @{text "B' \<Longrightarrow> C"} & @{text "B\<vartheta> = B'\<vartheta>"}} 
1108 
\] 

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

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

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

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

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

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

20498  1116 

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

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

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

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

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

1123 
by means of iterated application of the following inferences: 

20498  1124 
\[ 
29771  1125 
\infer[(@{inference_def imp_lift})]{@{text "(\<^vec>H \<Longrightarrow> \<^vec>A) \<Longrightarrow> (\<^vec>H \<Longrightarrow> B)"}}{@{text "\<^vec>A \<Longrightarrow> B"}} 
20498  1126 
\] 
1127 
\[ 

29771  1128 
\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  1129 
\] 
29771  1130 
By combining raw composition with lifting, we get full @{inference 
1131 
resolution} as follows: 

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

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

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

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

1139 
\end{tabular}} 

1140 
\] 

1141 

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

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

1145 
solved situation (again modulo unification): 

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

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

1149 
\] 

20498  1150 

52422  1151 
%FIXME @{inference_def elim_resolution}, @{inference_def dest_resolution} 
18537  1152 
*} 
1153 

29768  1154 
text %mlref {* 
1155 
\begin{mldecls} 

46262  1156 
@{index_ML_op "RSN": "thm * (int * thm) > thm"} \\ 
1157 
@{index_ML_op "RS": "thm * thm > thm"} \\ 

46256  1158 

46262  1159 
@{index_ML_op "RLN": "thm list * (int * thm list) > thm list"} \\ 
1160 
@{index_ML_op "RL": "thm list * thm list > thm list"} \\ 

46256  1161 

46262  1162 
@{index_ML_op "MRS": "thm list * thm > thm"} \\ 
1163 
@{index_ML_op "OF": "thm * thm list > thm"} \\ 

29768  1164 
\end{mldecls} 
1165 

1166 
\begin{description} 

1167 

46256  1168 
\item @{text "rule\<^sub>1 RSN (i, rule\<^sub>2)"} resolves the conclusion of 
1169 
@{text "rule\<^sub>1"} with the @{text i}th premise of @{text "rule\<^sub>2"}, 

1170 
according to the @{inference resolution} principle explained above. 

1171 
Unless there is precisely one resolvent it raises exception @{ML 

1172 
THM}. 

1173 

1174 
This corresponds to the rule attribute @{attribute THEN} in Isar 

1175 
source language. 

1176 

1177 
\item @{text "rule\<^sub>1 RS rule\<^sub>2"} abbreviates @{text "rule\<^sub>1 RS (1, 

1178 
rule\<^sub>2)"}. 

29768  1179 

46256  1180 
\item @{text "rules\<^sub>1 RLN (i, rules\<^sub>2)"} joins lists of rules. For 
1181 
every @{text "rule\<^sub>1"} in @{text "rules\<^sub>1"} and @{text "rule\<^sub>2"} in 

1182 
@{text "rules\<^sub>2"}, it resolves the conclusion of @{text "rule\<^sub>1"} with 

1183 
the @{text "i"}th premise of @{text "rule\<^sub>2"}, accumulating multiple 

1184 
results in one big list. Note that such strict enumerations of 

1185 
higherorder unifications can be inefficient compared to the lazy 

1186 
variant seen in elementary tactics like @{ML resolve_tac}. 

1187 

1188 
\item @{text "rules\<^sub>1 RL rules\<^sub>2"} abbreviates @{text "rules\<^sub>1 RLN (1, 

1189 
rules\<^sub>2)"}. 

1190 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52788
diff
changeset

1191 
\item @{text "[rule\<^sub>1, \<dots>, rule\<^sub>n] MRS rule"} resolves @{text "rule\<^sub>i"} 
46256  1192 
against premise @{text "i"} of @{text "rule"}, for @{text "i = n, \<dots>, 
1193 
1"}. By working from right to left, newly emerging premises are 
