improved code equations taken over from AFP
authorhaftmann
Fri Mar 22 19:18:08 2019 +0000 (3 months ago)
changeset 69946494934c30f38
parent 69945 35ba13ac6e5c
child 69947 77a92e8d5167
improved code equations taken over from AFP
src/HOL/Code_Numeral.thy
src/HOL/Library/Code_Target_Nat.thy
     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.33    by (simp_all add: prod_eq_iff)
    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.57 +lemma divmod_integer_code [code]: \<^marker>\<open>contributor \<open>René Thiemann\<close>\<close> \<^marker>\<open>contributor \<open>Akihisa Yamada\<close>\<close>
    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  
    1.79 +export_code divmod_integer in Haskell
    1.80 +
    1.81  
    1.82  subsection \<open>Type of target language naturals\<close>
    1.83  
     2.1 --- a/src/HOL/Library/Code_Target_Nat.thy	Fri Mar 22 12:34:49 2019 +0000
     2.2 +++ b/src/HOL/Library/Code_Target_Nat.thy	Fri Mar 22 19:18:08 2019 +0000
     2.3 @@ -93,14 +93,26 @@
     2.4    "integer_of_nat (m mod n) = of_nat m mod of_nat n"
     2.5    by transfer (simp add: zmod_int)
     2.6  
     2.7 -lemma [code]:
     2.8 -  "Divides.divmod_nat m n = (m div n, m mod n)"
     2.9 -  by (fact divmod_nat_def)
    2.10 +context
    2.11 +  includes integer.lifting
    2.12 +begin
    2.13 +
    2.14 +lemma divmod_nat_code [code]: \<^marker>\<open>contributor \<open>René Thiemann\<close>\<close> \<^marker>\<open>contributor \<open>Akihisa Yamada\<close>\<close>
    2.15 +  "Divides.divmod_nat m n = (
    2.16 +     let k = integer_of_nat m; l = integer_of_nat n
    2.17 +     in map_prod nat_of_integer nat_of_integer
    2.18 +       (if k = 0 then (0, 0)
    2.19 +        else if l = 0 then (0, k) else
    2.20 +          Code_Numeral.divmod_abs k l))"
    2.21 +  by (simp add: prod_eq_iff Let_def; transfer)
    2.22 +    (simp add: nat_div_distrib nat_mod_distrib)
    2.23 +
    2.24 +end
    2.25  
    2.26  lemma [code]:
    2.27    "divmod m n = map_prod nat_of_integer nat_of_integer (divmod m n)"
    2.28 -  by (simp only: prod_eq_iff divmod_def map_prod_def case_prod_beta fst_conv snd_conv)
    2.29 -    (transfer, simp_all only: nat_div_distrib nat_mod_distrib
    2.30 +  by (simp only: prod_eq_iff divmod_def map_prod_def case_prod_beta fst_conv snd_conv; transfer)
    2.31 +    (simp_all only: nat_div_distrib nat_mod_distrib
    2.32          zero_le_numeral nat_numeral)
    2.33    
    2.34  lemma [code]: