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)