summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/ex/Locales.thy

author | haftmann |

Wed Mar 12 19:38:14 2008 +0100 (2008-03-12) | |

changeset 26265 | 4b63b9e9b10d |

parent 19931 | fb32b43e7f80 |

permissions | -rw-r--r-- |

separated Random.thy from Quickcheck.thy

1 (* Title: HOL/ex/Locales.thy

2 ID: $Id$

3 Author: Markus Wenzel, LMU München

4 *)

6 header {* Using locales in Isabelle/Isar -- outdated version! *}

8 theory Locales imports Main begin

10 text_raw {*

11 \newcommand{\isasyminv}{\isasyminverse}

12 \newcommand{\isasymIN}{\isatext{\isakeyword{in}}}

13 \newcommand{\isasymINCLUDES}{\isatext{\isakeyword{includes}}}

14 *}

16 subsection {* Overview *}

18 text {*

19 Locales provide a mechanism for encapsulating local contexts. The

20 original version due to Florian Kammüller \cite{Kamm-et-al:1999}

21 refers directly to Isabelle's meta-logic \cite{Paulson:1989}, which

22 is minimal higher-order logic with connectives @{text "\<And>"}

23 (universal quantification), @{text "\<Longrightarrow>"} (implication), and @{text

24 "\<equiv>"} (equality).

26 From this perspective, a locale is essentially a meta-level

27 predicate, together with some infrastructure to manage the

28 abstracted parameters (@{text "\<And>"}), assumptions (@{text "\<Longrightarrow>"}), and

29 definitions for (@{text "\<equiv>"}) in a reasonable way during the proof

30 process. This simple predicate view also provides a solid

31 semantical basis for our specification concepts to be developed

32 later.

34 \medskip The present version of locales for Isabelle/Isar builds on

35 top of the rich infrastructure of proof contexts

36 \cite{Wenzel:1999,Wenzel:2001:isar-ref,Wenzel:2001:Thesis}, which in

37 turn is based on the same meta-logic. Thus we achieve a tight

38 integration with Isar proof texts, and a slightly more abstract view

39 of the underlying logical concepts. An Isar proof context

40 encapsulates certain language elements that correspond to @{text

41 "\<And>/\<Longrightarrow>/\<equiv>"} at the level of structure proof texts. Moreover, there are

42 extra-logical concepts like term abbreviations or local theorem

43 attributes (declarations of simplification rules etc.) that are

44 useful in applications (e.g.\ consider standard simplification rules

45 declared in a group context).

47 Locales also support concrete syntax, i.e.\ a localized version of

48 the existing concept of mixfix annotations of Isabelle

49 \cite{Paulson:1994:Isabelle}. Furthermore, there is a separate

50 concept of ``implicit structures'' that admits to refer to

51 particular locale parameters in a casual manner (basically a

52 simplified version of the idea of ``anti-quotations'', or

53 generalized de-Bruijn indexes as demonstrated elsewhere

54 \cite[\S13--14]{Wenzel:2001:Isar-examples}).

56 Implicit structures work particular well together with extensible

57 records in HOL \cite{Naraschewski-Wenzel:1998} (without the

58 ``object-oriented'' features discussed there as well). Thus we

59 achieve a specification technique where record type schemes

60 represent polymorphic signatures of mathematical structures, and

61 actual locales describe the corresponding logical properties.

62 Semantically speaking, such abstract mathematical structures are

63 just predicates over record types. Due to type inference of

64 simply-typed records (which subsumes structural subtyping) we arrive

65 at succinct specification texts --- ``signature morphisms''

66 degenerate to implicit type-instantiations. Additional eye-candy is

67 provided by the separate concept of ``indexed concrete syntax'' used

68 for record selectors, so we get close to informal mathematical

69 notation.

71 \medskip Operations for building up locale contexts from existing

72 ones include \emph{merge} (disjoint union) and \emph{rename} (of

73 term parameters only, types are inferred automatically). Here we

74 draw from existing traditions of algebraic specification languages.

75 A structured specification corresponds to a directed acyclic graph

76 of potentially renamed nodes (due to distributivity renames may

77 pushed inside of merges). The result is a ``flattened'' list of

78 primitive context elements in canonical order (corresponding to

79 left-to-right reading of merges, while suppressing duplicates).

81 \medskip The present version of Isabelle/Isar locales still lacks

82 some important specification concepts.

84 \begin{itemize}

86 \item Separate language elements for \emph{instantiation} of

87 locales.

89 Currently users may simulate this to some extend by having primitive

90 Isabelle/Isar operations (@{text of} for substitution and @{text OF}

91 for composition, \cite{Wenzel:2001:isar-ref}) act on the

92 automatically exported results stemming from different contexts.

94 \item Interpretation of locales (think of ``views'', ``functors''

95 etc.).

97 In principle one could directly work with functions over structures

98 (extensible records), and predicates being derived from locale

99 definitions.

101 \end{itemize}

103 \medskip Subsequently, we demonstrate some readily available

104 concepts of Isabelle/Isar locales by some simple examples of

105 abstract algebraic reasoning.

106 *}

