# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1442937307 -3600
# Node ID a9e6052188fae96f304b10e1f766af483e45cadd
# Parent  1da01148d4b1604eabf610662514300b9d75e2cf
New lemmas

diff -r 1da01148d4b1 -r a9e6052188fa src/HOL/Int.thy
--- a/src/HOL/Int.thy	Tue Sep 22 16:53:59 2015 +0100
+++ b/src/HOL/Int.thy	Tue Sep 22 16:55:07 2015 +0100
@@ -258,6 +258,10 @@
   "0 = of_int z \<longleftrightarrow> z = 0"
   using of_int_eq_iff [of 0 z] by simp
 
+lemma of_int_eq_1_iff [iff]:
+   "of_int z = 1 \<longleftrightarrow> z = 1"
+  using of_int_eq_iff [of z 1] by simp
+
 end
 
 context linordered_idom
@@ -291,8 +295,49 @@
   "of_int z < 0 \<longleftrightarrow> z < 0"
   using of_int_less_iff [of z 0] by simp
 
+lemma of_int_1_le_iff [simp]:
+  "1 \<le> of_int z \<longleftrightarrow> 1 \<le> z"
+  using of_int_le_iff [of 1 z] by simp
+
+lemma of_int_le_1_iff [simp]:
+  "of_int z \<le> 1 \<longleftrightarrow> z \<le> 1"
+  using of_int_le_iff [of z 1] by simp
+
+lemma of_int_1_less_iff [simp]:
+  "1 < of_int z \<longleftrightarrow> 1 < z"
+  using of_int_less_iff [of 1 z] by simp
+
+lemma of_int_less_1_iff [simp]:
+  "of_int z < 1 \<longleftrightarrow> z < 1"
+  using of_int_less_iff [of z 1] by simp
+
 end
 
+text \<open>Comparisons involving @{term of_int}.\<close>
+
+lemma of_int_eq_numeral_iff [iff]:
+   "of_int z = (numeral n :: 'a::ring_char_0) 
+   \<longleftrightarrow> z = numeral n"
+  using of_int_eq_iff by fastforce
+
+lemma of_int_le_numeral_iff [simp]:           
+   "of_int z \<le> (numeral n :: 'a::linordered_idom) 
+   \<longleftrightarrow> z \<le> numeral n"
+  using of_int_le_iff [of z "numeral n"] by simp
+
+lemma of_int_numeral_le_iff [simp]:  
+   "(numeral n :: 'a::linordered_idom) \<le> of_int z \<longleftrightarrow> numeral n \<le> z"
+  using of_int_le_iff [of "numeral n"] by simp
+
+lemma of_int_less_numeral_iff [simp]:           
+   "of_int z < (numeral n :: 'a::linordered_idom) 
+   \<longleftrightarrow> z < numeral n"
+  using of_int_less_iff [of z "numeral n"] by simp
+
+lemma of_int_numeral_less_iff [simp]:           
+   "(numeral n :: 'a::linordered_idom) < of_int z \<longleftrightarrow> numeral n < z"
+  using of_int_less_iff [of "numeral n" z] by simp
+
 lemma of_nat_less_of_int_iff:
   "(of_nat n::'a::linordered_idom) < of_int x \<longleftrightarrow> int n < x"
   by (metis of_int_of_nat_eq of_int_less_iff)
diff -r 1da01148d4b1 -r a9e6052188fa src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Tue Sep 22 16:53:59 2015 +0100
+++ b/src/HOL/Topological_Spaces.thy	Tue Sep 22 16:55:07 2015 +0100
@@ -377,6 +377,10 @@
 lemma at_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> at a within S = at a"
   unfolding filter_eq_iff eventually_at_topological by (metis open_Int Int_iff UNIV_I)
 
+lemma at_within_open_NO_MATCH:
+  "a \<in> s \<Longrightarrow> open s \<Longrightarrow> NO_MATCH UNIV s \<Longrightarrow> at a within s = at a"
+  by (simp only: at_within_open)
+
 lemma at_within_empty [simp]: "at a within {} = bot"
   unfolding at_within_def by simp