Quelle Code_Target_Int.thy Sprache: Isabelle

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

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

theory Code_Target_Int
imports Main
begin

code_datatype int_of_integer

context
includes integer.lifting
begin

lemma [code]:
  "integer_of_int (int_of_integer k) = k"
  by transfer rule

lemma [code]:
  "Int.Pos = int_of_integer \ integer_of_num"
  by transfer (simp add: fun_eq_iff)

lemma [code]:
  "Int.Neg = int_of_integer \ uminus \ integer_of_num"
  by transfer (simp add: fun_eq_iff)

lemma [code_abbrev]:
  "int_of_integer (numeral k) = Int.Pos k"
  by transfer simp

lemma [code_abbrev]:
  "int_of_integer (- numeral k) = Int.Neg k"
  by transfer simp

context
begin

qualified definition positive :: "num \ int"
  where [simp]: "positive = numeral"

qualified definition negative :: "num \ int"
  where [simp]: "negative = uminus \ numeral"

lemma [code_computation_unfold]:
  "numeral = positive"
  "Int.Pos = positive"
  "Int.Neg = negative"
  by (simp_all add: fun_eq_iff)

end

lemma [code, symmetric, code_post]:
  "0 = int_of_integer 0"
  by transfer simp

lemma [code, symmetric, code_post]:
  "1 = int_of_integer 1"
  by transfer simp

lemma [code_post]:
  "int_of_integer (- 1) = - 1"
  by simp

lemma [code]:
  "k + l = int_of_integer (of_int k + of_int l)"
  by transfer simp

lemma [code]:
  "- k = int_of_integer (- of_int k)"
  by transfer simp

lemma [code]:
  "k - l = int_of_integer (of_int k - of_int l)"
  by transfer simp

lemma [code]:
  "Int.dup k = int_of_integer (Code_Numeral.dup (of_int k))"
  by transfer simp

declare [[code drop: Int.sub]]

lemma [code]:
  "k * l = int_of_integer (of_int k * of_int l)"
  by simp

lemma [code]:
  "k div l = int_of_integer (of_int k div of_int l)"
  by simp

lemma [code]:
  "k mod l = int_of_integer (of_int k mod of_int l)"
  by simp

lemma [code]:
  "divmod m n = map_prod int_of_integer int_of_integer (divmod m n)"
  unfolding prod_eq_iff divmod_def map_prod_def case_prod_beta fst_conv snd_conv
  by transfer simp

lemma [code]:
  "HOL.equal k l = HOL.equal (of_int k :: integer) (of_int l)"
  by transfer (simp add: equal)

lemma [code]:
  "k \ l \ (of_int k :: integer) \ of_int l"
  by transfer rule

lemma [code]:
  "k < l \ (of_int k :: integer) < of_int l"
  by transfer rule

lemma gcd_int_of_integer [code]:
  "gcd (int_of_integer x) (int_of_integer y) = int_of_integer (gcd x y)"
  by transfer rule

lemma lcm_int_of_integer [code]:
  "lcm (int_of_integer x) (int_of_integer y) = int_of_integer (lcm x y)"
  by transfer rule

end

lemma (in ring_1) of_int_code_if:
  "of_int k = (if k = 0 then 0
     else if k < 0 then - of_int (- k)
     else let
       l = 2 * of_int (k div 2);
       j = k mod 2
     in if j = 0 then l else l + 1)"
proof -
  from div_mult_mod_eq have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
  show ?thesis
    by (simp add: Let_def of_int_add [symmetric]) (simp add: * mult.commute)
qed

declare of_int_code_if [code]

lemma [code]:
  "nat = nat_of_integer \ of_int"
  including integer.lifting by transfer (simp add: fun_eq_iff)

definition char_of_int :: "int \ char"
  where [code_abbrev]: "char_of_int = char_of"

definition int_of_char :: "char \ int"
  where [code_abbrev]: "int_of_char = of_char"

lemma [code]:
  "char_of_int = char_of_integer \ integer_of_int"
  including integer.lifting unfolding char_of_integer_def char_of_int_def
  by transfer (simp add: fun_eq_iff)

lemma [code]:
  "int_of_char = int_of_integer \ integer_of_char"
  including integer.lifting unfolding integer_of_char_def int_of_char_def
  by transfer (simp add: fun_eq_iff)

context
  includes integer.lifting and bit_operations_syntax
begin

lemma [code]:
  \<open>bit (int_of_integer k) n \<longleftrightarrow> bit k n\<close>
  by transfer rule

lemma [code]:
  \<open>NOT (int_of_integer k) = int_of_integer (NOT k)\<close>
  by transfer rule

lemma [code]:
  \<open>int_of_integer k AND int_of_integer l = int_of_integer (k AND l)\<close>
  by transfer rule

lemma [code]:
  \<open>int_of_integer k OR int_of_integer l = int_of_integer (k OR l)\<close>
  by transfer rule

lemma [code]:
  \<open>int_of_integer k XOR int_of_integer l = int_of_integer (k XOR l)\<close>
  by transfer rule

lemma [code]:
  \<open>push_bit n (int_of_integer k) = int_of_integer (push_bit n k)\<close>
  by transfer rule

lemma [code]:
  \<open>drop_bit n (int_of_integer k) = int_of_integer (drop_bit n k)\<close>
  by transfer rule

lemma [code]:
  \<open>take_bit n (int_of_integer k) = int_of_integer (take_bit n k)\<close>
  by transfer rule

lemma [code]:
  \<open>mask n = int_of_integer (mask n)\<close>
  by transfer rule

lemma [code]:
  \<open>set_bit n (int_of_integer k) = int_of_integer (set_bit n k)\<close>
  by transfer rule

lemma [code]:
  \<open>unset_bit n (int_of_integer k) = int_of_integer (unset_bit n k)\<close>
  by transfer rule

lemma [code]:
  \<open>flip_bit n (int_of_integer k) = int_of_integer (flip_bit n k)\<close>
  by transfer rule

end

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

end

quality100%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.