src/HOL/ex/Gauge_Integration.thy
 changeset 46501 fe51817749d1 parent 45605 a89b4bc311a5 child 49962 a8cc904a6820
equal inserted replaced
46500:0196966d6d2d 46501:fe51817749d1
`   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 `