removed duplicates
authornipkow
Thu Jun 14 10:51:12 2018 +0200 (11 days ago)
changeset 684413b11d48a711a
parent 68440 6826718f732d
child 68442 477b3f7067c9
child 68446 92ddca1edc43
removed duplicates
src/HOL/Rat.thy
     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