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: + +
+ 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 ++ + Also, some facts about ring homomorphisms and ideals are mechanised. + +
Polynomials: + Polynomials have a natural, mathematical representation. Facts about + the following topics are provided: + +
+ +Still missing are + Polynomials over a factorial domain form a factorial domain + (difficult), and polynomials over a field form a pid. + +
[Jacobson1985] Nathan Jacobson, Basic Algebra I, Freeman, 1985. + +
[Ballarin1999] Clemens Ballarin, Computer Algebra and Theorem Proving, + Author's PhD thesis, 1999. + +
Last modified on $Date$ + +
+Clemens Ballarin. Karlsruhe, October 1999 + +ballarin@ira.uka.de +
+ diff -r a1fb91eb9b4d -r 3d0c34795831 src/HOL/Algebra/ROOT.ML --- /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*) diff -r a1fb91eb9b4d -r 3d0c34795831 src/HOL/Algebra/abstract/Abstract.thy --- /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 diff -r a1fb91eb9b4d -r 3d0c34795831 src/HOL/Algebra/abstract/Factor.ML --- /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"; + diff -r a1fb91eb9b4d -r 3d0c34795831 src/HOL/Algebra/abstract/Factor.thy --- /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 diff -r a1fb91eb9b4d -r 3d0c34795831 src/HOL/Algebra/abstract/Field.thy --- /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 diff -r a1fb91eb9b4d -r 3d0c34795831 src/HOL/Algebra/abstract/Ideal.ML --- /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"; + diff -r a1fb91eb9b4d -r 3d0c34795831 src/HOL/Algebra/abstract/Ideal.thy --- /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 diff -r a1fb91eb9b4d -r 3d0c34795831 src/HOL/Algebra/abstract/NatSum.ML --- /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"; + + + + diff -r a1fb91eb9b4d -r 3d0c34795831 src/HOL/Algebra/abstract/NatSum.thy --- /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 diff -r a1fb91eb9b4d -r 3d0c34795831 src/HOL/Algebra/abstract/PID.thy --- /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 + diff -r a1fb91eb9b4d -r 3d0c34795831 src/HOL/Algebra/abstract/Ring.ML --- /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"; + + + diff -r a1fb91eb9b4d -r 3d0c34795831 src/HOL/Algebra/abstract/Ring.thy --- /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 diff -r a1fb91eb9b4d -r 3d0c34795831 src/HOL/Algebra/abstract/RingHomo.ML --- /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]; diff -r a1fb91eb9b4d -r 3d0c34795831 src/HOL/Algebra/abstract/RingHomo.thy --- /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 diff -r a1fb91eb9b4d -r 3d0c34795831 src/HOL/Algebra/poly/Degree.ML --- /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"; diff -r a1fb91eb9b4d -r 3d0c34795831 src/HOL/Algebra/poly/Degree.thy --- /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 diff -r a1fb91eb9b4d -r 3d0c34795831 src/HOL/Algebra/poly/LongDiv.ML --- /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"; diff -r a1fb91eb9b4d -r 3d0c34795831 src/HOL/Algebra/poly/LongDiv.thy --- /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 + diff -r a1fb91eb9b4d -r 3d0c34795831 src/HOL/Algebra/poly/PolyHomo.ML --- /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(); + diff -r a1fb91eb9b4d -r 3d0c34795831 src/HOL/Algebra/poly/PolyHomo.thy --- /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 diff -r a1fb91eb9b4d -r 3d0c34795831 src/HOL/Algebra/poly/PolyRing.ML --- /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]; diff -r a1fb91eb9b4d -r 3d0c34795831 src/HOL/Algebra/poly/PolyRing.thy --- /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 diff -r a1fb91eb9b4d -r 3d0c34795831 src/HOL/Algebra/poly/Polynomial.thy --- /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 + + + + diff -r a1fb91eb9b4d -r 3d0c34795831 src/HOL/Algebra/poly/ProtoPoly.ML --- /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"; diff -r a1fb91eb9b4d -r 3d0c34795831 src/HOL/Algebra/poly/ProtoPoly.thy --- /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 f i = <0>" + +end diff -r a1fb91eb9b4d -r 3d0c34795831 src/HOL/Algebra/poly/UnivPoly.ML --- /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