src/HOL/Presburger.thy
changeset 58777 6ba2f1fa243b
parent 57514 bdc2c6b40bf2
child 58787 af9eb5e566dd
     1.1 --- a/src/HOL/Presburger.thy	Fri Oct 24 15:07:51 2014 +0200
     1.2 +++ b/src/HOL/Presburger.thy	Thu Oct 23 19:40:39 2014 +0200
     1.3 @@ -434,6 +434,78 @@
     1.4  lemma [presburger, algebra]: "m mod (Suc (Suc 0)) = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
     1.5  lemma [presburger, algebra]: "m mod 2 = (1::int) \<longleftrightarrow> \<not> 2 dvd m " by presburger
     1.6  
     1.7 +context semiring_parity
     1.8 +begin
     1.9 +
    1.10 +declare even_times_iff [presburger]
    1.11 +
    1.12 +declare even_power [presburger]
    1.13 +
    1.14 +lemma [presburger]:
    1.15 +  "even (a + b) \<longleftrightarrow> even a \<and> even b \<or> odd a \<and> odd b"
    1.16 +  by auto
    1.17 +
    1.18 +end
    1.19 +
    1.20 +context ring_parity
    1.21 +begin
    1.22 +
    1.23 +declare even_minus [presburger]
    1.24 +
    1.25 +end
    1.26 +
    1.27 +context linordered_idom
    1.28 +begin
    1.29 +
    1.30 +declare zero_le_power_iff [presburger]
    1.31 +
    1.32 +declare zero_le_power_eq [presburger]
    1.33 +
    1.34 +declare zero_less_power_eq [presburger]
    1.35 +
    1.36 +declare power_less_zero_eq [presburger]
    1.37 +  
    1.38 +declare power_le_zero_eq [presburger]
    1.39 +
    1.40 +end
    1.41 +
    1.42 +declare even_Suc [presburger]
    1.43 +
    1.44 +lemma [presburger]:
    1.45 +  "Suc n div Suc (Suc 0) = n div Suc (Suc 0) \<longleftrightarrow> even n"
    1.46 +  by presburger
    1.47 +
    1.48 +declare even_diff_nat [presburger]
    1.49 +
    1.50 +lemma [presburger]:
    1.51 +  fixes k :: int
    1.52 +  shows "(k + 1) div 2 = k div 2 \<longleftrightarrow> even k"
    1.53 +  by presburger
    1.54 +
    1.55 +lemma [presburger]:
    1.56 +  fixes k :: int
    1.57 +  shows "(k + 1) div 2 = k div 2 + 1 \<longleftrightarrow> odd k"
    1.58 +  by presburger
    1.59 +
    1.60 +lemma [presburger]:
    1.61 +  "even n \<longleftrightarrow> even (int n)"
    1.62 +  using even_int_iff [of n] by simp
    1.63 +  
    1.64 +
    1.65 +subsection {* Nice facts about division by @{term 4} *}  
    1.66 +
    1.67 +lemma even_even_mod_4_iff:
    1.68 +  "even (n::nat) \<longleftrightarrow> even (n mod 4)"
    1.69 +  by presburger
    1.70 +
    1.71 +lemma odd_mod_4_div_2:
    1.72 +  "n mod 4 = (3::nat) \<Longrightarrow> odd ((n - 1) div 2)"
    1.73 +  by presburger
    1.74 +
    1.75 +lemma even_mod_4_div_2:
    1.76 +  "n mod 4 = (1::nat) \<Longrightarrow> even ((n - 1) div 2)"
    1.77 +  by presburger
    1.78 +
    1.79  
    1.80  subsection {* Try0 *}
    1.81