--- a/src/HOL/Finite_Set.ML Thu Mar 25 10:31:25 2004 +0100
+++ b/src/HOL/Finite_Set.ML Thu Mar 25 10:32:21 2004 +0100
@@ -32,7 +32,6 @@
end;
val Diff1_foldSet = thm "Diff1_foldSet";
-val bounded_nat_set_is_finite = thm "bounded_nat_set_is_finite";
val cardR_SucD = thm "cardR_SucD";
val cardR_determ = thm "cardR_determ";
val cardR_emptyE = thm "cardR_emptyE";
@@ -83,7 +82,6 @@
val finite_UN_I = thm "finite_UN_I";
val finite_Un = thm "finite_Un";
val finite_UnI = thm "finite_UnI";
-val finite_atMost = thm "finite_atMost";
val finite_converse = thm "finite_converse";
val finite_empty_induct = thm "finite_empty_induct";
val finite_imageD = thm "finite_imageD";
@@ -92,7 +90,6 @@
val finite_imp_foldSet = thm "finite_imp_foldSet";
val finite_induct = thm "finite_induct";
val finite_insert = thm "finite_insert";
-val finite_lessThan = thm "finite_lessThan";
val finite_range_imageI = thm "finite_range_imageI";
val finite_subset = thm "finite_subset";
val finite_subset_induct = thm "finite_subset_induct";
--- a/src/HOL/Finite_Set.thy Thu Mar 25 10:31:25 2004 +0100
+++ b/src/HOL/Finite_Set.thy Thu Mar 25 10:32:21 2004 +0100
@@ -7,7 +7,7 @@
header {* Finite sets *}
-theory Finite_Set = Divides + Power + Inductive + SetInterval:
+theory Finite_Set = Divides + Power + Inductive:
subsection {* Types Classes @{text plus_ac0} and @{text times_ac1} *}
@@ -34,9 +34,9 @@
proof qed (rule add_commute add_assoc almost_semiring.add_0)+
axclass times_ac1 < times, one
- commute: "x * y = y * x"
- assoc: "(x * y) * z = x * (y * z)"
- one: "1 * x = x"
+ commute: "x * y = y * x"
+ assoc: "(x * y) * z = x * (y * z)"
+ one [simp]: "1 * x = x"
theorem times_ac1_left_commute: "(x::'a::times_ac1) * ((y::'a) * z) =
y * (x * z)"
@@ -50,7 +50,7 @@
finally show ?thesis .
qed
-theorem times_ac1_one_right: "(x::'a::times_ac1) * 1 = x"
+theorem times_ac1_one_right [simp]: "(x::'a::times_ac1) * 1 = x"
proof -
have "x * 1 = 1 * x"
by (rule times_ac1.commute)
@@ -347,38 +347,6 @@
done
-subsubsection {* Intervals of nats *}
-
-lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..k(}"
- by (induct k) (simp_all add: lessThan_Suc)
-
-lemma finite_atMost [iff]: fixes k :: nat shows "finite {..k}"
- by (induct k) (simp_all add: atMost_Suc)
-
-lemma finite_greaterThanLessThan [iff]:
- fixes l :: nat shows "finite {)l..u(}"
-by (simp add: greaterThanLessThan_def)
-
-lemma finite_atLeastLessThan [iff]:
- fixes l :: nat shows "finite {l..u(}"
-by (simp add: atLeastLessThan_def)
-
-lemma finite_greaterThanAtMost [iff]:
- fixes l :: nat shows "finite {)l..u}"
-by (simp add: greaterThanAtMost_def)
-
-lemma finite_atLeastAtMost [iff]:
- fixes l :: nat shows "finite {l..u}"
-by (simp add: atLeastAtMost_def)
-
-lemma bounded_nat_set_is_finite:
- "(ALL i:N. i < (n::nat)) ==> finite N"
- -- {* A bounded set of natural numbers is finite. *}
- apply (rule finite_subset)
- apply (rule_tac [2] finite_lessThan, auto)
- done
-
-
subsubsection {* Finiteness of transitive closure *}
text {* (Thanks to Sidi Ehmety) *}
@@ -849,63 +817,24 @@
by (simp add: setsum_def
LC.fold_insert [OF LC.intro] plus_ac0_left_commute)
-lemma setsum_0: "setsum (\<lambda>i. 0) A = 0"
- apply (case_tac "finite A")
- prefer 2 apply (simp add: setsum_def)
- apply (erule finite_induct, auto)
- done
-
-lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
- apply (case_tac "finite A")
- prefer 2 apply (simp add: setsum_def)
- apply (erule rev_mp)
- apply (erule finite_induct, auto)
- done
-
-lemma card_eq_setsum: "finite A ==> card A = setsum (\<lambda>x. 1) A"
- -- {* Could allow many @{text "card"} proofs to be simplified. *}
- by (induct set: Finites) auto
-
-lemma setsum_Un_Int: "finite A ==> finite B
- ==> setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
- -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
- apply (induct set: Finites, simp)
- apply (simp add: plus_ac0 Int_insert_left insert_absorb)
- done
-
-lemma setsum_Un_disjoint: "finite A ==> finite B
- ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
- apply (subst setsum_Un_Int [symmetric], auto)
+lemma setsum_reindex [rule_format]: "finite B ==>
+ inj_on f B --> setsum h (f ` B) = setsum (h \<circ> f) B"
+apply (rule finite_induct, assumption, force)
+apply (rule impI, auto)
+apply (simp add: inj_on_def)
+apply (subgoal_tac "f x \<notin> f ` F")
+apply (subgoal_tac "finite (f ` F)")
+apply (auto simp add: setsum_insert)
+apply (simp add: inj_on_def)
done
-lemma setsum_UN_disjoint:
- fixes f :: "'a => 'b::plus_ac0"
- shows
- "finite I ==> (ALL i:I. finite (A i)) ==>
- (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
- setsum f (UNION I A) = setsum (\<lambda>i. setsum f (A i)) I"
- apply (induct set: Finites, simp, atomize)
- apply (subgoal_tac "ALL i:F. x \<noteq> i")
- prefer 2 apply blast
- apply (subgoal_tac "A x Int UNION F A = {}")
- prefer 2 apply blast
- apply (simp add: setsum_Un_disjoint)
- done
+lemma setsum_reindex_id: "finite B ==> inj_on f B ==>
+ setsum f B = setsum id (f ` B)"
+by (auto simp add: setsum_reindex id_o)
-lemma setsum_Union_disjoint:
- "finite C ==> (ALL A:C. finite A) ==>
- (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
- setsum f (Union C) = setsum (setsum f) C"
- apply (frule setsum_UN_disjoint [of C id f])
- apply (unfold Union_def id_def, assumption+)
- done
-
-lemma setsum_addf: "setsum (\<lambda>x. f x + g x) A = (setsum f A + setsum g A)"
- apply (case_tac "finite A")
- prefer 2 apply (simp add: setsum_def)
- apply (erule finite_induct, auto)
- apply (simp add: plus_ac0)
- done
+lemma setsum_reindex_cong: "finite A ==> inj_on f A ==>
+ B = f ` A ==> g = h \<circ> f ==> setsum h B = setsum g A"
+ by (frule setsum_reindex, assumption, simp)
lemma setsum_cong:
"A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
@@ -925,28 +854,10 @@
apply (simp add: Ball_def del:insert_Diff_single)
done
-lemma card_UN_disjoint:
- fixes f :: "'a => 'b::plus_ac0"
- shows
- "finite I ==> (ALL i:I. finite (A i)) ==>
- (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
- card (UNION I A) = setsum (\<lambda>i. card (A i)) I"
- apply (subst card_eq_setsum)
- apply (subst finite_UN, assumption+)
- apply (subgoal_tac "setsum (\<lambda>i. card (A i)) I =
- setsum (%i. (setsum (%x. 1) (A i))) I")
- apply (erule ssubst)
- apply (erule setsum_UN_disjoint, assumption+)
- apply (rule setsum_cong)
- apply (simp, simp add: card_eq_setsum)
- done
-
-lemma card_Union_disjoint:
- "finite C ==> (ALL A:C. finite A) ==>
- (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
- card (Union C) = setsum card C"
- apply (frule card_UN_disjoint [of C id])
- apply (unfold Union_def id_def, assumption+)
+lemma setsum_0: "setsum (%i. 0) A = 0"
+ apply (case_tac "finite A")
+ prefer 2 apply (simp add: setsum_def)
+ apply (erule finite_induct, auto)
done
lemma setsum_0': "ALL a:F. f a = 0 ==> setsum f F = 0"
@@ -955,32 +866,85 @@
apply (rule setsum_cong, auto)
done
+lemma card_eq_setsum: "finite A ==> card A = setsum (%x. 1) A"
+ -- {* Could allow many @{text "card"} proofs to be simplified. *}
+ by (induct set: Finites) auto
-subsubsection {* Reindexing sums *}
+lemma setsum_Un_Int: "finite A ==> finite B
+ ==> setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
+ -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
+ apply (induct set: Finites, simp)
+ apply (simp add: plus_ac0 Int_insert_left insert_absorb)
+ done
+
+lemma setsum_Un_disjoint: "finite A ==> finite B
+ ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
+ apply (subst setsum_Un_Int [symmetric], auto)
+ done
-lemma setsum_reindex [rule_format]: "finite B ==>
- inj_on f B --> setsum h (f ` B) = setsum (h \<circ> f) B"
-apply (rule finite_induct, assumption, force)
-apply (rule impI, auto)
-apply (simp add: inj_on_def)
-apply (subgoal_tac "f x \<notin> f ` F")
-apply (subgoal_tac "finite (f ` F)")
-apply (auto simp add: setsum_insert)
-apply (simp add: inj_on_def)
+lemma setsum_UN_disjoint:
+ "finite I ==> (ALL i:I. finite (A i)) ==>
+ (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
+ setsum f (UNION I A) = setsum (%i. setsum f (A i)) I"
+ apply (induct set: Finites, simp, atomize)
+ apply (subgoal_tac "ALL i:F. x \<noteq> i")
+ prefer 2 apply blast
+ apply (subgoal_tac "A x Int UNION F A = {}")
+ prefer 2 apply blast
+ apply (simp add: setsum_Un_disjoint)
+ done
+
+lemma setsum_Union_disjoint:
+ "finite C ==> (ALL A:C. finite A) ==>
+ (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
+ setsum f (Union C) = setsum (setsum f) C"
+ apply (frule setsum_UN_disjoint [of C id f])
+ apply (unfold Union_def id_def, assumption+)
done
-lemma setsum_reindex_id: "finite B ==> inj_on f B ==>
- setsum f B = setsum id (f ` B)"
-by (auto simp add: setsum_reindex id_o)
+lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
+ (\<Sum> x:A. (\<Sum> y:B x. f x y)) =
+ (\<Sum> z:(SIGMA x:A. B x). f (fst z) (snd z))"
+ apply (subst Sigma_def)
+ apply (subst setsum_UN_disjoint)
+ apply assumption
+ apply (rule ballI)
+ apply (drule_tac x = i in bspec, assumption)
+ apply (subgoal_tac "(UN y:(B i). {(i, y)}) <= (%y. (i, y)) ` (B i)")
+ apply (rule finite_surj)
+ apply auto
+ apply (rule setsum_cong, rule refl)
+ apply (subst setsum_UN_disjoint)
+ apply (erule bspec, assumption)
+ apply auto
+ done
+lemma setsum_cartesian_product: "finite A ==> finite B ==>
+ (\<Sum> x:A. (\<Sum> y:B. f x y)) =
+ (\<Sum> z:A <*> B. f (fst z) (snd z))"
+ by (erule setsum_Sigma, auto);
+
+lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
+ apply (case_tac "finite A")
+ prefer 2 apply (simp add: setsum_def)
+ apply (erule finite_induct, auto)
+ apply (simp add: plus_ac0)
+ done
subsubsection {* Properties in more restricted classes of structures *}
+lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
+ apply (case_tac "finite A")
+ prefer 2 apply (simp add: setsum_def)
+ apply (erule rev_mp)
+ apply (erule finite_induct, auto)
+ done
+
lemma setsum_eq_0_iff [simp]:
"finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
by (induct set: Finites) auto
-lemma setsum_constant_nat:
+lemma setsum_constant_nat [simp]:
"finite A ==> (\<Sum>x: A. y) = (card A) * y"
-- {* Later generalized to any semiring. *}
by (erule finite_induct, auto)
@@ -1022,13 +986,35 @@
apply (blast intro: add_mono)
done
-subsubsection {* Cardinality of Sigma and Cartesian product *}
+subsubsection {* Cardinality of unions and Sigma sets *}
+
+lemma card_UN_disjoint:
+ "finite I ==> (ALL i:I. finite (A i)) ==>
+ (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
+ card (UNION I A) = setsum (%i. card (A i)) I"
+ apply (subst card_eq_setsum)
+ apply (subst finite_UN, assumption+)
+ apply (subgoal_tac "setsum (%i. card (A i)) I =
+ setsum (%i. (setsum (%x. 1) (A i))) I")
+ apply (erule ssubst)
+ apply (erule setsum_UN_disjoint, assumption+)
+ apply (rule setsum_cong)
+ apply simp+
+ done
+
+lemma card_Union_disjoint:
+ "finite C ==> (ALL A:C. finite A) ==>
+ (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
+ card (Union C) = setsum card C"
+ apply (frule card_UN_disjoint [of C id])
+ apply (unfold Union_def id_def, assumption+)
+ done
lemma SigmaI_insert: "y \<notin> A ==>
(SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
by auto
-lemma card_cartesian_product_singleton [simp]: "finite A ==>
+lemma card_cartesian_product_singleton: "finite A ==>
card({x} <*> A) = card(A)"
apply (subgoal_tac "inj_on (%y .(x,y)) A")
apply (frule card_image, assumption)
@@ -1042,14 +1028,12 @@
apply (erule finite_induct, auto)
apply (subst SigmaI_insert, assumption)
apply (subst card_Un_disjoint)
- apply (auto intro: finite_SigmaI)
+ apply (auto intro: finite_SigmaI simp add: card_cartesian_product_singleton)
done
-lemma card_cartesian_product [simp]: "[| finite A; finite B |] ==>
+lemma card_cartesian_product: "[| finite A; finite B |] ==>
card (A <*> B) = card(A) * card(B)"
- apply (subst card_SigmaI, assumption+)
- apply (simp add: setsum_constant_nat)
- done
+ by simp
subsection {* Generalized product over a set *}
@@ -1077,54 +1061,24 @@
by (auto simp add: setprod_def LC_def LC.fold_insert
times_ac1_left_commute)
-lemma setprod_1: "setprod (\<lambda>i. 1) A = 1"
- apply (case_tac "finite A")
- apply (erule finite_induct, auto simp add: times_ac1)
- apply (simp add: setprod_def)
- done
-
-lemma setprod_Un_Int: "finite A ==> finite B
- ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
- apply (induct set: Finites, simp)
- apply (simp add: times_ac1 insert_absorb)
- apply (simp add: times_ac1 Int_insert_left insert_absorb)
- done
-
-lemma setprod_Un_disjoint: "finite A ==> finite B
- ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
- apply (subst setprod_Un_Int [symmetric], auto simp add: times_ac1)
+lemma setprod_reindex [rule_format]: "finite B ==>
+ inj_on f B --> setprod h (f ` B) = setprod (h \<circ> f) B"
+apply (rule finite_induct, assumption, force)
+apply (rule impI, auto)
+apply (simp add: inj_on_def)
+apply (subgoal_tac "f x \<notin> f ` F")
+apply (subgoal_tac "finite (f ` F)")
+apply (auto simp add: setprod_insert)
+apply (simp add: inj_on_def)
done
-lemma setprod_UN_disjoint:
- fixes f :: "'a => 'b::times_ac1"
- shows
- "finite I ==> (ALL i:I. finite (A i)) ==>
- (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
- setprod f (UNION I A) = setprod (\<lambda>i. setprod f (A i)) I"
- apply (induct set: Finites, simp, atomize)
- apply (subgoal_tac "ALL i:F. x \<noteq> i")
- prefer 2 apply blast
- apply (subgoal_tac "A x Int UNION F A = {}")
- prefer 2 apply blast
- apply (simp add: setprod_Un_disjoint)
- done
+lemma setprod_reindex_id: "finite B ==> inj_on f B ==>
+ setprod f B = setprod id (f ` B)"
+by (auto simp add: setprod_reindex id_o)
-lemma setprod_Union_disjoint:
- "finite C ==> (ALL A:C. finite A) ==>
- (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
- setprod f (Union C) = setprod (setprod f) C"
- apply (frule setprod_UN_disjoint [of C id f])
- apply (unfold Union_def id_def, assumption+)
- done
-
-lemma setprod_timesf: "setprod (\<lambda>x. f x * g x) A =
- (setprod f A * setprod g A)"
- apply (case_tac "finite A")
- prefer 2 apply (simp add: setprod_def times_ac1)
- apply (erule finite_induct, auto)
- apply (simp add: times_ac1)
- apply (simp add: times_ac1)
- done
+lemma setprod_reindex_cong: "finite A ==> inj_on f A ==>
+ B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
+ by (frule setprod_reindex, assumption, simp)
lemma setprod_cong:
"A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
@@ -1144,30 +1098,79 @@
apply (simp add: Ball_def del:insert_Diff_single)
done
+lemma setprod_1: "setprod (%i. 1) A = 1"
+ apply (case_tac "finite A")
+ apply (erule finite_induct, auto simp add: times_ac1)
+ apply (simp add: setprod_def)
+ done
+
lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1"
apply (subgoal_tac "setprod f F = setprod (%x. 1) F")
apply (erule ssubst, rule setprod_1)
apply (rule setprod_cong, auto)
done
-
-subsubsection {* Reindexing products *}
+lemma setprod_Un_Int: "finite A ==> finite B
+ ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
+ apply (induct set: Finites, simp)
+ apply (simp add: times_ac1 insert_absorb)
+ apply (simp add: times_ac1 Int_insert_left insert_absorb)
+ done
-lemma setprod_reindex [rule_format]: "finite B ==>
- inj_on f B --> setprod h (f ` B) = setprod (h \<circ> f) B"
-apply (rule finite_induct, assumption, force)
-apply (rule impI, auto)
-apply (simp add: inj_on_def)
-apply (subgoal_tac "f x \<notin> f ` F")
-apply (subgoal_tac "finite (f ` F)")
-apply (auto simp add: setprod_insert)
-apply (simp add: inj_on_def)
+lemma setprod_Un_disjoint: "finite A ==> finite B
+ ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
+ apply (subst setprod_Un_Int [symmetric], auto simp add: times_ac1)
+ done
+
+lemma setprod_UN_disjoint:
+ "finite I ==> (ALL i:I. finite (A i)) ==>
+ (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
+ setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
+ apply (induct set: Finites, simp, atomize)
+ apply (subgoal_tac "ALL i:F. x \<noteq> i")
+ prefer 2 apply blast
+ apply (subgoal_tac "A x Int UNION F A = {}")
+ prefer 2 apply blast
+ apply (simp add: setprod_Un_disjoint)
done
-lemma setprod_reindex_id: "finite B ==> inj_on f B ==>
- setprod f B = setprod id (f ` B)"
-by (auto simp add: setprod_reindex id_o)
+lemma setprod_Union_disjoint:
+ "finite C ==> (ALL A:C. finite A) ==>
+ (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
+ setprod f (Union C) = setprod (setprod f) C"
+ apply (frule setprod_UN_disjoint [of C id f])
+ apply (unfold Union_def id_def, assumption+)
+ done
+lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
+ (\<Prod> x:A. (\<Prod> y: B x. f x y)) =
+ (\<Prod> z:(SIGMA x:A. B x). f (fst z) (snd z))"
+ apply (subst Sigma_def)
+ apply (subst setprod_UN_disjoint)
+ apply assumption
+ apply (rule ballI)
+ apply (drule_tac x = i in bspec, assumption)
+ apply (subgoal_tac "(UN y:(B i). {(i, y)}) <= (%y. (i, y)) ` (B i)")
+ apply (rule finite_surj)
+ apply auto
+ apply (rule setprod_cong, rule refl)
+ apply (subst setprod_UN_disjoint)
+ apply (erule bspec, assumption)
+ apply auto
+ done
+
+lemma setprod_cartesian_product: "finite A ==> finite B ==>
+ (\<Prod> x:A. (\<Prod> y: B. f x y)) =
+ (\<Prod> z:(A <*> B). f (fst z) (snd z))"
+ by (erule setprod_Sigma, auto)
+
+lemma setprod_timesf: "setprod (%x. f x * g x) A =
+ (setprod f A * setprod g A)"
+ apply (case_tac "finite A")
+ prefer 2 apply (simp add: setprod_def times_ac1)
+ apply (erule finite_induct, auto)
+ apply (simp add: times_ac1)
+ done
subsubsection {* Properties in more restricted classes of structures *}
--- a/src/HOL/Infinite_Set.thy Thu Mar 25 10:31:25 2004 +0100
+++ b/src/HOL/Infinite_Set.thy Thu Mar 25 10:32:21 2004 +0100
@@ -5,7 +5,7 @@
header {* Infnite Sets and Related Concepts*}
-theory Infinite_Set = Hilbert_Choice + Finite_Set:
+theory Infinite_Set = Hilbert_Choice + Finite_Set + SetInterval:
subsection "Infinite Sets"
--- a/src/HOL/Integ/IntDef.thy Thu Mar 25 10:31:25 2004 +0100
+++ b/src/HOL/Integ/IntDef.thy Thu Mar 25 10:32:21 2004 +0100
@@ -37,7 +37,7 @@
One_int_def: "1 == int 1"
minus_int_def:
- "- z == contents (\<Union>(x,y) \<in> Rep_Integ(z). { Abs_Integ(intrel``{(y,x)}) })"
+ "- z == contents (\<Union>(x,y) \<in> Rep_Integ(z). { Abs_Integ(intrel``{(y,x)}) })"
add_int_def:
"z + w ==
@@ -82,13 +82,8 @@
declare inj_on_Abs_Integ [THEN inj_on_iff, simp]
Abs_Integ_inverse [simp]
-lemma inj_Rep_Integ: "inj(Rep_Integ)"
-apply (rule inj_on_inverseI)
-apply (rule Rep_Integ_inverse)
-done
-
text{*Case analysis on the representation of an integer as an equivalence
- class.*}
+ class of pairs of naturals.*}
lemma eq_Abs_Integ [case_names Abs_Integ, cases type: int]:
"(!!x y. z = Abs_Integ(intrel``{(x,y)}) ==> P) ==> P"
apply (rule Rep_Integ [of z, unfolded Integ_def, THEN quotientE])
@@ -952,7 +947,6 @@
val equiv_intrel_iff = thm "equiv_intrel_iff";
val intrel_in_integ = thm "intrel_in_integ";
val inj_on_Abs_Integ = thm "inj_on_Abs_Integ";
-val inj_Rep_Integ = thm "inj_Rep_Integ";
val inj_int = thm "inj_int";
val zminus_zminus = thm "zminus_zminus";
val zminus_0 = thm "zminus_0";
--- a/src/HOL/Integ/Presburger.thy Thu Mar 25 10:31:25 2004 +0100
+++ b/src/HOL/Integ/Presburger.thy Thu Mar 25 10:32:21 2004 +0100
@@ -7,7 +7,7 @@
generation for Cooper Algorithm
*)
-theory Presburger = NatSimprocs
+theory Presburger = NatSimprocs + SetInterval
files
("cooper_dec.ML")
("cooper_proof.ML")
--- a/src/HOL/NumberTheory/Euler.thy Thu Mar 25 10:31:25 2004 +0100
+++ b/src/HOL/NumberTheory/Euler.thy Thu Mar 25 10:32:21 2004 +0100
@@ -138,7 +138,7 @@
also have "... = int(setsum (%x.2) (SetS a p))";
apply (insert prems)
apply (auto simp add: SetS_elems_card SetS_finite SetS_elems_finite
- card_setsum_aux)
+ card_setsum_aux simp del: setsum_constant_nat)
done
also have "... = 2 * int(card( SetS a p))";
by (auto simp add: prems SetS_finite setsum_const2)
@@ -342,4 +342,4 @@
apply (frule Euler_part1, auto simp add: zcong_sym)
done
-end;
\ No newline at end of file
+end
\ No newline at end of file
--- a/src/HOL/NumberTheory/Finite2.thy Thu Mar 25 10:31:25 2004 +0100
+++ b/src/HOL/NumberTheory/Finite2.thy Thu Mar 25 10:32:21 2004 +0100
@@ -342,7 +342,7 @@
apply (subgoal_tac "(\<Sum>x \<in> UNION A g. 1) = (\<Sum>x \<in> A. \<Sum>x \<in> g x. 1)");
apply (auto simp only: card_eq_setsum)
apply (erule setsum_same_function)
-by (auto simp add: card_eq_setsum)
+by auto;
lemma int_card_indexed_union_disjoint_sets [rule_format]: "finite A ==>
((\<forall>x \<in> A. finite (g x)) &
--- a/src/HOL/Presburger.thy Thu Mar 25 10:31:25 2004 +0100
+++ b/src/HOL/Presburger.thy Thu Mar 25 10:32:21 2004 +0100
@@ -7,7 +7,7 @@
generation for Cooper Algorithm
*)
-theory Presburger = NatSimprocs
+theory Presburger = NatSimprocs + SetInterval
files
("cooper_dec.ML")
("cooper_proof.ML")
--- a/src/HOL/SetInterval.ML Thu Mar 25 10:31:25 2004 +0100
+++ b/src/HOL/SetInterval.ML Thu Mar 25 10:32:21 2004 +0100
@@ -49,3 +49,7 @@
val lessThan_def = thm "lessThan_def";
val lessThan_iff = thm "lessThan_iff";
val single_Diff_lessThan = thm "single_Diff_lessThan";
+
+val bounded_nat_set_is_finite = thm "bounded_nat_set_is_finite";
+val finite_atMost = thm "finite_atMost";
+val finite_lessThan = thm "finite_lessThan";
--- a/src/HOL/SetInterval.thy Thu Mar 25 10:31:25 2004 +0100
+++ b/src/HOL/SetInterval.thy Thu Mar 25 10:32:21 2004 +0100
@@ -1,12 +1,13 @@
(* Title: HOL/SetInterval.thy
ID: $Id$
Author: Tobias Nipkow and Clemens Ballarin
+ Additions by Jeremy Avigad in March 2004
Copyright 2000 TU Muenchen
lessThan, greaterThan, atLeast, atMost and two-sided intervals
*)
-theory SetInterval = NatArith:
+theory SetInterval = IntArith:
constdefs
lessThan :: "('a::ord) => 'a set" ("(1{.._'(})")
@@ -58,23 +59,11 @@
"INT i<n. A" == "INT i:{..n(}. A"
-subsection {*lessThan*}
+subsection {* Various equivalences *}
lemma lessThan_iff [iff]: "(i: lessThan k) = (i<k)"
by (simp add: lessThan_def)
-lemma lessThan_0 [simp]: "lessThan (0::nat) = {}"
-by (simp add: lessThan_def)
-
-lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)"
-by (simp add: lessThan_def less_Suc_eq, blast)
-
-lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k"
-by (simp add: lessThan_def atMost_def less_Suc_eq_le)
-
-lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV"
-by blast
-
lemma Compl_lessThan [simp]:
"!!k:: 'a::linorder. -lessThan k = atLeast k"
apply (auto simp add: lessThan_def atLeast_def)
@@ -83,24 +72,9 @@
lemma single_Diff_lessThan [simp]: "!!k:: 'a::order. {k} - lessThan k = {k}"
by auto
-subsection {*greaterThan*}
-
lemma greaterThan_iff [iff]: "(i: greaterThan k) = (k<i)"
by (simp add: greaterThan_def)
-lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc"
-apply (simp add: greaterThan_def)
-apply (blast dest: gr0_conv_Suc [THEN iffD1])
-done
-
-lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}"
-apply (simp add: greaterThan_def)
-apply (auto elim: linorder_neqE)
-done
-
-lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}"
-by blast
-
lemma Compl_greaterThan [simp]:
"!!k:: 'a::linorder. -greaterThan k = atMost k"
apply (simp add: greaterThan_def atMost_def le_def, auto)
@@ -111,48 +85,22 @@
apply (rule double_complement)
done
-
-subsection {*atLeast*}
-
lemma atLeast_iff [iff]: "(i: atLeast k) = (k<=i)"
by (simp add: atLeast_def)
-lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV"
-by (unfold atLeast_def UNIV_def, simp)
-
-lemma atLeast_Suc: "atLeast (Suc k) = atLeast k - {k}"
-apply (simp add: atLeast_def)
-apply (simp add: Suc_le_eq)
-apply (simp add: order_le_less, blast)
-done
-
-lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV"
-by blast
-
lemma Compl_atLeast [simp]:
"!!k:: 'a::linorder. -atLeast k = lessThan k"
apply (simp add: lessThan_def atLeast_def le_def, auto)
done
-
-subsection {*atMost*}
-
lemma atMost_iff [iff]: "(i: atMost k) = (i<=k)"
by (simp add: atMost_def)
-lemma atMost_0 [simp]: "atMost (0::nat) = {0}"
-by (simp add: atMost_def)
-
-lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)"
-apply (simp add: atMost_def)
-apply (simp add: less_Suc_eq order_le_less, blast)
-done
-
-lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"
-by blast
+lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}"
+by (blast intro: order_antisym)
-subsection {*Logical Equivalences for Set Inclusion and Equality*}
+subsection {* Logical Equivalences for Set Inclusion and Equality *}
lemma atLeast_subset_iff [iff]:
"(atLeast x \<subseteq> atLeast y) = (y \<le> (x::'a::order))"
@@ -195,11 +143,6 @@
done
-subsection {*Combined properties*}
-
-lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}"
-by (blast intro: order_antisym)
-
subsection {*Two-sided intervals*}
(* greaterThanLessThan *)
@@ -208,25 +151,12 @@
"(i : {)l..u(}) = (l < i & i < u)"
by (simp add: greaterThanLessThan_def)
-lemma greaterThanLessThan_0 [simp]: "{)l..0::nat(} == {}"
-by (simp add: greaterThanLessThan_def)
-
-lemma greaterThanLessThan_Suc_greaterThanAtMost:
- "{)l..Suc n(} = {)l..n}"
-by (auto simp add: greaterThanLessThan_def greaterThanAtMost_def)
-
(* atLeastLessThan *)
lemma atLeastLessThan_iff [simp]:
"(i : {l..u(}) = (l <= i & i < u)"
by (simp add: atLeastLessThan_def)
-lemma atLeastLessThan_0 [simp]: "{l..0::nat(} == {}"
-by (simp add: atLeastLessThan_def)
-
-lemma atLeastLessThan_Suc_atLeastAtMost: "{l..Suc n(} = {l..n}"
-by (auto simp add: atLeastLessThan_def atLeastAtMost_def)
-
(* greaterThanAtMost *)
lemma greaterThanAtMost_iff [simp]:
@@ -239,11 +169,226 @@
"(i : {l..u}) = (l <= i & i <= u)"
by (simp add: atLeastAtMost_def)
-
(* The above four lemmas could be declared as iffs.
If we do so, a call to blast in Hyperreal/Star.ML, lemma STAR_Int
seems to take forever (more than one hour). *)
+
+subsection {* Intervals of natural numbers *}
+
+lemma lessThan_0 [simp]: "lessThan (0::nat) = {}"
+by (simp add: lessThan_def)
+
+lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)"
+by (simp add: lessThan_def less_Suc_eq, blast)
+
+lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k"
+by (simp add: lessThan_def atMost_def less_Suc_eq_le)
+
+lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV"
+by blast
+
+lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc"
+apply (simp add: greaterThan_def)
+apply (blast dest: gr0_conv_Suc [THEN iffD1])
+done
+
+lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}"
+apply (simp add: greaterThan_def)
+apply (auto elim: linorder_neqE)
+done
+
+lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}"
+by blast
+
+lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV"
+by (unfold atLeast_def UNIV_def, simp)
+
+lemma atLeast_Suc: "atLeast (Suc k) = atLeast k - {k}"
+apply (simp add: atLeast_def)
+apply (simp add: Suc_le_eq)
+apply (simp add: order_le_less, blast)
+done
+
+lemma atLeast_Suc_greaterThan: "atLeast (Suc k) = greaterThan k"
+ by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le)
+
+lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV"
+by blast
+
+lemma atMost_0 [simp]: "atMost (0::nat) = {0}"
+by (simp add: atMost_def)
+
+lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)"
+apply (simp add: atMost_def)
+apply (simp add: less_Suc_eq order_le_less, blast)
+done
+
+lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"
+by blast
+
+(* Intervals of nats with Suc *)
+
+lemma atLeastLessThanSuc_atLeastAtMost: "{l..Suc u(} = {l..u}"
+ by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def)
+
+lemma atLeastSucAtMost_greaterThanAtMost: "{Suc l..u} = {)l..u}"
+ by (simp add: atLeast_Suc_greaterThan atLeastAtMost_def
+ greaterThanAtMost_def)
+
+lemma atLeastSucLessThan_greaterThanLessThan: "{Suc l..u(} = {)l..u(}"
+ by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def
+ greaterThanLessThan_def)
+
+subsubsection {* Finiteness *}
+
+lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..k(}"
+ by (induct k) (simp_all add: lessThan_Suc)
+
+lemma finite_atMost [iff]: fixes k :: nat shows "finite {..k}"
+ by (induct k) (simp_all add: atMost_Suc)
+
+lemma finite_greaterThanLessThan [iff]:
+ fixes l :: nat shows "finite {)l..u(}"
+by (simp add: greaterThanLessThan_def)
+
+lemma finite_atLeastLessThan [iff]:
+ fixes l :: nat shows "finite {l..u(}"
+by (simp add: atLeastLessThan_def)
+
+lemma finite_greaterThanAtMost [iff]:
+ fixes l :: nat shows "finite {)l..u}"
+by (simp add: greaterThanAtMost_def)
+
+lemma finite_atLeastAtMost [iff]:
+ fixes l :: nat shows "finite {l..u}"
+by (simp add: atLeastAtMost_def)
+
+lemma bounded_nat_set_is_finite:
+ "(ALL i:N. i < (n::nat)) ==> finite N"
+ -- {* A bounded set of natural numbers is finite. *}
+ apply (rule finite_subset)
+ apply (rule_tac [2] finite_lessThan, auto)
+ done
+
+subsubsection {* Cardinality *}
+
+lemma card_lessThan [simp]: "card {..u(} = u"
+ by (induct_tac u, simp_all add: lessThan_Suc)
+
+lemma card_atMost [simp]: "card {..u} = Suc u"
+ by (simp add: lessThan_Suc_atMost [THEN sym])
+
+lemma card_atLeastLessThan [simp]: "card {l..u(} = u - l"
+ apply (subgoal_tac "card {l..u(} = card {..u-l(}")
+ apply (erule ssubst, rule card_lessThan)
+ apply (subgoal_tac "(%x. x + l) ` {..u-l(} = {l..u(}")
+ apply (erule subst)
+ apply (rule card_image)
+ apply (rule finite_lessThan)
+ apply (simp add: inj_on_def)
+ apply (auto simp add: image_def atLeastLessThan_def lessThan_def)
+ apply arith
+ apply (rule_tac x = "x - l" in exI)
+ apply arith
+ done
+
+lemma card_atLeastAtMost [simp]: "card {l..u} = Suc u - l"
+ by (subst atLeastLessThanSuc_atLeastAtMost [THEN sym], simp)
+
+lemma card_greaterThanAtMost [simp]: "card {)l..u} = u - l"
+ by (subst atLeastSucAtMost_greaterThanAtMost [THEN sym], simp)
+
+lemma card_greaterThanLessThan [simp]: "card {)l..u(} = u - Suc l"
+ by (subst atLeastSucLessThan_greaterThanLessThan [THEN sym], simp)
+
+subsection {* Intervals of integers *}
+
+lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..u+1(} = {l..(u::int)}"
+ by (auto simp add: atLeastAtMost_def atLeastLessThan_def)
+
+lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {)l..(u::int)}"
+ by (auto simp add: atLeastAtMost_def greaterThanAtMost_def)
+
+lemma atLeastPlusOneLessThan_greaterThanLessThan_int:
+ "{l+1..u(} = {)l..(u::int)(}"
+ by (auto simp add: atLeastLessThan_def greaterThanLessThan_def)
+
+subsubsection {* Finiteness *}
+
+lemma image_atLeastZeroLessThan_int: "0 \<le> u ==>
+ {(0::int)..u(} = int ` {..nat u(}"
+ apply (unfold image_def lessThan_def)
+ apply auto
+ apply (rule_tac x = "nat x" in exI)
+ apply (auto simp add: zless_nat_conj zless_nat_eq_int_zless [THEN sym])
+ done
+
+lemma finite_atLeastZeroLessThan_int: "finite {(0::int)..u(}"
+ apply (case_tac "0 \<le> u")
+ apply (subst image_atLeastZeroLessThan_int, assumption)
+ apply (rule finite_imageI)
+ apply auto
+ apply (subgoal_tac "{0..u(} = {}")
+ apply auto
+ done
+
+lemma image_atLeastLessThan_int_shift:
+ "(%x. x + (l::int)) ` {0..u-l(} = {l..u(}"
+ apply (auto simp add: image_def atLeastLessThan_iff)
+ apply (rule_tac x = "x - l" in bexI)
+ apply auto
+ done
+
+lemma finite_atLeastLessThan_int [iff]: "finite {l..(u::int)(}"
+ apply (subgoal_tac "(%x. x + l) ` {0..u-l(} = {l..u(}")
+ apply (erule subst)
+ apply (rule finite_imageI)
+ apply (rule finite_atLeastZeroLessThan_int)
+ apply (rule image_atLeastLessThan_int_shift)
+ done
+
+lemma finite_atLeastAtMost_int [iff]: "finite {l..(u::int)}"
+ by (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym], simp)
+
+lemma finite_greaterThanAtMost_int [iff]: "finite {)l..(u::int)}"
+ by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp)
+
+lemma finite_greaterThanLessThan_int [iff]: "finite {)l..(u::int)(}"
+ by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp)
+
+subsubsection {* Cardinality *}
+
+lemma card_atLeastZeroLessThan_int: "card {(0::int)..u(} = nat u"
+ apply (case_tac "0 \<le> u")
+ apply (subst image_atLeastZeroLessThan_int, assumption)
+ apply (subst card_image)
+ apply (auto simp add: inj_on_def)
+ done
+
+lemma card_atLeastLessThan_int [simp]: "card {l..u(} = nat (u - l)"
+ apply (subgoal_tac "card {l..u(} = card {0..u-l(}")
+ apply (erule ssubst, rule card_atLeastZeroLessThan_int)
+ apply (subgoal_tac "(%x. x + l) ` {0..u-l(} = {l..u(}")
+ apply (erule subst)
+ apply (rule card_image)
+ apply (rule finite_atLeastZeroLessThan_int)
+ apply (simp add: inj_on_def)
+ apply (rule image_atLeastLessThan_int_shift)
+ done
+
+lemma card_atLeastAtMost_int [simp]: "card {l..u} = nat (u - l + 1)"
+ apply (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym])
+ apply (auto simp add: compare_rls)
+ done
+
+lemma card_greaterThanAtMost_int [simp]: "card {)l..u} = nat (u - l)"
+ by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp)
+
+lemma card_greaterThanLessThan_int [simp]: "card {)l..u(} = nat (u - (l + 1))"
+ by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp)
+
+
subsection {*Lemmas useful with the summation operator setsum*}
(* For examples, see Algebra/poly/UnivPoly.thy *)