Theory Continuous_Interval

theory Continuous_Interval
  imports Main
begin

section ‹Continuous Intervals›

definition 
  continuous_list :: "(nat × nat) list ⇒ bool"
where
  "continuous_list xs = 
      (∀i. Suc i < length xs ⟶ fst (xs ! Suc i) = snd (xs ! i))"

lemma continuous_list_nil:
  "continuous_list []"
  by (simp add: continuous_list_def)

lemma continuous_list_singleton:
  "continuous_list [x]"
  by (simp add: continuous_list_def)

lemma continuous_list_cons:
  "continuous_list (x # xs) ⟹ continuous_list xs"
  by (simp add: continuous_list_def)

lemma continuous_list_app:
  "continuous_list (xs @ ys) ⟹ continuous_list xs ∧ continuous_list ys"
proof (induct xs)
  case Nil
  then show ?case 
    by (clarsimp simp: continuous_list_nil continuous_list_cons)
next
  case (Cons x1 xs)
  note IH1 = this(1) and
       IH2 = this(2)

  from continuous_list_cons IH2
  have "continuous_list (xs @ ys)"
    by simp
  with IH1
  have "continuous_list ys"
    by simp

  have "xs = [] ∨ xs ≠ []"
    by simp
  then show ?case
  proof
    assume "xs = []"
    with IH2 continuous_list_singleton
    have "continuous_list (x1 # xs)"
      by blast
    with ‹continuous_list ys›
    show ?thesis
      by simp
  next
    assume "xs ≠ []"
    hence "∃x xs'. xs = x # xs'"
      using neq_Nil_conv by blast
    then obtain x xs' where
      "xs = x # xs'"
      by blast

    have "continuous_list (x1 # (x # xs'))"
      unfolding continuous_list_def
    proof(intro allI impI)
      fix i
      assume "Suc i < length (x1 # (x # xs'))"
      have "i = 0 ∨ i ≠ 0"
        by blast
      then show "fst ((x1 # x # xs') ! Suc i) = snd ((x1 # x # xs') ! i)"
      proof
        assume "i = 0"
        then show ?thesis
          using IH2 ‹xs = x # xs'› continuous_list_def by auto
      next
        assume "i ≠ 0"
        then show ?thesis
          using IH1 ‹Suc i < length (x1 # x # xs')› ‹continuous_list (xs @ ys)› ‹xs = x # xs'›
                continuous_list_def
          by auto
      qed
    qed
    with ‹continuous_list ys› ‹xs = x # xs'›
    show ?thesis
      by simp
  qed
qed

lemma continuous_list_interval_1:
  assumes "continuous_list xs"
  and     "xs ≠ []"
  and     "fst (hd xs) ≤ i"
  and     "i < snd (last xs)"
  shows "∃j < length xs. fst (xs ! j) ≤ i ∧ i < snd (xs ! j)"
  using assms
proof (induct xs)
  case Nil
  then show ?case 
    by simp
next
  case (Cons x1 xs)
  note IH = this

  have "xs = [] ⟶ ?case"
  proof 
    assume "xs = []"
    with IH(4,5)
    show ?case
      by simp
  qed

  have "xs ≠ [] ⟶ ?case"
  proof
    assume "xs ≠ []"
    hence "∃a b xs'. xs = (a, b) # xs'"
      by (metis (full_types) list.exhaust surj_pair)
    then obtain a b xs' where
      "xs = (a, b) # xs'"
      by blast

    from IH(2)
    have "continuous_list xs"
      using continuous_list_cons by blast

    from IH(5) ‹xs ≠ []›
    have "i < snd (last xs)"
      by simp

    have "a ≤ i ∨ i < a"
      by linarith
    then show ?case
    proof
      assume "a ≤ i"
      with IH(1)
            [OF ‹continuous_list xs› 
                ‹xs ≠ []› _ 
                ‹i < snd (last xs)›] 
           ‹xs = (a, b) # xs'›
      show ?thesis
        by auto
    next
      assume "i < a"
      with IH(2) ‹xs = (a, b) # xs'›
      have "i < snd x1"
        using continuous_list_def by auto
      with IH(4)
      show ?thesis
        by auto
    qed
  qed

  with ‹xs = [] ⟶ ?case›
  show ?case
    by blast
qed

lemma continuous_list_interval_2:
  assumes "continuous_list xs"
  and     "length xs = Suc n"
  and     "fst (xs ! 0) ≤ i"
  and     "i < snd (xs ! n)"
  shows "∃j < length xs. fst (xs ! j) ≤ i ∧ i < snd (xs ! j)"
proof -
  from ‹length xs = Suc n›
  have "xs ≠ []"
    by auto

  from ‹fst (xs ! 0) ≤ i› ‹xs ≠ []›
  have "fst (hd xs) ≤ i"
    by (simp add: hd_conv_nth)

  from ‹i < snd (xs ! n)› 
        ‹length xs = Suc n› ‹xs ≠ []›
  have "i < snd (last xs)"
    by (simp add: last_conv_nth)

  from continuous_list_interval_1
          [OF ‹continuous_list xs› 
              ‹xs ≠ []› 
              ‹fst (hd xs) ≤ i›
              ‹i < snd (last xs)›]
  show ?thesis
    by assumption
qed

end