Greatly extended CRing. Added Module.
authorballarin
Wed Apr 30 10:01:35 2003 +0200 (2003-04-30)
changeset 13936d3671b878828
parent 13935 4822d9597d1e
child 13937 e9d57517c9b1
Greatly extended CRing. Added Module.
src/HOL/Algebra/CRing.thy
src/HOL/Algebra/Coset.thy
src/HOL/Algebra/FiniteProduct.thy
src/HOL/Algebra/Group.thy
src/HOL/Algebra/Module.thy
src/HOL/Algebra/ROOT.ML
src/HOL/Algebra/Summation.thy
src/HOL/Algebra/poly/PolyHomo.thy
src/HOL/Algebra/poly/UnivPoly.ML
src/HOL/Algebra/poly/UnivPoly.thy
src/HOL/Algebra/poly/UnivPoly2.ML
src/HOL/Algebra/poly/UnivPoly2.thy
src/HOL/Algebra/ringsimp.ML
     1.1 --- a/src/HOL/Algebra/CRing.thy	Tue Apr 29 12:36:49 2003 +0200
     1.2 +++ b/src/HOL/Algebra/CRing.thy	Wed Apr 30 10:01:35 2003 +0200
     1.3 @@ -5,41 +5,294 @@
     1.4    Copyright: Clemens Ballarin
     1.5  *)
     1.6  
     1.7 -theory CRing = Summation
     1.8 +theory CRing = FiniteProduct
     1.9  files ("ringsimp.ML"):
    1.10  
    1.11 +section {* Abelian Groups *}
    1.12 +
    1.13 +record 'a ring = "'a monoid" +
    1.14 +  zero :: 'a ("\<zero>\<index>")
    1.15 +  add :: "['a, 'a] => 'a" (infixl "\<oplus>\<index>" 65)
    1.16 +
    1.17 +text {* Derived operations. *}
    1.18 +
    1.19 +constdefs
    1.20 +  a_inv :: "[('a, 'm) ring_scheme, 'a ] => 'a" ("\<ominus>\<index> _" [81] 80)
    1.21 +  "a_inv R == m_inv (| carrier = carrier R, mult = add R, one = zero R |)"
    1.22 +
    1.23 +  minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" (infixl "\<ominus>\<index>" 65)
    1.24 +  "[| x \<in> carrier R; y \<in> carrier R |] ==> minus R x y == add R x (a_inv R y)"
    1.25 +
    1.26 +locale abelian_monoid = struct G +
    1.27 +  assumes a_comm_monoid: "comm_monoid (| carrier = carrier G,
    1.28 +      mult = add G, one = zero G |)"
    1.29 +
    1.30 +text {*
    1.31 +  The following definition is redundant but simple to use.
    1.32 +*}
    1.33 +
    1.34 +locale abelian_group = abelian_monoid +
    1.35 +  assumes a_comm_group: "comm_group (| carrier = carrier G,
    1.36 +      mult = add G, one = zero G |)"
    1.37 +
    1.38 +subsection {* Basic Properties *}
    1.39 +
    1.40 +lemma abelian_monoidI:
    1.41 +  assumes a_closed:
    1.42 +      "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==> add R x y \<in> carrier R"
    1.43 +    and zero_closed: "zero R \<in> carrier R"
    1.44 +    and a_assoc:
    1.45 +      "!!x y z. [| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |] ==>
    1.46 +      add R (add R x y) z = add R x (add R y z)"
    1.47 +    and l_zero: "!!x. x \<in> carrier R ==> add R (zero R) x = x"
    1.48 +    and a_comm:
    1.49 +      "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==> add R x y = add R y x"
    1.50 +  shows "abelian_monoid R"
    1.51 +  by (auto intro!: abelian_monoid.intro comm_monoidI intro: prems)
    1.52 +
    1.53 +lemma abelian_groupI:
    1.54 +  assumes a_closed:
    1.55 +      "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==> add R x y \<in> carrier R"
    1.56 +    and zero_closed: "zero R \<in> carrier R"
    1.57 +    and a_assoc:
    1.58 +      "!!x y z. [| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |] ==>
    1.59 +      add R (add R x y) z = add R x (add R y z)"
    1.60 +    and a_comm:
    1.61 +      "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==> add R x y = add R y x"
    1.62 +    and l_zero: "!!x. x \<in> carrier R ==> add R (zero R) x = x"
    1.63 +    and l_inv_ex: "!!x. x \<in> carrier R ==> EX y : carrier R. add R y x = zero R"
    1.64 +  shows "abelian_group R"
    1.65 +  by (auto intro!: abelian_group.intro abelian_monoidI
    1.66 +      abelian_group_axioms.intro comm_monoidI comm_groupI
    1.67 +    intro: prems)
    1.68 +
    1.69 +(* TODO: The following thms are probably unnecessary. *)
    1.70 +
    1.71 +lemma (in abelian_monoid) a_magma:
    1.72 +  "magma (| carrier = carrier G, mult = add G, one = zero G |)"
    1.73 +  by (rule comm_monoid.axioms) (rule a_comm_monoid)
    1.74 +
    1.75 +lemma (in abelian_monoid) a_semigroup:
    1.76 +  "semigroup (| carrier = carrier G, mult = add G, one = zero G |)"
    1.77 +  by (unfold semigroup_def) (fast intro: comm_monoid.axioms a_comm_monoid)
    1.78 +
    1.79 +lemma (in abelian_monoid) a_monoid:
    1.80 +  "monoid (| carrier = carrier G, mult = add G, one = zero G |)"
    1.81 +  by (unfold monoid_def) (fast intro: a_comm_monoid comm_monoid.axioms)
    1.82 +
    1.83 +lemma (in abelian_group) a_group:
    1.84 +  "group (| carrier = carrier G, mult = add G, one = zero G |)"
    1.85 +  by (unfold group_def semigroup_def)
    1.86 +    (fast intro: comm_group.axioms a_comm_group)
    1.87 +
    1.88 +lemma (in abelian_monoid) a_comm_semigroup:
    1.89 +  "comm_semigroup (| carrier = carrier G, mult = add G, one = zero G |)"
    1.90 +  by (unfold comm_semigroup_def semigroup_def)
    1.91 +    (fast intro: comm_monoid.axioms a_comm_monoid)
    1.92 +
    1.93 +lemmas monoid_record_simps = semigroup.simps monoid.simps
    1.94 +
    1.95 +lemma (in abelian_monoid) a_closed [intro, simp]:
    1.96 +  "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<oplus> y \<in> carrier G"
    1.97 +  by (rule magma.m_closed [OF a_magma, simplified monoid_record_simps]) 
    1.98 +
    1.99 +lemma (in abelian_monoid) zero_closed [intro, simp]:
   1.100 +  "\<zero> \<in> carrier G"
   1.101 +  by (rule monoid.one_closed [OF a_monoid, simplified monoid_record_simps])
   1.102 +
   1.103 +lemma (in abelian_group) a_inv_closed [intro, simp]:
   1.104 +  "x \<in> carrier G ==> \<ominus> x \<in> carrier G"
   1.105 +  by (simp add: a_inv_def
   1.106 +    group.inv_closed [OF a_group, simplified monoid_record_simps])
   1.107 +
   1.108 +lemma (in abelian_group) minus_closed [intro, simp]:
   1.109 +  "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<ominus> y \<in> carrier G"
   1.110 +  by (simp add: minus_def)
   1.111 +
   1.112 +lemma (in abelian_group) a_l_cancel [simp]:
   1.113 +  "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
   1.114 +   (x \<oplus> y = x \<oplus> z) = (y = z)"
   1.115 +  by (rule group.l_cancel [OF a_group, simplified monoid_record_simps])
   1.116 +
   1.117 +lemma (in abelian_group) a_r_cancel [simp]:
   1.118 +  "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
   1.119 +   (y \<oplus> x = z \<oplus> x) = (y = z)"
   1.120 +  by (rule group.r_cancel [OF a_group, simplified monoid_record_simps])
   1.121 +
   1.122 +lemma (in abelian_monoid) a_assoc:
   1.123 +  "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
   1.124 +  (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
   1.125 +  by (rule semigroup.m_assoc [OF a_semigroup, simplified monoid_record_simps])
   1.126 +
   1.127 +lemma (in abelian_monoid) l_zero [simp]:
   1.128 +  "x \<in> carrier G ==> \<zero> \<oplus> x = x"
   1.129 +  by (rule monoid.l_one [OF a_monoid, simplified monoid_record_simps])
   1.130 +
   1.131 +lemma (in abelian_group) l_neg:
   1.132 +  "x \<in> carrier G ==> \<ominus> x \<oplus> x = \<zero>"
   1.133 +  by (simp add: a_inv_def
   1.134 +    group.l_inv [OF a_group, simplified monoid_record_simps])
   1.135 +
   1.136 +lemma (in abelian_monoid) a_comm:
   1.137 +  "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<oplus> y = y \<oplus> x"
   1.138 +  by (rule comm_semigroup.m_comm [OF a_comm_semigroup,
   1.139 +    simplified monoid_record_simps])
   1.140 +
   1.141 +lemma (in abelian_monoid) a_lcomm:
   1.142 +  "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
   1.143 +   x \<oplus> (y \<oplus> z) = y \<oplus> (x \<oplus> z)"
   1.144 +  by (rule comm_semigroup.m_lcomm [OF a_comm_semigroup,
   1.145 +    simplified monoid_record_simps])
   1.146 +
   1.147 +lemma (in abelian_monoid) r_zero [simp]:
   1.148 +  "x \<in> carrier G ==> x \<oplus> \<zero> = x"
   1.149 +  using monoid.r_one [OF a_monoid]
   1.150 +  by simp
   1.151 +
   1.152 +lemma (in abelian_group) r_neg:
   1.153 +  "x \<in> carrier G ==> x \<oplus> (\<ominus> x) = \<zero>"
   1.154 +  using group.r_inv [OF a_group]
   1.155 +  by (simp add: a_inv_def)
   1.156 +
   1.157 +lemma (in abelian_group) minus_zero [simp]:
   1.158 +  "\<ominus> \<zero> = \<zero>"
   1.159 +  by (simp add: a_inv_def
   1.160 +    group.inv_one [OF a_group, simplified monoid_record_simps])
   1.161 +
   1.162 +lemma (in abelian_group) minus_minus [simp]:
   1.163 +  "x \<in> carrier G ==> \<ominus> (\<ominus> x) = x"
   1.164 +  using group.inv_inv [OF a_group, simplified monoid_record_simps]
   1.165 +  by (simp add: a_inv_def)
   1.166 +
   1.167 +lemma (in abelian_group) a_inv_inj:
   1.168 +  "inj_on (a_inv G) (carrier G)"
   1.169 +  using group.inv_inj [OF a_group, simplified monoid_record_simps]
   1.170 +  by (simp add: a_inv_def)
   1.171 +
   1.172 +lemma (in abelian_group) minus_add:
   1.173 +  "[| x \<in> carrier G; y \<in> carrier G |] ==> \<ominus> (x \<oplus> y) = \<ominus> x \<oplus> \<ominus> y"
   1.174 +  using comm_group.inv_mult [OF a_comm_group]
   1.175 +  by (simp add: a_inv_def)
   1.176 +
   1.177 +lemmas (in abelian_monoid) a_ac = a_assoc a_comm a_lcomm
   1.178 +
   1.179 +subsection {* Sums over Finite Sets *}
   1.180 +
   1.181 +text {*
   1.182 +  This definition makes it easy to lift lemmas from @{term finprod}.
   1.183 +*}
   1.184 +
   1.185 +constdefs
   1.186 +  finsum :: "[('b, 'm) ring_scheme, 'a => 'b, 'a set] => 'b"
   1.187 +  "finsum G f A == finprod (| carrier = carrier G,
   1.188 +     mult = add G, one = zero G |) f A"
   1.189 +
   1.190 +(*
   1.191 +  lemmas (in abelian_monoid) finsum_empty [simp] =
   1.192 +    comm_monoid.finprod_empty [OF a_comm_monoid, simplified]
   1.193 +  is dangeous, because attributes (like simplified) are applied upon opening
   1.194 +  the locale, simplified refers to the simpset at that time!!!
   1.195 +
   1.196 +  lemmas (in abelian_monoid) finsum_empty [simp] =
   1.197 +    abelian_monoid.finprod_empty [OF a_abelian_monoid, folded finsum_def,
   1.198 +      simplified monoid_record_simps]
   1.199 +makes the locale slow, because proofs are repeated for every
   1.200 +"lemma (in abelian_monoid)" command.
   1.201 +When lemma is used time in UnivPoly.thy from beginning to UP_cring goes down
   1.202 +from 110 secs to 60 secs.
   1.203 +*)
   1.204 +
   1.205 +lemma (in abelian_monoid) finsum_empty [simp]:
   1.206 +  "finsum G f {} = \<zero>"
   1.207 +  by (rule comm_monoid.finprod_empty [OF a_comm_monoid,
   1.208 +    folded finsum_def, simplified monoid_record_simps])
   1.209 +
   1.210 +lemma (in abelian_monoid) finsum_insert [simp]:
   1.211 +  "[| finite F; a \<notin> F; f \<in> F -> carrier G; f a \<in> carrier G |]
   1.212 +  ==> finsum G f (insert a F) = f a \<oplus> finsum G f F"
   1.213 +  by (rule comm_monoid.finprod_insert [OF a_comm_monoid,
   1.214 +    folded finsum_def, simplified monoid_record_simps])
   1.215 +
   1.216 +lemma (in abelian_monoid) finsum_zero [simp]:
   1.217 +  "finite A ==> finsum G (%i. \<zero>) A = \<zero>"
   1.218 +  by (rule comm_monoid.finprod_one [OF a_comm_monoid, folded finsum_def,
   1.219 +    simplified monoid_record_simps])
   1.220 +
   1.221 +lemma (in abelian_monoid) finsum_closed [simp]:
   1.222 +  fixes A
   1.223 +  assumes fin: "finite A" and f: "f \<in> A -> carrier G" 
   1.224 +  shows "finsum G f A \<in> carrier G"
   1.225 +  by (rule comm_monoid.finprod_closed [OF a_comm_monoid,
   1.226 +    folded finsum_def, simplified monoid_record_simps])
   1.227 +
   1.228 +lemma (in abelian_monoid) finsum_Un_Int:
   1.229 +  "[| finite A; finite B; g \<in> A -> carrier G; g \<in> B -> carrier G |] ==>
   1.230 +     finsum G g (A Un B) \<oplus> finsum G g (A Int B) =
   1.231 +     finsum G g A \<oplus> finsum G g B"
   1.232 +  by (rule comm_monoid.finprod_Un_Int [OF a_comm_monoid,
   1.233 +    folded finsum_def, simplified monoid_record_simps])
   1.234 +
   1.235 +lemma (in abelian_monoid) finsum_Un_disjoint:
   1.236 +  "[| finite A; finite B; A Int B = {};
   1.237 +      g \<in> A -> carrier G; g \<in> B -> carrier G |]
   1.238 +   ==> finsum G g (A Un B) = finsum G g A \<oplus> finsum G g B"
   1.239 +  by (rule comm_monoid.finprod_Un_disjoint [OF a_comm_monoid,
   1.240 +    folded finsum_def, simplified monoid_record_simps])
   1.241 +
   1.242 +lemma (in abelian_monoid) finsum_addf:
   1.243 +  "[| finite A; f \<in> A -> carrier G; g \<in> A -> carrier G |] ==>
   1.244 +   finsum G (%x. f x \<oplus> g x) A = (finsum G f A \<oplus> finsum G g A)"
   1.245 +  by (rule comm_monoid.finprod_multf [OF a_comm_monoid,
   1.246 +    folded finsum_def, simplified monoid_record_simps])
   1.247 +
   1.248 +lemma (in abelian_monoid) finsum_cong':
   1.249 +  "[| A = B; g : B -> carrier G;
   1.250 +      !!i. i : B ==> f i = g i |] ==> finsum G f A = finsum G g B"
   1.251 +  by (rule comm_monoid.finprod_cong' [OF a_comm_monoid,
   1.252 +    folded finsum_def, simplified monoid_record_simps]) auto
   1.253 +
   1.254 +lemma (in abelian_monoid) finsum_0 [simp]:
   1.255 +  "f : {0::nat} -> carrier G ==> finsum G f {..0} = f 0"
   1.256 +  by (rule comm_monoid.finprod_0 [OF a_comm_monoid, folded finsum_def,
   1.257 +    simplified monoid_record_simps])
   1.258 +
   1.259 +lemma (in abelian_monoid) finsum_Suc [simp]:
   1.260 +  "f : {..Suc n} -> carrier G ==>
   1.261 +   finsum G f {..Suc n} = (f (Suc n) \<oplus> finsum G f {..n})"
   1.262 +  by (rule comm_monoid.finprod_Suc [OF a_comm_monoid, folded finsum_def,
   1.263 +    simplified monoid_record_simps])
   1.264 +
   1.265 +lemma (in abelian_monoid) finsum_Suc2:
   1.266 +  "f : {..Suc n} -> carrier G ==>
   1.267 +   finsum G f {..Suc n} = (finsum G (%i. f (Suc i)) {..n} \<oplus> f 0)"
   1.268 +  by (rule comm_monoid.finprod_Suc2 [OF a_comm_monoid, folded finsum_def,
   1.269 +    simplified monoid_record_simps])
   1.270 +
   1.271 +lemma (in abelian_monoid) finsum_add [simp]:
   1.272 +  "[| f : {..n} -> carrier G; g : {..n} -> carrier G |] ==>
   1.273 +     finsum G (%i. f i \<oplus> g i) {..n::nat} =
   1.274 +     finsum G f {..n} \<oplus> finsum G g {..n}"
   1.275 +  by (rule comm_monoid.finprod_mult [OF a_comm_monoid, folded finsum_def,
   1.276 +    simplified monoid_record_simps])
   1.277 +
   1.278 +lemma (in abelian_monoid) finsum_cong:
   1.279 +  "[| A = B; !!i. i : B ==> f i = g i;
   1.280 +      g : B -> carrier G = True |] ==> finsum G f A = finsum G g B"
   1.281 +  by (rule comm_monoid.finprod_cong [OF a_comm_monoid, folded finsum_def,
   1.282 +    simplified monoid_record_simps]) auto
   1.283 +
   1.284 +text {*Usually, if this rule causes a failed congruence proof error,
   1.285 +   the reason is that the premise @{text "g \<in> B -> carrier G"} cannot be shown.
   1.286 +   Adding @{thm [source] Pi_def} to the simpset is often useful. *}
   1.287 +
   1.288  section {* The Algebraic Hierarchy of Rings *}
   1.289  
   1.290  subsection {* Basic Definitions *}
   1.291  
   1.292 -record 'a ring = "'a group" +
   1.293 -  zero :: 'a ("\<zero>\<index>")
   1.294 -  add :: "['a, 'a] => 'a" (infixl "\<oplus>\<index>" 65)
   1.295 -  a_inv :: "'a => 'a" ("\<ominus>\<index> _" [81] 80)
   1.296 -
   1.297 -locale cring = abelian_monoid R +
   1.298 -  assumes a_abelian_group: "abelian_group (| carrier = carrier R,
   1.299 -      mult = add R, one = zero R, m_inv = a_inv R |)"
   1.300 -    and m_inv_def: "[| EX y. y \<in> carrier R & x \<otimes> y = \<one>; x \<in> carrier R |]
   1.301 -      ==> inv x = (THE y. y \<in> carrier R & x \<otimes> y = \<one>)"
   1.302 -    and l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
   1.303 +locale cring = abelian_group R + comm_monoid R +
   1.304 +  assumes l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
   1.305        ==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
   1.306  
   1.307 -text {* Derived operation. *}
   1.308 -
   1.309 -constdefs
   1.310 -  minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" (infixl "\<ominus>\<index>" 65)
   1.311 -  "[| x \<in> carrier R; y \<in> carrier R |] ==> minus R x y == add R x (a_inv R y)"
   1.312 -
   1.313 -(*
   1.314 -  -- {* Definition of derived operations *}
   1.315 -
   1.316 -  minus_def:    "a - b = a + (-b)"
   1.317 -  inverse_def:  "inverse a = (if a dvd 1 then THE x. a*x = 1 else 0)"
   1.318 -  divide_def:   "a / b = a * inverse b"
   1.319 -  power_def:    "a ^ n = nat_rec 1 (%u b. b * a) n"
   1.320 -*)
   1.321 -
   1.322  locale "domain" = cring +
   1.323    assumes one_not_zero [simp]: "\<one> ~= \<zero>"
   1.324      and integral: "[| a \<otimes> b = \<zero>; a \<in> carrier R; b \<in> carrier R |] ==>
   1.325 @@ -47,117 +300,41 @@
   1.326  
   1.327  subsection {* Basic Facts of Rings *}
   1.328  
   1.329 -lemma (in cring) a_magma [simp, intro]:
   1.330 -  "magma (| carrier = carrier R,
   1.331 -     mult = add R, one = zero R, m_inv = a_inv R |)"
   1.332 -  using a_abelian_group by (simp only: abelian_group_def)
   1.333 -
   1.334 -lemma (in cring) a_l_one [simp, intro]:
   1.335 -  "l_one (| carrier = carrier R,
   1.336 -     mult = add R, one = zero R, m_inv = a_inv R |)"
   1.337 -  using a_abelian_group by (simp only: abelian_group_def)
   1.338 -
   1.339 -lemma (in cring) a_abelian_group_parts [simp, intro]:
   1.340 -  "semigroup_axioms (| carrier = carrier R,
   1.341 -     mult = add R, one = zero R, m_inv = a_inv R |)"
   1.342 -  "group_axioms (| carrier = carrier R,
   1.343 -     mult = add R, one = zero R, m_inv = a_inv R |)"
   1.344 -  "abelian_semigroup_axioms (| carrier = carrier R,
   1.345 -     mult = add R, one = zero R, m_inv = a_inv R |)"
   1.346 -  using a_abelian_group by (simp_all only: abelian_group_def)
   1.347 -
   1.348 -lemma (in cring) a_semigroup:
   1.349 -  "semigroup (| carrier = carrier R,
   1.350 -     mult = add R, one = zero R, m_inv = a_inv R |)"
   1.351 -  by (simp add: semigroup_def)
   1.352 -
   1.353 -lemma (in cring) a_group:
   1.354 -  "group (| carrier = carrier R,
   1.355 -     mult = add R, one = zero R, m_inv = a_inv R |)"
   1.356 -  by (simp add: group_def)
   1.357 -
   1.358 -lemma (in cring) a_abelian_semigroup:
   1.359 -  "abelian_semigroup (| carrier = carrier R,
   1.360 -     mult = add R, one = zero R, m_inv = a_inv R |)"
   1.361 -  by (simp add: abelian_semigroup_def)
   1.362 -
   1.363 -lemmas group_record_simps = semigroup.simps monoid.simps group.simps
   1.364 -
   1.365 -lemmas (in cring) a_closed [intro, simp] =
   1.366 -  magma.m_closed [OF a_magma, simplified group_record_simps]
   1.367 -
   1.368 -lemmas (in cring) zero_closed [intro, simp] = 
   1.369 -  l_one.one_closed [OF a_l_one, simplified group_record_simps]
   1.370 -
   1.371 -lemmas (in cring) a_inv_closed [intro, simp] =
   1.372 -  group.inv_closed [OF a_group, simplified group_record_simps]
   1.373 +lemma cringI:
   1.374 +  assumes abelian_group: "abelian_group R"
   1.375 +    and comm_monoid: "comm_monoid R"
   1.376 +    and l_distr: "!!x y z. [| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
   1.377 +      ==> mult R (add R x y) z = add R (mult R x z) (mult R y z)"
   1.378 +  shows "cring R"
   1.379 +  by (auto intro: cring.intro
   1.380 +    abelian_group.axioms comm_monoid.axioms cring_axioms.intro prems)
   1.381  
   1.382 -lemma (in cring) minus_closed [intro, simp]:
   1.383 -  "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y \<in> carrier R"
   1.384 -  by (simp add: minus_def)
   1.385 -
   1.386 -lemmas (in cring) a_l_cancel [simp] =
   1.387 -  group.l_cancel [OF a_group, simplified group_record_simps]
   1.388 -
   1.389 -lemmas (in cring) a_r_cancel [simp] =
   1.390 -  group.r_cancel [OF a_group, simplified group_record_simps]
   1.391 -
   1.392 -lemmas (in cring) a_assoc =
   1.393 -  semigroup.m_assoc [OF a_semigroup, simplified group_record_simps]
   1.394 -
   1.395 -lemmas (in cring) l_zero [simp] =
   1.396 -  l_one.l_one [OF a_l_one, simplified group_record_simps]
   1.397 -
   1.398 -lemmas (in cring) l_neg =
   1.399 -  group.l_inv [OF a_group, simplified group_record_simps]
   1.400 -
   1.401 -lemmas (in cring) a_comm =
   1.402 -  abelian_semigroup.m_comm [OF a_abelian_semigroup,
   1.403 -  simplified group_record_simps]
   1.404 +lemma (in cring) is_abelian_group:
   1.405 +  "abelian_group R"
   1.406 +  by (auto intro!: abelian_groupI a_assoc a_comm l_neg)
   1.407  
   1.408 -lemmas (in cring) a_lcomm =
   1.409 -  abelian_semigroup.m_lcomm [OF a_abelian_semigroup, simplified group_record_simps]
   1.410 -
   1.411 -lemma (in cring) r_zero [simp]:
   1.412 -  "x \<in> carrier R ==> x \<oplus> \<zero> = x"
   1.413 -  using group.r_one [OF a_group]
   1.414 -  by simp
   1.415 -
   1.416 -lemma (in cring) r_neg:
   1.417 -  "x \<in> carrier R ==> x \<oplus> (\<ominus> x) = \<zero>"
   1.418 -  using group.r_inv [OF a_group]
   1.419 -  by simp
   1.420 -
   1.421 -lemmas (in cring) minus_zero [simp] =
   1.422 -  group.inv_one [OF a_group, simplified group_record_simps]
   1.423 -
   1.424 -lemma (in cring) minus_minus [simp]:
   1.425 -  "x \<in> carrier R ==> \<ominus> (\<ominus> x) = x"
   1.426 -  using group.inv_inv [OF a_group, simplified group_record_simps]
   1.427 -  by simp
   1.428 -
   1.429 -lemma (in cring) minus_add:
   1.430 -  "[| x \<in> carrier R; y \<in> carrier R |] ==> \<ominus> (x \<oplus> y) = \<ominus> x \<oplus> \<ominus> y"
   1.431 -  using abelian_group.inv_mult [OF a_abelian_group]
   1.432 -  by simp
   1.433 -
   1.434 -lemmas (in cring) a_ac = a_assoc a_comm a_lcomm
   1.435 +lemma (in cring) is_comm_monoid:
   1.436 +  "comm_monoid R"
   1.437 +  by (auto intro!: comm_monoidI m_assoc m_comm)
   1.438  
   1.439  subsection {* Normaliser for Commutative Rings *}
   1.440  
   1.441 -lemma (in cring) r_neg2:
   1.442 -  "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<oplus> (\<ominus> x \<oplus> y) = y"
   1.443 +lemma (in abelian_group) r_neg2:
   1.444 +  "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<oplus> (\<ominus> x \<oplus> y) = y"
   1.445  proof -
   1.446 -  assume G: "x \<in> carrier R" "y \<in> carrier R"
   1.447 -  then have "(x \<oplus> \<ominus> x) \<oplus> y = y" by (simp only: r_neg l_zero)
   1.448 -  with G show ?thesis by (simp add: a_ac)
   1.449 +  assume G: "x \<in> carrier G" "y \<in> carrier G"
   1.450 +  then have "(x \<oplus> \<ominus> x) \<oplus> y = y"
   1.451 +    by (simp only: r_neg l_zero)
   1.452 +  with G show ?thesis 
   1.453 +    by (simp add: a_ac)
   1.454  qed
   1.455  
   1.456 -lemma (in cring) r_neg1:
   1.457 -  "[| x \<in> carrier R; y \<in> carrier R |] ==> \<ominus> x \<oplus> (x \<oplus> y) = y"
   1.458 +lemma (in abelian_group) r_neg1:
   1.459 +  "[| x \<in> carrier G; y \<in> carrier G |] ==> \<ominus> x \<oplus> (x \<oplus> y) = y"
   1.460  proof -
   1.461 -  assume G: "x \<in> carrier R" "y \<in> carrier R"
   1.462 -  then have "(\<ominus> x \<oplus> x) \<oplus> y = y" by (simp only: l_neg l_zero)
   1.463 +  assume G: "x \<in> carrier G" "y \<in> carrier G"
   1.464 +  then have "(\<ominus> x \<oplus> x) \<oplus> y = y" 
   1.465 +    by (simp only: l_neg l_zero)
   1.466    with G show ?thesis by (simp add: a_ac)
   1.467  qed
   1.468  
   1.469 @@ -165,10 +342,10 @@
   1.470    "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
   1.471    ==> z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y"
   1.472  proof -
   1.473 -  assume G: "x \<in> carrier R" "y \<in> carrier R" "z \<in> carrier R"
   1.474 +  assume R: "x \<in> carrier R" "y \<in> carrier R" "z \<in> carrier R"
   1.475    then have "z \<otimes> (x \<oplus> y) = (x \<oplus> y) \<otimes> z" by (simp add: m_comm)
   1.476 -  also from G have "... = x \<otimes> z \<oplus> y \<otimes> z" by (simp add: l_distr)
   1.477 -  also from G have "... = z \<otimes> x \<oplus> z \<otimes> y" by (simp add: m_comm)
   1.478 +  also from R have "... = x \<otimes> z \<oplus> y \<otimes> z" by (simp add: l_distr)
   1.479 +  also from R have "... = z \<otimes> x \<oplus> z \<otimes> y" by (simp add: m_comm)
   1.480    finally show ?thesis .
   1.481  qed
   1.482  
   1.483 @@ -191,7 +368,7 @@
   1.484    "x \<in> carrier R ==> x \<otimes> \<zero> = \<zero>"
   1.485  proof -
   1.486    assume R: "x \<in> carrier R"
   1.487 -  then have "x \<otimes> \<zero> = \<zero> \<otimes> x" by (simp add: ac)
   1.488 +  then have "x \<otimes> \<zero> = \<zero> \<otimes> x" by (simp add: m_ac)
   1.489    also from R have "... = \<zero>" by simp
   1.490    finally show ?thesis .
   1.491  qed
   1.492 @@ -211,15 +388,19 @@
   1.493    "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<otimes> \<ominus> y = \<ominus> (x \<otimes> y)"
   1.494  proof -
   1.495    assume R: "x \<in> carrier R" "y \<in> carrier R"
   1.496 -  then have "x \<otimes> \<ominus> y = \<ominus> y \<otimes> x" by (simp add: ac)
   1.497 +  then have "x \<otimes> \<ominus> y = \<ominus> y \<otimes> x" by (simp add: m_ac)
   1.498    also from R have "... = \<ominus> (y \<otimes> x)" by (simp add: l_minus)
   1.499 -  also from R have "... = \<ominus> (x \<otimes> y)" by (simp add: ac)
   1.500 +  also from R have "... = \<ominus> (x \<otimes> y)" by (simp add: m_ac)
   1.501    finally show ?thesis .
   1.502  qed
   1.503  
   1.504 +lemma (in cring) minus_eq:
   1.505 +  "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y = x \<oplus> \<ominus> y"
   1.506 +  by (simp only: minus_def)
   1.507 +
   1.508  lemmas (in cring) cring_simprules =
   1.509    a_closed zero_closed a_inv_closed minus_closed m_closed one_closed
   1.510 -  a_assoc l_zero l_neg a_comm m_assoc l_one l_distr m_comm minus_def
   1.511 +  a_assoc l_zero l_neg a_comm m_assoc l_one l_distr m_comm minus_eq
   1.512    r_zero r_neg r_neg2 r_neg1 minus_add minus_minus minus_zero
   1.513    a_lcomm m_lcomm r_distr l_null r_null l_minus r_minus
   1.514  
   1.515 @@ -227,7 +408,11 @@
   1.516  
   1.517  method_setup algebra =
   1.518    {* Method.ctxt_args cring_normalise *}
   1.519 -  {* computes distributive normal form in commutative rings (locales version) *}
   1.520 +  {* computes distributive normal form in locale context cring *}
   1.521 +
   1.522 +lemma (in cring) nat_pow_zero:
   1.523 +  "(n::nat) ~= 0 ==> \<zero> (^) n = \<zero>"
   1.524 +  by (induct n) simp_all
   1.525  
   1.526  text {* Two examples for use of method algebra *}
   1.527  
   1.528 @@ -244,83 +429,6 @@
   1.529  
   1.530  subsection {* Sums over Finite Sets *}
   1.531  
   1.532 -text {*
   1.533 -  This definition makes it easy to lift lemmas from @{term finprod}.
   1.534 -*}
   1.535 -
   1.536 -constdefs
   1.537 -  finsum :: "[('b, 'm) ring_scheme, 'a => 'b, 'a set] => 'b"
   1.538 -  "finsum R f A == finprod (| carrier = carrier R,
   1.539 -     mult = add R, one = zero R, m_inv = a_inv R |) f A"
   1.540 -
   1.541 -lemma (in cring) a_abelian_monoid:
   1.542 -  "abelian_monoid (| carrier = carrier R,
   1.543 -     mult = add R, one = zero R, m_inv = a_inv R |)"
   1.544 -  by (simp add: abelian_monoid_def)
   1.545 -
   1.546 -(*
   1.547 -  lemmas (in cring) finsum_empty [simp] =
   1.548 -    abelian_monoid.finprod_empty [OF a_abelian_monoid, simplified]
   1.549 -  is dangeous, because attributes (like simplified) are applied upon opening
   1.550 -  the locale, simplified refers to the simpset at that time!!!
   1.551 -*)
   1.552 -
   1.553 -lemmas (in cring) finsum_empty [simp] =
   1.554 -  abelian_monoid.finprod_empty [OF a_abelian_monoid, folded finsum_def,
   1.555 -    simplified group_record_simps]
   1.556 -
   1.557 -lemmas (in cring) finsum_insert [simp] =
   1.558 -  abelian_monoid.finprod_insert [OF a_abelian_monoid, folded finsum_def,
   1.559 -    simplified group_record_simps]
   1.560 -
   1.561 -lemmas (in cring) finsum_zero =
   1.562 -  abelian_monoid.finprod_one [OF a_abelian_monoid, folded finsum_def,
   1.563 -    simplified group_record_simps]
   1.564 -
   1.565 -lemmas (in cring) finsum_closed [simp] =
   1.566 -  abelian_monoid.finprod_closed [OF a_abelian_monoid, folded finsum_def,
   1.567 -    simplified group_record_simps]
   1.568 -
   1.569 -lemmas (in cring) finsum_Un_Int =
   1.570 -  abelian_monoid.finprod_Un_Int [OF a_abelian_monoid, folded finsum_def,
   1.571 -    simplified group_record_simps]
   1.572 -
   1.573 -lemmas (in cring) finsum_Un_disjoint =
   1.574 -  abelian_monoid.finprod_Un_disjoint [OF a_abelian_monoid, folded finsum_def,
   1.575 -    simplified group_record_simps]
   1.576 -
   1.577 -lemmas (in cring) finsum_addf =
   1.578 -  abelian_monoid.finprod_multf [OF a_abelian_monoid, folded finsum_def,
   1.579 -    simplified group_record_simps]
   1.580 -
   1.581 -lemmas (in cring) finsum_cong' =
   1.582 -  abelian_monoid.finprod_cong' [OF a_abelian_monoid, folded finsum_def,
   1.583 -    simplified group_record_simps]
   1.584 -
   1.585 -lemmas (in cring) finsum_0 [simp] =
   1.586 -  abelian_monoid.finprod_0 [OF a_abelian_monoid, folded finsum_def,
   1.587 -    simplified group_record_simps]
   1.588 -
   1.589 -lemmas (in cring) finsum_Suc [simp] =
   1.590 -  abelian_monoid.finprod_Suc [OF a_abelian_monoid, folded finsum_def,
   1.591 -    simplified group_record_simps]
   1.592 -
   1.593 -lemmas (in cring) finsum_Suc2 =
   1.594 -  abelian_monoid.finprod_Suc2 [OF a_abelian_monoid, folded finsum_def,
   1.595 -    simplified group_record_simps]
   1.596 -
   1.597 -lemmas (in cring) finsum_add [simp] =
   1.598 -  abelian_monoid.finprod_mult [OF a_abelian_monoid, folded finsum_def,
   1.599 -    simplified group_record_simps]
   1.600 -
   1.601 -lemmas (in cring) finsum_cong =
   1.602 -  abelian_monoid.finprod_cong [OF a_abelian_monoid, folded finsum_def,
   1.603 -    simplified group_record_simps]
   1.604 -
   1.605 -text {*Usually, if this rule causes a failed congruence proof error,
   1.606 -   the reason is that the premise @{text "g \<in> B -> carrier G"} cannot be shown.
   1.607 -   Adding @{thm [source] Pi_def} to the simpset is often useful. *}
   1.608 -
   1.609  lemma (in cring) finsum_ldistr:
   1.610    "[| finite A; a \<in> carrier R; f \<in> A -> carrier R |] ==>
   1.611     finsum R f A \<otimes> a = finsum R (%i. f i \<otimes> a) A"
   1.612 @@ -380,4 +488,90 @@
   1.613    with R show ?thesis by algebra
   1.614  qed
   1.615  
   1.616 +subsection {* Morphisms *}
   1.617 +
   1.618 +constdefs
   1.619 +  ring_hom :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme] => ('a => 'b) set"
   1.620 +  "ring_hom R S == {h. h \<in> carrier R -> carrier S &
   1.621 +      (ALL x y. x \<in> carrier R & y \<in> carrier R -->
   1.622 +        h (mult R x y) = mult S (h x) (h y) &
   1.623 +        h (add R x y) = add S (h x) (h y)) &
   1.624 +      h (one R) = one S}"
   1.625 +
   1.626 +lemma ring_hom_memI:
   1.627 +  assumes hom_closed: "!!x. x \<in> carrier R ==> h x \<in> carrier S"
   1.628 +    and hom_mult: "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==>
   1.629 +      h (mult R x y) = mult S (h x) (h y)"
   1.630 +    and hom_add: "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==>
   1.631 +      h (add R x y) = add S (h x) (h y)"
   1.632 +    and hom_one: "h (one R) = one S"
   1.633 +  shows "h \<in> ring_hom R S"
   1.634 +  by (auto simp add: ring_hom_def prems Pi_def)
   1.635 +
   1.636 +lemma ring_hom_closed:
   1.637 +  "[| h \<in> ring_hom R S; x \<in> carrier R |] ==> h x \<in> carrier S"
   1.638 +  by (auto simp add: ring_hom_def funcset_mem)
   1.639 +
   1.640 +lemma ring_hom_mult:
   1.641 +  "[| h \<in> ring_hom R S; x \<in> carrier R; y \<in> carrier R |] ==>
   1.642 +  h (mult R x y) = mult S (h x) (h y)"
   1.643 +  by (simp add: ring_hom_def)
   1.644 +
   1.645 +lemma ring_hom_add:
   1.646 +  "[| h \<in> ring_hom R S; x \<in> carrier R; y \<in> carrier R |] ==>
   1.647 +  h (add R x y) = add S (h x) (h y)"
   1.648 +  by (simp add: ring_hom_def)
   1.649 +
   1.650 +lemma ring_hom_one:
   1.651 +  "h \<in> ring_hom R S ==> h (one R) = one S"
   1.652 +  by (simp add: ring_hom_def)
   1.653 +
   1.654 +locale ring_hom_cring = cring R + cring S + var h +
   1.655 +  assumes homh [simp, intro]: "h \<in> ring_hom R S"
   1.656 +  notes hom_closed [simp, intro] = ring_hom_closed [OF homh]
   1.657 +    and hom_mult [simp] = ring_hom_mult [OF homh]
   1.658 +    and hom_add [simp] = ring_hom_add [OF homh]
   1.659 +    and hom_one [simp] = ring_hom_one [OF homh]
   1.660 +
   1.661 +lemma (in ring_hom_cring) hom_zero [simp]:
   1.662 +  "h \<zero> = \<zero>\<^sub>2"
   1.663 +proof -
   1.664 +  have "h \<zero> \<oplus>\<^sub>2 h \<zero> = h \<zero> \<oplus>\<^sub>2 \<zero>\<^sub>2"
   1.665 +    by (simp add: hom_add [symmetric] del: hom_add)
   1.666 +  then show ?thesis by (simp del: S.r_zero)
   1.667 +qed
   1.668 +
   1.669 +lemma (in ring_hom_cring) hom_a_inv [simp]:
   1.670 +  "x \<in> carrier R ==> h (\<ominus> x) = \<ominus>\<^sub>2 h x"
   1.671 +proof -
   1.672 +  assume R: "x \<in> carrier R"
   1.673 +  then have "h x \<oplus>\<^sub>2 h (\<ominus> x) = h x \<oplus>\<^sub>2 (\<ominus>\<^sub>2 h x)"
   1.674 +    by (simp add: hom_add [symmetric] R.r_neg S.r_neg del: hom_add)
   1.675 +  with R show ?thesis by simp
   1.676 +qed
   1.677 +
   1.678 +lemma (in ring_hom_cring) hom_finsum [simp]:
   1.679 +  "[| finite A; f \<in> A -> carrier R |] ==>
   1.680 +  h (finsum R f A) = finsum S (h o f) A"
   1.681 +proof (induct set: Finites)
   1.682 +  case empty then show ?case by simp
   1.683 +next
   1.684 +  case insert then show ?case by (simp add: Pi_def)
   1.685 +qed
   1.686 +
   1.687 +lemma (in ring_hom_cring) hom_finprod:
   1.688 +  "[| finite A; f \<in> A -> carrier R |] ==>
   1.689 +  h (finprod R f A) = finprod S (h o f) A"
   1.690 +proof (induct set: Finites)
   1.691 +  case empty then show ?case by simp
   1.692 +next
   1.693 +  case insert then show ?case by (simp add: Pi_def)
   1.694 +qed
   1.695 +
   1.696 +declare ring_hom_cring.hom_finprod [simp]
   1.697 +
   1.698 +lemma id_ring_hom [simp]:
   1.699 +  "id \<in> ring_hom R R"
   1.700 +  by (auto intro!: ring_hom_memI)
   1.701 +
   1.702  end
     2.1 --- a/src/HOL/Algebra/Coset.thy	Tue Apr 29 12:36:49 2003 +0200
     2.2 +++ b/src/HOL/Algebra/Coset.thy	Wed Apr 30 10:01:35 2003 +0200
     2.3 @@ -10,27 +10,27 @@
     2.4  declare (in group) l_inv [simp]  r_inv [simp] 
     2.5  
     2.6  constdefs
     2.7 -  r_coset    :: "[('a,'b) group_scheme,'a set, 'a] => 'a set"    
     2.8 +  r_coset    :: "[('a,'b) monoid_scheme,'a set, 'a] => 'a set"    
     2.9     "r_coset G H a == (% x. (mult G) x a) ` H"
    2.10  
    2.11 -  l_coset    :: "[('a,'b) group_scheme, 'a, 'a set] => 'a set"
    2.12 +  l_coset    :: "[('a,'b) monoid_scheme, 'a, 'a set] => 'a set"
    2.13     "l_coset G a H == (% x. (mult G) a x) ` H"
    2.14  
    2.15 -  rcosets  :: "[('a,'b) group_scheme,'a set] => ('a set)set"
    2.16 +  rcosets  :: "[('a,'b) monoid_scheme,'a set] => ('a set)set"
    2.17     "rcosets G H == r_coset G H ` (carrier G)"
    2.18  
    2.19 -  set_mult  :: "[('a,'b) group_scheme,'a set,'a set] => 'a set"
    2.20 +  set_mult  :: "[('a,'b) monoid_scheme,'a set,'a set] => 'a set"
    2.21     "set_mult G H K == (%(x,y). (mult G) x y) ` (H \<times> K)"
    2.22  
    2.23 -  set_inv   :: "[('a,'b) group_scheme,'a set] => 'a set"
    2.24 +  set_inv   :: "[('a,'b) monoid_scheme,'a set] => 'a set"
    2.25     "set_inv G H == (m_inv G) ` H"
    2.26  
    2.27 -  normal     :: "['a set, ('a,'b) group_scheme] => bool"       (infixl "<|" 60)
    2.28 +  normal     :: "['a set, ('a,'b) monoid_scheme] => bool"       (infixl "<|" 60)
    2.29     "normal H G == subgroup H G & 
    2.30                    (\<forall>x \<in> carrier G. r_coset G H x = l_coset G x H)"
    2.31  
    2.32  syntax (xsymbols)
    2.33 -  normal  :: "['a set, ('a,'b) group_scheme] => bool" (infixl "\<lhd>" 60)
    2.34 +  normal  :: "['a set, ('a,'b) monoid_scheme] => bool" (infixl "\<lhd>" 60)
    2.35  
    2.36  locale coset = group G +
    2.37    fixes rcos      :: "['a set, 'a] => 'a set"     (infixl "#>" 60)
    2.38 @@ -153,7 +153,7 @@
    2.39  subsection{*normal subgroups*}
    2.40  
    2.41  (*????????????????
    2.42 -text{*Allows use of theorems proved in the locale coset*}
    2.43 +text "Allows use of theorems proved in the locale coset"
    2.44  lemma subgroup_imp_coset: "subgroup H G ==> coset G"
    2.45  apply (drule subgroup_imp_group)
    2.46  apply (simp add: group_def coset_def)  
    2.47 @@ -406,13 +406,13 @@
    2.48  subsection {*Factorization of a Group*}
    2.49  
    2.50  constdefs
    2.51 -  FactGroup :: "[('a,'b) group_scheme, 'a set] => ('a set) group"
    2.52 +  FactGroup :: "[('a,'b) monoid_scheme, 'a set] => ('a set) monoid"
    2.53       (infixl "Mod" 60)
    2.54     "FactGroup G H ==
    2.55        (| carrier = rcosets G H,
    2.56  	 mult = (%X: rcosets G H. %Y: rcosets G H. set_mult G X Y),
    2.57 -	 one = H,
    2.58 -	 m_inv = (%X: rcosets G H. set_inv G X) |)"
    2.59 +	 one = H (*,
    2.60 +	 m_inv = (%X: rcosets G H. set_inv G X) *) |)"
    2.61  
    2.62  lemma (in coset) setmult_closed:
    2.63       "[| H <| G; K1 \<in> rcosets G H; K2 \<in> rcosets G H |] 
    2.64 @@ -482,18 +482,13 @@
    2.65    "H <| G ==> group (G Mod H)"
    2.66  apply (insert is_coset) 
    2.67  apply (simp add: FactGroup_def) 
    2.68 -apply (rule group.intro)
    2.69 -   apply (rule magma.intro) 
    2.70 -   apply (simp add: coset.setmult_closed)
    2.71 -  apply (rule semigroup_axioms.intro)
    2.72 +apply (rule groupI)
    2.73 +    apply (simp add: coset.setmult_closed)
    2.74 +   apply (simp add: normal_imp_subgroup subgroup_in_rcosets)
    2.75    apply (simp add: restrictI coset.setmult_closed coset.setrcos_assoc)
    2.76 - apply (rule l_one.intro)
    2.77 -  apply (simp add: normal_imp_subgroup subgroup_in_rcosets)
    2.78   apply (simp add: normal_imp_subgroup
    2.79     subgroup_in_rcosets coset.setrcos_mult_eq)
    2.80 -apply (rule group_axioms.intro)
    2.81 - apply (simp add: restrictI setinv_closed)
    2.82 -apply (simp add: setinv_closed coset.setrcos_inv_mult_group_eq)
    2.83 +apply (auto dest: coset.setrcos_inv_mult_group_eq simp add: setinv_closed)
    2.84  done
    2.85  
    2.86  (*????????????????
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Wed Apr 30 10:01:35 2003 +0200
     3.3 @@ -0,0 +1,483 @@
     3.4 +(*  Title:      Product Operator for Commutative Monoids
     3.5 +    ID:         $Id$
     3.6 +    Author:     Clemens Ballarin, started 19 November 2002
     3.7 +
     3.8 +This file is largely based on HOL/Finite_Set.thy.
     3.9 +*)
    3.10 +
    3.11 +header {* Product Operator *}
    3.12 +
    3.13 +theory FiniteProduct = Group:
    3.14 +
    3.15 +(* Instantiation of LC from Finite_Set.thy is not possible,
    3.16 +   because here we have explicit typing rules like x : carrier G.
    3.17 +   We introduce an explicit argument for the domain D *)
    3.18 +
    3.19 +consts
    3.20 +  foldSetD :: "['a set, 'b => 'a => 'a, 'a] => ('b set * 'a) set"
    3.21 +
    3.22 +inductive "foldSetD D f e"
    3.23 +  intros
    3.24 +    emptyI [intro]: "e : D ==> ({}, e) : foldSetD D f e"
    3.25 +    insertI [intro]: "[| x ~: A; f x y : D; (A, y) : foldSetD D f e |] ==>
    3.26 +                      (insert x A, f x y) : foldSetD D f e"
    3.27 +
    3.28 +inductive_cases empty_foldSetDE [elim!]: "({}, x) : foldSetD D f e"
    3.29 +
    3.30 +constdefs
    3.31 +  foldD :: "['a set, 'b => 'a => 'a, 'a, 'b set] => 'a"
    3.32 +  "foldD D f e A == THE x. (A, x) : foldSetD D f e"
    3.33 +
    3.34 +lemma foldSetD_closed:
    3.35 +  "[| (A, z) : foldSetD D f e ; e : D; !!x y. [| x : A; y : D |] ==> f x y : D 
    3.36 +      |] ==> z : D";
    3.37 +  by (erule foldSetD.elims) auto
    3.38 +
    3.39 +lemma Diff1_foldSetD:
    3.40 +  "[| (A - {x}, y) : foldSetD D f e; x : A; f x y : D |] ==>
    3.41 +   (A, f x y) : foldSetD D f e"
    3.42 +  apply (erule insert_Diff [THEN subst], rule foldSetD.intros)
    3.43 +    apply auto
    3.44 +  done
    3.45 +
    3.46 +lemma foldSetD_imp_finite [simp]: "(A, x) : foldSetD D f e ==> finite A"
    3.47 +  by (induct set: foldSetD) auto
    3.48 +
    3.49 +lemma finite_imp_foldSetD:
    3.50 +  "[| finite A; e : D; !!x y. [| x : A; y : D |] ==> f x y : D |] ==>
    3.51 +   EX x. (A, x) : foldSetD D f e"
    3.52 +proof (induct set: Finites)
    3.53 +  case empty then show ?case by auto
    3.54 +next
    3.55 +  case (insert F x)
    3.56 +  then obtain y where y: "(F, y) : foldSetD D f e" by auto
    3.57 +  with insert have "y : D" by (auto dest: foldSetD_closed)
    3.58 +  with y and insert have "(insert x F, f x y) : foldSetD D f e"
    3.59 +    by (intro foldSetD.intros) auto
    3.60 +  then show ?case ..
    3.61 +qed
    3.62 +
    3.63 +subsection {* Left-commutative operations *}
    3.64 +
    3.65 +locale LCD =
    3.66 +  fixes B :: "'b set"
    3.67 +  and D :: "'a set"
    3.68 +  and f :: "'b => 'a => 'a"    (infixl "\<cdot>" 70)
    3.69 +  assumes left_commute:
    3.70 +    "[| x : B; y : B; z : D |] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
    3.71 +  and f_closed [simp, intro!]: "!!x y. [| x : B; y : D |] ==> f x y : D"
    3.72 +
    3.73 +lemma (in LCD) foldSetD_closed [dest]:
    3.74 +  "(A, z) : foldSetD D f e ==> z : D";
    3.75 +  by (erule foldSetD.elims) auto
    3.76 +
    3.77 +lemma (in LCD) Diff1_foldSetD:
    3.78 +  "[| (A - {x}, y) : foldSetD D f e; x : A; A <= B |] ==>
    3.79 +  (A, f x y) : foldSetD D f e"
    3.80 +  apply (subgoal_tac "x : B")
    3.81 +   prefer 2 apply fast
    3.82 +  apply (erule insert_Diff [THEN subst], rule foldSetD.intros)
    3.83 +    apply auto
    3.84 +  done
    3.85 +
    3.86 +lemma (in LCD) foldSetD_imp_finite [simp]:
    3.87 +  "(A, x) : foldSetD D f e ==> finite A"
    3.88 +  by (induct set: foldSetD) auto
    3.89 +
    3.90 +lemma (in LCD) finite_imp_foldSetD:
    3.91 +  "[| finite A; A <= B; e : D |] ==> EX x. (A, x) : foldSetD D f e"
    3.92 +proof (induct set: Finites)
    3.93 +  case empty then show ?case by auto
    3.94 +next
    3.95 +  case (insert F x)
    3.96 +  then obtain y where y: "(F, y) : foldSetD D f e" by auto
    3.97 +  with insert have "y : D" by auto
    3.98 +  with y and insert have "(insert x F, f x y) : foldSetD D f e"
    3.99 +    by (intro foldSetD.intros) auto
   3.100 +  then show ?case ..
   3.101 +qed
   3.102 +
   3.103 +lemma (in LCD) foldSetD_determ_aux:
   3.104 +  "e : D ==> ALL A x. A <= B & card A < n --> (A, x) : foldSetD D f e -->
   3.105 +    (ALL y. (A, y) : foldSetD D f e --> y = x)"
   3.106 +  apply (induct n)
   3.107 +   apply (auto simp add: less_Suc_eq) (* slow *)
   3.108 +  apply (erule foldSetD.cases)
   3.109 +   apply blast
   3.110 +  apply (erule foldSetD.cases)
   3.111 +   apply blast
   3.112 +  apply clarify
   3.113 +  txt {* force simplification of @{text "card A < card (insert ...)"}. *}
   3.114 +  apply (erule rev_mp)
   3.115 +  apply (simp add: less_Suc_eq_le)
   3.116 +  apply (rule impI)
   3.117 +  apply (rename_tac Aa xa ya Ab xb yb, case_tac "xa = xb")
   3.118 +   apply (subgoal_tac "Aa = Ab")
   3.119 +    prefer 2 apply (blast elim!: equalityE)
   3.120 +   apply blast
   3.121 +  txt {* case @{prop "xa \<notin> xb"}. *}
   3.122 +  apply (subgoal_tac "Aa - {xb} = Ab - {xa} & xb : Aa & xa : Ab")
   3.123 +   prefer 2 apply (blast elim!: equalityE)
   3.124 +  apply clarify
   3.125 +  apply (subgoal_tac "Aa = insert xb Ab - {xa}")
   3.126 +   prefer 2 apply blast
   3.127 +  apply (subgoal_tac "card Aa <= card Ab")
   3.128 +   prefer 2
   3.129 +   apply (rule Suc_le_mono [THEN subst])
   3.130 +   apply (simp add: card_Suc_Diff1)
   3.131 +  apply (rule_tac A1 = "Aa - {xb}" in finite_imp_foldSetD [THEN exE])
   3.132 +     apply (blast intro: foldSetD_imp_finite finite_Diff)
   3.133 +    apply best
   3.134 +   apply assumption
   3.135 +  apply (frule (1) Diff1_foldSetD)
   3.136 +   apply best
   3.137 +  apply (subgoal_tac "ya = f xb x")
   3.138 +   prefer 2
   3.139 +   apply (subgoal_tac "Aa <= B")
   3.140 +    prefer 2 apply best (* slow *)
   3.141 +   apply (blast del: equalityCE)
   3.142 +  apply (subgoal_tac "(Ab - {xa}, x) : foldSetD D f e")
   3.143 +   prefer 2 apply simp
   3.144 +  apply (subgoal_tac "yb = f xa x")
   3.145 +   prefer 2 
   3.146 +   apply (blast del: equalityCE dest: Diff1_foldSetD)
   3.147 +  apply (simp (no_asm_simp))
   3.148 +  apply (rule left_commute)
   3.149 +    apply assumption
   3.150 +   apply best (* slow *)
   3.151 +  apply best
   3.152 +  done
   3.153 +
   3.154 +lemma (in LCD) foldSetD_determ:
   3.155 +  "[| (A, x) : foldSetD D f e; (A, y) : foldSetD D f e; e : D; A <= B |]
   3.156 +  ==> y = x"
   3.157 +  by (blast intro: foldSetD_determ_aux [rule_format])
   3.158 +
   3.159 +lemma (in LCD) foldD_equality:
   3.160 +  "[| (A, y) : foldSetD D f e; e : D; A <= B |] ==> foldD D f e A = y"
   3.161 +  by (unfold foldD_def) (blast intro: foldSetD_determ)
   3.162 +
   3.163 +lemma foldD_empty [simp]:
   3.164 +  "e : D ==> foldD D f e {} = e"
   3.165 +  by (unfold foldD_def) blast
   3.166 +
   3.167 +lemma (in LCD) foldD_insert_aux:
   3.168 +  "[| x ~: A; x : B; e : D; A <= B |] ==>
   3.169 +    ((insert x A, v) : foldSetD D f e) =
   3.170 +    (EX y. (A, y) : foldSetD D f e & v = f x y)"
   3.171 +  apply auto
   3.172 +  apply (rule_tac A1 = A in finite_imp_foldSetD [THEN exE])
   3.173 +     apply (fastsimp dest: foldSetD_imp_finite)
   3.174 +    apply assumption
   3.175 +   apply assumption
   3.176 +  apply (blast intro: foldSetD_determ)
   3.177 +  done
   3.178 +
   3.179 +lemma (in LCD) foldD_insert:
   3.180 +    "[| finite A; x ~: A; x : B; e : D; A <= B |] ==>
   3.181 +     foldD D f e (insert x A) = f x (foldD D f e A)"
   3.182 +  apply (unfold foldD_def)
   3.183 +  apply (simp add: foldD_insert_aux)
   3.184 +  apply (rule the_equality)
   3.185 +   apply (auto intro: finite_imp_foldSetD
   3.186 +     cong add: conj_cong simp add: foldD_def [symmetric] foldD_equality)
   3.187 +  done
   3.188 +
   3.189 +lemma (in LCD) foldD_closed [simp]:
   3.190 +  "[| finite A; e : D; A <= B |] ==> foldD D f e A : D"
   3.191 +proof (induct set: Finites)
   3.192 +  case empty then show ?case by (simp add: foldD_empty)
   3.193 +next
   3.194 +  case insert then show ?case by (simp add: foldD_insert)
   3.195 +qed
   3.196 +
   3.197 +lemma (in LCD) foldD_commute:
   3.198 +  "[| finite A; x : B; e : D; A <= B |] ==>
   3.199 +   f x (foldD D f e A) = foldD D f (f x e) A"
   3.200 +  apply (induct set: Finites)
   3.201 +   apply simp
   3.202 +  apply (auto simp add: left_commute foldD_insert)
   3.203 +  done
   3.204 +
   3.205 +lemma Int_mono2:
   3.206 +  "[| A <= C; B <= C |] ==> A Int B <= C"
   3.207 +  by blast
   3.208 +
   3.209 +lemma (in LCD) foldD_nest_Un_Int:
   3.210 +  "[| finite A; finite C; e : D; A <= B; C <= B |] ==>
   3.211 +   foldD D f (foldD D f e C) A = foldD D f (foldD D f e (A Int C)) (A Un C)"
   3.212 +  apply (induct set: Finites)
   3.213 +   apply simp
   3.214 +  apply (simp add: foldD_insert foldD_commute Int_insert_left insert_absorb
   3.215 +    Int_mono2 Un_subset_iff)
   3.216 +  done
   3.217 +
   3.218 +lemma (in LCD) foldD_nest_Un_disjoint:
   3.219 +  "[| finite A; finite B; A Int B = {}; e : D; A <= B; C <= B |]
   3.220 +    ==> foldD D f e (A Un B) = foldD D f (foldD D f e B) A"
   3.221 +  by (simp add: foldD_nest_Un_Int)
   3.222 +
   3.223 +-- {* Delete rules to do with @{text foldSetD} relation. *}
   3.224 +
   3.225 +declare foldSetD_imp_finite [simp del]
   3.226 +  empty_foldSetDE [rule del]
   3.227 +  foldSetD.intros [rule del]
   3.228 +declare (in LCD)
   3.229 +  foldSetD_closed [rule del]
   3.230 +
   3.231 +subsection {* Commutative monoids *}
   3.232 +
   3.233 +text {*
   3.234 +  We enter a more restrictive context, with @{text "f :: 'a => 'a => 'a"}
   3.235 +  instead of @{text "'b => 'a => 'a"}.
   3.236 +*}
   3.237 +
   3.238 +locale ACeD =
   3.239 +  fixes D :: "'a set"
   3.240 +    and f :: "'a => 'a => 'a"    (infixl "\<cdot>" 70)
   3.241 +    and e :: 'a
   3.242 +  assumes ident [simp]: "x : D ==> x \<cdot> e = x"
   3.243 +    and commute: "[| x : D; y : D |] ==> x \<cdot> y = y \<cdot> x"
   3.244 +    and assoc: "[| x : D; y : D; z : D |] ==> (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
   3.245 +    and e_closed [simp]: "e : D"
   3.246 +    and f_closed [simp]: "[| x : D; y : D |] ==> x \<cdot> y : D"
   3.247 +
   3.248 +lemma (in ACeD) left_commute:
   3.249 +  "[| x : D; y : D; z : D |] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
   3.250 +proof -
   3.251 +  assume D: "x : D" "y : D" "z : D"
   3.252 +  then have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp add: commute)
   3.253 +  also from D have "... = y \<cdot> (z \<cdot> x)" by (simp add: assoc)
   3.254 +  also from D have "z \<cdot> x = x \<cdot> z" by (simp add: commute)
   3.255 +  finally show ?thesis .
   3.256 +qed
   3.257 +
   3.258 +lemmas (in ACeD) AC = assoc commute left_commute
   3.259 +
   3.260 +lemma (in ACeD) left_ident [simp]: "x : D ==> e \<cdot> x = x"
   3.261 +proof -
   3.262 +  assume D: "x : D"
   3.263 +  have "x \<cdot> e = x" by (rule ident)
   3.264 +  with D show ?thesis by (simp add: commute)
   3.265 +qed
   3.266 +
   3.267 +lemma (in ACeD) foldD_Un_Int:
   3.268 +  "[| finite A; finite B; A <= D; B <= D |] ==>
   3.269 +    foldD D f e A \<cdot> foldD D f e B =
   3.270 +    foldD D f e (A Un B) \<cdot> foldD D f e (A Int B)"
   3.271 +  apply (induct set: Finites)
   3.272 +   apply (simp add: left_commute LCD.foldD_closed [OF LCD.intro [of D]])
   3.273 +  apply (simp add: AC insert_absorb Int_insert_left
   3.274 +    LCD.foldD_insert [OF LCD.intro [of D]]
   3.275 +    LCD.foldD_closed [OF LCD.intro [of D]]
   3.276 +    Int_mono2 Un_subset_iff)
   3.277 +  done
   3.278 +
   3.279 +lemma (in ACeD) foldD_Un_disjoint:
   3.280 +  "[| finite A; finite B; A Int B = {}; A <= D; B <= D |] ==>
   3.281 +    foldD D f e (A Un B) = foldD D f e A \<cdot> foldD D f e B"
   3.282 +  by (simp add: foldD_Un_Int
   3.283 +    left_commute LCD.foldD_closed [OF LCD.intro [of D]] Un_subset_iff)
   3.284 +
   3.285 +subsection {* Products over Finite Sets *}
   3.286 +
   3.287 +constdefs
   3.288 +  finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b"
   3.289 +  "finprod G f A == if finite A
   3.290 +      then foldD (carrier G) (mult G o f) (one G) A
   3.291 +      else arbitrary"
   3.292 +
   3.293 +(* TODO: nice syntax for the summation operator inside the locale
   3.294 +   like \<Otimes>\<index> i\<in>A. f i, probably needs hand-coded translation *)
   3.295 +
   3.296 +ML_setup {* 
   3.297 +  Context.>> (fn thy => (simpset_ref_of thy :=
   3.298 +    simpset_of thy setsubgoaler asm_full_simp_tac; thy))
   3.299 +*}
   3.300 +
   3.301 +lemma (in comm_monoid) finprod_empty [simp]: 
   3.302 +  "finprod G f {} = \<one>"
   3.303 +  by (simp add: finprod_def)
   3.304 +
   3.305 +ML_setup {* 
   3.306 +  Context.>> (fn thy => (simpset_ref_of thy :=
   3.307 +    simpset_of thy setsubgoaler asm_simp_tac; thy))
   3.308 +*}
   3.309 +
   3.310 +declare funcsetI [intro]
   3.311 +  funcset_mem [dest]
   3.312 +
   3.313 +lemma (in comm_monoid) finprod_insert [simp]:
   3.314 +  "[| finite F; a \<notin> F; f \<in> F -> carrier G; f a \<in> carrier G |] ==>
   3.315 +   finprod G f (insert a F) = f a \<otimes> finprod G f F"
   3.316 +  apply (rule trans)
   3.317 +   apply (simp add: finprod_def)
   3.318 +  apply (rule trans)
   3.319 +   apply (rule LCD.foldD_insert [OF LCD.intro [of "insert a F"]])
   3.320 +         apply simp
   3.321 +         apply (rule m_lcomm)
   3.322 +           apply fast
   3.323 +          apply fast
   3.324 +         apply assumption
   3.325 +        apply (fastsimp intro: m_closed)
   3.326 +       apply simp+
   3.327 +   apply fast
   3.328 +  apply (auto simp add: finprod_def)
   3.329 +  done
   3.330 +
   3.331 +lemma (in comm_monoid) finprod_one [simp]:
   3.332 +  "finite A ==> finprod G (%i. \<one>) A = \<one>"
   3.333 +proof (induct set: Finites)
   3.334 +  case empty show ?case by simp
   3.335 +next
   3.336 +  case (insert A a)
   3.337 +  have "(%i. \<one>) \<in> A -> carrier G" by auto
   3.338 +  with insert show ?case by simp
   3.339 +qed
   3.340 +
   3.341 +lemma (in comm_monoid) finprod_closed [simp]:
   3.342 +  fixes A
   3.343 +  assumes fin: "finite A" and f: "f \<in> A -> carrier G" 
   3.344 +  shows "finprod G f A \<in> carrier G"
   3.345 +using fin f
   3.346 +proof induct
   3.347 +  case empty show ?case by simp
   3.348 +next
   3.349 +  case (insert A a)
   3.350 +  then have a: "f a \<in> carrier G" by fast
   3.351 +  from insert have A: "f \<in> A -> carrier G" by fast
   3.352 +  from insert A a show ?case by simp
   3.353 +qed
   3.354 +
   3.355 +lemma funcset_Int_left [simp, intro]:
   3.356 +  "[| f \<in> A -> C; f \<in> B -> C |] ==> f \<in> A Int B -> C"
   3.357 +  by fast
   3.358 +
   3.359 +lemma funcset_Un_left [iff]:
   3.360 +  "(f \<in> A Un B -> C) = (f \<in> A -> C & f \<in> B -> C)"
   3.361 +  by fast
   3.362 +
   3.363 +lemma (in comm_monoid) finprod_Un_Int:
   3.364 +  "[| finite A; finite B; g \<in> A -> carrier G; g \<in> B -> carrier G |] ==>
   3.365 +     finprod G g (A Un B) \<otimes> finprod G g (A Int B) =
   3.366 +     finprod G g A \<otimes> finprod G g B"
   3.367 +-- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
   3.368 +proof (induct set: Finites)
   3.369 +  case empty then show ?case by (simp add: finprod_closed)
   3.370 +next
   3.371 +  case (insert A a)
   3.372 +  then have a: "g a \<in> carrier G" by fast
   3.373 +  from insert have A: "g \<in> A -> carrier G" by fast
   3.374 +  from insert A a show ?case
   3.375 +    by (simp add: m_ac Int_insert_left insert_absorb finprod_closed
   3.376 +          Int_mono2 Un_subset_iff) 
   3.377 +qed
   3.378 +
   3.379 +lemma (in comm_monoid) finprod_Un_disjoint:
   3.380 +  "[| finite A; finite B; A Int B = {};
   3.381 +      g \<in> A -> carrier G; g \<in> B -> carrier G |]
   3.382 +   ==> finprod G g (A Un B) = finprod G g A \<otimes> finprod G g B"
   3.383 +  apply (subst finprod_Un_Int [symmetric])
   3.384 +      apply (auto simp add: finprod_closed)
   3.385 +  done
   3.386 +
   3.387 +lemma (in comm_monoid) finprod_multf:
   3.388 +  "[| finite A; f \<in> A -> carrier G; g \<in> A -> carrier G |] ==>
   3.389 +   finprod G (%x. f x \<otimes> g x) A = (finprod G f A \<otimes> finprod G g A)"
   3.390 +proof (induct set: Finites)
   3.391 +  case empty show ?case by simp
   3.392 +next
   3.393 +  case (insert A a) then
   3.394 +  have fA: "f : A -> carrier G" by fast
   3.395 +  from insert have fa: "f a : carrier G" by fast
   3.396 +  from insert have gA: "g : A -> carrier G" by fast
   3.397 +  from insert have ga: "g a : carrier G" by fast
   3.398 +  from insert have fgA: "(%x. f x \<otimes> g x) : A -> carrier G"
   3.399 +    by (simp add: Pi_def)
   3.400 +  show ?case  (* check if all simps are really necessary *)
   3.401 +    by (simp add: insert fA fa gA ga fgA m_ac Int_insert_left insert_absorb
   3.402 +      Int_mono2 Un_subset_iff)
   3.403 +qed
   3.404 +
   3.405 +lemma (in comm_monoid) finprod_cong':
   3.406 +  "[| A = B; g : B -> carrier G;
   3.407 +      !!i. i : B ==> f i = g i |] ==> finprod G f A = finprod G g B"
   3.408 +proof -
   3.409 +  assume prems: "A = B" "g : B -> carrier G"
   3.410 +    "!!i. i : B ==> f i = g i"
   3.411 +  show ?thesis
   3.412 +  proof (cases "finite B")
   3.413 +    case True
   3.414 +    then have "!!A. [| A = B; g : B -> carrier G;
   3.415 +      !!i. i : B ==> f i = g i |] ==> finprod G f A = finprod G g B"
   3.416 +    proof induct
   3.417 +      case empty thus ?case by simp
   3.418 +    next
   3.419 +      case (insert B x)
   3.420 +      then have "finprod G f A = finprod G f (insert x B)" by simp
   3.421 +      also from insert have "... = f x \<otimes> finprod G f B"
   3.422 +      proof (intro finprod_insert)
   3.423 +	show "finite B" .
   3.424 +      next
   3.425 +	show "x ~: B" .
   3.426 +      next
   3.427 +	assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
   3.428 +	  "g \<in> insert x B \<rightarrow> carrier G"
   3.429 +	thus "f : B -> carrier G" by fastsimp
   3.430 +      next
   3.431 +	assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
   3.432 +	  "g \<in> insert x B \<rightarrow> carrier G"
   3.433 +	thus "f x \<in> carrier G" by fastsimp
   3.434 +      qed
   3.435 +      also from insert have "... = g x \<otimes> finprod G g B" by fastsimp
   3.436 +      also from insert have "... = finprod G g (insert x B)"
   3.437 +      by (intro finprod_insert [THEN sym]) auto
   3.438 +      finally show ?case .
   3.439 +    qed
   3.440 +    with prems show ?thesis by simp
   3.441 +  next
   3.442 +    case False with prems show ?thesis by (simp add: finprod_def)
   3.443 +  qed
   3.444 +qed
   3.445 +
   3.446 +lemma (in comm_monoid) finprod_cong:
   3.447 +  "[| A = B; !!i. i : B ==> f i = g i;
   3.448 +      g : B -> carrier G = True |] ==> finprod G f A = finprod G g B"
   3.449 +  by (rule finprod_cong') fast+
   3.450 +
   3.451 +text {*Usually, if this rule causes a failed congruence proof error,
   3.452 +  the reason is that the premise @{text "g : B -> carrier G"} cannot be shown.
   3.453 +  Adding @{thm [source] Pi_def} to the simpset is often useful.
   3.454 +  For this reason, @{thm [source] comm_monoid.finprod_cong}
   3.455 +  is not added to the simpset by default.
   3.456 +*}
   3.457 +
   3.458 +declare funcsetI [rule del]
   3.459 +  funcset_mem [rule del]
   3.460 +
   3.461 +lemma (in comm_monoid) finprod_0 [simp]:
   3.462 +  "f : {0::nat} -> carrier G ==> finprod G f {..0} = f 0"
   3.463 +by (simp add: Pi_def)
   3.464 +
   3.465 +lemma (in comm_monoid) finprod_Suc [simp]:
   3.466 +  "f : {..Suc n} -> carrier G ==>
   3.467 +   finprod G f {..Suc n} = (f (Suc n) \<otimes> finprod G f {..n})"
   3.468 +by (simp add: Pi_def atMost_Suc)
   3.469 +
   3.470 +lemma (in comm_monoid) finprod_Suc2:
   3.471 +  "f : {..Suc n} -> carrier G ==>
   3.472 +   finprod G f {..Suc n} = (finprod G (%i. f (Suc i)) {..n} \<otimes> f 0)"
   3.473 +proof (induct n)
   3.474 +  case 0 thus ?case by (simp add: Pi_def)
   3.475 +next
   3.476 +  case Suc thus ?case by (simp add: m_assoc Pi_def)
   3.477 +qed
   3.478 +
   3.479 +lemma (in comm_monoid) finprod_mult [simp]:
   3.480 +  "[| f : {..n} -> carrier G; g : {..n} -> carrier G |] ==>
   3.481 +     finprod G (%i. f i \<otimes> g i) {..n::nat} =
   3.482 +     finprod G f {..n} \<otimes> finprod G g {..n}"
   3.483 +  by (induct n) (simp_all add: m_ac Pi_def)
   3.484 +
   3.485 +end
   3.486 +
     4.1 --- a/src/HOL/Algebra/Group.thy	Tue Apr 29 12:36:49 2003 +0200
     4.2 +++ b/src/HOL/Algebra/Group.thy	Wed Apr 30 10:01:35 2003 +0200
     4.3 @@ -6,18 +6,23 @@
     4.4  Based on work by Florian Kammueller, L C Paulson and Markus Wenzel.
     4.5  *)
     4.6  
     4.7 -header {* Algebraic Structures up to Abelian Groups *}
     4.8 +header {* Algebraic Structures up to Commutative Groups *}
     4.9  
    4.10  theory Group = FuncSet:
    4.11  
    4.12 +axclass number < type
    4.13 +
    4.14 +instance nat :: number ..
    4.15 +instance int :: number ..
    4.16 +
    4.17 +section {* From Magmas to Groups *}
    4.18 +
    4.19  text {*
    4.20    Definitions follow Jacobson, Basic Algebra I, Freeman, 1985; with
    4.21    the exception of \emph{magma} which, following Bourbaki, is a set
    4.22    together with a binary, closed operation.
    4.23  *}
    4.24  
    4.25 -section {* From Magmas to Groups *}
    4.26 -
    4.27  subsection {* Definitions *}
    4.28  
    4.29  record 'a semigroup =
    4.30 @@ -27,8 +32,23 @@
    4.31  record 'a monoid = "'a semigroup" +
    4.32    one :: 'a ("\<one>\<index>")
    4.33  
    4.34 -record 'a group = "'a monoid" +
    4.35 -  m_inv :: "'a => 'a" ("inv\<index> _" [81] 80)
    4.36 +constdefs
    4.37 +  m_inv :: "[('a, 'm) monoid_scheme, 'a] => 'a" ("inv\<index> _" [81] 80)
    4.38 +  "m_inv G x == (THE y. y \<in> carrier G &
    4.39 +                  mult G x y = one G & mult G y x = one G)"
    4.40 +
    4.41 +  Units :: "('a, 'm) monoid_scheme => 'a set"
    4.42 +  "Units G == {y. y \<in> carrier G &
    4.43 +                  (EX x : carrier G. mult G x y = one G & mult G y x = one G)}"
    4.44 +
    4.45 +consts
    4.46 +  pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a" (infixr "'(^')\<index>" 75)
    4.47 +
    4.48 +defs (overloaded)
    4.49 +  nat_pow_def: "pow G a n == nat_rec (one G) (%u b. mult G b a) n"
    4.50 +  int_pow_def: "pow G a z ==
    4.51 +    let p = nat_rec (one G) (%u b. mult G b a)
    4.52 +    in if neg z then m_inv G (p (nat (-z))) else p (nat z)"
    4.53  
    4.54  locale magma = struct G +
    4.55    assumes m_closed [intro, simp]:
    4.56 @@ -37,32 +57,237 @@
    4.57  locale semigroup = magma +
    4.58    assumes m_assoc:
    4.59      "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
    4.60 -     (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
    4.61 +    (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
    4.62  
    4.63 -locale l_one = struct G +
    4.64 +locale monoid = semigroup +
    4.65    assumes one_closed [intro, simp]: "\<one> \<in> carrier G"
    4.66      and l_one [simp]: "x \<in> carrier G ==> \<one> \<otimes> x = x"
    4.67 +    and r_one [simp]: "x \<in> carrier G ==> x \<otimes> \<one> = x"
    4.68  
    4.69 -locale group = semigroup + l_one +
    4.70 -  assumes inv_closed [intro, simp]: "x \<in> carrier G ==> inv x \<in> carrier G"
    4.71 -    and l_inv: "x \<in> carrier G ==> inv x \<otimes> x = \<one>"
    4.72 +lemma monoidI:
    4.73 +  assumes m_closed:
    4.74 +      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y \<in> carrier G"
    4.75 +    and one_closed: "one G \<in> carrier G"
    4.76 +    and m_assoc:
    4.77 +      "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
    4.78 +      mult G (mult G x y) z = mult G x (mult G y z)"
    4.79 +    and l_one: "!!x. x \<in> carrier G ==> mult G (one G) x = x"
    4.80 +    and r_one: "!!x. x \<in> carrier G ==> mult G x (one G) = x"
    4.81 +  shows "monoid G"
    4.82 +  by (fast intro!: monoid.intro magma.intro semigroup_axioms.intro
    4.83 +    semigroup.intro monoid_axioms.intro
    4.84 +    intro: prems)
    4.85 +
    4.86 +lemma (in monoid) Units_closed [dest]:
    4.87 +  "x \<in> Units G ==> x \<in> carrier G"
    4.88 +  by (unfold Units_def) fast
    4.89 +
    4.90 +lemma (in monoid) inv_unique:
    4.91 +  assumes eq: "y \<otimes> x = \<one>" "x \<otimes> y' = \<one>"
    4.92 +    and G: "x \<in> carrier G" "y \<in> carrier G" "y' \<in> carrier G"
    4.93 +  shows "y = y'"
    4.94 +proof -
    4.95 +  from G eq have "y = y \<otimes> (x \<otimes> y')" by simp
    4.96 +  also from G have "... = (y \<otimes> x) \<otimes> y'" by (simp add: m_assoc)
    4.97 +  also from G eq have "... = y'" by simp
    4.98 +  finally show ?thesis .
    4.99 +qed
   4.100 +
   4.101 +lemma (in monoid) Units_inv_closed [intro, simp]:
   4.102 +  "x \<in> Units G ==> inv x \<in> carrier G"
   4.103 +  apply (unfold Units_def m_inv_def)
   4.104 +  apply auto
   4.105 +  apply (rule theI2, fast)
   4.106 +   apply (fast intro: inv_unique)
   4.107 +  apply fast
   4.108 +  done
   4.109 +
   4.110 +lemma (in monoid) Units_l_inv:
   4.111 +  "x \<in> Units G ==> inv x \<otimes> x = \<one>"
   4.112 +  apply (unfold Units_def m_inv_def)
   4.113 +  apply auto
   4.114 +  apply (rule theI2, fast)
   4.115 +   apply (fast intro: inv_unique)
   4.116 +  apply fast
   4.117 +  done
   4.118 +
   4.119 +lemma (in monoid) Units_r_inv:
   4.120 +  "x \<in> Units G ==> x \<otimes> inv x = \<one>"
   4.121 +  apply (unfold Units_def m_inv_def)
   4.122 +  apply auto
   4.123 +  apply (rule theI2, fast)
   4.124 +   apply (fast intro: inv_unique)
   4.125 +  apply fast
   4.126 +  done
   4.127 +
   4.128 +lemma (in monoid) Units_inv_Units [intro, simp]:
   4.129 +  "x \<in> Units G ==> inv x \<in> Units G"
   4.130 +proof -
   4.131 +  assume x: "x \<in> Units G"
   4.132 +  show "inv x \<in> Units G"
   4.133 +    by (auto simp add: Units_def
   4.134 +      intro: Units_l_inv Units_r_inv x Units_closed [OF x])
   4.135 +qed
   4.136 +
   4.137 +lemma (in monoid) Units_l_cancel [simp]:
   4.138 +  "[| x \<in> Units G; y \<in> carrier G; z \<in> carrier G |] ==>
   4.139 +   (x \<otimes> y = x \<otimes> z) = (y = z)"
   4.140 +proof
   4.141 +  assume eq: "x \<otimes> y = x \<otimes> z"
   4.142 +    and G: "x \<in> Units G" "y \<in> carrier G" "z \<in> carrier G"
   4.143 +  then have "(inv x \<otimes> x) \<otimes> y = (inv x \<otimes> x) \<otimes> z"
   4.144 +    by (simp add: m_assoc Units_closed)
   4.145 +  with G show "y = z" by (simp add: Units_l_inv)
   4.146 +next
   4.147 +  assume eq: "y = z"
   4.148 +    and G: "x \<in> Units G" "y \<in> carrier G" "z \<in> carrier G"
   4.149 +  then show "x \<otimes> y = x \<otimes> z" by simp
   4.150 +qed
   4.151 +
   4.152 +lemma (in monoid) Units_inv_inv [simp]:
   4.153 +  "x \<in> Units G ==> inv (inv x) = x"
   4.154 +proof -
   4.155 +  assume x: "x \<in> Units G"
   4.156 +  then have "inv x \<otimes> inv (inv x) = inv x \<otimes> x"
   4.157 +    by (simp add: Units_l_inv Units_r_inv)
   4.158 +  with x show ?thesis by (simp add: Units_closed)
   4.159 +qed
   4.160 +
   4.161 +lemma (in monoid) inv_inj_on_Units:
   4.162 +  "inj_on (m_inv G) (Units G)"
   4.163 +proof (rule inj_onI)
   4.164 +  fix x y
   4.165 +  assume G: "x \<in> Units G" "y \<in> Units G" and eq: "inv x = inv y"
   4.166 +  then have "inv (inv x) = inv (inv y)" by simp
   4.167 +  with G show "x = y" by simp
   4.168 +qed
   4.169 +
   4.170 +text {* Power *}
   4.171 +
   4.172 +lemma (in monoid) nat_pow_closed [intro, simp]:
   4.173 +  "x \<in> carrier G ==> x (^) (n::nat) \<in> carrier G"
   4.174 +  by (induct n) (simp_all add: nat_pow_def)
   4.175 +
   4.176 +lemma (in monoid) nat_pow_0 [simp]:
   4.177 +  "x (^) (0::nat) = \<one>"
   4.178 +  by (simp add: nat_pow_def)
   4.179 +
   4.180 +lemma (in monoid) nat_pow_Suc [simp]:
   4.181 +  "x (^) (Suc n) = x (^) n \<otimes> x"
   4.182 +  by (simp add: nat_pow_def)
   4.183 +
   4.184 +lemma (in monoid) nat_pow_one [simp]:
   4.185 +  "\<one> (^) (n::nat) = \<one>"
   4.186 +  by (induct n) simp_all
   4.187 +
   4.188 +lemma (in monoid) nat_pow_mult:
   4.189 +  "x \<in> carrier G ==> x (^) (n::nat) \<otimes> x (^) m = x (^) (n + m)"
   4.190 +  by (induct m) (simp_all add: m_assoc [THEN sym])
   4.191 +
   4.192 +lemma (in monoid) nat_pow_pow:
   4.193 +  "x \<in> carrier G ==> (x (^) n) (^) m = x (^) (n * m::nat)"
   4.194 +  by (induct m) (simp, simp add: nat_pow_mult add_commute)
   4.195 +
   4.196 +text {*
   4.197 +  A group is a monoid all of whose elements are invertible.
   4.198 +*}
   4.199 +
   4.200 +locale group = monoid +
   4.201 +  assumes Units: "carrier G <= Units G"
   4.202 +
   4.203 +theorem groupI:
   4.204 +  assumes m_closed [simp]:
   4.205 +      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y \<in> carrier G"
   4.206 +    and one_closed [simp]: "one G \<in> carrier G"
   4.207 +    and m_assoc:
   4.208 +      "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
   4.209 +      mult G (mult G x y) z = mult G x (mult G y z)"
   4.210 +    and l_one [simp]: "!!x. x \<in> carrier G ==> mult G (one G) x = x"
   4.211 +    and l_inv_ex: "!!x. x \<in> carrier G ==> EX y : carrier G. mult G y x = one G"
   4.212 +  shows "group G"
   4.213 +proof -
   4.214 +  have l_cancel [simp]:
   4.215 +    "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
   4.216 +    (mult G x y = mult G x z) = (y = z)"
   4.217 +  proof
   4.218 +    fix x y z
   4.219 +    assume eq: "mult G x y = mult G x z"
   4.220 +      and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
   4.221 +    with l_inv_ex obtain x_inv where xG: "x_inv \<in> carrier G"
   4.222 +      and l_inv: "mult G x_inv x = one G" by fast
   4.223 +    from G eq xG have "mult G (mult G x_inv x) y = mult G (mult G x_inv x) z"
   4.224 +      by (simp add: m_assoc)
   4.225 +    with G show "y = z" by (simp add: l_inv)
   4.226 +  next
   4.227 +    fix x y z
   4.228 +    assume eq: "y = z"
   4.229 +      and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
   4.230 +    then show "mult G x y = mult G x z" by simp
   4.231 +  qed
   4.232 +  have r_one:
   4.233 +    "!!x. x \<in> carrier G ==> mult G x (one G) = x"
   4.234 +  proof -
   4.235 +    fix x
   4.236 +    assume x: "x \<in> carrier G"
   4.237 +    with l_inv_ex obtain x_inv where xG: "x_inv \<in> carrier G"
   4.238 +      and l_inv: "mult G x_inv x = one G" by fast
   4.239 +    from x xG have "mult G x_inv (mult G x (one G)) = mult G x_inv x"
   4.240 +      by (simp add: m_assoc [symmetric] l_inv)
   4.241 +    with x xG show "mult G x (one G) = x" by simp 
   4.242 +  qed
   4.243 +  have inv_ex:
   4.244 +    "!!x. x \<in> carrier G ==> EX y : carrier G. mult G y x = one G &
   4.245 +      mult G x y = one G"
   4.246 +  proof -
   4.247 +    fix x
   4.248 +    assume x: "x \<in> carrier G"
   4.249 +    with l_inv_ex obtain y where y: "y \<in> carrier G"
   4.250 +      and l_inv: "mult G y x = one G" by fast
   4.251 +    from x y have "mult G y (mult G x y) = mult G y (one G)"
   4.252 +      by (simp add: m_assoc [symmetric] l_inv r_one)
   4.253 +    with x y have r_inv: "mult G x y = one G"
   4.254 +      by simp
   4.255 +    from x y show "EX y : carrier G. mult G y x = one G &
   4.256 +      mult G x y = one G"
   4.257 +      by (fast intro: l_inv r_inv)
   4.258 +  qed
   4.259 +  then have carrier_subset_Units: "carrier G <= Units G"
   4.260 +    by (unfold Units_def) fast
   4.261 +  show ?thesis
   4.262 +    by (fast intro!: group.intro magma.intro semigroup_axioms.intro
   4.263 +      semigroup.intro monoid_axioms.intro group_axioms.intro
   4.264 +      carrier_subset_Units intro: prems r_one)
   4.265 +qed
   4.266 +
   4.267 +lemma (in monoid) monoid_groupI:
   4.268 +  assumes l_inv_ex:
   4.269 +    "!!x. x \<in> carrier G ==> EX y : carrier G. mult G y x = one G"
   4.270 +  shows "group G"
   4.271 +  by (rule groupI) (auto intro: m_assoc l_inv_ex)
   4.272 +
   4.273 +lemma (in group) Units_eq [simp]:
   4.274 +  "Units G = carrier G"
   4.275 +proof
   4.276 +  show "Units G <= carrier G" by fast
   4.277 +next
   4.278 +  show "carrier G <= Units G" by (rule Units)
   4.279 +qed
   4.280 +
   4.281 +lemma (in group) inv_closed [intro, simp]:
   4.282 +  "x \<in> carrier G ==> inv x \<in> carrier G"
   4.283 +  using Units_inv_closed by simp
   4.284 +
   4.285 +lemma (in group) l_inv:
   4.286 +  "x \<in> carrier G ==> inv x \<otimes> x = \<one>"
   4.287 +  using Units_l_inv by simp
   4.288  
   4.289  subsection {* Cancellation Laws and Basic Properties *}
   4.290  
   4.291  lemma (in group) l_cancel [simp]:
   4.292    "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
   4.293     (x \<otimes> y = x \<otimes> z) = (y = z)"
   4.294 -proof
   4.295 -  assume eq: "x \<otimes> y = x \<otimes> z"
   4.296 -    and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
   4.297 -  then have "(inv x \<otimes> x) \<otimes> y = (inv x \<otimes> x) \<otimes> z" by (simp add: m_assoc)
   4.298 -  with G show "y = z" by (simp add: l_inv)
   4.299 -next
   4.300 -  assume eq: "y = z"
   4.301 -    and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
   4.302 -  then show "x \<otimes> y = x \<otimes> z" by simp
   4.303 -qed
   4.304 -
   4.305 +  using Units_l_inv by simp
   4.306 +(*
   4.307  lemma (in group) r_one [simp]:  
   4.308    "x \<in> carrier G ==> x \<otimes> \<one> = x"
   4.309  proof -
   4.310 @@ -71,7 +296,7 @@
   4.311      by (simp add: m_assoc [symmetric] l_inv)
   4.312    with x show ?thesis by simp 
   4.313  qed
   4.314 -
   4.315 +*)
   4.316  lemma (in group) r_inv:
   4.317    "x \<in> carrier G ==> x \<otimes> inv x = \<one>"
   4.318  proof -
   4.319 @@ -106,11 +331,11 @@
   4.320  
   4.321  lemma (in group) inv_inv [simp]:
   4.322    "x \<in> carrier G ==> inv (inv x) = x"
   4.323 -proof -
   4.324 -  assume x: "x \<in> carrier G"
   4.325 -  then have "inv x \<otimes> inv (inv x) = inv x \<otimes> x" by (simp add: l_inv r_inv)
   4.326 -  with x show ?thesis by simp
   4.327 -qed
   4.328 +  using Units_inv_inv by simp
   4.329 +
   4.330 +lemma (in group) inv_inj:
   4.331 +  "inj_on (m_inv G) (carrier G)"
   4.332 +  using inv_inj_on_Units by simp
   4.333  
   4.334  lemma (in group) inv_mult_group:
   4.335    "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv y \<otimes> inv x"
   4.336 @@ -121,6 +346,20 @@
   4.337    with G show ?thesis by simp
   4.338  qed
   4.339  
   4.340 +text {* Power *}
   4.341 +
   4.342 +lemma (in group) int_pow_def2:
   4.343 +  "a (^) (z::int) = (if neg z then inv (a (^) (nat (-z))) else a (^) (nat z))"
   4.344 +  by (simp add: int_pow_def nat_pow_def Let_def)
   4.345 +
   4.346 +lemma (in group) int_pow_0 [simp]:
   4.347 +  "x (^) (0::int) = \<one>"
   4.348 +  by (simp add: int_pow_def2)
   4.349 +
   4.350 +lemma (in group) int_pow_one [simp]:
   4.351 +  "\<one> (^) (z::int) = \<one>"
   4.352 +  by (simp add: int_pow_def2)
   4.353 +
   4.354  subsection {* Substructures *}
   4.355  
   4.356  locale submagma = var H + struct G +
   4.357 @@ -128,7 +367,7 @@
   4.358      and m_closed [intro, simp]: "[| x \<in> H; y \<in> H |] ==> x \<otimes> y \<in> H"
   4.359  
   4.360  declare (in submagma) magma.intro [intro] semigroup.intro [intro]
   4.361 -
   4.362 +  semigroup_axioms.intro [intro]
   4.363  (*
   4.364  alternative definition of submagma
   4.365  
   4.366 @@ -167,21 +406,21 @@
   4.367      and m_inv_closed [intro, simp]: "x \<in> H ==> inv x \<in> H"
   4.368  
   4.369  declare (in subgroup) group.intro [intro]
   4.370 -
   4.371 +(*
   4.372  lemma (in subgroup) l_oneI [intro]:
   4.373    includes l_one G
   4.374    shows "l_one (G(| carrier := H |))"
   4.375    by rule simp_all
   4.376 -
   4.377 +*)
   4.378  lemma (in subgroup) group_axiomsI [intro]:
   4.379    includes group G
   4.380    shows "group_axioms (G(| carrier := H |))"
   4.381 -  by rule (simp_all add: l_inv)
   4.382 +  by rule (auto intro: l_inv r_inv simp add: Units_def)
   4.383  
   4.384  lemma (in subgroup) groupI [intro]:
   4.385    includes group G
   4.386    shows "group (G(| carrier := H |))"
   4.387 -  using prems by fast
   4.388 +  by (rule groupI) (auto intro: m_assoc l_inv)
   4.389  
   4.390  text {*
   4.391    Since @{term H} is nonempty, it contains some element @{term x}.  Since
   4.392 @@ -223,8 +462,8 @@
   4.393  
   4.394  declare magma.m_closed [simp]
   4.395  
   4.396 -declare l_one.one_closed [iff] group.inv_closed [simp]
   4.397 -  l_one.l_one [simp] group.r_one [simp] group.inv_inv [simp]
   4.398 +declare monoid.one_closed [iff] group.inv_closed [simp]
   4.399 +  monoid.l_one [simp] monoid.r_one [simp] group.inv_inv [simp]
   4.400  
   4.401  lemma subgroup_nonempty:
   4.402    "~ subgroup {} G"
   4.403 @@ -241,6 +480,11 @@
   4.404    with subgroup_nonempty show ?thesis by contradiction
   4.405  qed
   4.406  
   4.407 +(*
   4.408 +lemma (in monoid) Units_subgroup:
   4.409 +  "subgroup (Units G) G"
   4.410 +*)
   4.411 +
   4.412  subsection {* Direct Products *}
   4.413  
   4.414  constdefs
   4.415 @@ -251,13 +495,13 @@
   4.416    "G \<times>\<^sub>s H == (| carrier = carrier G \<times> carrier H,
   4.417      mult = (%(xg, xh) (yg, yh). (mult G xg yg, mult H xh yh)) |)"
   4.418  
   4.419 -  DirProdMonoid ::
   4.420 +  DirProdGroup ::
   4.421      "[('a, 'm) monoid_scheme, ('b, 'n) monoid_scheme] => ('a \<times> 'b) monoid"
   4.422 -    (infixr "\<times>\<^sub>m" 80)
   4.423 -  "G \<times>\<^sub>m H == (| carrier = carrier (G \<times>\<^sub>s H),
   4.424 +    (infixr "\<times>\<^sub>g" 80)
   4.425 +  "G \<times>\<^sub>g H == (| carrier = carrier (G \<times>\<^sub>s H),
   4.426      mult = mult (G \<times>\<^sub>s H),
   4.427      one = (one G, one H) |)"
   4.428 -
   4.429 +(*
   4.430    DirProdGroup ::
   4.431      "[('a, 'm) group_scheme, ('b, 'n) group_scheme] => ('a \<times> 'b) group"
   4.432      (infixr "\<times>\<^sub>g" 80)
   4.433 @@ -265,6 +509,7 @@
   4.434      mult = mult (G \<times>\<^sub>m H),
   4.435      one = one (G \<times>\<^sub>m H),
   4.436      m_inv = (%(g, h). (m_inv G g, m_inv H h)) |)"
   4.437 +*)
   4.438  
   4.439  lemma DirProdSemigroup_magma:
   4.440    includes magma G + magma H
   4.441 @@ -287,13 +532,13 @@
   4.442    includes magma G + magma H
   4.443    shows "magma (G \<times>\<^sub>g H)"
   4.444    by rule
   4.445 -    (auto simp add: DirProdGroup_def DirProdMonoid_def DirProdSemigroup_def)
   4.446 +    (auto simp add: DirProdGroup_def DirProdSemigroup_def)
   4.447  
   4.448  lemma DirProdGroup_semigroup_axioms:
   4.449    includes semigroup G + semigroup H
   4.450    shows "semigroup_axioms (G \<times>\<^sub>g H)"
   4.451    by rule
   4.452 -    (auto simp add: DirProdGroup_def DirProdMonoid_def DirProdSemigroup_def
   4.453 +    (auto simp add: DirProdGroup_def DirProdSemigroup_def
   4.454        G.m_assoc H.m_assoc)
   4.455  
   4.456  lemma DirProdGroup_semigroup:
   4.457 @@ -308,11 +553,9 @@
   4.458  lemma DirProdGroup_group:
   4.459    includes group G + group H
   4.460    shows "group (G \<times>\<^sub>g H)"
   4.461 -by rule
   4.462 -  (auto intro: magma.intro l_one.intro
   4.463 -      semigroup_axioms.intro group_axioms.intro
   4.464 -    simp add: DirProdGroup_def DirProdMonoid_def DirProdSemigroup_def
   4.465 -      G.m_assoc H.m_assoc G.l_inv H.l_inv)
   4.466 +  by (rule groupI)
   4.467 +    (auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv
   4.468 +      simp add: DirProdGroup_def DirProdSemigroup_def)
   4.469  
   4.470  subsection {* Homomorphisms *}
   4.471  
   4.472 @@ -376,14 +619,20 @@
   4.473    with x show ?thesis by simp
   4.474  qed
   4.475  
   4.476 -section {* Abelian Structures *}
   4.477 +section {* Commutative Structures *}
   4.478 +
   4.479 +text {*
   4.480 +  Naming convention: multiplicative structures that are commutative
   4.481 +  are called \emph{commutative}, additive structures are called
   4.482 +  \emph{Abelian}.
   4.483 +*}
   4.484  
   4.485  subsection {* Definition *}
   4.486  
   4.487 -locale abelian_semigroup = semigroup +
   4.488 +locale comm_semigroup = semigroup +
   4.489    assumes m_comm: "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x"
   4.490  
   4.491 -lemma (in abelian_semigroup) m_lcomm:
   4.492 +lemma (in comm_semigroup) m_lcomm:
   4.493    "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
   4.494     x \<otimes> (y \<otimes> z) = y \<otimes> (x \<otimes> z)"
   4.495  proof -
   4.496 @@ -394,11 +643,33 @@
   4.497    finally show ?thesis .
   4.498  qed
   4.499  
   4.500 -lemmas (in abelian_semigroup) ac = m_assoc m_comm m_lcomm
   4.501 +lemmas (in comm_semigroup) m_ac = m_assoc m_comm m_lcomm
   4.502 +
   4.503 +locale comm_monoid = comm_semigroup + monoid
   4.504  
   4.505 -locale abelian_monoid = abelian_semigroup + l_one
   4.506 +lemma comm_monoidI:
   4.507 +  assumes m_closed:
   4.508 +      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y \<in> carrier G"
   4.509 +    and one_closed: "one G \<in> carrier G"
   4.510 +    and m_assoc:
   4.511 +      "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
   4.512 +      mult G (mult G x y) z = mult G x (mult G y z)"
   4.513 +    and l_one: "!!x. x \<in> carrier G ==> mult G (one G) x = x"
   4.514 +    and m_comm:
   4.515 +      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y = mult G y x"
   4.516 +  shows "comm_monoid G"
   4.517 +  using l_one
   4.518 +  by (auto intro!: comm_monoid.intro magma.intro semigroup_axioms.intro
   4.519 +    comm_semigroup_axioms.intro monoid_axioms.intro
   4.520 +    intro: prems simp: m_closed one_closed m_comm)
   4.521  
   4.522 -lemma (in abelian_monoid) l_one [simp]:
   4.523 +lemma (in monoid) monoid_comm_monoidI:
   4.524 +  assumes m_comm:
   4.525 +      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y = mult G y x"
   4.526 +  shows "comm_monoid G"
   4.527 +  by (rule comm_monoidI) (auto intro: m_assoc m_comm)
   4.528 +(*
   4.529 +lemma (in comm_monoid) r_one [simp]:
   4.530    "x \<in> carrier G ==> x \<otimes> \<one> = x"
   4.531  proof -
   4.532    assume G: "x \<in> carrier G"
   4.533 @@ -406,11 +677,38 @@
   4.534    also from G have "... = x" by simp
   4.535    finally show ?thesis .
   4.536  qed
   4.537 +*)
   4.538  
   4.539 -locale abelian_group = abelian_monoid + group
   4.540 +lemma (in comm_monoid) nat_pow_distr:
   4.541 +  "[| x \<in> carrier G; y \<in> carrier G |] ==>
   4.542 +  (x \<otimes> y) (^) (n::nat) = x (^) n \<otimes> y (^) n"
   4.543 +  by (induct n) (simp, simp add: m_ac)
   4.544 +
   4.545 +locale comm_group = comm_monoid + group
   4.546 +
   4.547 +lemma (in group) group_comm_groupI:
   4.548 +  assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==>
   4.549 +      mult G x y = mult G y x"
   4.550 +  shows "comm_group G"
   4.551 +  by (fast intro: comm_group.intro comm_semigroup_axioms.intro
   4.552 +    group.axioms prems)
   4.553  
   4.554 -lemma (in abelian_group) inv_mult:
   4.555 +lemma comm_groupI:
   4.556 +  assumes m_closed:
   4.557 +      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y \<in> carrier G"
   4.558 +    and one_closed: "one G \<in> carrier G"
   4.559 +    and m_assoc:
   4.560 +      "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
   4.561 +      mult G (mult G x y) z = mult G x (mult G y z)"
   4.562 +    and m_comm:
   4.563 +      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y = mult G y x"
   4.564 +    and l_one: "!!x. x \<in> carrier G ==> mult G (one G) x = x"
   4.565 +    and l_inv_ex: "!!x. x \<in> carrier G ==> EX y : carrier G. mult G y x = one G"
   4.566 +  shows "comm_group G"
   4.567 +  by (fast intro: group.group_comm_groupI groupI prems)
   4.568 +
   4.569 +lemma (in comm_group) inv_mult:
   4.570    "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv x \<otimes> inv y"
   4.571 -  by (simp add: ac inv_mult_group)
   4.572 +  by (simp add: m_ac inv_mult_group)
   4.573  
   4.574  end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Algebra/Module.thy	Wed Apr 30 10:01:35 2003 +0200
     5.3 @@ -0,0 +1,161 @@
     5.4 +(*  Title:      HOL/Algebra/Module
     5.5 +    ID:         $Id$
     5.6 +    Author:     Clemens Ballarin, started 15 April 2003
     5.7 +    Copyright:  Clemens Ballarin
     5.8 +*)
     5.9 +
    5.10 +theory Module = CRing:
    5.11 +
    5.12 +section {* Modules over an Abelian Group *}
    5.13 +
    5.14 +record ('a, 'b) module = "'b ring" +
    5.15 +  smult :: "['a, 'b] => 'b" (infixl "\<odot>\<index>" 70)
    5.16 +
    5.17 +locale module = cring R + abelian_group M +
    5.18 +  assumes smult_closed [simp, intro]:
    5.19 +      "[| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^sub>2 x \<in> carrier M"
    5.20 +    and smult_l_distr:
    5.21 +      "[| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
    5.22 +      (a \<oplus> b) \<odot>\<^sub>2 x = a \<odot>\<^sub>2 x \<oplus>\<^sub>2 b \<odot>\<^sub>2 x"
    5.23 +    and smult_r_distr:
    5.24 +      "[| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
    5.25 +      a \<odot>\<^sub>2 (x \<oplus>\<^sub>2 y) = a \<odot>\<^sub>2 x \<oplus>\<^sub>2 a \<odot>\<^sub>2 y"
    5.26 +    and smult_assoc1:
    5.27 +      "[| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
    5.28 +      (a \<otimes> b) \<odot>\<^sub>2 x = a \<odot>\<^sub>2 (b \<odot>\<^sub>2 x)"
    5.29 +    and smult_one [simp]:
    5.30 +      "x \<in> carrier M ==> \<one> \<odot>\<^sub>2 x = x"
    5.31 +
    5.32 +locale algebra = module R M + cring M +
    5.33 +  assumes smult_assoc2:
    5.34 +      "[| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
    5.35 +      (a \<odot>\<^sub>2 x) \<otimes>\<^sub>2 y = a \<odot>\<^sub>2 (x \<otimes>\<^sub>2 y)"
    5.36 +
    5.37 +lemma moduleI:
    5.38 +  assumes cring: "cring R"
    5.39 +    and abelian_group: "abelian_group M"
    5.40 +    and smult_closed:
    5.41 +      "!!a x. [| a \<in> carrier R; x \<in> carrier M |] ==> smult M a x \<in> carrier M"
    5.42 +    and smult_l_distr:
    5.43 +      "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
    5.44 +      smult M (add R a b) x = add M (smult M a x) (smult M b x)"
    5.45 +    and smult_r_distr:
    5.46 +      "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
    5.47 +      smult M a (add M x y) = add M (smult M a x) (smult M a y)"
    5.48 +    and smult_assoc1:
    5.49 +      "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
    5.50 +      smult M (mult R a b) x = smult M a (smult M b x)"
    5.51 +    and smult_one:
    5.52 +      "!!x. x \<in> carrier M ==> smult M (one R) x = x"
    5.53 +  shows "module R M"
    5.54 +  by (auto intro: module.intro cring.axioms abelian_group.axioms
    5.55 +    module_axioms.intro prems)
    5.56 +
    5.57 +lemma algebraI:
    5.58 +  assumes R_cring: "cring R"
    5.59 +    and M_cring: "cring M"
    5.60 +    and smult_closed:
    5.61 +      "!!a x. [| a \<in> carrier R; x \<in> carrier M |] ==> smult M a x \<in> carrier M"
    5.62 +    and smult_l_distr:
    5.63 +      "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
    5.64 +      smult M (add R a b) x = add M (smult M a x) (smult M b x)"
    5.65 +    and smult_r_distr:
    5.66 +      "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
    5.67 +      smult M a (add M x y) = add M (smult M a x) (smult M a y)"
    5.68 +    and smult_assoc1:
    5.69 +      "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
    5.70 +      smult M (mult R a b) x = smult M a (smult M b x)"
    5.71 +    and smult_one:
    5.72 +      "!!x. x \<in> carrier M ==> smult M (one R) x = x"
    5.73 +    and smult_assoc2:
    5.74 +      "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
    5.75 +      mult M (smult M a x) y = smult M a (mult M x y)"
    5.76 +  shows "algebra R M"
    5.77 +  by (auto intro!: algebra.intro algebra_axioms.intro cring.axioms 
    5.78 +    module_axioms.intro prems)
    5.79 +
    5.80 +lemma (in algebra) R_cring:
    5.81 +  "cring R"
    5.82 +  by (rule cring.intro) assumption+
    5.83 +
    5.84 +lemma (in algebra) M_cring:
    5.85 +  "cring M"
    5.86 +  by (rule cring.intro) assumption+
    5.87 +
    5.88 +lemma (in algebra) module:
    5.89 +  "module R M"
    5.90 +  by (auto intro: moduleI R_cring is_abelian_group
    5.91 +    smult_l_distr smult_r_distr smult_assoc1)
    5.92 +
    5.93 +subsection {* Basic Properties of Algebras *}
    5.94 +
    5.95 +lemma (in algebra) smult_l_null [simp]:
    5.96 +  "x \<in> carrier M ==> \<zero> \<odot>\<^sub>2 x = \<zero>\<^sub>2"
    5.97 +proof -
    5.98 +  assume M: "x \<in> carrier M"
    5.99 +  note facts = M smult_closed
   5.100 +  from facts have "\<zero> \<odot>\<^sub>2 x = (\<zero> \<odot>\<^sub>2 x \<oplus>\<^sub>2 \<zero> \<odot>\<^sub>2 x) \<oplus>\<^sub>2 \<ominus>\<^sub>2 (\<zero> \<odot>\<^sub>2 x)" by algebra
   5.101 +  also from M have "... = (\<zero> \<oplus> \<zero>) \<odot>\<^sub>2 x \<oplus>\<^sub>2 \<ominus>\<^sub>2 (\<zero> \<odot>\<^sub>2 x)"
   5.102 +    by (simp add: smult_l_distr del: R.l_zero R.r_zero)
   5.103 +  also from facts have "... = \<zero>\<^sub>2" by algebra
   5.104 +  finally show ?thesis .
   5.105 +qed
   5.106 +
   5.107 +lemma (in algebra) smult_r_null [simp]:
   5.108 +  "a \<in> carrier R ==> a \<odot>\<^sub>2 \<zero>\<^sub>2 = \<zero>\<^sub>2";
   5.109 +proof -
   5.110 +  assume R: "a \<in> carrier R"
   5.111 +  note facts = R smult_closed
   5.112 +  from facts have "a \<odot>\<^sub>2 \<zero>\<^sub>2 = (a \<odot>\<^sub>2 \<zero>\<^sub>2 \<oplus>\<^sub>2 a \<odot>\<^sub>2 \<zero>\<^sub>2) \<oplus>\<^sub>2 \<ominus>\<^sub>2 (a \<odot>\<^sub>2 \<zero>\<^sub>2)"
   5.113 +    by algebra
   5.114 +  also from R have "... = a \<odot>\<^sub>2 (\<zero>\<^sub>2 \<oplus>\<^sub>2 \<zero>\<^sub>2) \<oplus>\<^sub>2 \<ominus>\<^sub>2 (a \<odot>\<^sub>2 \<zero>\<^sub>2)"
   5.115 +    by (simp add: smult_r_distr del: M.l_zero M.r_zero)
   5.116 +  also from facts have "... = \<zero>\<^sub>2" by algebra
   5.117 +  finally show ?thesis .
   5.118 +qed
   5.119 +
   5.120 +lemma (in algebra) smult_l_minus:
   5.121 +  "[| a \<in> carrier R; x \<in> carrier M |] ==> (\<ominus>a) \<odot>\<^sub>2 x = \<ominus>\<^sub>2 (a \<odot>\<^sub>2 x)"
   5.122 +proof -
   5.123 +  assume RM: "a \<in> carrier R" "x \<in> carrier M"
   5.124 +  note facts = RM smult_closed
   5.125 +  from facts have "(\<ominus>a) \<odot>\<^sub>2 x = (\<ominus>a \<odot>\<^sub>2 x \<oplus>\<^sub>2 a \<odot>\<^sub>2 x) \<oplus>\<^sub>2 \<ominus>\<^sub>2(a \<odot>\<^sub>2 x)" by algebra
   5.126 +  also from RM have "... = (\<ominus>a \<oplus> a) \<odot>\<^sub>2 x \<oplus>\<^sub>2 \<ominus>\<^sub>2(a \<odot>\<^sub>2 x)"
   5.127 +    by (simp add: smult_l_distr)
   5.128 +  also from facts smult_l_null have "... = \<ominus>\<^sub>2(a \<odot>\<^sub>2 x)" by algebra
   5.129 +  finally show ?thesis .
   5.130 +qed
   5.131 +
   5.132 +lemma (in algebra) smult_r_minus:
   5.133 +  "[| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^sub>2 (\<ominus>\<^sub>2x) = \<ominus>\<^sub>2 (a \<odot>\<^sub>2 x)"
   5.134 +proof -
   5.135 +  assume RM: "a \<in> carrier R" "x \<in> carrier M"
   5.136 +  note facts = RM smult_closed
   5.137 +  from facts have "a \<odot>\<^sub>2 (\<ominus>\<^sub>2x) = (a \<odot>\<^sub>2 \<ominus>\<^sub>2x \<oplus>\<^sub>2 a \<odot>\<^sub>2 x) \<oplus>\<^sub>2 \<ominus>\<^sub>2(a \<odot>\<^sub>2 x)"
   5.138 +    by algebra
   5.139 +  also from RM have "... = a \<odot>\<^sub>2 (\<ominus>\<^sub>2x \<oplus>\<^sub>2 x) \<oplus>\<^sub>2 \<ominus>\<^sub>2(a \<odot>\<^sub>2 x)"
   5.140 +    by (simp add: smult_r_distr)
   5.141 +  also from facts smult_r_null have "... = \<ominus>\<^sub>2(a \<odot>\<^sub>2 x)" by algebra
   5.142 +  finally show ?thesis .
   5.143 +qed
   5.144 +
   5.145 +subsection {* Every Abelian Group is a $\mathbb{Z}$-module *}
   5.146 +
   5.147 +text {* Not finished. *}
   5.148 +
   5.149 +constdefs
   5.150 +  INTEG :: "int ring"
   5.151 +  "INTEG == (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)"
   5.152 +
   5.153 +(*
   5.154 +  INTEG_MODULE :: "('a, 'm) ring_scheme => (int, 'a) module"
   5.155 +  "INTEG_MODULE R == (| carrier = carrier R, mult = mult R, one = one R,
   5.156 +    zero = zero R, add = add R, smult = (%n. %x:carrier R. ... ) |)"
   5.157 +*)
   5.158 +
   5.159 +lemma cring_INTEG:
   5.160 +  "cring INTEG"
   5.161 +  by (unfold INTEG_def) (auto intro!: cringI abelian_groupI comm_monoidI
   5.162 +    zadd_zminus_inverse2 zadd_zmult_distrib)
   5.163 +
   5.164 +end
     6.1 --- a/src/HOL/Algebra/ROOT.ML	Tue Apr 29 12:36:49 2003 +0200
     6.2 +++ b/src/HOL/Algebra/ROOT.ML	Wed Apr 30 10:01:35 2003 +0200
     6.3 @@ -1,9 +1,16 @@
     6.4  (*
     6.5 -    Polynomials
     6.6 +    The Isabelle Algebraic Library
     6.7      $Id$
     6.8      Author: Clemens Ballarin, started 24 September 1999
     6.9  *)
    6.10  
    6.11 +(* New development, based on explicit structures *)
    6.12 +
    6.13 +use_thy "Sylow";		(* Groups *)
    6.14 +(* use_thy "UnivPoly"; *)	(* Rings and polynomials *)
    6.15 +
    6.16 +(* Old development, based on axiomatic type classes.
    6.17 +   Will be withdrawn in future. *)
    6.18 +
    6.19  with_path "abstract" time_use_thy "Abstract";        (*The ring theory*)
    6.20  with_path "poly"     time_use_thy "Polynomial";      (*The full theory*)
    6.21 -use_thy "Sylow";
     7.1 --- a/src/HOL/Algebra/Summation.thy	Tue Apr 29 12:36:49 2003 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,500 +0,0 @@
     7.4 -(*  Title:      Summation Operator for Abelian Groups
     7.5 -    ID:         $Id$
     7.6 -    Author:     Clemens Ballarin, started 19 November 2002
     7.7 -
     7.8 -This file is largely based on HOL/Finite_Set.thy.
     7.9 -*)
    7.10 -
    7.11 -header {* Summation Operator *}
    7.12 -
    7.13 -theory Summation = Group:
    7.14 -
    7.15 -(* Instantiation of LC from Finite_Set.thy is not possible,
    7.16 -   because here we have explicit typing rules like x : carrier G.
    7.17 -   We introduce an explicit argument for the domain D *)
    7.18 -
    7.19 -consts
    7.20 -  foldSetD :: "['a set, 'b => 'a => 'a, 'a] => ('b set * 'a) set"
    7.21 -
    7.22 -inductive "foldSetD D f e"
    7.23 -  intros
    7.24 -    emptyI [intro]: "e : D ==> ({}, e) : foldSetD D f e"
    7.25 -    insertI [intro]: "[| x ~: A; f x y : D; (A, y) : foldSetD D f e |] ==>
    7.26 -                      (insert x A, f x y) : foldSetD D f e"
    7.27 -
    7.28 -inductive_cases empty_foldSetDE [elim!]: "({}, x) : foldSetD D f e"
    7.29 -
    7.30 -constdefs
    7.31 -  foldD :: "['a set, 'b => 'a => 'a, 'a, 'b set] => 'a"
    7.32 -  "foldD D f e A == THE x. (A, x) : foldSetD D f e"
    7.33 -
    7.34 -lemma foldSetD_closed:
    7.35 -  "[| (A, z) : foldSetD D f e ; e : D; !!x y. [| x : A; y : D |] ==> f x y : D 
    7.36 -      |] ==> z : D";
    7.37 -  by (erule foldSetD.elims) auto
    7.38 -
    7.39 -lemma Diff1_foldSetD:
    7.40 -  "[| (A - {x}, y) : foldSetD D f e; x : A; f x y : D |] ==>
    7.41 -   (A, f x y) : foldSetD D f e"
    7.42 -  apply (erule insert_Diff [THEN subst], rule foldSetD.intros)
    7.43 -   apply auto
    7.44 -  done
    7.45 -
    7.46 -lemma foldSetD_imp_finite [simp]: "(A, x) : foldSetD D f e ==> finite A"
    7.47 -  by (induct set: foldSetD) auto
    7.48 -
    7.49 -lemma finite_imp_foldSetD:
    7.50 -  "[| finite A; e : D; !!x y. [| x : A; y : D |] ==> f x y : D |] ==>
    7.51 -   EX x. (A, x) : foldSetD D f e"
    7.52 -proof (induct set: Finites)
    7.53 -  case empty then show ?case by auto
    7.54 -next
    7.55 -  case (insert F x)
    7.56 -  then obtain y where y: "(F, y) : foldSetD D f e" by auto
    7.57 -  with insert have "y : D" by (auto dest: foldSetD_closed)
    7.58 -  with y and insert have "(insert x F, f x y) : foldSetD D f e"
    7.59 -    by (intro foldSetD.intros) auto
    7.60 -  then show ?case ..
    7.61 -qed
    7.62 -
    7.63 -subsection {* Left-commutative operations *}
    7.64 -
    7.65 -locale LCD =
    7.66 -  fixes B :: "'b set"
    7.67 -  and D :: "'a set"
    7.68 -  and f :: "'b => 'a => 'a"    (infixl "\<cdot>" 70)
    7.69 -  assumes left_commute: "[| x : B; y : B; z : D |] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
    7.70 -  and f_closed [simp, intro!]: "!!x y. [| x : B; y : D |] ==> f x y : D"
    7.71 -
    7.72 -lemma (in LCD) foldSetD_closed [dest]:
    7.73 -  "(A, z) : foldSetD D f e ==> z : D";
    7.74 -  by (erule foldSetD.elims) auto
    7.75 -
    7.76 -lemma (in LCD) Diff1_foldSetD:
    7.77 -  "[| (A - {x}, y) : foldSetD D f e; x : A; A <= B |] ==>
    7.78 -   (A, f x y) : foldSetD D f e"
    7.79 -  apply (subgoal_tac "x : B")
    7.80 -  prefer 2 apply fast
    7.81 -  apply (erule insert_Diff [THEN subst], rule foldSetD.intros)
    7.82 -   apply auto
    7.83 -  done
    7.84 -
    7.85 -lemma (in LCD) foldSetD_imp_finite [simp]:
    7.86 -  "(A, x) : foldSetD D f e ==> finite A"
    7.87 -  by (induct set: foldSetD) auto
    7.88 -
    7.89 -lemma (in LCD) finite_imp_foldSetD:
    7.90 -  "[| finite A; A <= B; e : D |] ==> EX x. (A, x) : foldSetD D f e"
    7.91 -proof (induct set: Finites)
    7.92 -  case empty then show ?case by auto
    7.93 -next
    7.94 -  case (insert F x)
    7.95 -  then obtain y where y: "(F, y) : foldSetD D f e" by auto
    7.96 -  with insert have "y : D" by auto
    7.97 -  with y and insert have "(insert x F, f x y) : foldSetD D f e"
    7.98 -    by (intro foldSetD.intros) auto
    7.99 -  then show ?case ..
   7.100 -qed
   7.101 -
   7.102 -lemma (in LCD) foldSetD_determ_aux:
   7.103 -  "e : D ==> ALL A x. A <= B & card A < n --> (A, x) : foldSetD D f e -->
   7.104 -    (ALL y. (A, y) : foldSetD D f e --> y = x)"
   7.105 -  apply (induct n)
   7.106 -   apply (auto simp add: less_Suc_eq)
   7.107 -  apply (erule foldSetD.cases)
   7.108 -   apply blast
   7.109 -  apply (erule foldSetD.cases)
   7.110 -   apply blast
   7.111 -  apply clarify
   7.112 -  txt {* force simplification of @{text "card A < card (insert ...)"}. *}
   7.113 -  apply (erule rev_mp)
   7.114 -  apply (simp add: less_Suc_eq_le)
   7.115 -  apply (rule impI)
   7.116 -  apply (rename_tac Aa xa ya Ab xb yb, case_tac "xa = xb")
   7.117 -   apply (subgoal_tac "Aa = Ab")
   7.118 -    prefer 2 apply (blast elim!: equalityE)
   7.119 -   apply blast
   7.120 -  txt {* case @{prop "xa \<notin> xb"}. *}
   7.121 -  apply (subgoal_tac "Aa - {xb} = Ab - {xa} & xb : Aa & xa : Ab")
   7.122 -   prefer 2 apply (blast elim!: equalityE)
   7.123 -  apply clarify
   7.124 -  apply (subgoal_tac "Aa = insert xb Ab - {xa}")
   7.125 -   prefer 2 apply blast
   7.126 -  apply (subgoal_tac "card Aa <= card Ab")
   7.127 -   prefer 2
   7.128 -   apply (rule Suc_le_mono [THEN subst])
   7.129 -   apply (simp add: card_Suc_Diff1)
   7.130 -  apply (rule_tac A1 = "Aa - {xb}" in finite_imp_foldSetD [THEN exE])
   7.131 -  apply (blast intro: foldSetD_imp_finite finite_Diff)
   7.132 -(* new subgoal from finite_imp_foldSetD *)
   7.133 -    apply best (* blast doesn't seem to solve this *)
   7.134 -   apply assumption
   7.135 -  apply (frule (1) Diff1_foldSetD)
   7.136 -(* new subgoal from Diff1_foldSetD *)
   7.137 -    apply best
   7.138 -(*
   7.139 -apply (best del: foldSetD_closed elim: foldSetD_closed)
   7.140 -    apply (rule f_closed) apply assumption apply (rule foldSetD_closed)
   7.141 -    prefer 3 apply assumption apply (rule e_closed)
   7.142 -    apply (rule f_closed) apply force apply assumption
   7.143 -*)
   7.144 -  apply (subgoal_tac "ya = f xb x")
   7.145 -   prefer 2
   7.146 -(* new subgoal to make IH applicable *) 
   7.147 -  apply (subgoal_tac "Aa <= B")
   7.148 -   prefer 2 apply best
   7.149 -   apply (blast del: equalityCE)
   7.150 -  apply (subgoal_tac "(Ab - {xa}, x) : foldSetD D f e")
   7.151 -   prefer 2 apply simp
   7.152 -  apply (subgoal_tac "yb = f xa x")
   7.153 -   prefer 2 
   7.154 -(*   apply (drule_tac x = xa in Diff1_foldSetD)
   7.155 -     apply assumption
   7.156 -     apply (rule f_closed) apply best apply (rule foldSetD_closed)
   7.157 -     prefer 3 apply assumption apply (rule e_closed)
   7.158 -     apply (rule f_closed) apply best apply assumption
   7.159 -*)
   7.160 -   apply (blast del: equalityCE dest: Diff1_foldSetD)
   7.161 -   apply (simp (no_asm_simp))
   7.162 -   apply (rule left_commute)
   7.163 -   apply assumption apply best apply best
   7.164 - done
   7.165 -
   7.166 -lemma (in LCD) foldSetD_determ:
   7.167 -  "[| (A, x) : foldSetD D f e; (A, y) : foldSetD D f e; e : D; A <= B |]
   7.168 -   ==> y = x"
   7.169 -  by (blast intro: foldSetD_determ_aux [rule_format])
   7.170 -
   7.171 -lemma (in LCD) foldD_equality:
   7.172 -  "[| (A, y) : foldSetD D f e; e : D; A <= B |] ==> foldD D f e A = y"
   7.173 -  by (unfold foldD_def) (blast intro: foldSetD_determ)
   7.174 -
   7.175 -lemma foldD_empty [simp]:
   7.176 -  "e : D ==> foldD D f e {} = e"
   7.177 -  by (unfold foldD_def) blast
   7.178 -
   7.179 -lemma (in LCD) foldD_insert_aux:
   7.180 -  "[| x ~: A; x : B; e : D; A <= B |] ==>
   7.181 -    ((insert x A, v) : foldSetD D f e) =
   7.182 -    (EX y. (A, y) : foldSetD D f e & v = f x y)"
   7.183 -  apply auto
   7.184 -  apply (rule_tac A1 = A in finite_imp_foldSetD [THEN exE])
   7.185 -   apply (fastsimp dest: foldSetD_imp_finite)
   7.186 -(* new subgoal by finite_imp_foldSetD *)
   7.187 -    apply assumption
   7.188 -    apply assumption
   7.189 -  apply (blast intro: foldSetD_determ)
   7.190 -  done
   7.191 -
   7.192 -lemma (in LCD) foldD_insert:
   7.193 -    "[| finite A; x ~: A; x : B; e : D; A <= B |] ==>
   7.194 -     foldD D f e (insert x A) = f x (foldD D f e A)"
   7.195 -  apply (unfold foldD_def)
   7.196 -  apply (simp add: foldD_insert_aux)
   7.197 -  apply (rule the_equality)
   7.198 -  apply (auto intro: finite_imp_foldSetD
   7.199 -    cong add: conj_cong simp add: foldD_def [symmetric] foldD_equality)
   7.200 -  done
   7.201 -
   7.202 -lemma (in LCD) foldD_closed [simp]:
   7.203 -  "[| finite A; e : D; A <= B |] ==> foldD D f e A : D"
   7.204 -proof (induct set: Finites)
   7.205 -  case empty then show ?case by (simp add: foldD_empty)
   7.206 -next
   7.207 -  case insert then show ?case by (simp add: foldD_insert)
   7.208 -qed
   7.209 -
   7.210 -lemma (in LCD) foldD_commute:
   7.211 -  "[| finite A; x : B; e : D; A <= B |] ==>
   7.212 -   f x (foldD D f e A) = foldD D f (f x e) A"
   7.213 -  apply (induct set: Finites)
   7.214 -   apply simp
   7.215 -  apply (auto simp add: left_commute foldD_insert)
   7.216 -  done
   7.217 -
   7.218 -lemma Int_mono2:
   7.219 -  "[| A <= C; B <= C |] ==> A Int B <= C"
   7.220 -  by blast
   7.221 -
   7.222 -lemma (in LCD) foldD_nest_Un_Int:
   7.223 -  "[| finite A; finite C; e : D; A <= B; C <= B |] ==>
   7.224 -   foldD D f (foldD D f e C) A = foldD D f (foldD D f e (A Int C)) (A Un C)"
   7.225 -  apply (induct set: Finites)
   7.226 -   apply simp
   7.227 -  apply (simp add: foldD_insert foldD_commute Int_insert_left insert_absorb
   7.228 -    Int_mono2 Un_subset_iff)
   7.229 -  done
   7.230 -
   7.231 -lemma (in LCD) foldD_nest_Un_disjoint:
   7.232 -  "[| finite A; finite B; A Int B = {}; e : D; A <= B; C <= B |]
   7.233 -    ==> foldD D f e (A Un B) = foldD D f (foldD D f e B) A"
   7.234 -  by (simp add: foldD_nest_Un_Int)
   7.235 -
   7.236 --- {* Delete rules to do with @{text foldSetD} relation. *}
   7.237 -
   7.238 -declare foldSetD_imp_finite [simp del]
   7.239 -  empty_foldSetDE [rule del]
   7.240 -  foldSetD.intros [rule del]
   7.241 -declare (in LCD)
   7.242 -  foldSetD_closed [rule del]
   7.243 -
   7.244 -subsection {* Commutative monoids *}
   7.245 -
   7.246 -text {*
   7.247 -  We enter a more restrictive context, with @{text "f :: 'a => 'a => 'a"}
   7.248 -  instead of @{text "'b => 'a => 'a"}.
   7.249 -*}
   7.250 -
   7.251 -locale ACeD =
   7.252 -  fixes D :: "'a set"
   7.253 -    and f :: "'a => 'a => 'a"    (infixl "\<cdot>" 70)
   7.254 -    and e :: 'a
   7.255 -  assumes ident [simp]: "x : D ==> x \<cdot> e = x"
   7.256 -    and commute: "[| x : D; y : D |] ==> x \<cdot> y = y \<cdot> x"
   7.257 -    and assoc: "[| x : D; y : D; z : D |] ==> (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
   7.258 -    and e_closed [simp]: "e : D"
   7.259 -    and f_closed [simp]: "[| x : D; y : D |] ==> x \<cdot> y : D"
   7.260 -
   7.261 -lemma (in ACeD) left_commute:
   7.262 -  "[| x : D; y : D; z : D |] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
   7.263 -proof -
   7.264 -  assume D: "x : D" "y : D" "z : D"
   7.265 -  then have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp add: commute)
   7.266 -  also from D have "... = y \<cdot> (z \<cdot> x)" by (simp add: assoc)
   7.267 -  also from D have "z \<cdot> x = x \<cdot> z" by (simp add: commute)
   7.268 -  finally show ?thesis .
   7.269 -qed
   7.270 -
   7.271 -lemmas (in ACeD) AC = assoc commute left_commute
   7.272 -
   7.273 -lemma (in ACeD) left_ident [simp]: "x : D ==> e \<cdot> x = x"
   7.274 -proof -
   7.275 -  assume D: "x : D"
   7.276 -  have "x \<cdot> e = x" by (rule ident)
   7.277 -  with D show ?thesis by (simp add: commute)
   7.278 -qed
   7.279 -
   7.280 -lemma (in ACeD) foldD_Un_Int:
   7.281 -  "[| finite A; finite B; A <= D; B <= D |] ==>
   7.282 -    foldD D f e A \<cdot> foldD D f e B =
   7.283 -    foldD D f e (A Un B) \<cdot> foldD D f e (A Int B)"
   7.284 -  apply (induct set: Finites)
   7.285 -   apply (simp add: left_commute LCD.foldD_closed [OF LCD.intro [of D]])
   7.286 -(* left_commute is required to show premise of LCD.intro *)
   7.287 -  apply (simp add: AC insert_absorb Int_insert_left
   7.288 -    LCD.foldD_insert [OF LCD.intro [of D]]
   7.289 -    LCD.foldD_closed [OF LCD.intro [of D]]
   7.290 -    Int_mono2 Un_subset_iff)
   7.291 -  done
   7.292 -
   7.293 -lemma (in ACeD) foldD_Un_disjoint:
   7.294 -  "[| finite A; finite B; A Int B = {}; A <= D; B <= D |] ==>
   7.295 -    foldD D f e (A Un B) = foldD D f e A \<cdot> foldD D f e B"
   7.296 -  by (simp add: foldD_Un_Int
   7.297 -    left_commute LCD.foldD_closed [OF LCD.intro [of D]] Un_subset_iff)
   7.298 -
   7.299 -subsection {* Products over Finite Sets *}
   7.300 -
   7.301 -constdefs
   7.302 -  finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b"
   7.303 -  "finprod G f A == if finite A
   7.304 -      then foldD (carrier G) (mult G o f) (one G) A
   7.305 -      else arbitrary"
   7.306 -
   7.307 -(*
   7.308 -locale finite_prod = abelian_monoid + var prod +
   7.309 -  defines "prod == (%f A. if finite A
   7.310 -      then foldD (carrier G) (op \<otimes> o f) \<one> A
   7.311 -      else arbitrary)"
   7.312 -*)
   7.313 -(* TODO: nice syntax for the summation operator inside the locale
   7.314 -   like \<Otimes>\<index> i\<in>A. f i, probably needs hand-coded translation *)
   7.315 -
   7.316 -ML_setup {* 
   7.317 -
   7.318 -Context.>> (fn thy => (simpset_ref_of thy :=
   7.319 -  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
   7.320 -
   7.321 -lemma (in abelian_monoid) finprod_empty [simp]: 
   7.322 -  "finprod G f {} = \<one>"
   7.323 -  by (simp add: finprod_def)
   7.324 -
   7.325 -ML_setup {* 
   7.326 -
   7.327 -Context.>> (fn thy => (simpset_ref_of thy :=
   7.328 -  simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
   7.329 -
   7.330 -declare funcsetI [intro]
   7.331 -  funcset_mem [dest]
   7.332 -
   7.333 -lemma (in abelian_monoid) finprod_insert [simp]:
   7.334 -  "[| finite F; a \<notin> F; f \<in> F -> carrier G; f a \<in> carrier G |] ==>
   7.335 -   finprod G f (insert a F) = f a \<otimes> finprod G f F"
   7.336 -  apply (rule trans)
   7.337 -  apply (simp add: finprod_def)
   7.338 -  apply (rule trans)
   7.339 -  apply (rule LCD.foldD_insert [OF LCD.intro [of "insert a F"]])
   7.340 -    apply simp
   7.341 -    apply (rule m_lcomm)
   7.342 -      apply fast apply fast apply assumption
   7.343 -    apply (fastsimp intro: m_closed)
   7.344 -    apply simp+ apply fast
   7.345 -  apply (auto simp add: finprod_def)
   7.346 -  done
   7.347 -
   7.348 -lemma (in abelian_monoid) finprod_one:
   7.349 -  "finite A ==> finprod G (%i. \<one>) A = \<one>"
   7.350 -proof (induct set: Finites)
   7.351 -  case empty show ?case by simp
   7.352 -next
   7.353 -  case (insert A a)
   7.354 -  have "(%i. \<one>) \<in> A -> carrier G" by auto
   7.355 -  with insert show ?case by simp
   7.356 -qed
   7.357 -
   7.358 -lemma (in abelian_monoid) finprod_closed [simp]:
   7.359 -  fixes A
   7.360 -  assumes fin: "finite A" and f: "f \<in> A -> carrier G" 
   7.361 -  shows "finprod G f A \<in> carrier G"
   7.362 -using fin f
   7.363 -proof induct
   7.364 -  case empty show ?case by simp
   7.365 -next
   7.366 -  case (insert A a)
   7.367 -  then have a: "f a \<in> carrier G" by fast
   7.368 -  from insert have A: "f \<in> A -> carrier G" by fast
   7.369 -  from insert A a show ?case by simp
   7.370 -qed
   7.371 -
   7.372 -lemma funcset_Int_left [simp, intro]:
   7.373 -  "[| f \<in> A -> C; f \<in> B -> C |] ==> f \<in> A Int B -> C"
   7.374 -  by fast
   7.375 -
   7.376 -lemma funcset_Un_left [iff]:
   7.377 -  "(f \<in> A Un B -> C) = (f \<in> A -> C & f \<in> B -> C)"
   7.378 -  by fast
   7.379 -
   7.380 -lemma (in abelian_monoid) finprod_Un_Int:
   7.381 -  "[| finite A; finite B; g \<in> A -> carrier G; g \<in> B -> carrier G |] ==>
   7.382 -     finprod G g (A Un B) \<otimes> finprod G g (A Int B) =
   7.383 -     finprod G g A \<otimes> finprod G g B"
   7.384 -  -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
   7.385 -proof (induct set: Finites)
   7.386 -  case empty then show ?case by (simp add: finprod_closed)
   7.387 -next
   7.388 -  case (insert A a)
   7.389 -  then have a: "g a \<in> carrier G" by fast
   7.390 -  from insert have A: "g \<in> A -> carrier G" by fast
   7.391 -  from insert A a show ?case
   7.392 -    by (simp add: ac Int_insert_left insert_absorb finprod_closed
   7.393 -          Int_mono2 Un_subset_iff) 
   7.394 -qed
   7.395 -
   7.396 -lemma (in abelian_monoid) finprod_Un_disjoint:
   7.397 -  "[| finite A; finite B; A Int B = {};
   7.398 -      g \<in> A -> carrier G; g \<in> B -> carrier G |]
   7.399 -   ==> finprod G g (A Un B) = finprod G g A \<otimes> finprod G g B"
   7.400 -  apply (subst finprod_Un_Int [symmetric])
   7.401 -    apply (auto simp add: finprod_closed)
   7.402 -  done
   7.403 -
   7.404 -lemma (in abelian_monoid) finprod_multf:
   7.405 -  "[| finite A; f \<in> A -> carrier G; g \<in> A -> carrier G |] ==>
   7.406 -   finprod G (%x. f x \<otimes> g x) A = (finprod G f A \<otimes> finprod G g A)"
   7.407 -proof (induct set: Finites)
   7.408 -  case empty show ?case by simp
   7.409 -next
   7.410 -  case (insert A a) then
   7.411 -  have fA: "f : A -> carrier G" by fast
   7.412 -  from insert have fa: "f a : carrier G" by fast
   7.413 -  from insert have gA: "g : A -> carrier G" by fast
   7.414 -  from insert have ga: "g a : carrier G" by fast
   7.415 -  from insert have fga: "(%x. f x \<otimes> g x) a : carrier G" by (simp add: Pi_def)
   7.416 -  from insert have fgA: "(%x. f x \<otimes> g x) : A -> carrier G"
   7.417 -    by (simp add: Pi_def)
   7.418 -  show ?case  (* check if all simps are really necessary *)
   7.419 -    by (simp add: insert fA fa gA ga fgA fga ac finprod_closed Int_insert_left insert_absorb Int_mono2 Un_subset_iff)
   7.420 -qed
   7.421 -
   7.422 -lemma (in abelian_monoid) finprod_cong':
   7.423 -  "[| A = B; g : B -> carrier G;
   7.424 -      !!i. i : B ==> f i = g i |] ==> finprod G f A = finprod G g B"
   7.425 -proof -
   7.426 -  assume prems: "A = B" "g : B -> carrier G"
   7.427 -    "!!i. i : B ==> f i = g i"
   7.428 -  show ?thesis
   7.429 -  proof (cases "finite B")
   7.430 -    case True
   7.431 -    then have "!!A. [| A = B; g : B -> carrier G;
   7.432 -      !!i. i : B ==> f i = g i |] ==> finprod G f A = finprod G g B"
   7.433 -    proof induct
   7.434 -      case empty thus ?case by simp
   7.435 -    next
   7.436 -      case (insert B x)
   7.437 -      then have "finprod G f A = finprod G f (insert x B)" by simp
   7.438 -      also from insert have "... = f x \<otimes> finprod G f B"
   7.439 -      proof (intro finprod_insert)
   7.440 -	show "finite B" .
   7.441 -      next
   7.442 -	show "x ~: B" .
   7.443 -      next
   7.444 -	assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
   7.445 -	  "g \<in> insert x B \<rightarrow> carrier G"
   7.446 -	thus "f : B -> carrier G" by fastsimp
   7.447 -      next
   7.448 -	assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
   7.449 -	  "g \<in> insert x B \<rightarrow> carrier G"
   7.450 -	thus "f x \<in> carrier G" by fastsimp
   7.451 -      qed
   7.452 -      also from insert have "... = g x \<otimes> finprod G g B" by fastsimp
   7.453 -      also from insert have "... = finprod G g (insert x B)"
   7.454 -      by (intro finprod_insert [THEN sym]) auto
   7.455 -      finally show ?case .
   7.456 -    qed
   7.457 -    with prems show ?thesis by simp
   7.458 -  next
   7.459 -    case False with prems show ?thesis by (simp add: finprod_def)
   7.460 -  qed
   7.461 -qed
   7.462 -
   7.463 -lemma (in abelian_monoid) finprod_cong:
   7.464 -  "[| A = B; !!i. i : B ==> f i = g i;
   7.465 -      g : B -> carrier G = True |] ==> finprod G f A = finprod G g B"
   7.466 -  by (rule finprod_cong') fast+
   7.467 -
   7.468 -text {*Usually, if this rule causes a failed congruence proof error,
   7.469 -  the reason is that the premise @{text "g : B -> carrier G"} cannot be shown.
   7.470 -  Adding @{thm [source] Pi_def} to the simpset is often useful.
   7.471 -  For this reason, @{thm [source] abelian_monoid.finprod_cong}
   7.472 -  is not added to the simpset by default.
   7.473 -*}
   7.474 -
   7.475 -declare funcsetI [rule del]
   7.476 -  funcset_mem [rule del]
   7.477 -
   7.478 -lemma (in abelian_monoid) finprod_0 [simp]:
   7.479 -  "f : {0::nat} -> carrier G ==> finprod G f {..0} = f 0"
   7.480 -by (simp add: Pi_def)
   7.481 -
   7.482 -lemma (in abelian_monoid) finprod_Suc [simp]:
   7.483 -  "f : {..Suc n} -> carrier G ==>
   7.484 -   finprod G f {..Suc n} = (f (Suc n) \<otimes> finprod G f {..n})"
   7.485 -by (simp add: Pi_def atMost_Suc)
   7.486 -
   7.487 -lemma (in abelian_monoid) finprod_Suc2:
   7.488 -  "f : {..Suc n} -> carrier G ==>
   7.489 -   finprod G f {..Suc n} = (finprod G (%i. f (Suc i)) {..n} \<otimes> f 0)"
   7.490 -proof (induct n)
   7.491 -  case 0 thus ?case by (simp add: Pi_def)
   7.492 -next
   7.493 -  case Suc thus ?case by (simp add: m_assoc Pi_def finprod_closed)
   7.494 -qed
   7.495 -
   7.496 -lemma (in abelian_monoid) finprod_mult [simp]:
   7.497 -  "[| f : {..n} -> carrier G; g : {..n} -> carrier G |] ==>
   7.498 -     finprod G (%i. f i \<otimes> g i) {..n::nat} =
   7.499 -     finprod G f {..n} \<otimes> finprod G g {..n}"
   7.500 -  by (induct n) (simp_all add: ac Pi_def finprod_closed)
   7.501 -
   7.502 -end
   7.503 -
     8.1 --- a/src/HOL/Algebra/poly/PolyHomo.thy	Tue Apr 29 12:36:49 2003 +0200
     8.2 +++ b/src/HOL/Algebra/poly/PolyHomo.thy	Wed Apr 30 10:01:35 2003 +0200
     8.3 @@ -4,7 +4,7 @@
     8.4      Author: Clemens Ballarin, started 15 April 1997
     8.5  *)
     8.6  
     8.7 -PolyHomo = UnivPoly +
     8.8 +PolyHomo = UnivPoly2 +
     8.9  
    8.10  consts
    8.11    EVAL2	:: "['a::ring => 'b, 'b, 'a up] => 'b::ring"
     9.1 --- a/src/HOL/Algebra/poly/UnivPoly.ML	Tue Apr 29 12:36:49 2003 +0200
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,359 +0,0 @@
     9.4 -(*
     9.5 -    Degree of polynomials
     9.6 -    $Id$
     9.7 -    written by Clemens Ballarin, started 22 January 1997
     9.8 -*)
     9.9 -
    9.10 -(*
    9.11 -(* Relating degree and bound *)
    9.12 -
    9.13 -Goal "[| bound m f; f n ~= 0 |] ==> n <= m";
    9.14 -by (force_tac (claset() addDs [inst "m" "n" boundD], 
    9.15 -               simpset()) 1); 
    9.16 -qed "below_bound";
    9.17 -
    9.18 -goal UnivPoly.thy "bound (LEAST n. bound n (Rep_UP p)) (Rep_UP p)";
    9.19 -by (rtac exE 1);
    9.20 -by (rtac LeastI 2);
    9.21 -by (assume_tac 2);
    9.22 -by (res_inst_tac [("a", "Rep_UP p")] CollectD 1);
    9.23 -by (rtac (rewrite_rule [UP_def] Rep_UP) 1);
    9.24 -qed "Least_is_bound";
    9.25 -
    9.26 -Goalw [coeff_def, deg_def]
    9.27 -  "!! p. ALL m. n < m --> coeff m p = 0 ==> deg p <= n";
    9.28 -by (rtac Least_le 1);
    9.29 -by (Fast_tac 1);
    9.30 -qed "deg_aboveI";
    9.31 -
    9.32 -Goalw [coeff_def, deg_def]
    9.33 -  "(n ~= 0 --> coeff n p ~= 0) ==> n <= deg p";
    9.34 -by (case_tac "n = 0" 1);
    9.35 -(* Case n=0 *)
    9.36 -by (Asm_simp_tac 1);
    9.37 -(* Case n~=0 *)
    9.38 -by (rotate_tac 1 1);
    9.39 -by (Asm_full_simp_tac 1);
    9.40 -by (rtac below_bound 1);
    9.41 -by (assume_tac 2);
    9.42 -by (rtac Least_is_bound 1);
    9.43 -qed "deg_belowI";
    9.44 -
    9.45 -Goalw [coeff_def, deg_def]
    9.46 -  "deg p < m ==> coeff m p = 0";
    9.47 -by (rtac exE 1); (* create !! x. *)
    9.48 -by (rtac boundD 2);
    9.49 -by (assume_tac 3);
    9.50 -by (rtac LeastI 2);
    9.51 -by (assume_tac 2);
    9.52 -by (res_inst_tac [("a", "Rep_UP p")] CollectD 1);
    9.53 -by (rtac (rewrite_rule [UP_def] Rep_UP) 1);
    9.54 -qed "deg_aboveD";
    9.55 -
    9.56 -Goalw [deg_def]
    9.57 -  "deg p = Suc y ==> ~ bound y (Rep_UP p)";
    9.58 -by (rtac not_less_Least 1);
    9.59 -by (Asm_simp_tac 1);
    9.60 -val lemma1 = result();
    9.61 -
    9.62 -Goalw [deg_def, coeff_def]
    9.63 -  "deg p = Suc y ==> coeff (deg p) p ~= 0";
    9.64 -by (rtac ccontr 1);
    9.65 -by (dtac notnotD 1);
    9.66 -by (cut_inst_tac [("p", "p")] Least_is_bound 1);
    9.67 -by (subgoal_tac "bound y (Rep_UP p)" 1);
    9.68 -(* prove subgoal *)
    9.69 -by (rtac boundI 2);  
    9.70 -by (case_tac "Suc y < m" 2);
    9.71 -(* first case *)
    9.72 -by (rtac boundD 2);  
    9.73 -by (assume_tac 2);
    9.74 -by (Asm_simp_tac 2);
    9.75 -(* second case *)
    9.76 -by (dtac leI 2);
    9.77 -by (dtac Suc_leI 2);
    9.78 -by (dtac le_anti_sym 2);
    9.79 -by (assume_tac 2);
    9.80 -by (Asm_full_simp_tac 2);
    9.81 -(* end prove subgoal *)
    9.82 -by (fold_goals_tac [deg_def]);
    9.83 -by (dtac lemma1 1);
    9.84 -by (etac notE 1);
    9.85 -by (assume_tac 1);
    9.86 -val lemma2 = result();
    9.87 -
    9.88 -Goal "deg p ~= 0 ==> coeff (deg p) p ~= 0";
    9.89 -by (rtac lemma2 1);
    9.90 -by (Full_simp_tac 1);
    9.91 -by (dtac Suc_pred 1);
    9.92 -by (rtac sym 1);
    9.93 -by (Asm_simp_tac 1);
    9.94 -qed "deg_lcoeff";
    9.95 -
    9.96 -Goal "p ~= 0 ==> coeff (deg p) p ~= 0";
    9.97 -by (etac contrapos_np 1); 
    9.98 -by (case_tac "deg p = 0" 1);
    9.99 -by (blast_tac (claset() addSDs [deg_lcoeff]) 2); 
   9.100 -by (rtac up_eqI 1);
   9.101 -by (case_tac "n=0" 1);
   9.102 -by (rotate_tac ~2 1);
   9.103 -by (Asm_full_simp_tac 1);
   9.104 -by (asm_full_simp_tac (simpset() addsimps [deg_aboveD]) 1);
   9.105 -qed "nonzero_lcoeff";
   9.106 -
   9.107 -Goal "(deg p <= n) = bound n (Rep_UP p)";
   9.108 -by (rtac iffI 1);
   9.109 -(* ==> *)
   9.110 -by (rtac boundI 1);
   9.111 -by (fold_goals_tac [coeff_def]);
   9.112 -by (rtac deg_aboveD 1);
   9.113 -by (fast_arith_tac 1);
   9.114 -(* <== *)
   9.115 -by (rtac deg_aboveI 1);
   9.116 -by (rewtac coeff_def);
   9.117 -by (Fast_tac 1);
   9.118 -qed "deg_above_is_bound";
   9.119 -
   9.120 -(* Lemmas on the degree function *)
   9.121 -
   9.122 -Goalw [max_def]
   9.123 -  "!! p::'a::ring up. deg (p + q) <= max (deg p) (deg q)";
   9.124 -by (case_tac "deg p <= deg q" 1);
   9.125 -(* case deg p <= deg q *)
   9.126 -by (rtac deg_aboveI 1);
   9.127 -by (Asm_simp_tac 1);
   9.128 -by (strip_tac 1);
   9.129 -by (dtac le_less_trans 1);
   9.130 -by (assume_tac 1);
   9.131 -by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
   9.132 -(* case deg p > deg q *)
   9.133 -by (rtac deg_aboveI 1);
   9.134 -by (Asm_simp_tac 1);
   9.135 -by (dtac not_leE 1);
   9.136 -by (strip_tac 1);
   9.137 -by (dtac less_trans 1);
   9.138 -by (assume_tac 1);
   9.139 -by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
   9.140 -qed "deg_add";
   9.141 -
   9.142 -Goal "!!p::('a::ring up). deg p < deg q ==> deg (p + q) = deg q";
   9.143 -by (rtac order_antisym 1);
   9.144 -by (rtac le_trans 1);
   9.145 -by (rtac deg_add 1);
   9.146 -by (Asm_simp_tac 1);
   9.147 -by (rtac deg_belowI 1);
   9.148 -by (asm_simp_tac (simpset() addsimps [deg_aboveD, deg_lcoeff]) 1);
   9.149 -qed "deg_add_equal";
   9.150 -
   9.151 -Goal "deg (monom m::'a::ring up) <= m";
   9.152 -by (asm_simp_tac 
   9.153 -  (simpset() addsimps [deg_aboveI, less_not_refl2 RS not_sym]) 1);
   9.154 -qed "deg_monom_ring";
   9.155 -
   9.156 -Goal "deg (monom m::'a::domain up) = m";
   9.157 -by (rtac le_anti_sym 1);
   9.158 -(* <= *)
   9.159 -by (rtac deg_monom_ring 1);
   9.160 -(* >= *)
   9.161 -by (asm_simp_tac 
   9.162 -  (simpset() addsimps [deg_belowI, less_not_refl2 RS not_sym]) 1);
   9.163 -qed "deg_monom";
   9.164 -
   9.165 -Goal "!! a::'a::ring. deg (const a) = 0";
   9.166 -by (rtac le_anti_sym 1);
   9.167 -by (rtac deg_aboveI 1);
   9.168 -by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
   9.169 -by (rtac deg_belowI 1);
   9.170 -by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
   9.171 -qed "deg_const";
   9.172 -
   9.173 -Goal "deg (0::'a::ringS up) = 0";
   9.174 -by (rtac le_anti_sym 1);
   9.175 -by (rtac deg_aboveI 1);
   9.176 -by (Simp_tac 1);
   9.177 -by (rtac deg_belowI 1);
   9.178 -by (Simp_tac 1);
   9.179 -qed "deg_zero";
   9.180 -
   9.181 -Goal "deg (<1>::'a::ring up) = 0";
   9.182 -by (rtac le_anti_sym 1);
   9.183 -by (rtac deg_aboveI 1);
   9.184 -by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
   9.185 -by (rtac deg_belowI 1);
   9.186 -by (Simp_tac 1);
   9.187 -qed "deg_one";
   9.188 -
   9.189 -Goal "!!p::('a::ring) up. deg (-p) = deg p";
   9.190 -by (rtac le_anti_sym 1);
   9.191 -(* <= *)
   9.192 -by (simp_tac (simpset() addsimps [deg_aboveI, deg_aboveD]) 1);
   9.193 -by (simp_tac (simpset() addsimps [deg_belowI, deg_lcoeff, uminus_monom_neq]) 1);
   9.194 -qed "deg_uminus";
   9.195 -
   9.196 -Addsimps [deg_monom, deg_const, deg_zero, deg_one, deg_uminus];
   9.197 -
   9.198 -Goal
   9.199 -  "!! a::'a::ring. deg (a *s p) <= (if a = 0 then 0 else deg p)";
   9.200 -by (case_tac "a = 0" 1);
   9.201 -by (REPEAT (asm_simp_tac (simpset() addsimps [deg_aboveI, deg_aboveD]) 1));
   9.202 -qed "deg_smult_ring";
   9.203 -
   9.204 -Goal
   9.205 -  "!! a::'a::domain. deg (a *s p) = (if a = 0 then 0 else deg p)";
   9.206 -by (rtac le_anti_sym 1);
   9.207 -by (rtac deg_smult_ring 1);
   9.208 -by (case_tac "a = 0" 1);
   9.209 -by (REPEAT (asm_simp_tac (simpset() addsimps [deg_belowI, deg_lcoeff]) 1));
   9.210 -qed "deg_smult";
   9.211 -
   9.212 -Goal
   9.213 -  "!! p::'a::ring up. [| deg p + deg q < k |] ==> \
   9.214 -\       coeff i p * coeff (k - i) q = 0";
   9.215 -by (simp_tac (simpset() addsimps [coeff_def]) 1);
   9.216 -by (rtac bound_mult_zero 1);
   9.217 -by (assume_tac 3);
   9.218 -by (simp_tac (simpset() addsimps [deg_above_is_bound RS sym]) 1);
   9.219 -by (simp_tac (simpset() addsimps [deg_above_is_bound RS sym]) 1);
   9.220 -qed "deg_above_mult_zero";
   9.221 -
   9.222 -Goal
   9.223 -  "!! p::'a::ring up. deg (p * q) <= deg p + deg q";
   9.224 -by (rtac deg_aboveI 1);
   9.225 -by (asm_simp_tac (simpset() addsimps [deg_above_mult_zero]) 1);
   9.226 -qed "deg_mult_ring";
   9.227 -
   9.228 -goal Main.thy 
   9.229 -  "!!k::nat. k < n ==> m < n + m - k";
   9.230 -by (arith_tac 1);
   9.231 -qed "less_add_diff";
   9.232 -
   9.233 -Goal "!!p. coeff n p ~= 0 ==> n <= deg p";
   9.234 -(* More general than deg_belowI, and simplifies the next proof! *)
   9.235 -by (rtac deg_belowI 1);
   9.236 -by (Fast_tac 1);
   9.237 -qed "deg_below2I";
   9.238 -
   9.239 -Goal
   9.240 -  "!! p::'a::domain up. \
   9.241 -\    [| p ~= 0; q ~= 0 |] ==> deg (p * q) = deg p + deg q";
   9.242 -by (rtac le_anti_sym 1);
   9.243 -by (rtac deg_mult_ring 1);
   9.244 -(* deg p + deg q <= deg (p * q) *)
   9.245 -by (rtac deg_below2I 1);
   9.246 -by (Simp_tac 1);
   9.247 -(*
   9.248 -by (rtac conjI 1);
   9.249 -by (rtac impI 1);
   9.250 -*)
   9.251 -by (res_inst_tac [("m", "deg p"), ("n", "deg p + deg q")] SUM_extend 1);
   9.252 -by (rtac le_add1 1);
   9.253 -by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
   9.254 -by (res_inst_tac [("m", "deg p"), ("n", "deg p")] SUM_extend_below 1);
   9.255 -by (rtac le_refl 1);
   9.256 -by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
   9.257 -by (asm_simp_tac (simpset() addsimps [nonzero_lcoeff]) 1);
   9.258 -(*
   9.259 -by (rtac impI 1);
   9.260 -by (res_inst_tac [("m", "deg p"), ("n", "deg p + deg q")] SUM_extend 1);
   9.261 -by (rtac le_add1 1);
   9.262 -by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
   9.263 -by (res_inst_tac [("m", "deg p"), ("n", "deg p")] SUM_extend_below 1);
   9.264 -by (rtac le_refl 1);
   9.265 -by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
   9.266 -by (asm_simp_tac (simpset() addsimps [nonzero_lcoeff]) 1);
   9.267 -*)
   9.268 -qed "deg_mult";
   9.269 -
   9.270 -Addsimps [deg_smult, deg_mult];
   9.271 -
   9.272 -(* Representation theorems about polynomials *)
   9.273 -
   9.274 -goal PolyRing.thy
   9.275 -  "!! p::nat=>'a::ring up. \
   9.276 -\    coeff k (setsum p {..n}) = setsum (%i. coeff k (p i)) {..n}";
   9.277 -by (induct_tac "n" 1);
   9.278 -by Auto_tac;
   9.279 -qed "coeff_SUM";
   9.280 -
   9.281 -goal UnivPoly.thy
   9.282 -  "!! f::(nat=>'a::ring). \
   9.283 -\    bound n f ==> setsum (%i. if i = x then f i else 0) {..n} = f x";
   9.284 -by (simp_tac (simpset() addsimps [SUM_if_singleton]) 1);
   9.285 -by (auto_tac
   9.286 -    (claset() addDs [not_leE],
   9.287 -     simpset()));
   9.288 -qed "bound_SUM_if";
   9.289 -
   9.290 -Goal
   9.291 -  "!! p::'a::ring up. deg p <= n ==> \
   9.292 -\  setsum (%i. coeff i p *s monom i) {..n} = p";
   9.293 -by (rtac up_eqI 1);
   9.294 -by (simp_tac (simpset() addsimps [coeff_SUM]) 1);
   9.295 -by (rtac trans 1);
   9.296 -by (res_inst_tac [("x", "na")] bound_SUM_if 2);
   9.297 -by (full_simp_tac (simpset() addsimps [deg_above_is_bound, coeff_def]) 2);
   9.298 -by (rtac SUM_cong 1);
   9.299 -by (rtac refl 1);
   9.300 -by (Asm_simp_tac 1);
   9.301 -qed "up_repr";
   9.302 -
   9.303 -Goal
   9.304 -  "!! p::'a::ring up. [| deg p <= n; P p |] ==> \
   9.305 -\  P (setsum (%i. coeff i p *s monom i) {..n})";
   9.306 -by (asm_simp_tac (simpset() addsimps [up_repr]) 1);
   9.307 -qed "up_reprD";
   9.308 -
   9.309 -Goal
   9.310 -  "!! p::'a::ring up. \
   9.311 -\  [| deg p <= n; P (setsum (%i. coeff i p *s monom i) {..n}) |] \
   9.312 -\    ==> P p";
   9.313 -by (asm_full_simp_tac (simpset() addsimps [up_repr]) 1);
   9.314 -qed "up_repr2D";
   9.315 -
   9.316 -(*
   9.317 -Goal
   9.318 -  "!! p::'a::ring up. [| deg p <= n; deg q <= m |] ==> \
   9.319 -\    (SUM n (%i. coeff i p *s monom i) = SUM m (%i. coeff i q *s monom i)) \
   9.320 -\    = (coeff k f = coeff k g)
   9.321 -...
   9.322 -qed "up_unique";
   9.323 -*)
   9.324 -
   9.325 -(* Polynomials over integral domains are again integral domains *)
   9.326 -
   9.327 -Goal "!!p::'a::domain up. p * q = 0 ==> p = 0 | q = 0";
   9.328 -by (rtac classical 1);
   9.329 -by (subgoal_tac "deg p = 0 & deg q = 0" 1);
   9.330 -by (res_inst_tac [("p", "p"), ("n", "0")] up_repr2D 1);
   9.331 -by (Asm_simp_tac 1);
   9.332 -by (res_inst_tac [("p", "q"), ("n", "0")] up_repr2D 1);
   9.333 -by (Asm_simp_tac 1);
   9.334 -by (subgoal_tac "coeff 0 p = 0 | coeff 0 q = 0" 1);
   9.335 -by (force_tac (claset() addIs [up_eqI], simpset()) 1);
   9.336 -by (rtac integral 1);
   9.337 -by (subgoal_tac "coeff 0 (p * q) = 0" 1);
   9.338 -by (Asm_simp_tac 2);
   9.339 -by (Full_simp_tac 1);
   9.340 -by (dres_inst_tac [("f", "deg")] arg_cong 1);
   9.341 -by (Asm_full_simp_tac 1);
   9.342 -qed "up_integral";
   9.343 -
   9.344 -Goal "!! a::'a::domain. a *s p = 0 ==> a = 0 | p = 0";
   9.345 -by (full_simp_tac (simpset() addsimps [const_mult_is_smult RS sym]) 1);
   9.346 -by (dtac up_integral 1);
   9.347 -by Auto_tac;
   9.348 -by (rtac (const_inj RS injD) 1);
   9.349 -by (Simp_tac 1);
   9.350 -qed "smult_integral";
   9.351 -*)
   9.352 -
   9.353 -(* Divisibility and degree *)
   9.354 -
   9.355 -Goalw [dvd_def]
   9.356 -  "!! p::'a::domain up. [| p dvd q; q ~= 0 |] ==> deg p <= deg q";
   9.357 -by (etac exE 1);
   9.358 -by (hyp_subst_tac 1);
   9.359 -by (case_tac "p = 0" 1);
   9.360 -by (case_tac "k = 0" 2);
   9.361 -by Auto_tac;
   9.362 -qed "dvd_imp_deg";
    10.1 --- a/src/HOL/Algebra/poly/UnivPoly.thy	Tue Apr 29 12:36:49 2003 +0200
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,779 +0,0 @@
    10.4 -(*
    10.5 -  Title:     Univariate Polynomials
    10.6 -  Id:        $Id$
    10.7 -  Author:    Clemens Ballarin, started 9 December 1996
    10.8 -  Copyright: Clemens Ballarin
    10.9 -*)
   10.10 -
   10.11 -header {* Univariate Polynomials *}
   10.12 -
   10.13 -theory UnivPoly = Abstract:
   10.14 -
   10.15 -(* already proved in Finite_Set.thy
   10.16 -
   10.17 -lemma setsum_cong:
   10.18 -  "[| A = B; !!i. i : B ==> f i = g i |] ==> setsum f A = setsum g B"
   10.19 -proof -
   10.20 -  assume prems: "A = B" "!!i. i : B ==> f i = g i"
   10.21 -  show ?thesis
   10.22 -  proof (cases "finite B")
   10.23 -    case True
   10.24 -    then have "!!A. [| A = B; !!i. i : B ==> f i = g i |] ==>
   10.25 -      setsum f A = setsum g B"
   10.26 -    proof induct
   10.27 -      case empty thus ?case by simp
   10.28 -    next
   10.29 -      case insert thus ?case by simp
   10.30 -    qed
   10.31 -    with prems show ?thesis by simp
   10.32 -  next
   10.33 -    case False with prems show ?thesis by (simp add: setsum_def)
   10.34 -  qed
   10.35 -qed
   10.36 -*)
   10.37 -
   10.38 -(* Instruct simplifier to simplify assumptions introduced by congs.
   10.39 -   This makes setsum_cong more convenient to use, because assumptions
   10.40 -   like i:{m..n} get simplified (to m <= i & i <= n). *)
   10.41 -
   10.42 -ML_setup {* 
   10.43 -
   10.44 -Addcongs [thm "setsum_cong"];
   10.45 -Context.>> (fn thy => (simpset_ref_of thy :=
   10.46 -  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
   10.47 -
   10.48 -section {* Definition of type up *}
   10.49 -
   10.50 -constdefs
   10.51 -  bound  :: "[nat, nat => 'a::zero] => bool"
   10.52 -  "bound n f == (ALL i. n < i --> f i = 0)"
   10.53 -
   10.54 -lemma boundI [intro!]: "[| !! m. n < m ==> f m = 0 |] ==> bound n f"
   10.55 -proof (unfold bound_def)
   10.56 -qed fast
   10.57 -
   10.58 -lemma boundE [elim?]: "[| bound n f; (!! m. n < m ==> f m = 0) ==> P |] ==> P"
   10.59 -proof (unfold bound_def)
   10.60 -qed fast
   10.61 -
   10.62 -lemma boundD [dest]: "[| bound n f; n < m |] ==> f m = 0"
   10.63 -proof (unfold bound_def)
   10.64 -qed fast
   10.65 -
   10.66 -lemma bound_below:
   10.67 -  assumes bound: "bound m f" and nonzero: "f n ~= 0" shows "n <= m"
   10.68 -proof (rule classical)
   10.69 -  assume "~ ?thesis"
   10.70 -  then have "m < n" by arith
   10.71 -  with bound have "f n = 0" ..
   10.72 -  with nonzero show ?thesis by contradiction
   10.73 -qed
   10.74 -
   10.75 -typedef (UP)
   10.76 -  ('a) up = "{f :: nat => 'a::zero. EX n. bound n f}"
   10.77 -by (rule+)   (* Question: what does trace_rule show??? *)
   10.78 -
   10.79 -section {* Constants *}
   10.80 -
   10.81 -consts
   10.82 -  coeff  :: "['a up, nat] => ('a::zero)"
   10.83 -  monom  :: "['a::zero, nat] => 'a up"              ("(3_*X^/_)" [71, 71] 70)
   10.84 -  "*s"   :: "['a::{zero, times}, 'a up] => 'a up"   (infixl 70)
   10.85 -
   10.86 -defs
   10.87 -  coeff_def: "coeff p n == Rep_UP p n"
   10.88 -  monom_def: "monom a n == Abs_UP (%i. if i=n then a else 0)"
   10.89 -  smult_def: "a *s p == Abs_UP (%i. a * Rep_UP p i)"
   10.90 -
   10.91 -lemma coeff_bound_ex: "EX n. bound n (coeff p)"
   10.92 -proof -
   10.93 -  have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
   10.94 -  then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
   10.95 -  then show ?thesis ..
   10.96 -qed
   10.97 -  
   10.98 -lemma bound_coeff_obtain:
   10.99 -  assumes prem: "(!!n. bound n (coeff p) ==> P)" shows "P"
  10.100 -proof -
  10.101 -  have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
  10.102 -  then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
  10.103 -  with prem show P .
  10.104 -qed
  10.105 -
  10.106 -text {* Ring operations *}
  10.107 -
  10.108 -instance up :: (zero) zero ..
  10.109 -instance up :: (one) one ..
  10.110 -instance up :: (plus) plus ..
  10.111 -instance up :: (minus) minus ..
  10.112 -instance up :: (times) times ..
  10.113 -instance up :: (inverse) inverse ..
  10.114 -instance up :: (power) power ..
  10.115 -
  10.116 -defs
  10.117 -  up_add_def:	"p + q == Abs_UP (%n. Rep_UP p n + Rep_UP q n)"
  10.118 -  up_mult_def:  "p * q == Abs_UP (%n::nat. setsum
  10.119 -		     (%i. Rep_UP p i * Rep_UP q (n-i)) {..n})"
  10.120 -  up_zero_def:  "0 == monom 0 0"
  10.121 -  up_one_def:   "1 == monom 1 0"
  10.122 -  up_uminus_def:"- p == (- 1) *s p"
  10.123 -                (* easier to use than "Abs_UP (%i. - Rep_UP p i)" *)
  10.124 -                (* note: - 1 is different from -1; latter is of class number *)
  10.125 -
  10.126 -  up_minus_def:   "(a::'a::{plus, minus} up) - b == a + (-b)"
  10.127 -  up_inverse_def: "inverse (a::'a::{zero, one, times, inverse} up) == 
  10.128 -                     (if a dvd 1 then THE x. a*x = 1 else 0)"
  10.129 -  up_divide_def:  "(a::'a::{times, inverse} up) / b == a * inverse b"
  10.130 -  up_power_def:   "(a::'a::{one, times, power} up) ^ n ==
  10.131 -                     nat_rec 1 (%u b. b * a) n"
  10.132 -
  10.133 -subsection {* Effect of operations on coefficients *}
  10.134 -
  10.135 -lemma coeff_monom [simp]: "coeff (monom a m) n = (if m=n then a else 0)"
  10.136 -proof -
  10.137 -  have "(%n. if n = m then a else 0) : UP"
  10.138 -    using UP_def by force
  10.139 -  from this show ?thesis
  10.140 -    by (simp add: coeff_def monom_def Abs_UP_inverse Rep_UP)
  10.141 -qed
  10.142 -
  10.143 -lemma coeff_zero [simp]: "coeff 0 n = 0"
  10.144 -proof (unfold up_zero_def)
  10.145 -qed simp
  10.146 -
  10.147 -lemma coeff_one [simp]: "coeff 1 n = (if n=0 then 1 else 0)"
  10.148 -proof (unfold up_one_def)
  10.149 -qed simp
  10.150 -
  10.151 -(* term order
  10.152 -lemma coeff_smult [simp]: "coeff (a *s p) n = (a::'a::ring) * coeff p n"
  10.153 -proof -
  10.154 -  have "!!f. f : UP ==> (%n. a * f n) : UP"
  10.155 -    by (unfold UP_def) (force simp add: ring_simps)
  10.156 -*)      (* this force step is slow *)
  10.157 -(*  then show ?thesis
  10.158 -    apply (simp add: coeff_def smult_def Abs_UP_inverse Rep_UP)
  10.159 -qed
  10.160 -*)
  10.161 -lemma coeff_smult [simp]: "coeff (a *s p) n = (a::'a::ring) * coeff p n"
  10.162 -proof -
  10.163 -  have "Rep_UP p : UP ==> (%n. a * Rep_UP p n) : UP"
  10.164 -    by (unfold UP_def) (force simp add: ring_simps)
  10.165 -      (* this force step is slow *)
  10.166 -  then show ?thesis
  10.167 -    by (simp add: coeff_def smult_def Abs_UP_inverse Rep_UP)
  10.168 -qed
  10.169 -
  10.170 -lemma coeff_add [simp]: "coeff (p+q) n = (coeff p n + coeff q n::'a::ring)"
  10.171 -proof -
  10.172 -  {
  10.173 -    fix f g
  10.174 -    assume fup: "(f::nat=>'a::ring) : UP" and gup: "(g::nat=>'a::ring) : UP"
  10.175 -    have "(%i. f i + g i) : UP"
  10.176 -    proof -
  10.177 -      from fup obtain n where boundn: "bound n f"
  10.178 -	by (unfold UP_def) fast
  10.179 -      from gup obtain m where boundm: "bound m g"
  10.180 -	by (unfold UP_def) fast
  10.181 -      have "bound (max n m) (%i. (f i + g i))"
  10.182 -      proof
  10.183 -	fix i
  10.184 -	assume "max n m < i"
  10.185 -	with boundn and boundm show "f i + g i = 0"
  10.186 -          by (fastsimp simp add: ring_simps)
  10.187 -      qed
  10.188 -      then show "(%i. (f i + g i)) : UP"
  10.189 -	by (unfold UP_def) fast
  10.190 -    qed
  10.191 -  }
  10.192 -  then show ?thesis
  10.193 -    by (simp add: coeff_def up_add_def Abs_UP_inverse Rep_UP)
  10.194 -qed
  10.195 -
  10.196 -lemma coeff_mult [simp]:
  10.197 -  "coeff (p * q) n = (setsum (%i. coeff p i * coeff q (n-i)) {..n}::'a::ring)"
  10.198 -proof -
  10.199 -  {
  10.200 -    fix f g
  10.201 -    assume fup: "(f::nat=>'a::ring) : UP" and gup: "(g::nat=>'a::ring) : UP"
  10.202 -    have "(%n. setsum (%i. f i * g (n-i)) {..n}) : UP"
  10.203 -    proof -
  10.204 -      from fup obtain n where "bound n f"
  10.205 -	by (unfold UP_def) fast
  10.206 -      from gup obtain m where "bound m g"
  10.207 -	by (unfold UP_def) fast
  10.208 -      have "bound (n + m) (%n. setsum (%i. f i * g (n-i)) {..n})"
  10.209 -      proof
  10.210 -	fix k
  10.211 -	assume bound: "n + m < k"
  10.212 -	{
  10.213 -	  fix i
  10.214 -	  have "f i * g (k-i) = 0"
  10.215 -	  proof cases
  10.216 -	    assume "n < i"
  10.217 -	    show ?thesis by (auto! simp add: ring_simps)
  10.218 -	  next
  10.219 -	    assume "~ (n < i)"
  10.220 -	    with bound have "m < k-i" by arith
  10.221 -	    then show ?thesis by (auto! simp add: ring_simps)
  10.222 -	  qed
  10.223 -	}
  10.224 -	then show "setsum (%i. f i * g (k-i)) {..k} = 0"
  10.225 -	  by (simp add: ring_simps)
  10.226 -      qed
  10.227 -      then show "(%n. setsum (%i. f i * g (n-i)) {..n}) : UP"
  10.228 -	by (unfold UP_def) fast
  10.229 -    qed
  10.230 -  }
  10.231 -  then show ?thesis
  10.232 -    by (simp add: coeff_def up_mult_def Abs_UP_inverse Rep_UP)
  10.233 -qed
  10.234 -
  10.235 -lemma coeff_uminus [simp]: "coeff (-p) n = (-coeff p n::'a::ring)"
  10.236 -by (unfold up_uminus_def) (simp add: ring_simps)
  10.237 -
  10.238 -(* Other lemmas *)
  10.239 -
  10.240 -lemma up_eqI: assumes prem: "(!! n. coeff p n = coeff q n)" shows "p = q"
  10.241 -proof -
  10.242 -  have "p = Abs_UP (%u. Rep_UP p u)" by (simp add: Rep_UP_inverse)
  10.243 -  also from prem have "... = Abs_UP (Rep_UP q)" by (simp only: coeff_def)
  10.244 -  also have "... = q" by (simp add: Rep_UP_inverse)
  10.245 -  finally show ?thesis .
  10.246 -qed
  10.247 -
  10.248 -(* ML_setup {* Addsimprocs [ring_simproc] *} *)
  10.249 -
  10.250 -instance up :: (ring) ring
  10.251 -proof
  10.252 -  fix p q r :: "'a::ring up"
  10.253 -  fix n
  10.254 -  show "(p + q) + r = p + (q + r)"
  10.255 -    by (rule up_eqI) simp
  10.256 -  show "0 + p = p"
  10.257 -    by (rule up_eqI) simp
  10.258 -  show "(-p) + p = 0"
  10.259 -    by (rule up_eqI) simp
  10.260 -  show "p + q = q + p"
  10.261 -    by (rule up_eqI) simp
  10.262 -  show "(p * q) * r = p * (q * r)"
  10.263 -  proof (rule up_eqI)
  10.264 -    fix n 
  10.265 -    {
  10.266 -      fix k and a b c :: "nat=>'a::ring"
  10.267 -      have "k <= n ==> 
  10.268 -	setsum (%j. setsum (%i. a i * b (j-i)) {..j} * c (n-j)) {..k} = 
  10.269 -	setsum (%j. a j * setsum  (%i. b i * c (n-j-i)) {..k-j}) {..k}"
  10.270 -	(is "_ ==> ?eq k")
  10.271 -      proof (induct k)
  10.272 -	case 0 show ?case by simp
  10.273 -      next
  10.274 -	case (Suc k)
  10.275 -	then have "k <= n" by arith
  10.276 -	then have "?eq k" by (rule Suc)
  10.277 -	then show ?case
  10.278 -	  by (simp add: Suc_diff_le natsum_ldistr)
  10.279 -      qed
  10.280 -    }
  10.281 -    then show "coeff ((p * q) * r) n = coeff (p * (q * r)) n"
  10.282 -      by simp
  10.283 -  qed
  10.284 -  show "1 * p = p"
  10.285 -  proof (rule up_eqI)
  10.286 -    fix n
  10.287 -    show "coeff (1 * p) n = coeff p n"
  10.288 -    proof (cases n)
  10.289 -      case 0 then show ?thesis by simp
  10.290 -    next
  10.291 -      case Suc then show ?thesis by (simp del: natsum_Suc add: natsum_Suc2)
  10.292 -    qed
  10.293 -  qed
  10.294 -  show "(p + q) * r = p * r + q * r"
  10.295 -    by (rule up_eqI) simp
  10.296 -  show "p * q = q * p"
  10.297 -  proof (rule up_eqI)
  10.298 -    fix n 
  10.299 -    {
  10.300 -      fix k
  10.301 -      fix a b :: "nat=>'a::ring"
  10.302 -      have "k <= n ==> 
  10.303 -	setsum (%i. a i * b (n-i)) {..k} =
  10.304 -	setsum (%i. a (k-i) * b (i+n-k)) {..k}"
  10.305 -	(is "_ ==> ?eq k")
  10.306 -      proof (induct k)
  10.307 -	case 0 show ?case by simp
  10.308 -      next
  10.309 -	case (Suc k) then show ?case by (subst natsum_Suc2) simp
  10.310 -      qed
  10.311 -    }
  10.312 -    then show "coeff (p * q) n = coeff (q * p) n"
  10.313 -      by simp
  10.314 -  qed
  10.315 -
  10.316 -  show "p - q = p + (-q)"
  10.317 -    by (simp add: up_minus_def)
  10.318 -  show "inverse p = (if p dvd 1 then THE x. p*x = 1 else 0)"
  10.319 -    by (simp add: up_inverse_def)
  10.320 -  show "p / q = p * inverse q"
  10.321 -    by (simp add: up_divide_def)
  10.322 -  show "p ^ n = nat_rec 1 (%u b. b * p) n"
  10.323 -    by (simp add: up_power_def)
  10.324 -  qed
  10.325 -
  10.326 -(* Further properties of monom *)
  10.327 -
  10.328 -lemma monom_zero [simp]:
  10.329 -  "monom 0 n = 0"
  10.330 -  by (simp add: monom_def up_zero_def)
  10.331 -(* term order: application of coeff_mult goes wrong: rule not symmetric
  10.332 -lemma monom_mult_is_smult:
  10.333 -  "monom (a::'a::ring) 0 * p = a *s p"
  10.334 -proof (rule up_eqI)
  10.335 -  fix k
  10.336 -  show "coeff (monom a 0 * p) k = coeff (a *s p) k"
  10.337 -  proof (cases k)
  10.338 -    case 0 then show ?thesis by simp
  10.339 -  next
  10.340 -    case Suc then show ?thesis by simp
  10.341 -  qed
  10.342 -qed
  10.343 -*)
  10.344 -ML_setup {* Delsimprocs [ring_simproc] *}
  10.345 -
  10.346 -lemma monom_mult_is_smult:
  10.347 -  "monom (a::'a::ring) 0 * p = a *s p"
  10.348 -proof (rule up_eqI)
  10.349 -  fix k
  10.350 -  have "coeff (p * monom a 0) k = coeff (a *s p) k"
  10.351 -  proof (cases k)
  10.352 -    case 0 then show ?thesis by simp ring
  10.353 -  next
  10.354 -    case Suc then show ?thesis by (simp add: ring_simps) ring
  10.355 -  qed
  10.356 -  then show "coeff (monom a 0 * p) k = coeff (a *s p) k" by ring
  10.357 -qed
  10.358 -
  10.359 -ML_setup {* Addsimprocs [ring_simproc] *}
  10.360 -
  10.361 -lemma monom_add [simp]:
  10.362 -  "monom (a + b) n = monom (a::'a::ring) n + monom b n"
  10.363 -by (rule up_eqI) simp
  10.364 -
  10.365 -lemma monom_mult_smult:
  10.366 -  "monom (a * b) n = a *s monom (b::'a::ring) n"
  10.367 -by (rule up_eqI) simp
  10.368 -
  10.369 -lemma monom_uminus [simp]:
  10.370 -  "monom (-a) n = - monom (a::'a::ring) n"
  10.371 -by (rule up_eqI) simp
  10.372 -
  10.373 -lemma monom_one [simp]:
  10.374 -  "monom 1 0 = 1"
  10.375 -by (simp add: up_one_def)
  10.376 -
  10.377 -lemma monom_inj:
  10.378 -  "(monom a n = monom b n) = (a = b)"
  10.379 -proof
  10.380 -  assume "monom a n = monom b n"
  10.381 -  then have "coeff (monom a n) n = coeff (monom b n) n" by simp
  10.382 -  then show "a = b" by simp
  10.383 -next
  10.384 -  assume "a = b" then show "monom a n = monom b n" by simp
  10.385 -qed
  10.386 -
  10.387 -(* Properties of *s:
  10.388 -   Polynomials form a module *)
  10.389 -
  10.390 -lemma smult_l_distr:
  10.391 -  "(a + b::'a::ring) *s p = a *s p + b *s p"
  10.392 -by (rule up_eqI) simp
  10.393 -
  10.394 -lemma smult_r_distr:
  10.395 -  "(a::'a::ring) *s (p + q) = a *s p + a *s q"
  10.396 -by (rule up_eqI) simp
  10.397 -
  10.398 -lemma smult_assoc1:
  10.399 -  "(a * b::'a::ring) *s p = a *s (b *s p)"
  10.400 -by (rule up_eqI) simp
  10.401 -
  10.402 -lemma smult_one [simp]:
  10.403 -  "(1::'a::ring) *s p = p"
  10.404 -by (rule up_eqI) simp
  10.405 -
  10.406 -(* Polynomials form an algebra *)
  10.407 -
  10.408 -ML_setup {* Delsimprocs [ring_simproc] *}
  10.409 -
  10.410 -lemma smult_assoc2:
  10.411 -  "(a *s p) * q = (a::'a::ring) *s (p * q)"
  10.412 -by (rule up_eqI) (simp add: natsum_rdistr m_assoc)
  10.413 -(* Simproc fails. *)
  10.414 -
  10.415 -ML_setup {* Addsimprocs [ring_simproc] *}
  10.416 -
  10.417 -(* the following can be derived from the above ones,
  10.418 -   for generality reasons, it is therefore done *)
  10.419 -
  10.420 -lemma smult_l_null [simp]:
  10.421 -  "(0::'a::ring) *s p = 0"
  10.422 -proof -
  10.423 -  fix a
  10.424 -  have "0 *s p = (0 *s p + a *s p) + - (a *s p)" by simp
  10.425 -  also have "... = (0 + a) *s p + - (a *s p)" by (simp only: smult_l_distr)
  10.426 -  also have "... = 0" by simp
  10.427 -  finally show ?thesis .
  10.428 -qed
  10.429 -
  10.430 -lemma smult_r_null [simp]:
  10.431 -  "(a::'a::ring) *s 0 = 0";
  10.432 -proof -
  10.433 -  fix p
  10.434 -  have "a *s 0 = (a *s 0 + a *s p) + - (a *s p)" by simp
  10.435 -  also have "... = a *s (0 + p) + - (a *s p)" by (simp only: smult_r_distr)
  10.436 -  also have "... = 0" by simp
  10.437 -  finally show ?thesis .
  10.438 -qed
  10.439 -
  10.440 -lemma smult_l_minus:
  10.441 -  "(-a::'a::ring) *s p = - (a *s p)"
  10.442 -proof -
  10.443 -  have "(-a) *s p = (-a *s p + a *s p) + -(a *s p)" by simp 
  10.444 -  also have "... = (-a + a) *s p + -(a *s p)" by (simp only: smult_l_distr)
  10.445 -  also have "... = -(a *s p)" by simp
  10.446 -  finally show ?thesis .
  10.447 -qed
  10.448 -
  10.449 -lemma smult_r_minus:
  10.450 -  "(a::'a::ring) *s (-p) = - (a *s p)"
  10.451 -proof -
  10.452 -  have "a *s (-p) = (a *s -p + a *s p) + -(a *s p)" by simp
  10.453 -  also have "... = a *s (-p + p) + -(a *s p)" by (simp only: smult_r_distr)
  10.454 -  also have "... = -(a *s p)" by simp
  10.455 -  finally show ?thesis .
  10.456 -qed
  10.457 -
  10.458 -section {* The degree function *}
  10.459 -
  10.460 -constdefs
  10.461 -  deg :: "('a::zero) up => nat"
  10.462 -  "deg p == LEAST n. bound n (coeff p)"
  10.463 -
  10.464 -lemma deg_aboveI:
  10.465 -  "(!!m. n < m ==> coeff p m = 0) ==> deg p <= n"
  10.466 -by (unfold deg_def) (fast intro: Least_le)
  10.467 -
  10.468 -lemma deg_aboveD:
  10.469 -  assumes prem: "deg p < m" shows "coeff p m = 0"
  10.470 -proof -
  10.471 -  obtain n where "bound n (coeff p)" by (rule bound_coeff_obtain)
  10.472 -  then have "bound (deg p) (coeff p)" by (unfold deg_def, rule LeastI)
  10.473 -  then show "coeff p m = 0" by (rule boundD)
  10.474 -qed
  10.475 -
  10.476 -lemma deg_belowI:
  10.477 -  assumes prem: "n ~= 0 ==> coeff p n ~= 0" shows "n <= deg p"
  10.478 -(* logically, this is a slightly stronger version of deg_aboveD *)
  10.479 -proof (cases "n=0")
  10.480 -  case True then show ?thesis by simp
  10.481 -next
  10.482 -  case False then have "coeff p n ~= 0" by (rule prem)
  10.483 -  then have "~ deg p < n" by (fast dest: deg_aboveD)
  10.484 -  then show ?thesis by arith
  10.485 -qed
  10.486 -
  10.487 -lemma lcoeff_nonzero_deg:
  10.488 -  assumes deg: "deg p ~= 0" shows "coeff p (deg p) ~= 0"
  10.489 -proof -
  10.490 -  obtain m where "deg p <= m" and m_coeff: "coeff p m ~= 0"
  10.491 -  proof -
  10.492 -    have minus: "!!(n::nat) m. n ~= 0 ==> (n - Suc 0 < m) = (n <= m)"
  10.493 -      by arith (* make public?, why does proof not work with "1" *)
  10.494 -    from deg have "deg p - 1 < (LEAST n. bound n (coeff p))"
  10.495 -      by (unfold deg_def) arith
  10.496 -    then have "~ bound (deg p - 1) (coeff p)" by (rule not_less_Least)
  10.497 -    then have "EX m. deg p - 1 < m & coeff p m ~= 0"
  10.498 -      by (unfold bound_def) fast
  10.499 -    then have "EX m. deg p <= m & coeff p m ~= 0" by (simp add: deg minus)
  10.500 -    then show ?thesis by auto 
  10.501 -  qed
  10.502 -  with deg_belowI have "deg p = m" by fastsimp
  10.503 -  with m_coeff show ?thesis by simp
  10.504 -qed
  10.505 -
  10.506 -lemma lcoeff_nonzero_nonzero:
  10.507 -  assumes deg: "deg p = 0" and nonzero: "p ~= 0" shows "coeff p 0 ~= 0"
  10.508 -proof -
  10.509 -  have "EX m. coeff p m ~= 0"
  10.510 -  proof (rule classical)
  10.511 -    assume "~ ?thesis"
  10.512 -    then have "p = 0" by (auto intro: up_eqI)
  10.513 -    with nonzero show ?thesis by contradiction
  10.514 -  qed
  10.515 -  then obtain m where coeff: "coeff p m ~= 0" ..
  10.516 -  then have "m <= deg p" by (rule deg_belowI)
  10.517 -  then have "m = 0" by (simp add: deg)
  10.518 -  with coeff show ?thesis by simp
  10.519 -qed
  10.520 -
  10.521 -lemma lcoeff_nonzero:
  10.522 -  "p ~= 0 ==> coeff p (deg p) ~= 0"
  10.523 -proof (cases "deg p = 0")
  10.524 -  case True
  10.525 -  assume "p ~= 0"
  10.526 -  with True show ?thesis by (simp add: lcoeff_nonzero_nonzero)
  10.527 -next
  10.528 -  case False
  10.529 -  assume "p ~= 0"
  10.530 -  with False show ?thesis by (simp add: lcoeff_nonzero_deg)
  10.531 -qed
  10.532 -
  10.533 -lemma deg_eqI:
  10.534 -  "[| !!m. n < m ==> coeff p m = 0;
  10.535 -      !!n. n ~= 0 ==> coeff p n ~= 0|] ==> deg p = n"
  10.536 -by (fast intro: le_anti_sym deg_aboveI deg_belowI)
  10.537 -
  10.538 -(* Degree and polynomial operations *)
  10.539 -
  10.540 -lemma deg_add [simp]:
  10.541 -  "deg ((p::'a::ring up) + q) <= max (deg p) (deg q)"
  10.542 -proof (cases "deg p <= deg q")
  10.543 -  case True show ?thesis by (rule deg_aboveI) (simp add: True deg_aboveD) 
  10.544 -next
  10.545 -  case False show ?thesis by (rule deg_aboveI) (simp add: False deg_aboveD)
  10.546 -qed
  10.547 -
  10.548 -lemma deg_monom_ring:
  10.549 -  "deg (monom a n::'a::ring up) <= n"
  10.550 -by (rule deg_aboveI) simp
  10.551 -
  10.552 -lemma deg_monom [simp]:
  10.553 -  "a ~= 0 ==> deg (monom a n::'a::ring up) = n"
  10.554 -by (fastsimp intro: le_anti_sym deg_aboveI deg_belowI)
  10.555 -
  10.556 -lemma deg_const [simp]:
  10.557 -  "deg (monom (a::'a::ring) 0) = 0"
  10.558 -proof (rule le_anti_sym)
  10.559 -  show "deg (monom a 0) <= 0" by (rule deg_aboveI) simp
  10.560 -next
  10.561 -  show "0 <= deg (monom a 0)" by (rule deg_belowI) simp
  10.562 -qed
  10.563 -
  10.564 -lemma deg_zero [simp]:
  10.565 -  "deg 0 = 0"
  10.566 -proof (rule le_anti_sym)
  10.567 -  show "deg 0 <= 0" by (rule deg_aboveI) simp
  10.568 -next
  10.569 -  show "0 <= deg 0" by (rule deg_belowI) simp
  10.570 -qed
  10.571 -
  10.572 -lemma deg_one [simp]:
  10.573 -  "deg 1 = 0"
  10.574 -proof (rule le_anti_sym)
  10.575 -  show "deg 1 <= 0" by (rule deg_aboveI) simp
  10.576 -next
  10.577 -  show "0 <= deg 1" by (rule deg_belowI) simp
  10.578 -qed
  10.579 -
  10.580 -lemma uminus_monom:
  10.581 -  "!!a::'a::ring. (-a = 0) = (a = 0)"
  10.582 -proof
  10.583 -  fix a::"'a::ring"
  10.584 -  assume "a = 0"
  10.585 -  then show "-a = 0" by simp
  10.586 -next
  10.587 -  fix a::"'a::ring"
  10.588 -  assume "- a = 0"
  10.589 -  then have "-(- a) = 0" by simp
  10.590 -  then show "a = 0" by simp
  10.591 -qed
  10.592 -
  10.593 -lemma deg_uminus [simp]:
  10.594 -  "deg (-p::('a::ring) up) = deg p"
  10.595 -proof (rule le_anti_sym)
  10.596 -  show "deg (- p) <= deg p" by (simp add: deg_aboveI deg_aboveD)
  10.597 -next
  10.598 -  show "deg p <= deg (- p)" 
  10.599 -  by (simp add: deg_belowI lcoeff_nonzero_deg uminus_monom)
  10.600 -qed
  10.601 -
  10.602 -lemma deg_smult_ring:
  10.603 -  "deg ((a::'a::ring) *s p) <= (if a = 0 then 0 else deg p)"
  10.604 -proof (cases "a = 0")
  10.605 -qed (simp add: deg_aboveI deg_aboveD)+
  10.606 -
  10.607 -lemma deg_smult [simp]:
  10.608 -  "deg ((a::'a::domain) *s p) = (if a = 0 then 0 else deg p)"
  10.609 -proof (rule le_anti_sym)
  10.610 -  show "deg (a *s p) <= (if a = 0 then 0 else deg p)" by (rule deg_smult_ring)
  10.611 -next
  10.612 -  show "(if a = 0 then 0 else deg p) <= deg (a *s p)"
  10.613 -  proof (cases "a = 0")
  10.614 -  qed (simp, simp add: deg_belowI lcoeff_nonzero_deg integral_iff)
  10.615 -qed
  10.616 -
  10.617 -lemma deg_mult_ring:
  10.618 -  "deg (p * q::'a::ring up) <= deg p + deg q"
  10.619 -proof (rule deg_aboveI)
  10.620 -  fix m
  10.621 -  assume boundm: "deg p + deg q < m"
  10.622 -  {
  10.623 -    fix k i
  10.624 -    assume boundk: "deg p + deg q < k"
  10.625 -    then have "coeff p i * coeff q (k - i) = 0"
  10.626 -    proof (cases "deg p < i")
  10.627 -      case True then show ?thesis by (simp add: deg_aboveD)
  10.628 -    next
  10.629 -      case False with boundk have "deg q < k - i" by arith
  10.630 -      then show ?thesis by (simp add: deg_aboveD)
  10.631 -    qed
  10.632 -  }
  10.633 -      (* This is similar to bound_mult_zero and deg_above_mult_zero in the old
  10.634 -         proofs. *)
  10.635 -  with boundm show "coeff (p * q) m = 0" by simp
  10.636 -qed
  10.637 -
  10.638 -lemma deg_mult [simp]:
  10.639 -  "[| (p::'a::domain up) ~= 0; q ~= 0|] ==> deg (p * q) = deg p + deg q"
  10.640 -proof (rule le_anti_sym)
  10.641 -  show "deg (p * q) <= deg p + deg q" by (rule deg_mult_ring)
  10.642 -next
  10.643 -  let ?s = "(%i. coeff p i * coeff q (deg p + deg q - i))"
  10.644 -  assume nz: "p ~= 0" "q ~= 0"
  10.645 -  have less_add_diff: "!!(k::nat) n m. k < n ==> m < n + m - k" by arith
  10.646 -  show "deg p + deg q <= deg (p * q)"
  10.647 -  proof (rule deg_belowI, simp)
  10.648 -    have "setsum ?s {.. deg p + deg q}
  10.649 -      = setsum ?s ({.. deg p(} Un {deg p .. deg p + deg q})"
  10.650 -      by (simp only: ivl_disj_un_one)
  10.651 -    also have "... = setsum ?s {deg p .. deg p + deg q}"
  10.652 -      by (simp add: setsum_Un_disjoint ivl_disj_int_one
  10.653 -        setsum_0 deg_aboveD less_add_diff)
  10.654 -    also have "... = setsum ?s ({deg p} Un {)deg p .. deg p + deg q})"
  10.655 -      by (simp only: ivl_disj_un_singleton)
  10.656 -    also have "... = coeff p (deg p) * coeff q (deg q)" 
  10.657 -      by (simp add: setsum_Un_disjoint ivl_disj_int_singleton 
  10.658 -        setsum_0 deg_aboveD)
  10.659 -    finally have "setsum ?s {.. deg p + deg q} 
  10.660 -      = coeff p (deg p) * coeff q (deg q)" .
  10.661 -    with nz show "setsum ?s {.. deg p + deg q} ~= 0"
  10.662 -      by (simp add: integral_iff lcoeff_nonzero)
  10.663 -    qed
  10.664 -  qed
  10.665 -
  10.666 -lemma coeff_natsum:
  10.667 -  "((coeff (setsum p A) k)::'a::ring) = 
  10.668 -   setsum (%i. coeff (p i) k) A"
  10.669 -proof (cases "finite A")
  10.670 -  case True then show ?thesis by induct auto
  10.671 -next
  10.672 -  case False then show ?thesis by (simp add: setsum_def)
  10.673 -qed
  10.674 -(* Instance of a more general result!!! *)
  10.675 -
  10.676 -(*
  10.677 -lemma coeff_natsum:
  10.678 -  "((coeff (setsum p {..n::nat}) k)::'a::ring) = 
  10.679 -   setsum (%i. coeff (p i) k) {..n}"
  10.680 -by (induct n) auto
  10.681 -*)
  10.682 -
  10.683 -lemma up_repr:
  10.684 -  "setsum (%i. monom (coeff p i) i) {..deg (p::'a::ring up)} = p"
  10.685 -proof (rule up_eqI)
  10.686 -  let ?s = "(%i. monom (coeff p i) i)"
  10.687 -  fix k
  10.688 -  show "coeff (setsum ?s {..deg p}) k = coeff p k"
  10.689 -  proof (cases "k <= deg p")
  10.690 -    case True
  10.691 -    hence "coeff (setsum ?s {..deg p}) k = 
  10.692 -          coeff (setsum ?s ({..k} Un {)k..deg p})) k"
  10.693 -      by (simp only: ivl_disj_un_one)
  10.694 -    also from True
  10.695 -    have "... = coeff (setsum ?s {..k}) k"
  10.696 -      by (simp add: setsum_Un_disjoint ivl_disj_int_one order_less_imp_not_eq2
  10.697 -        setsum_0 coeff_natsum )
  10.698 -    also
  10.699 -    have "... = coeff (setsum ?s ({..k(} Un {k})) k"
  10.700 -      by (simp only: ivl_disj_un_singleton)
  10.701 -    also have "... = coeff p k"
  10.702 -      by (simp add: setsum_Un_disjoint ivl_disj_int_singleton 
  10.703 -        setsum_0 coeff_natsum deg_aboveD)
  10.704 -    finally show ?thesis .
  10.705 -  next
  10.706 -    case False
  10.707 -    hence "coeff (setsum ?s {..deg p}) k = 
  10.708 -          coeff (setsum ?s ({..deg p(} Un {deg p})) k"
  10.709 -      by (simp only: ivl_disj_un_singleton)
  10.710 -    also from False have "... = coeff p k"
  10.711 -      by (simp add: setsum_Un_disjoint ivl_disj_int_singleton 
  10.712 -        setsum_0 coeff_natsum deg_aboveD)
  10.713 -    finally show ?thesis .
  10.714 -  qed
  10.715 -qed
  10.716 -
  10.717 -lemma up_repr_le:
  10.718 -  "deg (p::'a::ring up) <= n ==> setsum (%i. monom (coeff p i) i) {..n} = p"
  10.719 -proof -
  10.720 -  let ?s = "(%i. monom (coeff p i) i)"
  10.721 -  assume "deg p <= n"
  10.722 -  then have "setsum ?s {..n} = setsum ?s ({..deg p} Un {)deg p..n})"
  10.723 -    by (simp only: ivl_disj_un_one)
  10.724 -  also have "... = setsum ?s {..deg p}"
  10.725 -    by (simp add: setsum_Un_disjoint ivl_disj_int_one
  10.726 -      setsum_0 deg_aboveD)
  10.727 -  also have "... = p" by (rule up_repr)
  10.728 -  finally show ?thesis .
  10.729 -qed
  10.730 -
  10.731 -instance up :: ("domain") "domain"
  10.732 -proof
  10.733 -  show "1 ~= (0::'a up)"
  10.734 -  proof (* notI is applied here *)
  10.735 -    assume "1 = (0::'a up)"
  10.736 -    hence "coeff 1 0 = (coeff 0 0::'a)" by simp
  10.737 -    hence "1 = (0::'a)" by simp
  10.738 -    with one_not_zero show "False" by contradiction
  10.739 -  qed
  10.740 -next
  10.741 -  fix p q :: "'a::domain up"
  10.742 -  assume pq: "p * q = 0"
  10.743 -  show "p = 0 | q = 0"
  10.744 -  proof (rule classical)
  10.745 -    assume c: "~ (p = 0 | q = 0)"
  10.746 -    then have "deg p + deg q = deg (p * q)" by simp
  10.747 -    also from pq have "... = 0" by simp
  10.748 -    finally have "deg p + deg q = 0" .
  10.749 -    then have f1: "deg p = 0 & deg q = 0" by simp
  10.750 -    from f1 have "p = setsum (%i. (monom (coeff p i) i)) {..0}"
  10.751 -      by (simp only: up_repr_le)
  10.752 -    also have "... = monom (coeff p 0) 0" by simp
  10.753 -    finally have p: "p = monom (coeff p 0) 0" .
  10.754 -    from f1 have "q = setsum (%i. (monom (coeff q i) i)) {..0}"
  10.755 -      by (simp only: up_repr_le)
  10.756 -    also have "... = monom (coeff q 0) 0" by simp
  10.757 -    finally have q: "q = monom (coeff q 0) 0" .
  10.758 -    have "coeff p 0 * coeff q 0 = coeff (p * q) 0" by simp
  10.759 -    also from pq have "... = 0" by simp
  10.760 -    finally have "coeff p 0 * coeff q 0 = 0" .
  10.761 -    then have "coeff p 0 = 0 | coeff q 0 = 0" by (simp only: integral_iff)
  10.762 -    with p q show "p = 0 | q = 0" by fastsimp
  10.763 -  qed
  10.764 -qed
  10.765 -
  10.766 -lemma monom_inj_zero:
  10.767 -  "(monom a n = 0) = (a = 0)"
  10.768 -proof -
  10.769 -  have "(monom a n = 0) = (monom a n = monom 0 n)" by simp
  10.770 -  also have "... = (a = 0)" by (simp add: monom_inj del: monom_zero)
  10.771 -  finally show ?thesis .
  10.772 -qed
  10.773 -(* term order: makes this simpler!!!
  10.774 -lemma smult_integral:
  10.775 -  "(a::'a::domain) *s p = 0 ==> a = 0 | p = 0"
  10.776 -by (simp add: monom_mult_is_smult [THEN sym] integral_iff monom_inj_zero) fast
  10.777 -*)
  10.778 -lemma smult_integral:
  10.779 -  "(a::'a::domain) *s p = 0 ==> a = 0 | p = 0"
  10.780 -by (simp add: monom_mult_is_smult [THEN sym] integral_iff monom_inj_zero)
  10.781 -
  10.782 -end
  10.783 \ No newline at end of file
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/Algebra/poly/UnivPoly2.ML	Wed Apr 30 10:01:35 2003 +0200
    11.3 @@ -0,0 +1,359 @@
    11.4 +(*
    11.5 +    Degree of polynomials
    11.6 +    $Id$
    11.7 +    written by Clemens Ballarin, started 22 January 1997
    11.8 +*)
    11.9 +
   11.10 +(*
   11.11 +(* Relating degree and bound *)
   11.12 +
   11.13 +Goal "[| bound m f; f n ~= 0 |] ==> n <= m";
   11.14 +by (force_tac (claset() addDs [inst "m" "n" boundD], 
   11.15 +               simpset()) 1); 
   11.16 +qed "below_bound";
   11.17 +
   11.18 +goal UnivPoly2.thy "bound (LEAST n. bound n (Rep_UP p)) (Rep_UP p)";
   11.19 +by (rtac exE 1);
   11.20 +by (rtac LeastI 2);
   11.21 +by (assume_tac 2);
   11.22 +by (res_inst_tac [("a", "Rep_UP p")] CollectD 1);
   11.23 +by (rtac (rewrite_rule [UP_def] Rep_UP) 1);
   11.24 +qed "Least_is_bound";
   11.25 +
   11.26 +Goalw [coeff_def, deg_def]
   11.27 +  "!! p. ALL m. n < m --> coeff m p = 0 ==> deg p <= n";
   11.28 +by (rtac Least_le 1);
   11.29 +by (Fast_tac 1);
   11.30 +qed "deg_aboveI";
   11.31 +
   11.32 +Goalw [coeff_def, deg_def]
   11.33 +  "(n ~= 0 --> coeff n p ~= 0) ==> n <= deg p";
   11.34 +by (case_tac "n = 0" 1);
   11.35 +(* Case n=0 *)
   11.36 +by (Asm_simp_tac 1);
   11.37 +(* Case n~=0 *)
   11.38 +by (rotate_tac 1 1);
   11.39 +by (Asm_full_simp_tac 1);
   11.40 +by (rtac below_bound 1);
   11.41 +by (assume_tac 2);
   11.42 +by (rtac Least_is_bound 1);
   11.43 +qed "deg_belowI";
   11.44 +
   11.45 +Goalw [coeff_def, deg_def]
   11.46 +  "deg p < m ==> coeff m p = 0";
   11.47 +by (rtac exE 1); (* create !! x. *)
   11.48 +by (rtac boundD 2);
   11.49 +by (assume_tac 3);
   11.50 +by (rtac LeastI 2);
   11.51 +by (assume_tac 2);
   11.52 +by (res_inst_tac [("a", "Rep_UP p")] CollectD 1);
   11.53 +by (rtac (rewrite_rule [UP_def] Rep_UP) 1);
   11.54 +qed "deg_aboveD";
   11.55 +
   11.56 +Goalw [deg_def]
   11.57 +  "deg p = Suc y ==> ~ bound y (Rep_UP p)";
   11.58 +by (rtac not_less_Least 1);
   11.59 +by (Asm_simp_tac 1);
   11.60 +val lemma1 = result();
   11.61 +
   11.62 +Goalw [deg_def, coeff_def]
   11.63 +  "deg p = Suc y ==> coeff (deg p) p ~= 0";
   11.64 +by (rtac ccontr 1);
   11.65 +by (dtac notnotD 1);
   11.66 +by (cut_inst_tac [("p", "p")] Least_is_bound 1);
   11.67 +by (subgoal_tac "bound y (Rep_UP p)" 1);
   11.68 +(* prove subgoal *)
   11.69 +by (rtac boundI 2);  
   11.70 +by (case_tac "Suc y < m" 2);
   11.71 +(* first case *)
   11.72 +by (rtac boundD 2);  
   11.73 +by (assume_tac 2);
   11.74 +by (Asm_simp_tac 2);
   11.75 +(* second case *)
   11.76 +by (dtac leI 2);
   11.77 +by (dtac Suc_leI 2);
   11.78 +by (dtac le_anti_sym 2);
   11.79 +by (assume_tac 2);
   11.80 +by (Asm_full_simp_tac 2);
   11.81 +(* end prove subgoal *)
   11.82 +by (fold_goals_tac [deg_def]);
   11.83 +by (dtac lemma1 1);
   11.84 +by (etac notE 1);
   11.85 +by (assume_tac 1);
   11.86 +val lemma2 = result();
   11.87 +
   11.88 +Goal "deg p ~= 0 ==> coeff (deg p) p ~= 0";
   11.89 +by (rtac lemma2 1);
   11.90 +by (Full_simp_tac 1);
   11.91 +by (dtac Suc_pred 1);
   11.92 +by (rtac sym 1);
   11.93 +by (Asm_simp_tac 1);
   11.94 +qed "deg_lcoeff";
   11.95 +
   11.96 +Goal "p ~= 0 ==> coeff (deg p) p ~= 0";
   11.97 +by (etac contrapos_np 1); 
   11.98 +by (case_tac "deg p = 0" 1);
   11.99 +by (blast_tac (claset() addSDs [deg_lcoeff]) 2); 
  11.100 +by (rtac up_eqI 1);
  11.101 +by (case_tac "n=0" 1);
  11.102 +by (rotate_tac ~2 1);
  11.103 +by (Asm_full_simp_tac 1);
  11.104 +by (asm_full_simp_tac (simpset() addsimps [deg_aboveD]) 1);
  11.105 +qed "nonzero_lcoeff";
  11.106 +
  11.107 +Goal "(deg p <= n) = bound n (Rep_UP p)";
  11.108 +by (rtac iffI 1);
  11.109 +(* ==> *)
  11.110 +by (rtac boundI 1);
  11.111 +by (fold_goals_tac [coeff_def]);
  11.112 +by (rtac deg_aboveD 1);
  11.113 +by (fast_arith_tac 1);
  11.114 +(* <== *)
  11.115 +by (rtac deg_aboveI 1);
  11.116 +by (rewtac coeff_def);
  11.117 +by (Fast_tac 1);
  11.118 +qed "deg_above_is_bound";
  11.119 +
  11.120 +(* Lemmas on the degree function *)
  11.121 +
  11.122 +Goalw [max_def]
  11.123 +  "!! p::'a::ring up. deg (p + q) <= max (deg p) (deg q)";
  11.124 +by (case_tac "deg p <= deg q" 1);
  11.125 +(* case deg p <= deg q *)
  11.126 +by (rtac deg_aboveI 1);
  11.127 +by (Asm_simp_tac 1);
  11.128 +by (strip_tac 1);
  11.129 +by (dtac le_less_trans 1);
  11.130 +by (assume_tac 1);
  11.131 +by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
  11.132 +(* case deg p > deg q *)
  11.133 +by (rtac deg_aboveI 1);
  11.134 +by (Asm_simp_tac 1);
  11.135 +by (dtac not_leE 1);
  11.136 +by (strip_tac 1);
  11.137 +by (dtac less_trans 1);
  11.138 +by (assume_tac 1);
  11.139 +by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
  11.140 +qed "deg_add";
  11.141 +
  11.142 +Goal "!!p::('a::ring up). deg p < deg q ==> deg (p + q) = deg q";
  11.143 +by (rtac order_antisym 1);
  11.144 +by (rtac le_trans 1);
  11.145 +by (rtac deg_add 1);
  11.146 +by (Asm_simp_tac 1);
  11.147 +by (rtac deg_belowI 1);
  11.148 +by (asm_simp_tac (simpset() addsimps [deg_aboveD, deg_lcoeff]) 1);
  11.149 +qed "deg_add_equal";
  11.150 +
  11.151 +Goal "deg (monom m::'a::ring up) <= m";
  11.152 +by (asm_simp_tac 
  11.153 +  (simpset() addsimps [deg_aboveI, less_not_refl2 RS not_sym]) 1);
  11.154 +qed "deg_monom_ring";
  11.155 +
  11.156 +Goal "deg (monom m::'a::domain up) = m";
  11.157 +by (rtac le_anti_sym 1);
  11.158 +(* <= *)
  11.159 +by (rtac deg_monom_ring 1);
  11.160 +(* >= *)
  11.161 +by (asm_simp_tac 
  11.162 +  (simpset() addsimps [deg_belowI, less_not_refl2 RS not_sym]) 1);
  11.163 +qed "deg_monom";
  11.164 +
  11.165 +Goal "!! a::'a::ring. deg (const a) = 0";
  11.166 +by (rtac le_anti_sym 1);
  11.167 +by (rtac deg_aboveI 1);
  11.168 +by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
  11.169 +by (rtac deg_belowI 1);
  11.170 +by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
  11.171 +qed "deg_const";
  11.172 +
  11.173 +Goal "deg (0::'a::ringS up) = 0";
  11.174 +by (rtac le_anti_sym 1);
  11.175 +by (rtac deg_aboveI 1);
  11.176 +by (Simp_tac 1);
  11.177 +by (rtac deg_belowI 1);
  11.178 +by (Simp_tac 1);
  11.179 +qed "deg_zero";
  11.180 +
  11.181 +Goal "deg (<1>::'a::ring up) = 0";
  11.182 +by (rtac le_anti_sym 1);
  11.183 +by (rtac deg_aboveI 1);
  11.184 +by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
  11.185 +by (rtac deg_belowI 1);
  11.186 +by (Simp_tac 1);
  11.187 +qed "deg_one";
  11.188 +
  11.189 +Goal "!!p::('a::ring) up. deg (-p) = deg p";
  11.190 +by (rtac le_anti_sym 1);
  11.191 +(* <= *)
  11.192 +by (simp_tac (simpset() addsimps [deg_aboveI, deg_aboveD]) 1);
  11.193 +by (simp_tac (simpset() addsimps [deg_belowI, deg_lcoeff, uminus_monom_neq]) 1);
  11.194 +qed "deg_uminus";
  11.195 +
  11.196 +Addsimps [deg_monom, deg_const, deg_zero, deg_one, deg_uminus];
  11.197 +
  11.198 +Goal
  11.199 +  "!! a::'a::ring. deg (a *s p) <= (if a = 0 then 0 else deg p)";
  11.200 +by (case_tac "a = 0" 1);
  11.201 +by (REPEAT (asm_simp_tac (simpset() addsimps [deg_aboveI, deg_aboveD]) 1));
  11.202 +qed "deg_smult_ring";
  11.203 +
  11.204 +Goal
  11.205 +  "!! a::'a::domain. deg (a *s p) = (if a = 0 then 0 else deg p)";
  11.206 +by (rtac le_anti_sym 1);
  11.207 +by (rtac deg_smult_ring 1);
  11.208 +by (case_tac "a = 0" 1);
  11.209 +by (REPEAT (asm_simp_tac (simpset() addsimps [deg_belowI, deg_lcoeff]) 1));
  11.210 +qed "deg_smult";
  11.211 +
  11.212 +Goal
  11.213 +  "!! p::'a::ring up. [| deg p + deg q < k |] ==> \
  11.214 +\       coeff i p * coeff (k - i) q = 0";
  11.215 +by (simp_tac (simpset() addsimps [coeff_def]) 1);
  11.216 +by (rtac bound_mult_zero 1);
  11.217 +by (assume_tac 3);
  11.218 +by (simp_tac (simpset() addsimps [deg_above_is_bound RS sym]) 1);
  11.219 +by (simp_tac (simpset() addsimps [deg_above_is_bound RS sym]) 1);
  11.220 +qed "deg_above_mult_zero";
  11.221 +
  11.222 +Goal
  11.223 +  "!! p::'a::ring up. deg (p * q) <= deg p + deg q";
  11.224 +by (rtac deg_aboveI 1);
  11.225 +by (asm_simp_tac (simpset() addsimps [deg_above_mult_zero]) 1);
  11.226 +qed "deg_mult_ring";
  11.227 +
  11.228 +goal Main.thy 
  11.229 +  "!!k::nat. k < n ==> m < n + m - k";
  11.230 +by (arith_tac 1);
  11.231 +qed "less_add_diff";
  11.232 +
  11.233 +Goal "!!p. coeff n p ~= 0 ==> n <= deg p";
  11.234 +(* More general than deg_belowI, and simplifies the next proof! *)
  11.235 +by (rtac deg_belowI 1);
  11.236 +by (Fast_tac 1);
  11.237 +qed "deg_below2I";
  11.238 +
  11.239 +Goal
  11.240 +  "!! p::'a::domain up. \
  11.241 +\    [| p ~= 0; q ~= 0 |] ==> deg (p * q) = deg p + deg q";
  11.242 +by (rtac le_anti_sym 1);
  11.243 +by (rtac deg_mult_ring 1);
  11.244 +(* deg p + deg q <= deg (p * q) *)
  11.245 +by (rtac deg_below2I 1);
  11.246 +by (Simp_tac 1);
  11.247 +(*
  11.248 +by (rtac conjI 1);
  11.249 +by (rtac impI 1);
  11.250 +*)
  11.251 +by (res_inst_tac [("m", "deg p"), ("n", "deg p + deg q")] SUM_extend 1);
  11.252 +by (rtac le_add1 1);
  11.253 +by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
  11.254 +by (res_inst_tac [("m", "deg p"), ("n", "deg p")] SUM_extend_below 1);
  11.255 +by (rtac le_refl 1);
  11.256 +by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
  11.257 +by (asm_simp_tac (simpset() addsimps [nonzero_lcoeff]) 1);
  11.258 +(*
  11.259 +by (rtac impI 1);
  11.260 +by (res_inst_tac [("m", "deg p"), ("n", "deg p + deg q")] SUM_extend 1);
  11.261 +by (rtac le_add1 1);
  11.262 +by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
  11.263 +by (res_inst_tac [("m", "deg p"), ("n", "deg p")] SUM_extend_below 1);
  11.264 +by (rtac le_refl 1);
  11.265 +by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
  11.266 +by (asm_simp_tac (simpset() addsimps [nonzero_lcoeff]) 1);
  11.267 +*)
  11.268 +qed "deg_mult";
  11.269 +
  11.270 +Addsimps [deg_smult, deg_mult];
  11.271 +
  11.272 +(* Representation theorems about polynomials *)
  11.273 +
  11.274 +goal PolyRing.thy
  11.275 +  "!! p::nat=>'a::ring up. \
  11.276 +\    coeff k (setsum p {..n}) = setsum (%i. coeff k (p i)) {..n}";
  11.277 +by (induct_tac "n" 1);
  11.278 +by Auto_tac;
  11.279 +qed "coeff_SUM";
  11.280 +
  11.281 +goal UnivPoly2.thy
  11.282 +  "!! f::(nat=>'a::ring). \
  11.283 +\    bound n f ==> setsum (%i. if i = x then f i else 0) {..n} = f x";
  11.284 +by (simp_tac (simpset() addsimps [SUM_if_singleton]) 1);
  11.285 +by (auto_tac
  11.286 +    (claset() addDs [not_leE],
  11.287 +     simpset()));
  11.288 +qed "bound_SUM_if";
  11.289 +
  11.290 +Goal
  11.291 +  "!! p::'a::ring up. deg p <= n ==> \
  11.292 +\  setsum (%i. coeff i p *s monom i) {..n} = p";
  11.293 +by (rtac up_eqI 1);
  11.294 +by (simp_tac (simpset() addsimps [coeff_SUM]) 1);
  11.295 +by (rtac trans 1);
  11.296 +by (res_inst_tac [("x", "na")] bound_SUM_if 2);
  11.297 +by (full_simp_tac (simpset() addsimps [deg_above_is_bound, coeff_def]) 2);
  11.298 +by (rtac SUM_cong 1);
  11.299 +by (rtac refl 1);
  11.300 +by (Asm_simp_tac 1);
  11.301 +qed "up_repr";
  11.302 +
  11.303 +Goal
  11.304 +  "!! p::'a::ring up. [| deg p <= n; P p |] ==> \
  11.305 +\  P (setsum (%i. coeff i p *s monom i) {..n})";
  11.306 +by (asm_simp_tac (simpset() addsimps [up_repr]) 1);
  11.307 +qed "up_reprD";
  11.308 +
  11.309 +Goal
  11.310 +  "!! p::'a::ring up. \
  11.311 +\  [| deg p <= n; P (setsum (%i. coeff i p *s monom i) {..n}) |] \
  11.312 +\    ==> P p";
  11.313 +by (asm_full_simp_tac (simpset() addsimps [up_repr]) 1);
  11.314 +qed "up_repr2D";
  11.315 +
  11.316 +(*
  11.317 +Goal
  11.318 +  "!! p::'a::ring up. [| deg p <= n; deg q <= m |] ==> \
  11.319 +\    (SUM n (%i. coeff i p *s monom i) = SUM m (%i. coeff i q *s monom i)) \
  11.320 +\    = (coeff k f = coeff k g)
  11.321 +...
  11.322 +qed "up_unique";
  11.323 +*)
  11.324 +
  11.325 +(* Polynomials over integral domains are again integral domains *)
  11.326 +
  11.327 +Goal "!!p::'a::domain up. p * q = 0 ==> p = 0 | q = 0";
  11.328 +by (rtac classical 1);
  11.329 +by (subgoal_tac "deg p = 0 & deg q = 0" 1);
  11.330 +by (res_inst_tac [("p", "p"), ("n", "0")] up_repr2D 1);
  11.331 +by (Asm_simp_tac 1);
  11.332 +by (res_inst_tac [("p", "q"), ("n", "0")] up_repr2D 1);
  11.333 +by (Asm_simp_tac 1);
  11.334 +by (subgoal_tac "coeff 0 p = 0 | coeff 0 q = 0" 1);
  11.335 +by (force_tac (claset() addIs [up_eqI], simpset()) 1);
  11.336 +by (rtac integral 1);
  11.337 +by (subgoal_tac "coeff 0 (p * q) = 0" 1);
  11.338 +by (Asm_simp_tac 2);
  11.339 +by (Full_simp_tac 1);
  11.340 +by (dres_inst_tac [("f", "deg")] arg_cong 1);
  11.341 +by (Asm_full_simp_tac 1);
  11.342 +qed "up_integral";
  11.343 +
  11.344 +Goal "!! a::'a::domain. a *s p = 0 ==> a = 0 | p = 0";
  11.345 +by (full_simp_tac (simpset() addsimps [const_mult_is_smult RS sym]) 1);
  11.346 +by (dtac up_integral 1);
  11.347 +by Auto_tac;
  11.348 +by (rtac (const_inj RS injD) 1);
  11.349 +by (Simp_tac 1);
  11.350 +qed "smult_integral";
  11.351 +*)
  11.352 +
  11.353 +(* Divisibility and degree *)
  11.354 +
  11.355 +Goalw [dvd_def]
  11.356 +  "!! p::'a::domain up. [| p dvd q; q ~= 0 |] ==> deg p <= deg q";
  11.357 +by (etac exE 1);
  11.358 +by (hyp_subst_tac 1);
  11.359 +by (case_tac "p = 0" 1);
  11.360 +by (case_tac "k = 0" 2);
  11.361 +by Auto_tac;
  11.362 +qed "dvd_imp_deg";
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Wed Apr 30 10:01:35 2003 +0200
    12.3 @@ -0,0 +1,779 @@
    12.4 +(*
    12.5 +  Title:     Univariate Polynomials
    12.6 +  Id:        $Id$
    12.7 +  Author:    Clemens Ballarin, started 9 December 1996
    12.8 +  Copyright: Clemens Ballarin
    12.9 +*)
   12.10 +
   12.11 +header {* Univariate Polynomials *}
   12.12 +
   12.13 +theory UnivPoly2 = Abstract:
   12.14 +
   12.15 +(* already proved in Finite_Set.thy
   12.16 +
   12.17 +lemma setsum_cong:
   12.18 +  "[| A = B; !!i. i : B ==> f i = g i |] ==> setsum f A = setsum g B"
   12.19 +proof -
   12.20 +  assume prems: "A = B" "!!i. i : B ==> f i = g i"
   12.21 +  show ?thesis
   12.22 +  proof (cases "finite B")
   12.23 +    case True
   12.24 +    then have "!!A. [| A = B; !!i. i : B ==> f i = g i |] ==>
   12.25 +      setsum f A = setsum g B"
   12.26 +    proof induct
   12.27 +      case empty thus ?case by simp
   12.28 +    next
   12.29 +      case insert thus ?case by simp
   12.30 +    qed
   12.31 +    with prems show ?thesis by simp
   12.32 +  next
   12.33 +    case False with prems show ?thesis by (simp add: setsum_def)
   12.34 +  qed
   12.35 +qed
   12.36 +*)
   12.37 +
   12.38 +(* Instruct simplifier to simplify assumptions introduced by congs.
   12.39 +   This makes setsum_cong more convenient to use, because assumptions
   12.40 +   like i:{m..n} get simplified (to m <= i & i <= n). *)
   12.41 +
   12.42 +ML_setup {* 
   12.43 +
   12.44 +Addcongs [thm "setsum_cong"];
   12.45 +Context.>> (fn thy => (simpset_ref_of thy :=
   12.46 +  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
   12.47 +
   12.48 +section {* Definition of type up *}
   12.49 +
   12.50 +constdefs
   12.51 +  bound  :: "[nat, nat => 'a::zero] => bool"
   12.52 +  "bound n f == (ALL i. n < i --> f i = 0)"
   12.53 +
   12.54 +lemma boundI [intro!]: "[| !! m. n < m ==> f m = 0 |] ==> bound n f"
   12.55 +proof (unfold bound_def)
   12.56 +qed fast
   12.57 +
   12.58 +lemma boundE [elim?]: "[| bound n f; (!! m. n < m ==> f m = 0) ==> P |] ==> P"
   12.59 +proof (unfold bound_def)
   12.60 +qed fast
   12.61 +
   12.62 +lemma boundD [dest]: "[| bound n f; n < m |] ==> f m = 0"
   12.63 +proof (unfold bound_def)
   12.64 +qed fast
   12.65 +
   12.66 +lemma bound_below:
   12.67 +  assumes bound: "bound m f" and nonzero: "f n ~= 0" shows "n <= m"
   12.68 +proof (rule classical)
   12.69 +  assume "~ ?thesis"
   12.70 +  then have "m < n" by arith
   12.71 +  with bound have "f n = 0" ..
   12.72 +  with nonzero show ?thesis by contradiction
   12.73 +qed
   12.74 +
   12.75 +typedef (UP)
   12.76 +  ('a) up = "{f :: nat => 'a::zero. EX n. bound n f}"
   12.77 +by (rule+)   (* Question: what does trace_rule show??? *)
   12.78 +
   12.79 +section {* Constants *}
   12.80 +
   12.81 +consts
   12.82 +  coeff  :: "['a up, nat] => ('a::zero)"
   12.83 +  monom  :: "['a::zero, nat] => 'a up"              ("(3_*X^/_)" [71, 71] 70)
   12.84 +  "*s"   :: "['a::{zero, times}, 'a up] => 'a up"   (infixl 70)
   12.85 +
   12.86 +defs
   12.87 +  coeff_def: "coeff p n == Rep_UP p n"
   12.88 +  monom_def: "monom a n == Abs_UP (%i. if i=n then a else 0)"
   12.89 +  smult_def: "a *s p == Abs_UP (%i. a * Rep_UP p i)"
   12.90 +
   12.91 +lemma coeff_bound_ex: "EX n. bound n (coeff p)"
   12.92 +proof -
   12.93 +  have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
   12.94 +  then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
   12.95 +  then show ?thesis ..
   12.96 +qed
   12.97 +  
   12.98 +lemma bound_coeff_obtain:
   12.99 +  assumes prem: "(!!n. bound n (coeff p) ==> P)" shows "P"
  12.100 +proof -
  12.101 +  have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
  12.102 +  then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
  12.103 +  with prem show P .
  12.104 +qed
  12.105 +
  12.106 +text {* Ring operations *}
  12.107 +
  12.108 +instance up :: (zero) zero ..
  12.109 +instance up :: (one) one ..
  12.110 +instance up :: (plus) plus ..
  12.111 +instance up :: (minus) minus ..
  12.112 +instance up :: (times) times ..
  12.113 +instance up :: (inverse) inverse ..
  12.114 +instance up :: (power) power ..
  12.115 +
  12.116 +defs
  12.117 +  up_add_def:	"p + q == Abs_UP (%n. Rep_UP p n + Rep_UP q n)"
  12.118 +  up_mult_def:  "p * q == Abs_UP (%n::nat. setsum
  12.119 +		     (%i. Rep_UP p i * Rep_UP q (n-i)) {..n})"
  12.120 +  up_zero_def:  "0 == monom 0 0"
  12.121 +  up_one_def:   "1 == monom 1 0"
  12.122 +  up_uminus_def:"- p == (- 1) *s p"
  12.123 +                (* easier to use than "Abs_UP (%i. - Rep_UP p i)" *)
  12.124 +                (* note: - 1 is different from -1; latter is of class number *)
  12.125 +
  12.126 +  up_minus_def:   "(a::'a::{plus, minus} up) - b == a + (-b)"
  12.127 +  up_inverse_def: "inverse (a::'a::{zero, one, times, inverse} up) == 
  12.128 +                     (if a dvd 1 then THE x. a*x = 1 else 0)"
  12.129 +  up_divide_def:  "(a::'a::{times, inverse} up) / b == a * inverse b"
  12.130 +  up_power_def:   "(a::'a::{one, times, power} up) ^ n ==
  12.131 +                     nat_rec 1 (%u b. b * a) n"
  12.132 +
  12.133 +subsection {* Effect of operations on coefficients *}
  12.134 +
  12.135 +lemma coeff_monom [simp]: "coeff (monom a m) n = (if m=n then a else 0)"
  12.136 +proof -
  12.137 +  have "(%n. if n = m then a else 0) : UP"
  12.138 +    using UP_def by force
  12.139 +  from this show ?thesis
  12.140 +    by (simp add: coeff_def monom_def Abs_UP_inverse Rep_UP)
  12.141 +qed
  12.142 +
  12.143 +lemma coeff_zero [simp]: "coeff 0 n = 0"
  12.144 +proof (unfold up_zero_def)
  12.145 +qed simp
  12.146 +
  12.147 +lemma coeff_one [simp]: "coeff 1 n = (if n=0 then 1 else 0)"
  12.148 +proof (unfold up_one_def)
  12.149 +qed simp
  12.150 +
  12.151 +(* term order
  12.152 +lemma coeff_smult [simp]: "coeff (a *s p) n = (a::'a::ring) * coeff p n"
  12.153 +proof -
  12.154 +  have "!!f. f : UP ==> (%n. a * f n) : UP"
  12.155 +    by (unfold UP_def) (force simp add: ring_simps)
  12.156 +*)      (* this force step is slow *)
  12.157 +(*  then show ?thesis
  12.158 +    apply (simp add: coeff_def smult_def Abs_UP_inverse Rep_UP)
  12.159 +qed
  12.160 +*)
  12.161 +lemma coeff_smult [simp]: "coeff (a *s p) n = (a::'a::ring) * coeff p n"
  12.162 +proof -
  12.163 +  have "Rep_UP p : UP ==> (%n. a * Rep_UP p n) : UP"
  12.164 +    by (unfold UP_def) (force simp add: ring_simps)
  12.165 +      (* this force step is slow *)
  12.166 +  then show ?thesis
  12.167 +    by (simp add: coeff_def smult_def Abs_UP_inverse Rep_UP)
  12.168 +qed
  12.169 +
  12.170 +lemma coeff_add [simp]: "coeff (p+q) n = (coeff p n + coeff q n::'a::ring)"
  12.171 +proof -
  12.172 +  {
  12.173 +    fix f g
  12.174 +    assume fup: "(f::nat=>'a::ring) : UP" and gup: "(g::nat=>'a::ring) : UP"
  12.175 +    have "(%i. f i + g i) : UP"
  12.176 +    proof -
  12.177 +      from fup obtain n where boundn: "bound n f"
  12.178 +	by (unfold UP_def) fast
  12.179 +      from gup obtain m where boundm: "bound m g"
  12.180 +	by (unfold UP_def) fast
  12.181 +      have "bound (max n m) (%i. (f i + g i))"
  12.182 +      proof
  12.183 +	fix i
  12.184 +	assume "max n m < i"
  12.185 +	with boundn and boundm show "f i + g i = 0"
  12.186 +          by (fastsimp simp add: ring_simps)
  12.187 +      qed
  12.188 +      then show "(%i. (f i + g i)) : UP"
  12.189 +	by (unfold UP_def) fast
  12.190 +    qed
  12.191 +  }
  12.192 +  then show ?thesis
  12.193 +    by (simp add: coeff_def up_add_def Abs_UP_inverse Rep_UP)
  12.194 +qed
  12.195 +
  12.196 +lemma coeff_mult [simp]:
  12.197 +  "coeff (p * q) n = (setsum (%i. coeff p i * coeff q (n-i)) {..n}::'a::ring)"
  12.198 +proof -
  12.199 +  {
  12.200 +    fix f g
  12.201 +    assume fup: "(f::nat=>'a::ring) : UP" and gup: "(g::nat=>'a::ring) : UP"
  12.202 +    have "(%n. setsum (%i. f i * g (n-i)) {..n}) : UP"
  12.203 +    proof -
  12.204 +      from fup obtain n where "bound n f"
  12.205 +	by (unfold UP_def) fast
  12.206 +      from gup obtain m where "bound m g"
  12.207 +	by (unfold UP_def) fast
  12.208 +      have "bound (n + m) (%n. setsum (%i. f i * g (n-i)) {..n})"
  12.209 +      proof
  12.210 +	fix k
  12.211 +	assume bound: "n + m < k"
  12.212 +	{
  12.213 +	  fix i
  12.214 +	  have "f i * g (k-i) = 0"
  12.215 +	  proof cases
  12.216 +	    assume "n < i"
  12.217 +	    show ?thesis by (auto! simp add: ring_simps)
  12.218 +	  next
  12.219 +	    assume "~ (n < i)"
  12.220 +	    with bound have "m < k-i" by arith
  12.221 +	    then show ?thesis by (auto! simp add: ring_simps)
  12.222 +	  qed
  12.223 +	}
  12.224 +	then show "setsum (%i. f i * g (k-i)) {..k} = 0"
  12.225 +	  by (simp add: ring_simps)
  12.226 +      qed
  12.227 +      then show "(%n. setsum (%i. f i * g (n-i)) {..n}) : UP"
  12.228 +	by (unfold UP_def) fast
  12.229 +    qed
  12.230 +  }
  12.231 +  then show ?thesis
  12.232 +    by (simp add: coeff_def up_mult_def Abs_UP_inverse Rep_UP)
  12.233 +qed
  12.234 +
  12.235 +lemma coeff_uminus [simp]: "coeff (-p) n = (-coeff p n::'a::ring)"
  12.236 +by (unfold up_uminus_def) (simp add: ring_simps)
  12.237 +
  12.238 +(* Other lemmas *)
  12.239 +
  12.240 +lemma up_eqI: assumes prem: "(!! n. coeff p n = coeff q n)" shows "p = q"
  12.241 +proof -
  12.242 +  have "p = Abs_UP (%u. Rep_UP p u)" by (simp add: Rep_UP_inverse)
  12.243 +  also from prem have "... = Abs_UP (Rep_UP q)" by (simp only: coeff_def)
  12.244 +  also have "... = q" by (simp add: Rep_UP_inverse)
  12.245 +  finally show ?thesis .
  12.246 +qed
  12.247 +
  12.248 +(* ML_setup {* Addsimprocs [ring_simproc] *} *)
  12.249 +
  12.250 +instance up :: (ring) ring
  12.251 +proof
  12.252 +  fix p q r :: "'a::ring up"
  12.253 +  fix n
  12.254 +  show "(p + q) + r = p + (q + r)"
  12.255 +    by (rule up_eqI) simp
  12.256 +  show "0 + p = p"
  12.257 +    by (rule up_eqI) simp
  12.258 +  show "(-p) + p = 0"
  12.259 +    by (rule up_eqI) simp
  12.260 +  show "p + q = q + p"
  12.261 +    by (rule up_eqI) simp
  12.262 +  show "(p * q) * r = p * (q * r)"
  12.263 +  proof (rule up_eqI)
  12.264 +    fix n 
  12.265 +    {
  12.266 +      fix k and a b c :: "nat=>'a::ring"
  12.267 +      have "k <= n ==> 
  12.268 +	setsum (%j. setsum (%i. a i * b (j-i)) {..j} * c (n-j)) {..k} = 
  12.269 +	setsum (%j. a j * setsum  (%i. b i * c (n-j-i)) {..k-j}) {..k}"
  12.270 +	(is "_ ==> ?eq k")
  12.271 +      proof (induct k)
  12.272 +	case 0 show ?case by simp
  12.273 +      next
  12.274 +	case (Suc k)
  12.275 +	then have "k <= n" by arith
  12.276 +	then have "?eq k" by (rule Suc)
  12.277 +	then show ?case
  12.278 +	  by (simp add: Suc_diff_le natsum_ldistr)
  12.279 +      qed
  12.280 +    }
  12.281 +    then show "coeff ((p * q) * r) n = coeff (p * (q * r)) n"
  12.282 +      by simp
  12.283 +  qed
  12.284 +  show "1 * p = p"
  12.285 +  proof (rule up_eqI)
  12.286 +    fix n
  12.287 +    show "coeff (1 * p) n = coeff p n"
  12.288 +    proof (cases n)
  12.289 +      case 0 then show ?thesis by simp
  12.290 +    next
  12.291 +      case Suc then show ?thesis by (simp del: natsum_Suc add: natsum_Suc2)
  12.292 +    qed
  12.293 +  qed
  12.294 +  show "(p + q) * r = p * r + q * r"
  12.295 +    by (rule up_eqI) simp
  12.296 +  show "p * q = q * p"
  12.297 +  proof (rule up_eqI)
  12.298 +    fix n 
  12.299 +    {
  12.300 +      fix k
  12.301 +      fix a b :: "nat=>'a::ring"
  12.302 +      have "k <= n ==> 
  12.303 +	setsum (%i. a i * b (n-i)) {..k} =
  12.304 +	setsum (%i. a (k-i) * b (i+n-k)) {..k}"
  12.305 +	(is "_ ==> ?eq k")
  12.306 +      proof (induct k)
  12.307 +	case 0 show ?case by simp
  12.308 +      next
  12.309 +	case (Suc k) then show ?case by (subst natsum_Suc2) simp
  12.310 +      qed
  12.311 +    }
  12.312 +    then show "coeff (p * q) n = coeff (q * p) n"
  12.313 +      by simp
  12.314 +  qed
  12.315 +
  12.316 +  show "p - q = p + (-q)"
  12.317 +    by (simp add: up_minus_def)
  12.318 +  show "inverse p = (if p dvd 1 then THE x. p*x = 1 else 0)"
  12.319 +    by (simp add: up_inverse_def)
  12.320 +  show "p / q = p * inverse q"
  12.321 +    by (simp add: up_divide_def)
  12.322 +  show "p ^ n = nat_rec 1 (%u b. b * p) n"
  12.323 +    by (simp add: up_power_def)
  12.324 +  qed
  12.325 +
  12.326 +(* Further properties of monom *)
  12.327 +
  12.328 +lemma monom_zero [simp]:
  12.329 +  "monom 0 n = 0"
  12.330 +  by (simp add: monom_def up_zero_def)
  12.331 +(* term order: application of coeff_mult goes wrong: rule not symmetric
  12.332 +lemma monom_mult_is_smult:
  12.333 +  "monom (a::'a::ring) 0 * p = a *s p"
  12.334 +proof (rule up_eqI)
  12.335 +  fix k
  12.336 +  show "coeff (monom a 0 * p) k = coeff (a *s p) k"
  12.337 +  proof (cases k)
  12.338 +    case 0 then show ?thesis by simp
  12.339 +  next
  12.340 +    case Suc then show ?thesis by simp
  12.341 +  qed
  12.342 +qed
  12.343 +*)
  12.344 +ML_setup {* Delsimprocs [ring_simproc] *}
  12.345 +
  12.346 +lemma monom_mult_is_smult:
  12.347 +  "monom (a::'a::ring) 0 * p = a *s p"
  12.348 +proof (rule up_eqI)
  12.349 +  fix k
  12.350 +  have "coeff (p * monom a 0) k = coeff (a *s p) k"
  12.351 +  proof (cases k)
  12.352 +    case 0 then show ?thesis by simp ring
  12.353 +  next
  12.354 +    case Suc then show ?thesis by (simp add: ring_simps) ring
  12.355 +  qed
  12.356 +  then show "coeff (monom a 0 * p) k = coeff (a *s p) k" by ring
  12.357 +qed
  12.358 +
  12.359 +ML_setup {* Addsimprocs [ring_simproc] *}
  12.360 +
  12.361 +lemma monom_add [simp]:
  12.362 +  "monom (a + b) n = monom (a::'a::ring) n + monom b n"
  12.363 +by (rule up_eqI) simp
  12.364 +
  12.365 +lemma monom_mult_smult:
  12.366 +  "monom (a * b) n = a *s monom (b::'a::ring) n"
  12.367 +by (rule up_eqI) simp
  12.368 +
  12.369 +lemma monom_uminus [simp]:
  12.370 +  "monom (-a) n = - monom (a::'a::ring) n"
  12.371 +by (rule up_eqI) simp
  12.372 +
  12.373 +lemma monom_one [simp]:
  12.374 +  "monom 1 0 = 1"
  12.375 +by (simp add: up_one_def)
  12.376 +
  12.377 +lemma monom_inj:
  12.378 +  "(monom a n = monom b n) = (a = b)"
  12.379 +proof
  12.380 +  assume "monom a n = monom b n"
  12.381 +  then have "coeff (monom a n) n = coeff (monom b n) n" by simp
  12.382 +  then show "a = b" by simp
  12.383 +next
  12.384 +  assume "a = b" then show "monom a n = monom b n" by simp
  12.385 +qed
  12.386 +
  12.387 +(* Properties of *s:
  12.388 +   Polynomials form a module *)
  12.389 +
  12.390 +lemma smult_l_distr:
  12.391 +  "(a + b::'a::ring) *s p = a *s p + b *s p"
  12.392 +by (rule up_eqI) simp
  12.393 +
  12.394 +lemma smult_r_distr:
  12.395 +  "(a::'a::ring) *s (p + q) = a *s p + a *s q"
  12.396 +by (rule up_eqI) simp
  12.397 +
  12.398 +lemma smult_assoc1:
  12.399 +  "(a * b::'a::ring) *s p = a *s (b *s p)"
  12.400 +by (rule up_eqI) simp
  12.401 +
  12.402 +lemma smult_one [simp]:
  12.403 +  "(1::'a::ring) *s p = p"
  12.404 +by (rule up_eqI) simp
  12.405 +
  12.406 +(* Polynomials form an algebra *)
  12.407 +
  12.408 +ML_setup {* Delsimprocs [ring_simproc] *}
  12.409 +
  12.410 +lemma smult_assoc2:
  12.411 +  "(a *s p) * q = (a::'a::ring) *s (p * q)"
  12.412 +by (rule up_eqI) (simp add: natsum_rdistr m_assoc)
  12.413 +(* Simproc fails. *)
  12.414 +
  12.415 +ML_setup {* Addsimprocs [ring_simproc] *}
  12.416 +
  12.417 +(* the following can be derived from the above ones,
  12.418 +   for generality reasons, it is therefore done *)
  12.419 +
  12.420 +lemma smult_l_null [simp]:
  12.421 +  "(0::'a::ring) *s p = 0"
  12.422 +proof -
  12.423 +  fix a
  12.424 +  have "0 *s p = (0 *s p + a *s p) + - (a *s p)" by simp
  12.425 +  also have "... = (0 + a) *s p + - (a *s p)" by (simp only: smult_l_distr)
  12.426 +  also have "... = 0" by simp
  12.427 +  finally show ?thesis .
  12.428 +qed
  12.429 +
  12.430 +lemma smult_r_null [simp]:
  12.431 +  "(a::'a::ring) *s 0 = 0";
  12.432 +proof -
  12.433 +  fix p
  12.434 +  have "a *s 0 = (a *s 0 + a *s p) + - (a *s p)" by simp
  12.435 +  also have "... = a *s (0 + p) + - (a *s p)" by (simp only: smult_r_distr)
  12.436 +  also have "... = 0" by simp
  12.437 +  finally show ?thesis .
  12.438 +qed
  12.439 +
  12.440 +lemma smult_l_minus:
  12.441 +  "(-a::'a::ring) *s p = - (a *s p)"
  12.442 +proof -
  12.443 +  have "(-a) *s p = (-a *s p + a *s p) + -(a *s p)" by simp 
  12.444 +  also have "... = (-a + a) *s p + -(a *s p)" by (simp only: smult_l_distr)
  12.445 +  also have "... = -(a *s p)" by simp
  12.446 +  finally show ?thesis .
  12.447 +qed
  12.448 +
  12.449 +lemma smult_r_minus:
  12.450 +  "(a::'a::ring) *s (-p) = - (a *s p)"
  12.451 +proof -
  12.452 +  have "a *s (-p) = (a *s -p + a *s p) + -(a *s p)" by simp
  12.453 +  also have "... = a *s (-p + p) + -(a *s p)" by (simp only: smult_r_distr)
  12.454 +  also have "... = -(a *s p)" by simp
  12.455 +  finally show ?thesis .
  12.456 +qed
  12.457 +
  12.458 +section {* The degree function *}
  12.459 +
  12.460 +constdefs
  12.461 +  deg :: "('a::zero) up => nat"
  12.462 +  "deg p == LEAST n. bound n (coeff p)"
  12.463 +
  12.464 +lemma deg_aboveI:
  12.465 +  "(!!m. n < m ==> coeff p m = 0) ==> deg p <= n"
  12.466 +by (unfold deg_def) (fast intro: Least_le)
  12.467 +
  12.468 +lemma deg_aboveD:
  12.469 +  assumes prem: "deg p < m" shows "coeff p m = 0"
  12.470 +proof -
  12.471 +  obtain n where "bound n (coeff p)" by (rule bound_coeff_obtain)
  12.472 +  then have "bound (deg p) (coeff p)" by (unfold deg_def, rule LeastI)
  12.473 +  then show "coeff p m = 0" by (rule boundD)
  12.474 +qed
  12.475 +
  12.476 +lemma deg_belowI:
  12.477 +  assumes prem: "n ~= 0 ==> coeff p n ~= 0" shows "n <= deg p"
  12.478 +(* logically, this is a slightly stronger version of deg_aboveD *)
  12.479 +proof (cases "n=0")
  12.480 +  case True then show ?thesis by simp
  12.481 +next
  12.482 +  case False then have "coeff p n ~= 0" by (rule prem)
  12.483 +  then have "~ deg p < n" by (fast dest: deg_aboveD)
  12.484 +  then show ?thesis by arith
  12.485 +qed
  12.486 +
  12.487 +lemma lcoeff_nonzero_deg:
  12.488 +  assumes deg: "deg p ~= 0" shows "coeff p (deg p) ~= 0"
  12.489 +proof -
  12.490 +  obtain m where "deg p <= m" and m_coeff: "coeff p m ~= 0"
  12.491 +  proof -
  12.492 +    have minus: "!!(n::nat) m. n ~= 0 ==> (n - Suc 0 < m) = (n <= m)"
  12.493 +      by arith (* make public?, why does proof not work with "1" *)
  12.494 +    from deg have "deg p - 1 < (LEAST n. bound n (coeff p))"
  12.495 +      by (unfold deg_def) arith
  12.496 +    then have "~ bound (deg p - 1) (coeff p)" by (rule not_less_Least)
  12.497 +    then have "EX m. deg p - 1 < m & coeff p m ~= 0"
  12.498 +      by (unfold bound_def) fast
  12.499 +    then have "EX m. deg p <= m & coeff p m ~= 0" by (simp add: deg minus)
  12.500 +    then show ?thesis by auto 
  12.501 +  qed
  12.502 +  with deg_belowI have "deg p = m" by fastsimp
  12.503 +  with m_coeff show ?thesis by simp
  12.504 +qed
  12.505 +
  12.506 +lemma lcoeff_nonzero_nonzero:
  12.507 +  assumes deg: "deg p = 0" and nonzero: "p ~= 0" shows "coeff p 0 ~= 0"
  12.508 +proof -
  12.509 +  have "EX m. coeff p m ~= 0"
  12.510 +  proof (rule classical)
  12.511 +    assume "~ ?thesis"
  12.512 +    then have "p = 0" by (auto intro: up_eqI)
  12.513 +    with nonzero show ?thesis by contradiction
  12.514 +  qed
  12.515 +  then obtain m where coeff: "coeff p m ~= 0" ..
  12.516 +  then have "m <= deg p" by (rule deg_belowI)
  12.517 +  then have "m = 0" by (simp add: deg)
  12.518 +  with coeff show ?thesis by simp
  12.519 +qed
  12.520 +
  12.521 +lemma lcoeff_nonzero:
  12.522 +  "p ~= 0 ==> coeff p (deg p) ~= 0"
  12.523 +proof (cases "deg p = 0")
  12.524 +  case True
  12.525 +  assume "p ~= 0"
  12.526 +  with True show ?thesis by (simp add: lcoeff_nonzero_nonzero)
  12.527 +next
  12.528 +  case False
  12.529 +  assume "p ~= 0"
  12.530 +  with False show ?thesis by (simp add: lcoeff_nonzero_deg)
  12.531 +qed
  12.532 +
  12.533 +lemma deg_eqI:
  12.534 +  "[| !!m. n < m ==> coeff p m = 0;
  12.535 +      !!n. n ~= 0 ==> coeff p n ~= 0|] ==> deg p = n"
  12.536 +by (fast intro: le_anti_sym deg_aboveI deg_belowI)
  12.537 +
  12.538 +(* Degree and polynomial operations *)
  12.539 +
  12.540 +lemma deg_add [simp]:
  12.541 +  "deg ((p::'a::ring up) + q) <= max (deg p) (deg q)"
  12.542 +proof (cases "deg p <= deg q")
  12.543 +  case True show ?thesis by (rule deg_aboveI) (simp add: True deg_aboveD) 
  12.544 +next
  12.545 +  case False show ?thesis by (rule deg_aboveI) (simp add: False deg_aboveD)
  12.546 +qed
  12.547 +
  12.548 +lemma deg_monom_ring:
  12.549 +  "deg (monom a n::'a::ring up) <= n"
  12.550 +by (rule deg_aboveI) simp
  12.551 +
  12.552 +lemma deg_monom [simp]:
  12.553 +  "a ~= 0 ==> deg (monom a n::'a::ring up) = n"
  12.554 +by (fastsimp intro: le_anti_sym deg_aboveI deg_belowI)
  12.555 +
  12.556 +lemma deg_const [simp]:
  12.557 +  "deg (monom (a::'a::ring) 0) = 0"
  12.558 +proof (rule le_anti_sym)
  12.559 +  show "deg (monom a 0) <= 0" by (rule deg_aboveI) simp
  12.560 +next
  12.561 +  show "0 <= deg (monom a 0)" by (rule deg_belowI) simp
  12.562 +qed
  12.563 +
  12.564 +lemma deg_zero [simp]:
  12.565 +  "deg 0 = 0"
  12.566 +proof (rule le_anti_sym)
  12.567 +  show "deg 0 <= 0" by (rule deg_aboveI) simp
  12.568 +next
  12.569 +  show "0 <= deg 0" by (rule deg_belowI) simp
  12.570 +qed
  12.571 +
  12.572 +lemma deg_one [simp]:
  12.573 +  "deg 1 = 0"
  12.574 +proof (rule le_anti_sym)
  12.575 +  show "deg 1 <= 0" by (rule deg_aboveI) simp
  12.576 +next
  12.577 +  show "0 <= deg 1" by (rule deg_belowI) simp
  12.578 +qed
  12.579 +
  12.580 +lemma uminus_monom:
  12.581 +  "!!a::'a::ring. (-a = 0) = (a = 0)"
  12.582 +proof
  12.583 +  fix a::"'a::ring"
  12.584 +  assume "a = 0"
  12.585 +  then show "-a = 0" by simp
  12.586 +next
  12.587 +  fix a::"'a::ring"
  12.588 +  assume "- a = 0"
  12.589 +  then have "-(- a) = 0" by simp
  12.590 +  then show "a = 0" by simp
  12.591 +qed
  12.592 +
  12.593 +lemma deg_uminus [simp]:
  12.594 +  "deg (-p::('a::ring) up) = deg p"
  12.595 +proof (rule le_anti_sym)
  12.596 +  show "deg (- p) <= deg p" by (simp add: deg_aboveI deg_aboveD)
  12.597 +next
  12.598 +  show "deg p <= deg (- p)" 
  12.599 +  by (simp add: deg_belowI lcoeff_nonzero_deg uminus_monom)
  12.600 +qed
  12.601 +
  12.602 +lemma deg_smult_ring:
  12.603 +  "deg ((a::'a::ring) *s p) <= (if a = 0 then 0 else deg p)"
  12.604 +proof (cases "a = 0")
  12.605 +qed (simp add: deg_aboveI deg_aboveD)+
  12.606 +
  12.607 +lemma deg_smult [simp]:
  12.608 +  "deg ((a::'a::domain) *s p) = (if a = 0 then 0 else deg p)"
  12.609 +proof (rule le_anti_sym)
  12.610 +  show "deg (a *s p) <= (if a = 0 then 0 else deg p)" by (rule deg_smult_ring)
  12.611 +next
  12.612 +  show "(if a = 0 then 0 else deg p) <= deg (a *s p)"
  12.613 +  proof (cases "a = 0")
  12.614 +  qed (simp, simp add: deg_belowI lcoeff_nonzero_deg integral_iff)
  12.615 +qed
  12.616 +
  12.617 +lemma deg_mult_ring:
  12.618 +  "deg (p * q::'a::ring up) <= deg p + deg q"
  12.619 +proof (rule deg_aboveI)
  12.620 +  fix m
  12.621 +  assume boundm: "deg p + deg q < m"
  12.622 +  {
  12.623 +    fix k i
  12.624 +    assume boundk: "deg p + deg q < k"
  12.625 +    then have "coeff p i * coeff q (k - i) = 0"
  12.626 +    proof (cases "deg p < i")
  12.627 +      case True then show ?thesis by (simp add: deg_aboveD)
  12.628 +    next
  12.629 +      case False with boundk have "deg q < k - i" by arith
  12.630 +      then show ?thesis by (simp add: deg_aboveD)
  12.631 +    qed
  12.632 +  }
  12.633 +      (* This is similar to bound_mult_zero and deg_above_mult_zero in the old
  12.634 +         proofs. *)
  12.635 +  with boundm show "coeff (p * q) m = 0" by simp
  12.636 +qed
  12.637 +
  12.638 +lemma deg_mult [simp]:
  12.639 +  "[| (p::'a::domain up) ~= 0; q ~= 0|] ==> deg (p * q) = deg p + deg q"
  12.640 +proof (rule le_anti_sym)
  12.641 +  show "deg (p * q) <= deg p + deg q" by (rule deg_mult_ring)
  12.642 +next
  12.643 +  let ?s = "(%i. coeff p i * coeff q (deg p + deg q - i))"
  12.644 +  assume nz: "p ~= 0" "q ~= 0"
  12.645 +  have less_add_diff: "!!(k::nat) n m. k < n ==> m < n + m - k" by arith
  12.646 +  show "deg p + deg q <= deg (p * q)"
  12.647 +  proof (rule deg_belowI, simp)
  12.648 +    have "setsum ?s {.. deg p + deg q}
  12.649 +      = setsum ?s ({.. deg p(} Un {deg p .. deg p + deg q})"
  12.650 +      by (simp only: ivl_disj_un_one)
  12.651 +    also have "... = setsum ?s {deg p .. deg p + deg q}"
  12.652 +      by (simp add: setsum_Un_disjoint ivl_disj_int_one
  12.653 +        setsum_0 deg_aboveD less_add_diff)
  12.654 +    also have "... = setsum ?s ({deg p} Un {)deg p .. deg p + deg q})"
  12.655 +      by (simp only: ivl_disj_un_singleton)
  12.656 +    also have "... = coeff p (deg p) * coeff q (deg q)" 
  12.657 +      by (simp add: setsum_Un_disjoint ivl_disj_int_singleton 
  12.658 +        setsum_0 deg_aboveD)
  12.659 +    finally have "setsum ?s {.. deg p + deg q} 
  12.660 +      = coeff p (deg p) * coeff q (deg q)" .
  12.661 +    with nz show "setsum ?s {.. deg p + deg q} ~= 0"
  12.662 +      by (simp add: integral_iff lcoeff_nonzero)
  12.663 +    qed
  12.664 +  qed
  12.665 +
  12.666 +lemma coeff_natsum:
  12.667 +  "((coeff (setsum p A) k)::'a::ring) = 
  12.668 +   setsum (%i. coeff (p i) k) A"
  12.669 +proof (cases "finite A")
  12.670 +  case True then show ?thesis by induct auto
  12.671 +next
  12.672 +  case False then show ?thesis by (simp add: setsum_def)
  12.673 +qed
  12.674 +(* Instance of a more general result!!! *)
  12.675 +
  12.676 +(*
  12.677 +lemma coeff_natsum:
  12.678 +  "((coeff (setsum p {..n::nat}) k)::'a::ring) = 
  12.679 +   setsum (%i. coeff (p i) k) {..n}"
  12.680 +by (induct n) auto
  12.681 +*)
  12.682 +
  12.683 +lemma up_repr:
  12.684 +  "setsum (%i. monom (coeff p i) i) {..deg (p::'a::ring up)} = p"
  12.685 +proof (rule up_eqI)
  12.686 +  let ?s = "(%i. monom (coeff p i) i)"
  12.687 +  fix k
  12.688 +  show "coeff (setsum ?s {..deg p}) k = coeff p k"
  12.689 +  proof (cases "k <= deg p")
  12.690 +    case True
  12.691 +    hence "coeff (setsum ?s {..deg p}) k = 
  12.692 +          coeff (setsum ?s ({..k} Un {)k..deg p})) k"
  12.693 +      by (simp only: ivl_disj_un_one)
  12.694 +    also from True
  12.695 +    have "... = coeff (setsum ?s {..k}) k"
  12.696 +      by (simp add: setsum_Un_disjoint ivl_disj_int_one order_less_imp_not_eq2
  12.697 +        setsum_0 coeff_natsum )
  12.698 +    also
  12.699 +    have "... = coeff (setsum ?s ({..k(} Un {k})) k"
  12.700 +      by (simp only: ivl_disj_un_singleton)
  12.701 +    also have "... = coeff p k"
  12.702 +      by (simp add: setsum_Un_disjoint ivl_disj_int_singleton 
  12.703 +        setsum_0 coeff_natsum deg_aboveD)
  12.704 +    finally show ?thesis .
  12.705 +  next
  12.706 +    case False
  12.707 +    hence "coeff (setsum ?s {..deg p}) k = 
  12.708 +          coeff (setsum ?s ({..deg p(} Un {deg p})) k"
  12.709 +      by (simp only: ivl_disj_un_singleton)
  12.710 +    also from False have "... = coeff p k"
  12.711 +      by (simp add: setsum_Un_disjoint ivl_disj_int_singleton 
  12.712 +        setsum_0 coeff_natsum deg_aboveD)
  12.713 +    finally show ?thesis .
  12.714 +  qed
  12.715 +qed
  12.716 +
  12.717 +lemma up_repr_le:
  12.718 +  "deg (p::'a::ring up) <= n ==> setsum (%i. monom (coeff p i) i) {..n} = p"
  12.719 +proof -
  12.720 +  let ?s = "(%i. monom (coeff p i) i)"
  12.721 +  assume "deg p <= n"
  12.722 +  then have "setsum ?s {..n} = setsum ?s ({..deg p} Un {)deg p..n})"
  12.723 +    by (simp only: ivl_disj_un_one)
  12.724 +  also have "... = setsum ?s {..deg p}"
  12.725 +    by (simp add: setsum_Un_disjoint ivl_disj_int_one
  12.726 +      setsum_0 deg_aboveD)
  12.727 +  also have "... = p" by (rule up_repr)
  12.728 +  finally show ?thesis .
  12.729 +qed
  12.730 +
  12.731 +instance up :: ("domain") "domain"
  12.732 +proof
  12.733 +  show "1 ~= (0::'a up)"
  12.734 +  proof (* notI is applied here *)
  12.735 +    assume "1 = (0::'a up)"
  12.736 +    hence "coeff 1 0 = (coeff 0 0::'a)" by simp
  12.737 +    hence "1 = (0::'a)" by simp
  12.738 +    with one_not_zero show "False" by contradiction
  12.739 +  qed
  12.740 +next
  12.741 +  fix p q :: "'a::domain up"
  12.742 +  assume pq: "p * q = 0"
  12.743 +  show "p = 0 | q = 0"
  12.744 +  proof (rule classical)
  12.745 +    assume c: "~ (p = 0 | q = 0)"
  12.746 +    then have "deg p + deg q = deg (p * q)" by simp
  12.747 +    also from pq have "... = 0" by simp
  12.748 +    finally have "deg p + deg q = 0" .
  12.749 +    then have f1: "deg p = 0 & deg q = 0" by simp
  12.750 +    from f1 have "p = setsum (%i. (monom (coeff p i) i)) {..0}"
  12.751 +      by (simp only: up_repr_le)
  12.752 +    also have "... = monom (coeff p 0) 0" by simp
  12.753 +    finally have p: "p = monom (coeff p 0) 0" .
  12.754 +    from f1 have "q = setsum (%i. (monom (coeff q i) i)) {..0}"
  12.755 +      by (simp only: up_repr_le)
  12.756 +    also have "... = monom (coeff q 0) 0" by simp
  12.757 +    finally have q: "q = monom (coeff q 0) 0" .
  12.758 +    have "coeff p 0 * coeff q 0 = coeff (p * q) 0" by simp
  12.759 +    also from pq have "... = 0" by simp
  12.760 +    finally have "coeff p 0 * coeff q 0 = 0" .
  12.761 +    then have "coeff p 0 = 0 | coeff q 0 = 0" by (simp only: integral_iff)
  12.762 +    with p q show "p = 0 | q = 0" by fastsimp
  12.763 +  qed
  12.764 +qed
  12.765 +
  12.766 +lemma monom_inj_zero:
  12.767 +  "(monom a n = 0) = (a = 0)"
  12.768 +proof -
  12.769 +  have "(monom a n = 0) = (monom a n = monom 0 n)" by simp
  12.770 +  also have "... = (a = 0)" by (simp add: monom_inj del: monom_zero)
  12.771 +  finally show ?thesis .
  12.772 +qed
  12.773 +(* term order: makes this simpler!!!
  12.774 +lemma smult_integral:
  12.775 +  "(a::'a::domain) *s p = 0 ==> a = 0 | p = 0"
  12.776 +by (simp add: monom_mult_is_smult [THEN sym] integral_iff monom_inj_zero) fast
  12.777 +*)
  12.778 +lemma smult_integral:
  12.779 +  "(a::'a::domain) *s p = 0 ==> a = 0 | p = 0"
  12.780 +by (simp add: monom_mult_is_smult [THEN sym] integral_iff monom_inj_zero)
  12.781 +
  12.782 +end
  12.783 \ No newline at end of file
    13.1 --- a/src/HOL/Algebra/ringsimp.ML	Tue Apr 29 12:36:49 2003 +0200
    13.2 +++ b/src/HOL/Algebra/ringsimp.ML	Wed Apr 30 10:01:35 2003 +0200
    13.3 @@ -56,8 +56,8 @@
    13.4  (*** Term order for commutative rings ***)
    13.5  
    13.6  fun ring_ord a =
    13.7 -  find_index_eq a ["CRing.ring.zero", "CRing.ring.add", "Cring.ring.a_inv",
    13.8 -  "CRing.ring.minus", "Group.monoid.one", "Group.semigroup.mult"];
    13.9 +  find_index_eq a ["CRing.ring.zero", "CRing.ring.add", "CRing.a_inv",
   13.10 +  "CRing.minus", "Group.monoid.one", "Group.semigroup.mult"];
   13.11  
   13.12  fun termless_ring (a, b) = (term_lpo ring_ord (a, b) = LESS);
   13.13