--- 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";
-
--- 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 \<longleftrightarrow>
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
--- 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";
-
--- 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 \<longleftrightarrow> (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 \<longleftrightarrow> (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
--- 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";
--- 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 \<equiv> \<exists>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
--- 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];
--- 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 \<longleftrightarrow> (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
--- 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
-*)
--- 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";
--- 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
-
--- 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();
-
--- 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
--- 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";
--- 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
--- 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