author | wenzelm |

Thu Sep 07 20:12:08 2006 +0200 (2006-09-07 ago) | |

changeset 20491 | 98ba42f19995 |

parent 20490 | e502690952be |

child 20492 | c9bfc874488c |

tuned;

1.1 --- a/doc-src/IsarImplementation/Thy/ML.thy Thu Sep 07 15:16:51 2006 +0200 1.2 +++ b/doc-src/IsarImplementation/Thy/ML.thy Thu Sep 07 20:12:08 2006 +0200 1.3 @@ -18,7 +18,7 @@ 1.4 1.5 chapter {* Cookbook *} 1.6 1.7 -section {* Defining a method that depends on declarations in the context *} 1.8 +section {* A method that depends on declarations in the context *} 1.9 1.10 text FIXME 1.11

2.1 --- a/doc-src/IsarImplementation/Thy/document/ML.tex Thu Sep 07 15:16:51 2006 +0200 2.2 +++ b/doc-src/IsarImplementation/Thy/document/ML.tex Thu Sep 07 20:12:08 2006 +0200 2.3 @@ -43,7 +43,7 @@ 2.4 } 2.5 \isamarkuptrue% 2.6 % 2.7 -\isamarkupsection{Defining a method that depends on declarations in the context% 2.8 +\isamarkupsection{A method that depends on declarations in the context% 2.9 } 2.10 \isamarkuptrue% 2.11 %

3.1 --- a/doc-src/IsarImplementation/Thy/document/integration.tex Thu Sep 07 15:16:51 2006 +0200 3.2 +++ b/doc-src/IsarImplementation/Thy/document/integration.tex Thu Sep 07 20:12:08 2006 +0200 3.3 @@ -510,15 +510,6 @@ 3.4 % 3.5 \endisadelimmlref 3.6 % 3.7 -\isamarkupsection{Sessions and document preparation% 3.8 -} 3.9 -\isamarkuptrue% 3.10 -% 3.11 -\begin{isamarkuptext}% 3.12 -FIXME% 3.13 -\end{isamarkuptext}% 3.14 -\isamarkuptrue% 3.15 -% 3.16 \isadelimtheory 3.17 % 3.18 \endisadelimtheory

4.1 --- a/doc-src/IsarImplementation/Thy/document/logic.tex Thu Sep 07 15:16:51 2006 +0200 4.2 +++ b/doc-src/IsarImplementation/Thy/document/logic.tex Thu Sep 07 20:12:08 2006 +0200 4.3 @@ -28,15 +28,18 @@ 4.4 which has been introduced as a natural-deduction framework in 4.5 \cite{paulson700}. This is essentially the same logic as ``\isa{{\isasymlambda}HOL}'' in the more abstract framework of Pure Type Systems (PTS) 4.6 \cite{Barendregt-Geuvers:2001}, although there are some key 4.7 - differences in the practical treatment of simple types. 4.8 + differences in the specific treatment of simple types in 4.9 + Isabelle/Pure. 4.10 4.11 Following type-theoretic parlance, the Pure logic consists of three 4.12 levels of \isa{{\isasymlambda}}-calculus with corresponding arrows: \isa{{\isasymRightarrow}} for syntactic function space (terms depending on terms), \isa{{\isasymAnd}} for universal quantification (proofs depending on terms), and 4.13 \isa{{\isasymLongrightarrow}} for implication (proofs depending on proofs). 4.14 4.15 Pure derivations are relative to a logical theory, which declares 4.16 - type constructors, term constants, and axioms. Term constants and 4.17 - axioms support schematic polymorphism.% 4.18 + type constructors, term constants, and axioms. Theory declarations 4.19 + support schematic polymorphism, which is strictly speaking outside 4.20 + the logic.\footnote{Incidently, this is the main logical reason, why 4.21 + the theory context \isa{{\isasymTheta}} is separate from the context \isa{{\isasymGamma}} of the core calculus.}% 4.22 \end{isamarkuptext}% 4.23 \isamarkuptrue% 4.24 % 4.25 @@ -50,38 +53,42 @@ 4.26 4.27 \medskip A \emph{type class} is an abstract syntactic entity 4.28 declared in the theory context. The \emph{subclass relation} \isa{c\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlisub {\isadigit{2}}} is specified by stating an acyclic 4.29 - generating relation; the transitive closure maintained internally. 4.30 + generating relation; the transitive closure is maintained 4.31 + internally. The resulting relation is an ordering: reflexive, 4.32 + transitive, and antisymmetric. 4.33 4.34 A \emph{sort} is a list of type classes written as \isa{{\isacharbraceleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlisub m{\isacharbraceright}}, which represents symbolic 4.35 intersection. Notationally, the curly braces are omitted for 4.36 singleton intersections, i.e.\ any class \isa{c} may be read as 4.37 a sort \isa{{\isacharbraceleft}c{\isacharbraceright}}. The ordering on type classes is extended to 4.38 - sorts in the canonical fashion: \isa{{\isacharbraceleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}\ c\isactrlisub m{\isacharbraceright}\ {\isasymsubseteq}\ {\isacharbraceleft}d\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ d\isactrlisub n{\isacharbraceright}} iff \isa{{\isasymforall}j{\isachardot}\ {\isasymexists}i{\isachardot}\ c\isactrlisub i\ {\isasymsubseteq}\ d\isactrlisub j}. The empty intersection \isa{{\isacharbraceleft}{\isacharbraceright}} refers to the 4.39 - universal sort, which is the largest element wrt.\ the sort order. 4.40 - The intersections of all (i.e.\ finitely many) classes declared in 4.41 - the current theory are the minimal elements wrt.\ sort order. 4.42 + sorts according to the meaning of intersections: \isa{{\isacharbraceleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}\ c\isactrlisub m{\isacharbraceright}\ {\isasymsubseteq}\ {\isacharbraceleft}d\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ d\isactrlisub n{\isacharbraceright}} iff 4.43 + \isa{{\isasymforall}j{\isachardot}\ {\isasymexists}i{\isachardot}\ c\isactrlisub i\ {\isasymsubseteq}\ d\isactrlisub j}. The empty intersection 4.44 + \isa{{\isacharbraceleft}{\isacharbraceright}} refers to the universal sort, which is the largest 4.45 + element wrt.\ the sort order. The intersections of all (finitely 4.46 + many) classes declared in the current theory are the minimal 4.47 + elements wrt.\ the sort order. 4.48 4.49 - \medskip A \emph{fixed type variable} is pair of a basic name 4.50 + \medskip A \emph{fixed type variable} is a pair of a basic name 4.51 (starting with \isa{{\isacharprime}} character) and a sort constraint. For 4.52 example, \isa{{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ s{\isacharparenright}} which is usually printed as \isa{{\isasymalpha}\isactrlisub s}. A \emph{schematic type variable} is a pair of an 4.53 - indexname and a sort constraint. For example, \isa{{\isacharparenleft}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}{\isacharcomma}\ s{\isacharparenright}} which is usually printed \isa{{\isacharquery}{\isasymalpha}\isactrlisub s}. 4.54 + indexname and a sort constraint. For example, \isa{{\isacharparenleft}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}{\isacharcomma}\ s{\isacharparenright}} which is usually printed as \isa{{\isacharquery}{\isasymalpha}\isactrlisub s}. 4.55 4.56 Note that \emph{all} syntactic components contribute to the identity 4.57 - of a type variables, including the literal sort constraint. The 4.58 - core logic handles type variables with the same name but different 4.59 - sorts as different, even though the outer layers of the system make 4.60 - it hard to produce anything like this. 4.61 + of type variables, including the literal sort constraint. The core 4.62 + logic handles type variables with the same name but different sorts 4.63 + as different, although some outer layers of the system make it hard 4.64 + to produce anything like this. 4.65 4.66 - A \emph{type constructor} is an \isa{k}-ary type operator 4.67 - declared in the theory. 4.68 + A \emph{type constructor} is a \isa{k}-ary operator on types 4.69 + declared in the theory. Type constructor application is usually 4.70 + written postfix. For \isa{k\ {\isacharequal}\ {\isadigit{0}}} the argument tuple is omitted, 4.71 + e.g.\ \isa{prop} instead of \isa{{\isacharparenleft}{\isacharparenright}prop}. For \isa{k\ {\isacharequal}\ {\isadigit{1}}} the parentheses are omitted, e.g.\ \isa{{\isasymalpha}\ list} instead of 4.72 + \isa{{\isacharparenleft}{\isasymalpha}{\isacharparenright}list}. Further notation is provided for specific 4.73 + constructors, notably right-associative infix \isa{{\isasymalpha}\ {\isasymRightarrow}\ {\isasymbeta}} 4.74 + instead of \isa{{\isacharparenleft}{\isasymalpha}{\isacharcomma}\ {\isasymbeta}{\isacharparenright}fun} constructor. 4.75 4.76 A \emph{type} is defined inductively over type variables and type 4.77 - constructors: \isa{{\isasymtau}\ {\isacharequal}\ {\isasymalpha}\isactrlisub s\ {\isacharbar}\ {\isacharquery}{\isasymalpha}\isactrlisub s\ {\isacharbar}\ {\isacharparenleft}{\isasymtau}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlsub k{\isacharparenright}c}. Type constructor application is usually written 4.78 - postfix. For \isa{k\ {\isacharequal}\ {\isadigit{0}}} the argument tuple is omitted, e.g.\ 4.79 - \isa{prop} instead of \isa{{\isacharparenleft}{\isacharparenright}prop}. For \isa{k\ {\isacharequal}\ {\isadigit{1}}} the 4.80 - parentheses are omitted, e.g.\ \isa{{\isasymtau}\ list} instead of \isa{{\isacharparenleft}{\isasymtau}{\isacharparenright}\ list}. Further notation is provided for specific 4.81 - constructors, notably right-associative infix \isa{{\isasymtau}\isactrlisub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymtau}\isactrlisub {\isadigit{2}}} instead of \isa{{\isacharparenleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymtau}\isactrlisub {\isadigit{2}}{\isacharparenright}fun} 4.82 - constructor. 4.83 + constructors as follows: \isa{{\isasymtau}\ {\isacharequal}\ {\isasymalpha}\isactrlisub s\ {\isacharbar}\ {\isacharquery}{\isasymalpha}\isactrlisub s\ {\isacharbar}\ {\isacharparenleft}{\isasymtau}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlsub k{\isacharparenright}c}. 4.84 4.85 A \emph{type abbreviation} is a syntactic abbreviation of an 4.86 arbitrary type expression of the theory. Type abbreviations looks 4.87 @@ -89,21 +96,23 @@ 4.88 core logic encounters them. 4.89 4.90 A \emph{type arity} declares the image behavior of a type 4.91 - constructor wrt.\ the algebra of sorts: \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlisub n{\isacharparenright}s} means that \isa{{\isacharparenleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub k{\isacharparenright}c} is 4.92 + constructor wrt.\ the algebra of sorts: \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlisub k{\isacharparenright}s} means that \isa{{\isacharparenleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub k{\isacharparenright}c} is 4.93 of sort \isa{s} if each argument type \isa{{\isasymtau}\isactrlisub i} is of 4.94 - sort \isa{s\isactrlisub i}. The sort algebra is always maintained as 4.95 - \emph{coregular}, which means that type arities are consistent with 4.96 - the subclass relation: for each type constructor \isa{c} and 4.97 - classes \isa{c\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlisub {\isadigit{2}}}, any arity \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlisub {\isadigit{1}}{\isacharparenright}c\isactrlisub {\isadigit{1}}} has a corresponding arity \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlisub {\isadigit{2}}{\isacharparenright}c\isactrlisub {\isadigit{2}}} where \isa{\isactrlvec s\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ \isactrlvec s\isactrlisub {\isadigit{2}}} holds pointwise for all argument sorts. 4.98 + sort \isa{s\isactrlisub i}. Arity declarations are implicitly 4.99 + completed, i.e.\ \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c} entails \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isacharprime}} for any \isa{c{\isacharprime}\ {\isasymsupseteq}\ c}. 4.100 4.101 - The key property of the order-sorted algebra of types is that sort 4.102 + \medskip The sort algebra is always maintained as \emph{coregular}, 4.103 + which means that type arities are consistent with the subclass 4.104 + relation: for each type constructor \isa{c} and classes \isa{c\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlisub {\isadigit{2}}}, any arity \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlisub {\isadigit{1}}{\isacharparenright}c\isactrlisub {\isadigit{1}}} has a corresponding arity \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlisub {\isadigit{2}}{\isacharparenright}c\isactrlisub {\isadigit{2}}} where \isa{\isactrlvec s\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ \isactrlvec s\isactrlisub {\isadigit{2}}} holds pointwise for all argument sorts. 4.105 + 4.106 + The key property of a coregular order-sorted algebra is that sort 4.107 constraints may be always fulfilled in a most general fashion: for 4.108 each type constructor \isa{c} and sort \isa{s} there is a 4.109 - most general vector of argument sorts \isa{{\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlisub k{\isacharparenright}} such that \isa{{\isacharparenleft}{\isasymtau}\isactrlbsub s\isactrlisub {\isadigit{1}}\isactrlesub {\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlbsub s\isactrlisub k\isactrlesub {\isacharparenright}} for arbitrary \isa{{\isasymtau}\isactrlisub i} of 4.110 - sort \isa{s\isactrlisub i}. This means the unification problem on 4.111 - the algebra of types has most general solutions (modulo renaming and 4.112 - equivalence of sorts). As a consequence, type-inference is able to 4.113 - produce primary types.% 4.114 + most general vector of argument sorts \isa{{\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlisub k{\isacharparenright}} such that a type scheme \isa{{\isacharparenleft}{\isasymalpha}\isactrlbsub s\isactrlisub {\isadigit{1}}\isactrlesub {\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlbsub s\isactrlisub k\isactrlesub {\isacharparenright}c} is 4.115 + of sort \isa{s}. Consequently, the unification problem on the 4.116 + algebra of types has most general solutions (modulo renaming and 4.117 + equivalence of sorts). Moreover, the usual type-inference algorithm 4.118 + will produce primary types as expected \cite{nipkow-prehofer}.% 4.119 \end{isamarkuptext}% 4.120 \isamarkuptrue% 4.121 % 4.122 @@ -147,18 +156,18 @@ 4.123 tests the subsort relation \isa{s\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ s\isactrlisub {\isadigit{2}}}. 4.124 4.125 \item \verb|Sign.of_sort|~\isa{thy\ {\isacharparenleft}{\isasymtau}{\isacharcomma}\ s{\isacharparenright}} tests whether a type 4.126 - expression of of a given sort. 4.127 + is of a given sort. 4.128 4.129 \item \verb|Sign.add_types|~\isa{{\isacharbrackleft}{\isacharparenleft}c{\isacharcomma}\ k{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} declares new 4.130 - type constructors \isa{c} with \isa{k} arguments, and 4.131 + type constructors \isa{c} with \isa{k} arguments and 4.132 optional mixfix syntax. 4.133 4.134 \item \verb|Sign.add_tyabbrs_i|~\isa{{\isacharbrackleft}{\isacharparenleft}c{\isacharcomma}\ \isactrlvec {\isasymalpha}{\isacharcomma}\ {\isasymtau}{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} 4.135 - defines type abbreviation \isa{{\isacharparenleft}\isactrlvec {\isasymalpha}{\isacharparenright}c} (with optional 4.136 - mixfix syntax) as \isa{{\isasymtau}}. 4.137 + defines a new type abbreviation \isa{{\isacharparenleft}\isactrlvec {\isasymalpha}{\isacharparenright}c\ {\isacharequal}\ {\isasymtau}} with 4.138 + optional mixfix syntax. 4.139 4.140 \item \verb|Sign.primitive_class|~\isa{{\isacharparenleft}c{\isacharcomma}\ {\isacharbrackleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlisub n{\isacharbrackright}{\isacharparenright}} declares new class \isa{c} derived together with 4.141 - class relations \isa{c\ {\isasymsubseteq}\ c\isactrlisub i}. 4.142 + class relations \isa{c\ {\isasymsubseteq}\ c\isactrlisub i}, for \isa{i\ {\isacharequal}\ {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ n}. 4.143 4.144 \item \verb|Sign.primitive_classrel|~\isa{{\isacharparenleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ c\isactrlisub {\isadigit{2}}{\isacharparenright}} declares class relation \isa{c\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlisub {\isadigit{2}}}. 4.145 4.146 @@ -183,6 +192,13 @@ 4.147 \begin{isamarkuptext}% 4.148 \glossary{Term}{FIXME} 4.149 4.150 + The language of terms is that of simply-typed \isa{{\isasymlambda}}-calculus 4.151 + with de-Bruijn indices for bound variables, and named free 4.152 + variables, and constants. Terms with loose bound variables are 4.153 + usually considered malformed. The types of variables and constants 4.154 + is stored explicitly at each occurrence in the term (which is a 4.155 + known performance issue). 4.156 + 4.157 FIXME de-Bruijn representation of lambda terms 4.158 4.159 Term syntax provides explicit abstraction \isa{{\isasymlambda}x\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}{\isachardot}\ b{\isacharparenleft}x{\isacharparenright}} 4.160 @@ -203,15 +219,6 @@ 4.161 \end{isamarkuptext}% 4.162 \isamarkuptrue% 4.163 % 4.164 -\isamarkupsection{Proof terms% 4.165 -} 4.166 -\isamarkuptrue% 4.167 -% 4.168 -\begin{isamarkuptext}% 4.169 -FIXME% 4.170 -\end{isamarkuptext}% 4.171 -\isamarkuptrue% 4.172 -% 4.173 \isamarkupsection{Theorems \label{sec:thms}% 4.174 } 4.175 \isamarkuptrue% 4.176 @@ -267,22 +274,53 @@ 4.177 \end{isamarkuptext}% 4.178 \isamarkuptrue% 4.179 % 4.180 -\isamarkupsubsection{Primitive inferences% 4.181 +\isamarkupsection{Proof terms% 4.182 } 4.183 \isamarkuptrue% 4.184 % 4.185 \begin{isamarkuptext}% 4.186 -FIXME% 4.187 +FIXME !?% 4.188 \end{isamarkuptext}% 4.189 \isamarkuptrue% 4.190 % 4.191 -\isamarkupsubsection{Higher-order resolution% 4.192 +\isamarkupsection{Rules \label{sec:rules}% 4.193 } 4.194 \isamarkuptrue% 4.195 % 4.196 \begin{isamarkuptext}% 4.197 FIXME 4.198 4.199 + A \emph{rule} is any Pure theorem in HHF normal form; there is a 4.200 + separate calculus for rule composition, which is modeled after 4.201 + Gentzen's Natural Deduction \cite{Gentzen:1935}, but allows 4.202 + rules to be nested arbitrarily, similar to \cite{extensions91}. 4.203 + 4.204 + Normally, all theorems accessible to the user are proper rules. 4.205 + Low-level inferences are occasional required internally, but the 4.206 + result should be always presented in canonical form. The higher 4.207 + interfaces of Isabelle/Isar will always produce proper rules. It is 4.208 + important to maintain this invariant in add-on applications! 4.209 + 4.210 + There are two main principles of rule composition: \isa{resolution} (i.e.\ backchaining of rules) and \isa{by{\isacharminus}assumption} (i.e.\ closing a branch); both principles are 4.211 + combined in the variants of \isa{elim{\isacharminus}resosultion} and \isa{dest{\isacharminus}resolution}. Raw \isa{composition} is occasionally 4.212 + useful as well, also it is strictly speaking outside of the proper 4.213 + rule calculus. 4.214 + 4.215 + Rules are treated modulo general higher-order unification, which is 4.216 + unification modulo the equational theory of \isa{{\isasymalpha}{\isasymbeta}{\isasymeta}}-conversion 4.217 + on \isa{{\isasymlambda}}-terms. Moreover, propositions are understood modulo 4.218 + the (derived) equivalence \isa{{\isacharparenleft}A\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ B\ x{\isacharparenright}{\isacharparenright}\ {\isasymequiv}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ A\ {\isasymLongrightarrow}\ B\ x{\isacharparenright}}. 4.219 + 4.220 + This means that any operations within the rule calculus may be 4.221 + subject to spontaneous \isa{{\isasymalpha}{\isasymbeta}{\isasymeta}}-HHF conversions. It is common 4.222 + practice not to contract or expand unnecessarily. Some mechanisms 4.223 + prefer an one form, others the opposite, so there is a potential 4.224 + danger to produce some oscillation! 4.225 + 4.226 + Only few operations really work \emph{modulo} HHF conversion, but 4.227 + expect a normal form: quantifiers \isa{{\isasymAnd}} before implications 4.228 + \isa{{\isasymLongrightarrow}} at each level of nesting. 4.229 + 4.230 \glossary{Hereditary Harrop Formula}{The set of propositions in HHF 4.231 format is defined inductively as \isa{H\ {\isacharequal}\ {\isacharparenleft}{\isasymAnd}x\isactrlsup {\isacharasterisk}{\isachardot}\ H\isactrlsup {\isacharasterisk}\ {\isasymLongrightarrow}\ A{\isacharparenright}}, for variables \isa{x} and atomic propositions \isa{A}. 4.232 Any proposition may be put into HHF form by normalizing with the rule 4.233 @@ -295,15 +333,6 @@ 4.234 \end{isamarkuptext}% 4.235 \isamarkuptrue% 4.236 % 4.237 -\isamarkupsubsection{Equational reasoning% 4.238 -} 4.239 -\isamarkuptrue% 4.240 -% 4.241 -\begin{isamarkuptext}% 4.242 -FIXME% 4.243 -\end{isamarkuptext}% 4.244 -\isamarkuptrue% 4.245 -% 4.246 \isadelimtheory 4.247 % 4.248 \endisadelimtheory

5.1 --- a/doc-src/IsarImplementation/Thy/document/proof.tex Thu Sep 07 15:16:51 2006 +0200 5.2 +++ b/doc-src/IsarImplementation/Thy/document/proof.tex Thu Sep 07 20:12:08 2006 +0200 5.3 @@ -217,7 +217,7 @@ 5.4 definition works by fixing \isa{x} and assuming \isa{x\ {\isasymequiv}\ t}, 5.5 with the following export rule to reverse the effect: 5.6 \[ 5.7 - \infer{\isa{{\isasymGamma}\ {\isacharbackslash}\ x\ {\isasymequiv}\ t\ {\isasymturnstile}\ B\ t}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B\ x}} 5.8 + \infer[(\isa{{\isasymequiv}{\isacharminus}expand})]{\isa{{\isasymGamma}\ {\isacharbackslash}\ x\ {\isasymequiv}\ t\ {\isasymturnstile}\ B\ t}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B\ x}} 5.9 \] 5.10 This works, because the assumption \isa{x\ {\isasymequiv}\ t} was introduced in 5.11 a context with \isa{x} being fresh, so \isa{x} does not 5.12 @@ -291,22 +291,30 @@ 5.13 references to free variables or assumptions not present in the proof 5.14 context. 5.15 5.16 - \medskip The \isa{prove} operation provides an interface for 5.17 - structured backwards reasoning under program control, with some 5.18 - explicit sanity checks of the result. The goal context can be 5.19 - augmented by additional fixed variables (cf.\ 5.20 - \secref{sec:variables}) and assumptions (cf.\ 5.21 - \secref{sec:assumptions}), which will be available as local facts 5.22 - during the proof and discharged into implications in the result. 5.23 - Type and term variables are generalized as usual, according to the 5.24 - context. 5.25 + \medskip The \isa{SUBPROOF} combinator allows to structure a 5.26 + tactical proof recursively by decomposing a selected sub-goal: 5.27 + \isa{{\isacharparenleft}{\isasymAnd}x{\isachardot}\ A{\isacharparenleft}x{\isacharparenright}\ {\isasymLongrightarrow}\ B{\isacharparenleft}x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}} is turned into \isa{B{\isacharparenleft}x{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}} 5.28 + after fixing \isa{x} and assuming \isa{A{\isacharparenleft}x{\isacharparenright}}. This means 5.29 + the tactic needs to solve the conclusion, but may use the premise as 5.30 + a local fact, for locally fixed variables. 5.31 5.32 - The \isa{prove{\isacharunderscore}multi} operation handles several simultaneous 5.33 - claims within a single goal, by using Pure conjunction internally. 5.34 + The \isa{prove} operation provides an interface for structured 5.35 + backwards reasoning under program control, with some explicit sanity 5.36 + checks of the result. The goal context can be augmented by 5.37 + additional fixed variables (cf.\ \secref{sec:variables}) and 5.38 + assumptions (cf.\ \secref{sec:assumptions}), which will be available 5.39 + as local facts during the proof and discharged into implications in 5.40 + the result. Type and term variables are generalized as usual, 5.41 + according to the context. 5.42 5.43 - \medskip Tactical proofs may be structured recursively by 5.44 - decomposing a sub-goal: \isa{{\isacharparenleft}{\isasymAnd}x{\isachardot}\ A{\isacharparenleft}x{\isacharparenright}\ {\isasymLongrightarrow}\ B{\isacharparenleft}x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}} is turned 5.45 - into \isa{B{\isacharparenleft}x{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}} after fixing \isa{x} and assuming \isa{A{\isacharparenleft}x{\isacharparenright}}.% 5.46 + The \isa{obtain} operation produces results by eliminating 5.47 + existing facts by means of a given tactic. This acts like a dual 5.48 + conclusion: the proof demonstrates that the context may be augmented 5.49 + by certain fixed variables and assumptions. See also 5.50 + \cite{isabelle-isar-ref} for the user-level \isa{{\isasymOBTAIN}} and 5.51 + \isa{{\isasymGUESS}} elements. Final results, which may not refer to 5.52 + the parameters in the conclusion, need to exported explicitly into 5.53 + the original context.% 5.54 \end{isamarkuptext}% 5.55 \isamarkuptrue% 5.56 % 5.57 @@ -318,31 +326,39 @@ 5.58 % 5.59 \begin{isamarkuptext}% 5.60 \begin{mldecls} 5.61 + \indexml{SUBPROOF}\verb|SUBPROOF: ({context: Proof.context, schematics: ctyp list * cterm list,|\isasep\isanewline% 5.62 +\verb| params: cterm list, asms: cterm list, concl: cterm,|\isasep\isanewline% 5.63 +\verb| prems: thm list} -> tactic) -> Proof.context -> int -> tactic| \\ 5.64 \indexml{Goal.prove}\verb|Goal.prove: Proof.context -> string list -> term list -> term ->|\isasep\isanewline% 5.65 \verb| ({prems: thm list, context: Proof.context} -> tactic) -> thm| \\ 5.66 \indexml{Goal.prove-multi}\verb|Goal.prove_multi: Proof.context -> string list -> term list -> term list ->|\isasep\isanewline% 5.67 \verb| ({prems: thm list, context: Proof.context} -> tactic) -> thm list| \\ 5.68 - \indexml{SUBPROOF}\verb|SUBPROOF: ({context: Proof.context, schematics: ctyp list * cterm list,|\isasep\isanewline% 5.69 -\verb| params: cterm list, asms: cterm list, concl: cterm,|\isasep\isanewline% 5.70 -\verb| prems: thm list} -> tactic) -> Proof.context -> int -> tactic| 5.71 + \indexml{Obtain.result}\verb|Obtain.result: (Proof.context -> tactic) ->|\isasep\isanewline% 5.72 +\verb| thm list -> Proof.context -> (cterm list * thm list) * Proof.context| 5.73 \end{mldecls} 5.74 5.75 \begin{description} 5.76 5.77 + \item \verb|SUBPROOF|~\isa{tac} decomposes the structure of a 5.78 + particular sub-goal, producing an extended context and a reduced 5.79 + goal, which needs to be solved by the given tactic. All schematic 5.80 + parameters of the goal are imported into the context as fixed ones, 5.81 + which may not be instantiated in the sub-proof. 5.82 + 5.83 \item \verb|Goal.prove|~\isa{ctxt\ xs\ As\ C\ tac} states goal \isa{C} in the context augmented by fixed variables \isa{xs} and 5.84 assumptions \isa{As}, and applies tactic \isa{tac} to solve 5.85 it. The latter may depend on the local assumptions being presented 5.86 as facts. The result is in HHF normal form. 5.87 5.88 \item \verb|Goal.prove_multi| is simular to \verb|Goal.prove|, but 5.89 - states several conclusions simultaneously. \verb|Tactic.conjunction_tac| may be used to split these into individual 5.90 - subgoals before commencing the actual proof. 5.91 + states several conclusions simultaneously. The goal is encoded by 5.92 + means of Pure conjunction; \verb|Tactic.conjunction_tac| will turn 5.93 + this into a collection of individual subgoals. 5.94 5.95 - \item \verb|SUBPROOF|~\isa{tac} decomposes the structure of a 5.96 - particular sub-goal, producing an extended context and a reduced 5.97 - goal, which needs to be solved by the given tactic. All schematic 5.98 - parameters of the goal are imported into the context as fixed ones, 5.99 - which may not be instantiated in the sub-proof. 5.100 + \item \verb|Obtain.result|~\isa{tac\ thms\ ctxt} eliminates the 5.101 + given facts using a tactic, which results in additional fixed 5.102 + variables and assumptions in the context. Final results need to be 5.103 + exported explicitly. 5.104 5.105 \end{description}% 5.106 \end{isamarkuptext}%

6.1 --- a/doc-src/IsarImplementation/Thy/integration.thy Thu Sep 07 15:16:51 2006 +0200 6.2 +++ b/doc-src/IsarImplementation/Thy/integration.thy Thu Sep 07 20:12:08 2006 +0200 6.3 @@ -432,9 +432,4 @@ 6.4 \end{description} 6.5 *} 6.6 6.7 - 6.8 -section {* Sessions and document preparation *} 6.9 - 6.10 -text FIXME 6.11 - 6.12 end

7.1 --- a/doc-src/IsarImplementation/Thy/logic.thy Thu Sep 07 15:16:51 2006 +0200 7.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy Thu Sep 07 20:12:08 2006 +0200 7.3 @@ -11,7 +11,8 @@ 7.4 \cite{paulson700}. This is essentially the same logic as ``@{text 7.5 "\<lambda>HOL"}'' in the more abstract framework of Pure Type Systems (PTS) 7.6 \cite{Barendregt-Geuvers:2001}, although there are some key 7.7 - differences in the practical treatment of simple types. 7.8 + differences in the specific treatment of simple types in 7.9 + Isabelle/Pure. 7.10 7.11 Following type-theoretic parlance, the Pure logic consists of three 7.12 levels of @{text "\<lambda>"}-calculus with corresponding arrows: @{text 7.13 @@ -20,8 +21,11 @@ 7.14 @{text "\<Longrightarrow>"} for implication (proofs depending on proofs). 7.15 7.16 Pure derivations are relative to a logical theory, which declares 7.17 - type constructors, term constants, and axioms. Term constants and 7.18 - axioms support schematic polymorphism. 7.19 + type constructors, term constants, and axioms. Theory declarations 7.20 + support schematic polymorphism, which is strictly speaking outside 7.21 + the logic.\footnote{Incidently, this is the main logical reason, why 7.22 + the theory context @{text "\<Theta>"} is separate from the context @{text 7.23 + "\<Gamma>"} of the core calculus.} 7.24 *} 7.25 7.26 7.27 @@ -34,46 +38,48 @@ 7.28 \medskip A \emph{type class} is an abstract syntactic entity 7.29 declared in the theory context. The \emph{subclass relation} @{text 7.30 "c\<^isub>1 \<subseteq> c\<^isub>2"} is specified by stating an acyclic 7.31 - generating relation; the transitive closure maintained internally. 7.32 + generating relation; the transitive closure is maintained 7.33 + internally. The resulting relation is an ordering: reflexive, 7.34 + transitive, and antisymmetric. 7.35 7.36 A \emph{sort} is a list of type classes written as @{text 7.37 "{c\<^isub>1, \<dots>, c\<^isub>m}"}, which represents symbolic 7.38 intersection. Notationally, the curly braces are omitted for 7.39 singleton intersections, i.e.\ any class @{text "c"} may be read as 7.40 a sort @{text "{c}"}. The ordering on type classes is extended to 7.41 - sorts in the canonical fashion: @{text "{c\<^isub>1, \<dots> c\<^isub>m} \<subseteq> 7.42 - {d\<^isub>1, \<dots>, d\<^isub>n}"} iff @{text "\<forall>j. \<exists>i. c\<^isub>i \<subseteq> 7.43 - d\<^isub>j"}. The empty intersection @{text "{}"} refers to the 7.44 - universal sort, which is the largest element wrt.\ the sort order. 7.45 - The intersections of all (i.e.\ finitely many) classes declared in 7.46 - the current theory are the minimal elements wrt.\ sort order. 7.47 + sorts according to the meaning of intersections: @{text 7.48 + "{c\<^isub>1, \<dots> c\<^isub>m} \<subseteq> {d\<^isub>1, \<dots>, d\<^isub>n}"} iff 7.49 + @{text "\<forall>j. \<exists>i. c\<^isub>i \<subseteq> d\<^isub>j"}. The empty intersection 7.50 + @{text "{}"} refers to the universal sort, which is the largest 7.51 + element wrt.\ the sort order. The intersections of all (finitely 7.52 + many) classes declared in the current theory are the minimal 7.53 + elements wrt.\ the sort order. 7.54 7.55 - \medskip A \emph{fixed type variable} is pair of a basic name 7.56 + \medskip A \emph{fixed type variable} is a pair of a basic name 7.57 (starting with @{text "'"} character) and a sort constraint. For 7.58 example, @{text "('a, s)"} which is usually printed as @{text 7.59 "\<alpha>\<^isub>s"}. A \emph{schematic type variable} is a pair of an 7.60 indexname and a sort constraint. For example, @{text "(('a, 0), 7.61 - s)"} which is usually printed @{text "?\<alpha>\<^isub>s"}. 7.62 + s)"} which is usually printed as @{text "?\<alpha>\<^isub>s"}. 7.63 7.64 Note that \emph{all} syntactic components contribute to the identity 7.65 - of a type variables, including the literal sort constraint. The 7.66 - core logic handles type variables with the same name but different 7.67 - sorts as different, even though the outer layers of the system make 7.68 - it hard to produce anything like this. 7.69 + of type variables, including the literal sort constraint. The core 7.70 + logic handles type variables with the same name but different sorts 7.71 + as different, although some outer layers of the system make it hard 7.72 + to produce anything like this. 7.73 7.74 - A \emph{type constructor} is an @{text "k"}-ary type operator 7.75 - declared in the theory. 7.76 + A \emph{type constructor} is a @{text "k"}-ary operator on types 7.77 + declared in the theory. Type constructor application is usually 7.78 + written postfix. For @{text "k = 0"} the argument tuple is omitted, 7.79 + e.g.\ @{text "prop"} instead of @{text "()prop"}. For @{text "k = 7.80 + 1"} the parentheses are omitted, e.g.\ @{text "\<alpha> list"} instead of 7.81 + @{text "(\<alpha>)list"}. Further notation is provided for specific 7.82 + constructors, notably right-associative infix @{text "\<alpha> \<Rightarrow> \<beta>"} 7.83 + instead of @{text "(\<alpha>, \<beta>)fun"} constructor. 7.84 7.85 A \emph{type} is defined inductively over type variables and type 7.86 - constructors: @{text "\<tau> = \<alpha>\<^isub>s | ?\<alpha>\<^isub>s | (\<tau>\<^sub>1, \<dots>, 7.87 - \<tau>\<^sub>k)c"}. Type constructor application is usually written 7.88 - postfix. For @{text "k = 0"} the argument tuple is omitted, e.g.\ 7.89 - @{text "prop"} instead of @{text "()prop"}. For @{text "k = 1"} the 7.90 - parentheses are omitted, e.g.\ @{text "\<tau> list"} instead of @{text 7.91 - "(\<tau>) list"}. Further notation is provided for specific 7.92 - constructors, notably right-associative infix @{text "\<tau>\<^isub>1 \<Rightarrow> 7.93 - \<tau>\<^isub>2"} instead of @{text "(\<tau>\<^isub>1, \<tau>\<^isub>2)fun"} 7.94 - constructor. 7.95 + constructors as follows: @{text "\<tau> = \<alpha>\<^isub>s | ?\<alpha>\<^isub>s | 7.96 + (\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)c"}. 7.97 7.98 A \emph{type abbreviation} is a syntactic abbreviation of an 7.99 arbitrary type expression of the theory. Type abbreviations looks 7.100 @@ -82,26 +88,30 @@ 7.101 7.102 A \emph{type arity} declares the image behavior of a type 7.103 constructor wrt.\ the algebra of sorts: @{text "c :: (s\<^isub>1, \<dots>, 7.104 - s\<^isub>n)s"} means that @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>k)c"} is 7.105 + s\<^isub>k)s"} means that @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>k)c"} is 7.106 of sort @{text "s"} if each argument type @{text "\<tau>\<^isub>i"} is of 7.107 - sort @{text "s\<^isub>i"}. The sort algebra is always maintained as 7.108 - \emph{coregular}, which means that type arities are consistent with 7.109 - the subclass relation: for each type constructor @{text "c"} and 7.110 - classes @{text "c\<^isub>1 \<subseteq> c\<^isub>2"}, any arity @{text "c :: 7.111 + sort @{text "s\<^isub>i"}. Arity declarations are implicitly 7.112 + completed, i.e.\ @{text "c :: (\<^vec>s)c"} entails @{text "c :: 7.113 + (\<^vec>s)c'"} for any @{text "c' \<supseteq> c"}. 7.114 + 7.115 + \medskip The sort algebra is always maintained as \emph{coregular}, 7.116 + which means that type arities are consistent with the subclass 7.117 + relation: for each type constructor @{text "c"} and classes @{text 7.118 + "c\<^isub>1 \<subseteq> c\<^isub>2"}, any arity @{text "c :: 7.119 (\<^vec>s\<^isub>1)c\<^isub>1"} has a corresponding arity @{text "c 7.120 :: (\<^vec>s\<^isub>2)c\<^isub>2"} where @{text "\<^vec>s\<^isub>1 \<subseteq> 7.121 \<^vec>s\<^isub>2"} holds pointwise for all argument sorts. 7.122 7.123 - The key property of the order-sorted algebra of types is that sort 7.124 + The key property of a coregular order-sorted algebra is that sort 7.125 constraints may be always fulfilled in a most general fashion: for 7.126 each type constructor @{text "c"} and sort @{text "s"} there is a 7.127 most general vector of argument sorts @{text "(s\<^isub>1, \<dots>, 7.128 - s\<^isub>k)"} such that @{text "(\<tau>\<^bsub>s\<^isub>1\<^esub>, \<dots>, 7.129 - \<tau>\<^bsub>s\<^isub>k\<^esub>)"} for arbitrary @{text "\<tau>\<^isub>i"} of 7.130 - sort @{text "s\<^isub>i"}. This means the unification problem on 7.131 - the algebra of types has most general solutions (modulo renaming and 7.132 - equivalence of sorts). As a consequence, type-inference is able to 7.133 - produce primary types. 7.134 + s\<^isub>k)"} such that a type scheme @{text 7.135 + "(\<alpha>\<^bsub>s\<^isub>1\<^esub>, \<dots>, \<alpha>\<^bsub>s\<^isub>k\<^esub>)c"} is 7.136 + of sort @{text "s"}. Consequently, the unification problem on the 7.137 + algebra of types has most general solutions (modulo renaming and 7.138 + equivalence of sorts). Moreover, the usual type-inference algorithm 7.139 + will produce primary types as expected \cite{nipkow-prehofer}. 7.140 *} 7.141 7.142 text %mlref {* 7.143 @@ -139,19 +149,19 @@ 7.144 tests the subsort relation @{text "s\<^isub>1 \<subseteq> s\<^isub>2"}. 7.145 7.146 \item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether a type 7.147 - expression of of a given sort. 7.148 + is of a given sort. 7.149 7.150 \item @{ML Sign.add_types}~@{text "[(c, k, mx), \<dots>]"} declares new 7.151 - type constructors @{text "c"} with @{text "k"} arguments, and 7.152 + type constructors @{text "c"} with @{text "k"} arguments and 7.153 optional mixfix syntax. 7.154 7.155 \item @{ML Sign.add_tyabbrs_i}~@{text "[(c, \<^vec>\<alpha>, \<tau>, mx), \<dots>]"} 7.156 - defines type abbreviation @{text "(\<^vec>\<alpha>)c"} (with optional 7.157 - mixfix syntax) as @{text "\<tau>"}. 7.158 + defines a new type abbreviation @{text "(\<^vec>\<alpha>)c = \<tau>"} with 7.159 + optional mixfix syntax. 7.160 7.161 \item @{ML Sign.primitive_class}~@{text "(c, [c\<^isub>1, \<dots>, 7.162 c\<^isub>n])"} declares new class @{text "c"} derived together with 7.163 - class relations @{text "c \<subseteq> c\<^isub>i"}. 7.164 + class relations @{text "c \<subseteq> c\<^isub>i"}, for @{text "i = 1, \<dots>, n"}. 7.165 7.166 \item @{ML Sign.primitive_classrel}~@{text "(c\<^isub>1, 7.167 c\<^isub>2)"} declares class relation @{text "c\<^isub>1 \<subseteq> 7.168 @@ -170,6 +180,13 @@ 7.169 text {* 7.170 \glossary{Term}{FIXME} 7.171 7.172 + The language of terms is that of simply-typed @{text "\<lambda>"}-calculus 7.173 + with de-Bruijn indices for bound variables, and named free 7.174 + variables, and constants. Terms with loose bound variables are 7.175 + usually considered malformed. The types of variables and constants 7.176 + is stored explicitly at each occurrence in the term (which is a 7.177 + known performance issue). 7.178 + 7.179 FIXME de-Bruijn representation of lambda terms 7.180 7.181 Term syntax provides explicit abstraction @{text "\<lambda>x :: \<alpha>. b(x)"} 7.182 @@ -193,13 +210,6 @@ 7.183 *} 7.184 7.185 7.186 -section {* Proof terms *} 7.187 - 7.188 -text {* 7.189 - FIXME 7.190 -*} 7.191 - 7.192 - 7.193 section {* Theorems \label{sec:thms} *} 7.194 7.195 text {* 7.196 @@ -258,17 +268,54 @@ 7.197 7.198 *} 7.199 7.200 -subsection {* Primitive inferences *} 7.201 + 7.202 +section {* Proof terms *} 7.203 7.204 -text FIXME 7.205 +text {* 7.206 + FIXME !? 7.207 +*} 7.208 7.209 7.210 -subsection {* Higher-order resolution *} 7.211 +section {* Rules \label{sec:rules} *} 7.212 7.213 text {* 7.214 7.215 FIXME 7.216 7.217 + A \emph{rule} is any Pure theorem in HHF normal form; there is a 7.218 + separate calculus for rule composition, which is modeled after 7.219 + Gentzen's Natural Deduction \cite{Gentzen:1935}, but allows 7.220 + rules to be nested arbitrarily, similar to \cite{extensions91}. 7.221 + 7.222 + Normally, all theorems accessible to the user are proper rules. 7.223 + Low-level inferences are occasional required internally, but the 7.224 + result should be always presented in canonical form. The higher 7.225 + interfaces of Isabelle/Isar will always produce proper rules. It is 7.226 + important to maintain this invariant in add-on applications! 7.227 + 7.228 + There are two main principles of rule composition: @{text 7.229 + "resolution"} (i.e.\ backchaining of rules) and @{text 7.230 + "by-assumption"} (i.e.\ closing a branch); both principles are 7.231 + combined in the variants of @{text "elim-resosultion"} and @{text 7.232 + "dest-resolution"}. Raw @{text "composition"} is occasionally 7.233 + useful as well, also it is strictly speaking outside of the proper 7.234 + rule calculus. 7.235 + 7.236 + Rules are treated modulo general higher-order unification, which is 7.237 + unification modulo the equational theory of @{text "\<alpha>\<beta>\<eta>"}-conversion 7.238 + on @{text "\<lambda>"}-terms. Moreover, propositions are understood modulo 7.239 + the (derived) equivalence @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}. 7.240 + 7.241 + This means that any operations within the rule calculus may be 7.242 + subject to spontaneous @{text "\<alpha>\<beta>\<eta>"}-HHF conversions. It is common 7.243 + practice not to contract or expand unnecessarily. Some mechanisms 7.244 + prefer an one form, others the opposite, so there is a potential 7.245 + danger to produce some oscillation! 7.246 + 7.247 + Only few operations really work \emph{modulo} HHF conversion, but 7.248 + expect a normal form: quantifiers @{text "\<And>"} before implications 7.249 + @{text "\<Longrightarrow>"} at each level of nesting. 7.250 + 7.251 \glossary{Hereditary Harrop Formula}{The set of propositions in HHF 7.252 format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow> 7.253 A)"}, for variables @{text "x"} and atomic propositions @{text "A"}. 7.254 @@ -282,9 +329,4 @@ 7.255 7.256 *} 7.257 7.258 -subsection {* Equational reasoning *} 7.259 - 7.260 -text FIXME 7.261 - 7.262 - 7.263 end

