src/HOL/ex/Locales.thy
author ballarin
Tue Jun 20 15:53:44 2006 +0200 (2006-06-20)
changeset 19931 fb32b43e7f80
parent 17388 495c799df31d
permissions -rw-r--r--
Restructured locales with predicates: import is now an interpretation.
New method intro_locales.
wenzelm@12075
     1
(*  Title:      HOL/ex/Locales.thy
wenzelm@12075
     2
    ID:         $Id$
wenzelm@12574
     3
    Author:     Markus Wenzel, LMU München
wenzelm@12075
     4
*)
wenzelm@12075
     5
wenzelm@17388
     6
header {* Using locales in Isabelle/Isar -- outdated version! *}
wenzelm@12075
     7
haftmann@16417
     8
theory Locales imports Main begin
wenzelm@12075
     9
wenzelm@12507
    10
text_raw {*
wenzelm@12507
    11
  \newcommand{\isasyminv}{\isasyminverse}
wenzelm@12507
    12
  \newcommand{\isasymIN}{\isatext{\isakeyword{in}}}
wenzelm@12965
    13
  \newcommand{\isasymINCLUDES}{\isatext{\isakeyword{includes}}}
wenzelm@12507
    14
*}
wenzelm@12507
    15
wenzelm@12507
    16
subsection {* Overview *}
wenzelm@12507
    17
wenzelm@12091
    18
text {*
wenzelm@12105
    19
  Locales provide a mechanism for encapsulating local contexts.  The
wenzelm@12574
    20
  original version due to Florian Kammüller \cite{Kamm-et-al:1999}
wenzelm@13538
    21
  refers directly to Isabelle's meta-logic \cite{Paulson:1989}, which
wenzelm@13538
    22
  is minimal higher-order logic with connectives @{text "\<And>"}
wenzelm@13538
    23
  (universal quantification), @{text "\<Longrightarrow>"} (implication), and @{text
wenzelm@13538
    24
  "\<equiv>"} (equality).
wenzelm@13538
    25
wenzelm@13538
    26
  From this perspective, a locale is essentially a meta-level
wenzelm@13538
    27
  predicate, together with some infrastructure to manage the
wenzelm@13538
    28
  abstracted parameters (@{text "\<And>"}), assumptions (@{text "\<Longrightarrow>"}), and
wenzelm@13538
    29
  definitions for (@{text "\<equiv>"}) in a reasonable way during the proof
wenzelm@13538
    30
  process.  This simple predicate view also provides a solid
wenzelm@13538
    31
  semantical basis for our specification concepts to be developed
wenzelm@13538
    32
  later.
wenzelm@12507
    33
wenzelm@13538
    34
  \medskip The present version of locales for Isabelle/Isar builds on
wenzelm@13538
    35
  top of the rich infrastructure of proof contexts
wenzelm@13538
    36
  \cite{Wenzel:1999,Wenzel:2001:isar-ref,Wenzel:2001:Thesis}, which in
wenzelm@13538
    37
  turn is based on the same meta-logic.  Thus we achieve a tight
wenzelm@13538
    38
  integration with Isar proof texts, and a slightly more abstract view
wenzelm@13538
    39
  of the underlying logical concepts.  An Isar proof context
wenzelm@13538
    40
  encapsulates certain language elements that correspond to @{text
wenzelm@13538
    41
  "\<And>/\<Longrightarrow>/\<equiv>"} at the level of structure proof texts.  Moreover, there are
wenzelm@13538
    42
  extra-logical concepts like term abbreviations or local theorem
wenzelm@13538
    43
  attributes (declarations of simplification rules etc.) that are
wenzelm@13538
    44
  useful in applications (e.g.\ consider standard simplification rules
wenzelm@13538
    45
  declared in a group context).
wenzelm@12507
    46
wenzelm@13538
    47
  Locales also support concrete syntax, i.e.\ a localized version of
wenzelm@12507
    48
  the existing concept of mixfix annotations of Isabelle
wenzelm@12507
    49
  \cite{Paulson:1994:Isabelle}.  Furthermore, there is a separate
wenzelm@12507
    50
  concept of ``implicit structures'' that admits to refer to
wenzelm@13538
    51
  particular locale parameters in a casual manner (basically a
wenzelm@13538
    52
  simplified version of the idea of ``anti-quotations'', or
wenzelm@13538
    53
  generalized de-Bruijn indexes as demonstrated elsewhere
wenzelm@13538
    54
  \cite[\S13--14]{Wenzel:2001:Isar-examples}).
wenzelm@12105
    55
wenzelm@12507
    56
  Implicit structures work particular well together with extensible
wenzelm@13538
    57
  records in HOL \cite{Naraschewski-Wenzel:1998} (without the
wenzelm@13538
    58
  ``object-oriented'' features discussed there as well).  Thus we
wenzelm@13538
    59
  achieve a specification technique where record type schemes
wenzelm@13538
    60
  represent polymorphic signatures of mathematical structures, and
wenzelm@13538
    61
  actual locales describe the corresponding logical properties.
wenzelm@13538
    62
  Semantically speaking, such abstract mathematical structures are
wenzelm@13538
    63
  just predicates over record types.  Due to type inference of
wenzelm@13538
    64
  simply-typed records (which subsumes structural subtyping) we arrive
wenzelm@13538
    65
  at succinct specification texts --- ``signature morphisms''
wenzelm@13538
    66
  degenerate to implicit type-instantiations.  Additional eye-candy is
wenzelm@13538
    67
  provided by the separate concept of ``indexed concrete syntax'' used
wenzelm@13538
    68
  for record selectors, so we get close to informal mathematical
wenzelm@13538
    69
  notation.
wenzelm@12507
    70
wenzelm@13538
    71
  \medskip Operations for building up locale contexts from existing
wenzelm@13538
    72
  ones include \emph{merge} (disjoint union) and \emph{rename} (of
wenzelm@13538
    73
  term parameters only, types are inferred automatically).  Here we
wenzelm@13538
    74
  draw from existing traditions of algebraic specification languages.
wenzelm@13538
    75
  A structured specification corresponds to a directed acyclic graph
wenzelm@13538
    76
  of potentially renamed nodes (due to distributivity renames may
wenzelm@13538
    77
  pushed inside of merges).  The result is a ``flattened'' list of
wenzelm@13538
    78
  primitive context elements in canonical order (corresponding to
wenzelm@13538
    79
  left-to-right reading of merges, while suppressing duplicates).
wenzelm@12507
    80
wenzelm@13538
    81
  \medskip The present version of Isabelle/Isar locales still lacks
wenzelm@13538
    82
  some important specification concepts.
wenzelm@13538
    83
wenzelm@12507
    84
  \begin{itemize}
wenzelm@12099
    85
wenzelm@13538
    86
  \item Separate language elements for \emph{instantiation} of
wenzelm@12507
    87
  locales.
wenzelm@12507
    88
wenzelm@12507
    89
  Currently users may simulate this to some extend by having primitive
wenzelm@12507
    90
  Isabelle/Isar operations (@{text of} for substitution and @{text OF}
wenzelm@12507
    91
  for composition, \cite{Wenzel:2001:isar-ref}) act on the
wenzelm@12507
    92
  automatically exported results stemming from different contexts.
wenzelm@12507
    93
wenzelm@13538
    94
  \item Interpretation of locales (think of ``views'', ``functors''
wenzelm@13538
    95
  etc.).
wenzelm@12507
    96
wenzelm@12507
    97
  In principle one could directly work with functions over structures
wenzelm@12507
    98
  (extensible records), and predicates being derived from locale
wenzelm@12507
    99
  definitions.
wenzelm@12507
   100
wenzelm@12507
   101
  \end{itemize}
wenzelm@12507
   102
wenzelm@12507
   103
  \medskip Subsequently, we demonstrate some readily available
wenzelm@12507
   104
  concepts of Isabelle/Isar locales by some simple examples of
wenzelm@12507
   105
  abstract algebraic reasoning.
wenzelm@12091
   106
*}
wenzelm@12091
   107
