# HG changeset patch # User wenzelm # Date 1163976535 -3600 # Node ID 6cdd0589aa73f03dbbd7a402ef7cc07b3b434352 # Parent 25ed0a4c7dc52da06a15fd158e2b3221580a01f8 HOL-Algebra: converted legacy ML scripts; diff -r 25ed0a4c7dc5 -r 6cdd0589aa73 src/HOL/Algebra/abstract/Factor.ML --- a/src/HOL/Algebra/abstract/Factor.ML Sun Nov 19 13:02:55 2006 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,47 +0,0 @@ -(* - Factorisation within a factorial domain - $Id$ - Author: Clemens Ballarin, started 25 November 1997 -*) - -Goalw [thm "assoc_def"] "!! c::'a::factorial. \ -\ [| irred c; irred a; irred b; c dvd a*b |] ==> c assoc a | c assoc b"; -by (ftac (thm "factorial_prime") 1); -by (rewrite_goals_tac [thm "irred_def", thm "prime_def"]); -by (Blast_tac 1); -qed "irred_dvd_lemma"; - -Goalw [thm "assoc_def"] "!! c::'a::factorial. \ -\ [| irred c; a dvd 1 |] ==> \ -\ (ALL b : set factors. irred b) & c dvd foldr op* factors a --> \ -\ (EX d. c assoc d & d : set factors)"; -by (induct_tac "factors" 1); -(* Base case: c dvd a contradicts irred c *) -by (full_simp_tac (simpset() addsimps [thm "irred_def"]) 1); -by (blast_tac (claset() addIs [thm "dvd_trans_ring"]) 1); -(* Induction step *) -by (ftac (thm "factorial_prime") 1); -by (full_simp_tac (simpset() addsimps [thm "irred_def", thm "prime_def"]) 1); -by (Blast_tac 1); -qed "irred_dvd_list_lemma"; - -Goal "!! c::'a::factorial. \ -\ [| irred c; ALL b : set factors. irred b; a dvd 1; \ -\ c dvd foldr op* factors a |] ==> \ -\ EX d. c assoc d & d : set factors"; -by (rtac (irred_dvd_list_lemma RS mp) 1); -by (Auto_tac); -qed "irred_dvd_list"; - -Goalw [thm "Factorisation_def"] "!! c::'a::factorial. \ -\ [| irred c; Factorisation x factors u; c dvd x |] ==> \ -\ EX d. c assoc d & d : set factors"; -by (rtac (irred_dvd_list_lemma RS mp) 1); -by (Auto_tac); -qed "Factorisation_dvd"; - -Goalw [thm "Factorisation_def"] "!! c::'a::factorial. \ -\ [| Factorisation x factors u; a : set factors |] ==> irred a"; -by (Blast_tac 1); -qed "Factorisation_irred"; - diff -r 25ed0a4c7dc5 -r 6cdd0589aa73 src/HOL/Algebra/abstract/Factor.thy --- a/src/HOL/Algebra/abstract/Factor.thy Sun Nov 19 13:02:55 2006 +0100 +++ b/src/HOL/Algebra/abstract/Factor.thy Sun Nov 19 23:48:55 2006 +0100 @@ -6,11 +6,54 @@ theory Factor imports Ring2 begin -constdefs - Factorisation :: "['a::ring, 'a list, 'a] => bool" +definition + Factorisation :: "['a::ring, 'a list, 'a] => bool" where (* factorisation of x into a list of irred factors and a unit u *) - "Factorisation x factors u == + "Factorisation x factors u \ x = foldr op* factors u & (ALL a : set factors. irred a) & u dvd 1" +lemma irred_dvd_lemma: "!! c::'a::factorial. + [| irred c; irred a; irred b; c dvd a*b |] ==> c assoc a | c assoc b" + apply (unfold assoc_def) + apply (frule factorial_prime) + apply (unfold irred_def prime_def) + apply blast + done + +lemma irred_dvd_list_lemma: "!! c::'a::factorial. + [| irred c; a dvd 1 |] ==> + (ALL b : set factors. irred b) & c dvd foldr op* factors a --> + (EX d. c assoc d & d : set factors)" + apply (unfold assoc_def) + apply (induct_tac factors) + (* Base case: c dvd a contradicts irred c *) + apply (simp add: irred_def) + apply (blast intro: dvd_trans_ring) + (* Induction step *) + apply (frule factorial_prime) + apply (simp add: irred_def prime_def) + apply blast + done + +lemma irred_dvd_list: "!! c::'a::factorial. + [| irred c; ALL b : set factors. irred b; a dvd 1; + c dvd foldr op* factors a |] ==> + EX d. c assoc d & d : set factors" + apply (rule irred_dvd_list_lemma [THEN mp]) + apply auto + done + +lemma Factorisation_dvd: "!! c::'a::factorial. + [| irred c; Factorisation x factors u; c dvd x |] ==> + EX d. c assoc d & d : set factors" + apply (unfold Factorisation_def) + apply (rule irred_dvd_list_lemma [THEN mp]) + apply auto + done + +lemma Factorisation_irred: "!! c::'a::factorial. + [| Factorisation x factors u; a : set factors |] ==> irred a" + unfolding Factorisation_def by blast + end diff -r 25ed0a4c7dc5 -r 6cdd0589aa73 src/HOL/Algebra/abstract/Ideal2.ML --- a/src/HOL/Algebra/abstract/Ideal2.ML Sun Nov 19 13:02:55 2006 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,328 +0,0 @@ -(* - Ideals for commutative rings - $Id$ - Author: Clemens Ballarin, started 24 September 1999 -*) - -(* is_ideal *) - -Goalw [thm "is_ideal_def"] - "!! I. [| !! a b. [| a:I; b:I |] ==> a + b : I; \ -\ !! a. a:I ==> - a : I; 0 : I; \ -\ !! a r. a:I ==> a * r : I |] ==> is_ideal I"; -by Auto_tac; -qed "is_idealI"; - -Goalw [thm "is_ideal_def"] "[| is_ideal I; a:I; b:I |] ==> a + b : I"; -by (Fast_tac 1); -qed "is_ideal_add"; - -Goalw [thm "is_ideal_def"] "[| is_ideal I; a:I |] ==> - a : I"; -by (Fast_tac 1); -qed "is_ideal_uminus"; - -Goalw [thm "is_ideal_def"] "[| is_ideal I |] ==> 0 : I"; -by (Fast_tac 1); -qed "is_ideal_zero"; - -Goalw [thm "is_ideal_def"] "[| is_ideal I; a:I |] ==> a * r : I"; -by (Fast_tac 1); -qed "is_ideal_mult"; - -Goalw [dvd_def, thm "is_ideal_def"] "[| a dvd b; is_ideal I; a:I |] ==> b:I"; -by (Fast_tac 1); -qed "is_ideal_dvd"; - -Goalw [thm "is_ideal_def"] "is_ideal (UNIV::('a::ring) set)"; -by Auto_tac; -qed "UNIV_is_ideal"; - -Goalw [thm "is_ideal_def"] "is_ideal {0::'a::ring}"; -by Auto_tac; -qed "zero_is_ideal"; - -Addsimps [is_ideal_add, is_ideal_uminus, is_ideal_zero, is_ideal_mult, - UNIV_is_ideal, zero_is_ideal]; - -Goal "is_ideal {x::'a::ring. a dvd x}"; -by (rtac is_idealI 1); -by Auto_tac; -qed "is_ideal_1"; - -Goal "is_ideal {x::'a::ring. EX u v. x = a * u + b * v}"; -by (rtac is_idealI 1); -(* by Auto_tac; FIXME: makes Zumkeller's order fail (raises exn Domain) *) -by (Clarify_tac 1); -by (Clarify_tac 2); -by (Clarify_tac 3); -by (Clarify_tac 4); -by (res_inst_tac [("x", "u+ua")] exI 1); -by (res_inst_tac [("x", "v+va")] exI 1); -by (res_inst_tac [("x", "-u")] exI 2); -by (res_inst_tac [("x", "-v")] exI 2); -by (res_inst_tac [("x", "0")] exI 3); -by (res_inst_tac [("x", "0")] exI 3); -by (res_inst_tac [("x", "u * r")] exI 4); -by (res_inst_tac [("x", "v * r")] exI 4); -by (REPEAT (Simp_tac 1)); -qed "is_ideal_2"; - -(* ideal_of *) - -Goalw [thm "is_ideal_def", thm "ideal_of_def"] "is_ideal (ideal_of S)"; -by (Blast_tac 1); (* Here, blast_tac is much superior to fast_tac! *) -qed "ideal_of_is_ideal"; - -Goalw [thm "ideal_of_def"] "a:S ==> a : (ideal_of S)"; -by Auto_tac; -qed "generator_in_ideal"; - -Goalw [thm "ideal_of_def"] "ideal_of {1::'a::ring} = UNIV"; -by (force_tac (claset() addDs [is_ideal_mult], - simpset() addsimps [l_one] delsimprocs [ring_simproc]) 1); - (* FIXME: Zumkeller's order raises Domain exn *) -qed "ideal_of_one_eq"; - -Goalw [thm "ideal_of_def"] "ideal_of {} = {0::'a::ring}"; -by (rtac subset_antisym 1); -by (rtac subsetI 1); -by (dtac InterD 1); -by (assume_tac 2); -by (auto_tac (claset(), simpset() addsimps [is_ideal_zero])); -qed "ideal_of_empty_eq"; - -Goalw [thm "ideal_of_def"] "ideal_of {a} = {x::'a::ring. a dvd x}"; -by (rtac subset_antisym 1); -by (rtac subsetI 1); -by (dtac InterD 1); -by (assume_tac 2); -by (auto_tac (claset() addIs [is_ideal_1], simpset())); -by (asm_simp_tac (simpset() addsimps [is_ideal_dvd]) 1); -qed "pideal_structure"; - -Goalw [thm "ideal_of_def"] - "ideal_of {a, b} = {x::'a::ring. EX u v. x = a * u + b * v}"; -by (rtac subset_antisym 1); -by (rtac subsetI 1); -by (dtac InterD 1); -by (assume_tac 2); -by (auto_tac (claset() addIs [is_ideal_2], - simpset() delsimprocs [ring_simproc])); -(* FIXME: Zumkeller's order *) -by (res_inst_tac [("x", "1")] exI 1); -by (res_inst_tac [("x", "0")] exI 1); -by (res_inst_tac [("x", "0")] exI 2); -by (res_inst_tac [("x", "1")] exI 2); -by (Simp_tac 1); -by (Simp_tac 1); -qed "ideal_of_2_structure"; - -Goalw [thm "ideal_of_def"] "A <= B ==> ideal_of A <= ideal_of B"; -by Auto_tac; -qed "ideal_of_mono"; - -Goal "ideal_of {0::'a::ring} = {0}"; -by (simp_tac (simpset() addsimps [pideal_structure]) 1); -by (rtac subset_antisym 1); -by (auto_tac (claset() addIs [thm "dvd_zero_left"], simpset())); -qed "ideal_of_zero_eq"; - -Goal "[| is_ideal I; a : I |] ==> ideal_of {a::'a::ring} <= I"; -by (auto_tac (claset(), - simpset() addsimps [pideal_structure, is_ideal_dvd])); -qed "element_generates_subideal"; - -(* is_pideal *) - -Goalw [thm "is_pideal_def"] "is_pideal (I::('a::ring) set) ==> is_ideal I"; -by (fast_tac (claset() addIs [ideal_of_is_ideal]) 1); -qed "is_pideal_imp_is_ideal"; - -Goalw [thm "is_pideal_def"] "is_pideal (ideal_of {a::'a::ring})"; -by (Fast_tac 1); -qed "pideal_is_pideal"; - -Goalw [thm "is_pideal_def"] "is_pideal I ==> EX a. I = ideal_of {a}"; -by (assume_tac 1); -qed "is_pidealD"; - -(* Ideals and divisibility *) - -Goal "b dvd a ==> ideal_of {a::'a::ring} <= ideal_of {b}"; -by (auto_tac (claset() addIs [thm "dvd_trans_ring"], - simpset() addsimps [pideal_structure])); -qed "dvd_imp_subideal"; - -Goal "ideal_of {a::'a::ring} <= ideal_of {b} ==> b dvd a"; -by (auto_tac (claset() addSDs [subsetD], - simpset() addsimps [pideal_structure])); -qed "subideal_imp_dvd"; - -Goal "(ideal_of {a::'a::ring} <= ideal_of {b}) = (b dvd a)"; -by (rtac iffI 1); -by (REPEAT (ares_tac [subideal_imp_dvd, dvd_imp_subideal] 1)); -qed "subideal_is_dvd"; - -Goal "(ideal_of {a::'a::ring} < ideal_of {b}) ==> ~ a dvd b"; -by (full_simp_tac (simpset() addsimps [psubset_eq, pideal_structure]) 1); -by (etac conjE 1); -by (dres_inst_tac [("c", "a")] subsetD 1); -by (auto_tac (claset() addIs [thm "dvd_trans_ring"], - simpset())); -qed "psubideal_not_dvd"; - -Goal "[| b dvd a; ~ a dvd b |] ==> ideal_of {a::'a::ring} < ideal_of {b}"; -by (rtac psubsetI 1); -by (etac dvd_imp_subideal 1); -by (blast_tac (claset() addIs [dvd_imp_subideal, subideal_imp_dvd]) 1); -qed "not_dvd_psubideal_singleton"; - -Goal "(ideal_of {a::'a::ring} < ideal_of {b}) = (b dvd a & ~ a dvd b)"; -by (rtac iffI 1); -by (REPEAT (ares_tac - [conjI, psubideal_not_dvd, psubset_imp_subset RS subideal_imp_dvd] 1)); -by (etac conjE 1); -by (REPEAT (ares_tac [not_dvd_psubideal_singleton] 1)); -qed "psubideal_is_dvd"; - -Goal "[| a dvd b; b dvd a |] ==> ideal_of {a::'a::ring} = ideal_of {b}"; -by (rtac subset_antisym 1); -by (REPEAT (ares_tac [dvd_imp_subideal] 1)); -qed "assoc_pideal_eq"; - -AddIffs [subideal_is_dvd, psubideal_is_dvd]; - -Goal "!!a::'a::ring. a dvd b ==> b : (ideal_of {a})"; -by (rtac is_ideal_dvd 1); -by (assume_tac 1); -by (rtac ideal_of_is_ideal 1); -by (rtac generator_in_ideal 1); -by (Simp_tac 1); -qed "dvd_imp_in_pideal"; - -Goal "!!a::'a::ring. b : (ideal_of {a}) ==> a dvd b"; -by (full_simp_tac (simpset() addsimps [pideal_structure]) 1); -qed "in_pideal_imp_dvd"; - -Goal "~ (a dvd b) ==> ideal_of {a::'a::ring} < ideal_of {a, b}"; -by (asm_simp_tac (simpset() addsimps [psubset_eq, ideal_of_mono]) 1); -by (etac contrapos_pp 1); -by (full_simp_tac (simpset() addsimps [ideal_of_2_structure]) 1); -by (rtac in_pideal_imp_dvd 1); -by (Asm_simp_tac 1); -by (res_inst_tac [("x", "0")] exI 1); -by (res_inst_tac [("x", "1")] exI 1); -by (Simp_tac 1); -qed "not_dvd_psubideal"; - -Goalw [thm "irred_def"] - "[| irred (a::'a::ring); is_pideal I; ideal_of {a} < I |] ==> x : I"; -by (dtac is_pidealD 1); -by (etac exE 1); -by (Clarify_tac 1); -by (eres_inst_tac [("x", "aa")] allE 1); -by (Clarify_tac 1); -by (dres_inst_tac [("a", "1")] dvd_imp_subideal 1); -by (auto_tac (claset(), simpset() addsimps [ideal_of_one_eq])); -qed "irred_imp_max_ideal"; - -(* Pid are factorial *) - -(* Divisor chain condition *) -(* proofs not finished *) - -Goal "(ALL i. I i <= I (Suc i)) ==> (n <= m & a : I n --> a : I m)"; -by (induct_tac "m" 1); -by (Blast_tac 1); -(* induction step *) -by (rename_tac "m" 1); -by (case_tac "n <= m" 1); -by Auto_tac; -by (subgoal_tac "n = Suc m" 1); -by (arith_tac 2); -by (Force_tac 1); -qed_spec_mp "subset_chain_lemma"; - -Goal "[| ALL i. is_ideal (I i); ALL i. I i <= I (Suc i) |] \ -\ ==> is_ideal (Union (I`UNIV))"; -by (rtac is_idealI 1); -by Auto_tac; -by (res_inst_tac [("x", "max x xa")] exI 1); -by (rtac is_ideal_add 1); -by (Asm_simp_tac 1); -by (rtac subset_chain_lemma 1); -by (assume_tac 1); -by (rtac conjI 1); -by (assume_tac 2); -by (arith_tac 1); -by (rtac subset_chain_lemma 1); -by (assume_tac 1); -by (rtac conjI 1); -by (assume_tac 2); -by (arith_tac 1); -by (res_inst_tac [("x", "x")] exI 1); -by (Asm_simp_tac 1); -by (res_inst_tac [("x", "x")] exI 1); -by (Asm_simp_tac 1); -qed "chain_is_ideal"; - -(* -Goal "ALL i. ideal_of {a i} < ideal_of {a (Suc i)} ==> \ -\ EX n. Union ((ideal_of o (%a. {a}))`UNIV) = ideal_of {a n}"; - -Goal "wf {(a::'a::pid, b). a dvd b & ~ b dvd a}"; -by (simp_tac (simpset() - addsimps [psubideal_is_dvd RS sym, wf_iff_no_infinite_down_chain] - delsimps [psubideal_is_dvd]) 1); -*) - -(* Primeness condition *) - -Goalw [thm "prime_def"] "irred a ==> prime (a::'a::pid)"; -by (rtac conjI 1); -by (rtac conjI 2); -by (Clarify_tac 3); -by (dres_inst_tac [("I", "ideal_of {a, b}"), ("x", "1")] - irred_imp_max_ideal 3); -by (auto_tac (claset() addIs [ideal_of_is_ideal, thm "pid_ax"], - simpset() addsimps [thm "irred_def", not_dvd_psubideal, thm "pid_ax"])); -by (full_simp_tac (simpset() addsimps [ideal_of_2_structure]) 1); -by (Clarify_tac 1); -by (dres_inst_tac [("f", "op* aa")] arg_cong 1); -by (full_simp_tac (simpset() addsimps [r_distr]) 1); -by (etac subst 1); -by (asm_simp_tac (simpset() addsimps [m_assoc RS sym] - delsimprocs [ring_simproc]) 1); -qed "pid_irred_imp_prime"; - -(* Fields are Pid *) - -Goal "a ~= 0 ==> ideal_of {a::'a::field} = UNIV"; -by (rtac subset_antisym 1); -by (Simp_tac 1); -by (rtac subset_trans 1); -by (rtac dvd_imp_subideal 2); -by (rtac (thm "field_ax") 2); -by (assume_tac 2); -by (simp_tac (simpset() addsimps [ideal_of_one_eq]) 1); -qed "field_pideal_univ"; - -Goal "[| is_ideal I; I ~= {0} |] ==> {0} < I"; -by (asm_simp_tac (simpset() addsimps [psubset_eq, not_sym, is_ideal_zero]) 1); -qed "proper_ideal"; - -Goalw [thm "is_pideal_def"] "is_ideal (I::('a::field) set) ==> is_pideal I"; -by (case_tac "I = {0}" 1); -by (res_inst_tac [("x", "0")] exI 1); -by (asm_simp_tac (simpset() addsimps [ideal_of_zero_eq]) 1); -(* case "I ~= {0}" *) -by (ftac proper_ideal 1); -by (assume_tac 1); -by (dtac psubset_imp_ex_mem 1); -by (etac exE 1); -by (res_inst_tac [("x", "b")] exI 1); -by (cut_inst_tac [("a", "b")] element_generates_subideal 1); - by (assume_tac 1); by (Blast_tac 1); -by (auto_tac (claset(), simpset() addsimps [field_pideal_univ])); -qed "field_pid"; - diff -r 25ed0a4c7dc5 -r 6cdd0589aa73 src/HOL/Algebra/abstract/Ideal2.thy --- a/src/HOL/Algebra/abstract/Ideal2.thy Sun Nov 19 13:02:55 2006 +0100 +++ b/src/HOL/Algebra/abstract/Ideal2.thy Sun Nov 19 23:48:55 2006 +0100 @@ -6,21 +6,318 @@ theory Ideal2 imports Ring2 begin -consts - ideal_of :: "('a::ring) set => 'a set" - is_ideal :: "('a::ring) set => bool" - is_pideal :: "('a::ring) set => bool" +definition + is_ideal :: "('a::ring) set => bool" where + "is_ideal I \ (ALL a: I. ALL b: I. a + b : I) & + (ALL a: I. - a : I) & 0 : I & + (ALL a: I. ALL r. a * r : I)" -defs - is_ideal_def: "is_ideal I == (ALL a: I. ALL b: I. a + b : I) & - (ALL a: I. - a : I) & 0 : I & - (ALL a: I. ALL r. a * r : I)" - ideal_of_def: "ideal_of S == Inter {I. is_ideal I & S <= I}" - is_pideal_def: "is_pideal I == (EX a. I = ideal_of {a})" +definition + ideal_of :: "('a::ring) set => 'a set" where + "ideal_of S = Inter {I. is_ideal I & S <= I}" + +definition + is_pideal :: "('a::ring) set => bool" where + "is_pideal I \ (EX a. I = ideal_of {a})" + text {* Principle ideal domains *} axclass pid < "domain" pid_ax: "is_ideal I ==> is_pideal I" + +(* is_ideal *) + +lemma is_idealI: + "!! I. [| !! a b. [| a:I; b:I |] ==> a + b : I; + !! a. a:I ==> - a : I; 0 : I; + !! a r. a:I ==> a * r : I |] ==> is_ideal I" + unfolding is_ideal_def by blast + +lemma is_ideal_add [simp]: "[| is_ideal I; a:I; b:I |] ==> a + b : I" + unfolding is_ideal_def by blast + +lemma is_ideal_uminus [simp]: "[| is_ideal I; a:I |] ==> - a : I" + unfolding is_ideal_def by blast + +lemma is_ideal_zero [simp]: "[| is_ideal I |] ==> 0 : I" + unfolding is_ideal_def by blast + +lemma is_ideal_mult [simp]: "[| is_ideal I; a:I |] ==> a * r : I" + unfolding is_ideal_def by blast + +lemma is_ideal_dvd: "[| a dvd b; is_ideal I; a:I |] ==> b:I" + unfolding is_ideal_def dvd_def by blast + +lemma UNIV_is_ideal [simp]: "is_ideal (UNIV::('a::ring) set)" + unfolding is_ideal_def by blast + +lemma zero_is_ideal [simp]: "is_ideal {0::'a::ring}" + unfolding is_ideal_def by auto + +lemma is_ideal_1: "is_ideal {x::'a::ring. a dvd x}" + apply (rule is_idealI) + apply auto + done + +lemma is_ideal_2: "is_ideal {x::'a::ring. EX u v. x = a * u + b * v}" + apply (rule is_idealI) + apply auto + apply (rule_tac x = "u+ua" in exI) + apply (rule_tac x = "v+va" in exI) + apply (rule_tac [2] x = "-u" in exI) + apply (rule_tac [2] x = "-v" in exI) + apply (rule_tac [3] x = "0" in exI) + apply (rule_tac [3] x = "0" in exI) + apply (rule_tac [4] x = "u * r" in exI) + apply (rule_tac [4] x = "v * r" in exI) + apply simp_all + done + + +(* ideal_of *) + +lemma ideal_of_is_ideal: "is_ideal (ideal_of S)" + unfolding is_ideal_def ideal_of_def by blast + +lemma generator_in_ideal: "a:S ==> a : (ideal_of S)" + unfolding ideal_of_def by blast + +lemma ideal_of_one_eq: "ideal_of {1::'a::ring} = UNIV" + apply (unfold ideal_of_def) + apply (force dest: is_ideal_mult simp add: l_one) + done + +lemma ideal_of_empty_eq: "ideal_of {} = {0::'a::ring}" + apply (unfold ideal_of_def) + apply (rule subset_antisym) + apply (rule subsetI) + apply (drule InterD) + prefer 2 apply assumption + apply (auto simp add: is_ideal_zero) + done + +lemma pideal_structure: "ideal_of {a} = {x::'a::ring. a dvd x}" + apply (unfold ideal_of_def) + apply (rule subset_antisym) + apply (rule subsetI) + apply (drule InterD) + prefer 2 apply assumption + apply (auto intro: is_ideal_1) + apply (simp add: is_ideal_dvd) + done + +lemma ideal_of_2_structure: + "ideal_of {a, b} = {x::'a::ring. EX u v. x = a * u + b * v}" + apply (unfold ideal_of_def) + apply (rule subset_antisym) + apply (rule subsetI) + apply (drule InterD) + prefer 2 apply assumption + apply (tactic {* auto_tac (claset() addIs [thm "is_ideal_2"], + simpset() delsimprocs [ring_simproc]) *}) + apply (rule_tac x = "1" in exI) + apply (rule_tac x = "0" in exI) + apply (rule_tac [2] x = "0" in exI) + apply (rule_tac [2] x = "1" in exI) + apply simp + apply simp + done + +lemma ideal_of_mono: "A <= B ==> ideal_of A <= ideal_of B" + unfolding ideal_of_def by blast + +lemma ideal_of_zero_eq: "ideal_of {0::'a::ring} = {0}" + apply (simp add: pideal_structure) + apply (rule subset_antisym) + apply (auto intro: "dvd_zero_left") + done + +lemma element_generates_subideal: "[| is_ideal I; a : I |] ==> ideal_of {a::'a::ring} <= I" + apply (auto simp add: pideal_structure is_ideal_dvd) + done + + +(* is_pideal *) + +lemma is_pideal_imp_is_ideal: "is_pideal (I::('a::ring) set) ==> is_ideal I" + unfolding is_pideal_def by (fast intro: ideal_of_is_ideal) + +lemma pideal_is_pideal: "is_pideal (ideal_of {a::'a::ring})" + unfolding is_pideal_def by blast + +lemma is_pidealD: "is_pideal I ==> EX a. I = ideal_of {a}" + unfolding is_pideal_def . + + +(* Ideals and divisibility *) + +lemma dvd_imp_subideal: "b dvd a ==> ideal_of {a::'a::ring} <= ideal_of {b}" + by (auto intro: dvd_trans_ring simp add: pideal_structure) + +lemma subideal_imp_dvd: "ideal_of {a::'a::ring} <= ideal_of {b} ==> b dvd a" + by (auto dest!: subsetD simp add: pideal_structure) + +lemma psubideal_not_dvd: "(ideal_of {a::'a::ring} < ideal_of {b}) ==> ~ a dvd b" + apply (simp add: psubset_eq pideal_structure) + apply (erule conjE) + apply (drule_tac c = "a" in subsetD) + apply (auto intro: dvd_trans_ring) + done + +lemma not_dvd_psubideal_singleton: + "[| b dvd a; ~ a dvd b |] ==> ideal_of {a::'a::ring} < ideal_of {b}" + apply (rule psubsetI) + apply (erule dvd_imp_subideal) + apply (blast intro: dvd_imp_subideal subideal_imp_dvd) + done + +lemma subideal_is_dvd [iff]: "(ideal_of {a::'a::ring} <= ideal_of {b}) = (b dvd a)" + apply (rule iffI) + apply (assumption | rule subideal_imp_dvd dvd_imp_subideal)+ + done + +lemma psubideal_is_dvd [iff]: "(ideal_of {a::'a::ring} < ideal_of {b}) = (b dvd a & ~ a dvd b)" + apply (rule iffI) + apply (assumption | rule conjI psubideal_not_dvd psubset_imp_subset [THEN subideal_imp_dvd])+ + apply (erule conjE) + apply (assumption | rule not_dvd_psubideal_singleton)+ + done + +lemma assoc_pideal_eq: "[| a dvd b; b dvd a |] ==> ideal_of {a::'a::ring} = ideal_of {b}" + apply (rule subset_antisym) + apply (assumption | rule dvd_imp_subideal)+ + done + +lemma dvd_imp_in_pideal: "!!a::'a::ring. a dvd b ==> b : (ideal_of {a})" + apply (rule is_ideal_dvd) + apply assumption + apply (rule ideal_of_is_ideal) + apply (rule generator_in_ideal) + apply simp + done + +lemma in_pideal_imp_dvd: "!!a::'a::ring. b : (ideal_of {a}) ==> a dvd b" + by (simp add: pideal_structure) + +lemma not_dvd_psubideal: "~ (a dvd b) ==> ideal_of {a::'a::ring} < ideal_of {a, b}" + apply (simp add: psubset_eq ideal_of_mono) + apply (erule contrapos_pp) + apply (simp add: ideal_of_2_structure) + apply (rule in_pideal_imp_dvd) + apply simp + apply (rule_tac x = "0" in exI) + apply (rule_tac x = "1" in exI) + apply simp + done + +lemma irred_imp_max_ideal: + "[| irred (a::'a::ring); is_pideal I; ideal_of {a} < I |] ==> x : I" + apply (unfold irred_def) + apply (drule is_pidealD) + apply (erule exE) + apply clarify + apply (erule_tac x = "aa" in allE) + apply clarify + apply (drule_tac a = "1" in dvd_imp_subideal) + apply (auto simp add: ideal_of_one_eq) + done + +(* Pid are factorial *) + +(* Divisor chain condition *) +(* proofs not finished *) + +lemma subset_chain_lemma [rule_format (no_asm)]: + "(ALL i. I i <= I (Suc i)) ==> (n <= m & a : I n --> a : I m)" + apply (induct_tac m) + apply blast + (* induction step *) + apply (rename_tac m) + apply (case_tac "n <= m") + apply auto + apply (subgoal_tac "n = Suc m") + prefer 2 + apply arith + apply force + done + +lemma chain_is_ideal: "[| ALL i. is_ideal (I i); ALL i. I i <= I (Suc i) |] + ==> is_ideal (Union (I`UNIV))" + apply (rule is_idealI) + apply auto + apply (rule_tac x = "max x xa" in exI) + apply (rule is_ideal_add) + apply simp + apply (rule subset_chain_lemma) + apply assumption + apply (rule conjI) + prefer 2 + apply assumption + apply arith + apply (rule subset_chain_lemma) + apply assumption + apply (rule conjI) + prefer 2 + apply assumption + apply arith + apply (rule_tac x = "x" in exI) + apply simp + apply (rule_tac x = "x" in exI) + apply simp + done + + +(* Primeness condition *) + +lemma pid_irred_imp_prime: "irred a ==> prime (a::'a::pid)" + apply (unfold prime_def) + apply (rule conjI) + apply (rule_tac [2] conjI) + apply (tactic "Clarify_tac 3") + apply (drule_tac [3] I = "ideal_of {a, b}" and x = "1" in irred_imp_max_ideal) + apply (auto intro: ideal_of_is_ideal pid_ax simp add: irred_def not_dvd_psubideal pid_ax) + apply (simp add: ideal_of_2_structure) + apply clarify + apply (drule_tac f = "op* aa" in arg_cong) + apply (simp add: r_distr) + apply (erule subst) + apply (tactic {* asm_simp_tac (simpset() addsimps [thm "m_assoc" RS sym] + delsimprocs [ring_simproc]) 1 *}) + done + +(* Fields are Pid *) + +lemma field_pideal_univ: "a ~= 0 ==> ideal_of {a::'a::field} = UNIV" + apply (rule subset_antisym) + apply simp + apply (rule subset_trans) + prefer 2 + apply (rule dvd_imp_subideal) + apply (rule field_ax) + apply assumption + apply (simp add: ideal_of_one_eq) + done + +lemma proper_ideal: "[| is_ideal I; I ~= {0} |] ==> {0} < I" + by (simp add: psubset_eq not_sym is_ideal_zero) + +lemma field_pid: "is_ideal (I::('a::field) set) ==> is_pideal I" + apply (unfold is_pideal_def) + apply (case_tac "I = {0}") + apply (rule_tac x = "0" in exI) + apply (simp add: ideal_of_zero_eq) + (* case "I ~= {0}" *) + apply (frule proper_ideal) + apply assumption + apply (drule psubset_imp_ex_mem) + apply (erule exE) + apply (rule_tac x = b in exI) + apply (cut_tac a = b in element_generates_subideal) + apply assumption + apply blast + apply (auto simp add: field_pideal_univ) + done + end diff -r 25ed0a4c7dc5 -r 6cdd0589aa73 src/HOL/Algebra/abstract/Ring2.ML --- a/src/HOL/Algebra/abstract/Ring2.ML Sun Nov 19 13:02:55 2006 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,350 +0,0 @@ -(* - Abstract class ring (commutative, with 1) - $Id$ - Author: Clemens Ballarin, started 9 December 1996 -*) - -(* -val a_assoc = thm "semigroup_add.add_assoc"; -val l_zero = thm "comm_monoid_add.add_0"; -val a_comm = thm "ab_semigroup_add.add_commute"; - -section "Rings"; - -fun make_left_commute assoc commute s = - [rtac (commute RS trans) 1, rtac (assoc RS trans) 1, - rtac (commute RS arg_cong) 1]; - -(* addition *) - -qed_goal "a_lcomm" Ring2.thy "!!a::'a::ring. a+(b+c) = b+(a+c)" - (make_left_commute a_assoc a_comm); - -val a_ac = [a_assoc, a_comm, a_lcomm]; - -Goal "!!a::'a::ring. a + 0 = a"; -by (rtac (a_comm RS trans) 1); -by (rtac l_zero 1); -qed "r_zero"; - -Goal "!!a::'a::ring. a + (-a) = 0"; -by (rtac (a_comm RS trans) 1); -by (rtac l_neg 1); -qed "r_neg"; - -Goal "!! a::'a::ring. a + b = a + c ==> b = c"; -by (rtac box_equals 1); -by (rtac l_zero 2); -by (rtac l_zero 2); -by (res_inst_tac [("a1", "a")] (l_neg RS subst) 1); -by (asm_simp_tac (simpset() addsimps [a_assoc]) 1); -qed "a_lcancel"; - -Goal "!! a::'a::ring. b + a = c + a ==> b = c"; -by (rtac a_lcancel 1); -by (asm_simp_tac (simpset() addsimps a_ac) 1); -qed "a_rcancel"; - -Goal "!! a::'a::ring. (a + b = a + c) = (b = c)"; -by (auto_tac (claset() addSDs [a_lcancel], simpset())); -qed "a_lcancel_eq"; - -Goal "!! a::'a::ring. (b + a = c + a) = (b = c)"; -by (simp_tac (simpset() addsimps [a_lcancel_eq, a_comm]) 1); -qed "a_rcancel_eq"; - -Addsimps [a_lcancel_eq, a_rcancel_eq]; - -Goal "!!a::'a::ring. -(-a) = a"; -by (rtac a_lcancel 1); -by (rtac (r_neg RS trans) 1); -by (rtac (l_neg RS sym) 1); -qed "minus_minus"; - -Goal "- 0 = (0::'a::ring)"; -by (rtac a_lcancel 1); -by (rtac (r_neg RS trans) 1); -by (rtac (l_zero RS sym) 1); -qed "minus0"; - -Goal "!!a::'a::ring. -(a + b) = (-a) + (-b)"; -by (res_inst_tac [("a", "a+b")] a_lcancel 1); -by (simp_tac (simpset() addsimps ([r_neg, l_neg, l_zero]@a_ac)) 1); -qed "minus_add"; - -(* multiplication *) - -qed_goal "m_lcomm" Ring2.thy "!!a::'a::ring. a*(b*c) = b*(a*c)" - (make_left_commute m_assoc m_comm); - -val m_ac = [m_assoc, m_comm, m_lcomm]; - -Goal "!!a::'a::ring. a * 1 = a"; -by (rtac (m_comm RS trans) 1); -by (rtac l_one 1); -qed "r_one"; - -(* distributive and derived *) - -Goal "!!a::'a::ring. a * (b + c) = a * b + a * c"; -by (rtac (m_comm RS trans) 1); -by (rtac (l_distr RS trans) 1); -by (simp_tac (simpset() addsimps [m_comm]) 1); -qed "r_distr"; - -val m_distr = m_ac @ [l_distr, r_distr]; - -(* the following two proofs can be found in - Jacobson, Basic Algebra I, pp. 88-89 *) - -Goal "!!a::'a::ring. 0 * a = 0"; -by (rtac a_lcancel 1); -by (rtac (l_distr RS sym RS trans) 1); -by (simp_tac (simpset() addsimps [r_zero]) 1); -qed "l_null"; - -Goal "!!a::'a::ring. a * 0 = 0"; -by (rtac (m_comm RS trans) 1); -by (rtac l_null 1); -qed "r_null"; - -Goal "!!a::'a::ring. (-a) * b = - (a * b)"; -by (rtac a_lcancel 1); -by (rtac (r_neg RS sym RSN (2, trans)) 1); -by (rtac (l_distr RS sym RS trans) 1); -by (simp_tac (simpset() addsimps [l_null, r_neg]) 1); -qed "l_minus"; - -Goal "!!a::'a::ring. a * (-b) = - (a * b)"; -by (rtac a_lcancel 1); -by (rtac (r_neg RS sym RSN (2, trans)) 1); -by (rtac (r_distr RS sym RS trans) 1); -by (simp_tac (simpset() addsimps [r_null, r_neg]) 1); -qed "r_minus"; - -val m_minus = [l_minus, r_minus]; - -Addsimps [l_zero, r_zero, l_neg, r_neg, minus_minus, minus0, - l_one, r_one, l_null, r_null]; - -(* further rules *) - -Goal "!!a::'a::ring. -a = 0 ==> a = 0"; -by (res_inst_tac [("t", "a")] (minus_minus RS subst) 1); -by (Asm_simp_tac 1); -qed "uminus_monom"; - -Goal "!!a::'a::ring. a ~= 0 ==> -a ~= 0"; -by (blast_tac (claset() addIs [uminus_monom]) 1); -qed "uminus_monom_neq"; - -Goal "!!a::'a::ring. a * b ~= 0 ==> a ~= 0"; -by Auto_tac; -qed "l_nullD"; - -Goal "!!a::'a::ring. a * b ~= 0 ==> b ~= 0"; -by Auto_tac; -qed "r_nullD"; - -(* reflection between a = b and a -- b = 0 *) - -Goal "!!a::'a::ring. a = b ==> a + (-b) = 0"; -by (Asm_simp_tac 1); -qed "eq_imp_diff_zero"; - -Goal "!!a::'a::ring. a + (-b) = 0 ==> a = b"; -by (res_inst_tac [("a", "-b")] a_rcancel 1); -by (Asm_simp_tac 1); -qed "diff_zero_imp_eq"; - -(* this could be a rewrite rule, but won't terminate - ==> make it a simproc? -Goal "!!a::'a::ring. (a = b) = (a -- b = 0)"; -*) - -*) - -val dvd_def = thm "dvd_def'"; - -Goalw [dvd_def] - "!!a::'a::ring. [| a dvd 1; b dvd 1 |] ==> a * b dvd 1"; -by (Clarify_tac 1); -by (res_inst_tac [("x", "k * ka")] exI 1); -by (Asm_full_simp_tac 1); -qed "unit_mult"; - -Goal "!!a::'a::ring. a dvd 1 ==> a^n dvd 1"; -by (induct_tac "n" 1); -by (Simp_tac 1); -by (asm_simp_tac (simpset() addsimps [unit_mult]) 1); -qed "unit_power"; - -Goalw [dvd_def] - "!! a::'a::ring. [| a dvd b; a dvd c |] ==> a dvd b + c"; -by (Clarify_tac 1); -by (res_inst_tac [("x", "k + ka")] exI 1); -by (simp_tac (simpset() addsimps [r_distr]) 1); -qed "dvd_add_right"; - -Goalw [dvd_def] - "!! a::'a::ring. a dvd b ==> a dvd -b"; -by (Clarify_tac 1); -by (res_inst_tac [("x", "-k")] exI 1); -by (simp_tac (simpset() addsimps [r_minus]) 1); -qed "dvd_uminus_right"; - -Goalw [dvd_def] - "!! a::'a::ring. a dvd b ==> a dvd c*b"; -by (Clarify_tac 1); -by (res_inst_tac [("x", "c * k")] exI 1); -by (Simp_tac 1); -qed "dvd_l_mult_right"; - -Goalw [dvd_def] - "!! a::'a::ring. a dvd b ==> a dvd b*c"; -by (Clarify_tac 1); -by (res_inst_tac [("x", "k * c")] exI 1); -by (Simp_tac 1); -qed "dvd_r_mult_right"; - -Addsimps [dvd_add_right, dvd_uminus_right, dvd_l_mult_right, dvd_r_mult_right]; - -(* Inverse of multiplication *) - -section "inverse"; - -Goal "!! a::'a::ring. [| a * x = 1; a * y = 1 |] ==> x = y"; -by (res_inst_tac [("a", "(a*y)*x"), ("b", "y*(a*x)")] box_equals 1); -by (Simp_tac 1); -by Auto_tac; -qed "inverse_unique"; - -Goal "!! a::'a::ring. a dvd 1 ==> a * inverse a = 1"; -by (asm_full_simp_tac (simpset () addsimps [inverse_def, dvd_def] - delsimprocs [ring_simproc]) 1); -by (Clarify_tac 1); -by (rtac theI 1); -by (atac 1); -by (rtac inverse_unique 1); -by (atac 1); -by (atac 1); -qed "r_inverse_ring"; - -Goal "!! a::'a::ring. a dvd 1 ==> inverse a * a= 1"; -by (asm_simp_tac (simpset() addsimps [r_inverse_ring]) 1); -qed "l_inverse_ring"; - -(* Integral domain *) - -(* -section "Integral domains"; - -Goal "0 ~= (1::'a::domain)"; -by (rtac not_sym 1); -by (rtac one_not_zero 1); -qed "zero_not_one"; - -Goal "!! a::'a::domain. a dvd 1 ==> a ~= 0"; -by (auto_tac (claset() addDs [dvd_zero_left], - simpset() addsimps [one_not_zero] )); -qed "unit_imp_nonzero"; - -Goal "[| a * b = 0; a ~= 0 |] ==> (b::'a::domain) = 0"; -by (dtac integral 1); -by (Fast_tac 1); -qed "r_integral"; - -Goal "[| a * b = 0; b ~= 0 |] ==> (a::'a::domain) = 0"; -by (dtac integral 1); -by (Fast_tac 1); -qed "l_integral"; - -Goal "!! a::'a::domain. [| a ~= 0; b ~= 0 |] ==> a * b ~= 0"; -by (blast_tac (claset() addIs [l_integral]) 1); -qed "not_integral"; - -Addsimps [not_integral, one_not_zero, zero_not_one]; - -Goal "!! a::'a::domain. [| a * x = x; x ~= 0 |] ==> a = 1"; -by (res_inst_tac [("a", "- 1")] a_lcancel 1); -by (Simp_tac 1); -by (rtac l_integral 1); -by (assume_tac 2); -by (asm_simp_tac (simpset() addsimps [l_distr, l_minus]) 1); -qed "l_one_integral"; - -Goal "!! a::'a::domain. [| x * a = x; x ~= 0 |] ==> a = 1"; -by (res_inst_tac [("a", "- 1")] a_rcancel 1); -by (Simp_tac 1); -by (rtac r_integral 1); -by (assume_tac 2); -by (asm_simp_tac (simpset() addsimps [r_distr, r_minus]) 1); -qed "r_one_integral"; - -(* cancellation laws for multiplication *) - -Goal "!! a::'a::domain. [| a ~= 0; a * b = a * c |] ==> b = c"; -by (rtac diff_zero_imp_eq 1); -by (dtac eq_imp_diff_zero 1); -by (full_simp_tac (simpset() addsimps [r_minus RS sym, r_distr RS sym]) 1); -by (fast_tac (claset() addIs [l_integral]) 1); -qed "m_lcancel"; - -Goal "!! a::'a::domain. [| a ~= 0; b * a = c * a |] ==> b = c"; -by (rtac m_lcancel 1); -by (assume_tac 1); -by (Asm_full_simp_tac 1); -qed "m_rcancel"; - -Goal "!! a::'a::domain. a ~= 0 ==> (a * b = a * c) = (b = c)"; -by (auto_tac (claset() addDs [m_lcancel], simpset())); -qed "m_lcancel_eq"; - -Goal "!! a::'a::domain. a ~= 0 ==> (b * a = c * a) = (b = c)"; -by (asm_simp_tac (simpset() addsimps [m_lcancel_eq, m_comm]) 1); -qed "m_rcancel_eq"; - -Addsimps [m_lcancel_eq, m_rcancel_eq]; -*) - -(* Fields *) - -section "Fields"; - -Goal "!! a::'a::field. (a dvd 1) = (a ~= 0)"; -by (auto_tac (claset() addDs [thm "field_ax", thm "dvd_zero_left"], - simpset() addsimps [thm "field_one_not_zero"])); -qed "field_unit"; - -(* required for instantiation of field < domain in file Field.thy *) - -Addsimps [field_unit]; - -val field_one_not_zero = thm "field_one_not_zero"; - -Goal "!! a::'a::field. a ~= 0 ==> a * inverse a = 1"; -by (asm_full_simp_tac (simpset() addsimps [r_inverse_ring]) 1); -qed "r_inverse"; - -Goal "!! a::'a::field. a ~= 0 ==> inverse a * a= 1"; -by (asm_full_simp_tac (simpset() addsimps [l_inverse_ring]) 1); -qed "l_inverse"; - -Addsimps [l_inverse, r_inverse]; - -(* fields are integral domains *) - -Goal "!! a::'a::field. a * b = 0 ==> a = 0 | b = 0"; -by (Step_tac 1); -by (res_inst_tac [("a", "(a*b)*inverse b")] box_equals 1); -by (rtac refl 3); -by (Simp_tac 2); -by Auto_tac; -qed "field_integral"; - -(* fields are factorial domains *) - -Goalw [thm "prime_def", thm "irred_def"] - "!! a::'a::field. irred a ==> prime a"; -by (blast_tac (claset() addIs [thm "field_ax"]) 1); -qed "field_fact_prime"; diff -r 25ed0a4c7dc5 -r 6cdd0589aa73 src/HOL/Algebra/abstract/Ring2.thy --- a/src/HOL/Algebra/abstract/Ring2.thy Sun Nov 19 13:02:55 2006 +0100 +++ b/src/HOL/Algebra/abstract/Ring2.thy Sun Nov 19 23:48:55 2006 +0100 @@ -8,7 +8,7 @@ header {* The algebraic hierarchy of rings as axiomatic classes *} theory Ring2 imports Main -uses ("order.ML") begin +begin section {* Constants *} @@ -102,16 +102,142 @@ prove about fields is that they are domains. *) field_ax: "a ~= 0 ==> a dvd 1" + section {* Basic facts *} subsection {* Normaliser for rings *} -use "order.ML" +(* derived rewrite rules *) + +lemma a_lcomm: "(a::'a::ring)+(b+c) = b+(a+c)" + apply (rule a_comm [THEN trans]) + apply (rule a_assoc [THEN trans]) + apply (rule a_comm [THEN arg_cong]) + done + +lemma r_zero: "(a::'a::ring) + 0 = a" + apply (rule a_comm [THEN trans]) + apply (rule l_zero) + done + +lemma r_neg: "(a::'a::ring) + (-a) = 0" + apply (rule a_comm [THEN trans]) + apply (rule l_neg) + done + +lemma r_neg2: "(a::'a::ring) + (-a + b) = b" + apply (rule a_assoc [symmetric, THEN trans]) + apply (simp add: r_neg l_zero) + done + +lemma r_neg1: "-(a::'a::ring) + (a + b) = b" + apply (rule a_assoc [symmetric, THEN trans]) + apply (simp add: l_neg l_zero) + done + + +(* auxiliary *) + +lemma a_lcancel: "!! a::'a::ring. a + b = a + c ==> b = c" + apply (rule box_equals) + prefer 2 + apply (rule l_zero) + prefer 2 + apply (rule l_zero) + apply (rule_tac a1 = a in l_neg [THEN subst]) + apply (simp add: a_assoc) + done + +lemma minus_add: "-((a::'a::ring) + b) = (-a) + (-b)" + apply (rule_tac a = "a + b" in a_lcancel) + apply (simp add: r_neg l_neg l_zero a_assoc a_comm a_lcomm) + done + +lemma minus_minus: "-(-(a::'a::ring)) = a" + apply (rule a_lcancel) + apply (rule r_neg [THEN trans]) + apply (rule l_neg [symmetric]) + done + +lemma minus0: "- 0 = (0::'a::ring)" + apply (rule a_lcancel) + apply (rule r_neg [THEN trans]) + apply (rule l_zero [symmetric]) + done + + +(* derived rules for multiplication *) + +lemma m_lcomm: "(a::'a::ring)*(b*c) = b*(a*c)" + apply (rule m_comm [THEN trans]) + apply (rule m_assoc [THEN trans]) + apply (rule m_comm [THEN arg_cong]) + done + +lemma r_one: "(a::'a::ring) * 1 = a" + apply (rule m_comm [THEN trans]) + apply (rule l_one) + done + +lemma r_distr: "(a::'a::ring) * (b + c) = a * b + a * c" + apply (rule m_comm [THEN trans]) + apply (rule l_distr [THEN trans]) + apply (simp add: m_comm) + done + + +(* the following proof is from Jacobson, Basic Algebra I, pp. 88-89 *) +lemma l_null: "0 * (a::'a::ring) = 0" + apply (rule a_lcancel) + apply (rule l_distr [symmetric, THEN trans]) + apply (simp add: r_zero) + done + +lemma r_null: "(a::'a::ring) * 0 = 0" + apply (rule m_comm [THEN trans]) + apply (rule l_null) + done + +lemma l_minus: "(-(a::'a::ring)) * b = - (a * b)" + apply (rule a_lcancel) + apply (rule r_neg [symmetric, THEN [2] trans]) + apply (rule l_distr [symmetric, THEN trans]) + apply (simp add: l_null r_neg) + done + +lemma r_minus: "(a::'a::ring) * (-b) = - (a * b)" + apply (rule a_lcancel) + apply (rule r_neg [symmetric, THEN [2] trans]) + apply (rule r_distr [symmetric, THEN trans]) + apply (simp add: r_null r_neg) + done + +(*** Term order for commutative rings ***) + +ML {* +fun ring_ord (Const (a, _)) = + find_index (fn a' => a = a') + ["HOL.zero", "HOL.plus", "HOL.uminus", "HOL.minus", "HOL.one", "HOL.times"] + | ring_ord _ = ~1; + +fun termless_ring (a, b) = (Term.term_lpo ring_ord (a, b) = LESS); + +val ring_ss = HOL_basic_ss settermless termless_ring addsimps + [thm "a_assoc", thm "l_zero", thm "l_neg", thm "a_comm", thm "m_assoc", + thm "l_one", thm "l_distr", thm "m_comm", thm "minus_def", + thm "r_zero", thm "r_neg", thm "r_neg2", thm "r_neg1", thm "minus_add", + thm "minus_minus", thm "minus0", thm "a_lcomm", thm "m_lcomm", (*thm "r_one",*) + thm "r_distr", thm "l_null", thm "r_null", thm "l_minus", thm "r_minus"]; +*} (* Note: r_one is not necessary in ring_ss *) method_setup ring = {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (full_simp_tac ring_ss)) *} {* computes distributive normal form in rings *} +lemmas ring_simps = + l_zero r_zero l_neg r_neg minus_minus minus0 + l_one r_one l_null r_null l_minus r_minus + subsection {* Rings and the summation operator *} @@ -278,7 +404,108 @@ then show ?thesis using dvd_def by blast qed -lemma dvd_def': - "m dvd n \ \k. n = m * k" unfolding dvd_def by simp + +lemma unit_mult: + "!!a::'a::ring. [| a dvd 1; b dvd 1 |] ==> a * b dvd 1" + apply (unfold dvd_def) + apply clarify + apply (rule_tac x = "k * ka" in exI) + apply simp + done + +lemma unit_power: "!!a::'a::ring. a dvd 1 ==> a^n dvd 1" + apply (induct_tac n) + apply simp + apply (simp add: unit_mult) + done + +lemma dvd_add_right [simp]: + "!! a::'a::ring. [| a dvd b; a dvd c |] ==> a dvd b + c" + apply (unfold dvd_def) + apply clarify + apply (rule_tac x = "k + ka" in exI) + apply (simp add: r_distr) + done + +lemma dvd_uminus_right [simp]: + "!! a::'a::ring. a dvd b ==> a dvd -b" + apply (unfold dvd_def) + apply clarify + apply (rule_tac x = "-k" in exI) + apply (simp add: r_minus) + done + +lemma dvd_l_mult_right [simp]: + "!! a::'a::ring. a dvd b ==> a dvd c*b" + apply (unfold dvd_def) + apply clarify + apply (rule_tac x = "c * k" in exI) + apply simp + done + +lemma dvd_r_mult_right [simp]: + "!! a::'a::ring. a dvd b ==> a dvd b*c" + apply (unfold dvd_def) + apply clarify + apply (rule_tac x = "k * c" in exI) + apply simp + done + + +(* Inverse of multiplication *) + +section "inverse" + +lemma inverse_unique: "!! a::'a::ring. [| a * x = 1; a * y = 1 |] ==> x = y" + apply (rule_tac a = "(a*y) * x" and b = "y * (a*x)" in box_equals) + apply (simp (no_asm)) + apply auto + done + +lemma r_inverse_ring: "!! a::'a::ring. a dvd 1 ==> a * inverse a = 1" + apply (unfold inverse_def dvd_def) + apply (tactic {* asm_full_simp_tac (simpset () delsimprocs [ring_simproc]) 1 *}) + apply clarify + apply (rule theI) + apply assumption + apply (rule inverse_unique) + apply assumption + apply assumption + done + +lemma l_inverse_ring: "!! a::'a::ring. a dvd 1 ==> inverse a * a = 1" + by (simp add: r_inverse_ring) + + +(* Fields *) + +section "Fields" + +lemma field_unit [simp]: "!! a::'a::field. (a dvd 1) = (a ~= 0)" + by (auto dest: field_ax dvd_zero_left simp add: field_one_not_zero) + +lemma r_inverse [simp]: "!! a::'a::field. a ~= 0 ==> a * inverse a = 1" + by (simp add: r_inverse_ring) + +lemma l_inverse [simp]: "!! a::'a::field. a ~= 0 ==> inverse a * a= 1" + by (simp add: l_inverse_ring) + + +(* fields are integral domains *) + +lemma field_integral: "!! a::'a::field. a * b = 0 ==> a = 0 | b = 0" + apply (tactic "Step_tac 1") + apply (rule_tac a = " (a*b) * inverse b" in box_equals) + apply (rule_tac [3] refl) + prefer 2 + apply (simp (no_asm)) + apply auto + done + + +(* fields are factorial domains *) + +lemma field_fact_prime: "!! a::'a::field. irred a ==> prime a" + unfolding prime_def irred_def by (blast intro: field_ax) end diff -r 25ed0a4c7dc5 -r 6cdd0589aa73 src/HOL/Algebra/abstract/RingHomo.ML --- a/src/HOL/Algebra/abstract/RingHomo.ML Sun Nov 19 13:02:55 2006 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,64 +0,0 @@ -(* - Ring homomorphism - $Id$ - Author: Clemens Ballarin, started 15 April 1997 -*) - -(* Ring homomorphism *) - -Goalw [thm "homo_def"] - "!! f. [| !! a b. f (a + b) = f a + f b; !! a b. f (a * b) = f a * f b; \ -\ f 1 = 1 |] ==> homo f"; -by Auto_tac; -qed "homoI"; - -Goalw [thm "homo_def"] "!! f. homo f ==> f (a + b) = f a + f b"; -by (Fast_tac 1); -qed "homo_add"; - -Goalw [thm "homo_def"] "!! f. homo f ==> f (a * b) = f a * f b"; -by (Fast_tac 1); -qed "homo_mult"; - -Goalw [thm "homo_def"] "!! f. homo f ==> f 1 = 1"; -by (Fast_tac 1); -qed "homo_one"; - -Goal "!! f::('a::ring=>'b::ring). homo f ==> f 0 = 0"; -by (res_inst_tac [("a", "f 0")] a_lcancel 1); -by (asm_simp_tac (simpset() addsimps [homo_add RS sym]) 1); -qed "homo_zero"; - -Goal - "!! f::('a::ring=>'b::ring). homo f ==> f (-a) = - f a"; -by (res_inst_tac [("a", "f a")] a_lcancel 1); -by (ftac homo_zero 1); -by (asm_simp_tac (simpset() addsimps [homo_add RS sym]) 1); -qed "homo_uminus"; - -Goal "!! f::('a::ring=>'b::ring). homo f ==> f (a ^ n) = f a ^ n"; -by (induct_tac "n" 1); -by (dtac homo_one 1); -by (Asm_simp_tac 1); -by (dres_inst_tac [("a", "a^n"), ("b", "a")] homo_mult 1); -by (Asm_full_simp_tac 1); -qed "homo_power"; - -Goal - "!! f::('a::ring=>'b::ring). \ -\ homo f ==> f (setsum g {..n::nat}) = setsum (f o g) {..n}"; -by (induct_tac "n" 1); -by (Asm_simp_tac 1); -by (Simp_tac 1); -by (dres_inst_tac [("a", "g (Suc n)"), ("b", "setsum g {..n}")] homo_add 1); -by (Asm_full_simp_tac 1); -qed "homo_SUM"; - -Addsimps [homo_add, homo_mult, homo_one, homo_zero, - homo_uminus, homo_power, homo_SUM]; - -Goal "homo (%x. x)"; -by (fast_tac (claset() addSIs [homoI]) 1); -qed "id_homo"; - -Addsimps [id_homo]; diff -r 25ed0a4c7dc5 -r 6cdd0589aa73 src/HOL/Algebra/abstract/RingHomo.thy --- a/src/HOL/Algebra/abstract/RingHomo.thy Sun Nov 19 13:02:55 2006 +0100 +++ b/src/HOL/Algebra/abstract/RingHomo.thy Sun Nov 19 23:48:55 2006 +0100 @@ -4,12 +4,60 @@ Author: Clemens Ballarin, started 15 April 1997 *) +header {* Ring homomorphism *} + theory RingHomo imports Ring2 begin -constdefs - homo :: "('a::ring => 'b::ring) => bool" - "homo f == (ALL a b. f (a + b) = f a + f b & +definition + homo :: "('a::ring => 'b::ring) => bool" where + "homo f \ (ALL a b. f (a + b) = f a + f b & f (a * b) = f a * f b) & f 1 = 1" + +lemma homoI: + "!! f. [| !! a b. f (a + b) = f a + f b; !! a b. f (a * b) = f a * f b; + f 1 = 1 |] ==> homo f" + unfolding homo_def by blast + +lemma homo_add [simp]: "!! f. homo f ==> f (a + b) = f a + f b" + unfolding homo_def by blast + +lemma homo_mult [simp]: "!! f. homo f ==> f (a * b) = f a * f b" + unfolding homo_def by blast + +lemma homo_one [simp]: "!! f. homo f ==> f 1 = 1" + unfolding homo_def by blast + +lemma homo_zero [simp]: "!! f::('a::ring=>'b::ring). homo f ==> f 0 = 0" + apply (rule_tac a = "f 0" in a_lcancel) + apply (simp (no_asm_simp) add: homo_add [symmetric]) + done + +lemma homo_uminus [simp]: + "!! f::('a::ring=>'b::ring). homo f ==> f (-a) = - f a" + apply (rule_tac a = "f a" in a_lcancel) + apply (frule homo_zero) + apply (simp (no_asm_simp) add: homo_add [symmetric]) + done + +lemma homo_power [simp]: "!! f::('a::ring=>'b::ring). homo f ==> f (a ^ n) = f a ^ n" + apply (induct_tac n) + apply (drule homo_one) + apply simp + apply (drule_tac a = "a^n" and b = "a" in homo_mult) + apply simp + done + +lemma homo_SUM [simp]: + "!! f::('a::ring=>'b::ring). + homo f ==> f (setsum g {..n::nat}) = setsum (f o g) {..n}" + apply (induct_tac n) + apply simp + apply simp + done + +lemma id_homo [simp]: "homo (%x. x)" + by (blast intro!: homoI) + end diff -r 25ed0a4c7dc5 -r 6cdd0589aa73 src/HOL/Algebra/abstract/order.ML --- a/src/HOL/Algebra/abstract/order.ML Sun Nov 19 13:02:55 2006 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,142 +0,0 @@ -(* - Title: Term order, needed for normal forms in rings - Id: $Id$ - Author: Clemens Ballarin - Copyright: TU Muenchen -*) - -(*** Term order for commutative rings ***) - -fun ring_ord (Const (a, _)) = - find_index (fn a' => a = a') ["HOL.zero", "HOL.plus", "HOL.uminus", "HOL.minus", "HOL.one", "HOL.times"] - | ring_ord _ = ~1; - -fun termless_ring (a, b) = (Term.term_lpo ring_ord (a, b) = LESS); - -(* Some code useful for debugging - -val intT = HOLogic.intT; -val a = Free ("a", intT); -val b = Free ("b", intT); -val c = Free ("c", intT); -val plus = Const ("HOL.plus", [intT, intT]--->intT); -val mult = Const ("HOL.times", [intT, intT]--->intT); -val uminus = Const ("HOL.uminus", intT-->intT); -val one = Const ("HOL.one", intT); -val f = Const("f", intT-->intT); - -*) - -(*** Rewrite rules ***) - -val a_assoc = thm "ring_class.a_assoc"; -val l_zero = thm "ring_class.l_zero"; -val l_neg = thm "ring_class.l_neg"; -val a_comm = thm "ring_class.a_comm"; -val m_assoc = thm "ring_class.m_assoc"; -val l_one = thm "ring_class.l_one"; -val l_distr = thm "ring_class.l_distr"; -val m_comm = thm "ring_class.m_comm"; -val minus_def = thm "ring_class.minus_def"; -val inverse_def = thm "ring_class.inverse_def"; -val divide_def = thm "ring_class.divide_def"; -val power_def = thm "ring_class.power_def"; - -(* These are the following axioms: - - a_assoc: "(a + b) + c = a + (b + c)" - l_zero: "0 + a = a" - l_neg: "(-a) + a = 0" - a_comm: "a + b = b + a" - - m_assoc: "(a * b) * c = a * (b * c)" - l_one: "1 * a = a" - - l_distr: "(a + b) * c = a * c + b * c" - - m_comm: "a * b = b * a" - - -- {* Definition of derived operations *} - - minus_def: "a - b = a + (-b)" - inverse_def: "inverse a = (if a dvd 1 then THE x. a*x = 1 else 0)" - divide_def: "a / b = a * inverse b" - power_def: "a ^ n = nat_rec 1 (%u b. b * a) n" -*) - -(* These lemmas are needed in the proofs *) -val trans = thm "trans"; -val sym = thm "sym"; -val subst = thm "subst"; -val box_equals = thm "box_equals"; -val arg_cong = thm "arg_cong"; - -(* derived rewrite rules *) -val a_lcomm = prove_goal (the_context ()) "(a::'a::ring)+(b+c) = b+(a+c)" - (fn _ => [rtac (a_comm RS trans) 1, rtac (a_assoc RS trans) 1, - rtac (a_comm RS arg_cong) 1]); -val r_zero = prove_goal (the_context ()) "(a::'a::ring) + 0 = a" - (fn _ => [rtac (a_comm RS trans) 1, rtac l_zero 1]); -val r_neg = prove_goal (the_context ()) "(a::'a::ring) + (-a) = 0" - (fn _ => [rtac (a_comm RS trans) 1, rtac l_neg 1]); -val r_neg2 = prove_goal (the_context ()) "(a::'a::ring) + (-a + b) = b" - (fn _ => [rtac (a_assoc RS sym RS trans) 1, - simp_tac (simpset() addsimps [r_neg, l_zero]) 1]); -val r_neg1 = prove_goal (the_context ()) "-(a::'a::ring) + (a + b) = b" - (fn _ => [rtac (a_assoc RS sym RS trans) 1, - simp_tac (simpset() addsimps [l_neg, l_zero]) 1]); -(* auxiliary *) -val a_lcancel = prove_goal (the_context ()) "!! a::'a::ring. a + b = a + c ==> b = c" - (fn _ => [rtac box_equals 1, rtac l_zero 2, rtac l_zero 2, - res_inst_tac [("a1", "a")] (l_neg RS subst) 1, - asm_simp_tac (simpset() addsimps [a_assoc]) 1]); -val minus_add = prove_goal (the_context ()) "-((a::'a::ring) + b) = (-a) + (-b)" - (fn _ => [res_inst_tac [("a", "a+b")] a_lcancel 1, - simp_tac (simpset() addsimps [r_neg, l_neg, l_zero, - a_assoc, a_comm, a_lcomm]) 1]); -val minus_minus = prove_goal (the_context ()) "-(-(a::'a::ring)) = a" - (fn _ => [rtac a_lcancel 1, rtac (r_neg RS trans) 1, rtac (l_neg RS sym) 1]); -val minus0 = prove_goal (the_context ()) "- 0 = (0::'a::ring)" - (fn _ => [rtac a_lcancel 1, rtac (r_neg RS trans) 1, - rtac (l_zero RS sym) 1]); - -(* derived rules for multiplication *) -val m_lcomm = prove_goal (the_context ()) "(a::'a::ring)*(b*c) = b*(a*c)" - (fn _ => [rtac (m_comm RS trans) 1, rtac (m_assoc RS trans) 1, - rtac (m_comm RS arg_cong) 1]); -val r_one = prove_goal (the_context ()) "(a::'a::ring) * 1 = a" - (fn _ => [rtac (m_comm RS trans) 1, rtac l_one 1]); -val r_distr = prove_goal (the_context ()) "(a::'a::ring) * (b + c) = a * b + a * c" - (fn _ => [rtac (m_comm RS trans) 1, rtac (l_distr RS trans) 1, - simp_tac (simpset() addsimps [m_comm]) 1]); -(* the following proof is from Jacobson, Basic Algebra I, pp. 88-89 *) -val l_null = prove_goal (the_context ()) "0 * (a::'a::ring) = 0" - (fn _ => [rtac a_lcancel 1, rtac (l_distr RS sym RS trans) 1, - simp_tac (simpset() addsimps [r_zero]) 1]); -val r_null = prove_goal (the_context ()) "(a::'a::ring) * 0 = 0" - (fn _ => [rtac (m_comm RS trans) 1, rtac l_null 1]); -val l_minus = prove_goal (the_context ()) "(-(a::'a::ring)) * b = - (a * b)" - (fn _ => [rtac a_lcancel 1, rtac (r_neg RS sym RSN (2, trans)) 1, - rtac (l_distr RS sym RS trans) 1, - simp_tac (simpset() addsimps [l_null, r_neg]) 1]); -val r_minus = prove_goal (the_context ()) "(a::'a::ring) * (-b) = - (a * b)" - (fn _ => [rtac a_lcancel 1, rtac (r_neg RS sym RSN (2, trans)) 1, - rtac (r_distr RS sym RS trans) 1, - simp_tac (simpset() addsimps [r_null, r_neg]) 1]); - -val ring_ss = HOL_basic_ss settermless termless_ring addsimps - [a_assoc, l_zero, l_neg, a_comm, m_assoc, l_one, l_distr, m_comm, minus_def, - r_zero, r_neg, r_neg2, r_neg1, minus_add, minus_minus, minus0, - a_lcomm, m_lcomm, (*r_one,*) r_distr, l_null, r_null, l_minus, r_minus]; - -(* Note: r_one is not necessary in ring_ss *) - -val x = bind_thms ("ring_simps", - [l_zero, r_zero, l_neg, r_neg, minus_minus, minus0, - l_one, r_one, l_null, r_null, l_minus, r_minus]); - -(* note: not added (and not proved): - a_lcancel_eq, a_rcancel_eq, power_one, power_Suc, power_zero, power_one, - m_lcancel_eq, m_rcancel_eq, - thms involving dvd, integral domains, fields -*) diff -r 25ed0a4c7dc5 -r 6cdd0589aa73 src/HOL/Algebra/poly/LongDiv.ML --- a/src/HOL/Algebra/poly/LongDiv.ML Sun Nov 19 13:02:55 2006 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,279 +0,0 @@ -(* - Long division of polynomials - $Id$ - Author: Clemens Ballarin, started 23 June 1999 -*) - -(* legacy bindings and theorems *) - -val deg_aboveI = thm "deg_aboveI"; -val smult_l_minus = thm "smult_l_minus"; -val deg_monom_ring = thm "deg_monom_ring"; -val deg_smult_ring = thm "deg_smult_ring"; -val smult_l_distr = thm "smult_l_distr"; -val smult_r_distr = thm "smult_r_distr"; -val smult_r_minus = thm "smult_r_minus"; -val smult_assoc2 = thm "smult_assoc2"; -val smult_assoc1 = thm "smult_assoc1"; -val monom_mult_smult = thm "monom_mult_smult"; -val field_ax = thm "field_ax"; -val lcoeff_nonzero = thm "lcoeff_nonzero"; - -val lcoeff_def = thm "lcoeff_def"; -val eucl_size_def = thm "eucl_size_def"; - -val SUM_shrink_below_lemma = thm "SUM_shrink_below_lemma"; - -Goal - "!! f::(nat=>'a::ring). \ -\ [| m <= n; !!i. i < m ==> f i = 0; P (setsum (%i. f (i+m)) {..n-m}) |] \ -\ ==> P (setsum f {..n})"; -by (asm_full_simp_tac - (simpset() addsimps [SUM_shrink_below_lemma, add_diff_inverse, leD]) 1); -qed "SUM_extend_below"; - -Goal - "!! p::'a::ring up. \ -\ [| deg p <= n; P (setsum (%i. monom (coeff p i) i) {..n}) |] \ -\ ==> P p"; -by (asm_full_simp_tac (simpset() addsimps [thm "up_repr_le"]) 1); -qed "up_repr2D"; - -(* Start of LongDiv *) - -Goal - "!!p::('a::ring up). \ -\ [| deg p <= deg r; deg q <= deg r; \ -\ coeff p (deg r) = - (coeff q (deg r)); deg r ~= 0 |] ==> \ -\ deg (p + q) < deg r"; -by (res_inst_tac [("j", "deg r - 1")] le_less_trans 1); -by (arith_tac 2); -by (rtac deg_aboveI 1); -by (strip_tac 1); -by (case_tac "deg r = m" 1); -by (Clarify_tac 1); -by (Asm_full_simp_tac 1); -(* case "deg q ~= m" *) -by (subgoal_tac "deg p < m & deg q < m" 1); -by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1); -by (arith_tac 1); -qed "deg_lcoeff_cancel"; - -Goal - "!!p::('a::ring up). \ -\ [| deg p <= deg r; deg q <= deg r; \ -\ p ~= -q; coeff p (deg r) = - (coeff q (deg r)) |] ==> \ -\ deg (p + q) < deg r"; -by (rtac deg_lcoeff_cancel 1); -by (REPEAT (atac 1)); -by (rtac classical 1); -by (Clarify_tac 1); -by (etac notE 1); -by (res_inst_tac [("p", "p")] up_repr2D 1 THEN atac 1); -by (res_inst_tac [("p", "q")] up_repr2D 1 THEN atac 1); -by (rotate_tac ~1 1); -by (asm_full_simp_tac (simpset() addsimps [smult_l_minus]) 1); -qed "deg_lcoeff_cancel2"; - -Goal - "!!g::('a::ring up). g ~= 0 ==> \ -\ Ex (% (q, r, k). \ -\ (lcoeff g)^k *s f = q * g + r & (eucl_size r < eucl_size g))"; -by (res_inst_tac [("P", "%f. Ex (% (q, r, k). \ -\ (lcoeff g)^k *s f = q * g + r & (eucl_size r < eucl_size g))")] - wf_induct 1); -(* TO DO: replace by measure_induct *) -by (res_inst_tac [("f", "eucl_size")] wf_measure 1); -by (case_tac "eucl_size x < eucl_size g" 1); -by (res_inst_tac [("x", "(0, x, 0)")] exI 1); -by (Asm_simp_tac 1); -(* case "eucl_size x >= eucl_size g" *) -by (dres_inst_tac [("x", "lcoeff g *s x - (monom (lcoeff x) (deg x - deg g)) * g")] spec 1); -by (etac impE 1); -by (full_simp_tac (simpset() addsimps [inv_image_def, measure_def, lcoeff_def]) 1); -by (case_tac "x = 0" 1); -by (rotate_tac ~1 1); -by (asm_full_simp_tac (simpset() addsimps [eucl_size_def]) 1); -(* case "x ~= 0 *) -by (rotate_tac ~1 1); -by (asm_full_simp_tac (simpset() addsimps [eucl_size_def]) 1); -(* by (Simp_tac 1); *) -by (rtac impI 1); -by (rtac deg_lcoeff_cancel2 1); - (* replace by linear arithmetic??? *) - by (rtac le_trans 2); - by (rtac deg_smult_ring 2); - by (Simp_tac 2); - by (Simp_tac 1); - by (rtac le_trans 1); - by (rtac deg_mult_ring 1); - by (rtac le_trans 1); -(**) - by (rtac add_le_mono 1); by (rtac le_refl 1); - (* term order forces to use this instead of add_le_mono1 *) - by (rtac deg_monom_ring 1); - by (Asm_simp_tac 1); -(**) -(* - by (rtac add_le_mono1 1); - by (rtac deg_smult_ring 1); -(* by (asm_simp_tac (simpset() addsimps [leI]) 1); *) - by (Asm_simp_tac 1); - by (cut_inst_tac [("m", "deg x - deg g"), ("'a", "'a")] deg_monom_ring 1); - by (arith_tac 1); -*) -by (Force_tac 1); -by (Simp_tac 1); -(**) - (* This change is probably caused by application of commutativity *) -by (res_inst_tac [("m", "deg g"), ("n", "deg x")] SUM_extend 1); -by (Simp_tac 1); -by (Asm_simp_tac 1); -by (arith_tac 1); -by (res_inst_tac [("m", "deg g"), ("n", "deg g")] SUM_extend_below 1); -by (rtac le_refl 1); -by (Asm_simp_tac 1); -by (arith_tac 1); -by (Simp_tac 1); -(**) -(* -by (res_inst_tac [("m", "deg x - deg g"), ("n", "deg x")] SUM_extend 1); -by (Simp_tac 1); -by (asm_simp_tac (simpset() addsimps [less_not_refl2 RS not_sym]) 1); -by (res_inst_tac [("m", "deg x - deg g"), ("n", "deg x - deg g")] - SUM_extend_below 1); -by (rtac le_refl 1); -by (asm_simp_tac (simpset() addsimps [less_not_refl2]) 1); -by (asm_simp_tac (simpset() addsimps [diff_diff_right, leI, m_comm]) 1); -*) -(* end of subproof deg f1 < deg f *) -by (etac exE 1); -by (res_inst_tac [("x", "((%(q,r,k). (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); -by (Clarify_tac 1); -by (dtac sym 1); -by (simp_tac (simpset() addsimps [l_distr, a_assoc] - delsimprocs [ring_simproc]) 1); -by (asm_simp_tac (simpset() delsimprocs [ring_simproc]) 1); -by (simp_tac (simpset() addsimps [minus_def, smult_r_distr, smult_r_minus, - monom_mult_smult, smult_assoc1, smult_assoc2] - delsimprocs [ring_simproc]) 1); -by (Simp_tac 1); -qed "long_div_eucl_size"; - -Goal - "!!g::('a::ring up). g ~= 0 ==> \ -\ Ex (% (q, r, k). \ -\ (lcoeff g)^k *s f = q * g + r & (r = 0 | deg r < deg g))"; -by (forw_inst_tac [("f", "f")] - (simplify (simpset() addsimps [eucl_size_def] - delsimprocs [ring_simproc]) long_div_eucl_size) 1); -by (auto_tac (claset(), simpset() delsimprocs [ring_simproc])); -by (case_tac "aa = 0" 1); -by (Blast_tac 1); -(* case "aa ~= 0 *) -by (rotate_tac ~1 1); -by Auto_tac; -qed "long_div_ring"; - -(* Next one fails *) -Goal - "!!g::('a::ring up). [| g ~= 0; (lcoeff g) dvd 1 |] ==> \ -\ Ex (% (q, r). f = q * g + r & (r = 0 | deg r < deg g))"; -by (forw_inst_tac [("f", "f")] long_div_ring 1); -by (etac exE 1); -by (res_inst_tac [("x", "((%(q,r,k). (inverse(lcoeff g ^k) *s q)) x, \ -\ (%(q,r,k). inverse(lcoeff g ^k) *s r) x)")] exI 1); -by (Clarify_tac 1); -(* by (Simp_tac 1); *) -by (rtac conjI 1); -by (dtac sym 1); -by (asm_simp_tac (simpset() addsimps [smult_r_distr RS sym, smult_assoc2] - delsimprocs [ring_simproc]) 1); -by (asm_simp_tac (simpset() addsimps [l_inverse_ring, unit_power, smult_assoc1 RS sym]) 1); -(* degree property *) -by (etac disjE 1); -by (Asm_simp_tac 1); -by (rtac disjI2 1); -by (rtac le_less_trans 1); -by (rtac deg_smult_ring 1); -by (Asm_simp_tac 1); -qed "long_div_unit"; - -Goal - "!!g::('a::field up). g ~= 0 ==> \ -\ Ex (% (q, r). f = q * g + r & (r = 0 | deg r < deg g))"; -by (rtac long_div_unit 1); -by (assume_tac 1); -by (asm_simp_tac (simpset() addsimps [lcoeff_def, lcoeff_nonzero, field_ax]) 1); -qed "long_div_theorem"; - -Goal "- (0::'a::ring) = 0"; -by (Simp_tac 1); -val uminus_zero = result(); - -Goal "!!a::'a::ring. a - b = 0 ==> a = b"; -by (res_inst_tac [("s", "a - (a - b)")] trans 1); -by (asm_simp_tac (simpset() delsimprocs [ring_simproc]) 1); -by (Simp_tac 1); -by (Simp_tac 1); -val diff_zero_imp_eq = result(); - -Goal "!!a::'a::ring. a = b ==> a + (-b) = 0"; -by (Asm_simp_tac 1); -val eq_imp_diff_zero = result(); - -Goal - "!!g::('a::field up). [| g ~= 0; \ -\ f = q1 * g + r1; (r1 = 0 | deg r1 < deg g); \ -\ f = q2 * g + r2; (r2 = 0 | deg r2 < deg g) |] ==> q1 = q2"; -by (subgoal_tac "(q1 - q2) * g = r2 - r1" 1); (* 1 *) -by (thin_tac "f = ?x" 1); -by (thin_tac "f = ?x" 1); -by (rtac diff_zero_imp_eq 1); -by (rtac classical 1); -by (etac disjE 1); -(* r1 = 0 *) -by (etac disjE 1); -(* r2 = 0 *) -by (asm_full_simp_tac (simpset() - addsimps [thm "integral_iff", minus_def, l_zero, uminus_zero] - delsimprocs [ring_simproc]) 1); -(* r2 ~= 0 *) -by (dres_inst_tac [("f", "deg"), ("y", "r2 - r1")] arg_cong 1); -by (asm_full_simp_tac (simpset() addsimps [minus_def, l_zero, uminus_zero] - delsimprocs [ring_simproc]) 1); -(* r1 ~=0 *) -by (etac disjE 1); -(* r2 = 0 *) -by (dres_inst_tac [("f", "deg"), ("y", "r2 - r1")] arg_cong 1); -by (asm_full_simp_tac (simpset() addsimps [minus_def, l_zero, uminus_zero] - delsimprocs [ring_simproc]) 1); -(* r2 ~= 0 *) -by (dres_inst_tac [("f", "deg"), ("y", "r2 - r1")] arg_cong 1); -by (asm_full_simp_tac (simpset() addsimps [minus_def] - delsimprocs [ring_simproc]) 1); -by (dtac (order_eq_refl RS add_leD2) 1); -by (dtac leD 1); -by (etac notE 1 THEN rtac (deg_add RS le_less_trans) 1); -by (Asm_simp_tac 1); -(* proof of 1 *) -by (rtac diff_zero_imp_eq 1); -by (hyp_subst_tac 1); -by (dres_inst_tac [("a", "?x+?y")] eq_imp_diff_zero 1); -by (Asm_full_simp_tac 1); -qed "long_div_quo_unique"; - -Goal - "!!g::('a::field up). [| g ~= 0; \ -\ f = q1 * g + r1; (r1 = 0 | deg r1 < deg g); \ -\ f = q2 * g + r2; (r2 = 0 | deg r2 < deg g) |] ==> r1 = r2"; -by (subgoal_tac "q1 = q2" 1); -by (Clarify_tac 1); -by (res_inst_tac [("a", "q2 * g + r1 - q2 * g"), ("b", "q2 * g + r2 - q2 * g")] - box_equals 1); -by (Asm_full_simp_tac 1); -by (Simp_tac 1); -by (Simp_tac 1); -by (rtac long_div_quo_unique 1); -by (REPEAT (atac 1)); -qed "long_div_rem_unique"; diff -r 25ed0a4c7dc5 -r 6cdd0589aa73 src/HOL/Algebra/poly/LongDiv.thy --- a/src/HOL/Algebra/poly/LongDiv.thy Sun Nov 19 13:02:55 2006 +0100 +++ b/src/HOL/Algebra/poly/LongDiv.thy Sun Nov 19 23:48:55 2006 +0100 @@ -6,23 +6,255 @@ theory LongDiv imports PolyHomo begin -consts - lcoeff :: "'a::ring up => 'a" - eucl_size :: "'a::ring => nat" +definition + lcoeff :: "'a::ring up => 'a" where + "lcoeff p = coeff p (deg p)" -defs - lcoeff_def: "lcoeff p == coeff p (deg p)" - eucl_size_def: "eucl_size p == (if p = 0 then 0 else deg p+1)" +definition + eucl_size :: "'a::zero up => nat" where + "eucl_size p = (if p = 0 then 0 else deg p + 1)" lemma SUM_shrink_below_lemma: "!! f::(nat=>'a::ring). (ALL i. i < m --> f i = 0) --> setsum (%i. f (i+m)) {..d} = setsum f {..m+d}" apply (induct_tac d) apply (induct_tac m) - apply (simp) - apply (force) - apply (simp add: ab_semigroup_add_class.add_commute[of m]) + apply simp + apply force + apply (simp add: ab_semigroup_add_class.add_commute [of m]) + done + +lemma SUM_extend_below: + "!! f::(nat=>'a::ring). + [| m <= n; !!i. i < m ==> f i = 0; P (setsum (%i. f (i+m)) {..n-m}) |] + ==> P (setsum f {..n})" + by (simp add: SUM_shrink_below_lemma add_diff_inverse leD) + +lemma up_repr2D: + "!! p::'a::ring up. + [| deg p <= n; P (setsum (%i. monom (coeff p i) i) {..n}) |] + ==> P p" + by (simp add: up_repr_le) + + +(* Start of LongDiv *) + +lemma deg_lcoeff_cancel: + "!!p::('a::ring up). + [| deg p <= deg r; deg q <= deg r; + coeff p (deg r) = - (coeff q (deg r)); deg r ~= 0 |] ==> + deg (p + q) < deg r" + apply (rule_tac j = "deg r - 1" in le_less_trans) + prefer 2 + apply arith + apply (rule deg_aboveI) + apply (case_tac "deg r = m") + apply clarify + apply simp + (* case "deg q ~= m" *) + apply (subgoal_tac "deg p < m & deg q < m") + apply (simp (no_asm_simp) add: deg_aboveD) + apply arith + done + +lemma deg_lcoeff_cancel2: + "!!p::('a::ring up). + [| deg p <= deg r; deg q <= deg r; + p ~= -q; coeff p (deg r) = - (coeff q (deg r)) |] ==> + deg (p + q) < deg r" + apply (rule deg_lcoeff_cancel) + apply assumption+ + apply (rule classical) + apply clarify + apply (erule notE) + apply (rule_tac p = p in up_repr2D, assumption) + apply (rule_tac p = q in up_repr2D, assumption) + apply (rotate_tac -1) + apply (simp add: smult_l_minus) + done + +lemma long_div_eucl_size: + "!!g::('a::ring up). g ~= 0 ==> + Ex (% (q, r, k). + (lcoeff g)^k *s f = q * g + r & (eucl_size r < eucl_size g))" + apply (rule_tac P = "%f. Ex (% (q, r, k) . (lcoeff g) ^k *s f = q * g + r & (eucl_size r < eucl_size g))" in wf_induct) + (* TO DO: replace by measure_induct *) + apply (rule_tac f = eucl_size in wf_measure) + apply (case_tac "eucl_size x < eucl_size g") + apply (rule_tac x = "(0, x, 0)" in exI) + apply (simp (no_asm_simp)) + (* case "eucl_size x >= eucl_size g" *) + apply (drule_tac x = "lcoeff g *s x - (monom (lcoeff x) (deg x - deg g)) * g" in spec) + apply (erule impE) + apply (simp (no_asm_use) add: inv_image_def measure_def lcoeff_def) + apply (case_tac "x = 0") + apply (rotate_tac -1) + apply (simp add: eucl_size_def) + (* case "x ~= 0 *) + apply (rotate_tac -1) + apply (simp add: eucl_size_def) + apply (rule impI) + apply (rule deg_lcoeff_cancel2) + (* replace by linear arithmetic??? *) + apply (rule_tac [2] le_trans) + apply (rule_tac [2] deg_smult_ring) + prefer 2 + apply simp + apply (simp (no_asm)) + apply (rule le_trans) + apply (rule deg_mult_ring) + apply (rule le_trans) +(**) + apply (rule add_le_mono) + apply (rule le_refl) + (* term order forces to use this instead of add_le_mono1 *) + apply (rule deg_monom_ring) + apply (simp (no_asm_simp)) + apply force + apply (simp (no_asm)) +(**) + (* This change is probably caused by application of commutativity *) + apply (rule_tac m = "deg g" and n = "deg x" in SUM_extend) + apply (simp (no_asm)) + apply (simp (no_asm_simp)) + apply arith + apply (rule_tac m = "deg g" and n = "deg g" in SUM_extend_below) + apply (rule le_refl) + apply (simp (no_asm_simp)) + apply arith + apply (simp (no_asm)) +(**) +(* end of subproof deg f1 < deg f *) + apply (erule exE) + apply (rule_tac x = "((% (q,r,k) . (monom (lcoeff g ^ k * lcoeff x) (deg x - deg g) + q)) xa, (% (q,r,k) . r) xa, (% (q,r,k) . Suc k) xa) " in exI) + apply clarify + apply (drule sym) + apply (tactic {* simp_tac (simpset() addsimps [thm "l_distr", thm "a_assoc"] + delsimprocs [ring_simproc]) 1 *}) + apply (tactic {* asm_simp_tac (simpset() delsimprocs [ring_simproc]) 1 *}) + apply (tactic {* simp_tac (simpset () addsimps [thm "minus_def", thm "smult_r_distr", + thm "smult_r_minus", thm "monom_mult_smult", thm "smult_assoc1", thm "smult_assoc2"] + delsimprocs [ring_simproc]) 1 *}) + apply simp + done + +ML {* simplify (simpset() addsimps [thm "eucl_size_def"] + delsimprocs [ring_simproc]) (thm "long_div_eucl_size") *} + +thm long_div_eucl_size [simplified] + +lemma long_div_ring: + "!!g::('a::ring up). g ~= 0 ==> + Ex (% (q, r, k). + (lcoeff g)^k *s f = q * g + r & (r = 0 | deg r < deg g))" + apply (tactic {* forw_inst_tac [("f", "f")] + (simplify (simpset() addsimps [thm "eucl_size_def"] + delsimprocs [ring_simproc]) (thm "long_div_eucl_size")) 1 *}) + apply (tactic {* auto_tac (claset(), simpset() delsimprocs [ring_simproc]) *}) + apply (case_tac "aa = 0") + apply blast + (* case "aa ~= 0 *) + apply (rotate_tac -1) + apply auto + done + +(* Next one fails *) +lemma long_div_unit: + "!!g::('a::ring up). [| g ~= 0; (lcoeff g) dvd 1 |] ==> + Ex (% (q, r). f = q * g + r & (r = 0 | deg r < deg g))" + apply (frule_tac f = "f" in long_div_ring) + apply (erule exE) + apply (rule_tac x = "((% (q,r,k) . (inverse (lcoeff g ^k) *s q)) x, (% (q,r,k) . inverse (lcoeff g ^k) *s r) x) " in exI) + apply clarify + apply (rule conjI) + apply (drule sym) + apply (tactic {* asm_simp_tac + (simpset() addsimps [thm "smult_r_distr" RS sym, thm "smult_assoc2"] + delsimprocs [ring_simproc]) 1 *}) + apply (simp (no_asm_simp) add: l_inverse_ring unit_power smult_assoc1 [symmetric]) + (* degree property *) + apply (erule disjE) + apply (simp (no_asm_simp)) + apply (rule disjI2) + apply (rule le_less_trans) + apply (rule deg_smult_ring) + apply (simp (no_asm_simp)) + done + +lemma long_div_theorem: + "!!g::('a::field up). g ~= 0 ==> + Ex (% (q, r). f = q * g + r & (r = 0 | deg r < deg g))" + apply (rule long_div_unit) + apply assumption + apply (simp (no_asm_simp) add: lcoeff_def lcoeff_nonzero field_ax) + done + +lemma uminus_zero: "- (0::'a::ring) = 0" + by simp + +lemma diff_zero_imp_eq: "!!a::'a::ring. a - b = 0 ==> a = b" + apply (rule_tac s = "a - (a - b) " in trans) + apply (tactic {* asm_simp_tac (simpset() delsimprocs [ring_simproc]) 1 *}) + apply simp + apply (simp (no_asm)) + done + +lemma eq_imp_diff_zero: "!!a::'a::ring. a = b ==> a + (-b) = 0" + by simp + +lemma long_div_quo_unique: + "!!g::('a::field up). [| g ~= 0; + f = q1 * g + r1; (r1 = 0 | deg r1 < deg g); + f = q2 * g + r2; (r2 = 0 | deg r2 < deg g) |] ==> q1 = q2" + apply (subgoal_tac "(q1 - q2) * g = r2 - r1") (* 1 *) + apply (erule_tac V = "f = ?x" in thin_rl) + apply (erule_tac V = "f = ?x" in thin_rl) + apply (rule diff_zero_imp_eq) + apply (rule classical) + apply (erule disjE) + (* r1 = 0 *) + apply (erule disjE) + (* r2 = 0 *) + apply (tactic {* asm_full_simp_tac (simpset() + addsimps [thm "integral_iff", thm "minus_def", thm "l_zero", thm "uminus_zero"] + delsimprocs [ring_simproc]) 1 *}) + (* r2 ~= 0 *) + apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong) + apply (tactic {* asm_full_simp_tac (simpset() addsimps + [thm "minus_def", thm "l_zero", thm "uminus_zero"] delsimprocs [ring_simproc]) 1 *}) + (* r1 ~=0 *) + apply (erule disjE) + (* r2 = 0 *) + apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong) + apply (tactic {* asm_full_simp_tac (simpset() addsimps + [thm "minus_def", thm "l_zero", thm "uminus_zero"] delsimprocs [ring_simproc]) 1 *}) + (* r2 ~= 0 *) + apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong) + apply (tactic {* asm_full_simp_tac (simpset() addsimps [thm "minus_def"] + delsimprocs [ring_simproc]) 1 *}) + apply (drule order_eq_refl [THEN add_leD2]) + apply (drule leD) + apply (erule notE, rule deg_add [THEN le_less_trans]) + apply (simp (no_asm_simp)) + (* proof of 1 *) + apply (rule diff_zero_imp_eq) + apply hypsubst + apply (drule_tac a = "?x+?y" in eq_imp_diff_zero) + apply simp + done + +lemma long_div_rem_unique: + "!!g::('a::field up). [| g ~= 0; + f = q1 * g + r1; (r1 = 0 | deg r1 < deg g); + f = q2 * g + r2; (r2 = 0 | deg r2 < deg g) |] ==> r1 = r2" + apply (subgoal_tac "q1 = q2") + apply clarify + apply (rule_tac a = "q2 * g + r1 - q2 * g" and b = "q2 * g + r2 - q2 * g" in box_equals) + apply simp + apply (simp (no_asm)) + apply (simp (no_asm)) + apply (rule long_div_quo_unique) + apply assumption+ done end - diff -r 25ed0a4c7dc5 -r 6cdd0589aa73 src/HOL/Algebra/poly/PolyHomo.ML --- a/src/HOL/Algebra/poly/PolyHomo.ML Sun Nov 19 13:02:55 2006 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,232 +0,0 @@ -(* - Universal property and evaluation homomorphism of univariate polynomials - $Id$ - Author: Clemens Ballarin, started 16 April 1997 -*) - -(* Summation result for tactic-style proofs *) - -val natsum_add = thm "natsum_add"; -val natsum_ldistr = thm "natsum_ldistr"; -val natsum_rdistr = thm "natsum_rdistr"; - -Goal - "!! f::(nat=>'a::ring). \ -\ m <= n & (ALL i. m < i & i <= n --> f i = 0) --> \ -\ setsum f {..m} = setsum f {..n}"; -by (induct_tac "n" 1); -(* Base case *) -by (Simp_tac 1); -(* Induction step *) -by (case_tac "m <= n" 1); -by Auto_tac; -by (subgoal_tac "m = Suc n" 1); -by (Asm_simp_tac 1); -by (fast_arith_tac 1); -val SUM_shrink_lemma = result(); - -Goal - "!! f::(nat=>'a::ring). \ -\ [| m <= n; !!i. [| m < i; i <= n |] ==> f i = 0; P (setsum f {..n}) |] \ -\ ==> P (setsum f {..m})"; -by (cut_inst_tac [("m", "m"), ("n", "n"), ("f", "f")] SUM_shrink_lemma 1); -by (Asm_full_simp_tac 1); -qed "SUM_shrink"; - -Goal - "!! f::(nat=>'a::ring). \ -\ [| m <= n; !!i. [| m < i; i <= n |] ==> f i = 0; P (setsum f {..m}) |] \ -\ ==> P (setsum f {..n})"; -by (cut_inst_tac [("m", "m"), ("n", "n"), ("f", "f")] SUM_shrink_lemma 1); -by (Asm_full_simp_tac 1); -qed "SUM_extend"; - -Goal - "!!f::nat=>'a::ring. j <= n + m --> \ -\ setsum (%k. setsum (%i. f i * g (k - i)) {..k}) {..j} = \ -\ setsum (%k. setsum (%i. f k * g i) {..j - k}) {..j}"; -by (induct_tac "j" 1); -(* Base case *) -by (Simp_tac 1); -(* Induction step *) -by (simp_tac (simpset() addsimps [Suc_diff_le, natsum_add]) 1); -(* -by (asm_simp_tac (simpset() addsimps a_ac) 1); -*) -by (Asm_simp_tac 1); -val DiagSum_lemma = result(); - -Goal - "!!f::nat=>'a::ring. \ -\ setsum (%k. setsum (%i. f i * g (k - i)) {..k}) {..n + m} = \ -\ setsum (%k. setsum (%i. f k * g i) {..n + m - k}) {..n + m}"; -by (rtac (DiagSum_lemma RS mp) 1); -by (rtac le_refl 1); -qed "DiagSum"; - -Goal - "!! f::nat=>'a::ring. [| bound n f; bound m g|] ==> \ -\ setsum (%k. setsum (%i. f i * g (k-i)) {..k}) {..n + m} = \ -\ setsum f {..n} * setsum g {..m}"; -by (simp_tac (simpset() addsimps [natsum_ldistr, DiagSum]) 1); -(* SUM_rdistr must be applied after SUM_ldistr ! *) -by (simp_tac (simpset() addsimps [natsum_rdistr]) 1); -by (res_inst_tac [("m", "n"), ("n", "n+m")] SUM_extend 1); -by (rtac le_add1 1); -by (Force_tac 1); -by (rtac (thm "natsum_cong") 1); -by (rtac refl 1); -by (res_inst_tac [("m", "m"), ("n", "n+m-i")] SUM_shrink 1); -by (asm_simp_tac (simpset() addsimps [le_add_diff]) 1); -by Auto_tac; -qed "CauchySum"; - -(* Ring homomorphisms and polynomials *) -(* -Goal "homo (const::'a::ring=>'a up)"; -by (auto_tac (claset() addSIs [homoI], simpset())); -qed "const_homo"; - -Delsimps [const_add, const_mult, const_one, const_zero]; -Addsimps [const_homo]; - -Goal - "!!f::'a::ring up=>'b::ring. homo f ==> f (a *s p) = f (const a) * f p"; -by (asm_simp_tac (simpset() addsimps [const_mult_is_smult RS sym]) 1); -qed "homo_smult"; - -Addsimps [homo_smult]; -*) - -val deg_add = thm "deg_add"; -val deg_mult_ring = thm "deg_mult_ring"; -val deg_aboveD = thm "deg_aboveD"; -val coeff_add = thm "coeff_add"; -val coeff_mult = thm "coeff_mult"; -val boundI = thm "boundI"; -val monom_mult_is_smult = thm "monom_mult_is_smult"; - -(* Evaluation homomorphism *) - -Goal - "!! phi::('a::ring=>'b::ring). homo phi ==> homo (EVAL2 phi a)"; -by (rtac homoI 1); -by (rewtac (thm "EVAL2_def")); -(* + commutes *) -(* degree estimations: - bound of all sums can be extended to max (deg aa) (deg b) *) -by (res_inst_tac [("m", "deg (aa + b)"), ("n", "max (deg aa) (deg b)")] - SUM_shrink 1); -by (rtac deg_add 1); -by (asm_simp_tac (simpset() delsimps [coeff_add] addsimps [deg_aboveD]) 1); -by (res_inst_tac [("m", "deg aa"), ("n", "max (deg aa) (deg b)")] - SUM_shrink 1); -by (rtac le_maxI1 1); -by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1); -by (res_inst_tac [("m", "deg b"), ("n", "max (deg aa) (deg b)")] - SUM_shrink 1); -by (rtac le_maxI2 1); -by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1); -(* actual homom property + *) -by (asm_simp_tac (simpset() addsimps [l_distr, natsum_add]) 1); - -(* * commutes *) -by (res_inst_tac [("m", "deg (aa * b)"), ("n", "deg aa + deg b")] - SUM_shrink 1); -by (rtac deg_mult_ring 1); -by (asm_simp_tac (simpset() delsimps [coeff_mult] addsimps [deg_aboveD]) 1); -by (rtac trans 1); -by (rtac CauchySum 2); -by (asm_simp_tac (simpset() addsimps [boundI, deg_aboveD]) 2); -by (asm_simp_tac (simpset() addsimps [boundI, deg_aboveD]) 2); -(* getting a^i and a^(k-i) together is difficult, so we do it manually *) -by (res_inst_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}")] trans 1); -by (asm_simp_tac (simpset() - addsimps [power_mult, leD RS add_diff_inverse, natsum_ldistr]) 1); -by (Simp_tac 1); -(* 1 commutes *) -by (Asm_simp_tac 1); -qed "EVAL2_homo"; - -Goalw [thm "EVAL2_def"] - "!! phi::'a::ring=>'b::ring. EVAL2 phi a (monom b 0) = phi b"; -by (Simp_tac 1); -qed "EVAL2_const"; - -Goalw [thm "EVAL2_def"] - "!! phi::'a::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom 1 1) = a"; -(* Must be able to distinguish 0 from 1, hence 'a::domain *) -by (Asm_simp_tac 1); -qed "EVAL2_monom1"; - -Goalw [thm "EVAL2_def"] - "!! phi::'a::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom 1 n) = a ^ n"; -by (Simp_tac 1); -by (case_tac "n" 1); -by Auto_tac; -qed "EVAL2_monom"; - -Goal - "!! phi::'a::ring=>'b::ring. \ -\ homo phi ==> EVAL2 phi a (b *s p) = phi b * EVAL2 phi a p"; -by (asm_simp_tac (simpset() - addsimps [monom_mult_is_smult RS sym, EVAL2_homo, EVAL2_const]) 1); -qed "EVAL2_smult"; - -val up_eqI = thm "up_eqI"; - -Goal "monom (a::'a::ring) n = monom a 0 * monom 1 n"; -by (simp_tac (simpset() addsimps [monom_mult_is_smult]) 1); -by (rtac up_eqI 1); -by (Simp_tac 1); -qed "monom_decomp"; - -Goal - "!! phi::'a::domain=>'b::ring. \ -\ homo phi ==> EVAL2 phi a (monom b n) = phi b * a ^ n"; -by (stac monom_decomp 1); -by (asm_simp_tac (simpset() - addsimps [EVAL2_homo, EVAL2_const, EVAL2_monom]) 1); -qed "EVAL2_monom_n"; - -Goalw [thm "EVAL_def"] "!! a::'a::ring. homo (EVAL a)"; -by (asm_simp_tac (simpset() addsimps [EVAL2_homo]) 1); -qed "EVAL_homo"; - -Goalw [thm "EVAL_def"] "!! a::'a::ring. EVAL a (monom b 0) = b"; -by (asm_simp_tac (simpset() addsimps [EVAL2_const]) 1); -qed "EVAL_const"; - -Goalw [thm "EVAL_def"] "!! a::'a::domain. EVAL a (monom 1 n) = a ^ n"; -by (asm_simp_tac (simpset() addsimps [EVAL2_monom]) 1); -qed "EVAL_monom"; - -Goalw [thm "EVAL_def"] "!! a::'a::ring. EVAL a (b *s p) = b * EVAL a p"; -by (asm_simp_tac (simpset() addsimps [EVAL2_smult]) 1); -qed "EVAL_smult"; - -Goalw [thm "EVAL_def"] "!! a::'a::domain. EVAL a (monom b n) = b * a ^ n"; -by (asm_simp_tac (simpset() addsimps [EVAL2_monom_n]) 1); -qed "EVAL_monom_n"; - -(* Examples *) - -Goal - "EVAL (x::'a::domain) (a*X^2 + b*X^1 + c*X^0) = a * x ^ 2 + b * x ^ 1 + c"; -by (asm_simp_tac (simpset() delsimps [power_Suc] - addsimps [EVAL_homo, EVAL_monom, EVAL_monom_n]) 1); -result(); - -Goal - "EVAL (y::'a::domain) \ -\ (EVAL (monom x 0) (monom 1 1 + monom (a*X^2 + b*X^1 + c*X^0) 0)) = \ -\ x ^ 1 + (a * y ^ 2 + b * y ^ 1 + c)"; -by (asm_simp_tac (simpset() delsimps [power_Suc] - addsimps [EVAL_homo, EVAL_monom, EVAL_monom_n, EVAL_const]) 1); -result(); - diff -r 25ed0a4c7dc5 -r 6cdd0589aa73 src/HOL/Algebra/poly/PolyHomo.thy --- a/src/HOL/Algebra/poly/PolyHomo.thy Sun Nov 19 13:02:55 2006 +0100 +++ b/src/HOL/Algebra/poly/PolyHomo.thy Sun Nov 19 23:48:55 2006 +0100 @@ -6,13 +6,181 @@ theory PolyHomo imports UnivPoly2 begin -consts - EVAL2 :: "['a::ring => 'b, 'b, 'a up] => 'b::ring" - EVAL :: "['a::ring, 'a up] => 'a" +definition + EVAL2 :: "['a::ring => 'b, 'b, 'a up] => 'b::ring" where + "EVAL2 phi a p = setsum (%i. phi (coeff p i) * a ^ i) {..deg p}" + +definition + EVAL :: "['a::ring, 'a up] => 'a" where + "EVAL = EVAL2 (%x. x)" + +lemma SUM_shrink_lemma: + "!! f::(nat=>'a::ring). + m <= n & (ALL i. m < i & i <= n --> f i = 0) --> + setsum f {..m} = setsum f {..n}" + apply (induct_tac n) + (* Base case *) + apply (simp (no_asm)) + (* Induction step *) + apply (case_tac "m <= n") + apply auto + apply (subgoal_tac "m = Suc n") + apply (simp (no_asm_simp)) + apply arith + done + +lemma SUM_shrink: + "!! f::(nat=>'a::ring). + [| m <= n; !!i. [| m < i; i <= n |] ==> f i = 0; P (setsum f {..n}) |] + ==> P (setsum f {..m})" + apply (cut_tac m = m and n = n and f = f in SUM_shrink_lemma) + apply simp + done + +lemma SUM_extend: + "!! f::(nat=>'a::ring). + [| m <= n; !!i. [| m < i; i <= n |] ==> f i = 0; P (setsum f {..m}) |] + ==> P (setsum f {..n})" + apply (cut_tac m = m and n = n and f = f in SUM_shrink_lemma) + apply simp + done + +lemma DiagSum_lemma: + "!!f::nat=>'a::ring. j <= n + m --> + setsum (%k. setsum (%i. f i * g (k - i)) {..k}) {..j} = + setsum (%k. setsum (%i. f k * g i) {..j - k}) {..j}" + apply (induct_tac j) + (* Base case *) + apply (simp (no_asm)) + (* Induction step *) + apply (simp (no_asm) add: Suc_diff_le natsum_add) + apply (simp (no_asm_simp)) + done + +lemma DiagSum: + "!!f::nat=>'a::ring. + setsum (%k. setsum (%i. f i * g (k - i)) {..k}) {..n + m} = + setsum (%k. setsum (%i. f k * g i) {..n + m - k}) {..n + m}" + apply (rule DiagSum_lemma [THEN mp]) + apply (rule le_refl) + done + +lemma CauchySum: + "!! f::nat=>'a::ring. [| bound n f; bound m g|] ==> + setsum (%k. setsum (%i. f i * g (k-i)) {..k}) {..n + m} = + setsum f {..n} * setsum g {..m}" + apply (simp (no_asm) add: natsum_ldistr DiagSum) + (* SUM_rdistr must be applied after SUM_ldistr ! *) + apply (simp (no_asm) add: natsum_rdistr) + apply (rule_tac m = n and n = "n + m" in SUM_extend) + apply (rule le_add1) + apply force + apply (rule natsum_cong) + apply (rule refl) + apply (rule_tac m = m and n = "n +m - i" in SUM_shrink) + apply (simp (no_asm_simp) add: le_add_diff) + apply auto + done + +(* Evaluation homomorphism *) -defs - EVAL2_def: "EVAL2 phi a p == - setsum (%i. phi (coeff p i) * a ^ i) {..deg p}" - EVAL_def: "EVAL == EVAL2 (%x. x)" +lemma EVAL2_homo: + "!! phi::('a::ring=>'b::ring). homo phi ==> homo (EVAL2 phi a)" + apply (rule homoI) + apply (unfold EVAL2_def) + (* + commutes *) + (* degree estimations: + bound of all sums can be extended to max (deg aa) (deg b) *) + apply (rule_tac m = "deg (aa + b) " and n = "max (deg aa) (deg b)" in SUM_shrink) + apply (rule deg_add) + apply (simp (no_asm_simp) del: coeff_add add: deg_aboveD) + apply (rule_tac m = "deg aa" and n = "max (deg aa) (deg b)" in SUM_shrink) + apply (rule le_maxI1) + apply (simp (no_asm_simp) add: deg_aboveD) + apply (rule_tac m = "deg b" and n = "max (deg aa) (deg b) " in SUM_shrink) + apply (rule le_maxI2) + apply (simp (no_asm_simp) add: deg_aboveD) + (* actual homom property + *) + apply (simp (no_asm_simp) add: l_distr natsum_add) + + (* * commutes *) + apply (rule_tac m = "deg (aa * b) " and n = "deg aa + deg b" in SUM_shrink) + apply (rule deg_mult_ring) + apply (simp (no_asm_simp) del: coeff_mult add: deg_aboveD) + apply (rule trans) + apply (rule_tac [2] CauchySum) + prefer 2 + apply (simp add: boundI deg_aboveD) + prefer 2 + apply (simp add: boundI deg_aboveD) + (* getting a^i and a^(k-i) together is difficult, so we do it manually *) + apply (rule_tac s = "setsum (%k. setsum (%i. phi (coeff aa i) * (phi (coeff b (k - i)) * (a ^ i * a ^ (k - i)))) {..k}) {..deg aa + deg b}" in trans) + apply (simp (no_asm_simp) add: power_mult leD [THEN add_diff_inverse] natsum_ldistr) + apply (simp (no_asm)) + (* 1 commutes *) + apply (simp (no_asm_simp)) + done + +lemma EVAL2_const: + "!!phi::'a::ring=>'b::ring. EVAL2 phi a (monom b 0) = phi b" + by (simp add: EVAL2_def) + +lemma EVAL2_monom1: + "!! phi::'a::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom 1 1) = a" + by (simp add: EVAL2_def) + (* Must be able to distinguish 0 from 1, hence 'a::domain *) + +lemma EVAL2_monom: + "!! phi::'a::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom 1 n) = a ^ n" + apply (unfold EVAL2_def) + apply (simp (no_asm)) + apply (case_tac n) + apply auto + done + +lemma EVAL2_smult: + "!!phi::'a::ring=>'b::ring. + homo phi ==> EVAL2 phi a (b *s p) = phi b * EVAL2 phi a p" + by (simp (no_asm_simp) add: monom_mult_is_smult [symmetric] EVAL2_homo EVAL2_const) + +lemma monom_decomp: "monom (a::'a::ring) n = monom a 0 * monom 1 n" + apply (simp (no_asm) add: monom_mult_is_smult) + apply (rule up_eqI) + apply (simp (no_asm)) + done + +lemma EVAL2_monom_n: + "!! phi::'a::domain=>'b::ring. + homo phi ==> EVAL2 phi a (monom b n) = phi b * a ^ n" + apply (subst monom_decomp) + apply (simp (no_asm_simp) add: EVAL2_homo EVAL2_const EVAL2_monom) + done + +lemma EVAL_homo: "!!a::'a::ring. homo (EVAL a)" + by (simp add: EVAL_def EVAL2_homo) + +lemma EVAL_const: "!!a::'a::ring. EVAL a (monom b 0) = b" + by (simp add: EVAL_def EVAL2_const) + +lemma EVAL_monom: "!!a::'a::domain. EVAL a (monom 1 n) = a ^ n" + by (simp add: EVAL_def EVAL2_monom) + +lemma EVAL_smult: "!!a::'a::ring. EVAL a (b *s p) = b * EVAL a p" + by (simp add: EVAL_def EVAL2_smult) + +lemma EVAL_monom_n: "!!a::'a::domain. EVAL a (monom b n) = b * a ^ n" + by (simp add: EVAL_def EVAL2_monom_n) + + +(* Examples *) + +lemma "EVAL (x::'a::domain) (a*X^2 + b*X^1 + c*X^0) = a * x ^ 2 + b * x ^ 1 + c" + by (simp del: power_Suc add: EVAL_homo EVAL_monom EVAL_monom_n) + +lemma + "EVAL (y::'a::domain) + (EVAL (monom x 0) (monom 1 1 + monom (a*X^2 + b*X^1 + c*X^0) 0)) = + x ^ 1 + (a * y ^ 2 + b * y ^ 1 + c)" + by (simp del: power_Suc add: EVAL_homo EVAL_monom EVAL_monom_n EVAL_const) end diff -r 25ed0a4c7dc5 -r 6cdd0589aa73 src/HOL/Algebra/poly/UnivPoly2.ML --- a/src/HOL/Algebra/poly/UnivPoly2.ML Sun Nov 19 13:02:55 2006 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,359 +0,0 @@ -(* - Degree of polynomials - $Id$ - written by Clemens Ballarin, started 22 January 1997 -*) - -(* -(* Relating degree and bound *) - -Goal "[| bound m f; f n ~= 0 |] ==> n <= m"; -by (force_tac (claset() addDs [inst "m" "n" boundD], - simpset()) 1); -qed "below_bound"; - -goal UnivPoly2.thy "bound (LEAST n. bound n (Rep_UP p)) (Rep_UP p)"; -by (rtac exE 1); -by (rtac LeastI 2); -by (assume_tac 2); -by (res_inst_tac [("a", "Rep_UP p")] CollectD 1); -by (rtac (rewrite_rule [UP_def] Rep_UP) 1); -qed "Least_is_bound"; - -Goalw [coeff_def, deg_def] - "!! p. ALL m. n < m --> coeff m p = 0 ==> deg p <= n"; -by (rtac Least_le 1); -by (Fast_tac 1); -qed "deg_aboveI"; - -Goalw [coeff_def, deg_def] - "(n ~= 0 --> coeff n p ~= 0) ==> n <= deg p"; -by (case_tac "n = 0" 1); -(* Case n=0 *) -by (Asm_simp_tac 1); -(* Case n~=0 *) -by (rotate_tac 1 1); -by (Asm_full_simp_tac 1); -by (rtac below_bound 1); -by (assume_tac 2); -by (rtac Least_is_bound 1); -qed "deg_belowI"; - -Goalw [coeff_def, deg_def] - "deg p < m ==> coeff m p = 0"; -by (rtac exE 1); (* create !! x. *) -by (rtac boundD 2); -by (assume_tac 3); -by (rtac LeastI 2); -by (assume_tac 2); -by (res_inst_tac [("a", "Rep_UP p")] CollectD 1); -by (rtac (rewrite_rule [UP_def] Rep_UP) 1); -qed "deg_aboveD"; - -Goalw [deg_def] - "deg p = Suc y ==> ~ bound y (Rep_UP p)"; -by (rtac not_less_Least 1); -by (Asm_simp_tac 1); -val lemma1 = result(); - -Goalw [deg_def, coeff_def] - "deg p = Suc y ==> coeff (deg p) p ~= 0"; -by (rtac ccontr 1); -by (dtac notnotD 1); -by (cut_inst_tac [("p", "p")] Least_is_bound 1); -by (subgoal_tac "bound y (Rep_UP p)" 1); -(* prove subgoal *) -by (rtac boundI 2); -by (case_tac "Suc y < m" 2); -(* first case *) -by (rtac boundD 2); -by (assume_tac 2); -by (Asm_simp_tac 2); -(* second case *) -by (dtac leI 2); -by (dtac Suc_leI 2); -by (dtac le_anti_sym 2); -by (assume_tac 2); -by (Asm_full_simp_tac 2); -(* end prove subgoal *) -by (fold_goals_tac [deg_def]); -by (dtac lemma1 1); -by (etac notE 1); -by (assume_tac 1); -val lemma2 = result(); - -Goal "deg p ~= 0 ==> coeff (deg p) p ~= 0"; -by (rtac lemma2 1); -by (Full_simp_tac 1); -by (dtac Suc_pred 1); -by (rtac sym 1); -by (Asm_simp_tac 1); -qed "deg_lcoeff"; - -Goal "p ~= 0 ==> coeff (deg p) p ~= 0"; -by (etac contrapos_np 1); -by (case_tac "deg p = 0" 1); -by (blast_tac (claset() addSDs [deg_lcoeff]) 2); -by (rtac up_eqI 1); -by (case_tac "n=0" 1); -by (rotate_tac ~2 1); -by (Asm_full_simp_tac 1); -by (asm_full_simp_tac (simpset() addsimps [deg_aboveD]) 1); -qed "nonzero_lcoeff"; - -Goal "(deg p <= n) = bound n (Rep_UP p)"; -by (rtac iffI 1); -(* ==> *) -by (rtac boundI 1); -by (fold_goals_tac [coeff_def]); -by (rtac deg_aboveD 1); -by (fast_arith_tac 1); -(* <== *) -by (rtac deg_aboveI 1); -by (rewtac coeff_def); -by (Fast_tac 1); -qed "deg_above_is_bound"; - -(* Lemmas on the degree function *) - -Goalw [max_def] - "!! p::'a::ring up. deg (p + q) <= max (deg p) (deg q)"; -by (case_tac "deg p <= deg q" 1); -(* case deg p <= deg q *) -by (rtac deg_aboveI 1); -by (Asm_simp_tac 1); -by (strip_tac 1); -by (dtac le_less_trans 1); -by (assume_tac 1); -by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1); -(* case deg p > deg q *) -by (rtac deg_aboveI 1); -by (Asm_simp_tac 1); -by (dtac not_leE 1); -by (strip_tac 1); -by (dtac less_trans 1); -by (assume_tac 1); -by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1); -qed "deg_add"; - -Goal "!!p::('a::ring up). deg p < deg q ==> deg (p + q) = deg q"; -by (rtac order_antisym 1); -by (rtac le_trans 1); -by (rtac deg_add 1); -by (Asm_simp_tac 1); -by (rtac deg_belowI 1); -by (asm_simp_tac (simpset() addsimps [deg_aboveD, deg_lcoeff]) 1); -qed "deg_add_equal"; - -Goal "deg (monom m::'a::ring up) <= m"; -by (asm_simp_tac - (simpset() addsimps [deg_aboveI, less_not_refl2 RS not_sym]) 1); -qed "deg_monom_ring"; - -Goal "deg (monom m::'a::domain up) = m"; -by (rtac le_anti_sym 1); -(* <= *) -by (rtac deg_monom_ring 1); -(* >= *) -by (asm_simp_tac - (simpset() addsimps [deg_belowI, less_not_refl2 RS not_sym]) 1); -qed "deg_monom"; - -Goal "!! a::'a::ring. deg (const a) = 0"; -by (rtac le_anti_sym 1); -by (rtac deg_aboveI 1); -by (simp_tac (simpset() addsimps [less_not_refl2]) 1); -by (rtac deg_belowI 1); -by (simp_tac (simpset() addsimps [less_not_refl2]) 1); -qed "deg_const"; - -Goal "deg (0::'a::ringS up) = 0"; -by (rtac le_anti_sym 1); -by (rtac deg_aboveI 1); -by (Simp_tac 1); -by (rtac deg_belowI 1); -by (Simp_tac 1); -qed "deg_zero"; - -Goal "deg (<1>::'a::ring up) = 0"; -by (rtac le_anti_sym 1); -by (rtac deg_aboveI 1); -by (simp_tac (simpset() addsimps [less_not_refl2]) 1); -by (rtac deg_belowI 1); -by (Simp_tac 1); -qed "deg_one"; - -Goal "!!p::('a::ring) up. deg (-p) = deg p"; -by (rtac le_anti_sym 1); -(* <= *) -by (simp_tac (simpset() addsimps [deg_aboveI, deg_aboveD]) 1); -by (simp_tac (simpset() addsimps [deg_belowI, deg_lcoeff, uminus_monom_neq]) 1); -qed "deg_uminus"; - -Addsimps [deg_monom, deg_const, deg_zero, deg_one, deg_uminus]; - -Goal - "!! a::'a::ring. deg (a *s p) <= (if a = 0 then 0 else deg p)"; -by (case_tac "a = 0" 1); -by (REPEAT (asm_simp_tac (simpset() addsimps [deg_aboveI, deg_aboveD]) 1)); -qed "deg_smult_ring"; - -Goal - "!! a::'a::domain. deg (a *s p) = (if a = 0 then 0 else deg p)"; -by (rtac le_anti_sym 1); -by (rtac deg_smult_ring 1); -by (case_tac "a = 0" 1); -by (REPEAT (asm_simp_tac (simpset() addsimps [deg_belowI, deg_lcoeff]) 1)); -qed "deg_smult"; - -Goal - "!! p::'a::ring up. [| deg p + deg q < k |] ==> \ -\ coeff i p * coeff (k - i) q = 0"; -by (simp_tac (simpset() addsimps [coeff_def]) 1); -by (rtac bound_mult_zero 1); -by (assume_tac 3); -by (simp_tac (simpset() addsimps [deg_above_is_bound RS sym]) 1); -by (simp_tac (simpset() addsimps [deg_above_is_bound RS sym]) 1); -qed "deg_above_mult_zero"; - -Goal - "!! p::'a::ring up. deg (p * q) <= deg p + deg q"; -by (rtac deg_aboveI 1); -by (asm_simp_tac (simpset() addsimps [deg_above_mult_zero]) 1); -qed "deg_mult_ring"; - -goal Main.thy - "!!k::nat. k < n ==> m < n + m - k"; -by (arith_tac 1); -qed "less_add_diff"; - -Goal "!!p. coeff n p ~= 0 ==> n <= deg p"; -(* More general than deg_belowI, and simplifies the next proof! *) -by (rtac deg_belowI 1); -by (Fast_tac 1); -qed "deg_below2I"; - -Goal - "!! p::'a::domain up. \ -\ [| p ~= 0; q ~= 0 |] ==> deg (p * q) = deg p + deg q"; -by (rtac le_anti_sym 1); -by (rtac deg_mult_ring 1); -(* deg p + deg q <= deg (p * q) *) -by (rtac deg_below2I 1); -by (Simp_tac 1); -(* -by (rtac conjI 1); -by (rtac impI 1); -*) -by (res_inst_tac [("m", "deg p"), ("n", "deg p + deg q")] SUM_extend 1); -by (rtac le_add1 1); -by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1); -by (res_inst_tac [("m", "deg p"), ("n", "deg p")] SUM_extend_below 1); -by (rtac le_refl 1); -by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1); -by (asm_simp_tac (simpset() addsimps [nonzero_lcoeff]) 1); -(* -by (rtac impI 1); -by (res_inst_tac [("m", "deg p"), ("n", "deg p + deg q")] SUM_extend 1); -by (rtac le_add1 1); -by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1); -by (res_inst_tac [("m", "deg p"), ("n", "deg p")] SUM_extend_below 1); -by (rtac le_refl 1); -by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1); -by (asm_simp_tac (simpset() addsimps [nonzero_lcoeff]) 1); -*) -qed "deg_mult"; - -Addsimps [deg_smult, deg_mult]; - -(* Representation theorems about polynomials *) - -goal PolyRing.thy - "!! p::nat=>'a::ring up. \ -\ coeff k (setsum p {..n}) = setsum (%i. coeff k (p i)) {..n}"; -by (induct_tac "n" 1); -by Auto_tac; -qed "coeff_SUM"; - -goal UnivPoly2.thy - "!! f::(nat=>'a::ring). \ -\ bound n f ==> setsum (%i. if i = x then f i else 0) {..n} = f x"; -by (simp_tac (simpset() addsimps [SUM_if_singleton]) 1); -by (auto_tac - (claset() addDs [not_leE], - simpset())); -qed "bound_SUM_if"; - -Goal - "!! p::'a::ring up. deg p <= n ==> \ -\ setsum (%i. coeff i p *s monom i) {..n} = p"; -by (rtac up_eqI 1); -by (simp_tac (simpset() addsimps [coeff_SUM]) 1); -by (rtac trans 1); -by (res_inst_tac [("x", "na")] bound_SUM_if 2); -by (full_simp_tac (simpset() addsimps [deg_above_is_bound, coeff_def]) 2); -by (rtac SUM_cong 1); -by (rtac refl 1); -by (Asm_simp_tac 1); -qed "up_repr"; - -Goal - "!! p::'a::ring up. [| deg p <= n; P p |] ==> \ -\ P (setsum (%i. coeff i p *s monom i) {..n})"; -by (asm_simp_tac (simpset() addsimps [up_repr]) 1); -qed "up_reprD"; - -Goal - "!! p::'a::ring up. \ -\ [| deg p <= n; P (setsum (%i. coeff i p *s monom i) {..n}) |] \ -\ ==> P p"; -by (asm_full_simp_tac (simpset() addsimps [up_repr]) 1); -qed "up_repr2D"; - -(* -Goal - "!! p::'a::ring up. [| deg p <= n; deg q <= m |] ==> \ -\ (SUM n (%i. coeff i p *s monom i) = SUM m (%i. coeff i q *s monom i)) \ -\ = (coeff k f = coeff k g) -... -qed "up_unique"; -*) - -(* Polynomials over integral domains are again integral domains *) - -Goal "!!p::'a::domain up. p * q = 0 ==> p = 0 | q = 0"; -by (rtac classical 1); -by (subgoal_tac "deg p = 0 & deg q = 0" 1); -by (res_inst_tac [("p", "p"), ("n", "0")] up_repr2D 1); -by (Asm_simp_tac 1); -by (res_inst_tac [("p", "q"), ("n", "0")] up_repr2D 1); -by (Asm_simp_tac 1); -by (subgoal_tac "coeff 0 p = 0 | coeff 0 q = 0" 1); -by (force_tac (claset() addIs [up_eqI], simpset()) 1); -by (rtac integral 1); -by (subgoal_tac "coeff 0 (p * q) = 0" 1); -by (Asm_simp_tac 2); -by (Full_simp_tac 1); -by (dres_inst_tac [("f", "deg")] arg_cong 1); -by (Asm_full_simp_tac 1); -qed "up_integral"; - -Goal "!! a::'a::domain. a *s p = 0 ==> a = 0 | p = 0"; -by (full_simp_tac (simpset() addsimps [const_mult_is_smult RS sym]) 1); -by (dtac up_integral 1); -by Auto_tac; -by (rtac (const_inj RS injD) 1); -by (Simp_tac 1); -qed "smult_integral"; -*) - -(* Divisibility and degree *) - -Goalw [dvd_def] - "!! p::'a::domain up. [| p dvd q; q ~= 0 |] ==> deg p <= deg q"; -by (etac exE 1); -by (hyp_subst_tac 1); -by (case_tac "p = 0" 1); -by (case_tac "k = 0" 2); -by Auto_tac; -qed "dvd_imp_deg"; diff -r 25ed0a4c7dc5 -r 6cdd0589aa73 src/HOL/Algebra/poly/UnivPoly2.thy --- a/src/HOL/Algebra/poly/UnivPoly2.thy Sun Nov 19 13:02:55 2006 +0100 +++ b/src/HOL/Algebra/poly/UnivPoly2.thy Sun Nov 19 23:48:55 2006 +0100 @@ -11,29 +11,6 @@ imports "../abstract/Abstract" begin -(* already proved in Finite_Set.thy - -lemma setsum_cong: - "[| A = B; !!i. i : B ==> f i = g i |] ==> setsum f A = setsum g B" -proof - - assume prems: "A = B" "!!i. i : B ==> f i = g i" - show ?thesis - proof (cases "finite B") - case True - then have "!!A. [| A = B; !!i. i : B ==> f i = g i |] ==> - setsum f A = setsum g B" - proof induct - case empty thus ?case by simp - next - case insert thus ?case by simp - qed - with prems show ?thesis by simp - next - case False with prems show ?thesis by (simp add: setsum_def) - qed -qed -*) - (* With this variant of setsum_cong, assumptions like i:{m..n} get simplified (to m <= i & i <= n). *) @@ -41,21 +18,18 @@ section {* Definition of type up *} -constdefs - bound :: "[nat, nat => 'a::zero] => bool" - "bound n f == (ALL i. n < i --> f i = 0)" +definition + bound :: "[nat, nat => 'a::zero] => bool" where + "bound n f = (ALL i. n < i --> f i = 0)" lemma boundI [intro!]: "[| !! m. n < m ==> f m = 0 |] ==> bound n f" -proof (unfold bound_def) -qed fast + unfolding bound_def by blast lemma boundE [elim?]: "[| bound n f; (!! m. n < m ==> f m = 0) ==> P |] ==> P" -proof (unfold bound_def) -qed fast + unfolding bound_def by blast lemma boundD [dest]: "[| bound n f; n < m |] ==> f m = 0" -proof (unfold bound_def) -qed fast + unfolding bound_def by blast lemma bound_below: assumes bound: "bound m f" and nonzero: "f n ~= 0" shows "n <= m" @@ -67,20 +41,23 @@ qed typedef (UP) - ('a) up = "{f :: nat => 'a::zero. EX n. bound n f}" -by (rule+) (* Question: what does trace_rule show??? *) + ('a) up = "{f :: nat => 'a::zero. EX n. bound n f}" + by (rule+) (* Question: what does trace_rule show??? *) + section {* Constants *} -consts - coeff :: "['a up, nat] => ('a::zero)" - monom :: "['a::zero, nat] => 'a up" ("(3_*X^/_)" [71, 71] 70) - "*s" :: "['a::{zero, times}, 'a up] => 'a up" (infixl 70) +definition + coeff :: "['a up, nat] => ('a::zero)" where + "coeff p n = Rep_UP p n" -defs - coeff_def: "coeff p n == Rep_UP p n" - monom_def: "monom a n == Abs_UP (%i. if i=n then a else 0)" - smult_def: "a *s p == Abs_UP (%i. a * Rep_UP p i)" +definition + monom :: "['a::zero, nat] => 'a up" ("(3_*X^/_)" [71, 71] 70) where + "monom a n = Abs_UP (%i. if i=n then a else 0)" + +definition + smult :: "['a::{zero, times}, 'a up] => 'a up" (infixl "*s" 70) where + "a *s p = Abs_UP (%i. a * Rep_UP p i)" lemma coeff_bound_ex: "EX n. bound n (coeff p)" proof - @@ -97,6 +74,7 @@ with prem show P . qed + text {* Ring operations *} instance up :: (zero) zero .. @@ -124,6 +102,7 @@ up_power_def: "(a::'a::{one, times, power} up) ^ n == nat_rec 1 (%u b. b * a) n" + subsection {* Effect of operations on coefficients *} lemma coeff_monom [simp]: "coeff (monom a m) n = (if m=n then a else 0)" @@ -451,9 +430,9 @@ section {* The degree function *} -constdefs - deg :: "('a::zero) up => nat" - "deg p == LEAST n. bound n (coeff p)" +definition + deg :: "('a::zero) up => nat" where + "deg p = (LEAST n. bound n (coeff p))" lemma deg_aboveI: "(!!m. n < m ==> coeff p m = 0) ==> deg p <= n" @@ -773,4 +752,16 @@ "(a::'a::domain) *s p = 0 ==> a = 0 | p = 0" by (simp add: monom_mult_is_smult [THEN sym] integral_iff monom_inj_zero) + +(* Divisibility and degree *) + +lemma "!! p::'a::domain up. [| p dvd q; q ~= 0 |] ==> deg p <= deg q" + apply (unfold dvd_def) + apply (erule exE) + apply hypsubst + apply (case_tac "p = 0") + apply (case_tac [2] "k = 0") + apply auto + done + end diff -r 25ed0a4c7dc5 -r 6cdd0589aa73 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Sun Nov 19 13:02:55 2006 +0100 +++ b/src/HOL/IsaMakefile Sun Nov 19 23:48:55 2006 +0100 @@ -385,37 +385,19 @@ HOL-Algebra: HOL $(LOG)/HOL-Algebra.gz -$(LOG)/HOL-Algebra.gz: $(OUT)/HOL Algebra/ROOT.ML \ - Library/Primes.thy Library/FuncSet.thy \ - Algebra/AbelCoset.thy \ - Algebra/Bij.thy \ - Algebra/Coset.thy \ - Algebra/Exponent.thy \ - Algebra/FiniteProduct.thy \ - Algebra/Group.thy \ - Algebra/Ideal.thy \ - Algebra/Lattice.thy \ - Algebra/Module.thy \ - Algebra/Ring.thy \ - Algebra/Sylow.thy \ - Algebra/UnivPoly.thy \ - Algebra/IntRing.thy \ - Algebra/QuotRing.thy \ - Algebra/RingHom.thy \ - Algebra/abstract/Abstract.thy \ - Algebra/abstract/Factor.ML Algebra/abstract/Factor.thy \ - Algebra/abstract/Field.thy \ - Algebra/abstract/Ideal2.ML Algebra/abstract/Ideal2.thy \ - Algebra/abstract/PID.thy \ - Algebra/abstract/Ring2.ML Algebra/abstract/Ring2.thy \ - Algebra/abstract/RingHomo.ML Algebra/abstract/RingHomo.thy\ - Algebra/abstract/order.ML \ - Algebra/document/root.tex \ - Algebra/poly/LongDiv.ML Algebra/poly/LongDiv.thy \ - Algebra/poly/PolyHomo.ML Algebra/poly/PolyHomo.thy \ - Algebra/poly/Polynomial.thy \ - Algebra/poly/UnivPoly2.ML Algebra/poly/UnivPoly2.thy \ - Algebra/ringsimp.ML +$(LOG)/HOL-Algebra.gz: $(OUT)/HOL Algebra/ROOT.ML Library/Primes.thy \ + Library/FuncSet.thy Algebra/AbelCoset.thy Algebra/Bij.thy \ + Algebra/Coset.thy Algebra/Exponent.thy Algebra/FiniteProduct.thy \ + Algebra/Group.thy Algebra/Ideal.thy Algebra/IntRing.thy \ + Algebra/Lattice.thy Algebra/Module.thy Algebra/QuotRing.thy \ + Algebra/Ring.thy Algebra/RingHom.thy Algebra/Sylow.thy \ + Algebra/UnivPoly.thy Algebra/abstract/Abstract.thy \ + Algebra/abstract/Factor.thy Algebra/abstract/Field.thy \ + Algebra/abstract/Ideal2.thy Algebra/abstract/PID.thy \ + Algebra/abstract/Ring2.thy Algebra/abstract/RingHomo.thy \ + Algebra/document/root.tex Algebra/poly/LongDiv.thy \ + Algebra/poly/PolyHomo.thy Algebra/poly/Polynomial.thy \ + Algebra/poly/UnivPoly2.thy Algebra/ringsimp.ML @cd Algebra; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Algebra ## HOL-Auth