src/HOL/Code_Numeral.thy
changeset 51143 0a2371e7ced3
parent 49962 a8cc904a6820
child 51375 d9e62d9c98de
     1.1 --- a/src/HOL/Code_Numeral.thy	Fri Feb 15 08:31:30 2013 +0100
     1.2 +++ b/src/HOL/Code_Numeral.thy	Fri Feb 15 08:31:31 2013 +0100
     1.3 @@ -1,337 +1,614 @@
     1.4 -(* Author: Florian Haftmann, TU Muenchen *)
     1.5 +(*  Title:      HOL/Code_Numeral.thy
     1.6 +    Author:     Florian Haftmann, TU Muenchen
     1.7 +*)
     1.8  
     1.9 -header {* Type of target language numerals *}
    1.10 +header {* Numeric types for code generation onto target language numerals only *}
    1.11  
    1.12  theory Code_Numeral
    1.13 -imports Nat_Transfer Divides
    1.14 +imports Nat_Transfer Divides Lifting
    1.15 +begin
    1.16 +
    1.17 +subsection {* Type of target language integers *}
    1.18 +
    1.19 +typedef integer = "UNIV \<Colon> int set"
    1.20 +  morphisms int_of_integer integer_of_int ..
    1.21 +
    1.22 +setup_lifting (no_code) type_definition_integer
    1.23 +
    1.24 +lemma integer_eq_iff:
    1.25 +  "k = l \<longleftrightarrow> int_of_integer k = int_of_integer l"
    1.26 +  by transfer rule
    1.27 +
    1.28 +lemma integer_eqI:
    1.29 +  "int_of_integer k = int_of_integer l \<Longrightarrow> k = l"
    1.30 +  using integer_eq_iff [of k l] by simp
    1.31 +
    1.32 +lemma int_of_integer_integer_of_int [simp]:
    1.33 +  "int_of_integer (integer_of_int k) = k"
    1.34 +  by transfer rule
    1.35 +
    1.36 +lemma integer_of_int_int_of_integer [simp]:
    1.37 +  "integer_of_int (int_of_integer k) = k"
    1.38 +  by transfer rule
    1.39 +
    1.40 +instantiation integer :: ring_1
    1.41  begin
    1.42  
    1.43 -text {*
    1.44 -  Code numerals are isomorphic to HOL @{typ nat} but
    1.45 -  mapped to target-language builtin numerals.
    1.46 -*}
    1.47 +lift_definition zero_integer :: integer
    1.48 +  is "0 :: int"
    1.49 +  .
    1.50 +
    1.51 +declare zero_integer.rep_eq [simp]
    1.52  
    1.53 -subsection {* Datatype of target language numerals *}
    1.54 +lift_definition one_integer :: integer
    1.55 +  is "1 :: int"
    1.56 +  .
    1.57 +
    1.58 +declare one_integer.rep_eq [simp]
    1.59  
    1.60 -typedef code_numeral = "UNIV \<Colon> nat set"
    1.61 -  morphisms nat_of of_nat ..
    1.62 +lift_definition plus_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
    1.63 +  is "plus :: int \<Rightarrow> int \<Rightarrow> int"
    1.64 +  .
    1.65 +
    1.66 +declare plus_integer.rep_eq [simp]
    1.67  
    1.68 -lemma of_nat_nat_of [simp]:
    1.69 -  "of_nat (nat_of k) = k"
    1.70 -  by (rule nat_of_inverse)
    1.71 +lift_definition uminus_integer :: "integer \<Rightarrow> integer"
    1.72 +  is "uminus :: int \<Rightarrow> int"
    1.73 +  .
    1.74 +
    1.75 +declare uminus_integer.rep_eq [simp]
    1.76  
    1.77 -lemma nat_of_of_nat [simp]:
    1.78 -  "nat_of (of_nat n) = n"
    1.79 -  by (rule of_nat_inverse) (rule UNIV_I)
    1.80 +lift_definition minus_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
    1.81 +  is "minus :: int \<Rightarrow> int \<Rightarrow> int"
    1.82 +  .
    1.83 +
    1.84 +declare minus_integer.rep_eq [simp]
    1.85  
    1.86 -lemma [measure_function]:
    1.87 -  "is_measure nat_of" by (rule is_measure_trivial)
    1.88 +lift_definition times_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
    1.89 +  is "times :: int \<Rightarrow> int \<Rightarrow> int"
    1.90 +  .
    1.91 +
    1.92 +declare times_integer.rep_eq [simp]
    1.93  
    1.94 -lemma code_numeral:
    1.95 -  "(\<And>n\<Colon>code_numeral. PROP P n) \<equiv> (\<And>n\<Colon>nat. PROP P (of_nat n))"
    1.96 -proof
    1.97 -  fix n :: nat
    1.98 -  assume "\<And>n\<Colon>code_numeral. PROP P n"
    1.99 -  then show "PROP P (of_nat n)" .
   1.100 -next
   1.101 -  fix n :: code_numeral
   1.102 -  assume "\<And>n\<Colon>nat. PROP P (of_nat n)"
   1.103 -  then have "PROP P (of_nat (nat_of n))" .
   1.104 -  then show "PROP P n" by simp
   1.105 +instance proof
   1.106 +qed (transfer, simp add: algebra_simps)+
   1.107 +
   1.108 +end
   1.109 +
   1.110 +lemma [transfer_rule]:
   1.111 +  "fun_rel HOL.eq cr_integer (of_nat :: nat \<Rightarrow> int) (of_nat :: nat \<Rightarrow> integer)"
   1.112 +  by (unfold of_nat_def [abs_def])  transfer_prover
   1.113 +
   1.114 +lemma [transfer_rule]:
   1.115 +  "fun_rel HOL.eq cr_integer (\<lambda>k :: int. k :: int) (of_int :: int \<Rightarrow> integer)"
   1.116 +proof -
   1.117 +  have "fun_rel HOL.eq cr_integer (of_int :: int \<Rightarrow> int) (of_int :: int \<Rightarrow> integer)"
   1.118 +    by (unfold of_int_of_nat [abs_def]) transfer_prover
   1.119 +  then show ?thesis by (simp add: id_def)
   1.120  qed
   1.121  
   1.122 -lemma code_numeral_case:
   1.123 -  assumes "\<And>n. k = of_nat n \<Longrightarrow> P"
   1.124 -  shows P
   1.125 -  by (rule assms [of "nat_of k"]) simp
   1.126 -
   1.127 -lemma code_numeral_induct_raw:
   1.128 -  assumes "\<And>n. P (of_nat n)"
   1.129 -  shows "P k"
   1.130 +lemma [transfer_rule]:
   1.131 +  "fun_rel HOL.eq cr_integer (numeral :: num \<Rightarrow> int) (numeral :: num \<Rightarrow> integer)"
   1.132  proof -
   1.133 -  from assms have "P (of_nat (nat_of k))" .
   1.134 +  have "fun_rel HOL.eq cr_integer (numeral :: num \<Rightarrow> int) (\<lambda>n. of_int (numeral n))"
   1.135 +    by transfer_prover
   1.136    then show ?thesis by simp
   1.137  qed
   1.138  
   1.139 -lemma nat_of_inject [simp]:
   1.140 -  "nat_of k = nat_of l \<longleftrightarrow> k = l"
   1.141 -  by (rule nat_of_inject)
   1.142 +lemma [transfer_rule]:
   1.143 +  "fun_rel HOL.eq cr_integer (neg_numeral :: num \<Rightarrow> int) (neg_numeral :: num \<Rightarrow> integer)"
   1.144 +  by (unfold neg_numeral_def [abs_def]) transfer_prover
   1.145 +
   1.146 +lemma [transfer_rule]:
   1.147 +  "fun_rel HOL.eq (fun_rel HOL.eq cr_integer) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> int) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> integer)"
   1.148 +  by (unfold Num.sub_def [abs_def]) transfer_prover
   1.149 +
   1.150 +lemma int_of_integer_of_nat [simp]:
   1.151 +  "int_of_integer (of_nat n) = of_nat n"
   1.152 +  by transfer rule
   1.153 +
   1.154 +lift_definition integer_of_nat :: "nat \<Rightarrow> integer"
   1.155 +  is "of_nat :: nat \<Rightarrow> int"
   1.156 +  .
   1.157 +
   1.158 +lemma integer_of_nat_eq_of_nat [code]:
   1.159 +  "integer_of_nat = of_nat"
   1.160 +  by transfer rule
   1.161 +
   1.162 +lemma int_of_integer_integer_of_nat [simp]:
   1.163 +  "int_of_integer (integer_of_nat n) = of_nat n"
   1.164 +  by transfer rule
   1.165 +
   1.166 +lift_definition nat_of_integer :: "integer \<Rightarrow> nat"
   1.167 +  is Int.nat
   1.168 +  .
   1.169  
   1.170 -lemma of_nat_inject [simp]:
   1.171 -  "of_nat n = of_nat m \<longleftrightarrow> n = m"
   1.172 -  by (rule of_nat_inject) (rule UNIV_I)+
   1.173 +lemma nat_of_integer_of_nat [simp]:
   1.174 +  "nat_of_integer (of_nat n) = n"
   1.175 +  by transfer simp
   1.176 +
   1.177 +lemma int_of_integer_of_int [simp]:
   1.178 +  "int_of_integer (of_int k) = k"
   1.179 +  by transfer simp
   1.180 +
   1.181 +lemma nat_of_integer_integer_of_nat [simp]:
   1.182 +  "nat_of_integer (integer_of_nat n) = n"
   1.183 +  by transfer simp
   1.184 +
   1.185 +lemma integer_of_int_eq_of_int [simp, code_abbrev]:
   1.186 +  "integer_of_int = of_int"
   1.187 +  by transfer (simp add: fun_eq_iff)
   1.188  
   1.189 -instantiation code_numeral :: zero
   1.190 +lemma of_int_integer_of [simp]:
   1.191 +  "of_int (int_of_integer k) = (k :: integer)"
   1.192 +  by transfer rule
   1.193 +
   1.194 +lemma int_of_integer_numeral [simp]:
   1.195 +  "int_of_integer (numeral k) = numeral k"
   1.196 +  by transfer rule
   1.197 +
   1.198 +lemma int_of_integer_neg_numeral [simp]:
   1.199 +  "int_of_integer (neg_numeral k) = neg_numeral k"
   1.200 +  by transfer rule
   1.201 +
   1.202 +lemma int_of_integer_sub [simp]:
   1.203 +  "int_of_integer (Num.sub k l) = Num.sub k l"
   1.204 +  by transfer rule
   1.205 +
   1.206 +instantiation integer :: "{ring_div, equal, linordered_idom}"
   1.207  begin
   1.208  
   1.209 -definition [simp, code del]:
   1.210 -  "0 = of_nat 0"
   1.211 +lift_definition div_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
   1.212 +  is "Divides.div :: int \<Rightarrow> int \<Rightarrow> int"
   1.213 +  .
   1.214 +
   1.215 +declare div_integer.rep_eq [simp]
   1.216 +
   1.217 +lift_definition mod_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
   1.218 +  is "Divides.mod :: int \<Rightarrow> int \<Rightarrow> int"
   1.219 +  .
   1.220 +
   1.221 +declare mod_integer.rep_eq [simp]
   1.222 +
   1.223 +lift_definition abs_integer :: "integer \<Rightarrow> integer"
   1.224 +  is "abs :: int \<Rightarrow> int"
   1.225 +  .
   1.226 +
   1.227 +declare abs_integer.rep_eq [simp]
   1.228  
   1.229 -instance ..
   1.230 +lift_definition sgn_integer :: "integer \<Rightarrow> integer"
   1.231 +  is "sgn :: int \<Rightarrow> int"
   1.232 +  .
   1.233 +
   1.234 +declare sgn_integer.rep_eq [simp]
   1.235 +
   1.236 +lift_definition less_eq_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
   1.237 +  is "less_eq :: int \<Rightarrow> int \<Rightarrow> bool"
   1.238 +  .
   1.239 +
   1.240 +lift_definition less_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
   1.241 +  is "less :: int \<Rightarrow> int \<Rightarrow> bool"
   1.242 +  .
   1.243 +
   1.244 +lift_definition equal_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
   1.245 +  is "HOL.equal :: int \<Rightarrow> int \<Rightarrow> bool"
   1.246 +  .
   1.247 +
   1.248 +instance proof
   1.249 +qed (transfer, simp add: algebra_simps equal less_le_not_le [symmetric] mult_strict_right_mono linear)+
   1.250  
   1.251  end
   1.252  
   1.253 -definition Suc where [simp]:
   1.254 -  "Suc k = of_nat (Nat.Suc (nat_of k))"
   1.255 +lemma [transfer_rule]:
   1.256 +  "fun_rel cr_integer (fun_rel cr_integer cr_integer) (min :: _ \<Rightarrow> _ \<Rightarrow> int) (min :: _ \<Rightarrow> _ \<Rightarrow> integer)"
   1.257 +  by (unfold min_def [abs_def]) transfer_prover
   1.258 +
   1.259 +lemma [transfer_rule]:
   1.260 +  "fun_rel cr_integer (fun_rel cr_integer cr_integer) (max :: _ \<Rightarrow> _ \<Rightarrow> int) (max :: _ \<Rightarrow> _ \<Rightarrow> integer)"
   1.261 +  by (unfold max_def [abs_def]) transfer_prover
   1.262 +
   1.263 +lemma int_of_integer_min [simp]:
   1.264 +  "int_of_integer (min k l) = min (int_of_integer k) (int_of_integer l)"
   1.265 +  by transfer rule
   1.266 +
   1.267 +lemma int_of_integer_max [simp]:
   1.268 +  "int_of_integer (max k l) = max (int_of_integer k) (int_of_integer l)"
   1.269 +  by transfer rule
   1.270  
   1.271 -rep_datatype "0 \<Colon> code_numeral" Suc
   1.272 -proof -
   1.273 -  fix P :: "code_numeral \<Rightarrow> bool"
   1.274 -  fix k :: code_numeral
   1.275 -  assume "P 0" then have init: "P (of_nat 0)" by simp
   1.276 -  assume "\<And>k. P k \<Longrightarrow> P (Suc k)"
   1.277 -    then have "\<And>n. P (of_nat n) \<Longrightarrow> P (Suc (of_nat n))" .
   1.278 -    then have step: "\<And>n. P (of_nat n) \<Longrightarrow> P (of_nat (Nat.Suc n))" by simp
   1.279 -  from init step have "P (of_nat (nat_of k))"
   1.280 -    by (induct ("nat_of k")) simp_all
   1.281 -  then show "P k" by simp
   1.282 -qed simp_all
   1.283 +lemma nat_of_integer_non_positive [simp]:
   1.284 +  "k \<le> 0 \<Longrightarrow> nat_of_integer k = 0"
   1.285 +  by transfer simp
   1.286 +
   1.287 +lemma of_nat_of_integer [simp]:
   1.288 +  "of_nat (nat_of_integer k) = max 0 k"
   1.289 +  by transfer auto
   1.290 +
   1.291  
   1.292 -declare code_numeral_case [case_names nat, cases type: code_numeral]
   1.293 -declare code_numeral.induct [case_names nat, induct type: code_numeral]
   1.294 +subsection {* Code theorems for target language integers *}
   1.295 +
   1.296 +text {* Constructors *}
   1.297  
   1.298 -lemma code_numeral_decr [termination_simp]:
   1.299 -  "k \<noteq> of_nat 0 \<Longrightarrow> nat_of k - Nat.Suc 0 < nat_of k"
   1.300 -  by (cases k) simp
   1.301 +definition Pos :: "num \<Rightarrow> integer"
   1.302 +where
   1.303 +  [simp, code_abbrev]: "Pos = numeral"
   1.304 +
   1.305 +lemma [transfer_rule]:
   1.306 +  "fun_rel HOL.eq cr_integer numeral Pos"
   1.307 +  by simp transfer_prover
   1.308  
   1.309 -lemma [simp, code]:
   1.310 -  "code_numeral_size = nat_of"
   1.311 -proof (rule ext)
   1.312 -  fix k
   1.313 -  have "code_numeral_size k = nat_size (nat_of k)"
   1.314 -    by (induct k rule: code_numeral.induct) (simp_all del: zero_code_numeral_def Suc_def, simp_all)
   1.315 -  also have "nat_size (nat_of k) = nat_of k" by (induct ("nat_of k")) simp_all
   1.316 -  finally show "code_numeral_size k = nat_of k" .
   1.317 -qed
   1.318 +definition Neg :: "num \<Rightarrow> integer"
   1.319 +where
   1.320 +  [simp, code_abbrev]: "Neg = neg_numeral"
   1.321 +
   1.322 +lemma [transfer_rule]:
   1.323 +  "fun_rel HOL.eq cr_integer neg_numeral Neg"
   1.324 +  by simp transfer_prover
   1.325 +
   1.326 +code_datatype "0::integer" Pos Neg
   1.327 +
   1.328 +
   1.329 +text {* Auxiliary operations *}
   1.330 +
   1.331 +lift_definition dup :: "integer \<Rightarrow> integer"
   1.332 +  is "\<lambda>k::int. k + k"
   1.333 +  .
   1.334  
   1.335 -lemma [simp, code]:
   1.336 -  "size = nat_of"
   1.337 -proof (rule ext)
   1.338 -  fix k
   1.339 -  show "size k = nat_of k"
   1.340 -  by (induct k) (simp_all del: zero_code_numeral_def Suc_def, simp_all)
   1.341 -qed
   1.342 +lemma dup_code [code]:
   1.343 +  "dup 0 = 0"
   1.344 +  "dup (Pos n) = Pos (Num.Bit0 n)"
   1.345 +  "dup (Neg n) = Neg (Num.Bit0 n)"
   1.346 +  by (transfer, simp only: neg_numeral_def numeral_Bit0 minus_add_distrib)+
   1.347 +
   1.348 +lift_definition sub :: "num \<Rightarrow> num \<Rightarrow> integer"
   1.349 +  is "\<lambda>m n. numeral m - numeral n :: int"
   1.350 +  .
   1.351  
   1.352 -lemmas [code del] = code_numeral.recs code_numeral.cases
   1.353 -
   1.354 -lemma [code]:
   1.355 -  "HOL.equal k l \<longleftrightarrow> HOL.equal (nat_of k) (nat_of l)"
   1.356 -  by (cases k, cases l) (simp add: equal)
   1.357 -
   1.358 -lemma [code nbe]:
   1.359 -  "HOL.equal (k::code_numeral) k \<longleftrightarrow> True"
   1.360 -  by (rule equal_refl)
   1.361 +lemma sub_code [code]:
   1.362 +  "sub Num.One Num.One = 0"
   1.363 +  "sub (Num.Bit0 m) Num.One = Pos (Num.BitM m)"
   1.364 +  "sub (Num.Bit1 m) Num.One = Pos (Num.Bit0 m)"
   1.365 +  "sub Num.One (Num.Bit0 n) = Neg (Num.BitM n)"
   1.366 +  "sub Num.One (Num.Bit1 n) = Neg (Num.Bit0 n)"
   1.367 +  "sub (Num.Bit0 m) (Num.Bit0 n) = dup (sub m n)"
   1.368 +  "sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)"
   1.369 +  "sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1"
   1.370 +  "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1"
   1.371 +  by (transfer, simp add: dbl_def dbl_inc_def dbl_dec_def)+
   1.372  
   1.373  
   1.374 -subsection {* Basic arithmetic *}
   1.375 +text {* Implementations *}
   1.376  
   1.377 -instantiation code_numeral :: "{minus, linordered_semidom, semiring_div, linorder}"
   1.378 -begin
   1.379 -
   1.380 -definition [simp, code del]:
   1.381 -  "(1\<Colon>code_numeral) = of_nat 1"
   1.382 +lemma one_integer_code [code, code_unfold]:
   1.383 +  "1 = Pos Num.One"
   1.384 +  by simp
   1.385  
   1.386 -definition [simp, code del]:
   1.387 -  "n + m = of_nat (nat_of n + nat_of m)"
   1.388 -
   1.389 -definition [simp, code del]:
   1.390 -  "n - m = of_nat (nat_of n - nat_of m)"
   1.391 -
   1.392 -definition [simp, code del]:
   1.393 -  "n * m = of_nat (nat_of n * nat_of m)"
   1.394 -
   1.395 -definition [simp, code del]:
   1.396 -  "n div m = of_nat (nat_of n div nat_of m)"
   1.397 +lemma plus_integer_code [code]:
   1.398 +  "k + 0 = (k::integer)"
   1.399 +  "0 + l = (l::integer)"
   1.400 +  "Pos m + Pos n = Pos (m + n)"
   1.401 +  "Pos m + Neg n = sub m n"
   1.402 +  "Neg m + Pos n = sub n m"
   1.403 +  "Neg m + Neg n = Neg (m + n)"
   1.404 +  by (transfer, simp)+
   1.405  
   1.406 -definition [simp, code del]:
   1.407 -  "n mod m = of_nat (nat_of n mod nat_of m)"
   1.408 -
   1.409 -definition [simp, code del]:
   1.410 -  "n \<le> m \<longleftrightarrow> nat_of n \<le> nat_of m"
   1.411 -
   1.412 -definition [simp, code del]:
   1.413 -  "n < m \<longleftrightarrow> nat_of n < nat_of m"
   1.414 -
   1.415 -instance proof
   1.416 -qed (auto simp add: code_numeral distrib_right intro: mult_commute)
   1.417 +lemma uminus_integer_code [code]:
   1.418 +  "uminus 0 = (0::integer)"
   1.419 +  "uminus (Pos m) = Neg m"
   1.420 +  "uminus (Neg m) = Pos m"
   1.421 +  by simp_all
   1.422  
   1.423 -end
   1.424 -
   1.425 -lemma nat_of_numeral [simp]: "nat_of (numeral k) = numeral k"
   1.426 -  by (induct k rule: num_induct) (simp_all add: numeral_inc)
   1.427 +lemma minus_integer_code [code]:
   1.428 +  "k - 0 = (k::integer)"
   1.429 +  "0 - l = uminus (l::integer)"
   1.430 +  "Pos m - Pos n = sub m n"
   1.431 +  "Pos m - Neg n = Pos (m + n)"
   1.432 +  "Neg m - Pos n = Neg (m + n)"
   1.433 +  "Neg m - Neg n = sub n m"
   1.434 +  by (transfer, simp)+
   1.435  
   1.436 -definition Num :: "num \<Rightarrow> code_numeral"
   1.437 -  where [simp, code_abbrev]: "Num = numeral"
   1.438 +lemma abs_integer_code [code]:
   1.439 +  "\<bar>k\<bar> = (if (k::integer) < 0 then - k else k)"
   1.440 +  by simp
   1.441  
   1.442 -code_datatype "0::code_numeral" Num
   1.443 -
   1.444 -lemma one_code_numeral_code [code]:
   1.445 -  "(1\<Colon>code_numeral) = Numeral1"
   1.446 +lemma sgn_integer_code [code]:
   1.447 +  "sgn k = (if k = 0 then 0 else if (k::integer) < 0 then - 1 else 1)"
   1.448    by simp
   1.449  
   1.450 -lemma [code_abbrev]: "Numeral1 = (1\<Colon>code_numeral)"
   1.451 -  using one_code_numeral_code ..
   1.452 +lemma times_integer_code [code]:
   1.453 +  "k * 0 = (0::integer)"
   1.454 +  "0 * l = (0::integer)"
   1.455 +  "Pos m * Pos n = Pos (m * n)"
   1.456 +  "Pos m * Neg n = Neg (m * n)"
   1.457 +  "Neg m * Pos n = Neg (m * n)"
   1.458 +  "Neg m * Neg n = Pos (m * n)"
   1.459 +  by simp_all
   1.460 +
   1.461 +definition divmod_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer \<times> integer"
   1.462 +where
   1.463 +  "divmod_integer k l = (k div l, k mod l)"
   1.464 +
   1.465 +lemma fst_divmod [simp]:
   1.466 +  "fst (divmod_integer k l) = k div l"
   1.467 +  by (simp add: divmod_integer_def)
   1.468 +
   1.469 +lemma snd_divmod [simp]:
   1.470 +  "snd (divmod_integer k l) = k mod l"
   1.471 +  by (simp add: divmod_integer_def)
   1.472 +
   1.473 +definition divmod_abs :: "integer \<Rightarrow> integer \<Rightarrow> integer \<times> integer"
   1.474 +where
   1.475 +  "divmod_abs k l = (\<bar>k\<bar> div \<bar>l\<bar>, \<bar>k\<bar> mod \<bar>l\<bar>)"
   1.476 +
   1.477 +lemma fst_divmod_abs [simp]:
   1.478 +  "fst (divmod_abs k l) = \<bar>k\<bar> div \<bar>l\<bar>"
   1.479 +  by (simp add: divmod_abs_def)
   1.480 +
   1.481 +lemma snd_divmod_abs [simp]:
   1.482 +  "snd (divmod_abs k l) = \<bar>k\<bar> mod \<bar>l\<bar>"
   1.483 +  by (simp add: divmod_abs_def)
   1.484  
   1.485 -lemma plus_code_numeral_code [code nbe]:
   1.486 -  "of_nat n + of_nat m = of_nat (n + m)"
   1.487 -  by simp
   1.488 +lemma divmod_abs_terminate_code [code]:
   1.489 +  "divmod_abs (Neg k) (Neg l) = divmod_abs (Pos k) (Pos l)"
   1.490 +  "divmod_abs (Neg k) (Pos l) = divmod_abs (Pos k) (Pos l)"
   1.491 +  "divmod_abs (Pos k) (Neg l) = divmod_abs (Pos k) (Pos l)"
   1.492 +  "divmod_abs j 0 = (0, \<bar>j\<bar>)"
   1.493 +  "divmod_abs 0 j = (0, 0)"
   1.494 +  by (simp_all add: prod_eq_iff)
   1.495 +
   1.496 +lemma divmod_abs_rec_code [code]:
   1.497 +  "divmod_abs (Pos k) (Pos l) =
   1.498 +    (let j = sub k l in
   1.499 +       if j < 0 then (0, Pos k)
   1.500 +       else let (q, r) = divmod_abs j (Pos l) in (q + 1, r))"
   1.501 +  apply (simp add: prod_eq_iff Let_def prod_case_beta)
   1.502 +  apply transfer
   1.503 +  apply (simp add: sub_non_negative sub_negative div_pos_pos_trivial mod_pos_pos_trivial div_pos_geq mod_pos_geq)
   1.504 +  done
   1.505  
   1.506 -lemma minus_code_numeral_code [code nbe]:
   1.507 -  "of_nat n - of_nat m = of_nat (n - m)"
   1.508 +lemma divmod_integer_code [code]:
   1.509 +  "divmod_integer k l =
   1.510 +    (if k = 0 then (0, 0) else if l = 0 then (0, k) else
   1.511 +    (apsnd \<circ> times \<circ> sgn) l (if sgn k = sgn l
   1.512 +      then divmod_abs k l
   1.513 +      else (let (r, s) = divmod_abs k l in
   1.514 +        if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"
   1.515 +proof -
   1.516 +  have aux1: "\<And>k l::int. sgn k = sgn l \<longleftrightarrow> k = 0 \<and> l = 0 \<or> 0 < l \<and> 0 < k \<or> l < 0 \<and> k < 0"
   1.517 +    by (auto simp add: sgn_if)
   1.518 +  have aux2: "\<And>q::int. - int_of_integer k = int_of_integer l * q \<longleftrightarrow> int_of_integer k = int_of_integer l * - q" by auto
   1.519 +  show ?thesis
   1.520 +    by (simp add: prod_eq_iff integer_eq_iff prod_case_beta aux1)
   1.521 +      (auto simp add: zdiv_zminus1_eq_if zmod_zminus1_eq_if div_minus_right mod_minus_right aux2)
   1.522 +qed
   1.523 +
   1.524 +lemma div_integer_code [code]:
   1.525 +  "k div l = fst (divmod_integer k l)"
   1.526    by simp
   1.527  
   1.528 -lemma times_code_numeral_code [code nbe]:
   1.529 -  "of_nat n * of_nat m = of_nat (n * m)"
   1.530 -  by simp
   1.531 -
   1.532 -lemma less_eq_code_numeral_code [code nbe]:
   1.533 -  "of_nat n \<le> of_nat m \<longleftrightarrow> n \<le> m"
   1.534 -  by simp
   1.535 -
   1.536 -lemma less_code_numeral_code [code nbe]:
   1.537 -  "of_nat n < of_nat m \<longleftrightarrow> n < m"
   1.538 +lemma mod_integer_code [code]:
   1.539 +  "k mod l = snd (divmod_integer k l)"
   1.540    by simp
   1.541  
   1.542 -lemma code_numeral_zero_minus_one:
   1.543 -  "(0::code_numeral) - 1 = 0"
   1.544 -  by simp
   1.545 +lemma equal_integer_code [code]:
   1.546 +  "HOL.equal 0 (0::integer) \<longleftrightarrow> True"
   1.547 +  "HOL.equal 0 (Pos l) \<longleftrightarrow> False"
   1.548 +  "HOL.equal 0 (Neg l) \<longleftrightarrow> False"
   1.549 +  "HOL.equal (Pos k) 0 \<longleftrightarrow> False"
   1.550 +  "HOL.equal (Pos k) (Pos l) \<longleftrightarrow> HOL.equal k l"
   1.551 +  "HOL.equal (Pos k) (Neg l) \<longleftrightarrow> False"
   1.552 +  "HOL.equal (Neg k) 0 \<longleftrightarrow> False"
   1.553 +  "HOL.equal (Neg k) (Pos l) \<longleftrightarrow> False"
   1.554 +  "HOL.equal (Neg k) (Neg l) \<longleftrightarrow> HOL.equal k l"
   1.555 +  by (simp_all add: equal)
   1.556 +
   1.557 +lemma equal_integer_refl [code nbe]:
   1.558 +  "HOL.equal (k::integer) k \<longleftrightarrow> True"
   1.559 +  by (fact equal_refl)
   1.560  
   1.561 -lemma Suc_code_numeral_minus_one:
   1.562 -  "Suc n - 1 = n"
   1.563 -  by simp
   1.564 +lemma less_eq_integer_code [code]:
   1.565 +  "0 \<le> (0::integer) \<longleftrightarrow> True"
   1.566 +  "0 \<le> Pos l \<longleftrightarrow> True"
   1.567 +  "0 \<le> Neg l \<longleftrightarrow> False"
   1.568 +  "Pos k \<le> 0 \<longleftrightarrow> False"
   1.569 +  "Pos k \<le> Pos l \<longleftrightarrow> k \<le> l"
   1.570 +  "Pos k \<le> Neg l \<longleftrightarrow> False"
   1.571 +  "Neg k \<le> 0 \<longleftrightarrow> True"
   1.572 +  "Neg k \<le> Pos l \<longleftrightarrow> True"
   1.573 +  "Neg k \<le> Neg l \<longleftrightarrow> l \<le> k"
   1.574 +  by simp_all
   1.575 +
   1.576 +lemma less_integer_code [code]:
   1.577 +  "0 < (0::integer) \<longleftrightarrow> False"
   1.578 +  "0 < Pos l \<longleftrightarrow> True"
   1.579 +  "0 < Neg l \<longleftrightarrow> False"
   1.580 +  "Pos k < 0 \<longleftrightarrow> False"
   1.581 +  "Pos k < Pos l \<longleftrightarrow> k < l"
   1.582 +  "Pos k < Neg l \<longleftrightarrow> False"
   1.583 +  "Neg k < 0 \<longleftrightarrow> True"
   1.584 +  "Neg k < Pos l \<longleftrightarrow> True"
   1.585 +  "Neg k < Neg l \<longleftrightarrow> l < k"
   1.586 +  by simp_all
   1.587  
   1.588 -lemma of_nat_code [code]:
   1.589 -  "of_nat = Nat.of_nat"
   1.590 -proof
   1.591 -  fix n :: nat
   1.592 -  have "Nat.of_nat n = of_nat n"
   1.593 -    by (induct n) simp_all
   1.594 -  then show "of_nat n = Nat.of_nat n"
   1.595 -    by (rule sym)
   1.596 +lift_definition integer_of_num :: "num \<Rightarrow> integer"
   1.597 +  is "numeral :: num \<Rightarrow> int"
   1.598 +  .
   1.599 +
   1.600 +lemma integer_of_num [code]:
   1.601 +  "integer_of_num num.One = 1"
   1.602 +  "integer_of_num (num.Bit0 n) = (let k = integer_of_num n in k + k)"
   1.603 +  "integer_of_num (num.Bit1 n) = (let k = integer_of_num n in k + k + 1)"
   1.604 +  by (transfer, simp only: numeral.simps Let_def)+
   1.605 +
   1.606 +lift_definition num_of_integer :: "integer \<Rightarrow> num"
   1.607 +  is "num_of_nat \<circ> nat"
   1.608 +  .
   1.609 +
   1.610 +lemma num_of_integer_code [code]:
   1.611 +  "num_of_integer k = (if k \<le> 1 then Num.One
   1.612 +     else let
   1.613 +       (l, j) = divmod_integer k 2;
   1.614 +       l' = num_of_integer l;
   1.615 +       l'' = l' + l'
   1.616 +     in if j = 0 then l'' else l'' + Num.One)"
   1.617 +proof -
   1.618 +  {
   1.619 +    assume "int_of_integer k mod 2 = 1"
   1.620 +    then have "nat (int_of_integer k mod 2) = nat 1" by simp
   1.621 +    moreover assume *: "1 < int_of_integer k"
   1.622 +    ultimately have **: "nat (int_of_integer k) mod 2 = 1" by (simp add: nat_mod_distrib)
   1.623 +    have "num_of_nat (nat (int_of_integer k)) =
   1.624 +      num_of_nat (2 * (nat (int_of_integer k) div 2) + nat (int_of_integer k) mod 2)"
   1.625 +      by simp
   1.626 +    then have "num_of_nat (nat (int_of_integer k)) =
   1.627 +      num_of_nat (nat (int_of_integer k) div 2 + nat (int_of_integer k) div 2 + nat (int_of_integer k) mod 2)"
   1.628 +      by (simp add: mult_2)
   1.629 +    with ** have "num_of_nat (nat (int_of_integer k)) =
   1.630 +      num_of_nat (nat (int_of_integer k) div 2 + nat (int_of_integer k) div 2 + 1)"
   1.631 +      by simp
   1.632 +  }
   1.633 +  note aux = this
   1.634 +  show ?thesis
   1.635 +    by (auto simp add: num_of_integer_def nat_of_integer_def Let_def prod_case_beta
   1.636 +      not_le integer_eq_iff less_eq_integer_def
   1.637 +      nat_mult_distrib nat_div_distrib num_of_nat_One num_of_nat_plus_distrib
   1.638 +       mult_2 [where 'a=nat] aux add_One)
   1.639  qed
   1.640  
   1.641 -lemma code_numeral_not_eq_zero: "i \<noteq> of_nat 0 \<longleftrightarrow> i \<ge> 1"
   1.642 -  by (cases i) auto
   1.643 -
   1.644 -definition nat_of_aux :: "code_numeral \<Rightarrow> nat \<Rightarrow> nat" where
   1.645 -  "nat_of_aux i n = nat_of i + n"
   1.646 -
   1.647 -lemma nat_of_aux_code [code]:
   1.648 -  "nat_of_aux i n = (if i = 0 then n else nat_of_aux (i - 1) (Nat.Suc n))"
   1.649 -  by (auto simp add: nat_of_aux_def code_numeral_not_eq_zero)
   1.650 -
   1.651 -lemma nat_of_code [code]:
   1.652 -  "nat_of i = nat_of_aux i 0"
   1.653 -  by (simp add: nat_of_aux_def)
   1.654 -
   1.655 -definition div_mod :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<times> code_numeral" where
   1.656 -  [code del]: "div_mod n m = (n div m, n mod m)"
   1.657 -
   1.658 -lemma [code]:
   1.659 -  "div_mod n m = (if m = 0 then (0, n) else (n div m, n mod m))"
   1.660 -  unfolding div_mod_def by auto
   1.661 -
   1.662 -lemma [code]:
   1.663 -  "n div m = fst (div_mod n m)"
   1.664 -  unfolding div_mod_def by simp
   1.665 -
   1.666 -lemma [code]:
   1.667 -  "n mod m = snd (div_mod n m)"
   1.668 -  unfolding div_mod_def by simp
   1.669 -
   1.670 -definition int_of :: "code_numeral \<Rightarrow> int" where
   1.671 -  "int_of = Nat.of_nat o nat_of"
   1.672 -
   1.673 -lemma int_of_code [code]:
   1.674 -  "int_of k = (if k = 0 then 0
   1.675 -    else (if k mod 2 = 0 then 2 * int_of (k div 2) else 2 * int_of (k div 2) + 1))"
   1.676 +lemma nat_of_integer_code [code]:
   1.677 +  "nat_of_integer k = (if k \<le> 0 then 0
   1.678 +     else let
   1.679 +       (l, j) = divmod_integer k 2;
   1.680 +       l' = nat_of_integer l;
   1.681 +       l'' = l' + l'
   1.682 +     in if j = 0 then l'' else l'' + 1)"
   1.683  proof -
   1.684 -  have "(nat_of k div 2) * 2 + nat_of k mod 2 = nat_of k" 
   1.685 -    by (rule mod_div_equality)
   1.686 -  then have "int ((nat_of k div 2) * 2 + nat_of k mod 2) = int (nat_of k)" 
   1.687 -    by simp
   1.688 -  then have "int (nat_of k) = int (nat_of k div 2) * 2 + int (nat_of k mod 2)" 
   1.689 -    unfolding of_nat_mult of_nat_add by simp
   1.690 -  then show ?thesis by (auto simp add: int_of_def mult_ac)
   1.691 +  obtain j where "k = integer_of_int j"
   1.692 +  proof
   1.693 +    show "k = integer_of_int (int_of_integer k)" by simp
   1.694 +  qed
   1.695 +  moreover have "2 * (j div 2) = j - j mod 2"
   1.696 +    by (simp add: zmult_div_cancel mult_commute)
   1.697 +  ultimately show ?thesis
   1.698 +    by (auto simp add: split_def Let_def mod_integer_def nat_of_integer_def not_le
   1.699 +      nat_add_distrib [symmetric] Suc_nat_eq_nat_zadd1)
   1.700 +      (auto simp add: mult_2 [symmetric])
   1.701  qed
   1.702  
   1.703 +lemma int_of_integer_code [code]:
   1.704 +  "int_of_integer k = (if k < 0 then - (int_of_integer (- k))
   1.705 +     else if k = 0 then 0
   1.706 +     else let
   1.707 +       (l, j) = divmod_integer k 2;
   1.708 +       l' = 2 * int_of_integer l
   1.709 +     in if j = 0 then l' else l' + 1)"
   1.710 +  by (auto simp add: split_def Let_def integer_eq_iff zmult_div_cancel)
   1.711  
   1.712 -hide_const (open) of_nat nat_of Suc int_of
   1.713 +lemma integer_of_int_code [code]:
   1.714 +  "integer_of_int k = (if k < 0 then - (integer_of_int (- k))
   1.715 +     else if k = 0 then 0
   1.716 +     else let
   1.717 +       (l, j) = divmod_int k 2;
   1.718 +       l' = 2 * integer_of_int l
   1.719 +     in if j = 0 then l' else l' + 1)"
   1.720 +  by (auto simp add: split_def Let_def integer_eq_iff zmult_div_cancel)
   1.721 +
   1.722 +hide_const (open) Pos Neg sub dup divmod_abs
   1.723  
   1.724  
   1.725 -subsection {* Code generator setup *}
   1.726 +subsection {* Serializer setup for target language integers *}
   1.727  
   1.728 -text {* Implementation of code numerals by bounded integers *}
   1.729 +code_reserved Eval int Integer abs
   1.730  
   1.731 -code_type code_numeral
   1.732 -  (SML "int")
   1.733 +code_type integer
   1.734 +  (SML "IntInf.int")
   1.735    (OCaml "Big'_int.big'_int")
   1.736    (Haskell "Integer")
   1.737    (Scala "BigInt")
   1.738 +  (Eval "int")
   1.739  
   1.740 -code_instance code_numeral :: equal
   1.741 +code_instance integer :: equal
   1.742    (Haskell -)
   1.743  
   1.744 -setup {*
   1.745 -  Numeral.add_code @{const_name Num}
   1.746 -    false Code_Printer.literal_naive_numeral "SML"
   1.747 -  #> fold (Numeral.add_code @{const_name Num}
   1.748 -    false Code_Printer.literal_numeral) ["OCaml", "Haskell", "Scala"]
   1.749 -*}
   1.750 -
   1.751 -code_reserved SML Int int
   1.752 -code_reserved Eval Integer
   1.753 -
   1.754 -code_const "0::code_numeral"
   1.755 +code_const "0::integer"
   1.756    (SML "0")
   1.757    (OCaml "Big'_int.zero'_big'_int")
   1.758    (Haskell "0")
   1.759    (Scala "BigInt(0)")
   1.760  
   1.761 -code_const "plus \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   1.762 -  (SML "Int.+/ ((_),/ (_))")
   1.763 +setup {*
   1.764 +  fold (Numeral.add_code @{const_name Code_Numeral.Pos}
   1.765 +    false Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"]
   1.766 +*}
   1.767 +
   1.768 +setup {*
   1.769 +  fold (Numeral.add_code @{const_name Code_Numeral.Neg}
   1.770 +    true Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"]
   1.771 +*}
   1.772 +
   1.773 +code_const "plus :: integer \<Rightarrow> _ \<Rightarrow> _"
   1.774 +  (SML "IntInf.+ ((_), (_))")
   1.775    (OCaml "Big'_int.add'_big'_int")
   1.776    (Haskell infixl 6 "+")
   1.777    (Scala infixl 7 "+")
   1.778    (Eval infixl 8 "+")
   1.779  
   1.780 -code_const "minus \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   1.781 -  (SML "Int.max/ (0 : int,/ Int.-/ ((_),/ (_)))")
   1.782 -  (OCaml "Big'_int.max'_big'_int/ Big'_int.zero'_big'_int/ (Big'_int.sub'_big'_int/ _/ _)")
   1.783 -  (Haskell "Prelude.max/ (0 :: Integer)/ (_/ -/ _)")
   1.784 -  (Scala "!(_/ -/ _).max(0)")
   1.785 -  (Eval "Integer.max/ 0/ (_/ -/ _)")
   1.786 +code_const "uminus :: integer \<Rightarrow> _"
   1.787 +  (SML "IntInf.~")
   1.788 +  (OCaml "Big'_int.minus'_big'_int")
   1.789 +  (Haskell "negate")
   1.790 +  (Scala "!(- _)")
   1.791 +  (Eval "~/ _")
   1.792 +
   1.793 +code_const "minus :: integer \<Rightarrow> _"
   1.794 +  (SML "IntInf.- ((_), (_))")
   1.795 +  (OCaml "Big'_int.sub'_big'_int")
   1.796 +  (Haskell infixl 6 "-")
   1.797 +  (Scala infixl 7 "-")
   1.798 +  (Eval infixl 8 "-")
   1.799  
   1.800 -code_const "times \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   1.801 -  (SML "Int.*/ ((_),/ (_))")
   1.802 +code_const Code_Numeral.dup
   1.803 +  (SML "IntInf.*/ (2,/ (_))")
   1.804 +  (OCaml "Big'_int.mult'_big'_int/ (Big'_int.big'_int'_of'_int/ 2)")
   1.805 +  (Haskell "!(2 * _)")
   1.806 +  (Scala "!(2 * _)")
   1.807 +  (Eval "!(2 * _)")
   1.808 +
   1.809 +code_const Code_Numeral.sub
   1.810 +  (SML "!(raise/ Fail/ \"sub\")")
   1.811 +  (OCaml "failwith/ \"sub\"")
   1.812 +  (Haskell "error/ \"sub\"")
   1.813 +  (Scala "!sys.error(\"sub\")")
   1.814 +
   1.815 +code_const "times :: integer \<Rightarrow> _ \<Rightarrow> _"
   1.816 +  (SML "IntInf.* ((_), (_))")
   1.817    (OCaml "Big'_int.mult'_big'_int")
   1.818    (Haskell infixl 7 "*")
   1.819    (Scala infixl 8 "*")
   1.820 -  (Eval infixl 8 "*")
   1.821 +  (Eval infixl 9 "*")
   1.822  
   1.823 -code_const Code_Numeral.div_mod
   1.824 -  (SML "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (Int.div (n, m), Int.mod (n, m)))")
   1.825 +code_const Code_Numeral.divmod_abs
   1.826 +  (SML "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)")
   1.827    (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)")
   1.828 -  (Haskell "divMod")
   1.829 +  (Haskell "divMod/ (abs _)/ (abs _)")
   1.830    (Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
   1.831 -  (Eval "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (Integer.div'_mod n m))")
   1.832 +  (Eval "Integer.div'_mod/ (abs _)/ (abs _)")
   1.833  
   1.834 -code_const "HOL.equal \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   1.835 -  (SML "!((_ : Int.int) = _)")
   1.836 +code_const "HOL.equal :: integer \<Rightarrow> _ \<Rightarrow> bool"
   1.837 +  (SML "!((_ : IntInf.int) = _)")
   1.838    (OCaml "Big'_int.eq'_big'_int")
   1.839    (Haskell infix 4 "==")
   1.840    (Scala infixl 5 "==")
   1.841 -  (Eval "!((_ : int) = _)")
   1.842 +  (Eval infixl 6 "=")
   1.843  
   1.844 -code_const "less_eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   1.845 -  (SML "Int.<=/ ((_),/ (_))")
   1.846 +code_const "less_eq :: integer \<Rightarrow> _ \<Rightarrow> bool"
   1.847 +  (SML "IntInf.<= ((_), (_))")
   1.848    (OCaml "Big'_int.le'_big'_int")
   1.849    (Haskell infix 4 "<=")
   1.850    (Scala infixl 4 "<=")
   1.851    (Eval infixl 6 "<=")
   1.852  
   1.853 -code_const "less \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   1.854 -  (SML "Int.</ ((_),/ (_))")
   1.855 +code_const "less :: integer \<Rightarrow> _ \<Rightarrow> bool"
   1.856 +  (SML "IntInf.< ((_), (_))")
   1.857    (OCaml "Big'_int.lt'_big'_int")
   1.858    (Haskell infix 4 "<")
   1.859    (Scala infixl 4 "<")
   1.860 @@ -346,5 +623,321 @@
   1.861  code_modulename Haskell
   1.862    Code_Numeral Arith
   1.863  
   1.864 +
   1.865 +subsection {* Type of target language naturals *}
   1.866 +
   1.867 +typedef natural = "UNIV \<Colon> nat set"
   1.868 +  morphisms nat_of_natural natural_of_nat ..
   1.869 +
   1.870 +setup_lifting (no_code) type_definition_natural
   1.871 +
   1.872 +lemma natural_eq_iff [termination_simp]:
   1.873 +  "m = n \<longleftrightarrow> nat_of_natural m = nat_of_natural n"
   1.874 +  by transfer rule
   1.875 +
   1.876 +lemma natural_eqI:
   1.877 +  "nat_of_natural m = nat_of_natural n \<Longrightarrow> m = n"
   1.878 +  using natural_eq_iff [of m n] by simp
   1.879 +
   1.880 +lemma nat_of_natural_of_nat_inverse [simp]:
   1.881 +  "nat_of_natural (natural_of_nat n) = n"
   1.882 +  by transfer rule
   1.883 +
   1.884 +lemma natural_of_nat_of_natural_inverse [simp]:
   1.885 +  "natural_of_nat (nat_of_natural n) = n"
   1.886 +  by transfer rule
   1.887 +
   1.888 +instantiation natural :: "{comm_monoid_diff, semiring_1}"
   1.889 +begin
   1.890 +
   1.891 +lift_definition zero_natural :: natural
   1.892 +  is "0 :: nat"
   1.893 +  .
   1.894 +
   1.895 +declare zero_natural.rep_eq [simp]
   1.896 +
   1.897 +lift_definition one_natural :: natural
   1.898 +  is "1 :: nat"
   1.899 +  .
   1.900 +
   1.901 +declare one_natural.rep_eq [simp]
   1.902 +
   1.903 +lift_definition plus_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
   1.904 +  is "plus :: nat \<Rightarrow> nat \<Rightarrow> nat"
   1.905 +  .
   1.906 +
   1.907 +declare plus_natural.rep_eq [simp]
   1.908 +
   1.909 +lift_definition minus_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
   1.910 +  is "minus :: nat \<Rightarrow> nat \<Rightarrow> nat"
   1.911 +  .
   1.912 +
   1.913 +declare minus_natural.rep_eq [simp]
   1.914 +
   1.915 +lift_definition times_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
   1.916 +  is "times :: nat \<Rightarrow> nat \<Rightarrow> nat"
   1.917 +  .
   1.918 +
   1.919 +declare times_natural.rep_eq [simp]
   1.920 +
   1.921 +instance proof
   1.922 +qed (transfer, simp add: algebra_simps)+
   1.923 +
   1.924 +end
   1.925 +
   1.926 +lemma [transfer_rule]:
   1.927 +  "fun_rel HOL.eq cr_natural (\<lambda>n::nat. n) (of_nat :: nat \<Rightarrow> natural)"
   1.928 +proof -
   1.929 +  have "fun_rel HOL.eq cr_natural (of_nat :: nat \<Rightarrow> nat) (of_nat :: nat \<Rightarrow> natural)"
   1.930 +    by (unfold of_nat_def [abs_def]) transfer_prover
   1.931 +  then show ?thesis by (simp add: id_def)
   1.932 +qed
   1.933 +
   1.934 +lemma [transfer_rule]:
   1.935 +  "fun_rel HOL.eq cr_natural (numeral :: num \<Rightarrow> nat) (numeral :: num \<Rightarrow> natural)"
   1.936 +proof -
   1.937 +  have "fun_rel HOL.eq cr_natural (numeral :: num \<Rightarrow> nat) (\<lambda>n. of_nat (numeral n))"
   1.938 +    by transfer_prover
   1.939 +  then show ?thesis by simp
   1.940 +qed
   1.941 +
   1.942 +lemma nat_of_natural_of_nat [simp]:
   1.943 +  "nat_of_natural (of_nat n) = n"
   1.944 +  by transfer rule
   1.945 +
   1.946 +lemma natural_of_nat_of_nat [simp, code_abbrev]:
   1.947 +  "natural_of_nat = of_nat"
   1.948 +  by transfer rule
   1.949 +
   1.950 +lemma of_nat_of_natural [simp]:
   1.951 +  "of_nat (nat_of_natural n) = n"
   1.952 +  by transfer rule
   1.953 +
   1.954 +lemma nat_of_natural_numeral [simp]:
   1.955 +  "nat_of_natural (numeral k) = numeral k"
   1.956 +  by transfer rule
   1.957 +
   1.958 +instantiation natural :: "{semiring_div, equal, linordered_semiring}"
   1.959 +begin
   1.960 +
   1.961 +lift_definition div_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
   1.962 +  is "Divides.div :: nat \<Rightarrow> nat \<Rightarrow> nat"
   1.963 +  .
   1.964 +
   1.965 +declare div_natural.rep_eq [simp]
   1.966 +
   1.967 +lift_definition mod_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
   1.968 +  is "Divides.mod :: nat \<Rightarrow> nat \<Rightarrow> nat"
   1.969 +  .
   1.970 +
   1.971 +declare mod_natural.rep_eq [simp]
   1.972 +
   1.973 +lift_definition less_eq_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool"
   1.974 +  is "less_eq :: nat \<Rightarrow> nat \<Rightarrow> bool"
   1.975 +  .
   1.976 +
   1.977 +declare less_eq_natural.rep_eq [termination_simp]
   1.978 +
   1.979 +lift_definition less_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool"
   1.980 +  is "less :: nat \<Rightarrow> nat \<Rightarrow> bool"
   1.981 +  .
   1.982 +
   1.983 +declare less_natural.rep_eq [termination_simp]
   1.984 +
   1.985 +lift_definition equal_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool"
   1.986 +  is "HOL.equal :: nat \<Rightarrow> nat \<Rightarrow> bool"
   1.987 +  .
   1.988 +
   1.989 +instance proof
   1.990 +qed (transfer, simp add: algebra_simps equal less_le_not_le [symmetric] linear)+
   1.991 +
   1.992  end
   1.993  
   1.994 +lemma [transfer_rule]:
   1.995 +  "fun_rel cr_natural (fun_rel cr_natural cr_natural) (min :: _ \<Rightarrow> _ \<Rightarrow> nat) (min :: _ \<Rightarrow> _ \<Rightarrow> natural)"
   1.996 +  by (unfold min_def [abs_def]) transfer_prover
   1.997 +
   1.998 +lemma [transfer_rule]:
   1.999 +  "fun_rel cr_natural (fun_rel cr_natural cr_natural) (max :: _ \<Rightarrow> _ \<Rightarrow> nat) (max :: _ \<Rightarrow> _ \<Rightarrow> natural)"
  1.1000 +  by (unfold max_def [abs_def]) transfer_prover
  1.1001 +
  1.1002 +lemma nat_of_natural_min [simp]:
  1.1003 +  "nat_of_natural (min k l) = min (nat_of_natural k) (nat_of_natural l)"
  1.1004 +  by transfer rule
  1.1005 +
  1.1006 +lemma nat_of_natural_max [simp]:
  1.1007 +  "nat_of_natural (max k l) = max (nat_of_natural k) (nat_of_natural l)"
  1.1008 +  by transfer rule
  1.1009 +
  1.1010 +lift_definition natural_of_integer :: "integer \<Rightarrow> natural"
  1.1011 +  is "nat :: int \<Rightarrow> nat"
  1.1012 +  .
  1.1013 +
  1.1014 +lift_definition integer_of_natural :: "natural \<Rightarrow> integer"
  1.1015 +  is "of_nat :: nat \<Rightarrow> int"
  1.1016 +  .
  1.1017 +
  1.1018 +lemma natural_of_integer_of_natural [simp]:
  1.1019 +  "natural_of_integer (integer_of_natural n) = n"
  1.1020 +  by transfer simp
  1.1021 +
  1.1022 +lemma integer_of_natural_of_integer [simp]:
  1.1023 +  "integer_of_natural (natural_of_integer k) = max 0 k"
  1.1024 +  by transfer auto
  1.1025 +
  1.1026 +lemma int_of_integer_of_natural [simp]:
  1.1027 +  "int_of_integer (integer_of_natural n) = of_nat (nat_of_natural n)"
  1.1028 +  by transfer rule
  1.1029 +
  1.1030 +lemma integer_of_natural_of_nat [simp]:
  1.1031 +  "integer_of_natural (of_nat n) = of_nat n"
  1.1032 +  by transfer rule
  1.1033 +
  1.1034 +lemma [measure_function]:
  1.1035 +  "is_measure nat_of_natural"
  1.1036 +  by (rule is_measure_trivial)
  1.1037 +
  1.1038 +
  1.1039 +subsection {* Inductive represenation of target language naturals *}
  1.1040 +
  1.1041 +lift_definition Suc :: "natural \<Rightarrow> natural"
  1.1042 +  is Nat.Suc
  1.1043 +  .
  1.1044 +
  1.1045 +declare Suc.rep_eq [simp]
  1.1046 +
  1.1047 +rep_datatype "0::natural" Suc
  1.1048 +  by (transfer, fact nat.induct nat.inject nat.distinct)+
  1.1049 +
  1.1050 +lemma natural_case [case_names nat, cases type: natural]:
  1.1051 +  fixes m :: natural
  1.1052 +  assumes "\<And>n. m = of_nat n \<Longrightarrow> P"
  1.1053 +  shows P
  1.1054 +  using assms by transfer blast
  1.1055 +
  1.1056 +lemma [simp, code]:
  1.1057 +  "natural_size = nat_of_natural"
  1.1058 +proof (rule ext)
  1.1059 +  fix n
  1.1060 +  show "natural_size n = nat_of_natural n"
  1.1061 +    by (induct n) simp_all
  1.1062 +qed
  1.1063 +
  1.1064 +lemma [simp, code]:
  1.1065 +  "size = nat_of_natural"
  1.1066 +proof (rule ext)
  1.1067 +  fix n
  1.1068 +  show "size n = nat_of_natural n"
  1.1069 +    by (induct n) simp_all
  1.1070 +qed
  1.1071 +
  1.1072 +lemma natural_decr [termination_simp]:
  1.1073 +  "n \<noteq> 0 \<Longrightarrow> nat_of_natural n - Nat.Suc 0 < nat_of_natural n"
  1.1074 +  by transfer simp
  1.1075 +
  1.1076 +lemma natural_zero_minus_one:
  1.1077 +  "(0::natural) - 1 = 0"
  1.1078 +  by simp
  1.1079 +
  1.1080 +lemma Suc_natural_minus_one:
  1.1081 +  "Suc n - 1 = n"
  1.1082 +  by transfer simp
  1.1083 +
  1.1084 +hide_const (open) Suc
  1.1085 +
  1.1086 +
  1.1087 +subsection {* Code refinement for target language naturals *}
  1.1088 +
  1.1089 +lift_definition Nat :: "integer \<Rightarrow> natural"
  1.1090 +  is nat
  1.1091 +  .
  1.1092 +
  1.1093 +lemma [code_post]:
  1.1094 +  "Nat 0 = 0"
  1.1095 +  "Nat 1 = 1"
  1.1096 +  "Nat (numeral k) = numeral k"
  1.1097 +  by (transfer, simp)+
  1.1098 +
  1.1099 +lemma [code abstype]:
  1.1100 +  "Nat (integer_of_natural n) = n"
  1.1101 +  by transfer simp
  1.1102 +
  1.1103 +lemma [code abstract]:
  1.1104 +  "integer_of_natural (natural_of_nat n) = of_nat n"
  1.1105 +  by simp
  1.1106 +
  1.1107 +lemma [code abstract]:
  1.1108 +  "integer_of_natural (natural_of_integer k) = max 0 k"
  1.1109 +  by simp
  1.1110 +
  1.1111 +lemma [code_abbrev]:
  1.1112 +  "natural_of_integer (Code_Numeral.Pos k) = numeral k"
  1.1113 +  by transfer simp
  1.1114 +
  1.1115 +lemma [code abstract]:
  1.1116 +  "integer_of_natural 0 = 0"
  1.1117 +  by transfer simp
  1.1118 +
  1.1119 +lemma [code abstract]:
  1.1120 +  "integer_of_natural 1 = 1"
  1.1121 +  by transfer simp
  1.1122 +
  1.1123 +lemma [code abstract]:
  1.1124 +  "integer_of_natural (Code_Numeral.Suc n) = integer_of_natural n + 1"
  1.1125 +  by transfer simp
  1.1126 +
  1.1127 +lemma [code]:
  1.1128 +  "nat_of_natural = nat_of_integer \<circ> integer_of_natural"
  1.1129 +  by transfer (simp add: fun_eq_iff)
  1.1130 +
  1.1131 +lemma [code, code_unfold]:
  1.1132 +  "natural_case f g n = (if n = 0 then f else g (n - 1))"
  1.1133 +  by (cases n rule: natural.exhaust) (simp_all, simp add: Suc_def)
  1.1134 +
  1.1135 +declare natural.recs [code del]
  1.1136 +
  1.1137 +lemma [code abstract]:
  1.1138 +  "integer_of_natural (m + n) = integer_of_natural m + integer_of_natural n"
  1.1139 +  by transfer simp
  1.1140 +
  1.1141 +lemma [code abstract]:
  1.1142 +  "integer_of_natural (m - n) = max 0 (integer_of_natural m - integer_of_natural n)"
  1.1143 +  by transfer simp
  1.1144 +
  1.1145 +lemma [code abstract]:
  1.1146 +  "integer_of_natural (m * n) = integer_of_natural m * integer_of_natural n"
  1.1147 +  by transfer (simp add: of_nat_mult)
  1.1148 +
  1.1149 +lemma [code abstract]:
  1.1150 +  "integer_of_natural (m div n) = integer_of_natural m div integer_of_natural n"
  1.1151 +  by transfer (simp add: zdiv_int)
  1.1152 +
  1.1153 +lemma [code abstract]:
  1.1154 +  "integer_of_natural (m mod n) = integer_of_natural m mod integer_of_natural n"
  1.1155 +  by transfer (simp add: zmod_int)
  1.1156 +
  1.1157 +lemma [code]:
  1.1158 +  "HOL.equal m n \<longleftrightarrow> HOL.equal (integer_of_natural m) (integer_of_natural n)"
  1.1159 +  by transfer (simp add: equal)
  1.1160 +
  1.1161 +lemma [code nbe]:
  1.1162 +  "HOL.equal n (n::natural) \<longleftrightarrow> True"
  1.1163 +  by (simp add: equal)
  1.1164 +
  1.1165 +lemma [code]:
  1.1166 +  "m \<le> n \<longleftrightarrow> integer_of_natural m \<le> integer_of_natural n"
  1.1167 +  by transfer simp
  1.1168 +
  1.1169 +lemma [code]:
  1.1170 +  "m < n \<longleftrightarrow> integer_of_natural m < integer_of_natural n"
  1.1171 +  by transfer simp
  1.1172 +
  1.1173 +hide_const (open) Nat
  1.1174 +
  1.1175 +
  1.1176 +code_reflect Code_Numeral
  1.1177 +  datatypes natural = _
  1.1178 +  functions integer_of_natural natural_of_integer
  1.1179 +
  1.1180 +end
  1.1181 +