# HG changeset patch
# User nipkow
# Date 1530198892 -7200
# Node ID 29235951f104b72476ff9f0fbd34984585fe8489
# Parent  d31e986fbebce4754e9e7d75ceb306cea7e7b096
added lemmas

diff -r d31e986fbebc -r 29235951f104 src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Thu Jun 28 14:14:05 2018 +0100
+++ b/src/HOL/Rat.thy	Thu Jun 28 17:14:52 2018 +0200
@@ -821,6 +821,16 @@
 
 end
 
+lemma Rats_cases [cases set: Rats]:
+  assumes "q \<in> \<rat>"
+  obtains (of_rat) r where "q = of_rat r"
+proof -
+  from \<open>q \<in> \<rat>\<close> have "q \<in> range of_rat"
+    by (simp only: Rats_def)
+  then obtain r where "q = of_rat r" ..
+  then show thesis ..
+qed
+
 lemma Rats_of_rat [simp]: "of_rat r \<in> \<rat>"
   by (simp add: Rats_def)
 
@@ -851,11 +861,8 @@
   apply (rule of_rat_add [symmetric])
   done
 
-lemma Rats_minus [simp]: "a \<in> \<rat> \<Longrightarrow> - a \<in> \<rat>"
-  apply (auto simp add: Rats_def)
-  apply (rule range_eqI)
-  apply (rule of_rat_minus [symmetric])
-  done
+lemma Rats_minus_iff [simp]: "- a \<in> \<rat> \<longleftrightarrow> a \<in> \<rat>"
+by (metis Rats_cases Rats_of_rat add.inverse_inverse of_rat_minus)
 
 lemma Rats_diff [simp]: "a \<in> \<rat> \<Longrightarrow> b \<in> \<rat> \<Longrightarrow> a - b \<in> \<rat>"
   apply (auto simp add: Rats_def)
@@ -890,16 +897,6 @@
   apply (rule of_rat_power [symmetric])
   done
 
-lemma Rats_cases [cases set: Rats]:
-  assumes "q \<in> \<rat>"
-  obtains (of_rat) r where "q = of_rat r"
-proof -
-  from \<open>q \<in> \<rat>\<close> have "q \<in> range of_rat"
-    by (simp only: Rats_def)
-  then obtain r where "q = of_rat r" ..
-  then show thesis ..
-qed
-
 lemma Rats_induct [case_names of_rat, induct set: Rats]: "q \<in> \<rat> \<Longrightarrow> (\<And>r. P (of_rat r)) \<Longrightarrow> P q"
   by (rule Rats_cases) auto
 
diff -r d31e986fbebc -r 29235951f104 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Thu Jun 28 14:14:05 2018 +0100
+++ b/src/HOL/Real.thy	Thu Jun 28 17:14:52 2018 +0200
@@ -1192,6 +1192,10 @@
 
 subsection \<open>Rationals\<close>
 
+lemma Rats_abs_iff[simp]:
+  "\<bar>(x::real)\<bar> \<in> \<rat> \<longleftrightarrow> x \<in> \<rat>"
+by(simp add: abs_real_def split: if_splits)
+
 lemma Rats_eq_int_div_int: "\<rat> = {real_of_int i / real_of_int j | i j. j \<noteq> 0}"  (is "_ = ?S")
 proof
   show "\<rat> \<subseteq> ?S"