clarified uniqueness criterion for euclidean rings
authorhaftmann
Mon Oct 09 19:10:49 2017 +0200 (18 months ago)
changeset 6683817989f6bc7b2
parent 66837 6ba663ff2b1c
child 66839 909ba5ed93dd
clarified uniqueness criterion for euclidean rings
src/HOL/Code_Numeral.thy
src/HOL/Computational_Algebra/Field_as_Ring.thy
src/HOL/Computational_Algebra/Polynomial_Factorial.thy
src/HOL/Enum.thy
src/HOL/Euclidean_Division.thy
     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)
     2.1 --- a/src/HOL/Computational_Algebra/Field_as_Ring.thy	Mon Oct 09 19:10:48 2017 +0200
     2.2 +++ b/src/HOL/Computational_Algebra/Field_as_Ring.thy	Mon Oct 09 19:10:49 2017 +0200
     2.3 @@ -29,9 +29,9 @@
     2.4  
     2.5  definition [simp]: "normalize_real = (normalize_field :: real \<Rightarrow> _)"
     2.6  definition [simp]: "unit_factor_real = (unit_factor_field :: real \<Rightarrow> _)"
     2.7 +definition [simp]: "modulo_real = (mod_field :: real \<Rightarrow> _)"
     2.8  definition [simp]: "euclidean_size_real = (euclidean_size_field :: real \<Rightarrow> _)"
     2.9 -definition [simp]: "uniqueness_constraint_real = (top :: real \<Rightarrow> real \<Rightarrow> bool)"
    2.10 -definition [simp]: "modulo_real = (mod_field :: real \<Rightarrow> _)"
    2.11 +definition [simp]: "division_segment (x :: real) = 1"
    2.12  
    2.13  instance
    2.14    by standard
    2.15 @@ -60,9 +60,9 @@
    2.16  
    2.17  definition [simp]: "normalize_rat = (normalize_field :: rat \<Rightarrow> _)"
    2.18  definition [simp]: "unit_factor_rat = (unit_factor_field :: rat \<Rightarrow> _)"
    2.19 +definition [simp]: "modulo_rat = (mod_field :: rat \<Rightarrow> _)"
    2.20  definition [simp]: "euclidean_size_rat = (euclidean_size_field :: rat \<Rightarrow> _)"
    2.21 -definition [simp]: "uniqueness_constraint_rat = (top :: rat \<Rightarrow> rat \<Rightarrow> bool)"
    2.22 -definition [simp]: "modulo_rat = (mod_field :: rat \<Rightarrow> _)"
    2.23 +definition [simp]: "division_segment (x :: rat) = 1"
    2.24  
    2.25  instance
    2.26    by standard
    2.27 @@ -91,9 +91,9 @@
    2.28  
    2.29  definition [simp]: "normalize_complex = (normalize_field :: complex \<Rightarrow> _)"
    2.30  definition [simp]: "unit_factor_complex = (unit_factor_field :: complex \<Rightarrow> _)"
    2.31 +definition [simp]: "modulo_complex = (mod_field :: complex \<Rightarrow> _)"
    2.32  definition [simp]: "euclidean_size_complex = (euclidean_size_field :: complex \<Rightarrow> _)"
    2.33 -definition [simp]: "uniqueness_constraint_complex = (top :: complex \<Rightarrow> complex \<Rightarrow> bool)"
    2.34 -definition [simp]: "modulo_complex = (mod_field :: complex \<Rightarrow> _)"
    2.35 +definition [simp]: "division_segment (x :: complex) = 1"
    2.36  
    2.37  instance
    2.38    by standard
     3.1 --- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Mon Oct 09 19:10:48 2017 +0200
     3.2 +++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Mon Oct 09 19:10:49 2017 +0200
     3.3 @@ -745,8 +745,8 @@
     3.4  definition euclidean_size_poly :: "'a poly \<Rightarrow> nat"
     3.5    where "euclidean_size_poly p = (if p = 0 then 0 else 2 ^ degree p)"
     3.6  
     3.7 -definition uniqueness_constraint_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> bool"
     3.8 -  where [simp]: "uniqueness_constraint_poly = top"
     3.9 +definition division_segment_poly :: "'a poly \<Rightarrow> 'a poly"
    3.10 +  where [simp]: "division_segment_poly p = 1"
    3.11  
    3.12  instance proof
    3.13    show "(q * p + r) div p = q" if "p \<noteq> 0"
     4.1 --- a/src/HOL/Enum.thy	Mon Oct 09 19:10:48 2017 +0200
     4.2 +++ b/src/HOL/Enum.thy	Mon Oct 09 19:10:49 2017 +0200
     4.3 @@ -716,7 +716,7 @@
     4.4  definition [simp]: "normalize = (id :: finite_2 \<Rightarrow> _)"
     4.5  definition [simp]: "unit_factor = (id :: finite_2 \<Rightarrow> _)"
     4.6  definition [simp]: "euclidean_size x = (case x of a\<^sub>1 \<Rightarrow> 0 | a\<^sub>2 \<Rightarrow> 1)"
     4.7 -definition [simp]: "uniqueness_constraint = (\<top> :: finite_2 \<Rightarrow> _)"
     4.8 +definition [simp]: "division_segment (x :: finite_2) = 1"
     4.9  instance
    4.10    by standard
    4.11      (auto simp add: divide_finite_2_def times_finite_2_def dvd_finite_2_unfold
    4.12 @@ -868,7 +868,7 @@
    4.13  definition [simp]: "normalize x = (case x of a\<^sub>3 \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> x)"
    4.14  definition [simp]: "unit_factor = (id :: finite_3 \<Rightarrow> _)"
    4.15  definition [simp]: "euclidean_size x = (case x of a\<^sub>1 \<Rightarrow> 0 | _ \<Rightarrow> 1)"
    4.16 -definition [simp]: "uniqueness_constraint = (\<top> :: finite_3 \<Rightarrow> _)"
    4.17 +definition [simp]: "division_segment (x :: finite_3) = 1"
    4.18  instance proof
    4.19    fix x :: finite_3
    4.20    assume "x \<noteq> 0"
     5.1 --- a/src/HOL/Euclidean_Division.thy	Mon Oct 09 19:10:48 2017 +0200
     5.2 +++ b/src/HOL/Euclidean_Division.thy	Mon Oct 09 19:10:49 2017 +0200
     5.3 @@ -506,17 +506,18 @@
     5.4  subsection \<open>Uniquely determined division\<close>
     5.5    
     5.6  class unique_euclidean_semiring = euclidean_semiring + 
     5.7 -  fixes uniqueness_constraint :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
     5.8    assumes size_mono_mult:
     5.9      "b \<noteq> 0 \<Longrightarrow> euclidean_size a < euclidean_size c
    5.10        \<Longrightarrow> euclidean_size (a * b) < euclidean_size (c * b)"
    5.11      -- \<open>FIXME justify\<close>
    5.12 -  assumes uniqueness_constraint_mono_mult:
    5.13 -    "uniqueness_constraint a b \<Longrightarrow> uniqueness_constraint (a * c) (b * c)"
    5.14 -  assumes uniqueness_constraint_mod:
    5.15 -    "b \<noteq> 0 \<Longrightarrow> \<not> b dvd a \<Longrightarrow> uniqueness_constraint (a mod b) b"
    5.16 +  fixes division_segment :: "'a \<Rightarrow> 'a"
    5.17 +  assumes is_unit_division_segment: "is_unit (division_segment a)"
    5.18 +    and division_segment_mult:
    5.19 +    "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> division_segment (a * b) = division_segment a * division_segment b"
    5.20 +    and division_segment_mod:
    5.21 +    "b \<noteq> 0 \<Longrightarrow> \<not> b dvd a \<Longrightarrow> division_segment (a mod b) = division_segment b"
    5.22    assumes div_bounded:
    5.23 -    "b \<noteq> 0 \<Longrightarrow> uniqueness_constraint r b
    5.24 +    "b \<noteq> 0 \<Longrightarrow> division_segment r = division_segment b
    5.25      \<Longrightarrow> euclidean_size r < euclidean_size b
    5.26      \<Longrightarrow> (q * b + r) div b = q"
    5.27  begin
    5.28 @@ -528,7 +529,7 @@
    5.29        and "a mod b = 0"
    5.30        and "a = q * b"
    5.31    | (remainder) q r where "b \<noteq> 0"
    5.32 -      and "uniqueness_constraint r b"
    5.33 +      and "division_segment r = division_segment b"
    5.34        and "euclidean_size r < euclidean_size b"
    5.35        and "r \<noteq> 0"
    5.36        and "a div b = q"
    5.37 @@ -552,19 +553,19 @@
    5.38      case False
    5.39      then have "a mod b \<noteq> 0"
    5.40        by (simp add: mod_eq_0_iff_dvd)
    5.41 -    moreover from \<open>b \<noteq> 0\<close> \<open>\<not> b dvd a\<close> have "uniqueness_constraint (a mod b) b"
    5.42 -      by (rule uniqueness_constraint_mod)
    5.43 +    moreover from \<open>b \<noteq> 0\<close> \<open>\<not> b dvd a\<close> have "division_segment (a mod b) = division_segment b"
    5.44 +      by (rule division_segment_mod)
    5.45      moreover have "euclidean_size (a mod b) < euclidean_size b"
    5.46        using \<open>b \<noteq> 0\<close> by (rule mod_size_less)
    5.47      moreover have "a = a div b * b + a mod b"
    5.48        by (simp add: div_mult_mod_eq)
    5.49      ultimately show thesis
    5.50 -      using \<open>b \<noteq> 0\<close> by (blast intro: remainder)
    5.51 +      using \<open>b \<noteq> 0\<close> by (blast intro!: remainder)
    5.52    qed
    5.53  qed
    5.54  
    5.55  lemma div_eqI:
    5.56 -  "a div b = q" if "b \<noteq> 0" "uniqueness_constraint r b"
    5.57 +  "a div b = q" if "b \<noteq> 0" "division_segment r = division_segment b"
    5.58      "euclidean_size r < euclidean_size b" "q * b + r = a"
    5.59  proof -
    5.60    from that have "(q * b + r) div b = q"
    5.61 @@ -574,7 +575,7 @@
    5.62  qed
    5.63  
    5.64  lemma mod_eqI:
    5.65 -  "a mod b = r" if "b \<noteq> 0" "uniqueness_constraint r b"
    5.66 +  "a mod b = r" if "b \<noteq> 0" "division_segment r = division_segment b"
    5.67      "euclidean_size r < euclidean_size b" "q * b + r = a" 
    5.68  proof -
    5.69    from that have "a div b = q"
    5.70 @@ -618,9 +619,9 @@
    5.71      from \<open>b \<noteq> 0\<close> \<open>c \<noteq> 0\<close> have "b * c \<noteq> 0"
    5.72        by simp
    5.73      from remainder \<open>c \<noteq> 0\<close>
    5.74 -    have "uniqueness_constraint (r * c) (b * c)"
    5.75 +    have "division_segment (r * c) = division_segment (b * c)"
    5.76        and "euclidean_size (r * c) < euclidean_size (b * c)"
    5.77 -      by (simp_all add: uniqueness_constraint_mono_mult uniqueness_constraint_mod size_mono_mult)
    5.78 +      by (simp_all add: division_segment_mult division_segment_mod size_mono_mult)
    5.79      with remainder show ?thesis
    5.80        by (auto intro!: div_eqI [of _ "c * (a mod b)"] simp add: algebra_simps)
    5.81          (use \<open>b * c \<noteq> 0\<close> in simp)
    5.82 @@ -728,8 +729,8 @@
    5.83  definition euclidean_size_nat :: "nat \<Rightarrow> nat"
    5.84    where [simp]: "euclidean_size_nat = id"
    5.85  
    5.86 -definition uniqueness_constraint_nat :: "nat \<Rightarrow> nat \<Rightarrow> bool"
    5.87 -  where [simp]: "uniqueness_constraint_nat = \<top>"
    5.88 +definition division_segment_nat :: "nat \<Rightarrow> nat"
    5.89 +  where [simp]: "division_segment_nat n = 1"
    5.90  
    5.91  definition modulo_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    5.92    where "m mod n = m - (m div n * (n::nat))"
    5.93 @@ -1372,15 +1373,9 @@
    5.94  
    5.95  end
    5.96  
    5.97 -instantiation int :: unique_euclidean_ring
    5.98 +instantiation int :: idom_modulo
    5.99  begin
   5.100  
   5.101 -definition euclidean_size_int :: "int \<Rightarrow> nat"
   5.102 -  where [simp]: "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
   5.103 -
   5.104 -definition uniqueness_constraint_int :: "int \<Rightarrow> int \<Rightarrow> bool"
   5.105 -  where [simp]: "uniqueness_constraint_int k l \<longleftrightarrow> unit_factor k = unit_factor l"
   5.106 -
   5.107  definition modulo_int :: "int \<Rightarrow> int \<Rightarrow> int"
   5.108    where "k mod l = (if l = 0 then k
   5.109      else if sgn k = sgn l
   5.110 @@ -1396,6 +1391,36 @@
   5.111    by (auto simp add: modulo_int_def sgn_0_0 sgn_1_pos sgn_mult abs_mult
   5.112      nat_mult_distrib dvd_int_iff)
   5.113  
   5.114 +instance proof
   5.115 +  fix k l :: int
   5.116 +  obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m" 
   5.117 +    by (blast intro: int_sgnE elim: that)
   5.118 +  then show "k div l * l + k mod l = k"
   5.119 +    by (auto simp add: divide_int_unfold modulo_int_unfold algebra_simps dest!: sgn_not_eq_imp)
   5.120 +       (simp_all add: of_nat_mult [symmetric] of_nat_add [symmetric]
   5.121 +         distrib_left [symmetric] minus_mult_right
   5.122 +         del: of_nat_mult minus_mult_right [symmetric])
   5.123 +qed
   5.124 +
   5.125 +end
   5.126 +
   5.127 +instantiation int :: unique_euclidean_ring
   5.128 +begin
   5.129 +
   5.130 +definition euclidean_size_int :: "int \<Rightarrow> nat"
   5.131 +  where [simp]: "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
   5.132 +
   5.133 +definition division_segment_int :: "int \<Rightarrow> int"
   5.134 +  where "division_segment_int k = (if k \<ge> 0 then 1 else - 1)"
   5.135 +
   5.136 +lemma division_segment_eq_sgn:
   5.137 +  "division_segment k = sgn k" if "k \<noteq> 0" for k :: int
   5.138 +  using that by (simp add: division_segment_int_def)
   5.139 +
   5.140 +lemma abs_division_segment [simp]:
   5.141 +  "\<bar>division_segment k\<bar> = 1" for k :: int
   5.142 +  by (simp add: division_segment_int_def)
   5.143 +
   5.144  lemma abs_mod_less:
   5.145    "\<bar>k mod l\<bar> < \<bar>l\<bar>" if "l \<noteq> 0" for k l :: int
   5.146  proof -
   5.147 @@ -1418,13 +1443,9 @@
   5.148  
   5.149  instance proof
   5.150    fix k l :: int
   5.151 -  obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m" 
   5.152 -    by (blast intro: int_sgnE elim: that)
   5.153 -  then show "k div l * l + k mod l = k"
   5.154 -    by (auto simp add: divide_int_unfold modulo_int_unfold algebra_simps dest!: sgn_not_eq_imp)
   5.155 -       (simp_all add: of_nat_mult [symmetric] of_nat_add [symmetric]
   5.156 -         distrib_left [symmetric] minus_mult_right
   5.157 -         del: of_nat_mult minus_mult_right [symmetric])
   5.158 +  show "division_segment (k mod l) = division_segment l" if
   5.159 +    "l \<noteq> 0" and "\<not> l dvd k"
   5.160 +    using that by (simp add: division_segment_eq_sgn dvd_eq_mod_eq_0 sgn_mod)
   5.161  next
   5.162    fix l q r :: int
   5.163    obtain n m and s t
   5.164 @@ -1433,12 +1454,12 @@
   5.165    assume \<open>l \<noteq> 0\<close>
   5.166    with l have "s \<noteq> 0" and "n > 0"
   5.167      by (simp_all add: sgn_0_0)
   5.168 -  assume "uniqueness_constraint r l"
   5.169 +  assume "division_segment r = division_segment l"
   5.170    moreover have "r = sgn r * \<bar>r\<bar>"
   5.171      by (simp add: sgn_mult_abs)
   5.172    moreover define u where "u = nat \<bar>r\<bar>"
   5.173    ultimately have "r = sgn l * int u"
   5.174 -    by simp
   5.175 +    using division_segment_eq_sgn \<open>l \<noteq> 0\<close> by (cases "r = 0") simp_all
   5.176    with l \<open>n > 0\<close> have r: "r = sgn s * int u"
   5.177      by (simp add: sgn_mult)
   5.178    assume "euclidean_size r < euclidean_size l"
   5.179 @@ -1481,7 +1502,7 @@
   5.180        by (simp only: *, simp only: l q divide_int_unfold)
   5.181          (auto simp add: sgn_mult sgn_0_0 sgn_1_pos algebra_simps dest: dvd_imp_le)
   5.182    qed
   5.183 -qed (use mult_le_mono2 [of 1] in \<open>auto simp add: abs_mult sgn_mult abs_mod_less sgn_mod nat_mult_distrib\<close>)
   5.184 +qed (use mult_le_mono2 [of 1] in \<open>auto simp add: division_segment_int_def not_le sign_simps abs_mult sgn_mult abs_mod_less sgn_mod nat_mult_distrib\<close>)
   5.185  
   5.186  end
   5.187