wenzelm@13538
   108
wenzelm@12091
   109
subsection {* Local contexts as mathematical structures *}
wenzelm@12091
   110
wenzelm@12099
   111
text {*
wenzelm@13538
   112
  The following definitions of @{text group_context} and @{text
wenzelm@13538
   113
  abelian_group_context} merely encapsulate local parameters (with
wenzelm@13538
   114
  private syntax) and assumptions; local definitions of derived
wenzelm@13538
   115
  concepts could be given, too, but are unused below.
wenzelm@12075
   116
*}
wenzelm@12075
   117
wenzelm@12574
   118
locale group_context =
wenzelm@12075
   119
  fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<cdot>" 70)
wenzelm@12075
   120
    and inv :: "'a \<Rightarrow> 'a"    ("(_\<inv>)" [1000] 999)
wenzelm@12075
   121
    and one :: 'a    ("\<one>")
wenzelm@12075
   122
  assumes assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
wenzelm@12075
   123
    and left_inv: "x\<inv> \<cdot> x = \<one>"
wenzelm@12075
   124
    and left_one: "\<one> \<cdot> x = x"
wenzelm@12075
   125
wenzelm@12574
   126
locale abelian_group_context = group_context +
wenzelm@12075
   127
  assumes commute: "x \<cdot> y = y \<cdot> x"
wenzelm@12075
   128
wenzelm@12099
   129
