--- a/doc-src/Codegen/Thy/pictures/adaption.tex Fri Mar 27 15:14:31 2009 -0700
+++ b/doc-src/Codegen/Thy/pictures/adaption.tex Mon Mar 30 07:49:26 2009 -0700
@@ -6,6 +6,12 @@
\begin{document}
+\thispagestyle{empty}
+\setlength{\fboxrule}{0.01pt}
+\setlength{\fboxsep}{4pt}
+
+\fbox{
+
\begin{tikzpicture}[scale = 0.5]
\tikzstyle water=[color = blue, thick]
\tikzstyle ice=[color = black, very thick, cap = round, join = round, fill = white]
@@ -43,4 +49,6 @@
(adaption) -- (reserved);
\end{tikzpicture}
+}
+
\end{document}
--- a/doc-src/Codegen/Thy/pictures/architecture.tex Fri Mar 27 15:14:31 2009 -0700
+++ b/doc-src/Codegen/Thy/pictures/architecture.tex Mon Mar 30 07:49:26 2009 -0700
@@ -6,6 +6,12 @@
\begin{document}
+\thispagestyle{empty}
+\setlength{\fboxrule}{0.01pt}
+\setlength{\fboxsep}{4pt}
+
+\fbox{
+
\begin{tikzpicture}[x = 4.2cm, y = 1cm]
\tikzstyle entity=[rounded corners, draw, thick, color = black, fill = white];
\tikzstyle process=[ellipse, draw, thick, color = green, fill = white];
@@ -30,4 +36,6 @@
\draw [style=process_arrow] (seri) -- (Haskell);
\end{tikzpicture}
+}
+
\end{document}
--- a/doc-src/Locales/Locales/Examples.thy Fri Mar 27 15:14:31 2009 -0700
+++ b/doc-src/Locales/Locales/Examples.thy Mon Mar 30 07:49:26 2009 -0700
@@ -252,7 +252,8 @@
additionally outputs the conclusions.
The syntax of the locale commands discussed in this tutorial is
- shown in Table~\ref{tab:commands}. See the
+ shown in Table~\ref{tab:commands}. The grammer is complete with the
+ exception of additional context elements not discussed here. See the
Isabelle/Isar Reference Manual~\cite{IsarRef}
for full documentation. *}
--- a/doc-src/Locales/Locales/Examples1.thy Fri Mar 27 15:14:31 2009 -0700
+++ b/doc-src/Locales/Locales/Examples1.thy Mon Mar 30 07:49:26 2009 -0700
@@ -43,13 +43,12 @@
@{text partial_order} in the global context of the theory. The
parameter @{term le} is replaced by @{term "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"}. *}
- interpretation %visible nat!: partial_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
+ interpretation %visible nat: partial_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
txt {* The locale name is succeeded by a \emph{parameter
- instantiation}. In general, this is a list of terms, which refer to
+ instantiation}. This is a list of terms, which refer to
the parameters in the order of declaration in the locale. The
- locale name is preceded by an optional \emph{interpretation prefix},
- which is used to qualify names from the locale in the global
- context.
+ locale name is preceded by an optional \emph{interpretation
+ qualifier}.
The command creates the goal%
\footnote{Note that @{text op} binds tighter than functions
@@ -62,14 +61,12 @@
interpreted for natural numbers, for example @{thm [source]
nat.trans}: @{thm [display, indent=2] nat.trans}
- Interpretation accepts a qualifier, @{text nat} in the example,
- which is applied to all names processed by the interpretation. If
- followed by an exclamation point the qualifier is mandatory --- that
- is, the above theorem cannot be referred to simply by @{text trans}.
- A qualifier succeeded by an exclamation point is called
- \emph{strict}. It prevents unwanted hiding of theorems. It is
- advisable to use strict qualifiers for all interpretations in
- theories. *}
+ The interpretation qualifier, @{text nat} in the example, is applied
+ to all names processed by the interpretation. If a qualifer is
+ given in the \isakeyword{interpretation} command, its use is
+ mandatory when referencing the name. For example, the above theorem
+ cannot be referred to simply by @{text trans}. This prevents
+ unwanted hiding of theorems. *}
subsection {* Second Version: Replacement of Definitions *}
--- a/doc-src/Locales/Locales/Examples2.thy Fri Mar 27 15:14:31 2009 -0700
+++ b/doc-src/Locales/Locales/Examples2.thy Mon Mar 30 07:49:26 2009 -0700
@@ -7,7 +7,7 @@
\isakeyword{where} and require proofs. The revised command
that replaces @{text "\<sqsubset>"} by @{text "<"}, is: *}
-interpretation %visible nat!: partial_order "op \<le> :: [nat, nat] \<Rightarrow> bool"
+interpretation %visible nat: partial_order "op \<le> :: [nat, nat] \<Rightarrow> bool"
where "partial_order.less op \<le> (x::nat) y = (x < y)"
proof -
txt {* The goals are @{subgoals [display]}
--- a/doc-src/Locales/Locales/Examples3.thy Fri Mar 27 15:14:31 2009 -0700
+++ b/doc-src/Locales/Locales/Examples3.thy Mon Mar 30 07:49:26 2009 -0700
@@ -14,8 +14,8 @@
\isakeyword{interpret}). This interpretation is inside the proof of the global
interpretation. The third revision of the example illustrates this. *}
-interpretation %visible nat!: partial_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
- where "partial_order.less op \<le> (x::nat) y = (x < y)"
+interpretation %visible nat: partial_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
+ where nat_less_eq: "partial_order.less op \<le> (x::nat) y = (x < y)"
proof -
show "partial_order (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"
by unfold_locales auto
@@ -48,11 +48,12 @@
interpretation is reproduced in order to give an example of a more
elaborate interpretation proof. *}
-interpretation %visible nat!: lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
- where "lattice.meet op \<le> (x::nat) y = min x y"
- and "lattice.join op \<le> (x::nat) y = max x y"
+interpretation %visible nat: lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
+ where "partial_order.less op \<le> (x::nat) y = (x < y)"
+ and nat_meet_eq: "lattice.meet op \<le> (x::nat) y = min x y"
+ and nat_join_eq: "lattice.join op \<le> (x::nat) y = max x y"
proof -
- show "lattice (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"
+ show lattice: "lattice (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"
txt {* We have already shown that this is a partial order, *}
apply unfold_locales
txt {* hence only the lattice axioms remain to be shown: @{subgoals
@@ -61,20 +62,41 @@
txt {* the goals become @{subgoals [display]} which can be solved
by Presburger arithmetic. *}
by arith+
- txt {* In order to show the equations, we put ourselves in a
+ txt {* For the first of the equations, we refer to the theorem
+ generated in the previous interpretation. *}
+ show "partial_order.less op \<le> (x::nat) y = (x < y)"
+ by (rule nat_less_eq)
+ txt {* In order to show the remaining equations, we put ourselves in a
situation where the lattice theorems can be used in a convenient way. *}
- then interpret nat: lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool" .
+ from lattice interpret nat: lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool" .
show "lattice.meet op \<le> (x::nat) y = min x y"
by (bestsimp simp: nat.meet_def nat.is_inf_def)
show "lattice.join op \<le> (x::nat) y = max x y"
by (bestsimp simp: nat.join_def nat.is_sup_def)
qed
-text {* That the relation @{text \<le>} is a total order completes this
- sequence of interpretations. *}
+text {* The interpretation that the relation @{text \<le>} is a total
+ order follows next. *}
+
+interpretation %visible nat: total_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
+ where "partial_order.less op \<le> (x::nat) y = (x < y)"
+ and "lattice.meet op \<le> (x::nat) y = min x y"
+ and "lattice.join op \<le> (x::nat) y = max x y"
+proof -
+ show "total_order (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)" by unfold_locales arith
+qed (rule nat_less_eq nat_meet_eq nat_join_eq)+
-interpretation %visible nat!: total_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
- by unfold_locales arith
+text {* Note that since the locale hierarchy reflects that total
+ orders are distributive lattices, an explicit interpretation of
+ distributive lattices for the order relation on natural numbers is
+ only necessary for mapping the definitions to the right operators on
+ @{typ nat}. *}
+
+interpretation %visible nat: distrib_lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
+ where "partial_order.less op \<le> (x::nat) y = (x < y)"
+ and "lattice.meet op \<le> (x::nat) y = min x y"
+ and "lattice.join op \<le> (x::nat) y = max x y"
+ by unfold_locales [1] (rule nat_less_eq nat_meet_eq nat_join_eq)+
text {* Theorems that are available in the theory at this point are shown in
Table~\ref{tab:nat-lattice}.
@@ -98,29 +120,6 @@
\caption{Interpreted theorems for @{text \<le>} on the natural numbers.}
\label{tab:nat-lattice}
\end{table}
-
- Note that since the locale hierarchy reflects that total orders are
- distributive lattices, an explicit interpretation of distributive
- lattices for the order relation on natural numbers is not neccessary.
-
- Why not push this idea further and just give the last interpretation
- as a single interpretation instead of the sequence of three? The
- reasons for this are twofold:
-\begin{itemize}
-\item
- Often it is easier to work in an incremental fashion, because later
- interpretations require theorems provided by earlier
- interpretations.
-\item
- Assume that a definition is made in some locale $l_1$, and that $l_2$
- imports $l_1$. Let an equation for the definition be
- proved in an interpretation of $l_2$. The equation will be unfolded
- in interpretations of theorems added to $l_2$ or below in the import
- hierarchy, but not for theorems added above $l_2$.
- Hence, an equation interpreting a definition should always be given in
- an interpretation of the locale where the definition is made, not in
- an interpretation of a locale further down the hierarchy.
-\end{itemize}
*}
@@ -131,7 +130,7 @@
incrementally. *}
interpretation nat_dvd: partial_order "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
- where "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
+ where nat_dvd_less_eq: "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
proof -
show "partial_order (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool)"
by unfold_locales (auto simp: dvd_def)
@@ -146,11 +145,10 @@
divisibility. Instead, interpretation substitutes @{term "x dvd y \<and>
x \<noteq> y"}. *}
-interpretation nat_dvd!: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
- where nat_dvd_meet_eq:
- "lattice.meet op dvd = gcd"
- and nat_dvd_join_eq:
- "lattice.join op dvd = lcm"
+interpretation nat_dvd: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
+ where "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
+ and nat_dvd_meet_eq: "lattice.meet op dvd = gcd"
+ and nat_dvd_join_eq: "lattice.join op dvd = lcm"
proof -
show "lattice (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool)"
apply unfold_locales
@@ -161,6 +159,8 @@
apply (auto intro: lcm_dvd1 lcm_dvd2 lcm_least)
done
then interpret nat_dvd: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool" .
+ show "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
+ by (rule nat_dvd_less_eq)
show "lattice.meet op dvd = gcd"
apply (auto simp add: expand_fun_eq)
apply (unfold nat_dvd.meet_def)
@@ -199,13 +199,20 @@
lemma %invisible gcd_lcm_distr:
"gcd x (lcm y z) = lcm (gcd x y) (gcd x z)" sorry
-interpretation %visible nat_dvd!:
+interpretation %visible nat_dvd:
distrib_lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
- apply unfold_locales
- txt {* @{subgoals [display]} *}
- apply (unfold nat_dvd_meet_eq nat_dvd_join_eq)
- txt {* @{subgoals [display]} *}
- apply (rule gcd_lcm_distr) done
+ where "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
+ and "lattice.meet op dvd = gcd"
+ and "lattice.join op dvd = lcm"
+proof -
+ show "distrib_lattice (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool)"
+ apply unfold_locales
+ txt {* @{subgoals [display]} *}
+ apply (unfold nat_dvd_meet_eq nat_dvd_join_eq)
+ txt {* @{subgoals [display]} *}
+ apply (rule gcd_lcm_distr)
+ done
+qed (rule nat_dvd_less_eq nat_dvd_meet_eq nat_dvd_join_eq)+
text {* Theorems that are available in the theory after these
@@ -250,47 +257,47 @@
Inspecting the grammar of locale commands in
Table~\ref{tab:commands} reveals that the import of a locale can be
more than just a single locale. In general, the import is a
- \emph{locale expression}. Locale expressions enable to combine locales
- and rename parameters. A locale name is a locale expression. If
- $e_1$ and $e_2$ are locale expressions then $e_1 + e_2$ is their
- \emph{merge}. If $e$ is an expression, then $e~q_1 \ldots q_n$ is
- a \emph{renamed expression} where the parameters in $e$ are renamed
- to $q_1 \ldots q_n$. Using a locale expression, a locale for order
+ \emph{locale expression}. These enable to combine locales
+ and instantiate parameters. A locale expression is a sequence of
+ locale \emph{instances} followed by an optional \isakeyword{for}
+ clause. Each instance consists of a locale reference, which may be
+ preceded by a qualifer and succeeded by instantiations of the
+ parameters of that locale. Instantiations may be either positional
+ or through explicit parameter argument pairs.
+
+ Using a locale expression, a locale for order
preserving maps can be declared in the following way. *}
locale order_preserving =
- le: partial_order + le': partial_order le' for le' (infixl "\<preceq>" 50) +
+ le: partial_order le + le': partial_order le'
+ for le (infixl "\<sqsubseteq>" 50) and le' (infixl "\<preceq>" 50) +
fixes \<phi> :: "'a \<Rightarrow> 'b"
assumes hom_le: "x \<sqsubseteq> y \<Longrightarrow> \<phi> x \<preceq> \<phi> y"
-text {* The second line contains the expression, which is the
- merge of two partial order locales. The parameter of the second one
- is @{text le'} with new infix syntax @{text \<preceq>}. The
- parameters of the entire locale are @{text le}, @{text le'} and
- @{text \<phi>}. This is their \emph{canonical order},
- which is obtained by a left-to-right traversal of the expression,
- where only the new parameters are appended to the end of the list. The
- parameters introduced in the locale elements of the declaration
- follow.
+text {* The second and third line contain the expression --- two
+ instances of the partial order locale with instantiations @{text le}
+ and @{text le'}, respectively. The \isakeyword{for} clause consists
+ of parameter declarations and is similar to the context element
+ \isakeyword{fixes}. The notable difference is that the
+ \isakeyword{for} clause is part of the expression, and only
+ parameters defined in the expression may occur in its instances.
- In renamings parameters are referred to by position in the canonical
- order; an underscore is used to skip a parameter position, which is
- then not renamed. Renaming deletes the syntax of a parameter unless
- a new mixfix annotation is given.
+ Instances are \emph{morphisms} on locales. Their effect on the
+ parameters is naturally lifted to terms, propositions and theorems,
+ and thus to the assumptions and conclusions of a locale. The
+ assumption of a locale expression is the conjunction of the
+ assumptions of the instances. The conclusions of a sequence of
+ instances are obtained by appending the conclusions of the
+ instances in the order of the sequence.
- Parameter renamings are morphisms between locales. These can be
- lifted to terms and theorems and thus be applied to assumptions and
- conclusions. The assumption of a merge is the conjunction of the
- assumptions of the merged locale. The conclusions of a merge are
- obtained by appending the conclusions of the left locale and of the
- right locale. *}
-
-text {* The locale @{text order_preserving} contains theorems for both
- orders @{text \<sqsubseteq>} and @{text \<preceq>}. How can one refer to a theorem for
- a particular order, @{text \<sqsubseteq>} or @{text \<preceq>}? Names in locales are
- qualified by the locale parameters. More precisely, a name is
- qualified by the parameters of the locale in which its declaration
- occurs. Here are examples: *}
+ The qualifiers in the expression are already a familiar concept from
+ the \isakeyword{interpretation} command
+ (Section~\ref{sec:po-first}). Here, they serve to distinguish names
+ (in particular theorem names) for the two partial orders within the
+ locale. Qualifiers in the \isakeyword{locale} command (and in
+ \isakeyword{sublocale}) default to optional --- that is, they need
+ not occur in references to the qualified names. Here are examples
+ of theorems in locale @{text order_preserving}: *}
context %invisible order_preserving begin
@@ -300,16 +307,14 @@
@{thm [source] hom_le}: @{thm hom_le}
*}
-text {* When renaming a locale, the morphism is also applied
- to the qualifiers. Hence theorems for the partial order @{text \<preceq>}
+text {* The theorems for the partial order @{text \<preceq>}
are qualified by @{text le'}. For example, @{thm [source]
le'.less_le_trans}: @{thm [display, indent=2] le'.less_le_trans} *}
end %invisible
text {* This example reveals that there is no infix syntax for the strict
- version of @{text \<preceq>}! This can, of course, not be introduced
- automatically, but it can be declared manually through an abbreviation.
+ version of @{text \<preceq>}! This can be declared through an abbreviation.
*}
abbreviation (in order_preserving)
@@ -318,22 +323,39 @@
text (in order_preserving) {* Now the theorem is displayed nicely as
@{thm le'.less_le_trans}. *}
-text {* Not only names of theorems are qualified. In fact, all names
- are qualified, in particular names introduced by definitions and
- abbreviations. The name of the strict order of @{text \<sqsubseteq>} is @{text
- le.less} and therefore @{text le'.less} is the name of the strict
- order of @{text \<preceq>}. Hence, the equation in the above abbreviation
- could have been written as @{text "less' \<equiv> le'.less"}. *}
+text {* Qualifiers not only apply to theorem names, but also to names
+ introduced by definitions and abbreviations. In locale
+ @{text partial_order} the full name of the strict order of @{text \<sqsubseteq>} is
+ @{text le.less} and therefore @{text le'.less} is the full name of
+ the strict order of @{text \<preceq>}. Hence, the equation in the
+ abbreviation above could have been also written as @{text "less' \<equiv>
+ le'.less"}. *}
-text {* Two more locales illustrate working with locale expressions.
- A map @{text \<phi>} is a lattice homomorphism if it preserves meet and join. *}
+text {* Readers may find the declaration of locale @{text
+ order_preserving} a little awkward, because the declaration and
+ concrete syntax for @{text le} from @{text partial_order} are
+ repeated in the declaration of @{text order_preserving}. Locale
+ expressions provide a convenient short hand for this. A parameter
+ in an instance is \emph{untouched} if no instantiation term is
+ provided for it. In positional instantiations, a parameter position
+ may be skipped with an underscore, and it is allowed to give fewer
+ instantiation terms than the instantiated locale's number of
+ parameters. In named instantiations, instantiation pairs for
+ certain parameters may simply be omitted. Untouched parameters are
+ declared by the locale expression and with their concrete syntax by
+ implicitly adding them to the beginning of the \isakeyword{for}
+ clause.
- locale lattice_hom = le: lattice + le': lattice le' for le' (infixl "\<preceq>" 50) +
+ The following locales illustrate this. A map @{text \<phi>} is a
+ lattice homomorphism if it preserves meet and join. *}
+
+ locale lattice_hom =
+ le: lattice + le': lattice le' for le' (infixl "\<preceq>" 50) +
fixes \<phi>
assumes hom_meet:
- "\<phi> (lattice.meet le x y) = lattice.meet le' (\<phi> x) (\<phi> y)"
+ "\<phi> (x \<sqinter> y) = le'.meet (\<phi> x) (\<phi> y)"
and hom_join:
- "\<phi> (lattice.join le x y) = lattice.join le' (\<phi> x) (\<phi> y)"
+ "\<phi> (x \<squnion> y) = le'.join (\<phi> x) (\<phi> y)"
abbreviation (in lattice_hom)
meet' (infixl "\<sqinter>''" 50) where "meet' \<equiv> le'.meet"
@@ -342,8 +364,12 @@
text {* A homomorphism is an endomorphism if both orders coincide. *}
- locale lattice_end =
- lattice_hom le le for le (infixl "\<sqsubseteq>" 50)
+ locale lattice_end = lattice_hom _ le
+
+text {* In this declaration, the first parameter of @{text
+ lattice_hom}, @{text le}, is untouched and then used to instantiate
+ the second parameter. Its concrete syntax is preserved. *}
+
text {* The inheritance diagram of the situation we have now is shown
in Figure~\ref{fig:hom}, where the dashed line depicts an
@@ -390,7 +416,7 @@
text {* It can be shown easily that a lattice homomorphism is order
preserving. As the final example of this section, a locale
- interpretation is used to assert this. *}
+ interpretation is used to assert this: *}
sublocale lattice_hom \<subseteq> order_preserving proof unfold_locales
fix x y
@@ -404,6 +430,7 @@
Theorems and other declarations --- syntax, in particular --- from
the locale @{text order_preserving} are now active in @{text
lattice_hom}, for example
+
@{thm [source] le'.less_le_trans}:
@{thm le'.less_le_trans}
*}
@@ -423,7 +450,7 @@
Haftmann and Wenzel \cite{HaftmannWenzel2007} overcome a restriction
of axiomatic type classes through a combination with locale
interpretation. The result is a Haskell-style class system with a
- facility to generate Haskell code. Classes are sufficient for
+ facility to generate ML and Haskell code. Classes are sufficient for
simple specifications with a single type parameter. The locales for
orders and lattices presented in this tutorial fall into this
category. Order preserving maps, homomorphisms and vector spaces,
@@ -447,7 +474,7 @@
& \textit{name} $|$ \textit{attribute} $|$
\textit{name} \textit{attribute} \\
\textit{qualifier} & ::=
- & \textit{name} [``\textbf{!}''] \\[2ex]
+ & \textit{name} [``\textbf{?}'' $|$ ``\textbf{!}''] \\[2ex]
\multicolumn{3}{l}{Context Elements} \\
@@ -493,7 +520,7 @@
& \textbf{where} \textit{name} ``\textbf{=}'' \textit{term}
( \textbf{and} \textit{name} ``\textbf{=}'' \textit{term} )$^*$ \\
\textit{instance} & ::=
- & [ \textit{qualifier} \textbf{:} ]
+ & [ \textit{qualifier} ``\textbf{:}'' ]
\textit{qualified-name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\
\textit{expression} & ::=
& \textit{instance} ( ``\textbf{+}'' \textit{instance} )$^*$
--- a/doc-src/Locales/Locales/document/Examples.tex Fri Mar 27 15:14:31 2009 -0700
+++ b/doc-src/Locales/Locales/document/Examples.tex Mon Mar 30 07:49:26 2009 -0700
@@ -481,7 +481,8 @@
additionally outputs the conclusions.
The syntax of the locale commands discussed in this tutorial is
- shown in Table~\ref{tab:commands}. See the
+ shown in Table~\ref{tab:commands}. The grammer is complete with the
+ exception of additional context elements not discussed here. See the
Isabelle/Isar Reference Manual~\cite{IsarRef}
for full documentation.%
\end{isamarkuptext}%
--- a/doc-src/Locales/Locales/document/Examples1.tex Fri Mar 27 15:14:31 2009 -0700
+++ b/doc-src/Locales/Locales/document/Examples1.tex Mon Mar 30 07:49:26 2009 -0700
@@ -72,14 +72,13 @@
%
\isatagvisible
\isacommand{interpretation}\isamarkupfalse%
-\ nat{\isacharbang}{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}%
+\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}%
\begin{isamarkuptxt}%
The locale name is succeeded by a \emph{parameter
- instantiation}. In general, this is a list of terms, which refer to
+ instantiation}. This is a list of terms, which refer to
the parameters in the order of declaration in the locale. The
- locale name is preceded by an optional \emph{interpretation prefix},
- which is used to qualify names from the locale in the global
- context.
+ locale name is preceded by an optional \emph{interpretation
+ qualifier}.
The command creates the goal%
\footnote{Note that \isa{op} binds tighter than functions
@@ -104,14 +103,12 @@
\ \ {\isasymlbrakk}{\isacharquery}x\ {\isasymle}\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasymle}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isasymle}\ {\isacharquery}z%
\end{isabelle}
- Interpretation accepts a qualifier, \isa{nat} in the example,
- which is applied to all names processed by the interpretation. If
- followed by an exclamation point the qualifier is mandatory --- that
- is, the above theorem cannot be referred to simply by \isa{trans}.
- A qualifier succeeded by an exclamation point is called
- \emph{strict}. It prevents unwanted hiding of theorems. It is
- advisable to use strict qualifiers for all interpretations in
- theories.%
+ The interpretation qualifier, \isa{nat} in the example, is applied
+ to all names processed by the interpretation. If a qualifer is
+ given in the \isakeyword{interpretation} command, its use is
+ mandatory when referencing the name. For example, the above theorem
+ cannot be referred to simply by \isa{trans}. This prevents
+ unwanted hiding of theorems.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/Locales/Locales/document/Examples2.tex Fri Mar 27 15:14:31 2009 -0700
+++ b/doc-src/Locales/Locales/document/Examples2.tex Mon Mar 30 07:49:26 2009 -0700
@@ -32,7 +32,7 @@
%
\isatagvisible
\isacommand{interpretation}\isamarkupfalse%
-\ nat{\isacharbang}{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ {\isacharbrackleft}nat{\isacharcomma}\ nat{\isacharbrackright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
+\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ {\isacharbrackleft}nat{\isacharcomma}\ nat{\isacharbrackright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharminus}%
--- a/doc-src/Locales/Locales/document/Examples3.tex Fri Mar 27 15:14:31 2009 -0700
+++ b/doc-src/Locales/Locales/document/Examples3.tex Mon Mar 30 07:49:26 2009 -0700
@@ -41,8 +41,8 @@
%
\isatagvisible
\isacommand{interpretation}\isamarkupfalse%
-\ nat{\isacharbang}{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
-\ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
+\ \ \isakeyword{where}\ nat{\isacharunderscore}less{\isacharunderscore}eq{\isacharcolon}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharminus}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
@@ -104,13 +104,14 @@
%
\isatagvisible
\isacommand{interpretation}\isamarkupfalse%
-\ nat{\isacharbang}{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
-\ \ \isakeyword{where}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ min\ x\ y{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ max\ x\ y{\isachardoublequoteclose}\isanewline
+\ nat{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
+\ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{and}\ nat{\isacharunderscore}meet{\isacharunderscore}eq{\isacharcolon}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ min\ x\ y{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{and}\ nat{\isacharunderscore}join{\isacharunderscore}eq{\isacharcolon}\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ max\ x\ y{\isachardoublequoteclose}\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharminus}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}lattice\ {\isacharparenleft}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequoteclose}%
+\ lattice{\isacharcolon}\ {\isachardoublequoteopen}lattice\ {\isacharparenleft}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptxt}%
We have already shown that this is a partial order,%
\end{isamarkuptxt}%
@@ -137,12 +138,21 @@
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ arith{\isacharplus}%
\begin{isamarkuptxt}%
-In order to show the equations, we put ourselves in a
+For the first of the equations, we refer to the theorem
+ generated in the previous interpretation.%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}rule\ nat{\isacharunderscore}less{\isacharunderscore}eq{\isacharparenright}%
+\begin{isamarkuptxt}%
+In order to show the remaining equations, we put ourselves in a
situation where the lattice theorems can be used in a convenient way.%
\end{isamarkuptxt}%
\isamarkuptrue%
-\ \ \isacommand{then}\isamarkupfalse%
-\ \isacommand{interpret}\isamarkupfalse%
+\ \ \isacommand{from}\isamarkupfalse%
+\ lattice\ \isacommand{interpret}\isamarkupfalse%
\ nat{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
@@ -163,8 +173,8 @@
\endisadelimvisible
%
\begin{isamarkuptext}%
-That the relation \isa{{\isasymle}} is a total order completes this
- sequence of interpretations.%
+The interpretation that the relation \isa{{\isasymle}} is a total
+ order follows next.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -174,9 +184,45 @@
%
\isatagvisible
\isacommand{interpretation}\isamarkupfalse%
-\ nat{\isacharbang}{\isacharcolon}\ total{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
+\ nat{\isacharcolon}\ total{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
+\ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ min\ x\ y{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ max\ x\ y{\isachardoublequoteclose}\isanewline
+\isacommand{proof}\isamarkupfalse%
+\ {\isacharminus}\isanewline
+\ \ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}total{\isacharunderscore}order\ {\isacharparenleft}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ unfold{\isacharunderscore}locales\ arith\isanewline
+\isacommand{qed}\isamarkupfalse%
+\ {\isacharparenleft}rule\ nat{\isacharunderscore}less{\isacharunderscore}eq\ nat{\isacharunderscore}meet{\isacharunderscore}eq\ nat{\isacharunderscore}join{\isacharunderscore}eq{\isacharparenright}{\isacharplus}%
+\endisatagvisible
+{\isafoldvisible}%
+%
+\isadelimvisible
+%
+\endisadelimvisible
+%
+\begin{isamarkuptext}%
+Note that since the locale hierarchy reflects that total
+ orders are distributive lattices, an explicit interpretation of
+ distributive lattices for the order relation on natural numbers is
+ only necessary for mapping the definitions to the right operators on
+ \isa{nat}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimvisible
+%
+\endisadelimvisible
+%
+\isatagvisible
+\isacommand{interpretation}\isamarkupfalse%
+\ nat{\isacharcolon}\ distrib{\isacharunderscore}lattice\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
+\ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ min\ x\ y{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ max\ x\ y{\isachardoublequoteclose}\isanewline
\ \ \isacommand{by}\isamarkupfalse%
-\ unfold{\isacharunderscore}locales\ arith%
+\ unfold{\isacharunderscore}locales\ {\isacharbrackleft}{\isadigit{1}}{\isacharbrackright}\ {\isacharparenleft}rule\ nat{\isacharunderscore}less{\isacharunderscore}eq\ nat{\isacharunderscore}meet{\isacharunderscore}eq\ nat{\isacharunderscore}join{\isacharunderscore}eq{\isacharparenright}{\isacharplus}%
\endisatagvisible
{\isafoldvisible}%
%
@@ -198,38 +244,15 @@
\isa{nat{\isachardot}meet{\isacharunderscore}left} from locale \isa{lattice}: \\
\quad \isa{min\ {\isacharquery}x\ {\isacharquery}y\ {\isasymle}\ {\isacharquery}x} \\
\isa{nat{\isachardot}join{\isacharunderscore}distr} from locale \isa{distrib{\isacharunderscore}lattice}: \\
- \quad \isa{lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharquery}x\ {\isacharparenleft}lattice{\isachardot}meet\ op\ {\isasymle}\ {\isacharquery}y\ {\isacharquery}z{\isacharparenright}\ {\isacharequal}\ lattice{\isachardot}meet\ op\ {\isasymle}\ {\isacharparenleft}lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharquery}x\ {\isacharquery}y{\isacharparenright}\ {\isacharparenleft}lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharquery}x\ {\isacharquery}z{\isacharparenright}} \\
+ \quad \isa{max\ {\isacharquery}x\ {\isacharparenleft}min\ {\isacharquery}y\ {\isacharquery}z{\isacharparenright}\ {\isacharequal}\ min\ {\isacharparenleft}max\ {\isacharquery}x\ {\isacharquery}y{\isacharparenright}\ {\isacharparenleft}max\ {\isacharquery}x\ {\isacharquery}z{\isacharparenright}} \\
\isa{nat{\isachardot}less{\isacharunderscore}total} from locale \isa{total{\isacharunderscore}order}: \\
- \quad \isa{partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharquery}x\ {\isacharquery}y\ {\isasymor}\ {\isacharquery}x\ {\isacharequal}\ {\isacharquery}y\ {\isasymor}\ partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharquery}y\ {\isacharquery}x}
+ \quad \isa{{\isacharquery}x\ {\isacharless}\ {\isacharquery}y\ {\isasymor}\ {\isacharquery}x\ {\isacharequal}\ {\isacharquery}y\ {\isasymor}\ {\isacharquery}y\ {\isacharless}\ {\isacharquery}x}
\end{tabular}
\end{center}
\hrule
\caption{Interpreted theorems for \isa{{\isasymle}} on the natural numbers.}
\label{tab:nat-lattice}
-\end{table}
-
- Note that since the locale hierarchy reflects that total orders are
- distributive lattices, an explicit interpretation of distributive
- lattices for the order relation on natural numbers is not neccessary.
-
- Why not push this idea further and just give the last interpretation
- as a single interpretation instead of the sequence of three? The
- reasons for this are twofold:
-\begin{itemize}
-\item
- Often it is easier to work in an incremental fashion, because later
- interpretations require theorems provided by earlier
- interpretations.
-\item
- Assume that a definition is made in some locale $l_1$, and that $l_2$
- imports $l_1$. Let an equation for the definition be
- proved in an interpretation of $l_2$. The equation will be unfolded
- in interpretations of theorems added to $l_2$ or below in the import
- hierarchy, but not for theorems added above $l_2$.
- Hence, an equation interpreting a definition should always be given in
- an interpretation of the locale where the definition is made, not in
- an interpretation of a locale further down the hierarchy.
-\end{itemize}%
+\end{table}%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -245,7 +268,7 @@
\isamarkuptrue%
\isacommand{interpretation}\isamarkupfalse%
\ nat{\isacharunderscore}dvd{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
-\ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ dvd\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ dvd\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isakeyword{where}\ nat{\isacharunderscore}dvd{\isacharunderscore}less{\isacharunderscore}eq{\isacharcolon}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ dvd\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ dvd\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
@@ -285,11 +308,10 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{interpretation}\isamarkupfalse%
-\ nat{\isacharunderscore}dvd{\isacharbang}{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
-\ \ \isakeyword{where}\ nat{\isacharunderscore}dvd{\isacharunderscore}meet{\isacharunderscore}eq{\isacharcolon}\isanewline
-\ \ \ \ \ \ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ dvd\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isakeyword{and}\ nat{\isacharunderscore}dvd{\isacharunderscore}join{\isacharunderscore}eq{\isacharcolon}\isanewline
-\ \ \ \ \ \ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ dvd\ {\isacharequal}\ lcm{\isachardoublequoteclose}\isanewline
+\ nat{\isacharunderscore}dvd{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
+\ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ dvd\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ dvd\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{and}\ nat{\isacharunderscore}dvd{\isacharunderscore}meet{\isacharunderscore}eq{\isacharcolon}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ dvd\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{and}\ nat{\isacharunderscore}dvd{\isacharunderscore}join{\isacharunderscore}eq{\isacharcolon}\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ dvd\ {\isacharequal}\ lcm{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
@@ -319,6 +341,10 @@
\ nat{\isacharunderscore}dvd{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ dvd\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ dvd\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}rule\ nat{\isacharunderscore}dvd{\isacharunderscore}less{\isacharunderscore}eq{\isacharparenright}\isanewline
+\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ dvd\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ expand{\isacharunderscore}fun{\isacharunderscore}eq{\isacharparenright}\isanewline
@@ -381,9 +407,16 @@
%
\isatagvisible
\isacommand{interpretation}\isamarkupfalse%
-\ nat{\isacharunderscore}dvd{\isacharbang}{\isacharcolon}\isanewline
+\ nat{\isacharunderscore}dvd{\isacharcolon}\isanewline
\ \ distrib{\isacharunderscore}lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
-\ \ \isacommand{apply}\isamarkupfalse%
+\ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ dvd\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ dvd\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ dvd\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ dvd\ {\isacharequal}\ lcm{\isachardoublequoteclose}\isanewline
+\isacommand{proof}\isamarkupfalse%
+\ {\isacharminus}\isanewline
+\ \ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}distrib{\isacharunderscore}lattice\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ unfold{\isacharunderscore}locales%
\begin{isamarkuptxt}%
\begin{isabelle}%
@@ -394,7 +427,7 @@
\end{isabelle}%
\end{isamarkuptxt}%
\isamarkuptrue%
-\ \ \isacommand{apply}\isamarkupfalse%
+\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}unfold\ nat{\isacharunderscore}dvd{\isacharunderscore}meet{\isacharunderscore}eq\ nat{\isacharunderscore}dvd{\isacharunderscore}join{\isacharunderscore}eq{\isacharparenright}%
\begin{isamarkuptxt}%
\begin{isabelle}%
@@ -402,9 +435,12 @@
\end{isabelle}%
\end{isamarkuptxt}%
\isamarkuptrue%
-\ \ \isacommand{apply}\isamarkupfalse%
-\ {\isacharparenleft}rule\ gcd{\isacharunderscore}lcm{\isacharunderscore}distr{\isacharparenright}\ \isacommand{done}\isamarkupfalse%
-%
+\ \ \ \ \isacommand{apply}\isamarkupfalse%
+\ {\isacharparenleft}rule\ gcd{\isacharunderscore}lcm{\isacharunderscore}distr{\isacharparenright}\isanewline
+\ \ \ \ \isacommand{done}\isamarkupfalse%
+\isanewline
+\isacommand{qed}\isamarkupfalse%
+\ {\isacharparenleft}rule\ nat{\isacharunderscore}dvd{\isacharunderscore}less{\isacharunderscore}eq\ nat{\isacharunderscore}dvd{\isacharunderscore}meet{\isacharunderscore}eq\ nat{\isacharunderscore}dvd{\isacharunderscore}join{\isacharunderscore}eq{\isacharparenright}{\isacharplus}%
\endisatagvisible
{\isafoldvisible}%
%
@@ -426,7 +462,7 @@
\isa{nat{\isacharunderscore}dvd{\isachardot}meet{\isacharunderscore}left} from locale \isa{lattice}: \\
\quad \isa{gcd\ {\isacharquery}x\ {\isacharquery}y\ dvd\ {\isacharquery}x} \\
\isa{nat{\isacharunderscore}dvd{\isachardot}join{\isacharunderscore}distr} from locale \isa{distrib{\isacharunderscore}lattice}: \\
- \quad \isa{lattice{\isachardot}join\ op\ dvd\ {\isacharquery}x\ {\isacharparenleft}lattice{\isachardot}meet\ op\ dvd\ {\isacharquery}y\ {\isacharquery}z{\isacharparenright}\ {\isacharequal}\ lattice{\isachardot}meet\ op\ dvd\ {\isacharparenleft}lattice{\isachardot}join\ op\ dvd\ {\isacharquery}x\ {\isacharquery}y{\isacharparenright}\ {\isacharparenleft}lattice{\isachardot}join\ op\ dvd\ {\isacharquery}x\ {\isacharquery}z{\isacharparenright}} \\
+ \quad \isa{lcm\ {\isacharquery}x\ {\isacharparenleft}gcd\ {\isacharquery}y\ {\isacharquery}z{\isacharparenright}\ {\isacharequal}\ gcd\ {\isacharparenleft}lcm\ {\isacharquery}x\ {\isacharquery}y{\isacharparenright}\ {\isacharparenleft}lcm\ {\isacharquery}x\ {\isacharquery}z{\isacharparenright}} \\
\end{tabular}
\end{center}
\hrule
@@ -457,52 +493,49 @@
Inspecting the grammar of locale commands in
Table~\ref{tab:commands} reveals that the import of a locale can be
more than just a single locale. In general, the import is a
- \emph{locale expression}. Locale expressions enable to combine locales
- and rename parameters. A locale name is a locale expression. If
- $e_1$ and $e_2$ are locale expressions then $e_1 + e_2$ is their
- \emph{merge}. If $e$ is an expression, then $e~q_1 \ldots q_n$ is
- a \emph{renamed expression} where the parameters in $e$ are renamed
- to $q_1 \ldots q_n$. Using a locale expression, a locale for order
+ \emph{locale expression}. These enable to combine locales
+ and instantiate parameters. A locale expression is a sequence of
+ locale \emph{instances} followed by an optional \isakeyword{for}
+ clause. Each instance consists of a locale reference, which may be
+ preceded by a qualifer and succeeded by instantiations of the
+ parameters of that locale. Instantiations may be either positional
+ or through explicit parameter argument pairs.
+
+ Using a locale expression, a locale for order
preserving maps can be declared in the following way.%
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \isacommand{locale}\isamarkupfalse%
\ order{\isacharunderscore}preserving\ {\isacharequal}\isanewline
-\ \ \ \ le{\isacharcolon}\ partial{\isacharunderscore}order\ {\isacharplus}\ le{\isacharprime}{\isacharcolon}\ partial{\isacharunderscore}order\ le{\isacharprime}\ \isakeyword{for}\ le{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasympreceq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ {\isacharplus}\isanewline
+\ \ \ \ le{\isacharcolon}\ partial{\isacharunderscore}order\ le\ {\isacharplus}\ le{\isacharprime}{\isacharcolon}\ partial{\isacharunderscore}order\ le{\isacharprime}\isanewline
+\ \ \ \ \ \ \isakeyword{for}\ le\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqsubseteq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{and}\ le{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasympreceq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ {\isacharplus}\isanewline
\ \ \ \ \isakeyword{fixes}\ {\isasymphi}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isachardoublequoteclose}\isanewline
\ \ \ \ \isakeyword{assumes}\ hom{\isacharunderscore}le{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymsqsubseteq}\ y\ {\isasymLongrightarrow}\ {\isasymphi}\ x\ {\isasympreceq}\ {\isasymphi}\ y{\isachardoublequoteclose}%
\begin{isamarkuptext}%
-The second line contains the expression, which is the
- merge of two partial order locales. The parameter of the second one
- is \isa{le{\isacharprime}} with new infix syntax \isa{{\isasympreceq}}. The
- parameters of the entire locale are \isa{le}, \isa{le{\isacharprime}} and
- \isa{{\isasymphi}}. This is their \emph{canonical order},
- which is obtained by a left-to-right traversal of the expression,
- where only the new parameters are appended to the end of the list. The
- parameters introduced in the locale elements of the declaration
- follow.
-
- In renamings parameters are referred to by position in the canonical
- order; an underscore is used to skip a parameter position, which is
- then not renamed. Renaming deletes the syntax of a parameter unless
- a new mixfix annotation is given.
+The second and third line contain the expression --- two
+ instances of the partial order locale with instantiations \isa{le}
+ and \isa{le{\isacharprime}}, respectively. The \isakeyword{for} clause consists
+ of parameter declarations and is similar to the context element
+ \isakeyword{fixes}. The notable difference is that the
+ \isakeyword{for} clause is part of the expression, and only
+ parameters defined in the expression may occur in its instances.
- Parameter renamings are morphisms between locales. These can be
- lifted to terms and theorems and thus be applied to assumptions and
- conclusions. The assumption of a merge is the conjunction of the
- assumptions of the merged locale. The conclusions of a merge are
- obtained by appending the conclusions of the left locale and of the
- right locale.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-The locale \isa{order{\isacharunderscore}preserving} contains theorems for both
- orders \isa{{\isasymsqsubseteq}} and \isa{{\isasympreceq}}. How can one refer to a theorem for
- a particular order, \isa{{\isasymsqsubseteq}} or \isa{{\isasympreceq}}? Names in locales are
- qualified by the locale parameters. More precisely, a name is
- qualified by the parameters of the locale in which its declaration
- occurs. Here are examples:%
+ Instances are \emph{morphisms} on locales. Their effect on the
+ parameters is naturally lifted to terms, propositions and theorems,
+ and thus to the assumptions and conclusions of a locale. The
+ assumption of a locale expression is the conjunction of the
+ assumptions of the instances. The conclusions of a sequence of
+ instances are obtained by appending the conclusions of the
+ instances in the order of the sequence.
+
+ The qualifiers in the expression are already a familiar concept from
+ the \isakeyword{interpretation} command
+ (Section~\ref{sec:po-first}). Here, they serve to distinguish names
+ (in particular theorem names) for the two partial orders within the
+ locale. Qualifiers in the \isakeyword{locale} command (and in
+ \isakeyword{sublocale}) default to optional --- that is, they need
+ not occur in references to the qualified names. Here are examples
+ of theorems in locale \isa{order{\isacharunderscore}preserving}:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -528,8 +561,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-When renaming a locale, the morphism is also applied
- to the qualifiers. Hence theorems for the partial order \isa{{\isasympreceq}}
+The theorems for the partial order \isa{{\isasympreceq}}
are qualified by \isa{le{\isacharprime}}. For example, \isa{le{\isacharprime}{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}: \begin{isabelle}%
\ \ {\isasymlbrakk}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasympreceq}\ {\isacharquery}x\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasympreceq}\ {\isacharquery}z{\isasymrbrakk}\isanewline
\isaindent{\ \ }{\isasymLongrightarrow}\ partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasympreceq}\ {\isacharquery}x\ {\isacharquery}z%
@@ -553,8 +585,7 @@
%
\begin{isamarkuptext}%
This example reveals that there is no infix syntax for the strict
- version of \isa{{\isasympreceq}}! This can, of course, not be introduced
- automatically, but it can be declared manually through an abbreviation.%
+ version of \isa{{\isasympreceq}}! This can be declared through an abbreviation.%
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \isacommand{abbreviation}\isamarkupfalse%
@@ -567,26 +598,42 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Not only names of theorems are qualified. In fact, all names
- are qualified, in particular names introduced by definitions and
- abbreviations. The name of the strict order of \isa{{\isasymsqsubseteq}} is \isa{le{\isachardot}less} and therefore \isa{le{\isacharprime}{\isachardot}less} is the name of the strict
- order of \isa{{\isasympreceq}}. Hence, the equation in the above abbreviation
- could have been written as \isa{less{\isacharprime}\ {\isasymequiv}\ le{\isacharprime}{\isachardot}less}.%
+Qualifiers not only apply to theorem names, but also to names
+ introduced by definitions and abbreviations. In locale
+ \isa{partial{\isacharunderscore}order} the full name of the strict order of \isa{{\isasymsqsubseteq}} is
+ \isa{le{\isachardot}less} and therefore \isa{le{\isacharprime}{\isachardot}less} is the full name of
+ the strict order of \isa{{\isasympreceq}}. Hence, the equation in the
+ abbreviation above could have been also written as \isa{less{\isacharprime}\ {\isasymequiv}\ le{\isacharprime}{\isachardot}less}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Two more locales illustrate working with locale expressions.
- A map \isa{{\isasymphi}} is a lattice homomorphism if it preserves meet and join.%
+Readers may find the declaration of locale \isa{order{\isacharunderscore}preserving} a little awkward, because the declaration and
+ concrete syntax for \isa{le} from \isa{partial{\isacharunderscore}order} are
+ repeated in the declaration of \isa{order{\isacharunderscore}preserving}. Locale
+ expressions provide a convenient short hand for this. A parameter
+ in an instance is \emph{untouched} if no instantiation term is
+ provided for it. In positional instantiations, a parameter position
+ may be skipped with an underscore, and it is allowed to give fewer
+ instantiation terms than the instantiated locale's number of
+ parameters. In named instantiations, instantiation pairs for
+ certain parameters may simply be omitted. Untouched parameters are
+ declared by the locale expression and with their concrete syntax by
+ implicitly adding them to the beginning of the \isakeyword{for}
+ clause.
+
+ The following locales illustrate this. A map \isa{{\isasymphi}} is a
+ lattice homomorphism if it preserves meet and join.%
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \isacommand{locale}\isamarkupfalse%
-\ lattice{\isacharunderscore}hom\ {\isacharequal}\ le{\isacharcolon}\ lattice\ {\isacharplus}\ le{\isacharprime}{\isacharcolon}\ lattice\ le{\isacharprime}\ \isakeyword{for}\ le{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasympreceq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ {\isacharplus}\isanewline
+\ lattice{\isacharunderscore}hom\ {\isacharequal}\isanewline
+\ \ \ \ le{\isacharcolon}\ lattice\ {\isacharplus}\ le{\isacharprime}{\isacharcolon}\ lattice\ le{\isacharprime}\ \isakeyword{for}\ le{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasympreceq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ {\isacharplus}\isanewline
\ \ \ \ \isakeyword{fixes}\ {\isasymphi}\isanewline
\ \ \ \ \isakeyword{assumes}\ hom{\isacharunderscore}meet{\isacharcolon}\isanewline
-\ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymphi}\ {\isacharparenleft}lattice{\isachardot}meet\ le\ x\ y{\isacharparenright}\ {\isacharequal}\ lattice{\isachardot}meet\ le{\isacharprime}\ {\isacharparenleft}{\isasymphi}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymphi}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymphi}\ {\isacharparenleft}x\ {\isasymsqinter}\ y{\isacharparenright}\ {\isacharequal}\ le{\isacharprime}{\isachardot}meet\ {\isacharparenleft}{\isasymphi}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymphi}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isakeyword{and}\ hom{\isacharunderscore}join{\isacharcolon}\isanewline
-\ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymphi}\ {\isacharparenleft}lattice{\isachardot}join\ le\ x\ y{\isacharparenright}\ {\isacharequal}\ lattice{\isachardot}join\ le{\isacharprime}\ {\isacharparenleft}{\isasymphi}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymphi}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymphi}\ {\isacharparenleft}x\ {\isasymsqunion}\ y{\isacharparenright}\ {\isacharequal}\ le{\isacharprime}{\isachardot}join\ {\isacharparenleft}{\isasymphi}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymphi}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\ \ \isacommand{abbreviation}\isamarkupfalse%
\ {\isacharparenleft}\isakeyword{in}\ lattice{\isacharunderscore}hom{\isacharparenright}\isanewline
@@ -599,8 +646,13 @@
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \isacommand{locale}\isamarkupfalse%
-\ lattice{\isacharunderscore}end\ {\isacharequal}\isanewline
-\ \ \ \ lattice{\isacharunderscore}hom\ le\ le\ \isakeyword{for}\ le\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqsubseteq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}%
+\ lattice{\isacharunderscore}end\ {\isacharequal}\ lattice{\isacharunderscore}hom\ {\isacharunderscore}\ le%
+\begin{isamarkuptext}%
+In this declaration, the first parameter of \isa{lattice{\isacharunderscore}hom}, \isa{le}, is untouched and then used to instantiate
+ the second parameter. Its concrete syntax is preserved.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\begin{isamarkuptext}%
The inheritance diagram of the situation we have now is shown
in Figure~\ref{fig:hom}, where the dashed line depicts an
@@ -648,7 +700,7 @@
\begin{isamarkuptext}%
It can be shown easily that a lattice homomorphism is order
preserving. As the final example of this section, a locale
- interpretation is used to assert this.%
+ interpretation is used to assert this:%
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \isacommand{sublocale}\isamarkupfalse%
@@ -688,6 +740,7 @@
\begin{isamarkuptext}%
Theorems and other declarations --- syntax, in particular --- from
the locale \isa{order{\isacharunderscore}preserving} are now active in \isa{lattice{\isacharunderscore}hom}, for example
+
\isa{le{\isacharprime}{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}:
\isa{{\isasymlbrakk}{\isacharquery}x\ {\isasymprec}\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasympreceq}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isasymprec}\ {\isacharquery}z}%
\end{isamarkuptext}%
@@ -709,7 +762,7 @@
Haftmann and Wenzel \cite{HaftmannWenzel2007} overcome a restriction
of axiomatic type classes through a combination with locale
interpretation. The result is a Haskell-style class system with a
- facility to generate Haskell code. Classes are sufficient for
+ facility to generate ML and Haskell code. Classes are sufficient for
simple specifications with a single type parameter. The locales for
orders and lattices presented in this tutorial fall into this
category. Order preserving maps, homomorphisms and vector spaces,
@@ -734,7 +787,7 @@
& \textit{name} $|$ \textit{attribute} $|$
\textit{name} \textit{attribute} \\
\textit{qualifier} & ::=
- & \textit{name} [``\textbf{!}''] \\[2ex]
+ & \textit{name} [``\textbf{?}'' $|$ ``\textbf{!}''] \\[2ex]
\multicolumn{3}{l}{Context Elements} \\
@@ -780,7 +833,7 @@
& \textbf{where} \textit{name} ``\textbf{=}'' \textit{term}
( \textbf{and} \textit{name} ``\textbf{=}'' \textit{term} )$^*$ \\
\textit{instance} & ::=
- & [ \textit{qualifier} \textbf{:} ]
+ & [ \textit{qualifier} ``\textbf{:}'' ]
\textit{qualified-name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\
\textit{expression} & ::=
& \textit{instance} ( ``\textbf{+}'' \textit{instance} )$^*$
--- a/doc-src/Locales/Locales/document/root.tex Fri Mar 27 15:14:31 2009 -0700
+++ b/doc-src/Locales/Locales/document/root.tex Mon Mar 30 07:49:26 2009 -0700
@@ -29,13 +29,8 @@
\maketitle
-%\thispagestyle{myheadings}
-%\markright{Technical Report TUM-I0723, Technische Universit\"at M\"unchen, 2007}
-\thispagestyle{myheadings}
-\markright{This tutorial is currently not consistent.}
-
\begin{abstract}
- Locales are Isabelle's mechanism to deal with parametric theories.
+ Locales are Isabelle's mechanism for dealing with parametric theories.
We present typical examples of locale specifications,
along with interpretations between locales to change their
hierarchic dependencies and interpretations to reuse locales in
@@ -43,7 +38,7 @@
This tutorial is intended for locale novices; familiarity with
Isabelle and Isar is presumed.
- The 2nd revision accommodates changes introduced by the locales
+ The second revision accommodates changes introduced by the locales
reimplementation for Isabelle 2009. Most notably, in complex
specifications (\emph{locale expressions}) renaming has been
generalised to instantiation.
--- a/etc/isar-keywords-ZF.el Fri Mar 27 15:14:31 2009 -0700
+++ b/etc/isar-keywords-ZF.el Mon Mar 30 07:49:26 2009 -0700
@@ -18,6 +18,7 @@
"ML"
"ML_command"
"ML_prf"
+ "ML_test"
"ML_val"
"ProofGeneral\\.inform_file_processed"
"ProofGeneral\\.inform_file_retracted"
@@ -348,6 +349,7 @@
(defconst isar-keywords-theory-decl
'("ML"
+ "ML_test"
"abbreviation"
"arities"
"attribute_setup"
--- a/etc/isar-keywords.el Fri Mar 27 15:14:31 2009 -0700
+++ b/etc/isar-keywords.el Mon Mar 30 07:49:26 2009 -0700
@@ -18,6 +18,7 @@
"ML"
"ML_command"
"ML_prf"
+ "ML_test"
"ML_val"
"ProofGeneral\\.inform_file_processed"
"ProofGeneral\\.inform_file_retracted"
@@ -419,6 +420,7 @@
(defconst isar-keywords-theory-decl
'("ML"
+ "ML_test"
"abbreviation"
"arities"
"atom_decl"
--- a/lib/jedit/isabelle.xml Fri Mar 27 15:14:31 2009 -0700
+++ b/lib/jedit/isabelle.xml Mon Mar 30 07:49:26 2009 -0700
@@ -45,6 +45,7 @@
<OPERATOR>ML</OPERATOR>
<LABEL>ML_command</LABEL>
<OPERATOR>ML_prf</OPERATOR>
+ <OPERATOR>ML_test</OPERATOR>
<LABEL>ML_val</LABEL>
<OPERATOR>abbreviation</OPERATOR>
<KEYWORD4>actions</KEYWORD4>
--- a/src/FOL/ex/LocaleTest.thy Fri Mar 27 15:14:31 2009 -0700
+++ b/src/FOL/ex/LocaleTest.thy Mon Mar 30 07:49:26 2009 -0700
@@ -1,7 +1,7 @@
-(* Title: FOL/ex/NewLocaleTest.thy
+(* Title: FOL/ex/LocaleTest.thy
Author: Clemens Ballarin, TU Muenchen
-Testing environment for locale expressions.
+Test environment for the locale implementation.
*)
theory LocaleTest
--- a/src/HOL/Nominal/nominal_inductive2.ML Fri Mar 27 15:14:31 2009 -0700
+++ b/src/HOL/Nominal/nominal_inductive2.ML Mon Mar 30 07:49:26 2009 -0700
@@ -181,7 +181,7 @@
| xs => error ("No such case(s) in inductive definition: " ^ commas_quote xs));
fun mk_avoids params name sets =
let
- val (_, ctxt') = ProofContext.add_fixes_i
+ val (_, ctxt') = ProofContext.add_fixes
(map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params) ctxt;
fun mk s =
let
--- a/src/HOL/Tools/function_package/fundef_common.ML Fri Mar 27 15:14:31 2009 -0700
+++ b/src/HOL/Tools/function_package/fundef_common.ML Mon Mar 30 07:49:26 2009 -0700
@@ -65,7 +65,7 @@
defname : string,
(* contains no logical entities: invariant under morphisms *)
- add_simps : (string -> string) -> string -> Attrib.src list -> thm list
+ add_simps : (binding -> binding) -> string -> Attrib.src list -> thm list
-> local_theory -> thm list * local_theory,
case_names : string list,
@@ -289,8 +289,8 @@
(* Preprocessors *)
type fixes = ((string * typ) * mixfix) list
-type 'a spec = ((bstring * Attrib.src list) * 'a list) list
-type preproc = fundef_config -> bool list -> Proof.context -> fixes -> term spec
+type 'a spec = (Attrib.binding * 'a list) list
+type preproc = fundef_config -> Proof.context -> fixes -> term spec
-> (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list)
val fname_of = fst o dest_Free o fst o strip_comb o fst
@@ -301,9 +301,9 @@
| mk_case_names _ n 1 = [n]
| mk_case_names _ n k = map (fn i => n ^ "_" ^ string_of_int i) (1 upto k)
-fun empty_preproc check _ _ ctxt fixes spec =
+fun empty_preproc check _ ctxt fixes spec =
let
- val (nas,tss) = split_list spec
+ val (bnds, tss) = split_list spec
val ts = flat tss
val _ = check ctxt fixes ts
val fnames = map (fst o fst) fixes
@@ -314,9 +314,9 @@
|> map (map snd)
(* using theorem names for case name currently disabled *)
- val cnames = map_index (fn (i, (n,_)) => mk_case_names i "" 1) nas |> flat
+ val cnames = map_index (fn (i, _) => mk_case_names i "" 1) bnds |> flat
in
- (ts, curry op ~~ nas o Library.unflat tss, sort, cnames)
+ (ts, curry op ~~ bnds o Library.unflat tss, sort, cnames)
end
structure Preprocessor = GenericDataFun
@@ -344,23 +344,9 @@
fun config_parser default =
(Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 option_parser) --| P.$$$ ")") [])
>> (fn opts => fold apply_opt opts default)
-
- val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")"
-
- fun pipe_error t =
- P.!!! (Scan.fail_with (K (cat_lines ["Equations must be separated by " ^ quote "|", quote t])))
-
- val statement_ow =
- SpecParse.opt_thm_name ":" -- (P.prop -- Scan.optional (otherwise >> K true) false)
- --| Scan.ahead ((P.term :-- pipe_error) || Scan.succeed ("",""))
-
- val statements_ow = P.enum1 "|" statement_ow
-
- val flags_statements = statements_ow
- >> (fn sow => (map (snd o snd) sow, map (apsnd fst) sow))
in
fun fundef_parser default_cfg =
- config_parser default_cfg -- P.fixes --| P.where_ -- flags_statements
+ config_parser default_cfg -- P.fixes -- SpecParse.where_alt_specs
end
--- a/src/HOL/Tools/function_package/fundef_datatype.ML Fri Mar 27 15:14:31 2009 -0700
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML Mon Mar 30 07:49:26 2009 -0700
@@ -15,10 +15,10 @@
val add_fun : FundefCommon.fundef_config ->
(binding * typ option * mixfix) list -> (Attrib.binding * term) list ->
- bool list -> bool -> local_theory -> Proof.context
+ bool -> local_theory -> Proof.context
val add_fun_cmd : FundefCommon.fundef_config ->
(binding * string option * mixfix) list -> (Attrib.binding * string) list ->
- bool list -> bool -> local_theory -> Proof.context
+ bool -> local_theory -> Proof.context
end
structure FundefDatatype : FUNDEF_DATATYPE =
@@ -235,50 +235,40 @@
end
fun add_catchall ctxt fixes spec =
- let
- val catchalls = mk_catchall fixes (mk_arities (map (split_def ctxt) (map snd spec)))
- in
- spec @ map (pair true) catchalls
- end
+ spec @ mk_catchall fixes (mk_arities (map (split_def ctxt) spec))
fun warn_if_redundant ctxt origs tss =
let
fun msg t = "Ignoring redundant equation: " ^ quote (Syntax.string_of_term ctxt t)
val (tss', _) = chop (length origs) tss
- fun check ((_, t), []) = (Output.warning (msg t); [])
- | check ((_, t), s) = s
+ fun check (t, []) = (Output.warning (msg t); [])
+ | check (t, s) = s
in
(map check (origs ~~ tss'); tss)
end
-fun sequential_preproc (config as FundefConfig {sequential, ...}) flags ctxt fixes spec =
- let
- val enabled = sequential orelse exists I flags
- in
- if enabled then
+fun sequential_preproc (config as FundefConfig {sequential, ...}) ctxt fixes spec =
+ if sequential then
let
- val flags' = if sequential then map (K true) flags else flags
-
- val (nas, eqss) = split_list spec
+ val (bnds, eqss) = split_list spec
val eqs = map the_single eqss
val feqs = eqs
|> tap (check_defs ctxt fixes) (* Standard checks *)
|> tap (map (check_pats ctxt)) (* More checks for sequential mode *)
- |> curry op ~~ flags'
val compleqs = add_catchall ctxt fixes feqs (* Completion *)
val spliteqs = warn_if_redundant ctxt feqs
- (FundefSplit.split_some_equations ctxt compleqs)
+ (FundefSplit.split_all_equations ctxt compleqs)
fun restore_spec thms =
- nas ~~ Library.take (length nas, Library.unflat spliteqs thms)
+ bnds ~~ Library.take (length bnds, Library.unflat spliteqs thms)
- val spliteqs' = flat (Library.take (length nas, spliteqs))
+ val spliteqs' = flat (Library.take (length bnds, spliteqs))
val fnames = map (fst o fst) fixes
val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) spliteqs'
@@ -286,18 +276,17 @@
|> map (map snd)
- val nas' = nas @ replicate (length spliteqs - length nas) ("",[])
+ val bnds' = bnds @ replicate (length spliteqs - length bnds) Attrib.empty_binding
(* using theorem names for case name currently disabled *)
- val case_names = map_index (fn (i, ((n, _), es)) => mk_case_names i "" (length es))
- (nas' ~~ spliteqs)
+ val case_names = map_index (fn (i, (_, es)) => mk_case_names i "" (length es))
+ (bnds' ~~ spliteqs)
|> flat
in
(flat spliteqs, restore_spec, sort, case_names)
end
else
- FundefCommon.empty_preproc check_defs config flags ctxt fixes spec
- end
+ FundefCommon.empty_preproc check_defs config ctxt fixes spec
val setup =
Method.setup @{binding pat_completeness} (Scan.succeed pat_completeness)
@@ -308,11 +297,11 @@
val fun_config = FundefConfig { sequential=true, default="%x. undefined" (*FIXME dynamic scoping*),
domintros=false, tailrec=false }
-fun gen_fun add config fixes statements flags int lthy =
+fun gen_fun add config fixes statements int lthy =
let val group = serial_string () in
lthy
|> LocalTheory.set_group group
- |> add fixes statements config flags
+ |> add fixes statements config
|> by_pat_completeness_auto int
|> LocalTheory.restore
|> LocalTheory.set_group group
@@ -329,7 +318,7 @@
val _ =
OuterSyntax.local_theory' "fun" "define general recursive functions (short version)" K.thy_decl
(fundef_parser fun_config
- >> (fn ((config, fixes), (flags, statements)) => add_fun_cmd config fixes statements flags));
+ >> (fn ((config, fixes), statements) => add_fun_cmd config fixes statements));
end
--- a/src/HOL/Tools/function_package/fundef_lib.ML Fri Mar 27 15:14:31 2009 -0700
+++ b/src/HOL/Tools/function_package/fundef_lib.ML Mon Mar 30 07:49:26 2009 -0700
@@ -55,7 +55,7 @@
fun dest_all_all_ctx ctx (Const ("all", _) $ Abs (a as (n,T,b))) =
let
val [(n', _)] = Variable.variant_frees ctx [] [(n,T)]
- val (_, ctx') = ProofContext.add_fixes_i [(Binding.name n', SOME T, NoSyn)] ctx
+ val (_, ctx') = ProofContext.add_fixes [(Binding.name n', SOME T, NoSyn)] ctx
val (n'', body) = Term.dest_abs (n', T, b)
val _ = (n' = n'') orelse error "dest_all_ctx"
--- a/src/HOL/Tools/function_package/fundef_package.ML Fri Mar 27 15:14:31 2009 -0700
+++ b/src/HOL/Tools/function_package/fundef_package.ML Mon Mar 30 07:49:26 2009 -0700
@@ -10,13 +10,11 @@
val add_fundef : (binding * typ option * mixfix) list
-> (Attrib.binding * term) list
-> FundefCommon.fundef_config
- -> bool list
-> local_theory
-> Proof.state
val add_fundef_cmd : (binding * string option * mixfix) list
- -> (Attrib.binding * string) list
+ -> (Attrib.binding * string) list
-> FundefCommon.fundef_config
- -> bool list
-> local_theory
-> Proof.state
@@ -36,20 +34,28 @@
open FundefLib
open FundefCommon
+val simp_attribs = map (Attrib.internal o K)
+ [Simplifier.simp_add,
+ Code.add_default_eqn_attribute,
+ Nitpick_Const_Simp_Thms.add]
+
+val psimp_attribs = map (Attrib.internal o K)
+ [Simplifier.simp_add,
+ Nitpick_Const_Psimp_Thms.add]
+
fun note_theorem ((name, atts), ths) =
LocalTheory.note Thm.theoremK ((Binding.qualified_name name, atts), ths)
-fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
+fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
fun add_simps fnames post sort extra_qualify label moreatts simps lthy =
let
- val atts = Attrib.internal (K Simplifier.simp_add) :: moreatts
val spec = post simps
- |> map (apfst (apsnd (append atts)))
+ |> map (apfst (apsnd (fn ats => moreatts @ ats)))
|> map (apfst (apfst extra_qualify))
val (saved_spec_simps, lthy) =
- fold_map note_theorem spec lthy
+ fold_map (LocalTheory.note Thm.theoremK) spec lthy
val saved_simps = flat (map snd saved_spec_simps)
val simps_by_f = sort saved_simps
@@ -72,15 +78,15 @@
val (((psimps', pinducts'), (_, [termination'])), lthy) =
lthy
- |> addsmps (Long_Name.qualify "partial") "psimps"
- [Attrib.internal (K Nitpick_Const_Psimp_Thms.add)] psimps
- ||> fold_option (snd oo addsmps I "simps" [Attrib.internal (K Nitpick_Const_Simp_Thms.add)]) trsimps
+ |> addsmps (Binding.qualify false "partial") "psimps"
+ psimp_attribs psimps
+ ||> fold_option (snd oo addsmps I "simps" simp_attribs) trsimps
||>> note_theorem ((qualify "pinduct",
[Attrib.internal (K (RuleCases.case_names cnames)),
Attrib.internal (K (RuleCases.consumes 1)),
Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
||>> note_theorem ((qualify "termination", []), [termination])
- ||> (snd o note_theorem ((qualify "cases",
+ ||> (snd o note_theorem ((qualify "cases",
[Attrib.internal (K (RuleCases.case_names cnames))]), [cases]))
||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros
@@ -90,18 +96,18 @@
if not do_print then ()
else Specification.print_consts lthy (K false) (map fst fixes)
in
- lthy
+ lthy
|> LocalTheory.declaration (add_fundef_data o morph_fundef_data cdata)
end
-fun gen_add_fundef is_external prep default_constraint fixspec eqns config flags lthy =
+fun gen_add_fundef is_external prep default_constraint fixspec eqns config lthy =
let
val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx))
val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy
val fixes = map (apfst (apfst Binding.name_of)) fixes0;
- val spec = map (fn ((b, atts), prop) => ((Binding.name_of b, atts), [prop])) spec0;
- val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
+ val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0;
+ val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config ctxt' fixes spec
val defname = mk_defname fixes
@@ -131,14 +137,10 @@
val tsimps = map remove_domain_condition psimps
val tinduct = map remove_domain_condition pinducts
- val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
- val allatts = (not has_guards ? cons Code.add_default_eqn_attrib)
- [Attrib.internal (K Nitpick_Const_Simp_Thms.add)]
-
val qualify = Long_Name.qualify defname;
in
lthy
- |> add_simps I "simps" allatts tsimps |> snd
+ |> add_simps I "simps" simp_attribs tsimps |> snd
|> note_theorem ((qualify "induct", [Attrib.internal (K (RuleCases.case_names case_names))]), tinduct) |> snd
end
@@ -156,9 +158,9 @@
val goal = HOLogic.mk_Trueprop (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
in
lthy
- |> ProofContext.note_thmss_i "" [((Binding.empty, [ContextRules.rule_del]), [([allI], [])])] |> snd
- |> ProofContext.note_thmss_i "" [((Binding.empty, [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
- |> ProofContext.note_thmss_i ""
+ |> ProofContext.note_thmss "" [((Binding.empty, [ContextRules.rule_del]), [([allI], [])])] |> snd
+ |> ProofContext.note_thmss "" [((Binding.empty, [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
+ |> ProofContext.note_thmss ""
[((Binding.name "termination", [ContextRules.intro_bang (SOME 0)]),
[([Goal.norm_result termination], [])])] |> snd
|> Proof.theorem_i NONE (total_termination_afterqed data) [[(goal, [])]]
@@ -209,12 +211,10 @@
local structure P = OuterParse and K = OuterKeyword in
-val _ = OuterKeyword.keyword "otherwise";
-
val _ =
OuterSyntax.local_theory_to_proof "function" "define general recursive functions" K.thy_goal
(fundef_parser default_config
- >> (fn ((config, fixes), (flags, statements)) => add_fundef_cmd fixes statements config flags));
+ >> (fn ((config, fixes), statements) => add_fundef_cmd fixes statements config));
val _ =
OuterSyntax.local_theory_to_proof "termination" "prove termination of a recursive function" K.thy_goal
--- a/src/Pure/Isar/attrib.ML Fri Mar 27 15:14:31 2009 -0700
+++ b/src/Pure/Isar/attrib.ML Mon Mar 30 07:49:26 2009 -0700
@@ -18,10 +18,13 @@
val attribute_i: theory -> src -> attribute
val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
val map_specs: ('a -> 'att) ->
- (('c * 'a list) * 'd) list -> (('c * 'att list) * 'd) list
+ (('c * 'a list) * 'b) list -> (('c * 'att list) * 'b) list
val map_facts: ('a -> 'att) ->
(('c * 'a list) * ('d * 'a list) list) list ->
(('c * 'att list) * ('d * 'att list) list) list
+ val map_facts_refs: ('a -> 'att) -> ('b -> 'fact) ->
+ (('c * 'a list) * ('b * 'a list) list) list ->
+ (('c * 'att list) * ('fact * 'att list) list) list
val crude_closure: Proof.context -> src -> src
val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory
val syntax: attribute context_parser -> src -> attribute
@@ -121,14 +124,17 @@
fun attribute thy = attribute_i thy o intern_src thy;
fun eval_thms ctxt args = ProofContext.note_thmss Thm.theoremK
- [(Thm.empty_binding, map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt
+ [(Thm.empty_binding, args |> map (fn (a, atts) =>
+ (ProofContext.get_fact ctxt a, map (attribute (ProofContext.theory_of ctxt)) atts)))] ctxt
|> fst |> maps snd;
(* attributed declarations *)
fun map_specs f = map (apfst (apsnd (map f)));
+
fun map_facts f = map (apfst (apsnd (map f)) o apsnd (map (apsnd (map f))));
+fun map_facts_refs f g = map_facts f #> map (apsnd (map (apfst g)));
(* crude_closure *)
--- a/src/Pure/Isar/class.ML Fri Mar 27 15:14:31 2009 -0700
+++ b/src/Pure/Isar/class.ML Mon Mar 30 07:49:26 2009 -0700
@@ -225,8 +225,9 @@
|> (map o apsnd o apsnd o map_atyps o K o TFree) (Name.aT, [class]);
val all_params = Locale.params_of thy class;
val raw_params = (snd o chop (length supparams)) all_params;
- fun add_const (b, SOME raw_ty, _) thy =
+ fun add_const ((raw_c, raw_ty), _) thy =
let
+ val b = Binding.name raw_c;
val c = Sign.full_name thy b;
val ty = map_atyps (K (TFree (Name.aT, base_sort))) raw_ty;
val ty0 = Type.strip_sorts ty;
@@ -284,7 +285,7 @@
`(fn thy => calculate thy class sups base_sort param_map assm_axiom)
#-> (fn (base_morph, morph, export_morph, axiom, assm_intro, of_class) =>
Locale.add_registration (class, (morph, export_morph))
- #> Locale.activate_global_facts (class, morph $> export_morph)
+ #> Context.theory_map (Locale.activate_facts (class, morph $> export_morph))
#> register class sups params base_sort base_morph axiom assm_intro of_class))
|> TheoryTarget.init (SOME class)
|> pair class
--- a/src/Pure/Isar/class_target.ML Fri Mar 27 15:14:31 2009 -0700
+++ b/src/Pure/Isar/class_target.ML Mon Mar 30 07:49:26 2009 -0700
@@ -287,8 +287,8 @@
|> fold (fn dep_morph => Locale.add_dependency sub (sup,
dep_morph $> Element.satisfy_morphism (the_list some_wit) $> export))
(the_list some_dep_morph)
- |> (fn thy => fold_rev Locale.activate_global_facts
- (Locale.get_registrations thy) thy)
+ |> (fn thy => fold_rev (Context.theory_map o Locale.activate_facts)
+ (Locale.get_registrations thy) thy)
end;
--- a/src/Pure/Isar/code_unit.ML Fri Mar 27 15:14:31 2009 -0700
+++ b/src/Pure/Isar/code_unit.ML Mon Mar 30 07:49:26 2009 -0700
@@ -325,19 +325,18 @@
val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm
handle TERM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm)
| THM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm);
- fun vars_of t = fold_aterms
- (fn Var (v, _) => insert (op =) v
- | Free _ => bad_thm ("Illegal free variable in rewrite theorem\n"
- ^ Display.string_of_thm thm)
- | _ => I) t [];
- fun tvars_of t = fold_term_types
- (fn _ => fold_atyps (fn TVar (v, _) => insert (op =) v
- | TFree _ => bad_thm
+ fun vars_of t = fold_aterms (fn Var (v, _) => insert (op =) v
+ | Free _ => bad_thm ("Illegal free variable in rewrite theorem\n"
+ ^ Display.string_of_thm thm)
+ | _ => I) t [];
+ fun tvars_of t = fold_term_types (fn _ =>
+ fold_atyps (fn TVar (v, _) => insert (op =) v
+ | TFree _ => bad_thm
("Illegal free type variable in rewrite theorem\n" ^ Display.string_of_thm thm))) t [];
val lhs_vs = vars_of lhs;
val rhs_vs = vars_of rhs;
val lhs_tvs = tvars_of lhs;
- val rhs_tvs = tvars_of lhs;
+ val rhs_tvs = tvars_of rhs;
val _ = if null (subtract (op =) lhs_vs rhs_vs)
then ()
else bad_thm ("Free variables on right hand side of rewrite theorem\n"
--- a/src/Pure/Isar/constdefs.ML Fri Mar 27 15:14:31 2009 -0700
+++ b/src/Pure/Isar/constdefs.ML Mon Mar 30 07:49:26 2009 -0700
@@ -25,13 +25,13 @@
fun err msg ts = error (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts));
val thy_ctxt = ProofContext.init thy;
- val struct_ctxt = #2 (ProofContext.add_fixes_i structs thy_ctxt);
+ val struct_ctxt = #2 (ProofContext.add_fixes structs thy_ctxt);
val ((d, mx), var_ctxt) =
(case raw_decl of
NONE => ((NONE, NoSyn), struct_ctxt)
| SOME raw_var =>
struct_ctxt |> prep_vars [raw_var] |-> (fn [(x, T, mx)] =>
- ProofContext.add_fixes_i [(x, T, mx)] #> snd #> pair (SOME x, mx)));
+ ProofContext.add_fixes [(x, T, mx)] #> snd #> pair (SOME x, mx)));
val prop = prep_prop var_ctxt raw_prop;
val (c, T) = #1 (LocalDefs.cert_def thy_ctxt (Logic.strip_imp_concl prop));
--- a/src/Pure/Isar/element.ML Fri Mar 27 15:14:31 2009 -0700
+++ b/src/Pure/Isar/element.ML Mon Mar 30 07:49:26 2009 -0700
@@ -60,8 +60,9 @@
(Attrib.binding * (thm list * Attrib.src list) list) list
val eq_morphism: theory -> thm list -> morphism
val transfer_morphism: theory -> morphism
- val activate: (typ, term, Facts.ref) ctxt list -> Proof.context -> context_i list * Proof.context
- val activate_i: context_i list -> Proof.context -> context_i list * Proof.context
+ val init: context_i -> Context.generic -> Context.generic
+ val activate_i: context_i -> Proof.context -> context_i * Proof.context
+ val activate: (typ, term, Facts.ref) ctxt -> Proof.context -> context_i * Proof.context
end;
structure Element: ELEMENT =
@@ -481,64 +482,54 @@
-(** activate in context, return elements and facts **)
+(** activate in context **)
-local
+(* init *)
-fun activate_elem (Fixes fixes) ctxt =
- ctxt |> ProofContext.add_fixes_i fixes |> snd
- | activate_elem (Constrains _) ctxt =
- ctxt
- | activate_elem (Assumes asms) ctxt =
+fun init (Fixes fixes) = Context.map_proof (ProofContext.add_fixes fixes #> #2)
+ | init (Constrains _) = I
+ | init (Assumes asms) = Context.map_proof (fn ctxt =>
let
val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms;
- val ts = maps (map #1 o #2) asms';
- val (_, ctxt') =
- ctxt |> fold Variable.auto_fixes ts
- |> ProofContext.add_assms_i Assumption.presume_export asms';
- in ctxt' end
- | activate_elem (Defines defs) ctxt =
+ val (_, ctxt') = ctxt
+ |> fold Variable.auto_fixes (maps (map #1 o #2) asms')
+ |> ProofContext.add_assms_i Assumption.assume_export asms';
+ in ctxt' end)
+ | init (Defines defs) = Context.map_proof (fn ctxt =>
let
val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
- let val ((c, _), t') = LocalDefs.cert_def ctxt t
+ let val ((c, _), t') = LocalDefs.cert_def ctxt t (* FIXME adapt ps? *)
in (t', ((Thm.def_binding_optional (Binding.name c) name, atts), [(t', ps)])) end);
- val (_, ctxt') =
- ctxt |> fold (Variable.auto_fixes o #1) asms
+ val (_, ctxt') = ctxt
+ |> fold Variable.auto_fixes (map #1 asms)
|> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
- in ctxt' end
- | activate_elem (Notes (kind, facts)) ctxt =
+ in ctxt' end)
+ | init (Notes (kind, facts)) = (fn context =>
let
- val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
- val (res, ctxt') = ctxt |> ProofContext.note_thmss_i kind facts';
- in ctxt' end;
+ val facts' = Attrib.map_facts (Attrib.attribute_i (Context.theory_of context)) facts;
+ val context' = context |> Context.mapping
+ (PureThy.note_thmss kind facts' #> #2)
+ (ProofContext.note_thmss kind facts' #> #2);
+ in context' end);
-fun gen_activate prep_facts raw_elems ctxt =
+
+(* activate *)
+
+fun activate_i elem ctxt =
let
- fun activate elem ctxt =
- let val elem' = (map_ctxt_attrib Args.assignable o prep_facts ctxt) elem
- in (elem', activate_elem elem' ctxt) end
- val (elems, ctxt') = fold_map activate raw_elems ctxt;
- in (elems |> map (map_ctxt_attrib Args.closure), ctxt') end;
+ val elem' = map_ctxt_attrib Args.assignable elem;
+ val ctxt' = Context.proof_map (init elem') ctxt;
+ in (map_ctxt_attrib Args.closure elem', ctxt') end;
-fun check_name name =
- if Long_Name.is_qualified name then error ("Illegal qualified name: " ^ quote name)
- else name;
-
-fun prep_facts prep_name get intern ctxt =
- map_ctxt
- {binding = Binding.map_name prep_name,
+fun activate raw_elem ctxt =
+ let val elem = raw_elem |> map_ctxt
+ {binding = tap Name.of_binding,
typ = I,
term = I,
pattern = I,
- fact = get ctxt,
- attrib = intern (ProofContext.theory_of ctxt)};
-
-in
-
-fun activate x = gen_activate (prep_facts check_name ProofContext.get_fact Attrib.intern_src) x;
-fun activate_i x = gen_activate (K I) x;
+ fact = ProofContext.get_fact ctxt,
+ attrib = Attrib.intern_src (ProofContext.theory_of ctxt)}
+ in activate_i elem ctxt end;
end;
-
-end;
--- a/src/Pure/Isar/expression.ML Fri Mar 27 15:14:31 2009 -0700
+++ b/src/Pure/Isar/expression.ML Mon Mar 30 07:49:26 2009 -0700
@@ -20,14 +20,14 @@
(* Declaring locales *)
val cert_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context_i list ->
- Proof.context -> ((binding * typ option * mixfix) list * (string * morphism) list
+ Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
* Element.context_i list) * ((string * typ) list * Proof.context)
val cert_read_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context list ->
- Proof.context -> ((binding * typ option * mixfix) list * (string * morphism) list
+ Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
* Element.context_i list) * ((string * typ) list * Proof.context)
(*FIXME*)
val read_declaration: expression -> (Proof.context -> Proof.context) -> Element.context list ->
- Proof.context -> ((binding * typ option * mixfix) list * (string * morphism) list
+ Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
* Element.context_i list) * ((string * typ) list * Proof.context)
val add_locale: binding -> binding -> expression_i -> Element.context_i list ->
theory -> string * local_theory
@@ -70,32 +70,27 @@
fun intern thy instances = map (apfst (Locale.intern thy)) instances;
-(** Parameters of expression.
+(** Parameters of expression **)
- Sanity check of instantiations and extraction of implicit parameters.
- The latter only occurs iff strict = false.
- Positional instantiations are extended to match full length of parameter list
- of instantiated locale. **)
+(*Sanity check of instantiations and extraction of implicit parameters.
+ The latter only occurs iff strict = false.
+ Positional instantiations are extended to match full length of parameter list
+ of instantiated locale.*)
fun parameters_of thy strict (expr, fixed) =
let
fun reject_dups message xs =
- let val dups = duplicates (op =) xs
- in
- if null dups then () else error (message ^ commas dups)
- end;
+ (case duplicates (op =) xs of
+ [] => ()
+ | dups => error (message ^ commas dups));
- fun match_bind (n, b) = (n = Binding.name_of b);
- fun parm_eq ((b1, mx1: mixfix), (b2, mx2)) =
- Binding.eq_name (b1, b2) andalso
- (mx1 = mx2 orelse
- error ("Conflicting syntax for parameter " ^ quote (Binding.str_of b1) ^ " in expression"));
+ fun parm_eq ((p1: string, mx1: mixfix), (p2, mx2)) = p1 = p2 andalso
+ (mx1 = mx2 orelse error ("Conflicting syntax for parameter " ^ quote p1 ^ " in expression"));
- fun params_loc loc =
- (Locale.params_of thy loc |> map (fn (p, _, mx) => (p, mx)), loc);
- fun params_inst (expr as (loc, (prfx, Positional insts))) =
+ fun params_loc loc = Locale.params_of thy loc |> map (apfst #1);
+ fun params_inst (loc, (prfx, Positional insts)) =
let
- val (ps, loc') = params_loc loc;
+ val ps = params_loc loc;
val d = length ps - length insts;
val insts' =
if d < 0 then error ("More arguments than parameters in instantiation of locale " ^
@@ -103,29 +98,27 @@
else insts @ replicate d NONE;
val ps' = (ps ~~ insts') |>
map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE);
- in (ps', (loc', (prfx, Positional insts'))) end
- | params_inst (expr as (loc, (prfx, Named insts))) =
+ in (ps', (loc, (prfx, Positional insts'))) end
+ | params_inst (loc, (prfx, Named insts)) =
let
val _ = reject_dups "Duplicate instantiation of the following parameter(s): "
(map fst insts);
-
- val (ps, loc') = params_loc loc;
- val ps' = fold (fn (p, _) => fn ps =>
- if AList.defined match_bind ps p then AList.delete match_bind p ps
- else error (quote p ^" not a parameter of instantiated expression.")) insts ps;
- in (ps', (loc', (prfx, Named insts))) end;
+ val ps' = (insts, params_loc loc) |-> fold (fn (p, _) => fn ps =>
+ if AList.defined (op =) ps p then AList.delete (op =) p ps
+ else error (quote p ^ " not a parameter of instantiated expression"));
+ in (ps', (loc, (prfx, Named insts))) end;
fun params_expr is =
+ let
+ val (is', ps') = fold_map (fn i => fn ps =>
let
- val (is', ps') = fold_map (fn i => fn ps =>
- let
- val (ps', i') = params_inst i;
- val ps'' = distinct parm_eq (ps @ ps');
- in (i', ps'') end) is []
- in (ps', is') end;
+ val (ps', i') = params_inst i;
+ val ps'' = distinct parm_eq (ps @ ps');
+ in (i', ps'') end) is []
+ in (ps', is') end;
val (implicit, expr') = params_expr expr;
- val implicit' = map (#1 #> Name.of_binding) implicit;
+ val implicit' = map #1 implicit;
val fixed' = map (#1 #> Name.of_binding) fixed;
val _ = reject_dups "Duplicate fixed parameter(s): " fixed';
val implicit'' =
@@ -133,7 +126,7 @@
else
let val _ = reject_dups
"Parameter(s) declared simultaneously in expression and for clause: " (implicit' @ fixed')
- in map (fn (b, mx) => (b, NONE, mx)) implicit end;
+ in map (fn (x, mx) => (Binding.name x, NONE, mx)) implicit end;
in (expr', implicit'' @ fixed) end;
@@ -163,7 +156,7 @@
(* Instantiation morphism *)
-fun inst_morph (parm_names, parm_types) ((prfx, strict), insts') ctxt =
+fun inst_morph (parm_names, parm_types) ((prfx, mandatory), insts') ctxt =
let
(* parameters *)
val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst;
@@ -178,13 +171,13 @@
(* instantiation *)
val (type_parms'', res') = chop (length type_parms) res;
val insts'' = (parm_names ~~ res') |> map_filter
- (fn (inst as (x, Free (y, _))) => if x = y then NONE else SOME inst |
- inst => SOME inst);
+ (fn inst as (x, Free (y, _)) => if x = y then NONE else SOME inst
+ | inst => SOME inst);
val instT = Symtab.make (type_parm_names ~~ map Logic.dest_type type_parms'');
val inst = Symtab.make insts'';
in
(Element.inst_morphism (ProofContext.theory_of ctxt) (instT, inst) $>
- Morphism.binding_morphism (Binding.prefix strict prfx), ctxt')
+ Morphism.binding_morphism (Binding.prefix mandatory prfx), ctxt')
end;
@@ -247,7 +240,7 @@
in
((t, Syntax.check_props (ProofContext.set_mode ProofContext.mode_pattern ctxt') pats),
(ctxt', ts))
- end
+ end;
val (cs', (context', _)) = fold_map prep cs
(context, Syntax.check_terms
(ProofContext.set_mode ProofContext.mode_schematic context) (map fst cs));
@@ -265,7 +258,8 @@
(fold_burrow o fold_burrow) check (inst_cs :: elem_css @ [concl_cs]) ctxt;
val (elem_css', [concl_cs']) = chop (length elem_css) css';
in
- (map restore_inst (insts ~~ inst_cs'), map restore_elem (elems ~~ elem_css'),
+ (map restore_inst (insts ~~ inst_cs'),
+ map restore_elem (elems ~~ elem_css'),
concl_cs', ctxt')
end;
@@ -276,13 +270,14 @@
fun declare_elem prep_vars (Fixes fixes) ctxt =
let val (vars, _) = prep_vars fixes ctxt
- in ctxt |> ProofContext.add_fixes_i vars |> snd end
+ in ctxt |> ProofContext.add_fixes vars |> snd end
| declare_elem prep_vars (Constrains csts) ctxt =
ctxt |> prep_vars (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) csts) |> snd
| declare_elem _ (Assumes _) ctxt = ctxt
| declare_elem _ (Defines _) ctxt = ctxt
| declare_elem _ (Notes _) ctxt = ctxt;
+
(** Finish locale elements **)
fun closeup _ _ false elem = elem
@@ -319,8 +314,7 @@
fun finish_inst ctxt parms do_close (loc, (prfx, inst)) =
let
val thy = ProofContext.theory_of ctxt;
- val (parm_names, parm_types) = Locale.params_of thy loc |>
- map_split (fn (b, SOME T, _) => (Binding.name_of b, T));
+ val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt;
in (loc, morph) end;
@@ -347,11 +341,9 @@
val (raw_insts, fixed) = parameters_of thy strict (apfst (prep_expr thy) raw_import);
- fun prep_insts (loc, (prfx, inst)) (i, insts, ctxt) =
+ fun prep_insts_cumulative (loc, (prfx, inst)) (i, insts, ctxt) =
let
- val (parm_names, parm_types) = Locale.params_of thy loc |>
- map_split (fn (b, SOME T, _) => (Name.of_binding b, T))
- (*FIXME return value of Locale.params_of has strange type*)
+ val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
val inst' = prep_inst ctxt parm_names inst;
val parm_types' = map (TypeInfer.paramify_vars o
Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT) parm_types;
@@ -360,14 +352,14 @@
val (insts'', _, _, ctxt' (* FIXME not used *) ) = check_autofix insts' [] [] ctxt;
val inst''' = insts'' |> List.last |> snd |> snd;
val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst''') ctxt;
- val ctxt'' = Locale.activate_declarations thy (loc, morph) ctxt;
+ val ctxt'' = Locale.activate_declarations (loc, morph) ctxt;
in (i + 1, insts', ctxt'') end;
fun prep_elem insts raw_elem (elems, ctxt) =
let
val ctxt' = declare_elem prep_vars_elem raw_elem ctxt;
val elems' = elems @ [parse_elem parse_typ parse_prop ctxt' raw_elem];
- val (_, _, _, ctxt'') = check_autofix insts elems' [] ctxt';
+ val (_, _, _, ctxt'' (* FIXME not used *) ) = check_autofix insts elems' [] ctxt';
in (elems', ctxt') end;
fun prep_concl raw_concl (insts, elems, ctxt) =
@@ -376,12 +368,11 @@
in check_autofix insts elems concl ctxt end;
val fors = prep_vars_inst fixed ctxt1 |> fst;
- val ctxt2 = ctxt1 |> ProofContext.add_fixes_i fors |> snd;
- val (_, insts', ctxt3) = fold prep_insts raw_insts (0, [], ctxt2);
+ val ctxt2 = ctxt1 |> ProofContext.add_fixes fors |> snd;
+ val (_, insts', ctxt3) = fold prep_insts_cumulative raw_insts (0, [], ctxt2);
val ctxt4 = init_body ctxt3;
val (elems, ctxt5) = fold (prep_elem insts') raw_elems ([], ctxt4);
- val (insts, elems', concl, ctxt6) =
- prep_concl raw_concl (insts', elems, ctxt5);
+ val (insts, elems', concl, ctxt6) = prep_concl raw_concl (insts', elems, ctxt5);
(* Retrieve parameter types *)
val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Name.of_binding o #1) fixes)
@@ -390,18 +381,21 @@
val parms = xs ~~ Ts; (* params from expression and elements *)
val Fixes fors' = finish_primitive parms I (Fixes fors);
+ val fixed = map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fors';
val (deps, elems'') = finish ctxt6 parms do_close insts elems';
- in ((fors', deps, elems'', concl), (parms, ctxt7)) end
+ in ((fixed, deps, elems'', concl), (parms, ctxt7)) end
in
fun cert_full_context_statement x =
prep_full_context_statement (K I) (K I) ProofContext.cert_vars
make_inst ProofContext.cert_vars (K I) x;
+
fun cert_read_full_context_statement x =
prep_full_context_statement Syntax.parse_typ Syntax.parse_prop ProofContext.read_vars
make_inst ProofContext.cert_vars (K I) x;
+
fun read_full_context_statement x =
prep_full_context_statement Syntax.parse_typ Syntax.parse_prop ProofContext.read_vars
parse_inst ProofContext.read_vars intern x;
@@ -419,7 +413,7 @@
prep true false ([], []) I raw_elems raw_concl context;
val (_, context') = context |>
ProofContext.set_stmt true |>
- activate elems;
+ fold_map activate elems;
in (concl, context') end;
in
@@ -432,6 +426,9 @@
(* Locale declaration: import + elements *)
+fun fix_params params =
+ ProofContext.add_fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params) #> snd;
+
local
fun prep_declaration prep activate raw_import init_body raw_elems context =
@@ -440,11 +437,11 @@
prep false true raw_import init_body raw_elems [] context ;
(* Declare parameters and imported facts *)
val context' = context |>
- ProofContext.add_fixes_i fixed |> snd |>
- fold Locale.activate_local_facts deps;
+ fix_params fixed |>
+ fold (Context.proof_map o Locale.activate_facts) deps;
val (elems', _) = context' |>
ProofContext.set_stmt true |>
- activate elems;
+ fold_map activate elems;
in ((fixed, deps, elems'), (parms, ctxt')) end;
in
@@ -477,7 +474,7 @@
val propss = map (props_of thy) deps;
val goal_ctxt = context |>
- ProofContext.add_fixes_i fixed |> snd |>
+ fix_params fixed |>
(fold o fold) Variable.auto_fixes propss;
val export = Variable.export_morphism goal_ctxt context;
@@ -658,13 +655,13 @@
fun define_preds pname parms (((exts, exts'), (ints, ints')), defs) thy =
let
- val defs' = map (cterm_of thy #> Assumption.assume #> Drule.gen_all #> Drule.abs_def) defs;
+ val defs' = map (cterm_of thy #> Assumption.assume #> Drule.abs_def) defs;
val (a_pred, a_intro, a_axioms, thy'') =
if null exts then (NONE, NONE, [], thy)
else
let
- val aname = if null ints then pname else Binding.suffix_name ("_" ^ axiomsN) pname
+ val aname = if null ints then pname else Binding.suffix_name ("_" ^ axiomsN) pname;
val ((statement, intro, axioms), thy') =
thy
|> def_pred aname parms defs' exts exts';
@@ -731,13 +728,15 @@
val extraTs = fold Term.add_tfrees exts' [] \\ fold Term.add_tfreesT (map snd parms) [];
val _ =
if null extraTs then ()
- else warning ("Additional type variable(s) in locale specification " ^ quote (Binding.str_of bname));
+ else warning ("Additional type variable(s) in locale specification " ^
+ quote (Binding.str_of bname));
val a_satisfy = Element.satisfy_morphism a_axioms;
val b_satisfy = Element.satisfy_morphism b_axioms;
val params = fixed @
- (body_elems |> map_filter (fn Fixes fixes => SOME fixes | _ => NONE) |> flat);
+ maps (fn Fixes fixes =>
+ map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fixes | _ => []) body_elems;
val asm = if is_some b_statement then b_statement else a_statement;
val notes =
@@ -790,7 +789,7 @@
fun after_qed witss = ProofContext.theory
(fold2 (fn (name, morph) => fn wits => Locale.add_dependency target
(name, morph $> Element.satisfy_morphism wits $> export)) deps witss #>
- (fn thy => fold_rev Locale.activate_global_facts
+ (fn thy => fold_rev (Context.theory_map o Locale.activate_facts)
(Locale.get_registrations thy) thy));
in Element.witness_proof after_qed propss goal_ctxt end;
@@ -830,19 +829,19 @@
fun store_eqns_activate regs [] thy =
thy
|> fold (fn (name, morph) =>
- Locale.activate_global_facts (name, morph $> export)) regs
+ Context.theory_map (Locale.activate_facts (name, morph $> export))) regs
| store_eqns_activate regs eqs thy =
let
- val eqs' = eqs |> map (Morphism.thm (export' $> export) #>
- LocalDefs.meta_rewrite_rule (ProofContext.init thy) #>
+ val eqs' = eqs |> map (Morphism.thm (export' $> export));
+ val morph_eqs = eqs' |> map (LocalDefs.meta_rewrite_rule (ProofContext.init thy) #>
Drule.abs_def);
- val eq_morph = Element.eq_morphism thy eqs';
+ val eq_morph = Element.eq_morphism thy morph_eqs;
val eq_attns' = map ((apsnd o map) (Attrib.attribute_i thy)) eq_attns;
in
thy
|> fold (fn (name, morph) =>
Locale.amend_registration eq_morph (name, morph) #>
- Locale.activate_global_facts (name, morph $> eq_morph $> export)) regs
+ Context.theory_map (Locale.activate_facts (name, morph $> eq_morph $> export))) regs
|> PureThy.note_thmss Thm.lemmaK (eq_attns' ~~ map (fn eq => [([eq], [])]) eqs')
|> snd
end;
@@ -876,7 +875,7 @@
fun store_reg (name, morph) thms =
let
val morph' = morph $> Element.satisfy_morphism thms $> export;
- in Locale.activate_local_facts (name, morph') end;
+ in Context.proof_map (Locale.activate_facts (name, morph')) end;
fun after_qed wits =
Proof.map_context (fold2 store_reg regs wits);
--- a/src/Pure/Isar/local_defs.ML Fri Mar 27 15:14:31 2009 -0700
+++ b/src/Pure/Isar/local_defs.ML Mon Mar 30 07:49:26 2009 -0700
@@ -96,7 +96,7 @@
val lhss = map (fst o Logic.dest_equals) eqs;
in
ctxt
- |> ProofContext.add_fixes_i (map2 (fn x => fn mx => (x, NONE, mx)) bvars mxs) |> #2
+ |> ProofContext.add_fixes (map2 (fn x => fn mx => (x, NONE, mx)) bvars mxs) |> #2
|> fold Variable.declare_term eqs
|> ProofContext.add_assms_i def_export
(map2 (fn a => fn eq => (a, [(eq, [])])) (names ~~ atts) eqs)
@@ -115,7 +115,7 @@
val T = Term.fastype_of rhs;
val ([x'], ctxt') = ctxt
|> Variable.declare_term rhs
- |> ProofContext.add_fixes_i [(x, SOME T, mx)];
+ |> ProofContext.add_fixes [(x, SOME T, mx)];
val lhs = Free (x', T);
val _ = cert_def ctxt' (Logic.mk_equals (lhs, rhs));
fun abbrev_export _ _ = (I, Envir.expand_term_frees [((x', T), rhs)]);
--- a/src/Pure/Isar/locale.ML Fri Mar 27 15:14:31 2009 -0700
+++ b/src/Pure/Isar/locale.ML Mon Mar 30 07:49:26 2009 -0700
@@ -30,7 +30,7 @@
sig
(* Locale specification *)
val register_locale: binding ->
- (string * sort) list * (binding * typ option * mixfix) list ->
+ (string * sort) list * ((string * typ) * mixfix) list ->
term option * term list ->
thm option * thm option -> thm list ->
declaration list * declaration list ->
@@ -39,7 +39,7 @@
val intern: theory -> xstring -> string
val extern: theory -> string -> xstring
val defined: theory -> string -> bool
- val params_of: theory -> string -> (binding * typ option * mixfix) list
+ val params_of: theory -> string -> ((string * typ) * mixfix) list
val intros_of: theory -> string -> thm option * thm option
val axioms_of: theory -> string -> thm list
val instance_of: theory -> string -> morphism -> term list
@@ -56,10 +56,8 @@
val add_dependency: string -> string * morphism -> theory -> theory
(* Activation *)
- val activate_declarations: theory -> string * morphism ->
- Proof.context -> Proof.context
- val activate_global_facts: string * morphism -> theory -> theory
- val activate_local_facts: string * morphism -> Proof.context -> Proof.context
+ val activate_declarations: string * morphism -> Proof.context -> Proof.context
+ val activate_facts: string * morphism -> Context.generic -> Context.generic
val init: string -> theory -> Proof.context
(* Reasoning about locales *)
@@ -91,7 +89,7 @@
datatype locale = Loc of {
(** static part **)
- parameters: (string * sort) list * (binding * typ option * mixfix) list,
+ parameters: (string * sort) list * ((string * typ) * mixfix) list,
(* type and term parameters *)
spec: term option * term list,
(* assumptions (as a single predicate expression) and defines *)
@@ -109,8 +107,10 @@
fun mk_locale ((parameters, spec, intros, axioms), ((decls, notes), dependencies)) =
Loc {parameters = parameters, intros = intros, axioms = axioms, spec = spec,
decls = decls, notes = notes, dependencies = dependencies};
+
fun map_locale f (Loc {parameters, spec, intros, axioms, decls, notes, dependencies}) =
mk_locale (f ((parameters, spec, intros, axioms), ((decls, notes), dependencies)));
+
fun merge_locale (Loc {parameters, spec, intros, axioms, decls = (decls1, decls2),
notes, dependencies}, Loc {decls = (decls1', decls2'), notes = notes',
dependencies = dependencies', ...}) = mk_locale
@@ -163,7 +163,7 @@
fun axioms_of thy = #axioms o the_locale thy;
fun instance_of thy name morph = params_of thy name |>
- map (fn (b, T, _) => Morphism.term morph (Free (Name.of_binding b, the T)));
+ map (Morphism.term morph o Free o #1);
fun specification_of thy = #spec o the_locale thy;
@@ -178,26 +178,20 @@
(** Identifiers: activated locales in theory or proof context **)
-type identifiers = (string * term list) list;
-
-val empty = ([] : identifiers);
-
fun ident_eq thy ((n: string, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts);
local
-datatype 'a delayed = Ready of 'a | ToDo of ('a delayed * 'a delayed);
+datatype 'a delayed = Ready of 'a | ToDo of 'a delayed * 'a delayed;
structure Identifiers = GenericDataFun
(
- type T = identifiers delayed;
- val empty = Ready empty;
+ type T = (string * term list) list delayed;
+ val empty = Ready [];
val extend = I;
fun merge _ = ToDo;
);
-in
-
fun finish thy (ToDo (i1, i2)) = merge (ident_eq thy) (finish thy i1, finish thy i2)
| finish _ (Ready ids) = ids;
@@ -206,13 +200,10 @@
Ready _ => NONE
| ids => SOME (Context.theory_map (Identifiers.put (Ready (finish thy ids))) thy)))));
-fun get_global_idents thy =
- let val (Ready ids) = (Identifiers.get o Context.Theory) thy in ids end;
-val put_global_idents = Context.theory_map o Identifiers.put o Ready;
+in
-fun get_local_idents ctxt =
- let val (Ready ids) = (Identifiers.get o Context.Proof) ctxt in ids end;
-val put_local_idents = Context.proof_map o Identifiers.put o Ready;
+val get_idents = (fn Ready ids => ids) o Identifiers.get;
+val put_idents = Identifiers.put o Ready;
end;
@@ -228,15 +219,14 @@
then error "Roundup bound exceeded (sublocale relation probably not terminating)."
else
let
- val {parameters = (_, params), dependencies, ...} = the_locale thy name;
+ val dependencies = dependencies_of thy name;
val instance = instance_of thy name morph;
in
if member (ident_eq thy) marked (name, instance)
then (deps, marked)
else
let
- val dependencies' =
- map (fn ((name, morph'), _) => (name, morph' $> morph)) dependencies;
+ val dependencies' = map (fn (name, morph') => (name, morph' $> morph)) dependencies;
val marked' = (name, instance) :: marked;
val (deps', marked'') = fold_rev (add thy (depth + 1)) dependencies' ([], marked');
in
@@ -250,12 +240,12 @@
let
(* Find all dependencies incuding new ones (which are dependencies enriching
existing registrations). *)
- val (dependencies, marked') = add thy 0 (name, morph) ([], empty);
+ val (dependencies, marked') = add thy 0 (name, morph) ([], []);
(* Filter out exisiting fragments. *)
val dependencies' = filter_out (fn (name, morph) =>
member (ident_eq thy) marked (name, instance_of thy name morph)) dependencies;
in
- (merge (ident_eq thy) (marked, marked'), input |> fold_rev (activate_dep thy) dependencies')
+ (merge (ident_eq thy) (marked, marked'), input |> fold_rev activate_dep dependencies')
end;
end;
@@ -263,12 +253,14 @@
(* Declarations, facts and entire locale content *)
-fun activate_decls thy (name, morph) ctxt =
+fun activate_decls (name, morph) context =
let
+ val thy = Context.theory_of context;
val {decls = (typ_decls, term_decls), ...} = the_locale thy name;
in
- ctxt |> fold_rev (fn (decl, _) => Context.proof_map (decl morph)) typ_decls |>
- fold_rev (fn (decl, _) => Context.proof_map (decl morph)) term_decls
+ context
+ |> fold_rev (fn (decl, _) => decl morph) typ_decls
+ |> fold_rev (fn (decl, _) => decl morph) term_decls
end;
fun activate_notes activ_elem transfer thy (name, morph) input =
@@ -284,84 +276,52 @@
fun activate_all name thy activ_elem transfer (marked, input) =
let
- val {parameters = (_, params), spec = (asm, defs), ...} =
- the_locale thy name;
- in
- input |>
- (if not (null params) then activ_elem (Fixes params) else I) |>
+ val {parameters = (_, params), spec = (asm, defs), ...} = the_locale thy name;
+ val input' = input |>
+ (not (null params) ?
+ activ_elem (Fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params))) |>
(* FIXME type parameters *)
- (if is_some asm then activ_elem (Assumes [(Attrib.empty_binding, [(the asm, [])])]) else I) |>
+ (case asm of SOME A => activ_elem (Assumes [(Attrib.empty_binding, [(A, [])])]) | _ => I) |>
(if not (null defs)
then activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs))
- else I) |>
- pair marked |> roundup thy (activate_notes activ_elem transfer) (name, Morphism.identity)
+ else I);
+ val activate = activate_notes activ_elem transfer thy;
+ in
+ roundup thy activate (name, Morphism.identity) (marked, input')
end;
(** Public activation functions **)
-local
-
-fun init_global_elem (Notes (kind, facts)) thy =
+fun activate_declarations dep = Context.proof_map (fn context =>
let
- val facts' = Attrib.map_facts (Attrib.attribute_i thy) facts
- in PureThy.note_thmss kind facts' thy |> snd end
+ val thy = Context.theory_of context;
+ val context' = roundup thy activate_decls dep (get_idents context, context) |-> put_idents;
+ in context' end);
-fun init_local_elem (Fixes fixes) ctxt = ctxt |>
- ProofContext.add_fixes_i fixes |> snd
- | init_local_elem (Assumes assms) ctxt =
- let
- val assms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) assms
- in
- ctxt |> fold Variable.auto_fixes (maps (map fst o snd) assms') |>
- ProofContext.add_assms_i Assumption.assume_export assms' |> snd
- end
- | init_local_elem (Defines defs) ctxt =
- let
- val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs
- in
- ctxt |> fold Variable.auto_fixes (map (fst o snd) defs') |>
- ProofContext.add_assms_i LocalDefs.def_export (map (fn (attn, t) => (attn, [t])) defs') |>
- snd
- end
- | init_local_elem (Notes (kind, facts)) ctxt =
- let
- val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts
- in ProofContext.note_thmss_i kind facts' ctxt |> snd end
-
-fun cons_elem false (Notes notes) elems = elems
- | cons_elem _ elem elems = elem :: elems
-
-in
-
-fun activate_declarations thy dep ctxt =
- roundup thy activate_decls dep (get_local_idents ctxt, ctxt) |-> put_local_idents;
-
-fun activate_global_facts dep thy =
- roundup thy (activate_notes init_global_elem Element.transfer_morphism)
- dep (get_global_idents thy, thy) |-> put_global_idents;
-
-fun activate_local_facts dep ctxt =
- roundup (ProofContext.theory_of ctxt)
- (activate_notes init_local_elem (Element.transfer_morphism o ProofContext.theory_of)) dep
- (get_local_idents ctxt, ctxt) |-> put_local_idents;
+fun activate_facts dep context =
+ let
+ val thy = Context.theory_of context;
+ val activate = activate_notes Element.init (Element.transfer_morphism o Context.theory_of) thy;
+ in roundup thy activate dep (get_idents context, context) |-> put_idents end;
fun init name thy =
- activate_all name thy init_local_elem (Element.transfer_morphism o ProofContext.theory_of)
- (empty, ProofContext.init thy) |-> put_local_idents;
+ activate_all name thy Element.init (Element.transfer_morphism o Context.theory_of)
+ ([], Context.Proof (ProofContext.init thy)) |-> put_idents |> Context.proof_of;
-fun print_locale thy show_facts name =
+fun print_locale thy show_facts raw_name =
let
- val name' = intern thy name;
- val ctxt = init name' thy
+ val name = intern thy raw_name;
+ val ctxt = init name thy;
+ fun cons_elem (elem as Notes _) = show_facts ? cons elem
+ | cons_elem elem = cons elem;
+ val elems =
+ activate_all name thy cons_elem (K (Element.transfer_morphism thy)) ([], [])
+ |> snd |> rev;
in
- Pretty.big_list "locale elements:"
- (activate_all name' thy (cons_elem show_facts) (K (Element.transfer_morphism thy))
- (empty, []) |> snd |> rev |>
- map (Element.pretty_ctxt ctxt) |> map Pretty.chunks) |> Pretty.writeln
- end
-
-end;
+ Pretty.big_list "locale elements:" (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)
+ |> Pretty.writeln
+ end;
(*** Registrations: interpretations in theories ***)
@@ -379,24 +339,24 @@
);
val get_registrations =
- Registrations.get #> map fst #> map (apsnd op $>);
+ Registrations.get #> map (#1 #> apsnd op $>);
fun add_registration (name, (base_morph, export)) thy =
- roundup thy (fn _ => fn (name', morph') =>
- (Registrations.map o cons) ((name', (morph', export)), stamp ()))
- (name, base_morph) (get_global_idents thy, thy) |> snd
- (* FIXME |-> put_global_idents ?*);
+ roundup thy (fn (name', morph') => Registrations.map (cons ((name', (morph', export)), stamp ())))
+ (name, base_morph) (get_idents (Context.Theory thy), thy) |> snd;
+ (* FIXME |-> put_global_idents ?*)
fun amend_registration morph (name, base_morph) thy =
let
- val regs = (Registrations.get #> map fst) thy;
+ val regs = map #1 (Registrations.get thy);
val base = instance_of thy name base_morph;
fun match (name', (morph', _)) =
name = name' andalso eq_list (op aconv) (base, instance_of thy name' morph');
val i = find_index match (rev regs);
- val _ = if i = ~1 then error ("No registration of locale " ^
+ val _ =
+ if i = ~1 then error ("No registration of locale " ^
quote (extern thy name) ^ " and parameter instantiation " ^
- space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ " available.")
+ space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ " available")
else ();
in
Registrations.map (nth_map (length regs - 1 - i)
@@ -404,14 +364,13 @@
end;
-
(*** Storing results ***)
(* Theorems *)
fun add_thmss loc kind args ctxt =
let
- val ([Notes args'], ctxt') = Element.activate_i [Notes (kind, args)] ctxt;
+ val (Notes args', ctxt') = Element.activate_i (Notes (kind, args)) ctxt;
val ctxt'' = ctxt' |> ProofContext.theory (
(change_locale loc o apfst o apsnd) (cons (args', stamp ()))
#>
--- a/src/Pure/Isar/obtain.ML Fri Mar 27 15:14:31 2009 -0700
+++ b/src/Pure/Isar/obtain.ML Mon Mar 30 07:49:26 2009 -0700
@@ -118,7 +118,7 @@
(*obtain vars*)
val (vars, vars_ctxt) = prep_vars raw_vars ctxt;
- val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
+ val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes vars;
val xs = map (Name.of_binding o #1) vars;
(*obtain asms*)
@@ -294,7 +294,7 @@
|> Proof.fix_i (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms)
|> `Proof.context_of |-> (fn fix_ctxt => Proof.assm_i
(obtain_export fix_ctxt rule (map cert ts)) [(Thm.empty_binding, asms)])
- |> Proof.add_binds_i AutoBind.no_facts
+ |> Proof.bind_terms AutoBind.no_facts
end;
val goal = Var (("guess", 0), propT);
--- a/src/Pure/Isar/proof.ML Fri Mar 27 15:14:31 2009 -0700
+++ b/src/Pure/Isar/proof.ML Mon Mar 30 07:49:26 2009 -0700
@@ -17,7 +17,7 @@
val theory_of: state -> theory
val map_context: (context -> context) -> state -> state
val map_contexts: (context -> context) -> state -> state
- val add_binds_i: (indexname * term option) list -> state -> state
+ val bind_terms: (indexname * term option) list -> state -> state
val put_thms: bool -> string * thm list option -> state -> state
val the_facts: state -> thm list
val the_fact: state -> thm
@@ -204,7 +204,7 @@
fun map_contexts f = map_all (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
-val add_binds_i = map_context o ProofContext.add_binds_i;
+val bind_terms = map_context o ProofContext.bind_terms;
val put_thms = map_context oo ProofContext.put_thms;
@@ -531,15 +531,15 @@
local
-fun gen_fix add_fixes args =
+fun gen_fix prep_vars args =
assert_forward
- #> map_context (snd o add_fixes args)
+ #> map_context (fn ctxt => snd (ProofContext.add_fixes (prep_vars ctxt args) ctxt))
#> put_facts NONE;
in
-val fix = gen_fix ProofContext.add_fixes;
-val fix_i = gen_fix ProofContext.add_fixes_i;
+val fix = gen_fix (fn ctxt => fn args => fst (ProofContext.read_vars args ctxt));
+val fix_i = gen_fix (K I);
end;
@@ -620,29 +620,27 @@
local
-fun gen_thmss note_ctxt more_facts opt_chain opt_result prep_atts args state =
+fun gen_thmss more_facts opt_chain opt_result prep_atts prep_fact args state =
state
|> assert_forward
- |> map_context_result (note_ctxt (Attrib.map_facts (prep_atts (theory_of state)) args))
+ |> map_context_result (ProofContext.note_thmss ""
+ (Attrib.map_facts_refs (prep_atts (theory_of state)) (prep_fact (context_of state)) args))
|> these_factss (more_facts state)
||> opt_chain
|> opt_result;
in
-val note_thmss = gen_thmss (ProofContext.note_thmss "") (K []) I #2 Attrib.attribute;
-val note_thmss_i = gen_thmss (ProofContext.note_thmss_i "") (K []) I #2 (K I);
-
-val from_thmss =
- gen_thmss (ProofContext.note_thmss "") (K []) chain #2 Attrib.attribute o no_binding;
-val from_thmss_i = gen_thmss (ProofContext.note_thmss_i "") (K []) chain #2 (K I) o no_binding;
+val note_thmss = gen_thmss (K []) I #2 Attrib.attribute ProofContext.get_fact;
+val note_thmss_i = gen_thmss (K []) I #2 (K I) (K I);
-val with_thmss =
- gen_thmss (ProofContext.note_thmss "") the_facts chain #2 Attrib.attribute o no_binding;
-val with_thmss_i = gen_thmss (ProofContext.note_thmss_i "") the_facts chain #2 (K I) o no_binding;
+val from_thmss = gen_thmss (K []) chain #2 Attrib.attribute ProofContext.get_fact o no_binding;
+val from_thmss_i = gen_thmss (K []) chain #2 (K I) (K I) o no_binding;
-val local_results =
- gen_thmss (ProofContext.note_thmss_i "") (K []) I I (K I) o map (apsnd Thm.simple_fact);
+val with_thmss = gen_thmss the_facts chain #2 Attrib.attribute ProofContext.get_fact o no_binding;
+val with_thmss_i = gen_thmss the_facts chain #2 (K I) (K I) o no_binding;
+
+val local_results = gen_thmss (K []) I I (K I) (K I) o map (apsnd Thm.simple_fact);
fun get_thmss state srcs = the_facts (note_thmss [((Binding.empty, []), srcs)] state);
@@ -653,11 +651,13 @@
local
-fun gen_using f g note prep_atts args state =
+fun gen_using f g prep_atts prep_fact args state =
state
|> assert_backward
|> map_context_result
- (note "" (Attrib.map_facts (prep_atts (theory_of state)) (no_binding args)))
+ (ProofContext.note_thmss ""
+ (Attrib.map_facts_refs (prep_atts (theory_of state)) (prep_fact (context_of state))
+ (no_binding args)))
|> (fn (named_facts, state') =>
state' |> map_goal I (fn (statement, _, using, goal, before_qed, after_qed) =>
let
@@ -671,10 +671,10 @@
in
-val using = gen_using append_using (K (K I)) ProofContext.note_thmss Attrib.attribute;
-val using_i = gen_using append_using (K (K I)) ProofContext.note_thmss_i (K I);
-val unfolding = gen_using unfold_using unfold_goals ProofContext.note_thmss Attrib.attribute;
-val unfolding_i = gen_using unfold_using unfold_goals ProofContext.note_thmss_i (K I);
+val using = gen_using append_using (K (K I)) Attrib.attribute ProofContext.get_fact;
+val using_i = gen_using append_using (K (K I)) (K I) (K I);
+val unfolding = gen_using unfold_using unfold_goals Attrib.attribute ProofContext.get_fact;
+val unfolding_i = gen_using unfold_using unfold_goals (K I) (K I);
end;
@@ -695,7 +695,7 @@
in
state'
|> assume_i assumptions
- |> add_binds_i AutoBind.no_facts
+ |> bind_terms AutoBind.no_facts
|> `the_facts |-> (fn thms => note_thmss_i [((Binding.name name, []), [(thms, [])])])
end;
--- a/src/Pure/Isar/proof_context.ML Fri Mar 27 15:14:31 2009 -0700
+++ b/src/Pure/Isar/proof_context.ML Mon Mar 30 07:49:26 2009 -0700
@@ -70,8 +70,7 @@
val export: Proof.context -> Proof.context -> thm list -> thm list
val export_morphism: Proof.context -> Proof.context -> morphism
val norm_export_morphism: Proof.context -> Proof.context -> morphism
- val add_binds: (indexname * string option) list -> Proof.context -> Proof.context
- val add_binds_i: (indexname * term option) list -> Proof.context -> Proof.context
+ val bind_terms: (indexname * term option) list -> Proof.context -> Proof.context
val auto_bind_goal: term list -> Proof.context -> Proof.context
val auto_bind_facts: term list -> Proof.context -> Proof.context
val match_bind: bool -> (string list * string) list -> Proof.context -> term list * Proof.context
@@ -102,19 +101,15 @@
val mandatory_path: string -> Proof.context -> Proof.context
val restore_naming: Proof.context -> Proof.context -> Proof.context
val reset_naming: Proof.context -> Proof.context
- val note_thmss: string -> (Thm.binding * (Facts.ref * attribute list) list) list ->
- Proof.context -> (string * thm list) list * Proof.context
- val note_thmss_i: string -> (Thm.binding * (thm list * attribute list) list) list ->
+ val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list ->
Proof.context -> (string * thm list) list * Proof.context
val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
val read_vars: (binding * string option * mixfix) list -> Proof.context ->
(binding * typ option * mixfix) list * Proof.context
val cert_vars: (binding * typ option * mixfix) list -> Proof.context ->
(binding * typ option * mixfix) list * Proof.context
- val add_fixes: (binding * string option * mixfix) list ->
- Proof.context -> string list * Proof.context
- val add_fixes_i: (binding * typ option * mixfix) list ->
- Proof.context -> string list * Proof.context
+ val add_fixes: (binding * typ option * mixfix) list -> Proof.context ->
+ string list * Proof.context
val auto_fixes: Proof.context * (term list list * 'a) -> Proof.context * (term list list * 'a)
val bind_fixes: string list -> Proof.context -> (term -> term) * Proof.context
val add_assms: Assumption.export ->
@@ -542,17 +537,17 @@
local
-structure AllowDummies = ProofDataFun(type T = bool fun init _ = false);
+structure Allow_Dummies = ProofDataFun(type T = bool fun init _ = false);
fun check_dummies ctxt t =
- if AllowDummies.get ctxt then t
+ if Allow_Dummies.get ctxt then t
else Term.no_dummy_patterns t handle TERM _ => error "Illegal dummy pattern(s) in term";
fun prepare_dummies ts = #1 (fold_map Term.replace_dummy_patterns ts 1);
in
-val allow_dummies = AllowDummies.put true;
+val allow_dummies = Allow_Dummies.put true;
fun prepare_patterns ctxt =
let val Mode {pattern, ...} = get_mode ctxt in
@@ -775,7 +770,7 @@
-(** bindings **)
+(** term bindings **)
(* simult_matches *)
@@ -785,28 +780,23 @@
| SOME (env, _) => map (apsnd snd) (Envir.alist_of env));
-(* add_binds(_i) *)
-
-local
+(* bind_terms *)
-fun gen_bind prep (xi as (x, _), raw_t) ctxt =
+val bind_terms = fold (fn (xi, t) => fn ctxt =>
ctxt
- |> Variable.add_binds [(xi, Option.map (prep (set_mode mode_default ctxt)) raw_t)];
+ |> Variable.bind_term (xi, Option.map (cert_term (set_mode mode_default ctxt)) t));
-in
+
+(* auto_bind *)
fun drop_schematic (b as (xi, SOME t)) = if Term.exists_subterm is_Var t then (xi, NONE) else b
| drop_schematic b = b;
-val add_binds = fold (gen_bind Syntax.read_term);
-val add_binds_i = fold (gen_bind cert_term);
+fun auto_bind f ts ctxt = ctxt |> bind_terms (map drop_schematic (f (theory_of ctxt) ts));
-fun auto_bind f ts ctxt = ctxt |> add_binds_i (map drop_schematic (f (theory_of ctxt) ts));
val auto_bind_goal = auto_bind AutoBind.goal;
val auto_bind_facts = auto_bind AutoBind.facts;
-end;
-
(* match_bind(_i) *)
@@ -831,8 +821,8 @@
val ctxt'' =
tap (Variable.warn_extra_tfrees ctxt)
(if gen then
- ctxt (*sic!*) |> fold Variable.declare_term (map #2 binds') |> add_binds_i binds''
- else ctxt' |> add_binds_i binds'');
+ ctxt (*sic!*) |> fold Variable.declare_term (map #2 binds') |> bind_terms binds''
+ else ctxt' |> bind_terms binds'');
in (ts, ctxt'') end;
in
@@ -868,8 +858,8 @@
(*generalize result: context evaluated now, binds added later*)
val gen = Variable.exportT_terms ctxt' ctxt;
- fun gen_binds c = c |> add_binds_i (map #1 binds ~~ map SOME (gen (map #2 binds)));
- in (ctxt' |> add_binds_i (map (apsnd SOME) binds), (propss, gen_binds)) end;
+ fun gen_binds c = c |> bind_terms (map #1 binds ~~ map SOME (gen (map #2 binds)));
+ in (ctxt' |> bind_terms (map (apsnd SOME) binds), (propss, gen_binds)) end;
in
@@ -965,25 +955,23 @@
| update_thms do_props (b, SOME ths) ctxt = ctxt |> map_facts
(Facts.add_local do_props (naming_of ctxt) (b, ths) #> snd);
-fun gen_note_thmss get k = fold_map (fn ((b, more_attrs), raw_facts) => fn ctxt =>
+in
+
+fun note_thmss kind = fold_map (fn ((b, more_attrs), raw_facts) => fn ctxt =>
let
val pos = Binding.pos_of b;
val name = full_name ctxt b;
val _ = ContextPosition.report_visible ctxt (Markup.local_fact_decl name) pos;
- val facts = PureThy.name_thmss false pos name (map (apfst (get ctxt)) raw_facts);
+ val facts = PureThy.name_thmss false pos name raw_facts;
fun app (th, attrs) x =
- swap (Library.foldl_map (Thm.proof_attributes (surround (Thm.kind k) (attrs @ more_attrs))) (x, th));
+ swap (Library.foldl_map
+ (Thm.proof_attributes (surround (Thm.kind kind) (attrs @ more_attrs))) (x, th));
val (res, ctxt') = fold_map app facts ctxt;
val thms = PureThy.name_thms false false pos name (flat res);
val Mode {stmt, ...} = get_mode ctxt;
in ((name, thms), ctxt' |> update_thms stmt (b, SOME thms)) end);
-in
-
-fun note_thmss k = gen_note_thmss get_fact k;
-fun note_thmss_i k = gen_note_thmss (K I) k;
-
fun put_thms do_props thms ctxt = ctxt
|> map_naming (K local_naming)
|> ContextPosition.set_visible false
@@ -1115,9 +1103,11 @@
error ("Illegal mixfix syntax for internal/skolem constant " ^ quote x)
else (true, (x, T, mx));
-fun gen_fixes prep raw_vars ctxt =
+in
+
+fun add_fixes raw_vars ctxt =
let
- val (vars, _) = prep raw_vars ctxt;
+ val (vars, _) = cert_vars raw_vars ctxt;
val (xs', ctxt') = Variable.add_fixes (map (Name.of_binding o #1) vars) ctxt;
val ctxt'' =
ctxt'
@@ -1127,11 +1117,6 @@
ContextPosition.report_visible ctxt (Markup.fixed_decl x') (Binding.pos_of b));
in (xs', ctxt'') end;
-in
-
-val add_fixes = gen_fixes read_vars;
-val add_fixes_i = gen_fixes cert_vars;
-
end;
@@ -1142,7 +1127,7 @@
fun bind_fixes xs ctxt =
let
- val (_, ctxt') = ctxt |> add_fixes_i (map (fn x => (Binding.name x, NONE, NoSyn)) xs);
+ val (_, ctxt') = ctxt |> add_fixes (map (fn x => (Binding.name x, NONE, NoSyn)) xs);
fun bind (t as Free (x, T)) =
if member (op =) xs x then
(case lookup_skolem ctxt' x of SOME x' => Free (x', T) | NONE => t)
@@ -1167,7 +1152,7 @@
in
ctxt2
|> auto_bind_facts (flat propss)
- |> note_thmss_i Thm.assumptionK (map fst args ~~ map (map (fn th => ([th], []))) premss)
+ |> note_thmss Thm.assumptionK (map fst args ~~ map (map (fn th => ([th], []))) premss)
end;
in
@@ -1221,7 +1206,7 @@
val RuleCases.Case {assumes, binds, cases, ...} = RuleCases.apply ts c;
in
ctxt'
- |> add_binds_i (map drop_schematic binds)
+ |> bind_terms (map drop_schematic binds)
|> add_cases true (map (apsnd SOME) cases)
|> pair (assumes, (binds, cases))
end;
--- a/src/Pure/Isar/rule_insts.ML Fri Mar 27 15:14:31 2009 -0700
+++ b/src/Pure/Isar/rule_insts.ML Mon Mar 30 07:49:26 2009 -0700
@@ -283,7 +283,7 @@
val (param_names, ctxt') = ctxt
|> Variable.declare_thm thm
|> Thm.fold_terms Variable.declare_constraints st
- |> ProofContext.add_fixes_i (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params);
+ |> ProofContext.add_fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params);
(* Process type insts: Tinsts_env *)
fun absent xi = error
--- a/src/Pure/Isar/specification.ML Fri Mar 27 15:14:31 2009 -0700
+++ b/src/Pure/Isar/specification.ML Mon Mar 30 07:49:26 2009 -0700
@@ -108,7 +108,7 @@
val thy = ProofContext.theory_of ctxt;
val (vars, vars_ctxt) = ctxt |> prep_vars raw_vars;
- val (xs, params_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
+ val (xs, params_ctxt) = vars_ctxt |> ProofContext.add_fixes vars;
val Asss = (map o map) (map (parse_prop params_ctxt) o snd) raw_specss;
val names = Variable.names_of (params_ctxt |> (fold o fold o fold) Variable.declare_term Asss)
@@ -312,7 +312,7 @@
|> fold_map ProofContext.inferred_param xs;
val asm = Term.list_all_free (xs ~~ Ts, Logic.list_implies (props, thesis));
in
- ctxt' |> (snd o ProofContext.add_fixes_i (map (fn b => (b, NONE, NoSyn)) bs));
+ ctxt' |> (snd o ProofContext.add_fixes (map (fn b => (b, NONE, NoSyn)) bs));
ctxt' |> Variable.auto_fixes asm
|> ProofContext.add_assms_i Assumption.assume_export
[((name, [ContextRules.intro_query NONE]), [(asm, [])])]
@@ -325,9 +325,9 @@
val stmt = [((Binding.empty, atts), [(thesis, [])])];
val (facts, goal_ctxt) = elems_ctxt
- |> (snd o ProofContext.add_fixes_i [(Binding.name AutoBind.thesisN, NONE, NoSyn)])
+ |> (snd o ProofContext.add_fixes [(Binding.name AutoBind.thesisN, NONE, NoSyn)])
|> fold_map assume_case (obtains ~~ propp)
- |-> (fn ths => ProofContext.note_thmss_i Thm.assumptionK
+ |-> (fn ths => ProofContext.note_thmss Thm.assumptionK
[((Binding.name Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
in ((prems, stmt, facts), goal_ctxt) end);
@@ -370,7 +370,7 @@
end;
in
goal_ctxt
- |> ProofContext.note_thmss_i Thm.assumptionK
+ |> ProofContext.note_thmss Thm.assumptionK
[((Binding.name AutoBind.assmsN, []), [(prems, [])])]
|> snd
|> Proof.theorem_i before_qed after_qed' (map snd stmt)
--- a/src/Pure/Isar/theory_target.ML Fri Mar 27 15:14:31 2009 -0700
+++ b/src/Pure/Isar/theory_target.ML Mon Mar 30 07:49:26 2009 -0700
@@ -160,9 +160,9 @@
in
lthy |> LocalTheory.theory
(PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd)
- |> not is_locale ? LocalTheory.target (ProofContext.note_thmss_i kind global_facts #> snd)
+ |> not is_locale ? LocalTheory.target (ProofContext.note_thmss kind global_facts #> snd)
|> is_locale ? LocalTheory.target (Locale.add_thmss target kind target_facts)
- |> ProofContext.note_thmss_i kind local_facts
+ |> ProofContext.note_thmss kind local_facts
end;
--- a/src/Pure/ML/ml_antiquote.ML Fri Mar 27 15:14:31 2009 -0700
+++ b/src/Pure/ML/ml_antiquote.ML Mon Mar 30 07:49:26 2009 -0700
@@ -87,7 +87,7 @@
val _ = macro "note" (Args.context :|-- (fn ctxt =>
P.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms >> (fn ((a, srcs), ths) =>
((a, map (Attrib.attribute (ProofContext.theory_of ctxt)) srcs), [(ths, [])])))
- >> (fn args => #2 (ProofContext.note_thmss_i "" args ctxt))));
+ >> (fn args => #2 (ProofContext.note_thmss "" args ctxt))));
val _ = value "ctyp" (Args.typ >> (fn T =>
"Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T)));
--- a/src/Pure/Tools/find_theorems.ML Fri Mar 27 15:14:31 2009 -0700
+++ b/src/Pure/Tools/find_theorems.ML Mon Mar 30 07:49:26 2009 -0700
@@ -11,8 +11,8 @@
Pattern of 'term
val tac_limit: int ref
val limit: int ref
- val find_theorems: Proof.context -> thm option -> bool ->
- (bool * string criterion) list -> (Facts.ref * thm) list
+ val find_theorems: Proof.context -> thm option -> int option -> bool ->
+ (bool * string criterion) list -> int option * (Facts.ref * thm) list
val pretty_thm: Proof.context -> Facts.ref * thm -> Pretty.T
val print_theorems: Proof.context -> thm option -> int option -> bool ->
(bool * string criterion) list -> unit
@@ -254,12 +254,13 @@
in app (opt_add r r', consts', fs) end;
in app end;
+
in
fun filter_criterion ctxt opt_goal (b, c) =
(if b then I else (apfst opt_not)) o filter_crit ctxt opt_goal c;
-fun all_filters filters thms =
+fun sorted_filter filters thms =
let
fun eval_filters thm = app_filters thm (SOME (0, 0), NONE, filters);
@@ -270,6 +271,15 @@
prod_ord int_ord int_ord ((p1, s1), (p0, s0));
in map_filter eval_filters thms |> sort thm_ord |> map #2 end;
+fun lazy_filter filters = let
+ fun lazy_match thms = Seq.make (fn () => first_match thms)
+
+ and first_match [] = NONE
+ | first_match (thm::thms) =
+ case app_filters thm (SOME (0, 0), NONE, filters) of
+ NONE => first_match thms
+ | SOME (_, t) => SOME (t, lazy_match thms);
+ in lazy_match end;
end;
@@ -334,7 +344,7 @@
val limit = ref 40;
-fun find_theorems ctxt opt_goal rem_dups raw_criteria =
+fun find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
let
val assms = ProofContext.get_fact ctxt (Facts.named "local.assms")
handle ERROR _ => [];
@@ -344,13 +354,25 @@
val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
val filters = map (filter_criterion ctxt opt_goal') criteria;
- val raw_matches = all_filters filters (all_facts_of ctxt);
+ fun find_all facts =
+ let
+ val raw_matches = sorted_filter filters facts;
+
+ val matches =
+ if rem_dups
+ then rem_thm_dups (nicer_shortest ctxt) raw_matches
+ else raw_matches;
- val matches =
- if rem_dups
- then rem_thm_dups (nicer_shortest ctxt) raw_matches
- else raw_matches;
- in matches end;
+ val len = length matches;
+ val lim = the_default (! limit) opt_limit;
+ in (SOME len, Library.drop (len - lim, matches)) end;
+
+ val find =
+ if rem_dups orelse is_none opt_limit
+ then find_all
+ else pair NONE o Seq.list_of o Seq.take (the opt_limit) o lazy_filter filters
+
+ in find (all_facts_of ctxt) end;
fun pretty_thm ctxt (thmref, thm) = Pretty.block
@@ -362,11 +384,16 @@
val start = start_timing ();
val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
- val matches = find_theorems ctxt opt_goal rem_dups raw_criteria;
-
- val len = length matches;
- val lim = the_default (! limit) opt_limit;
- val thms = Library.drop (len - lim, matches);
+ val (foundo, thms) = find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria;
+ val returned = length thms;
+
+ val tally_msg =
+ case foundo of
+ NONE => "displaying " ^ string_of_int returned ^ " theorems"
+ | SOME found => "found " ^ string_of_int found ^ " theorems" ^
+ (if returned < found
+ then " (" ^ string_of_int returned ^ " displayed)"
+ else "");
val end_msg = " in " ^ Time.toString (#all (end_timing start)) ^ " secs";
in
@@ -374,16 +401,12 @@
:: Pretty.str "" ::
(if null thms then [Pretty.str ("nothing found" ^ end_msg)]
else
- [Pretty.str ("found " ^ string_of_int len ^ " theorems" ^
- (if len <= lim then ""
- else " (" ^ string_of_int lim ^ " displayed)")
- ^ end_msg ^ ":"), Pretty.str ""] @
+ [Pretty.str (tally_msg ^ end_msg ^ ":"), Pretty.str ""] @
map (pretty_thm ctxt) thms)
|> Pretty.chunks |> Pretty.writeln
end;
-
(** command syntax **)
fun find_theorems_cmd ((opt_lim, rem_dups), spec) =
--- a/src/Pure/variable.ML Fri Mar 27 15:14:31 2009 -0700
+++ b/src/Pure/variable.ML Mon Mar 30 07:49:26 2009 -0700
@@ -30,7 +30,7 @@
val declare_thm: thm -> Proof.context -> Proof.context
val thm_context: thm -> Proof.context
val variant_frees: Proof.context -> term list -> (string * 'a) list -> (string * 'a) list
- val add_binds: (indexname * term option) list -> Proof.context -> Proof.context
+ val bind_term: indexname * term option -> Proof.context -> Proof.context
val expand_binds: Proof.context -> term -> term
val lookup_const: Proof.context -> string -> string option
val is_const: Proof.context -> string -> bool
@@ -250,15 +250,13 @@
(** term bindings **)
-fun add_bind (xi, NONE) = map_binds (Vartab.delete_safe xi)
- | add_bind ((x, i), SOME t) =
+fun bind_term (xi, NONE) = map_binds (Vartab.delete_safe xi)
+ | bind_term ((x, i), SOME t) =
let
val u = Term.close_schematic_term t;
val U = Term.fastype_of u;
in declare_term u #> map_binds (Vartab.update ((x, i), (U, u))) end;
-val add_binds = fold add_bind;
-
fun expand_binds ctxt =
let
val binds = binds_of ctxt;
@@ -486,7 +484,7 @@
val all_vars = Thm.fold_terms Term.add_vars st [];
val no_binds = map (fn (xi, _) => (xi, NONE)) all_vars;
in
- add_binds no_binds #>
+ fold bind_term no_binds #>
fold (declare_constraints o Var) all_vars #>
focus (Thm.cprem_of st i)
end;
--- a/src/Tools/auto_solve.ML Fri Mar 27 15:14:31 2009 -0700
+++ b/src/Tools/auto_solve.ML Mon Mar 30 07:49:26 2009 -0700
@@ -13,6 +13,7 @@
sig
val auto : bool ref
val auto_time_limit : int ref
+ val limit : int ref
val seek_solution : bool -> Proof.state -> Proof.state
end;
@@ -22,6 +23,7 @@
val auto = ref false;
val auto_time_limit = ref 2500;
+val limit = ref 5;
fun seek_solution int state =
let
@@ -34,9 +36,9 @@
handle TERM _ => t::conj_to_list ts;
val crits = [(true, FindTheorems.Solves)];
- fun find g = (NONE, FindTheorems.find_theorems ctxt g true crits);
- fun find_cterm g = (SOME g, FindTheorems.find_theorems ctxt
- (SOME (Goal.init g)) true crits);
+ fun find g = (NONE, snd (FindTheorems.find_theorems ctxt g (SOME (!limit)) false crits));
+ fun find_cterm g = (SOME g, snd (FindTheorems.find_theorems ctxt
+ (SOME (Goal.init g)) (SOME (!limit)) false crits));
fun prt_result (goal, results) =
let
--- a/src/Tools/code/code_target.ML Fri Mar 27 15:14:31 2009 -0700
+++ b/src/Tools/code/code_target.ML Mon Mar 30 07:49:26 2009 -0700
@@ -411,7 +411,7 @@
val names_hidden = names_class @ names_inst @ names_tyco @ names_const;
val names2 = subtract (op =) names_hidden names1;
val program3 = Graph.subgraph (not o member (op =) names_hidden) program2;
- val names_all = Graph.all_succs program2 names2;
+ val names_all = Graph.all_succs program3 names2;
val includes = abs_includes names_all;
val program4 = Graph.subgraph (member (op =) names_all) program3;
val empty_funs = filter_out (member (op =) abortable)
--- a/src/Tools/code/code_wellsorted.ML Fri Mar 27 15:14:31 2009 -0700
+++ b/src/Tools/code/code_wellsorted.ML Mon Mar 30 07:49:26 2009 -0700
@@ -353,14 +353,20 @@
fun code_deps thy consts =
let
val eqngr = code_depgr thy consts;
- fun mk_entry (const, (_, (_, parents))) =
- let
- val name = Code_Unit.string_of_const thy const;
- val nameparents = map (Code_Unit.string_of_const thy) parents;
- in { name = name, ID = name, dir = "", unfold = true,
- path = "", parents = nameparents }
- end;
- val prgr = Graph.fold ((fn x => fn xs => xs @ [x]) o mk_entry) eqngr [];
+ val constss = Graph.strong_conn eqngr;
+ val mapping = Symtab.empty |> fold (fn consts => fold (fn const =>
+ Symtab.update (const, consts)) consts) constss;
+ fun succs consts = consts
+ |> maps (Graph.imm_succs eqngr)
+ |> subtract (op =) consts
+ |> map (the o Symtab.lookup mapping)
+ |> distinct (op =);
+ val conn = [] |> fold (fn consts => cons (consts, succs consts)) constss;
+ fun namify consts = map (Code_Unit.string_of_const thy) consts
+ |> commas;
+ val prgr = map (fn (consts, constss) =>
+ { name = namify consts, ID = namify consts, dir = "", unfold = true,
+ path = "", parents = map namify constss }) conn;
in Present.display_graph prgr end;
local