Unit_inv_l, Unit_inv_r made [simp].
authorballarin
Tue Jul 29 16:17:13 2008 +0200 (2008-07-29)
changeset 27698197f0517f0bd
parent 27697 bcf941cc3324
child 27699 489e3f33af0e
Unit_inv_l, Unit_inv_r made [simp].
src/HOL/Algebra/Coset.thy
src/HOL/Algebra/Group.thy
src/HOL/Algebra/Ideal.thy
     1.1 --- a/src/HOL/Algebra/Coset.thy	Tue Jul 29 16:16:10 2008 +0200
     1.2 +++ b/src/HOL/Algebra/Coset.thy	Tue Jul 29 16:17:13 2008 +0200
     1.3 @@ -621,7 +621,8 @@
     1.4        assume [simp]: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
     1.5  	 and "inv x \<otimes> y \<in> H" and "inv y \<otimes> z \<in> H"
     1.6        hence "(inv x \<otimes> y) \<otimes> (inv y \<otimes> z) \<in> H" by simp
     1.7 -      hence "inv x \<otimes> (y \<otimes> inv y) \<otimes> z \<in> H" by (simp add: m_assoc del: r_inv) 
     1.8 +      hence "inv x \<otimes> (y \<otimes> inv y) \<otimes> z \<in> H"
     1.9 +	by (simp add: m_assoc del: r_inv Units_r_inv) 
    1.10        thus "inv x \<otimes> z \<in> H" by simp
    1.11      qed
    1.12    qed
     2.1 --- a/src/HOL/Algebra/Group.thy	Tue Jul 29 16:16:10 2008 +0200
     2.2 +++ b/src/HOL/Algebra/Group.thy	Tue Jul 29 16:17:13 2008 +0200
     2.3 @@ -77,6 +77,27 @@
     2.4    finally show ?thesis .
     2.5  qed
     2.6  
     2.7 +lemma (in monoid) Units_m_closed [intro, simp]:
     2.8 +  assumes x: "x \<in> Units G" and y: "y \<in> Units G"
     2.9 +  shows "x \<otimes> y \<in> Units G"
    2.10 +proof -
    2.11 +  from x obtain x' where x: "x \<in> carrier G" "x' \<in> carrier G" and xinv: "x \<otimes> x' = \<one>" "x' \<otimes> x = \<one>"
    2.12 +    unfolding Units_def by fast
    2.13 +  from y obtain y' where y: "y \<in> carrier G" "y' \<in> carrier G" and yinv: "y \<otimes> y' = \<one>" "y' \<otimes> y = \<one>"
    2.14 +    unfolding Units_def by fast
    2.15 +  from x y xinv yinv have "y' \<otimes> (x' \<otimes> x) \<otimes> y = \<one>" by simp
    2.16 +  moreover from x y xinv yinv have "x \<otimes> (y \<otimes> y') \<otimes> x' = \<one>" by simp
    2.17 +  moreover note x y
    2.18 +  ultimately show ?thesis unfolding Units_def
    2.19 +    -- "Must avoid premature use of @{text hyp_subst_tac}."
    2.20 +    apply (rule_tac CollectI)
    2.21 +    apply (rule)
    2.22 +    apply (fast)
    2.23 +    apply (rule bexI [where x = "y' \<otimes> x'"])
    2.24 +    apply (auto simp: m_assoc)
    2.25 +    done
    2.26 +qed
    2.27 +
    2.28  lemma (in monoid) Units_one_closed [intro, simp]:
    2.29    "\<one> \<in> Units G"
    2.30    by (unfold Units_def) auto
    2.31 @@ -96,14 +117,14 @@
    2.32    "x \<in> Units G ==> \<exists>y \<in> carrier G. x \<otimes> y = \<one>"
    2.33    by (unfold Units_def) auto
    2.34  
    2.35 -lemma (in monoid) Units_l_inv:
    2.36 +lemma (in monoid) Units_l_inv [simp]:
    2.37    "x \<in> Units G ==> inv x \<otimes> x = \<one>"
    2.38    apply (unfold Units_def m_inv_def, auto)
    2.39    apply (rule theI2, fast)
    2.40     apply (fast intro: inv_unique, fast)
    2.41    done
    2.42  
    2.43 -lemma (in monoid) Units_r_inv:
    2.44 +lemma (in monoid) Units_r_inv [simp]:
    2.45    "x \<in> Units G ==> x \<otimes> inv x = \<one>"
    2.46    apply (unfold Units_def m_inv_def, auto)
    2.47    apply (rule theI2, fast)
    2.48 @@ -126,7 +147,7 @@
    2.49    assume eq: "x \<otimes> y = x \<otimes> z"
    2.50      and G: "x \<in> Units G"  "y \<in> carrier G"  "z \<in> carrier G"
    2.51    then have "(inv x \<otimes> x) \<otimes> y = (inv x \<otimes> x) \<otimes> z"
    2.52 -    by (simp add: m_assoc Units_closed)
    2.53 +    by (simp add: m_assoc Units_closed del: Units_l_inv)
    2.54    with G show "y = z" by (simp add: Units_l_inv)
    2.55  next
    2.56    assume eq: "y = z"
    2.57 @@ -138,9 +159,8 @@
    2.58    "x \<in> Units G ==> inv (inv x) = x"
    2.59  proof -
    2.60    assume x: "x \<in> Units G"
    2.61 -  then have "inv x \<otimes> inv (inv x) = inv x \<otimes> x"
    2.62 -    by (simp add: Units_l_inv Units_r_inv)
    2.63 -  with x show ?thesis by (simp add: Units_closed)
    2.64 +  then have "inv x \<otimes> inv (inv x) = inv x \<otimes> x" by simp
    2.65 +  with x show ?thesis by (simp add: Units_closed del: Units_l_inv Units_r_inv)
    2.66  qed
    2.67  
    2.68  lemma (in monoid) inv_inj_on_Units:
    2.69 @@ -187,6 +207,13 @@
    2.70    "x \<in> carrier G ==> (x (^) n) (^) m = x (^) (n * m::nat)"
    2.71    by (induct m) (simp, simp add: nat_pow_mult add_commute)
    2.72  
    2.73 +
    2.74 +(* Jacobson defines submonoid here. *)
    2.75 +(* Jacobson defines the order of a monoid here. *)
    2.76 +
    2.77 +
    2.78 +subsection {* Groups *}
    2.79 +
    2.80  text {*
    2.81    A group is a monoid all of whose elements are invertible.
    2.82  *}
    2.83 @@ -194,7 +221,6 @@
    2.84  locale group = monoid +
    2.85    assumes Units: "carrier G <= Units G"
    2.86  
    2.87 -
    2.88  lemma (in group) is_group: "group G" by (rule group_axioms)
    2.89  
    2.90  theorem groupI:
    2.91 @@ -254,12 +280,10 @@
    2.92    qed
    2.93    then have carrier_subset_Units: "carrier G <= Units G"
    2.94      by (unfold Units_def) fast
    2.95 -  show ?thesis
    2.96 -    by (fast intro!: group.intro monoid.intro group_axioms.intro
    2.97 -      carrier_subset_Units intro: prems r_one)
    2.98 +  show ?thesis by unfold_locales (auto simp: r_one m_assoc carrier_subset_Units)
    2.99  qed
   2.100  
   2.101 -lemma (in monoid) monoid_groupI:
   2.102 +lemma (in monoid) group_l_invI:
   2.103    assumes l_inv_ex:
   2.104      "!!x. x \<in> carrier G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one>"
   2.105    shows "group G"
   2.106 @@ -313,7 +337,7 @@
   2.107    assume eq: "y \<otimes> x = z \<otimes> x"
   2.108      and G: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
   2.109    then have "y \<otimes> (x \<otimes> inv x) = z \<otimes> (x \<otimes> inv x)"
   2.110 -    by (simp add: m_assoc [symmetric] del: r_inv)
   2.111 +    by (simp add: m_assoc [symmetric] del: r_inv Units_r_inv)
   2.112    with G show "y = z" by simp
   2.113  next
   2.114    assume eq: "y = z"
   2.115 @@ -324,7 +348,7 @@
   2.116  lemma (in group) inv_one [simp]:
   2.117    "inv \<one> = \<one>"
   2.118  proof -
   2.119 -  have "inv \<one> = \<one> \<otimes> (inv \<one>)" by (simp del: r_inv)
   2.120 +  have "inv \<one> = \<one> \<otimes> (inv \<one>)" by (simp del: r_inv Units_r_inv)
   2.121    moreover have "... = \<one>" by simp
   2.122    finally show ?thesis .
   2.123  qed
   2.124 @@ -343,7 +367,7 @@
   2.125    assume G: "x \<in> carrier G"  "y \<in> carrier G"
   2.126    then have "inv (x \<otimes> y) \<otimes> (x \<otimes> y) = (inv y \<otimes> inv x) \<otimes> (x \<otimes> y)"
   2.127      by (simp add: m_assoc l_inv) (simp add: m_assoc [symmetric])
   2.128 -  with G show ?thesis by (simp del: l_inv)
   2.129 +  with G show ?thesis by (simp del: l_inv Units_l_inv)
   2.130  qed
   2.131  
   2.132  lemma (in group) inv_comm:
   2.133 @@ -401,7 +425,10 @@
   2.134  proof -
   2.135    interpret group [G] by fact
   2.136    show ?thesis
   2.137 -    by (rule groupI) (auto intro: m_assoc l_inv mem_carrier)
   2.138 +    apply (rule monoid.group_l_invI)
   2.139 +    apply (unfold_locales) [1]
   2.140 +    apply (auto intro: m_assoc l_inv mem_carrier)
   2.141 +    done
   2.142  qed
   2.143  
   2.144  text {*
   2.145 @@ -499,27 +526,11 @@
   2.146  proof -
   2.147    interpret G: group [G] by fact
   2.148    interpret H: group [H] by fact
   2.149 -  show ?thesis apply (rule group.inv_equality [OF DirProd_group])
   2.150 -  apply (simp_all add: prems group.l_inv)
   2.151 -  done
   2.152 -qed
   2.153 -
   2.154 -text{*This alternative proof of the previous result demonstrates interpret.
   2.155 -   It uses @{text Prod.inv_equality} (available after @{text interpret})
   2.156 -   instead of @{text "group.inv_equality [OF DirProd_group]"}. *}
   2.157 -lemma
   2.158 -  assumes "group G" and "group H"
   2.159 -  assumes g: "g \<in> carrier G"
   2.160 -      and h: "h \<in> carrier H"
   2.161 -  shows "m_inv (G \<times>\<times> H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
   2.162 -proof -
   2.163 -  interpret G: group [G] by fact
   2.164 -  interpret H: group [H] by fact
   2.165    interpret Prod: group ["G \<times>\<times> H"]
   2.166      by (auto intro: DirProd_group group.intro group.axioms prems)
   2.167    show ?thesis by (simp add: Prod.inv_equality g h)
   2.168  qed
   2.169 -  
   2.170 +
   2.171  
   2.172  subsection {* Homomorphisms and Isomorphisms *}
   2.173  
   2.174 @@ -604,7 +615,7 @@
   2.175    also from x have "... = h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h x)"
   2.176      by (simp add: hom_mult [symmetric] del: hom_mult)
   2.177    finally have "h x \<otimes>\<^bsub>H\<^esub> h (inv x) = h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h x)" .
   2.178 -  with x show ?thesis by (simp del: H.r_inv)
   2.179 +  with x show ?thesis by (simp del: H.r_inv H.Units_r_inv)
   2.180  qed
   2.181  
   2.182  
     3.1 --- a/src/HOL/Algebra/Ideal.thy	Tue Jul 29 16:16:10 2008 +0200
     3.2 +++ b/src/HOL/Algebra/Ideal.thy	Tue Jul 29 16:17:13 2008 +0200
     3.3 @@ -950,7 +950,7 @@
     3.4          have aUnit: "a \<in> Units R" by (simp add: field_Units)
     3.5      hence a: "a \<otimes> inv a = \<one>" by (rule Units_r_inv)
     3.6      from aI and aUnit
     3.7 -        have "a \<otimes> inv a \<in> I" by (simp add: I_r_closed)
     3.8 +        have "a \<otimes> inv a \<in> I" by (simp add: I_r_closed del: Units_r_inv)
     3.9      hence oneI: "\<one> \<in> I" by (simp add: a[symmetric])
    3.10  
    3.11      have "carrier R \<subseteq> I"