(* Title: HOL/ex/Locales.thy
ID: $Id$
Author: Markus Wenzel, LMU Muenchen
License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
header {* Basic use of locales in Isabelle/Isar *}
theory Locales = Main:
text {*
Locales provide a mechanism for encapsulating local contexts. The
original version due to Florian Kamm\"uller \cite{Kamm-et-al:1999}
refers directly to the raw meta-logic of Isabelle. The present
version for Isabelle/Isar
\cite{Wenzel:1999,Wenzel:2001:isar-ref,Wenzel:2001:Thesis} builds on
top of the rich infrastructure of proof contexts instead; this also
covers essential extra-logical concepts like term abbreviations or
local theorem attributes (e.g.\ declarations of simplification
rules).
Subsequently, we demonstrate basic use of locales to model
mathematical structures (by the inevitable group theory example).
*}
text_raw {*
\newcommand{\isasyminv}{\isasyminverse}
\newcommand{\isasymone}{\isamath{1}}
\newcommand{\isasymIN}{\isatext{\isakeyword{in}}}
*}
subsection {* Local contexts as mathematical structures *}
text {*
The following definitions of @{text group} and @{text abelian_group}
merely encapsulate local parameters (with private syntax) and
assumptions; local definitions may be given as well, but are not
shown here.
*}
locale group =
fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<cdot>" 70)
and inv :: "'a \<Rightarrow> 'a" ("(_\<inv>)" [1000] 999)
and one :: 'a ("\<one>")
assumes assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
and left_inv: "x\<inv> \<cdot> x = \<one>"
and left_one: "\<one> \<cdot> x = x"
locale abelian_group = group +
assumes commute: "x \<cdot> y = y \<cdot> x"
text {*
\medskip We may now prove theorems within a local context, just by
including a directive ``@{text "(\<IN> name)"}'' in the goal
specification. The final result will be stored within the named
locale; a second copy is exported to the enclosing theory context.
*}
theorem (in group)
right_inv: "x \<cdot> x\<inv> = \<one>"
proof -
have "x \<cdot> x\<inv> = \<one> \<cdot> (x \<cdot> x\<inv>)" by (simp only: left_one)
also have "\<dots> = \<one> \<cdot> x \<cdot> x\<inv>" by (simp only: assoc)
also have "\<dots> = (x\<inv>)\<inv> \<cdot> x\<inv> \<cdot> x \<cdot> x\<inv>" by (simp only: left_inv)
also have "\<dots> = (x\<inv>)\<inv> \<cdot> (x\<inv> \<cdot> x) \<cdot> x\<inv>" by (simp only: assoc)
also have "\<dots> = (x\<inv>)\<inv> \<cdot> \<one> \<cdot> x\<inv>" by (simp only: left_inv)
also have "\<dots> = (x\<inv>)\<inv> \<cdot> (\<one> \<cdot> x\<inv>)" by (simp only: assoc)
also have "\<dots> = (x\<inv>)\<inv> \<cdot> x\<inv>" by (simp only: left_one)
also have "\<dots> = \<one>" by (simp only: left_inv)
finally show ?thesis .
qed
theorem (in group)
right_one: "x \<cdot> \<one> = x"
proof -
have "x \<cdot> \<one> = x \<cdot> (x\<inv> \<cdot> x)" by (simp only: left_inv)
also have "\<dots> = x \<cdot> x\<inv> \<cdot> x" by (simp only: assoc)
also have "\<dots> = \<one> \<cdot> x" by (simp only: right_inv)
also have "\<dots> = x" by (simp only: left_one)
finally show ?thesis .
qed
text {*
\medskip Apart from the named context we may also refer to further
context elements (parameters, assumptions, etc.) in a casual manner;
these are discharged when the proof is finished.
*}
theorem (in group)
(assumes eq: "e \<cdot> x = x")
one_equality: "\<one> = e"
proof -
have "\<one> = x \<cdot> x\<inv>" by (simp only: right_inv)
also have "\<dots> = (e \<cdot> x) \<cdot> x\<inv>" by (simp only: eq)
also have "\<dots> = e \<cdot> (x \<cdot> x\<inv>)" by (simp only: assoc)
also have "\<dots> = e \<cdot> \<one>" by (simp only: right_inv)
also have "\<dots> = e" by (simp only: right_one)
finally show ?thesis .
qed
theorem (in group)
(assumes eq: "x' \<cdot> x = \<one>")
inv_equality: "x\<inv> = x'"
proof -
have "x\<inv> = \<one> \<cdot> x\<inv>" by (simp only: left_one)
also have "\<dots> = (x' \<cdot> x) \<cdot> x\<inv>" by (simp only: eq)
also have "\<dots> = x' \<cdot> (x \<cdot> x\<inv>)" by (simp only: assoc)
also have "\<dots> = x' \<cdot> \<one>" by (simp only: right_inv)
also have "\<dots> = x'" by (simp only: right_one)
finally show ?thesis .
qed
theorem (in group)
inv_prod: "(x \<cdot> y)\<inv> = y\<inv> \<cdot> x\<inv>"
proof (rule inv_equality)
show "(y\<inv> \<cdot> x\<inv>) \<cdot> (x \<cdot> y) = \<one>"
proof -
have "(y\<inv> \<cdot> x\<inv>) \<cdot> (x \<cdot> y) = (y\<inv> \<cdot> (x\<inv> \<cdot> x)) \<cdot> y" by (simp only: assoc)
also have "\<dots> = (y\<inv> \<cdot> \<one>) \<cdot> y" by (simp only: left_inv)
also have "\<dots> = y\<inv> \<cdot> y" by (simp only: right_one)
also have "\<dots> = \<one>" by (simp only: left_inv)
finally show ?thesis .
qed
qed
text {*
\medskip Established results are automatically propagated through
the hierarchy of locales. Below we establish a trivial fact in
commutative groups, while referring both to theorems of @{text
group} and the additional assumption of @{text abelian_group}.
*}
theorem (in abelian_group)
inv_prod': "(x \<cdot> y)\<inv> = x\<inv> \<cdot> y\<inv>"
proof -
have "(x \<cdot> y)\<inv> = y\<inv> \<cdot> x\<inv>" by (rule inv_prod)
also have "\<dots> = x\<inv> \<cdot> y\<inv>" by (rule commute)
finally show ?thesis .
qed
text {*
\medskip Some further properties of inversion in general group
theory follow.
*}
theorem (in group)
inv_inv: "(x\<inv>)\<inv> = x"
proof (rule inv_equality)
show "x \<cdot> x\<inv> = \<one>" by (simp only: right_inv)
qed
theorem (in group)
(assumes eq: "x\<inv> = y\<inv>")
inv_inject: "x = y"
proof -
have "x = x \<cdot> \<one>" by (simp only: right_one)
also have "\<dots> = x \<cdot> (y\<inv> \<cdot> y)" by (simp only: left_inv)
also have "\<dots> = x \<cdot> (x\<inv> \<cdot> y)" by (simp only: eq)
also have "\<dots> = (x \<cdot> x\<inv>) \<cdot> y" by (simp only: assoc)
also have "\<dots> = \<one> \<cdot> y" by (simp only: right_inv)
also have "\<dots> = y" by (simp only: left_one)
finally show ?thesis .
qed
text {*
\bigskip We see that this representation of structures as local
contexts is rather light-weight and convenient to use for abstract
reasoning. Here the ``components'' (the group operations) have been
exhibited directly as context parameters; logically this corresponds
to a curried predicate definition. Occasionally, this
``externalized'' version of the informal idea of classes of tuple
structures may cause some inconveniences, especially in
meta-theoretical studies (involving functors from groups to groups,
for example).
Another drawback of the naive approach above is that concrete syntax
will get lost on any kind of operation on the locale itself (such as
renaming, copying, or instantiation). Whenever the particular
terminology of local parameters is affected the associated syntax
would have to be changed as well, which is hard to achieve formally.
*}
subsection {* Explicit structures referenced implicitly *}
text {*
The issue of multiple parameters raised above may be easily
addressed by stating properties over a record of group operations,
instead of the individual constituents. See
\cite{Naraschewski-Wenzel:1998,Nipkow-et-al:2001:HOL} on
(extensible) record types in Isabelle/HOL.
*}
record 'a group =
prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
inv :: "'a \<Rightarrow> 'a"
one :: 'a
text {*
Now concrete syntax essentially needs refer to record selections;
this is possible by giving defined operations with private syntax
within the locale (e.g.\ see appropriate examples by Kamm\"uller).
In the subsequent formulation of group structures we go one step
further by using \emph{implicit} references to the underlying
abstract entity. To this end we define global syntax, which is
translated to refer to the ``current'' structure at hand, denoted by
the dummy item ``@{text \<struct>}'' (according to the builtin syntax
mechanism for locales).
*}
syntax
"_prod" :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<cdot>" 70)
"_inv" :: "'a \<Rightarrow> 'a" ("(_\<inv>)" [1000] 999)
"_one" :: 'a ("\<one>")
translations
"x \<cdot> y" \<rightleftharpoons> "prod \<struct> x y"
"x\<inv>" \<rightleftharpoons> "inv \<struct> x"
"\<one>" \<rightleftharpoons> "one \<struct>"
text {*
The following locale definition introduces a single parameter, which
is declared as a ``\isakeyword{structure}''. In its context the
dummy ``@{text \<struct>}'' refers to this very parameter, independently of
the present naming.
*}
locale group_struct =
fixes G :: "'a group" (structure)
assumes assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
and left_inv: "x\<inv> \<cdot> x = \<one>"
and left_one: "\<one> \<cdot> x = x"
text {*
We may now proceed to prove results within @{text group_struct} just
as before for @{text group}. Proper treatment of ``@{text \<struct>}'' is
hidden in concrete syntax, so the proof text is exactly the same as
before.
*}
theorem (in group_struct)
right_inv: "x \<cdot> x\<inv> = \<one>"
proof -
have "x \<cdot> x\<inv> = \<one> \<cdot> (x \<cdot> x\<inv>)" by (simp only: left_one)
also have "\<dots> = \<one> \<cdot> x \<cdot> x\<inv>" by (simp only: assoc)
also have "\<dots> = (x\<inv>)\<inv> \<cdot> x\<inv> \<cdot> x \<cdot> x\<inv>" by (simp only: left_inv)
also have "\<dots> = (x\<inv>)\<inv> \<cdot> (x\<inv> \<cdot> x) \<cdot> x\<inv>" by (simp only: assoc)
also have "\<dots> = (x\<inv>)\<inv> \<cdot> \<one> \<cdot> x\<inv>" by (simp only: left_inv)
also have "\<dots> = (x\<inv>)\<inv> \<cdot> (\<one> \<cdot> x\<inv>)" by (simp only: assoc)
also have "\<dots> = (x\<inv>)\<inv> \<cdot> x\<inv>" by (simp only: left_one)
also have "\<dots> = \<one>" by (simp only: left_inv)
finally show ?thesis .
qed
theorem (in group_struct)
right_one: "x \<cdot> \<one> = x"
proof -
have "x \<cdot> \<one> = x \<cdot> (x\<inv> \<cdot> x)" by (simp only: left_inv)
also have "\<dots> = x \<cdot> x\<inv> \<cdot> x" by (simp only: assoc)
also have "\<dots> = \<one> \<cdot> x" by (simp only: right_inv)
also have "\<dots> = x" by (simp only: left_one)
finally show ?thesis .
qed
text {*
\medskip Several implicit structures may be active at the same time
(say up to 3 in practice). The concrete syntax facility for locales
actually maintains indexed dummies @{text "\<struct>\<^sub>1"}, @{text
"\<struct>\<^sub>2"}, @{text "\<struct>\<^sub>3"}, \dots (@{text \<struct>} is the same as
@{text "\<struct>\<^sub>1"}). So we are able to provide concrete syntax to
cover the 2nd and 3rd group structure as well.
*}
syntax
"_prod'" :: "'a \<Rightarrow> index \<Rightarrow> 'a \<Rightarrow> 'a" ("(_ \<cdot>_/ _)" [70, 1000, 71] 70)
"_inv'" :: "'a \<Rightarrow> index \<Rightarrow> 'a" ("(_\<inv>_)" [1000] 999)
"_one'" :: "index \<Rightarrow> 'a" ("\<one>_")
translations
"x \<cdot>\<^sub>2 y" \<rightleftharpoons> "prod \<struct>\<^sub>2 x y"
"x \<cdot>\<^sub>3 y" \<rightleftharpoons> "prod \<struct>\<^sub>3 x y"
"x\<inv>\<^sub>2" \<rightleftharpoons> "inv \<struct>\<^sub>2 x"
"x\<inv>\<^sub>3" \<rightleftharpoons> "inv \<struct>\<^sub>3 x"
"\<one>\<^sub>2" \<rightleftharpoons> "one \<struct>\<^sub>2"
"\<one>\<^sub>3" \<rightleftharpoons> "one \<struct>\<^sub>3"
text {*
\medskip The following synthetic example demonstrates how to refer
to several structures of type @{text group} succinctly; one might
also think of working with several renamed versions of the @{text
group_struct} locale above.
*}
lemma
(fixes G :: "'a group" (structure)
and H :: "'a group" (structure))
True
proof
have "x \<cdot> y \<cdot> \<one> = prod G (prod G x y) (one G)" ..
have "x \<cdot>\<^sub>2 y \<cdot>\<^sub>2 \<one>\<^sub>2 = prod H (prod H x y) (one H)" ..
have "x \<cdot> \<one>\<^sub>2 = prod G x (one H)" ..
qed
text {*
\medskip As a minor drawback of this advanced technique we require
slightly more work to setup abstract and concrete syntax properly
(but only once in the beginning). The resulting casual mode of
writing @{text "x \<cdot> y"} for @{text "prod G x y"} etc.\ mimics common
practice of informal mathematics quite nicely, while using a simple
and robust formal representation.
*}
end