use lifting_forget for deregistering numeric types as a quotient type
authorkuncar
Mon Sep 16 15:30:20 2013 +0200 (2013-09-16)
changeset 5365218fbca265e2e
parent 53651 ee90c67502c9
child 53653 a792a504ff22
use lifting_forget for deregistering numeric types as a quotient type
src/HOL/Int.thy
src/HOL/Rat.thy
src/HOL/Real.thy
     1.1 --- a/src/HOL/Int.thy	Mon Sep 16 15:30:17 2013 +0200
     1.2 +++ b/src/HOL/Int.thy	Mon Sep 16 15:30:20 2013 +0200
     1.3 @@ -1660,12 +1660,7 @@
     1.4  
     1.5  text {* De-register @{text "int"} as a quotient type: *}
     1.6  
     1.7 -lemmas [transfer_rule del] =
     1.8 -  int.id_abs_transfer int.rel_eq_transfer zero_int.transfer one_int.transfer
     1.9 -  plus_int.transfer uminus_int.transfer minus_int.transfer times_int.transfer
    1.10 -  int_transfer less_eq_int.transfer less_int.transfer of_int.transfer
    1.11 -  nat.transfer int.right_unique int.right_total int.bi_total
    1.12 -
    1.13 -declare Quotient_int [quot_del]
    1.14 +lifting_update int.lifting
    1.15 +lifting_forget int.lifting
    1.16  
    1.17  end
     2.1 --- a/src/HOL/Rat.thy	Mon Sep 16 15:30:17 2013 +0200
     2.2 +++ b/src/HOL/Rat.thy	Mon Sep 16 15:30:20 2013 +0200
     2.3 @@ -1143,20 +1143,12 @@
     2.4  lemma "123.456 = -111.111 + 200 + 30 + 4 + 5/10 + 6/100 + (7/1000::rat)"
     2.5    by simp
     2.6  
     2.7 +subsection {* Hiding implementation details *}
     2.8  
     2.9  hide_const (open) normalize positive
    2.10  
    2.11 -lemmas [transfer_rule del] =
    2.12 -  rat.rel_eq_transfer
    2.13 -  Fract.transfer zero_rat.transfer one_rat.transfer plus_rat.transfer
    2.14 -  uminus_rat.transfer times_rat.transfer inverse_rat.transfer
    2.15 -  positive.transfer of_rat.transfer rat.right_unique rat.right_total
    2.16 -
    2.17 -lemmas [transfer_domain_rule del] = Domainp_cr_rat rat.domain
    2.18 -
    2.19 -text {* De-register @{text "rat"} as a quotient type: *}
    2.20 -
    2.21 -declare Quotient_rat[quot_del]
    2.22 +lifting_update rat.lifting
    2.23 +lifting_forget rat.lifting
    2.24  
    2.25  end
    2.26  
     3.1 --- a/src/HOL/Real.thy	Mon Sep 16 15:30:17 2013 +0200
     3.2 +++ b/src/HOL/Real.thy	Mon Sep 16 15:30:20 2013 +0200
     3.3 @@ -987,14 +987,8 @@
     3.4  declare Abs_real_induct [induct del]
     3.5  declare Abs_real_cases [cases del]
     3.6  
     3.7 -lemmas [transfer_rule del] =
     3.8 -  real.rel_eq_transfer
     3.9 -  zero_real.transfer one_real.transfer plus_real.transfer uminus_real.transfer
    3.10 -  times_real.transfer inverse_real.transfer positive.transfer real.right_unique
    3.11 -  real.right_total
    3.12 -
    3.13 -lemmas [transfer_domain_rule del] = 
    3.14 -  real.domain real.domain_eq Domainp_pcr_real real.domain_par real.domain_par_left_total
    3.15 +lifting_update real.lifting
    3.16 +lifting_forget real.lifting
    3.17    
    3.18  subsection{*More Lemmas*}
    3.19