explicit conversion integer_of_nat already in Code_Numeral_Types;
authorhaftmann
Wed Feb 13 13:38:52 2013 +0100 (2013-02-13)
changeset 510957ae79f2e3cc7
parent 51094 84b03c49c223
child 51096 60e4b75fefe1
explicit conversion integer_of_nat already in Code_Numeral_Types;
tuned code postprocessor setup: present arithmetic results as plain numerals without conversions
src/HOL/Library/Code_Numeral_Types.thy
src/HOL/Library/Code_Target_Int.thy
src/HOL/Library/Code_Target_Nat.thy
     1.1 --- a/src/HOL/Library/Code_Numeral_Types.thy	Wed Feb 13 13:38:52 2013 +0100
     1.2 +++ b/src/HOL/Library/Code_Numeral_Types.thy	Wed Feb 13 13:38:52 2013 +0100
     1.3 @@ -83,6 +83,14 @@
     1.4    "int_of_integer (of_nat n) = of_nat n"
     1.5    by (induct n) simp_all
     1.6  
     1.7 +definition integer_of_nat :: "nat \<Rightarrow> integer"
     1.8 +where
     1.9 +  "integer_of_nat = of_nat"
    1.10 +
    1.11 +lemma int_of_integer_integer_of_nat [simp]:
    1.12 +  "int_of_integer (integer_of_nat n) = of_nat n"
    1.13 +  by (simp add: integer_of_nat_def)
    1.14 +  
    1.15  definition nat_of_integer :: "integer \<Rightarrow> nat"
    1.16  where
    1.17    "nat_of_integer k = Int.nat (int_of_integer k)"
    1.18 @@ -95,7 +103,11 @@
    1.19    "int_of_integer (of_int k) = k"
    1.20    by (induct k) (simp_all, simp only: neg_numeral_def numeral_One int_of_integer_uminus int_of_integer_one)
    1.21  
    1.22 -lemma integer_integer_of_int_eq_of_integer_integer_of_int [simp, code_abbrev]:
    1.23 +lemma nat_of_integer_integer_of_nat [simp]:
    1.24 +  "nat_of_integer (integer_of_nat n) = n"
    1.25 +  by (simp add: integer_of_nat_def)
    1.26 +
    1.27 +lemma integer_of_int_eq_of_int [simp, code_abbrev]:
    1.28    "integer_of_int = of_int"
    1.29    by rule (simp add: integer_eq_iff)
    1.30  
    1.31 @@ -785,6 +797,12 @@
    1.32  where
    1.33    "Nat = natural_of_integer"
    1.34  
    1.35 +lemma [code_post]:
    1.36 +  "Nat 0 = 0"
    1.37 +  "Nat 1 = 1"
    1.38 +  "Nat (numeral k) = numeral k"
    1.39 +  by (simp_all add: Nat_def nat_of_integer_def natural_of_integer_def)
    1.40 +
    1.41  lemma [code abstype]:
    1.42    "Nat (integer_of_natural n) = n"
    1.43    by (unfold Nat_def) (fact natural_of_integer_of_natural)
     2.1 --- a/src/HOL/Library/Code_Target_Int.thy	Wed Feb 13 13:38:52 2013 +0100
     2.2 +++ b/src/HOL/Library/Code_Target_Int.thy	Wed Feb 13 13:38:52 2013 +0100
     2.3 @@ -26,18 +26,18 @@
     2.4    by (simp add: integer_of_num_def fun_eq_iff)
     2.5  
     2.6  lemma [code_abbrev]:
     2.7 -  "int_of_integer (Code_Numeral_Types.Pos k) = Int.Pos k"
     2.8 +  "int_of_integer (numeral k) = Int.Pos k"
     2.9    by simp
    2.10  
    2.11  lemma [code_abbrev]:
    2.12 -  "int_of_integer (Code_Numeral_Types.Neg k) = Int.Neg k"
    2.13 +  "int_of_integer (neg_numeral k) = Int.Neg k"
    2.14    by simp
    2.15 -
    2.16 -lemma [code]:
    2.17 +  
    2.18 +lemma [code, symmetric, code_post]:
    2.19    "0 = int_of_integer 0"
    2.20    by simp
    2.21  
    2.22 -lemma [code]:
    2.23 +lemma [code, symmetric, code_post]:
    2.24    "1 = int_of_integer 1"
    2.25    by simp
    2.26  
     3.1 --- a/src/HOL/Library/Code_Target_Nat.thy	Wed Feb 13 13:38:52 2013 +0100
     3.2 +++ b/src/HOL/Library/Code_Target_Nat.thy	Wed Feb 13 13:38:52 2013 +0100
     3.3 @@ -14,13 +14,15 @@
     3.4  where
     3.5    "Nat = nat_of_integer"
     3.6  
     3.7 -definition integer_of_nat :: "nat \<Rightarrow> integer"
     3.8 -where
     3.9 -  [code_abbrev]: "integer_of_nat = of_nat"
    3.10 +lemma [code_post]:
    3.11 +  "Nat 0 = 0"
    3.12 +  "Nat 1 = 1"
    3.13 +  "Nat (numeral k) = numeral k"
    3.14 +  by (simp_all add: Nat_def nat_of_integer_def)
    3.15  
    3.16 -lemma int_of_integer_integer_of_nat [simp]:
    3.17 -  "int_of_integer (integer_of_nat n) = of_nat n"
    3.18 -  by (simp add: integer_of_nat_def)
    3.19 +lemma [code_abbrev]:
    3.20 +  "integer_of_nat = of_nat"
    3.21 +  by (fact integer_of_nat_def)
    3.22  
    3.23  lemma [code_unfold]:
    3.24    "Int.nat (int_of_integer k) = nat_of_integer k"
    3.25 @@ -35,7 +37,7 @@
    3.26    by (simp add: integer_of_nat_def)
    3.27  
    3.28  lemma [code_abbrev]:
    3.29 -  "nat_of_integer (Code_Numeral_Types.Pos k) = nat_of_num k"
    3.30 +  "nat_of_integer (numeral k) = nat_of_num k"
    3.31    by (simp add: nat_of_integer_def nat_of_num_numeral)
    3.32  
    3.33  lemma [code abstract]: