author haftmann Fri, 22 Mar 2019 19:18:08 +0000 changeset 69946 494934c30f38 parent 69945 35ba13ac6e5c child 69947 77a92e8d5167
improved code equations taken over from AFP
 src/HOL/Code_Numeral.thy file | annotate | diff | comparison | revisions src/HOL/Library/Code_Target_Nat.thy file | annotate | diff | comparison | revisions
--- a/src/HOL/Code_Numeral.thy	Fri Mar 22 12:34:49 2019 +0000
+++ b/src/HOL/Code_Numeral.thy	Fri Mar 22 19:18:08 2019 +0000
@@ -190,11 +190,18 @@
is "less_eq :: int \<Rightarrow> int \<Rightarrow> bool"
.

+lemma integer_less_eq_iff:
+  "k \<le> l \<longleftrightarrow> int_of_integer k \<le> int_of_integer l"
+  by (fact less_eq_integer.rep_eq)

lift_definition less_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
is "less :: int \<Rightarrow> int \<Rightarrow> bool"
.

+lemma integer_less_iff:
+  "k < l \<longleftrightarrow> int_of_integer k < int_of_integer l"
+  by (fact less_integer.rep_eq)
+
lift_definition equal_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
is "HOL.equal :: int \<Rightarrow> int \<Rightarrow> bool"
.
@@ -320,7 +327,7 @@
end

declare divmod_algorithm_code [where ?'a = integer,
-  folded integer_of_num_def, unfolded integer_of_num_triv,
+  folded integer_of_num_def, unfolded integer_of_num_triv,
code]

lemma integer_of_nat_0: "integer_of_nat 0 = 0"
@@ -492,7 +499,7 @@
"divmod_abs 0 j = (0, 0)"

-lemma divmod_integer_code [code]:
+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
@@ -500,14 +507,30 @@
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"
+  have *: "sgn k = sgn l \<longleftrightarrow> k = 0 \<and> l = 0 \<or> 0 < l \<and> 0 < k \<or> l < 0 \<and> k < 0" for k l :: int
-  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
+  have **: "- k = l * q \<longleftrightarrow> k = - (l * q)" for k l q :: int
+    by auto
show ?thesis
-    by (simp add: prod_eq_iff integer_eq_iff case_prod_beta aux1)
-      (auto simp add: zdiv_zminus1_eq_if zmod_zminus1_eq_if div_minus_right mod_minus_right aux2)
+    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

+  "divmod_integer k l =
+   (if k = 0 then (0, 0)
+    else if l > 0 then
+            (if k > 0 then Code_Numeral.divmod_abs k l
+             else case Code_Numeral.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 Code_Numeral.divmod_abs k l
+             else case Code_Numeral.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
@@ -743,6 +766,8 @@
code_identifier
code_module Code_Numeral \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith

+

subsection \<open>Type of target language naturals\<close>

--- a/src/HOL/Library/Code_Target_Nat.thy	Fri Mar 22 12:34:49 2019 +0000
+++ b/src/HOL/Library/Code_Target_Nat.thy	Fri Mar 22 19:18:08 2019 +0000
@@ -93,14 +93,26 @@
"integer_of_nat (m mod n) = of_nat m mod of_nat n"

-lemma [code]:
-  "Divides.divmod_nat m n = (m div n, m mod n)"
-  by (fact divmod_nat_def)
+context
+  includes integer.lifting
+begin
+
+  "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)