src/HOL/Library/Code_Target_Nat.thy
author haftmann
Sun Jun 23 21:16:07 2013 +0200 (2013-06-23)
changeset 52435 6646bb548c6b
parent 51143 0a2371e7ced3
child 53027 1774d569b604
permissions -rw-r--r--
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann@50023
     1
(*  Title:      HOL/Library/Code_Target_Nat.thy
haftmann@51113
     2
    Author:     Florian Haftmann, TU Muenchen
haftmann@50023
     3
*)
haftmann@50023
     4
haftmann@50023
     5
header {* Implementation of natural numbers by target-language integers *}
haftmann@50023
     6
haftmann@50023
     7
theory Code_Target_Nat
haftmann@51143
     8
imports Code_Abstract_Nat
haftmann@50023
     9
begin
haftmann@50023
    10
haftmann@50023
    11
subsection {* Implementation for @{typ nat} *}
haftmann@50023
    12
haftmann@51114
    13
lift_definition Nat :: "integer \<Rightarrow> nat"
haftmann@51114
    14
  is nat
haftmann@51114
    15
  .
haftmann@50023
    16
haftmann@51095
    17
lemma [code_post]:
haftmann@51095
    18
  "Nat 0 = 0"
haftmann@51095
    19
  "Nat 1 = 1"
haftmann@51095
    20
  "Nat (numeral k) = numeral k"
haftmann@51114
    21
  by (transfer, simp)+
haftmann@50023
    22
haftmann@51095
    23
lemma [code_abbrev]:
haftmann@51095
    24
  "integer_of_nat = of_nat"
haftmann@51114
    25
  by transfer rule
haftmann@50023
    26
haftmann@50023
    27
lemma [code_unfold]:
haftmann@50023
    28
  "Int.nat (int_of_integer k) = nat_of_integer k"
haftmann@51114
    29
  by transfer rule
haftmann@50023
    30
haftmann@50023
    31
lemma [code abstype]:
haftmann@50023
    32
  "Code_Target_Nat.Nat (integer_of_nat n) = n"
haftmann@51114
    33
  by transfer simp
haftmann@50023
    34
haftmann@50023
    35
lemma [code abstract]:
haftmann@50023
    36
  "integer_of_nat (nat_of_integer k) = max 0 k"
haftmann@51114
    37
  by transfer auto
haftmann@50023
    38
haftmann@50023
    39
lemma [code_abbrev]:
haftmann@51095
    40
  "nat_of_integer (numeral k) = nat_of_num k"
haftmann@51114
    41
  by transfer (simp add: nat_of_num_numeral)
haftmann@50023
    42
haftmann@50023
    43
lemma [code abstract]:
haftmann@50023
    44
  "integer_of_nat (nat_of_num n) = integer_of_num n"
haftmann@51114
    45
  by transfer (simp add: nat_of_num_numeral)
haftmann@50023
    46
haftmann@50023
    47
lemma [code abstract]:
haftmann@50023
    48
  "integer_of_nat 0 = 0"
haftmann@51114
    49
  by transfer simp
haftmann@50023
    50
haftmann@50023
    51
lemma [code abstract]:
haftmann@50023
    52
  "integer_of_nat 1 = 1"
haftmann@51114
    53
  by transfer simp
haftmann@50023
    54
haftmann@51113
    55
lemma [code]:
haftmann@51113
    56
  "Suc n = n + 1"
haftmann@51113
    57
  by simp
haftmann@51113
    58
haftmann@50023
    59
lemma [code abstract]:
haftmann@50023
    60
  "integer_of_nat (m + n) = of_nat m + of_nat n"
haftmann@51114
    61
  by transfer simp
haftmann@50023
    62
haftmann@50023
    63
lemma [code abstract]:
haftmann@50023
    64
  "integer_of_nat (m - n) = max 0 (of_nat m - of_nat n)"
haftmann@51114
    65
  by transfer simp
haftmann@50023
    66
haftmann@50023
    67
