equal
deleted
inserted
replaced
415 let ?D1 = "take N D" 
415 let ?D1 = "take N D" 
416 let ?D2 = "drop N D" 
416 let ?D2 = "drop N D" 
417 def D1 \<equiv> "take N D @ [(d, t, b)]" 
417 def D1 \<equiv> "take N D @ [(d, t, b)]" 
418 def D2 \<equiv> "(if b = e then [] else [(b, t, e)]) @ drop (Suc N) D" 
418 def D2 \<equiv> "(if b = e then [] else [(b, t, e)]) @ drop (Suc N) D" 
419 
419 
420 have "D \<noteq> []" using `N < length D` by auto 
420 from hd_drop_conv_nth[OF `N < length D`] 
421 from hd_drop_conv_nth[OF this `N < length D`] 

422 have "fst (hd ?D2) = d" using `D ! N = (d, t, e)` by auto 
421 have "fst (hd ?D2) = d" using `D ! N = (d, t, e)` by auto 
423 with fine_append_split[OF _ _ append_take_drop_id[symmetric]] 
422 with fine_append_split[OF _ _ append_take_drop_id[symmetric]] 
424 have fine1: "fine \<delta> (a,d) ?D1" and fine2: "fine \<delta> (d,c) ?D2" 
423 have fine1: "fine \<delta> (a,d) ?D1" and fine2: "fine \<delta> (d,c) ?D2" 
425 using `N < length D` fine by auto 
424 using `N < length D` fine by auto 
426 
425 