text {*
wenzelm@12099
   130
  \medskip We may now prove theorems within a local context, just by
wenzelm@12099
   131
  including a directive ``@{text "(\<IN> name)"}'' in the goal
wenzelm@12099
   132
  specification.  The final result will be stored within the named
wenzelm@13538
   133
  locale, still holding the context; a second copy is exported to the
wenzelm@13538
   134
  enclosing theory context (with qualified name).
wenzelm@12099
   135
*}
wenzelm@12099
   136
wenzelm@12574
   137
theorem (in group_context)
wenzelm@12075
   138
  right_inv: "x \<cdot> x\<inv> = \<one>"
wenzelm@12075
   139
proof -
wenzelm@12075
   140
  have "x \<cdot> x\<inv> = \<one> \<cdot> (x \<cdot> x\<inv>)" by (simp only: left_one)
wenzelm@12075
   141
  also have "\<dots> = \<one> \<cdot> x \<cdot> x\<inv>" by (simp only: assoc)
wenzelm@12075
   142
  also have "\<dots> = (x\<inv>)\<inv> \<cdot> x\<inv> \<cdot> x \<cdot> x\<inv>" by (simp only: left_inv)
wenzelm@12075
   143
  also have "\<dots> = (x\<inv>)\<inv> \<cdot> (x\<inv> \<cdot> x) \<cdot> x\<inv>" by (simp only: assoc)
wenzelm@12075
   144
  also have "\<dots> = (x\<inv>)\<inv> \<cdot> \<one> \<cdot> x\<inv>" by (simp only: left_inv)
wenzelm@12075
   145
  also have "\<dots> = (x\<inv>)\<inv> \<cdot> (\<one> \<cdot> x\<inv>)" by (simp only: assoc)
wenzelm@12075
   146
  also have "\<dots> = (x\<inv>)\<inv> \<cdot> x\<inv>" by (simp only: left_one)
wenzelm@12075
   147
  also have "\<dots> = \<one>" by (simp only: left_inv)
wenzelm@12075
   148
  finally show ?thesis .
wenzelm@12075
   149
qed
wenzelm@12075
   150
wenzelm@12574
   151
theorem (in group_context)
wenzelm@12075
   152
  right_one: "x \<cdot> \<one> = x"
wenzelm@12075
   153
proof -
wenzelm@12075
   154
  have "x \<cdot> \<one> = x \<cdot> (x\<inv> \<cdot> x)" by (simp only: left_inv)
wenzelm@12075
   155
  also have "\<dots> = x \<cdot> x\<inv> \<cdot> x" by (simp only: assoc)
wenzelm@12075
   156
  also have "\<dots> = \<one> \<cdot> x" by (simp only: right_inv)
wenzelm@12075
   157
  also have "\<dots> = x" by (simp only: left_one)
wenzelm@12075
   158
  finally show ?thesis .
wenzelm@12075
   159
qed
wenzelm@12075
   160
wenzelm@12099
   161
text {*
wenzelm@13538
   162
  Facts like @{text right_one} are available @{text group_context} as
wenzelm@13538
   163
  stated above.  The exported version looses the additional
wenzelm@13538
   164
  infrastructure of Isar proof contexts (syntax etc.) retaining only
wenzelm@13538
   165
  the pure logical content: @{thm [source] group_context.right_one}
wenzelm@13538
   166
  becomes @{thm group_context.right_one} (in Isabelle outermost @{text
wenzelm@13538
   167
  \<And>} quantification is replaced by schematic variables).
wenzelm@13538
   168
wenzelm@13538
   169
  \medskip Apart from a named locale we may also refer to further
wenzelm@13538
   170
  context elements (parameters, assumptions, etc.) in an ad-hoc
wenzelm@13538
   171
  fashion, just for this particular statement.  In the result (local
wenzelm@13538
   172
  or global), any additional elements are discharged as usual.
wenzelm@12099
   173
*}
wenzelm@12099
   174
wenzelm@12574
   175
theorem (in group_context)
wenzelm@12937
   176
  assumes eq: "e \<cdot> x = x"
wenzelm@12937
   177
  shows one_equality: "\<one> = e"
wenzelm@12075
   178
proof -
wenzelm@12075
   179
  have "\<one> = x \<cdot> x\<inv>" by (simp only: right_inv)
wenzelm@12075
   180
  also have "\<dots> = (e \<cdot> x) \<cdot> x\<inv>" by (simp only: eq)
wenzelm@12075
   181
  also have "\<dots> = e \<cdot> (x \<cdot> x\<inv>)" by (simp only: assoc)
wenzelm@12075
   182
  also have "\<dots> = e \<cdot> \<one>" by (simp only: right_inv)
wenzelm@12075
   183
  also have "\<dots> = e" by (simp only: right_one)
wenzelm@12075
   184
  finally show ?thesis .
wenzelm@12075
   185
