# HG changeset patch # User haftmann # Date 1245751714 -7200 # Node ID a946fe9a0476d59440e9512fb81d14869920381c # Parent 1a92eb45060f198ce87db6217fb26d399e0d93e7 dropped duplicated lemmas, tuned header diff -r 1a92eb45060f -r a946fe9a0476 src/HOL/NewNumberTheory/MiscAlgebra.thy --- 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} \ - 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 \ A" - by (auto simp add: Pi_def); - (* These go in Group.thy. *) (*