simple new lemmas, mostly about sets
authorpaulson <lp15@cam.ac.uk>
Thu Sep 15 14:14:49 2016 +0100 (2016-09-15)
changeset 6387915bbf6360339
parent 63877 b4051d3f4e94
child 63880 729accd056ad
simple new lemmas, mostly about sets
src/HOL/Archimedean_Field.thy
src/HOL/Complete_Lattices.thy
src/HOL/Set.thy
src/HOL/Set_Interval.thy
     1.1 --- a/src/HOL/Archimedean_Field.thy	Thu Sep 15 11:44:05 2016 +0200
     1.2 +++ b/src/HOL/Archimedean_Field.thy	Thu Sep 15 14:14:49 2016 +0100
     1.3 @@ -492,6 +492,18 @@
     1.4  lemma ceiling_add_le: "\<lceil>x + y\<rceil> \<le> \<lceil>x\<rceil> + \<lceil>y\<rceil>"
     1.5    by (simp only: ceiling_le_iff of_int_add add_mono le_of_int_ceiling)
     1.6  
     1.7 +lemma finite_int_segment:
     1.8 +  fixes a :: "'a::floor_ceiling"
     1.9 +  shows "finite {x \<in> \<int>. a \<le> x \<and> x \<le> b}"
    1.10 +proof -
    1.11 +  have "finite {ceiling a..floor b}"
    1.12 +    by simp
    1.13 +  moreover have "{x \<in> \<int>. a \<le> x \<and> x \<le> b} = of_int ` {ceiling a..floor b}"
    1.14 +    by (auto simp: le_floor_iff ceiling_le_iff elim!: Ints_cases)
    1.15 +  ultimately show ?thesis
    1.16 +    by simp
    1.17 +qed
    1.18 +
    1.19  
    1.20  text \<open>Ceiling with numerals.\<close>
    1.21  
     2.1 --- a/src/HOL/Complete_Lattices.thy	Thu Sep 15 11:44:05 2016 +0200
     2.2 +++ b/src/HOL/Complete_Lattices.thy	Thu Sep 15 14:14:49 2016 +0100
     2.3 @@ -1055,6 +1055,11 @@
     2.4  lemma Union_subsetI: "(\<And>x. x \<in> A \<Longrightarrow> \<exists>y. y \<in> B \<and> x \<subseteq> y) \<Longrightarrow> \<Union>A \<subseteq> \<Union>B"
     2.5    by blast
     2.6  
     2.7 +lemma disjnt_inj_on_iff:
     2.8 +     "\<lbrakk>inj_on f (\<Union>\<A>); X \<in> \<A>; Y \<in> \<A>\<rbrakk> \<Longrightarrow> disjnt (f ` X) (f ` Y) \<longleftrightarrow> disjnt X Y"
     2.9 +  apply (auto simp: disjnt_def)
    2.10 +  using inj_on_eq_iff by fastforce
    2.11 +
    2.12  
    2.13  subsubsection \<open>Unions of families\<close>
    2.14  
     3.1 --- a/src/HOL/Set.thy	Thu Sep 15 11:44:05 2016 +0200
     3.2 +++ b/src/HOL/Set.thy	Thu Sep 15 14:14:49 2016 +0100
     3.3 @@ -1858,6 +1858,24 @@
     3.4  lemma disjnt_iff: "disjnt A B \<longleftrightarrow> (\<forall>x. \<not> (x \<in> A \<and> x \<in> B))"
     3.5    by (force simp: disjnt_def)
     3.6  
     3.7 +lemma disjnt_sym: "disjnt A B \<Longrightarrow> disjnt B A"
     3.8 +  using disjnt_iff by blast
     3.9 +
    3.10 +lemma disjnt_empty1 [simp]: "disjnt {} A" and disjnt_empty2 [simp]: "disjnt A {}"
    3.11 +  by (auto simp: disjnt_def)
    3.12 +
    3.13 +lemma disjnt_insert1 [simp]: "disjnt (insert a X) Y \<longleftrightarrow> a \<notin> Y \<and> disjnt X Y"
    3.14 +  by (simp add: disjnt_def)
    3.15 +
    3.16 +lemma disjnt_insert2 [simp]: "disjnt Y (insert a X) \<longleftrightarrow> a \<notin> Y \<and> disjnt Y X"
    3.17 +  by (simp add: disjnt_def)
    3.18 +
    3.19 +lemma disjnt_subset1 : "\<lbrakk>disjnt X Y; Z \<subseteq> X\<rbrakk> \<Longrightarrow> disjnt Z Y"
    3.20 +  by (auto simp: disjnt_def)
    3.21 +
    3.22 +lemma disjnt_subset2 : "\<lbrakk>disjnt X Y; Z \<subseteq> Y\<rbrakk> \<Longrightarrow> disjnt X Z"
    3.23 +  by (auto simp: disjnt_def)
    3.24 +
    3.25  lemma pairwise_empty [simp]: "pairwise P {}"
    3.26    by (simp add: pairwise_def)
    3.27  
    3.28 @@ -1871,6 +1889,9 @@
    3.29  lemma pairwise_image: "pairwise r (f ` s) \<longleftrightarrow> pairwise (\<lambda>x y. (f x \<noteq> f y) \<longrightarrow> r (f x) (f y)) s"
    3.30    by (force simp: pairwise_def)
    3.31  
    3.32 +lemma disjoint_image_subset: "\<lbrakk>pairwise disjnt \<A>; \<And>X. X \<in> \<A> \<Longrightarrow> f X \<subseteq> X\<rbrakk> \<Longrightarrow> pairwise disjnt (f `\<A>)"
    3.33 +  unfolding disjnt_def pairwise_def by fast
    3.34 +
    3.35  lemma Int_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> False) \<Longrightarrow> A \<inter> B = {}"
    3.36    by blast
    3.37  
     4.1 --- a/src/HOL/Set_Interval.thy	Thu Sep 15 11:44:05 2016 +0200
     4.2 +++ b/src/HOL/Set_Interval.thy	Thu Sep 15 14:14:49 2016 +0100
     4.3 @@ -130,6 +130,12 @@
     4.4  
     4.5  subsection \<open>Logical Equivalences for Set Inclusion and Equality\<close>
     4.6  
     4.7 +lemma atLeast_empty_triv [simp]: "{{}..} = UNIV"
     4.8 +  by auto
     4.9 +
    4.10 +lemma atMost_UNIV_triv [simp]: "{..UNIV} = UNIV"
    4.11 +  by auto
    4.12 +
    4.13  lemma atLeast_subset_iff [iff]:
    4.14       "(atLeast x \<subseteq> atLeast y) = (y \<le> (x::'a::order))"
    4.15  by (blast intro: order_trans)