Theory Piecewise_Continuous

section ‹Piecewise Continous Functions›
theory Piecewise_Continuous
  imports
    Laplace_Transform_Library
begin

subsection ‹at within filters›

lemma at_within_self_singleton[simp]: "at i within {i} = bot"
  by (auto intro!: antisym filter_leI simp: eventually_at_filter)

lemma at_within_t1_space_avoid:
  "(at x within X - {i}) = (at x within X)" if "x  i" for x i::"'a::t1_space"
proof (safe intro!: antisym filter_leI)
  fix P
  assume "eventually P (at x within X - {i})"
  moreover have "eventually (λx. x  i) (nhds x)"
    by (rule t1_space_nhds) fact
  ultimately
  show "eventually P (at x within X)"
    unfolding eventually_at_filter
    by eventually_elim auto
qed (simp add: eventually_mono order.order_iff_strict eventually_at_filter)

lemma at_within_t1_space_avoid_finite:
  "(at x within X - I) = (at x within X)" if "finite I" "x  I" for x::"'a::t1_space"
  using that
proof (induction I)
  case (insert i I)
  then show ?case
    by auto (metis Diff_insert at_within_t1_space_avoid)
qed simp

lemma at_within_interior:
  "NO_MATCH (UNIV::'a set) (S::'a::topological_space set)  x  interior S  at x within S = at x"
  by (rule at_within_interior)


subsection ‹intervals›

lemma Compl_Icc: "- {a .. b} = {..<a}  {b<..}" for a b::"'a::linorder"
  by auto

lemma interior_Icc[simp]: "interior {a..b} = {a<..<b}"
  for a b::"'a::{linorder_topology, dense_order, no_bot, no_top}"
    ― ‹TODO: is no_bot› and no_top› really required?›
  by (auto simp add: Compl_Icc interior_closure)

lemma closure_finite[simp]: "closure X = X" if "finite X" for X::"'a::t1_space set"
  using that
  by (induction X) (simp_all add: closure_insert)

definition piecewise_continuous_on :: "'a::linorder_topology  'a  'a set  ('a  'b::topological_space)  bool"
where "piecewise_continuous_on a b I f 
  (continuous_on ({a .. b} - I) f  finite I 
    (iI. (i  {a<..b}  (l. (f  l) (at_left i))) 
      (i  {a..<b}  (u. (f  u) (at_right i)))))"

lemma piecewise_continuous_on_subset:
  "piecewise_continuous_on a b I f  {c .. d}  {a .. b}  piecewise_continuous_on c d I f"
  by (force simp add: piecewise_continuous_on_def intro: continuous_on_subset)

lemma piecewise_continuous_onE:
  assumes "piecewise_continuous_on a b I f"
  obtains l u
  where "finite I"
      and "continuous_on ({a..b} - I) f"
      and "(i. i  I  a < i  i  b  (f  l i) (at_left i))"
      and "(i. i  I  a  i  i < b  (f  u i) (at_right i))"
  using assms
  by (auto simp: piecewise_continuous_on_def Ball_def) metis

lemma piecewise_continuous_onI:
  assumes "finite I" "continuous_on ({a..b} - I) f"
    and "(i. i  I  a < i  i  b  (f  l i) (at_left i))"
    and "(i. i  I  a  i  i < b  (f  u i) (at_right i))"
  shows "piecewise_continuous_on a b I f"
  using assms
  by (force simp: piecewise_continuous_on_def)

lemma piecewise_continuous_onI':
  fixes a b::"'a::{linorder_topology, dense_order, no_bot, no_top}"
  assumes "finite I" "x. a < x  x < b  isCont f x"
    and "a  I  continuous (at_right a) f"
    and "b  I  continuous (at_left b) f"
    and "(i. i  I  a < i  i  b  (f  l i) (at_left i))"
    and "(i. i  I  a  i  i < b  (f  u i) (at_right i))"
  shows "piecewise_continuous_on a b I f"
