Discontinued theories src/HOL/Algebra/abstract and .../poly.
authorballarin
Mon Mar 25 20:00:27 2013 +0100 (2013-03-25)
changeset 515177957d26c3334
parent 51516 237190475d79
child 51518 6a56b7088a6a
child 51533 3f6280aedbcc
Discontinued theories src/HOL/Algebra/abstract and .../poly.
NEWS
src/HOL/Algebra/README.html
src/HOL/Algebra/abstract/Abstract.thy
src/HOL/Algebra/abstract/Factor.thy
src/HOL/Algebra/abstract/Field.thy
src/HOL/Algebra/abstract/Ideal2.thy
src/HOL/Algebra/abstract/PID.thy
src/HOL/Algebra/abstract/Ring2.thy
src/HOL/Algebra/abstract/RingHomo.thy
src/HOL/Algebra/poly/LongDiv.thy
src/HOL/Algebra/poly/PolyHomo.thy
src/HOL/Algebra/poly/Polynomial.thy
src/HOL/Algebra/poly/UnivPoly2.thy
src/HOL/ROOT
     1.1 --- a/NEWS	Mon Mar 25 19:53:44 2013 +0100
     1.2 +++ b/NEWS	Mon Mar 25 20:00:27 2013 +0100
     1.3 @@ -92,6 +92,14 @@
     1.4        isar_shrink ~> isar_compress
     1.5  
     1.6  
     1.7 +*** HOL-Algebra ***
     1.8 +
     1.9 +* Discontinued theories src/HOL/Algebra/abstract and .../poly.
    1.10 +Existing theories should be based on src/HOL/Library/Polynomial
    1.11 +instead.  The latter provides integration with HOL's type classes for
    1.12 +rings.  INCOMPATIBILITY.
    1.13 +
    1.14 +
    1.15  *** System ***
    1.16  
    1.17  * Discontinued "isabelle usedir" option -P (remote path) and -r (reset
     2.1 --- a/src/HOL/Algebra/README.html	Mon Mar 25 19:53:44 2013 +0100
     2.2 +++ b/src/HOL/Algebra/README.html	Mon Mar 25 20:00:27 2013 +0100
     2.3 @@ -68,42 +68,10 @@
     2.4  	  Degree function.  Universal Property.
     2.5  </UL>
     2.6  
     2.7 -<H2>Legacy Development of Rings using Axiomatic Type Classes</H2>
     2.8 -
     2.9 -<P>This development of univariate polynomials is separated into an
    2.10 -abstract development of rings and the development of polynomials
    2.11 -itself. The formalisation is based on [Jacobson1985], and polynomials
    2.12 -have a sparse, mathematical representation. These theories were
    2.13 -developed as a base for the integration of a computer algebra system
    2.14 -to Isabelle [Ballarin1999], and was designed to match implementations
    2.15 -of these domains in some typed computer algebra systems.  Summary:
    2.16 -
    2.17 -<P><EM>Rings:</EM>
    2.18 -  Classes of rings are represented by axiomatic type classes. The
    2.19 -  following are available:
    2.20 +<H2>Development of Polynomials using Type Classes</H2>
    2.21  
    2.22 -<PRE>
    2.23 -  ring:		Commutative rings with one (including a summation
    2.24 -		operator, which is needed for the polynomials)
    2.25 -  domain:	Integral domains
    2.26 -  factorial:	Factorial domains (divisor chain condition is missing)
    2.27 -  pid:		Principal ideal domains
    2.28 -  field:	Fields
    2.29 -</PRE>
    2.30 -
    2.31 -  Also, some facts about ring homomorphisms and ideals are mechanised.
    2.32 -
    2.33 -<P><EM>Polynomials:</EM>
    2.34 -  Polynomials have a natural, mathematical representation. Facts about
    2.35 -  the following topics are provided:
    2.36 -
    2.37 -<MENU>
    2.38 -<LI>Degree function
    2.39 -<LI> Universal Property, evaluation homomorphism
    2.40 -<LI>Long division (existence and uniqueness)
    2.41 -<LI>Polynomials over a ring form a ring
    2.42 -<LI>Polynomials over an integral domain form an integral domain
    2.43 -</MENU>
    2.44 +<P>A development of univariate polynomials for HOL's ring classes
    2.45 +is available at <CODE>HOL/Library/Polynomial</CODE>.
    2.46  
    2.47  <P>[Jacobson1985] Nathan Jacobson, Basic Algebra I, Freeman, 1985.
    2.48  
     3.1 --- a/src/HOL/Algebra/abstract/Abstract.thy	Mon Mar 25 19:53:44 2013 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,10 +0,0 @@
     3.4 -(*  Author: Clemens Ballarin, started 17 July 1997
     3.5 -
     3.6 -Summary theory of the development of abstract algebra.
     3.7 -*)
     3.8 -
     3.9 -theory Abstract
    3.10 -imports RingHomo Field
    3.11 -begin
    3.12 -
    3.13 -end
     4.1 --- a/src/HOL/Algebra/abstract/Factor.thy	Mon Mar 25 19:53:44 2013 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,60 +0,0 @@
     4.4 -(*  Author: Clemens Ballarin, started 25 November 1997
     4.5 -
     4.6 -Factorisation within a factorial domain.
     4.7 -*)
     4.8 -
     4.9 -theory Factor
    4.10 -imports Ring2
    4.11 -begin
    4.12 -
    4.13 -definition
    4.14 -  Factorisation :: "['a::ring, 'a list, 'a] => bool" where
    4.15 -  (* factorisation of x into a list of irred factors and a unit u *)
    4.16 -  "Factorisation x factors u \<longleftrightarrow>
    4.17 -     x = foldr op* factors u &
    4.18 -     (ALL a : set factors. irred a) & u dvd 1"
    4.19 -
    4.20 -lemma irred_dvd_lemma: "!! c::'a::factorial.
    4.21 -   [| irred c; irred a; irred b; c dvd a*b |] ==> c assoc a | c assoc b"
    4.22 -  apply (unfold assoc_def)
    4.23 -  apply (frule factorial_prime)
    4.24 -  apply (unfold irred_def prime_def)
    4.25 -  apply blast
    4.26 -  done
    4.27 -
    4.28 -lemma irred_dvd_list_lemma: "!! c::'a::factorial.
    4.29 -   [| irred c; a dvd 1 |] ==>  
    4.30 -   (ALL b : set factors. irred b) & c dvd foldr op* factors a -->  
    4.31 -   (EX d. c assoc d & d : set factors)"
    4.32 -  apply (unfold assoc_def)
    4.33 -  apply (induct_tac factors)
    4.34 -  (* Base case: c dvd a contradicts irred c *)
    4.35 -   apply (simp add: irred_def)
    4.36 -   apply (blast intro: dvd_trans_ring)
    4.37 -  (* Induction step *)
    4.38 -  apply (frule factorial_prime)
    4.39 -  apply (simp add: irred_def prime_def)
    4.40 -  apply blast
    4.41 -  done
    4.42 -
    4.43 -lemma irred_dvd_list: "!! c::'a::factorial.  
    4.44 -   [| irred c; ALL b : set factors. irred b; a dvd 1;  
    4.45 -     c dvd foldr op* factors a |] ==>  
    4.46 -   EX d. c assoc d & d : set factors"
    4.47 -  apply (rule irred_dvd_list_lemma [THEN mp])
    4.48 -    apply auto
    4.49 -  done
    4.50 -
    4.51 -lemma Factorisation_dvd: "!! c::'a::factorial.  
    4.52 -   [| irred c; Factorisation x factors u; c dvd x |] ==>  
    4.53 -   EX d. c assoc d & d : set factors"
    4.54 -  apply (unfold Factorisation_def)
    4.55 -  apply (rule irred_dvd_list_lemma [THEN mp])
    4.56 -    apply auto
    4.57 -  done
    4.58 -
    4.59 -lemma Factorisation_irred: "!! c::'a::factorial.
    4.60 -    [| Factorisation x factors u; a : set factors |] ==> irred a"
    4.61 -  unfolding Factorisation_def by blast
    4.62 -
    4.63 -end
     5.1 --- a/src/HOL/Algebra/abstract/Field.thy	Mon Mar 25 19:53:44 2013 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,21 +0,0 @@
     5.4 -(*  Author: Clemens Ballarin, started 15 November 1997
     5.5 -
     5.6 -Properties of abstract class field.
     5.7 -*)
     5.8 -
     5.9 -theory Field
    5.10 -imports Factor PID
    5.11 -begin
    5.12 -
    5.13 -instance field < "domain"
    5.14 -  apply intro_classes
    5.15 -   apply (rule field_one_not_zero)
    5.16 -  apply (erule field_integral)
    5.17 -  done
    5.18 -
    5.19 -instance field < factorial
    5.20 -  apply intro_classes
    5.21 -  apply (erule field_fact_prime)
    5.22 -  done
    5.23 -
    5.24 -end
     6.1 --- a/src/HOL/Algebra/abstract/Ideal2.thy	Mon Mar 25 19:53:44 2013 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,324 +0,0 @@
     6.4 -(*  Author: Clemens Ballarin, started 24 September 1999
     6.5 -
     6.6 -Ideals for commutative rings.
     6.7 -*)
     6.8 -
     6.9 -theory Ideal2
    6.10 -imports Ring2
    6.11 -begin
    6.12 -
    6.13 -definition
    6.14 -  is_ideal :: "('a::ring) set => bool" where
    6.15 -  "is_ideal I \<longleftrightarrow> (ALL a: I. ALL b: I. a + b : I) &
    6.16 -                           (ALL a: I. - a : I) & 0 : I &
    6.17 -                           (ALL a: I. ALL r. a * r : I)"
    6.18 -
    6.19 -definition
    6.20 -  ideal_of :: "('a::ring) set => 'a set" where
    6.21 -  "ideal_of S = Inter {I. is_ideal I & S <= I}"
    6.22 -
    6.23 -definition
    6.24 -  is_pideal :: "('a::ring) set => bool" where
    6.25 -  "is_pideal I \<longleftrightarrow> (EX a. I = ideal_of {a})"
    6.26 -
    6.27 -
    6.28 -text {* Principle ideal domains *}
    6.29 -
    6.30 -class pid =
    6.31 -  assumes pid_ax: "is_ideal (I :: ('a::domain) set) \<Longrightarrow> is_pideal I"
    6.32 -
    6.33 -(* is_ideal *)
    6.34 -
    6.35 -lemma is_idealI:
    6.36 -  "!! I. [| !! a b. [| a:I; b:I |] ==> a + b : I;
    6.37 -      !! a. a:I ==> - a : I; 0 : I;
    6.38 -      !! a r. a:I ==> a * r : I |] ==> is_ideal I"
    6.39 -  unfolding is_ideal_def by blast
    6.40 -
    6.41 -lemma is_ideal_add [simp]: "[| is_ideal I; a:I; b:I |] ==> a + b : I"
    6.42 -  unfolding is_ideal_def by blast
    6.43 -
    6.44 -lemma is_ideal_uminus [simp]: "[| is_ideal I; a:I |] ==> - a : I"
    6.45 -  unfolding is_ideal_def by blast
    6.46 -
    6.47 -lemma is_ideal_zero [simp]: "[| is_ideal I |] ==> 0 : I"
    6.48 -  unfolding is_ideal_def by blast
    6.49 -
    6.50 -lemma is_ideal_mult [simp]: "[| is_ideal I; a:I |] ==> a * r : I"
    6.51 -  unfolding is_ideal_def by blast
    6.52 -
    6.53 -lemma is_ideal_dvd: "[| a dvd b; is_ideal I; a:I |] ==> b:I"
    6.54 -  unfolding is_ideal_def dvd_def by blast
    6.55 -
    6.56 -lemma UNIV_is_ideal [simp]: "is_ideal (UNIV::('a::ring) set)"
    6.57 -  unfolding is_ideal_def by blast
    6.58 -
    6.59 -lemma zero_is_ideal [simp]: "is_ideal {0::'a::ring}"
    6.60 -  unfolding is_ideal_def by auto
    6.61 -
    6.62 -lemma is_ideal_1: "is_ideal {x::'a::ring. a dvd x}"
    6.63 -  apply (rule is_idealI)
    6.64 -  apply auto
    6.65 -  done
    6.66 -
    6.67 -lemma is_ideal_2: "is_ideal {x::'a::ring. EX u v. x = a * u + b * v}"
    6.68 -  apply (rule is_idealI)
    6.69 -  apply auto
    6.70 -     apply (rule_tac x = "u+ua" in exI)
    6.71 -     apply (rule_tac x = "v+va" in exI)
    6.72 -     apply (rule_tac [2] x = "-u" in exI)
    6.73 -     apply (rule_tac [2] x = "-v" in exI)
    6.74 -     apply (rule_tac [3] x = "0" in exI)
    6.75 -     apply (rule_tac [3] x = "0" in exI)
    6.76 -     apply (rule_tac [4] x = "u * r" in exI)
    6.77 -     apply (rule_tac [4] x = "v * r" in exI)
    6.78 -  apply simp_all
    6.79 -  done
    6.80 -
    6.81 -
    6.82 -(* ideal_of *)
    6.83 -
    6.84 -lemma ideal_of_is_ideal: "is_ideal (ideal_of S)"
    6.85 -  unfolding is_ideal_def ideal_of_def by blast
    6.86 -
    6.87 -lemma generator_in_ideal: "a:S ==> a : (ideal_of S)"
    6.88 -  unfolding ideal_of_def by blast
    6.89 -
    6.90 -lemma ideal_of_one_eq: "ideal_of {1::'a::ring} = UNIV"
    6.91 -  apply (unfold ideal_of_def)
    6.92 -  apply (force dest: is_ideal_mult simp add: l_one)
    6.93 -  done
    6.94 -
    6.95 -lemma ideal_of_empty_eq: "ideal_of {} = {0::'a::ring}"
    6.96 -  apply (unfold ideal_of_def)
    6.97 -  apply (rule subset_antisym)
    6.98 -   apply (rule subsetI)
    6.99 -   apply (drule InterD)
   6.100 -    prefer 2 apply assumption
   6.101 -   apply (auto simp add: is_ideal_zero)
   6.102 -  done
   6.103 -
   6.104 -lemma pideal_structure: "ideal_of {a} = {x::'a::ring. a dvd x}"
   6.105 -  apply (unfold ideal_of_def)
   6.106 -  apply (rule subset_antisym)
   6.107 -   apply (rule subsetI)
   6.108 -   apply (drule InterD)
   6.109 -    prefer 2 apply assumption
   6.110 -   apply (auto intro: is_ideal_1)
   6.111 -  apply (simp add: is_ideal_dvd)
   6.112 -  done
   6.113 -
   6.114 -lemma ideal_of_2_structure:
   6.115 -    "ideal_of {a, b} = {x::'a::ring. EX u v. x = a * u + b * v}"
   6.116 -  apply (unfold ideal_of_def)
   6.117 -  apply (rule subset_antisym)
   6.118 -   apply (rule subsetI)
   6.119 -   apply (drule InterD)
   6.120 -    prefer 2 apply assumption
   6.121 -   using [[simproc del: ring]]
   6.122 -   apply (auto intro: is_ideal_2)
   6.123 -   using [[simproc ring]]
   6.124 -   apply (rule_tac x = "1" in exI)
   6.125 -   apply (rule_tac x = "0" in exI)
   6.126 -   apply (rule_tac [2] x = "0" in exI)
   6.127 -   apply (rule_tac [2] x = "1" in exI)
   6.128 -   apply simp
   6.129 -  apply simp
   6.130 -  done
   6.131 -
   6.132 -lemma ideal_of_mono: "A <= B ==> ideal_of A <= ideal_of B"
   6.133 -  unfolding ideal_of_def by blast
   6.134 -
   6.135 -lemma ideal_of_zero_eq: "ideal_of {0::'a::ring} = {0}"
   6.136 -  apply (simp add: pideal_structure)
   6.137 -  apply (rule subset_antisym)
   6.138 -   apply (auto intro: "dvd_zero_left")
   6.139 -  done
   6.140 -
   6.141 -lemma element_generates_subideal: "[| is_ideal I; a : I |] ==> ideal_of {a::'a::ring} <= I"
   6.142 -  apply (auto simp add: pideal_structure is_ideal_dvd)
   6.143 -  done
   6.144 -
   6.145 -
   6.146 -(* is_pideal *)
   6.147 -
   6.148 -lemma is_pideal_imp_is_ideal: "is_pideal (I::('a::ring) set) ==> is_ideal I"
   6.149 -  unfolding is_pideal_def by (fast intro: ideal_of_is_ideal)
   6.150 -
   6.151 -lemma pideal_is_pideal: "is_pideal (ideal_of {a::'a::ring})"
   6.152 -  unfolding is_pideal_def by blast
   6.153 -
   6.154 -lemma is_pidealD: "is_pideal I ==> EX a. I = ideal_of {a}"
   6.155 -  unfolding is_pideal_def .
   6.156 -
   6.157 -
   6.158 -(* Ideals and divisibility *)
   6.159 -
   6.160 -lemma dvd_imp_subideal: "b dvd a ==> ideal_of {a::'a::ring} <= ideal_of {b}"
   6.161 -  by (auto intro: dvd_trans_ring simp add: pideal_structure)
   6.162 -
   6.163 -lemma subideal_imp_dvd: "ideal_of {a::'a::ring} <= ideal_of {b} ==> b dvd a"
   6.164 -  by (auto dest!: subsetD simp add: pideal_structure)
   6.165 -
   6.166 -lemma psubideal_not_dvd: "(ideal_of {a::'a::ring} < ideal_of {b}) ==> ~ a dvd b"
   6.167 -  apply (simp add: psubset_eq pideal_structure)
   6.168 -  apply (erule conjE)
   6.169 -  apply (drule_tac c = "a" in subsetD)
   6.170 -   apply (auto intro: dvd_trans_ring)
   6.171 -  done
   6.172 -
   6.173 -lemma not_dvd_psubideal_singleton:
   6.174 -    "[| b dvd a; ~ a dvd b |] ==> ideal_of {a::'a::ring} < ideal_of {b}"
   6.175 -  apply (rule psubsetI)
   6.176 -   apply (erule dvd_imp_subideal)
   6.177 -  apply (blast intro: dvd_imp_subideal subideal_imp_dvd)
   6.178 -  done
   6.179 -
   6.180 -lemma subideal_is_dvd [iff]: "(ideal_of {a::'a::ring} <= ideal_of {b}) = (b dvd a)"
   6.181 -  apply (rule iffI)
   6.182 -   apply (assumption | rule subideal_imp_dvd dvd_imp_subideal)+
   6.183 -  done
   6.184 -
   6.185 -lemma psubideal_is_dvd [iff]: "(ideal_of {a::'a::ring} < ideal_of {b}) = (b dvd a & ~ a dvd b)"
   6.186 -  apply (rule iffI)
   6.187 -  apply (assumption | rule conjI psubideal_not_dvd psubset_imp_subset [THEN subideal_imp_dvd])+
   6.188 -  apply (erule conjE)
   6.189 -  apply (assumption | rule not_dvd_psubideal_singleton)+
   6.190 -  done
   6.191 -
   6.192 -lemma assoc_pideal_eq: "[| a dvd b; b dvd a |] ==> ideal_of {a::'a::ring} = ideal_of {b}"
   6.193 -  apply (rule subset_antisym)
   6.194 -  apply (assumption | rule dvd_imp_subideal)+
   6.195 -  done
   6.196 -
   6.197 -lemma dvd_imp_in_pideal: "!!a::'a::ring. a dvd b ==> b : (ideal_of {a})"
   6.198 -  apply (rule is_ideal_dvd)
   6.199 -    apply assumption
   6.200 -   apply (rule ideal_of_is_ideal)
   6.201 -  apply (rule generator_in_ideal)
   6.202 -  apply simp
   6.203 -  done
   6.204 -
   6.205 -lemma in_pideal_imp_dvd: "!!a::'a::ring. b : (ideal_of {a}) ==> a dvd b"
   6.206 -  by (simp add: pideal_structure)
   6.207 -
   6.208 -lemma not_dvd_psubideal: "~ (a dvd b) ==> ideal_of {a::'a::ring} < ideal_of {a, b}"
   6.209 -  apply (simp add: psubset_eq ideal_of_mono)
   6.210 -  apply (erule contrapos_pp)
   6.211 -  apply (simp add: ideal_of_2_structure)
   6.212 -  apply (rule in_pideal_imp_dvd)
   6.213 -  apply simp
   6.214 -  apply (rule_tac x = "0" in exI)
   6.215 -  apply (rule_tac x = "1" in exI)
   6.216 -  apply simp
   6.217 -  done
   6.218 -
   6.219 -lemma irred_imp_max_ideal:
   6.220 -    "[| irred (a::'a::ring); is_pideal I; ideal_of {a} < I |] ==> x : I"
   6.221 -  apply (unfold irred_def)
   6.222 -  apply (drule is_pidealD)
   6.223 -  apply (erule exE)
   6.224 -  apply clarify
   6.225 -  apply (erule_tac x = "aa" in allE)
   6.226 -  apply clarify
   6.227 -  apply (drule_tac a = "1" in dvd_imp_subideal)
   6.228 -  apply (auto simp add: ideal_of_one_eq)
   6.229 -  done
   6.230 -
   6.231 -(* Pid are factorial *)
   6.232 -
   6.233 -(* Divisor chain condition *)
   6.234 -(* proofs not finished *)
   6.235 -
   6.236 -lemma subset_chain_lemma [rule_format (no_asm)]:
   6.237 -  "(ALL i. I i <= I (Suc i)) ==> (n <= m & a : I n --> a : I m)"
   6.238 -  apply (induct_tac m)
   6.239 -   apply blast
   6.240 -  (* induction step *)
   6.241 -   apply (rename_tac m)
   6.242 -   apply (case_tac "n <= m")
   6.243 -    apply auto
   6.244 -  apply (subgoal_tac "n = Suc m")
   6.245 -   prefer 2
   6.246 -   apply arith
   6.247 -  apply force
   6.248 -  done
   6.249 -
   6.250 -lemma chain_is_ideal: "[| ALL i. is_ideal (I i); ALL i. I i <= I (Suc i) |]
   6.251 -    ==> is_ideal (Union (I`UNIV))"
   6.252 -  apply (rule is_idealI)
   6.253 -     apply auto
   6.254 -    apply (rule_tac x = "max x xa" in exI)
   6.255 -    apply (rule is_ideal_add)
   6.256 -      apply simp
   6.257 -     apply (rule subset_chain_lemma)
   6.258 -      apply assumption
   6.259 -     apply (rule conjI)
   6.260 -      prefer 2
   6.261 -      apply assumption
   6.262 -     apply arith
   6.263 -    apply (rule subset_chain_lemma)
   6.264 -    apply assumption
   6.265 -   apply (rule conjI)
   6.266 -     prefer 2
   6.267 -     apply assumption
   6.268 -    apply arith
   6.269 -   apply (rule_tac x = "x" in exI)
   6.270 -   apply simp
   6.271 -   apply (rule_tac x = "x" in exI)
   6.272 -   apply simp
   6.273 -   done
   6.274 -
   6.275 -
   6.276 -(* Primeness condition *)
   6.277 -
   6.278 -lemma pid_irred_imp_prime: "irred a ==> prime (a::'a::pid)"
   6.279 -  apply (unfold prime_def)
   6.280 -  apply (rule conjI)
   6.281 -   apply (rule_tac [2] conjI)
   6.282 -    apply (tactic "clarify_tac @{context} 3")
   6.283 -    apply (drule_tac [3] I = "ideal_of {a, b}" and x = "1" in irred_imp_max_ideal)
   6.284 -      apply (auto intro: ideal_of_is_ideal pid_ax simp add: irred_def not_dvd_psubideal pid_ax)
   6.285 -  apply (simp add: ideal_of_2_structure)
   6.286 -  apply clarify
   6.287 -  apply (drule_tac f = "op* aa" in arg_cong)
   6.288 -  apply (simp add: r_distr)
   6.289 -  apply (erule subst)
   6.290 -  using [[simproc del: ring]]
   6.291 -  apply (simp add: m_assoc [symmetric])
   6.292 -  done
   6.293 -
   6.294 -(* Fields are Pid *)
   6.295 -
   6.296 -lemma field_pideal_univ: "a ~= 0 ==> ideal_of {a::'a::field} = UNIV"
   6.297 -  apply (rule subset_antisym)
   6.298 -   apply simp
   6.299 -  apply (rule subset_trans)
   6.300 -   prefer 2
   6.301 -   apply (rule dvd_imp_subideal)
   6.302 -   apply (rule field_ax)
   6.303 -   apply assumption
   6.304 -  apply (simp add: ideal_of_one_eq)
   6.305 -  done
   6.306 -
   6.307 -lemma proper_ideal: "[| is_ideal I; I ~= {0} |] ==> {0} < I"
   6.308 -  by (simp add: psubset_eq not_sym is_ideal_zero)
   6.309 -
   6.310 -lemma field_pid: "is_ideal (I::('a::field) set) ==> is_pideal I"
   6.311 -  apply (unfold is_pideal_def)
   6.312 -  apply (case_tac "I = {0}")
   6.313 -   apply (rule_tac x = "0" in exI)
   6.314 -  apply (simp add: ideal_of_zero_eq)
   6.315 -  (* case "I ~= {0}" *)
   6.316 -  apply (frule proper_ideal)
   6.317 -   apply assumption
   6.318 -  apply (drule psubset_imp_ex_mem)
   6.319 -  apply (erule exE)
   6.320 -  apply (rule_tac x = b in exI)
   6.321 -  apply (cut_tac a = b in element_generates_subideal)
   6.322 -    apply assumption
   6.323 -   apply blast
   6.324 -  apply (auto simp add: field_pideal_univ)
   6.325 -  done
   6.326 -
   6.327 -end
     7.1 --- a/src/HOL/Algebra/abstract/PID.thy	Mon Mar 25 19:53:44 2013 +0100
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,15 +0,0 @@
     7.4 -(*  Author: Clemens Ballarin, started 5 October 1999
     7.5 -
     7.6 -Principle ideal domains.
     7.7 -*)
     7.8 -
     7.9 -theory PID
    7.10 -imports Ideal2
    7.11 -begin
    7.12 -
    7.13 -instance pid < factorial
    7.14 -  apply intro_classes
    7.15 -  apply (erule pid_irred_imp_prime)
    7.16 -  done
    7.17 -
    7.18 -end
     8.1 --- a/src/HOL/Algebra/abstract/Ring2.thy	Mon Mar 25 19:53:44 2013 +0100
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,485 +0,0 @@
     8.4 -(*  Title:     HOL/Algebra/abstract/Ring2.thy
     8.5 -    Author:    Clemens Ballarin
     8.6 -
     8.7 -The algebraic hierarchy of rings as axiomatic classes.
     8.8 -*)
     8.9 -
    8.10 -header {* The algebraic hierarchy of rings as type classes *}
    8.11 -
    8.12 -theory Ring2
    8.13 -imports Main
    8.14 -begin
    8.15 -
    8.16 -subsection {* Ring axioms *}
    8.17 -
    8.18 -class ring = zero + one + plus + minus + uminus + times + inverse + power + dvd +
    8.19 -  assumes a_assoc:      "(a + b) + c = a + (b + c)"
    8.20 -  and l_zero:           "0 + a = a"
    8.21 -  and l_neg:            "(-a) + a = 0"
    8.22 -  and a_comm:           "a + b = b + a"
    8.23 -
    8.24 -  assumes m_assoc:      "(a * b) * c = a * (b * c)"
    8.25 -  and l_one:            "1 * a = a"
    8.26 -
    8.27 -  assumes l_distr:      "(a + b) * c = a * c + b * c"
    8.28 -
    8.29 -  assumes m_comm:       "a * b = b * a"
    8.30 -
    8.31 -  assumes minus_def:    "a - b = a + (-b)"
    8.32 -  and inverse_def:      "inverse a = (if a dvd 1 then THE x. a*x = 1 else 0)"
    8.33 -  and divide_def:       "a / b = a * inverse b"
    8.34 -begin
    8.35 -
    8.36 -definition
    8.37 -  assoc :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "assoc" 50)
    8.38 -  where "a assoc b \<longleftrightarrow> a dvd b & b dvd a"
    8.39 -
    8.40 -definition
    8.41 -  irred :: "'a \<Rightarrow> bool" where
    8.42 -  "irred a \<longleftrightarrow> a ~= 0 & ~ a dvd 1 & (ALL d. d dvd a --> d dvd 1 | a dvd d)"
    8.43 -
    8.44 -definition
    8.45 -  prime :: "'a \<Rightarrow> bool" where
    8.46 -  "prime p \<longleftrightarrow> p ~= 0 & ~ p dvd 1 & (ALL a b. p dvd (a*b) --> p dvd a | p dvd b)"
    8.47 -
    8.48 -end
    8.49 -
    8.50 -
    8.51 -subsection {* Integral domains *}
    8.52 -
    8.53 -class "domain" = ring +
    8.54 -  assumes one_not_zero: "1 ~= 0"
    8.55 -  and integral: "a * b = 0 ==> a = 0 | b = 0"
    8.56 -
    8.57 -subsection {* Factorial domains *}
    8.58 -
    8.59 -class factorial = "domain" +
    8.60 -(*
    8.61 -  Proper definition using divisor chain condition currently not supported.
    8.62 -  factorial_divisor:    "wf {(a, b). a dvd b & ~ (b dvd a)}"
    8.63 -*)
    8.64 -  (*assumes factorial_divisor: "True"*)
    8.65 -  assumes factorial_prime: "irred a ==> prime a"
    8.66 -
    8.67 -
    8.68 -subsection {* Euclidean domains *}
    8.69 -
    8.70 -(*
    8.71 -class euclidean = "domain" +
    8.72 -  assumes euclidean_ax: "b ~= 0 ==> Ex (% (q, r, e_size::('a::ringS)=>nat).
    8.73 -                   a = b * q + r & e_size r < e_size b)"
    8.74 -
    8.75 -  Nothing has been proved about Euclidean domains, yet.
    8.76 -  Design question:
    8.77 -    Fix quo, rem and e_size as constants that are axiomatised with
    8.78 -    euclidean_ax?
    8.79 -    - advantage: more pragmatic and easier to use
    8.80 -    - disadvantage: for every type, one definition of quo and rem will
    8.81 -        be fixed, users may want to use differing ones;
    8.82 -        also, it seems not possible to prove that fields are euclidean
    8.83 -        domains, because that would require generic (type-independent)
    8.84 -        definitions of quo and rem.
    8.85 -*)
    8.86 -
    8.87 -subsection {* Fields *}
    8.88 -
    8.89 -class field = ring +
    8.90 -  assumes field_one_not_zero: "1 ~= 0"
    8.91 -                (* Avoid a common superclass as the first thing we will
    8.92 -                   prove about fields is that they are domains. *)
    8.93 -  and field_ax: "a ~= 0 ==> a dvd 1"
    8.94 -
    8.95 -
    8.96 -section {* Basic facts *}
    8.97 -
    8.98 -subsection {* Normaliser for rings *}
    8.99 -
   8.100 -(* derived rewrite rules *)
   8.101 -
   8.102 -lemma a_lcomm: "(a::'a::ring)+(b+c) = b+(a+c)"
   8.103 -  apply (rule a_comm [THEN trans])
   8.104 -  apply (rule a_assoc [THEN trans])
   8.105 -  apply (rule a_comm [THEN arg_cong])
   8.106 -  done
   8.107 -
   8.108 -lemma r_zero: "(a::'a::ring) + 0 = a"
   8.109 -  apply (rule a_comm [THEN trans])
   8.110 -  apply (rule l_zero)
   8.111 -  done
   8.112 -
   8.113 -lemma r_neg: "(a::'a::ring) + (-a) = 0"
   8.114 -  apply (rule a_comm [THEN trans])
   8.115 -  apply (rule l_neg)
   8.116 -  done
   8.117 -
   8.118 -lemma r_neg2: "(a::'a::ring) + (-a + b) = b"
   8.119 -  apply (rule a_assoc [symmetric, THEN trans])
   8.120 -  apply (simp add: r_neg l_zero)
   8.121 -  done
   8.122 -
   8.123 -lemma r_neg1: "-(a::'a::ring) + (a + b) = b"
   8.124 -  apply (rule a_assoc [symmetric, THEN trans])
   8.125 -  apply (simp add: l_neg l_zero)
   8.126 -  done
   8.127 -
   8.128 -
   8.129 -(* auxiliary *)
   8.130 -
   8.131 -lemma a_lcancel: "!! a::'a::ring. a + b = a + c ==> b = c"
   8.132 -  apply (rule box_equals)
   8.133 -  prefer 2
   8.134 -  apply (rule l_zero)
   8.135 -  prefer 2
   8.136 -  apply (rule l_zero)
   8.137 -  apply (rule_tac a1 = a in l_neg [THEN subst])
   8.138 -  apply (simp add: a_assoc)
   8.139 -  done
   8.140 -
   8.141 -lemma minus_add: "-((a::'a::ring) + b) = (-a) + (-b)"
   8.142 -  apply (rule_tac a = "a + b" in a_lcancel)
   8.143 -  apply (simp add: r_neg l_neg l_zero a_assoc a_comm a_lcomm)
   8.144 -  done
   8.145 -
   8.146 -lemma minus_minus: "-(-(a::'a::ring)) = a"
   8.147 -  apply (rule a_lcancel)
   8.148 -  apply (rule r_neg [THEN trans])
   8.149 -  apply (rule l_neg [symmetric])
   8.150 -  done
   8.151 -
   8.152 -lemma minus0: "- 0 = (0::'a::ring)"
   8.153 -  apply (rule a_lcancel)
   8.154 -  apply (rule r_neg [THEN trans])
   8.155 -  apply (rule l_zero [symmetric])
   8.156 -  done
   8.157 -
   8.158 -
   8.159 -(* derived rules for multiplication *)
   8.160 -
   8.161 -lemma m_lcomm: "(a::'a::ring)*(b*c) = b*(a*c)"
   8.162 -  apply (rule m_comm [THEN trans])
   8.163 -  apply (rule m_assoc [THEN trans])
   8.164 -  apply (rule m_comm [THEN arg_cong])
   8.165 -  done
   8.166 -
   8.167 -lemma r_one: "(a::'a::ring) * 1 = a"
   8.168 -  apply (rule m_comm [THEN trans])
   8.169 -  apply (rule l_one)
   8.170 -  done
   8.171 -
   8.172 -lemma r_distr: "(a::'a::ring) * (b + c) = a * b + a * c"
   8.173 -  apply (rule m_comm [THEN trans])
   8.174 -  apply (rule l_distr [THEN trans])
   8.175 -  apply (simp add: m_comm)
   8.176 -  done
   8.177 -
   8.178 -
   8.179 -(* the following proof is from Jacobson, Basic Algebra I, pp. 88-89 *)
   8.180 -lemma l_null: "0 * (a::'a::ring) = 0"
   8.181 -  apply (rule a_lcancel)
   8.182 -  apply (rule l_distr [symmetric, THEN trans])
   8.183 -  apply (simp add: r_zero)
   8.184 -  done
   8.185 -
   8.186 -lemma r_null: "(a::'a::ring) * 0 = 0"
   8.187 -  apply (rule m_comm [THEN trans])
   8.188 -  apply (rule l_null)
   8.189 -  done
   8.190 -
   8.191 -lemma l_minus: "(-(a::'a::ring)) * b = - (a * b)"
   8.192 -  apply (rule a_lcancel)
   8.193 -  apply (rule r_neg [symmetric, THEN [2] trans])
   8.194 -  apply (rule l_distr [symmetric, THEN trans])
   8.195 -  apply (simp add: l_null r_neg)
   8.196 -  done
   8.197 -
   8.198 -lemma r_minus: "(a::'a::ring) * (-b) = - (a * b)"
   8.199 -  apply (rule a_lcancel)
   8.200 -  apply (rule r_neg [symmetric, THEN [2] trans])
   8.201 -  apply (rule r_distr [symmetric, THEN trans])
   8.202 -  apply (simp add: r_null r_neg)
   8.203 -  done
   8.204 -
   8.205 -(*** Term order for commutative rings ***)
   8.206 -
   8.207 -ML {*
   8.208 -fun ring_ord (Const (a, _)) =
   8.209 -    find_index (fn a' => a = a')
   8.210 -      [@{const_name Groups.zero}, @{const_name Groups.plus}, @{const_name Groups.uminus},
   8.211 -        @{const_name Groups.minus}, @{const_name Groups.one}, @{const_name Groups.times}]
   8.212 -  | ring_ord _ = ~1;
   8.213 -
   8.214 -fun termless_ring (a, b) = (Term_Ord.term_lpo ring_ord (a, b) = LESS);
   8.215 -
   8.216 -val ring_ss =
   8.217 -  (HOL_basic_ss |> Simplifier.set_termless termless_ring)
   8.218 -  addsimps
   8.219 -  [@{thm a_assoc}, @{thm l_zero}, @{thm l_neg}, @{thm a_comm}, @{thm m_assoc},
   8.220 -   @{thm l_one}, @{thm l_distr}, @{thm m_comm}, @{thm minus_def},
   8.221 -   @{thm r_zero}, @{thm r_neg}, @{thm r_neg2}, @{thm r_neg1}, @{thm minus_add},
   8.222 -   @{thm minus_minus}, @{thm minus0}, @{thm a_lcomm}, @{thm m_lcomm}, (*@{thm r_one},*)
   8.223 -   @{thm r_distr}, @{thm l_null}, @{thm r_null}, @{thm l_minus}, @{thm r_minus}];
   8.224 -*}   (* Note: r_one is not necessary in ring_ss *)
   8.225 -
   8.226 -method_setup ring = {*
   8.227 -  Scan.succeed (K (SIMPLE_METHOD' (full_simp_tac ring_ss)))
   8.228 -*} "compute distributive normal form in rings"
   8.229 -
   8.230 -
   8.231 -subsection {* Rings and the summation operator *}
   8.232 -
   8.233 -(* Basic facts --- move to HOL!!! *)
   8.234 -
   8.235 -(* needed because natsum_cong (below) disables atMost_0 *)
   8.236 -lemma natsum_0 [simp]: "setsum f {..(0::nat)} = (f 0::'a::comm_monoid_add)"
   8.237 -by simp
   8.238 -(*
   8.239 -lemma natsum_Suc [simp]:
   8.240 -  "setsum f {..Suc n} = (f (Suc n) + setsum f {..n}::'a::comm_monoid_add)"
   8.241 -by (simp add: atMost_Suc)
   8.242 -*)
   8.243 -lemma natsum_Suc2:
   8.244 -  "setsum f {..Suc n} = (f 0::'a::comm_monoid_add) + (setsum (%i. f (Suc i)) {..n})"
   8.245 -proof (induct n)
   8.246 -  case 0 show ?case by simp
   8.247 -next
   8.248 -  case Suc thus ?case by (simp add: add_assoc)
   8.249 -qed
   8.250 -
   8.251 -lemma natsum_cong [cong]:
   8.252 -  "!!k. [| j = k; !!i::nat. i <= k ==> f i = (g i::'a::comm_monoid_add) |] ==>
   8.253 -        setsum f {..j} = setsum g {..k}"
   8.254 -by (induct j) auto
   8.255 -
   8.256 -lemma natsum_zero [simp]: "setsum (%i. 0) {..n::nat} = (0::'a::comm_monoid_add)"
   8.257 -by (induct n) simp_all
   8.258 -
   8.259 -lemma natsum_add [simp]:
   8.260 -  "!!f::nat=>'a::comm_monoid_add.
   8.261 -   setsum (%i. f i + g i) {..n::nat} = setsum f {..n} + setsum g {..n}"
   8.262 -by (induct n) (simp_all add: add_ac)
   8.263 -
   8.264 -(* Facts specific to rings *)
   8.265 -
   8.266 -subclass (in ring) comm_monoid_add
   8.267 -proof
   8.268 -  fix x y z
   8.269 -  show "x + y = y + x" by (rule a_comm)
   8.270 -  show "(x + y) + z = x + (y + z)" by (rule a_assoc)
   8.271 -  show "0 + x = x" by (rule l_zero)
   8.272 -qed
   8.273 -
   8.274 -simproc_setup
   8.275 -  ring ("t + u::'a::ring" | "t - u::'a::ring" | "t * u::'a::ring" | "- t::'a::ring") =
   8.276 -{*
   8.277 -  fn _ => fn ss => fn ct =>
   8.278 -    let
   8.279 -      val ctxt = Simplifier.the_context ss;
   8.280 -      val {t, T, maxidx, ...} = Thm.rep_cterm ct;
   8.281 -      val rew =
   8.282 -        Goal.prove ctxt [] []
   8.283 -          (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, Var (("x", maxidx + 1), T))))
   8.284 -          (fn _ => simp_tac (Simplifier.inherit_context ss ring_ss) 1)
   8.285 -        |> mk_meta_eq;
   8.286 -      val (t', u) = Logic.dest_equals (Thm.prop_of rew);
   8.287 -    in if t' aconv u then NONE else SOME rew end
   8.288 -*}
   8.289 -
   8.290 -lemma natsum_ldistr:
   8.291 -  "!!a::'a::ring. setsum f {..n::nat} * a = setsum (%i. f i * a) {..n}"
   8.292 -by (induct n) simp_all
   8.293 -
   8.294 -lemma natsum_rdistr:
   8.295 -  "!!a::'a::ring. a * setsum f {..n::nat} = setsum (%i. a * f i) {..n}"
   8.296 -by (induct n) simp_all
   8.297 -
   8.298 -subsection {* Integral Domains *}
   8.299 -
   8.300 -declare one_not_zero [simp]
   8.301 -
   8.302 -lemma zero_not_one [simp]:
   8.303 -  "0 ~= (1::'a::domain)"
   8.304 -by (rule not_sym) simp
   8.305 -
   8.306 -lemma integral_iff: (* not by default a simp rule! *)
   8.307 -  "(a * b = (0::'a::domain)) = (a = 0 | b = 0)"
   8.308 -proof
   8.309 -  assume "a * b = 0" then show "a = 0 | b = 0" by (simp add: integral)
   8.310 -next
   8.311 -  assume "a = 0 | b = 0" then show "a * b = 0" by auto
   8.312 -qed
   8.313 -
   8.314 -(*
   8.315 -lemma "(a::'a::ring) - (a - b) = b" apply simp
   8.316 - simproc seems to fail on this example (fixed with new term order)
   8.317 -*)
   8.318 -(*
   8.319 -lemma bug: "(b::'a::ring) - (b - a) = a" by simp
   8.320 -   simproc for rings cannot prove "(a::'a::ring) - (a - b) = b"
   8.321 -*)
   8.322 -lemma m_lcancel:
   8.323 -  assumes prem: "(a::'a::domain) ~= 0" shows conc: "(a * b = a * c) = (b = c)"
   8.324 -proof
   8.325 -  assume eq: "a * b = a * c"
   8.326 -  then have "a * (b - c) = 0" by simp
   8.327 -  then have "a = 0 | (b - c) = 0" by (simp only: integral_iff)
   8.328 -  with prem have "b - c = 0" by auto
   8.329 -  then have "b = b - (b - c)" by simp
   8.330 -  also have "b - (b - c) = c" by simp
   8.331 -  finally show "b = c" .
   8.332 -next
   8.333 -  assume "b = c" then show "a * b = a * c" by simp
   8.334 -qed
   8.335 -
   8.336 -lemma m_rcancel:
   8.337 -  "(a::'a::domain) ~= 0 ==> (b * a = c * a) = (b = c)"
   8.338 -by (simp add: m_lcancel)
   8.339 -
   8.340 -declare power_Suc [simp]
   8.341 -
   8.342 -lemma power_one [simp]:
   8.343 -  "1 ^ n = (1::'a::ring)" by (induct n) simp_all
   8.344 -
   8.345 -lemma power_zero [simp]:
   8.346 -  "n \<noteq> 0 \<Longrightarrow> 0 ^ n = (0::'a::ring)" by (induct n) simp_all
   8.347 -
   8.348 -lemma power_mult [simp]:
   8.349 -  "(a::'a::ring) ^ m * a ^ n = a ^ (m + n)"
   8.350 -  by (induct m) simp_all
   8.351 -
   8.352 -
   8.353 -section "Divisibility"
   8.354 -
   8.355 -lemma dvd_zero_right [simp]:
   8.356 -  "(a::'a::ring) dvd 0"
   8.357 -proof
   8.358 -  show "0 = a * 0" by simp
   8.359 -qed
   8.360 -
   8.361 -lemma dvd_zero_left:
   8.362 -  "0 dvd (a::'a::ring) \<Longrightarrow> a = 0" unfolding dvd_def by simp
   8.363 -
   8.364 -lemma dvd_refl_ring [simp]:
   8.365 -  "(a::'a::ring) dvd a"
   8.366 -proof
   8.367 -  show "a = a * 1" by simp
   8.368 -qed
   8.369 -
   8.370 -lemma dvd_trans_ring:
   8.371 -  fixes a b c :: "'a::ring"
   8.372 -  assumes a_dvd_b: "a dvd b"
   8.373 -  and b_dvd_c: "b dvd c"
   8.374 -  shows "a dvd c"
   8.375 -proof -
   8.376 -  from a_dvd_b obtain l where "b = a * l" using dvd_def by blast
   8.377 -  moreover from b_dvd_c obtain j where "c = b * j" using dvd_def by blast
   8.378 -  ultimately have "c = a * (l * j)" by simp
   8.379 -  then have "\<exists>k. c = a * k" ..
   8.380 -  then show ?thesis using dvd_def by blast
   8.381 -qed
   8.382 -
   8.383 -
   8.384 -lemma unit_mult:
   8.385 -  "!!a::'a::ring. [| a dvd 1; b dvd 1 |] ==> a * b dvd 1"
   8.386 -  apply (unfold dvd_def)
   8.387 -  apply clarify
   8.388 -  apply (rule_tac x = "k * ka" in exI)
   8.389 -  apply simp
   8.390 -  done
   8.391 -
   8.392 -lemma unit_power: "!!a::'a::ring. a dvd 1 ==> a^n dvd 1"
   8.393 -  apply (induct_tac n)
   8.394 -   apply simp
   8.395 -  apply (simp add: unit_mult)
   8.396 -  done
   8.397 -
   8.398 -lemma dvd_add_right [simp]:
   8.399 -  "!! a::'a::ring. [| a dvd b; a dvd c |] ==> a dvd b + c"
   8.400 -  apply (unfold dvd_def)
   8.401 -  apply clarify
   8.402 -  apply (rule_tac x = "k + ka" in exI)
   8.403 -  apply (simp add: r_distr)
   8.404 -  done
   8.405 -
   8.406 -lemma dvd_uminus_right [simp]:
   8.407 -  "!! a::'a::ring. a dvd b ==> a dvd -b"
   8.408 -  apply (unfold dvd_def)
   8.409 -  apply clarify
   8.410 -  apply (rule_tac x = "-k" in exI)
   8.411 -  apply (simp add: r_minus)
   8.412 -  done
   8.413 -
   8.414 -lemma dvd_l_mult_right [simp]:
   8.415 -  "!! a::'a::ring. a dvd b ==> a dvd c*b"
   8.416 -  apply (unfold dvd_def)
   8.417 -  apply clarify
   8.418 -  apply (rule_tac x = "c * k" in exI)
   8.419 -  apply simp
   8.420 -  done
   8.421 -
   8.422 -lemma dvd_r_mult_right [simp]:
   8.423 -  "!! a::'a::ring. a dvd b ==> a dvd b*c"
   8.424 -  apply (unfold dvd_def)
   8.425 -  apply clarify
   8.426 -  apply (rule_tac x = "k * c" in exI)
   8.427 -  apply simp
   8.428 -  done
   8.429 -
   8.430 -
   8.431 -(* Inverse of multiplication *)
   8.432 -
   8.433 -section "inverse"
   8.434 -
   8.435 -lemma inverse_unique: "!! a::'a::ring. [| a * x = 1; a * y = 1 |] ==> x = y"
   8.436 -  apply (rule_tac a = "(a*y) * x" and b = "y * (a*x)" in box_equals)
   8.437 -    apply (simp (no_asm))
   8.438 -  apply auto
   8.439 -  done
   8.440 -
   8.441 -lemma r_inverse_ring: "!! a::'a::ring. a dvd 1 ==> a * inverse a = 1"
   8.442 -  apply (unfold inverse_def dvd_def)
   8.443 -  using [[simproc del: ring]]
   8.444 -  apply simp
   8.445 -  apply clarify
   8.446 -  apply (rule theI)
   8.447 -   apply assumption
   8.448 -  apply (rule inverse_unique)
   8.449 -   apply assumption
   8.450 -  apply assumption
   8.451 -  done
   8.452 -
   8.453 -lemma l_inverse_ring: "!! a::'a::ring. a dvd 1 ==> inverse a * a = 1"
   8.454 -  by (simp add: r_inverse_ring)
   8.455 -
   8.456 -
   8.457 -(* Fields *)
   8.458 -
   8.459 -section "Fields"
   8.460 -
   8.461 -lemma field_unit [simp]: "!! a::'a::field. (a dvd 1) = (a ~= 0)"
   8.462 -  by (auto dest: field_ax dvd_zero_left simp add: field_one_not_zero)
   8.463 -
   8.464 -lemma r_inverse [simp]: "!! a::'a::field. a ~= 0 ==> a * inverse a = 1"
   8.465 -  by (simp add: r_inverse_ring)
   8.466 -
   8.467 -lemma l_inverse [simp]: "!! a::'a::field. a ~= 0 ==> inverse a * a= 1"
   8.468 -  by (simp add: l_inverse_ring)
   8.469 -
   8.470 -
   8.471 -(* fields are integral domains *)
   8.472 -
   8.473 -lemma field_integral: "!! a::'a::field. a * b = 0 ==> a = 0 | b = 0"
   8.474 -  apply step
   8.475 -  apply (rule_tac a = " (a*b) * inverse b" in box_equals)
   8.476 -    apply (rule_tac [3] refl)
   8.477 -   prefer 2
   8.478 -   apply (simp (no_asm))
   8.479 -   apply auto
   8.480 -  done
   8.481 -
   8.482 -
   8.483 -(* fields are factorial domains *)
   8.484 -
   8.485 -lemma field_fact_prime: "!! a::'a::field. irred a ==> prime a"
   8.486 -  unfolding prime_def irred_def by (blast intro: field_ax)
   8.487 -
   8.488 -end
     9.1 --- a/src/HOL/Algebra/abstract/RingHomo.thy	Mon Mar 25 19:53:44 2013 +0100
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,64 +0,0 @@
     9.4 -(*  Author: Clemens Ballarin, started 15 April 1997
     9.5 -
     9.6 -Ring homomorphism.
     9.7 -*)
     9.8 -
     9.9 -header {* Ring homomorphism *}
    9.10 -
    9.11 -theory RingHomo
    9.12 -imports Ring2
    9.13 -begin
    9.14 -
    9.15 -definition
    9.16 -  homo :: "('a::ring => 'b::ring) => bool" where
    9.17 -  "homo f \<longleftrightarrow> (ALL a b. f (a + b) = f a + f b &
    9.18 -                                   f (a * b) = f a * f b) &
    9.19 -                                   f 1 = 1"
    9.20 -
    9.21 -
    9.22 -lemma homoI:
    9.23 -  "!! f. [| !! a b. f (a + b) = f a + f b; !! a b. f (a * b) = f a * f b;  
    9.24 -            f 1 = 1 |] ==> homo f"
    9.25 -  unfolding homo_def by blast
    9.26 -
    9.27 -lemma homo_add [simp]: "!! f. homo f ==> f (a + b) = f a + f b"
    9.28 -  unfolding homo_def by blast
    9.29 -
    9.30 -lemma homo_mult [simp]: "!! f. homo f ==> f (a * b) = f a * f b"
    9.31 -  unfolding homo_def by blast
    9.32 -
    9.33 -lemma homo_one [simp]: "!! f. homo f ==> f 1 = 1"
    9.34 -  unfolding homo_def by blast
    9.35 -
    9.36 -lemma homo_zero [simp]: "!! f::('a::ring=>'b::ring). homo f ==> f 0 = 0"
    9.37 -  apply (rule_tac a = "f 0" in a_lcancel)
    9.38 -  apply (simp (no_asm_simp) add: homo_add [symmetric])
    9.39 -  done
    9.40 -
    9.41 -lemma homo_uminus [simp]:
    9.42 -  "!! f::('a::ring=>'b::ring). homo f ==> f (-a) = - f a"
    9.43 -  apply (rule_tac a = "f a" in a_lcancel)
    9.44 -  apply (frule homo_zero)
    9.45 -  apply (simp (no_asm_simp) add: homo_add [symmetric])
    9.46 -  done
    9.47 -
    9.48 -lemma homo_power [simp]: "!! f::('a::ring=>'b::ring). homo f ==> f (a ^ n) = f a ^ n"
    9.49 -  apply (induct_tac n)
    9.50 -   apply (drule homo_one)
    9.51 -   apply simp
    9.52 -  apply (drule_tac a = "a^n" and b = "a" in homo_mult)
    9.53 -  apply simp
    9.54 -  done
    9.55 -
    9.56 -lemma homo_SUM [simp]:
    9.57 -  "!! f::('a::ring=>'b::ring).  
    9.58 -    homo f ==> f (setsum g {..n::nat}) = setsum (f o g) {..n}"
    9.59 -  apply (induct_tac n)
    9.60 -   apply simp
    9.61 -  apply simp
    9.62 -  done
    9.63 -
    9.64 -lemma id_homo [simp]: "homo (%x. x)"
    9.65 -  by (blast intro!: homoI)
    9.66 -
    9.67 -end
    10.1 --- a/src/HOL/Algebra/poly/LongDiv.thy	Mon Mar 25 19:53:44 2013 +0100
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,257 +0,0 @@
    10.4 -(*  Author: Clemens Ballarin, started 23 June 1999
    10.5 -
    10.6 -Experimental theory: long division of polynomials.
    10.7 -*)
    10.8 -
    10.9 -theory LongDiv
   10.10 -imports PolyHomo
   10.11 -begin
   10.12 -
   10.13 -definition
   10.14 -  lcoeff :: "'a::ring up => 'a" where
   10.15 -  "lcoeff p = coeff p (deg p)"
   10.16 -
   10.17 -definition
   10.18 -  eucl_size :: "'a::zero up => nat" where
   10.19 -  "eucl_size p = (if p = 0 then 0 else deg p + 1)"
   10.20 -
   10.21 -lemma SUM_shrink_below_lemma:
   10.22 -  "!! f::(nat=>'a::ring). (ALL i. i < m --> f i = 0) --> 
   10.23 -  setsum (%i. f (i+m)) {..d} = setsum f {..m+d}"
   10.24 -  apply (induct_tac d)
   10.25 -   apply (induct_tac m)
   10.26 -    apply simp
   10.27 -   apply force
   10.28 -  apply (simp add: add_commute [of m]) 
   10.29 -  done
   10.30 -
   10.31 -lemma SUM_extend_below: 
   10.32 -  "!! f::(nat=>'a::ring).  
   10.33 -     [| m <= n; !!i. i < m ==> f i = 0; P (setsum (%i. f (i+m)) {..n-m}) |]  
   10.34 -     ==> P (setsum f {..n})"
   10.35 -  by (simp add: SUM_shrink_below_lemma add_diff_inverse leD)
   10.36 -
   10.37 -lemma up_repr2D: 
   10.38 -  "!! p::'a::ring up.  
   10.39 -   [| deg p <= n; P (setsum (%i. monom (coeff p i) i) {..n}) |]  
   10.40 -     ==> P p"
   10.41 -  by (simp add: up_repr_le)
   10.42 -
   10.43 -
   10.44 -(* Start of LongDiv *)
   10.45 -
   10.46 -lemma deg_lcoeff_cancel: 
   10.47 -  "!!p::('a::ring up).  
   10.48 -     [| deg p <= deg r; deg q <= deg r;  
   10.49 -        coeff p (deg r) = - (coeff q (deg r)); deg r ~= 0 |] ==>  
   10.50 -     deg (p + q) < deg r"
   10.51 -  apply (rule le_less_trans [of _ "deg r - 1"])
   10.52 -   prefer 2
   10.53 -   apply arith
   10.54 -  apply (rule deg_aboveI)
   10.55 -  apply (case_tac "deg r = m")
   10.56 -   apply clarify
   10.57 -   apply simp
   10.58 -  (* case "deg q ~= m" *)
   10.59 -   apply (subgoal_tac "deg p < m & deg q < m")
   10.60 -    apply (simp (no_asm_simp) add: deg_aboveD)
   10.61 -  apply arith
   10.62 -  done
   10.63 -
   10.64 -lemma deg_lcoeff_cancel2: 
   10.65 -  "!!p::('a::ring up).  
   10.66 -     [| deg p <= deg r; deg q <= deg r;  
   10.67 -        p ~= -q; coeff p (deg r) = - (coeff q (deg r)) |] ==>  
   10.68 -     deg (p + q) < deg r"
   10.69 -  apply (rule deg_lcoeff_cancel)
   10.70 -     apply assumption+
   10.71 -  apply (rule classical)
   10.72 -  apply clarify
   10.73 -  apply (erule notE)
   10.74 -  apply (rule_tac p = p in up_repr2D, assumption)
   10.75 -  apply (rule_tac p = q in up_repr2D, assumption)
   10.76 -  apply (rotate_tac -1)
   10.77 -  apply (simp add: smult_l_minus)
   10.78 -  done
   10.79 -
   10.80 -lemma long_div_eucl_size: 
   10.81 -  "!!g::('a::ring up). g ~= 0 ==>  
   10.82 -     Ex (% (q, r, k).  
   10.83 -       (lcoeff g)^k *s f = q * g + r & (eucl_size r < eucl_size g))"
   10.84 -  apply (rule_tac P = "%f. Ex (% (q, r, k) . (lcoeff g) ^k *s f = q * g + r & (eucl_size r < eucl_size g))" in wf_induct)
   10.85 -  (* TO DO: replace by measure_induct *)
   10.86 -  apply (rule_tac f = eucl_size in wf_measure)
   10.87 -  apply (case_tac "eucl_size x < eucl_size g")
   10.88 -   apply (rule_tac x = "(0, x, 0)" in exI)
   10.89 -   apply (simp (no_asm_simp))
   10.90 -  (* case "eucl_size x >= eucl_size g" *)
   10.91 -  apply (drule_tac x = "lcoeff g *s x - (monom (lcoeff x) (deg x - deg g)) * g" in spec)
   10.92 -  apply (erule impE)
   10.93 -   apply (simp (no_asm_use) add: inv_image_def measure_def lcoeff_def)
   10.94 -   apply (case_tac "x = 0")
   10.95 -    apply (rotate_tac -1)
   10.96 -    apply (simp add: eucl_size_def)
   10.97 -    (* case "x ~= 0 *)
   10.98 -    apply (rotate_tac -1)
   10.99 -   apply (simp add: eucl_size_def)
  10.100 -   apply (rule impI)
  10.101 -   apply (rule deg_lcoeff_cancel2)
  10.102 -  (* replace by linear arithmetic??? *)
  10.103 -      apply (rule_tac [2] le_trans)
  10.104 -       apply (rule_tac [2] deg_smult_ring)
  10.105 -      prefer 2
  10.106 -      apply simp
  10.107 -     apply (simp (no_asm))
  10.108 -     apply (rule le_trans)
  10.109 -      apply (rule deg_mult_ring)
  10.110 -     apply (rule le_trans)
  10.111 -(**)
  10.112 -      apply (rule add_le_mono)
  10.113 -       apply (rule le_refl)
  10.114 -    (* term order forces to use this instead of add_le_mono1 *)
  10.115 -      apply (rule deg_monom_ring)
  10.116 -     apply (simp (no_asm_simp))
  10.117 -    apply force
  10.118 -   apply (simp (no_asm))
  10.119 -(**)
  10.120 -   (* This change is probably caused by application of commutativity *)
  10.121 -   apply (rule_tac m = "deg g" and n = "deg x" in SUM_extend)
  10.122 -     apply (simp (no_asm))
  10.123 -    apply (simp (no_asm_simp))
  10.124 -    apply arith
  10.125 -   apply (rule_tac m = "deg g" and n = "deg g" in SUM_extend_below)
  10.126 -     apply (rule le_refl)
  10.127 -    apply (simp (no_asm_simp))
  10.128 -    apply arith
  10.129 -   apply (simp (no_asm))
  10.130 -(**)
  10.131 -(* end of subproof deg f1 < deg f *)
  10.132 -  apply (erule exE)
  10.133 -  apply (rule_tac x = "((% (q,r,k) . (monom (lcoeff g ^ k * lcoeff x) (deg x - deg g) + q)) xa, (% (q,r,k) . r) xa, (% (q,r,k) . Suc k) xa) " in exI)
  10.134 -  apply clarify
  10.135 -  apply (drule sym)
  10.136 -  using [[simproc del: ring]]
  10.137 -  apply (simp (no_asm_use) add: l_distr a_assoc)
  10.138 -  apply (simp (no_asm_simp))
  10.139 -  apply (simp (no_asm_use) add: minus_def smult_r_distr smult_r_minus
  10.140 -    monom_mult_smult smult_assoc2)
  10.141 -  using [[simproc ring]]
  10.142 -  apply (simp add: smult_assoc1 [symmetric])
  10.143 -  done
  10.144 -
  10.145 -lemma long_div_ring_aux:
  10.146 -  "(g :: 'a::ring up) ~= 0 ==>
  10.147 -    Ex (\<lambda>(q, r, k). lcoeff g ^ k *s f = q * g + r \<and>
  10.148 -      (if r = 0 then 0 else deg r + 1) < (if g = 0 then 0 else deg g + 1))"
  10.149 -proof -
  10.150 -  note [[simproc del: ring]]
  10.151 -  assume "g ~= 0"
  10.152 -  then show ?thesis
  10.153 -    by (rule long_div_eucl_size [simplified eucl_size_def])
  10.154 -qed
  10.155 -
  10.156 -lemma long_div_ring: 
  10.157 -  "!!g::('a::ring up). g ~= 0 ==>  
  10.158 -     Ex (% (q, r, k).  
  10.159 -       (lcoeff g)^k *s f = q * g + r & (r = 0 | deg r < deg g))"
  10.160 -  apply (frule_tac f = f in long_div_ring_aux)
  10.161 -  using [[simproc del: ring]]
  10.162 -  apply auto
  10.163 -  apply (case_tac "aa = 0")
  10.164 -   apply blast
  10.165 -  (* case "aa ~= 0 *)
  10.166 -  apply (rotate_tac -1)
  10.167 -  apply auto
  10.168 -  done
  10.169 -
  10.170 -(* Next one fails *)
  10.171 -lemma long_div_unit: 
  10.172 -  "!!g::('a::ring up). [| g ~= 0; (lcoeff g) dvd 1 |] ==>  
  10.173 -     Ex (% (q, r). f = q * g + r & (r = 0 | deg r < deg g))"
  10.174 -  apply (frule_tac f = "f" in long_div_ring)
  10.175 -  apply (erule exE)
  10.176 -  apply (rule_tac x = "((% (q,r,k) . (inverse (lcoeff g ^k) *s q)) x, (% (q,r,k) . inverse (lcoeff g ^k) *s r) x) " in exI)
  10.177 -  apply clarify
  10.178 -  apply (rule conjI)
  10.179 -   apply (drule sym)
  10.180 -   using [[simproc del: ring]]
  10.181 -   apply (simp (no_asm_simp) add: smult_r_distr [symmetric] smult_assoc2)
  10.182 -   using [[simproc ring]]
  10.183 -   apply (simp (no_asm_simp) add: l_inverse_ring unit_power smult_assoc1 [symmetric])
  10.184 -  (* degree property *)
  10.185 -   apply (erule disjE)
  10.186 -    apply (simp (no_asm_simp))
  10.187 -  apply (rule disjI2)
  10.188 -  apply (rule le_less_trans)
  10.189 -   apply (rule deg_smult_ring)
  10.190 -  apply (simp (no_asm_simp))
  10.191 -  done
  10.192 -
  10.193 -lemma long_div_theorem: 
  10.194 -  "!!g::('a::field up). g ~= 0 ==>  
  10.195 -     Ex (% (q, r). f = q * g + r & (r = 0 | deg r < deg g))"
  10.196 -  apply (rule long_div_unit)
  10.197 -   apply assumption
  10.198 -  apply (simp (no_asm_simp) add: lcoeff_def lcoeff_nonzero field_ax)
  10.199 -  done
  10.200 -
  10.201 -lemma uminus_zero: "- (0::'a::ring) = 0"
  10.202 -  by simp
  10.203 -
  10.204 -lemma diff_zero_imp_eq: "!!a::'a::ring. a - b = 0 ==> a = b"
  10.205 -  apply (rule_tac s = "a - (a - b) " in trans)
  10.206 -   apply simp
  10.207 -  apply (simp (no_asm))
  10.208 -  done
  10.209 -
  10.210 -lemma eq_imp_diff_zero: "!!a::'a::ring. a = b ==> a + (-b) = 0"
  10.211 -  by simp
  10.212 -
  10.213 -lemma long_div_quo_unique: 
  10.214 -  "!!g::('a::field up). [| g ~= 0;  
  10.215 -     f = q1 * g + r1; (r1 = 0 | deg r1 < deg g);  
  10.216 -     f = q2 * g + r2; (r2 = 0 | deg r2 < deg g) |] ==> q1 = q2"
  10.217 -  apply (subgoal_tac "(q1 - q2) * g = r2 - r1") (* 1 *)
  10.218 -   apply (erule_tac V = "f = ?x" in thin_rl)
  10.219 -  apply (erule_tac V = "f = ?x" in thin_rl)
  10.220 -  apply (rule diff_zero_imp_eq)
  10.221 -  apply (rule classical)
  10.222 -  apply (erule disjE)
  10.223 -  (* r1 = 0 *)
  10.224 -    apply (erule disjE)
  10.225 -  (* r2 = 0 *)
  10.226 -     using [[simproc del: ring]]
  10.227 -     apply (simp add: integral_iff minus_def l_zero uminus_zero)
  10.228 -  (* r2 ~= 0 *)
  10.229 -    apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong)
  10.230 -    apply (simp add: minus_def l_zero uminus_zero)
  10.231 -  (* r1 ~=0 *)
  10.232 -   apply (erule disjE)
  10.233 -  (* r2 = 0 *)
  10.234 -    apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong)
  10.235 -    apply (simp add: minus_def l_zero uminus_zero)
  10.236 -  (* r2 ~= 0 *)
  10.237 -   apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong)
  10.238 -   apply (simp add: minus_def)
  10.239 -   apply (drule order_eq_refl [THEN add_leD2])
  10.240 -   apply (drule leD)
  10.241 -   apply (erule notE, rule deg_add [THEN le_less_trans])
  10.242 -   apply (simp (no_asm_simp))
  10.243 -  (* proof of 1 *)
  10.244 -   apply (rule diff_zero_imp_eq)
  10.245 -  apply hypsubst
  10.246 -  apply (drule_tac a = "?x+?y" in eq_imp_diff_zero)
  10.247 -  using [[simproc ring]]
  10.248 -  apply simp
  10.249 -  done
  10.250 -
  10.251 -lemma long_div_rem_unique: 
  10.252 -  "!!g::('a::field up). [| g ~= 0;  
  10.253 -     f = q1 * g + r1; (r1 = 0 | deg r1 < deg g);  
  10.254 -     f = q2 * g + r2; (r2 = 0 | deg r2 < deg g) |] ==> r1 = r2"
  10.255 -  apply (subgoal_tac "q1 = q2")
  10.256 -   apply (metis a_comm a_lcancel m_comm)
  10.257 -  apply (metis a_comm l_zero long_div_quo_unique m_comm conc)
  10.258 -  done
  10.259 -
  10.260 -end
    11.1 --- a/src/HOL/Algebra/poly/PolyHomo.thy	Mon Mar 25 19:53:44 2013 +0100
    11.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.3 @@ -1,187 +0,0 @@
    11.4 -(*  Author: Clemens Ballarin, started 15 April 1997
    11.5 -
    11.6 -Universal property and evaluation homomorphism of univariate polynomials.
    11.7 -*)
    11.8 -
    11.9 -theory PolyHomo
   11.10 -imports UnivPoly2
   11.11 -begin
   11.12 -
   11.13 -definition
   11.14 -  EVAL2 :: "['a::ring => 'b, 'b, 'a up] => 'b::ring" where
   11.15 -  "EVAL2 phi a p = setsum (%i. phi (coeff p i) * a ^ i) {..deg p}"
   11.16 -
   11.17 -definition
   11.18 -  EVAL :: "['a::ring, 'a up] => 'a" where
   11.19 -  "EVAL = EVAL2 (%x. x)"
   11.20 -
   11.21 -lemma SUM_shrink_lemma:
   11.22 -  "!! f::(nat=>'a::ring).
   11.23 -     m <= n & (ALL i. m < i & i <= n --> f i = 0) -->
   11.24 -     setsum f {..m} = setsum f {..n}"
   11.25 -  apply (induct_tac n)
   11.26 -  (* Base case *)
   11.27 -   apply (simp (no_asm))
   11.28 -  (* Induction step *)
   11.29 -  apply (case_tac "m <= n")
   11.30 -   apply auto
   11.31 -  apply (subgoal_tac "m = Suc n")
   11.32 -   apply (simp (no_asm_simp))
   11.33 -  apply arith
   11.34 -  done
   11.35 -
   11.36 -lemma SUM_shrink:
   11.37 -  "!! f::(nat=>'a::ring).
   11.38 -     [| m <= n; !!i. [| m < i; i <= n |] ==> f i = 0; P (setsum f {..n}) |]
   11.39 -   ==> P (setsum f {..m})"
   11.40 -  apply (cut_tac m = m and n = n and f = f in SUM_shrink_lemma)
   11.41 -  apply simp
   11.42 -  done
   11.43 -
   11.44 -lemma SUM_extend:
   11.45 -  "!! f::(nat=>'a::ring).
   11.46 -     [| m <= n; !!i. [| m < i; i <= n |] ==> f i = 0; P (setsum f {..m}) |]
   11.47 -     ==> P (setsum f {..n})"
   11.48 -  apply (cut_tac m = m and n = n and f = f in SUM_shrink_lemma)
   11.49 -  apply simp
   11.50 -  done
   11.51 -
   11.52 -lemma DiagSum_lemma:
   11.53 -  "!!f::nat=>'a::ring. j <= n + m -->
   11.54 -     setsum (%k. setsum (%i. f i * g (k - i)) {..k}) {..j} =
   11.55 -     setsum (%k. setsum (%i. f k * g i) {..j - k}) {..j}"
   11.56 -  apply (induct_tac j)
   11.57 -  (* Base case *)
   11.58 -   apply (simp (no_asm))
   11.59 -  (* Induction step *)
   11.60 -  apply (simp (no_asm) add: Suc_diff_le natsum_add)
   11.61 -  apply (simp (no_asm_simp))
   11.62 -  done
   11.63 -
   11.64 -lemma DiagSum:
   11.65 -  "!!f::nat=>'a::ring.
   11.66 -     setsum (%k. setsum (%i. f i * g (k - i)) {..k}) {..n + m} =
   11.67 -     setsum (%k. setsum (%i. f k * g i) {..n + m - k}) {..n + m}"
   11.68 -  apply (rule DiagSum_lemma [THEN mp])
   11.69 -  apply (rule le_refl)
   11.70 -  done
   11.71 -
   11.72 -lemma CauchySum:
   11.73 -  "!! f::nat=>'a::ring. [| bound n f; bound m g|] ==>
   11.74 -     setsum (%k. setsum (%i. f i * g (k-i)) {..k}) {..n + m} =
   11.75 -     setsum f {..n} * setsum g {..m}"
   11.76 -  apply (simp (no_asm) add: natsum_ldistr DiagSum)
   11.77 -  (* SUM_rdistr must be applied after SUM_ldistr ! *)
   11.78 -  apply (simp (no_asm) add: natsum_rdistr)
   11.79 -  apply (rule_tac m = n and n = "n + m" in SUM_extend)
   11.80 -  apply (rule le_add1)
   11.81 -   apply force
   11.82 -  apply (rule natsum_cong)
   11.83 -   apply (rule refl)
   11.84 -  apply (rule_tac m = m and n = "n +m - i" in SUM_shrink)
   11.85 -    apply (simp (no_asm_simp) add: le_add_diff)
   11.86 -   apply auto
   11.87 -  done
   11.88 -
   11.89 -(* Evaluation homomorphism *)
   11.90 -
   11.91 -lemma EVAL2_homo:
   11.92 -    "!! phi::('a::ring=>'b::ring). homo phi ==> homo (EVAL2 phi a)"
   11.93 -  apply (rule homoI)
   11.94 -    apply (unfold EVAL2_def)
   11.95 -  (* + commutes *)
   11.96 -  (* degree estimations:
   11.97 -    bound of all sums can be extended to max (deg aa) (deg b) *)
   11.98 -    apply (rule_tac m = "deg (aa + b) " and n = "max (deg aa) (deg b)" in SUM_shrink)
   11.99 -      apply (rule deg_add)
  11.100 -     apply (simp (no_asm_simp) del: coeff_add add: deg_aboveD)
  11.101 -    apply (rule_tac m = "deg aa" and n = "max (deg aa) (deg b)" in SUM_shrink)
  11.102 -     apply (rule le_maxI1)
  11.103 -    apply (simp (no_asm_simp) add: deg_aboveD)
  11.104 -   apply (rule_tac m = "deg b" and n = "max (deg aa) (deg b) " in SUM_shrink)
  11.105 -     apply (rule le_maxI2)
  11.106 -    apply (simp (no_asm_simp) add: deg_aboveD)
  11.107 -  (* actual homom property + *)
  11.108 -    apply (simp (no_asm_simp) add: l_distr natsum_add)
  11.109 -
  11.110 -  (* * commutes *)
  11.111 -   apply (rule_tac m = "deg (aa * b) " and n = "deg aa + deg b" in SUM_shrink)
  11.112 -    apply (rule deg_mult_ring)
  11.113 -    apply (simp (no_asm_simp) del: coeff_mult add: deg_aboveD)
  11.114 -   apply (rule trans)
  11.115 -    apply (rule_tac [2] CauchySum)
  11.116 -     prefer 2
  11.117 -     apply (simp add: boundI deg_aboveD)
  11.118 -    prefer 2
  11.119 -    apply (simp add: boundI deg_aboveD)
  11.120 -  (* getting a^i and a^(k-i) together is difficult, so we do it manually *)
  11.121 -  apply (rule_tac s = "setsum (%k. setsum (%i. phi (coeff aa i) * (phi (coeff b (k - i)) * (a ^ i * a ^ (k - i)))) {..k}) {..deg aa + deg b}" in trans)
  11.122 -    apply (simp (no_asm_simp) add: power_mult leD [THEN add_diff_inverse] natsum_ldistr)
  11.123 -   apply (simp (no_asm))
  11.124 -  (* 1 commutes *)
  11.125 -  apply (simp (no_asm_simp))
  11.126 -  done
  11.127 -
  11.128 -lemma EVAL2_const:
  11.129 -    "!!phi::'a::ring=>'b::ring. EVAL2 phi a (monom b 0) = phi b"
  11.130 -  by (simp add: EVAL2_def)
  11.131 -
  11.132 -lemma EVAL2_monom1:
  11.133 -    "!! phi::'a::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom 1 1) = a"
  11.134 -  by (simp add: EVAL2_def)
  11.135 -  (* Must be able to distinguish 0 from 1, hence 'a::domain *)
  11.136 -
  11.137 -lemma EVAL2_monom:
  11.138 -  "!! phi::'a::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom 1 n) = a ^ n"
  11.139 -  apply (unfold EVAL2_def)
  11.140 -  apply (simp (no_asm))
  11.141 -  apply (case_tac n)
  11.142 -   apply auto
  11.143 -  done
  11.144 -
  11.145 -lemma EVAL2_smult:
  11.146 -  "!!phi::'a::ring=>'b::ring.
  11.147 -     homo phi ==> EVAL2 phi a (b *s p) = phi b * EVAL2 phi a p"
  11.148 -  by (simp (no_asm_simp) add: monom_mult_is_smult [symmetric] EVAL2_homo EVAL2_const)
  11.149 -
  11.150 -lemma monom_decomp: "monom (a::'a::ring) n = monom a 0 * monom 1 n"
  11.151 -  apply (simp (no_asm) add: monom_mult_is_smult)
  11.152 -  apply (rule up_eqI)
  11.153 -  apply (simp (no_asm))
  11.154 -  done
  11.155 -
  11.156 -lemma EVAL2_monom_n:
  11.157 -  "!! phi::'a::domain=>'b::ring.
  11.158 -     homo phi ==> EVAL2 phi a (monom b n) = phi b * a ^ n"
  11.159 -  apply (subst monom_decomp)
  11.160 -  apply (simp (no_asm_simp) add: EVAL2_homo EVAL2_const EVAL2_monom)
  11.161 -  done
  11.162 -
  11.163 -lemma EVAL_homo: "!!a::'a::ring. homo (EVAL a)"
  11.164 -  by (simp add: EVAL_def EVAL2_homo)
  11.165 -
  11.166 -lemma EVAL_const: "!!a::'a::ring. EVAL a (monom b 0) = b"
  11.167 -  by (simp add: EVAL_def EVAL2_const)
  11.168 -
  11.169 -lemma EVAL_monom: "!!a::'a::domain. EVAL a (monom 1 n) = a ^ n"
  11.170 -  by (simp add: EVAL_def EVAL2_monom)
  11.171 -
  11.172 -lemma EVAL_smult: "!!a::'a::ring. EVAL a (b *s p) = b * EVAL a p"
  11.173 -  by (simp add: EVAL_def EVAL2_smult)
  11.174 -
  11.175 -lemma EVAL_monom_n: "!!a::'a::domain. EVAL a (monom b n) = b * a ^ n"
  11.176 -  by (simp add: EVAL_def EVAL2_monom_n)
  11.177 -
  11.178 -
  11.179 -(* Examples *)
  11.180 -
  11.181 -lemma "EVAL (x::'a::domain) (a*X^2 + b*X^1 + c*X^0) = a * x ^ 2 + b * x ^ 1 + c"
  11.182 -  by (simp del: power_Suc add: EVAL_homo EVAL_monom EVAL_monom_n)
  11.183 -
  11.184 -lemma
  11.185 -  "EVAL (y::'a::domain)
  11.186 -    (EVAL (monom x 0) (monom 1 1 + monom (a*X^2 + b*X^1 + c*X^0) 0)) =
  11.187 -   x ^ 1 + (a * y ^ 2 + b * y ^ 1 + c)"
  11.188 -  by (simp del: add: EVAL_homo EVAL_monom EVAL_monom_n EVAL_const)
  11.189 -
  11.190 -end
    12.1 --- a/src/HOL/Algebra/poly/Polynomial.thy	Mon Mar 25 19:53:44 2013 +0100
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,10 +0,0 @@
    12.4 -(*  Author: Clemens Ballarin, started 17 July 1997
    12.5 -
    12.6 -Summary theory of the development of (not instantiated) polynomials.
    12.7 -*)
    12.8 -
    12.9 -theory Polynomial
   12.10 -imports LongDiv
   12.11 -begin
   12.12 -
   12.13 -end
    13.1 --- a/src/HOL/Algebra/poly/UnivPoly2.thy	Mon Mar 25 19:53:44 2013 +0100
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,810 +0,0 @@
    13.4 -(*  Title:      HOL/Algebra/poly/UnivPoly2.thy
    13.5 -    Author:     Clemens Ballarin, started 9 December 1996
    13.6 -    Copyright:  Clemens Ballarin
    13.7 -*)
    13.8 -
    13.9 -header {* Univariate Polynomials *}
   13.10 -
   13.11 -theory UnivPoly2
   13.12 -imports "../abstract/Abstract"
   13.13 -begin
   13.14 -
   13.15 -(* With this variant of setsum_cong, assumptions
   13.16 -   like i:{m..n} get simplified (to m <= i & i <= n). *)
   13.17 -
   13.18 -declare strong_setsum_cong [cong]
   13.19 -
   13.20 -
   13.21 -section {* Definition of type up *}
   13.22 -
   13.23 -definition
   13.24 -  bound :: "[nat, nat => 'a::zero] => bool" where
   13.25 -  "bound n f = (ALL i. n < i --> f i = 0)"
   13.26 -
   13.27 -lemma boundI [intro!]: "[| !! m. n < m ==> f m = 0 |] ==> bound n f"
   13.28 -  unfolding bound_def by blast
   13.29 -
   13.30 -lemma boundE [elim?]: "[| bound n f; (!! m. n < m ==> f m = 0) ==> P |] ==> P"
   13.31 -  unfolding bound_def by blast
   13.32 -
   13.33 -lemma boundD [dest]: "[| bound n f; n < m |] ==> f m = 0"
   13.34 -  unfolding bound_def by blast
   13.35 -
   13.36 -lemma bound_below:
   13.37 -  assumes bound: "bound m f" and nonzero: "f n ~= 0" shows "n <= m"
   13.38 -proof (rule classical)
   13.39 -  assume "~ ?thesis"
   13.40 -  then have "m < n" by arith
   13.41 -  with bound have "f n = 0" ..
   13.42 -  with nonzero show ?thesis by contradiction
   13.43 -qed
   13.44 -
   13.45 -
   13.46 -definition "UP = {f :: nat => 'a::zero. EX n. bound n f}"
   13.47 -
   13.48 -typedef 'a up = "UP :: (nat => 'a::zero) set"
   13.49 -  morphisms Rep_UP Abs_UP
   13.50 -proof -
   13.51 -  have "bound 0 (\<lambda>_. 0::'a)" by (rule boundI) (rule refl)
   13.52 -  then show ?thesis unfolding UP_def by blast
   13.53 -qed
   13.54 -
   13.55 -
   13.56 -section {* Constants *}
   13.57 -
   13.58 -definition
   13.59 -  coeff :: "['a up, nat] => ('a::zero)"
   13.60 -  where "coeff p n = Rep_UP p n"
   13.61 -
   13.62 -definition
   13.63 -  monom :: "['a::zero, nat] => 'a up"  ("(3_*X^/_)" [71, 71] 70)
   13.64 -  where "monom a n = Abs_UP (%i. if i=n then a else 0)"
   13.65 -
   13.66 -definition
   13.67 -  smult :: "['a::{zero, times}, 'a up] => 'a up"  (infixl "*s" 70)
   13.68 -  where "a *s p = Abs_UP (%i. a * Rep_UP p i)"
   13.69 -
   13.70 -lemma coeff_bound_ex: "EX n. bound n (coeff p)"
   13.71 -proof -
   13.72 -  have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
   13.73 -  then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
   13.74 -  then show ?thesis ..
   13.75 -qed
   13.76 -  
   13.77 -lemma bound_coeff_obtain:
   13.78 -  assumes prem: "(!!n. bound n (coeff p) ==> P)" shows "P"
   13.79 -proof -
   13.80 -  have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
   13.81 -  then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
   13.82 -  with prem show P .
   13.83 -qed
   13.84 -
   13.85 -
   13.86 -text {* Ring operations *}
   13.87 -
   13.88 -instantiation up :: (zero) zero
   13.89 -begin
   13.90 -
   13.91 -definition
   13.92 -  up_zero_def: "0 = monom 0 0"
   13.93 -
   13.94 -instance ..
   13.95 -
   13.96 -end
   13.97 -
   13.98 -instantiation up :: ("{one, zero}") one
   13.99 -begin
  13.100 -
  13.101 -definition
  13.102 -  up_one_def: "1 = monom 1 0"
  13.103 -
  13.104 -instance ..
  13.105 -
  13.106 -end
  13.107 -
  13.108 -instantiation up :: ("{plus, zero}") plus
  13.109 -begin
  13.110 -
  13.111 -definition
  13.112 -  up_add_def: "p + q = Abs_UP (%n. Rep_UP p n + Rep_UP q n)"
  13.113 -
  13.114 -instance ..
  13.115 -
  13.116 -end
  13.117 -
  13.118 -instantiation up :: ("{one, times, uminus, zero}") uminus
  13.119 -begin
  13.120 -
  13.121 -definition
  13.122 -  (* note: - 1 is different from -1; latter is of class number *)
  13.123 -  up_uminus_def:"- p = (- 1) *s p"
  13.124 -  (* easier to use than "Abs_UP (%i. - Rep_UP p i)" *)
  13.125 -
  13.126 -instance ..
  13.127 -
  13.128 -end
  13.129 -
  13.130 -instantiation up :: ("{one, plus, times, minus, uminus, zero}") minus
  13.131 -begin
  13.132 -
  13.133 -definition
  13.134 -  up_minus_def: "(a :: 'a up) - b = a + (-b)"
  13.135 -
  13.136 -instance ..
  13.137 -
  13.138 -end
  13.139 -
  13.140 -instantiation up :: ("{times, comm_monoid_add}") times
  13.141 -begin
  13.142 -
  13.143 -definition
  13.144 -  up_mult_def: "p * q = Abs_UP (%n::nat. setsum
  13.145 -                     (%i. Rep_UP p i * Rep_UP q (n-i)) {..n})"
  13.146 -
  13.147 -instance ..
  13.148 -
  13.149 -end
  13.150 -
  13.151 -instance up :: ("{times, comm_monoid_add}") Rings.dvd ..
  13.152 -
  13.153 -instantiation up :: ("{times, one, comm_monoid_add, uminus, minus}") inverse
  13.154 -begin
  13.155 -
  13.156 -definition
  13.157 -  up_inverse_def: "inverse (a :: 'a up) = (if a dvd 1 then
  13.158 -                     THE x. a * x = 1 else 0)"
  13.159 -
  13.160 -definition
  13.161 -  up_divide_def: "(a :: 'a up) / b = a * inverse b"
  13.162 -
  13.163 -instance ..
  13.164 -
  13.165 -end
  13.166 -
  13.167 -
  13.168 -subsection {* Effect of operations on coefficients *}
  13.169 -
  13.170 -lemma coeff_monom [simp]: "coeff (monom a m) n = (if m=n then a else 0)"
  13.171 -proof -
  13.172 -  have "(%n. if n = m then a else 0) : UP"
  13.173 -    using UP_def by force
  13.174 -  from this show ?thesis
  13.175 -    by (simp add: coeff_def monom_def Abs_UP_inverse Rep_UP)
  13.176 -qed
  13.177 -
  13.178 -lemma coeff_zero [simp]: "coeff 0 n = 0"
  13.179 -proof (unfold up_zero_def)
  13.180 -qed simp
  13.181 -
  13.182 -lemma coeff_one [simp]: "coeff 1 n = (if n=0 then 1 else 0)"
  13.183 -proof (unfold up_one_def)
  13.184 -qed simp
  13.185 -
  13.186 -(* term order
  13.187 -lemma coeff_smult [simp]: "coeff (a *s p) n = (a::'a::ring) * coeff p n"
  13.188 -proof -
  13.189 -  have "!!f. f : UP ==> (%n. a * f n) : UP"
  13.190 -    by (unfold UP_def) (force simp add: algebra_simps)
  13.191 -*)      (* this force step is slow *)
  13.192 -(*  then show ?thesis
  13.193 -    apply (simp add: coeff_def smult_def Abs_UP_inverse Rep_UP)
  13.194 -qed
  13.195 -*)
  13.196 -lemma coeff_smult [simp]: "coeff (a *s p) n = (a::'a::ring) * coeff p n"
  13.197 -proof -
  13.198 -  have "Rep_UP p : UP ==> (%n. a * Rep_UP p n) : UP"
  13.199 -    by (unfold UP_def) (force simp add: algebra_simps)
  13.200 -      (* this force step is slow *)
  13.201 -  then show ?thesis
  13.202 -    by (simp add: coeff_def smult_def Abs_UP_inverse Rep_UP)
  13.203 -qed
  13.204 -
  13.205 -lemma coeff_add [simp]: "coeff (p+q) n = (coeff p n + coeff q n::'a::ring)"
  13.206 -proof -
  13.207 -  {
  13.208 -    fix f g
  13.209 -    assume fup: "(f::nat=>'a::ring) : UP" and gup: "(g::nat=>'a::ring) : UP"
  13.210 -    have "(%i. f i + g i) : UP"
  13.211 -    proof -
  13.212 -      from fup obtain n where boundn: "bound n f"
  13.213 -        by (unfold UP_def) fast
  13.214 -      from gup obtain m where boundm: "bound m g"
  13.215 -        by (unfold UP_def) fast
  13.216 -      have "bound (max n m) (%i. (f i + g i))"
  13.217 -      proof
  13.218 -        fix i
  13.219 -        assume "max n m < i"
  13.220 -        with boundn and boundm show "f i + g i = 0"
  13.221 -          by (fastforce simp add: algebra_simps)
  13.222 -      qed
  13.223 -      then show "(%i. (f i + g i)) : UP"
  13.224 -        by (unfold UP_def) fast
  13.225 -    qed
  13.226 -  }
  13.227 -  then show ?thesis
  13.228 -    by (simp add: coeff_def up_add_def Abs_UP_inverse Rep_UP)
  13.229 -qed
  13.230 -
  13.231 -lemma coeff_mult [simp]:
  13.232 -  "coeff (p * q) n = (setsum (%i. coeff p i * coeff q (n-i)) {..n}::'a::ring)"
  13.233 -proof -
  13.234 -  {
  13.235 -    fix f g
  13.236 -    assume fup: "(f::nat=>'a::ring) : UP" and gup: "(g::nat=>'a::ring) : UP"
  13.237 -    have "(%n. setsum (%i. f i * g (n-i)) {..n}) : UP"
  13.238 -    proof -
  13.239 -      from fup obtain n where "bound n f"
  13.240 -        by (unfold UP_def) fast
  13.241 -      from gup obtain m where "bound m g"
  13.242 -        by (unfold UP_def) fast
  13.243 -      have "bound (n + m) (%n. setsum (%i. f i * g (n-i)) {..n})"
  13.244 -      proof
  13.245 -        fix k
  13.246 -        assume bound: "n + m < k"
  13.247 -        {
  13.248 -          fix i
  13.249 -          have "f i * g (k-i) = 0"
  13.250 -          proof cases
  13.251 -            assume "n < i"
  13.252 -            with `bound n f` show ?thesis by (auto simp add: algebra_simps)
  13.253 -          next
  13.254 -            assume "~ (n < i)"
  13.255 -            with bound have "m < k-i" by arith
  13.256 -            with `bound m g` show ?thesis by (auto simp add: algebra_simps)
  13.257 -          qed
  13.258 -        }
  13.259 -        then show "setsum (%i. f i * g (k-i)) {..k} = 0"
  13.260 -          by (simp add: algebra_simps)
  13.261 -      qed
  13.262 -      then show "(%n. setsum (%i. f i * g (n-i)) {..n}) : UP"
  13.263 -        by (unfold UP_def) fast
  13.264 -    qed
  13.265 -  }
  13.266 -  then show ?thesis
  13.267 -    by (simp add: coeff_def up_mult_def Abs_UP_inverse Rep_UP)
  13.268 -qed
  13.269 -
  13.270 -lemma coeff_uminus [simp]: "coeff (-p) n = (-coeff p n::'a::ring)"
  13.271 -by (unfold up_uminus_def) (simp add: algebra_simps)
  13.272 -
  13.273 -(* Other lemmas *)
  13.274 -
  13.275 -lemma up_eqI: assumes prem: "(!! n. coeff p n = coeff q n)" shows "p = q"
  13.276 -proof -
  13.277 -  have "p = Abs_UP (%u. Rep_UP p u)" by (simp add: Rep_UP_inverse)
  13.278 -  also from prem have "... = Abs_UP (Rep_UP q)" by (simp only: coeff_def)
  13.279 -  also have "... = q" by (simp add: Rep_UP_inverse)
  13.280 -  finally show ?thesis .
  13.281 -qed
  13.282 -
  13.283 -instance up :: (ring) ring
  13.284 -proof
  13.285 -  fix p q r :: "'a::ring up"
  13.286 -  show "(p + q) + r = p + (q + r)"
  13.287 -    by (rule up_eqI) simp
  13.288 -  show "0 + p = p"
  13.289 -    by (rule up_eqI) simp
  13.290 -  show "(-p) + p = 0"
  13.291 -    by (rule up_eqI) simp
  13.292 -  show "p + q = q + p"
  13.293 -    by (rule up_eqI) simp
  13.294 -  show "(p * q) * r = p * (q * r)"
  13.295 -  proof (rule up_eqI)
  13.296 -    fix n 
  13.297 -    {
  13.298 -      fix k and a b c :: "nat=>'a::ring"
  13.299 -      have "k <= n ==> 
  13.300 -        setsum (%j. setsum (%i. a i * b (j-i)) {..j} * c (n-j)) {..k} = 
  13.301 -        setsum (%j. a j * setsum  (%i. b i * c (n-j-i)) {..k-j}) {..k}"
  13.302 -        (is "_ ==> ?eq k")
  13.303 -      proof (induct k)
  13.304 -        case 0 show ?case by simp
  13.305 -      next
  13.306 -        case (Suc k)
  13.307 -        then have "k <= n" by arith
  13.308 -        then have "?eq k" by (rule Suc)
  13.309 -        then show ?case
  13.310 -          by (simp add: Suc_diff_le natsum_ldistr)
  13.311 -      qed
  13.312 -    }
  13.313 -    then show "coeff ((p * q) * r) n = coeff (p * (q * r)) n"
  13.314 -      by simp
  13.315 -  qed
  13.316 -  show "1 * p = p"
  13.317 -  proof (rule up_eqI)
  13.318 -    fix n
  13.319 -    show "coeff (1 * p) n = coeff p n"
  13.320 -    proof (cases n)
  13.321 -      case 0 then show ?thesis by simp
  13.322 -    next
  13.323 -      case Suc then show ?thesis by (simp del: setsum_atMost_Suc add: natsum_Suc2)
  13.324 -    qed
  13.325 -  qed
  13.326 -  show "(p + q) * r = p * r + q * r"
  13.327 -    by (rule up_eqI) simp
  13.328 -  show "\<And>q. p * q = q * p"
  13.329 -  proof (rule up_eqI)
  13.330 -    fix q
  13.331 -    fix n 
  13.332 -    {
  13.333 -      fix k
  13.334 -      fix a b :: "nat=>'a::ring"
  13.335 -      have "k <= n ==> 
  13.336 -        setsum (%i. a i * b (n-i)) {..k} =
  13.337 -        setsum (%i. a (k-i) * b (i+n-k)) {..k}"
  13.338 -        (is "_ ==> ?eq k")
  13.339 -      proof (induct k)
  13.340 -        case 0 show ?case by simp
  13.341 -      next
  13.342 -        case (Suc k) then show ?case by (subst natsum_Suc2) simp
  13.343 -      qed
  13.344 -    }
  13.345 -    then show "coeff (p * q) n = coeff (q * p) n"
  13.346 -      by simp
  13.347 -  qed
  13.348 -
  13.349 -  show "p - q = p + (-q)"
  13.350 -    by (simp add: up_minus_def)
  13.351 -  show "inverse p = (if p dvd 1 then THE x. p*x = 1 else 0)"
  13.352 -    by (simp add: up_inverse_def)
  13.353 -  show "p / q = p * inverse q"
  13.354 -    by (simp add: up_divide_def)
  13.355 -qed
  13.356 -
  13.357 -(* Further properties of monom *)
  13.358 -
  13.359 -lemma monom_zero [simp]:
  13.360 -  "monom 0 n = 0"
  13.361 -  by (simp add: monom_def up_zero_def)
  13.362 -(* term order: application of coeff_mult goes wrong: rule not symmetric
  13.363 -lemma monom_mult_is_smult:
  13.364 -  "monom (a::'a::ring) 0 * p = a *s p"
  13.365 -proof (rule up_eqI)
  13.366 -  fix k
  13.367 -  show "coeff (monom a 0 * p) k = coeff (a *s p) k"
  13.368 -  proof (cases k)
  13.369 -    case 0 then show ?thesis by simp
  13.370 -  next
  13.371 -    case Suc then show ?thesis by simp
  13.372 -  qed
  13.373 -qed
  13.374 -*)
  13.375 -
  13.376 -lemma monom_mult_is_smult:
  13.377 -  "monom (a::'a::ring) 0 * p = a *s p"
  13.378 -proof (rule up_eqI)
  13.379 -  note [[simproc del: ring]]
  13.380 -  fix k
  13.381 -  have "coeff (p * monom a 0) k = coeff (a *s p) k"
  13.382 -  proof (cases k)
  13.383 -    case 0 then show ?thesis by simp ring
  13.384 -  next
  13.385 -    case Suc then show ?thesis by simp (ring, simp)
  13.386 -  qed
  13.387 -  then show "coeff (monom a 0 * p) k = coeff (a *s p) k" by ring
  13.388 -qed
  13.389 -
  13.390 -lemma monom_add [simp]:
  13.391 -  "monom (a + b) n = monom (a::'a::ring) n + monom b n"
  13.392 -by (rule up_eqI) simp
  13.393 -
  13.394 -lemma monom_mult_smult:
  13.395 -  "monom (a * b) n = a *s monom (b::'a::ring) n"
  13.396 -by (rule up_eqI) simp
  13.397 -
  13.398 -lemma monom_uminus [simp]:
  13.399 -  "monom (-a) n = - monom (a::'a::ring) n"
  13.400 -by (rule up_eqI) simp
  13.401 -
  13.402 -lemma monom_one [simp]:
  13.403 -  "monom 1 0 = 1"
  13.404 -by (simp add: up_one_def)
  13.405 -
  13.406 -lemma monom_inj:
  13.407 -  "(monom a n = monom b n) = (a = b)"
  13.408 -proof
  13.409 -  assume "monom a n = monom b n"
  13.410 -  then have "coeff (monom a n) n = coeff (monom b n) n" by simp
  13.411 -  then show "a = b" by simp
  13.412 -next
  13.413 -  assume "a = b" then show "monom a n = monom b n" by simp
  13.414 -qed
  13.415 -
  13.416 -(* Properties of *s:
  13.417 -   Polynomials form a module *)
  13.418 -
  13.419 -lemma smult_l_distr:
  13.420 -  "(a + b::'a::ring) *s p = a *s p + b *s p"
  13.421 -by (rule up_eqI) simp
  13.422 -
  13.423 -lemma smult_r_distr:
  13.424 -  "(a::'a::ring) *s (p + q) = a *s p + a *s q"
  13.425 -by (rule up_eqI) simp
  13.426 -
  13.427 -lemma smult_assoc1:
  13.428 -  "(a * b::'a::ring) *s p = a *s (b *s p)"
  13.429 -by (rule up_eqI) simp
  13.430 -
  13.431 -lemma smult_one [simp]:
  13.432 -  "(1::'a::ring) *s p = p"
  13.433 -by (rule up_eqI) simp
  13.434 -
  13.435 -(* Polynomials form an algebra *)
  13.436 -
  13.437 -lemma smult_assoc2:
  13.438 -  "(a *s p) * q = (a::'a::ring) *s (p * q)"
  13.439 -using [[simproc del: ring]]
  13.440 -by (rule up_eqI) (simp add: natsum_rdistr m_assoc)
  13.441 -
  13.442 -(* the following can be derived from the above ones,
  13.443 -   for generality reasons, it is therefore done *)
  13.444 -
  13.445 -lemma smult_l_null [simp]:
  13.446 -  "(0::'a::ring) *s p = 0"
  13.447 -proof -
  13.448 -  fix a
  13.449 -  have "0 *s p = (0 *s p + a *s p) + - (a *s p)" by simp
  13.450 -  also have "... = (0 + a) *s p + - (a *s p)" by (simp only: smult_l_distr)
  13.451 -  also have "... = 0" by simp
  13.452 -  finally show ?thesis .
  13.453 -qed
  13.454 -
  13.455 -lemma smult_r_null [simp]:
  13.456 -  "(a::'a::ring) *s 0 = 0"
  13.457 -proof -
  13.458 -  fix p
  13.459 -  have "a *s 0 = (a *s 0 + a *s p) + - (a *s p)" by simp
  13.460 -  also have "... = a *s (0 + p) + - (a *s p)" by (simp only: smult_r_distr)
  13.461 -  also have "... = 0" by simp
  13.462 -  finally show ?thesis .
  13.463 -qed
  13.464 -
  13.465 -lemma smult_l_minus:
  13.466 -  "(-a::'a::ring) *s p = - (a *s p)"
  13.467 -proof -
  13.468 -  have "(-a) *s p = (-a *s p + a *s p) + -(a *s p)" by simp 
  13.469 -  also have "... = (-a + a) *s p + -(a *s p)" by (simp only: smult_l_distr)
  13.470 -  also have "... = -(a *s p)" by simp
  13.471 -  finally show ?thesis .
  13.472 -qed
  13.473 -
  13.474 -lemma smult_r_minus:
  13.475 -  "(a::'a::ring) *s (-p) = - (a *s p)"
  13.476 -proof -
  13.477 -  have "a *s (-p) = (a *s -p + a *s p) + -(a *s p)" by simp
  13.478 -  also have "... = a *s (-p + p) + -(a *s p)" by (simp only: smult_r_distr)
  13.479 -  also have "... = -(a *s p)" by simp
  13.480 -  finally show ?thesis .
  13.481 -qed
  13.482 -
  13.483 -
  13.484 -section {* The degree function *}
  13.485 -
  13.486 -definition
  13.487 -  deg :: "('a::zero) up => nat"
  13.488 -  where "deg p = (LEAST n. bound n (coeff p))"
  13.489 -
  13.490 -lemma deg_aboveI:
  13.491 -  "(!!m. n < m ==> coeff p m = 0) ==> deg p <= n"
  13.492 -by (unfold deg_def) (fast intro: Least_le)
  13.493 -
  13.494 -lemma deg_aboveD:
  13.495 -  assumes "deg p < m" shows "coeff p m = 0"
  13.496 -proof -
  13.497 -  obtain n where "bound n (coeff p)" by (rule bound_coeff_obtain)
  13.498 -  then have "bound (deg p) (coeff p)" by (unfold deg_def, rule LeastI)
  13.499 -  then show "coeff p m = 0" using `deg p < m` by (rule boundD)
  13.500 -qed
  13.501 -
  13.502 -lemma deg_belowI:
  13.503 -  assumes prem: "n ~= 0 ==> coeff p n ~= 0" shows "n <= deg p"
  13.504 -(* logically, this is a slightly stronger version of deg_aboveD *)
  13.505 -proof (cases "n=0")
  13.506 -  case True then show ?thesis by simp
  13.507 -next
  13.508 -  case False then have "coeff p n ~= 0" by (rule prem)
  13.509 -  then have "~ deg p < n" by (fast dest: deg_aboveD)
  13.510 -  then show ?thesis by arith
  13.511 -qed
  13.512 -
  13.513 -lemma lcoeff_nonzero_deg:
  13.514 -  assumes deg: "deg p ~= 0" shows "coeff p (deg p) ~= 0"
  13.515 -proof -
  13.516 -  obtain m where "deg p <= m" and m_coeff: "coeff p m ~= 0"
  13.517 -  proof -
  13.518 -    have minus: "!!(n::nat) m. n ~= 0 ==> (n - Suc 0 < m) = (n <= m)"
  13.519 -      by arith (* make public?, why does proof not work with "1" *)
  13.520 -    from deg have "deg p - 1 < (LEAST n. bound n (coeff p))"
  13.521 -      by (unfold deg_def) arith
  13.522 -    then have "~ bound (deg p - 1) (coeff p)" by (rule not_less_Least)
  13.523 -    then have "EX m. deg p - 1 < m & coeff p m ~= 0"
  13.524 -      by (unfold bound_def) fast
  13.525 -    then have "EX m. deg p <= m & coeff p m ~= 0" by (simp add: deg minus)
  13.526 -    then show ?thesis by (auto intro: that)
  13.527 -  qed
  13.528 -  with deg_belowI have "deg p = m" by fastforce
  13.529 -  with m_coeff show ?thesis by simp
  13.530 -qed
  13.531 -
  13.532 -lemma lcoeff_nonzero_nonzero:
  13.533 -  assumes deg: "deg p = 0" and nonzero: "p ~= 0" shows "coeff p 0 ~= 0"
  13.534 -proof -
  13.535 -  have "EX m. coeff p m ~= 0"
  13.536 -  proof (rule classical)
  13.537 -    assume "~ ?thesis"
  13.538 -    then have "p = 0" by (auto intro: up_eqI)
  13.539 -    with nonzero show ?thesis by contradiction
  13.540 -  qed
  13.541 -  then obtain m where coeff: "coeff p m ~= 0" ..
  13.542 -  then have "m <= deg p" by (rule deg_belowI)
  13.543 -  then have "m = 0" by (simp add: deg)
  13.544 -  with coeff show ?thesis by simp
  13.545 -qed
  13.546 -
  13.547 -lemma lcoeff_nonzero:
  13.548 -  "p ~= 0 ==> coeff p (deg p) ~= 0"
  13.549 -proof (cases "deg p = 0")
  13.550 -  case True
  13.551 -  assume "p ~= 0"
  13.552 -  with True show ?thesis by (simp add: lcoeff_nonzero_nonzero)
  13.553 -next
  13.554 -  case False
  13.555 -  assume "p ~= 0"
  13.556 -  with False show ?thesis by (simp add: lcoeff_nonzero_deg)
  13.557 -qed
  13.558 -
  13.559 -lemma deg_eqI:
  13.560 -  "[| !!m. n < m ==> coeff p m = 0;
  13.561 -      !!n. n ~= 0 ==> coeff p n ~= 0|] ==> deg p = n"
  13.562 -by (fast intro: le_antisym deg_aboveI deg_belowI)
  13.563 -
  13.564 -(* Degree and polynomial operations *)
  13.565 -
  13.566 -lemma deg_add [simp]:
  13.567 -  "deg ((p::'a::ring up) + q) <= max (deg p) (deg q)"
  13.568 -by (rule deg_aboveI) (simp add: deg_aboveD)
  13.569 -
  13.570 -lemma deg_monom_ring:
  13.571 -  "deg (monom a n::'a::ring up) <= n"
  13.572 -by (rule deg_aboveI) simp
  13.573 -
  13.574 -lemma deg_monom [simp]:
  13.575 -  "a ~= 0 ==> deg (monom a n::'a::ring up) = n"
  13.576 -by (fastforce intro: le_antisym deg_aboveI deg_belowI)
  13.577 -
  13.578 -lemma deg_const [simp]:
  13.579 -  "deg (monom (a::'a::ring) 0) = 0"
  13.580 -proof (rule le_antisym)
  13.581 -  show "deg (monom a 0) <= 0" by (rule deg_aboveI) simp
  13.582 -next
  13.583 -  show "0 <= deg (monom a 0)" by (rule deg_belowI) simp
  13.584 -qed
  13.585 -
  13.586 -lemma deg_zero [simp]:
  13.587 -  "deg 0 = 0"
  13.588 -proof (rule le_antisym)
  13.589 -  show "deg 0 <= 0" by (rule deg_aboveI) simp
  13.590 -next
  13.591 -  show "0 <= deg 0" by (rule deg_belowI) simp
  13.592 -qed
  13.593 -
  13.594 -lemma deg_one [simp]:
  13.595 -  "deg 1 = 0"
  13.596 -proof (rule le_antisym)
  13.597 -  show "deg 1 <= 0" by (rule deg_aboveI) simp
  13.598 -next
  13.599 -  show "0 <= deg 1" by (rule deg_belowI) simp
  13.600 -qed
  13.601 -
  13.602 -lemma uminus_monom:
  13.603 -  "!!a::'a::ring. (-a = 0) = (a = 0)"
  13.604 -proof
  13.605 -  fix a::"'a::ring"
  13.606 -  assume "a = 0"
  13.607 -  then show "-a = 0" by simp
  13.608 -next
  13.609 -  fix a::"'a::ring"
  13.610 -  assume "- a = 0"
  13.611 -  then have "-(- a) = 0" by simp
  13.612 -  then show "a = 0" by simp
  13.613 -qed
  13.614 -
  13.615 -lemma deg_uminus [simp]:
  13.616 -  "deg (-p::('a::ring) up) = deg p"
  13.617 -proof (rule le_antisym)
  13.618 -  show "deg (- p) <= deg p" by (simp add: deg_aboveI deg_aboveD)
  13.619 -next
  13.620 -  show "deg p <= deg (- p)" 
  13.621 -  by (simp add: deg_belowI lcoeff_nonzero_deg uminus_monom)
  13.622 -qed
  13.623 -
  13.624 -lemma deg_smult_ring:
  13.625 -  "deg ((a::'a::ring) *s p) <= (if a = 0 then 0 else deg p)"
  13.626 -proof (cases "a = 0")
  13.627 -qed (simp add: deg_aboveI deg_aboveD)+
  13.628 -
  13.629 -lemma deg_smult [simp]:
  13.630 -  "deg ((a::'a::domain) *s p) = (if a = 0 then 0 else deg p)"
  13.631 -proof (rule le_antisym)
  13.632 -  show "deg (a *s p) <= (if a = 0 then 0 else deg p)" by (rule deg_smult_ring)
  13.633 -next
  13.634 -  show "(if a = 0 then 0 else deg p) <= deg (a *s p)"
  13.635 -  proof (cases "a = 0")
  13.636 -  qed (simp, simp add: deg_belowI lcoeff_nonzero_deg integral_iff)
  13.637 -qed
  13.638 -
  13.639 -lemma deg_mult_ring:
  13.640 -  "deg (p * q::'a::ring up) <= deg p + deg q"
  13.641 -proof (rule deg_aboveI)
  13.642 -  fix m
  13.643 -  assume boundm: "deg p + deg q < m"
  13.644 -  {
  13.645 -    fix k i
  13.646 -    assume boundk: "deg p + deg q < k"
  13.647 -    then have "coeff p i * coeff q (k - i) = 0"
  13.648 -    proof (cases "deg p < i")
  13.649 -      case True then show ?thesis by (simp add: deg_aboveD)
  13.650 -    next
  13.651 -      case False with boundk have "deg q < k - i" by arith
  13.652 -      then show ?thesis by (simp add: deg_aboveD)
  13.653 -    qed
  13.654 -  }
  13.655 -      (* This is similar to bound_mult_zero and deg_above_mult_zero in the old
  13.656 -         proofs. *)
  13.657 -  with boundm show "coeff (p * q) m = 0" by simp
  13.658 -qed
  13.659 -
  13.660 -lemma deg_mult [simp]:
  13.661 -  "[| (p::'a::domain up) ~= 0; q ~= 0|] ==> deg (p * q) = deg p + deg q"
  13.662 -proof (rule le_antisym)
  13.663 -  show "deg (p * q) <= deg p + deg q" by (rule deg_mult_ring)
  13.664 -next
  13.665 -  let ?s = "(%i. coeff p i * coeff q (deg p + deg q - i))"
  13.666 -  assume nz: "p ~= 0" "q ~= 0"
  13.667 -  have less_add_diff: "!!(k::nat) n m. k < n ==> m < n + m - k" by arith
  13.668 -  show "deg p + deg q <= deg (p * q)"
  13.669 -  proof (rule deg_belowI, simp)
  13.670 -    have "setsum ?s {.. deg p + deg q}
  13.671 -      = setsum ?s ({..< deg p} Un {deg p .. deg p + deg q})"
  13.672 -      by (simp only: ivl_disj_un_one)
  13.673 -    also have "... = setsum ?s {deg p .. deg p + deg q}"
  13.674 -      by (simp add: setsum_Un_disjoint ivl_disj_int_one
  13.675 -        setsum_0 deg_aboveD less_add_diff)
  13.676 -    also have "... = setsum ?s ({deg p} Un {deg p <.. deg p + deg q})"
  13.677 -      by (simp only: ivl_disj_un_singleton)
  13.678 -    also have "... = coeff p (deg p) * coeff q (deg q)" 
  13.679 -      by (simp add: setsum_Un_disjoint setsum_0 deg_aboveD)
  13.680 -    finally have "setsum ?s {.. deg p + deg q} 
  13.681 -      = coeff p (deg p) * coeff q (deg q)" .
  13.682 -    with nz show "setsum ?s {.. deg p + deg q} ~= 0"
  13.683 -      by (simp add: integral_iff lcoeff_nonzero)
  13.684 -    qed
  13.685 -  qed
  13.686 -
  13.687 -lemma coeff_natsum:
  13.688 -  "((coeff (setsum p A) k)::'a::ring) = 
  13.689 -   setsum (%i. coeff (p i) k) A"
  13.690 -proof (cases "finite A")
  13.691 -  case True then show ?thesis by induct auto
  13.692 -next
  13.693 -  case False then show ?thesis by simp
  13.694 -qed
  13.695 -(* Instance of a more general result!!! *)
  13.696 -
  13.697 -(*
  13.698 -lemma coeff_natsum:
  13.699 -  "((coeff (setsum p {..n::nat}) k)::'a::ring) = 
  13.700 -   setsum (%i. coeff (p i) k) {..n}"
  13.701 -by (induct n) auto
  13.702 -*)
  13.703 -
  13.704 -lemma up_repr:
  13.705 -  "setsum (%i. monom (coeff p i) i) {..deg (p::'a::ring up)} = p"
  13.706 -proof (rule up_eqI)
  13.707 -  let ?s = "(%i. monom (coeff p i) i)"
  13.708 -  fix k
  13.709 -  show "coeff (setsum ?s {..deg p}) k = coeff p k"
  13.710 -  proof (cases "k <= deg p")
  13.711 -    case True
  13.712 -    hence "coeff (setsum ?s {..deg p}) k = 
  13.713 -          coeff (setsum ?s ({..k} Un {k<..deg p})) k"
  13.714 -      by (simp only: ivl_disj_un_one)
  13.715 -    also from True
  13.716 -    have "... = coeff (setsum ?s {..k}) k"
  13.717 -      by (simp add: setsum_Un_disjoint ivl_disj_int_one order_less_imp_not_eq2
  13.718 -        setsum_0 coeff_natsum )
  13.719 -    also
  13.720 -    have "... = coeff (setsum ?s ({..<k} Un {k})) k"
  13.721 -      by (simp only: ivl_disj_un_singleton)
  13.722 -    also have "... = coeff p k"
  13.723 -      by (simp add: setsum_Un_disjoint setsum_0 coeff_natsum deg_aboveD)
  13.724 -    finally show ?thesis .
  13.725 -  next
  13.726 -    case False
  13.727 -    hence "coeff (setsum ?s {..deg p}) k = 
  13.728 -          coeff (setsum ?s ({..<deg p} Un {deg p})) k"
  13.729 -      by (simp only: ivl_disj_un_singleton)
  13.730 -    also from False have "... = coeff p k"
  13.731 -      by (simp add: setsum_Un_disjoint setsum_0 coeff_natsum deg_aboveD)
  13.732 -    finally show ?thesis .
  13.733 -  qed
  13.734 -qed
  13.735 -
  13.736 -lemma up_repr_le:
  13.737 -  "deg (p::'a::ring up) <= n ==> setsum (%i. monom (coeff p i) i) {..n} = p"
  13.738 -proof -
  13.739 -  let ?s = "(%i. monom (coeff p i) i)"
  13.740 -  assume "deg p <= n"
  13.741 -  then have "setsum ?s {..n} = setsum ?s ({..deg p} Un {deg p<..n})"
  13.742 -    by (simp only: ivl_disj_un_one)
  13.743 -  also have "... = setsum ?s {..deg p}"
  13.744 -    by (simp add: setsum_Un_disjoint ivl_disj_int_one
  13.745 -      setsum_0 deg_aboveD)
  13.746 -  also have "... = p" by (rule up_repr)
  13.747 -  finally show ?thesis .
  13.748 -qed
  13.749 -
  13.750 -instance up :: ("domain") "domain"
  13.751 -proof
  13.752 -  show "1 ~= (0::'a up)"
  13.753 -  proof (* notI is applied here *)
  13.754 -    assume "1 = (0::'a up)"
  13.755 -    hence "coeff 1 0 = (coeff 0 0::'a)" by simp
  13.756 -    hence "1 = (0::'a)" by simp
  13.757 -    with one_not_zero show "False" by contradiction
  13.758 -  qed
  13.759 -next
  13.760 -  fix p q :: "'a::domain up"
  13.761 -  assume pq: "p * q = 0"
  13.762 -  show "p = 0 | q = 0"
  13.763 -  proof (rule classical)
  13.764 -    assume c: "~ (p = 0 | q = 0)"
  13.765 -    then have "deg p + deg q = deg (p * q)" by simp
  13.766 -    also from pq have "... = 0" by simp
  13.767 -    finally have "deg p + deg q = 0" .
  13.768 -    then have f1: "deg p = 0 & deg q = 0" by simp
  13.769 -    from f1 have "p = setsum (%i. (monom (coeff p i) i)) {..0}"
  13.770 -      by (simp only: up_repr_le)
  13.771 -    also have "... = monom (coeff p 0) 0" by simp
  13.772 -    finally have p: "p = monom (coeff p 0) 0" .
  13.773 -    from f1 have "q = setsum (%i. (monom (coeff q i) i)) {..0}"
  13.774 -      by (simp only: up_repr_le)
  13.775 -    also have "... = monom (coeff q 0) 0" by simp
  13.776 -    finally have q: "q = monom (coeff q 0) 0" .
  13.777 -    have "coeff p 0 * coeff q 0 = coeff (p * q) 0" by simp
  13.778 -    also from pq have "... = 0" by simp
  13.779 -    finally have "coeff p 0 * coeff q 0 = 0" .
  13.780 -    then have "coeff p 0 = 0 | coeff q 0 = 0" by (simp only: integral_iff)
  13.781 -    with p q show "p = 0 | q = 0" by fastforce
  13.782 -  qed
  13.783 -qed
  13.784 -
  13.785 -lemma monom_inj_zero:
  13.786 -  "(monom a n = 0) = (a = 0)"
  13.787 -proof -
  13.788 -  have "(monom a n = 0) = (monom a n = monom 0 n)" by simp
  13.789 -  also have "... = (a = 0)" by (simp add: monom_inj del: monom_zero)
  13.790 -  finally show ?thesis .
  13.791 -qed
  13.792 -(* term order: makes this simpler!!!
  13.793 -lemma smult_integral:
  13.794 -  "(a::'a::domain) *s p = 0 ==> a = 0 | p = 0"
  13.795 -by (simp add: monom_mult_is_smult [THEN sym] integral_iff monom_inj_zero) fast
  13.796 -*)
  13.797 -lemma smult_integral:
  13.798 -  "(a::'a::domain) *s p = 0 ==> a = 0 | p = 0"
  13.799 -by (simp add: monom_mult_is_smult [THEN sym] integral_iff monom_inj_zero)
  13.800 -
  13.801 -
  13.802 -(* Divisibility and degree *)
  13.803 -
  13.804 -lemma "!! p::'a::domain up. [| p dvd q; q ~= 0 |] ==> deg p <= deg q"
  13.805 -  apply (unfold dvd_def)
  13.806 -  apply (erule exE)
  13.807 -  apply hypsubst
  13.808 -  apply (case_tac "p = 0")
  13.809 -   apply (case_tac [2] "k = 0")
  13.810 -    apply auto
  13.811 -  done
  13.812 -
  13.813 -end
    14.1 --- a/src/HOL/ROOT	Mon Mar 25 19:53:44 2013 +0100
    14.2 +++ b/src/HOL/ROOT	Mon Mar 25 20:00:27 2013 +0100
    14.3 @@ -268,10 +268,6 @@
    14.4      Divisibility         (* Rings *)
    14.5      IntRing              (* Ideals and residue classes *)
    14.6      UnivPoly             (* Polynomials *)
    14.7 -  theories [document = false]
    14.8 -    (*** Old development, based on axiomatic type classes ***)
    14.9 -    "abstract/Abstract"  (*The ring theory*)
   14.10 -    "poly/Polynomial"    (*The full theory*)
   14.11    files "document/root.bib" "document/root.tex"
   14.12  
   14.13  session "HOL-Auth" in Auth = HOL +