109 subsection {* Local contexts as mathematical structures *}

111 text {*

112 The following definitions of @{text group_context} and @{text

113 abelian_group_context} merely encapsulate local parameters (with

114 private syntax) and assumptions; local definitions of derived

115 concepts could be given, too, but are unused below.

116 *}

118 locale group_context =

119 fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<cdot>" 70)

120 and inv :: "'a \<Rightarrow> 'a" ("(_\<inv>)" [1000] 999)

121 and one :: 'a ("\<one>")

122 assumes assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"

123 and left_inv: "x\<inv> \<cdot> x = \<one>"

124 and left_one: "\<one> \<cdot> x = x"

126 locale abelian_group_context = group_context +

127 assumes commute: "x \<cdot> y = y \<cdot> x"

129 text {*

130 \medskip We may now prove theorems within a local context, just by

131 including a directive ``@{text "(\<IN> name)"}'' in the goal

132 specification. The final result will be stored within the named

133 locale, still holding the context; a second copy is exported to the

134 enclosing theory context (with qualified name).

135 *}

137 theorem (in group_context)

138 right_inv: "x \<cdot> x\<inv> = \<one>"

139 proof -

140 have "x \<cdot> x\<inv> = \<one> \<cdot> (x \<cdot> x\<inv>)" by (simp only: left_one)

141 also have "\<dots> = \<one> \<cdot> x \<cdot> x\<inv>" by (simp only: assoc)

142 also have "\<dots> = (x\<inv>)\<inv> \<cdot> x\<inv> \<cdot> x \<cdot> x\<inv>" by (simp only: left_inv)

143 also have "\<dots> = (x\<inv>)\<inv> \<cdot> (x\<inv> \<cdot> x) \<cdot> x\<inv>" by (simp only: assoc)

144 also have "\<dots> = (x\<inv>)\<inv> \<cdot> \<one> \<cdot> x\<inv>" by (simp only: left_inv)

145 also have "\<dots> = (x\<inv>)\<inv> \<cdot> (\<one> \<cdot> x\<inv>)" by (simp only: assoc)

146 also have "\<dots> = (x\<inv>)\<inv> \<cdot> x\<inv>" by (simp only: left_one)

147 also have "\<dots> = \<one>" by (simp only: left_inv)

148 finally show ?thesis .

149 qed

151 theorem (in group_context)

152 right_one: "x \<cdot> \<one> = x"

153 proof -

154 have "x \<cdot> \<one> = x \<cdot> (x\<inv> \<cdot> x)" by (simp only: left_inv)

155 also have "\<dots> = x \<cdot> x\<inv> \<cdot> x" by (simp only: assoc)

156 also have "\<dots> = \<one> \<cdot> x" by (simp only: right_inv)

157 also have "\<dots> = x" by (simp only: left_one)

158 finally show ?thesis .

159 qed

