src/HOL/Code_Numeral.thy
 changeset 66806 a4e82b58d833 parent 66801 f3fda9777f9a child 66815 93c6632ddf44
```     1.1 --- a/src/HOL/Code_Numeral.thy	Sun Oct 08 22:28:21 2017 +0200
1.2 +++ b/src/HOL/Code_Numeral.thy	Sun Oct 08 22:28:21 2017 +0200
1.3 @@ -247,7 +247,7 @@
1.4
1.5  end
1.6
1.7 -instantiation integer :: ring_div
1.8 +instantiation integer :: unique_euclidean_ring
1.9  begin
1.10
1.11  lift_definition modulo_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
1.12 @@ -256,12 +256,33 @@
1.13
1.14  declare modulo_integer.rep_eq [simp]
1.15
1.16 +lift_definition euclidean_size_integer :: "integer \<Rightarrow> nat"
1.17 +  is "euclidean_size :: int \<Rightarrow> nat"
1.18 +  .
1.19 +
1.20 +declare euclidean_size_integer.rep_eq [simp]
1.21 +
1.22 +lift_definition uniqueness_constraint_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
1.23 +  is "uniqueness_constraint :: int \<Rightarrow> int \<Rightarrow> bool"
1.24 +  .
1.25 +
1.26 +declare uniqueness_constraint_integer.rep_eq [simp]
1.27 +
1.28  instance
1.29 -  by (standard; transfer) simp_all
1.30 +  by (standard; transfer)
1.31 +    (use mult_le_mono2 [of 1] in \<open>auto simp add: sgn_mult_abs abs_mult sgn_mult abs_mod_less sgn_mod nat_mult_distrib\<close>, rule div_eqI, simp_all)
1.32
1.33  end
1.34
1.35 -instantiation integer :: semiring_numeral_div
1.36 +lemma [code]:
1.37 +  "euclidean_size = nat_of_integer \<circ> abs"
1.38 +  by (simp add: fun_eq_iff nat_of_integer.rep_eq)
1.39 +
1.40 +lemma [code]:
1.41 +  "uniqueness_constraint (k :: integer) l \<longleftrightarrow> unit_factor k = unit_factor l"
1.42 +  by (simp add: integer_eq_iff)
1.43 +
1.44 +instantiation integer :: unique_euclidean_semiring_numeral
1.45  begin
1.46
1.47  definition divmod_integer :: "num \<Rightarrow> num \<Rightarrow> integer \<times> integer"
1.48 @@ -283,15 +304,15 @@
1.49      by (fact divmod_step_integer_def)
1.50  qed (transfer,
1.52 -  semiring_numeral_div_class.div_less
1.53 -  semiring_numeral_div_class.mod_less
1.54 -  semiring_numeral_div_class.div_positive
1.55 -  semiring_numeral_div_class.mod_less_eq_dividend
1.56 -  semiring_numeral_div_class.pos_mod_bound
1.57 -  semiring_numeral_div_class.pos_mod_sign
1.58 -  semiring_numeral_div_class.mod_mult2_eq
1.59 -  semiring_numeral_div_class.div_mult2_eq
1.60 -  semiring_numeral_div_class.discrete)+
1.61 +  unique_euclidean_semiring_numeral_class.div_less
1.62 +  unique_euclidean_semiring_numeral_class.mod_less
1.63 +  unique_euclidean_semiring_numeral_class.div_positive
1.64 +  unique_euclidean_semiring_numeral_class.mod_less_eq_dividend
1.65 +  unique_euclidean_semiring_numeral_class.pos_mod_bound
1.66 +  unique_euclidean_semiring_numeral_class.pos_mod_sign
1.67 +  unique_euclidean_semiring_numeral_class.mod_mult2_eq
1.68 +  unique_euclidean_semiring_numeral_class.div_mult2_eq
1.69 +  unique_euclidean_semiring_numeral_class.discrete)+
1.70
1.71  end
1.72
1.73 @@ -853,7 +874,7 @@
1.74    "nat_of_natural (max k l) = max (nat_of_natural k) (nat_of_natural l)"
1.75    by transfer rule
1.76
1.77 -instantiation natural :: "{semiring_div, normalization_semidom}"
1.78 +instantiation natural :: unique_euclidean_semiring
1.79  begin
1.80
1.81  lift_definition normalize_natural :: "natural \<Rightarrow> natural"
1.82 @@ -880,11 +901,32 @@
1.83
1.84  declare modulo_natural.rep_eq [simp]
1.85
1.86 +lift_definition euclidean_size_natural :: "natural \<Rightarrow> nat"
1.87 +  is "euclidean_size :: nat \<Rightarrow> nat"
1.88 +  .
1.89 +
1.90 +declare euclidean_size_natural.rep_eq [simp]
1.91 +
1.92 +lift_definition uniqueness_constraint_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool"
1.93 +  is "uniqueness_constraint :: nat \<Rightarrow> nat \<Rightarrow> bool"
1.94 +  .
1.95 +
1.96 +declare uniqueness_constraint_natural.rep_eq [simp]
1.97 +
1.98  instance
1.99 -  by standard (transfer, auto simp add: algebra_simps unit_factor_nat_def gr0_conv_Suc)+
1.100 +  by (standard; transfer)
1.101 +    (auto simp add: algebra_simps unit_factor_nat_def gr0_conv_Suc)
1.102
1.103  end
1.104
1.105 +lemma [code]:
1.106 +  "euclidean_size = nat_of_natural"
1.107 +  by (simp add: fun_eq_iff)
1.108 +
1.109 +lemma [code]:
1.110 +  "uniqueness_constraint = (\<top> :: natural \<Rightarrow> natural \<Rightarrow> bool)"
1.111 +  by (simp add: fun_eq_iff)
1.112 +
1.113  lift_definition natural_of_integer :: "integer \<Rightarrow> natural"
1.114    is "nat :: int \<Rightarrow> nat"
1.115    .
```