qed
wenzelm@12075
   186
wenzelm@12574
   187
theorem (in group_context)
wenzelm@12937
   188
  assumes eq: "x' \<cdot> x = \<one>"
wenzelm@12937
   189
  shows inv_equality: "x\<inv> = x'"
wenzelm@12075
   190
proof -
wenzelm@12075
   191
  have "x\<inv> = \<one> \<cdot> x\<inv>" by (simp only: left_one)
wenzelm@12075
   192
  also have "\<dots> = (x' \<cdot> x) \<cdot> x\<inv>" by (simp only: eq)
wenzelm@12075
   193
  also have "\<dots> = x' \<cdot> (x \<cdot> x\<inv>)" by (simp only: assoc)
wenzelm@12075
   194
  also have "\<dots> = x' \<cdot> \<one>" by (simp only: right_inv)
wenzelm@12075
   195
  also have "\<dots> = x'" by (simp only: right_one)
wenzelm@12075
   196
  finally show ?thesis .
wenzelm@12075
   197
qed
wenzelm@12075
   198
wenzelm@12574
   199
theorem (in group_context)
wenzelm@12075
   200
  inv_prod: "(x \<cdot> y)\<inv> = y\<inv> \<cdot> x\<inv>"
wenzelm@12075
   201
proof (rule inv_equality)
wenzelm@12075
   202
  show "(y\<inv> \<cdot> x\<inv>) \<cdot> (x \<cdot> y) = \<one>"
wenzelm@12075
   203
  proof -
wenzelm@12075
   204
    have "(y\<inv> \<cdot> x\<inv>) \<cdot> (x \<cdot> y) = (y\<inv> \<cdot> (x\<inv> \<cdot> x)) \<cdot> y" by (simp only: assoc)
wenzelm@12075
   205
    also have "\<dots> = (y\<inv> \<cdot> \<one>) \<cdot> y" by (simp only: left_inv)
wenzelm@12075
   206
    also have "\<dots> = y\<inv> \<cdot> y" by (simp only: right_one)
wenzelm@12075
   207
    also have "\<dots> = \<one>" by (simp only: left_inv)
wenzelm@12075
   208
    finally show ?thesis .
wenzelm@12075
   209
  qed
wenzelm@12075
   210
qed
wenzelm@12075
   211
wenzelm@12099
   212
text {*
wenzelm@12105
   213
  \medskip Established results are automatically propagated through
wenzelm@12105
   214
  the hierarchy of locales.  Below we establish a trivial fact in
wenzelm@12105
   215
  commutative groups, while referring both to theorems of @{text
wenzelm@12105
   216
  group} and the additional assumption of @{text abelian_group}.
wenzelm@12099
   217
*}
wenzelm@12099
   218
wenzelm@12574
   219
theorem (in abelian_group_context)
wenzelm@12075
   220
  inv_prod': "(x \<cdot> y)\<inv> = x\<inv> \<cdot> y\<inv>"
wenzelm@12075
   221
proof -
wenzelm@12075
   222
  have "(x \<cdot> y)\<inv> = y\<inv> \<cdot> x\<inv>" by (rule inv_prod)
wenzelm@12075
   223
  also have "\<dots> = x\<inv> \<cdot> y\<inv>" by (rule commute)
wenzelm@12075
   224
  finally show ?thesis .
wenzelm@12075
   225
qed
wenzelm@12075
   226
wenzelm@12099
   227
text {*
wenzelm@12507
   228
  We see that the initial import of @{text group} within the
wenzelm@12507
   229
  definition of @{text abelian_group} is actually evaluated
wenzelm@12507
   230
  dynamically.  Thus any results in @{text group} are made available
wenzelm@12507
   231
  to the derived context of @{text abelian_group} as well.  Note that
wenzelm@12965
   232
  the alternative context element @{text \<INCLUDES>} would import
wenzelm@12507
   233
  existing locales in a static fashion, without participating in
wenzelm@12507
   234
  further facts emerging later on.
wenzelm@12507
   235
wenzelm@12507
   236
  \medskip Some more properties of inversion in general group theory
wenzelm@12507
   237
  follow.
wenzelm@12099
   238
*}
wenzelm@12099
   239
wenzelm@12574
   240
theorem (in group_context)
wenzelm@12075
   241
  inv_inv: "(x\<inv>)\<inv> = x"
wenzelm@12075
   242
proof (rule inv_equality)
wenzelm@12075
   243
  show "x \<cdot> x\<inv> = \<one>" by (simp only: right_inv)
wenzelm@12075
   244
qed
wenzelm@12075
   245
wenzelm@12574
   246
theorem (in group_context)
wenzelm@12937
   247
  assumes eq: "x\<inv> = y\<inv>"
wenzelm@12937
   248
  shows inv_inject: "x = y"