161 text {*

162 Facts like @{text right_one} are available @{text group_context} as

163 stated above. The exported version looses the additional

164 infrastructure of Isar proof contexts (syntax etc.) retaining only

165 the pure logical content: @{thm [source] group_context.right_one}

166 becomes @{thm group_context.right_one} (in Isabelle outermost @{text

167 \<And>} quantification is replaced by schematic variables).

169 \medskip Apart from a named locale we may also refer to further

170 context elements (parameters, assumptions, etc.) in an ad-hoc

171 fashion, just for this particular statement. In the result (local

172 or global), any additional elements are discharged as usual.

173 *}

175 theorem (in group_context)

176 assumes eq: "e \<cdot> x = x"

177 shows one_equality: "\<one> = e"

178 proof -

179 have "\<one> = x \<cdot> x\<inv>" by (simp only: right_inv)

180 also have "\<dots> = (e \<cdot> x) \<cdot> x\<inv>" by (simp only: eq)

181 also have "\<dots> = e \<cdot> (x \<cdot> x\<inv>)" by (simp only: assoc)

182 also have "\<dots> = e \<cdot> \<one>" by (simp only: right_inv)

183 also have "\<dots> = e" by (simp only: right_one)

184 finally show ?thesis .

185 qed

187 theorem (in group_context)

188 assumes eq: "x' \<cdot> x = \<one>"

189 shows inv_equality: "x\<inv> = x'"

190 proof -

191 have "x\<inv> = \<one> \<cdot> x\<inv>" by (simp only: left_one)

192 also have "\<dots> = (x' \<cdot> x) \<cdot> x\<inv>" by (simp only: eq)

193 also have "\<dots> = x' \<cdot> (x \<cdot> x\<inv>)" by (simp only: assoc)

194 also have "\<dots> = x' \<cdot> \<one>" by (simp only: right_inv)

195 also have "\<dots> = x'" by (simp only: right_one)

196 finally show ?thesis .

197 qed

199 theorem (in group_context)

200 inv_prod: "(x \<cdot> y)\<inv> = y\<inv> \<cdot> x\<inv>"

201 proof (rule inv_equality)

202 show "(y\<inv> \<cdot> x\<inv>) \<cdot> (x \<cdot> y) = \<one>"

203 proof -

204 have "(y\<inv> \<cdot> x\<inv>) \<cdot> (x \<cdot> y) = (y\<inv> \<cdot> (x\<inv> \<cdot> x)) \<cdot> y" by (simp only: assoc)

205 also have "\<dots> = (y\<inv> \<cdot> \<one>) \<cdot> y" by (simp only: left_inv)

206 also have "\<dots> = y\<inv> \<cdot> y" by (simp only: right_one)

207 also have "\<dots> = \<one>" by (simp only: left_inv)

208 finally show ?thesis .

209 qed

210 qed

212 text {*

213 \medskip Established results are automatically propagated through

214 the hierarchy of locales. Below we establish a trivial fact in

215 commutative groups, while referring both to theorems of @{text

216 group} and the additional assumption of @{text abelian_group}.

217 *}

219 theorem (in abelian_group_context)

220 inv_prod': "(x \<cdot> y)\<inv> = x\<inv> \<cdot> y\<inv>"

221 proof -

222 have "(x \<cdot> y)\<inv> = y\<inv> \<cdot> x\<inv>" by (rule inv_prod)

223 also have "\<dots> = x\<inv> \<cdot> y\<inv>" by (rule commute)

224 finally show ?thesis .

225 qed

227 text {*

228 We see that the initial import of @{text group} within the

229 definition of @{text abelian_group} is actually evaluated

230 dynamically. Thus any results in @{text group} are made available

231 to the derived context of @{text abelian_group} as well. Note that

232 the alternative context element @{text \<INCLUDES>} would import

233 existing locales in a static fashion, without participating in

234 further facts emerging later on.

236 \medskip Some more properties of inversion in general group theory

237 follow.

238 *}

240 theorem (in group_context)

241 inv_inv: "(x\<inv>)\<inv> = x"

242 proof (rule inv_equality)

243 show "x \<cdot> x\<inv> = \<one>" by (simp only: right_inv)

244 qed

246 theorem (in group_context)

247 assumes eq: "x\<inv> = y\<inv>"

248 shows inv_inject: "x = y"

249 proof -

