equal
deleted
inserted
replaced
18 |
18 |
19 lemmas rev_min_pm1 [simp] = trans [OF add_commute rev_min_pm] |
19 lemmas rev_min_pm1 [simp] = trans [OF add_commute rev_min_pm] |
20 |
20 |
21 lemma min_minus [simp] : "min m (m - k) = (m - k :: nat)" by arith |
21 lemma min_minus [simp] : "min m (m - k) = (m - k :: nat)" by arith |
22 |
22 |
23 lemmas min_minus' [simp] = trans [OF min_max.inf_commute min_minus] |
23 lemmas min_minus' [simp] = trans [OF min.commute min_minus] |
24 |
24 |
25 lemma mod_2_neq_1_eq_eq_0: |
25 lemma mod_2_neq_1_eq_eq_0: |
26 fixes k :: int |
26 fixes k :: int |
27 shows "k mod 2 \<noteq> 1 \<longleftrightarrow> k mod 2 = 0" |
27 shows "k mod 2 \<noteq> 1 \<longleftrightarrow> k mod 2 = 0" |
28 by arith |
28 by arith |