Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Code_Target_Nat.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Library/Code_Target_Nat.thy
    Author:     Florian Haftmann, TU Muenchen
*)

section \<open>Implementation of natural numbers by target-language integers\<close>

theory Code_Target_Nat
imports Code_Abstract_Nat
begin

subsection \<open>Implementation for \<^typ>\<open>nat\<close>\<close>

context
includes natural.lifting integer.lifting
begin

lift_definition Nat :: "integer \ nat"
  is nat
  .

lemma [code_post]:
  "Nat 0 = 0"
  "Nat 1 = 1"
  "Nat (numeral k) = numeral k"
  by (transfer, simp)+

lemma [code_abbrev]:
  "integer_of_nat = of_nat"
  by transfer rule

lemma [code_unfold]:
  "Int.nat (int_of_integer k) = nat_of_integer k"
  by transfer rule

lemma [code abstype]:
  "Code_Target_Nat.Nat (integer_of_nat n) = n"
  by transfer simp

lemma [code abstract]:
  "integer_of_nat (nat_of_integer k) = max 0 k"
  by transfer auto

lemma [code_abbrev]:
  "nat_of_integer (numeral k) = nat_of_num k"
  by transfer (simp add: nat_of_num_numeral)

context
begin

qualified definition natural :: "num \ nat"
  where [simp]: "natural = nat_of_num"

lemma [code_computation_unfold]:
  "numeral = natural"
  "nat_of_num = natural"
  by (simp_all add: nat_of_num_numeral)

end

lemma [code abstract]:
  "integer_of_nat (nat_of_num n) = integer_of_num n"
  by (simp add: nat_of_num_numeral integer_of_nat_numeral)

lemma [code abstract]:
  "integer_of_nat 0 = 0"
  by transfer simp

lemma [code abstract]:
  "integer_of_nat 1 = 1"
  by transfer simp

lemma [code]:
  "Suc n = n + 1"
  by simp

lemma [code abstract]:
  "integer_of_nat (m + n) = of_nat m + of_nat n"
  by transfer simp

lemma [code abstract]:
  "integer_of_nat (m - n) = max 0 (of_nat m - of_nat n)"
  by transfer simp

lemma [code abstract]:
  "integer_of_nat (m * n) = of_nat m * of_nat n"
  by transfer (simp add: of_nat_mult)

lemma [code abstract]:
  "integer_of_nat (m div n) = of_nat m div of_nat n"
  by transfer (simp add: zdiv_int)

lemma [code abstract]:
  "integer_of_nat (m mod n) = of_nat m mod of_nat n"
  by transfer (simp add: zmod_int)

context
  includes integer.lifting
begin

lemma divmod_nat_code [code]: \<^marker>\<open>contributor \<open>René Thiemann\<close>\<close> \<^marker>\<open>contributor \<open>Akihisa Yamada\<close>\<close>
  "Divides.divmod_nat m n = (
     let k = integer_of_nat m; l = integer_of_nat n
     in map_prod nat_of_integer nat_of_integer
       (if k = 0 then (0, 0)
        else if l = 0 then (0, k) else
          Code_Numeral.divmod_abs k l))"
  by (simp add: prod_eq_iff Let_def; transfer)
    (simp add: nat_div_distrib nat_mod_distrib)

end

lemma [code]:
  "divmod m n = map_prod nat_of_integer nat_of_integer (divmod m n)"
  by (simp only: prod_eq_iff divmod_def map_prod_def case_prod_beta fst_conv snd_conv; transfer)
    (simp_all only: nat_div_distrib nat_mod_distrib
        zero_le_numeral nat_numeral)

lemma [code]:
  "HOL.equal m n = HOL.equal (of_nat m :: integer) (of_nat n)"
  by transfer (simp add: equal)

lemma [code]:
  "m \ n \ (of_nat m :: integer) \ of_nat n"
  by simp

lemma [code]:
  "m < n \ (of_nat m :: integer) < of_nat n"
  by simp

lemma num_of_nat_code [code]:
  "num_of_nat = num_of_integer \ of_nat"
  by transfer (simp add: fun_eq_iff)

end

lemma (in semiring_1) of_nat_code_if:
  "of_nat n = (if n = 0 then 0
     else let
       (m, q) = Divides.divmod_nat n 2;
       m' = 2 * of_nat m
     in if q = 0 then m' else m' + 1)"
proof -
  from div_mult_mod_eq have *: "of_nat n = of_nat (n div 2 * 2 + n mod 2)" by simp
  show ?thesis
    by (simp add: Let_def divmod_nat_def of_nat_add [symmetric])
      (simp add: * mult.commute of_nat_mult add.commute)
qed

declare of_nat_code_if [code]

definition int_of_nat :: "nat \ int" where
  [code_abbrev]: "int_of_nat = of_nat"

lemma [code]:
  "int_of_nat n = int_of_integer (of_nat n)"
  by (simp add: int_of_nat_def)

lemma [code abstract]:
  "integer_of_nat (nat k) = max 0 (integer_of_int k)"
  including integer.lifting by transfer auto

definition char_of_nat :: "nat \ char"
  where [code_abbrev]: "char_of_nat = char_of"

definition nat_of_char :: "char \ nat"
  where [code_abbrev]: "nat_of_char = of_char"

lemma [code]:
  "char_of_nat = char_of_integer \ integer_of_nat"
  including integer.lifting unfolding char_of_integer_def char_of_nat_def
  by transfer (simp add: fun_eq_iff)

lemma [code abstract]:
  "integer_of_nat (nat_of_char c) = integer_of_char c"
  by (cases c) (simp add: nat_of_char_def integer_of_char_def integer_of_nat_eq_of_nat)

lemma term_of_nat_code [code]:
  \<comment> \<open>Use \<^term>\<open>Code_Numeral.nat_of_integer\<close> in term reconstruction
        instead of \<^term>\<open>Code_Target_Nat.Nat\<close> such that reconstructed
        terms can be fed back to the code generator\<close>
  "term_of_class.term_of n =
   Code_Evaluation.App
     (Code_Evaluation.Const (STR ''Code_Numeral.nat_of_integer'')
        (typerep.Typerep (STR ''fun'')
           [typerep.Typerep (STR ''Code_Numeral.integer'') [],
         typerep.Typerep (STR ''Nat.nat'') []]))
     (term_of_class.term_of (integer_of_nat n))"
  by (simp add: term_of_anything)

lemma nat_of_integer_code_post [code_post]:
  "nat_of_integer 0 = 0"
  "nat_of_integer 1 = 1"
  "nat_of_integer (numeral k) = numeral k"
  including integer.lifting by (transfer, simp)+

code_identifier
  code_module Code_Target_Nat \<rightharpoonup>
    (SML) Arith and (OCaml) Arith and (Haskell) Arith

end

¤ Dauer der Verarbeitung: 0.19 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.