equal
deleted
inserted
replaced
556 done |
556 done |
557 |
557 |
558 lemma decr_lemma: "0 < (d::int) \<Longrightarrow> x - (abs(x-z)+1) * d < z" |
558 lemma decr_lemma: "0 < (d::int) \<Longrightarrow> x - (abs(x-z)+1) * d < z" |
559 apply(induct rule: int_gr_induct) |
559 apply(induct rule: int_gr_induct) |
560 apply simp |
560 apply simp |
561 apply arith |
|
562 apply (simp add:int_distrib) |
561 apply (simp add:int_distrib) |
563 apply arith |
|
564 done |
562 done |
565 |
563 |
566 lemma incr_lemma: "0 < (d::int) \<Longrightarrow> z < x + (abs(x-z)+1) * d" |
564 lemma incr_lemma: "0 < (d::int) \<Longrightarrow> z < x + (abs(x-z)+1) * d" |
567 apply(induct rule: int_gr_induct) |
565 apply(induct rule: int_gr_induct) |
568 apply simp |
566 apply simp |
569 apply arith |
|
570 apply (simp add:int_distrib) |
567 apply (simp add:int_distrib) |
571 apply arith |
|
572 done |
568 done |
573 |
569 |
574 lemma minusinfinity: |
570 lemma minusinfinity: |
575 assumes "0 < d" and |
571 assumes "0 < d" and |
576 P1eqP1: "ALL x k. P1 x = P1(x - k*d)" and |
572 P1eqP1: "ALL x k. P1 x = P1(x - k*d)" and |