src/HOL/Library/Code_Target_Nat.thy
author Manuel Eberl <eberlm@in.tum.de>
Mon Mar 26 16:14:16 2018 +0200 (19 months ago)
changeset 67951 655aa11359dc
parent 66808 1907167b6038
child 68028 1f9f973eed2a
permissions -rw-r--r--
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
haftmann@50023
     1
(*  Title:      HOL/Library/Code_Target_Nat.thy
haftmann@51113
     2
    Author:     Florian Haftmann, TU Muenchen
haftmann@50023
     3
*)
haftmann@50023
     4
wenzelm@60500
     5
section \<open>Implementation of natural numbers by target-language integers\<close>
haftmann@50023
     6
haftmann@50023
     7
theory Code_Target_Nat
haftmann@51143
     8
imports Code_Abstract_Nat
haftmann@50023
     9
begin
haftmann@50023
    10
wenzelm@60500
    11
subsection \<open>Implementation for @{typ nat}\<close>
haftmann@50023
    12
kuncar@55736
    13
context
kuncar@55736
    14
includes natural.lifting integer.lifting
kuncar@55736
    15
begin
kuncar@55736
    16
haftmann@51114
    17
lift_definition Nat :: "integer \<Rightarrow> nat"
haftmann@51114
    18
  is nat
haftmann@51114
    19
  .
haftmann@50023
    20
haftmann@51095
    21
lemma [code_post]:
haftmann@51095
    22
  "Nat 0 = 0"
haftmann@51095
    23
  "Nat 1 = 1"
haftmann@51095
    24
  "Nat (numeral k) = numeral k"
haftmann@51114
    25
  by (transfer, simp)+
haftmann@50023
    26
haftmann@51095
    27
lemma [code_abbrev]:
haftmann@51095
    28
  "integer_of_nat = of_nat"
haftmann@51114
    29
  by transfer rule
haftmann@50023
    30
haftmann@50023
    31
lemma [code_unfold]:
haftmann@50023
    32
  "Int.nat (int_of_integer k) = nat_of_integer k"
haftmann@51114
    33
  by transfer rule
haftmann@50023
    34
haftmann@50023
    35
lemma [code abstype]:
haftmann@50023
    36
  "Code_Target_Nat.Nat (integer_of_nat n) = n"
haftmann@51114
    37
  by transfer simp
haftmann@50023
    38
haftmann@50023
    39
lemma [code abstract]:
haftmann@50023
    40
  "integer_of_nat (nat_of_integer k) = max 0 k"
haftmann@51114
    41
  by transfer auto
haftmann@50023
    42
haftmann@50023
    43
lemma [code_abbrev]:
haftmann@51095
    44
  "nat_of_integer (numeral k) = nat_of_num k"
haftmann@51114
    45
  by transfer (simp add: nat_of_num_numeral)
haftmann@50023
    46
haftmann@64997
    47
context
haftmann@64997
    48
begin  
haftmann@64997
    49
haftmann@64997
    50
qualified definition natural :: "num \<Rightarrow> nat"
haftmann@64997
    51
  where [simp]: "natural = nat_of_num"
haftmann@64997
    52
haftmann@64997
    53
lemma [code_computation_unfold]:
haftmann@64997
    54
  "numeral = natural"
haftmann@64997
    55
  "nat_of_num = natural"
haftmann@64997
    56
  by (simp_all add: nat_of_num_numeral)
haftmann@64997
    57
haftmann@64997
    58
end
haftmann@64997
    59
haftmann@50023
    60
lemma [code abstract]:
haftmann@50023
    61
  "integer_of_nat (nat_of_num n) = integer_of_num n"
haftmann@66190
    62
  by (simp add: nat_of_num_numeral integer_of_nat_numeral)
haftmann@50023
    63
haftmann@50023
    64
lemma [code abstract]:
haftmann@50023
    65
  "integer_of_nat 0 = 0"
haftmann@51114
    66
  by transfer simp
haftmann@50023
    67
haftmann@50023
    68
lemma [code abstract]:
haftmann@50023
    69
  "integer_of_nat 1 = 1"
haftmann@51114
    70
  by transfer simp
haftmann@50023
    71
haftmann@51113
    72
lemma [code]:
haftmann@51113
    73
  "Suc n = n + 1"
haftmann@51113
    74
  by simp
haftmann@51113
    75
haftmann@50023
    76
lemma [code abstract]:
haftmann@50023
    77
  "integer_of_nat (m + n) = of_nat m + of_nat n"
haftmann@51114
    78
  by transfer simp
haftmann@50023
    79
haftmann@50023
    80
lemma [code abstract]:
haftmann@50023
    81
  "integer_of_nat (m - n) = max 0 (of_nat m - of_nat n)"
haftmann@51114
    82
  by transfer simp
haftmann@50023
    83
haftmann@50023
    84
lemma [code abstract]:
haftmann@50023
    85
  "integer_of_nat (m * n) = of_nat m * of_nat n"
haftmann@51114
    86
  by transfer (simp add: of_nat_mult)
haftmann@50023
    87
haftmann@50023
    88
lemma [code abstract]:
haftmann@50023
    89
  "integer_of_nat (m div n) = of_nat m div of_nat n"
haftmann@51114
    90
  by transfer (simp add: zdiv_int)
haftmann@50023
    91
haftmann@50023
    92
lemma [code abstract]:
haftmann@50023
    93
  "integer_of_nat (m mod n) = of_nat m mod of_nat n"
