# HG changeset patch # User paulson # Date 1080207141 -3600 # Node ID ea2707645af8633f6a09f9be6e5d7592164906ce # Parent ef8c7c5eb01b78a873559323ce09992d1f1121bf new material from Avigad diff -r ef8c7c5eb01b -r ea2707645af8 src/HOL/Finite_Set.ML --- 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"; diff -r ef8c7c5eb01b -r ea2707645af8 src/HOL/Finite_Set.thy --- 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 (\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 (\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 \ f) B" +apply (rule finite_induct, assumption, force) +apply (rule impI, auto) +apply (simp add: inj_on_def) +apply (subgoal_tac "f x \ 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 \ 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 \ 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 \ 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 (\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 \ 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 \ 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, simp add: card_eq_setsum) - done - -lemma card_Union_disjoint: - "finite C ==> (ALL A:C. finite A) ==> - (ALL A:C. ALL B:C. A \ 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 \ f) B" -apply (rule finite_induct, assumption, force) -apply (rule impI, auto) -apply (simp add: inj_on_def) -apply (subgoal_tac "f x \ 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 \ 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 \ 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 \ 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) ==> + (\ x:A. (\ y:B x. f x y)) = + (\ 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 ==> + (\ x:A. (\ y:B. f x y)) = + (\ 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 ==> (\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 \ 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 \ 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 \ A ==> (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \ (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 (\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 \ f) B" +apply (rule finite_induct, assumption, force) +apply (rule impI, auto) +apply (simp add: inj_on_def) +apply (subgoal_tac "f x \ 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 \ 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 \ 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 \ 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 (\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 \ 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 \ f) B" -apply (rule finite_induct, assumption, force) -apply (rule impI, auto) -apply (simp add: inj_on_def) -apply (subgoal_tac "f x \ 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 \ 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 \ 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 \ 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) ==> + (\ x:A. (\ y: B x. f x y)) = + (\ 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 ==> + (\ x:A. (\ y: B. f x y)) = + (\ 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 *} diff -r ef8c7c5eb01b -r ea2707645af8 src/HOL/Infinite_Set.thy --- 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" diff -r ef8c7c5eb01b -r ea2707645af8 src/HOL/Integ/IntDef.thy --- 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 (\(x,y) \ Rep_Integ(z). { Abs_Integ(intrel``{(y,x)}) })" + "- z == contents (\(x,y) \ 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"; diff -r ef8c7c5eb01b -r ea2707645af8 src/HOL/Integ/Presburger.thy --- 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") diff -r ef8c7c5eb01b -r ea2707645af8 src/HOL/NumberTheory/Euler.thy --- 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 diff -r ef8c7c5eb01b -r ea2707645af8 src/HOL/NumberTheory/Finite2.thy --- 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 "(\x \ UNION A g. 1) = (\x \ A. \x \ 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 ==> ((\x \ A. finite (g x)) & diff -r ef8c7c5eb01b -r ea2707645af8 src/HOL/Presburger.thy --- 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") diff -r ef8c7c5eb01b -r ea2707645af8 src/HOL/SetInterval.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"; diff -r ef8c7c5eb01b -r ea2707645af8 src/HOL/SetInterval.thy --- 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 atLeast y) = (y \ (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 \ 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 \ 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 \ 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 *)