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 *)
     5 
     6 header {* Using locales in Isabelle/Isar -- outdated version! *}
     7 
     8 theory Locales imports Main begin
     9 
    10 text_raw {*
    11   \newcommand{\isasyminv}{\isasyminverse}
    12   \newcommand{\isasymIN}{\isatext{\isakeyword{in}}}
    13   \newcommand{\isasymINCLUDES}{\isatext{\isakeyword{includes}}}
    14 *}
    15 
    16 subsection {* Overview *}
    17 
    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).
    25 
    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.
    33 
    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).
    46 
    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}).
    55 
    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.
    70 
    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).
    80 
    81   \medskip The present version of Isabelle/Isar locales still lacks
    82   some important specification concepts.
    83 
    84   \begin{itemize}
    85 
    86   \item Separate language elements for \emph{instantiation} of
    87   locales.
    88 
    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.
    93 
    94   \item Interpretation of locales (think of ``views'', ``functors''
    95   etc.).
    96 
    97   In principle one could directly work with functions over structures
    98   (extensible records), and predicates being derived from locale
    99   definitions.
   100 
   101   \end{itemize}
   102 
   103   \medskip Subsequently, we demonstrate some readily available
   104   concepts of Isabelle/Isar locales by some simple examples of
   105   abstract algebraic reasoning.
   106 *}
   107 
   108 
   109 subsection {* Local contexts as mathematical structures *}
   110 
   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 *}
   117 
   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"
   125 
   126 locale abelian_group_context = group_context +
   127   assumes commute: "x \<cdot> y = y \<cdot> x"
   128 
   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 *}
   136 
   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
   150 
   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
   160 
   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).
   168 
   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 *}
   174 
   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
   186 
   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
   198 
   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
   211 
   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 *}
   218 
   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
   226 
   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.
   235 
   236   \medskip Some more properties of inversion in general group theory
   237   follow.
   238 *}
   239 
   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
   245 
   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
   258 
   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:
   265 
   266   @{thm [display] group_context_def [no_vars]}
   267 
   268   The corresponding introduction rule is as follows:
   269 
   270   @{thm [display, mode = no_brackets] group_context.intro [no_vars]}
   271 
   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).
   276 
   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 *}
   284 
   285 
   286 subsection {* Explicit structures referenced implicitly *}
   287 
   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 *}
   293 
   294 record 'a semigroup =
   295   prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<cdot>\<index>" 70)
   296 
   297 record 'a group = "'a semigroup" +
   298   inv :: "'a \<Rightarrow> 'a"    ("(_\<inv>\<index>)" [1000] 999)
   299   one :: 'a    ("\<one>\<index>")
   300 
   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"}.
   308 
   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 *}
   314 
   315 locale semigroup =
   316   fixes S    (structure)
   317   assumes assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
   318 
   319 locale group = semigroup G +
   320   assumes left_inv: "x\<inv> \<cdot> x = \<one>"
   321     and left_one: "\<one> \<cdot> x = x"
   322 
   323 declare semigroup.intro [intro?]
   324   group.intro [intro?] group_axioms.intro [intro?]
   325 
   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}.
   336 
   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 *}
   341 
   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
   355 
   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
   365 
   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>}).
   372 
   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 *}
   377 
   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)+
   385 
   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 *}
   391 
   392 
   393 subsection {* Simple meta-theory of structures *}
   394 
   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.
   401 
   402   For example, the direct product of semigroups works as follows.
   403 *}
   404 
   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>"
   409 
   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
   427 
   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}.
   433 
   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 *}
   439 
   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
   454 
   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 *}
   462 
   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))"
   469 
   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
   505 
   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)+
   508 
   509 end