src/HOL/Word/Num_Lemmas.thy
changeset 30943 eb3dbbe971f6
parent 30445 757ba2bb2b39
child 31018 b8a8cf6e16f2
equal deleted inserted replaced
30942:1e246776f876 30943:eb3dbbe971f6
    64   "even n ==> even d ==> 0 <= d ==> (n + 1) mod (d :: int) = (n mod d) + 1"
    64   "even n ==> even d ==> 0 <= d ==> (n + 1) mod (d :: int) = (n mod d) + 1"
    65   apply (simp add: add_commute)
    65   apply (simp add: add_commute)
    66   apply (safe dest!: even_equiv_def [THEN iffD1])
    66   apply (safe dest!: even_equiv_def [THEN iffD1])
    67   apply (subst pos_zmod_mult_2)
    67   apply (subst pos_zmod_mult_2)
    68    apply arith
    68    apply arith
    69   apply (simp add: zmod_zmult_zmult1)
    69   apply (simp add: mod_mult_mult1)
    70  done
    70  done
    71 
    71 
    72 lemmas eme1p = emep1 [simplified add_commute]
    72 lemmas eme1p = emep1 [simplified add_commute]
    73 
    73 
    74 lemma le_diff_eq': "(a \<le> c - b) = (b + a \<le> (c::int))" by arith
    74 lemma le_diff_eq': "(a \<le> c - b) = (b + a \<le> (c::int))" by arith