# HG changeset patch # User ballarin # Date 1224169640 -7200 # Node ID 2ededdda7294985c1cc50bc385782034c1c7e07f # Parent d8fdecb1ea004cd68d6405e657c12dd468727b53 Removed outdated locales tutorial. diff -r d8fdecb1ea00 -r 2ededdda7294 src/HOL/ex/Locales.thy --- a/src/HOL/ex/Locales.thy Thu Oct 16 08:51:05 2008 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,509 +0,0 @@ -(* Title: HOL/ex/Locales.thy - ID: $Id$ - Author: Markus Wenzel, LMU München -*) - -header {* Using locales in Isabelle/Isar -- outdated version! *} - -theory Locales imports Main begin - -text_raw {* - \newcommand{\isasyminv}{\isasyminverse} - \newcommand{\isasymIN}{\isatext{\isakeyword{in}}} - \newcommand{\isasymINCLUDES}{\isatext{\isakeyword{includes}}} -*} - -subsection {* Overview *} - -text {* - Locales provide a mechanism for encapsulating local contexts. The - original version due to Florian Kammüller \cite{Kamm-et-al:1999} - refers directly to Isabelle's meta-logic \cite{Paulson:1989}, which - is minimal higher-order logic with connectives @{text "\"} - (universal quantification), @{text "\"} (implication), and @{text - "\"} (equality). - - From this perspective, a locale is essentially a meta-level - predicate, together with some infrastructure to manage the - abstracted parameters (@{text "\"}), assumptions (@{text "\"}), and - definitions for (@{text "\"}) in a reasonable way during the proof - process. This simple predicate view also provides a solid - semantical basis for our specification concepts to be developed - later. - - \medskip The present version of locales for Isabelle/Isar builds on - top of the rich infrastructure of proof contexts - \cite{Wenzel:1999,Wenzel:2001:isar-ref,Wenzel:2001:Thesis}, which in - turn is based on the same meta-logic. Thus we achieve a tight - integration with Isar proof texts, and a slightly more abstract view - of the underlying logical concepts. An Isar proof context - encapsulates certain language elements that correspond to @{text - "\/\/\"} at the level of structure proof texts. Moreover, there are - extra-logical concepts like term abbreviations or local theorem - attributes (declarations of simplification rules etc.) that are - useful in applications (e.g.\ consider standard simplification rules - declared in a group context). - - Locales also support concrete syntax, i.e.\ a localized version of - the existing concept of mixfix annotations of Isabelle - \cite{Paulson:1994:Isabelle}. Furthermore, there is a separate - concept of ``implicit structures'' that admits to refer to - particular locale parameters in a casual manner (basically a - simplified version of the idea of ``anti-quotations'', or - generalized de-Bruijn indexes as demonstrated elsewhere - \cite[\S13--14]{Wenzel:2001:Isar-examples}). - - Implicit structures work particular well together with extensible - records in HOL \cite{Naraschewski-Wenzel:1998} (without the - ``object-oriented'' features discussed there as well). Thus we - achieve a specification technique where record type schemes - represent polymorphic signatures of mathematical structures, and - actual locales describe the corresponding logical properties. - Semantically speaking, such abstract mathematical structures are - just predicates over record types. Due to type inference of - simply-typed records (which subsumes structural subtyping) we arrive - at succinct specification texts --- ``signature morphisms'' - degenerate to implicit type-instantiations. Additional eye-candy is - provided by the separate concept of ``indexed concrete syntax'' used - for record selectors, so we get close to informal mathematical - notation. - - \medskip Operations for building up locale contexts from existing - ones include \emph{merge} (disjoint union) and \emph{rename} (of - term parameters only, types are inferred automatically). Here we - draw from existing traditions of algebraic specification languages. - A structured specification corresponds to a directed acyclic graph - of potentially renamed nodes (due to distributivity renames may - pushed inside of merges). The result is a ``flattened'' list of - primitive context elements in canonical order (corresponding to - left-to-right reading of merges, while suppressing duplicates). - - \medskip The present version of Isabelle/Isar locales still lacks - some important specification concepts. - - \begin{itemize} - - \item Separate language elements for \emph{instantiation} of - locales. - - Currently users may simulate this to some extend by having primitive - Isabelle/Isar operations (@{text of} for substitution and @{text OF} - for composition, \cite{Wenzel:2001:isar-ref}) act on the - automatically exported results stemming from different contexts. - - \item Interpretation of locales (think of ``views'', ``functors'' - etc.). - - In principle one could directly work with functions over structures - (extensible records), and predicates being derived from locale - definitions. - - \end{itemize} - - \medskip Subsequently, we demonstrate some readily available - concepts of Isabelle/Isar locales by some simple examples of - abstract algebraic reasoning. -*} - - -subsection {* Local contexts as mathematical structures *} - -text {* - The following definitions of @{text group_context} and @{text - abelian_group_context} merely encapsulate local parameters (with - private syntax) and assumptions; local definitions of derived - concepts could be given, too, but are unused below. -*} - -locale group_context = - fixes prod :: "'a \ 'a \ 'a" (infixl "\" 70) - and inv :: "'a \ 'a" ("(_\)" [1000] 999) - and one :: 'a ("\") - assumes assoc: "(x \ y) \ z = x \ (y \ z)" - and left_inv: "x\ \ x = \" - and left_one: "\ \ x = x" - -locale abelian_group_context = group_context + - assumes commute: "x \ y = y \ x" - -text {* - \medskip We may now prove theorems within a local context, just by - including a directive ``@{text "(\ name)"}'' in the goal - specification. The final result will be stored within the named - locale, still holding the context; a second copy is exported to the - enclosing theory context (with qualified name). -*} - -theorem (in group_context) - right_inv: "x \ x\ = \" -proof - - have "x \ x\ = \ \ (x \ x\)" by (simp only: left_one) - also have "\ = \ \ x \ x\" by (simp only: assoc) - also have "\ = (x\)\ \ x\ \ x \ x\" by (simp only: left_inv) - also have "\ = (x\)\ \ (x\ \ x) \ x\" by (simp only: assoc) - also have "\ = (x\)\ \ \ \ x\" by (simp only: left_inv) - also have "\ = (x\)\ \ (\ \ x\)" by (simp only: assoc) - also have "\ = (x\)\ \ x\" by (simp only: left_one) - also have "\ = \" by (simp only: left_inv) - finally show ?thesis . -qed - -theorem (in group_context) - right_one: "x \ \ = x" -proof - - have "x \ \ = x \ (x\ \ x)" by (simp only: left_inv) - also have "\ = x \ x\ \ x" by (simp only: assoc) - also have "\ = \ \ x" by (simp only: right_inv) - also have "\ = x" by (simp only: left_one) - finally show ?thesis . -qed - -text {* - Facts like @{text right_one} are available @{text group_context} as - stated above. The exported version looses the additional - infrastructure of Isar proof contexts (syntax etc.) retaining only - the pure logical content: @{thm [source] group_context.right_one} - becomes @{thm group_context.right_one} (in Isabelle outermost @{text - \} quantification is replaced by schematic variables). - - \medskip Apart from a named locale we may also refer to further - context elements (parameters, assumptions, etc.) in an ad-hoc - fashion, just for this particular statement. In the result (local - or global), any additional elements are discharged as usual. -*} - -theorem (in group_context) - assumes eq: "e \ x = x" - shows one_equality: "\ = e" -proof - - have "\ = x \ x\" by (simp only: right_inv) - also have "\ = (e \ x) \ x\" by (simp only: eq) - also have "\ = e \ (x \ x\)" by (simp only: assoc) - also have "\ = e \ \" by (simp only: right_inv) - also have "\ = e" by (simp only: right_one) - finally show ?thesis . -qed - -theorem (in group_context) - assumes eq: "x' \ x = \" - shows inv_equality: "x\ = x'" -proof - - have "x\ = \ \ x\" by (simp only: left_one) - also have "\ = (x' \ x) \ x\" by (simp only: eq) - also have "\ = x' \ (x \ x\)" by (simp only: assoc) - also have "\ = x' \ \" by (simp only: right_inv) - also have "\ = x'" by (simp only: right_one) - finally show ?thesis . -qed - -theorem (in group_context) - inv_prod: "(x \ y)\ = y\ \ x\" -proof (rule inv_equality) - show "(y\ \ x\) \ (x \ y) = \" - proof - - have "(y\ \ x\) \ (x \ y) = (y\ \ (x\ \ x)) \ y" by (simp only: assoc) - also have "\ = (y\ \ \) \ y" by (simp only: left_inv) - also have "\ = y\ \ y" by (simp only: right_one) - also have "\ = \" 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_context) - inv_prod': "(x \ y)\ = x\ \ y\" -proof - - have "(x \ y)\ = y\ \ x\" by (rule inv_prod) - also have "\ = x\ \ y\" by (rule commute) - finally show ?thesis . -qed - -text {* - We see that the initial import of @{text group} within the - definition of @{text abelian_group} is actually evaluated - dynamically. Thus any results in @{text group} are made available - to the derived context of @{text abelian_group} as well. Note that - the alternative context element @{text \} would import - existing locales in a static fashion, without participating in - further facts emerging later on. - - \medskip Some more properties of inversion in general group theory - follow. -*} - -theorem (in group_context) - inv_inv: "(x\)\ = x" -proof (rule inv_equality) - show "x \ x\ = \" by (simp only: right_inv) -qed - -theorem (in group_context) - assumes eq: "x\ = y\" - shows inv_inject: "x = y" -proof - - have "x = x \ \" by (simp only: right_one) - also have "\ = x \ (y\ \ y)" by (simp only: left_inv) - also have "\ = x \ (x\ \ y)" by (simp only: eq) - also have "\ = (x \ x\) \ y" by (simp only: assoc) - also have "\ = \ \ y" by (simp only: right_inv) - also have "\ = 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: - - @{thm [display] group_context_def [no_vars]} - - The corresponding introduction rule is as follows: - - @{thm [display, mode = no_brackets] group_context.intro [no_vars]} - - 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 minor 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 {* - We introduce the same hierarchy of basic group structures as above, - this time using extensible record types for the signature part, - together with concrete syntax for selector functions. -*} - -record 'a semigroup = - prod :: "'a \ 'a \ 'a" (infixl "\\" 70) - -record 'a group = "'a semigroup" + - inv :: "'a \ 'a" ("(_\\)" [1000] 999) - one :: 'a ("\\") - -text {* - The mixfix annotations above include a special ``structure index - indicator'' @{text \} that makes grammar productions dependent on - certain parameters that have been declared as ``structure'' in a - locale context later on. Thus we achieve casual notation as - encountered in informal mathematics, e.g.\ @{text "x \ y"} for - @{text "prod G x y"}. - - \medskip The following locale definitions introduce operate on a - single parameter declared as ``\isakeyword{structure}''. Type - inference takes care to fill in the appropriate record type schemes - internally. -*} - -locale semigroup = - fixes S (structure) - assumes assoc: "(x \ y) \ z = x \ (y \ z)" - -locale group = semigroup G + - assumes left_inv: "x\ \ x = \" - and left_one: "\ \ x = x" - -declare semigroup.intro [intro?] - group.intro [intro?] group_axioms.intro [intro?] - -text {* - Note that we prefer to call the @{text group} record structure - @{text G} rather than @{text S} inherited from @{text semigroup}. - This does not affect our concrete syntax, which is only dependent on - the \emph{positional} arrangements of currently active structures - (actually only one above), rather than names. In fact, these - parameter names rarely occur in the term language at all (due to the - ``indexed syntax'' facility of Isabelle). On the other hand, names - of locale facts will get qualified accordingly, e.g. @{text S.assoc} - versus @{text G.assoc}. - - \medskip We may now proceed to prove results within @{text group} - just as before for @{text group}. The subsequent proof texts are - exactly the same as despite the more advanced internal arrangement. -*} - -theorem (in group) - right_inv: "x \ x\ = \" -proof - - have "x \ x\ = \ \ (x \ x\)" by (simp only: left_one) - also have "\ = \ \ x \ x\" by (simp only: assoc) - also have "\ = (x\)\ \ x\ \ x \ x\" by (simp only: left_inv) - also have "\ = (x\)\ \ (x\ \ x) \ x\" by (simp only: assoc) - also have "\ = (x\)\ \ \ \ x\" by (simp only: left_inv) - also have "\ = (x\)\ \ (\ \ x\)" by (simp only: assoc) - also have "\ = (x\)\ \ x\" by (simp only: left_one) - also have "\ = \" by (simp only: left_inv) - finally show ?thesis . -qed - -theorem (in group) - right_one: "x \ \ = x" -proof - - have "x \ \ = x \ (x\ \ x)" by (simp only: left_inv) - also have "\ = x \ x\ \ x" by (simp only: assoc) - also have "\ = \ \ x" by (simp only: right_inv) - also have "\ = x" by (simp only: left_one) - finally show ?thesis . -qed - -text {* - \medskip Several implicit structures may be active at the same time. - The concrete syntax facility for locales actually maintains indexed - structures that may be references implicitly --- via mixfix - annotations that have been decorated by an ``index argument'' - (@{text \}). - - The following synthetic example demonstrates how to refer to several - structures of type @{text group} succinctly. We work with two - versions of the @{text group} locale above. -*} - -lemma - includes group G - includes group H - shows "x \ y \ \ = prod G (prod G x y) (one G)" - and "x \\<^sub>2 y \\<^sub>2 \\<^sub>2 = prod H (prod H x y) (one H)" - and "x \ \\<^sub>2 = prod G x (one H)" - by (rule refl)+ - -text {* - Note that the trivial statements above need to be given as a - simultaneous goal in order to have type-inference make the implicit - typing of structures @{text G} and @{text H} agree. -*} - - -subsection {* Simple meta-theory of structures *} - -text {* - The packaging of the logical specification as a predicate and the - syntactic structure as a record type provides a reasonable starting - point for simple meta-theoretic studies of mathematical structures. - This includes operations on structures (also known as ``functors''), - and statements about such constructions. - - For example, the direct product of semigroups works as follows. -*} - -constdefs - semigroup_product :: "'a semigroup \ 'b semigroup \ ('a \ 'b) semigroup" - "semigroup_product S T \ - \prod = \p q. (prod S (fst p) (fst q), prod T (snd p) (snd q))\" - -lemma semigroup_product [intro]: - assumes S: "semigroup S" - and T: "semigroup T" - shows "semigroup (semigroup_product S T)" -proof - fix p q r :: "'a \ 'b" - have "prod S (prod S (fst p) (fst q)) (fst r) = - prod S (fst p) (prod S (fst q) (fst r))" - by (rule semigroup.assoc [OF S]) - moreover have "prod T (prod T (snd p) (snd q)) (snd r) = - prod T (snd p) (prod T (snd q) (snd r))" - by (rule semigroup.assoc [OF T]) - ultimately - show "prod (semigroup_product S T) (prod (semigroup_product S T) p q) r = - prod (semigroup_product S T) p (prod (semigroup_product S T) q r)" - by (simp add: semigroup_product_def) -qed - -text {* - The above proof is fairly easy, but obscured by the lack of concrete - syntax. In fact, we didn't make use of the infrastructure of - locales, apart from the raw predicate definition of @{text - semigroup}. - - The alternative version below uses local context expressions to - achieve a succinct proof body. The resulting statement is exactly - the same as before, even though its specification is a bit more - complex. -*} - -lemma - includes semigroup S + semigroup T - fixes U (structure) - defines "U \ semigroup_product S T" - shows "semigroup U" -proof - fix p q r :: "'a \ 'b" - have "(fst p \\<^sub>1 fst q) \\<^sub>1 fst r = fst p \\<^sub>1 (fst q \\<^sub>1 fst r)" - by (rule S.assoc) - moreover have "(snd p \\<^sub>2 snd q) \\<^sub>2 snd r = snd p \\<^sub>2 (snd q \\<^sub>2 snd r)" - by (rule T.assoc) - ultimately show "(p \\<^sub>3 q) \\<^sub>3 r = p \\<^sub>3 (q \\<^sub>3 r)" - by (simp add: U_def semigroup_product_def semigroup.defs) -qed - -text {* - Direct products of group structures may be defined in a similar - manner, taking two further operations into account. Subsequently, - we use high-level record operations to convert between different - signature types explicitly; see also - \cite[\S8.3]{isabelle-hol-book}. -*} - -constdefs - group_product :: "'a group \ 'b group \ ('a \ 'b) group" - "group_product G H \ - semigroup.extend - (semigroup_product (semigroup.truncate G) (semigroup.truncate H)) - (group.fields (\p. (inv G (fst p), inv H (snd p))) (one G, one H))" - -lemma group_product_aux: - includes group G + group H - fixes I (structure) - defines "I \ group_product G H" - shows "group I" -proof - show "semigroup I" - proof - - let ?G' = "semigroup.truncate G" and ?H' = "semigroup.truncate H" - have "prod (semigroup_product ?G' ?H') = prod I" - by (simp add: I_def group_product_def group.defs - semigroup_product_def semigroup.defs) - moreover - have "semigroup ?G'" and "semigroup ?H'" - using prems by (simp_all add: semigroup_def semigroup.defs G.assoc H.assoc) - then have "semigroup (semigroup_product ?G' ?H')" .. - ultimately show ?thesis by (simp add: I_def semigroup_def) - qed - show "group_axioms I" - proof - fix p :: "'a \ 'b" - have "(fst p)\\<^sub>1 \\<^sub>1 fst p = \\<^sub>1" - by (rule G.left_inv) - moreover have "(snd p)\\<^sub>2 \\<^sub>2 snd p = \\<^sub>2" - by (rule H.left_inv) - ultimately show "p\\<^sub>3 \\<^sub>3 p = \\<^sub>3" - by (simp add: I_def group_product_def group.defs - semigroup_product_def semigroup.defs) - have "\\<^sub>1 \\<^sub>1 fst p = fst p" by (rule G.left_one) - moreover have "\\<^sub>2 \\<^sub>2 snd p = snd p" by (rule H.left_one) - ultimately show "\\<^sub>3 \\<^sub>3 p = p" - by (simp add: I_def group_product_def group.defs - semigroup_product_def semigroup.defs) - qed -qed - -theorem group_product: "group G \ group H \ group (group_product G H)" - by (rule group_product_aux) (assumption | rule group.axioms)+ - -end