src/HOL/Rat.thy
changeset 51956 a4d81cdebf8b
parent 51185 145d76c35f8b
child 52146 ceb31e1ded30
     1.1 --- a/src/HOL/Rat.thy	Mon May 13 12:13:24 2013 +0200
     1.2 +++ b/src/HOL/Rat.thy	Mon May 13 13:59:04 2013 +0200
     1.3 @@ -49,13 +49,8 @@
     1.4    morphisms Rep_Rat Abs_Rat
     1.5    by (rule part_equivp_ratrel)
     1.6  
     1.7 -declare rat.forall_transfer [transfer_rule del]
     1.8 -
     1.9 -lemma forall_rat_transfer [transfer_rule]: (* TODO: generate automatically *)
    1.10 -  "(fun_rel (fun_rel cr_rat op =) op =)
    1.11 -    (transfer_bforall (\<lambda>x. snd x \<noteq> 0)) transfer_forall"
    1.12 -  using rat.forall_transfer by simp
    1.13 -
    1.14 +lemma Domainp_cr_rat [transfer_domain_rule]: "Domainp cr_rat = (\<lambda>x. snd x \<noteq> 0)"
    1.15 +by (simp add: rat.domain)
    1.16  
    1.17  subsubsection {* Representation and basic operations *}
    1.18  
    1.19 @@ -1126,11 +1121,13 @@
    1.20  hide_const (open) normalize positive
    1.21  
    1.22  lemmas [transfer_rule del] =
    1.23 -  rat.All_transfer rat.Ex_transfer rat.rel_eq_transfer forall_rat_transfer
    1.24 +  rat.rel_eq_transfer
    1.25    Fract.transfer zero_rat.transfer one_rat.transfer plus_rat.transfer
    1.26    uminus_rat.transfer times_rat.transfer inverse_rat.transfer
    1.27    positive.transfer of_rat.transfer rat.right_unique rat.right_total
    1.28  
    1.29 +lemmas [transfer_domain_rule del] = Domainp_cr_rat rat.domain
    1.30 +
    1.31  text {* De-register @{text "rat"} as a quotient type: *}
    1.32  
    1.33  declare Quotient_rat[quot_del]