250 have "x = x \<cdot> \<one>" by (simp only: right_one)

251 also have "\<dots> = x \<cdot> (y\<inv> \<cdot> y)" by (simp only: left_inv)

252 also have "\<dots> = x \<cdot> (x\<inv> \<cdot> y)" by (simp only: eq)

253 also have "\<dots> = (x \<cdot> x\<inv>) \<cdot> y" by (simp only: assoc)

254 also have "\<dots> = \<one> \<cdot> y" by (simp only: right_inv)

255 also have "\<dots> = y" by (simp only: left_one)

256 finally show ?thesis .

257 qed

259 text {*

260 \bigskip We see that this representation of structures as local

261 contexts is rather light-weight and convenient to use for abstract

262 reasoning. Here the ``components'' (the group operations) have been

263 exhibited directly as context parameters; logically this corresponds

264 to a curried predicate definition:

266 @{thm [display] group_context_def [no_vars]}

268 The corresponding introduction rule is as follows:

270 @{thm [display, mode = no_brackets] group_context.intro [no_vars]}

272 Occasionally, this ``externalized'' version of the informal idea of

273 classes of tuple structures may cause some inconveniences,

274 especially in meta-theoretical studies (involving functors from

275 groups to groups, for example).

277 Another minor drawback of the naive approach above is that concrete

278 syntax will get lost on any kind of operation on the locale itself

279 (such as renaming, copying, or instantiation). Whenever the

280 particular terminology of local parameters is affected the

281 associated syntax would have to be changed as well, which is hard to

282 achieve formally.

283 *}

286 subsection {* Explicit structures referenced implicitly *}

288 text {*

289 We introduce the same hierarchy of basic group structures as above,

290 this time using extensible record types for the signature part,

291 together with concrete syntax for selector functions.

292 *}

294 record 'a semigroup =

295 prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<cdot>\<index>" 70)

297 record 'a group = "'a semigroup" +

298 inv :: "'a \<Rightarrow> 'a" ("(_\<inv>\<index>)" [1000] 999)

299 one :: 'a ("\<one>\<index>")

301 text {*

302 The mixfix annotations above include a special ``structure index

303 indicator'' @{text \<index>} that makes grammar productions dependent on

304 certain parameters that have been declared as ``structure'' in a

305 locale context later on. Thus we achieve casual notation as

306 encountered in informal mathematics, e.g.\ @{text "x \<cdot> y"} for

307 @{text "prod G x y"}.

309 \medskip The following locale definitions introduce operate on a

310 single parameter declared as ``\isakeyword{structure}''. Type

311 inference takes care to fill in the appropriate record type schemes

312 internally.

313 *}

315 locale semigroup =

316 fixes S (structure)

317 assumes assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"

319 locale group = semigroup G +

320 assumes left_inv: "x\<inv> \<cdot> x = \<one>"

321 and left_one: "\<one> \<cdot> x = x"

323 declare semigroup.intro [intro?]

324 group.intro [intro?] group_axioms.intro [intro?]

326 text {*

327 Note that we prefer to call the @{text group} record structure

328 @{text G} rather than @{text S} inherited from @{text semigroup}.

329 This does not affect our concrete syntax, which is only dependent on

330 the \emph{positional} arrangements of currently active structures

331 (actually only one above), rather than names. In fact, these

332 parameter names rarely occur in the term language at all (due to the

333 ``indexed syntax'' facility of Isabelle). On the other hand, names

334 of locale facts will get qualified accordingly, e.g. @{text S.assoc}

335 versus @{text G.assoc}.

337 \medskip We may now proceed to prove results within @{text group}

338 just as before for @{text group}. The subsequent proof texts are

339 exactly the same as despite the more advanced internal arrangement.

340 *}

342 theorem (in group)

343 right_inv: "x \<cdot> x\<inv> = \<one>"

344 proof -

345 have "x \<cdot> x\<inv> = \<one> \<cdot> (x \<cdot> x\<inv>)" by (simp only: left_one)

346 also have "\<dots> = \<one> \<cdot> x \<cdot> x\<inv>" by (simp only: assoc)

