src/HOL/Number_Theory/MiscAlgebra.thy
 author haftmann Thu Jul 02 10:06:47 2015 +0200 (2015-07-02) changeset 60634 e3b6e516608b parent 60527 eb431a5651fe child 60773 d09c66a0ea10 permissions -rw-r--r--
separate (semi)ring with normalization
 wenzelm@41959 ` 1` ```(* Title: HOL/Number_Theory/MiscAlgebra.thy ``` nipkow@31719 ` 2` ``` Author: Jeremy Avigad ``` wenzelm@60527 ` 3` ```*) ``` nipkow@31719 ` 4` wenzelm@60527 ` 5` ```section \Things that can be added to the Algebra library\ ``` nipkow@31719 ` 6` nipkow@31719 ` 7` ```theory MiscAlgebra ``` haftmann@31772 ` 8` ```imports ``` nipkow@31719 ` 9` ``` "~~/src/HOL/Algebra/Ring" ``` nipkow@31719 ` 10` ``` "~~/src/HOL/Algebra/FiniteProduct" ``` haftmann@44106 ` 11` ```begin ``` nipkow@31719 ` 12` wenzelm@60527 ` 13` ```subsection \Finiteness stuff\ ``` nipkow@31719 ` 14` wenzelm@44872 ` 15` ```lemma bounded_set1_int [intro]: "finite {(x::int). a < x & x < b & P x}" ``` nipkow@31719 ` 16` ``` apply (subgoal_tac "{x. a < x & x < b & P x} <= {a<..The rest is for the algebra libraries\ ``` nipkow@31719 ` 23` wenzelm@60527 ` 24` ```subsubsection \These go in Group.thy\ ``` nipkow@31719 ` 25` wenzelm@60527 ` 26` ```text \ ``` nipkow@31719 ` 27` ``` Show that the units in any monoid give rise to a group. ``` nipkow@31719 ` 28` nipkow@31719 ` 29` ``` The file Residues.thy provides some infrastructure to use ``` nipkow@31719 ` 30` ``` facts about the unit group within the ring locale. ``` wenzelm@60527 ` 31` ```\ ``` nipkow@31719 ` 32` haftmann@35416 ` 33` ```definition units_of :: "('a, 'b) monoid_scheme => 'a monoid" where ``` nipkow@31719 ` 34` ``` "units_of G == (| carrier = Units G, ``` nipkow@31719 ` 35` ``` Group.monoid.mult = Group.monoid.mult G, ``` haftmann@44106 ` 36` ``` one = one G |)" ``` nipkow@31719 ` 37` nipkow@31719 ` 38` ```(* ``` nipkow@31719 ` 39` nipkow@31719 ` 40` ```lemma (in monoid) Units_mult_closed [intro]: ``` nipkow@31719 ` 41` ``` "x : Units G ==> y : Units G ==> x \ y : Units G" ``` nipkow@31719 ` 42` ``` apply (unfold Units_def) ``` nipkow@31719 ` 43` ``` apply (clarsimp) ``` nipkow@31719 ` 44` ``` apply (rule_tac x = "xaa \ xa" in bexI) ``` nipkow@31719 ` 45` ``` apply auto ``` nipkow@31719 ` 46` ``` apply (subst m_assoc) ``` nipkow@31719 ` 47` ``` apply auto ``` nipkow@31719 ` 48` ``` apply (subst (2) m_assoc [symmetric]) ``` nipkow@31719 ` 49` ``` apply auto ``` nipkow@31719 ` 50` ``` apply (subst m_assoc) ``` nipkow@31719 ` 51` ``` apply auto ``` nipkow@31719 ` 52` ``` apply (subst (2) m_assoc [symmetric]) ``` nipkow@31719 ` 53` ``` apply auto ``` nipkow@31719 ` 54` ```done ``` nipkow@31719 ` 55` nipkow@31719 ` 56` ```*) ``` nipkow@31719 ` 57` nipkow@31719 ` 58` ```lemma (in monoid) units_group: "group(units_of G)" ``` nipkow@31719 ` 59` ``` apply (unfold units_of_def) ``` nipkow@31719 ` 60` ``` apply (rule groupI) ``` nipkow@31719 ` 61` ``` apply auto ``` nipkow@31719 ` 62` ``` apply (subst m_assoc) ``` nipkow@31719 ` 63` ``` apply auto ``` nipkow@31719 ` 64` ``` apply (rule_tac x = "inv x" in bexI) ``` nipkow@31719 ` 65` ``` apply auto ``` wenzelm@44872 ` 66` ``` done ``` nipkow@31719 ` 67` nipkow@31719 ` 68` ```lemma (in comm_monoid) units_comm_group: "comm_group(units_of G)" ``` nipkow@31719 ` 69` ``` apply (rule group.group_comm_groupI) ``` nipkow@31719 ` 70` ``` apply (rule units_group) ``` wenzelm@41541 ` 71` ``` apply (insert comm_monoid_axioms) ``` nipkow@31719 ` 72` ``` apply (unfold units_of_def Units_def comm_monoid_def comm_monoid_axioms_def) ``` wenzelm@41541 ` 73` ``` apply auto ``` wenzelm@41541 ` 74` ``` done ``` nipkow@31719 ` 75` nipkow@31719 ` 76` ```lemma units_of_carrier: "carrier (units_of G) = Units G" ``` wenzelm@44872 ` 77` ``` unfolding units_of_def by auto ``` nipkow@31719 ` 78` nipkow@31719 ` 79` ```lemma units_of_mult: "mult(units_of G) = mult G" ``` wenzelm@44872 ` 80` ``` unfolding units_of_def by auto ``` nipkow@31719 ` 81` nipkow@31719 ` 82` ```lemma units_of_one: "one(units_of G) = one G" ``` wenzelm@44872 ` 83` ``` unfolding units_of_def by auto ``` nipkow@31719 ` 84` wenzelm@60527 ` 85` ```lemma (in monoid) units_of_inv: "x : Units G ==> m_inv (units_of G) x = m_inv G x" ``` nipkow@31719 ` 86` ``` apply (rule sym) ``` nipkow@31719 ` 87` ``` apply (subst m_inv_def) ``` nipkow@31719 ` 88` ``` apply (rule the1_equality) ``` nipkow@31719 ` 89` ``` apply (rule ex_ex1I) ``` nipkow@31719 ` 90` ``` apply (subst (asm) Units_def) ``` nipkow@31719 ` 91` ``` apply auto ``` nipkow@31719 ` 92` ``` apply (erule inv_unique) ``` nipkow@31719 ` 93` ``` apply auto ``` nipkow@31719 ` 94` ``` apply (rule Units_closed) ``` nipkow@31719 ` 95` ``` apply (simp_all only: units_of_carrier [symmetric]) ``` nipkow@31719 ` 96` ``` apply (insert units_group) ``` nipkow@31719 ` 97` ``` apply auto ``` nipkow@31719 ` 98` ``` apply (subst units_of_mult [symmetric]) ``` nipkow@31719 ` 99` ``` apply (subst units_of_one [symmetric]) ``` nipkow@31719 ` 100` ``` apply (erule group.r_inv, assumption) ``` nipkow@31719 ` 101` ``` apply (subst units_of_mult [symmetric]) ``` nipkow@31719 ` 102` ``` apply (subst units_of_one [symmetric]) ``` nipkow@31719 ` 103` ``` apply (erule group.l_inv, assumption) ``` wenzelm@60527 ` 104` ``` done ``` nipkow@31719 ` 105` wenzelm@60527 ` 106` ```lemma (in group) inj_on_const_mult: "a: (carrier G) ==> inj_on (%x. a \ x) (carrier G)" ``` wenzelm@44872 ` 107` ``` unfolding inj_on_def by auto ``` nipkow@31719 ` 108` wenzelm@60527 ` 109` ```lemma (in group) surj_const_mult: "a : (carrier G) ==> (%x. a \ x) ` (carrier G) = (carrier G)" ``` nipkow@31719 ` 110` ``` apply (auto simp add: image_def) ``` nipkow@31719 ` 111` ``` apply (rule_tac x = "(m_inv G a) \ x" in bexI) ``` nipkow@31719 ` 112` ``` apply auto ``` nipkow@31719 ` 113` ```(* auto should get this. I suppose we need "comm_monoid_simprules" ``` haftmann@57514 ` 114` ``` for ac_simps rewriting. *) ``` nipkow@31719 ` 115` ``` apply (subst m_assoc [symmetric]) ``` nipkow@31719 ` 116` ``` apply auto ``` wenzelm@44872 ` 117` ``` done ``` nipkow@31719 ` 118` wenzelm@60527 ` 119` ```lemma (in group) l_cancel_one [simp]: ``` wenzelm@60527 ` 120` ``` "x : carrier G \ a : carrier G \ (x \ a = x) = (a = one G)" ``` nipkow@31719 ` 121` ``` apply auto ``` nipkow@31719 ` 122` ``` apply (subst l_cancel [symmetric]) ``` nipkow@31719 ` 123` ``` prefer 4 ``` nipkow@31719 ` 124` ``` apply (erule ssubst) ``` nipkow@31719 ` 125` ``` apply auto ``` wenzelm@44872 ` 126` ``` done ``` nipkow@31719 ` 127` nipkow@31719 ` 128` ```lemma (in group) r_cancel_one [simp]: "x : carrier G \ a : carrier G \ ``` nipkow@31719 ` 129` ``` (a \ x = x) = (a = one G)" ``` nipkow@31719 ` 130` ``` apply auto ``` nipkow@31719 ` 131` ``` apply (subst r_cancel [symmetric]) ``` nipkow@31719 ` 132` ``` prefer 4 ``` nipkow@31719 ` 133` ``` apply (erule ssubst) ``` nipkow@31719 ` 134` ``` apply auto ``` wenzelm@44872 ` 135` ``` done ``` nipkow@31719 ` 136` nipkow@31719 ` 137` ```(* Is there a better way to do this? *) ``` nipkow@31719 ` 138` ```lemma (in group) l_cancel_one' [simp]: "x : carrier G \ a : carrier G \ ``` nipkow@31719 ` 139` ``` (x = x \ a) = (a = one G)" ``` wenzelm@44872 ` 140` ``` apply (subst eq_commute) ``` wenzelm@44872 ` 141` ``` apply simp ``` wenzelm@44872 ` 142` ``` done ``` nipkow@31719 ` 143` nipkow@31719 ` 144` ```lemma (in group) r_cancel_one' [simp]: "x : carrier G \ a : carrier G \ ``` nipkow@31719 ` 145` ``` (x = a \ x) = (a = one G)" ``` wenzelm@44872 ` 146` ``` apply (subst eq_commute) ``` wenzelm@44872 ` 147` ``` apply simp ``` wenzelm@44872 ` 148` ``` done ``` nipkow@31719 ` 149` nipkow@31719 ` 150` ```(* This should be generalized to arbitrary groups, not just commutative ``` nipkow@31719 ` 151` ``` ones, using Lagrange's theorem. *) ``` nipkow@31719 ` 152` nipkow@31719 ` 153` ```lemma (in comm_group) power_order_eq_one: ``` wenzelm@44872 ` 154` ``` assumes fin [simp]: "finite (carrier G)" ``` wenzelm@44872 ` 155` ``` and a [simp]: "a : carrier G" ``` wenzelm@44872 ` 156` ``` shows "a (^) card(carrier G) = one G" ``` nipkow@31719 ` 157` ```proof - ``` nipkow@31719 ` 158` ``` have "(\x:carrier G. x) = (\x:carrier G. a \ x)" ``` wenzelm@44872 ` 159` ``` by (subst (2) finprod_reindex [symmetric], ``` nipkow@31719 ` 160` ``` auto simp add: Pi_def inj_on_const_mult surj_const_mult) ``` nipkow@31719 ` 161` ``` also have "\ = (\x:carrier G. a) \ (\x:carrier G. x)" ``` nipkow@31719 ` 162` ``` by (auto simp add: finprod_multf Pi_def) ``` nipkow@31719 ` 163` ``` also have "(\x:carrier G. a) = a (^) card(carrier G)" ``` nipkow@31719 ` 164` ``` by (auto simp add: finprod_const) ``` nipkow@31719 ` 165` ``` finally show ?thesis ``` nipkow@31719 ` 166` ```(* uses the preceeding lemma *) ``` nipkow@31719 ` 167` ``` by auto ``` nipkow@31719 ` 168` ```qed ``` nipkow@31719 ` 169` nipkow@31719 ` 170` wenzelm@60527 ` 171` ```subsubsection \Miscellaneous\ ``` nipkow@31719 ` 172` wenzelm@60527 ` 173` ```lemma (in cring) field_intro2: "\\<^bsub>R\<^esub> ~= \\<^bsub>R\<^esub> \ \x \ carrier R - {\\<^bsub>R\<^esub>}. x \ Units R \ field R" ``` nipkow@31719 ` 174` ``` apply (unfold_locales) ``` wenzelm@41541 ` 175` ``` apply (insert cring_axioms, auto) ``` nipkow@31719 ` 176` ``` apply (rule trans) ``` nipkow@31719 ` 177` ``` apply (subgoal_tac "a = (a \ b) \ inv b") ``` nipkow@31719 ` 178` ``` apply assumption ``` wenzelm@44872 ` 179` ``` apply (subst m_assoc) ``` wenzelm@41541 ` 180` ``` apply auto ``` nipkow@31719 ` 181` ``` apply (unfold Units_def) ``` nipkow@31719 ` 182` ``` apply auto ``` wenzelm@41541 ` 183` ``` done ``` nipkow@31719 ` 184` nipkow@31719 ` 185` ```lemma (in monoid) inv_char: "x : carrier G \ y : carrier G \ ``` wenzelm@41541 ` 186` ``` x \ y = \ \ y \ x = \ \ inv x = y" ``` nipkow@31719 ` 187` ``` apply (subgoal_tac "x : Units G") ``` nipkow@31719 ` 188` ``` apply (subgoal_tac "y = inv x \ \") ``` nipkow@31719 ` 189` ``` apply simp ``` nipkow@31719 ` 190` ``` apply (erule subst) ``` nipkow@31719 ` 191` ``` apply (subst m_assoc [symmetric]) ``` nipkow@31719 ` 192` ``` apply auto ``` nipkow@31719 ` 193` ``` apply (unfold Units_def) ``` nipkow@31719 ` 194` ``` apply auto ``` wenzelm@41541 ` 195` ``` done ``` nipkow@31719 ` 196` nipkow@31719 ` 197` ```lemma (in comm_monoid) comm_inv_char: "x : carrier G \ y : carrier G \ ``` nipkow@31719 ` 198` ``` x \ y = \ \ inv x = y" ``` nipkow@31719 ` 199` ``` apply (rule inv_char) ``` nipkow@31719 ` 200` ``` apply auto ``` wenzelm@44872 ` 201` ``` apply (subst m_comm, auto) ``` wenzelm@41541 ` 202` ``` done ``` nipkow@31719 ` 203` wenzelm@44872 ` 204` ```lemma (in ring) inv_neg_one [simp]: "inv (\ \) = \ \" ``` nipkow@31719 ` 205` ``` apply (rule inv_char) ``` nipkow@31719 ` 206` ``` apply (auto simp add: l_minus r_minus) ``` wenzelm@41541 ` 207` ``` done ``` nipkow@31719 ` 208` wenzelm@44872 ` 209` ```lemma (in monoid) inv_eq_imp_eq: "x : Units G \ y : Units G \ ``` nipkow@31719 ` 210` ``` inv x = inv y \ x = y" ``` nipkow@31719 ` 211` ``` apply (subgoal_tac "inv(inv x) = inv(inv y)") ``` nipkow@31719 ` 212` ``` apply (subst (asm) Units_inv_inv)+ ``` nipkow@31719 ` 213` ``` apply auto ``` wenzelm@44872 ` 214` ``` done ``` nipkow@31719 ` 215` nipkow@31719 ` 216` ```lemma (in ring) Units_minus_one_closed [intro]: "\ \ : Units R" ``` nipkow@31719 ` 217` ``` apply (unfold Units_def) ``` nipkow@31719 ` 218` ``` apply auto ``` nipkow@31719 ` 219` ``` apply (rule_tac x = "\ \" in bexI) ``` nipkow@31719 ` 220` ``` apply auto ``` nipkow@31719 ` 221` ``` apply (simp add: l_minus r_minus) ``` wenzelm@44872 ` 222` ``` done ``` nipkow@31719 ` 223` nipkow@31719 ` 224` ```lemma (in monoid) inv_one [simp]: "inv \ = \" ``` nipkow@31719 ` 225` ``` apply (rule inv_char) ``` nipkow@31719 ` 226` ``` apply auto ``` wenzelm@44872 ` 227` ``` done ``` nipkow@31719 ` 228` nipkow@31719 ` 229` ```lemma (in ring) inv_eq_neg_one_eq: "x : Units R \ (inv x = \ \) = (x = \ \)" ``` nipkow@31719 ` 230` ``` apply auto ``` nipkow@31719 ` 231` ``` apply (subst Units_inv_inv [symmetric]) ``` nipkow@31719 ` 232` ``` apply auto ``` wenzelm@44872 ` 233` ``` done ``` nipkow@31719 ` 234` nipkow@31719 ` 235` ```lemma (in monoid) inv_eq_one_eq: "x : Units G \ (inv x = \) = (x = \)" ``` wenzelm@60527 ` 236` ``` by (metis Units_inv_inv inv_one) ``` nipkow@31719 ` 237` nipkow@31719 ` 238` wenzelm@60527 ` 239` ```subsubsection \This goes in FiniteProduct\ ``` nipkow@31719 ` 240` nipkow@31719 ` 241` ```lemma (in comm_monoid) finprod_UN_disjoint: ``` nipkow@31719 ` 242` ``` "finite I \ (ALL i:I. finite (A i)) \ (ALL i:I. ALL j:I. i ~= j \ ``` nipkow@31719 ` 243` ``` (A i) Int (A j) = {}) \ ``` nipkow@31719 ` 244` ``` (ALL i:I. ALL x: (A i). g x : carrier G) \ ``` nipkow@31719 ` 245` ``` finprod G g (UNION I A) = finprod G (%i. finprod G g (A i)) I" ``` nipkow@31719 ` 246` ``` apply (induct set: finite) ``` nipkow@31719 ` 247` ``` apply force ``` nipkow@31719 ` 248` ``` apply clarsimp ``` nipkow@31719 ` 249` ``` apply (subst finprod_Un_disjoint) ``` nipkow@31719 ` 250` ``` apply blast ``` nipkow@31719 ` 251` ``` apply (erule finite_UN_I) ``` nipkow@31719 ` 252` ``` apply blast ``` nipkow@44890 ` 253` ``` apply (fastforce) ``` wenzelm@44872 ` 254` ``` apply (auto intro!: funcsetI finprod_closed) ``` wenzelm@44872 ` 255` ``` done ``` nipkow@31719 ` 256` nipkow@31719 ` 257` ```lemma (in comm_monoid) finprod_Union_disjoint: ``` nipkow@31719 ` 258` ``` "[| finite C; (ALL A:C. finite A & (ALL x:A. f x : carrier G)); ``` wenzelm@44872 ` 259` ``` (ALL A:C. ALL B:C. A ~= B --> A Int B = {}) |] ``` wenzelm@44872 ` 260` ``` ==> finprod G f (Union C) = finprod G (finprod G f) C" ``` nipkow@31719 ` 261` ``` apply (frule finprod_UN_disjoint [of C id f]) ``` haftmann@44106 ` 262` ``` apply (auto simp add: SUP_def) ``` wenzelm@44872 ` 263` ``` done ``` nipkow@31719 ` 264` wenzelm@44872 ` 265` ```lemma (in comm_monoid) finprod_one: ``` wenzelm@44872 ` 266` ``` "finite A \ (\x. x:A \ f x = \) \ finprod G f A = \" ``` wenzelm@44872 ` 267` ``` by (induct set: finite) auto ``` nipkow@31719 ` 268` nipkow@31719 ` 269` nipkow@31719 ` 270` ```(* need better simplification rules for rings *) ``` nipkow@31719 ` 271` ```(* the next one holds more generally for abelian groups *) ``` nipkow@31719 ` 272` wenzelm@60527 ` 273` ```lemma (in cring) sum_zero_eq_neg: "x : carrier R \ y : carrier R \ x \ y = \ \ x = \ y" ``` wenzelm@60527 ` 274` ``` by (metis minus_equality) ``` nipkow@31719 ` 275` wenzelm@60527 ` 276` ```lemma (in domain) square_eq_one: ``` nipkow@31719 ` 277` ``` fixes x ``` wenzelm@60527 ` 278` ``` assumes [simp]: "x : carrier R" ``` wenzelm@60527 ` 279` ``` and "x \ x = \" ``` nipkow@31719 ` 280` ``` shows "x = \ | x = \\" ``` nipkow@31719 ` 281` ```proof - ``` nipkow@31719 ` 282` ``` have "(x \ \) \ (x \ \ \) = x \ x \ \ \" ``` nipkow@31719 ` 283` ``` by (simp add: ring_simprules) ``` wenzelm@60526 ` 284` ``` also from \x \ x = \\ have "\ = \" ``` nipkow@31719 ` 285` ``` by (simp add: ring_simprules) ``` nipkow@31719 ` 286` ``` finally have "(x \ \) \ (x \ \ \) = \" . ``` wenzelm@44872 ` 287` ``` then have "(x \ \) = \ | (x \ \ \) = \" ``` nipkow@31719 ` 288` ``` by (intro integral, auto) ``` wenzelm@44872 ` 289` ``` then show ?thesis ``` nipkow@31719 ` 290` ``` apply auto ``` nipkow@31719 ` 291` ``` apply (erule notE) ``` nipkow@31719 ` 292` ``` apply (rule sum_zero_eq_neg) ``` nipkow@31719 ` 293` ``` apply auto ``` nipkow@31719 ` 294` ``` apply (subgoal_tac "x = \ (\ \)") ``` wenzelm@44872 ` 295` ``` apply (simp add: ring_simprules) ``` nipkow@31719 ` 296` ``` apply (rule sum_zero_eq_neg) ``` nipkow@31719 ` 297` ``` apply auto ``` nipkow@31719 ` 298` ``` done ``` nipkow@31719 ` 299` ```qed ``` nipkow@31719 ` 300` wenzelm@60527 ` 301` ```lemma (in Ring.domain) inv_eq_self: "x : Units R \ x = inv x \ x = \ \ x = \\" ``` wenzelm@60527 ` 302` ``` by (metis Units_closed Units_l_inv square_eq_one) ``` nipkow@31719 ` 303` nipkow@31719 ` 304` wenzelm@60527 ` 305` ```text \ ``` nipkow@31719 ` 306` ``` The following translates theorems about groups to the facts about ``` nipkow@31719 ` 307` ``` the units of a ring. (The list should be expanded as more things are ``` nipkow@31719 ` 308` ``` needed.) ``` wenzelm@60527 ` 309` ```\ ``` nipkow@31719 ` 310` wenzelm@60527 ` 311` ```lemma (in ring) finite_ring_finite_units [intro]: "finite (carrier R) \ finite (Units R)" ``` wenzelm@44872 ` 312` ``` by (rule finite_subset) auto ``` nipkow@31719 ` 313` wenzelm@44872 ` 314` ```lemma (in monoid) units_of_pow: ``` wenzelm@60527 ` 315` ``` fixes n :: nat ``` wenzelm@60527 ` 316` ``` shows "x \ Units G \ x (^)\<^bsub>units_of G\<^esub> n = x (^)\<^bsub>G\<^esub> n" ``` nipkow@31719 ` 317` ``` apply (induct n) ``` wenzelm@44872 ` 318` ``` apply (auto simp add: units_group group.is_monoid ``` wenzelm@41541 ` 319` ``` monoid.nat_pow_0 monoid.nat_pow_Suc units_of_one units_of_mult) ``` wenzelm@41541 ` 320` ``` done ``` nipkow@31719 ` 321` nipkow@31719 ` 322` ```lemma (in cring) units_power_order_eq_one: "finite (Units R) \ a : Units R ``` nipkow@31719 ` 323` ``` \ a (^) card(Units R) = \" ``` nipkow@31719 ` 324` ``` apply (subst units_of_carrier [symmetric]) ``` nipkow@31719 ` 325` ``` apply (subst units_of_one [symmetric]) ``` nipkow@31719 ` 326` ``` apply (subst units_of_pow [symmetric]) ``` nipkow@31719 ` 327` ``` apply assumption ``` nipkow@31719 ` 328` ``` apply (rule comm_group.power_order_eq_one) ``` nipkow@31719 ` 329` ``` apply (rule units_comm_group) ``` nipkow@31719 ` 330` ``` apply (unfold units_of_def, auto) ``` wenzelm@41541 ` 331` ``` done ``` nipkow@31719 ` 332` nipkow@31719 ` 333` ```end ```