author nipkow Thu Jun 14 10:51:12 2018 +0200 (11 days ago) changeset 68441 3b11d48a711a parent 68440 6826718f732d child 68442 477b3f7067c9 child 68446 92ddca1edc43
removed duplicates
 src/HOL/Rat.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Rat.thy	Wed Jun 13 15:24:20 2018 +0200
1.2 +++ b/src/HOL/Rat.thy	Thu Jun 14 10:51:12 2018 +0200
1.3 @@ -710,13 +710,13 @@
1.4  lemma nonzero_of_rat_inverse: "a \<noteq> 0 \<Longrightarrow> of_rat (inverse a) = inverse (of_rat a)"
1.5    by (rule inverse_unique [symmetric]) (simp add: of_rat_mult [symmetric])
1.6
1.7 -lemma of_rat_inverse: "(of_rat (inverse a) :: 'a::{field_char_0,field}) = inverse (of_rat a)"
1.8 +lemma of_rat_inverse: "(of_rat (inverse a) :: 'a::field_char_0) = inverse (of_rat a)"
1.9    by (cases "a = 0") (simp_all add: nonzero_of_rat_inverse)
1.10
1.11  lemma nonzero_of_rat_divide: "b \<noteq> 0 \<Longrightarrow> of_rat (a / b) = of_rat a / of_rat b"
1.12    by (simp add: divide_inverse of_rat_mult nonzero_of_rat_inverse)
1.13
1.14 -lemma of_rat_divide: "(of_rat (a / b) :: 'a::{field_char_0,field}) = of_rat a / of_rat b"
1.15 +lemma of_rat_divide: "(of_rat (a / b) :: 'a::field_char_0) = of_rat a / of_rat b"
1.16    by (cases "b = 0") (simp_all add: nonzero_of_rat_divide)
1.17
1.18  lemma of_rat_power: "(of_rat (a ^ n) :: 'a::field_char_0) = of_rat a ^ n"
1.19 @@ -869,31 +869,17 @@
1.20    apply (rule of_rat_mult [symmetric])
1.21    done
1.22
1.23 -lemma nonzero_Rats_inverse: "a \<in> \<rat> \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> inverse a \<in> \<rat>"
1.24 +lemma Rats_inverse [simp]: "a \<in> \<rat> \<Longrightarrow> inverse a \<in> \<rat>"
1.25    for a :: "'a::field_char_0"
1.26    apply (auto simp add: Rats_def)
1.27    apply (rule range_eqI)
1.28 -  apply (erule nonzero_of_rat_inverse [symmetric])
1.29 -  done
1.30 -
1.31 -lemma Rats_inverse [simp]: "a \<in> \<rat> \<Longrightarrow> inverse a \<in> \<rat>"
1.32 -  for a :: "'a::{field_char_0,field}"
1.33 -  apply (auto simp add: Rats_def)
1.34 -  apply (rule range_eqI)
1.35    apply (rule of_rat_inverse [symmetric])
1.36    done
1.37
1.38 -lemma nonzero_Rats_divide: "a \<in> \<rat> \<Longrightarrow> b \<in> \<rat> \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a / b \<in> \<rat>"
1.39 +lemma Rats_divide [simp]: "a \<in> \<rat> \<Longrightarrow> b \<in> \<rat> \<Longrightarrow> a / b \<in> \<rat>"
1.40    for a b :: "'a::field_char_0"
1.41    apply (auto simp add: Rats_def)
1.42    apply (rule range_eqI)
1.43 -  apply (erule nonzero_of_rat_divide [symmetric])
1.44 -  done
1.45 -
1.46 -lemma Rats_divide [simp]: "a \<in> \<rat> \<Longrightarrow> b \<in> \<rat> \<Longrightarrow> a / b \<in> \<rat>"
1.47 -  for a b :: "'a::{field_char_0, field}"
1.48 -  apply (auto simp add: Rats_def)
1.49 -  apply (rule range_eqI)
1.50    apply (rule of_rat_divide [symmetric])
1.51    done
1.52
```