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