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