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.51    fact le_add_diff_inverse2
    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    .