2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Markus Wenzel, LMU Muenchen |
3 Author: Markus Wenzel, LMU Muenchen |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
5 *) |
5 *) |
6 |
6 |
7 header {* Locales and simple mathematical structures *} |
7 header {* Basic use of locales *} |
8 |
8 |
9 theory Locales = Main: |
9 theory Locales = Main: |
|
10 |
|
11 text {* |
|
12 The inevitable group theory examples formulated with locales. |
|
13 *} |
|
14 |
|
15 |
|
16 subsection {* Local contexts as mathematical structures *} |
10 |
17 |
11 text_raw {* |
18 text_raw {* |
12 \newcommand{\isasyminv}{\isasyminverse} |
19 \newcommand{\isasyminv}{\isasyminverse} |
13 \newcommand{\isasymone}{\isamath{1}} |
20 \newcommand{\isasymone}{\isamath{1}} |
14 *} |
|
15 |
|
16 |
|
17 subsection {* Groups *} |
|
18 |
|
19 text {* |
|
20 Locales version of the inevitable group example. |
|
21 *} |
21 *} |
22 |
22 |
23 locale group = |
23 locale group = |
24 fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<cdot>" 70) |
24 fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<cdot>" 70) |
25 and inv :: "'a \<Rightarrow> 'a" ("(_\<inv>)" [1000] 999) |
25 and inv :: "'a \<Rightarrow> 'a" ("(_\<inv>)" [1000] 999) |
117 also have "\<dots> = \<one> \<cdot> y" by (simp only: right_inv) |
117 also have "\<dots> = \<one> \<cdot> y" by (simp only: right_inv) |
118 also have "\<dots> = y" by (simp only: left_one) |
118 also have "\<dots> = y" by (simp only: left_one) |
119 finally show ?thesis . |
119 finally show ?thesis . |
120 qed |
120 qed |
121 |
121 |
|
122 |
|
123 subsection {* Referencing structures implicitly *} |
|
124 |
|
125 record 'a semigroup = |
|
126 prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
|
127 |
|
128 syntax |
|
129 "_prod1" :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<odot>" 70) |
|
130 "_prod2" :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<odot>\<^sub>2" 70) |
|
131 "_prod3" :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<odot>\<^sub>3" 70) |
|
132 translations |
|
133 "x \<odot> y" \<rightleftharpoons> "(\<struct>prod) x y" |
|
134 "x \<odot>\<^sub>2 y" \<rightleftharpoons> "(\<struct>\<struct>prod) x y" |
|
135 "x \<odot>\<^sub>3 y" \<rightleftharpoons> "(\<struct>\<struct>\<struct>prod) x y" |
|
136 |
|
137 lemma |
|
138 (fixes S :: "'a semigroup" (structure) |
|
139 and T :: "'a semigroup" (structure) |
|
140 and U :: "'a semigroup" (structure)) |
|
141 "prod S a b = a \<odot> b" .. |
|
142 |
|
143 lemma |
|
144 (fixes S :: "'a semigroup" (structure) |
|
145 and T :: "'a semigroup" (structure) |
|
146 and U :: "'a semigroup" (structure)) |
|
147 "prod T a b = a \<odot>\<^sub>2 b" .. |
|
148 |
|
149 lemma |
|
150 (fixes S :: "'a semigroup" (structure) |
|
151 and T :: "'a semigroup" (structure) |
|
152 and U :: "'a semigroup" (structure)) |
|
153 "prod U a b = a \<odot>\<^sub>3 b" .. |
|
154 |
122 end |
155 end |