--- a/src/HOL/Code_Numeral.thy Fri Feb 15 08:31:30 2013 +0100
+++ b/src/HOL/Code_Numeral.thy Fri Feb 15 08:31:31 2013 +0100
@@ -1,337 +1,614 @@
-(* Author: Florian Haftmann, TU Muenchen *)
+(* Title: HOL/Code_Numeral.thy
+ Author: Florian Haftmann, TU Muenchen
+*)
-header {* Type of target language numerals *}
+header {* Numeric types for code generation onto target language numerals only *}
theory Code_Numeral
-imports Nat_Transfer Divides
+imports Nat_Transfer Divides Lifting
+begin
+
+subsection {* Type of target language integers *}
+
+typedef integer = "UNIV \<Colon> int set"
+ morphisms int_of_integer integer_of_int ..
+
+setup_lifting (no_code) type_definition_integer
+
+lemma integer_eq_iff:
+ "k = l \<longleftrightarrow> int_of_integer k = int_of_integer l"
+ by transfer rule
+
+lemma integer_eqI:
+ "int_of_integer k = int_of_integer l \<Longrightarrow> k = l"
+ using integer_eq_iff [of k l] by simp
+
+lemma int_of_integer_integer_of_int [simp]:
+ "int_of_integer (integer_of_int k) = k"
+ by transfer rule
+
+lemma integer_of_int_int_of_integer [simp]:
+ "integer_of_int (int_of_integer k) = k"
+ by transfer rule
+
+instantiation integer :: ring_1
begin
-text {*
- Code numerals are isomorphic to HOL @{typ nat} but
- mapped to target-language builtin numerals.
-*}
+lift_definition zero_integer :: integer
+ is "0 :: int"
+ .
+
+declare zero_integer.rep_eq [simp]
-subsection {* Datatype of target language numerals *}
+lift_definition one_integer :: integer
+ is "1 :: int"
+ .
+
+declare one_integer.rep_eq [simp]
-typedef code_numeral = "UNIV \<Colon> nat set"
- morphisms nat_of of_nat ..
+lift_definition plus_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
+ is "plus :: int \<Rightarrow> int \<Rightarrow> int"
+ .
+
+declare plus_integer.rep_eq [simp]
-lemma of_nat_nat_of [simp]:
- "of_nat (nat_of k) = k"
- by (rule nat_of_inverse)
+lift_definition uminus_integer :: "integer \<Rightarrow> integer"
+ is "uminus :: int \<Rightarrow> int"
+ .
+
+declare uminus_integer.rep_eq [simp]
-lemma nat_of_of_nat [simp]:
- "nat_of (of_nat n) = n"
- by (rule of_nat_inverse) (rule UNIV_I)
+lift_definition minus_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
+ is "minus :: int \<Rightarrow> int \<Rightarrow> int"
+ .
+
+declare minus_integer.rep_eq [simp]
-lemma [measure_function]:
- "is_measure nat_of" by (rule is_measure_trivial)
+lift_definition times_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
+ is "times :: int \<Rightarrow> int \<Rightarrow> int"
+ .
+
+declare times_integer.rep_eq [simp]
-lemma code_numeral:
- "(\<And>n\<Colon>code_numeral. PROP P n) \<equiv> (\<And>n\<Colon>nat. PROP P (of_nat n))"
-proof
- fix n :: nat
- assume "\<And>n\<Colon>code_numeral. PROP P n"
- then show "PROP P (of_nat n)" .
-next
- fix n :: code_numeral
- assume "\<And>n\<Colon>nat. PROP P (of_nat n)"
- then have "PROP P (of_nat (nat_of n))" .
- then show "PROP P n" by simp
+instance proof
+qed (transfer, simp add: algebra_simps)+
+
+end
+
+lemma [transfer_rule]:
+ "fun_rel HOL.eq cr_integer (of_nat :: nat \<Rightarrow> int) (of_nat :: nat \<Rightarrow> integer)"
+ by (unfold of_nat_def [abs_def]) transfer_prover
+
+lemma [transfer_rule]:
+ "fun_rel HOL.eq cr_integer (\<lambda>k :: int. k :: int) (of_int :: int \<Rightarrow> integer)"
+proof -
+ have "fun_rel HOL.eq cr_integer (of_int :: int \<Rightarrow> int) (of_int :: int \<Rightarrow> integer)"
+ by (unfold of_int_of_nat [abs_def]) transfer_prover
+ then show ?thesis by (simp add: id_def)
qed
-lemma code_numeral_case:
- assumes "\<And>n. k = of_nat n \<Longrightarrow> P"
- shows P
- by (rule assms [of "nat_of k"]) simp
-
-lemma code_numeral_induct_raw:
- assumes "\<And>n. P (of_nat n)"
- shows "P k"
+lemma [transfer_rule]:
+ "fun_rel HOL.eq cr_integer (numeral :: num \<Rightarrow> int) (numeral :: num \<Rightarrow> integer)"
proof -
- from assms have "P (of_nat (nat_of k))" .
+ have "fun_rel HOL.eq cr_integer (numeral :: num \<Rightarrow> int) (\<lambda>n. of_int (numeral n))"
+ by transfer_prover
then show ?thesis by simp
qed
-lemma nat_of_inject [simp]:
- "nat_of k = nat_of l \<longleftrightarrow> k = l"
- by (rule nat_of_inject)
+lemma [transfer_rule]:
+ "fun_rel HOL.eq cr_integer (neg_numeral :: num \<Rightarrow> int) (neg_numeral :: num \<Rightarrow> integer)"
+ by (unfold neg_numeral_def [abs_def]) transfer_prover
+
+lemma [transfer_rule]:
+ "fun_rel HOL.eq (fun_rel HOL.eq cr_integer) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> int) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> integer)"
+ by (unfold Num.sub_def [abs_def]) transfer_prover
+
+lemma int_of_integer_of_nat [simp]:
+ "int_of_integer (of_nat n) = of_nat n"
+ by transfer rule
+
+lift_definition integer_of_nat :: "nat \<Rightarrow> integer"
+ is "of_nat :: nat \<Rightarrow> int"
+ .
+
+lemma integer_of_nat_eq_of_nat [code]:
+ "integer_of_nat = of_nat"
+ by transfer rule
+
+lemma int_of_integer_integer_of_nat [simp]:
+ "int_of_integer (integer_of_nat n) = of_nat n"
+ by transfer rule
+
+lift_definition nat_of_integer :: "integer \<Rightarrow> nat"
+ is Int.nat
+ .
-lemma of_nat_inject [simp]:
- "of_nat n = of_nat m \<longleftrightarrow> n = m"
- by (rule of_nat_inject) (rule UNIV_I)+
+lemma nat_of_integer_of_nat [simp]:
+ "nat_of_integer (of_nat n) = n"
+ by transfer simp
+
+lemma int_of_integer_of_int [simp]:
+ "int_of_integer (of_int k) = k"
+ by transfer simp
+
+lemma nat_of_integer_integer_of_nat [simp]:
+ "nat_of_integer (integer_of_nat n) = n"
+ by transfer simp
+
+lemma integer_of_int_eq_of_int [simp, code_abbrev]:
+ "integer_of_int = of_int"
+ by transfer (simp add: fun_eq_iff)
-instantiation code_numeral :: zero
+lemma of_int_integer_of [simp]:
+ "of_int (int_of_integer k) = (k :: integer)"
+ by transfer rule
+
+lemma int_of_integer_numeral [simp]:
+ "int_of_integer (numeral k) = numeral k"
+ by transfer rule
+
+lemma int_of_integer_neg_numeral [simp]:
+ "int_of_integer (neg_numeral k) = neg_numeral k"
+ by transfer rule
+
+lemma int_of_integer_sub [simp]:
+ "int_of_integer (Num.sub k l) = Num.sub k l"
+ by transfer rule
+
+instantiation integer :: "{ring_div, equal, linordered_idom}"
begin
-definition [simp, code del]:
- "0 = of_nat 0"
+lift_definition div_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
+ is "Divides.div :: int \<Rightarrow> int \<Rightarrow> int"
+ .
+
+declare div_integer.rep_eq [simp]
+
+lift_definition mod_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
+ is "Divides.mod :: int \<Rightarrow> int \<Rightarrow> int"
+ .
+
+declare mod_integer.rep_eq [simp]
+
+lift_definition abs_integer :: "integer \<Rightarrow> integer"
+ is "abs :: int \<Rightarrow> int"
+ .
+
+declare abs_integer.rep_eq [simp]
-instance ..
+lift_definition sgn_integer :: "integer \<Rightarrow> integer"
+ is "sgn :: int \<Rightarrow> int"
+ .
+
+declare sgn_integer.rep_eq [simp]
+
+lift_definition less_eq_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
+ is "less_eq :: int \<Rightarrow> int \<Rightarrow> bool"
+ .
+
+lift_definition less_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
+ is "less :: int \<Rightarrow> int \<Rightarrow> bool"
+ .
+
+lift_definition equal_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
+ is "HOL.equal :: int \<Rightarrow> int \<Rightarrow> bool"
+ .
+
+instance proof
+qed (transfer, simp add: algebra_simps equal less_le_not_le [symmetric] mult_strict_right_mono linear)+
end
-definition Suc where [simp]:
- "Suc k = of_nat (Nat.Suc (nat_of k))"
+lemma [transfer_rule]:
+ "fun_rel cr_integer (fun_rel cr_integer cr_integer) (min :: _ \<Rightarrow> _ \<Rightarrow> int) (min :: _ \<Rightarrow> _ \<Rightarrow> integer)"
+ by (unfold min_def [abs_def]) transfer_prover
+
+lemma [transfer_rule]:
+ "fun_rel cr_integer (fun_rel cr_integer cr_integer) (max :: _ \<Rightarrow> _ \<Rightarrow> int) (max :: _ \<Rightarrow> _ \<Rightarrow> integer)"
+ by (unfold max_def [abs_def]) transfer_prover
+
+lemma int_of_integer_min [simp]:
+ "int_of_integer (min k l) = min (int_of_integer k) (int_of_integer l)"
+ by transfer rule
+
+lemma int_of_integer_max [simp]:
+ "int_of_integer (max k l) = max (int_of_integer k) (int_of_integer l)"
+ by transfer rule
-rep_datatype "0 \<Colon> code_numeral" Suc
-proof -
- fix P :: "code_numeral \<Rightarrow> bool"
- fix k :: code_numeral
- assume "P 0" then have init: "P (of_nat 0)" by simp
- assume "\<And>k. P k \<Longrightarrow> P (Suc k)"
- then have "\<And>n. P (of_nat n) \<Longrightarrow> P (Suc (of_nat n))" .
- then have step: "\<And>n. P (of_nat n) \<Longrightarrow> P (of_nat (Nat.Suc n))" by simp
- from init step have "P (of_nat (nat_of k))"
- by (induct ("nat_of k")) simp_all
- then show "P k" by simp
-qed simp_all
+lemma nat_of_integer_non_positive [simp]:
+ "k \<le> 0 \<Longrightarrow> nat_of_integer k = 0"
+ by transfer simp
+
+lemma of_nat_of_integer [simp]:
+ "of_nat (nat_of_integer k) = max 0 k"
+ by transfer auto
+
-declare code_numeral_case [case_names nat, cases type: code_numeral]
-declare code_numeral.induct [case_names nat, induct type: code_numeral]
+subsection {* Code theorems for target language integers *}
+
+text {* Constructors *}
-lemma code_numeral_decr [termination_simp]:
- "k \<noteq> of_nat 0 \<Longrightarrow> nat_of k - Nat.Suc 0 < nat_of k"
- by (cases k) simp
+definition Pos :: "num \<Rightarrow> integer"
+where
+ [simp, code_abbrev]: "Pos = numeral"
+
+lemma [transfer_rule]:
+ "fun_rel HOL.eq cr_integer numeral Pos"
+ by simp transfer_prover
-lemma [simp, code]:
- "code_numeral_size = nat_of"
-proof (rule ext)
- fix k
- have "code_numeral_size k = nat_size (nat_of k)"
- by (induct k rule: code_numeral.induct) (simp_all del: zero_code_numeral_def Suc_def, simp_all)
- also have "nat_size (nat_of k) = nat_of k" by (induct ("nat_of k")) simp_all
- finally show "code_numeral_size k = nat_of k" .
-qed
+definition Neg :: "num \<Rightarrow> integer"
+where
+ [simp, code_abbrev]: "Neg = neg_numeral"
+
+lemma [transfer_rule]:
+ "fun_rel HOL.eq cr_integer neg_numeral Neg"
+ by simp transfer_prover
+
+code_datatype "0::integer" Pos Neg
+
+
+text {* Auxiliary operations *}
+
+lift_definition dup :: "integer \<Rightarrow> integer"
+ is "\<lambda>k::int. k + k"
+ .
-lemma [simp, code]:
- "size = nat_of"
-proof (rule ext)
- fix k
- show "size k = nat_of k"
- by (induct k) (simp_all del: zero_code_numeral_def Suc_def, simp_all)
-qed
+lemma dup_code [code]:
+ "dup 0 = 0"
+ "dup (Pos n) = Pos (Num.Bit0 n)"
+ "dup (Neg n) = Neg (Num.Bit0 n)"
+ by (transfer, simp only: neg_numeral_def numeral_Bit0 minus_add_distrib)+
+
+lift_definition sub :: "num \<Rightarrow> num \<Rightarrow> integer"
+ is "\<lambda>m n. numeral m - numeral n :: int"
+ .
-lemmas [code del] = code_numeral.recs code_numeral.cases
-
-lemma [code]:
- "HOL.equal k l \<longleftrightarrow> HOL.equal (nat_of k) (nat_of l)"
- by (cases k, cases l) (simp add: equal)
-
-lemma [code nbe]:
- "HOL.equal (k::code_numeral) k \<longleftrightarrow> True"
- by (rule equal_refl)
+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)+
-subsection {* Basic arithmetic *}
+text {* Implementations *}
-instantiation code_numeral :: "{minus, linordered_semidom, semiring_div, linorder}"
-begin
-
-definition [simp, code del]:
- "(1\<Colon>code_numeral) = of_nat 1"
+lemma one_integer_code [code, code_unfold]:
+ "1 = Pos Num.One"
+ by simp
-definition [simp, code del]:
- "n + m = of_nat (nat_of n + nat_of m)"
-
-definition [simp, code del]:
- "n - m = of_nat (nat_of n - nat_of m)"
-
-definition [simp, code del]:
- "n * m = of_nat (nat_of n * nat_of m)"
-
-definition [simp, code del]:
- "n div m = of_nat (nat_of n div nat_of m)"
+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)+
-definition [simp, code del]:
- "n mod m = of_nat (nat_of n mod nat_of m)"
-
-definition [simp, code del]:
- "n \<le> m \<longleftrightarrow> nat_of n \<le> nat_of m"
-
-definition [simp, code del]:
- "n < m \<longleftrightarrow> nat_of n < nat_of m"
-
-instance proof
-qed (auto simp add: code_numeral distrib_right intro: mult_commute)
+lemma uminus_integer_code [code]:
+ "uminus 0 = (0::integer)"
+ "uminus (Pos m) = Neg m"
+ "uminus (Neg m) = Pos m"
+ by simp_all
-end
-
-lemma nat_of_numeral [simp]: "nat_of (numeral k) = numeral k"
- by (induct k rule: num_induct) (simp_all add: numeral_inc)
+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)+
-definition Num :: "num \<Rightarrow> code_numeral"
- where [simp, code_abbrev]: "Num = numeral"
+lemma abs_integer_code [code]:
+ "\<bar>k\<bar> = (if (k::integer) < 0 then - k else k)"
+ by simp
-code_datatype "0::code_numeral" Num
-
-lemma one_code_numeral_code [code]:
- "(1\<Colon>code_numeral) = Numeral1"
+lemma sgn_integer_code [code]:
+ "sgn k = (if k = 0 then 0 else if (k::integer) < 0 then - 1 else 1)"
by simp
-lemma [code_abbrev]: "Numeral1 = (1\<Colon>code_numeral)"
- using one_code_numeral_code ..
+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 \<Rightarrow> integer \<Rightarrow> integer \<times> integer"
+where
+ "divmod_integer k l = (k div l, k mod l)"
+
+lemma fst_divmod [simp]:
+ "fst (divmod_integer k l) = k div l"
+ by (simp add: divmod_integer_def)
+
+lemma snd_divmod [simp]:
+ "snd (divmod_integer k l) = k mod l"
+ by (simp add: divmod_integer_def)
+
+definition divmod_abs :: "integer \<Rightarrow> integer \<Rightarrow> integer \<times> integer"
+where
+ "divmod_abs k l = (\<bar>k\<bar> div \<bar>l\<bar>, \<bar>k\<bar> mod \<bar>l\<bar>)"
+
+lemma fst_divmod_abs [simp]:
+ "fst (divmod_abs k l) = \<bar>k\<bar> div \<bar>l\<bar>"
+ by (simp add: divmod_abs_def)
+
+lemma snd_divmod_abs [simp]:
+ "snd (divmod_abs k l) = \<bar>k\<bar> mod \<bar>l\<bar>"
+ by (simp add: divmod_abs_def)
-lemma plus_code_numeral_code [code nbe]:
- "of_nat n + of_nat m = of_nat (n + m)"
- by simp
+lemma divmod_abs_terminate_code [code]:
+ "divmod_abs (Neg k) (Neg l) = divmod_abs (Pos k) (Pos l)"
+ "divmod_abs (Neg k) (Pos l) = divmod_abs (Pos k) (Pos l)"
+ "divmod_abs (Pos k) (Neg l) = divmod_abs (Pos k) (Pos l)"
+ "divmod_abs j 0 = (0, \<bar>j\<bar>)"
+ "divmod_abs 0 j = (0, 0)"
+ by (simp_all add: prod_eq_iff)
+
+lemma divmod_abs_rec_code [code]:
+ "divmod_abs (Pos k) (Pos l) =
+ (let j = sub k l in
+ if j < 0 then (0, Pos k)
+ else let (q, r) = divmod_abs j (Pos l) in (q + 1, r))"
+ apply (simp add: prod_eq_iff Let_def prod_case_beta)
+ apply transfer
+ apply (simp add: sub_non_negative sub_negative div_pos_pos_trivial mod_pos_pos_trivial div_pos_geq mod_pos_geq)
+ done
-lemma minus_code_numeral_code [code nbe]:
- "of_nat n - of_nat m = of_nat (n - m)"
+lemma divmod_integer_code [code]:
+ "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 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"
+ by (auto simp add: sgn_if)
+ 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
+ show ?thesis
+ by (simp add: prod_eq_iff integer_eq_iff prod_case_beta aux1)
+ (auto simp add: zdiv_zminus1_eq_if zmod_zminus1_eq_if div_minus_right mod_minus_right aux2)
+qed
+
+lemma div_integer_code [code]:
+ "k div l = fst (divmod_integer k l)"
by simp
-lemma times_code_numeral_code [code nbe]:
- "of_nat n * of_nat m = of_nat (n * m)"
- by simp
-
-lemma less_eq_code_numeral_code [code nbe]:
- "of_nat n \<le> of_nat m \<longleftrightarrow> n \<le> m"
- by simp
-
-lemma less_code_numeral_code [code nbe]:
- "of_nat n < of_nat m \<longleftrightarrow> n < m"
+lemma mod_integer_code [code]:
+ "k mod l = snd (divmod_integer k l)"
by simp
-lemma code_numeral_zero_minus_one:
- "(0::code_numeral) - 1 = 0"
- by simp
+lemma equal_integer_code [code]:
+ "HOL.equal 0 (0::integer) \<longleftrightarrow> True"
+ "HOL.equal 0 (Pos l) \<longleftrightarrow> False"
+ "HOL.equal 0 (Neg l) \<longleftrightarrow> False"
+ "HOL.equal (Pos k) 0 \<longleftrightarrow> False"
+ "HOL.equal (Pos k) (Pos l) \<longleftrightarrow> HOL.equal k l"
+ "HOL.equal (Pos k) (Neg l) \<longleftrightarrow> False"
+ "HOL.equal (Neg k) 0 \<longleftrightarrow> False"
+ "HOL.equal (Neg k) (Pos l) \<longleftrightarrow> False"
+ "HOL.equal (Neg k) (Neg l) \<longleftrightarrow> HOL.equal k l"
+ by (simp_all add: equal)
+
+lemma equal_integer_refl [code nbe]:
+ "HOL.equal (k::integer) k \<longleftrightarrow> True"
+ by (fact equal_refl)
-lemma Suc_code_numeral_minus_one:
- "Suc n - 1 = n"
- by simp
+lemma less_eq_integer_code [code]:
+ "0 \<le> (0::integer) \<longleftrightarrow> True"
+ "0 \<le> Pos l \<longleftrightarrow> True"
+ "0 \<le> Neg l \<longleftrightarrow> False"
+ "Pos k \<le> 0 \<longleftrightarrow> False"
+ "Pos k \<le> Pos l \<longleftrightarrow> k \<le> l"
+ "Pos k \<le> Neg l \<longleftrightarrow> False"
+ "Neg k \<le> 0 \<longleftrightarrow> True"
+ "Neg k \<le> Pos l \<longleftrightarrow> True"
+ "Neg k \<le> Neg l \<longleftrightarrow> l \<le> k"
+ by simp_all
+
+lemma less_integer_code [code]:
+ "0 < (0::integer) \<longleftrightarrow> False"
+ "0 < Pos l \<longleftrightarrow> True"
+ "0 < Neg l \<longleftrightarrow> False"
+ "Pos k < 0 \<longleftrightarrow> False"
+ "Pos k < Pos l \<longleftrightarrow> k < l"
+ "Pos k < Neg l \<longleftrightarrow> False"
+ "Neg k < 0 \<longleftrightarrow> True"
+ "Neg k < Pos l \<longleftrightarrow> True"
+ "Neg k < Neg l \<longleftrightarrow> l < k"
+ by simp_all
-lemma of_nat_code [code]:
- "of_nat = Nat.of_nat"
-proof
- fix n :: nat
- have "Nat.of_nat n = of_nat n"
- by (induct n) simp_all
- then show "of_nat n = Nat.of_nat n"
- by (rule sym)
+lift_definition integer_of_num :: "num \<Rightarrow> integer"
+ is "numeral :: num \<Rightarrow> int"
+ .
+
+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 (transfer, simp only: numeral.simps Let_def)+
+
+lift_definition num_of_integer :: "integer \<Rightarrow> num"
+ is "num_of_nat \<circ> nat"
+ .
+
+lemma num_of_integer_code [code]:
+ "num_of_integer k = (if k \<le> 1 then Num.One
+ else let
+ (l, j) = divmod_integer k 2;
+ l' = num_of_integer l;
+ l'' = l' + l'
+ in if j = 0 then l'' else l'' + Num.One)"
+proof -
+ {
+ assume "int_of_integer k mod 2 = 1"
+ then have "nat (int_of_integer k mod 2) = nat 1" by simp
+ moreover assume *: "1 < int_of_integer k"
+ ultimately have **: "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
+ then 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 + 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 prod_case_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 code_numeral_not_eq_zero: "i \<noteq> of_nat 0 \<longleftrightarrow> i \<ge> 1"
- by (cases i) auto
-
-definition nat_of_aux :: "code_numeral \<Rightarrow> nat \<Rightarrow> nat" where
- "nat_of_aux i n = nat_of i + n"
-
-lemma nat_of_aux_code [code]:
- "nat_of_aux i n = (if i = 0 then n else nat_of_aux (i - 1) (Nat.Suc n))"
- by (auto simp add: nat_of_aux_def code_numeral_not_eq_zero)
-
-lemma nat_of_code [code]:
- "nat_of i = nat_of_aux i 0"
- by (simp add: nat_of_aux_def)
-
-definition div_mod :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<times> code_numeral" where
- [code del]: "div_mod n m = (n div m, n mod m)"
-
-lemma [code]:
- "div_mod n m = (if m = 0 then (0, n) else (n div m, n mod m))"
- unfolding div_mod_def by auto
-
-lemma [code]:
- "n div m = fst (div_mod n m)"
- unfolding div_mod_def by simp
-
-lemma [code]:
- "n mod m = snd (div_mod n m)"
- unfolding div_mod_def by simp
-
-definition int_of :: "code_numeral \<Rightarrow> int" where
- "int_of = Nat.of_nat o nat_of"
-
-lemma int_of_code [code]:
- "int_of k = (if k = 0 then 0
- else (if k mod 2 = 0 then 2 * int_of (k div 2) else 2 * int_of (k div 2) + 1))"
+lemma nat_of_integer_code [code]:
+ "nat_of_integer k = (if k \<le> 0 then 0
+ else let
+ (l, j) = divmod_integer k 2;
+ l' = nat_of_integer l;
+ l'' = l' + l'
+ in if j = 0 then l'' else l'' + 1)"
proof -
- have "(nat_of k div 2) * 2 + nat_of k mod 2 = nat_of k"
- by (rule mod_div_equality)
- then have "int ((nat_of k div 2) * 2 + nat_of k mod 2) = int (nat_of k)"
- by simp
- then have "int (nat_of k) = int (nat_of k div 2) * 2 + int (nat_of k mod 2)"
- unfolding of_nat_mult of_nat_add by simp
- then show ?thesis by (auto simp add: int_of_def mult_ac)
+ obtain j where "k = integer_of_int j"
+ proof
+ show "k = integer_of_int (int_of_integer k)" by simp
+ qed
+ moreover have "2 * (j div 2) = j - j mod 2"
+ by (simp add: zmult_div_cancel mult_commute)
+ ultimately show ?thesis
+ by (auto simp add: split_def Let_def mod_integer_def nat_of_integer_def not_le
+ nat_add_distrib [symmetric] Suc_nat_eq_nat_zadd1)
+ (auto simp add: mult_2 [symmetric])
qed
+lemma int_of_integer_code [code]:
+ "int_of_integer k = (if k < 0 then - (int_of_integer (- k))
+ else if k = 0 then 0
+ else let
+ (l, j) = divmod_integer k 2;
+ l' = 2 * int_of_integer l
+ in if j = 0 then l' else l' + 1)"
+ by (auto simp add: split_def Let_def integer_eq_iff zmult_div_cancel)
-hide_const (open) of_nat nat_of Suc int_of
+lemma integer_of_int_code [code]:
+ "integer_of_int k = (if k < 0 then - (integer_of_int (- k))
+ else if k = 0 then 0
+ else let
+ (l, j) = divmod_int k 2;
+ l' = 2 * integer_of_int l
+ in if j = 0 then l' else l' + 1)"
+ by (auto simp add: split_def Let_def integer_eq_iff zmult_div_cancel)
+
+hide_const (open) Pos Neg sub dup divmod_abs
-subsection {* Code generator setup *}
+subsection {* Serializer setup for target language integers *}
-text {* Implementation of code numerals by bounded integers *}
+code_reserved Eval int Integer abs
-code_type code_numeral
- (SML "int")
+code_type integer
+ (SML "IntInf.int")
(OCaml "Big'_int.big'_int")
(Haskell "Integer")
(Scala "BigInt")
+ (Eval "int")
-code_instance code_numeral :: equal
+code_instance integer :: equal
(Haskell -)
-setup {*
- Numeral.add_code @{const_name Num}
- false Code_Printer.literal_naive_numeral "SML"
- #> fold (Numeral.add_code @{const_name Num}
- false Code_Printer.literal_numeral) ["OCaml", "Haskell", "Scala"]
-*}
-
-code_reserved SML Int int
-code_reserved Eval Integer
-
-code_const "0::code_numeral"
+code_const "0::integer"
(SML "0")
(OCaml "Big'_int.zero'_big'_int")
(Haskell "0")
(Scala "BigInt(0)")
-code_const "plus \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
- (SML "Int.+/ ((_),/ (_))")
+setup {*
+ fold (Numeral.add_code @{const_name Code_Numeral.Pos}
+ false Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"]
+*}
+
+setup {*
+ fold (Numeral.add_code @{const_name Code_Numeral.Neg}
+ true Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"]
+*}
+
+code_const "plus :: integer \<Rightarrow> _ \<Rightarrow> _"
+ (SML "IntInf.+ ((_), (_))")
(OCaml "Big'_int.add'_big'_int")
(Haskell infixl 6 "+")
(Scala infixl 7 "+")
(Eval infixl 8 "+")
-code_const "minus \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
- (SML "Int.max/ (0 : int,/ Int.-/ ((_),/ (_)))")
- (OCaml "Big'_int.max'_big'_int/ Big'_int.zero'_big'_int/ (Big'_int.sub'_big'_int/ _/ _)")
- (Haskell "Prelude.max/ (0 :: Integer)/ (_/ -/ _)")
- (Scala "!(_/ -/ _).max(0)")
- (Eval "Integer.max/ 0/ (_/ -/ _)")
+code_const "uminus :: integer \<Rightarrow> _"
+ (SML "IntInf.~")
+ (OCaml "Big'_int.minus'_big'_int")
+ (Haskell "negate")
+ (Scala "!(- _)")
+ (Eval "~/ _")
+
+code_const "minus :: integer \<Rightarrow> _"
+ (SML "IntInf.- ((_), (_))")
+ (OCaml "Big'_int.sub'_big'_int")
+ (Haskell infixl 6 "-")
+ (Scala infixl 7 "-")
+ (Eval infixl 8 "-")
-code_const "times \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
- (SML "Int.*/ ((_),/ (_))")
+code_const Code_Numeral.dup
+ (SML "IntInf.*/ (2,/ (_))")
+ (OCaml "Big'_int.mult'_big'_int/ (Big'_int.big'_int'_of'_int/ 2)")
+ (Haskell "!(2 * _)")
+ (Scala "!(2 * _)")
+ (Eval "!(2 * _)")
+
+code_const Code_Numeral.sub
+ (SML "!(raise/ Fail/ \"sub\")")
+ (OCaml "failwith/ \"sub\"")
+ (Haskell "error/ \"sub\"")
+ (Scala "!sys.error(\"sub\")")
+
+code_const "times :: integer \<Rightarrow> _ \<Rightarrow> _"
+ (SML "IntInf.* ((_), (_))")
(OCaml "Big'_int.mult'_big'_int")
(Haskell infixl 7 "*")
(Scala infixl 8 "*")
- (Eval infixl 8 "*")
+ (Eval infixl 9 "*")
-code_const Code_Numeral.div_mod
- (SML "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (Int.div (n, m), Int.mod (n, m)))")
+code_const Code_Numeral.divmod_abs
+ (SML "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)")
(OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)")
- (Haskell "divMod")
+ (Haskell "divMod/ (abs _)/ (abs _)")
(Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
- (Eval "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (Integer.div'_mod n m))")
+ (Eval "Integer.div'_mod/ (abs _)/ (abs _)")
-code_const "HOL.equal \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
- (SML "!((_ : Int.int) = _)")
+code_const "HOL.equal :: integer \<Rightarrow> _ \<Rightarrow> bool"
+ (SML "!((_ : IntInf.int) = _)")
(OCaml "Big'_int.eq'_big'_int")
(Haskell infix 4 "==")
(Scala infixl 5 "==")
- (Eval "!((_ : int) = _)")
+ (Eval infixl 6 "=")
-code_const "less_eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
- (SML "Int.<=/ ((_),/ (_))")
+code_const "less_eq :: integer \<Rightarrow> _ \<Rightarrow> bool"
+ (SML "IntInf.<= ((_), (_))")
(OCaml "Big'_int.le'_big'_int")
(Haskell infix 4 "<=")
(Scala infixl 4 "<=")
(Eval infixl 6 "<=")
-code_const "less \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
- (SML "Int.</ ((_),/ (_))")
+code_const "less :: integer \<Rightarrow> _ \<Rightarrow> bool"
+ (SML "IntInf.< ((_), (_))")
(OCaml "Big'_int.lt'_big'_int")
(Haskell infix 4 "<")
(Scala infixl 4 "<")
@@ -346,5 +623,321 @@
code_modulename Haskell
Code_Numeral Arith
+
+subsection {* Type of target language naturals *}
+
+typedef natural = "UNIV \<Colon> nat set"
+ morphisms nat_of_natural natural_of_nat ..
+
+setup_lifting (no_code) type_definition_natural
+
+lemma natural_eq_iff [termination_simp]:
+ "m = n \<longleftrightarrow> nat_of_natural m = nat_of_natural n"
+ by transfer rule
+
+lemma natural_eqI:
+ "nat_of_natural m = nat_of_natural n \<Longrightarrow> m = n"
+ using natural_eq_iff [of m n] by simp
+
+lemma nat_of_natural_of_nat_inverse [simp]:
+ "nat_of_natural (natural_of_nat n) = n"
+ by transfer rule
+
+lemma natural_of_nat_of_natural_inverse [simp]:
+ "natural_of_nat (nat_of_natural n) = n"
+ by transfer rule
+
+instantiation natural :: "{comm_monoid_diff, semiring_1}"
+begin
+
+lift_definition zero_natural :: natural
+ is "0 :: nat"
+ .
+
+declare zero_natural.rep_eq [simp]
+
+lift_definition one_natural :: natural
+ is "1 :: nat"
+ .
+
+declare one_natural.rep_eq [simp]
+
+lift_definition plus_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
+ is "plus :: nat \<Rightarrow> nat \<Rightarrow> nat"
+ .
+
+declare plus_natural.rep_eq [simp]
+
+lift_definition minus_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
+ is "minus :: nat \<Rightarrow> nat \<Rightarrow> nat"
+ .
+
+declare minus_natural.rep_eq [simp]
+
+lift_definition times_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
+ is "times :: nat \<Rightarrow> nat \<Rightarrow> nat"
+ .
+
+declare times_natural.rep_eq [simp]
+
+instance proof
+qed (transfer, simp add: algebra_simps)+
+
+end
+
+lemma [transfer_rule]:
+ "fun_rel HOL.eq cr_natural (\<lambda>n::nat. n) (of_nat :: nat \<Rightarrow> natural)"
+proof -
+ have "fun_rel HOL.eq cr_natural (of_nat :: nat \<Rightarrow> nat) (of_nat :: nat \<Rightarrow> natural)"
+ by (unfold of_nat_def [abs_def]) transfer_prover
+ then show ?thesis by (simp add: id_def)
+qed
+
+lemma [transfer_rule]:
+ "fun_rel HOL.eq cr_natural (numeral :: num \<Rightarrow> nat) (numeral :: num \<Rightarrow> natural)"
+proof -
+ have "fun_rel HOL.eq cr_natural (numeral :: num \<Rightarrow> nat) (\<lambda>n. of_nat (numeral n))"
+ by transfer_prover
+ then show ?thesis by simp
+qed
+
+lemma nat_of_natural_of_nat [simp]:
+ "nat_of_natural (of_nat n) = n"
+ by transfer rule
+
+lemma natural_of_nat_of_nat [simp, code_abbrev]:
+ "natural_of_nat = of_nat"
+ by transfer rule
+
+lemma of_nat_of_natural [simp]:
+ "of_nat (nat_of_natural n) = n"
+ by transfer rule
+
+lemma nat_of_natural_numeral [simp]:
+ "nat_of_natural (numeral k) = numeral k"
+ by transfer rule
+
+instantiation natural :: "{semiring_div, equal, linordered_semiring}"
+begin
+
+lift_definition div_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
+ is "Divides.div :: nat \<Rightarrow> nat \<Rightarrow> nat"
+ .
+
+declare div_natural.rep_eq [simp]
+
+lift_definition mod_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
+ is "Divides.mod :: nat \<Rightarrow> nat \<Rightarrow> nat"
+ .
+
+declare mod_natural.rep_eq [simp]
+
+lift_definition less_eq_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool"
+ is "less_eq :: nat \<Rightarrow> nat \<Rightarrow> bool"
+ .
+
+declare less_eq_natural.rep_eq [termination_simp]
+
+lift_definition less_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool"
+ is "less :: nat \<Rightarrow> nat \<Rightarrow> bool"
+ .
+
+declare less_natural.rep_eq [termination_simp]
+
+lift_definition equal_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool"
+ is "HOL.equal :: nat \<Rightarrow> nat \<Rightarrow> bool"
+ .
+
+instance proof
+qed (transfer, simp add: algebra_simps equal less_le_not_le [symmetric] linear)+
+
end
+lemma [transfer_rule]:
+ "fun_rel cr_natural (fun_rel cr_natural cr_natural) (min :: _ \<Rightarrow> _ \<Rightarrow> nat) (min :: _ \<Rightarrow> _ \<Rightarrow> natural)"
+ by (unfold min_def [abs_def]) transfer_prover
+
+lemma [transfer_rule]:
+ "fun_rel cr_natural (fun_rel cr_natural cr_natural) (max :: _ \<Rightarrow> _ \<Rightarrow> nat) (max :: _ \<Rightarrow> _ \<Rightarrow> natural)"
+ by (unfold max_def [abs_def]) transfer_prover
+
+lemma nat_of_natural_min [simp]:
+ "nat_of_natural (min k l) = min (nat_of_natural k) (nat_of_natural l)"
+ by transfer rule
+
+lemma nat_of_natural_max [simp]:
+ "nat_of_natural (max k l) = max (nat_of_natural k) (nat_of_natural l)"
+ by transfer rule
+
+lift_definition natural_of_integer :: "integer \<Rightarrow> natural"
+ is "nat :: int \<Rightarrow> nat"
+ .
+
+lift_definition integer_of_natural :: "natural \<Rightarrow> integer"
+ is "of_nat :: nat \<Rightarrow> int"
+ .
+
+lemma natural_of_integer_of_natural [simp]:
+ "natural_of_integer (integer_of_natural n) = n"
+ by transfer simp
+
+lemma integer_of_natural_of_integer [simp]:
+ "integer_of_natural (natural_of_integer k) = max 0 k"
+ by transfer auto
+
+lemma int_of_integer_of_natural [simp]:
+ "int_of_integer (integer_of_natural n) = of_nat (nat_of_natural n)"
+ by transfer rule
+
+lemma integer_of_natural_of_nat [simp]:
+ "integer_of_natural (of_nat n) = of_nat n"
+ by transfer rule
+
+lemma [measure_function]:
+ "is_measure nat_of_natural"
+ by (rule is_measure_trivial)
+
+
+subsection {* Inductive represenation of target language naturals *}
+
+lift_definition Suc :: "natural \<Rightarrow> natural"
+ is Nat.Suc
+ .
+
+declare Suc.rep_eq [simp]
+
+rep_datatype "0::natural" Suc
+ by (transfer, fact nat.induct nat.inject nat.distinct)+
+
+lemma natural_case [case_names nat, cases type: natural]:
+ fixes m :: natural
+ assumes "\<And>n. m = of_nat n \<Longrightarrow> P"
+ shows P
+ using assms by transfer blast
+
+lemma [simp, code]:
+ "natural_size = nat_of_natural"
+proof (rule ext)
+ fix n
+ show "natural_size n = nat_of_natural n"
+ by (induct n) simp_all
+qed
+
+lemma [simp, code]:
+ "size = nat_of_natural"
+proof (rule ext)
+ fix n
+ show "size n = nat_of_natural n"
+ by (induct n) simp_all
+qed
+
+lemma natural_decr [termination_simp]:
+ "n \<noteq> 0 \<Longrightarrow> nat_of_natural n - Nat.Suc 0 < nat_of_natural n"
+ by transfer simp
+
+lemma natural_zero_minus_one:
+ "(0::natural) - 1 = 0"
+ by simp
+
+lemma Suc_natural_minus_one:
+ "Suc n - 1 = n"
+ by transfer simp
+
+hide_const (open) Suc
+
+
+subsection {* Code refinement for target language naturals *}
+
+lift_definition Nat :: "integer \<Rightarrow> natural"
+ is nat
+ .
+
+lemma [code_post]:
+ "Nat 0 = 0"
+ "Nat 1 = 1"
+ "Nat (numeral k) = numeral k"
+ by (transfer, simp)+
+
+lemma [code abstype]:
+ "Nat (integer_of_natural n) = n"
+ by transfer simp
+
+lemma [code abstract]:
+ "integer_of_natural (natural_of_nat n) = of_nat n"
+ by simp
+
+lemma [code abstract]:
+ "integer_of_natural (natural_of_integer k) = max 0 k"
+ by simp
+
+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 \<circ> integer_of_natural"
+ by transfer (simp add: fun_eq_iff)
+
+lemma [code, code_unfold]:
+ "natural_case 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.recs [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 add: of_nat_mult)
+
+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]:
+ "HOL.equal m n \<longleftrightarrow> HOL.equal (integer_of_natural m) (integer_of_natural n)"
+ by transfer (simp add: equal)
+
+lemma [code nbe]:
+ "HOL.equal n (n::natural) \<longleftrightarrow> True"
+ by (simp add: equal)
+
+lemma [code]:
+ "m \<le> n \<longleftrightarrow> integer_of_natural m \<le> integer_of_natural n"
+ by transfer simp
+
+lemma [code]:
+ "m < n \<longleftrightarrow> integer_of_natural m < integer_of_natural n"
+ by transfer simp
+
+hide_const (open) Nat
+
+
+code_reflect Code_Numeral
+ datatypes natural = _
+ functions integer_of_natural natural_of_integer
+
+end
+