author haftmann Mon Oct 09 19:10:49 2017 +0200 (20 months ago) changeset 66838 17989f6bc7b2 parent 66837 6ba663ff2b1c child 66839 909ba5ed93dd
clarified uniqueness criterion for euclidean rings
 src/HOL/Code_Numeral.thy file | annotate | diff | revisions src/HOL/Computational_Algebra/Field_as_Ring.thy file | annotate | diff | revisions src/HOL/Computational_Algebra/Polynomial_Factorial.thy file | annotate | diff | revisions src/HOL/Enum.thy file | annotate | diff | revisions src/HOL/Euclidean_Division.thy file | annotate | diff | revisions
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.5  declare euclidean_size_integer.rep_eq [simp]
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.13 -declare uniqueness_constraint_integer.rep_eq [simp]
1.14 +declare division_segment_integer.rep_eq [simp]
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.22  end
1.24 @@ -258,8 +259,8 @@
1.25    by (simp add: fun_eq_iff nat_of_integer.rep_eq)
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.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.37  declare euclidean_size_natural.rep_eq [simp]
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.45 -declare uniqueness_constraint_natural.rep_eq [simp]
1.46 +declare division_segment_natural.rep_eq [simp]
1.48  instance
1.49    by (standard; transfer)
1.50 @@ -886,8 +887,8 @@
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.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.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.13  instance
2.14    by standard
2.15 @@ -60,9 +60,9 @@
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.25  instance
2.26    by standard
2.27 @@ -91,9 +91,9 @@
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.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.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.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.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.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.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.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.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.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.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.95  end
5.97 -instantiation int :: unique_euclidean_ring
5.98 +instantiation int :: idom_modulo
5.99  begin
5.101 -definition euclidean_size_int :: "int \<Rightarrow> nat"
5.102 -  where [simp]: "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
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.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.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.121 +         distrib_left [symmetric] minus_mult_right
5.122 +         del: of_nat_mult minus_mult_right [symmetric])
5.123 +qed
5.125 +end
5.127 +instantiation int :: unique_euclidean_ring
5.128 +begin
5.130 +definition euclidean_size_int :: "int \<Rightarrow> nat"
5.131 +  where [simp]: "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
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.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.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.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.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.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.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.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.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.186  end