equal
deleted
inserted
replaced
512 from subb have sube: "m \<noteq> 0 \<Longrightarrow> ? mm. m = Suc mm & mm <= na" by arith |
512 from subb have sube: "m \<noteq> 0 \<Longrightarrow> ? mm. m = Suc mm & mm <= na" by arith |
513 show "f (s 0) (foldseq f (\<lambda>k. if k < m then s (Suc k) else foldseq f (\<lambda>k. s (Suc (k + m))) (na - m)) m) = |
513 show "f (s 0) (foldseq f (\<lambda>k. if k < m then s (Suc k) else foldseq f (\<lambda>k. s (Suc (k + m))) (na - m)) m) = |
514 foldseq f (\<lambda>k. if k < m then s k else foldseq f (\<lambda>k. s (k + m)) (Suc na - m)) m" |
514 foldseq f (\<lambda>k. if k < m then s k else foldseq f (\<lambda>k. s (k + m)) (Suc na - m)) m" |
515 apply (simp add: subd) |
515 apply (simp add: subd) |
516 apply (cases "m = 0") |
516 apply (cases "m = 0") |
517 apply (simp) |
517 apply simp |
518 apply (drule sube) |
518 apply (drule sube) |
519 apply (auto) |
519 apply auto |
520 apply (rule a) |
520 apply (rule a) |
521 by (simp add: subc cong del: if_cong) |
521 apply (simp add: subc cong del: if_weak_cong) |
|
522 done |
522 qed |
523 qed |
523 then show ?thesis using assms by simp |
524 then show ?thesis using assms by simp |
524 qed |
525 qed |
525 |
526 |
526 lemma foldseq_zerotail: |
527 lemma foldseq_zerotail: |