--- 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 "\<And>"}
- (universal quantification), @{text "\<Longrightarrow>"} (implication), and @{text
- "\<equiv>"} (equality).
-
- From this perspective, a locale is essentially a meta-level
- predicate, together with some infrastructure to manage the
- abstracted parameters (@{text "\<And>"}), assumptions (@{text "\<Longrightarrow>"}), and
- definitions for (@{text "\<equiv>"}) 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
- "\<And>/\<Longrightarrow>/\<equiv>"} 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 \<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_context = group_context +
- 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, still holding the context; a second copy is exported to the
- enclosing theory context (with qualified name).
-*}
-
-theorem (in group_context)
- 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_context)
- 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 {*
- 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
- \<And>} 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 \<cdot> x = x"
- shows 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_context)
- assumes eq: "x' \<cdot> x = \<one>"
- shows 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_context)
- 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_context)
- 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 {*
- 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 \<INCLUDES>} 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\<inv>)\<inv> = x"
-proof (rule inv_equality)
- show "x \<cdot> x\<inv> = \<one>" by (simp only: right_inv)
-qed
-
-theorem (in group_context)
- assumes eq: "x\<inv> = y\<inv>"
- shows 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:
-
- @{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 \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<cdot>\<index>" 70)
-
-record 'a group = "'a semigroup" +
- inv :: "'a \<Rightarrow> 'a" ("(_\<inv>\<index>)" [1000] 999)
- one :: 'a ("\<one>\<index>")
-
-text {*
- The mixfix annotations above include a special ``structure index
- indicator'' @{text \<index>} 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 \<cdot> 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 \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
-
-locale group = semigroup G +
- assumes left_inv: "x\<inv> \<cdot> x = \<one>"
- and left_one: "\<one> \<cdot> 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 \<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 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 \<index>}).
-
- 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 \<cdot> y \<cdot> \<one> = prod G (prod G x y) (one G)"
- and "x \<cdot>\<^sub>2 y \<cdot>\<^sub>2 \<one>\<^sub>2 = prod H (prod H x y) (one H)"
- and "x \<cdot> \<one>\<^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 \<Rightarrow> 'b semigroup \<Rightarrow> ('a \<times> 'b) semigroup"
- "semigroup_product S T \<equiv>
- \<lparr>prod = \<lambda>p q. (prod S (fst p) (fst q), prod T (snd p) (snd q))\<rparr>"
-
-lemma semigroup_product [intro]:
- assumes S: "semigroup S"
- and T: "semigroup T"
- shows "semigroup (semigroup_product S T)"
-proof
- fix p q r :: "'a \<times> '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 \<equiv> semigroup_product S T"
- shows "semigroup U"
-proof
- fix p q r :: "'a \<times> 'b"
- 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)"
- by (rule S.assoc)
- 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)"
- by (rule T.assoc)
- ultimately show "(p \<cdot>\<^sub>3 q) \<cdot>\<^sub>3 r = p \<cdot>\<^sub>3 (q \<cdot>\<^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 \<Rightarrow> 'b group \<Rightarrow> ('a \<times> 'b) group"
- "group_product G H \<equiv>
- semigroup.extend
- (semigroup_product (semigroup.truncate G) (semigroup.truncate H))
- (group.fields (\<lambda>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 \<equiv> 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 \<times> 'b"
- have "(fst p)\<inv>\<^sub>1 \<cdot>\<^sub>1 fst p = \<one>\<^sub>1"
- by (rule G.left_inv)
- moreover have "(snd p)\<inv>\<^sub>2 \<cdot>\<^sub>2 snd p = \<one>\<^sub>2"
- by (rule H.left_inv)
- ultimately show "p\<inv>\<^sub>3 \<cdot>\<^sub>3 p = \<one>\<^sub>3"
- by (simp add: I_def group_product_def group.defs
- semigroup_product_def semigroup.defs)
- have "\<one>\<^sub>1 \<cdot>\<^sub>1 fst p = fst p" by (rule G.left_one)
- moreover have "\<one>\<^sub>2 \<cdot>\<^sub>2 snd p = snd p" by (rule H.left_one)
- ultimately show "\<one>\<^sub>3 \<cdot>\<^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 \<Longrightarrow> group H \<Longrightarrow> group (group_product G H)"
- by (rule group_product_aux) (assumption | rule group.axioms)+
-
-end