src/HOL/ex/Locales.thy
author wenzelm
Fri, 14 Dec 2001 22:27:43 +0100
changeset 12507 cc36d5da9bc0
parent 12356 ce0961b1f536
child 12574 ff84d5f14085
permissions -rw-r--r--
updated;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12075
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/ex/Locales.thy
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, LMU Muenchen
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
     5
*)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
     6
12507
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
     7
header {* Using locales in Isabelle/Isar *}
12075
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
     8
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
     9
theory Locales = Main:
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    10
12507
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    11
text_raw {*
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    12
  \newcommand{\isasyminv}{\isasyminverse}
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    13
  \newcommand{\isasymIN}{\isatext{\isakeyword{in}}}
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    14
  \newcommand{\isasymUSES}{\isatext{\isakeyword{uses}}}
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    15
*}
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    16
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    17
subsection {* Overview *}
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    18
12091
08b4da78d1ad added structures;
wenzelm
parents: 12075
diff changeset
    19
text {*
12105
wenzelm
parents: 12099
diff changeset
    20
  Locales provide a mechanism for encapsulating local contexts.  The
wenzelm
parents: 12099
diff changeset
    21
  original version due to Florian Kamm\"uller \cite{Kamm-et-al:1999}
12507
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    22
  refers directly to the raw meta-logic of Isabelle.  Semantically, a
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    23
  locale is just a (curried) predicate of the pure meta-logic
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    24
  \cite{Paulson:1989}.
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    25
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    26
  The present version for Isabelle/Isar builds on top of the rich
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    27
  infrastructure of proof contexts
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    28
  \cite{Wenzel:1999,Wenzel:2001:isar-ref,Wenzel:2001:Thesis},
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    29
  achieving a tight integration with Isar proof texts, and a slightly
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    30
  more abstract view of the underlying concepts.  An Isar proof
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    31
  context encapsulates certain language elements that correspond to
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    32
  @{text \<And>} (universal quantification), @{text \<Longrightarrow>} (implication), and
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    33
  @{text "\<equiv>"} (definitions) of the pure Isabelle framework.  Moreover,
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    34
  there are extra-logical concepts like term abbreviations or local
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    35
  theorem attributes (declarations of simplification rules etc.) that
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    36
  are indispensable in realistic applications.
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    37
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    38
  Locales support concrete syntax, providing a localized version of
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    39
  the existing concept of mixfix annotations of Isabelle
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    40
  \cite{Paulson:1994:Isabelle}.  Furthermore, there is a separate
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    41
  concept of ``implicit structures'' that admits to refer to
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    42
  particular locale parameters in a casual manner (essentially derived
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    43
  from the basic idea of ``anti-quotations'' or generalized de-Bruijn
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    44
  indexes demonstrated in \cite[\S13--14]{Wenzel:2001:Isar-examples}).
12105
wenzelm
parents: 12099
diff changeset
    45
12507
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    46
  Implicit structures work particular well together with extensible
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    47
  records in HOL \cite{Naraschewski-Wenzel:1998} (the
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    48
  ``object-oriented'' features discussed there are not required here).
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    49
  Thus we shall essentially use record types to represent polymorphic
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    50
  signatures of mathematical structures, while locales describe their
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    51
  logical properties as a predicate.  Due to type inference of
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    52
  simply-typed records we are able to give succinct specifications,
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    53
  without caring about signature morphisms ourselves.  Further
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    54
  eye-candy is provided by the independent concept of ``indexed
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    55
  concrete syntax'' for record selectors.
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    56
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    57
  Operations for building up locale contexts from existing definitions
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    58
  cover common operations of \emph{merge} (disjunctive union in
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    59
  canonical order) and \emph{rename} (of term parameters; types are
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    60
  always inferred automatically).
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    61
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    62
  \medskip Note that the following further concepts are still
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    63
  \emph{absent}:
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    64
  \begin{itemize}
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
    65
12507
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    66
  \item Specific language elements for \emph{instantiation} of
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    67
  locales.
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    68
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    69
  Currently users may simulate this to some extend by having primitive
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    70
  Isabelle/Isar operations (@{text of} for substitution and @{text OF}
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    71
  for composition, \cite{Wenzel:2001:isar-ref}) act on the
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    72
  automatically exported results stemming from different contexts.
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    73
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    74
  \item Interpretation of locales, analogous to ``functors'' in
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    75
  abstract algebra.
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    76
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    77
  In principle one could directly work with functions over structures
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    78
  (extensible records), and predicates being derived from locale
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    79
  definitions.
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    80
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    81
  \end{itemize}
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    82
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    83
  \medskip Subsequently, we demonstrate some readily available
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    84
  concepts of Isabelle/Isar locales by some simple examples of
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
    85
  abstract algebraic reasoning.
12091
08b4da78d1ad added structures;
wenzelm
parents: 12075
diff changeset
    86
*}
08b4da78d1ad added structures;
wenzelm
parents: 12075
diff changeset
    87
