src/HOL/Code_Numeral.thy
changeset 64592 7759f1766189
parent 64246 15d1ee6e847b
child 64848 c50db2128048
     1.1 --- a/src/HOL/Code_Numeral.thy	Sat Dec 17 15:22:13 2016 +0100
     1.2 +++ b/src/HOL/Code_Numeral.thy	Sat Dec 17 15:22:14 2016 +0100
     1.3 @@ -168,21 +168,9 @@
     1.4    "integer_of_num (Num.Bit0 Num.One) = 2"
     1.5    by (transfer, simp)+
     1.6  
     1.7 -instantiation integer :: "{ring_div, equal, linordered_idom}"
     1.8 +instantiation integer :: "{linordered_idom, equal}"
     1.9  begin
    1.10  
    1.11 -lift_definition divide_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
    1.12 -  is "divide :: int \<Rightarrow> int \<Rightarrow> int"
    1.13 -  .
    1.14 -
    1.15 -declare divide_integer.rep_eq [simp]
    1.16 -
    1.17 -lift_definition modulo_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
    1.18 -  is "modulo :: int \<Rightarrow> int \<Rightarrow> int"
    1.19 -  .
    1.20 -
    1.21 -declare modulo_integer.rep_eq [simp]
    1.22 -
    1.23  lift_definition abs_integer :: "integer \<Rightarrow> integer"
    1.24    is "abs :: int \<Rightarrow> int"
    1.25    .
    1.26 @@ -199,6 +187,7 @@
    1.27    is "less_eq :: int \<Rightarrow> int \<Rightarrow> bool"
    1.28    .
    1.29  
    1.30 +
    1.31  lift_definition less_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
    1.32    is "less :: int \<Rightarrow> int \<Rightarrow> bool"
    1.33    .
    1.34 @@ -207,8 +196,8 @@
    1.35    is "HOL.equal :: int \<Rightarrow> int \<Rightarrow> bool"
    1.36    .
    1.37  
    1.38 -instance proof
    1.39 -qed (transfer, simp add: algebra_simps equal less_le_not_le [symmetric] mult_strict_right_mono linear)+
    1.40 +instance
    1.41 +  by standard (transfer, simp add: algebra_simps equal less_le_not_le [symmetric] mult_strict_right_mono linear)+
    1.42  
    1.43  end
    1.44  
    1.45 @@ -236,6 +225,38 @@
    1.46    "of_nat (nat_of_integer k) = max 0 k"
    1.47    by transfer auto
    1.48  
    1.49 +instantiation integer :: "{ring_div, normalization_semidom}"
    1.50 +begin
    1.51 +
    1.52 +lift_definition normalize_integer :: "integer \<Rightarrow> integer"
    1.53 +  is "normalize :: int \<Rightarrow> int"
    1.54 +  .
    1.55 +
    1.56 +declare normalize_integer.rep_eq [simp]
    1.57 +
    1.58 +lift_definition unit_factor_integer :: "integer \<Rightarrow> integer"
    1.59 +  is "unit_factor :: int \<Rightarrow> int"
    1.60 +  .
    1.61 +
    1.62 +declare unit_factor_integer.rep_eq [simp]
    1.63 +
    1.64 +lift_definition divide_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
    1.65 +  is "divide :: int \<Rightarrow> int \<Rightarrow> int"
    1.66 +  .
    1.67 +
    1.68 +declare divide_integer.rep_eq [simp]
    1.69 +
    1.70 +lift_definition modulo_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
    1.71 +  is "modulo :: int \<Rightarrow> int \<Rightarrow> int"
    1.72 +  .
    1.73 +
    1.74 +declare modulo_integer.rep_eq [simp]
    1.75 +
    1.76 +instance
    1.77 +  by standard (transfer, simp add: mult_sgn_abs sgn_mult)+
    1.78 +
    1.79 +end
    1.80 +
    1.81  instantiation integer :: semiring_numeral_div
    1.82  begin
    1.83  
    1.84 @@ -389,6 +410,14 @@
    1.85    "Neg m * Neg n = Pos (m * n)"
    1.86    by simp_all
    1.87  
    1.88 +lemma normalize_integer_code [code]:
    1.89 +  "normalize = (abs :: integer \<Rightarrow> integer)"
    1.90 +  by transfer simp
    1.91 +
    1.92 +lemma unit_factor_integer_code [code]:
    1.93 +  "unit_factor = (sgn :: integer \<Rightarrow> integer)"
    1.94 +  by transfer simp
    1.95 +
    1.96  definition divmod_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer \<times> integer"
    1.97  where
    1.98    "divmod_integer k l = (k div l, k mod l)"
    1.99 @@ -760,21 +789,9 @@
   1.100    "nat_of_natural (numeral k) = numeral k"
   1.101    by transfer rule
   1.102  
   1.103 -instantiation natural :: "{semiring_div, equal, linordered_semiring}"
   1.104 +instantiation natural :: "{linordered_semiring, equal}"
   1.105  begin
   1.106  
   1.107 -lift_definition divide_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
   1.108 -  is "divide :: nat \<Rightarrow> nat \<Rightarrow> nat"
   1.109 -  .
   1.110 -
   1.111 -declare divide_natural.rep_eq [simp]
   1.112 -
   1.113 -lift_definition modulo_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
   1.114 -  is "modulo :: nat \<Rightarrow> nat \<Rightarrow> nat"
   1.115 -  .
   1.116 -
   1.117 -declare modulo_natural.rep_eq [simp]
   1.118 -
   1.119  lift_definition less_eq_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool"
   1.120    is "less_eq :: nat \<Rightarrow> nat \<Rightarrow> bool"
   1.121    .
   1.122 @@ -812,6 +829,38 @@
   1.123    "nat_of_natural (max k l) = max (nat_of_natural k) (nat_of_natural l)"
   1.124    by transfer rule
   1.125  
   1.126 +instantiation natural :: "{semiring_div, normalization_semidom}"
   1.127 +begin
   1.128 +
   1.129 +lift_definition normalize_natural :: "natural \<Rightarrow> natural"
   1.130 +  is "normalize :: nat \<Rightarrow> nat"
   1.131 +  .
   1.132 +
   1.133 +declare normalize_natural.rep_eq [simp]
   1.134 +
   1.135 +lift_definition unit_factor_natural :: "natural \<Rightarrow> natural"
   1.136 +  is "unit_factor :: nat \<Rightarrow> nat"
   1.137 +  .
   1.138 +
   1.139 +declare unit_factor_natural.rep_eq [simp]
   1.140 +
   1.141 +lift_definition divide_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
   1.142 +  is "divide :: nat \<Rightarrow> nat \<Rightarrow> nat"
   1.143 +  .
   1.144 +
   1.145 +declare divide_natural.rep_eq [simp]
   1.146 +
   1.147 +lift_definition modulo_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
   1.148 +  is "modulo :: nat \<Rightarrow> nat \<Rightarrow> nat"
   1.149 +  .
   1.150 +
   1.151 +declare modulo_natural.rep_eq [simp]
   1.152 +
   1.153 +instance
   1.154 +  by standard (transfer, auto simp add: algebra_simps unit_factor_nat_def gr0_conv_Suc)+
   1.155 +
   1.156 +end
   1.157 +
   1.158  lift_definition natural_of_integer :: "integer \<Rightarrow> natural"
   1.159    is "nat :: int \<Rightarrow> nat"
   1.160    .
   1.161 @@ -945,7 +994,32 @@
   1.162  
   1.163  lemma [code abstract]:
   1.164    "integer_of_natural (m * n) = integer_of_natural m * integer_of_natural n"
   1.165 -  by transfer (simp add: of_nat_mult)
   1.166 +  by transfer simp
   1.167 +
   1.168 +lemma [code]:
   1.169 +  "normalize n = n" for n :: natural
   1.170 +  by transfer simp
   1.171 +
   1.172 +lemma [code]:
   1.173 +  "unit_factor n = of_bool (n \<noteq> 0)" for n :: natural
   1.174 +proof (cases "n = 0")
   1.175 +  case True
   1.176 +  then show ?thesis
   1.177 +    by simp
   1.178 +next
   1.179 +  case False
   1.180 +  then have "unit_factor n = 1"
   1.181 +  proof transfer
   1.182 +    fix n :: nat
   1.183 +    assume "n \<noteq> 0"
   1.184 +    then obtain m where "n = Suc m"
   1.185 +      by (cases n) auto
   1.186 +    then show "unit_factor n = 1"
   1.187 +      by simp
   1.188 +  qed
   1.189 +  with False show ?thesis
   1.190 +    by simp
   1.191 +qed
   1.192  
   1.193  lemma [code abstract]:
   1.194    "integer_of_natural (m div n) = integer_of_natural m div integer_of_natural n"