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