2257 from H have xsl: "length xs = k+1" |
2257 from H have xsl: "length xs = k+1" |
2258 by (simp add: natpermute_def) |
2258 by (simp add: natpermute_def) |
2259 from i have i': "i < length (replicate (k+1) 0)" "i < k+1" |
2259 from i have i': "i < length (replicate (k+1) 0)" "i < k+1" |
2260 unfolding length_replicate by presburger+ |
2260 unfolding length_replicate by presburger+ |
2261 have "xs = replicate (k+1) 0 [i := n]" |
2261 have "xs = replicate (k+1) 0 [i := n]" |
2262 apply (rule nth_equalityI) |
2262 proof (rule nth_equalityI) |
2263 unfolding xsl length_list_update length_replicate |
2263 show "length xs = length (replicate (k + 1) 0[i := n])" |
2264 apply simp |
2264 by (metis length_list_update length_replicate xsl) |
2265 apply clarify |
2265 show "xs ! j = replicate (k + 1) 0[i := n] ! j" if "j < length xs" for j |
2266 unfolding nth_list_update[OF i'(1)] |
2266 proof (cases "j = i") |
2267 using i zxs |
2267 case True |
2268 apply (case_tac "ia = i") |
2268 then show ?thesis |
2269 apply (auto simp del: replicate.simps) |
2269 by (metis i'(1) i(2) nth_list_update) |
2270 done |
2270 next |
|
2271 case False |
|
2272 with that show ?thesis |
|
2273 by (simp add: xsl zxs del: replicate.simps split: nat.split) |
|
2274 qed |
|
2275 qed |
2271 then show "xs \<in> ?B" using i by blast |
2276 then show "xs \<in> ?B" using i by blast |
2272 qed |
2277 qed |
2273 show "?B \<subseteq> ?A" |
2278 show "?B \<subseteq> ?A" |
2274 proof |
2279 proof |
2275 fix xs |
2280 fix xs |