# HG changeset patch # User paulson # Date 1473945289 -3600 # Node ID 15bbf6360339dc4c89837b9a068b2991d4a4d67f # Parent b4051d3f4e94a9ef786679b0193a84f9e256bbd3 simple new lemmas, mostly about sets diff -r b4051d3f4e94 -r 15bbf6360339 src/HOL/Archimedean_Field.thy --- a/src/HOL/Archimedean_Field.thy Thu Sep 15 11:44:05 2016 +0200 +++ b/src/HOL/Archimedean_Field.thy Thu Sep 15 14:14:49 2016 +0100 @@ -492,6 +492,18 @@ lemma ceiling_add_le: "\x + y\ \ \x\ + \y\" by (simp only: ceiling_le_iff of_int_add add_mono le_of_int_ceiling) +lemma finite_int_segment: + fixes a :: "'a::floor_ceiling" + shows "finite {x \ \. a \ x \ x \ b}" +proof - + have "finite {ceiling a..floor b}" + by simp + moreover have "{x \ \. a \ x \ x \ b} = of_int ` {ceiling a..floor b}" + by (auto simp: le_floor_iff ceiling_le_iff elim!: Ints_cases) + ultimately show ?thesis + by simp +qed + text \Ceiling with numerals.\ diff -r b4051d3f4e94 -r 15bbf6360339 src/HOL/Complete_Lattices.thy --- a/src/HOL/Complete_Lattices.thy Thu Sep 15 11:44:05 2016 +0200 +++ b/src/HOL/Complete_Lattices.thy Thu Sep 15 14:14:49 2016 +0100 @@ -1055,6 +1055,11 @@ lemma Union_subsetI: "(\x. x \ A \ \y. y \ B \ x \ y) \ \A \ \B" by blast +lemma disjnt_inj_on_iff: + "\inj_on f (\\); X \ \; Y \ \\ \ disjnt (f ` X) (f ` Y) \ disjnt X Y" + apply (auto simp: disjnt_def) + using inj_on_eq_iff by fastforce + subsubsection \Unions of families\ diff -r b4051d3f4e94 -r 15bbf6360339 src/HOL/Set.thy --- a/src/HOL/Set.thy Thu Sep 15 11:44:05 2016 +0200 +++ b/src/HOL/Set.thy Thu Sep 15 14:14:49 2016 +0100 @@ -1858,6 +1858,24 @@ lemma disjnt_iff: "disjnt A B \ (\x. \ (x \ A \ x \ B))" by (force simp: disjnt_def) +lemma disjnt_sym: "disjnt A B \ disjnt B A" + using disjnt_iff by blast + +lemma disjnt_empty1 [simp]: "disjnt {} A" and disjnt_empty2 [simp]: "disjnt A {}" + by (auto simp: disjnt_def) + +lemma disjnt_insert1 [simp]: "disjnt (insert a X) Y \ a \ Y \ disjnt X Y" + by (simp add: disjnt_def) + +lemma disjnt_insert2 [simp]: "disjnt Y (insert a X) \ a \ Y \ disjnt Y X" + by (simp add: disjnt_def) + +lemma disjnt_subset1 : "\disjnt X Y; Z \ X\ \ disjnt Z Y" + by (auto simp: disjnt_def) + +lemma disjnt_subset2 : "\disjnt X Y; Z \ Y\ \ disjnt X Z" + by (auto simp: disjnt_def) + lemma pairwise_empty [simp]: "pairwise P {}" by (simp add: pairwise_def) @@ -1871,6 +1889,9 @@ lemma pairwise_image: "pairwise r (f ` s) \ pairwise (\x y. (f x \ f y) \ r (f x) (f y)) s" by (force simp: pairwise_def) +lemma disjoint_image_subset: "\pairwise disjnt \; \X. X \ \ \ f X \ X\ \ pairwise disjnt (f `\)" + unfolding disjnt_def pairwise_def by fast + lemma Int_emptyI: "(\x. x \ A \ x \ B \ False) \ A \ B = {}" by blast diff -r b4051d3f4e94 -r 15bbf6360339 src/HOL/Set_Interval.thy --- a/src/HOL/Set_Interval.thy Thu Sep 15 11:44:05 2016 +0200 +++ b/src/HOL/Set_Interval.thy Thu Sep 15 14:14:49 2016 +0100 @@ -130,6 +130,12 @@ subsection \Logical Equivalences for Set Inclusion and Equality\ +lemma atLeast_empty_triv [simp]: "{{}..} = UNIV" + by auto + +lemma atMost_UNIV_triv [simp]: "{..UNIV} = UNIV" + by auto + lemma atLeast_subset_iff [iff]: "(atLeast x \ atLeast y) = (y \ (x::'a::order))" by (blast intro: order_trans)