--- a/src/HOL/ex/Locales.thy Thu Nov 08 00:25:36 2001 +0100
+++ b/src/HOL/ex/Locales.thy Thu Nov 08 00:26:06 2001 +0100
@@ -4,20 +4,33 @@
License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
-header {* Basic use of locales *}
+header {* Basic use of locales in Isabelle/Isar *}
theory Locales = Main:
text {*
- The inevitable group theory examples formulated with locales.
+ Locales provide a mechanism for encapsulating local contexts. While
+ the original version by Florian Kamm\"uller refers to the raw
+ meta-logic, the present one of Isabelle/Isar builds on top of the
+ rich infrastructure of Isar proof contexts. 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_raw {*
- \newcommand{\isasyminv}{\isasyminverse}
- \newcommand{\isasymone}{\isamath{1}}
+text {*
+ The following definitions of @{text group} and @{text abelian_group}
+ simply encapsulate local parameters (with private syntax) and
+ assumptions; local definitions may be given as well, but are not
+ shown here.
*}
locale group =
@@ -31,6 +44,13 @@
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 -
@@ -55,6 +75,12 @@
finally show ?thesis .
qed
+text {*
+ \medskip Apart from the named locale context we may also refer to
+ further ad-hoc elements (parameters, assumptions, etc.); these are
+ discharged when the proof is finished.
+*}
+
theorem (in group)
(assumes eq: "e \<cdot> x = x")
one_equality: "\<one> = e"
@@ -92,6 +118,13 @@
qed
qed
+text {*
+ \medskip Results are automatically propagated through the hierarchy
+ of locales. Below we establish a trivial fact of commutative
+ groups, while referring both to theorems of @{text group} and the
+ characteristic assumption of @{text abelian_group}.
+*}
+
theorem (in abelian_group)
inv_prod': "(x \<cdot> y)\<inv> = x\<inv> \<cdot> y\<inv>"
proof -
@@ -100,6 +133,10 @@
finally show ?thesis .
qed
+text {*
+ \medskip Some further facts of general group theory follow.
+*}
+
theorem (in group)
inv_inv: "(x\<inv>)\<inv> = x"
proof (rule inv_equality)
@@ -119,37 +156,149 @@
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).
-subsection {* Referencing structures implicitly *}
+ 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 {* Referencing explicit structures implicitly *}
-record 'a semigroup =
+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.
+*}
+
+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
- "_prod1" :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<odot>" 70)
- "_prod2" :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<odot>\<^sub>2" 70)
- "_prod3" :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<odot>\<^sub>3" 70)
+ "_prod" :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<cdot>" 70)
+ "_inv" :: "'a \<Rightarrow> 'a" ("(_\<inv>)" [1000] 999)
+ "_one" :: 'a ("\<one>")
translations
- "x \<odot> y" \<rightleftharpoons> "(\<struct>prod) x y"
- "x \<odot>\<^sub>2 y" \<rightleftharpoons> "(\<struct>\<struct>prod) x y"
- "x \<odot>\<^sub>3 y" \<rightleftharpoons> "(\<struct>\<struct>\<struct>prod) x y"
+ "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 ``\isakeyword{structure}''.
+*}
+
+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 {*
+ In its context the dummy ``@{text \<struct>}'' refers to this very
+ parameter, independently of the present naming. 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 for @{text
+ group} given 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 renamed versions of the @{text
+ group_struct} locale above.
+*}
lemma
- (fixes S :: "'a semigroup" (structure)
- and T :: "'a semigroup" (structure)
- and U :: "'a semigroup" (structure))
- "prod S a b = a \<odot> b" ..
+ (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
-lemma
- (fixes S :: "'a semigroup" (structure)
- and T :: "'a semigroup" (structure)
- and U :: "'a semigroup" (structure))
- "prod T a b = a \<odot>\<^sub>2 b" ..
+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.
+*}
-lemma
- (fixes S :: "'a semigroup" (structure)
- and T :: "'a semigroup" (structure)
- and U :: "'a semigroup" (structure))
- "prod U a b = a \<odot>\<^sub>3 b" ..
-
-end
\ No newline at end of file
+end