src/HOL/Number_Theory/MiscAlgebra.thy
changeset 32479 521cc9bf2958
parent 31952 40501bb2d57c
child 35416 d8d7d1b785af
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Number_Theory/MiscAlgebra.thy	Tue Sep 01 15:39:33 2009 +0200
     1.3 @@ -0,0 +1,355 @@
     1.4 +(*  Title:      MiscAlgebra.thy
     1.5 +    Author:     Jeremy Avigad
     1.6 +
     1.7 +These are things that can be added to the Algebra library.
     1.8 +*)
     1.9 +
    1.10 +theory MiscAlgebra
    1.11 +imports
    1.12 +  "~~/src/HOL/Algebra/Ring"
    1.13 +  "~~/src/HOL/Algebra/FiniteProduct"
    1.14 +begin;
    1.15 +
    1.16 +(* finiteness stuff *)
    1.17 +
    1.18 +lemma bounded_set1_int [intro]: "finite {(x::int). a < x & x < b & P x}" 
    1.19 +  apply (subgoal_tac "{x. a < x & x < b & P x} <= {a<..<b}")
    1.20 +  apply (erule finite_subset)
    1.21 +  apply auto
    1.22 +done
    1.23 +
    1.24 +
    1.25 +(* The rest is for the algebra libraries *)
    1.26 +
    1.27 +(* These go in Group.thy. *)
    1.28 +
    1.29 +(*
    1.30 +  Show that the units in any monoid give rise to a group.
    1.31 +
    1.32 +  The file Residues.thy provides some infrastructure to use
    1.33 +  facts about the unit group within the ring locale.
    1.34 +*)
    1.35 +
    1.36 +
    1.37 +constdefs 
    1.38 +  units_of :: "('a, 'b) monoid_scheme => 'a monoid"
    1.39 +  "units_of G == (| carrier = Units G,
    1.40 +     Group.monoid.mult = Group.monoid.mult G,
    1.41 +     one  = one G |)";
    1.42 +
    1.43 +(*
    1.44 +
    1.45 +lemma (in monoid) Units_mult_closed [intro]:
    1.46 +  "x : Units G ==> y : Units G ==> x \<otimes> y : Units G"
    1.47 +  apply (unfold Units_def)
    1.48 +  apply (clarsimp)
    1.49 +  apply (rule_tac x = "xaa \<otimes> xa" in bexI)
    1.50 +  apply auto
    1.51 +  apply (subst m_assoc)
    1.52 +  apply auto
    1.53 +  apply (subst (2) m_assoc [symmetric])
    1.54 +  apply auto
    1.55 +  apply (subst m_assoc)
    1.56 +  apply auto
    1.57 +  apply (subst (2) m_assoc [symmetric])
    1.58 +  apply auto
    1.59 +done
    1.60 +
    1.61 +*)
    1.62 +
    1.63 +lemma (in monoid) units_group: "group(units_of G)"
    1.64 +  apply (unfold units_of_def)
    1.65 +  apply (rule groupI)
    1.66 +  apply auto
    1.67 +  apply (subst m_assoc)
    1.68 +  apply auto
    1.69 +  apply (rule_tac x = "inv x" in bexI)
    1.70 +  apply auto
    1.71 +done
    1.72 +
    1.73 +lemma (in comm_monoid) units_comm_group: "comm_group(units_of G)"
    1.74 +  apply (rule group.group_comm_groupI)
    1.75 +  apply (rule units_group)
    1.76 +  apply (insert prems)
    1.77 +  apply (unfold units_of_def Units_def comm_monoid_def comm_monoid_axioms_def)
    1.78 +  apply auto;
    1.79 +done;
    1.80 +
    1.81 +lemma units_of_carrier: "carrier (units_of G) = Units G"
    1.82 +  by (unfold units_of_def, auto)
    1.83 +
    1.84 +lemma units_of_mult: "mult(units_of G) = mult G"
    1.85 +  by (unfold units_of_def, auto)
    1.86 +
    1.87 +lemma units_of_one: "one(units_of G) = one G"
    1.88 +  by (unfold units_of_def, auto)
    1.89 +
    1.90 +lemma (in monoid) units_of_inv: "x : Units G ==> 
    1.91 +    m_inv (units_of G) x = m_inv G x"
    1.92 +  apply (rule sym)
    1.93 +  apply (subst m_inv_def)
    1.94 +  apply (rule the1_equality)
    1.95 +  apply (rule ex_ex1I)
    1.96 +  apply (subst (asm) Units_def)
    1.97 +  apply auto
    1.98 +  apply (erule inv_unique)
    1.99 +  apply auto
   1.100 +  apply (rule Units_closed)
   1.101 +  apply (simp_all only: units_of_carrier [symmetric])
   1.102 +  apply (insert units_group)
   1.103 +  apply auto
   1.104 +  apply (subst units_of_mult [symmetric])
   1.105 +  apply (subst units_of_one [symmetric])
   1.106 +  apply (erule group.r_inv, assumption)
   1.107 +  apply (subst units_of_mult [symmetric])
   1.108 +  apply (subst units_of_one [symmetric])
   1.109 +  apply (erule group.l_inv, assumption)
   1.110 +done
   1.111 +
   1.112 +lemma (in group) inj_on_const_mult: "a: (carrier G) ==> 
   1.113 +    inj_on (%x. a \<otimes> x) (carrier G)"
   1.114 +  by (unfold inj_on_def, auto)
   1.115 +
   1.116 +lemma (in group) surj_const_mult: "a : (carrier G) ==>
   1.117 +    (%x. a \<otimes> x) ` (carrier G) = (carrier G)" 
   1.118 +  apply (auto simp add: image_def)
   1.119 +  apply (rule_tac x = "(m_inv G a) \<otimes> x" in bexI)
   1.120 +  apply auto
   1.121 +(* auto should get this. I suppose we need "comm_monoid_simprules"
   1.122 +   for mult_ac rewriting. *)
   1.123 +  apply (subst m_assoc [symmetric])
   1.124 +  apply auto
   1.125 +done
   1.126 +
   1.127 +lemma (in group) l_cancel_one [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
   1.128 +    (x \<otimes> a = x) = (a = one G)"
   1.129 +  apply auto
   1.130 +  apply (subst l_cancel [symmetric])
   1.131 +  prefer 4
   1.132 +  apply (erule ssubst)
   1.133 +  apply auto
   1.134 +done
   1.135 +
   1.136 +lemma (in group) r_cancel_one [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
   1.137 +    (a \<otimes> x = x) = (a = one G)"
   1.138 +  apply auto
   1.139 +  apply (subst r_cancel [symmetric])
   1.140 +  prefer 4
   1.141 +  apply (erule ssubst)
   1.142 +  apply auto
   1.143 +done
   1.144 +
   1.145 +(* Is there a better way to do this? *)
   1.146 +
   1.147 +lemma (in group) l_cancel_one' [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
   1.148 +    (x = x \<otimes> a) = (a = one G)"
   1.149 +  by (subst eq_commute, simp)
   1.150 +
   1.151 +lemma (in group) r_cancel_one' [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
   1.152 +    (x = a \<otimes> x) = (a = one G)"
   1.153 +  by (subst eq_commute, simp)
   1.154 +
   1.155 +(* This should be generalized to arbitrary groups, not just commutative
   1.156 +   ones, using Lagrange's theorem. *)
   1.157 +
   1.158 +lemma (in comm_group) power_order_eq_one:
   1.159 +    assumes fin [simp]: "finite (carrier G)"
   1.160 +        and a [simp]: "a : carrier G" 
   1.161 +      shows "a (^) card(carrier G) = one G" 
   1.162 +proof -
   1.163 +  have "(\<Otimes>x:carrier G. x) = (\<Otimes>x:carrier G. a \<otimes> x)"
   1.164 +    by (subst (2) finprod_reindex [symmetric], 
   1.165 +      auto simp add: Pi_def inj_on_const_mult surj_const_mult)
   1.166 +  also have "\<dots> = (\<Otimes>x:carrier G. a) \<otimes> (\<Otimes>x:carrier G. x)"
   1.167 +    by (auto simp add: finprod_multf Pi_def)
   1.168 +  also have "(\<Otimes>x:carrier G. a) = a (^) card(carrier G)"
   1.169 +    by (auto simp add: finprod_const)
   1.170 +  finally show ?thesis
   1.171 +(* uses the preceeding lemma *)
   1.172 +    by auto
   1.173 +qed
   1.174 +
   1.175 +
   1.176 +(* Miscellaneous *)
   1.177 +
   1.178 +lemma (in cring) field_intro2: "\<zero>\<^bsub>R\<^esub> ~= \<one>\<^bsub>R\<^esub> \<Longrightarrow> ALL x : carrier R - {\<zero>\<^bsub>R\<^esub>}.
   1.179 +    x : Units R \<Longrightarrow> field R"
   1.180 +  apply (unfold_locales)
   1.181 +  apply (insert prems, auto)
   1.182 +  apply (rule trans)
   1.183 +  apply (subgoal_tac "a = (a \<otimes> b) \<otimes> inv b")
   1.184 +  apply assumption
   1.185 +  apply (subst m_assoc) 
   1.186 +  apply (auto simp add: Units_r_inv)
   1.187 +  apply (unfold Units_def)
   1.188 +  apply auto
   1.189 +done
   1.190 +
   1.191 +lemma (in monoid) inv_char: "x : carrier G \<Longrightarrow> y : carrier G \<Longrightarrow>
   1.192 +  x \<otimes> y = \<one> \<Longrightarrow> y \<otimes> x = \<one> \<Longrightarrow> inv x = y"
   1.193 +  apply (subgoal_tac "x : Units G")
   1.194 +  apply (subgoal_tac "y = inv x \<otimes> \<one>")
   1.195 +  apply simp
   1.196 +  apply (erule subst)
   1.197 +  apply (subst m_assoc [symmetric])
   1.198 +  apply auto
   1.199 +  apply (unfold Units_def)
   1.200 +  apply auto
   1.201 +done
   1.202 +
   1.203 +lemma (in comm_monoid) comm_inv_char: "x : carrier G \<Longrightarrow> y : carrier G \<Longrightarrow>
   1.204 +  x \<otimes> y = \<one> \<Longrightarrow> inv x = y"
   1.205 +  apply (rule inv_char)
   1.206 +  apply auto
   1.207 +  apply (subst m_comm, auto) 
   1.208 +done
   1.209 +
   1.210 +lemma (in ring) inv_neg_one [simp]: "inv (\<ominus> \<one>) = \<ominus> \<one>"  
   1.211 +  apply (rule inv_char)
   1.212 +  apply (auto simp add: l_minus r_minus)
   1.213 +done
   1.214 +
   1.215 +lemma (in monoid) inv_eq_imp_eq: "x : Units G \<Longrightarrow> y : Units G \<Longrightarrow> 
   1.216 +    inv x = inv y \<Longrightarrow> x = y"
   1.217 +  apply (subgoal_tac "inv(inv x) = inv(inv y)")
   1.218 +  apply (subst (asm) Units_inv_inv)+
   1.219 +  apply auto
   1.220 +done
   1.221 +
   1.222 +lemma (in ring) Units_minus_one_closed [intro]: "\<ominus> \<one> : Units R"
   1.223 +  apply (unfold Units_def)
   1.224 +  apply auto
   1.225 +  apply (rule_tac x = "\<ominus> \<one>" in bexI)
   1.226 +  apply auto
   1.227 +  apply (simp add: l_minus r_minus)
   1.228 +done
   1.229 +
   1.230 +lemma (in monoid) inv_one [simp]: "inv \<one> = \<one>"
   1.231 +  apply (rule inv_char)
   1.232 +  apply auto
   1.233 +done
   1.234 +
   1.235 +lemma (in ring) inv_eq_neg_one_eq: "x : Units R \<Longrightarrow> (inv x = \<ominus> \<one>) = (x = \<ominus> \<one>)"
   1.236 +  apply auto
   1.237 +  apply (subst Units_inv_inv [symmetric])
   1.238 +  apply auto
   1.239 +done
   1.240 +
   1.241 +lemma (in monoid) inv_eq_one_eq: "x : Units G \<Longrightarrow> (inv x = \<one>) = (x = \<one>)"
   1.242 +  apply auto
   1.243 +  apply (subst Units_inv_inv [symmetric])
   1.244 +  apply auto
   1.245 +done
   1.246 +
   1.247 +
   1.248 +(* This goes in FiniteProduct *)
   1.249 +
   1.250 +lemma (in comm_monoid) finprod_UN_disjoint:
   1.251 +  "finite I \<Longrightarrow> (ALL i:I. finite (A i)) \<longrightarrow> (ALL i:I. ALL j:I. i ~= j \<longrightarrow>
   1.252 +     (A i) Int (A j) = {}) \<longrightarrow>
   1.253 +      (ALL i:I. ALL x: (A i). g x : carrier G) \<longrightarrow>
   1.254 +        finprod G g (UNION I A) = finprod G (%i. finprod G g (A i)) I"
   1.255 +  apply (induct set: finite)
   1.256 +  apply force
   1.257 +  apply clarsimp
   1.258 +  apply (subst finprod_Un_disjoint)
   1.259 +  apply blast
   1.260 +  apply (erule finite_UN_I)
   1.261 +  apply blast
   1.262 +  apply (fastsimp)
   1.263 +  apply (auto intro!: funcsetI finprod_closed) 
   1.264 +done
   1.265 +
   1.266 +lemma (in comm_monoid) finprod_Union_disjoint:
   1.267 +  "[| finite C; (ALL A:C. finite A & (ALL x:A. f x : carrier G));
   1.268 +      (ALL A:C. ALL B:C. A ~= B --> A Int B = {}) |] 
   1.269 +   ==> finprod G f (Union C) = finprod G (finprod G f) C" 
   1.270 +  apply (frule finprod_UN_disjoint [of C id f])
   1.271 +  apply (unfold Union_def id_def, auto)
   1.272 +done
   1.273 +
   1.274 +lemma (in comm_monoid) finprod_one [rule_format]: 
   1.275 +  "finite A \<Longrightarrow> (ALL x:A. f x = \<one>) \<longrightarrow>
   1.276 +     finprod G f A = \<one>"
   1.277 +by (induct set: finite) auto
   1.278 +
   1.279 +
   1.280 +(* need better simplification rules for rings *)
   1.281 +(* the next one holds more generally for abelian groups *)
   1.282 +
   1.283 +lemma (in cring) sum_zero_eq_neg:
   1.284 +  "x : carrier R \<Longrightarrow> y : carrier R \<Longrightarrow> x \<oplus> y = \<zero> \<Longrightarrow> x = \<ominus> y"
   1.285 +  apply (subgoal_tac "\<ominus> y = \<zero> \<oplus> \<ominus> y") 
   1.286 +  apply (erule ssubst)back
   1.287 +  apply (erule subst)
   1.288 +  apply (simp add: ring_simprules)+
   1.289 +done
   1.290 +
   1.291 +(* there's a name conflict -- maybe "domain" should be
   1.292 +   "integral_domain" *)
   1.293 +
   1.294 +lemma (in Ring.domain) square_eq_one: 
   1.295 +  fixes x
   1.296 +  assumes [simp]: "x : carrier R" and
   1.297 +    "x \<otimes> x = \<one>"
   1.298 +  shows "x = \<one> | x = \<ominus>\<one>"
   1.299 +proof -
   1.300 +  have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = x \<otimes> x \<oplus> \<ominus> \<one>"
   1.301 +    by (simp add: ring_simprules)
   1.302 +  also with `x \<otimes> x = \<one>` have "\<dots> = \<zero>"
   1.303 +    by (simp add: ring_simprules)
   1.304 +  finally have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = \<zero>" .
   1.305 +  hence "(x \<oplus> \<one>) = \<zero> | (x \<oplus> \<ominus> \<one>) = \<zero>"
   1.306 +    by (intro integral, auto)
   1.307 +  thus ?thesis
   1.308 +    apply auto
   1.309 +    apply (erule notE)
   1.310 +    apply (rule sum_zero_eq_neg)
   1.311 +    apply auto
   1.312 +    apply (subgoal_tac "x = \<ominus> (\<ominus> \<one>)")
   1.313 +    apply (simp add: ring_simprules) 
   1.314 +    apply (rule sum_zero_eq_neg)
   1.315 +    apply auto
   1.316 +    done
   1.317 +qed
   1.318 +
   1.319 +lemma (in Ring.domain) inv_eq_self: "x : Units R \<Longrightarrow>
   1.320 +    x = inv x \<Longrightarrow> x = \<one> | x = \<ominus> \<one>"
   1.321 +  apply (rule square_eq_one)
   1.322 +  apply auto
   1.323 +  apply (erule ssubst)back
   1.324 +  apply (erule Units_r_inv)
   1.325 +done
   1.326 +
   1.327 +
   1.328 +(*
   1.329 +  The following translates theorems about groups to the facts about
   1.330 +  the units of a ring. (The list should be expanded as more things are
   1.331 +  needed.)
   1.332 +*)
   1.333 +
   1.334 +lemma (in ring) finite_ring_finite_units [intro]: "finite (carrier R) \<Longrightarrow> 
   1.335 +    finite (Units R)"
   1.336 +  by (rule finite_subset, auto)
   1.337 +
   1.338 +(* this belongs with MiscAlgebra.thy *)
   1.339 +lemma (in monoid) units_of_pow: 
   1.340 +    "x : Units G \<Longrightarrow> x (^)\<^bsub>units_of G\<^esub> (n::nat) = x (^)\<^bsub>G\<^esub> n"
   1.341 +  apply (induct n)
   1.342 +  apply (auto simp add: units_group group.is_monoid  
   1.343 +    monoid.nat_pow_0 monoid.nat_pow_Suc units_of_one units_of_mult
   1.344 +    One_nat_def)
   1.345 +done
   1.346 +
   1.347 +lemma (in cring) units_power_order_eq_one: "finite (Units R) \<Longrightarrow> a : Units R
   1.348 +    \<Longrightarrow> a (^) card(Units R) = \<one>"
   1.349 +  apply (subst units_of_carrier [symmetric])
   1.350 +  apply (subst units_of_one [symmetric])
   1.351 +  apply (subst units_of_pow [symmetric])
   1.352 +  apply assumption
   1.353 +  apply (rule comm_group.power_order_eq_one)
   1.354 +  apply (rule units_comm_group)
   1.355 +  apply (unfold units_of_def, auto)
   1.356 +done
   1.357 +
   1.358 +end