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