proof (rule piecewise_continuous_onI)
  have "x  I  a  x  x  b  (f  f x) (at x within {a..b})" for x
    using assms(2)[of x] assms(3,4)
    by (cases "a = x"; cases "b = x"; cases "x  {a<..<b}")
      (auto simp: at_within_Icc_at_left at_within_Icc_at_right isCont_def
        continuous_within filterlim_at_split at_within_interior)
  then show "continuous_on ({a .. b} - I) f"
    by (auto simp: continuous_on_def finite I at_within_t1_space_avoid_finite)
qed fact+

lemma piecewise_continuous_onE':
  fixes a b::"'a::{linorder_topology, dense_order, no_bot, no_top}"
  assumes "piecewise_continuous_on a b I f"
  obtains l u
  where "finite I"
      and "x. a < x  x < b  x  I  isCont f x"
      and "(x. a < x  x  b  (f  l x) (at_left x))"
      and "(x. a  x  x < b  (f  u x) (at_right x))"
      and "x. a  x  x  b  x  I  f x = l x"
      and "x. a  x  x  b  x  I  f x = u x"
proof -
  from piecewise_continuous_onE[OF assms] obtain l u
    where "finite I"
      and continuous: "continuous_on ({a..b} - I) f"
      and left: "(i. i  I  a < i  i  b  (f  l i) (at_left i))"
      and right: "(i. i  I  a  i  i < b  (f  u i) (at_right i))"
    by metis
  define l' where "l' x = (if x  I then l x else f x)" for x
  define u' where "u' x = (if x  I then u x else f x)" for x
  note finite I
  moreover from continuous
  have "a < x  x < b  x  I  isCont f x" for x
    by (rule continuous_on_interior) (auto simp: interior_diff finite I)
  moreover
  from continuous have "a < x  x  b  x  I  (f  f x) (at_left x)" for x
    by (cases "x = b")
     (auto simp: continuous_on_def at_within_t1_space_avoid_finite finite I
        at_within_Icc_at_left at_within_interior filterlim_at_split
        dest!: bspec[where x=x])
  then have "a < x  x  b  (f  l' x) (at_left x)" for x
    by (auto simp: l'_def left)
  moreover
  from continuous have "a  x  x < b  x  I  (f  f x) (at_right x)" for x
    by (cases "x = a")
     (auto simp: continuous_on_def at_within_t1_space_avoid_finite finite I
        at_within_Icc_at_right at_within_interior filterlim_at_split
        dest!: bspec[where x=x])
  then have "a  x  x < b  (f  u' x) (at_right x)" for x
    by (auto simp: u'_def right)
  moreover have "a  x  x  b  x  I  f x = l' x" for x by (auto simp: l'_def)
  moreover have "a  x  x  b  x  I  f x = u' x" for x by (auto simp: u'_def)
  ultimately show ?thesis ..
qed

lemma tendsto_avoid_at_within:
  "(f  l) (at x within X)"
  if "(f  l) (at x within X - {x})"
  using that
  by (auto simp: eventually_at_filter dest!: topological_tendstoD intro!: topological_tendstoI)

lemma tendsto_within_subset_eventuallyI:
  "(f  fx) (at x within X)"
  if g: "(g  gy) (at y within Y)"
    and ev: "F x in (at y within Y). f x = g x"
    and xy: "x = y"
    and fxgy: "fx = gy"
    and XY: "X - {x}  Y"
  apply (rule tendsto_avoid_at_within)
  apply (rule tendsto_within_subset[where S = "Y"])
  unfolding xy
   apply (subst tendsto_cong[OF ev ])
   apply (rule g[folded fxgy])
  apply (rule XY[unfolded xy])
  done

lemma piecewise_continuous_on_insertE:
  assumes "piecewise_continuous_on a b (insert i I) f"
  assumes "i  {a .. b}"
  obtains g h where
    "piecewise_continuous_on a i I g"
    "piecewise_continuous_on i b I h"
    "x. a  x  x < i  g x = f x"
    "x. i < x  x  b  h x = f x"
proof -
  from piecewise_continuous_onE[OF assms(1)] i  {a .. b} obtain l u where
        finite: "finite I"
    and cf: "continuous_on ({a..b} - insert i I) f"
    and l: "(i. i  I  a < i  i  b  (f  l i) (at_left i))" "i > a  (f  l i) (at_left i)"
    and u: "(i. i  I  a  i  i < b  (f  u i) (at_right i))" "i < b  (f  u i) (at_right i)"
    by auto (metis (mono_tags))

  have fl: "(f(i := x)  l j) (at_left j)" if "j  I" "a < j" "j  b" for j x
    using l(1)
    by (rule tendsto_within_subset_eventuallyI)
       (auto simp: eventually_at_filter frequently_def t1_space_nhds that)
  have fr: "(f(i := x)  u j) (at_right j)" if "j  I" "a  j" "j < b" for j x
    using u(1)
    by (rule tendsto_within_subset_eventuallyI)
       (auto simp: eventually_at_filter frequently_def t1_space_nhds that)
  from cf have tendsto: "(f  f x) (at x within {a..b} - insert i I)"
    if "x  {a .. b} - insert i I" for x using that
    by (auto simp: continuous_on_def)
  have "continuous_on ({a..i} - I) (f(i:=l i))"
    apply (cases "a = i")
    subgoal by (auto simp: continuous_on_def Diff_triv)
    unfolding continuous_on_def
    apply safe
    subgoal for x
      apply (cases "x = i")
      subgoal
        apply (rule tendsto_within_subset_eventuallyI)
            apply (rule l(2))
        by (auto simp: eventually_at_filter)
      subgoal
        apply (subst at_within_t1_space_avoid[symmetric], assumption)
        apply (rule tendsto_within_subset_eventuallyI[where y=x])
            apply (rule tendsto)
        using i  {a .. b} by (auto simp: eventually_at_filter)
      done
    done
  then have "piecewise_continuous_on a i I (f(i:=l i))"
    using i  {a .. b}
    by (auto intro!: piecewise_continuous_onI finite fl fr)

  moreover
  have "continuous_on ({i..b} - I) (f(i:=u i))"
    apply (cases "b = i")
    subgoal by (auto simp: continuous_on_def Diff_triv)
    unfolding continuous_on_def
    apply safe
    subgoal for x
      apply (cases "x = i")
      subgoal
        apply (rule tendsto_within_subset_eventuallyI)
            apply (rule u(2))
        by (auto simp: eventually_at_filter)
      subgoal
        apply (subst at_within_t1_space_avoid[symmetric], assumption)
        apply (rule tendsto_within_subset_eventuallyI[where y=x])
            apply (rule tendsto)
        using i  {a .. b} by (auto simp: eventually_at_filter)
      done
    done
  then have "piecewise_continuous_on i b I (f(i:=u i))"
    using i  {a .. b}
    by (auto intro!: piecewise_continuous_onI finite fl fr)
  moreover have "(f(i:=l i)) x = f x" if "a  x" "x < i" for x
    using that by auto
  moreover have "(f(i:=u i)) x = f x" if "i < x" "x  b" for x
    using that by auto
  ultimately show ?thesis ..
qed

lemma eventually_avoid_finite:
  "F x in at y within Y. x  I" if "finite I" for y::"'a::t1_space"
  using that
proof (induction)
  case empty
  then show ?case by simp
next
  case (insert x F)
  then show ?case
    apply (auto intro!: eventually_conj)
    apply (cases "y = x")
    subgoal by (simp add: eventually_at_filter)
    subgoal by (rule tendsto_imp_eventually_ne) (rule tendsto_ident_at)
    done
qed

lemma eventually_at_left_linorder:― ‹TODO: generalize @{thm eventually_at_left_real}
  "a > (b :: 'a :: linorder_topology)  eventually (λx. x  {b<..<a}) (at_left a)"
  unfolding eventually_at_left
  by auto

lemma eventually_at_right_linorder:― ‹TODO: generalize @{thm eventually_at_right_real}
  "a > (b :: 'a :: linorder_topology)  eventually (λx. x  {b<..<a}) (at_right b)"
  unfolding eventually_at_right
  by auto

lemma piecewise_continuous_on_congI:
  "piecewise_continuous_on a b I g"
  if "piecewise_continuous_on a b I f"
    and eq: "x. x  {a .. b} - I  g x = f x"
proof -
  from piecewise_continuous_onE[OF that(1)]
  obtain l u where finite: "finite I"
    and *:
    "continuous_on ({a..b} - I) f"
    "(i. i  I  a < i  i  b  (f  l i) (at_left i))"
    "i. i  I  a  i  i < b  (f  u i) (at_right i)"
    by blast
  note finite
  moreover
  from * have "continuous_on ({a..b} - I) g"
    using that(2)
    by (auto simp: eq cong: continuous_on_cong) (subst continuous_on_cong[OF refl eq]; assumption)
  moreover
  have "F x in at_left i. f x = g x" if "a < i" "i  b" for i
    using eventually_avoid_finite[OF finite I, of i "{..<i}"]
      eventually_at_left_linorder[OF a < i]
    by eventually_elim (subst eq, use that in auto)
  then have "i  I  a < i  i  b  (g  l i) (at_left i)" for i
    using *(2)
    by (rule Lim_transform_eventually[rotated]) auto
  moreover
  have "F x in at_right i. f x = g x" if "a  i" "i < b" for i
    using eventually_avoid_finite[OF finite I, of i "{i<..}"]
      eventually_at_right_linorder[OF i < b]
    by eventually_elim (subst eq, use that in auto)
  then have "i  I  a  i  i < b  (g  u i) (at_right i)" for i
    using *(3)
    by (rule Lim_transform_eventually[rotated]) auto
  ultimately
  show ?thesis
    by (rule piecewise_continuous_onI) auto
qed

lemma piecewise_continuous_on_cong[cong]:
  "piecewise_continuous_on a b I f  piecewise_continuous_on c d J g"
  if "a = c"
    "b = d"
    "I = J"
    "x. c  x  x  d  x  J  f x = g x"
  using that
  by (auto intro: piecewise_continuous_on_congI)

lemma tendsto_at_left_continuous_on_avoidI: "(f  g i) (at_left i)"
  if g: "continuous_on ({a..i} - I) g"
    and gf: "x. a < x  x < i  g x = f x"
    "i  I" "finite I" "a < i"
  for i::"'a::linorder_topology"
proof (rule Lim_transform_eventually)
  from that have "i  {a .. i}" by auto
  from g have "(g  g i) (at i within {a..i} - I)"
    using i  I i  {a .. i}
    by (auto elim!: piecewise_continuous_onE simp: continuous_on_def)
  then show "(g  g i) (at_left i)"
    by (metis that at_within_Icc_at_left at_within_t1_space_avoid_finite
        greaterThanLessThan_iff)
  show "F x in at_left i. g x = f x"
    using eventually_at_left_linorder[OF a < i]
    by eventually_elim (auto simp: a < i gf)
qed

lemma tendsto_at_right_continuous_on_avoidI: "(f  g i) (at_right i)"
  if g: "continuous_on ({i..b} - I) g"
    and gf: "x. i < x  x < b  g x = f x"
    "i  I" "finite I" "i < b"
  for i::"'a::linorder_topology"
proof (rule Lim_transform_eventually)
  from that have "i  {i .. b}" by auto
  from g have "(g  g i) (at i within {i..b} - I)"
    using i  I i  {i .. b}
    by (auto elim!: piecewise_continuous_onE simp: continuous_on_def)
  then show "(g  g i) (at_right i)"
    by (metis that at_within_Icc_at_right at_within_t1_space_avoid_finite
        greaterThanLessThan_iff)
  show "F x in at_right i. g x = f x"
    using eventually_at_right_linorder[OF i < b]
    by eventually_elim (auto simp: i < b gf)
qed

lemma piecewise_continuous_on_insert_leftI:
  "piecewise_continuous_on a b (insert a I) f" if "piecewise_continuous_on a b I f"
  apply (cases "a  I")
  subgoal using that by (auto dest: insert_absorb)
  subgoal
    using that
    apply (rule piecewise_continuous_onE)
    subgoal for l u
      apply (rule piecewise_continuous_onI[where u="u(a:=f a)"])
         apply (auto intro: continuous_on_subset )
      apply (rule tendsto_at_right_continuous_on_avoidI, assumption)
         apply auto
      done
    done
  done

lemma piecewise_continuous_on_insert_rightI:
  "piecewise_continuous_on a b (insert b I) f" if "piecewise_continuous_on a b I f"
  apply (cases "b  I")
  subgoal using that by (auto dest: insert_absorb)
  subgoal
    using that
    apply (rule piecewise_continuous_onE)
    subgoal for l u
      apply (rule piecewise_continuous_onI[where l="l(b:=f b)"])
         apply (auto intro: continuous_on_subset )
      apply (rule tendsto_at_left_continuous_on_avoidI, assumption)
         apply auto
      done
    done
  done

theorem piecewise_continuous_on_induct[consumes 1, case_names empty combine weaken]:
  assumes pc: "piecewise_continuous_on a b I f"
  assumes 1: "a b f. continuous_on {a .. b} f  P a b {} f"
  assumes 2: "a i b I f1 f2 f. a  i  i  b  i  I  P a i I f1  P i b I f2 
    piecewise_continuous_on a i I f1 
    piecewise_continuous_on i b I f2 
    (x. a  x  x < i  f1 x = f x) 
    (x. i < x  x  b  f2 x = f x) 
    (i > a  (f  f1 i) (at_left i)) 
    (i < b  (f  f2 i) (at_right i)) 
    P a b (insert i I) f"
  assumes 3: "a b i I f. P a b I f  finite I  i  I  P a b (insert i I) f"
  shows "P a b I f"
proof -
  from pc have "finite I"
    by (auto simp: piecewise_continuous_on_def)
  then show ?thesis
    using pc
  proof (induction I arbitrary: a b f)
    case empty
    then show ?case
      by (auto simp: piecewise_continuous_on_def 1)
  next
    case (insert i I)
    show ?case
    proof (cases "i  {a .. b}")
      case True
      from insert.prems[THEN piecewise_continuous_on_insertE, OF i  {a .. b}]
      obtain g h
        where g: "piecewise_continuous_on a i I g"
          and h: "piecewise_continuous_on i b I h"
          and gf: "x. a  x  x < i  g x = f x"
          and hf: "x. i < x  x  b  h x = f x"
        by metis
      from g have pcg: "piecewise_continuous_on a i I (f(i:=g i))"
        by (rule piecewise_continuous_on_congI) (auto simp: gf)
      from h have pch: "piecewise_continuous_on i b I (f(i:=h i))"
        by (rule piecewise_continuous_on_congI) (auto simp: hf)

      have fg: "(f  g i) (at_left i)" if "a < i"
        apply (rule tendsto_at_left_continuous_on_avoidI[where a=a and I=I])
        using g i  I a < i
        by (auto elim!: piecewise_continuous_onE simp: gf)
      have fh: "(f  h i) (at_right i)" if "i < b"
        apply (rule tendsto_at_right_continuous_on_avoidI[where b=b and I=I])
        using h i  I i < b
        by (auto elim!: piecewise_continuous_onE simp: hf)
      show ?thesis
        apply (rule 2)
        using True apply force
        using True apply force
                apply (rule insert)
               apply (rule insert.IH, rule pcg)
              apply (rule insert.IH, rule pch)
             apply fact
            apply fact
        using 3
        by (auto simp: fg fh)
    next
      case False
      with insert.prems
      have "piecewise_continuous_on a b I f"
        by (auto simp: piecewise_continuous_on_def)
      from insert.IH[OF this] show ?thesis
        by (rule 3) fact+
    qed
  qed
qed

lemma continuous_on_imp_piecewise_continuous_on:
  "continuous_on {a .. b} f  piecewise_continuous_on a b {} f"
  by (auto simp: piecewise_continuous_on_def)

lemma piecewise_continuous_on_imp_absolutely_integrable:
  fixes a b::real and f::"real  'a::euclidean_space"
  assumes "piecewise_continuous_on a b I f"
  shows "f absolutely_integrable_on {a..b}"
  using assms
proof (induction rule: piecewise_continuous_on_induct)
  case (empty a b f)
  show ?case
    by (auto intro!: absolutely_integrable_onI integrable_continuous_interval
          continuous_intros empty)
next
  case (combine a i b I f1 f2 f)
  from combine(10)
  have "f absolutely_integrable_on {a..i}"
    by (rule absolutely_integrable_spike[where S="{i}"]) (auto simp: combine)
  moreover
  from combine(11)
  have "f absolutely_integrable_on {i..b}"
    by (rule absolutely_integrable_spike[where S="{i}"]) (auto simp: combine)
  ultimately
  show ?case
    by (rule absolutely_integrable_on_combine) fact+
qed

lemma piecewise_continuous_on_integrable:
  fixes a b::real and f::"real  'a::euclidean_space"
  assumes "piecewise_continuous_on a b I f"
  shows "f integrable_on {a..b}"
  using piecewise_continuous_on_imp_absolutely_integrable[OF assms]
  unfolding absolutely_integrable_on_def by auto

lemma piecewise_continuous_on_comp:
  assumes p: "piecewise_continuous_on a b I f"
  assumes c: "x. isCont (λ(x, y). g x y) x"
  shows "piecewise_continuous_on a b I (λx. g x (f x))"
proof -
  from piecewise_continuous_onE[OF p]
  obtain l u
    where I: "finite I"
      and cf: "continuous_on ({a..b} - I) f"
      and l: "(i. i  I  a < i  i  b  (f  l i) (at_left i))"
      and u: "(i. i  I  a  i  i < b  (f  u i) (at_right i))"
    by metis
  note finite I
  moreover
  from c have cg: "continuous_on UNIV (λ(x, y). g x y)"
    using c by (auto simp: continuous_on_def isCont_def intro: tendsto_within_subset)
  then have "continuous_on ({a..b} - I) (λx. g x (f x))"
    by (intro continuous_on_compose2[OF cg, where f="λx. (x, f x)", simplified])
      (auto intro!: continuous_intros cf)
  moreover
  note tendstcomp = tendsto_compose[OF c[unfolded isCont_def], where f="λx. (x, f x)", simplified, THEN tendsto_eq_rhs]
  have "((λx. g x (f x))  g i (u i)) (at_right i)" if "i  I" "a  i" "i < b" for i
    by (rule tendstcomp) (auto intro!: tendsto_eq_intros u[OF i  I] that)
  moreover
  have "((λx. g x (f x))  g i (l i)) (at_left i)" if "i  I" "a < i" "i  b" for i
    by (rule tendstcomp) (auto intro!: tendsto_eq_intros l[OF i  I] that)
  ultimately show ?thesis
    by (intro piecewise_continuous_onI)
qed

lemma bounded_piecewise_continuous_image:
  "bounded (f ` {a .. b})"
  if "piecewise_continuous_on a b I f" for a b::real
  using that
proof (induction rule: piecewise_continuous_on_induct)
  case (empty a b f)
  then show ?case by (auto intro!: compact_imp_bounded compact_continuous_image)
next
  case (combine a i b I f1 f2 f)
  have "(f ` {a..b})  (insert (f i) (f1 ` {a..i}  f2 ` {i..b}))"
    using combine
    by (auto simp: image_iff) (metis antisym_conv atLeastAtMost_iff le_cases not_less)
  also have "bounded "
    using combine by auto
  finally (bounded_subset[rotated]) show ?case .
qed

lemma tendsto_within_eventually:
  "(f  l) (at x within X)"
  if
    "(f  l) (at x within Y)"
    "F y in at x within X. y  Y"
  using _ that(1)
proof (rule tendsto_mono)
  show "at x within X  at x within Y"
  proof (rule filter_leI)
    fix P
    assume "eventually P (at x within Y)"
    with that(2) show "eventually P (at x within X)"
      unfolding eventually_at_filter
      by eventually_elim auto
  qed
qed

lemma at_within_eq_bot_lemma:
  "at x within {b..c} = (if x < b  b > c then bot else at x within {b..c})"
  for x b c::"'a::linorder_topology"
  by (auto intro!: not_in_closure_trivial_limitI)

lemma at_within_eq_bot_lemma2:
  "at x within {a..b} = (if x > b  a > b then bot else at x within {a..b})"
  for x a b::"'a::linorder_topology"
  by (auto intro!: not_in_closure_trivial_limitI)

lemma piecewise_continuous_on_combine:
  "piecewise_continuous_on a c J f"
  if "piecewise_continuous_on a b J f" "piecewise_continuous_on b c J f"
  using that
  apply (auto elim!: piecewise_continuous_onE)
  subgoal for l u l' u'
    apply (rule piecewise_continuous_onI[where
          l="λi. if i  b then l i else l' i" and
          u="λi. if i < b then u i else u' i"])
    subgoal by force
    subgoal
      apply (rule continuous_on_subset[where s="({a .. b}  {b .. c} - J)"])
      apply (auto simp: continuous_on_def at_within_t1_space_avoid_finite)
       apply (rule Lim_Un)
      subgoal by auto
      subgoal by (subst at_within_eq_bot_lemma) auto
      apply (rule Lim_Un)
      subgoal by (subst at_within_eq_bot_lemma2) auto
      subgoal by auto
      done
    by auto
  done

lemma piecewise_continuous_on_finite_superset:
  "piecewise_continuous_on a b I f  I  J  finite J  piecewise_continuous_on a b J f"
  for a b::"'a::{linorder_topology, dense_order, no_bot, no_top}"
  apply (auto simp add: piecewise_continuous_on_def)
    apply (rule continuous_on_subset, assumption, force)
  subgoal for i
    apply (cases "i  I")
     apply (auto simp: continuous_on_def at_within_t1_space_avoid_finite)
    apply (drule bspec[where x=i])
     apply (auto simp: at_within_t1_space_avoid)
    apply (cases "i = b")
     apply (auto simp: at_within_Icc_at_left )
    apply (subst (asm) at_within_interior[where x=i])
    by (auto simp: filterlim_at_split)
  subgoal for i
    apply (cases "i  I")
     apply (auto simp: continuous_on_def at_within_t1_space_avoid_finite)
    apply (drule bspec[where x=i])
     apply (auto simp: at_within_t1_space_avoid)
    apply (cases "i = a")
     apply (auto simp: at_within_Icc_at_right)
    apply (subst (asm) at_within_interior[where x=i])
    subgoal by (simp add: interior_Icc)
    by (auto simp: filterlim_at_split)
  done

lemma piecewise_continuous_on_splitI:
  "piecewise_continuous_on a c K f"
  if
    "piecewise_continuous_on a b I f"
    "piecewise_continuous_on b c J f"
    "I  K" "J  K" "finite K"
  for a b::"'a::{linorder_topology, dense_order, no_bot, no_top}"
  apply (rule piecewise_continuous_on_combine[where b=b])
  subgoal
    by (rule piecewise_continuous_on_finite_superset, fact)
    (use that in auto elim!: piecewise_continuous_onE)
  subgoal
    by (rule piecewise_continuous_on_finite_superset, fact)
    (use that in auto elim!: piecewise_continuous_onE)
  done

end