--- a/doc-src/Locales/Locales/Examples.thy Sun Mar 29 19:41:04 2009 +0200
+++ b/doc-src/Locales/Locales/Examples.thy Sun Mar 29 19:48:35 2009 +0200
@@ -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 Sun Mar 29 19:41:04 2009 +0200
+++ b/doc-src/Locales/Locales/Examples1.thy Sun Mar 29 19:48:35 2009 +0200
@@ -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 Sun Mar 29 19:41:04 2009 +0200
+++ b/doc-src/Locales/Locales/Examples2.thy Sun Mar 29 19:48:35 2009 +0200
@@ -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 Sun Mar 29 19:41:04 2009 +0200
+++ b/doc-src/Locales/Locales/Examples3.thy Sun Mar 29 19:48:35 2009 +0200
@@ -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
@@ -284,11 +291,13 @@
instances in the order of the sequence.
The qualifiers in the expression are already a familiar concept from
- the \isakeyword{interpretation} command. They serve to distinguish
- names (in particular theorem names) for the two partial orders
- within the locale. Qualifiers in the \isakeyword{locale} command
- default to optional. Here are examples of theorems in locale @{text
- order_preserving}: *}
+ 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
@@ -359,7 +368,7 @@
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 preseverd. *}
+ the second parameter. Its concrete syntax is preserved. *}
text {* The inheritance diagram of the situation we have now is shown
--- a/doc-src/Locales/Locales/document/Examples.tex Sun Mar 29 19:41:04 2009 +0200
+++ b/doc-src/Locales/Locales/document/Examples.tex Sun Mar 29 19:48:35 2009 +0200
@@ -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 Sun Mar 29 19:41:04 2009 +0200
+++ b/doc-src/Locales/Locales/document/Examples1.tex Sun Mar 29 19:48:35 2009 +0200
@@ -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 Sun Mar 29 19:41:04 2009 +0200
+++ b/doc-src/Locales/Locales/document/Examples2.tex Sun Mar 29 19:48:35 2009 +0200
@@ -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 Sun Mar 29 19:41:04 2009 +0200
+++ b/doc-src/Locales/Locales/document/Examples3.tex Sun Mar 29 19:48:35 2009 +0200
@@ -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
@@ -493,10 +529,13 @@
instances in the order of the sequence.
The qualifiers in the expression are already a familiar concept from
- the \isakeyword{interpretation} command. They serve to distinguish
- names (in particular theorem names) for the two partial orders
- within the locale. Qualifiers in the \isakeyword{locale} command
- default to optional. Here are examples of theorems in locale \isa{order{\isacharunderscore}preserving}:%
+ 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%
%
@@ -610,7 +649,7 @@
\ 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 preseverd.%
+ the second parameter. Its concrete syntax is preserved.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/Locales/Locales/document/root.tex Sun Mar 29 19:41:04 2009 +0200
+++ b/doc-src/Locales/Locales/document/root.tex Sun Mar 29 19:48:35 2009 +0200
@@ -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/src/Pure/Isar/expression.ML Sun Mar 29 19:41:04 2009 +0200
+++ b/src/Pure/Isar/expression.ML Sun Mar 29 19:48:35 2009 +0200
@@ -832,10 +832,10 @@
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