src/HOL/Algebra/abstract/Ideal2.ML
changeset 21416 f23e4e75dfd3
parent 20318 0e0ea63fe768
equal deleted inserted replaced
21415:39f98c88f88a 21416:f23e4e75dfd3
   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);