wenzelm@12075
   249
proof -
wenzelm@12075
   250
  have "x = x \<cdot> \<one>" by (simp only: right_one)
wenzelm@12075
   251
  also have "\<dots> = x \<cdot> (y\<inv> \<cdot> y)" by (simp only: left_inv)
wenzelm@12075
   252
  also have "\<dots> = x \<cdot> (x\<inv> \<cdot> y)" by (simp only: eq)
wenzelm@12075
   253
  also have "\<dots> = (x \<cdot> x\<inv>) \<cdot> y" by (simp only: assoc)
wenzelm@12075
   254
  also have "\<dots> = \<one> \<cdot> y" by (simp only: right_inv)
wenzelm@12075
   255
  also have "\<dots> = y" by (simp only: left_one)
wenzelm@12075
   256
  finally show ?thesis .
wenzelm@12075
   257
qed
wenzelm@12075
   258
wenzelm@12099
   259
text {*
wenzelm@12099
   260
  \bigskip We see that this representation of structures as local
wenzelm@12099
   261
  contexts is rather light-weight and convenient to use for abstract
wenzelm@12099
   262
  reasoning.  Here the ``components'' (the group operations) have been
wenzelm@12099
   263
  exhibited directly as context parameters; logically this corresponds
wenzelm@13383
   264
  to a curried predicate definition:
wenzelm@13383
   265
wenzelm@13419
   266
  @{thm [display] group_context_def [no_vars]}
wenzelm@13419
   267
wenzelm@13419
   268
  The corresponding introduction rule is as follows:
wenzelm@13419
   269
wenzelm@13457
   270
  @{thm [display, mode = no_brackets] group_context.intro [no_vars]}
wenzelm@13383
   271
wenzelm@13383
   272
  Occasionally, this ``externalized'' version of the informal idea of
wenzelm@13383
   273
  classes of tuple structures may cause some inconveniences,
wenzelm@13383
   274
  especially in meta-theoretical studies (involving functors from
wenzelm@13383
   275
  groups to groups, for example).
wenzelm@12091
   276
wenzelm@12507
   277
  Another minor drawback of the naive approach above is that concrete
wenzelm@12507
   278
  syntax will get lost on any kind of operation on the locale itself
wenzelm@12507
   279
  (such as renaming, copying, or instantiation).  Whenever the
wenzelm@12507
   280
  particular terminology of local parameters is affected the
wenzelm@12507
   281
  associated syntax would have to be changed as well, which is hard to
wenzelm@12507
   282
  achieve formally.
wenzelm@12099
   283
*}
wenzelm@12099
   284
wenzelm@12099
   285
wenzelm@12105
   286
subsection {* Explicit structures referenced implicitly *}
wenzelm@12091
   287
wenzelm@12099
   288
text {*
wenzelm@12507
   289
  We introduce the same hierarchy of basic group structures as above,
wenzelm@12507
   290
  this time using extensible record types for the signature part,
wenzelm@12507
   291
  together with concrete syntax for selector functions.
wenzelm@12099
   292
*}
wenzelm@12099
   293
wenzelm@12507
   294
record 'a semigroup =
wenzelm@12507
   295
  prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<cdot>\<index>" 70)
wenzelm@12507
   296
wenzelm@12507
   297
record 'a group = "'a semigroup" +
wenzelm@12507
   298
  inv :: "'a \<Rightarrow> 'a"    ("(_\<inv>\<index>)" [1000] 999)
wenzelm@12507
   299
  one :: 'a    ("\<one>\<index>")
wenzelm@12099
   300
wenzelm@12099
   301
text {*
wenzelm@12507
   302
  The mixfix annotations above include a special ``structure index
wenzelm@13457
   303
  indicator'' @{text \<index>} that makes grammar productions dependent on
wenzelm@12507
   304
  certain parameters that have been declared as ``structure'' in a
wenzelm@12507
   305
  locale context later on.  Thus we achieve casual notation as
wenzelm@12507
   306
  encountered in informal mathematics, e.g.\ @{text "x \<cdot> y"} for
wenzelm@12507
   307
  @{text "prod G x y"}.
wenzelm@12099
   308
wenzelm@12507
   309
  \medskip The following locale definitions introduce operate on a
wenzelm@12507
   310
  single parameter declared as ``\isakeyword{structure}''.  Type
wenzelm@12507
   311
  inference takes care to fill in the appropriate record type schemes
wenzelm@12507
   312
  internally.
wenzelm@12099
   313
*}
wenzelm@12091
   314
wenzelm@12574
   315
locale semigroup =
wenzelm@13457
   316
  fixes S    (structure)
wenzelm@12507
   317
  assumes assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
wenzelm@12099
   318
wenzelm@12574
   319
