1.1 --- a/src/HOL/ex/Locales.thy Thu Dec 20 21:15:37 2001 +0100
1.2 +++ b/src/HOL/ex/Locales.thy Fri Dec 21 00:38:04 2001 +0100
1.3 @@ -1,6 +1,6 @@
1.4 (* Title: HOL/ex/Locales.thy
1.5 ID: $Id$
1.6 - Author: Markus Wenzel, LMU Muenchen
1.7 + Author: Markus Wenzel, LMU München
1.8 License: GPL (GNU GENERAL PUBLIC LICENSE)
1.9 *)
1.10
1.11 @@ -18,7 +18,7 @@
1.12
1.13 text {*
1.14 Locales provide a mechanism for encapsulating local contexts. The
1.15 - original version due to Florian Kamm\"uller \cite{Kamm-et-al:1999}
1.16 + original version due to Florian Kammüller \cite{Kamm-et-al:1999}
1.17 refers directly to the raw meta-logic of Isabelle. Semantically, a
1.18 locale is just a (curried) predicate of the pure meta-logic
1.19 \cite{Paulson:1989}.
1.20 @@ -94,7 +94,7 @@
1.21 shown here.
1.22 *}
1.23
1.24 -locale group =
1.25 +locale group_context =
1.26 fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<cdot>" 70)
1.27 and inv :: "'a \<Rightarrow> 'a" ("(_\<inv>)" [1000] 999)
1.28 and one :: 'a ("\<one>")
1.29 @@ -102,7 +102,7 @@
1.30 and left_inv: "x\<inv> \<cdot> x = \<one>"
1.31 and left_one: "\<one> \<cdot> x = x"
1.32
1.33 -locale abelian_group = group +
1.34 +locale abelian_group_context = group_context +
1.35 assumes commute: "x \<cdot> y = y \<cdot> x"
1.36
1.37 text {*
1.38 @@ -112,7 +112,7 @@
1.39 locale; a second copy is exported to the enclosing theory context.
1.40 *}
1.41
1.42 -theorem (in group)
1.43 +theorem (in group_context)
1.44 right_inv: "x \<cdot> x\<inv> = \<one>"
1.45 proof -
1.46 have "x \<cdot> x\<inv> = \<one> \<cdot> (x \<cdot> x\<inv>)" by (simp only: left_one)
1.47 @@ -126,7 +126,7 @@
1.48 finally show ?thesis .
1.49 qed
1.50
1.51 -theorem (in group)
1.52 +theorem (in group_context)
1.53 right_one: "x \<cdot> \<one> = x"
1.54 proof -
1.55 have "x \<cdot> \<one> = x \<cdot> (x\<inv> \<cdot> x)" by (simp only: left_inv)
1.56 @@ -142,7 +142,7 @@
1.57 these are discharged when the proof is finished.
1.58 *}
1.59
1.60 -theorem (in group)
1.61 +theorem (in group_context)
1.62 (assumes eq: "e \<cdot> x = x")
1.63 one_equality: "\<one> = e"
1.64 proof -
1.65 @@ -154,7 +154,7 @@
1.66 finally show ?thesis .
1.67 qed
1.68
1.69 -theorem (in group)
1.70 +theorem (in group_context)
1.71 (assumes eq: "x' \<cdot> x = \<one>")
1.72 inv_equality: "x\<inv> = x'"
1.73 proof -
1.74 @@ -166,7 +166,7 @@
1.75 finally show ?thesis .
1.76 qed
1.77
1.78 -theorem (in group)
1.79 +theorem (in group_context)
1.80 inv_prod: "(x \<cdot> y)\<inv> = y\<inv> \<cdot> x\<inv>"
1.81 proof (rule inv_equality)
1.82 show "(y\<inv> \<cdot> x\<inv>) \<cdot> (x \<cdot> y) = \<one>"
1.83 @@ -186,7 +186,7 @@
1.84 group} and the additional assumption of @{text abelian_group}.
1.85 *}
1.86
1.87 -theorem (in abelian_group)
1.88 +theorem (in abelian_group_context)
1.89 inv_prod': "(x \<cdot> y)\<inv> = x\<inv> \<cdot> y\<inv>"
1.90 proof -
1.91 have "(x \<cdot> y)\<inv> = y\<inv> \<cdot> x\<inv>" by (rule inv_prod)
1.92 @@ -207,13 +207,13 @@
1.93 follow.
1.94 *}
1.95
1.96 -theorem (in group)
1.97 +theorem (in group_context)
1.98 inv_inv: "(x\<inv>)\<inv> = x"
1.99 proof (rule inv_equality)
1.100 show "x \<cdot> x\<inv> = \<one>" by (simp only: right_inv)
1.101 qed
1.102
1.103 -theorem (in group)
1.104 +theorem (in group_context)
1.105 (assumes eq: "x\<inv> = y\<inv>")
1.106 inv_inject: "x = y"
1.107 proof -
1.108 @@ -263,7 +263,7 @@
1.109
1.110 text {*
1.111 The mixfix annotations above include a special ``structure index
1.112 - indicator'' @{text \<index>} that makes grammer productions dependent on
1.113 + indicator'' @{text \<index>} that makes gammer productions dependent on
1.114 certain parameters that have been declared as ``structure'' in a
1.115 locale context later on. Thus we achieve casual notation as
1.116 encountered in informal mathematics, e.g.\ @{text "x \<cdot> y"} for
1.117 @@ -275,11 +275,11 @@
1.118 internally.
1.119 *}
1.120
1.121 -locale semigroup_struct =
1.122 +locale semigroup =
1.123 fixes S :: "'a group" (structure)
1.124 assumes assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
1.125
1.126 -locale group_struct = semigroup_struct G +
1.127 +locale group = semigroup G +
1.128 assumes left_inv: "x\<inv> \<cdot> x = \<one>"
1.129 and left_one: "\<one> \<cdot> x = x"
1.130
1.131 @@ -294,13 +294,12 @@
1.132 of locale facts will get qualified accordingly, e.g. @{text S.assoc}
1.133 versus @{text G.assoc}.
1.134
1.135 - \medskip We may now proceed to prove results within @{text
1.136 - group_struct} just as before for @{text group}. The subsequent
1.137 - proof texts are exactly the same as despite the more advanced
1.138 - internal arrangement.
1.139 + \medskip We may now proceed to prove results within @{text group}
1.140 + just as before for @{text group}. The subsequent proof texts are
1.141 + exactly the same as despite the more advanced internal arrangement.
1.142 *}
1.143
1.144 -theorem (in group_struct)
1.145 +theorem (in group)
1.146 right_inv: "x \<cdot> x\<inv> = \<one>"
1.147 proof -
1.148 have "x \<cdot> x\<inv> = \<one> \<cdot> (x \<cdot> x\<inv>)" by (simp only: left_one)
1.149 @@ -314,7 +313,7 @@
1.150 finally show ?thesis .
1.151 qed
1.152
1.153 -theorem (in group_struct)
1.154 +theorem (in group)
1.155 right_one: "x \<cdot> \<one> = x"
1.156 proof -
1.157 have "x \<cdot> \<one> = x \<cdot> (x\<inv> \<cdot> x)" by (simp only: left_inv)
1.158 @@ -325,28 +324,26 @@
1.159 qed
1.160
1.161 text {*
1.162 - FIXME
1.163 - \medskip Several implicit structures may be active at the same time
1.164 - (say up to 3 in practice). The concrete syntax facility for locales
1.165 - actually maintains indexed dummies @{text "\<struct>\<^sub>1"}, @{text
1.166 - "\<struct>\<^sub>2"}, @{text "\<struct>\<^sub>3"}, \dots (@{text \<struct>} is the same as
1.167 - @{text "\<struct>\<^sub>1"}). So we are able to provide concrete syntax to
1.168 - cover the 2nd and 3rd group structure as well.
1.169 + \medskip Several implicit structures may be active at the same time.
1.170 + The concrete syntax facility for locales actually maintains indexed
1.171 + structures that may be references implicitly --- via mixfix
1.172 + annotations that have been decorated by an ``index argument''
1.173 + (@{text \<index>}).
1.174
1.175 - \medskip The following synthetic example demonstrates how to refer
1.176 - to several structures of type @{text group} succinctly; one might
1.177 - also think of working with several renamed versions of the @{text
1.178 - group_struct} locale above.
1.179 + The following synthetic example demonstrates how to refer to several
1.180 + structures of type @{text group} succinctly. We work with two
1.181 + versions of the @{text group} locale above.
1.182 *}
1.183
1.184 -lemma
1.185 - (fixes G :: "'a group" (structure)
1.186 - and H :: "'a group" (structure)) (* FIXME (uses group_struct G + group_struct H) *)
1.187 - True
1.188 -proof
1.189 - have "x \<cdot> y \<cdot> \<one> = prod G (prod G x y) (one G)" ..
1.190 - have "x \<cdot>\<^sub>2 y \<cdot>\<^sub>2 \<one>\<^sub>2 = prod H (prod H x y) (one H)" ..
1.191 - have "x \<cdot> \<one>\<^sub>2 = prod G x (one H)" ..
1.192 -qed
1.193 +lemma (uses group G + group H)
1.194 + "x \<cdot> y \<cdot> \<one> = prod G (prod G x y) (one G)" and
1.195 + "x \<cdot>\<^sub>2 y \<cdot>\<^sub>2 \<one>\<^sub>2 = prod H (prod H x y) (one H)" and
1.196 + "x \<cdot> \<one>\<^sub>2 = prod G x (one H)" by (rule refl)+
1.197 +
1.198 +text {*
1.199 + Note that the trivial statements above need to be given as a
1.200 + simultaneous goal in order to have type-inference make the implicit
1.201 + typing of structures @{text G} and @{text H} agree.
1.202 +*}
1.203
1.204 end