clarified parity
authorhaftmann
Mon Oct 09 19:10:51 2017 +0200 (19 months ago)
changeset 66839909ba5ed93dd
parent 66838 17989f6bc7b2
child 66840 0d689d71dbdc
clarified parity
src/HOL/Code_Numeral.thy
src/HOL/Euclidean_Division.thy
src/HOL/Parity.thy
     1.1 --- a/src/HOL/Code_Numeral.thy	Mon Oct 09 19:10:49 2017 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Mon Oct 09 19:10:51 2017 +0200
     1.3 @@ -263,7 +263,7 @@
     1.4    by transfer (simp add: division_segment_int_def)
     1.5  
     1.6  instance integer :: ring_parity
     1.7 -  by (standard; transfer) (simp_all add: of_nat_div odd_iff_mod_2_eq_one)
     1.8 +  by (standard; transfer) (simp_all add: of_nat_div division_segment_int_def)
     1.9  
    1.10  instantiation integer :: unique_euclidean_semiring_numeral
    1.11  begin
    1.12 @@ -891,7 +891,7 @@
    1.13    by (simp add: natural_eq_iff)
    1.14  
    1.15  instance natural :: semiring_parity
    1.16 -  by (standard; transfer) (simp_all add: of_nat_div odd_iff_mod_2_eq_one)
    1.17 +  by (standard; transfer) simp_all
    1.18  
    1.19  lift_definition natural_of_integer :: "integer \<Rightarrow> natural"
    1.20    is "nat :: int \<Rightarrow> nat"
     2.1 --- a/src/HOL/Euclidean_Division.thy	Mon Oct 09 19:10:49 2017 +0200
     2.2 +++ b/src/HOL/Euclidean_Division.thy	Mon Oct 09 19:10:51 2017 +0200
     2.3 @@ -511,7 +511,7 @@
     2.4        \<Longrightarrow> euclidean_size (a * b) < euclidean_size (c * b)"
     2.5      -- \<open>FIXME justify\<close>
     2.6    fixes division_segment :: "'a \<Rightarrow> 'a"
     2.7 -  assumes is_unit_division_segment: "is_unit (division_segment a)"
     2.8 +  assumes is_unit_division_segment [simp]: "is_unit (division_segment a)"
     2.9      and division_segment_mult:
    2.10      "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> division_segment (a * b) = division_segment a * division_segment b"
    2.11      and division_segment_mod:
    2.12 @@ -522,6 +522,10 @@
    2.13      \<Longrightarrow> (q * b + r) div b = q"
    2.14  begin
    2.15  
    2.16 +lemma division_segment_not_0 [simp]:
    2.17 +  "division_segment a \<noteq> 0"
    2.18 +  using is_unit_division_segment [of a] is_unitE [of "division_segment a"] by blast
    2.19 +
    2.20  lemma divmod_cases [case_names divides remainder by0]:
    2.21    obtains 
    2.22      (divides) q where "b \<noteq> 0"
     3.1 --- a/src/HOL/Parity.thy	Mon Oct 09 19:10:49 2017 +0200
     3.2 +++ b/src/HOL/Parity.thy	Mon Oct 09 19:10:51 2017 +0200
     3.3 @@ -13,10 +13,48 @@
     3.4  
     3.5  class semiring_parity = linordered_semidom + unique_euclidean_semiring +
     3.6    assumes of_nat_div: "of_nat (m div n) = of_nat m div of_nat n"
     3.7 -    and odd_imp_mod_2_eq_1: "\<not> 2 dvd a \<Longrightarrow> a mod 2 = 1"
     3.8 +    and division_segment_of_nat [simp]: "division_segment (of_nat n) = 1"
     3.9 +    and division_segment_euclidean_size [simp]: "division_segment a * of_nat (euclidean_size a) = a"
    3.10 +begin
    3.11 +
    3.12 +lemma division_segment_eq_iff:
    3.13 +  "a = b" if "division_segment a = division_segment b"
    3.14 +    and "euclidean_size a = euclidean_size b"
    3.15 +  using that division_segment_euclidean_size [of a] by simp
    3.16 +
    3.17 +lemma euclidean_size_of_nat [simp]:
    3.18 +  "euclidean_size (of_nat n) = n"
    3.19 +proof -
    3.20 +  have "division_segment (of_nat n) * of_nat (euclidean_size (of_nat n)) = of_nat n"
    3.21 +    by (fact division_segment_euclidean_size)
    3.22 +  then show ?thesis by simp
    3.23 +qed
    3.24  
    3.25 -context semiring_parity
    3.26 -begin
    3.27 +lemma of_nat_euclidean_size:
    3.28 +  "of_nat (euclidean_size a) = a div division_segment a"
    3.29 +proof -
    3.30 +  have "of_nat (euclidean_size a) = division_segment a * of_nat (euclidean_size a) div division_segment a"
    3.31 +    by (subst nonzero_mult_div_cancel_left) simp_all
    3.32 +  also have "\<dots> = a div division_segment a"
    3.33 +    by simp
    3.34 +  finally show ?thesis .
    3.35 +qed
    3.36 +
    3.37 +lemma division_segment_1 [simp]:
    3.38 +  "division_segment 1 = 1"
    3.39 +  using division_segment_of_nat [of 1] by simp
    3.40 +
    3.41 +lemma division_segment_numeral [simp]:
    3.42 +  "division_segment (numeral k) = 1"
    3.43 +  using division_segment_of_nat [of "numeral k"] by simp
    3.44 +
    3.45 +lemma euclidean_size_1 [simp]:
    3.46 +  "euclidean_size 1 = 1"
    3.47 +  using euclidean_size_of_nat [of 1] by simp
    3.48 +
    3.49 +lemma euclidean_size_numeral [simp]:
    3.50 +  "euclidean_size (numeral k) = numeral k"
    3.51 +  using euclidean_size_of_nat [of "numeral k"] by simp
    3.52  
    3.53  lemma of_nat_dvd_iff:
    3.54    "of_nat m dvd of_nat n \<longleftrightarrow> m dvd n" (is "?P \<longleftrightarrow> ?Q")
    3.55 @@ -86,7 +124,43 @@
    3.56  
    3.57  lemma odd_iff_mod_2_eq_one:
    3.58    "odd a \<longleftrightarrow> a mod 2 = 1"
    3.59 -  by (auto dest: odd_imp_mod_2_eq_1)
    3.60 +proof
    3.61 +  assume "a mod 2 = 1"
    3.62 +  then show "odd a"
    3.63 +    by auto
    3.64 +next
    3.65 +  assume "odd a"
    3.66 +  have eucl: "euclidean_size (a mod 2) = 1"
    3.67 +  proof (rule order_antisym)
    3.68 +    show "euclidean_size (a mod 2) \<le> 1"
    3.69 +      using mod_size_less [of 2 a] by simp
    3.70 +    show "1 \<le> euclidean_size (a mod 2)"
    3.71 +    proof (rule ccontr)
    3.72 +      assume "\<not> 1 \<le> euclidean_size (a mod 2)"
    3.73 +      then have "euclidean_size (a mod 2) = 0"
    3.74 +        by simp
    3.75 +      then have "division_segment (a mod 2) * of_nat (euclidean_size (a mod 2)) = division_segment (a mod 2) * of_nat 0"
    3.76 +        by simp
    3.77 +      with \<open>odd a\<close> show False
    3.78 +        by (simp add: dvd_eq_mod_eq_0)
    3.79 +    qed
    3.80 +  qed 
    3.81 +  from \<open>odd a\<close> have "\<not> of_nat 2 dvd division_segment a * of_nat (euclidean_size a)"
    3.82 +    by simp
    3.83 +  then have "\<not> of_nat 2 dvd of_nat (euclidean_size a)"
    3.84 +    by (auto simp only: dvd_mult_unit_iff' is_unit_division_segment)
    3.85 +  then have "\<not> 2 dvd euclidean_size a"
    3.86 +    using of_nat_dvd_iff [of 2] by simp
    3.87 +  then have "euclidean_size a mod 2 = 1"
    3.88 +    by (simp add: semidom_modulo_class.dvd_eq_mod_eq_0)
    3.89 +  then have "of_nat (euclidean_size a mod 2) = of_nat 1"
    3.90 +    by simp
    3.91 +  then have "of_nat (euclidean_size a) mod 2 = 1"
    3.92 +    by (simp add: of_nat_mod)
    3.93 +  from \<open>odd a\<close> eucl
    3.94 +  show "a mod 2 = 1"
    3.95 +    by (auto intro: division_segment_eq_iff simp add: division_segment_mod)
    3.96 +qed
    3.97  
    3.98  lemma parity_cases [case_names even odd]:
    3.99    assumes "even a \<Longrightarrow> a mod 2 = 0 \<Longrightarrow> P"
   3.100 @@ -487,22 +561,7 @@
   3.101  subsection \<open>Instance for @{typ int}\<close>
   3.102  
   3.103  instance int :: ring_parity
   3.104 -proof
   3.105 -  fix k l :: int
   3.106 -  show "k mod 2 = 1" if "\<not> 2 dvd k"
   3.107 -  proof (rule order_antisym)
   3.108 -    have "0 \<le> k mod 2" and "k mod 2 < 2"
   3.109 -      by auto
   3.110 -    moreover have "k mod 2 \<noteq> 0"
   3.111 -      using that by (simp add: dvd_eq_mod_eq_0)
   3.112 -    ultimately have "0 < k mod 2"
   3.113 -      by (simp only: less_le) simp
   3.114 -    then show "1 \<le> k mod 2"
   3.115 -      by simp
   3.116 -    from \<open>k mod 2 < 2\<close> show "k mod 2 \<le> 1"
   3.117 -      by (simp only: less_le) simp
   3.118 -  qed
   3.119 -qed (simp_all add: dvd_eq_mod_eq_0 divide_int_def)
   3.120 +  by standard (simp_all add: dvd_eq_mod_eq_0 divide_int_def division_segment_int_def)
   3.121  
   3.122  lemma even_diff_iff [simp]:
   3.123    "even (k - l) \<longleftrightarrow> even (k + l)" for k l :: int