src/HOL/Algebra/Group.thy
 author paulson Wed Jun 06 14:25:53 2018 +0100 (12 months ago) changeset 68399 0b71d08528f0 parent 68188 2af1f142f855 child 68443 43055b016688 permissions -rw-r--r--
resolution of name clashes in Algebra
 wenzelm@35849  1 (* Title: HOL/Algebra/Group.thy  wenzelm@35849  2  Author: Clemens Ballarin, started 4 February 2003  ballarin@13813  3 ballarin@13813  4 Based on work by Florian Kammueller, L C Paulson and Markus Wenzel.  ballarin@13813  5 *)  ballarin@13813  6 haftmann@28823  7 theory Group  immler@68188  8 imports Complete_Lattice "HOL-Library.FuncSet"  haftmann@28823  9 begin  ballarin@13813  10 wenzelm@61382  11 section \Monoids and Groups\  ballarin@13936  12 wenzelm@61382  13 subsection \Definitions\  ballarin@20318  14 wenzelm@61382  15 text \  wenzelm@58622  16  Definitions follow @{cite "Jacobson:1985"}.  wenzelm@61382  17 \  ballarin@13813  18 paulson@14963  19 record 'a monoid = "'a partial_object" +  paulson@14963  20  mult :: "['a, 'a] \ 'a" (infixl "\\" 70)  paulson@14963  21  one :: 'a ("\\")  ballarin@13817  22 wenzelm@35847  23 definition  paulson@14852  24  m_inv :: "('a, 'b) monoid_scheme => 'a => 'a" ("inv\ _" [81] 80)  wenzelm@67091  25  where "inv\<^bsub>G\<^esub> x = (THE y. y \ carrier G \ x \\<^bsub>G\<^esub> y = \\<^bsub>G\<^esub> \ y \\<^bsub>G\<^esub> x = \\<^bsub>G\<^esub>)"  ballarin@13936  26 wenzelm@35847  27 definition  wenzelm@14651  28  Units :: "_ => 'a set"  wenzelm@67443  29  \ \The set of invertible elements\  wenzelm@67091  30  where "Units G = {y. y \ carrier G \ (\x \ carrier G. x \\<^bsub>G\<^esub> y = \\<^bsub>G\<^esub> \ y \\<^bsub>G\<^esub> x = \\<^bsub>G\<^esub>)}"  ballarin@13936  31 ballarin@13936  32 consts  nipkow@67341  33  pow :: "[('a, 'm) monoid_scheme, 'a, 'b::semiring_1] => 'a" (infixr "[^]\" 75)  wenzelm@35850  34 wenzelm@35850  35 overloading nat_pow == "pow :: [_, 'a, nat] => 'a"  wenzelm@35850  36 begin  blanchet@55415  37  definition "nat_pow G a n = rec_nat \\<^bsub>G\<^esub> (%u b. b \\<^bsub>G\<^esub> a) n"  wenzelm@35850  38 end  ballarin@13936  39 wenzelm@35850  40 overloading int_pow == "pow :: [_, 'a, int] => 'a"  wenzelm@35850  41 begin  wenzelm@35850  42  definition "int_pow G a z =  blanchet@55415  43  (let p = rec_nat \\<^bsub>G\<^esub> (%u b. b \\<^bsub>G\<^esub> a)  huffman@46559  44  in if z < 0 then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z))"  wenzelm@35850  45 end  ballarin@13813  46 nipkow@67341  47 lemma int_pow_int: "x [^]\<^bsub>G\<^esub> (int n) = x [^]\<^bsub>G\<^esub> n"  Andreas@61628  48 by(simp add: int_pow_def nat_pow_def)  Andreas@61628  49 ballarin@19783  50 locale monoid =  ballarin@19783  51  fixes G (structure)  ballarin@13813  52  assumes m_closed [intro, simp]:  paulson@14963  53  "\x \ carrier G; y \ carrier G\ \ x \ y \ carrier G"  paulson@14963  54  and m_assoc:  paulson@14963  55  "\x \ carrier G; y \ carrier G; z \ carrier G\  paulson@14963  56  \ (x \ y) \ z = x \ (y \ z)"  paulson@14963  57  and one_closed [intro, simp]: "\ \ carrier G"  paulson@14963  58  and l_one [simp]: "x \ carrier G \ \ \ x = x"  paulson@14963  59  and r_one [simp]: "x \ carrier G \ x \ \ = x"  ballarin@13817  60 ballarin@13936  61 lemma monoidI:  ballarin@19783  62  fixes G (structure)  ballarin@13936  63  assumes m_closed:  wenzelm@14693  64  "!!x y. [| x \ carrier G; y \ carrier G |] ==> x \ y \ carrier G"  wenzelm@14693  65  and one_closed: "\ \ carrier G"  ballarin@13936  66  and m_assoc:  ballarin@13936  67  "!!x y z. [| x \ carrier G; y \ carrier G; z \ carrier G |] ==>  wenzelm@14693  68  (x \ y) \ z = x \ (y \ z)"  wenzelm@14693  69  and l_one: "!!x. x \ carrier G ==> \ \ x = x"  wenzelm@14693  70  and r_one: "!!x. x \ carrier G ==> x \ \ = x"  ballarin@13936  71  shows "monoid G"  ballarin@27714  72  by (fast intro!: monoid.intro intro: assms)  ballarin@13936  73 ballarin@13936  74 lemma (in monoid) Units_closed [dest]:  ballarin@13936  75  "x \ Units G ==> x \ carrier G"  ballarin@13936  76  by (unfold Units_def) fast  ballarin@13936  77 ballarin@13936  78 lemma (in monoid) inv_unique:  wenzelm@14693  79  assumes eq: "y \ x = \" "x \ y' = \"  wenzelm@14693  80  and G: "x \ carrier G" "y \ carrier G" "y' \ carrier G"  ballarin@13936  81  shows "y = y'"  ballarin@13936  82 proof -  ballarin@13936  83  from G eq have "y = y \ (x \ y')" by simp  ballarin@13936  84  also from G have "... = (y \ x) \ y'" by (simp add: m_assoc)  ballarin@13936  85  also from G eq have "... = y'" by simp  ballarin@13936  86  finally show ?thesis .  ballarin@13936  87 qed  ballarin@13936  88 ballarin@27698  89 lemma (in monoid) Units_m_closed [intro, simp]:  ballarin@27698  90  assumes x: "x \ Units G" and y: "y \ Units G"  ballarin@27698  91  shows "x \ y \ Units G"  ballarin@27698  92 proof -  ballarin@27698  93  from x obtain x' where x: "x \ carrier G" "x' \ carrier G" and xinv: "x \ x' = \" "x' \ x = \"  ballarin@27698  94  unfolding Units_def by fast  ballarin@27698  95  from y obtain y' where y: "y \ carrier G" "y' \ carrier G" and yinv: "y \ y' = \" "y' \ y = \"  ballarin@27698  96  unfolding Units_def by fast  ballarin@27698  97  from x y xinv yinv have "y' \ (x' \ x) \ y = \" by simp  ballarin@27698  98  moreover from x y xinv yinv have "x \ (y \ y') \ x' = \" by simp  ballarin@27698  99  moreover note x y  ballarin@27698  100  ultimately show ?thesis unfolding Units_def  wenzelm@67443  101  \ \Must avoid premature use of \hyp_subst_tac\.\  ballarin@27698  102  apply (rule_tac CollectI)  ballarin@27698  103  apply (rule)  ballarin@27698  104  apply (fast)  ballarin@27698  105  apply (rule bexI [where x = "y' \ x'"])  ballarin@27698  106  apply (auto simp: m_assoc)  ballarin@27698  107  done  ballarin@27698  108 qed  ballarin@27698  109 ballarin@13940  110 lemma (in monoid) Units_one_closed [intro, simp]:  ballarin@13940  111  "\ \ Units G"  ballarin@13940  112  by (unfold Units_def) auto  ballarin@13940  113 ballarin@13936  114 lemma (in monoid) Units_inv_closed [intro, simp]:  ballarin@13936  115  "x \ Units G ==> inv x \ carrier G"  paulson@13943  116  apply (unfold Units_def m_inv_def, auto)  ballarin@13936  117  apply (rule theI2, fast)  paulson@13943  118  apply (fast intro: inv_unique, fast)  ballarin@13936  119  done  ballarin@13936  120 ballarin@19981  121 lemma (in monoid) Units_l_inv_ex:  ballarin@19981  122  "x \ Units G ==> \y \ carrier G. y \ x = \"  ballarin@19981  123  by (unfold Units_def) auto  ballarin@19981  124 ballarin@19981  125 lemma (in monoid) Units_r_inv_ex:  ballarin@19981  126  "x \ Units G ==> \y \ carrier G. x \ y = \"  ballarin@19981  127  by (unfold Units_def) auto  ballarin@19981  128 ballarin@27698  129 lemma (in monoid) Units_l_inv [simp]:  ballarin@13936  130  "x \ Units G ==> inv x \ x = \"  paulson@13943  131  apply (unfold Units_def m_inv_def, auto)  ballarin@13936  132  apply (rule theI2, fast)  paulson@13943  133  apply (fast intro: inv_unique, fast)  ballarin@13936  134  done  ballarin@13936  135 ballarin@27698  136 lemma (in monoid) Units_r_inv [simp]:  ballarin@13936  137  "x \ Units G ==> x \ inv x = \"  paulson@13943  138  apply (unfold Units_def m_inv_def, auto)  ballarin@13936  139  apply (rule theI2, fast)  paulson@13943  140  apply (fast intro: inv_unique, fast)  ballarin@13936  141  done  ballarin@13936  142 ballarin@13936  143 lemma (in monoid) Units_inv_Units [intro, simp]:  ballarin@13936  144  "x \ Units G ==> inv x \ Units G"  ballarin@13936  145 proof -  ballarin@13936  146  assume x: "x \ Units G"  ballarin@13936  147  show "inv x \ Units G"  ballarin@13936  148  by (auto simp add: Units_def  ballarin@13936  149  intro: Units_l_inv Units_r_inv x Units_closed [OF x])  ballarin@13936  150 qed  ballarin@13936  151 ballarin@13936  152 lemma (in monoid) Units_l_cancel [simp]:  ballarin@13936  153  "[| x \ Units G; y \ carrier G; z \ carrier G |] ==>  ballarin@13936  154  (x \ y = x \ z) = (y = z)"  ballarin@13936  155 proof  ballarin@13936  156  assume eq: "x \ y = x \ z"  wenzelm@14693  157  and G: "x \ Units G" "y \ carrier G" "z \ carrier G"  ballarin@13936  158  then have "(inv x \ x) \ y = (inv x \ x) \ z"  ballarin@27698  159  by (simp add: m_assoc Units_closed del: Units_l_inv)  wenzelm@44472  160  with G show "y = z" by simp  ballarin@13936  161 next  ballarin@13936  162  assume eq: "y = z"  wenzelm@14693  163  and G: "x \ Units G" "y \ carrier G" "z \ carrier G"  ballarin@13936  164  then show "x \ y = x \ z" by simp  ballarin@13936  165 qed  ballarin@13936  166 ballarin@13936  167 lemma (in monoid) Units_inv_inv [simp]:  ballarin@13936  168  "x \ Units G ==> inv (inv x) = x"  ballarin@13936  169 proof -  ballarin@13936  170  assume x: "x \ Units G"  ballarin@27698  171  then have "inv x \ inv (inv x) = inv x \ x" by simp  ballarin@27698  172  with x show ?thesis by (simp add: Units_closed del: Units_l_inv Units_r_inv)  ballarin@13936  173 qed  ballarin@13936  174 ballarin@13936  175 lemma (in monoid) inv_inj_on_Units:  ballarin@13936  176  "inj_on (m_inv G) (Units G)"  ballarin@13936  177 proof (rule inj_onI)  ballarin@13936  178  fix x y  wenzelm@14693  179  assume G: "x \ Units G" "y \ Units G" and eq: "inv x = inv y"  ballarin@13936  180  then have "inv (inv x) = inv (inv y)" by simp  ballarin@13936  181  with G show "x = y" by simp  ballarin@13936  182 qed  ballarin@13936  183 ballarin@13940  184 lemma (in monoid) Units_inv_comm:  ballarin@13940  185  assumes inv: "x \ y = \"  wenzelm@14693  186  and G: "x \ Units G" "y \ Units G"  ballarin@13940  187  shows "y \ x = \"  ballarin@13940  188 proof -  ballarin@13940  189  from G have "x \ y \ x = x \ \" by (auto simp add: inv Units_closed)  ballarin@13940  190  with G show ?thesis by (simp del: r_one add: m_assoc Units_closed)  ballarin@13940  191 qed  ballarin@13940  192 Andreas@61628  193 lemma (in monoid) carrier_not_empty: "carrier G \ {}"  Andreas@61628  194 by auto  Andreas@61628  195 wenzelm@61382  196 text \Power\  ballarin@13936  197 ballarin@13936  198 lemma (in monoid) nat_pow_closed [intro, simp]:  nipkow@67341  199  "x \ carrier G ==> x [^] (n::nat) \ carrier G"  ballarin@13936  200  by (induct n) (simp_all add: nat_pow_def)  ballarin@13936  201 ballarin@13936  202 lemma (in monoid) nat_pow_0 [simp]:  nipkow@67341  203  "x [^] (0::nat) = \"  ballarin@13936  204  by (simp add: nat_pow_def)  ballarin@13936  205 ballarin@13936  206 lemma (in monoid) nat_pow_Suc [simp]:  nipkow@67341  207  "x [^] (Suc n) = x [^] n \ x"  ballarin@13936  208  by (simp add: nat_pow_def)  ballarin@13936  209 ballarin@13936  210 lemma (in monoid) nat_pow_one [simp]:  nipkow@67341  211  "\ [^] (n::nat) = \"  ballarin@13936  212  by (induct n) simp_all  ballarin@13936  213 ballarin@13936  214 lemma (in monoid) nat_pow_mult:  nipkow@67341  215  "x \ carrier G ==> x [^] (n::nat) \ x [^] m = x [^] (n + m)"  ballarin@13936  216  by (induct m) (simp_all add: m_assoc [THEN sym])  ballarin@13936  217 ballarin@13936  218 lemma (in monoid) nat_pow_pow:  nipkow@67341  219  "x \ carrier G ==> (x [^] n) [^] m = x [^] (n * m::nat)"  haftmann@57512  220  by (induct m) (simp, simp add: nat_pow_mult add.commute)  ballarin@13936  221 ballarin@27698  222 ballarin@27698  223 (* Jacobson defines submonoid here. *)  ballarin@27698  224 (* Jacobson defines the order of a monoid here. *)  ballarin@27698  225 ballarin@27698  226 wenzelm@61382  227 subsection \Groups\  ballarin@27698  228 wenzelm@61382  229 text \  ballarin@13936  230  A group is a monoid all of whose elements are invertible.  wenzelm@61382  231 \  ballarin@13936  232 ballarin@13936  233 locale group = monoid +  ballarin@13936  234  assumes Units: "carrier G <= Units G"  ballarin@13936  235 wenzelm@26199  236 lemma (in group) is_group: "group G" by (rule group_axioms)  paulson@14761  237 ballarin@13936  238 theorem groupI:  ballarin@19783  239  fixes G (structure)  ballarin@13936  240  assumes m_closed [simp]:  wenzelm@14693  241  "!!x y. [| x \ carrier G; y \ carrier G |] ==> x \ y \ carrier G"  wenzelm@14693  242  and one_closed [simp]: "\ \ carrier G"  ballarin@13936  243  and m_assoc:  ballarin@13936  244  "!!x y z. [| x \ carrier G; y \ carrier G; z \ carrier G |] ==>  wenzelm@14693  245  (x \ y) \ z = x \ (y \ z)"  wenzelm@14693  246  and l_one [simp]: "!!x. x \ carrier G ==> \ \ x = x"  paulson@14963  247  and l_inv_ex: "!!x. x \ carrier G ==> \y \ carrier G. y \ x = \"  ballarin@13936  248  shows "group G"  ballarin@13936  249 proof -  ballarin@13936  250  have l_cancel [simp]:  ballarin@13936  251  "!!x y z. [| x \ carrier G; y \ carrier G; z \ carrier G |] ==>  wenzelm@14693  252  (x \ y = x \ z) = (y = z)"  ballarin@13936  253  proof  ballarin@13936  254  fix x y z  wenzelm@14693  255  assume eq: "x \ y = x \ z"  wenzelm@14693  256  and G: "x \ carrier G" "y \ carrier G" "z \ carrier G"  ballarin@13936  257  with l_inv_ex obtain x_inv where xG: "x_inv \ carrier G"  wenzelm@14693  258  and l_inv: "x_inv \ x = \" by fast  wenzelm@14693  259  from G eq xG have "(x_inv \ x) \ y = (x_inv \ x) \ z"  ballarin@13936  260  by (simp add: m_assoc)  ballarin@13936  261  with G show "y = z" by (simp add: l_inv)  ballarin@13936  262  next  ballarin@13936  263  fix x y z  ballarin@13936  264  assume eq: "y = z"  wenzelm@14693  265  and G: "x \ carrier G" "y \ carrier G" "z \ carrier G"  wenzelm@14693  266  then show "x \ y = x \ z" by simp  ballarin@13936  267  qed  ballarin@13936  268  have r_one:  wenzelm@14693  269  "!!x. x \ carrier G ==> x \ \ = x"  ballarin@13936  270  proof -  ballarin@13936  271  fix x  ballarin@13936  272  assume x: "x \ carrier G"  ballarin@13936  273  with l_inv_ex obtain x_inv where xG: "x_inv \ carrier G"  wenzelm@14693  274  and l_inv: "x_inv \ x = \" by fast  wenzelm@14693  275  from x xG have "x_inv \ (x \ \) = x_inv \ x"  ballarin@13936  276  by (simp add: m_assoc [symmetric] l_inv)  wenzelm@14693  277  with x xG show "x \ \ = x" by simp  ballarin@13936  278  qed  ballarin@13936  279  have inv_ex:  wenzelm@67091  280  "\x. x \ carrier G \ \y \ carrier G. y \ x = \ \ x \ y = \"  ballarin@13936  281  proof -  ballarin@13936  282  fix x  ballarin@13936  283  assume x: "x \ carrier G"  ballarin@13936  284  with l_inv_ex obtain y where y: "y \ carrier G"  wenzelm@14693  285  and l_inv: "y \ x = \" by fast  wenzelm@14693  286  from x y have "y \ (x \ y) = y \ \"  ballarin@13936  287  by (simp add: m_assoc [symmetric] l_inv r_one)  wenzelm@14693  288  with x y have r_inv: "x \ y = \"  ballarin@13936  289  by simp  wenzelm@67091  290  from x y show "\y \ carrier G. y \ x = \ \ x \ y = \"  ballarin@13936  291  by (fast intro: l_inv r_inv)  ballarin@13936  292  qed  wenzelm@67091  293  then have carrier_subset_Units: "carrier G \ Units G"  ballarin@13936  294  by (unfold Units_def) fast  wenzelm@61169  295  show ?thesis  wenzelm@61169  296  by standard (auto simp: r_one m_assoc carrier_subset_Units)  ballarin@13936  297 qed  ballarin@13936  298 ballarin@27698  299 lemma (in monoid) group_l_invI:  ballarin@13936  300  assumes l_inv_ex:  paulson@14963  301  "!!x. x \ carrier G ==> \y \ carrier G. y \ x = \"  ballarin@13936  302  shows "group G"  ballarin@13936  303  by (rule groupI) (auto intro: m_assoc l_inv_ex)  ballarin@13936  304 ballarin@13936  305 lemma (in group) Units_eq [simp]:  ballarin@13936  306  "Units G = carrier G"  ballarin@13936  307 proof  wenzelm@67091  308  show "Units G \ carrier G" by fast  ballarin@13936  309 next  wenzelm@67091  310  show "carrier G \ Units G" by (rule Units)  ballarin@13936  311 qed  ballarin@13936  312 ballarin@13936  313 lemma (in group) inv_closed [intro, simp]:  ballarin@13936  314  "x \ carrier G ==> inv x \ carrier G"  ballarin@13936  315  using Units_inv_closed by simp  ballarin@13936  316 ballarin@19981  317 lemma (in group) l_inv_ex [simp]:  ballarin@19981  318  "x \ carrier G ==> \y \ carrier G. y \ x = \"  ballarin@19981  319  using Units_l_inv_ex by simp  ballarin@19981  320 ballarin@19981  321 lemma (in group) r_inv_ex [simp]:  ballarin@19981  322  "x \ carrier G ==> \y \ carrier G. x \ y = \"  ballarin@19981  323  using Units_r_inv_ex by simp  ballarin@19981  324 paulson@14963  325 lemma (in group) l_inv [simp]:  ballarin@13936  326  "x \ carrier G ==> inv x \ x = \"  lp15@68399  327  by simp  ballarin@13813  328 ballarin@20318  329 wenzelm@61382  330 subsection \Cancellation Laws and Basic Properties\  ballarin@13813  331 paulson@14963  332 lemma (in group) r_inv [simp]:  ballarin@13813  333  "x \ carrier G ==> x \ inv x = \"  lp15@68399  334  by simp  ballarin@13813  335 lp15@68399  336 lemma (in group) right_cancel [simp]:  ballarin@13813  337  "[| x \ carrier G; y \ carrier G; z \ carrier G |] ==>  ballarin@13813  338  (y \ x = z \ x) = (y = z)"  lp15@68399  339  by (metis inv_closed m_assoc r_inv r_one)  ballarin@13813  340 ballarin@13854  341 lemma (in group) inv_one [simp]:  ballarin@13854  342  "inv \ = \"  ballarin@13854  343 proof -  ballarin@27698  344  have "inv \ = \ \ (inv \)" by (simp del: r_inv Units_r_inv)  paulson@14963  345  moreover have "... = \" by simp  ballarin@13854  346  finally show ?thesis .  ballarin@13854  347 qed  ballarin@13854  348 ballarin@13813  349 lemma (in group) inv_inv [simp]:  ballarin@13813  350  "x \ carrier G ==> inv (inv x) = x"  ballarin@13936  351  using Units_inv_inv by simp  ballarin@13936  352 ballarin@13936  353 lemma (in group) inv_inj:  ballarin@13936  354  "inj_on (m_inv G) (carrier G)"  ballarin@13936  355  using inv_inj_on_Units by simp  ballarin@13813  356 ballarin@13854  357 lemma (in group) inv_mult_group:  ballarin@13813  358  "[| x \ carrier G; y \ carrier G |] ==> inv (x \ y) = inv y \ inv x"  ballarin@13813  359 proof -  wenzelm@14693  360  assume G: "x \ carrier G" "y \ carrier G"  ballarin@13813  361  then have "inv (x \ y) \ (x \ y) = (inv y \ inv x) \ (x \ y)"  wenzelm@44472  362  by (simp add: m_assoc) (simp add: m_assoc [symmetric])  ballarin@27698  363  with G show ?thesis by (simp del: l_inv Units_l_inv)  ballarin@13813  364 qed  ballarin@13813  365 ballarin@13940  366 lemma (in group) inv_comm:  ballarin@13940  367  "[| x \ y = \; x \ carrier G; y \ carrier G |] ==> y \ x = \"  wenzelm@14693  368  by (rule Units_inv_comm) auto  ballarin@13940  369 paulson@13944  370 lemma (in group) inv_equality:  paulson@13943  371  "[|y \ x = \; x \ carrier G; y \ carrier G|] ==> inv x = y"  lp15@68399  372  using inv_unique r_inv by blast  paulson@13943  373 ballarin@57271  374 (* Contributed by Joachim Breitner *)  ballarin@57271  375 lemma (in group) inv_solve_left:  ballarin@57271  376  "\ a \ carrier G; b \ carrier G; c \ carrier G \ \ a = inv b \ c \ c = b \ a"  ballarin@57271  377  by (metis inv_equality l_inv_ex l_one m_assoc r_inv)  ballarin@57271  378 lemma (in group) inv_solve_right:  ballarin@57271  379  "\ a \ carrier G; b \ carrier G; c \ carrier G \ \ a = b \ inv c \ b = a \ c"  ballarin@57271  380  by (metis inv_equality l_inv_ex l_one m_assoc r_inv)  ballarin@57271  381 wenzelm@61382  382 text \Power\  ballarin@13936  383 ballarin@13936  384 lemma (in group) int_pow_def2:  nipkow@67341  385  "a [^] (z::int) = (if z < 0 then inv (a [^] (nat (-z))) else a [^] (nat z))"  ballarin@13936  386  by (simp add: int_pow_def nat_pow_def Let_def)  ballarin@13936  387 ballarin@13936  388 lemma (in group) int_pow_0 [simp]:  nipkow@67341  389  "x [^] (0::int) = \"  ballarin@13936  390  by (simp add: int_pow_def2)  ballarin@13936  391 ballarin@13936  392 lemma (in group) int_pow_one [simp]:  nipkow@67341  393  "\ [^] (z::int) = \"  ballarin@13936  394  by (simp add: int_pow_def2)  ballarin@13936  395 ballarin@57271  396 (* The following are contributed by Joachim Breitner *)  ballarin@20318  397 ballarin@57271  398 lemma (in group) int_pow_closed [intro, simp]:  nipkow@67341  399  "x \ carrier G ==> x [^] (i::int) \ carrier G"  ballarin@57271  400  by (simp add: int_pow_def2)  ballarin@57271  401 ballarin@57271  402 lemma (in group) int_pow_1 [simp]:  nipkow@67341  403  "x \ carrier G \ x [^] (1::int) = x"  ballarin@57271  404  by (simp add: int_pow_def2)  ballarin@57271  405 ballarin@57271  406 lemma (in group) int_pow_neg:  nipkow@67341  407  "x \ carrier G \ x [^] (-i::int) = inv (x [^] i)"  ballarin@57271  408  by (simp add: int_pow_def2)  ballarin@57271  409 ballarin@57271  410 lemma (in group) int_pow_mult:  nipkow@67341  411  "x \ carrier G \ x [^] (i + j::int) = x [^] i \ x [^] j"  ballarin@57271  412 proof -  ballarin@57271  413  have [simp]: "-i - j = -j - i" by simp  wenzelm@67613  414  assume "x \ carrier G" then  ballarin@57271  415  show ?thesis  ballarin@57271  416  by (auto simp add: int_pow_def2 inv_solve_left inv_solve_right nat_add_distrib [symmetric] nat_pow_mult )  ballarin@57271  417 qed  ballarin@57271  418 Andreas@61628  419 lemma (in group) int_pow_diff:  nipkow@67341  420  "x \ carrier G \ x [^] (n - m :: int) = x [^] n \ inv (x [^] m)"  Andreas@61628  421 by(simp only: diff_conv_add_uminus int_pow_mult int_pow_neg)  Andreas@61628  422 Andreas@61628  423 lemma (in group) inj_on_multc: "c \ carrier G \ inj_on (\x. x \ c) (carrier G)"  Andreas@61628  424 by(simp add: inj_on_def)  Andreas@61628  425 Andreas@61628  426 lemma (in group) inj_on_cmult: "c \ carrier G \ inj_on (\x. c \ x) (carrier G)"  Andreas@61628  427 by(simp add: inj_on_def)  Andreas@61628  428 wenzelm@61382  429 subsection \Subgroups\  ballarin@13813  430 ballarin@19783  431 locale subgroup =  ballarin@19783  432  fixes H and G (structure)  paulson@14963  433  assumes subset: "H \ carrier G"  paulson@14963  434  and m_closed [intro, simp]: "\x \ H; y \ H\ \ x \ y \ H"  ballarin@20318  435  and one_closed [simp]: "\ \ H"  paulson@14963  436  and m_inv_closed [intro,simp]: "x \ H \ inv x \ H"  ballarin@13813  437 ballarin@20318  438 lemma (in subgroup) is_subgroup:  wenzelm@26199  439  "subgroup H G" by (rule subgroup_axioms)  ballarin@20318  440 ballarin@13813  441 declare (in subgroup) group.intro [intro]  ballarin@13949  442 paulson@14963  443 lemma (in subgroup) mem_carrier [simp]:  paulson@14963  444  "x \ H \ x \ carrier G"  paulson@14963  445  using subset by blast  ballarin@13813  446 paulson@14963  447 lemma subgroup_imp_subset:  paulson@14963  448  "subgroup H G \ H \ carrier G"  paulson@14963  449  by (rule subgroup.subset)  paulson@14963  450 paulson@14963  451 lemma (in subgroup) subgroup_is_group [intro]:  ballarin@27611  452  assumes "group G"  ballarin@27611  453  shows "group (G\carrier := H\)"  ballarin@27611  454 proof -  ballarin@29237  455  interpret group G by fact  ballarin@27611  456  show ?thesis  ballarin@27698  457  apply (rule monoid.group_l_invI)  ballarin@27698  458  apply (unfold_locales) [1]  ballarin@27698  459  apply (auto intro: m_assoc l_inv mem_carrier)  ballarin@27698  460  done  ballarin@27611  461 qed  ballarin@13813  462 wenzelm@61382  463 text \  ballarin@13813  464  Since @{term H} is nonempty, it contains some element @{term x}. Since  wenzelm@63167  465  it is closed under inverse, it contains \inv x\. Since  wenzelm@63167  466  it is closed under product, it contains \x \ inv x = \\.  wenzelm@61382  467 \  ballarin@13813  468 ballarin@13813  469 lemma (in group) one_in_subset:  ballarin@13813  470  "[| H \ carrier G; H \ {}; \a \ H. inv a \ H; \a\H. \b\H. a \ b \ H |]  ballarin@13813  471  ==> \ \ H"  wenzelm@44472  472 by force  ballarin@13813  473 wenzelm@61382  474 text \A characterization of subgroups: closed, non-empty subset.\  ballarin@13813  475 ballarin@13813  476 lemma (in group) subgroupI:  ballarin@13813  477  assumes subset: "H \ carrier G" and non_empty: "H \ {}"  paulson@14963  478  and inv: "!!a. a \ H \ inv a \ H"  paulson@14963  479  and mult: "!!a b. \a \ H; b \ H\ \ a \ b \ H"  ballarin@13813  480  shows "subgroup H G"  ballarin@27714  481 proof (simp add: subgroup_def assms)  ballarin@27714  482  show "\ \ H" by (rule one_in_subset) (auto simp only: assms)  ballarin@13813  483 qed  ballarin@13813  484 ballarin@13936  485 declare monoid.one_closed [iff] group.inv_closed [simp]  ballarin@13936  486  monoid.l_one [simp] monoid.r_one [simp] group.inv_inv [simp]  ballarin@13813  487 ballarin@13813  488 lemma subgroup_nonempty:  wenzelm@67091  489  "\ subgroup {} G"  ballarin@13813  490  by (blast dest: subgroup.one_closed)  ballarin@13813  491 ballarin@13813  492 lemma (in subgroup) finite_imp_card_positive:  ballarin@13813  493  "finite (carrier G) ==> 0 < card H"  ballarin@13813  494 proof (rule classical)  wenzelm@67091  495  assume "finite (carrier G)" and a: "\ 0 < card H"  paulson@14963  496  then have "finite H" by (blast intro: finite_subset [OF subset])  wenzelm@41528  497  with is_subgroup a have "subgroup {} G" by simp  ballarin@13813  498  with subgroup_nonempty show ?thesis by contradiction  ballarin@13813  499 qed  ballarin@13813  500 ballarin@13936  501 (*  ballarin@13936  502 lemma (in monoid) Units_subgroup:  ballarin@13936  503  "subgroup (Units G) G"  ballarin@13936  504 *)  ballarin@13936  505 ballarin@20318  506 wenzelm@61382  507 subsection \Direct Products\  ballarin@13813  508 wenzelm@35848  509 definition  wenzelm@35848  510  DirProd :: "_ \ _ \ ('a \ 'b) monoid" (infixr "\\" 80) where  wenzelm@35848  511  "G \\ H =  wenzelm@35848  512  \carrier = carrier G \ carrier H,  wenzelm@35848  513  mult = ($$g, h) (g', h'). (g \\<^bsub>G\<^esub> g', h \\<^bsub>H\<^esub> h')),  wenzelm@35848  514  one = (\\<^bsub>G\<^esub>, \\<^bsub>H\<^esub>)\"  ballarin@13813  515 paulson@14963  516 lemma DirProd_monoid:  ballarin@27611  517  assumes "monoid G" and "monoid H"  paulson@14963  518  shows "monoid (G \\ H)"  paulson@14963  519 proof -  wenzelm@30729  520  interpret G: monoid G by fact  wenzelm@30729  521  interpret H: monoid H by fact  ballarin@27714  522  from assms  paulson@14963  523  show ?thesis by (unfold monoid_def DirProd_def, auto)  paulson@14963  524 qed  ballarin@13813  525 ballarin@13813  526 wenzelm@61382  527 text\Does not use the previous result because it's easier just to use auto.\  paulson@14963  528 lemma DirProd_group:  ballarin@27611  529  assumes "group G" and "group H"  paulson@14963  530  shows "group (G \\ H)"  ballarin@27611  531 proof -  wenzelm@30729  532  interpret G: group G by fact  wenzelm@30729  533  interpret H: group H by fact  ballarin@27611  534  show ?thesis by (rule groupI)  paulson@14963  535  (auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv  paulson@14963  536  simp add: DirProd_def)  ballarin@27611  537 qed  ballarin@13813  538 paulson@14963  539 lemma carrier_DirProd [simp]:  paulson@14963  540  "carrier (G \\ H) = carrier G \ carrier H"  paulson@14963  541  by (simp add: DirProd_def)  paulson@13944  542 paulson@14963  543 lemma one_DirProd [simp]:  paulson@14963  544  "\\<^bsub>G \\ H\<^esub> = (\\<^bsub>G\<^esub>, \\<^bsub>H\<^esub>)"  paulson@14963  545  by (simp add: DirProd_def)  paulson@13944  546 paulson@14963  547 lemma mult_DirProd [simp]:  paulson@14963  548  "(g, h) \\<^bsub>(G \\ H)\<^esub> (g', h') = (g \\<^bsub>G\<^esub> g', h \\<^bsub>H\<^esub> h')"  paulson@14963  549  by (simp add: DirProd_def)  paulson@13944  550 paulson@14963  551 lemma inv_DirProd [simp]:  ballarin@27611  552  assumes "group G" and "group H"  paulson@13944  553  assumes g: "g \ carrier G"  paulson@13944  554  and h: "h \ carrier H"  paulson@14963  555  shows "m_inv (G \\ H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"  ballarin@27611  556 proof -  wenzelm@30729  557  interpret G: group G by fact  wenzelm@30729  558  interpret H: group H by fact  wenzelm@30729  559  interpret Prod: group "G \\ H"  ballarin@27714  560  by (auto intro: DirProd_group group.intro group.axioms assms)  paulson@14963  561  show ?thesis by (simp add: Prod.inv_equality g h)  paulson@14963  562 qed  ballarin@27698  563 paulson@14963  564 wenzelm@61382  565 subsection \Homomorphisms and Isomorphisms\  ballarin@13813  566 wenzelm@35847  567 definition  wenzelm@35847  568  hom :: "_ => _ => ('a => 'b) set" where  wenzelm@35848  569  "hom G H =  wenzelm@67091  570  {h. h \ carrier G \ carrier H \  wenzelm@14693  571  (\x \ carrier G. \y \ carrier G. h (x \\<^bsub>G\<^esub> y) = h x \\<^bsub>H\<^esub> h y)}"  ballarin@13813  572 paulson@14761  573 lemma (in group) hom_compose:  nipkow@31754  574  "[|h \ hom G H; i \ hom H I|] ==> compose (carrier G) i h \ hom G I"  nipkow@44890  575 by (fastforce simp add: hom_def compose_def)  paulson@13943  576 wenzelm@35848  577 definition  wenzelm@35848  578  iso :: "_ => _ => ('a => 'b) set" (infixr "\" 60)  wenzelm@67091  579  where "G \ H = {h. h \ hom G H \ bij_betw h (carrier G) (carrier H)}"  paulson@14761  580 wenzelm@67091  581 lemma iso_refl: "(\x. x) \ G \ G"  nipkow@31727  582 by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)  paulson@14761  583 paulson@14761  584 lemma (in group) iso_sym:  nipkow@33057  585  "h \ G \ H \ inv_into (carrier G) h \ H \ G"  nipkow@33057  586 apply (simp add: iso_def bij_betw_inv_into)  nipkow@33057  587 apply (subgoal_tac "inv_into (carrier G) h \ carrier H \ carrier G")  nipkow@33057  588  prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_inv_into])  nipkow@33057  589 apply (simp add: hom_def bij_betw_def inv_into_f_eq f_inv_into_f Pi_def)  paulson@14761  590 done  paulson@14761  591 paulson@14761  592 lemma (in group) iso_trans:  paulson@14803  593  "[|h \ G \ H; i \ H \ I|] ==> (compose (carrier G) i h) \ G \ I"  paulson@14761  594 by (auto simp add: iso_def hom_compose bij_betw_compose)  paulson@14761  595 paulson@14963  596 lemma DirProd_commute_iso:  paulson@14963  597  shows "(\(x,y). (y,x)) \ (G \\ H) \ (H \\ G)"  nipkow@31754  598 by (auto simp add: iso_def hom_def inj_on_def bij_betw_def)  paulson@14761  599 paulson@14963  600 lemma DirProd_assoc_iso:  paulson@14963  601  shows "(\(x,y,z). (x,(y,z))) \ (G \\ H \\ I) \ (G \\ (H \\ I))"  nipkow@31727  602 by (auto simp add: iso_def hom_def inj_on_def bij_betw_def)  paulson@14761  603 paulson@14761  604 wenzelm@61382  605 text\Basis for homomorphism proofs: we assume two groups @{term G} and  wenzelm@61382  606  @{term H}, with a homomorphism @{term h} between them\  ballarin@61565  607 locale group_hom = G?: group G + H?: group H for G (structure) and H (structure) +  ballarin@29237  608  fixes h  ballarin@13813  609  assumes homh: "h \ hom G H"  ballarin@29240  610 ballarin@29240  611 lemma (in group_hom) hom_mult [simp]:  ballarin@29240  612  "[| x \ carrier G; y \ carrier G |] ==> h (x \\<^bsub>G\<^esub> y) = h x \\<^bsub>H\<^esub> h y"  ballarin@29240  613 proof -  ballarin@29240  614  assume "x \ carrier G" "y \ carrier G"  ballarin@29240  615  with homh [unfolded hom_def] show ?thesis by simp  ballarin@29240  616 qed  ballarin@29240  617 ballarin@29240  618 lemma (in group_hom) hom_closed [simp]:  ballarin@29240  619  "x \ carrier G ==> h x \ carrier H"  ballarin@29240  620 proof -  ballarin@29240  621  assume "x \ carrier G"  nipkow@31754  622  with homh [unfolded hom_def] show ?thesis by auto  ballarin@29240  623 qed  ballarin@13813  624 ballarin@13813  625 lemma (in group_hom) one_closed [simp]:  ballarin@13813  626  "h \ \ carrier H"  ballarin@13813  627  by simp  ballarin@13813  628 ballarin@13813  629 lemma (in group_hom) hom_one [simp]:  wenzelm@14693  630  "h \ = \\<^bsub>H\<^esub>"  ballarin@13813  631 proof -  ballarin@15076  632  have "h \ \\<^bsub>H\<^esub> \\<^bsub>H\<^esub> = h \ \\<^bsub>H\<^esub> h \"  ballarin@13813  633  by (simp add: hom_mult [symmetric] del: hom_mult)  ballarin@13813  634  then show ?thesis by (simp del: r_one)  ballarin@13813  635 qed  ballarin@13813  636 ballarin@13813  637 lemma (in group_hom) inv_closed [simp]:  ballarin@13813  638  "x \ carrier G ==> h (inv x) \ carrier H"  ballarin@13813  639  by simp  ballarin@13813  640 ballarin@13813  641 lemma (in group_hom) hom_inv [simp]:  wenzelm@14693  642  "x \ carrier G ==> h (inv x) = inv\<^bsub>H\<^esub> (h x)"  ballarin@13813  643 proof -  ballarin@13813  644  assume x: "x \ carrier G"  wenzelm@14693  645  then have "h x \\<^bsub>H\<^esub> h (inv x) = \\<^bsub>H\<^esub>"  paulson@14963  646  by (simp add: hom_mult [symmetric] del: hom_mult)  wenzelm@14693  647  also from x have "... = h x \\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h x)"  paulson@14963  648  by (simp add: hom_mult [symmetric] del: hom_mult)  wenzelm@14693  649  finally have "h x \\<^bsub>H\<^esub> h (inv x) = h x \\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h x)" .  ballarin@27698  650  with x show ?thesis by (simp del: H.r_inv H.Units_r_inv)  ballarin@13813  651 qed  ballarin@13813  652 ballarin@57271  653 (* Contributed by Joachim Breitner *)  ballarin@57271  654 lemma (in group) int_pow_is_hom:  nipkow@67399  655  "x \ carrier G \ (([^]) x) \ hom \ carrier = UNIV, mult = (+), one = 0::int \ G "  ballarin@57271  656  unfolding hom_def by (simp add: int_pow_mult)  ballarin@57271  657 ballarin@20318  658 wenzelm@61382  659 subsection \Commutative Structures\  ballarin@13936  660 wenzelm@61382  661 text \  ballarin@13936  662  Naming convention: multiplicative structures that are commutative  ballarin@13936  663  are called \emph{commutative}, additive structures are called  ballarin@13936  664  \emph{Abelian}.  wenzelm@61382  665 \  ballarin@13813  666 paulson@14963  667 locale comm_monoid = monoid +  paulson@14963  668  assumes m_comm: "\x \ carrier G; y \ carrier G\ \ x \ y = y \ x"  ballarin@13813  669 paulson@14963  670 lemma (in comm_monoid) m_lcomm:  paulson@14963  671  "\x \ carrier G; y \ carrier G; z \ carrier G\ \  ballarin@13813  672  x \ (y \ z) = y \ (x \ z)"  ballarin@13813  673 proof -  wenzelm@14693  674  assume xyz: "x \ carrier G" "y \ carrier G" "z \ carrier G"  ballarin@13813  675  from xyz have "x \ (y \ z) = (x \ y) \ z" by (simp add: m_assoc)  ballarin@13813  676  also from xyz have "... = (y \ x) \ z" by (simp add: m_comm)  ballarin@13813  677  also from xyz have "... = y \ (x \ z)" by (simp add: m_assoc)  ballarin@13813  678  finally show ?thesis .  ballarin@13813  679 qed  ballarin@13813  680 paulson@14963  681 lemmas (in comm_monoid) m_ac = m_assoc m_comm m_lcomm  ballarin@13813  682 ballarin@13936  683 lemma comm_monoidI:  ballarin@19783  684  fixes G (structure)  ballarin@13936  685  assumes m_closed:  wenzelm@14693  686  "!!x y. [| x \ carrier G; y \ carrier G |] ==> x \ y \ carrier G"  wenzelm@14693  687  and one_closed: "\ \ carrier G"  ballarin@13936  688  and m_assoc:  ballarin@13936  689  "!!x y z. [| x \ carrier G; y \ carrier G; z \ carrier G |] ==>  wenzelm@14693  690  (x \ y) \ z = x \ (y \ z)"  wenzelm@14693  691  and l_one: "!!x. x \ carrier G ==> \ \ x = x"  ballarin@13936  692  and m_comm:  wenzelm@14693  693  "!!x y. [| x \ carrier G; y \ carrier G |] ==> x \ y = y \ x"  ballarin@13936  694  shows "comm_monoid G"  ballarin@13936  695  using l_one  paulson@14963  696  by (auto intro!: comm_monoid.intro comm_monoid_axioms.intro monoid.intro  ballarin@27714  697  intro: assms simp: m_closed one_closed m_comm)  ballarin@13817  698 ballarin@13936  699 lemma (in monoid) monoid_comm_monoidI:  ballarin@13936  700  assumes m_comm:  wenzelm@14693  701  "!!x y. [| x \ carrier G; y \ carrier G |] ==> x \ y = y \ x"  ballarin@13936  702  shows "comm_monoid G"  ballarin@13936  703  by (rule comm_monoidI) (auto intro: m_assoc m_comm)  paulson@14963  704 wenzelm@14693  705 (*lemma (in comm_monoid) r_one [simp]:  ballarin@13817  706  "x \ carrier G ==> x \ \ = x"  ballarin@13817  707 proof -  ballarin@13817  708  assume G: "x \ carrier G"  ballarin@13817  709  then have "x \ \ = \ \ x" by (simp add: m_comm)  ballarin@13817  710  also from G have "... = x" by simp  ballarin@13817  711  finally show ?thesis .  wenzelm@14693  712 qed*)  paulson@14963  713 ballarin@13936  714 lemma (in comm_monoid) nat_pow_distr:  ballarin@13936  715  "[| x \ carrier G; y \ carrier G |] ==>  nipkow@67341  716  (x \ y) [^] (n::nat) = x [^] n \ y [^] n"  ballarin@13936  717  by (induct n) (simp, simp add: m_ac)  ballarin@13936  718 ballarin@13936  719 locale comm_group = comm_monoid + group  ballarin@13936  720 ballarin@13936  721 lemma (in group) group_comm_groupI:  ballarin@13936  722  assumes m_comm: "!!x y. [| x \ carrier G; y \ carrier G |] ==>  wenzelm@14693  723  x \ y = y \ x"  ballarin@13936  724  shows "comm_group G"  wenzelm@61169  725  by standard (simp_all add: m_comm)  ballarin@13817  726 ballarin@13936  727 lemma comm_groupI:  ballarin@19783  728  fixes G (structure)  ballarin@13936  729  assumes m_closed:  wenzelm@14693  730  "!!x y. [| x \ carrier G; y \ carrier G |] ==> x \ y \ carrier G"  wenzelm@14693  731  and one_closed: "\ \ carrier G"  ballarin@13936  732  and m_assoc:  ballarin@13936  733  "!!x y z. [| x \ carrier G; y \ carrier G; z \ carrier G |] ==>  wenzelm@14693  734  (x \ y) \ z = x \ (y \ z)"  ballarin@13936  735  and m_comm:  wenzelm@14693  736  "!!x y. [| x \ carrier G; y \ carrier G |] ==> x \ y = y \ x"  wenzelm@14693  737  and l_one: "!!x. x \ carrier G ==> \ \ x = x"  paulson@14963  738  and l_inv_ex: "!!x. x \ carrier G ==> \y \ carrier G. y \ x = \"  ballarin@13936  739  shows "comm_group G"  ballarin@27714  740  by (fast intro: group.group_comm_groupI groupI assms)  ballarin@13936  741 ballarin@13936  742 lemma (in comm_group) inv_mult:  ballarin@13854  743  "[| x \ carrier G; y \ carrier G |] ==> inv (x \ y) = inv x \ inv y"  ballarin@13936  744  by (simp add: m_ac inv_mult_group)  ballarin@13854  745 ballarin@20318  746 wenzelm@61382  747 subsection \The Lattice of Subgroups of a Group\  ballarin@14751  748 wenzelm@61382  749 text_raw \\label{sec:subgroup-lattice}\  ballarin@14751  750 ballarin@14751  751 theorem (in group) subgroups_partial_order:  nipkow@67399  752  "partial_order \carrier = {H. subgroup H G}, eq = (=), le = ($$\"  wenzelm@61169  753  by standard simp_all  ballarin@14751  754 ballarin@14751  755 lemma (in group) subgroup_self:  ballarin@14751  756  "subgroup (carrier G) G"  ballarin@14751  757  by (rule subgroupI) auto  ballarin@14751  758 ballarin@14751  759 lemma (in group) subgroup_imp_group:  wenzelm@55926  760  "subgroup H G ==> group (G\carrier := H\)"  wenzelm@26199  761  by (erule subgroup.subgroup_is_group) (rule group_axioms)  ballarin@14751  762 ballarin@14751  763 lemma (in group) is_monoid [intro, simp]:  ballarin@14751  764  "monoid G"  paulson@14963  765  by (auto intro: monoid.intro m_assoc)  ballarin@14751  766 ballarin@14751  767 lemma (in group) subgroup_inv_equality:  wenzelm@55926  768  "[| subgroup H G; x \ H |] ==> m_inv (G \carrier := H\) x = inv x"  ballarin@14751  769 apply (rule_tac inv_equality [THEN sym])  paulson@14761  770  apply (rule group.l_inv [OF subgroup_imp_group, simplified], assumption+)  paulson@14761  771  apply (rule subsetD [OF subgroup.subset], assumption+)  paulson@14761  772 apply (rule subsetD [OF subgroup.subset], assumption)  paulson@14761  773 apply (rule_tac group.inv_closed [OF subgroup_imp_group, simplified], assumption+)  ballarin@14751  774 done  ballarin@14751  775 ballarin@14751  776 theorem (in group) subgroups_Inter:  wenzelm@67091  777  assumes subgr: "(\H. H \ A \ subgroup H G)"  wenzelm@67091  778  and not_empty: "A \ {}"  ballarin@14751  779  shows "subgroup (\A) G"  ballarin@14751  780 proof (rule subgroupI)  ballarin@14751  781  from subgr [THEN subgroup.subset] and not_empty  ballarin@14751  782  show "\A \ carrier G" by blast  ballarin@14751  783 next  ballarin@14751  784  from subgr [THEN subgroup.one_closed]  wenzelm@67091  785  show "\A \ {}" by blast  ballarin@14751  786 next  ballarin@14751  787  fix x assume "x \ \A"  ballarin@14751  788  with subgr [THEN subgroup.m_inv_closed]  ballarin@14751  789  show "inv x \ \A" by blast  ballarin@14751  790 next  ballarin@14751  791  fix x y assume "x \ \A" "y \ \A"  ballarin@14751  792  with subgr [THEN subgroup.m_closed]  ballarin@14751  793  show "x \ y \ \A" by blast  ballarin@14751  794 qed  ballarin@14751  795 ballarin@66579  796 theorem (in group) subgroups_complete_lattice:  nipkow@67399  797  "complete_lattice \carrier = {H. subgroup H G}, eq = (=), le = (\)\"  ballarin@66579  798  (is "complete_lattice ?L")  ballarin@66579  799 proof (rule partial_order.complete_lattice_criterion1)  ballarin@66579  800  show "partial_order ?L" by (rule subgroups_partial_order)  ballarin@66579  801 next  ballarin@66579  802  have "greatest ?L (carrier G) (carrier ?L)"  ballarin@66579  803  by (unfold greatest_def) (simp add: subgroup.subset subgroup_self)  ballarin@66579  804  then show "\G. greatest ?L G (carrier ?L)" ..  ballarin@66579  805 next  ballarin@66579  806  fix A  wenzelm@67091  807  assume L: "A \ carrier ?L" and non_empty: "A \ {}"  ballarin@66579  808  then have Int_subgroup: "subgroup (\A) G"  ballarin@66579  809  by (fastforce intro: subgroups_Inter)  ballarin@66579  810  have "greatest ?L (\A) (Lower ?L A)" (is "greatest _ ?Int _")  ballarin@66579  811  proof (rule greatest_LowerI)  ballarin@66579  812  fix H  ballarin@66579  813  assume H: "H \ A"  ballarin@66579  814  with L have subgroupH: "subgroup H G" by auto  ballarin@66579  815  from subgroupH have groupH: "group (G \carrier := H\)" (is "group ?H")  ballarin@66579  816  by (rule subgroup_imp_group)  ballarin@66579  817  from groupH have monoidH: "monoid ?H"  ballarin@66579  818  by (rule group.is_monoid)  ballarin@66579  819  from H have Int_subset: "?Int \ H" by fastforce  ballarin@66579  820  then show "le ?L ?Int H" by simp  ballarin@66579  821  next  ballarin@66579  822  fix H  ballarin@66579  823  assume H: "H \ Lower ?L A"  ballarin@66579  824  with L Int_subgroup show "le ?L H ?Int"  ballarin@66579  825  by (fastforce simp: Lower_def intro: Inter_greatest)  ballarin@66579  826  next  ballarin@66579  827  show "A \ carrier ?L" by (rule L)  ballarin@66579  828  next  ballarin@66579  829  show "?Int \ carrier ?L" by simp (rule Int_subgroup)  ballarin@66579  830  qed  ballarin@66579  831  then show "\I. greatest ?L I (Lower ?L A)" ..  ballarin@66579  832 qed  ballarin@66579  833 ballarin@13813  834 end