347 also have "\<dots> = (x\<inv>)\<inv> \<cdot> x\<inv> \<cdot> x \<cdot> x\<inv>" by (simp only: left_inv)

348 also have "\<dots> = (x\<inv>)\<inv> \<cdot> (x\<inv> \<cdot> x) \<cdot> x\<inv>" by (simp only: assoc)

349 also have "\<dots> = (x\<inv>)\<inv> \<cdot> \<one> \<cdot> x\<inv>" by (simp only: left_inv)

350 also have "\<dots> = (x\<inv>)\<inv> \<cdot> (\<one> \<cdot> x\<inv>)" by (simp only: assoc)

351 also have "\<dots> = (x\<inv>)\<inv> \<cdot> x\<inv>" by (simp only: left_one)

352 also have "\<dots> = \<one>" by (simp only: left_inv)

353 finally show ?thesis .

354 qed

356 theorem (in group)

357 right_one: "x \<cdot> \<one> = x"

358 proof -

359 have "x \<cdot> \<one> = x \<cdot> (x\<inv> \<cdot> x)" by (simp only: left_inv)

360 also have "\<dots> = x \<cdot> x\<inv> \<cdot> x" by (simp only: assoc)

361 also have "\<dots> = \<one> \<cdot> x" by (simp only: right_inv)

362 also have "\<dots> = x" by (simp only: left_one)

363 finally show ?thesis .

364 qed

366 text {*

367 \medskip Several implicit structures may be active at the same time.

368 The concrete syntax facility for locales actually maintains indexed

369 structures that may be references implicitly --- via mixfix

370 annotations that have been decorated by an ``index argument''

371 (@{text \<index>}).

373 The following synthetic example demonstrates how to refer to several

374 structures of type @{text group} succinctly. We work with two

375 versions of the @{text group} locale above.

376 *}

378 lemma

379 includes group G

380 includes group H

381 shows "x \<cdot> y \<cdot> \<one> = prod G (prod G x y) (one G)"

382 and "x \<cdot>\<^sub>2 y \<cdot>\<^sub>2 \<one>\<^sub>2 = prod H (prod H x y) (one H)"

383 and "x \<cdot> \<one>\<^sub>2 = prod G x (one H)"

384 by (rule refl)+

386 text {*

387 Note that the trivial statements above need to be given as a

388 simultaneous goal in order to have type-inference make the implicit

389 typing of structures @{text G} and @{text H} agree.

390 *}

393 subsection {* Simple meta-theory of structures *}

395 text {*

396 The packaging of the logical specification as a predicate and the

397 syntactic structure as a record type provides a reasonable starting

398 point for simple meta-theoretic studies of mathematical structures.

399 This includes operations on structures (also known as ``functors''),

400 and statements about such constructions.

402 For example, the direct product of semigroups works as follows.

403 *}

405 constdefs

406 semigroup_product :: "'a semigroup \<Rightarrow> 'b semigroup \<Rightarrow> ('a \<times> 'b) semigroup"

407 "semigroup_product S T \<equiv>

408 \<lparr>prod = \<lambda>p q. (prod S (fst p) (fst q), prod T (snd p) (snd q))\<rparr>"

410 lemma semigroup_product [intro]:

411 assumes S: "semigroup S"

412 and T: "semigroup T"

413 shows "semigroup (semigroup_product S T)"

414 proof

415 fix p q r :: "'a \<times> 'b"

416 have "prod S (prod S (fst p) (fst q)) (fst r) =

417 prod S (fst p) (prod S (fst q) (fst r))"

418 by (rule semigroup.assoc [OF S])

419 moreover have "prod T (prod T (snd p) (snd q)) (snd r) =

420 prod T (snd p) (prod T (snd q) (snd r))"

421 by (rule semigroup.assoc [OF T])

422 ultimately

423 show "prod (semigroup_product S T) (prod (semigroup_product S T) p q) r =

424 prod (semigroup_product S T) p (prod (semigroup_product S T) q r)"

425 by (simp add: semigroup_product_def)

426 qed