08b4da78d1ad added structures;
wenzelm
parents: 12075
diff changeset
    88
subsection {* Local contexts as mathematical structures *}
08b4da78d1ad added structures;
wenzelm
parents: 12075
diff changeset
    89
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
    90
text {*
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
    91
  The following definitions of @{text group} and @{text abelian_group}
12105
wenzelm
parents: 12099
diff changeset
    92
  merely encapsulate local parameters (with private syntax) and
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
    93
  assumptions; local definitions may be given as well, but are not
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
    94
  shown here.
12075
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    95
*}
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    96
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    97
locale group =
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    98
  fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<cdot>" 70)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    99
    and inv :: "'a \<Rightarrow> 'a"    ("(_\<inv>)" [1000] 999)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   100
    and one :: 'a    ("\<one>")
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   101
  assumes assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   102
    and left_inv: "x\<inv> \<cdot> x = \<one>"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   103
    and left_one: "\<one> \<cdot> x = x"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   104
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   105
locale abelian_group = group +
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   106
  assumes commute: "x \<cdot> y = y \<cdot> x"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   107
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   108
text {*
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   109
  \medskip We may now prove theorems within a local context, just by
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   110
  including a directive ``@{text "(\<IN> name)"}'' in the goal
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   111
  specification.  The final result will be stored within the named
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   112
  locale; a second copy is exported to the enclosing theory context.
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   113
*}
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   114
12075
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   115
theorem (in group)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   116
  right_inv: "x \<cdot> x\<inv> = \<one>"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   117
proof -
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   118
  have "x \<cdot> x\<inv> = \<one> \<cdot> (x \<cdot> x\<inv>)" by (simp only: left_one)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   119
  also have "\<dots> = \<one> \<cdot> x \<cdot> x\<inv>" by (simp only: assoc)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   120
  also have "\<dots> = (x\<inv>)\<inv> \<cdot> x\<inv> \<cdot> x \<cdot> x\<inv>" by (simp only: left_inv)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   121
  also have "\<dots> = (x\<inv>)\<inv> \<cdot> (x\<inv> \<cdot> x) \<cdot> x\<inv>" by (simp only: assoc)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   122
  also have "\<dots> = (x\<inv>)\<inv> \<cdot> \<one> \<cdot> x\<inv>" by (simp only: left_inv)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   123
  also have "\<dots> = (x\<inv>)\<inv> \<cdot> (\<one> \<cdot> x\<inv>)" by (simp only: assoc)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   124
  also have "\<dots> = (x\<inv>)\<inv> \<cdot> x\<inv>" by (simp only: left_one)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   125
  also have "\<dots> = \<one>" by (simp only: left_inv)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   126
  finally show ?thesis .
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   127
qed
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   128
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   129
theorem (in group)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   130
  right_one: "x \<cdot> \<one> = x"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   131
proof -
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   132
  have "x \<cdot> \<one> = x \<cdot> (x\<inv> \<cdot> x)" by (simp only: left_inv)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   133
  also have "\<dots> = x \<cdot> x\<inv> \<cdot> x" by (simp only: assoc)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   134
  also have "\<dots> = \<one> \<cdot> x" by (simp only: right_inv)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   135
  also have "\<dots> = x" by (simp only: left_one)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   136
  finally show ?thesis .
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   137
qed
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   138
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   139
text {*
12105
wenzelm
parents: 12099
diff changeset
   140
  \medskip Apart from the named context we may also refer to further
wenzelm
parents: 12099
diff changeset
   141
  context elements (parameters, assumptions, etc.) in a casual manner;
wenzelm
parents: 12099
diff changeset
   142
  these are discharged when the proof is finished.
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   143
*}
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   144
12075
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   145
theorem (in group)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   146
  (assumes eq: "e \<cdot> x = x")
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   147
  one_equality: "\<one> = e"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   148
