src/HOL/Rat.thy

 definition Rats :: "'a set" ("\<rat>")
   where "\<rat> = range of_rat"
 
 end
 
-lemma Rats_of_rat [simp]: "of_rat r \<in> \<rat>"
-  by (simp add: Rats_def)
-
-lemma Rats_of_int [simp]: "of_int z \<in> \<rat>"
-  by (subst of_rat_of_int_eq [symmetric]) (rule Rats_of_rat)
-
-lemma Ints_subset_Rats: "\<int> \<subseteq> \<rat>"
-  using Ints_cases Rats_of_int by blast
-
-lemma Rats_of_nat [simp]: "of_nat n \<in> \<rat>"
-  by (subst of_rat_of_nat_eq [symmetric]) (rule Rats_of_rat)
-
-lemma Nats_subset_Rats: "\<nat> \<subseteq> \<rat>"
-  using Ints_subset_Rats Nats_subset_Ints by blast
-
-lemma Rats_number_of [simp]: "numeral w \<in> \<rat>"
-  by (subst of_rat_numeral_eq [symmetric]) (rule Rats_of_rat)
-
-lemma Rats_0 [simp]: "0 \<in> \<rat>"
-  unfolding Rats_def by (rule range_eqI) (rule of_rat_0 [symmetric])
-
-lemma Rats_1 [simp]: "1 \<in> \<rat>"
-  unfolding Rats_def by (rule range_eqI) (rule of_rat_1 [symmetric])
-
-lemma Rats_add [simp]: "a \<in> \<rat> \<Longrightarrow> b \<in> \<rat> \<Longrightarrow> a + b \<in> \<rat>"
-  apply (auto simp add: Rats_def)
-  apply (rule range_eqI)
-  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_diff [simp]: "a \<in> \<rat> \<Longrightarrow> b \<in> \<rat> \<Longrightarrow> a - b \<in> \<rat>"
-  apply (auto simp add: Rats_def)
-  apply (rule range_eqI)
-  apply (rule of_rat_diff [symmetric])
-  done
-
-lemma Rats_mult [simp]: "a \<in> \<rat> \<Longrightarrow> b \<in> \<rat> \<Longrightarrow> a * b \<in> \<rat>"
-  apply (auto simp add: Rats_def)
-  apply (rule range_eqI)
-  apply (rule of_rat_mult [symmetric])
-  done
-
-lemma Rats_inverse [simp]: "a \<in> \<rat> \<Longrightarrow> inverse a \<in> \<rat>"
-  for a :: "'a::field_char_0"
-  apply (auto simp add: Rats_def)
-  apply (rule range_eqI)
-  apply (rule of_rat_inverse [symmetric])
-  done
-
-lemma Rats_divide [simp]: "a \<in> \<rat> \<Longrightarrow> b \<in> \<rat> \<Longrightarrow> a / b \<in> \<rat>"
-  for a b :: "'a::field_char_0"
-  apply (auto simp add: Rats_def)
-  apply (rule range_eqI)
-  apply (rule of_rat_divide [symmetric])
-  done
-
-lemma Rats_power [simp]: "a \<in> \<rat> \<Longrightarrow> a ^ n \<in> \<rat>"
-  for a :: "'a::field_char_0"
-  apply (auto simp add: Rats_def)
-  apply (rule range_eqI)
-  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_of_rat [simp]: "of_rat r \<in> \<rat>"
+  by (simp add: Rats_def)
+
+lemma Rats_of_int [simp]: "of_int z \<in> \<rat>"
+  by (subst of_rat_of_int_eq [symmetric]) (rule Rats_of_rat)
+
+lemma Ints_subset_Rats: "\<int> \<subseteq> \<rat>"
+  using Ints_cases Rats_of_int by blast
+
+lemma Rats_of_nat [simp]: "of_nat n \<in> \<rat>"
+  by (subst of_rat_of_nat_eq [symmetric]) (rule Rats_of_rat)
+
+lemma Nats_subset_Rats: "\<nat> \<subseteq> \<rat>"
+  using Ints_subset_Rats Nats_subset_Ints by blast
+
+lemma Rats_number_of [simp]: "numeral w \<in> \<rat>"
+  by (subst of_rat_numeral_eq [symmetric]) (rule Rats_of_rat)
+
+lemma Rats_0 [simp]: "0 \<in> \<rat>"
+  unfolding Rats_def by (rule range_eqI) (rule of_rat_0 [symmetric])
+
+lemma Rats_1 [simp]: "1 \<in> \<rat>"
+  unfolding Rats_def by (rule range_eqI) (rule of_rat_1 [symmetric])
+
+lemma Rats_add [simp]: "a \<in> \<rat> \<Longrightarrow> b \<in> \<rat> \<Longrightarrow> a + b \<in> \<rat>"
+  apply (auto simp add: Rats_def)
+  apply (rule range_eqI)
+  apply (rule of_rat_add [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)
+  apply (rule range_eqI)
+  apply (rule of_rat_diff [symmetric])
+  done
+
+lemma Rats_mult [simp]: "a \<in> \<rat> \<Longrightarrow> b \<in> \<rat> \<Longrightarrow> a * b \<in> \<rat>"
+  apply (auto simp add: Rats_def)
+  apply (rule range_eqI)
+  apply (rule of_rat_mult [symmetric])
+  done
+
+lemma Rats_inverse [simp]: "a \<in> \<rat> \<Longrightarrow> inverse a \<in> \<rat>"
+  for a :: "'a::field_char_0"
+  apply (auto simp add: Rats_def)
+  apply (rule range_eqI)
+  apply (rule of_rat_inverse [symmetric])
+  done
+
+lemma Rats_divide [simp]: "a \<in> \<rat> \<Longrightarrow> b \<in> \<rat> \<Longrightarrow> a / b \<in> \<rat>"
+  for a b :: "'a::field_char_0"
+  apply (auto simp add: Rats_def)
+  apply (rule range_eqI)
+  apply (rule of_rat_divide [symmetric])
+  done
+
+lemma Rats_power [simp]: "a \<in> \<rat> \<Longrightarrow> a ^ n \<in> \<rat>"
+  for a :: "'a::field_char_0"
+  apply (auto simp add: Rats_def)
+  apply (rule range_eqI)
+  apply (rule of_rat_power [symmetric])
+  done
 
 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
 
 lemma Rats_infinite: "\<not> finite \<rat>"