src/HOL/Library/Code_Target_Nat.thy
 author Christian Sternagel Thu Dec 13 13:11:38 2012 +0100 (2012-12-13) changeset 50516 ed6b40d15d1c parent 50023 28f3263d4d1b child 51095 7ae79f2e3cc7 permissions -rw-r--r--
renamed "emb" to "list_hembeq";
make "list_hembeq" reflexive independent of the base order;
renamed "sub" to "sublisteq";
dropped "transp_on" (state transitivity explicitly instead);
no need to hide "sub" after renaming;
replaced some ASCII symbols by proper Isabelle symbols;
NEWS
```     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 definition integer_of_nat :: "nat \<Rightarrow> integer"
```
```    18 where
```
```    19   [code_abbrev]: "integer_of_nat = of_nat"
```
```    20
```
```    21 lemma int_of_integer_integer_of_nat [simp]:
```
```    22   "int_of_integer (integer_of_nat n) = of_nat n"
```
```    23   by (simp add: integer_of_nat_def)
```
```    24
```
```    25 lemma [code_unfold]:
```
```    26   "Int.nat (int_of_integer k) = nat_of_integer k"
```
```    27   by (simp add: nat_of_integer_def)
```
```    28
```
```    29 lemma [code abstype]:
```
```    30   "Code_Target_Nat.Nat (integer_of_nat n) = n"
```
```    31   by (simp add: Nat_def integer_of_nat_def)
```
```    32
```
```    33 lemma [code abstract]:
```
```    34   "integer_of_nat (nat_of_integer k) = max 0 k"
```
```    35   by (simp add: integer_of_nat_def)
```
```    36
```
```    37 lemma [code_abbrev]:
```
```    38   "nat_of_integer (Code_Numeral_Types.Pos k) = nat_of_num k"
```
```    39   by (simp add: nat_of_integer_def nat_of_num_numeral)
```
```    40
```
```    41 lemma [code abstract]:
```
```    42   "integer_of_nat (nat_of_num n) = integer_of_num n"
```
```    43   by (simp add: integer_eq_iff integer_of_num_def nat_of_num_numeral)
```
```    44
```
```    45 lemma [code abstract]:
```
```    46   "integer_of_nat 0 = 0"
```
```    47   by (simp add: integer_eq_iff integer_of_nat_def)
```
```    48
```
```    49 lemma [code abstract]:
```
```    50   "integer_of_nat 1 = 1"
```
```    51   by (simp add: integer_eq_iff integer_of_nat_def)
```
```    52
```
```    53 lemma [code abstract]:
```
```    54   "integer_of_nat (m + n) = of_nat m + of_nat n"
```
```    55   by (simp add: integer_eq_iff integer_of_nat_def)
```
```    56
```
```    57 lemma [code abstract]:
```
```    58   "integer_of_nat (Code_Binary_Nat.dup n) = Code_Numeral_Types.dup (of_nat n)"
```
```    59   by (simp add: integer_eq_iff Code_Binary_Nat.dup_def integer_of_nat_def)
```
```    60
```
```    61 lemma [code, code del]:
```
```    62   "Code_Binary_Nat.sub = Code_Binary_Nat.sub" ..
```
```    63
```
```    64 lemma [code abstract]:
```
```    65   "integer_of_nat (m - n) = max 0 (of_nat m - of_nat n)"
```
```    66   by (simp add: integer_eq_iff integer_of_nat_def)
```
```    67
```
```    68 lemma [code abstract]:
```
```    69   "integer_of_nat (m * n) = of_nat m * of_nat n"
```
```    70   by (simp add: integer_eq_iff of_nat_mult integer_of_nat_def)
```
```    71
```
```    72 lemma [code abstract]:
```
```    73   "integer_of_nat (m div n) = of_nat m div of_nat n"
```
```    74   by (simp add: integer_eq_iff zdiv_int integer_of_nat_def)
```
```    75
```
```    76 lemma [code abstract]:
```
```    77   "integer_of_nat (m mod n) = of_nat m mod of_nat n"
```
```    78   by (simp add: integer_eq_iff zmod_int integer_of_nat_def)
```
```    79
```
```    80 lemma [code]:
```
```    81   "Divides.divmod_nat m n = (m div n, m mod n)"
```
```    82   by (simp add: prod_eq_iff)
```
```    83
```
```    84 lemma [code]:
```
```    85   "HOL.equal m n = HOL.equal (of_nat m :: integer) (of_nat n)"
```
```    86   by (simp add: equal integer_eq_iff)
```
```    87
```
```    88 lemma [code]:
```
```    89   "m \<le> n \<longleftrightarrow> (of_nat m :: integer) \<le> of_nat n"
```
```    90   by simp
```
```    91
```
```    92 lemma [code]:
```
```    93   "m < n \<longleftrightarrow> (of_nat m :: integer) < of_nat n"
```
```    94   by simp
```
```    95
```
```    96 lemma num_of_nat_code [code]:
```
```    97   "num_of_nat = num_of_integer \<circ> of_nat"
```
```    98   by (simp add: fun_eq_iff num_of_integer_def integer_of_nat_def)
```
```    99
```
```   100 lemma (in semiring_1) of_nat_code:
```
```   101   "of_nat n = (if n = 0 then 0
```
```   102      else let
```
```   103        (m, q) = divmod_nat n 2;
```
```   104        m' = 2 * of_nat m
```
```   105      in if q = 0 then m' else m' + 1)"
```
```   106 proof -
```
```   107   from mod_div_equality have *: "of_nat n = of_nat (n div 2 * 2 + n mod 2)" by simp
```
```   108   show ?thesis
```
```   109     by (simp add: Let_def divmod_nat_div_mod mod_2_not_eq_zero_eq_one_nat
```
```   110       of_nat_add [symmetric])
```
```   111       (simp add: * mult_commute of_nat_mult add_commute)
```
```   112 qed
```
```   113
```
```   114 declare of_nat_code [code]
```
```   115
```
```   116 definition int_of_nat :: "nat \<Rightarrow> int" where
```
```   117   [code_abbrev]: "int_of_nat = of_nat"
```
```   118
```
```   119 lemma [code]:
```
```   120   "int_of_nat n = int_of_integer (of_nat n)"
```
```   121   by (simp add: int_of_nat_def)
```
```   122
```
```   123 lemma [code abstract]:
```
```   124   "integer_of_nat (nat k) = max 0 (integer_of_int k)"
```
```   125   by (simp add: integer_of_nat_def of_int_of_nat max_def)
```
```   126
```
```   127 code_modulename SML
```
```   128   Code_Target_Nat Arith
```
```   129
```
```   130 code_modulename OCaml
```
```   131   Code_Target_Nat Arith
```
```   132
```
```   133 code_modulename Haskell
```
```   134   Code_Target_Nat Arith
```
```   135
```
```   136 end
```
```   137
```