8.1 --- a/doc-src/IsarImplementation/Thy/proof.thy Thu Sep 07 15:16:51 2006 +0200 8.2 +++ b/doc-src/IsarImplementation/Thy/proof.thy Thu Sep 07 20:12:08 2006 +0200 8.3 @@ -196,7 +196,7 @@ 8.4 definition works by fixing @{text "x"} and assuming @{text "x \<equiv> t"}, 8.5 with the following export rule to reverse the effect: 8.6 \[ 8.7 - \infer{@{text "\<Gamma> \\ x \<equiv> t \<turnstile> B t"}}{@{text "\<Gamma> \<turnstile> B x"}} 8.8 + \infer[(@{text "\<equiv>-expand"})]{@{text "\<Gamma> \\ x \<equiv> t \<turnstile> B t"}}{@{text "\<Gamma> \<turnstile> B x"}} 8.9 \] 8.10 This works, because the assumption @{text "x \<equiv> t"} was introduced in 8.11 a context with @{text "x"} being fresh, so @{text "x"} does not 8.12 @@ -258,39 +258,54 @@ 8.13 references to free variables or assumptions not present in the proof 8.14 context. 8.15 8.16 - \medskip The @{text "prove"} operation provides an interface for 8.17 - structured backwards reasoning under program control, with some 8.18 - explicit sanity checks of the result. The goal context can be 8.19 - augmented by additional fixed variables (cf.\ 8.20 - \secref{sec:variables}) and assumptions (cf.\ 8.21 - \secref{sec:assumptions}), which will be available as local facts 8.22 - during the proof and discharged into implications in the result. 8.23 - Type and term variables are generalized as usual, according to the 8.24 - context. 8.25 + \medskip The @{text "SUBPROOF"} combinator allows to structure a 8.26 + tactical proof recursively by decomposing a selected sub-goal: 8.27 + @{text "(\<And>x. A(x) \<Longrightarrow> B(x)) \<Longrightarrow> \<dots>"} is turned into @{text "B(x) \<Longrightarrow> \<dots>"} 8.28 + after fixing @{text "x"} and assuming @{text "A(x)"}. This means 8.29 + the tactic needs to solve the conclusion, but may use the premise as 8.30 + a local fact, for locally fixed variables. 8.31 8.32 - The @{text "prove_multi"} operation handles several simultaneous 8.33 - claims within a single goal, by using Pure conjunction internally. 8.34 + The @{text "prove"} operation provides an interface for structured 8.35 + backwards reasoning under program control, with some explicit sanity 8.36 + checks of the result. The goal context can be augmented by 8.37 + additional fixed variables (cf.\ \secref{sec:variables}) and 8.38 + assumptions (cf.\ \secref{sec:assumptions}), which will be available 8.39 + as local facts during the proof and discharged into implications in 8.40 + the result. Type and term variables are generalized as usual, 8.41 + according to the context. 8.42 8.43 - \medskip Tactical proofs may be structured recursively by 8.44 - decomposing a sub-goal: @{text "(\<And>x. A(x) \<Longrightarrow> B(x)) \<Longrightarrow> \<dots>"} is turned 8.45 - into @{text "B(x) \<Longrightarrow> \<dots>"} after fixing @{text "x"} and assuming @{text 8.46 - "A(x)"}. 8.47 + The @{text "obtain"} operation produces results by eliminating 8.48 + existing facts by means of a given tactic. This acts like a dual 8.49 + conclusion: the proof demonstrates that the context may be augmented 8.50 + by certain fixed variables and assumptions. See also 8.51 + \cite{isabelle-isar-ref} for the user-level @{text "\<OBTAIN>"} and 8.52 + @{text "\<GUESS>"} elements. Final results, which may not refer to 8.53 + the parameters in the conclusion, need to exported explicitly into 8.54 + the original context. 8.55 *} 8.56 8.57 text %mlref {* 8.58 \begin{mldecls} 8.59 + @{index_ML SUBPROOF: 8.60 + "({context: Proof.context, schematics: ctyp list * cterm list, 8.61 + params: cterm list, asms: cterm list, concl: cterm, 8.62 + prems: thm list} -> tactic) -> Proof.context -> int -> tactic"} \\ 8.63 @{index_ML Goal.prove: "Proof.context -> string list -> term list -> term -> 8.64 ({prems: thm list, context: Proof.context} -> tactic) -> thm"} \\ 8.65 @{index_ML Goal.prove_multi: "Proof.context -> string list -> term list -> term list -> 8.66 ({prems: thm list, context: Proof.context} -> tactic) -> thm list"} \\ 8.67 - @{index_ML SUBPROOF: 8.68 - "({context: Proof.context, schematics: ctyp list * cterm list, 8.69 - params: cterm list, asms: cterm list, concl: cterm, 8.70 - prems: thm list} -> tactic) -> Proof.context -> int -> tactic"} 8.71 + @{index_ML Obtain.result: "(Proof.context -> tactic) -> 8.72 + thm list -> Proof.context -> (cterm list * thm list) * Proof.context"} 8.73 \end{mldecls} 8.74 8.75 \begin{description} 8.76 8.77 + \item @{ML SUBPROOF}~@{text "tac"} decomposes the structure of a 8.78 + particular sub-goal, producing an extended context and a reduced 8.79 + goal, which needs to be solved by the given tactic. All schematic 8.80 + parameters of the goal are imported into the context as fixed ones, 8.81 + which may not be instantiated in the sub-proof. 8.82 + 8.83 \item @{ML Goal.prove}~@{text "ctxt xs As C tac"} states goal @{text 8.84 "C"} in the context augmented by fixed variables @{text "xs"} and 8.85 assumptions @{text "As"}, and applies tactic @{text "tac"} to solve 8.86 @@ -298,15 +313,14 @@ 8.87 as facts. The result is in HHF normal form. 8.88 8.89 \item @{ML Goal.prove_multi} is simular to @{ML Goal.prove}, but 8.90 - states several conclusions simultaneously. @{ML 8.91 - Tactic.conjunction_tac} may be used to split these into individual 8.92 - subgoals before commencing the actual proof. 8.93 + states several conclusions simultaneously. The goal is encoded by 8.94 + means of Pure conjunction; @{ML Tactic.conjunction_tac} will turn 8.95 + this into a collection of individual subgoals. 8.96 8.97 - \item @{ML SUBPROOF}~@{text "tac"} decomposes the structure of a 8.98 - particular sub-goal, producing an extended context and a reduced 8.99 - goal, which needs to be solved by the given tactic. All schematic 8.100 - parameters of the goal are imported into the context as fixed ones, 8.101 - which may not be instantiated in the sub-proof. 8.102 + \item @{ML Obtain.result}~@{text "tac thms ctxt"} eliminates the 8.103 + given facts using a tactic, which results in additional fixed 8.104 + variables and assumptions in the context. Final results need to be 8.105 + exported explicitly. 8.106 8.107 \end{description} 8.108 *}

