equal
deleted
inserted
replaced
144 qed |
144 qed |
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 |
149 using assms unfolding moment_def rev_take |
150 sorry |
150 by (simp, metis Suc_diff_le diff_Suc_Suc drop_Suc tl_drop) |
151 |
|
152 |
151 |
153 lemma moment_plus: |
152 lemma moment_plus: |
154 assumes "Suc i \<le> length s" |
153 assumes "Suc i \<le> length s" |
155 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)" |
156 proof - |
155 proof - |