src/HOL/Algebra/Group.thy
changeset 13943 83d842ccd4aa
parent 13940 c67798653056
child 13944 9b34607cd83e
     1.1 --- a/src/HOL/Algebra/Group.thy	Thu May 01 08:39:37 2003 +0200
     1.2 +++ b/src/HOL/Algebra/Group.thy	Thu May 01 10:29:44 2003 +0200
     1.3 @@ -99,29 +99,23 @@
     1.4  
     1.5  lemma (in monoid) Units_inv_closed [intro, simp]:
     1.6    "x \<in> Units G ==> inv x \<in> carrier G"
     1.7 -  apply (unfold Units_def m_inv_def)
     1.8 -  apply auto
     1.9 +  apply (unfold Units_def m_inv_def, auto)
    1.10    apply (rule theI2, fast)
    1.11 -   apply (fast intro: inv_unique)
    1.12 -  apply fast
    1.13 +   apply (fast intro: inv_unique, fast)
    1.14    done
    1.15  
    1.16  lemma (in monoid) Units_l_inv:
    1.17    "x \<in> Units G ==> inv x \<otimes> x = \<one>"
    1.18 -  apply (unfold Units_def m_inv_def)
    1.19 -  apply auto
    1.20 +  apply (unfold Units_def m_inv_def, auto)
    1.21    apply (rule theI2, fast)
    1.22 -   apply (fast intro: inv_unique)
    1.23 -  apply fast
    1.24 +   apply (fast intro: inv_unique, fast)
    1.25    done
    1.26  
    1.27  lemma (in monoid) Units_r_inv:
    1.28    "x \<in> Units G ==> x \<otimes> inv x = \<one>"
    1.29 -  apply (unfold Units_def m_inv_def)
    1.30 -  apply auto
    1.31 +  apply (unfold Units_def m_inv_def, auto)
    1.32    apply (rule theI2, fast)
    1.33 -   apply (fast intro: inv_unique)
    1.34 -  apply fast
    1.35 +   apply (fast intro: inv_unique, fast)
    1.36    done
    1.37  
    1.38  lemma (in monoid) Units_inv_Units [intro, simp]:
    1.39 @@ -354,6 +348,14 @@
    1.40    "[| x \<otimes> y = \<one>; x \<in> carrier G; y \<in> carrier G |] ==> y \<otimes> x = \<one>"
    1.41    by (rule Units_inv_comm) auto                          
    1.42  
    1.43 +lemma (in group) m_inv_equality:
    1.44 +     "[|y \<otimes> x = \<one>; x \<in> carrier G; y \<in> carrier G|] ==> inv x = y"
    1.45 +apply (simp add: m_inv_def)
    1.46 +apply (rule the_equality)
    1.47 + apply (simp add: inv_comm [of y x]) 
    1.48 +apply (rule r_cancel [THEN iffD1], auto) 
    1.49 +done
    1.50 +
    1.51  text {* Power *}
    1.52  
    1.53  lemma (in group) int_pow_def2:
    1.54 @@ -594,6 +596,15 @@
    1.55    "[| h \<in> hom G H; x \<in> carrier G |] ==> h x \<in> carrier H"
    1.56    by (auto simp add: hom_def funcset_mem)
    1.57  
    1.58 +lemma compose_hom:
    1.59 +     "[|group G; h \<in> hom G G; h' \<in> hom G G; h' \<in> carrier G -> carrier G|]
    1.60 +      ==> compose (carrier G) h h' \<in> hom G G"
    1.61 +apply (simp (no_asm_simp) add: hom_def)
    1.62 +apply (intro conjI) 
    1.63 + apply (force simp add: funcset_compose hom_def)
    1.64 +apply (simp add: compose_def group.axioms hom_mult funcset_mem) 
    1.65 +done
    1.66 +
    1.67  locale group_hom = group G + group H + var h +
    1.68    assumes homh: "h \<in> hom G H"
    1.69    notes hom_mult [simp] = hom_mult [OF homh]