summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/ex/Locales.thy

author | wenzelm |

Tue, 04 Dec 2001 02:01:49 +0100 | |

changeset 12356 | ce0961b1f536 |

parent 12105 | 1e4451999200 |

child 12507 | cc36d5da9bc0 |

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

removed \newcommand{\isasymone};

(* Title: HOL/ex/Locales.thy ID: $Id$ Author: Markus Wenzel, LMU Muenchen License: GPL (GNU GENERAL PUBLIC LICENSE) *) header {* Basic use of locales in Isabelle/Isar *} theory Locales = Main: text {* Locales provide a mechanism for encapsulating local contexts. The original version due to Florian Kamm\"uller \cite{Kamm-et-al:1999} refers directly to the raw meta-logic of Isabelle. The present version for Isabelle/Isar \cite{Wenzel:1999,Wenzel:2001:isar-ref,Wenzel:2001:Thesis} builds on top of the rich infrastructure of proof contexts instead; this also covers essential extra-logical concepts like term abbreviations or local theorem attributes (e.g.\ declarations of simplification rules). Subsequently, we demonstrate basic use of locales to model mathematical structures (by the inevitable group theory example). *} text_raw {* \newcommand{\isasyminv}{\isasyminverse} \newcommand{\isasymIN}{\isatext{\isakeyword{in}}} *} subsection {* Local contexts as mathematical structures *} text {* The following definitions of @{text group} and @{text abelian_group} merely encapsulate local parameters (with private syntax) and assumptions; local definitions may be given as well, but are not shown here. *} locale group = fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<cdot>" 70) and inv :: "'a \<Rightarrow> 'a" ("(_\<inv>)" [1000] 999) and one :: 'a ("\<one>") 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" 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 - 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) 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 Apart from the named context we may also refer to further context elements (parameters, assumptions, etc.) in a casual manner; these are discharged when the proof is finished. *} theorem (in group) (assumes eq: "e \<cdot> x = x") one_equality: "\<one> = e" proof - have "\<one> = x \<cdot> x\<inv>" by (simp only: right_inv) also have "\<dots> = (e \<cdot> x) \<cdot> x\<inv>" by (simp only: eq) also have "\<dots> = e \<cdot> (x \<cdot> x\<inv>)" by (simp only: assoc) also have "\<dots> = e \<cdot> \<one>" by (simp only: right_inv) also have "\<dots> = e" by (simp only: right_one) finally show ?thesis . qed theorem (in group) (assumes eq: "x' \<cdot> x = \<one>") inv_equality: "x\<inv> = x'" proof - have "x\<inv> = \<one> \<cdot> x\<inv>" by (simp only: left_one) also have "\<dots> = (x' \<cdot> x) \<cdot> x\<inv>" by (simp only: eq) also have "\<dots> = x' \<cdot> (x \<cdot> x\<inv>)" by (simp only: assoc) also have "\<dots> = x' \<cdot> \<one>" by (simp only: right_inv) also have "\<dots> = x'" by (simp only: right_one) finally show ?thesis . qed theorem (in group) inv_prod: "(x \<cdot> y)\<inv> = y\<inv> \<cdot> x\<inv>" proof (rule inv_equality) show "(y\<inv> \<cdot> x\<inv>) \<cdot> (x \<cdot> y) = \<one>" proof - have "(y\<inv> \<cdot> x\<inv>) \<cdot> (x \<cdot> y) = (y\<inv> \<cdot> (x\<inv> \<cdot> x)) \<cdot> y" by (simp only: assoc) also have "\<dots> = (y\<inv> \<cdot> \<one>) \<cdot> y" by (simp only: left_inv) also have "\<dots> = y\<inv> \<cdot> y" by (simp only: right_one) also have "\<dots> = \<one>" by (simp only: left_inv) finally show ?thesis . qed qed text {* \medskip Established results are automatically propagated through the hierarchy of locales. Below we establish a trivial fact in commutative groups, while referring both to theorems of @{text group} and the additional assumption of @{text abelian_group}. *} theorem (in abelian_group) inv_prod': "(x \<cdot> y)\<inv> = x\<inv> \<cdot> y\<inv>" proof - have "(x \<cdot> y)\<inv> = y\<inv> \<cdot> x\<inv>" by (rule inv_prod) also have "\<dots> = x\<inv> \<cdot> y\<inv>" by (rule commute) finally show ?thesis . qed text {* \medskip Some further properties of inversion in general group theory follow. *} theorem (in group) inv_inv: "(x\<inv>)\<inv> = x" proof (rule inv_equality) show "x \<cdot> x\<inv> = \<one>" by (simp only: right_inv) qed theorem (in group) (assumes eq: "x\<inv> = y\<inv>") inv_inject: "x = y" proof - have "x = x \<cdot> \<one>" by (simp only: right_one) also have "\<dots> = x \<cdot> (y\<inv> \<cdot> y)" by (simp only: left_inv) also have "\<dots> = x \<cdot> (x\<inv> \<cdot> y)" by (simp only: eq) also have "\<dots> = (x \<cdot> x\<inv>) \<cdot> y" by (simp only: assoc) also have "\<dots> = \<one> \<cdot> y" by (simp only: right_inv) also have "\<dots> = y" by (simp only: left_one) 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). 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 {* Explicit structures referenced implicitly *} 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. See \cite{Naraschewski-Wenzel:1998,Nipkow-et-al:2001:HOL} on (extensible) record types in Isabelle/HOL. *} 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 "_prod" :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<cdot>" 70) "_inv" :: "'a \<Rightarrow> 'a" ("(_\<inv>)" [1000] 999) "_one" :: 'a ("\<one>") translations "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 a ``\isakeyword{structure}''. In its context the dummy ``@{text \<struct>}'' refers to this very parameter, independently of the present naming. *} 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 {* 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 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 several renamed versions of the @{text group_struct} locale above. *} lemma (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 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. *} end