summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Thu, 08 Nov 2001 00:26:06 +0100 | |

changeset 12099 | 8504c948fae2 |

parent 12098 | 784fe681ba26 |

child 12100 | bb10ac677955 |

more explanations on advanced syntax;

--- 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