summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Thu, 28 Feb 2002 18:09:04 +0100 | |

changeset 12976 | 5cfe2941a5db |

parent 12975 | d796a2fd6c69 |

child 12977 | fcc9a30a7ef2 |

contexts, locales, sym(metric);

--- a/doc-src/IsarRef/generic.tex Thu Feb 28 17:46:46 2002 +0100 +++ b/doc-src/IsarRef/generic.tex Thu Feb 28 18:09:04 2002 +0100 @@ -5,11 +5,6 @@ \subsection{Axiomatic type classes}\label{sec:axclass} -%FIXME -% - qualified names -% - class intro rules; -% - class axioms; - \indexisarcmd{axclass}\indexisarcmd{instance}\indexisarmeth{intro-classes} \begin{matharray}{rcl} \isarcmd{axclass} & : & \isartrans{theory}{theory} \\ @@ -36,8 +31,13 @@ the intersection of existing classes, with additional axioms holding. Class axioms may not contain more than one type variable. The class axioms (with implicit sort constraints added) are bound to the given names. Furthermore - a class introduction rule is generated, which is employed by method - $intro_classes$ to support instantiation proofs of this class. + a class introduction rule is generated (being bound as $c{.}intro$); this + rule is employed by method $intro_classes$ to support instantiation proofs + of this class. + + The ``axioms'' are stored as theorems according to the given name + specifications, adding the class name $c$ as name space prefix; these facts + are stored collectively as $c.axioms$, too. \item [$\INSTANCE~c@1 \subseteq c@2$ and $\INSTANCE~t :: (\vec s)c$] setup a goal stating a class relation or type arity. The proof would usually @@ -45,6 +45,7 @@ of the type classes involved. After finishing the proof, the theory will be augmented by a type signature declaration corresponding to the resulting theorem. + \item [$intro_classes$] repeatedly expands all class introduction rules of this theory. Note that this method usually needs not be named explicitly, as it is already included in the default proof step (of $\PROOFNAME$, @@ -55,18 +56,142 @@ \subsection{Locales and local contexts}\label{sec:locale} -FIXME +Locales are named local contexts, consisting of a declaration elements that +are modeled after the Isar proof context (cf.\ \S\ref{sec:proof-context}). + +\subsubsection{Localized commands} -\indexouternonterm{locale}\indexouternonterm{contextelem} +Existing locales may be augmented later on by adding new facts. Note that the +actual context definition may not be changed! Several theory commands that +produce facts in some way are available in ``localized'' versions, referring +to a named locale instead of the global theory context. +\indexouternonterm{locale} \begin{rail} locale: '(' 'in' name ')' ; +\end{rail} - contextelem: FIXME - ; +Emerging facts of localized commands are stored in two versions, both in the +target locale and the theory (after export). The latter view produces a +qualified binding, using the locale name as a name space prefix. + +For example, ``$\LEMMAS~(\IN~loc)~a = \vec b$'' retrieves facts $\vec b$ from +the locale context of $loc$ and augments its body by an appropriate +``$\isarkeyword{notes}$'' element (see below). The exported view of $a$, +after discharging the locale context, is stored as $loc{.}a$ within the global +theory. A localized goal ``$\LEMMANAME~(\IN~loc)~a:~\phi$'' work similarly, +only that the fact emerges through the subsequent proof, +which may refer to the full infrastructure of the locale context (including +local parameters with typing and concrete syntax, assumptions, definitions +etc.). Most notably, fact declarations of the locale are active during the +proof, too (e.g.\ local $simp$ rules). + + +\subsubsection{Locale specifications} + +\indexisarcmd{locale}\indexisarcmd{print-locale}\indexisarcmd{print-locales} +\begin{matharray}{rcl} + \isarcmd{locale} & : & \isarkeep{theory} \\ + \isarcmd{print_locale}^* & : & \isarkeep{theory~|~proof} \\ + \isarcmd{print_locales}^* & : & \isarkeep{theory~|~proof} \\ +\end{matharray} + +\indexouternonterm{contextexpr}\indexouternonterm{contextelem} + +\railalias{printlocale}{print\_locale} +\railterm{printlocale} + +\begin{rail} + 'locale' name ('=' localeexpr)? + ; + printlocale localeexpr + ; + localeexpr: ((contextexpr '+' (contextelem+)) | contextexpr | (contextelem+)) + ; + + contextexpr: nameref | '(' contextexpr ')' | + (contextexpr (name+)) | (contextexpr + '+') + ; + contextelem: fixes | assumes | defines | notes | includes + ; + fixes: 'fixes' (name ('::' type)? structmixfix? + 'and') + ; + assumes: 'assumes' (thmdecl? props + 'and') + ; + defines: 'defines' (thmdecl? prop proppat? + 'and') + ; + notes: 'notes' (thmdef? thmrefs + 'and') + ; + includes: 'includes' contextexpr + ; \end{rail} +\begin{descr} + +\item [$\LOCALE~loc~=~import~+~body$] defines new locale $loc$ as a context + consisting of a certain view of existing locales ($import$) plus some + additional elements ($body$). Both $import$ and $body$ are optional; the + trivial $\LOCALE~loc$ defines an empty locale, which may still be useful to + collect declarations of facts later on. Type-inference on locale + expressions automatically takes care of the most general typing that the + combined context elements may acquire. + + The $import$ consists of a structured context expression, consisting of + references to existing locales, renamed contexts, or merged contexts. + Renaming uses positional notation: $c~\vec x$ means that (a prefix) the + fixed parameters of context $c$ are named according to $\vec x$; a + ``\texttt{_}'' (underscore).\indexisarthm{_@\texttt{_}} means to skip that + position. Also note that concrete syntax only works with the original name. + Merging proceeds from left-to-right, suppressing any duplicates emerging + from different paths through an import hierarchy. + + The $body$ consists of basic context elements, further context expressions + may be included as well. + + \begin{descr} + + \item [$\FIXES{~x::\tau~(mx)}$] declares a local parameter of type $\tau$ + and mixfix annotation $mx$ (both are optional). The special syntax + declaration $(structure)$ means that $x$ may be referenced + implicitly in this context. %see also FIXME + + \item [$\ASSUMES{a}{\vec\phi}$] introduces local premises, similar to + $\ASSUMENAME$ within a proof (cf.\ \S\ref{sec:proof-context}). + + \item [$\DEFINES{a}{x \equiv t}$] defines a previously declared parameter. + This is close to $\DEFNAME$ within a proof (cf.\ + \S\ref{sec:proof-context}), but $\DEFINESNAME$ takes an equational + proposition instead of variable-term. The left-hand side of the equation + may have additional arguments, e.g.\ $\DEFINES{}{f~\vec x \equiv t}$. + + \item [$\NOTES{a}{\vec b}$] reconsiders facts within a local context. Most + notably, this may include arbitrary declarations in any attribute + specifications included here, e.g.\ a local $simp$ rule. + + \item [$\INCLUDES{c}$] copies the specified context in a statically scoped + manner. + + In contrast, the initial $import$ specification of a locale expression + maintains a dynamic relation to the locales being referenced (benefiting + from any later fact declarations in the obvious manner). + \end{descr} + + Note that $\IS{p}$ patterns given in the syntax of $\ASSUMESNAME$ and + $\DEFINESNAME$ above is actually illegal in locale definitions. In the long + goal format of \S\ref{sec:goals}, term bindings may be included as expected. + +\item [$\isarkeyword{print_locale}~import~+~body$] prints the specified locale + expression in a flattened form. The notable special case + $\isarkeyword{print_locale}~loc$ just prints the contents of the named + locale, but keep in mind that type-inference will normalize type variables + according to the usual alphabetical order. + +\item [$\isarkeyword{print_locales}$] prints the names of all locales of the + current theory. + +\end{descr} + \section{Derived proof schemes} @@ -124,7 +249,8 @@ \indexisarcmd{also}\indexisarcmd{finally} \indexisarcmd{moreover}\indexisarcmd{ultimately} -\indexisarcmd{print-trans-rules}\indexisaratt{trans} +\indexisarcmd{print-trans-rules} +\indexisaratt{trans}\indexisaratt{sym}\indexisaratt{symmetric} \begin{matharray}{rcl} \isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\ \isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\ @@ -132,6 +258,8 @@ \isarcmd{ultimately} & : & \isartrans{proof(state)}{proof(chain)} \\ \isarcmd{print_trans_rules}^* & : & \isarkeep{theory~|~proof} \\ trans & : & \isaratt \\ + sym & : & \isaratt \\ + symmetric & : & \isaratt \\ \end{matharray} Calculational proof is forward reasoning with implicit application of @@ -204,6 +332,17 @@ symmetry) rules declared in the current context. \item [$trans$] declares theorems as transitivity rules. + +\item [$sym$] declares symmetry rules, to be used either with the $symmetric$ + operation (see below), or in canonical single-step eliminations (such as + ``$\ASSUME{}{x = y}~\HENCE{}{y = x}~\DDOT$''). + + Isabelle/Pure declares symmetry of $\equiv$, common object-logics add + further standard rules, such as symmetry of $=$ and $\not=$. + +\item [$symmetric$] resolves a theorem with some rule declared as $sym$ in the + current context. For example, ``$\ASSUME{[symmetric]}{x = y}$'' produces a + swapped fact derived from that assumption. \end{descr} @@ -581,12 +720,11 @@ FIXME move? -\indexisarmeth{subst}\indexisarmeth{hypsubst}\indexisarmeth{split}\indexisaratt{symmetric} +\indexisarmeth{subst}\indexisarmeth{hypsubst}\indexisarmeth{split} \begin{matharray}{rcl} subst & : & \isarmeth \\ hypsubst^* & : & \isarmeth \\ split & : & \isarmeth \\ - symmetric & : & \isaratt \\ \end{matharray} \begin{rail} @@ -612,8 +750,6 @@ Note that the $simp$ method already involves repeated application of split rules as declared in the current context (see \S\ref{sec:simp}). -\item [$symmetric$] applies the symmetry rule of meta or object equality. - FIXME sym decl \end{descr}

