1.1 --- a/src/HOL/Algebra/abstract/Factor.ML Sun Nov 19 13:02:55 2006 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,47 +0,0 @@
1.4 -(*
1.5 - Factorisation within a factorial domain
1.6 - $Id$
1.7 - Author: Clemens Ballarin, started 25 November 1997
1.8 -*)
1.9 -
1.10 -Goalw [thm "assoc_def"] "!! c::'a::factorial. \
1.11 -\ [| irred c; irred a; irred b; c dvd a*b |] ==> c assoc a | c assoc b";
1.12 -by (ftac (thm "factorial_prime") 1);
1.13 -by (rewrite_goals_tac [thm "irred_def", thm "prime_def"]);
1.14 -by (Blast_tac 1);
1.15 -qed "irred_dvd_lemma";
1.16 -
1.17 -Goalw [thm "assoc_def"] "!! c::'a::factorial. \
1.18 -\ [| irred c; a dvd 1 |] ==> \
1.19 -\ (ALL b : set factors. irred b) & c dvd foldr op* factors a --> \
1.20 -\ (EX d. c assoc d & d : set factors)";
1.21 -by (induct_tac "factors" 1);
1.22 -(* Base case: c dvd a contradicts irred c *)
1.23 -by (full_simp_tac (simpset() addsimps [thm "irred_def"]) 1);
1.24 -by (blast_tac (claset() addIs [thm "dvd_trans_ring"]) 1);
1.25 -(* Induction step *)
1.26 -by (ftac (thm "factorial_prime") 1);
1.27 -by (full_simp_tac (simpset() addsimps [thm "irred_def", thm "prime_def"]) 1);
1.28 -by (Blast_tac 1);
1.29 -qed "irred_dvd_list_lemma";
1.30 -
1.31 -Goal "!! c::'a::factorial. \
1.32 -\ [| irred c; ALL b : set factors. irred b; a dvd 1; \
1.33 -\ c dvd foldr op* factors a |] ==> \
1.34 -\ EX d. c assoc d & d : set factors";
1.35 -by (rtac (irred_dvd_list_lemma RS mp) 1);
1.36 -by (Auto_tac);
1.37 -qed "irred_dvd_list";
1.38 -
1.39 -Goalw [thm "Factorisation_def"] "!! c::'a::factorial. \
1.40 -\ [| irred c; Factorisation x factors u; c dvd x |] ==> \
1.41 -\ EX d. c assoc d & d : set factors";
1.42 -by (rtac (irred_dvd_list_lemma RS mp) 1);
1.43 -by (Auto_tac);
1.44 -qed "Factorisation_dvd";
1.45 -
1.46 -Goalw [thm "Factorisation_def"] "!! c::'a::factorial. \
1.47 -\ [| Factorisation x factors u; a : set factors |] ==> irred a";
1.48 -by (Blast_tac 1);
1.49 -qed "Factorisation_irred";
1.50 -
2.1 --- a/src/HOL/Algebra/abstract/Factor.thy Sun Nov 19 13:02:55 2006 +0100
2.2 +++ b/src/HOL/Algebra/abstract/Factor.thy Sun Nov 19 23:48:55 2006 +0100
2.3 @@ -6,11 +6,54 @@
2.4
2.5 theory Factor imports Ring2 begin
2.6
2.7 -constdefs
2.8 - Factorisation :: "['a::ring, 'a list, 'a] => bool"
2.9 +definition
2.10 + Factorisation :: "['a::ring, 'a list, 'a] => bool" where
2.11 (* factorisation of x into a list of irred factors and a unit u *)
2.12 - "Factorisation x factors u ==
2.13 + "Factorisation x factors u \<longleftrightarrow>
2.14 x = foldr op* factors u &
2.15 (ALL a : set factors. irred a) & u dvd 1"
2.16
2.17 +lemma irred_dvd_lemma: "!! c::'a::factorial.
2.18 + [| irred c; irred a; irred b; c dvd a*b |] ==> c assoc a | c assoc b"
2.19 + apply (unfold assoc_def)
2.20 + apply (frule factorial_prime)
2.21 + apply (unfold irred_def prime_def)
2.22 + apply blast
2.23 + done
2.24 +
2.25 +lemma irred_dvd_list_lemma: "!! c::'a::factorial.
2.26 + [| irred c; a dvd 1 |] ==>
2.27 + (ALL b : set factors. irred b) & c dvd foldr op* factors a -->
2.28 + (EX d. c assoc d & d : set factors)"
2.29 + apply (unfold assoc_def)
2.30 + apply (induct_tac factors)
2.31 + (* Base case: c dvd a contradicts irred c *)
2.32 + apply (simp add: irred_def)
2.33 + apply (blast intro: dvd_trans_ring)
2.34 + (* Induction step *)
2.35 + apply (frule factorial_prime)
2.36 + apply (simp add: irred_def prime_def)
2.37 + apply blast
2.38 + done
2.39 +
2.40 +lemma irred_dvd_list: "!! c::'a::factorial.
2.41 + [| irred c; ALL b : set factors. irred b; a dvd 1;
2.42 + c dvd foldr op* factors a |] ==>
2.43 + EX d. c assoc d & d : set factors"
2.44 + apply (rule irred_dvd_list_lemma [THEN mp])
2.45 + apply auto
2.46 + done
2.47 +
2.48 +lemma Factorisation_dvd: "!! c::'a::factorial.
2.49 + [| irred c; Factorisation x factors u; c dvd x |] ==>
2.50 + EX d. c assoc d & d : set factors"
2.51 + apply (unfold Factorisation_def)
2.52 + apply (rule irred_dvd_list_lemma [THEN mp])
2.53 + apply auto
2.54 + done
2.55 +
2.56 +lemma Factorisation_irred: "!! c::'a::factorial.
2.57 + [| Factorisation x factors u; a : set factors |] ==> irred a"
2.58 + unfolding Factorisation_def by blast
2.59 +
2.60 end
3.1 --- a/src/HOL/Algebra/abstract/Ideal2.ML Sun Nov 19 13:02:55 2006 +0100
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,328 +0,0 @@
3.4 -(*
3.5 - Ideals for commutative rings
3.6 - $Id$
3.7 - Author: Clemens Ballarin, started 24 September 1999
3.8 -*)
3.9 -
3.10 -(* is_ideal *)
3.11 -
3.12 -Goalw [thm "is_ideal_def"]
3.13 - "!! I. [| !! a b. [| a:I; b:I |] ==> a + b : I; \
3.14 -\ !! a. a:I ==> - a : I; 0 : I; \
3.15 -\ !! a r. a:I ==> a * r : I |] ==> is_ideal I";
3.16 -by Auto_tac;
3.17 -qed "is_idealI";
3.18 -
3.19 -Goalw [thm "is_ideal_def"] "[| is_ideal I; a:I; b:I |] ==> a + b : I";
3.20 -by (Fast_tac 1);
3.21 -qed "is_ideal_add";
3.22 -
3.23 -Goalw [thm "is_ideal_def"] "[| is_ideal I; a:I |] ==> - a : I";
3.24 -by (Fast_tac 1);
3.25 -qed "is_ideal_uminus";
3.26 -
3.27 -Goalw [thm "is_ideal_def"] "[| is_ideal I |] ==> 0 : I";
3.28 -by (Fast_tac 1);
3.29 -qed "is_ideal_zero";
3.30 -
3.31 -Goalw [thm "is_ideal_def"] "[| is_ideal I; a:I |] ==> a * r : I";
3.32 -by (Fast_tac 1);
3.33 -qed "is_ideal_mult";
3.34 -
3.35 -Goalw [dvd_def, thm "is_ideal_def"] "[| a dvd b; is_ideal I; a:I |] ==> b:I";
3.36 -by (Fast_tac 1);
3.37 -qed "is_ideal_dvd";
3.38 -
3.39 -Goalw [thm "is_ideal_def"] "is_ideal (UNIV::('a::ring) set)";
3.40 -by Auto_tac;
3.41 -qed "UNIV_is_ideal";
3.42 -
3.43 -Goalw [thm "is_ideal_def"] "is_ideal {0::'a::ring}";
3.44 -by Auto_tac;
3.45 -qed "zero_is_ideal";
3.46 -
3.47 -Addsimps [is_ideal_add, is_ideal_uminus, is_ideal_zero, is_ideal_mult,
3.48 - UNIV_is_ideal, zero_is_ideal];
3.49 -
3.50 -Goal "is_ideal {x::'a::ring. a dvd x}";
3.51 -by (rtac is_idealI 1);
3.52 -by Auto_tac;
3.53 -qed "is_ideal_1";
3.54 -
3.55 -Goal "is_ideal {x::'a::ring. EX u v. x = a * u + b * v}";
3.56 -by (rtac is_idealI 1);
3.57 -(* by Auto_tac; FIXME: makes Zumkeller's order fail (raises exn Domain) *)
3.58 -by (Clarify_tac 1);
3.59 -by (Clarify_tac 2);
3.60 -by (Clarify_tac 3);
3.61 -by (Clarify_tac 4);
3.62 -by (res_inst_tac [("x", "u+ua")] exI 1);
3.63 -by (res_inst_tac [("x", "v+va")] exI 1);
3.64 -by (res_inst_tac [("x", "-u")] exI 2);
3.65 -by (res_inst_tac [("x", "-v")] exI 2);
3.66 -by (res_inst_tac [("x", "0")] exI 3);
3.67 -by (res_inst_tac [("x", "0")] exI 3);
3.68 -by (res_inst_tac [("x", "u * r")] exI 4);
3.69 -by (res_inst_tac [("x", "v * r")] exI 4);
3.70 -by (REPEAT (Simp_tac 1));
3.71 -qed "is_ideal_2";
3.72 -
3.73 -(* ideal_of *)
3.74 -
3.75 -Goalw [thm "is_ideal_def", thm "ideal_of_def"] "is_ideal (ideal_of S)";
3.76 -by (Blast_tac 1); (* Here, blast_tac is much superior to fast_tac! *)
3.77 -qed "ideal_of_is_ideal";
3.78 -
3.79 -Goalw [thm "ideal_of_def"] "a:S ==> a : (ideal_of S)";
3.80 -by Auto_tac;
3.81 -qed "generator_in_ideal";
3.82 -
3.83 -Goalw [thm "ideal_of_def"] "ideal_of {1::'a::ring} = UNIV";
3.84 -by (force_tac (claset() addDs [is_ideal_mult],
3.85 - simpset() addsimps [l_one] delsimprocs [ring_simproc]) 1);
3.86 - (* FIXME: Zumkeller's order raises Domain exn *)
3.87 -qed "ideal_of_one_eq";
3.88 -
3.89 -Goalw [thm "ideal_of_def"] "ideal_of {} = {0::'a::ring}";
3.90 -by (rtac subset_antisym 1);
3.91 -by (rtac subsetI 1);
3.92 -by (dtac InterD 1);
3.93 -by (assume_tac 2);
3.94 -by (auto_tac (claset(), simpset() addsimps [is_ideal_zero]));
3.95 -qed "ideal_of_empty_eq";
3.96 -
3.97 -Goalw [thm "ideal_of_def"] "ideal_of {a} = {x::'a::ring. a dvd x}";
3.98 -by (rtac subset_antisym 1);
3.99 -by (rtac subsetI 1);
3.100 -by (dtac InterD 1);
3.101 -by (assume_tac 2);
3.102 -by (auto_tac (claset() addIs [is_ideal_1], simpset()));
3.103 -by (asm_simp_tac (simpset() addsimps [is_ideal_dvd]) 1);
3.104 -qed "pideal_structure";
3.105 -
3.106 -Goalw [thm "ideal_of_def"]
3.107 - "ideal_of {a, b} = {x::'a::ring. EX u v. x = a * u + b * v}";
3.108 -by (rtac subset_antisym 1);
3.109 -by (rtac subsetI 1);
3.110 -by (dtac InterD 1);
3.111 -by (assume_tac 2);
3.112 -by (auto_tac (claset() addIs [is_ideal_2],
3.113 - simpset() delsimprocs [ring_simproc]));
3.114 -(* FIXME: Zumkeller's order *)
3.115 -by (res_inst_tac [("x", "1")] exI 1);
3.116 -by (res_inst_tac [("x", "0")] exI 1);
3.117 -by (res_inst_tac [("x", "0")] exI 2);
3.118 -by (res_inst_tac [("x", "1")] exI 2);
3.119 -by (Simp_tac 1);
3.120 -by (Simp_tac 1);
3.121 -qed "ideal_of_2_structure";
3.122 -
3.123 -Goalw [thm "ideal_of_def"] "A <= B ==> ideal_of A <= ideal_of B";
3.124 -by Auto_tac;
3.125 -qed "ideal_of_mono";
3.126 -
3.127 -Goal "ideal_of {0::'a::ring} = {0}";
3.128 -by (simp_tac (simpset() addsimps [pideal_structure]) 1);
3.129 -by (rtac subset_antisym 1);
3.130 -by (auto_tac (claset() addIs [thm "dvd_zero_left"], simpset()));
3.131 -qed "ideal_of_zero_eq";
3.132 -
3.133 -Goal "[| is_ideal I; a : I |] ==> ideal_of {a::'a::ring} <= I";
3.134 -by (auto_tac (claset(),
3.135 - simpset() addsimps [pideal_structure, is_ideal_dvd]));
3.136 -qed "element_generates_subideal";
3.137 -
3.138 -(* is_pideal *)
3.139 -
3.140 -Goalw [thm "is_pideal_def"] "is_pideal (I::('a::ring) set) ==> is_ideal I";
3.141 -by (fast_tac (claset() addIs [ideal_of_is_ideal]) 1);
3.142 -qed "is_pideal_imp_is_ideal";
3.143 -
3.144 -Goalw [thm "is_pideal_def"] "is_pideal (ideal_of {a::'a::ring})";
3.145 -by (Fast_tac 1);
3.146 -qed "pideal_is_pideal";
3.147 -
3.148 -Goalw [thm "is_pideal_def"] "is_pideal I ==> EX a. I = ideal_of {a}";
3.149 -by (assume_tac 1);
3.150 -qed "is_pidealD";
3.151 -
3.152 -(* Ideals and divisibility *)
3.153 -
3.154 -Goal "b dvd a ==> ideal_of {a::'a::ring} <= ideal_of {b}";
3.155 -by (auto_tac (claset() addIs [thm "dvd_trans_ring"],
3.156 - simpset() addsimps [pideal_structure]));
3.157 -qed "dvd_imp_subideal";
3.158 -
3.159 -Goal "ideal_of {a::'a::ring} <= ideal_of {b} ==> b dvd a";
3.160 -by (auto_tac (claset() addSDs [subsetD],
3.161 - simpset() addsimps [pideal_structure]));
3.162 -qed "subideal_imp_dvd";
3.163 -
3.164 -Goal "(ideal_of {a::'a::ring} <= ideal_of {b}) = (b dvd a)";
3.165 -by (rtac iffI 1);
3.166 -by (REPEAT (ares_tac [subideal_imp_dvd, dvd_imp_subideal] 1));
3.167 -qed "subideal_is_dvd";
3.168 -
3.169 -Goal "(ideal_of {a::'a::ring} < ideal_of {b}) ==> ~ a dvd b";
3.170 -by (full_simp_tac (simpset() addsimps [psubset_eq, pideal_structure]) 1);
3.171 -by (etac conjE 1);
3.172 -by (dres_inst_tac [("c", "a")] subsetD 1);
3.173 -by (auto_tac (claset() addIs [thm "dvd_trans_ring"],
3.174 - simpset()));
3.175 -qed "psubideal_not_dvd";
3.176 -
3.177 -Goal "[| b dvd a; ~ a dvd b |] ==> ideal_of {a::'a::ring} < ideal_of {b}";
3.178 -by (rtac psubsetI 1);
3.179 -by (etac dvd_imp_subideal 1);
3.180 -by (blast_tac (claset() addIs [dvd_imp_subideal, subideal_imp_dvd]) 1);
3.181 -qed "not_dvd_psubideal_singleton";
3.182 -
3.183 -Goal "(ideal_of {a::'a::ring} < ideal_of {b}) = (b dvd a & ~ a dvd b)";
3.184 -by (rtac iffI 1);
3.185 -by (REPEAT (ares_tac
3.186 - [conjI, psubideal_not_dvd, psubset_imp_subset RS subideal_imp_dvd] 1));
3.187 -by (etac conjE 1);
3.188 -by (REPEAT (ares_tac [not_dvd_psubideal_singleton] 1));
3.189 -qed "psubideal_is_dvd";
3.190 -
3.191 -Goal "[| a dvd b; b dvd a |] ==> ideal_of {a::'a::ring} = ideal_of {b}";
3.192 -by (rtac subset_antisym 1);
3.193 -by (REPEAT (ares_tac [dvd_imp_subideal] 1));
3.194 -qed "assoc_pideal_eq";
3.195 -
3.196 -AddIffs [subideal_is_dvd, psubideal_is_dvd];
3.197 -
3.198 -Goal "!!a::'a::ring. a dvd b ==> b : (ideal_of {a})";
3.199 -by (rtac is_ideal_dvd 1);
3.200 -by (assume_tac 1);
3.201 -by (rtac ideal_of_is_ideal 1);
3.202 -by (rtac generator_in_ideal 1);
3.203 -by (Simp_tac 1);
3.204 -qed "dvd_imp_in_pideal";
3.205 -
3.206 -Goal "!!a::'a::ring. b : (ideal_of {a}) ==> a dvd b";
3.207 -by (full_simp_tac (simpset() addsimps [pideal_structure]) 1);
3.208 -qed "in_pideal_imp_dvd";
3.209 -
3.210 -Goal "~ (a dvd b) ==> ideal_of {a::'a::ring} < ideal_of {a, b}";
3.211 -by (asm_simp_tac (simpset() addsimps [psubset_eq, ideal_of_mono]) 1);
3.212 -by (etac contrapos_pp 1);
3.213 -by (full_simp_tac (simpset() addsimps [ideal_of_2_structure]) 1);
3.214 -by (rtac in_pideal_imp_dvd 1);
3.215 -by (Asm_simp_tac 1);
3.216 -by (res_inst_tac [("x", "0")] exI 1);
3.217 -by (res_inst_tac [("x", "1")] exI 1);
3.218 -by (Simp_tac 1);
3.219 -qed "not_dvd_psubideal";
3.220 -
3.221 -Goalw [thm "irred_def"]
3.222 - "[| irred (a::'a::ring); is_pideal I; ideal_of {a} < I |] ==> x : I";
3.223 -by (dtac is_pidealD 1);
3.224 -by (etac exE 1);
3.225 -by (Clarify_tac 1);
3.226 -by (eres_inst_tac [("x", "aa")] allE 1);
3.227 -by (Clarify_tac 1);
3.228 -by (dres_inst_tac [("a", "1")] dvd_imp_subideal 1);
3.229 -by (auto_tac (claset(), simpset() addsimps [ideal_of_one_eq]));
3.230 -qed "irred_imp_max_ideal";
3.231 -
3.232 -(* Pid are factorial *)
3.233 -
3.234 -(* Divisor chain condition *)
3.235 -(* proofs not finished *)
3.236 -
3.237 -Goal "(ALL i. I i <= I (Suc i)) ==> (n <= m & a : I n --> a : I m)";
3.238 -by (induct_tac "m" 1);
3.239 -by (Blast_tac 1);
3.240 -(* induction step *)
3.241 -by (rename_tac "m" 1);
3.242 -by (case_tac "n <= m" 1);
3.243 -by Auto_tac;
3.244 -by (subgoal_tac "n = Suc m" 1);
3.245 -by (arith_tac 2);
3.246 -by (Force_tac 1);
3.247 -qed_spec_mp "subset_chain_lemma";
3.248 -
3.249 -Goal "[| ALL i. is_ideal (I i); ALL i. I i <= I (Suc i) |] \
3.250 -\ ==> is_ideal (Union (I`UNIV))";
3.251 -by (rtac is_idealI 1);
3.252 -by Auto_tac;
3.253 -by (res_inst_tac [("x", "max x xa")] exI 1);
3.254 -by (rtac is_ideal_add 1);
3.255 -by (Asm_simp_tac 1);
3.256 -by (rtac subset_chain_lemma 1);
3.257 -by (assume_tac 1);
3.258 -by (rtac conjI 1);
3.259 -by (assume_tac 2);
3.260 -by (arith_tac 1);
3.261 -by (rtac subset_chain_lemma 1);
3.262 -by (assume_tac 1);
3.263 -by (rtac conjI 1);
3.264 -by (assume_tac 2);
3.265 -by (arith_tac 1);
3.266 -by (res_inst_tac [("x", "x")] exI 1);
3.267 -by (Asm_simp_tac 1);
3.268 -by (res_inst_tac [("x", "x")] exI 1);
3.269 -by (Asm_simp_tac 1);
3.270 -qed "chain_is_ideal";
3.271 -
3.272 -(*
3.273 -Goal "ALL i. ideal_of {a i} < ideal_of {a (Suc i)} ==> \
3.274 -\ EX n. Union ((ideal_of o (%a. {a}))`UNIV) = ideal_of {a n}";
3.275 -
3.276 -Goal "wf {(a::'a::pid, b). a dvd b & ~ b dvd a}";
3.277 -by (simp_tac (simpset()
3.278 - addsimps [psubideal_is_dvd RS sym, wf_iff_no_infinite_down_chain]
3.279 - delsimps [psubideal_is_dvd]) 1);
3.280 -*)
3.281 -
3.282 -(* Primeness condition *)
3.283 -
3.284 -Goalw [thm "prime_def"] "irred a ==> prime (a::'a::pid)";
3.285 -by (rtac conjI 1);
3.286 -by (rtac conjI 2);
3.287 -by (Clarify_tac 3);
3.288 -by (dres_inst_tac [("I", "ideal_of {a, b}"), ("x", "1")]
3.289 - irred_imp_max_ideal 3);
3.290 -by (auto_tac (claset() addIs [ideal_of_is_ideal, thm "pid_ax"],
3.291 - simpset() addsimps [thm "irred_def", not_dvd_psubideal, thm "pid_ax"]));
3.292 -by (full_simp_tac (simpset() addsimps [ideal_of_2_structure]) 1);
3.293 -by (Clarify_tac 1);
3.294 -by (dres_inst_tac [("f", "op* aa")] arg_cong 1);
3.295 -by (full_simp_tac (simpset() addsimps [r_distr]) 1);
3.296 -by (etac subst 1);
3.297 -by (asm_simp_tac (simpset() addsimps [m_assoc RS sym]
3.298 - delsimprocs [ring_simproc]) 1);
3.299 -qed "pid_irred_imp_prime";
3.300 -
3.301 -(* Fields are Pid *)
3.302 -
3.303 -Goal "a ~= 0 ==> ideal_of {a::'a::field} = UNIV";
3.304 -by (rtac subset_antisym 1);
3.305 -by (Simp_tac 1);
3.306 -by (rtac subset_trans 1);
3.307 -by (rtac dvd_imp_subideal 2);
3.308 -by (rtac (thm "field_ax") 2);
3.309 -by (assume_tac 2);
3.310 -by (simp_tac (simpset() addsimps [ideal_of_one_eq]) 1);
3.311 -qed "field_pideal_univ";
3.312 -
3.313 -Goal "[| is_ideal I; I ~= {0} |] ==> {0} < I";
3.314 -by (asm_simp_tac (simpset() addsimps [psubset_eq, not_sym, is_ideal_zero]) 1);
3.315 -qed "proper_ideal";
3.316 -
3.317 -Goalw [thm "is_pideal_def"] "is_ideal (I::('a::field) set) ==> is_pideal I";
3.318 -by (case_tac "I = {0}" 1);
3.319 -by (res_inst_tac [("x", "0")] exI 1);
3.320 -by (asm_simp_tac (simpset() addsimps [ideal_of_zero_eq]) 1);
3.321 -(* case "I ~= {0}" *)
3.322 -by (ftac proper_ideal 1);
3.323 -by (assume_tac 1);
3.324 -by (dtac psubset_imp_ex_mem 1);
3.325 -by (etac exE 1);
3.326 -by (res_inst_tac [("x", "b")] exI 1);
3.327 -by (cut_inst_tac [("a", "b")] element_generates_subideal 1);
3.328 - by (assume_tac 1); by (Blast_tac 1);
3.329 -by (auto_tac (claset(), simpset() addsimps [field_pideal_univ]));
3.330 -qed "field_pid";
3.331 -
4.1 --- a/src/HOL/Algebra/abstract/Ideal2.thy Sun Nov 19 13:02:55 2006 +0100
4.2 +++ b/src/HOL/Algebra/abstract/Ideal2.thy Sun Nov 19 23:48:55 2006 +0100
4.3 @@ -6,21 +6,318 @@
4.4
4.5 theory Ideal2 imports Ring2 begin
4.6
4.7 -consts
4.8 - ideal_of :: "('a::ring) set => 'a set"
4.9 - is_ideal :: "('a::ring) set => bool"
4.10 - is_pideal :: "('a::ring) set => bool"
4.11 +definition
4.12 + is_ideal :: "('a::ring) set => bool" where
4.13 + "is_ideal I \<longleftrightarrow> (ALL a: I. ALL b: I. a + b : I) &
4.14 + (ALL a: I. - a : I) & 0 : I &
4.15 + (ALL a: I. ALL r. a * r : I)"
4.16
4.17 -defs
4.18 - is_ideal_def: "is_ideal I == (ALL a: I. ALL b: I. a + b : I) &
4.19 - (ALL a: I. - a : I) & 0 : I &
4.20 - (ALL a: I. ALL r. a * r : I)"
4.21 - ideal_of_def: "ideal_of S == Inter {I. is_ideal I & S <= I}"
4.22 - is_pideal_def: "is_pideal I == (EX a. I = ideal_of {a})"
4.23 +definition
4.24 + ideal_of :: "('a::ring) set => 'a set" where
4.25 + "ideal_of S = Inter {I. is_ideal I & S <= I}"
4.26 +
4.27 +definition
4.28 + is_pideal :: "('a::ring) set => bool" where
4.29 + "is_pideal I \<longleftrightarrow> (EX a. I = ideal_of {a})"
4.30 +
4.31
4.32 text {* Principle ideal domains *}
4.33
4.34 axclass pid < "domain"
4.35 pid_ax: "is_ideal I ==> is_pideal I"
4.36
4.37 +
4.38 +(* is_ideal *)
4.39 +
4.40 +lemma is_idealI:
4.41 + "!! I. [| !! a b. [| a:I; b:I |] ==> a + b : I;
4.42 + !! a. a:I ==> - a : I; 0 : I;
4.43 + !! a r. a:I ==> a * r : I |] ==> is_ideal I"
4.44 + unfolding is_ideal_def by blast
4.45 +
4.46 +lemma is_ideal_add [simp]: "[| is_ideal I; a:I; b:I |] ==> a + b : I"
4.47 + unfolding is_ideal_def by blast
4.48 +
4.49 +lemma is_ideal_uminus [simp]: "[| is_ideal I; a:I |] ==> - a : I"
4.50 + unfolding is_ideal_def by blast
4.51 +
4.52 +lemma is_ideal_zero [simp]: "[| is_ideal I |] ==> 0 : I"
4.53 + unfolding is_ideal_def by blast
4.54 +
4.55 +lemma is_ideal_mult [simp]: "[| is_ideal I; a:I |] ==> a * r : I"
4.56 + unfolding is_ideal_def by blast
4.57 +
4.58 +lemma is_ideal_dvd: "[| a dvd b; is_ideal I; a:I |] ==> b:I"
4.59 + unfolding is_ideal_def dvd_def by blast
4.60 +
4.61 +lemma UNIV_is_ideal [simp]: "is_ideal (UNIV::('a::ring) set)"
4.62 + unfolding is_ideal_def by blast
4.63 +
4.64 +lemma zero_is_ideal [simp]: "is_ideal {0::'a::ring}"
4.65 + unfolding is_ideal_def by auto
4.66 +
4.67 +lemma is_ideal_1: "is_ideal {x::'a::ring. a dvd x}"
4.68 + apply (rule is_idealI)
4.69 + apply auto
4.70 + done
4.71 +
4.72 +lemma is_ideal_2: "is_ideal {x::'a::ring. EX u v. x = a * u + b * v}"
4.73 + apply (rule is_idealI)
4.74 + apply auto
4.75 + apply (rule_tac x = "u+ua" in exI)
4.76 + apply (rule_tac x = "v+va" in exI)
4.77 + apply (rule_tac [2] x = "-u" in exI)
4.78 + apply (rule_tac [2] x = "-v" in exI)
4.79 + apply (rule_tac [3] x = "0" in exI)
4.80 + apply (rule_tac [3] x = "0" in exI)
4.81 + apply (rule_tac [4] x = "u * r" in exI)
4.82 + apply (rule_tac [4] x = "v * r" in exI)
4.83 + apply simp_all
4.84 + done
4.85 +
4.86 +
4.87 +(* ideal_of *)
4.88 +
4.89 +lemma ideal_of_is_ideal: "is_ideal (ideal_of S)"
4.90 + unfolding is_ideal_def ideal_of_def by blast
4.91 +
4.92 +lemma generator_in_ideal: "a:S ==> a : (ideal_of S)"
4.93 + unfolding ideal_of_def by blast
4.94 +
4.95 +lemma ideal_of_one_eq: "ideal_of {1::'a::ring} = UNIV"
4.96 + apply (unfold ideal_of_def)
4.97 + apply (force dest: is_ideal_mult simp add: l_one)
4.98 + done
4.99 +
4.100 +lemma ideal_of_empty_eq: "ideal_of {} = {0::'a::ring}"
4.101 + apply (unfold ideal_of_def)
4.102 + apply (rule subset_antisym)
4.103 + apply (rule subsetI)
4.104 + apply (drule InterD)
4.105 + prefer 2 apply assumption
4.106 + apply (auto simp add: is_ideal_zero)
4.107 + done
4.108 +
4.109 +lemma pideal_structure: "ideal_of {a} = {x::'a::ring. a dvd x}"
4.110 + apply (unfold ideal_of_def)
4.111 + apply (rule subset_antisym)
4.112 + apply (rule subsetI)
4.113 + apply (drule InterD)
4.114 + prefer 2 apply assumption
4.115 + apply (auto intro: is_ideal_1)
4.116 + apply (simp add: is_ideal_dvd)
4.117 + done
4.118 +
4.119 +lemma ideal_of_2_structure:
4.120 + "ideal_of {a, b} = {x::'a::ring. EX u v. x = a * u + b * v}"
4.121 + apply (unfold ideal_of_def)
4.122 + apply (rule subset_antisym)
4.123 + apply (rule subsetI)
4.124 + apply (drule InterD)
4.125 + prefer 2 apply assumption
4.126 + apply (tactic {* auto_tac (claset() addIs [thm "is_ideal_2"],
4.127 + simpset() delsimprocs [ring_simproc]) *})
4.128 + apply (rule_tac x = "1" in exI)
4.129 + apply (rule_tac x = "0" in exI)
4.130 + apply (rule_tac [2] x = "0" in exI)
4.131 + apply (rule_tac [2] x = "1" in exI)
4.132 + apply simp
4.133 + apply simp
4.134 + done
4.135 +
4.136 +lemma ideal_of_mono: "A <= B ==> ideal_of A <= ideal_of B"
4.137 + unfolding ideal_of_def by blast
4.138 +
4.139 +lemma ideal_of_zero_eq: "ideal_of {0::'a::ring} = {0}"
4.140 + apply (simp add: pideal_structure)
4.141 + apply (rule subset_antisym)
4.142 + apply (auto intro: "dvd_zero_left")
4.143 + done
4.144 +
4.145 +lemma element_generates_subideal: "[| is_ideal I; a : I |] ==> ideal_of {a::'a::ring} <= I"
4.146 + apply (auto simp add: pideal_structure is_ideal_dvd)
4.147 + done
4.148 +
4.149 +
4.150 +(* is_pideal *)
4.151 +
4.152 +lemma is_pideal_imp_is_ideal: "is_pideal (I::('a::ring) set) ==> is_ideal I"
4.153 + unfolding is_pideal_def by (fast intro: ideal_of_is_ideal)
4.154 +
4.155 +lemma pideal_is_pideal: "is_pideal (ideal_of {a::'a::ring})"
4.156 + unfolding is_pideal_def by blast
4.157 +
4.158 +lemma is_pidealD: "is_pideal I ==> EX a. I = ideal_of {a}"
4.159 + unfolding is_pideal_def .
4.160 +
4.161 +
4.162 +(* Ideals and divisibility *)
4.163 +
4.164 +lemma dvd_imp_subideal: "b dvd a ==> ideal_of {a::'a::ring} <= ideal_of {b}"
4.165 + by (auto intro: dvd_trans_ring simp add: pideal_structure)
4.166 +
4.167 +lemma subideal_imp_dvd: "ideal_of {a::'a::ring} <= ideal_of {b} ==> b dvd a"
4.168 + by (auto dest!: subsetD simp add: pideal_structure)
4.169 +
4.170 +lemma psubideal_not_dvd: "(ideal_of {a::'a::ring} < ideal_of {b}) ==> ~ a dvd b"
4.171 + apply (simp add: psubset_eq pideal_structure)
4.172 + apply (erule conjE)
4.173 + apply (drule_tac c = "a" in subsetD)
4.174 + apply (auto intro: dvd_trans_ring)
4.175 + done
4.176 +
4.177 +lemma not_dvd_psubideal_singleton:
4.178 + "[| b dvd a; ~ a dvd b |] ==> ideal_of {a::'a::ring} < ideal_of {b}"
4.179 + apply (rule psubsetI)
4.180 + apply (erule dvd_imp_subideal)
4.181 + apply (blast intro: dvd_imp_subideal subideal_imp_dvd)
4.182 + done
4.183 +
4.184 +lemma subideal_is_dvd [iff]: "(ideal_of {a::'a::ring} <= ideal_of {b}) = (b dvd a)"
4.185 + apply (rule iffI)
4.186 + apply (assumption | rule subideal_imp_dvd dvd_imp_subideal)+
4.187 + done
4.188 +
4.189 +lemma psubideal_is_dvd [iff]: "(ideal_of {a::'a::ring} < ideal_of {b}) = (b dvd a & ~ a dvd b)"
4.190 + apply (rule iffI)
4.191 + apply (assumption | rule conjI psubideal_not_dvd psubset_imp_subset [THEN subideal_imp_dvd])+
4.192 + apply (erule conjE)
4.193 + apply (assumption | rule not_dvd_psubideal_singleton)+
4.194 + done
4.195 +
4.196 +lemma assoc_pideal_eq: "[| a dvd b; b dvd a |] ==> ideal_of {a::'a::ring} = ideal_of {b}"
4.197 + apply (rule subset_antisym)
4.198 + apply (assumption | rule dvd_imp_subideal)+
4.199 + done
4.200 +
4.201 +lemma dvd_imp_in_pideal: "!!a::'a::ring. a dvd b ==> b : (ideal_of {a})"
4.202 + apply (rule is_ideal_dvd)
4.203 + apply assumption
4.204 + apply (rule ideal_of_is_ideal)
4.205 + apply (rule generator_in_ideal)
4.206 + apply simp
4.207 + done
4.208 +
4.209 +lemma in_pideal_imp_dvd: "!!a::'a::ring. b : (ideal_of {a}) ==> a dvd b"
4.210 + by (simp add: pideal_structure)
4.211 +
4.212 +lemma not_dvd_psubideal: "~ (a dvd b) ==> ideal_of {a::'a::ring} < ideal_of {a, b}"
4.213 + apply (simp add: psubset_eq ideal_of_mono)
4.214 + apply (erule contrapos_pp)
4.215 + apply (simp add: ideal_of_2_structure)
4.216 + apply (rule in_pideal_imp_dvd)
4.217 + apply simp
4.218 + apply (rule_tac x = "0" in exI)
4.219 + apply (rule_tac x = "1" in exI)
4.220 + apply simp
4.221 + done
4.222 +
4.223 +lemma irred_imp_max_ideal:
4.224 + "[| irred (a::'a::ring); is_pideal I; ideal_of {a} < I |] ==> x : I"
4.225 + apply (unfold irred_def)
4.226 + apply (drule is_pidealD)
4.227 + apply (erule exE)
4.228 + apply clarify
4.229 + apply (erule_tac x = "aa" in allE)
4.230 + apply clarify
4.231 + apply (drule_tac a = "1" in dvd_imp_subideal)
4.232 + apply (auto simp add: ideal_of_one_eq)
4.233 + done
4.234 +
4.235 +(* Pid are factorial *)
4.236 +
4.237 +(* Divisor chain condition *)
4.238 +(* proofs not finished *)
4.239 +
4.240 +lemma subset_chain_lemma [rule_format (no_asm)]:
4.241 + "(ALL i. I i <= I (Suc i)) ==> (n <= m & a : I n --> a : I m)"
4.242 + apply (induct_tac m)
4.243 + apply blast
4.244 + (* induction step *)
4.245 + apply (rename_tac m)
4.246 + apply (case_tac "n <= m")
4.247 + apply auto
4.248 + apply (subgoal_tac "n = Suc m")
4.249 + prefer 2
4.250 + apply arith
4.251 + apply force
4.252 + done
4.253 +
4.254 +lemma chain_is_ideal: "[| ALL i. is_ideal (I i); ALL i. I i <= I (Suc i) |]
4.255 + ==> is_ideal (Union (I`UNIV))"
4.256 + apply (rule is_idealI)
4.257 + apply auto
4.258 + apply (rule_tac x = "max x xa" in exI)
4.259 + apply (rule is_ideal_add)
4.260 + apply simp
4.261 + apply (rule subset_chain_lemma)
4.262 + apply assumption
4.263 + apply (rule conjI)
4.264 + prefer 2
4.265 + apply assumption
4.266 + apply arith
4.267 + apply (rule subset_chain_lemma)
4.268 + apply assumption
4.269 + apply (rule conjI)
4.270 + prefer 2
4.271 + apply assumption
4.272 + apply arith
4.273 + apply (rule_tac x = "x" in exI)
4.274 + apply simp
4.275 + apply (rule_tac x = "x" in exI)
4.276 + apply simp
4.277 + done
4.278 +
4.279 +
4.280 +(* Primeness condition *)
4.281 +
4.282 +lemma pid_irred_imp_prime: "irred a ==> prime (a::'a::pid)"
4.283 + apply (unfold prime_def)
4.284 + apply (rule conjI)
4.285 + apply (rule_tac [2] conjI)
4.286 + apply (tactic "Clarify_tac 3")
4.287 + apply (drule_tac [3] I = "ideal_of {a, b}" and x = "1" in irred_imp_max_ideal)
4.288 + apply (auto intro: ideal_of_is_ideal pid_ax simp add: irred_def not_dvd_psubideal pid_ax)
4.289 + apply (simp add: ideal_of_2_structure)
4.290 + apply clarify
4.291 + apply (drule_tac f = "op* aa" in arg_cong)
4.292 + apply (simp add: r_distr)
4.293 + apply (erule subst)
4.294 + apply (tactic {* asm_simp_tac (simpset() addsimps [thm "m_assoc" RS sym]
4.295 + delsimprocs [ring_simproc]) 1 *})
4.296 + done
4.297 +
4.298 +(* Fields are Pid *)
4.299 +
4.300 +lemma field_pideal_univ: "a ~= 0 ==> ideal_of {a::'a::field} = UNIV"
4.301 + apply (rule subset_antisym)
4.302 + apply simp
4.303 + apply (rule subset_trans)
4.304 + prefer 2
4.305 + apply (rule dvd_imp_subideal)
4.306 + apply (rule field_ax)
4.307 + apply assumption
4.308 + apply (simp add: ideal_of_one_eq)
4.309 + done
4.310 +
4.311 +lemma proper_ideal: "[| is_ideal I; I ~= {0} |] ==> {0} < I"
4.312 + by (simp add: psubset_eq not_sym is_ideal_zero)
4.313 +
4.314 +lemma field_pid: "is_ideal (I::('a::field) set) ==> is_pideal I"
4.315 + apply (unfold is_pideal_def)
4.316 + apply (case_tac "I = {0}")
4.317 + apply (rule_tac x = "0" in exI)
4.318 + apply (simp add: ideal_of_zero_eq)
4.319 + (* case "I ~= {0}" *)
4.320 + apply (frule proper_ideal)
4.321 + apply assumption
4.322 + apply (drule psubset_imp_ex_mem)
4.323 + apply (erule exE)
4.324 + apply (rule_tac x = b in exI)
4.325 + apply (cut_tac a = b in element_generates_subideal)
4.326 + apply assumption
4.327 + apply blast
4.328 + apply (auto simp add: field_pideal_univ)
4.329 + done
4.330 +
4.331 end
5.1 --- a/src/HOL/Algebra/abstract/Ring2.ML Sun Nov 19 13:02:55 2006 +0100
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,350 +0,0 @@
5.4 -(*
5.5 - Abstract class ring (commutative, with 1)
5.6 - $Id$
5.7 - Author: Clemens Ballarin, started 9 December 1996
5.8 -*)
5.9 -
5.10 -(*
5.11 -val a_assoc = thm "semigroup_add.add_assoc";
5.12 -val l_zero = thm "comm_monoid_add.add_0";
5.13 -val a_comm = thm "ab_semigroup_add.add_commute";
5.14 -
5.15 -section "Rings";
5.16 -
5.17 -fun make_left_commute assoc commute s =
5.18 - [rtac (commute RS trans) 1, rtac (assoc RS trans) 1,
5.19 - rtac (commute RS arg_cong) 1];
5.20 -
5.21 -(* addition *)
5.22 -
5.23 -qed_goal "a_lcomm" Ring2.thy "!!a::'a::ring. a+(b+c) = b+(a+c)"
5.24 - (make_left_commute a_assoc a_comm);
5.25 -
5.26 -val a_ac = [a_assoc, a_comm, a_lcomm];
5.27 -
5.28 -Goal "!!a::'a::ring. a + 0 = a";
5.29 -by (rtac (a_comm RS trans) 1);
5.30 -by (rtac l_zero 1);
5.31 -qed "r_zero";
5.32 -
5.33 -Goal "!!a::'a::ring. a + (-a) = 0";
5.34 -by (rtac (a_comm RS trans) 1);
5.35 -by (rtac l_neg 1);
5.36 -qed "r_neg";
5.37 -
5.38 -Goal "!! a::'a::ring. a + b = a + c ==> b = c";
5.39 -by (rtac box_equals 1);
5.40 -by (rtac l_zero 2);
5.41 -by (rtac l_zero 2);
5.42 -by (res_inst_tac [("a1", "a")] (l_neg RS subst) 1);
5.43 -by (asm_simp_tac (simpset() addsimps [a_assoc]) 1);
5.44 -qed "a_lcancel";
5.45 -
5.46 -Goal "!! a::'a::ring. b + a = c + a ==> b = c";
5.47 -by (rtac a_lcancel 1);
5.48 -by (asm_simp_tac (simpset() addsimps a_ac) 1);
5.49 -qed "a_rcancel";
5.50 -
5.51 -Goal "!! a::'a::ring. (a + b = a + c) = (b = c)";
5.52 -by (auto_tac (claset() addSDs [a_lcancel], simpset()));
5.53 -qed "a_lcancel_eq";
5.54 -
5.55 -Goal "!! a::'a::ring. (b + a = c + a) = (b = c)";
5.56 -by (simp_tac (simpset() addsimps [a_lcancel_eq, a_comm]) 1);
5.57 -qed "a_rcancel_eq";
5.58 -
5.59 -Addsimps [a_lcancel_eq, a_rcancel_eq];
5.60 -
5.61 -Goal "!!a::'a::ring. -(-a) = a";
5.62 -by (rtac a_lcancel 1);
5.63 -by (rtac (r_neg RS trans) 1);
5.64 -by (rtac (l_neg RS sym) 1);
5.65 -qed "minus_minus";
5.66 -
5.67 -Goal "- 0 = (0::'a::ring)";
5.68 -by (rtac a_lcancel 1);
5.69 -by (rtac (r_neg RS trans) 1);
5.70 -by (rtac (l_zero RS sym) 1);
5.71 -qed "minus0";
5.72 -
5.73 -Goal "!!a::'a::ring. -(a + b) = (-a) + (-b)";
5.74 -by (res_inst_tac [("a", "a+b")] a_lcancel 1);
5.75 -by (simp_tac (simpset() addsimps ([r_neg, l_neg, l_zero]@a_ac)) 1);
5.76 -qed "minus_add";
5.77 -
5.78 -(* multiplication *)
5.79 -
5.80 -qed_goal "m_lcomm" Ring2.thy "!!a::'a::ring. a*(b*c) = b*(a*c)"
5.81 - (make_left_commute m_assoc m_comm);
5.82 -
5.83 -val m_ac = [m_assoc, m_comm, m_lcomm];
5.84 -
5.85 -Goal "!!a::'a::ring. a * 1 = a";
5.86 -by (rtac (m_comm RS trans) 1);
5.87 -by (rtac l_one 1);
5.88 -qed "r_one";
5.89 -
5.90 -(* distributive and derived *)
5.91 -
5.92 -Goal "!!a::'a::ring. a * (b + c) = a * b + a * c";
5.93 -by (rtac (m_comm RS trans) 1);
5.94 -by (rtac (l_distr RS trans) 1);
5.95 -by (simp_tac (simpset() addsimps [m_comm]) 1);
5.96 -qed "r_distr";
5.97 -
5.98 -val m_distr = m_ac @ [l_distr, r_distr];
5.99 -
5.100 -(* the following two proofs can be found in
5.101 - Jacobson, Basic Algebra I, pp. 88-89 *)
5.102 -
5.103 -Goal "!!a::'a::ring. 0 * a = 0";
5.104 -by (rtac a_lcancel 1);
5.105 -by (rtac (l_distr RS sym RS trans) 1);
5.106 -by (simp_tac (simpset() addsimps [r_zero]) 1);
5.107 -qed "l_null";
5.108 -
5.109 -Goal "!!a::'a::ring. a * 0 = 0";
5.110 -by (rtac (m_comm RS trans) 1);
5.111 -by (rtac l_null 1);
5.112 -qed "r_null";
5.113 -
5.114 -Goal "!!a::'a::ring. (-a) * b = - (a * b)";
5.115 -by (rtac a_lcancel 1);
5.116 -by (rtac (r_neg RS sym RSN (2, trans)) 1);
5.117 -by (rtac (l_distr RS sym RS trans) 1);
5.118 -by (simp_tac (simpset() addsimps [l_null, r_neg]) 1);
5.119 -qed "l_minus";
5.120 -
5.121 -Goal "!!a::'a::ring. a * (-b) = - (a * b)";
5.122 -by (rtac a_lcancel 1);
5.123 -by (rtac (r_neg RS sym RSN (2, trans)) 1);
5.124 -by (rtac (r_distr RS sym RS trans) 1);
5.125 -by (simp_tac (simpset() addsimps [r_null, r_neg]) 1);
5.126 -qed "r_minus";
5.127 -
5.128 -val m_minus = [l_minus, r_minus];
5.129 -
5.130 -Addsimps [l_zero, r_zero, l_neg, r_neg, minus_minus, minus0,
5.131 - l_one, r_one, l_null, r_null];
5.132 -
5.133 -(* further rules *)
5.134 -
5.135 -Goal "!!a::'a::ring. -a = 0 ==> a = 0";
5.136 -by (res_inst_tac [("t", "a")] (minus_minus RS subst) 1);
5.137 -by (Asm_simp_tac 1);
5.138 -qed "uminus_monom";
5.139 -
5.140 -Goal "!!a::'a::ring. a ~= 0 ==> -a ~= 0";
5.141 -by (blast_tac (claset() addIs [uminus_monom]) 1);
5.142 -qed "uminus_monom_neq";
5.143 -
5.144 -Goal "!!a::'a::ring. a * b ~= 0 ==> a ~= 0";
5.145 -by Auto_tac;
5.146 -qed "l_nullD";
5.147 -
5.148 -Goal "!!a::'a::ring. a * b ~= 0 ==> b ~= 0";
5.149 -by Auto_tac;
5.150 -qed "r_nullD";
5.151 -
5.152 -(* reflection between a = b and a -- b = 0 *)
5.153 -
5.154 -Goal "!!a::'a::ring. a = b ==> a + (-b) = 0";
5.155 -by (Asm_simp_tac 1);
5.156 -qed "eq_imp_diff_zero";
5.157 -
5.158 -Goal "!!a::'a::ring. a + (-b) = 0 ==> a = b";
5.159 -by (res_inst_tac [("a", "-b")] a_rcancel 1);
5.160 -by (Asm_simp_tac 1);
5.161 -qed "diff_zero_imp_eq";
5.162 -
5.163 -(* this could be a rewrite rule, but won't terminate
5.164 - ==> make it a simproc?
5.165 -Goal "!!a::'a::ring. (a = b) = (a -- b = 0)";
5.166 -*)
5.167 -
5.168 -*)
5.169 -
5.170 -val dvd_def = thm "dvd_def'";
5.171 -
5.172 -Goalw [dvd_def]
5.173 - "!!a::'a::ring. [| a dvd 1; b dvd 1 |] ==> a * b dvd 1";
5.174 -by (Clarify_tac 1);
5.175 -by (res_inst_tac [("x", "k * ka")] exI 1);
5.176 -by (Asm_full_simp_tac 1);
5.177 -qed "unit_mult";
5.178 -
5.179 -Goal "!!a::'a::ring. a dvd 1 ==> a^n dvd 1";
5.180 -by (induct_tac "n" 1);
5.181 -by (Simp_tac 1);
5.182 -by (asm_simp_tac (simpset() addsimps [unit_mult]) 1);
5.183 -qed "unit_power";
5.184 -
5.185 -Goalw [dvd_def]
5.186 - "!! a::'a::ring. [| a dvd b; a dvd c |] ==> a dvd b + c";
5.187 -by (Clarify_tac 1);
5.188 -by (res_inst_tac [("x", "k + ka")] exI 1);
5.189 -by (simp_tac (simpset() addsimps [r_distr]) 1);
5.190 -qed "dvd_add_right";
5.191 -
5.192 -Goalw [dvd_def]
5.193 - "!! a::'a::ring. a dvd b ==> a dvd -b";
5.194 -by (Clarify_tac 1);
5.195 -by (res_inst_tac [("x", "-k")] exI 1);
5.196 -by (simp_tac (simpset() addsimps [r_minus]) 1);
5.197 -qed "dvd_uminus_right";
5.198 -
5.199 -Goalw [dvd_def]
5.200 - "!! a::'a::ring. a dvd b ==> a dvd c*b";
5.201 -by (Clarify_tac 1);
5.202 -by (res_inst_tac [("x", "c * k")] exI 1);
5.203 -by (Simp_tac 1);
5.204 -qed "dvd_l_mult_right";
5.205 -
5.206 -Goalw [dvd_def]
5.207 - "!! a::'a::ring. a dvd b ==> a dvd b*c";
5.208 -by (Clarify_tac 1);
5.209 -by (res_inst_tac [("x", "k * c")] exI 1);
5.210 -by (Simp_tac 1);
5.211 -qed "dvd_r_mult_right";
5.212 -
5.213 -Addsimps [dvd_add_right, dvd_uminus_right, dvd_l_mult_right, dvd_r_mult_right];
5.214 -
5.215 -(* Inverse of multiplication *)
5.216 -
5.217 -section "inverse";
5.218 -
5.219 -Goal "!! a::'a::ring. [| a * x = 1; a * y = 1 |] ==> x = y";
5.220 -by (res_inst_tac [("a", "(a*y)*x"), ("b", "y*(a*x)")] box_equals 1);
5.221 -by (Simp_tac 1);
5.222 -by Auto_tac;
5.223 -qed "inverse_unique";
5.224 -
5.225 -Goal "!! a::'a::ring. a dvd 1 ==> a * inverse a = 1";
5.226 -by (asm_full_simp_tac (simpset () addsimps [inverse_def, dvd_def]
5.227 - delsimprocs [ring_simproc]) 1);
5.228 -by (Clarify_tac 1);
5.229 -by (rtac theI 1);
5.230 -by (atac 1);
5.231 -by (rtac inverse_unique 1);
5.232 -by (atac 1);
5.233 -by (atac 1);
5.234 -qed "r_inverse_ring";
5.235 -
5.236 -Goal "!! a::'a::ring. a dvd 1 ==> inverse a * a= 1";
5.237 -by (asm_simp_tac (simpset() addsimps [r_inverse_ring]) 1);
5.238 -qed "l_inverse_ring";
5.239 -
5.240 -(* Integral domain *)
5.241 -
5.242 -(*
5.243 -section "Integral domains";
5.244 -
5.245 -Goal "0 ~= (1::'a::domain)";
5.246 -by (rtac not_sym 1);
5.247 -by (rtac one_not_zero 1);
5.248 -qed "zero_not_one";
5.249 -
5.250 -Goal "!! a::'a::domain. a dvd 1 ==> a ~= 0";
5.251 -by (auto_tac (claset() addDs [dvd_zero_left],
5.252 - simpset() addsimps [one_not_zero] ));
5.253 -qed "unit_imp_nonzero";
5.254 -
5.255 -Goal "[| a * b = 0; a ~= 0 |] ==> (b::'a::domain) = 0";
5.256 -by (dtac integral 1);
5.257 -by (Fast_tac 1);
5.258 -qed "r_integral";
5.259 -
5.260 -Goal "[| a * b = 0; b ~= 0 |] ==> (a::'a::domain) = 0";
5.261 -by (dtac integral 1);
5.262 -by (Fast_tac 1);
5.263 -qed "l_integral";
5.264 -
5.265 -Goal "!! a::'a::domain. [| a ~= 0; b ~= 0 |] ==> a * b ~= 0";
5.266 -by (blast_tac (claset() addIs [l_integral]) 1);
5.267 -qed "not_integral";
5.268 -
5.269 -Addsimps [not_integral, one_not_zero, zero_not_one];
5.270 -
5.271 -Goal "!! a::'a::domain. [| a * x = x; x ~= 0 |] ==> a = 1";
5.272 -by (res_inst_tac [("a", "- 1")] a_lcancel 1);
5.273 -by (Simp_tac 1);
5.274 -by (rtac l_integral 1);
5.275 -by (assume_tac 2);
5.276 -by (asm_simp_tac (simpset() addsimps [l_distr, l_minus]) 1);
5.277 -qed "l_one_integral";
5.278 -
5.279 -Goal "!! a::'a::domain. [| x * a = x; x ~= 0 |] ==> a = 1";
5.280 -by (res_inst_tac [("a", "- 1")] a_rcancel 1);
5.281 -by (Simp_tac 1);
5.282 -by (rtac r_integral 1);
5.283 -by (assume_tac 2);
5.284 -by (asm_simp_tac (simpset() addsimps [r_distr, r_minus]) 1);
5.285 -qed "r_one_integral";
5.286 -
5.287 -(* cancellation laws for multiplication *)
5.288 -
5.289 -Goal "!! a::'a::domain. [| a ~= 0; a * b = a * c |] ==> b = c";
5.290 -by (rtac diff_zero_imp_eq 1);
5.291 -by (dtac eq_imp_diff_zero 1);
5.292 -by (full_simp_tac (simpset() addsimps [r_minus RS sym, r_distr RS sym]) 1);
5.293 -by (fast_tac (claset() addIs [l_integral]) 1);
5.294 -qed "m_lcancel";
5.295 -
5.296 -Goal "!! a::'a::domain. [| a ~= 0; b * a = c * a |] ==> b = c";
5.297 -by (rtac m_lcancel 1);
5.298 -by (assume_tac 1);
5.299 -by (Asm_full_simp_tac 1);
5.300 -qed "m_rcancel";
5.301 -
5.302 -Goal "!! a::'a::domain. a ~= 0 ==> (a * b = a * c) = (b = c)";
5.303 -by (auto_tac (claset() addDs [m_lcancel], simpset()));
5.304 -qed "m_lcancel_eq";
5.305 -
5.306 -Goal "!! a::'a::domain. a ~= 0 ==> (b * a = c * a) = (b = c)";
5.307 -by (asm_simp_tac (simpset() addsimps [m_lcancel_eq, m_comm]) 1);
5.308 -qed "m_rcancel_eq";
5.309 -
5.310 -Addsimps [m_lcancel_eq, m_rcancel_eq];
5.311 -*)
5.312 -
5.313 -(* Fields *)
5.314 -
5.315 -section "Fields";
5.316 -
5.317 -Goal "!! a::'a::field. (a dvd 1) = (a ~= 0)";
5.318 -by (auto_tac (claset() addDs [thm "field_ax", thm "dvd_zero_left"],
5.319 - simpset() addsimps [thm "field_one_not_zero"]));
5.320 -qed "field_unit";
5.321 -
5.322 -(* required for instantiation of field < domain in file Field.thy *)
5.323 -
5.324 -Addsimps [field_unit];
5.325 -
5.326 -val field_one_not_zero = thm "field_one_not_zero";
5.327 -
5.328 -Goal "!! a::'a::field. a ~= 0 ==> a * inverse a = 1";
5.329 -by (asm_full_simp_tac (simpset() addsimps [r_inverse_ring]) 1);
5.330 -qed "r_inverse";
5.331 -
5.332 -Goal "!! a::'a::field. a ~= 0 ==> inverse a * a= 1";
5.333 -by (asm_full_simp_tac (simpset() addsimps [l_inverse_ring]) 1);
5.334 -qed "l_inverse";
5.335 -
5.336 -Addsimps [l_inverse, r_inverse];
5.337 -
5.338 -(* fields are integral domains *)
5.339 -
5.340 -Goal "!! a::'a::field. a * b = 0 ==> a = 0 | b = 0";
5.341 -by (Step_tac 1);
5.342 -by (res_inst_tac [("a", "(a*b)*inverse b")] box_equals 1);
5.343 -by (rtac refl 3);
5.344 -by (Simp_tac 2);
5.345 -by Auto_tac;
5.346 -qed "field_integral";
5.347 -
5.348 -(* fields are factorial domains *)
5.349 -
5.350 -Goalw [thm "prime_def", thm "irred_def"]
5.351 - "!! a::'a::field. irred a ==> prime a";
5.352 -by (blast_tac (claset() addIs [thm "field_ax"]) 1);
5.353 -qed "field_fact_prime";
6.1 --- a/src/HOL/Algebra/abstract/Ring2.thy Sun Nov 19 13:02:55 2006 +0100
6.2 +++ b/src/HOL/Algebra/abstract/Ring2.thy Sun Nov 19 23:48:55 2006 +0100
6.3 @@ -8,7 +8,7 @@
6.4 header {* The algebraic hierarchy of rings as axiomatic classes *}
6.5
6.6 theory Ring2 imports Main
6.7 -uses ("order.ML") begin
6.8 +begin
6.9
6.10 section {* Constants *}
6.11
6.12 @@ -102,16 +102,142 @@
6.13 prove about fields is that they are domains. *)
6.14 field_ax: "a ~= 0 ==> a dvd 1"
6.15
6.16 +
6.17 section {* Basic facts *}
6.18
6.19 subsection {* Normaliser for rings *}
6.20
6.21 -use "order.ML"
6.22 +(* derived rewrite rules *)
6.23 +
6.24 +lemma a_lcomm: "(a::'a::ring)+(b+c) = b+(a+c)"
6.25 + apply (rule a_comm [THEN trans])
6.26 + apply (rule a_assoc [THEN trans])
6.27 + apply (rule a_comm [THEN arg_cong])
6.28 + done
6.29 +
6.30 +lemma r_zero: "(a::'a::ring) + 0 = a"
6.31 + apply (rule a_comm [THEN trans])
6.32 + apply (rule l_zero)
6.33 + done
6.34 +
6.35 +lemma r_neg: "(a::'a::ring) + (-a) = 0"
6.36 + apply (rule a_comm [THEN trans])
6.37 + apply (rule l_neg)
6.38 + done
6.39 +
6.40 +lemma r_neg2: "(a::'a::ring) + (-a + b) = b"
6.41 + apply (rule a_assoc [symmetric, THEN trans])
6.42 + apply (simp add: r_neg l_zero)
6.43 + done
6.44 +
6.45 +lemma r_neg1: "-(a::'a::ring) + (a + b) = b"
6.46 + apply (rule a_assoc [symmetric, THEN trans])
6.47 + apply (simp add: l_neg l_zero)
6.48 + done
6.49 +
6.50 +
6.51 +(* auxiliary *)
6.52 +
6.53 +lemma a_lcancel: "!! a::'a::ring. a + b = a + c ==> b = c"
6.54 + apply (rule box_equals)
6.55 + prefer 2
6.56 + apply (rule l_zero)
6.57 + prefer 2
6.58 + apply (rule l_zero)
6.59 + apply (rule_tac a1 = a in l_neg [THEN subst])
6.60 + apply (simp add: a_assoc)
6.61 + done
6.62 +
6.63 +lemma minus_add: "-((a::'a::ring) + b) = (-a) + (-b)"
6.64 + apply (rule_tac a = "a + b" in a_lcancel)
6.65 + apply (simp add: r_neg l_neg l_zero a_assoc a_comm a_lcomm)
6.66 + done
6.67 +
6.68 +lemma minus_minus: "-(-(a::'a::ring)) = a"
6.69 + apply (rule a_lcancel)
6.70 + apply (rule r_neg [THEN trans])
6.71 + apply (rule l_neg [symmetric])
6.72 + done
6.73 +
6.74 +lemma minus0: "- 0 = (0::'a::ring)"
6.75 + apply (rule a_lcancel)
6.76 + apply (rule r_neg [THEN trans])
6.77 + apply (rule l_zero [symmetric])
6.78 + done
6.79 +
6.80 +
6.81 +(* derived rules for multiplication *)
6.82 +
6.83 +lemma m_lcomm: "(a::'a::ring)*(b*c) = b*(a*c)"
6.84 + apply (rule m_comm [THEN trans])
6.85 + apply (rule m_assoc [THEN trans])
6.86 + apply (rule m_comm [THEN arg_cong])
6.87 + done
6.88 +
6.89 +lemma r_one: "(a::'a::ring) * 1 = a"
6.90 + apply (rule m_comm [THEN trans])
6.91 + apply (rule l_one)
6.92 + done
6.93 +
6.94 +lemma r_distr: "(a::'a::ring) * (b + c) = a * b + a * c"
6.95 + apply (rule m_comm [THEN trans])
6.96 + apply (rule l_distr [THEN trans])
6.97 + apply (simp add: m_comm)
6.98 + done
6.99 +
6.100 +
6.101 +(* the following proof is from Jacobson, Basic Algebra I, pp. 88-89 *)
6.102 +lemma l_null: "0 * (a::'a::ring) = 0"
6.103 + apply (rule a_lcancel)
6.104 + apply (rule l_distr [symmetric, THEN trans])
6.105 + apply (simp add: r_zero)
6.106 + done
6.107 +
6.108 +lemma r_null: "(a::'a::ring) * 0 = 0"
6.109 + apply (rule m_comm [THEN trans])
6.110 + apply (rule l_null)
6.111 + done
6.112 +
6.113 +lemma l_minus: "(-(a::'a::ring)) * b = - (a * b)"
6.114 + apply (rule a_lcancel)
6.115 + apply (rule r_neg [symmetric, THEN [2] trans])
6.116 + apply (rule l_distr [symmetric, THEN trans])
6.117 + apply (simp add: l_null r_neg)
6.118 + done
6.119 +
6.120 +lemma r_minus: "(a::'a::ring) * (-b) = - (a * b)"
6.121 + apply (rule a_lcancel)
6.122 + apply (rule r_neg [symmetric, THEN [2] trans])
6.123 + apply (rule r_distr [symmetric, THEN trans])
6.124 + apply (simp add: r_null r_neg)
6.125 + done
6.126 +
6.127 +(*** Term order for commutative rings ***)
6.128 +
6.129 +ML {*
6.130 +fun ring_ord (Const (a, _)) =
6.131 + find_index (fn a' => a = a')
6.132 + ["HOL.zero", "HOL.plus", "HOL.uminus", "HOL.minus", "HOL.one", "HOL.times"]
6.133 + | ring_ord _ = ~1;
6.134 +
6.135 +fun termless_ring (a, b) = (Term.term_lpo ring_ord (a, b) = LESS);
6.136 +
6.137 +val ring_ss = HOL_basic_ss settermless termless_ring addsimps
6.138 + [thm "a_assoc", thm "l_zero", thm "l_neg", thm "a_comm", thm "m_assoc",
6.139 + thm "l_one", thm "l_distr", thm "m_comm", thm "minus_def",
6.140 + thm "r_zero", thm "r_neg", thm "r_neg2", thm "r_neg1", thm "minus_add",
6.141 + thm "minus_minus", thm "minus0", thm "a_lcomm", thm "m_lcomm", (*thm "r_one",*)
6.142 + thm "r_distr", thm "l_null", thm "r_null", thm "l_minus", thm "r_minus"];
6.143 +*} (* Note: r_one is not necessary in ring_ss *)
6.144
6.145 method_setup ring =
6.146 {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (full_simp_tac ring_ss)) *}
6.147 {* computes distributive normal form in rings *}
6.148
6.149 +lemmas ring_simps =
6.150 + l_zero r_zero l_neg r_neg minus_minus minus0
6.151 + l_one r_one l_null r_null l_minus r_minus
6.152 +
6.153
6.154 subsection {* Rings and the summation operator *}
6.155
6.156 @@ -278,7 +404,108 @@
6.157 then show ?thesis using dvd_def by blast
6.158 qed
6.159
6.160 -lemma dvd_def':
6.161 - "m dvd n \<equiv> \<exists>k. n = m * k" unfolding dvd_def by simp
6.162 +
6.163 +lemma unit_mult:
6.164 + "!!a::'a::ring. [| a dvd 1; b dvd 1 |] ==> a * b dvd 1"
6.165 + apply (unfold dvd_def)
6.166 + apply clarify
6.167 + apply (rule_tac x = "k * ka" in exI)
6.168 + apply simp
6.169 + done
6.170 +
6.171 +lemma unit_power: "!!a::'a::ring. a dvd 1 ==> a^n dvd 1"
6.172 + apply (induct_tac n)
6.173 + apply simp
6.174 + apply (simp add: unit_mult)
6.175 + done
6.176 +
6.177 +lemma dvd_add_right [simp]:
6.178 + "!! a::'a::ring. [| a dvd b; a dvd c |] ==> a dvd b + c"
6.179 + apply (unfold dvd_def)
6.180 + apply clarify
6.181 + apply (rule_tac x = "k + ka" in exI)
6.182 + apply (simp add: r_distr)
6.183 + done
6.184 +
6.185 +lemma dvd_uminus_right [simp]:
6.186 + "!! a::'a::ring. a dvd b ==> a dvd -b"
6.187 + apply (unfold dvd_def)
6.188 + apply clarify
6.189 + apply (rule_tac x = "-k" in exI)
6.190 + apply (simp add: r_minus)
6.191 + done
6.192 +
6.193 +lemma dvd_l_mult_right [simp]:
6.194 + "!! a::'a::ring. a dvd b ==> a dvd c*b"
6.195 + apply (unfold dvd_def)
6.196 + apply clarify
6.197 + apply (rule_tac x = "c * k" in exI)
6.198 + apply simp
6.199 + done
6.200 +
6.201 +lemma dvd_r_mult_right [simp]:
6.202 + "!! a::'a::ring. a dvd b ==> a dvd b*c"
6.203 + apply (unfold dvd_def)
6.204 + apply clarify
6.205 + apply (rule_tac x = "k * c" in exI)
6.206 + apply simp
6.207 + done
6.208 +
6.209 +
6.210 +(* Inverse of multiplication *)
6.211 +
6.212 +section "inverse"
6.213 +
6.214 +lemma inverse_unique: "!! a::'a::ring. [| a * x = 1; a * y = 1 |] ==> x = y"
6.215 + apply (rule_tac a = "(a*y) * x" and b = "y * (a*x)" in box_equals)
6.216 + apply (simp (no_asm))
6.217 + apply auto
6.218 + done
6.219 +
6.220 +lemma r_inverse_ring: "!! a::'a::ring. a dvd 1 ==> a * inverse a = 1"
6.221 + apply (unfold inverse_def dvd_def)
6.222 + apply (tactic {* asm_full_simp_tac (simpset () delsimprocs [ring_simproc]) 1 *})
6.223 + apply clarify
6.224 + apply (rule theI)
6.225 + apply assumption
6.226 + apply (rule inverse_unique)
6.227 + apply assumption
6.228 + apply assumption
6.229 + done
6.230 +
6.231 +lemma l_inverse_ring: "!! a::'a::ring. a dvd 1 ==> inverse a * a = 1"
6.232 + by (simp add: r_inverse_ring)
6.233 +
6.234 +
6.235 +(* Fields *)
6.236 +
6.237 +section "Fields"
6.238 +
6.239 +lemma field_unit [simp]: "!! a::'a::field. (a dvd 1) = (a ~= 0)"
6.240 + by (auto dest: field_ax dvd_zero_left simp add: field_one_not_zero)
6.241 +
6.242 +lemma r_inverse [simp]: "!! a::'a::field. a ~= 0 ==> a * inverse a = 1"
6.243 + by (simp add: r_inverse_ring)
6.244 +
6.245 +lemma l_inverse [simp]: "!! a::'a::field. a ~= 0 ==> inverse a * a= 1"
6.246 + by (simp add: l_inverse_ring)
6.247 +
6.248 +
6.249 +(* fields are integral domains *)
6.250 +
6.251 +lemma field_integral: "!! a::'a::field. a * b = 0 ==> a = 0 | b = 0"
6.252 + apply (tactic "Step_tac 1")
6.253 + apply (rule_tac a = " (a*b) * inverse b" in box_equals)
6.254 + apply (rule_tac [3] refl)
6.255 + prefer 2
6.256 + apply (simp (no_asm))
6.257 + apply auto
6.258 + done
6.259 +
6.260 +
6.261 +(* fields are factorial domains *)
6.262 +
6.263 +lemma field_fact_prime: "!! a::'a::field. irred a ==> prime a"
6.264 + unfolding prime_def irred_def by (blast intro: field_ax)
6.265
6.266 end
7.1 --- a/src/HOL/Algebra/abstract/RingHomo.ML Sun Nov 19 13:02:55 2006 +0100
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,64 +0,0 @@
7.4 -(*
7.5 - Ring homomorphism
7.6 - $Id$
7.7 - Author: Clemens Ballarin, started 15 April 1997
7.8 -*)
7.9 -
7.10 -(* Ring homomorphism *)
7.11 -
7.12 -Goalw [thm "homo_def"]
7.13 - "!! f. [| !! a b. f (a + b) = f a + f b; !! a b. f (a * b) = f a * f b; \
7.14 -\ f 1 = 1 |] ==> homo f";
7.15 -by Auto_tac;
7.16 -qed "homoI";
7.17 -
7.18 -Goalw [thm "homo_def"] "!! f. homo f ==> f (a + b) = f a + f b";
7.19 -by (Fast_tac 1);
7.20 -qed "homo_add";
7.21 -
7.22 -Goalw [thm "homo_def"] "!! f. homo f ==> f (a * b) = f a * f b";
7.23 -by (Fast_tac 1);
7.24 -qed "homo_mult";
7.25 -
7.26 -Goalw [thm "homo_def"] "!! f. homo f ==> f 1 = 1";
7.27 -by (Fast_tac 1);
7.28 -qed "homo_one";
7.29 -
7.30 -Goal "!! f::('a::ring=>'b::ring). homo f ==> f 0 = 0";
7.31 -by (res_inst_tac [("a", "f 0")] a_lcancel 1);
7.32 -by (asm_simp_tac (simpset() addsimps [homo_add RS sym]) 1);
7.33 -qed "homo_zero";
7.34 -
7.35 -Goal
7.36 - "!! f::('a::ring=>'b::ring). homo f ==> f (-a) = - f a";
7.37 -by (res_inst_tac [("a", "f a")] a_lcancel 1);
7.38 -by (ftac homo_zero 1);
7.39 -by (asm_simp_tac (simpset() addsimps [homo_add RS sym]) 1);
7.40 -qed "homo_uminus";
7.41 -
7.42 -Goal "!! f::('a::ring=>'b::ring). homo f ==> f (a ^ n) = f a ^ n";
7.43 -by (induct_tac "n" 1);
7.44 -by (dtac homo_one 1);
7.45 -by (Asm_simp_tac 1);
7.46 -by (dres_inst_tac [("a", "a^n"), ("b", "a")] homo_mult 1);
7.47 -by (Asm_full_simp_tac 1);
7.48 -qed "homo_power";
7.49 -
7.50 -Goal
7.51 - "!! f::('a::ring=>'b::ring). \
7.52 -\ homo f ==> f (setsum g {..n::nat}) = setsum (f o g) {..n}";
7.53 -by (induct_tac "n" 1);
7.54 -by (Asm_simp_tac 1);
7.55 -by (Simp_tac 1);
7.56 -by (dres_inst_tac [("a", "g (Suc n)"), ("b", "setsum g {..n}")] homo_add 1);
7.57 -by (Asm_full_simp_tac 1);
7.58 -qed "homo_SUM";
7.59 -
7.60 -Addsimps [homo_add, homo_mult, homo_one, homo_zero,
7.61 - homo_uminus, homo_power, homo_SUM];
7.62 -
7.63 -Goal "homo (%x. x)";
7.64 -by (fast_tac (claset() addSIs [homoI]) 1);
7.65 -qed "id_homo";
7.66 -
7.67 -Addsimps [id_homo];
8.1 --- a/src/HOL/Algebra/abstract/RingHomo.thy Sun Nov 19 13:02:55 2006 +0100
8.2 +++ b/src/HOL/Algebra/abstract/RingHomo.thy Sun Nov 19 23:48:55 2006 +0100
8.3 @@ -4,12 +4,60 @@
8.4 Author: Clemens Ballarin, started 15 April 1997
8.5 *)
8.6
8.7 +header {* Ring homomorphism *}
8.8 +
8.9 theory RingHomo imports Ring2 begin
8.10
8.11 -constdefs
8.12 - homo :: "('a::ring => 'b::ring) => bool"
8.13 - "homo f == (ALL a b. f (a + b) = f a + f b &
8.14 +definition
8.15 + homo :: "('a::ring => 'b::ring) => bool" where
8.16 + "homo f \<longleftrightarrow> (ALL a b. f (a + b) = f a + f b &
8.17 f (a * b) = f a * f b) &
8.18 f 1 = 1"
8.19
8.20 +
8.21 +lemma homoI:
8.22 + "!! f. [| !! a b. f (a + b) = f a + f b; !! a b. f (a * b) = f a * f b;
8.23 + f 1 = 1 |] ==> homo f"
8.24 + unfolding homo_def by blast
8.25 +
8.26 +lemma homo_add [simp]: "!! f. homo f ==> f (a + b) = f a + f b"
8.27 + unfolding homo_def by blast
8.28 +
8.29 +lemma homo_mult [simp]: "!! f. homo f ==> f (a * b) = f a * f b"
8.30 + unfolding homo_def by blast
8.31 +
8.32 +lemma homo_one [simp]: "!! f. homo f ==> f 1 = 1"
8.33 + unfolding homo_def by blast
8.34 +
8.35 +lemma homo_zero [simp]: "!! f::('a::ring=>'b::ring). homo f ==> f 0 = 0"
8.36 + apply (rule_tac a = "f 0" in a_lcancel)
8.37 + apply (simp (no_asm_simp) add: homo_add [symmetric])
8.38 + done
8.39 +
8.40 +lemma homo_uminus [simp]:
8.41 + "!! f::('a::ring=>'b::ring). homo f ==> f (-a) = - f a"
8.42 + apply (rule_tac a = "f a" in a_lcancel)
8.43 + apply (frule homo_zero)
8.44 + apply (simp (no_asm_simp) add: homo_add [symmetric])
8.45 + done
8.46 +
8.47 +lemma homo_power [simp]: "!! f::('a::ring=>'b::ring). homo f ==> f (a ^ n) = f a ^ n"
8.48 + apply (induct_tac n)
8.49 + apply (drule homo_one)
8.50 + apply simp
8.51 + apply (drule_tac a = "a^n" and b = "a" in homo_mult)
8.52 + apply simp
8.53 + done
8.54 +
8.55 +lemma homo_SUM [simp]:
8.56 + "!! f::('a::ring=>'b::ring).
8.57 + homo f ==> f (setsum g {..n::nat}) = setsum (f o g) {..n}"
8.58 + apply (induct_tac n)
8.59 + apply simp
8.60 + apply simp
8.61 + done
8.62 +
8.63 +lemma id_homo [simp]: "homo (%x. x)"
8.64 + by (blast intro!: homoI)
8.65 +
8.66 end
9.1 --- a/src/HOL/Algebra/abstract/order.ML Sun Nov 19 13:02:55 2006 +0100
9.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
9.3 @@ -1,142 +0,0 @@
9.4 -(*
9.5 - Title: Term order, needed for normal forms in rings
9.6 - Id: $Id$
9.7 - Author: Clemens Ballarin
9.8 - Copyright: TU Muenchen
9.9 -*)
9.10 -
9.11 -(*** Term order for commutative rings ***)
9.12 -
9.13 -fun ring_ord (Const (a, _)) =
9.14 - find_index (fn a' => a = a') ["HOL.zero", "HOL.plus", "HOL.uminus", "HOL.minus", "HOL.one", "HOL.times"]
9.15 - | ring_ord _ = ~1;
9.16 -
9.17 -fun termless_ring (a, b) = (Term.term_lpo ring_ord (a, b) = LESS);
9.18 -
9.19 -(* Some code useful for debugging
9.20 -
9.21 -val intT = HOLogic.intT;
9.22 -val a = Free ("a", intT);
9.23 -val b = Free ("b", intT);
9.24 -val c = Free ("c", intT);
9.25 -val plus = Const ("HOL.plus", [intT, intT]--->intT);
9.26 -val mult = Const ("HOL.times", [intT, intT]--->intT);
9.27 -val uminus = Const ("HOL.uminus", intT-->intT);
9.28 -val one = Const ("HOL.one", intT);
9.29 -val f = Const("f", intT-->intT);
9.30 -
9.31 -*)
9.32 -
9.33 -(*** Rewrite rules ***)
9.34 -
9.35 -val a_assoc = thm "ring_class.a_assoc";
9.36 -val l_zero = thm "ring_class.l_zero";
9.37 -val l_neg = thm "ring_class.l_neg";
9.38 -val a_comm = thm "ring_class.a_comm";
9.39 -val m_assoc = thm "ring_class.m_assoc";
9.40 -val l_one = thm "ring_class.l_one";
9.41 -val l_distr = thm "ring_class.l_distr";
9.42 -val m_comm = thm "ring_class.m_comm";
9.43 -val minus_def = thm "ring_class.minus_def";
9.44 -val inverse_def = thm "ring_class.inverse_def";
9.45 -val divide_def = thm "ring_class.divide_def";
9.46 -val power_def = thm "ring_class.power_def";
9.47 -
9.48 -(* These are the following axioms:
9.49 -
9.50 - a_assoc: "(a + b) + c = a + (b + c)"
9.51 - l_zero: "0 + a = a"
9.52 - l_neg: "(-a) + a = 0"
9.53 - a_comm: "a + b = b + a"
9.54 -
9.55 - m_assoc: "(a * b) * c = a * (b * c)"
9.56 - l_one: "1 * a = a"
9.57 -
9.58 - l_distr: "(a + b) * c = a * c + b * c"
9.59 -
9.60 - m_comm: "a * b = b * a"
9.61 -
9.62 - -- {* Definition of derived operations *}
9.63 -
9.64 - minus_def: "a - b = a + (-b)"
9.65 - inverse_def: "inverse a = (if a dvd 1 then THE x. a*x = 1 else 0)"
9.66 - divide_def: "a / b = a * inverse b"
9.67 - power_def: "a ^ n = nat_rec 1 (%u b. b * a) n"
9.68 -*)
9.69 -
9.70 -(* These lemmas are needed in the proofs *)
9.71 -val trans = thm "trans";
9.72 -val sym = thm "sym";
9.73 -val subst = thm "subst";
9.74 -val box_equals = thm "box_equals";
9.75 -val arg_cong = thm "arg_cong";
9.76 -
9.77 -(* derived rewrite rules *)
9.78 -val a_lcomm = prove_goal (the_context ()) "(a::'a::ring)+(b+c) = b+(a+c)"
9.79 - (fn _ => [rtac (a_comm RS trans) 1, rtac (a_assoc RS trans) 1,
9.80 - rtac (a_comm RS arg_cong) 1]);
9.81 -val r_zero = prove_goal (the_context ()) "(a::'a::ring) + 0 = a"
9.82 - (fn _ => [rtac (a_comm RS trans) 1, rtac l_zero 1]);
9.83 -val r_neg = prove_goal (the_context ()) "(a::'a::ring) + (-a) = 0"
9.84 - (fn _ => [rtac (a_comm RS trans) 1, rtac l_neg 1]);
9.85 -val r_neg2 = prove_goal (the_context ()) "(a::'a::ring) + (-a + b) = b"
9.86 - (fn _ => [rtac (a_assoc RS sym RS trans) 1,
9.87 - simp_tac (simpset() addsimps [r_neg, l_zero]) 1]);
9.88 -val r_neg1 = prove_goal (the_context ()) "-(a::'a::ring) + (a + b) = b"
9.89 - (fn _ => [rtac (a_assoc RS sym RS trans) 1,
9.90 - simp_tac (simpset() addsimps [l_neg, l_zero]) 1]);
9.91 -(* auxiliary *)
9.92 -val a_lcancel = prove_goal (the_context ()) "!! a::'a::ring. a + b = a + c ==> b = c"
9.93 - (fn _ => [rtac box_equals 1, rtac l_zero 2, rtac l_zero 2,
9.94 - res_inst_tac [("a1", "a")] (l_neg RS subst) 1,
9.95 - asm_simp_tac (simpset() addsimps [a_assoc]) 1]);
9.96 -val minus_add = prove_goal (the_context ()) "-((a::'a::ring) + b) = (-a) + (-b)"
9.97 - (fn _ => [res_inst_tac [("a", "a+b")] a_lcancel 1,
9.98 - simp_tac (simpset() addsimps [r_neg, l_neg, l_zero,
9.99 - a_assoc, a_comm, a_lcomm]) 1]);
9.100 -val minus_minus = prove_goal (the_context ()) "-(-(a::'a::ring)) = a"
9.101 - (fn _ => [rtac a_lcancel 1, rtac (r_neg RS trans) 1, rtac (l_neg RS sym) 1]);
9.102 -val minus0 = prove_goal (the_context ()) "- 0 = (0::'a::ring)"
9.103 - (fn _ => [rtac a_lcancel 1, rtac (r_neg RS trans) 1,
9.104 - rtac (l_zero RS sym) 1]);
9.105 -
9.106 -(* derived rules for multiplication *)
9.107 -val m_lcomm = prove_goal (the_context ()) "(a::'a::ring)*(b*c) = b*(a*c)"
9.108 - (fn _ => [rtac (m_comm RS trans) 1, rtac (m_assoc RS trans) 1,
9.109 - rtac (m_comm RS arg_cong) 1]);
9.110 -val r_one = prove_goal (the_context ()) "(a::'a::ring) * 1 = a"
9.111 - (fn _ => [rtac (m_comm RS trans) 1, rtac l_one 1]);
9.112 -val r_distr = prove_goal (the_context ()) "(a::'a::ring) * (b + c) = a * b + a * c"
9.113 - (fn _ => [rtac (m_comm RS trans) 1, rtac (l_distr RS trans) 1,
9.114 - simp_tac (simpset() addsimps [m_comm]) 1]);
9.115 -(* the following proof is from Jacobson, Basic Algebra I, pp. 88-89 *)
9.116 -val l_null = prove_goal (the_context ()) "0 * (a::'a::ring) = 0"
9.117 - (fn _ => [rtac a_lcancel 1, rtac (l_distr RS sym RS trans) 1,
9.118 - simp_tac (simpset() addsimps [r_zero]) 1]);
9.119 -val r_null = prove_goal (the_context ()) "(a::'a::ring) * 0 = 0"
9.120 - (fn _ => [rtac (m_comm RS trans) 1, rtac l_null 1]);
9.121 -val l_minus = prove_goal (the_context ()) "(-(a::'a::ring)) * b = - (a * b)"
9.122 - (fn _ => [rtac a_lcancel 1, rtac (r_neg RS sym RSN (2, trans)) 1,
9.123 - rtac (l_distr RS sym RS trans) 1,
9.124 - simp_tac (simpset() addsimps [l_null, r_neg]) 1]);
9.125 -val r_minus = prove_goal (the_context ()) "(a::'a::ring) * (-b) = - (a * b)"
9.126 - (fn _ => [rtac a_lcancel 1, rtac (r_neg RS sym RSN (2, trans)) 1,
9.127 - rtac (r_distr RS sym RS trans) 1,
9.128 - simp_tac (simpset() addsimps [r_null, r_neg]) 1]);
9.129 -
9.130 -val ring_ss = HOL_basic_ss settermless termless_ring addsimps
9.131 - [a_assoc, l_zero, l_neg, a_comm, m_assoc, l_one, l_distr, m_comm, minus_def,
9.132 - r_zero, r_neg, r_neg2, r_neg1, minus_add, minus_minus, minus0,
9.133 - a_lcomm, m_lcomm, (*r_one,*) r_distr, l_null, r_null, l_minus, r_minus];
9.134 -
9.135 -(* Note: r_one is not necessary in ring_ss *)
9.136 -
9.137 -val x = bind_thms ("ring_simps",
9.138 - [l_zero, r_zero, l_neg, r_neg, minus_minus, minus0,
9.139 - l_one, r_one, l_null, r_null, l_minus, r_minus]);
9.140 -
9.141 -(* note: not added (and not proved):
9.142 - a_lcancel_eq, a_rcancel_eq, power_one, power_Suc, power_zero, power_one,
9.143 - m_lcancel_eq, m_rcancel_eq,
9.144 - thms involving dvd, integral domains, fields
9.145 -*)
10.1 --- a/src/HOL/Algebra/poly/LongDiv.ML Sun Nov 19 13:02:55 2006 +0100
10.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
10.3 @@ -1,279 +0,0 @@
10.4 -(*
10.5 - Long division of polynomials
10.6 - $Id$
10.7 - Author: Clemens Ballarin, started 23 June 1999
10.8 -*)
10.9 -
10.10 -(* legacy bindings and theorems *)
10.11 -
10.12 -val deg_aboveI = thm "deg_aboveI";
10.13 -val smult_l_minus = thm "smult_l_minus";
10.14 -val deg_monom_ring = thm "deg_monom_ring";
10.15 -val deg_smult_ring = thm "deg_smult_ring";
10.16 -val smult_l_distr = thm "smult_l_distr";
10.17 -val smult_r_distr = thm "smult_r_distr";
10.18 -val smult_r_minus = thm "smult_r_minus";
10.19 -val smult_assoc2 = thm "smult_assoc2";
10.20 -val smult_assoc1 = thm "smult_assoc1";
10.21 -val monom_mult_smult = thm "monom_mult_smult";
10.22 -val field_ax = thm "field_ax";
10.23 -val lcoeff_nonzero = thm "lcoeff_nonzero";
10.24 -
10.25 -val lcoeff_def = thm "lcoeff_def";
10.26 -val eucl_size_def = thm "eucl_size_def";
10.27 -
10.28 -val SUM_shrink_below_lemma = thm "SUM_shrink_below_lemma";
10.29 -
10.30 -Goal
10.31 - "!! f::(nat=>'a::ring). \
10.32 -\ [| m <= n; !!i. i < m ==> f i = 0; P (setsum (%i. f (i+m)) {..n-m}) |] \
10.33 -\ ==> P (setsum f {..n})";
10.34 -by (asm_full_simp_tac
10.35 - (simpset() addsimps [SUM_shrink_below_lemma, add_diff_inverse, leD]) 1);
10.36 -qed "SUM_extend_below";
10.37 -
10.38 -Goal
10.39 - "!! p::'a::ring up. \
10.40 -\ [| deg p <= n; P (setsum (%i. monom (coeff p i) i) {..n}) |] \
10.41 -\ ==> P p";
10.42 -by (asm_full_simp_tac (simpset() addsimps [thm "up_repr_le"]) 1);
10.43 -qed "up_repr2D";
10.44 -
10.45 -(* Start of LongDiv *)
10.46 -
10.47 -Goal
10.48 - "!!p::('a::ring up). \
10.49 -\ [| deg p <= deg r; deg q <= deg r; \
10.50 -\ coeff p (deg r) = - (coeff q (deg r)); deg r ~= 0 |] ==> \
10.51 -\ deg (p + q) < deg r";
10.52 -by (res_inst_tac [("j", "deg r - 1")] le_less_trans 1);
10.53 -by (arith_tac 2);
10.54 -by (rtac deg_aboveI 1);
10.55 -by (strip_tac 1);
10.56 -by (case_tac "deg r = m" 1);
10.57 -by (Clarify_tac 1);
10.58 -by (Asm_full_simp_tac 1);
10.59 -(* case "deg q ~= m" *)
10.60 -by (subgoal_tac "deg p < m & deg q < m" 1);
10.61 -by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
10.62 -by (arith_tac 1);
10.63 -qed "deg_lcoeff_cancel";
10.64 -
10.65 -Goal
10.66 - "!!p::('a::ring up). \
10.67 -\ [| deg p <= deg r; deg q <= deg r; \
10.68 -\ p ~= -q; coeff p (deg r) = - (coeff q (deg r)) |] ==> \
10.69 -\ deg (p + q) < deg r";
10.70 -by (rtac deg_lcoeff_cancel 1);
10.71 -by (REPEAT (atac 1));
10.72 -by (rtac classical 1);
10.73 -by (Clarify_tac 1);
10.74 -by (etac notE 1);
10.75 -by (res_inst_tac [("p", "p")] up_repr2D 1 THEN atac 1);
10.76 -by (res_inst_tac [("p", "q")] up_repr2D 1 THEN atac 1);
10.77 -by (rotate_tac ~1 1);
10.78 -by (asm_full_simp_tac (simpset() addsimps [smult_l_minus]) 1);
10.79 -qed "deg_lcoeff_cancel2";
10.80 -
10.81 -Goal
10.82 - "!!g::('a::ring up). g ~= 0 ==> \
10.83 -\ Ex (% (q, r, k). \
10.84 -\ (lcoeff g)^k *s f = q * g + r & (eucl_size r < eucl_size g))";
10.85 -by (res_inst_tac [("P", "%f. Ex (% (q, r, k). \
10.86 -\ (lcoeff g)^k *s f = q * g + r & (eucl_size r < eucl_size g))")]
10.87 - wf_induct 1);
10.88 -(* TO DO: replace by measure_induct *)
10.89 -by (res_inst_tac [("f", "eucl_size")] wf_measure 1);
10.90 -by (case_tac "eucl_size x < eucl_size g" 1);
10.91 -by (res_inst_tac [("x", "(0, x, 0)")] exI 1);
10.92 -by (Asm_simp_tac 1);
10.93 -(* case "eucl_size x >= eucl_size g" *)
10.94 -by (dres_inst_tac [("x", "lcoeff g *s x - (monom (lcoeff x) (deg x - deg g)) * g")] spec 1);
10.95 -by (etac impE 1);
10.96 -by (full_simp_tac (simpset() addsimps [inv_image_def, measure_def, lcoeff_def]) 1);
10.97 -by (case_tac "x = 0" 1);
10.98 -by (rotate_tac ~1 1);
10.99 -by (asm_full_simp_tac (simpset() addsimps [eucl_size_def]) 1);
10.100 -(* case "x ~= 0 *)
10.101 -by (rotate_tac ~1 1);
10.102 -by (asm_full_simp_tac (simpset() addsimps [eucl_size_def]) 1);
10.103 -(* by (Simp_tac 1); *)
10.104 -by (rtac impI 1);
10.105 -by (rtac deg_lcoeff_cancel2 1);
10.106 - (* replace by linear arithmetic??? *)
10.107 - by (rtac le_trans 2);
10.108 - by (rtac deg_smult_ring 2);
10.109 - by (Simp_tac 2);
10.110 - by (Simp_tac 1);
10.111 - by (rtac le_trans 1);
10.112 - by (rtac deg_mult_ring 1);
10.113 - by (rtac le_trans 1);
10.114 -(**)
10.115 - by (rtac add_le_mono 1); by (rtac le_refl 1);
10.116 - (* term order forces to use this instead of add_le_mono1 *)
10.117 - by (rtac deg_monom_ring 1);
10.118 - by (Asm_simp_tac 1);
10.119 -(**)
10.120 -(*
10.121 - by (rtac add_le_mono1 1);
10.122 - by (rtac deg_smult_ring 1);
10.123 -(* by (asm_simp_tac (simpset() addsimps [leI]) 1); *)
10.124 - by (Asm_simp_tac 1);
10.125 - by (cut_inst_tac [("m", "deg x - deg g"), ("'a", "'a")] deg_monom_ring 1);
10.126 - by (arith_tac 1);
10.127 -*)
10.128 -by (Force_tac 1);
10.129 -by (Simp_tac 1);
10.130 -(**)
10.131 - (* This change is probably caused by application of commutativity *)
10.132 -by (res_inst_tac [("m", "deg g"), ("n", "deg x")] SUM_extend 1);
10.133 -by (Simp_tac 1);
10.134 -by (Asm_simp_tac 1);
10.135 -by (arith_tac 1);
10.136 -by (res_inst_tac [("m", "deg g"), ("n", "deg g")] SUM_extend_below 1);
10.137 -by (rtac le_refl 1);
10.138 -by (Asm_simp_tac 1);
10.139 -by (arith_tac 1);
10.140 -by (Simp_tac 1);
10.141 -(**)
10.142 -(*
10.143 -by (res_inst_tac [("m", "deg x - deg g"), ("n", "deg x")] SUM_extend 1);
10.144 -by (Simp_tac 1);
10.145 -by (asm_simp_tac (simpset() addsimps [less_not_refl2 RS not_sym]) 1);
10.146 -by (res_inst_tac [("m", "deg x - deg g"), ("n", "deg x - deg g")]
10.147 - SUM_extend_below 1);
10.148 -by (rtac le_refl 1);
10.149 -by (asm_simp_tac (simpset() addsimps [less_not_refl2]) 1);
10.150 -by (asm_simp_tac (simpset() addsimps [diff_diff_right, leI, m_comm]) 1);
10.151 -*)
10.152 -(* end of subproof deg f1 < deg f *)
10.153 -by (etac exE 1);
10.154 -by (res_inst_tac [("x", "((%(q,r,k). (monom (lcoeff g ^ k * lcoeff x) (deg x - deg g) + q)) xa, (%(q,r,k). r) xa, (%(q,r,k). Suc k) xa)")] exI 1);
10.155 -by (Clarify_tac 1);
10.156 -by (dtac sym 1);
10.157 -by (simp_tac (simpset() addsimps [l_distr, a_assoc]
10.158 - delsimprocs [ring_simproc]) 1);
10.159 -by (asm_simp_tac (simpset() delsimprocs [ring_simproc]) 1);
10.160 -by (simp_tac (simpset() addsimps [minus_def, smult_r_distr, smult_r_minus,
10.161 - monom_mult_smult, smult_assoc1, smult_assoc2]
10.162 - delsimprocs [ring_simproc]) 1);
10.163 -by (Simp_tac 1);
10.164 -qed "long_div_eucl_size";
10.165 -
10.166 -Goal
10.167 - "!!g::('a::ring up). g ~= 0 ==> \
10.168 -\ Ex (% (q, r, k). \
10.169 -\ (lcoeff g)^k *s f = q * g + r & (r = 0 | deg r < deg g))";
10.170 -by (forw_inst_tac [("f", "f")]
10.171 - (simplify (simpset() addsimps [eucl_size_def]
10.172 - delsimprocs [ring_simproc]) long_div_eucl_size) 1);
10.173 -by (auto_tac (claset(), simpset() delsimprocs [ring_simproc]));
10.174 -by (case_tac "aa = 0" 1);
10.175 -by (Blast_tac 1);
10.176 -(* case "aa ~= 0 *)
10.177 -by (rotate_tac ~1 1);
10.178 -by Auto_tac;
10.179 -qed "long_div_ring";
10.180 -
10.181 -(* Next one fails *)
10.182 -Goal
10.183 - "!!g::('a::ring up). [| g ~= 0; (lcoeff g) dvd 1 |] ==> \
10.184 -\ Ex (% (q, r). f = q * g + r & (r = 0 | deg r < deg g))";
10.185 -by (forw_inst_tac [("f", "f")] long_div_ring 1);
10.186 -by (etac exE 1);
10.187 -by (res_inst_tac [("x", "((%(q,r,k). (inverse(lcoeff g ^k) *s q)) x, \
10.188 -\ (%(q,r,k). inverse(lcoeff g ^k) *s r) x)")] exI 1);
10.189 -by (Clarify_tac 1);
10.190 -(* by (Simp_tac 1); *)
10.191 -by (rtac conjI 1);
10.192 -by (dtac sym 1);
10.193 -by (asm_simp_tac (simpset() addsimps [smult_r_distr RS sym, smult_assoc2]
10.194 - delsimprocs [ring_simproc]) 1);
10.195 -by (asm_simp_tac (simpset() addsimps [l_inverse_ring, unit_power, smult_assoc1 RS sym]) 1);
10.196 -(* degree property *)
10.197 -by (etac disjE 1);
10.198 -by (Asm_simp_tac 1);
10.199 -by (rtac disjI2 1);
10.200 -by (rtac le_less_trans 1);
10.201 -by (rtac deg_smult_ring 1);
10.202 -by (Asm_simp_tac 1);
10.203 -qed "long_div_unit";
10.204 -
10.205 -Goal
10.206 - "!!g::('a::field up). g ~= 0 ==> \
10.207 -\ Ex (% (q, r). f = q * g + r & (r = 0 | deg r < deg g))";
10.208 -by (rtac long_div_unit 1);
10.209 -by (assume_tac 1);
10.210 -by (asm_simp_tac (simpset() addsimps [lcoeff_def, lcoeff_nonzero, field_ax]) 1);
10.211 -qed "long_div_theorem";
10.212 -
10.213 -Goal "- (0::'a::ring) = 0";
10.214 -by (Simp_tac 1);
10.215 -val uminus_zero = result();
10.216 -
10.217 -Goal "!!a::'a::ring. a - b = 0 ==> a = b";
10.218 -by (res_inst_tac [("s", "a - (a - b)")] trans 1);
10.219 -by (asm_simp_tac (simpset() delsimprocs [ring_simproc]) 1);
10.220 -by (Simp_tac 1);
10.221 -by (Simp_tac 1);
10.222 -val diff_zero_imp_eq = result();
10.223 -
10.224 -Goal "!!a::'a::ring. a = b ==> a + (-b) = 0";
10.225 -by (Asm_simp_tac 1);
10.226 -val eq_imp_diff_zero = result();
10.227 -
10.228 -Goal
10.229 - "!!g::('a::field up). [| g ~= 0; \
10.230 -\ f = q1 * g + r1; (r1 = 0 | deg r1 < deg g); \
10.231 -\ f = q2 * g + r2; (r2 = 0 | deg r2 < deg g) |] ==> q1 = q2";
10.232 -by (subgoal_tac "(q1 - q2) * g = r2 - r1" 1); (* 1 *)
10.233 -by (thin_tac "f = ?x" 1);
10.234 -by (thin_tac "f = ?x" 1);
10.235 -by (rtac diff_zero_imp_eq 1);
10.236 -by (rtac classical 1);
10.237 -by (etac disjE 1);
10.238 -(* r1 = 0 *)
10.239 -by (etac disjE 1);
10.240 -(* r2 = 0 *)
10.241 -by (asm_full_simp_tac (simpset()
10.242 - addsimps [thm "integral_iff", minus_def, l_zero, uminus_zero]
10.243 - delsimprocs [ring_simproc]) 1);
10.244 -(* r2 ~= 0 *)
10.245 -by (dres_inst_tac [("f", "deg"), ("y", "r2 - r1")] arg_cong 1);
10.246 -by (asm_full_simp_tac (simpset() addsimps [minus_def, l_zero, uminus_zero]
10.247 - delsimprocs [ring_simproc]) 1);
10.248 -(* r1 ~=0 *)
10.249 -by (etac disjE 1);
10.250 -(* r2 = 0 *)
10.251 -by (dres_inst_tac [("f", "deg"), ("y", "r2 - r1")] arg_cong 1);
10.252 -by (asm_full_simp_tac (simpset() addsimps [minus_def, l_zero, uminus_zero]
10.253 - delsimprocs [ring_simproc]) 1);
10.254 -(* r2 ~= 0 *)
10.255 -by (dres_inst_tac [("f", "deg"), ("y", "r2 - r1")] arg_cong 1);
10.256 -by (asm_full_simp_tac (simpset() addsimps [minus_def]
10.257 - delsimprocs [ring_simproc]) 1);
10.258 -by (dtac (order_eq_refl RS add_leD2) 1);
10.259 -by (dtac leD 1);
10.260 -by (etac notE 1 THEN rtac (deg_add RS le_less_trans) 1);
10.261 -by (Asm_simp_tac 1);
10.262 -(* proof of 1 *)
10.263 -by (rtac diff_zero_imp_eq 1);
10.264 -by (hyp_subst_tac 1);
10.265 -by (dres_inst_tac [("a", "?x+?y")] eq_imp_diff_zero 1);
10.266 -by (Asm_full_simp_tac 1);
10.267 -qed "long_div_quo_unique";
10.268 -
10.269 -Goal
10.270 - "!!g::('a::field up). [| g ~= 0; \
10.271 -\ f = q1 * g + r1; (r1 = 0 | deg r1 < deg g); \
10.272 -\ f = q2 * g + r2; (r2 = 0 | deg r2 < deg g) |] ==> r1 = r2";
10.273 -by (subgoal_tac "q1 = q2" 1);
10.274 -by (Clarify_tac 1);
10.275 -by (res_inst_tac [("a", "q2 * g + r1 - q2 * g"), ("b", "q2 * g + r2 - q2 * g")]
10.276 - box_equals 1);
10.277 -by (Asm_full_simp_tac 1);
10.278 -by (Simp_tac 1);
10.279 -by (Simp_tac 1);
10.280 -by (rtac long_div_quo_unique 1);
10.281 -by (REPEAT (atac 1));
10.282 -qed "long_div_rem_unique";
11.1 --- a/src/HOL/Algebra/poly/LongDiv.thy Sun Nov 19 13:02:55 2006 +0100
11.2 +++ b/src/HOL/Algebra/poly/LongDiv.thy Sun Nov 19 23:48:55 2006 +0100
11.3 @@ -6,23 +6,255 @@
11.4
11.5 theory LongDiv imports PolyHomo begin
11.6
11.7 -consts
11.8 - lcoeff :: "'a::ring up => 'a"
11.9 - eucl_size :: "'a::ring => nat"
11.10 +definition
11.11 + lcoeff :: "'a::ring up => 'a" where
11.12 + "lcoeff p = coeff p (deg p)"
11.13
11.14 -defs
11.15 - lcoeff_def: "lcoeff p == coeff p (deg p)"
11.16 - eucl_size_def: "eucl_size p == (if p = 0 then 0 else deg p+1)"
11.17 +definition
11.18 + eucl_size :: "'a::zero up => nat" where
11.19 + "eucl_size p = (if p = 0 then 0 else deg p + 1)"
11.20
11.21 lemma SUM_shrink_below_lemma:
11.22 "!! f::(nat=>'a::ring). (ALL i. i < m --> f i = 0) -->
11.23 setsum (%i. f (i+m)) {..d} = setsum f {..m+d}"
11.24 apply (induct_tac d)
11.25 apply (induct_tac m)
11.26 - apply (simp)
11.27 - apply (force)
11.28 - apply (simp add: ab_semigroup_add_class.add_commute[of m])
11.29 + apply simp
11.30 + apply force
11.31 + apply (simp add: ab_semigroup_add_class.add_commute [of m])
11.32 + done
11.33 +
11.34 +lemma SUM_extend_below:
11.35 + "!! f::(nat=>'a::ring).
11.36 + [| m <= n; !!i. i < m ==> f i = 0; P (setsum (%i. f (i+m)) {..n-m}) |]
11.37 + ==> P (setsum f {..n})"
11.38 + by (simp add: SUM_shrink_below_lemma add_diff_inverse leD)
11.39 +
11.40 +lemma up_repr2D:
11.41 + "!! p::'a::ring up.
11.42 + [| deg p <= n; P (setsum (%i. monom (coeff p i) i) {..n}) |]
11.43 + ==> P p"
11.44 + by (simp add: up_repr_le)
11.45 +
11.46 +
11.47 +(* Start of LongDiv *)
11.48 +
11.49 +lemma deg_lcoeff_cancel:
11.50 + "!!p::('a::ring up).
11.51 + [| deg p <= deg r; deg q <= deg r;
11.52 + coeff p (deg r) = - (coeff q (deg r)); deg r ~= 0 |] ==>
11.53 + deg (p + q) < deg r"
11.54 + apply (rule_tac j = "deg r - 1" in le_less_trans)
11.55 + prefer 2
11.56 + apply arith
11.57 + apply (rule deg_aboveI)
11.58 + apply (case_tac "deg r = m")
11.59 + apply clarify
11.60 + apply simp
11.61 + (* case "deg q ~= m" *)
11.62 + apply (subgoal_tac "deg p < m & deg q < m")
11.63 + apply (simp (no_asm_simp) add: deg_aboveD)
11.64 + apply arith
11.65 + done
11.66 +
11.67 +lemma deg_lcoeff_cancel2:
11.68 + "!!p::('a::ring up).
11.69 + [| deg p <= deg r; deg q <= deg r;
11.70 + p ~= -q; coeff p (deg r) = - (coeff q (deg r)) |] ==>
11.71 + deg (p + q) < deg r"
11.72 + apply (rule deg_lcoeff_cancel)
11.73 + apply assumption+
11.74 + apply (rule classical)
11.75 + apply clarify
11.76 + apply (erule notE)
11.77 + apply (rule_tac p = p in up_repr2D, assumption)
11.78 + apply (rule_tac p = q in up_repr2D, assumption)
11.79 + apply (rotate_tac -1)
11.80 + apply (simp add: smult_l_minus)
11.81 + done
11.82 +
11.83 +lemma long_div_eucl_size:
11.84 + "!!g::('a::ring up). g ~= 0 ==>
11.85 + Ex (% (q, r, k).
11.86 + (lcoeff g)^k *s f = q * g + r & (eucl_size r < eucl_size g))"
11.87 + apply (rule_tac P = "%f. Ex (% (q, r, k) . (lcoeff g) ^k *s f = q * g + r & (eucl_size r < eucl_size g))" in wf_induct)
11.88 + (* TO DO: replace by measure_induct *)
11.89 + apply (rule_tac f = eucl_size in wf_measure)
11.90 + apply (case_tac "eucl_size x < eucl_size g")
11.91 + apply (rule_tac x = "(0, x, 0)" in exI)
11.92 + apply (simp (no_asm_simp))
11.93 + (* case "eucl_size x >= eucl_size g" *)
11.94 + apply (drule_tac x = "lcoeff g *s x - (monom (lcoeff x) (deg x - deg g)) * g" in spec)
11.95 + apply (erule impE)
11.96 + apply (simp (no_asm_use) add: inv_image_def measure_def lcoeff_def)
11.97 + apply (case_tac "x = 0")
11.98 + apply (rotate_tac -1)
11.99 + apply (simp add: eucl_size_def)
11.100 + (* case "x ~= 0 *)
11.101 + apply (rotate_tac -1)
11.102 + apply (simp add: eucl_size_def)
11.103 + apply (rule impI)
11.104 + apply (rule deg_lcoeff_cancel2)
11.105 + (* replace by linear arithmetic??? *)
11.106 + apply (rule_tac [2] le_trans)
11.107 + apply (rule_tac [2] deg_smult_ring)
11.108 + prefer 2
11.109 + apply simp
11.110 + apply (simp (no_asm))
11.111 + apply (rule le_trans)
11.112 + apply (rule deg_mult_ring)
11.113 + apply (rule le_trans)
11.114 +(**)
11.115 + apply (rule add_le_mono)
11.116 + apply (rule le_refl)
11.117 + (* term order forces to use this instead of add_le_mono1 *)
11.118 + apply (rule deg_monom_ring)
11.119 + apply (simp (no_asm_simp))
11.120 + apply force
11.121 + apply (simp (no_asm))
11.122 +(**)
11.123 + (* This change is probably caused by application of commutativity *)
11.124 + apply (rule_tac m = "deg g" and n = "deg x" in SUM_extend)
11.125 + apply (simp (no_asm))
11.126 + apply (simp (no_asm_simp))
11.127 + apply arith
11.128 + apply (rule_tac m = "deg g" and n = "deg g" in SUM_extend_below)
11.129 + apply (rule le_refl)
11.130 + apply (simp (no_asm_simp))
11.131 + apply arith
11.132 + apply (simp (no_asm))
11.133 +(**)
11.134 +(* end of subproof deg f1 < deg f *)
11.135 + apply (erule exE)
11.136 + apply (rule_tac x = "((% (q,r,k) . (monom (lcoeff g ^ k * lcoeff x) (deg x - deg g) + q)) xa, (% (q,r,k) . r) xa, (% (q,r,k) . Suc k) xa) " in exI)
11.137 + apply clarify
11.138 + apply (drule sym)
11.139 + apply (tactic {* simp_tac (simpset() addsimps [thm "l_distr", thm "a_assoc"]
11.140 + delsimprocs [ring_simproc]) 1 *})
11.141 + apply (tactic {* asm_simp_tac (simpset() delsimprocs [ring_simproc]) 1 *})
11.142 + apply (tactic {* simp_tac (simpset () addsimps [thm "minus_def", thm "smult_r_distr",
11.143 + thm "smult_r_minus", thm "monom_mult_smult", thm "smult_assoc1", thm "smult_assoc2"]
11.144 + delsimprocs [ring_simproc]) 1 *})
11.145 + apply simp
11.146 + done
11.147 +
11.148 +ML {* simplify (simpset() addsimps [thm "eucl_size_def"]
11.149 + delsimprocs [ring_simproc]) (thm "long_div_eucl_size") *}
11.150 +
11.151 +thm long_div_eucl_size [simplified]
11.152 +
11.153 +lemma long_div_ring:
11.154 + "!!g::('a::ring up). g ~= 0 ==>
11.155 + Ex (% (q, r, k).
11.156 + (lcoeff g)^k *s f = q * g + r & (r = 0 | deg r < deg g))"
11.157 + apply (tactic {* forw_inst_tac [("f", "f")]
11.158 + (simplify (simpset() addsimps [thm "eucl_size_def"]
11.159 + delsimprocs [ring_simproc]) (thm "long_div_eucl_size")) 1 *})
11.160 + apply (tactic {* auto_tac (claset(), simpset() delsimprocs [ring_simproc]) *})
11.161 + apply (case_tac "aa = 0")
11.162 + apply blast
11.163 + (* case "aa ~= 0 *)
11.164 + apply (rotate_tac -1)
11.165 + apply auto
11.166 + done
11.167 +
11.168 +(* Next one fails *)
11.169 +lemma long_div_unit:
11.170 + "!!g::('a::ring up). [| g ~= 0; (lcoeff g) dvd 1 |] ==>
11.171 + Ex (% (q, r). f = q * g + r & (r = 0 | deg r < deg g))"
11.172 + apply (frule_tac f = "f" in long_div_ring)
11.173 + apply (erule exE)
11.174 + apply (rule_tac x = "((% (q,r,k) . (inverse (lcoeff g ^k) *s q)) x, (% (q,r,k) . inverse (lcoeff g ^k) *s r) x) " in exI)
11.175 + apply clarify
11.176 + apply (rule conjI)
11.177 + apply (drule sym)
11.178 + apply (tactic {* asm_simp_tac
11.179 + (simpset() addsimps [thm "smult_r_distr" RS sym, thm "smult_assoc2"]
11.180 + delsimprocs [ring_simproc]) 1 *})
11.181 + apply (simp (no_asm_simp) add: l_inverse_ring unit_power smult_assoc1 [symmetric])
11.182 + (* degree property *)
11.183 + apply (erule disjE)
11.184 + apply (simp (no_asm_simp))
11.185 + apply (rule disjI2)
11.186 + apply (rule le_less_trans)
11.187 + apply (rule deg_smult_ring)
11.188 + apply (simp (no_asm_simp))
11.189 + done
11.190 +
11.191 +lemma long_div_theorem:
11.192 + "!!g::('a::field up). g ~= 0 ==>
11.193 + Ex (% (q, r). f = q * g + r & (r = 0 | deg r < deg g))"
11.194 + apply (rule long_div_unit)
11.195 + apply assumption
11.196 + apply (simp (no_asm_simp) add: lcoeff_def lcoeff_nonzero field_ax)
11.197 + done
11.198 +
11.199 +lemma uminus_zero: "- (0::'a::ring) = 0"
11.200 + by simp
11.201 +
11.202 +lemma diff_zero_imp_eq: "!!a::'a::ring. a - b = 0 ==> a = b"
11.203 + apply (rule_tac s = "a - (a - b) " in trans)
11.204 + apply (tactic {* asm_simp_tac (simpset() delsimprocs [ring_simproc]) 1 *})
11.205 + apply simp
11.206 + apply (simp (no_asm))
11.207 + done
11.208 +
11.209 +lemma eq_imp_diff_zero: "!!a::'a::ring. a = b ==> a + (-b) = 0"
11.210 + by simp
11.211 +
11.212 +lemma long_div_quo_unique:
11.213 + "!!g::('a::field up). [| g ~= 0;
11.214 + f = q1 * g + r1; (r1 = 0 | deg r1 < deg g);
11.215 + f = q2 * g + r2; (r2 = 0 | deg r2 < deg g) |] ==> q1 = q2"
11.216 + apply (subgoal_tac "(q1 - q2) * g = r2 - r1") (* 1 *)
11.217 + apply (erule_tac V = "f = ?x" in thin_rl)
11.218 + apply (erule_tac V = "f = ?x" in thin_rl)
11.219 + apply (rule diff_zero_imp_eq)
11.220 + apply (rule classical)
11.221 + apply (erule disjE)
11.222 + (* r1 = 0 *)
11.223 + apply (erule disjE)
11.224 + (* r2 = 0 *)
11.225 + apply (tactic {* asm_full_simp_tac (simpset()
11.226 + addsimps [thm "integral_iff", thm "minus_def", thm "l_zero", thm "uminus_zero"]
11.227 + delsimprocs [ring_simproc]) 1 *})
11.228 + (* r2 ~= 0 *)
11.229 + apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong)
11.230 + apply (tactic {* asm_full_simp_tac (simpset() addsimps
11.231 + [thm "minus_def", thm "l_zero", thm "uminus_zero"] delsimprocs [ring_simproc]) 1 *})
11.232 + (* r1 ~=0 *)
11.233 + apply (erule disjE)
11.234 + (* r2 = 0 *)
11.235 + apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong)
11.236 + apply (tactic {* asm_full_simp_tac (simpset() addsimps
11.237 + [thm "minus_def", thm "l_zero", thm "uminus_zero"] delsimprocs [ring_simproc]) 1 *})
11.238 + (* r2 ~= 0 *)
11.239 + apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong)
11.240 + apply (tactic {* asm_full_simp_tac (simpset() addsimps [thm "minus_def"]
11.241 + delsimprocs [ring_simproc]) 1 *})
11.242 + apply (drule order_eq_refl [THEN add_leD2])
11.243 + apply (drule leD)
11.244 + apply (erule notE, rule deg_add [THEN le_less_trans])
11.245 + apply (simp (no_asm_simp))
11.246 + (* proof of 1 *)
11.247 + apply (rule diff_zero_imp_eq)
11.248 + apply hypsubst
11.249 + apply (drule_tac a = "?x+?y" in eq_imp_diff_zero)
11.250 + apply simp
11.251 + done
11.252 +
11.253 +lemma long_div_rem_unique:
11.254 + "!!g::('a::field up). [| g ~= 0;
11.255 + f = q1 * g + r1; (r1 = 0 | deg r1 < deg g);
11.256 + f = q2 * g + r2; (r2 = 0 | deg r2 < deg g) |] ==> r1 = r2"
11.257 + apply (subgoal_tac "q1 = q2")
11.258 + apply clarify
11.259 + apply (rule_tac a = "q2 * g + r1 - q2 * g" and b = "q2 * g + r2 - q2 * g" in box_equals)
11.260 + apply simp
11.261 + apply (simp (no_asm))
11.262 + apply (simp (no_asm))
11.263 + apply (rule long_div_quo_unique)
11.264 + apply assumption+
11.265 done
11.266
11.267 end
11.268 -
12.1 --- a/src/HOL/Algebra/poly/PolyHomo.ML Sun Nov 19 13:02:55 2006 +0100
12.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
12.3 @@ -1,232 +0,0 @@
12.4 -(*
12.5 - Universal property and evaluation homomorphism of univariate polynomials
12.6 - $Id$
12.7 - Author: Clemens Ballarin, started 16 April 1997
12.8 -*)
12.9 -
12.10 -(* Summation result for tactic-style proofs *)
12.11 -
12.12 -val natsum_add = thm "natsum_add";
12.13 -val natsum_ldistr = thm "natsum_ldistr";
12.14 -val natsum_rdistr = thm "natsum_rdistr";
12.15 -
12.16 -Goal
12.17 - "!! f::(nat=>'a::ring). \
12.18 -\ m <= n & (ALL i. m < i & i <= n --> f i = 0) --> \
12.19 -\ setsum f {..m} = setsum f {..n}";
12.20 -by (induct_tac "n" 1);
12.21 -(* Base case *)
12.22 -by (Simp_tac 1);
12.23 -(* Induction step *)
12.24 -by (case_tac "m <= n" 1);
12.25 -by Auto_tac;
12.26 -by (subgoal_tac "m = Suc n" 1);
12.27 -by (Asm_simp_tac 1);
12.28 -by (fast_arith_tac 1);
12.29 -val SUM_shrink_lemma = result();
12.30 -
12.31 -Goal
12.32 - "!! f::(nat=>'a::ring). \
12.33 -\ [| m <= n; !!i. [| m < i; i <= n |] ==> f i = 0; P (setsum f {..n}) |] \
12.34 -\ ==> P (setsum f {..m})";
12.35 -by (cut_inst_tac [("m", "m"), ("n", "n"), ("f", "f")] SUM_shrink_lemma 1);
12.36 -by (Asm_full_simp_tac 1);
12.37 -qed "SUM_shrink";
12.38 -
12.39 -Goal
12.40 - "!! f::(nat=>'a::ring). \
12.41 -\ [| m <= n; !!i. [| m < i; i <= n |] ==> f i = 0; P (setsum f {..m}) |] \
12.42 -\ ==> P (setsum f {..n})";
12.43 -by (cut_inst_tac [("m", "m"), ("n", "n"), ("f", "f")] SUM_shrink_lemma 1);
12.44 -by (Asm_full_simp_tac 1);
12.45 -qed "SUM_extend";
12.46 -
12.47 -Goal
12.48 - "!!f::nat=>'a::ring. j <= n + m --> \
12.49 -\ setsum (%k. setsum (%i. f i * g (k - i)) {..k}) {..j} = \
12.50 -\ setsum (%k. setsum (%i. f k * g i) {..j - k}) {..j}";
12.51 -by (induct_tac "j" 1);
12.52 -(* Base case *)
12.53 -by (Simp_tac 1);
12.54 -(* Induction step *)
12.55 -by (simp_tac (simpset() addsimps [Suc_diff_le, natsum_add]) 1);
12.56 -(*
12.57 -by (asm_simp_tac (simpset() addsimps a_ac) 1);
12.58 -*)
12.59 -by (Asm_simp_tac 1);
12.60 -val DiagSum_lemma = result();
12.61 -
12.62 -Goal
12.63 - "!!f::nat=>'a::ring. \
12.64 -\ setsum (%k. setsum (%i. f i * g (k - i)) {..k}) {..n + m} = \
12.65 -\ setsum (%k. setsum (%i. f k * g i) {..n + m - k}) {..n + m}";
12.66 -by (rtac (DiagSum_lemma RS mp) 1);
12.67 -by (rtac le_refl 1);
12.68 -qed "DiagSum";
12.69 -
12.70 -Goal
12.71 - "!! f::nat=>'a::ring. [| bound n f; bound m g|] ==> \
12.72 -\ setsum (%k. setsum (%i. f i * g (k-i)) {..k}) {..n + m} = \
12.73 -\ setsum f {..n} * setsum g {..m}";
12.74 -by (simp_tac (simpset() addsimps [natsum_ldistr, DiagSum]) 1);
12.75 -(* SUM_rdistr must be applied after SUM_ldistr ! *)
12.76 -by (simp_tac (simpset() addsimps [natsum_rdistr]) 1);
12.77 -by (res_inst_tac [("m", "n"), ("n", "n+m")] SUM_extend 1);
12.78 -by (rtac le_add1 1);
12.79 -by (Force_tac 1);
12.80 -by (rtac (thm "natsum_cong") 1);
12.81 -by (rtac refl 1);
12.82 -by (res_inst_tac [("m", "m"), ("n", "n+m-i")] SUM_shrink 1);
12.83 -by (asm_simp_tac (simpset() addsimps [le_add_diff]) 1);
12.84 -by Auto_tac;
12.85 -qed "CauchySum";
12.86 -
12.87 -(* Ring homomorphisms and polynomials *)
12.88 -(*
12.89 -Goal "homo (const::'a::ring=>'a up)";
12.90 -by (auto_tac (claset() addSIs [homoI], simpset()));
12.91 -qed "const_homo";
12.92 -
12.93 -Delsimps [const_add, const_mult, const_one, const_zero];
12.94 -Addsimps [const_homo];
12.95 -
12.96 -Goal
12.97 - "!!f::'a::ring up=>'b::ring. homo f ==> f (a *s p) = f (const a) * f p";
12.98 -by (asm_simp_tac (simpset() addsimps [const_mult_is_smult RS sym]) 1);
12.99 -qed "homo_smult";
12.100 -
12.101 -Addsimps [homo_smult];
12.102 -*)
12.103 -
12.104 -val deg_add = thm "deg_add";
12.105 -val deg_mult_ring = thm "deg_mult_ring";
12.106 -val deg_aboveD = thm "deg_aboveD";
12.107 -val coeff_add = thm "coeff_add";
12.108 -val coeff_mult = thm "coeff_mult";
12.109 -val boundI = thm "boundI";
12.110 -val monom_mult_is_smult = thm "monom_mult_is_smult";
12.111 -
12.112 -(* Evaluation homomorphism *)
12.113 -
12.114 -Goal
12.115 - "!! phi::('a::ring=>'b::ring). homo phi ==> homo (EVAL2 phi a)";
12.116 -by (rtac homoI 1);
12.117 -by (rewtac (thm "EVAL2_def"));
12.118 -(* + commutes *)
12.119 -(* degree estimations:
12.120 - bound of all sums can be extended to max (deg aa) (deg b) *)
12.121 -by (res_inst_tac [("m", "deg (aa + b)"), ("n", "max (deg aa) (deg b)")]
12.122 - SUM_shrink 1);
12.123 -by (rtac deg_add 1);
12.124 -by (asm_simp_tac (simpset() delsimps [coeff_add] addsimps [deg_aboveD]) 1);
12.125 -by (res_inst_tac [("m", "deg aa"), ("n", "max (deg aa) (deg b)")]
12.126 - SUM_shrink 1);
12.127 -by (rtac le_maxI1 1);
12.128 -by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
12.129 -by (res_inst_tac [("m", "deg b"), ("n", "max (deg aa) (deg b)")]
12.130 - SUM_shrink 1);
12.131 -by (rtac le_maxI2 1);
12.132 -by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
12.133 -(* actual homom property + *)
12.134 -by (asm_simp_tac (simpset() addsimps [l_distr, natsum_add]) 1);
12.135 -
12.136 -(* * commutes *)
12.137 -by (res_inst_tac [("m", "deg (aa * b)"), ("n", "deg aa + deg b")]
12.138 - SUM_shrink 1);
12.139 -by (rtac deg_mult_ring 1);
12.140 -by (asm_simp_tac (simpset() delsimps [coeff_mult] addsimps [deg_aboveD]) 1);
12.141 -by (rtac trans 1);
12.142 -by (rtac CauchySum 2);
12.143 -by (asm_simp_tac (simpset() addsimps [boundI, deg_aboveD]) 2);
12.144 -by (asm_simp_tac (simpset() addsimps [boundI, deg_aboveD]) 2);
12.145 -(* getting a^i and a^(k-i) together is difficult, so we do it manually *)
12.146 -by (res_inst_tac [("s",
12.147 -" setsum \
12.148 -\ (%k. setsum \
12.149 -\ (%i. phi (coeff aa i) * (phi (coeff b (k - i)) * \
12.150 -\ (a ^ i * a ^ (k - i)))) {..k}) \
12.151 -\ {..deg aa + deg b}")] trans 1);
12.152 -by (asm_simp_tac (simpset()
12.153 - addsimps [power_mult, leD RS add_diff_inverse, natsum_ldistr]) 1);
12.154 -by (Simp_tac 1);
12.155 -(* 1 commutes *)
12.156 -by (Asm_simp_tac 1);
12.157 -qed "EVAL2_homo";
12.158 -
12.159 -Goalw [thm "EVAL2_def"]
12.160 - "!! phi::'a::ring=>'b::ring. EVAL2 phi a (monom b 0) = phi b";
12.161 -by (Simp_tac 1);
12.162 -qed "EVAL2_const";
12.163 -
12.164 -Goalw [thm "EVAL2_def"]
12.165 - "!! phi::'a::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom 1 1) = a";
12.166 -(* Must be able to distinguish 0 from 1, hence 'a::domain *)
12.167 -by (Asm_simp_tac 1);
12.168 -qed "EVAL2_monom1";
12.169 -
12.170 -Goalw [thm "EVAL2_def"]
12.171 - "!! phi::'a::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom 1 n) = a ^ n";
12.172 -by (Simp_tac 1);
12.173 -by (case_tac "n" 1);
12.174 -by Auto_tac;
12.175 -qed "EVAL2_monom";
12.176 -
12.177 -Goal
12.178 - "!! phi::'a::ring=>'b::ring. \
12.179 -\ homo phi ==> EVAL2 phi a (b *s p) = phi b * EVAL2 phi a p";
12.180 -by (asm_simp_tac (simpset()
12.181 - addsimps [monom_mult_is_smult RS sym, EVAL2_homo, EVAL2_const]) 1);
12.182 -qed "EVAL2_smult";
12.183 -
12.184 -val up_eqI = thm "up_eqI";
12.185 -
12.186 -Goal "monom (a::'a::ring) n = monom a 0 * monom 1 n";
12.187 -by (simp_tac (simpset() addsimps [monom_mult_is_smult]) 1);
12.188 -by (rtac up_eqI 1);
12.189 -by (Simp_tac 1);
12.190 -qed "monom_decomp";
12.191 -
12.192 -Goal
12.193 - "!! phi::'a::domain=>'b::ring. \
12.194 -\ homo phi ==> EVAL2 phi a (monom b n) = phi b * a ^ n";
12.195 -by (stac monom_decomp 1);
12.196 -by (asm_simp_tac (simpset()
12.197 - addsimps [EVAL2_homo, EVAL2_const, EVAL2_monom]) 1);
12.198 -qed "EVAL2_monom_n";
12.199 -
12.200 -Goalw [thm "EVAL_def"] "!! a::'a::ring. homo (EVAL a)";
12.201 -by (asm_simp_tac (simpset() addsimps [EVAL2_homo]) 1);
12.202 -qed "EVAL_homo";
12.203 -
12.204 -Goalw [thm "EVAL_def"] "!! a::'a::ring. EVAL a (monom b 0) = b";
12.205 -by (asm_simp_tac (simpset() addsimps [EVAL2_const]) 1);
12.206 -qed "EVAL_const";
12.207 -
12.208 -Goalw [thm "EVAL_def"] "!! a::'a::domain. EVAL a (monom 1 n) = a ^ n";
12.209 -by (asm_simp_tac (simpset() addsimps [EVAL2_monom]) 1);
12.210 -qed "EVAL_monom";
12.211 -
12.212 -Goalw [thm "EVAL_def"] "!! a::'a::ring. EVAL a (b *s p) = b * EVAL a p";
12.213 -by (asm_simp_tac (simpset() addsimps [EVAL2_smult]) 1);
12.214 -qed "EVAL_smult";
12.215 -
12.216 -Goalw [thm "EVAL_def"] "!! a::'a::domain. EVAL a (monom b n) = b * a ^ n";
12.217 -by (asm_simp_tac (simpset() addsimps [EVAL2_monom_n]) 1);
12.218 -qed "EVAL_monom_n";
12.219 -
12.220 -(* Examples *)
12.221 -
12.222 -Goal
12.223 - "EVAL (x::'a::domain) (a*X^2 + b*X^1 + c*X^0) = a * x ^ 2 + b * x ^ 1 + c";
12.224 -by (asm_simp_tac (simpset() delsimps [power_Suc]
12.225 - addsimps [EVAL_homo, EVAL_monom, EVAL_monom_n]) 1);
12.226 -result();
12.227 -
12.228 -Goal
12.229 - "EVAL (y::'a::domain) \
12.230 -\ (EVAL (monom x 0) (monom 1 1 + monom (a*X^2 + b*X^1 + c*X^0) 0)) = \
12.231 -\ x ^ 1 + (a * y ^ 2 + b * y ^ 1 + c)";
12.232 -by (asm_simp_tac (simpset() delsimps [power_Suc]
12.233 - addsimps [EVAL_homo, EVAL_monom, EVAL_monom_n, EVAL_const]) 1);
12.234 -result();
12.235 -
13.1 --- a/src/HOL/Algebra/poly/PolyHomo.thy Sun Nov 19 13:02:55 2006 +0100
13.2 +++ b/src/HOL/Algebra/poly/PolyHomo.thy Sun Nov 19 23:48:55 2006 +0100
13.3 @@ -6,13 +6,181 @@
13.4
13.5 theory PolyHomo imports UnivPoly2 begin
13.6
13.7 -consts
13.8 - EVAL2 :: "['a::ring => 'b, 'b, 'a up] => 'b::ring"
13.9 - EVAL :: "['a::ring, 'a up] => 'a"
13.10 +definition
13.11 + EVAL2 :: "['a::ring => 'b, 'b, 'a up] => 'b::ring" where
13.12 + "EVAL2 phi a p = setsum (%i. phi (coeff p i) * a ^ i) {..deg p}"
13.13
13.14 -defs
13.15 - EVAL2_def: "EVAL2 phi a p ==
13.16 - setsum (%i. phi (coeff p i) * a ^ i) {..deg p}"
13.17 - EVAL_def: "EVAL == EVAL2 (%x. x)"
13.18 +definition
13.19 + EVAL :: "['a::ring, 'a up] => 'a" where
13.20 + "EVAL = EVAL2 (%x. x)"
13.21 +
13.22 +lemma SUM_shrink_lemma:
13.23 + "!! f::(nat=>'a::ring).
13.24 + m <= n & (ALL i. m < i & i <= n --> f i = 0) -->
13.25 + setsum f {..m} = setsum f {..n}"
13.26 + apply (induct_tac n)
13.27 + (* Base case *)
13.28 + apply (simp (no_asm))
13.29 + (* Induction step *)
13.30 + apply (case_tac "m <= n")
13.31 + apply auto
13.32 + apply (subgoal_tac "m = Suc n")
13.33 + apply (simp (no_asm_simp))
13.34 + apply arith
13.35 + done
13.36 +
13.37 +lemma SUM_shrink:
13.38 + "!! f::(nat=>'a::ring).
13.39 + [| m <= n; !!i. [| m < i; i <= n |] ==> f i = 0; P (setsum f {..n}) |]
13.40 + ==> P (setsum f {..m})"
13.41 + apply (cut_tac m = m and n = n and f = f in SUM_shrink_lemma)
13.42 + apply simp
13.43 + done
13.44 +
13.45 +lemma SUM_extend:
13.46 + "!! f::(nat=>'a::ring).
13.47 + [| m <= n; !!i. [| m < i; i <= n |] ==> f i = 0; P (setsum f {..m}) |]
13.48 + ==> P (setsum f {..n})"
13.49 + apply (cut_tac m = m and n = n and f = f in SUM_shrink_lemma)
13.50 + apply simp
13.51 + done
13.52 +
13.53 +lemma DiagSum_lemma:
13.54 + "!!f::nat=>'a::ring. j <= n + m -->
13.55 + setsum (%k. setsum (%i. f i * g (k - i)) {..k}) {..j} =
13.56 + setsum (%k. setsum (%i. f k * g i) {..j - k}) {..j}"
13.57 + apply (induct_tac j)
13.58 + (* Base case *)
13.59 + apply (simp (no_asm))
13.60 + (* Induction step *)
13.61 + apply (simp (no_asm) add: Suc_diff_le natsum_add)
13.62 + apply (simp (no_asm_simp))
13.63 + done
13.64 +
13.65 +lemma DiagSum:
13.66 + "!!f::nat=>'a::ring.
13.67 + setsum (%k. setsum (%i. f i * g (k - i)) {..k}) {..n + m} =
13.68 + setsum (%k. setsum (%i. f k * g i) {..n + m - k}) {..n + m}"
13.69 + apply (rule DiagSum_lemma [THEN mp])
13.70 + apply (rule le_refl)
13.71 + done
13.72 +
13.73 +lemma CauchySum:
13.74 + "!! f::nat=>'a::ring. [| bound n f; bound m g|] ==>
13.75 + setsum (%k. setsum (%i. f i * g (k-i)) {..k}) {..n + m} =
13.76 + setsum f {..n} * setsum g {..m}"
13.77 + apply (simp (no_asm) add: natsum_ldistr DiagSum)
13.78 + (* SUM_rdistr must be applied after SUM_ldistr ! *)
13.79 + apply (simp (no_asm) add: natsum_rdistr)
13.80 + apply (rule_tac m = n and n = "n + m" in SUM_extend)
13.81 + apply (rule le_add1)
13.82 + apply force
13.83 + apply (rule natsum_cong)
13.84 + apply (rule refl)
13.85 + apply (rule_tac m = m and n = "n +m - i" in SUM_shrink)
13.86 + apply (simp (no_asm_simp) add: le_add_diff)
13.87 + apply auto
13.88 + done
13.89 +
13.90 +(* Evaluation homomorphism *)
13.91 +
13.92 +lemma EVAL2_homo:
13.93 + "!! phi::('a::ring=>'b::ring). homo phi ==> homo (EVAL2 phi a)"
13.94 + apply (rule homoI)
13.95 + apply (unfold EVAL2_def)
13.96 + (* + commutes *)
13.97 + (* degree estimations:
13.98 + bound of all sums can be extended to max (deg aa) (deg b) *)
13.99 + apply (rule_tac m = "deg (aa + b) " and n = "max (deg aa) (deg b)" in SUM_shrink)
13.100 + apply (rule deg_add)
13.101 + apply (simp (no_asm_simp) del: coeff_add add: deg_aboveD)
13.102 + apply (rule_tac m = "deg aa" and n = "max (deg aa) (deg b)" in SUM_shrink)
13.103 + apply (rule le_maxI1)
13.104 + apply (simp (no_asm_simp) add: deg_aboveD)
13.105 + apply (rule_tac m = "deg b" and n = "max (deg aa) (deg b) " in SUM_shrink)
13.106 + apply (rule le_maxI2)
13.107 + apply (simp (no_asm_simp) add: deg_aboveD)
13.108 + (* actual homom property + *)
13.109 + apply (simp (no_asm_simp) add: l_distr natsum_add)
13.110 +
13.111 + (* * commutes *)
13.112 + apply (rule_tac m = "deg (aa * b) " and n = "deg aa + deg b" in SUM_shrink)
13.113 + apply (rule deg_mult_ring)
13.114 + apply (simp (no_asm_simp) del: coeff_mult add: deg_aboveD)
13.115 + apply (rule trans)
13.116 + apply (rule_tac [2] CauchySum)
13.117 + prefer 2
13.118 + apply (simp add: boundI deg_aboveD)
13.119 + prefer 2
13.120 + apply (simp add: boundI deg_aboveD)
13.121 + (* getting a^i and a^(k-i) together is difficult, so we do it manually *)
13.122 + apply (rule_tac s = "setsum (%k. setsum (%i. phi (coeff aa i) * (phi (coeff b (k - i)) * (a ^ i * a ^ (k - i)))) {..k}) {..deg aa + deg b}" in trans)
13.123 + apply (simp (no_asm_simp) add: power_mult leD [THEN add_diff_inverse] natsum_ldistr)
13.124 + apply (simp (no_asm))
13.125 + (* 1 commutes *)
13.126 + apply (simp (no_asm_simp))
13.127 + done
13.128 +
13.129 +lemma EVAL2_const:
13.130 + "!!phi::'a::ring=>'b::ring. EVAL2 phi a (monom b 0) = phi b"
13.131 + by (simp add: EVAL2_def)
13.132 +
13.133 +lemma EVAL2_monom1:
13.134 + "!! phi::'a::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom 1 1) = a"
13.135 + by (simp add: EVAL2_def)
13.136 + (* Must be able to distinguish 0 from 1, hence 'a::domain *)
13.137 +
13.138 +lemma EVAL2_monom:
13.139 + "!! phi::'a::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom 1 n) = a ^ n"
13.140 + apply (unfold EVAL2_def)
13.141 + apply (simp (no_asm))
13.142 + apply (case_tac n)
13.143 + apply auto
13.144 + done
13.145 +
13.146 +lemma EVAL2_smult:
13.147 + "!!phi::'a::ring=>'b::ring.
13.148 + homo phi ==> EVAL2 phi a (b *s p) = phi b * EVAL2 phi a p"
13.149 + by (simp (no_asm_simp) add: monom_mult_is_smult [symmetric] EVAL2_homo EVAL2_const)
13.150 +
13.151 +lemma monom_decomp: "monom (a::'a::ring) n = monom a 0 * monom 1 n"
13.152 + apply (simp (no_asm) add: monom_mult_is_smult)
13.153 + apply (rule up_eqI)
13.154 + apply (simp (no_asm))
13.155 + done
13.156 +
13.157 +lemma EVAL2_monom_n:
13.158 + "!! phi::'a::domain=>'b::ring.
13.159 + homo phi ==> EVAL2 phi a (monom b n) = phi b * a ^ n"
13.160 + apply (subst monom_decomp)
13.161 + apply (simp (no_asm_simp) add: EVAL2_homo EVAL2_const EVAL2_monom)
13.162 + done
13.163 +
13.164 +lemma EVAL_homo: "!!a::'a::ring. homo (EVAL a)"
13.165 + by (simp add: EVAL_def EVAL2_homo)
13.166 +
13.167 +lemma EVAL_const: "!!a::'a::ring. EVAL a (monom b 0) = b"
13.168 + by (simp add: EVAL_def EVAL2_const)
13.169 +
13.170 +lemma EVAL_monom: "!!a::'a::domain. EVAL a (monom 1 n) = a ^ n"
13.171 + by (simp add: EVAL_def EVAL2_monom)
13.172 +
13.173 +lemma EVAL_smult: "!!a::'a::ring. EVAL a (b *s p) = b * EVAL a p"
13.174 + by (simp add: EVAL_def EVAL2_smult)
13.175 +
13.176 +lemma EVAL_monom_n: "!!a::'a::domain. EVAL a (monom b n) = b * a ^ n"
13.177 + by (simp add: EVAL_def EVAL2_monom_n)
13.178 +
13.179 +
13.180 +(* Examples *)
13.181 +
13.182 +lemma "EVAL (x::'a::domain) (a*X^2 + b*X^1 + c*X^0) = a * x ^ 2 + b * x ^ 1 + c"
13.183 + by (simp del: power_Suc add: EVAL_homo EVAL_monom EVAL_monom_n)
13.184 +
13.185 +lemma
13.186 + "EVAL (y::'a::domain)
13.187 + (EVAL (monom x 0) (monom 1 1 + monom (a*X^2 + b*X^1 + c*X^0) 0)) =
13.188 + x ^ 1 + (a * y ^ 2 + b * y ^ 1 + c)"
13.189 + by (simp del: power_Suc add: EVAL_homo EVAL_monom EVAL_monom_n EVAL_const)
13.190
13.191 end
14.1 --- a/src/HOL/Algebra/poly/UnivPoly2.ML Sun Nov 19 13:02:55 2006 +0100
14.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
14.3 @@ -1,359 +0,0 @@
14.4 -(*
14.5 - Degree of polynomials
14.6 - $Id$
14.7 - written by Clemens Ballarin, started 22 January 1997
14.8 -*)
14.9 -
14.10 -(*
14.11 -(* Relating degree and bound *)
14.12 -
14.13 -Goal "[| bound m f; f n ~= 0 |] ==> n <= m";
14.14 -by (force_tac (claset() addDs [inst "m" "n" boundD],
14.15 - simpset()) 1);
14.16 -qed "below_bound";
14.17 -
14.18 -goal UnivPoly2.thy "bound (LEAST n. bound n (Rep_UP p)) (Rep_UP p)";
14.19 -by (rtac exE 1);
14.20 -by (rtac LeastI 2);
14.21 -by (assume_tac 2);
14.22 -by (res_inst_tac [("a", "Rep_UP p")] CollectD 1);
14.23 -by (rtac (rewrite_rule [UP_def] Rep_UP) 1);
14.24 -qed "Least_is_bound";
14.25 -
14.26 -Goalw [coeff_def, deg_def]
14.27 - "!! p. ALL m. n < m --> coeff m p = 0 ==> deg p <= n";
14.28 -by (rtac Least_le 1);
14.29 -by (Fast_tac 1);
14.30 -qed "deg_aboveI";
14.31 -
14.32 -Goalw [coeff_def, deg_def]
14.33 - "(n ~= 0 --> coeff n p ~= 0) ==> n <= deg p";
14.34 -by (case_tac "n = 0" 1);
14.35 -(* Case n=0 *)
14.36 -by (Asm_simp_tac 1);
14.37 -(* Case n~=0 *)
14.38 -by (rotate_tac 1 1);
14.39 -by (Asm_full_simp_tac 1);
14.40 -by (rtac below_bound 1);
14.41 -by (assume_tac 2);
14.42 -by (rtac Least_is_bound 1);
14.43 -qed "deg_belowI";
14.44 -
14.45 -Goalw [coeff_def, deg_def]
14.46 - "deg p < m ==> coeff m p = 0";
14.47 -by (rtac exE 1); (* create !! x. *)
14.48 -by (rtac boundD 2);
14.49 -by (assume_tac 3);
14.50 -by (rtac LeastI 2);
14.51 -by (assume_tac 2);
14.52 -by (res_inst_tac [("a", "Rep_UP p")] CollectD 1);
14.53 -by (rtac (rewrite_rule [UP_def] Rep_UP) 1);
14.54 -qed "deg_aboveD";
14.55 -
14.56 -Goalw [deg_def]
14.57 - "deg p = Suc y ==> ~ bound y (Rep_UP p)";
14.58 -by (rtac not_less_Least 1);
14.59 -by (Asm_simp_tac 1);
14.60 -val lemma1 = result();
14.61 -
14.62 -Goalw [deg_def, coeff_def]
14.63 - "deg p = Suc y ==> coeff (deg p) p ~= 0";
14.64 -by (rtac ccontr 1);
14.65 -by (dtac notnotD 1);
14.66 -by (cut_inst_tac [("p", "p")] Least_is_bound 1);
14.67 -by (subgoal_tac "bound y (Rep_UP p)" 1);
14.68 -(* prove subgoal *)
14.69 -by (rtac boundI 2);
14.70 -by (case_tac "Suc y < m" 2);
14.71 -(* first case *)
14.72 -by (rtac boundD 2);
14.73 -by (assume_tac 2);
14.74 -by (Asm_simp_tac 2);
14.75 -(* second case *)
14.76 -by (dtac leI 2);
14.77 -by (dtac Suc_leI 2);
14.78 -by (dtac le_anti_sym 2);
14.79 -by (assume_tac 2);
14.80 -by (Asm_full_simp_tac 2);
14.81 -(* end prove subgoal *)
14.82 -by (fold_goals_tac [deg_def]);
14.83 -by (dtac lemma1 1);
14.84 -by (etac notE 1);
14.85 -by (assume_tac 1);
14.86 -val lemma2 = result();
14.87 -
14.88 -Goal "deg p ~= 0 ==> coeff (deg p) p ~= 0";
14.89 -by (rtac lemma2 1);
14.90 -by (Full_simp_tac 1);
14.91 -by (dtac Suc_pred 1);
14.92 -by (rtac sym 1);
14.93 -by (Asm_simp_tac 1);
14.94 -qed "deg_lcoeff";
14.95 -
14.96 -Goal "p ~= 0 ==> coeff (deg p) p ~= 0";
14.97 -by (etac contrapos_np 1);
14.98 -by (case_tac "deg p = 0" 1);
14.99 -by (blast_tac (claset() addSDs [deg_lcoeff]) 2);
14.100 -by (rtac up_eqI 1);
14.101 -by (case_tac "n=0" 1);
14.102 -by (rotate_tac ~2 1);
14.103 -by (Asm_full_simp_tac 1);
14.104 -by (asm_full_simp_tac (simpset() addsimps [deg_aboveD]) 1);
14.105 -qed "nonzero_lcoeff";
14.106 -
14.107 -Goal "(deg p <= n) = bound n (Rep_UP p)";
14.108 -by (rtac iffI 1);
14.109 -(* ==> *)
14.110 -by (rtac boundI 1);
14.111 -by (fold_goals_tac [coeff_def]);
14.112 -by (rtac deg_aboveD 1);
14.113 -by (fast_arith_tac 1);
14.114 -(* <== *)
14.115 -by (rtac deg_aboveI 1);
14.116 -by (rewtac coeff_def);
14.117 -by (Fast_tac 1);
14.118 -qed "deg_above_is_bound";
14.119 -
14.120 -(* Lemmas on the degree function *)
14.121 -
14.122 -Goalw [max_def]
14.123 - "!! p::'a::ring up. deg (p + q) <= max (deg p) (deg q)";
14.124 -by (case_tac "deg p <= deg q" 1);
14.125 -(* case deg p <= deg q *)
14.126 -by (rtac deg_aboveI 1);
14.127 -by (Asm_simp_tac 1);
14.128 -by (strip_tac 1);
14.129 -by (dtac le_less_trans 1);
14.130 -by (assume_tac 1);
14.131 -by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
14.132 -(* case deg p > deg q *)
14.133 -by (rtac deg_aboveI 1);
14.134 -by (Asm_simp_tac 1);
14.135 -by (dtac not_leE 1);
14.136 -by (strip_tac 1);
14.137 -by (dtac less_trans 1);
14.138 -by (assume_tac 1);
14.139 -by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
14.140 -qed "deg_add";
14.141 -
14.142 -Goal "!!p::('a::ring up). deg p < deg q ==> deg (p + q) = deg q";
14.143 -by (rtac order_antisym 1);
14.144 -by (rtac le_trans 1);
14.145 -by (rtac deg_add 1);
14.146 -by (Asm_simp_tac 1);
14.147 -by (rtac deg_belowI 1);
14.148 -by (asm_simp_tac (simpset() addsimps [deg_aboveD, deg_lcoeff]) 1);
14.149 -qed "deg_add_equal";
14.150 -
14.151 -Goal "deg (monom m::'a::ring up) <= m";
14.152 -by (asm_simp_tac
14.153 - (simpset() addsimps [deg_aboveI, less_not_refl2 RS not_sym]) 1);
14.154 -qed "deg_monom_ring";
14.155 -
14.156 -Goal "deg (monom m::'a::domain up) = m";
14.157 -by (rtac le_anti_sym 1);
14.158 -(* <= *)
14.159 -by (rtac deg_monom_ring 1);
14.160 -(* >= *)
14.161 -by (asm_simp_tac
14.162 - (simpset() addsimps [deg_belowI, less_not_refl2 RS not_sym]) 1);
14.163 -qed "deg_monom";
14.164 -
14.165 -Goal "!! a::'a::ring. deg (const a) = 0";
14.166 -by (rtac le_anti_sym 1);
14.167 -by (rtac deg_aboveI 1);
14.168 -by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
14.169 -by (rtac deg_belowI 1);
14.170 -by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
14.171 -qed "deg_const";
14.172 -
14.173 -Goal "deg (0::'a::ringS up) = 0";
14.174 -by (rtac le_anti_sym 1);
14.175 -by (rtac deg_aboveI 1);
14.176 -by (Simp_tac 1);
14.177 -by (rtac deg_belowI 1);
14.178 -by (Simp_tac 1);
14.179 -qed "deg_zero";
14.180 -
14.181 -Goal "deg (<1>::'a::ring up) = 0";
14.182 -by (rtac le_anti_sym 1);
14.183 -by (rtac deg_aboveI 1);
14.184 -by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
14.185 -by (rtac deg_belowI 1);
14.186 -by (Simp_tac 1);
14.187 -qed "deg_one";
14.188 -
14.189 -Goal "!!p::('a::ring) up. deg (-p) = deg p";
14.190 -by (rtac le_anti_sym 1);
14.191 -(* <= *)
14.192 -by (simp_tac (simpset() addsimps [deg_aboveI, deg_aboveD]) 1);
14.193 -by (simp_tac (simpset() addsimps [deg_belowI, deg_lcoeff, uminus_monom_neq]) 1);
14.194 -qed "deg_uminus";
14.195 -
14.196 -Addsimps [deg_monom, deg_const, deg_zero, deg_one, deg_uminus];
14.197 -
14.198 -Goal
14.199 - "!! a::'a::ring. deg (a *s p) <= (if a = 0 then 0 else deg p)";
14.200 -by (case_tac "a = 0" 1);
14.201 -by (REPEAT (asm_simp_tac (simpset() addsimps [deg_aboveI, deg_aboveD]) 1));
14.202 -qed "deg_smult_ring";
14.203 -
14.204 -Goal
14.205 - "!! a::'a::domain. deg (a *s p) = (if a = 0 then 0 else deg p)";
14.206 -by (rtac le_anti_sym 1);
14.207 -by (rtac deg_smult_ring 1);
14.208 -by (case_tac "a = 0" 1);
14.209 -by (REPEAT (asm_simp_tac (simpset() addsimps [deg_belowI, deg_lcoeff]) 1));
14.210 -qed "deg_smult";
14.211 -
14.212 -Goal
14.213 - "!! p::'a::ring up. [| deg p + deg q < k |] ==> \
14.214 -\ coeff i p * coeff (k - i) q = 0";
14.215 -by (simp_tac (simpset() addsimps [coeff_def]) 1);
14.216 -by (rtac bound_mult_zero 1);
14.217 -by (assume_tac 3);
14.218 -by (simp_tac (simpset() addsimps [deg_above_is_bound RS sym]) 1);
14.219 -by (simp_tac (simpset() addsimps [deg_above_is_bound RS sym]) 1);
14.220 -qed "deg_above_mult_zero";
14.221 -
14.222 -Goal
14.223 - "!! p::'a::ring up. deg (p * q) <= deg p + deg q";
14.224 -by (rtac deg_aboveI 1);
14.225 -by (asm_simp_tac (simpset() addsimps [deg_above_mult_zero]) 1);
14.226 -qed "deg_mult_ring";
14.227 -
14.228 -goal Main.thy
14.229 - "!!k::nat. k < n ==> m < n + m - k";
14.230 -by (arith_tac 1);
14.231 -qed "less_add_diff";
14.232 -
14.233 -Goal "!!p. coeff n p ~= 0 ==> n <= deg p";
14.234 -(* More general than deg_belowI, and simplifies the next proof! *)
14.235 -by (rtac deg_belowI 1);
14.236 -by (Fast_tac 1);
14.237 -qed "deg_below2I";
14.238 -
14.239 -Goal
14.240 - "!! p::'a::domain up. \
14.241 -\ [| p ~= 0; q ~= 0 |] ==> deg (p * q) = deg p + deg q";
14.242 -by (rtac le_anti_sym 1);
14.243 -by (rtac deg_mult_ring 1);
14.244 -(* deg p + deg q <= deg (p * q) *)
14.245 -by (rtac deg_below2I 1);
14.246 -by (Simp_tac 1);
14.247 -(*
14.248 -by (rtac conjI 1);
14.249 -by (rtac impI 1);
14.250 -*)
14.251 -by (res_inst_tac [("m", "deg p"), ("n", "deg p + deg q")] SUM_extend 1);
14.252 -by (rtac le_add1 1);
14.253 -by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
14.254 -by (res_inst_tac [("m", "deg p"), ("n", "deg p")] SUM_extend_below 1);
14.255 -by (rtac le_refl 1);
14.256 -by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
14.257 -by (asm_simp_tac (simpset() addsimps [nonzero_lcoeff]) 1);
14.258 -(*
14.259 -by (rtac impI 1);
14.260 -by (res_inst_tac [("m", "deg p"), ("n", "deg p + deg q")] SUM_extend 1);
14.261 -by (rtac le_add1 1);
14.262 -by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
14.263 -by (res_inst_tac [("m", "deg p"), ("n", "deg p")] SUM_extend_below 1);
14.264 -by (rtac le_refl 1);
14.265 -by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
14.266 -by (asm_simp_tac (simpset() addsimps [nonzero_lcoeff]) 1);
14.267 -*)
14.268 -qed "deg_mult";
14.269 -
14.270 -Addsimps [deg_smult, deg_mult];
14.271 -
14.272 -(* Representation theorems about polynomials *)
14.273 -
14.274 -goal PolyRing.thy
14.275 - "!! p::nat=>'a::ring up. \
14.276 -\ coeff k (setsum p {..n}) = setsum (%i. coeff k (p i)) {..n}";
14.277 -by (induct_tac "n" 1);
14.278 -by Auto_tac;
14.279 -qed "coeff_SUM";
14.280 -
14.281 -goal UnivPoly2.thy
14.282 - "!! f::(nat=>'a::ring). \
14.283 -\ bound n f ==> setsum (%i. if i = x then f i else 0) {..n} = f x";
14.284 -by (simp_tac (simpset() addsimps [SUM_if_singleton]) 1);
14.285 -by (auto_tac
14.286 - (claset() addDs [not_leE],
14.287 - simpset()));
14.288 -qed "bound_SUM_if";
14.289 -
14.290 -Goal
14.291 - "!! p::'a::ring up. deg p <= n ==> \
14.292 -\ setsum (%i. coeff i p *s monom i) {..n} = p";
14.293 -by (rtac up_eqI 1);
14.294 -by (simp_tac (simpset() addsimps [coeff_SUM]) 1);
14.295 -by (rtac trans 1);
14.296 -by (res_inst_tac [("x", "na")] bound_SUM_if 2);
14.297 -by (full_simp_tac (simpset() addsimps [deg_above_is_bound, coeff_def]) 2);
14.298 -by (rtac SUM_cong 1);
14.299 -by (rtac refl 1);
14.300 -by (Asm_simp_tac 1);
14.301 -qed "up_repr";
14.302 -
14.303 -Goal
14.304 - "!! p::'a::ring up. [| deg p <= n; P p |] ==> \
14.305 -\ P (setsum (%i. coeff i p *s monom i) {..n})";
14.306 -by (asm_simp_tac (simpset() addsimps [up_repr]) 1);
14.307 -qed "up_reprD";
14.308 -
14.309 -Goal
14.310 - "!! p::'a::ring up. \
14.311 -\ [| deg p <= n; P (setsum (%i. coeff i p *s monom i) {..n}) |] \
14.312 -\ ==> P p";
14.313 -by (asm_full_simp_tac (simpset() addsimps [up_repr]) 1);
14.314 -qed "up_repr2D";
14.315 -
14.316 -(*
14.317 -Goal
14.318 - "!! p::'a::ring up. [| deg p <= n; deg q <= m |] ==> \
14.319 -\ (SUM n (%i. coeff i p *s monom i) = SUM m (%i. coeff i q *s monom i)) \
14.320 -\ = (coeff k f = coeff k g)
14.321 -...
14.322 -qed "up_unique";
14.323 -*)
14.324 -
14.325 -(* Polynomials over integral domains are again integral domains *)
14.326 -
14.327 -Goal "!!p::'a::domain up. p * q = 0 ==> p = 0 | q = 0";
14.328 -by (rtac classical 1);
14.329 -by (subgoal_tac "deg p = 0 & deg q = 0" 1);
14.330 -by (res_inst_tac [("p", "p"), ("n", "0")] up_repr2D 1);
14.331 -by (Asm_simp_tac 1);
14.332 -by (res_inst_tac [("p", "q"), ("n", "0")] up_repr2D 1);
14.333 -by (Asm_simp_tac 1);
14.334 -by (subgoal_tac "coeff 0 p = 0 | coeff 0 q = 0" 1);
14.335 -by (force_tac (claset() addIs [up_eqI], simpset()) 1);
14.336 -by (rtac integral 1);
14.337 -by (subgoal_tac "coeff 0 (p * q) = 0" 1);
14.338 -by (Asm_simp_tac 2);
14.339 -by (Full_simp_tac 1);
14.340 -by (dres_inst_tac [("f", "deg")] arg_cong 1);
14.341 -by (Asm_full_simp_tac 1);
14.342 -qed "up_integral";
14.343 -
14.344 -Goal "!! a::'a::domain. a *s p = 0 ==> a = 0 | p = 0";
14.345 -by (full_simp_tac (simpset() addsimps [const_mult_is_smult RS sym]) 1);
14.346 -by (dtac up_integral 1);
14.347 -by Auto_tac;
14.348 -by (rtac (const_inj RS injD) 1);
14.349 -by (Simp_tac 1);
14.350 -qed "smult_integral";
14.351 -*)
14.352 -
14.353 -(* Divisibility and degree *)
14.354 -
14.355 -Goalw [dvd_def]
14.356 - "!! p::'a::domain up. [| p dvd q; q ~= 0 |] ==> deg p <= deg q";
14.357 -by (etac exE 1);
14.358 -by (hyp_subst_tac 1);
14.359 -by (case_tac "p = 0" 1);
14.360 -by (case_tac "k = 0" 2);
14.361 -by Auto_tac;
14.362 -qed "dvd_imp_deg";
15.1 --- a/src/HOL/Algebra/poly/UnivPoly2.thy Sun Nov 19 13:02:55 2006 +0100
15.2 +++ b/src/HOL/Algebra/poly/UnivPoly2.thy Sun Nov 19 23:48:55 2006 +0100
15.3 @@ -11,29 +11,6 @@
15.4 imports "../abstract/Abstract"
15.5 begin
15.6
15.7 -(* already proved in Finite_Set.thy
15.8 -
15.9 -lemma setsum_cong:
15.10 - "[| A = B; !!i. i : B ==> f i = g i |] ==> setsum f A = setsum g B"
15.11 -proof -
15.12 - assume prems: "A = B" "!!i. i : B ==> f i = g i"
15.13 - show ?thesis
15.14 - proof (cases "finite B")
15.15 - case True
15.16 - then have "!!A. [| A = B; !!i. i : B ==> f i = g i |] ==>
15.17 - setsum f A = setsum g B"
15.18 - proof induct
15.19 - case empty thus ?case by simp
15.20 - next
15.21 - case insert thus ?case by simp
15.22 - qed
15.23 - with prems show ?thesis by simp
15.24 - next
15.25 - case False with prems show ?thesis by (simp add: setsum_def)
15.26 - qed
15.27 -qed
15.28 -*)
15.29 -
15.30 (* With this variant of setsum_cong, assumptions
15.31 like i:{m..n} get simplified (to m <= i & i <= n). *)
15.32
15.33 @@ -41,21 +18,18 @@
15.34
15.35 section {* Definition of type up *}
15.36
15.37 -constdefs
15.38 - bound :: "[nat, nat => 'a::zero] => bool"
15.39 - "bound n f == (ALL i. n < i --> f i = 0)"
15.40 +definition
15.41 + bound :: "[nat, nat => 'a::zero] => bool" where
15.42 + "bound n f = (ALL i. n < i --> f i = 0)"
15.43
15.44 lemma boundI [intro!]: "[| !! m. n < m ==> f m = 0 |] ==> bound n f"
15.45 -proof (unfold bound_def)
15.46 -qed fast
15.47 + unfolding bound_def by blast
15.48
15.49 lemma boundE [elim?]: "[| bound n f; (!! m. n < m ==> f m = 0) ==> P |] ==> P"
15.50 -proof (unfold bound_def)
15.51 -qed fast
15.52 + unfolding bound_def by blast
15.53
15.54 lemma boundD [dest]: "[| bound n f; n < m |] ==> f m = 0"
15.55 -proof (unfold bound_def)
15.56 -qed fast
15.57 + unfolding bound_def by blast
15.58
15.59 lemma bound_below:
15.60 assumes bound: "bound m f" and nonzero: "f n ~= 0" shows "n <= m"
15.61 @@ -67,20 +41,23 @@
15.62 qed
15.63
15.64 typedef (UP)
15.65 - ('a) up = "{f :: nat => 'a::zero. EX n. bound n f}"
15.66 -by (rule+) (* Question: what does trace_rule show??? *)
15.67 + ('a) up = "{f :: nat => 'a::zero. EX n. bound n f}"
15.68 + by (rule+) (* Question: what does trace_rule show??? *)
15.69 +
15.70
15.71 section {* Constants *}
15.72
15.73 -consts
15.74 - coeff :: "['a up, nat] => ('a::zero)"
15.75 - monom :: "['a::zero, nat] => 'a up" ("(3_*X^/_)" [71, 71] 70)
15.76 - "*s" :: "['a::{zero, times}, 'a up] => 'a up" (infixl 70)
15.77 +definition
15.78 + coeff :: "['a up, nat] => ('a::zero)" where
15.79 + "coeff p n = Rep_UP p n"
15.80
15.81 -defs
15.82 - coeff_def: "coeff p n == Rep_UP p n"
15.83 - monom_def: "monom a n == Abs_UP (%i. if i=n then a else 0)"
15.84 - smult_def: "a *s p == Abs_UP (%i. a * Rep_UP p i)"
15.85 +definition
15.86 + monom :: "['a::zero, nat] => 'a up" ("(3_*X^/_)" [71, 71] 70) where
15.87 + "monom a n = Abs_UP (%i. if i=n then a else 0)"
15.88 +
15.89 +definition
15.90 + smult :: "['a::{zero, times}, 'a up] => 'a up" (infixl "*s" 70) where
15.91 + "a *s p = Abs_UP (%i. a * Rep_UP p i)"
15.92
15.93 lemma coeff_bound_ex: "EX n. bound n (coeff p)"
15.94 proof -
15.95 @@ -97,6 +74,7 @@
15.96 with prem show P .
15.97 qed
15.98
15.99 +
15.100 text {* Ring operations *}
15.101
15.102 instance up :: (zero) zero ..
15.103 @@ -124,6 +102,7 @@
15.104 up_power_def: "(a::'a::{one, times, power} up) ^ n ==
15.105 nat_rec 1 (%u b. b * a) n"
15.106
15.107 +
15.108 subsection {* Effect of operations on coefficients *}
15.109
15.110 lemma coeff_monom [simp]: "coeff (monom a m) n = (if m=n then a else 0)"
15.111 @@ -451,9 +430,9 @@
15.112
15.113 section {* The degree function *}
15.114
15.115 -constdefs
15.116 - deg :: "('a::zero) up => nat"
15.117 - "deg p == LEAST n. bound n (coeff p)"
15.118 +definition
15.119 + deg :: "('a::zero) up => nat" where
15.120 + "deg p = (LEAST n. bound n (coeff p))"
15.121
15.122 lemma deg_aboveI:
15.123 "(!!m. n < m ==> coeff p m = 0) ==> deg p <= n"
15.124 @@ -773,4 +752,16 @@
15.125 "(a::'a::domain) *s p = 0 ==> a = 0 | p = 0"
15.126 by (simp add: monom_mult_is_smult [THEN sym] integral_iff monom_inj_zero)
15.127
15.128 +
15.129 +(* Divisibility and degree *)
15.130 +
15.131 +lemma "!! p::'a::domain up. [| p dvd q; q ~= 0 |] ==> deg p <= deg q"
15.132 + apply (unfold dvd_def)
15.133 + apply (erule exE)
15.134 + apply hypsubst
15.135 + apply (case_tac "p = 0")
15.136 + apply (case_tac [2] "k = 0")
15.137 + apply auto
15.138 + done
15.139 +
15.140 end
16.1 --- a/src/HOL/IsaMakefile Sun Nov 19 13:02:55 2006 +0100
16.2 +++ b/src/HOL/IsaMakefile Sun Nov 19 23:48:55 2006 +0100
16.3 @@ -385,37 +385,19 @@
16.4
16.5 HOL-Algebra: HOL $(LOG)/HOL-Algebra.gz
16.6
16.7 -$(LOG)/HOL-Algebra.gz: $(OUT)/HOL Algebra/ROOT.ML \
16.8 - Library/Primes.thy Library/FuncSet.thy \
16.9 - Algebra/AbelCoset.thy \
16.10 - Algebra/Bij.thy \
16.11 - Algebra/Coset.thy \
16.12 - Algebra/Exponent.thy \
16.13 - Algebra/FiniteProduct.thy \
16.14 - Algebra/Group.thy \
16.15 - Algebra/Ideal.thy \
16.16 - Algebra/Lattice.thy \
16.17 - Algebra/Module.thy \
16.18 - Algebra/Ring.thy \
16.19 - Algebra/Sylow.thy \
16.20 - Algebra/UnivPoly.thy \
16.21 - Algebra/IntRing.thy \
16.22 - Algebra/QuotRing.thy \
16.23 - Algebra/RingHom.thy \
16.24 - Algebra/abstract/Abstract.thy \
16.25 - Algebra/abstract/Factor.ML Algebra/abstract/Factor.thy \
16.26 - Algebra/abstract/Field.thy \
16.27 - Algebra/abstract/Ideal2.ML Algebra/abstract/Ideal2.thy \
16.28 - Algebra/abstract/PID.thy \
16.29 - Algebra/abstract/Ring2.ML Algebra/abstract/Ring2.thy \
16.30 - Algebra/abstract/RingHomo.ML Algebra/abstract/RingHomo.thy\
16.31 - Algebra/abstract/order.ML \
16.32 - Algebra/document/root.tex \
16.33 - Algebra/poly/LongDiv.ML Algebra/poly/LongDiv.thy \
16.34 - Algebra/poly/PolyHomo.ML Algebra/poly/PolyHomo.thy \
16.35 - Algebra/poly/Polynomial.thy \
16.36 - Algebra/poly/UnivPoly2.ML Algebra/poly/UnivPoly2.thy \
16.37 - Algebra/ringsimp.ML
16.38 +$(LOG)/HOL-Algebra.gz: $(OUT)/HOL Algebra/ROOT.ML Library/Primes.thy \
16.39 + Library/FuncSet.thy Algebra/AbelCoset.thy Algebra/Bij.thy \
16.40 + Algebra/Coset.thy Algebra/Exponent.thy Algebra/FiniteProduct.thy \
16.41 + Algebra/Group.thy Algebra/Ideal.thy Algebra/IntRing.thy \
16.42 + Algebra/Lattice.thy Algebra/Module.thy Algebra/QuotRing.thy \
16.43 + Algebra/Ring.thy Algebra/RingHom.thy Algebra/Sylow.thy \
16.44 + Algebra/UnivPoly.thy Algebra/abstract/Abstract.thy \
16.45 + Algebra/abstract/Factor.thy Algebra/abstract/Field.thy \
16.46 + Algebra/abstract/Ideal2.thy Algebra/abstract/PID.thy \
16.47 + Algebra/abstract/Ring2.thy Algebra/abstract/RingHomo.thy \
16.48 + Algebra/document/root.tex Algebra/poly/LongDiv.thy \
16.49 + Algebra/poly/PolyHomo.thy Algebra/poly/Polynomial.thy \
16.50 + Algebra/poly/UnivPoly2.thy Algebra/ringsimp.ML
16.51 @cd Algebra; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Algebra
16.52
16.53 ## HOL-Auth