src/HOL/Code_Numeral.thy
changeset 66815 93c6632ddf44
parent 66806 a4e82b58d833
child 66817 0b12755ccbb2
     1.1 --- a/src/HOL/Code_Numeral.thy	Sun Oct 08 22:28:22 2017 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Sun Oct 08 22:28:22 2017 +0200
     1.3 @@ -282,6 +282,9 @@
     1.4    "uniqueness_constraint (k :: integer) l \<longleftrightarrow> unit_factor k = unit_factor l"
     1.5    by (simp add: integer_eq_iff)
     1.6  
     1.7 +instance integer :: ring_parity
     1.8 +  by (standard; transfer) (simp_all add: of_nat_div odd_iff_mod_2_eq_one)
     1.9 +
    1.10  instantiation integer :: unique_euclidean_semiring_numeral
    1.11  begin
    1.12  
    1.13 @@ -927,6 +930,9 @@
    1.14    "uniqueness_constraint = (\<top> :: natural \<Rightarrow> natural \<Rightarrow> bool)"
    1.15    by (simp add: fun_eq_iff)
    1.16  
    1.17 +instance natural :: semiring_parity
    1.18 +  by (standard; transfer) (simp_all add: of_nat_div odd_iff_mod_2_eq_one)
    1.19 +
    1.20  lift_definition natural_of_integer :: "integer \<Rightarrow> natural"
    1.21    is "nat :: int \<Rightarrow> nat"
    1.22    .