src/HOL/ex/Locales.thy
author wenzelm
Thu, 08 Nov 2001 23:50:08 +0100
changeset 12105 1e4451999200
parent 12099 8504c948fae2
child 12356 ce0961b1f536
permissions -rw-r--r--
tuned;
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
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
     7
header {* Basic use of 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
12091
08b4da78d1ad added structures;
wenzelm
parents: 12075
diff changeset
    11
text {*
12105
wenzelm
parents: 12099
diff changeset
    12
  Locales provide a mechanism for encapsulating local contexts.  The
wenzelm
parents: 12099
diff changeset
    13
  original version due to Florian Kamm\"uller \cite{Kamm-et-al:1999}
wenzelm
parents: 12099
diff changeset
    14
  refers directly to the raw meta-logic of Isabelle.  The present
wenzelm
parents: 12099
diff changeset
    15
  version for Isabelle/Isar
wenzelm
parents: 12099
diff changeset
    16
  \cite{Wenzel:1999,Wenzel:2001:isar-ref,Wenzel:2001:Thesis} builds on
wenzelm
parents: 12099
diff changeset
    17
  top of the rich infrastructure of proof contexts instead; this also
wenzelm
parents: 12099
diff changeset
    18
  covers essential extra-logical concepts like term abbreviations or
wenzelm
parents: 12099
diff changeset
    19
  local theorem attributes (e.g.\ declarations of simplification
wenzelm
parents: 12099
diff changeset
    20
  rules).
wenzelm
parents: 12099
diff changeset
    21
wenzelm
parents: 12099
diff changeset
    22
  Subsequently, we demonstrate basic use of locales to model
wenzelm
parents: 12099
diff changeset
    23
  mathematical structures (by the inevitable group theory example).
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
    24
*}
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
    25
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
    26
text_raw {*
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
    27
  \newcommand{\isasyminv}{\isasyminverse}
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
    28
  \newcommand{\isasymone}{\isamath{1}}
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
    29
  \newcommand{\isasymIN}{\isatext{\isakeyword{in}}}
12091
08b4da78d1ad added structures;
wenzelm
parents: 12075
diff changeset
    30
*}
08b4da78d1ad added structures;
wenzelm
parents: 12075
diff changeset
    31
08b4da78d1ad added structures;
wenzelm
parents: 12075
diff changeset
    32
08b4da78d1ad added structures;
wenzelm
parents: 12075
diff changeset
    33
subsection {* Local contexts as mathematical structures *}
08b4da78d1ad added structures;
wenzelm
parents: 12075
diff changeset
    34
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
    35
text {*
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
    36
  The following definitions of @{text group} and @{text abelian_group}
12105
wenzelm
parents: 12099
diff changeset
    37
  merely encapsulate local parameters (with private syntax) and
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
    38
  assumptions; local definitions may be given as well, but are not
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
    39
  shown here.
12075
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    40
*}
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    41
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    42
locale group =
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    43
  fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<cdot>" 70)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    44
    and inv :: "'a \<Rightarrow> 'a"    ("(_\<inv>)" [1000] 999)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    45
    and one :: 'a    ("\<one>")
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    46
  assumes assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    47
    and left_inv: "x\<inv> \<cdot> x = \<one>"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    48
    and left_one: "\<one> \<cdot> x = x"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    49
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    50
locale abelian_group = group +
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    51
  assumes commute: "x \<cdot> y = y \<cdot> x"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    52
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
    53
text {*
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
    54
  \medskip We may now prove theorems within a local context, just by
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
    55
  including a directive ``@{text "(\<IN> name)"}'' in the goal
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
    56
  specification.  The final result will be stored within the named
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
    57
  locale; a second copy is exported to the enclosing theory context.
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
    58
*}
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
    59
12075
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    60
theorem (in group)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    61
  right_inv: "x \<cdot> x\<inv> = \<one>"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    62
proof -
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    63
  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
    64
  also have "\<dots> = \<one> \<cdot> x \<cdot> x\<inv>" by (simp only: assoc)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    65
  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
    66
  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
    67
  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
    68
  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
    69
  also have "\<dots> = (x\<inv>)\<inv> \<cdot> x\<inv>" by (simp only: left_one)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    70
  also have "\<dots> = \<one>" by (simp only: left_inv)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    71
  finally show ?thesis .
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    72
qed
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    73
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    74
theorem (in group)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    75
  right_one: "x \<cdot> \<one> = x"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    76
proof -
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    77
  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
    78
  also have "\<dots> = x \<cdot> x\<inv> \<cdot> x" by (simp only: assoc)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    79
  also have "\<dots> = \<one> \<cdot> x" by (simp only: right_inv)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    80
  also have "\<dots> = x" by (simp only: left_one)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    81
  finally show ?thesis .
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    82
qed
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    83
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
    84
text {*
12105
wenzelm
parents: 12099
diff changeset
    85
  \medskip Apart from the named context we may also refer to further
wenzelm
parents: 12099
diff changeset
    86
  context elements (parameters, assumptions, etc.) in a casual manner;
wenzelm
parents: 12099
diff changeset
    87
  these are discharged when the proof is finished.
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
    88
*}
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
    89
12075
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    90
theorem (in group)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    91
  (assumes eq: "e \<cdot> x = x")
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    92
  one_equality: "\<one> = e"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    93
proof -
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    94
  have "\<one> = x \<cdot> x\<inv>" by (simp only: right_inv)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    95
  also have "\<dots> = (e \<cdot> x) \<cdot> x\<inv>" by (simp only: eq)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    96
  also have "\<dots> = e \<cdot> (x \<cdot> x\<inv>)" by (simp only: assoc)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    97
  also have "\<dots> = e \<cdot> \<one>" by (simp only: right_inv)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    98
  also have "\<dots> = e" by (simp only: right_one)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    99
  finally show ?thesis .
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   100
qed
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   101
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   102
theorem (in group)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   103
  (assumes eq: "x' \<cdot> x = \<one>")
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   104
  inv_equality: "x\<inv> = x'"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   105
proof -
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   106
  have "x\<inv> = \<one> \<cdot> x\<inv>" by (simp only: left_one)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   107
  also have "\<dots> = (x' \<cdot> x) \<cdot> x\<inv>" by (simp only: eq)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   108
  also have "\<dots> = x' \<cdot> (x \<cdot> x\<inv>)" by (simp only: assoc)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   109
  also have "\<dots> = x' \<cdot> \<one>" by (simp only: right_inv)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   110
  also have "\<dots> = x'" by (simp only: right_one)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   111
  finally show ?thesis .
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   112
qed
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   113
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   114
theorem (in group)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   115
  inv_prod: "(x \<cdot> y)\<inv> = y\<inv> \<cdot> x\<inv>"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   116
proof (rule inv_equality)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   117
  show "(y\<inv> \<cdot> x\<inv>) \<cdot> (x \<cdot> y) = \<one>"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   118
  proof -
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   119
    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
   120
    also have "\<dots> = (y\<inv> \<cdot> \<one>) \<cdot> y" by (simp only: left_inv)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   121
    also have "\<dots> = y\<inv> \<cdot> y" by (simp only: right_one)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   122
    also have "\<dots> = \<one>" by (simp only: left_inv)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   123
    finally show ?thesis .
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   124
  qed
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   125
qed
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   126
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   127
text {*
12105
wenzelm
parents: 12099
diff changeset
   128
  \medskip Established results are automatically propagated through
wenzelm
parents: 12099
diff changeset
   129
  the hierarchy of locales.  Below we establish a trivial fact in
wenzelm
parents: 12099
diff changeset
   130
  commutative groups, while referring both to theorems of @{text
wenzelm
parents: 12099
diff changeset
   131
  group} and the additional assumption of @{text abelian_group}.
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   132
*}
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   133
12075
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   134
theorem (in abelian_group)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   135
  inv_prod': "(x \<cdot> y)\<inv> = x\<inv> \<cdot> y\<inv>"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   136
proof -
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   137
  have "(x \<cdot> y)\<inv> = y\<inv> \<cdot> x\<inv>" by (rule inv_prod)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   138
  also have "\<dots> = x\<inv> \<cdot> y\<inv>" by (rule commute)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   139
  finally show ?thesis .
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   140
qed
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   141
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   142
text {*
12105
wenzelm
parents: 12099
diff changeset
   143
  \medskip Some further properties of inversion in general group
wenzelm
parents: 12099
diff changeset
   144
  theory follow.
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   145
*}
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   146
12075
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   147
theorem (in group)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   148
  inv_inv: "(x\<inv>)\<inv> = x"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   149
proof (rule inv_equality)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   150
  show "x \<cdot> x\<inv> = \<one>" by (simp only: right_inv)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   151
qed
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   152
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   153
theorem (in group)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   154
  (assumes eq: "x\<inv> = y\<inv>")
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   155
  inv_inject: "x = y"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   156
proof -
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   157
  have "x = x \<cdot> \<one>" by (simp only: right_one)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   158
  also have "\<dots> = x \<cdot> (y\<inv> \<cdot> y)" by (simp only: left_inv)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   159
  also have "\<dots> = x \<cdot> (x\<inv> \<cdot> y)" by (simp only: eq)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   160
  also have "\<dots> = (x \<cdot> x\<inv>) \<cdot> y" by (simp only: assoc)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   161
  also have "\<dots> = \<one> \<cdot> y" by (simp only: right_inv)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   162
  also have "\<dots> = y" by (simp only: left_one)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   163
  finally show ?thesis .
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   164
qed
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   165
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   166
text {*
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   167
  \bigskip We see that this representation of structures as local
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   168
  contexts is rather light-weight and convenient to use for abstract
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   169
  reasoning.  Here the ``components'' (the group operations) have been
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   170
  exhibited directly as context parameters; logically this corresponds
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   171
  to a curried predicate definition.  Occasionally, this
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   172
  ``externalized'' version of the informal idea of classes of tuple
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   173
  structures may cause some inconveniences, especially in
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   174
  meta-theoretical studies (involving functors from groups to groups,
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   175
  for example).
12091
08b4da78d1ad added structures;
wenzelm
parents: 12075
diff changeset
   176
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   177
  Another drawback of the naive approach above is that concrete syntax
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   178
  will get lost on any kind of operation on the locale itself (such as
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   179
  renaming, copying, or instantiation).  Whenever the particular
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   180
  terminology of local parameters is affected the associated syntax
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   181
  would have to be changed as well, which is hard to achieve formally.
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   182
*}
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   183
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   184
12105
wenzelm
parents: 12099
diff changeset
   185
subsection {* Explicit structures referenced implicitly *}
12091
08b4da78d1ad added structures;
wenzelm
parents: 12075
diff changeset
   186
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   187
text {*
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   188
  The issue of multiple parameters raised above may be easily
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   189
  addressed by stating properties over a record of group operations,
12105
wenzelm
parents: 12099
diff changeset
   190
  instead of the individual constituents.  See
wenzelm
parents: 12099
diff changeset
   191
  \cite{Naraschewski-Wenzel:1998,Nipkow-et-al:2001:HOL} on
wenzelm
parents: 12099
diff changeset
   192
  (extensible) record types in Isabelle/HOL.
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   193
*}
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   194
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   195
record 'a group =
12091
08b4da78d1ad added structures;
wenzelm
parents: 12075
diff changeset
   196
  prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   197
  inv :: "'a \<Rightarrow> 'a"
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   198
  one :: 'a
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   199
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   200
text {*
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   201
  Now concrete syntax essentially needs refer to record selections;
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   202
  this is possible by giving defined operations with private syntax
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   203
  within the locale (e.g.\ see appropriate examples by Kamm\"uller).
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   204
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   205
  In the subsequent formulation of group structures we go one step
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   206
  further by using \emph{implicit} references to the underlying
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   207
  abstract entity.  To this end we define global syntax, which is
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   208
  translated to refer to the ``current'' structure at hand, denoted by
12105
wenzelm
parents: 12099
diff changeset
   209
  the dummy item ``@{text \<struct>}'' (according to the builtin syntax
wenzelm
parents: 12099
diff changeset
   210
  mechanism for locales).
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   211
*}
12091
08b4da78d1ad added structures;
wenzelm
parents: 12075
diff changeset
   212
08b4da78d1ad added structures;
wenzelm
parents: 12075
diff changeset
   213
syntax
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   214
  "_prod" :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<cdot>" 70)
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   215
  "_inv" :: "'a \<Rightarrow> 'a"    ("(_\<inv>)" [1000] 999)
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   216
  "_one" :: 'a    ("\<one>")
12091
08b4da78d1ad added structures;
wenzelm
parents: 12075
diff changeset
   217
translations
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   218
  "x \<cdot> y"  \<rightleftharpoons>  "prod \<struct> x y"
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   219
  "x\<inv>"  \<rightleftharpoons>  "inv \<struct> x"
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   220
  "\<one>"  \<rightleftharpoons>  "one \<struct>"
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   221
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   222
text {*
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   223
  The following locale definition introduces a single parameter, which
12105
wenzelm
parents: 12099
diff changeset
   224
  is declared as a ``\isakeyword{structure}''. In its context the
wenzelm
parents: 12099
diff changeset
   225
  dummy ``@{text \<struct>}'' refers to this very parameter, independently of
wenzelm
parents: 12099
diff changeset
   226
  the present naming.
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   227
*}
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   228
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   229
locale group_struct =
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   230
  fixes G :: "'a group"    (structure)
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   231
  assumes assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   232
    and left_inv: "x\<inv> \<cdot> x = \<one>"
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   233
    and left_one: "\<one> \<cdot> x = x"
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   234
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   235
text {*
12105
wenzelm
parents: 12099
diff changeset
   236
  We may now proceed to prove results within @{text group_struct} just
wenzelm
parents: 12099
diff changeset
   237
  as before for @{text group}.  Proper treatment of ``@{text \<struct>}'' is
wenzelm
parents: 12099
diff changeset
   238
  hidden in concrete syntax, so the proof text is exactly the same as
wenzelm
parents: 12099
diff changeset
   239
  before.
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   240
*}
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   241
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   242
theorem (in group_struct)
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   243
  right_inv: "x \<cdot> x\<inv> = \<one>"
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   244
proof -
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   245
  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
   246
  also have "\<dots> = \<one> \<cdot> x \<cdot> x\<inv>" by (simp only: assoc)
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   247
  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
   248
  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
   249
  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
   250
  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
   251
  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
   252
  also have "\<dots> = \<one>" by (simp only: left_inv)
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   253
  finally show ?thesis .
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   254
qed
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   255
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   256
theorem (in group_struct)
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   257
  right_one: "x \<cdot> \<one> = x"
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   258
proof -
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   259
  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
   260
  also have "\<dots> = x \<cdot> x\<inv> \<cdot> x" by (simp only: assoc)
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   261
  also have "\<dots> = \<one> \<cdot> x" by (simp only: right_inv)
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   262
  also have "\<dots> = x" by (simp only: left_one)
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   263
  finally show ?thesis .
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   264
qed
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   265
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   266
text {*
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   267
  \medskip Several implicit structures may be active at the same time
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   268
  (say up to 3 in practice).  The concrete syntax facility for locales
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   269
  actually maintains indexed dummies @{text "\<struct>\<^sub>1"}, @{text
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   270
  "\<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
   271
  @{text "\<struct>\<^sub>1"}).  So we are able to provide concrete syntax to
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   272
  cover the 2nd and 3rd group structure as well.
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   273
*}
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   274
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   275
syntax
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   276
  "_prod'" :: "'a \<Rightarrow> index \<Rightarrow> 'a \<Rightarrow> 'a"    ("(_ \<cdot>_/ _)" [70, 1000, 71] 70)
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   277
  "_inv'" :: "'a \<Rightarrow> index \<Rightarrow> 'a"    ("(_\<inv>_)" [1000] 999)
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   278
  "_one'" :: "index \<Rightarrow> 'a"    ("\<one>_")
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   279
translations
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   280
  "x \<cdot>\<^sub>2 y"  \<rightleftharpoons>  "prod \<struct>\<^sub>2 x y"
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   281
  "x \<cdot>\<^sub>3 y"  \<rightleftharpoons>  "prod \<struct>\<^sub>3 x y"
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   282
  "x\<inv>\<^sub>2"  \<rightleftharpoons>  "inv \<struct>\<^sub>2 x"
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   283
  "x\<inv>\<^sub>3"  \<rightleftharpoons>  "inv \<struct>\<^sub>3 x"
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   284
  "\<one>\<^sub>2"  \<rightleftharpoons>  "one \<struct>\<^sub>2"
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   285
  "\<one>\<^sub>3"  \<rightleftharpoons>  "one \<struct>\<^sub>3"
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   286
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   287
text {*
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   288
  \medskip The following synthetic example demonstrates how to refer
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   289
  to several structures of type @{text group} succinctly; one might
12105
wenzelm
parents: 12099
diff changeset
   290
  also think of working with several renamed versions of the @{text
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   291
  group_struct} locale above.
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   292
*}
12091
08b4da78d1ad added structures;
wenzelm
parents: 12075
diff changeset
   293
08b4da78d1ad added structures;
wenzelm
parents: 12075
diff changeset
   294
lemma
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   295
  (fixes G :: "'a group" (structure)
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   296
    and H :: "'a group" (structure))
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   297
  True
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   298
proof
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   299
  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
   300
  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
   301
  have "x \<cdot> \<one>\<^sub>2 = prod G x (one H)" ..
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   302
qed
12091
08b4da78d1ad added structures;
wenzelm
parents: 12075
diff changeset
   303
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   304
text {*
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   305
  \medskip As a minor drawback of this advanced technique we require
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   306
  slightly more work to setup abstract and concrete syntax properly
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   307
  (but only once in the beginning).  The resulting casual mode of
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   308
  writing @{text "x \<cdot> y"} for @{text "prod G x y"} etc.\ mimics common
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   309
  practice of informal mathematics quite nicely, while using a simple
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   310
  and robust formal representation.
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   311
*}
12091
08b4da78d1ad added structures;
wenzelm
parents: 12075
diff changeset
   312
12099
8504c948fae2 more explanations on advanced syntax;
wenzelm
parents: 12091
diff changeset
   313
end