src/HOL/Number_Theory/MiscAlgebra.thy
changeset 60527 eb431a5651fe
parent 60526 fad653acf58f
child 60773 d09c66a0ea10
     1.1 --- a/src/HOL/Number_Theory/MiscAlgebra.thy	Fri Jun 19 21:41:33 2015 +0200
     1.2 +++ b/src/HOL/Number_Theory/MiscAlgebra.thy	Fri Jun 19 23:40:46 2015 +0200
     1.3 @@ -1,8 +1,8 @@
     1.4  (*  Title:      HOL/Number_Theory/MiscAlgebra.thy
     1.5      Author:     Jeremy Avigad
     1.6 +*)
     1.7  
     1.8 -These are things that can be added to the Algebra library.
     1.9 -*)
    1.10 +section \<open>Things that can be added to the Algebra library\<close>
    1.11  
    1.12  theory MiscAlgebra
    1.13  imports
    1.14 @@ -10,26 +10,25 @@
    1.15    "~~/src/HOL/Algebra/FiniteProduct"
    1.16  begin
    1.17  
    1.18 -(* finiteness stuff *)
    1.19 +subsection \<open>Finiteness stuff\<close>
    1.20  
    1.21  lemma bounded_set1_int [intro]: "finite {(x::int). a < x & x < b & P x}"
    1.22    apply (subgoal_tac "{x. a < x & x < b & P x} <= {a<..<b}")
    1.23    apply (erule finite_subset)
    1.24    apply auto
    1.25 -done
    1.26 +  done
    1.27  
    1.28  
    1.29 -(* The rest is for the algebra libraries *)
    1.30 +subsection \<open>The rest is for the algebra libraries\<close>
    1.31  
    1.32 -(* These go in Group.thy. *)
    1.33 +subsubsection \<open>These go in Group.thy\<close>
    1.34  
    1.35 -(*
    1.36 +text \<open>
    1.37    Show that the units in any monoid give rise to a group.
    1.38  
    1.39    The file Residues.thy provides some infrastructure to use
    1.40    facts about the unit group within the ring locale.
    1.41 -*)
    1.42 -
    1.43 +\<close>
    1.44  
    1.45  definition units_of :: "('a, 'b) monoid_scheme => 'a monoid" where
    1.46    "units_of G == (| carrier = Units G,
    1.47 @@ -83,8 +82,7 @@
    1.48  lemma units_of_one: "one(units_of G) = one G"
    1.49    unfolding units_of_def by auto
    1.50  
    1.51 -lemma (in monoid) units_of_inv: "x : Units G ==>
    1.52 -    m_inv (units_of G) x = m_inv G x"
    1.53 +lemma (in monoid) units_of_inv: "x : Units G ==> m_inv (units_of G) x = m_inv G x"
    1.54    apply (rule sym)
    1.55    apply (subst m_inv_def)
    1.56    apply (rule the1_equality)
    1.57 @@ -103,14 +101,12 @@
    1.58    apply (subst units_of_mult [symmetric])
    1.59    apply (subst units_of_one [symmetric])
    1.60    apply (erule group.l_inv, assumption)
    1.61 -done
    1.62 +  done
    1.63  
    1.64 -lemma (in group) inj_on_const_mult: "a: (carrier G) ==>
    1.65 -    inj_on (%x. a \<otimes> x) (carrier G)"
    1.66 +lemma (in group) inj_on_const_mult: "a: (carrier G) ==> inj_on (%x. a \<otimes> x) (carrier G)"
    1.67    unfolding inj_on_def by auto
    1.68  
    1.69 -lemma (in group) surj_const_mult: "a : (carrier G) ==>
    1.70 -    (%x. a \<otimes> x) ` (carrier G) = (carrier G)"
    1.71 +lemma (in group) surj_const_mult: "a : (carrier G) ==> (%x. a \<otimes> x) ` (carrier G) = (carrier G)"
    1.72    apply (auto simp add: image_def)
    1.73    apply (rule_tac x = "(m_inv G a) \<otimes> x" in bexI)
    1.74    apply auto
    1.75 @@ -120,8 +116,8 @@
    1.76    apply auto
    1.77    done
    1.78  
    1.79 -lemma (in group) l_cancel_one [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
    1.80 -    (x \<otimes> a = x) = (a = one G)"
    1.81 +lemma (in group) l_cancel_one [simp]:
    1.82 +    "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow> (x \<otimes> a = x) = (a = one G)"
    1.83    apply auto
    1.84    apply (subst l_cancel [symmetric])
    1.85    prefer 4
    1.86 @@ -139,7 +135,6 @@
    1.87    done
    1.88  
    1.89  (* Is there a better way to do this? *)
    1.90 -
    1.91  lemma (in group) l_cancel_one' [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
    1.92      (x = x \<otimes> a) = (a = one G)"
    1.93    apply (subst eq_commute)
    1.94 @@ -173,10 +168,9 @@
    1.95  qed
    1.96  
    1.97  
    1.98 -(* Miscellaneous *)
    1.99 +subsubsection \<open>Miscellaneous\<close>
   1.100  
   1.101 -lemma (in cring) field_intro2: "\<zero>\<^bsub>R\<^esub> ~= \<one>\<^bsub>R\<^esub> \<Longrightarrow> ALL x : carrier R - {\<zero>\<^bsub>R\<^esub>}.
   1.102 -    x : Units R \<Longrightarrow> field R"
   1.103 +lemma (in cring) field_intro2: "\<zero>\<^bsub>R\<^esub> ~= \<one>\<^bsub>R\<^esub> \<Longrightarrow> \<forall>x \<in> carrier R - {\<zero>\<^bsub>R\<^esub>}. x \<in> Units R \<Longrightarrow> field R"
   1.104    apply (unfold_locales)
   1.105    apply (insert cring_axioms, auto)
   1.106    apply (rule trans)
   1.107 @@ -239,10 +233,10 @@
   1.108    done
   1.109  
   1.110  lemma (in monoid) inv_eq_one_eq: "x : Units G \<Longrightarrow> (inv x = \<one>) = (x = \<one>)"
   1.111 -by (metis Units_inv_inv inv_one)
   1.112 +  by (metis Units_inv_inv inv_one)
   1.113  
   1.114  
   1.115 -(* This goes in FiniteProduct *)
   1.116 +subsubsection \<open>This goes in FiniteProduct\<close>
   1.117  
   1.118  lemma (in comm_monoid) finprod_UN_disjoint:
   1.119    "finite I \<Longrightarrow> (ALL i:I. finite (A i)) \<longrightarrow> (ALL i:I. ALL j:I. i ~= j \<longrightarrow>
   1.120 @@ -276,17 +270,13 @@
   1.121  (* need better simplification rules for rings *)
   1.122  (* the next one holds more generally for abelian groups *)
   1.123  
   1.124 -lemma (in cring) sum_zero_eq_neg:
   1.125 -    "x : carrier R \<Longrightarrow> y : carrier R \<Longrightarrow> x \<oplus> y = \<zero> \<Longrightarrow> x = \<ominus> y"
   1.126 -by (metis minus_equality)
   1.127 +lemma (in cring) sum_zero_eq_neg: "x : carrier R \<Longrightarrow> y : carrier R \<Longrightarrow> x \<oplus> y = \<zero> \<Longrightarrow> x = \<ominus> y"
   1.128 +  by (metis minus_equality)
   1.129  
   1.130 -(* there's a name conflict -- maybe "domain" should be
   1.131 -   "integral_domain" *)
   1.132 -
   1.133 -lemma (in Ring.domain) square_eq_one:
   1.134 +lemma (in domain) square_eq_one:
   1.135    fixes x
   1.136 -  assumes [simp]: "x : carrier R" and
   1.137 -    "x \<otimes> x = \<one>"
   1.138 +  assumes [simp]: "x : carrier R"
   1.139 +    and "x \<otimes> x = \<one>"
   1.140    shows "x = \<one> | x = \<ominus>\<one>"
   1.141  proof -
   1.142    have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = x \<otimes> x \<oplus> \<ominus> \<one>"
   1.143 @@ -308,23 +298,22 @@
   1.144      done
   1.145  qed
   1.146  
   1.147 -lemma (in Ring.domain) inv_eq_self: "x : Units R \<Longrightarrow>
   1.148 -    x = inv x \<Longrightarrow> x = \<one> | x = \<ominus> \<one>"
   1.149 -by (metis Units_closed Units_l_inv square_eq_one)
   1.150 +lemma (in Ring.domain) inv_eq_self: "x : Units R \<Longrightarrow> x = inv x \<Longrightarrow> x = \<one> \<or> x = \<ominus>\<one>"
   1.151 +  by (metis Units_closed Units_l_inv square_eq_one)
   1.152  
   1.153  
   1.154 -(*
   1.155 +text \<open>
   1.156    The following translates theorems about groups to the facts about
   1.157    the units of a ring. (The list should be expanded as more things are
   1.158    needed.)
   1.159 -*)
   1.160 +\<close>
   1.161  
   1.162 -lemma (in ring) finite_ring_finite_units [intro]:
   1.163 -    "finite (carrier R) \<Longrightarrow> finite (Units R)"
   1.164 +lemma (in ring) finite_ring_finite_units [intro]: "finite (carrier R) \<Longrightarrow> finite (Units R)"
   1.165    by (rule finite_subset) auto
   1.166  
   1.167  lemma (in monoid) units_of_pow:
   1.168 -    "x : Units G \<Longrightarrow> x (^)\<^bsub>units_of G\<^esub> (n::nat) = x (^)\<^bsub>G\<^esub> n"
   1.169 +  fixes n :: nat
   1.170 +  shows "x \<in> Units G \<Longrightarrow> x (^)\<^bsub>units_of G\<^esub> n = x (^)\<^bsub>G\<^esub> n"
   1.171    apply (induct n)
   1.172    apply (auto simp add: units_group group.is_monoid
   1.173      monoid.nat_pow_0 monoid.nat_pow_Suc units_of_one units_of_mult)