src/HOL/Library/Code_Target_Nat.thy
changeset 50023 28f3263d4d1b
child 51095 7ae79f2e3cc7
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Code_Target_Nat.thy	Thu Nov 08 10:02:38 2012 +0100
     1.3 @@ -0,0 +1,137 @@
     1.4 +(*  Title:      HOL/Library/Code_Target_Nat.thy
     1.5 +    Author:     Stefan Berghofer, Florian Haftmann, TU Muenchen
     1.6 +*)
     1.7 +
     1.8 +header {* Implementation of natural numbers by target-language integers *}
     1.9 +
    1.10 +theory Code_Target_Nat
    1.11 +imports Main Code_Numeral_Types Code_Binary_Nat
    1.12 +begin
    1.13 +
    1.14 +subsection {* Implementation for @{typ nat} *}
    1.15 +
    1.16 +definition Nat :: "integer \<Rightarrow> nat"
    1.17 +where
    1.18 +  "Nat = nat_of_integer"
    1.19 +
    1.20 +definition integer_of_nat :: "nat \<Rightarrow> integer"
    1.21 +where
    1.22 +  [code_abbrev]: "integer_of_nat = of_nat"
    1.23 +
    1.24 +lemma int_of_integer_integer_of_nat [simp]:
    1.25 +  "int_of_integer (integer_of_nat n) = of_nat n"
    1.26 +  by (simp add: integer_of_nat_def)
    1.27 +
    1.28 +lemma [code_unfold]:
    1.29 +  "Int.nat (int_of_integer k) = nat_of_integer k"
    1.30 +  by (simp add: nat_of_integer_def)
    1.31 +
    1.32 +lemma [code abstype]:
    1.33 +  "Code_Target_Nat.Nat (integer_of_nat n) = n"
    1.34 +  by (simp add: Nat_def integer_of_nat_def)
    1.35 +
    1.36 +lemma [code abstract]:
    1.37 +  "integer_of_nat (nat_of_integer k) = max 0 k"
    1.38 +  by (simp add: integer_of_nat_def)
    1.39 +
    1.40 +lemma [code_abbrev]:
    1.41 +  "nat_of_integer (Code_Numeral_Types.Pos k) = nat_of_num k"
    1.42 +  by (simp add: nat_of_integer_def nat_of_num_numeral)
    1.43 +
    1.44 +lemma [code abstract]:
    1.45 +  "integer_of_nat (nat_of_num n) = integer_of_num n"
    1.46 +  by (simp add: integer_eq_iff integer_of_num_def nat_of_num_numeral)
    1.47 +
    1.48 +lemma [code abstract]:
    1.49 +  "integer_of_nat 0 = 0"
    1.50 +  by (simp add: integer_eq_iff integer_of_nat_def)
    1.51 +
    1.52 +lemma [code abstract]:
    1.53 +  "integer_of_nat 1 = 1"
    1.54 +  by (simp add: integer_eq_iff integer_of_nat_def)
    1.55 +
    1.56 +lemma [code abstract]:
    1.57 +  "integer_of_nat (m + n) = of_nat m + of_nat n"
    1.58 +  by (simp add: integer_eq_iff integer_of_nat_def)
    1.59 +
    1.60 +lemma [code abstract]:
    1.61 +  "integer_of_nat (Code_Binary_Nat.dup n) = Code_Numeral_Types.dup (of_nat n)"
    1.62 +  by (simp add: integer_eq_iff Code_Binary_Nat.dup_def integer_of_nat_def)
    1.63 +
    1.64 +lemma [code, code del]:
    1.65 +  "Code_Binary_Nat.sub = Code_Binary_Nat.sub" ..
    1.66 +
    1.67 +lemma [code abstract]:
    1.68 +  "integer_of_nat (m - n) = max 0 (of_nat m - of_nat n)"
    1.69 +  by (simp add: integer_eq_iff integer_of_nat_def)
    1.70 +
    1.71 +lemma [code abstract]:
    1.72 +  "integer_of_nat (m * n) = of_nat m * of_nat n"
    1.73 +  by (simp add: integer_eq_iff of_nat_mult integer_of_nat_def)
    1.74 +
    1.75 +lemma [code abstract]:
    1.76 +  "integer_of_nat (m div n) = of_nat m div of_nat n"
    1.77 +  by (simp add: integer_eq_iff zdiv_int integer_of_nat_def)
    1.78 +
    1.79 +lemma [code abstract]:
    1.80 +  "integer_of_nat (m mod n) = of_nat m mod of_nat n"
    1.81 +  by (simp add: integer_eq_iff zmod_int integer_of_nat_def)
    1.82 +
    1.83 +lemma [code]:
    1.84 +  "Divides.divmod_nat m n = (m div n, m mod n)"
    1.85 +  by (simp add: prod_eq_iff)
    1.86 +
    1.87 +lemma [code]:
    1.88 +  "HOL.equal m n = HOL.equal (of_nat m :: integer) (of_nat n)"
    1.89 +  by (simp add: equal integer_eq_iff)
    1.90 +
    1.91 +lemma [code]:
    1.92 +  "m \<le> n \<longleftrightarrow> (of_nat m :: integer) \<le> of_nat n"
    1.93 +  by simp
    1.94 +
    1.95 +lemma [code]:
    1.96 +  "m < n \<longleftrightarrow> (of_nat m :: integer) < of_nat n"
    1.97 +  by simp
    1.98 +
    1.99 +lemma num_of_nat_code [code]:
   1.100 +  "num_of_nat = num_of_integer \<circ> of_nat"
   1.101 +  by (simp add: fun_eq_iff num_of_integer_def integer_of_nat_def)
   1.102 +
   1.103 +lemma (in semiring_1) of_nat_code:
   1.104 +  "of_nat n = (if n = 0 then 0
   1.105 +     else let
   1.106 +       (m, q) = divmod_nat n 2;
   1.107 +       m' = 2 * of_nat m
   1.108 +     in if q = 0 then m' else m' + 1)"
   1.109 +proof -
   1.110 +  from mod_div_equality have *: "of_nat n = of_nat (n div 2 * 2 + n mod 2)" by simp
   1.111 +  show ?thesis
   1.112 +    by (simp add: Let_def divmod_nat_div_mod mod_2_not_eq_zero_eq_one_nat
   1.113 +      of_nat_add [symmetric])
   1.114 +      (simp add: * mult_commute of_nat_mult add_commute)
   1.115 +qed
   1.116 +
   1.117 +declare of_nat_code [code]
   1.118 +
   1.119 +definition int_of_nat :: "nat \<Rightarrow> int" where
   1.120 +  [code_abbrev]: "int_of_nat = of_nat"
   1.121 +
   1.122 +lemma [code]:
   1.123 +  "int_of_nat n = int_of_integer (of_nat n)"
   1.124 +  by (simp add: int_of_nat_def)
   1.125 +
   1.126 +lemma [code abstract]:
   1.127 +  "integer_of_nat (nat k) = max 0 (integer_of_int k)"
   1.128 +  by (simp add: integer_of_nat_def of_int_of_nat max_def)
   1.129 +
   1.130 +code_modulename SML
   1.131 +  Code_Target_Nat Arith
   1.132 +
   1.133 +code_modulename OCaml
   1.134 +  Code_Target_Nat Arith
   1.135 +
   1.136 +code_modulename Haskell
   1.137 +  Code_Target_Nat Arith
   1.138 +
   1.139 +end
   1.140 +