# HG changeset patch
# User ballarin
# Date 1364238027 -3600
# Node ID 7957d26c3334269feb9d3912918ee42d1a0a6118
# Parent 237190475d790f2aac1f0108174a3e1f8dbb77e0
Discontinued theories src/HOL/Algebra/abstract and .../poly.
diff -r 237190475d79 -r 7957d26c3334 NEWS
--- a/NEWS Mon Mar 25 19:53:44 2013 +0100
+++ b/NEWS Mon Mar 25 20:00:27 2013 +0100
@@ -92,6 +92,14 @@
isar_shrink ~> isar_compress
+*** HOL-Algebra ***
+
+* Discontinued theories src/HOL/Algebra/abstract and .../poly.
+Existing theories should be based on src/HOL/Library/Polynomial
+instead. The latter provides integration with HOL's type classes for
+rings. INCOMPATIBILITY.
+
+
*** System ***
* Discontinued "isabelle usedir" option -P (remote path) and -r (reset
diff -r 237190475d79 -r 7957d26c3334 src/HOL/Algebra/README.html
--- a/src/HOL/Algebra/README.html Mon Mar 25 19:53:44 2013 +0100
+++ b/src/HOL/Algebra/README.html Mon Mar 25 20:00:27 2013 +0100
@@ -68,42 +68,10 @@
Degree function. Universal Property.
-Legacy Development of Rings using Axiomatic Type Classes
-
-This development of univariate polynomials is separated into an
-abstract development of rings and the development of polynomials
-itself. The formalisation is based on [Jacobson1985], and polynomials
-have a sparse, mathematical representation. These theories were
-developed as a base for the integration of a computer algebra system
-to Isabelle [Ballarin1999], and was designed to match implementations
-of these domains in some typed computer algebra systems. Summary:
-
-
Rings:
- Classes of rings are represented by axiomatic type classes. The
- following are available:
+
Development of Polynomials using Type Classes
-
- ring: Commutative rings with one (including a summation
- operator, which is needed for the polynomials)
- domain: Integral domains
- factorial: Factorial domains (divisor chain condition is missing)
- pid: Principal ideal domains
- field: Fields
-
-
- Also, some facts about ring homomorphisms and ideals are mechanised.
-
-Polynomials:
- Polynomials have a natural, mathematical representation. Facts about
- the following topics are provided:
-
-
+A development of univariate polynomials for HOL's ring classes
+is available at HOL/Library/Polynomial.
[Jacobson1985] Nathan Jacobson, Basic Algebra I, Freeman, 1985.
diff -r 237190475d79 -r 7957d26c3334 src/HOL/Algebra/abstract/Abstract.thy
--- a/src/HOL/Algebra/abstract/Abstract.thy Mon Mar 25 19:53:44 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-(* Author: Clemens Ballarin, started 17 July 1997
-
-Summary theory of the development of abstract algebra.
-*)
-
-theory Abstract
-imports RingHomo Field
-begin
-
-end
diff -r 237190475d79 -r 7957d26c3334 src/HOL/Algebra/abstract/Factor.thy
--- a/src/HOL/Algebra/abstract/Factor.thy Mon Mar 25 19:53:44 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-(* Author: Clemens Ballarin, started 25 November 1997
-
-Factorisation within a factorial domain.
-*)
-
-theory Factor
-imports Ring2
-begin
-
-definition
- Factorisation :: "['a::ring, 'a list, 'a] => bool" where
- (* factorisation of x into a list of irred factors and a unit u *)
- "Factorisation x factors u \
- x = foldr op* factors u &
- (ALL a : set factors. irred a) & u dvd 1"
-
-lemma irred_dvd_lemma: "!! c::'a::factorial.
- [| irred c; irred a; irred b; c dvd a*b |] ==> c assoc a | c assoc b"
- apply (unfold assoc_def)
- apply (frule factorial_prime)
- apply (unfold irred_def prime_def)
- apply blast
- done
-
-lemma irred_dvd_list_lemma: "!! c::'a::factorial.
- [| irred c; a dvd 1 |] ==>
- (ALL b : set factors. irred b) & c dvd foldr op* factors a -->
- (EX d. c assoc d & d : set factors)"
- apply (unfold assoc_def)
- apply (induct_tac factors)
- (* Base case: c dvd a contradicts irred c *)
- apply (simp add: irred_def)
- apply (blast intro: dvd_trans_ring)
- (* Induction step *)
- apply (frule factorial_prime)
- apply (simp add: irred_def prime_def)
- apply blast
- done
-
-lemma irred_dvd_list: "!! c::'a::factorial.
- [| irred c; ALL b : set factors. irred b; a dvd 1;
- c dvd foldr op* factors a |] ==>
- EX d. c assoc d & d : set factors"
- apply (rule irred_dvd_list_lemma [THEN mp])
- apply auto
- done
-
-lemma Factorisation_dvd: "!! c::'a::factorial.
- [| irred c; Factorisation x factors u; c dvd x |] ==>
- EX d. c assoc d & d : set factors"
- apply (unfold Factorisation_def)
- apply (rule irred_dvd_list_lemma [THEN mp])
- apply auto
- done
-
-lemma Factorisation_irred: "!! c::'a::factorial.
- [| Factorisation x factors u; a : set factors |] ==> irred a"
- unfolding Factorisation_def by blast
-
-end
diff -r 237190475d79 -r 7957d26c3334 src/HOL/Algebra/abstract/Field.thy
--- a/src/HOL/Algebra/abstract/Field.thy Mon Mar 25 19:53:44 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,21 +0,0 @@
-(* Author: Clemens Ballarin, started 15 November 1997
-
-Properties of abstract class field.
-*)
-
-theory Field
-imports Factor PID
-begin
-
-instance field < "domain"
- apply intro_classes
- apply (rule field_one_not_zero)
- apply (erule field_integral)
- done
-
-instance field < factorial
- apply intro_classes
- apply (erule field_fact_prime)
- done
-
-end
diff -r 237190475d79 -r 7957d26c3334 src/HOL/Algebra/abstract/Ideal2.thy
--- a/src/HOL/Algebra/abstract/Ideal2.thy Mon Mar 25 19:53:44 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,324 +0,0 @@
-(* Author: Clemens Ballarin, started 24 September 1999
-
-Ideals for commutative rings.
-*)
-
-theory Ideal2
-imports Ring2
-begin
-
-definition
- is_ideal :: "('a::ring) set => bool" where
- "is_ideal I \ (ALL a: I. ALL b: I. a + b : I) &
- (ALL a: I. - a : I) & 0 : I &
- (ALL a: I. ALL r. a * r : I)"
-
-definition
- ideal_of :: "('a::ring) set => 'a set" where
- "ideal_of S = Inter {I. is_ideal I & S <= I}"
-
-definition
- is_pideal :: "('a::ring) set => bool" where
- "is_pideal I \ (EX a. I = ideal_of {a})"
-
-
-text {* Principle ideal domains *}
-
-class pid =
- assumes pid_ax: "is_ideal (I :: ('a::domain) set) \ is_pideal I"
-
-(* is_ideal *)
-
-lemma is_idealI:
- "!! I. [| !! a b. [| a:I; b:I |] ==> a + b : I;
- !! a. a:I ==> - a : I; 0 : I;
- !! a r. a:I ==> a * r : I |] ==> is_ideal I"
- unfolding is_ideal_def by blast
-
-lemma is_ideal_add [simp]: "[| is_ideal I; a:I; b:I |] ==> a + b : I"
- unfolding is_ideal_def by blast
-
-lemma is_ideal_uminus [simp]: "[| is_ideal I; a:I |] ==> - a : I"
- unfolding is_ideal_def by blast
-
-lemma is_ideal_zero [simp]: "[| is_ideal I |] ==> 0 : I"
- unfolding is_ideal_def by blast
-
-lemma is_ideal_mult [simp]: "[| is_ideal I; a:I |] ==> a * r : I"
- unfolding is_ideal_def by blast
-
-lemma is_ideal_dvd: "[| a dvd b; is_ideal I; a:I |] ==> b:I"
- unfolding is_ideal_def dvd_def by blast
-
-lemma UNIV_is_ideal [simp]: "is_ideal (UNIV::('a::ring) set)"
- unfolding is_ideal_def by blast
-
-lemma zero_is_ideal [simp]: "is_ideal {0::'a::ring}"
- unfolding is_ideal_def by auto
-
-lemma is_ideal_1: "is_ideal {x::'a::ring. a dvd x}"
- apply (rule is_idealI)
- apply auto
- done
-
-lemma is_ideal_2: "is_ideal {x::'a::ring. EX u v. x = a * u + b * v}"
- apply (rule is_idealI)
- apply auto
- apply (rule_tac x = "u+ua" in exI)
- apply (rule_tac x = "v+va" in exI)
- apply (rule_tac [2] x = "-u" in exI)
- apply (rule_tac [2] x = "-v" in exI)
- apply (rule_tac [3] x = "0" in exI)
- apply (rule_tac [3] x = "0" in exI)
- apply (rule_tac [4] x = "u * r" in exI)
- apply (rule_tac [4] x = "v * r" in exI)
- apply simp_all
- done
-
-
-(* ideal_of *)
-
-lemma ideal_of_is_ideal: "is_ideal (ideal_of S)"
- unfolding is_ideal_def ideal_of_def by blast
-
-lemma generator_in_ideal: "a:S ==> a : (ideal_of S)"
- unfolding ideal_of_def by blast
-
-lemma ideal_of_one_eq: "ideal_of {1::'a::ring} = UNIV"
- apply (unfold ideal_of_def)
- apply (force dest: is_ideal_mult simp add: l_one)
- done
-
-lemma ideal_of_empty_eq: "ideal_of {} = {0::'a::ring}"
- apply (unfold ideal_of_def)
- apply (rule subset_antisym)
- apply (rule subsetI)
- apply (drule InterD)
- prefer 2 apply assumption
- apply (auto simp add: is_ideal_zero)
- done
-
-lemma pideal_structure: "ideal_of {a} = {x::'a::ring. a dvd x}"
- apply (unfold ideal_of_def)
- apply (rule subset_antisym)
- apply (rule subsetI)
- apply (drule InterD)
- prefer 2 apply assumption
- apply (auto intro: is_ideal_1)
- apply (simp add: is_ideal_dvd)
- done
-
-lemma ideal_of_2_structure:
- "ideal_of {a, b} = {x::'a::ring. EX u v. x = a * u + b * v}"
- apply (unfold ideal_of_def)
- apply (rule subset_antisym)
- apply (rule subsetI)
- apply (drule InterD)
- prefer 2 apply assumption
- using [[simproc del: ring]]
- apply (auto intro: is_ideal_2)
- using [[simproc ring]]
- apply (rule_tac x = "1" in exI)
- apply (rule_tac x = "0" in exI)
- apply (rule_tac [2] x = "0" in exI)
- apply (rule_tac [2] x = "1" in exI)
- apply simp
- apply simp
- done
-
-lemma ideal_of_mono: "A <= B ==> ideal_of A <= ideal_of B"
- unfolding ideal_of_def by blast
-
-lemma ideal_of_zero_eq: "ideal_of {0::'a::ring} = {0}"
- apply (simp add: pideal_structure)
- apply (rule subset_antisym)
- apply (auto intro: "dvd_zero_left")
- done
-
-lemma element_generates_subideal: "[| is_ideal I; a : I |] ==> ideal_of {a::'a::ring} <= I"
- apply (auto simp add: pideal_structure is_ideal_dvd)
- done
-
-
-(* is_pideal *)
-
-lemma is_pideal_imp_is_ideal: "is_pideal (I::('a::ring) set) ==> is_ideal I"
- unfolding is_pideal_def by (fast intro: ideal_of_is_ideal)
-
-lemma pideal_is_pideal: "is_pideal (ideal_of {a::'a::ring})"
- unfolding is_pideal_def by blast
-
-lemma is_pidealD: "is_pideal I ==> EX a. I = ideal_of {a}"
- unfolding is_pideal_def .
-
-
-(* Ideals and divisibility *)
-
-lemma dvd_imp_subideal: "b dvd a ==> ideal_of {a::'a::ring} <= ideal_of {b}"
- by (auto intro: dvd_trans_ring simp add: pideal_structure)
-
-lemma subideal_imp_dvd: "ideal_of {a::'a::ring} <= ideal_of {b} ==> b dvd a"
- by (auto dest!: subsetD simp add: pideal_structure)
-
-lemma psubideal_not_dvd: "(ideal_of {a::'a::ring} < ideal_of {b}) ==> ~ a dvd b"
- apply (simp add: psubset_eq pideal_structure)
- apply (erule conjE)
- apply (drule_tac c = "a" in subsetD)
- apply (auto intro: dvd_trans_ring)
- done
-
-lemma not_dvd_psubideal_singleton:
- "[| b dvd a; ~ a dvd b |] ==> ideal_of {a::'a::ring} < ideal_of {b}"
- apply (rule psubsetI)
- apply (erule dvd_imp_subideal)
- apply (blast intro: dvd_imp_subideal subideal_imp_dvd)
- done
-
-lemma subideal_is_dvd [iff]: "(ideal_of {a::'a::ring} <= ideal_of {b}) = (b dvd a)"
- apply (rule iffI)
- apply (assumption | rule subideal_imp_dvd dvd_imp_subideal)+
- done
-
-lemma psubideal_is_dvd [iff]: "(ideal_of {a::'a::ring} < ideal_of {b}) = (b dvd a & ~ a dvd b)"
- apply (rule iffI)
- apply (assumption | rule conjI psubideal_not_dvd psubset_imp_subset [THEN subideal_imp_dvd])+
- apply (erule conjE)
- apply (assumption | rule not_dvd_psubideal_singleton)+
- done
-
-lemma assoc_pideal_eq: "[| a dvd b; b dvd a |] ==> ideal_of {a::'a::ring} = ideal_of {b}"
- apply (rule subset_antisym)
- apply (assumption | rule dvd_imp_subideal)+
- done
-
-lemma dvd_imp_in_pideal: "!!a::'a::ring. a dvd b ==> b : (ideal_of {a})"
- apply (rule is_ideal_dvd)
- apply assumption
- apply (rule ideal_of_is_ideal)
- apply (rule generator_in_ideal)
- apply simp
- done
-
-lemma in_pideal_imp_dvd: "!!a::'a::ring. b : (ideal_of {a}) ==> a dvd b"
- by (simp add: pideal_structure)
-
-lemma not_dvd_psubideal: "~ (a dvd b) ==> ideal_of {a::'a::ring} < ideal_of {a, b}"
- apply (simp add: psubset_eq ideal_of_mono)
- apply (erule contrapos_pp)
- apply (simp add: ideal_of_2_structure)
- apply (rule in_pideal_imp_dvd)
- apply simp
- apply (rule_tac x = "0" in exI)
- apply (rule_tac x = "1" in exI)
- apply simp
- done
-
-lemma irred_imp_max_ideal:
- "[| irred (a::'a::ring); is_pideal I; ideal_of {a} < I |] ==> x : I"
- apply (unfold irred_def)
- apply (drule is_pidealD)
- apply (erule exE)
- apply clarify
- apply (erule_tac x = "aa" in allE)
- apply clarify
- apply (drule_tac a = "1" in dvd_imp_subideal)
- apply (auto simp add: ideal_of_one_eq)
- done
-
-(* Pid are factorial *)
-
-(* Divisor chain condition *)
-(* proofs not finished *)
-
-lemma subset_chain_lemma [rule_format (no_asm)]:
- "(ALL i. I i <= I (Suc i)) ==> (n <= m & a : I n --> a : I m)"
- apply (induct_tac m)
- apply blast
- (* induction step *)
- apply (rename_tac m)
- apply (case_tac "n <= m")
- apply auto
- apply (subgoal_tac "n = Suc m")
- prefer 2
- apply arith
- apply force
- done
-
-lemma chain_is_ideal: "[| ALL i. is_ideal (I i); ALL i. I i <= I (Suc i) |]
- ==> is_ideal (Union (I`UNIV))"
- apply (rule is_idealI)
- apply auto
- apply (rule_tac x = "max x xa" in exI)
- apply (rule is_ideal_add)
- apply simp
- apply (rule subset_chain_lemma)
- apply assumption
- apply (rule conjI)
- prefer 2
- apply assumption
- apply arith
- apply (rule subset_chain_lemma)
- apply assumption
- apply (rule conjI)
- prefer 2
- apply assumption
- apply arith
- apply (rule_tac x = "x" in exI)
- apply simp
- apply (rule_tac x = "x" in exI)
- apply simp
- done
-
-
-(* Primeness condition *)
-
-lemma pid_irred_imp_prime: "irred a ==> prime (a::'a::pid)"
- apply (unfold prime_def)
- apply (rule conjI)
- apply (rule_tac [2] conjI)
- apply (tactic "clarify_tac @{context} 3")
- apply (drule_tac [3] I = "ideal_of {a, b}" and x = "1" in irred_imp_max_ideal)
- apply (auto intro: ideal_of_is_ideal pid_ax simp add: irred_def not_dvd_psubideal pid_ax)
- apply (simp add: ideal_of_2_structure)
- apply clarify
- apply (drule_tac f = "op* aa" in arg_cong)
- apply (simp add: r_distr)
- apply (erule subst)
- using [[simproc del: ring]]
- apply (simp add: m_assoc [symmetric])
- done
-
-(* Fields are Pid *)
-
-lemma field_pideal_univ: "a ~= 0 ==> ideal_of {a::'a::field} = UNIV"
- apply (rule subset_antisym)
- apply simp
- apply (rule subset_trans)
- prefer 2
- apply (rule dvd_imp_subideal)
- apply (rule field_ax)
- apply assumption
- apply (simp add: ideal_of_one_eq)
- done
-
-lemma proper_ideal: "[| is_ideal I; I ~= {0} |] ==> {0} < I"
- by (simp add: psubset_eq not_sym is_ideal_zero)
-
-lemma field_pid: "is_ideal (I::('a::field) set) ==> is_pideal I"
- apply (unfold is_pideal_def)
- apply (case_tac "I = {0}")
- apply (rule_tac x = "0" in exI)
- apply (simp add: ideal_of_zero_eq)
- (* case "I ~= {0}" *)
- apply (frule proper_ideal)
- apply assumption
- apply (drule psubset_imp_ex_mem)
- apply (erule exE)
- apply (rule_tac x = b in exI)
- apply (cut_tac a = b in element_generates_subideal)
- apply assumption
- apply blast
- apply (auto simp add: field_pideal_univ)
- done
-
-end
diff -r 237190475d79 -r 7957d26c3334 src/HOL/Algebra/abstract/PID.thy
--- a/src/HOL/Algebra/abstract/PID.thy Mon Mar 25 19:53:44 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-(* Author: Clemens Ballarin, started 5 October 1999
-
-Principle ideal domains.
-*)
-
-theory PID
-imports Ideal2
-begin
-
-instance pid < factorial
- apply intro_classes
- apply (erule pid_irred_imp_prime)
- done
-
-end
diff -r 237190475d79 -r 7957d26c3334 src/HOL/Algebra/abstract/Ring2.thy
--- a/src/HOL/Algebra/abstract/Ring2.thy Mon Mar 25 19:53:44 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,485 +0,0 @@
-(* Title: HOL/Algebra/abstract/Ring2.thy
- Author: Clemens Ballarin
-
-The algebraic hierarchy of rings as axiomatic classes.
-*)
-
-header {* The algebraic hierarchy of rings as type classes *}
-
-theory Ring2
-imports Main
-begin
-
-subsection {* Ring axioms *}
-
-class ring = zero + one + plus + minus + uminus + times + inverse + power + dvd +
- assumes a_assoc: "(a + b) + c = a + (b + c)"
- and l_zero: "0 + a = a"
- and l_neg: "(-a) + a = 0"
- and a_comm: "a + b = b + a"
-
- assumes m_assoc: "(a * b) * c = a * (b * c)"
- and l_one: "1 * a = a"
-
- assumes l_distr: "(a + b) * c = a * c + b * c"
-
- assumes m_comm: "a * b = b * a"
-
- assumes minus_def: "a - b = a + (-b)"
- and inverse_def: "inverse a = (if a dvd 1 then THE x. a*x = 1 else 0)"
- and divide_def: "a / b = a * inverse b"
-begin
-
-definition
- assoc :: "'a \ 'a \ bool" (infixl "assoc" 50)
- where "a assoc b \ a dvd b & b dvd a"
-
-definition
- irred :: "'a \ bool" where
- "irred a \ a ~= 0 & ~ a dvd 1 & (ALL d. d dvd a --> d dvd 1 | a dvd d)"
-
-definition
- prime :: "'a \ bool" where
- "prime p \ p ~= 0 & ~ p dvd 1 & (ALL a b. p dvd (a*b) --> p dvd a | p dvd b)"
-
-end
-
-
-subsection {* Integral domains *}
-
-class "domain" = ring +
- assumes one_not_zero: "1 ~= 0"
- and integral: "a * b = 0 ==> a = 0 | b = 0"
-
-subsection {* Factorial domains *}
-
-class factorial = "domain" +
-(*
- Proper definition using divisor chain condition currently not supported.
- factorial_divisor: "wf {(a, b). a dvd b & ~ (b dvd a)}"
-*)
- (*assumes factorial_divisor: "True"*)
- assumes factorial_prime: "irred a ==> prime a"
-
-
-subsection {* Euclidean domains *}
-
-(*
-class euclidean = "domain" +
- assumes euclidean_ax: "b ~= 0 ==> Ex (% (q, r, e_size::('a::ringS)=>nat).
- a = b * q + r & e_size r < e_size b)"
-
- Nothing has been proved about Euclidean domains, yet.
- Design question:
- Fix quo, rem and e_size as constants that are axiomatised with
- euclidean_ax?
- - advantage: more pragmatic and easier to use
- - disadvantage: for every type, one definition of quo and rem will
- be fixed, users may want to use differing ones;
- also, it seems not possible to prove that fields are euclidean
- domains, because that would require generic (type-independent)
- definitions of quo and rem.
-*)
-
-subsection {* Fields *}
-
-class field = ring +
- assumes field_one_not_zero: "1 ~= 0"
- (* Avoid a common superclass as the first thing we will
- prove about fields is that they are domains. *)
- and field_ax: "a ~= 0 ==> a dvd 1"
-
-
-section {* Basic facts *}
-
-subsection {* Normaliser for rings *}
-
-(* derived rewrite rules *)
-
-lemma a_lcomm: "(a::'a::ring)+(b+c) = b+(a+c)"
- apply (rule a_comm [THEN trans])
- apply (rule a_assoc [THEN trans])
- apply (rule a_comm [THEN arg_cong])
- done
-
-lemma r_zero: "(a::'a::ring) + 0 = a"
- apply (rule a_comm [THEN trans])
- apply (rule l_zero)
- done
-
-lemma r_neg: "(a::'a::ring) + (-a) = 0"
- apply (rule a_comm [THEN trans])
- apply (rule l_neg)
- done
-
-lemma r_neg2: "(a::'a::ring) + (-a + b) = b"
- apply (rule a_assoc [symmetric, THEN trans])
- apply (simp add: r_neg l_zero)
- done
-
-lemma r_neg1: "-(a::'a::ring) + (a + b) = b"
- apply (rule a_assoc [symmetric, THEN trans])
- apply (simp add: l_neg l_zero)
- done
-
-
-(* auxiliary *)
-
-lemma a_lcancel: "!! a::'a::ring. a + b = a + c ==> b = c"
- apply (rule box_equals)
- prefer 2
- apply (rule l_zero)
- prefer 2
- apply (rule l_zero)
- apply (rule_tac a1 = a in l_neg [THEN subst])
- apply (simp add: a_assoc)
- done
-
-lemma minus_add: "-((a::'a::ring) + b) = (-a) + (-b)"
- apply (rule_tac a = "a + b" in a_lcancel)
- apply (simp add: r_neg l_neg l_zero a_assoc a_comm a_lcomm)
- done
-
-lemma minus_minus: "-(-(a::'a::ring)) = a"
- apply (rule a_lcancel)
- apply (rule r_neg [THEN trans])
- apply (rule l_neg [symmetric])
- done
-
-lemma minus0: "- 0 = (0::'a::ring)"
- apply (rule a_lcancel)
- apply (rule r_neg [THEN trans])
- apply (rule l_zero [symmetric])
- done
-
-
-(* derived rules for multiplication *)
-
-lemma m_lcomm: "(a::'a::ring)*(b*c) = b*(a*c)"
- apply (rule m_comm [THEN trans])
- apply (rule m_assoc [THEN trans])
- apply (rule m_comm [THEN arg_cong])
- done
-
-lemma r_one: "(a::'a::ring) * 1 = a"
- apply (rule m_comm [THEN trans])
- apply (rule l_one)
- done
-
-lemma r_distr: "(a::'a::ring) * (b + c) = a * b + a * c"
- apply (rule m_comm [THEN trans])
- apply (rule l_distr [THEN trans])
- apply (simp add: m_comm)
- done
-
-
-(* the following proof is from Jacobson, Basic Algebra I, pp. 88-89 *)
-lemma l_null: "0 * (a::'a::ring) = 0"
- apply (rule a_lcancel)
- apply (rule l_distr [symmetric, THEN trans])
- apply (simp add: r_zero)
- done
-
-lemma r_null: "(a::'a::ring) * 0 = 0"
- apply (rule m_comm [THEN trans])
- apply (rule l_null)
- done
-
-lemma l_minus: "(-(a::'a::ring)) * b = - (a * b)"
- apply (rule a_lcancel)
- apply (rule r_neg [symmetric, THEN [2] trans])
- apply (rule l_distr [symmetric, THEN trans])
- apply (simp add: l_null r_neg)
- done
-
-lemma r_minus: "(a::'a::ring) * (-b) = - (a * b)"
- apply (rule a_lcancel)
- apply (rule r_neg [symmetric, THEN [2] trans])
- apply (rule r_distr [symmetric, THEN trans])
- apply (simp add: r_null r_neg)
- done
-
-(*** Term order for commutative rings ***)
-
-ML {*
-fun ring_ord (Const (a, _)) =
- find_index (fn a' => a = a')
- [@{const_name Groups.zero}, @{const_name Groups.plus}, @{const_name Groups.uminus},
- @{const_name Groups.minus}, @{const_name Groups.one}, @{const_name Groups.times}]
- | ring_ord _ = ~1;
-
-fun termless_ring (a, b) = (Term_Ord.term_lpo ring_ord (a, b) = LESS);
-
-val ring_ss =
- (HOL_basic_ss |> Simplifier.set_termless termless_ring)
- addsimps
- [@{thm a_assoc}, @{thm l_zero}, @{thm l_neg}, @{thm a_comm}, @{thm m_assoc},
- @{thm l_one}, @{thm l_distr}, @{thm m_comm}, @{thm minus_def},
- @{thm r_zero}, @{thm r_neg}, @{thm r_neg2}, @{thm r_neg1}, @{thm minus_add},
- @{thm minus_minus}, @{thm minus0}, @{thm a_lcomm}, @{thm m_lcomm}, (*@{thm r_one},*)
- @{thm r_distr}, @{thm l_null}, @{thm r_null}, @{thm l_minus}, @{thm r_minus}];
-*} (* Note: r_one is not necessary in ring_ss *)
-
-method_setup ring = {*
- Scan.succeed (K (SIMPLE_METHOD' (full_simp_tac ring_ss)))
-*} "compute distributive normal form in rings"
-
-
-subsection {* Rings and the summation operator *}
-
-(* Basic facts --- move to HOL!!! *)
-
-(* needed because natsum_cong (below) disables atMost_0 *)
-lemma natsum_0 [simp]: "setsum f {..(0::nat)} = (f 0::'a::comm_monoid_add)"
-by simp
-(*
-lemma natsum_Suc [simp]:
- "setsum f {..Suc n} = (f (Suc n) + setsum f {..n}::'a::comm_monoid_add)"
-by (simp add: atMost_Suc)
-*)
-lemma natsum_Suc2:
- "setsum f {..Suc n} = (f 0::'a::comm_monoid_add) + (setsum (%i. f (Suc i)) {..n})"
-proof (induct n)
- case 0 show ?case by simp
-next
- case Suc thus ?case by (simp add: add_assoc)
-qed
-
-lemma natsum_cong [cong]:
- "!!k. [| j = k; !!i::nat. i <= k ==> f i = (g i::'a::comm_monoid_add) |] ==>
- setsum f {..j} = setsum g {..k}"
-by (induct j) auto
-
-lemma natsum_zero [simp]: "setsum (%i. 0) {..n::nat} = (0::'a::comm_monoid_add)"
-by (induct n) simp_all
-
-lemma natsum_add [simp]:
- "!!f::nat=>'a::comm_monoid_add.
- setsum (%i. f i + g i) {..n::nat} = setsum f {..n} + setsum g {..n}"
-by (induct n) (simp_all add: add_ac)
-
-(* Facts specific to rings *)
-
-subclass (in ring) comm_monoid_add
-proof
- fix x y z
- show "x + y = y + x" by (rule a_comm)
- show "(x + y) + z = x + (y + z)" by (rule a_assoc)
- show "0 + x = x" by (rule l_zero)
-qed
-
-simproc_setup
- ring ("t + u::'a::ring" | "t - u::'a::ring" | "t * u::'a::ring" | "- t::'a::ring") =
-{*
- fn _ => fn ss => fn ct =>
- let
- val ctxt = Simplifier.the_context ss;
- val {t, T, maxidx, ...} = Thm.rep_cterm ct;
- val rew =
- Goal.prove ctxt [] []
- (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, Var (("x", maxidx + 1), T))))
- (fn _ => simp_tac (Simplifier.inherit_context ss ring_ss) 1)
- |> mk_meta_eq;
- val (t', u) = Logic.dest_equals (Thm.prop_of rew);
- in if t' aconv u then NONE else SOME rew end
-*}
-
-lemma natsum_ldistr:
- "!!a::'a::ring. setsum f {..n::nat} * a = setsum (%i. f i * a) {..n}"
-by (induct n) simp_all
-
-lemma natsum_rdistr:
- "!!a::'a::ring. a * setsum f {..n::nat} = setsum (%i. a * f i) {..n}"
-by (induct n) simp_all
-
-subsection {* Integral Domains *}
-
-declare one_not_zero [simp]
-
-lemma zero_not_one [simp]:
- "0 ~= (1::'a::domain)"
-by (rule not_sym) simp
-
-lemma integral_iff: (* not by default a simp rule! *)
- "(a * b = (0::'a::domain)) = (a = 0 | b = 0)"
-proof
- assume "a * b = 0" then show "a = 0 | b = 0" by (simp add: integral)
-next
- assume "a = 0 | b = 0" then show "a * b = 0" by auto
-qed
-
-(*
-lemma "(a::'a::ring) - (a - b) = b" apply simp
- simproc seems to fail on this example (fixed with new term order)
-*)
-(*
-lemma bug: "(b::'a::ring) - (b - a) = a" by simp
- simproc for rings cannot prove "(a::'a::ring) - (a - b) = b"
-*)
-lemma m_lcancel:
- assumes prem: "(a::'a::domain) ~= 0" shows conc: "(a * b = a * c) = (b = c)"
-proof
- assume eq: "a * b = a * c"
- then have "a * (b - c) = 0" by simp
- then have "a = 0 | (b - c) = 0" by (simp only: integral_iff)
- with prem have "b - c = 0" by auto
- then have "b = b - (b - c)" by simp
- also have "b - (b - c) = c" by simp
- finally show "b = c" .
-next
- assume "b = c" then show "a * b = a * c" by simp
-qed
-
-lemma m_rcancel:
- "(a::'a::domain) ~= 0 ==> (b * a = c * a) = (b = c)"
-by (simp add: m_lcancel)
-
-declare power_Suc [simp]
-
-lemma power_one [simp]:
- "1 ^ n = (1::'a::ring)" by (induct n) simp_all
-
-lemma power_zero [simp]:
- "n \ 0 \ 0 ^ n = (0::'a::ring)" by (induct n) simp_all
-
-lemma power_mult [simp]:
- "(a::'a::ring) ^ m * a ^ n = a ^ (m + n)"
- by (induct m) simp_all
-
-
-section "Divisibility"
-
-lemma dvd_zero_right [simp]:
- "(a::'a::ring) dvd 0"
-proof
- show "0 = a * 0" by simp
-qed
-
-lemma dvd_zero_left:
- "0 dvd (a::'a::ring) \ a = 0" unfolding dvd_def by simp
-
-lemma dvd_refl_ring [simp]:
- "(a::'a::ring) dvd a"
-proof
- show "a = a * 1" by simp
-qed
-
-lemma dvd_trans_ring:
- fixes a b c :: "'a::ring"
- assumes a_dvd_b: "a dvd b"
- and b_dvd_c: "b dvd c"
- shows "a dvd c"
-proof -
- from a_dvd_b obtain l where "b = a * l" using dvd_def by blast
- moreover from b_dvd_c obtain j where "c = b * j" using dvd_def by blast
- ultimately have "c = a * (l * j)" by simp
- then have "\k. c = a * k" ..
- then show ?thesis using dvd_def by blast
-qed
-
-
-lemma unit_mult:
- "!!a::'a::ring. [| a dvd 1; b dvd 1 |] ==> a * b dvd 1"
- apply (unfold dvd_def)
- apply clarify
- apply (rule_tac x = "k * ka" in exI)
- apply simp
- done
-
-lemma unit_power: "!!a::'a::ring. a dvd 1 ==> a^n dvd 1"
- apply (induct_tac n)
- apply simp
- apply (simp add: unit_mult)
- done
-
-lemma dvd_add_right [simp]:
- "!! a::'a::ring. [| a dvd b; a dvd c |] ==> a dvd b + c"
- apply (unfold dvd_def)
- apply clarify
- apply (rule_tac x = "k + ka" in exI)
- apply (simp add: r_distr)
- done
-
-lemma dvd_uminus_right [simp]:
- "!! a::'a::ring. a dvd b ==> a dvd -b"
- apply (unfold dvd_def)
- apply clarify
- apply (rule_tac x = "-k" in exI)
- apply (simp add: r_minus)
- done
-
-lemma dvd_l_mult_right [simp]:
- "!! a::'a::ring. a dvd b ==> a dvd c*b"
- apply (unfold dvd_def)
- apply clarify
- apply (rule_tac x = "c * k" in exI)
- apply simp
- done
-
-lemma dvd_r_mult_right [simp]:
- "!! a::'a::ring. a dvd b ==> a dvd b*c"
- apply (unfold dvd_def)
- apply clarify
- apply (rule_tac x = "k * c" in exI)
- apply simp
- done
-
-
-(* Inverse of multiplication *)
-
-section "inverse"
-
-lemma inverse_unique: "!! a::'a::ring. [| a * x = 1; a * y = 1 |] ==> x = y"
- apply (rule_tac a = "(a*y) * x" and b = "y * (a*x)" in box_equals)
- apply (simp (no_asm))
- apply auto
- done
-
-lemma r_inverse_ring: "!! a::'a::ring. a dvd 1 ==> a * inverse a = 1"
- apply (unfold inverse_def dvd_def)
- using [[simproc del: ring]]
- apply simp
- apply clarify
- apply (rule theI)
- apply assumption
- apply (rule inverse_unique)
- apply assumption
- apply assumption
- done
-
-lemma l_inverse_ring: "!! a::'a::ring. a dvd 1 ==> inverse a * a = 1"
- by (simp add: r_inverse_ring)
-
-
-(* Fields *)
-
-section "Fields"
-
-lemma field_unit [simp]: "!! a::'a::field. (a dvd 1) = (a ~= 0)"
- by (auto dest: field_ax dvd_zero_left simp add: field_one_not_zero)
-
-lemma r_inverse [simp]: "!! a::'a::field. a ~= 0 ==> a * inverse a = 1"
- by (simp add: r_inverse_ring)
-
-lemma l_inverse [simp]: "!! a::'a::field. a ~= 0 ==> inverse a * a= 1"
- by (simp add: l_inverse_ring)
-
-
-(* fields are integral domains *)
-
-lemma field_integral: "!! a::'a::field. a * b = 0 ==> a = 0 | b = 0"
- apply step
- apply (rule_tac a = " (a*b) * inverse b" in box_equals)
- apply (rule_tac [3] refl)
- prefer 2
- apply (simp (no_asm))
- apply auto
- done
-
-
-(* fields are factorial domains *)
-
-lemma field_fact_prime: "!! a::'a::field. irred a ==> prime a"
- unfolding prime_def irred_def by (blast intro: field_ax)
-
-end
diff -r 237190475d79 -r 7957d26c3334 src/HOL/Algebra/abstract/RingHomo.thy
--- a/src/HOL/Algebra/abstract/RingHomo.thy Mon Mar 25 19:53:44 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,64 +0,0 @@
-(* Author: Clemens Ballarin, started 15 April 1997
-
-Ring homomorphism.
-*)
-
-header {* Ring homomorphism *}
-
-theory RingHomo
-imports Ring2
-begin
-
-definition
- homo :: "('a::ring => 'b::ring) => bool" where
- "homo f \ (ALL a b. f (a + b) = f a + f b &
- f (a * b) = f a * f b) &
- f 1 = 1"
-
-
-lemma homoI:
- "!! f. [| !! a b. f (a + b) = f a + f b; !! a b. f (a * b) = f a * f b;
- f 1 = 1 |] ==> homo f"
- unfolding homo_def by blast
-
-lemma homo_add [simp]: "!! f. homo f ==> f (a + b) = f a + f b"
- unfolding homo_def by blast
-
-lemma homo_mult [simp]: "!! f. homo f ==> f (a * b) = f a * f b"
- unfolding homo_def by blast
-
-lemma homo_one [simp]: "!! f. homo f ==> f 1 = 1"
- unfolding homo_def by blast
-
-lemma homo_zero [simp]: "!! f::('a::ring=>'b::ring). homo f ==> f 0 = 0"
- apply (rule_tac a = "f 0" in a_lcancel)
- apply (simp (no_asm_simp) add: homo_add [symmetric])
- done
-
-lemma homo_uminus [simp]:
- "!! f::('a::ring=>'b::ring). homo f ==> f (-a) = - f a"
- apply (rule_tac a = "f a" in a_lcancel)
- apply (frule homo_zero)
- apply (simp (no_asm_simp) add: homo_add [symmetric])
- done
-
-lemma homo_power [simp]: "!! f::('a::ring=>'b::ring). homo f ==> f (a ^ n) = f a ^ n"
- apply (induct_tac n)
- apply (drule homo_one)
- apply simp
- apply (drule_tac a = "a^n" and b = "a" in homo_mult)
- apply simp
- done
-
-lemma homo_SUM [simp]:
- "!! f::('a::ring=>'b::ring).
- homo f ==> f (setsum g {..n::nat}) = setsum (f o g) {..n}"
- apply (induct_tac n)
- apply simp
- apply simp
- done
-
-lemma id_homo [simp]: "homo (%x. x)"
- by (blast intro!: homoI)
-
-end
diff -r 237190475d79 -r 7957d26c3334 src/HOL/Algebra/poly/LongDiv.thy
--- a/src/HOL/Algebra/poly/LongDiv.thy Mon Mar 25 19:53:44 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,257 +0,0 @@
-(* Author: Clemens Ballarin, started 23 June 1999
-
-Experimental theory: long division of polynomials.
-*)
-
-theory LongDiv
-imports PolyHomo
-begin
-
-definition
- lcoeff :: "'a::ring up => 'a" where
- "lcoeff p = coeff p (deg p)"
-
-definition
- eucl_size :: "'a::zero up => nat" where
- "eucl_size p = (if p = 0 then 0 else deg p + 1)"
-
-lemma SUM_shrink_below_lemma:
- "!! f::(nat=>'a::ring). (ALL i. i < m --> f i = 0) -->
- setsum (%i. f (i+m)) {..d} = setsum f {..m+d}"
- apply (induct_tac d)
- apply (induct_tac m)
- apply simp
- apply force
- apply (simp add: add_commute [of m])
- done
-
-lemma SUM_extend_below:
- "!! f::(nat=>'a::ring).
- [| m <= n; !!i. i < m ==> f i = 0; P (setsum (%i. f (i+m)) {..n-m}) |]
- ==> P (setsum f {..n})"
- by (simp add: SUM_shrink_below_lemma add_diff_inverse leD)
-
-lemma up_repr2D:
- "!! p::'a::ring up.
- [| deg p <= n; P (setsum (%i. monom (coeff p i) i) {..n}) |]
- ==> P p"
- by (simp add: up_repr_le)
-
-
-(* Start of LongDiv *)
-
-lemma deg_lcoeff_cancel:
- "!!p::('a::ring up).
- [| deg p <= deg r; deg q <= deg r;
- coeff p (deg r) = - (coeff q (deg r)); deg r ~= 0 |] ==>
- deg (p + q) < deg r"
- apply (rule le_less_trans [of _ "deg r - 1"])
- prefer 2
- apply arith
- apply (rule deg_aboveI)
- apply (case_tac "deg r = m")
- apply clarify
- apply simp
- (* case "deg q ~= m" *)
- apply (subgoal_tac "deg p < m & deg q < m")
- apply (simp (no_asm_simp) add: deg_aboveD)
- apply arith
- done
-
-lemma deg_lcoeff_cancel2:
- "!!p::('a::ring up).
- [| deg p <= deg r; deg q <= deg r;
- p ~= -q; coeff p (deg r) = - (coeff q (deg r)) |] ==>
- deg (p + q) < deg r"
- apply (rule deg_lcoeff_cancel)
- apply assumption+
- apply (rule classical)
- apply clarify
- apply (erule notE)
- apply (rule_tac p = p in up_repr2D, assumption)
- apply (rule_tac p = q in up_repr2D, assumption)
- apply (rotate_tac -1)
- apply (simp add: smult_l_minus)
- done
-
-lemma long_div_eucl_size:
- "!!g::('a::ring up). g ~= 0 ==>
- Ex (% (q, r, k).
- (lcoeff g)^k *s f = q * g + r & (eucl_size r < eucl_size g))"
- 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)
- (* TO DO: replace by measure_induct *)
- apply (rule_tac f = eucl_size in wf_measure)
- apply (case_tac "eucl_size x < eucl_size g")
- apply (rule_tac x = "(0, x, 0)" in exI)
- apply (simp (no_asm_simp))
- (* case "eucl_size x >= eucl_size g" *)
- apply (drule_tac x = "lcoeff g *s x - (monom (lcoeff x) (deg x - deg g)) * g" in spec)
- apply (erule impE)
- apply (simp (no_asm_use) add: inv_image_def measure_def lcoeff_def)
- apply (case_tac "x = 0")
- apply (rotate_tac -1)
- apply (simp add: eucl_size_def)
- (* case "x ~= 0 *)
- apply (rotate_tac -1)
- apply (simp add: eucl_size_def)
- apply (rule impI)
- apply (rule deg_lcoeff_cancel2)
- (* replace by linear arithmetic??? *)
- apply (rule_tac [2] le_trans)
- apply (rule_tac [2] deg_smult_ring)
- prefer 2
- apply simp
- apply (simp (no_asm))
- apply (rule le_trans)
- apply (rule deg_mult_ring)
- apply (rule le_trans)
-(**)
- apply (rule add_le_mono)
- apply (rule le_refl)
- (* term order forces to use this instead of add_le_mono1 *)
- apply (rule deg_monom_ring)
- apply (simp (no_asm_simp))
- apply force
- apply (simp (no_asm))
-(**)
- (* This change is probably caused by application of commutativity *)
- apply (rule_tac m = "deg g" and n = "deg x" in SUM_extend)
- apply (simp (no_asm))
- apply (simp (no_asm_simp))
- apply arith
- apply (rule_tac m = "deg g" and n = "deg g" in SUM_extend_below)
- apply (rule le_refl)
- apply (simp (no_asm_simp))
- apply arith
- apply (simp (no_asm))
-(**)
-(* end of subproof deg f1 < deg f *)
- apply (erule exE)
- 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)
- apply clarify
- apply (drule sym)
- using [[simproc del: ring]]
- apply (simp (no_asm_use) add: l_distr a_assoc)
- apply (simp (no_asm_simp))
- apply (simp (no_asm_use) add: minus_def smult_r_distr smult_r_minus
- monom_mult_smult smult_assoc2)
- using [[simproc ring]]
- apply (simp add: smult_assoc1 [symmetric])
- done
-
-lemma long_div_ring_aux:
- "(g :: 'a::ring up) ~= 0 ==>
- Ex (\(q, r, k). lcoeff g ^ k *s f = q * g + r \
- (if r = 0 then 0 else deg r + 1) < (if g = 0 then 0 else deg g + 1))"
-proof -
- note [[simproc del: ring]]
- assume "g ~= 0"
- then show ?thesis
- by (rule long_div_eucl_size [simplified eucl_size_def])
-qed
-
-lemma long_div_ring:
- "!!g::('a::ring up). g ~= 0 ==>
- Ex (% (q, r, k).
- (lcoeff g)^k *s f = q * g + r & (r = 0 | deg r < deg g))"
- apply (frule_tac f = f in long_div_ring_aux)
- using [[simproc del: ring]]
- apply auto
- apply (case_tac "aa = 0")
- apply blast
- (* case "aa ~= 0 *)
- apply (rotate_tac -1)
- apply auto
- done
-
-(* Next one fails *)
-lemma long_div_unit:
- "!!g::('a::ring up). [| g ~= 0; (lcoeff g) dvd 1 |] ==>
- Ex (% (q, r). f = q * g + r & (r = 0 | deg r < deg g))"
- apply (frule_tac f = "f" in long_div_ring)
- apply (erule exE)
- 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)
- apply clarify
- apply (rule conjI)
- apply (drule sym)
- using [[simproc del: ring]]
- apply (simp (no_asm_simp) add: smult_r_distr [symmetric] smult_assoc2)
- using [[simproc ring]]
- apply (simp (no_asm_simp) add: l_inverse_ring unit_power smult_assoc1 [symmetric])
- (* degree property *)
- apply (erule disjE)
- apply (simp (no_asm_simp))
- apply (rule disjI2)
- apply (rule le_less_trans)
- apply (rule deg_smult_ring)
- apply (simp (no_asm_simp))
- done
-
-lemma long_div_theorem:
- "!!g::('a::field up). g ~= 0 ==>
- Ex (% (q, r). f = q * g + r & (r = 0 | deg r < deg g))"
- apply (rule long_div_unit)
- apply assumption
- apply (simp (no_asm_simp) add: lcoeff_def lcoeff_nonzero field_ax)
- done
-
-lemma uminus_zero: "- (0::'a::ring) = 0"
- by simp
-
-lemma diff_zero_imp_eq: "!!a::'a::ring. a - b = 0 ==> a = b"
- apply (rule_tac s = "a - (a - b) " in trans)
- apply simp
- apply (simp (no_asm))
- done
-
-lemma eq_imp_diff_zero: "!!a::'a::ring. a = b ==> a + (-b) = 0"
- by simp
-
-lemma long_div_quo_unique:
- "!!g::('a::field up). [| g ~= 0;
- f = q1 * g + r1; (r1 = 0 | deg r1 < deg g);
- f = q2 * g + r2; (r2 = 0 | deg r2 < deg g) |] ==> q1 = q2"
- apply (subgoal_tac "(q1 - q2) * g = r2 - r1") (* 1 *)
- apply (erule_tac V = "f = ?x" in thin_rl)
- apply (erule_tac V = "f = ?x" in thin_rl)
- apply (rule diff_zero_imp_eq)
- apply (rule classical)
- apply (erule disjE)
- (* r1 = 0 *)
- apply (erule disjE)
- (* r2 = 0 *)
- using [[simproc del: ring]]
- apply (simp add: integral_iff minus_def l_zero uminus_zero)
- (* r2 ~= 0 *)
- apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong)
- apply (simp add: minus_def l_zero uminus_zero)
- (* r1 ~=0 *)
- apply (erule disjE)
- (* r2 = 0 *)
- apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong)
- apply (simp add: minus_def l_zero uminus_zero)
- (* r2 ~= 0 *)
- apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong)
- apply (simp add: minus_def)
- apply (drule order_eq_refl [THEN add_leD2])
- apply (drule leD)
- apply (erule notE, rule deg_add [THEN le_less_trans])
- apply (simp (no_asm_simp))
- (* proof of 1 *)
- apply (rule diff_zero_imp_eq)
- apply hypsubst
- apply (drule_tac a = "?x+?y" in eq_imp_diff_zero)
- using [[simproc ring]]
- apply simp
- done
-
-lemma long_div_rem_unique:
- "!!g::('a::field up). [| g ~= 0;
- f = q1 * g + r1; (r1 = 0 | deg r1 < deg g);
- f = q2 * g + r2; (r2 = 0 | deg r2 < deg g) |] ==> r1 = r2"
- apply (subgoal_tac "q1 = q2")
- apply (metis a_comm a_lcancel m_comm)
- apply (metis a_comm l_zero long_div_quo_unique m_comm conc)
- done
-
-end
diff -r 237190475d79 -r 7957d26c3334 src/HOL/Algebra/poly/PolyHomo.thy
--- a/src/HOL/Algebra/poly/PolyHomo.thy Mon Mar 25 19:53:44 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,187 +0,0 @@
-(* Author: Clemens Ballarin, started 15 April 1997
-
-Universal property and evaluation homomorphism of univariate polynomials.
-*)
-
-theory PolyHomo
-imports UnivPoly2
-begin
-
-definition
- EVAL2 :: "['a::ring => 'b, 'b, 'a up] => 'b::ring" where
- "EVAL2 phi a p = setsum (%i. phi (coeff p i) * a ^ i) {..deg p}"
-
-definition
- EVAL :: "['a::ring, 'a up] => 'a" where
- "EVAL = EVAL2 (%x. x)"
-
-lemma SUM_shrink_lemma:
- "!! f::(nat=>'a::ring).
- m <= n & (ALL i. m < i & i <= n --> f i = 0) -->
- setsum f {..m} = setsum f {..n}"
- apply (induct_tac n)
- (* Base case *)
- apply (simp (no_asm))
- (* Induction step *)
- apply (case_tac "m <= n")
- apply auto
- apply (subgoal_tac "m = Suc n")
- apply (simp (no_asm_simp))
- apply arith
- done
-
-lemma SUM_shrink:
- "!! f::(nat=>'a::ring).
- [| m <= n; !!i. [| m < i; i <= n |] ==> f i = 0; P (setsum f {..n}) |]
- ==> P (setsum f {..m})"
- apply (cut_tac m = m and n = n and f = f in SUM_shrink_lemma)
- apply simp
- done
-
-lemma SUM_extend:
- "!! f::(nat=>'a::ring).
- [| m <= n; !!i. [| m < i; i <= n |] ==> f i = 0; P (setsum f {..m}) |]
- ==> P (setsum f {..n})"
- apply (cut_tac m = m and n = n and f = f in SUM_shrink_lemma)
- apply simp
- done
-
-lemma DiagSum_lemma:
- "!!f::nat=>'a::ring. j <= n + m -->
- setsum (%k. setsum (%i. f i * g (k - i)) {..k}) {..j} =
- setsum (%k. setsum (%i. f k * g i) {..j - k}) {..j}"
- apply (induct_tac j)
- (* Base case *)
- apply (simp (no_asm))
- (* Induction step *)
- apply (simp (no_asm) add: Suc_diff_le natsum_add)
- apply (simp (no_asm_simp))
- done
-
-lemma DiagSum:
- "!!f::nat=>'a::ring.
- setsum (%k. setsum (%i. f i * g (k - i)) {..k}) {..n + m} =
- setsum (%k. setsum (%i. f k * g i) {..n + m - k}) {..n + m}"
- apply (rule DiagSum_lemma [THEN mp])
- apply (rule le_refl)
- done
-
-lemma CauchySum:
- "!! f::nat=>'a::ring. [| bound n f; bound m g|] ==>
- setsum (%k. setsum (%i. f i * g (k-i)) {..k}) {..n + m} =
- setsum f {..n} * setsum g {..m}"
- apply (simp (no_asm) add: natsum_ldistr DiagSum)
- (* SUM_rdistr must be applied after SUM_ldistr ! *)
- apply (simp (no_asm) add: natsum_rdistr)
- apply (rule_tac m = n and n = "n + m" in SUM_extend)
- apply (rule le_add1)
- apply force
- apply (rule natsum_cong)
- apply (rule refl)
- apply (rule_tac m = m and n = "n +m - i" in SUM_shrink)
- apply (simp (no_asm_simp) add: le_add_diff)
- apply auto
- done
-
-(* Evaluation homomorphism *)
-
-lemma EVAL2_homo:
- "!! phi::('a::ring=>'b::ring). homo phi ==> homo (EVAL2 phi a)"
- apply (rule homoI)
- apply (unfold EVAL2_def)
- (* + commutes *)
- (* degree estimations:
- bound of all sums can be extended to max (deg aa) (deg b) *)
- apply (rule_tac m = "deg (aa + b) " and n = "max (deg aa) (deg b)" in SUM_shrink)
- apply (rule deg_add)
- apply (simp (no_asm_simp) del: coeff_add add: deg_aboveD)
- apply (rule_tac m = "deg aa" and n = "max (deg aa) (deg b)" in SUM_shrink)
- apply (rule le_maxI1)
- apply (simp (no_asm_simp) add: deg_aboveD)
- apply (rule_tac m = "deg b" and n = "max (deg aa) (deg b) " in SUM_shrink)
- apply (rule le_maxI2)
- apply (simp (no_asm_simp) add: deg_aboveD)
- (* actual homom property + *)
- apply (simp (no_asm_simp) add: l_distr natsum_add)
-
- (* * commutes *)
- apply (rule_tac m = "deg (aa * b) " and n = "deg aa + deg b" in SUM_shrink)
- apply (rule deg_mult_ring)
- apply (simp (no_asm_simp) del: coeff_mult add: deg_aboveD)
- apply (rule trans)
- apply (rule_tac [2] CauchySum)
- prefer 2
- apply (simp add: boundI deg_aboveD)
- prefer 2
- apply (simp add: boundI deg_aboveD)
- (* getting a^i and a^(k-i) together is difficult, so we do it manually *)
- 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)
- apply (simp (no_asm_simp) add: power_mult leD [THEN add_diff_inverse] natsum_ldistr)
- apply (simp (no_asm))
- (* 1 commutes *)
- apply (simp (no_asm_simp))
- done
-
-lemma EVAL2_const:
- "!!phi::'a::ring=>'b::ring. EVAL2 phi a (monom b 0) = phi b"
- by (simp add: EVAL2_def)
-
-lemma EVAL2_monom1:
- "!! phi::'a::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom 1 1) = a"
- by (simp add: EVAL2_def)
- (* Must be able to distinguish 0 from 1, hence 'a::domain *)
-
-lemma EVAL2_monom:
- "!! phi::'a::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom 1 n) = a ^ n"
- apply (unfold EVAL2_def)
- apply (simp (no_asm))
- apply (case_tac n)
- apply auto
- done
-
-lemma EVAL2_smult:
- "!!phi::'a::ring=>'b::ring.
- homo phi ==> EVAL2 phi a (b *s p) = phi b * EVAL2 phi a p"
- by (simp (no_asm_simp) add: monom_mult_is_smult [symmetric] EVAL2_homo EVAL2_const)
-
-lemma monom_decomp: "monom (a::'a::ring) n = monom a 0 * monom 1 n"
- apply (simp (no_asm) add: monom_mult_is_smult)
- apply (rule up_eqI)
- apply (simp (no_asm))
- done
-
-lemma EVAL2_monom_n:
- "!! phi::'a::domain=>'b::ring.
- homo phi ==> EVAL2 phi a (monom b n) = phi b * a ^ n"
- apply (subst monom_decomp)
- apply (simp (no_asm_simp) add: EVAL2_homo EVAL2_const EVAL2_monom)
- done
-
-lemma EVAL_homo: "!!a::'a::ring. homo (EVAL a)"
- by (simp add: EVAL_def EVAL2_homo)
-
-lemma EVAL_const: "!!a::'a::ring. EVAL a (monom b 0) = b"
- by (simp add: EVAL_def EVAL2_const)
-
-lemma EVAL_monom: "!!a::'a::domain. EVAL a (monom 1 n) = a ^ n"
- by (simp add: EVAL_def EVAL2_monom)
-
-lemma EVAL_smult: "!!a::'a::ring. EVAL a (b *s p) = b * EVAL a p"
- by (simp add: EVAL_def EVAL2_smult)
-
-lemma EVAL_monom_n: "!!a::'a::domain. EVAL a (monom b n) = b * a ^ n"
- by (simp add: EVAL_def EVAL2_monom_n)
-
-
-(* Examples *)
-
-lemma "EVAL (x::'a::domain) (a*X^2 + b*X^1 + c*X^0) = a * x ^ 2 + b * x ^ 1 + c"
- by (simp del: power_Suc add: EVAL_homo EVAL_monom EVAL_monom_n)
-
-lemma
- "EVAL (y::'a::domain)
- (EVAL (monom x 0) (monom 1 1 + monom (a*X^2 + b*X^1 + c*X^0) 0)) =
- x ^ 1 + (a * y ^ 2 + b * y ^ 1 + c)"
- by (simp del: add: EVAL_homo EVAL_monom EVAL_monom_n EVAL_const)
-
-end
diff -r 237190475d79 -r 7957d26c3334 src/HOL/Algebra/poly/Polynomial.thy
--- a/src/HOL/Algebra/poly/Polynomial.thy Mon Mar 25 19:53:44 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-(* Author: Clemens Ballarin, started 17 July 1997
-
-Summary theory of the development of (not instantiated) polynomials.
-*)
-
-theory Polynomial
-imports LongDiv
-begin
-
-end
diff -r 237190475d79 -r 7957d26c3334 src/HOL/Algebra/poly/UnivPoly2.thy
--- a/src/HOL/Algebra/poly/UnivPoly2.thy Mon Mar 25 19:53:44 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,810 +0,0 @@
-(* Title: HOL/Algebra/poly/UnivPoly2.thy
- Author: Clemens Ballarin, started 9 December 1996
- Copyright: Clemens Ballarin
-*)
-
-header {* Univariate Polynomials *}
-
-theory UnivPoly2
-imports "../abstract/Abstract"
-begin
-
-(* With this variant of setsum_cong, assumptions
- like i:{m..n} get simplified (to m <= i & i <= n). *)
-
-declare strong_setsum_cong [cong]
-
-
-section {* Definition of type up *}
-
-definition
- bound :: "[nat, nat => 'a::zero] => bool" where
- "bound n f = (ALL i. n < i --> f i = 0)"
-
-lemma boundI [intro!]: "[| !! m. n < m ==> f m = 0 |] ==> bound n f"
- unfolding bound_def by blast
-
-lemma boundE [elim?]: "[| bound n f; (!! m. n < m ==> f m = 0) ==> P |] ==> P"
- unfolding bound_def by blast
-
-lemma boundD [dest]: "[| bound n f; n < m |] ==> f m = 0"
- unfolding bound_def by blast
-
-lemma bound_below:
- assumes bound: "bound m f" and nonzero: "f n ~= 0" shows "n <= m"
-proof (rule classical)
- assume "~ ?thesis"
- then have "m < n" by arith
- with bound have "f n = 0" ..
- with nonzero show ?thesis by contradiction
-qed
-
-
-definition "UP = {f :: nat => 'a::zero. EX n. bound n f}"
-
-typedef 'a up = "UP :: (nat => 'a::zero) set"
- morphisms Rep_UP Abs_UP
-proof -
- have "bound 0 (\_. 0::'a)" by (rule boundI) (rule refl)
- then show ?thesis unfolding UP_def by blast
-qed
-
-
-section {* Constants *}
-
-definition
- coeff :: "['a up, nat] => ('a::zero)"
- where "coeff p n = Rep_UP p n"
-
-definition
- monom :: "['a::zero, nat] => 'a up" ("(3_*X^/_)" [71, 71] 70)
- where "monom a n = Abs_UP (%i. if i=n then a else 0)"
-
-definition
- smult :: "['a::{zero, times}, 'a up] => 'a up" (infixl "*s" 70)
- where "a *s p = Abs_UP (%i. a * Rep_UP p i)"
-
-lemma coeff_bound_ex: "EX n. bound n (coeff p)"
-proof -
- have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
- then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
- then show ?thesis ..
-qed
-
-lemma bound_coeff_obtain:
- assumes prem: "(!!n. bound n (coeff p) ==> P)" shows "P"
-proof -
- have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
- then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
- with prem show P .
-qed
-
-
-text {* Ring operations *}
-
-instantiation up :: (zero) zero
-begin
-
-definition
- up_zero_def: "0 = monom 0 0"
-
-instance ..
-
-end
-
-instantiation up :: ("{one, zero}") one
-begin
-
-definition
- up_one_def: "1 = monom 1 0"
-
-instance ..
-
-end
-
-instantiation up :: ("{plus, zero}") plus
-begin
-
-definition
- up_add_def: "p + q = Abs_UP (%n. Rep_UP p n + Rep_UP q n)"
-
-instance ..
-
-end
-
-instantiation up :: ("{one, times, uminus, zero}") uminus
-begin
-
-definition
- (* note: - 1 is different from -1; latter is of class number *)
- up_uminus_def:"- p = (- 1) *s p"
- (* easier to use than "Abs_UP (%i. - Rep_UP p i)" *)
-
-instance ..
-
-end
-
-instantiation up :: ("{one, plus, times, minus, uminus, zero}") minus
-begin
-
-definition
- up_minus_def: "(a :: 'a up) - b = a + (-b)"
-
-instance ..
-
-end
-
-instantiation up :: ("{times, comm_monoid_add}") times
-begin
-
-definition
- up_mult_def: "p * q = Abs_UP (%n::nat. setsum
- (%i. Rep_UP p i * Rep_UP q (n-i)) {..n})"
-
-instance ..
-
-end
-
-instance up :: ("{times, comm_monoid_add}") Rings.dvd ..
-
-instantiation up :: ("{times, one, comm_monoid_add, uminus, minus}") inverse
-begin
-
-definition
- up_inverse_def: "inverse (a :: 'a up) = (if a dvd 1 then
- THE x. a * x = 1 else 0)"
-
-definition
- up_divide_def: "(a :: 'a up) / b = a * inverse b"
-
-instance ..
-
-end
-
-
-subsection {* Effect of operations on coefficients *}
-
-lemma coeff_monom [simp]: "coeff (monom a m) n = (if m=n then a else 0)"
-proof -
- have "(%n. if n = m then a else 0) : UP"
- using UP_def by force
- from this show ?thesis
- by (simp add: coeff_def monom_def Abs_UP_inverse Rep_UP)
-qed
-
-lemma coeff_zero [simp]: "coeff 0 n = 0"
-proof (unfold up_zero_def)
-qed simp
-
-lemma coeff_one [simp]: "coeff 1 n = (if n=0 then 1 else 0)"
-proof (unfold up_one_def)
-qed simp
-
-(* term order
-lemma coeff_smult [simp]: "coeff (a *s p) n = (a::'a::ring) * coeff p n"
-proof -
- have "!!f. f : UP ==> (%n. a * f n) : UP"
- by (unfold UP_def) (force simp add: algebra_simps)
-*) (* this force step is slow *)
-(* then show ?thesis
- apply (simp add: coeff_def smult_def Abs_UP_inverse Rep_UP)
-qed
-*)
-lemma coeff_smult [simp]: "coeff (a *s p) n = (a::'a::ring) * coeff p n"
-proof -
- have "Rep_UP p : UP ==> (%n. a * Rep_UP p n) : UP"
- by (unfold UP_def) (force simp add: algebra_simps)
- (* this force step is slow *)
- then show ?thesis
- by (simp add: coeff_def smult_def Abs_UP_inverse Rep_UP)
-qed
-
-lemma coeff_add [simp]: "coeff (p+q) n = (coeff p n + coeff q n::'a::ring)"
-proof -
- {
- fix f g
- assume fup: "(f::nat=>'a::ring) : UP" and gup: "(g::nat=>'a::ring) : UP"
- have "(%i. f i + g i) : UP"
- proof -
- from fup obtain n where boundn: "bound n f"
- by (unfold UP_def) fast
- from gup obtain m where boundm: "bound m g"
- by (unfold UP_def) fast
- have "bound (max n m) (%i. (f i + g i))"
- proof
- fix i
- assume "max n m < i"
- with boundn and boundm show "f i + g i = 0"
- by (fastforce simp add: algebra_simps)
- qed
- then show "(%i. (f i + g i)) : UP"
- by (unfold UP_def) fast
- qed
- }
- then show ?thesis
- by (simp add: coeff_def up_add_def Abs_UP_inverse Rep_UP)
-qed
-
-lemma coeff_mult [simp]:
- "coeff (p * q) n = (setsum (%i. coeff p i * coeff q (n-i)) {..n}::'a::ring)"
-proof -
- {
- fix f g
- assume fup: "(f::nat=>'a::ring) : UP" and gup: "(g::nat=>'a::ring) : UP"
- have "(%n. setsum (%i. f i * g (n-i)) {..n}) : UP"
- proof -
- from fup obtain n where "bound n f"
- by (unfold UP_def) fast
- from gup obtain m where "bound m g"
- by (unfold UP_def) fast
- have "bound (n + m) (%n. setsum (%i. f i * g (n-i)) {..n})"
- proof
- fix k
- assume bound: "n + m < k"
- {
- fix i
- have "f i * g (k-i) = 0"
- proof cases
- assume "n < i"
- with `bound n f` show ?thesis by (auto simp add: algebra_simps)
- next
- assume "~ (n < i)"
- with bound have "m < k-i" by arith
- with `bound m g` show ?thesis by (auto simp add: algebra_simps)
- qed
- }
- then show "setsum (%i. f i * g (k-i)) {..k} = 0"
- by (simp add: algebra_simps)
- qed
- then show "(%n. setsum (%i. f i * g (n-i)) {..n}) : UP"
- by (unfold UP_def) fast
- qed
- }
- then show ?thesis
- by (simp add: coeff_def up_mult_def Abs_UP_inverse Rep_UP)
-qed
-
-lemma coeff_uminus [simp]: "coeff (-p) n = (-coeff p n::'a::ring)"
-by (unfold up_uminus_def) (simp add: algebra_simps)
-
-(* Other lemmas *)
-
-lemma up_eqI: assumes prem: "(!! n. coeff p n = coeff q n)" shows "p = q"
-proof -
- have "p = Abs_UP (%u. Rep_UP p u)" by (simp add: Rep_UP_inverse)
- also from prem have "... = Abs_UP (Rep_UP q)" by (simp only: coeff_def)
- also have "... = q" by (simp add: Rep_UP_inverse)
- finally show ?thesis .
-qed
-
-instance up :: (ring) ring
-proof
- fix p q r :: "'a::ring up"
- show "(p + q) + r = p + (q + r)"
- by (rule up_eqI) simp
- show "0 + p = p"
- by (rule up_eqI) simp
- show "(-p) + p = 0"
- by (rule up_eqI) simp
- show "p + q = q + p"
- by (rule up_eqI) simp
- show "(p * q) * r = p * (q * r)"
- proof (rule up_eqI)
- fix n
- {
- fix k and a b c :: "nat=>'a::ring"
- have "k <= n ==>
- setsum (%j. setsum (%i. a i * b (j-i)) {..j} * c (n-j)) {..k} =
- setsum (%j. a j * setsum (%i. b i * c (n-j-i)) {..k-j}) {..k}"
- (is "_ ==> ?eq k")
- proof (induct k)
- case 0 show ?case by simp
- next
- case (Suc k)
- then have "k <= n" by arith
- then have "?eq k" by (rule Suc)
- then show ?case
- by (simp add: Suc_diff_le natsum_ldistr)
- qed
- }
- then show "coeff ((p * q) * r) n = coeff (p * (q * r)) n"
- by simp
- qed
- show "1 * p = p"
- proof (rule up_eqI)
- fix n
- show "coeff (1 * p) n = coeff p n"
- proof (cases n)
- case 0 then show ?thesis by simp
- next
- case Suc then show ?thesis by (simp del: setsum_atMost_Suc add: natsum_Suc2)
- qed
- qed
- show "(p + q) * r = p * r + q * r"
- by (rule up_eqI) simp
- show "\q. p * q = q * p"
- proof (rule up_eqI)
- fix q
- fix n
- {
- fix k
- fix a b :: "nat=>'a::ring"
- have "k <= n ==>
- setsum (%i. a i * b (n-i)) {..k} =
- setsum (%i. a (k-i) * b (i+n-k)) {..k}"
- (is "_ ==> ?eq k")
- proof (induct k)
- case 0 show ?case by simp
- next
- case (Suc k) then show ?case by (subst natsum_Suc2) simp
- qed
- }
- then show "coeff (p * q) n = coeff (q * p) n"
- by simp
- qed
-
- show "p - q = p + (-q)"
- by (simp add: up_minus_def)
- show "inverse p = (if p dvd 1 then THE x. p*x = 1 else 0)"
- by (simp add: up_inverse_def)
- show "p / q = p * inverse q"
- by (simp add: up_divide_def)
-qed
-
-(* Further properties of monom *)
-
-lemma monom_zero [simp]:
- "monom 0 n = 0"
- by (simp add: monom_def up_zero_def)
-(* term order: application of coeff_mult goes wrong: rule not symmetric
-lemma monom_mult_is_smult:
- "monom (a::'a::ring) 0 * p = a *s p"
-proof (rule up_eqI)
- fix k
- show "coeff (monom a 0 * p) k = coeff (a *s p) k"
- proof (cases k)
- case 0 then show ?thesis by simp
- next
- case Suc then show ?thesis by simp
- qed
-qed
-*)
-
-lemma monom_mult_is_smult:
- "monom (a::'a::ring) 0 * p = a *s p"
-proof (rule up_eqI)
- note [[simproc del: ring]]
- fix k
- have "coeff (p * monom a 0) k = coeff (a *s p) k"
- proof (cases k)
- case 0 then show ?thesis by simp ring
- next
- case Suc then show ?thesis by simp (ring, simp)
- qed
- then show "coeff (monom a 0 * p) k = coeff (a *s p) k" by ring
-qed
-
-lemma monom_add [simp]:
- "monom (a + b) n = monom (a::'a::ring) n + monom b n"
-by (rule up_eqI) simp
-
-lemma monom_mult_smult:
- "monom (a * b) n = a *s monom (b::'a::ring) n"
-by (rule up_eqI) simp
-
-lemma monom_uminus [simp]:
- "monom (-a) n = - monom (a::'a::ring) n"
-by (rule up_eqI) simp
-
-lemma monom_one [simp]:
- "monom 1 0 = 1"
-by (simp add: up_one_def)
-
-lemma monom_inj:
- "(monom a n = monom b n) = (a = b)"
-proof
- assume "monom a n = monom b n"
- then have "coeff (monom a n) n = coeff (monom b n) n" by simp
- then show "a = b" by simp
-next
- assume "a = b" then show "monom a n = monom b n" by simp
-qed
-
-(* Properties of *s:
- Polynomials form a module *)
-
-lemma smult_l_distr:
- "(a + b::'a::ring) *s p = a *s p + b *s p"
-by (rule up_eqI) simp
-
-lemma smult_r_distr:
- "(a::'a::ring) *s (p + q) = a *s p + a *s q"
-by (rule up_eqI) simp
-
-lemma smult_assoc1:
- "(a * b::'a::ring) *s p = a *s (b *s p)"
-by (rule up_eqI) simp
-
-lemma smult_one [simp]:
- "(1::'a::ring) *s p = p"
-by (rule up_eqI) simp
-
-(* Polynomials form an algebra *)
-
-lemma smult_assoc2:
- "(a *s p) * q = (a::'a::ring) *s (p * q)"
-using [[simproc del: ring]]
-by (rule up_eqI) (simp add: natsum_rdistr m_assoc)
-
-(* the following can be derived from the above ones,
- for generality reasons, it is therefore done *)
-
-lemma smult_l_null [simp]:
- "(0::'a::ring) *s p = 0"
-proof -
- fix a
- have "0 *s p = (0 *s p + a *s p) + - (a *s p)" by simp
- also have "... = (0 + a) *s p + - (a *s p)" by (simp only: smult_l_distr)
- also have "... = 0" by simp
- finally show ?thesis .
-qed
-
-lemma smult_r_null [simp]:
- "(a::'a::ring) *s 0 = 0"
-proof -
- fix p
- have "a *s 0 = (a *s 0 + a *s p) + - (a *s p)" by simp
- also have "... = a *s (0 + p) + - (a *s p)" by (simp only: smult_r_distr)
- also have "... = 0" by simp
- finally show ?thesis .
-qed
-
-lemma smult_l_minus:
- "(-a::'a::ring) *s p = - (a *s p)"
-proof -
- have "(-a) *s p = (-a *s p + a *s p) + -(a *s p)" by simp
- also have "... = (-a + a) *s p + -(a *s p)" by (simp only: smult_l_distr)
- also have "... = -(a *s p)" by simp
- finally show ?thesis .
-qed
-
-lemma smult_r_minus:
- "(a::'a::ring) *s (-p) = - (a *s p)"
-proof -
- have "a *s (-p) = (a *s -p + a *s p) + -(a *s p)" by simp
- also have "... = a *s (-p + p) + -(a *s p)" by (simp only: smult_r_distr)
- also have "... = -(a *s p)" by simp
- finally show ?thesis .
-qed
-
-
-section {* The degree function *}
-
-definition
- deg :: "('a::zero) up => nat"
- where "deg p = (LEAST n. bound n (coeff p))"
-
-lemma deg_aboveI:
- "(!!m. n < m ==> coeff p m = 0) ==> deg p <= n"
-by (unfold deg_def) (fast intro: Least_le)
-
-lemma deg_aboveD:
- assumes "deg p < m" shows "coeff p m = 0"
-proof -
- obtain n where "bound n (coeff p)" by (rule bound_coeff_obtain)
- then have "bound (deg p) (coeff p)" by (unfold deg_def, rule LeastI)
- then show "coeff p m = 0" using `deg p < m` by (rule boundD)
-qed
-
-lemma deg_belowI:
- assumes prem: "n ~= 0 ==> coeff p n ~= 0" shows "n <= deg p"
-(* logically, this is a slightly stronger version of deg_aboveD *)
-proof (cases "n=0")
- case True then show ?thesis by simp
-next
- case False then have "coeff p n ~= 0" by (rule prem)
- then have "~ deg p < n" by (fast dest: deg_aboveD)
- then show ?thesis by arith
-qed
-
-lemma lcoeff_nonzero_deg:
- assumes deg: "deg p ~= 0" shows "coeff p (deg p) ~= 0"
-proof -
- obtain m where "deg p <= m" and m_coeff: "coeff p m ~= 0"
- proof -
- have minus: "!!(n::nat) m. n ~= 0 ==> (n - Suc 0 < m) = (n <= m)"
- by arith (* make public?, why does proof not work with "1" *)
- from deg have "deg p - 1 < (LEAST n. bound n (coeff p))"
- by (unfold deg_def) arith
- then have "~ bound (deg p - 1) (coeff p)" by (rule not_less_Least)
- then have "EX m. deg p - 1 < m & coeff p m ~= 0"
- by (unfold bound_def) fast
- then have "EX m. deg p <= m & coeff p m ~= 0" by (simp add: deg minus)
- then show ?thesis by (auto intro: that)
- qed
- with deg_belowI have "deg p = m" by fastforce
- with m_coeff show ?thesis by simp
-qed
-
-lemma lcoeff_nonzero_nonzero:
- assumes deg: "deg p = 0" and nonzero: "p ~= 0" shows "coeff p 0 ~= 0"
-proof -
- have "EX m. coeff p m ~= 0"
- proof (rule classical)
- assume "~ ?thesis"
- then have "p = 0" by (auto intro: up_eqI)
- with nonzero show ?thesis by contradiction
- qed
- then obtain m where coeff: "coeff p m ~= 0" ..
- then have "m <= deg p" by (rule deg_belowI)
- then have "m = 0" by (simp add: deg)
- with coeff show ?thesis by simp
-qed
-
-lemma lcoeff_nonzero:
- "p ~= 0 ==> coeff p (deg p) ~= 0"
-proof (cases "deg p = 0")
- case True
- assume "p ~= 0"
- with True show ?thesis by (simp add: lcoeff_nonzero_nonzero)
-next
- case False
- assume "p ~= 0"
- with False show ?thesis by (simp add: lcoeff_nonzero_deg)
-qed
-
-lemma deg_eqI:
- "[| !!m. n < m ==> coeff p m = 0;
- !!n. n ~= 0 ==> coeff p n ~= 0|] ==> deg p = n"
-by (fast intro: le_antisym deg_aboveI deg_belowI)
-
-(* Degree and polynomial operations *)
-
-lemma deg_add [simp]:
- "deg ((p::'a::ring up) + q) <= max (deg p) (deg q)"
-by (rule deg_aboveI) (simp add: deg_aboveD)
-
-lemma deg_monom_ring:
- "deg (monom a n::'a::ring up) <= n"
-by (rule deg_aboveI) simp
-
-lemma deg_monom [simp]:
- "a ~= 0 ==> deg (monom a n::'a::ring up) = n"
-by (fastforce intro: le_antisym deg_aboveI deg_belowI)
-
-lemma deg_const [simp]:
- "deg (monom (a::'a::ring) 0) = 0"
-proof (rule le_antisym)
- show "deg (monom a 0) <= 0" by (rule deg_aboveI) simp
-next
- show "0 <= deg (monom a 0)" by (rule deg_belowI) simp
-qed
-
-lemma deg_zero [simp]:
- "deg 0 = 0"
-proof (rule le_antisym)
- show "deg 0 <= 0" by (rule deg_aboveI) simp
-next
- show "0 <= deg 0" by (rule deg_belowI) simp
-qed
-
-lemma deg_one [simp]:
- "deg 1 = 0"
-proof (rule le_antisym)
- show "deg 1 <= 0" by (rule deg_aboveI) simp
-next
- show "0 <= deg 1" by (rule deg_belowI) simp
-qed
-
-lemma uminus_monom:
- "!!a::'a::ring. (-a = 0) = (a = 0)"
-proof
- fix a::"'a::ring"
- assume "a = 0"
- then show "-a = 0" by simp
-next
- fix a::"'a::ring"
- assume "- a = 0"
- then have "-(- a) = 0" by simp
- then show "a = 0" by simp
-qed
-
-lemma deg_uminus [simp]:
- "deg (-p::('a::ring) up) = deg p"
-proof (rule le_antisym)
- show "deg (- p) <= deg p" by (simp add: deg_aboveI deg_aboveD)
-next
- show "deg p <= deg (- p)"
- by (simp add: deg_belowI lcoeff_nonzero_deg uminus_monom)
-qed
-
-lemma deg_smult_ring:
- "deg ((a::'a::ring) *s p) <= (if a = 0 then 0 else deg p)"
-proof (cases "a = 0")
-qed (simp add: deg_aboveI deg_aboveD)+
-
-lemma deg_smult [simp]:
- "deg ((a::'a::domain) *s p) = (if a = 0 then 0 else deg p)"
-proof (rule le_antisym)
- show "deg (a *s p) <= (if a = 0 then 0 else deg p)" by (rule deg_smult_ring)
-next
- show "(if a = 0 then 0 else deg p) <= deg (a *s p)"
- proof (cases "a = 0")
- qed (simp, simp add: deg_belowI lcoeff_nonzero_deg integral_iff)
-qed
-
-lemma deg_mult_ring:
- "deg (p * q::'a::ring up) <= deg p + deg q"
-proof (rule deg_aboveI)
- fix m
- assume boundm: "deg p + deg q < m"
- {
- fix k i
- assume boundk: "deg p + deg q < k"
- then have "coeff p i * coeff q (k - i) = 0"
- proof (cases "deg p < i")
- case True then show ?thesis by (simp add: deg_aboveD)
- next
- case False with boundk have "deg q < k - i" by arith
- then show ?thesis by (simp add: deg_aboveD)
- qed
- }
- (* This is similar to bound_mult_zero and deg_above_mult_zero in the old
- proofs. *)
- with boundm show "coeff (p * q) m = 0" by simp
-qed
-
-lemma deg_mult [simp]:
- "[| (p::'a::domain up) ~= 0; q ~= 0|] ==> deg (p * q) = deg p + deg q"
-proof (rule le_antisym)
- show "deg (p * q) <= deg p + deg q" by (rule deg_mult_ring)
-next
- let ?s = "(%i. coeff p i * coeff q (deg p + deg q - i))"
- assume nz: "p ~= 0" "q ~= 0"
- have less_add_diff: "!!(k::nat) n m. k < n ==> m < n + m - k" by arith
- show "deg p + deg q <= deg (p * q)"
- proof (rule deg_belowI, simp)
- have "setsum ?s {.. deg p + deg q}
- = setsum ?s ({..< deg p} Un {deg p .. deg p + deg q})"
- by (simp only: ivl_disj_un_one)
- also have "... = setsum ?s {deg p .. deg p + deg q}"
- by (simp add: setsum_Un_disjoint ivl_disj_int_one
- setsum_0 deg_aboveD less_add_diff)
- also have "... = setsum ?s ({deg p} Un {deg p <.. deg p + deg q})"
- by (simp only: ivl_disj_un_singleton)
- also have "... = coeff p (deg p) * coeff q (deg q)"
- by (simp add: setsum_Un_disjoint setsum_0 deg_aboveD)
- finally have "setsum ?s {.. deg p + deg q}
- = coeff p (deg p) * coeff q (deg q)" .
- with nz show "setsum ?s {.. deg p + deg q} ~= 0"
- by (simp add: integral_iff lcoeff_nonzero)
- qed
- qed
-
-lemma coeff_natsum:
- "((coeff (setsum p A) k)::'a::ring) =
- setsum (%i. coeff (p i) k) A"
-proof (cases "finite A")
- case True then show ?thesis by induct auto
-next
- case False then show ?thesis by simp
-qed
-(* Instance of a more general result!!! *)
-
-(*
-lemma coeff_natsum:
- "((coeff (setsum p {..n::nat}) k)::'a::ring) =
- setsum (%i. coeff (p i) k) {..n}"
-by (induct n) auto
-*)
-
-lemma up_repr:
- "setsum (%i. monom (coeff p i) i) {..deg (p::'a::ring up)} = p"
-proof (rule up_eqI)
- let ?s = "(%i. monom (coeff p i) i)"
- fix k
- show "coeff (setsum ?s {..deg p}) k = coeff p k"
- proof (cases "k <= deg p")
- case True
- hence "coeff (setsum ?s {..deg p}) k =
- coeff (setsum ?s ({..k} Un {k<..deg p})) k"
- by (simp only: ivl_disj_un_one)
- also from True
- have "... = coeff (setsum ?s {..k}) k"
- by (simp add: setsum_Un_disjoint ivl_disj_int_one order_less_imp_not_eq2
- setsum_0 coeff_natsum )
- also
- have "... = coeff (setsum ?s ({.. setsum (%i. monom (coeff p i) i) {..n} = p"
-proof -
- let ?s = "(%i. monom (coeff p i) i)"
- assume "deg p <= n"
- then have "setsum ?s {..n} = setsum ?s ({..deg p} Un {deg p<..n})"
- by (simp only: ivl_disj_un_one)
- also have "... = setsum ?s {..deg p}"
- by (simp add: setsum_Un_disjoint ivl_disj_int_one
- setsum_0 deg_aboveD)
- also have "... = p" by (rule up_repr)
- finally show ?thesis .
-qed
-
-instance up :: ("domain") "domain"
-proof
- show "1 ~= (0::'a up)"
- proof (* notI is applied here *)
- assume "1 = (0::'a up)"
- hence "coeff 1 0 = (coeff 0 0::'a)" by simp
- hence "1 = (0::'a)" by simp
- with one_not_zero show "False" by contradiction
- qed
-next
- fix p q :: "'a::domain up"
- assume pq: "p * q = 0"
- show "p = 0 | q = 0"
- proof (rule classical)
- assume c: "~ (p = 0 | q = 0)"
- then have "deg p + deg q = deg (p * q)" by simp
- also from pq have "... = 0" by simp
- finally have "deg p + deg q = 0" .
- then have f1: "deg p = 0 & deg q = 0" by simp
- from f1 have "p = setsum (%i. (monom (coeff p i) i)) {..0}"
- by (simp only: up_repr_le)
- also have "... = monom (coeff p 0) 0" by simp
- finally have p: "p = monom (coeff p 0) 0" .
- from f1 have "q = setsum (%i. (monom (coeff q i) i)) {..0}"
- by (simp only: up_repr_le)
- also have "... = monom (coeff q 0) 0" by simp
- finally have q: "q = monom (coeff q 0) 0" .
- have "coeff p 0 * coeff q 0 = coeff (p * q) 0" by simp
- also from pq have "... = 0" by simp
- finally have "coeff p 0 * coeff q 0 = 0" .
- then have "coeff p 0 = 0 | coeff q 0 = 0" by (simp only: integral_iff)
- with p q show "p = 0 | q = 0" by fastforce
- qed
-qed
-
-lemma monom_inj_zero:
- "(monom a n = 0) = (a = 0)"
-proof -
- have "(monom a n = 0) = (monom a n = monom 0 n)" by simp
- also have "... = (a = 0)" by (simp add: monom_inj del: monom_zero)
- finally show ?thesis .
-qed
-(* term order: makes this simpler!!!
-lemma smult_integral:
- "(a::'a::domain) *s p = 0 ==> a = 0 | p = 0"
-by (simp add: monom_mult_is_smult [THEN sym] integral_iff monom_inj_zero) fast
-*)
-lemma smult_integral:
- "(a::'a::domain) *s p = 0 ==> a = 0 | p = 0"
-by (simp add: monom_mult_is_smult [THEN sym] integral_iff monom_inj_zero)
-
-
-(* Divisibility and degree *)
-
-lemma "!! p::'a::domain up. [| p dvd q; q ~= 0 |] ==> deg p <= deg q"
- apply (unfold dvd_def)
- apply (erule exE)
- apply hypsubst
- apply (case_tac "p = 0")
- apply (case_tac [2] "k = 0")
- apply auto
- done
-
-end
diff -r 237190475d79 -r 7957d26c3334 src/HOL/ROOT
--- a/src/HOL/ROOT Mon Mar 25 19:53:44 2013 +0100
+++ b/src/HOL/ROOT Mon Mar 25 20:00:27 2013 +0100
@@ -268,10 +268,6 @@
Divisibility (* Rings *)
IntRing (* Ideals and residue classes *)
UnivPoly (* Polynomials *)
- theories [document = false]
- (*** Old development, based on axiomatic type classes ***)
- "abstract/Abstract" (*The ring theory*)
- "poly/Polynomial" (*The full theory*)
files "document/root.bib" "document/root.tex"
session "HOL-Auth" in Auth = HOL +