unregister lifting setup following the best practice of Lifting
authorkuncar
Tue Feb 25 19:07:14 2014 +0100 (2014-02-25)
changeset 55736f1ed1e9cd080
parent 55735 81ba62493610
child 55737 84f6ac9f6e41
unregister lifting setup following the best practice of Lifting
src/HOL/Code_Numeral.thy
src/HOL/Library/Code_Target_Int.thy
src/HOL/Library/Code_Target_Nat.thy
     1.1 --- a/src/HOL/Code_Numeral.thy	Tue Feb 25 17:06:17 2014 +0000
     1.2 +++ b/src/HOL/Code_Numeral.thy	Tue Feb 25 19:07:14 2014 +0100
     1.3 @@ -928,6 +928,11 @@
     1.4  
     1.5  hide_const (open) Nat
     1.6  
     1.7 +lifting_update integer.lifting
     1.8 +lifting_forget integer.lifting
     1.9 +
    1.10 +lifting_update natural.lifting
    1.11 +lifting_forget natural.lifting
    1.12  
    1.13  code_reflect Code_Numeral
    1.14    datatypes natural = _
     2.1 --- a/src/HOL/Library/Code_Target_Int.thy	Tue Feb 25 17:06:17 2014 +0000
     2.2 +++ b/src/HOL/Library/Code_Target_Int.thy	Tue Feb 25 19:07:14 2014 +0100
     2.3 @@ -12,6 +12,10 @@
     2.4  
     2.5  declare [[code drop: integer_of_int]]
     2.6  
     2.7 +context
     2.8 +includes integer.lifting
     2.9 +begin
    2.10 +
    2.11  lemma [code]:
    2.12    "integer_of_int (int_of_integer k) = k"
    2.13    by transfer rule
    2.14 @@ -86,6 +90,7 @@
    2.15  lemma [code]:
    2.16    "k < l \<longleftrightarrow> (of_int k :: integer) < of_int l"
    2.17    by transfer rule
    2.18 +end
    2.19  
    2.20  lemma (in ring_1) of_int_code_if:
    2.21    "of_int k = (if k = 0 then 0
    2.22 @@ -105,7 +110,7 @@
    2.23  
    2.24  lemma [code]:
    2.25    "nat = nat_of_integer \<circ> of_int"
    2.26 -  by transfer (simp add: fun_eq_iff)
    2.27 +  including integer.lifting by transfer (simp add: fun_eq_iff)
    2.28  
    2.29  code_identifier
    2.30    code_module Code_Target_Int \<rightharpoonup>
     3.1 --- a/src/HOL/Library/Code_Target_Nat.thy	Tue Feb 25 17:06:17 2014 +0000
     3.2 +++ b/src/HOL/Library/Code_Target_Nat.thy	Tue Feb 25 19:07:14 2014 +0100
     3.3 @@ -10,6 +10,10 @@
     3.4  
     3.5  subsection {* Implementation for @{typ nat} *}
     3.6  
     3.7 +context
     3.8 +includes natural.lifting integer.lifting
     3.9 +begin
    3.10 +
    3.11  lift_definition Nat :: "integer \<Rightarrow> nat"
    3.12    is nat
    3.13    .
    3.14 @@ -96,6 +100,8 @@
    3.15    "num_of_nat = num_of_integer \<circ> of_nat"
    3.16    by transfer (simp add: fun_eq_iff)
    3.17  
    3.18 +end
    3.19 +
    3.20  lemma (in semiring_1) of_nat_code_if:
    3.21    "of_nat n = (if n = 0 then 0
    3.22       else let
    3.23 @@ -120,7 +126,7 @@
    3.24  
    3.25  lemma [code abstract]:
    3.26    "integer_of_nat (nat k) = max 0 (integer_of_int k)"
    3.27 -  by transfer auto
    3.28 +  including integer.lifting by transfer auto
    3.29  
    3.30  lemma term_of_nat_code [code]:
    3.31    -- {* Use @{term Code_Numeral.nat_of_integer} in term reconstruction
    3.32 @@ -139,7 +145,7 @@
    3.33    "nat_of_integer 0 = 0"
    3.34    "nat_of_integer 1 = 1"
    3.35    "nat_of_integer (numeral k) = numeral k"
    3.36 -  by (transfer, simp)+
    3.37 +  including integer.lifting by (transfer, simp)+
    3.38  
    3.39  code_identifier
    3.40    code_module Code_Target_Nat \<rightharpoonup>