lemma integer_of_num [code]: "integer_of_num Num.One = 1" "integer_of_num (Num.Bit0 n) = (let k = integer_of_num n in k + k)" "integer_of_num (Num.Bit1 n) = (let k = integer_of_num n in k + k + 1)" by (simp_all only: integer_of_num_def numeral.simps Let_def)
instantiation integer :: linordered_euclidean_semiring_division begin
definition divmod_integer :: "num \ num \ integer \ integer" where
divmod_integer'_def: "divmod_integer m n = (numeral m div numeral n, numeral m mod numeral n)"
definition divmod_step_integer :: "integer \ integer \ integer \ integer \ integer" where "divmod_step_integer l qr = (let (q, r) = qr inif\<bar>l\<bar> \<le> \<bar>r\<bar> then (2 * q + 1, r - l)
else (2 * q, r))"
instanceby standard
(auto simp add: divmod_integer'_def divmod_step_integer_def integer_less_eq_iff)
end
lemma integer_of_nat_0: "integer_of_nat 0 = 0" by transfer simp
lemma integer_of_nat_1: "integer_of_nat 1 = 1" by transfer simp
lemma integer_of_nat_numeral: "integer_of_nat (numeral n) = numeral n" by transfer simp
subsection \<open>Code theorems for target language integers\<close>
lift_definition sub :: "num \ num \ integer" is"\m n. numeral m - numeral n :: int"
.
lemma sub_code [code]: "sub Num.One Num.One = 0" "sub (Num.Bit0 m) Num.One = Pos (Num.BitM m)" "sub (Num.Bit1 m) Num.One = Pos (Num.Bit0 m)" "sub Num.One (Num.Bit0 n) = Neg (Num.BitM n)" "sub Num.One (Num.Bit1 n) = Neg (Num.Bit0 n)" "sub (Num.Bit0 m) (Num.Bit0 n) = dup (sub m n)" "sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)" "sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1" "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1" by (transfer; simp add: dbl_def dbl_inc_def dbl_dec_def)+
text\<open>Implementations\<close>
lemma one_integer_code [code, code_unfold]: "1 = Pos Num.One" by simp
lemma plus_integer_code [code]: "k + 0 = (k::integer)" "0 + l = (l::integer)" "Pos m + Pos n = Pos (m + n)" "Pos m + Neg n = sub m n" "Neg m + Pos n = sub n m" "Neg m + Neg n = Neg (m + n)" by (transfer, simp)+
lemma uminus_integer_code [code]: "uminus 0 = (0::integer)" "uminus (Pos m) = Neg m" "uminus (Neg m) = Pos m" by simp_all
lemma minus_integer_code [code]: "k - 0 = (k::integer)" "0 - l = uminus (l::integer)" "Pos m - Pos n = sub m n" "Pos m - Neg n = Pos (m + n)" "Neg m - Pos n = Neg (m + n)" "Neg m - Neg n = sub n m" by (transfer, simp)+
lemma abs_integer_code [code]: "\k\ = (if (k::integer) < 0 then - k else k)" by simp
lemma sgn_integer_code [code]: "sgn k = (if k = 0 then 0 else if (k::integer) < 0 then - 1 else 1)" by simp
lemma times_integer_code [code]: "k * 0 = (0::integer)" "0 * l = (0::integer)" "Pos m * Pos n = Pos (m * n)" "Pos m * Neg n = Neg (m * n)" "Neg m * Pos n = Neg (m * n)" "Neg m * Neg n = Pos (m * n)" by simp_all
definition divmod_integer :: "integer \ integer \ integer \ integer" where "divmod_integer k l = (k div l, k mod l)"
lemma fst_divmod_integer [simp]: "fst (divmod_integer k l) = k div l" by (simp add: divmod_integer_def)
lemma snd_divmod_integer [simp]: "snd (divmod_integer k l) = k mod l" by (simp add: divmod_integer_def)
definition divmod_abs :: "integer \ integer \ integer \ integer" where "divmod_abs k l = (\k\ div \l\, \k\ mod \l\)"
lemma fst_divmod_abs [simp]: "fst (divmod_abs k l) = \k\ div \l\" by (simp add: divmod_abs_def)
lemma snd_divmod_abs [simp]: "snd (divmod_abs k l) = \k\ mod \l\" by (simp add: divmod_abs_def)
lemma divmod_integer_eq_cases: "divmod_integer k l =
(if k = 0 then (0, 0) else if l = 0 then (0, k) else
(apsnd \<circ> times \<circ> sgn) l (if sgn k = sgn l then divmod_abs k l
else (let (r, s) = divmod_abs k l in if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))" proof - have *: "sgn k = sgn l \ k = 0 \ l = 0 \ 0 < l \ 0 < k \ l < 0 \ k < 0" for k l :: int by (auto simp add: sgn_if) have **: "- k = l * q \ k = - (l * q)" for k l q :: int by auto show ?thesis by (simp add: divmod_integer_def divmod_abs_def)
(transfer, auto simp add: * ** not_less zdiv_zminus1_eq_if zmod_zminus1_eq_if div_minus_right mod_minus_right) qed
lemma divmod_integer_code [code]: \<^marker>\<open>contributor \<open>René Thiemann\<close>\<close> \<^marker>\<open>contributor \<open>Akihisa Yamada\<close>\<close> "divmod_integer k l =
(if k = 0 then (0, 0)
else if l > 0 then
(if k > 0 then divmod_abs k l
else case divmod_abs k l of (r, s) \<Rightarrow> if s = 0 then (- r, 0) else (- r - 1, l - s))
else if l = 0 then (0, k)
else apsnd uminus
(if k < 0 then divmod_abs k l
else case divmod_abs k l of (r, s) \<Rightarrow> if s = 0 then (- r, 0) else (- r - 1, - l - s)))" by (cases l "0 :: integer" rule: linorder_cases)
(auto split: prod.splits simp add: divmod_integer_eq_cases)
lemma div_integer_code [code]: "k div l = fst (divmod_integer k l)" by simp
lemma mod_integer_code [code]: "k mod l = snd (divmod_integer k l)" by simp
context includes bit_operations_syntax begin
lemma and_integer_code [code]: \<open>0 AND k = 0\<close> \<open>k AND 0 = 0\<close> \<open>Neg Num.One AND k = k\<close> \<open>k AND Neg Num.One = k\<close> \<open>Pos Num.One AND Pos Num.One = Pos Num.One\<close> \<open>Pos Num.One AND Pos (Num.Bit0 n) = 0\<close> \<open>Pos (Num.Bit0 m) AND Pos Num.One = 0\<close> \<open>Pos Num.One AND Pos (Num.Bit1 n) = Pos Num.One\<close> \<open>Pos (Num.Bit1 m) AND Pos Num.One = Pos Num.One\<close> \<open>Pos (Num.Bit0 m) AND Pos (Num.Bit0 n) = dup (Pos m AND Pos n)\<close> \<open>Pos (Num.Bit0 m) AND Pos (Num.Bit1 n) = dup (Pos m AND Pos n)\<close> \<open>Pos (Num.Bit1 m) AND Pos (Num.Bit0 n) = dup (Pos m AND Pos n)\<close> \<open>Pos (Num.Bit1 m) AND Pos (Num.Bit1 n) = Pos Num.One + dup (Pos m AND Pos n)\<close> \<open>Pos m AND Neg (num.Bit0 n) = (case and_not_num m (Num.BitM n) of None \<Rightarrow> 0 | Some n' \<Rightarrow> Pos n')\<close> \<open>Neg (num.Bit0 m) AND Pos n = (case and_not_num n (Num.BitM m) of None \<Rightarrow> 0 | Some n' \<Rightarrow> Pos n')\<close> \<open>Pos m AND Neg (num.Bit1 n) = (case and_not_num m (Num.Bit0 n) of None \<Rightarrow> 0 | Some n' \<Rightarrow> Pos n')\<close> \<open>Neg (num.Bit1 m) AND Pos n = (case and_not_num n (Num.Bit0 m) of None \<Rightarrow> 0 | Some n' \<Rightarrow> Pos n')\<close> \<open>Neg m AND Neg n = NOT (sub m Num.One OR sub n Num.One)\<close> for k :: integer by (transfer; simp)+
lemma or_integer_code [code]: \<open>0 OR k = k\<close> \<open>k OR 0 = k\<close> \<open>Neg Num.One OR k = Neg Num.One\<close> \<open>k OR Neg Num.One = Neg Num.One\<close> \<open>Pos Num.One OR Pos Num.One = Pos Num.One\<close> \<open>Pos Num.One OR Pos (Num.Bit0 n) = Pos (Num.Bit1 n)\<close> \<open>Pos (Num.Bit0 m) OR Pos Num.One = Pos (Num.Bit1 m)\<close> \<open>Pos Num.One OR Pos (Num.Bit1 n) = Pos (Num.Bit1 n)\<close> \<open>Pos (Num.Bit1 m) OR Pos Num.One = Pos (Num.Bit1 m)\<close> \<open>Pos (Num.Bit0 m) OR Pos (Num.Bit0 n) = dup (Pos m OR Pos n)\<close> \<open>Pos (Num.Bit0 m) OR Pos (Num.Bit1 n) = Pos Num.One + dup (Pos m OR Pos n)\<close> \<open>Pos (Num.Bit1 m) OR Pos (Num.Bit0 n) = Pos Num.One + dup (Pos m OR Pos n)\<close> \<open>Pos (Num.Bit1 m) OR Pos (Num.Bit1 n) = Pos Num.One + dup (Pos m OR Pos n)\<close> \<open>Pos m OR Neg (num.Bit0 n) = Neg (or_not_num_neg m (Num.BitM n))\<close> \<open>Neg (num.Bit0 m) OR Pos n = Neg (or_not_num_neg n (Num.BitM m))\<close> \<open>Pos m OR Neg (num.Bit1 n) = Neg (or_not_num_neg m (Num.Bit0 n))\<close> \<open>Neg (num.Bit1 m) OR Pos n = Neg (or_not_num_neg n (Num.Bit0 m))\<close> \<open>Neg m OR Neg n = NOT (sub m Num.One AND sub n Num.One)\<close> for k :: integer by (transfer; simp)+
lemma xor_integer_code [code]: \<open>0 XOR k = k\<close> \<open>k XOR 0 = k\<close> \<open>Neg Num.One XOR k = NOT k\<close> \<open>k XOR Neg Num.One = NOT k\<close> \<open>Neg m XOR k = NOT (sub m num.One XOR k)\<close> \<open>k XOR Neg n = NOT (k XOR (sub n num.One))\<close> \<open>Pos Num.One XOR Pos Num.One = 0\<close> \<open>Pos Num.One XOR Pos (Num.Bit0 n) = Pos (Num.Bit1 n)\<close> \<open>Pos (Num.Bit0 m) XOR Pos Num.One = Pos (Num.Bit1 m)\<close> \<open>Pos Num.One XOR Pos (Num.Bit1 n) = Pos (Num.Bit0 n)\<close> \<open>Pos (Num.Bit1 m) XOR Pos Num.One = Pos (Num.Bit0 m)\<close> \<open>Pos (Num.Bit0 m) XOR Pos (Num.Bit0 n) = dup (Pos m XOR Pos n)\<close> \<open>Pos (Num.Bit0 m) XOR Pos (Num.Bit1 n) = Pos Num.One + dup (Pos m XOR Pos n)\<close> \<open>Pos (Num.Bit1 m) XOR Pos (Num.Bit0 n) = Pos Num.One + dup (Pos m XOR Pos n)\<close> \<open>Pos (Num.Bit1 m) XOR Pos (Num.Bit1 n) = dup (Pos m XOR Pos n)\<close> for k :: integer by (transfer; simp)+
lemma [code]: \<open>NOT k = - k - 1\<close> for k :: integer by (fact not_eq_complement)
lemma [code]: \<open>bit k n \<longleftrightarrow> k AND push_bit n 1 \<noteq> (0 :: integer)\<close> by (simp add: and_exp_eq_0_iff_not_bit)
lemma [code]: \<open>mask n = push_bit n 1 - (1 :: integer)\<close> by (simp add: mask_eq_exp_minus_1)
lemma [code]: \<open>set_bit n k = k OR push_bit n 1\<close> for k :: integer by (fact set_bit_def)
lemma [code]: \<open>unset_bit n k = k AND NOT (push_bit n 1)\<close> for k :: integer by (fact unset_bit_def)
lemma [code]: \<open>flip_bit n k = k XOR push_bit n 1\<close> for k :: integer by (fact flip_bit_def)
lemma [code]: \<open>take_bit n k = k AND mask n\<close> for k :: integer by (fact take_bit_eq_mask)
end
definition bit_cut_integer :: "integer \ integer \ bool" where"bit_cut_integer k = (k div 2, odd k)"
lemma bit_cut_integer_code [code]: "bit_cut_integer k = (if k = 0 then (0, False)
else let (r, s) = Code_Numeral.divmod_abs k 2 in (if k > 0 then r else - r - s, s = 1))" proof - have"bit_cut_integer k = (let (r, s) = divmod_integer k 2 in (r, s = 1))" by (simp add: divmod_integer_def bit_cut_integer_def odd_iff_mod_2_eq_one) thenshow ?thesis by (simp add: divmod_integer_code) (auto simp add: split_def) qed
lemma equal_integer_refl [code nbe]: "HOL.equal (k::integer) k \ True" by (fact equal_refl)
lemma less_eq_integer_code [code]: "0 \ (0::integer) \ True" "0 \ Pos l \ True" "0 \ Neg l \ False" "Pos k \ 0 \ False" "Pos k \ Pos l \ k \ l" "Pos k \ Neg l \ False" "Neg k \ 0 \ True" "Neg k \ Pos l \ True" "Neg k \ Neg l \ l \ k" by simp_all
lemma less_integer_code [code]: "0 < (0::integer) \ False" "0 < Pos l \ True" "0 < Neg l \ False" "Pos k < 0 \ False" "Pos k < Pos l \ k < l" "Pos k < Neg l \ False" "Neg k < 0 \ True" "Neg k < Pos l \ True" "Neg k < Neg l \ l < k" by simp_all
lemma num_of_integer_code [code]: "num_of_integer k = (if k \ 1 then Num.One
else let
(l, j) = divmod_integer k 2;
l' = num_of_integer l;
l'' = l' + l' inif j = 0 then l'' else l'' + Num.One)" proof -
{ assume"int_of_integer k mod 2 = 1" thenhave"nat (int_of_integer k mod 2) = nat 1"by simp moreoverassume *: "1 < int_of_integer k" ultimatelyhave **: "nat (int_of_integer k) mod 2 = 1"by (simp add: nat_mod_distrib) have"num_of_nat (nat (int_of_integer k)) =
num_of_nat (2 * (nat (int_of_integer k) div 2) + nat (int_of_integer k) mod 2)" by simp thenhave"num_of_nat (nat (int_of_integer k)) =
num_of_nat (nat (int_of_integer k) div 2 + nat (int_of_integer k) div 2 + nat (int_of_integer k) mod 2)" by (simp add: mult_2) with ** have"num_of_nat (nat (int_of_integer k)) =
num_of_nat (nat (int_of_integer k) div 2 + nat (int_of_integer k) div 2 + 1)" by simp
} note aux = this show ?thesis by (auto simp add: num_of_integer_def nat_of_integer_def Let_def case_prod_beta
not_le integer_eq_iff less_eq_integer_def
nat_mult_distrib nat_div_distrib num_of_nat_One num_of_nat_plus_distrib
mult_2 [where'a=nat] aux add_One) qed
lemma nat_of_integer_code [code]: "nat_of_integer k = (if k \ 0 then 0
else let
(l, j) = divmod_integer k 2;
l' = nat_of_integer l;
l'' = l' + l' inif j = 0 then l'' else l'' + 1)" proof - obtain j where k: "k = integer_of_int j" proof show"k = integer_of_int (int_of_integer k)"by simp qed have *: "nat j mod 2 = nat_of_integer (of_int j mod 2)"if"j \ 0" using that by transfer (simp add: nat_mod_distrib) from k show ?thesis by (auto simp add: split_def Let_def nat_of_integer_def nat_div_distrib mult_2 [symmetric]
minus_mod_eq_mult_div [symmetric] *) qed
lemma int_of_integer_code [code]: \<open>int_of_integer k = ( if k = 0 then 0
else if k = - 1 then - 1
else let
(l, j) = divmod_integer k 2;
l' = 2 * int_of_integer l inif j = 0 then l' else l' + 1)\<close> by (auto simp add: case_prod_unfold Let_def integer_eq_iff simp flip: minus_mod_eq_mult_div)
lemma integer_of_int_code [code]: \<open>integer_of_int k = ( if k = 0 then 0
else if k = - 1 then - 1
else let
l = 2 * integer_of_int (k div 2);
j = k mod 2 inif j = 0 then l else l + 1)\<close> by (simp add: integer_eq_iff Let_def flip: minus_mod_eq_mult_div)
hide_const (open) Pos Neg sub dup divmod_abs
context begin
qualified definition push_bit :: \<open>integer \<Rightarrow> integer \<Rightarrow> integer\<close> where\<open>push_bit i k = Bit_Operations.push_bit (nat_of_integer \<bar>i\<bar>) k\<close>
qualified lemma push_bit_code [code]: \<open>push_bit i k = k * 2 ^ nat_of_integer \<bar>i\<bar>\<close> by (simp add: push_bit_def push_bit_eq_mult)
lemma push_bit_integer_code [code]: \<open>Bit_Operations.push_bit n k = push_bit (of_nat n) k\<close> by (simp add: push_bit_def)
qualified definition drop_bit :: \<open>integer \<Rightarrow> integer \<Rightarrow> integer\<close> where\<open>drop_bit i k = Bit_Operations.drop_bit (nat_of_integer \<bar>i\<bar>) k\<close>
qualified lemma drop_bit_code [code]: \<open>drop_bit i k = k div 2 ^ nat_of_integer \<bar>i\<bar>\<close> by (simp add: drop_bit_def drop_bit_eq_div)
lemma drop_bit_integer_code [code]: \<open>Bit_Operations.drop_bit n k = drop_bit (of_nat n) k\<close> by (simp add: drop_bit_def)
end
subsection \<open>Serializer setup for target language integers\<close>
code_printing
type_constructor integer \<rightharpoonup>
(SML) "IntInf.int" and (OCaml) "Z.t" and (Haskell) "Integer" and (Scala) "BigInt" and (Eval) "int"
| class_instance integer :: equal \<rightharpoonup>
(Haskell) -
code_reserved
(Eval) int Integer
code_printing
constant "0::integer"\<rightharpoonup>
(SML) "!(0/ :/ IntInf.int)" and (OCaml) "Z.zero" and (Haskell) "!(0/ ::/ Integer)" and (Scala) "BigInt(0)"
code_printing
constant "plus :: integer \ _ \ _" \
(SML) "IntInf.+ ((_), (_))" and (OCaml) "Z.add" and (Haskell) infixl 6 "+" and (Scala) infixl 7 "+" and (Eval) infixl 8 "+"
| constant "uminus :: integer \ _" \
(SML) "IntInf.~" and (OCaml) "Z.neg" and (Haskell) "negate" and (Scala) "!(- _)" and (Eval) "~/ _"
| constant "minus :: integer \ _" \
(SML) "IntInf.- ((_), (_))" and (OCaml) "Z.sub" and (Haskell) infixl 6 "-" and (Scala) infixl 7 "-" and (Eval) infixl 8 "-"
| constant Code_Numeral.dup \<rightharpoonup>
(SML) "IntInf.*/ (2,/ (_))" and (OCaml) "Z.shift'_left/ _/ 1" and (Haskell) "!(2 * _)" and (Scala) "!(2 * _)" and (Eval) "!(2 * _)"
| constant Code_Numeral.sub \<rightharpoonup>
(SML) "!(raise/ Fail/ \"sub\")" and (OCaml) "failwith/ \"sub\"" and (Haskell) "error/ \"sub\"" and (Scala) "!sys.error(\"sub\")"
| constant "times :: integer \ _ \ _" \
(SML) "IntInf.* ((_), (_))" and (OCaml) "Z.mul" and (Haskell) infixl 7 "*" and (Scala) infixl 8 "*" and (Eval) infixl 9 "*"
| constant Code_Numeral.divmod_abs \<rightharpoonup>
(SML) "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)" and (OCaml) "!(fun k l ->/ if Z.equal Z.zero l then/ (Z.zero, l) else/ Z.div'_rem/ (Z.abs k)/ (Z.abs l))" and (Haskell) "divMod/ (abs _)/ (abs _)" and (Scala) "!((k: BigInt) => (l: BigInt) =>/ l == 0 match { case true => (BigInt(0), k) case false => (k.abs '/% l.abs) })" and (Eval) "Integer.div'_mod/ (abs _)/ (abs _)"
| constant "HOL.equal :: integer \ _ \ bool" \
(SML) "!((_ : IntInf.int) = _)" and (OCaml) "Z.equal" and (Haskell) infix 4 "==" and (Scala) infixl 5 "==" and (Eval) infixl 6 "="
| constant "less_eq :: integer \ _ \ bool" \
(SML) "IntInf.<= ((_), (_))" and (OCaml) "Z.leq" and (Haskell) infix 4 "<=" and (Scala) infixl 4 "<=" and (Eval) infixl 6 "<="
| constant "less :: integer \ _ \ bool" \
(SML) "IntInf.< ((_), (_))" and (OCaml) "Z.lt" and (Haskell) infix 4 "<" and (Scala) infixl 4 "<" and (Eval) infixl 6 "<"
| constant "abs :: integer \ _" \
(SML) "IntInf.abs" and (OCaml) "Z.abs" and (Haskell) "Prelude.abs" and (Scala) "_.abs" and (Eval) "abs"
| constant "Bit_Operations.and :: integer \ integer \ integer" \
(SML) "IntInf.andb ((_),/ (_))" and (OCaml) "Z.logand" and (Haskell) infixl 7 ".&." and (Scala) infixl 3 "&"
| constant "Bit_Operations.or :: integer \ integer \ integer" \
(SML) "IntInf.orb ((_),/ (_))" and (OCaml) "Z.logor" and (Haskell) infixl 5 ".|." and (Scala) infixl 1 "|"
| constant "Bit_Operations.xor :: integer \ integer \ integer" \
(SML) "IntInf.xorb ((_),/ (_))" and (OCaml) "Z.logxor" and (Haskell) infixl 6 ".^." and (Scala) infixl 2 "^"
| constant "Bit_Operations.not :: integer \ integer" \
(SML) "IntInf.notb" and (OCaml) "Z.lognot" and (Haskell) "Data.Bits.complement" and (Scala) "_.unary'_~"
code_reserved
(Eval) abs
code_printing code_module Bit_Shifts \<rightharpoonup>
(SML) \<open> structure Bit_Shifts : sig
type int = IntInf.int
val push : int -> int -> int
val drop : int -> int -> int end = struct
open IntInf;
fun fold _ [] y = y
| fold f (x :: xs) y = fold f xs (f x y);
fun replicate n x = (if n <= 0 then [] else x :: replicate (n - 1) x);
val max_index = pow (fromInt 2, Word.wordSize) - fromInt 1; (*largest possible word*)
val word_of_int = Word.fromLargeInt o toLarge;
val word_max_index = word_of_int max_index;
fun words_of_int k = case divMod (k, max_index)
of (b, s) => word_of_int s :: replicate b word_max_index;
fun push' i k = << (k, i);
fun drop' i k = ~>> (k, i);
(* The implementations are formally total, though indices >~ max_index will produce heavy computation load *)
fun push i = fold push' (words_of_int (abs i));
fun drop i = fold drop' (words_of_int (abs i));
end;\<close> for constant Code_Numeral.push_bit Code_Numeral.drop_bit and (OCaml) \<open>
module Bit_Shifts : sig
val push : Z.t -> Z.t -> Z.t
val drop : Z.t -> Z.t -> Z.t end = struct
let rec fold f xs y = match xs with
[] -> y
| (x :: xs) -> fold f xs (f x y);;
let rec replicate n x = (if Z.leq n Z.zero then [] else x :: replicate (Z.pred n) x);;
let max_index = Z.of_int max_int;;
let splitIndex i = let (b, s) = Z.div_rem i max_index in Z.to_int s :: replicate b max_int;;
let push' i k = Z.shift_left k i;;
let drop' i k = Z.shift_right k i;;
(* The implementations are formally total, though indices >~ max_index will produce heavy computation load *)
let push i = fold push' (splitIndex (Z.abs i));;
let drop i = fold drop' (splitIndex (Z.abs i));;
end;; \<close> for constant Code_Numeral.push_bit Code_Numeral.drop_bit and (Haskell) \<open>
module Bit_Shifts (push, drop, push', drop') where
drop :: Integer -> Integer -> Integer
drop i = fold (flip shiftR) (splitIndex (abs i))
push' :: Int -> Int -> Int
push' i = flip shiftL (abs i)
drop' :: Int -> Int -> Int
drop' i = flip shiftR (abs i) \<close> for constant Code_Numeral.push_bit Code_Numeral.drop_bit and (Scala) \<open>
object Bit_Shifts {
private val maxIndex : BigInt = BigInt(Int.MaxValue);
private def replicate[A](i : BigInt, x : A) : List[A] =
i <= 0 match { case true => Nil case false => x :: replicate[A](i - 1, x)
}
} \<close> for constant Code_Numeral.push_bit Code_Numeral.drop_bit
code_reserved
(SML) Bit_Shifts and (Haskell) Bit_Shifts and (Scala) Bit_Shifts
code_printing
constant Code_Numeral.push_bit \<rightharpoonup>
(SML) "Bit'_Shifts.push" and (OCaml) "Bit'_Shifts.push" and (Haskell) "Bit'_Shifts.push" and (Scala) "Bit'_Shifts.push"
| constant Code_Numeral.drop_bit \<rightharpoonup>
(SML) "Bit'_Shifts.drop" and (OCaml) "Bit'_Shifts.drop" and (Haskell) "Bit'_Shifts.drop" and (Scala) "Bit'_Shifts.drop"
code_identifier code_module Code_Numeral \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
subsection \<open>Type of target language naturals\<close>
lemma [code abstype]: "Nat (integer_of_natural n) = n" by transfer simp
lemma [code]: "natural_of_nat n = natural_of_integer (integer_of_nat n)" by transfer simp
lemma [code abstract]: "integer_of_natural (natural_of_integer k) = max 0 k" by simp
lemma [code]: \<open>integer_of_natural (mask n) = mask n\<close> by transfer (simp add: mask_eq_exp_minus_1)
lemma [code_abbrev]: "natural_of_integer (Code_Numeral.Pos k) = numeral k" by transfer simp
lemma [code abstract]: "integer_of_natural 0 = 0" by transfer simp
lemma [code abstract]: "integer_of_natural 1 = 1" by transfer simp
lemma [code abstract]: "integer_of_natural (Code_Numeral.Suc n) = integer_of_natural n + 1" by transfer simp
lemma [code]: "nat_of_natural = nat_of_integer \ integer_of_natural" by transfer (simp add: fun_eq_iff)
lemma [code, code_unfold]: "case_natural f g n = (if n = 0 then f else g (n - 1))" by (cases n rule: natural.exhaust) (simp_all, simp add: Suc_def)
declare natural.rec [code del]
lemma [code abstract]: "integer_of_natural (m + n) = integer_of_natural m + integer_of_natural n" by transfer simp
lemma [code abstract]: "integer_of_natural (m - n) = max 0 (integer_of_natural m - integer_of_natural n)" by transfer simp
lemma [code abstract]: "integer_of_natural (m * n) = integer_of_natural m * integer_of_natural n" by transfer simp
lemma [code abstract]: "integer_of_natural (m div n) = integer_of_natural m div integer_of_natural n" by transfer (simp add: zdiv_int)
lemma [code abstract]: "integer_of_natural (m mod n) = integer_of_natural m mod integer_of_natural n" by transfer (simp add: zmod_int)
lemma [code nbe]: "HOL.equal n (n::natural) \ True" by (rule equal_class.equal_refl)
lemma [code]: "HOL.equal m n \ HOL.equal (integer_of_natural m) (integer_of_natural n)" by transfer (simp add: equal)
lemma [code]: "m \ n \ integer_of_natural m \ integer_of_natural n" by transfer simp
lemma [code]: "m < n \ integer_of_natural m < integer_of_natural n" by transfer simp
context includes bit_operations_syntax begin
lemma [code]: \<open>bit m n \<longleftrightarrow> bit (integer_of_natural m) n\<close> by transfer (simp add: bit_simps)
lemma [code abstract]: \<open>integer_of_natural (m AND n) = integer_of_natural m AND integer_of_natural n\<close> by transfer (simp add: of_nat_and_eq)
lemma [code abstract]: \<open>integer_of_natural (m OR n) = integer_of_natural m OR integer_of_natural n\<close> by transfer (simp add: of_nat_or_eq)
lemma [code abstract]: \<open>integer_of_natural (m XOR n) = integer_of_natural m XOR integer_of_natural n\<close> by transfer (simp add: of_nat_xor_eq)
lemma [code abstract]: \<open>integer_of_natural (mask n) = mask n\<close> by transfer (simp add: of_nat_mask_eq)
lemma [code abstract]: \<open>integer_of_natural (set_bit n m) = set_bit n (integer_of_natural m)\<close> by transfer (simp add: of_nat_set_bit_eq)
lemma [code abstract]: \<open>integer_of_natural (unset_bit n m) = unset_bit n (integer_of_natural m)\<close> by transfer (simp add: of_nat_unset_bit_eq)
lemma [code abstract]: \<open>integer_of_natural (flip_bit n m) = flip_bit n (integer_of_natural m)\<close> by transfer (simp add: of_nat_flip_bit_eq)
lemma [code abstract]: \<open>integer_of_natural (push_bit n m) = push_bit n (integer_of_natural m)\<close> by transfer (simp add: of_nat_push_bit)
lemma [code abstract]: \<open>integer_of_natural (drop_bit n m) = drop_bit n (integer_of_natural m)\<close> by transfer (simp add: of_nat_drop_bit)
lemma [code abstract]: \<open>integer_of_natural (take_bit n m) = take_bit n (integer_of_natural m)\<close> by transfer (simp add: of_nat_take_bit)
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.
