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
```