src/HOL/Algebra/Group.thy
 author wenzelm Tue Oct 10 19:23:03 2017 +0200 (2017-10-10) changeset 66831 29ea2b900a05 parent 66579 2db3fe23fdaf child 67091 1393c2340eec permissions -rw-r--r--
tuned: each session has at most one defining entry;
 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  ballarin@66579  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@35848  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@63167  29  \\The set of invertible elements\  wenzelm@35848  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  huffman@47108  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 Andreas@61628  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@63167  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]:  ballarin@13936  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]:  ballarin@13936  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]:  ballarin@13936  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]:  ballarin@13936  211  "\ (^) (n::nat) = \"  ballarin@13936  212  by (induct n) simp_all  ballarin@13936  213 ballarin@13936  214 lemma (in monoid) nat_pow_mult:  ballarin@13936  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:  ballarin@13936  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:  paulson@14963  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  paulson@14963  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  ballarin@13936  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  ballarin@13936  308  show "Units G <= carrier G" by fast  ballarin@13936  309 next  ballarin@13936  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 = \"  ballarin@13936  327  using Units_l_inv by simp  ballarin@13813  328 ballarin@20318  329 wenzelm@61382  330 subsection \Cancellation Laws and Basic Properties\  ballarin@13813  331 ballarin@13813  332 lemma (in group) l_cancel [simp]:  ballarin@13813  333  "[| x \ carrier G; y \ carrier G; z \ carrier G |] ==>  ballarin@13813  334  (x \ y = x \ z) = (y = z)"  ballarin@13936  335  using Units_l_inv by simp  ballarin@13940  336 paulson@14963  337 lemma (in group) r_inv [simp]:  ballarin@13813  338  "x \ carrier G ==> x \ inv x = \"  ballarin@13813  339 proof -  ballarin@13813  340  assume x: "x \ carrier G"  ballarin@13813  341  then have "inv x \ (x \ inv x) = inv x \ \"  wenzelm@44472  342  by (simp add: m_assoc [symmetric])  ballarin@13813  343  with x show ?thesis by (simp del: r_one)  ballarin@13813  344 qed  ballarin@13813  345 ballarin@13813  346 lemma (in group) r_cancel [simp]:  ballarin@13813  347  "[| x \ carrier G; y \ carrier G; z \ carrier G |] ==>  ballarin@13813  348  (y \ x = z \ x) = (y = z)"  ballarin@13813  349 proof  ballarin@13813  350  assume eq: "y \ x = z \ x"  wenzelm@14693  351  and G: "x \ carrier G" "y \ carrier G" "z \ carrier G"  ballarin@13813  352  then have "y \ (x \ inv x) = z \ (x \ inv x)"  ballarin@27698  353  by (simp add: m_assoc [symmetric] del: r_inv Units_r_inv)  paulson@14963  354  with G show "y = z" by simp  ballarin@13813  355 next  ballarin@13813  356  assume eq: "y = z"  wenzelm@14693  357  and G: "x \ carrier G" "y \ carrier G" "z \ carrier G"  ballarin@13813  358  then show "y \ x = z \ x" by simp  ballarin@13813  359 qed  ballarin@13813  360 ballarin@13854  361 lemma (in group) inv_one [simp]:  ballarin@13854  362  "inv \ = \"  ballarin@13854  363 proof -  ballarin@27698  364  have "inv \ = \ \ (inv \)" by (simp del: r_inv Units_r_inv)  paulson@14963  365  moreover have "... = \" by simp  ballarin@13854  366  finally show ?thesis .  ballarin@13854  367 qed  ballarin@13854  368 ballarin@13813  369 lemma (in group) inv_inv [simp]:  ballarin@13813  370  "x \ carrier G ==> inv (inv x) = x"  ballarin@13936  371  using Units_inv_inv by simp  ballarin@13936  372 ballarin@13936  373 lemma (in group) inv_inj:  ballarin@13936  374  "inj_on (m_inv G) (carrier G)"  ballarin@13936  375  using inv_inj_on_Units by simp  ballarin@13813  376 ballarin@13854  377 lemma (in group) inv_mult_group:  ballarin@13813  378  "[| x \ carrier G; y \ carrier G |] ==> inv (x \ y) = inv y \ inv x"  ballarin@13813  379 proof -  wenzelm@14693  380  assume G: "x \ carrier G" "y \ carrier G"  ballarin@13813  381  then have "inv (x \ y) \ (x \ y) = (inv y \ inv x) \ (x \ y)"  wenzelm@44472  382  by (simp add: m_assoc) (simp add: m_assoc [symmetric])  ballarin@27698  383  with G show ?thesis by (simp del: l_inv Units_l_inv)  ballarin@13813  384 qed  ballarin@13813  385 ballarin@13940  386 lemma (in group) inv_comm:  ballarin@13940  387  "[| x \ y = \; x \ carrier G; y \ carrier G |] ==> y \ x = \"  wenzelm@14693  388  by (rule Units_inv_comm) auto  ballarin@13940  389 paulson@13944  390 lemma (in group) inv_equality:  paulson@13943  391  "[|y \ x = \; x \ carrier G; y \ carrier G|] ==> inv x = y"  paulson@13943  392 apply (simp add: m_inv_def)  paulson@13943  393 apply (rule the_equality)  wenzelm@14693  394  apply (simp add: inv_comm [of y x])  wenzelm@14693  395 apply (rule r_cancel [THEN iffD1], auto)  paulson@13943  396 done  paulson@13943  397 ballarin@57271  398 (* Contributed by Joachim Breitner *)  ballarin@57271  399 lemma (in group) inv_solve_left:  ballarin@57271  400  "\ a \ carrier G; b \ carrier G; c \ carrier G \ \ a = inv b \ c \ c = b \ a"  ballarin@57271  401  by (metis inv_equality l_inv_ex l_one m_assoc r_inv)  ballarin@57271  402 lemma (in group) inv_solve_right:  ballarin@57271  403  "\ a \ carrier G; b \ carrier G; c \ carrier G \ \ a = b \ inv c \ b = a \ c"  ballarin@57271  404  by (metis inv_equality l_inv_ex l_one m_assoc r_inv)  ballarin@57271  405 wenzelm@61382  406 text \Power\  ballarin@13936  407 ballarin@13936  408 lemma (in group) int_pow_def2:  huffman@46559  409  "a (^) (z::int) = (if z < 0 then inv (a (^) (nat (-z))) else a (^) (nat z))"  ballarin@13936  410  by (simp add: int_pow_def nat_pow_def Let_def)  ballarin@13936  411 ballarin@13936  412 lemma (in group) int_pow_0 [simp]:  ballarin@13936  413  "x (^) (0::int) = \"  ballarin@13936  414  by (simp add: int_pow_def2)  ballarin@13936  415 ballarin@13936  416 lemma (in group) int_pow_one [simp]:  ballarin@13936  417  "\ (^) (z::int) = \"  ballarin@13936  418  by (simp add: int_pow_def2)  ballarin@13936  419 ballarin@57271  420 (* The following are contributed by Joachim Breitner *)  ballarin@20318  421 ballarin@57271  422 lemma (in group) int_pow_closed [intro, simp]:  ballarin@57271  423  "x \ carrier G ==> x (^) (i::int) \ carrier G"  ballarin@57271  424  by (simp add: int_pow_def2)  ballarin@57271  425 ballarin@57271  426 lemma (in group) int_pow_1 [simp]:  ballarin@57271  427  "x \ carrier G \ x (^) (1::int) = x"  ballarin@57271  428  by (simp add: int_pow_def2)  ballarin@57271  429 ballarin@57271  430 lemma (in group) int_pow_neg:  ballarin@57271  431  "x \ carrier G \ x (^) (-i::int) = inv (x (^) i)"  ballarin@57271  432  by (simp add: int_pow_def2)  ballarin@57271  433 ballarin@57271  434 lemma (in group) int_pow_mult:  ballarin@57271  435  "x \ carrier G \ x (^) (i + j::int) = x (^) i \ x (^) j"  ballarin@57271  436 proof -  ballarin@57271  437  have [simp]: "-i - j = -j - i" by simp  ballarin@57271  438  assume "x : carrier G" then  ballarin@57271  439  show ?thesis  ballarin@57271  440  by (auto simp add: int_pow_def2 inv_solve_left inv_solve_right nat_add_distrib [symmetric] nat_pow_mult )  ballarin@57271  441 qed  ballarin@57271  442 Andreas@61628  443 lemma (in group) int_pow_diff:  Andreas@61628  444  "x \ carrier G \ x (^) (n - m :: int) = x (^) n \ inv (x (^) m)"  Andreas@61628  445 by(simp only: diff_conv_add_uminus int_pow_mult int_pow_neg)  Andreas@61628  446 Andreas@61628  447 lemma (in group) inj_on_multc: "c \ carrier G \ inj_on (\x. x \ c) (carrier G)"  Andreas@61628  448 by(simp add: inj_on_def)  Andreas@61628  449 Andreas@61628  450 lemma (in group) inj_on_cmult: "c \ carrier G \ inj_on (\x. c \ x) (carrier G)"  Andreas@61628  451 by(simp add: inj_on_def)  Andreas@61628  452 wenzelm@61382  453 subsection \Subgroups\  ballarin@13813  454 ballarin@19783  455 locale subgroup =  ballarin@19783  456  fixes H and G (structure)  paulson@14963  457  assumes subset: "H \ carrier G"  paulson@14963  458  and m_closed [intro, simp]: "\x \ H; y \ H\ \ x \ y \ H"  ballarin@20318  459  and one_closed [simp]: "\ \ H"  paulson@14963  460  and m_inv_closed [intro,simp]: "x \ H \ inv x \ H"  ballarin@13813  461 ballarin@20318  462 lemma (in subgroup) is_subgroup:  wenzelm@26199  463  "subgroup H G" by (rule subgroup_axioms)  ballarin@20318  464 ballarin@13813  465 declare (in subgroup) group.intro [intro]  ballarin@13949  466 paulson@14963  467 lemma (in subgroup) mem_carrier [simp]:  paulson@14963  468  "x \ H \ x \ carrier G"  paulson@14963  469  using subset by blast  ballarin@13813  470 paulson@14963  471 lemma subgroup_imp_subset:  paulson@14963  472  "subgroup H G \ H \ carrier G"  paulson@14963  473  by (rule subgroup.subset)  paulson@14963  474 paulson@14963  475 lemma (in subgroup) subgroup_is_group [intro]:  ballarin@27611  476  assumes "group G"  ballarin@27611  477  shows "group (G\carrier := H\)"  ballarin@27611  478 proof -  ballarin@29237  479  interpret group G by fact  ballarin@27611  480  show ?thesis  ballarin@27698  481  apply (rule monoid.group_l_invI)  ballarin@27698  482  apply (unfold_locales) [1]  ballarin@27698  483  apply (auto intro: m_assoc l_inv mem_carrier)  ballarin@27698  484  done  ballarin@27611  485 qed  ballarin@13813  486 wenzelm@61382  487 text \  ballarin@13813  488  Since @{term H} is nonempty, it contains some element @{term x}. Since  wenzelm@63167  489  it is closed under inverse, it contains \inv x\. Since  wenzelm@63167  490  it is closed under product, it contains \x \ inv x = \\.  wenzelm@61382  491 \  ballarin@13813  492 ballarin@13813  493 lemma (in group) one_in_subset:  ballarin@13813  494  "[| H \ carrier G; H \ {}; \a \ H. inv a \ H; \a\H. \b\H. a \ b \ H |]  ballarin@13813  495  ==> \ \ H"  wenzelm@44472  496 by force  ballarin@13813  497 wenzelm@61382  498 text \A characterization of subgroups: closed, non-empty subset.\  ballarin@13813  499 ballarin@13813  500 lemma (in group) subgroupI:  ballarin@13813  501  assumes subset: "H \ carrier G" and non_empty: "H \ {}"  paulson@14963  502  and inv: "!!a. a \ H \ inv a \ H"  paulson@14963  503  and mult: "!!a b. \a \ H; b \ H\ \ a \ b \ H"  ballarin@13813  504  shows "subgroup H G"  ballarin@27714  505 proof (simp add: subgroup_def assms)  ballarin@27714  506  show "\ \ H" by (rule one_in_subset) (auto simp only: assms)  ballarin@13813  507 qed  ballarin@13813  508 ballarin@13936  509 declare monoid.one_closed [iff] group.inv_closed [simp]  ballarin@13936  510  monoid.l_one [simp] monoid.r_one [simp] group.inv_inv [simp]  ballarin@13813  511 ballarin@13813  512 lemma subgroup_nonempty:  ballarin@13813  513  "~ subgroup {} G"  ballarin@13813  514  by (blast dest: subgroup.one_closed)  ballarin@13813  515 ballarin@13813  516 lemma (in subgroup) finite_imp_card_positive:  ballarin@13813  517  "finite (carrier G) ==> 0 < card H"  ballarin@13813  518 proof (rule classical)  wenzelm@41528  519  assume "finite (carrier G)" and a: "~ 0 < card H"  paulson@14963  520  then have "finite H" by (blast intro: finite_subset [OF subset])  wenzelm@41528  521  with is_subgroup a have "subgroup {} G" by simp  ballarin@13813  522  with subgroup_nonempty show ?thesis by contradiction  ballarin@13813  523 qed  ballarin@13813  524 ballarin@13936  525 (*  ballarin@13936  526 lemma (in monoid) Units_subgroup:  ballarin@13936  527  "subgroup (Units G) G"  ballarin@13936  528 *)  ballarin@13936  529 ballarin@20318  530 wenzelm@61382  531 subsection \Direct Products\  ballarin@13813  532 wenzelm@35848  533 definition  wenzelm@35848  534  DirProd :: "_ \ _ \ ('a \ 'b) monoid" (infixr "\\" 80) where  wenzelm@35848  535  "G \\ H =  wenzelm@35848  536  \carrier = carrier G \ carrier H,  wenzelm@35848  537  mult = ($$g, h) (g', h'). (g \\<^bsub>G\<^esub> g', h \\<^bsub>H\<^esub> h')),  wenzelm@35848  538  one = (\\<^bsub>G\<^esub>, \\<^bsub>H\<^esub>)\"  ballarin@13813  539 paulson@14963  540 lemma DirProd_monoid:  ballarin@27611  541  assumes "monoid G" and "monoid H"  paulson@14963  542  shows "monoid (G \\ H)"  paulson@14963  543 proof -  wenzelm@30729  544  interpret G: monoid G by fact  wenzelm@30729  545  interpret H: monoid H by fact  ballarin@27714  546  from assms  paulson@14963  547  show ?thesis by (unfold monoid_def DirProd_def, auto)  paulson@14963  548 qed  ballarin@13813  549 ballarin@13813  550 wenzelm@61382  551 text\Does not use the previous result because it's easier just to use auto.\  paulson@14963  552 lemma DirProd_group:  ballarin@27611  553  assumes "group G" and "group H"  paulson@14963  554  shows "group (G \\ H)"  ballarin@27611  555 proof -  wenzelm@30729  556  interpret G: group G by fact  wenzelm@30729  557  interpret H: group H by fact  ballarin@27611  558  show ?thesis by (rule groupI)  paulson@14963  559  (auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv  paulson@14963  560  simp add: DirProd_def)  ballarin@27611  561 qed  ballarin@13813  562 paulson@14963  563 lemma carrier_DirProd [simp]:  paulson@14963  564  "carrier (G \\ H) = carrier G \ carrier H"  paulson@14963  565  by (simp add: DirProd_def)  paulson@13944  566 paulson@14963  567 lemma one_DirProd [simp]:  paulson@14963  568  "\\<^bsub>G \\ H\<^esub> = (\\<^bsub>G\<^esub>, \\<^bsub>H\<^esub>)"  paulson@14963  569  by (simp add: DirProd_def)  paulson@13944  570 paulson@14963  571 lemma mult_DirProd [simp]:  paulson@14963  572  "(g, h) \\<^bsub>(G \\ H)\<^esub> (g', h') = (g \\<^bsub>G\<^esub> g', h \\<^bsub>H\<^esub> h')"  paulson@14963  573  by (simp add: DirProd_def)  paulson@13944  574 paulson@14963  575 lemma inv_DirProd [simp]:  ballarin@27611  576  assumes "group G" and "group H"  paulson@13944  577  assumes g: "g \ carrier G"  paulson@13944  578  and h: "h \ carrier H"  paulson@14963  579  shows "m_inv (G \\ H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"  ballarin@27611  580 proof -  wenzelm@30729  581  interpret G: group G by fact  wenzelm@30729  582  interpret H: group H by fact  wenzelm@30729  583  interpret Prod: group "G \\ H"  ballarin@27714  584  by (auto intro: DirProd_group group.intro group.axioms assms)  paulson@14963  585  show ?thesis by (simp add: Prod.inv_equality g h)  paulson@14963  586 qed  ballarin@27698  587 paulson@14963  588 wenzelm@61382  589 subsection \Homomorphisms and Isomorphisms\  ballarin@13813  590 wenzelm@35847  591 definition  wenzelm@35847  592  hom :: "_ => _ => ('a => 'b) set" where  wenzelm@35848  593  "hom G H =  wenzelm@61384  594  {h. h \ carrier G \ carrier H &  wenzelm@14693  595  (\x \ carrier G. \y \ carrier G. h (x \\<^bsub>G\<^esub> y) = h x \\<^bsub>H\<^esub> h y)}"  ballarin@13813  596 paulson@14761  597 lemma (in group) hom_compose:  nipkow@31754  598  "[|h \ hom G H; i \ hom H I|] ==> compose (carrier G) i h \ hom G I"  nipkow@44890  599 by (fastforce simp add: hom_def compose_def)  paulson@13943  600 wenzelm@35848  601 definition  wenzelm@35848  602  iso :: "_ => _ => ('a => 'b) set" (infixr "\" 60)  wenzelm@35848  603  where "G \ H = {h. h \ hom G H & bij_betw h (carrier G) (carrier H)}"  paulson@14761  604 paulson@14803  605 lemma iso_refl: "(%x. x) \ G \ G"  nipkow@31727  606 by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)  paulson@14761  607 paulson@14761  608 lemma (in group) iso_sym:  nipkow@33057  609  "h \ G \ H \ inv_into (carrier G) h \ H \ G"  nipkow@33057  610 apply (simp add: iso_def bij_betw_inv_into)  nipkow@33057  611 apply (subgoal_tac "inv_into (carrier G) h \ carrier H \ carrier G")  nipkow@33057  612  prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_inv_into])  nipkow@33057  613 apply (simp add: hom_def bij_betw_def inv_into_f_eq f_inv_into_f Pi_def)  paulson@14761  614 done  paulson@14761  615 paulson@14761  616 lemma (in group) iso_trans:  paulson@14803  617  "[|h \ G \ H; i \ H \ I|] ==> (compose (carrier G) i h) \ G \ I"  paulson@14761  618 by (auto simp add: iso_def hom_compose bij_betw_compose)  paulson@14761  619 paulson@14963  620 lemma DirProd_commute_iso:  paulson@14963  621  shows "(\(x,y). (y,x)) \ (G \\ H) \ (H \\ G)"  nipkow@31754  622 by (auto simp add: iso_def hom_def inj_on_def bij_betw_def)  paulson@14761  623 paulson@14963  624 lemma DirProd_assoc_iso:  paulson@14963  625  shows "(\(x,y,z). (x,(y,z))) \ (G \\ H \\ I) \ (G \\ (H \\ I))"  nipkow@31727  626 by (auto simp add: iso_def hom_def inj_on_def bij_betw_def)  paulson@14761  627 paulson@14761  628 wenzelm@61382  629 text\Basis for homomorphism proofs: we assume two groups @{term G} and  wenzelm@61382  630  @{term H}, with a homomorphism @{term h} between them\  ballarin@61565  631 locale group_hom = G?: group G + H?: group H for G (structure) and H (structure) +  ballarin@29237  632  fixes h  ballarin@13813  633  assumes homh: "h \ hom G H"  ballarin@29240  634 ballarin@29240  635 lemma (in group_hom) hom_mult [simp]:  ballarin@29240  636  "[| x \ carrier G; y \ carrier G |] ==> h (x \\<^bsub>G\<^esub> y) = h x \\<^bsub>H\<^esub> h y"  ballarin@29240  637 proof -  ballarin@29240  638  assume "x \ carrier G" "y \ carrier G"  ballarin@29240  639  with homh [unfolded hom_def] show ?thesis by simp  ballarin@29240  640 qed  ballarin@29240  641 ballarin@29240  642 lemma (in group_hom) hom_closed [simp]:  ballarin@29240  643  "x \ carrier G ==> h x \ carrier H"  ballarin@29240  644 proof -  ballarin@29240  645  assume "x \ carrier G"  nipkow@31754  646  with homh [unfolded hom_def] show ?thesis by auto  ballarin@29240  647 qed  ballarin@13813  648 ballarin@13813  649 lemma (in group_hom) one_closed [simp]:  ballarin@13813  650  "h \ \ carrier H"  ballarin@13813  651  by simp  ballarin@13813  652 ballarin@13813  653 lemma (in group_hom) hom_one [simp]:  wenzelm@14693  654  "h \ = \\<^bsub>H\<^esub>"  ballarin@13813  655 proof -  ballarin@15076  656  have "h \ \\<^bsub>H\<^esub> \\<^bsub>H\<^esub> = h \ \\<^bsub>H\<^esub> h \"  ballarin@13813  657  by (simp add: hom_mult [symmetric] del: hom_mult)  ballarin@13813  658  then show ?thesis by (simp del: r_one)  ballarin@13813  659 qed  ballarin@13813  660 ballarin@13813  661 lemma (in group_hom) inv_closed [simp]:  ballarin@13813  662  "x \ carrier G ==> h (inv x) \ carrier H"  ballarin@13813  663  by simp  ballarin@13813  664 ballarin@13813  665 lemma (in group_hom) hom_inv [simp]:  wenzelm@14693  666  "x \ carrier G ==> h (inv x) = inv\<^bsub>H\<^esub> (h x)"  ballarin@13813  667 proof -  ballarin@13813  668  assume x: "x \ carrier G"  wenzelm@14693  669  then have "h x \\<^bsub>H\<^esub> h (inv x) = \\<^bsub>H\<^esub>"  paulson@14963  670  by (simp add: hom_mult [symmetric] del: hom_mult)  wenzelm@14693  671  also from x have "... = h x \\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h x)"  paulson@14963  672  by (simp add: hom_mult [symmetric] del: hom_mult)  wenzelm@14693  673  finally have "h x \\<^bsub>H\<^esub> h (inv x) = h x \\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h x)" .  ballarin@27698  674  with x show ?thesis by (simp del: H.r_inv H.Units_r_inv)  ballarin@13813  675 qed  ballarin@13813  676 ballarin@57271  677 (* Contributed by Joachim Breitner *)  ballarin@57271  678 lemma (in group) int_pow_is_hom:  ballarin@57271  679  "x \ carrier G \ (op(^) x) \ hom \ carrier = UNIV, mult = op +, one = 0::int \ G "  ballarin@57271  680  unfolding hom_def by (simp add: int_pow_mult)  ballarin@57271  681 ballarin@20318  682 wenzelm@61382  683 subsection \Commutative Structures\  ballarin@13936  684 wenzelm@61382  685 text \  ballarin@13936  686  Naming convention: multiplicative structures that are commutative  ballarin@13936  687  are called \emph{commutative}, additive structures are called  ballarin@13936  688  \emph{Abelian}.  wenzelm@61382  689 \  ballarin@13813  690 paulson@14963  691 locale comm_monoid = monoid +  paulson@14963  692  assumes m_comm: "\x \ carrier G; y \ carrier G\ \ x \ y = y \ x"  ballarin@13813  693 paulson@14963  694 lemma (in comm_monoid) m_lcomm:  paulson@14963  695  "\x \ carrier G; y \ carrier G; z \ carrier G\ \  ballarin@13813  696  x \ (y \ z) = y \ (x \ z)"  ballarin@13813  697 proof -  wenzelm@14693  698  assume xyz: "x \ carrier G" "y \ carrier G" "z \ carrier G"  ballarin@13813  699  from xyz have "x \ (y \ z) = (x \ y) \ z" by (simp add: m_assoc)  ballarin@13813  700  also from xyz have "... = (y \ x) \ z" by (simp add: m_comm)  ballarin@13813  701  also from xyz have "... = y \ (x \ z)" by (simp add: m_assoc)  ballarin@13813  702  finally show ?thesis .  ballarin@13813  703 qed  ballarin@13813  704 paulson@14963  705 lemmas (in comm_monoid) m_ac = m_assoc m_comm m_lcomm  ballarin@13813  706 ballarin@13936  707 lemma comm_monoidI:  ballarin@19783  708  fixes G (structure)  ballarin@13936  709  assumes m_closed:  wenzelm@14693  710  "!!x y. [| x \ carrier G; y \ carrier G |] ==> x \ y \ carrier G"  wenzelm@14693  711  and one_closed: "\ \ carrier G"  ballarin@13936  712  and m_assoc:  ballarin@13936  713  "!!x y z. [| x \ carrier G; y \ carrier G; z \ carrier G |] ==>  wenzelm@14693  714  (x \ y) \ z = x \ (y \ z)"  wenzelm@14693  715  and l_one: "!!x. x \ carrier G ==> \ \ x = x"  ballarin@13936  716  and m_comm:  wenzelm@14693  717  "!!x y. [| x \ carrier G; y \ carrier G |] ==> x \ y = y \ x"  ballarin@13936  718  shows "comm_monoid G"  ballarin@13936  719  using l_one  paulson@14963  720  by (auto intro!: comm_monoid.intro comm_monoid_axioms.intro monoid.intro  ballarin@27714  721  intro: assms simp: m_closed one_closed m_comm)  ballarin@13817  722 ballarin@13936  723 lemma (in monoid) monoid_comm_monoidI:  ballarin@13936  724  assumes m_comm:  wenzelm@14693  725  "!!x y. [| x \ carrier G; y \ carrier G |] ==> x \ y = y \ x"  ballarin@13936  726  shows "comm_monoid G"  ballarin@13936  727  by (rule comm_monoidI) (auto intro: m_assoc m_comm)  paulson@14963  728 wenzelm@14693  729 (*lemma (in comm_monoid) r_one [simp]:  ballarin@13817  730  "x \ carrier G ==> x \ \ = x"  ballarin@13817  731 proof -  ballarin@13817  732  assume G: "x \ carrier G"  ballarin@13817  733  then have "x \ \ = \ \ x" by (simp add: m_comm)  ballarin@13817  734  also from G have "... = x" by simp  ballarin@13817  735  finally show ?thesis .  wenzelm@14693  736 qed*)  paulson@14963  737 ballarin@13936  738 lemma (in comm_monoid) nat_pow_distr:  ballarin@13936  739  "[| x \ carrier G; y \ carrier G |] ==>  ballarin@13936  740  (x \ y) (^) (n::nat) = x (^) n \ y (^) n"  ballarin@13936  741  by (induct n) (simp, simp add: m_ac)  ballarin@13936  742 ballarin@13936  743 locale comm_group = comm_monoid + group  ballarin@13936  744 ballarin@13936  745 lemma (in group) group_comm_groupI:  ballarin@13936  746  assumes m_comm: "!!x y. [| x \ carrier G; y \ carrier G |] ==>  wenzelm@14693  747  x \ y = y \ x"  ballarin@13936  748  shows "comm_group G"  wenzelm@61169  749  by standard (simp_all add: m_comm)  ballarin@13817  750 ballarin@13936  751 lemma comm_groupI:  ballarin@19783  752  fixes G (structure)  ballarin@13936  753  assumes m_closed:  wenzelm@14693  754  "!!x y. [| x \ carrier G; y \ carrier G |] ==> x \ y \ carrier G"  wenzelm@14693  755  and one_closed: "\ \ carrier G"  ballarin@13936  756  and m_assoc:  ballarin@13936  757  "!!x y z. [| x \ carrier G; y \ carrier G; z \ carrier G |] ==>  wenzelm@14693  758  (x \ y) \ z = x \ (y \ z)"  ballarin@13936  759  and m_comm:  wenzelm@14693  760  "!!x y. [| x \ carrier G; y \ carrier G |] ==> x \ y = y \ x"  wenzelm@14693  761  and l_one: "!!x. x \ carrier G ==> \ \ x = x"  paulson@14963  762  and l_inv_ex: "!!x. x \ carrier G ==> \y \ carrier G. y \ x = \"  ballarin@13936  763  shows "comm_group G"  ballarin@27714  764  by (fast intro: group.group_comm_groupI groupI assms)  ballarin@13936  765 ballarin@13936  766 lemma (in comm_group) inv_mult:  ballarin@13854  767  "[| x \ carrier G; y \ carrier G |] ==> inv (x \ y) = inv x \ inv y"  ballarin@13936  768  by (simp add: m_ac inv_mult_group)  ballarin@13854  769 ballarin@20318  770 wenzelm@61382  771 subsection \The Lattice of Subgroups of a Group\  ballarin@14751  772 wenzelm@61382  773 text_raw \\label{sec:subgroup-lattice}\  ballarin@14751  774 ballarin@14751  775 theorem (in group) subgroups_partial_order:  wenzelm@55926  776  "partial_order \carrier = {H. subgroup H G}, eq = op =, le = op \\"  wenzelm@61169  777  by standard simp_all  ballarin@14751  778 ballarin@14751  779 lemma (in group) subgroup_self:  ballarin@14751  780  "subgroup (carrier G) G"  ballarin@14751  781  by (rule subgroupI) auto  ballarin@14751  782 ballarin@14751  783 lemma (in group) subgroup_imp_group:  wenzelm@55926  784  "subgroup H G ==> group (G\carrier := H$$"  wenzelm@26199  785  by (erule subgroup.subgroup_is_group) (rule group_axioms)  ballarin@14751  786 ballarin@14751  787 lemma (in group) is_monoid [intro, simp]:  ballarin@14751  788  "monoid G"  paulson@14963  789  by (auto intro: monoid.intro m_assoc)  ballarin@14751  790 ballarin@14751  791 lemma (in group) subgroup_inv_equality:  wenzelm@55926  792  "[| subgroup H G; x \ H |] ==> m_inv (G \carrier := H\) x = inv x"  ballarin@14751  793 apply (rule_tac inv_equality [THEN sym])  paulson@14761  794  apply (rule group.l_inv [OF subgroup_imp_group, simplified], assumption+)  paulson@14761  795  apply (rule subsetD [OF subgroup.subset], assumption+)  paulson@14761  796 apply (rule subsetD [OF subgroup.subset], assumption)  paulson@14761  797 apply (rule_tac group.inv_closed [OF subgroup_imp_group, simplified], assumption+)  ballarin@14751  798 done  ballarin@14751  799 ballarin@14751  800 theorem (in group) subgroups_Inter:  ballarin@14751  801  assumes subgr: "(!!H. H \ A ==> subgroup H G)"  ballarin@14751  802  and not_empty: "A ~= {}"  ballarin@14751  803  shows "subgroup (\A) G"  ballarin@14751  804 proof (rule subgroupI)  ballarin@14751  805  from subgr [THEN subgroup.subset] and not_empty  ballarin@14751  806  show "\A \ carrier G" by blast  ballarin@14751  807 next  ballarin@14751  808  from subgr [THEN subgroup.one_closed]  ballarin@14751  809  show "\A ~= {}" by blast  ballarin@14751  810 next  ballarin@14751  811  fix x assume "x \ \A"  ballarin@14751  812  with subgr [THEN subgroup.m_inv_closed]  ballarin@14751  813  show "inv x \ \A" by blast  ballarin@14751  814 next  ballarin@14751  815  fix x y assume "x \ \A" "y \ \A"  ballarin@14751  816  with subgr [THEN subgroup.m_closed]  ballarin@14751  817  show "x \ y \ \A" by blast  ballarin@14751  818 qed  ballarin@14751  819 ballarin@66579  820 theorem (in group) subgroups_complete_lattice:  ballarin@66579  821  "complete_lattice \carrier = {H. subgroup H G}, eq = op =, le = op \\"  ballarin@66579  822  (is "complete_lattice ?L")  ballarin@66579  823 proof (rule partial_order.complete_lattice_criterion1)  ballarin@66579  824  show "partial_order ?L" by (rule subgroups_partial_order)  ballarin@66579  825 next  ballarin@66579  826  have "greatest ?L (carrier G) (carrier ?L)"  ballarin@66579  827  by (unfold greatest_def) (simp add: subgroup.subset subgroup_self)  ballarin@66579  828  then show "\G. greatest ?L G (carrier ?L)" ..  ballarin@66579  829 next  ballarin@66579  830  fix A  ballarin@66579  831  assume L: "A \ carrier ?L" and non_empty: "A ~= {}"  ballarin@66579  832  then have Int_subgroup: "subgroup (\A) G"  ballarin@66579  833  by (fastforce intro: subgroups_Inter)  ballarin@66579  834  have "greatest ?L (\A) (Lower ?L A)" (is "greatest _ ?Int _")  ballarin@66579  835  proof (rule greatest_LowerI)  ballarin@66579  836  fix H  ballarin@66579  837  assume H: "H \ A"  ballarin@66579  838  with L have subgroupH: "subgroup H G" by auto  ballarin@66579  839  from subgroupH have groupH: "group (G \carrier := H\)" (is "group ?H")  ballarin@66579  840  by (rule subgroup_imp_group)  ballarin@66579  841  from groupH have monoidH: "monoid ?H"  ballarin@66579  842  by (rule group.is_monoid)  ballarin@66579  843  from H have Int_subset: "?Int \ H" by fastforce  ballarin@66579  844  then show "le ?L ?Int H" by simp  ballarin@66579  845  next  ballarin@66579  846  fix H  ballarin@66579  847  assume H: "H \ Lower ?L A"  ballarin@66579  848  with L Int_subgroup show "le ?L H ?Int"  ballarin@66579  849  by (fastforce simp: Lower_def intro: Inter_greatest)  ballarin@66579  850  next  ballarin@66579  851  show "A \ carrier ?L" by (rule L)  ballarin@66579  852  next  ballarin@66579  853  show "?Int \ carrier ?L" by simp (rule Int_subgroup)  ballarin@66579  854  qed  ballarin@66579  855  then show "\I. greatest ?L I (Lower ?L A)" ..  ballarin@66579  856 qed  ballarin@66579  857 ballarin@13813  858 end