--- a/src/HOL/NewNumberTheory/MiscAlgebra.thy Tue Jun 23 12:08:33 2009 +0200
+++ b/src/HOL/NewNumberTheory/MiscAlgebra.thy Tue Jun 23 12:08:34 2009 +0200
@@ -1,22 +1,15 @@
(* Title: MiscAlgebra.thy
- ID:
Author: Jeremy Avigad
- These are things that can be added to the Algebra library,
- as well as a few things that could possibly go in Main.
+These are things that can be added to the Algebra library.
*)
theory MiscAlgebra
-imports
+imports
"~~/src/HOL/Algebra/Ring"
"~~/src/HOL/Algebra/FiniteProduct"
begin;
-declare One_nat_def [simp del]
-
-
-(* Some things for Main? *)
-
(* finiteness stuff *)
lemma int_bounded_set1 [intro]: "finite {(x::int). a < x & x < b & P x}"
@@ -25,33 +18,9 @@
apply auto
done
-lemma image_set_eq_image: "{ f x | x. P x} = f ` { x. P x}"
- unfolding image_def apply auto
-done
-
-lemma finite_image_set [simp]: "finite {x. P x} \<Longrightarrow>
- finite { f x | x. P x}"
- apply (subst image_set_eq_image)
- apply auto
-done
-
-(* Examples:
-
-lemma "finite {x. 0 < x & x < 100 & prime (x::int)}"
- by auto
-
-lemma "finite { 3 * x | x. 0 < x & x < 100 & prime (x::int) }"
- by auto
-
-*)
(* The rest is for the algebra libraries *)
-(* This goes in FuncSet.thy. Any reason not to make it a simp rule? *)
-
-lemma funcset_id [simp]: "(%x. x): A \<rightarrow> A"
- by (auto simp add: Pi_def);
-
(* These go in Group.thy. *)
(*