proof -
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   149
  have "\<one> = x \<cdot> x\<inv>" by (simp only: right_inv)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   150
  also have "\<dots> = (e \<cdot> x) \<cdot> x\<inv>" by (simp only: eq)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   151
  also have "\<dots> = e \<cdot> (x \<cdot> x\<inv>)" by (simp only: assoc)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   152
  also have "\<dots> = e \<cdot> \<one>" by (simp only: right_inv)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   153
  also have "\<dots> = e" by (simp only: right_one)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   154
  finally show ?thesis .
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   155
qed
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   156
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   157
theorem (in group)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   158
  (assumes eq: "x' \<cdot> x = \<one>")
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   159
  inv_equality: "x\<inv> = x'"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   160
proof -
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   161
  have "x\<inv> = \<one> \<cdot> x\<inv>" by (simp only: left_one)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   162
  also have "\<dots> = (x' \<cdot> x) \<cdot> x\<inv>" by (simp only: eq)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   163
  also have "\<dots> = x' \<cdot> (x \<cdot> x\<inv>)" by (simp only: assoc)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   164
  also have "\<dots> = x' \<cdot> \<one>" by (simp only: right_inv)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   165
  also have "\<dots> = x'" by (simp only: right_one)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   166
  finally show ?thesis .
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   167
qed
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   168
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   169
theorem (in group)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   170
  inv_prod: "(x \<cdot> y)\<inv> = y\<inv> \<cdot> x\<inv>"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   171
proof (rule inv_equality)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   172
  show "(y\<inv> \<cdot> x\<inv>) \<cdot> (x \<cdot> y) = \<one>"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   173
  proof -
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   174
    have "(y\<inv> \<cdot> x\<inv>) \<cdot> (x \<cdot> y) = (y\<inv> \<cdot> (x\<inv> \<cdot> x)) \<cdot> y" by (simp only: assoc)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   175
    also have "\<dots> = (y\<inv> \<cdot> \<one>) \<cdot> y" by (simp only: left_inv)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   176
    also have "\<dots> = y\<inv> \<cdot> y" by (simp only: right_one)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   177
    also have "\<dots> = \<one>" by (simp only: left_inv)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   178
    finally show ?thesis .
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   179
  qed
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   180
qed
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   181
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   182
text {*
12105
wenzelm
parents: 12099
diff changeset
   183
  \medskip Established results are automatically propagated through
wenzelm
parents: 12099
diff changeset
   184
  the hierarchy of locales.  Below we establish a trivial fact in
wenzelm
parents: 12099
diff changeset
   185
  commutative groups, while referring both to theorems of @{text
wenzelm
parents: 12099
diff changeset
   186
  group} and the additional assumption of @{text abelian_group}.
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   187
*}
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   188
12075
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   189
theorem (in abelian_group)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   190
  inv_prod': "(x \<cdot> y)\<inv> = x\<inv> \<cdot> y\<inv>"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   191
proof -
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   192
  have "(x \<cdot> y)\<inv> = y\<inv> \<cdot> x\<inv>" by (rule inv_prod)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   193
  also have "\<dots> = x\<inv> \<cdot> y\<inv>" by (rule commute)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   194
  finally show ?thesis .
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   195
qed
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   196
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   197
text {*
12507
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   198
  We see that the initial import of @{text group} within the
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   199
  definition of @{text abelian_group} is actually evaluated
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   200
  dynamically.  Thus any results in @{text group} are made available
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   201
  to the derived context of @{text abelian_group} as well.  Note that
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   202
  the alternative context element @{text \<USES>} would import
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   203
  existing locales in a static fashion, without participating in
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   204
  further facts emerging later on.
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   205
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   206
  \medskip Some more properties of inversion in general group theory
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   207
  follow.
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   208
*}
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   209
12075
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   210
theorem (in group)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   211
  inv_inv: "(x\<inv>)\<inv> = x"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   212
proof (rule inv_equality)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   213
  show "x \<cdot> x\<inv> = \<one>" by (simp only: right_inv)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   214
