src/ZF/ex/Group.thy
author wenzelm
Mon, 17 Sep 2007 16:36:41 +0200
changeset 24612 d1b315bdb8d7
parent 22931 11cc1ccad58e
child 26199 04817a8802f2
permissions -rw-r--r--
avoid direct access to print_mode;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
     1
(* Title:  ZF/ex/Group.thy
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
     2
  Id:     $Id$
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
     3
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
     4
*)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
     5
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
     6
header {* Groups *}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
     7
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14891
diff changeset
     8
theory Group imports Main begin
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
     9
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    10
text{*Based on work by Clemens Ballarin, Florian Kammueller, L C Paulson and
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    11
Markus Wenzel.*}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    12
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    13
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    14
subsection {* Monoids *}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    15
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    16
(*First, we must simulate a record declaration:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    17
record monoid = 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    18
  carrier :: i
14891
f2e9f7d813af fixed the groupI ambiguity
paulson
parents: 14884
diff changeset
    19
  mult :: "[i,i] => i" (infixl "\<cdot>\<index>" 70)
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    20
  one :: i ("\<one>\<index>")
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    21
*)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    22
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 19931
diff changeset
    23
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    24
  carrier :: "i => i" where
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 19931
diff changeset
    25
  "carrier(M) == fst(M)"
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    26
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    27
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    28
  mmult :: "[i, i, i] => i" (infixl "\<cdot>\<index>" 70) where
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 19931
diff changeset
    29
  "mmult(M,x,y) == fst(snd(M)) ` <x,y>"
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    30
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    31
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    32
  one :: "i => i" ("\<one>\<index>") where
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 19931
diff changeset
    33
  "one(M) == fst(snd(snd(M)))"
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    34
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    35
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    36
  update_carrier :: "[i,i] => i" where
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 19931
diff changeset
    37
  "update_carrier(M,A) == <A,snd(M)>"
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    38
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 19931
diff changeset
    39
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    40
  m_inv :: "i => i => i" ("inv\<index> _" [81] 80) where
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 19931
diff changeset
    41
  "inv\<^bsub>G\<^esub> x == (THE y. y \<in> carrier(G) & y \<cdot>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub> & x \<cdot>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub>)"
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    42
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    43
locale monoid = struct G +
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    44
  assumes m_closed [intro, simp]:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    45
         "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> x \<cdot> y \<in> carrier(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    46
      and m_assoc:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    47
         "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    48
          \<Longrightarrow> (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    49
      and one_closed [intro, simp]: "\<one> \<in> carrier(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    50
      and l_one [simp]: "x \<in> carrier(G) \<Longrightarrow> \<one> \<cdot> x = x"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    51
      and r_one [simp]: "x \<in> carrier(G) \<Longrightarrow> x \<cdot> \<one> = x"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    52
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    53
text{*Simulating the record*}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    54
lemma carrier_eq [simp]: "carrier(<A,Z>) = A"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    55
  by (simp add: carrier_def)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    56
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    57
lemma mult_eq [simp]: "mmult(<A,M,Z>, x, y) = M ` <x,y>"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    58
  by (simp add: mmult_def)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    59
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    60
lemma one_eq [simp]: "one(<A,M,I,Z>) = I"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    61
  by (simp add: one_def)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    62
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    63
lemma update_carrier_eq [simp]: "update_carrier(<A,Z>,B) = <B,Z>"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    64
  by (simp add: update_carrier_def)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    65
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    66
lemma carrier_update_carrier [simp]: "carrier(update_carrier(M,B)) = B"
22931
11cc1ccad58e tuned proofs;
wenzelm
parents: 21404
diff changeset
    67
  by (simp add: update_carrier_def) 
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    68
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    69
lemma mult_update_carrier [simp]: "mmult(update_carrier(M,B),x,y) = mmult(M,x,y)"
22931
11cc1ccad58e tuned proofs;
wenzelm
parents: 21404
diff changeset
    70
  by (simp add: update_carrier_def mmult_def) 
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    71
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    72
lemma one_update_carrier [simp]: "one(update_carrier(M,B)) = one(M)"
22931
11cc1ccad58e tuned proofs;
wenzelm
parents: 21404
diff changeset
    73
  by (simp add: update_carrier_def one_def) 
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    74
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    75
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    76
lemma (in monoid) inv_unique:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    77
  assumes eq: "y \<cdot> x = \<one>"  "x \<cdot> y' = \<one>"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    78
    and G: "x \<in> carrier(G)"  "y \<in> carrier(G)"  "y' \<in> carrier(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    79
  shows "y = y'"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    80
proof -
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    81
  from G eq have "y = y \<cdot> (x \<cdot> y')" by simp
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    82
  also from G have "... = (y \<cdot> x) \<cdot> y'" by (simp add: m_assoc)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    83
  also from G eq have "... = y'" by simp
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    84
  finally show ?thesis .
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    85
qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    86
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    87
text {*
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    88
  A group is a monoid all of whose elements are invertible.
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    89
*}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    90
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    91
locale group = monoid +
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    92
  assumes inv_ex:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    93
     "\<And>x. x \<in> carrier(G) \<Longrightarrow> \<exists>y \<in> carrier(G). y \<cdot> x = \<one> & x \<cdot> y = \<one>"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    94
22931
11cc1ccad58e tuned proofs;
wenzelm
parents: 21404
diff changeset
    95
lemma (in group) is_group [simp]: "group(G)" by fact
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    96
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    97
theorem groupI:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    98
  includes struct G
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
    99
  assumes m_closed [simp]:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   100
      "\<And>x y. \<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> x \<cdot> y \<in> carrier(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   101
    and one_closed [simp]: "\<one> \<in> carrier(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   102
    and m_assoc:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   103
      "\<And>x y z. \<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> \<Longrightarrow>
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   104
      (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   105
    and l_one [simp]: "\<And>x. x \<in> carrier(G) \<Longrightarrow> \<one> \<cdot> x = x"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   106
    and l_inv_ex: "\<And>x. x \<in> carrier(G) \<Longrightarrow> \<exists>y \<in> carrier(G). y \<cdot> x = \<one>"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   107
  shows "group(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   108
proof -
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   109
  have l_cancel [simp]:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   110
    "\<And>x y z. \<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> \<Longrightarrow>
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   111
    (x \<cdot> y = x \<cdot> z) <-> (y = z)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   112
  proof
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   113
    fix x y z
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   114
    assume G: "x \<in> carrier(G)"  "y \<in> carrier(G)"  "z \<in> carrier(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   115
    { 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   116
      assume eq: "x \<cdot> y = x \<cdot> z"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   117
      with G l_inv_ex obtain x_inv where xG: "x_inv \<in> carrier(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   118
	and l_inv: "x_inv \<cdot> x = \<one>" by fast
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   119
      from G eq xG have "(x_inv \<cdot> x) \<cdot> y = (x_inv \<cdot> x) \<cdot> z"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   120
	by (simp add: m_assoc)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   121
      with G show "y = z" by (simp add: l_inv)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   122
    next
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   123
      assume eq: "y = z"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   124
      with G show "x \<cdot> y = x \<cdot> z" by simp
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   125
    }
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   126
  qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   127
  have r_one:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   128
    "\<And>x. x \<in> carrier(G) \<Longrightarrow> x \<cdot> \<one> = x"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   129
  proof -
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   130
    fix x
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   131
    assume x: "x \<in> carrier(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   132
    with l_inv_ex obtain x_inv where xG: "x_inv \<in> carrier(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   133
      and l_inv: "x_inv \<cdot> x = \<one>" by fast
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   134
    from x xG have "x_inv \<cdot> (x \<cdot> \<one>) = x_inv \<cdot> x"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   135
      by (simp add: m_assoc [symmetric] l_inv)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   136
    with x xG show "x \<cdot> \<one> = x" by simp
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   137
  qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   138
  have inv_ex:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   139
    "!!x. x \<in> carrier(G) ==> \<exists>y \<in> carrier(G). y \<cdot> x = \<one> & x \<cdot> y = \<one>"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   140
  proof -
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   141
    fix x
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   142
    assume x: "x \<in> carrier(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   143
    with l_inv_ex obtain y where y: "y \<in> carrier(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   144
      and l_inv: "y \<cdot> x = \<one>" by fast
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   145
    from x y have "y \<cdot> (x \<cdot> y) = y \<cdot> \<one>"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   146
      by (simp add: m_assoc [symmetric] l_inv r_one)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   147
    with x y have r_inv: "x \<cdot> y = \<one>"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   148
      by simp
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   149
    from x y show "\<exists>y \<in> carrier(G). y \<cdot> x = \<one> & x \<cdot> y = \<one>"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   150
      by (fast intro: l_inv r_inv)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   151
  qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   152
  show ?thesis
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   153
    by (blast intro: group.intro monoid.intro group_axioms.intro 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   154
                     prems r_one inv_ex)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   155
qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   156
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   157
lemma (in group) inv [simp]:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   158
  "x \<in> carrier(G) \<Longrightarrow> inv x \<in> carrier(G) & inv x \<cdot> x = \<one> & x \<cdot> inv x = \<one>"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   159
  apply (frule inv_ex) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   160
  apply (unfold Bex_def m_inv_def)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   161
  apply (erule exE) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   162
  apply (rule theI)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   163
  apply (rule ex1I, assumption)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   164
   apply (blast intro: inv_unique)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   165
  done
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   166
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   167
lemma (in group) inv_closed [intro!]:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   168
  "x \<in> carrier(G) \<Longrightarrow> inv x \<in> carrier(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   169
  by simp
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   170
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   171
lemma (in group) l_inv:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   172
  "x \<in> carrier(G) \<Longrightarrow> inv x \<cdot> x = \<one>"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   173
  by simp
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   174
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   175
lemma (in group) r_inv:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   176
  "x \<in> carrier(G) \<Longrightarrow> x \<cdot> inv x = \<one>"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   177
  by simp
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   178
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   179
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   180
subsection {* Cancellation Laws and Basic Properties *}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   181
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   182
lemma (in group) l_cancel [simp]:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   183
  assumes [simp]: "x \<in> carrier(G)" "y \<in> carrier(G)" "z \<in> carrier(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   184
  shows "(x \<cdot> y = x \<cdot> z) <-> (y = z)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   185
proof
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   186
  assume eq: "x \<cdot> y = x \<cdot> z"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   187
  hence  "(inv x \<cdot> x) \<cdot> y = (inv x \<cdot> x) \<cdot> z"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   188
    by (simp only: m_assoc inv_closed prems)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   189
  thus "y = z" by simp
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   190
next
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   191
  assume eq: "y = z"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   192
  then show "x \<cdot> y = x \<cdot> z" by simp
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   193
qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   194
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   195
lemma (in group) r_cancel [simp]:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   196
  assumes [simp]: "x \<in> carrier(G)" "y \<in> carrier(G)" "z \<in> carrier(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   197
  shows "(y \<cdot> x = z \<cdot> x) <-> (y = z)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   198
proof
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   199
  assume eq: "y \<cdot> x = z \<cdot> x"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   200
  then have "y \<cdot> (x \<cdot> inv x) = z \<cdot> (x \<cdot> inv x)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   201
    by (simp only: m_assoc [symmetric] inv_closed prems)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   202
  thus "y = z" by simp
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   203
next
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   204
  assume eq: "y = z"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   205
  thus  "y \<cdot> x = z \<cdot> x" by simp
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   206
qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   207
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   208
lemma (in group) inv_comm:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   209
  assumes inv: "x \<cdot> y = \<one>"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   210
      and G: "x \<in> carrier(G)"  "y \<in> carrier(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   211
  shows "y \<cdot> x = \<one>"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   212
proof -
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   213
  from G have "x \<cdot> y \<cdot> x = x \<cdot> \<one>" by (auto simp add: inv)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   214
  with G show ?thesis by (simp del: r_one add: m_assoc)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   215
qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   216
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   217
lemma (in group) inv_equality:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   218
     "\<lbrakk>y \<cdot> x = \<one>; x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> inv x = y"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   219
apply (simp add: m_inv_def)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   220
apply (rule the_equality)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   221
 apply (simp add: inv_comm [of y x])
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   222
apply (rule r_cancel [THEN iffD1], auto)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   223
done
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   224
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   225
lemma (in group) inv_one [simp]:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   226
  "inv \<one> = \<one>"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   227
  by (auto intro: inv_equality) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   228
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   229
lemma (in group) inv_inv [simp]: "x \<in> carrier(G) \<Longrightarrow> inv (inv x) = x"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   230
  by (auto intro: inv_equality) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   231
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   232
text{*This proof is by cancellation*}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   233
lemma (in group) inv_mult_group:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   234
  "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> inv (x \<cdot> y) = inv y \<cdot> inv x"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   235
proof -
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   236
  assume G: "x \<in> carrier(G)"  "y \<in> carrier(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   237
  then have "inv (x \<cdot> y) \<cdot> (x \<cdot> y) = (inv y \<cdot> inv x) \<cdot> (x \<cdot> y)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   238
    by (simp add: m_assoc l_inv) (simp add: m_assoc [symmetric] l_inv)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   239
  with G show ?thesis by (simp_all del: inv add: inv_closed)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   240
qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   241
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   242
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   243
subsection {* Substructures *}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   244
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   245
locale subgroup = var H + struct G + 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   246
  assumes subset: "H \<subseteq> carrier(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   247
    and m_closed [intro, simp]: "\<lbrakk>x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> x \<cdot> y \<in> H"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   248
    and  one_closed [simp]: "\<one> \<in> H"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   249
    and m_inv_closed [intro,simp]: "x \<in> H \<Longrightarrow> inv x \<in> H"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   250
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   251
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   252
lemma (in subgroup) mem_carrier [simp]:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   253
  "x \<in> H \<Longrightarrow> x \<in> carrier(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   254
  using subset by blast
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   255
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   256
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   257
lemma subgroup_imp_subset:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   258
  "subgroup(H,G) \<Longrightarrow> H \<subseteq> carrier(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   259
  by (rule subgroup.subset)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   260
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   261
lemma (in subgroup) group_axiomsI [intro]:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   262
  includes group G
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   263
  shows "group_axioms (update_carrier(G,H))"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   264
by (force intro: group_axioms.intro l_inv r_inv) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   265
14891
f2e9f7d813af fixed the groupI ambiguity
paulson
parents: 14884
diff changeset
   266
lemma (in subgroup) is_group [intro]:
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   267
  includes group G
14891
f2e9f7d813af fixed the groupI ambiguity
paulson
parents: 14884
diff changeset
   268
  shows "group (update_carrier(G,H))"
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   269
  by (rule groupI) (auto intro: m_assoc l_inv mem_carrier)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   270
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   271
text {*
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   272
  Since @{term H} is nonempty, it contains some element @{term x}.  Since
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   273
  it is closed under inverse, it contains @{text "inv x"}.  Since
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   274
  it is closed under product, it contains @{text "x \<cdot> inv x = \<one>"}.
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   275
*}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   276
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   277
text {*
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   278
  Since @{term H} is nonempty, it contains some element @{term x}.  Since
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   279
  it is closed under inverse, it contains @{text "inv x"}.  Since
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   280
  it is closed under product, it contains @{text "x \<cdot> inv x = \<one>"}.
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   281
*}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   282
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   283
lemma (in group) one_in_subset:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   284
  "\<lbrakk>H \<subseteq> carrier(G); H \<noteq> 0; \<forall>a \<in> H. inv a \<in> H; \<forall>a\<in>H. \<forall>b\<in>H. a \<cdot> b \<in> H\<rbrakk>
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   285
   \<Longrightarrow> \<one> \<in> H"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   286
by (force simp add: l_inv)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   287
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   288
text {* A characterization of subgroups: closed, non-empty subset. *}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   289
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   290
declare monoid.one_closed [simp] group.inv_closed [simp]
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   291
  monoid.l_one [simp] monoid.r_one [simp] group.inv_inv [simp]
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   292
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   293
lemma subgroup_nonempty:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   294
  "~ subgroup(0,G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   295
  by (blast dest: subgroup.one_closed)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   296
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   297
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   298
subsection {* Direct Products *}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   299
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 19931
diff changeset
   300
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   301
  DirProdGroup :: "[i,i] => i"  (infixr "\<Otimes>" 80) where
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   302
  "G \<Otimes> H == <carrier(G) \<times> carrier(H),
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   303
              (\<lambda><<g,h>, <g', h'>>
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   304
                   \<in> (carrier(G) \<times> carrier(H)) \<times> (carrier(G) \<times> carrier(H)).
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   305
                <g \<cdot>\<^bsub>G\<^esub> g', h \<cdot>\<^bsub>H\<^esub> h'>),
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   306
              <\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>>, 0>"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   307
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   308
lemma DirProdGroup_group:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   309
  includes group G + group H
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   310
  shows "group (G \<Otimes> H)"
22931
11cc1ccad58e tuned proofs;
wenzelm
parents: 21404
diff changeset
   311
  by (force intro!: groupI G.m_assoc H.m_assoc G.l_inv H.l_inv
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   312
          simp add: DirProdGroup_def)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   313
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   314
lemma carrier_DirProdGroup [simp]:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   315
     "carrier (G \<Otimes> H) = carrier(G) \<times> carrier(H)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   316
  by (simp add: DirProdGroup_def)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   317
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   318
lemma one_DirProdGroup [simp]:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   319
     "\<one>\<^bsub>G \<Otimes> H\<^esub> = <\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>>"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   320
  by (simp add: DirProdGroup_def)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   321
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   322
lemma mult_DirProdGroup [simp]:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   323
     "[|g \<in> carrier(G); h \<in> carrier(H); g' \<in> carrier(G); h' \<in> carrier(H)|]
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   324
      ==> <g, h> \<cdot>\<^bsub>G \<Otimes> H\<^esub> <g', h'> = <g \<cdot>\<^bsub>G\<^esub> g', h \<cdot>\<^bsub>H\<^esub> h'>"
22931
11cc1ccad58e tuned proofs;
wenzelm
parents: 21404
diff changeset
   325
  by (simp add: DirProdGroup_def)
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   326
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   327
lemma inv_DirProdGroup [simp]:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   328
  includes group G + group H
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   329
  assumes g: "g \<in> carrier(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   330
      and h: "h \<in> carrier(H)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   331
  shows "inv \<^bsub>G \<Otimes> H\<^esub> <g, h> = <inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h>"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   332
  apply (rule group.inv_equality [OF DirProdGroup_group])
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 16417
diff changeset
   333
  apply (simp_all add: prems group.l_inv)
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   334
  done
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   335
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   336
subsection {* Isomorphisms *}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   337
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 19931
diff changeset
   338
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   339
  hom :: "[i,i] => i" where
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   340
  "hom(G,H) ==
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   341
    {h \<in> carrier(G) -> carrier(H).
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   342
      (\<forall>x \<in> carrier(G). \<forall>y \<in> carrier(G). h ` (x \<cdot>\<^bsub>G\<^esub> y) = (h ` x) \<cdot>\<^bsub>H\<^esub> (h ` y))}"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   343
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   344
lemma hom_mult:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   345
  "\<lbrakk>h \<in> hom(G,H); x \<in> carrier(G); y \<in> carrier(G)\<rbrakk>
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   346
   \<Longrightarrow> h ` (x \<cdot>\<^bsub>G\<^esub> y) = h ` x \<cdot>\<^bsub>H\<^esub> h ` y"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   347
  by (simp add: hom_def)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   348
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   349
lemma hom_closed:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   350
  "\<lbrakk>h \<in> hom(G,H); x \<in> carrier(G)\<rbrakk> \<Longrightarrow> h ` x \<in> carrier(H)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   351
  by (auto simp add: hom_def)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   352
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   353
lemma (in group) hom_compose:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   354
     "\<lbrakk>h \<in> hom(G,H); i \<in> hom(H,I)\<rbrakk> \<Longrightarrow> i O h \<in> hom(G,I)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   355
by (force simp add: hom_def comp_fun) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   356
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   357
lemma hom_is_fun:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   358
  "h \<in> hom(G,H) \<Longrightarrow> h \<in> carrier(G) -> carrier(H)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   359
  by (simp add: hom_def)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   360
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   361
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   362
subsection {* Isomorphisms *}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   363
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 19931
diff changeset
   364
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   365
  iso :: "[i,i] => i"  (infixr "\<cong>" 60) where
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   366
  "G \<cong> H == hom(G,H) \<inter> bij(carrier(G), carrier(H))"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   367
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   368
lemma (in group) iso_refl: "id(carrier(G)) \<in> G \<cong> G"
22931
11cc1ccad58e tuned proofs;
wenzelm
parents: 21404
diff changeset
   369
  by (simp add: iso_def hom_def id_type id_bij) 
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   370
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   371
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   372
lemma (in group) iso_sym:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   373
     "h \<in> G \<cong> H \<Longrightarrow> converse(h) \<in> H \<cong> G"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   374
apply (simp add: iso_def bij_converse_bij, clarify) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   375
apply (subgoal_tac "converse(h) \<in> carrier(H) \<rightarrow> carrier(G)") 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   376
 prefer 2 apply (simp add: bij_converse_bij bij_is_fun) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   377
apply (auto intro: left_inverse_eq [of _ "carrier(G)" "carrier(H)"] 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   378
            simp add: hom_def bij_is_inj right_inverse_bij); 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   379
done
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   380
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   381
lemma (in group) iso_trans: 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   382
     "\<lbrakk>h \<in> G \<cong> H; i \<in> H \<cong> I\<rbrakk> \<Longrightarrow> i O h \<in> G \<cong> I"
22931
11cc1ccad58e tuned proofs;
wenzelm
parents: 21404
diff changeset
   383
  by (auto simp add: iso_def hom_compose comp_bij)
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   384
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   385
lemma DirProdGroup_commute_iso:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   386
  includes group G + group H
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   387
  shows "(\<lambda><x,y> \<in> carrier(G \<Otimes> H). <y,x>) \<in> (G \<Otimes> H) \<cong> (H \<Otimes> G)"
22931
11cc1ccad58e tuned proofs;
wenzelm
parents: 21404
diff changeset
   388
  by (auto simp add: iso_def hom_def inj_def surj_def bij_def) 
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   389
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   390
lemma DirProdGroup_assoc_iso:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   391
  includes group G + group H + group I
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   392
  shows "(\<lambda><<x,y>,z> \<in> carrier((G \<Otimes> H) \<Otimes> I). <x,<y,z>>)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   393
          \<in> ((G \<Otimes> H) \<Otimes> I) \<cong> (G \<Otimes> (H \<Otimes> I))"
22931
11cc1ccad58e tuned proofs;
wenzelm
parents: 21404
diff changeset
   394
  by (auto intro: lam_type simp add: iso_def hom_def inj_def surj_def bij_def) 
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   395
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   396
text{*Basis for homomorphism proofs: we assume two groups @{term G} and
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   397
  @term{H}, with a homomorphism @{term h} between them*}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   398
locale group_hom = group G + group H + var h +
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   399
  assumes homh: "h \<in> hom(G,H)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   400
  notes hom_mult [simp] = hom_mult [OF homh]
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   401
    and hom_closed [simp] = hom_closed [OF homh]
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   402
    and hom_is_fun [simp] = hom_is_fun [OF homh]
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   403
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   404
lemma (in group_hom) one_closed [simp]:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   405
  "h ` \<one> \<in> carrier(H)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   406
  by simp
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   407
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   408
lemma (in group_hom) hom_one [simp]:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   409
  "h ` \<one> = \<one>\<^bsub>H\<^esub>"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   410
proof -
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   411
  have "h ` \<one> \<cdot>\<^bsub>H\<^esub> \<one>\<^bsub>H\<^esub> = (h ` \<one>) \<cdot>\<^bsub>H\<^esub> (h ` \<one>)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   412
    by (simp add: hom_mult [symmetric] del: hom_mult)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   413
  then show ?thesis by (simp del: r_one)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   414
qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   415
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   416
lemma (in group_hom) inv_closed [simp]:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   417
  "x \<in> carrier(G) \<Longrightarrow> h ` (inv x) \<in> carrier(H)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   418
  by simp
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   419
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   420
lemma (in group_hom) hom_inv [simp]:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   421
  "x \<in> carrier(G) \<Longrightarrow> h ` (inv x) = inv\<^bsub>H\<^esub> (h ` x)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   422
proof -
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   423
  assume x: "x \<in> carrier(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   424
  then have "h ` x \<cdot>\<^bsub>H\<^esub> h ` (inv x) = \<one>\<^bsub>H\<^esub>"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   425
    by (simp add: hom_mult [symmetric] G.r_inv del: hom_mult)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   426
  also from x have "... = h ` x \<cdot>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h ` x)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   427
    by (simp add: hom_mult [symmetric] H.r_inv del: hom_mult)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   428
  finally have "h ` x \<cdot>\<^bsub>H\<^esub> h ` (inv x) = h ` x \<cdot>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h ` x)" .
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   429
  with x show ?thesis by (simp del: inv add: is_group)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   430
qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   431
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   432
subsection {* Commutative Structures *}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   433
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   434
text {*
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   435
  Naming convention: multiplicative structures that are commutative
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   436
  are called \emph{commutative}, additive structures are called
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   437
  \emph{Abelian}.
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   438
*}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   439
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   440
subsection {* Definition *}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   441
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   442
locale comm_monoid = monoid +
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   443
  assumes m_comm: "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> x \<cdot> y = y \<cdot> x"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   444
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   445
lemma (in comm_monoid) m_lcomm:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   446
  "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> \<Longrightarrow>
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   447
   x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   448
proof -
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   449
  assume xyz: "x \<in> carrier(G)"  "y \<in> carrier(G)"  "z \<in> carrier(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   450
  from xyz have "x \<cdot> (y \<cdot> z) = (x \<cdot> y) \<cdot> z" by (simp add: m_assoc)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   451
  also from xyz have "... = (y \<cdot> x) \<cdot> z" by (simp add: m_comm)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   452
  also from xyz have "... = y \<cdot> (x \<cdot> z)" by (simp add: m_assoc)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   453
  finally show ?thesis .
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   454
qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   455
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   456
lemmas (in comm_monoid) m_ac = m_assoc m_comm m_lcomm
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   457
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   458
locale comm_group = comm_monoid + group
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   459
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   460
lemma (in comm_group) inv_mult:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   461
  "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> inv (x \<cdot> y) = inv x \<cdot> inv y"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   462
  by (simp add: m_ac inv_mult_group)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   463
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   464
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   465
lemma (in group) subgroup_self: "subgroup (carrier(G),G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   466
by (simp add: subgroup_def prems) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   467
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   468
lemma (in group) subgroup_imp_group:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   469
  "subgroup(H,G) \<Longrightarrow> group (update_carrier(G,H))"
14891
f2e9f7d813af fixed the groupI ambiguity
paulson
parents: 14884
diff changeset
   470
by (simp add: subgroup.is_group)
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   471
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   472
lemma (in group) subgroupI:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   473
  assumes subset: "H \<subseteq> carrier(G)" and non_empty: "H \<noteq> 0"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   474
    and inv: "!!a. a \<in> H ==> inv a \<in> H"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   475
    and mult: "!!a b. [|a \<in> H; b \<in> H|] ==> a \<cdot> b \<in> H"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   476
  shows "subgroup(H,G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   477
proof (simp add: subgroup_def prems)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   478
  show "\<one> \<in> H" by (rule one_in_subset) (auto simp only: prems)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   479
qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   480
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   481
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   482
subsection {* Bijections of a Set, Permutation Groups, Automorphism Groups *}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   483
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 19931
diff changeset
   484
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   485
  BijGroup :: "i=>i" where
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   486
  "BijGroup(S) ==
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   487
    <bij(S,S),
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   488
     \<lambda><g,f> \<in> bij(S,S) \<times> bij(S,S). g O f,
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   489
     id(S), 0>"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   490
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   491
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   492
subsection {*Bijections Form a Group *}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   493
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   494
theorem group_BijGroup: "group(BijGroup(S))"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   495
apply (simp add: BijGroup_def)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   496
apply (rule groupI) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   497
    apply (simp_all add: id_bij comp_bij comp_assoc) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   498
 apply (simp add: id_bij bij_is_fun left_comp_id [of _ S S] fun_is_rel)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   499
apply (blast intro: left_comp_inverse bij_is_inj bij_converse_bij)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   500
done
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   501
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   502
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   503
subsection{*Automorphisms Form a Group*}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   504
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   505
lemma Bij_Inv_mem: "\<lbrakk>f \<in> bij(S,S);  x \<in> S\<rbrakk> \<Longrightarrow> converse(f) ` x \<in> S" 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   506
by (blast intro: apply_funtype bij_is_fun bij_converse_bij)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   507
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   508
lemma inv_BijGroup: "f \<in> bij(S,S) \<Longrightarrow> m_inv (BijGroup(S), f) = converse(f)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   509
apply (rule group.inv_equality)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   510
apply (rule group_BijGroup)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   511
apply (simp_all add: BijGroup_def bij_converse_bij 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   512
          left_comp_inverse [OF bij_is_inj]) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   513
done
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   514
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   515
lemma iso_is_bij: "h \<in> G \<cong> H ==> h \<in> bij(carrier(G), carrier(H))"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   516
by (simp add: iso_def)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   517
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   518
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 19931
diff changeset
   519
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   520
  auto :: "i=>i" where
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   521
  "auto(G) == iso(G,G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   522
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   523
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   524
  AutoGroup :: "i=>i" where
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   525
  "AutoGroup(G) == update_carrier(BijGroup(carrier(G)), auto(G))"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   526
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   527
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   528
lemma (in group) id_in_auto: "id(carrier(G)) \<in> auto(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   529
  by (simp add: iso_refl auto_def)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   530
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   531
lemma (in group) subgroup_auto:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   532
      "subgroup (auto(G)) (BijGroup (carrier(G)))"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   533
proof (rule subgroup.intro)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   534
  show "auto(G) \<subseteq> carrier (BijGroup (carrier(G)))"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   535
    by (auto simp add: auto_def BijGroup_def iso_def)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   536
next
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   537
  fix x y
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   538
  assume "x \<in> auto(G)" "y \<in> auto(G)" 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   539
  thus "x \<cdot>\<^bsub>BijGroup (carrier(G))\<^esub> y \<in> auto(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   540
    by (auto simp add: BijGroup_def auto_def iso_def bij_is_fun 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   541
                       group.hom_compose comp_bij)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   542
next
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   543
  show "\<one>\<^bsub>BijGroup (carrier(G))\<^esub> \<in> auto(G)" by (simp add:  BijGroup_def id_in_auto)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   544
next
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   545
  fix x 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   546
  assume "x \<in> auto(G)" 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   547
  thus "inv\<^bsub>BijGroup (carrier(G))\<^esub> x \<in> auto(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   548
    by (simp add: auto_def inv_BijGroup iso_is_bij iso_sym) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   549
qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   550
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   551
theorem (in group) AutoGroup: "group (AutoGroup(G))"
14891
f2e9f7d813af fixed the groupI ambiguity
paulson
parents: 14884
diff changeset
   552
by (simp add: AutoGroup_def subgroup.is_group subgroup_auto group_BijGroup)
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   553
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   554
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   555
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   556
subsection{*Cosets and Quotient Groups*}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   557
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 19931
diff changeset
   558
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   559
  r_coset  :: "[i,i,i] => i"  (infixl "#>\<index>" 60) where
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 19931
diff changeset
   560
  "H #>\<^bsub>G\<^esub> a == \<Union>h\<in>H. {h \<cdot>\<^bsub>G\<^esub> a}"
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   561
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   562
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   563
  l_coset  :: "[i,i,i] => i"  (infixl "<#\<index>" 60) where
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 19931
diff changeset
   564
  "a <#\<^bsub>G\<^esub> H == \<Union>h\<in>H. {a \<cdot>\<^bsub>G\<^esub> h}"
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   565
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   566
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   567
  RCOSETS  :: "[i,i] => i"  ("rcosets\<index> _" [81] 80) where
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 19931
diff changeset
   568
  "rcosets\<^bsub>G\<^esub> H == \<Union>a\<in>carrier(G). {H #>\<^bsub>G\<^esub> a}"
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   569
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   570
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   571
  set_mult :: "[i,i,i] => i"  (infixl "<#>\<index>" 60) where
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 19931
diff changeset
   572
  "H <#>\<^bsub>G\<^esub> K == \<Union>h\<in>H. \<Union>k\<in>K. {h \<cdot>\<^bsub>G\<^esub> k}"
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   573
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   574
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   575
  SET_INV  :: "[i,i] => i"  ("set'_inv\<index> _" [81] 80) where
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 19931
diff changeset
   576
  "set_inv\<^bsub>G\<^esub> H == \<Union>h\<in>H. {inv\<^bsub>G\<^esub> h}"
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   577
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   578
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   579
locale normal = subgroup + group +
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   580
  assumes coset_eq: "(\<forall>x \<in> carrier(G). H #> x = x <# H)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   581
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 19931
diff changeset
   582
notation
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 19931
diff changeset
   583
  normal  (infixl "\<lhd>" 60)
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   584
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   585
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   586
subsection {*Basic Properties of Cosets*}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   587
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   588
lemma (in group) coset_mult_assoc:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   589
     "\<lbrakk>M \<subseteq> carrier(G); g \<in> carrier(G); h \<in> carrier(G)\<rbrakk>
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   590
      \<Longrightarrow> (M #> g) #> h = M #> (g \<cdot> h)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   591
by (force simp add: r_coset_def m_assoc)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   592
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   593
lemma (in group) coset_mult_one [simp]: "M \<subseteq> carrier(G) \<Longrightarrow> M #> \<one> = M"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   594
by (force simp add: r_coset_def)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   595
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   596
lemma (in group) solve_equation:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   597
    "\<lbrakk>subgroup(H,G); x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> \<exists>h\<in>H. y = h \<cdot> x"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   598
apply (rule bexI [of _ "y \<cdot> (inv x)"])
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   599
apply (auto simp add: subgroup.m_closed subgroup.m_inv_closed m_assoc
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   600
                      subgroup.subset [THEN subsetD])
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   601
done
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   602
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   603
lemma (in group) repr_independence:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   604
     "\<lbrakk>y \<in> H #> x;  x \<in> carrier(G); subgroup(H,G)\<rbrakk> \<Longrightarrow> H #> x = H #> y"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   605
by (auto simp add: r_coset_def m_assoc [symmetric]
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   606
                   subgroup.subset [THEN subsetD]
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   607
                   subgroup.m_closed solve_equation)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   608
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   609
lemma (in group) coset_join2:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   610
     "\<lbrakk>x \<in> carrier(G);  subgroup(H,G);  x\<in>H\<rbrakk> \<Longrightarrow> H #> x = H"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   611
  --{*Alternative proof is to put @{term "x=\<one>"} in @{text repr_independence}.*}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   612
by (force simp add: subgroup.m_closed r_coset_def solve_equation)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   613
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   614
lemma (in group) r_coset_subset_G:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   615
     "\<lbrakk>H \<subseteq> carrier(G); x \<in> carrier(G)\<rbrakk> \<Longrightarrow> H #> x \<subseteq> carrier(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   616
by (auto simp add: r_coset_def)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   617
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   618
lemma (in group) rcosI:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   619
     "\<lbrakk>h \<in> H; H \<subseteq> carrier(G); x \<in> carrier(G)\<rbrakk> \<Longrightarrow> h \<cdot> x \<in> H #> x"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   620
by (auto simp add: r_coset_def)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   621
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   622
lemma (in group) rcosetsI:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   623
     "\<lbrakk>H \<subseteq> carrier(G); x \<in> carrier(G)\<rbrakk> \<Longrightarrow> H #> x \<in> rcosets H"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   624
by (auto simp add: RCOSETS_def)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   625
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   626
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   627
text{*Really needed?*}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   628
lemma (in group) transpose_inv:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   629
     "\<lbrakk>x \<cdot> y = z;  x \<in> carrier(G);  y \<in> carrier(G);  z \<in> carrier(G)\<rbrakk>
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   630
      \<Longrightarrow> (inv x) \<cdot> z = y"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   631
by (force simp add: m_assoc [symmetric])
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   632
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   633
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   634
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   635
subsection {* Normal subgroups *}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   636
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   637
lemma normal_imp_subgroup: "H \<lhd> G ==> subgroup(H,G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   638
  by (simp add: normal_def subgroup_def)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   639
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   640
lemma (in group) normalI: 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   641
  "subgroup(H,G) \<Longrightarrow> (\<forall>x \<in> carrier(G). H #> x = x <# H) \<Longrightarrow> H \<lhd> G";
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 16417
diff changeset
   642
  by (simp add: normal_def normal_axioms_def)
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   643
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   644
lemma (in normal) inv_op_closed1:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   645
     "\<lbrakk>x \<in> carrier(G); h \<in> H\<rbrakk> \<Longrightarrow> (inv x) \<cdot> h \<cdot> x \<in> H"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   646
apply (insert coset_eq) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   647
apply (auto simp add: l_coset_def r_coset_def)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   648
apply (drule bspec, assumption)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   649
apply (drule equalityD1 [THEN subsetD], blast, clarify)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   650
apply (simp add: m_assoc)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   651
apply (simp add: m_assoc [symmetric])
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   652
done
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   653
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   654
lemma (in normal) inv_op_closed2:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   655
     "\<lbrakk>x \<in> carrier(G); h \<in> H\<rbrakk> \<Longrightarrow> x \<cdot> h \<cdot> (inv x) \<in> H"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   656
apply (subgoal_tac "inv (inv x) \<cdot> h \<cdot> (inv x) \<in> H") 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   657
apply simp 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   658
apply (blast intro: inv_op_closed1) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   659
done
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   660
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   661
text{*Alternative characterization of normal subgroups*}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   662
lemma (in group) normal_inv_iff:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   663
     "(N \<lhd> G) <->
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   664
      (subgroup(N,G) & (\<forall>x \<in> carrier(G). \<forall>h \<in> N. x \<cdot> h \<cdot> (inv x) \<in> N))"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   665
      (is "_ <-> ?rhs")
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   666
proof
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   667
  assume N: "N \<lhd> G"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   668
  show ?rhs
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   669
    by (blast intro: N normal.inv_op_closed2 normal_imp_subgroup) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   670
next
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   671
  assume ?rhs
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   672
  hence sg: "subgroup(N,G)" 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   673
    and closed: "\<And>x. x\<in>carrier(G) \<Longrightarrow> \<forall>h\<in>N. x \<cdot> h \<cdot> inv x \<in> N" by auto
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   674
  hence sb: "N \<subseteq> carrier(G)" by (simp add: subgroup.subset) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   675
  show "N \<lhd> G"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   676
  proof (intro normalI [OF sg], simp add: l_coset_def r_coset_def, clarify)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   677
    fix x
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   678
    assume x: "x \<in> carrier(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   679
    show "(\<Union>h\<in>N. {h \<cdot> x}) = (\<Union>h\<in>N. {x \<cdot> h})"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   680
    proof
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   681
      show "(\<Union>h\<in>N. {h \<cdot> x}) \<subseteq> (\<Union>h\<in>N. {x \<cdot> h})"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   682
      proof clarify
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   683
        fix n
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   684
        assume n: "n \<in> N" 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   685
        show "n \<cdot> x \<in> (\<Union>h\<in>N. {x \<cdot> h})"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   686
        proof (rule UN_I) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   687
          from closed [of "inv x"]
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   688
          show "inv x \<cdot> n \<cdot> x \<in> N" by (simp add: x n)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   689
          show "n \<cdot> x \<in> {x \<cdot> (inv x \<cdot> n \<cdot> x)}"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   690
            by (simp add: x n m_assoc [symmetric] sb [THEN subsetD])
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   691
        qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   692
      qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   693
    next
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   694
      show "(\<Union>h\<in>N. {x \<cdot> h}) \<subseteq> (\<Union>h\<in>N. {h \<cdot> x})"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   695
      proof clarify
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   696
        fix n
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   697
        assume n: "n \<in> N" 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   698
        show "x \<cdot> n \<in> (\<Union>h\<in>N. {h \<cdot> x})"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   699
        proof (rule UN_I) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   700
          show "x \<cdot> n \<cdot> inv x \<in> N" by (simp add: x n closed)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   701
          show "x \<cdot> n \<in> {x \<cdot> n \<cdot> inv x \<cdot> x}"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   702
            by (simp add: x n m_assoc sb [THEN subsetD])
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   703
        qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   704
      qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   705
    qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   706
  qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   707
qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   708
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   709
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   710
subsection{*More Properties of Cosets*}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   711
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   712
lemma (in group) l_coset_subset_G:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   713
     "\<lbrakk>H \<subseteq> carrier(G); x \<in> carrier(G)\<rbrakk> \<Longrightarrow> x <# H \<subseteq> carrier(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   714
by (auto simp add: l_coset_def subsetD)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   715
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   716
lemma (in group) l_coset_swap:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   717
     "\<lbrakk>y \<in> x <# H;  x \<in> carrier(G);  subgroup(H,G)\<rbrakk> \<Longrightarrow> x \<in> y <# H"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   718
proof (simp add: l_coset_def)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   719
  assume "\<exists>h\<in>H. y = x \<cdot> h"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   720
    and x: "x \<in> carrier(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   721
    and sb: "subgroup(H,G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   722
  then obtain h' where h': "h' \<in> H & x \<cdot> h' = y" by blast
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   723
  show "\<exists>h\<in>H. x = y \<cdot> h"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   724
  proof
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   725
    show "x = y \<cdot> inv h'" using h' x sb
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   726
      by (auto simp add: m_assoc subgroup.subset [THEN subsetD])
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   727
    show "inv h' \<in> H" using h' sb
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   728
      by (auto simp add: subgroup.subset [THEN subsetD] subgroup.m_inv_closed)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   729
  qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   730
qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   731
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   732
lemma (in group) l_coset_carrier:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   733
     "\<lbrakk>y \<in> x <# H;  x \<in> carrier(G);  subgroup(H,G)\<rbrakk> \<Longrightarrow> y \<in> carrier(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   734
by (auto simp add: l_coset_def m_assoc
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   735
                   subgroup.subset [THEN subsetD] subgroup.m_closed)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   736
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   737
lemma (in group) l_repr_imp_subset:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   738
  assumes y: "y \<in> x <# H" and x: "x \<in> carrier(G)" and sb: "subgroup(H,G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   739
  shows "y <# H \<subseteq> x <# H"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   740
proof -
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   741
  from y
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   742
  obtain h' where "h' \<in> H" "x \<cdot> h' = y" by (auto simp add: l_coset_def)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   743
  thus ?thesis using x sb
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   744
    by (auto simp add: l_coset_def m_assoc
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   745
                       subgroup.subset [THEN subsetD] subgroup.m_closed)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   746
qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   747
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   748
lemma (in group) l_repr_independence:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   749
  assumes y: "y \<in> x <# H" and x: "x \<in> carrier(G)" and sb: "subgroup(H,G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   750
  shows "x <# H = y <# H"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   751
proof
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   752
  show "x <# H \<subseteq> y <# H"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   753
    by (rule l_repr_imp_subset,
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   754
        (blast intro: l_coset_swap l_coset_carrier y x sb)+)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   755
  show "y <# H \<subseteq> x <# H" by (rule l_repr_imp_subset [OF y x sb])
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   756
qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   757
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   758
lemma (in group) setmult_subset_G:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   759
     "\<lbrakk>H \<subseteq> carrier(G); K \<subseteq> carrier(G)\<rbrakk> \<Longrightarrow> H <#> K \<subseteq> carrier(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   760
by (auto simp add: set_mult_def subsetD)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   761
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   762
lemma (in group) subgroup_mult_id: "subgroup(H,G) \<Longrightarrow> H <#> H = H"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   763
apply (rule equalityI) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   764
apply (auto simp add: subgroup.m_closed set_mult_def Sigma_def image_def)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   765
apply (rule_tac x = x in bexI)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   766
apply (rule bexI [of _ "\<one>"])
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   767
apply (auto simp add: subgroup.m_closed subgroup.one_closed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   768
                      r_one subgroup.subset [THEN subsetD])
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   769
done
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   770
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   771
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   772
subsubsection {* Set of inverses of an @{text r_coset}. *}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   773
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   774
lemma (in normal) rcos_inv:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   775
  assumes x:     "x \<in> carrier(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   776
  shows "set_inv (H #> x) = H #> (inv x)" 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   777
proof (simp add: r_coset_def SET_INV_def x inv_mult_group, safe intro!: equalityI)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   778
  fix h
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   779
  assume "h \<in> H"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   780
  show "inv x \<cdot> inv h \<in> (\<Union>j\<in>H. {j \<cdot> inv x})"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   781
  proof (rule UN_I)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   782
    show "inv x \<cdot> inv h \<cdot> x \<in> H"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   783
      by (simp add: inv_op_closed1 prems)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   784
    show "inv x \<cdot> inv h \<in> {inv x \<cdot> inv h \<cdot> x \<cdot> inv x}"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   785
      by (simp add: prems m_assoc)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   786
  qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   787
next
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   788
  fix h
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   789
  assume "h \<in> H"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   790
  show "h \<cdot> inv x \<in> (\<Union>j\<in>H. {inv x \<cdot> inv j})"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   791
  proof (rule UN_I)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   792
    show "x \<cdot> inv h \<cdot> inv x \<in> H"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   793
      by (simp add: inv_op_closed2 prems)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   794
    show "h \<cdot> inv x \<in> {inv x \<cdot> inv (x \<cdot> inv h \<cdot> inv x)}"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   795
      by (simp add: prems m_assoc [symmetric] inv_mult_group)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   796
  qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   797
qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   798
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   799
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   800
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   801
subsubsection {*Theorems for @{text "<#>"} with @{text "#>"} or @{text "<#"}.*}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   802
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   803
lemma (in group) setmult_rcos_assoc:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   804
     "\<lbrakk>H \<subseteq> carrier(G); K \<subseteq> carrier(G); x \<in> carrier(G)\<rbrakk>
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   805
      \<Longrightarrow> H <#> (K #> x) = (H <#> K) #> x"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   806
by (force simp add: r_coset_def set_mult_def m_assoc)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   807
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   808
lemma (in group) rcos_assoc_lcos:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   809
     "\<lbrakk>H \<subseteq> carrier(G); K \<subseteq> carrier(G); x \<in> carrier(G)\<rbrakk>
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   810
      \<Longrightarrow> (H #> x) <#> K = H <#> (x <# K)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   811
by (force simp add: r_coset_def l_coset_def set_mult_def m_assoc)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   812
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   813
lemma (in normal) rcos_mult_step1:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   814
     "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk>
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   815
      \<Longrightarrow> (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   816
by (simp add: setmult_rcos_assoc subset
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   817
              r_coset_subset_G l_coset_subset_G rcos_assoc_lcos)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   818
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   819
lemma (in normal) rcos_mult_step2:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   820
     "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk>
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   821
      \<Longrightarrow> (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   822
by (insert coset_eq, simp add: normal_def)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   823
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   824
lemma (in normal) rcos_mult_step3:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   825
     "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk>
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   826
      \<Longrightarrow> (H <#> (H #> x)) #> y = H #> (x \<cdot> y)"
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 16417
diff changeset
   827
  by (simp add: setmult_rcos_assoc coset_mult_assoc
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 16417
diff changeset
   828
              subgroup_mult_id subset prems normal.axioms)
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   829
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   830
lemma (in normal) rcos_sum:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   831
     "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk>
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   832
      \<Longrightarrow> (H #> x) <#> (H #> y) = H #> (x \<cdot> y)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   833
by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   834
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   835
lemma (in normal) rcosets_mult_eq: "M \<in> rcosets H \<Longrightarrow> H <#> M = M"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   836
  -- {* generalizes @{text subgroup_mult_id} *}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   837
  by (auto simp add: RCOSETS_def subset
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 16417
diff changeset
   838
        setmult_rcos_assoc subgroup_mult_id prems normal.axioms)
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   839
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   840
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   841
subsubsection{*Two distinct right cosets are disjoint*}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   842
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 19931
diff changeset
   843
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   844
  r_congruent :: "[i,i] => i" ("rcong\<index> _" [60] 60) where
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 19931
diff changeset
   845
  "rcong\<^bsub>G\<^esub> H == {<x,y> \<in> carrier(G) * carrier(G). inv\<^bsub>G\<^esub> x \<cdot>\<^bsub>G\<^esub> y \<in> H}"
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   846
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   847
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   848
lemma (in subgroup) equiv_rcong:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   849
   includes group G
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   850
   shows "equiv (carrier(G), rcong H)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   851
proof (simp add: equiv_def, intro conjI)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   852
  show "rcong H \<subseteq> carrier(G) \<times> carrier(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   853
    by (auto simp add: r_congruent_def) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   854
next
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   855
  show "refl (carrier(G), rcong H)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   856
    by (auto simp add: r_congruent_def refl_def) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   857
next
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   858
  show "sym (rcong H)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   859
  proof (simp add: r_congruent_def sym_def, clarify)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   860
    fix x y
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   861
    assume [simp]: "x \<in> carrier(G)" "y \<in> carrier(G)" 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   862
       and "inv x \<cdot> y \<in> H"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   863
    hence "inv (inv x \<cdot> y) \<in> H" by (simp add: m_inv_closed) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   864
    thus "inv y \<cdot> x \<in> H" by (simp add: inv_mult_group)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   865
  qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   866
next
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   867
  show "trans (rcong H)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   868
  proof (simp add: r_congruent_def trans_def, clarify)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   869
    fix x y z
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   870
    assume [simp]: "x \<in> carrier(G)" "y \<in> carrier(G)" "z \<in> carrier(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   871
       and "inv x \<cdot> y \<in> H" and "inv y \<cdot> z \<in> H"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   872
    hence "(inv x \<cdot> y) \<cdot> (inv y \<cdot> z) \<in> H" by simp
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   873
    hence "inv x \<cdot> (y \<cdot> inv y) \<cdot> z \<in> H" by (simp add: m_assoc del: inv) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   874
    thus "inv x \<cdot> z \<in> H" by simp
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   875
  qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   876
qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   877
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   878
text{*Equivalence classes of @{text rcong} correspond to left cosets.
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   879
  Was there a mistake in the definitions? I'd have expected them to
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   880
  correspond to right cosets.*}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   881
lemma (in subgroup) l_coset_eq_rcong:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   882
  includes group G
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   883
  assumes a: "a \<in> carrier(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   884
  shows "a <# H = (rcong H) `` {a}" 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   885
by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   886
                Collect_image_eq) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   887
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   888
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   889
lemma (in group) rcos_equation:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   890
  includes subgroup H G
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   891
  shows
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   892
     "\<lbrakk>ha \<cdot> a = h \<cdot> b; a \<in> carrier(G);  b \<in> carrier(G);  
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   893
        h \<in> H;  ha \<in> H;  hb \<in> H\<rbrakk>
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   894
      \<Longrightarrow> hb \<cdot> a \<in> (\<Union>h\<in>H. {h \<cdot> b})"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   895
apply (rule UN_I [of "hb \<cdot> ((inv ha) \<cdot> h)"], simp)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   896
apply (simp add: m_assoc transpose_inv)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   897
done
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   898
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   899
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   900
lemma (in group) rcos_disjoint:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   901
  includes subgroup H G
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   902
  shows "\<lbrakk>a \<in> rcosets H; b \<in> rcosets H; a\<noteq>b\<rbrakk> \<Longrightarrow> a \<inter> b = 0"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   903
apply (simp add: RCOSETS_def r_coset_def)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   904
apply (blast intro: rcos_equation prems sym)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   905
done
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   906
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   907
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   908
subsection {*Order of a Group and Lagrange's Theorem*}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   909
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 19931
diff changeset
   910
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   911
  order :: "i => i" where
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   912
  "order(S) == |carrier(S)|"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   913
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   914
lemma (in group) rcos_self:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   915
  includes subgroup
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   916
  shows "x \<in> carrier(G) \<Longrightarrow> x \<in> H #> x"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   917
apply (simp add: r_coset_def)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   918
apply (rule_tac x="\<one>" in bexI, auto) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   919
done
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   920
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   921
lemma (in group) rcosets_part_G:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   922
  includes subgroup
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   923
  shows "\<Union>(rcosets H) = carrier(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   924
apply (rule equalityI)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   925
 apply (force simp add: RCOSETS_def r_coset_def)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   926
apply (auto simp add: RCOSETS_def intro: rcos_self prems)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   927
done
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   928
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   929
lemma (in group) cosets_finite:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   930
     "\<lbrakk>c \<in> rcosets H;  H \<subseteq> carrier(G);  Finite (carrier(G))\<rbrakk> \<Longrightarrow> Finite(c)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   931
apply (auto simp add: RCOSETS_def)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   932
apply (simp add: r_coset_subset_G [THEN subset_Finite])
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   933
done
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   934
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   935
text{*More general than the HOL version, which also requires @{term G} to
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   936
      be finite.*}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   937
lemma (in group) card_cosets_equal:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   938
  assumes H:   "H \<subseteq> carrier(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   939
  shows "c \<in> rcosets H \<Longrightarrow> |c| = |H|"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   940
proof (simp add: RCOSETS_def, clarify)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   941
  fix a
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   942
  assume a: "a \<in> carrier(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   943
  show "|H #> a| = |H|"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   944
  proof (rule eqpollI [THEN cardinal_cong])
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   945
    show "H #> a \<lesssim> H"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   946
    proof (simp add: lepoll_def, intro exI) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   947
      show "(\<lambda>y \<in> H#>a. y \<cdot> inv a) \<in> inj(H #> a, H)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   948
        by (auto intro: lam_type 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   949
                 simp add: inj_def r_coset_def m_assoc subsetD [OF H] a)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   950
    qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   951
    show "H \<lesssim> H #> a"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   952
    proof (simp add: lepoll_def, intro exI) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   953
      show "(\<lambda>y\<in> H. y \<cdot> a) \<in> inj(H, H #> a)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   954
        by (auto intro: lam_type 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   955
                 simp add: inj_def r_coset_def  subsetD [OF H] a)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   956
    qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   957
  qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   958
qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   959
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   960
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   961
lemma (in group) rcosets_subset_PowG:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   962
     "subgroup(H,G) \<Longrightarrow> rcosets H \<subseteq> Pow(carrier(G))"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   963
apply (simp add: RCOSETS_def)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   964
apply (blast dest: r_coset_subset_G subgroup.subset)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   965
done
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   966
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   967
theorem (in group) lagrange:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   968
     "\<lbrakk>Finite(carrier(G)); subgroup(H,G)\<rbrakk>
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   969
      \<Longrightarrow> |rcosets H| #* |H| = order(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   970
apply (simp (no_asm_simp) add: order_def rcosets_part_G [symmetric])
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   971
apply (subst mult_commute)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   972
apply (rule card_partition)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   973
   apply (simp add: rcosets_subset_PowG [THEN subset_Finite])
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   974
  apply (simp add: rcosets_part_G)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   975
 apply (simp add: card_cosets_equal [OF subgroup.subset])
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   976
apply (simp add: rcos_disjoint)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   977
done
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   978
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   979
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   980
subsection {*Quotient Groups: Factorization of a Group*}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   981
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 19931
diff changeset
   982
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   983
  FactGroup :: "[i,i] => i" (infixl "Mod" 65) where
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   984
    --{*Actually defined for groups rather than monoids*}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   985
  "G Mod H == 
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 19931
diff changeset
   986
     <rcosets\<^bsub>G\<^esub> H, \<lambda><K1,K2> \<in> (rcosets\<^bsub>G\<^esub> H) \<times> (rcosets\<^bsub>G\<^esub> H). K1 <#>\<^bsub>G\<^esub> K2, H, 0>"
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   987
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   988
lemma (in normal) setmult_closed:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   989
     "\<lbrakk>K1 \<in> rcosets H; K2 \<in> rcosets H\<rbrakk> \<Longrightarrow> K1 <#> K2 \<in> rcosets H"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   990
by (auto simp add: rcos_sum RCOSETS_def)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   991
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   992
lemma (in normal) setinv_closed:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   993
     "K \<in> rcosets H \<Longrightarrow> set_inv K \<in> rcosets H"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   994
by (auto simp add: rcos_inv RCOSETS_def)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   995
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   996
lemma (in normal) rcosets_assoc:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   997
     "\<lbrakk>M1 \<in> rcosets H; M2 \<in> rcosets H; M3 \<in> rcosets H\<rbrakk>
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   998
      \<Longrightarrow> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
   999
by (auto simp add: RCOSETS_def rcos_sum m_assoc)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1000
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1001
lemma (in subgroup) subgroup_in_rcosets:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1002
  includes group G
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1003
  shows "H \<in> rcosets H"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1004
proof -
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1005
  have "H #> \<one> = H"
22931
11cc1ccad58e tuned proofs;
wenzelm
parents: 21404
diff changeset
  1006
    using _ `subgroup(H, G)` by (rule coset_join2) simp_all
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1007
  then show ?thesis
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1008
    by (auto simp add: RCOSETS_def intro: sym)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1009
qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1010
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1011
lemma (in normal) rcosets_inv_mult_group_eq:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1012
     "M \<in> rcosets H \<Longrightarrow> set_inv M <#> M = H"
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 16417
diff changeset
  1013
by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset prems normal.axioms)
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1014
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1015
theorem (in normal) factorgroup_is_group:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1016
  "group (G Mod H)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1017
apply (simp add: FactGroup_def)
14891
f2e9f7d813af fixed the groupI ambiguity
paulson
parents: 14884
diff changeset
  1018
apply (rule groupI)
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1019
    apply (simp add: setmult_closed)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1020
   apply (simp add: normal_imp_subgroup subgroup_in_rcosets)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1021
  apply (simp add: setmult_closed rcosets_assoc)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1022
 apply (simp add: normal_imp_subgroup
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1023
                  subgroup_in_rcosets rcosets_mult_eq)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1024
apply (auto dest: rcosets_inv_mult_group_eq simp add: setinv_closed)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1025
done
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1026
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1027
lemma (in normal) inv_FactGroup:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1028
     "X \<in> carrier (G Mod H) \<Longrightarrow> inv\<^bsub>G Mod H\<^esub> X = set_inv X"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1029
apply (rule group.inv_equality [OF factorgroup_is_group]) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1030
apply (simp_all add: FactGroup_def setinv_closed rcosets_inv_mult_group_eq)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1031
done
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1032
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1033
text{*The coset map is a homomorphism from @{term G} to the quotient group
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1034
  @{term "G Mod H"}*}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1035
lemma (in normal) r_coset_hom_Mod:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1036
  "(\<lambda>a \<in> carrier(G). H #> a) \<in> hom(G, G Mod H)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1037
by (auto simp add: FactGroup_def RCOSETS_def hom_def rcos_sum intro: lam_type) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1038
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1039
14891
f2e9f7d813af fixed the groupI ambiguity
paulson
parents: 14884
diff changeset
  1040
subsection{*The First Isomorphism Theorem*}
f2e9f7d813af fixed the groupI ambiguity
paulson
parents: 14884
diff changeset
  1041
f2e9f7d813af fixed the groupI ambiguity
paulson
parents: 14884
diff changeset
  1042
text{*The quotient by the kernel of a homomorphism is isomorphic to the 
f2e9f7d813af fixed the groupI ambiguity
paulson
parents: 14884
diff changeset
  1043
  range of that homomorphism.*}
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1044
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 19931
diff changeset
  1045
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
  1046
  kernel :: "[i,i,i] => i" where
14884
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1047
    --{*the kernel of a homomorphism*}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1048
  "kernel(G,H,h) == {x \<in> carrier(G). h ` x = \<one>\<^bsub>H\<^esub>}";
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1049
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1050
lemma (in group_hom) subgroup_kernel: "subgroup (kernel(G,H,h), G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1051
apply (rule subgroup.intro) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1052
apply (auto simp add: kernel_def group.intro prems) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1053
done
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1054
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1055
text{*The kernel of a homomorphism is a normal subgroup*}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1056
lemma (in group_hom) normal_kernel: "(kernel(G,H,h)) \<lhd> G"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1057
apply (simp add: group.normal_inv_iff subgroup_kernel group.intro prems)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1058
apply (simp add: kernel_def)  
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1059
done
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1060
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1061
lemma (in group_hom) FactGroup_nonempty:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1062
  assumes X: "X \<in> carrier (G Mod kernel(G,H,h))"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1063
  shows "X \<noteq> 0"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1064
proof -
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1065
  from X
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1066
  obtain g where "g \<in> carrier(G)" 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1067
             and "X = kernel(G,H,h) #> g"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1068
    by (auto simp add: FactGroup_def RCOSETS_def)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1069
  thus ?thesis 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1070
   by (auto simp add: kernel_def r_coset_def image_def intro: hom_one)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1071
qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1072
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1073
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1074
lemma (in group_hom) FactGroup_contents_mem:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1075
  assumes X: "X \<in> carrier (G Mod (kernel(G,H,h)))"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1076
  shows "contents (h``X) \<in> carrier(H)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1077
proof -
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1078
  from X
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1079
  obtain g where g: "g \<in> carrier(G)" 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1080
             and "X = kernel(G,H,h) #> g"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1081
    by (auto simp add: FactGroup_def RCOSETS_def)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1082
  hence "h `` X = {h ` g}"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1083
    by (auto simp add: kernel_def r_coset_def image_UN 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1084
                       image_eq_UN [OF hom_is_fun] g)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1085
  thus ?thesis by (auto simp add: g)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1086
qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1087
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1088
lemma mult_FactGroup:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1089
     "[|X \<in> carrier(G Mod H); X' \<in> carrier(G Mod H)|] 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1090
      ==> X \<cdot>\<^bsub>(G Mod H)\<^esub> X' = X <#>\<^bsub>G\<^esub> X'"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1091
by (simp add: FactGroup_def) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1092
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1093
lemma (in normal) FactGroup_m_closed:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1094
     "[|X \<in> carrier(G Mod H); X' \<in> carrier(G Mod H)|] 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1095
      ==> X <#>\<^bsub>G\<^esub> X' \<in> carrier(G Mod H)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1096
by (simp add: FactGroup_def setmult_closed) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1097
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1098
lemma (in group_hom) FactGroup_hom:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1099
     "(\<lambda>X \<in> carrier(G Mod (kernel(G,H,h))). contents (h``X))
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1100
      \<in> hom (G Mod (kernel(G,H,h)), H)" 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1101
proof (simp add: hom_def FactGroup_contents_mem lam_type mult_FactGroup normal.FactGroup_m_closed [OF normal_kernel], intro ballI)  
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1102
  fix X and X'
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1103
  assume X:  "X  \<in> carrier (G Mod kernel(G,H,h))"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1104
     and X': "X' \<in> carrier (G Mod kernel(G,H,h))"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1105
  then
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1106
  obtain g and g'
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1107
           where "g \<in> carrier(G)" and "g' \<in> carrier(G)" 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1108
             and "X = kernel(G,H,h) #> g" and "X' = kernel(G,H,h) #> g'"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1109
    by (auto simp add: FactGroup_def RCOSETS_def)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1110
  hence all: "\<forall>x\<in>X. h ` x = h ` g" "\<forall>x\<in>X'. h ` x = h ` g'" 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1111
    and Xsub: "X \<subseteq> carrier(G)" and X'sub: "X' \<subseteq> carrier(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1112
    by (force simp add: kernel_def r_coset_def image_def)+
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1113
  hence "h `` (X <#> X') = {h ` g \<cdot>\<^bsub>H\<^esub> h ` g'}" using X X'
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1114
    by (auto dest!: FactGroup_nonempty
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1115
             simp add: set_mult_def image_eq_UN [OF hom_is_fun] image_UN
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1116
                       subsetD [OF Xsub] subsetD [OF X'sub]) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1117
  thus "contents (h `` (X <#> X')) = contents (h `` X) \<cdot>\<^bsub>H\<^esub> contents (h `` X')"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1118
    by (simp add: all image_eq_UN [OF hom_is_fun] FactGroup_nonempty 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1119
                  X X' Xsub X'sub)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1120
qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1121
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1122
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1123
text{*Lemma for the following injectivity result*}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1124
lemma (in group_hom) FactGroup_subset:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1125
     "\<lbrakk>g \<in> carrier(G); g' \<in> carrier(G); h ` g = h ` g'\<rbrakk>
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1126
      \<Longrightarrow>  kernel(G,H,h) #> g \<subseteq> kernel(G,H,h) #> g'"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1127
apply (clarsimp simp add: kernel_def r_coset_def image_def)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1128
apply (rename_tac y)  
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1129
apply (rule_tac x="y \<cdot> g \<cdot> inv g'" in bexI) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1130
apply (simp_all add: G.m_assoc) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1131
done
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1132
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1133
lemma (in group_hom) FactGroup_inj:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1134
     "(\<lambda>X\<in>carrier (G Mod kernel(G,H,h)). contents (h `` X))
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1135
      \<in> inj(carrier (G Mod kernel(G,H,h)), carrier(H))"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1136
proof (simp add: inj_def FactGroup_contents_mem lam_type, clarify) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1137
  fix X and X'
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1138
  assume X:  "X  \<in> carrier (G Mod kernel(G,H,h))"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1139
     and X': "X' \<in> carrier (G Mod kernel(G,H,h))"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1140
  then
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1141
  obtain g and g'
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1142
           where gX: "g \<in> carrier(G)"  "g' \<in> carrier(G)" 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1143
              "X = kernel(G,H,h) #> g" "X' = kernel(G,H,h) #> g'"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1144
    by (auto simp add: FactGroup_def RCOSETS_def)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1145
  hence all: "\<forall>x\<in>X. h ` x = h ` g" "\<forall>x\<in>X'. h ` x = h ` g'"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1146
    and Xsub: "X \<subseteq> carrier(G)" and X'sub: "X' \<subseteq> carrier(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1147
    by (force simp add: kernel_def r_coset_def image_def)+
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1148
  assume "contents (h `` X) = contents (h `` X')"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1149
  hence h: "h ` g = h ` g'"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1150
    by (simp add: all image_eq_UN [OF hom_is_fun] FactGroup_nonempty 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1151
                  X X' Xsub X'sub)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1152
  show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1153
qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1154
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1155
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1156
lemma (in group_hom) kernel_rcoset_subset:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1157
  assumes g: "g \<in> carrier(G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1158
  shows "kernel(G,H,h) #> g \<subseteq> carrier (G)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1159
    by (auto simp add: g kernel_def r_coset_def) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1160
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1161
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1162
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1163
text{*If the homomorphism @{term h} is onto @{term H}, then so is the
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1164
homomorphism from the quotient group*}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1165
lemma (in group_hom) FactGroup_surj:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1166
  assumes h: "h \<in> surj(carrier(G), carrier(H))"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1167
  shows "(\<lambda>X\<in>carrier (G Mod kernel(G,H,h)). contents (h `` X))
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1168
         \<in> surj(carrier (G Mod kernel(G,H,h)), carrier(H))"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1169
proof (simp add: surj_def FactGroup_contents_mem lam_type, clarify)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1170
  fix y
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1171
  assume y: "y \<in> carrier(H)"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1172
  with h obtain g where g: "g \<in> carrier(G)" "h ` g = y"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1173
    by (auto simp add: surj_def) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1174
  hence "(\<Union>x\<in>kernel(G,H,h) #> g. {h ` x}) = {y}" 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1175
    by (auto simp add: y kernel_def r_coset_def) 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1176
  with g show "\<exists>x\<in>carrier(G Mod kernel(G, H, h)). contents(h `` x) = y"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1177
        --{*The witness is @{term "kernel(G,H,h) #> g"}*}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1178
    by (force simp add: FactGroup_def RCOSETS_def 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1179
           image_eq_UN [OF hom_is_fun] kernel_rcoset_subset)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1180
qed
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1181
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1182
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1183
text{*If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1184
 quotient group @{term "G Mod (kernel(G,H,h))"} is isomorphic to @{term H}.*}
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1185
theorem (in group_hom) FactGroup_iso:
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1186
  "h \<in> surj(carrier(G), carrier(H))
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1187
   \<Longrightarrow> (\<lambda>X\<in>carrier (G Mod kernel(G,H,h)). contents (h``X)) \<in> (G Mod (kernel(G,H,h))) \<cong> H"
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1188
by (simp add: iso_def FactGroup_hom FactGroup_inj bij_def FactGroup_surj)
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1189
 
0d7d8b1b3a97 Groups, Rings and supporting lemmas
paulson
parents:
diff changeset
  1190
end