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