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"
```