src/HOL/Library/Code_Target_Nat.thy
author haftmann
Wed Feb 13 13:38:52 2013 +0100 (2013-02-13)
changeset 51095 7ae79f2e3cc7
parent 50023 28f3263d4d1b
child 51113 222fb6cb2c3e
permissions -rw-r--r--
explicit conversion integer_of_nat already in Code_Numeral_Types;
tuned code postprocessor setup: present arithmetic results as plain numerals without conversions
     1 (*  Title:      HOL/Library/Code_Target_Nat.thy
     2     Author:     Stefan Berghofer, Florian Haftmann, TU Muenchen
     3 *)
     4 
     5 header {* Implementation of natural numbers by target-language integers *}
     6 
     7 theory Code_Target_Nat
     8 imports Main Code_Numeral_Types Code_Binary_Nat
     9 begin
    10 
    11 subsection {* Implementation for @{typ nat} *}
    12 
    13 definition Nat :: "integer \<Rightarrow> nat"
    14 where
    15   "Nat = nat_of_integer"
    16 
    17 lemma [code_post]:
    18   "Nat 0 = 0"
    19   "Nat 1 = 1"
    20   "Nat (numeral k) = numeral k"
    21   by (simp_all add: Nat_def nat_of_integer_def)
    22 
    23 lemma [code_abbrev]:
    24   "integer_of_nat = of_nat"
    25   by (fact integer_of_nat_def)
    26 
    27 lemma [code_unfold]:
    28   "Int.nat (int_of_integer k) = nat_of_integer k"
    29   by (simp add: nat_of_integer_def)
    30 
    31 lemma [code abstype]:
    32   "Code_Target_Nat.Nat (integer_of_nat n) = n"
    33   by (simp add: Nat_def integer_of_nat_def)
    34 
    35 lemma [code abstract]:
    36   "integer_of_nat (nat_of_integer k) = max 0 k"
    37   by (simp add: integer_of_nat_def)
    38 
    39 lemma [code_abbrev]:
    40   "nat_of_integer (numeral k) = nat_of_num k"
    41   by (simp add: nat_of_integer_def nat_of_num_numeral)
    42 
    43 lemma [code abstract]:
    44   "integer_of_nat (nat_of_num n) = integer_of_num n"
    45   by (simp add: integer_eq_iff integer_of_num_def nat_of_num_numeral)
    46 
    47 lemma [code abstract]:
    48   "integer_of_nat 0 = 0"
    49   by (simp add: integer_eq_iff integer_of_nat_def)
    50 
    51 lemma [code abstract]:
    52   "integer_of_nat 1 = 1"
    53   by (simp add: integer_eq_iff integer_of_nat_def)
    54 
    55 lemma [code abstract]:
    56   "integer_of_nat (m + n) = of_nat m + of_nat n"
    57   by (simp add: integer_eq_iff integer_of_nat_def)
    58 
    59 lemma [code abstract]:
    60   "integer_of_nat (Code_Binary_Nat.dup n) = Code_Numeral_Types.dup (of_nat n)"
    61   by (simp add: integer_eq_iff Code_Binary_Nat.dup_def integer_of_nat_def)
    62 
    63 lemma [code, code del]:
    64   "Code_Binary_Nat.sub = Code_Binary_Nat.sub" ..
    65 
    66 lemma [code abstract]:
    67   "integer_of_nat (m - n) = max 0 (of_nat m - of_nat n)"
    68   by (simp add: integer_eq_iff integer_of_nat_def)
    69 
    70 lemma [code abstract]:
    71   "integer_of_nat (m * n) = of_nat m * of_nat n"
    72   by (simp add: integer_eq_iff of_nat_mult integer_of_nat_def)
    73 
    74 lemma [code abstract]:
    75   "integer_of_nat (m div n) = of_nat m div of_nat n"
    76   by (simp add: integer_eq_iff zdiv_int integer_of_nat_def)
    77 
    78 lemma [code abstract]:
    79   "integer_of_nat (m mod n) = of_nat m mod of_nat n"
    80   by (simp add: integer_eq_iff zmod_int integer_of_nat_def)
    81 
    82 lemma [code]:
    83   "Divides.divmod_nat m n = (m div n, m mod n)"
    84   by (simp add: prod_eq_iff)
    85 
    86 lemma [code]:
    87   "HOL.equal m n = HOL.equal (of_nat m :: integer) (of_nat n)"
    88   by (simp add: equal integer_eq_iff)
    89 
    90 lemma [code]:
    91   "m \<le> n \<longleftrightarrow> (of_nat m :: integer) \<le> of_nat n"
    92   by simp
    93 
    94 lemma [code]:
    95   "m < n \<longleftrightarrow> (of_nat m :: integer) < of_nat n"
    96   by simp
    97 
    98 lemma num_of_nat_code [code]:
    99   "num_of_nat = num_of_integer \<circ> of_nat"
   100   by (simp add: fun_eq_iff num_of_integer_def integer_of_nat_def)
   101 
   102 lemma (in semiring_1) of_nat_code:
   103   "of_nat n = (if n = 0 then 0
   104      else let
   105        (m, q) = divmod_nat n 2;
   106        m' = 2 * of_nat m
   107      in if q = 0 then m' else m' + 1)"
   108 proof -
   109   from mod_div_equality have *: "of_nat n = of_nat (n div 2 * 2 + n mod 2)" by simp
   110   show ?thesis
   111     by (simp add: Let_def divmod_nat_div_mod mod_2_not_eq_zero_eq_one_nat
   112       of_nat_add [symmetric])
   113       (simp add: * mult_commute of_nat_mult add_commute)
   114 qed
   115 
   116 declare of_nat_code [code]
   117 
   118 definition int_of_nat :: "nat \<Rightarrow> int" where
   119   [code_abbrev]: "int_of_nat = of_nat"
   120 
   121 lemma [code]:
   122   "int_of_nat n = int_of_integer (of_nat n)"
   123   by (simp add: int_of_nat_def)
   124 
   125 lemma [code abstract]:
   126   "integer_of_nat (nat k) = max 0 (integer_of_int k)"
   127   by (simp add: integer_of_nat_def of_int_of_nat max_def)
   128 
   129 code_modulename SML
   130   Code_Target_Nat Arith
   131 
   132 code_modulename OCaml
   133   Code_Target_Nat Arith
   134 
   135 code_modulename Haskell
   136   Code_Target_Nat Arith
   137 
   138 end
   139