Locales: new element constrains, parameter renaming with syntax,
experimental command instantiate withdrawn.
--- a/NEWS Wed Jun 01 10:52:17 2005 +0200
+++ b/NEWS Wed Jun 01 12:30:49 2005 +0200
@@ -141,8 +141,11 @@
- Fixed parameter management in theorem generation for goals with "includes".
INCOMPATIBILITY: rarely, the generated theorem statement is different.
-* Locales: locale expressions permit optional mixfix redeclaration for
- renamed parameters.
+* Locales: new context element "constrains" for adding type constraints
+ to parameters.
+
+* Locales: context expressions permit optional syntax redeclaration when
+ renaming parameters.
* Locales: new commands for the interpretation of locale expressions
in theories (interpretation) and proof contexts (interpret). These take an
@@ -155,6 +158,9 @@
Use print_interps to inspect active interpretations of a particular locale.
For details, see the Isar Reference manual.
+* Locales: INCOMPATIBILITY: experimental command "instantiate" has
+ been withdrawn. Use "interpret" instead.
+
* Locales: proper static binding of attribute syntax -- i.e. types /
terms / facts mentioned as arguments are always those of the locale
definition context, independently of the context of later
--- a/doc-src/IsarRef/generic.tex Wed Jun 01 10:52:17 2005 +0200
+++ b/doc-src/IsarRef/generic.tex Wed Jun 01 12:30:49 2005 +0200
@@ -122,10 +122,12 @@
contextexpr: nameref | '(' contextexpr ')' |
(contextexpr (name mixfix? +)) | (contextexpr + '+')
;
- contextelem: fixes | assumes | defines | notes | includes
+ contextelem: fixes | constrains | assumes | defines | notes | includes
;
fixes: 'fixes' (name ('::' type)? structmixfix? + 'and')
;
+ constrains: 'constrains' (name '::' type + 'and')
+ ;
assumes: 'assumes' (thmdecl? props + 'and')
;
defines: 'defines' (thmdecl? prop proppat? + 'and')
@@ -168,6 +170,9 @@
declaration ``$(structure)$'' means that $x$ may be referenced
implicitly in this context.
+ \item [$\CONSTRAINS{~x::\tau}$] introduces a type constraint $\tau$
+ on the local parameter $x$.
+
\item [$\ASSUMES{a}{\vec\phi}$] introduces local premises, similar to
$\ASSUMENAME$ within a proof (cf.\ \S\ref{sec:proof-context}).
@@ -305,6 +310,15 @@
account when choosing attributes for local theorems.
\end{warn}
+\begin{warn}
+ An interpretation may subsume previous interpretations. A warning
+ is issued, since it is likely that these could have been generalized
+ in the first place. The locale package does not attempt to remove
+ subsumed interpretations. This situation is normally harmless, but
+ note that $blast$ gets confused by the presence of multiple axclass
+ instances a rule.
+\end{warn}
+
\section{Derived proof schemes}
--- a/doc-src/Locales/IsaMakefile Wed Jun 01 10:52:17 2005 +0200
+++ b/doc-src/Locales/IsaMakefile Wed Jun 01 12:30:49 2005 +0200
@@ -13,7 +13,7 @@
SRC = $(ISABELLE_HOME)/src
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log
-USEDIR = $(ISATOOL) usedir -i true -d "" -D generated
+USEDIR = $(ISATOOL) usedir -i true -d "" -H false -D generated
## Locales
@@ -23,7 +23,7 @@
HOL:
@cd $(SRC)/HOL; $(ISATOOL) make HOL
-$(LOG)/HOL-Locales.gz: $(OUT)/HOL Locales/ROOT.ML Locales/Locales.thy
+$(LOG)/HOL-Locales.gz: $(OUT)/HOL Locales/ROOT.ML Locales/Locales.thy Locales/document/root.tex Locales/document/root.bib
@$(USEDIR) $(OUT)/HOL Locales
--- a/doc-src/Locales/Locales/Locales.thy Wed Jun 01 10:52:17 2005 +0200
+++ b/doc-src/Locales/Locales/Locales.thy Wed Jun 01 12:30:49 2005 +0200
@@ -14,6 +14,9 @@
section {* Overview *}
text {*
+ The present text is based on~\cite{Ballarin2004a}. It was updated
+ for for Isabelle2005, but does not cover locale interpretation.
+
Locales are an extension of the Isabelle proof assistant. They
provide support for modular reasoning. Locales were initially
developed by Kamm\"uller~\cite{Kammuller2000} to support reasoning
@@ -129,9 +132,9 @@
Figure~\ref{fig-grammar}.
A key concept, introduced by Wenzel, is that
locales are (internally) lists
- of \emph{context elements}. There are four kinds, identified
- by the keywords \textbf{fixes}, \textbf{assumes}, \textbf{defines} and
- \textbf{notes}.
+ of \emph{context elements}. There are five kinds, identified
+ by the keywords \textbf{fixes}, \textbf{constrains},
+ \textbf{assumes}, \textbf{defines} and \textbf{notes}.
\begin{figure}
\hrule
@@ -146,13 +149,15 @@
& \textit{locale-expr1} ( ``\textbf{+}'' \textit{locale-expr1} )$^*$ \\
\textit{locale-expr1} & ::=
& ( \textit{qualified-name} $|$
- ``\textbf{(}'' \textit{locale-expr} ``\textbf{)}'' )
- ( \textit{name} $|$ ``\textbf{\_}'' )$^*$ \\
+ ``\textbf{(}'' \textit{locale-expr} ``\textbf{)}'' ) \\
+ & & ( \textit{name} [ \textit{mixfix} ] $|$ ``\textbf{\_}'' )$^*$ \\
\textit{fixes} & ::=
& \textit{name} [ ``\textbf{::}'' \textit{type} ]
[ ``\textbf{(}'' \textbf{structure} ``\textbf{)}'' $|$
\textit{mixfix} ] \\
+ \textit{constrains} & ::=
+ & \textit{name} ``\textbf{::}'' \textit{type} \\
\textit{assumes} & ::=
& [ \textit{attr-name} ``\textbf{:}'' ] \textit{proposition} \\
\textit{defines} & ::=
@@ -164,11 +169,16 @@
\textit{element} & ::=
& \textbf{fixes} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ \\
& |
+ & \textbf{constrains} \textit{constrains}
+ ( \textbf{and} \textit{constrains} )$^*$ \\
+ & |
& \textbf{assumes} \textit{assumes} ( \textbf{and} \textit{assumes} )$^*$ \\
& |
& \textbf{defines} \textit{defines} ( \textbf{and} \textit{defines} )$^*$ \\
& |
& \textbf{notes} \textit{notes} ( \textbf{and} \textit{notes} )$^*$ \\
+ \textit{element1} & ::=
+ & \textit{element} \\
& | & \textbf{includes} \textit{locale-expr} \\
\textit{locale} & ::=
@@ -191,7 +201,7 @@
& | & \textbf{declare} [ \textit{in-target} ] ( \textit{qualified-name}
[ \textit{attribute} ] )$^+$ \\
& | & \textit{theorem} \textit{proposition} \textit{proof} \\
- & | & \textit{theorem} \textit{element}$^*$
+ & | & \textit{theorem} \textit{element1}$^*$
\textbf{shows} \textit{proposition} \textit{proof} \\
& | & \textbf{print\_locale} \textit{locale} \\
& | & \textbf{print\_locales}
@@ -210,8 +220,7 @@
declaring a named locale, it is possible to \emph{import} another
named locale, or indeed several ones by importing a locale
expression. The second part of the declaration, also optional,
- consists of a number of context element declarations. Here, a fifth
- kind, \textbf{includes}, is available.
+ consists of a number of context element declarations.
A number of Isar commands have an additional, optional \emph{target}
argument, which always refers to a named locale. These commands
@@ -226,7 +235,7 @@
\textbf{theorem} (and related commands), theorems stored in the target
can be used in the associated proof scripts.
- The Locales package permits a \emph{long goals format} for
+ The Locales package provides a \emph{long goals format} for
propositions stated with \textbf{theorem} (and friends). While
normally a goal is just a formula, a long goal is a list of context
elements, followed by the keyword \textbf{shows}, followed by the
@@ -286,15 +295,15 @@
text {*
The parameter @{term prod} has a
- syntax annotation allowing the infix ``@{text "\<cdot>"}'' in the
+ syntax annotation enabling the infix ``@{text "\<cdot>"}'' in the
assumption of associativity. Parameters may have arbitrary mixfix
syntax, like constants. In the example, the type of @{term prod} is
specified explicitly. This is not necessary. If no type is
specified, a most general type is inferred simultaneously for all
parameters, taking into account all assumptions (and type
specifications of parameters, if present).%
-\footnote{Type inference also takes into account definitions and
- import, as introduced later.}
+\footnote{Type inference also takes into account type constraints,
+ definitions and import, as introduced later.}
Free variables in assumptions are implicitly universally quantified,
unless they are parameters. Hence the context defined by the locale
@@ -587,8 +596,8 @@
The expression is only well-formed if $n$ does not
exceed the number of parameters of $e$. Underscores denote
parameters that are not renamed.
- Parameters whose names are changed lose mixfix syntax,
- and there is currently no way to re-equip them with such.
+ Renaming by default removes mixfix syntax, but new syntax may be
+ specified.
\item[Merge.]
The locale expression $e_1 + e_2$ denotes
the locale obtained by merging the locales of $e_1$
@@ -615,16 +624,16 @@
specification of semigroup homomorphisms.
*}
-locale semi_hom = comm_semi sum + comm_semi +
+locale semi_hom = comm_semi sum (infixl "\<oplus>" 65) + comm_semi +
fixes hom
- assumes hom: "hom (sum x y) = hom x \<cdot> hom y"
+ assumes hom: "hom (x \<oplus> y) = hom x \<cdot> hom y"
text {*
This locale defines a context with three parameters @{text "sum"},
- @{text "prod"} and @{text "hom"}. Only the second parameter has
- mixfix syntax. The first two are associative operations,
- the first of type @{typ "['a, 'a] \<Rightarrow> 'a"}, the second of
- type @{typ "['b, 'b] \<Rightarrow> 'b"}.
+ @{text "prod"} and @{text "hom"}. The first two parameters have
+ mixfix syntax. They are associative operations,
+ the first of type @{typeof [locale=semi_hom] prod}, the second of
+ type @{typeof [locale=semi_hom] sum}.
How are facts that are imported via a locale expression identified?
Facts are always introduced in a named locale (either in the
@@ -643,12 +652,12 @@
facts, though.
*}
-theorem (in semi_hom) "hom x \<cdot> (hom y \<cdot> hom z) = hom (sum x (sum y z))"
+theorem (in semi_hom) "hom x \<cdot> (hom y \<cdot> hom z) = hom (x \<oplus> (y \<oplus> z))"
proof -
have "hom x \<cdot> (hom y \<cdot> hom z) = hom y \<cdot> (hom x \<cdot> hom z)"
by (simp add: prod.lcomm)
- also have "\<dots> = hom (sum y (sum x z))" by (simp add: hom)
- also have "\<dots> = hom (sum x (sum y z))" by (simp add: sum.lcomm)
+ also have "\<dots> = hom (y \<oplus> (x \<oplus> z))" by (simp add: hom)
+ also have "\<dots> = hom (x \<oplus> (y \<oplus> z))" by (simp add: sum.lcomm)
finally show ?thesis .
qed
@@ -822,15 +831,16 @@
and the list of context elements
\[
\begin{array}{ll}
- \textbf{fixes} & @{text sum} :: @{typ [quotes] "['a, 'a] \<Rightarrow> 'a"} \\
+ \textbf{fixes} & @{text sum} :: @{typ [quotes] "['a, 'a] \<Rightarrow> 'a"}
+ ~(\textbf{infixl}~@{text [quotes] "\<oplus>"}~65) \\
\textbf{assumes} & @{text [quotes] "semi sum"} \\
- \textbf{notes} & @{text sum.assoc}: @{text [quotes] "sum (sum ?x ?y) ?z
+ \textbf{notes} & @{text sum.assoc}: @{text [quotes] "(?x \<oplus> ?y) \<oplus> ?z
= sum ?x (sum ?y ?z)"} \\
\textbf{assumes} & @{text [quotes] "comm_semi_axioms sum"} \\
- \textbf{notes} & @{text sum.comm}: @{text [quotes] "sum ?x ?y = sum
- ?y ?x"} \\
- \textbf{notes} & @{text sum.lcomm}: @{text [quotes] "sum ?x (sum ?y ?z)
- = sum ?y (sum ?x ?z)"}
+ \textbf{notes} & @{text sum.comm}: @{text [quotes] "?x \<oplus> ?y =
+ ?y \<oplus> ?x"} \\
+ \textbf{notes} & @{text sum.lcomm}: @{text [quotes] "?x \<oplus> (?y \<oplus> ?z)
+ = ?y \<oplus> (?x \<oplus> ?z)"}
\end{array}
\]
@@ -867,14 +877,15 @@
Hence $\C(@{text "semi_hom"})$, shown below, is again well-formed.
\[
\begin{array}{ll}
- \textbf{fixes} & @{text sum} :: @{typ [quotes] "['a, 'a] \<Rightarrow> 'a"} \\
+ \textbf{fixes} & @{text sum} :: @{typ [quotes] "['a, 'a] \<Rightarrow> 'a"}
+ ~(\textbf{infixl}~@{text [quotes] "\<oplus>"}~65) \\
\textbf{assumes} & @{text [quotes] "semi sum"} \\
- \textbf{notes} & @{text sum.assoc}: @{text [quotes] "sum (sum ?x ?y) ?z
- = sum ?x (sum ?y ?z)"} \\
+ \textbf{notes} & @{text sum.assoc}: @{text [quotes] "(?x \<oplus> ?y) \<oplus> ?z
+ = ?x \<oplus> (?y \<oplus> ?z)"} \\
\textbf{assumes} & @{text [quotes] "comm_semi_axioms sum"} \\
- \textbf{notes} & @{text sum.comm}: @{text [quotes] "sum ?x ?y = sum ?y ?x"} \\
- \textbf{notes} & @{text sum.lcomm}: @{text [quotes] "sum ?x (sum ?y ?z)
- = sum ?y (sum ?x ?z)"} \\
+ \textbf{notes} & @{text sum.comm}: @{text [quotes] "?x \<oplus> ?y = ?y \<oplus> ?x"} \\
+ \textbf{notes} & @{text sum.lcomm}: @{text [quotes] "?x \<oplus> (?y \<oplus> ?z)
+ = ?y \<oplus> (?x \<oplus> ?z)"} \\
\textbf{fixes} & @{text prod} :: @{typ [quotes] "['b, 'b] \<Rightarrow> 'b"}
~(\textbf{infixl}~@{text [quotes] "\<cdot>"}~70) \\
\textbf{assumes} & @{text [quotes] "semi prod"} \\
@@ -887,7 +898,7 @@
\textbf{fixes} & @{text hom} :: @{typ [quotes] "'a \<Rightarrow> 'b"} \\
\textbf{assumes} & @{text [quotes] "semi_hom_axioms sum"} \\
\textbf{notes} & @{text "sum_prod_hom.hom"}:
- @{text "hom (sum x y) = hom x \<cdot> hom y"}
+ @{text "hom (x \<oplus> y) = hom x \<cdot> hom y"}
\end{array}
\]
@@ -959,11 +970,17 @@
particular mixfix syntax is required.
Its definition is
\begin{center}
- \textbf{locale} \textit{var} = \textbf{fixes} @{text "x_"}
+ \textbf{locale} @{text var} = \textbf{fixes} @{text "x_"}
\end{center}
- The use of the internal variable @{text "x_"}
+ The use of the internal variable @{text "x_"}
enforces that the parameter is renamed before being used, because
- internal variables may not occur in the input syntax.
+ internal variables may not occur in the input syntax. Using
+ @{text var}, the locale @{text magma} could have been replaced by
+ the locale expression
+\begin{center}
+ @{text var} @{text prod} (\textbf{infixl} @{text [quotes] \<cdot>} 70)
+\end{center}
+ in the above locale declarations.
*}
subsection {* Includes *}
@@ -971,20 +988,7 @@
text {*
\label{sec-includes}
The context element \textbf{includes} takes a locale expression $e$
- as argument. It can occur at any point in a locale declaration, and
- it adds $\C(e)$ to the current context.
-
- If \textbf{includes} $e$ appears as context element in the
- declaration of a named locale $l$, the included context is only
- visible in subsequent context elements, but it is not propagated to
- $l$. That is, if $l$ is later used as a target, context elements
- from $\C(e)$ are not added to the context. Although it is
- conceivable that this mechanism could be used to add only selected
- facts from $e$ to $l$ (with \textbf{notes} elements following
- \textbf{includes} $e$), currently no useful applications of this are
- known.
-
- The more common use of \textbf{includes} $e$ is in long goals, where it
+ as argument. It can only occur in long goals, where it
adds, like a target, locale context to the proof context. Unlike
with targets, the proved theorem is not stored
in the locale. Instead, it is exported immediately.
@@ -1049,13 +1053,10 @@
effective in the context of a locale, and only if the first argument
is a
\emph{structural} parameter --- that is, a parameter with annotation
- \textbf{(structure)}. The token has the effect of replacing the
- parameter with a subscripted number, the index of the structural
- parameter in the locale. This replacement takes place both for
- printing and
- parsing. Subscripted $1$ for the first structural
- parameter may be omitted, as in this specification of semigroups with
- structures:
+ \textbf{(structure)}. The token has the effect of subscripting the
+ parameter --- by bracketing it between \verb.\<^bsub>. and \verb.\<^esub>..
+ Additionally, the subscript of the first structural parameter may be
+ omitted, as in this specification of semigroups with structures:
*}
locale comm_semi' =
@@ -1063,22 +1064,20 @@
assumes assoc: "(x \<star> y) \<star> z = x \<star> (y \<star> z)" and comm: "x \<star> y = y \<star> x"
text {*
- Here @{text "x \<star> y"} is equivalent to @{text "x \<star>\<^sub>1 y"} and
- abbreviates @{term "s_op G x y"}. A specification of homomorphisms
+ Here @{text "x \<star> y"} is equivalent to @{text "x \<star>\<^bsub>G\<^esub> y"} and
+ abbreviates @{text "s_op G x y"}. A specification of homomorphisms
requires a second structural parameter.
*}
locale semi'_hom = comm_semi' + comm_semi' H +
fixes hom
- assumes hom: "hom (x \<star> y) = hom x \<star>\<^sub>2 hom y"
+ assumes hom: "hom (x \<star> y) = hom x \<star>\<^bsub>H\<^esub> hom y"
text {*
The parameter @{text H} is defined in the second \textbf{fixes}
- element of $\C(@{term "semi'_comm"})$. Hence @{text "\<star>\<^sub>2"}
- abbreviates @{term "s_op H x y"}. The same construction can be done
- with records instead of an \textit{ad-hoc} type. In general, the
- $i$th structural parameter is addressed by index $i$. Only the
- index $1$ may be omitted. *}
+ element of $\C(@{term "semi'_comm"})$. Hence @{text "\<star>\<^bsub>H\<^esub>"}
+ abbreviates @{text "s_op H x y"}. The same construction can be done
+ with records instead of an \textit{ad-hoc} type. *}
record 'a semi = prod :: "['a, 'a] \<Rightarrow> 'a" (infixl "\<bullet>\<index>" 70)
@@ -1119,7 +1118,7 @@
section {* Conclusions and Outlook *}
text {*
- Locales provide a simple means of modular reasoning. They allow to
+ Locales provide a simple means of modular reasoning. They enable to
abbreviate frequently occurring context statements and maintain facts
valid in these contexts. Importantly, using structures, they allow syntax to be
effective only in certain contexts, and thus to mimic common
@@ -1157,7 +1156,7 @@
A detailed comparison of locales with module systems in type theory
has not been undertaken yet, but could be beneficial. For example,
a module system for Coq has recently been presented by Chrzaszcz
- \cite{Chrzaszcz2003}. While the
+ \cite{Chrzaszcz2003,Chrzaszcz2004}. While the
latter usually constitute extensions of the calculus, locales are
a rather thin layer that does not change Isabelle's meta logic.
Locales mainly manage specifications and facts. Functors, like
--- a/doc-src/Locales/Locales/document/root.bib Wed Jun 01 10:52:17 2005 +0200
+++ b/doc-src/Locales/Locales/document/root.bib Wed Jun 01 12:30:49 2005 +0200
@@ -32,8 +32,7 @@
title = "Types for Proofs and Programs: International Workshop, {TYPES} '98, {Kloster Irsee, Germany, March 27--31, 1998}, Selected Papers",
booktitle = "TYPES '98",
publisher = "Springer",
- series = "LNCS",
- number = 1657,
+ series = "LNCS 1657",
year = 1999
}
% CADE-17
@@ -51,8 +50,7 @@
title = "17th International Conference on Automated Deduction, Pittsburgh, PA, USA, June 17--20, 2000: Proceedings",
booktitle = "CADE 17",
publisher = "Springer",
- series = "LNCS",
- number = 1831,
+ series = "LNCS 1831",
year = 2000
}
@@ -60,8 +58,7 @@
author = "Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel",
title = "{Isabelle/HOL}: A Proof Assistant for Higher-Order Logic",
publisher = "Springer",
- series = "LNCS",
- number = 2283,
+ series = "LNCS 2283",
year = 2002,
available = { CB }
}
@@ -80,8 +77,7 @@
title = "Types for Proofs and Programs (TYPES 2002)",
booktitle = "TYPES 2002",
publisher = "Springer",
- series = "LNCS",
- number = 2646,
+ series = "LNCS 2646",
year = 2003
}
@@ -110,7 +106,7 @@
% TPHOLs 2003
@inproceedings{Chrzaszcz2003,
- author = "Jacek Chrzaszcz",
+ author = "Jacek Chrz{\c{a}}szcz",
title = "Implementing Modules in the {Coq} System",
pages = "270--286",
crossref = "BasinWolff2003",
@@ -122,8 +118,7 @@
title = "Theorem proving in higher order logics: 16th International Conference, TPHOLs 2003, Rome, Italy, September 2003: proceedings",
booktitle = "TPHOLs 2003",
publisher = "Springer",
- series = "LNCS",
- number = 2758,
+ series = "LNCS 2758",
year = 2003
}
@@ -148,7 +143,31 @@
title = {Tools and Algorithms for Construction and Analysis of Systems, 6th International Conference, TACAS 2000, Berlin, Germany, March 25 -- April 2, 2000, Proceedings},
booktitle = "TACAS 2000",
publisher = {Springer},
- series = {LNCS},
- number = {1785},
+ series = {LNCS 1785},
year = {2000},
-}
\ No newline at end of file
+}
+
+% TYPES 2004
+
+@inproceedings{Ballarin2004a,
+ author = "Clemens Ballarin",
+ title = "Locales and Locale Expressions in {Isabelle/Isar}",
+ pages = "34--50",
+ crossref = "BerardiEtAl2004"
+}
+
+@inproceedings{Chrzaszcz2004,
+ author = "Jacek Chrz{\c{a}}szcz",
+ title = "Modules in {Coq} Are and Will Be Correct",
+ pages = "130--136",
+ crossref = "BerardiEtAl2004",
+ available = { CB }
+}
+@proceedings{BerardiEtAl2004,
+ editor = "Stefano Berardi and Mario Coppo and Ferruccio Damiani",
+ title = "Types for Proofs and Programs, TYPES 2003, Torino, Italy",
+ booktitle = "Types for Proofs and Programs, TYPES 2003, Torino, Italy",
+ publisher = "Springer",
+ series = "LNCS 3085",
+ year = 2004
+}
--- a/doc-src/Locales/Makefile Wed Jun 01 10:52:17 2005 +0200
+++ b/doc-src/Locales/Makefile Wed Jun 01 12:30:49 2005 +0200
@@ -16,7 +16,7 @@
NAME = locales
-FILES = locales.tex Locales/generated/root.bib \
+FILES = Locales/generated/root.tex Locales/generated/root.bib \
Locales/generated/session.tex Locales/generated/Locales.tex \
Locales/generated/isabelle.sty Locales/generated/isabellesym.sty \
Locales/generated/pdfsetup.sty
@@ -24,17 +24,19 @@
dvi: $(NAME).dvi
$(NAME).dvi: $(FILES)
- env TEXINPUTS=$(TEXPATH) $(LATEX) $(NAME)
- env BIBINPUTS=$(TEXPATH) $(BIBTEX) $(NAME)
- env TEXINPUTS=$(TEXPATH) $(LATEX) $(NAME)
- env TEXINPUTS=$(TEXPATH) $(LATEX) $(NAME)
- env TEXINPUTS=$(TEXPATH) $(LATEX) $(NAME)
+ env TEXINPUTS=$(TEXPATH) $(LATEX) root
+ env BIBINPUTS=$(TEXPATH) $(BIBTEX) root
+ env TEXINPUTS=$(TEXPATH) $(LATEX) root
+ env TEXINPUTS=$(TEXPATH) $(LATEX) root
+ env TEXINPUTS=$(TEXPATH) $(LATEX) root
+ mv root.dvi $(NAME).dvi
pdf: $(NAME).pdf
$(NAME).pdf: $(FILES)
- env TEXINPUTS=$(TEXPATH) $(PDFLATEX) $(NAME)
- env BIBINPUTS=$(TEXPATH) $(BIBTEX) $(NAME)
- env TEXINPUTS=$(TEXPATH) $(PDFLATEX) $(NAME)
- env TEXINPUTS=$(TEXPATH) $(PDFLATEX) $(NAME)
- env TEXINPUTS=$(TEXPATH) $(PDFLATEX) $(NAME)
+ env TEXINPUTS=$(TEXPATH) $(PDFLATEX) root
+ env BIBINPUTS=$(TEXPATH) $(BIBTEX) root
+ env TEXINPUTS=$(TEXPATH) $(PDFLATEX) root
+ env TEXINPUTS=$(TEXPATH) $(PDFLATEX) root
+ env TEXINPUTS=$(TEXPATH) $(PDFLATEX) root
+ mv root.pdf $(NAME).pdf
--- a/doc-src/Locales/locales.tex Wed Jun 01 10:52:17 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,48 +0,0 @@
-\documentclass[leqno]{article}
-\usepackage{isabelle,isabellesym}
-
-\usepackage{amsmath}
-\usepackage{amssymb}
-\usepackage{array}
-
-% this should be the last package used
-\usepackage{pdfsetup}
-
-\urlstyle{rm}
-\isabellestyle{tt}
-%\renewcommand{\isacharunderscore}{\_}%
-% the latter is not necessary with \isabellestyle{tt}
-
-\begin{document}
-
-\title{Locales and Locale Expressions in Isabelle/Isar}
-\author{Clemens Ballarin \\
- Fakult\"at f\"ur Informatik \\ Technische Universit\"at M\"unchen \\
- 85748 Garching, Germany \\
- ballarin@in.tum.de}
-\date{}
-
-\maketitle
-
-\begin{abstract}
- Locales provide a module system for the Isabelle proof assistant.
- Recently, locales have been ported to the new Isar format for
- structured proofs. At the same time, they have been extended by
- locale expressions, a language for composing locale specifications,
- and by structures, which provide syntax for algebraic structures.
- The present paper presents both and is suitable as a tutorial to
- locales in Isar, because it covers both basics and recent
- extensions, and contains many examples.
-\end{abstract}
-
-%\tableofcontents
-
-\parindent 0pt\parskip 0.5ex
-
-% include generated text of all theories
-\input{session}
-
-\bibliographystyle{plain}
-\bibliography{root}
-
-\end{document}
--- a/doc-src/isar.sty Wed Jun 01 10:52:17 2005 +0200
+++ b/doc-src/isar.sty Wed Jun 01 12:30:49 2005 +0200
@@ -42,6 +42,7 @@
\newcommand{\WITHNAME}{\isarkeyword{with}}
\newcommand{\USINGNAME}{\isarkeyword{using}}
\newcommand{\FIXESNAME}{\isarkeyword{fixes}}
+\newcommand{\CONSTRAINSNAME}{\isarkeyword{constrains}}
\newcommand{\ASSUMESNAME}{\isarkeyword{assumes}}
\newcommand{\DEFINESNAME}{\isarkeyword{defines}}
\newcommand{\NOTESNAME}{\isarkeyword{notes}}
@@ -86,6 +87,7 @@
\newcommand{\WITH}[1]{\WITHNAME~#1}
\newcommand{\USING}[1]{\USINGNAME~#1}
\newcommand{\FIXES}[1]{\FIXESNAME~#1}
+\newcommand{\CONSTRAINS}[1]{\CONSTRAINSNAME~#1}
\newcommand{\ASSUMES}[2]{\ASSUMESNAME\I@optname{#1}~#2}
\newcommand{\DEFINES}[2]{\DEFINESNAME\I@optname{#1}~#2}
\newcommand{\NOTES}[2]{\NOTESNAME~\ifthenelse{\equal{}{#1}}{}{#1=}#2}
--- a/etc/isar-keywords-ZF.el Wed Jun 01 10:52:17 2005 +0200
+++ b/etc/isar-keywords-ZF.el Wed Jun 01 12:30:49 2005 +0200
@@ -73,7 +73,6 @@
"inductive_cases"
"init_toplevel"
"instance"
- "instantiate"
"interpret"
"interpretation"
"judgment"
@@ -192,6 +191,7 @@
"case_eqns"
"con_defs"
"concl"
+ "constrains"
"defines"
"domains"
"elimination"
@@ -413,7 +413,6 @@
(defconst isar-keywords-proof-decl
'("also"
- "instantiate"
"let"
"moreover"
"note"
--- a/etc/isar-keywords.el Wed Jun 01 10:52:17 2005 +0200
+++ b/etc/isar-keywords.el Wed Jun 01 12:30:49 2005 +0200
@@ -76,7 +76,6 @@
"inductive_cases"
"init_toplevel"
"instance"
- "instantiate"
"interpret"
"interpretation"
"judgment"
@@ -202,6 +201,7 @@
"compose"
"concl"
"congs"
+ "constrains"
"defines"
"distinct"
"files"
@@ -447,7 +447,6 @@
(defconst isar-keywords-proof-decl
'("also"
- "instantiate"
"let"
"moreover"
"note"
--- a/src/FOL/IsaMakefile Wed Jun 01 10:52:17 2005 +0200
+++ b/src/FOL/IsaMakefile Wed Jun 01 12:30:49 2005 +0200
@@ -47,7 +47,6 @@
$(LOG)/FOL-ex.gz: $(OUT)/FOL ex/First_Order_Logic.thy \
ex/If.thy ex/IffOracle.ML ex/IffOracle.thy ex/List.ML ex/List.thy \
ex/LocaleTest.thy \
- ex/LocaleInst.thy \
ex/Nat.ML ex/Nat.thy ex/Nat2.ML ex/Nat2.thy ex/Natural_Numbers.thy \
ex/Prolog.ML ex/Prolog.thy ex/ROOT.ML ex/Classical.thy ex/document/root.tex\
ex/foundn.ML ex/Intuitionistic.thy ex/intro.ML ex/prop.ML ex/quant.ML
--- a/src/FOL/ex/LocaleInst.thy Wed Jun 01 10:52:17 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,133 +0,0 @@
-(* Title: FOL/ex/LocaleInst.thy
- ID: $Id$
- Author: Clemens Ballarin
- Copyright (c) 2004 by Clemens Ballarin
-
-Test of locale instantiation mechanism, also provides a few examples.
-*)
-
-header {* Test of Locale instantiation *}
-
-theory LocaleInst = FOL:
-
-ML {* set show_hyps *}
-
-subsection {* Locale without assumptions *}
-
-locale L1 = notes rev_conjI [intro] = conjI [THEN iffD1 [OF conj_commute]]
-
-lemma "[| A; B |] ==> A & B"
-proof -
- instantiate my: L1 txt {* No chained fact required. *}
- assume B and A txt {* order reversed *}
- then show "A & B" .. txt {* Applies @{thm my.rev_conjI}. *}
-qed
-
-locale L11 = notes rev_conjI = conjI [THEN iffD1 [OF conj_commute]]
-
-lemma "[| A; B |] ==> A & B"
-proof -
- instantiate [intro]: L11 txt {* Attribute supplied at instantiation. *}
- assume B and A
- then show "A & B" ..
-qed
-
-subsection {* Simple locale with assumptions *}
-
-typedecl i
-arities i :: "term"
-
-consts bin :: "[i, i] => i" (infixl "#" 60)
-
-axioms i_assoc: "(x # y) # z = x # (y # z)"
- i_comm: "x # y = y # x"
-
-locale L2 =
- fixes OP (infixl "+" 60)
- assumes assoc: "(x + y) + z = x + (y + z)"
- and comm: "x + y = y + x"
-
-lemma (in L2) lcomm: "x + (y + z) = y + (x + z)"
-proof -
- have "x + (y + z) = (x + y) + z" by (simp add: assoc)
- also have "... = (y + x) + z" by (simp add: comm)
- also have "... = y + (x + z)" by (simp add: assoc)
- finally show ?thesis .
-qed
-
-lemmas (in L2) AC = comm assoc lcomm
-
-lemma "(x::i) # y # z # w = y # x # w # z"
-proof -
- have "L2 (op #)" by (rule L2.intro [of "op #", OF i_assoc i_comm])
- then instantiate my: L2
- txt {* Chained fact required to discharge assumptions of @{text L2}
- and instantiate parameters. *}
- show ?thesis by (simp only: my.OP.AC) (* or simply AC *)
-qed
-
-subsection {* Nested locale with assumptions *}
-
-locale L3 =
- fixes OP (infixl "+" 60)
- assumes assoc: "(x + y) + z = x + (y + z)"
-
-locale L4 = L3 +
- assumes comm: "x + y = y + x"
-
-lemma (in L4) lcomm: "x + (y + z) = y + (x + z)"
-proof -
- have "x + (y + z) = (x + y) + z" by (simp add: assoc)
- also have "... = (y + x) + z" by (simp add: comm)
- also have "... = y + (x + z)" by (simp add: assoc)
- finally show ?thesis .
-qed
-
-lemmas (in L4) AC = comm assoc lcomm
-
-text {* Conceptually difficult locale:
- 2nd context fragment contains facts with differing metahyps. *}
-
-lemma L4_intro:
- fixes OP (infixl "+" 60)
- assumes assoc: "!!x y z. (x + y) + z = x + (y + z)"
- and comm: "!!x y. x + y = y + x"
- shows "L4 (op+)"
- by (blast intro: L4.intro L3.intro assoc L4_axioms.intro comm)
-
-lemma "(x::i) # y # z # w = y # x # w # z"
-proof -
- have "L4 (op #)" by (rule L4_intro [of "op #", OF i_assoc i_comm])
- then instantiate my: L4
- show ?thesis by (simp only: my.OP.AC) (* or simply AC *)
-qed
-
-subsection {* Locale with definition *}
-
-text {* This example is admittedly not very creative :-) *}
-
-locale L5 = L4 + var A +
- defines A_def: "A == True"
-
-lemma (in L5) lem: A
- by (unfold A_def) rule
-
-lemma "L5(op #) ==> True"
-proof -
- assume "L5(op #)"
- then instantiate my: L5
- show ?thesis by (rule lem) (* lem instantiated to True *)
-qed
-
-subsection {* Instantiation in a context with target *}
-
-lemma (in L4) (* Target might confuse instantiation command. *)
- fixes A (infixl "$" 60)
- assumes A: "L4(A)"
- shows "(x::i) $ y $ z $ w = y $ x $ w $ z"
-proof -
- from A instantiate A: L4
- show ?thesis by (simp only: A.OP.AC)
-qed
-
-end
--- a/src/FOL/ex/LocaleTest.thy Wed Jun 01 10:52:17 2005 +0200
+++ b/src/FOL/ex/LocaleTest.thy Wed Jun 01 12:30:49 2005 +0200
@@ -13,16 +13,21 @@
begin
ML {* set quick_and_dirty *} (* allow for thm command in batch mode *)
-ML {* reset Toplevel.debug *}
+ML {* set Toplevel.debug *}
ML {* set show_hyps *}
ML {* set show_sorts *}
section {* Renaming with Syntax *}
-locale S = var mult +
+
+locale (open) S = var mult +
assumes "mult(x, y) = mult(y, x)"
+(* Making this declaration (open) reveals a problem when mixing open and
+ closed locales. *)
-locale S' = S mult (infixl "**" 60)
+print_locale S
+
+locale (open) S' = S mult (infixl "**" 60)
print_locale S'
@@ -32,17 +37,16 @@
locale U = T mult (infixl "**" 60) + T add (infixl "++" 55) + var h +
assumes hom: "h(x ** y) = h(x) ++ h(y)"
-locale var' = fixes x :: "'a => 'b"
+locale V = U _ add
-(* doesn't work in FOL, but should in HOL *)
-(* locale T' = var' mult (infixl "**" 60) *)
+
+section {* Constrains *}
-locale V = U _ add
-print_locale V
-
-locale T' = fixes mult assumes "mult(x, y) = mult(y, x)"
-locale U' = T' mult + T' add + var h +
- assumes hom: "h(mult(x, y)) = add(h(x), h(y))"
+locale Z = fixes a (structure)
+locale Z' = Z +
+ constrains a :: "'a => 'b"
+ assumes "a (x :: 'a) = a (y)"
+print_locale Z'
section {* Interpretation *}
--- a/src/FOL/ex/ROOT.ML Wed Jun 01 10:52:17 2005 +0200
+++ b/src/FOL/ex/ROOT.ML Wed Jun 01 12:30:49 2005 +0200
@@ -13,7 +13,7 @@
time_use "foundn.ML";
time_use_thy "Prolog";
-time_use_thy "LocaleInst";
+time_use_thy "LocaleTest";
writeln"\n** Intuitionistic examples **\n";
time_use_thy "Intuitionistic";
--- a/src/Pure/Isar/isar_syn.ML Wed Jun 01 10:52:17 2005 +0200
+++ b/src/Pure/Isar/isar_syn.ML Wed Jun 01 12:30:49 2005 +0200
@@ -386,11 +386,6 @@
OuterSyntax.command "using" "augment goal facts" K.prf_decl
(facts >> (Toplevel.print oo (Toplevel.proof o IsarThy.using_facts)));
-val instantiateP =
- OuterSyntax.command "instantiate" "instantiate locale" K.prf_decl
- (P.opt_thm_name ":" -- P.xname
- >> (Toplevel.print oo (Toplevel.proof o IsarThy.instantiate_locale)));
-
(* proof context *)
@@ -785,9 +780,9 @@
val _ = OuterSyntax.add_keywords
["!", "!!", "%", "%%", "(", ")", "+", ",", "--", ":", "::", ";", "<",
"<=", "=", "==", "=>", "?", "[", "]", "advanced", "and", "assumes", "begin",
- "binder", "concl", "defines", "files", "fixes", "imports", "in", "includes",
- "infix", "infixl", "infixr", "is", "notes", "open", "output",
- "overloaded", "shows", "structure", "where", "|", "\\<equiv>",
+ "binder", "concl", "constrains", "defines", "files", "fixes", "imports",
+ "in", "includes", "infix", "infixl", "infixr", "is", "notes", "open",
+ "output", "overloaded", "shows", "structure", "where", "|", "\\<equiv>",
"\\<leftharpoondown>", "\\<rightharpoonup>",
"\\<rightleftharpoons>", "\\<subseteq>"];
@@ -813,7 +808,8 @@
forget_proofP, deferP, preferP, applyP, apply_endP, proofP, alsoP,
finallyP, moreoverP, ultimatelyP, backP, cannot_undoP, clear_undosP,
redoP, undos_proofP, undoP, killP, interpretationP, interpretP,
- instantiateP, (*diagnostic commands*) pretty_setmarginP,
+ (*diagnostic commands*)
+ pretty_setmarginP,
print_commandsP, print_contextP, print_theoryP, print_syntaxP,
print_theoremsP, print_localesP, print_localeP,
print_registrationsP, print_attributesP, print_simpsetP,