qed
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   215
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   216
theorem (in group)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   217
  (assumes eq: "x\<inv> = y\<inv>")
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   218
  inv_inject: "x = y"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   219
proof -
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   220
  have "x = x \<cdot> \<one>" by (simp only: right_one)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   221
  also have "\<dots> = x \<cdot> (y\<inv> \<cdot> y)" by (simp only: left_inv)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   222
  also have "\<dots> = x \<cdot> (x\<inv> \<cdot> y)" by (simp only: eq)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   223
  also have "\<dots> = (x \<cdot> x\<inv>) \<cdot> y" by (simp only: assoc)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   224
  also have "\<dots> = \<one> \<cdot> y" by (simp only: right_inv)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   225
  also have "\<dots> = y" by (simp only: left_one)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   226
  finally show ?thesis .
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   227
qed
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   228
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   229
text {*
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   230
  \bigskip We see that this representation of structures as local
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   231
  contexts is rather light-weight and convenient to use for abstract
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   232
  reasoning.  Here the ``components'' (the group operations) have been
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   233
  exhibited directly as context parameters; logically this corresponds
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   234
  to a curried predicate definition.  Occasionally, this
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   235
  ``externalized'' version of the informal idea of classes of tuple
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   236
  structures may cause some inconveniences, especially in
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   237
  meta-theoretical studies (involving functors from groups to groups,
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   238
  for example).
12091
08b4da78d1ad added structures;
wenzelm
parents: 12075
diff changeset
   239
12507
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   240
  Another minor drawback of the naive approach above is that concrete
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   241
  syntax will get lost on any kind of operation on the locale itself
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   242
  (such as renaming, copying, or instantiation).  Whenever the
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   243
  particular terminology of local parameters is affected the
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   244
  associated syntax would have to be changed as well, which is hard to
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   245
  achieve formally.
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   246
*}
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   247
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   248
12105
wenzelm
parents: 12099
diff changeset
   249
subsection {* Explicit structures referenced implicitly *}
12091
08b4da78d1ad added structures;
wenzelm
parents: 12075
diff changeset
   250
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   251
text {*
12507
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   252
  We introduce the same hierarchy of basic group structures as above,
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   253
  this time using extensible record types for the signature part,
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   254
  together with concrete syntax for selector functions.
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   255
*}
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   256
12507
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   257
record 'a semigroup =
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   258
  prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<cdot>\<index>" 70)
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   259
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   260
record 'a group = "'a semigroup" +
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   261
  inv :: "'a \<Rightarrow> 'a"    ("(_\<inv>\<index>)" [1000] 999)
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   262
  one :: 'a    ("\<one>\<index>")
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   263
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   264
text {*
12507
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   265
  The mixfix annotations above include a special ``structure index
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   266
  indicator'' @{text \<index>} that makes grammer productions dependent on
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   267
  certain parameters that have been declared as ``structure'' in a
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   268
  locale context later on.  Thus we achieve casual notation as
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   269
  encountered in informal mathematics, e.g.\ @{text "x \<cdot> y"} for
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   270
  @{text "prod G x y"}.
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   271
12507
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   272
  \medskip The following locale definitions introduce operate on a
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   273
  single parameter declared as ``\isakeyword{structure}''.  Type
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   274
  inference takes care to fill in the appropriate record type schemes
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   275
  internally.
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   276
*}
12091
08b4da78d1ad added structures;
wenzelm
parents: 12075
diff changeset
   277
12507
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   278
locale semigroup_struct =
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   279
  fixes S :: "'a group"    (structure)
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   280
  assumes assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   281