locale group = semigroup G +
wenzelm@12507
   320
  assumes left_inv: "x\<inv> \<cdot> x = \<one>"
wenzelm@12099
   321
    and left_one: "\<one> \<cdot> x = x"
wenzelm@12099
   322
ballarin@14254
   323
declare semigroup.intro [intro?]
ballarin@14254
   324
  group.intro [intro?] group_axioms.intro [intro?]
ballarin@14254
   325
wenzelm@12099
   326
text {*
wenzelm@12507
   327
  Note that we prefer to call the @{text group} record structure
wenzelm@12507
   328
  @{text G} rather than @{text S} inherited from @{text semigroup}.
wenzelm@12507
   329
  This does not affect our concrete syntax, which is only dependent on
wenzelm@12507
   330
  the \emph{positional} arrangements of currently active structures
wenzelm@12507
   331
  (actually only one above), rather than names.  In fact, these
wenzelm@12507
   332
  parameter names rarely occur in the term language at all (due to the
wenzelm@12507
   333
  ``indexed syntax'' facility of Isabelle).  On the other hand, names
wenzelm@12507
   334
  of locale facts will get qualified accordingly, e.g. @{text S.assoc}
wenzelm@12507
   335
  versus @{text G.assoc}.
wenzelm@12507
   336
wenzelm@12574
   337
  \medskip We may now proceed to prove results within @{text group}
wenzelm@12574
   338
  just as before for @{text group}.  The subsequent proof texts are
wenzelm@12574
   339
  exactly the same as despite the more advanced internal arrangement.
wenzelm@12099
   340
*}
wenzelm@12099
   341
wenzelm@12574
   342
theorem (in group)
wenzelm@12099
   343
  right_inv: "x \<cdot> x\<inv> = \<one>"
wenzelm@12099
   344
proof -
wenzelm@12099
   345
  have "x \<cdot> x\<inv> = \<one> \<cdot> (x \<cdot> x\<inv>)" by (simp only: left_one)
wenzelm@12099
   346
  also have "\<dots> = \<one> \<cdot> x \<cdot> x\<inv>" by (simp only: assoc)
wenzelm@12099
   347
  also have "\<dots> = (x\<inv>)\<inv> \<cdot> x\<inv> \<cdot> x \<cdot> x\<inv>" by (simp only: left_inv)
wenzelm@12099
   348
  also have "\<dots> = (x\<inv>)\<inv> \<cdot> (x\<inv> \<cdot> x) \<cdot> x\<inv>" by (simp only: assoc)
wenzelm@12099
   349
  also have "\<dots> = (x\<inv>)\<inv> \<cdot> \<one> \<cdot> x\<inv>" by (simp only: left_inv)
wenzelm@12099
   350
  also have "\<dots> = (x\<inv>)\<inv> \<cdot> (\<one> \<cdot> x\<inv>)" by (simp only: assoc)
wenzelm@12099
   351
  also have "\<dots> = (x\<inv>)\<inv> \<cdot> x\<inv>" by (simp only: left_one)
wenzelm@12099
   352
  also have "\<dots> = \<one>" by (simp only: left_inv)
wenzelm@12099
   353
  finally show ?thesis .
wenzelm@12099
   354
qed
wenzelm@12099
   355
wenzelm@12574
   356
theorem (in group)
wenzelm@12099
   357
  right_one: "x \<cdot> \<one> = x"
wenzelm@12099
   358
proof -
wenzelm@12099
   359
  have "x \<cdot> \<one> = x \<cdot> (x\<inv> \<cdot> x)" by (simp only: left_inv)
wenzelm@12099
   360
  also have "\<dots> = x \<cdot> x\<inv> \<cdot> x" by (simp only: assoc)
wenzelm@12099
   361
  also have "\<dots> = \<one> \<cdot> x" by (simp only: right_inv)
wenzelm@12099
   362
  also have "\<dots> = x" by (simp only: left_one)
wenzelm@12099
   363
  finally show ?thesis .
wenzelm@12099
   364
qed
wenzelm@12099
   365
wenzelm@12099
   366
text {*
wenzelm@12574
   367
  \medskip Several implicit structures may be active at the same time.
wenzelm@12574
   368
  The concrete syntax facility for locales actually maintains indexed
wenzelm@12574
   369
  structures that may be references implicitly --- via mixfix
wenzelm@12574
   370
  annotations that have been decorated by an ``index argument''
wenzelm@12574
   371
  (@{text \<index>}).
wenzelm@12099
   372
wenzelm@12574
   373
  The following synthetic example demonstrates how to refer to several
wenzelm@12574
   374
  structures of type @{text group} succinctly.  We work with two
wenzelm@12574
   375
  versions of the @{text group} locale above.
wenzelm@12099
   376
*}
wenzelm@12091
   377
wenzelm@12937
   378
