--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/README.html Fri Nov 05 11:14:26 1999 +0100
@@ -0,0 +1,59 @@
+<!-- $Id$ -->
+<HTML><HEAD><TITLE>HOL/Algebra/README.html</TITLE></HEAD><BODY>
+
+<H2>Algebra: Theories of Rings and Polynomials</H2>
+
+<P>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:
+
+<P><EM>Rings:</EM>
+ Classes of rings are represented by axiomatic type classes. The
+ following are available:
+
+<PRE>
+ ringS: Syntactic class
+ 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
+</PRE>
+
+ Also, some facts about ring homomorphisms and ideals are mechanised.
+
+<P><EM>Polynomials:</EM>
+ Polynomials have a natural, mathematical representation. Facts about
+ the following topics are provided:
+
+<MENU>
+<LI>Degree function
+<LI> Universal Property, evaluation homomorphism
+<LI>Long division (existence and uniqueness)
+<LI>Polynomials over a ring form a ring
+<LI>Polynomials over an integral domain form an integral domain
+</MENU>
+
+ <P>Still missing are
+ Polynomials over a factorial domain form a factorial domain
+ (difficult), and polynomials over a field form a pid.
+
+<P>[Jacobson1985] Nathan Jacobson, Basic Algebra I, Freeman, 1985.
+
+<P>[Ballarin1999] Clemens Ballarin, Computer Algebra and Theorem Proving,
+ Author's <A HREF="http://iaks-www.ira.uka.de/iaks-calmet/ballarin/publications.html">PhD thesis</A>, 1999.
+
+<HR>
+<P>Last modified on $Date$
+
+<ADDRESS>
+<P><A HREF="http://iaks-www.ira.uka.de/iaks-calmet/ballarin">Clemens Ballarin</A>. Karlsruhe, October 1999
+
+<A NAME="ballarin@ira.uka.de" HREF="mailto:ballarin@ira.uka.de">ballarin@ira.uka.de</A>
+</ADDRESS>
+</BODY></HTML>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/ROOT.ML Fri Nov 05 11:14:26 1999 +0100
@@ -0,0 +1,11 @@
+(*
+ Polynomials
+ $Id$
+ Author: Clemens Ballarin, started 24 September 1999
+*)
+
+add_path "abstract";
+add_path "poly";
+
+use_thy "Abstract"; (*The ring theory*)
+use_thy "Polynomial"; (*The full theory*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/abstract/Abstract.thy Fri Nov 05 11:14:26 1999 +0100
@@ -0,0 +1,7 @@
+(*
+ Summary theory of the development of abstract algebra
+ $Id$
+ Author: Clemens Ballarin, started 17 July 1997
+*)
+
+Abstract = RingHomo + Field
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/abstract/Factor.ML Fri Nov 05 11:14:26 1999 +0100
@@ -0,0 +1,49 @@
+(*
+ Factorisation within a factorial domain
+ $Id$
+ Author: Clemens Ballarin, started 25 November 1997
+*)
+
+open Factor;
+
+goalw Ring.thy [assoc_def] "!! c::'a::factorial. \
+\ [| irred c; irred a; irred b; c dvd (a*b) |] ==> c assoc a | c assoc b";
+by (ftac factorial_prime 1);
+by (rewrite_goals_tac [irred_def, prime_def]);
+by (Blast_tac 1);
+qed "irred_dvd_lemma";
+
+goalw Ring.thy [assoc_def] "!! 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)";
+by (induct_tac "factors" 1);
+(* Base case: c dvd a contradicts irred c *)
+by (full_simp_tac (simpset() addsimps [irred_def]) 1);
+by (blast_tac (claset() addIs [dvd_trans_ring]) 1);
+(* Induction step *)
+by (ftac factorial_prime 1);
+by (full_simp_tac (simpset() addsimps [irred_def, prime_def]) 1);
+by (Blast_tac 1);
+qed "irred_dvd_list_lemma";
+
+goal Ring.thy "!! 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";
+by (rtac (irred_dvd_list_lemma RS mp) 1);
+by (Auto_tac);
+qed "irred_dvd_list";
+
+Goalw [Factorisation_def] "!! c::'a::factorial. \
+\ [| irred c; Factorisation x factors u; c dvd x |] ==> \
+\ EX d. c assoc d & d : set factors";
+by (rtac (irred_dvd_list_lemma RS mp) 1);
+by (Auto_tac);
+qed "Factorisation_dvd";
+
+Goalw [Factorisation_def] "!! c::'a::factorial. \
+\ [| Factorisation x factors u; a : set factors |] ==> irred a";
+by (Blast_tac 1);
+qed "Factorisation_irred";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/abstract/Factor.thy Fri Nov 05 11:14:26 1999 +0100
@@ -0,0 +1,18 @@
+(*
+ Factorisation within a factorial domain
+ $Id$
+ Author: Clemens Ballarin, started 25 November 1997
+*)
+
+Factor = Ring +
+
+consts
+ Factorisation :: ['a::ringS, 'a list, 'a] => bool
+ (* factorisation of x into a list of irred factors and a unit u *)
+
+defs
+ Factorisation_def "Factorisation x factors u ==
+ x = foldr op* factors u &
+ (ALL a : set factors. irred a) & u dvd <1>"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/abstract/Field.thy Fri Nov 05 11:14:26 1999 +0100
@@ -0,0 +1,15 @@
+(*
+ Properties of abstract class field
+ $Id$
+ Author: Clemens Ballarin, started 15 November 1997
+*)
+
+Field = Factor + Ideal +
+
+instance
+ field < domain (field_integral)
+
+instance
+ field < factorial (TrueI, field_fact_prime)
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/abstract/Ideal.ML Fri Nov 05 11:14:26 1999 +0100
@@ -0,0 +1,322 @@
+(*
+ Ideals for commutative rings
+ $Id$
+ Author: Clemens Ballarin, started 24 September 1999
+*)
+
+(* is_ideal *)
+
+Goalw [is_ideal_def]
+ "!! 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";
+by Auto_tac;
+qed "is_idealI";
+
+Goalw [is_ideal_def] "[| is_ideal I; a:I; b:I |] ==> a + b : I";
+by (Fast_tac 1);
+qed "is_ideal_add";
+
+Goalw [is_ideal_def] "[| is_ideal I; a:I |] ==> - a : I";
+by (Fast_tac 1);
+qed "is_ideal_uminus";
+
+Goalw [is_ideal_def] "[| is_ideal I |] ==> <0> : I";
+by (Fast_tac 1);
+qed "is_ideal_zero";
+
+Goalw [is_ideal_def] "[| is_ideal I; a:I |] ==> a * r : I";
+by (Fast_tac 1);
+qed "is_ideal_mult";
+
+Goalw [dvd_def, is_ideal_def] "[| a dvd b; is_ideal I; a:I |] ==> b:I";
+by (Fast_tac 1);
+qed "is_ideal_dvd";
+
+Goalw [is_ideal_def] "is_ideal (UNIV::('a::ring) set)";
+by Auto_tac;
+qed "UNIV_is_ideal";
+
+Goalw [is_ideal_def] "is_ideal {<0>::'a::ring}";
+by Auto_tac;
+qed "zero_is_ideal";
+
+Addsimps [is_ideal_add, is_ideal_uminus, is_ideal_zero, is_ideal_mult,
+ UNIV_is_ideal, zero_is_ideal];
+
+Goal "is_ideal {x::'a::ring. a dvd x}";
+by (rtac is_idealI 1);
+by Auto_tac;
+qed "is_ideal_1";
+
+Goal "is_ideal {x::'a::ring. EX u v. x = a * u + b * v}";
+by (rtac is_idealI 1);
+by Auto_tac;
+by (res_inst_tac [("x", "u+ua")] exI 1);
+by (res_inst_tac [("x", "v+va")] exI 1);
+by (res_inst_tac [("x", "-u")] exI 2);
+by (res_inst_tac [("x", "-v")] exI 2);
+by (res_inst_tac [("x", "<0>")] exI 3);
+by (res_inst_tac [("x", "<0>")] exI 3);
+by (res_inst_tac [("x", "u * r")] exI 4);
+by (res_inst_tac [("x", "v * r")] exI 4);
+by (REPEAT (simp_tac (simpset() addsimps [r_distr, l_distr, r_minus, minus_add, m_assoc]@a_ac) 1));
+qed "is_ideal_2";
+
+(* ideal_of *)
+
+Goalw [is_ideal_def, ideal_of_def] "is_ideal (ideal_of S)";
+by (Blast_tac 1); (* Here, blast_tac is much superior to fast_tac! *)
+qed "ideal_of_is_ideal";
+
+Goalw [ideal_of_def] "a:S ==> a : (ideal_of S)";
+by Auto_tac;
+qed "generator_in_ideal";
+
+Goalw [ideal_of_def] "ideal_of {<1>::'a::ring} = UNIV";
+by (auto_tac (claset() addSDs [is_ideal_mult], simpset()));
+ (* loops if is_ideal_mult is added as non-safe rule *)
+qed "ideal_of_one_eq";
+
+Goalw [ideal_of_def] "ideal_of {} = {<0>::'a::ring}";
+by (rtac subset_antisym 1);
+by (rtac subsetI 1);
+by (dtac InterD 1);
+by (assume_tac 2);
+by (auto_tac (claset(), simpset() addsimps [is_ideal_zero]));
+qed "ideal_of_empty_eq";
+
+Goalw [ideal_of_def] "ideal_of {a} = {x::'a::ring. a dvd x}";
+by (rtac subset_antisym 1);
+by (rtac subsetI 1);
+by (dtac InterD 1);
+by (assume_tac 2);
+by (auto_tac (claset() addIs [is_ideal_1], simpset()));
+by (asm_simp_tac (simpset() addsimps [is_ideal_dvd]) 1);
+qed "pideal_structure";
+
+Goalw [ideal_of_def]
+ "ideal_of {a, b} = {x::'a::ring. EX u v. x = a * u + b * v}";
+by (rtac subset_antisym 1);
+by (rtac subsetI 1);
+by (dtac InterD 1);
+by (assume_tac 2);
+by (auto_tac (claset() addIs [is_ideal_2], simpset()));
+by (res_inst_tac [("x", "<1>")] exI 1);
+by (res_inst_tac [("x", "<0>")] exI 1);
+by (res_inst_tac [("x", "<0>")] exI 2);
+by (res_inst_tac [("x", "<1>")] exI 2);
+by (Simp_tac 1);
+by (Simp_tac 1);
+qed "ideal_of_2_structure";
+
+Goalw [ideal_of_def] "A <= B ==> ideal_of A <= ideal_of B";
+by Auto_tac;
+qed "ideal_of_mono";
+
+Goal "ideal_of {<0>::'a::ring} = {<0>}";
+by (simp_tac (simpset() addsimps [pideal_structure]) 1);
+by (rtac subset_antisym 1);
+by (auto_tac (claset() addIs [dvd_zero_left], simpset()));
+qed "ideal_of_zero_eq";
+
+Goal "[| is_ideal I; a : I |] ==> ideal_of {a::'a::ring} <= I";
+by (auto_tac (claset(),
+ simpset() addsimps [pideal_structure, is_ideal_dvd]));
+qed "element_generates_subideal";
+
+(* is_pideal *)
+
+Goalw [is_pideal_def] "is_pideal (I::('a::ring) set) ==> is_ideal I";
+by (fast_tac (claset() addIs [ideal_of_is_ideal]) 1);
+qed "is_pideal_imp_is_ideal";
+
+Goalw [is_pideal_def] "is_pideal (ideal_of {a::'a::ring})";
+by (Fast_tac 1);
+qed "pideal_is_pideal";
+
+Goalw [is_pideal_def] "is_pideal I ==> EX a. I = ideal_of {a}";
+by (assume_tac 1);
+qed "is_pidealD";
+
+(* Ideals and divisibility *)
+
+Goal "b dvd a ==> ideal_of {a::'a::ring} <= ideal_of {b}";
+by (auto_tac (claset() addIs [dvd_trans_ring],
+ simpset() addsimps [pideal_structure]));
+qed "dvd_imp_subideal";
+
+Goal "ideal_of {a::'a::ring} <= ideal_of {b} ==> b dvd a";
+by (auto_tac (claset() addSDs [subsetD],
+ simpset() addsimps [pideal_structure]));
+qed "subideal_imp_dvd";
+
+Goal "(ideal_of {a::'a::ring} <= ideal_of {b}) = b dvd a";
+by (rtac iffI 1);
+by (REPEAT (ares_tac [subideal_imp_dvd, dvd_imp_subideal] 1));
+qed "subideal_is_dvd";
+
+Goal "(ideal_of {a::'a::ring} < ideal_of {b}) ==> ~ (a dvd b)";
+by (full_simp_tac (simpset() addsimps [psubset_eq, pideal_structure]) 1);
+by (etac conjE 1);
+by (dres_inst_tac [("c", "a")] subsetD 1);
+by (auto_tac (claset() addIs [dvd_trans_ring],
+ simpset()));
+qed "psubideal_not_dvd";
+
+Goal "[| b dvd a; ~ (a dvd b) |] ==> ideal_of {a::'a::ring} < ideal_of {b}";
+by (rtac psubsetI 1);
+by (rtac dvd_imp_subideal 1 THEN atac 1);
+by (rtac contrapos 1); by (assume_tac 1);
+by (rtac subideal_imp_dvd 1);
+by (Asm_simp_tac 1);
+qed "not_dvd_psubideal";
+
+Goal "(ideal_of {a::'a::ring} < ideal_of {b}) = (b dvd a & ~ (a dvd b))";
+by (rtac iffI 1);
+by (REPEAT (ares_tac
+ [conjI, psubideal_not_dvd, psubset_imp_subset RS subideal_imp_dvd] 1));
+by (etac conjE 1);
+by (REPEAT (ares_tac [not_dvd_psubideal] 1));
+qed "psubideal_is_dvd";
+
+Goal "[| a dvd b; b dvd a |] ==> ideal_of {a::'a::ring} = ideal_of {b}";
+by (rtac subset_antisym 1);
+by (REPEAT (ares_tac [dvd_imp_subideal] 1));
+qed "assoc_pideal_eq";
+
+AddIffs [subideal_is_dvd, psubideal_is_dvd];
+
+Goal "!!a::'a::ring. a dvd b ==> b : (ideal_of {a})";
+by (rtac is_ideal_dvd 1);
+by (assume_tac 1);
+by (rtac ideal_of_is_ideal 1);
+by (rtac generator_in_ideal 1);
+by (Simp_tac 1);
+qed "dvd_imp_in_pideal";
+
+Goal "!!a::'a::ring. b : (ideal_of {a}) ==> a dvd b";
+by (full_simp_tac (simpset() addsimps [pideal_structure]) 1);
+qed "in_pideal_imp_dvd";
+
+Goal "~ (a dvd b) ==> ideal_of {a::'a::ring} < ideal_of {a, b}";
+by (asm_simp_tac (simpset() addsimps [psubset_eq, ideal_of_mono]) 1);
+by (simp_tac (simpset() addsimps [ideal_of_2_structure]) 1);
+by (etac contrapos 1);
+by (rtac in_pideal_imp_dvd 1);
+by (Asm_simp_tac 1);
+by (res_inst_tac [("x", "<0>")] exI 1);
+by (res_inst_tac [("x", "<1>")] exI 1);
+by (Simp_tac 1);
+qed "not_dvd_psubideal";
+
+Goalw [irred_def]
+ "[| irred (a::'a::ring); is_pideal I; ideal_of {a} < I |] ==> x : I";
+by (dtac is_pidealD 1);
+by (etac exE 1);
+by (Clarify_tac 1);
+by (eres_inst_tac [("x", "aa")] allE 1);
+by (Clarify_tac 1);
+by (dres_inst_tac [("a", "<1>")] dvd_imp_subideal 1);
+by (auto_tac (claset(), simpset() addsimps [ideal_of_one_eq]));
+qed "irred_imp_max_ideal";
+
+(* Pid are factorial *)
+
+(* Divisor chain condition *)
+(* proofs not finished *)
+
+Goal "(ALL i. I i <= I (Suc i)) --> (n <= m & a : I n --> a : I m)";
+by (rtac impI 1);
+by (nat_ind_tac "m" 1);
+by (Blast_tac 1);
+(* induction step *)
+by (case_tac "n <= m" 1);
+by Auto_tac;
+by (subgoal_tac "n = Suc m" 1);
+by (hyp_subst_tac 1);
+by Auto_tac;
+qed "subset_chain_lemma";
+
+Goal "[| ALL i. is_ideal (I i); ALL i. I i <= I (Suc i) |] ==> \
+\ is_ideal (Union (I``UNIV))";
+by (rtac is_idealI 1);
+by Auto_tac;
+by (res_inst_tac [("x", "max x xa")] exI 1);
+by (rtac is_ideal_add 1);
+by (Asm_simp_tac 1);
+by (rtac (subset_chain_lemma RS mp RS mp) 1);
+by (assume_tac 1);
+by (rtac conjI 1);
+by (assume_tac 2);
+by (arith_tac 1);
+by (rtac (subset_chain_lemma RS mp RS mp) 1);
+by (assume_tac 1);
+by (rtac conjI 1);
+by (assume_tac 2);
+by (arith_tac 1);
+by (res_inst_tac [("x", "x")] exI 1);
+by (Asm_simp_tac 1);
+by (res_inst_tac [("x", "x")] exI 1);
+by (Asm_simp_tac 1);
+qed "chain_is_ideal";
+
+(*
+Goal "ALL i. ideal_of {a i} < ideal_of {a (Suc i)} ==> \
+\ EX n. Union ((ideal_of o (%a. {a}))``UNIV) = ideal_of {a n}";
+
+Goal "wf {(a::'a::pid, b). a dvd b & ~ (b dvd a)}";
+by (simp_tac (simpset()
+ addsimps [psubideal_is_dvd RS sym, wf_iff_no_infinite_down_chain]
+ delsimps [psubideal_is_dvd]) 1);
+*)
+
+(* Primeness condition *)
+
+Goalw [prime_def] "irred a ==> prime (a::'a::pid)";
+by (rtac conjI 1);
+by (rtac conjI 2);
+by (Clarify_tac 3);
+by (dres_inst_tac [("I", "ideal_of {a, b}"), ("x", "<1>")]
+ irred_imp_max_ideal 3);
+by (auto_tac (claset() addIs [ideal_of_is_ideal, pid_ax],
+ simpset() addsimps [irred_def, not_dvd_psubideal, pid_ax]));
+by (full_simp_tac (simpset() addsimps [ideal_of_2_structure]) 1);
+by (Clarify_tac 1);
+by (dres_inst_tac [("f", "op* aa")] arg_cong 1);
+by (full_simp_tac (simpset() addsimps [r_distr]) 1);
+by (etac ssubst 1);
+by (asm_simp_tac (simpset() addsimps [m_assoc RS sym]) 1);
+qed "pid_irred_imp_prime";
+
+(* Fields are Pid *)
+
+Goal "a ~= <0> ==> ideal_of {a::'a::field} = UNIV";
+by (rtac subset_antisym 1);
+by (Simp_tac 1);
+by (rtac subset_trans 1);
+by (rtac dvd_imp_subideal 2);
+by (rtac field_ax 2);
+by (assume_tac 2);
+by (simp_tac (simpset() addsimps [ideal_of_one_eq]) 1);
+qed "field_pideal_univ";
+
+Goal "[| is_ideal I; I ~= {<0>} |] ==> {<0>} < I";
+by (asm_simp_tac (simpset() addsimps [psubset_eq, not_sym, is_ideal_zero]) 1);
+qed "proper_ideal";
+
+Goalw [is_pideal_def] "is_ideal (I::('a::field) set) ==> is_pideal I";
+by (case_tac "I = {<0>}" 1);
+by (res_inst_tac [("x", "<0>")] exI 1);
+by (asm_simp_tac (simpset() addsimps [ideal_of_zero_eq]) 1);
+(* case "I ~= {<0>}" *)
+by (ftac proper_ideal 1);
+by (assume_tac 1);
+by (dtac psubset_imp_ex_mem 1);
+by (etac exE 1);
+by (res_inst_tac [("x", "b")] exI 1);
+by (cut_inst_tac [("a", "b")] element_generates_subideal 1);
+ by (assume_tac 1); by (Blast_tac 1);
+by (auto_tac (claset(), simpset() addsimps [field_pideal_univ]));
+qed "field_pid";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/abstract/Ideal.thy Fri Nov 05 11:14:26 1999 +0100
@@ -0,0 +1,28 @@
+(*
+ Ideals for commutative rings
+ $Id$
+ Author: Clemens Ballarin, started 24 September 1999
+*)
+
+Ideal = Ring +
+
+consts
+ ideal_of :: ('a::ringS) set => 'a set
+ is_ideal :: ('a::ringS) set => bool
+ is_pideal :: ('a::ringS) set => bool
+
+defs
+ is_ideal_def "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)"
+ ideal_of_def "ideal_of S == Inter {I. is_ideal I & S <= I}"
+ is_pideal_def "is_pideal I == (EX a. I = ideal_of {a})"
+
+(* Principle ideal domains *)
+
+axclass
+ pid < domain
+
+ pid_ax "is_ideal I ==> is_pideal I"
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/abstract/NatSum.ML Fri Nov 05 11:14:26 1999 +0100
@@ -0,0 +1,268 @@
+(*
+ Sums with naturals as index domain
+ $Id$
+ Author: Clemens Ballarin, started 12 December 1996
+*)
+
+open NatSum;
+
+section "Basic Properties";
+
+Goalw [SUM_def] "SUM 0 f = (f 0::'a::ring)";
+by (Asm_simp_tac 1);
+qed "SUM_0";
+
+Goalw [SUM_def]
+ "SUM (Suc n) f = (f (Suc n) + SUM n f::'a::ring)";
+by (Simp_tac 1);
+qed "SUM_Suc";
+
+Addsimps [SUM_0, SUM_Suc];
+
+Goal
+ "SUM (Suc n) f = (SUM n (%i. f (Suc i)) + f 0::'a::ring)";
+by (nat_ind_tac "n" 1);
+(* Base case *)
+by (Simp_tac 1);
+(* Induction step *)
+by (asm_full_simp_tac (simpset() addsimps [a_assoc]) 1);
+qed "SUM_Suc2";
+
+(* Congruence rules *)
+
+val [p_equal, p_context] = goal NatSum.thy
+ "[| m = n; !!i. i <= n ==> f i = g i |] ==> SUM m f = (SUM n g::'a::ring)";
+by (simp_tac (simpset() addsimps [p_equal]) 1);
+by (cut_inst_tac [("n", "n")] le_refl 1);
+by (etac rev_mp 1);
+by (res_inst_tac [("P", "%k. k <= n --> SUM k f = SUM k g")] nat_induct 1);
+(* Base case *)
+by (simp_tac (simpset() addsimps [p_context]) 1);
+(* Induction step *)
+by (rtac impI 1);
+by (etac impE 1);
+by (rtac Suc_leD 1);
+by (assume_tac 1);
+by (asm_simp_tac (simpset() addsimps [p_context]) 1);
+qed "SUM_cong";
+
+Addcongs [SUM_cong];
+
+(* Results needed for the development of polynomials *)
+
+section "Ring Properties";
+
+Goal "SUM n (%i. <0>) = (<0>::'a::ring)";
+by (nat_ind_tac "n" 1);
+by (Simp_tac 1);
+by (Asm_simp_tac 1);
+qed "SUM_zero";
+
+Addsimps [SUM_zero];
+
+Goal
+ "!!f::nat=>'a::ring. SUM n (%i. f i + g i) = SUM n f + SUM n g";
+by (nat_ind_tac "n" 1);
+(* Base case *)
+by (Simp_tac 1);
+(* Induction step *)
+by (asm_simp_tac (simpset() addsimps a_ac) 1);
+qed "SUM_add";
+
+Goal
+ "!!a::'a::ring. SUM n f * a = SUM n (%i. f i * a)";
+by (nat_ind_tac "n" 1);
+(* Base case *)
+by (Simp_tac 1);
+(* Induction step *)
+by (asm_simp_tac (simpset() addsimps [l_distr]) 1);
+qed "SUM_ldistr";
+
+Goal
+ "!!a::'a::ring. a * SUM n f = SUM n (%i. a * f i)";
+by (nat_ind_tac "n" 1);
+(* Base case *)
+by (Simp_tac 1);
+(* Induction step *)
+by (asm_simp_tac (simpset() addsimps [r_distr]) 1);
+qed "SUM_rdistr";
+
+section "Results for the Construction of Polynomials";
+
+goal Main.thy (* could go to Arith *)
+ "!!j::nat. [| m <= j; Suc j <= n |] ==> (n - m) - Suc (j - m) = n - Suc j";
+by (asm_simp_tac (simpset() addsimps [Suc_diff_le RS sym]) 1);
+by (asm_simp_tac (simpset() addsimps [diff_right_cancel, less_imp_le]) 1);
+qed "Suc_diff_lemma";
+
+Goal
+ "!!a::nat=>'a::ring. k <= n --> \
+\ SUM k (%j. SUM j (%i. a i * b (j-i)) * c (n-j)) = \
+\ SUM k (%j. a j * SUM (k-j) (%i. b i * c (n-j-i)))";
+by (nat_ind_tac "k" 1);
+(* Base case *)
+by (simp_tac (simpset() addsimps [m_assoc]) 1);
+(* Induction step *)
+by (rtac impI 1);
+by (etac impE 1);
+by (rtac Suc_leD 1);
+by (assume_tac 1);
+by (asm_simp_tac (simpset() addsimps a_ac@[Suc_diff_le, l_distr, r_distr, m_assoc, SUM_add]) 1);
+by (asm_simp_tac (simpset() addsimps a_ac@[Suc_diff_lemma, SUM_ldistr, m_assoc]) 1);
+qed "poly_assoc_lemma1";
+
+Goal
+ "!!a::nat=>'a::ring. \
+\ SUM n (%j. SUM j (%i. a i * b (j-i)) * c (n-j)) = \
+\ SUM n (%j. a j * SUM (n-j) (%i. b i * c (n-j-i)))";
+by (rtac (poly_assoc_lemma1 RS mp) 1);
+by (rtac le_refl 1);
+qed "poly_assoc_lemma";
+
+goal Main.thy (* could go to Arith *)
+ "!! n. Suc i <= n ==> Suc (a + (n - Suc i)) = a + (n - i)";
+by (asm_simp_tac (simpset() delsimps [add_Suc] addsimps [add_Suc_right RS sym, Suc_diff_Suc]) 1);
+qed "Suc_add_diff_Suc";
+
+goal Main.thy (* could go to Arith *)
+ "!! n. [| Suc j <= n; i <= j |] ==> \
+\ n - Suc i - (n - Suc j) = n - i - (n - j)";
+by (res_inst_tac [("m1", "n - Suc i"), ("n1", "n - Suc j")]
+ (diff_Suc_Suc RS subst) 1);
+by (subgoal_tac "Suc i <= n" 1);
+by (asm_simp_tac (simpset() delsimps [diff_Suc_Suc] addsimps [Suc_diff_Suc]) 1);
+by (fast_arith_tac 1);
+qed "diff_lemma2";
+
+Goal
+ "!! a::nat=>'a::ring. j <= n --> \
+\ SUM j (%i. a i * b (n-i)) = SUM j (%i. a (n-i-(n-j)) * b (i+(n-j)))";
+by (nat_ind_tac "j" 1);
+(* Base case *)
+by (Simp_tac 1);
+(* Induction step *)
+by (rtac impI 1);
+by (etac impE 1);
+by (rtac Suc_leD 1);
+by (assume_tac 1);
+by (stac SUM_Suc2 1);
+by (stac SUM_Suc 1);
+by (asm_simp_tac (simpset()
+ addsimps [a_comm, Suc_add_diff_Suc, diff_diff_cancel, diff_lemma2]) 1);
+qed "poly_comm_lemma1";
+
+Goal
+ "!!a::nat=>'a::ring. SUM n (%i. a i * b (n-i)) = SUM n (%i. a (n-i) * b i)";
+by (cut_inst_tac [("j", "n"), ("n", "n")] poly_comm_lemma1 1);
+by (Asm_full_simp_tac 1);
+qed "poly_comm_lemma";
+
+section "Changing the Range of Summation";
+
+Goal
+ "!! f::(nat=>'a::ring). \
+\ SUM n (%i. if i = x then f i else <0>) = (if x <= n then f x else <0>)";
+by (nat_ind_tac "n" 1);
+(* Base case *)
+by (simp_tac (simpset() setloop (split_tac [expand_if])) 1);
+(* Induction step *)
+by (asm_simp_tac (simpset() setloop (split_tac [expand_if])) 1);
+by (Clarify_tac 1);
+by (res_inst_tac [("f", "f")] arg_cong 1);
+by (fast_arith_tac 1);
+qed "SUM_if_singleton";
+
+Goal
+ "!! f::(nat=>'a::ring). \
+\ m <= n & (ALL i. m < i & i <= n --> f i = <0>) --> \
+\ SUM m f = SUM n f";
+by (nat_ind_tac "n" 1);
+(* Base case *)
+by (Simp_tac 1);
+(* Induction step *)
+by (case_tac "m <= n" 1);
+by (rtac impI 1);
+by (etac impE 1);
+by (SELECT_GOAL Auto_tac 1);
+by (etac conjE 1);
+by (dres_inst_tac [("x", "Suc n")] spec 1);
+by (asm_simp_tac (simpset() addsimps [less_Suc_eq_le]) 1);
+(* case n < m, in fact m = Suc n *)
+by (rtac impI 1);
+by (etac conjE 1);
+by (subgoal_tac "m = Suc n" 1);
+by (Asm_simp_tac 1);
+by (fast_arith_tac 1);
+val SUM_shrink_lemma = result();
+
+Goal
+ "!! f::(nat=>'a::ring). \
+\ [| m <= n; !!i. [| m < i; i <= n |] ==> f i = <0>; P (SUM n f) |] ==> \
+\ P (SUM m f)";
+by (cut_inst_tac [("m", "m"), ("n", "n"), ("f", "f")] SUM_shrink_lemma 1);
+by (Asm_full_simp_tac 1);
+qed "SUM_shrink";
+
+Goal
+ "!! f::(nat=>'a::ring). \
+\ [| m <= n; !!i. [| m < i; i <= n |] ==> f i = <0>; P (SUM m f) |] ==> \
+\ P (SUM n f)";
+by (cut_inst_tac [("m", "m"), ("n", "n"), ("f", "f")] SUM_shrink_lemma 1);
+by (Asm_full_simp_tac 1);
+qed "SUM_extend";
+
+Goal
+ "!! f::(nat=>'a::ring). \
+\ (ALL i. i < m --> f i = <0>) --> SUM d (%i. f (i+m)) = SUM (m+d) f";
+by (nat_ind_tac "d" 1);
+(* Base case *)
+by (nat_ind_tac "m" 1);
+by (Simp_tac 1);
+by (rtac impI 1);
+by (etac impE 1);
+by (Asm_simp_tac 1);
+by (subgoal_tac "SUM m f = <0>" 1);
+by (Asm_simp_tac 1);
+by (Asm_full_simp_tac 1);
+(* Induction step *)
+by (asm_simp_tac (simpset() addsimps add_ac) 1);
+val SUM_shrink_below_lemma = result();
+
+Goal
+ "!! f::(nat=>'a::ring). \
+\ [| m <= n; !!i. i < m ==> f i = <0>; P (SUM (n-m) (%i. f (i+m))) |] ==> \
+\ P (SUM n f)";
+by (asm_full_simp_tac (simpset() addsimps
+ [SUM_shrink_below_lemma, add_diff_inverse, leD]) 1);
+qed "SUM_extend_below";
+
+section "Result for the Univeral Property of Polynomials";
+
+Goal
+ "!!f::nat=>'a::ring. j <= n + m --> \
+\ SUM j (%k. SUM k (%i. f i * g (k - i))) = \
+\ SUM j (%k. SUM (j - k) (%i. f k * g i))";
+by (nat_ind_tac "j" 1);
+(* Base case *)
+by (Simp_tac 1);
+(* Induction step *)
+by (simp_tac (simpset() addsimps [Suc_diff_le]) 1);
+by (simp_tac (simpset() addsimps [SUM_add]) 1);
+by (rtac impI 1);
+by (etac impE 1);
+by (dtac Suc_leD 1);
+by (assume_tac 1);
+by (asm_simp_tac (simpset() addsimps a_ac) 1);
+val DiagSum_lemma = result();
+
+Goal
+ "!!f::nat=>'a::ring. \
+\ SUM (n + m) (%k. SUM k (%i. f i * g (k - i))) = \
+\ SUM (n + m) (%k. SUM (n + m - k) (%i. f k * g i))";
+by (rtac (DiagSum_lemma RS mp) 1);
+by (rtac le_refl 1);
+qed "DiagSum";
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/abstract/NatSum.thy Fri Nov 05 11:14:26 1999 +0100
@@ -0,0 +1,15 @@
+(*
+ Sums with naturals as index domain
+ $Id$
+ Author: Clemens Ballarin, started 12 December 1996
+*)
+
+NatSum = Ring +
+
+consts
+ SUM :: [nat, nat => 'a] => 'a::ringS
+
+defs
+ SUM_def "SUM n f == nat_rec <0> (%m sum. f m + sum) (Suc n)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/abstract/PID.thy Fri Nov 05 11:14:26 1999 +0100
@@ -0,0 +1,13 @@
+(*
+ Principle ideal domains
+ $Id$
+ Author: Clemens Ballarin, started 5 October 1999
+*)
+
+PID = Ideal +
+
+instance
+ pid < factorial (TrueI, pid_irred_imp_prime)
+
+end
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/abstract/Ring.ML Fri Nov 05 11:14:26 1999 +0100
@@ -0,0 +1,396 @@
+(*
+ Abstract class ring (commutative, with 1)
+ $Id$
+ Author: Clemens Ballarin, started 9 December 1996
+*)
+
+open Ring;
+
+Blast.overloaded ("Divides.op dvd", domain_type);
+
+section "Rings";
+
+fun make_left_commute assoc commute s =
+ [rtac (commute RS trans) 1, rtac (assoc RS trans) 1,
+ rtac (commute RS arg_cong) 1];
+
+(* addition *)
+
+qed_goal "a_lcomm" Ring.thy "!!a::'a::ring. a+(b+c) = b+(a+c)"
+ (make_left_commute a_assoc a_comm);
+
+val a_ac = [a_assoc, a_comm, a_lcomm];
+
+qed_goal "r_zero" Ring.thy "!!a::'a::ring. a + <0> = a"
+ (fn _ => [rtac (a_comm RS trans) 1, rtac l_zero 1]);
+
+qed_goal "r_neg" Ring.thy "!!a::'a::ring. a + (-a) = <0>"
+ (fn _ => [rtac (a_comm RS trans) 1, rtac l_neg 1]);
+
+Goal "!! a::'a::ring. a + b = a + c ==> b = c";
+by (rtac box_equals 1);
+by (rtac l_zero 2);
+by (rtac l_zero 2);
+by (res_inst_tac [("a1", "a")] (l_neg RS subst) 1);
+by (asm_simp_tac (simpset() addsimps [a_assoc]) 1);
+qed "a_lcancel";
+
+Goal "!! a::'a::ring. b + a = c + a ==> b = c";
+by (rtac a_lcancel 1);
+by (asm_simp_tac (simpset() addsimps a_ac) 1);
+qed "a_rcancel";
+
+Goal "!! a::'a::ring. (a + b = a + c) = (b = c)";
+by (auto_tac (claset() addSDs [a_lcancel], simpset()));
+qed "a_lcancel_eq";
+
+Goal "!! a::'a::ring. (b + a = c + a) = (b = c)";
+by (simp_tac (simpset() addsimps [a_lcancel_eq, a_comm]) 1);
+qed "a_rcancel_eq";
+
+Addsimps [a_lcancel_eq, a_rcancel_eq];
+
+Goal "!!a::'a::ring. -(-a) = a";
+by (rtac a_lcancel 1);
+by (rtac (r_neg RS trans) 1);
+by (rtac (l_neg RS sym) 1);
+qed "minus_minus";
+
+Goal "- <0> = (<0>::'a::ring)";
+by (rtac a_lcancel 1);
+by (rtac (r_neg RS trans) 1);
+by (rtac (l_zero RS sym) 1);
+qed "minus0";
+
+Goal "!!a::'a::ring. -(a + b) = (-a) + (-b)";
+by (res_inst_tac [("a", "a+b")] a_lcancel 1);
+by (simp_tac (simpset() addsimps ([r_neg, l_neg, l_zero]@a_ac)) 1);
+qed "minus_add";
+
+(* multiplication *)
+
+qed_goal "m_lcomm" Ring.thy "!!a::'a::ring. a*(b*c) = b*(a*c)"
+ (make_left_commute m_assoc m_comm);
+
+val m_ac = [m_assoc, m_comm, m_lcomm];
+
+qed_goal "r_one" Ring.thy "!!a::'a::ring. a * <1> = a"
+ (fn _ => [rtac (m_comm RS trans) 1, rtac l_one 1]);
+
+(* distributive and derived *)
+
+Goal "!!a::'a::ring. a * (b + c) = a * b + a * c";
+by (rtac (m_comm RS trans) 1);
+by (rtac (l_distr RS trans) 1);
+by (simp_tac (simpset() addsimps [m_comm]) 1);
+qed "r_distr";
+
+val m_distr = m_ac @ [l_distr, r_distr];
+
+(* the following two proofs can be found in
+ Jacobson, Basic Algebra I, pp. 88-89 *)
+
+Goal "!!a::'a::ring. <0> * a = <0>";
+by (rtac a_lcancel 1);
+by (rtac (l_distr RS sym RS trans) 1);
+by (simp_tac (simpset() addsimps [r_zero]) 1);
+qed "l_null";
+
+qed_goal "r_null" Ring.thy "!!a::'a::ring. a * <0> = <0>"
+ (fn _ => [rtac (m_comm RS trans) 1, rtac l_null 1]);
+
+Goal "!!a::'a::ring. (-a) * b = - (a * b)";
+by (rtac a_lcancel 1);
+by (rtac (r_neg RS sym RSN (2, trans)) 1);
+by (rtac (l_distr RS sym RS trans) 1);
+by (simp_tac (simpset() addsimps [l_null, r_neg]) 1);
+qed "l_minus";
+
+Goal "!!a::'a::ring. a * (-b) = - (a * b)";
+by (rtac a_lcancel 1);
+by (rtac (r_neg RS sym RSN (2, trans)) 1);
+by (rtac (r_distr RS sym RS trans) 1);
+by (simp_tac (simpset() addsimps [r_null, r_neg]) 1);
+qed "r_minus";
+
+val m_minus = [l_minus, r_minus];
+
+(* one and zero are distinct *)
+
+qed_goal "zero_not_one" Ring.thy "<0> ~= (<1>::'a::ring)"
+ (fn _ => [rtac not_sym 1, rtac one_not_zero 1]);
+
+Addsimps [l_zero, r_zero, l_neg, r_neg, minus_minus, minus0,
+ l_one, r_one, l_null, r_null,
+ one_not_zero, zero_not_one];
+
+(* further rules *)
+
+Goal "!!a::'a::ring. -a = <0> ==> a = <0>";
+by (res_inst_tac [("t", "a")] (minus_minus RS subst) 1);
+by (Asm_simp_tac 1);
+qed "uminus_monom";
+
+Goal "!!a::'a::ring. a ~= <0> ==> -a ~= <0>";
+by (etac contrapos 1);
+by (rtac uminus_monom 1);
+by (assume_tac 1);
+qed "uminus_monom_neq";
+
+Goal "!!a::'a::ring. a * b ~= <0> ==> a ~= <0>";
+by (etac contrapos 1);
+by (Asm_simp_tac 1);
+qed "l_nullD";
+
+Goal "!!a::'a::ring. a * b ~= <0> ==> b ~= <0>";
+by (etac contrapos 1);
+by (Asm_simp_tac 1);
+qed "r_nullD";
+
+(* reflection between a = b and a -- b = <0> *)
+
+Goal "!!a::'a::ring. a = b ==> a + (-b) = <0>";
+by (Asm_simp_tac 1);
+qed "eq_imp_diff_zero";
+
+Goal "!!a::'a::ring. a + (-b) = <0> ==> a = b";
+by (res_inst_tac [("a", "-b")] a_rcancel 1);
+by (Asm_simp_tac 1);
+qed "diff_zero_imp_eq";
+
+(* this could be a rewrite rule, but won't terminate
+ ==> make it a simproc?
+Goal "!!a::'a::ring. (a = b) = (a -- b = <0>)";
+*)
+
+(* Power *)
+
+Goal "!!a::'a::ring. a ^ 0 = <1>";
+by (simp_tac (simpset() addsimps [power_ax]) 1);
+qed "power_0";
+
+Goal "!!a::'a::ring. a ^ Suc n = a ^ n * a";
+by (simp_tac (simpset() addsimps [power_ax]) 1);
+qed "power_Suc";
+
+Addsimps [power_0, power_Suc];
+
+Goal "<1> ^ n = (<1>::'a::ring)";
+by (nat_ind_tac "n" 1);
+by (Simp_tac 1);
+by (Asm_simp_tac 1);
+qed "power_one";
+
+Goal "!!n. n ~= 0 ==> <0> ^ n = (<0>::'a::ring)";
+by (etac rev_mp 1);
+by (nat_ind_tac "n" 1);
+by (Simp_tac 1);
+by (Simp_tac 1);
+qed "power_zero";
+
+Addsimps [power_zero, power_one];
+
+Goal "!! a::'a::ring. a ^ m * a ^ n = a ^ (m + n)";
+by (nat_ind_tac "m" 1);
+by (Simp_tac 1);
+by (asm_simp_tac (simpset() addsimps m_ac) 1);
+qed "power_mult";
+
+(* Divisibility *)
+section "Divisibility";
+
+Goalw [dvd_def] "!! a::'a::ring. a dvd <0>";
+by (res_inst_tac [("x", "<0>")] exI 1);
+by (Simp_tac 1);
+qed "dvd_zero_right";
+
+Goalw [dvd_def] "!! a::'a::ring. <0> dvd a ==> a = <0>";
+by Auto_tac;
+qed "dvd_zero_left";
+
+Goalw [dvd_def] "!! a::'a::ring. a dvd a";
+by (res_inst_tac [("x", "<1>")] exI 1);
+by (Simp_tac 1);
+qed "dvd_refl_ring";
+
+Goalw [dvd_def] "!! a::'a::ring. [| a dvd b; b dvd c |] ==> a dvd c";
+by (Step_tac 1);
+by (res_inst_tac [("x", "k * ka")] exI 1);
+by (simp_tac (simpset() addsimps m_ac) 1);
+qed "dvd_trans_ring";
+
+Addsimps [dvd_zero_right, dvd_refl_ring];
+
+Goal "!! a::'a::ring. a dvd <1> ==> a ~= <0>";
+by (auto_tac (claset() addDs [dvd_zero_left], simpset()));
+qed "unit_imp_nonzero";
+
+Goalw [dvd_def]
+ "!!a::'a::ring. [| a dvd <1>; b dvd <1> |] ==> a * b dvd <1>";
+by (Clarify_tac 1);
+by (res_inst_tac [("x", "k * ka")] exI 1);
+by (asm_full_simp_tac (simpset() addsimps m_ac) 1);
+qed "unit_mult";
+
+Goal "!!a::'a::ring. a dvd <1> ==> a^n dvd <1>";
+by (induct_tac "n" 1);
+by (Simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [unit_mult]) 1);
+qed "unit_power";
+
+Goalw [dvd_def]
+ "!! a::'a::ring. [| a dvd b; a dvd c |] ==> a dvd (b + c)";
+by (Clarify_tac 1);
+by (res_inst_tac [("x", "k + ka")] exI 1);
+by (simp_tac (simpset() addsimps [r_distr]) 1);
+qed "dvd_add_right";
+
+Goalw [dvd_def]
+ "!! a::'a::ring. a dvd b ==> a dvd (-b)";
+by (Clarify_tac 1);
+by (res_inst_tac [("x", "-k")] exI 1);
+by (simp_tac (simpset() addsimps [r_minus]) 1);
+qed "dvd_uminus_right";
+
+Goalw [dvd_def]
+ "!! a::'a::ring. a dvd b ==> a dvd (c * b)";
+by (Clarify_tac 1);
+by (res_inst_tac [("x", "c * k")] exI 1);
+by (simp_tac (simpset() addsimps m_ac) 1);
+qed "dvd_l_mult_right";
+
+Goalw [dvd_def]
+ "!! a::'a::ring. a dvd b ==> a dvd (b * c)";
+by (Clarify_tac 1);
+by (res_inst_tac [("x", "k * c")] exI 1);
+by (simp_tac (simpset() addsimps m_ac) 1);
+qed "dvd_r_mult_right";
+
+Addsimps [dvd_add_right, dvd_uminus_right, dvd_l_mult_right, dvd_r_mult_right];
+
+(* Inverse of multiplication *)
+
+section "inverse";
+
+Goal "!! a::'a::ring. [| a * x = <1>; a * y = <1> |] ==> x = y";
+by (res_inst_tac [("a", "(a*y)*x"), ("b", "y*(a*x)")] box_equals 1);
+by (simp_tac (simpset() addsimps m_ac) 1);
+by Auto_tac;
+qed "inverse_unique";
+
+Goalw [inverse_def, dvd_def]
+ "!! a::'a::ring. a dvd <1> ==> a * inverse a = <1>";
+by (Asm_simp_tac 1);
+by (Clarify_tac 1);
+by (rtac selectI 1);
+by (rtac sym 1);
+by (assume_tac 1);
+qed "r_inverse_ring";
+
+Goal "!! a::'a::ring. a dvd <1> ==> inverse a * a= <1>";
+by (asm_simp_tac (simpset() addsimps r_inverse_ring::m_ac) 1);
+qed "l_inverse_ring";
+
+(* Integral domain *)
+
+section "Integral domains";
+
+Goal
+ "!! a. [| a * b = <0>; a ~= <0> |] ==> (b::'a::domain) = <0>";
+by (dtac integral 1);
+by (Fast_tac 1);
+qed "r_integral";
+
+Goal
+ "!! a. [| a * b = <0>; b ~= <0> |] ==> (a::'a::domain) = <0>";
+by (dtac integral 1);
+by (Fast_tac 1);
+qed "l_integral";
+
+Goal
+ "!! a::'a::domain. [| a ~= <0>; b ~= <0> |] ==> a * b ~= <0>";
+by (etac contrapos 1);
+by (rtac l_integral 1);
+by (assume_tac 1);
+by (assume_tac 1);
+qed "not_integral";
+
+Addsimps [not_integral];
+
+Goal "!! a::'a::domain. [| a * x = x; x ~= <0> |] ==> a = <1>";
+by (res_inst_tac [("a", "- <1>")] a_lcancel 1);
+by (Simp_tac 1);
+by (rtac l_integral 1);
+by (assume_tac 2);
+by (asm_simp_tac (simpset() addsimps [l_distr, l_minus]) 1);
+qed "l_one_integral";
+
+Goal "!! a::'a::domain. [| x * a = x; x ~= <0> |] ==> a = <1>";
+by (res_inst_tac [("a", "- <1>")] a_rcancel 1);
+by (Simp_tac 1);
+by (rtac r_integral 1);
+by (assume_tac 2);
+by (asm_simp_tac (simpset() addsimps [r_distr, r_minus]) 1);
+qed "r_one_integral";
+
+(* cancellation laws for multiplication *)
+
+Goal "!! a::'a::domain. [| a ~= <0>; a * b = a * c |] ==> b = c";
+by (rtac diff_zero_imp_eq 1);
+by (dtac eq_imp_diff_zero 1);
+by (full_simp_tac (simpset() addsimps [r_minus RS sym, r_distr RS sym]) 1);
+by (fast_tac (claset() addIs [l_integral]) 1);
+qed "m_lcancel";
+
+Goal "!! a::'a::domain. [| a ~= <0>; b * a = c * a |] ==> b = c";
+by (rtac m_lcancel 1);
+by (assume_tac 1);
+by (asm_full_simp_tac (simpset() addsimps m_ac) 1);
+qed "m_rcancel";
+
+Goal "!! a::'a::domain. a ~= <0> ==> (a * b = a * c) = (b = c)";
+by (auto_tac (claset() addDs [m_lcancel], simpset()));
+qed "m_lcancel_eq";
+
+Goal "!! a::'a::domain. a ~= <0> ==> (b * a = c * a) = (b = c)";
+by (asm_simp_tac (simpset() addsimps [m_lcancel_eq, m_comm]) 1);
+qed "m_rcancel_eq";
+
+Addsimps [m_lcancel_eq, m_rcancel_eq];
+
+(* Fields *)
+
+section "Fields";
+
+Goal "!! a::'a::field. a dvd <1> = (a ~= <0>)";
+by (blast_tac (claset() addDs [field_ax, unit_imp_nonzero]) 1);
+qed "field_unit";
+
+Addsimps [field_unit];
+
+Goal "!! a::'a::field. a ~= <0> ==> a * inverse a = <1>";
+by (asm_full_simp_tac (simpset() addsimps [r_inverse_ring]) 1);
+qed "r_inverse";
+
+Goal "!! a::'a::field. a ~= <0> ==> inverse a * a= <1>";
+by (asm_full_simp_tac (simpset() addsimps [l_inverse_ring]) 1);
+qed "l_inverse";
+
+Addsimps [l_inverse, r_inverse];
+
+(* fields are factorial domains *)
+
+Goal "!! a::'a::field. a * b = <0> ==> a = <0> | b = <0>";
+by (Step_tac 1);
+by (res_inst_tac [("a", "(a*b)*inverse b")] box_equals 1);
+by (rtac refl 3);
+by (simp_tac (simpset() addsimps m_ac) 2);
+by Auto_tac;
+qed "field_integral";
+
+Goalw [prime_def, irred_def] "!! a::'a::field. irred a ==> prime a";
+by (blast_tac (claset() addIs [field_ax]) 1);
+qed "field_fact_prime";
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/abstract/Ring.thy Fri Nov 05 11:14:26 1999 +0100
@@ -0,0 +1,111 @@
+(*
+ Abstract class ring (commutative, with 1)
+ $Id$
+ Author: Clemens Ballarin, started 9 December 1996
+*)
+
+Ring = Main +
+
+(* Syntactic class ring *)
+
+axclass
+ ringS < plus, minus, times, power
+
+consts
+ (* Basic rings *)
+ "<0>" :: 'a::ringS ("<0>")
+ "<1>" :: 'a::ringS ("<1>")
+ "--" :: ['a, 'a] => 'a::ringS (infixl 65)
+
+ (* Divisibility *)
+ assoc :: ['a::times, 'a] => bool (infixl 70)
+ irred :: 'a::ringS => bool
+ prime :: 'a::ringS => bool
+
+ (* Fields *)
+ inverse :: 'a::ringS => 'a
+ "'/'/" :: ['a, 'a] => 'a::ringS (infixl 70)
+
+translations
+ "a -- b" == "a + (-b)"
+ "a // b" == "a * inverse b"
+
+(* Class ring and ring axioms *)
+
+axclass
+ ring < ringS
+
+ a_assoc "(a + b) + c = a + (b + c)"
+ l_zero "<0> + a = a"
+ l_neg "(-a) + a = <0>"
+ a_comm "a + b = b + a"
+
+ m_assoc "(a * b) * c = a * (b * c)"
+ l_one "<1> * a = a"
+
+ l_distr "(a + b) * c = a * c + b * c"
+
+ m_comm "a * b = b * a"
+
+ one_not_zero "<1> ~= <0>"
+ (* if <1> = <0>, then the ring has only one element! *)
+
+ power_ax "a ^ n = nat_rec <1> (%u b. b * a) n"
+
+defs
+ assoc_def "a assoc b == a dvd b & b dvd a"
+ irred_def "irred a == a ~= <0> & ~ a dvd <1>
+ & (ALL d. d dvd a --> d dvd <1> | a dvd d)"
+ prime_def "prime p == p ~= <0> & ~ p dvd <1>
+ & (ALL a b. p dvd (a*b) --> p dvd a | p dvd b)"
+
+ inverse_def "inverse a == if a dvd <1> then @x. a*x = <1> else <0>"
+
+(* Integral domains *)
+
+axclass
+ domain < ring
+
+ integral "a * b = <0> ==> a = <0> | b = <0>"
+
+(* Factorial domains *)
+
+axclass
+ factorial < domain
+
+(*
+ Proper definition using divisor chain condition currently not supported.
+ factorial_divisor "wf {(a, b). a dvd b & ~ (b dvd a)}"
+*)
+ factorial_divisor "True"
+ factorial_prime "irred a ==> prime a"
+
+(* Euclidean domains *)
+
+(*
+axclass
+ euclidean < domain
+
+ 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.
+*)
+
+(* Fields *)
+
+axclass
+ field < ring
+
+ field_ax "a ~= <0> ==> a dvd <1>"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/abstract/RingHomo.ML Fri Nov 05 11:14:26 1999 +0100
@@ -0,0 +1,65 @@
+(*
+ Ring homomorphism
+ $Id$
+ Author: Clemens Ballarin, started 15 April 1997
+*)
+
+open RingHomo;
+
+(* Ring homomorphism *)
+
+Goalw [homo_def]
+ "!! f. [| !! a b. f (a + b) = f a + f b; !! a b. f (a * b) = f a * f b; \
+\ f <1> = <1> |] ==> homo f";
+by Auto_tac;
+qed "homoI";
+
+Goalw [homo_def] "!! f. homo f ==> f (a + b) = f a + f b";
+by (Fast_tac 1);
+qed "homo_add";
+
+Goalw [homo_def] "!! f. homo f ==> f (a * b) = f a * f b";
+by (Fast_tac 1);
+qed "homo_mult";
+
+Goalw [homo_def] "!! f. homo f ==> f <1> = <1>";
+by (Fast_tac 1);
+qed "homo_one";
+
+Goal "!! f::('a::ring=>'b::ring). homo f ==> f <0> = <0>";
+by (res_inst_tac [("a", "f <0>")] a_lcancel 1);
+by (asm_simp_tac (simpset() addsimps [homo_add RS sym]) 1);
+qed "homo_zero";
+
+Goal
+ "!! f::('a::ring=>'b::ring). homo f ==> f (-a) = - f a";
+by (res_inst_tac [("a", "f a")] a_lcancel 1);
+by (ftac homo_zero 1);
+by (asm_simp_tac (simpset() addsimps [homo_add RS sym]) 1);
+qed "homo_uminus";
+
+Goal "!! f::('a::ring=>'b::ring). homo f ==> f (a ^ n) = f a ^ n";
+by (nat_ind_tac "n" 1);
+by (dtac homo_one 1);
+by (Asm_simp_tac 1);
+by (dres_inst_tac [("a", "a^n"), ("b", "a")] homo_mult 1);
+by (Asm_simp_tac 1);
+qed "homo_power";
+
+Goal
+ "!! f::('a::ring=>'b::ring). homo f ==> f (SUM n g) = SUM n (f o g)";
+by (nat_ind_tac "n" 1);
+by (Asm_simp_tac 1);
+by (Simp_tac 1);
+by (dres_inst_tac [("a", "g (Suc n)"), ("b", "SUM n g")] homo_add 1);
+by (Asm_simp_tac 1);
+qed "homo_SUM";
+
+Addsimps [homo_add, homo_mult, homo_one, homo_zero,
+ homo_uminus, homo_power, homo_SUM];
+
+Goal "homo (%x. x)";
+by (fast_tac (claset() addSIs [homoI]) 1);
+qed "id_homo";
+
+Addsimps [id_homo];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/abstract/RingHomo.thy Fri Nov 05 11:14:26 1999 +0100
@@ -0,0 +1,17 @@
+(*
+ Ring homomorphism
+ $Id$
+ Author: Clemens Ballarin, started 15 April 1997
+*)
+
+RingHomo = NatSum +
+
+consts
+ homo :: ('a::ringS => 'b::ringS) => bool
+
+defs
+ homo_def "homo f == (ALL a b. f (a + b) = f a + f b &
+ f (a * b) = f a * f b) &
+ f <1> = <1>"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/poly/Degree.ML Fri Nov 05 11:14:26 1999 +0100
@@ -0,0 +1,363 @@
+(*
+ Degree of polynomials
+ $Id$
+ written by Clemens Ballarin, started 22 January 1997
+*)
+
+(* Relating degree and bound *)
+
+goal ProtoPoly.thy
+ "!! f. [| bound m f; f n ~= <0> |] ==> n <= m";
+by (rtac classical 1);
+by (dtac not_leE 1);
+by (dtac boundD 1 THEN atac 1);
+by (etac notE 1);
+by (assume_tac 1);
+qed "below_bound";
+
+goal UnivPoly.thy "bound (LEAST n. bound n (Rep_UP p)) (Rep_UP p)";
+by (rtac exE 1);
+by (rtac LeastI 2);
+by (assume_tac 2);
+by (res_inst_tac [("a", "Rep_UP p")] CollectD 1);
+by (rtac (rewrite_rule [UP_def] Rep_UP) 1);
+qed "Least_is_bound";
+
+Goalw [coeff_def, deg_def]
+ "!! p. ALL m. n < m --> coeff m p = <0> ==> deg p <= n";
+by (rtac Least_le 1);
+by (Fast_tac 1);
+qed "deg_aboveI";
+
+Goalw [coeff_def, deg_def]
+ "!! p. (n ~= 0 --> coeff n p ~= <0>) ==> n <= deg p";
+by (case_tac "n = 0" 1);
+(* Case n=0 *)
+by (Asm_simp_tac 1);
+(* Case n~=0 *)
+by (rotate_tac 1 1);
+by (Asm_full_simp_tac 1);
+by (rtac below_bound 1);
+by (assume_tac 2);
+by (rtac Least_is_bound 1);
+qed "deg_belowI";
+
+Goalw [coeff_def, deg_def]
+ "!! p. deg p < m ==> coeff m p = <0>";
+by (rtac exE 1); (* create !! x. *)
+by (rtac boundD 2);
+by (assume_tac 3);
+by (rtac LeastI 2);
+by (assume_tac 2);
+by (res_inst_tac [("a", "Rep_UP p")] CollectD 1);
+by (rtac (rewrite_rule [UP_def] Rep_UP) 1);
+qed "deg_aboveD";
+
+Goalw [deg_def]
+ "!! p. deg p = Suc y ==> ~ bound y (Rep_UP p)";
+by (rtac not_less_Least 1);
+by (Asm_simp_tac 1);
+val lemma1 = result();
+
+Goalw [deg_def, coeff_def]
+ "!! p. deg p = Suc y ==> coeff (deg p) p ~= <0>";
+by (rtac classical 1);
+by (dtac notnotD 1);
+by (cut_inst_tac [("p", "p")] Least_is_bound 1);
+by (subgoal_tac "bound y (Rep_UP p)" 1);
+(* prove subgoal *)
+by (rtac boundI 2);
+by (case_tac "Suc y < m" 2);
+(* first case *)
+by (rtac boundD 2);
+by (assume_tac 2);
+by (Asm_simp_tac 2);
+(* second case *)
+by (dtac leI 2);
+by (dtac Suc_leI 2);
+by (dtac le_anti_sym 2);
+by (assume_tac 2);
+by (Asm_full_simp_tac 2);
+(* end prove subgoal *)
+by (fold_goals_tac [deg_def]);
+by (dtac lemma1 1);
+by (etac notE 1);
+by (assume_tac 1);
+val lemma2 = result();
+
+Goal
+ "!! p. deg p ~= 0 ==> coeff (deg p) p ~= <0>";
+by (rtac lemma2 1);
+by (Full_simp_tac 1);
+by (dtac Suc_pred 1);
+by (rtac sym 1);
+by (Asm_simp_tac 1);
+qed "deg_lcoeff";
+
+Goal
+ "!! p. p ~= <0> ==> coeff (deg p) p ~= <0>";
+by (etac contrapos 1);
+by (ftac contrapos2 1);
+by (rtac deg_lcoeff 1);
+by (assume_tac 1);
+by (rtac up_eqI 1);
+by (case_tac "n=0" 1);
+by (rotate_tac ~2 1);
+by (Asm_full_simp_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [deg_aboveD]) 1);
+qed "nonzero_lcoeff";
+
+Goal "(deg p <= n) = bound n (Rep_UP p)";
+by (rtac iffI 1);
+(* ==> *)
+by (rtac boundI 1);
+by (fold_goals_tac [coeff_def]);
+by (rtac deg_aboveD 1);
+by (fast_arith_tac 1);
+(* <== *)
+by (rtac deg_aboveI 1);
+by (rewtac coeff_def);
+by (Fast_tac 1);
+qed "deg_above_is_bound";
+
+(* Lemmas on the degree function *)
+
+Goalw [max_def]
+ "!! p::'a::ring up. deg (p + q) <= max (deg p) (deg q)";
+by (case_tac "deg p <= deg q" 1);
+(* case deg p <= deg q *)
+by (rtac deg_aboveI 1);
+by (Asm_simp_tac 1);
+by (strip_tac 1);
+by (dtac le_less_trans 1);
+by (assume_tac 1);
+by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
+(* case deg p > deg q *)
+by (rtac deg_aboveI 1);
+by (Asm_simp_tac 1);
+by (dtac not_leE 1);
+by (strip_tac 1);
+by (dtac less_trans 1);
+by (assume_tac 1);
+by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
+qed "deg_add";
+
+Goal "!!p::('a::ring up). deg p < deg q ==> deg (p + q) = deg q";
+by (rtac order_antisym 1);
+by (rtac le_trans 1);
+by (rtac deg_add 1);
+by (Asm_simp_tac 1);
+by (rtac deg_belowI 1);
+by (asm_simp_tac (simpset() addsimps [deg_aboveD, deg_lcoeff]) 1);
+qed "deg_add_equal";
+
+Goal "deg (monom m::'a::ring up) = m";
+by (rtac le_anti_sym 1);
+(* <= *)
+by (asm_simp_tac
+ (simpset() addsimps [deg_aboveI, less_not_refl2 RS not_sym]) 1);
+(* >= *)
+by (asm_simp_tac
+ (simpset() addsimps [deg_belowI, less_not_refl2 RS not_sym]) 1);
+qed "deg_monom";
+
+Goal "!! a::'a::ring. deg (const a) = 0";
+by (rtac le_anti_sym 1);
+by (rtac deg_aboveI 1);
+by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
+by (rtac deg_belowI 1);
+by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
+qed "deg_const";
+
+Goal "deg (<0>::'a::ringS up) = 0";
+by (rtac le_anti_sym 1);
+by (rtac deg_aboveI 1);
+by (Simp_tac 1);
+by (rtac deg_belowI 1);
+by (Simp_tac 1);
+qed "deg_zero";
+
+Goal "deg (<1>::'a::ring up) = 0";
+by (rtac le_anti_sym 1);
+by (rtac deg_aboveI 1);
+by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
+by (rtac deg_belowI 1);
+by (Simp_tac 1);
+qed "deg_one";
+
+Goal "!!p::('a::ring) up. deg (-p) = deg p";
+by (rtac le_anti_sym 1);
+(* <= *)
+by (simp_tac (simpset() addsimps [deg_aboveI, deg_aboveD]) 1);
+by (simp_tac (simpset() addsimps [deg_belowI, deg_lcoeff, uminus_monom_neq]) 1);
+qed "deg_uminus";
+
+Addsimps [deg_monom, deg_const, deg_zero, deg_one, deg_uminus];
+
+Goal
+ "!! a::'a::ring. deg (a *s p) <= (if a = <0> then 0 else deg p)";
+by (case_tac "a = <0>" 1);
+by (REPEAT (asm_simp_tac (simpset() addsimps [deg_aboveI, deg_aboveD]) 1));
+qed "deg_smult_ring";
+
+Goal
+ "!! a::'a::domain. deg (a *s p) = (if a = <0> then 0 else deg p)";
+by (rtac le_anti_sym 1);
+by (rtac deg_smult_ring 1);
+by (case_tac "a = <0>" 1);
+by (REPEAT (asm_simp_tac (simpset() addsimps [deg_belowI, deg_lcoeff]) 1));
+qed "deg_smult";
+
+Goal
+ "!! p::'a::ring up. [| deg p + deg q < k |] ==> \
+\ coeff i p * coeff (k - i) q = <0>";
+by (simp_tac (simpset() addsimps [coeff_def]) 1);
+by (rtac bound_mult_zero 1);
+by (assume_tac 3);
+by (simp_tac (simpset() addsimps [deg_above_is_bound RS sym]) 1);
+by (simp_tac (simpset() addsimps [deg_above_is_bound RS sym]) 1);
+qed "deg_above_mult_zero";
+
+Goal
+ "!! p::'a::ring up. deg (p * q) <= deg p + deg q";
+by (rtac deg_aboveI 1);
+by (asm_simp_tac (simpset() addsimps [deg_above_mult_zero]) 1);
+qed "deg_mult_ring";
+
+goal Main.thy
+ "!!k::nat. k < n ==> m < n + m - k";
+by (arith_tac 1);
+qed "less_add_diff";
+
+Goal "!!p. coeff n p ~= <0> ==> n <= deg p";
+(* More general than deg_belowI, and simplifies the next proof! *)
+by (rtac deg_belowI 1);
+by (Fast_tac 1);
+qed "deg_below2I";
+
+Goal
+ "!! p::'a::domain up. \
+\ [| p ~= <0>; q ~= <0> |] ==> deg (p * q) = deg p + deg q";
+by (rtac le_anti_sym 1);
+by (rtac deg_mult_ring 1);
+(* deg p + deg q <= deg (p * q) *)
+by (rtac deg_below2I 1);
+by (Simp_tac 1);
+(*
+by (rtac conjI 1);
+by (rtac impI 1);
+*)
+by (res_inst_tac [("m", "deg p"), ("n", "deg p + deg q")] SUM_extend 1);
+by (rtac le_add1 1);
+by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
+by (res_inst_tac [("m", "deg p"), ("n", "deg p")] SUM_extend_below 1);
+by (rtac le_refl 1);
+by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
+by (asm_simp_tac (simpset() addsimps [nonzero_lcoeff]) 1);
+(*
+by (rtac impI 1);
+by (res_inst_tac [("m", "deg p"), ("n", "deg p + deg q")] SUM_extend 1);
+by (rtac le_add1 1);
+by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
+by (res_inst_tac [("m", "deg p"), ("n", "deg p")] SUM_extend_below 1);
+by (rtac le_refl 1);
+by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
+by (asm_simp_tac (simpset() addsimps [nonzero_lcoeff]) 1);
+*)
+qed "deg_mult";
+
+Addsimps [deg_smult, deg_mult];
+
+(* Representation theorems about polynomials *)
+
+goal PolyRing.thy
+ "!! p::nat=>'a::ring up. coeff k (SUM n p) = SUM n (%i. coeff k (p i))";
+by (nat_ind_tac "n" 1);
+(* Base case *)
+by (Simp_tac 1);
+(* Induction step *)
+by (Asm_simp_tac 1);
+qed "coeff_SUM";
+
+goal UnivPoly.thy
+ "!! f::(nat=>'a::ring). \
+\ bound n f ==> SUM n (%i. if i = x then f i else <0>) = f x";
+by (simp_tac (simpset() addsimps [SUM_if_singleton]) 1);
+by (auto_tac
+ (claset() addDs [not_leE],
+ simpset() setloop (split_tac [expand_if])));
+qed "bound_SUM_if";
+
+Goal
+ "!! p::'a::ring up. deg p <= n ==> SUM n (%i. coeff i p *s monom i) = p";
+by (rtac up_eqI 1);
+by (simp_tac (simpset() addsimps [coeff_SUM]) 1);
+by (rtac trans 1);
+by (res_inst_tac [("x", "na")] bound_SUM_if 2);
+by (full_simp_tac (simpset() addsimps [deg_above_is_bound, coeff_def]) 2);
+by (rtac SUM_cong 1);
+by (rtac refl 1);
+by (asm_simp_tac
+ (simpset() setloop (split_tac [expand_if])) 1);
+qed "up_repr";
+
+Goal
+ "!! p::'a::ring up. [| deg p <= n; P p |] ==> \
+\ P (SUM n (%i. coeff i p *s monom i))";
+by (asm_simp_tac (simpset() addsimps [up_repr]) 1);
+qed "up_reprD";
+
+Goal
+ "!! p::'a::ring up. [| deg p <= n; P (SUM n (%i. coeff i p *s monom i)) |] \
+\ ==> P p";
+by (asm_full_simp_tac (simpset() addsimps [up_repr]) 1);
+qed "up_repr2D";
+
+(*
+Goal
+ "!! p::'a::ring up. [| deg p <= n; deg q <= m |] ==> \
+\ (SUM n (%i. coeff i p *s monom i) = SUM m (%i. coeff i q *s monom i)) \
+\ = (coeff k f = coeff k g)
+...
+qed "up_unique";
+*)
+
+(* Polynomials over integral domains are again integral domains *)
+
+Goal "!!p::'a::domain up. p * q = <0> ==> p = <0> | q = <0>";
+by (rtac classical 1);
+by (subgoal_tac "deg p = 0 & deg q = 0" 1);
+by (res_inst_tac [("p", "p"), ("n", "0")] up_repr2D 1);
+by (Asm_simp_tac 1);
+by (res_inst_tac [("p", "q"), ("n", "0")] up_repr2D 1);
+by (Asm_simp_tac 1);
+by (subgoal_tac "coeff 0 p = <0> | coeff 0 q = <0>" 1);
+by (SELECT_GOAL (auto_tac (claset() addIs [up_eqI], simpset())) 1);
+by (rtac integral 1);
+by (subgoal_tac "coeff 0 (p * q) = <0>" 1);
+by (Full_simp_tac 1);
+by (Asm_simp_tac 1);
+
+by (dres_inst_tac [("f", "deg")] arg_cong 1);
+by (Asm_full_simp_tac 1);
+qed "up_integral";
+
+Goal "!! a::'a::domain. a *s p = <0> ==> a = <0> | p = <0>";
+by (full_simp_tac (simpset() addsimps [const_mult_is_smult RS sym]) 1);
+by (dtac up_integral 1);
+by Auto_tac;
+by (rtac (const_inj RS injD) 1);
+by (Simp_tac 1);
+qed "smult_integral";
+
+(* Divisibility and degree *)
+
+Goalw [dvd_def]
+ "!! p::'a::domain up. [| p dvd q; q ~= <0> |] ==> deg p <= deg q";
+by (etac exE 1);
+by (hyp_subst_tac 1);
+by (case_tac "p = <0>" 1);
+by (Asm_simp_tac 1);
+by (dtac r_nullD 1);
+by (asm_simp_tac (simpset() addsimps [le_add1]) 1);
+qed "dvd_imp_deg";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/poly/Degree.thy Fri Nov 05 11:14:26 1999 +0100
@@ -0,0 +1,15 @@
+(*
+ Degree of polynomials
+ $Id$
+ written by Clemens Ballarin, started 22. 1. 1997
+*)
+
+Degree = PolyRing +
+
+consts
+ deg :: ('a::ringS) up => nat
+
+defs
+ deg_def "deg p == LEAST n. bound n (Rep_UP p)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/poly/LongDiv.ML Fri Nov 05 11:14:26 1999 +0100
@@ -0,0 +1,214 @@
+(*
+ Long division of polynomials
+ $Id$
+ Author: Clemens Ballarin, started 23 June 1999
+*)
+
+open LongDiv;
+
+(*
+Goalw [lcoeff_def]
+ "!!p::('a::ring up). \
+\ [| deg p = deg q; lcoeff p = - (lcoeff q); deg q ~= 0 |] ==> \
+\ deg (p + q) < deg q";
+by (res_inst_tac [("j", "deg q - 1")] le_less_trans 1);
+by (rtac deg_aboveI 1);
+by (strip_tac 1);
+by (dtac pred_less_imp_le 1);
+by (case_tac "deg q = m" 1);
+by (Clarify_tac 1);
+by (Asm_full_simp_tac 1);
+(* case "deg q ~= m" *)
+by (dtac le_neq_implies_less 1);
+by (assume_tac 1);
+by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
+(* end case *)
+by (asm_full_simp_tac (simpset() addsimps [le_pred_eq]) 1);
+qed "deg_lcoeff_cancel";
+*)
+
+Goal
+ "!!p::('a::ring up). \
+\ [| deg p <= deg r; deg q <= deg r; \
+\ coeff (deg r) p = - (coeff (deg r) q); deg r ~= 0 |] ==> \
+\ deg (p + q) < deg r";
+by (res_inst_tac [("j", "deg r - 1")] le_less_trans 1);
+by (rtac deg_aboveI 1);
+by (strip_tac 1);
+by (dtac pred_less_imp_le 1);
+by (case_tac "deg r = m" 1);
+by (Clarify_tac 1);
+by (Asm_full_simp_tac 1);
+(* case "deg q ~= m" *)
+by (dtac le_neq_implies_less 1 THEN atac 1);
+by (dres_inst_tac [("i", "deg p")] le_less_trans 1); by (assume_tac 1);
+by (dres_inst_tac [("i", "deg q")] le_less_trans 1); by (assume_tac 1);
+by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
+(* end case *)
+by (asm_full_simp_tac (simpset() addsimps [le_pred_eq]) 1);
+qed "deg_lcoeff_cancel";
+
+Goal
+ "!!p::('a::ring up). \
+\ [| deg p <= deg r; deg q <= deg r; \
+\ p ~= -q; coeff (deg r) p = - (coeff (deg r) q) |] ==> \
+\ deg (p + q) < deg r";
+by (rtac deg_lcoeff_cancel 1);
+by (REPEAT (atac 1));
+by (rtac classical 1);
+by (Clarify_tac 1);
+by (etac notE 1);
+by (res_inst_tac [("p", "p")] up_repr2D 1 THEN atac 1);
+by (res_inst_tac [("p", "q")] up_repr2D 1 THEN atac 1);
+by (rotate_tac ~1 1);
+by (asm_full_simp_tac (simpset() addsimps [smult_l_minus]) 1);
+qed "deg_lcoeff_cancel2";
+
+Goal
+ "!!g::('a::ring up). g ~= <0> ==> \
+\ Ex (% (q, r, k). \
+\ (lcoeff g)^k *s f = q * g + r & (eucl_size r < eucl_size g))";
+by (res_inst_tac [("P", "%f. Ex (% (q, r, k). \
+\ (lcoeff g)^k *s f = q * g + r & (eucl_size r < eucl_size g))")]
+ wf_induct 1);
+(* TO DO: replace by measure_induct *)
+by (res_inst_tac [("f", "eucl_size")] wf_measure 1);
+by (case_tac "eucl_size x < eucl_size g" 1);
+by (res_inst_tac [("x", "(<0>, x, 0)")] exI 1);
+by (Asm_simp_tac 1);
+(* case "eucl_size x >= eucl_size g" *)
+by (dres_inst_tac [("x", "lcoeff g *s x -- (lcoeff x *s monom (deg x - deg g)) * g")] spec 1);
+by (etac impE 1);
+by (full_simp_tac (simpset() addsimps [inv_image_def, measure_def, lcoeff_def]) 1);
+by (case_tac "x = <0>" 1);
+by (rotate_tac ~1 1);
+by (asm_full_simp_tac (simpset() addsimps [eucl_size_def]) 1);
+(* case "x ~= <0> *)
+by (rotate_tac ~1 1);
+by (asm_full_simp_tac (simpset() addsimps [eucl_size_def]) 1);
+by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (rtac impI 1);
+by (rtac deg_lcoeff_cancel2 1);
+ (* replace by linear arithmetic??? *)
+ by (rtac le_trans 1);
+ by (rtac deg_smult_ring 1);
+ by (simp_tac (simpset() addsplits [expand_if]) 1);
+ by (Simp_tac 1);
+ by (rtac le_trans 1);
+ by (rtac deg_mult_ring 1);
+ by (rtac le_trans 1);
+ by (rtac add_le_mono1 1);
+ by (rtac deg_smult_ring 1);
+ by (asm_simp_tac (simpset() addsimps [leI] addsplits [expand_if]) 1);
+by (SELECT_GOAL Auto_tac 1);
+by (Simp_tac 1);
+by (res_inst_tac [("m", "deg x - deg g"), ("n", "deg x")] SUM_extend 1);
+by (Simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [less_not_refl2 RS not_sym]) 1);
+by (res_inst_tac [("m", "deg x - deg g"), ("n", "deg x - deg g")]
+ SUM_extend_below 1);
+by (rtac le_refl 1);
+by (asm_simp_tac (simpset() addsimps [less_not_refl2]) 1);
+by (asm_simp_tac (simpset() addsimps [diff_diff_right, leI, m_comm]) 1);
+(* end of subproof deg f1 < deg f *)
+by (etac exE 1);
+by (res_inst_tac [("x", "((%(q,r,k). ((lcoeff g ^ k * lcoeff x) *s monom (deg x - deg g) + q)) xa, (%(q,r,k). r) xa, (%(q,r,k). Suc k) xa)")] exI 1);
+by (Clarify_tac 1);
+by (rtac conjI 1);
+by (dtac sym 1);
+by (simp_tac (simpset() addsimps [l_distr, a_assoc]) 1);
+by (Asm_simp_tac 1);
+by (simp_tac (simpset() addsimps a_ac@[smult_l_distr, smult_r_distr, smult_r_minus, smult_assoc2, smult_assoc1]) 1);
+by Auto_tac;
+qed "long_div_eucl_size";
+
+Goal
+ "!!g::('a::ring up). g ~= <0> ==> \
+\ Ex (% (q, r, k). \
+\ (lcoeff g)^k *s f = q * g + r & (r = <0> | deg r < deg g))";
+by (forw_inst_tac [("f", "f")]
+ (simplify (simpset() addsimps [eucl_size_def]) long_div_eucl_size) 1);
+by Auto_tac;
+by (case_tac "aa = <0>" 1);
+by (Blast_tac 1);
+(* case "aa ~= <0> *)
+by (rotate_tac ~1 1);
+by Auto_tac;
+qed "long_div_ring";
+
+Goal
+ "!!g::('a::ring up). [| g ~= <0>; (lcoeff g) dvd <1> |] ==> \
+\ Ex (% (q, r). f = q * g + r & (r = <0> | deg r < deg g))";
+by (forw_inst_tac [("f", "f")] long_div_ring 1);
+by (etac exE 1);
+by (res_inst_tac [("x", "((%(q,r,k). (Ring.inverse(lcoeff g ^k) *s q)) x, \
+\ (%(q,r,k). Ring.inverse(lcoeff g ^k) *s r) x)")] exI 1);
+by (Clarify_tac 1);
+by (Simp_tac 1);
+by (rtac conjI 1);
+by (dtac sym 1);
+by (asm_simp_tac (simpset() addsimps [smult_r_distr RS sym, smult_assoc2]) 1);
+by (asm_simp_tac (simpset() addsimps [l_inverse_ring, unit_power, smult_assoc1 RS sym]) 1);
+(* degree property *)
+by (etac disjE 1);
+by (Asm_simp_tac 1);
+by (rtac disjI2 1);
+by (rtac le_less_trans 1);
+by (rtac deg_smult_ring 1);
+by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+qed "long_div_unit";
+
+Goal
+ "!!g::('a::field up). g ~= <0> ==> \
+\ Ex (% (q, r). f = q * g + r & (r = <0> | deg r < deg g))";
+by (rtac long_div_unit 1);
+by (assume_tac 1);
+by (asm_simp_tac (simpset() addsimps [lcoeff_def, nonzero_lcoeff, field_ax]) 1);
+qed "long_div_theorem";
+
+Goal
+ "!!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";
+by (subgoal_tac "(q1 -- q2) * g = r2 -- r1" 1); (* 1 *)
+by (thin_tac "f = ?x" 1);
+by (thin_tac "f = ?x" 1);
+by (rtac diff_zero_imp_eq 1);
+by (rtac classical 1);
+by (etac disjE 1);
+(* r1 = <0> *)
+by (etac disjE 1);
+(* r2 = <0> *)
+by (SELECT_GOAL (auto_tac (claset() addDs [integral], simpset())) 1);
+(* r2 ~= <0> *)
+by (dres_inst_tac [("f", "deg"), ("y", "r2 -- r1")] arg_cong 1);
+by (SELECT_GOAL Auto_tac 1);
+(* r1 ~=<0> *)
+by (etac disjE 1);
+(* r2 = <0> *)
+by (dres_inst_tac [("f", "deg"), ("y", "r2 -- r1")] arg_cong 1);
+by (SELECT_GOAL Auto_tac 1);
+(* r2 ~= <0> *)
+by (dres_inst_tac [("f", "deg"), ("y", "r2 -- r1")] arg_cong 1);
+by (SELECT_GOAL Auto_tac 1);
+by (dtac (order_eq_refl RS add_leD2) 1);
+by (dtac leD 1);
+by (etac notE 1 THEN rtac (deg_add RS le_less_trans) 1);
+by (Asm_simp_tac 1);
+(* proof of 1 *)
+by (rtac diff_zero_imp_eq 1);
+by (Asm_full_simp_tac 1);
+by (dres_inst_tac [("a", "?x+?y")] eq_imp_diff_zero 1);
+by (asm_full_simp_tac (simpset() addsimps (l_distr::minus_add::l_minus::a_ac)) 1);
+qed "long_div_quo_unique";
+
+Goal
+ "!!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";
+by (subgoal_tac "q1 = q2" 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [a_lcancel_eq]) 1);
+by (rtac long_div_quo_unique 1);
+by (REPEAT (atac 1));
+qed "long_div_rem_unique";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/poly/LongDiv.thy Fri Nov 05 11:14:26 1999 +0100
@@ -0,0 +1,18 @@
+(*
+ Experimental theory: long division of polynomials
+ $Id$
+ Author: Clemens Ballarin, started 23 June 1999
+*)
+
+LongDiv = PolyHomo +
+
+consts
+ lcoeff :: "'a::ringS up => 'a"
+ eucl_size :: 'a::ringS => nat
+
+defs
+ lcoeff_def "lcoeff p == coeff (deg p) p"
+ eucl_size_def "eucl_size p == if p = <0> then 0 else deg p+1"
+
+end
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/poly/PolyHomo.ML Fri Nov 05 11:14:26 1999 +0100
@@ -0,0 +1,127 @@
+(*
+ Universal property and evaluation homomorphism of univariate polynomials
+ $Id$
+ Author: Clemens Ballarin, started 16 April 1997
+*)
+
+(* Ring homomorphisms and polynomials *)
+
+Goal "homo (const::'a::ring=>'a up)";
+by (auto_tac (claset() addSIs [homoI], simpset()));
+qed "const_homo";
+
+Delsimps [const_add, const_mult, const_one, const_zero];
+Addsimps [const_homo];
+
+Goal
+ "!!f::'a::ring up=>'b::ring. homo f ==> f (a *s p) = f (const a) * f p";
+by (asm_simp_tac (simpset() addsimps [const_mult_is_smult RS sym]) 1);
+qed "homo_smult";
+
+Addsimps [homo_smult];
+
+(* Evaluation homomorphism *)
+
+Goal
+ "!! phi::('a::ring=>'b::ring). homo phi ==> homo (EVAL2 phi a)";
+by (rtac homoI 1);
+by (rewtac EVAL2_def);
+(* + commutes *)
+(* degree estimations:
+ bound of all sums can be extended to max (deg aa) (deg b) *)
+by (res_inst_tac [("m", "deg (aa + b)"), ("n", "max (deg aa) (deg b)")]
+ SUM_shrink 1);
+by (rtac deg_add 1);
+by (asm_simp_tac (simpset() delsimps [coeff_add] addsimps [deg_aboveD]) 1);
+by (res_inst_tac [("m", "deg aa"), ("n", "max (deg aa) (deg b)")]
+ SUM_shrink 1);
+by (rtac le_maxI1 1);
+by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
+by (res_inst_tac [("m", "deg b"), ("n", "max (deg aa) (deg b)")]
+ SUM_shrink 1);
+by (rtac le_maxI2 1);
+by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
+(* actual homom property + *)
+by (asm_simp_tac (simpset() addsimps [l_distr, SUM_add]) 1);
+
+(* * commutes *)
+by (res_inst_tac [("m", "deg (aa * b)"), ("n", "deg aa + deg b")]
+ SUM_shrink 1);
+by (rtac deg_mult_ring 1);
+by (asm_simp_tac (simpset() delsimps [coeff_mult] addsimps [deg_aboveD]) 1);
+by (rtac trans 1);
+by (rtac CauchySum 2);
+by (asm_simp_tac (simpset() addsimps [boundI, deg_aboveD]) 2);
+by (asm_simp_tac (simpset() addsimps [boundI, deg_aboveD]) 2);
+(* getting a^i and a^(k-i) together is difficult, so we do is manually *)
+by (res_inst_tac [("s",
+" SUM (deg aa + deg b) \
+\ (%k. SUM k \
+\ (%i. phi (coeff i aa) * (phi (coeff (k - i) b) * \
+\ (a ^ i * a ^ (k - i)))))")] trans 1);
+by (asm_simp_tac (simpset()
+ addsimps [power_mult, leD RS add_diff_inverse, SUM_ldistr]) 1);
+by (simp_tac (simpset() addsimps m_ac) 1);
+by (simp_tac (simpset() addsimps m_ac) 1);
+(* <1> commutes *)
+by (Asm_simp_tac 1);
+qed "EVAL2_homo";
+
+Goalw [EVAL2_def]
+ "!! phi::'a::ring=>'b::ring. EVAL2 phi a (const b) = phi b";
+by (Simp_tac 1);
+qed "EVAL2_const";
+
+(* This is probably redundant *)
+Goalw [EVAL2_def]
+ "!! phi::'a::ring=>'b::ring. homo phi ==> EVAL2 phi a (monom 1) = a";
+by (Asm_simp_tac 1);
+qed "EVAL2_monom1";
+
+Goalw [EVAL2_def]
+ "!! phi::'a::ring=>'b::ring. homo phi ==> EVAL2 phi a (monom n) = a ^ n";
+by (Simp_tac 1);
+by (nat_ind_tac "n" 1); (* really a case split *)
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
+qed "EVAL2_monom";
+
+Goal
+ "!! phi::'a::ring=>'b::ring. \
+\ homo phi ==> EVAL2 phi a (b *s p) = phi b * EVAL2 phi a p";
+by (asm_simp_tac
+ (simpset() addsimps [const_mult_is_smult RS sym, EVAL2_homo, EVAL2_const]) 1);
+qed "EVAL2_smult";
+
+Goalw [EVAL_def] "!! a::'a::ring. homo (EVAL a)";
+by (asm_simp_tac (simpset() addsimps [EVAL2_homo, id_homo]) 1);
+qed "EVAL_homo";
+
+Goalw [EVAL_def] "!! a::'a::ring. EVAL a (const b) = b";
+by (asm_simp_tac (simpset() addsimps [EVAL2_const]) 1);
+qed "EVAL_const";
+
+Goalw [EVAL_def] "!! a::'a::ring. EVAL a (monom n) = a ^ n";
+by (asm_simp_tac (simpset() addsimps [EVAL2_monom]) 1);
+qed "EVAL_monom";
+
+Goalw [EVAL_def] "!! a::'a::ring. EVAL a (b *s p) = b * EVAL a p";
+by (asm_simp_tac (simpset() addsimps [EVAL2_smult]) 1);
+qed "EVAL_smult";
+
+(* Examples *)
+
+Goal
+ "EVAL (x::'a::ring) (a*X^2 + b*X^1 + c*X^0) = a * x ^ 2 + b * x ^ 1 + c";
+by (asm_simp_tac (simpset() delsimps [power_Suc]
+ addsimps [EVAL_homo, EVAL_monom, EVAL_smult]) 1);
+result();
+
+Goal
+ "EVAL (y::'a::ring) \
+\ (EVAL (const x) (monom 1 + const (a*X^2 + b*X^1 + c*X^0))) = \
+\ x ^ 1 + (a * y ^ 2 + b * y ^ 1 + c)";
+by (asm_simp_tac (simpset() delsimps [power_Suc]
+ addsimps [EVAL_homo, EVAL_monom, EVAL_smult, EVAL_const]) 1);
+result();
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/poly/PolyHomo.thy Fri Nov 05 11:14:26 1999 +0100
@@ -0,0 +1,22 @@
+(*
+ Universal property and evaluation homomorphism of univariate polynomials
+ $Id$
+ Author: Clemens Ballarin, started 15 April 1997
+*)
+
+PolyHomo = Degree +
+
+(* Instantiate result from Degree.ML *)
+
+instance
+ up :: (domain) domain (up_integral)
+
+consts
+ EVAL2 :: ('a::ringS => 'b) => 'b => 'a up => 'b::ringS
+ EVAL :: 'a => 'a up => 'a
+
+defs
+ EVAL2_def "EVAL2 phi a p == SUM (deg p) (%i. phi (coeff i p) * a ^ i)"
+ EVAL_def "EVAL == EVAL2 (%x. x)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/poly/PolyRing.ML Fri Nov 05 11:14:26 1999 +0100
@@ -0,0 +1,96 @@
+(*
+ Instantiate polynomials to form a ring and prove further properties
+ $Id$
+ Author: Clemens Ballarin, started 22 January 1997
+*)
+
+open PolyRing;
+
+(* Properties of *s:
+ Polynomials form a module *)
+
+goal UnivPoly.thy "!!a::'a::ring. (a + b) *s p = a *s p + b *s p";
+by (rtac up_eqI 1);
+by (simp_tac (simpset() addsimps [l_distr]) 1);
+qed "smult_l_distr";
+
+goal UnivPoly.thy "!!a::'a::ring. a *s (p + q) = a *s p + a *s q";
+by (rtac up_eqI 1);
+by (simp_tac (simpset() addsimps [r_distr]) 1);
+qed "smult_r_distr";
+
+goal UnivPoly.thy "!!a::'a::ring. (a * b) *s p = a *s (b *s p)";
+by (rtac up_eqI 1);
+by (simp_tac (simpset() addsimps [m_assoc]) 1);
+qed "smult_assoc1";
+
+goal UnivPoly.thy "(<1>::'a::ring) *s p = p";
+by (rtac up_eqI 1);
+by (Simp_tac 1);
+qed "smult_one";
+
+(* Polynomials form an algebra *)
+
+goal UnivPoly.thy "!!a::'a::ring. (a *s p) * q = a *s (p * q)";
+by (rtac up_eqI 1);
+by (simp_tac (simpset() addsimps [SUM_rdistr, m_assoc]) 1);
+qed "smult_assoc2";
+
+(* the following can be derived from the above ones,
+ for generality reasons, it is therefore done *)
+
+Goal "(<0>::'a::ring) *s p = <0>";
+by (rtac a_lcancel 1);
+by (rtac (smult_l_distr RS sym RS trans) 1);
+by (Simp_tac 1);
+qed "smult_l_null";
+
+Goal "!!a::'a::ring. a *s <0> = <0>";
+by (rtac a_lcancel 1);
+by (rtac (smult_r_distr RS sym RS trans) 1);
+by (Simp_tac 1);
+qed "smult_r_null";
+
+Goal "!!a::'a::ring. (-a) *s p = - (a *s p)";
+by (rtac a_lcancel 1);
+by (rtac (r_neg RS sym RSN (2, trans)) 1);
+by (rtac (smult_l_distr RS sym RS trans) 1);
+by (simp_tac (simpset() addsimps [smult_l_null, r_neg]) 1);
+qed "smult_l_minus";
+
+Goal "!!a::'a::ring. a *s (-p) = - (a *s p)";
+by (rtac a_lcancel 1);
+by (rtac (r_neg RS sym RSN (2, trans)) 1);
+by (rtac (smult_r_distr RS sym RS trans) 1);
+by (simp_tac (simpset() addsimps [smult_r_null, r_neg]) 1);
+qed "smult_r_minus";
+
+val smult_minus = [smult_l_minus, smult_r_minus];
+
+(* Integrity of smult *)
+(*
+Goal
+ "!! a::'a::domain. a *s b = <0> ==> a = <0> | b = <0>";
+by (simp_tac (simpset() addsimps [disj_commute]) 1);
+
+by (rtac (disj_commute RS trans) 1);
+by (rtac contrapos2 1);
+by (assume_tac 1);
+by (rtac up_neqI 1);
+by (Full_simp_tac 1);
+by (etac conjE 1);
+by (rtac not_integral 1);
+by (assume_tac 1);
+by (etac contrapos 1);
+back();
+by (rtac up_eqI 1);
+by (Simp_tac 1);
+
+by (rtac integral 1);
+
+by (etac conjE 1);
+
+by (rtac disjCI 1);
+*)
+
+Addsimps [smult_one, smult_l_null, smult_r_null];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/poly/PolyRing.thy Fri Nov 05 11:14:26 1999 +0100
@@ -0,0 +1,15 @@
+(*
+ Instantiate polynomials to form a ring and prove further properties
+ $Id$
+ Author: Clemens Ballarin, started 20 January 1997
+*)
+
+PolyRing = UnivPoly +
+
+instance
+ up :: (ring) ring
+ (up_a_assoc, up_l_zero, up_l_neg, up_a_comm,
+ up_m_assoc, up_l_one, up_l_distr, up_m_comm, up_one_not_zero,
+ up_power_def) {| rtac refl 1 |}
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/poly/Polynomial.thy Fri Nov 05 11:14:26 1999 +0100
@@ -0,0 +1,11 @@
+(*
+ Summary theory of the development of (not instantiated) polynomials
+ $Id$
+ Author: Clemens Ballarin, started 17 July 1997
+*)
+
+Polynomial = LongDiv
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/poly/ProtoPoly.ML Fri Nov 05 11:14:26 1999 +0100
@@ -0,0 +1,32 @@
+(*
+ Prepearing definitions for polynomials
+ $Id$
+ Author: Clemens Ballarin, started 9 December 1996
+*)
+
+open ProtoPoly;
+
+(* Rules for bound *)
+
+val prem = goalw ProtoPoly.thy [bound_def]
+ "[| !! m. n < m ==> f m = <0> |] ==> bound n f";
+by (fast_tac (claset() addIs prem) 1);
+qed "boundI";
+
+Goalw [bound_def]
+ "!! f. [| bound n f; n < m |] ==> f m = <0>";
+by (Fast_tac 1);
+qed "boundD";
+
+Goalw [bound_def]
+ "!! f. [| bound n f; n <= m |] ==> bound m f";
+by (fast_tac (set_cs addIs [le_less_trans]) 1);
+(* Need set_cs, otherwise starts reasoning about naturals *)
+qed "le_bound";
+
+AddSIs [boundI];
+AddDs [boundD];
+
+Goal "(%x. <0>) : {f. EX n. bound n f}";
+by (Blast_tac 1);
+qed "UP_witness";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/poly/ProtoPoly.thy Fri Nov 05 11:14:26 1999 +0100
@@ -0,0 +1,15 @@
+(*
+ Prepearing definitions for polynomials
+ $Id$
+ Author: Clemens Ballarin, started 9 December 1996
+*)
+
+ProtoPoly = Abstract +
+
+consts
+ bound :: [nat, nat => 'a::ringS] => bool
+
+defs
+ bound_def "bound n f == ALL i. n<i --> f i = <0>"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/poly/UnivPoly.ML Fri Nov 05 11:14:26 1999 +0100
@@ -0,0 +1,262 @@
+(*
+ Univariate Polynomials
+ $Id$
+ Author: Clemens Ballarin, started 9 December 1996
+TODO: monom is *mono*morphism (probably induction needed)
+*)
+
+(* Closure of UP under +, *s, monom, const and * *)
+
+Goalw [UP_def]
+ "!! f g. [| f : UP; g : UP |] ==> (%n. (f n + g n::'a::ring)) : UP";
+by (Step_tac 1);
+(* instantiate bound for the sum and do case split *)
+by (res_inst_tac [("x", "if n<=na then na else n")] exI 1);
+by (case_tac "n <= na" 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 2);
+(* first case, bound of g higher *)
+by (etac (make_elim le_bound) 1 THEN atac 1);
+by (REPEAT (Step_tac 1));
+by (Asm_simp_tac 1);
+(* second case is identical,
+ apart from we have to massage the inequality *)
+by (dtac (not_leE RS less_imp_le) 1);
+by (etac (make_elim le_bound) 1 THEN atac 1);
+by (REPEAT (Step_tac 1));
+by (Asm_simp_tac 1);
+qed "UP_closed_add";
+
+Goalw [UP_def]
+ "!! f. f : UP ==> (%n. (a * f n::'a::ring)) : UP";
+by (REPEAT (Step_tac 1));
+by (Asm_simp_tac 1);
+qed "UP_closed_smult";
+
+Goalw [UP_def]
+ "!! m. (%n. if m = n then <1> else <0>) : UP";
+by (Step_tac 1);
+by (res_inst_tac [("x", "m")] exI 1);
+by (Step_tac 1);
+by (dtac (less_not_refl2 RS not_sym) 1);
+by (Asm_simp_tac 1);
+qed "UP_closed_monom";
+
+Goalw [UP_def]
+ "!! a. (%n. if n = 0 then a else <0>) : UP";
+by (Step_tac 1);
+by (res_inst_tac [("x", "0")] exI 1);
+by (rtac boundI 1);
+by (asm_simp_tac (simpset() addsimps [less_not_refl2]) 1);
+qed "UP_closed_const";
+
+Goal
+ "!! f::nat=>'a::ring. \
+\ [| bound n f; bound m g; n + m < k |] ==> f i * g (k - i) = <0>";
+(* Case split: either f i or g (k - i) is zero *)
+by (case_tac "n<i" 1);
+(* First case, f i is zero *)
+by (SELECT_GOAL Auto_tac 1);
+(* Second case, we have to derive m < k-i *)
+by (subgoal_tac "m < k-i" 1);
+by (SELECT_GOAL Auto_tac 1);
+(* More inequalities, quite nasty *)
+by (rtac add_less_imp_less_diff 1);
+by (stac add_commute 1);
+by (dtac leI 1);
+by (rtac le_less_trans 1);
+by (assume_tac 2);
+by (asm_simp_tac (simpset() addsimps [add_le_mono1]) 1);
+qed "bound_mult_zero";
+
+Goalw [UP_def]
+ "!! f g. [| f : UP; g : UP |] ==> \
+\ (%n. (SUM n (%i. f i * g (n-i))::'a::ring)) : UP";
+by (Step_tac 1);
+(* Instantiate bound for the product, and remove bound in goal *)
+by (res_inst_tac [("x", "n + na")] exI 1);
+by (Step_tac 1);
+(* Show that the sum is 0 *)
+by (asm_simp_tac (simpset() addsimps [bound_mult_zero]) 1);
+qed "UP_closed_mult";
+
+(* %x. <0> represents a polynomial *)
+
+Goalw [UP_def] "(%x. <0>) : UP";
+by (Fast_tac 1);
+qed "UP_zero";
+
+(* Effect of +, *s, monom, * and the other operations on the coefficients *)
+
+Goalw [coeff_def, up_add_def]
+ "coeff n (p+q) = (coeff n p + coeff n q::'a::ring)";
+by (asm_simp_tac (simpset() addsimps [Abs_UP_inverse, UP_closed_add, Rep_UP]) 1);
+qed "coeff_add";
+
+Goalw [coeff_def, up_smult_def]
+ "!!a::'a::ring. coeff n (a *s p) = a * coeff n p";
+by (asm_simp_tac (simpset() addsimps [Abs_UP_inverse, UP_closed_smult, Rep_UP]) 1);
+qed "coeff_smult";
+
+Goalw [coeff_def, monom_def]
+ "coeff n (monom m) = (if m=n then <1> else <0>)";
+by (asm_simp_tac (simpset() addsimps [Abs_UP_inverse, UP_closed_monom, Rep_UP]) 1);
+qed "coeff_monom";
+
+Goalw [coeff_def, const_def]
+ "coeff n (const a) = (if n=0 then a else <0>)";
+by (asm_simp_tac (simpset() addsimps [Abs_UP_inverse, UP_closed_const, Rep_UP]) 1);
+qed "coeff_const";
+
+Goalw [coeff_def, up_mult_def]
+ "coeff n (p * q) = (SUM n (%i. coeff i p * coeff (n-i) q)::'a::ring)";
+by (asm_simp_tac (simpset() addsimps [Abs_UP_inverse, UP_closed_mult, Rep_UP]) 1);
+qed "coeff_mult";
+
+Goalw [coeff_def, up_zero_def] "coeff n <0> = <0>";
+by (asm_simp_tac (simpset() addsimps [Abs_UP_inverse, UP_zero, Rep_UP]) 1);
+qed "coeff_zero";
+
+Addsimps [coeff_add, coeff_smult, coeff_monom, coeff_const,
+ coeff_mult, coeff_zero];
+
+Goalw [up_one_def]
+ "coeff n <1> = (if n=0 then <1> else <0>)";
+by (Simp_tac 1);
+qed "coeff_one";
+
+Goalw [up_uminus_def] "coeff n (-p) = (-coeff n p::'a::ring)";
+by (simp_tac (simpset() addsimps m_minus) 1);
+qed "coeff_uminus";
+
+Addsimps [coeff_one, coeff_uminus];
+
+(* Polynomials form a ring *)
+
+Goalw [coeff_def]
+ "!! p q. [| !! n. coeff n p = coeff n q |] ==> p = q";
+by (res_inst_tac [("t", "p")] (Rep_UP_inverse RS subst) 1);
+by (res_inst_tac [("t", "q")] (Rep_UP_inverse RS subst) 1);
+by (Asm_simp_tac 1);
+qed "up_eqI";
+
+Goalw [coeff_def]
+ "!! p q. coeff n p ~= coeff n q ==> p ~= q";
+by (etac contrapos 1);
+by (Asm_simp_tac 1);
+qed "up_neqI";
+
+Goal "!! a::('a::ring) up. (a + b) + c = a + (b + c)";
+by (rtac up_eqI 1);
+by (Simp_tac 1);
+by (rtac a_assoc 1);
+qed "up_a_assoc";
+
+Goal "!! a::('a::ring) up. <0> + a = a";
+by (rtac up_eqI 1);
+by (Simp_tac 1);
+qed "up_l_zero";
+
+Goal "!! a::('a::ring) up. (-a) + a = <0>";
+by (rtac up_eqI 1);
+by (Simp_tac 1);
+qed "up_l_neg";
+
+Goal "!! a::('a::ring) up. a + b = b + a";
+by (rtac up_eqI 1);
+by (Simp_tac 1);
+by (rtac a_comm 1);
+qed "up_a_comm";
+
+Goal "!! a::('a::ring) up. (a * b) * c = a * (b * c)";
+by (rtac up_eqI 1);
+by (Simp_tac 1);
+by (rtac poly_assoc_lemma 1);
+qed "up_m_assoc";
+
+Goal "!! a::('a::ring) up. <1> * a = a";
+by (rtac up_eqI 1);
+by (Simp_tac 1);
+by (nat_ind_tac "n" 1); (* this is only a case split *)
+(* Base case *)
+by (Simp_tac 1);
+(* Induction step *)
+by (simp_tac (simpset() delsimps [SUM_Suc] addsimps [SUM_Suc2]) 1);
+qed "up_l_one";
+
+Goal "!! a::('a::ring) up. (a + b) * c = a * c + b * c";
+by (rtac up_eqI 1);
+by (simp_tac (simpset() addsimps [l_distr, SUM_add]) 1);
+qed "up_l_distr";
+
+Goal "!! a::('a::ring) up. a * b = b * a";
+by (rtac up_eqI 1);
+by (cut_inst_tac [("a", "%i. coeff i a"), ("b", "%i. coeff i b")]
+ poly_comm_lemma 1);
+by (asm_full_simp_tac (simpset() addsimps [m_comm]) 1);
+qed "up_m_comm";
+
+Goal "<1> ~= (<0>::('a::ring) up)";
+by (res_inst_tac [("n", "0")] up_neqI 1);
+by (Simp_tac 1);
+qed "up_one_not_zero";
+
+(* Further algebraic rules *)
+
+Goal "!! a::'a::ring. const a * p = a *s p";
+by (rtac up_eqI 1);
+by (nat_ind_tac "n" 1); (* really only a case split *)
+by (Simp_tac 1);
+by (simp_tac (simpset() delsimps [SUM_Suc] addsimps [SUM_Suc2]) 1);
+qed "const_mult_is_smult";
+
+Goal "!! a::'a::ring. const (a + b) = const a + const b";
+by (rtac up_eqI 1);
+by (simp_tac (simpset() setloop (split_tac [expand_if])) 1);
+qed "const_add";
+
+Goal "!! a::'a::ring. const (a * b) = const a * const b";
+by (simp_tac (simpset() addsimps [const_mult_is_smult]) 1);
+by (rtac up_eqI 1);
+by (simp_tac (simpset() setloop (split_tac [expand_if])) 1);
+qed "const_mult";
+
+Goal "const (<1>::'a::ring) = <1>";
+by (rtac up_eqI 1);
+by (Simp_tac 1);
+qed "const_one";
+
+Goal "const (<0>::'a::ring) = <0>";
+by (rtac up_eqI 1);
+by (simp_tac (simpset() setloop (split_tac [expand_if])) 1);
+qed "const_zero";
+
+Addsimps [const_add, const_mult, const_one, const_zero];
+
+Goalw [inj_on_def, UNIV_def, const_def] "inj const";
+by (Simp_tac 1);
+by (strip_tac 1);
+by (dres_inst_tac [("f", "Rep_UP")] arg_cong 1);
+by (full_simp_tac (simpset() addsimps [Abs_UP_inverse, UP_closed_const,
+ expand_fun_eq]) 1);
+by (dres_inst_tac [("x", "0")] spec 1);
+by (Full_simp_tac 1);
+qed "const_inj";
+
+(*Lemma used in PolyHomo*)
+Goal
+ "!! f::nat=>'a::ring. [| bound n f; bound m g|] ==> \
+\ SUM (n + m) (%k. SUM k (%i. f i * g (k-i))) = SUM n f * SUM m g";
+by (simp_tac (simpset() addsimps [SUM_ldistr, DiagSum]) 1);
+(* SUM_rdistr must be applied after SUM_ldistr ! *)
+by (simp_tac (simpset() addsimps [SUM_rdistr]) 1);
+by (res_inst_tac [("m", "n"), ("n", "n+m")] SUM_extend 1);
+by (rtac le_add1 1);
+by (SELECT_GOAL Auto_tac 1);
+by (rtac SUM_cong 1);
+by (rtac refl 1);
+by (res_inst_tac [("m", "m"), ("n", "n+m-i")] SUM_shrink 1);
+by (asm_simp_tac (simpset() addsimps [le_add_diff]) 1);
+by (SELECT_GOAL Auto_tac 1);
+by (rtac refl 1);
+qed "CauchySum";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/poly/UnivPoly.thy Fri Nov 05 11:14:26 1999 +0100
@@ -0,0 +1,42 @@
+(*
+ Univariate Polynomials
+ $Id$
+ Author: Clemens Ballarin, started 9 December 1996
+*)
+
+UnivPoly = ProtoPoly +
+
+typedef (UP)
+ ('a) up = "{f :: nat => 'a::ringS. EX n. bound n f}" (UP_witness)
+
+instance
+ up :: (ringS) ringS
+
+consts
+ coeff :: [nat, 'a up] => 'a::ringS
+ "*s" :: ['a::ringS, 'a up] => 'a up (infixl 70)
+ monom :: nat => ('a::ringS) up
+ const :: 'a::ringS => 'a up
+
+ "*X^" :: ['a, nat] => 'a up ("(3_*X^/_)" [71, 71] 70)
+
+translations
+ "a *X^ n" == "a *s monom n"
+ (* this translation is only nice for non-nested polynomials *)
+
+defs
+ coeff_def "coeff n p == Rep_UP p n"
+ up_add_def "p + q == Abs_UP (%n. Rep_UP p n + Rep_UP q n)"
+ up_smult_def "a *s p == Abs_UP (%n. a * Rep_UP p n)"
+ monom_def "monom m == Abs_UP (%n. if m=n then <1> else <0>)"
+ const_def "const a == Abs_UP (%n. if n=0 then a else <0>)"
+ up_mult_def "p * q == Abs_UP (%n. SUM n
+ (%i. Rep_UP p i * Rep_UP q (n-i)))"
+
+ up_zero_def "<0> == Abs_UP (%x. <0>)"
+ up_one_def "<1> == monom 0"
+ up_uminus_def "- p == (-<1>) *s p"
+ up_power_def "a ^ n == nat_rec (<1>::('a::ringS) up) (%u b. b * a) n"
+end
+
+