more lemmas
authorhaftmann
Tue Mar 20 09:27:40 2018 +0000 (14 months ago)
changeset 679069cc32b18c785
parent 67905 fe0f4eeceeb7
child 67907 02a14c1cb917
child 67911 3cda747493d8
more lemmas
src/HOL/Parity.thy
     1.1 --- a/src/HOL/Parity.thy	Tue Mar 20 09:27:39 2018 +0000
     1.2 +++ b/src/HOL/Parity.thy	Tue Mar 20 09:27:40 2018 +0000
     1.3 @@ -418,6 +418,20 @@
     1.4    "even (a - b) \<longleftrightarrow> even (a + b)"
     1.5    using even_add [of a "- b"] by simp
     1.6  
     1.7 +lemma minus_1_mod_2_eq [simp]:
     1.8 +  "- 1 mod 2 = 1"
     1.9 +  by (simp add: mod_2_eq_odd)
    1.10 +
    1.11 +lemma minus_1_div_2_eq [simp]:
    1.12 +  "- 1 div 2 = - 1"
    1.13 +proof -
    1.14 +  from div_mult_mod_eq [of "- 1" 2]
    1.15 +  have "- 1 div 2 * 2 = - 1 * 2"
    1.16 +    using local.add_implies_diff by fastforce
    1.17 +  then show ?thesis
    1.18 +    using mult_right_cancel [of 2 "- 1 div 2" "- 1"] by simp
    1.19 +qed
    1.20 +
    1.21  end
    1.22  
    1.23