src/HOL/Library/Efficient_Nat.thy
changeset 46028 9f113cdf3d66
parent 45793 331ebffe0593
child 46497 89ccf66aa73d
     1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Thu Dec 29 10:47:55 2011 +0100
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Thu Dec 29 10:47:55 2011 +0100
     1.3 @@ -26,11 +26,11 @@
     1.4  
     1.5  code_datatype number_nat_inst.number_of_nat
     1.6  
     1.7 -lemma zero_nat_code [code, code_unfold_post]:
     1.8 +lemma zero_nat_code [code, code_unfold]:
     1.9    "0 = (Numeral0 :: nat)"
    1.10    by simp
    1.11  
    1.12 -lemma one_nat_code [code, code_unfold_post]:
    1.13 +lemma one_nat_code [code, code_unfold]:
    1.14    "1 = (Numeral1 :: nat)"
    1.15    by simp
    1.16  
    1.17 @@ -286,8 +286,8 @@
    1.18    Natural numerals.
    1.19  *}
    1.20  
    1.21 -lemma [code_unfold_post]:
    1.22 -  "nat (number_of i) = number_nat_inst.number_of_nat i"
    1.23 +lemma [code_abbrev]:
    1.24 +  "number_nat_inst.number_of_nat i = nat (number_of i)"
    1.25    -- {* this interacts as desired with @{thm nat_number_of_def} *}
    1.26    by (simp add: number_nat_inst.number_of_nat)
    1.27  
    1.28 @@ -307,7 +307,7 @@
    1.29  *}
    1.30  
    1.31  definition int :: "nat \<Rightarrow> int" where
    1.32 -  [code del]: "int = of_nat"
    1.33 +  [code del, code_abbrev]: "int = of_nat"
    1.34  
    1.35  lemma int_code' [code]:
    1.36    "int (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
    1.37 @@ -317,7 +317,7 @@
    1.38    "nat (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
    1.39    unfolding nat_number_of_def number_of_is_id neg_def by simp
    1.40  
    1.41 -lemma of_nat_int [code_unfold_post]:
    1.42 +lemma of_nat_int: (* FIXME delete candidate *)
    1.43    "of_nat = int" by (simp add: int_def)
    1.44  
    1.45  lemma of_nat_aux_int [code_unfold]: