src/HOL/Code_Numeral.thy
changeset 61275 053ec04ea866
parent 61274 0261eec37233
child 61857 542f2c6da692
     1.1 --- a/src/HOL/Code_Numeral.thy	Sun Sep 27 10:11:14 2015 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Sun Sep 27 10:11:15 2015 +0200
     1.3 @@ -147,6 +147,25 @@
     1.4    "int_of_integer (Num.sub k l) = Num.sub k l"
     1.5    by transfer rule
     1.6  
     1.7 +lift_definition integer_of_num :: "num \<Rightarrow> integer"
     1.8 +  is "numeral :: num \<Rightarrow> int"
     1.9 +  .
    1.10 +
    1.11 +lemma integer_of_num [code]:
    1.12 +  "integer_of_num num.One = 1"
    1.13 +  "integer_of_num (num.Bit0 n) = (let k = integer_of_num n in k + k)"
    1.14 +  "integer_of_num (num.Bit1 n) = (let k = integer_of_num n in k + k + 1)"
    1.15 +  by (transfer, simp only: numeral.simps Let_def)+
    1.16 +
    1.17 +lemma numeral_unfold_integer_of_num:
    1.18 +  "numeral = integer_of_num"
    1.19 +  by (simp add: integer_of_num_def map_fun_def fun_eq_iff)
    1.20 +
    1.21 +lemma integer_of_num_triv:
    1.22 +  "integer_of_num Num.One = 1"
    1.23 +  "integer_of_num (Num.Bit0 Num.One) = 2"
    1.24 +  by (transfer, simp)+
    1.25 +
    1.26  instantiation integer :: "{ring_div, equal, linordered_idom}"
    1.27  begin
    1.28  
    1.29 @@ -215,18 +234,43 @@
    1.30    "of_nat (nat_of_integer k) = max 0 k"
    1.31    by transfer auto
    1.32  
    1.33 -instance integer :: semiring_numeral_div
    1.34 -  by intro_classes (transfer,
    1.35 -    fact le_add_diff_inverse2
    1.36 -    semiring_numeral_div_class.div_less
    1.37 -    semiring_numeral_div_class.mod_less
    1.38 -    semiring_numeral_div_class.div_positive
    1.39 -    semiring_numeral_div_class.mod_less_eq_dividend
    1.40 -    semiring_numeral_div_class.pos_mod_bound
    1.41 -    semiring_numeral_div_class.pos_mod_sign
    1.42 -    semiring_numeral_div_class.mod_mult2_eq
    1.43 -    semiring_numeral_div_class.div_mult2_eq
    1.44 -    semiring_numeral_div_class.discrete)+
    1.45 +instantiation integer :: semiring_numeral_div
    1.46 +begin
    1.47 +
    1.48 +definition divmod_integer :: "num \<Rightarrow> num \<Rightarrow> integer \<times> integer"
    1.49 +where
    1.50 +  divmod_integer'_def: "divmod_integer m n = (numeral m div numeral n, numeral m mod numeral n)"
    1.51 +
    1.52 +definition divmod_step_integer :: "num \<Rightarrow> integer \<times> integer \<Rightarrow> integer \<times> integer"
    1.53 +where
    1.54 +  "divmod_step_integer l qr = (let (q, r) = qr
    1.55 +    in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
    1.56 +    else (2 * q, r))"
    1.57 +
    1.58 +instance proof
    1.59 +  show "divmod m n = (numeral m div numeral n :: integer, numeral m mod numeral n)"
    1.60 +    for m n by (fact divmod_integer'_def)
    1.61 +  show "divmod_step l qr = (let (q, r) = qr
    1.62 +    in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
    1.63 +    else (2 * q, r))" for l and qr :: "integer \<times> integer"
    1.64 +    by (fact divmod_step_integer_def)
    1.65 +qed (transfer,
    1.66 +  fact le_add_diff_inverse2
    1.67 +  semiring_numeral_div_class.div_less
    1.68 +  semiring_numeral_div_class.mod_less
    1.69 +  semiring_numeral_div_class.div_positive
    1.70 +  semiring_numeral_div_class.mod_less_eq_dividend
    1.71 +  semiring_numeral_div_class.pos_mod_bound
    1.72 +  semiring_numeral_div_class.pos_mod_sign
    1.73 +  semiring_numeral_div_class.mod_mult2_eq
    1.74 +  semiring_numeral_div_class.div_mult2_eq
    1.75 +  semiring_numeral_div_class.discrete)+
    1.76 +
    1.77 +end
    1.78 +
    1.79 +declare divmod_algorithm_code [where ?'a = integer,
    1.80 +  unfolded numeral_unfold_integer_of_num, unfolded integer_of_num_triv, 
    1.81 +  code]
    1.82  
    1.83  lemma integer_of_nat_0: "integer_of_nat 0 = 0"
    1.84  by transfer simp
    1.85 @@ -440,16 +484,6 @@
    1.86    "Neg k < Neg l \<longleftrightarrow> l < k"
    1.87    by simp_all
    1.88  
    1.89 -lift_definition integer_of_num :: "num \<Rightarrow> integer"
    1.90 -  is "numeral :: num \<Rightarrow> int"
    1.91 -  .
    1.92 -
    1.93 -lemma integer_of_num [code]:
    1.94 -  "integer_of_num num.One = 1"
    1.95 -  "integer_of_num (num.Bit0 n) = (let k = integer_of_num n in k + k)"
    1.96 -  "integer_of_num (num.Bit1 n) = (let k = integer_of_num n in k + k + 1)"
    1.97 -  by (transfer, simp only: numeral.simps Let_def)+
    1.98 -
    1.99  lift_definition num_of_integer :: "integer \<Rightarrow> num"
   1.100    is "num_of_nat \<circ> nat"
   1.101    .