src/HOL/Algebra/More_Group.thy
changeset 66760 d44ea023ac09
parent 65416 f707dbcf11e3
child 67341 df79ef3b3a41
     1.1 --- a/src/HOL/Algebra/More_Group.thy	Mon Oct 02 19:58:29 2017 +0200
     1.2 +++ b/src/HOL/Algebra/More_Group.thy	Mon Oct 02 22:48:01 2017 +0200
     1.3 @@ -5,8 +5,7 @@
     1.4  section \<open>More on groups\<close>
     1.5  
     1.6  theory More_Group
     1.7 -imports
     1.8 -  Ring
     1.9 +  imports Ring
    1.10  begin
    1.11  
    1.12  text \<open>
    1.13 @@ -16,63 +15,62 @@
    1.14    facts about the unit group within the ring locale.
    1.15  \<close>
    1.16  
    1.17 -definition units_of :: "('a, 'b) monoid_scheme => 'a monoid" where
    1.18 -  "units_of G == (| carrier = Units G,
    1.19 -     Group.monoid.mult = Group.monoid.mult G,
    1.20 -     one  = one G |)"
    1.21 +definition units_of :: "('a, 'b) monoid_scheme \<Rightarrow> 'a monoid"
    1.22 +  where "units_of G =
    1.23 +    \<lparr>carrier = Units G, Group.monoid.mult = Group.monoid.mult G, one  = one G\<rparr>"
    1.24  
    1.25 -lemma (in monoid) units_group: "group(units_of G)"
    1.26 +lemma (in monoid) units_group: "group (units_of G)"
    1.27    apply (unfold units_of_def)
    1.28    apply (rule groupI)
    1.29 -  apply auto
    1.30 -  apply (subst m_assoc)
    1.31 -  apply auto
    1.32 +      apply auto
    1.33 +   apply (subst m_assoc)
    1.34 +      apply auto
    1.35    apply (rule_tac x = "inv x" in bexI)
    1.36 -  apply auto
    1.37 +   apply auto
    1.38    done
    1.39  
    1.40 -lemma (in comm_monoid) units_comm_group: "comm_group(units_of G)"
    1.41 +lemma (in comm_monoid) units_comm_group: "comm_group (units_of G)"
    1.42    apply (rule group.group_comm_groupI)
    1.43 -  apply (rule units_group)
    1.44 +   apply (rule units_group)
    1.45    apply (insert comm_monoid_axioms)
    1.46    apply (unfold units_of_def Units_def comm_monoid_def comm_monoid_axioms_def)
    1.47    apply auto
    1.48    done
    1.49  
    1.50  lemma units_of_carrier: "carrier (units_of G) = Units G"
    1.51 -  unfolding units_of_def by auto
    1.52 +  by (auto simp: units_of_def)
    1.53  
    1.54 -lemma units_of_mult: "mult(units_of G) = mult G"
    1.55 -  unfolding units_of_def by auto
    1.56 +lemma units_of_mult: "mult (units_of G) = mult G"
    1.57 +  by (auto simp: units_of_def)
    1.58  
    1.59 -lemma units_of_one: "one(units_of G) = one G"
    1.60 -  unfolding units_of_def by auto
    1.61 +lemma units_of_one: "one (units_of G) = one G"
    1.62 +  by (auto simp: units_of_def)
    1.63  
    1.64 -lemma (in monoid) units_of_inv: "x : Units G ==> m_inv (units_of G) x = m_inv G x"
    1.65 +lemma (in monoid) units_of_inv: "x \<in> Units G \<Longrightarrow> m_inv (units_of G) x = m_inv G x"
    1.66    apply (rule sym)
    1.67    apply (subst m_inv_def)
    1.68    apply (rule the1_equality)
    1.69 -  apply (rule ex_ex1I)
    1.70 -  apply (subst (asm) Units_def)
    1.71 -  apply auto
    1.72 -  apply (erule inv_unique)
    1.73 -  apply auto
    1.74 -  apply (rule Units_closed)
    1.75 -  apply (simp_all only: units_of_carrier [symmetric])
    1.76 -  apply (insert units_group)
    1.77 -  apply auto
    1.78 -  apply (subst units_of_mult [symmetric])
    1.79 -  apply (subst units_of_one [symmetric])
    1.80 -  apply (erule group.r_inv, assumption)
    1.81 +   apply (rule ex_ex1I)
    1.82 +    apply (subst (asm) Units_def)
    1.83 +    apply auto
    1.84 +     apply (erule inv_unique)
    1.85 +        apply auto
    1.86 +    apply (rule Units_closed)
    1.87 +    apply (simp_all only: units_of_carrier [symmetric])
    1.88 +    apply (insert units_group)
    1.89 +    apply auto
    1.90 +   apply (subst units_of_mult [symmetric])
    1.91 +   apply (subst units_of_one [symmetric])
    1.92 +   apply (erule group.r_inv, assumption)
    1.93    apply (subst units_of_mult [symmetric])
    1.94    apply (subst units_of_one [symmetric])
    1.95    apply (erule group.l_inv, assumption)
    1.96    done
    1.97  
    1.98 -lemma (in group) inj_on_const_mult: "a: (carrier G) ==> inj_on (%x. a \<otimes> x) (carrier G)"
    1.99 +lemma (in group) inj_on_const_mult: "a \<in> carrier G \<Longrightarrow> inj_on (\<lambda>x. a \<otimes> x) (carrier G)"
   1.100    unfolding inj_on_def by auto
   1.101  
   1.102 -lemma (in group) surj_const_mult: "a : (carrier G) ==> (%x. a \<otimes> x) ` (carrier G) = (carrier G)"
   1.103 +lemma (in group) surj_const_mult: "a \<in> carrier G \<Longrightarrow> (\<lambda>x. a \<otimes> x) ` carrier G = carrier G"
   1.104    apply (auto simp add: image_def)
   1.105    apply (rule_tac x = "(m_inv G a) \<otimes> x" in bexI)
   1.106    apply auto
   1.107 @@ -82,33 +80,29 @@
   1.108    apply auto
   1.109    done
   1.110  
   1.111 -lemma (in group) l_cancel_one [simp]:
   1.112 -    "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow> (x \<otimes> a = x) = (a = one G)"
   1.113 +lemma (in group) l_cancel_one [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> x \<otimes> a = x \<longleftrightarrow> a = one G"
   1.114    apply auto
   1.115    apply (subst l_cancel [symmetric])
   1.116 -  prefer 4
   1.117 -  apply (erule ssubst)
   1.118 -  apply auto
   1.119 +     prefer 4
   1.120 +     apply (erule ssubst)
   1.121 +     apply auto
   1.122    done
   1.123  
   1.124 -lemma (in group) r_cancel_one [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
   1.125 -    (a \<otimes> x = x) = (a = one G)"
   1.126 +lemma (in group) r_cancel_one [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> a \<otimes> x = x \<longleftrightarrow> a = one G"
   1.127    apply auto
   1.128    apply (subst r_cancel [symmetric])
   1.129 -  prefer 4
   1.130 -  apply (erule ssubst)
   1.131 -  apply auto
   1.132 +     prefer 4
   1.133 +     apply (erule ssubst)
   1.134 +     apply auto
   1.135    done
   1.136  
   1.137  (* Is there a better way to do this? *)
   1.138 -lemma (in group) l_cancel_one' [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
   1.139 -    (x = x \<otimes> a) = (a = one G)"
   1.140 +lemma (in group) l_cancel_one' [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> x = x \<otimes> a \<longleftrightarrow> a = one G"
   1.141    apply (subst eq_commute)
   1.142    apply simp
   1.143    done
   1.144  
   1.145 -lemma (in group) r_cancel_one' [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
   1.146 -    (x = a \<otimes> x) = (a = one G)"
   1.147 +lemma (in group) r_cancel_one' [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> x = a \<otimes> x \<longleftrightarrow> a = one G"
   1.148    apply (subst eq_commute)
   1.149    apply simp
   1.150    done
   1.151 @@ -118,7 +112,7 @@
   1.152  
   1.153  lemma (in comm_group) power_order_eq_one:
   1.154    assumes fin [simp]: "finite (carrier G)"
   1.155 -    and a [simp]: "a : carrier G"
   1.156 +    and a [simp]: "a \<in> carrier G"
   1.157    shows "a (^) card(carrier G) = one G"
   1.158  proof -
   1.159    have "(\<Otimes>x\<in>carrier G. x) = (\<Otimes>x\<in>carrier G. a \<otimes> x)"