lemma
wenzelm@12955
   379
  includes group G
wenzelm@12955
   380
  includes group H
wenzelm@13107
   381
  shows "x \<cdot> y \<cdot> \<one> = prod G (prod G x y) (one G)"
wenzelm@13107
   382
    and "x \<cdot>\<^sub>2 y \<cdot>\<^sub>2 \<one>\<^sub>2 = prod H (prod H x y) (one H)"
wenzelm@13107
   383
    and "x \<cdot> \<one>\<^sub>2 = prod G x (one H)"
wenzelm@13107
   384
  by (rule refl)+
wenzelm@12574
   385
wenzelm@12574
   386
text {*
wenzelm@12574
   387
  Note that the trivial statements above need to be given as a
wenzelm@12574
   388
  simultaneous goal in order to have type-inference make the implicit
wenzelm@12574
   389
  typing of structures @{text G} and @{text H} agree.
wenzelm@12574
   390
*}
wenzelm@12091
   391
wenzelm@13457
   392
wenzelm@13457
   393
subsection {* Simple meta-theory of structures *}
wenzelm@13457
   394
wenzelm@13457
   395
text {*
wenzelm@13457
   396
  The packaging of the logical specification as a predicate and the
wenzelm@13457
   397
  syntactic structure as a record type provides a reasonable starting
wenzelm@13457
   398
  point for simple meta-theoretic studies of mathematical structures.
wenzelm@13457
   399
  This includes operations on structures (also known as ``functors''),
wenzelm@13457
   400
  and statements about such constructions.
wenzelm@13457
   401
wenzelm@13457
   402
  For example, the direct product of semigroups works as follows.
wenzelm@13457
   403
*}
wenzelm@13457
   404
wenzelm@13457
   405
constdefs
wenzelm@13457
   406
  semigroup_product :: "'a semigroup \<Rightarrow> 'b semigroup \<Rightarrow> ('a \<times> 'b) semigroup"
wenzelm@13538
   407
  "semigroup_product S T \<equiv>
wenzelm@13538
   408
    \<lparr>prod = \<lambda>p q. (prod S (fst p) (fst q), prod T (snd p) (snd q))\<rparr>"
wenzelm@13457
   409
wenzelm@13457
   410
lemma semigroup_product [intro]:
wenzelm@13457
   411
  assumes S: "semigroup S"
wenzelm@13457
   412
    and T: "semigroup T"
wenzelm@13457
   413
  shows "semigroup (semigroup_product S T)"
wenzelm@13457
   414
proof
wenzelm@13457
   415
  fix p q r :: "'a \<times> 'b"
wenzelm@13457
   416
  have "prod S (prod S (fst p) (fst q)) (fst r) =
wenzelm@13457
   417
      prod S (fst p) (prod S (fst q) (fst r))"
wenzelm@13457
   418
    by (rule semigroup.assoc [OF S])
wenzelm@13457
   419
  moreover have "prod T (prod T (snd p) (snd q)) (snd r) =
wenzelm@13457
   420
      prod T (snd p) (prod T (snd q) (snd r))"
wenzelm@13457
   421
    by (rule semigroup.assoc [OF T])
wenzelm@13538
   422
  ultimately
wenzelm@13538
   423
  show "prod (semigroup_product S T) (prod (semigroup_product S T) p q) r =
wenzelm@13457
   424
      prod (semigroup_product S T) p (prod (semigroup_product S T) q r)"
wenzelm@13457
   425
    by (simp add: semigroup_product_def)
wenzelm@13457
   426
qed
wenzelm@13457
   427
wenzelm@13457
   428
text {*
wenzelm@13457
   429
  The above proof is fairly easy, but obscured by the lack of concrete
wenzelm@13457
   430
  syntax.  In fact, we didn't make use of the infrastructure of
wenzelm@13457
   431
  locales, apart from the raw predicate definition of @{text
wenzelm@13457
   432
  semigroup}.
wenzelm@13457
   433
wenzelm@13457
   434
  The alternative version below uses local context expressions to
wenzelm@13457
   435
  achieve a succinct proof body.  The resulting statement is exactly
wenzelm@13457
   436
  the same as before, even though its specification is a bit more
wenzelm@13457
   437
  complex.
wenzelm@13457
   438
*}
wenzelm@13457
   439
wenzelm@13457
   440
lemma
wenzelm@13457
   441
  includes semigroup S + semigroup T
wenzelm@13457
   442
  fixes U    (structure)
wenzelm@13457
   443
  defines "U \<equiv> semigroup_product S T"
wenzelm@13457
   444
  shows "semigroup U"
wenzelm@13457
   445
proof
wenzelm@13457
   446
  fix p q r :: "'a \<times> 'b"
wenzelm@13457
   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)"
wenzelm@13457
   448
    by (rule S.assoc)
