src/HOL/Code_Numeral.thy
 changeset 66838 17989f6bc7b2 parent 66836 4eb431c3f974 child 66839 909ba5ed93dd
```     1.1 --- a/src/HOL/Code_Numeral.thy	Mon Oct 09 19:10:48 2017 +0200
1.2 +++ b/src/HOL/Code_Numeral.thy	Mon Oct 09 19:10:49 2017 +0200
1.3 @@ -241,15 +241,16 @@
1.4
1.5  declare euclidean_size_integer.rep_eq [simp]
1.6
1.7 -lift_definition uniqueness_constraint_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
1.8 -  is "uniqueness_constraint :: int \<Rightarrow> int \<Rightarrow> bool"
1.9 +lift_definition division_segment_integer :: "integer \<Rightarrow> integer"
1.10 +  is "division_segment :: int \<Rightarrow> int"
1.11    .
1.12
1.13 -declare uniqueness_constraint_integer.rep_eq [simp]
1.14 +declare division_segment_integer.rep_eq [simp]
1.15
1.16  instance
1.17    by (standard; transfer)
1.18 -    (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.19 +    (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
1.20 +     division_segment_mult division_segment_mod intro: div_eqI\<close>)
1.21
1.22  end
1.23
1.24 @@ -258,8 +259,8 @@
1.25    by (simp add: fun_eq_iff nat_of_integer.rep_eq)
1.26
1.27  lemma [code]:
1.28 -  "uniqueness_constraint (k :: integer) l \<longleftrightarrow> sgn k = sgn l"
1.29 -  by (simp add: integer_eq_iff)
1.30 +  "division_segment (k :: integer) = (if k \<ge> 0 then 1 else - 1)"
1.31 +  by transfer (simp add: division_segment_int_def)
1.32
1.33  instance integer :: ring_parity
1.34    by (standard; transfer) (simp_all add: of_nat_div odd_iff_mod_2_eq_one)
1.35 @@ -869,11 +870,11 @@
1.36
1.37  declare euclidean_size_natural.rep_eq [simp]
1.38
1.39 -lift_definition uniqueness_constraint_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool"
1.40 -  is "uniqueness_constraint :: nat \<Rightarrow> nat \<Rightarrow> bool"
1.41 +lift_definition division_segment_natural :: "natural \<Rightarrow> natural"
1.42 +  is "division_segment :: nat \<Rightarrow> nat"
1.43    .
1.44
1.45 -declare uniqueness_constraint_natural.rep_eq [simp]
1.46 +declare division_segment_natural.rep_eq [simp]
1.47
1.48  instance
1.49    by (standard; transfer)
1.50 @@ -886,8 +887,8 @@
1.51    by (simp add: fun_eq_iff)
1.52
1.53  lemma [code]:
1.54 -  "uniqueness_constraint = (\<top> :: natural \<Rightarrow> natural \<Rightarrow> bool)"
1.55 -  by (simp add: fun_eq_iff)
1.56 +  "division_segment (n::natural) = 1"
1.57 +  by (simp add: natural_eq_iff)
1.58
1.59  instance natural :: semiring_parity
1.60    by (standard; transfer) (simp_all add: of_nat_div odd_iff_mod_2_eq_one)
```