equal
deleted
inserted
replaced
145 |
145 |
146 lemma moment_Suc_tl: |
146 lemma moment_Suc_tl: |
147 assumes "Suc i \<le> length s" |
147 assumes "Suc i \<le> length s" |
148 shows "tl (moment (Suc i) s) = moment i s" |
148 shows "tl (moment (Suc i) s) = moment i s" |
149 using assms unfolding moment_def rev_take |
149 using assms unfolding moment_def rev_take |
150 by (simp, metis Suc_diff_le diff_Suc_Suc drop_Suc tl_drop) |
150 by (simp, metis Suc_diff_le diff_Suc_Suc drop_Suc tl_drop) |
151 |
151 |
152 lemma moment_plus: |
152 lemma moment_plus: |
153 assumes "Suc i \<le> length s" |
153 assumes "Suc i \<le> length s" |
154 shows "(moment (Suc i) s) = (hd (moment (Suc i) s)) # (moment i s)" |
154 shows "(moment (Suc i) s) = (hd (moment (Suc i) s)) # (moment i s)" |
155 proof - |
155 proof - |
156 have "(moment (Suc i) s) \<noteq> []" |
156 have "(moment (Suc i) s) \<noteq> []" using assms |
157 using assms by (auto simp add: moment_def) |
157 by (simp add:moment_def rev_take) |
158 hence "(moment (Suc i) s) = (hd (moment (Suc i) s)) # tl (moment (Suc i) s)" |
158 hence "(moment (Suc i) s) = (hd (moment (Suc i) s)) # tl (moment (Suc i) s)" |
159 by auto |
159 by auto |
160 with moment_Suc_tl[OF assms] |
160 with moment_Suc_tl[OF assms] |
161 show ?thesis by metis |
161 show ?thesis by metis |
162 qed |
162 qed |