1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Algebra/README.html Fri Nov 05 11:14:26 1999 +0100
1.3 @@ -0,0 +1,59 @@
1.4 +<!-- $Id$ -->
1.5 +<HTML><HEAD><TITLE>HOL/Algebra/README.html</TITLE></HEAD><BODY>
1.6 +
1.7 +<H2>Algebra: Theories of Rings and Polynomials</H2>
1.8 +
1.9 +<P>This development of univariate polynomials is separated into an
1.10 +abstract development of rings and the development of polynomials
1.11 +itself. The formalisation is based on [Jacobson1985], and polynomials
1.12 +have a sparse, mathematical representation. These theories were
1.13 +developed as a base for the integration of a computer algebra system
1.14 +to Isabelle [Ballarin1999], and was designed to match implementations
1.15 +of these domains in some typed computer algebra systems. Summary:
1.16 +
1.17 +<P><EM>Rings:</EM>
1.18 + Classes of rings are represented by axiomatic type classes. The
1.19 + following are available:
1.20 +
1.21 +<PRE>
1.22 + ringS: Syntactic class
1.23 + ring: Commutative rings with one (including a summation
1.24 + operator, which is needed for the polynomials)
1.25 + domain: Integral domains
1.26 + factorial: Factorial domains (divisor chain condition is missing)
1.27 + pid: Principal ideal domains
1.28 + field: Fields
1.29 +</PRE>
1.30 +
1.31 + Also, some facts about ring homomorphisms and ideals are mechanised.
1.32 +
1.33 +<P><EM>Polynomials:</EM>
1.34 + Polynomials have a natural, mathematical representation. Facts about
1.35 + the following topics are provided:
1.36 +
1.37 +<MENU>
1.38 +<LI>Degree function
1.39 +<LI> Universal Property, evaluation homomorphism
1.40 +<LI>Long division (existence and uniqueness)
1.41 +<LI>Polynomials over a ring form a ring
1.42 +<LI>Polynomials over an integral domain form an integral domain
1.43 +</MENU>
1.44 +
1.45 + <P>Still missing are
1.46 + Polynomials over a factorial domain form a factorial domain
1.47 + (difficult), and polynomials over a field form a pid.
1.48 +
1.49 +<P>[Jacobson1985] Nathan Jacobson, Basic Algebra I, Freeman, 1985.
1.50 +
1.51 +<P>[Ballarin1999] Clemens Ballarin, Computer Algebra and Theorem Proving,
1.52 + Author's <A HREF="http://iaks-www.ira.uka.de/iaks-calmet/ballarin/publications.html">PhD thesis</A>, 1999.
1.53 +
1.54 +<HR>
1.55 +<P>Last modified on $Date$
1.56 +
1.57 +<ADDRESS>
1.58 +<P><A HREF="http://iaks-www.ira.uka.de/iaks-calmet/ballarin">Clemens Ballarin</A>. Karlsruhe, October 1999
1.59 +
1.60 +<A NAME="ballarin@ira.uka.de" HREF="mailto:ballarin@ira.uka.de">ballarin@ira.uka.de</A>
1.61 +</ADDRESS>
1.62 +</BODY></HTML>
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/HOL/Algebra/ROOT.ML Fri Nov 05 11:14:26 1999 +0100
2.3 @@ -0,0 +1,11 @@
2.4 +(*
2.5 + Polynomials
2.6 + $Id$
2.7 + Author: Clemens Ballarin, started 24 September 1999
2.8 +*)
2.9 +
2.10 +add_path "abstract";
2.11 +add_path "poly";
2.12 +
2.13 +use_thy "Abstract"; (*The ring theory*)
2.14 +use_thy "Polynomial"; (*The full theory*)
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/HOL/Algebra/abstract/Abstract.thy Fri Nov 05 11:14:26 1999 +0100
3.3 @@ -0,0 +1,7 @@
3.4 +(*
3.5 + Summary theory of the development of abstract algebra
3.6 + $Id$
3.7 + Author: Clemens Ballarin, started 17 July 1997
3.8 +*)
3.9 +
3.10 +Abstract = RingHomo + Field
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/HOL/Algebra/abstract/Factor.ML Fri Nov 05 11:14:26 1999 +0100
4.3 @@ -0,0 +1,49 @@
4.4 +(*
4.5 + Factorisation within a factorial domain
4.6 + $Id$
4.7 + Author: Clemens Ballarin, started 25 November 1997
4.8 +*)
4.9 +
4.10 +open Factor;
4.11 +
4.12 +goalw Ring.thy [assoc_def] "!! c::'a::factorial. \
4.13 +\ [| irred c; irred a; irred b; c dvd (a*b) |] ==> c assoc a | c assoc b";
4.14 +by (ftac factorial_prime 1);
4.15 +by (rewrite_goals_tac [irred_def, prime_def]);
4.16 +by (Blast_tac 1);
4.17 +qed "irred_dvd_lemma";
4.18 +
4.19 +goalw Ring.thy [assoc_def] "!! c::'a::factorial. \
4.20 +\ [| irred c; a dvd <1> |] ==> \
4.21 +\ (ALL b : set factors. irred b) & c dvd foldr op* factors a --> \
4.22 +\ (EX d. c assoc d & d : set factors)";
4.23 +by (induct_tac "factors" 1);
4.24 +(* Base case: c dvd a contradicts irred c *)
4.25 +by (full_simp_tac (simpset() addsimps [irred_def]) 1);
4.26 +by (blast_tac (claset() addIs [dvd_trans_ring]) 1);
4.27 +(* Induction step *)
4.28 +by (ftac factorial_prime 1);
4.29 +by (full_simp_tac (simpset() addsimps [irred_def, prime_def]) 1);
4.30 +by (Blast_tac 1);
4.31 +qed "irred_dvd_list_lemma";
4.32 +
4.33 +goal Ring.thy "!! c::'a::factorial. \
4.34 +\ [| irred c; ALL b : set factors. irred b; a dvd <1>; \
4.35 +\ c dvd foldr op* factors a |] ==> \
4.36 +\ EX d. c assoc d & d : set factors";
4.37 +by (rtac (irred_dvd_list_lemma RS mp) 1);
4.38 +by (Auto_tac);
4.39 +qed "irred_dvd_list";
4.40 +
4.41 +Goalw [Factorisation_def] "!! c::'a::factorial. \
4.42 +\ [| irred c; Factorisation x factors u; c dvd x |] ==> \
4.43 +\ EX d. c assoc d & d : set factors";
4.44 +by (rtac (irred_dvd_list_lemma RS mp) 1);
4.45 +by (Auto_tac);
4.46 +qed "Factorisation_dvd";
4.47 +
4.48 +Goalw [Factorisation_def] "!! c::'a::factorial. \
4.49 +\ [| Factorisation x factors u; a : set factors |] ==> irred a";
4.50 +by (Blast_tac 1);
4.51 +qed "Factorisation_irred";
4.52 +
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/HOL/Algebra/abstract/Factor.thy Fri Nov 05 11:14:26 1999 +0100
5.3 @@ -0,0 +1,18 @@
5.4 +(*
5.5 + Factorisation within a factorial domain
5.6 + $Id$
5.7 + Author: Clemens Ballarin, started 25 November 1997
5.8 +*)
5.9 +
5.10 +Factor = Ring +
5.11 +
5.12 +consts
5.13 + Factorisation :: ['a::ringS, 'a list, 'a] => bool
5.14 + (* factorisation of x into a list of irred factors and a unit u *)
5.15 +
5.16 +defs
5.17 + Factorisation_def "Factorisation x factors u ==
5.18 + x = foldr op* factors u &
5.19 + (ALL a : set factors. irred a) & u dvd <1>"
5.20 +
5.21 +end
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/HOL/Algebra/abstract/Field.thy Fri Nov 05 11:14:26 1999 +0100
6.3 @@ -0,0 +1,15 @@
6.4 +(*
6.5 + Properties of abstract class field
6.6 + $Id$
6.7 + Author: Clemens Ballarin, started 15 November 1997
6.8 +*)
6.9 +
6.10 +Field = Factor + Ideal +
6.11 +
6.12 +instance
6.13 + field < domain (field_integral)
6.14 +
6.15 +instance
6.16 + field < factorial (TrueI, field_fact_prime)
6.17 +
6.18 +end
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/HOL/Algebra/abstract/Ideal.ML Fri Nov 05 11:14:26 1999 +0100
7.3 @@ -0,0 +1,322 @@
7.4 +(*
7.5 + Ideals for commutative rings
7.6 + $Id$
7.7 + Author: Clemens Ballarin, started 24 September 1999
7.8 +*)
7.9 +
7.10 +(* is_ideal *)
7.11 +
7.12 +Goalw [is_ideal_def]
7.13 + "!! I. [| !! a b. [| a:I; b:I |] ==> a + b : I; \
7.14 +\ !! a. a:I ==> - a : I; <0> : I; \
7.15 +\ !! a r. a:I ==> a * r : I |] ==> is_ideal I";
7.16 +by Auto_tac;
7.17 +qed "is_idealI";
7.18 +
7.19 +Goalw [is_ideal_def] "[| is_ideal I; a:I; b:I |] ==> a + b : I";
7.20 +by (Fast_tac 1);
7.21 +qed "is_ideal_add";
7.22 +
7.23 +Goalw [is_ideal_def] "[| is_ideal I; a:I |] ==> - a : I";
7.24 +by (Fast_tac 1);
7.25 +qed "is_ideal_uminus";
7.26 +
7.27 +Goalw [is_ideal_def] "[| is_ideal I |] ==> <0> : I";
7.28 +by (Fast_tac 1);
7.29 +qed "is_ideal_zero";
7.30 +
7.31 +Goalw [is_ideal_def] "[| is_ideal I; a:I |] ==> a * r : I";
7.32 +by (Fast_tac 1);
7.33 +qed "is_ideal_mult";
7.34 +
7.35 +Goalw [dvd_def, is_ideal_def] "[| a dvd b; is_ideal I; a:I |] ==> b:I";
7.36 +by (Fast_tac 1);
7.37 +qed "is_ideal_dvd";
7.38 +
7.39 +Goalw [is_ideal_def] "is_ideal (UNIV::('a::ring) set)";
7.40 +by Auto_tac;
7.41 +qed "UNIV_is_ideal";
7.42 +
7.43 +Goalw [is_ideal_def] "is_ideal {<0>::'a::ring}";
7.44 +by Auto_tac;
7.45 +qed "zero_is_ideal";
7.46 +
7.47 +Addsimps [is_ideal_add, is_ideal_uminus, is_ideal_zero, is_ideal_mult,
7.48 + UNIV_is_ideal, zero_is_ideal];
7.49 +
7.50 +Goal "is_ideal {x::'a::ring. a dvd x}";
7.51 +by (rtac is_idealI 1);
7.52 +by Auto_tac;
7.53 +qed "is_ideal_1";
7.54 +
7.55 +Goal "is_ideal {x::'a::ring. EX u v. x = a * u + b * v}";
7.56 +by (rtac is_idealI 1);
7.57 +by Auto_tac;
7.58 +by (res_inst_tac [("x", "u+ua")] exI 1);
7.59 +by (res_inst_tac [("x", "v+va")] exI 1);
7.60 +by (res_inst_tac [("x", "-u")] exI 2);
7.61 +by (res_inst_tac [("x", "-v")] exI 2);
7.62 +by (res_inst_tac [("x", "<0>")] exI 3);
7.63 +by (res_inst_tac [("x", "<0>")] exI 3);
7.64 +by (res_inst_tac [("x", "u * r")] exI 4);
7.65 +by (res_inst_tac [("x", "v * r")] exI 4);
7.66 +by (REPEAT (simp_tac (simpset() addsimps [r_distr, l_distr, r_minus, minus_add, m_assoc]@a_ac) 1));
7.67 +qed "is_ideal_2";
7.68 +
7.69 +(* ideal_of *)
7.70 +
7.71 +Goalw [is_ideal_def, ideal_of_def] "is_ideal (ideal_of S)";
7.72 +by (Blast_tac 1); (* Here, blast_tac is much superior to fast_tac! *)
7.73 +qed "ideal_of_is_ideal";
7.74 +
7.75 +Goalw [ideal_of_def] "a:S ==> a : (ideal_of S)";
7.76 +by Auto_tac;
7.77 +qed "generator_in_ideal";
7.78 +
7.79 +Goalw [ideal_of_def] "ideal_of {<1>::'a::ring} = UNIV";
7.80 +by (auto_tac (claset() addSDs [is_ideal_mult], simpset()));
7.81 + (* loops if is_ideal_mult is added as non-safe rule *)
7.82 +qed "ideal_of_one_eq";
7.83 +
7.84 +Goalw [ideal_of_def] "ideal_of {} = {<0>::'a::ring}";
7.85 +by (rtac subset_antisym 1);
7.86 +by (rtac subsetI 1);
7.87 +by (dtac InterD 1);
7.88 +by (assume_tac 2);
7.89 +by (auto_tac (claset(), simpset() addsimps [is_ideal_zero]));
7.90 +qed "ideal_of_empty_eq";
7.91 +
7.92 +Goalw [ideal_of_def] "ideal_of {a} = {x::'a::ring. a dvd x}";
7.93 +by (rtac subset_antisym 1);
7.94 +by (rtac subsetI 1);
7.95 +by (dtac InterD 1);
7.96 +by (assume_tac 2);
7.97 +by (auto_tac (claset() addIs [is_ideal_1], simpset()));
7.98 +by (asm_simp_tac (simpset() addsimps [is_ideal_dvd]) 1);
7.99 +qed "pideal_structure";
7.100 +
7.101 +Goalw [ideal_of_def]
7.102 + "ideal_of {a, b} = {x::'a::ring. EX u v. x = a * u + b * v}";
7.103 +by (rtac subset_antisym 1);
7.104 +by (rtac subsetI 1);
7.105 +by (dtac InterD 1);
7.106 +by (assume_tac 2);
7.107 +by (auto_tac (claset() addIs [is_ideal_2], simpset()));
7.108 +by (res_inst_tac [("x", "<1>")] exI 1);
7.109 +by (res_inst_tac [("x", "<0>")] exI 1);
7.110 +by (res_inst_tac [("x", "<0>")] exI 2);
7.111 +by (res_inst_tac [("x", "<1>")] exI 2);
7.112 +by (Simp_tac 1);
7.113 +by (Simp_tac 1);
7.114 +qed "ideal_of_2_structure";
7.115 +
7.116 +Goalw [ideal_of_def] "A <= B ==> ideal_of A <= ideal_of B";
7.117 +by Auto_tac;
7.118 +qed "ideal_of_mono";
7.119 +
7.120 +Goal "ideal_of {<0>::'a::ring} = {<0>}";
7.121 +by (simp_tac (simpset() addsimps [pideal_structure]) 1);
7.122 +by (rtac subset_antisym 1);
7.123 +by (auto_tac (claset() addIs [dvd_zero_left], simpset()));
7.124 +qed "ideal_of_zero_eq";
7.125 +
7.126 +Goal "[| is_ideal I; a : I |] ==> ideal_of {a::'a::ring} <= I";
7.127 +by (auto_tac (claset(),
7.128 + simpset() addsimps [pideal_structure, is_ideal_dvd]));
7.129 +qed "element_generates_subideal";
7.130 +
7.131 +(* is_pideal *)
7.132 +
7.133 +Goalw [is_pideal_def] "is_pideal (I::('a::ring) set) ==> is_ideal I";
7.134 +by (fast_tac (claset() addIs [ideal_of_is_ideal]) 1);
7.135 +qed "is_pideal_imp_is_ideal";
7.136 +
7.137 +Goalw [is_pideal_def] "is_pideal (ideal_of {a::'a::ring})";
7.138 +by (Fast_tac 1);
7.139 +qed "pideal_is_pideal";
7.140 +
7.141 +Goalw [is_pideal_def] "is_pideal I ==> EX a. I = ideal_of {a}";
7.142 +by (assume_tac 1);
7.143 +qed "is_pidealD";
7.144 +
7.145 +(* Ideals and divisibility *)
7.146 +
7.147 +Goal "b dvd a ==> ideal_of {a::'a::ring} <= ideal_of {b}";
7.148 +by (auto_tac (claset() addIs [dvd_trans_ring],
7.149 + simpset() addsimps [pideal_structure]));
7.150 +qed "dvd_imp_subideal";
7.151 +
7.152 +Goal "ideal_of {a::'a::ring} <= ideal_of {b} ==> b dvd a";
7.153 +by (auto_tac (claset() addSDs [subsetD],
7.154 + simpset() addsimps [pideal_structure]));
7.155 +qed "subideal_imp_dvd";
7.156 +
7.157 +Goal "(ideal_of {a::'a::ring} <= ideal_of {b}) = b dvd a";
7.158 +by (rtac iffI 1);
7.159 +by (REPEAT (ares_tac [subideal_imp_dvd, dvd_imp_subideal] 1));
7.160 +qed "subideal_is_dvd";
7.161 +
7.162 +Goal "(ideal_of {a::'a::ring} < ideal_of {b}) ==> ~ (a dvd b)";
7.163 +by (full_simp_tac (simpset() addsimps [psubset_eq, pideal_structure]) 1);
7.164 +by (etac conjE 1);
7.165 +by (dres_inst_tac [("c", "a")] subsetD 1);
7.166 +by (auto_tac (claset() addIs [dvd_trans_ring],
7.167 + simpset()));
7.168 +qed "psubideal_not_dvd";
7.169 +
7.170 +Goal "[| b dvd a; ~ (a dvd b) |] ==> ideal_of {a::'a::ring} < ideal_of {b}";
7.171 +by (rtac psubsetI 1);
7.172 +by (rtac dvd_imp_subideal 1 THEN atac 1);
7.173 +by (rtac contrapos 1); by (assume_tac 1);
7.174 +by (rtac subideal_imp_dvd 1);
7.175 +by (Asm_simp_tac 1);
7.176 +qed "not_dvd_psubideal";
7.177 +
7.178 +Goal "(ideal_of {a::'a::ring} < ideal_of {b}) = (b dvd a & ~ (a dvd b))";
7.179 +by (rtac iffI 1);
7.180 +by (REPEAT (ares_tac
7.181 + [conjI, psubideal_not_dvd, psubset_imp_subset RS subideal_imp_dvd] 1));
7.182 +by (etac conjE 1);
7.183 +by (REPEAT (ares_tac [not_dvd_psubideal] 1));
7.184 +qed "psubideal_is_dvd";
7.185 +
7.186 +Goal "[| a dvd b; b dvd a |] ==> ideal_of {a::'a::ring} = ideal_of {b}";
7.187 +by (rtac subset_antisym 1);
7.188 +by (REPEAT (ares_tac [dvd_imp_subideal] 1));
7.189 +qed "assoc_pideal_eq";
7.190 +
7.191 +AddIffs [subideal_is_dvd, psubideal_is_dvd];
7.192 +
7.193 +Goal "!!a::'a::ring. a dvd b ==> b : (ideal_of {a})";
7.194 +by (rtac is_ideal_dvd 1);
7.195 +by (assume_tac 1);
7.196 +by (rtac ideal_of_is_ideal 1);
7.197 +by (rtac generator_in_ideal 1);
7.198 +by (Simp_tac 1);
7.199 +qed "dvd_imp_in_pideal";
7.200 +
7.201 +Goal "!!a::'a::ring. b : (ideal_of {a}) ==> a dvd b";
7.202 +by (full_simp_tac (simpset() addsimps [pideal_structure]) 1);
7.203 +qed "in_pideal_imp_dvd";
7.204 +
7.205 +Goal "~ (a dvd b) ==> ideal_of {a::'a::ring} < ideal_of {a, b}";
7.206 +by (asm_simp_tac (simpset() addsimps [psubset_eq, ideal_of_mono]) 1);
7.207 +by (simp_tac (simpset() addsimps [ideal_of_2_structure]) 1);
7.208 +by (etac contrapos 1);
7.209 +by (rtac in_pideal_imp_dvd 1);
7.210 +by (Asm_simp_tac 1);
7.211 +by (res_inst_tac [("x", "<0>")] exI 1);
7.212 +by (res_inst_tac [("x", "<1>")] exI 1);
7.213 +by (Simp_tac 1);
7.214 +qed "not_dvd_psubideal";
7.215 +
7.216 +Goalw [irred_def]
7.217 + "[| irred (a::'a::ring); is_pideal I; ideal_of {a} < I |] ==> x : I";
7.218 +by (dtac is_pidealD 1);
7.219 +by (etac exE 1);
7.220 +by (Clarify_tac 1);
7.221 +by (eres_inst_tac [("x", "aa")] allE 1);
7.222 +by (Clarify_tac 1);
7.223 +by (dres_inst_tac [("a", "<1>")] dvd_imp_subideal 1);
7.224 +by (auto_tac (claset(), simpset() addsimps [ideal_of_one_eq]));
7.225 +qed "irred_imp_max_ideal";
7.226 +
7.227 +(* Pid are factorial *)
7.228 +
7.229 +(* Divisor chain condition *)
7.230 +(* proofs not finished *)
7.231 +
7.232 +Goal "(ALL i. I i <= I (Suc i)) --> (n <= m & a : I n --> a : I m)";
7.233 +by (rtac impI 1);
7.234 +by (nat_ind_tac "m" 1);
7.235 +by (Blast_tac 1);
7.236 +(* induction step *)
7.237 +by (case_tac "n <= m" 1);
7.238 +by Auto_tac;
7.239 +by (subgoal_tac "n = Suc m" 1);
7.240 +by (hyp_subst_tac 1);
7.241 +by Auto_tac;
7.242 +qed "subset_chain_lemma";
7.243 +
7.244 +Goal "[| ALL i. is_ideal (I i); ALL i. I i <= I (Suc i) |] ==> \
7.245 +\ is_ideal (Union (I``UNIV))";
7.246 +by (rtac is_idealI 1);
7.247 +by Auto_tac;
7.248 +by (res_inst_tac [("x", "max x xa")] exI 1);
7.249 +by (rtac is_ideal_add 1);
7.250 +by (Asm_simp_tac 1);
7.251 +by (rtac (subset_chain_lemma RS mp RS mp) 1);
7.252 +by (assume_tac 1);
7.253 +by (rtac conjI 1);
7.254 +by (assume_tac 2);
7.255 +by (arith_tac 1);
7.256 +by (rtac (subset_chain_lemma RS mp RS mp) 1);
7.257 +by (assume_tac 1);
7.258 +by (rtac conjI 1);
7.259 +by (assume_tac 2);
7.260 +by (arith_tac 1);
7.261 +by (res_inst_tac [("x", "x")] exI 1);
7.262 +by (Asm_simp_tac 1);
7.263 +by (res_inst_tac [("x", "x")] exI 1);
7.264 +by (Asm_simp_tac 1);
7.265 +qed "chain_is_ideal";
7.266 +
7.267 +(*
7.268 +Goal "ALL i. ideal_of {a i} < ideal_of {a (Suc i)} ==> \
7.269 +\ EX n. Union ((ideal_of o (%a. {a}))``UNIV) = ideal_of {a n}";
7.270 +
7.271 +Goal "wf {(a::'a::pid, b). a dvd b & ~ (b dvd a)}";
7.272 +by (simp_tac (simpset()
7.273 + addsimps [psubideal_is_dvd RS sym, wf_iff_no_infinite_down_chain]
7.274 + delsimps [psubideal_is_dvd]) 1);
7.275 +*)
7.276 +
7.277 +(* Primeness condition *)
7.278 +
7.279 +Goalw [prime_def] "irred a ==> prime (a::'a::pid)";
7.280 +by (rtac conjI 1);
7.281 +by (rtac conjI 2);
7.282 +by (Clarify_tac 3);
7.283 +by (dres_inst_tac [("I", "ideal_of {a, b}"), ("x", "<1>")]
7.284 + irred_imp_max_ideal 3);
7.285 +by (auto_tac (claset() addIs [ideal_of_is_ideal, pid_ax],
7.286 + simpset() addsimps [irred_def, not_dvd_psubideal, pid_ax]));
7.287 +by (full_simp_tac (simpset() addsimps [ideal_of_2_structure]) 1);
7.288 +by (Clarify_tac 1);
7.289 +by (dres_inst_tac [("f", "op* aa")] arg_cong 1);
7.290 +by (full_simp_tac (simpset() addsimps [r_distr]) 1);
7.291 +by (etac ssubst 1);
7.292 +by (asm_simp_tac (simpset() addsimps [m_assoc RS sym]) 1);
7.293 +qed "pid_irred_imp_prime";
7.294 +
7.295 +(* Fields are Pid *)
7.296 +
7.297 +Goal "a ~= <0> ==> ideal_of {a::'a::field} = UNIV";
7.298 +by (rtac subset_antisym 1);
7.299 +by (Simp_tac 1);
7.300 +by (rtac subset_trans 1);
7.301 +by (rtac dvd_imp_subideal 2);
7.302 +by (rtac field_ax 2);
7.303 +by (assume_tac 2);
7.304 +by (simp_tac (simpset() addsimps [ideal_of_one_eq]) 1);
7.305 +qed "field_pideal_univ";
7.306 +
7.307 +Goal "[| is_ideal I; I ~= {<0>} |] ==> {<0>} < I";
7.308 +by (asm_simp_tac (simpset() addsimps [psubset_eq, not_sym, is_ideal_zero]) 1);
7.309 +qed "proper_ideal";
7.310 +
7.311 +Goalw [is_pideal_def] "is_ideal (I::('a::field) set) ==> is_pideal I";
7.312 +by (case_tac "I = {<0>}" 1);
7.313 +by (res_inst_tac [("x", "<0>")] exI 1);
7.314 +by (asm_simp_tac (simpset() addsimps [ideal_of_zero_eq]) 1);
7.315 +(* case "I ~= {<0>}" *)
7.316 +by (ftac proper_ideal 1);
7.317 +by (assume_tac 1);
7.318 +by (dtac psubset_imp_ex_mem 1);
7.319 +by (etac exE 1);
7.320 +by (res_inst_tac [("x", "b")] exI 1);
7.321 +by (cut_inst_tac [("a", "b")] element_generates_subideal 1);
7.322 + by (assume_tac 1); by (Blast_tac 1);
7.323 +by (auto_tac (claset(), simpset() addsimps [field_pideal_univ]));
7.324 +qed "field_pid";
7.325 +
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/src/HOL/Algebra/abstract/Ideal.thy Fri Nov 05 11:14:26 1999 +0100
8.3 @@ -0,0 +1,28 @@
8.4 +(*
8.5 + Ideals for commutative rings
8.6 + $Id$
8.7 + Author: Clemens Ballarin, started 24 September 1999
8.8 +*)
8.9 +
8.10 +Ideal = Ring +
8.11 +
8.12 +consts
8.13 + ideal_of :: ('a::ringS) set => 'a set
8.14 + is_ideal :: ('a::ringS) set => bool
8.15 + is_pideal :: ('a::ringS) set => bool
8.16 +
8.17 +defs
8.18 + is_ideal_def "is_ideal I == (ALL a: I. ALL b: I. a + b : I) &
8.19 + (ALL a: I. - a : I) & <0> : I &
8.20 + (ALL a: I. ALL r. a * r : I)"
8.21 + ideal_of_def "ideal_of S == Inter {I. is_ideal I & S <= I}"
8.22 + is_pideal_def "is_pideal I == (EX a. I = ideal_of {a})"
8.23 +
8.24 +(* Principle ideal domains *)
8.25 +
8.26 +axclass
8.27 + pid < domain
8.28 +
8.29 + pid_ax "is_ideal I ==> is_pideal I"
8.30 +
8.31 +end
8.32 \ No newline at end of file
9.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
9.2 +++ b/src/HOL/Algebra/abstract/NatSum.ML Fri Nov 05 11:14:26 1999 +0100
9.3 @@ -0,0 +1,268 @@
9.4 +(*
9.5 + Sums with naturals as index domain
9.6 + $Id$
9.7 + Author: Clemens Ballarin, started 12 December 1996
9.8 +*)
9.9 +
9.10 +open NatSum;
9.11 +
9.12 +section "Basic Properties";
9.13 +
9.14 +Goalw [SUM_def] "SUM 0 f = (f 0::'a::ring)";
9.15 +by (Asm_simp_tac 1);
9.16 +qed "SUM_0";
9.17 +
9.18 +Goalw [SUM_def]
9.19 + "SUM (Suc n) f = (f (Suc n) + SUM n f::'a::ring)";
9.20 +by (Simp_tac 1);
9.21 +qed "SUM_Suc";
9.22 +
9.23 +Addsimps [SUM_0, SUM_Suc];
9.24 +
9.25 +Goal
9.26 + "SUM (Suc n) f = (SUM n (%i. f (Suc i)) + f 0::'a::ring)";
9.27 +by (nat_ind_tac "n" 1);
9.28 +(* Base case *)
9.29 +by (Simp_tac 1);
9.30 +(* Induction step *)
9.31 +by (asm_full_simp_tac (simpset() addsimps [a_assoc]) 1);
9.32 +qed "SUM_Suc2";
9.33 +
9.34 +(* Congruence rules *)
9.35 +
9.36 +val [p_equal, p_context] = goal NatSum.thy
9.37 + "[| m = n; !!i. i <= n ==> f i = g i |] ==> SUM m f = (SUM n g::'a::ring)";
9.38 +by (simp_tac (simpset() addsimps [p_equal]) 1);
9.39 +by (cut_inst_tac [("n", "n")] le_refl 1);
9.40 +by (etac rev_mp 1);
9.41 +by (res_inst_tac [("P", "%k. k <= n --> SUM k f = SUM k g")] nat_induct 1);
9.42 +(* Base case *)
9.43 +by (simp_tac (simpset() addsimps [p_context]) 1);
9.44 +(* Induction step *)
9.45 +by (rtac impI 1);
9.46 +by (etac impE 1);
9.47 +by (rtac Suc_leD 1);
9.48 +by (assume_tac 1);
9.49 +by (asm_simp_tac (simpset() addsimps [p_context]) 1);
9.50 +qed "SUM_cong";
9.51 +
9.52 +Addcongs [SUM_cong];
9.53 +
9.54 +(* Results needed for the development of polynomials *)
9.55 +
9.56 +section "Ring Properties";
9.57 +
9.58 +Goal "SUM n (%i. <0>) = (<0>::'a::ring)";
9.59 +by (nat_ind_tac "n" 1);
9.60 +by (Simp_tac 1);
9.61 +by (Asm_simp_tac 1);
9.62 +qed "SUM_zero";
9.63 +
9.64 +Addsimps [SUM_zero];
9.65 +
9.66 +Goal
9.67 + "!!f::nat=>'a::ring. SUM n (%i. f i + g i) = SUM n f + SUM n g";
9.68 +by (nat_ind_tac "n" 1);
9.69 +(* Base case *)
9.70 +by (Simp_tac 1);
9.71 +(* Induction step *)
9.72 +by (asm_simp_tac (simpset() addsimps a_ac) 1);
9.73 +qed "SUM_add";
9.74 +
9.75 +Goal
9.76 + "!!a::'a::ring. SUM n f * a = SUM n (%i. f i * a)";
9.77 +by (nat_ind_tac "n" 1);
9.78 +(* Base case *)
9.79 +by (Simp_tac 1);
9.80 +(* Induction step *)
9.81 +by (asm_simp_tac (simpset() addsimps [l_distr]) 1);
9.82 +qed "SUM_ldistr";
9.83 +
9.84 +Goal
9.85 + "!!a::'a::ring. a * SUM n f = SUM n (%i. a * f i)";
9.86 +by (nat_ind_tac "n" 1);
9.87 +(* Base case *)
9.88 +by (Simp_tac 1);
9.89 +(* Induction step *)
9.90 +by (asm_simp_tac (simpset() addsimps [r_distr]) 1);
9.91 +qed "SUM_rdistr";
9.92 +
9.93 +section "Results for the Construction of Polynomials";
9.94 +
9.95 +goal Main.thy (* could go to Arith *)
9.96 + "!!j::nat. [| m <= j; Suc j <= n |] ==> (n - m) - Suc (j - m) = n - Suc j";
9.97 +by (asm_simp_tac (simpset() addsimps [Suc_diff_le RS sym]) 1);
9.98 +by (asm_simp_tac (simpset() addsimps [diff_right_cancel, less_imp_le]) 1);
9.99 +qed "Suc_diff_lemma";
9.100 +
9.101 +Goal
9.102 + "!!a::nat=>'a::ring. k <= n --> \
9.103 +\ SUM k (%j. SUM j (%i. a i * b (j-i)) * c (n-j)) = \
9.104 +\ SUM k (%j. a j * SUM (k-j) (%i. b i * c (n-j-i)))";
9.105 +by (nat_ind_tac "k" 1);
9.106 +(* Base case *)
9.107 +by (simp_tac (simpset() addsimps [m_assoc]) 1);
9.108 +(* Induction step *)
9.109 +by (rtac impI 1);
9.110 +by (etac impE 1);
9.111 +by (rtac Suc_leD 1);
9.112 +by (assume_tac 1);
9.113 +by (asm_simp_tac (simpset() addsimps a_ac@[Suc_diff_le, l_distr, r_distr, m_assoc, SUM_add]) 1);
9.114 +by (asm_simp_tac (simpset() addsimps a_ac@[Suc_diff_lemma, SUM_ldistr, m_assoc]) 1);
9.115 +qed "poly_assoc_lemma1";
9.116 +
9.117 +Goal
9.118 + "!!a::nat=>'a::ring. \
9.119 +\ SUM n (%j. SUM j (%i. a i * b (j-i)) * c (n-j)) = \
9.120 +\ SUM n (%j. a j * SUM (n-j) (%i. b i * c (n-j-i)))";
9.121 +by (rtac (poly_assoc_lemma1 RS mp) 1);
9.122 +by (rtac le_refl 1);
9.123 +qed "poly_assoc_lemma";
9.124 +
9.125 +goal Main.thy (* could go to Arith *)
9.126 + "!! n. Suc i <= n ==> Suc (a + (n - Suc i)) = a + (n - i)";
9.127 +by (asm_simp_tac (simpset() delsimps [add_Suc] addsimps [add_Suc_right RS sym, Suc_diff_Suc]) 1);
9.128 +qed "Suc_add_diff_Suc";
9.129 +
9.130 +goal Main.thy (* could go to Arith *)
9.131 + "!! n. [| Suc j <= n; i <= j |] ==> \
9.132 +\ n - Suc i - (n - Suc j) = n - i - (n - j)";
9.133 +by (res_inst_tac [("m1", "n - Suc i"), ("n1", "n - Suc j")]
9.134 + (diff_Suc_Suc RS subst) 1);
9.135 +by (subgoal_tac "Suc i <= n" 1);
9.136 +by (asm_simp_tac (simpset() delsimps [diff_Suc_Suc] addsimps [Suc_diff_Suc]) 1);
9.137 +by (fast_arith_tac 1);
9.138 +qed "diff_lemma2";
9.139 +
9.140 +Goal
9.141 + "!! a::nat=>'a::ring. j <= n --> \
9.142 +\ SUM j (%i. a i * b (n-i)) = SUM j (%i. a (n-i-(n-j)) * b (i+(n-j)))";
9.143 +by (nat_ind_tac "j" 1);
9.144 +(* Base case *)
9.145 +by (Simp_tac 1);
9.146 +(* Induction step *)
9.147 +by (rtac impI 1);
9.148 +by (etac impE 1);
9.149 +by (rtac Suc_leD 1);
9.150 +by (assume_tac 1);
9.151 +by (stac SUM_Suc2 1);
9.152 +by (stac SUM_Suc 1);
9.153 +by (asm_simp_tac (simpset()
9.154 + addsimps [a_comm, Suc_add_diff_Suc, diff_diff_cancel, diff_lemma2]) 1);
9.155 +qed "poly_comm_lemma1";
9.156 +
9.157 +Goal
9.158 + "!!a::nat=>'a::ring. SUM n (%i. a i * b (n-i)) = SUM n (%i. a (n-i) * b i)";
9.159 +by (cut_inst_tac [("j", "n"), ("n", "n")] poly_comm_lemma1 1);
9.160 +by (Asm_full_simp_tac 1);
9.161 +qed "poly_comm_lemma";
9.162 +
9.163 +section "Changing the Range of Summation";
9.164 +
9.165 +Goal
9.166 + "!! f::(nat=>'a::ring). \
9.167 +\ SUM n (%i. if i = x then f i else <0>) = (if x <= n then f x else <0>)";
9.168 +by (nat_ind_tac "n" 1);
9.169 +(* Base case *)
9.170 +by (simp_tac (simpset() setloop (split_tac [expand_if])) 1);
9.171 +(* Induction step *)
9.172 +by (asm_simp_tac (simpset() setloop (split_tac [expand_if])) 1);
9.173 +by (Clarify_tac 1);
9.174 +by (res_inst_tac [("f", "f")] arg_cong 1);
9.175 +by (fast_arith_tac 1);
9.176 +qed "SUM_if_singleton";
9.177 +
9.178 +Goal
9.179 + "!! f::(nat=>'a::ring). \
9.180 +\ m <= n & (ALL i. m < i & i <= n --> f i = <0>) --> \
9.181 +\ SUM m f = SUM n f";
9.182 +by (nat_ind_tac "n" 1);
9.183 +(* Base case *)
9.184 +by (Simp_tac 1);
9.185 +(* Induction step *)
9.186 +by (case_tac "m <= n" 1);
9.187 +by (rtac impI 1);
9.188 +by (etac impE 1);
9.189 +by (SELECT_GOAL Auto_tac 1);
9.190 +by (etac conjE 1);
9.191 +by (dres_inst_tac [("x", "Suc n")] spec 1);
9.192 +by (asm_simp_tac (simpset() addsimps [less_Suc_eq_le]) 1);
9.193 +(* case n < m, in fact m = Suc n *)
9.194 +by (rtac impI 1);
9.195 +by (etac conjE 1);
9.196 +by (subgoal_tac "m = Suc n" 1);
9.197 +by (Asm_simp_tac 1);
9.198 +by (fast_arith_tac 1);
9.199 +val SUM_shrink_lemma = result();
9.200 +
9.201 +Goal
9.202 + "!! f::(nat=>'a::ring). \
9.203 +\ [| m <= n; !!i. [| m < i; i <= n |] ==> f i = <0>; P (SUM n f) |] ==> \
9.204 +\ P (SUM m f)";
9.205 +by (cut_inst_tac [("m", "m"), ("n", "n"), ("f", "f")] SUM_shrink_lemma 1);
9.206 +by (Asm_full_simp_tac 1);
9.207 +qed "SUM_shrink";
9.208 +
9.209 +Goal
9.210 + "!! f::(nat=>'a::ring). \
9.211 +\ [| m <= n; !!i. [| m < i; i <= n |] ==> f i = <0>; P (SUM m f) |] ==> \
9.212 +\ P (SUM n f)";
9.213 +by (cut_inst_tac [("m", "m"), ("n", "n"), ("f", "f")] SUM_shrink_lemma 1);
9.214 +by (Asm_full_simp_tac 1);
9.215 +qed "SUM_extend";
9.216 +
9.217 +Goal
9.218 + "!! f::(nat=>'a::ring). \
9.219 +\ (ALL i. i < m --> f i = <0>) --> SUM d (%i. f (i+m)) = SUM (m+d) f";
9.220 +by (nat_ind_tac "d" 1);
9.221 +(* Base case *)
9.222 +by (nat_ind_tac "m" 1);
9.223 +by (Simp_tac 1);
9.224 +by (rtac impI 1);
9.225 +by (etac impE 1);
9.226 +by (Asm_simp_tac 1);
9.227 +by (subgoal_tac "SUM m f = <0>" 1);
9.228 +by (Asm_simp_tac 1);
9.229 +by (Asm_full_simp_tac 1);
9.230 +(* Induction step *)
9.231 +by (asm_simp_tac (simpset() addsimps add_ac) 1);
9.232 +val SUM_shrink_below_lemma = result();
9.233 +
9.234 +Goal
9.235 + "!! f::(nat=>'a::ring). \
9.236 +\ [| m <= n; !!i. i < m ==> f i = <0>; P (SUM (n-m) (%i. f (i+m))) |] ==> \
9.237 +\ P (SUM n f)";
9.238 +by (asm_full_simp_tac (simpset() addsimps
9.239 + [SUM_shrink_below_lemma, add_diff_inverse, leD]) 1);
9.240 +qed "SUM_extend_below";
9.241 +
9.242 +section "Result for the Univeral Property of Polynomials";
9.243 +
9.244 +Goal
9.245 + "!!f::nat=>'a::ring. j <= n + m --> \
9.246 +\ SUM j (%k. SUM k (%i. f i * g (k - i))) = \
9.247 +\ SUM j (%k. SUM (j - k) (%i. f k * g i))";
9.248 +by (nat_ind_tac "j" 1);
9.249 +(* Base case *)
9.250 +by (Simp_tac 1);
9.251 +(* Induction step *)
9.252 +by (simp_tac (simpset() addsimps [Suc_diff_le]) 1);
9.253 +by (simp_tac (simpset() addsimps [SUM_add]) 1);
9.254 +by (rtac impI 1);
9.255 +by (etac impE 1);
9.256 +by (dtac Suc_leD 1);
9.257 +by (assume_tac 1);
9.258 +by (asm_simp_tac (simpset() addsimps a_ac) 1);
9.259 +val DiagSum_lemma = result();
9.260 +
9.261 +Goal
9.262 + "!!f::nat=>'a::ring. \
9.263 +\ SUM (n + m) (%k. SUM k (%i. f i * g (k - i))) = \
9.264 +\ SUM (n + m) (%k. SUM (n + m - k) (%i. f k * g i))";
9.265 +by (rtac (DiagSum_lemma RS mp) 1);
9.266 +by (rtac le_refl 1);
9.267 +qed "DiagSum";
9.268 +
9.269 +
9.270 +
9.271 +
10.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
10.2 +++ b/src/HOL/Algebra/abstract/NatSum.thy Fri Nov 05 11:14:26 1999 +0100
10.3 @@ -0,0 +1,15 @@
10.4 +(*
10.5 + Sums with naturals as index domain
10.6 + $Id$
10.7 + Author: Clemens Ballarin, started 12 December 1996
10.8 +*)
10.9 +
10.10 +NatSum = Ring +
10.11 +
10.12 +consts
10.13 + SUM :: [nat, nat => 'a] => 'a::ringS
10.14 +
10.15 +defs
10.16 + SUM_def "SUM n f == nat_rec <0> (%m sum. f m + sum) (Suc n)"
10.17 +
10.18 +end
11.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
11.2 +++ b/src/HOL/Algebra/abstract/PID.thy Fri Nov 05 11:14:26 1999 +0100
11.3 @@ -0,0 +1,13 @@
11.4 +(*
11.5 + Principle ideal domains
11.6 + $Id$
11.7 + Author: Clemens Ballarin, started 5 October 1999
11.8 +*)
11.9 +
11.10 +PID = Ideal +
11.11 +
11.12 +instance
11.13 + pid < factorial (TrueI, pid_irred_imp_prime)
11.14 +
11.15 +end
11.16 +
12.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
12.2 +++ b/src/HOL/Algebra/abstract/Ring.ML Fri Nov 05 11:14:26 1999 +0100
12.3 @@ -0,0 +1,396 @@
12.4 +(*
12.5 + Abstract class ring (commutative, with 1)
12.6 + $Id$
12.7 + Author: Clemens Ballarin, started 9 December 1996
12.8 +*)
12.9 +
12.10 +open Ring;
12.11 +
12.12 +Blast.overloaded ("Divides.op dvd", domain_type);
12.13 +
12.14 +section "Rings";
12.15 +
12.16 +fun make_left_commute assoc commute s =
12.17 + [rtac (commute RS trans) 1, rtac (assoc RS trans) 1,
12.18 + rtac (commute RS arg_cong) 1];
12.19 +
12.20 +(* addition *)
12.21 +
12.22 +qed_goal "a_lcomm" Ring.thy "!!a::'a::ring. a+(b+c) = b+(a+c)"
12.23 + (make_left_commute a_assoc a_comm);
12.24 +
12.25 +val a_ac = [a_assoc, a_comm, a_lcomm];
12.26 +
12.27 +qed_goal "r_zero" Ring.thy "!!a::'a::ring. a + <0> = a"
12.28 + (fn _ => [rtac (a_comm RS trans) 1, rtac l_zero 1]);
12.29 +
12.30 +qed_goal "r_neg" Ring.thy "!!a::'a::ring. a + (-a) = <0>"
12.31 + (fn _ => [rtac (a_comm RS trans) 1, rtac l_neg 1]);
12.32 +
12.33 +Goal "!! a::'a::ring. a + b = a + c ==> b = c";
12.34 +by (rtac box_equals 1);
12.35 +by (rtac l_zero 2);
12.36 +by (rtac l_zero 2);
12.37 +by (res_inst_tac [("a1", "a")] (l_neg RS subst) 1);
12.38 +by (asm_simp_tac (simpset() addsimps [a_assoc]) 1);
12.39 +qed "a_lcancel";
12.40 +
12.41 +Goal "!! a::'a::ring. b + a = c + a ==> b = c";
12.42 +by (rtac a_lcancel 1);
12.43 +by (asm_simp_tac (simpset() addsimps a_ac) 1);
12.44 +qed "a_rcancel";
12.45 +
12.46 +Goal "!! a::'a::ring. (a + b = a + c) = (b = c)";
12.47 +by (auto_tac (claset() addSDs [a_lcancel], simpset()));
12.48 +qed "a_lcancel_eq";
12.49 +
12.50 +Goal "!! a::'a::ring. (b + a = c + a) = (b = c)";
12.51 +by (simp_tac (simpset() addsimps [a_lcancel_eq, a_comm]) 1);
12.52 +qed "a_rcancel_eq";
12.53 +
12.54 +Addsimps [a_lcancel_eq, a_rcancel_eq];
12.55 +
12.56 +Goal "!!a::'a::ring. -(-a) = a";
12.57 +by (rtac a_lcancel 1);
12.58 +by (rtac (r_neg RS trans) 1);
12.59 +by (rtac (l_neg RS sym) 1);
12.60 +qed "minus_minus";
12.61 +
12.62 +Goal "- <0> = (<0>::'a::ring)";
12.63 +by (rtac a_lcancel 1);
12.64 +by (rtac (r_neg RS trans) 1);
12.65 +by (rtac (l_zero RS sym) 1);
12.66 +qed "minus0";
12.67 +
12.68 +Goal "!!a::'a::ring. -(a + b) = (-a) + (-b)";
12.69 +by (res_inst_tac [("a", "a+b")] a_lcancel 1);
12.70 +by (simp_tac (simpset() addsimps ([r_neg, l_neg, l_zero]@a_ac)) 1);
12.71 +qed "minus_add";
12.72 +
12.73 +(* multiplication *)
12.74 +
12.75 +qed_goal "m_lcomm" Ring.thy "!!a::'a::ring. a*(b*c) = b*(a*c)"
12.76 + (make_left_commute m_assoc m_comm);
12.77 +
12.78 +val m_ac = [m_assoc, m_comm, m_lcomm];
12.79 +
12.80 +qed_goal "r_one" Ring.thy "!!a::'a::ring. a * <1> = a"
12.81 + (fn _ => [rtac (m_comm RS trans) 1, rtac l_one 1]);
12.82 +
12.83 +(* distributive and derived *)
12.84 +
12.85 +Goal "!!a::'a::ring. a * (b + c) = a * b + a * c";
12.86 +by (rtac (m_comm RS trans) 1);
12.87 +by (rtac (l_distr RS trans) 1);
12.88 +by (simp_tac (simpset() addsimps [m_comm]) 1);
12.89 +qed "r_distr";
12.90 +
12.91 +val m_distr = m_ac @ [l_distr, r_distr];
12.92 +
12.93 +(* the following two proofs can be found in
12.94 + Jacobson, Basic Algebra I, pp. 88-89 *)
12.95 +
12.96 +Goal "!!a::'a::ring. <0> * a = <0>";
12.97 +by (rtac a_lcancel 1);
12.98 +by (rtac (l_distr RS sym RS trans) 1);
12.99 +by (simp_tac (simpset() addsimps [r_zero]) 1);
12.100 +qed "l_null";
12.101 +
12.102 +qed_goal "r_null" Ring.thy "!!a::'a::ring. a * <0> = <0>"
12.103 + (fn _ => [rtac (m_comm RS trans) 1, rtac l_null 1]);
12.104 +
12.105 +Goal "!!a::'a::ring. (-a) * b = - (a * b)";
12.106 +by (rtac a_lcancel 1);
12.107 +by (rtac (r_neg RS sym RSN (2, trans)) 1);
12.108 +by (rtac (l_distr RS sym RS trans) 1);
12.109 +by (simp_tac (simpset() addsimps [l_null, r_neg]) 1);
12.110 +qed "l_minus";
12.111 +
12.112 +Goal "!!a::'a::ring. a * (-b) = - (a * b)";
12.113 +by (rtac a_lcancel 1);
12.114 +by (rtac (r_neg RS sym RSN (2, trans)) 1);
12.115 +by (rtac (r_distr RS sym RS trans) 1);
12.116 +by (simp_tac (simpset() addsimps [r_null, r_neg]) 1);
12.117 +qed "r_minus";
12.118 +
12.119 +val m_minus = [l_minus, r_minus];
12.120 +
12.121 +(* one and zero are distinct *)
12.122 +
12.123 +qed_goal "zero_not_one" Ring.thy "<0> ~= (<1>::'a::ring)"
12.124 + (fn _ => [rtac not_sym 1, rtac one_not_zero 1]);
12.125 +
12.126 +Addsimps [l_zero, r_zero, l_neg, r_neg, minus_minus, minus0,
12.127 + l_one, r_one, l_null, r_null,
12.128 + one_not_zero, zero_not_one];
12.129 +
12.130 +(* further rules *)
12.131 +
12.132 +Goal "!!a::'a::ring. -a = <0> ==> a = <0>";
12.133 +by (res_inst_tac [("t", "a")] (minus_minus RS subst) 1);
12.134 +by (Asm_simp_tac 1);
12.135 +qed "uminus_monom";
12.136 +
12.137 +Goal "!!a::'a::ring. a ~= <0> ==> -a ~= <0>";
12.138 +by (etac contrapos 1);
12.139 +by (rtac uminus_monom 1);
12.140 +by (assume_tac 1);
12.141 +qed "uminus_monom_neq";
12.142 +
12.143 +Goal "!!a::'a::ring. a * b ~= <0> ==> a ~= <0>";
12.144 +by (etac contrapos 1);
12.145 +by (Asm_simp_tac 1);
12.146 +qed "l_nullD";
12.147 +
12.148 +Goal "!!a::'a::ring. a * b ~= <0> ==> b ~= <0>";
12.149 +by (etac contrapos 1);
12.150 +by (Asm_simp_tac 1);
12.151 +qed "r_nullD";
12.152 +
12.153 +(* reflection between a = b and a -- b = <0> *)
12.154 +
12.155 +Goal "!!a::'a::ring. a = b ==> a + (-b) = <0>";
12.156 +by (Asm_simp_tac 1);
12.157 +qed "eq_imp_diff_zero";
12.158 +
12.159 +Goal "!!a::'a::ring. a + (-b) = <0> ==> a = b";
12.160 +by (res_inst_tac [("a", "-b")] a_rcancel 1);
12.161 +by (Asm_simp_tac 1);
12.162 +qed "diff_zero_imp_eq";
12.163 +
12.164 +(* this could be a rewrite rule, but won't terminate
12.165 + ==> make it a simproc?
12.166 +Goal "!!a::'a::ring. (a = b) = (a -- b = <0>)";
12.167 +*)
12.168 +
12.169 +(* Power *)
12.170 +
12.171 +Goal "!!a::'a::ring. a ^ 0 = <1>";
12.172 +by (simp_tac (simpset() addsimps [power_ax]) 1);
12.173 +qed "power_0";
12.174 +
12.175 +Goal "!!a::'a::ring. a ^ Suc n = a ^ n * a";
12.176 +by (simp_tac (simpset() addsimps [power_ax]) 1);
12.177 +qed "power_Suc";
12.178 +
12.179 +Addsimps [power_0, power_Suc];
12.180 +
12.181 +Goal "<1> ^ n = (<1>::'a::ring)";
12.182 +by (nat_ind_tac "n" 1);
12.183 +by (Simp_tac 1);
12.184 +by (Asm_simp_tac 1);
12.185 +qed "power_one";
12.186 +
12.187 +Goal "!!n. n ~= 0 ==> <0> ^ n = (<0>::'a::ring)";
12.188 +by (etac rev_mp 1);
12.189 +by (nat_ind_tac "n" 1);
12.190 +by (Simp_tac 1);
12.191 +by (Simp_tac 1);
12.192 +qed "power_zero";
12.193 +
12.194 +Addsimps [power_zero, power_one];
12.195 +
12.196 +Goal "!! a::'a::ring. a ^ m * a ^ n = a ^ (m + n)";
12.197 +by (nat_ind_tac "m" 1);
12.198 +by (Simp_tac 1);
12.199 +by (asm_simp_tac (simpset() addsimps m_ac) 1);
12.200 +qed "power_mult";
12.201 +
12.202 +(* Divisibility *)
12.203 +section "Divisibility";
12.204 +
12.205 +Goalw [dvd_def] "!! a::'a::ring. a dvd <0>";
12.206 +by (res_inst_tac [("x", "<0>")] exI 1);
12.207 +by (Simp_tac 1);
12.208 +qed "dvd_zero_right";
12.209 +
12.210 +Goalw [dvd_def] "!! a::'a::ring. <0> dvd a ==> a = <0>";
12.211 +by Auto_tac;
12.212 +qed "dvd_zero_left";
12.213 +
12.214 +Goalw [dvd_def] "!! a::'a::ring. a dvd a";
12.215 +by (res_inst_tac [("x", "<1>")] exI 1);
12.216 +by (Simp_tac 1);
12.217 +qed "dvd_refl_ring";
12.218 +
12.219 +Goalw [dvd_def] "!! a::'a::ring. [| a dvd b; b dvd c |] ==> a dvd c";
12.220 +by (Step_tac 1);
12.221 +by (res_inst_tac [("x", "k * ka")] exI 1);
12.222 +by (simp_tac (simpset() addsimps m_ac) 1);
12.223 +qed "dvd_trans_ring";
12.224 +
12.225 +Addsimps [dvd_zero_right, dvd_refl_ring];
12.226 +
12.227 +Goal "!! a::'a::ring. a dvd <1> ==> a ~= <0>";
12.228 +by (auto_tac (claset() addDs [dvd_zero_left], simpset()));
12.229 +qed "unit_imp_nonzero";
12.230 +
12.231 +Goalw [dvd_def]
12.232 + "!!a::'a::ring. [| a dvd <1>; b dvd <1> |] ==> a * b dvd <1>";
12.233 +by (Clarify_tac 1);
12.234 +by (res_inst_tac [("x", "k * ka")] exI 1);
12.235 +by (asm_full_simp_tac (simpset() addsimps m_ac) 1);
12.236 +qed "unit_mult";
12.237 +
12.238 +Goal "!!a::'a::ring. a dvd <1> ==> a^n dvd <1>";
12.239 +by (induct_tac "n" 1);
12.240 +by (Simp_tac 1);
12.241 +by (asm_simp_tac (simpset() addsimps [unit_mult]) 1);
12.242 +qed "unit_power";
12.243 +
12.244 +Goalw [dvd_def]
12.245 + "!! a::'a::ring. [| a dvd b; a dvd c |] ==> a dvd (b + c)";
12.246 +by (Clarify_tac 1);
12.247 +by (res_inst_tac [("x", "k + ka")] exI 1);
12.248 +by (simp_tac (simpset() addsimps [r_distr]) 1);
12.249 +qed "dvd_add_right";
12.250 +
12.251 +Goalw [dvd_def]
12.252 + "!! a::'a::ring. a dvd b ==> a dvd (-b)";
12.253 +by (Clarify_tac 1);
12.254 +by (res_inst_tac [("x", "-k")] exI 1);
12.255 +by (simp_tac (simpset() addsimps [r_minus]) 1);
12.256 +qed "dvd_uminus_right";
12.257 +
12.258 +Goalw [dvd_def]
12.259 + "!! a::'a::ring. a dvd b ==> a dvd (c * b)";
12.260 +by (Clarify_tac 1);
12.261 +by (res_inst_tac [("x", "c * k")] exI 1);
12.262 +by (simp_tac (simpset() addsimps m_ac) 1);
12.263 +qed "dvd_l_mult_right";
12.264 +
12.265 +Goalw [dvd_def]
12.266 + "!! a::'a::ring. a dvd b ==> a dvd (b * c)";
12.267 +by (Clarify_tac 1);
12.268 +by (res_inst_tac [("x", "k * c")] exI 1);
12.269 +by (simp_tac (simpset() addsimps m_ac) 1);
12.270 +qed "dvd_r_mult_right";
12.271 +
12.272 +Addsimps [dvd_add_right, dvd_uminus_right, dvd_l_mult_right, dvd_r_mult_right];
12.273 +
12.274 +(* Inverse of multiplication *)
12.275 +
12.276 +section "inverse";
12.277 +
12.278 +Goal "!! a::'a::ring. [| a * x = <1>; a * y = <1> |] ==> x = y";
12.279 +by (res_inst_tac [("a", "(a*y)*x"), ("b", "y*(a*x)")] box_equals 1);
12.280 +by (simp_tac (simpset() addsimps m_ac) 1);
12.281 +by Auto_tac;
12.282 +qed "inverse_unique";
12.283 +
12.284 +Goalw [inverse_def, dvd_def]
12.285 + "!! a::'a::ring. a dvd <1> ==> a * inverse a = <1>";
12.286 +by (Asm_simp_tac 1);
12.287 +by (Clarify_tac 1);
12.288 +by (rtac selectI 1);
12.289 +by (rtac sym 1);
12.290 +by (assume_tac 1);
12.291 +qed "r_inverse_ring";
12.292 +
12.293 +Goal "!! a::'a::ring. a dvd <1> ==> inverse a * a= <1>";
12.294 +by (asm_simp_tac (simpset() addsimps r_inverse_ring::m_ac) 1);
12.295 +qed "l_inverse_ring";
12.296 +
12.297 +(* Integral domain *)
12.298 +
12.299 +section "Integral domains";
12.300 +
12.301 +Goal
12.302 + "!! a. [| a * b = <0>; a ~= <0> |] ==> (b::'a::domain) = <0>";
12.303 +by (dtac integral 1);
12.304 +by (Fast_tac 1);
12.305 +qed "r_integral";
12.306 +
12.307 +Goal
12.308 + "!! a. [| a * b = <0>; b ~= <0> |] ==> (a::'a::domain) = <0>";
12.309 +by (dtac integral 1);
12.310 +by (Fast_tac 1);
12.311 +qed "l_integral";
12.312 +
12.313 +Goal
12.314 + "!! a::'a::domain. [| a ~= <0>; b ~= <0> |] ==> a * b ~= <0>";
12.315 +by (etac contrapos 1);
12.316 +by (rtac l_integral 1);
12.317 +by (assume_tac 1);
12.318 +by (assume_tac 1);
12.319 +qed "not_integral";
12.320 +
12.321 +Addsimps [not_integral];
12.322 +
12.323 +Goal "!! a::'a::domain. [| a * x = x; x ~= <0> |] ==> a = <1>";
12.324 +by (res_inst_tac [("a", "- <1>")] a_lcancel 1);
12.325 +by (Simp_tac 1);
12.326 +by (rtac l_integral 1);
12.327 +by (assume_tac 2);
12.328 +by (asm_simp_tac (simpset() addsimps [l_distr, l_minus]) 1);
12.329 +qed "l_one_integral";
12.330 +
12.331 +Goal "!! a::'a::domain. [| x * a = x; x ~= <0> |] ==> a = <1>";
12.332 +by (res_inst_tac [("a", "- <1>")] a_rcancel 1);
12.333 +by (Simp_tac 1);
12.334 +by (rtac r_integral 1);
12.335 +by (assume_tac 2);
12.336 +by (asm_simp_tac (simpset() addsimps [r_distr, r_minus]) 1);
12.337 +qed "r_one_integral";
12.338 +
12.339 +(* cancellation laws for multiplication *)
12.340 +
12.341 +Goal "!! a::'a::domain. [| a ~= <0>; a * b = a * c |] ==> b = c";
12.342 +by (rtac diff_zero_imp_eq 1);
12.343 +by (dtac eq_imp_diff_zero 1);
12.344 +by (full_simp_tac (simpset() addsimps [r_minus RS sym, r_distr RS sym]) 1);
12.345 +by (fast_tac (claset() addIs [l_integral]) 1);
12.346 +qed "m_lcancel";
12.347 +
12.348 +Goal "!! a::'a::domain. [| a ~= <0>; b * a = c * a |] ==> b = c";
12.349 +by (rtac m_lcancel 1);
12.350 +by (assume_tac 1);
12.351 +by (asm_full_simp_tac (simpset() addsimps m_ac) 1);
12.352 +qed "m_rcancel";
12.353 +
12.354 +Goal "!! a::'a::domain. a ~= <0> ==> (a * b = a * c) = (b = c)";
12.355 +by (auto_tac (claset() addDs [m_lcancel], simpset()));
12.356 +qed "m_lcancel_eq";
12.357 +
12.358 +Goal "!! a::'a::domain. a ~= <0> ==> (b * a = c * a) = (b = c)";
12.359 +by (asm_simp_tac (simpset() addsimps [m_lcancel_eq, m_comm]) 1);
12.360 +qed "m_rcancel_eq";
12.361 +
12.362 +Addsimps [m_lcancel_eq, m_rcancel_eq];
12.363 +
12.364 +(* Fields *)
12.365 +
12.366 +section "Fields";
12.367 +
12.368 +Goal "!! a::'a::field. a dvd <1> = (a ~= <0>)";
12.369 +by (blast_tac (claset() addDs [field_ax, unit_imp_nonzero]) 1);
12.370 +qed "field_unit";
12.371 +
12.372 +Addsimps [field_unit];
12.373 +
12.374 +Goal "!! a::'a::field. a ~= <0> ==> a * inverse a = <1>";
12.375 +by (asm_full_simp_tac (simpset() addsimps [r_inverse_ring]) 1);
12.376 +qed "r_inverse";
12.377 +
12.378 +Goal "!! a::'a::field. a ~= <0> ==> inverse a * a= <1>";
12.379 +by (asm_full_simp_tac (simpset() addsimps [l_inverse_ring]) 1);
12.380 +qed "l_inverse";
12.381 +
12.382 +Addsimps [l_inverse, r_inverse];
12.383 +
12.384 +(* fields are factorial domains *)
12.385 +
12.386 +Goal "!! a::'a::field. a * b = <0> ==> a = <0> | b = <0>";
12.387 +by (Step_tac 1);
12.388 +by (res_inst_tac [("a", "(a*b)*inverse b")] box_equals 1);
12.389 +by (rtac refl 3);
12.390 +by (simp_tac (simpset() addsimps m_ac) 2);
12.391 +by Auto_tac;
12.392 +qed "field_integral";
12.393 +
12.394 +Goalw [prime_def, irred_def] "!! a::'a::field. irred a ==> prime a";
12.395 +by (blast_tac (claset() addIs [field_ax]) 1);
12.396 +qed "field_fact_prime";
12.397 +
12.398 +
12.399 +
13.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
13.2 +++ b/src/HOL/Algebra/abstract/Ring.thy Fri Nov 05 11:14:26 1999 +0100
13.3 @@ -0,0 +1,111 @@
13.4 +(*
13.5 + Abstract class ring (commutative, with 1)
13.6 + $Id$
13.7 + Author: Clemens Ballarin, started 9 December 1996
13.8 +*)
13.9 +
13.10 +Ring = Main +
13.11 +
13.12 +(* Syntactic class ring *)
13.13 +
13.14 +axclass
13.15 + ringS < plus, minus, times, power
13.16 +
13.17 +consts
13.18 + (* Basic rings *)
13.19 + "<0>" :: 'a::ringS ("<0>")
13.20 + "<1>" :: 'a::ringS ("<1>")
13.21 + "--" :: ['a, 'a] => 'a::ringS (infixl 65)
13.22 +
13.23 + (* Divisibility *)
13.24 + assoc :: ['a::times, 'a] => bool (infixl 70)
13.25 + irred :: 'a::ringS => bool
13.26 + prime :: 'a::ringS => bool
13.27 +
13.28 + (* Fields *)
13.29 + inverse :: 'a::ringS => 'a
13.30 + "'/'/" :: ['a, 'a] => 'a::ringS (infixl 70)
13.31 +
13.32 +translations
13.33 + "a -- b" == "a + (-b)"
13.34 + "a // b" == "a * inverse b"
13.35 +
13.36 +(* Class ring and ring axioms *)
13.37 +
13.38 +axclass
13.39 + ring < ringS
13.40 +
13.41 + a_assoc "(a + b) + c = a + (b + c)"
13.42 + l_zero "<0> + a = a"
13.43 + l_neg "(-a) + a = <0>"
13.44 + a_comm "a + b = b + a"
13.45 +
13.46 + m_assoc "(a * b) * c = a * (b * c)"
13.47 + l_one "<1> * a = a"
13.48 +
13.49 + l_distr "(a + b) * c = a * c + b * c"
13.50 +
13.51 + m_comm "a * b = b * a"
13.52 +
13.53 + one_not_zero "<1> ~= <0>"
13.54 + (* if <1> = <0>, then the ring has only one element! *)
13.55 +
13.56 + power_ax "a ^ n = nat_rec <1> (%u b. b * a) n"
13.57 +
13.58 +defs
13.59 + assoc_def "a assoc b == a dvd b & b dvd a"
13.60 + irred_def "irred a == a ~= <0> & ~ a dvd <1>
13.61 + & (ALL d. d dvd a --> d dvd <1> | a dvd d)"
13.62 + prime_def "prime p == p ~= <0> & ~ p dvd <1>
13.63 + & (ALL a b. p dvd (a*b) --> p dvd a | p dvd b)"
13.64 +
13.65 + inverse_def "inverse a == if a dvd <1> then @x. a*x = <1> else <0>"
13.66 +
13.67 +(* Integral domains *)
13.68 +
13.69 +axclass
13.70 + domain < ring
13.71 +
13.72 + integral "a * b = <0> ==> a = <0> | b = <0>"
13.73 +
13.74 +(* Factorial domains *)
13.75 +
13.76 +axclass
13.77 + factorial < domain
13.78 +
13.79 +(*
13.80 + Proper definition using divisor chain condition currently not supported.
13.81 + factorial_divisor "wf {(a, b). a dvd b & ~ (b dvd a)}"
13.82 +*)
13.83 + factorial_divisor "True"
13.84 + factorial_prime "irred a ==> prime a"
13.85 +
13.86 +(* Euclidean domains *)
13.87 +
13.88 +(*
13.89 +axclass
13.90 + euclidean < domain
13.91 +
13.92 + euclidean_ax "b ~= <0> ==> Ex (% (q, r, e_size::('a::ringS)=>nat).
13.93 + a = b * q + r & e_size r < e_size b)"
13.94 +
13.95 + Nothing has been proved about euclidean domains, yet.
13.96 + Design question:
13.97 + Fix quo, rem and e_size as constants that are axiomatised with
13.98 + euclidean_ax?
13.99 + - advantage: more pragmatic and easier to use
13.100 + - disadvantage: for every type, one definition of quo and rem will
13.101 + be fixed, users may want to use differing ones;
13.102 + also, it seems not possible to prove that fields are euclidean
13.103 + domains, because that would require generic (type-independent)
13.104 + definitions of quo and rem.
13.105 +*)
13.106 +
13.107 +(* Fields *)
13.108 +
13.109 +axclass
13.110 + field < ring
13.111 +
13.112 + field_ax "a ~= <0> ==> a dvd <1>"
13.113 +
13.114 +end
14.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
14.2 +++ b/src/HOL/Algebra/abstract/RingHomo.ML Fri Nov 05 11:14:26 1999 +0100
14.3 @@ -0,0 +1,65 @@
14.4 +(*
14.5 + Ring homomorphism
14.6 + $Id$
14.7 + Author: Clemens Ballarin, started 15 April 1997
14.8 +*)
14.9 +
14.10 +open RingHomo;
14.11 +
14.12 +(* Ring homomorphism *)
14.13 +
14.14 +Goalw [homo_def]
14.15 + "!! f. [| !! a b. f (a + b) = f a + f b; !! a b. f (a * b) = f a * f b; \
14.16 +\ f <1> = <1> |] ==> homo f";
14.17 +by Auto_tac;
14.18 +qed "homoI";
14.19 +
14.20 +Goalw [homo_def] "!! f. homo f ==> f (a + b) = f a + f b";
14.21 +by (Fast_tac 1);
14.22 +qed "homo_add";
14.23 +
14.24 +Goalw [homo_def] "!! f. homo f ==> f (a * b) = f a * f b";
14.25 +by (Fast_tac 1);
14.26 +qed "homo_mult";
14.27 +
14.28 +Goalw [homo_def] "!! f. homo f ==> f <1> = <1>";
14.29 +by (Fast_tac 1);
14.30 +qed "homo_one";
14.31 +
14.32 +Goal "!! f::('a::ring=>'b::ring). homo f ==> f <0> = <0>";
14.33 +by (res_inst_tac [("a", "f <0>")] a_lcancel 1);
14.34 +by (asm_simp_tac (simpset() addsimps [homo_add RS sym]) 1);
14.35 +qed "homo_zero";
14.36 +
14.37 +Goal
14.38 + "!! f::('a::ring=>'b::ring). homo f ==> f (-a) = - f a";
14.39 +by (res_inst_tac [("a", "f a")] a_lcancel 1);
14.40 +by (ftac homo_zero 1);
14.41 +by (asm_simp_tac (simpset() addsimps [homo_add RS sym]) 1);
14.42 +qed "homo_uminus";
14.43 +
14.44 +Goal "!! f::('a::ring=>'b::ring). homo f ==> f (a ^ n) = f a ^ n";
14.45 +by (nat_ind_tac "n" 1);
14.46 +by (dtac homo_one 1);
14.47 +by (Asm_simp_tac 1);
14.48 +by (dres_inst_tac [("a", "a^n"), ("b", "a")] homo_mult 1);
14.49 +by (Asm_simp_tac 1);
14.50 +qed "homo_power";
14.51 +
14.52 +Goal
14.53 + "!! f::('a::ring=>'b::ring). homo f ==> f (SUM n g) = SUM n (f o g)";
14.54 +by (nat_ind_tac "n" 1);
14.55 +by (Asm_simp_tac 1);
14.56 +by (Simp_tac 1);
14.57 +by (dres_inst_tac [("a", "g (Suc n)"), ("b", "SUM n g")] homo_add 1);
14.58 +by (Asm_simp_tac 1);
14.59 +qed "homo_SUM";
14.60 +
14.61 +Addsimps [homo_add, homo_mult, homo_one, homo_zero,
14.62 + homo_uminus, homo_power, homo_SUM];
14.63 +
14.64 +Goal "homo (%x. x)";
14.65 +by (fast_tac (claset() addSIs [homoI]) 1);
14.66 +qed "id_homo";
14.67 +
14.68 +Addsimps [id_homo];
15.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
15.2 +++ b/src/HOL/Algebra/abstract/RingHomo.thy Fri Nov 05 11:14:26 1999 +0100
15.3 @@ -0,0 +1,17 @@
15.4 +(*
15.5 + Ring homomorphism
15.6 + $Id$
15.7 + Author: Clemens Ballarin, started 15 April 1997
15.8 +*)
15.9 +
15.10 +RingHomo = NatSum +
15.11 +
15.12 +consts
15.13 + homo :: ('a::ringS => 'b::ringS) => bool
15.14 +
15.15 +defs
15.16 + homo_def "homo f == (ALL a b. f (a + b) = f a + f b &
15.17 + f (a * b) = f a * f b) &
15.18 + f <1> = <1>"
15.19 +
15.20 +end
16.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
16.2 +++ b/src/HOL/Algebra/poly/Degree.ML Fri Nov 05 11:14:26 1999 +0100
16.3 @@ -0,0 +1,363 @@
16.4 +(*
16.5 + Degree of polynomials
16.6 + $Id$
16.7 + written by Clemens Ballarin, started 22 January 1997
16.8 +*)
16.9 +
16.10 +(* Relating degree and bound *)
16.11 +
16.12 +goal ProtoPoly.thy
16.13 + "!! f. [| bound m f; f n ~= <0> |] ==> n <= m";
16.14 +by (rtac classical 1);
16.15 +by (dtac not_leE 1);
16.16 +by (dtac boundD 1 THEN atac 1);
16.17 +by (etac notE 1);
16.18 +by (assume_tac 1);
16.19 +qed "below_bound";
16.20 +
16.21 +goal UnivPoly.thy "bound (LEAST n. bound n (Rep_UP p)) (Rep_UP p)";
16.22 +by (rtac exE 1);
16.23 +by (rtac LeastI 2);
16.24 +by (assume_tac 2);
16.25 +by (res_inst_tac [("a", "Rep_UP p")] CollectD 1);
16.26 +by (rtac (rewrite_rule [UP_def] Rep_UP) 1);
16.27 +qed "Least_is_bound";
16.28 +
16.29 +Goalw [coeff_def, deg_def]
16.30 + "!! p. ALL m. n < m --> coeff m p = <0> ==> deg p <= n";
16.31 +by (rtac Least_le 1);
16.32 +by (Fast_tac 1);
16.33 +qed "deg_aboveI";
16.34 +
16.35 +Goalw [coeff_def, deg_def]
16.36 + "!! p. (n ~= 0 --> coeff n p ~= <0>) ==> n <= deg p";
16.37 +by (case_tac "n = 0" 1);
16.38 +(* Case n=0 *)
16.39 +by (Asm_simp_tac 1);
16.40 +(* Case n~=0 *)
16.41 +by (rotate_tac 1 1);
16.42 +by (Asm_full_simp_tac 1);
16.43 +by (rtac below_bound 1);
16.44 +by (assume_tac 2);
16.45 +by (rtac Least_is_bound 1);
16.46 +qed "deg_belowI";
16.47 +
16.48 +Goalw [coeff_def, deg_def]
16.49 + "!! p. deg p < m ==> coeff m p = <0>";
16.50 +by (rtac exE 1); (* create !! x. *)
16.51 +by (rtac boundD 2);
16.52 +by (assume_tac 3);
16.53 +by (rtac LeastI 2);
16.54 +by (assume_tac 2);
16.55 +by (res_inst_tac [("a", "Rep_UP p")] CollectD 1);
16.56 +by (rtac (rewrite_rule [UP_def] Rep_UP) 1);
16.57 +qed "deg_aboveD";
16.58 +
16.59 +Goalw [deg_def]
16.60 + "!! p. deg p = Suc y ==> ~ bound y (Rep_UP p)";
16.61 +by (rtac not_less_Least 1);
16.62 +by (Asm_simp_tac 1);
16.63 +val lemma1 = result();
16.64 +
16.65 +Goalw [deg_def, coeff_def]
16.66 + "!! p. deg p = Suc y ==> coeff (deg p) p ~= <0>";
16.67 +by (rtac classical 1);
16.68 +by (dtac notnotD 1);
16.69 +by (cut_inst_tac [("p", "p")] Least_is_bound 1);
16.70 +by (subgoal_tac "bound y (Rep_UP p)" 1);
16.71 +(* prove subgoal *)
16.72 +by (rtac boundI 2);
16.73 +by (case_tac "Suc y < m" 2);
16.74 +(* first case *)
16.75 +by (rtac boundD 2);
16.76 +by (assume_tac 2);
16.77 +by (Asm_simp_tac 2);
16.78 +(* second case *)
16.79 +by (dtac leI 2);
16.80 +by (dtac Suc_leI 2);
16.81 +by (dtac le_anti_sym 2);
16.82 +by (assume_tac 2);
16.83 +by (Asm_full_simp_tac 2);
16.84 +(* end prove subgoal *)
16.85 +by (fold_goals_tac [deg_def]);
16.86 +by (dtac lemma1 1);
16.87 +by (etac notE 1);
16.88 +by (assume_tac 1);
16.89 +val lemma2 = result();
16.90 +
16.91 +Goal
16.92 + "!! p. deg p ~= 0 ==> coeff (deg p) p ~= <0>";
16.93 +by (rtac lemma2 1);
16.94 +by (Full_simp_tac 1);
16.95 +by (dtac Suc_pred 1);
16.96 +by (rtac sym 1);
16.97 +by (Asm_simp_tac 1);
16.98 +qed "deg_lcoeff";
16.99 +
16.100 +Goal
16.101 + "!! p. p ~= <0> ==> coeff (deg p) p ~= <0>";
16.102 +by (etac contrapos 1);
16.103 +by (ftac contrapos2 1);
16.104 +by (rtac deg_lcoeff 1);
16.105 +by (assume_tac 1);
16.106 +by (rtac up_eqI 1);
16.107 +by (case_tac "n=0" 1);
16.108 +by (rotate_tac ~2 1);
16.109 +by (Asm_full_simp_tac 1);
16.110 +by (asm_full_simp_tac (simpset() addsimps [deg_aboveD]) 1);
16.111 +qed "nonzero_lcoeff";
16.112 +
16.113 +Goal "(deg p <= n) = bound n (Rep_UP p)";
16.114 +by (rtac iffI 1);
16.115 +(* ==> *)
16.116 +by (rtac boundI 1);
16.117 +by (fold_goals_tac [coeff_def]);
16.118 +by (rtac deg_aboveD 1);
16.119 +by (fast_arith_tac 1);
16.120 +(* <== *)
16.121 +by (rtac deg_aboveI 1);
16.122 +by (rewtac coeff_def);
16.123 +by (Fast_tac 1);
16.124 +qed "deg_above_is_bound";
16.125 +
16.126 +(* Lemmas on the degree function *)
16.127 +
16.128 +Goalw [max_def]
16.129 + "!! p::'a::ring up. deg (p + q) <= max (deg p) (deg q)";
16.130 +by (case_tac "deg p <= deg q" 1);
16.131 +(* case deg p <= deg q *)
16.132 +by (rtac deg_aboveI 1);
16.133 +by (Asm_simp_tac 1);
16.134 +by (strip_tac 1);
16.135 +by (dtac le_less_trans 1);
16.136 +by (assume_tac 1);
16.137 +by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
16.138 +(* case deg p > deg q *)
16.139 +by (rtac deg_aboveI 1);
16.140 +by (Asm_simp_tac 1);
16.141 +by (dtac not_leE 1);
16.142 +by (strip_tac 1);
16.143 +by (dtac less_trans 1);
16.144 +by (assume_tac 1);
16.145 +by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
16.146 +qed "deg_add";
16.147 +
16.148 +Goal "!!p::('a::ring up). deg p < deg q ==> deg (p + q) = deg q";
16.149 +by (rtac order_antisym 1);
16.150 +by (rtac le_trans 1);
16.151 +by (rtac deg_add 1);
16.152 +by (Asm_simp_tac 1);
16.153 +by (rtac deg_belowI 1);
16.154 +by (asm_simp_tac (simpset() addsimps [deg_aboveD, deg_lcoeff]) 1);
16.155 +qed "deg_add_equal";
16.156 +
16.157 +Goal "deg (monom m::'a::ring up) = m";
16.158 +by (rtac le_anti_sym 1);
16.159 +(* <= *)
16.160 +by (asm_simp_tac
16.161 + (simpset() addsimps [deg_aboveI, less_not_refl2 RS not_sym]) 1);
16.162 +(* >= *)
16.163 +by (asm_simp_tac
16.164 + (simpset() addsimps [deg_belowI, less_not_refl2 RS not_sym]) 1);
16.165 +qed "deg_monom";
16.166 +
16.167 +Goal "!! a::'a::ring. deg (const a) = 0";
16.168 +by (rtac le_anti_sym 1);
16.169 +by (rtac deg_aboveI 1);
16.170 +by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
16.171 +by (rtac deg_belowI 1);
16.172 +by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
16.173 +qed "deg_const";
16.174 +
16.175 +Goal "deg (<0>::'a::ringS up) = 0";
16.176 +by (rtac le_anti_sym 1);
16.177 +by (rtac deg_aboveI 1);
16.178 +by (Simp_tac 1);
16.179 +by (rtac deg_belowI 1);
16.180 +by (Simp_tac 1);
16.181 +qed "deg_zero";
16.182 +
16.183 +Goal "deg (<1>::'a::ring up) = 0";
16.184 +by (rtac le_anti_sym 1);
16.185 +by (rtac deg_aboveI 1);
16.186 +by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
16.187 +by (rtac deg_belowI 1);
16.188 +by (Simp_tac 1);
16.189 +qed "deg_one";
16.190 +
16.191 +Goal "!!p::('a::ring) up. deg (-p) = deg p";
16.192 +by (rtac le_anti_sym 1);
16.193 +(* <= *)
16.194 +by (simp_tac (simpset() addsimps [deg_aboveI, deg_aboveD]) 1);
16.195 +by (simp_tac (simpset() addsimps [deg_belowI, deg_lcoeff, uminus_monom_neq]) 1);
16.196 +qed "deg_uminus";
16.197 +
16.198 +Addsimps [deg_monom, deg_const, deg_zero, deg_one, deg_uminus];
16.199 +
16.200 +Goal
16.201 + "!! a::'a::ring. deg (a *s p) <= (if a = <0> then 0 else deg p)";
16.202 +by (case_tac "a = <0>" 1);
16.203 +by (REPEAT (asm_simp_tac (simpset() addsimps [deg_aboveI, deg_aboveD]) 1));
16.204 +qed "deg_smult_ring";
16.205 +
16.206 +Goal
16.207 + "!! a::'a::domain. deg (a *s p) = (if a = <0> then 0 else deg p)";
16.208 +by (rtac le_anti_sym 1);
16.209 +by (rtac deg_smult_ring 1);
16.210 +by (case_tac "a = <0>" 1);
16.211 +by (REPEAT (asm_simp_tac (simpset() addsimps [deg_belowI, deg_lcoeff]) 1));
16.212 +qed "deg_smult";
16.213 +
16.214 +Goal
16.215 + "!! p::'a::ring up. [| deg p + deg q < k |] ==> \
16.216 +\ coeff i p * coeff (k - i) q = <0>";
16.217 +by (simp_tac (simpset() addsimps [coeff_def]) 1);
16.218 +by (rtac bound_mult_zero 1);
16.219 +by (assume_tac 3);
16.220 +by (simp_tac (simpset() addsimps [deg_above_is_bound RS sym]) 1);
16.221 +by (simp_tac (simpset() addsimps [deg_above_is_bound RS sym]) 1);
16.222 +qed "deg_above_mult_zero";
16.223 +
16.224 +Goal
16.225 + "!! p::'a::ring up. deg (p * q) <= deg p + deg q";
16.226 +by (rtac deg_aboveI 1);
16.227 +by (asm_simp_tac (simpset() addsimps [deg_above_mult_zero]) 1);
16.228 +qed "deg_mult_ring";
16.229 +
16.230 +goal Main.thy
16.231 + "!!k::nat. k < n ==> m < n + m - k";
16.232 +by (arith_tac 1);
16.233 +qed "less_add_diff";
16.234 +
16.235 +Goal "!!p. coeff n p ~= <0> ==> n <= deg p";
16.236 +(* More general than deg_belowI, and simplifies the next proof! *)
16.237 +by (rtac deg_belowI 1);
16.238 +by (Fast_tac 1);
16.239 +qed "deg_below2I";
16.240 +
16.241 +Goal
16.242 + "!! p::'a::domain up. \
16.243 +\ [| p ~= <0>; q ~= <0> |] ==> deg (p * q) = deg p + deg q";
16.244 +by (rtac le_anti_sym 1);
16.245 +by (rtac deg_mult_ring 1);
16.246 +(* deg p + deg q <= deg (p * q) *)
16.247 +by (rtac deg_below2I 1);
16.248 +by (Simp_tac 1);
16.249 +(*
16.250 +by (rtac conjI 1);
16.251 +by (rtac impI 1);
16.252 +*)
16.253 +by (res_inst_tac [("m", "deg p"), ("n", "deg p + deg q")] SUM_extend 1);
16.254 +by (rtac le_add1 1);
16.255 +by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
16.256 +by (res_inst_tac [("m", "deg p"), ("n", "deg p")] SUM_extend_below 1);
16.257 +by (rtac le_refl 1);
16.258 +by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
16.259 +by (asm_simp_tac (simpset() addsimps [nonzero_lcoeff]) 1);
16.260 +(*
16.261 +by (rtac impI 1);
16.262 +by (res_inst_tac [("m", "deg p"), ("n", "deg p + deg q")] SUM_extend 1);
16.263 +by (rtac le_add1 1);
16.264 +by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
16.265 +by (res_inst_tac [("m", "deg p"), ("n", "deg p")] SUM_extend_below 1);
16.266 +by (rtac le_refl 1);
16.267 +by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
16.268 +by (asm_simp_tac (simpset() addsimps [nonzero_lcoeff]) 1);
16.269 +*)
16.270 +qed "deg_mult";
16.271 +
16.272 +Addsimps [deg_smult, deg_mult];
16.273 +
16.274 +(* Representation theorems about polynomials *)
16.275 +
16.276 +goal PolyRing.thy
16.277 + "!! p::nat=>'a::ring up. coeff k (SUM n p) = SUM n (%i. coeff k (p i))";
16.278 +by (nat_ind_tac "n" 1);
16.279 +(* Base case *)
16.280 +by (Simp_tac 1);
16.281 +(* Induction step *)
16.282 +by (Asm_simp_tac 1);
16.283 +qed "coeff_SUM";
16.284 +
16.285 +goal UnivPoly.thy
16.286 + "!! f::(nat=>'a::ring). \
16.287 +\ bound n f ==> SUM n (%i. if i = x then f i else <0>) = f x";
16.288 +by (simp_tac (simpset() addsimps [SUM_if_singleton]) 1);
16.289 +by (auto_tac
16.290 + (claset() addDs [not_leE],
16.291 + simpset() setloop (split_tac [expand_if])));
16.292 +qed "bound_SUM_if";
16.293 +
16.294 +Goal
16.295 + "!! p::'a::ring up. deg p <= n ==> SUM n (%i. coeff i p *s monom i) = p";
16.296 +by (rtac up_eqI 1);
16.297 +by (simp_tac (simpset() addsimps [coeff_SUM]) 1);
16.298 +by (rtac trans 1);
16.299 +by (res_inst_tac [("x", "na")] bound_SUM_if 2);
16.300 +by (full_simp_tac (simpset() addsimps [deg_above_is_bound, coeff_def]) 2);
16.301 +by (rtac SUM_cong 1);
16.302 +by (rtac refl 1);
16.303 +by (asm_simp_tac
16.304 + (simpset() setloop (split_tac [expand_if])) 1);
16.305 +qed "up_repr";
16.306 +
16.307 +Goal
16.308 + "!! p::'a::ring up. [| deg p <= n; P p |] ==> \
16.309 +\ P (SUM n (%i. coeff i p *s monom i))";
16.310 +by (asm_simp_tac (simpset() addsimps [up_repr]) 1);
16.311 +qed "up_reprD";
16.312 +
16.313 +Goal
16.314 + "!! p::'a::ring up. [| deg p <= n; P (SUM n (%i. coeff i p *s monom i)) |] \
16.315 +\ ==> P p";
16.316 +by (asm_full_simp_tac (simpset() addsimps [up_repr]) 1);
16.317 +qed "up_repr2D";
16.318 +
16.319 +(*
16.320 +Goal
16.321 + "!! p::'a::ring up. [| deg p <= n; deg q <= m |] ==> \
16.322 +\ (SUM n (%i. coeff i p *s monom i) = SUM m (%i. coeff i q *s monom i)) \
16.323 +\ = (coeff k f = coeff k g)
16.324 +...
16.325 +qed "up_unique";
16.326 +*)
16.327 +
16.328 +(* Polynomials over integral domains are again integral domains *)
16.329 +
16.330 +Goal "!!p::'a::domain up. p * q = <0> ==> p = <0> | q = <0>";
16.331 +by (rtac classical 1);
16.332 +by (subgoal_tac "deg p = 0 & deg q = 0" 1);
16.333 +by (res_inst_tac [("p", "p"), ("n", "0")] up_repr2D 1);
16.334 +by (Asm_simp_tac 1);
16.335 +by (res_inst_tac [("p", "q"), ("n", "0")] up_repr2D 1);
16.336 +by (Asm_simp_tac 1);
16.337 +by (subgoal_tac "coeff 0 p = <0> | coeff 0 q = <0>" 1);
16.338 +by (SELECT_GOAL (auto_tac (claset() addIs [up_eqI], simpset())) 1);
16.339 +by (rtac integral 1);
16.340 +by (subgoal_tac "coeff 0 (p * q) = <0>" 1);
16.341 +by (Full_simp_tac 1);
16.342 +by (Asm_simp_tac 1);
16.343 +
16.344 +by (dres_inst_tac [("f", "deg")] arg_cong 1);
16.345 +by (Asm_full_simp_tac 1);
16.346 +qed "up_integral";
16.347 +
16.348 +Goal "!! a::'a::domain. a *s p = <0> ==> a = <0> | p = <0>";
16.349 +by (full_simp_tac (simpset() addsimps [const_mult_is_smult RS sym]) 1);
16.350 +by (dtac up_integral 1);
16.351 +by Auto_tac;
16.352 +by (rtac (const_inj RS injD) 1);
16.353 +by (Simp_tac 1);
16.354 +qed "smult_integral";
16.355 +
16.356 +(* Divisibility and degree *)
16.357 +
16.358 +Goalw [dvd_def]
16.359 + "!! p::'a::domain up. [| p dvd q; q ~= <0> |] ==> deg p <= deg q";
16.360 +by (etac exE 1);
16.361 +by (hyp_subst_tac 1);
16.362 +by (case_tac "p = <0>" 1);
16.363 +by (Asm_simp_tac 1);
16.364 +by (dtac r_nullD 1);
16.365 +by (asm_simp_tac (simpset() addsimps [le_add1]) 1);
16.366 +qed "dvd_imp_deg";
17.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
17.2 +++ b/src/HOL/Algebra/poly/Degree.thy Fri Nov 05 11:14:26 1999 +0100
17.3 @@ -0,0 +1,15 @@
17.4 +(*
17.5 + Degree of polynomials
17.6 + $Id$
17.7 + written by Clemens Ballarin, started 22. 1. 1997
17.8 +*)
17.9 +
17.10 +Degree = PolyRing +
17.11 +
17.12 +consts
17.13 + deg :: ('a::ringS) up => nat
17.14 +
17.15 +defs
17.16 + deg_def "deg p == LEAST n. bound n (Rep_UP p)"
17.17 +
17.18 +end
18.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
18.2 +++ b/src/HOL/Algebra/poly/LongDiv.ML Fri Nov 05 11:14:26 1999 +0100
18.3 @@ -0,0 +1,214 @@
18.4 +(*
18.5 + Long division of polynomials
18.6 + $Id$
18.7 + Author: Clemens Ballarin, started 23 June 1999
18.8 +*)
18.9 +
18.10 +open LongDiv;
18.11 +
18.12 +(*
18.13 +Goalw [lcoeff_def]
18.14 + "!!p::('a::ring up). \
18.15 +\ [| deg p = deg q; lcoeff p = - (lcoeff q); deg q ~= 0 |] ==> \
18.16 +\ deg (p + q) < deg q";
18.17 +by (res_inst_tac [("j", "deg q - 1")] le_less_trans 1);
18.18 +by (rtac deg_aboveI 1);
18.19 +by (strip_tac 1);
18.20 +by (dtac pred_less_imp_le 1);
18.21 +by (case_tac "deg q = m" 1);
18.22 +by (Clarify_tac 1);
18.23 +by (Asm_full_simp_tac 1);
18.24 +(* case "deg q ~= m" *)
18.25 +by (dtac le_neq_implies_less 1);
18.26 +by (assume_tac 1);
18.27 +by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
18.28 +(* end case *)
18.29 +by (asm_full_simp_tac (simpset() addsimps [le_pred_eq]) 1);
18.30 +qed "deg_lcoeff_cancel";
18.31 +*)
18.32 +
18.33 +Goal
18.34 + "!!p::('a::ring up). \
18.35 +\ [| deg p <= deg r; deg q <= deg r; \
18.36 +\ coeff (deg r) p = - (coeff (deg r) q); deg r ~= 0 |] ==> \
18.37 +\ deg (p + q) < deg r";
18.38 +by (res_inst_tac [("j", "deg r - 1")] le_less_trans 1);
18.39 +by (rtac deg_aboveI 1);
18.40 +by (strip_tac 1);
18.41 +by (dtac pred_less_imp_le 1);
18.42 +by (case_tac "deg r = m" 1);
18.43 +by (Clarify_tac 1);
18.44 +by (Asm_full_simp_tac 1);
18.45 +(* case "deg q ~= m" *)
18.46 +by (dtac le_neq_implies_less 1 THEN atac 1);
18.47 +by (dres_inst_tac [("i", "deg p")] le_less_trans 1); by (assume_tac 1);
18.48 +by (dres_inst_tac [("i", "deg q")] le_less_trans 1); by (assume_tac 1);
18.49 +by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
18.50 +(* end case *)
18.51 +by (asm_full_simp_tac (simpset() addsimps [le_pred_eq]) 1);
18.52 +qed "deg_lcoeff_cancel";
18.53 +
18.54 +Goal
18.55 + "!!p::('a::ring up). \
18.56 +\ [| deg p <= deg r; deg q <= deg r; \
18.57 +\ p ~= -q; coeff (deg r) p = - (coeff (deg r) q) |] ==> \
18.58 +\ deg (p + q) < deg r";
18.59 +by (rtac deg_lcoeff_cancel 1);
18.60 +by (REPEAT (atac 1));
18.61 +by (rtac classical 1);
18.62 +by (Clarify_tac 1);
18.63 +by (etac notE 1);
18.64 +by (res_inst_tac [("p", "p")] up_repr2D 1 THEN atac 1);
18.65 +by (res_inst_tac [("p", "q")] up_repr2D 1 THEN atac 1);
18.66 +by (rotate_tac ~1 1);
18.67 +by (asm_full_simp_tac (simpset() addsimps [smult_l_minus]) 1);
18.68 +qed "deg_lcoeff_cancel2";
18.69 +
18.70 +Goal
18.71 + "!!g::('a::ring up). g ~= <0> ==> \
18.72 +\ Ex (% (q, r, k). \
18.73 +\ (lcoeff g)^k *s f = q * g + r & (eucl_size r < eucl_size g))";
18.74 +by (res_inst_tac [("P", "%f. Ex (% (q, r, k). \
18.75 +\ (lcoeff g)^k *s f = q * g + r & (eucl_size r < eucl_size g))")]
18.76 + wf_induct 1);
18.77 +(* TO DO: replace by measure_induct *)
18.78 +by (res_inst_tac [("f", "eucl_size")] wf_measure 1);
18.79 +by (case_tac "eucl_size x < eucl_size g" 1);
18.80 +by (res_inst_tac [("x", "(<0>, x, 0)")] exI 1);
18.81 +by (Asm_simp_tac 1);
18.82 +(* case "eucl_size x >= eucl_size g" *)
18.83 +by (dres_inst_tac [("x", "lcoeff g *s x -- (lcoeff x *s monom (deg x - deg g)) * g")] spec 1);
18.84 +by (etac impE 1);
18.85 +by (full_simp_tac (simpset() addsimps [inv_image_def, measure_def, lcoeff_def]) 1);
18.86 +by (case_tac "x = <0>" 1);
18.87 +by (rotate_tac ~1 1);
18.88 +by (asm_full_simp_tac (simpset() addsimps [eucl_size_def]) 1);
18.89 +(* case "x ~= <0> *)
18.90 +by (rotate_tac ~1 1);
18.91 +by (asm_full_simp_tac (simpset() addsimps [eucl_size_def]) 1);
18.92 +by (simp_tac (simpset() addsplits [expand_if]) 1);
18.93 +by (rtac impI 1);
18.94 +by (rtac deg_lcoeff_cancel2 1);
18.95 + (* replace by linear arithmetic??? *)
18.96 + by (rtac le_trans 1);
18.97 + by (rtac deg_smult_ring 1);
18.98 + by (simp_tac (simpset() addsplits [expand_if]) 1);
18.99 + by (Simp_tac 1);
18.100 + by (rtac le_trans 1);
18.101 + by (rtac deg_mult_ring 1);
18.102 + by (rtac le_trans 1);
18.103 + by (rtac add_le_mono1 1);
18.104 + by (rtac deg_smult_ring 1);
18.105 + by (asm_simp_tac (simpset() addsimps [leI] addsplits [expand_if]) 1);
18.106 +by (SELECT_GOAL Auto_tac 1);
18.107 +by (Simp_tac 1);
18.108 +by (res_inst_tac [("m", "deg x - deg g"), ("n", "deg x")] SUM_extend 1);
18.109 +by (Simp_tac 1);
18.110 +by (asm_simp_tac (simpset() addsimps [less_not_refl2 RS not_sym]) 1);
18.111 +by (res_inst_tac [("m", "deg x - deg g"), ("n", "deg x - deg g")]
18.112 + SUM_extend_below 1);
18.113 +by (rtac le_refl 1);
18.114 +by (asm_simp_tac (simpset() addsimps [less_not_refl2]) 1);
18.115 +by (asm_simp_tac (simpset() addsimps [diff_diff_right, leI, m_comm]) 1);
18.116 +(* end of subproof deg f1 < deg f *)
18.117 +by (etac exE 1);
18.118 +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);
18.119 +by (Clarify_tac 1);
18.120 +by (rtac conjI 1);
18.121 +by (dtac sym 1);
18.122 +by (simp_tac (simpset() addsimps [l_distr, a_assoc]) 1);
18.123 +by (Asm_simp_tac 1);
18.124 +by (simp_tac (simpset() addsimps a_ac@[smult_l_distr, smult_r_distr, smult_r_minus, smult_assoc2, smult_assoc1]) 1);
18.125 +by Auto_tac;
18.126 +qed "long_div_eucl_size";
18.127 +
18.128 +Goal
18.129 + "!!g::('a::ring up). g ~= <0> ==> \
18.130 +\ Ex (% (q, r, k). \
18.131 +\ (lcoeff g)^k *s f = q * g + r & (r = <0> | deg r < deg g))";
18.132 +by (forw_inst_tac [("f", "f")]
18.133 + (simplify (simpset() addsimps [eucl_size_def]) long_div_eucl_size) 1);
18.134 +by Auto_tac;
18.135 +by (case_tac "aa = <0>" 1);
18.136 +by (Blast_tac 1);
18.137 +(* case "aa ~= <0> *)
18.138 +by (rotate_tac ~1 1);
18.139 +by Auto_tac;
18.140 +qed "long_div_ring";
18.141 +
18.142 +Goal
18.143 + "!!g::('a::ring up). [| g ~= <0>; (lcoeff g) dvd <1> |] ==> \
18.144 +\ Ex (% (q, r). f = q * g + r & (r = <0> | deg r < deg g))";
18.145 +by (forw_inst_tac [("f", "f")] long_div_ring 1);
18.146 +by (etac exE 1);
18.147 +by (res_inst_tac [("x", "((%(q,r,k). (Ring.inverse(lcoeff g ^k) *s q)) x, \
18.148 +\ (%(q,r,k). Ring.inverse(lcoeff g ^k) *s r) x)")] exI 1);
18.149 +by (Clarify_tac 1);
18.150 +by (Simp_tac 1);
18.151 +by (rtac conjI 1);
18.152 +by (dtac sym 1);
18.153 +by (asm_simp_tac (simpset() addsimps [smult_r_distr RS sym, smult_assoc2]) 1);
18.154 +by (asm_simp_tac (simpset() addsimps [l_inverse_ring, unit_power, smult_assoc1 RS sym]) 1);
18.155 +(* degree property *)
18.156 +by (etac disjE 1);
18.157 +by (Asm_simp_tac 1);
18.158 +by (rtac disjI2 1);
18.159 +by (rtac le_less_trans 1);
18.160 +by (rtac deg_smult_ring 1);
18.161 +by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
18.162 +qed "long_div_unit";
18.163 +
18.164 +Goal
18.165 + "!!g::('a::field up). g ~= <0> ==> \
18.166 +\ Ex (% (q, r). f = q * g + r & (r = <0> | deg r < deg g))";
18.167 +by (rtac long_div_unit 1);
18.168 +by (assume_tac 1);
18.169 +by (asm_simp_tac (simpset() addsimps [lcoeff_def, nonzero_lcoeff, field_ax]) 1);
18.170 +qed "long_div_theorem";
18.171 +
18.172 +Goal
18.173 + "!!g::('a::field up). [| g ~= <0>; \
18.174 +\ f = q1 * g + r1; (r1 = <0> | deg r1 < deg g); \
18.175 +\ f = q2 * g + r2; (r2 = <0> | deg r2 < deg g) |] ==> q1 = q2";
18.176 +by (subgoal_tac "(q1 -- q2) * g = r2 -- r1" 1); (* 1 *)
18.177 +by (thin_tac "f = ?x" 1);
18.178 +by (thin_tac "f = ?x" 1);
18.179 +by (rtac diff_zero_imp_eq 1);
18.180 +by (rtac classical 1);
18.181 +by (etac disjE 1);
18.182 +(* r1 = <0> *)
18.183 +by (etac disjE 1);
18.184 +(* r2 = <0> *)
18.185 +by (SELECT_GOAL (auto_tac (claset() addDs [integral], simpset())) 1);
18.186 +(* r2 ~= <0> *)
18.187 +by (dres_inst_tac [("f", "deg"), ("y", "r2 -- r1")] arg_cong 1);
18.188 +by (SELECT_GOAL Auto_tac 1);
18.189 +(* r1 ~=<0> *)
18.190 +by (etac disjE 1);
18.191 +(* r2 = <0> *)
18.192 +by (dres_inst_tac [("f", "deg"), ("y", "r2 -- r1")] arg_cong 1);
18.193 +by (SELECT_GOAL Auto_tac 1);
18.194 +(* r2 ~= <0> *)
18.195 +by (dres_inst_tac [("f", "deg"), ("y", "r2 -- r1")] arg_cong 1);
18.196 +by (SELECT_GOAL Auto_tac 1);
18.197 +by (dtac (order_eq_refl RS add_leD2) 1);
18.198 +by (dtac leD 1);
18.199 +by (etac notE 1 THEN rtac (deg_add RS le_less_trans) 1);
18.200 +by (Asm_simp_tac 1);
18.201 +(* proof of 1 *)
18.202 +by (rtac diff_zero_imp_eq 1);
18.203 +by (Asm_full_simp_tac 1);
18.204 +by (dres_inst_tac [("a", "?x+?y")] eq_imp_diff_zero 1);
18.205 +by (asm_full_simp_tac (simpset() addsimps (l_distr::minus_add::l_minus::a_ac)) 1);
18.206 +qed "long_div_quo_unique";
18.207 +
18.208 +Goal
18.209 + "!!g::('a::field up). [| g ~= <0>; \
18.210 +\ f = q1 * g + r1; (r1 = <0> | deg r1 < deg g); \
18.211 +\ f = q2 * g + r2; (r2 = <0> | deg r2 < deg g) |] ==> r1 = r2";
18.212 +by (subgoal_tac "q1 = q2" 1);
18.213 +by (Clarify_tac 1);
18.214 +by (asm_full_simp_tac (simpset() addsimps [a_lcancel_eq]) 1);
18.215 +by (rtac long_div_quo_unique 1);
18.216 +by (REPEAT (atac 1));
18.217 +qed "long_div_rem_unique";
19.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
19.2 +++ b/src/HOL/Algebra/poly/LongDiv.thy Fri Nov 05 11:14:26 1999 +0100
19.3 @@ -0,0 +1,18 @@
19.4 +(*
19.5 + Experimental theory: long division of polynomials
19.6 + $Id$
19.7 + Author: Clemens Ballarin, started 23 June 1999
19.8 +*)
19.9 +
19.10 +LongDiv = PolyHomo +
19.11 +
19.12 +consts
19.13 + lcoeff :: "'a::ringS up => 'a"
19.14 + eucl_size :: 'a::ringS => nat
19.15 +
19.16 +defs
19.17 + lcoeff_def "lcoeff p == coeff (deg p) p"
19.18 + eucl_size_def "eucl_size p == if p = <0> then 0 else deg p+1"
19.19 +
19.20 +end
19.21 +
20.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
20.2 +++ b/src/HOL/Algebra/poly/PolyHomo.ML Fri Nov 05 11:14:26 1999 +0100
20.3 @@ -0,0 +1,127 @@
20.4 +(*
20.5 + Universal property and evaluation homomorphism of univariate polynomials
20.6 + $Id$
20.7 + Author: Clemens Ballarin, started 16 April 1997
20.8 +*)
20.9 +
20.10 +(* Ring homomorphisms and polynomials *)
20.11 +
20.12 +Goal "homo (const::'a::ring=>'a up)";
20.13 +by (auto_tac (claset() addSIs [homoI], simpset()));
20.14 +qed "const_homo";
20.15 +
20.16 +Delsimps [const_add, const_mult, const_one, const_zero];
20.17 +Addsimps [const_homo];
20.18 +
20.19 +Goal
20.20 + "!!f::'a::ring up=>'b::ring. homo f ==> f (a *s p) = f (const a) * f p";
20.21 +by (asm_simp_tac (simpset() addsimps [const_mult_is_smult RS sym]) 1);
20.22 +qed "homo_smult";
20.23 +
20.24 +Addsimps [homo_smult];
20.25 +
20.26 +(* Evaluation homomorphism *)
20.27 +
20.28 +Goal
20.29 + "!! phi::('a::ring=>'b::ring). homo phi ==> homo (EVAL2 phi a)";
20.30 +by (rtac homoI 1);
20.31 +by (rewtac EVAL2_def);
20.32 +(* + commutes *)
20.33 +(* degree estimations:
20.34 + bound of all sums can be extended to max (deg aa) (deg b) *)
20.35 +by (res_inst_tac [("m", "deg (aa + b)"), ("n", "max (deg aa) (deg b)")]
20.36 + SUM_shrink 1);
20.37 +by (rtac deg_add 1);
20.38 +by (asm_simp_tac (simpset() delsimps [coeff_add] addsimps [deg_aboveD]) 1);
20.39 +by (res_inst_tac [("m", "deg aa"), ("n", "max (deg aa) (deg b)")]
20.40 + SUM_shrink 1);
20.41 +by (rtac le_maxI1 1);
20.42 +by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
20.43 +by (res_inst_tac [("m", "deg b"), ("n", "max (deg aa) (deg b)")]
20.44 + SUM_shrink 1);
20.45 +by (rtac le_maxI2 1);
20.46 +by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
20.47 +(* actual homom property + *)
20.48 +by (asm_simp_tac (simpset() addsimps [l_distr, SUM_add]) 1);
20.49 +
20.50 +(* * commutes *)
20.51 +by (res_inst_tac [("m", "deg (aa * b)"), ("n", "deg aa + deg b")]
20.52 + SUM_shrink 1);
20.53 +by (rtac deg_mult_ring 1);
20.54 +by (asm_simp_tac (simpset() delsimps [coeff_mult] addsimps [deg_aboveD]) 1);
20.55 +by (rtac trans 1);
20.56 +by (rtac CauchySum 2);
20.57 +by (asm_simp_tac (simpset() addsimps [boundI, deg_aboveD]) 2);
20.58 +by (asm_simp_tac (simpset() addsimps [boundI, deg_aboveD]) 2);
20.59 +(* getting a^i and a^(k-i) together is difficult, so we do is manually *)
20.60 +by (res_inst_tac [("s",
20.61 +" SUM (deg aa + deg b) \
20.62 +\ (%k. SUM k \
20.63 +\ (%i. phi (coeff i aa) * (phi (coeff (k - i) b) * \
20.64 +\ (a ^ i * a ^ (k - i)))))")] trans 1);
20.65 +by (asm_simp_tac (simpset()
20.66 + addsimps [power_mult, leD RS add_diff_inverse, SUM_ldistr]) 1);
20.67 +by (simp_tac (simpset() addsimps m_ac) 1);
20.68 +by (simp_tac (simpset() addsimps m_ac) 1);
20.69 +(* <1> commutes *)
20.70 +by (Asm_simp_tac 1);
20.71 +qed "EVAL2_homo";
20.72 +
20.73 +Goalw [EVAL2_def]
20.74 + "!! phi::'a::ring=>'b::ring. EVAL2 phi a (const b) = phi b";
20.75 +by (Simp_tac 1);
20.76 +qed "EVAL2_const";
20.77 +
20.78 +(* This is probably redundant *)
20.79 +Goalw [EVAL2_def]
20.80 + "!! phi::'a::ring=>'b::ring. homo phi ==> EVAL2 phi a (monom 1) = a";
20.81 +by (Asm_simp_tac 1);
20.82 +qed "EVAL2_monom1";
20.83 +
20.84 +Goalw [EVAL2_def]
20.85 + "!! phi::'a::ring=>'b::ring. homo phi ==> EVAL2 phi a (monom n) = a ^ n";
20.86 +by (Simp_tac 1);
20.87 +by (nat_ind_tac "n" 1); (* really a case split *)
20.88 +by (Asm_simp_tac 1);
20.89 +by (Asm_simp_tac 1);
20.90 +qed "EVAL2_monom";
20.91 +
20.92 +Goal
20.93 + "!! phi::'a::ring=>'b::ring. \
20.94 +\ homo phi ==> EVAL2 phi a (b *s p) = phi b * EVAL2 phi a p";
20.95 +by (asm_simp_tac
20.96 + (simpset() addsimps [const_mult_is_smult RS sym, EVAL2_homo, EVAL2_const]) 1);
20.97 +qed "EVAL2_smult";
20.98 +
20.99 +Goalw [EVAL_def] "!! a::'a::ring. homo (EVAL a)";
20.100 +by (asm_simp_tac (simpset() addsimps [EVAL2_homo, id_homo]) 1);
20.101 +qed "EVAL_homo";
20.102 +
20.103 +Goalw [EVAL_def] "!! a::'a::ring. EVAL a (const b) = b";
20.104 +by (asm_simp_tac (simpset() addsimps [EVAL2_const]) 1);
20.105 +qed "EVAL_const";
20.106 +
20.107 +Goalw [EVAL_def] "!! a::'a::ring. EVAL a (monom n) = a ^ n";
20.108 +by (asm_simp_tac (simpset() addsimps [EVAL2_monom]) 1);
20.109 +qed "EVAL_monom";
20.110 +
20.111 +Goalw [EVAL_def] "!! a::'a::ring. EVAL a (b *s p) = b * EVAL a p";
20.112 +by (asm_simp_tac (simpset() addsimps [EVAL2_smult]) 1);
20.113 +qed "EVAL_smult";
20.114 +
20.115 +(* Examples *)
20.116 +
20.117 +Goal
20.118 + "EVAL (x::'a::ring) (a*X^2 + b*X^1 + c*X^0) = a * x ^ 2 + b * x ^ 1 + c";
20.119 +by (asm_simp_tac (simpset() delsimps [power_Suc]
20.120 + addsimps [EVAL_homo, EVAL_monom, EVAL_smult]) 1);
20.121 +result();
20.122 +
20.123 +Goal
20.124 + "EVAL (y::'a::ring) \
20.125 +\ (EVAL (const x) (monom 1 + const (a*X^2 + b*X^1 + c*X^0))) = \
20.126 +\ x ^ 1 + (a * y ^ 2 + b * y ^ 1 + c)";
20.127 +by (asm_simp_tac (simpset() delsimps [power_Suc]
20.128 + addsimps [EVAL_homo, EVAL_monom, EVAL_smult, EVAL_const]) 1);
20.129 +result();
20.130 +
21.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
21.2 +++ b/src/HOL/Algebra/poly/PolyHomo.thy Fri Nov 05 11:14:26 1999 +0100
21.3 @@ -0,0 +1,22 @@
21.4 +(*
21.5 + Universal property and evaluation homomorphism of univariate polynomials
21.6 + $Id$
21.7 + Author: Clemens Ballarin, started 15 April 1997
21.8 +*)
21.9 +
21.10 +PolyHomo = Degree +
21.11 +
21.12 +(* Instantiate result from Degree.ML *)
21.13 +
21.14 +instance
21.15 + up :: (domain) domain (up_integral)
21.16 +
21.17 +consts
21.18 + EVAL2 :: ('a::ringS => 'b) => 'b => 'a up => 'b::ringS
21.19 + EVAL :: 'a => 'a up => 'a
21.20 +
21.21 +defs
21.22 + EVAL2_def "EVAL2 phi a p == SUM (deg p) (%i. phi (coeff i p) * a ^ i)"
21.23 + EVAL_def "EVAL == EVAL2 (%x. x)"
21.24 +
21.25 +end
22.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
22.2 +++ b/src/HOL/Algebra/poly/PolyRing.ML Fri Nov 05 11:14:26 1999 +0100
22.3 @@ -0,0 +1,96 @@
22.4 +(*
22.5 + Instantiate polynomials to form a ring and prove further properties
22.6 + $Id$
22.7 + Author: Clemens Ballarin, started 22 January 1997
22.8 +*)
22.9 +
22.10 +open PolyRing;
22.11 +
22.12 +(* Properties of *s:
22.13 + Polynomials form a module *)
22.14 +
22.15 +goal UnivPoly.thy "!!a::'a::ring. (a + b) *s p = a *s p + b *s p";
22.16 +by (rtac up_eqI 1);
22.17 +by (simp_tac (simpset() addsimps [l_distr]) 1);
22.18 +qed "smult_l_distr";
22.19 +
22.20 +goal UnivPoly.thy "!!a::'a::ring. a *s (p + q) = a *s p + a *s q";
22.21 +by (rtac up_eqI 1);
22.22 +by (simp_tac (simpset() addsimps [r_distr]) 1);
22.23 +qed "smult_r_distr";
22.24 +
22.25 +goal UnivPoly.thy "!!a::'a::ring. (a * b) *s p = a *s (b *s p)";
22.26 +by (rtac up_eqI 1);
22.27 +by (simp_tac (simpset() addsimps [m_assoc]) 1);
22.28 +qed "smult_assoc1";
22.29 +
22.30 +goal UnivPoly.thy "(<1>::'a::ring) *s p = p";
22.31 +by (rtac up_eqI 1);
22.32 +by (Simp_tac 1);
22.33 +qed "smult_one";
22.34 +
22.35 +(* Polynomials form an algebra *)
22.36 +
22.37 +goal UnivPoly.thy "!!a::'a::ring. (a *s p) * q = a *s (p * q)";
22.38 +by (rtac up_eqI 1);
22.39 +by (simp_tac (simpset() addsimps [SUM_rdistr, m_assoc]) 1);
22.40 +qed "smult_assoc2";
22.41 +
22.42 +(* the following can be derived from the above ones,
22.43 + for generality reasons, it is therefore done *)
22.44 +
22.45 +Goal "(<0>::'a::ring) *s p = <0>";
22.46 +by (rtac a_lcancel 1);
22.47 +by (rtac (smult_l_distr RS sym RS trans) 1);
22.48 +by (Simp_tac 1);
22.49 +qed "smult_l_null";
22.50 +
22.51 +Goal "!!a::'a::ring. a *s <0> = <0>";
22.52 +by (rtac a_lcancel 1);
22.53 +by (rtac (smult_r_distr RS sym RS trans) 1);
22.54 +by (Simp_tac 1);
22.55 +qed "smult_r_null";
22.56 +
22.57 +Goal "!!a::'a::ring. (-a) *s p = - (a *s p)";
22.58 +by (rtac a_lcancel 1);
22.59 +by (rtac (r_neg RS sym RSN (2, trans)) 1);
22.60 +by (rtac (smult_l_distr RS sym RS trans) 1);
22.61 +by (simp_tac (simpset() addsimps [smult_l_null, r_neg]) 1);
22.62 +qed "smult_l_minus";
22.63 +
22.64 +Goal "!!a::'a::ring. a *s (-p) = - (a *s p)";
22.65 +by (rtac a_lcancel 1);
22.66 +by (rtac (r_neg RS sym RSN (2, trans)) 1);
22.67 +by (rtac (smult_r_distr RS sym RS trans) 1);
22.68 +by (simp_tac (simpset() addsimps [smult_r_null, r_neg]) 1);
22.69 +qed "smult_r_minus";
22.70 +
22.71 +val smult_minus = [smult_l_minus, smult_r_minus];
22.72 +
22.73 +(* Integrity of smult *)
22.74 +(*
22.75 +Goal
22.76 + "!! a::'a::domain. a *s b = <0> ==> a = <0> | b = <0>";
22.77 +by (simp_tac (simpset() addsimps [disj_commute]) 1);
22.78 +
22.79 +by (rtac (disj_commute RS trans) 1);
22.80 +by (rtac contrapos2 1);
22.81 +by (assume_tac 1);
22.82 +by (rtac up_neqI 1);
22.83 +by (Full_simp_tac 1);
22.84 +by (etac conjE 1);
22.85 +by (rtac not_integral 1);
22.86 +by (assume_tac 1);
22.87 +by (etac contrapos 1);
22.88 +back();
22.89 +by (rtac up_eqI 1);
22.90 +by (Simp_tac 1);
22.91 +
22.92 +by (rtac integral 1);
22.93 +
22.94 +by (etac conjE 1);
22.95 +
22.96 +by (rtac disjCI 1);
22.97 +*)
22.98 +
22.99 +Addsimps [smult_one, smult_l_null, smult_r_null];
23.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
23.2 +++ b/src/HOL/Algebra/poly/PolyRing.thy Fri Nov 05 11:14:26 1999 +0100
23.3 @@ -0,0 +1,15 @@
23.4 +(*
23.5 + Instantiate polynomials to form a ring and prove further properties
23.6 + $Id$
23.7 + Author: Clemens Ballarin, started 20 January 1997
23.8 +*)
23.9 +
23.10 +PolyRing = UnivPoly +
23.11 +
23.12 +instance
23.13 + up :: (ring) ring
23.14 + (up_a_assoc, up_l_zero, up_l_neg, up_a_comm,
23.15 + up_m_assoc, up_l_one, up_l_distr, up_m_comm, up_one_not_zero,
23.16 + up_power_def) {| rtac refl 1 |}
23.17 +
23.18 +end
24.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
24.2 +++ b/src/HOL/Algebra/poly/Polynomial.thy Fri Nov 05 11:14:26 1999 +0100
24.3 @@ -0,0 +1,11 @@
24.4 +(*
24.5 + Summary theory of the development of (not instantiated) polynomials
24.6 + $Id$
24.7 + Author: Clemens Ballarin, started 17 July 1997
24.8 +*)
24.9 +
24.10 +Polynomial = LongDiv
24.11 +
24.12 +
24.13 +
24.14 +
25.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
25.2 +++ b/src/HOL/Algebra/poly/ProtoPoly.ML Fri Nov 05 11:14:26 1999 +0100
25.3 @@ -0,0 +1,32 @@
25.4 +(*
25.5 + Prepearing definitions for polynomials
25.6 + $Id$
25.7 + Author: Clemens Ballarin, started 9 December 1996
25.8 +*)
25.9 +
25.10 +open ProtoPoly;
25.11 +
25.12 +(* Rules for bound *)
25.13 +
25.14 +val prem = goalw ProtoPoly.thy [bound_def]
25.15 + "[| !! m. n < m ==> f m = <0> |] ==> bound n f";
25.16 +by (fast_tac (claset() addIs prem) 1);
25.17 +qed "boundI";
25.18 +
25.19 +Goalw [bound_def]
25.20 + "!! f. [| bound n f; n < m |] ==> f m = <0>";
25.21 +by (Fast_tac 1);
25.22 +qed "boundD";
25.23 +
25.24 +Goalw [bound_def]
25.25 + "!! f. [| bound n f; n <= m |] ==> bound m f";
25.26 +by (fast_tac (set_cs addIs [le_less_trans]) 1);
25.27 +(* Need set_cs, otherwise starts reasoning about naturals *)
25.28 +qed "le_bound";
25.29 +
25.30 +AddSIs [boundI];
25.31 +AddDs [boundD];
25.32 +
25.33 +Goal "(%x. <0>) : {f. EX n. bound n f}";
25.34 +by (Blast_tac 1);
25.35 +qed "UP_witness";
26.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
26.2 +++ b/src/HOL/Algebra/poly/ProtoPoly.thy Fri Nov 05 11:14:26 1999 +0100
26.3 @@ -0,0 +1,15 @@
26.4 +(*
26.5 + Prepearing definitions for polynomials
26.6 + $Id$
26.7 + Author: Clemens Ballarin, started 9 December 1996
26.8 +*)
26.9 +
26.10 +ProtoPoly = Abstract +
26.11 +
26.12 +consts
26.13 + bound :: [nat, nat => 'a::ringS] => bool
26.14 +
26.15 +defs
26.16 + bound_def "bound n f == ALL i. n<i --> f i = <0>"
26.17 +
26.18 +end
27.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
27.2 +++ b/src/HOL/Algebra/poly/UnivPoly.ML Fri Nov 05 11:14:26 1999 +0100
27.3 @@ -0,0 +1,262 @@
27.4 +(*
27.5 + Univariate Polynomials
27.6 + $Id$
27.7 + Author: Clemens Ballarin, started 9 December 1996
27.8 +TODO: monom is *mono*morphism (probably induction needed)
27.9 +*)
27.10 +
27.11 +(* Closure of UP under +, *s, monom, const and * *)
27.12 +
27.13 +Goalw [UP_def]
27.14 + "!! f g. [| f : UP; g : UP |] ==> (%n. (f n + g n::'a::ring)) : UP";
27.15 +by (Step_tac 1);
27.16 +(* instantiate bound for the sum and do case split *)
27.17 +by (res_inst_tac [("x", "if n<=na then na else n")] exI 1);
27.18 +by (case_tac "n <= na" 1);
27.19 +by (Asm_simp_tac 1);
27.20 +by (Asm_simp_tac 2);
27.21 +(* first case, bound of g higher *)
27.22 +by (etac (make_elim le_bound) 1 THEN atac 1);
27.23 +by (REPEAT (Step_tac 1));
27.24 +by (Asm_simp_tac 1);
27.25 +(* second case is identical,
27.26 + apart from we have to massage the inequality *)
27.27 +by (dtac (not_leE RS less_imp_le) 1);
27.28 +by (etac (make_elim le_bound) 1 THEN atac 1);
27.29 +by (REPEAT (Step_tac 1));
27.30 +by (Asm_simp_tac 1);
27.31 +qed "UP_closed_add";
27.32 +
27.33 +Goalw [UP_def]
27.34 + "!! f. f : UP ==> (%n. (a * f n::'a::ring)) : UP";
27.35 +by (REPEAT (Step_tac 1));
27.36 +by (Asm_simp_tac 1);
27.37 +qed "UP_closed_smult";
27.38 +
27.39 +Goalw [UP_def]
27.40 + "!! m. (%n. if m = n then <1> else <0>) : UP";
27.41 +by (Step_tac 1);
27.42 +by (res_inst_tac [("x", "m")] exI 1);
27.43 +by (Step_tac 1);
27.44 +by (dtac (less_not_refl2 RS not_sym) 1);
27.45 +by (Asm_simp_tac 1);
27.46 +qed "UP_closed_monom";
27.47 +
27.48 +Goalw [UP_def]
27.49 + "!! a. (%n. if n = 0 then a else <0>) : UP";
27.50 +by (Step_tac 1);
27.51 +by (res_inst_tac [("x", "0")] exI 1);
27.52 +by (rtac boundI 1);
27.53 +by (asm_simp_tac (simpset() addsimps [less_not_refl2]) 1);
27.54 +qed "UP_closed_const";
27.55 +
27.56 +Goal
27.57 + "!! f::nat=>'a::ring. \
27.58 +\ [| bound n f; bound m g; n + m < k |] ==> f i * g (k - i) = <0>";
27.59 +(* Case split: either f i or g (k - i) is zero *)
27.60 +by (case_tac "n<i" 1);
27.61 +(* First case, f i is zero *)
27.62 +by (SELECT_GOAL Auto_tac 1);
27.63 +(* Second case, we have to derive m < k-i *)
27.64 +by (subgoal_tac "m < k-i" 1);
27.65 +by (SELECT_GOAL Auto_tac 1);
27.66 +(* More inequalities, quite nasty *)
27.67 +by (rtac add_less_imp_less_diff 1);
27.68 +by (stac add_commute 1);
27.69 +by (dtac leI 1);
27.70 +by (rtac le_less_trans 1);
27.71 +by (assume_tac 2);
27.72 +by (asm_simp_tac (simpset() addsimps [add_le_mono1]) 1);
27.73 +qed "bound_mult_zero";
27.74 +
27.75 +Goalw [UP_def]
27.76 + "!! f g. [| f : UP; g : UP |] ==> \
27.77 +\ (%n. (SUM n (%i. f i * g (n-i))::'a::ring)) : UP";
27.78 +by (Step_tac 1);
27.79 +(* Instantiate bound for the product, and remove bound in goal *)
27.80 +by (res_inst_tac [("x", "n + na")] exI 1);
27.81 +by (Step_tac 1);
27.82 +(* Show that the sum is 0 *)
27.83 +by (asm_simp_tac (simpset() addsimps [bound_mult_zero]) 1);
27.84 +qed "UP_closed_mult";
27.85 +
27.86 +(* %x. <0> represents a polynomial *)
27.87 +
27.88 +Goalw [UP_def] "(%x. <0>) : UP";
27.89 +by (Fast_tac 1);
27.90 +qed "UP_zero";
27.91 +
27.92 +(* Effect of +, *s, monom, * and the other operations on the coefficients *)
27.93 +
27.94 +Goalw [coeff_def, up_add_def]
27.95 + "coeff n (p+q) = (coeff n p + coeff n q::'a::ring)";
27.96 +by (asm_simp_tac (simpset() addsimps [Abs_UP_inverse, UP_closed_add, Rep_UP]) 1);
27.97 +qed "coeff_add";
27.98 +
27.99 +Goalw [coeff_def, up_smult_def]
27.100 + "!!a::'a::ring. coeff n (a *s p) = a * coeff n p";
27.101 +by (asm_simp_tac (simpset() addsimps [Abs_UP_inverse, UP_closed_smult, Rep_UP]) 1);
27.102 +qed "coeff_smult";
27.103 +
27.104 +Goalw [coeff_def, monom_def]
27.105 + "coeff n (monom m) = (if m=n then <1> else <0>)";
27.106 +by (asm_simp_tac (simpset() addsimps [Abs_UP_inverse, UP_closed_monom, Rep_UP]) 1);
27.107 +qed "coeff_monom";
27.108 +
27.109 +Goalw [coeff_def, const_def]
27.110 + "coeff n (const a) = (if n=0 then a else <0>)";
27.111 +by (asm_simp_tac (simpset() addsimps [Abs_UP_inverse, UP_closed_const, Rep_UP]) 1);
27.112 +qed "coeff_const";
27.113 +
27.114 +Goalw [coeff_def, up_mult_def]
27.115 + "coeff n (p * q) = (SUM n (%i. coeff i p * coeff (n-i) q)::'a::ring)";
27.116 +by (asm_simp_tac (simpset() addsimps [Abs_UP_inverse, UP_closed_mult, Rep_UP]) 1);
27.117 +qed "coeff_mult";
27.118 +
27.119 +Goalw [coeff_def, up_zero_def] "coeff n <0> = <0>";
27.120 +by (asm_simp_tac (simpset() addsimps [Abs_UP_inverse, UP_zero, Rep_UP]) 1);
27.121 +qed "coeff_zero";
27.122 +
27.123 +Addsimps [coeff_add, coeff_smult, coeff_monom, coeff_const,
27.124 + coeff_mult, coeff_zero];
27.125 +
27.126 +Goalw [up_one_def]
27.127 + "coeff n <1> = (if n=0 then <1> else <0>)";
27.128 +by (Simp_tac 1);
27.129 +qed "coeff_one";
27.130 +
27.131 +Goalw [up_uminus_def] "coeff n (-p) = (-coeff n p::'a::ring)";
27.132 +by (simp_tac (simpset() addsimps m_minus) 1);
27.133 +qed "coeff_uminus";
27.134 +
27.135 +Addsimps [coeff_one, coeff_uminus];
27.136 +
27.137 +(* Polynomials form a ring *)
27.138 +
27.139 +Goalw [coeff_def]
27.140 + "!! p q. [| !! n. coeff n p = coeff n q |] ==> p = q";
27.141 +by (res_inst_tac [("t", "p")] (Rep_UP_inverse RS subst) 1);
27.142 +by (res_inst_tac [("t", "q")] (Rep_UP_inverse RS subst) 1);
27.143 +by (Asm_simp_tac 1);
27.144 +qed "up_eqI";
27.145 +
27.146 +Goalw [coeff_def]
27.147 + "!! p q. coeff n p ~= coeff n q ==> p ~= q";
27.148 +by (etac contrapos 1);
27.149 +by (Asm_simp_tac 1);
27.150 +qed "up_neqI";
27.151 +
27.152 +Goal "!! a::('a::ring) up. (a + b) + c = a + (b + c)";
27.153 +by (rtac up_eqI 1);
27.154 +by (Simp_tac 1);
27.155 +by (rtac a_assoc 1);
27.156 +qed "up_a_assoc";
27.157 +
27.158 +Goal "!! a::('a::ring) up. <0> + a = a";
27.159 +by (rtac up_eqI 1);
27.160 +by (Simp_tac 1);
27.161 +qed "up_l_zero";
27.162 +
27.163 +Goal "!! a::('a::ring) up. (-a) + a = <0>";
27.164 +by (rtac up_eqI 1);
27.165 +by (Simp_tac 1);
27.166 +qed "up_l_neg";
27.167 +
27.168 +Goal "!! a::('a::ring) up. a + b = b + a";
27.169 +by (rtac up_eqI 1);
27.170 +by (Simp_tac 1);
27.171 +by (rtac a_comm 1);
27.172 +qed "up_a_comm";
27.173 +
27.174 +Goal "!! a::('a::ring) up. (a * b) * c = a * (b * c)";
27.175 +by (rtac up_eqI 1);
27.176 +by (Simp_tac 1);
27.177 +by (rtac poly_assoc_lemma 1);
27.178 +qed "up_m_assoc";
27.179 +
27.180 +Goal "!! a::('a::ring) up. <1> * a = a";
27.181 +by (rtac up_eqI 1);
27.182 +by (Simp_tac 1);
27.183 +by (nat_ind_tac "n" 1); (* this is only a case split *)
27.184 +(* Base case *)
27.185 +by (Simp_tac 1);
27.186 +(* Induction step *)
27.187 +by (simp_tac (simpset() delsimps [SUM_Suc] addsimps [SUM_Suc2]) 1);
27.188 +qed "up_l_one";
27.189 +
27.190 +Goal "!! a::('a::ring) up. (a + b) * c = a * c + b * c";
27.191 +by (rtac up_eqI 1);
27.192 +by (simp_tac (simpset() addsimps [l_distr, SUM_add]) 1);
27.193 +qed "up_l_distr";
27.194 +
27.195 +Goal "!! a::('a::ring) up. a * b = b * a";
27.196 +by (rtac up_eqI 1);
27.197 +by (cut_inst_tac [("a", "%i. coeff i a"), ("b", "%i. coeff i b")]
27.198 + poly_comm_lemma 1);
27.199 +by (asm_full_simp_tac (simpset() addsimps [m_comm]) 1);
27.200 +qed "up_m_comm";
27.201 +
27.202 +Goal "<1> ~= (<0>::('a::ring) up)";
27.203 +by (res_inst_tac [("n", "0")] up_neqI 1);
27.204 +by (Simp_tac 1);
27.205 +qed "up_one_not_zero";
27.206 +
27.207 +(* Further algebraic rules *)
27.208 +
27.209 +Goal "!! a::'a::ring. const a * p = a *s p";
27.210 +by (rtac up_eqI 1);
27.211 +by (nat_ind_tac "n" 1); (* really only a case split *)
27.212 +by (Simp_tac 1);
27.213 +by (simp_tac (simpset() delsimps [SUM_Suc] addsimps [SUM_Suc2]) 1);
27.214 +qed "const_mult_is_smult";
27.215 +
27.216 +Goal "!! a::'a::ring. const (a + b) = const a + const b";
27.217 +by (rtac up_eqI 1);
27.218 +by (simp_tac (simpset() setloop (split_tac [expand_if])) 1);
27.219 +qed "const_add";
27.220 +
27.221 +Goal "!! a::'a::ring. const (a * b) = const a * const b";
27.222 +by (simp_tac (simpset() addsimps [const_mult_is_smult]) 1);
27.223 +by (rtac up_eqI 1);
27.224 +by (simp_tac (simpset() setloop (split_tac [expand_if])) 1);
27.225 +qed "const_mult";
27.226 +
27.227 +Goal "const (<1>::'a::ring) = <1>";
27.228 +by (rtac up_eqI 1);
27.229 +by (Simp_tac 1);
27.230 +qed "const_one";
27.231 +
27.232 +Goal "const (<0>::'a::ring) = <0>";
27.233 +by (rtac up_eqI 1);
27.234 +by (simp_tac (simpset() setloop (split_tac [expand_if])) 1);
27.235 +qed "const_zero";
27.236 +
27.237 +Addsimps [const_add, const_mult, const_one, const_zero];
27.238 +
27.239 +Goalw [inj_on_def, UNIV_def, const_def] "inj const";
27.240 +by (Simp_tac 1);
27.241 +by (strip_tac 1);
27.242 +by (dres_inst_tac [("f", "Rep_UP")] arg_cong 1);
27.243 +by (full_simp_tac (simpset() addsimps [Abs_UP_inverse, UP_closed_const,
27.244 + expand_fun_eq]) 1);
27.245 +by (dres_inst_tac [("x", "0")] spec 1);
27.246 +by (Full_simp_tac 1);
27.247 +qed "const_inj";
27.248 +
27.249 +(*Lemma used in PolyHomo*)
27.250 +Goal
27.251 + "!! f::nat=>'a::ring. [| bound n f; bound m g|] ==> \
27.252 +\ SUM (n + m) (%k. SUM k (%i. f i * g (k-i))) = SUM n f * SUM m g";
27.253 +by (simp_tac (simpset() addsimps [SUM_ldistr, DiagSum]) 1);
27.254 +(* SUM_rdistr must be applied after SUM_ldistr ! *)
27.255 +by (simp_tac (simpset() addsimps [SUM_rdistr]) 1);
27.256 +by (res_inst_tac [("m", "n"), ("n", "n+m")] SUM_extend 1);
27.257 +by (rtac le_add1 1);
27.258 +by (SELECT_GOAL Auto_tac 1);
27.259 +by (rtac SUM_cong 1);
27.260 +by (rtac refl 1);
27.261 +by (res_inst_tac [("m", "m"), ("n", "n+m-i")] SUM_shrink 1);
27.262 +by (asm_simp_tac (simpset() addsimps [le_add_diff]) 1);
27.263 +by (SELECT_GOAL Auto_tac 1);
27.264 +by (rtac refl 1);
27.265 +qed "CauchySum";
28.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
28.2 +++ b/src/HOL/Algebra/poly/UnivPoly.thy Fri Nov 05 11:14:26 1999 +0100
28.3 @@ -0,0 +1,42 @@
28.4 +(*
28.5 + Univariate Polynomials
28.6 + $Id$
28.7 + Author: Clemens Ballarin, started 9 December 1996
28.8 +*)
28.9 +
28.10 +UnivPoly = ProtoPoly +
28.11 +
28.12 +typedef (UP)
28.13 + ('a) up = "{f :: nat => 'a::ringS. EX n. bound n f}" (UP_witness)
28.14 +
28.15 +instance
28.16 + up :: (ringS) ringS
28.17 +
28.18 +consts
28.19 + coeff :: [nat, 'a up] => 'a::ringS
28.20 + "*s" :: ['a::ringS, 'a up] => 'a up (infixl 70)
28.21 + monom :: nat => ('a::ringS) up
28.22 + const :: 'a::ringS => 'a up
28.23 +
28.24 + "*X^" :: ['a, nat] => 'a up ("(3_*X^/_)" [71, 71] 70)
28.25 +
28.26 +translations
28.27 + "a *X^ n" == "a *s monom n"
28.28 + (* this translation is only nice for non-nested polynomials *)
28.29 +
28.30 +defs
28.31 + coeff_def "coeff n p == Rep_UP p n"
28.32 + up_add_def "p + q == Abs_UP (%n. Rep_UP p n + Rep_UP q n)"
28.33 + up_smult_def "a *s p == Abs_UP (%n. a * Rep_UP p n)"
28.34 + monom_def "monom m == Abs_UP (%n. if m=n then <1> else <0>)"
28.35 + const_def "const a == Abs_UP (%n. if n=0 then a else <0>)"
28.36 + up_mult_def "p * q == Abs_UP (%n. SUM n
28.37 + (%i. Rep_UP p i * Rep_UP q (n-i)))"
28.38 +
28.39 + up_zero_def "<0> == Abs_UP (%x. <0>)"
28.40 + up_one_def "<1> == monom 0"
28.41 + up_uminus_def "- p == (-<1>) *s p"
28.42 + up_power_def "a ^ n == nat_rec (<1>::('a::ringS) up) (%u b. b * a) n"
28.43 +end
28.44 +
28.45 +