New lemmas
authorpaulson <lp15@cam.ac.uk>
Tue Sep 22 16:55:07 2015 +0100 (2015-09-22)
changeset 61234a9e6052188fa
parent 61233 1da01148d4b1
child 61235 37862ccec075
New lemmas
src/HOL/Int.thy
src/HOL/Topological_Spaces.thy
     1.1 --- a/src/HOL/Int.thy	Tue Sep 22 16:53:59 2015 +0100
     1.2 +++ b/src/HOL/Int.thy	Tue Sep 22 16:55:07 2015 +0100
     1.3 @@ -258,6 +258,10 @@
     1.4    "0 = of_int z \<longleftrightarrow> z = 0"
     1.5    using of_int_eq_iff [of 0 z] by simp
     1.6  
     1.7 +lemma of_int_eq_1_iff [iff]:
     1.8 +   "of_int z = 1 \<longleftrightarrow> z = 1"
     1.9 +  using of_int_eq_iff [of z 1] by simp
    1.10 +
    1.11  end
    1.12  
    1.13  context linordered_idom
    1.14 @@ -291,8 +295,49 @@
    1.15    "of_int z < 0 \<longleftrightarrow> z < 0"
    1.16    using of_int_less_iff [of z 0] by simp
    1.17  
    1.18 +lemma of_int_1_le_iff [simp]:
    1.19 +  "1 \<le> of_int z \<longleftrightarrow> 1 \<le> z"
    1.20 +  using of_int_le_iff [of 1 z] by simp
    1.21 +
    1.22 +lemma of_int_le_1_iff [simp]:
    1.23 +  "of_int z \<le> 1 \<longleftrightarrow> z \<le> 1"
    1.24 +  using of_int_le_iff [of z 1] by simp
    1.25 +
    1.26 +lemma of_int_1_less_iff [simp]:
    1.27 +  "1 < of_int z \<longleftrightarrow> 1 < z"
    1.28 +  using of_int_less_iff [of 1 z] by simp
    1.29 +
    1.30 +lemma of_int_less_1_iff [simp]:
    1.31 +  "of_int z < 1 \<longleftrightarrow> z < 1"
    1.32 +  using of_int_less_iff [of z 1] by simp
    1.33 +
    1.34  end
    1.35  
    1.36 +text \<open>Comparisons involving @{term of_int}.\<close>
    1.37 +
    1.38 +lemma of_int_eq_numeral_iff [iff]:
    1.39 +   "of_int z = (numeral n :: 'a::ring_char_0) 
    1.40 +   \<longleftrightarrow> z = numeral n"
    1.41 +  using of_int_eq_iff by fastforce
    1.42 +
    1.43 +lemma of_int_le_numeral_iff [simp]:           
    1.44 +   "of_int z \<le> (numeral n :: 'a::linordered_idom) 
    1.45 +   \<longleftrightarrow> z \<le> numeral n"
    1.46 +  using of_int_le_iff [of z "numeral n"] by simp
    1.47 +
    1.48 +lemma of_int_numeral_le_iff [simp]:  
    1.49 +   "(numeral n :: 'a::linordered_idom) \<le> of_int z \<longleftrightarrow> numeral n \<le> z"
    1.50 +  using of_int_le_iff [of "numeral n"] by simp
    1.51 +
    1.52 +lemma of_int_less_numeral_iff [simp]:           
    1.53 +   "of_int z < (numeral n :: 'a::linordered_idom) 
    1.54 +   \<longleftrightarrow> z < numeral n"
    1.55 +  using of_int_less_iff [of z "numeral n"] by simp
    1.56 +
    1.57 +lemma of_int_numeral_less_iff [simp]:           
    1.58 +   "(numeral n :: 'a::linordered_idom) < of_int z \<longleftrightarrow> numeral n < z"
    1.59 +  using of_int_less_iff [of "numeral n" z] by simp
    1.60 +
    1.61  lemma of_nat_less_of_int_iff:
    1.62    "(of_nat n::'a::linordered_idom) < of_int x \<longleftrightarrow> int n < x"
    1.63    by (metis of_int_of_nat_eq of_int_less_iff)
     2.1 --- a/src/HOL/Topological_Spaces.thy	Tue Sep 22 16:53:59 2015 +0100
     2.2 +++ b/src/HOL/Topological_Spaces.thy	Tue Sep 22 16:55:07 2015 +0100
     2.3 @@ -377,6 +377,10 @@
     2.4  lemma at_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> at a within S = at a"
     2.5    unfolding filter_eq_iff eventually_at_topological by (metis open_Int Int_iff UNIV_I)
     2.6  
     2.7 +lemma at_within_open_NO_MATCH:
     2.8 +  "a \<in> s \<Longrightarrow> open s \<Longrightarrow> NO_MATCH UNIV s \<Longrightarrow> at a within s = at a"
     2.9 +  by (simp only: at_within_open)
    2.10 +
    2.11  lemma at_within_empty [simp]: "at a within {} = bot"
    2.12    unfolding at_within_def by simp
    2.13