wenzelm@13457
   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)"
wenzelm@13457
   450
    by (rule T.assoc)
wenzelm@13457
   451
  ultimately show "(p \<cdot>\<^sub>3 q) \<cdot>\<^sub>3 r = p \<cdot>\<^sub>3 (q \<cdot>\<^sub>3 r)"
wenzelm@13457
   452
    by (simp add: U_def semigroup_product_def semigroup.defs)
wenzelm@13457
   453
qed
wenzelm@13457
   454
wenzelm@13457
   455
text {*
wenzelm@13457
   456
  Direct products of group structures may be defined in a similar
wenzelm@13457
   457
  manner, taking two further operations into account.  Subsequently,
wenzelm@13457
   458
  we use high-level record operations to convert between different
wenzelm@13457
   459
  signature types explicitly; see also
wenzelm@13457
   460
  \cite[\S8.3]{isabelle-hol-book}.
wenzelm@13457
   461
*}
wenzelm@13457
   462
wenzelm@13457
   463
constdefs
wenzelm@13457
   464
  group_product :: "'a group \<Rightarrow> 'b group \<Rightarrow> ('a \<times> 'b) group"
wenzelm@13457
   465
  "group_product G H \<equiv>
wenzelm@13457
   466
    semigroup.extend
wenzelm@13457
   467
      (semigroup_product (semigroup.truncate G) (semigroup.truncate H))
wenzelm@13457
   468
      (group.fields (\<lambda>p. (inv G (fst p), inv H (snd p))) (one G, one H))"
wenzelm@13457
   469
wenzelm@13457
   470
lemma group_product_aux:
wenzelm@13457
   471
  includes group G + group H
wenzelm@13457
   472
  fixes I    (structure)
wenzelm@13457
   473
  defines "I \<equiv> group_product G H"
wenzelm@13457
   474
  shows "group I"
wenzelm@13457
   475
proof
wenzelm@13457
   476
  show "semigroup I"
wenzelm@13457
   477
  proof -
wenzelm@13457
   478
    let ?G' = "semigroup.truncate G" and ?H' = "semigroup.truncate H"
wenzelm@13457
   479
    have "prod (semigroup_product ?G' ?H') = prod I"
wenzelm@13538
   480
      by (simp add: I_def group_product_def group.defs
wenzelm@13538
   481
	semigroup_product_def semigroup.defs)
wenzelm@13457
   482
    moreover
wenzelm@13457
   483
    have "semigroup ?G'" and "semigroup ?H'"
ballarin@19931
   484
      using prems by (simp_all add: semigroup_def semigroup.defs G.assoc H.assoc)
wenzelm@13457
   485
    then have "semigroup (semigroup_product ?G' ?H')" ..
wenzelm@13457
   486
    ultimately show ?thesis by (simp add: I_def semigroup_def)
wenzelm@13457
   487
  qed
wenzelm@13457
   488
  show "group_axioms I"
wenzelm@13457
   489
  proof
wenzelm@13457
   490
    fix p :: "'a \<times> 'b"
wenzelm@13457
   491
    have "(fst p)\<inv>\<^sub>1 \<cdot>\<^sub>1 fst p = \<one>\<^sub>1"
wenzelm@13457
   492
      by (rule G.left_inv)
wenzelm@13457
   493
    moreover have "(snd p)\<inv>\<^sub>2 \<cdot>\<^sub>2 snd p = \<one>\<^sub>2"
wenzelm@13457
   494
      by (rule H.left_inv)
wenzelm@13457
   495
    ultimately show "p\<inv>\<^sub>3 \<cdot>\<^sub>3 p = \<one>\<^sub>3"
wenzelm@13538
   496
      by (simp add: I_def group_product_def group.defs
wenzelm@13538
   497
	semigroup_product_def semigroup.defs)
wenzelm@13457
   498
    have "\<one>\<^sub>1 \<cdot>\<^sub>1 fst p = fst p" by (rule G.left_one)
wenzelm@13457
   499
    moreover have "\<one>\<^sub>2 \<cdot>\<^sub>2 snd p = snd p" by (rule H.left_one)
wenzelm@13457
   500
    ultimately show "\<one>\<^sub>3 \<cdot>\<^sub>3 p = p"
wenzelm@13538
   501
      by (simp add: I_def group_product_def group.defs
wenzelm@13538
   502
	semigroup_product_def semigroup.defs)
wenzelm@13457
   503
  qed
wenzelm@13457
   504
qed
wenzelm@13457
   505
wenzelm@13457
   506
theorem group_product: "group G \<Longrightarrow> group H \<Longrightarrow> group (group_product G H)"
wenzelm@13457
   507
  by (rule group_product_aux) (assumption | rule group.axioms)+
wenzelm@13457
   508
wenzelm@12099
   509
end