428 text {*

429 The above proof is fairly easy, but obscured by the lack of concrete

430 syntax. In fact, we didn't make use of the infrastructure of

431 locales, apart from the raw predicate definition of @{text

432 semigroup}.

434 The alternative version below uses local context expressions to

435 achieve a succinct proof body. The resulting statement is exactly

436 the same as before, even though its specification is a bit more

437 complex.

438 *}

440 lemma

441 includes semigroup S + semigroup T

442 fixes U (structure)

443 defines "U \<equiv> semigroup_product S T"

444 shows "semigroup U"

445 proof

446 fix p q r :: "'a \<times> 'b"

447 have "(fst p \<cdot>\<^sub>1 fst q) \<cdot>\<^sub>1 fst r = fst p \<cdot>\<^sub>1 (fst q \<cdot>\<^sub>1 fst r)"

448 by (rule S.assoc)

449 moreover have "(snd p \<cdot>\<^sub>2 snd q) \<cdot>\<^sub>2 snd r = snd p \<cdot>\<^sub>2 (snd q \<cdot>\<^sub>2 snd r)"

450 by (rule T.assoc)

451 ultimately show "(p \<cdot>\<^sub>3 q) \<cdot>\<^sub>3 r = p \<cdot>\<^sub>3 (q \<cdot>\<^sub>3 r)"

452 by (simp add: U_def semigroup_product_def semigroup.defs)

453 qed

455 text {*

456 Direct products of group structures may be defined in a similar

457 manner, taking two further operations into account. Subsequently,

458 we use high-level record operations to convert between different

459 signature types explicitly; see also

460 \cite[\S8.3]{isabelle-hol-book}.

461 *}

463 constdefs

464 group_product :: "'a group \<Rightarrow> 'b group \<Rightarrow> ('a \<times> 'b) group"

465 "group_product G H \<equiv>

466 semigroup.extend

467 (semigroup_product (semigroup.truncate G) (semigroup.truncate H))

468 (group.fields (\<lambda>p. (inv G (fst p), inv H (snd p))) (one G, one H))"

470 lemma group_product_aux:

471 includes group G + group H

472 fixes I (structure)

473 defines "I \<equiv> group_product G H"

474 shows "group I"

475 proof

476 show "semigroup I"

477 proof -

478 let ?G' = "semigroup.truncate G" and ?H' = "semigroup.truncate H"

479 have "prod (semigroup_product ?G' ?H') = prod I"

480 by (simp add: I_def group_product_def group.defs

481 semigroup_product_def semigroup.defs)

482 moreover

483 have "semigroup ?G'" and "semigroup ?H'"

484 using prems by (simp_all add: semigroup_def semigroup.defs G.assoc H.assoc)

485 then have "semigroup (semigroup_product ?G' ?H')" ..

486 ultimately show ?thesis by (simp add: I_def semigroup_def)

487 qed

488 show "group_axioms I"

489 proof

490 fix p :: "'a \<times> 'b"

491 have "(fst p)\<inv>\<^sub>1 \<cdot>\<^sub>1 fst p = \<one>\<^sub>1"

492 by (rule G.left_inv)

493 moreover have "(snd p)\<inv>\<^sub>2 \<cdot>\<^sub>2 snd p = \<one>\<^sub>2"

494 by (rule H.left_inv)

495 ultimately show "p\<inv>\<^sub>3 \<cdot>\<^sub>3 p = \<one>\<^sub>3"

496 by (simp add: I_def group_product_def group.defs

497 semigroup_product_def semigroup.defs)

498 have "\<one>\<^sub>1 \<cdot>\<^sub>1 fst p = fst p" by (rule G.left_one)

499 moreover have "\<one>\<^sub>2 \<cdot>\<^sub>2 snd p = snd p" by (rule H.left_one)

500 ultimately show "\<one>\<^sub>3 \<cdot>\<^sub>3 p = p"

501 by (simp add: I_def group_product_def group.defs

502 semigroup_product_def semigroup.defs)

503 qed

504 qed

506 theorem group_product: "group G \<Longrightarrow> group H \<Longrightarrow> group (group_product G H)"

507 by (rule group_product_aux) (assumption | rule group.axioms)+

509 end