src/HOL/Presburger.thy
changeset 36749 a8dc19a352e6
parent 35216 7641e8d831d2
child 36798 3981db162131
equal deleted inserted replaced
36724:5779d9fbedd0 36749:a8dc19a352e6
   455 lemma [presburger, algebra]: "m mod 2 = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
   455 lemma [presburger, algebra]: "m mod 2 = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
   456 lemma [presburger, algebra]: "m mod (Suc (Suc 0)) = (1::nat) \<longleftrightarrow> \<not> 2 dvd m " by presburger
   456 lemma [presburger, algebra]: "m mod (Suc (Suc 0)) = (1::nat) \<longleftrightarrow> \<not> 2 dvd m " by presburger
   457 lemma [presburger, algebra]: "m mod (Suc (Suc 0)) = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
   457 lemma [presburger, algebra]: "m mod (Suc (Suc 0)) = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
   458 lemma [presburger, algebra]: "m mod 2 = (1::int) \<longleftrightarrow> \<not> 2 dvd m " by presburger
   458 lemma [presburger, algebra]: "m mod 2 = (1::int) \<longleftrightarrow> \<not> 2 dvd m " by presburger
   459 
   459 
   460 
       
   461 lemma zdvd_period:
       
   462   fixes a d :: int
       
   463   assumes advdd: "a dvd d"
       
   464   shows "a dvd (x + t) \<longleftrightarrow> a dvd ((x + c * d) + t)"
       
   465   using advdd
       
   466   apply -
       
   467   apply (rule iffI)
       
   468   by algebra+
       
   469 
       
   470 end
   460 end