--- a/doc-src/IsarRef/pure.tex Thu Feb 28 17:46:46 2002 +0100 +++ b/doc-src/IsarRef/pure.tex Thu Feb 28 18:09:04 2002 +0100 @@ -319,11 +319,12 @@ \begin{rail} 'axioms' (axmdecl prop +) ; - ('lemmas' | 'theorems') (thmdef? thmrefs + 'and') + ('lemmas' | 'theorems') locale? (thmdef? thmrefs + 'and') ; \end{rail} \begin{descr} + \item [$\isarkeyword{axioms}~a: \phi$] introduces arbitrary statements as axioms of the meta-logic. In fact, axioms are ``axiomatic theorems'', and may be referred later just as any other theorem. @@ -331,11 +332,15 @@ Axioms are usually only introduced when declaring new logical systems. Everyday work is typically done the hard way, with proper definitions and actual proven theorems. -\item [$\isarkeyword{lemmas}~a = \vec b$] stores existing facts. Typical - applications would also involve attributes, to declare Simplifier rules, for - example. + +\item [$\isarkeyword{lemmas}~a = \vec b$] restrieves and stores existing facts + in the theory context, or the specified locale (see also + \S\ref{sec:locale}). Typical applications would also involve attributes, to + declare Simplifier rules, for example. + \item [$\isarkeyword{theorems}$] is essentially the same as $\isarkeyword{lemmas}$, but marks the result as a different kind of facts. + \end{descr} @@ -721,7 +726,7 @@ the order of facts is less significant here. -\subsection{Goal statements} +\subsection{Goal statements}\label{sec:goals} \indexisarcmd{lemma}\indexisarcmd{theorem}\indexisarcmd{corollary} \indexisarcmd{have}\indexisarcmd{show}\indexisarcmd{hence}\indexisarcmd{thus} @@ -1127,7 +1132,7 @@ ; 'prefer' nat ; - 'declare' thmrefs + 'declare' locale? (thmrefs + 'and') ; \end{rail} @@ -1163,10 +1168,11 @@ branch points.} Basically, any proof command may return multiple results. \item [$\isarkeyword{declare}~thms$] declares theorems to the current theory - context. No theorem binding is involved here, unlike - $\isarkeyword{theorems}$ or $\isarkeyword{lemmas}$ (cf.\ - \S\ref{sec:axms-thms}). So $\isarkeyword{declare}$ only has the effect of - applying attributes as included in the theorem specification. + context (or the specified locale, see also \S\ref{sec:locale}). No theorem + binding is involved here, unlike $\isarkeyword{theorems}$ or + $\isarkeyword{lemmas}$ (cf.\ \S\ref{sec:axms-thms}), so + $\isarkeyword{declare}$ only has the effect of applying attributes as + included in the theorem specification. \end{descr} Any proper Isar proof method may be used with tactic script commands such as

--- a/doc-src/IsarRef/syntax.tex Thu Feb 28 17:46:46 2002 +0100 +++ b/doc-src/IsarRef/syntax.tex Thu Feb 28 18:09:04 2002 +0100 @@ -256,12 +256,14 @@ $\isarkeyword{syntax}$ (see \S\ref{sec:syn-trans}) support the full range of general mixfixes and binders. -\indexouternonterm{infix}\indexouternonterm{mixfix} +\indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix} \begin{rail} infix: '(' ('infix' | 'infixl' | 'infixr') string? nat ')' ; mixfix: infix | '(' string prios? nat? ')' | '(' 'binder' string prios? nat ')' ; + structmixfix: mixfix | '(' 'structure' ')' + ; prios: '[' (nat + ',') ']' ;