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

doc-src/IsarImplementation/Thy/logic.thy

changeset 20491 | 98ba42f19995 |

parent 20480 | 4e0522d38968 |

child 20493 | 48fea5e99505 |

1.1 --- a/doc-src/IsarImplementation/Thy/logic.thy Thu Sep 07 15:16:51 2006 +0200 1.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy Thu Sep 07 20:12:08 2006 +0200 1.3 @@ -11,7 +11,8 @@ 1.4 \cite{paulson700}. This is essentially the same logic as ``@{text 1.5 "\<lambda>HOL"}'' in the more abstract framework of Pure Type Systems (PTS) 1.6 \cite{Barendregt-Geuvers:2001}, although there are some key 1.7 - differences in the practical treatment of simple types. 1.8 + differences in the specific treatment of simple types in 1.9 + Isabelle/Pure. 1.10 1.11 Following type-theoretic parlance, the Pure logic consists of three 1.12 levels of @{text "\<lambda>"}-calculus with corresponding arrows: @{text 1.13 @@ -20,8 +21,11 @@ 1.14 @{text "\<Longrightarrow>"} for implication (proofs depending on proofs). 1.15 1.16 Pure derivations are relative to a logical theory, which declares 1.17 - type constructors, term constants, and axioms. Term constants and 1.18 - axioms support schematic polymorphism. 1.19 + type constructors, term constants, and axioms. Theory declarations 1.20 + support schematic polymorphism, which is strictly speaking outside 1.21 + the logic.\footnote{Incidently, this is the main logical reason, why 1.22 + the theory context @{text "\<Theta>"} is separate from the context @{text 1.23 + "\<Gamma>"} of the core calculus.} 1.24 *} 1.25 1.26 1.27 @@ -34,46 +38,48 @@ 1.28 \medskip A \emph{type class} is an abstract syntactic entity 1.29 declared in the theory context. The \emph{subclass relation} @{text 1.30 "c\<^isub>1 \<subseteq> c\<^isub>2"} is specified by stating an acyclic 1.31 - generating relation; the transitive closure maintained internally. 1.32 + generating relation; the transitive closure is maintained 1.33 + internally. The resulting relation is an ordering: reflexive, 1.34 + transitive, and antisymmetric. 1.35 1.36 A \emph{sort} is a list of type classes written as @{text 1.37 "{c\<^isub>1, \<dots>, c\<^isub>m}"}, which represents symbolic 1.38 intersection. Notationally, the curly braces are omitted for 1.39 singleton intersections, i.e.\ any class @{text "c"} may be read as 1.40 a sort @{text "{c}"}. The ordering on type classes is extended to 1.41 - sorts in the canonical fashion: @{text "{c\<^isub>1, \<dots> c\<^isub>m} \<subseteq> 1.42 - {d\<^isub>1, \<dots>, d\<^isub>n}"} iff @{text "\<forall>j. \<exists>i. c\<^isub>i \<subseteq> 1.43 - d\<^isub>j"}. The empty intersection @{text "{}"} refers to the 1.44 - universal sort, which is the largest element wrt.\ the sort order. 1.45 - The intersections of all (i.e.\ finitely many) classes declared in 1.46 - the current theory are the minimal elements wrt.\ sort order. 1.47 + sorts according to the meaning of intersections: @{text 1.48 + "{c\<^isub>1, \<dots> c\<^isub>m} \<subseteq> {d\<^isub>1, \<dots>, d\<^isub>n}"} iff 1.49 + @{text "\<forall>j. \<exists>i. c\<^isub>i \<subseteq> d\<^isub>j"}. The empty intersection 1.50 + @{text "{}"} refers to the universal sort, which is the largest 1.51 + element wrt.\ the sort order. The intersections of all (finitely 1.52 + many) classes declared in the current theory are the minimal 1.53 + elements wrt.\ the sort order. 1.54 1.55 - \medskip A \emph{fixed type variable} is pair of a basic name 1.56 + \medskip A \emph{fixed type variable} is a pair of a basic name 1.57 (starting with @{text "'"} character) and a sort constraint. For 1.58 example, @{text "('a, s)"} which is usually printed as @{text 1.59 "\<alpha>\<^isub>s"}. A \emph{schematic type variable} is a pair of an 1.60 indexname and a sort constraint. For example, @{text "(('a, 0), 1.61 - s)"} which is usually printed @{text "?\<alpha>\<^isub>s"}. 1.62 + s)"} which is usually printed as @{text "?\<alpha>\<^isub>s"}. 1.63 1.64 Note that \emph{all} syntactic components contribute to the identity 1.65 - of a type variables, including the literal sort constraint. The 1.66 - core logic handles type variables with the same name but different 1.67 - sorts as different, even though the outer layers of the system make 1.68 - it hard to produce anything like this. 1.69 + of type variables, including the literal sort constraint. The core 1.70 + logic handles type variables with the same name but different sorts 1.71 + as different, although some outer layers of the system make it hard 1.72 + to produce anything like this. 1.73 1.74 - A \emph{type constructor} is an @{text "k"}-ary type operator 1.75 - declared in the theory. 1.76 + A \emph{type constructor} is a @{text "k"}-ary operator on types 1.77 + declared in the theory. Type constructor application is usually 1.78 + written postfix. For @{text "k = 0"} the argument tuple is omitted, 1.79 + e.g.\ @{text "prop"} instead of @{text "()prop"}. For @{text "k = 1.80 + 1"} the parentheses are omitted, e.g.\ @{text "\<alpha> list"} instead of 1.81 + @{text "(\<alpha>)list"}. Further notation is provided for specific 1.82 + constructors, notably right-associative infix @{text "\<alpha> \<Rightarrow> \<beta>"} 1.83 + instead of @{text "(\<alpha>, \<beta>)fun"} constructor. 1.84 1.85 A \emph{type} is defined inductively over type variables and type 1.86 - constructors: @{text "\<tau> = \<alpha>\<^isub>s | ?\<alpha>\<^isub>s | (\<tau>\<^sub>1, \<dots>, 1.87 - \<tau>\<^sub>k)c"}. Type constructor application is usually written 1.88 - postfix. For @{text "k = 0"} the argument tuple is omitted, e.g.\ 1.89 - @{text "prop"} instead of @{text "()prop"}. For @{text "k = 1"} the 1.90 - parentheses are omitted, e.g.\ @{text "\<tau> list"} instead of @{text 1.91 - "(\<tau>) list"}. Further notation is provided for specific 1.92 - constructors, notably right-associative infix @{text "\<tau>\<^isub>1 \<Rightarrow> 1.93 - \<tau>\<^isub>2"} instead of @{text "(\<tau>\<^isub>1, \<tau>\<^isub>2)fun"} 1.94 - constructor. 1.95 + constructors as follows: @{text "\<tau> = \<alpha>\<^isub>s | ?\<alpha>\<^isub>s | 1.96 + (\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)c"}. 1.97 1.98 A \emph{type abbreviation} is a syntactic abbreviation of an 1.99 arbitrary type expression of the theory. Type abbreviations looks 1.100 @@ -82,26 +88,30 @@ 1.101 1.102 A \emph{type arity} declares the image behavior of a type 1.103 constructor wrt.\ the algebra of sorts: @{text "c :: (s\<^isub>1, \<dots>, 1.104 - s\<^isub>n)s"} means that @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>k)c"} is 1.105 + s\<^isub>k)s"} means that @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>k)c"} is 1.106 of sort @{text "s"} if each argument type @{text "\<tau>\<^isub>i"} is of 1.107 - sort @{text "s\<^isub>i"}. The sort algebra is always maintained as 1.108 - \emph{coregular}, which means that type arities are consistent with 1.109 - the subclass relation: for each type constructor @{text "c"} and 1.110 - classes @{text "c\<^isub>1 \<subseteq> c\<^isub>2"}, any arity @{text "c :: 1.111 + sort @{text "s\<^isub>i"}. Arity declarations are implicitly 1.112 + completed, i.e.\ @{text "c :: (\<^vec>s)c"} entails @{text "c :: 1.113 + (\<^vec>s)c'"} for any @{text "c' \<supseteq> c"}. 1.114 + 1.115 + \medskip The sort algebra is always maintained as \emph{coregular}, 1.116 + which means that type arities are consistent with the subclass 1.117 + relation: for each type constructor @{text "c"} and classes @{text 1.118 + "c\<^isub>1 \<subseteq> c\<^isub>2"}, any arity @{text "c :: 1.119 (\<^vec>s\<^isub>1)c\<^isub>1"} has a corresponding arity @{text "c 1.120 :: (\<^vec>s\<^isub>2)c\<^isub>2"} where @{text "\<^vec>s\<^isub>1 \<subseteq> 1.121 \<^vec>s\<^isub>2"} holds pointwise for all argument sorts. 1.122 1.123 - The key property of the order-sorted algebra of types is that sort 1.124 + The key property of a coregular order-sorted algebra is that sort 1.125 constraints may be always fulfilled in a most general fashion: for 1.126 each type constructor @{text "c"} and sort @{text "s"} there is a 1.127 most general vector of argument sorts @{text "(s\<^isub>1, \<dots>, 1.128 - s\<^isub>k)"} such that @{text "(\<tau>\<^bsub>s\<^isub>1\<^esub>, \<dots>, 1.129 - \<tau>\<^bsub>s\<^isub>k\<^esub>)"} for arbitrary @{text "\<tau>\<^isub>i"} of 1.130 - sort @{text "s\<^isub>i"}. This means the unification problem on 1.131 - the algebra of types has most general solutions (modulo renaming and 1.132 - equivalence of sorts). As a consequence, type-inference is able to 1.133 - produce primary types. 1.134 + s\<^isub>k)"} such that a type scheme @{text 1.135 + "(\<alpha>\<^bsub>s\<^isub>1\<^esub>, \<dots>, \<alpha>\<^bsub>s\<^isub>k\<^esub>)c"} is 1.136 + of sort @{text "s"}. Consequently, the unification problem on the 1.137 + algebra of types has most general solutions (modulo renaming and 1.138 + equivalence of sorts). Moreover, the usual type-inference algorithm 1.139 + will produce primary types as expected \cite{nipkow-prehofer}. 1.140 *} 1.141 1.142 text %mlref {* 1.143 @@ -139,19 +149,19 @@ 1.144 tests the subsort relation @{text "s\<^isub>1 \<subseteq> s\<^isub>2"}. 1.145 1.146 \item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether a type 1.147 - expression of of a given sort. 1.148 + is of a given sort. 1.149 1.150 \item @{ML Sign.add_types}~@{text "[(c, k, mx), \<dots>]"} declares new 1.151 - type constructors @{text "c"} with @{text "k"} arguments, and 1.152 + type constructors @{text "c"} with @{text "k"} arguments and 1.153 optional mixfix syntax. 1.154 1.155 \item @{ML Sign.add_tyabbrs_i}~@{text "[(c, \<^vec>\<alpha>, \<tau>, mx), \<dots>]"} 1.156 - defines type abbreviation @{text "(\<^vec>\<alpha>)c"} (with optional 1.157 - mixfix syntax) as @{text "\<tau>"}. 1.158 + defines a new type abbreviation @{text "(\<^vec>\<alpha>)c = \<tau>"} with 1.159 + optional mixfix syntax. 1.160 1.161 \item @{ML Sign.primitive_class}~@{text "(c, [c\<^isub>1, \<dots>, 1.162 c\<^isub>n])"} declares new class @{text "c"} derived together with 1.163 - class relations @{text "c \<subseteq> c\<^isub>i"}. 1.164 + class relations @{text "c \<subseteq> c\<^isub>i"}, for @{text "i = 1, \<dots>, n"}. 1.165 1.166 \item @{ML Sign.primitive_classrel}~@{text "(c\<^isub>1, 1.167 c\<^isub>2)"} declares class relation @{text "c\<^isub>1 \<subseteq> 1.168 @@ -170,6 +180,13 @@ 1.169 text {* 1.170 \glossary{Term}{FIXME} 1.171 1.172 + The language of terms is that of simply-typed @{text "\<lambda>"}-calculus 1.173 + with de-Bruijn indices for bound variables, and named free 1.174 + variables, and constants. Terms with loose bound variables are 1.175 + usually considered malformed. The types of variables and constants 1.176 + is stored explicitly at each occurrence in the term (which is a 1.177 + known performance issue). 1.178 + 1.179 FIXME de-Bruijn representation of lambda terms 1.180 1.181 Term syntax provides explicit abstraction @{text "\<lambda>x :: \<alpha>. b(x)"} 1.182 @@ -193,13 +210,6 @@ 1.183 *} 1.184 1.185 1.186 -section {* Proof terms *} 1.187 - 1.188 -text {* 1.189 - FIXME 1.190 -*} 1.191 - 1.192 - 1.193 section {* Theorems \label{sec:thms} *} 1.194 1.195 text {* 1.196 @@ -258,17 +268,54 @@ 1.197 1.198 *} 1.199 1.200 -subsection {* Primitive inferences *} 1.201 + 1.202 +section {* Proof terms *} 1.203 1.204 -text FIXME 1.205 +text {* 1.206 + FIXME !? 1.207 +*} 1.208 1.209 1.210 -subsection {* Higher-order resolution *} 1.211 +section {* Rules \label{sec:rules} *} 1.212 1.213 text {* 1.214 1.215 FIXME 1.216 1.217 + A \emph{rule} is any Pure theorem in HHF normal form; there is a 1.218 + separate calculus for rule composition, which is modeled after 1.219 + Gentzen's Natural Deduction \cite{Gentzen:1935}, but allows 1.220 + rules to be nested arbitrarily, similar to \cite{extensions91}. 1.221 + 1.222 + Normally, all theorems accessible to the user are proper rules. 1.223 + Low-level inferences are occasional required internally, but the 1.224 + result should be always presented in canonical form. The higher 1.225 + interfaces of Isabelle/Isar will always produce proper rules. It is 1.226 + important to maintain this invariant in add-on applications! 1.227 + 1.228 + There are two main principles of rule composition: @{text 1.229 + "resolution"} (i.e.\ backchaining of rules) and @{text 1.230 + "by-assumption"} (i.e.\ closing a branch); both principles are 1.231 + combined in the variants of @{text "elim-resosultion"} and @{text 1.232 + "dest-resolution"}. Raw @{text "composition"} is occasionally 1.233 + useful as well, also it is strictly speaking outside of the proper 1.234 + rule calculus. 1.235 + 1.236 + Rules are treated modulo general higher-order unification, which is 1.237 + unification modulo the equational theory of @{text "\<alpha>\<beta>\<eta>"}-conversion 1.238 + on @{text "\<lambda>"}-terms. Moreover, propositions are understood modulo 1.239 + the (derived) equivalence @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}. 1.240 + 1.241 + This means that any operations within the rule calculus may be 1.242 + subject to spontaneous @{text "\<alpha>\<beta>\<eta>"}-HHF conversions. It is common 1.243 + practice not to contract or expand unnecessarily. Some mechanisms 1.244 + prefer an one form, others the opposite, so there is a potential 1.245 + danger to produce some oscillation! 1.246 + 1.247 + Only few operations really work \emph{modulo} HHF conversion, but 1.248 + expect a normal form: quantifiers @{text "\<And>"} before implications 1.249 + @{text "\<Longrightarrow>"} at each level of nesting. 1.250 + 1.251 \glossary{Hereditary Harrop Formula}{The set of propositions in HHF 1.252 format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow> 1.253 A)"}, for variables @{text "x"} and atomic propositions @{text "A"}. 1.254 @@ -282,9 +329,4 @@ 1.255 1.256 *} 1.257 1.258 -subsection {* Equational reasoning *} 1.259 - 1.260 -text FIXME 1.261 - 1.262 - 1.263 end