src/HOL/Code_Numeral.thy
 changeset 69946 494934c30f38 parent 69906 55534affe445 child 70009 435fb018e8ee
```     1.1 --- a/src/HOL/Code_Numeral.thy	Fri Mar 22 12:34:49 2019 +0000
1.2 +++ b/src/HOL/Code_Numeral.thy	Fri Mar 22 19:18:08 2019 +0000
1.3 @@ -190,11 +190,18 @@
1.4    is "less_eq :: int \<Rightarrow> int \<Rightarrow> bool"
1.5    .
1.6
1.7 +lemma integer_less_eq_iff:
1.8 +  "k \<le> l \<longleftrightarrow> int_of_integer k \<le> int_of_integer l"
1.9 +  by (fact less_eq_integer.rep_eq)
1.10
1.11  lift_definition less_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
1.12    is "less :: int \<Rightarrow> int \<Rightarrow> bool"
1.13    .
1.14
1.15 +lemma integer_less_iff:
1.16 +  "k < l \<longleftrightarrow> int_of_integer k < int_of_integer l"
1.17 +  by (fact less_integer.rep_eq)
1.18 +
1.19  lift_definition equal_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
1.20    is "HOL.equal :: int \<Rightarrow> int \<Rightarrow> bool"
1.21    .
1.22 @@ -320,7 +327,7 @@
1.23  end
1.24
1.25  declare divmod_algorithm_code [where ?'a = integer,
1.26 -  folded integer_of_num_def, unfolded integer_of_num_triv,
1.27 +  folded integer_of_num_def, unfolded integer_of_num_triv,
1.28    code]
1.29
1.30  lemma integer_of_nat_0: "integer_of_nat 0 = 0"
1.31 @@ -492,7 +499,7 @@
1.32    "divmod_abs 0 j = (0, 0)"
1.34
1.35 -lemma divmod_integer_code [code]:
1.36 +lemma divmod_integer_eq_cases:
1.37    "divmod_integer k l =
1.38      (if k = 0 then (0, 0) else if l = 0 then (0, k) else
1.39      (apsnd \<circ> times \<circ> sgn) l (if sgn k = sgn l
1.40 @@ -500,14 +507,30 @@
1.41        else (let (r, s) = divmod_abs k l in
1.42          if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"
1.43  proof -
1.44 -  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"
1.45 +  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
1.46      by (auto simp add: sgn_if)
1.47 -  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
1.48 +  have **: "- k = l * q \<longleftrightarrow> k = - (l * q)" for k l q :: int
1.49 +    by auto
1.50    show ?thesis
1.51 -    by (simp add: prod_eq_iff integer_eq_iff case_prod_beta aux1)
1.52 -      (auto simp add: zdiv_zminus1_eq_if zmod_zminus1_eq_if div_minus_right mod_minus_right aux2)
1.53 +    by (simp add: divmod_integer_def divmod_abs_def)
1.54 +      (transfer, auto simp add: * ** not_less zdiv_zminus1_eq_if zmod_zminus1_eq_if div_minus_right mod_minus_right)
1.55  qed
1.56
1.58 +  "divmod_integer k l =
1.59 +   (if k = 0 then (0, 0)
1.60 +    else if l > 0 then
1.61 +            (if k > 0 then Code_Numeral.divmod_abs k l
1.62 +             else case Code_Numeral.divmod_abs k l of (r, s) \<Rightarrow>
1.63 +                  if s = 0 then (- r, 0) else (- r - 1, l - s))
1.64 +    else if l = 0 then (0, k)
1.65 +    else apsnd uminus
1.66 +            (if k < 0 then Code_Numeral.divmod_abs k l
1.67 +             else case Code_Numeral.divmod_abs k l of (r, s) \<Rightarrow>
1.68 +                  if s = 0 then (- r, 0) else (- r - 1, - l - s)))"
1.69 +  by (cases l "0 :: integer" rule: linorder_cases)
1.70 +    (auto split: prod.splits simp add: divmod_integer_eq_cases)
1.71 +
1.72  lemma div_integer_code [code]:
1.73    "k div l = fst (divmod_integer k l)"
1.74    by simp
1.75 @@ -743,6 +766,8 @@
1.76  code_identifier
1.77    code_module Code_Numeral \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
1.78