9.1 --- a/doc-src/IsarImplementation/Thy/unused.thy Thu Sep 07 15:16:51 2006 +0200 9.2 +++ b/doc-src/IsarImplementation/Thy/unused.thy Thu Sep 07 20:12:08 2006 +0200 9.3 @@ -1,3 +1,6 @@ 9.4 + 9.5 +section {* Sessions and document preparation *} 9.6 + 9.7 section {* Structured output *} 9.8 9.9 subsection {* Pretty printing *}

10.1 --- a/doc-src/IsarImplementation/style.sty Thu Sep 07 15:16:51 2006 +0200 10.2 +++ b/doc-src/IsarImplementation/style.sty Thu Sep 07 20:12:08 2006 +0200 10.3 @@ -49,6 +49,8 @@ 10.4 \renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{\ML}~~}Reference}\begingroup\def\isastyletext{\rm}\small} 10.5 \renewcommand{\endisatagmlref}{\endgroup} 10.6 10.7 +\newcommand{\isasymGUESS}{\isakeyword{guess}} 10.8 +\newcommand{\isasymOBTAIN}{\isakeyword{obtain}} 10.9 \newcommand{\isasymTHEORY}{\isakeyword{theory}} 10.10 \newcommand{\isasymIMPORTS}{\isakeyword{imports}} 10.11 \newcommand{\isasymUSES}{\isakeyword{uses}}