equal
deleted
inserted
replaced
52 |
52 |
53 lemma minus_numeral: "f (gm x (numeral n)) = f x" |
53 lemma minus_numeral: "f (gm x (numeral n)) = f x" |
54 by (subst of_nat_numeral[symmetric], subst minus_of_nat) (rule refl) |
54 by (subst of_nat_numeral[symmetric], subst minus_of_nat) (rule refl) |
55 |
55 |
56 lemma minus_1: "f (gn1 x) = f x" |
56 lemma minus_1: "f (gn1 x) = f x" |
57 using minus_of_nat[of x 1] by (simp add: minus_1_eq minus_eq[symmetric]) |
57 using minus_of_nat[of x 1] by (simp flip: minus_1_eq minus_eq) |
58 |
58 |
59 lemmas periodic_simps = plus_of_nat minus_of_nat plus_of_int minus_of_int |
59 lemmas periodic_simps = plus_of_nat minus_of_nat plus_of_int minus_of_int |
60 plus_numeral minus_numeral plus_1 minus_1 |
60 plus_numeral minus_numeral plus_1 minus_1 |
61 |
61 |
62 end |
62 end |