haftmann@51114
    94
  by transfer (simp add: zmod_int)
haftmann@50023
    95
haftmann@50023
    96
lemma [code]:
haftmann@50023
    97
  "Divides.divmod_nat m n = (m div n, m mod n)"
haftmann@66808
    98
  by (fact divmod_nat_def)
haftmann@50023
    99
haftmann@50023
   100
lemma [code]:
haftmann@61275
   101
  "divmod m n = map_prod nat_of_integer nat_of_integer (divmod m n)"
haftmann@61275
   102
  by (simp only: prod_eq_iff divmod_def map_prod_def case_prod_beta fst_conv snd_conv)
haftmann@61275
   103
    (transfer, simp_all only: nat_div_distrib nat_mod_distrib
haftmann@61275
   104
        zero_le_numeral nat_numeral)
haftmann@61275
   105
  
haftmann@61275
   106
lemma [code]:
haftmann@50023
   107
  "HOL.equal m n = HOL.equal (of_nat m :: integer) (of_nat n)"
haftmann@51114
   108
  by transfer (simp add: equal)
haftmann@50023
   109
haftmann@50023
   110
lemma [code]:
haftmann@50023
   111
  "m \<le> n \<longleftrightarrow> (of_nat m :: integer) \<le> of_nat n"
haftmann@50023
   112
  by simp
haftmann@50023
   113
haftmann@50023
   114
lemma [code]:
haftmann@50023
   115
  "m < n \<longleftrightarrow> (of_nat m :: integer) < of_nat n"
haftmann@50023
   116
  by simp
haftmann@50023
   117
haftmann@50023
   118
lemma num_of_nat_code [code]:
haftmann@50023
   119
  "num_of_nat = num_of_integer \<circ> of_nat"
haftmann@51114
   120
  by transfer (simp add: fun_eq_iff)
haftmann@50023
   121
kuncar@55736
   122
end
kuncar@55736
   123
haftmann@54796
   124
lemma (in semiring_1) of_nat_code_if:
haftmann@50023
   125
  "of_nat n = (if n = 0 then 0
haftmann@50023
   126
     else let
haftmann@61433
   127
       (m, q) = Divides.divmod_nat n 2;
haftmann@50023
   128
       m' = 2 * of_nat m
haftmann@50023
   129
     in if q = 0 then m' else m' + 1)"
haftmann@50023
   130
proof -
haftmann@64242
   131
  from div_mult_mod_eq have *: "of_nat n = of_nat (n div 2 * 2 + n mod 2)" by simp
haftmann@50023
   132
  show ?thesis
haftmann@66808
   133
    by (simp add: Let_def divmod_nat_def of_nat_add [symmetric])
haftmann@57512
   134
      (simp add: * mult.commute of_nat_mult add.commute)
haftmann@50023
   135
qed
haftmann@50023
   136
haftmann@54796
   137
declare of_nat_code_if [code]
haftmann@50023
   138
haftmann@50023
   139
definition int_of_nat :: "nat \<Rightarrow> int" where
haftmann@50023
   140
  [code_abbrev]: "int_of_nat = of_nat"
haftmann@50023
   141
haftmann@50023
   142
lemma [code]:
haftmann@50023
   143
  "int_of_nat n = int_of_integer (of_nat n)"
haftmann@50023
   144
  by (simp add: int_of_nat_def)
haftmann@50023
   145
haftmann@50023
   146
lemma [code abstract]:
haftmann@50023
   147
  "integer_of_nat (nat k) = max 0 (integer_of_int k)"
kuncar@55736
   148
  including integer.lifting by transfer auto
haftmann@50023
   149
Andreas@53027
   150
lemma term_of_nat_code [code]:
wenzelm@61585
   151
  \<comment> \<open>Use @{term Code_Numeral.nat_of_integer} in term reconstruction
Andreas@53027
   152
        instead of @{term Code_Target_Nat.Nat} such that reconstructed
wenzelm@60500
   153
        terms can be fed back to the code generator\<close>
Andreas@53027
   154
  "term_of_class.term_of n =
Andreas@53027
   155
   Code_Evaluation.App
Andreas@53027
   156
     (Code_Evaluation.Const (STR ''Code_Numeral.nat_of_integer'')
Andreas@53027
   157
        (typerep.Typerep (STR ''fun'')
Andreas@53027
   158
           [typerep.Typerep (STR ''Code_Numeral.integer'') [],
Andreas@53027
   159
         typerep.Typerep (STR ''Nat.nat'') []]))
Andreas@53027
   160
     (term_of_class.term_of (integer_of_nat n))"
haftmann@54796
   161
  by (simp add: term_of_anything)
Andreas@53027
   162
Andreas@53027
   163
lemma nat_of_integer_code_post [code_post]:
Andreas@53027
   164
  "nat_of_integer 0 = 0"
Andreas@53027
   165
  "nat_of_integer 1 = 1"
Andreas@53027
   166
  "nat_of_integer (numeral k) = numeral k"
kuncar@55736
   167
  including integer.lifting by (transfer, simp)+
Andreas@53027
   168
haftmann@52435
   169
code_identifier
haftmann@52435
   170
  code_module Code_Target_Nat \<rightharpoonup>
haftmann@52435
   171
    (SML) Arith and (OCaml) Arith and (Haskell) Arith
haftmann@50023
   172
haftmann@50023
   173
end