src/HOL/ex/Locales.thy
author wenzelm
Tue, 06 Nov 2001 23:45:58 +0100
changeset 12075 8d65dd96381f
child 12091 08b4da78d1ad
permissions -rw-r--r--
Locales and simple mathematical structures;
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
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
     7
header {* Locales and simple mathematical structures *}
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
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    11
text_raw {*
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    12
  \newcommand{\isasyminv}{\isasyminverse}
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    13
  \newcommand{\isasymone}{\isamath{1}}
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    14
*}
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    15
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    16
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    17
subsection {* Groups *}
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    18
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    19
text {*
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    20
  Locales version of the inevitable group example.
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    21
*}
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    22
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    23
locale group =
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    24
  fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<cdot>" 70)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    25
    and inv :: "'a \<Rightarrow> 'a"    ("(_\<inv>)" [1000] 999)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    26
    and one :: 'a    ("\<one>")
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    27
  assumes assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    28
    and left_inv: "x\<inv> \<cdot> x = \<one>"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    29
    and left_one: "\<one> \<cdot> x = x"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    30
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    31
locale abelian_group = group +
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    32
  assumes commute: "x \<cdot> y = y \<cdot> x"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    33
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    34
theorem (in group)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    35
  right_inv: "x \<cdot> x\<inv> = \<one>"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    36
proof -
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    37
  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
    38
  also have "\<dots> = \<one> \<cdot> x \<cdot> x\<inv>" by (simp only: assoc)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    39
  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
    40
  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
    41
  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
    42
  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
    43
  also have "\<dots> = (x\<inv>)\<inv> \<cdot> x\<inv>" by (simp only: left_one)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    44
  also have "\<dots> = \<one>" by (simp only: left_inv)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    45
  finally show ?thesis .
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    46
qed
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    47
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    48
theorem (in group)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    49
  right_one: "x \<cdot> \<one> = x"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    50
proof -
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    51
  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
    52
  also have "\<dots> = x \<cdot> x\<inv> \<cdot> x" by (simp only: assoc)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    53
  also have "\<dots> = \<one> \<cdot> x" by (simp only: right_inv)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    54
  also have "\<dots> = x" by (simp only: left_one)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    55
  finally show ?thesis .
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    56
qed
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    57
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    58
theorem (in group)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    59
  (assumes eq: "e \<cdot> x = x")
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    60
  one_equality: "\<one> = e"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    61
proof -
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    62
  have "\<one> = x \<cdot> x\<inv>" by (simp only: right_inv)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    63
  also have "\<dots> = (e \<cdot> x) \<cdot> x\<inv>" by (simp only: eq)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    64
  also have "\<dots> = e \<cdot> (x \<cdot> x\<inv>)" by (simp only: assoc)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    65
  also have "\<dots> = e \<cdot> \<one>" by (simp only: right_inv)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    66
  also have "\<dots> = e" by (simp only: right_one)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    67
  finally show ?thesis .
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    68
qed
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    69
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    70
theorem (in group)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    71
  (assumes eq: "x' \<cdot> x = \<one>")
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    72
  inv_equality: "x\<inv> = x'"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    73
proof -
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    74
  have "x\<inv> = \<one> \<cdot> x\<inv>" by (simp only: left_one)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    75
  also have "\<dots> = (x' \<cdot> x) \<cdot> x\<inv>" by (simp only: eq)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    76
  also have "\<dots> = x' \<cdot> (x \<cdot> x\<inv>)" by (simp only: assoc)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    77
  also have "\<dots> = x' \<cdot> \<one>" by (simp only: right_inv)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    78
  also have "\<dots> = x'" by (simp only: right_one)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    79
  finally show ?thesis .
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    80
qed
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    81
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    82
theorem (in group)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    83
  inv_prod: "(x \<cdot> y)\<inv> = y\<inv> \<cdot> x\<inv>"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    84
proof (rule inv_equality)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    85
  show "(y\<inv> \<cdot> x\<inv>) \<cdot> (x \<cdot> y) = \<one>"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    86
  proof -
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    87
    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
    88
    also have "\<dots> = (y\<inv> \<cdot> \<one>) \<cdot> y" by (simp only: left_inv)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    89
    also have "\<dots> = y\<inv> \<cdot> y" by (simp only: right_one)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    90
    also have "\<dots> = \<one>" by (simp only: left_inv)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    91
    finally show ?thesis .
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    92
  qed
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    93
qed
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    94
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    95
theorem (in abelian_group)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    96
  inv_prod': "(x \<cdot> y)\<inv> = x\<inv> \<cdot> y\<inv>"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    97
proof -
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    98
  have "(x \<cdot> y)\<inv> = y\<inv> \<cdot> x\<inv>" by (rule inv_prod)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
    99
  also have "\<dots> = x\<inv> \<cdot> y\<inv>" by (rule commute)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   100
  finally show ?thesis .
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   101
qed
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   102
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   103
theorem (in group)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   104
  inv_inv: "(x\<inv>)\<inv> = x"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   105
proof (rule inv_equality)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   106
  show "x \<cdot> x\<inv> = \<one>" by (simp only: right_inv)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   107
qed
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   108
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   109
theorem (in group)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   110
  (assumes eq: "x\<inv> = y\<inv>")
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   111
  inv_inject: "x = y"
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   112
proof -
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   113
  have "x = x \<cdot> \<one>" by (simp only: right_one)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   114
  also have "\<dots> = x \<cdot> (y\<inv> \<cdot> y)" by (simp only: left_inv)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   115
  also have "\<dots> = x \<cdot> (x\<inv> \<cdot> y)" by (simp only: eq)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   116
  also have "\<dots> = (x \<cdot> x\<inv>) \<cdot> y" by (simp only: assoc)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   117
  also have "\<dots> = \<one> \<cdot> y" by (simp only: right_inv)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   118
  also have "\<dots> = y" by (simp only: left_one)
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   119
  finally show ?thesis .
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   120
qed
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   121
8d65dd96381f Locales and simple mathematical structures;
wenzelm
parents:
diff changeset
   122
end