12507
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   282
locale group_struct = semigroup_struct G +
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   283
  assumes left_inv: "x\<inv> \<cdot> x = \<one>"
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   284
    and left_one: "\<one> \<cdot> x = x"
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   285
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   286
text {*
12507
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   287
  Note that we prefer to call the @{text group} record structure
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   288
  @{text G} rather than @{text S} inherited from @{text semigroup}.
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   289
  This does not affect our concrete syntax, which is only dependent on
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   290
  the \emph{positional} arrangements of currently active structures
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   291
  (actually only one above), rather than names.  In fact, these
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   292
  parameter names rarely occur in the term language at all (due to the
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   293
  ``indexed syntax'' facility of Isabelle).  On the other hand, names
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   294
  of locale facts will get qualified accordingly, e.g. @{text S.assoc}
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   295
  versus @{text G.assoc}.
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   296
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   297
  \medskip We may now proceed to prove results within @{text
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   298
  group_struct} just as before for @{text group}.  The subsequent
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   299
  proof texts are exactly the same as despite the more advanced
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   300
  internal arrangement.
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   301
*}
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   302
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   303
theorem (in group_struct)
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   304
  right_inv: "x \<cdot> x\<inv> = \<one>"
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   305
proof -
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   306
  have "x \<cdot> x\<inv> = \<one> \<cdot> (x \<cdot> x\<inv>)" by (simp only: left_one)
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   307
  also have "\<dots> = \<one> \<cdot> x \<cdot> x\<inv>" by (simp only: assoc)
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   308
  also have "\<dots> = (x\<inv>)\<inv> \<cdot> x\<inv> \<cdot> x \<cdot> x\<inv>" by (simp only: left_inv)
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   309
  also have "\<dots> = (x\<inv>)\<inv> \<cdot> (x\<inv> \<cdot> x) \<cdot> x\<inv>" by (simp only: assoc)
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   310
  also have "\<dots> = (x\<inv>)\<inv> \<cdot> \<one> \<cdot> x\<inv>" by (simp only: left_inv)
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   311
  also have "\<dots> = (x\<inv>)\<inv> \<cdot> (\<one> \<cdot> x\<inv>)" by (simp only: assoc)
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   312
  also have "\<dots> = (x\<inv>)\<inv> \<cdot> x\<inv>" by (simp only: left_one)
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   313
  also have "\<dots> = \<one>" by (simp only: left_inv)
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   314
  finally show ?thesis .
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   315
qed
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   316
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   317
theorem (in group_struct)
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   318
  right_one: "x \<cdot> \<one> = x"
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   319
proof -
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   320
  have "x \<cdot> \<one> = x \<cdot> (x\<inv> \<cdot> x)" by (simp only: left_inv)
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   321
  also have "\<dots> = x \<cdot> x\<inv> \<cdot> x" by (simp only: assoc)
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   322
  also have "\<dots> = \<one> \<cdot> x" by (simp only: right_inv)
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   323
  also have "\<dots> = x" by (simp only: left_one)
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   324
  finally show ?thesis .
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   325
qed
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   326
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   327
text {*
12507
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   328
  FIXME
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   329
  \medskip Several implicit structures may be active at the same time
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   330
  (say up to 3 in practice).  The concrete syntax facility for locales
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   331
  actually maintains indexed dummies @{text "\<struct>\<^sub>1"}, @{text
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   332
  "\<struct>\<^sub>2"}, @{text "\<struct>\<^sub>3"}, \dots (@{text \<struct>} is the same as
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   333
  @{text "\<struct>\<^sub>1"}).  So we are able to provide concrete syntax to
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   334
  cover the 2nd and 3rd group structure as well.
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   335
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   336
  \medskip The following synthetic example demonstrates how to refer
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   337
  to several structures of type @{text group} succinctly; one might
12105
wenzelm
parents: 12099
diff changeset
   338
  also think of working with several renamed versions of the @{text
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   339
  group_struct} locale above.
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   340
*}
12091
08b4da78d1ad added structures;
wenzelm
parents: 12075
diff changeset
   341
08b4da78d1ad added structures;
wenzelm
parents: 12075
diff changeset
   342
lemma
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   343
  (fixes G :: "'a group" (structure)
12507
cc36d5da9bc0 updated;
wenzelm
parents: 12356
diff changeset
   344
    and H :: "'a group" (structure))  (* FIXME (uses group_struct G + group_struct H) *)
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   345
  True
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   346
proof
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   347
  have "x \<cdot> y \<cdot> \<one> = prod G (prod G x y) (one G)" ..
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   348
  have "x \<cdot>\<^sub>2 y \<cdot>\<^sub>2 \<one>\<^sub>2 = prod H (prod H x y) (one H)" ..
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   349
  have "x \<cdot> \<one>\<^sub>2 = prod G x (one H)" ..
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   350
qed
12091
08b4da78d1ad added structures;
wenzelm
parents: 12075
diff changeset
   351
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   352
end