src/HOL/Algebra/Group.thy
 author ballarin Tue Apr 13 09:42:40 2004 +0200 (2004-04-13) changeset 14551 2cb6ff394bfb parent 14286 0ae66ffb9784 child 14651 02b8f3bcf7fe permissions -rw-r--r--
Various changes to HOL-Algebra;
Locale instantiation.
 ballarin@13813  1 (*  ballarin@13813  2  Title: HOL/Algebra/Group.thy  ballarin@13813  3  Id: $Id$  ballarin@13813  4  Author: Clemens Ballarin, started 4 February 2003  ballarin@13813  5 ballarin@13813  6 Based on work by Florian Kammueller, L C Paulson and Markus Wenzel.  ballarin@13813  7 *)  ballarin@13813  8 ballarin@13949  9 header {* Groups *}  ballarin@13813  10 ballarin@13835  11 theory Group = FuncSet:  ballarin@13813  12 ballarin@13936  13 section {* From Magmas to Groups *}  ballarin@13936  14 ballarin@13813  15 text {*  ballarin@13813  16  Definitions follow Jacobson, Basic Algebra I, Freeman, 1985; with  ballarin@13813  17  the exception of \emph{magma} which, following Bourbaki, is a set  ballarin@13813  18  together with a binary, closed operation.  ballarin@13813  19 *}  ballarin@13813  20 ballarin@13813  21 subsection {* Definitions *}  ballarin@13813  22 ballarin@14286  23 (* Object with a carrier set. *)  ballarin@14286  24 ballarin@14286  25 record 'a partial_object =  ballarin@13813  26  carrier :: "'a set"  ballarin@14286  27 ballarin@14286  28 record 'a semigroup = "'a partial_object" +  ballarin@13813  29  mult :: "['a, 'a] => 'a" (infixl "\\" 70)  ballarin@13813  30 ballarin@13817  31 record 'a monoid = "'a semigroup" +  ballarin@13813  32  one :: 'a ("\\")  ballarin@13817  33 ballarin@13936  34 constdefs  ballarin@13936  35  m_inv :: "[('a, 'm) monoid_scheme, 'a] => 'a" ("inv\ _" [81] 80)  ballarin@13936  36  "m_inv G x == (THE y. y \ carrier G &  ballarin@13936  37  mult G x y = one G & mult G y x = one G)"  ballarin@13936  38 ballarin@13936  39  Units :: "('a, 'm) monoid_scheme => 'a set"  ballarin@13936  40  "Units G == {y. y \ carrier G &  ballarin@13936  41  (EX x : carrier G. mult G x y = one G & mult G y x = one G)}"  ballarin@13936  42 ballarin@13936  43 consts  ballarin@13936  44  pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a" (infixr "'(^')\" 75)  ballarin@13936  45 ballarin@13936  46 defs (overloaded)  ballarin@13936  47  nat_pow_def: "pow G a n == nat_rec (one G) (%u b. mult G b a) n"  ballarin@13936  48  int_pow_def: "pow G a z ==  ballarin@13936  49  let p = nat_rec (one G) (%u b. mult G b a)  ballarin@13936  50  in if neg z then m_inv G (p (nat (-z))) else p (nat z)"  ballarin@13813  51 ballarin@13813  52 locale magma = struct G +  ballarin@13813  53  assumes m_closed [intro, simp]:  ballarin@13813  54  "[| x \ carrier G; y \ carrier G |] ==> x \ y \ carrier G"  ballarin@13813  55 ballarin@13813  56 locale semigroup = magma +  ballarin@13813  57  assumes m_assoc:  ballarin@13813  58  "[| x \ carrier G; y \ carrier G; z \ carrier G |] ==>  ballarin@13936  59  (x \ y) \ z = x \ (y \ z)"  ballarin@13813  60 ballarin@13936  61 locale monoid = semigroup +  ballarin@13813  62  assumes one_closed [intro, simp]: "\ \ carrier G"  ballarin@13813  63  and l_one [simp]: "x \ carrier G ==> \ \ x = x"  ballarin@13936  64  and r_one [simp]: "x \ carrier G ==> x \ \ = x"  ballarin@13817  65 ballarin@13936  66 lemma monoidI:  ballarin@13936  67  assumes m_closed:  ballarin@13936  68  "!!x y. [| x \ carrier G; y \ carrier G |] ==> mult G x y \ carrier G"  ballarin@13936  69  and one_closed: "one G \ carrier G"  ballarin@13936  70  and m_assoc:  ballarin@13936  71  "!!x y z. [| x \ carrier G; y \ carrier G; z \ carrier G |] ==>  ballarin@13936  72  mult G (mult G x y) z = mult G x (mult G y z)"  ballarin@13936  73  and l_one: "!!x. x \ carrier G ==> mult G (one G) x = x"  ballarin@13936  74  and r_one: "!!x. x \ carrier G ==> mult G x (one G) = x"  ballarin@13936  75  shows "monoid G"  ballarin@13936  76  by (fast intro!: monoid.intro magma.intro semigroup_axioms.intro  ballarin@13936  77  semigroup.intro monoid_axioms.intro  ballarin@13936  78  intro: prems)  ballarin@13936  79 ballarin@13936  80 lemma (in monoid) Units_closed [dest]:  ballarin@13936  81  "x \ Units G ==> x \ carrier G"  ballarin@13936  82  by (unfold Units_def) fast  ballarin@13936  83 ballarin@13936  84 lemma (in monoid) inv_unique:  ballarin@13936  85  assumes eq: "y \ x = \" "x \ y' = \"  ballarin@13936  86  and G: "x \ carrier G" "y \ carrier G" "y' \ carrier G"  ballarin@13936  87  shows "y = y'"  ballarin@13936  88 proof -  ballarin@13936  89  from G eq have "y = y \ (x \ y')" by simp  ballarin@13936  90  also from G have "... = (y \ x) \ y'" by (simp add: m_assoc)  ballarin@13936  91  also from G eq have "... = y'" by simp  ballarin@13936  92  finally show ?thesis .  ballarin@13936  93 qed  ballarin@13936  94 ballarin@13940  95 lemma (in monoid) Units_one_closed [intro, simp]:  ballarin@13940  96  "\ \ Units G"  ballarin@13940  97  by (unfold Units_def) auto  ballarin@13940  98 ballarin@13936  99 lemma (in monoid) Units_inv_closed [intro, simp]:  ballarin@13936  100  "x \ Units G ==> inv x \ carrier G"  paulson@13943  101  apply (unfold Units_def m_inv_def, auto)  ballarin@13936  102  apply (rule theI2, fast)  paulson@13943  103  apply (fast intro: inv_unique, fast)  ballarin@13936  104  done  ballarin@13936  105 ballarin@13936  106 lemma (in monoid) Units_l_inv:  ballarin@13936  107  "x \ Units G ==> inv x \ x = \"  paulson@13943  108  apply (unfold Units_def m_inv_def, auto)  ballarin@13936  109  apply (rule theI2, fast)  paulson@13943  110  apply (fast intro: inv_unique, fast)  ballarin@13936  111  done  ballarin@13936  112 ballarin@13936  113 lemma (in monoid) Units_r_inv:  ballarin@13936  114  "x \ Units G ==> x \ inv x = \"  paulson@13943  115  apply (unfold Units_def m_inv_def, auto)  ballarin@13936  116  apply (rule theI2, fast)  paulson@13943  117  apply (fast intro: inv_unique, fast)  ballarin@13936  118  done  ballarin@13936  119 ballarin@13936  120 lemma (in monoid) Units_inv_Units [intro, simp]:  ballarin@13936  121  "x \ Units G ==> inv x \ Units G"  ballarin@13936  122 proof -  ballarin@13936  123  assume x: "x \ Units G"  ballarin@13936  124  show "inv x \ Units G"  ballarin@13936  125  by (auto simp add: Units_def  ballarin@13936  126  intro: Units_l_inv Units_r_inv x Units_closed [OF x])  ballarin@13936  127 qed  ballarin@13936  128 ballarin@13936  129 lemma (in monoid) Units_l_cancel [simp]:  ballarin@13936  130  "[| x \ Units G; y \ carrier G; z \ carrier G |] ==>  ballarin@13936  131  (x \ y = x \ z) = (y = z)"  ballarin@13936  132 proof  ballarin@13936  133  assume eq: "x \ y = x \ z"  ballarin@13936  134  and G: "x \ Units G" "y \ carrier G" "z \ carrier G"  ballarin@13936  135  then have "(inv x \ x) \ y = (inv x \ x) \ z"  ballarin@13936  136  by (simp add: m_assoc Units_closed)  ballarin@13936  137  with G show "y = z" by (simp add: Units_l_inv)  ballarin@13936  138 next  ballarin@13936  139  assume eq: "y = z"  ballarin@13936  140  and G: "x \ Units G" "y \ carrier G" "z \ carrier G"  ballarin@13936  141  then show "x \ y = x \ z" by simp  ballarin@13936  142 qed  ballarin@13936  143 ballarin@13936  144 lemma (in monoid) Units_inv_inv [simp]:  ballarin@13936  145  "x \ Units G ==> inv (inv x) = x"  ballarin@13936  146 proof -  ballarin@13936  147  assume x: "x \ Units G"  ballarin@13936  148  then have "inv x \ inv (inv x) = inv x \ x"  ballarin@13936  149  by (simp add: Units_l_inv Units_r_inv)  ballarin@13936  150  with x show ?thesis by (simp add: Units_closed)  ballarin@13936  151 qed  ballarin@13936  152 ballarin@13936  153 lemma (in monoid) inv_inj_on_Units:  ballarin@13936  154  "inj_on (m_inv G) (Units G)"  ballarin@13936  155 proof (rule inj_onI)  ballarin@13936  156  fix x y  ballarin@13936  157  assume G: "x \ Units G" "y \ Units G" and eq: "inv x = inv y"  ballarin@13936  158  then have "inv (inv x) = inv (inv y)" by simp  ballarin@13936  159  with G show "x = y" by simp  ballarin@13936  160 qed  ballarin@13936  161 ballarin@13940  162 lemma (in monoid) Units_inv_comm:  ballarin@13940  163  assumes inv: "x \ y = \"  ballarin@13940  164  and G: "x \ Units G" "y \ Units G"  ballarin@13940  165  shows "y \ x = \"  ballarin@13940  166 proof -  ballarin@13940  167  from G have "x \ y \ x = x \ \" by (auto simp add: inv Units_closed)  ballarin@13940  168  with G show ?thesis by (simp del: r_one add: m_assoc Units_closed)  ballarin@13940  169 qed  ballarin@13940  170 ballarin@13936  171 text {* Power *}  ballarin@13936  172 ballarin@13936  173 lemma (in monoid) nat_pow_closed [intro, simp]:  ballarin@13936  174  "x \ carrier G ==> x (^) (n::nat) \ carrier G"  ballarin@13936  175  by (induct n) (simp_all add: nat_pow_def)  ballarin@13936  176 ballarin@13936  177 lemma (in monoid) nat_pow_0 [simp]:  ballarin@13936  178  "x (^) (0::nat) = \"  ballarin@13936  179  by (simp add: nat_pow_def)  ballarin@13936  180 ballarin@13936  181 lemma (in monoid) nat_pow_Suc [simp]:  ballarin@13936  182  "x (^) (Suc n) = x (^) n \ x"  ballarin@13936  183  by (simp add: nat_pow_def)  ballarin@13936  184 ballarin@13936  185 lemma (in monoid) nat_pow_one [simp]:  ballarin@13936  186  "\ (^) (n::nat) = \"  ballarin@13936  187  by (induct n) simp_all  ballarin@13936  188 ballarin@13936  189 lemma (in monoid) nat_pow_mult:  ballarin@13936  190  "x \ carrier G ==> x (^) (n::nat) \ x (^) m = x (^) (n + m)"  ballarin@13936  191  by (induct m) (simp_all add: m_assoc [THEN sym])  ballarin@13936  192 ballarin@13936  193 lemma (in monoid) nat_pow_pow:  ballarin@13936  194  "x \ carrier G ==> (x (^) n) (^) m = x (^) (n * m::nat)"  ballarin@13936  195  by (induct m) (simp, simp add: nat_pow_mult add_commute)  ballarin@13936  196 ballarin@13936  197 text {*  ballarin@13936  198  A group is a monoid all of whose elements are invertible.  ballarin@13936  199 *}  ballarin@13936  200 ballarin@13936  201 locale group = monoid +  ballarin@13936  202  assumes Units: "carrier G <= Units G"  ballarin@13936  203 ballarin@13936  204 theorem groupI:  ballarin@13936  205  assumes m_closed [simp]:  ballarin@13936  206  "!!x y. [| x \ carrier G; y \ carrier G |] ==> mult G x y \ carrier G"  ballarin@13936  207  and one_closed [simp]: "one G \ carrier G"  ballarin@13936  208  and m_assoc:  ballarin@13936  209  "!!x y z. [| x \ carrier G; y \ carrier G; z \ carrier G |] ==>  ballarin@13936  210  mult G (mult G x y) z = mult G x (mult G y z)"  ballarin@13936  211  and l_one [simp]: "!!x. x \ carrier G ==> mult G (one G) x = x"  ballarin@13936  212  and l_inv_ex: "!!x. x \ carrier G ==> EX y : carrier G. mult G y x = one G"  ballarin@13936  213  shows "group G"  ballarin@13936  214 proof -  ballarin@13936  215  have l_cancel [simp]:  ballarin@13936  216  "!!x y z. [| x \ carrier G; y \ carrier G; z \ carrier G |] ==>  ballarin@13936  217  (mult G x y = mult G x z) = (y = z)"  ballarin@13936  218  proof  ballarin@13936  219  fix x y z  ballarin@13936  220  assume eq: "mult G x y = mult G x z"  ballarin@13936  221  and G: "x \ carrier G" "y \ carrier G" "z \ carrier G"  ballarin@13936  222  with l_inv_ex obtain x_inv where xG: "x_inv \ carrier G"  ballarin@13936  223  and l_inv: "mult G x_inv x = one G" by fast  ballarin@13936  224  from G eq xG have "mult G (mult G x_inv x) y = mult G (mult G x_inv x) z"  ballarin@13936  225  by (simp add: m_assoc)  ballarin@13936  226  with G show "y = z" by (simp add: l_inv)  ballarin@13936  227  next  ballarin@13936  228  fix x y z  ballarin@13936  229  assume eq: "y = z"  ballarin@13936  230  and G: "x \ carrier G" "y \ carrier G" "z \ carrier G"  ballarin@13936  231  then show "mult G x y = mult G x z" by simp  ballarin@13936  232  qed  ballarin@13936  233  have r_one:  ballarin@13936  234  "!!x. x \ carrier G ==> mult G x (one G) = x"  ballarin@13936  235  proof -  ballarin@13936  236  fix x  ballarin@13936  237  assume x: "x \ carrier G"  ballarin@13936  238  with l_inv_ex obtain x_inv where xG: "x_inv \ carrier G"  ballarin@13936  239  and l_inv: "mult G x_inv x = one G" by fast  ballarin@13936  240  from x xG have "mult G x_inv (mult G x (one G)) = mult G x_inv x"  ballarin@13936  241  by (simp add: m_assoc [symmetric] l_inv)  ballarin@13936  242  with x xG show "mult G x (one G) = x" by simp  ballarin@13936  243  qed  ballarin@13936  244  have inv_ex:  ballarin@13936  245  "!!x. x \ carrier G ==> EX y : carrier G. mult G y x = one G &  ballarin@13936  246  mult G x y = one G"  ballarin@13936  247  proof -  ballarin@13936  248  fix x  ballarin@13936  249  assume x: "x \ carrier G"  ballarin@13936  250  with l_inv_ex obtain y where y: "y \ carrier G"  ballarin@13936  251  and l_inv: "mult G y x = one G" by fast  ballarin@13936  252  from x y have "mult G y (mult G x y) = mult G y (one G)"  ballarin@13936  253  by (simp add: m_assoc [symmetric] l_inv r_one)  ballarin@13936  254  with x y have r_inv: "mult G x y = one G"  ballarin@13936  255  by simp  ballarin@13936  256  from x y show "EX y : carrier G. mult G y x = one G &  ballarin@13936  257  mult G x y = one G"  ballarin@13936  258  by (fast intro: l_inv r_inv)  ballarin@13936  259  qed  ballarin@13936  260  then have carrier_subset_Units: "carrier G <= Units G"  ballarin@13936  261  by (unfold Units_def) fast  ballarin@13936  262  show ?thesis  ballarin@13936  263  by (fast intro!: group.intro magma.intro semigroup_axioms.intro  ballarin@13936  264  semigroup.intro monoid_axioms.intro group_axioms.intro  ballarin@13936  265  carrier_subset_Units intro: prems r_one)  ballarin@13936  266 qed  ballarin@13936  267 ballarin@13936  268 lemma (in monoid) monoid_groupI:  ballarin@13936  269  assumes l_inv_ex:  ballarin@13936  270  "!!x. x \ carrier G ==> EX y : carrier G. mult G y x = one G"  ballarin@13936  271  shows "group G"  ballarin@13936  272  by (rule groupI) (auto intro: m_assoc l_inv_ex)  ballarin@13936  273 ballarin@13936  274 lemma (in group) Units_eq [simp]:  ballarin@13936  275  "Units G = carrier G"  ballarin@13936  276 proof  ballarin@13936  277  show "Units G <= carrier G" by fast  ballarin@13936  278 next  ballarin@13936  279  show "carrier G <= Units G" by (rule Units)  ballarin@13936  280 qed  ballarin@13936  281 ballarin@13936  282 lemma (in group) inv_closed [intro, simp]:  ballarin@13936  283  "x \ carrier G ==> inv x \ carrier G"  ballarin@13936  284  using Units_inv_closed by simp  ballarin@13936  285 ballarin@13936  286 lemma (in group) l_inv:  ballarin@13936  287  "x \ carrier G ==> inv x \ x = \"  ballarin@13936  288  using Units_l_inv by simp  ballarin@13813  289 ballarin@13813  290 subsection {* Cancellation Laws and Basic Properties *}  ballarin@13813  291 ballarin@13813  292 lemma (in group) l_cancel [simp]:  ballarin@13813  293  "[| x \ carrier G; y \ carrier G; z \ carrier G |] ==>  ballarin@13813  294  (x \ y = x \ z) = (y = z)"  ballarin@13936  295  using Units_l_inv by simp  ballarin@13940  296 ballarin@13813  297 lemma (in group) r_inv:  ballarin@13813  298  "x \ carrier G ==> x \ inv x = \"  ballarin@13813  299 proof -  ballarin@13813  300  assume x: "x \ carrier G"  ballarin@13813  301  then have "inv x \ (x \ inv x) = inv x \ \"  ballarin@13813  302  by (simp add: m_assoc [symmetric] l_inv)  ballarin@13813  303  with x show ?thesis by (simp del: r_one)  ballarin@13813  304 qed  ballarin@13813  305 ballarin@13813  306 lemma (in group) r_cancel [simp]:  ballarin@13813  307  "[| x \ carrier G; y \ carrier G; z \ carrier G |] ==>  ballarin@13813  308  (y \ x = z \ x) = (y = z)"  ballarin@13813  309 proof  ballarin@13813  310  assume eq: "y \ x = z \ x"  ballarin@13813  311  and G: "x \ carrier G" "y \ carrier G" "z \ carrier G"  ballarin@13813  312  then have "y \ (x \ inv x) = z \ (x \ inv x)"  ballarin@13813  313  by (simp add: m_assoc [symmetric])  ballarin@13813  314  with G show "y = z" by (simp add: r_inv)  ballarin@13813  315 next  ballarin@13813  316  assume eq: "y = z"  ballarin@13813  317  and G: "x \ carrier G" "y \ carrier G" "z \ carrier G"  ballarin@13813  318  then show "y \ x = z \ x" by simp  ballarin@13813  319 qed  ballarin@13813  320 ballarin@13854  321 lemma (in group) inv_one [simp]:  ballarin@13854  322  "inv \ = \"  ballarin@13854  323 proof -  ballarin@13854  324  have "inv \ = \ \ (inv \)" by simp  ballarin@13854  325  moreover have "... = \" by (simp add: r_inv)  ballarin@13854  326  finally show ?thesis .  ballarin@13854  327 qed  ballarin@13854  328 ballarin@13813  329 lemma (in group) inv_inv [simp]:  ballarin@13813  330  "x \ carrier G ==> inv (inv x) = x"  ballarin@13936  331  using Units_inv_inv by simp  ballarin@13936  332 ballarin@13936  333 lemma (in group) inv_inj:  ballarin@13936  334  "inj_on (m_inv G) (carrier G)"  ballarin@13936  335  using inv_inj_on_Units by simp  ballarin@13813  336 ballarin@13854  337 lemma (in group) inv_mult_group:  ballarin@13813  338  "[| x \ carrier G; y \ carrier G |] ==> inv (x \ y) = inv y \ inv x"  ballarin@13813  339 proof -  ballarin@13813  340  assume G: "x \ carrier G" "y \ carrier G"  ballarin@13813  341  then have "inv (x \ y) \ (x \ y) = (inv y \ inv x) \ (x \ y)"  ballarin@13813  342  by (simp add: m_assoc l_inv) (simp add: m_assoc [symmetric] l_inv)  ballarin@13813  343  with G show ?thesis by simp  ballarin@13813  344 qed  ballarin@13813  345 ballarin@13940  346 lemma (in group) inv_comm:  ballarin@13940  347  "[| x \ y = \; x \ carrier G; y \ carrier G |] ==> y \ x = \"  ballarin@13940  348  by (rule Units_inv_comm) auto  ballarin@13940  349 paulson@13944  350 lemma (in group) inv_equality:  paulson@13943  351  "[|y \ x = \; x \ carrier G; y \ carrier G|] ==> inv x = y"  paulson@13943  352 apply (simp add: m_inv_def)  paulson@13943  353 apply (rule the_equality)  paulson@13943  354  apply (simp add: inv_comm [of y x])  paulson@13943  355 apply (rule r_cancel [THEN iffD1], auto)  paulson@13943  356 done  paulson@13943  357 ballarin@13936  358 text {* Power *}  ballarin@13936  359 ballarin@13936  360 lemma (in group) int_pow_def2:  ballarin@13936  361  "a (^) (z::int) = (if neg z then inv (a (^) (nat (-z))) else a (^) (nat z))"  ballarin@13936  362  by (simp add: int_pow_def nat_pow_def Let_def)  ballarin@13936  363 ballarin@13936  364 lemma (in group) int_pow_0 [simp]:  ballarin@13936  365  "x (^) (0::int) = \"  ballarin@13936  366  by (simp add: int_pow_def2)  ballarin@13936  367 ballarin@13936  368 lemma (in group) int_pow_one [simp]:  ballarin@13936  369  "\ (^) (z::int) = \"  ballarin@13936  370  by (simp add: int_pow_def2)  ballarin@13936  371 ballarin@13813  372 subsection {* Substructures *}  ballarin@13813  373 ballarin@13813  374 locale submagma = var H + struct G +  ballarin@13813  375  assumes subset [intro, simp]: "H \ carrier G"  ballarin@13813  376  and m_closed [intro, simp]: "[| x \ H; y \ H |] ==> x \ y \ H"  ballarin@13813  377 ballarin@13813  378 declare (in submagma) magma.intro [intro] semigroup.intro [intro]  ballarin@13936  379  semigroup_axioms.intro [intro]  ballarin@13813  380 (*  ballarin@13813  381 alternative definition of submagma  ballarin@13813  382 ballarin@13813  383 locale submagma = var H + struct G +  ballarin@13813  384  assumes subset [intro, simp]: "carrier H \ carrier G"  ballarin@13813  385  and m_equal [simp]: "mult H = mult G"  ballarin@13813  386  and m_closed [intro, simp]:  ballarin@13813  387  "[| x \ carrier H; y \ carrier H |] ==> x \ y \ carrier H"  ballarin@13813  388 *)  ballarin@13813  389 ballarin@13813  390 lemma submagma_imp_subset:  ballarin@13813  391  "submagma H G ==> H \ carrier G"  ballarin@13813  392  by (rule submagma.subset)  ballarin@13813  393 ballarin@13813  394 lemma (in submagma) subsetD [dest, simp]:  ballarin@13813  395  "x \ H ==> x \ carrier G"  ballarin@13813  396  using subset by blast  ballarin@13813  397 ballarin@13813  398 lemma (in submagma) magmaI [intro]:  ballarin@13813  399  includes magma G  ballarin@13813  400  shows "magma (G(| carrier := H |))"  ballarin@13813  401  by rule simp  ballarin@13813  402 ballarin@13813  403 lemma (in submagma) semigroup_axiomsI [intro]:  ballarin@13813  404  includes semigroup G  ballarin@13813  405  shows "semigroup_axioms (G(| carrier := H |))"  ballarin@13813  406  by rule (simp add: m_assoc)  ballarin@13813  407 ballarin@13813  408 lemma (in submagma) semigroupI [intro]:  ballarin@13813  409  includes semigroup G  ballarin@13813  410  shows "semigroup (G(| carrier := H |))"  ballarin@13813  411  using prems by fast  ballarin@13813  412 ballarin@14551  413 ballarin@13813  414 locale subgroup = submagma H G +  ballarin@13813  415  assumes one_closed [intro, simp]: "\ \ H"  ballarin@13813  416  and m_inv_closed [intro, simp]: "x \ H ==> inv x \ H"  ballarin@13813  417 ballarin@13813  418 declare (in subgroup) group.intro [intro]  ballarin@13949  419 ballarin@13813  420 lemma (in subgroup) group_axiomsI [intro]:  ballarin@13813  421  includes group G  ballarin@13813  422  shows "group_axioms (G(| carrier := H |))"  ballarin@14254  423  by (rule group_axioms.intro) (auto intro: l_inv r_inv simp add: Units_def)  ballarin@13813  424 ballarin@13813  425 lemma (in subgroup) groupI [intro]:  ballarin@13813  426  includes group G  ballarin@13813  427  shows "group (G(| carrier := H |))"  ballarin@13936  428  by (rule groupI) (auto intro: m_assoc l_inv)  ballarin@13813  429 ballarin@13813  430 text {*  ballarin@13813  431  Since @{term H} is nonempty, it contains some element @{term x}. Since  ballarin@13813  432  it is closed under inverse, it contains @{text "inv x"}. Since  ballarin@13813  433  it is closed under product, it contains @{text "x \ inv x = \"}.  ballarin@13813  434 *}  ballarin@13813  435 ballarin@13813  436 lemma (in group) one_in_subset:  ballarin@13813  437  "[| H \ carrier G; H \ {}; \a \ H. inv a \ H; \a\H. \b\H. a \ b \ H |]  ballarin@13813  438  ==> \ \ H"  ballarin@13813  439 by (force simp add: l_inv)  ballarin@13813  440 ballarin@13813  441 text {* A characterization of subgroups: closed, non-empty subset. *}  ballarin@13813  442 ballarin@13813  443 lemma (in group) subgroupI:  ballarin@13813  444  assumes subset: "H \ carrier G" and non_empty: "H \ {}"  ballarin@13813  445  and inv: "!!a. a \ H ==> inv a \ H"  ballarin@13813  446  and mult: "!!a b. [|a \ H; b \ H|] ==> a \ b \ H"  ballarin@13813  447  shows "subgroup H G"  ballarin@14254  448 proof (rule subgroup.intro)  ballarin@14254  449  from subset and mult show "submagma H G" by (rule submagma.intro)  ballarin@13813  450 next  ballarin@13813  451  have "\ \ H" by (rule one_in_subset) (auto simp only: prems)  ballarin@13813  452  with inv show "subgroup_axioms H G"  ballarin@13813  453  by (intro subgroup_axioms.intro) simp_all  ballarin@13813  454 qed  ballarin@13813  455 ballarin@13813  456 text {*  ballarin@13813  457  Repeat facts of submagmas for subgroups. Necessary???  ballarin@13813  458 *}  ballarin@13813  459 ballarin@13813  460 lemma (in subgroup) subset:  ballarin@13813  461  "H \ carrier G"  ballarin@13813  462  ..  ballarin@13813  463 ballarin@13813  464 lemma (in subgroup) m_closed:  ballarin@13813  465  "[| x \ H; y \ H |] ==> x \ y \ H"  ballarin@13813  466  ..  ballarin@13813  467 ballarin@13813  468 declare magma.m_closed [simp]  ballarin@13813  469 ballarin@13936  470 declare monoid.one_closed [iff] group.inv_closed [simp]  ballarin@13936  471  monoid.l_one [simp] monoid.r_one [simp] group.inv_inv [simp]  ballarin@13813  472 ballarin@13813  473 lemma subgroup_nonempty:  ballarin@13813  474  "~ subgroup {} G"  ballarin@13813  475  by (blast dest: subgroup.one_closed)  ballarin@13813  476 ballarin@13813  477 lemma (in subgroup) finite_imp_card_positive:  ballarin@13813  478  "finite (carrier G) ==> 0 < card H"  ballarin@13813  479 proof (rule classical)  ballarin@14254  480  have sub: "subgroup H G" using prems by (rule subgroup.intro)  ballarin@13813  481  assume fin: "finite (carrier G)"  ballarin@13813  482  and zero: "~ 0 < card H"  ballarin@13813  483  then have "finite H" by (blast intro: finite_subset dest: subset)  ballarin@13813  484  with zero sub have "subgroup {} G" by simp  ballarin@13813  485  with subgroup_nonempty show ?thesis by contradiction  ballarin@13813  486 qed  ballarin@13813  487 ballarin@13936  488 (*  ballarin@13936  489 lemma (in monoid) Units_subgroup:  ballarin@13936  490  "subgroup (Units G) G"  ballarin@13936  491 *)  ballarin@13936  492 ballarin@13813  493 subsection {* Direct Products *}  ballarin@13813  494 ballarin@13813  495 constdefs  ballarin@13817  496  DirProdSemigroup ::  ballarin@13854  497  "[('a, 'm) semigroup_scheme, ('b, 'n) semigroup_scheme]  ballarin@13817  498  => ('a \ 'b) semigroup"  ballarin@13817  499  (infixr "\\<^sub>s" 80)  ballarin@13817  500  "G \\<^sub>s H == (| carrier = carrier G \ carrier H,  ballarin@13817  501  mult = (%(xg, xh) (yg, yh). (mult G xg yg, mult H xh yh)) |)"  ballarin@13817  502 ballarin@13936  503  DirProdGroup ::  ballarin@13854  504  "[('a, 'm) monoid_scheme, ('b, 'n) monoid_scheme] => ('a \ 'b) monoid"  ballarin@13936  505  (infixr "\\<^sub>g" 80)  ballarin@13936  506  "G \\<^sub>g H == (| carrier = carrier (G \\<^sub>s H),  ballarin@13817  507  mult = mult (G \\<^sub>s H),  ballarin@13817  508  one = (one G, one H) |)"  ballarin@13813  509 ballarin@13817  510 lemma DirProdSemigroup_magma:  ballarin@13813  511  includes magma G + magma H  ballarin@13817  512  shows "magma (G \\<^sub>s H)"  ballarin@14254  513  by (rule magma.intro) (auto simp add: DirProdSemigroup_def)  ballarin@13813  514 ballarin@13817  515 lemma DirProdSemigroup_semigroup_axioms:  ballarin@13813  516  includes semigroup G + semigroup H  ballarin@13817  517  shows "semigroup_axioms (G \\<^sub>s H)"  ballarin@14254  518  by (rule semigroup_axioms.intro)  ballarin@14254  519  (auto simp add: DirProdSemigroup_def G.m_assoc H.m_assoc)  ballarin@13813  520 ballarin@13817  521 lemma DirProdSemigroup_semigroup:  ballarin@13813  522  includes semigroup G + semigroup H  ballarin@13817  523  shows "semigroup (G \\<^sub>s H)"  ballarin@13813  524  using prems  ballarin@13813  525  by (fast intro: semigroup.intro  ballarin@13817  526  DirProdSemigroup_magma DirProdSemigroup_semigroup_axioms)  ballarin@13813  527 ballarin@13813  528 lemma DirProdGroup_magma:  ballarin@13813  529  includes magma G + magma H  ballarin@13813  530  shows "magma (G \\<^sub>g H)"  ballarin@14254  531  by (rule magma.intro)  ballarin@13936  532  (auto simp add: DirProdGroup_def DirProdSemigroup_def)  ballarin@13813  533 ballarin@13813  534 lemma DirProdGroup_semigroup_axioms:  ballarin@13813  535  includes semigroup G + semigroup H  ballarin@13813  536  shows "semigroup_axioms (G \\<^sub>g H)"  ballarin@14254  537  by (rule semigroup_axioms.intro)  ballarin@13936  538  (auto simp add: DirProdGroup_def DirProdSemigroup_def  ballarin@13817  539  G.m_assoc H.m_assoc)  ballarin@13813  540 ballarin@13813  541 lemma DirProdGroup_semigroup:  ballarin@13813  542  includes semigroup G + semigroup H  ballarin@13813  543  shows "semigroup (G \\<^sub>g H)"  ballarin@13813  544  using prems  ballarin@13813  545  by (fast intro: semigroup.intro  ballarin@13813  546  DirProdGroup_magma DirProdGroup_semigroup_axioms)  ballarin@13813  547 ballarin@13813  548 (* ... and further lemmas for group ... *)  ballarin@13813  549 ballarin@13817  550 lemma DirProdGroup_group:  ballarin@13813  551  includes group G + group H  ballarin@13813  552  shows "group (G \\<^sub>g H)"  ballarin@13936  553  by (rule groupI)  ballarin@13936  554  (auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv  ballarin@13936  555  simp add: DirProdGroup_def DirProdSemigroup_def)  ballarin@13813  556 paulson@13944  557 lemma carrier_DirProdGroup [simp]:  paulson@13944  558  "carrier (G \\<^sub>g H) = carrier G \ carrier H"  paulson@13944  559  by (simp add: DirProdGroup_def DirProdSemigroup_def)  paulson@13944  560 paulson@13944  561 lemma one_DirProdGroup [simp]:  paulson@13944  562  "one (G \\<^sub>g H) = (one G, one H)"  paulson@13944  563  by (simp add: DirProdGroup_def DirProdSemigroup_def);  paulson@13944  564 paulson@13944  565 lemma mult_DirProdGroup [simp]:  paulson@13944  566  "mult (G \\<^sub>g H) (g, h) (g', h') = (mult G g g', mult H h h')"  paulson@13944  567  by (simp add: DirProdGroup_def DirProdSemigroup_def)  paulson@13944  568 paulson@13944  569 lemma inv_DirProdGroup [simp]:  paulson@13944  570  includes group G + group H  paulson@13944  571  assumes g: "g \ carrier G"  paulson@13944  572  and h: "h \ carrier H"  paulson@13944  573  shows "m_inv (G \\<^sub>g H) (g, h) = (m_inv G g, m_inv H h)"  paulson@13944  574  apply (rule group.inv_equality [OF DirProdGroup_group])  paulson@13944  575  apply (simp_all add: prems group_def group.l_inv)  paulson@13944  576  done  paulson@13944  577 ballarin@13813  578 subsection {* Homomorphisms *}  ballarin@13813  579 ballarin@13813  580 constdefs  ballarin@13817  581  hom :: "[('a, 'c) semigroup_scheme, ('b, 'd) semigroup_scheme]  ballarin@13817  582  => ('a => 'b)set"  ballarin@13813  583  "hom G H ==  ballarin@13813  584  {h. h \ carrier G -> carrier H &  ballarin@13813  585  (\x \ carrier G. \y \ carrier G. h (mult G x y) = mult H (h x) (h y))}"  ballarin@13813  586 ballarin@13813  587 lemma (in semigroup) hom:  ballarin@13813  588  includes semigroup G  ballarin@13813  589  shows "semigroup (| carrier = hom G G, mult = op o |)"  ballarin@14254  590 proof (rule semigroup.intro)  ballarin@13813  591  show "magma (| carrier = hom G G, mult = op o |)"  ballarin@14254  592  by (rule magma.intro) (simp add: Pi_def hom_def)  ballarin@13813  593 next  ballarin@13813  594  show "semigroup_axioms (| carrier = hom G G, mult = op o |)"  ballarin@14254  595  by (rule semigroup_axioms.intro) (simp add: o_assoc)  ballarin@13813  596 qed  ballarin@13813  597 ballarin@13813  598 lemma hom_mult:  ballarin@13813  599  "[| h \ hom G H; x \ carrier G; y \ carrier G |]  ballarin@13813  600  ==> h (mult G x y) = mult H (h x) (h y)"  ballarin@13813  601  by (simp add: hom_def)  ballarin@13813  602 ballarin@13813  603 lemma hom_closed:  ballarin@13813  604  "[| h \ hom G H; x \ carrier G |] ==> h x \ carrier H"  ballarin@13813  605  by (auto simp add: hom_def funcset_mem)  ballarin@13813  606 paulson@13943  607 lemma compose_hom:  paulson@13943  608  "[|group G; h \ hom G G; h' \ hom G G; h' \ carrier G -> carrier G|]  paulson@13943  609  ==> compose (carrier G) h h' \ hom G G"  paulson@13943  610 apply (simp (no_asm_simp) add: hom_def)  paulson@13943  611 apply (intro conjI)  paulson@13943  612  apply (force simp add: funcset_compose hom_def)  paulson@13943  613 apply (simp add: compose_def group.axioms hom_mult funcset_mem)  paulson@13943  614 done  paulson@13943  615 ballarin@13813  616 locale group_hom = group G + group H + var h +  ballarin@13813  617  assumes homh: "h \ hom G H"  ballarin@13813  618  notes hom_mult [simp] = hom_mult [OF homh]  ballarin@13813  619  and hom_closed [simp] = hom_closed [OF homh]  ballarin@13813  620 ballarin@13813  621 lemma (in group_hom) one_closed [simp]:  ballarin@13813  622  "h \ \ carrier H"  ballarin@13813  623  by simp  ballarin@13813  624 ballarin@13813  625 lemma (in group_hom) hom_one [simp]:  ballarin@13813  626  "h \ = \\<^sub>2"  ballarin@13813  627 proof -  ballarin@13813  628  have "h \ \\<^sub>2 \\<^sub>2 = h \ \\<^sub>2 h \"  ballarin@13813  629  by (simp add: hom_mult [symmetric] del: hom_mult)  ballarin@13813  630  then show ?thesis by (simp del: r_one)  ballarin@13813  631 qed  ballarin@13813  632 ballarin@13813  633 lemma (in group_hom) inv_closed [simp]:  ballarin@13813  634  "x \ carrier G ==> h (inv x) \ carrier H"  ballarin@13813  635  by simp  ballarin@13813  636 ballarin@13813  637 lemma (in group_hom) hom_inv [simp]:  ballarin@13813  638  "x \ carrier G ==> h (inv x) = inv\<^sub>2 (h x)"  ballarin@13813  639 proof -  ballarin@13813  640  assume x: "x \ carrier G"  ballarin@13813  641  then have "h x \\<^sub>2 h (inv x) = \\<^sub>2"  ballarin@13813  642  by (simp add: hom_mult [symmetric] G.r_inv del: hom_mult)  ballarin@13813  643  also from x have "... = h x \\<^sub>2 inv\<^sub>2 (h x)"  ballarin@13813  644  by (simp add: hom_mult [symmetric] H.r_inv del: hom_mult)  ballarin@13813  645  finally have "h x \\<^sub>2 h (inv x) = h x \\<^sub>2 inv\<^sub>2 (h x)" .  ballarin@13813  646  with x show ?thesis by simp  ballarin@13813  647 qed  ballarin@13813  648 ballarin@13949  649 subsection {* Commutative Structures *}  ballarin@13936  650 ballarin@13936  651 text {*  ballarin@13936  652  Naming convention: multiplicative structures that are commutative  ballarin@13936  653  are called \emph{commutative}, additive structures are called  ballarin@13936  654  \emph{Abelian}.  ballarin@13936  655 *}  ballarin@13813  656 ballarin@13813  657 subsection {* Definition *}  ballarin@13813  658 ballarin@13936  659 locale comm_semigroup = semigroup +  ballarin@13813  660  assumes m_comm: "[| x \ carrier G; y \ carrier G |] ==> x \ y = y \ x"  ballarin@13813  661 ballarin@13936  662 lemma (in comm_semigroup) m_lcomm:  ballarin@13813  663  "[| x \ carrier G; y \ carrier G; z \ carrier G |] ==>  ballarin@13813  664  x \ (y \ z) = y \ (x \ z)"  ballarin@13813  665 proof -  ballarin@13813  666  assume xyz: "x \ carrier G" "y \ carrier G" "z \ carrier G"  ballarin@13813  667  from xyz have "x \ (y \ z) = (x \ y) \ z" by (simp add: m_assoc)  ballarin@13813  668  also from xyz have "... = (y \ x) \ z" by (simp add: m_comm)  ballarin@13813  669  also from xyz have "... = y \ (x \ z)" by (simp add: m_assoc)  ballarin@13813  670  finally show ?thesis .  ballarin@13813  671 qed  ballarin@13813  672 ballarin@13936  673 lemmas (in comm_semigroup) m_ac = m_assoc m_comm m_lcomm  ballarin@13936  674 ballarin@13936  675 locale comm_monoid = comm_semigroup + monoid  ballarin@13813  676 ballarin@13936  677 lemma comm_monoidI:  ballarin@13936  678  assumes m_closed:  ballarin@13936  679  "!!x y. [| x \ carrier G; y \ carrier G |] ==> mult G x y \ carrier G"  ballarin@13936  680  and one_closed: "one G \ carrier G"  ballarin@13936  681  and m_assoc:  ballarin@13936  682  "!!x y z. [| x \ carrier G; y \ carrier G; z \ carrier G |] ==>  ballarin@13936  683  mult G (mult G x y) z = mult G x (mult G y z)"  ballarin@13936  684  and l_one: "!!x. x \ carrier G ==> mult G (one G) x = x"  ballarin@13936  685  and m_comm:  ballarin@13936  686  "!!x y. [| x \ carrier G; y \ carrier G |] ==> mult G x y = mult G y x"  ballarin@13936  687  shows "comm_monoid G"  ballarin@13936  688  using l_one  ballarin@13936  689  by (auto intro!: comm_monoid.intro magma.intro semigroup_axioms.intro  ballarin@13936  690  comm_semigroup_axioms.intro monoid_axioms.intro  ballarin@13936  691  intro: prems simp: m_closed one_closed m_comm)  ballarin@13817  692 ballarin@13936  693 lemma (in monoid) monoid_comm_monoidI:  ballarin@13936  694  assumes m_comm:  ballarin@13936  695  "!!x y. [| x \ carrier G; y \ carrier G |] ==> mult G x y = mult G y x"  ballarin@13936  696  shows "comm_monoid G"  ballarin@13936  697  by (rule comm_monoidI) (auto intro: m_assoc m_comm)  ballarin@13936  698 (*  ballarin@13936  699 lemma (in comm_monoid) r_one [simp]:  ballarin@13817  700  "x \ carrier G ==> x \ \ = x"  ballarin@13817  701 proof -  ballarin@13817  702  assume G: "x \ carrier G"  ballarin@13817  703  then have "x \ \ = \ \ x" by (simp add: m_comm)  ballarin@13817  704  also from G have "... = x" by simp  ballarin@13817  705  finally show ?thesis .  ballarin@13817  706 qed  ballarin@13936  707 *)  ballarin@13817  708 ballarin@13936  709 lemma (in comm_monoid) nat_pow_distr:  ballarin@13936  710  "[| x \ carrier G; y \ carrier G |] ==>  ballarin@13936  711  (x \ y) (^) (n::nat) = x (^) n \ y (^) n"  ballarin@13936  712  by (induct n) (simp, simp add: m_ac)  ballarin@13936  713 ballarin@13936  714 locale comm_group = comm_monoid + group  ballarin@13936  715 ballarin@13936  716 lemma (in group) group_comm_groupI:  ballarin@13936  717  assumes m_comm: "!!x y. [| x \ carrier G; y \ carrier G |] ==>  ballarin@13936  718  mult G x y = mult G y x"  ballarin@13936  719  shows "comm_group G"  ballarin@13936  720  by (fast intro: comm_group.intro comm_semigroup_axioms.intro  ballarin@13936  721  group.axioms prems)  ballarin@13817  722 ballarin@13936  723 lemma comm_groupI:  ballarin@13936  724  assumes m_closed:  ballarin@13936  725  "!!x y. [| x \ carrier G; y \ carrier G |] ==> mult G x y \ carrier G"  ballarin@13936  726  and one_closed: "one G \ carrier G"  ballarin@13936  727  and m_assoc:  ballarin@13936  728  "!!x y z. [| x \ carrier G; y \ carrier G; z \ carrier G |] ==>  ballarin@13936  729  mult G (mult G x y) z = mult G x (mult G y z)"  ballarin@13936  730  and m_comm:  ballarin@13936  731  "!!x y. [| x \ carrier G; y \ carrier G |] ==> mult G x y = mult G y x"  ballarin@13936  732  and l_one: "!!x. x \ carrier G ==> mult G (one G) x = x"  ballarin@13936  733  and l_inv_ex: "!!x. x \ carrier G ==> EX y : carrier G. mult G y x = one G"  ballarin@13936  734  shows "comm_group G"  ballarin@13936  735  by (fast intro: group.group_comm_groupI groupI prems)  ballarin@13936  736 ballarin@13936  737 lemma (in comm_group) inv_mult:  ballarin@13854  738  "[| x \ carrier G; y \ carrier G |] ==> inv (x \ y) = inv x \ inv y"  ballarin@13936  739  by (simp add: m_ac inv_mult_group)  ballarin@13854  740 ballarin@13813  741 end