equal
deleted
inserted
replaced
31 |
31 |
32 lemma sum_imp_diff: "j = k + i ==> j - i = (k :: nat)" by arith |
32 lemma sum_imp_diff: "j = k + i ==> j - i = (k :: nat)" by arith |
33 |
33 |
34 lemma zless2: "0 < (2 :: int)" by arith |
34 lemma zless2: "0 < (2 :: int)" by arith |
35 |
35 |
36 lemmas zless2p [simp] = zless2 [THEN zero_less_power] |
36 lemmas zless2p = zless2 [THEN zero_less_power] |
37 lemmas zle2p [simp] = zless2p [THEN order_less_imp_le] |
37 lemmas zle2p = zless2p [THEN order_less_imp_le] |
38 |
38 |
39 lemmas pos_mod_sign2 = zless2 [THEN pos_mod_sign [where b = "2::int"]] |
39 lemmas pos_mod_sign2 = zless2 [THEN pos_mod_sign [where b = "2::int"]] |
40 lemmas pos_mod_bound2 = zless2 [THEN pos_mod_bound [where b = "2::int"]] |
40 lemmas pos_mod_bound2 = zless2 [THEN pos_mod_bound [where b = "2::int"]] |
41 |
41 |
42 lemma nmod2: "n mod (2::int) = 0 | n mod 2 = 1" by arith |
42 lemma nmod2: "n mod (2::int) = 0 | n mod 2 = 1" by arith |