equal
deleted
inserted
replaced
122 qed "ideal_of_mono"; |
122 qed "ideal_of_mono"; |
123 |
123 |
124 Goal "ideal_of {0::'a::ring} = {0}"; |
124 Goal "ideal_of {0::'a::ring} = {0}"; |
125 by (simp_tac (simpset() addsimps [pideal_structure]) 1); |
125 by (simp_tac (simpset() addsimps [pideal_structure]) 1); |
126 by (rtac subset_antisym 1); |
126 by (rtac subset_antisym 1); |
127 by (auto_tac (claset() addIs [dvd_zero_left], simpset())); |
127 by (auto_tac (claset() addIs [thm "dvd_zero_left"], simpset())); |
128 qed "ideal_of_zero_eq"; |
128 qed "ideal_of_zero_eq"; |
129 |
129 |
130 Goal "[| is_ideal I; a : I |] ==> ideal_of {a::'a::ring} <= I"; |
130 Goal "[| is_ideal I; a : I |] ==> ideal_of {a::'a::ring} <= I"; |
131 by (auto_tac (claset(), |
131 by (auto_tac (claset(), |
132 simpset() addsimps [pideal_structure, is_ideal_dvd])); |
132 simpset() addsimps [pideal_structure, is_ideal_dvd])); |
147 qed "is_pidealD"; |
147 qed "is_pidealD"; |
148 |
148 |
149 (* Ideals and divisibility *) |
149 (* Ideals and divisibility *) |
150 |
150 |
151 Goal "b dvd a ==> ideal_of {a::'a::ring} <= ideal_of {b}"; |
151 Goal "b dvd a ==> ideal_of {a::'a::ring} <= ideal_of {b}"; |
152 by (auto_tac (claset() addIs [dvd_trans_ring], |
152 by (auto_tac (claset() addIs [thm "dvd_trans_ring"], |
153 simpset() addsimps [pideal_structure])); |
153 simpset() addsimps [pideal_structure])); |
154 qed "dvd_imp_subideal"; |
154 qed "dvd_imp_subideal"; |
155 |
155 |
156 Goal "ideal_of {a::'a::ring} <= ideal_of {b} ==> b dvd a"; |
156 Goal "ideal_of {a::'a::ring} <= ideal_of {b} ==> b dvd a"; |
157 by (auto_tac (claset() addSDs [subsetD], |
157 by (auto_tac (claset() addSDs [subsetD], |
165 |
165 |
166 Goal "(ideal_of {a::'a::ring} < ideal_of {b}) ==> ~ a dvd b"; |
166 Goal "(ideal_of {a::'a::ring} < ideal_of {b}) ==> ~ a dvd b"; |
167 by (full_simp_tac (simpset() addsimps [psubset_eq, pideal_structure]) 1); |
167 by (full_simp_tac (simpset() addsimps [psubset_eq, pideal_structure]) 1); |
168 by (etac conjE 1); |
168 by (etac conjE 1); |
169 by (dres_inst_tac [("c", "a")] subsetD 1); |
169 by (dres_inst_tac [("c", "a")] subsetD 1); |
170 by (auto_tac (claset() addIs [dvd_trans_ring], |
170 by (auto_tac (claset() addIs [thm "dvd_trans_ring"], |
171 simpset())); |
171 simpset())); |
172 qed "psubideal_not_dvd"; |
172 qed "psubideal_not_dvd"; |
173 |
173 |
174 Goal "[| b dvd a; ~ a dvd b |] ==> ideal_of {a::'a::ring} < ideal_of {b}"; |
174 Goal "[| b dvd a; ~ a dvd b |] ==> ideal_of {a::'a::ring} < ideal_of {b}"; |
175 by (rtac psubsetI 1); |
175 by (rtac psubsetI 1); |