lemma [code abstract]:
haftmann@50023
    68
  "integer_of_nat (m * n) = of_nat m * of_nat n"
haftmann@51114
    69
  by transfer (simp add: of_nat_mult)
haftmann@50023
    70
haftmann@50023
    71
lemma [code abstract]:
haftmann@50023
    72
  "integer_of_nat (m div n) = of_nat m div of_nat n"
haftmann@51114
    73
  by transfer (simp add: zdiv_int)
haftmann@50023
    74
haftmann@50023
    75
lemma [code abstract]:
haftmann@50023
    76
  "integer_of_nat (m mod n) = of_nat m mod of_nat n"
haftmann@51114
    77
  by transfer (simp add: zmod_int)
haftmann@50023
    78
haftmann@50023
    79
lemma [code]:
haftmann@50023
    80
  "Divides.divmod_nat m n = (m div n, m mod n)"
haftmann@50023
    81
  by (simp add: prod_eq_iff)
haftmann@50023
    82
haftmann@50023
    83
lemma [code]:
haftmann@50023
    84
  "HOL.equal m n = HOL.equal (of_nat m :: integer) (of_nat n)"
haftmann@51114
    85
  by transfer (simp add: equal)
haftmann@50023
    86
haftmann@50023
    87
lemma [code]:
haftmann@50023
    88
  "m \<le> n \<longleftrightarrow> (of_nat m :: integer) \<le> of_nat n"
haftmann@50023
    89
  by simp
haftmann@50023
    90
haftmann@50023
    91
lemma [code]:
haftmann@50023
    92
  "m < n \<longleftrightarrow> (of_nat m :: integer) < of_nat n"
haftmann@50023
    93
  by simp
haftmann@50023
    94
haftmann@50023
    95
lemma num_of_nat_code [code]:
haftmann@50023
    96
  "num_of_nat = num_of_integer \<circ> of_nat"
haftmann@51114
    97
  by transfer (simp add: fun_eq_iff)
haftmann@50023
    98
haftmann@50023
    99
lemma (in semiring_1) of_nat_code:
haftmann@50023
   100
  "of_nat n = (if n = 0 then 0
haftmann@50023
   101
     else let
haftmann@50023
   102
       (m, q) = divmod_nat n 2;
haftmann@50023
   103
       m' = 2 * of_nat m
haftmann@50023
   104
     in if q = 0 then m' else m' + 1)"
haftmann@50023
   105
proof -
haftmann@50023
   106
  from mod_div_equality have *: "of_nat n = of_nat (n div 2 * 2 + n mod 2)" by simp
haftmann@50023
   107
  show ?thesis
haftmann@50023
   108
    by (simp add: Let_def divmod_nat_div_mod mod_2_not_eq_zero_eq_one_nat
haftmann@50023
   109
      of_nat_add [symmetric])
haftmann@50023
   110
      (simp add: * mult_commute of_nat_mult add_commute)
haftmann@50023
   111
qed
haftmann@50023
   112
haftmann@50023
   113
declare of_nat_code [code]
haftmann@50023
   114
haftmann@50023
   115
definition int_of_nat :: "nat \<Rightarrow> int" where
haftmann@50023
   116
  [code_abbrev]: "int_of_nat = of_nat"
haftmann@50023
   117
haftmann@50023
   118
lemma [code]:
haftmann@50023
   119
  "int_of_nat n = int_of_integer (of_nat n)"
haftmann@50023
   120
  by (simp add: int_of_nat_def)
haftmann@50023
   121
haftmann@50023
   122
lemma [code abstract]:
haftmann@50023
   123
  "integer_of_nat (nat k) = max 0 (integer_of_int k)"
haftmann@51114
   124
  by transfer auto
haftmann@50023
   125
haftmann@52435
   126
code_identifier
haftmann@52435
   127
  code_module Code_Target_Nat \<rightharpoonup>
haftmann@52435
   128
    (SML) Arith and (OCaml) Arith and (Haskell) Arith
haftmann@50023
   129
haftmann@50023
   130
end
haftmann@50023
   131